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