X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fng_assembly%2Ffreescale%2Fopcode_base_lemmas.ma;h=ebaf9ae14a52f01f8974c05390eebf7d713795e0;hb=ec07ff398325533d848da92e9dc69852d24b78a5;hp=f781ffadb7d38e28ff902749027be5eb25baed10;hpb=20fdd66303330e6209059e90b6a98af71ec29567;p=helm.git

diff --git a/helm/software/matita/contribs/ng_assembly/freescale/opcode_base_lemmas.ma b/helm/software/matita/contribs/ng_assembly/freescale/opcode_base_lemmas.ma
index f781ffadb..ebaf9ae14 100755
--- a/helm/software/matita/contribs/ng_assembly/freescale/opcode_base_lemmas.ma
+++ b/helm/software/matita/contribs/ng_assembly/freescale/opcode_base_lemmas.ma
@@ -13,18 +13,14 @@
 (**************************************************************************)
 
 (* ********************************************************************** *)
-(*                           Progetto FreeScale                           *)
+(*                          Progetto FreeScale                            *)
 (*                                                                        *)
-(* Sviluppato da:                                                         *)
-(*   Cosimo Oliboni, oliboni@cs.unibo.it                                  *)
+(*   Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it              *)
+(*   Ultima modifica: 05/08/2009                                          *)
 (*                                                                        *)
-(* Questo materiale fa parte della tesi:                                  *)
-(*   "Formalizzazione Interattiva dei Microcontroller a 8bit FreeScale"   *)
-(*                                                                        *)
-(*                    data ultima modifica 15/11/2007                     *)
 (* ********************************************************************** *)
 
-include "freescale/bool_lemmas.ma".
+include "num/bool_lemmas.ma".
 include "freescale/opcode_base.ma".
 
 (* ********************************************** *)
@@ -33,41 +29,14 @@ include "freescale/opcode_base.ma".
 
 ndefinition mcu_type_destruct_aux ≝
 Πm1,m2:mcu_type.ΠP:Prop.m1 = m2 →
- match m1 with
-  [ HC05 ⇒ match m2 with [ HC05 ⇒ P → P | _ ⇒ P ]
-  | HC08 ⇒ match m2 with [ HC08 ⇒ P → P | _ ⇒ P ]
-  | HCS08 ⇒ match m2 with [ HCS08 ⇒ P → P | _ ⇒ P ]
-  | RS08 ⇒ match m2 with [ RS08 ⇒ P → P | _ ⇒ P ]
-  ].
+ match eq_mcutype m1 m2 with [ true ⇒ P → P | false ⇒ P ].
 
-ndefinition mcu_type_destruct : mcu_type_destruct_aux.
- #m1; #m2; #P;
+ndefinition mcutype_destruct : mcu_type_destruct_aux.
+ #m1; #m2; #P; #H;
+ nrewrite < H;
  nelim m1;
- ##[ ##1: nelim m2; nnormalize; #H;
-          ##[ ##1: napply (λx:P.x)
-          ##| ##*: napply (False_ind ??);
-                   nchange with (match HC05 with [ HC05 ⇒ False | _ ⇒ True ]);
-                   nrewrite > H; nnormalize; napply I
-          ##]
- ##| ##2: nelim m2; nnormalize; #H;
-          ##[ ##2: napply (λx:P.x)
-          ##| ##*: napply (False_ind ??);
-                   nchange with (match HC08 with [ HC08 ⇒ False | _ ⇒ True ]);
-                   nrewrite > H; nnormalize; napply I
-          ##]
- ##| ##3: nelim m2; nnormalize; #H;
-          ##[ ##3: napply (λx:P.x)
-          ##| ##*: napply (False_ind ??);
-                   nchange with (match HCS08 with [ HCS08 ⇒ False | _ ⇒ True ]);
-                   nrewrite > H; nnormalize; napply I
-          ##]
- ##| ##4: nelim m2; nnormalize; #H;
-          ##[ ##4: napply (λx:P.x)
-          ##| ##*: napply (False_ind ??);
-                   nchange with (match RS08 with [ RS08 ⇒ False | _ ⇒ True ]);
-                   nrewrite > H; nnormalize; napply I
-          ##]
- ##]
+ nnormalize;
+ napply (λx.x).
 nqed.
 
 nlemma symmetric_eqmcutype : symmetricT mcu_type bool eq_mcutype.
@@ -75,7 +44,7 @@ nlemma symmetric_eqmcutype : symmetricT mcu_type bool eq_mcutype.
  nelim m1;
  nelim m2;
  nnormalize;
- napply (refl_eq ??).
+ napply refl_eq.
 nqed.
 
 nlemma eqmcutype_to_eq : ∀m1,m2:mcu_type.(eq_mcutype m1 m2 = true) → (m1 = m2).
@@ -83,8 +52,8 @@ nlemma eqmcutype_to_eq : ∀m1,m2:mcu_type.(eq_mcutype m1 m2 = true) → (m1 = m
  ncases m1;
  ncases m2;
  nnormalize;
- ##[ ##1,6,11,16: #H; napply (refl_eq ??)
- ##| ##*: #H; napply (bool_destruct ??? H)
+ ##[ ##1,6,11,16: #H; napply refl_eq
+ ##| ##*: #H; napply (bool_destruct … H)
  ##]
 nqed.
 
@@ -93,39 +62,40 @@ nlemma eq_to_eqmcutype : ∀m1,m2.m1 = m2 → eq_mcutype m1 m2 = true.
  ncases m1;
  ncases m2;
  nnormalize;
- ##[ ##1,6,11,16: #H; napply (refl_eq ??)
- ##| ##*: #H; napply (mcu_type_destruct ??? H)
+ ##[ ##1,6,11,16: #H; napply refl_eq
+ ##| ##*: #H; napply (mcutype_destruct … H)
  ##]
 nqed.
 
-nlemma instr_mode_destruct_MODE_DIRn : ∀n1,n2.MODE_DIRn n1 = MODE_DIRn n2 → n1 = n2.
- #n1; #n2; #H;
- nchange with (match MODE_DIRn n2 with [ MODE_DIRn a ⇒ n1 = a | _ ⇒ False ]);
- nrewrite < H;
- nnormalize;
- napply (refl_eq ??).
-nqed.
-
-nlemma instr_mode_destruct_MODE_DIRn_and_IMM1 : ∀n1,n2.MODE_DIRn_and_IMM1 n1 = MODE_DIRn_and_IMM1 n2 → n1 = n2.
- #n1; #n2; #H;
- nchange with (match MODE_DIRn_and_IMM1 n2 with [ MODE_DIRn_and_IMM1 a ⇒ n1 = a | _ ⇒ False ]);
- nrewrite < H;
+nlemma decidable_mcutype : ∀x,y:mcu_type.decidable (x = y).
+ #x; #y;
  nnormalize;
- napply (refl_eq ??).
+ nelim x;
+ nelim y;
+ ##[ ##1,6,11,16: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
+ ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …);
+          nnormalize; #H;
+          napply False_ind;
+          napply (mcutype_destruct … H)
+ ##]
 nqed.
 
-nlemma instr_mode_destruct_MODE_TNY : ∀e1,e2.MODE_TNY e1 = MODE_TNY e2 → e1 = e2.
- #e1; #e2; #H;
- nchange with (match MODE_TNY e2 with [ MODE_TNY a ⇒ e1 = a | _ ⇒ False ]);
- nrewrite < H;
+nlemma neqmcutype_to_neq : ∀m1,m2:mcu_type.(eq_mcutype m1 m2 = false) → (m1 ≠ m2).
+ #m1; #m2;
+ ncases m1;
+ ncases m2;
  nnormalize;
- napply (refl_eq ??).
+ ##[ ##1,6,11,16: #H; napply (bool_destruct … H)
+ ##| ##*: #H; #H1; napply (mcutype_destruct … H1)
+ ##]
 nqed.
 
-nlemma instr_mode_destruct_MODE_SRT : ∀t1,t2.MODE_SRT t1 = MODE_SRT t2 → t1 = t2.
- #t1; #t2; #H;
- nchange with (match MODE_SRT t2 with [ MODE_SRT a ⇒ t1 = a | _ ⇒ False ]);
- nrewrite < H;
+nlemma neq_to_neqmcutype : ∀m1,m2.m1 ≠ m2 → eq_mcutype m1 m2 = false.
+ #m1; #m2;
+ ncases m1;
+ ncases m2;
  nnormalize;
- napply (refl_eq ??).
+ ##[ ##1,6,11,16: #H; nelim (H (refl_eq …))
+ ##| ##*: #H; napply refl_eq
+ ##]
 nqed.