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