+++ /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 "freescale/opcode_base_lemmas_opcode.ma".
-include "freescale/opcode_base_lemmas_instrmode.ma".
-include "num/word16_lemmas.ma".
-
-(* ********************************************** *)
-(* MATTONI BASE PER DEFINIRE LE TABELLE DELLE MCU *)
-(* ********************************************** *)
-
-nlemma anyop_destruct : ∀m.∀x1,x2:opcode.anyOP m x1 = anyOP m x2 → x1 = x2.
- #m; #x1; #x2; #H;
- nchange with (match anyOP m x2 with [ anyOP a ⇒ x1 = a ]);
- nrewrite < H;
- nnormalize;
- napply refl_eq.
-nqed.
-
-nlemma symmetric_eqanyop : ∀m.∀op1,op2:any_opcode m.eq_anyop m op1 op2 = eq_anyop m op2 op1.
- #m;
- ncases m;
- #op1; #op2;
- ncases op1;
- #x1;
- ncases op2;
- #x2;
- nchange with (eq_op x1 x2 = eq_op x2 x1);
- nrewrite > (symmetric_eqop x1 x2);
- napply refl_eq.
-nqed.
-
-nlemma eqanyop_to_eq : ∀m.∀op1,op2:any_opcode m.eq_anyop m op1 op2 = true → op1 = op2.
- #m;
- ncases m;
- #op1; #op2;
- ncases op1;
- #x1;
- ncases op2;
- #x2;
- nchange with ((eq_op x1 x2 = true) → ?);
- #H;
- nrewrite > (eqop_to_eq … H);
- napply refl_eq.
-nqed.
-
-nlemma eq_to_eqanyop : ∀m.∀op1,op2:any_opcode m.op1 = op2 → eq_anyop m op1 op2 = true.
- #m;
- ncases m;
- #op1; #op2;
- ncases op1;
- #p1;
- ncases op2;
- #p2; #H;
- nrewrite > (anyop_destruct … H);
- nchange with (eq_op p2 p2 = true);
- nrewrite > (eq_to_eqop p2 p2 (refl_eq opcode p2));
- napply refl_eq.
-nqed.
-
-nlemma decidable_anyop : ∀m.∀x,y:any_opcode m.decidable (x = y).
- #m; #x; nelim x; #e1; #y; nelim y; #e2;
- nnormalize;
- napply (or2_elim (? = ?) (? ≠ ?) ? (decidable_op e1 e2) …);
- ##[ ##2: #H; napply (or2_intro2 (? = ?) (? ≠ ?) … ); nnormalize; #H1; napply (H (anyop_destruct m … H1))
- ##| ##1: #H; nrewrite > H; napply (or2_intro1 (? = ?) (? ≠ ?) (refl_eq …))
- ##]
-nqed.
-
-nlemma neqanyop_to_neq : ∀m.∀op1,op2:any_opcode m.(eq_anyop m op1 op2 = false) → (op1 ≠ op2).
- #m; #op1; nelim op1; #e1; #op2; nelim op2; #e2;
- nchange with (((eq_op e1 e2) = false) → ?);
- #H;
- nnormalize;
- #H1;
- napply (neqop_to_neq … H);
- napply (anyop_destruct m … H1).
-nqed.
-
-nlemma neq_to_neqanyop : ∀m.∀op1,op2:any_opcode m.op1 ≠ op2 → eq_anyop m op1 op2 = false.
- #m; #op1; nelim op1; #e1; #op2; nelim op2; #e2;
- #H; nchange with ((eq_op e1 e2) = false);
- napply (neq_to_neqop e1 e2 ?);
- nnormalize;
- #H1;
- nrewrite > H1 in H:(%); #H;
- napply (H (refl_eq …)).
-nqed.
-
-nlemma b8w16_destruct_b8_b8 : ∀x1,x2.Byte x1 = Byte x2 → x1 = x2.
- #x1; #x2; #H;
- nchange with (match Byte x2 with [ Byte a ⇒ x1 = a | Word _ ⇒ False ]);
- nrewrite < H;
- nnormalize;
- napply refl_eq.
-nqed.
-
-nlemma b8w16_destruct_w16_w16 : ∀x1,x2.Word x1 = Word x2 → x1 = x2.
- #x1; #x2; #H;
- nchange with (match Word x2 with [ Word a ⇒ x1 = a | Byte _ ⇒ False ]);
- nrewrite < H;
- nnormalize;
- napply refl_eq.
-nqed.
-
-nlemma b8w16_destruct_b8_w16 : ∀x1,x2.Byte x1 = Word x2 → False.
- #x1; #x2; #H;
- nchange with (match Byte x1 with [ Word _ ⇒ True | Byte a ⇒ False ]);
- nrewrite > H;
- nnormalize;
- napply I.
-nqed.
-
-nlemma b8w16_destruct_w16_b8 : ∀x1,x2.Word x1 = Byte x2 → False.
- #x1; #x2; #H;
- nchange with (match Word x1 with [ Word a ⇒ False | Byte _ ⇒ True ]);
- nrewrite > H;
- nnormalize;
- napply I.
-nqed.
-
-nlemma symmetric_eqb8w16 : ∀bw1,bw2.eq_b8w16 bw1 bw2 = eq_b8w16 bw2 bw1.
- #bw1; #bw2;
- ncases bw1;
- #x1;
- ncases bw2;
- #x2;
- ##[ ##1: nchange with (eq_b8 x1 x2 = eq_b8 x2 x1);
- nrewrite > (symmetric_eqb8 x1 x2);
- napply refl_eq
- ##| ##2,3: nnormalize; napply refl_eq
- ##| ##4: nchange with (eq_w16 x1 x2 = eq_w16 x2 x1);
- nrewrite > (symmetric_eqw16 x1 x2);
- napply refl_eq
- ##]
-nqed.
-
-nlemma eqb8w16_to_eq : ∀bw1,bw2.eq_b8w16 bw1 bw2 = true → bw1 = bw2.
- #bw1; #bw2;
- ncases bw1; #e1; ncases bw2; #e2;
- ##[ ##1: nchange with ((eq_b8 e1 e2 = true) → ?); #H; nrewrite > (eqb8_to_eq … H); napply refl_eq
- ##| ##2,3: nnormalize; #H; napply (bool_destruct … H)
- ##| ##4: nchange with ((eq_w16 e1 e2 = true) → ?); #H; nrewrite > (eqw16_to_eq … H); napply refl_eq
- ##]
-nqed.
-
-nlemma eq_to_eqb8w16 : ∀bw1,bw2.bw1 = bw2 → eq_b8w16 bw1 bw2 = true.
- #bw1; #bw2;
- ncases bw1; #e1; ncases bw2; #e2;
- ##[ ##1: #H; nrewrite > (b8w16_destruct_b8_b8 … H);
- nchange with (eq_b8 e2 e2 = true);
- nrewrite > (eq_to_eqb8 e2 e2 (refl_eq …));
- napply refl_eq
- ##| ##2: #H; nelim (b8w16_destruct_b8_w16 … H)
- ##| ##3: #H; nelim (b8w16_destruct_w16_b8 … H);
- ##| ##4: #H; nrewrite > (b8w16_destruct_w16_w16 … H);
- nchange with (eq_w16 e2 e2 = true);
- nrewrite > (eq_to_eqw16 e2 e2 (refl_eq …));
- napply refl_eq
- ##]
-nqed.
-
-nlemma decidable_b8w16 : ∀x,y:byte8_or_word16.decidable (x = y).
- #x; nelim x; #e1; #y; nelim y; #e2;
- nnormalize;
- ##[ ##1: napply (or2_elim (? = ?) (? ≠ ?) ? (decidable_b8 e1 e2) …);
- ##[ ##2: #H; napply (or2_intro2 (? = ?) (? ≠ ?) … ); nnormalize; #H1; napply (H (b8w16_destruct_b8_b8 … H1))
- ##| ##1: #H; nrewrite > H; napply (or2_intro1 (? = ?) (? ≠ ?) (refl_eq …))
- ##]
- ##| ##2: napply (or2_intro2 (? = ?) (? ≠ ?) …); nnormalize; #H; napply (b8w16_destruct_b8_w16 … H)
- ##| ##3: napply (or2_intro2 (? = ?) (? ≠ ?) …); nnormalize; #H; napply (b8w16_destruct_w16_b8 … H)
- ##| ##4: napply (or2_elim (? = ?) (? ≠ ?) ? (decidable_w16 e1 e2) …);
- ##[ ##2: #H; napply (or2_intro2 (? = ?) (? ≠ ?) … ); nnormalize; #H1; napply (H (b8w16_destruct_w16_w16 … H1))
- ##| ##1: #H; nrewrite > H; napply (or2_intro1 (? = ?) (? ≠ ?) (refl_eq …))
- ##]
- ##]
-nqed.
-
-nlemma neqb8w16_to_neq : ∀bw1,bw2.eq_b8w16 bw1 bw2 = false → bw1 ≠ bw2.
- #bw1; #bw2;
- ncases bw1; #e1; ncases bw2; #e2;
- ##[ ##1: nchange with ((eq_b8 e1 e2 = false) → ?); #H;
- nnormalize; #H1; napply (neqb8_to_neq … H); napply (b8w16_destruct_b8_b8 … H1)
- ##| ##2: nnormalize; #H; #H1; napply (b8w16_destruct_b8_w16 … H1)
- ##| ##3: nnormalize; #H; #H1; napply (b8w16_destruct_w16_b8 … H1)
- ##| ##4: nchange with ((eq_w16 e1 e2 = false) → ?); #H;
- nnormalize; #H1; napply (neqw16_to_neq … H); napply (b8w16_destruct_w16_w16 … H1)
- ##]
-nqed.
projects / helm.git / blobdiff