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