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/RS08_status_base.ma".
25 (* *********************************** *)
26 (* STATUS INTERNO DEL PROCESSORE (ALU) *)
27 (* *********************************** *)
29 nlemma aluRS08_destruct_1 :
30 ∀x1,x2,x3,x4,x5,x6,x7,x8,y1,y2,y3,y4,y5,y6,y7,y8.
31 mk_alu_RS08 x1 x2 x3 x4 x5 x6 x7 x8 = mk_alu_RS08 y1 y2 y3 y4 y5 y6 y7 y8 →
33 #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8;
34 #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #H;
35 nchange with (match mk_alu_RS08 y1 y2 y3 y4 y5 y6 y7 y8
36 with [ mk_alu_RS08 a _ _ _ _ _ _ _ ⇒ x1 = a ]);
42 nlemma aluRS08_destruct_2 :
43 ∀x1,x2,x3,x4,x5,x6,x7,x8,y1,y2,y3,y4,y5,y6,y7,y8.
44 mk_alu_RS08 x1 x2 x3 x4 x5 x6 x7 x8 = mk_alu_RS08 y1 y2 y3 y4 y5 y6 y7 y8 →
46 #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8;
47 #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #H;
48 nchange with (match mk_alu_RS08 y1 y2 y3 y4 y5 y6 y7 y8
49 with [ mk_alu_RS08 _ a _ _ _ _ _ _ ⇒ x2 = a ]);
55 nlemma aluRS08_destruct_3 :
56 ∀x1,x2,x3,x4,x5,x6,x7,x8,y1,y2,y3,y4,y5,y6,y7,y8.
57 mk_alu_RS08 x1 x2 x3 x4 x5 x6 x7 x8 = mk_alu_RS08 y1 y2 y3 y4 y5 y6 y7 y8 →
59 #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8;
60 #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #H;
61 nchange with (match mk_alu_RS08 y1 y2 y3 y4 y5 y6 y7 y8
62 with [ mk_alu_RS08 _ _ a _ _ _ _ _ ⇒ x3 = a ]);
68 nlemma aluRS08_destruct_4 :
69 ∀x1,x2,x3,x4,x5,x6,x7,x8,y1,y2,y3,y4,y5,y6,y7,y8.
70 mk_alu_RS08 x1 x2 x3 x4 x5 x6 x7 x8 = mk_alu_RS08 y1 y2 y3 y4 y5 y6 y7 y8 →
72 #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8;
73 #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #H;
74 nchange with (match mk_alu_RS08 y1 y2 y3 y4 y5 y6 y7 y8
75 with [ mk_alu_RS08 _ _ _ a _ _ _ _ ⇒ x4 = a ]);
81 nlemma aluRS08_destruct_5 :
82 ∀x1,x2,x3,x4,x5,x6,x7,x8,y1,y2,y3,y4,y5,y6,y7,y8.
83 mk_alu_RS08 x1 x2 x3 x4 x5 x6 x7 x8 = mk_alu_RS08 y1 y2 y3 y4 y5 y6 y7 y8 →
85 #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8;
86 #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #H;
87 nchange with (match mk_alu_RS08 y1 y2 y3 y4 y5 y6 y7 y8
88 with [ mk_alu_RS08 _ _ _ _ a _ _ _ ⇒ x5 = a ]);
94 nlemma aluRS08_destruct_6 :
95 ∀x1,x2,x3,x4,x5,x6,x7,x8,y1,y2,y3,y4,y5,y6,y7,y8.
96 mk_alu_RS08 x1 x2 x3 x4 x5 x6 x7 x8 = mk_alu_RS08 y1 y2 y3 y4 y5 y6 y7 y8 →
98 #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8;
99 #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #H;
100 nchange with (match mk_alu_RS08 y1 y2 y3 y4 y5 y6 y7 y8
101 with [ mk_alu_RS08 _ _ _ _ _ a _ _ ⇒ x6 = a ]);
107 nlemma aluRS08_destruct_7 :
108 ∀x1,x2,x3,x4,x5,x6,x7,x8,y1,y2,y3,y4,y5,y6,y7,y8.
109 mk_alu_RS08 x1 x2 x3 x4 x5 x6 x7 x8 = mk_alu_RS08 y1 y2 y3 y4 y5 y6 y7 y8 →
111 #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8;
112 #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #H;
113 nchange with (match mk_alu_RS08 y1 y2 y3 y4 y5 y6 y7 y8
114 with [ mk_alu_RS08 _ _ _ _ _ _ a _ ⇒ x7 = a ]);
120 nlemma aluRS08_destruct_8 :
121 ∀x1,x2,x3,x4,x5,x6,x7,x8,y1,y2,y3,y4,y5,y6,y7,y8.
122 mk_alu_RS08 x1 x2 x3 x4 x5 x6 x7 x8 = mk_alu_RS08 y1 y2 y3 y4 y5 y6 y7 y8 →
124 #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8;
125 #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #H;
126 nchange with (match mk_alu_RS08 y1 y2 y3 y4 y5 y6 y7 y8
127 with [ mk_alu_RS08 _ _ _ _ _ _ _ a ⇒ x8 = a ]);
133 nlemma eq_to_eqaluRS08 : ∀alu1,alu2.alu1 = alu2 → eq_RS08_alu alu1 alu2 = true.
136 #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8;
138 #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #H;
139 nrewrite > (aluRS08_destruct_1 … H);
140 nrewrite > (aluRS08_destruct_2 … H);
141 nrewrite > (aluRS08_destruct_3 … H);
142 nrewrite > (aluRS08_destruct_4 … H);
143 nrewrite > (aluRS08_destruct_5 … H);
144 nrewrite > (aluRS08_destruct_6 … H);
145 nrewrite > (aluRS08_destruct_7 … H);
146 nrewrite > (aluRS08_destruct_8 … H);
148 ((eqc ? y1 y1) ⊗ (eqc ? y2 y2) ⊗
149 (eqc ? y3 y3) ⊗ (eqc ? y4 y4) ⊗
150 (eqc ? y5 y5) ⊗ (eqc ? y6 y6) ⊗
151 (eqc ? y7 y7) ⊗ (eqc ? y8 y8)) = true);
152 nrewrite > (eq_to_eqc ? y1 y1 (refl_eq …));
153 nrewrite > (eq_to_eqc ? y2 y2 (refl_eq …));
154 nrewrite > (eq_to_eqc ? y3 y3 (refl_eq …));
155 nrewrite > (eq_to_eqc ? y4 y4 (refl_eq …));
156 nrewrite > (eq_to_eqc ? y5 y5 (refl_eq …));
157 nrewrite > (eq_to_eqc ? y6 y6 (refl_eq …));
158 nrewrite > (eq_to_eqc ? y7 y7 (refl_eq …));
159 nrewrite > (eq_to_eqc ? y8 y8 (refl_eq …));
163 nlemma neqaluRS08_to_neq : ∀alu1,alu2.eq_RS08_alu alu1 alu2 = false → alu1 ≠ alu2.
165 napply (not_to_not (s1 = s2) (eq_RS08_alu s1 s2 = true) …);
166 ##[ ##1: napply (eq_to_eqaluRS08 s1 s2)
167 ##| ##2: napply (eqfalse_to_neqtrue … H)
171 nlemma eqaluRS08_to_eq : ∀alu1,alu2.eq_RS08_alu alu1 alu2 = true → alu1 = alu2.
174 #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8;
176 #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #H;
177 nchange in H:(%) with (
178 ((eqc ? x1 y1) ⊗ (eqc ? x2 y2) ⊗
179 (eqc ? x3 y3) ⊗ (eqc ? x4 y4) ⊗
180 (eqc ? x5 y5) ⊗ (eqc ? x6 y6) ⊗
181 (eqc ? x7 y7) ⊗ (eqc ? x8 y8)) = true);
182 nrewrite > (eqc_to_eq … (andb_true_true_r … H));
183 nletin H1 ≝ (andb_true_true_l … H);
184 nrewrite > (eqc_to_eq … (andb_true_true_r … H1));
185 nletin H2 ≝ (andb_true_true_l … H1);
186 nrewrite > (eqc_to_eq … (andb_true_true_r … H2));
187 nletin H3 ≝ (andb_true_true_l … H2);
188 nrewrite > (eqc_to_eq … (andb_true_true_r … H3));
189 nletin H4 ≝ (andb_true_true_l … H3);
190 nrewrite > (eqc_to_eq … (andb_true_true_r … H4));
191 nletin H5 ≝ (andb_true_true_l … H4);
192 nrewrite > (eqc_to_eq … (andb_true_true_r … H5));
193 nletin H6 ≝ (andb_true_true_l … H5);
194 nrewrite > (eqc_to_eq … (andb_true_true_r … H6));
195 nrewrite > (eqc_to_eq … (andb_true_true_l … H6));
199 nlemma neq_to_neqaluRS08 : ∀alu1,alu2.alu1 ≠ alu2 → eq_RS08_alu alu1 alu2 = false.
201 napply (neqtrue_to_eqfalse (eq_RS08_alu s1 s2));
202 napply (not_to_not (eq_RS08_alu s1 s2 = true) (s1 = s2) ? H);
203 napply (eqaluRS08_to_eq s1 s2).
206 nlemma decidable_aluRS08 : ∀x,y:alu_RS08.decidable (x = y).
208 napply (or2_elim (eq_RS08_alu x y = true) (eq_RS08_alu x y = false) ? (decidable_bexpr ?));
209 ##[ ##1: #H; napply (or2_intro1 (x = y) (x ≠ y) (eqaluRS08_to_eq … H))
210 ##| ##2: #H; napply (or2_intro2 (x = y) (x ≠ y) (neqaluRS08_to_neq … H))
215 nlemma symmetric_eqaluRS08 : symmetricT alu_RS08 bool eq_RS08_alu.
218 #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8;
220 #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8;
222 ((eqc ? x1 y1) ⊗ (eqc ? x2 y2) ⊗
223 (eqc ? x3 y3) ⊗ (eqc ? x4 y4) ⊗
224 (eqc ? x5 y5) ⊗ (eqc ? x6 y6) ⊗
225 (eqc ? x7 y7) ⊗ (eqc ? x8 y8)) =
226 ((eqc ? y1 x1) ⊗ (eqc ? y2 x2) ⊗
227 (eqc ? y3 x3) ⊗ (eqc ? y4 x4) ⊗
228 (eqc ? y5 x5) ⊗ (eqc ? y6 x6) ⊗
229 (eqc ? y7 x7) ⊗ (eqc ? y8 x8)));
230 nrewrite > (symmetric_eqc ? x1 y1);
231 nrewrite > (symmetric_eqc ? x2 y2);
232 nrewrite > (symmetric_eqc ? x3 y3);
233 nrewrite > (symmetric_eqc ? x4 y4);
234 nrewrite > (symmetric_eqc ? x5 y5);
235 nrewrite > (symmetric_eqc ? x6 y6);
236 nrewrite > (symmetric_eqc ? x7 y7);
237 nrewrite > (symmetric_eqc ? x8 y8);
241 nlemma aluRS08_is_comparable : comparable.
243 ##[ napply (mk_alu_RS08 (zeroc ?) (zeroc ?) (zeroc ?) (zeroc ?)
244 (zeroc ?) (zeroc ?) (zeroc ?) (zeroc ?))
245 ##| napply forall_RS08_alu
246 ##| napply eq_RS08_alu
247 ##| napply eqaluRS08_to_eq
248 ##| napply eq_to_eqaluRS08
249 ##| napply neqaluRS08_to_neq
250 ##| napply neq_to_neqaluRS08
251 ##| napply decidable_aluRS08
252 ##| napply symmetric_eqaluRS08
256 unification hint 0 ≔ ⊢ carr aluRS08_is_comparable ≡ alu_RS08.