freescale/word32.ma freescale/word16.ma
freescale/word16.ma freescale/byte8.ma
freescale/byte8.ma freescale/exadecim.ma
+freescale/opcode_base_lemmas1.ma freescale/bool_lemmas.ma freescale/opcode_base.ma
freescale/option.ma freescale/bool.ma
+freescale/aux_bases_lemmas.ma freescale/aux_bases.ma freescale/bool_lemmas.ma
freescale/prod.ma freescale/bool.ma
+freescale/opcode_base.ma freescale/aux_bases.ma freescale/theory.ma freescale/word16.ma
freescale/word16_lemmas.ma freescale/byte8_lemmas.ma freescale/word16.ma
freescale/exadecim.ma freescale/bool.ma freescale/nat.ma freescale/prod.ma
freescale/nat_lemmas.ma freescale/bool_lemmas.ma freescale/nat.ma
napply (refl_eq ??).
nqed.
-nlemma eqoct_to_eq : ∀o1,o2.eq_oct o1 o2 = true → o1 = o2.
- #n1; #n2; #H;
- nletin K ≝ (bool_destruct ?? (n1 = n2) H);
- nelim n1 in K:(%) ⊢ %;
- nelim n2;
+nlemma eqoct_to_eq : ∀n1,n2.eq_oct n1 n2 = true → n1 = n2.
+ #n1; #n2;
+ ncases n1;
+ ncases n2;
nnormalize;
##[ ##1,10,19,28,37,46,55,64: #H; napply (refl_eq ??)
- ##| ##*: #H; napply H
+ ##| ##*: #H; napply (bool_destruct ??? H)
##]
nqed.
nlemma eq_to_eqoct : ∀n1,n2.n1 = n2 → eq_oct n1 n2 = true.
- #n1; #n2; #H;
- nletin K ≝ (oct_destruct ?? (eq_oct n1 n2 = true) H);
- nelim n1 in K:(%) ⊢ %;
- nelim n2;
+ #n1; #n2;
+ ncases n1;
+ ncases n2;
nnormalize;
##[ ##1,10,19,28,37,46,55,64: #H; napply (refl_eq ??)
- ##| ##*: #H; napply H
+ ##| ##*: #H; napply (oct_destruct ??? H)
##]
nqed.
nqed.
nlemma eqbitrig_to_eq : ∀t1,t2.eq_bitrig t1 t2 = true → t1 = t2.
- #t1; #t2; #H;
- nletin K ≝ (bool_destruct ?? (t1 = t2) H);
- nelim t1 in K:(%) ⊢ %;
- ##[ ##1: nelim t2; nnormalize; #H;
+ #t1; #t2;
+ ncases t1;
+ ##[ ##1: ncases t2; nnormalize; #H;
##[ ##1: napply (refl_eq ??)
- ##| ##*: napply H
+ ##| ##*: napply (bool_destruct ??? H)
##]
- ##| ##2: nelim t2; nnormalize; #H;
+ ##| ##2: ncases t2; nnormalize; #H;
##[ ##2: napply (refl_eq ??)
- ##| ##*: napply H
+ ##| ##*: napply (bool_destruct ??? H)
##]
- ##| ##3: nelim t2; nnormalize; #H;
+ ##| ##3: ncases t2; nnormalize; #H;
##[ ##3: napply (refl_eq ??)
- ##| ##*: napply H
+ ##| ##*: napply (bool_destruct ??? H)
##]
- ##| ##4: nelim t2; nnormalize; #H;
+ ##| ##4: ncases t2; nnormalize; #H;
##[ ##4: napply (refl_eq ??)
- ##| ##*: napply H
+ ##| ##*: napply (bool_destruct ??? H)
##]
- ##| ##5: nelim t2; nnormalize; #H;
+ ##| ##5: ncases t2; nnormalize; #H;
##[ ##5: napply (refl_eq ??)
- ##| ##*: napply H
+ ##| ##*: napply (bool_destruct ??? H)
##]
- ##| ##6: nelim t2; nnormalize; #H;
+ ##| ##6: ncases t2; nnormalize; #H;
##[ ##6: napply (refl_eq ??)
- ##| ##*: napply H
+ ##| ##*:napply (bool_destruct ??? H)
##]
- ##| ##7: nelim t2; nnormalize; #H;
+ ##| ##7: ncases t2; nnormalize; #H;
##[ ##7: napply (refl_eq ??)
- ##| ##*: napply H
+ ##| ##*: napply (bool_destruct ??? H)
##]
- ##| ##8: nelim t2; nnormalize; #H;
+ ##| ##8: ncases t2; nnormalize; #H;
##[ ##8: napply (refl_eq ??)
- ##| ##*: napply H
+ ##| ##*: napply (bool_destruct ??? H)
##]
- ##| ##9: nelim t2; nnormalize; #H;
+ ##| ##9: ncases t2; nnormalize; #H;
##[ ##9: napply (refl_eq ??)
- ##| ##*: napply H
+ ##| ##*: napply (bool_destruct ??? H)
##]
- ##| ##10: nelim t2; nnormalize; #H;
+ ##| ##10: ncases t2; nnormalize; #H;
##[ ##10: napply (refl_eq ??)
- ##| ##*: napply H
+ ##| ##*: napply (bool_destruct ??? H)
##]
- ##| ##11: nelim t2; nnormalize; #H;
+ ##| ##11: ncases t2; nnormalize; #H;
##[ ##11: napply (refl_eq ??)
- ##| ##*: napply H
+ ##| ##*: napply (bool_destruct ??? H)
##]
- ##| ##12: nelim t2; nnormalize; #H;
+ ##| ##12: ncases t2; nnormalize; #H;
##[ ##12: napply (refl_eq ??)
- ##| ##*: napply H
+ ##| ##*: napply (bool_destruct ??? H)
##]
- ##| ##13: nelim t2; nnormalize; #H;
+ ##| ##13: ncases t2; nnormalize; #H;
##[ ##13: napply (refl_eq ??)
- ##| ##*: napply H
+ ##| ##*: napply (bool_destruct ??? H)
##]
- ##| ##14: nelim t2; nnormalize; #H;
+ ##| ##14: ncases t2; nnormalize; #H;
##[ ##14: napply (refl_eq ??)
- ##| ##*: napply H
+ ##| ##*: napply (bool_destruct ??? H)
##]
- ##| ##15: nelim t2; nnormalize; #H;
+ ##| ##15: ncases t2; nnormalize; #H;
##[ ##15: napply (refl_eq ??)
- ##| ##*: napply H
+ ##| ##*: napply (bool_destruct ??? H)
##]
- ##| ##16: nelim t2; nnormalize; #H;
+ ##| ##16: ncases t2; nnormalize; #H;
##[ ##16: napply (refl_eq ??)
- ##| ##*: napply H
+ ##| ##*: napply (bool_destruct ??? H)
##]
- ##| ##17: nelim t2; nnormalize; #H;
+ ##| ##17: ncases t2; nnormalize; #H;
##[ ##17: napply (refl_eq ??)
- ##| ##*: napply H
+ ##| ##*: napply (bool_destruct ??? H)
##]
- ##| ##18: nelim t2; nnormalize; #H;
+ ##| ##18: ncases t2; nnormalize; #H;
##[ ##18: napply (refl_eq ??)
- ##| ##*: napply H
+ ##| ##*: napply (bool_destruct ??? H)
##]
- ##| ##19: nelim t2; nnormalize; #H;
+ ##| ##19: ncases t2; nnormalize; #H;
##[ ##19: napply (refl_eq ??)
- ##| ##*: napply H
+ ##| ##*: napply (bool_destruct ??? H)
##]
- ##| ##20: nelim t2; nnormalize; #H;
+ ##| ##20: ncases t2; nnormalize; #H;
##[ ##20: napply (refl_eq ??)
- ##| ##*: napply H
+ ##| ##*: napply (bool_destruct ??? H)
##]
- ##| ##21: nelim t2; nnormalize; #H;
+ ##| ##21: ncases t2; nnormalize; #H;
##[ ##21: napply (refl_eq ??)
- ##| ##*: napply H
+ ##| ##*: napply (bool_destruct ??? H)
##]
- ##| ##22: nelim t2; nnormalize; #H;
+ ##| ##22: ncases t2; nnormalize; #H;
##[ ##22: napply (refl_eq ??)
- ##| ##*: napply H
+ ##| ##*: napply (bool_destruct ??? H)
##]
- ##| ##23: nelim t2; nnormalize; #H;
+ ##| ##23: ncases t2; nnormalize; #H;
##[ ##23: napply (refl_eq ??)
- ##| ##*: napply H
+ ##| ##*: napply (bool_destruct ??? H)
##]
- ##| ##24: nelim t2; nnormalize; #H;
+ ##| ##24: ncases t2; nnormalize; #H;
##[ ##24: napply (refl_eq ??)
- ##| ##*: napply H
+ ##| ##*: napply (bool_destruct ??? H)
##]
- ##| ##25: nelim t2; nnormalize; #H;
+ ##| ##25: ncases t2; nnormalize; #H;
##[ ##25: napply (refl_eq ??)
- ##| ##*: napply H
+ ##| ##*: napply (bool_destruct ??? H)
##]
- ##| ##26: nelim t2; nnormalize; #H;
+ ##| ##26: ncases t2; nnormalize; #H;
##[ ##26: napply (refl_eq ??)
- ##| ##*: napply H
+ ##| ##*: napply (bool_destruct ??? H)
##]
- ##| ##27: nelim t2; nnormalize; #H;
+ ##| ##27: ncases t2; nnormalize; #H;
##[ ##27: napply (refl_eq ??)
- ##| ##*: napply H
+ ##| ##*: napply (bool_destruct ??? H)
##]
- ##| ##28: nelim t2; nnormalize; #H;
+ ##| ##28: ncases t2; nnormalize; #H;
##[ ##28: napply (refl_eq ??)
- ##| ##*: napply H
+ ##| ##*: napply (bool_destruct ??? H)
##]
- ##| ##29: nelim t2; nnormalize; #H;
+ ##| ##29: ncases t2; nnormalize; #H;
##[ ##29: napply (refl_eq ??)
- ##| ##*: napply H
+ ##| ##*: napply (bool_destruct ??? H)
##]
- ##| ##30: nelim t2; nnormalize; #H;
+ ##| ##30: ncases t2; nnormalize; #H;
##[ ##30: napply (refl_eq ??)
- ##| ##*: napply H
+ ##| ##*: napply (bool_destruct ??? H)
##]
- ##| ##31: nelim t2; nnormalize; #H;
+ ##| ##31: ncases t2; nnormalize; #H;
##[ ##31: napply (refl_eq ??)
- ##| ##*: napply H
+ ##| ##*: napply (bool_destruct ??? H)
##]
- ##| ##32: nelim t2; nnormalize; #H;
+ ##| ##32: ncases t2; nnormalize; #H;
##[ ##32: napply (refl_eq ??)
- ##| ##*: napply H
+ ##| ##*: napply (bool_destruct ??? H)
##]
##]
nqed.
nlemma eq_to_eqbitrig : ∀t1,t2.t1 = t2 → eq_bitrig t1 t2 = true.
- #t1; #t2; #H;
- nletin K ≝ (bitrigesim_destruct ?? (eq_bitrig t1 t2 = true) H);
- nelim t1 in K:(%) ⊢ %;
- ##[ ##1: nelim t2; nnormalize; #H;
+ #t1; #t2;
+ ncases t1;
+ ##[ ##1: ncases t2; nnormalize; #H;
##[ ##1: napply (refl_eq ??)
- ##| ##*: napply H
+ ##| ##*: napply (bitrigesim_destruct ??? H)
##]
- ##| ##2: nelim t2; nnormalize; #H;
+ ##| ##2: ncases t2; nnormalize; #H;
##[ ##2: napply (refl_eq ??)
- ##| ##*: napply H
+ ##| ##*: napply (bitrigesim_destruct ??? H)
##]
- ##| ##3: nelim t2; nnormalize; #H;
+ ##| ##3: ncases t2; nnormalize; #H;
##[ ##3: napply (refl_eq ??)
- ##| ##*: napply H
+ ##| ##*: napply (bitrigesim_destruct ??? H)
##]
- ##| ##4: nelim t2; nnormalize; #H;
+ ##| ##4: ncases t2; nnormalize; #H;
##[ ##4: napply (refl_eq ??)
- ##| ##*: napply H
+ ##| ##*: napply (bitrigesim_destruct ??? H)
##]
- ##| ##5: nelim t2; nnormalize; #H;
+ ##| ##5: ncases t2; nnormalize; #H;
##[ ##5: napply (refl_eq ??)
- ##| ##*: napply H
+ ##| ##*: napply (bitrigesim_destruct ??? H)
##]
- ##| ##6: nelim t2; nnormalize; #H;
+ ##| ##6: ncases t2; nnormalize; #H;
##[ ##6: napply (refl_eq ??)
- ##| ##*: napply H
+ ##| ##*: napply (bitrigesim_destruct ??? H)
##]
- ##| ##7: nelim t2; nnormalize; #H;
+ ##| ##7: ncases t2; nnormalize; #H;
##[ ##7: napply (refl_eq ??)
- ##| ##*: napply H
+ ##| ##*: napply (bitrigesim_destruct ??? H)
##]
- ##| ##8: nelim t2; nnormalize; #H;
+ ##| ##8: ncases t2; nnormalize; #H;
##[ ##8: napply (refl_eq ??)
- ##| ##*: napply H
+ ##| ##*: napply (bitrigesim_destruct ??? H)
##]
- ##| ##9: nelim t2; nnormalize; #H;
+ ##| ##9: ncases t2; nnormalize; #H;
##[ ##9: napply (refl_eq ??)
- ##| ##*: napply H
+ ##| ##*: napply (bitrigesim_destruct ??? H)
##]
- ##| ##10: nelim t2; nnormalize; #H;
+ ##| ##10: ncases t2; nnormalize; #H;
##[ ##10: napply (refl_eq ??)
- ##| ##*: napply H
+ ##| ##*: napply (bitrigesim_destruct ??? H)
##]
- ##| ##11: nelim t2; nnormalize; #H;
+ ##| ##11: ncases t2; nnormalize; #H;
##[ ##11: napply (refl_eq ??)
- ##| ##*: napply H
+ ##| ##*: napply (bitrigesim_destruct ??? H)
##]
- ##| ##12: nelim t2; nnormalize; #H;
+ ##| ##12: ncases t2; nnormalize; #H;
##[ ##12: napply (refl_eq ??)
- ##| ##*: napply H
+ ##| ##*: napply (bitrigesim_destruct ??? H)
##]
- ##| ##13: nelim t2; nnormalize; #H;
+ ##| ##13: ncases t2; nnormalize; #H;
##[ ##13: napply (refl_eq ??)
- ##| ##*: napply H
+ ##| ##*: napply (bitrigesim_destruct ??? H)
##]
- ##| ##14: nelim t2; nnormalize; #H;
+ ##| ##14: ncases t2; nnormalize; #H;
##[ ##14: napply (refl_eq ??)
- ##| ##*: napply H
+ ##| ##*: napply (bitrigesim_destruct ??? H)
##]
- ##| ##15: nelim t2; nnormalize; #H;
+ ##| ##15: ncases t2; nnormalize; #H;
##[ ##15: napply (refl_eq ??)
- ##| ##*: napply H
+ ##| ##*: napply (bitrigesim_destruct ??? H)
##]
- ##| ##16: nelim t2; nnormalize; #H;
+ ##| ##16: ncases t2; nnormalize; #H;
##[ ##16: napply (refl_eq ??)
- ##| ##*: napply H
+ ##| ##*: napply (bitrigesim_destruct ??? H)
##]
- ##| ##17: nelim t2; nnormalize; #H;
+ ##| ##17: ncases t2; nnormalize; #H;
##[ ##17: napply (refl_eq ??)
- ##| ##*: napply H
+ ##| ##*: napply (bitrigesim_destruct ??? H)
##]
- ##| ##18: nelim t2; nnormalize; #H;
+ ##| ##18: ncases t2; nnormalize; #H;
##[ ##18: napply (refl_eq ??)
- ##| ##*: napply H
+ ##| ##*: napply (bitrigesim_destruct ??? H)
##]
- ##| ##19: nelim t2; nnormalize; #H;
+ ##| ##19: ncases t2; nnormalize; #H;
##[ ##19: napply (refl_eq ??)
- ##| ##*: napply H
+ ##| ##*: napply (bitrigesim_destruct ??? H)
##]
- ##| ##20: nelim t2; nnormalize; #H;
+ ##| ##20: ncases t2; nnormalize; #H;
##[ ##20: napply (refl_eq ??)
- ##| ##*: napply H
+ ##| ##*: napply (bitrigesim_destruct ??? H)
##]
- ##| ##21: nelim t2; nnormalize; #H;
+ ##| ##21: ncases t2; nnormalize; #H;
##[ ##21: napply (refl_eq ??)
- ##| ##*: napply H
+ ##| ##*: napply (bitrigesim_destruct ??? H)
##]
- ##| ##22: nelim t2; nnormalize; #H;
+ ##| ##22: ncases t2; nnormalize; #H;
##[ ##22: napply (refl_eq ??)
- ##| ##*: napply H
+ ##| ##*: napply (bitrigesim_destruct ??? H)
##]
- ##| ##23: nelim t2; nnormalize; #H;
+ ##| ##23: ncases t2; nnormalize; #H;
##[ ##23: napply (refl_eq ??)
- ##| ##*: napply H
+ ##| ##*: napply (bitrigesim_destruct ??? H)
##]
- ##| ##24: nelim t2; nnormalize; #H;
+ ##| ##24: ncases t2; nnormalize; #H;
##[ ##24: napply (refl_eq ??)
- ##| ##*: napply H
+ ##| ##*: napply (bitrigesim_destruct ??? H)
##]
- ##| ##25: nelim t2; nnormalize; #H;
+ ##| ##25: ncases t2; nnormalize; #H;
##[ ##25: napply (refl_eq ??)
- ##| ##*: napply H
+ ##| ##*: napply (bitrigesim_destruct ??? H)
##]
- ##| ##26: nelim t2; nnormalize; #H;
+ ##| ##26: ncases t2; nnormalize; #H;
##[ ##26: napply (refl_eq ??)
- ##| ##*: napply H
+ ##| ##*: napply (bitrigesim_destruct ??? H)
##]
- ##| ##27: nelim t2; nnormalize; #H;
+ ##| ##27: ncases t2; nnormalize; #H;
##[ ##27: napply (refl_eq ??)
- ##| ##*: napply H
+ ##| ##*: napply (bitrigesim_destruct ??? H)
##]
- ##| ##28: nelim t2; nnormalize; #H;
+ ##| ##28: ncases t2; nnormalize; #H;
##[ ##28: napply (refl_eq ??)
- ##| ##*: napply H
+ ##| ##*: napply (bitrigesim_destruct ??? H)
##]
- ##| ##29: nelim t2; nnormalize; #H;
+ ##| ##29: ncases t2; nnormalize; #H;
##[ ##29: napply (refl_eq ??)
- ##| ##*: napply H
+ ##| ##*: napply (bitrigesim_destruct ??? H)
##]
- ##| ##30: nelim t2; nnormalize; #H;
+ ##| ##30: ncases t2; nnormalize; #H;
##[ ##30: napply (refl_eq ??)
- ##| ##*: napply H
+ ##| ##*: napply (bitrigesim_destruct ??? H)
##]
- ##| ##31: nelim t2; nnormalize; #H;
+ ##| ##31: ncases t2; nnormalize; #H;
##[ ##31: napply (refl_eq ??)
- ##| ##*: napply H
+ ##| ##*: napply (bitrigesim_destruct ??? H)
##]
- ##| ##32: nelim t2; nnormalize; #H;
+ ##| ##32: ncases t2; nnormalize; #H;
##[ ##32: napply (refl_eq ??)
- ##| ##*: napply H
+ ##| ##*: napply (bitrigesim_destruct ??? H)
##]
##]
nqed.
nqed.
nlemma eqbool_to_eq : ∀b1,b2:bool.(eq_bool b1 b2 = true) → (b1 = b2).
- #b1; #b2; #H;
- nletin K ≝ (bool_destruct ?? (b1 = b2) H);
- nelim b1 in K:(%) ⊢ %;
- nelim b2;
+ #b1; #b2;
+ ncases b1;
+ ncases b2;
nnormalize;
- ##[ ##2,3: #H; napply H
- ##| ##1,4: #H; napply (refl_eq ??)
+ ##[ ##1,4: #H; napply (refl_eq ??)
+ ##| ##*: #H; napply (bool_destruct ??? H)
##]
nqed.
nlemma eq_to_eqbool : ∀b1,b2.b1 = b2 → eq_bool b1 b2 = true.
- #b1; #b2; #H;
- nletin K ≝ (bool_destruct ?? (eq_bool b1 b2 = true) H);
- nelim b1 in K:(%) ⊢ %;
- nelim b2;
+ #b1; #b2;
+ ncases b1;
+ ncases b2;
nnormalize;
- ##[ ##2,3: #H; napply H
- ##| ##1,4: #H; napply (refl_eq ??)
+ ##[ ##1,4: #H; napply (refl_eq ??)
+ ##| ##*: #H; napply (bool_destruct ??? H)
##]
nqed.
nlemma andb_true_true_l: ∀b1,b2.(b1 ⊗ b2) = true → b1 = true.
- #b1; #b2; #H;
- nletin K ≝ (bool_destruct ?? (b1 = true) H);
- nelim b1 in K:(%) ⊢ %;
- nelim b2;
+ #b1; #b2;
+ ncases b1;
+ ncases b2;
nnormalize;
- ##[ ##3,4: #H; napply H
- ##| ##1,2: #H; napply (refl_eq ??)
+ ##[ ##1,2: #H; napply (refl_eq ??)
+ ##| ##*: #H; napply (bool_destruct ??? H)
##]
nqed.
nlemma andb_true_true_r: ∀b1,b2.(b1 ⊗ b2) = true → b2 = true.
- #b1; #b2; #H;
- nletin K ≝ (bool_destruct ?? (b2 = true) H);
- nelim b1 in K:(%) ⊢ %;
- nelim b2;
+ #b1; #b2;
+ ncases b1;
+ ncases b2;
nnormalize;
- ##[ ##2,4: #H; napply H
- ##| ##1,3: #H; napply (refl_eq ??)
+ ##[ ##1,3: #H; napply (refl_eq ??)
+ ##| ##*: #H; napply (bool_destruct ??? H)
##]
nqed.
nlemma orb_false_false_l : ∀b1,b2:bool.(b1 ⊕ b2) = false → b1 = false.
- #b1; #b2; #H;
- nletin K ≝ (bool_destruct ?? (b1 = false) H);
- nelim b1 in K:(%) ⊢ %;
- nelim b2;
+ #b1; #b2;
+ ncases b1;
+ ncases b2;
nnormalize;
- ##[ ##1,2,3: #H; napply H
- ##| ##4: #H; napply (refl_eq ??)
+ ##[ ##4: #H; napply (refl_eq ??)
+ ##| ##*: #H; napply (bool_destruct ??? H)
##]
nqed.
nlemma orb_false_false_r : ∀b1,b2:bool.(b1 ⊕ b2) = false → b2 = false.
- #b1; #b2; #H;
- nletin K ≝ (bool_destruct ?? (b2 = false) H);
- nelim b1 in K:(%) ⊢ %;
- nelim b2;
+ #b1; #b2;
+ ncases b1;
+ ncases b2;
nnormalize;
- ##[ ##1,2,3: #H; napply H
- ##| ##4: #H; napply (refl_eq ??)
+ ##[ ##4: #H; napply (refl_eq ??)
+ ##| ##*: #H; napply (bool_destruct ??? H)
##]
nqed.
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.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* ********************************************************************** *)
+(* Progetto FreeScale *)
+(* *)
+(* Sviluppato da: *)
+(* 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/aux_bases.ma".
+include "freescale/word16.ma".
+include "freescale/theory.ma".
+
+(* ********************************************** *)
+(* MATTONI BASE PER DEFINIRE LE TABELLE DELLE MCU *)
+(* ********************************************** *)
+
+(* enumerazione delle ALU *)
+ninductive mcu_type: Type ≝
+ HC05 : mcu_type
+| HC08 : mcu_type
+| HCS08 : mcu_type
+| RS08 : mcu_type.
+
+ndefinition mcu_type_ind : ΠP:mcu_type → Prop.P HC05 → P HC08 → P HCS08 → P RS08 → Πm:mcu_type.P m ≝
+λP:mcu_type → Prop.λp:P HC05.λp1:P HC08.λp2:P HCS08.λp3:P RS08.λm:mcu_type.
+ match m with [ HC05 ⇒ p | HC08 ⇒ p1 | HCS08 ⇒ p2 | RS08 ⇒ p3 ].
+
+ndefinition mcu_type_rec : ΠP:mcu_type → Set.P HC05 → P HC08 → P HCS08 → P RS08 → Πm:mcu_type.P m ≝
+λP:mcu_type → Set.λp:P HC05.λp1:P HC08.λp2:P HCS08.λp3:P RS08.λm:mcu_type.
+ match m with [ HC05 ⇒ p | HC08 ⇒ p1 | HCS08 ⇒ p2 | RS08 ⇒ p3 ].
+
+ndefinition mcu_type_rect : ΠP:mcu_type → Type.P HC05 → P HC08 → P HCS08 → P RS08 → Πm:mcu_type.P m ≝
+λP:mcu_type → Type.λp:P HC05.λp1:P HC08.λp2:P HCS08.λp3:P RS08.λm:mcu_type.
+ match m with [ HC05 ⇒ p | HC08 ⇒ p1 | HCS08 ⇒ p2 | RS08 ⇒ p3 ].
+
+ndefinition eq_mcutype ≝
+λm1,m2:mcu_type.
+ match m1 with
+ [ HC05 ⇒ match m2 with [ HC05 ⇒ true | _ ⇒ false ]
+ | HC08 ⇒ match m2 with [ HC08 ⇒ true | _ ⇒ false ]
+ | HCS08 ⇒ match m2 with [ HCS08 ⇒ true | _ ⇒ false ]
+ | RS08 ⇒ match m2 with [ RS08 ⇒ true | _ ⇒ false ]
+ ].
+
+(* enumerazione delle modalita' di indirizzamento = caricamento degli operandi *)
+ninductive instr_mode: Type ≝
+ (* INHERENT = nessun operando *)
+ MODE_INH : instr_mode
+ (* INHERENT = nessun operando (A implicito) *)
+| MODE_INHA : instr_mode
+ (* INHERENT = nessun operando (X implicito) *)
+| MODE_INHX : instr_mode
+ (* INHERENT = nessun operando (H implicito) *)
+| MODE_INHH : instr_mode
+
+ (* INHERENT_ADDRESS = nessun operando (HX implicito) *)
+| MODE_INHX0ADD : instr_mode
+ (* INHERENT_ADDRESS = nessun operando (HX implicito+0x00bb) *)
+| MODE_INHX1ADD : instr_mode
+ (* INHERENT_ADDRESS = nessun operando (HX implicito+0xwwww) *)
+| MODE_INHX2ADD : instr_mode
+
+ (* IMMEDIATE = operando valore immediato byte = 0xbb *)
+| MODE_IMM1 : instr_mode
+ (* IMMEDIATE_EXT = operando valore immediato byte = 0xbb -> esteso a word *)
+| MODE_IMM1EXT : instr_mode
+ (* IMMEDIATE = operando valore immediato word = 0xwwww *)
+| MODE_IMM2 : instr_mode
+ (* DIRECT = operando offset byte = [0x00bb] *)
+| MODE_DIR1 : instr_mode
+ (* DIRECT = operando offset word = [0xwwww] *)
+| MODE_DIR2 : instr_mode
+ (* INDEXED = nessun operando (implicito [X] *)
+| MODE_IX0 : instr_mode
+ (* INDEXED = operando offset relativo byte = [X+0x00bb] *)
+| MODE_IX1 : instr_mode
+ (* INDEXED = operando offset relativo word = [X+0xwwww] *)
+| MODE_IX2 : instr_mode
+ (* INDEXED = operando offset relativo byte = [SP+0x00bb] *)
+| MODE_SP1 : instr_mode
+ (* INDEXED = operando offset relativo word = [SP+0xwwww] *)
+| MODE_SP2 : instr_mode
+
+ (* DIRECT → DIRECT = carica da diretto/scrive su diretto *)
+| MODE_DIR1_to_DIR1 : instr_mode
+ (* IMMEDIATE → DIRECT = carica da immediato/scrive su diretto *)
+| MODE_IMM1_to_DIR1 : instr_mode
+ (* INDEXED++ → DIRECT = carica da [X]/scrive su diretto/H:X++ *)
+| MODE_IX0p_to_DIR1 : instr_mode
+ (* DIRECT → INDEXED++ = carica da diretto/scrive su [X]/H:X++ *)
+| MODE_DIR1_to_IX0p : instr_mode
+
+ (* INHERENT(A) + IMMEDIATE *)
+| MODE_INHA_and_IMM1 : instr_mode
+ (* INHERENT(X) + IMMEDIATE *)
+| MODE_INHX_and_IMM1 : instr_mode
+ (* IMMEDIATE + IMMEDIATE *)
+| MODE_IMM1_and_IMM1 : instr_mode
+ (* DIRECT + IMMEDIATE *)
+| MODE_DIR1_and_IMM1 : instr_mode
+ (* INDEXED + IMMEDIATE *)
+| MODE_IX0_and_IMM1 : instr_mode
+ (* INDEXED++ + IMMEDIATE *)
+| MODE_IX0p_and_IMM1 : instr_mode
+ (* INDEXED + IMMEDIATE *)
+| MODE_IX1_and_IMM1 : instr_mode
+ (* INDEXED++ + IMMEDIATE *)
+| MODE_IX1p_and_IMM1 : instr_mode
+ (* INDEXED + IMMEDIATE *)
+| MODE_SP1_and_IMM1 : instr_mode
+
+ (* DIRECT(mTNY) = operando offset byte(maschera scrittura implicita 3 bit) *)
+ (* ex: DIR3 e' carica b, scrivi b con n-simo bit modificato *)
+| MODE_DIRn : oct → instr_mode
+ (* DIRECT(mTNY) + IMMEDIATE = operando offset byte(maschera lettura implicita 3 bit) *)
+ (* + operando valore immediato byte *)
+ (* ex: DIR2_and_IMM1 e' carica b, carica imm, restituisci n-simo bit di b + imm *)
+| MODE_DIRn_and_IMM1 : oct → instr_mode
+ (* TINY = nessun operando (diretto implicito 4bit = [0x00000000:0000iiii]) *)
+| MODE_TNY : exadecim → instr_mode
+ (* SHORT = nessun operando (diretto implicito 5bit = [0x00000000:000iiiii]) *)
+| MODE_SRT : bitrigesim → instr_mode
+.
+
+ndefinition instr_mode_ind
+ : ΠP:instr_mode → Prop.
+ P MODE_INH → P MODE_INHA → P MODE_INHX → P MODE_INHH → P MODE_INHX0ADD → P MODE_INHX1ADD →
+ P MODE_INHX2ADD → P MODE_IMM1 → P MODE_IMM1EXT → P MODE_IMM2 → P MODE_DIR1 → P MODE_DIR2 →
+ P MODE_IX0 → P MODE_IX1 → P MODE_IX2 → P MODE_SP1 → P MODE_SP2 → P MODE_DIR1_to_DIR1 →
+ P MODE_IMM1_to_DIR1 → P MODE_IX0p_to_DIR1 → P MODE_DIR1_to_IX0p → P MODE_INHA_and_IMM1 →
+ P MODE_INHX_and_IMM1 → P MODE_IMM1_and_IMM1 → P MODE_DIR1_and_IMM1 → P MODE_IX0_and_IMM1 →
+ P MODE_IX0p_and_IMM1 → P MODE_IX1_and_IMM1 → P MODE_IX1p_and_IMM1 → P MODE_SP1_and_IMM1 →
+ (Πd:oct.P (MODE_DIRn d)) → (Πd:oct.P (MODE_DIRn_and_IMM1 d)) → (Πd:exadecim.P (MODE_TNY d)) →
+ (Πd:bitrigesim.P (MODE_SRT d)) → Πi:instr_mode.P i ≝
+λP:instr_mode → Prop.
+λp:P MODE_INH.λp1:P MODE_INHA.λp2:P MODE_INHX.λp3:P MODE_INHH.λp4:P MODE_INHX0ADD.λp5:P MODE_INHX1ADD.
+λp6:P MODE_INHX2ADD.λp7:P MODE_IMM1.λp8:P MODE_IMM1EXT.λp9:P MODE_IMM2.λp10:P MODE_DIR1.λp11:P MODE_DIR2.
+λp12:P MODE_IX0.λp13:P MODE_IX1.λp14:P MODE_IX2.λp15:P MODE_SP1.λp16:P MODE_SP2.λp17:P MODE_DIR1_to_DIR1.
+λp18:P MODE_IMM1_to_DIR1.λp19:P MODE_IX0p_to_DIR1.λp20:P MODE_DIR1_to_IX0p.λp21:P MODE_INHA_and_IMM1.
+λp22:P MODE_INHX_and_IMM1.λp23:P MODE_IMM1_and_IMM1.λp24:P MODE_DIR1_and_IMM1.λp25:P MODE_IX0_and_IMM1.
+λp26:P MODE_IX0p_and_IMM1.λp27:P MODE_IX1_and_IMM1.λp28:P MODE_IX1p_and_IMM1.λp29:P MODE_SP1_and_IMM1.
+λf:Πd:oct.P (MODE_DIRn d).λf1:Πd:oct.P (MODE_DIRn_and_IMM1 d).λf2:Πd:exadecim.P (MODE_TNY d).
+λf3:Πd:bitrigesim.P (MODE_SRT d).λi:instr_mode.
+ match i with
+ [ MODE_INH ⇒ p | MODE_INHA ⇒ p1 | MODE_INHX ⇒ p2 | MODE_INHH ⇒ p3 | MODE_INHX0ADD ⇒ p4
+ | MODE_INHX1ADD ⇒ p5 | MODE_INHX2ADD ⇒ p6 | MODE_IMM1 ⇒ p7 | MODE_IMM1EXT ⇒ p8
+ | MODE_IMM2 ⇒ p9 | MODE_DIR1 ⇒ p10 | MODE_DIR2 ⇒ p11 | MODE_IX0 ⇒ p12 | MODE_IX1 ⇒ p13
+ | MODE_IX2 ⇒ p14 | MODE_SP1 ⇒ p15 | MODE_SP2 ⇒ p16 | MODE_DIR1_to_DIR1 ⇒ p17
+ | MODE_IMM1_to_DIR1 ⇒ p18 | MODE_IX0p_to_DIR1 ⇒ p19 | MODE_DIR1_to_IX0p ⇒ p20
+ | MODE_INHA_and_IMM1 ⇒ p21 | MODE_INHX_and_IMM1 ⇒ p22 | MODE_IMM1_and_IMM1 ⇒ p23
+ | MODE_DIR1_and_IMM1 ⇒ p24 | MODE_IX0_and_IMM1 ⇒ p25 | MODE_IX0p_and_IMM1 ⇒ p26
+ | MODE_IX1_and_IMM1 ⇒ p27 | MODE_IX1p_and_IMM1 ⇒ p28 | MODE_SP1_and_IMM1 ⇒ p29
+ | MODE_DIRn (d:oct) ⇒ f d | MODE_DIRn_and_IMM1 (d:oct) ⇒ f1 d | MODE_TNY (d:exadecim) ⇒ f2 d
+ | MODE_SRT (d:bitrigesim) ⇒ f3 d ].
+
+ndefinition instr_mode_rec
+ : ΠP:instr_mode → Set.
+ P MODE_INH → P MODE_INHA → P MODE_INHX → P MODE_INHH → P MODE_INHX0ADD → P MODE_INHX1ADD →
+ P MODE_INHX2ADD → P MODE_IMM1 → P MODE_IMM1EXT → P MODE_IMM2 → P MODE_DIR1 → P MODE_DIR2 →
+ P MODE_IX0 → P MODE_IX1 → P MODE_IX2 → P MODE_SP1 → P MODE_SP2 → P MODE_DIR1_to_DIR1 →
+ P MODE_IMM1_to_DIR1 → P MODE_IX0p_to_DIR1 → P MODE_DIR1_to_IX0p → P MODE_INHA_and_IMM1 →
+ P MODE_INHX_and_IMM1 → P MODE_IMM1_and_IMM1 → P MODE_DIR1_and_IMM1 → P MODE_IX0_and_IMM1 →
+ P MODE_IX0p_and_IMM1 → P MODE_IX1_and_IMM1 → P MODE_IX1p_and_IMM1 → P MODE_SP1_and_IMM1 →
+ (Πd:oct.P (MODE_DIRn d)) → (Πd:oct.P (MODE_DIRn_and_IMM1 d)) → (Πd:exadecim.P (MODE_TNY d)) →
+ (Πd:bitrigesim.P (MODE_SRT d)) → Πi:instr_mode.P i ≝
+λP:instr_mode → Set.
+λp:P MODE_INH.λp1:P MODE_INHA.λp2:P MODE_INHX.λp3:P MODE_INHH.λp4:P MODE_INHX0ADD.λp5:P MODE_INHX1ADD.
+λp6:P MODE_INHX2ADD.λp7:P MODE_IMM1.λp8:P MODE_IMM1EXT.λp9:P MODE_IMM2.λp10:P MODE_DIR1.λp11:P MODE_DIR2.
+λp12:P MODE_IX0.λp13:P MODE_IX1.λp14:P MODE_IX2.λp15:P MODE_SP1.λp16:P MODE_SP2.λp17:P MODE_DIR1_to_DIR1.
+λp18:P MODE_IMM1_to_DIR1.λp19:P MODE_IX0p_to_DIR1.λp20:P MODE_DIR1_to_IX0p.λp21:P MODE_INHA_and_IMM1.
+λp22:P MODE_INHX_and_IMM1.λp23:P MODE_IMM1_and_IMM1.λp24:P MODE_DIR1_and_IMM1.λp25:P MODE_IX0_and_IMM1.
+λp26:P MODE_IX0p_and_IMM1.λp27:P MODE_IX1_and_IMM1.λp28:P MODE_IX1p_and_IMM1.λp29:P MODE_SP1_and_IMM1.
+λf:Πd:oct.P (MODE_DIRn d).λf1:Πd:oct.P (MODE_DIRn_and_IMM1 d).λf2:Πd:exadecim.P (MODE_TNY d).
+λf3:Πd:bitrigesim.P (MODE_SRT d).λi:instr_mode.
+ match i with
+ [ MODE_INH ⇒ p | MODE_INHA ⇒ p1 | MODE_INHX ⇒ p2 | MODE_INHH ⇒ p3 | MODE_INHX0ADD ⇒ p4
+ | MODE_INHX1ADD ⇒ p5 | MODE_INHX2ADD ⇒ p6 | MODE_IMM1 ⇒ p7 | MODE_IMM1EXT ⇒ p8
+ | MODE_IMM2 ⇒ p9 | MODE_DIR1 ⇒ p10 | MODE_DIR2 ⇒ p11 | MODE_IX0 ⇒ p12 | MODE_IX1 ⇒ p13
+ | MODE_IX2 ⇒ p14 | MODE_SP1 ⇒ p15 | MODE_SP2 ⇒ p16 | MODE_DIR1_to_DIR1 ⇒ p17
+ | MODE_IMM1_to_DIR1 ⇒ p18 | MODE_IX0p_to_DIR1 ⇒ p19 | MODE_DIR1_to_IX0p ⇒ p20
+ | MODE_INHA_and_IMM1 ⇒ p21 | MODE_INHX_and_IMM1 ⇒ p22 | MODE_IMM1_and_IMM1 ⇒ p23
+ | MODE_DIR1_and_IMM1 ⇒ p24 | MODE_IX0_and_IMM1 ⇒ p25 | MODE_IX0p_and_IMM1 ⇒ p26
+ | MODE_IX1_and_IMM1 ⇒ p27 | MODE_IX1p_and_IMM1 ⇒ p28 | MODE_SP1_and_IMM1 ⇒ p29
+ | MODE_DIRn (d:oct) ⇒ f d | MODE_DIRn_and_IMM1 (d:oct) ⇒ f1 d | MODE_TNY (d:exadecim) ⇒ f2 d
+ | MODE_SRT (d:bitrigesim) ⇒ f3 d ].
+
+ndefinition instr_mode_rect
+ : ΠP:instr_mode → Type.
+ P MODE_INH → P MODE_INHA → P MODE_INHX → P MODE_INHH → P MODE_INHX0ADD → P MODE_INHX1ADD →
+ P MODE_INHX2ADD → P MODE_IMM1 → P MODE_IMM1EXT → P MODE_IMM2 → P MODE_DIR1 → P MODE_DIR2 →
+ P MODE_IX0 → P MODE_IX1 → P MODE_IX2 → P MODE_SP1 → P MODE_SP2 → P MODE_DIR1_to_DIR1 →
+ P MODE_IMM1_to_DIR1 → P MODE_IX0p_to_DIR1 → P MODE_DIR1_to_IX0p → P MODE_INHA_and_IMM1 →
+ P MODE_INHX_and_IMM1 → P MODE_IMM1_and_IMM1 → P MODE_DIR1_and_IMM1 → P MODE_IX0_and_IMM1 →
+ P MODE_IX0p_and_IMM1 → P MODE_IX1_and_IMM1 → P MODE_IX1p_and_IMM1 → P MODE_SP1_and_IMM1 →
+ (Πd:oct.P (MODE_DIRn d)) → (Πd:oct.P (MODE_DIRn_and_IMM1 d)) → (Πd:exadecim.P (MODE_TNY d)) →
+ (Πd:bitrigesim.P (MODE_SRT d)) → Πi:instr_mode.P i ≝
+λP:instr_mode → Type.
+λp:P MODE_INH.λp1:P MODE_INHA.λp2:P MODE_INHX.λp3:P MODE_INHH.λp4:P MODE_INHX0ADD.λp5:P MODE_INHX1ADD.
+λp6:P MODE_INHX2ADD.λp7:P MODE_IMM1.λp8:P MODE_IMM1EXT.λp9:P MODE_IMM2.λp10:P MODE_DIR1.λp11:P MODE_DIR2.
+λp12:P MODE_IX0.λp13:P MODE_IX1.λp14:P MODE_IX2.λp15:P MODE_SP1.λp16:P MODE_SP2.λp17:P MODE_DIR1_to_DIR1.
+λp18:P MODE_IMM1_to_DIR1.λp19:P MODE_IX0p_to_DIR1.λp20:P MODE_DIR1_to_IX0p.λp21:P MODE_INHA_and_IMM1.
+λp22:P MODE_INHX_and_IMM1.λp23:P MODE_IMM1_and_IMM1.λp24:P MODE_DIR1_and_IMM1.λp25:P MODE_IX0_and_IMM1.
+λp26:P MODE_IX0p_and_IMM1.λp27:P MODE_IX1_and_IMM1.λp28:P MODE_IX1p_and_IMM1.λp29:P MODE_SP1_and_IMM1.
+λf:Πd:oct.P (MODE_DIRn d).λf1:Πd:oct.P (MODE_DIRn_and_IMM1 d).λf2:Πd:exadecim.P (MODE_TNY d).
+λf3:Πd:bitrigesim.P (MODE_SRT d).λi:instr_mode.
+ match i with
+ [ MODE_INH ⇒ p | MODE_INHA ⇒ p1 | MODE_INHX ⇒ p2 | MODE_INHH ⇒ p3 | MODE_INHX0ADD ⇒ p4
+ | MODE_INHX1ADD ⇒ p5 | MODE_INHX2ADD ⇒ p6 | MODE_IMM1 ⇒ p7 | MODE_IMM1EXT ⇒ p8
+ | MODE_IMM2 ⇒ p9 | MODE_DIR1 ⇒ p10 | MODE_DIR2 ⇒ p11 | MODE_IX0 ⇒ p12 | MODE_IX1 ⇒ p13
+ | MODE_IX2 ⇒ p14 | MODE_SP1 ⇒ p15 | MODE_SP2 ⇒ p16 | MODE_DIR1_to_DIR1 ⇒ p17
+ | MODE_IMM1_to_DIR1 ⇒ p18 | MODE_IX0p_to_DIR1 ⇒ p19 | MODE_DIR1_to_IX0p ⇒ p20
+ | MODE_INHA_and_IMM1 ⇒ p21 | MODE_INHX_and_IMM1 ⇒ p22 | MODE_IMM1_and_IMM1 ⇒ p23
+ | MODE_DIR1_and_IMM1 ⇒ p24 | MODE_IX0_and_IMM1 ⇒ p25 | MODE_IX0p_and_IMM1 ⇒ p26
+ | MODE_IX1_and_IMM1 ⇒ p27 | MODE_IX1p_and_IMM1 ⇒ p28 | MODE_SP1_and_IMM1 ⇒ p29
+ | MODE_DIRn (d:oct) ⇒ f d | MODE_DIRn_and_IMM1 (d:oct) ⇒ f1 d | MODE_TNY (d:exadecim) ⇒ f2 d
+ | MODE_SRT (d:bitrigesim) ⇒ f3 d ].
+
+ndefinition eq_instrmode ≝
+λi1,i2:instr_mode.
+ match i1 with
+ [ MODE_INH ⇒ match i2 with [ MODE_INH ⇒ true | _ ⇒ false ]
+ | MODE_INHA ⇒ match i2 with [ MODE_INHA ⇒ true | _ ⇒ false ]
+ | MODE_INHX ⇒ match i2 with [ MODE_INHX ⇒ true | _ ⇒ false ]
+ | MODE_INHH ⇒ match i2 with [ MODE_INHH ⇒ true | _ ⇒ false ]
+ | MODE_INHX0ADD ⇒ match i2 with [ MODE_INHX0ADD ⇒ true | _ ⇒ false ]
+ | MODE_INHX1ADD ⇒ match i2 with [ MODE_INHX1ADD ⇒ true | _ ⇒ false ]
+ | MODE_INHX2ADD ⇒ match i2 with [ MODE_INHX2ADD ⇒ true | _ ⇒ false ]
+ | MODE_IMM1 ⇒ match i2 with [ MODE_IMM1 ⇒ true | _ ⇒ false ]
+ | MODE_IMM1EXT ⇒ match i2 with [ MODE_IMM1EXT ⇒ true | _ ⇒ false ]
+ | MODE_IMM2 ⇒ match i2 with [ MODE_IMM2 ⇒ true | _ ⇒ false ]
+ | MODE_DIR1 ⇒ match i2 with [ MODE_DIR1 ⇒ true | _ ⇒ false ]
+ | MODE_DIR2 ⇒ match i2 with [ MODE_DIR2 ⇒ true | _ ⇒ false ]
+ | MODE_IX0 ⇒ match i2 with [ MODE_IX0 ⇒ true | _ ⇒ false ]
+ | MODE_IX1 ⇒ match i2 with [ MODE_IX1 ⇒ true | _ ⇒ false ]
+ | MODE_IX2 ⇒ match i2 with [ MODE_IX2 ⇒ true | _ ⇒ false ]
+ | MODE_SP1 ⇒ match i2 with [ MODE_SP1 ⇒ true | _ ⇒ false ]
+ | MODE_SP2 ⇒ match i2 with [ MODE_SP2 ⇒ true | _ ⇒ false ]
+ | MODE_DIR1_to_DIR1 ⇒ match i2 with [ MODE_DIR1_to_DIR1 ⇒ true | _ ⇒ false ]
+ | MODE_IMM1_to_DIR1 ⇒ match i2 with [ MODE_IMM1_to_DIR1 ⇒ true | _ ⇒ false ]
+ | MODE_IX0p_to_DIR1 ⇒ match i2 with [ MODE_IX0p_to_DIR1 ⇒ true | _ ⇒ false ]
+ | MODE_DIR1_to_IX0p ⇒ match i2 with [ MODE_DIR1_to_IX0p ⇒ true | _ ⇒ false ]
+ | MODE_INHA_and_IMM1 ⇒ match i2 with [ MODE_INHA_and_IMM1 ⇒ true | _ ⇒ false ]
+ | MODE_INHX_and_IMM1 ⇒ match i2 with [ MODE_INHX_and_IMM1 ⇒ true | _ ⇒ false ]
+ | MODE_IMM1_and_IMM1 ⇒ match i2 with [ MODE_IMM1_and_IMM1 ⇒ true | _ ⇒ false ]
+ | MODE_DIR1_and_IMM1 ⇒ match i2 with [ MODE_DIR1_and_IMM1 ⇒ true | _ ⇒ false ]
+ | MODE_IX0_and_IMM1 ⇒ match i2 with [ MODE_IX0_and_IMM1 ⇒ true | _ ⇒ false ]
+ | MODE_IX0p_and_IMM1 ⇒ match i2 with [ MODE_IX0p_and_IMM1 ⇒ true | _ ⇒ false ]
+ | MODE_IX1_and_IMM1 ⇒ match i2 with [ MODE_IX1_and_IMM1 ⇒ true | _ ⇒ false ]
+ | MODE_IX1p_and_IMM1 ⇒ match i2 with [ MODE_IX1p_and_IMM1 ⇒ true | _ ⇒ false ]
+ | MODE_SP1_and_IMM1 ⇒ match i2 with [ MODE_SP1_and_IMM1 ⇒ true | _ ⇒ false ]
+ | MODE_DIRn n1 ⇒ match i2 with [ MODE_DIRn n2 ⇒ eq_oct n1 n2 | _ ⇒ false ]
+ | MODE_DIRn_and_IMM1 n1 ⇒ match i2 with [ MODE_DIRn_and_IMM1 n2 ⇒ eq_oct n1 n2 | _ ⇒ false ]
+ | MODE_TNY e1 ⇒ match i2 with [ MODE_TNY e2 ⇒ eq_ex e1 e2 | _ ⇒ false ]
+ | MODE_SRT t1 ⇒ match i2 with [ MODE_SRT t2 ⇒ eq_bitrig t1 t2 | _ ⇒ false ]
+ ].
+
+(* enumerazione delle istruzioni di tutte le ALU *)
+ninductive opcode: Type ≝
+ ADC : opcode (* add with carry *)
+| ADD : opcode (* add *)
+| AIS : opcode (* add immediate to SP *)
+| AIX : opcode (* add immediate to X *)
+| AND : opcode (* and *)
+| ASL : opcode (* aritmetic shift left *)
+| ASR : opcode (* aritmetic shift right *)
+| BCC : opcode (* branch if C=0 *)
+| BCLRn : opcode (* clear bit n *)
+| BCS : opcode (* branch if C=1 *)
+| BEQ : opcode (* branch if Z=1 *)
+| BGE : opcode (* branch if N⊙V=0 (great or equal) *)
+| BGND : opcode (* !!background mode!! *)
+| BGT : opcode (* branch if Z|N⊙V=0 clear (great) *)
+| BHCC : opcode (* branch if H=0 *)
+| BHCS : opcode (* branch if H=1 *)
+| BHI : opcode (* branch if C|Z=0, (higher) *)
+| BIH : opcode (* branch if nIRQ=1 *)
+| BIL : opcode (* branch if nIRQ=0 *)
+| BIT : opcode (* flag = and (bit test) *)
+| BLE : opcode (* branch if Z|N⊙V=1 (less or equal) *)
+| BLS : opcode (* branch if C|Z=1 (lower or same) *)
+| BLT : opcode (* branch if N⊙1=1 (less) *)
+| BMC : opcode (* branch if I=0 (interrupt mask clear) *)
+| BMI : opcode (* branch if N=1 (minus) *)
+| BMS : opcode (* branch if I=1 (interrupt mask set) *)
+| BNE : opcode (* branch if Z=0 *)
+| BPL : opcode (* branch if N=0 (plus) *)
+| BRA : opcode (* branch always *)
+| BRCLRn : opcode (* branch if bit n clear *)
+| BRN : opcode (* branch never (nop) *)
+| BRSETn : opcode (* branch if bit n set *)
+| BSETn : opcode (* set bit n *)
+| BSR : opcode (* branch to subroutine *)
+| CBEQA : opcode (* compare (A) and BEQ *)
+| CBEQX : opcode (* compare (X) and BEQ *)
+| CLC : opcode (* C=0 *)
+| CLI : opcode (* I=0 *)
+| CLR : opcode (* operand=0 *)
+| CMP : opcode (* flag = sub (compare A) *)
+| COM : opcode (* not (1 complement) *)
+| CPHX : opcode (* flag = sub (compare H:X) *)
+| CPX : opcode (* flag = sub (compare X) *)
+| DAA : opcode (* decimal adjust A *)
+| DBNZ : opcode (* dec and BNE *)
+| DEC : opcode (* operand=operand-1 (decrement) *)
+| DIV : opcode (* div *)
+| EOR : opcode (* xor *)
+| INC : opcode (* operand=operand+1 (increment) *)
+| JMP : opcode (* jmp word [operand] *)
+| JSR : opcode (* jmp to subroutine *)
+| LDA : opcode (* load in A *)
+| LDHX : opcode (* load in H:X *)
+| LDX : opcode (* load in X *)
+| LSR : opcode (* logical shift right *)
+| MOV : opcode (* move *)
+| MUL : opcode (* mul *)
+| NEG : opcode (* neg (2 complement) *)
+| NOP : opcode (* nop *)
+| NSA : opcode (* nibble swap A (al:ah <- ah:al) *)
+| ORA : opcode (* or *)
+| PSHA : opcode (* push A *)
+| PSHH : opcode (* push H *)
+| PSHX : opcode (* push X *)
+| PULA : opcode (* pop A *)
+| PULH : opcode (* pop H *)
+| PULX : opcode (* pop X *)
+| ROL : opcode (* rotate left *)
+| ROR : opcode (* rotate right *)
+| RSP : opcode (* reset SP (0x00FF) *)
+| RTI : opcode (* return from interrupt *)
+| RTS : opcode (* return from subroutine *)
+| SBC : opcode (* sub with carry*)
+| SEC : opcode (* C=1 *)
+| SEI : opcode (* I=1 *)
+| SHA : opcode (* swap spc_high,A *)
+| SLA : opcode (* swap spc_low,A *)
+| STA : opcode (* store from A *)
+| STHX : opcode (* store from H:X *)
+| STOP : opcode (* !!stop mode!! *)
+| STX : opcode (* store from X *)
+| SUB : opcode (* sub *)
+| SWI : opcode (* software interrupt *)
+| TAP : opcode (* flag=A (transfer A to process status byte *)
+| TAX : opcode (* X=A (transfer A to X) *)
+| TPA : opcode (* A=flag (transfer process status byte to A) *)
+| TST : opcode (* flag = sub (test) *)
+| TSX : opcode (* X:H=SP (transfer SP to H:X) *)
+| TXA : opcode (* A=X (transfer X to A) *)
+| TXS : opcode (* SP=X:H (transfer H:X to SP) *)
+| WAIT : opcode (* !!wait mode!! *)
+.
+
+ndefinition opcode_ind
+ : ΠP:opcode → Prop.
+ P ADC → P ADD → P AIS → P AIX → P AND → P ASL → P ASR → P BCC → P BCLRn → P BCS → P BEQ →
+ P BGE → P BGND → P BGT → P BHCC → P BHCS → P BHI → P BIH → P BIL → P BIT → P BLE → P BLS →
+ P BLT → P BMC → P BMI → P BMS → P BNE → P BPL → P BRA → P BRCLRn → P BRN → P BRSETn → P BSETn →
+ P BSR → P CBEQA → P CBEQX → P CLC → P CLI → P CLR → P CMP → P COM → P CPHX → P CPX → P DAA →
+ P DBNZ → P DEC → P DIV → P EOR → P INC → P JMP → P JSR → P LDA → P LDHX → P LDX → P LSR → P MOV →
+ P MUL → P NEG → P NOP → P NSA → P ORA → P PSHA → P PSHH → P PSHX → P PULA → P PULH → P PULX →
+ P ROL → P ROR → P RSP → P RTI → P RTS → P SBC → P SEC → P SEI → P SHA → P SLA → P STA → P STHX →
+ P STOP → P STX → P SUB → P SWI → P TAP → P TAX → P TPA → P TST → P TSX → P TXA → P TXS → P WAIT →
+ Πo:opcode.P o ≝
+λP:opcode → Prop.
+λp:P ADC.λp1:P ADD.λp2:P AIS.λp3:P AIX.λp4:P AND.λp5:P ASL.λp6:P ASR.λp7:P BCC.λp8:P BCLRn.λp9:P BCS.
+λp10:P BEQ.λp11:P BGE.λp12:P BGND.λp13:P BGT.λp14:P BHCC.λp15:P BHCS.λp16:P BHI.λp17:P BIH.λp18:P BIL.
+λp19:P BIT.λp20:P BLE.λp21:P BLS.λp22:P BLT.λp23:P BMC.λp24:P BMI.λp25:P BMS.λp26:P BNE.λp27:P BPL.
+λp28:P BRA.λp29:P BRCLRn.λp30:P BRN.λp31:P BRSETn.λp32:P BSETn.λp33:P BSR.λp34:P CBEQA.λp35:P CBEQX.
+λp36:P CLC.λp37:P CLI.λp38:P CLR.λp39:P CMP.λp40:P COM.λp41:P CPHX.λp42:P CPX.λp43:P DAA.λp44:P DBNZ.
+λp45:P DEC.λp46:P DIV.λp47:P EOR.λp48:P INC.λp49:P JMP.λp50:P JSR.λp51:P LDA.λp52:P LDHX.λp53:P LDX.
+λp54:P LSR.λp55:P MOV.λp56:P MUL.λp57:P NEG.λp58:P NOP.λp59:P NSA.λp60:P ORA.λp61:P PSHA.λp62:P PSHH.
+λp63:P PSHX.λp64:P PULA.λp65:P PULH.λp66:P PULX.λp67:P ROL.λp68:P ROR.λp69:P RSP.λp70:P RTI.λp71:P RTS.
+λp72:P SBC.λp73:P SEC.λp74:P SEI.λp75:P SHA.λp76:P SLA.λp77:P STA.λp78:P STHX.λp79:P STOP.λp80:P STX.
+λp81:P SUB.λp82:P SWI.λp83:P TAP.λp84:P TAX.λp85:P TPA.λp86:P TST.λp87:P TSX.λp88:P TXA.λp89:P TXS.
+λp90:P WAIT.λo:opcode.
+ match o with
+ [ ADC ⇒ p | ADD ⇒ p1 | AIS ⇒ p2 | AIX ⇒ p3 | AND ⇒ p4 | ASL ⇒ p5 | ASR ⇒ p6 | BCC ⇒ p7 | BCLRn ⇒ p8
+ | BCS ⇒ p9 | BEQ ⇒ p10 | BGE ⇒ p11 | BGND ⇒ p12 | BGT ⇒ p13 | BHCC ⇒ p14 | BHCS ⇒ p15 | BHI ⇒ p16
+ | BIH ⇒ p17 | BIL ⇒ p18 | BIT ⇒ p19 | BLE ⇒ p20 | BLS ⇒ p21 | BLT ⇒ p22 | BMC ⇒ p23 | BMI ⇒ p24
+ | BMS ⇒ p25 | BNE ⇒ p26 | BPL ⇒ p27 | BRA ⇒ p28 | BRCLRn ⇒ p29 | BRN ⇒ p30 | BRSETn ⇒ p31 | BSETn ⇒ p32
+ | BSR ⇒ p33 | CBEQA ⇒ p34 | CBEQX ⇒ p35 | CLC ⇒ p36 | CLI ⇒ p37 | CLR ⇒ p38 | CMP ⇒ p39 | COM ⇒ p40
+ | CPHX ⇒ p41 | CPX ⇒ p42 | DAA ⇒ p43 | DBNZ ⇒ p44 | DEC ⇒ p45 | DIV ⇒ p46 | EOR ⇒ p47 | INC ⇒ p48
+ | JMP ⇒ p49 | JSR ⇒ p50 | LDA ⇒ p51 | LDHX ⇒ p52 | LDX ⇒ p53 | LSR ⇒ p54 | MOV ⇒ p55 | MUL ⇒ p56
+ | NEG ⇒ p57 | NOP ⇒ p58 | NSA ⇒ p59 | ORA ⇒ p60 | PSHA ⇒ p61 | PSHH ⇒ p62 | PSHX ⇒ p63 | PULA ⇒ p64
+ | PULH ⇒ p65 | PULX ⇒ p66 | ROL ⇒ p67 | ROR ⇒ p68 | RSP ⇒ p69 | RTI ⇒ p70 | RTS ⇒ p71 | SBC ⇒ p72
+ | SEC ⇒ p73 | SEI ⇒ p74 | SHA ⇒ p75 | SLA ⇒ p76 | STA ⇒ p77 | STHX ⇒ p78 | STOP ⇒ p79 | STX ⇒ p80
+ | SUB ⇒ p81 | SWI ⇒ p82 | TAP ⇒ p83 | TAX ⇒ p84 | TPA ⇒ p85 | TST ⇒ p86 | TSX ⇒ p87 | TXA ⇒ p88
+ | TXS ⇒ p89 | WAIT ⇒ p90 ].
+
+ndefinition opcode_rec
+ : ΠP:opcode → Set.
+ P ADC → P ADD → P AIS → P AIX → P AND → P ASL → P ASR → P BCC → P BCLRn → P BCS → P BEQ →
+ P BGE → P BGND → P BGT → P BHCC → P BHCS → P BHI → P BIH → P BIL → P BIT → P BLE → P BLS →
+ P BLT → P BMC → P BMI → P BMS → P BNE → P BPL → P BRA → P BRCLRn → P BRN → P BRSETn → P BSETn →
+ P BSR → P CBEQA → P CBEQX → P CLC → P CLI → P CLR → P CMP → P COM → P CPHX → P CPX → P DAA →
+ P DBNZ → P DEC → P DIV → P EOR → P INC → P JMP → P JSR → P LDA → P LDHX → P LDX → P LSR → P MOV →
+ P MUL → P NEG → P NOP → P NSA → P ORA → P PSHA → P PSHH → P PSHX → P PULA → P PULH → P PULX →
+ P ROL → P ROR → P RSP → P RTI → P RTS → P SBC → P SEC → P SEI → P SHA → P SLA → P STA → P STHX →
+ P STOP → P STX → P SUB → P SWI → P TAP → P TAX → P TPA → P TST → P TSX → P TXA → P TXS → P WAIT →
+ Πo:opcode.P o ≝
+λP:opcode → Set.
+λp:P ADC.λp1:P ADD.λp2:P AIS.λp3:P AIX.λp4:P AND.λp5:P ASL.λp6:P ASR.λp7:P BCC.λp8:P BCLRn.λp9:P BCS.
+λp10:P BEQ.λp11:P BGE.λp12:P BGND.λp13:P BGT.λp14:P BHCC.λp15:P BHCS.λp16:P BHI.λp17:P BIH.λp18:P BIL.
+λp19:P BIT.λp20:P BLE.λp21:P BLS.λp22:P BLT.λp23:P BMC.λp24:P BMI.λp25:P BMS.λp26:P BNE.λp27:P BPL.
+λp28:P BRA.λp29:P BRCLRn.λp30:P BRN.λp31:P BRSETn.λp32:P BSETn.λp33:P BSR.λp34:P CBEQA.λp35:P CBEQX.
+λp36:P CLC.λp37:P CLI.λp38:P CLR.λp39:P CMP.λp40:P COM.λp41:P CPHX.λp42:P CPX.λp43:P DAA.λp44:P DBNZ.
+λp45:P DEC.λp46:P DIV.λp47:P EOR.λp48:P INC.λp49:P JMP.λp50:P JSR.λp51:P LDA.λp52:P LDHX.λp53:P LDX.
+λp54:P LSR.λp55:P MOV.λp56:P MUL.λp57:P NEG.λp58:P NOP.λp59:P NSA.λp60:P ORA.λp61:P PSHA.λp62:P PSHH.
+λp63:P PSHX.λp64:P PULA.λp65:P PULH.λp66:P PULX.λp67:P ROL.λp68:P ROR.λp69:P RSP.λp70:P RTI.λp71:P RTS.
+λp72:P SBC.λp73:P SEC.λp74:P SEI.λp75:P SHA.λp76:P SLA.λp77:P STA.λp78:P STHX.λp79:P STOP.λp80:P STX.
+λp81:P SUB.λp82:P SWI.λp83:P TAP.λp84:P TAX.λp85:P TPA.λp86:P TST.λp87:P TSX.λp88:P TXA.λp89:P TXS.
+λp90:P WAIT.λo:opcode.
+ match o with
+ [ ADC ⇒ p | ADD ⇒ p1 | AIS ⇒ p2 | AIX ⇒ p3 | AND ⇒ p4 | ASL ⇒ p5 | ASR ⇒ p6 | BCC ⇒ p7 | BCLRn ⇒ p8
+ | BCS ⇒ p9 | BEQ ⇒ p10 | BGE ⇒ p11 | BGND ⇒ p12 | BGT ⇒ p13 | BHCC ⇒ p14 | BHCS ⇒ p15 | BHI ⇒ p16
+ | BIH ⇒ p17 | BIL ⇒ p18 | BIT ⇒ p19 | BLE ⇒ p20 | BLS ⇒ p21 | BLT ⇒ p22 | BMC ⇒ p23 | BMI ⇒ p24
+ | BMS ⇒ p25 | BNE ⇒ p26 | BPL ⇒ p27 | BRA ⇒ p28 | BRCLRn ⇒ p29 | BRN ⇒ p30 | BRSETn ⇒ p31 | BSETn ⇒ p32
+ | BSR ⇒ p33 | CBEQA ⇒ p34 | CBEQX ⇒ p35 | CLC ⇒ p36 | CLI ⇒ p37 | CLR ⇒ p38 | CMP ⇒ p39 | COM ⇒ p40
+ | CPHX ⇒ p41 | CPX ⇒ p42 | DAA ⇒ p43 | DBNZ ⇒ p44 | DEC ⇒ p45 | DIV ⇒ p46 | EOR ⇒ p47 | INC ⇒ p48
+ | JMP ⇒ p49 | JSR ⇒ p50 | LDA ⇒ p51 | LDHX ⇒ p52 | LDX ⇒ p53 | LSR ⇒ p54 | MOV ⇒ p55 | MUL ⇒ p56
+ | NEG ⇒ p57 | NOP ⇒ p58 | NSA ⇒ p59 | ORA ⇒ p60 | PSHA ⇒ p61 | PSHH ⇒ p62 | PSHX ⇒ p63 | PULA ⇒ p64
+ | PULH ⇒ p65 | PULX ⇒ p66 | ROL ⇒ p67 | ROR ⇒ p68 | RSP ⇒ p69 | RTI ⇒ p70 | RTS ⇒ p71 | SBC ⇒ p72
+ | SEC ⇒ p73 | SEI ⇒ p74 | SHA ⇒ p75 | SLA ⇒ p76 | STA ⇒ p77 | STHX ⇒ p78 | STOP ⇒ p79 | STX ⇒ p80
+ | SUB ⇒ p81 | SWI ⇒ p82 | TAP ⇒ p83 | TAX ⇒ p84 | TPA ⇒ p85 | TST ⇒ p86 | TSX ⇒ p87 | TXA ⇒ p88
+ | TXS ⇒ p89 | WAIT ⇒ p90 ].
+
+ndefinition opcode_rect
+ : ΠP:opcode → Type.
+ P ADC → P ADD → P AIS → P AIX → P AND → P ASL → P ASR → P BCC → P BCLRn → P BCS → P BEQ →
+ P BGE → P BGND → P BGT → P BHCC → P BHCS → P BHI → P BIH → P BIL → P BIT → P BLE → P BLS →
+ P BLT → P BMC → P BMI → P BMS → P BNE → P BPL → P BRA → P BRCLRn → P BRN → P BRSETn → P BSETn →
+ P BSR → P CBEQA → P CBEQX → P CLC → P CLI → P CLR → P CMP → P COM → P CPHX → P CPX → P DAA →
+ P DBNZ → P DEC → P DIV → P EOR → P INC → P JMP → P JSR → P LDA → P LDHX → P LDX → P LSR → P MOV →
+ P MUL → P NEG → P NOP → P NSA → P ORA → P PSHA → P PSHH → P PSHX → P PULA → P PULH → P PULX →
+ P ROL → P ROR → P RSP → P RTI → P RTS → P SBC → P SEC → P SEI → P SHA → P SLA → P STA → P STHX →
+ P STOP → P STX → P SUB → P SWI → P TAP → P TAX → P TPA → P TST → P TSX → P TXA → P TXS → P WAIT →
+ Πo:opcode.P o ≝
+λP:opcode → Type.
+λp:P ADC.λp1:P ADD.λp2:P AIS.λp3:P AIX.λp4:P AND.λp5:P ASL.λp6:P ASR.λp7:P BCC.λp8:P BCLRn.λp9:P BCS.
+λp10:P BEQ.λp11:P BGE.λp12:P BGND.λp13:P BGT.λp14:P BHCC.λp15:P BHCS.λp16:P BHI.λp17:P BIH.λp18:P BIL.
+λp19:P BIT.λp20:P BLE.λp21:P BLS.λp22:P BLT.λp23:P BMC.λp24:P BMI.λp25:P BMS.λp26:P BNE.λp27:P BPL.
+λp28:P BRA.λp29:P BRCLRn.λp30:P BRN.λp31:P BRSETn.λp32:P BSETn.λp33:P BSR.λp34:P CBEQA.λp35:P CBEQX.
+λp36:P CLC.λp37:P CLI.λp38:P CLR.λp39:P CMP.λp40:P COM.λp41:P CPHX.λp42:P CPX.λp43:P DAA.λp44:P DBNZ.
+λp45:P DEC.λp46:P DIV.λp47:P EOR.λp48:P INC.λp49:P JMP.λp50:P JSR.λp51:P LDA.λp52:P LDHX.λp53:P LDX.
+λp54:P LSR.λp55:P MOV.λp56:P MUL.λp57:P NEG.λp58:P NOP.λp59:P NSA.λp60:P ORA.λp61:P PSHA.λp62:P PSHH.
+λp63:P PSHX.λp64:P PULA.λp65:P PULH.λp66:P PULX.λp67:P ROL.λp68:P ROR.λp69:P RSP.λp70:P RTI.λp71:P RTS.
+λp72:P SBC.λp73:P SEC.λp74:P SEI.λp75:P SHA.λp76:P SLA.λp77:P STA.λp78:P STHX.λp79:P STOP.λp80:P STX.
+λp81:P SUB.λp82:P SWI.λp83:P TAP.λp84:P TAX.λp85:P TPA.λp86:P TST.λp87:P TSX.λp88:P TXA.λp89:P TXS.
+λp90:P WAIT.λo:opcode.
+ match o with
+ [ ADC ⇒ p | ADD ⇒ p1 | AIS ⇒ p2 | AIX ⇒ p3 | AND ⇒ p4 | ASL ⇒ p5 | ASR ⇒ p6 | BCC ⇒ p7 | BCLRn ⇒ p8
+ | BCS ⇒ p9 | BEQ ⇒ p10 | BGE ⇒ p11 | BGND ⇒ p12 | BGT ⇒ p13 | BHCC ⇒ p14 | BHCS ⇒ p15 | BHI ⇒ p16
+ | BIH ⇒ p17 | BIL ⇒ p18 | BIT ⇒ p19 | BLE ⇒ p20 | BLS ⇒ p21 | BLT ⇒ p22 | BMC ⇒ p23 | BMI ⇒ p24
+ | BMS ⇒ p25 | BNE ⇒ p26 | BPL ⇒ p27 | BRA ⇒ p28 | BRCLRn ⇒ p29 | BRN ⇒ p30 | BRSETn ⇒ p31 | BSETn ⇒ p32
+ | BSR ⇒ p33 | CBEQA ⇒ p34 | CBEQX ⇒ p35 | CLC ⇒ p36 | CLI ⇒ p37 | CLR ⇒ p38 | CMP ⇒ p39 | COM ⇒ p40
+ | CPHX ⇒ p41 | CPX ⇒ p42 | DAA ⇒ p43 | DBNZ ⇒ p44 | DEC ⇒ p45 | DIV ⇒ p46 | EOR ⇒ p47 | INC ⇒ p48
+ | JMP ⇒ p49 | JSR ⇒ p50 | LDA ⇒ p51 | LDHX ⇒ p52 | LDX ⇒ p53 | LSR ⇒ p54 | MOV ⇒ p55 | MUL ⇒ p56
+ | NEG ⇒ p57 | NOP ⇒ p58 | NSA ⇒ p59 | ORA ⇒ p60 | PSHA ⇒ p61 | PSHH ⇒ p62 | PSHX ⇒ p63 | PULA ⇒ p64
+ | PULH ⇒ p65 | PULX ⇒ p66 | ROL ⇒ p67 | ROR ⇒ p68 | RSP ⇒ p69 | RTI ⇒ p70 | RTS ⇒ p71 | SBC ⇒ p72
+ | SEC ⇒ p73 | SEI ⇒ p74 | SHA ⇒ p75 | SLA ⇒ p76 | STA ⇒ p77 | STHX ⇒ p78 | STOP ⇒ p79 | STX ⇒ p80
+ | SUB ⇒ p81 | SWI ⇒ p82 | TAP ⇒ p83 | TAX ⇒ p84 | TPA ⇒ p85 | TST ⇒ p86 | TSX ⇒ p87 | TXA ⇒ p88
+ | TXS ⇒ p89 | WAIT ⇒ p90 ].
+
+ndefinition eq_op ≝
+λop1,op2:opcode.
+ match op1 with
+ [ ADC ⇒ match op2 with [ ADC ⇒ true | _ ⇒ false ] | ADD ⇒ match op2 with [ ADD ⇒ true | _ ⇒ false ]
+ | AIS ⇒ match op2 with [ AIS ⇒ true | _ ⇒ false ] | AIX ⇒ match op2 with [ AIX ⇒ true | _ ⇒ false ]
+ | AND ⇒ match op2 with [ AND ⇒ true | _ ⇒ false ] | ASL ⇒ match op2 with [ ASL ⇒ true | _ ⇒ false ]
+ | ASR ⇒ match op2 with [ ASR ⇒ true | _ ⇒ false ] | BCC ⇒ match op2 with [ BCC ⇒ true | _ ⇒ false ]
+ | BCLRn ⇒ match op2 with [ BCLRn ⇒ true | _ ⇒ false ] | BCS ⇒ match op2 with [ BCS ⇒ true | _ ⇒ false ]
+ | BEQ ⇒ match op2 with [ BEQ ⇒ true | _ ⇒ false ] | BGE ⇒ match op2 with [ BGE ⇒ true | _ ⇒ false ]
+ | BGND ⇒ match op2 with [ BGND ⇒ true | _ ⇒ false ] | BGT ⇒ match op2 with [ BGT ⇒ true | _ ⇒ false ]
+ | BHCC ⇒ match op2 with [ BHCC ⇒ true | _ ⇒ false ] | BHCS ⇒ match op2 with [ BHCS ⇒ true | _ ⇒ false ]
+ | BHI ⇒ match op2 with [ BHI ⇒ true | _ ⇒ false ] | BIH ⇒ match op2 with [ BIH ⇒ true | _ ⇒ false ]
+ | BIL ⇒ match op2 with [ BIL ⇒ true | _ ⇒ false ] | BIT ⇒ match op2 with [ BIT ⇒ true | _ ⇒ false ]
+ | BLE ⇒ match op2 with [ BLE ⇒ true | _ ⇒ false ] | BLS ⇒ match op2 with [ BLS ⇒ true | _ ⇒ false ]
+ | BLT ⇒ match op2 with [ BLT ⇒ true | _ ⇒ false ] | BMC ⇒ match op2 with [ BMC ⇒ true | _ ⇒ false ]
+ | BMI ⇒ match op2 with [ BMI ⇒ true | _ ⇒ false ] | BMS ⇒ match op2 with [ BMS ⇒ true | _ ⇒ false ]
+ | BNE ⇒ match op2 with [ BNE ⇒ true | _ ⇒ false ] | BPL ⇒ match op2 with [ BPL ⇒ true | _ ⇒ false ]
+ | BRA ⇒ match op2 with [ BRA ⇒ true | _ ⇒ false ] | BRCLRn ⇒ match op2 with [ BRCLRn ⇒ true | _ ⇒ false ]
+ | BRN ⇒ match op2 with [ BRN ⇒ true | _ ⇒ false ] | BRSETn ⇒ match op2 with [ BRSETn ⇒ true | _ ⇒ false ]
+ | BSETn ⇒ match op2 with [ BSETn ⇒ true | _ ⇒ false ] | BSR ⇒ match op2 with [ BSR ⇒ true | _ ⇒ false ]
+ | CBEQA ⇒ match op2 with [ CBEQA ⇒ true | _ ⇒ false ] | CBEQX ⇒ match op2 with [ CBEQX ⇒ true | _ ⇒ false ]
+ | CLC ⇒ match op2 with [ CLC ⇒ true | _ ⇒ false ] | CLI ⇒ match op2 with [ CLI ⇒ true | _ ⇒ false ]
+ | CLR ⇒ match op2 with [ CLR ⇒ true | _ ⇒ false ] | CMP ⇒ match op2 with [ CMP ⇒ true | _ ⇒ false ]
+ | COM ⇒ match op2 with [ COM ⇒ true | _ ⇒ false ] | CPHX ⇒ match op2 with [ CPHX ⇒ true | _ ⇒ false ]
+ | CPX ⇒ match op2 with [ CPX ⇒ true | _ ⇒ false ] | DAA ⇒ match op2 with [ DAA ⇒ true | _ ⇒ false ]
+ | DBNZ ⇒ match op2 with [ DBNZ ⇒ true | _ ⇒ false ] | DEC ⇒ match op2 with [ DEC ⇒ true | _ ⇒ false ]
+ | DIV ⇒ match op2 with [ DIV ⇒ true | _ ⇒ false ] | EOR ⇒ match op2 with [ EOR ⇒ true | _ ⇒ false ]
+ | INC ⇒ match op2 with [ INC ⇒ true | _ ⇒ false ] | JMP ⇒ match op2 with [ JMP ⇒ true | _ ⇒ false ]
+ | JSR ⇒ match op2 with [ JSR ⇒ true | _ ⇒ false ] | LDA ⇒ match op2 with [ LDA ⇒ true | _ ⇒ false ]
+ | LDHX ⇒ match op2 with [ LDHX ⇒ true | _ ⇒ false ] | LDX ⇒ match op2 with [ LDX ⇒ true | _ ⇒ false ]
+ | LSR ⇒ match op2 with [ LSR ⇒ true | _ ⇒ false ] | MOV ⇒ match op2 with [ MOV ⇒ true | _ ⇒ false ]
+ | MUL ⇒ match op2 with [ MUL ⇒ true | _ ⇒ false ] | NEG ⇒ match op2 with [ NEG ⇒ true | _ ⇒ false ]
+ | NOP ⇒ match op2 with [ NOP ⇒ true | _ ⇒ false ] | NSA ⇒ match op2 with [ NSA ⇒ true | _ ⇒ false ]
+ | ORA ⇒ match op2 with [ ORA ⇒ true | _ ⇒ false ] | PSHA ⇒ match op2 with [ PSHA ⇒ true | _ ⇒ false ]
+ | PSHH ⇒ match op2 with [ PSHH ⇒ true | _ ⇒ false ] | PSHX ⇒ match op2 with [ PSHX ⇒ true | _ ⇒ false ]
+ | PULA ⇒ match op2 with [ PULA ⇒ true | _ ⇒ false ] | PULH ⇒ match op2 with [ PULH ⇒ true | _ ⇒ false ]
+ | PULX ⇒ match op2 with [ PULX ⇒ true | _ ⇒ false ] | ROL ⇒ match op2 with [ ROL ⇒ true | _ ⇒ false ]
+ | ROR ⇒ match op2 with [ ROR ⇒ true | _ ⇒ false ] | RSP ⇒ match op2 with [ RSP ⇒ true | _ ⇒ false ]
+ | RTI ⇒ match op2 with [ RTI ⇒ true | _ ⇒ false ] | RTS ⇒ match op2 with [ RTS ⇒ true | _ ⇒ false ]
+ | SBC ⇒ match op2 with [ SBC ⇒ true | _ ⇒ false ] | SEC ⇒ match op2 with [ SEC ⇒ true | _ ⇒ false ]
+ | SEI ⇒ match op2 with [ SEI ⇒ true | _ ⇒ false ] | SHA ⇒ match op2 with [ SHA ⇒ true | _ ⇒ false ]
+ | SLA ⇒ match op2 with [ SLA ⇒ true | _ ⇒ false ] | STA ⇒ match op2 with [ STA ⇒ true | _ ⇒ false ]
+ | STHX ⇒ match op2 with [ STHX ⇒ true | _ ⇒ false ] | STOP ⇒ match op2 with [ STOP ⇒ true | _ ⇒ false ]
+ | STX ⇒ match op2 with [ STX ⇒ true | _ ⇒ false ] | SUB ⇒ match op2 with [ SUB ⇒ true | _ ⇒ false ]
+ | SWI ⇒ match op2 with [ SWI ⇒ true | _ ⇒ false ] | TAP ⇒ match op2 with [ TAP ⇒ true | _ ⇒ false ]
+ | TAX ⇒ match op2 with [ TAX ⇒ true | _ ⇒ false ] | TPA ⇒ match op2 with [ TPA ⇒ true | _ ⇒ false ]
+ | TST ⇒ match op2 with [ TST ⇒ true | _ ⇒ false ] | TSX ⇒ match op2 with [ TSX ⇒ true | _ ⇒ false ]
+ | TXA ⇒ match op2 with [ TXA ⇒ true | _ ⇒ false ] | TXS ⇒ match op2 with [ TXS ⇒ true | _ ⇒ false ]
+ | WAIT ⇒ match op2 with [ WAIT ⇒ true | _ ⇒ false ]
+ ].
+
+(* introduzione di un tipo opcode dipendente dall'mcu_type (phantom type) *)
+ninductive any_opcode (m:mcu_type) : Type ≝
+ anyOP : opcode → any_opcode m.
+
+ndefinition any_opcode_ind
+ : Πm:mcu_type.ΠP:any_opcode m → Prop.(Πo:opcode.P (anyOP m o)) → Πa:any_opcode m.P a ≝
+λm:mcu_type.λP:any_opcode m → Prop.λf:Πo:opcode.P (anyOP m o).λa:any_opcode m.
+ match a with [ anyOP (o:opcode) ⇒ f o ].
+
+ndefinition any_opcode_rec
+ : Πm:mcu_type.ΠP:any_opcode m → Set.(Πo:opcode.P (anyOP m o)) → Πa:any_opcode m.P a ≝
+λm:mcu_type.λP:any_opcode m → Set.λf:Πo:opcode.P (anyOP m o).λa:any_opcode m.
+ match a with [ anyOP (o:opcode) ⇒ f o ].
+
+ndefinition any_opcode_rect
+ : Πm:mcu_type.ΠP:any_opcode m → Type.(Πo:opcode.P (anyOP m o)) → Πa:any_opcode m.P a ≝
+λm:mcu_type.λP:any_opcode m → Type.λf:Πo:opcode.P (anyOP m o).λa:any_opcode m.
+ match a with [ anyOP (o:opcode) ⇒ f o ].
+
+ndefinition eq_anyop ≝
+λm:mcu_type.λop1,op2:any_opcode m.
+ match op1 with [ anyOP op1' ⇒
+ match op2 with [ anyOP op2' ⇒
+ eq_op op1' op2' ]].
+
+(* raggruppamento di byte e word in un tipo unico *)
+ninductive byte8_or_word16 : Type ≝
+ Byte: byte8 → byte8_or_word16
+| Word: word16 → byte8_or_word16.
+
+ndefinition byte8_or_word16_ind
+ : ΠP:byte8_or_word16 → Prop.(Πb:byte8.P (Byte b)) → (Πw:word16.P (Word w)) → Πb:byte8_or_word16.P b ≝
+λP:byte8_or_word16 → Prop.λf:Πb:byte8.P (Byte b).λf1:Πw:word16.P (Word w).λb:byte8_or_word16.
+ match b with [ Byte (b1:byte8) ⇒ f b1 | Word (w:word16) ⇒ f1 w ].
+
+ndefinition byte8_or_word16_rec
+ : ΠP:byte8_or_word16 → Set.(Πb:byte8.P (Byte b)) → (Πw:word16.P (Word w)) → Πb:byte8_or_word16.P b ≝
+λP:byte8_or_word16 → Set.λf:Πb:byte8.P (Byte b).λf1:Πw:word16.P (Word w).λb:byte8_or_word16.
+ match b with [ Byte (b1:byte8) ⇒ f b1 | Word (w:word16) ⇒ f1 w ].
+
+ndefinition byte8_or_word16_rect
+ : ΠP:byte8_or_word16 → Type.(Πb:byte8.P (Byte b)) → (Πw:word16.P (Word w)) → Πb:byte8_or_word16.P b ≝
+λP:byte8_or_word16 → Type.λf:Πb:byte8.P (Byte b).λf1:Πw:word16.P (Word w).λb:byte8_or_word16.
+ match b with [ Byte (b1:byte8) ⇒ f b1 | Word (w:word16) ⇒ f1 w ].
+
+ndefinition eq_b8w16 ≝
+λbw1,bw2:byte8_or_word16.
+ match bw1 with
+ [ Byte b1 ⇒ match bw2 with [ Byte b2 ⇒ eq_b8 b1 b2 | Word _ ⇒ false ]
+ | Word w1 ⇒ match bw2 with [ Byte _ ⇒ false | Word w2 ⇒ eq_w16 w1 w1 ]
+ ].
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* ********************************************************************** *)
+(* Progetto FreeScale *)
+(* *)
+(* Sviluppato da: *)
+(* 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".
+include "freescale/opcode_base.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
+ ##]
+ ##]
+nqed.
+
+nlemma symmetric_eqmcutype : symmetricT mcu_type bool eq_mcutype.
+ #m1; #m2;
+ nelim m1;
+ nelim m2;
+ nnormalize;
+ napply (refl_eq ??).
+nqed.
+
+nlemma eqmcutype_to_eq : ∀m1,m2:mcu_type.(eq_mcutype m1 m2 = true) → (m1 = m2).
+ #m1; #m2;
+ ncases m1;
+ ncases m2;
+ nnormalize;
+ ##[ ##1,6,11,16: #H; napply (refl_eq ??)
+ ##| ##*: #H; napply (bool_destruct ??? H)
+ ##]
+nqed.
+
+nlemma eq_to_eqmcutype : ∀m1,m2.m1 = m2 → eq_mcutype m1 m2 = true.
+ #m1; #m2;
+ ncases m1;
+ ncases m2;
+ nnormalize;
+ ##[ ##1,6,11,16: #H; napply (refl_eq ??)
+ ##| ##*: #H; napply (mcu_type_destruct ??? H)
+ ##]
+nqed.
(symmetricT T bool f) →
(eq_option T o1 o2 f = eq_option T o2 o1 f).
#T; #o1; #o2; #f; #H;
- ncases o1;
- ncases o2;
+ napply (option_ind T ??? o1);
+ napply (option_ind T ??? o2);
nnormalize;
##[ ##1: napply (refl_eq ??)
- ##| ##2,3: #x; napply (refl_eq ??)
- ##| ##4: #x1; #x2; nrewrite > (H x1 x2); napply (refl_eq ??)
+ ##| ##2,3: #H; napply (refl_eq ??)
+ ##| ##4: #a; #a0;
+ nrewrite > (H a0 a);
+ napply (refl_eq ??)
##]
nqed.
(∀x1,x2:T.x1 = x2 → f x1 x2 = true) →
(o1 = o2 → eq_option T o1 o2 f = true).
#T; #o1; #o2; #f; #H;
- ncases o1;
- ncases o2;
- ##[ ##1: nnormalize; #H1; napply (refl_eq ??)
- ##| ##2: #H1; #H2; nelim (option_destruct_none_some ?? H2)
- ##| ##3: #H1; #H2; nelim (option_destruct_some_none ?? H2)
- ##| ##4: #x1; #x2; #H1;
+ napply (option_ind T ??? o1);
+ napply (option_ind T ??? o2);
+ nnormalize;
+ ##[ ##1: #H1; napply (refl_eq ??)
+ ##| ##2: #a; #H1; nelim (option_destruct_none_some ?? H1)
+ ##| ##3: #a; #H1; nelim (option_destruct_some_none ?? H1)
+ ##| ##4: #a; #a0; #H1;
nrewrite > (option_destruct ??? H1);
- nnormalize;
- nrewrite > (H x1 x1 (refl_eq ??));
+ nrewrite > (H a a (refl_eq ??));
napply (refl_eq ??)
##]
nqed.
(∀x1,x2:T.f x1 x2 = true → x1 = x2) →
(eq_option T o1 o2 f = true → o1 = o2).
#T; #o1; #o2; #f; #H;
- ncases o1;
- ncases o2;
- ##[ ##1: nnormalize; #H1; napply (refl_eq ??)
- ##| ##2,3: #H1; #H2; nnormalize in H2:(%); napply (bool_destruct ??? H2)
- ##| ##4: #x1; #x2; #H1;
- nnormalize in H1:(%);
+ napply (option_ind T ??? o1);
+ napply (option_ind T ??? o2);
+ nnormalize;
+ ##[ ##1: #H1; napply (refl_eq ??)
+ ##| ##2,3: #a; #H1; napply (bool_destruct ??? H1)
+ ##| ##4: #a; #a0; #H1;
nrewrite > (H ?? H1);
napply (refl_eq ??)
##]
ninductive Prod5T (T1:Type) (T2:Type) (T3:Type) (T4:Type) (T5:Type) : Type ≝
quintuple : T1 → T2 → T3 → T4 → T5 → Prod5T T1 T2 T3 T4 T5.
-ndefinition Pro54T_ind
+ndefinition Prod5T_ind
: ΠT1,T2,T3,T4,T5:Type.ΠP:Prod5T T1 T2 T3 T4 T5 → Prop.
(Πt:T1.Πt1:T2.Πt2:T3.Πt3:T4.Πt4:T5.P (quintuple T1 T2 T3 T4 T5 t t1 t2 t3 t4)) →
Πp:Prod5T T1 T2 T3 T4 T5.P p ≝
λp:Prod5T T1 T2 T3 T4 T5.
match p with [ quintuple t t1 t2 t3 t4 ⇒ f t t1 t2 t3 t4 ].
-ndefinition Pro54T_rec
+ndefinition Prod5T_rec
: ΠT1,T2,T3,T4,T5:Type.ΠP:Prod5T T1 T2 T3 T4 T5 → Set.
(Πt:T1.Πt1:T2.Πt2:T3.Πt3:T4.Πt4:T5.P (quintuple T1 T2 T3 T4 T5 t t1 t2 t3 t4)) →
Πp:Prod5T T1 T2 T3 T4 T5.P p ≝
λp:Prod5T T1 T2 T3 T4 T5.
match p with [ quintuple t t1 t2 t3 t4 ⇒ f t t1 t2 t3 t4 ].
-ndefinition Pro54T_rect
+ndefinition Prod5T_rect
: ΠT1,T2,T3,T4,T5:Type.ΠP:Prod5T T1 T2 T3 T4 T5 → Type.
(Πt:T1.Πt1:T2.Πt2:T3.Πt3:T4.Πt4:T5.P (quintuple T1 T2 T3 T4 T5 t t1 t2 t3 t4)) →
Πp:Prod5T T1 T2 T3 T4 T5.P p ≝
(symmetricT T2 bool f2) →
(eq_pair T1 T2 p1 p2 f1 f2 = eq_pair T1 T2 p2 p1 f1 f2).
#T1; #T2; #p1; #p2; #f1; #f2; #H; #H1;
- ncases p1;
- ncases p2;
- #x2; #y2; #x1; #y1;
+ napply (ProdT_ind T1 T2 ?? p1);
+ #x1; #y1;
+ napply (ProdT_ind T1 T2 ?? p2);
+ #x2; #y2;
nnormalize;
nrewrite > (H x1 x2);
ncases (f1 x2 x1);
(∀y1,y2:T2.y1 = y2 → f2 y1 y2 = true) →
(p1 = p2 → eq_pair T1 T2 p1 p2 f1 f2 = true).
#T1; #T2; #p1; #p2; #f1; #f2; #H1; #H2;
- ncases p1;
- ncases p2;
- #x2; #y2; #x1; #y1; #H;
+ napply (ProdT_ind T1 T2 ?? p1);
+ #x1; #y1;
+ napply (ProdT_ind T1 T2 ?? p2);
+ #x2; #y2; #H;
nnormalize;
nrewrite > (H1 ?? (pair_destruct_1 ?????? H));
nnormalize;
(∀y1,y2:T2.f2 y1 y2 = true → y1 = y2) →
(eq_pair T1 T2 p1 p2 f1 f2 = true → p1 = p2).
#T1; #T2; #p1; #p2; #f1; #f2; #H1; #H2;
- ncases p1;
- ncases p2;
- #x2; #y2; #x1; #y1; #H;
+ napply (ProdT_ind T1 T2 ?? p1);
+ #x1; #y1;
+ napply (ProdT_ind T1 T2 ?? p2);
+ #x2; #y2; #H;
nnormalize in H:(%);
nletin K ≝ (H1 x1 x2);
ncases (f1 x1 x2) in H:(%) K:(%);
(symmetricT T3 bool f3) →
(eq_triple T1 T2 T3 p1 p2 f1 f2 f3 = eq_triple T1 T2 T3 p2 p1 f1 f2 f3).
#T1; #T2; #T3; #p1; #p2; #f1; #f2; #f3; #H; #H1; #H2;
- ncases p1;
- ncases p2;
- #x2; #y2; #z2; #x1; #y1; #z1;
+ napply (Prod3T_ind T1 T2 T3 ?? p1);
+ #x1; #y1; #z1;
+ napply (Prod3T_ind T1 T2 T3 ?? p2);
+ #x2; #y2; #z2;
nnormalize;
nrewrite > (H x1 x2);
ncases (f1 x2 x1);
(∀z1,z2:T3.z1 = z2 → f3 z1 z2 = true) →
(p1 = p2 → eq_triple T1 T2 T3 p1 p2 f1 f2 f3 = true).
#T1; #T2; #T3; #p1; #p2; #f1; #f2; #f3; #H1; #H2; #H3;
- ncases p1;
- ncases p2;
- #x2; #y2; #z2; #x1; #y1; #z1; #H;
+ napply (Prod3T_ind T1 T2 T3 ?? p1);
+ #x1; #y1; #z1;
+ napply (Prod3T_ind T1 T2 T3 ?? p2);
+ #x2; #y2; #z2; #H;
nnormalize;
nrewrite > (H1 ?? (triple_destruct_1 ????????? H));
nnormalize;
(∀z1,z2:T3.f3 z1 z2 = true → z1 = z2) →
(eq_triple T1 T2 T3 p1 p2 f1 f2 f3 = true → p1 = p2).
#T1; #T2; #T3; #p1; #p2; #f1; #f2; #f3; #H1; #H2; #H3;
- ncases p1;
- ncases p2;
- #x2; #y2; #z2; #x1; #y1; #z1; #H;
+ napply (Prod3T_ind T1 T2 T3 ?? p1);
+ #x1; #y1; #z1;
+ napply (Prod3T_ind T1 T2 T3 ?? p2);
+ #x2; #y2; #z2; #H;
nnormalize in H:(%);
nletin K ≝ (H1 x1 x2);
ncases (f1 x1 x2) in H:(%) K:(%);
(symmetricT T4 bool f4) →
(eq_quadruple T1 T2 T3 T4 p1 p2 f1 f2 f3 f4 = eq_quadruple T1 T2 T3 T4 p2 p1 f1 f2 f3 f4).
#T1; #T2; #T3; #T4; #p1; #p2; #f1; #f2; #f3; #f4; #H; #H1; #H2; #H3;
- ncases p1;
- ncases p2;
- #x2; #y2; #z2; #v2; #x1; #y1; #z1; #v1;
+ napply (Prod4T_ind T1 T2 T3 T4 ?? p1);
+ #x1; #y1; #z1; #v1;
+ napply (Prod4T_ind T1 T2 T3 T4 ?? p2);
+ #x2; #y2; #z2; #v2;
nnormalize;
nrewrite > (H x1 x2);
ncases (f1 x2 x1);
(∀v1,v2:T4.v1 = v2 → f4 v1 v2 = true) →
(p1 = p2 → eq_quadruple T1 T2 T3 T4 p1 p2 f1 f2 f3 f4 = true).
#T1; #T2; #T3; #T4; #p1; #p2; #f1; #f2; #f3; #f4; #H1; #H2; #H3; #H4;
- ncases p1;
- ncases p2;
- #x2; #y2; #z2; #v2; #x1; #y1; #z1; #v1; #H;
+ napply (Prod4T_ind T1 T2 T3 T4 ?? p1);
+ #x1; #y1; #z1; #v1;
+ napply (Prod4T_ind T1 T2 T3 T4 ?? p2);
+ #x2; #y2; #z2; #v2; #H;
nnormalize;
nrewrite > (H1 ?? (quadruple_destruct_1 ???????????? H));
nnormalize;
(∀v1,v2:T4.f4 v1 v2 = true → v1 = v2) →
(eq_quadruple T1 T2 T3 T4 p1 p2 f1 f2 f3 f4 = true → p1 = p2).
#T1; #T2; #T3; #T4; #p1; #p2; #f1; #f2; #f3; #f4; #H1; #H2; #H3; #H4;
- ncases p1;
- ncases p2;
- #x2; #y2; #z2; #v2; #x1; #y1; #z1; #v1; #H;
+ napply (Prod4T_ind T1 T2 T3 T4 ?? p1);
+ #x1; #y1; #z1; #v1;
+ napply (Prod4T_ind T1 T2 T3 T4 ?? p2);
+ #x2; #y2; #z2; #v2; #H;
nnormalize in H:(%);
nletin K ≝ (H1 x1 x2);
ncases (f1 x1 x2) in H:(%) K:(%);
(symmetricT T5 bool f5) →
(eq_quintuple T1 T2 T3 T4 T5 p1 p2 f1 f2 f3 f4 f5 = eq_quintuple T1 T2 T3 T4 T5 p2 p1 f1 f2 f3 f4 f5).
#T1; #T2; #T3; #T4; #T5; #p1; #p2; #f1; #f2; #f3; #f4; #f5; #H; #H1; #H2; #H3; #H4;
- ncases p1;
- ncases p2;
- #x2; #y2; #z2; #v2; #w2; #x1; #y1; #z1; #v1; #w1;
+ napply (Prod5T_ind T1 T2 T3 T4 T5 ?? p1);
+ #x1; #y1; #z1; #v1; #w1;
+ napply (Prod5T_ind T1 T2 T3 T4 T5 ?? p2);
+ #x2; #y2; #z2; #v2; #w2;
nnormalize;
nrewrite > (H x1 x2);
ncases (f1 x2 x1);
(∀w1,w2:T5.w1 = w2 → f5 w1 w2 = true) →
(p1 = p2 → eq_quintuple T1 T2 T3 T4 T5 p1 p2 f1 f2 f3 f4 f5 = true).
#T1; #T2; #T3; #T4; #T5; #p1; #p2; #f1; #f2; #f3; #f4; #f5; #H1; #H2; #H3; #H4; #H5;
- ncases p1;
- ncases p2;
- #x2; #y2; #z2; #v2; #w2; #x1; #y1; #z1; #v1; #w1; #H;
+ napply (Prod5T_ind T1 T2 T3 T4 T5 ?? p1);
+ #x1; #y1; #z1; #v1; #w1;
+ napply (Prod5T_ind T1 T2 T3 T4 T5 ?? p2);
+ #x2; #y2; #z2; #v2; #w2; #H;
nnormalize;
nrewrite > (H1 ?? (quintuple_destruct_1 ??????????????? H));
nnormalize;
(∀w1,w2:T5.f5 w1 w2 = true → w1 = w2) →
(eq_quintuple T1 T2 T3 T4 T5 p1 p2 f1 f2 f3 f4 f5 = true → p1 = p2).
#T1; #T2; #T3; #T4; #T5; #p1; #p2; #f1; #f2; #f3; #f4; #f5; #H1; #H2; #H3; #H4; #H5;
- ncases p1;
- ncases p2;
- #x2; #y2; #z2; #v2; #w2; #x1; #y1; #z1; #v1; #w1; #H;
+ napply (Prod5T_ind T1 T2 T3 T4 T5 ?? p1);
+ #x1; #y1; #z1; #v1; #w1;
+ napply (Prod5T_ind T1 T2 T3 T4 T5 ?? p2);
+ #x2; #y2; #z2; #v2; #w2; #H;
nnormalize in H:(%);
nletin K ≝ (H1 x1 x2);
ncases (f1 x1 x2) in H:(%) K:(%);
(* SOTTOINSIEME MINIMALE DELLA TEORIA *)
(* ********************************** *)
+(* logic/connectives.ma *)
+
ninductive True: Prop ≝
I : True.
ndefinition iff ≝
λA,B.(A -> B) ∧ (B -> A).
+(* higher_order_defs/relations *)
+
ndefinition relation : Type → Type ≝
λA:Type.A → A → Prop.
ndefinition antisymmetric : ∀A:Type.∀R:relation A.Prop ≝
λA.λR.∀x,y:A.R x y → ¬ (R y x).
+(* logic/equality.ma *)
+
ninductive eq (A:Type) (x:A) : A → Prop ≝
refl_eq : eq A x x.
ndefinition symmetricT: ∀A,T:Type.∀R:relationT A T.Prop ≝
λA,T.λR.∀x,y:A.R x y = R y x.
+
+ndefinition associative : ∀A:Type.∀R:relationT A A.Prop ≝
+λA.λR.∀x,y,z:A.R (R x y) z = R x (R y z).
+
+(* list/list.ma *)
+
+ninductive list (A:Type) : Type ≝
+ nil: list A
+| cons: A -> list A -> list A.
+
+nlet rec list_ind (A:Type) (P:list A → Prop) (p:P (nil A)) (f:(Πa:A.Πl':list A.P l' → P (cons A a l'))) (l:list A) on l ≝
+ match l with [ nil ⇒ p | cons h t ⇒ f h t (list_ind A P p f t) ].
+
+nlet rec list_rec (A:Type) (P:list A → Set) (p:P (nil A)) (f:Πa:A.Πl':list A.P l' → P (cons A a l')) (l:list A) on l ≝
+ match l with [ nil ⇒ p | cons h t ⇒ f h t (list_rec A P p f t) ].
+
+nlet rec list_rect (A:Type) (P:list A → Type) (p:P (nil A)) (f:Πa:A.Πl':list A.P l' → P (cons A a l')) (l:list A) on l ≝
+ match l with [ nil ⇒ p | cons h t ⇒ f h t (list_rect A P p f t) ].
+
+nlet rec append A (l1: list A) l2 on l1 ≝
+ match l1 with
+ [ nil => l2
+ | (cons hd tl) => cons A hd (append A tl l2) ].
+
+notation "hvbox(hd break :: tl)"
+ right associative with precedence 47
+ for @{'cons $hd $tl}.
+
+notation "[ list0 x sep ; ]"
+ non associative with precedence 90
+ for ${fold right @'nil rec acc @{'cons $x $acc}}.
+
+notation "hvbox(l1 break @ l2)"
+ right associative with precedence 47
+ for @{'append $l1 $l2 }.
+
+interpretation "nil" 'nil = (nil ?).
+interpretation "cons" 'cons hd tl = (cons ? hd tl).
+interpretation "append" 'append l1 l2 = (append ? l1 l2).
+
+nlemma list_destruct_1 : ∀T.∀x1,x2:T.∀y1,y2:list T.cons T x1 y1 = cons T x2 y2 → x1 = x2.
+ #T; #x1; #x2; #y1; #y2; #H;
+ nchange with (match cons T x2 y2 with [ nil ⇒ False | cons a _ ⇒ x1 = a ]);
+ nrewrite < H;
+ nnormalize;
+ napply (refl_eq ??).
+nqed.
+
+nlemma list_destruct_2 : ∀T.∀x1,x2:T.∀y1,y2:list T.cons T x1 y1 = cons T x2 y2 → y1 = y2.
+ #T; #x1; #x2; #y1; #y2; #H;
+ nchange with (match cons T x2 y2 with [ nil ⇒ False | cons _ b ⇒ y1 = b ]);
+ nrewrite < H;
+ nnormalize;
+ napply (refl_eq ??).
+nqed.
+
+nlemma list_destruct_cons_nil : ∀T.∀x:T.∀y:list T.cons T x y = nil T → False.
+ #T; #x; #y; #H;
+ nchange with (match cons T x y with [ nil ⇒ True | cons a b ⇒ False ]);
+ nrewrite > H;
+ nnormalize;
+ napply I.
+nqed.
+
+nlemma list_destruct_nil_cons : ∀T.∀x:T.∀y:list T.nil T = cons T x y → False.
+ #T; #x; #y; #H;
+ nchange with (match cons T x y with [ nil ⇒ True | cons a b ⇒ False ]);
+ nrewrite < H;
+ nnormalize;
+ napply I.
+nqed.
+
+nlemma append_nil : ∀T:Type.∀l:list T.(l@[]) = l.
+ #T; #l;
+ napply (list_ind T ??? l);
+ nnormalize;
+ ##[ ##1: napply (refl_eq ??)
+ ##| ##2: #x; #y; #H;
+ nrewrite > H;
+ napply (refl_eq ??)
+ ##]
+nqed.
+
+nlemma associative_list : ∀T.associative (list T) (append T).
+ #T; #x; #y; #z;
+ napply (list_ind T ??? x);
+ nnormalize;
+ ##[ ##1: napply (refl_eq ??)
+ ##| ##2: #a; #b; #H;
+ nrewrite > H;
+ napply (refl_eq ??)
+ ##]
+nqed.
+
+nlemma cons_append_commute : ∀T:Type.∀l1,l2:list T.∀a:T.a :: (l1 @ l2) = (a :: l1) @ l2.
+ #T; #l1; #l2; #a;
+ nnormalize;
+ napply (refl_eq ??).
+nqed.
+
+nlemma append_cons_commute : ∀T:Type.∀a:T.∀l,l1:list T.l @ (a::l1) = (l@[a]) @ l1.
+ #T; #a; #l; #l1;
+ nrewrite > (associative_list T l [a] l1);
+ nnormalize;
+ napply (refl_eq ??).
+nqed.
projects / helm.git / commitdiff