18 fixes x :: "'a::linorder" |
18 fixes x :: "'a::linorder" |
19 assumes mf: "mono f" |
19 assumes mf: "mono f" |
20 shows "max (f x) (f y) \<le> f (max x y)" |
20 shows "max (f x) (f y) \<le> f (max x y)" |
21 proof - |
21 proof - |
22 from mf and le_maxI1 [of x y] |
22 from mf and le_maxI1 [of x y] |
23 have fx: "f x \<le> f (max x y)" |
23 have fx: "f x \<le> f (max x y)" by (rule monoD) |
24 by (rule monoD) |
|
25 from mf and le_maxI2 [of y x] |
24 from mf and le_maxI2 [of y x] |
26 have fy: "f y \<le> f (max x y)" |
25 have fy: "f y \<le> f (max x y)" by (rule monoD) |
27 by (rule monoD) |
|
28 from fx and fy |
26 from fx and fy |
29 show "max (f x) (f y) \<le> f (max x y)" |
27 show "max (f x) (f y) \<le> f (max x y)" by auto |
30 by auto |
|
31 qed |
28 qed |
32 |
29 |
33 declare zero_le_power [intro] |
30 declare zero_le_power [intro] |
34 and zero_less_power [intro] |
31 and zero_less_power [intro] |
35 |
32 |
36 lemma int_nat_two_exp: "2 ^ k = int (2 ^ k)" |
33 lemma int_nat_two_exp: "2 ^ k = int (2 ^ k)" |
37 by (simp add: zpower_int [symmetric]) |
34 by (simp add: zpower_int [symmetric]) |
38 |
35 |
|
36 |
39 subsection {* Bits *} |
37 subsection {* Bits *} |
40 |
38 |
41 datatype bit |
39 datatype bit = |
42 = Zero ("\<zero>") |
40 Zero ("\<zero>") |
43 | One ("\<one>") |
41 | One ("\<one>") |
44 |
42 |
45 consts |
43 consts |
46 bitval :: "bit => nat" |
44 bitval :: "bit => nat" |
47 |
|
48 primrec |
45 primrec |
49 "bitval \<zero> = 0" |
46 "bitval \<zero> = 0" |
50 "bitval \<one> = 1" |
47 "bitval \<one> = 1" |
51 |
48 |
52 consts |
49 consts |
105 and zero: "!!bs. w = \<zero> # bs ==> P w" |
103 and zero: "!!bs. w = \<zero> # bs ==> P w" |
106 and one: "!!bs. w = \<one> # bs ==> P w" |
104 and one: "!!bs. w = \<one> # bs ==> P w" |
107 shows "P w" |
105 shows "P w" |
108 proof (cases w) |
106 proof (cases w) |
109 assume "w = []" |
107 assume "w = []" |
110 thus ?thesis |
108 thus ?thesis by (rule empty) |
111 by (rule empty) |
|
112 next |
109 next |
113 fix b bs |
110 fix b bs |
114 assume [simp]: "w = b # bs" |
111 assume [simp]: "w = b # bs" |
115 show "P w" |
112 show "P w" |
116 proof (cases b) |
113 proof (cases b) |
117 assume "b = \<zero>" |
114 assume "b = \<zero>" |
118 hence "w = \<zero> # bs" |
115 hence "w = \<zero> # bs" by simp |
119 by simp |
116 thus ?thesis by (rule zero) |
120 thus ?thesis |
|
121 by (rule zero) |
|
122 next |
117 next |
123 assume "b = \<one>" |
118 assume "b = \<one>" |
124 hence "w = \<one> # bs" |
119 hence "w = \<one> # bs" by simp |
125 by simp |
120 thus ?thesis by (rule one) |
126 thus ?thesis |
|
127 by (rule one) |
|
128 qed |
121 qed |
129 qed |
122 qed |
130 |
123 |
131 lemma bit_list_induct: |
124 lemma bit_list_induct: |
132 assumes empty: "P []" |
125 assumes empty: "P []" |
133 and zero: "!!bs. P bs ==> P (\<zero>#bs)" |
126 and zero: "!!bs. P bs ==> P (\<zero>#bs)" |
134 and one: "!!bs. P bs ==> P (\<one>#bs)" |
127 and one: "!!bs. P bs ==> P (\<one>#bs)" |
135 shows "P w" |
128 shows "P w" |
136 proof (induct w,simp_all add: empty) |
129 proof (induct w, simp_all add: empty) |
137 fix b bs |
130 fix b bs |
138 assume [intro!]: "P bs" |
131 assume "P bs" |
139 show "P (b#bs)" |
132 then show "P (b#bs)" |
140 by (cases b,auto intro!: zero one) |
133 by (cases b) (auto intro!: zero one) |
141 qed |
134 qed |
142 |
135 |
143 definition |
136 definition |
144 bv_msb :: "bit list => bit" where |
137 bv_msb :: "bit list => bit" where |
145 "bv_msb w = (if w = [] then \<zero> else hd w)" |
138 "bv_msb w = (if w = [] then \<zero> else hd w)" |
160 |
153 |
161 lemma bv_not_Cons [simp]: "bv_not (b#bs) = (bitnot b) # bv_not bs" |
154 lemma bv_not_Cons [simp]: "bv_not (b#bs) = (bitnot b) # bv_not bs" |
162 by (simp add: bv_not_def) |
155 by (simp add: bv_not_def) |
163 |
156 |
164 lemma bv_not_bv_not [simp]: "bv_not (bv_not w) = w" |
157 lemma bv_not_bv_not [simp]: "bv_not (bv_not w) = w" |
165 by (rule bit_list_induct [of _ w],simp_all) |
158 by (rule bit_list_induct [of _ w]) simp_all |
166 |
159 |
167 lemma bv_msb_Nil [simp]: "bv_msb [] = \<zero>" |
160 lemma bv_msb_Nil [simp]: "bv_msb [] = \<zero>" |
168 by (simp add: bv_msb_def) |
161 by (simp add: bv_msb_def) |
169 |
162 |
170 lemma bv_msb_Cons [simp]: "bv_msb (b#bs) = b" |
163 lemma bv_msb_Cons [simp]: "bv_msb (b#bs) = b" |
171 by (simp add: bv_msb_def) |
164 by (simp add: bv_msb_def) |
172 |
165 |
173 lemma bv_msb_bv_not [simp]: "0 < length w ==> bv_msb (bv_not w) = (bitnot (bv_msb w))" |
166 lemma bv_msb_bv_not [simp]: "0 < length w ==> bv_msb (bv_not w) = (bitnot (bv_msb w))" |
174 by (cases w,simp_all) |
167 by (cases w) simp_all |
175 |
168 |
176 lemma bv_msb_one_length [simp,intro]: "bv_msb w = \<one> ==> 0 < length w" |
169 lemma bv_msb_one_length [simp,intro]: "bv_msb w = \<one> ==> 0 < length w" |
177 by (cases w,simp_all) |
170 by (cases w) simp_all |
178 |
171 |
179 lemma length_bv_not [simp]: "length (bv_not w) = length w" |
172 lemma length_bv_not [simp]: "length (bv_not w) = length w" |
180 by (induct w,simp_all) |
173 by (induct w) simp_all |
181 |
174 |
182 definition |
175 definition |
183 bv_to_nat :: "bit list => nat" where |
176 bv_to_nat :: "bit list => nat" where |
184 "bv_to_nat = foldl (%bn b. 2 * bn + bitval b) 0" |
177 "bv_to_nat = foldl (%bn b. 2 * bn + bitval b) 0" |
185 |
178 |
210 |
204 |
211 lemma bv_to_nat1 [simp]: "bv_to_nat (\<one>#bs) = 2 ^ length bs + bv_to_nat bs" |
205 lemma bv_to_nat1 [simp]: "bv_to_nat (\<one>#bs) = 2 ^ length bs + bv_to_nat bs" |
212 by simp |
206 by simp |
213 |
207 |
214 lemma bv_to_nat_upper_range: "bv_to_nat w < 2 ^ length w" |
208 lemma bv_to_nat_upper_range: "bv_to_nat w < 2 ^ length w" |
215 proof (induct w,simp_all) |
209 proof (induct w, simp_all) |
216 fix b bs |
210 fix b bs |
217 assume "bv_to_nat bs < 2 ^ length bs" |
211 assume "bv_to_nat bs < 2 ^ length bs" |
218 show "bitval b * 2 ^ length bs + bv_to_nat bs < 2 * 2 ^ length bs" |
212 show "bitval b * 2 ^ length bs + bv_to_nat bs < 2 * 2 ^ length bs" |
219 proof (cases b,simp_all) |
213 proof (cases b, simp_all) |
220 have "bv_to_nat bs < 2 ^ length bs" |
214 have "bv_to_nat bs < 2 ^ length bs" by fact |
221 . |
215 also have "... < 2 * 2 ^ length bs" by auto |
222 also have "... < 2 * 2 ^ length bs" |
216 finally show "bv_to_nat bs < 2 * 2 ^ length bs" by simp |
223 by auto |
217 next |
224 finally show "bv_to_nat bs < 2 * 2 ^ length bs" |
218 have "bv_to_nat bs < 2 ^ length bs" by fact |
225 by simp |
219 hence "2 ^ length bs + bv_to_nat bs < 2 ^ length bs + 2 ^ length bs" by arith |
226 next |
220 also have "... = 2 * (2 ^ length bs)" by simp |
227 have "bv_to_nat bs < 2 ^ length bs" |
221 finally show "bv_to_nat bs < 2 ^ length bs" by simp |
228 . |
|
229 hence "2 ^ length bs + bv_to_nat bs < 2 ^ length bs + 2 ^ length bs" |
|
230 by arith |
|
231 also have "... = 2 * (2 ^ length bs)" |
|
232 by simp |
|
233 finally show "bv_to_nat bs < 2 ^ length bs" |
|
234 by simp |
|
235 qed |
222 qed |
236 qed |
223 qed |
237 |
224 |
238 lemma bv_extend_longer [simp]: |
225 lemma bv_extend_longer [simp]: |
239 assumes wn: "n \<le> length w" |
226 assumes wn: "n \<le> length w" |
248 have s: "n - Suc (length w) + 1 = n - length w" |
235 have s: "n - Suc (length w) + 1 = n - length w" |
249 by arith |
236 by arith |
250 have "bv_extend n b w = replicate (n - length w) b @ w" |
237 have "bv_extend n b w = replicate (n - length w) b @ w" |
251 by (simp add: bv_extend_def) |
238 by (simp add: bv_extend_def) |
252 also have "... = replicate (n - Suc (length w) + 1) b @ w" |
239 also have "... = replicate (n - Suc (length w) + 1) b @ w" |
253 by (subst s,rule) |
240 by (subst s) rule |
254 also have "... = (replicate (n - Suc (length w)) b @ replicate 1 b) @ w" |
241 also have "... = (replicate (n - Suc (length w)) b @ replicate 1 b) @ w" |
255 by (subst replicate_add,rule) |
242 by (subst replicate_add) rule |
256 also have "... = replicate (n - Suc (length w)) b @ b # w" |
243 also have "... = replicate (n - Suc (length w)) b @ b # w" |
257 by simp |
244 by simp |
258 also have "... = bv_extend n b (b#w)" |
245 also have "... = bv_extend n b (b#w)" |
259 by (simp add: bv_extend_def) |
246 by (simp add: bv_extend_def) |
260 finally show "bv_extend n b w = bv_extend n b (b#w)" |
247 finally show "bv_extend n b w = bv_extend n b (b#w)" . |
261 . |
|
262 qed |
248 qed |
263 |
249 |
264 consts |
250 consts |
265 rem_initial :: "bit => bit list => bit list" |
251 rem_initial :: "bit => bit list => bit list" |
266 |
|
267 primrec |
252 primrec |
268 "rem_initial b [] = []" |
253 "rem_initial b [] = []" |
269 "rem_initial b (x#xs) = (if b = x then rem_initial b xs else x#xs)" |
254 "rem_initial b (x#xs) = (if b = x then rem_initial b xs else x#xs)" |
270 |
255 |
271 lemma rem_initial_length: "length (rem_initial b w) \<le> length w" |
256 lemma rem_initial_length: "length (rem_initial b w) \<le> length w" |
274 lemma rem_initial_equal: |
259 lemma rem_initial_equal: |
275 assumes p: "length (rem_initial b w) = length w" |
260 assumes p: "length (rem_initial b w) = length w" |
276 shows "rem_initial b w = w" |
261 shows "rem_initial b w = w" |
277 proof - |
262 proof - |
278 have "length (rem_initial b w) = length w --> rem_initial b w = w" |
263 have "length (rem_initial b w) = length w --> rem_initial b w = w" |
279 proof (induct w,simp_all,clarify) |
264 proof (induct w, simp_all, clarify) |
280 fix xs |
265 fix xs |
281 assume "length (rem_initial b xs) = length xs --> rem_initial b xs = xs" |
266 assume "length (rem_initial b xs) = length xs --> rem_initial b xs = xs" |
282 assume f: "length (rem_initial b xs) = Suc (length xs)" |
267 assume f: "length (rem_initial b xs) = Suc (length xs)" |
283 with rem_initial_length [of b xs] |
268 with rem_initial_length [of b xs] |
284 show "rem_initial b xs = b#xs" |
269 show "rem_initial b xs = b#xs" |
285 by auto |
270 by auto |
286 qed |
271 qed |
287 thus ?thesis |
272 from this and p show ?thesis .. |
288 .. |
|
289 qed |
273 qed |
290 |
274 |
291 lemma bv_extend_rem_initial: "bv_extend (length w) b (rem_initial b w) = w" |
275 lemma bv_extend_rem_initial: "bv_extend (length w) b (rem_initial b w) = w" |
292 proof (induct w,simp_all,safe) |
276 proof (induct w, simp_all, safe) |
293 fix xs |
277 fix xs |
294 assume ind: "bv_extend (length xs) b (rem_initial b xs) = xs" |
278 assume ind: "bv_extend (length xs) b (rem_initial b xs) = xs" |
295 from rem_initial_length [of b xs] |
279 from rem_initial_length [of b xs] |
296 have [simp]: "Suc (length xs) - length (rem_initial b xs) = 1 + (length xs - length (rem_initial b xs))" |
280 have [simp]: "Suc (length xs) - length (rem_initial b xs) = |
|
281 1 + (length xs - length (rem_initial b xs))" |
297 by arith |
282 by arith |
298 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)" |
283 have "bv_extend (Suc (length xs)) b (rem_initial b xs) = |
|
284 replicate (Suc (length xs) - length (rem_initial b xs)) b @ (rem_initial b xs)" |
299 by (simp add: bv_extend_def) |
285 by (simp add: bv_extend_def) |
300 also have "... = replicate (1 + (length xs - length (rem_initial b xs))) b @ rem_initial b xs" |
286 also have "... = |
|
287 replicate (1 + (length xs - length (rem_initial b xs))) b @ rem_initial b xs" |
301 by simp |
288 by simp |
302 also have "... = (replicate 1 b @ replicate (length xs - length (rem_initial b xs)) b) @ rem_initial b xs" |
289 also have "... = |
303 by (subst replicate_add,rule refl) |
290 (replicate 1 b @ replicate (length xs - length (rem_initial b xs)) b) @ rem_initial b xs" |
|
291 by (subst replicate_add) (rule refl) |
304 also have "... = b # bv_extend (length xs) b (rem_initial b xs)" |
292 also have "... = b # bv_extend (length xs) b (rem_initial b xs)" |
305 by (auto simp add: bv_extend_def [symmetric]) |
293 by (auto simp add: bv_extend_def [symmetric]) |
306 also have "... = b # xs" |
294 also have "... = b # xs" |
307 by (simp add: ind) |
295 by (simp add: ind) |
308 finally show "bv_extend (Suc (length xs)) b (rem_initial b xs) = b # xs" |
296 finally show "bv_extend (Suc (length xs)) b (rem_initial b xs) = b # xs" . |
309 . |
|
310 qed |
297 qed |
311 |
298 |
312 lemma rem_initial_append1: |
299 lemma rem_initial_append1: |
313 assumes "rem_initial b xs ~= []" |
300 assumes "rem_initial b xs ~= []" |
314 shows "rem_initial b (xs @ ys) = rem_initial b xs @ ys" |
301 shows "rem_initial b (xs @ ys) = rem_initial b xs @ ys" |
315 proof - |
302 using assms by (induct xs) auto |
316 have "rem_initial b xs ~= [] --> rem_initial b (xs @ ys) = rem_initial b xs @ ys" (is "?P xs ys") |
|
317 by (induct xs,auto) |
|
318 thus ?thesis |
|
319 .. |
|
320 qed |
|
321 |
303 |
322 lemma rem_initial_append2: |
304 lemma rem_initial_append2: |
323 assumes "rem_initial b xs = []" |
305 assumes "rem_initial b xs = []" |
324 shows "rem_initial b (xs @ ys) = rem_initial b ys" |
306 shows "rem_initial b (xs @ ys) = rem_initial b ys" |
325 proof - |
307 using assms by (induct xs) auto |
326 have "rem_initial b xs = [] --> rem_initial b (xs @ ys) = rem_initial b ys" (is "?P xs ys") |
|
327 by (induct xs,auto) |
|
328 thus ?thesis |
|
329 .. |
|
330 qed |
|
331 |
308 |
332 definition |
309 definition |
333 norm_unsigned :: "bit list => bit list" where |
310 norm_unsigned :: "bit list => bit list" where |
334 "norm_unsigned = rem_initial \<zero>" |
311 "norm_unsigned = rem_initial \<zero>" |
335 |
312 |
365 assumes zero: "(n::nat) = 0 ==> R" |
341 assumes zero: "(n::nat) = 0 ==> R" |
366 and div : "[| n div 2 < n ; 0 < n |] ==> R" |
342 and div : "[| n div 2 < n ; 0 < n |] ==> R" |
367 shows "R" |
343 shows "R" |
368 proof (cases "n = 0") |
344 proof (cases "n = 0") |
369 assume "n = 0" |
345 assume "n = 0" |
370 thus R |
346 thus R by (rule zero) |
371 by (rule zero) |
|
372 next |
347 next |
373 assume "n ~= 0" |
348 assume "n ~= 0" |
374 hence nn0: "0 < n" |
349 hence "0 < n" by simp |
375 by simp |
350 hence "n div 2 < n" by arith |
376 hence "n div 2 < n" |
351 from this and `0 < n` show R by (rule div) |
377 by arith |
|
378 from this and nn0 |
|
379 show R |
|
380 by (rule div) |
|
381 qed |
352 qed |
382 |
353 |
383 lemma int_wf_ge_induct: |
354 lemma int_wf_ge_induct: |
384 assumes ind : "!!i::int. (!!j. [| k \<le> j ; j < i |] ==> P j) ==> P i" |
355 assumes ind : "!!i::int. (!!j. [| k \<le> j ; j < i |] ==> P j) ==> P i" |
385 shows "P i" |
356 shows "P i" |
386 proof (rule wf_induct_rule [OF wf_int_ge_less_than]) |
357 proof (rule wf_induct_rule [OF wf_int_ge_less_than]) |
387 fix x |
358 fix x |
388 assume ih: "(\<And>y\<Colon>int. (y, x) \<in> int_ge_less_than k \<Longrightarrow> P y)" |
359 assume ih: "(\<And>y\<Colon>int. (y, x) \<in> int_ge_less_than k \<Longrightarrow> P y)" |
389 thus "P x" |
360 thus "P x" |
390 by (rule ind, simp add: int_ge_less_than_def) |
361 by (rule ind) (simp add: int_ge_less_than_def) |
391 qed |
362 qed |
392 |
363 |
393 lemma unfold_nat_to_bv_helper: |
364 lemma unfold_nat_to_bv_helper: |
394 "nat_to_bv_helper b l = nat_to_bv_helper b [] @ l" |
365 "nat_to_bv_helper b l = nat_to_bv_helper b [] @ l" |
395 proof - |
366 proof - |
476 by (simp add: ring_distrib) |
446 by (simp add: ring_distrib) |
477 finally show ?thesis . |
447 finally show ?thesis . |
478 qed |
448 qed |
479 qed |
449 qed |
480 qed |
450 qed |
481 thus ?thesis |
451 thus ?thesis .. |
482 .. |
|
483 qed |
452 qed |
484 |
453 |
485 lemma bv_nat_bv [simp]: "bv_to_nat (nat_to_bv n) = n" |
454 lemma bv_nat_bv [simp]: "bv_to_nat (nat_to_bv n) = n" |
486 proof (induct n rule: less_induct) |
455 proof (induct n rule: less_induct) |
487 fix n |
456 fix n |
488 assume ind: "!!j. j < n \<Longrightarrow> bv_to_nat (nat_to_bv j) = j" |
457 assume ind: "!!j. j < n \<Longrightarrow> bv_to_nat (nat_to_bv j) = j" |
489 show "bv_to_nat (nat_to_bv n) = n" |
458 show "bv_to_nat (nat_to_bv n) = n" |
490 proof (rule n_div_2_cases [of n]) |
459 proof (rule n_div_2_cases [of n]) |
491 assume [simp]: "n = 0" |
460 assume "n = 0" |
492 show ?thesis |
461 then show ?thesis by simp |
493 by simp |
|
494 next |
462 next |
495 assume nn: "n div 2 < n" |
463 assume nn: "n div 2 < n" |
496 assume n0: "0 < n" |
464 assume n0: "0 < n" |
497 from ind and nn |
465 from ind and nn |
498 have ind': "bv_to_nat (nat_to_bv (n div 2)) = n div 2" |
466 have ind': "bv_to_nat (nat_to_bv (n div 2)) = n div 2" by blast |
499 by blast |
467 from n0 have n0': "n \<noteq> 0" by simp |
500 from n0 have n0': "n \<noteq> 0" |
|
501 by simp |
|
502 show ?thesis |
468 show ?thesis |
503 apply (subst nat_to_bv_def) |
469 apply (subst nat_to_bv_def) |
504 apply (simp only: nat_to_bv_helper.simps [of n]) |
470 apply (simp only: nat_to_bv_helper.simps [of n]) |
505 apply (simp only: n0' if_False) |
471 apply (simp only: n0' if_False) |
506 apply (subst unfold_nat_to_bv_helper) |
472 apply (subst unfold_nat_to_bv_helper) |
521 qed |
487 qed |
522 qed |
488 qed |
523 qed |
489 qed |
524 |
490 |
525 lemma bv_to_nat_type [simp]: "bv_to_nat (norm_unsigned w) = bv_to_nat w" |
491 lemma bv_to_nat_type [simp]: "bv_to_nat (norm_unsigned w) = bv_to_nat w" |
526 by (rule bit_list_induct,simp_all) |
492 by (rule bit_list_induct) simp_all |
527 |
493 |
528 lemma length_norm_unsigned_le [simp]: "length (norm_unsigned w) \<le> length w" |
494 lemma length_norm_unsigned_le [simp]: "length (norm_unsigned w) \<le> length w" |
529 by (rule bit_list_induct,simp_all) |
495 by (rule bit_list_induct) simp_all |
530 |
496 |
531 lemma bv_to_nat_rew_msb: "bv_msb w = \<one> ==> bv_to_nat w = 2 ^ (length w - 1) + bv_to_nat (tl w)" |
497 lemma bv_to_nat_rew_msb: "bv_msb w = \<one> ==> bv_to_nat w = 2 ^ (length w - 1) + bv_to_nat (tl w)" |
532 by (rule bit_list_cases [of w],simp_all) |
498 by (rule bit_list_cases [of w]) simp_all |
533 |
499 |
534 lemma norm_unsigned_result: "norm_unsigned xs = [] \<or> bv_msb (norm_unsigned xs) = \<one>" |
500 lemma norm_unsigned_result: "norm_unsigned xs = [] \<or> bv_msb (norm_unsigned xs) = \<one>" |
535 proof (rule length_induct [of _ xs]) |
501 proof (rule length_induct [of _ xs]) |
536 fix xs :: "bit list" |
502 fix xs :: "bit list" |
537 assume ind: "\<forall>ys. length ys < length xs --> norm_unsigned ys = [] \<or> bv_msb (norm_unsigned ys) = \<one>" |
503 assume ind: "\<forall>ys. length ys < length xs --> norm_unsigned ys = [] \<or> bv_msb (norm_unsigned ys) = \<one>" |
538 show "norm_unsigned xs = [] \<or> bv_msb (norm_unsigned xs) = \<one>" |
504 show "norm_unsigned xs = [] \<or> bv_msb (norm_unsigned xs) = \<one>" |
539 proof (rule bit_list_cases [of xs],simp_all) |
505 proof (rule bit_list_cases [of xs],simp_all) |
540 fix bs |
506 fix bs |
541 assume [simp]: "xs = \<zero>#bs" |
507 assume [simp]: "xs = \<zero>#bs" |
542 from ind |
508 from ind |
543 have "length bs < length xs --> norm_unsigned bs = [] \<or> bv_msb (norm_unsigned bs) = \<one>" |
509 have "length bs < length xs --> norm_unsigned bs = [] \<or> bv_msb (norm_unsigned bs) = \<one>" .. |
544 .. |
510 thus "norm_unsigned bs = [] \<or> bv_msb (norm_unsigned bs) = \<one>" by simp |
545 thus "norm_unsigned bs = [] \<or> bv_msb (norm_unsigned bs) = \<one>" |
|
546 by simp |
|
547 qed |
511 qed |
548 qed |
512 qed |
549 |
513 |
550 lemma norm_empty_bv_to_nat_zero: |
514 lemma norm_empty_bv_to_nat_zero: |
551 assumes nw: "norm_unsigned w = []" |
515 assumes nw: "norm_unsigned w = []" |
552 shows "bv_to_nat w = 0" |
516 shows "bv_to_nat w = 0" |
553 proof - |
517 proof - |
554 have "bv_to_nat w = bv_to_nat (norm_unsigned w)" |
518 have "bv_to_nat w = bv_to_nat (norm_unsigned w)" by simp |
555 by simp |
519 also have "... = bv_to_nat []" by (subst nw) (rule refl) |
556 also have "... = bv_to_nat []" |
520 also have "... = 0" by simp |
557 by (subst nw,rule) |
|
558 also have "... = 0" |
|
559 by simp |
|
560 finally show ?thesis . |
521 finally show ?thesis . |
561 qed |
522 qed |
562 |
523 |
563 lemma bv_to_nat_lower_limit: |
524 lemma bv_to_nat_lower_limit: |
564 assumes w0: "0 < bv_to_nat w" |
525 assumes w0: "0 < bv_to_nat w" |
565 shows "2 ^ (length (norm_unsigned w) - 1) \<le> bv_to_nat w" |
526 shows "2 ^ (length (norm_unsigned w) - 1) \<le> bv_to_nat w" |
566 proof - |
527 proof - |
567 from w0 and norm_unsigned_result [of w] |
528 from w0 and norm_unsigned_result [of w] |
568 have msbw: "bv_msb (norm_unsigned w) = \<one>" |
529 have msbw: "bv_msb (norm_unsigned w) = \<one>" |
569 by (auto simp add: norm_empty_bv_to_nat_zero) |
530 by (auto simp add: norm_empty_bv_to_nat_zero) |
570 have "2 ^ (length (norm_unsigned w) - 1) \<le> bv_to_nat (norm_unsigned w)" |
531 have "2 ^ (length (norm_unsigned w) - 1) \<le> bv_to_nat (norm_unsigned w)" |
571 by (subst bv_to_nat_rew_msb [OF msbw],simp) |
532 by (subst bv_to_nat_rew_msb [OF msbw],simp) |
572 thus ?thesis |
533 thus ?thesis by simp |
573 by simp |
|
574 qed |
534 qed |
575 |
535 |
576 lemmas [simp del] = nat_to_bv_non0 |
536 lemmas [simp del] = nat_to_bv_non0 |
577 |
537 |
578 lemma norm_unsigned_length [intro!]: "length (norm_unsigned w) \<le> length w" |
538 lemma norm_unsigned_length [intro!]: "length (norm_unsigned w) \<le> length w" |
582 by (simp add: norm_unsigned_def,rule rem_initial_equal) |
542 by (simp add: norm_unsigned_def,rule rem_initial_equal) |
583 |
543 |
584 lemma bv_extend_norm_unsigned: "bv_extend (length w) \<zero> (norm_unsigned w) = w" |
544 lemma bv_extend_norm_unsigned: "bv_extend (length w) \<zero> (norm_unsigned w) = w" |
585 by (simp add: norm_unsigned_def,rule bv_extend_rem_initial) |
545 by (simp add: norm_unsigned_def,rule bv_extend_rem_initial) |
586 |
546 |
587 lemma norm_unsigned_append1 [simp]: "norm_unsigned xs \<noteq> [] ==> norm_unsigned (xs @ ys) = norm_unsigned xs @ ys" |
547 lemma norm_unsigned_append1 [simp]: |
|
548 "norm_unsigned xs \<noteq> [] ==> norm_unsigned (xs @ ys) = norm_unsigned xs @ ys" |
588 by (simp add: norm_unsigned_def,rule rem_initial_append1) |
549 by (simp add: norm_unsigned_def,rule rem_initial_append1) |
589 |
550 |
590 lemma norm_unsigned_append2 [simp]: "norm_unsigned xs = [] ==> norm_unsigned (xs @ ys) = norm_unsigned ys" |
551 lemma norm_unsigned_append2 [simp]: |
|
552 "norm_unsigned xs = [] ==> norm_unsigned (xs @ ys) = norm_unsigned ys" |
591 by (simp add: norm_unsigned_def,rule rem_initial_append2) |
553 by (simp add: norm_unsigned_def,rule rem_initial_append2) |
592 |
554 |
593 lemma bv_to_nat_zero_imp_empty [rule_format]: |
555 lemma bv_to_nat_zero_imp_empty: |
594 "bv_to_nat w = 0 \<longrightarrow> norm_unsigned w = []" |
556 "bv_to_nat w = 0 \<Longrightarrow> norm_unsigned w = []" |
595 by (rule bit_list_induct [of _ w],simp_all) |
557 by (atomize (full), induct w rule: bit_list_induct) simp_all |
596 |
558 |
597 lemma bv_to_nat_nzero_imp_nempty: |
559 lemma bv_to_nat_nzero_imp_nempty: |
598 assumes "bv_to_nat w \<noteq> 0" |
560 "bv_to_nat w \<noteq> 0 \<Longrightarrow> norm_unsigned w \<noteq> []" |
599 shows "norm_unsigned w \<noteq> []" |
561 by (induct w rule: bit_list_induct) simp_all |
600 proof - |
|
601 have "bv_to_nat w \<noteq> 0 --> norm_unsigned w \<noteq> []" |
|
602 by (rule bit_list_induct [of _ w],simp_all) |
|
603 thus ?thesis |
|
604 .. |
|
605 qed |
|
606 |
562 |
607 lemma nat_helper1: |
563 lemma nat_helper1: |
608 assumes ass: "nat_to_bv (bv_to_nat w) = norm_unsigned w" |
564 assumes ass: "nat_to_bv (bv_to_nat w) = norm_unsigned w" |
609 shows "nat_to_bv (2 * bv_to_nat w + bitval x) = norm_unsigned (w @ [x])" |
565 shows "nat_to_bv (2 * bv_to_nat w + bitval x) = norm_unsigned (w @ [x])" |
610 proof (cases x) |
566 proof (cases x) |
620 have "?lhs = (1 + 2 * bv_to_nat w) mod 2" |
576 have "?lhs = (1 + 2 * bv_to_nat w) mod 2" |
621 by (simp add: add_commute) |
577 by (simp add: add_commute) |
622 also have "... = 1" |
578 also have "... = 1" |
623 by (subst mod_add1_eq) simp |
579 by (subst mod_add1_eq) simp |
624 finally have eq1: "?lhs = 1" . |
580 finally have eq1: "?lhs = 1" . |
625 have "?rhs = 0" |
581 have "?rhs = 0" by simp |
626 by simp |
|
627 with orig and eq1 |
582 with orig and eq1 |
628 show "nat_to_bv (Suc (2 * bv_to_nat w) div 2) @ [\<zero>] = norm_unsigned (w @ [\<one>])" |
583 show "nat_to_bv (Suc (2 * bv_to_nat w) div 2) @ [\<zero>] = norm_unsigned (w @ [\<one>])" |
629 by simp |
584 by simp |
630 next |
585 next |
631 have "nat_to_bv (Suc (2 * bv_to_nat w) div 2) @ [\<one>] = nat_to_bv ((1 + 2 * bv_to_nat w) div 2) @ [\<one>]" |
586 have "nat_to_bv (Suc (2 * bv_to_nat w) div 2) @ [\<one>] = |
|
587 nat_to_bv ((1 + 2 * bv_to_nat w) div 2) @ [\<one>]" |
632 by (simp add: add_commute) |
588 by (simp add: add_commute) |
633 also have "... = nat_to_bv (bv_to_nat w) @ [\<one>]" |
589 also have "... = nat_to_bv (bv_to_nat w) @ [\<one>]" |
634 by (subst div_add1_eq,simp) |
590 by (subst div_add1_eq) simp |
635 also have "... = norm_unsigned w @ [\<one>]" |
591 also have "... = norm_unsigned w @ [\<one>]" |
636 by (subst ass,rule refl) |
592 by (subst ass) (rule refl) |
637 also have "... = norm_unsigned (w @ [\<one>])" |
593 also have "... = norm_unsigned (w @ [\<one>])" |
638 by (cases "norm_unsigned w",simp_all) |
594 by (cases "norm_unsigned w") simp_all |
639 finally show "nat_to_bv (Suc (2 * bv_to_nat w) div 2) @ [\<one>] = norm_unsigned (w @ [\<one>])" |
595 finally show "nat_to_bv (Suc (2 * bv_to_nat w) div 2) @ [\<one>] = norm_unsigned (w @ [\<one>])" . |
640 . |
|
641 qed |
596 qed |
642 next |
597 next |
643 assume [simp]: "x = \<zero>" |
598 assume [simp]: "x = \<zero>" |
644 show ?thesis |
599 show ?thesis |
645 proof (cases "bv_to_nat w = 0") |
600 proof (cases "bv_to_nat w = 0") |
701 qed |
655 qed |
702 also have "... = (\<one>#rev ys) @ [y]" |
656 also have "... = (\<one>#rev ys) @ [y]" |
703 by simp |
657 by simp |
704 also have "... = \<one> # rev ys @ [y]" |
658 also have "... = \<one> # rev ys @ [y]" |
705 by simp |
659 by simp |
706 finally show "nat_to_bv (2 * 2 ^ length ys + (bv_to_nat (rev ys) * 2 + bitval y)) = \<one> # rev ys @ [y]" |
660 finally show "nat_to_bv (2 * 2 ^ length ys + (bv_to_nat (rev ys) * 2 + bitval y)) = |
707 . |
661 \<one> # rev ys @ [y]" . |
708 qed |
662 qed |
709 qed |
663 qed |
710 qed |
664 qed |
711 qed |
665 qed |
712 hence "nat_to_bv (2 ^ length (rev (rev xs)) + bv_to_nat (rev (rev xs))) = \<one> # rev (rev xs)" |
666 hence "nat_to_bv (2 ^ length (rev (rev xs)) + bv_to_nat (rev (rev xs))) = |
713 .. |
667 \<one> # rev (rev xs)" .. |
714 thus ?thesis |
668 thus ?thesis by simp |
715 by simp |
|
716 qed |
669 qed |
717 |
670 |
718 lemma nat_bv_nat [simp]: "nat_to_bv (bv_to_nat w) = norm_unsigned w" |
671 lemma nat_bv_nat [simp]: "nat_to_bv (bv_to_nat w) = norm_unsigned w" |
719 proof (rule bit_list_induct [of _ w],simp_all) |
672 proof (rule bit_list_induct [of _ w],simp_all) |
720 fix xs |
673 fix xs |
721 assume "nat_to_bv (bv_to_nat xs) = norm_unsigned xs" |
674 assume "nat_to_bv (bv_to_nat xs) = norm_unsigned xs" |
722 have "bv_to_nat xs = bv_to_nat (norm_unsigned xs)" |
675 have "bv_to_nat xs = bv_to_nat (norm_unsigned xs)" by simp |
723 by simp |
|
724 have "bv_to_nat xs < 2 ^ length xs" |
676 have "bv_to_nat xs < 2 ^ length xs" |
725 by (rule bv_to_nat_upper_range) |
677 by (rule bv_to_nat_upper_range) |
726 show "nat_to_bv (2 ^ length xs + bv_to_nat xs) = \<one> # xs" |
678 show "nat_to_bv (2 ^ length xs + bv_to_nat xs) = \<one> # xs" |
727 by (rule nat_helper2) |
679 by (rule nat_helper2) |
728 qed |
680 qed |
767 case False |
718 case False |
768 hence n0: "0 < n" by simp |
719 hence n0: "0 < n" by simp |
769 show ?thesis |
720 show ?thesis |
770 proof (rule ccontr) |
721 proof (rule ccontr) |
771 assume "~ length (nat_to_bv n) \<le> k" |
722 assume "~ length (nat_to_bv n) \<le> k" |
772 hence "k < length (nat_to_bv n)" |
723 hence "k < length (nat_to_bv n)" by simp |
773 by simp |
724 hence "k \<le> length (nat_to_bv n) - 1" by arith |
774 hence "k \<le> length (nat_to_bv n) - 1" |
725 hence "(2::nat) ^ k \<le> 2 ^ (length (nat_to_bv n) - 1)" by simp |
775 by arith |
726 also have "... = 2 ^ (length (norm_unsigned (nat_to_bv n)) - 1)" by simp |
776 hence "(2::nat) ^ k \<le> 2 ^ (length (nat_to_bv n) - 1)" |
|
777 by simp |
|
778 also have "... = 2 ^ (length (norm_unsigned (nat_to_bv n)) - 1)" |
|
779 by simp |
|
780 also have "... \<le> bv_to_nat (nat_to_bv n)" |
727 also have "... \<le> bv_to_nat (nat_to_bv n)" |
781 by (rule bv_to_nat_lower_limit,simp add: n0) |
728 by (rule bv_to_nat_lower_limit) (simp add: n0) |
782 also have "... = n" |
729 also have "... = n" by simp |
783 by simp |
|
784 finally have "2 ^ k \<le> n" . |
730 finally have "2 ^ k \<le> n" . |
785 with n0 |
731 with n0 have "2 ^ k - 1 < n" by arith |
786 have "2 ^ k - 1 < n" |
732 with nk show False by simp |
787 by arith |
|
788 with nk |
|
789 show False |
|
790 by simp |
|
791 qed |
733 qed |
792 qed |
734 qed |
793 |
735 |
794 lemma length_nat_to_bv_lower_limit: |
736 lemma length_nat_to_bv_lower_limit: |
795 assumes nk: "2 ^ k \<le> n" |
737 assumes nk: "2 ^ k \<le> n" |
796 shows "k < length (nat_to_bv n)" |
738 shows "k < length (nat_to_bv n)" |
797 proof (rule ccontr) |
739 proof (rule ccontr) |
798 assume "~ k < length (nat_to_bv n)" |
740 assume "~ k < length (nat_to_bv n)" |
799 hence lnk: "length (nat_to_bv n) \<le> k" |
741 hence lnk: "length (nat_to_bv n) \<le> k" by simp |
800 by simp |
742 have "n = bv_to_nat (nat_to_bv n)" by simp |
801 have "n = bv_to_nat (nat_to_bv n)" |
|
802 by simp |
|
803 also have "... < 2 ^ length (nat_to_bv n)" |
743 also have "... < 2 ^ length (nat_to_bv n)" |
804 by (rule bv_to_nat_upper_range) |
744 by (rule bv_to_nat_upper_range) |
805 also from lnk have "... \<le> 2 ^ k" |
745 also from lnk have "... \<le> 2 ^ k" by simp |
806 by simp |
|
807 finally have "n < 2 ^ k" . |
746 finally have "n < 2 ^ k" . |
808 with nk |
747 with nk show False by simp |
809 show False |
748 qed |
810 by simp |
749 |
811 qed |
|
812 |
750 |
813 subsection {* Unsigned Arithmetic Operations *} |
751 subsection {* Unsigned Arithmetic Operations *} |
814 |
752 |
815 definition |
753 definition |
816 bv_add :: "[bit list, bit list ] => bit list" where |
754 bv_add :: "[bit list, bit list ] => bit list" where |
828 lemma bv_add_length: "length (bv_add w1 w2) \<le> Suc (max (length w1) (length w2))" |
766 lemma bv_add_length: "length (bv_add w1 w2) \<le> Suc (max (length w1) (length w2))" |
829 proof (unfold bv_add_def,rule length_nat_to_bv_upper_limit) |
767 proof (unfold bv_add_def,rule length_nat_to_bv_upper_limit) |
830 from bv_to_nat_upper_range [of w1] and bv_to_nat_upper_range [of w2] |
768 from bv_to_nat_upper_range [of w1] and bv_to_nat_upper_range [of w2] |
831 have "bv_to_nat w1 + bv_to_nat w2 \<le> (2 ^ length w1 - 1) + (2 ^ length w2 - 1)" |
769 have "bv_to_nat w1 + bv_to_nat w2 \<le> (2 ^ length w1 - 1) + (2 ^ length w2 - 1)" |
832 by arith |
770 by arith |
833 also have "... \<le> max (2 ^ length w1 - 1) (2 ^ length w2 - 1) + max (2 ^ length w1 - 1) (2 ^ length w2 - 1)" |
771 also have "... \<le> |
|
772 max (2 ^ length w1 - 1) (2 ^ length w2 - 1) + max (2 ^ length w1 - 1) (2 ^ length w2 - 1)" |
834 by (rule add_mono,safe intro!: le_maxI1 le_maxI2) |
773 by (rule add_mono,safe intro!: le_maxI1 le_maxI2) |
835 also have "... = 2 * max (2 ^ length w1 - 1) (2 ^ length w2 - 1)" |
774 also have "... = 2 * max (2 ^ length w1 - 1) (2 ^ length w2 - 1)" by simp |
836 by simp |
|
837 also have "... \<le> 2 ^ Suc (max (length w1) (length w2)) - 2" |
775 also have "... \<le> 2 ^ Suc (max (length w1) (length w2)) - 2" |
838 proof (cases "length w1 \<le> length w2") |
776 proof (cases "length w1 \<le> length w2") |
839 assume w1w2: "length w1 \<le> length w2" |
777 assume w1w2: "length w1 \<le> length w2" |
840 hence "(2::nat) ^ length w1 \<le> 2 ^ length w2" |
778 hence "(2::nat) ^ length w1 \<le> 2 ^ length w2" by simp |
841 by simp |
779 hence "(2::nat) ^ length w1 - 1 \<le> 2 ^ length w2 - 1" by arith |
842 hence "(2::nat) ^ length w1 - 1 \<le> 2 ^ length w2 - 1" |
|
843 by arith |
|
844 with w1w2 show ?thesis |
780 with w1w2 show ?thesis |
845 by (simp add: diff_mult_distrib2 split: split_max) |
781 by (simp add: diff_mult_distrib2 split: split_max) |
846 next |
782 next |
847 assume [simp]: "~ (length w1 \<le> length w2)" |
783 assume [simp]: "~ (length w1 \<le> length w2)" |
848 have "~ ((2::nat) ^ length w1 - 1 \<le> 2 ^ length w2 - 1)" |
784 have "~ ((2::nat) ^ length w1 - 1 \<le> 2 ^ length w2 - 1)" |
849 proof |
785 proof |
850 assume "(2::nat) ^ length w1 - 1 \<le> 2 ^ length w2 - 1" |
786 assume "(2::nat) ^ length w1 - 1 \<le> 2 ^ length w2 - 1" |
851 hence "((2::nat) ^ length w1 - 1) + 1 \<le> (2 ^ length w2 - 1) + 1" |
787 hence "((2::nat) ^ length w1 - 1) + 1 \<le> (2 ^ length w2 - 1) + 1" |
852 by (rule add_right_mono) |
788 by (rule add_right_mono) |
853 hence "(2::nat) ^ length w1 \<le> 2 ^ length w2" |
789 hence "(2::nat) ^ length w1 \<le> 2 ^ length w2" by simp |
854 by simp |
790 hence "length w1 \<le> length w2" by simp |
855 hence "length w1 \<le> length w2" |
791 thus False by simp |
856 by simp |
|
857 thus False |
|
858 by simp |
|
859 qed |
792 qed |
860 thus ?thesis |
793 thus ?thesis |
861 by (simp add: diff_mult_distrib2 split: split_max) |
794 by (simp add: diff_mult_distrib2 split: split_max) |
862 qed |
795 qed |
863 finally show "bv_to_nat w1 + bv_to_nat w2 \<le> 2 ^ Suc (max (length w1) (length w2)) - 1" |
796 finally show "bv_to_nat w1 + bv_to_nat w2 \<le> 2 ^ Suc (max (length w1) (length w2)) - 1" |
931 else norm_signed (bv_not (\<zero>#nat_to_bv (nat (-n- 1)))))" |
866 else norm_signed (bv_not (\<zero>#nat_to_bv (nat (-n- 1)))))" |
932 |
867 |
933 lemma int_to_bv_ge0 [simp]: "0 \<le> n ==> int_to_bv n = norm_signed (\<zero> # nat_to_bv (nat n))" |
868 lemma int_to_bv_ge0 [simp]: "0 \<le> n ==> int_to_bv n = norm_signed (\<zero> # nat_to_bv (nat n))" |
934 by (simp add: int_to_bv_def) |
869 by (simp add: int_to_bv_def) |
935 |
870 |
936 lemma int_to_bv_lt0 [simp]: "n < 0 ==> int_to_bv n = norm_signed (bv_not (\<zero>#nat_to_bv (nat (-n- 1))))" |
871 lemma int_to_bv_lt0 [simp]: |
|
872 "n < 0 ==> int_to_bv n = norm_signed (bv_not (\<zero>#nat_to_bv (nat (-n- 1))))" |
937 by (simp add: int_to_bv_def) |
873 by (simp add: int_to_bv_def) |
938 |
874 |
939 lemma norm_signed_idem [simp]: "norm_signed (norm_signed w) = norm_signed w" |
875 lemma norm_signed_idem [simp]: "norm_signed (norm_signed w) = norm_signed w" |
940 proof (rule bit_list_induct [of _ w],simp_all) |
876 proof (rule bit_list_induct [of _ w], simp_all) |
941 fix xs |
877 fix xs |
942 assume "norm_signed (norm_signed xs) = norm_signed xs" |
878 assume eq: "norm_signed (norm_signed xs) = norm_signed xs" |
943 show "norm_signed (norm_signed (\<zero>#xs)) = norm_signed (\<zero>#xs)" |
879 show "norm_signed (norm_signed (\<zero>#xs)) = norm_signed (\<zero>#xs)" |
944 proof (rule bit_list_cases [of xs],simp_all) |
880 proof (rule bit_list_cases [of xs],simp_all) |
945 fix ys |
881 fix ys |
946 assume [symmetric,simp]: "xs = \<zero>#ys" |
882 assume "xs = \<zero>#ys" |
|
883 from this [symmetric] and eq |
947 show "norm_signed (norm_signed (\<zero>#ys)) = norm_signed (\<zero>#ys)" |
884 show "norm_signed (norm_signed (\<zero>#ys)) = norm_signed (\<zero>#ys)" |
948 by simp |
885 by simp |
949 qed |
886 qed |
950 next |
887 next |
951 fix xs |
888 fix xs |
952 assume "norm_signed (norm_signed xs) = norm_signed xs" |
889 assume eq: "norm_signed (norm_signed xs) = norm_signed xs" |
953 show "norm_signed (norm_signed (\<one>#xs)) = norm_signed (\<one>#xs)" |
890 show "norm_signed (norm_signed (\<one>#xs)) = norm_signed (\<one>#xs)" |
954 proof (rule bit_list_cases [of xs],simp_all) |
891 proof (rule bit_list_cases [of xs],simp_all) |
955 fix ys |
892 fix ys |
956 assume [symmetric,simp]: "xs = \<one>#ys" |
893 assume "xs = \<one>#ys" |
|
894 from this [symmetric] and eq |
957 show "norm_signed (norm_signed (\<one>#ys)) = norm_signed (\<one>#ys)" |
895 show "norm_signed (norm_signed (\<one>#ys)) = norm_signed (\<one>#ys)" |
958 by simp |
896 by simp |
959 qed |
897 qed |
960 qed |
898 qed |
961 |
899 |
973 |
911 |
974 lemma bv_to_int_Cons1 [simp]: "bv_to_int (\<one>#bs) = - int (bv_to_nat (bv_not bs) + 1)" |
912 lemma bv_to_int_Cons1 [simp]: "bv_to_int (\<one>#bs) = - int (bv_to_nat (bv_not bs) + 1)" |
975 by (simp add: bv_to_int_def) |
913 by (simp add: bv_to_int_def) |
976 |
914 |
977 lemma bv_to_int_type [simp]: "bv_to_int (norm_signed w) = bv_to_int w" |
915 lemma bv_to_int_type [simp]: "bv_to_int (norm_signed w) = bv_to_int w" |
978 proof (rule bit_list_induct [of _ w],simp_all) |
916 proof (rule bit_list_induct [of _ w], simp_all) |
979 fix xs |
917 fix xs |
980 assume ind: "bv_to_int (norm_signed xs) = bv_to_int xs" |
918 assume ind: "bv_to_int (norm_signed xs) = bv_to_int xs" |
981 show "bv_to_int (norm_signed (\<zero>#xs)) = int (bv_to_nat xs)" |
919 show "bv_to_int (norm_signed (\<zero>#xs)) = int (bv_to_nat xs)" |
982 proof (rule bit_list_cases [of xs],simp_all) |
920 proof (rule bit_list_cases [of xs], simp_all) |
983 fix ys |
921 fix ys |
984 assume [simp]: "xs = \<zero>#ys" |
922 assume [simp]: "xs = \<zero>#ys" |
985 from ind |
923 from ind |
986 show "bv_to_int (norm_signed (\<zero>#ys)) = int (bv_to_nat ys)" |
924 show "bv_to_int (norm_signed (\<zero>#ys)) = int (bv_to_nat ys)" |
987 by simp |
925 by simp |
988 qed |
926 qed |
989 next |
927 next |
990 fix xs |
928 fix xs |
991 assume ind: "bv_to_int (norm_signed xs) = bv_to_int xs" |
929 assume ind: "bv_to_int (norm_signed xs) = bv_to_int xs" |
992 show "bv_to_int (norm_signed (\<one>#xs)) = - int (bv_to_nat (bv_not xs)) + -1" |
930 show "bv_to_int (norm_signed (\<one>#xs)) = - int (bv_to_nat (bv_not xs)) + -1" |
993 proof (rule bit_list_cases [of xs],simp_all) |
931 proof (rule bit_list_cases [of xs], simp_all) |
994 fix ys |
932 fix ys |
995 assume [simp]: "xs = \<one>#ys" |
933 assume [simp]: "xs = \<one>#ys" |
996 from ind |
934 from ind |
997 show "bv_to_int (norm_signed (\<one>#ys)) = - int (bv_to_nat (bv_not ys)) + -1" |
935 show "bv_to_int (norm_signed (\<one>#ys)) = - int (bv_to_nat (bv_not ys)) + -1" |
998 by simp |
936 by simp |
1005 from bv_to_nat_upper_range |
943 from bv_to_nat_upper_range |
1006 show "int (bv_to_nat bs) < 2 ^ length bs" |
944 show "int (bv_to_nat bs) < 2 ^ length bs" |
1007 by (simp add: int_nat_two_exp) |
945 by (simp add: int_nat_two_exp) |
1008 next |
946 next |
1009 fix bs |
947 fix bs |
1010 have "- int (bv_to_nat (bv_not bs)) + -1 \<le> 0" |
948 have "- int (bv_to_nat (bv_not bs)) + -1 \<le> 0" by simp |
1011 by simp |
949 also have "... < 2 ^ length bs" by (induct bs) simp_all |
1012 also have "... < 2 ^ length bs" |
950 finally show "- int (bv_to_nat (bv_not bs)) + -1 < 2 ^ length bs" . |
1013 by (induct bs,simp_all) |
|
1014 finally show "- int (bv_to_nat (bv_not bs)) + -1 < 2 ^ length bs" |
|
1015 . |
|
1016 qed |
951 qed |
1017 |
952 |
1018 lemma bv_to_int_lower_range: "- (2 ^ (length w - 1)) \<le> bv_to_int w" |
953 lemma bv_to_int_lower_range: "- (2 ^ (length w - 1)) \<le> bv_to_int w" |
1019 proof (rule bit_list_cases [of w],simp_all) |
954 proof (rule bit_list_cases [of w],simp_all) |
1020 fix bs :: "bit list" |
955 fix bs :: "bit list" |
1021 have "- (2 ^ length bs) \<le> (0::int)" |
956 have "- (2 ^ length bs) \<le> (0::int)" by (induct bs) simp_all |
1022 by (induct bs,simp_all) |
957 also have "... \<le> int (bv_to_nat bs)" by simp |
1023 also have "... \<le> int (bv_to_nat bs)" |
958 finally show "- (2 ^ length bs) \<le> int (bv_to_nat bs)" . |
1024 by simp |
|
1025 finally show "- (2 ^ length bs) \<le> int (bv_to_nat bs)" |
|
1026 . |
|
1027 next |
959 next |
1028 fix bs |
960 fix bs |
1029 from bv_to_nat_upper_range [of "bv_not bs"] |
961 from bv_to_nat_upper_range [of "bv_not bs"] |
1030 show "- (2 ^ length bs) \<le> - int (bv_to_nat (bv_not bs)) + -1" |
962 show "- (2 ^ length bs) \<le> - int (bv_to_nat (bv_not bs)) + -1" |
1031 by (simp add: int_nat_two_exp) |
963 by (simp add: int_nat_two_exp) |
1061 apply simp |
993 apply simp |
1062 done |
994 done |
1063 qed |
995 qed |
1064 |
996 |
1065 lemma bv_int_bv [simp]: "bv_to_int (int_to_bv i) = i" |
997 lemma bv_int_bv [simp]: "bv_to_int (int_to_bv i) = i" |
1066 by (cases "0 \<le> i",simp_all) |
998 by (cases "0 \<le> i") simp_all |
1067 |
999 |
1068 lemma bv_msb_norm [simp]: "bv_msb (norm_signed w) = bv_msb w" |
1000 lemma bv_msb_norm [simp]: "bv_msb (norm_signed w) = bv_msb w" |
1069 by (rule bit_list_cases [of w],simp_all add: norm_signed_Cons) |
1001 by (rule bit_list_cases [of w]) (simp_all add: norm_signed_Cons) |
1070 |
1002 |
1071 lemma norm_signed_length: "length (norm_signed w) \<le> length w" |
1003 lemma norm_signed_length: "length (norm_signed w) \<le> length w" |
1072 apply (cases w,simp_all) |
1004 apply (cases w, simp_all) |
1073 apply (subst norm_signed_Cons) |
1005 apply (subst norm_signed_Cons) |
1074 apply (case_tac "a",simp_all) |
1006 apply (case_tac a, simp_all) |
1075 apply (rule rem_initial_length) |
1007 apply (rule rem_initial_length) |
1076 done |
1008 done |
1077 |
1009 |
1078 lemma norm_signed_equal: "length (norm_signed w) = length w ==> norm_signed w = w" |
1010 lemma norm_signed_equal: "length (norm_signed w) = length w ==> norm_signed w = w" |
1079 proof (rule bit_list_cases [of w],simp_all) |
1011 proof (rule bit_list_cases [of w], simp_all) |
1080 fix xs |
1012 fix xs |
1081 assume "length (norm_signed (\<zero>#xs)) = Suc (length xs)" |
1013 assume "length (norm_signed (\<zero>#xs)) = Suc (length xs)" |
1082 thus "norm_signed (\<zero>#xs) = \<zero>#xs" |
1014 thus "norm_signed (\<zero>#xs) = \<zero>#xs" |
1083 apply (simp add: norm_signed_Cons) |
1015 apply (simp add: norm_signed_Cons) |
1084 apply safe |
1016 apply safe |
1133 assumes one: "bv_to_int xs = bv_to_int ys" |
1065 assumes one: "bv_to_int xs = bv_to_int ys" |
1134 and len: "length xs = length ys" |
1066 and len: "length xs = length ys" |
1135 shows "xs = ys" |
1067 shows "xs = ys" |
1136 proof - |
1068 proof - |
1137 from one |
1069 from one |
1138 have "int_to_bv (bv_to_int xs) = int_to_bv (bv_to_int ys)" |
1070 have "int_to_bv (bv_to_int xs) = int_to_bv (bv_to_int ys)" by simp |
1139 by simp |
1071 hence xsys: "norm_signed xs = norm_signed ys" by simp |
1140 hence xsys: "norm_signed xs = norm_signed ys" |
|
1141 by simp |
|
1142 hence xsys': "bv_msb xs = bv_msb ys" |
1072 hence xsys': "bv_msb xs = bv_msb ys" |
1143 proof - |
1073 proof - |
1144 have "bv_msb xs = bv_msb (norm_signed xs)" |
1074 have "bv_msb xs = bv_msb (norm_signed xs)" by simp |
1145 by simp |
1075 also have "... = bv_msb (norm_signed ys)" by (simp add: xsys) |
1146 also have "... = bv_msb (norm_signed ys)" |
1076 also have "... = bv_msb ys" by simp |
1147 by (simp add: xsys) |
|
1148 also have "... = bv_msb ys" |
|
1149 by simp |
|
1150 finally show ?thesis . |
1077 finally show ?thesis . |
1151 qed |
1078 qed |
1152 have "xs = bv_extend (length xs) (bv_msb xs) (norm_signed xs)" |
1079 have "xs = bv_extend (length xs) (bv_msb xs) (norm_signed xs)" |
1153 by (simp add: bv_extend_norm_signed) |
1080 by (simp add: bv_extend_norm_signed) |
1154 also have "... = bv_extend (length ys) (bv_msb ys) (norm_signed ys)" |
1081 also have "... = bv_extend (length ys) (bv_msb ys) (norm_signed ys)" |
1170 lemma bv_to_int_lower_limit_gt0: |
1097 lemma bv_to_int_lower_limit_gt0: |
1171 assumes w0: "0 < bv_to_int w" |
1098 assumes w0: "0 < bv_to_int w" |
1172 shows "2 ^ (length (norm_signed w) - 2) \<le> bv_to_int w" |
1099 shows "2 ^ (length (norm_signed w) - 2) \<le> bv_to_int w" |
1173 proof - |
1100 proof - |
1174 from w0 |
1101 from w0 |
1175 have "0 \<le> bv_to_int w" |
1102 have "0 \<le> bv_to_int w" by simp |
1176 by simp |
1103 hence [simp]: "bv_msb w = \<zero>" by (rule bv_to_int_msb0) |
1177 hence [simp]: "bv_msb w = \<zero>" |
|
1178 by (rule bv_to_int_msb0) |
|
1179 have "2 ^ (length (norm_signed w) - 2) \<le> bv_to_int (norm_signed w)" |
1104 have "2 ^ (length (norm_signed w) - 2) \<le> bv_to_int (norm_signed w)" |
1180 proof (rule bit_list_cases [of w]) |
1105 proof (rule bit_list_cases [of w]) |
1181 assume "w = []" |
1106 assume "w = []" |
1182 with w0 |
1107 with w0 show ?thesis by simp |
1183 show ?thesis |
|
1184 by simp |
|
1185 next |
1108 next |
1186 fix w' |
1109 fix w' |
1187 assume weq: "w = \<zero> # w'" |
1110 assume weq: "w = \<zero> # w'" |
1188 thus ?thesis |
1111 thus ?thesis |
1189 proof (simp add: norm_signed_Cons,safe) |
1112 proof (simp add: norm_signed_Cons,safe) |
1190 assume "norm_unsigned w' = []" |
1113 assume "norm_unsigned w' = []" |
1191 with weq and w0 |
1114 with weq and w0 show False |
1192 show False |
1115 by (simp add: norm_empty_bv_to_nat_zero) |
1193 by (simp add: norm_empty_bv_to_nat_zero) |
|
1194 next |
1116 next |
1195 assume w'0: "norm_unsigned w' \<noteq> []" |
1117 assume w'0: "norm_unsigned w' \<noteq> []" |
1196 have "0 < bv_to_nat w'" |
1118 have "0 < bv_to_nat w'" |
1197 proof (rule ccontr) |
1119 proof (rule ccontr) |
1198 assume "~ (0 < bv_to_nat w')" |
1120 assume "~ (0 < bv_to_nat w')" |
1199 hence "bv_to_nat w' = 0" |
1121 hence "bv_to_nat w' = 0" |
1200 by arith |
1122 by arith |
1201 hence "norm_unsigned w' = []" |
1123 hence "norm_unsigned w' = []" |
1202 by (simp add: bv_to_nat_zero_imp_empty) |
1124 by (simp add: bv_to_nat_zero_imp_empty) |
1203 with w'0 |
1125 with w'0 |
1204 show False |
1126 show False by simp |
1205 by simp |
|
1206 qed |
1127 qed |
1207 with bv_to_nat_lower_limit [of w'] |
1128 with bv_to_nat_lower_limit [of w'] |
1208 show "2 ^ (length (norm_unsigned w') - Suc 0) \<le> int (bv_to_nat w')" |
1129 show "2 ^ (length (norm_unsigned w') - Suc 0) \<le> int (bv_to_nat w')" |
1209 by (simp add: int_nat_two_exp) |
1130 by (simp add: int_nat_two_exp) |
1210 qed |
1131 qed |
1211 next |
1132 next |
1212 fix w' |
1133 fix w' |
1213 assume "w = \<one> # w'" |
1134 assume "w = \<one> # w'" |
1214 from w0 |
1135 from w0 have "bv_msb w = \<zero>" by simp |
1215 have "bv_msb w = \<zero>" |
1136 with prems show ?thesis by simp |
1216 by simp |
1137 qed |
1217 with prems |
1138 also have "... = bv_to_int w" by simp |
1218 show ?thesis |
|
1219 by simp |
|
1220 qed |
|
1221 also have "... = bv_to_int w" |
|
1222 by simp |
|
1223 finally show ?thesis . |
1139 finally show ?thesis . |
1224 qed |
1140 qed |
1225 |
1141 |
1226 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))" |
1142 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))" |
1227 apply (rule bit_list_cases [of w],simp_all) |
1143 apply (rule bit_list_cases [of w],simp_all) |
1233 proof - |
1149 proof - |
1234 fix l |
1150 fix l |
1235 assume msb: "\<zero> = bv_msb (norm_unsigned l)" |
1151 assume msb: "\<zero> = bv_msb (norm_unsigned l)" |
1236 assume "norm_unsigned l \<noteq> []" |
1152 assume "norm_unsigned l \<noteq> []" |
1237 with norm_unsigned_result [of l] |
1153 with norm_unsigned_result [of l] |
1238 have "bv_msb (norm_unsigned l) = \<one>" |
1154 have "bv_msb (norm_unsigned l) = \<one>" by simp |
1239 by simp |
1155 with msb show False by simp |
1240 with msb |
|
1241 show False |
|
1242 by simp |
|
1243 next |
1156 next |
1244 fix xs |
1157 fix xs |
1245 assume p: "\<one> = bv_msb (tl (norm_signed (\<one> # xs)))" |
1158 assume p: "\<one> = bv_msb (tl (norm_signed (\<one> # xs)))" |
1246 have "\<one> \<noteq> bv_msb (tl (norm_signed (\<one> # xs)))" |
1159 have "\<one> \<noteq> bv_msb (tl (norm_signed (\<one> # xs)))" |
1247 by (rule bit_list_induct [of _ xs],simp_all) |
1160 by (rule bit_list_induct [of _ xs],simp_all) |
1248 with p |
1161 with p show False by simp |
1249 show False |
|
1250 by simp |
|
1251 qed |
1162 qed |
1252 |
1163 |
1253 lemma bv_to_int_upper_limit_lem1: |
1164 lemma bv_to_int_upper_limit_lem1: |
1254 assumes w0: "bv_to_int w < -1" |
1165 assumes w0: "bv_to_int w < -1" |
1255 shows "bv_to_int w < - (2 ^ (length (norm_signed w) - 2))" |
1166 shows "bv_to_int w < - (2 ^ (length (norm_signed w) - 2))" |
1256 proof - |
1167 proof - |
1257 from w0 |
1168 from w0 |
1258 have "bv_to_int w < 0" |
1169 have "bv_to_int w < 0" by simp |
1259 by simp |
|
1260 hence msbw [simp]: "bv_msb w = \<one>" |
1170 hence msbw [simp]: "bv_msb w = \<one>" |
1261 by (rule bv_to_int_msb1) |
1171 by (rule bv_to_int_msb1) |
1262 have "bv_to_int w = bv_to_int (norm_signed w)" |
1172 have "bv_to_int w = bv_to_int (norm_signed w)" by simp |
1263 by simp |
|
1264 also from norm_signed_result [of w] |
1173 also from norm_signed_result [of w] |
1265 have "... < - (2 ^ (length (norm_signed w) - 2))" |
1174 have "... < - (2 ^ (length (norm_signed w) - 2))" |
1266 proof (safe) |
1175 proof safe |
1267 assume "norm_signed w = []" |
1176 assume "norm_signed w = []" |
1268 hence "bv_to_int (norm_signed w) = 0" |
1177 hence "bv_to_int (norm_signed w) = 0" by simp |
1269 by simp |
1178 with w0 show ?thesis by simp |
1270 with w0 |
|
1271 show ?thesis |
|
1272 by simp |
|
1273 next |
1179 next |
1274 assume "norm_signed w = [\<one>]" |
1180 assume "norm_signed w = [\<one>]" |
1275 hence "bv_to_int (norm_signed w) = -1" |
1181 hence "bv_to_int (norm_signed w) = -1" by simp |
1276 by simp |
1182 with w0 show ?thesis by simp |
1277 with w0 |
|
1278 show ?thesis |
|
1279 by simp |
|
1280 next |
1183 next |
1281 assume "bv_msb (norm_signed w) \<noteq> bv_msb (tl (norm_signed w))" |
1184 assume "bv_msb (norm_signed w) \<noteq> bv_msb (tl (norm_signed w))" |
1282 hence msb_tl: "\<one> \<noteq> bv_msb (tl (norm_signed w))" |
1185 hence msb_tl: "\<one> \<noteq> bv_msb (tl (norm_signed w))" by simp |
1283 by simp |
|
1284 show "bv_to_int (norm_signed w) < - (2 ^ (length (norm_signed w) - 2))" |
1186 show "bv_to_int (norm_signed w) < - (2 ^ (length (norm_signed w) - 2))" |
1285 proof (rule bit_list_cases [of "norm_signed w"]) |
1187 proof (rule bit_list_cases [of "norm_signed w"]) |
1286 assume "norm_signed w = []" |
1188 assume "norm_signed w = []" |
1287 hence "bv_to_int (norm_signed w) = 0" |
1189 hence "bv_to_int (norm_signed w) = 0" by simp |
1288 by simp |
1190 with w0 show ?thesis by simp |
1289 with w0 |
|
1290 show ?thesis |
|
1291 by simp |
|
1292 next |
1191 next |
1293 fix w' |
1192 fix w' |
1294 assume nw: "norm_signed w = \<zero> # w'" |
1193 assume nw: "norm_signed w = \<zero> # w'" |
1295 from msbw |
1194 from msbw have "bv_msb (norm_signed w) = \<one>" by simp |
1296 have "bv_msb (norm_signed w) = \<one>" |
1195 with nw show ?thesis by simp |
1297 by simp |
|
1298 with nw |
|
1299 show ?thesis |
|
1300 by simp |
|
1301 next |
1196 next |
1302 fix w' |
1197 fix w' |
1303 assume weq: "norm_signed w = \<one> # w'" |
1198 assume weq: "norm_signed w = \<one> # w'" |
1304 show ?thesis |
1199 show ?thesis |
1305 proof (rule bit_list_cases [of w']) |
1200 proof (rule bit_list_cases [of w']) |
1306 assume w'eq: "w' = []" |
1201 assume w'eq: "w' = []" |
1307 from w0 |
1202 from w0 have "bv_to_int (norm_signed w) < -1" by simp |
1308 have "bv_to_int (norm_signed w) < -1" |
1203 with w'eq and weq show ?thesis by simp |
1309 by simp |
|
1310 with w'eq and weq |
|
1311 show ?thesis |
|
1312 by simp |
|
1313 next |
1204 next |
1314 fix w'' |
1205 fix w'' |
1315 assume w'eq: "w' = \<zero> # w''" |
1206 assume w'eq: "w' = \<zero> # w''" |
1316 show ?thesis |
1207 show ?thesis |
1317 apply (simp add: weq w'eq) |
1208 apply (simp add: weq w'eq) |
1339 proof (rule ccontr) |
1228 proof (rule ccontr) |
1340 from w0 wk |
1229 from w0 wk |
1341 have k1: "1 < k" |
1230 have k1: "1 < k" |
1342 by (cases "k - 1",simp_all) |
1231 by (cases "k - 1",simp_all) |
1343 assume "~ length (int_to_bv i) \<le> k" |
1232 assume "~ length (int_to_bv i) \<le> k" |
1344 hence "k < length (int_to_bv i)" |
1233 hence "k < length (int_to_bv i)" by simp |
1345 by simp |
1234 hence "k \<le> length (int_to_bv i) - 1" by arith |
1346 hence "k \<le> length (int_to_bv i) - 1" |
1235 hence a: "k - 1 \<le> length (int_to_bv i) - 2" by arith |
1347 by arith |
|
1348 hence a: "k - 1 \<le> length (int_to_bv i) - 2" |
|
1349 by arith |
|
1350 hence "(2::int) ^ (k - 1) \<le> 2 ^ (length (int_to_bv i) - 2)" by simp |
1236 hence "(2::int) ^ (k - 1) \<le> 2 ^ (length (int_to_bv i) - 2)" by simp |
1351 also have "... \<le> i" |
1237 also have "... \<le> i" |
1352 proof - |
1238 proof - |
1353 have "2 ^ (length (norm_signed (int_to_bv i)) - 2) \<le> bv_to_int (int_to_bv i)" |
1239 have "2 ^ (length (norm_signed (int_to_bv i)) - 2) \<le> bv_to_int (int_to_bv i)" |
1354 proof (rule bv_to_int_lower_limit_gt0) |
1240 proof (rule bv_to_int_lower_limit_gt0) |
1355 from w0 |
1241 from w0 show "0 < bv_to_int (int_to_bv i)" by simp |
1356 show "0 < bv_to_int (int_to_bv i)" |
|
1357 by simp |
|
1358 qed |
1242 qed |
1359 thus ?thesis |
1243 thus ?thesis by simp |
1360 by simp |
|
1361 qed |
1244 qed |
1362 finally have "2 ^ (k - 1) \<le> i" . |
1245 finally have "2 ^ (k - 1) \<le> i" . |
1363 with wk |
1246 with wk show False by simp |
1364 show False |
|
1365 by simp |
|
1366 qed |
1247 qed |
1367 |
1248 |
1368 lemma pos_length_pos: |
1249 lemma pos_length_pos: |
1369 assumes i0: "0 < bv_to_int w" |
1250 assumes i0: "0 < bv_to_int w" |
|
1251 shows "0 < length w" |
|
1252 proof - |
|
1253 from norm_signed_result [of w] |
|
1254 have "0 < length (norm_signed w)" |
|
1255 proof (auto) |
|
1256 assume ii: "norm_signed w = []" |
|
1257 have "bv_to_int (norm_signed w) = 0" by (subst ii) simp |
|
1258 hence "bv_to_int w = 0" by simp |
|
1259 with i0 show False by simp |
|
1260 next |
|
1261 assume ii: "norm_signed w = []" |
|
1262 assume jj: "bv_msb w \<noteq> \<zero>" |
|
1263 have "\<zero> = bv_msb (norm_signed w)" |
|
1264 by (subst ii) simp |
|
1265 also have "... \<noteq> \<zero>" |
|
1266 by (simp add: jj) |
|
1267 finally show False by simp |
|
1268 qed |
|
1269 also have "... \<le> length w" |
|
1270 by (rule norm_signed_length) |
|
1271 finally show ?thesis . |
|
1272 qed |
|
1273 |
|
1274 lemma neg_length_pos: |
|
1275 assumes i0: "bv_to_int w < -1" |
1370 shows "0 < length w" |
1276 shows "0 < length w" |
1371 proof - |
1277 proof - |
1372 from norm_signed_result [of w] |
1278 from norm_signed_result [of w] |
1373 have "0 < length (norm_signed w)" |
1279 have "0 < length (norm_signed w)" |
1374 proof (auto) |
1280 proof (auto) |
1375 assume ii: "norm_signed w = []" |
1281 assume ii: "norm_signed w = []" |
1376 have "bv_to_int (norm_signed w) = 0" |
1282 have "bv_to_int (norm_signed w) = 0" |
1377 by (subst ii,simp) |
1283 by (subst ii) simp |
1378 hence "bv_to_int w = 0" |
1284 hence "bv_to_int w = 0" by simp |
1379 by simp |
1285 with i0 show False by simp |
1380 with i0 |
|
1381 show False |
|
1382 by simp |
|
1383 next |
1286 next |
1384 assume ii: "norm_signed w = []" |
1287 assume ii: "norm_signed w = []" |
1385 assume jj: "bv_msb w \<noteq> \<zero>" |
1288 assume jj: "bv_msb w \<noteq> \<zero>" |
1386 have "\<zero> = bv_msb (norm_signed w)" |
1289 have "\<zero> = bv_msb (norm_signed w)" by (subst ii) simp |
1387 by (subst ii,simp) |
1290 also have "... \<noteq> \<zero>" by (simp add: jj) |
1388 also have "... \<noteq> \<zero>" |
|
1389 by (simp add: jj) |
|
1390 finally show False by simp |
1291 finally show False by simp |
1391 qed |
1292 qed |
1392 also have "... \<le> length w" |
1293 also have "... \<le> length w" |
1393 by (rule norm_signed_length) |
1294 by (rule norm_signed_length) |
1394 finally show ?thesis |
1295 finally show ?thesis . |
1395 . |
|
1396 qed |
|
1397 |
|
1398 lemma neg_length_pos: |
|
1399 assumes i0: "bv_to_int w < -1" |
|
1400 shows "0 < length w" |
|
1401 proof - |
|
1402 from norm_signed_result [of w] |
|
1403 have "0 < length (norm_signed w)" |
|
1404 proof (auto) |
|
1405 assume ii: "norm_signed w = []" |
|
1406 have "bv_to_int (norm_signed w) = 0" |
|
1407 by (subst ii,simp) |
|
1408 hence "bv_to_int w = 0" |
|
1409 by simp |
|
1410 with i0 |
|
1411 show False |
|
1412 by simp |
|
1413 next |
|
1414 assume ii: "norm_signed w = []" |
|
1415 assume jj: "bv_msb w \<noteq> \<zero>" |
|
1416 have "\<zero> = bv_msb (norm_signed w)" |
|
1417 by (subst ii,simp) |
|
1418 also have "... \<noteq> \<zero>" |
|
1419 by (simp add: jj) |
|
1420 finally show False by simp |
|
1421 qed |
|
1422 also have "... \<le> length w" |
|
1423 by (rule norm_signed_length) |
|
1424 finally show ?thesis |
|
1425 . |
|
1426 qed |
1296 qed |
1427 |
1297 |
1428 lemma length_int_to_bv_lower_limit_gt0: |
1298 lemma length_int_to_bv_lower_limit_gt0: |
1429 assumes wk: "2 ^ (k - 1) \<le> i" |
1299 assumes wk: "2 ^ (k - 1) \<le> i" |
1430 shows "k < length (int_to_bv i)" |
1300 shows "k < length (int_to_bv i)" |
1431 proof (rule ccontr) |
1301 proof (rule ccontr) |
1432 have "0 < (2::int) ^ (k - 1)" |
1302 have "0 < (2::int) ^ (k - 1)" |
1433 by (rule zero_less_power,simp) |
1303 by (rule zero_less_power) simp |
1434 also have "... \<le> i" |
1304 also have "... \<le> i" by (rule wk) |
1435 by (rule wk) |
1305 finally have i0: "0 < i" . |
1436 finally have i0: "0 < i" |
|
1437 . |
|
1438 have lii0: "0 < length (int_to_bv i)" |
1306 have lii0: "0 < length (int_to_bv i)" |
1439 apply (rule pos_length_pos) |
1307 apply (rule pos_length_pos) |
1440 apply (simp,rule i0) |
1308 apply (simp,rule i0) |
1441 done |
1309 done |
1442 assume "~ k < length (int_to_bv i)" |
1310 assume "~ k < length (int_to_bv i)" |
1443 hence "length (int_to_bv i) \<le> k" |
1311 hence "length (int_to_bv i) \<le> k" by simp |
1444 by simp |
|
1445 with lii0 |
1312 with lii0 |
1446 have a: "length (int_to_bv i) - 1 \<le> k - 1" |
1313 have a: "length (int_to_bv i) - 1 \<le> k - 1" |
1447 by arith |
1314 by arith |
1448 have "i < 2 ^ (length (int_to_bv i) - 1)" |
1315 have "i < 2 ^ (length (int_to_bv i) - 1)" |
1449 proof - |
1316 proof - |
1452 also have "... < 2 ^ (length (int_to_bv i) - 1)" |
1319 also have "... < 2 ^ (length (int_to_bv i) - 1)" |
1453 by (rule bv_to_int_upper_range) |
1320 by (rule bv_to_int_upper_range) |
1454 finally show ?thesis . |
1321 finally show ?thesis . |
1455 qed |
1322 qed |
1456 also have "(2::int) ^ (length (int_to_bv i) - 1) \<le> 2 ^ (k - 1)" using a |
1323 also have "(2::int) ^ (length (int_to_bv i) - 1) \<le> 2 ^ (k - 1)" using a |
1457 by simp |
1324 by simp |
1458 finally have "i < 2 ^ (k - 1)" . |
1325 finally have "i < 2 ^ (k - 1)" . |
1459 with wk |
1326 with wk show False by simp |
1460 show False |
|
1461 by simp |
|
1462 qed |
1327 qed |
1463 |
1328 |
1464 lemma length_int_to_bv_upper_limit_lem1: |
1329 lemma length_int_to_bv_upper_limit_lem1: |
1465 assumes w1: "i < -1" |
1330 assumes w1: "i < -1" |
1466 and wk: "- (2 ^ (k - 1)) \<le> i" |
1331 and wk: "- (2 ^ (k - 1)) \<le> i" |
1467 shows "length (int_to_bv i) \<le> k" |
1332 shows "length (int_to_bv i) \<le> k" |
1468 proof (rule ccontr) |
1333 proof (rule ccontr) |
1469 from w1 wk |
1334 from w1 wk |
1470 have k1: "1 < k" |
1335 have k1: "1 < k" by (cases "k - 1") simp_all |
1471 by (cases "k - 1",simp_all) |
|
1472 assume "~ length (int_to_bv i) \<le> k" |
1336 assume "~ length (int_to_bv i) \<le> k" |
1473 hence "k < length (int_to_bv i)" |
1337 hence "k < length (int_to_bv i)" by simp |
1474 by simp |
1338 hence "k \<le> length (int_to_bv i) - 1" by arith |
1475 hence "k \<le> length (int_to_bv i) - 1" |
1339 hence a: "k - 1 \<le> length (int_to_bv i) - 2" by arith |
1476 by arith |
|
1477 hence a: "k - 1 \<le> length (int_to_bv i) - 2" |
|
1478 by arith |
|
1479 have "i < - (2 ^ (length (int_to_bv i) - 2))" |
1340 have "i < - (2 ^ (length (int_to_bv i) - 2))" |
1480 proof - |
1341 proof - |
1481 have "i = bv_to_int (int_to_bv i)" |
1342 have "i = bv_to_int (int_to_bv i)" |
1482 by simp |
1343 by simp |
1483 also have "... < - (2 ^ (length (norm_signed (int_to_bv i)) - 2))" |
1344 also have "... < - (2 ^ (length (norm_signed (int_to_bv i)) - 2))" |
1484 by (rule bv_to_int_upper_limit_lem1,simp,rule w1) |
1345 by (rule bv_to_int_upper_limit_lem1,simp,rule w1) |
1485 finally show ?thesis by simp |
1346 finally show ?thesis by simp |
1486 qed |
1347 qed |
1487 also have "... \<le> -(2 ^ (k - 1))" |
1348 also have "... \<le> -(2 ^ (k - 1))" |
1488 proof - |
1349 proof - |
1489 have "(2::int) ^ (k - 1) \<le> 2 ^ (length (int_to_bv i) - 2)" using a |
1350 have "(2::int) ^ (k - 1) \<le> 2 ^ (length (int_to_bv i) - 2)" using a by simp |
1490 by simp |
1351 thus ?thesis by simp |
1491 thus ?thesis |
|
1492 by simp |
|
1493 qed |
1352 qed |
1494 finally have "i < -(2 ^ (k - 1))" . |
1353 finally have "i < -(2 ^ (k - 1))" . |
1495 with wk |
1354 with wk show False by simp |
1496 show False |
|
1497 by simp |
|
1498 qed |
1355 qed |
1499 |
1356 |
1500 lemma length_int_to_bv_lower_limit_lem1: |
1357 lemma length_int_to_bv_lower_limit_lem1: |
1501 assumes wk: "i < -(2 ^ (k - 1))" |
1358 assumes wk: "i < -(2 ^ (k - 1))" |
1502 shows "k < length (int_to_bv i)" |
1359 shows "k < length (int_to_bv i)" |
1503 proof (rule ccontr) |
1360 proof (rule ccontr) |
1504 from wk |
1361 from wk have "i \<le> -(2 ^ (k - 1)) - 1" by simp |
1505 have "i \<le> -(2 ^ (k - 1)) - 1" |
|
1506 by simp |
|
1507 also have "... < -1" |
1362 also have "... < -1" |
1508 proof - |
1363 proof - |
1509 have "0 < (2::int) ^ (k - 1)" |
1364 have "0 < (2::int) ^ (k - 1)" |
1510 by (rule zero_less_power,simp) |
1365 by (rule zero_less_power) simp |
1511 hence "-((2::int) ^ (k - 1)) < 0" |
1366 hence "-((2::int) ^ (k - 1)) < 0" by simp |
1512 by simp |
|
1513 thus ?thesis by simp |
1367 thus ?thesis by simp |
1514 qed |
1368 qed |
1515 finally have i1: "i < -1" . |
1369 finally have i1: "i < -1" . |
1516 have lii0: "0 < length (int_to_bv i)" |
1370 have lii0: "0 < length (int_to_bv i)" |
1517 apply (rule neg_length_pos) |
1371 apply (rule neg_length_pos) |
1518 apply (simp,rule i1) |
1372 apply (simp, rule i1) |
1519 done |
1373 done |
1520 assume "~ k < length (int_to_bv i)" |
1374 assume "~ k < length (int_to_bv i)" |
1521 hence "length (int_to_bv i) \<le> k" |
1375 hence "length (int_to_bv i) \<le> k" |
1522 by simp |
1376 by simp |
1523 with lii0 |
1377 with lii0 have a: "length (int_to_bv i) - 1 \<le> k - 1" by arith |
1524 have a: "length (int_to_bv i) - 1 \<le> k - 1" |
|
1525 by arith |
|
1526 hence "(2::int) ^ (length (int_to_bv i) - 1) \<le> 2 ^ (k - 1)" by simp |
1378 hence "(2::int) ^ (length (int_to_bv i) - 1) \<le> 2 ^ (k - 1)" by simp |
1527 hence "-((2::int) ^ (k - 1)) \<le> - (2 ^ (length (int_to_bv i) - 1))" |
1379 hence "-((2::int) ^ (k - 1)) \<le> - (2 ^ (length (int_to_bv i) - 1))" by simp |
1528 by simp |
|
1529 also have "... \<le> i" |
1380 also have "... \<le> i" |
1530 proof - |
1381 proof - |
1531 have "- (2 ^ (length (int_to_bv i) - 1)) \<le> bv_to_int (int_to_bv i)" |
1382 have "- (2 ^ (length (int_to_bv i) - 1)) \<le> bv_to_int (int_to_bv i)" |
1532 by (rule bv_to_int_lower_range) |
1383 by (rule bv_to_int_lower_range) |
1533 also have "... = i" |
1384 also have "... = i" |
1534 by simp |
1385 by simp |
1535 finally show ?thesis . |
1386 finally show ?thesis . |
1536 qed |
1387 qed |
1537 finally have "-(2 ^ (k - 1)) \<le> i" . |
1388 finally have "-(2 ^ (k - 1)) \<le> i" . |
1538 with wk |
1389 with wk show False by simp |
1539 show False |
1390 qed |
1540 by simp |
1391 |
1541 qed |
|
1542 |
1392 |
1543 subsection {* Signed Arithmetic Operations *} |
1393 subsection {* Signed Arithmetic Operations *} |
1544 |
1394 |
1545 subsubsection {* Conversion from unsigned to signed *} |
1395 subsubsection {* Conversion from unsigned to signed *} |
1546 |
1396 |
1590 using p |
1439 using p |
1591 apply simp |
1440 apply simp |
1592 done |
1441 done |
1593 show ?thesis |
1442 show ?thesis |
1594 proof (simp add: bv_uminus_def,rule length_int_to_bv_upper_limit_gt0,simp_all) |
1443 proof (simp add: bv_uminus_def,rule length_int_to_bv_upper_limit_gt0,simp_all) |
1595 from prems |
1444 from prems show "bv_to_int w < 0" by simp |
1596 show "bv_to_int w < 0" |
|
1597 by simp |
|
1598 next |
1445 next |
1599 have "-(2^(length w - 1)) \<le> bv_to_int w" |
1446 have "-(2^(length w - 1)) \<le> bv_to_int w" |
1600 by (rule bv_to_int_lower_range) |
1447 by (rule bv_to_int_lower_range) |
1601 hence "- bv_to_int w \<le> 2^(length w - 1)" |
1448 hence "- bv_to_int w \<le> 2^(length w - 1)" by simp |
1602 by simp |
1449 also from lw have "... < 2 ^ length w" by simp |
1603 also from lw have "... < 2 ^ length w" |
1450 finally show "- bv_to_int w < 2 ^ length w" by simp |
1604 by simp |
|
1605 finally show "- bv_to_int w < 2 ^ length w" |
|
1606 by simp |
|
1607 qed |
1451 qed |
1608 next |
1452 next |
1609 assume p: "- bv_to_int w = 1" |
1453 assume p: "- bv_to_int w = 1" |
1610 hence lw: "0 < length w" |
1454 hence lw: "0 < length w" by (cases w) simp_all |
1611 by (cases w,simp_all) |
|
1612 from p |
1455 from p |
1613 show ?thesis |
1456 show ?thesis |
1614 apply (simp add: bv_uminus_def) |
1457 apply (simp add: bv_uminus_def) |
1615 using lw |
1458 using lw |
1616 apply (simp (no_asm) add: nat_to_bv_non0) |
1459 apply (simp (no_asm) add: nat_to_bv_non0) |
1617 done |
1460 done |
1618 next |
1461 next |
1619 assume "- bv_to_int w = 0" |
1462 assume "- bv_to_int w = 0" |
1620 thus ?thesis |
1463 thus ?thesis by (simp add: bv_uminus_def) |
1621 by (simp add: bv_uminus_def) |
|
1622 next |
1464 next |
1623 assume p: "- bv_to_int w = -1" |
1465 assume p: "- bv_to_int w = -1" |
1624 thus ?thesis |
1466 thus ?thesis by (simp add: bv_uminus_def) |
1625 by (simp add: bv_uminus_def) |
|
1626 next |
1467 next |
1627 assume p: "- bv_to_int w < -1" |
1468 assume p: "- bv_to_int w < -1" |
1628 show ?thesis |
1469 show ?thesis |
1629 apply (simp add: bv_uminus_def) |
1470 apply (simp add: bv_uminus_def) |
1630 apply (rule length_int_to_bv_upper_limit_lem1) |
1471 apply (rule length_int_to_bv_upper_limit_lem1) |
1632 apply simp |
1473 apply simp |
1633 proof - |
1474 proof - |
1634 have "bv_to_int w < 2 ^ (length w - 1)" |
1475 have "bv_to_int w < 2 ^ (length w - 1)" |
1635 by (rule bv_to_int_upper_range) |
1476 by (rule bv_to_int_upper_range) |
1636 also have "... \<le> 2 ^ length w" by simp |
1477 also have "... \<le> 2 ^ length w" by simp |
1637 finally show "bv_to_int w \<le> 2 ^ length w" |
1478 finally show "bv_to_int w \<le> 2 ^ length w" by simp |
1638 by simp |
|
1639 qed |
1479 qed |
1640 qed |
1480 qed |
1641 qed |
1481 qed |
1642 |
1482 |
1643 lemma bv_uminus_length_utos: "length (bv_uminus (utos w)) \<le> Suc (length w)" |
1483 lemma bv_uminus_length_utos: "length (bv_uminus (utos w)) \<le> Suc (length w)" |
1644 proof - |
1484 proof - |
1645 have "-bv_to_int (utos w) = 0 \<or> -bv_to_int (utos w) = -1 \<or> -bv_to_int (utos w) < -1" |
1485 have "-bv_to_int (utos w) = 0 \<or> -bv_to_int (utos w) = -1 \<or> -bv_to_int (utos w) < -1" |
1646 apply (simp add: bv_to_int_utos) |
1486 by (simp add: bv_to_int_utos, arith) |
1647 by arith |
|
1648 thus ?thesis |
1487 thus ?thesis |
1649 proof safe |
1488 proof safe |
1650 assume "-bv_to_int (utos w) = 0" |
1489 assume "-bv_to_int (utos w) = 0" |
1651 thus ?thesis |
1490 thus ?thesis by (simp add: bv_uminus_def) |
1652 by (simp add: bv_uminus_def) |
|
1653 next |
1491 next |
1654 assume "-bv_to_int (utos w) = -1" |
1492 assume "-bv_to_int (utos w) = -1" |
1655 thus ?thesis |
1493 thus ?thesis by (simp add: bv_uminus_def) |
1656 by (simp add: bv_uminus_def) |
|
1657 next |
1494 next |
1658 assume p: "-bv_to_int (utos w) < -1" |
1495 assume p: "-bv_to_int (utos w) < -1" |
1659 show ?thesis |
1496 show ?thesis |
1660 apply (simp add: bv_uminus_def) |
1497 apply (simp add: bv_uminus_def) |
1661 apply (rule length_int_to_bv_upper_limit_lem1) |
1498 apply (rule length_int_to_bv_upper_limit_lem1) |
2026 by (simp add: zmult_ac) |
1848 by (simp add: zmult_ac) |
2027 thus "-(((2::int)^(length w1 - Suc 0)) * (2 ^ (length w2 - Suc 0))) \<le> ?Q" |
1849 thus "-(((2::int)^(length w1 - Suc 0)) * (2 ^ (length w2 - Suc 0))) \<le> ?Q" |
2028 by simp |
1850 by simp |
2029 qed |
1851 qed |
2030 qed |
1852 qed |
2031 finally show "-(2 ^ (length w1 + length w2 - Suc 0)) \<le> ?Q" |
1853 finally show "-(2 ^ (length w1 + length w2 - Suc 0)) \<le> ?Q" . |
2032 . |
|
2033 qed |
1854 qed |
2034 qed |
1855 qed |
2035 qed |
1856 qed |
2036 |
1857 |
2037 lemma bv_msb_one: "bv_msb w = \<one> ==> 0 < bv_to_nat w" |
1858 lemma bv_msb_one: "bv_msb w = \<one> ==> 0 < bv_to_nat w" |
2038 by (cases w,simp_all) |
1859 by (cases w) simp_all |
2039 |
1860 |
2040 lemma bv_smult_length_utos: "length (bv_smult (utos w1) w2) \<le> length w1 + length w2" |
1861 lemma bv_smult_length_utos: "length (bv_smult (utos w1) w2) \<le> length w1 + length w2" |
2041 proof - |
1862 proof - |
2042 let ?Q = "bv_to_int (utos w1) * bv_to_int w2" |
1863 let ?Q = "bv_to_int (utos w1) * bv_to_int w2" |
2043 |
1864 |
2044 have lmw: "?Q \<noteq> 0 ==> 0 < length (utos w1) \<and> 0 < length w2" |
1865 have lmw: "?Q \<noteq> 0 ==> 0 < length (utos w1) \<and> 0 < length w2" by auto |
2045 by auto |
1866 |
2046 |
1867 have "0 < ?Q \<or> ?Q = 0 \<or> ?Q = -1 \<or> ?Q < -1" by arith |
2047 have "0 < ?Q \<or> ?Q = 0 \<or> ?Q = -1 \<or> ?Q < -1" |
|
2048 by arith |
|
2049 thus ?thesis |
1868 thus ?thesis |
2050 proof (safe dest!: iffD1 [OF mult_eq_0_iff]) |
1869 proof (safe dest!: iffD1 [OF mult_eq_0_iff]) |
2051 assume "bv_to_int (utos w1) = 0" |
1870 assume "bv_to_int (utos w1) = 0" |
2052 thus ?thesis |
1871 thus ?thesis by (simp add: bv_smult_def) |
2053 by (simp add: bv_smult_def) |
|
2054 next |
1872 next |
2055 assume "bv_to_int w2 = 0" |
1873 assume "bv_to_int w2 = 0" |
2056 thus ?thesis |
1874 thus ?thesis by (simp add: bv_smult_def) |
2057 by (simp add: bv_smult_def) |
|
2058 next |
1875 next |
2059 assume p: "0 < ?Q" |
1876 assume p: "0 < ?Q" |
2060 thus ?thesis |
1877 thus ?thesis |
2061 proof (simp add: zero_less_mult_iff,safe) |
1878 proof (simp add: zero_less_mult_iff,safe) |
2062 assume biw2: "0 < bv_to_int w2" |
1879 assume biw2: "0 < bv_to_int w2" |
2181 assume ind: "\<forall>ys::bit list. length ys < length xs --> (\<forall>n. n < length ys --> ys ! (length ys - Suc n) = rev ys ! n)" |
1995 assume ind: "\<forall>ys::bit list. length ys < length xs --> (\<forall>n. n < length ys --> ys ! (length ys - Suc n) = rev ys ! n)" |
2182 assume notx: "n < length xs" |
1996 assume notx: "n < length xs" |
2183 show "xs ! (length xs - Suc n) = rev xs ! n" |
1997 show "xs ! (length xs - Suc n) = rev xs ! n" |
2184 proof (cases xs) |
1998 proof (cases xs) |
2185 assume "xs = []" |
1999 assume "xs = []" |
2186 with notx |
2000 with notx show ?thesis by simp |
2187 show ?thesis |
|
2188 by simp |
|
2189 next |
2001 next |
2190 fix y ys |
2002 fix y ys |
2191 assume [simp]: "xs = y # ys" |
2003 assume [simp]: "xs = y # ys" |
2192 show ?thesis |
2004 show ?thesis |
2193 proof (auto simp add: nth_append) |
2005 proof (auto simp add: nth_append) |
2194 assume noty: "n < length ys" |
2006 assume noty: "n < length ys" |
2195 from spec [OF ind,of ys] |
2007 from spec [OF ind,of ys] |
2196 have "\<forall>n. n < length ys --> ys ! (length ys - Suc n) = rev ys ! n" |
2008 have "\<forall>n. n < length ys --> ys ! (length ys - Suc n) = rev ys ! n" |
2197 by simp |
2009 by simp |
2198 hence "n < length ys --> ys ! (length ys - Suc n) = rev ys ! n" |
2010 hence "n < length ys --> ys ! (length ys - Suc n) = rev ys ! n" .. |
2199 .. |
2011 from this and noty |
2200 hence "ys ! (length ys - Suc n) = rev ys ! n" |
2012 have "ys ! (length ys - Suc n) = rev ys ! n" .. |
2201 .. |
|
2202 thus "(y # ys) ! (length ys - n) = rev ys ! n" |
2013 thus "(y # ys) ! (length ys - n) = rev ys ! n" |
2203 by (simp add: nth_Cons' noty linorder_not_less [symmetric]) |
2014 by (simp add: nth_Cons' noty linorder_not_less [symmetric]) |
2204 next |
2015 next |
2205 assume "~ n < length ys" |
2016 assume "~ n < length ys" |
2206 hence x: "length ys \<le> n" |
2017 hence x: "length ys \<le> n" by simp |
2207 by simp |
2018 from notx have "n < Suc (length ys)" by simp |
2208 from notx |
2019 hence "n \<le> length ys" by simp |
2209 have "n < Suc (length ys)" |
2020 with x have "length ys = n" by simp |
2210 by simp |
2021 thus "y = [y] ! (n - length ys)" by simp |
2211 hence "n \<le> length ys" |
|
2212 by simp |
|
2213 with x |
|
2214 have "length ys = n" |
|
2215 by simp |
|
2216 thus "y = [y] ! (n - length ys)" |
|
2217 by simp |
|
2218 qed |
2022 qed |
2219 qed |
2023 qed |
2220 qed |
2024 qed |
2221 hence "n < length w --> bv_select w n = rev w ! n" |
2025 then have "n < length w --> bv_select w n = rev w ! n" .. |
2222 .. |
2026 from this and notnull show ?thesis .. |
2223 thus ?thesis |
|
2224 .. |
|
2225 qed |
2027 qed |
2226 |
2028 |
2227 lemma bv_chop_append: "bv_chop (w1 @ w2) (length w2) = (w1,w2)" |
2029 lemma bv_chop_append: "bv_chop (w1 @ w2) (length w2) = (w1,w2)" |
2228 by (simp add: bv_chop_def Let_def) |
2030 by (simp add: bv_chop_def Let_def) |
2229 |
2031 |
2301 finally show ?thesis |
2101 finally show ?thesis |
2302 using i0 |
2102 using i0 |
2303 by (simp add: length_int_def) |
2103 by (simp add: length_int_def) |
2304 next |
2104 next |
2305 assume "~ 0 < i" |
2105 assume "~ 0 < i" |
2306 hence i0: "i \<le> 0" |
2106 hence i0: "i \<le> 0" by simp |
2307 by simp |
|
2308 show ?thesis |
2107 show ?thesis |
2309 proof (cases "i = 0") |
2108 proof (cases "i = 0") |
2310 assume "i = 0" |
2109 assume "i = 0" |
2311 thus ?thesis |
2110 thus ?thesis by (simp add: length_int_def) |
2312 by (simp add: length_int_def) |
|
2313 next |
2111 next |
2314 assume "i \<noteq> 0" |
2112 assume "i \<noteq> 0" |
2315 with i0 |
2113 with i0 have i0: "i < 0" by simp |
2316 have i0: "i < 0" |
2114 hence "length (int_to_bv i) = |
2317 by simp |
2115 length (norm_signed (\<one> # bv_not (norm_unsigned (nat_to_bv (nat (- i) - 1)))))" |
2318 hence "length (int_to_bv i) = length (norm_signed (\<one> # bv_not (norm_unsigned (nat_to_bv (nat (- i) - 1)))))" |
|
2319 by (simp add: int_to_bv_def nat_diff_distrib) |
2116 by (simp add: int_to_bv_def nat_diff_distrib) |
2320 also from norm_unsigned_result [of "nat_to_bv (nat (- i) - 1)"] |
2117 also from norm_unsigned_result [of "nat_to_bv (nat (- i) - 1)"] |
2321 have "... = Suc (length_nat (nat (- i) - 1))" |
2118 have "... = Suc (length_nat (nat (- i) - 1))" |
2322 apply safe |
2119 apply safe |
2323 apply (simp del: norm_unsigned_nat_to_bv) |
2120 apply (simp del: norm_unsigned_nat_to_bv) |
2411 lemma bv_to_int_extend [simp]: |
2207 lemma bv_to_int_extend [simp]: |
2412 assumes a: "bv_msb w = b" |
2208 assumes a: "bv_msb w = b" |
2413 shows "bv_to_int (bv_extend n b w) = bv_to_int w" |
2209 shows "bv_to_int (bv_extend n b w) = bv_to_int w" |
2414 proof (cases "bv_msb w") |
2210 proof (cases "bv_msb w") |
2415 assume [simp]: "bv_msb w = \<zero>" |
2211 assume [simp]: "bv_msb w = \<zero>" |
2416 with a have [simp]: "b = \<zero>" |
2212 with a have [simp]: "b = \<zero>" by simp |
2417 by simp |
2213 show ?thesis by (simp add: bv_to_int_def) |
2418 show ?thesis |
|
2419 by (simp add: bv_to_int_def) |
|
2420 next |
2214 next |
2421 assume [simp]: "bv_msb w = \<one>" |
2215 assume [simp]: "bv_msb w = \<one>" |
2422 with a have [simp]: "b = \<one>" |
2216 with a have [simp]: "b = \<one>" by simp |
2423 by simp |
|
2424 show ?thesis |
2217 show ?thesis |
2425 apply (simp add: bv_to_int_def) |
2218 apply (simp add: bv_to_int_def) |
2426 apply (simp add: bv_extend_def) |
2219 apply (simp add: bv_extend_def) |
2427 apply (induct "n - length w",simp_all) |
2220 apply (induct "n - length w",simp_all) |
2428 done |
2221 done |
2445 apply (rule LeastI) |
2238 apply (rule LeastI) |
2446 apply (subgoal_tac "y < 2 ^ y",assumption) |
2239 apply (subgoal_tac "y < 2 ^ y",assumption) |
2447 apply (cases "0 \<le> y") |
2240 apply (cases "0 \<le> y") |
2448 apply (induct y,simp_all) |
2241 apply (induct y,simp_all) |
2449 done |
2242 done |
2450 with xx |
2243 with xx have "y < x" by simp |
2451 have "y < x" by simp |
2244 with xy show False by simp |
2452 with xy |
|
2453 show False |
|
2454 by simp |
|
2455 qed |
2245 qed |
2456 |
2246 |
2457 lemma length_nat_mono_int [simp]: "x \<le> y ==> length_nat x \<le> length_nat y" |
2247 lemma length_nat_mono_int [simp]: "x \<le> y ==> length_nat x \<le> length_nat y" |
2458 apply (rule length_nat_mono) |
2248 by (rule length_nat_mono) arith |
2459 apply arith |
|
2460 done |
|
2461 |
2249 |
2462 lemma length_nat_pos [simp,intro!]: "0 < x ==> 0 < length_nat x" |
2250 lemma length_nat_pos [simp,intro!]: "0 < x ==> 0 < length_nat x" |
2463 by (simp add: length_nat_non0) |
2251 by (simp add: length_nat_non0) |
2464 |
2252 |
2465 lemma length_int_mono_gt0: "[| 0 \<le> x ; x \<le> y |] ==> length_int x \<le> length_int y" |
2253 lemma length_int_mono_gt0: "[| 0 \<le> x ; x \<le> y |] ==> length_int x \<le> length_int y" |
2466 by (cases "x = 0",simp_all add: length_int_gt0 nat_le_eq_zle) |
2254 by (cases "x = 0") (simp_all add: length_int_gt0 nat_le_eq_zle) |
2467 |
2255 |
2468 lemma length_int_mono_lt0: "[| x \<le> y ; y \<le> 0 |] ==> length_int y \<le> length_int x" apply (cases "y = 0",simp_all add: length_int_lt0) |
2256 lemma length_int_mono_lt0: "[| x \<le> y ; y \<le> 0 |] ==> length_int y \<le> length_int x" |
2469 done |
2257 by (cases "y = 0") (simp_all add: length_int_lt0) |
2470 |
2258 |
2471 lemmas [simp] = length_nat_non0 |
2259 lemmas [simp] = length_nat_non0 |
2472 |
2260 |
2473 lemma "nat_to_bv (number_of Numeral.Pls) = []" |
2261 lemma "nat_to_bv (number_of Numeral.Pls) = []" |
2474 by simp |
2262 by simp |
2475 |
2263 |
2476 consts |
2264 consts |
2477 fast_bv_to_nat_helper :: "[bit list, int] => int" |
2265 fast_bv_to_nat_helper :: "[bit list, int] => int" |
2478 |
|
2479 primrec |
2266 primrec |
2480 fast_bv_to_nat_Nil: "fast_bv_to_nat_helper [] k = k" |
2267 fast_bv_to_nat_Nil: "fast_bv_to_nat_helper [] k = k" |
2481 fast_bv_to_nat_Cons: "fast_bv_to_nat_helper (b#bs) k = fast_bv_to_nat_helper bs (k BIT (bit_case bit.B0 bit.B1 b))" |
2268 fast_bv_to_nat_Cons: "fast_bv_to_nat_helper (b#bs) k = |
2482 |
2269 fast_bv_to_nat_helper bs (k BIT (bit_case bit.B0 bit.B1 b))" |
2483 lemma fast_bv_to_nat_Cons0: "fast_bv_to_nat_helper (\<zero>#bs) bin = fast_bv_to_nat_helper bs (bin BIT bit.B0)" |
2270 |
|
2271 lemma fast_bv_to_nat_Cons0: "fast_bv_to_nat_helper (\<zero>#bs) bin = |
|
2272 fast_bv_to_nat_helper bs (bin BIT bit.B0)" |
2484 by simp |
2273 by simp |
2485 |
2274 |
2486 lemma fast_bv_to_nat_Cons1: "fast_bv_to_nat_helper (\<one>#bs) bin = fast_bv_to_nat_helper bs (bin BIT bit.B1)" |
2275 lemma fast_bv_to_nat_Cons1: "fast_bv_to_nat_helper (\<one>#bs) bin = |
|
2276 fast_bv_to_nat_helper bs (bin BIT bit.B1)" |
2487 by simp |
2277 by simp |
2488 |
2278 |
2489 lemma fast_bv_to_nat_def: "bv_to_nat bs == number_of (fast_bv_to_nat_helper bs Numeral.Pls)" |
2279 lemma fast_bv_to_nat_def: |
|
2280 "bv_to_nat bs == number_of (fast_bv_to_nat_helper bs Numeral.Pls)" |
2490 proof (simp add: bv_to_nat_def) |
2281 proof (simp add: bv_to_nat_def) |
2491 have "\<forall> bin. \<not> (neg (number_of bin :: int)) \<longrightarrow> (foldl (%bn b. 2 * bn + bitval b) (number_of bin) bs) = number_of (fast_bv_to_nat_helper bs bin)" |
2282 have "\<forall> bin. \<not> (neg (number_of bin :: int)) \<longrightarrow> (foldl (%bn b. 2 * bn + bitval b) (number_of bin) bs) = number_of (fast_bv_to_nat_helper bs bin)" |
2492 apply (induct bs,simp) |
2283 apply (induct bs,simp) |
2493 apply (case_tac a,simp_all) |
2284 apply (case_tac a,simp_all) |
2494 done |
2285 done |