+++ /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: Ing. Cosimo Oliboni, oliboni@cs.unibo.it *)
-(* Ultima modifica: 05/08/2009 *)
-(* *)
-(* ********************************************************************** *)
-
-include "num/oct_lemmas.ma".
-include "num/bitrigesim_lemmas.ma".
-include "num/exadecim_lemmas.ma".
-include "freescale/opcode_base.ma".
-
-(* ********************************************** *)
-(* MATTONI BASE PER DEFINIRE LE TABELLE DELLE MCU *)
-(* ********************************************** *)
-
-nlemma instrmode_destruct_MODE_DIRn : ∀n1,n2.MODE_DIRn n1 = MODE_DIRn n2 → n1 = n2.
- #n1; #n2; #H;
- nchange with (match MODE_DIRn n2 with [ MODE_DIRn a ⇒ n1 = a | _ ⇒ False ]);
- nrewrite < H;
- nnormalize;
- napply refl_eq.
-nqed.
-
-nlemma instrmode_destruct_MODE_DIRn_and_IMM1 : ∀n1,n2.MODE_DIRn_and_IMM1 n1 = MODE_DIRn_and_IMM1 n2 → n1 = n2.
- #n1; #n2; #H;
- nchange with (match MODE_DIRn_and_IMM1 n2 with [ MODE_DIRn_and_IMM1 a ⇒ n1 = a | _ ⇒ False ]);
- nrewrite < H;
- nnormalize;
- napply refl_eq.
-nqed.
-
-nlemma instrmode_destruct_MODE_TNY : ∀e1,e2.MODE_TNY e1 = MODE_TNY e2 → e1 = e2.
- #e1; #e2; #H;
- nchange with (match MODE_TNY e2 with [ MODE_TNY a ⇒ e1 = a | _ ⇒ False ]);
- nrewrite < H;
- nnormalize;
- napply refl_eq.
-nqed.
-
-nlemma instrmode_destruct_MODE_SRT : ∀t1,t2.MODE_SRT t1 = MODE_SRT t2 → t1 = t2.
- #t1; #t2; #H;
- nchange with (match MODE_SRT t2 with [ MODE_SRT a ⇒ t1 = a | _ ⇒ False ]);
- nrewrite < H;
- nnormalize;
- napply refl_eq.
-nqed.
-
-ndefinition instrmode_destruct_aux ≝
-Πi1,i2.ΠP:Prop.i1 = i2 →
- match eq_im i1 i2 with [ true ⇒ P → P | false ⇒ P ].
-
-ndefinition instrmode_destruct : instrmode_destruct_aux.
- #t1; #t2; #P; #H;
- nrewrite < H;
- nelim t1;
- nnormalize;
- ##[ ##31,32,33,34: #sub; nelim sub; nnormalize ##]
- napply (λx.x).
-nqed.
-
-nlemma eq_to_eqim : ∀n1,n2.n1 = n2 → eq_im n1 n2 = true.
- #n1; #n2; #H;
- nrewrite > H;
- nelim n2;
- ##[ ##31,32: #n; nchange with (eq_oct n n = true); napply (eq_to_eqoct n n (refl_eq …))
- ##| ##33: #n; nchange with (eq_ex n n = true); napply (eq_to_eqex n n (refl_eq …))
- ##| ##34: #n; nchange with (eq_bit n n = true); napply (eq_to_eqbit n n (refl_eq …))
- ##| ##*: nnormalize; napply refl_eq
- ##]
-nqed.
-
-nlemma neqim_to_neq : ∀n1,n2.eq_im n1 n2 = false → n1 ≠ n2.
- #n1; #n2; #H;
- napply (not_to_not (n1 = n2) (eq_im n1 n2 = true) …);
- ##[ ##1: napply (eq_to_eqim n1 n2)
- ##| ##2: napply (eqfalse_to_neqtrue … H)
- ##]
-nqed.
-
-nlemma eqim_to_eq1 : ∀i2.eq_im MODE_INH i2 = true → MODE_INH = i2.
- #i2; ncases i2; nnormalize;
- ##[ ##1: #H; napply refl_eq
- ##| ##31,32,33,34: #n; #H; napply (bool_destruct … H)
- ##| ##*: #H; napply (bool_destruct … H)
- ##]
-nqed.
-
-nlemma eqim_to_eq2 : ∀i2.eq_im MODE_INHA i2 = true → MODE_INHA = i2.
- #i2; ncases i2; nnormalize;
- ##[ ##2: #H; napply refl_eq
- ##| ##31,32,33,34: #n; #H; napply (bool_destruct … H)
- ##| ##*: #H; napply (bool_destruct … H)
- ##]
-nqed.
-
-nlemma eqim_to_eq3 : ∀i2.eq_im MODE_INHX i2 = true → MODE_INHX = i2.
- #i2; ncases i2; nnormalize;
- ##[ ##3: #H; napply refl_eq
- ##| ##31,32,33,34: #n; #H; napply (bool_destruct … H)
- ##| ##*: #H; napply (bool_destruct … H)
- ##]
-nqed.
-
-nlemma eqim_to_eq4 : ∀i2.eq_im MODE_INHH i2 = true → MODE_INHH = i2.
- #i2; ncases i2; nnormalize;
- ##[ ##4: #H; napply refl_eq
- ##| ##31,32,33,34: #n; #H; napply (bool_destruct … H)
- ##| ##*: #H; napply (bool_destruct … H)
- ##]
-nqed.
-
-nlemma eqim_to_eq5 : ∀i2.eq_im MODE_INHX0ADD i2 = true → MODE_INHX0ADD = i2.
- #i2; ncases i2; nnormalize;
- ##[ ##5: #H; napply refl_eq
- ##| ##31,32,33,34: #n; #H; napply (bool_destruct … H)
- ##| ##*: #H; napply (bool_destruct … H)
- ##]
-nqed.
-
-nlemma eqim_to_eq6 : ∀i2.eq_im MODE_INHX1ADD i2 = true → MODE_INHX1ADD = i2.
- #i2; ncases i2; nnormalize;
- ##[ ##6: #H; napply refl_eq
- ##| ##31,32,33,34: #n; #H; napply (bool_destruct … H)
- ##| ##*: #H; napply (bool_destruct … H)
- ##]
-nqed.
-
-nlemma eqim_to_eq7 : ∀i2.eq_im MODE_INHX2ADD i2 = true → MODE_INHX2ADD = i2.
- #i2; ncases i2; nnormalize;
- ##[ ##7: #H; napply refl_eq
- ##| ##31,32,33,34: #n; #H; napply (bool_destruct … H)
- ##| ##*: #H; napply (bool_destruct … H)
- ##]
-nqed.
-
-nlemma eqim_to_eq8 : ∀i2.eq_im MODE_IMM1 i2 = true → MODE_IMM1 = i2.
- #i2; ncases i2; nnormalize;
- ##[ ##8: #H; napply refl_eq
- ##| ##31,32,33,34: #n; #H; napply (bool_destruct … H)
- ##| ##*: #H; napply (bool_destruct … H)
- ##]
-nqed.
-
-nlemma eqim_to_eq9 : ∀i2.eq_im MODE_IMM1EXT i2 = true → MODE_IMM1EXT = i2.
- #i2; ncases i2; nnormalize;
- ##[ ##9: #H; napply refl_eq
- ##| ##31,32,33,34: #n; #H; napply (bool_destruct … H)
- ##| ##*: #H; napply (bool_destruct … H)
- ##]
-nqed.
-
-nlemma eqim_to_eq10 : ∀i2.eq_im MODE_IMM2 i2 = true → MODE_IMM2 = i2.
- #i2; ncases i2; nnormalize;
- ##[ ##10: #H; napply refl_eq
- ##| ##31,32,33,34: #n; #H; napply (bool_destruct … H)
- ##| ##*: #H; napply (bool_destruct … H)
- ##]
-nqed.
-
-nlemma eqim_to_eq11 : ∀i2.eq_im MODE_DIR1 i2 = true → MODE_DIR1 = i2.
- #i2; ncases i2; nnormalize;
- ##[ ##11: #H; napply refl_eq
- ##| ##31,32,33,34: #n; #H; napply (bool_destruct … H)
- ##| ##*: #H; napply (bool_destruct … H)
- ##]
-nqed.
-
-nlemma eqim_to_eq12 : ∀i2.eq_im MODE_DIR2 i2 = true → MODE_DIR2 = i2.
- #i2; ncases i2; nnormalize;
- ##[ ##12: #H; napply refl_eq
- ##| ##31,32,33,34: #n; #H; napply (bool_destruct … H)
- ##| ##*: #H; napply (bool_destruct … H)
- ##]
-nqed.
-
-nlemma eqim_to_eq13 : ∀i2.eq_im MODE_IX0 i2 = true → MODE_IX0 = i2.
- #i2; ncases i2; nnormalize;
- ##[ ##13: #H; napply refl_eq
- ##| ##31,32,33,34: #n; #H; napply (bool_destruct … H)
- ##| ##*: #H; napply (bool_destruct … H)
- ##]
-nqed.
-
-nlemma eqim_to_eq14 : ∀i2.eq_im MODE_IX1 i2 = true → MODE_IX1 = i2.
- #i2; ncases i2; nnormalize;
- ##[ ##14: #H; napply refl_eq
- ##| ##31,32,33,34: #n; #H; napply (bool_destruct … H)
- ##| ##*: #H; napply (bool_destruct … H)
- ##]
-nqed.
-
-nlemma eqim_to_eq15 : ∀i2.eq_im MODE_IX2 i2 = true → MODE_IX2 = i2.
- #i2; ncases i2; nnormalize;
- ##[ ##15: #H; napply refl_eq
- ##| ##31,32,33,34: #n; #H; napply (bool_destruct … H)
- ##| ##*: #H; napply (bool_destruct … H)
- ##]
-nqed.
-
-nlemma eqim_to_eq16 : ∀i2.eq_im MODE_SP1 i2 = true → MODE_SP1 = i2.
- #i2; ncases i2; nnormalize;
- ##[ ##16: #H; napply refl_eq
- ##| ##31,32,33,34: #n; #H; napply (bool_destruct … H)
- ##| ##*: #H; napply (bool_destruct … H)
- ##]
-nqed.
-
-nlemma eqim_to_eq17 : ∀i2.eq_im MODE_SP2 i2 = true → MODE_SP2 = i2.
- #i2; ncases i2; nnormalize;
- ##[ ##17: #H; napply refl_eq
- ##| ##31,32,33,34: #n; #H; napply (bool_destruct … H)
- ##| ##*: #H; napply (bool_destruct … H)
- ##]
-nqed.
-
-nlemma eqim_to_eq18 : ∀i2.eq_im MODE_DIR1_to_DIR1 i2 = true → MODE_DIR1_to_DIR1 = i2.
- #i2; ncases i2; nnormalize;
- ##[ ##18: #H; napply refl_eq
- ##| ##31,32,33,34: #n; #H; napply (bool_destruct … H)
- ##| ##*: #H; napply (bool_destruct … H)
- ##]
-nqed.
-
-nlemma eqim_to_eq19 : ∀i2.eq_im MODE_IMM1_to_DIR1 i2 = true → MODE_IMM1_to_DIR1 = i2.
- #i2; ncases i2; nnormalize;
- ##[ ##19: #H; napply refl_eq
- ##| ##31,32,33,34: #n; #H; napply (bool_destruct … H)
- ##| ##*: #H; napply (bool_destruct … H)
- ##]
-nqed.
-
-nlemma eqim_to_eq20 : ∀i2.eq_im MODE_IX0p_to_DIR1 i2 = true → MODE_IX0p_to_DIR1 = i2.
- #i2; ncases i2; nnormalize;
- ##[ ##20: #H; napply refl_eq
- ##| ##31,32,33,34: #n; #H; napply (bool_destruct … H)
- ##| ##*: #H; napply (bool_destruct … H)
- ##]
-nqed.
-
-nlemma eqim_to_eq21 : ∀i2.eq_im MODE_DIR1_to_IX0p i2 = true → MODE_DIR1_to_IX0p = i2.
- #i2; ncases i2; nnormalize;
- ##[ ##21: #H; napply refl_eq
- ##| ##31,32,33,34: #n; #H; napply (bool_destruct … H)
- ##| ##*: #H; napply (bool_destruct … H)
- ##]
-nqed.
-
-nlemma eqim_to_eq22 : ∀i2.eq_im MODE_INHA_and_IMM1 i2 = true → MODE_INHA_and_IMM1 = i2.
- #i2; ncases i2; nnormalize;
- ##[ ##22: #H; napply refl_eq
- ##| ##31,32,33,34: #n; #H; napply (bool_destruct … H)
- ##| ##*: #H; napply (bool_destruct … H)
- ##]
-nqed.
-
-nlemma eqim_to_eq23 : ∀i2.eq_im MODE_INHX_and_IMM1 i2 = true → MODE_INHX_and_IMM1 = i2.
- #i2; ncases i2; nnormalize;
- ##[ ##23: #H; napply refl_eq
- ##| ##31,32,33,34: #n; #H; napply (bool_destruct … H)
- ##| ##*: #H; napply (bool_destruct … H)
- ##]
-nqed.
-
-nlemma eqim_to_eq24 : ∀i2.eq_im MODE_IMM1_and_IMM1 i2 = true → MODE_IMM1_and_IMM1 = i2.
- #i2; ncases i2; nnormalize;
- ##[ ##24: #H; napply refl_eq
- ##| ##31,32,33,34: #n; #H; napply (bool_destruct … H)
- ##| ##*: #H; napply (bool_destruct … H)
- ##]
-nqed.
-
-nlemma eqim_to_eq25 : ∀i2.eq_im MODE_DIR1_and_IMM1 i2 = true → MODE_DIR1_and_IMM1 = i2.
- #i2; ncases i2; nnormalize;
- ##[ ##25: #H; napply refl_eq
- ##| ##31,32,33,34: #n; #H; napply (bool_destruct … H)
- ##| ##*: #H; napply (bool_destruct … H)
- ##]
-nqed.
-
-nlemma eqim_to_eq26 : ∀i2.eq_im MODE_IX0_and_IMM1 i2 = true → MODE_IX0_and_IMM1 = i2.
- #i2; ncases i2; nnormalize;
- ##[ ##26: #H; napply refl_eq
- ##| ##31,32,33,34: #n; #H; napply (bool_destruct … H)
- ##| ##*: #H; napply (bool_destruct … H)
- ##]
-nqed.
-
-nlemma eqim_to_eq27 : ∀i2.eq_im MODE_IX0p_and_IMM1 i2 = true → MODE_IX0p_and_IMM1 = i2.
- #i2; ncases i2; nnormalize;
- ##[ ##27: #H; napply refl_eq
- ##| ##31,32,33,34: #n; #H; napply (bool_destruct … H)
- ##| ##*: #H; napply (bool_destruct … H)
- ##]
-nqed.
-
-nlemma eqim_to_eq28 : ∀i2.eq_im MODE_IX1_and_IMM1 i2 = true → MODE_IX1_and_IMM1 = i2.
- #i2; ncases i2; nnormalize;
- ##[ ##28: #H; napply refl_eq
- ##| ##31,32,33,34: #n; #H; napply (bool_destruct … H)
- ##| ##*: #H; napply (bool_destruct … H)
- ##]
-nqed.
-
-nlemma eqim_to_eq29 : ∀i2.eq_im MODE_IX1p_and_IMM1 i2 = true → MODE_IX1p_and_IMM1 = i2.
- #i2; ncases i2; nnormalize;
- ##[ ##29: #H; napply refl_eq
- ##| ##31,32,33,34: #n; #H; napply (bool_destruct … H)
- ##| ##*: #H; napply (bool_destruct … H)
- ##]
-nqed.
-
-nlemma eqim_to_eq30 : ∀i2.eq_im MODE_SP1_and_IMM1 i2 = true → MODE_SP1_and_IMM1 = i2.
- #i2; ncases i2; nnormalize;
- ##[ ##30: #H; napply refl_eq
- ##| ##31,32,33,34: #n; #H; napply (bool_destruct … H)
- ##| ##*: #H; napply (bool_destruct … H)
- ##]
-nqed.
-
-nlemma eqim_to_eq31 : ∀n1,i2.eq_im (MODE_DIRn n1) i2 = true → MODE_DIRn n1 = i2.
- #n1; #i2; ncases i2;
- ##[ ##31: #n2; #H;
- nchange in H:(%) with (eq_oct n1 n2 = true);
- nrewrite > (eqoct_to_eq … H);
- napply refl_eq
- ##| ##32,33,34: nnormalize; #n2; #H; napply (bool_destruct … H)
- ##| ##*: nnormalize; #H; napply (bool_destruct … H)
- ##]
-nqed.
-
-nlemma eqim_to_eq32 : ∀n1,i2.eq_im (MODE_DIRn_and_IMM1 n1) i2 = true → MODE_DIRn_and_IMM1 n1 = i2.
- #n1; #i2; ncases i2;
- ##[ ##32: #n2; #H;
- nchange in H:(%) with (eq_oct n1 n2 = true);
- nrewrite > (eqoct_to_eq … H);
- napply refl_eq
- ##| ##31,33,34: nnormalize; #n2; #H; napply (bool_destruct … H)
- ##| ##*: nnormalize; #H; napply (bool_destruct … H)
- ##]
-nqed.
-
-nlemma eqim_to_eq33 : ∀n1,i2.eq_im (MODE_TNY n1) i2 = true → MODE_TNY n1 = i2.
- #n1; #i2; ncases i2;
- ##[ ##33: #n2; #H;
- nchange in H:(%) with (eq_ex n1 n2 = true);
- nrewrite > (eqex_to_eq … H);
- napply refl_eq
- ##| ##31,32,34: nnormalize; #n2; #H; napply (bool_destruct … H)
- ##| ##*: nnormalize; #H; napply (bool_destruct … H)
- ##]
-nqed.
-
-nlemma eqim_to_eq34 : ∀n1,i2.eq_im (MODE_SRT n1) i2 = true → MODE_SRT n1 = i2.
- #n1; #i2; ncases i2;
- ##[ ##34: #n2; #H;
- nchange in H:(%) with (eq_bit n1 n2 = true);
- nrewrite > (eqbit_to_eq … H);
- napply refl_eq
- ##| ##31,32,33: nnormalize; #n2; #H; napply (bool_destruct … H)
- ##| ##*: nnormalize; #H; napply (bool_destruct … H)
- ##]
-nqed.
-
-nlemma eqim_to_eq : ∀i1,i2.eq_im i1 i2 = true → i1 = i2.
- #i1; ncases i1;
- ##[ ##1: napply eqim_to_eq1 ##| ##2: napply eqim_to_eq2
- ##| ##3: napply eqim_to_eq3 ##| ##4: napply eqim_to_eq4
- ##| ##5: napply eqim_to_eq5 ##| ##6: napply eqim_to_eq6
- ##| ##7: napply eqim_to_eq7 ##| ##8: napply eqim_to_eq8
- ##| ##9: napply eqim_to_eq9 ##| ##10: napply eqim_to_eq10
- ##| ##11: napply eqim_to_eq11 ##| ##12: napply eqim_to_eq12
- ##| ##13: napply eqim_to_eq13 ##| ##14: napply eqim_to_eq14
- ##| ##15: napply eqim_to_eq15 ##| ##16: napply eqim_to_eq16
- ##| ##17: napply eqim_to_eq17 ##| ##18: napply eqim_to_eq18
- ##| ##19: napply eqim_to_eq19 ##| ##20: napply eqim_to_eq20
- ##| ##21: napply eqim_to_eq21 ##| ##22: napply eqim_to_eq22
- ##| ##23: napply eqim_to_eq23 ##| ##24: napply eqim_to_eq24
- ##| ##25: napply eqim_to_eq25 ##| ##26: napply eqim_to_eq26
- ##| ##27: napply eqim_to_eq27 ##| ##28: napply eqim_to_eq28
- ##| ##29: napply eqim_to_eq29 ##| ##30: napply eqim_to_eq30
- ##| ##31: napply eqim_to_eq31 ##| ##32: napply eqim_to_eq32
- ##| ##33: napply eqim_to_eq33 ##| ##34: napply eqim_to_eq34
- ##]
-nqed.
-
-nlemma neq_to_neqim : ∀n1,n2.n1 ≠ n2 → eq_im n1 n2 = false.
- #n1; #n2; #H;
- napply (neqtrue_to_eqfalse (eq_im n1 n2));
- napply (not_to_not (eq_im n1 n2 = true) (n1 = n2) ? H);
- napply (eqim_to_eq n1 n2).
-nqed.
-
-nlemma decidable_im : ∀x,y:instr_mode.decidable (x = y).
- #x; #y; nnormalize;
- napply (or2_elim (eq_im x y = true) (eq_im x y = false) ? (decidable_bexpr ?));
- ##[ ##1: #H; napply (or2_intro1 (x = y) (x ≠ y) (eqim_to_eq … H))
- ##| ##2: #H; napply (or2_intro2 (x = y) (x ≠ y) (neqim_to_neq … H))
- ##]
-nqed.
-
-nlemma symmetric_eqim : symmetricT instr_mode bool eq_im.
- #n1; #n2;
- napply (or2_elim (n1 = n2) (n1 ≠ n2) ? (decidable_im n1 n2));
- ##[ ##1: #H; nrewrite > H; napply refl_eq
- ##| ##2: #H; nrewrite > (neq_to_neqim n1 n2 H);
- napply (symmetric_eq ? (eq_im n2 n1) false);
- napply (neq_to_neqim n2 n1 (symmetric_neq ? n1 n2 H))
- ##]
-nqed.
projects / helm.git / blobdiff