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