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