src/HOL/Library/Word.thy
 author nipkow Tue Mar 03 17:05:18 2009 +0100 (2009-03-03) changeset 30224 79136ce06bdb parent 28562 4e74209f113e child 30960 fec1a04b7220 permissions -rw-r--r--
removed and renamed redundant lemmas
1 (*  Title:      HOL/Library/Word.thy
2     ID:         \$Id\$
3     Author:     Sebastian Skalberg (TU Muenchen)
4 *)
6 header {* Binary Words *}
8 theory Word
9 imports "~~/src/HOL/Main"
10 begin
12 subsection {* Auxilary Lemmas *}
14 lemma max_le [intro!]: "[| x \<le> z; y \<le> z |] ==> max x y \<le> z"
15   by (simp add: max_def)
17 lemma max_mono:
18   fixes x :: "'a::linorder"
19   assumes mf: "mono f"
20   shows       "max (f x) (f y) \<le> f (max x y)"
21 proof -
22   from mf and le_maxI1 [of x y]
23   have fx: "f x \<le> f (max x y)" by (rule monoD)
24   from mf and le_maxI2 [of y x]
25   have fy: "f y \<le> f (max x y)" by (rule monoD)
26   from fx and fy
27   show "max (f x) (f y) \<le> f (max x y)" by auto
28 qed
30 declare zero_le_power [intro]
31   and zero_less_power [intro]
33 lemma int_nat_two_exp: "2 ^ k = int (2 ^ k)"
34   by (simp add: zpower_int [symmetric])
37 subsection {* Bits *}
39 datatype bit =
40     Zero ("\<zero>")
41   | One ("\<one>")
43 primrec
44   bitval :: "bit => nat"
45 where
46   "bitval \<zero> = 0"
47   | "bitval \<one> = 1"
49 consts
50   bitnot :: "bit => bit"
51   bitand :: "bit => bit => bit" (infixr "bitand" 35)
52   bitor  :: "bit => bit => bit" (infixr "bitor"  30)
53   bitxor :: "bit => bit => bit" (infixr "bitxor" 30)
55 notation (xsymbols)
56   bitnot ("\<not>\<^sub>b _"  40) and
57   bitand (infixr "\<and>\<^sub>b" 35) and
58   bitor  (infixr "\<or>\<^sub>b" 30) and
59   bitxor (infixr "\<oplus>\<^sub>b" 30)
61 notation (HTML output)
62   bitnot ("\<not>\<^sub>b _"  40) and
63   bitand (infixr "\<and>\<^sub>b" 35) and
64   bitor  (infixr "\<or>\<^sub>b" 30) and
65   bitxor (infixr "\<oplus>\<^sub>b" 30)
67 primrec
68   bitnot_zero: "(bitnot \<zero>) = \<one>"
69   bitnot_one : "(bitnot \<one>)  = \<zero>"
71 primrec
72   bitand_zero: "(\<zero> bitand y) = \<zero>"
73   bitand_one:  "(\<one> bitand y) = y"
75 primrec
76   bitor_zero: "(\<zero> bitor y) = y"
77   bitor_one:  "(\<one> bitor y) = \<one>"
79 primrec
80   bitxor_zero: "(\<zero> bitxor y) = y"
81   bitxor_one:  "(\<one> bitxor y) = (bitnot y)"
83 lemma bitnot_bitnot [simp]: "(bitnot (bitnot b)) = b"
84   by (cases b) simp_all
86 lemma bitand_cancel [simp]: "(b bitand b) = b"
87   by (cases b) simp_all
89 lemma bitor_cancel [simp]: "(b bitor b) = b"
90   by (cases b) simp_all
92 lemma bitxor_cancel [simp]: "(b bitxor b) = \<zero>"
93   by (cases b) simp_all
96 subsection {* Bit Vectors *}
98 text {* First, a couple of theorems expressing case analysis and
99 induction principles for bit vectors. *}
101 lemma bit_list_cases:
102   assumes empty: "w = [] ==> P w"
103   and     zero:  "!!bs. w = \<zero> # bs ==> P w"
104   and     one:   "!!bs. w = \<one> # bs ==> P w"
105   shows   "P w"
106 proof (cases w)
107   assume "w = []"
108   thus ?thesis by (rule empty)
109 next
110   fix b bs
111   assume [simp]: "w = b # bs"
112   show "P w"
113   proof (cases b)
114     assume "b = \<zero>"
115     hence "w = \<zero> # bs" by simp
116     thus ?thesis by (rule zero)
117   next
118     assume "b = \<one>"
119     hence "w = \<one> # bs" by simp
120     thus ?thesis by (rule one)
121   qed
122 qed
124 lemma bit_list_induct:
125   assumes empty: "P []"
126   and     zero:  "!!bs. P bs ==> P (\<zero>#bs)"
127   and     one:   "!!bs. P bs ==> P (\<one>#bs)"
128   shows   "P w"
129 proof (induct w, simp_all add: empty)
130   fix b bs
131   assume "P bs"
132   then show "P (b#bs)"
133     by (cases b) (auto intro!: zero one)
134 qed
136 definition
137   bv_msb :: "bit list => bit" where
138   "bv_msb w = (if w = [] then \<zero> else hd w)"
140 definition
141   bv_extend :: "[nat,bit,bit list]=>bit list" where
142   "bv_extend i b w = (replicate (i - length w) b) @ w"
144 definition
145   bv_not :: "bit list => bit list" where
146   "bv_not w = map bitnot w"
148 lemma bv_length_extend [simp]: "length w \<le> i ==> length (bv_extend i b w) = i"
149   by (simp add: bv_extend_def)
151 lemma bv_not_Nil [simp]: "bv_not [] = []"
152   by (simp add: bv_not_def)
154 lemma bv_not_Cons [simp]: "bv_not (b#bs) = (bitnot b) # bv_not bs"
155   by (simp add: bv_not_def)
157 lemma bv_not_bv_not [simp]: "bv_not (bv_not w) = w"
158   by (rule bit_list_induct [of _ w]) simp_all
160 lemma bv_msb_Nil [simp]: "bv_msb [] = \<zero>"
161   by (simp add: bv_msb_def)
163 lemma bv_msb_Cons [simp]: "bv_msb (b#bs) = b"
164   by (simp add: bv_msb_def)
166 lemma bv_msb_bv_not [simp]: "0 < length w ==> bv_msb (bv_not w) = (bitnot (bv_msb w))"
167   by (cases w) simp_all
169 lemma bv_msb_one_length [simp,intro]: "bv_msb w = \<one> ==> 0 < length w"
170   by (cases w) simp_all
172 lemma length_bv_not [simp]: "length (bv_not w) = length w"
173   by (induct w) simp_all
175 definition
176   bv_to_nat :: "bit list => nat" where
177   "bv_to_nat = foldl (%bn b. 2 * bn + bitval b) 0"
179 lemma bv_to_nat_Nil [simp]: "bv_to_nat [] = 0"
180   by (simp add: bv_to_nat_def)
182 lemma bv_to_nat_helper [simp]: "bv_to_nat (b # bs) = bitval b * 2 ^ length bs + bv_to_nat bs"
183 proof -
184   let ?bv_to_nat' = "foldl (\<lambda>bn b. 2 * bn + bitval b)"
185   have helper: "\<And>base. ?bv_to_nat' base bs = base * 2 ^ length bs + ?bv_to_nat' 0 bs"
186   proof (induct bs)
187     case Nil
188     show ?case by simp
189   next
190     case (Cons x xs base)
191     show ?case
192       apply (simp only: foldl.simps)
193       apply (subst Cons [of "2 * base + bitval x"])
194       apply simp
195       apply (subst Cons [of "bitval x"])
197       done
198   qed
199   show ?thesis by (simp add: bv_to_nat_def) (rule helper)
200 qed
202 lemma bv_to_nat0 [simp]: "bv_to_nat (\<zero>#bs) = bv_to_nat bs"
203   by simp
205 lemma bv_to_nat1 [simp]: "bv_to_nat (\<one>#bs) = 2 ^ length bs + bv_to_nat bs"
206   by simp
208 lemma bv_to_nat_upper_range: "bv_to_nat w < 2 ^ length w"
209 proof (induct w, simp_all)
210   fix b bs
211   assume "bv_to_nat bs < 2 ^ length bs"
212   show "bitval b * 2 ^ length bs + bv_to_nat bs < 2 * 2 ^ length bs"
213   proof (cases b, simp_all)
214     have "bv_to_nat bs < 2 ^ length bs" by fact
215     also have "... < 2 * 2 ^ length bs" by auto
216     finally show "bv_to_nat bs < 2 * 2 ^ length bs" by simp
217   next
218     have "bv_to_nat bs < 2 ^ length bs" by fact
219     hence "2 ^ length bs + bv_to_nat bs < 2 ^ length bs + 2 ^ length bs" by arith
220     also have "... = 2 * (2 ^ length bs)" by simp
221     finally show "bv_to_nat bs < 2 ^ length bs" by simp
222   qed
223 qed
225 lemma bv_extend_longer [simp]:
226   assumes wn: "n \<le> length w"
227   shows       "bv_extend n b w = w"
228   by (simp add: bv_extend_def wn)
230 lemma bv_extend_shorter [simp]:
231   assumes wn: "length w < n"
232   shows       "bv_extend n b w = bv_extend n b (b#w)"
233 proof -
234   from wn
235   have s: "n - Suc (length w) + 1 = n - length w"
236     by arith
237   have "bv_extend n b w = replicate (n - length w) b @ w"
238     by (simp add: bv_extend_def)
239   also have "... = replicate (n - Suc (length w) + 1) b @ w"
240     by (subst s) rule
241   also have "... = (replicate (n - Suc (length w)) b @ replicate 1 b) @ w"
242     by (subst replicate_add) rule
243   also have "... = replicate (n - Suc (length w)) b @ b # w"
244     by simp
245   also have "... = bv_extend n b (b#w)"
246     by (simp add: bv_extend_def)
247   finally show "bv_extend n b w = bv_extend n b (b#w)" .
248 qed
250 consts
251   rem_initial :: "bit => bit list => bit list"
252 primrec
253   "rem_initial b [] = []"
254   "rem_initial b (x#xs) = (if b = x then rem_initial b xs else x#xs)"
256 lemma rem_initial_length: "length (rem_initial b w) \<le> length w"
257   by (rule bit_list_induct [of _ w],simp_all (no_asm),safe,simp_all)
259 lemma rem_initial_equal:
260   assumes p: "length (rem_initial b w) = length w"
261   shows      "rem_initial b w = w"
262 proof -
263   have "length (rem_initial b w) = length w --> rem_initial b w = w"
264   proof (induct w, simp_all, clarify)
265     fix xs
266     assume "length (rem_initial b xs) = length xs --> rem_initial b xs = xs"
267     assume f: "length (rem_initial b xs) = Suc (length xs)"
268     with rem_initial_length [of b xs]
269     show "rem_initial b xs = b#xs"
270       by auto
271   qed
272   from this and p show ?thesis ..
273 qed
275 lemma bv_extend_rem_initial: "bv_extend (length w) b (rem_initial b w) = w"
276 proof (induct w, simp_all, safe)
277   fix xs
278   assume ind: "bv_extend (length xs) b (rem_initial b xs) = xs"
279   from rem_initial_length [of b xs]
280   have [simp]: "Suc (length xs) - length (rem_initial b xs) =
281       1 + (length xs - length (rem_initial b xs))"
282     by arith
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)"
285     by (simp add: bv_extend_def)
286   also have "... =
287       replicate (1 + (length xs - length (rem_initial b xs))) b @ rem_initial b xs"
288     by simp
289   also have "... =
290       (replicate 1 b @ replicate (length xs - length (rem_initial b xs)) b) @ rem_initial b xs"
291     by (subst replicate_add) (rule refl)
292   also have "... = b # bv_extend (length xs) b (rem_initial b xs)"
293     by (auto simp add: bv_extend_def [symmetric])
294   also have "... = b # xs"
295     by (simp add: ind)
296   finally show "bv_extend (Suc (length xs)) b (rem_initial b xs) = b # xs" .
297 qed
299 lemma rem_initial_append1:
300   assumes "rem_initial b xs ~= []"
301   shows   "rem_initial b (xs @ ys) = rem_initial b xs @ ys"
302   using assms by (induct xs) auto
304 lemma rem_initial_append2:
305   assumes "rem_initial b xs = []"
306   shows   "rem_initial b (xs @ ys) = rem_initial b ys"
307   using assms by (induct xs) auto
309 definition
310   norm_unsigned :: "bit list => bit list" where
311   "norm_unsigned = rem_initial \<zero>"
313 lemma norm_unsigned_Nil [simp]: "norm_unsigned [] = []"
314   by (simp add: norm_unsigned_def)
316 lemma norm_unsigned_Cons0 [simp]: "norm_unsigned (\<zero>#bs) = norm_unsigned bs"
317   by (simp add: norm_unsigned_def)
319 lemma norm_unsigned_Cons1 [simp]: "norm_unsigned (\<one>#bs) = \<one>#bs"
320   by (simp add: norm_unsigned_def)
322 lemma norm_unsigned_idem [simp]: "norm_unsigned (norm_unsigned w) = norm_unsigned w"
323   by (rule bit_list_induct [of _ w],simp_all)
325 consts
326   nat_to_bv_helper :: "nat => bit list => bit list"
327 recdef nat_to_bv_helper "measure (\<lambda>n. n)"
328   "nat_to_bv_helper n = (%bs. (if n = 0 then bs
329                                else nat_to_bv_helper (n div 2) ((if n mod 2 = 0 then \<zero> else \<one>)#bs)))"
331 definition
332   nat_to_bv :: "nat => bit list" where
333   "nat_to_bv n = nat_to_bv_helper n []"
335 lemma nat_to_bv0 [simp]: "nat_to_bv 0 = []"
336   by (simp add: nat_to_bv_def)
338 lemmas [simp del] = nat_to_bv_helper.simps
340 lemma n_div_2_cases:
341   assumes zero: "(n::nat) = 0 ==> R"
342   and     div : "[| n div 2 < n ; 0 < n |] ==> R"
343   shows         "R"
344 proof (cases "n = 0")
345   assume "n = 0"
346   thus R by (rule zero)
347 next
348   assume "n ~= 0"
349   hence "0 < n" by simp
350   hence "n div 2 < n" by arith
351   from this and `0 < n` show R by (rule div)
352 qed
354 lemma int_wf_ge_induct:
355   assumes ind :  "!!i::int. (!!j. [| k \<le> j ; j < i |] ==> P j) ==> P i"
356   shows          "P i"
357 proof (rule wf_induct_rule [OF wf_int_ge_less_than])
358   fix x
359   assume ih: "(\<And>y\<Colon>int. (y, x) \<in> int_ge_less_than k \<Longrightarrow> P y)"
360   thus "P x"
361     by (rule ind) (simp add: int_ge_less_than_def)
362 qed
364 lemma unfold_nat_to_bv_helper:
365   "nat_to_bv_helper b l = nat_to_bv_helper b [] @ l"
366 proof -
367   have "\<forall>l. nat_to_bv_helper b l = nat_to_bv_helper b [] @ l"
368   proof (induct b rule: less_induct)
369     fix n
370     assume ind: "!!j. j < n \<Longrightarrow> \<forall> l. nat_to_bv_helper j l = nat_to_bv_helper j [] @ l"
371     show "\<forall>l. nat_to_bv_helper n l = nat_to_bv_helper n [] @ l"
372     proof
373       fix l
374       show "nat_to_bv_helper n l = nat_to_bv_helper n [] @ l"
375       proof (cases "n < 0")
376         assume "n < 0"
377         thus ?thesis
378           by (simp add: nat_to_bv_helper.simps)
379       next
380         assume "~n < 0"
381         show ?thesis
382         proof (rule n_div_2_cases [of n])
383           assume [simp]: "n = 0"
384           show ?thesis
385             apply (simp only: nat_to_bv_helper.simps [of n])
386             apply simp
387             done
388         next
389           assume n2n: "n div 2 < n"
390           assume [simp]: "0 < n"
391           hence n20: "0 \<le> n div 2"
392             by arith
393           from ind [of "n div 2"] and n2n n20
394           have ind': "\<forall>l. nat_to_bv_helper (n div 2) l = nat_to_bv_helper (n div 2) [] @ l"
395             by blast
396           show ?thesis
397             apply (simp only: nat_to_bv_helper.simps [of n])
398             apply (cases "n=0")
399             apply simp
400             apply (simp only: if_False)
401             apply simp
402             apply (subst spec [OF ind',of "\<zero>#l"])
403             apply (subst spec [OF ind',of "\<one>#l"])
404             apply (subst spec [OF ind',of "[\<one>]"])
405             apply (subst spec [OF ind',of "[\<zero>]"])
406             apply simp
407             done
408         qed
409       qed
410     qed
411   qed
412   thus ?thesis ..
413 qed
415 lemma nat_to_bv_non0 [simp]: "n\<noteq>0 ==> nat_to_bv n = nat_to_bv (n div 2) @ [if n mod 2 = 0 then \<zero> else \<one>]"
416 proof -
417   assume [simp]: "n\<noteq>0"
418   show ?thesis
419     apply (subst nat_to_bv_def [of n])
420     apply (simp only: nat_to_bv_helper.simps [of n])
421     apply (subst unfold_nat_to_bv_helper)
422     using prems
423     apply (simp)
424     apply (subst nat_to_bv_def [of "n div 2"])
425     apply auto
426     done
427 qed
429 lemma bv_to_nat_dist_append:
430   "bv_to_nat (l1 @ l2) = bv_to_nat l1 * 2 ^ length l2 + bv_to_nat l2"
431 proof -
432   have "\<forall>l2. bv_to_nat (l1 @ l2) = bv_to_nat l1 * 2 ^ length l2 + bv_to_nat l2"
433   proof (induct l1, simp_all)
434     fix x xs
435     assume ind: "\<forall>l2. bv_to_nat (xs @ l2) = bv_to_nat xs * 2 ^ length l2 + bv_to_nat l2"
436     show "\<forall>l2::bit list. 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"
437     proof
438       fix l2
439       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"
440       proof -
441         have "(2::nat) ^ (length xs + length l2) = 2 ^ length xs * 2 ^ length l2"
442           by (induct "length xs",simp_all)
443         hence "bitval x * 2 ^ (length xs + length l2) + bv_to_nat xs * 2 ^ length l2 =
444           bitval x * 2 ^ length xs * 2 ^ length l2 + bv_to_nat xs * 2 ^ length l2"
445           by simp
446         also have "... = (bitval x * 2 ^ length xs + bv_to_nat xs) * 2 ^ length l2"
447           by (simp add: ring_distribs)
448         finally show ?thesis by simp
449       qed
450     qed
451   qed
452   thus ?thesis ..
453 qed
455 lemma bv_nat_bv [simp]: "bv_to_nat (nat_to_bv n) = n"
456 proof (induct n rule: less_induct)
457   fix n
458   assume ind: "!!j. j < n \<Longrightarrow> bv_to_nat (nat_to_bv j) = j"
459   show "bv_to_nat (nat_to_bv n) = n"
460   proof (rule n_div_2_cases [of n])
461     assume "n = 0" then show ?thesis by simp
462   next
463     assume nn: "n div 2 < n"
464     assume n0: "0 < n"
465     from ind and nn
466     have ind': "bv_to_nat (nat_to_bv (n div 2)) = n div 2" by blast
467     from n0 have n0': "n \<noteq> 0" by simp
468     show ?thesis
469       apply (subst nat_to_bv_def)
470       apply (simp only: nat_to_bv_helper.simps [of n])
471       apply (simp only: n0' if_False)
472       apply (subst unfold_nat_to_bv_helper)
473       apply (subst bv_to_nat_dist_append)
474       apply (fold nat_to_bv_def)
475       apply (simp add: ind' split del: split_if)
476       apply (cases "n mod 2 = 0")
477       proof (simp_all)
478         assume "n mod 2 = 0"
479         with mod_div_equality [of n 2]
480         show "n div 2 * 2 = n" by simp
481       next
482         assume "n mod 2 = Suc 0"
483         with mod_div_equality [of n 2]
484         show "Suc (n div 2 * 2) = n" by arith
485       qed
486   qed
487 qed
489 lemma bv_to_nat_type [simp]: "bv_to_nat (norm_unsigned w) = bv_to_nat w"
490   by (rule bit_list_induct) simp_all
492 lemma length_norm_unsigned_le [simp]: "length (norm_unsigned w) \<le> length w"
493   by (rule bit_list_induct) simp_all
495 lemma bv_to_nat_rew_msb: "bv_msb w = \<one> ==> bv_to_nat w = 2 ^ (length w - 1) + bv_to_nat (tl w)"
496   by (rule bit_list_cases [of w]) simp_all
498 lemma norm_unsigned_result: "norm_unsigned xs = [] \<or> bv_msb (norm_unsigned xs) = \<one>"
499 proof (rule length_induct [of _ xs])
500   fix xs :: "bit list"
501   assume ind: "\<forall>ys. length ys < length xs --> norm_unsigned ys = [] \<or> bv_msb (norm_unsigned ys) = \<one>"
502   show "norm_unsigned xs = [] \<or> bv_msb (norm_unsigned xs) = \<one>"
503   proof (rule bit_list_cases [of xs],simp_all)
504     fix bs
505     assume [simp]: "xs = \<zero>#bs"
506     from ind
507     have "length bs < length xs --> norm_unsigned bs = [] \<or> bv_msb (norm_unsigned bs) = \<one>" ..
508     thus "norm_unsigned bs = [] \<or> bv_msb (norm_unsigned bs) = \<one>" by simp
509   qed
510 qed
512 lemma norm_empty_bv_to_nat_zero:
513   assumes nw: "norm_unsigned w = []"
514   shows       "bv_to_nat w = 0"
515 proof -
516   have "bv_to_nat w = bv_to_nat (norm_unsigned w)" by simp
517   also have "... = bv_to_nat []" by (subst nw) (rule refl)
518   also have "... = 0" by simp
519   finally show ?thesis .
520 qed
522 lemma bv_to_nat_lower_limit:
523   assumes w0: "0 < bv_to_nat w"
524   shows "2 ^ (length (norm_unsigned w) - 1) \<le> bv_to_nat w"
525 proof -
526   from w0 and norm_unsigned_result [of w]
527   have msbw: "bv_msb (norm_unsigned w) = \<one>"
528     by (auto simp add: norm_empty_bv_to_nat_zero)
529   have "2 ^ (length (norm_unsigned w) - 1) \<le> bv_to_nat (norm_unsigned w)"
530     by (subst bv_to_nat_rew_msb [OF msbw],simp)
531   thus ?thesis by simp
532 qed
534 lemmas [simp del] = nat_to_bv_non0
536 lemma norm_unsigned_length [intro!]: "length (norm_unsigned w) \<le> length w"
537 by (subst norm_unsigned_def,rule rem_initial_length)
539 lemma norm_unsigned_equal:
540   "length (norm_unsigned w) = length w ==> norm_unsigned w = w"
541 by (simp add: norm_unsigned_def,rule rem_initial_equal)
543 lemma bv_extend_norm_unsigned: "bv_extend (length w) \<zero> (norm_unsigned w) = w"
544 by (simp add: norm_unsigned_def,rule bv_extend_rem_initial)
546 lemma norm_unsigned_append1 [simp]:
547   "norm_unsigned xs \<noteq> [] ==> norm_unsigned (xs @ ys) = norm_unsigned xs @ ys"
548 by (simp add: norm_unsigned_def,rule rem_initial_append1)
550 lemma norm_unsigned_append2 [simp]:
551   "norm_unsigned xs = [] ==> norm_unsigned (xs @ ys) = norm_unsigned ys"
552 by (simp add: norm_unsigned_def,rule rem_initial_append2)
554 lemma bv_to_nat_zero_imp_empty:
555   "bv_to_nat w = 0 \<Longrightarrow> norm_unsigned w = []"
556 by (atomize (full), induct w rule: bit_list_induct) simp_all
558 lemma bv_to_nat_nzero_imp_nempty:
559   "bv_to_nat w \<noteq> 0 \<Longrightarrow> norm_unsigned w \<noteq> []"
560 by (induct w rule: bit_list_induct) simp_all
562 lemma nat_helper1:
563   assumes ass: "nat_to_bv (bv_to_nat w) = norm_unsigned w"
564   shows        "nat_to_bv (2 * bv_to_nat w + bitval x) = norm_unsigned (w @ [x])"
565 proof (cases x)
566   assume [simp]: "x = \<one>"
567   show ?thesis
568     apply (simp add: nat_to_bv_non0)
569     apply safe
570   proof -
571     fix q
572     assume "Suc (2 * bv_to_nat w) = 2 * q"
573     hence orig: "(2 * bv_to_nat w + 1) mod 2 = 2 * q mod 2" (is "?lhs = ?rhs")
574       by simp
575     have "?lhs = (1 + 2 * bv_to_nat w) mod 2"
577     also have "... = 1"
578       by (subst mod_add_eq) simp
579     finally have eq1: "?lhs = 1" .
580     have "?rhs  = 0" by simp
581     with orig and eq1
582     show "nat_to_bv (Suc (2 * bv_to_nat w) div 2) @ [\<zero>] = norm_unsigned (w @ [\<one>])"
583       by simp
584   next
585     have "nat_to_bv (Suc (2 * bv_to_nat w) div 2) @ [\<one>] =
586         nat_to_bv ((1 + 2 * bv_to_nat w) div 2) @ [\<one>]"
588     also have "... = nat_to_bv (bv_to_nat w) @ [\<one>]"
589       by (subst div_add1_eq) simp
590     also have "... = norm_unsigned w @ [\<one>]"
591       by (subst ass) (rule refl)
592     also have "... = norm_unsigned (w @ [\<one>])"
593       by (cases "norm_unsigned w") simp_all
594     finally show "nat_to_bv (Suc (2 * bv_to_nat w) div 2) @ [\<one>] = norm_unsigned (w @ [\<one>])" .
595   qed
596 next
597   assume [simp]: "x = \<zero>"
598   show ?thesis
599   proof (cases "bv_to_nat w = 0")
600     assume "bv_to_nat w = 0"
601     thus ?thesis
602       by (simp add: bv_to_nat_zero_imp_empty)
603   next
604     assume "bv_to_nat w \<noteq> 0"
605     thus ?thesis
606       apply simp
607       apply (subst nat_to_bv_non0)
608       apply simp
609       apply auto
610       apply (subst ass)
611       apply (cases "norm_unsigned w")
612       apply (simp_all add: norm_empty_bv_to_nat_zero)
613       done
614   qed
615 qed
617 lemma nat_helper2: "nat_to_bv (2 ^ length xs + bv_to_nat xs) = \<one> # xs"
618 proof -
619   have "\<forall>xs. nat_to_bv (2 ^ length (rev xs) + bv_to_nat (rev xs)) = \<one> # (rev xs)" (is "\<forall>xs. ?P xs")
620   proof
621     fix xs
622     show "?P xs"
623     proof (rule length_induct [of _ xs])
624       fix xs :: "bit list"
625       assume ind: "\<forall>ys. length ys < length xs --> ?P ys"
626       show "?P xs"
627       proof (cases xs)
628         assume "xs = []"
629         then show ?thesis by (simp add: nat_to_bv_non0)
630       next
631         fix y ys
632         assume [simp]: "xs = y # ys"
633         show ?thesis
634           apply simp
635           apply (subst bv_to_nat_dist_append)
636           apply simp
637         proof -
638           have "nat_to_bv (2 * 2 ^ length ys + (bv_to_nat (rev ys) * 2 + bitval y)) =
639             nat_to_bv (2 * (2 ^ length ys + bv_to_nat (rev ys)) + bitval y)"
641           also have "... = nat_to_bv (2 * (bv_to_nat (\<one>#rev ys)) + bitval y)"
642             by simp
643           also have "... = norm_unsigned (\<one>#rev ys) @ [y]"
644           proof -
645             from ind
646             have "nat_to_bv (2 ^ length (rev ys) + bv_to_nat (rev ys)) = \<one> # rev ys"
647               by auto
648             hence [simp]: "nat_to_bv (2 ^ length ys + bv_to_nat (rev ys)) = \<one> # rev ys"
649               by simp
650             show ?thesis
651               apply (subst nat_helper1)
652               apply simp_all
653               done
654           qed
655           also have "... = (\<one>#rev ys) @ [y]"
656             by simp
657           also have "... = \<one> # rev ys @ [y]"
658             by simp
659           finally show "nat_to_bv (2 * 2 ^ length ys + (bv_to_nat (rev ys) * 2 + bitval y)) =
660 	      \<one> # rev ys @ [y]" .
661         qed
662       qed
663     qed
664   qed
665   hence "nat_to_bv (2 ^ length (rev (rev xs)) + bv_to_nat (rev (rev xs))) =
666       \<one> # rev (rev xs)" ..
667   thus ?thesis by simp
668 qed
670 lemma nat_bv_nat [simp]: "nat_to_bv (bv_to_nat w) = norm_unsigned w"
671 proof (rule bit_list_induct [of _ w],simp_all)
672   fix xs
673   assume "nat_to_bv (bv_to_nat xs) = norm_unsigned xs"
674   have "bv_to_nat xs = bv_to_nat (norm_unsigned xs)" by simp
675   have "bv_to_nat xs < 2 ^ length xs"
676     by (rule bv_to_nat_upper_range)
677   show "nat_to_bv (2 ^ length xs + bv_to_nat xs) = \<one> # xs"
678     by (rule nat_helper2)
679 qed
681 lemma bv_to_nat_qinj:
682   assumes one: "bv_to_nat xs = bv_to_nat ys"
683   and     len: "length xs = length ys"
684   shows        "xs = ys"
685 proof -
686   from one
687   have "nat_to_bv (bv_to_nat xs) = nat_to_bv (bv_to_nat ys)"
688     by simp
689   hence xsys: "norm_unsigned xs = norm_unsigned ys"
690     by simp
691   have "xs = bv_extend (length xs) \<zero> (norm_unsigned xs)"
692     by (simp add: bv_extend_norm_unsigned)
693   also have "... = bv_extend (length ys) \<zero> (norm_unsigned ys)"
694     by (simp add: xsys len)
695   also have "... = ys"
696     by (simp add: bv_extend_norm_unsigned)
697   finally show ?thesis .
698 qed
700 lemma norm_unsigned_nat_to_bv [simp]:
701   "norm_unsigned (nat_to_bv n) = nat_to_bv n"
702 proof -
703   have "norm_unsigned (nat_to_bv n) = nat_to_bv (bv_to_nat (norm_unsigned (nat_to_bv n)))"
704     by (subst nat_bv_nat) simp
705   also have "... = nat_to_bv n" by simp
706   finally show ?thesis .
707 qed
709 lemma length_nat_to_bv_upper_limit:
710   assumes nk: "n \<le> 2 ^ k - 1"
711   shows       "length (nat_to_bv n) \<le> k"
712 proof (cases "n = 0")
713   case True
714   thus ?thesis
715     by (simp add: nat_to_bv_def nat_to_bv_helper.simps)
716 next
717   case False
718   hence n0: "0 < n" by simp
719   show ?thesis
720   proof (rule ccontr)
721     assume "~ length (nat_to_bv n) \<le> k"
722     hence "k < length (nat_to_bv n)" by simp
723     hence "k \<le> length (nat_to_bv n) - 1" by arith
724     hence "(2::nat) ^ k \<le> 2 ^ (length (nat_to_bv n) - 1)" by simp
725     also have "... = 2 ^ (length (norm_unsigned (nat_to_bv n)) - 1)" by simp
726     also have "... \<le> bv_to_nat (nat_to_bv n)"
727       by (rule bv_to_nat_lower_limit) (simp add: n0)
728     also have "... = n" by simp
729     finally have "2 ^ k \<le> n" .
730     with n0 have "2 ^ k - 1 < n" by arith
731     with nk show False by simp
732   qed
733 qed
735 lemma length_nat_to_bv_lower_limit:
736   assumes nk: "2 ^ k \<le> n"
737   shows       "k < length (nat_to_bv n)"
738 proof (rule ccontr)
739   assume "~ k < length (nat_to_bv n)"
740   hence lnk: "length (nat_to_bv n) \<le> k" by simp
741   have "n = bv_to_nat (nat_to_bv n)" by simp
742   also have "... < 2 ^ length (nat_to_bv n)"
743     by (rule bv_to_nat_upper_range)
744   also from lnk have "... \<le> 2 ^ k" by simp
745   finally have "n < 2 ^ k" .
746   with nk show False by simp
747 qed
750 subsection {* Unsigned Arithmetic Operations *}
752 definition
753   bv_add :: "[bit list, bit list ] => bit list" where
754   "bv_add w1 w2 = nat_to_bv (bv_to_nat w1 + bv_to_nat w2)"
756 lemma bv_add_type1 [simp]: "bv_add (norm_unsigned w1) w2 = bv_add w1 w2"
759 lemma bv_add_type2 [simp]: "bv_add w1 (norm_unsigned w2) = bv_add w1 w2"
762 lemma bv_add_returntype [simp]: "norm_unsigned (bv_add w1 w2) = bv_add w1 w2"
765 lemma bv_add_length: "length (bv_add w1 w2) \<le> Suc (max (length w1) (length w2))"
766 proof (unfold bv_add_def,rule length_nat_to_bv_upper_limit)
767   from bv_to_nat_upper_range [of w1] and bv_to_nat_upper_range [of w2]
768   have "bv_to_nat w1 + bv_to_nat w2 \<le> (2 ^ length w1 - 1) + (2 ^ length w2 - 1)"
769     by arith
770   also have "... \<le>
771       max (2 ^ length w1 - 1) (2 ^ length w2 - 1) + max (2 ^ length w1 - 1) (2 ^ length w2 - 1)"
772     by (rule add_mono,safe intro!: le_maxI1 le_maxI2)
773   also have "... = 2 * max (2 ^ length w1 - 1) (2 ^ length w2 - 1)" by simp
774   also have "... \<le> 2 ^ Suc (max (length w1) (length w2)) - 2"
775   proof (cases "length w1 \<le> length w2")
776     assume w1w2: "length w1 \<le> length w2"
777     hence "(2::nat) ^ length w1 \<le> 2 ^ length w2" by simp
778     hence "(2::nat) ^ length w1 - 1 \<le> 2 ^ length w2 - 1" by arith
779     with w1w2 show ?thesis
780       by (simp add: diff_mult_distrib2 split: split_max)
781   next
782     assume [simp]: "~ (length w1 \<le> length w2)"
783     have "~ ((2::nat) ^ length w1 - 1 \<le> 2 ^ length w2 - 1)"
784     proof
785       assume "(2::nat) ^ length w1 - 1 \<le> 2 ^ length w2 - 1"
786       hence "((2::nat) ^ length w1 - 1) + 1 \<le> (2 ^ length w2 - 1) + 1"
787         by (rule add_right_mono)
788       hence "(2::nat) ^ length w1 \<le> 2 ^ length w2" by simp
789       hence "length w1 \<le> length w2" by simp
790       thus False by simp
791     qed
792     thus ?thesis
793       by (simp add: diff_mult_distrib2 split: split_max)
794   qed
795   finally show "bv_to_nat w1 + bv_to_nat w2 \<le> 2 ^ Suc (max (length w1) (length w2)) - 1"
796     by arith
797 qed
799 definition
800   bv_mult :: "[bit list, bit list ] => bit list" where
801   "bv_mult w1 w2 = nat_to_bv (bv_to_nat w1 * bv_to_nat w2)"
803 lemma bv_mult_type1 [simp]: "bv_mult (norm_unsigned w1) w2 = bv_mult w1 w2"
804   by (simp add: bv_mult_def)
806 lemma bv_mult_type2 [simp]: "bv_mult w1 (norm_unsigned w2) = bv_mult w1 w2"
807   by (simp add: bv_mult_def)
809 lemma bv_mult_returntype [simp]: "norm_unsigned (bv_mult w1 w2) = bv_mult w1 w2"
810   by (simp add: bv_mult_def)
812 lemma bv_mult_length: "length (bv_mult w1 w2) \<le> length w1 + length w2"
813 proof (unfold bv_mult_def,rule length_nat_to_bv_upper_limit)
814   from bv_to_nat_upper_range [of w1] and bv_to_nat_upper_range [of w2]
815   have h: "bv_to_nat w1 \<le> 2 ^ length w1 - 1 \<and> bv_to_nat w2 \<le> 2 ^ length w2 - 1"
816     by arith
817   have "bv_to_nat w1 * bv_to_nat w2 \<le> (2 ^ length w1 - 1) * (2 ^ length w2 - 1)"
818     apply (cut_tac h)
819     apply (rule mult_mono)
820     apply auto
821     done
822   also have "... < 2 ^ length w1 * 2 ^ length w2"
823     by (rule mult_strict_mono,auto)
824   also have "... = 2 ^ (length w1 + length w2)"
826   finally show "bv_to_nat w1 * bv_to_nat w2 \<le> 2 ^ (length w1 + length w2) - 1"
827     by arith
828 qed
830 subsection {* Signed Vectors *}
832 consts
833   norm_signed :: "bit list => bit list"
834 primrec
835   norm_signed_Nil: "norm_signed [] = []"
836   norm_signed_Cons: "norm_signed (b#bs) =
837     (case b of
838       \<zero> => if norm_unsigned bs = [] then [] else b#norm_unsigned bs
839     | \<one> => b#rem_initial b bs)"
841 lemma norm_signed0 [simp]: "norm_signed [\<zero>] = []"
842   by simp
844 lemma norm_signed1 [simp]: "norm_signed [\<one>] = [\<one>]"
845   by simp
847 lemma norm_signed01 [simp]: "norm_signed (\<zero>#\<one>#xs) = \<zero>#\<one>#xs"
848   by simp
850 lemma norm_signed00 [simp]: "norm_signed (\<zero>#\<zero>#xs) = norm_signed (\<zero>#xs)"
851   by simp
853 lemma norm_signed10 [simp]: "norm_signed (\<one>#\<zero>#xs) = \<one>#\<zero>#xs"
854   by simp
856 lemma norm_signed11 [simp]: "norm_signed (\<one>#\<one>#xs) = norm_signed (\<one>#xs)"
857   by simp
859 lemmas [simp del] = norm_signed_Cons
861 definition
862   int_to_bv :: "int => bit list" where
863   "int_to_bv n = (if 0 \<le> n
864                  then norm_signed (\<zero>#nat_to_bv (nat n))
865                  else norm_signed (bv_not (\<zero>#nat_to_bv (nat (-n- 1)))))"
867 lemma int_to_bv_ge0 [simp]: "0 \<le> n ==> int_to_bv n = norm_signed (\<zero> # nat_to_bv (nat n))"
868   by (simp add: int_to_bv_def)
870 lemma int_to_bv_lt0 [simp]:
871     "n < 0 ==> int_to_bv n = norm_signed (bv_not (\<zero>#nat_to_bv (nat (-n- 1))))"
872   by (simp add: int_to_bv_def)
874 lemma norm_signed_idem [simp]: "norm_signed (norm_signed w) = norm_signed w"
875 proof (rule bit_list_induct [of _ w], simp_all)
876   fix xs
877   assume eq: "norm_signed (norm_signed xs) = norm_signed xs"
878   show "norm_signed (norm_signed (\<zero>#xs)) = norm_signed (\<zero>#xs)"
879   proof (rule bit_list_cases [of xs],simp_all)
880     fix ys
881     assume "xs = \<zero>#ys"
882     from this [symmetric] and eq
883     show "norm_signed (norm_signed (\<zero>#ys)) = norm_signed (\<zero>#ys)"
884       by simp
885   qed
886 next
887   fix xs
888   assume eq: "norm_signed (norm_signed xs) = norm_signed xs"
889   show "norm_signed (norm_signed (\<one>#xs)) = norm_signed (\<one>#xs)"
890   proof (rule bit_list_cases [of xs],simp_all)
891     fix ys
892     assume "xs = \<one>#ys"
893     from this [symmetric] and eq
894     show "norm_signed (norm_signed (\<one>#ys)) = norm_signed (\<one>#ys)"
895       by simp
896   qed
897 qed
899 definition
900   bv_to_int :: "bit list => int" where
901   "bv_to_int w =
902     (case bv_msb w of \<zero> => int (bv_to_nat w)
903     | \<one> => - int (bv_to_nat (bv_not w) + 1))"
905 lemma bv_to_int_Nil [simp]: "bv_to_int [] = 0"
906   by (simp add: bv_to_int_def)
908 lemma bv_to_int_Cons0 [simp]: "bv_to_int (\<zero>#bs) = int (bv_to_nat bs)"
909   by (simp add: bv_to_int_def)
911 lemma bv_to_int_Cons1 [simp]: "bv_to_int (\<one>#bs) = - int (bv_to_nat (bv_not bs) + 1)"
912   by (simp add: bv_to_int_def)
914 lemma bv_to_int_type [simp]: "bv_to_int (norm_signed w) = bv_to_int w"
915 proof (rule bit_list_induct [of _ w], simp_all)
916   fix xs
917   assume ind: "bv_to_int (norm_signed xs) = bv_to_int xs"
918   show "bv_to_int (norm_signed (\<zero>#xs)) = int (bv_to_nat xs)"
919   proof (rule bit_list_cases [of xs], simp_all)
920     fix ys
921     assume [simp]: "xs = \<zero>#ys"
922     from ind
923     show "bv_to_int (norm_signed (\<zero>#ys)) = int (bv_to_nat ys)"
924       by simp
925   qed
926 next
927   fix xs
928   assume ind: "bv_to_int (norm_signed xs) = bv_to_int xs"
929   show "bv_to_int (norm_signed (\<one>#xs)) = -1 - int (bv_to_nat (bv_not xs))"
930   proof (rule bit_list_cases [of xs], simp_all)
931     fix ys
932     assume [simp]: "xs = \<one>#ys"
933     from ind
934     show "bv_to_int (norm_signed (\<one>#ys)) = -1 - int (bv_to_nat (bv_not ys))"
935       by simp
936   qed
937 qed
939 lemma bv_to_int_upper_range: "bv_to_int w < 2 ^ (length w - 1)"
940 proof (rule bit_list_cases [of w],simp_all)
941   fix bs
942   from bv_to_nat_upper_range
943   show "int (bv_to_nat bs) < 2 ^ length bs"
944     by (simp add: int_nat_two_exp)
945 next
946   fix bs
947   have "-1 - int (bv_to_nat (bv_not bs)) \<le> 0" by simp
948   also have "... < 2 ^ length bs" by (induct bs) simp_all
949   finally show "-1 - int (bv_to_nat (bv_not bs)) < 2 ^ length bs" .
950 qed
952 lemma bv_to_int_lower_range: "- (2 ^ (length w - 1)) \<le> bv_to_int w"
953 proof (rule bit_list_cases [of w],simp_all)
954   fix bs :: "bit list"
955   have "- (2 ^ length bs) \<le> (0::int)" by (induct bs) simp_all
956   also have "... \<le> int (bv_to_nat bs)" by simp
957   finally show "- (2 ^ length bs) \<le> int (bv_to_nat bs)" .
958 next
959   fix bs
960   from bv_to_nat_upper_range [of "bv_not bs"]
961   show "- (2 ^ length bs) \<le> -1 - int (bv_to_nat (bv_not bs))"
962     by (simp add: int_nat_two_exp)
963 qed
965 lemma int_bv_int [simp]: "int_to_bv (bv_to_int w) = norm_signed w"
966 proof (rule bit_list_cases [of w],simp)
967   fix xs
968   assume [simp]: "w = \<zero>#xs"
969   show ?thesis
970     apply simp
971     apply (subst norm_signed_Cons [of "\<zero>" "xs"])
972     apply simp
973     using norm_unsigned_result [of xs]
974     apply safe
975     apply (rule bit_list_cases [of "norm_unsigned xs"])
976     apply simp_all
977     done
978 next
979   fix xs
980   assume [simp]: "w = \<one>#xs"
981   show ?thesis
982     apply (simp del: int_to_bv_lt0)
983     apply (rule bit_list_induct [of _ xs])
984     apply simp
985     apply (subst int_to_bv_lt0)
986     apply (subgoal_tac "- int (bv_to_nat (bv_not (\<zero> # bs))) + -1 < 0 + 0")
987     apply simp
988     apply (rule add_le_less_mono)
989     apply simp
990     apply simp
991     apply (simp del: bv_to_nat1 bv_to_nat_helper)
992     apply simp
993     done
994 qed
996 lemma bv_int_bv [simp]: "bv_to_int (int_to_bv i) = i"
997   by (cases "0 \<le> i") simp_all
999 lemma bv_msb_norm [simp]: "bv_msb (norm_signed w) = bv_msb w"
1000   by (rule bit_list_cases [of w]) (simp_all add: norm_signed_Cons)
1002 lemma norm_signed_length: "length (norm_signed w) \<le> length w"
1003   apply (cases w, simp_all)
1004   apply (subst norm_signed_Cons)
1005   apply (case_tac a, simp_all)
1006   apply (rule rem_initial_length)
1007   done
1009 lemma norm_signed_equal: "length (norm_signed w) = length w ==> norm_signed w = w"
1010 proof (rule bit_list_cases [of w], simp_all)
1011   fix xs
1012   assume "length (norm_signed (\<zero>#xs)) = Suc (length xs)"
1013   thus "norm_signed (\<zero>#xs) = \<zero>#xs"
1014     apply (simp add: norm_signed_Cons)
1015     apply safe
1016     apply simp_all
1017     apply (rule norm_unsigned_equal)
1018     apply assumption
1019     done
1020 next
1021   fix xs
1022   assume "length (norm_signed (\<one>#xs)) = Suc (length xs)"
1023   thus "norm_signed (\<one>#xs) = \<one>#xs"
1024     apply (simp add: norm_signed_Cons)
1025     apply (rule rem_initial_equal)
1026     apply assumption
1027     done
1028 qed
1030 lemma bv_extend_norm_signed: "bv_msb w = b ==> bv_extend (length w) b (norm_signed w) = w"
1031 proof (rule bit_list_cases [of w],simp_all)
1032   fix xs
1033   show "bv_extend (Suc (length xs)) \<zero> (norm_signed (\<zero>#xs)) = \<zero>#xs"
1034   proof (simp add: norm_signed_list_def,auto)
1035     assume "norm_unsigned xs = []"
1036     hence xx: "rem_initial \<zero> xs = []"
1037       by (simp add: norm_unsigned_def)
1038     have "bv_extend (Suc (length xs)) \<zero> (\<zero>#rem_initial \<zero> xs) = \<zero>#xs"
1039       apply (simp add: bv_extend_def replicate_app_Cons_same)
1040       apply (fold bv_extend_def)
1041       apply (rule bv_extend_rem_initial)
1042       done
1043     thus "bv_extend (Suc (length xs)) \<zero> [\<zero>] = \<zero>#xs"
1044       by (simp add: xx)
1045   next
1046     show "bv_extend (Suc (length xs)) \<zero> (\<zero>#norm_unsigned xs) = \<zero>#xs"
1047       apply (simp add: norm_unsigned_def)
1048       apply (simp add: bv_extend_def replicate_app_Cons_same)
1049       apply (fold bv_extend_def)
1050       apply (rule bv_extend_rem_initial)
1051       done
1052   qed
1053 next
1054   fix xs
1055   show "bv_extend (Suc (length xs)) \<one> (norm_signed (\<one>#xs)) = \<one>#xs"
1056     apply (simp add: norm_signed_Cons)
1057     apply (simp add: bv_extend_def replicate_app_Cons_same)
1058     apply (fold bv_extend_def)
1059     apply (rule bv_extend_rem_initial)
1060     done
1061 qed
1063 lemma bv_to_int_qinj:
1064   assumes one: "bv_to_int xs = bv_to_int ys"
1065   and     len: "length xs = length ys"
1066   shows        "xs = ys"
1067 proof -
1068   from one
1069   have "int_to_bv (bv_to_int xs) = int_to_bv (bv_to_int ys)" by simp
1070   hence xsys: "norm_signed xs = norm_signed ys" by simp
1071   hence xsys': "bv_msb xs = bv_msb ys"
1072   proof -
1073     have "bv_msb xs = bv_msb (norm_signed xs)" by simp
1074     also have "... = bv_msb (norm_signed ys)" by (simp add: xsys)
1075     also have "... = bv_msb ys" by simp
1076     finally show ?thesis .
1077   qed
1078   have "xs = bv_extend (length xs) (bv_msb xs) (norm_signed xs)"
1079     by (simp add: bv_extend_norm_signed)
1080   also have "... = bv_extend (length ys) (bv_msb ys) (norm_signed ys)"
1081     by (simp add: xsys xsys' len)
1082   also have "... = ys"
1083     by (simp add: bv_extend_norm_signed)
1084   finally show ?thesis .
1085 qed
1087 lemma int_to_bv_returntype [simp]: "norm_signed (int_to_bv w) = int_to_bv w"
1088   by (simp add: int_to_bv_def)
1090 lemma bv_to_int_msb0: "0 \<le> bv_to_int w1 ==> bv_msb w1 = \<zero>"
1091   by (rule bit_list_cases,simp_all)
1093 lemma bv_to_int_msb1: "bv_to_int w1 < 0 ==> bv_msb w1 = \<one>"
1094   by (rule bit_list_cases,simp_all)
1096 lemma bv_to_int_lower_limit_gt0:
1097   assumes w0: "0 < bv_to_int w"
1098   shows       "2 ^ (length (norm_signed w) - 2) \<le> bv_to_int w"
1099 proof -
1100   from w0
1101   have "0 \<le> bv_to_int w" by simp
1102   hence [simp]: "bv_msb w = \<zero>" by (rule bv_to_int_msb0)
1103   have "2 ^ (length (norm_signed w) - 2) \<le> bv_to_int (norm_signed w)"
1104   proof (rule bit_list_cases [of w])
1105     assume "w = []"
1106     with w0 show ?thesis by simp
1107   next
1108     fix w'
1109     assume weq: "w = \<zero> # w'"
1110     thus ?thesis
1111     proof (simp add: norm_signed_Cons,safe)
1112       assume "norm_unsigned w' = []"
1113       with weq and w0 show False
1114 	by (simp add: norm_empty_bv_to_nat_zero)
1115     next
1116       assume w'0: "norm_unsigned w' \<noteq> []"
1117       have "0 < bv_to_nat w'"
1118       proof (rule ccontr)
1119         assume "~ (0 < bv_to_nat w')"
1120         hence "bv_to_nat w' = 0"
1121           by arith
1122         hence "norm_unsigned w' = []"
1123           by (simp add: bv_to_nat_zero_imp_empty)
1124         with w'0
1125         show False by simp
1126       qed
1127       with bv_to_nat_lower_limit [of w']
1128       show "2 ^ (length (norm_unsigned w') - Suc 0) \<le> int (bv_to_nat w')"
1129         by (simp add: int_nat_two_exp)
1130     qed
1131   next
1132     fix w'
1133     assume "w = \<one> # w'"
1134     from w0 have "bv_msb w = \<zero>" by simp
1135     with prems show ?thesis by simp
1136   qed
1137   also have "...  = bv_to_int w" by simp
1138   finally show ?thesis .
1139 qed
1141 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   apply (rule bit_list_cases [of w],simp_all)
1143   apply (case_tac "bs",simp_all)
1144   apply (case_tac "a",simp_all)
1145   apply (simp add: norm_signed_Cons)
1146   apply safe
1147   apply simp
1148 proof -
1149   fix l
1150   assume msb: "\<zero> = bv_msb (norm_unsigned l)"
1151   assume "norm_unsigned l \<noteq> []"
1152   with norm_unsigned_result [of l]
1153   have "bv_msb (norm_unsigned l) = \<one>" by simp
1154   with msb show False by simp
1155 next
1156   fix xs
1157   assume p: "\<one> = bv_msb (tl (norm_signed (\<one> # xs)))"
1158   have "\<one> \<noteq> bv_msb (tl (norm_signed (\<one> # xs)))"
1159     by (rule bit_list_induct [of _ xs],simp_all)
1160   with p show False by simp
1161 qed
1163 lemma bv_to_int_upper_limit_lem1:
1164   assumes w0: "bv_to_int w < -1"
1165   shows       "bv_to_int w < - (2 ^ (length (norm_signed w) - 2))"
1166 proof -
1167   from w0
1168   have "bv_to_int w < 0" by simp
1169   hence msbw [simp]: "bv_msb w = \<one>"
1170     by (rule bv_to_int_msb1)
1171   have "bv_to_int w = bv_to_int (norm_signed w)" by simp
1172   also from norm_signed_result [of w]
1173   have "... < - (2 ^ (length (norm_signed w) - 2))"
1174   proof safe
1175     assume "norm_signed w = []"
1176     hence "bv_to_int (norm_signed w) = 0" by simp
1177     with w0 show ?thesis by simp
1178   next
1179     assume "norm_signed w = [\<one>]"
1180     hence "bv_to_int (norm_signed w) = -1" by simp
1181     with w0 show ?thesis by simp
1182   next
1183     assume "bv_msb (norm_signed w) \<noteq> bv_msb (tl (norm_signed w))"
1184     hence msb_tl: "\<one> \<noteq> bv_msb (tl (norm_signed w))" by simp
1185     show "bv_to_int (norm_signed w) < - (2 ^ (length (norm_signed w) - 2))"
1186     proof (rule bit_list_cases [of "norm_signed w"])
1187       assume "norm_signed w = []"
1188       hence "bv_to_int (norm_signed w) = 0" by simp
1189       with w0 show ?thesis by simp
1190     next
1191       fix w'
1192       assume nw: "norm_signed w = \<zero> # w'"
1193       from msbw have "bv_msb (norm_signed w) = \<one>" by simp
1194       with nw show ?thesis by simp
1195     next
1196       fix w'
1197       assume weq: "norm_signed w = \<one> # w'"
1198       show ?thesis
1199       proof (rule bit_list_cases [of w'])
1200         assume w'eq: "w' = []"
1201         from w0 have "bv_to_int (norm_signed w) < -1" by simp
1202         with w'eq and weq show ?thesis by simp
1203       next
1204         fix w''
1205         assume w'eq: "w' = \<zero> # w''"
1206         show ?thesis
1207           apply (simp add: weq w'eq)
1208           apply (subgoal_tac "- int (bv_to_nat (bv_not w'')) + -1 < 0 + 0")
1209           apply (simp add: int_nat_two_exp)
1210           apply (rule add_le_less_mono)
1211           apply simp_all
1212           done
1213       next
1214         fix w''
1215         assume w'eq: "w' = \<one> # w''"
1216         with weq and msb_tl show ?thesis by simp
1217       qed
1218     qed
1219   qed
1220   finally show ?thesis .
1221 qed
1223 lemma length_int_to_bv_upper_limit_gt0:
1224   assumes w0: "0 < i"
1225   and     wk: "i \<le> 2 ^ (k - 1) - 1"
1226   shows       "length (int_to_bv i) \<le> k"
1227 proof (rule ccontr)
1228   from w0 wk
1229   have k1: "1 < k"
1230     by (cases "k - 1",simp_all)
1231   assume "~ length (int_to_bv i) \<le> k"
1232   hence "k < length (int_to_bv i)" by simp
1233   hence "k \<le> length (int_to_bv i) - 1" by arith
1234   hence a: "k - 1 \<le> length (int_to_bv i) - 2" by arith
1235   hence "(2::int) ^ (k - 1) \<le> 2 ^ (length (int_to_bv i) - 2)" by simp
1236   also have "... \<le> i"
1237   proof -
1238     have "2 ^ (length (norm_signed (int_to_bv i)) - 2) \<le> bv_to_int (int_to_bv i)"
1239     proof (rule bv_to_int_lower_limit_gt0)
1240       from w0 show "0 < bv_to_int (int_to_bv i)" by simp
1241     qed
1242     thus ?thesis by simp
1243   qed
1244   finally have "2 ^ (k - 1) \<le> i" .
1245   with wk show False by simp
1246 qed
1248 lemma pos_length_pos:
1249   assumes i0: "0 < bv_to_int w"
1250   shows       "0 < length w"
1251 proof -
1252   from norm_signed_result [of w]
1253   have "0 < length (norm_signed w)"
1254   proof (auto)
1255     assume ii: "norm_signed w = []"
1256     have "bv_to_int (norm_signed w) = 0" by (subst ii) simp
1257     hence "bv_to_int w = 0" by simp
1258     with i0 show False by simp
1259   next
1260     assume ii: "norm_signed w = []"
1261     assume jj: "bv_msb w \<noteq> \<zero>"
1262     have "\<zero> = bv_msb (norm_signed w)"
1263       by (subst ii) simp
1264     also have "... \<noteq> \<zero>"
1265       by (simp add: jj)
1266     finally show False by simp
1267   qed
1268   also have "... \<le> length w"
1269     by (rule norm_signed_length)
1270   finally show ?thesis .
1271 qed
1273 lemma neg_length_pos:
1274   assumes i0: "bv_to_int w < -1"
1275   shows       "0 < length w"
1276 proof -
1277   from norm_signed_result [of w]
1278   have "0 < length (norm_signed w)"
1279   proof (auto)
1280     assume ii: "norm_signed w = []"
1281     have "bv_to_int (norm_signed w) = 0"
1282       by (subst ii) simp
1283     hence "bv_to_int w = 0" by simp
1284     with i0 show False by simp
1285   next
1286     assume ii: "norm_signed w = []"
1287     assume jj: "bv_msb w \<noteq> \<zero>"
1288     have "\<zero> = bv_msb (norm_signed w)" by (subst ii) simp
1289     also have "... \<noteq> \<zero>" by (simp add: jj)
1290     finally show False by simp
1291   qed
1292   also have "... \<le> length w"
1293     by (rule norm_signed_length)
1294   finally show ?thesis .
1295 qed
1297 lemma length_int_to_bv_lower_limit_gt0:
1298   assumes wk: "2 ^ (k - 1) \<le> i"
1299   shows       "k < length (int_to_bv i)"
1300 proof (rule ccontr)
1301   have "0 < (2::int) ^ (k - 1)"
1302     by (rule zero_less_power) simp
1303   also have "... \<le> i" by (rule wk)
1304   finally have i0: "0 < i" .
1305   have lii0: "0 < length (int_to_bv i)"
1306     apply (rule pos_length_pos)
1307     apply (simp,rule i0)
1308     done
1309   assume "~ k < length (int_to_bv i)"
1310   hence "length (int_to_bv i) \<le> k" by simp
1311   with lii0
1312   have a: "length (int_to_bv i) - 1 \<le> k - 1"
1313     by arith
1314   have "i < 2 ^ (length (int_to_bv i) - 1)"
1315   proof -
1316     have "i = bv_to_int (int_to_bv i)"
1317       by simp
1318     also have "... < 2 ^ (length (int_to_bv i) - 1)"
1319       by (rule bv_to_int_upper_range)
1320     finally show ?thesis .
1321   qed
1322   also have "(2::int) ^ (length (int_to_bv i) - 1) \<le> 2 ^ (k - 1)" using a
1323     by simp
1324   finally have "i < 2 ^ (k - 1)" .
1325   with wk show False by simp
1326 qed
1328 lemma length_int_to_bv_upper_limit_lem1:
1329   assumes w1: "i < -1"
1330   and     wk: "- (2 ^ (k - 1)) \<le> i"
1331   shows       "length (int_to_bv i) \<le> k"
1332 proof (rule ccontr)
1333   from w1 wk
1334   have k1: "1 < k" by (cases "k - 1") simp_all
1335   assume "~ length (int_to_bv i) \<le> k"
1336   hence "k < length (int_to_bv i)" by simp
1337   hence "k \<le> length (int_to_bv i) - 1" by arith
1338   hence a: "k - 1 \<le> length (int_to_bv i) - 2" by arith
1339   have "i < - (2 ^ (length (int_to_bv i) - 2))"
1340   proof -
1341     have "i = bv_to_int (int_to_bv i)"
1342       by simp
1343     also have "... < - (2 ^ (length (norm_signed (int_to_bv i)) - 2))"
1344       by (rule bv_to_int_upper_limit_lem1,simp,rule w1)
1345     finally show ?thesis by simp
1346   qed
1347   also have "... \<le> -(2 ^ (k - 1))"
1348   proof -
1349     have "(2::int) ^ (k - 1) \<le> 2 ^ (length (int_to_bv i) - 2)" using a by simp
1350     thus ?thesis by simp
1351   qed
1352   finally have "i < -(2 ^ (k - 1))" .
1353   with wk show False by simp
1354 qed
1356 lemma length_int_to_bv_lower_limit_lem1:
1357   assumes wk: "i < -(2 ^ (k - 1))"
1358   shows       "k < length (int_to_bv i)"
1359 proof (rule ccontr)
1360   from wk have "i \<le> -(2 ^ (k - 1)) - 1" by simp
1361   also have "... < -1"
1362   proof -
1363     have "0 < (2::int) ^ (k - 1)"
1364       by (rule zero_less_power) simp
1365     hence "-((2::int) ^ (k - 1)) < 0" by simp
1366     thus ?thesis by simp
1367   qed
1368   finally have i1: "i < -1" .
1369   have lii0: "0 < length (int_to_bv i)"
1370     apply (rule neg_length_pos)
1371     apply (simp, rule i1)
1372     done
1373   assume "~ k < length (int_to_bv i)"
1374   hence "length (int_to_bv i) \<le> k"
1375     by simp
1376   with lii0 have a: "length (int_to_bv i) - 1 \<le> k - 1" by arith
1377   hence "(2::int) ^ (length (int_to_bv i) - 1) \<le> 2 ^ (k - 1)" by simp
1378   hence "-((2::int) ^ (k - 1)) \<le> - (2 ^ (length (int_to_bv i) - 1))" by simp
1379   also have "... \<le> i"
1380   proof -
1381     have "- (2 ^ (length (int_to_bv i) - 1)) \<le> bv_to_int (int_to_bv i)"
1382       by (rule bv_to_int_lower_range)
1383     also have "... = i"
1384       by simp
1385     finally show ?thesis .
1386   qed
1387   finally have "-(2 ^ (k - 1)) \<le> i" .
1388   with wk show False by simp
1389 qed
1392 subsection {* Signed Arithmetic Operations *}
1394 subsubsection {* Conversion from unsigned to signed *}
1396 definition
1397   utos :: "bit list => bit list" where
1398   "utos w = norm_signed (\<zero> # w)"
1400 lemma utos_type [simp]: "utos (norm_unsigned w) = utos w"
1401   by (simp add: utos_def norm_signed_Cons)
1403 lemma utos_returntype [simp]: "norm_signed (utos w) = utos w"
1404   by (simp add: utos_def)
1406 lemma utos_length: "length (utos w) \<le> Suc (length w)"
1407   by (simp add: utos_def norm_signed_Cons)
1409 lemma bv_to_int_utos: "bv_to_int (utos w) = int (bv_to_nat w)"
1410 proof (simp add: utos_def norm_signed_Cons, safe)
1411   assume "norm_unsigned w = []"
1412   hence "bv_to_nat (norm_unsigned w) = 0" by simp
1413   thus "bv_to_nat w = 0" by simp
1414 qed
1417 subsubsection {* Unary minus *}
1419 definition
1420   bv_uminus :: "bit list => bit list" where
1421   "bv_uminus w = int_to_bv (- bv_to_int w)"
1423 lemma bv_uminus_type [simp]: "bv_uminus (norm_signed w) = bv_uminus w"
1424   by (simp add: bv_uminus_def)
1426 lemma bv_uminus_returntype [simp]: "norm_signed (bv_uminus w) = bv_uminus w"
1427   by (simp add: bv_uminus_def)
1429 lemma bv_uminus_length: "length (bv_uminus w) \<le> Suc (length w)"
1430 proof -
1431   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"
1432     by arith
1433   thus ?thesis
1434   proof safe
1435     assume p: "1 < - bv_to_int w"
1436     have lw: "0 < length w"
1437       apply (rule neg_length_pos)
1438       using p
1439       apply simp
1440       done
1441     show ?thesis
1442     proof (simp add: bv_uminus_def,rule length_int_to_bv_upper_limit_gt0,simp_all)
1443       from prems show "bv_to_int w < 0" by simp
1444     next
1445       have "-(2^(length w - 1)) \<le> bv_to_int w"
1446         by (rule bv_to_int_lower_range)
1447       hence "- bv_to_int w \<le> 2^(length w - 1)" by simp
1448       also from lw have "... < 2 ^ length w" by simp
1449       finally show "- bv_to_int w < 2 ^ length w" by simp
1450     qed
1451   next
1452     assume p: "- bv_to_int w = 1"
1453     hence lw: "0 < length w" by (cases w) simp_all
1454     from p
1455     show ?thesis
1456       apply (simp add: bv_uminus_def)
1457       using lw
1458       apply (simp (no_asm) add: nat_to_bv_non0)
1459       done
1460   next
1461     assume "- bv_to_int w = 0"
1462     thus ?thesis by (simp add: bv_uminus_def)
1463   next
1464     assume p: "- bv_to_int w = -1"
1465     thus ?thesis by (simp add: bv_uminus_def)
1466   next
1467     assume p: "- bv_to_int w < -1"
1468     show ?thesis
1469       apply (simp add: bv_uminus_def)
1470       apply (rule length_int_to_bv_upper_limit_lem1)
1471       apply (rule p)
1472       apply simp
1473     proof -
1474       have "bv_to_int w < 2 ^ (length w - 1)"
1475         by (rule bv_to_int_upper_range)
1476       also have "... \<le> 2 ^ length w" by simp
1477       finally show "bv_to_int w \<le> 2 ^ length w" by simp
1478     qed
1479   qed
1480 qed
1482 lemma bv_uminus_length_utos: "length (bv_uminus (utos w)) \<le> Suc (length w)"
1483 proof -
1484   have "-bv_to_int (utos w) = 0 \<or> -bv_to_int (utos w) = -1 \<or> -bv_to_int (utos w) < -1"
1485     by (simp add: bv_to_int_utos, arith)
1486   thus ?thesis
1487   proof safe
1488     assume "-bv_to_int (utos w) = 0"
1489     thus ?thesis by (simp add: bv_uminus_def)
1490   next
1491     assume "-bv_to_int (utos w) = -1"
1492     thus ?thesis by (simp add: bv_uminus_def)
1493   next
1494     assume p: "-bv_to_int (utos w) < -1"
1495     show ?thesis
1496       apply (simp add: bv_uminus_def)
1497       apply (rule length_int_to_bv_upper_limit_lem1)
1498       apply (rule p)
1499       apply (simp add: bv_to_int_utos)
1500       using bv_to_nat_upper_range [of w]
1501       apply (simp add: int_nat_two_exp)
1502       done
1503   qed
1504 qed
1506 definition
1507   bv_sadd :: "[bit list, bit list ] => bit list" where
1508   "bv_sadd w1 w2 = int_to_bv (bv_to_int w1 + bv_to_int w2)"
1510 lemma bv_sadd_type1 [simp]: "bv_sadd (norm_signed w1) w2 = bv_sadd w1 w2"
1513 lemma bv_sadd_type2 [simp]: "bv_sadd w1 (norm_signed w2) = bv_sadd w1 w2"
1516 lemma bv_sadd_returntype [simp]: "norm_signed (bv_sadd w1 w2) = bv_sadd w1 w2"
1520   assumes lw: "0 < max (length w1) (length w2)"
1521   shows   "((2::int) ^ (length w1 - 1)) + (2 ^ (length w2 - 1)) \<le> 2 ^ max (length w1) (length w2)"
1522 proof -
1523   have "((2::int) ^ (length w1 - 1)) + (2 ^ (length w2 - 1)) \<le>
1524       2 ^ (max (length w1) (length w2) - 1) + 2 ^ (max (length w1) (length w2) - 1)"
1525     apply (cases "length w1 \<le> length w2")
1526     apply (auto simp add: max_def)
1527     done
1528   also have "... = 2 ^ max (length w1) (length w2)"
1529   proof -
1530     from lw
1531     show ?thesis
1532       apply simp
1533       apply (subst power_Suc [symmetric])
1534       apply (simp del: power_int.simps)
1535       done
1536   qed
1537   finally show ?thesis .
1538 qed
1540 lemma bv_sadd_length: "length (bv_sadd w1 w2) \<le> Suc (max (length w1) (length w2))"
1541 proof -
1542   let ?Q = "bv_to_int w1 + bv_to_int w2"
1544   have helper: "?Q \<noteq> 0 ==> 0 < max (length w1) (length w2)"
1545   proof -
1546     assume p: "?Q \<noteq> 0"
1547     show "0 < max (length w1) (length w2)"
1548     proof (simp add: less_max_iff_disj,rule)
1549       assume [simp]: "w1 = []"
1550       show "w2 \<noteq> []"
1551       proof (rule ccontr,simp)
1552         assume [simp]: "w2 = []"
1553         from p show False by simp
1554       qed
1555     qed
1556   qed
1558   have "0 < ?Q \<or> ?Q = 0 \<or> ?Q = -1 \<or> ?Q < -1" by arith
1559   thus ?thesis
1560   proof safe
1561     assume "?Q = 0"
1562     thus ?thesis
1564   next
1565     assume "?Q = -1"
1566     thus ?thesis
1568   next
1569     assume p: "0 < ?Q"
1570     show ?thesis
1572       apply (rule length_int_to_bv_upper_limit_gt0)
1573       apply (rule p)
1574     proof simp
1575       from bv_to_int_upper_range [of w2]
1576       have "bv_to_int w2 \<le> 2 ^ (length w2 - 1)"
1577         by simp
1578       with bv_to_int_upper_range [of w1]
1579       have "bv_to_int w1 + bv_to_int w2 < (2 ^ (length w1 - 1)) + (2 ^ (length w2 - 1))"
1580         by (rule zadd_zless_mono)
1581       also have "... \<le> 2 ^ max (length w1) (length w2)"
1582         apply (rule adder_helper)
1583         apply (rule helper)
1584         using p
1585         apply simp
1586         done
1587       finally show "?Q < 2 ^ max (length w1) (length w2)" .
1588     qed
1589   next
1590     assume p: "?Q < -1"
1591     show ?thesis
1593       apply (rule length_int_to_bv_upper_limit_lem1,simp_all)
1594       apply (rule p)
1595     proof -
1596       have "(2 ^ (length w1 - 1)) + 2 ^ (length w2 - 1) \<le> (2::int) ^ max (length w1) (length w2)"
1597         apply (rule adder_helper)
1598         apply (rule helper)
1599         using p
1600         apply simp
1601         done
1602       hence "-((2::int) ^ max (length w1) (length w2)) \<le> - (2 ^ (length w1 - 1)) + -(2 ^ (length w2 - 1))"
1603         by simp
1604       also have "- (2 ^ (length w1 - 1)) + -(2 ^ (length w2 - 1)) \<le> ?Q"
1605         apply (rule add_mono)
1606         apply (rule bv_to_int_lower_range [of w1])
1607         apply (rule bv_to_int_lower_range [of w2])
1608         done
1609       finally show "- (2^max (length w1) (length w2)) \<le> ?Q" .
1610     qed
1611   qed
1612 qed
1614 definition
1615   bv_sub :: "[bit list, bit list] => bit list" where
1616   "bv_sub w1 w2 = bv_sadd w1 (bv_uminus w2)"
1618 lemma bv_sub_type1 [simp]: "bv_sub (norm_signed w1) w2 = bv_sub w1 w2"
1619   by (simp add: bv_sub_def)
1621 lemma bv_sub_type2 [simp]: "bv_sub w1 (norm_signed w2) = bv_sub w1 w2"
1622   by (simp add: bv_sub_def)
1624 lemma bv_sub_returntype [simp]: "norm_signed (bv_sub w1 w2) = bv_sub w1 w2"
1625   by (simp add: bv_sub_def)
1627 lemma bv_sub_length: "length (bv_sub w1 w2) \<le> Suc (max (length w1) (length w2))"
1628 proof (cases "bv_to_int w2 = 0")
1629   assume p: "bv_to_int w2 = 0"
1630   show ?thesis
1631   proof (simp add: bv_sub_def bv_sadd_def bv_uminus_def p)
1632     have "length (norm_signed w1) \<le> length w1"
1633       by (rule norm_signed_length)
1634     also have "... \<le> max (length w1) (length w2)"
1635       by (rule le_maxI1)
1636     also have "... \<le> Suc (max (length w1) (length w2))"
1637       by arith
1638     finally show "length (norm_signed w1) \<le> Suc (max (length w1) (length w2))" .
1639   qed
1640 next
1641   assume "bv_to_int w2 \<noteq> 0"
1642   hence "0 < length w2" by (cases w2,simp_all)
1643   hence lmw: "0 < max (length w1) (length w2)" by arith
1645   let ?Q = "bv_to_int w1 - bv_to_int w2"
1647   have "0 < ?Q \<or> ?Q = 0 \<or> ?Q = -1 \<or> ?Q < -1" by arith
1648   thus ?thesis
1649   proof safe
1650     assume "?Q = 0"
1651     thus ?thesis
1652       by (simp add: bv_sub_def bv_sadd_def bv_uminus_def)
1653   next
1654     assume "?Q = -1"
1655     thus ?thesis
1656       by (simp add: bv_sub_def bv_sadd_def bv_uminus_def)
1657   next
1658     assume p: "0 < ?Q"
1659     show ?thesis
1660       apply (simp add: bv_sub_def bv_sadd_def bv_uminus_def)
1661       apply (rule length_int_to_bv_upper_limit_gt0)
1662       apply (rule p)
1663     proof simp
1664       from bv_to_int_lower_range [of w2]
1665       have v2: "- bv_to_int w2 \<le> 2 ^ (length w2 - 1)" by simp
1666       have "bv_to_int w1 + - bv_to_int w2 < (2 ^ (length w1 - 1)) + (2 ^ (length w2 - 1))"
1667         apply (rule zadd_zless_mono)
1668         apply (rule bv_to_int_upper_range [of w1])
1669         apply (rule v2)
1670         done
1671       also have "... \<le> 2 ^ max (length w1) (length w2)"
1672         apply (rule adder_helper)
1673         apply (rule lmw)
1674         done
1675       finally show "?Q < 2 ^ max (length w1) (length w2)" by simp
1676     qed
1677   next
1678     assume p: "?Q < -1"
1679     show ?thesis
1680       apply (simp add: bv_sub_def bv_sadd_def bv_uminus_def)
1681       apply (rule length_int_to_bv_upper_limit_lem1)
1682       apply (rule p)
1683     proof simp
1684       have "(2 ^ (length w1 - 1)) + 2 ^ (length w2 - 1) \<le> (2::int) ^ max (length w1) (length w2)"
1685         apply (rule adder_helper)
1686         apply (rule lmw)
1687         done
1688       hence "-((2::int) ^ max (length w1) (length w2)) \<le> - (2 ^ (length w1 - 1)) + -(2 ^ (length w2 - 1))"
1689         by simp
1690       also have "- (2 ^ (length w1 - 1)) + -(2 ^ (length w2 - 1)) \<le> bv_to_int w1 + -bv_to_int w2"
1691         apply (rule add_mono)
1692         apply (rule bv_to_int_lower_range [of w1])
1693         using bv_to_int_upper_range [of w2]
1694         apply simp
1695         done
1696       finally show "- (2^max (length w1) (length w2)) \<le> ?Q" by simp
1697     qed
1698   qed
1699 qed
1701 definition
1702   bv_smult :: "[bit list, bit list] => bit list" where
1703   "bv_smult w1 w2 = int_to_bv (bv_to_int w1 * bv_to_int w2)"
1705 lemma bv_smult_type1 [simp]: "bv_smult (norm_signed w1) w2 = bv_smult w1 w2"
1706   by (simp add: bv_smult_def)
1708 lemma bv_smult_type2 [simp]: "bv_smult w1 (norm_signed w2) = bv_smult w1 w2"
1709   by (simp add: bv_smult_def)
1711 lemma bv_smult_returntype [simp]: "norm_signed (bv_smult w1 w2) = bv_smult w1 w2"
1712   by (simp add: bv_smult_def)
1714 lemma bv_smult_length: "length (bv_smult w1 w2) \<le> length w1 + length w2"
1715 proof -
1716   let ?Q = "bv_to_int w1 * bv_to_int w2"
1718   have lmw: "?Q \<noteq> 0 ==> 0 < length w1 \<and> 0 < length w2" by auto
1720   have "0 < ?Q \<or> ?Q = 0 \<or> ?Q = -1 \<or> ?Q < -1" by arith
1721   thus ?thesis
1722   proof (safe dest!: iffD1 [OF mult_eq_0_iff])
1723     assume "bv_to_int w1 = 0"
1724     thus ?thesis by (simp add: bv_smult_def)
1725   next
1726     assume "bv_to_int w2 = 0"
1727     thus ?thesis by (simp add: bv_smult_def)
1728   next
1729     assume p: "?Q = -1"
1730     show ?thesis
1731       apply (simp add: bv_smult_def p)
1732       apply (cut_tac lmw)
1733       apply arith
1734       using p
1735       apply simp
1736       done
1737   next
1738     assume p: "0 < ?Q"
1739     thus ?thesis
1740     proof (simp add: zero_less_mult_iff,safe)
1741       assume bi1: "0 < bv_to_int w1"
1742       assume bi2: "0 < bv_to_int w2"
1743       show ?thesis
1744         apply (simp add: bv_smult_def)
1745         apply (rule length_int_to_bv_upper_limit_gt0)
1746         apply (rule p)
1747       proof simp
1748         have "?Q < 2 ^ (length w1 - 1) * 2 ^ (length w2 - 1)"
1749           apply (rule mult_strict_mono)
1750           apply (rule bv_to_int_upper_range)
1751           apply (rule bv_to_int_upper_range)
1752           apply (rule zero_less_power)
1753           apply simp
1754           using bi2
1755           apply simp
1756           done
1757         also have "... \<le> 2 ^ (length w1 + length w2 - Suc 0)"
1758           apply simp
1759           apply (subst zpower_zadd_distrib [symmetric])
1760           apply simp
1761           done
1762         finally show "?Q < 2 ^ (length w1 + length w2 - Suc 0)" .
1763       qed
1764     next
1765       assume bi1: "bv_to_int w1 < 0"
1766       assume bi2: "bv_to_int w2 < 0"
1767       show ?thesis
1768         apply (simp add: bv_smult_def)
1769         apply (rule length_int_to_bv_upper_limit_gt0)
1770         apply (rule p)
1771       proof simp
1772         have "-bv_to_int w1 * -bv_to_int w2 \<le> 2 ^ (length w1 - 1) * 2 ^(length w2 - 1)"
1773           apply (rule mult_mono)
1774           using bv_to_int_lower_range [of w1]
1775           apply simp
1776           using bv_to_int_lower_range [of w2]
1777           apply simp
1778           apply (rule zero_le_power,simp)
1779           using bi2
1780           apply simp
1781           done
1782         hence "?Q \<le> 2 ^ (length w1 - 1) * 2 ^(length w2 - 1)"
1783           by simp
1784         also have "... < 2 ^ (length w1 + length w2 - Suc 0)"
1785           apply simp
1786           apply (subst zpower_zadd_distrib [symmetric])
1787           apply simp
1788           apply (cut_tac lmw)
1789           apply arith
1790           apply (cut_tac p)
1791           apply arith
1792           done
1793         finally show "?Q < 2 ^ (length w1 + length w2 - Suc 0)" .
1794       qed
1795     qed
1796   next
1797     assume p: "?Q < -1"
1798     show ?thesis
1799       apply (subst bv_smult_def)
1800       apply (rule length_int_to_bv_upper_limit_lem1)
1801       apply (rule p)
1802     proof simp
1803       have "(2::int) ^ (length w1 - 1) * 2 ^(length w2 - 1) \<le> 2 ^ (length w1 + length w2 - Suc 0)"
1804         apply simp
1805         apply (subst zpower_zadd_distrib [symmetric])
1806         apply simp
1807         done
1808       hence "-((2::int) ^ (length w1 + length w2 - Suc 0)) \<le> -(2^(length w1 - 1) * 2 ^ (length w2 - 1))"
1809         by simp
1810       also have "... \<le> ?Q"
1811       proof -
1812         from p
1813         have q: "bv_to_int w1 * bv_to_int w2 < 0"
1814           by simp
1815         thus ?thesis
1816         proof (simp add: mult_less_0_iff,safe)
1817           assume bi1: "0 < bv_to_int w1"
1818           assume bi2: "bv_to_int w2 < 0"
1819           have "-bv_to_int w2 * bv_to_int w1 \<le> ((2::int)^(length w2 - 1)) * (2 ^ (length w1 - 1))"
1820             apply (rule mult_mono)
1821             using bv_to_int_lower_range [of w2]
1822             apply simp
1823             using bv_to_int_upper_range [of w1]
1824             apply simp
1825             apply (rule zero_le_power,simp)
1826             using bi1
1827             apply simp
1828             done
1829           hence "-?Q \<le> ((2::int)^(length w1 - 1)) * (2 ^ (length w2 - 1))"
1830             by (simp add: zmult_ac)
1831           thus "-(((2::int)^(length w1 - Suc 0)) * (2 ^ (length w2 - Suc 0))) \<le> ?Q"
1832             by simp
1833         next
1834           assume bi1: "bv_to_int w1 < 0"
1835           assume bi2: "0 < bv_to_int w2"
1836           have "-bv_to_int w1 * bv_to_int w2 \<le> ((2::int)^(length w1 - 1)) * (2 ^ (length w2 - 1))"
1837             apply (rule mult_mono)
1838             using bv_to_int_lower_range [of w1]
1839             apply simp
1840             using bv_to_int_upper_range [of w2]
1841             apply simp
1842             apply (rule zero_le_power,simp)
1843             using bi2
1844             apply simp
1845             done
1846           hence "-?Q \<le> ((2::int)^(length w1 - 1)) * (2 ^ (length w2 - 1))"
1847             by (simp add: zmult_ac)
1848           thus "-(((2::int)^(length w1 - Suc 0)) * (2 ^ (length w2 - Suc 0))) \<le> ?Q"
1849             by simp
1850         qed
1851       qed
1852       finally show "-(2 ^ (length w1 + length w2 - Suc 0)) \<le> ?Q" .
1853     qed
1854   qed
1855 qed
1857 lemma bv_msb_one: "bv_msb w = \<one> ==> bv_to_nat w \<noteq> 0"
1858 by (cases w) simp_all
1860 lemma bv_smult_length_utos: "length (bv_smult (utos w1) w2) \<le> length w1 + length w2"
1861 proof -
1862   let ?Q = "bv_to_int (utos w1) * bv_to_int w2"
1864   have lmw: "?Q \<noteq> 0 ==> 0 < length (utos w1) \<and> 0 < length w2" by auto
1866   have "0 < ?Q \<or> ?Q = 0 \<or> ?Q = -1 \<or> ?Q < -1" by arith
1867   thus ?thesis
1868   proof (safe dest!: iffD1 [OF mult_eq_0_iff])
1869     assume "bv_to_int (utos w1) = 0"
1870     thus ?thesis by (simp add: bv_smult_def)
1871   next
1872     assume "bv_to_int w2 = 0"
1873     thus ?thesis by (simp add: bv_smult_def)
1874   next
1875     assume p: "0 < ?Q"
1876     thus ?thesis
1877     proof (simp add: zero_less_mult_iff,safe)
1878       assume biw2: "0 < bv_to_int w2"
1879       show ?thesis
1880         apply (simp add: bv_smult_def)
1881         apply (rule length_int_to_bv_upper_limit_gt0)
1882         apply (rule p)
1883       proof simp
1884         have "?Q < 2 ^ length w1 * 2 ^ (length w2 - 1)"
1885           apply (rule mult_strict_mono)
1886           apply (simp add: bv_to_int_utos int_nat_two_exp)
1887           apply (rule bv_to_nat_upper_range)
1888           apply (rule bv_to_int_upper_range)
1889           apply (rule zero_less_power,simp)
1890           using biw2
1891           apply simp
1892           done
1893         also have "... \<le> 2 ^ (length w1 + length w2 - Suc 0)"
1894           apply simp
1895           apply (subst zpower_zadd_distrib [symmetric])
1896           apply simp
1897           apply (cut_tac lmw)
1898           apply arith
1899           using p
1900           apply auto
1901           done
1902         finally show "?Q < 2 ^ (length w1 + length w2 - Suc 0)" .
1903       qed
1904     next
1905       assume "bv_to_int (utos w1) < 0"
1906       thus ?thesis by (simp add: bv_to_int_utos)
1907     qed
1908   next
1909     assume p: "?Q = -1"
1910     thus ?thesis
1911       apply (simp add: bv_smult_def)
1912       apply (cut_tac lmw)
1913       apply arith
1914       apply simp
1915       done
1916   next
1917     assume p: "?Q < -1"
1918     show ?thesis
1919       apply (subst bv_smult_def)
1920       apply (rule length_int_to_bv_upper_limit_lem1)
1921       apply (rule p)
1922     proof simp
1923       have "(2::int) ^ length w1 * 2 ^(length w2 - 1) \<le> 2 ^ (length w1 + length w2 - Suc 0)"
1924         apply simp
1925         apply (subst zpower_zadd_distrib [symmetric])
1926         apply simp
1927         apply (cut_tac lmw)
1928         apply arith
1929         apply (cut_tac p)
1930         apply arith
1931         done
1932       hence "-((2::int) ^ (length w1 + length w2 - Suc 0)) \<le> -(2^ length w1 * 2 ^ (length w2 - 1))"
1933         by simp
1934       also have "... \<le> ?Q"
1935       proof -
1936         from p
1937         have q: "bv_to_int (utos w1) * bv_to_int w2 < 0"
1938           by simp
1939         thus ?thesis
1940         proof (simp add: mult_less_0_iff,safe)
1941           assume bi1: "0 < bv_to_int (utos w1)"
1942           assume bi2: "bv_to_int w2 < 0"
1943           have "-bv_to_int w2 * bv_to_int (utos w1) \<le> ((2::int)^(length w2 - 1)) * (2 ^ length w1)"
1944             apply (rule mult_mono)
1945             using bv_to_int_lower_range [of w2]
1946             apply simp
1947             apply (simp add: bv_to_int_utos)
1948             using bv_to_nat_upper_range [of w1]
1949             apply (simp add: int_nat_two_exp)
1950             apply (rule zero_le_power,simp)
1951             using bi1
1952             apply simp
1953             done
1954           hence "-?Q \<le> ((2::int)^length w1) * (2 ^ (length w2 - 1))"
1955             by (simp add: zmult_ac)
1956           thus "-(((2::int)^length w1) * (2 ^ (length w2 - Suc 0))) \<le> ?Q"
1957             by simp
1958         next
1959           assume bi1: "bv_to_int (utos w1) < 0"
1960           thus "-(((2::int)^length w1) * (2 ^ (length w2 - Suc 0))) \<le> ?Q"
1961             by (simp add: bv_to_int_utos)
1962         qed
1963       qed
1964       finally show "-(2 ^ (length w1 + length w2 - Suc 0)) \<le> ?Q" .
1965     qed
1966   qed
1967 qed
1969 lemma bv_smult_sym: "bv_smult w1 w2 = bv_smult w2 w1"
1970   by (simp add: bv_smult_def zmult_ac)
1972 subsection {* Structural operations *}
1974 definition
1975   bv_select :: "[bit list,nat] => bit" where
1976   "bv_select w i = w ! (length w - 1 - i)"
1978 definition
1979   bv_chop :: "[bit list,nat] => bit list * bit list" where
1980   "bv_chop w i = (let len = length w in (take (len - i) w,drop (len - i) w))"
1982 definition
1983   bv_slice :: "[bit list,nat*nat] => bit list" where
1984   "bv_slice w = (\<lambda>(b,e). fst (bv_chop (snd (bv_chop w (b+1))) e))"
1986 lemma bv_select_rev:
1987   assumes notnull: "n < length w"
1988   shows            "bv_select w n = rev w ! n"
1989 proof -
1990   have "\<forall>n. n < length w --> bv_select w n = rev w ! n"
1991   proof (rule length_induct [of _ w],auto simp add: bv_select_def)
1992     fix xs :: "bit list"
1993     fix n
1994     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 notx: "n < length xs"
1996     show "xs ! (length xs - Suc n) = rev xs ! n"
1997     proof (cases xs)
1998       assume "xs = []"
1999       with notx show ?thesis by simp
2000     next
2001       fix y ys
2002       assume [simp]: "xs = y # ys"
2003       show ?thesis
2004       proof (auto simp add: nth_append)
2005         assume noty: "n < length ys"
2006         from spec [OF ind,of ys]
2007         have "\<forall>n. n < length ys --> ys ! (length ys - Suc n) = rev ys ! n"
2008           by simp
2009         hence "n < length ys --> ys ! (length ys - Suc n) = rev ys ! n" ..
2010 	from this and noty
2011         have "ys ! (length ys - Suc n) = rev ys ! n" ..
2012         thus "(y # ys) ! (length ys - n) = rev ys ! n"
2013           by (simp add: nth_Cons' noty linorder_not_less [symmetric])
2014       next
2015         assume "~ n < length ys"
2016         hence x: "length ys \<le> n" by simp
2017         from notx have "n < Suc (length ys)" by simp
2018         hence "n \<le> length ys" by simp
2019         with x have "length ys = n" by simp
2020         thus "y = [y] ! (n - length ys)" by simp
2021       qed
2022     qed
2023   qed
2024   then have "n < length w --> bv_select w n = rev w ! n" ..
2025   from this and notnull show ?thesis ..
2026 qed
2028 lemma bv_chop_append: "bv_chop (w1 @ w2) (length w2) = (w1,w2)"
2029   by (simp add: bv_chop_def Let_def)
2031 lemma append_bv_chop_id: "fst (bv_chop w l) @ snd (bv_chop w l) = w"
2032   by (simp add: bv_chop_def Let_def)
2034 lemma bv_chop_length_fst [simp]: "length (fst (bv_chop w i)) = length w - i"
2035   by (simp add: bv_chop_def Let_def)
2037 lemma bv_chop_length_snd [simp]: "length (snd (bv_chop w i)) = min i (length w)"
2038   by (simp add: bv_chop_def Let_def)
2040 lemma bv_slice_length [simp]: "[| j \<le> i; i < length w |] ==> length (bv_slice w (i,j)) = i - j + 1"
2041   by (auto simp add: bv_slice_def)
2043 definition
2044   length_nat :: "nat => nat" where
2045   [code del]: "length_nat x = (LEAST n. x < 2 ^ n)"
2047 lemma length_nat: "length (nat_to_bv n) = length_nat n"
2048   apply (simp add: length_nat_def)
2049   apply (rule Least_equality [symmetric])
2050   prefer 2
2051   apply (rule length_nat_to_bv_upper_limit)
2052   apply arith
2053   apply (rule ccontr)
2054 proof -
2055   assume "~ n < 2 ^ length (nat_to_bv n)"
2056   hence "2 ^ length (nat_to_bv n) \<le> n" by simp
2057   hence "length (nat_to_bv n) < length (nat_to_bv n)"
2058     by (rule length_nat_to_bv_lower_limit)
2059   thus False by simp
2060 qed
2062 lemma length_nat_0 [simp]: "length_nat 0 = 0"
2063   by (simp add: length_nat_def Least_equality)
2065 lemma length_nat_non0:
2066   assumes n0: "n \<noteq> 0"
2067   shows       "length_nat n = Suc (length_nat (n div 2))"
2068   apply (simp add: length_nat [symmetric])
2069   apply (subst nat_to_bv_non0 [of n])
2070   apply (simp_all add: n0)
2071   done
2073 definition
2074   length_int :: "int => nat" where
2075   "length_int x =
2076     (if 0 < x then Suc (length_nat (nat x))
2077     else if x = 0 then 0
2078     else Suc (length_nat (nat (-x - 1))))"
2080 lemma length_int: "length (int_to_bv i) = length_int i"
2081 proof (cases "0 < i")
2082   assume i0: "0 < i"
2083   hence "length (int_to_bv i) =
2084       length (norm_signed (\<zero> # norm_unsigned (nat_to_bv (nat i))))" by simp
2085   also from norm_unsigned_result [of "nat_to_bv (nat i)"]
2086   have "... = Suc (length_nat (nat i))"
2087     apply safe
2088     apply (simp del: norm_unsigned_nat_to_bv)
2089     apply (drule norm_empty_bv_to_nat_zero)
2090     using prems
2091     apply simp
2092     apply (cases "norm_unsigned (nat_to_bv (nat i))")
2093     apply (drule norm_empty_bv_to_nat_zero [of "nat_to_bv (nat i)"])
2094     using prems
2095     apply simp
2096     apply simp
2097     using prems
2098     apply (simp add: length_nat [symmetric])
2099     done
2100   finally show ?thesis
2101     using i0
2102     by (simp add: length_int_def)
2103 next
2104   assume "~ 0 < i"
2105   hence i0: "i \<le> 0" by simp
2106   show ?thesis
2107   proof (cases "i = 0")
2108     assume "i = 0"
2109     thus ?thesis by (simp add: length_int_def)
2110   next
2111     assume "i \<noteq> 0"
2112     with i0 have i0: "i < 0" by simp
2113     hence "length (int_to_bv i) =
2114         length (norm_signed (\<one> # bv_not (norm_unsigned (nat_to_bv (nat (- i) - 1)))))"
2115       by (simp add: int_to_bv_def nat_diff_distrib)
2116     also from norm_unsigned_result [of "nat_to_bv (nat (- i) - 1)"]
2117     have "... = Suc (length_nat (nat (- i) - 1))"
2118       apply safe
2119       apply (simp del: norm_unsigned_nat_to_bv)
2120       apply (drule norm_empty_bv_to_nat_zero [of "nat_to_bv (nat (-i) - Suc 0)"])
2121       using prems
2122       apply simp
2123       apply (cases "- i - 1 = 0")
2124       apply simp
2125       apply (simp add: length_nat [symmetric])
2126       apply (cases "norm_unsigned (nat_to_bv (nat (- i) - 1))")
2127       apply simp
2128       apply simp
2129       done
2130     finally
2131     show ?thesis
2132       using i0 by (simp add: length_int_def nat_diff_distrib del: int_to_bv_lt0)
2133   qed
2134 qed
2136 lemma length_int_0 [simp]: "length_int 0 = 0"
2137   by (simp add: length_int_def)
2139 lemma length_int_gt0: "0 < i ==> length_int i = Suc (length_nat (nat i))"
2140   by (simp add: length_int_def)
2142 lemma length_int_lt0: "i < 0 ==> length_int i = Suc (length_nat (nat (- i) - 1))"
2143   by (simp add: length_int_def nat_diff_distrib)
2145 lemma bv_chopI: "[| w = w1 @ w2 ; i = length w2 |] ==> bv_chop w i = (w1,w2)"
2146   by (simp add: bv_chop_def Let_def)
2148 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"
2149   apply (simp add: bv_slice_def)
2150   apply (subst bv_chopI [of "w1 @ w2 @ w3" w1 "w2 @ w3"])
2151   apply simp
2152   apply simp
2153   apply simp
2154   apply (subst bv_chopI [of "w2 @ w3" w2 w3],simp_all)
2155   done
2157 lemma bv_slice_bv_slice:
2158   assumes ki: "k \<le> i"
2159   and     ij: "i \<le> j"
2160   and     jl: "j \<le> l"
2161   and     lw: "l < length w"
2162   shows       "bv_slice w (j,i) = bv_slice (bv_slice w (l,k)) (j-k,i-k)"
2163 proof -
2164   def w1  == "fst (bv_chop w (Suc l))"
2165   and w2  == "fst (bv_chop (snd (bv_chop w (Suc l))) (Suc j))"
2166   and w3  == "fst (bv_chop (snd (bv_chop (snd (bv_chop w (Suc l))) (Suc j))) i)"
2167   and w4  == "fst (bv_chop (snd (bv_chop (snd (bv_chop (snd (bv_chop w (Suc l))) (Suc j))) i)) k)"
2168   and w5  == "snd (bv_chop (snd (bv_chop (snd (bv_chop (snd (bv_chop w (Suc l))) (Suc j))) i)) k)"
2169   note w_defs = this
2171   have w_def: "w = w1 @ w2 @ w3 @ w4 @ w5"
2172     by (simp add: w_defs append_bv_chop_id)
2174   from ki ij jl lw
2175   show ?thesis
2176     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"])
2177     apply simp_all
2178     apply (rule w_def)
2179     apply (simp add: w_defs min_def)
2180     apply (simp add: w_defs min_def)
2181     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])
2182     apply simp_all
2183     apply (rule w_def)
2184     apply (simp add: w_defs min_def)
2185     apply (simp add: w_defs min_def)
2186     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])
2187     apply simp_all
2188     apply (simp_all add: w_defs min_def)
2189     done
2190 qed
2192 lemma bv_to_nat_extend [simp]: "bv_to_nat (bv_extend n \<zero> w) = bv_to_nat w"
2193   apply (simp add: bv_extend_def)
2194   apply (subst bv_to_nat_dist_append)
2195   apply simp
2196   apply (induct "n - length w")
2197    apply simp_all
2198   done
2200 lemma bv_msb_extend_same [simp]: "bv_msb w = b ==> bv_msb (bv_extend n b w) = b"
2201   apply (simp add: bv_extend_def)
2202   apply (induct "n - length w")
2203    apply simp_all
2204   done
2206 lemma bv_to_int_extend [simp]:
2207   assumes a: "bv_msb w = b"
2208   shows      "bv_to_int (bv_extend n b w) = bv_to_int w"
2209 proof (cases "bv_msb w")
2210   assume [simp]: "bv_msb w = \<zero>"
2211   with a have [simp]: "b = \<zero>" by simp
2212   show ?thesis by (simp add: bv_to_int_def)
2213 next
2214   assume [simp]: "bv_msb w = \<one>"
2215   with a have [simp]: "b = \<one>" by simp
2216   show ?thesis
2217     apply (simp add: bv_to_int_def)
2218     apply (simp add: bv_extend_def)
2219     apply (induct "n - length w",simp_all)
2220     done
2221 qed
2223 lemma length_nat_mono [simp]: "x \<le> y ==> length_nat x \<le> length_nat y"
2224 proof (rule ccontr)
2225   assume xy: "x \<le> y"
2226   assume "~ length_nat x \<le> length_nat y"
2227   hence lxly: "length_nat y < length_nat x"
2228     by simp
2229   hence "length_nat y < (LEAST n. x < 2 ^ n)"
2230     by (simp add: length_nat_def)
2231   hence "~ x < 2 ^ length_nat y"
2232     by (rule not_less_Least)
2233   hence xx: "2 ^ length_nat y \<le> x"
2234     by simp
2235   have yy: "y < 2 ^ length_nat y"
2236     apply (simp add: length_nat_def)
2237     apply (rule LeastI)
2238     apply (subgoal_tac "y < 2 ^ y",assumption)
2239     apply (cases "0 \<le> y")
2240     apply (induct y,simp_all)
2241     done
2242   with xx have "y < x" by simp
2243   with xy show False by simp
2244 qed
2246 lemma length_nat_mono_int [simp]: "x \<le> y ==> length_nat x \<le> length_nat y"
2247   by (rule length_nat_mono) arith
2249 lemma length_nat_pos [simp,intro!]: "0 < x ==> 0 < length_nat x"
2250   by (simp add: length_nat_non0)
2252 lemma length_int_mono_gt0: "[| 0 \<le> x ; x \<le> y |] ==> length_int x \<le> length_int y"
2253   by (cases "x = 0") (simp_all add: length_int_gt0 nat_le_eq_zle)
2255 lemma length_int_mono_lt0: "[| x \<le> y ; y \<le> 0 |] ==> length_int y \<le> length_int x"
2256   by (cases "y = 0") (simp_all add: length_int_lt0)
2258 lemmas [simp] = length_nat_non0
2260 lemma "nat_to_bv (number_of Int.Pls) = []"
2261   by simp
2263 consts
2264   fast_bv_to_nat_helper :: "[bit list, int] => int"
2265 primrec
2266   fast_bv_to_nat_Nil: "fast_bv_to_nat_helper [] k = k"
2267   fast_bv_to_nat_Cons: "fast_bv_to_nat_helper (b#bs) k =
2268     fast_bv_to_nat_helper bs ((bit_case Int.Bit0 Int.Bit1 b) k)"
2270 declare fast_bv_to_nat_helper.simps [code del]
2272 lemma fast_bv_to_nat_Cons0: "fast_bv_to_nat_helper (\<zero>#bs) bin =
2273     fast_bv_to_nat_helper bs (Int.Bit0 bin)"
2274   by simp
2276 lemma fast_bv_to_nat_Cons1: "fast_bv_to_nat_helper (\<one>#bs) bin =
2277     fast_bv_to_nat_helper bs (Int.Bit1 bin)"
2278   by simp
2280 lemma fast_bv_to_nat_def:
2281   "bv_to_nat bs == number_of (fast_bv_to_nat_helper bs Int.Pls)"
2282 proof (simp add: bv_to_nat_def)
2283   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)"
2284     apply (induct bs,simp)
2285     apply (case_tac a,simp_all)
2286     done
2287   thus "foldl (\<lambda>bn b. 2 * bn + bitval b) 0 bs \<equiv> number_of (fast_bv_to_nat_helper bs Int.Pls)"
2288     by (simp del: nat_numeral_0_eq_0 add: nat_numeral_0_eq_0 [symmetric])
2289 qed
2291 declare fast_bv_to_nat_Cons [simp del]
2292 declare fast_bv_to_nat_Cons0 [simp]
2293 declare fast_bv_to_nat_Cons1 [simp]
2295 setup {*
2296 (*comments containing lcp are the removal of fast_bv_of_nat*)
2297 let
2298   fun is_const_bool (Const("True",_)) = true
2299     | is_const_bool (Const("False",_)) = true
2300     | is_const_bool _ = false
2301   fun is_const_bit (Const("Word.bit.Zero",_)) = true
2302     | is_const_bit (Const("Word.bit.One",_)) = true
2303     | is_const_bit _ = false
2304   fun num_is_usable (Const(@{const_name Int.Pls},_)) = true
2305     | num_is_usable (Const(@{const_name Int.Min},_)) = false
2306     | num_is_usable (Const(@{const_name Int.Bit0},_) \$ w) =
2307         num_is_usable w
2308     | num_is_usable (Const(@{const_name Int.Bit1},_) \$ w) =
2309         num_is_usable w
2310     | num_is_usable _ = false
2311   fun vec_is_usable (Const("List.list.Nil",_)) = true
2312     | vec_is_usable (Const("List.list.Cons",_) \$ b \$ bs) =
2313         vec_is_usable bs andalso is_const_bit b
2314     | vec_is_usable _ = false
2315   (*lcp** val fast1_th = PureThy.get_thm thy "Word.fast_nat_to_bv_def"*)
2316   val fast2_th = @{thm "Word.fast_bv_to_nat_def"};
2317   (*lcp** fun f sg thms (Const("Word.nat_to_bv",_) \$ (Const(@{const_name Int.number_of},_) \$ t)) =
2318     if num_is_usable t
2319       then SOME (Drule.cterm_instantiate [(cterm_of sg (Var (("w", 0), @{typ int})), cterm_of sg t)] fast1_th)
2320       else NONE
2321     | f _ _ _ = NONE *)
2322   fun g sg thms (Const("Word.bv_to_nat",_) \$ (t as (Const("List.list.Cons",_) \$ _ \$ _))) =
2323         if vec_is_usable t then
2324           SOME (Drule.cterm_instantiate [(cterm_of sg (Var(("bs",0),Type("List.list",[Type("Word.bit",[])]))),cterm_of sg t)] fast2_th)
2325         else NONE
2326     | g _ _ _ = NONE
2327   (*lcp** val simproc1 = Simplifier.simproc thy "nat_to_bv" ["Word.nat_to_bv (number_of w)"] f *)
2328   val simproc2 = Simplifier.simproc @{theory} "bv_to_nat" ["Word.bv_to_nat (x # xs)"] g
2329 in
2330   Simplifier.map_simpset (fn ss => ss addsimprocs [(*lcp*simproc1,*)simproc2])
2331 end*}
2333 declare bv_to_nat1 [simp del]
2334 declare bv_to_nat_helper [simp del]
2336 definition
2337   bv_mapzip :: "[bit => bit => bit,bit list, bit list] => bit list" where
2338   "bv_mapzip f w1 w2 =
2339     (let g = bv_extend (max (length w1) (length w2)) \<zero>
2340      in map (split f) (zip (g w1) (g w2)))"
2342 lemma bv_length_bv_mapzip [simp]:
2343     "length (bv_mapzip f w1 w2) = max (length w1) (length w2)"
2344   by (simp add: bv_mapzip_def Let_def split: split_max)
2346 lemma bv_mapzip_Nil [simp]: "bv_mapzip f [] [] = []"
2347   by (simp add: bv_mapzip_def Let_def)
2349 lemma bv_mapzip_Cons [simp]: "length w1 = length w2 ==>
2350     bv_mapzip f (x#w1) (y#w2) = f x y # bv_mapzip f w1 w2"
2351   by (simp add: bv_mapzip_def Let_def)
2353 end