X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fng_assembly%2Ffreescale%2Fexadecim_lemmas.ma;h=3726219a8c02a6002edbbddb64db2b0ed3a12217;hb=ee9a771a3cf2124ef65906ae75eb0ba7e2e4303b;hp=19f9dc96073e61f82dd2b35f745df67f6d208b46;hpb=64bdbee95e40a5be3bb6c5c2866869103730a4d0;p=helm.git

diff --git a/helm/software/matita/contribs/ng_assembly/freescale/exadecim_lemmas.ma b/helm/software/matita/contribs/ng_assembly/freescale/exadecim_lemmas.ma
index 19f9dc960..3726219a8 100755
--- a/helm/software/matita/contribs/ng_assembly/freescale/exadecim_lemmas.ma
+++ b/helm/software/matita/contribs/ng_assembly/freescale/exadecim_lemmas.ma
@@ -13,15 +13,11 @@
 (**************************************************************************)
 
 (* ********************************************************************** *)
-(*                           Progetto FreeScale                           *)
+(*                          Progetto FreeScale                            *)
 (*                                                                        *)
-(* Sviluppato da:                                                         *)
-(*   Cosimo Oliboni, oliboni@cs.unibo.it                                  *)
+(*   Sviluppato da: Cosimo Oliboni, oliboni@cs.unibo.it                   *)
+(*     Cosimo Oliboni, oliboni@cs.unibo.it                                *)
 (*                                                                        *)
-(* Questo materiale fa parte della tesi:                                  *)
-(*   "Formalizzazione Interattiva dei Microcontroller a 8bit FreeScale"   *)
-(*                                                                        *)
-(*                    data ultima modifica 15/11/2007                     *)
 (* ********************************************************************** *)
 
 include "freescale/bool_lemmas.ma".
@@ -31,8 +27,152 @@ include "freescale/exadecim.ma".
 (* ESADECIMALI *)
 (* *********** *)
 
-ndefinition exadecim_destruct :
- Πe1,e2:exadecim.ΠP:Prop.e1 = e2 →
+ndefinition exadecim_destruct1 : Πe2.ΠP:Prop.ΠH:x0 = e2.match e2 with [ x0 ⇒ P → P | _ ⇒ P ].
+ #e2; #P; ncases e2; nnormalize; #H;
+ ##[ ##1: napply (λx:P.x)
+ ##| ##*: napply (False_ind ??);
+          nchange with (match x0 with [ x0 ⇒ False | _ ⇒ True ]);
+          nrewrite > H; nnormalize; napply I
+ ##]
+nqed.
+
+ndefinition exadecim_destruct2 : Πe2.ΠP:Prop.ΠH:x1 = e2.match e2 with [ x1 ⇒ P → P | _ ⇒ P ].
+ #e2; #P; ncases e2; nnormalize; #H;
+ ##[ ##2: napply (λx:P.x)
+ ##| ##*: napply (False_ind ??);
+          nchange with (match x1 with [ x1 ⇒ False | _ ⇒ True ]);
+          nrewrite > H; nnormalize; napply I
+ ##]
+nqed.
+
+ndefinition exadecim_destruct3 : Πe2.ΠP:Prop.ΠH:x2 = e2.match e2 with [ x2 ⇒ P → P | _ ⇒ P ].
+ #e2; #P; ncases e2; nnormalize; #H;
+ ##[ ##3: napply (λx:P.x)
+ ##| ##*: napply (False_ind ??);
+          nchange with (match x2 with [ x2 ⇒ False | _ ⇒ True ]);
+          nrewrite > H; nnormalize; napply I
+ ##]
+nqed.
+
+ndefinition exadecim_destruct4 : Πe2.ΠP:Prop.ΠH:x3 = e2.match e2 with [ x3 ⇒ P → P | _ ⇒ P ].
+ #e2; #P; ncases e2; nnormalize; #H;
+ ##[ ##4: napply (λx:P.x)
+ ##| ##*: napply (False_ind ??);
+          nchange with (match x3 with [ x3 ⇒ False | _ ⇒ True ]);
+          nrewrite > H; nnormalize; napply I
+ ##]
+nqed.
+
+ndefinition exadecim_destruct5 : Πe2.ΠP:Prop.ΠH:x4 = e2.match e2 with [ x4 ⇒ P → P | _ ⇒ P ].
+ #e2; #P; ncases e2; nnormalize; #H;
+ ##[ ##5: napply (λx:P.x)
+ ##| ##*: napply (False_ind ??);
+          nchange with (match x4 with [ x4 ⇒ False | _ ⇒ True ]);
+          nrewrite > H; nnormalize; napply I
+ ##]
+nqed.
+
+ndefinition exadecim_destruct6 : Πe2.ΠP:Prop.ΠH:x5 = e2.match e2 with [ x5 ⇒ P → P | _ ⇒ P ].
+ #e2; #P; ncases e2; nnormalize; #H;
+ ##[ ##6: napply (λx:P.x)
+ ##| ##*: napply (False_ind ??);
+          nchange with (match x5 with [ x5 ⇒ False | _ ⇒ True ]);
+          nrewrite > H; nnormalize; napply I
+ ##]
+nqed.
+
+ndefinition exadecim_destruct7 : Πe2.ΠP:Prop.ΠH:x6 = e2.match e2 with [ x6 ⇒ P → P | _ ⇒ P ].
+ #e2; #P; ncases e2; nnormalize; #H;
+ ##[ ##7: napply (λx:P.x)
+ ##| ##*: napply (False_ind ??);
+          nchange with (match x6 with [ x6 ⇒ False | _ ⇒ True ]);
+          nrewrite > H; nnormalize; napply I
+ ##]
+nqed.
+
+ndefinition exadecim_destruct8 : Πe2.ΠP:Prop.ΠH:x7 = e2.match e2 with [ x7 ⇒ P → P | _ ⇒ P ].
+ #e2; #P; ncases e2; nnormalize; #H;
+ ##[ ##8: napply (λx:P.x)
+ ##| ##*: napply (False_ind ??);
+          nchange with (match x7 with [ x7 ⇒ False | _ ⇒ True ]);
+          nrewrite > H; nnormalize; napply I
+ ##]
+nqed.
+
+ndefinition exadecim_destruct9 : Πe2.ΠP:Prop.ΠH:x8 = e2.match e2 with [ x8 ⇒ P → P | _ ⇒ P ].
+ #e2; #P; ncases e2; nnormalize; #H;
+ ##[ ##9: napply (λx:P.x)
+ ##| ##*: napply (False_ind ??);
+          nchange with (match x8 with [ x8 ⇒ False | _ ⇒ True ]);
+          nrewrite > H; nnormalize; napply I
+ ##]
+nqed.
+
+ndefinition exadecim_destruct10 : Πe2.ΠP:Prop.ΠH:x9 = e2.match e2 with [ x9 ⇒ P → P | _ ⇒ P ].
+ #e2; #P; ncases e2; nnormalize; #H;
+ ##[ ##10: napply (λx:P.x)
+ ##| ##*: napply (False_ind ??);
+          nchange with (match x9 with [ x9 ⇒ False | _ ⇒ True ]);
+          nrewrite > H; nnormalize; napply I
+ ##]
+nqed.
+
+ndefinition exadecim_destruct11 : Πe2.ΠP:Prop.ΠH:xA = e2.match e2 with [ xA ⇒ P → P | _ ⇒ P ].
+ #e2; #P; ncases e2; nnormalize; #H;
+ ##[ ##11: napply (λx:P.x)
+ ##| ##*: napply (False_ind ??);
+          nchange with (match xA with [ xA ⇒ False | _ ⇒ True ]);
+          nrewrite > H; nnormalize; napply I
+ ##]
+nqed.
+
+ndefinition exadecim_destruct12 : Πe2.ΠP:Prop.ΠH:xB = e2.match e2 with [ xB ⇒ P → P | _ ⇒ P ].
+ #e2; #P; ncases e2; nnormalize; #H;
+ ##[ ##12: napply (λx:P.x)
+ ##| ##*: napply (False_ind ??);
+          nchange with (match xB with [ xB ⇒ False | _ ⇒ True ]);
+          nrewrite > H; nnormalize; napply I
+ ##]
+nqed.
+
+ndefinition exadecim_destruct13 : Πe2.ΠP:Prop.ΠH:xC = e2.match e2 with [ xC ⇒ P → P | _ ⇒ P ].
+ #e2; #P; ncases e2; nnormalize; #H;
+ ##[ ##13: napply (λx:P.x)
+ ##| ##*: napply (False_ind ??);
+          nchange with (match xC with [ xC ⇒ False | _ ⇒ True ]);
+          nrewrite > H; nnormalize; napply I
+ ##]
+nqed.
+
+ndefinition exadecim_destruct14 : Πe2.ΠP:Prop.ΠH:xD = e2.match e2 with [ xD ⇒ P → P | _ ⇒ P ].
+ #e2; #P; ncases e2; nnormalize; #H;
+ ##[ ##14: napply (λx:P.x)
+ ##| ##*: napply (False_ind ??);
+          nchange with (match xD with [ xD ⇒ False | _ ⇒ True ]);
+          nrewrite > H; nnormalize; napply I
+ ##]
+nqed.
+
+ndefinition exadecim_destruct15 : Πe2.ΠP:Prop.ΠH:xE = e2.match e2 with [ xE ⇒ P → P | _ ⇒ P ].
+ #e2; #P; ncases e2; nnormalize; #H;
+ ##[ ##15: napply (λx:P.x)
+ ##| ##*: napply (False_ind ??);
+          nchange with (match xE with [ xE ⇒ False | _ ⇒ True ]);
+          nrewrite > H; nnormalize; napply I
+ ##]
+nqed.
+
+ndefinition exadecim_destruct16 : Πe2.ΠP:Prop.ΠH:xF = e2.match e2 with [ xF ⇒ P → P | _ ⇒ P ].
+ #e2; #P; ncases e2; nnormalize; #H;
+ ##[ ##16: napply (λx:P.x)
+ ##| ##*: napply (False_ind ??);
+          nchange with (match xF with [ xF ⇒ False | _ ⇒ True ]);
+          nrewrite > H; nnormalize; napply I
+ ##]
+nqed.
+
+ndefinition exadecim_destruct_aux ≝
+Πe1,e2.ΠP:Prop.ΠH:e1 = e2.
  match e1 with
   [ x0 ⇒ match e2 with [ x0 ⇒ P → P | _ ⇒ P ]
   | x1 ⇒ match e2 with [ x1 ⇒ P → P | _ ⇒ P ]
@@ -51,104 +191,25 @@ ndefinition exadecim_destruct :
   | xE ⇒ match e2 with [ xE ⇒ P → P | _ ⇒ P ]
   | xF ⇒ match e2 with [ xF ⇒ P → P | _ ⇒ P ]
   ].
- #e1; #e2; #P;
- nelim e1;
- ##[ ##1: nelim e2; nnormalize; #H;
-          ##[ ##1: napply (λx:P.x)
-          ##| ##*: napply (False_ind ??);
-                   nchange with (match x0 with [ x0 ⇒ False | _ ⇒ True ]);
-                   nrewrite > H; nnormalize; napply I
-          ##]
- ##| ##2: nelim e2; nnormalize; #H;
-          ##[ ##2: napply (λx:P.x)
-          ##| ##*: napply (False_ind ??);
-                   nchange with (match x1 with [ x1 ⇒ False | _ ⇒ True ]);
-                   nrewrite > H; nnormalize; napply I
-          ##]
- ##| ##3: nelim e2; nnormalize; #H;
-          ##[ ##3: napply (λx:P.x)
-          ##| ##*: napply (False_ind ??);
-                   nchange with (match x2 with [ x2 ⇒ False | _ ⇒ True ]);
-                   nrewrite > H; nnormalize; napply I
-          ##]
- ##| ##4: nelim e2; nnormalize; #H;
-          ##[ ##4: napply (λx:P.x)
-          ##| ##*: napply (False_ind ??);
-                   nchange with (match x3 with [ x3 ⇒ False | _ ⇒ True ]);
-                   nrewrite > H; nnormalize; napply I
-          ##]
- ##| ##5: nelim e2; nnormalize; #H;
-          ##[ ##5: napply (λx:P.x)
-          ##| ##*: napply (False_ind ??);
-                   nchange with (match x4 with [ x4 ⇒ False | _ ⇒ True ]);
-                   nrewrite > H; nnormalize; napply I
-          ##]
- ##| ##6: nelim e2; nnormalize; #H;
-          ##[ ##6: napply (λx:P.x)
-          ##| ##*: napply (False_ind ??);
-                   nchange with (match x5 with [ x5 ⇒ False | _ ⇒ True ]);
-                   nrewrite > H; nnormalize; napply I
-          ##]
- ##| ##7: nelim e2; nnormalize; #H;
-          ##[ ##7: napply (λx:P.x)
-          ##| ##*: napply (False_ind ??);
-                   nchange with (match x6 with [ x6 ⇒ False | _ ⇒ True ]);
-                   nrewrite > H; nnormalize; napply I
-          ##]
- ##| ##8: nelim e2; nnormalize; #H;
-          ##[ ##8: napply (λx:P.x)
-          ##| ##*: napply (False_ind ??);
-                   nchange with (match x7 with [ x7 ⇒ False | _ ⇒ True ]);
-                   nrewrite > H; nnormalize; napply I
-          ##]
- ##| ##9: nelim e2; nnormalize; #H;
-          ##[ ##9: napply (λx:P.x)
-          ##| ##*: napply (False_ind ??);
-                   nchange with (match x8 with [ x8 ⇒ False | _ ⇒ True ]);
-                   nrewrite > H; nnormalize; napply I
-          ##]
- ##| ##10: nelim e2; nnormalize; #H;
-          ##[ ##10: napply (λx:P.x)
-          ##| ##*: napply (False_ind ??);
-                   nchange with (match x9 with [ x9 ⇒ False | _ ⇒ True ]);
-                   nrewrite > H; nnormalize; napply I
-          ##]
- ##| ##11: nelim e2; nnormalize; #H;
-          ##[ ##11: napply (λx:P.x)
-          ##| ##*: napply (False_ind ??);
-                   nchange with (match xA with [ xA ⇒ False | _ ⇒ True ]);
-                   nrewrite > H; nnormalize; napply I
-          ##]
- ##| ##12: nelim e2; nnormalize; #H;
-          ##[ ##12: napply (λx:P.x)
-          ##| ##*: napply (False_ind ??);
-                   nchange with (match xB with [ xB ⇒ False | _ ⇒ True ]);
-                   nrewrite > H; nnormalize; napply I
-          ##]
- ##| ##13: nelim e2; nnormalize; #H;
-          ##[ ##13: napply (λx:P.x)
-          ##| ##*: napply (False_ind ??);
-                   nchange with (match xC with [ xC ⇒ False | _ ⇒ True ]);
-                   nrewrite > H; nnormalize; napply I
-          ##]
- ##| ##14: nelim e2; nnormalize; #H;
-          ##[ ##14: napply (λx:P.x)
-          ##| ##*: napply (False_ind ??);
-                   nchange with (match xD with [ xD ⇒ False | _ ⇒ True ]);
-                   nrewrite > H; nnormalize; napply I
-          ##]
- ##| ##15: nelim e2; nnormalize; #H;
-          ##[ ##15: napply (λx:P.x)
-          ##| ##*: napply (False_ind ??);
-                   nchange with (match xE with [ xE ⇒ False | _ ⇒ True ]);
-                   nrewrite > H; nnormalize; napply I
-          ##]
- ##| ##16: nelim e2; nnormalize; #H;
-          ##[ ##16: napply (λx:P.x)
-          ##| ##*: napply (False_ind ??);
-                   nchange with (match xF with [ xF ⇒ False | _ ⇒ True ]);
-                   nrewrite > H; nnormalize; napply I
-          ##]
+
+ndefinition exadecim_destruct : exadecim_destruct_aux.
+ #e1; ncases e1;
+ ##[ ##1: napply exadecim_destruct1
+ ##| ##2: napply exadecim_destruct2
+ ##| ##3: napply exadecim_destruct3
+ ##| ##4: napply exadecim_destruct4
+ ##| ##5: napply exadecim_destruct5
+ ##| ##6: napply exadecim_destruct6
+ ##| ##7: napply exadecim_destruct7
+ ##| ##8: napply exadecim_destruct8
+ ##| ##9: napply exadecim_destruct9
+ ##| ##10: napply exadecim_destruct10
+ ##| ##11: napply exadecim_destruct11
+ ##| ##12: napply exadecim_destruct12
+ ##| ##13: napply exadecim_destruct13
+ ##| ##14: napply exadecim_destruct14
+ ##| ##15: napply exadecim_destruct15
+ ##| ##16: napply exadecim_destruct16
  ##]
 nqed.
 
@@ -382,23 +443,21 @@ nlemma symmetric_plusex_d_c : ∀e1,e2.plus_ex_d_c e1 e2 = plus_ex_d_c e2 e1.
 nqed.
 
 nlemma eqex_to_eq : ∀e1,e2:exadecim.(eq_ex e1 e2 = true) → (e1 = e2).
- #e1; #e2; #H;
- nletin K ≝ (bool_destruct ?? (e1 = e2) H);
- nelim e1 in K:(%) ⊢ %;
- nelim e2;
+ #e1; #e2;
+ ncases e1;
+ ncases e2;
  nnormalize;
  ##[ ##1,18,35,52,69,86,103,120,137,154,171,188,205,222,239,256: #H; napply (refl_eq ??)
- ##| ##*: #H; napply H
+ ##| ##*: #H; napply (bool_destruct ??? H)
  ##]
 nqed.
 
 nlemma eq_to_eqex : ∀e1,e2.e1 = e2 → eq_ex e1 e2 = true.
- #e1; #e2; #H;
- nletin K ≝ (exadecim_destruct ?? (eq_ex e1 e2 = true) H);
- nelim e1 in K:(%) ⊢ %;
- nelim e2;
+ #m1; #m2;
+ ncases m1;
+ ncases m2;
  nnormalize;
  ##[ ##1,18,35,52,69,86,103,120,137,154,171,188,205,222,239,256: #H; napply (refl_eq ??)
- ##| ##*: #H; napply H
+ ##| ##*: #H; napply (exadecim_destruct ??? H)
  ##]
 nqed.