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