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