BDD

diff --git a/helm/software/matita/contribs/didactic/shannon.ma b/helm/software/matita/contribs/didactic/shannon.ma
index e35f8046ed198fc6a05781c2833be181e5478340..be31459eba4f78964e5672ff092dd13e93d322f2 100644 (file)
--- a/helm/software/matita/contribs/didactic/shannon.ma
+++ b/helm/software/matita/contribs/didactic/shannon.ma
@@ -99,13 +99,11 @@ lemma sem_le_1 : ∀F,v.[[F]]_v ≤ 1. intros; cases (sem_bool F v); rewrite > H
 let rec subst (x:nat) (G: Formula) (F: Formula) on F ≝
  match F with
   [ FBot ⇒ FBot
-  | FTop ⇒ (*BEGIN*)FTop(*END*)
-  | FAtom n ⇒ if (*BEGIN*)eqb n x(*END*) then (*BEGIN*)G(*END*) else ((*BEGIN*)FAtom n(*END*))
-  (*BEGIN*)
+  | FTop ⇒ FTop
+  | FAtom n ⇒ if eqb n x then G else (FAtom n)
   | FAnd F1 F2 ⇒ FAnd (subst x G F1) (subst x G F2)
   | FOr F1 F2 ⇒ FOr (subst x G F1) (subst x G F2)
   | FImpl F1 F2 ⇒ FImpl (subst x G F1) (subst x G F2)
-  (*END*)
   | FNot F ⇒ FNot (subst x G F)
   ].
   
@@ -376,3 +374,36 @@ case FNot.
       change with ([[ FNot f ]]_v = [[ FNot f ]]_v).
     done.
 qed.
+
+let rec maxatom (F : Formula) on F : ℕ ≝
+  match F with
+  [ FTop ⇒ 0
+  | FBot ⇒ 0
+  | FAtom n ⇒ n
+  | FAnd F1 F2 ⇒ max (maxatom F1) (maxatom F2)
+  | FOr F1 F2 ⇒ max (maxatom F1) (maxatom F2)
+  | FImpl F1 F2 ⇒ max (maxatom F1) (maxatom F2)
+  | FNot F1 ⇒ maxatom F1
+  ]
+.
+
+let rec expandall (F : Formula) (v : ℕ → ℕ) (n : nat) on n: Formula ≝
+  match n with
+  [ O ⇒ F
+  | S m ⇒ 
+      if eqb [[ FAtom n ]]_v 0 
+      then (expandall F v m)[FBot/n] 
+      else ((expandall F v m)[FTop/n])
+  ]
+.
+
+lemma BDD : ∀F,n,v. [[ expandall F v n ]]_v = [[ F ]]_v.
+intros; elim n; simplify; [reflexivity]
+cases (sem_bool (FAtom (S n1)) v); simplify in H1; rewrite > H1; simplify;
+[ lapply (shannon (expandall F v n1) (S n1) v);
+  simplify in Hletin; rewrite > H1 in Hletin; simplify in Hletin;
+  rewrite > Hletin; assumption;
+| lapply (shannon (expandall F v n1) (S n1) v);
+  simplify in Hletin; rewrite > H1 in Hletin; simplify in Hletin;
+  rewrite > Hletin; assumption;]
+qed.