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