1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 (* ********************************************************************** *)
16 (* Progetto FreeScale *)
18 (* Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it *)
19 (* Ultima modifica: 05/08/2009 *)
21 (* ********************************************************************** *)
23 include "freescale/opcode_base_lemmas_opcode.ma".
24 include "freescale/opcode_base_lemmas_instrmode.ma".
25 include "num/word16_lemmas.ma".
27 (* ********************************************** *)
28 (* MATTONI BASE PER DEFINIRE LE TABELLE DELLE MCU *)
29 (* ********************************************** *)
31 nlemma anyop_destruct : ∀m.∀x1,x2:opcode.anyOP m x1 = anyOP m x2 → x1 = x2.
33 nchange with (match anyOP m x2 with [ anyOP a ⇒ x1 = a ]);
39 nlemma symmetric_eqanyop : ∀m.∀op1,op2:any_opcode m.eq_anyop m op1 op2 = eq_anyop m op2 op1.
47 nchange with (eq_op x1 x2 = eq_op x2 x1);
48 nrewrite > (symmetric_eqop x1 x2);
52 nlemma eqanyop_to_eq : ∀m.∀op1,op2:any_opcode m.eq_anyop m op1 op2 = true → op1 = op2.
60 nchange with ((eq_op x1 x2 = true) → ?);
62 nrewrite > (eqop_to_eq … H);
66 nlemma eq_to_eqanyop : ∀m.∀op1,op2:any_opcode m.op1 = op2 → eq_anyop m op1 op2 = true.
74 nrewrite > (anyop_destruct … H);
75 nchange with (eq_op p2 p2 = true);
76 nrewrite > (eq_to_eqop p2 p2 (refl_eq opcode p2));
80 nlemma decidable_anyop : ∀m.∀x,y:any_opcode m.decidable (x = y).
81 #m; #x; nelim x; #e1; #y; nelim y; #e2;
83 napply (or2_elim (? = ?) (? ≠ ?) ? (decidable_op e1 e2) …);
84 ##[ ##2: #H; napply (or2_intro2 (? = ?) (? ≠ ?) … ); nnormalize; #H1; napply (H (anyop_destruct m … H1))
85 ##| ##1: #H; nrewrite > H; napply (or2_intro1 (? = ?) (? ≠ ?) (refl_eq …))
89 nlemma neqanyop_to_neq : ∀m.∀op1,op2:any_opcode m.(eq_anyop m op1 op2 = false) → (op1 ≠ op2).
90 #m; #op1; nelim op1; #e1; #op2; nelim op2; #e2;
91 nchange with (((eq_op e1 e2) = false) → ?);
95 napply (neqop_to_neq … H);
96 napply (anyop_destruct m … H1).
99 nlemma neq_to_neqanyop : ∀m.∀op1,op2:any_opcode m.op1 ≠ op2 → eq_anyop m op1 op2 = false.
100 #m; #op1; nelim op1; #e1; #op2; nelim op2; #e2;
101 #H; nchange with ((eq_op e1 e2) = false);
102 napply (neq_to_neqop e1 e2 ?);
105 nrewrite > H1 in H:(%); #H;
106 napply (H (refl_eq …)).
109 nlemma b8w16_destruct_b8_b8 : ∀x1,x2.Byte x1 = Byte x2 → x1 = x2.
111 nchange with (match Byte x2 with [ Byte a ⇒ x1 = a | Word _ ⇒ False ]);
117 nlemma b8w16_destruct_w16_w16 : ∀x1,x2.Word x1 = Word x2 → x1 = x2.
119 nchange with (match Word x2 with [ Word a ⇒ x1 = a | Byte _ ⇒ False ]);
125 nlemma b8w16_destruct_b8_w16 : ∀x1,x2.Byte x1 = Word x2 → False.
127 nchange with (match Byte x1 with [ Word _ ⇒ True | Byte a ⇒ False ]);
133 nlemma b8w16_destruct_w16_b8 : ∀x1,x2.Word x1 = Byte x2 → False.
135 nchange with (match Word x1 with [ Word a ⇒ False | Byte _ ⇒ True ]);
141 nlemma symmetric_eqb8w16 : ∀bw1,bw2.eq_b8w16 bw1 bw2 = eq_b8w16 bw2 bw1.
147 ##[ ##1: nchange with (eq_b8 x1 x2 = eq_b8 x2 x1);
148 nrewrite > (symmetric_eqb8 x1 x2);
150 ##| ##2,3: nnormalize; napply refl_eq
151 ##| ##4: nchange with (eq_w16 x1 x2 = eq_w16 x2 x1);
152 nrewrite > (symmetric_eqw16 x1 x2);
157 nlemma eqb8w16_to_eq : ∀bw1,bw2.eq_b8w16 bw1 bw2 = true → bw1 = bw2.
159 ncases bw1; #e1; ncases bw2; #e2;
160 ##[ ##1: nchange with ((eq_b8 e1 e2 = true) → ?); #H; nrewrite > (eqb8_to_eq … H); napply refl_eq
161 ##| ##2,3: nnormalize; #H; napply (bool_destruct … H)
162 ##| ##4: nchange with ((eq_w16 e1 e2 = true) → ?); #H; nrewrite > (eqw16_to_eq … H); napply refl_eq
166 nlemma eq_to_eqb8w16 : ∀bw1,bw2.bw1 = bw2 → eq_b8w16 bw1 bw2 = true.
168 ncases bw1; #e1; ncases bw2; #e2;
169 ##[ ##1: #H; nrewrite > (b8w16_destruct_b8_b8 … H);
170 nchange with (eq_b8 e2 e2 = true);
171 nrewrite > (eq_to_eqb8 e2 e2 (refl_eq …));
173 ##| ##2: #H; nelim (b8w16_destruct_b8_w16 … H)
174 ##| ##3: #H; nelim (b8w16_destruct_w16_b8 … H);
175 ##| ##4: #H; nrewrite > (b8w16_destruct_w16_w16 … H);
176 nchange with (eq_w16 e2 e2 = true);
177 nrewrite > (eq_to_eqw16 e2 e2 (refl_eq …));
182 nlemma decidable_b8w16 : ∀x,y:byte8_or_word16.decidable (x = y).
183 #x; nelim x; #e1; #y; nelim y; #e2;
185 ##[ ##1: napply (or2_elim (? = ?) (? ≠ ?) ? (decidable_b8 e1 e2) …);
186 ##[ ##2: #H; napply (or2_intro2 (? = ?) (? ≠ ?) … ); nnormalize; #H1; napply (H (b8w16_destruct_b8_b8 … H1))
187 ##| ##1: #H; nrewrite > H; napply (or2_intro1 (? = ?) (? ≠ ?) (refl_eq …))
189 ##| ##2: napply (or2_intro2 (? = ?) (? ≠ ?) …); nnormalize; #H; napply (b8w16_destruct_b8_w16 … H)
190 ##| ##3: napply (or2_intro2 (? = ?) (? ≠ ?) …); nnormalize; #H; napply (b8w16_destruct_w16_b8 … H)
191 ##| ##4: napply (or2_elim (? = ?) (? ≠ ?) ? (decidable_w16 e1 e2) …);
192 ##[ ##2: #H; napply (or2_intro2 (? = ?) (? ≠ ?) … ); nnormalize; #H1; napply (H (b8w16_destruct_w16_w16 … H1))
193 ##| ##1: #H; nrewrite > H; napply (or2_intro1 (? = ?) (? ≠ ?) (refl_eq …))
198 nlemma neqb8w16_to_neq : ∀bw1,bw2.eq_b8w16 bw1 bw2 = false → bw1 ≠ bw2.
200 ncases bw1; #e1; ncases bw2; #e2;
201 ##[ ##1: nchange with ((eq_b8 e1 e2 = false) → ?); #H;
202 nnormalize; #H1; napply (neqb8_to_neq … H); napply (b8w16_destruct_b8_b8 … H1)
203 ##| ##2: nnormalize; #H; #H1; napply (b8w16_destruct_b8_w16 … H1)
204 ##| ##3: nnormalize; #H; #H1; napply (b8w16_destruct_w16_b8 … H1)
205 ##| ##4: nchange with ((eq_w16 e1 e2 = false) → ?); #H;
206 nnormalize; #H1; napply (neqw16_to_neq … H); napply (b8w16_destruct_w16_w16 … H1)