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