|
1 (* Author: Florian Haftmann, TUM |
|
2 *) |
|
3 |
|
4 section \<open>Proof of concept for algebraically founded bit word types\<close> |
|
5 |
|
6 theory Word_Type |
|
7 imports |
|
8 Main |
|
9 "~~/src/HOL/Library/Type_Length" |
|
10 begin |
|
11 |
|
12 subsection \<open>Compact syntax for types with a length\<close> |
|
13 |
|
14 syntax "_type_length" :: "type \<Rightarrow> nat" ("(1LENGTH/(1'(_')))") |
|
15 |
|
16 translations "LENGTH('a)" \<rightharpoonup> |
|
17 "CONST len_of (CONST Pure.type :: 'a itself)" |
|
18 |
|
19 print_translation \<open> |
|
20 let |
|
21 fun len_of_itself_tr' ctxt [Const (@{const_syntax Pure.type}, Type (_, [T]))] = |
|
22 Syntax.const @{syntax_const "_type_length"} $ Syntax_Phases.term_of_typ ctxt T |
|
23 in [(@{const_syntax len_of}, len_of_itself_tr')] end |
|
24 \<close> |
|
25 |
|
26 |
|
27 subsection \<open>Truncating bit representations of numeric types\<close> |
|
28 |
|
29 class semiring_bits = semiring_div_parity + |
|
30 assumes semiring_bits: "(1 + 2 * a) mod of_nat (2 * n) = 1 + 2 * (a mod of_nat n)" |
|
31 |
|
32 context semiring_bits |
|
33 begin |
|
34 |
|
35 definition bits :: "nat \<Rightarrow> 'a \<Rightarrow> 'a" |
|
36 where bits_eq_mod: "bits n a = a mod of_nat (2 ^ n)" |
|
37 |
|
38 lemma bits_bits [simp]: |
|
39 "bits n (bits n a) = bits n a" |
|
40 by (simp add: bits_eq_mod) |
|
41 |
|
42 lemma bits_0 [simp]: |
|
43 "bits 0 a = 0" |
|
44 by (simp add: bits_eq_mod) |
|
45 |
|
46 lemma bits_Suc [simp]: |
|
47 "bits (Suc n) a = bits n (a div 2) * 2 + a mod 2" |
|
48 proof - |
|
49 define b and c |
|
50 where "b = a div 2" and "c = a mod 2" |
|
51 then have a: "a = b * 2 + c" |
|
52 and "c = 0 \<or> c = 1" |
|
53 by (simp_all add: mod_div_equality parity) |
|
54 from \<open>c = 0 \<or> c = 1\<close> |
|
55 have "bits (Suc n) (b * 2 + c) = bits n b * 2 + c" |
|
56 proof |
|
57 assume "c = 0" |
|
58 moreover have "(2 * b) mod (2 * 2 ^ n) = 2 * (b mod 2 ^ n)" |
|
59 by (simp add: mod_mult_mult1) |
|
60 ultimately show ?thesis |
|
61 by (simp add: bits_eq_mod ac_simps) |
|
62 next |
|
63 assume "c = 1" |
|
64 with semiring_bits [of b "2 ^ n"] show ?thesis |
|
65 by (simp add: bits_eq_mod ac_simps) |
|
66 qed |
|
67 with a show ?thesis |
|
68 by (simp add: b_def c_def) |
|
69 qed |
|
70 |
|
71 lemma bits_of_0 [simp]: |
|
72 "bits n 0 = 0" |
|
73 by (simp add: bits_eq_mod) |
|
74 |
|
75 lemma bits_plus: |
|
76 "bits n (bits n a + bits n b) = bits n (a + b)" |
|
77 by (simp add: bits_eq_mod mod_add_eq [symmetric]) |
|
78 |
|
79 lemma bits_of_1_eq_0_iff [simp]: |
|
80 "bits n 1 = 0 \<longleftrightarrow> n = 0" |
|
81 by (induct n) simp_all |
|
82 |
|
83 end |
|
84 |
|
85 instance nat :: semiring_bits |
|
86 by standard (simp add: mod_Suc Suc_double_not_eq_double) |
|
87 |
|
88 instance int :: semiring_bits |
|
89 by standard (simp add: pos_zmod_mult_2) |
|
90 |
|
91 lemma bits_uminus: |
|
92 fixes k :: int |
|
93 shows "bits n (- (bits n k)) = bits n (- k)" |
|
94 by (simp add: bits_eq_mod mod_minus_eq [symmetric]) |
|
95 |
|
96 lemma bits_minus: |
|
97 fixes k l :: int |
|
98 shows "bits n (bits n k - bits n l) = bits n (k - l)" |
|
99 by (simp add: bits_eq_mod mod_diff_eq [symmetric]) |
|
100 |
|
101 lemma bits_nonnegative [simp]: |
|
102 fixes k :: int |
|
103 shows "bits n k \<ge> 0" |
|
104 by (simp add: bits_eq_mod) |
|
105 |
|
106 definition signed_bits :: "nat \<Rightarrow> int \<Rightarrow> int" |
|
107 where signed_bits_eq_bits: |
|
108 "signed_bits n k = bits (Suc n) (k + 2 ^ n) - 2 ^ n" |
|
109 |
|
110 lemma signed_bits_eq_bits': |
|
111 assumes "n > 0" |
|
112 shows "signed_bits (n - Suc 0) k = bits n (k + 2 ^ (n - 1)) - 2 ^ (n - 1)" |
|
113 using assms by (simp add: signed_bits_eq_bits) |
|
114 |
|
115 lemma signed_bits_0 [simp]: |
|
116 "signed_bits 0 k = - (k mod 2)" |
|
117 proof (cases "even k") |
|
118 case True |
|
119 then have "odd (k + 1)" |
|
120 by simp |
|
121 then have "(k + 1) mod 2 = 1" |
|
122 by (simp add: even_iff_mod_2_eq_zero) |
|
123 with True show ?thesis |
|
124 by (simp add: signed_bits_eq_bits) |
|
125 next |
|
126 case False |
|
127 then show ?thesis |
|
128 by (simp add: signed_bits_eq_bits odd_iff_mod_2_eq_one) |
|
129 qed |
|
130 |
|
131 lemma signed_bits_Suc [simp]: |
|
132 "signed_bits (Suc n) k = signed_bits n (k div 2) * 2 + k mod 2" |
|
133 using zero_not_eq_two by (simp add: signed_bits_eq_bits algebra_simps) |
|
134 |
|
135 lemma signed_bits_of_0 [simp]: |
|
136 "signed_bits n 0 = 0" |
|
137 by (simp add: signed_bits_eq_bits bits_eq_mod) |
|
138 |
|
139 lemma signed_bits_of_minus_1 [simp]: |
|
140 "signed_bits n (- 1) = - 1" |
|
141 by (induct n) simp_all |
|
142 |
|
143 lemma signed_bits_eq_iff_bits_eq: |
|
144 assumes "n > 0" |
|
145 shows "signed_bits (n - Suc 0) k = signed_bits (n - Suc 0) l \<longleftrightarrow> bits n k = bits n l" (is "?P \<longleftrightarrow> ?Q") |
|
146 proof - |
|
147 from assms obtain m where m: "n = Suc m" |
|
148 by (cases n) auto |
|
149 show ?thesis |
|
150 proof |
|
151 assume ?Q |
|
152 have "bits (Suc m) (k + 2 ^ m) = |
|
153 bits (Suc m) (bits (Suc m) k + bits (Suc m) (2 ^ m))" |
|
154 by (simp only: bits_plus) |
|
155 also have "\<dots> = |
|
156 bits (Suc m) (bits (Suc m) l + bits (Suc m) (2 ^ m))" |
|
157 by (simp only: \<open>?Q\<close> m [symmetric]) |
|
158 also have "\<dots> = bits (Suc m) (l + 2 ^ m)" |
|
159 by (simp only: bits_plus) |
|
160 finally show ?P |
|
161 by (simp only: signed_bits_eq_bits m) simp |
|
162 next |
|
163 assume ?P |
|
164 with assms have "(k + 2 ^ (n - Suc 0)) mod 2 ^ n = (l + 2 ^ (n - Suc 0)) mod 2 ^ n" |
|
165 by (simp add: signed_bits_eq_bits' bits_eq_mod) |
|
166 then have "(i + (k + 2 ^ (n - Suc 0))) mod 2 ^ n = (i + (l + 2 ^ (n - Suc 0))) mod 2 ^ n" for i |
|
167 by (metis mod_add_eq) |
|
168 then have "k mod 2 ^ n = l mod 2 ^ n" |
|
169 by (metis add_diff_cancel_right' uminus_add_conv_diff) |
|
170 then show ?Q |
|
171 by (simp add: bits_eq_mod) |
|
172 qed |
|
173 qed |
|
174 |
|
175 |
|
176 subsection \<open>Bit strings as quotient type\<close> |
|
177 |
|
178 subsubsection \<open>Basic properties\<close> |
|
179 |
|
180 quotient_type (overloaded) 'a word = int / "\<lambda>k l. bits LENGTH('a) k = bits LENGTH('a::len0) l" |
|
181 by (auto intro!: equivpI reflpI sympI transpI) |
|
182 |
|
183 instantiation word :: (len0) "{semiring_numeral, comm_semiring_0, comm_ring}" |
|
184 begin |
|
185 |
|
186 lift_definition zero_word :: "'a word" |
|
187 is 0 |
|
188 . |
|
189 |
|
190 lift_definition one_word :: "'a word" |
|
191 is 1 |
|
192 . |
|
193 |
|
194 lift_definition plus_word :: "'a word \<Rightarrow> 'a word \<Rightarrow> 'a word" |
|
195 is plus |
|
196 by (subst bits_plus [symmetric]) (simp add: bits_plus) |
|
197 |
|
198 lift_definition uminus_word :: "'a word \<Rightarrow> 'a word" |
|
199 is uminus |
|
200 by (subst bits_uminus [symmetric]) (simp add: bits_uminus) |
|
201 |
|
202 lift_definition minus_word :: "'a word \<Rightarrow> 'a word \<Rightarrow> 'a word" |
|
203 is minus |
|
204 by (subst bits_minus [symmetric]) (simp add: bits_minus) |
|
205 |
|
206 lift_definition times_word :: "'a word \<Rightarrow> 'a word \<Rightarrow> 'a word" |
|
207 is times |
|
208 by (auto simp add: bits_eq_mod intro: mod_mult_cong) |
|
209 |
|
210 instance |
|
211 by standard (transfer; simp add: algebra_simps)+ |
|
212 |
|
213 end |
|
214 |
|
215 instance word :: (len) comm_ring_1 |
|
216 by standard (transfer; simp)+ |
|
217 |
|
218 |
|
219 subsubsection \<open>Conversions\<close> |
|
220 |
|
221 lemma [transfer_rule]: |
|
222 "rel_fun HOL.eq pcr_word int of_nat" |
|
223 proof - |
|
224 note transfer_rule_of_nat [transfer_rule] |
|
225 show ?thesis by transfer_prover |
|
226 qed |
|
227 |
|
228 lemma [transfer_rule]: |
|
229 "rel_fun HOL.eq pcr_word (\<lambda>k. k) of_int" |
|
230 proof - |
|
231 note transfer_rule_of_int [transfer_rule] |
|
232 have "rel_fun HOL.eq pcr_word (of_int :: int \<Rightarrow> int) (of_int :: int \<Rightarrow> 'a word)" |
|
233 by transfer_prover |
|
234 then show ?thesis by (simp add: id_def) |
|
235 qed |
|
236 |
|
237 context semiring_1 |
|
238 begin |
|
239 |
|
240 lift_definition unsigned :: "'b::len0 word \<Rightarrow> 'a" |
|
241 is "of_nat \<circ> nat \<circ> bits LENGTH('b)" |
|
242 by simp |
|
243 |
|
244 lemma unsigned_0 [simp]: |
|
245 "unsigned 0 = 0" |
|
246 by transfer simp |
|
247 |
|
248 end |
|
249 |
|
250 context semiring_char_0 |
|
251 begin |
|
252 |
|
253 lemma word_eq_iff_unsigned: |
|
254 "a = b \<longleftrightarrow> unsigned a = unsigned b" |
|
255 by safe (transfer; simp add: eq_nat_nat_iff) |
|
256 |
|
257 end |
|
258 |
|
259 context ring_1 |
|
260 begin |
|
261 |
|
262 lift_definition signed :: "'b::len word \<Rightarrow> 'a" |
|
263 is "of_int \<circ> signed_bits (LENGTH('b) - 1)" |
|
264 by (simp add: signed_bits_eq_iff_bits_eq [symmetric]) |
|
265 |
|
266 lemma signed_0 [simp]: |
|
267 "signed 0 = 0" |
|
268 by transfer simp |
|
269 |
|
270 end |
|
271 |
|
272 lemma unsigned_of_nat [simp]: |
|
273 "unsigned (of_nat n :: 'a word) = bits LENGTH('a::len) n" |
|
274 by transfer (simp add: nat_eq_iff bits_eq_mod zmod_int) |
|
275 |
|
276 lemma of_nat_unsigned [simp]: |
|
277 "of_nat (unsigned a) = a" |
|
278 by transfer simp |
|
279 |
|
280 lemma of_int_unsigned [simp]: |
|
281 "of_int (unsigned a) = a" |
|
282 by transfer simp |
|
283 |
|
284 context ring_char_0 |
|
285 begin |
|
286 |
|
287 lemma word_eq_iff_signed: |
|
288 "a = b \<longleftrightarrow> signed a = signed b" |
|
289 by safe (transfer; auto simp add: signed_bits_eq_iff_bits_eq) |
|
290 |
|
291 end |
|
292 |
|
293 lemma signed_of_int [simp]: |
|
294 "signed (of_int k :: 'a word) = signed_bits (LENGTH('a::len) - 1) k" |
|
295 by transfer simp |
|
296 |
|
297 lemma of_int_signed [simp]: |
|
298 "of_int (signed a) = a" |
|
299 by transfer (simp add: signed_bits_eq_bits bits_eq_mod zdiff_zmod_left) |
|
300 |
|
301 |
|
302 subsubsection \<open>Properties\<close> |
|
303 |
|
304 |
|
305 subsubsection \<open>Division\<close> |
|
306 |
|
307 instantiation word :: (len0) modulo |
|
308 begin |
|
309 |
|
310 lift_definition divide_word :: "'a word \<Rightarrow> 'a word \<Rightarrow> 'a word" |
|
311 is "\<lambda>a b. bits LENGTH('a) a div bits LENGTH('a) b" |
|
312 by simp |
|
313 |
|
314 lift_definition modulo_word :: "'a word \<Rightarrow> 'a word \<Rightarrow> 'a word" |
|
315 is "\<lambda>a b. bits LENGTH('a) a mod bits LENGTH('a) b" |
|
316 by simp |
|
317 |
|
318 instance .. |
|
319 |
|
320 end |
|
321 |
|
322 |
|
323 subsubsection \<open>Orderings\<close> |
|
324 |
|
325 instantiation word :: (len0) linorder |
|
326 begin |
|
327 |
|
328 lift_definition less_eq_word :: "'a word \<Rightarrow> 'a word \<Rightarrow> bool" |
|
329 is "\<lambda>a b. bits LENGTH('a) a \<le> bits LENGTH('a) b" |
|
330 by simp |
|
331 |
|
332 lift_definition less_word :: "'a word \<Rightarrow> 'a word \<Rightarrow> bool" |
|
333 is "\<lambda>a b. bits LENGTH('a) a < bits LENGTH('a) b" |
|
334 by simp |
|
335 |
|
336 instance |
|
337 by standard (transfer; auto)+ |
|
338 |
|
339 end |
|
340 |
|
341 context linordered_semidom |
|
342 begin |
|
343 |
|
344 lemma word_less_eq_iff_unsigned: |
|
345 "a \<le> b \<longleftrightarrow> unsigned a \<le> unsigned b" |
|
346 by (transfer fixing: less_eq) (simp add: nat_le_eq_zle) |
|
347 |
|
348 lemma word_less_iff_unsigned: |
|
349 "a < b \<longleftrightarrow> unsigned a < unsigned b" |
|
350 by (transfer fixing: less) (auto dest: preorder_class.le_less_trans [OF bits_nonnegative]) |
|
351 |
|
352 end |
|
353 |
|
354 end |