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 (* Sviluppo: 2008-2010 *)
21 (* ********************************************************************** *)
23 include "num/word16_lemmas.ma".
24 include "emulator/status/RS08_status.ma".
26 (* *********************************** *)
27 (* STATUS INTERNO DEL PROCESSORE (ALU) *)
28 (* *********************************** *)
30 nlemma aluRS08_destruct_1 :
31 ∀x1,x2,x3,x4,x5,x6,x7,x8,y1,y2,y3,y4,y5,y6,y7,y8.
32 mk_alu_RS08 x1 x2 x3 x4 x5 x6 x7 x8 = mk_alu_RS08 y1 y2 y3 y4 y5 y6 y7 y8 →
34 #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8;
35 #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #H;
36 nchange with (match mk_alu_RS08 y1 y2 y3 y4 y5 y6 y7 y8
37 with [ mk_alu_RS08 a _ _ _ _ _ _ _ ⇒ x1 = a ]);
43 nlemma aluRS08_destruct_2 :
44 ∀x1,x2,x3,x4,x5,x6,x7,x8,y1,y2,y3,y4,y5,y6,y7,y8.
45 mk_alu_RS08 x1 x2 x3 x4 x5 x6 x7 x8 = mk_alu_RS08 y1 y2 y3 y4 y5 y6 y7 y8 →
47 #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8;
48 #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #H;
49 nchange with (match mk_alu_RS08 y1 y2 y3 y4 y5 y6 y7 y8
50 with [ mk_alu_RS08 _ a _ _ _ _ _ _ ⇒ x2 = a ]);
56 nlemma aluRS08_destruct_3 :
57 ∀x1,x2,x3,x4,x5,x6,x7,x8,y1,y2,y3,y4,y5,y6,y7,y8.
58 mk_alu_RS08 x1 x2 x3 x4 x5 x6 x7 x8 = mk_alu_RS08 y1 y2 y3 y4 y5 y6 y7 y8 →
60 #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8;
61 #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #H;
62 nchange with (match mk_alu_RS08 y1 y2 y3 y4 y5 y6 y7 y8
63 with [ mk_alu_RS08 _ _ a _ _ _ _ _ ⇒ x3 = a ]);
69 nlemma aluRS08_destruct_4 :
70 ∀x1,x2,x3,x4,x5,x6,x7,x8,y1,y2,y3,y4,y5,y6,y7,y8.
71 mk_alu_RS08 x1 x2 x3 x4 x5 x6 x7 x8 = mk_alu_RS08 y1 y2 y3 y4 y5 y6 y7 y8 →
73 #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8;
74 #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #H;
75 nchange with (match mk_alu_RS08 y1 y2 y3 y4 y5 y6 y7 y8
76 with [ mk_alu_RS08 _ _ _ a _ _ _ _ ⇒ x4 = a ]);
82 nlemma aluRS08_destruct_5 :
83 ∀x1,x2,x3,x4,x5,x6,x7,x8,y1,y2,y3,y4,y5,y6,y7,y8.
84 mk_alu_RS08 x1 x2 x3 x4 x5 x6 x7 x8 = mk_alu_RS08 y1 y2 y3 y4 y5 y6 y7 y8 →
86 #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8;
87 #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #H;
88 nchange with (match mk_alu_RS08 y1 y2 y3 y4 y5 y6 y7 y8
89 with [ mk_alu_RS08 _ _ _ _ a _ _ _ ⇒ x5 = a ]);
95 nlemma aluRS08_destruct_6 :
96 ∀x1,x2,x3,x4,x5,x6,x7,x8,y1,y2,y3,y4,y5,y6,y7,y8.
97 mk_alu_RS08 x1 x2 x3 x4 x5 x6 x7 x8 = mk_alu_RS08 y1 y2 y3 y4 y5 y6 y7 y8 →
99 #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8;
100 #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #H;
101 nchange with (match mk_alu_RS08 y1 y2 y3 y4 y5 y6 y7 y8
102 with [ mk_alu_RS08 _ _ _ _ _ a _ _ ⇒ x6 = a ]);
108 nlemma aluRS08_destruct_7 :
109 ∀x1,x2,x3,x4,x5,x6,x7,x8,y1,y2,y3,y4,y5,y6,y7,y8.
110 mk_alu_RS08 x1 x2 x3 x4 x5 x6 x7 x8 = mk_alu_RS08 y1 y2 y3 y4 y5 y6 y7 y8 →
112 #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8;
113 #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #H;
114 nchange with (match mk_alu_RS08 y1 y2 y3 y4 y5 y6 y7 y8
115 with [ mk_alu_RS08 _ _ _ _ _ _ a _ ⇒ x7 = a ]);
121 nlemma aluRS08_destruct_8 :
122 ∀x1,x2,x3,x4,x5,x6,x7,x8,y1,y2,y3,y4,y5,y6,y7,y8.
123 mk_alu_RS08 x1 x2 x3 x4 x5 x6 x7 x8 = mk_alu_RS08 y1 y2 y3 y4 y5 y6 y7 y8 →
125 #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8;
126 #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #H;
127 nchange with (match mk_alu_RS08 y1 y2 y3 y4 y5 y6 y7 y8
128 with [ mk_alu_RS08 _ _ _ _ _ _ _ a ⇒ x8 = a ]);
134 nlemma symmetric_eqaluRS08 : symmetricT alu_RS08 bool eq_RS08_alu.
137 #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8;
139 #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8;
141 ((eq_b8 x1 y1) ⊗ (eq_w16 x2 y2) ⊗
142 (eq_w16 x3 y3) ⊗ (eq_w16 x4 y4) ⊗
143 (eq_b8 x5 y5) ⊗ (eq_b8 x6 y6) ⊗
144 (eq_bool x7 y7) ⊗ (eq_bool x8 y8)) =
145 ((eq_b8 y1 x1) ⊗ (eq_w16 y2 x2) ⊗
146 (eq_w16 y3 x3) ⊗ (eq_w16 y4 x4) ⊗
147 (eq_b8 y5 x5) ⊗ (eq_b8 y6 x6) ⊗
148 (eq_bool y7 x7) ⊗ (eq_bool y8 x8)));
149 nrewrite > (symmetric_eqb8 x1 y1);
150 nrewrite > (symmetric_eqw16 x2 y2);
151 nrewrite > (symmetric_eqw16 x3 y3);
152 nrewrite > (symmetric_eqw16 x4 y4);
153 nrewrite > (symmetric_eqb8 x5 y5);
154 nrewrite > (symmetric_eqb8 x6 y6);
155 nrewrite > (symmetric_eqbool x7 y7);
156 nrewrite > (symmetric_eqbool x8 y8);
160 nlemma eqaluRS08_to_eq : ∀alu1,alu2.eq_RS08_alu alu1 alu2 = true → alu1 = alu2.
163 #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8;
165 #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #H;
166 nchange in H:(%) with (
167 ((eq_b8 x1 y1) ⊗ (eq_w16 x2 y2) ⊗
168 (eq_w16 x3 y3) ⊗ (eq_w16 x4 y4) ⊗
169 (eq_b8 x5 y5) ⊗ (eq_b8 x6 y6) ⊗
170 (eq_bool x7 y7) ⊗ (eq_bool x8 y8)) = true);
171 nrewrite > (eqbool_to_eq … (andb_true_true_r … H));
172 nletin H1 ≝ (andb_true_true_l … H);
173 nrewrite > (eqbool_to_eq … (andb_true_true_r … H1));
174 nletin H2 ≝ (andb_true_true_l … H1);
175 nrewrite > (eqb8_to_eq … (andb_true_true_r … H2));
176 nletin H3 ≝ (andb_true_true_l … H2);
177 nrewrite > (eqb8_to_eq … (andb_true_true_r … H3));
178 nletin H4 ≝ (andb_true_true_l … H3);
179 nrewrite > (eqw16_to_eq … (andb_true_true_r … H4));
180 nletin H5 ≝ (andb_true_true_l … H4);
181 nrewrite > (eqw16_to_eq … (andb_true_true_r … H5));
182 nletin H6 ≝ (andb_true_true_l … H5);
183 nrewrite > (eqw16_to_eq … (andb_true_true_r … H6));
184 nrewrite > (eqb8_to_eq … (andb_true_true_l … H6));
188 nlemma eq_to_eqaluRS08 : ∀alu1,alu2.alu1 = alu2 → eq_RS08_alu alu1 alu2 = true.
191 #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8;
193 #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #H;
194 nrewrite > (aluRS08_destruct_1 … H);
195 nrewrite > (aluRS08_destruct_2 … H);
196 nrewrite > (aluRS08_destruct_3 … H);
197 nrewrite > (aluRS08_destruct_4 … H);
198 nrewrite > (aluRS08_destruct_5 … H);
199 nrewrite > (aluRS08_destruct_6 … H);
200 nrewrite > (aluRS08_destruct_7 … H);
201 nrewrite > (aluRS08_destruct_8 … H);
203 ((eq_b8 y1 y1) ⊗ (eq_w16 y2 y2) ⊗
204 (eq_w16 y3 y3) ⊗ (eq_w16 y4 y4) ⊗
205 (eq_b8 y5 y5) ⊗ (eq_b8 y6 y6) ⊗
206 (eq_bool y7 y7) ⊗ (eq_bool y8 y8)) = true);
207 nrewrite > (eq_to_eqb8 y1 y1 (refl_eq …));
208 nrewrite > (eq_to_eqw16 y2 y2 (refl_eq …));
209 nrewrite > (eq_to_eqw16 y3 y3 (refl_eq …));
210 nrewrite > (eq_to_eqw16 y4 y4 (refl_eq …));
211 nrewrite > (eq_to_eqb8 y5 y5 (refl_eq …));
212 nrewrite > (eq_to_eqb8 y6 y6 (refl_eq …));
213 nrewrite > (eq_to_eqbool y7 y7 (refl_eq …));
214 nrewrite > (eq_to_eqbool y8 y8 (refl_eq …));
218 nlemma decidable_aluRS08_aux1
219 : ∀x1,x2,x3,x4,x5,x6,x7,x8,y1,y2,y3,y4,y5,y6,y7,y8.
221 (mk_alu_RS08 x1 x2 x3 x4 x5 x6 x7 x8) ≠
222 (mk_alu_RS08 y1 y2 y3 y4 y5 y6 y7 y8).
223 #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8;
224 #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8;
226 napply (H (aluRS08_destruct_1 … H1)).
229 nlemma decidable_aluRS08_aux2
230 : ∀x1,x2,x3,x4,x5,x6,x7,x8,y1,y2,y3,y4,y5,y6,y7,y8.
232 (mk_alu_RS08 x1 x2 x3 x4 x5 x6 x7 x8) ≠
233 (mk_alu_RS08 y1 y2 y3 y4 y5 y6 y7 y8).
234 #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8;
235 #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8;
237 napply (H (aluRS08_destruct_2 … H1)).
240 nlemma decidable_aluRS08_aux3
241 : ∀x1,x2,x3,x4,x5,x6,x7,x8,y1,y2,y3,y4,y5,y6,y7,y8.
243 (mk_alu_RS08 x1 x2 x3 x4 x5 x6 x7 x8) ≠
244 (mk_alu_RS08 y1 y2 y3 y4 y5 y6 y7 y8).
245 #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8;
246 #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8;
248 napply (H (aluRS08_destruct_3 … H1)).
251 nlemma decidable_aluRS08_aux4
252 : ∀x1,x2,x3,x4,x5,x6,x7,x8,y1,y2,y3,y4,y5,y6,y7,y8.
254 (mk_alu_RS08 x1 x2 x3 x4 x5 x6 x7 x8) ≠
255 (mk_alu_RS08 y1 y2 y3 y4 y5 y6 y7 y8).
256 #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8;
257 #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8;
259 napply (H (aluRS08_destruct_4 … H1)).
262 nlemma decidable_aluRS08_aux5
263 : ∀x1,x2,x3,x4,x5,x6,x7,x8,y1,y2,y3,y4,y5,y6,y7,y8.
265 (mk_alu_RS08 x1 x2 x3 x4 x5 x6 x7 x8) ≠
266 (mk_alu_RS08 y1 y2 y3 y4 y5 y6 y7 y8).
267 #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8;
268 #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8;
270 napply (H (aluRS08_destruct_5 … H1)).
273 nlemma decidable_aluRS08_aux6
274 : ∀x1,x2,x3,x4,x5,x6,x7,x8,y1,y2,y3,y4,y5,y6,y7,y8.
276 (mk_alu_RS08 x1 x2 x3 x4 x5 x6 x7 x8) ≠
277 (mk_alu_RS08 y1 y2 y3 y4 y5 y6 y7 y8).
278 #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8;
279 #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8;
281 napply (H (aluRS08_destruct_6 … H1)).
284 nlemma decidable_aluRS08_aux7
285 : ∀x1,x2,x3,x4,x5,x6,x7,x8,y1,y2,y3,y4,y5,y6,y7,y8.
287 (mk_alu_RS08 x1 x2 x3 x4 x5 x6 x7 x8) ≠
288 (mk_alu_RS08 y1 y2 y3 y4 y5 y6 y7 y8).
289 #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8;
290 #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8;
292 napply (H (aluRS08_destruct_7 … H1)).
295 nlemma decidable_aluRS08_aux8
296 : ∀x1,x2,x3,x4,x5,x6,x7,x8,y1,y2,y3,y4,y5,y6,y7,y8.
298 (mk_alu_RS08 x1 x2 x3 x4 x5 x6 x7 x8) ≠
299 (mk_alu_RS08 y1 y2 y3 y4 y5 y6 y7 y8).
300 #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8;
301 #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8;
303 napply (H (aluRS08_destruct_8 … H1)).
306 nlemma decidable_aluRS08 : ∀x,y:alu_RS08.decidable (x = y).
307 #x; nelim x; #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8;
308 #y; nelim y; #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8;
310 napply (or2_elim (? = ?) (? ≠ ?) ? (decidable_b8 x1 y1) …);
311 ##[ ##2: #H; napply (or2_intro2 … (decidable_aluRS08_aux1 … H))
312 ##| ##1: #H; napply (or2_elim (? = ?) (? ≠ ?) ? (decidable_w16 x2 y2) …);
313 ##[ ##2: #H1; napply (or2_intro2 … (decidable_aluRS08_aux2 … H1))
314 ##| ##1: #H1; napply (or2_elim (? = ?) (? ≠ ?) ? (decidable_w16 x3 y3) …);
315 ##[ ##2: #H2; napply (or2_intro2 … (decidable_aluRS08_aux3 … H2))
316 ##| ##1: #H2; napply (or2_elim (? = ?) (? ≠ ?) ? (decidable_w16 x4 y4) …);
317 ##[ ##2: #H3; napply (or2_intro2 … (decidable_aluRS08_aux4 … H3))
318 ##| ##1: #H3; napply (or2_elim (? = ?) (? ≠ ?) ? (decidable_b8 x5 y5) …);
319 ##[ ##2: #H4; napply (or2_intro2 … (decidable_aluRS08_aux5 … H4))
320 ##| ##1: #H4; napply (or2_elim (? = ?) (? ≠ ?) ? (decidable_b8 x6 y6) …);
321 ##[ ##2: #H5; napply (or2_intro2 … (decidable_aluRS08_aux6 … H5))
322 ##| ##1: #H5; napply (or2_elim (? = ?) (? ≠ ?) ? (decidable_bool x7 y7) …);
323 ##[ ##2: #H6; napply (or2_intro2 … (decidable_aluRS08_aux7 … H6))
324 ##| ##1: #H6; napply (or2_elim (? = ?) (? ≠ ?) ? (decidable_bool x8 y8) …);
325 ##[ ##2: #H7; napply (or2_intro2 … (decidable_aluRS08_aux8 … H7))
326 ##| ##1: #H7; nrewrite > H; nrewrite > H1; nrewrite > H2; nrewrite > H3;
327 nrewrite > H4; nrewrite > H5; nrewrite > H6; nrewrite > H7;
328 napply (or2_intro1 (? = ?) (? ≠ ?) (refl_eq …))