From c3fc204cc02f1031b5d17fb0f2be1fc01e5c452f Mon Sep 17 00:00:00 2001 From: Cosimo Oliboni Date: Mon, 13 Jul 2009 01:39:16 +0000 Subject: [PATCH] freescale translation (work in progress) --- .../matita/contribs/ng_assembly/depends | 3 + .../ng_assembly/freescale/aux_bases_lemmas.ma | 286 +++++---- .../ng_assembly/freescale/bool_lemmas.ma | 66 +- .../ng_assembly/freescale/exadecim_lemmas.ma | 18 +- .../ng_assembly/freescale/opcode_base.ma | 582 ++++++++++++++++++ .../freescale/opcode_base_lemmas1.ma | 97 +++ .../ng_assembly/freescale/option_lemmas.ma | 38 +- .../contribs/ng_assembly/freescale/prod.ma | 6 +- .../ng_assembly/freescale/prod_lemmas.ma | 84 +-- .../contribs/ng_assembly/freescale/theory.ma | 112 ++++ 10 files changed, 1044 insertions(+), 248 deletions(-) create mode 100755 helm/software/matita/contribs/ng_assembly/freescale/opcode_base.ma create mode 100755 helm/software/matita/contribs/ng_assembly/freescale/opcode_base_lemmas1.ma diff --git a/helm/software/matita/contribs/ng_assembly/depends b/helm/software/matita/contribs/ng_assembly/depends index bec7a1b91..7c36e0ac0 100644 --- a/helm/software/matita/contribs/ng_assembly/depends +++ b/helm/software/matita/contribs/ng_assembly/depends @@ -12,8 +12,11 @@ freescale/nat.ma freescale/bool.ma freescale/pts.ma 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 diff --git a/helm/software/matita/contribs/ng_assembly/freescale/aux_bases_lemmas.ma b/helm/software/matita/contribs/ng_assembly/freescale/aux_bases_lemmas.ma index c85df6e61..55ef3df23 100755 --- a/helm/software/matita/contribs/ng_assembly/freescale/aux_bases_lemmas.ma +++ b/helm/software/matita/contribs/ng_assembly/freescale/aux_bases_lemmas.ma @@ -104,25 +104,23 @@ nlemma symmetric_eqoct : symmetricT oct bool eq_oct. 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. @@ -402,271 +400,269 @@ nlemma symmetric_eqbitrig : symmetricT bitrigesim bool eq_bitrig. 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. diff --git a/helm/software/matita/contribs/ng_assembly/freescale/bool_lemmas.ma b/helm/software/matita/contribs/ng_assembly/freescale/bool_lemmas.ma index 5d05eb195..493a8e5b6 100755 --- a/helm/software/matita/contribs/ng_assembly/freescale/bool_lemmas.ma +++ b/helm/software/matita/contribs/ng_assembly/freescale/bool_lemmas.ma @@ -116,67 +116,61 @@ nlemma associative_orbool : ∀b1,b2,b3.((b1 ⊙ b2) ⊙ b3) = (b1 ⊙ (b2 ⊙ b 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. diff --git a/helm/software/matita/contribs/ng_assembly/freescale/exadecim_lemmas.ma b/helm/software/matita/contribs/ng_assembly/freescale/exadecim_lemmas.ma index 19f9dc960..762ab5d03 100755 --- a/helm/software/matita/contribs/ng_assembly/freescale/exadecim_lemmas.ma +++ b/helm/software/matita/contribs/ng_assembly/freescale/exadecim_lemmas.ma @@ -382,23 +382,21 @@ nlemma symmetric_plusex_d_c : ∀e1,e2.plus_ex_d_c e1 e2 = plus_ex_d_c e2 e1. 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. diff --git a/helm/software/matita/contribs/ng_assembly/freescale/opcode_base.ma b/helm/software/matita/contribs/ng_assembly/freescale/opcode_base.ma new file mode 100755 index 000000000..8f462ea87 --- /dev/null +++ b/helm/software/matita/contribs/ng_assembly/freescale/opcode_base.ma @@ -0,0 +1,582 @@ +(**************************************************************************) +(* ___ *) +(* ||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 ] + ]. 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 new file mode 100755 index 000000000..39a9baf8b --- /dev/null +++ b/helm/software/matita/contribs/ng_assembly/freescale/opcode_base_lemmas1.ma @@ -0,0 +1,97 @@ +(**************************************************************************) +(* ___ *) +(* ||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. diff --git a/helm/software/matita/contribs/ng_assembly/freescale/option_lemmas.ma b/helm/software/matita/contribs/ng_assembly/freescale/option_lemmas.ma index 30df5ac07..114dbdefd 100644 --- a/helm/software/matita/contribs/ng_assembly/freescale/option_lemmas.ma +++ b/helm/software/matita/contribs/ng_assembly/freescale/option_lemmas.ma @@ -60,12 +60,14 @@ nlemma bsymmetric_eqoption : (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. @@ -74,15 +76,15 @@ nlemma eq_to_eqoption : (∀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. @@ -92,12 +94,12 @@ nlemma eqoption_to_eq : (∀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 ??) ##] diff --git a/helm/software/matita/contribs/ng_assembly/freescale/prod.ma b/helm/software/matita/contribs/ng_assembly/freescale/prod.ma index 081d43408..24bea4f21 100644 --- a/helm/software/matita/contribs/ng_assembly/freescale/prod.ma +++ b/helm/software/matita/contribs/ng_assembly/freescale/prod.ma @@ -171,7 +171,7 @@ ndefinition eq_quadruple ≝ 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 ≝ @@ -180,7 +180,7 @@ ndefinition Pro54T_ind λ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 ≝ @@ -189,7 +189,7 @@ ndefinition Pro54T_rec λ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 ≝ diff --git a/helm/software/matita/contribs/ng_assembly/freescale/prod_lemmas.ma b/helm/software/matita/contribs/ng_assembly/freescale/prod_lemmas.ma index 96bc15172..0c8c6e633 100644 --- a/helm/software/matita/contribs/ng_assembly/freescale/prod_lemmas.ma +++ b/helm/software/matita/contribs/ng_assembly/freescale/prod_lemmas.ma @@ -58,9 +58,10 @@ nlemma bsymmetric_eqpair : (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); @@ -77,9 +78,10 @@ nlemma eq_to_eqpair : (∀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; @@ -94,9 +96,10 @@ nlemma eqpair_to_eq : (∀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:(%); @@ -147,9 +150,10 @@ nlemma bsymmetric_eqtriple : (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); @@ -172,9 +176,10 @@ nlemma eq_to_eqtriple : (∀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; @@ -192,9 +197,10 @@ nlemma eqtriple_to_eq : (∀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:(%); @@ -260,9 +266,10 @@ nlemma bsymmetric_eqquadruple : (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); @@ -291,9 +298,10 @@ nlemma eq_to_eqquadruple : (∀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; @@ -314,9 +322,10 @@ nlemma eqquadruple_to_eq : (∀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:(%); @@ -398,9 +407,10 @@ nlemma bsymmetric_eqquintuple : (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); @@ -435,9 +445,10 @@ nlemma eq_to_eqquintuple : (∀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; @@ -461,9 +472,10 @@ nlemma eqquintuple_to_eq : (∀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:(%); diff --git a/helm/software/matita/contribs/ng_assembly/freescale/theory.ma b/helm/software/matita/contribs/ng_assembly/freescale/theory.ma index 65800d2e5..dcf3789fd 100644 --- a/helm/software/matita/contribs/ng_assembly/freescale/theory.ma +++ b/helm/software/matita/contribs/ng_assembly/freescale/theory.ma @@ -30,6 +30,8 @@ include "freescale/pts.ma". (* SOTTOINSIEME MINIMALE DELLA TEORIA *) (* ********************************** *) +(* logic/connectives.ma *) + ninductive True: Prop ≝ I : True. @@ -140,6 +142,8 @@ ndefinition ex2_ind : ΠA:Type.ΠQ,R:A → Prop.ΠP:Prop.(Πa:A.Q a → R a → ndefinition iff ≝ λA,B.(A -> B) ∧ (B -> A). +(* higher_order_defs/relations *) + ndefinition relation : Type → Type ≝ λA:Type.A → A → Prop. @@ -164,6 +168,8 @@ ndefinition tight_apart : ∀A:Type.∀eq,ap:relation 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. @@ -203,3 +209,109 @@ ndefinition relationT : Type → Type → Type ≝ 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. -- 2.39.2