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 "emulator/status/HC08_status_base.ma".
25 (* *********************************** *)
26 (* STATUS INTERNO DEL PROCESSORE (ALU) *)
27 (* *********************************** *)
29 nlemma aluHC08_destruct_1 :
30 ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12.
31 mk_alu_HC08 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 = mk_alu_HC08 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 →
33 #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12;
34 #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #H;
35 nchange with (match mk_alu_HC08 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12
36 with [ mk_alu_HC08 a _ _ _ _ _ _ _ _ _ _ _ ⇒ x1 = a ]);
42 nlemma aluHC08_destruct_2 :
43 ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12.
44 mk_alu_HC08 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 = mk_alu_HC08 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 →
46 #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12;
47 #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #H;
48 nchange with (match mk_alu_HC08 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12
49 with [ mk_alu_HC08 _ a _ _ _ _ _ _ _ _ _ _ ⇒ x2 = a ]);
55 nlemma aluHC08_destruct_3 :
56 ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12.
57 mk_alu_HC08 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 = mk_alu_HC08 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 →
59 #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12;
60 #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #H;
61 nchange with (match mk_alu_HC08 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12
62 with [ mk_alu_HC08 _ _ a _ _ _ _ _ _ _ _ _ ⇒ x3 = a ]);
68 nlemma aluHC08_destruct_4 :
69 ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12.
70 mk_alu_HC08 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 = mk_alu_HC08 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 →
72 #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12;
73 #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #H;
74 nchange with (match mk_alu_HC08 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12
75 with [ mk_alu_HC08 _ _ _ a _ _ _ _ _ _ _ _ ⇒ x4 = a ]);
81 nlemma aluHC08_destruct_5 :
82 ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12.
83 mk_alu_HC08 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 = mk_alu_HC08 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 →
85 #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12;
86 #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #H;
87 nchange with (match mk_alu_HC08 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12
88 with [ mk_alu_HC08 _ _ _ _ a _ _ _ _ _ _ _ ⇒ x5 = a ]);
94 nlemma aluHC08_destruct_6 :
95 ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12.
96 mk_alu_HC08 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 = mk_alu_HC08 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 →
98 #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12;
99 #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #H;
100 nchange with (match mk_alu_HC08 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12
101 with [ mk_alu_HC08 _ _ _ _ _ a _ _ _ _ _ _ ⇒ x6 = a ]);
107 nlemma aluHC08_destruct_7 :
108 ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12.
109 mk_alu_HC08 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 = mk_alu_HC08 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 →
111 #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12;
112 #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #H;
113 nchange with (match mk_alu_HC08 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12
114 with [ mk_alu_HC08 _ _ _ _ _ _ a _ _ _ _ _ ⇒ x7 = a ]);
120 nlemma aluHC08_destruct_8 :
121 ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12.
122 mk_alu_HC08 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 = mk_alu_HC08 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 →
124 #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12;
125 #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #H;
126 nchange with (match mk_alu_HC08 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12
127 with [ mk_alu_HC08 _ _ _ _ _ _ _ a _ _ _ _ ⇒ x8 = a ]);
133 nlemma aluHC08_destruct_9 :
134 ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12.
135 mk_alu_HC08 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 = mk_alu_HC08 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 →
137 #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12;
138 #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #H;
139 nchange with (match mk_alu_HC08 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12
140 with [ mk_alu_HC08 _ _ _ _ _ _ _ _ a _ _ _ ⇒ x9 = a ]);
146 nlemma aluHC08_destruct_10 :
147 ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12.
148 mk_alu_HC08 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 = mk_alu_HC08 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 →
150 #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12;
151 #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #H;
152 nchange with (match mk_alu_HC08 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12
153 with [ mk_alu_HC08 _ _ _ _ _ _ _ _ _ a _ _ ⇒ x10 = a ]);
159 nlemma aluHC08_destruct_11 :
160 ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12.
161 mk_alu_HC08 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 = mk_alu_HC08 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 →
163 #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12;
164 #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #H;
165 nchange with (match mk_alu_HC08 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12
166 with [ mk_alu_HC08 _ _ _ _ _ _ _ _ _ _ a _ ⇒ x11 = a ]);
172 nlemma aluHC08_destruct_12 :
173 ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12.
174 mk_alu_HC08 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 = mk_alu_HC08 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 →
176 #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12;
177 #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #H;
178 nchange with (match mk_alu_HC08 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12
179 with [ mk_alu_HC08 _ _ _ _ _ _ _ _ _ _ _ a ⇒ x12 = a ]);
185 nlemma eq_to_eqaluHC08 : ∀alu1,alu2.alu1 = alu2 → eq_HC08_alu alu1 alu2 = true.
188 #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12;
190 #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #H;
191 nrewrite > (aluHC08_destruct_1 … H);
192 nrewrite > (aluHC08_destruct_2 … H);
193 nrewrite > (aluHC08_destruct_3 … H);
194 nrewrite > (aluHC08_destruct_4 … H);
195 nrewrite > (aluHC08_destruct_5 … H);
196 nrewrite > (aluHC08_destruct_6 … H);
197 nrewrite > (aluHC08_destruct_7 … H);
198 nrewrite > (aluHC08_destruct_8 … H);
199 nrewrite > (aluHC08_destruct_9 … H);
200 nrewrite > (aluHC08_destruct_10 … H);
201 nrewrite > (aluHC08_destruct_11 … H);
202 nrewrite > (aluHC08_destruct_12 … H);
204 ((eqc ? y1 y1) ⊗ (eqc ? y2 y2) ⊗ (eqc ? y3 y3) ⊗ (eqc ? y4 y4) ⊗
205 (eqc ? y5 y5) ⊗ (eqc ? y6 y6) ⊗ (eqc ? y7 y7) ⊗ (eqc ? y8 y8) ⊗
206 (eqc ? y9 y9) ⊗ (eqc ? y10 y10) ⊗ (eqc ? y11 y11) ⊗ (eqc ? y12 y12)) = true);
207 nrewrite > (eq_to_eqc ? y1 y1 (refl_eq …));
208 nrewrite > (eq_to_eqc ? y2 y2 (refl_eq …));
209 nrewrite > (eq_to_eqc ? y3 y3 (refl_eq …));
210 nrewrite > (eq_to_eqc ? y4 y4 (refl_eq …));
211 nrewrite > (eq_to_eqc ? y5 y5 (refl_eq …));
212 nrewrite > (eq_to_eqc ? y6 y6 (refl_eq …));
213 nrewrite > (eq_to_eqc ? y7 y7 (refl_eq …));
214 nrewrite > (eq_to_eqc ? y8 y8 (refl_eq …));
215 nrewrite > (eq_to_eqc ? y9 y9 (refl_eq …));
216 nrewrite > (eq_to_eqc ? y10 y10 (refl_eq …));
217 nrewrite > (eq_to_eqc ? y11 y11 (refl_eq …));
218 nrewrite > (eq_to_eqc ? y12 y12 (refl_eq …));
222 nlemma neqaluHC08_to_neq : ∀alu1,alu2.eq_HC08_alu alu1 alu2 = false → alu1 ≠ alu2.
224 napply (not_to_not (s1 = s2) (eq_HC08_alu s1 s2 = true) …);
225 ##[ ##1: napply (eq_to_eqaluHC08 s1 s2)
226 ##| ##2: napply (eqfalse_to_neqtrue … H)
230 nlemma eqaluHC08_to_eq : ∀alu1,alu2.eq_HC08_alu alu1 alu2 = true → alu1 = alu2.
233 #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12;
235 #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #H;
236 nchange in H:(%) with (
237 ((eqc ? x1 y1) ⊗ (eqc ? x2 y2) ⊗ (eqc ? x3 y3) ⊗ (eqc ? x4 y4) ⊗
238 (eqc ? x5 y5) ⊗ (eqc ? x6 y6) ⊗ (eqc ? x7 y7) ⊗ (eqc ? x8 y8) ⊗
239 (eqc ? x9 y9) ⊗ (eqc ? x10 y10) ⊗ (eqc ? x11 y11) ⊗ (eqc ? x12 y12)) = true);
240 nrewrite > (eqc_to_eq … (andb_true_true_r … H));
241 nletin H1 ≝ (andb_true_true_l … H);
242 nrewrite > (eqc_to_eq … (andb_true_true_r … H1));
243 nletin H2 ≝ (andb_true_true_l … H1);
244 nrewrite > (eqc_to_eq … (andb_true_true_r … H2));
245 nletin H3 ≝ (andb_true_true_l … H2);
246 nrewrite > (eqc_to_eq … (andb_true_true_r … H3));
247 nletin H4 ≝ (andb_true_true_l … H3);
248 nrewrite > (eqc_to_eq … (andb_true_true_r … H4));
249 nletin H5 ≝ (andb_true_true_l … H4);
250 nrewrite > (eqc_to_eq … (andb_true_true_r … H5));
251 nletin H6 ≝ (andb_true_true_l … H5);
252 nrewrite > (eqc_to_eq … (andb_true_true_r … H6));
253 nletin H7 ≝ (andb_true_true_l … H6);
254 nrewrite > (eqc_to_eq … (andb_true_true_r … H7));
255 nletin H8 ≝ (andb_true_true_l … H7);
256 nrewrite > (eqc_to_eq … (andb_true_true_r … H8));
257 nletin H9 ≝ (andb_true_true_l … H8);
258 nrewrite > (eqc_to_eq … (andb_true_true_r … H9));
259 nletin H10 ≝ (andb_true_true_l … H9);
260 nrewrite > (eqc_to_eq … (andb_true_true_r … H10));
261 nrewrite > (eqc_to_eq … (andb_true_true_l … H10));
265 nlemma neq_to_neqaluHC08 : ∀alu1,alu2.alu1 ≠ alu2 → eq_HC08_alu alu1 alu2 = false.
267 napply (neqtrue_to_eqfalse (eq_HC08_alu s1 s2));
268 napply (not_to_not (eq_HC08_alu s1 s2 = true) (s1 = s2) ? H);
269 napply (eqaluHC08_to_eq s1 s2).
272 nlemma decidable_aluHC08 : ∀x,y:alu_HC08.decidable (x = y).
274 napply (or2_elim (eq_HC08_alu x y = true) (eq_HC08_alu x y = false) ? (decidable_bexpr ?));
275 ##[ ##1: #H; napply (or2_intro1 (x = y) (x ≠ y) (eqaluHC08_to_eq … H))
276 ##| ##2: #H; napply (or2_intro2 (x = y) (x ≠ y) (neqaluHC08_to_neq … H))
280 nlemma symmetric_eqaluHC08 : symmetricT alu_HC08 bool eq_HC08_alu.
283 #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12;
285 #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12;
287 ((eqc ? x1 y1) ⊗ (eqc ? x2 y2) ⊗ (eqc ? x3 y3) ⊗ (eqc ? x4 y4) ⊗
288 (eqc ? x5 y5) ⊗ (eqc ? x6 y6) ⊗ (eqc ? x7 y7) ⊗ (eqc ? x8 y8) ⊗
289 (eqc ? x9 y9) ⊗ (eqc ? x10 y10) ⊗ (eqc ? x11 y11) ⊗ (eqc ? x12 y12)) =
290 ((eqc ? y1 x1) ⊗ (eqc ? y2 x2) ⊗ (eqc ? y3 x3) ⊗ (eqc ? y4 x4) ⊗
291 (eqc ? y5 x5) ⊗ (eqc ? y6 x6) ⊗ (eqc ? y7 x7) ⊗ (eqc ? y8 x8) ⊗
292 (eqc ? y9 x9) ⊗ (eqc ? y10 x10) ⊗ (eqc ? y11 x11) ⊗ (eqc ? y12 x12)));
293 nrewrite > (symmetric_eqc ? x1 y1);
294 nrewrite > (symmetric_eqc ? x2 y2);
295 nrewrite > (symmetric_eqc ? x3 y3);
296 nrewrite > (symmetric_eqc ? x4 y4);
297 nrewrite > (symmetric_eqc ? x5 y5);
298 nrewrite > (symmetric_eqc ? x6 y6);
299 nrewrite > (symmetric_eqc ? x7 y7);
300 nrewrite > (symmetric_eqc ? x8 y8);
301 nrewrite > (symmetric_eqc ? x9 y9);
302 nrewrite > (symmetric_eqc ? x10 y10);
303 nrewrite > (symmetric_eqc ? x11 y11);
304 nrewrite > (symmetric_eqc ? x12 y12);
308 nlemma aluHC08_is_comparable : comparable.
310 ##[ napply (mk_alu_HC08 (zeroc ?) (zeroc ?) (zeroc ?) (zeroc ?)
311 (zeroc ?) (zeroc ?) (zeroc ?) (zeroc ?)
312 (zeroc ?) (zeroc ?) (zeroc ?) (zeroc ?))
313 ##| napply forall_HC08_alu
314 ##| napply eq_HC08_alu
315 ##| napply eqaluHC08_to_eq
316 ##| napply eq_to_eqaluHC08
317 ##| napply neqaluHC08_to_neq
318 ##| napply neq_to_neqaluHC08
319 ##| napply decidable_aluHC08
320 ##| napply symmetric_eqaluHC08
324 unification hint 0 ≔ ⊢ carr aluHC08_is_comparable ≡ alu_HC08.