(* ********************************************************************** *)
(* Progetto FreeScale *)
(* *)
-(* Sviluppato da: Cosimo Oliboni, oliboni@cs.unibo.it *)
-(* Cosimo Oliboni, oliboni@cs.unibo.it *)
+(* Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it *)
+(* Ultima modifica: 05/08/2009 *)
(* *)
(* ********************************************************************** *)
-include "freescale/bool_lemmas.ma".
+include "num/bool_lemmas.ma".
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.
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).
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.
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.