|
1 (* Title: HOL/Library/Word.thy |
|
2 ID: $Id$ |
|
3 Author: Sebastian Skalberg (TU Muenchen) |
|
4 *) |
|
5 |
|
6 theory Word = Main files "word_setup.ML": |
|
7 |
|
8 subsection {* Auxilary Lemmas *} |
|
9 |
|
10 text {* Amazing that these are necessary, but I can't find equivalent |
|
11 ones in the other HOL theories. *} |
|
12 |
|
13 lemma max_le [intro!]: "[| x \<le> z; y \<le> z |] ==> max x y \<le> z" |
|
14 by (simp add: max_def) |
|
15 |
|
16 lemma max_mono: |
|
17 assumes mf: "mono f" |
|
18 shows "max (f (x::'a::linorder)) (f y) \<le> f (max x y)" |
|
19 proof - |
|
20 from mf and le_maxI1 [of x y] |
|
21 have fx: "f x \<le> f (max x y)" |
|
22 by (rule monoD) |
|
23 from mf and le_maxI2 [of y x] |
|
24 have fy: "f y \<le> f (max x y)" |
|
25 by (rule monoD) |
|
26 from fx and fy |
|
27 show "max (f x) (f y) \<le> f (max x y)" |
|
28 by auto |
|
29 qed |
|
30 |
|
31 lemma le_imp_power_le: |
|
32 assumes b0: "0 < (b::nat)" |
|
33 and xy: "x \<le> y" |
|
34 shows "b ^ x \<le> b ^ y" |
|
35 proof (rule ccontr) |
|
36 assume "~ b ^ x \<le> b ^ y" |
|
37 hence bybx: "b ^ y < b ^ x" |
|
38 by simp |
|
39 have "y < x" |
|
40 proof (rule nat_power_less_imp_less [OF _ bybx]) |
|
41 from b0 |
|
42 show "0 < b" |
|
43 . |
|
44 qed |
|
45 with xy |
|
46 show False |
|
47 by simp |
|
48 qed |
|
49 |
|
50 lemma less_imp_power_less: |
|
51 assumes b1: "1 < (b::nat)" |
|
52 and xy: "x < y" |
|
53 shows "b ^ x < b ^ y" |
|
54 proof (rule ccontr) |
|
55 assume "~ b ^ x < b ^ y" |
|
56 hence bybx: "b ^ y \<le> b ^ x" |
|
57 by simp |
|
58 have "y \<le> x" |
|
59 proof (rule power_le_imp_le_exp [OF _ bybx]) |
|
60 from b1 |
|
61 show "1 < b" |
|
62 . |
|
63 qed |
|
64 with xy |
|
65 show False |
|
66 by simp |
|
67 qed |
|
68 |
|
69 lemma [simp]: "1 < (b::nat) ==> (b ^ x \<le> b ^ y) = (x \<le> y)" |
|
70 apply rule |
|
71 apply (erule power_le_imp_le_exp) |
|
72 apply assumption |
|
73 apply (subgoal_tac "0 < b") |
|
74 apply (erule le_imp_power_le) |
|
75 apply assumption |
|
76 apply simp |
|
77 done |
|
78 |
|
79 lemma [simp]: "1 < (b::nat) ==> (b ^ x < b ^ y) = (x < y)" |
|
80 apply rule |
|
81 apply (subgoal_tac "0 < b") |
|
82 apply (erule nat_power_less_imp_less) |
|
83 apply assumption |
|
84 apply simp |
|
85 apply (erule less_imp_power_less) |
|
86 apply assumption |
|
87 done |
|
88 |
|
89 lemma power_le_imp_zle: |
|
90 assumes b1: "1 < (b::int)" |
|
91 and bxby: "b ^ x \<le> b ^ y" |
|
92 shows "x \<le> y" |
|
93 proof - |
|
94 from b1 |
|
95 have nb1: "1 < nat b" |
|
96 by arith |
|
97 from b1 |
|
98 have nb0: "0 \<le> b" |
|
99 by simp |
|
100 from bxby |
|
101 have "nat (b ^ x) \<le> nat (b ^ y)" |
|
102 by arith |
|
103 hence "nat b ^ x \<le> nat b ^ y" |
|
104 by (simp add: nat_power_eq [OF nb0]) |
|
105 with power_le_imp_le_exp and nb1 |
|
106 show "x \<le> y" |
|
107 by auto |
|
108 qed |
|
109 |
|
110 lemma zero_le_zpower [intro]: |
|
111 assumes b0: "0 \<le> (b::int)" |
|
112 shows "0 \<le> b ^ n" |
|
113 proof (induct n,simp) |
|
114 fix n |
|
115 assume ind: "0 \<le> b ^ n" |
|
116 have "b * 0 \<le> b * b ^ n" |
|
117 proof (subst mult_le_cancel_left,auto intro!: ind) |
|
118 assume "b < 0" |
|
119 with b0 |
|
120 show "b ^ n \<le> 0" |
|
121 by simp |
|
122 qed |
|
123 thus "0 \<le> b ^ Suc n" |
|
124 by simp |
|
125 qed |
|
126 |
|
127 lemma zero_less_zpower [intro]: |
|
128 assumes b0: "0 < (b::int)" |
|
129 shows "0 < b ^ n" |
|
130 proof - |
|
131 from b0 |
|
132 have b0': "0 \<le> b" |
|
133 by simp |
|
134 from b0 |
|
135 have "0 < nat b" |
|
136 by simp |
|
137 hence "0 < nat b ^ n" |
|
138 by (rule zero_less_power) |
|
139 hence xx: "nat 0 < nat (b ^ n)" |
|
140 by (subst nat_power_eq [OF b0'],simp) |
|
141 show "0 < b ^ n" |
|
142 apply (subst nat_less_eq_zless [symmetric]) |
|
143 apply simp |
|
144 apply (rule xx) |
|
145 done |
|
146 qed |
|
147 |
|
148 lemma power_less_imp_zless: |
|
149 assumes b0: "0 < (b::int)" |
|
150 and bxby: "b ^ x < b ^ y" |
|
151 shows "x < y" |
|
152 proof - |
|
153 from b0 |
|
154 have nb0: "0 < nat b" |
|
155 by arith |
|
156 from b0 |
|
157 have b0': "0 \<le> b" |
|
158 by simp |
|
159 have "nat (b ^ x) < nat (b ^ y)" |
|
160 proof (subst nat_less_eq_zless) |
|
161 show "0 \<le> b ^ x" |
|
162 by (rule zero_le_zpower [OF b0']) |
|
163 next |
|
164 show "b ^ x < b ^ y" |
|
165 by (rule bxby) |
|
166 qed |
|
167 hence "nat b ^ x < nat b ^ y" |
|
168 by (simp add: nat_power_eq [OF b0']) |
|
169 with nat_power_less_imp_less [OF nb0] |
|
170 show "x < y" |
|
171 . |
|
172 qed |
|
173 |
|
174 lemma le_imp_power_zle: |
|
175 assumes b0: "0 < (b::int)" |
|
176 and xy: "x \<le> y" |
|
177 shows "b ^ x \<le> b ^ y" |
|
178 proof (rule ccontr) |
|
179 assume "~ b ^ x \<le> b ^ y" |
|
180 hence bybx: "b ^ y < b ^ x" |
|
181 by simp |
|
182 have "y < x" |
|
183 proof (rule power_less_imp_zless [OF _ bybx]) |
|
184 from b0 |
|
185 show "0 < b" |
|
186 . |
|
187 qed |
|
188 with xy |
|
189 show False |
|
190 by simp |
|
191 qed |
|
192 |
|
193 lemma less_imp_power_zless: |
|
194 assumes b1: "1 < (b::int)" |
|
195 and xy: "x < y" |
|
196 shows "b ^ x < b ^ y" |
|
197 proof (rule ccontr) |
|
198 assume "~ b ^ x < b ^ y" |
|
199 hence bybx: "b ^ y \<le> b ^ x" |
|
200 by simp |
|
201 have "y \<le> x" |
|
202 proof (rule power_le_imp_zle [OF _ bybx]) |
|
203 from b1 |
|
204 show "1 < b" |
|
205 . |
|
206 qed |
|
207 with xy |
|
208 show False |
|
209 by simp |
|
210 qed |
|
211 |
|
212 lemma [simp]: "1 < (b::int) ==> (b ^ x \<le> b ^ y) = (x \<le> y)" |
|
213 apply rule |
|
214 apply (erule power_le_imp_zle) |
|
215 apply assumption |
|
216 apply (subgoal_tac "0 < b") |
|
217 apply (erule le_imp_power_zle) |
|
218 apply assumption |
|
219 apply simp |
|
220 done |
|
221 |
|
222 lemma [simp]: "1 < (b::int) ==> (b ^ x < b ^ y) = (x < y)" |
|
223 apply rule |
|
224 apply (subgoal_tac "0 < b") |
|
225 apply (erule power_less_imp_zless) |
|
226 apply assumption |
|
227 apply simp |
|
228 apply (erule less_imp_power_zless) |
|
229 apply assumption |
|
230 done |
|
231 |
|
232 lemma suc_zero_le: "[| 0 < x ; 0 < y |] ==> Suc 0 < x + y" |
|
233 by simp |
|
234 |
|
235 lemma int_nat_two_exp: "2 ^ k = int (2 ^ k)" |
|
236 by (induct k,simp_all) |
|
237 |
|
238 section {* Bits *} |
|
239 |
|
240 datatype bit |
|
241 = Zero ("\<zero>") |
|
242 | One ("\<one>") |
|
243 |
|
244 consts |
|
245 bitval :: "bit => int" |
|
246 |
|
247 primrec |
|
248 "bitval \<zero> = 0" |
|
249 "bitval \<one> = 1" |
|
250 |
|
251 consts |
|
252 bitnot :: "bit => bit" |
|
253 bitand :: "bit => bit => bit" (infixr "bitand" 35) |
|
254 bitor :: "bit => bit => bit" (infixr "bitor" 30) |
|
255 bitxor :: "bit => bit => bit" (infixr "bitxor" 30) |
|
256 |
|
257 syntax (xsymbols) |
|
258 bitnot :: "bit => bit" ("\<not>\<^sub>b _" [40] 40) |
|
259 bitand :: "bit => bit => bit" (infixr "\<and>\<^sub>b" 35) |
|
260 bitor :: "bit => bit => bit" (infixr "\<or>\<^sub>b" 30) |
|
261 bitxor :: "bit => bit => bit" (infixr "\<oplus>\<^sub>b" 30) |
|
262 |
|
263 primrec |
|
264 bitnot_zero: "(bitnot \<zero>) = \<one>" |
|
265 bitnot_one : "(bitnot \<one>) = \<zero>" |
|
266 |
|
267 primrec |
|
268 bitand_zero: "(\<zero> bitand y) = \<zero>" |
|
269 bitand_one: "(\<one> bitand y) = y" |
|
270 |
|
271 primrec |
|
272 bitor_zero: "(\<zero> bitor y) = y" |
|
273 bitor_one: "(\<one> bitor y) = \<one>" |
|
274 |
|
275 primrec |
|
276 bitxor_zero: "(\<zero> bitxor y) = y" |
|
277 bitxor_one: "(\<one> bitxor y) = (bitnot y)" |
|
278 |
|
279 lemma [simp]: "(bitnot (bitnot b)) = b" |
|
280 by (cases b,simp_all) |
|
281 |
|
282 lemma [simp]: "(b bitand b) = b" |
|
283 by (cases b,simp_all) |
|
284 |
|
285 lemma [simp]: "(b bitor b) = b" |
|
286 by (cases b,simp_all) |
|
287 |
|
288 lemma [simp]: "(b bitxor b) = \<zero>" |
|
289 by (cases b,simp_all) |
|
290 |
|
291 section {* Bit Vectors *} |
|
292 |
|
293 text {* First, a couple of theorems expressing case analysis and |
|
294 induction principles for bit vectors. *} |
|
295 |
|
296 lemma bit_list_cases: |
|
297 assumes empty: "w = [] ==> P w" |
|
298 and zero: "!!bs. w = \<zero> # bs ==> P w" |
|
299 and one: "!!bs. w = \<one> # bs ==> P w" |
|
300 shows "P w" |
|
301 proof (cases w) |
|
302 assume "w = []" |
|
303 thus ?thesis |
|
304 by (rule empty) |
|
305 next |
|
306 fix b bs |
|
307 assume [simp]: "w = b # bs" |
|
308 show "P w" |
|
309 proof (cases b) |
|
310 assume "b = \<zero>" |
|
311 hence "w = \<zero> # bs" |
|
312 by simp |
|
313 thus ?thesis |
|
314 by (rule zero) |
|
315 next |
|
316 assume "b = \<one>" |
|
317 hence "w = \<one> # bs" |
|
318 by simp |
|
319 thus ?thesis |
|
320 by (rule one) |
|
321 qed |
|
322 qed |
|
323 |
|
324 lemma bit_list_induct: |
|
325 assumes empty: "P []" |
|
326 and zero: "!!bs. P bs ==> P (\<zero>#bs)" |
|
327 and one: "!!bs. P bs ==> P (\<one>#bs)" |
|
328 shows "P w" |
|
329 proof (induct w,simp_all add: empty) |
|
330 fix b bs |
|
331 assume [intro!]: "P bs" |
|
332 show "P (b#bs)" |
|
333 by (cases b,auto intro!: zero one) |
|
334 qed |
|
335 |
|
336 constdefs |
|
337 bv_msb :: "bit list => bit" |
|
338 "bv_msb w == if w = [] then \<zero> else hd w" |
|
339 bv_extend :: "[nat,bit,bit list]=>bit list" |
|
340 "bv_extend i b w == (replicate (i - length w) b) @ w" |
|
341 bv_not :: "bit list => bit list" |
|
342 "bv_not w == map bitnot w" |
|
343 |
|
344 lemma bv_length_extend [simp]: "length w \<le> i ==> length (bv_extend i b w) = i" |
|
345 by (simp add: bv_extend_def) |
|
346 |
|
347 lemma [simp]: "bv_not [] = []" |
|
348 by (simp add: bv_not_def) |
|
349 |
|
350 lemma [simp]: "bv_not (b#bs) = (bitnot b) # bv_not bs" |
|
351 by (simp add: bv_not_def) |
|
352 |
|
353 lemma [simp]: "bv_not (bv_not w) = w" |
|
354 by (rule bit_list_induct [of _ w],simp_all) |
|
355 |
|
356 lemma [simp]: "bv_msb [] = \<zero>" |
|
357 by (simp add: bv_msb_def) |
|
358 |
|
359 lemma [simp]: "bv_msb (b#bs) = b" |
|
360 by (simp add: bv_msb_def) |
|
361 |
|
362 lemma [simp]: "0 < length w ==> bv_msb (bv_not w) = (bitnot (bv_msb w))" |
|
363 by (cases w,simp_all) |
|
364 |
|
365 lemma [simp,intro]: "bv_msb w = \<one> ==> 0 < length w" |
|
366 by (cases w,simp_all) |
|
367 |
|
368 lemma [simp]: "length (bv_not w) = length w" |
|
369 by (induct w,simp_all) |
|
370 |
|
371 constdefs |
|
372 bv_to_nat :: "bit list => int" |
|
373 "bv_to_nat bv == number_of (foldl (%bn b. bn BIT (b = \<one>)) bin.Pls bv)" |
|
374 |
|
375 lemma [simp]: "bv_to_nat [] = 0" |
|
376 by (simp add: bv_to_nat_def) |
|
377 |
|
378 lemma pos_number_of: "(0::int)\<le> number_of w ==> number_of (w BIT b) = (2::int) * number_of w + (if b then 1 else 0)" |
|
379 by (induct w,auto,simp add: iszero_def) |
|
380 |
|
381 lemma bv_to_nat_helper [simp]: "bv_to_nat (b # bs) = bitval b * 2 ^ length bs + bv_to_nat bs" |
|
382 proof - |
|
383 def bv_to_nat' == "%base bv. number_of (foldl (% bn b. bn BIT (b = \<one>)) base bv)::int" |
|
384 have bv_to_nat'_def: "!!base bv. bv_to_nat' base bv == number_of (foldl (% bn b. bn BIT (b = \<one>)) base bv)::int" |
|
385 by (simp add: bv_to_nat'_def) |
|
386 have [rule_format]: "\<forall> base bs. (0::int) \<le> number_of base --> (\<forall> b. bv_to_nat' base (b # bs) = bv_to_nat' (base BIT (b = \<one>)) bs)" |
|
387 by (simp add: bv_to_nat'_def) |
|
388 have helper [rule_format]: "\<forall> base. (0::int) \<le> number_of base --> bv_to_nat' base bs = number_of base * 2 ^ length bs + bv_to_nat' bin.Pls bs" |
|
389 proof (induct bs,simp add: bv_to_nat'_def,clarify) |
|
390 fix x xs base |
|
391 assume ind [rule_format]: "\<forall> base. (0::int) \<le> number_of base --> bv_to_nat' base xs = number_of base * 2 ^ length xs + bv_to_nat' bin.Pls xs" |
|
392 assume base_pos: "(0::int) \<le> number_of base" |
|
393 def qq == "number_of base::int" |
|
394 show "bv_to_nat' base (x # xs) = number_of base * 2 ^ (length (x # xs)) + bv_to_nat' bin.Pls (x # xs)" |
|
395 apply (unfold bv_to_nat'_def) |
|
396 apply (simp only: foldl.simps) |
|
397 apply (fold bv_to_nat'_def) |
|
398 apply (subst ind [of "base BIT (x = \<one>)"]) |
|
399 using base_pos |
|
400 apply simp |
|
401 apply (subst ind [of "bin.Pls BIT (x = \<one>)"]) |
|
402 apply simp |
|
403 apply (subst pos_number_of [of "base" "x = \<one>"]) |
|
404 using base_pos |
|
405 apply simp |
|
406 apply (subst pos_number_of [of "bin.Pls" "x = \<one>"]) |
|
407 apply simp |
|
408 apply (fold qq_def) |
|
409 apply (simp add: ring_distrib) |
|
410 done |
|
411 qed |
|
412 show ?thesis |
|
413 apply (unfold bv_to_nat_def [of "b # bs"]) |
|
414 apply (simp only: foldl.simps) |
|
415 apply (fold bv_to_nat'_def) |
|
416 apply (subst helper) |
|
417 apply simp |
|
418 apply (cases "b::bit") |
|
419 apply (simp add: bv_to_nat'_def bv_to_nat_def) |
|
420 apply (simp add: iszero_def) |
|
421 apply (simp add: bv_to_nat'_def bv_to_nat_def) |
|
422 done |
|
423 qed |
|
424 |
|
425 lemma bv_to_nat0 [simp]: "bv_to_nat (\<zero>#bs) = bv_to_nat bs" |
|
426 by simp |
|
427 |
|
428 lemma bv_to_nat1 [simp]: "bv_to_nat (\<one>#bs) = 2 ^ length bs + bv_to_nat bs" |
|
429 by simp |
|
430 |
|
431 lemma bv_to_nat_lower_range [intro,simp]: "0 \<le> bv_to_nat w" |
|
432 apply (induct w,simp_all) |
|
433 apply (case_tac a,simp_all) |
|
434 apply (rule add_increasing) |
|
435 apply auto |
|
436 done |
|
437 |
|
438 lemma bv_to_nat_upper_range: "bv_to_nat w < 2 ^ length w" |
|
439 proof (induct w,simp_all) |
|
440 fix b bs |
|
441 assume "bv_to_nat bs < 2 ^ length bs" |
|
442 show "bitval b * 2 ^ length bs + bv_to_nat bs < 2 * 2 ^ length bs" |
|
443 proof (cases b,simp_all) |
|
444 have "bv_to_nat bs < 2 ^ length bs" |
|
445 . |
|
446 also have "... < 2 * 2 ^ length bs" |
|
447 by auto |
|
448 finally show "bv_to_nat bs < 2 * 2 ^ length bs" |
|
449 by simp |
|
450 next |
|
451 have "bv_to_nat bs < 2 ^ length bs" |
|
452 . |
|
453 hence "2 ^ length bs + bv_to_nat bs < 2 ^ length bs + 2 ^ length bs" |
|
454 by arith |
|
455 also have "... = 2 * (2 ^ length bs)" |
|
456 by simp |
|
457 finally show "bv_to_nat bs < 2 ^ length bs" |
|
458 by simp |
|
459 qed |
|
460 qed |
|
461 |
|
462 lemma [simp]: |
|
463 assumes wn: "n \<le> length w" |
|
464 shows "bv_extend n b w = w" |
|
465 by (simp add: bv_extend_def wn) |
|
466 |
|
467 lemma [simp]: |
|
468 assumes wn: "length w < n" |
|
469 shows "bv_extend n b w = bv_extend n b (b#w)" |
|
470 proof - |
|
471 from wn |
|
472 have s: "n - Suc (length w) + 1 = n - length w" |
|
473 by arith |
|
474 have "bv_extend n b w = replicate (n - length w) b @ w" |
|
475 by (simp add: bv_extend_def) |
|
476 also have "... = replicate (n - Suc (length w) + 1) b @ w" |
|
477 by (subst s,rule) |
|
478 also have "... = (replicate (n - Suc (length w)) b @ replicate 1 b) @ w" |
|
479 by (subst replicate_add,rule) |
|
480 also have "... = replicate (n - Suc (length w)) b @ b # w" |
|
481 by simp |
|
482 also have "... = bv_extend n b (b#w)" |
|
483 by (simp add: bv_extend_def) |
|
484 finally show "bv_extend n b w = bv_extend n b (b#w)" |
|
485 . |
|
486 qed |
|
487 |
|
488 consts |
|
489 rem_initial :: "bit => bit list => bit list" |
|
490 |
|
491 primrec |
|
492 "rem_initial b [] = []" |
|
493 "rem_initial b (x#xs) = (if b = x then rem_initial b xs else x#xs)" |
|
494 |
|
495 lemma rem_initial_length: "length (rem_initial b w) \<le> length w" |
|
496 by (rule bit_list_induct [of _ w],simp_all (no_asm),safe,simp_all) |
|
497 |
|
498 lemma rem_initial_equal: |
|
499 assumes p: "length (rem_initial b w) = length w" |
|
500 shows "rem_initial b w = w" |
|
501 proof - |
|
502 have "length (rem_initial b w) = length w --> rem_initial b w = w" |
|
503 proof (induct w,simp_all,clarify) |
|
504 fix xs |
|
505 assume "length (rem_initial b xs) = length xs --> rem_initial b xs = xs" |
|
506 assume f: "length (rem_initial b xs) = Suc (length xs)" |
|
507 with rem_initial_length [of b xs] |
|
508 show "rem_initial b xs = b#xs" |
|
509 by auto |
|
510 qed |
|
511 thus ?thesis |
|
512 .. |
|
513 qed |
|
514 |
|
515 lemma bv_extend_rem_initial: "bv_extend (length w) b (rem_initial b w) = w" |
|
516 proof (induct w,simp_all,safe) |
|
517 fix xs |
|
518 assume ind: "bv_extend (length xs) b (rem_initial b xs) = xs" |
|
519 from rem_initial_length [of b xs] |
|
520 have [simp]: "Suc (length xs) - length (rem_initial b xs) = 1 + (length xs - length (rem_initial b xs))" |
|
521 by arith |
|
522 have "bv_extend (Suc (length xs)) b (rem_initial b xs) = replicate (Suc (length xs) - length (rem_initial b xs)) b @ (rem_initial b xs)" |
|
523 by (simp add: bv_extend_def) |
|
524 also have "... = replicate (1 + (length xs - length (rem_initial b xs))) b @ rem_initial b xs" |
|
525 by simp |
|
526 also have "... = (replicate 1 b @ replicate (length xs - length (rem_initial b xs)) b) @ rem_initial b xs" |
|
527 by (subst replicate_add,rule refl) |
|
528 also have "... = b # bv_extend (length xs) b (rem_initial b xs)" |
|
529 by (auto simp add: bv_extend_def [symmetric]) |
|
530 also have "... = b # xs" |
|
531 by (simp add: ind) |
|
532 finally show "bv_extend (Suc (length xs)) b (rem_initial b xs) = b # xs" |
|
533 . |
|
534 qed |
|
535 |
|
536 lemma rem_initial_append1: |
|
537 assumes "rem_initial b xs ~= []" |
|
538 shows "rem_initial b (xs @ ys) = rem_initial b xs @ ys" |
|
539 proof - |
|
540 have "rem_initial b xs ~= [] --> rem_initial b (xs @ ys) = rem_initial b xs @ ys" (is "?P xs ys") |
|
541 by (induct xs,auto) |
|
542 thus ?thesis |
|
543 .. |
|
544 qed |
|
545 |
|
546 lemma rem_initial_append2: |
|
547 assumes "rem_initial b xs = []" |
|
548 shows "rem_initial b (xs @ ys) = rem_initial b ys" |
|
549 proof - |
|
550 have "rem_initial b xs = [] --> rem_initial b (xs @ ys) = rem_initial b ys" (is "?P xs ys") |
|
551 by (induct xs,auto) |
|
552 thus ?thesis |
|
553 .. |
|
554 qed |
|
555 |
|
556 constdefs |
|
557 norm_unsigned :: "bit list => bit list" |
|
558 "norm_unsigned == rem_initial \<zero>" |
|
559 |
|
560 lemma [simp]: "norm_unsigned [] = []" |
|
561 by (simp add: norm_unsigned_def) |
|
562 |
|
563 lemma [simp]: "norm_unsigned (\<zero>#bs) = norm_unsigned bs" |
|
564 by (simp add: norm_unsigned_def) |
|
565 |
|
566 lemma [simp]: "norm_unsigned (\<one>#bs) = \<one>#bs" |
|
567 by (simp add: norm_unsigned_def) |
|
568 |
|
569 lemma [simp]: "norm_unsigned (norm_unsigned w) = norm_unsigned w" |
|
570 by (rule bit_list_induct [of _ w],simp_all) |
|
571 |
|
572 consts |
|
573 nat_to_bv_helper :: "int => bit list => bit list" |
|
574 |
|
575 recdef nat_to_bv_helper "measure nat" |
|
576 "nat_to_bv_helper n = (%bs. (if n \<le> 0 then bs |
|
577 else nat_to_bv_helper (n div 2) ((if n mod 2 = 0 then \<zero> else \<one>)#bs)))" |
|
578 |
|
579 constdefs |
|
580 nat_to_bv :: "int => bit list" |
|
581 "nat_to_bv n == nat_to_bv_helper n []" |
|
582 |
|
583 lemma nat_to_bv0 [simp]: "nat_to_bv 0 = []" |
|
584 by (simp add: nat_to_bv_def) |
|
585 |
|
586 lemmas [simp del] = nat_to_bv_helper.simps |
|
587 |
|
588 lemma n_div_2_cases: |
|
589 assumes n0 : "0 \<le> n" |
|
590 and zero: "(n::int) = 0 ==> R" |
|
591 and div : "[| n div 2 < n ; 0 < n |] ==> R" |
|
592 shows "R" |
|
593 proof (cases "n = 0") |
|
594 assume "n = 0" |
|
595 thus R |
|
596 by (rule zero) |
|
597 next |
|
598 assume "n ~= 0" |
|
599 with n0 |
|
600 have nn0: "0 < n" |
|
601 by simp |
|
602 hence "n div 2 < n" |
|
603 by arith |
|
604 from this and nn0 |
|
605 show R |
|
606 by (rule div) |
|
607 qed |
|
608 |
|
609 lemma int_wf_ge_induct: |
|
610 assumes base: "P (k::int)" |
|
611 and ind : "!!i. (!!j. [| k \<le> j ; j < i |] ==> P j) ==> P i" |
|
612 and valid: "k \<le> i" |
|
613 shows "P i" |
|
614 proof - |
|
615 have a: "\<forall> j. k \<le> j \<and> j < i --> P j" |
|
616 proof (rule int_ge_induct) |
|
617 show "k \<le> i" |
|
618 . |
|
619 next |
|
620 show "\<forall> j. k \<le> j \<and> j < k --> P j" |
|
621 by auto |
|
622 next |
|
623 fix i |
|
624 assume "k \<le> i" |
|
625 assume a: "\<forall> j. k \<le> j \<and> j < i --> P j" |
|
626 have pi: "P i" |
|
627 proof (rule ind) |
|
628 fix j |
|
629 assume "k \<le> j" and "j < i" |
|
630 with a |
|
631 show "P j" |
|
632 by auto |
|
633 qed |
|
634 show "\<forall> j. k \<le> j \<and> j < i + 1 --> P j" |
|
635 proof auto |
|
636 fix j |
|
637 assume kj: "k \<le> j" |
|
638 assume ji: "j \<le> i" |
|
639 show "P j" |
|
640 proof (cases "j = i") |
|
641 assume "j = i" |
|
642 with pi |
|
643 show "P j" |
|
644 by simp |
|
645 next |
|
646 assume "j ~= i" |
|
647 with ji |
|
648 have "j < i" |
|
649 by simp |
|
650 with kj and a |
|
651 show "P j" |
|
652 by blast |
|
653 qed |
|
654 qed |
|
655 qed |
|
656 show "P i" |
|
657 proof (rule ind) |
|
658 fix j |
|
659 assume "k \<le> j" and "j < i" |
|
660 with a |
|
661 show "P j" |
|
662 by auto |
|
663 qed |
|
664 qed |
|
665 |
|
666 lemma unfold_nat_to_bv_helper: |
|
667 "0 \<le> b ==> nat_to_bv_helper b l = nat_to_bv_helper b [] @ l" |
|
668 proof - |
|
669 assume "0 \<le> b" |
|
670 have "\<forall>l. nat_to_bv_helper b l = nat_to_bv_helper b [] @ l" |
|
671 proof (rule int_wf_ge_induct [where ?i = b]) |
|
672 show "0 \<le> b" |
|
673 . |
|
674 next |
|
675 show "\<forall> l. nat_to_bv_helper 0 l = nat_to_bv_helper 0 [] @ l" |
|
676 by (simp add: nat_to_bv_helper.simps) |
|
677 next |
|
678 fix n |
|
679 assume ind: "!!j. [| 0 \<le> j ; j < n |] ==> \<forall> l. nat_to_bv_helper j l = nat_to_bv_helper j [] @ l" |
|
680 show "\<forall>l. nat_to_bv_helper n l = nat_to_bv_helper n [] @ l" |
|
681 proof |
|
682 fix l |
|
683 show "nat_to_bv_helper n l = nat_to_bv_helper n [] @ l" |
|
684 proof (cases "n < 0") |
|
685 assume "n < 0" |
|
686 thus ?thesis |
|
687 by (simp add: nat_to_bv_helper.simps) |
|
688 next |
|
689 assume "~n < 0" |
|
690 show ?thesis |
|
691 proof (rule n_div_2_cases [of n]) |
|
692 from prems |
|
693 show "0 \<le> n" |
|
694 by simp |
|
695 next |
|
696 assume [simp]: "n = 0" |
|
697 show ?thesis |
|
698 apply (subst nat_to_bv_helper.simps [of n]) |
|
699 apply simp |
|
700 done |
|
701 next |
|
702 assume n2n: "n div 2 < n" |
|
703 assume [simp]: "0 < n" |
|
704 hence n20: "0 \<le> n div 2" |
|
705 by arith |
|
706 from ind [of "n div 2"] and n2n n20 |
|
707 have ind': "\<forall>l. nat_to_bv_helper (n div 2) l = nat_to_bv_helper (n div 2) [] @ l" |
|
708 by blast |
|
709 show ?thesis |
|
710 apply (subst nat_to_bv_helper.simps [of n]) |
|
711 apply simp |
|
712 apply (subst spec [OF ind',of "\<zero>#l"]) |
|
713 apply (subst spec [OF ind',of "\<one>#l"]) |
|
714 apply (subst spec [OF ind',of "[\<one>]"]) |
|
715 apply (subst spec [OF ind',of "[\<zero>]"]) |
|
716 apply simp |
|
717 done |
|
718 qed |
|
719 qed |
|
720 qed |
|
721 qed |
|
722 thus ?thesis |
|
723 .. |
|
724 qed |
|
725 |
|
726 lemma nat_to_bv_non0 [simp]: "0 < n ==> nat_to_bv n = nat_to_bv (n div 2) @ [if n mod 2 = 0 then \<zero> else \<one>]" |
|
727 proof - |
|
728 assume [simp]: "0 < n" |
|
729 show ?thesis |
|
730 apply (subst nat_to_bv_def [of n]) |
|
731 apply (subst nat_to_bv_helper.simps [of n]) |
|
732 apply (subst unfold_nat_to_bv_helper) |
|
733 using prems |
|
734 apply arith |
|
735 apply simp |
|
736 apply (subst nat_to_bv_def [of "n div 2"]) |
|
737 apply auto |
|
738 using prems |
|
739 apply auto |
|
740 done |
|
741 qed |
|
742 |
|
743 lemma bv_to_nat_dist_append: "bv_to_nat (l1 @ l2) = bv_to_nat l1 * 2 ^ length l2 + bv_to_nat l2" |
|
744 proof - |
|
745 have "\<forall>l2. bv_to_nat (l1 @ l2) = bv_to_nat l1 * 2 ^ length l2 + bv_to_nat l2" |
|
746 proof (induct l1,simp_all) |
|
747 fix x xs |
|
748 assume ind: "\<forall>l2. bv_to_nat (xs @ l2) = bv_to_nat xs * 2 ^ length l2 + bv_to_nat l2" |
|
749 show "\<forall>l2. bitval x * 2 ^ (length xs + length l2) + bv_to_nat xs * 2 ^ length l2 = (bitval x * 2 ^ length xs + bv_to_nat xs) * 2 ^ length l2" |
|
750 proof |
|
751 fix l2 |
|
752 show "bitval x * 2 ^ (length xs + length l2) + bv_to_nat xs * 2 ^ length l2 = (bitval x * 2 ^ length xs + bv_to_nat xs) * 2 ^ length l2" |
|
753 proof - |
|
754 have "(2::int) ^ (length xs + length l2) = 2 ^ length xs * 2 ^ length l2" |
|
755 by (induct "length xs",simp_all) |
|
756 hence "bitval x * 2 ^ (length xs + length l2) + bv_to_nat xs * 2 ^ length l2 = |
|
757 bitval x * 2 ^ length xs * 2 ^ length l2 + bv_to_nat xs * 2 ^ length l2" |
|
758 by simp |
|
759 also have "... = (bitval x * 2 ^ length xs + bv_to_nat xs) * 2 ^ length l2" |
|
760 by (simp add: ring_distrib) |
|
761 finally show ?thesis . |
|
762 qed |
|
763 qed |
|
764 qed |
|
765 thus ?thesis |
|
766 .. |
|
767 qed |
|
768 |
|
769 lemma bv_nat_bv [simp]: |
|
770 assumes n0: "0 \<le> n" |
|
771 shows "bv_to_nat (nat_to_bv n) = n" |
|
772 proof - |
|
773 have "0 \<le> n --> bv_to_nat (nat_to_bv n) = n" |
|
774 proof (rule int_wf_ge_induct [where ?k = 0],simp_all,clarify) |
|
775 fix n |
|
776 assume ind: "!!j. [| 0 \<le> j; j < n |] ==> bv_to_nat (nat_to_bv j) = j" |
|
777 assume n0: "0 \<le> n" |
|
778 show "bv_to_nat (nat_to_bv n) = n" |
|
779 proof (rule n_div_2_cases [of n]) |
|
780 show "0 \<le> n" |
|
781 . |
|
782 next |
|
783 assume [simp]: "n = 0" |
|
784 show ?thesis |
|
785 by simp |
|
786 next |
|
787 assume nn: "n div 2 < n" |
|
788 assume n0: "0 < n" |
|
789 hence n20: "0 \<le> n div 2" |
|
790 by arith |
|
791 from ind and n20 nn |
|
792 have ind': "bv_to_nat (nat_to_bv (n div 2)) = n div 2" |
|
793 by blast |
|
794 from n0 have n0': "~ n \<le> 0" |
|
795 by simp |
|
796 show ?thesis |
|
797 apply (subst nat_to_bv_def) |
|
798 apply (subst nat_to_bv_helper.simps [of n]) |
|
799 apply (simp add: n0' split del: split_if) |
|
800 apply (subst unfold_nat_to_bv_helper) |
|
801 apply (rule n20) |
|
802 apply (subst bv_to_nat_dist_append) |
|
803 apply (fold nat_to_bv_def) |
|
804 apply (simp add: ind' split del: split_if) |
|
805 apply (cases "n mod 2 = 0") |
|
806 proof simp_all |
|
807 assume "n mod 2 = 0" |
|
808 with zmod_zdiv_equality [of n 2] |
|
809 show "n div 2 * 2 = n" |
|
810 by simp |
|
811 next |
|
812 assume "n mod 2 = 1" |
|
813 with zmod_zdiv_equality [of n 2] |
|
814 show "n div 2 * 2 + 1 = n" |
|
815 by simp |
|
816 qed |
|
817 qed |
|
818 qed |
|
819 with n0 |
|
820 show ?thesis |
|
821 by auto |
|
822 qed |
|
823 |
|
824 lemma [simp]: "bv_to_nat (norm_unsigned w) = bv_to_nat w" |
|
825 by (rule bit_list_induct,simp_all) |
|
826 |
|
827 lemma [simp]: "length (norm_unsigned w) \<le> length w" |
|
828 by (rule bit_list_induct,simp_all) |
|
829 |
|
830 lemma bv_to_nat_rew_msb: "bv_msb w = \<one> ==> bv_to_nat w = 2 ^ (length w - 1) + bv_to_nat (tl w)" |
|
831 by (rule bit_list_cases [of w],simp_all) |
|
832 |
|
833 lemma norm_unsigned_result: "norm_unsigned xs = [] \<or> bv_msb (norm_unsigned xs) = \<one>" |
|
834 proof (rule length_induct [of _ xs]) |
|
835 fix xs :: "bit list" |
|
836 assume ind: "\<forall>ys. length ys < length xs --> norm_unsigned ys = [] \<or> bv_msb (norm_unsigned ys) = \<one>" |
|
837 show "norm_unsigned xs = [] \<or> bv_msb (norm_unsigned xs) = \<one>" |
|
838 proof (rule bit_list_cases [of xs],simp_all) |
|
839 fix bs |
|
840 assume [simp]: "xs = \<zero>#bs" |
|
841 from ind |
|
842 have "length bs < length xs --> norm_unsigned bs = [] \<or> bv_msb (norm_unsigned bs) = \<one>" |
|
843 .. |
|
844 thus "norm_unsigned bs = [] \<or> bv_msb (norm_unsigned bs) = \<one>" |
|
845 by simp |
|
846 qed |
|
847 qed |
|
848 |
|
849 lemma norm_empty_bv_to_nat_zero: |
|
850 assumes nw: "norm_unsigned w = []" |
|
851 shows "bv_to_nat w = 0" |
|
852 proof - |
|
853 have "bv_to_nat w = bv_to_nat (norm_unsigned w)" |
|
854 by simp |
|
855 also have "... = bv_to_nat []" |
|
856 by (subst nw,rule) |
|
857 also have "... = 0" |
|
858 by simp |
|
859 finally show ?thesis . |
|
860 qed |
|
861 |
|
862 lemma bv_to_nat_lower_limit: |
|
863 assumes w0: "0 < bv_to_nat w" |
|
864 shows "2 ^ (length (norm_unsigned w) - 1) \<le> bv_to_nat w" |
|
865 proof - |
|
866 from w0 and norm_unsigned_result [of w] |
|
867 have msbw: "bv_msb (norm_unsigned w) = \<one>" |
|
868 by (auto simp add: norm_empty_bv_to_nat_zero) |
|
869 have "2 ^ (length (norm_unsigned w) - 1) \<le> bv_to_nat (norm_unsigned w)" |
|
870 by (subst bv_to_nat_rew_msb [OF msbw],simp) |
|
871 thus ?thesis |
|
872 by simp |
|
873 qed |
|
874 |
|
875 lemmas [simp del] = nat_to_bv_non0 |
|
876 |
|
877 lemma norm_unsigned_length [intro!]: "length (norm_unsigned w) \<le> length w" |
|
878 by (subst norm_unsigned_def,rule rem_initial_length) |
|
879 |
|
880 lemma norm_unsigned_equal: "length (norm_unsigned w) = length w ==> norm_unsigned w = w" |
|
881 by (simp add: norm_unsigned_def,rule rem_initial_equal) |
|
882 |
|
883 lemma bv_extend_norm_unsigned: "bv_extend (length w) \<zero> (norm_unsigned w) = w" |
|
884 by (simp add: norm_unsigned_def,rule bv_extend_rem_initial) |
|
885 |
|
886 lemma norm_unsigned_append1 [simp]: "norm_unsigned xs \<noteq> [] ==> norm_unsigned (xs @ ys) = norm_unsigned xs @ ys" |
|
887 by (simp add: norm_unsigned_def,rule rem_initial_append1) |
|
888 |
|
889 lemma norm_unsigned_append2 [simp]: "norm_unsigned xs = [] ==> norm_unsigned (xs @ ys) = norm_unsigned ys" |
|
890 by (simp add: norm_unsigned_def,rule rem_initial_append2) |
|
891 |
|
892 lemma bv_to_nat_zero_imp_empty: |
|
893 assumes "bv_to_nat w = 0" |
|
894 shows "norm_unsigned w = []" |
|
895 proof - |
|
896 have "bv_to_nat w = 0 --> norm_unsigned w = []" |
|
897 apply (rule bit_list_induct [of _ w],simp_all) |
|
898 apply (subgoal_tac "0 < 2 ^ length bs + bv_to_nat bs") |
|
899 apply simp |
|
900 apply (subgoal_tac "(0::int) < 2 ^ length bs") |
|
901 apply (subgoal_tac "0 \<le> bv_to_nat bs") |
|
902 apply arith |
|
903 apply auto |
|
904 done |
|
905 thus ?thesis |
|
906 .. |
|
907 qed |
|
908 |
|
909 lemma bv_to_nat_nzero_imp_nempty: |
|
910 assumes "bv_to_nat w \<noteq> 0" |
|
911 shows "norm_unsigned w \<noteq> []" |
|
912 proof - |
|
913 have "bv_to_nat w \<noteq> 0 --> norm_unsigned w \<noteq> []" |
|
914 by (rule bit_list_induct [of _ w],simp_all) |
|
915 thus ?thesis |
|
916 .. |
|
917 qed |
|
918 |
|
919 lemma nat_helper1: |
|
920 assumes ass: "nat_to_bv (bv_to_nat w) = norm_unsigned w" |
|
921 shows "nat_to_bv (2 * bv_to_nat w + bitval x) = norm_unsigned (w @ [x])" |
|
922 proof (cases x) |
|
923 assume [simp]: "x = \<one>" |
|
924 show ?thesis |
|
925 apply (simp add: nat_to_bv_non0) |
|
926 apply safe |
|
927 proof - |
|
928 fix q |
|
929 assume "(2 * bv_to_nat w) + 1 = 2 * q" |
|
930 hence orig: "(2 * bv_to_nat w + 1) mod 2 = 2 * q mod 2" (is "?lhs = ?rhs") |
|
931 by simp |
|
932 have "?lhs = (1 + 2 * bv_to_nat w) mod 2" |
|
933 by (simp add: add_commute) |
|
934 also have "... = 1" |
|
935 by (simp add: zmod_zadd1_eq) |
|
936 finally have eq1: "?lhs = 1" . |
|
937 have "?rhs = 0" |
|
938 by simp |
|
939 with orig and eq1 |
|
940 have "(1::int) = 0" |
|
941 by simp |
|
942 thus "nat_to_bv ((2 * bv_to_nat w + 1) div 2) @ [\<zero>] = norm_unsigned (w @ [\<one>])" |
|
943 by simp |
|
944 next |
|
945 have "nat_to_bv ((2 * bv_to_nat w + 1) div 2) @ [\<one>] = nat_to_bv ((1 + 2 * bv_to_nat w) div 2) @ [\<one>]" |
|
946 by (simp add: add_commute) |
|
947 also have "... = nat_to_bv (bv_to_nat w) @ [\<one>]" |
|
948 by (subst zdiv_zadd1_eq,simp) |
|
949 also have "... = norm_unsigned w @ [\<one>]" |
|
950 by (subst ass,rule refl) |
|
951 also have "... = norm_unsigned (w @ [\<one>])" |
|
952 by (cases "norm_unsigned w",simp_all) |
|
953 finally show "nat_to_bv ((2 * bv_to_nat w + 1) div 2) @ [\<one>] = norm_unsigned (w @ [\<one>])" |
|
954 . |
|
955 qed |
|
956 next |
|
957 assume [simp]: "x = \<zero>" |
|
958 show ?thesis |
|
959 proof (cases "bv_to_nat w = 0") |
|
960 assume "bv_to_nat w = 0" |
|
961 thus ?thesis |
|
962 by (simp add: bv_to_nat_zero_imp_empty) |
|
963 next |
|
964 assume "bv_to_nat w \<noteq> 0" |
|
965 thus ?thesis |
|
966 apply simp |
|
967 apply (subst nat_to_bv_non0) |
|
968 apply simp |
|
969 apply auto |
|
970 apply (cut_tac bv_to_nat_lower_range [of w]) |
|
971 apply arith |
|
972 apply (subst ass) |
|
973 apply (cases "norm_unsigned w") |
|
974 apply (simp_all add: norm_empty_bv_to_nat_zero) |
|
975 done |
|
976 qed |
|
977 qed |
|
978 |
|
979 lemma nat_helper2: "nat_to_bv (2 ^ length xs + bv_to_nat xs) = \<one> # xs" |
|
980 proof - |
|
981 have "\<forall>xs. nat_to_bv (2 ^ length (rev xs) + bv_to_nat (rev xs)) = \<one> # (rev xs)" (is "\<forall>xs. ?P xs") |
|
982 proof |
|
983 fix xs |
|
984 show "?P xs" |
|
985 proof (rule length_induct [of _ xs]) |
|
986 fix xs :: "bit list" |
|
987 assume ind: "\<forall>ys. length ys < length xs --> ?P ys" |
|
988 show "?P xs" |
|
989 proof (cases xs) |
|
990 assume [simp]: "xs = []" |
|
991 show ?thesis |
|
992 by (simp add: nat_to_bv_non0) |
|
993 next |
|
994 fix y ys |
|
995 assume [simp]: "xs = y # ys" |
|
996 show ?thesis |
|
997 apply simp |
|
998 apply (subst bv_to_nat_dist_append) |
|
999 apply simp |
|
1000 proof - |
|
1001 have "nat_to_bv (2 * 2 ^ length ys + (bv_to_nat (rev ys) * 2 + bitval y)) = |
|
1002 nat_to_bv (2 * (2 ^ length ys + bv_to_nat (rev ys)) + bitval y)" |
|
1003 by (simp add: add_ac mult_ac) |
|
1004 also have "... = nat_to_bv (2 * (bv_to_nat (\<one>#rev ys)) + bitval y)" |
|
1005 by simp |
|
1006 also have "... = norm_unsigned (\<one>#rev ys) @ [y]" |
|
1007 proof - |
|
1008 from ind |
|
1009 have "nat_to_bv (2 ^ length (rev ys) + bv_to_nat (rev ys)) = \<one> # rev ys" |
|
1010 by auto |
|
1011 hence [simp]: "nat_to_bv (2 ^ length ys + bv_to_nat (rev ys)) = \<one> # rev ys" |
|
1012 by simp |
|
1013 show ?thesis |
|
1014 apply (subst nat_helper1) |
|
1015 apply simp_all |
|
1016 done |
|
1017 qed |
|
1018 also have "... = (\<one>#rev ys) @ [y]" |
|
1019 by simp |
|
1020 also have "... = \<one> # rev ys @ [y]" |
|
1021 by simp |
|
1022 finally show "nat_to_bv (2 * 2 ^ length ys + (bv_to_nat (rev ys) * 2 + bitval y)) = \<one> # rev ys @ [y]" |
|
1023 . |
|
1024 qed |
|
1025 qed |
|
1026 qed |
|
1027 qed |
|
1028 hence "nat_to_bv (2 ^ length (rev (rev xs)) + bv_to_nat (rev (rev xs))) = \<one> # rev (rev xs)" |
|
1029 .. |
|
1030 thus ?thesis |
|
1031 by simp |
|
1032 qed |
|
1033 |
|
1034 lemma nat_bv_nat [simp]: "nat_to_bv (bv_to_nat w) = norm_unsigned w" |
|
1035 proof (rule bit_list_induct [of _ w],simp_all) |
|
1036 fix xs |
|
1037 assume "nat_to_bv (bv_to_nat xs) = norm_unsigned xs" |
|
1038 have "bv_to_nat xs = bv_to_nat (norm_unsigned xs)" |
|
1039 by simp |
|
1040 have "bv_to_nat xs < 2 ^ length xs" |
|
1041 by (rule bv_to_nat_upper_range) |
|
1042 show "nat_to_bv (2 ^ length xs + bv_to_nat xs) = \<one> # xs" |
|
1043 by (rule nat_helper2) |
|
1044 qed |
|
1045 |
|
1046 lemma [simp]: "bv_to_nat (norm_unsigned xs) = bv_to_nat xs" |
|
1047 by (rule bit_list_induct [of _ w],simp_all) |
|
1048 |
|
1049 lemma bv_to_nat_qinj: |
|
1050 assumes one: "bv_to_nat xs = bv_to_nat ys" |
|
1051 and len: "length xs = length ys" |
|
1052 shows "xs = ys" |
|
1053 proof - |
|
1054 from one |
|
1055 have "nat_to_bv (bv_to_nat xs) = nat_to_bv (bv_to_nat ys)" |
|
1056 by simp |
|
1057 hence xsys: "norm_unsigned xs = norm_unsigned ys" |
|
1058 by simp |
|
1059 have "xs = bv_extend (length xs) \<zero> (norm_unsigned xs)" |
|
1060 by (simp add: bv_extend_norm_unsigned) |
|
1061 also have "... = bv_extend (length ys) \<zero> (norm_unsigned ys)" |
|
1062 by (simp add: xsys len) |
|
1063 also have "... = ys" |
|
1064 by (simp add: bv_extend_norm_unsigned) |
|
1065 finally show ?thesis . |
|
1066 qed |
|
1067 |
|
1068 lemma norm_unsigned_nat_to_bv [simp]: |
|
1069 assumes [simp]: "0 \<le> n" |
|
1070 shows "norm_unsigned (nat_to_bv n) = nat_to_bv n" |
|
1071 proof - |
|
1072 have "norm_unsigned (nat_to_bv n) = nat_to_bv (bv_to_nat (norm_unsigned (nat_to_bv n)))" |
|
1073 by (subst nat_bv_nat,simp) |
|
1074 also have "... = nat_to_bv n" |
|
1075 by simp |
|
1076 finally show ?thesis . |
|
1077 qed |
|
1078 |
|
1079 lemma length_nat_to_bv_upper_limit: |
|
1080 assumes nk: "n \<le> 2 ^ k - 1" |
|
1081 shows "length (nat_to_bv n) \<le> k" |
|
1082 proof (cases "n \<le> 0") |
|
1083 assume "n \<le> 0" |
|
1084 thus ?thesis |
|
1085 by (simp add: nat_to_bv_def nat_to_bv_helper.simps) |
|
1086 next |
|
1087 assume "~ n \<le> 0" |
|
1088 hence n0: "0 < n" |
|
1089 by simp |
|
1090 hence n00: "0 \<le> n" |
|
1091 by simp |
|
1092 show ?thesis |
|
1093 proof (rule ccontr) |
|
1094 assume "~ length (nat_to_bv n) \<le> k" |
|
1095 hence "k < length (nat_to_bv n)" |
|
1096 by simp |
|
1097 hence "k \<le> length (nat_to_bv n) - 1" |
|
1098 by arith |
|
1099 hence "(2::int) ^ k \<le> 2 ^ (length (nat_to_bv n) - 1)" |
|
1100 by simp |
|
1101 also have "... = 2 ^ (length (norm_unsigned (nat_to_bv n)) - 1)" |
|
1102 by (simp add: n00) |
|
1103 also have "... \<le> bv_to_nat (nat_to_bv n)" |
|
1104 by (rule bv_to_nat_lower_limit,simp add: n00 n0) |
|
1105 also have "... = n" |
|
1106 by (simp add: n00) |
|
1107 finally have "2 ^ k \<le> n" . |
|
1108 with n0 |
|
1109 have "2 ^ k - 1 < n" |
|
1110 by arith |
|
1111 with nk |
|
1112 show False |
|
1113 by simp |
|
1114 qed |
|
1115 qed |
|
1116 |
|
1117 lemma length_nat_to_bv_lower_limit: |
|
1118 assumes nk: "2 ^ k \<le> n" |
|
1119 shows "k < length (nat_to_bv n)" |
|
1120 proof (rule ccontr) |
|
1121 have "(0::int) \<le> 2 ^ k" |
|
1122 by auto |
|
1123 with nk |
|
1124 have [simp]: "0 \<le> n" |
|
1125 by auto |
|
1126 assume "~ k < length (nat_to_bv n)" |
|
1127 hence lnk: "length (nat_to_bv n) \<le> k" |
|
1128 by simp |
|
1129 have "n = bv_to_nat (nat_to_bv n)" |
|
1130 by simp |
|
1131 also have "... < 2 ^ length (nat_to_bv n)" |
|
1132 by (rule bv_to_nat_upper_range) |
|
1133 also from lnk have "... \<le> 2 ^ k" |
|
1134 by simp |
|
1135 finally have "n < 2 ^ k" . |
|
1136 with nk |
|
1137 show False |
|
1138 by simp |
|
1139 qed |
|
1140 |
|
1141 section {* Unsigned Arithmetic Operations *} |
|
1142 |
|
1143 constdefs |
|
1144 bv_add :: "[bit list, bit list ] => bit list" |
|
1145 "bv_add w1 w2 == nat_to_bv (bv_to_nat w1 + bv_to_nat w2)" |
|
1146 |
|
1147 lemma [simp]: "bv_add (norm_unsigned w1) w2 = bv_add w1 w2" |
|
1148 by (simp add: bv_add_def) |
|
1149 |
|
1150 lemma [simp]: "bv_add w1 (norm_unsigned w2) = bv_add w1 w2" |
|
1151 by (simp add: bv_add_def) |
|
1152 |
|
1153 lemma [simp]: "norm_unsigned (bv_add w1 w2) = bv_add w1 w2" |
|
1154 apply (simp add: bv_add_def) |
|
1155 apply (rule norm_unsigned_nat_to_bv) |
|
1156 apply (subgoal_tac "0 \<le> bv_to_nat w1") |
|
1157 apply (subgoal_tac "0 \<le> bv_to_nat w2") |
|
1158 apply arith |
|
1159 apply simp_all |
|
1160 done |
|
1161 |
|
1162 lemma bv_add_length: "length (bv_add w1 w2) \<le> Suc (max (length w1) (length w2))" |
|
1163 proof (unfold bv_add_def,rule length_nat_to_bv_upper_limit) |
|
1164 from bv_to_nat_upper_range [of w1] and bv_to_nat_upper_range [of w2] |
|
1165 have "bv_to_nat w1 + bv_to_nat w2 \<le> (2 ^ length w1 - 1) + (2 ^ length w2 - 1)" |
|
1166 by arith |
|
1167 also have "... \<le> max (2 ^ length w1 - 1) (2 ^ length w2 - 1) + max (2 ^ length w1 - 1) (2 ^ length w2 - 1)" |
|
1168 by (rule add_mono,safe intro!: le_maxI1 le_maxI2) |
|
1169 also have "... = 2 * max (2 ^ length w1 - 1) (2 ^ length w2 - 1)" |
|
1170 by simp |
|
1171 also have "... \<le> 2 ^ Suc (max (length w1) (length w2)) - 2" |
|
1172 proof (cases "length w1 \<le> length w2") |
|
1173 assume [simp]: "length w1 \<le> length w2" |
|
1174 hence "(2::int) ^ length w1 \<le> 2 ^ length w2" |
|
1175 by simp |
|
1176 hence [simp]: "(2::int) ^ length w1 - 1 \<le> 2 ^ length w2 - 1" |
|
1177 by arith |
|
1178 show ?thesis |
|
1179 by (simp split: split_max) |
|
1180 next |
|
1181 assume [simp]: "~ (length w1 \<le> length w2)" |
|
1182 have "~ ((2::int) ^ length w1 - 1 \<le> 2 ^ length w2 - 1)" |
|
1183 proof |
|
1184 assume "(2::int) ^ length w1 - 1 \<le> 2 ^ length w2 - 1" |
|
1185 hence "((2::int) ^ length w1 - 1) + 1 \<le> (2 ^ length w2 - 1) + 1" |
|
1186 by (rule add_right_mono) |
|
1187 hence "(2::int) ^ length w1 \<le> 2 ^ length w2" |
|
1188 by simp |
|
1189 hence "length w1 \<le> length w2" |
|
1190 by simp |
|
1191 thus False |
|
1192 by simp |
|
1193 qed |
|
1194 thus ?thesis |
|
1195 by (simp split: split_max) |
|
1196 qed |
|
1197 finally show "bv_to_nat w1 + bv_to_nat w2 \<le> 2 ^ Suc (max (length w1) (length w2)) - 1" |
|
1198 by arith |
|
1199 qed |
|
1200 |
|
1201 constdefs |
|
1202 bv_mult :: "[bit list, bit list ] => bit list" |
|
1203 "bv_mult w1 w2 == nat_to_bv (bv_to_nat w1 * bv_to_nat w2)" |
|
1204 |
|
1205 lemma [simp]: "bv_mult (norm_unsigned w1) w2 = bv_mult w1 w2" |
|
1206 by (simp add: bv_mult_def) |
|
1207 |
|
1208 lemma [simp]: "bv_mult w1 (norm_unsigned w2) = bv_mult w1 w2" |
|
1209 by (simp add: bv_mult_def) |
|
1210 |
|
1211 lemma [simp]: "norm_unsigned (bv_mult w1 w2) = bv_mult w1 w2" |
|
1212 apply (simp add: bv_mult_def) |
|
1213 apply (rule norm_unsigned_nat_to_bv) |
|
1214 apply (subgoal_tac "0 * 0 \<le> bv_to_nat w1 * bv_to_nat w2") |
|
1215 apply simp |
|
1216 apply (rule mult_mono,simp_all) |
|
1217 done |
|
1218 |
|
1219 lemma bv_mult_length: "length (bv_mult w1 w2) \<le> length w1 + length w2" |
|
1220 proof (unfold bv_mult_def,rule length_nat_to_bv_upper_limit) |
|
1221 from bv_to_nat_upper_range [of w1] and bv_to_nat_upper_range [of w2] |
|
1222 have h: "bv_to_nat w1 \<le> 2 ^ length w1 - 1 \<and> bv_to_nat w2 \<le> 2 ^ length w2 - 1" |
|
1223 by arith |
|
1224 have "bv_to_nat w1 * bv_to_nat w2 \<le> (2 ^ length w1 - 1) * (2 ^ length w2 - 1)" |
|
1225 apply (cut_tac h) |
|
1226 apply (rule mult_mono) |
|
1227 apply auto |
|
1228 done |
|
1229 also have "... < 2 ^ length w1 * 2 ^ length w2" |
|
1230 by (rule mult_strict_mono,auto) |
|
1231 also have "... = 2 ^ (length w1 + length w2)" |
|
1232 by (simp add: power_add) |
|
1233 finally show "bv_to_nat w1 * bv_to_nat w2 \<le> 2 ^ (length w1 + length w2) - 1" |
|
1234 by arith |
|
1235 qed |
|
1236 |
|
1237 section {* Signed Vectors *} |
|
1238 |
|
1239 consts |
|
1240 norm_signed :: "bit list => bit list" |
|
1241 |
|
1242 primrec |
|
1243 norm_signed_Nil: "norm_signed [] = []" |
|
1244 norm_signed_Cons: "norm_signed (b#bs) = (case b of \<zero> => if norm_unsigned bs = [] then [] else b#norm_unsigned bs | \<one> => b#rem_initial b bs)" |
|
1245 |
|
1246 lemma [simp]: "norm_signed [\<zero>] = []" |
|
1247 by simp |
|
1248 |
|
1249 lemma [simp]: "norm_signed [\<one>] = [\<one>]" |
|
1250 by simp |
|
1251 |
|
1252 lemma [simp]: "norm_signed (\<zero>#\<one>#xs) = \<zero>#\<one>#xs" |
|
1253 by simp |
|
1254 |
|
1255 lemma [simp]: "norm_signed (\<zero>#\<zero>#xs) = norm_signed (\<zero>#xs)" |
|
1256 by simp |
|
1257 |
|
1258 lemma [simp]: "norm_signed (\<one>#\<zero>#xs) = \<one>#\<zero>#xs" |
|
1259 by simp |
|
1260 |
|
1261 lemma [simp]: "norm_signed (\<one>#\<one>#xs) = norm_signed (\<one>#xs)" |
|
1262 by simp |
|
1263 |
|
1264 lemmas [simp del] = norm_signed_Cons |
|
1265 |
|
1266 constdefs |
|
1267 int_to_bv :: "int => bit list" |
|
1268 "int_to_bv n == if 0 \<le> n |
|
1269 then norm_signed (\<zero>#nat_to_bv n) |
|
1270 else norm_signed (bv_not (\<zero>#nat_to_bv (-n- 1)))" |
|
1271 |
|
1272 lemma int_to_bv_ge0 [simp]: "0 \<le> n ==> int_to_bv n = norm_signed (\<zero> # nat_to_bv n)" |
|
1273 by (simp add: int_to_bv_def) |
|
1274 |
|
1275 lemma int_to_bv_lt0 [simp]: "n < 0 ==> int_to_bv n = norm_signed (bv_not (\<zero>#nat_to_bv (-n- 1)))" |
|
1276 by (simp add: int_to_bv_def) |
|
1277 |
|
1278 lemma [simp]: "norm_signed (norm_signed w) = norm_signed w" |
|
1279 proof (rule bit_list_induct [of _ w],simp_all) |
|
1280 fix xs |
|
1281 assume "norm_signed (norm_signed xs) = norm_signed xs" |
|
1282 show "norm_signed (norm_signed (\<zero>#xs)) = norm_signed (\<zero>#xs)" |
|
1283 proof (rule bit_list_cases [of xs],simp_all) |
|
1284 fix ys |
|
1285 assume [symmetric,simp]: "xs = \<zero>#ys" |
|
1286 show "norm_signed (norm_signed (\<zero>#ys)) = norm_signed (\<zero>#ys)" |
|
1287 by simp |
|
1288 qed |
|
1289 next |
|
1290 fix xs |
|
1291 assume "norm_signed (norm_signed xs) = norm_signed xs" |
|
1292 show "norm_signed (norm_signed (\<one>#xs)) = norm_signed (\<one>#xs)" |
|
1293 proof (rule bit_list_cases [of xs],simp_all) |
|
1294 fix ys |
|
1295 assume [symmetric,simp]: "xs = \<one>#ys" |
|
1296 show "norm_signed (norm_signed (\<one>#ys)) = norm_signed (\<one>#ys)" |
|
1297 by simp |
|
1298 qed |
|
1299 qed |
|
1300 |
|
1301 constdefs |
|
1302 bv_to_int :: "bit list => int" |
|
1303 "bv_to_int w == case bv_msb w of \<zero> => bv_to_nat w | \<one> => -(bv_to_nat (bv_not w) + 1)" |
|
1304 |
|
1305 lemma [simp]: "bv_to_int [] = 0" |
|
1306 by (simp add: bv_to_int_def) |
|
1307 |
|
1308 lemma [simp]: "bv_to_int (\<zero>#bs) = bv_to_nat bs" |
|
1309 by (simp add: bv_to_int_def) |
|
1310 |
|
1311 lemma [simp]: "bv_to_int (\<one>#bs) = -(bv_to_nat (bv_not bs) + 1)" |
|
1312 by (simp add: bv_to_int_def) |
|
1313 |
|
1314 lemma [simp]: "bv_to_int (norm_signed w) = bv_to_int w" |
|
1315 proof (rule bit_list_induct [of _ w],simp_all) |
|
1316 fix xs |
|
1317 assume ind: "bv_to_int (norm_signed xs) = bv_to_int xs" |
|
1318 show "bv_to_int (norm_signed (\<zero>#xs)) = bv_to_nat xs" |
|
1319 proof (rule bit_list_cases [of xs],simp_all) |
|
1320 fix ys |
|
1321 assume [simp]: "xs = \<zero>#ys" |
|
1322 from ind |
|
1323 show "bv_to_int (norm_signed (\<zero>#ys)) = bv_to_nat ys" |
|
1324 by simp |
|
1325 qed |
|
1326 next |
|
1327 fix xs |
|
1328 assume ind: "bv_to_int (norm_signed xs) = bv_to_int xs" |
|
1329 show "bv_to_int (norm_signed (\<one>#xs)) = - bv_to_nat (bv_not xs) + -1" |
|
1330 proof (rule bit_list_cases [of xs],simp_all) |
|
1331 fix ys |
|
1332 assume [simp]: "xs = \<one>#ys" |
|
1333 from ind |
|
1334 show "bv_to_int (norm_signed (\<one>#ys)) = - bv_to_nat (bv_not ys) + -1" |
|
1335 by simp |
|
1336 qed |
|
1337 qed |
|
1338 |
|
1339 lemma bv_to_int_upper_range: "bv_to_int w < 2 ^ (length w - 1)" |
|
1340 proof (rule bit_list_cases [of w],simp_all) |
|
1341 fix bs |
|
1342 show "bv_to_nat bs < 2 ^ length bs" |
|
1343 by (rule bv_to_nat_upper_range) |
|
1344 next |
|
1345 fix bs |
|
1346 have "- (bv_to_nat (bv_not bs)) + -1 \<le> 0 + 0" |
|
1347 by (rule add_mono,simp_all) |
|
1348 also have "... < 2 ^ length bs" |
|
1349 by (induct bs,simp_all) |
|
1350 finally show "- (bv_to_nat (bv_not bs)) + -1 < 2 ^ length bs" |
|
1351 . |
|
1352 qed |
|
1353 |
|
1354 lemma bv_to_int_lower_range: "- (2 ^ (length w - 1)) \<le> bv_to_int w" |
|
1355 proof (rule bit_list_cases [of w],simp_all) |
|
1356 fix bs :: "bit list" |
|
1357 have "- (2 ^ length bs) \<le> (0::int)" |
|
1358 by (induct bs,simp_all) |
|
1359 also have "... \<le> bv_to_nat bs" |
|
1360 by simp |
|
1361 finally show "- (2 ^ length bs) \<le> bv_to_nat bs" |
|
1362 . |
|
1363 next |
|
1364 fix bs |
|
1365 from bv_to_nat_upper_range [of "bv_not bs"] |
|
1366 have "bv_to_nat (bv_not bs) < 2 ^ length bs" |
|
1367 by simp |
|
1368 hence "bv_to_nat (bv_not bs) + 1 \<le> 2 ^ length bs" |
|
1369 by simp |
|
1370 thus "- (2 ^ length bs) \<le> - bv_to_nat (bv_not bs) + -1" |
|
1371 by simp |
|
1372 qed |
|
1373 |
|
1374 lemma int_bv_int [simp]: "int_to_bv (bv_to_int w) = norm_signed w" |
|
1375 proof (rule bit_list_cases [of w],simp) |
|
1376 fix xs |
|
1377 assume [simp]: "w = \<zero>#xs" |
|
1378 show ?thesis |
|
1379 apply simp |
|
1380 apply (subst norm_signed_Cons [of "\<zero>" "xs"]) |
|
1381 apply simp |
|
1382 using norm_unsigned_result [of xs] |
|
1383 apply safe |
|
1384 apply (rule bit_list_cases [of "norm_unsigned xs"]) |
|
1385 apply simp_all |
|
1386 done |
|
1387 next |
|
1388 fix xs |
|
1389 assume [simp]: "w = \<one>#xs" |
|
1390 show ?thesis |
|
1391 apply simp |
|
1392 apply (rule bit_list_induct [of _ xs]) |
|
1393 apply simp |
|
1394 apply (subst int_to_bv_lt0) |
|
1395 apply (subgoal_tac "- bv_to_nat (bv_not (\<zero> # bs)) + -1 < 0 + 0") |
|
1396 apply simp |
|
1397 apply (rule add_le_less_mono) |
|
1398 apply simp |
|
1399 apply (rule order_trans [of _ 0]) |
|
1400 apply simp |
|
1401 apply (rule zero_le_zpower,simp) |
|
1402 apply simp |
|
1403 apply simp |
|
1404 apply (simp del: bv_to_nat1 bv_to_nat_helper) |
|
1405 apply simp |
|
1406 done |
|
1407 qed |
|
1408 |
|
1409 lemma bv_int_bv [simp]: "bv_to_int (int_to_bv i) = i" |
|
1410 by (cases "0 \<le> i",simp_all) |
|
1411 |
|
1412 lemma bv_msb_norm [simp]: "bv_msb (norm_signed w) = bv_msb w" |
|
1413 by (rule bit_list_cases [of w],simp_all add: norm_signed_Cons) |
|
1414 |
|
1415 lemma norm_signed_length: "length (norm_signed w) \<le> length w" |
|
1416 apply (cases w,simp_all) |
|
1417 apply (subst norm_signed_Cons) |
|
1418 apply (case_tac "a",simp_all) |
|
1419 apply (rule rem_initial_length) |
|
1420 done |
|
1421 |
|
1422 lemma norm_signed_equal: "length (norm_signed w) = length w ==> norm_signed w = w" |
|
1423 proof (rule bit_list_cases [of w],simp_all) |
|
1424 fix xs |
|
1425 assume "length (norm_signed (\<zero>#xs)) = Suc (length xs)" |
|
1426 thus "norm_signed (\<zero>#xs) = \<zero>#xs" |
|
1427 apply (simp add: norm_signed_Cons) |
|
1428 apply safe |
|
1429 apply simp_all |
|
1430 apply (rule norm_unsigned_equal) |
|
1431 apply assumption |
|
1432 done |
|
1433 next |
|
1434 fix xs |
|
1435 assume "length (norm_signed (\<one>#xs)) = Suc (length xs)" |
|
1436 thus "norm_signed (\<one>#xs) = \<one>#xs" |
|
1437 apply (simp add: norm_signed_Cons) |
|
1438 apply (rule rem_initial_equal) |
|
1439 apply assumption |
|
1440 done |
|
1441 qed |
|
1442 |
|
1443 lemma bv_extend_norm_signed: "bv_msb w = b ==> bv_extend (length w) b (norm_signed w) = w" |
|
1444 proof (rule bit_list_cases [of w],simp_all) |
|
1445 fix xs |
|
1446 show "bv_extend (Suc (length xs)) \<zero> (norm_signed (\<zero>#xs)) = \<zero>#xs" |
|
1447 proof (simp add: norm_signed_list_def,auto) |
|
1448 assume "norm_unsigned xs = []" |
|
1449 hence xx: "rem_initial \<zero> xs = []" |
|
1450 by (simp add: norm_unsigned_def) |
|
1451 have "bv_extend (Suc (length xs)) \<zero> (\<zero>#rem_initial \<zero> xs) = \<zero>#xs" |
|
1452 apply (simp add: bv_extend_def replicate_app_Cons_same) |
|
1453 apply (fold bv_extend_def) |
|
1454 apply (rule bv_extend_rem_initial) |
|
1455 done |
|
1456 thus "bv_extend (Suc (length xs)) \<zero> [\<zero>] = \<zero>#xs" |
|
1457 by (simp add: xx) |
|
1458 next |
|
1459 show "bv_extend (Suc (length xs)) \<zero> (\<zero>#norm_unsigned xs) = \<zero>#xs" |
|
1460 apply (simp add: norm_unsigned_def) |
|
1461 apply (simp add: bv_extend_def replicate_app_Cons_same) |
|
1462 apply (fold bv_extend_def) |
|
1463 apply (rule bv_extend_rem_initial) |
|
1464 done |
|
1465 qed |
|
1466 next |
|
1467 fix xs |
|
1468 show "bv_extend (Suc (length xs)) \<one> (norm_signed (\<one>#xs)) = \<one>#xs" |
|
1469 apply (simp add: norm_signed_Cons) |
|
1470 apply (simp add: bv_extend_def replicate_app_Cons_same) |
|
1471 apply (fold bv_extend_def) |
|
1472 apply (rule bv_extend_rem_initial) |
|
1473 done |
|
1474 qed |
|
1475 |
|
1476 lemma bv_to_int_qinj: |
|
1477 assumes one: "bv_to_int xs = bv_to_int ys" |
|
1478 and len: "length xs = length ys" |
|
1479 shows "xs = ys" |
|
1480 proof - |
|
1481 from one |
|
1482 have "int_to_bv (bv_to_int xs) = int_to_bv (bv_to_int ys)" |
|
1483 by simp |
|
1484 hence xsys: "norm_signed xs = norm_signed ys" |
|
1485 by simp |
|
1486 hence xsys': "bv_msb xs = bv_msb ys" |
|
1487 proof - |
|
1488 have "bv_msb xs = bv_msb (norm_signed xs)" |
|
1489 by simp |
|
1490 also have "... = bv_msb (norm_signed ys)" |
|
1491 by (simp add: xsys) |
|
1492 also have "... = bv_msb ys" |
|
1493 by simp |
|
1494 finally show ?thesis . |
|
1495 qed |
|
1496 have "xs = bv_extend (length xs) (bv_msb xs) (norm_signed xs)" |
|
1497 by (simp add: bv_extend_norm_signed) |
|
1498 also have "... = bv_extend (length ys) (bv_msb ys) (norm_signed ys)" |
|
1499 by (simp add: xsys xsys' len) |
|
1500 also have "... = ys" |
|
1501 by (simp add: bv_extend_norm_signed) |
|
1502 finally show ?thesis . |
|
1503 qed |
|
1504 |
|
1505 lemma [simp]: "norm_signed (int_to_bv w) = int_to_bv w" |
|
1506 by (simp add: int_to_bv_def) |
|
1507 |
|
1508 lemma bv_to_int_msb0: "0 \<le> bv_to_int w1 ==> bv_msb w1 = \<zero>" |
|
1509 apply (rule bit_list_cases,simp_all) |
|
1510 apply (subgoal_tac "0 \<le> bv_to_nat (bv_not bs)") |
|
1511 apply simp_all |
|
1512 done |
|
1513 |
|
1514 lemma bv_to_int_msb1: "bv_to_int w1 < 0 ==> bv_msb w1 = \<one>" |
|
1515 apply (rule bit_list_cases,simp_all) |
|
1516 apply (subgoal_tac "0 \<le> bv_to_nat bs") |
|
1517 apply simp_all |
|
1518 done |
|
1519 |
|
1520 lemma bv_to_int_lower_limit_gt0: |
|
1521 assumes w0: "0 < bv_to_int w" |
|
1522 shows "2 ^ (length (norm_signed w) - 2) \<le> bv_to_int w" |
|
1523 proof - |
|
1524 from w0 |
|
1525 have "0 \<le> bv_to_int w" |
|
1526 by simp |
|
1527 hence [simp]: "bv_msb w = \<zero>" |
|
1528 by (rule bv_to_int_msb0) |
|
1529 have "2 ^ (length (norm_signed w) - 2) \<le> bv_to_int (norm_signed w)" |
|
1530 proof (rule bit_list_cases [of w]) |
|
1531 assume "w = []" |
|
1532 with w0 |
|
1533 show ?thesis |
|
1534 by simp |
|
1535 next |
|
1536 fix w' |
|
1537 assume weq: "w = \<zero> # w'" |
|
1538 thus ?thesis |
|
1539 proof (simp add: norm_signed_Cons,safe) |
|
1540 assume "norm_unsigned w' = []" |
|
1541 with weq and w0 |
|
1542 show False |
|
1543 by (simp add: norm_empty_bv_to_nat_zero) |
|
1544 next |
|
1545 assume w'0: "norm_unsigned w' \<noteq> []" |
|
1546 have "0 < bv_to_nat w'" |
|
1547 proof (rule ccontr) |
|
1548 assume "~ (0 < bv_to_nat w')" |
|
1549 with bv_to_nat_lower_range [of w'] |
|
1550 have "bv_to_nat w' = 0" |
|
1551 by arith |
|
1552 hence "norm_unsigned w' = []" |
|
1553 by (simp add: bv_to_nat_zero_imp_empty) |
|
1554 with w'0 |
|
1555 show False |
|
1556 by simp |
|
1557 qed |
|
1558 with bv_to_nat_lower_limit [of w'] |
|
1559 have "2 ^ (length (norm_unsigned w') - 1) \<le> bv_to_nat w'" |
|
1560 . |
|
1561 thus "2 ^ (length (norm_unsigned w') - Suc 0) \<le> bv_to_nat w'" |
|
1562 by simp |
|
1563 qed |
|
1564 next |
|
1565 fix w' |
|
1566 assume "w = \<one> # w'" |
|
1567 from w0 |
|
1568 have "bv_msb w = \<zero>" |
|
1569 by simp |
|
1570 with prems |
|
1571 show ?thesis |
|
1572 by simp |
|
1573 qed |
|
1574 also have "... = bv_to_int w" |
|
1575 by simp |
|
1576 finally show ?thesis . |
|
1577 qed |
|
1578 |
|
1579 lemma norm_signed_result: "norm_signed w = [] \<or> norm_signed w = [\<one>] \<or> bv_msb (norm_signed w) \<noteq> bv_msb (tl (norm_signed w))" |
|
1580 apply (rule bit_list_cases [of w],simp_all) |
|
1581 apply (case_tac "bs",simp_all) |
|
1582 apply (case_tac "a",simp_all) |
|
1583 apply (simp add: norm_signed_Cons) |
|
1584 apply safe |
|
1585 apply simp |
|
1586 proof - |
|
1587 fix l |
|
1588 assume msb: "\<zero> = bv_msb (norm_unsigned l)" |
|
1589 assume "norm_unsigned l \<noteq> []" |
|
1590 with norm_unsigned_result [of l] |
|
1591 have "bv_msb (norm_unsigned l) = \<one>" |
|
1592 by simp |
|
1593 with msb |
|
1594 show False |
|
1595 by simp |
|
1596 next |
|
1597 fix xs |
|
1598 assume p: "\<one> = bv_msb (tl (norm_signed (\<one> # xs)))" |
|
1599 have "\<one> \<noteq> bv_msb (tl (norm_signed (\<one> # xs)))" |
|
1600 by (rule bit_list_induct [of _ xs],simp_all) |
|
1601 with p |
|
1602 show False |
|
1603 by simp |
|
1604 qed |
|
1605 |
|
1606 lemma bv_to_int_upper_limit_lem1: |
|
1607 assumes w0: "bv_to_int w < -1" |
|
1608 shows "bv_to_int w < - (2 ^ (length (norm_signed w) - 2))" |
|
1609 proof - |
|
1610 from w0 |
|
1611 have "bv_to_int w < 0" |
|
1612 by simp |
|
1613 hence msbw [simp]: "bv_msb w = \<one>" |
|
1614 by (rule bv_to_int_msb1) |
|
1615 have "bv_to_int w = bv_to_int (norm_signed w)" |
|
1616 by simp |
|
1617 also from norm_signed_result [of w] |
|
1618 have "... < - (2 ^ (length (norm_signed w) - 2))" |
|
1619 proof (safe) |
|
1620 assume "norm_signed w = []" |
|
1621 hence "bv_to_int (norm_signed w) = 0" |
|
1622 by simp |
|
1623 with w0 |
|
1624 show ?thesis |
|
1625 by simp |
|
1626 next |
|
1627 assume "norm_signed w = [\<one>]" |
|
1628 hence "bv_to_int (norm_signed w) = -1" |
|
1629 by simp |
|
1630 with w0 |
|
1631 show ?thesis |
|
1632 by simp |
|
1633 next |
|
1634 assume "bv_msb (norm_signed w) \<noteq> bv_msb (tl (norm_signed w))" |
|
1635 hence msb_tl: "\<one> \<noteq> bv_msb (tl (norm_signed w))" |
|
1636 by simp |
|
1637 show "bv_to_int (norm_signed w) < - (2 ^ (length (norm_signed w) - 2))" |
|
1638 proof (rule bit_list_cases [of "norm_signed w"]) |
|
1639 assume "norm_signed w = []" |
|
1640 hence "bv_to_int (norm_signed w) = 0" |
|
1641 by simp |
|
1642 with w0 |
|
1643 show ?thesis |
|
1644 by simp |
|
1645 next |
|
1646 fix w' |
|
1647 assume nw: "norm_signed w = \<zero> # w'" |
|
1648 from msbw |
|
1649 have "bv_msb (norm_signed w) = \<one>" |
|
1650 by simp |
|
1651 with nw |
|
1652 show ?thesis |
|
1653 by simp |
|
1654 next |
|
1655 fix w' |
|
1656 assume weq: "norm_signed w = \<one> # w'" |
|
1657 show ?thesis |
|
1658 proof (rule bit_list_cases [of w']) |
|
1659 assume w'eq: "w' = []" |
|
1660 from w0 |
|
1661 have "bv_to_int (norm_signed w) < -1" |
|
1662 by simp |
|
1663 with w'eq and weq |
|
1664 show ?thesis |
|
1665 by simp |
|
1666 next |
|
1667 fix w'' |
|
1668 assume w'eq: "w' = \<zero> # w''" |
|
1669 show ?thesis |
|
1670 apply (simp add: weq w'eq) |
|
1671 apply (subgoal_tac "-bv_to_nat (bv_not w'') + -1 < 0 + 0") |
|
1672 apply simp |
|
1673 apply (rule add_le_less_mono) |
|
1674 apply simp_all |
|
1675 done |
|
1676 next |
|
1677 fix w'' |
|
1678 assume w'eq: "w' = \<one> # w''" |
|
1679 with weq and msb_tl |
|
1680 show ?thesis |
|
1681 by simp |
|
1682 qed |
|
1683 qed |
|
1684 qed |
|
1685 finally show ?thesis . |
|
1686 qed |
|
1687 |
|
1688 lemma length_int_to_bv_upper_limit_gt0: |
|
1689 assumes w0: "0 < i" |
|
1690 and wk: "i \<le> 2 ^ (k - 1) - 1" |
|
1691 shows "length (int_to_bv i) \<le> k" |
|
1692 proof (rule ccontr) |
|
1693 from w0 wk |
|
1694 have k1: "1 < k" |
|
1695 by (cases "k - 1",simp_all,arith) |
|
1696 assume "~ length (int_to_bv i) \<le> k" |
|
1697 hence "k < length (int_to_bv i)" |
|
1698 by simp |
|
1699 hence "k \<le> length (int_to_bv i) - 1" |
|
1700 by arith |
|
1701 hence a: "k - 1 \<le> length (int_to_bv i) - 2" |
|
1702 by arith |
|
1703 have "(2::int) ^ (k - 1) \<le> 2 ^ (length (int_to_bv i) - 2)" |
|
1704 apply (rule le_imp_power_zle,simp) |
|
1705 apply (rule a) |
|
1706 done |
|
1707 also have "... \<le> i" |
|
1708 proof - |
|
1709 have "2 ^ (length (norm_signed (int_to_bv i)) - 2) \<le> bv_to_int (int_to_bv i)" |
|
1710 proof (rule bv_to_int_lower_limit_gt0) |
|
1711 from w0 |
|
1712 show "0 < bv_to_int (int_to_bv i)" |
|
1713 by simp |
|
1714 qed |
|
1715 thus ?thesis |
|
1716 by simp |
|
1717 qed |
|
1718 finally have "2 ^ (k - 1) \<le> i" . |
|
1719 with wk |
|
1720 show False |
|
1721 by simp |
|
1722 qed |
|
1723 |
|
1724 lemma pos_length_pos: |
|
1725 assumes i0: "0 < bv_to_int w" |
|
1726 shows "0 < length w" |
|
1727 proof - |
|
1728 from norm_signed_result [of w] |
|
1729 have "0 < length (norm_signed w)" |
|
1730 proof (auto) |
|
1731 assume ii: "norm_signed w = []" |
|
1732 have "bv_to_int (norm_signed w) = 0" |
|
1733 by (subst ii,simp) |
|
1734 hence "bv_to_int w = 0" |
|
1735 by simp |
|
1736 with i0 |
|
1737 show False |
|
1738 by simp |
|
1739 next |
|
1740 assume ii: "norm_signed w = []" |
|
1741 assume jj: "bv_msb w \<noteq> \<zero>" |
|
1742 have "\<zero> = bv_msb (norm_signed w)" |
|
1743 by (subst ii,simp) |
|
1744 also have "... \<noteq> \<zero>" |
|
1745 by (simp add: jj) |
|
1746 finally show False by simp |
|
1747 qed |
|
1748 also have "... \<le> length w" |
|
1749 by (rule norm_signed_length) |
|
1750 finally show ?thesis |
|
1751 . |
|
1752 qed |
|
1753 |
|
1754 lemma neg_length_pos: |
|
1755 assumes i0: "bv_to_int w < -1" |
|
1756 shows "0 < length w" |
|
1757 proof - |
|
1758 from norm_signed_result [of w] |
|
1759 have "0 < length (norm_signed w)" |
|
1760 proof (auto) |
|
1761 assume ii: "norm_signed w = []" |
|
1762 have "bv_to_int (norm_signed w) = 0" |
|
1763 by (subst ii,simp) |
|
1764 hence "bv_to_int w = 0" |
|
1765 by simp |
|
1766 with i0 |
|
1767 show False |
|
1768 by simp |
|
1769 next |
|
1770 assume ii: "norm_signed w = []" |
|
1771 assume jj: "bv_msb w \<noteq> \<zero>" |
|
1772 have "\<zero> = bv_msb (norm_signed w)" |
|
1773 by (subst ii,simp) |
|
1774 also have "... \<noteq> \<zero>" |
|
1775 by (simp add: jj) |
|
1776 finally show False by simp |
|
1777 qed |
|
1778 also have "... \<le> length w" |
|
1779 by (rule norm_signed_length) |
|
1780 finally show ?thesis |
|
1781 . |
|
1782 qed |
|
1783 |
|
1784 lemma length_int_to_bv_lower_limit_gt0: |
|
1785 assumes wk: "2 ^ (k - 1) \<le> i" |
|
1786 shows "k < length (int_to_bv i)" |
|
1787 proof (rule ccontr) |
|
1788 have "0 < (2::int) ^ (k - 1)" |
|
1789 by (rule zero_less_zpower,simp) |
|
1790 also have "... \<le> i" |
|
1791 by (rule wk) |
|
1792 finally have i0: "0 < i" |
|
1793 . |
|
1794 have lii0: "0 < length (int_to_bv i)" |
|
1795 apply (rule pos_length_pos) |
|
1796 apply (simp,rule i0) |
|
1797 done |
|
1798 assume "~ k < length (int_to_bv i)" |
|
1799 hence "length (int_to_bv i) \<le> k" |
|
1800 by simp |
|
1801 with lii0 |
|
1802 have a: "length (int_to_bv i) - 1 \<le> k - 1" |
|
1803 by arith |
|
1804 have "i < 2 ^ (length (int_to_bv i) - 1)" |
|
1805 proof - |
|
1806 have "i = bv_to_int (int_to_bv i)" |
|
1807 by simp |
|
1808 also have "... < 2 ^ (length (int_to_bv i) - 1)" |
|
1809 by (rule bv_to_int_upper_range) |
|
1810 finally show ?thesis . |
|
1811 qed |
|
1812 also have "(2::int) ^ (length (int_to_bv i) - 1) \<le> 2 ^ (k - 1)" |
|
1813 apply (rule le_imp_power_zle,simp) |
|
1814 apply (rule a) |
|
1815 done |
|
1816 finally have "i < 2 ^ (k - 1)" . |
|
1817 with wk |
|
1818 show False |
|
1819 by simp |
|
1820 qed |
|
1821 |
|
1822 lemma length_int_to_bv_upper_limit_lem1: |
|
1823 assumes w1: "i < -1" |
|
1824 and wk: "- (2 ^ (k - 1)) \<le> i" |
|
1825 shows "length (int_to_bv i) \<le> k" |
|
1826 proof (rule ccontr) |
|
1827 from w1 wk |
|
1828 have k1: "1 < k" |
|
1829 by (cases "k - 1",simp_all,arith) |
|
1830 assume "~ length (int_to_bv i) \<le> k" |
|
1831 hence "k < length (int_to_bv i)" |
|
1832 by simp |
|
1833 hence "k \<le> length (int_to_bv i) - 1" |
|
1834 by arith |
|
1835 hence a: "k - 1 \<le> length (int_to_bv i) - 2" |
|
1836 by arith |
|
1837 have "i < - (2 ^ (length (int_to_bv i) - 2))" |
|
1838 proof - |
|
1839 have "i = bv_to_int (int_to_bv i)" |
|
1840 by simp |
|
1841 also have "... < - (2 ^ (length (norm_signed (int_to_bv i)) - 2))" |
|
1842 by (rule bv_to_int_upper_limit_lem1,simp,rule w1) |
|
1843 finally show ?thesis by simp |
|
1844 qed |
|
1845 also have "... \<le> -(2 ^ (k - 1))" |
|
1846 proof - |
|
1847 have "(2::int) ^ (k - 1) \<le> 2 ^ (length (int_to_bv i) - 2)" |
|
1848 apply (rule le_imp_power_zle,simp) |
|
1849 apply (rule a) |
|
1850 done |
|
1851 thus ?thesis |
|
1852 by simp |
|
1853 qed |
|
1854 finally have "i < -(2 ^ (k - 1))" . |
|
1855 with wk |
|
1856 show False |
|
1857 by simp |
|
1858 qed |
|
1859 |
|
1860 lemma length_int_to_bv_lower_limit_lem1: |
|
1861 assumes wk: "i < -(2 ^ (k - 1))" |
|
1862 shows "k < length (int_to_bv i)" |
|
1863 proof (rule ccontr) |
|
1864 from wk |
|
1865 have "i \<le> -(2 ^ (k - 1)) - 1" |
|
1866 by simp |
|
1867 also have "... < -1" |
|
1868 proof - |
|
1869 have "0 < (2::int) ^ (k - 1)" |
|
1870 by (rule zero_less_zpower,simp) |
|
1871 hence "-((2::int) ^ (k - 1)) < 0" |
|
1872 by simp |
|
1873 thus ?thesis by simp |
|
1874 qed |
|
1875 finally have i1: "i < -1" . |
|
1876 have lii0: "0 < length (int_to_bv i)" |
|
1877 apply (rule neg_length_pos) |
|
1878 apply (simp,rule i1) |
|
1879 done |
|
1880 assume "~ k < length (int_to_bv i)" |
|
1881 hence "length (int_to_bv i) \<le> k" |
|
1882 by simp |
|
1883 with lii0 |
|
1884 have a: "length (int_to_bv i) - 1 \<le> k - 1" |
|
1885 by arith |
|
1886 have "(2::int) ^ (length (int_to_bv i) - 1) \<le> 2 ^ (k - 1)" |
|
1887 apply (rule le_imp_power_zle,simp) |
|
1888 apply (rule a) |
|
1889 done |
|
1890 hence "-((2::int) ^ (k - 1)) \<le> - (2 ^ (length (int_to_bv i) - 1))" |
|
1891 by simp |
|
1892 also have "... \<le> i" |
|
1893 proof - |
|
1894 have "- (2 ^ (length (int_to_bv i) - 1)) \<le> bv_to_int (int_to_bv i)" |
|
1895 by (rule bv_to_int_lower_range) |
|
1896 also have "... = i" |
|
1897 by simp |
|
1898 finally show ?thesis . |
|
1899 qed |
|
1900 finally have "-(2 ^ (k - 1)) \<le> i" . |
|
1901 with wk |
|
1902 show False |
|
1903 by simp |
|
1904 qed |
|
1905 |
|
1906 section {* Signed Arithmetic Operations *} |
|
1907 |
|
1908 subsection {* Conversion from unsigned to signed *} |
|
1909 |
|
1910 constdefs |
|
1911 utos :: "bit list => bit list" |
|
1912 "utos w == norm_signed (\<zero> # w)" |
|
1913 |
|
1914 lemma [simp]: "utos (norm_unsigned w) = utos w" |
|
1915 by (simp add: utos_def norm_signed_Cons) |
|
1916 |
|
1917 lemma [simp]: "norm_signed (utos w) = utos w" |
|
1918 by (simp add: utos_def) |
|
1919 |
|
1920 lemma utos_length: "length (utos w) \<le> Suc (length w)" |
|
1921 by (simp add: utos_def norm_signed_Cons) |
|
1922 |
|
1923 lemma bv_to_int_utos: "bv_to_int (utos w) = bv_to_nat w" |
|
1924 proof (simp add: utos_def norm_signed_Cons,safe) |
|
1925 assume "norm_unsigned w = []" |
|
1926 hence "bv_to_nat (norm_unsigned w) = 0" |
|
1927 by simp |
|
1928 thus "bv_to_nat w = 0" |
|
1929 by simp |
|
1930 qed |
|
1931 |
|
1932 subsection {* Unary minus *} |
|
1933 |
|
1934 constdefs |
|
1935 bv_uminus :: "bit list => bit list" |
|
1936 "bv_uminus w == int_to_bv (- bv_to_int w)" |
|
1937 |
|
1938 lemma [simp]: "bv_uminus (norm_signed w) = bv_uminus w" |
|
1939 by (simp add: bv_uminus_def) |
|
1940 |
|
1941 lemma [simp]: "norm_signed (bv_uminus w) = bv_uminus w" |
|
1942 by (simp add: bv_uminus_def) |
|
1943 |
|
1944 lemma bv_uminus_length: "length (bv_uminus w) \<le> Suc (length w)" |
|
1945 proof - |
|
1946 have "1 < -bv_to_int w \<or> -bv_to_int w = 1 \<or> -bv_to_int w = 0 \<or> -bv_to_int w = -1 \<or> -bv_to_int w < -1" |
|
1947 by arith |
|
1948 thus ?thesis |
|
1949 proof safe |
|
1950 assume p: "1 < - bv_to_int w" |
|
1951 have lw: "0 < length w" |
|
1952 apply (rule neg_length_pos) |
|
1953 using p |
|
1954 apply simp |
|
1955 done |
|
1956 show ?thesis |
|
1957 proof (simp add: bv_uminus_def,rule length_int_to_bv_upper_limit_gt0,simp_all) |
|
1958 from prems |
|
1959 show "bv_to_int w < 0" |
|
1960 by simp |
|
1961 next |
|
1962 have "-(2^(length w - 1)) \<le> bv_to_int w" |
|
1963 by (rule bv_to_int_lower_range) |
|
1964 hence "- bv_to_int w \<le> 2^(length w - 1)" |
|
1965 by simp |
|
1966 also from lw have "... < 2 ^ length w" |
|
1967 by simp |
|
1968 finally show "- bv_to_int w < 2 ^ length w" |
|
1969 by simp |
|
1970 qed |
|
1971 next |
|
1972 assume p: "- bv_to_int w = 1" |
|
1973 hence lw: "0 < length w" |
|
1974 by (cases w,simp_all) |
|
1975 from p |
|
1976 show ?thesis |
|
1977 apply (simp add: bv_uminus_def) |
|
1978 using lw |
|
1979 apply (simp (no_asm) add: nat_to_bv_non0) |
|
1980 done |
|
1981 next |
|
1982 assume "- bv_to_int w = 0" |
|
1983 thus ?thesis |
|
1984 by (simp add: bv_uminus_def) |
|
1985 next |
|
1986 assume p: "- bv_to_int w = -1" |
|
1987 thus ?thesis |
|
1988 by (simp add: bv_uminus_def) |
|
1989 next |
|
1990 assume p: "- bv_to_int w < -1" |
|
1991 show ?thesis |
|
1992 apply (simp add: bv_uminus_def) |
|
1993 apply (rule length_int_to_bv_upper_limit_lem1) |
|
1994 apply (rule p) |
|
1995 apply simp |
|
1996 proof - |
|
1997 have "bv_to_int w < 2 ^ (length w - 1)" |
|
1998 by (rule bv_to_int_upper_range) |
|
1999 also have "... \<le> 2 ^ length w" |
|
2000 by (rule le_imp_power_zle,simp_all) |
|
2001 finally show "bv_to_int w \<le> 2 ^ length w" |
|
2002 by simp |
|
2003 qed |
|
2004 qed |
|
2005 qed |
|
2006 |
|
2007 lemma bv_uminus_length_utos: "length (bv_uminus (utos w)) \<le> Suc (length w)" |
|
2008 proof - |
|
2009 have "-bv_to_int (utos w) = 0 \<or> -bv_to_int (utos w) = -1 \<or> -bv_to_int (utos w) < -1" |
|
2010 apply (simp add: bv_to_int_utos) |
|
2011 apply (cut_tac bv_to_nat_lower_range [of w]) |
|
2012 by arith |
|
2013 thus ?thesis |
|
2014 proof safe |
|
2015 assume "-bv_to_int (utos w) = 0" |
|
2016 thus ?thesis |
|
2017 by (simp add: bv_uminus_def) |
|
2018 next |
|
2019 assume "-bv_to_int (utos w) = -1" |
|
2020 thus ?thesis |
|
2021 by (simp add: bv_uminus_def) |
|
2022 next |
|
2023 assume p: "-bv_to_int (utos w) < -1" |
|
2024 show ?thesis |
|
2025 apply (simp add: bv_uminus_def) |
|
2026 apply (rule length_int_to_bv_upper_limit_lem1) |
|
2027 apply (rule p) |
|
2028 apply (simp add: bv_to_int_utos) |
|
2029 using bv_to_nat_upper_range [of w] |
|
2030 apply simp |
|
2031 done |
|
2032 qed |
|
2033 qed |
|
2034 |
|
2035 constdefs |
|
2036 bv_sadd :: "[bit list, bit list ] => bit list" |
|
2037 "bv_sadd w1 w2 == int_to_bv (bv_to_int w1 + bv_to_int w2)" |
|
2038 |
|
2039 lemma [simp]: "bv_sadd (norm_signed w1) w2 = bv_sadd w1 w2" |
|
2040 by (simp add: bv_sadd_def) |
|
2041 |
|
2042 lemma [simp]: "bv_sadd w1 (norm_signed w2) = bv_sadd w1 w2" |
|
2043 by (simp add: bv_sadd_def) |
|
2044 |
|
2045 lemma [simp]: "norm_signed (bv_sadd w1 w2) = bv_sadd w1 w2" |
|
2046 by (simp add: bv_sadd_def) |
|
2047 |
|
2048 lemma adder_helper: |
|
2049 assumes lw: "0 < max (length w1) (length w2)" |
|
2050 shows "((2::int) ^ (length w1 - 1)) + (2 ^ (length w2 - 1)) \<le> 2 ^ max (length w1) (length w2)" |
|
2051 proof - |
|
2052 have "((2::int) ^ (length w1 - 1)) + (2 ^ (length w2 - 1)) \<le> 2 ^ (max (length w1) (length w2) - 1) + 2 ^ (max (length w1) (length w2) - 1)" |
|
2053 apply (cases "length w1 \<le> length w2") |
|
2054 apply (auto simp add: max_def) |
|
2055 apply arith |
|
2056 apply arith |
|
2057 done |
|
2058 also have "... = 2 ^ max (length w1) (length w2)" |
|
2059 proof - |
|
2060 from lw |
|
2061 show ?thesis |
|
2062 apply simp |
|
2063 apply (subst power_Suc [symmetric]) |
|
2064 apply (simp del: power.simps) |
|
2065 done |
|
2066 qed |
|
2067 finally show ?thesis . |
|
2068 qed |
|
2069 |
|
2070 lemma bv_sadd_length: "length (bv_sadd w1 w2) \<le> Suc (max (length w1) (length w2))" |
|
2071 proof - |
|
2072 let ?Q = "bv_to_int w1 + bv_to_int w2" |
|
2073 |
|
2074 have helper: "?Q \<noteq> 0 ==> 0 < max (length w1) (length w2)" |
|
2075 proof - |
|
2076 assume p: "?Q \<noteq> 0" |
|
2077 show "0 < max (length w1) (length w2)" |
|
2078 proof (simp add: less_max_iff_disj,rule) |
|
2079 assume [simp]: "w1 = []" |
|
2080 show "w2 \<noteq> []" |
|
2081 proof (rule ccontr,simp) |
|
2082 assume [simp]: "w2 = []" |
|
2083 from p |
|
2084 show False |
|
2085 by simp |
|
2086 qed |
|
2087 qed |
|
2088 qed |
|
2089 |
|
2090 have "0 < ?Q \<or> ?Q = 0 \<or> ?Q = -1 \<or> ?Q < -1" |
|
2091 by arith |
|
2092 thus ?thesis |
|
2093 proof safe |
|
2094 assume "?Q = 0" |
|
2095 thus ?thesis |
|
2096 by (simp add: bv_sadd_def) |
|
2097 next |
|
2098 assume "?Q = -1" |
|
2099 thus ?thesis |
|
2100 by (simp add: bv_sadd_def) |
|
2101 next |
|
2102 assume p: "0 < ?Q" |
|
2103 show ?thesis |
|
2104 apply (simp add: bv_sadd_def) |
|
2105 apply (rule length_int_to_bv_upper_limit_gt0) |
|
2106 apply (rule p) |
|
2107 proof simp |
|
2108 from bv_to_int_upper_range [of w2] |
|
2109 have "bv_to_int w2 \<le> 2 ^ (length w2 - 1)" |
|
2110 by simp |
|
2111 with bv_to_int_upper_range [of w1] |
|
2112 have "bv_to_int w1 + bv_to_int w2 < (2 ^ (length w1 - 1)) + (2 ^ (length w2 - 1))" |
|
2113 by (rule zadd_zless_mono) |
|
2114 also have "... \<le> 2 ^ max (length w1) (length w2)" |
|
2115 apply (rule adder_helper) |
|
2116 apply (rule helper) |
|
2117 using p |
|
2118 apply simp |
|
2119 done |
|
2120 finally show "?Q < 2 ^ max (length w1) (length w2)" |
|
2121 . |
|
2122 qed |
|
2123 next |
|
2124 assume p: "?Q < -1" |
|
2125 show ?thesis |
|
2126 apply (simp add: bv_sadd_def) |
|
2127 apply (rule length_int_to_bv_upper_limit_lem1,simp_all) |
|
2128 apply (rule p) |
|
2129 proof - |
|
2130 have "(2 ^ (length w1 - 1)) + 2 ^ (length w2 - 1) \<le> (2::int) ^ max (length w1) (length w2)" |
|
2131 apply (rule adder_helper) |
|
2132 apply (rule helper) |
|
2133 using p |
|
2134 apply simp |
|
2135 done |
|
2136 hence "-((2::int) ^ max (length w1) (length w2)) \<le> - (2 ^ (length w1 - 1)) + -(2 ^ (length w2 - 1))" |
|
2137 by simp |
|
2138 also have "- (2 ^ (length w1 - 1)) + -(2 ^ (length w2 - 1)) \<le> ?Q" |
|
2139 apply (rule add_mono) |
|
2140 apply (rule bv_to_int_lower_range [of w1]) |
|
2141 apply (rule bv_to_int_lower_range [of w2]) |
|
2142 done |
|
2143 finally show "- (2^max (length w1) (length w2)) \<le> ?Q" . |
|
2144 qed |
|
2145 qed |
|
2146 qed |
|
2147 |
|
2148 constdefs |
|
2149 bv_sub :: "[bit list, bit list] => bit list" |
|
2150 "bv_sub w1 w2 == bv_sadd w1 (bv_uminus w2)" |
|
2151 |
|
2152 lemma [simp]: "bv_sub (norm_signed w1) w2 = bv_sub w1 w2" |
|
2153 by (simp add: bv_sub_def) |
|
2154 |
|
2155 lemma [simp]: "bv_sub w1 (norm_signed w2) = bv_sub w1 w2" |
|
2156 by (simp add: bv_sub_def) |
|
2157 |
|
2158 lemma [simp]: "norm_signed (bv_sub w1 w2) = bv_sub w1 w2" |
|
2159 by (simp add: bv_sub_def) |
|
2160 |
|
2161 lemma bv_sub_length: "length (bv_sub w1 w2) \<le> Suc (max (length w1) (length w2))" |
|
2162 proof (cases "bv_to_int w2 = 0") |
|
2163 assume p: "bv_to_int w2 = 0" |
|
2164 show ?thesis |
|
2165 proof (simp add: bv_sub_def bv_sadd_def bv_uminus_def p) |
|
2166 have "length (norm_signed w1) \<le> length w1" |
|
2167 by (rule norm_signed_length) |
|
2168 also have "... \<le> max (length w1) (length w2)" |
|
2169 by (rule le_maxI1) |
|
2170 also have "... \<le> Suc (max (length w1) (length w2))" |
|
2171 by arith |
|
2172 finally show "length (norm_signed w1) \<le> Suc (max (length w1) (length w2))" |
|
2173 . |
|
2174 qed |
|
2175 next |
|
2176 assume "bv_to_int w2 \<noteq> 0" |
|
2177 hence "0 < length w2" |
|
2178 by (cases w2,simp_all) |
|
2179 hence lmw: "0 < max (length w1) (length w2)" |
|
2180 by arith |
|
2181 |
|
2182 let ?Q = "bv_to_int w1 - bv_to_int w2" |
|
2183 |
|
2184 have "0 < ?Q \<or> ?Q = 0 \<or> ?Q = -1 \<or> ?Q < -1" |
|
2185 by arith |
|
2186 thus ?thesis |
|
2187 proof safe |
|
2188 assume "?Q = 0" |
|
2189 thus ?thesis |
|
2190 by (simp add: bv_sub_def bv_sadd_def bv_uminus_def) |
|
2191 next |
|
2192 assume "?Q = -1" |
|
2193 thus ?thesis |
|
2194 by (simp add: bv_sub_def bv_sadd_def bv_uminus_def) |
|
2195 next |
|
2196 assume p: "0 < ?Q" |
|
2197 show ?thesis |
|
2198 apply (simp add: bv_sub_def bv_sadd_def bv_uminus_def) |
|
2199 apply (rule length_int_to_bv_upper_limit_gt0) |
|
2200 apply (rule p) |
|
2201 proof simp |
|
2202 from bv_to_int_lower_range [of w2] |
|
2203 have v2: "- bv_to_int w2 \<le> 2 ^ (length w2 - 1)" |
|
2204 by simp |
|
2205 have "bv_to_int w1 + - bv_to_int w2 < (2 ^ (length w1 - 1)) + (2 ^ (length w2 - 1))" |
|
2206 apply (rule zadd_zless_mono) |
|
2207 apply (rule bv_to_int_upper_range [of w1]) |
|
2208 apply (rule v2) |
|
2209 done |
|
2210 also have "... \<le> 2 ^ max (length w1) (length w2)" |
|
2211 apply (rule adder_helper) |
|
2212 apply (rule lmw) |
|
2213 done |
|
2214 finally show "?Q < 2 ^ max (length w1) (length w2)" |
|
2215 by simp |
|
2216 qed |
|
2217 next |
|
2218 assume p: "?Q < -1" |
|
2219 show ?thesis |
|
2220 apply (simp add: bv_sub_def bv_sadd_def bv_uminus_def) |
|
2221 apply (rule length_int_to_bv_upper_limit_lem1) |
|
2222 apply (rule p) |
|
2223 proof simp |
|
2224 have "(2 ^ (length w1 - 1)) + 2 ^ (length w2 - 1) \<le> (2::int) ^ max (length w1) (length w2)" |
|
2225 apply (rule adder_helper) |
|
2226 apply (rule lmw) |
|
2227 done |
|
2228 hence "-((2::int) ^ max (length w1) (length w2)) \<le> - (2 ^ (length w1 - 1)) + -(2 ^ (length w2 - 1))" |
|
2229 by simp |
|
2230 also have "- (2 ^ (length w1 - 1)) + -(2 ^ (length w2 - 1)) \<le> bv_to_int w1 + -bv_to_int w2" |
|
2231 apply (rule add_mono) |
|
2232 apply (rule bv_to_int_lower_range [of w1]) |
|
2233 using bv_to_int_upper_range [of w2] |
|
2234 apply simp |
|
2235 done |
|
2236 finally show "- (2^max (length w1) (length w2)) \<le> ?Q" |
|
2237 by simp |
|
2238 qed |
|
2239 qed |
|
2240 qed |
|
2241 |
|
2242 constdefs |
|
2243 bv_smult :: "[bit list, bit list] => bit list" |
|
2244 "bv_smult w1 w2 == int_to_bv (bv_to_int w1 * bv_to_int w2)" |
|
2245 |
|
2246 lemma [simp]: "bv_smult (norm_signed w1) w2 = bv_smult w1 w2" |
|
2247 by (simp add: bv_smult_def) |
|
2248 |
|
2249 lemma [simp]: "bv_smult w1 (norm_signed w2) = bv_smult w1 w2" |
|
2250 by (simp add: bv_smult_def) |
|
2251 |
|
2252 lemma [simp]: "norm_signed (bv_smult w1 w2) = bv_smult w1 w2" |
|
2253 by (simp add: bv_smult_def) |
|
2254 |
|
2255 lemma bv_smult_length: "length (bv_smult w1 w2) \<le> length w1 + length w2" |
|
2256 proof - |
|
2257 let ?Q = "bv_to_int w1 * bv_to_int w2" |
|
2258 |
|
2259 have lmw: "?Q \<noteq> 0 ==> 0 < length w1 \<and> 0 < length w2" |
|
2260 by auto |
|
2261 |
|
2262 have "0 < ?Q \<or> ?Q = 0 \<or> ?Q = -1 \<or> ?Q < -1" |
|
2263 by arith |
|
2264 thus ?thesis |
|
2265 proof (safe dest!: iffD1 [OF mult_eq_0_iff]) |
|
2266 assume "bv_to_int w1 = 0" |
|
2267 thus ?thesis |
|
2268 by (simp add: bv_smult_def) |
|
2269 next |
|
2270 assume "bv_to_int w2 = 0" |
|
2271 thus ?thesis |
|
2272 by (simp add: bv_smult_def) |
|
2273 next |
|
2274 assume p: "?Q = -1" |
|
2275 show ?thesis |
|
2276 apply (simp add: bv_smult_def p) |
|
2277 apply (cut_tac lmw) |
|
2278 apply arith |
|
2279 using p |
|
2280 apply simp |
|
2281 done |
|
2282 next |
|
2283 assume p: "0 < ?Q" |
|
2284 thus ?thesis |
|
2285 proof (simp add: zero_less_mult_iff,safe) |
|
2286 assume bi1: "0 < bv_to_int w1" |
|
2287 assume bi2: "0 < bv_to_int w2" |
|
2288 show ?thesis |
|
2289 apply (simp add: bv_smult_def) |
|
2290 apply (rule length_int_to_bv_upper_limit_gt0) |
|
2291 apply (rule p) |
|
2292 proof simp |
|
2293 have "?Q < 2 ^ (length w1 - 1) * 2 ^ (length w2 - 1)" |
|
2294 apply (rule mult_strict_mono) |
|
2295 apply (rule bv_to_int_upper_range) |
|
2296 apply (rule bv_to_int_upper_range) |
|
2297 apply (rule zero_less_zpower) |
|
2298 apply simp |
|
2299 using bi2 |
|
2300 apply simp |
|
2301 done |
|
2302 also have "... \<le> 2 ^ (length w1 + length w2 - Suc 0)" |
|
2303 apply simp |
|
2304 apply (subst zpower_zadd_distrib [symmetric]) |
|
2305 apply simp |
|
2306 apply arith |
|
2307 done |
|
2308 finally show "?Q < 2 ^ (length w1 + length w2 - Suc 0)" |
|
2309 . |
|
2310 qed |
|
2311 next |
|
2312 assume bi1: "bv_to_int w1 < 0" |
|
2313 assume bi2: "bv_to_int w2 < 0" |
|
2314 show ?thesis |
|
2315 apply (simp add: bv_smult_def) |
|
2316 apply (rule length_int_to_bv_upper_limit_gt0) |
|
2317 apply (rule p) |
|
2318 proof simp |
|
2319 have "-bv_to_int w1 * -bv_to_int w2 \<le> 2 ^ (length w1 - 1) * 2 ^(length w2 - 1)" |
|
2320 apply (rule mult_mono) |
|
2321 using bv_to_int_lower_range [of w1] |
|
2322 apply simp |
|
2323 using bv_to_int_lower_range [of w2] |
|
2324 apply simp |
|
2325 apply (rule zero_le_zpower,simp) |
|
2326 using bi2 |
|
2327 apply simp |
|
2328 done |
|
2329 hence "?Q \<le> 2 ^ (length w1 - 1) * 2 ^(length w2 - 1)" |
|
2330 by simp |
|
2331 also have "... < 2 ^ (length w1 + length w2 - Suc 0)" |
|
2332 apply simp |
|
2333 apply (subst zpower_zadd_distrib [symmetric]) |
|
2334 apply simp |
|
2335 apply (cut_tac lmw) |
|
2336 apply arith |
|
2337 apply (cut_tac p) |
|
2338 apply arith |
|
2339 done |
|
2340 finally show "?Q < 2 ^ (length w1 + length w2 - Suc 0)" . |
|
2341 qed |
|
2342 qed |
|
2343 next |
|
2344 assume p: "?Q < -1" |
|
2345 show ?thesis |
|
2346 apply (subst bv_smult_def) |
|
2347 apply (rule length_int_to_bv_upper_limit_lem1) |
|
2348 apply (rule p) |
|
2349 proof simp |
|
2350 have "(2::int) ^ (length w1 - 1) * 2 ^(length w2 - 1) \<le> 2 ^ (length w1 + length w2 - Suc 0)" |
|
2351 apply simp |
|
2352 apply (subst zpower_zadd_distrib [symmetric]) |
|
2353 apply simp |
|
2354 apply (cut_tac lmw) |
|
2355 apply arith |
|
2356 apply (cut_tac p) |
|
2357 apply arith |
|
2358 done |
|
2359 hence "-((2::int) ^ (length w1 + length w2 - Suc 0)) \<le> -(2^(length w1 - 1) * 2 ^ (length w2 - 1))" |
|
2360 by simp |
|
2361 also have "... \<le> ?Q" |
|
2362 proof - |
|
2363 from p |
|
2364 have q: "bv_to_int w1 * bv_to_int w2 < 0" |
|
2365 by simp |
|
2366 thus ?thesis |
|
2367 proof (simp add: mult_less_0_iff,safe) |
|
2368 assume bi1: "0 < bv_to_int w1" |
|
2369 assume bi2: "bv_to_int w2 < 0" |
|
2370 have "-bv_to_int w2 * bv_to_int w1 \<le> ((2::int)^(length w2 - 1)) * (2 ^ (length w1 - 1))" |
|
2371 apply (rule mult_mono) |
|
2372 using bv_to_int_lower_range [of w2] |
|
2373 apply simp |
|
2374 using bv_to_int_upper_range [of w1] |
|
2375 apply simp |
|
2376 apply (rule zero_le_zpower,simp) |
|
2377 using bi1 |
|
2378 apply simp |
|
2379 done |
|
2380 hence "-?Q \<le> ((2::int)^(length w1 - 1)) * (2 ^ (length w2 - 1))" |
|
2381 by (simp add: zmult_ac) |
|
2382 thus "-(((2::int)^(length w1 - Suc 0)) * (2 ^ (length w2 - Suc 0))) \<le> ?Q" |
|
2383 by simp |
|
2384 next |
|
2385 assume bi1: "bv_to_int w1 < 0" |
|
2386 assume bi2: "0 < bv_to_int w2" |
|
2387 have "-bv_to_int w1 * bv_to_int w2 \<le> ((2::int)^(length w1 - 1)) * (2 ^ (length w2 - 1))" |
|
2388 apply (rule mult_mono) |
|
2389 using bv_to_int_lower_range [of w1] |
|
2390 apply simp |
|
2391 using bv_to_int_upper_range [of w2] |
|
2392 apply simp |
|
2393 apply (rule zero_le_zpower,simp) |
|
2394 using bi2 |
|
2395 apply simp |
|
2396 done |
|
2397 hence "-?Q \<le> ((2::int)^(length w1 - 1)) * (2 ^ (length w2 - 1))" |
|
2398 by (simp add: zmult_ac) |
|
2399 thus "-(((2::int)^(length w1 - Suc 0)) * (2 ^ (length w2 - Suc 0))) \<le> ?Q" |
|
2400 by simp |
|
2401 qed |
|
2402 qed |
|
2403 finally show "-(2 ^ (length w1 + length w2 - Suc 0)) \<le> ?Q" |
|
2404 . |
|
2405 qed |
|
2406 qed |
|
2407 qed |
|
2408 |
|
2409 lemma bv_msb_one: "bv_msb w = \<one> ==> 0 < bv_to_nat w" |
|
2410 apply (cases w,simp_all) |
|
2411 apply (subgoal_tac "0 + 0 < 2 ^ length list + bv_to_nat list") |
|
2412 apply simp |
|
2413 apply (rule add_less_le_mono) |
|
2414 apply (rule zero_less_zpower) |
|
2415 apply simp_all |
|
2416 done |
|
2417 |
|
2418 lemma bv_smult_length_utos: "length (bv_smult (utos w1) w2) \<le> length w1 + length w2" |
|
2419 proof - |
|
2420 let ?Q = "bv_to_int (utos w1) * bv_to_int w2" |
|
2421 |
|
2422 have lmw: "?Q \<noteq> 0 ==> 0 < length (utos w1) \<and> 0 < length w2" |
|
2423 by auto |
|
2424 |
|
2425 have "0 < ?Q \<or> ?Q = 0 \<or> ?Q = -1 \<or> ?Q < -1" |
|
2426 by arith |
|
2427 thus ?thesis |
|
2428 proof (safe dest!: iffD1 [OF mult_eq_0_iff]) |
|
2429 assume "bv_to_int (utos w1) = 0" |
|
2430 thus ?thesis |
|
2431 by (simp add: bv_smult_def) |
|
2432 next |
|
2433 assume "bv_to_int w2 = 0" |
|
2434 thus ?thesis |
|
2435 by (simp add: bv_smult_def) |
|
2436 next |
|
2437 assume p: "0 < ?Q" |
|
2438 thus ?thesis |
|
2439 proof (simp add: zero_less_mult_iff,safe) |
|
2440 assume biw2: "0 < bv_to_int w2" |
|
2441 show ?thesis |
|
2442 apply (simp add: bv_smult_def) |
|
2443 apply (rule length_int_to_bv_upper_limit_gt0) |
|
2444 apply (rule p) |
|
2445 proof simp |
|
2446 have "?Q < 2 ^ length w1 * 2 ^ (length w2 - 1)" |
|
2447 apply (rule mult_strict_mono) |
|
2448 apply (simp add: bv_to_int_utos) |
|
2449 apply (rule bv_to_nat_upper_range) |
|
2450 apply (rule bv_to_int_upper_range) |
|
2451 apply (rule zero_less_zpower,simp) |
|
2452 using biw2 |
|
2453 apply simp |
|
2454 done |
|
2455 also have "... \<le> 2 ^ (length w1 + length w2 - Suc 0)" |
|
2456 apply simp |
|
2457 apply (subst zpower_zadd_distrib [symmetric]) |
|
2458 apply simp |
|
2459 apply (cut_tac lmw) |
|
2460 apply arith |
|
2461 using p |
|
2462 apply auto |
|
2463 done |
|
2464 finally show "?Q < 2 ^ (length w1 + length w2 - Suc 0)" |
|
2465 . |
|
2466 qed |
|
2467 next |
|
2468 assume "bv_to_int (utos w1) < 0" |
|
2469 thus ?thesis |
|
2470 apply (simp add: bv_to_int_utos) |
|
2471 using bv_to_nat_lower_range [of w1] |
|
2472 apply simp |
|
2473 done |
|
2474 qed |
|
2475 next |
|
2476 assume p: "?Q = -1" |
|
2477 thus ?thesis |
|
2478 apply (simp add: bv_smult_def) |
|
2479 apply (cut_tac lmw) |
|
2480 apply arith |
|
2481 apply simp |
|
2482 done |
|
2483 next |
|
2484 assume p: "?Q < -1" |
|
2485 show ?thesis |
|
2486 apply (subst bv_smult_def) |
|
2487 apply (rule length_int_to_bv_upper_limit_lem1) |
|
2488 apply (rule p) |
|
2489 proof simp |
|
2490 have "(2::int) ^ length w1 * 2 ^(length w2 - 1) \<le> 2 ^ (length w1 + length w2 - Suc 0)" |
|
2491 apply simp |
|
2492 apply (subst zpower_zadd_distrib [symmetric]) |
|
2493 apply simp |
|
2494 apply (cut_tac lmw) |
|
2495 apply arith |
|
2496 apply (cut_tac p) |
|
2497 apply arith |
|
2498 done |
|
2499 hence "-((2::int) ^ (length w1 + length w2 - Suc 0)) \<le> -(2^ length w1 * 2 ^ (length w2 - 1))" |
|
2500 by simp |
|
2501 also have "... \<le> ?Q" |
|
2502 proof - |
|
2503 from p |
|
2504 have q: "bv_to_int (utos w1) * bv_to_int w2 < 0" |
|
2505 by simp |
|
2506 thus ?thesis |
|
2507 proof (simp add: mult_less_0_iff,safe) |
|
2508 assume bi1: "0 < bv_to_int (utos w1)" |
|
2509 assume bi2: "bv_to_int w2 < 0" |
|
2510 have "-bv_to_int w2 * bv_to_int (utos w1) \<le> ((2::int)^(length w2 - 1)) * (2 ^ length w1)" |
|
2511 apply (rule mult_mono) |
|
2512 using bv_to_int_lower_range [of w2] |
|
2513 apply simp |
|
2514 apply (simp add: bv_to_int_utos) |
|
2515 using bv_to_nat_upper_range [of w1] |
|
2516 apply simp |
|
2517 apply (rule zero_le_zpower,simp) |
|
2518 using bi1 |
|
2519 apply simp |
|
2520 done |
|
2521 hence "-?Q \<le> ((2::int)^length w1) * (2 ^ (length w2 - 1))" |
|
2522 by (simp add: zmult_ac) |
|
2523 thus "-(((2::int)^length w1) * (2 ^ (length w2 - Suc 0))) \<le> ?Q" |
|
2524 by simp |
|
2525 next |
|
2526 assume bi1: "bv_to_int (utos w1) < 0" |
|
2527 thus "-(((2::int)^length w1) * (2 ^ (length w2 - Suc 0))) \<le> ?Q" |
|
2528 apply (simp add: bv_to_int_utos) |
|
2529 using bv_to_nat_lower_range [of w1] |
|
2530 apply simp |
|
2531 done |
|
2532 qed |
|
2533 qed |
|
2534 finally show "-(2 ^ (length w1 + length w2 - Suc 0)) \<le> ?Q" |
|
2535 . |
|
2536 qed |
|
2537 qed |
|
2538 qed |
|
2539 |
|
2540 lemma bv_smult_sym: "bv_smult w1 w2 = bv_smult w2 w1" |
|
2541 by (simp add: bv_smult_def zmult_ac) |
|
2542 |
|
2543 section {* Structural operations *} |
|
2544 |
|
2545 constdefs |
|
2546 bv_select :: "[bit list,nat] => bit" |
|
2547 "bv_select w i == w ! (length w - 1 - i)" |
|
2548 bv_chop :: "[bit list,nat] => bit list * bit list" |
|
2549 "bv_chop w i == let len = length w in (take (len - i) w,drop (len - i) w)" |
|
2550 bv_slice :: "[bit list,nat*nat] => bit list" |
|
2551 "bv_slice w == \<lambda>(b,e). fst (bv_chop (snd (bv_chop w (b+1))) e)" |
|
2552 |
|
2553 lemma bv_select_rev: |
|
2554 assumes notnull: "n < length w" |
|
2555 shows "bv_select w n = rev w ! n" |
|
2556 proof - |
|
2557 have "\<forall>n. n < length w --> bv_select w n = rev w ! n" |
|
2558 proof (rule length_induct [of _ w],auto simp add: bv_select_def) |
|
2559 fix xs :: "bit list" |
|
2560 fix n |
|
2561 assume ind: "\<forall>ys::bit list. length ys < length xs --> (\<forall>n. n < length ys --> ys ! (length ys - Suc n) = rev ys ! n)" |
|
2562 assume notx: "n < length xs" |
|
2563 show "xs ! (length xs - Suc n) = rev xs ! n" |
|
2564 proof (cases xs) |
|
2565 assume "xs = []" |
|
2566 with notx |
|
2567 show ?thesis |
|
2568 by simp |
|
2569 next |
|
2570 fix y ys |
|
2571 assume [simp]: "xs = y # ys" |
|
2572 show ?thesis |
|
2573 proof (auto simp add: nth_append) |
|
2574 assume noty: "n < length ys" |
|
2575 from spec [OF ind,of ys] |
|
2576 have "\<forall>n. n < length ys --> ys ! (length ys - Suc n) = rev ys ! n" |
|
2577 by simp |
|
2578 hence "n < length ys --> ys ! (length ys - Suc n) = rev ys ! n" |
|
2579 .. |
|
2580 hence "ys ! (length ys - Suc n) = rev ys ! n" |
|
2581 .. |
|
2582 thus "(y # ys) ! (length ys - n) = rev ys ! n" |
|
2583 by (simp add: nth_Cons' noty not_less_iff_le [symmetric]) |
|
2584 next |
|
2585 assume "~ n < length ys" |
|
2586 hence x: "length ys \<le> n" |
|
2587 by simp |
|
2588 from notx |
|
2589 have "n < Suc (length ys)" |
|
2590 by simp |
|
2591 hence "n \<le> length ys" |
|
2592 by simp |
|
2593 with x |
|
2594 have "length ys = n" |
|
2595 by simp |
|
2596 thus "y = [y] ! (n - length ys)" |
|
2597 by simp |
|
2598 qed |
|
2599 qed |
|
2600 qed |
|
2601 hence "n < length w --> bv_select w n = rev w ! n" |
|
2602 .. |
|
2603 thus ?thesis |
|
2604 .. |
|
2605 qed |
|
2606 |
|
2607 lemma bv_chop_append: "bv_chop (w1 @ w2) (length w2) = (w1,w2)" |
|
2608 by (simp add: bv_chop_def Let_def) |
|
2609 |
|
2610 lemma append_bv_chop_id: "fst (bv_chop w l) @ snd (bv_chop w l) = w" |
|
2611 by (simp add: bv_chop_def Let_def) |
|
2612 |
|
2613 lemma bv_chop_length_fst [simp]: "length (fst (bv_chop w i)) = length w - i" |
|
2614 by (simp add: bv_chop_def Let_def,arith) |
|
2615 |
|
2616 lemma bv_chop_length_snd [simp]: "length (snd (bv_chop w i)) = min i (length w)" |
|
2617 by (simp add: bv_chop_def Let_def,arith) |
|
2618 |
|
2619 lemma bv_slice_length [simp]: "[| j \<le> i; i < length w |] ==> length (bv_slice w (i,j)) = i - j + 1" |
|
2620 by (auto simp add: bv_slice_def,arith) |
|
2621 |
|
2622 constdefs |
|
2623 length_nat :: "int => nat" |
|
2624 "length_nat x == LEAST n. x < 2 ^ n" |
|
2625 |
|
2626 lemma length_nat: "length (nat_to_bv n) = length_nat n" |
|
2627 apply (simp add: length_nat_def) |
|
2628 apply (rule Least_equality [symmetric]) |
|
2629 prefer 2 |
|
2630 apply (rule length_nat_to_bv_upper_limit) |
|
2631 apply arith |
|
2632 apply (rule ccontr) |
|
2633 proof - |
|
2634 assume "~ n < 2 ^ length (nat_to_bv n)" |
|
2635 hence "2 ^ length (nat_to_bv n) \<le> n" |
|
2636 by simp |
|
2637 hence "length (nat_to_bv n) < length (nat_to_bv n)" |
|
2638 by (rule length_nat_to_bv_lower_limit) |
|
2639 thus False |
|
2640 by simp |
|
2641 qed |
|
2642 |
|
2643 lemma length_nat_0 [simp]: "length_nat 0 = 0" |
|
2644 by (simp add: length_nat_def Least_equality) |
|
2645 |
|
2646 lemma length_nat_non0: |
|
2647 assumes n0: "0 < n" |
|
2648 shows "length_nat n = Suc (length_nat (n div 2))" |
|
2649 apply (simp add: length_nat [symmetric]) |
|
2650 apply (subst nat_to_bv_non0 [of n]) |
|
2651 apply (simp_all add: n0) |
|
2652 done |
|
2653 |
|
2654 constdefs |
|
2655 length_int :: "int => nat" |
|
2656 "length_int x == if 0 < x then Suc (length_nat x) else if x = 0 then 0 else Suc (length_nat (-x - 1))" |
|
2657 |
|
2658 lemma length_int: "length (int_to_bv i) = length_int i" |
|
2659 proof (cases "0 < i") |
|
2660 assume i0: "0 < i" |
|
2661 hence "length (int_to_bv i) = length (norm_signed (\<zero> # norm_unsigned (nat_to_bv i)))" |
|
2662 by simp |
|
2663 also from norm_unsigned_result [of "nat_to_bv i"] |
|
2664 have "... = Suc (length_nat i)" |
|
2665 apply safe |
|
2666 apply simp |
|
2667 apply (drule norm_empty_bv_to_nat_zero) |
|
2668 using prems |
|
2669 apply simp |
|
2670 apply (cases "norm_unsigned (nat_to_bv i)") |
|
2671 apply (drule norm_empty_bv_to_nat_zero [of "nat_to_bv i"]) |
|
2672 using prems |
|
2673 apply simp |
|
2674 apply simp |
|
2675 using prems |
|
2676 apply (simp add: length_nat [symmetric]) |
|
2677 done |
|
2678 finally show ?thesis |
|
2679 using i0 |
|
2680 by (simp add: length_int_def) |
|
2681 next |
|
2682 assume "~ 0 < i" |
|
2683 hence i0: "i \<le> 0" |
|
2684 by simp |
|
2685 show ?thesis |
|
2686 proof (cases "i = 0") |
|
2687 assume "i = 0" |
|
2688 thus ?thesis |
|
2689 by (simp add: length_int_def) |
|
2690 next |
|
2691 assume "i \<noteq> 0" |
|
2692 with i0 |
|
2693 have i0: "i < 0" |
|
2694 by simp |
|
2695 hence "length (int_to_bv i) = length (norm_signed (\<one> # bv_not (norm_unsigned (nat_to_bv (- i - 1)))))" |
|
2696 by (simp add: int_to_bv_def) |
|
2697 also from norm_unsigned_result [of "nat_to_bv (- i - 1)"] |
|
2698 have "... = Suc (length_nat (- i - 1))" |
|
2699 apply safe |
|
2700 apply simp |
|
2701 apply (drule norm_empty_bv_to_nat_zero [of "nat_to_bv (-i - 1)"]) |
|
2702 using prems |
|
2703 apply simp |
|
2704 apply (cases "- i - 1 = 0") |
|
2705 apply simp |
|
2706 apply (simp add: length_nat [symmetric]) |
|
2707 apply (cases "norm_unsigned (nat_to_bv (- i - 1))") |
|
2708 apply simp |
|
2709 apply simp |
|
2710 using prems |
|
2711 apply (simp add: length_nat [symmetric]) |
|
2712 done |
|
2713 finally |
|
2714 show ?thesis |
|
2715 using i0 |
|
2716 by (simp add: length_int_def) |
|
2717 qed |
|
2718 qed |
|
2719 |
|
2720 lemma length_int_0 [simp]: "length_int 0 = 0" |
|
2721 by (simp add: length_int_def) |
|
2722 |
|
2723 lemma length_int_gt0: "0 < i ==> length_int i = Suc (length_nat i)" |
|
2724 by (simp add: length_int_def) |
|
2725 |
|
2726 lemma length_int_lt0: "i < 0 ==> length_int i = Suc (length_nat (- i - 1))" |
|
2727 by (simp add: length_int_def) |
|
2728 |
|
2729 lemma bv_chopI: "[| w = w1 @ w2 ; i = length w2 |] ==> bv_chop w i = (w1,w2)" |
|
2730 by (simp add: bv_chop_def Let_def) |
|
2731 |
|
2732 lemma bv_sliceI: "[| j \<le> i ; i < length w ; w = w1 @ w2 @ w3 ; Suc i = length w2 + j ; j = length w3 |] ==> bv_slice w (i,j) = w2" |
|
2733 apply (simp add: bv_slice_def) |
|
2734 apply (subst bv_chopI [of "w1 @ w2 @ w3" w1 "w2 @ w3"]) |
|
2735 apply simp |
|
2736 apply simp |
|
2737 apply simp |
|
2738 apply (subst bv_chopI [of "w2 @ w3" w2 w3],simp_all) |
|
2739 done |
|
2740 |
|
2741 lemma bv_slice_bv_slice: |
|
2742 assumes ki: "k \<le> i" |
|
2743 and ij: "i \<le> j" |
|
2744 and jl: "j \<le> l" |
|
2745 and lw: "l < length w" |
|
2746 shows "bv_slice w (j,i) = bv_slice (bv_slice w (l,k)) (j-k,i-k)" |
|
2747 proof - |
|
2748 def w1 == "fst (bv_chop w (Suc l))" |
|
2749 def w2 == "fst (bv_chop (snd (bv_chop w (Suc l))) (Suc j))" |
|
2750 def w3 == "fst (bv_chop (snd (bv_chop (snd (bv_chop w (Suc l))) (Suc j))) i)" |
|
2751 def w4 == "fst (bv_chop (snd (bv_chop (snd (bv_chop (snd (bv_chop w (Suc l))) (Suc j))) i)) k)" |
|
2752 def w5 == "snd (bv_chop (snd (bv_chop (snd (bv_chop (snd (bv_chop w (Suc l))) (Suc j))) i)) k)" |
|
2753 |
|
2754 note w_defs = w1_def w2_def w3_def w4_def w5_def |
|
2755 |
|
2756 have w_def: "w = w1 @ w2 @ w3 @ w4 @ w5" |
|
2757 by (simp add: w_defs append_bv_chop_id) |
|
2758 |
|
2759 from ki ij jl lw |
|
2760 show ?thesis |
|
2761 apply (subst bv_sliceI [where ?j = i and ?i = j and ?w = w and ?w1.0 = "w1 @ w2" and ?w2.0 = w3 and ?w3.0 = "w4 @ w5"]) |
|
2762 apply simp_all |
|
2763 apply (rule w_def) |
|
2764 apply (simp add: w_defs min_def) |
|
2765 apply (simp add: w_defs min_def) |
|
2766 apply (subst bv_sliceI [where ?j = k and ?i = l and ?w = w and ?w1.0 = w1 and ?w2.0 = "w2 @ w3 @ w4" and ?w3.0 = w5]) |
|
2767 apply simp_all |
|
2768 apply (rule w_def) |
|
2769 apply (simp add: w_defs min_def) |
|
2770 apply (simp add: w_defs min_def) |
|
2771 apply (subst bv_sliceI [where ?j = "i-k" and ?i = "j-k" and ?w = "w2 @ w3 @ w4" and ?w1.0 = w2 and ?w2.0 = w3 and ?w3.0 = w4]) |
|
2772 apply simp_all |
|
2773 apply (simp_all add: w_defs min_def) |
|
2774 apply arith+ |
|
2775 done |
|
2776 qed |
|
2777 |
|
2778 lemma bv_to_nat_extend [simp]: "bv_to_nat (bv_extend n \<zero> w) = bv_to_nat w" |
|
2779 apply (simp add: bv_extend_def) |
|
2780 apply (subst bv_to_nat_dist_append) |
|
2781 apply simp |
|
2782 apply (induct "n - length w",simp_all) |
|
2783 done |
|
2784 |
|
2785 lemma bv_msb_extend_same [simp]: "bv_msb w = b ==> bv_msb (bv_extend n b w) = b" |
|
2786 apply (simp add: bv_extend_def) |
|
2787 apply (induct "n - length w",simp_all) |
|
2788 done |
|
2789 |
|
2790 lemma bv_to_int_extend [simp]: |
|
2791 assumes a: "bv_msb w = b" |
|
2792 shows "bv_to_int (bv_extend n b w) = bv_to_int w" |
|
2793 proof (cases "bv_msb w") |
|
2794 assume [simp]: "bv_msb w = \<zero>" |
|
2795 with a have [simp]: "b = \<zero>" |
|
2796 by simp |
|
2797 show ?thesis |
|
2798 by (simp add: bv_to_int_def) |
|
2799 next |
|
2800 assume [simp]: "bv_msb w = \<one>" |
|
2801 with a have [simp]: "b = \<one>" |
|
2802 by simp |
|
2803 show ?thesis |
|
2804 apply (simp add: bv_to_int_def) |
|
2805 apply (simp add: bv_extend_def) |
|
2806 apply (induct "n - length w",simp_all) |
|
2807 done |
|
2808 qed |
|
2809 |
|
2810 lemma length_nat_mono [simp]: "x \<le> y ==> length_nat x \<le> length_nat y" |
|
2811 proof (rule ccontr) |
|
2812 assume xy: "x \<le> y" |
|
2813 assume "~ length_nat x \<le> length_nat y" |
|
2814 hence lxly: "length_nat y < length_nat x" |
|
2815 by simp |
|
2816 hence "length_nat y < (LEAST n. x < 2 ^ n)" |
|
2817 by (simp add: length_nat_def) |
|
2818 hence "~ x < 2 ^ length_nat y" |
|
2819 by (rule not_less_Least) |
|
2820 hence xx: "2 ^ length_nat y \<le> x" |
|
2821 by simp |
|
2822 have yy: "y < 2 ^ length_nat y" |
|
2823 apply (simp add: length_nat_def) |
|
2824 apply (rule LeastI) |
|
2825 apply (subgoal_tac "y < 2 ^ (nat y)",assumption) |
|
2826 apply (cases "0 \<le> y") |
|
2827 apply (subgoal_tac "int (nat y) < int (2 ^ nat y)") |
|
2828 apply (simp add: int_nat_two_exp) |
|
2829 apply (induct "nat y",simp_all) |
|
2830 done |
|
2831 with xx |
|
2832 have "y < x" by simp |
|
2833 with xy |
|
2834 show False |
|
2835 by simp |
|
2836 qed |
|
2837 |
|
2838 lemma length_nat_mono_int [simp]: "x \<le> y ==> length_nat x \<le> length_nat y" |
|
2839 apply (rule length_nat_mono) |
|
2840 apply arith |
|
2841 done |
|
2842 |
|
2843 lemma length_nat_pos [simp,intro!]: "0 < x ==> 0 < length_nat x" |
|
2844 by (simp add: length_nat_non0) |
|
2845 |
|
2846 lemma length_int_mono_gt0: "[| 0 \<le> x ; x \<le> y |] ==> length_int x \<le> length_int y" |
|
2847 by (cases "x = 0",simp_all add: length_int_gt0) |
|
2848 |
|
2849 lemma length_int_mono_lt0: "[| x \<le> y ; y \<le> 0 |] ==> length_int y \<le> length_int x" |
|
2850 by (cases "y = 0",simp_all add: length_int_lt0) |
|
2851 |
|
2852 lemmas [simp] = length_nat_non0 |
|
2853 |
|
2854 lemma "nat_to_bv (number_of bin.Pls) = []" |
|
2855 by simp |
|
2856 |
|
2857 consts |
|
2858 fast_nat_to_bv_helper :: "bin => bit list => bit list" |
|
2859 |
|
2860 primrec |
|
2861 fast_nat_to_bv_Pls: "fast_nat_to_bv_helper bin.Pls res = res" |
|
2862 fast_nat_to_bv_Bit: "fast_nat_to_bv_helper (w BIT b) res = fast_nat_to_bv_helper w ((if b then \<one> else \<zero>) # res)" |
|
2863 |
|
2864 lemma fast_nat_to_bv_def: |
|
2865 assumes pos_w: "(0::int) \<le> number_of w" |
|
2866 shows "nat_to_bv (number_of w) == norm_unsigned (fast_nat_to_bv_helper w [])" |
|
2867 proof - |
|
2868 have h [rule_format]: "(0::int) \<le> number_of w ==> \<forall> l. norm_unsigned (nat_to_bv_helper (number_of w) l) = norm_unsigned (fast_nat_to_bv_helper w l)" |
|
2869 proof (induct w,simp add: nat_to_bv_helper.simps,simp) |
|
2870 fix bin b |
|
2871 assume ind: "(0::int) \<le> number_of bin ==> \<forall> l. norm_unsigned (nat_to_bv_helper (number_of bin) l) = norm_unsigned (fast_nat_to_bv_helper bin l)" |
|
2872 def qq == "number_of bin::int" |
|
2873 assume posbb: "(0::int) \<le> number_of (bin BIT b)" |
|
2874 hence indq [rule_format]: "\<forall> l. norm_unsigned (nat_to_bv_helper qq l) = norm_unsigned (fast_nat_to_bv_helper bin l)" |
|
2875 apply (unfold qq_def) |
|
2876 apply (rule ind) |
|
2877 apply simp |
|
2878 done |
|
2879 from posbb |
|
2880 have "0 \<le> qq" |
|
2881 by (simp add: qq_def) |
|
2882 with posbb |
|
2883 show "\<forall> l. norm_unsigned (nat_to_bv_helper (number_of (bin BIT b)) l) = norm_unsigned (fast_nat_to_bv_helper (bin BIT b) l)" |
|
2884 apply (subst pos_number_of,simp) |
|
2885 apply safe |
|
2886 apply (fold qq_def) |
|
2887 apply (cases "qq = 0") |
|
2888 apply (simp add: nat_to_bv_helper.simps) |
|
2889 apply (subst indq [symmetric]) |
|
2890 apply (subst indq [symmetric]) |
|
2891 apply (simp add: nat_to_bv_helper.simps) |
|
2892 apply (subgoal_tac "0 < qq") |
|
2893 prefer 2 |
|
2894 apply simp |
|
2895 apply simp |
|
2896 apply (subst indq [symmetric]) |
|
2897 apply (subst indq [symmetric]) |
|
2898 apply auto |
|
2899 apply (subst nat_to_bv_helper.simps [of "2 * qq + 1"]) |
|
2900 apply simp |
|
2901 apply safe |
|
2902 apply (subgoal_tac "2 * qq + 1 ~= 2 * q") |
|
2903 apply simp |
|
2904 apply arith |
|
2905 apply (subgoal_tac "(2 * qq + 1) div 2 = qq") |
|
2906 apply simp |
|
2907 apply (subst zdiv_zadd1_eq,simp) |
|
2908 apply (subst nat_to_bv_helper.simps [of "2 * qq"]) |
|
2909 apply simp |
|
2910 done |
|
2911 qed |
|
2912 from pos_w |
|
2913 have "nat_to_bv (number_of w) = norm_unsigned (nat_to_bv (number_of w))" |
|
2914 by simp |
|
2915 also have "... = norm_unsigned (fast_nat_to_bv_helper w [])" |
|
2916 apply (unfold nat_to_bv_def) |
|
2917 apply (rule h) |
|
2918 apply (rule pos_w) |
|
2919 done |
|
2920 finally show "nat_to_bv (number_of w) == norm_unsigned (fast_nat_to_bv_helper w [])" |
|
2921 by simp |
|
2922 qed |
|
2923 |
|
2924 lemma fast_nat_to_bv_Bit0: "fast_nat_to_bv_helper (w BIT False) res = fast_nat_to_bv_helper w (\<zero> # res)" |
|
2925 by simp |
|
2926 |
|
2927 lemma fast_nat_to_bv_Bit1: "fast_nat_to_bv_helper (w BIT True) res = fast_nat_to_bv_helper w (\<one> # res)" |
|
2928 by simp |
|
2929 |
|
2930 declare fast_nat_to_bv_Bit [simp del] |
|
2931 declare fast_nat_to_bv_Bit0 [simp] |
|
2932 declare fast_nat_to_bv_Bit1 [simp] |
|
2933 |
|
2934 consts |
|
2935 fast_bv_to_nat_helper :: "[bit list, bin] => bin" |
|
2936 |
|
2937 primrec |
|
2938 fast_bv_to_nat_Nil: "fast_bv_to_nat_helper [] bin = bin" |
|
2939 fast_bv_to_nat_Cons: "fast_bv_to_nat_helper (b#bs) bin = fast_bv_to_nat_helper bs (bin BIT (bit_case False True b))" |
|
2940 |
|
2941 lemma fast_bv_to_nat_Cons0: "fast_bv_to_nat_helper (\<zero>#bs) bin = fast_bv_to_nat_helper bs (bin BIT False)" |
|
2942 by simp |
|
2943 |
|
2944 lemma fast_bv_to_nat_Cons1: "fast_bv_to_nat_helper (\<one>#bs) bin = fast_bv_to_nat_helper bs (bin BIT True)" |
|
2945 by simp |
|
2946 |
|
2947 lemma fast_bv_to_nat_def: "bv_to_nat bs == number_of (fast_bv_to_nat_helper bs bin.Pls)" |
|
2948 proof (simp add: bv_to_nat_def) |
|
2949 have "\<forall> bin. (foldl (%bn b. bn BIT (b = \<one>)) bin bs) = (fast_bv_to_nat_helper bs bin)" |
|
2950 apply (induct bs,simp) |
|
2951 apply (case_tac a,simp_all) |
|
2952 done |
|
2953 thus "number_of (foldl (%bn b. bn BIT (b = \<one>)) bin.Pls bs) == number_of (fast_bv_to_nat_helper bs bin.Pls)::int" |
|
2954 by simp |
|
2955 qed |
|
2956 |
|
2957 declare fast_bv_to_nat_Cons [simp del] |
|
2958 declare fast_bv_to_nat_Cons0 [simp] |
|
2959 declare fast_bv_to_nat_Cons1 [simp] |
|
2960 |
|
2961 setup setup_word |
|
2962 |
|
2963 declare bv_to_nat1 [simp del] |
|
2964 declare bv_to_nat_helper [simp del] |
|
2965 |
|
2966 constdefs |
|
2967 bv_mapzip :: "[bit => bit => bit,bit list, bit list] => bit list" |
|
2968 "bv_mapzip f w1 w2 == let g = bv_extend (max (length w1) (length w2)) \<zero> |
|
2969 in map (split f) (zip (g w1) (g w2))" |
|
2970 |
|
2971 lemma bv_length_bv_mapzip [simp]: "length (bv_mapzip f w1 w2) = max (length w1) (length w2)" |
|
2972 by (simp add: bv_mapzip_def Let_def split: split_max) |
|
2973 |
|
2974 lemma [simp]: "bv_mapzip f [] [] = []" |
|
2975 by (simp add: bv_mapzip_def Let_def) |
|
2976 |
|
2977 lemma [simp]: "length w1 = length w2 ==> bv_mapzip f (x#w1) (y#w2) = f x y # bv_mapzip f w1 w2" |
|
2978 by (simp add: bv_mapzip_def Let_def) |
|
2979 |
|
2980 lemma [code]: "bv_to_nat bs = list_rec (0::int) (\<lambda>b bs n. bitval b * 2 ^ length bs + n) bs" |
|
2981 by (induct bs,simp_all add: bv_to_nat_helper) |
|
2982 |
|
2983 text {* The following can be added for speedup, but depends on the |
|
2984 exact definition of division and modulo of the ML compiler for soundness. *} |
|
2985 |
|
2986 (* |
|
2987 consts_code "op div" ("'('(_') div '(_')')") |
|
2988 consts_code "op mod" ("'('(_') mod '(_')')") |
|
2989 *) |
|
2990 |
|
2991 end |