X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fng_assembly%2Ffreescale%2Fopcode_base_lemmas1.ma;h=78a284c30224a49246ee638633eb3bf76d543e1e;hb=ec07ff398325533d848da92e9dc69852d24b78a5;hp=39a9baf8b3ed05316d2de7b34c71f1beaf7a14fe;hpb=c3fc204cc02f1031b5d17fb0f2be1fc01e5c452f;p=helm.git

diff --git a/helm/software/matita/contribs/ng_assembly/freescale/opcode_base_lemmas1.ma b/helm/software/matita/contribs/ng_assembly/freescale/opcode_base_lemmas1.ma
index 39a9baf8b..78a284c30 100755
--- a/helm/software/matita/contribs/ng_assembly/freescale/opcode_base_lemmas1.ma
+++ b/helm/software/matita/contribs/ng_assembly/freescale/opcode_base_lemmas1.ma
@@ -13,85 +13,196 @@
 (**************************************************************************)
 
 (* ********************************************************************** *)
-(*                           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 "freescale/opcode_base.ma".
+include "freescale/opcode_base_lemmas_opcode.ma".
+include "freescale/opcode_base_lemmas_instrmode.ma".
+include "num/word16_lemmas.ma".
 
 (* ********************************************** *)
 (* MATTONI BASE PER DEFINIRE LE TABELLE DELLE MCU *)
 (* ********************************************** *)
 
-ndefinition mcu_type_destruct :
- Π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 ]
-  ].
- #m1; #m2; #P;
- 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
-          ##]
+nlemma anyop_destruct : ∀m.∀x1,x2:opcode.anyOP m x1 = anyOP m x2 → x1 = x2.
+ #m; #x1; #x2; #H;
+ nchange with (match anyOP m x2 with [ anyOP a ⇒ x1 = a ]);
+ nrewrite < H;
+ nnormalize;
+ napply refl_eq.
+nqed.
+
+nlemma symmetric_eqanyop : ∀m.∀op1,op2:any_opcode m.eq_anyop m op1 op2 = eq_anyop m op2 op1.
+ #m;
+ ncases m;
+ #op1; #op2;
+ ncases op1;
+ #x1;
+ ncases op2;
+ #x2;
+ nchange with (eq_op x1 x2 = eq_op x2 x1);
+ nrewrite > (symmetric_eqop x1 x2);
+ napply refl_eq.
+nqed.
+
+nlemma eqanyop_to_eq : ∀m.∀op1,op2:any_opcode m.eq_anyop m op1 op2 = true → op1 = op2.
+ #m;
+ ncases m;
+ #op1; #op2;
+ ncases op1;
+ #x1;
+ ncases op2;
+ #x2;
+ nchange with ((eq_op x1 x2 = true) → ?);
+ #H;
+ nrewrite > (eqop_to_eq … H);
+ napply refl_eq.
+nqed.
+
+nlemma eq_to_eqanyop : ∀m.∀op1,op2:any_opcode m.op1 = op2 → eq_anyop m op1 op2 = true.
+ #m;
+ ncases m;
+ #op1; #op2;
+ ncases op1;
+ #p1;
+ ncases op2;
+ #p2; #H;
+ nrewrite > (anyop_destruct … H);
+ nchange with (eq_op p2 p2 = true);
+ nrewrite > (eq_to_eqop p2 p2 (refl_eq opcode p2));
+ napply refl_eq.
+nqed.
+
+nlemma decidable_anyop : ∀m.∀x,y:any_opcode m.decidable (x = y).
+ #m; #x; nelim x; #e1; #y; nelim y; #e2;
+ nnormalize;
+ napply (or2_elim (? = ?) (? ≠ ?) ? (decidable_op e1 e2) …);
+ ##[ ##2: #H; napply (or2_intro2 (? = ?) (? ≠ ?) … ); nnormalize; #H1; napply (H (anyop_destruct m … H1))
+ ##| ##1: #H; nrewrite > H; napply (or2_intro1 (? = ?) (? ≠ ?) (refl_eq …))
  ##]
 nqed.
 
-nlemma symmetric_eqmcutype : symmetricT mcu_type bool eq_mcutype.
- #m1; #m2;
- nelim m1;
- nelim m2;
+nlemma neqanyop_to_neq : ∀m.∀op1,op2:any_opcode m.(eq_anyop m op1 op2 = false) → (op1 ≠ op2).
+ #m; #op1; nelim op1; #e1; #op2; nelim op2; #e2;
+ nchange with (((eq_op e1 e2) = false) → ?);
+ #H;
+ nnormalize;
+ #H1;
+ napply (neqop_to_neq … H);
+ napply (anyop_destruct m … H1).
+nqed.
+
+nlemma neq_to_neqanyop : ∀m.∀op1,op2:any_opcode m.op1 ≠ op2 → eq_anyop m op1 op2 = false.
+ #m; #op1; nelim op1; #e1; #op2; nelim op2; #e2;
+ #H; nchange with ((eq_op e1 e2) = false);
+ napply (neq_to_neqop e1 e2 ?);
+ nnormalize;
+ #H1;
+ nrewrite > H1 in H:(%); #H;
+ napply (H (refl_eq …)).
+nqed.
+
+nlemma b8w16_destruct_b8_b8 : ∀x1,x2.Byte x1 = Byte x2 → x1 = x2.
+ #x1; #x2; #H;
+ nchange with (match Byte x2 with [ Byte a ⇒ x1 = a | Word _ ⇒ False ]);
+ nrewrite < H;
+ nnormalize;
+ napply refl_eq.
+nqed.
+
+nlemma b8w16_destruct_w16_w16 : ∀x1,x2.Word x1 = Word x2 → x1 = x2.
+ #x1; #x2; #H;
+ nchange with (match Word x2 with [ Word a ⇒ x1 = a | Byte _ ⇒ False ]);
+ nrewrite < H;
+ nnormalize;
+ napply refl_eq.
+nqed.
+
+nlemma b8w16_destruct_b8_w16 : ∀x1,x2.Byte x1 = Word x2 → False.
+ #x1; #x2; #H;
+ nchange with (match Byte x1 with [ Word _ ⇒ True | Byte a ⇒ False ]);
+ nrewrite > H;
  nnormalize;
- napply (refl_eq ??).
+ napply I.
 nqed.
 
-nlemma eqmcutype_to_eq : ∀m1,m2:mcu_type.(eq_mcutype m1 m2 = true) → (m1 = m2).
- #m1; #m2;
- ncases m1;
- ncases m2;
+nlemma b8w16_destruct_w16_b8 : ∀x1,x2.Word x1 = Byte x2 → False.
+ #x1; #x2; #H;
+ nchange with (match Word x1 with [ Word a ⇒ False | Byte _ ⇒ True ]);
+ nrewrite > H;
  nnormalize;
- ##[ ##1,6,11,16: #H; napply (refl_eq ??)
- ##| ##*: #H; napply (bool_destruct ??? H)
+ napply I.
+nqed.
+
+nlemma symmetric_eqb8w16 : ∀bw1,bw2.eq_b8w16 bw1 bw2 = eq_b8w16 bw2 bw1.
+ #bw1; #bw2;
+ ncases bw1;
+ #x1;
+ ncases bw2;
+ #x2;
+ ##[ ##1: nchange with (eq_b8 x1 x2 = eq_b8 x2 x1);
+          nrewrite > (symmetric_eqb8 x1 x2);
+          napply refl_eq
+ ##| ##2,3: nnormalize; napply refl_eq
+ ##| ##4: nchange with (eq_w16 x1 x2 = eq_w16 x2 x1);
+          nrewrite > (symmetric_eqw16 x1 x2);
+          napply refl_eq
+ ##]
+nqed.
+
+nlemma eqb8w16_to_eq : ∀bw1,bw2.eq_b8w16 bw1 bw2 = true → bw1 = bw2.
+ #bw1; #bw2;
+ ncases bw1; #e1; ncases bw2; #e2;
+ ##[ ##1: nchange with ((eq_b8 e1 e2 = true) → ?); #H; nrewrite > (eqb8_to_eq … H); napply refl_eq
+ ##| ##2,3: nnormalize; #H; napply (bool_destruct … H)
+ ##| ##4: nchange with ((eq_w16 e1 e2 = true) → ?); #H; nrewrite > (eqw16_to_eq … H); napply refl_eq
+ ##]
+nqed.
+
+nlemma eq_to_eqb8w16 : ∀bw1,bw2.bw1 = bw2 → eq_b8w16 bw1 bw2 = true.
+ #bw1; #bw2;
+ ncases bw1; #e1; ncases bw2; #e2;
+ ##[ ##1: #H; nrewrite > (b8w16_destruct_b8_b8 … H);
+          nchange with (eq_b8 e2 e2 = true);
+          nrewrite > (eq_to_eqb8 e2 e2 (refl_eq …));
+          napply refl_eq
+ ##| ##2: #H; nelim (b8w16_destruct_b8_w16 … H)
+ ##| ##3: #H; nelim (b8w16_destruct_w16_b8 … H);
+ ##| ##4: #H; nrewrite > (b8w16_destruct_w16_w16 … H);
+          nchange with (eq_w16 e2 e2 = true);
+          nrewrite > (eq_to_eqw16 e2 e2 (refl_eq …));
+          napply refl_eq
  ##]
 nqed.
 
-nlemma eq_to_eqmcutype : ∀m1,m2.m1 = m2 → eq_mcutype m1 m2 = true.
- #m1; #m2;
- ncases m1;
- ncases m2;
+nlemma decidable_b8w16 : ∀x,y:byte8_or_word16.decidable (x = y).
+ #x; nelim x; #e1; #y; nelim y; #e2;
  nnormalize;
- ##[ ##1,6,11,16: #H; napply (refl_eq ??)
- ##| ##*: #H; napply (mcu_type_destruct ??? H)
+ ##[ ##1: napply (or2_elim (? = ?) (? ≠ ?) ? (decidable_b8 e1 e2) …);
+          ##[ ##2: #H; napply (or2_intro2 (? = ?) (? ≠ ?) … ); nnormalize; #H1; napply (H (b8w16_destruct_b8_b8 … H1))
+          ##| ##1: #H; nrewrite > H; napply (or2_intro1 (? = ?) (? ≠ ?) (refl_eq …))
+          ##]
+ ##| ##2: napply (or2_intro2 (? = ?) (? ≠ ?) …); nnormalize; #H; napply (b8w16_destruct_b8_w16 … H)
+ ##| ##3: napply (or2_intro2 (? = ?) (? ≠ ?) …); nnormalize; #H; napply (b8w16_destruct_w16_b8 … H)
+ ##| ##4: napply (or2_elim (? = ?) (? ≠ ?) ? (decidable_w16 e1 e2) …);
+          ##[ ##2: #H; napply (or2_intro2 (? = ?) (? ≠ ?) … ); nnormalize; #H1; napply (H (b8w16_destruct_w16_w16 … H1))
+          ##| ##1: #H; nrewrite > H; napply (or2_intro1 (? = ?) (? ≠ ?) (refl_eq …))
+          ##]
+ ##]
+nqed.
+
+nlemma neqb8w16_to_neq : ∀bw1,bw2.eq_b8w16 bw1 bw2 = false → bw1 ≠ bw2.
+ #bw1; #bw2;
+ ncases bw1; #e1; ncases bw2; #e2;
+ ##[ ##1: nchange with ((eq_b8 e1 e2 = false) → ?); #H;
+          nnormalize; #H1; napply (neqb8_to_neq … H); napply (b8w16_destruct_b8_b8 … H1)
+ ##| ##2: nnormalize; #H; #H1; napply (b8w16_destruct_b8_w16 … H1)
+ ##| ##3: nnormalize; #H; #H1; napply (b8w16_destruct_w16_b8 … H1)
+ ##| ##4: nchange with ((eq_w16 e1 e2 = false) → ?); #H;
+          nnormalize; #H1; napply (neqw16_to_neq … H); napply (b8w16_destruct_w16_w16 … H1)
  ##]
 nqed.