freescale porting, work in progress

[helm.git] / helm / software / matita / contribs / ng_assembly / freescale / opcode_base_lemmas.ma

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 ce4e00642433efa96e0e1aab9fb3361bda074e55..ebaf9ae14a52f01f8974c05390eebf7d713795e0 100755 (executable)
--- a/helm/software/matita/contribs/ng_assembly/freescale/opcode_base_lemmas.ma
+++ b/helm/software/matita/contribs/ng_assembly/freescale/opcode_base_lemmas.ma
@@ -29,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.
@@ -90,38 +63,39 @@ nlemma eq_to_eqmcutype : ∀m1,m2.m1 = m2 → eq_mcutype m1 m2 = true.
  ncases m2;
  nnormalize;
  ##[ ##1,6,11,16: #H; napply refl_eq
- ##| ##*: #H; napply (mcu_type_destruct … H)
+ ##| ##*: #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.