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