dropped old Library/Word.thy and toy example ex/Adder.thy
authorhaftmann
Mon May 17 10:58:31 2010 +0200 (2010-05-17)
changeset 369625fb251d1c32f
parent 36954 ef698bd61057
child 36963 9a017146675f
dropped old Library/Word.thy and toy example ex/Adder.thy
src/HOL/IsaMakefile
src/HOL/Library/Library.thy
src/HOL/Library/Word.thy
src/HOL/ex/Codegenerator_Candidates.thy
src/HOL/ex/ROOT.ML
     1.1 --- a/src/HOL/IsaMakefile	Sun May 16 00:02:11 2010 +0200
     1.2 +++ b/src/HOL/IsaMakefile	Mon May 17 10:58:31 2010 +0200
     1.3 @@ -410,7 +410,7 @@
     1.4    Library/Library.thy Library/List_Prefix.thy Library/List_Set.thy	\
     1.5    Library/State_Monad.thy Library/Multiset.thy Library/Permutation.thy	\
     1.6    Library/Quotient_Type.thy Library/Quicksort.thy			\
     1.7 -  Library/Nat_Infinity.thy Library/Word.thy Library/README.html		\
     1.8 +  Library/Nat_Infinity.thy Library/README.html				\
     1.9    Library/Continuity.thy Library/Order_Relation.thy			\
    1.10    Library/Nested_Environment.thy Library/Ramsey.thy Library/Zorn.thy	\
    1.11    Library/Library/ROOT.ML Library/Library/document/root.tex		\
     2.1 --- a/src/HOL/Library/Library.thy	Sun May 16 00:02:11 2010 +0200
     2.2 +++ b/src/HOL/Library/Library.thy	Mon May 17 10:58:31 2010 +0200
     2.3 @@ -61,7 +61,6 @@
     2.4    Transitive_Closure_Table
     2.5    Univ_Poly
     2.6    While_Combinator
     2.7 -  Word
     2.8    Zorn
     2.9  begin
    2.10  end
     3.1 --- a/src/HOL/Library/Word.thy	Sun May 16 00:02:11 2010 +0200
     3.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.3 @@ -1,2314 +0,0 @@
     3.4 -(*  Title:      HOL/Library/Word.thy
     3.5 -    Author:     Sebastian Skalberg, TU Muenchen
     3.6 -*)
     3.7 -
     3.8 -header {* Binary Words *}
     3.9 -
    3.10 -theory Word
    3.11 -imports Main
    3.12 -begin
    3.13 -
    3.14 -subsection {* Auxilary Lemmas *}
    3.15 -
    3.16 -lemma max_le [intro!]: "[| x \<le> z; y \<le> z |] ==> max x y \<le> z"
    3.17 -  by (simp add: max_def)
    3.18 -
    3.19 -lemma max_mono:
    3.20 -  fixes x :: "'a::linorder"
    3.21 -  assumes mf: "mono f"
    3.22 -  shows       "max (f x) (f y) \<le> f (max x y)"
    3.23 -proof -
    3.24 -  from mf and le_maxI1 [of x y]
    3.25 -  have fx: "f x \<le> f (max x y)" by (rule monoD)
    3.26 -  from mf and le_maxI2 [of y x]
    3.27 -  have fy: "f y \<le> f (max x y)" by (rule monoD)
    3.28 -  from fx and fy
    3.29 -  show "max (f x) (f y) \<le> f (max x y)" by auto
    3.30 -qed
    3.31 -
    3.32 -declare zero_le_power [intro]
    3.33 -  and zero_less_power [intro]
    3.34 -
    3.35 -lemma int_nat_two_exp: "2 ^ k = int (2 ^ k)"
    3.36 -  by (simp add: zpower_int [symmetric])
    3.37 -
    3.38 -
    3.39 -subsection {* Bits *}
    3.40 -
    3.41 -datatype bit =
    3.42 -    Zero ("\<zero>")
    3.43 -  | One ("\<one>")
    3.44 -
    3.45 -primrec bitval :: "bit => nat" where
    3.46 -    "bitval \<zero> = 0"
    3.47 -  | "bitval \<one> = 1"
    3.48 -
    3.49 -primrec bitnot :: "bit => bit" where
    3.50 -    bitnot_zero: "(bitnot \<zero>) = \<one>"
    3.51 -  | bitnot_one : "(bitnot \<one>)  = \<zero>"
    3.52 -
    3.53 -primrec bitand :: "bit => bit => bit" (infixr "bitand" 35) where
    3.54 -    bitand_zero: "(\<zero> bitand y) = \<zero>"
    3.55 -  | bitand_one:  "(\<one> bitand y) = y"
    3.56 -
    3.57 -primrec bitor  :: "bit => bit => bit" (infixr "bitor"  30) where
    3.58 -    bitor_zero: "(\<zero> bitor y) = y"
    3.59 -  | bitor_one:  "(\<one> bitor y) = \<one>"
    3.60 -
    3.61 -primrec bitxor :: "bit => bit => bit" (infixr "bitxor" 30) where
    3.62 -    bitxor_zero: "(\<zero> bitxor y) = y"
    3.63 -  | bitxor_one:  "(\<one> bitxor y) = (bitnot y)"
    3.64 -
    3.65 -notation (xsymbols)
    3.66 -  bitnot ("\<not>\<^sub>b _" [40] 40) and
    3.67 -  bitand (infixr "\<and>\<^sub>b" 35) and
    3.68 -  bitor  (infixr "\<or>\<^sub>b" 30) and
    3.69 -  bitxor (infixr "\<oplus>\<^sub>b" 30)
    3.70 -
    3.71 -notation (HTML output)
    3.72 -  bitnot ("\<not>\<^sub>b _" [40] 40) and
    3.73 -  bitand (infixr "\<and>\<^sub>b" 35) and
    3.74 -  bitor  (infixr "\<or>\<^sub>b" 30) and
    3.75 -  bitxor (infixr "\<oplus>\<^sub>b" 30)
    3.76 -
    3.77 -lemma bitnot_bitnot [simp]: "(bitnot (bitnot b)) = b"
    3.78 -  by (cases b) simp_all
    3.79 -
    3.80 -lemma bitand_cancel [simp]: "(b bitand b) = b"
    3.81 -  by (cases b) simp_all
    3.82 -
    3.83 -lemma bitor_cancel [simp]: "(b bitor b) = b"
    3.84 -  by (cases b) simp_all
    3.85 -
    3.86 -lemma bitxor_cancel [simp]: "(b bitxor b) = \<zero>"
    3.87 -  by (cases b) simp_all
    3.88 -
    3.89 -
    3.90 -subsection {* Bit Vectors *}
    3.91 -
    3.92 -text {* First, a couple of theorems expressing case analysis and
    3.93 -induction principles for bit vectors. *}
    3.94 -
    3.95 -lemma bit_list_cases:
    3.96 -  assumes empty: "w = [] ==> P w"
    3.97 -  and     zero:  "!!bs. w = \<zero> # bs ==> P w"
    3.98 -  and     one:   "!!bs. w = \<one> # bs ==> P w"
    3.99 -  shows   "P w"
   3.100 -proof (cases w)
   3.101 -  assume "w = []"
   3.102 -  thus ?thesis by (rule empty)
   3.103 -next
   3.104 -  fix b bs
   3.105 -  assume [simp]: "w = b # bs"
   3.106 -  show "P w"
   3.107 -  proof (cases b)
   3.108 -    assume "b = \<zero>"
   3.109 -    hence "w = \<zero> # bs" by simp
   3.110 -    thus ?thesis by (rule zero)
   3.111 -  next
   3.112 -    assume "b = \<one>"
   3.113 -    hence "w = \<one> # bs" by simp
   3.114 -    thus ?thesis by (rule one)
   3.115 -  qed
   3.116 -qed
   3.117 -
   3.118 -lemma bit_list_induct:
   3.119 -  assumes empty: "P []"
   3.120 -  and     zero:  "!!bs. P bs ==> P (\<zero>#bs)"
   3.121 -  and     one:   "!!bs. P bs ==> P (\<one>#bs)"
   3.122 -  shows   "P w"
   3.123 -proof (induct w, simp_all add: empty)
   3.124 -  fix b bs
   3.125 -  assume "P bs"
   3.126 -  then show "P (b#bs)"
   3.127 -    by (cases b) (auto intro!: zero one)
   3.128 -qed
   3.129 -
   3.130 -definition
   3.131 -  bv_msb :: "bit list => bit" where
   3.132 -  "bv_msb w = (if w = [] then \<zero> else hd w)"
   3.133 -
   3.134 -definition
   3.135 -  bv_extend :: "[nat,bit,bit list]=>bit list" where
   3.136 -  "bv_extend i b w = (replicate (i - length w) b) @ w"
   3.137 -
   3.138 -definition
   3.139 -  bv_not :: "bit list => bit list" where
   3.140 -  "bv_not w = map bitnot w"
   3.141 -
   3.142 -lemma bv_length_extend [simp]: "length w \<le> i ==> length (bv_extend i b w) = i"
   3.143 -  by (simp add: bv_extend_def)
   3.144 -
   3.145 -lemma bv_not_Nil [simp]: "bv_not [] = []"
   3.146 -  by (simp add: bv_not_def)
   3.147 -
   3.148 -lemma bv_not_Cons [simp]: "bv_not (b#bs) = (bitnot b) # bv_not bs"
   3.149 -  by (simp add: bv_not_def)
   3.150 -
   3.151 -lemma bv_not_bv_not [simp]: "bv_not (bv_not w) = w"
   3.152 -  by (rule bit_list_induct [of _ w]) simp_all
   3.153 -
   3.154 -lemma bv_msb_Nil [simp]: "bv_msb [] = \<zero>"
   3.155 -  by (simp add: bv_msb_def)
   3.156 -
   3.157 -lemma bv_msb_Cons [simp]: "bv_msb (b#bs) = b"
   3.158 -  by (simp add: bv_msb_def)
   3.159 -
   3.160 -lemma bv_msb_bv_not [simp]: "0 < length w ==> bv_msb (bv_not w) = (bitnot (bv_msb w))"
   3.161 -  by (cases w) simp_all
   3.162 -
   3.163 -lemma bv_msb_one_length [simp,intro]: "bv_msb w = \<one> ==> 0 < length w"
   3.164 -  by (cases w) simp_all
   3.165 -
   3.166 -lemma length_bv_not [simp]: "length (bv_not w) = length w"
   3.167 -  by (induct w) simp_all
   3.168 -
   3.169 -definition
   3.170 -  bv_to_nat :: "bit list => nat" where
   3.171 -  "bv_to_nat = foldl (%bn b. 2 * bn + bitval b) 0"
   3.172 -
   3.173 -lemma bv_to_nat_Nil [simp]: "bv_to_nat [] = 0"
   3.174 -  by (simp add: bv_to_nat_def)
   3.175 -
   3.176 -lemma bv_to_nat_helper [simp]: "bv_to_nat (b # bs) = bitval b * 2 ^ length bs + bv_to_nat bs"
   3.177 -proof -
   3.178 -  let ?bv_to_nat' = "foldl (\<lambda>bn b. 2 * bn + bitval b)"
   3.179 -  have helper: "\<And>base. ?bv_to_nat' base bs = base * 2 ^ length bs + ?bv_to_nat' 0 bs"
   3.180 -  proof (induct bs)
   3.181 -    case Nil
   3.182 -    show ?case by simp
   3.183 -  next
   3.184 -    case (Cons x xs base)
   3.185 -    show ?case
   3.186 -      apply (simp only: foldl.simps)
   3.187 -      apply (subst Cons [of "2 * base + bitval x"])
   3.188 -      apply simp
   3.189 -      apply (subst Cons [of "bitval x"])
   3.190 -      apply (simp add: add_mult_distrib)
   3.191 -      done
   3.192 -  qed
   3.193 -  show ?thesis by (simp add: bv_to_nat_def) (rule helper)
   3.194 -qed
   3.195 -
   3.196 -lemma bv_to_nat0 [simp]: "bv_to_nat (\<zero>#bs) = bv_to_nat bs"
   3.197 -  by simp
   3.198 -
   3.199 -lemma bv_to_nat1 [simp]: "bv_to_nat (\<one>#bs) = 2 ^ length bs + bv_to_nat bs"
   3.200 -  by simp
   3.201 -
   3.202 -lemma bv_to_nat_upper_range: "bv_to_nat w < 2 ^ length w"
   3.203 -proof (induct w, simp_all)
   3.204 -  fix b bs
   3.205 -  assume "bv_to_nat bs < 2 ^ length bs"
   3.206 -  show "bitval b * 2 ^ length bs + bv_to_nat bs < 2 * 2 ^ length bs"
   3.207 -  proof (cases b, simp_all)
   3.208 -    have "bv_to_nat bs < 2 ^ length bs" by fact
   3.209 -    also have "... < 2 * 2 ^ length bs" by auto
   3.210 -    finally show "bv_to_nat bs < 2 * 2 ^ length bs" by simp
   3.211 -  next
   3.212 -    have "bv_to_nat bs < 2 ^ length bs" by fact
   3.213 -    hence "2 ^ length bs + bv_to_nat bs < 2 ^ length bs + 2 ^ length bs" by arith
   3.214 -    also have "... = 2 * (2 ^ length bs)" by simp
   3.215 -    finally show "bv_to_nat bs < 2 ^ length bs" by simp
   3.216 -  qed
   3.217 -qed
   3.218 -
   3.219 -lemma bv_extend_longer [simp]:
   3.220 -  assumes wn: "n \<le> length w"
   3.221 -  shows       "bv_extend n b w = w"
   3.222 -  by (simp add: bv_extend_def wn)
   3.223 -
   3.224 -lemma bv_extend_shorter [simp]:
   3.225 -  assumes wn: "length w < n"
   3.226 -  shows       "bv_extend n b w = bv_extend n b (b#w)"
   3.227 -proof -
   3.228 -  from wn
   3.229 -  have s: "n - Suc (length w) + 1 = n - length w"
   3.230 -    by arith
   3.231 -  have "bv_extend n b w = replicate (n - length w) b @ w"
   3.232 -    by (simp add: bv_extend_def)
   3.233 -  also have "... = replicate (n - Suc (length w) + 1) b @ w"
   3.234 -    by (subst s) rule
   3.235 -  also have "... = (replicate (n - Suc (length w)) b @ replicate 1 b) @ w"
   3.236 -    by (subst replicate_add) rule
   3.237 -  also have "... = replicate (n - Suc (length w)) b @ b # w"
   3.238 -    by simp
   3.239 -  also have "... = bv_extend n b (b#w)"
   3.240 -    by (simp add: bv_extend_def)
   3.241 -  finally show "bv_extend n b w = bv_extend n b (b#w)" .
   3.242 -qed
   3.243 -
   3.244 -primrec rem_initial :: "bit => bit list => bit list" where
   3.245 -    "rem_initial b [] = []"
   3.246 -  | "rem_initial b (x#xs) = (if b = x then rem_initial b xs else x#xs)"
   3.247 -
   3.248 -lemma rem_initial_length: "length (rem_initial b w) \<le> length w"
   3.249 -  by (rule bit_list_induct [of _ w],simp_all (no_asm),safe,simp_all)
   3.250 -
   3.251 -lemma rem_initial_equal:
   3.252 -  assumes p: "length (rem_initial b w) = length w"
   3.253 -  shows      "rem_initial b w = w"
   3.254 -proof -
   3.255 -  have "length (rem_initial b w) = length w --> rem_initial b w = w"
   3.256 -  proof (induct w, simp_all, clarify)
   3.257 -    fix xs
   3.258 -    assume "length (rem_initial b xs) = length xs --> rem_initial b xs = xs"
   3.259 -    assume f: "length (rem_initial b xs) = Suc (length xs)"
   3.260 -    with rem_initial_length [of b xs]
   3.261 -    show "rem_initial b xs = b#xs"
   3.262 -      by auto
   3.263 -  qed
   3.264 -  from this and p show ?thesis ..
   3.265 -qed
   3.266 -
   3.267 -lemma bv_extend_rem_initial: "bv_extend (length w) b (rem_initial b w) = w"
   3.268 -proof (induct w, simp_all, safe)
   3.269 -  fix xs
   3.270 -  assume ind: "bv_extend (length xs) b (rem_initial b xs) = xs"
   3.271 -  from rem_initial_length [of b xs]
   3.272 -  have [simp]: "Suc (length xs) - length (rem_initial b xs) =
   3.273 -      1 + (length xs - length (rem_initial b xs))"
   3.274 -    by arith
   3.275 -  have "bv_extend (Suc (length xs)) b (rem_initial b xs) =
   3.276 -      replicate (Suc (length xs) - length (rem_initial b xs)) b @ (rem_initial b xs)"
   3.277 -    by (simp add: bv_extend_def)
   3.278 -  also have "... =
   3.279 -      replicate (1 + (length xs - length (rem_initial b xs))) b @ rem_initial b xs"
   3.280 -    by simp
   3.281 -  also have "... =
   3.282 -      (replicate 1 b @ replicate (length xs - length (rem_initial b xs)) b) @ rem_initial b xs"
   3.283 -    by (subst replicate_add) (rule refl)
   3.284 -  also have "... = b # bv_extend (length xs) b (rem_initial b xs)"
   3.285 -    by (auto simp add: bv_extend_def [symmetric])
   3.286 -  also have "... = b # xs"
   3.287 -    by (simp add: ind)
   3.288 -  finally show "bv_extend (Suc (length xs)) b (rem_initial b xs) = b # xs" .
   3.289 -qed
   3.290 -
   3.291 -lemma rem_initial_append1:
   3.292 -  assumes "rem_initial b xs ~= []"
   3.293 -  shows   "rem_initial b (xs @ ys) = rem_initial b xs @ ys"
   3.294 -  using assms by (induct xs) auto
   3.295 -
   3.296 -lemma rem_initial_append2:
   3.297 -  assumes "rem_initial b xs = []"
   3.298 -  shows   "rem_initial b (xs @ ys) = rem_initial b ys"
   3.299 -  using assms by (induct xs) auto
   3.300 -
   3.301 -definition
   3.302 -  norm_unsigned :: "bit list => bit list" where
   3.303 -  "norm_unsigned = rem_initial \<zero>"
   3.304 -
   3.305 -lemma norm_unsigned_Nil [simp]: "norm_unsigned [] = []"
   3.306 -  by (simp add: norm_unsigned_def)
   3.307 -
   3.308 -lemma norm_unsigned_Cons0 [simp]: "norm_unsigned (\<zero>#bs) = norm_unsigned bs"
   3.309 -  by (simp add: norm_unsigned_def)
   3.310 -
   3.311 -lemma norm_unsigned_Cons1 [simp]: "norm_unsigned (\<one>#bs) = \<one>#bs"
   3.312 -  by (simp add: norm_unsigned_def)
   3.313 -
   3.314 -lemma norm_unsigned_idem [simp]: "norm_unsigned (norm_unsigned w) = norm_unsigned w"
   3.315 -  by (rule bit_list_induct [of _ w],simp_all)
   3.316 -
   3.317 -fun
   3.318 -  nat_to_bv_helper :: "nat => bit list => bit list"
   3.319 -where
   3.320 -  "nat_to_bv_helper n bs = (if n = 0 then bs
   3.321 -                               else nat_to_bv_helper (n div 2) ((if n mod 2 = 0 then \<zero> else \<one>)#bs))"
   3.322 -
   3.323 -definition
   3.324 -  nat_to_bv :: "nat => bit list" where
   3.325 -  "nat_to_bv n = nat_to_bv_helper n []"
   3.326 -
   3.327 -lemma nat_to_bv0 [simp]: "nat_to_bv 0 = []"
   3.328 -  by (simp add: nat_to_bv_def)
   3.329 -
   3.330 -lemmas [simp del] = nat_to_bv_helper.simps
   3.331 -
   3.332 -lemma n_div_2_cases:
   3.333 -  assumes zero: "(n::nat) = 0 ==> R"
   3.334 -  and     div : "[| n div 2 < n ; 0 < n |] ==> R"
   3.335 -  shows         "R"
   3.336 -proof (cases "n = 0")
   3.337 -  assume "n = 0"
   3.338 -  thus R by (rule zero)
   3.339 -next
   3.340 -  assume "n ~= 0"
   3.341 -  hence "0 < n" by simp
   3.342 -  hence "n div 2 < n" by arith
   3.343 -  from this and `0 < n` show R by (rule div)
   3.344 -qed
   3.345 -
   3.346 -lemma int_wf_ge_induct:
   3.347 -  assumes ind :  "!!i::int. (!!j. [| k \<le> j ; j < i |] ==> P j) ==> P i"
   3.348 -  shows          "P i"
   3.349 -proof (rule wf_induct_rule [OF wf_int_ge_less_than])
   3.350 -  fix x
   3.351 -  assume ih: "(\<And>y\<Colon>int. (y, x) \<in> int_ge_less_than k \<Longrightarrow> P y)"
   3.352 -  thus "P x"
   3.353 -    by (rule ind) (simp add: int_ge_less_than_def)
   3.354 -qed
   3.355 -
   3.356 -lemma unfold_nat_to_bv_helper:
   3.357 -  "nat_to_bv_helper b l = nat_to_bv_helper b [] @ l"
   3.358 -proof -
   3.359 -  have "\<forall>l. nat_to_bv_helper b l = nat_to_bv_helper b [] @ l"
   3.360 -  proof (induct b rule: less_induct)
   3.361 -    fix n
   3.362 -    assume ind: "!!j. j < n \<Longrightarrow> \<forall> l. nat_to_bv_helper j l = nat_to_bv_helper j [] @ l"
   3.363 -    show "\<forall>l. nat_to_bv_helper n l = nat_to_bv_helper n [] @ l"
   3.364 -    proof
   3.365 -      fix l
   3.366 -      show "nat_to_bv_helper n l = nat_to_bv_helper n [] @ l"
   3.367 -      proof (cases "n < 0")
   3.368 -        assume "n < 0"
   3.369 -        thus ?thesis
   3.370 -          by (simp add: nat_to_bv_helper.simps)
   3.371 -      next
   3.372 -        assume "~n < 0"
   3.373 -        show ?thesis
   3.374 -        proof (rule n_div_2_cases [of n])
   3.375 -          assume [simp]: "n = 0"
   3.376 -          show ?thesis
   3.377 -            apply (simp only: nat_to_bv_helper.simps [of n])
   3.378 -            apply simp
   3.379 -            done
   3.380 -        next
   3.381 -          assume n2n: "n div 2 < n"
   3.382 -          assume [simp]: "0 < n"
   3.383 -          hence n20: "0 \<le> n div 2"
   3.384 -            by arith
   3.385 -          from ind [of "n div 2"] and n2n n20
   3.386 -          have ind': "\<forall>l. nat_to_bv_helper (n div 2) l = nat_to_bv_helper (n div 2) [] @ l"
   3.387 -            by blast
   3.388 -          show ?thesis
   3.389 -            apply (simp only: nat_to_bv_helper.simps [of n])
   3.390 -            apply (cases "n=0")
   3.391 -            apply simp
   3.392 -            apply (simp only: if_False)
   3.393 -            apply simp
   3.394 -            apply (subst spec [OF ind',of "\<zero>#l"])
   3.395 -            apply (subst spec [OF ind',of "\<one>#l"])
   3.396 -            apply (subst spec [OF ind',of "[\<one>]"])
   3.397 -            apply (subst spec [OF ind',of "[\<zero>]"])
   3.398 -            apply simp
   3.399 -            done
   3.400 -        qed
   3.401 -      qed
   3.402 -    qed
   3.403 -  qed
   3.404 -  thus ?thesis ..
   3.405 -qed
   3.406 -
   3.407 -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>]"
   3.408 -proof -
   3.409 -  assume [simp]: "n\<noteq>0"
   3.410 -  show ?thesis
   3.411 -    apply (subst nat_to_bv_def [of n])
   3.412 -    apply (simp only: nat_to_bv_helper.simps [of n])
   3.413 -    apply (subst unfold_nat_to_bv_helper)
   3.414 -    using prems
   3.415 -    apply (simp)
   3.416 -    apply (subst nat_to_bv_def [of "n div 2"])
   3.417 -    apply auto
   3.418 -    done
   3.419 -qed
   3.420 -
   3.421 -lemma bv_to_nat_dist_append:
   3.422 -  "bv_to_nat (l1 @ l2) = bv_to_nat l1 * 2 ^ length l2 + bv_to_nat l2"
   3.423 -proof -
   3.424 -  have "\<forall>l2. bv_to_nat (l1 @ l2) = bv_to_nat l1 * 2 ^ length l2 + bv_to_nat l2"
   3.425 -  proof (induct l1, simp_all)
   3.426 -    fix x xs
   3.427 -    assume ind: "\<forall>l2. bv_to_nat (xs @ l2) = bv_to_nat xs * 2 ^ length l2 + bv_to_nat l2"
   3.428 -    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"
   3.429 -    proof
   3.430 -      fix l2
   3.431 -      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"
   3.432 -      proof -
   3.433 -        have "(2::nat) ^ (length xs + length l2) = 2 ^ length xs * 2 ^ length l2"
   3.434 -          by (induct ("length xs")) simp_all
   3.435 -        hence "bitval x * 2 ^ (length xs + length l2) + bv_to_nat xs * 2 ^ length l2 =
   3.436 -          bitval x * 2 ^ length xs * 2 ^ length l2 + bv_to_nat xs * 2 ^ length l2"
   3.437 -          by simp
   3.438 -        also have "... = (bitval x * 2 ^ length xs + bv_to_nat xs) * 2 ^ length l2"
   3.439 -          by (simp add: ring_distribs)
   3.440 -        finally show ?thesis by simp
   3.441 -      qed
   3.442 -    qed
   3.443 -  qed
   3.444 -  thus ?thesis ..
   3.445 -qed
   3.446 -
   3.447 -lemma bv_nat_bv [simp]: "bv_to_nat (nat_to_bv n) = n"
   3.448 -proof (induct n rule: less_induct)
   3.449 -  fix n
   3.450 -  assume ind: "!!j. j < n \<Longrightarrow> bv_to_nat (nat_to_bv j) = j"
   3.451 -  show "bv_to_nat (nat_to_bv n) = n"
   3.452 -  proof (rule n_div_2_cases [of n])
   3.453 -    assume "n = 0" then show ?thesis by simp
   3.454 -  next
   3.455 -    assume nn: "n div 2 < n"
   3.456 -    assume n0: "0 < n"
   3.457 -    from ind and nn
   3.458 -    have ind': "bv_to_nat (nat_to_bv (n div 2)) = n div 2" by blast
   3.459 -    from n0 have n0': "n \<noteq> 0" by simp
   3.460 -    show ?thesis
   3.461 -      apply (subst nat_to_bv_def)
   3.462 -      apply (simp only: nat_to_bv_helper.simps [of n])
   3.463 -      apply (simp only: n0' if_False)
   3.464 -      apply (subst unfold_nat_to_bv_helper)
   3.465 -      apply (subst bv_to_nat_dist_append)
   3.466 -      apply (fold nat_to_bv_def)
   3.467 -      apply (simp add: ind' split del: split_if)
   3.468 -      apply (cases "n mod 2 = 0")
   3.469 -      proof (simp_all)
   3.470 -        assume "n mod 2 = 0"
   3.471 -        with mod_div_equality [of n 2]
   3.472 -        show "n div 2 * 2 = n" by simp
   3.473 -      next
   3.474 -        assume "n mod 2 = Suc 0"
   3.475 -        with mod_div_equality [of n 2]
   3.476 -        show "Suc (n div 2 * 2) = n" by arith
   3.477 -      qed
   3.478 -  qed
   3.479 -qed
   3.480 -
   3.481 -lemma bv_to_nat_type [simp]: "bv_to_nat (norm_unsigned w) = bv_to_nat w"
   3.482 -  by (rule bit_list_induct) simp_all
   3.483 -
   3.484 -lemma length_norm_unsigned_le [simp]: "length (norm_unsigned w) \<le> length w"
   3.485 -  by (rule bit_list_induct) simp_all
   3.486 -
   3.487 -lemma bv_to_nat_rew_msb: "bv_msb w = \<one> ==> bv_to_nat w = 2 ^ (length w - 1) + bv_to_nat (tl w)"
   3.488 -  by (rule bit_list_cases [of w]) simp_all
   3.489 -
   3.490 -lemma norm_unsigned_result: "norm_unsigned xs = [] \<or> bv_msb (norm_unsigned xs) = \<one>"
   3.491 -proof (rule length_induct [of _ xs])
   3.492 -  fix xs :: "bit list"
   3.493 -  assume ind: "\<forall>ys. length ys < length xs --> norm_unsigned ys = [] \<or> bv_msb (norm_unsigned ys) = \<one>"
   3.494 -  show "norm_unsigned xs = [] \<or> bv_msb (norm_unsigned xs) = \<one>"
   3.495 -  proof (rule bit_list_cases [of xs],simp_all)
   3.496 -    fix bs
   3.497 -    assume [simp]: "xs = \<zero>#bs"
   3.498 -    from ind
   3.499 -    have "length bs < length xs --> norm_unsigned bs = [] \<or> bv_msb (norm_unsigned bs) = \<one>" ..
   3.500 -    thus "norm_unsigned bs = [] \<or> bv_msb (norm_unsigned bs) = \<one>" by simp
   3.501 -  qed
   3.502 -qed
   3.503 -
   3.504 -lemma norm_empty_bv_to_nat_zero:
   3.505 -  assumes nw: "norm_unsigned w = []"
   3.506 -  shows       "bv_to_nat w = 0"
   3.507 -proof -
   3.508 -  have "bv_to_nat w = bv_to_nat (norm_unsigned w)" by simp
   3.509 -  also have "... = bv_to_nat []" by (subst nw) (rule refl)
   3.510 -  also have "... = 0" by simp
   3.511 -  finally show ?thesis .
   3.512 -qed
   3.513 -
   3.514 -lemma bv_to_nat_lower_limit:
   3.515 -  assumes w0: "0 < bv_to_nat w"
   3.516 -  shows "2 ^ (length (norm_unsigned w) - 1) \<le> bv_to_nat w"
   3.517 -proof -
   3.518 -  from w0 and norm_unsigned_result [of w]
   3.519 -  have msbw: "bv_msb (norm_unsigned w) = \<one>"
   3.520 -    by (auto simp add: norm_empty_bv_to_nat_zero)
   3.521 -  have "2 ^ (length (norm_unsigned w) - 1) \<le> bv_to_nat (norm_unsigned w)"
   3.522 -    by (subst bv_to_nat_rew_msb [OF msbw],simp)
   3.523 -  thus ?thesis by simp
   3.524 -qed
   3.525 -
   3.526 -lemmas [simp del] = nat_to_bv_non0
   3.527 -
   3.528 -lemma norm_unsigned_length [intro!]: "length (norm_unsigned w) \<le> length w"
   3.529 -by (subst norm_unsigned_def,rule rem_initial_length)
   3.530 -
   3.531 -lemma norm_unsigned_equal:
   3.532 -  "length (norm_unsigned w) = length w ==> norm_unsigned w = w"
   3.533 -by (simp add: norm_unsigned_def,rule rem_initial_equal)
   3.534 -
   3.535 -lemma bv_extend_norm_unsigned: "bv_extend (length w) \<zero> (norm_unsigned w) = w"
   3.536 -by (simp add: norm_unsigned_def,rule bv_extend_rem_initial)
   3.537 -
   3.538 -lemma norm_unsigned_append1 [simp]:
   3.539 -  "norm_unsigned xs \<noteq> [] ==> norm_unsigned (xs @ ys) = norm_unsigned xs @ ys"
   3.540 -by (simp add: norm_unsigned_def,rule rem_initial_append1)
   3.541 -
   3.542 -lemma norm_unsigned_append2 [simp]:
   3.543 -  "norm_unsigned xs = [] ==> norm_unsigned (xs @ ys) = norm_unsigned ys"
   3.544 -by (simp add: norm_unsigned_def,rule rem_initial_append2)
   3.545 -
   3.546 -lemma bv_to_nat_zero_imp_empty:
   3.547 -  "bv_to_nat w = 0 \<Longrightarrow> norm_unsigned w = []"
   3.548 -by (atomize (full), induct w rule: bit_list_induct) simp_all
   3.549 -
   3.550 -lemma bv_to_nat_nzero_imp_nempty:
   3.551 -  "bv_to_nat w \<noteq> 0 \<Longrightarrow> norm_unsigned w \<noteq> []"
   3.552 -by (induct w rule: bit_list_induct) simp_all
   3.553 -
   3.554 -lemma nat_helper1:
   3.555 -  assumes ass: "nat_to_bv (bv_to_nat w) = norm_unsigned w"
   3.556 -  shows        "nat_to_bv (2 * bv_to_nat w + bitval x) = norm_unsigned (w @ [x])"
   3.557 -proof (cases x)
   3.558 -  assume [simp]: "x = \<one>"
   3.559 -  have "nat_to_bv (Suc (2 * bv_to_nat w) div 2) @ [\<one>] =
   3.560 -      nat_to_bv ((1 + 2 * bv_to_nat w) div 2) @ [\<one>]"
   3.561 -    by (simp add: add_commute)
   3.562 -  also have "... = nat_to_bv (bv_to_nat w) @ [\<one>]"
   3.563 -    by (subst div_add1_eq) simp
   3.564 -  also have "... = norm_unsigned w @ [\<one>]"
   3.565 -    by (subst ass) (rule refl)
   3.566 -  also have "... = norm_unsigned (w @ [\<one>])"
   3.567 -    by (cases "norm_unsigned w") simp_all
   3.568 -  finally have "nat_to_bv (Suc (2 * bv_to_nat w) div 2) @ [\<one>] = norm_unsigned (w @ [\<one>])" .
   3.569 -  then show ?thesis by (simp add: nat_to_bv_non0)
   3.570 -next
   3.571 -  assume [simp]: "x = \<zero>"
   3.572 -  show ?thesis
   3.573 -  proof (cases "bv_to_nat w = 0")
   3.574 -    assume "bv_to_nat w = 0"
   3.575 -    thus ?thesis
   3.576 -      by (simp add: bv_to_nat_zero_imp_empty)
   3.577 -  next
   3.578 -    assume "bv_to_nat w \<noteq> 0"
   3.579 -    thus ?thesis
   3.580 -      apply simp
   3.581 -      apply (subst nat_to_bv_non0)
   3.582 -      apply simp
   3.583 -      apply auto
   3.584 -      apply (subst ass)
   3.585 -      apply (cases "norm_unsigned w")
   3.586 -      apply (simp_all add: norm_empty_bv_to_nat_zero)
   3.587 -      done
   3.588 -  qed
   3.589 -qed
   3.590 -
   3.591 -lemma nat_helper2: "nat_to_bv (2 ^ length xs + bv_to_nat xs) = \<one> # xs"
   3.592 -proof -
   3.593 -  have "\<forall>xs. nat_to_bv (2 ^ length (rev xs) + bv_to_nat (rev xs)) = \<one> # (rev xs)" (is "\<forall>xs. ?P xs")
   3.594 -  proof
   3.595 -    fix xs
   3.596 -    show "?P xs"
   3.597 -    proof (rule length_induct [of _ xs])
   3.598 -      fix xs :: "bit list"
   3.599 -      assume ind: "\<forall>ys. length ys < length xs --> ?P ys"
   3.600 -      show "?P xs"
   3.601 -      proof (cases xs)
   3.602 -        assume "xs = []"
   3.603 -        then show ?thesis by (simp add: nat_to_bv_non0)
   3.604 -      next
   3.605 -        fix y ys
   3.606 -        assume [simp]: "xs = y # ys"
   3.607 -        show ?thesis
   3.608 -          apply simp
   3.609 -          apply (subst bv_to_nat_dist_append)
   3.610 -          apply simp
   3.611 -        proof -
   3.612 -          have "nat_to_bv (2 * 2 ^ length ys + (bv_to_nat (rev ys) * 2 + bitval y)) =
   3.613 -            nat_to_bv (2 * (2 ^ length ys + bv_to_nat (rev ys)) + bitval y)"
   3.614 -            by (simp add: add_ac mult_ac)
   3.615 -          also have "... = nat_to_bv (2 * (bv_to_nat (\<one>#rev ys)) + bitval y)"
   3.616 -            by simp
   3.617 -          also have "... = norm_unsigned (\<one>#rev ys) @ [y]"
   3.618 -          proof -
   3.619 -            from ind
   3.620 -            have "nat_to_bv (2 ^ length (rev ys) + bv_to_nat (rev ys)) = \<one> # rev ys"
   3.621 -              by auto
   3.622 -            hence [simp]: "nat_to_bv (2 ^ length ys + bv_to_nat (rev ys)) = \<one> # rev ys"
   3.623 -              by simp
   3.624 -            show ?thesis
   3.625 -              apply (subst nat_helper1)
   3.626 -              apply simp_all
   3.627 -              done
   3.628 -          qed
   3.629 -          also have "... = (\<one>#rev ys) @ [y]"
   3.630 -            by simp
   3.631 -          also have "... = \<one> # rev ys @ [y]"
   3.632 -            by simp
   3.633 -          finally show "nat_to_bv (2 * 2 ^ length ys + (bv_to_nat (rev ys) * 2 + bitval y)) =
   3.634 -              \<one> # rev ys @ [y]" .
   3.635 -        qed
   3.636 -      qed
   3.637 -    qed
   3.638 -  qed
   3.639 -  hence "nat_to_bv (2 ^ length (rev (rev xs)) + bv_to_nat (rev (rev xs))) =
   3.640 -      \<one> # rev (rev xs)" ..
   3.641 -  thus ?thesis by simp
   3.642 -qed
   3.643 -
   3.644 -lemma nat_bv_nat [simp]: "nat_to_bv (bv_to_nat w) = norm_unsigned w"
   3.645 -proof (rule bit_list_induct [of _ w],simp_all)
   3.646 -  fix xs
   3.647 -  assume "nat_to_bv (bv_to_nat xs) = norm_unsigned xs"
   3.648 -  have "bv_to_nat xs = bv_to_nat (norm_unsigned xs)" by simp
   3.649 -  have "bv_to_nat xs < 2 ^ length xs"
   3.650 -    by (rule bv_to_nat_upper_range)
   3.651 -  show "nat_to_bv (2 ^ length xs + bv_to_nat xs) = \<one> # xs"
   3.652 -    by (rule nat_helper2)
   3.653 -qed
   3.654 -
   3.655 -lemma bv_to_nat_qinj:
   3.656 -  assumes one: "bv_to_nat xs = bv_to_nat ys"
   3.657 -  and     len: "length xs = length ys"
   3.658 -  shows        "xs = ys"
   3.659 -proof -
   3.660 -  from one
   3.661 -  have "nat_to_bv (bv_to_nat xs) = nat_to_bv (bv_to_nat ys)"
   3.662 -    by simp
   3.663 -  hence xsys: "norm_unsigned xs = norm_unsigned ys"
   3.664 -    by simp
   3.665 -  have "xs = bv_extend (length xs) \<zero> (norm_unsigned xs)"
   3.666 -    by (simp add: bv_extend_norm_unsigned)
   3.667 -  also have "... = bv_extend (length ys) \<zero> (norm_unsigned ys)"
   3.668 -    by (simp add: xsys len)
   3.669 -  also have "... = ys"
   3.670 -    by (simp add: bv_extend_norm_unsigned)
   3.671 -  finally show ?thesis .
   3.672 -qed
   3.673 -
   3.674 -lemma norm_unsigned_nat_to_bv [simp]:
   3.675 -  "norm_unsigned (nat_to_bv n) = nat_to_bv n"
   3.676 -proof -
   3.677 -  have "norm_unsigned (nat_to_bv n) = nat_to_bv (bv_to_nat (norm_unsigned (nat_to_bv n)))"
   3.678 -    by (subst nat_bv_nat) simp
   3.679 -  also have "... = nat_to_bv n" by simp
   3.680 -  finally show ?thesis .
   3.681 -qed
   3.682 -
   3.683 -lemma length_nat_to_bv_upper_limit:
   3.684 -  assumes nk: "n \<le> 2 ^ k - 1"
   3.685 -  shows       "length (nat_to_bv n) \<le> k"
   3.686 -proof (cases "n = 0")
   3.687 -  case True
   3.688 -  thus ?thesis
   3.689 -    by (simp add: nat_to_bv_def nat_to_bv_helper.simps)
   3.690 -next
   3.691 -  case False
   3.692 -  hence n0: "0 < n" by simp
   3.693 -  show ?thesis
   3.694 -  proof (rule ccontr)
   3.695 -    assume "~ length (nat_to_bv n) \<le> k"
   3.696 -    hence "k < length (nat_to_bv n)" by simp
   3.697 -    hence "k \<le> length (nat_to_bv n) - 1" by arith
   3.698 -    hence "(2::nat) ^ k \<le> 2 ^ (length (nat_to_bv n) - 1)" by simp
   3.699 -    also have "... = 2 ^ (length (norm_unsigned (nat_to_bv n)) - 1)" by simp
   3.700 -    also have "... \<le> bv_to_nat (nat_to_bv n)"
   3.701 -      by (rule bv_to_nat_lower_limit) (simp add: n0)
   3.702 -    also have "... = n" by simp
   3.703 -    finally have "2 ^ k \<le> n" .
   3.704 -    with n0 have "2 ^ k - 1 < n" by arith
   3.705 -    with nk show False by simp
   3.706 -  qed
   3.707 -qed
   3.708 -
   3.709 -lemma length_nat_to_bv_lower_limit:
   3.710 -  assumes nk: "2 ^ k \<le> n"
   3.711 -  shows       "k < length (nat_to_bv n)"
   3.712 -proof (rule ccontr)
   3.713 -  assume "~ k < length (nat_to_bv n)"
   3.714 -  hence lnk: "length (nat_to_bv n) \<le> k" by simp
   3.715 -  have "n = bv_to_nat (nat_to_bv n)" by simp
   3.716 -  also have "... < 2 ^ length (nat_to_bv n)"
   3.717 -    by (rule bv_to_nat_upper_range)
   3.718 -  also from lnk have "... \<le> 2 ^ k" by simp
   3.719 -  finally have "n < 2 ^ k" .
   3.720 -  with nk show False by simp
   3.721 -qed
   3.722 -
   3.723 -
   3.724 -subsection {* Unsigned Arithmetic Operations *}
   3.725 -
   3.726 -definition
   3.727 -  bv_add :: "[bit list, bit list ] => bit list" where
   3.728 -  "bv_add w1 w2 = nat_to_bv (bv_to_nat w1 + bv_to_nat w2)"
   3.729 -
   3.730 -lemma bv_add_type1 [simp]: "bv_add (norm_unsigned w1) w2 = bv_add w1 w2"
   3.731 -  by (simp add: bv_add_def)
   3.732 -
   3.733 -lemma bv_add_type2 [simp]: "bv_add w1 (norm_unsigned w2) = bv_add w1 w2"
   3.734 -  by (simp add: bv_add_def)
   3.735 -
   3.736 -lemma bv_add_returntype [simp]: "norm_unsigned (bv_add w1 w2) = bv_add w1 w2"
   3.737 -  by (simp add: bv_add_def)
   3.738 -
   3.739 -lemma bv_add_length: "length (bv_add w1 w2) \<le> Suc (max (length w1) (length w2))"
   3.740 -proof (unfold bv_add_def,rule length_nat_to_bv_upper_limit)
   3.741 -  from bv_to_nat_upper_range [of w1] and bv_to_nat_upper_range [of w2]
   3.742 -  have "bv_to_nat w1 + bv_to_nat w2 \<le> (2 ^ length w1 - 1) + (2 ^ length w2 - 1)"
   3.743 -    by arith
   3.744 -  also have "... \<le>
   3.745 -      max (2 ^ length w1 - 1) (2 ^ length w2 - 1) + max (2 ^ length w1 - 1) (2 ^ length w2 - 1)"
   3.746 -    by (rule add_mono,safe intro!: le_maxI1 le_maxI2)
   3.747 -  also have "... = 2 * max (2 ^ length w1 - 1) (2 ^ length w2 - 1)" by simp
   3.748 -  also have "... \<le> 2 ^ Suc (max (length w1) (length w2)) - 2"
   3.749 -  proof (cases "length w1 \<le> length w2")
   3.750 -    assume w1w2: "length w1 \<le> length w2"
   3.751 -    hence "(2::nat) ^ length w1 \<le> 2 ^ length w2" by simp
   3.752 -    hence "(2::nat) ^ length w1 - 1 \<le> 2 ^ length w2 - 1" by arith
   3.753 -    with w1w2 show ?thesis
   3.754 -      by (simp add: diff_mult_distrib2 split: split_max)
   3.755 -  next
   3.756 -    assume [simp]: "~ (length w1 \<le> length w2)"
   3.757 -    have "~ ((2::nat) ^ length w1 - 1 \<le> 2 ^ length w2 - 1)"
   3.758 -    proof
   3.759 -      assume "(2::nat) ^ length w1 - 1 \<le> 2 ^ length w2 - 1"
   3.760 -      hence "((2::nat) ^ length w1 - 1) + 1 \<le> (2 ^ length w2 - 1) + 1"
   3.761 -        by (rule add_right_mono)
   3.762 -      hence "(2::nat) ^ length w1 \<le> 2 ^ length w2" by simp
   3.763 -      hence "length w1 \<le> length w2" by simp
   3.764 -      thus False by simp
   3.765 -    qed
   3.766 -    thus ?thesis
   3.767 -      by (simp add: diff_mult_distrib2 split: split_max)
   3.768 -  qed
   3.769 -  finally show "bv_to_nat w1 + bv_to_nat w2 \<le> 2 ^ Suc (max (length w1) (length w2)) - 1"
   3.770 -    by arith
   3.771 -qed
   3.772 -
   3.773 -definition
   3.774 -  bv_mult :: "[bit list, bit list ] => bit list" where
   3.775 -  "bv_mult w1 w2 = nat_to_bv (bv_to_nat w1 * bv_to_nat w2)"
   3.776 -
   3.777 -lemma bv_mult_type1 [simp]: "bv_mult (norm_unsigned w1) w2 = bv_mult w1 w2"
   3.778 -  by (simp add: bv_mult_def)
   3.779 -
   3.780 -lemma bv_mult_type2 [simp]: "bv_mult w1 (norm_unsigned w2) = bv_mult w1 w2"
   3.781 -  by (simp add: bv_mult_def)
   3.782 -
   3.783 -lemma bv_mult_returntype [simp]: "norm_unsigned (bv_mult w1 w2) = bv_mult w1 w2"
   3.784 -  by (simp add: bv_mult_def)
   3.785 -
   3.786 -lemma bv_mult_length: "length (bv_mult w1 w2) \<le> length w1 + length w2"
   3.787 -proof (unfold bv_mult_def,rule length_nat_to_bv_upper_limit)
   3.788 -  from bv_to_nat_upper_range [of w1] and bv_to_nat_upper_range [of w2]
   3.789 -  have h: "bv_to_nat w1 \<le> 2 ^ length w1 - 1 \<and> bv_to_nat w2 \<le> 2 ^ length w2 - 1"
   3.790 -    by arith
   3.791 -  have "bv_to_nat w1 * bv_to_nat w2 \<le> (2 ^ length w1 - 1) * (2 ^ length w2 - 1)"
   3.792 -    apply (cut_tac h)
   3.793 -    apply (rule mult_mono)
   3.794 -    apply auto
   3.795 -    done
   3.796 -  also have "... < 2 ^ length w1 * 2 ^ length w2"
   3.797 -    by (rule mult_strict_mono,auto)
   3.798 -  also have "... = 2 ^ (length w1 + length w2)"
   3.799 -    by (simp add: power_add)
   3.800 -  finally show "bv_to_nat w1 * bv_to_nat w2 \<le> 2 ^ (length w1 + length w2) - 1"
   3.801 -    by arith
   3.802 -qed
   3.803 -
   3.804 -subsection {* Signed Vectors *}
   3.805 -
   3.806 -primrec norm_signed :: "bit list => bit list" where
   3.807 -    norm_signed_Nil: "norm_signed [] = []"
   3.808 -  | norm_signed_Cons: "norm_signed (b#bs) =
   3.809 -      (case b of
   3.810 -        \<zero> => if norm_unsigned bs = [] then [] else b#norm_unsigned bs
   3.811 -      | \<one> => b#rem_initial b bs)"
   3.812 -
   3.813 -lemma norm_signed0 [simp]: "norm_signed [\<zero>] = []"
   3.814 -  by simp
   3.815 -
   3.816 -lemma norm_signed1 [simp]: "norm_signed [\<one>] = [\<one>]"
   3.817 -  by simp
   3.818 -
   3.819 -lemma norm_signed01 [simp]: "norm_signed (\<zero>#\<one>#xs) = \<zero>#\<one>#xs"
   3.820 -  by simp
   3.821 -
   3.822 -lemma norm_signed00 [simp]: "norm_signed (\<zero>#\<zero>#xs) = norm_signed (\<zero>#xs)"
   3.823 -  by simp
   3.824 -
   3.825 -lemma norm_signed10 [simp]: "norm_signed (\<one>#\<zero>#xs) = \<one>#\<zero>#xs"
   3.826 -  by simp
   3.827 -
   3.828 -lemma norm_signed11 [simp]: "norm_signed (\<one>#\<one>#xs) = norm_signed (\<one>#xs)"
   3.829 -  by simp
   3.830 -
   3.831 -lemmas [simp del] = norm_signed_Cons
   3.832 -
   3.833 -definition
   3.834 -  int_to_bv :: "int => bit list" where
   3.835 -  "int_to_bv n = (if 0 \<le> n
   3.836 -                 then norm_signed (\<zero>#nat_to_bv (nat n))
   3.837 -                 else norm_signed (bv_not (\<zero>#nat_to_bv (nat (-n- 1)))))"
   3.838 -
   3.839 -lemma int_to_bv_ge0 [simp]: "0 \<le> n ==> int_to_bv n = norm_signed (\<zero> # nat_to_bv (nat n))"
   3.840 -  by (simp add: int_to_bv_def)
   3.841 -
   3.842 -lemma int_to_bv_lt0 [simp]:
   3.843 -    "n < 0 ==> int_to_bv n = norm_signed (bv_not (\<zero>#nat_to_bv (nat (-n- 1))))"
   3.844 -  by (simp add: int_to_bv_def)
   3.845 -
   3.846 -lemma norm_signed_idem [simp]: "norm_signed (norm_signed w) = norm_signed w"
   3.847 -proof (rule bit_list_induct [of _ w], simp_all)
   3.848 -  fix xs
   3.849 -  assume eq: "norm_signed (norm_signed xs) = norm_signed xs"
   3.850 -  show "norm_signed (norm_signed (\<zero>#xs)) = norm_signed (\<zero>#xs)"
   3.851 -  proof (rule bit_list_cases [of xs],simp_all)
   3.852 -    fix ys
   3.853 -    assume "xs = \<zero>#ys"
   3.854 -    from this [symmetric] and eq
   3.855 -    show "norm_signed (norm_signed (\<zero>#ys)) = norm_signed (\<zero>#ys)"
   3.856 -      by simp
   3.857 -  qed
   3.858 -next
   3.859 -  fix xs
   3.860 -  assume eq: "norm_signed (norm_signed xs) = norm_signed xs"
   3.861 -  show "norm_signed (norm_signed (\<one>#xs)) = norm_signed (\<one>#xs)"
   3.862 -  proof (rule bit_list_cases [of xs],simp_all)
   3.863 -    fix ys
   3.864 -    assume "xs = \<one>#ys"
   3.865 -    from this [symmetric] and eq
   3.866 -    show "norm_signed (norm_signed (\<one>#ys)) = norm_signed (\<one>#ys)"
   3.867 -      by simp
   3.868 -  qed
   3.869 -qed
   3.870 -
   3.871 -definition
   3.872 -  bv_to_int :: "bit list => int" where
   3.873 -  "bv_to_int w =
   3.874 -    (case bv_msb w of \<zero> => int (bv_to_nat w)
   3.875 -    | \<one> => - int (bv_to_nat (bv_not w) + 1))"
   3.876 -
   3.877 -lemma bv_to_int_Nil [simp]: "bv_to_int [] = 0"
   3.878 -  by (simp add: bv_to_int_def)
   3.879 -
   3.880 -lemma bv_to_int_Cons0 [simp]: "bv_to_int (\<zero>#bs) = int (bv_to_nat bs)"
   3.881 -  by (simp add: bv_to_int_def)
   3.882 -
   3.883 -lemma bv_to_int_Cons1 [simp]: "bv_to_int (\<one>#bs) = - int (bv_to_nat (bv_not bs) + 1)"
   3.884 -  by (simp add: bv_to_int_def)
   3.885 -
   3.886 -lemma bv_to_int_type [simp]: "bv_to_int (norm_signed w) = bv_to_int w"
   3.887 -proof (rule bit_list_induct [of _ w], simp_all)
   3.888 -  fix xs
   3.889 -  assume ind: "bv_to_int (norm_signed xs) = bv_to_int xs"
   3.890 -  show "bv_to_int (norm_signed (\<zero>#xs)) = int (bv_to_nat xs)"
   3.891 -  proof (rule bit_list_cases [of xs], simp_all)
   3.892 -    fix ys
   3.893 -    assume [simp]: "xs = \<zero>#ys"
   3.894 -    from ind
   3.895 -    show "bv_to_int (norm_signed (\<zero>#ys)) = int (bv_to_nat ys)"
   3.896 -      by simp
   3.897 -  qed
   3.898 -next
   3.899 -  fix xs
   3.900 -  assume ind: "bv_to_int (norm_signed xs) = bv_to_int xs"
   3.901 -  show "bv_to_int (norm_signed (\<one>#xs)) = -1 - int (bv_to_nat (bv_not xs))"
   3.902 -  proof (rule bit_list_cases [of xs], simp_all)
   3.903 -    fix ys
   3.904 -    assume [simp]: "xs = \<one>#ys"
   3.905 -    from ind
   3.906 -    show "bv_to_int (norm_signed (\<one>#ys)) = -1 - int (bv_to_nat (bv_not ys))"
   3.907 -      by simp
   3.908 -  qed
   3.909 -qed
   3.910 -
   3.911 -lemma bv_to_int_upper_range: "bv_to_int w < 2 ^ (length w - 1)"
   3.912 -proof (rule bit_list_cases [of w],simp_all)
   3.913 -  fix bs
   3.914 -  from bv_to_nat_upper_range
   3.915 -  show "int (bv_to_nat bs) < 2 ^ length bs"
   3.916 -    by (simp add: int_nat_two_exp)
   3.917 -next
   3.918 -  fix bs
   3.919 -  have "-1 - int (bv_to_nat (bv_not bs)) \<le> 0" by simp
   3.920 -  also have "... < 2 ^ length bs" by (induct bs) simp_all
   3.921 -  finally show "-1 - int (bv_to_nat (bv_not bs)) < 2 ^ length bs" .
   3.922 -qed
   3.923 -
   3.924 -lemma bv_to_int_lower_range: "- (2 ^ (length w - 1)) \<le> bv_to_int w"
   3.925 -proof (rule bit_list_cases [of w],simp_all)
   3.926 -  fix bs :: "bit list"
   3.927 -  have "- (2 ^ length bs) \<le> (0::int)" by (induct bs) simp_all
   3.928 -  also have "... \<le> int (bv_to_nat bs)" by simp
   3.929 -  finally show "- (2 ^ length bs) \<le> int (bv_to_nat bs)" .
   3.930 -next
   3.931 -  fix bs
   3.932 -  from bv_to_nat_upper_range [of "bv_not bs"]
   3.933 -  show "- (2 ^ length bs) \<le> -1 - int (bv_to_nat (bv_not bs))"
   3.934 -    by (simp add: int_nat_two_exp)
   3.935 -qed
   3.936 -
   3.937 -lemma int_bv_int [simp]: "int_to_bv (bv_to_int w) = norm_signed w"
   3.938 -proof (rule bit_list_cases [of w],simp)
   3.939 -  fix xs
   3.940 -  assume [simp]: "w = \<zero>#xs"
   3.941 -  show ?thesis
   3.942 -    apply simp
   3.943 -    apply (subst norm_signed_Cons [of "\<zero>" "xs"])
   3.944 -    apply simp
   3.945 -    using norm_unsigned_result [of xs]
   3.946 -    apply safe
   3.947 -    apply (rule bit_list_cases [of "norm_unsigned xs"])
   3.948 -    apply simp_all
   3.949 -    done
   3.950 -next
   3.951 -  fix xs
   3.952 -  assume [simp]: "w = \<one>#xs"
   3.953 -  show ?thesis
   3.954 -    apply (simp del: int_to_bv_lt0)
   3.955 -    apply (rule bit_list_induct [of _ xs])
   3.956 -    apply simp
   3.957 -    apply (subst int_to_bv_lt0)
   3.958 -    apply (subgoal_tac "- int (bv_to_nat (bv_not (\<zero> # bs))) + -1 < 0 + 0")
   3.959 -    apply simp
   3.960 -    apply (rule add_le_less_mono)
   3.961 -    apply simp
   3.962 -    apply simp
   3.963 -    apply (simp del: bv_to_nat1 bv_to_nat_helper)
   3.964 -    apply simp
   3.965 -    done
   3.966 -qed
   3.967 -
   3.968 -lemma bv_int_bv [simp]: "bv_to_int (int_to_bv i) = i"
   3.969 -  by (cases "0 \<le> i") simp_all
   3.970 -
   3.971 -lemma bv_msb_norm [simp]: "bv_msb (norm_signed w) = bv_msb w"
   3.972 -  by (rule bit_list_cases [of w]) (simp_all add: norm_signed_Cons)
   3.973 -
   3.974 -lemma norm_signed_length: "length (norm_signed w) \<le> length w"
   3.975 -  apply (cases w, simp_all)
   3.976 -  apply (subst norm_signed_Cons)
   3.977 -  apply (case_tac a, simp_all)
   3.978 -  apply (rule rem_initial_length)
   3.979 -  done
   3.980 -
   3.981 -lemma norm_signed_equal: "length (norm_signed w) = length w ==> norm_signed w = w"
   3.982 -proof (rule bit_list_cases [of w], simp_all)
   3.983 -  fix xs
   3.984 -  assume "length (norm_signed (\<zero>#xs)) = Suc (length xs)"
   3.985 -  thus "norm_signed (\<zero>#xs) = \<zero>#xs"
   3.986 -    by (simp add: norm_signed_Cons norm_unsigned_equal [THEN eqTrueI]
   3.987 -             split: split_if_asm)
   3.988 -next
   3.989 -  fix xs
   3.990 -  assume "length (norm_signed (\<one>#xs)) = Suc (length xs)"
   3.991 -  thus "norm_signed (\<one>#xs) = \<one>#xs"
   3.992 -    apply (simp add: norm_signed_Cons)
   3.993 -    apply (rule rem_initial_equal)
   3.994 -    apply assumption
   3.995 -    done
   3.996 -qed
   3.997 -
   3.998 -lemma bv_extend_norm_signed: "bv_msb w = b ==> bv_extend (length w) b (norm_signed w) = w"
   3.999 -proof (rule bit_list_cases [of w],simp_all)
  3.1000 -  fix xs
  3.1001 -  show "bv_extend (Suc (length xs)) \<zero> (norm_signed (\<zero>#xs)) = \<zero>#xs"
  3.1002 -  proof (simp add: norm_signed_def,auto)
  3.1003 -    assume "norm_unsigned xs = []"
  3.1004 -    hence xx: "rem_initial \<zero> xs = []"
  3.1005 -      by (simp add: norm_unsigned_def)
  3.1006 -    have "bv_extend (Suc (length xs)) \<zero> (\<zero>#rem_initial \<zero> xs) = \<zero>#xs"
  3.1007 -      apply (simp add: bv_extend_def replicate_app_Cons_same)
  3.1008 -      apply (fold bv_extend_def)
  3.1009 -      apply (rule bv_extend_rem_initial)
  3.1010 -      done
  3.1011 -    thus "bv_extend (Suc (length xs)) \<zero> [\<zero>] = \<zero>#xs"
  3.1012 -      by (simp add: xx)
  3.1013 -  next
  3.1014 -    show "bv_extend (Suc (length xs)) \<zero> (\<zero>#norm_unsigned xs) = \<zero>#xs"
  3.1015 -      apply (simp add: norm_unsigned_def)
  3.1016 -      apply (simp add: bv_extend_def replicate_app_Cons_same)
  3.1017 -      apply (fold bv_extend_def)
  3.1018 -      apply (rule bv_extend_rem_initial)
  3.1019 -      done
  3.1020 -  qed
  3.1021 -next
  3.1022 -  fix xs
  3.1023 -  show "bv_extend (Suc (length xs)) \<one> (norm_signed (\<one>#xs)) = \<one>#xs"
  3.1024 -    apply (simp add: norm_signed_Cons)
  3.1025 -    apply (simp add: bv_extend_def replicate_app_Cons_same)
  3.1026 -    apply (fold bv_extend_def)
  3.1027 -    apply (rule bv_extend_rem_initial)
  3.1028 -    done
  3.1029 -qed
  3.1030 -
  3.1031 -lemma bv_to_int_qinj:
  3.1032 -  assumes one: "bv_to_int xs = bv_to_int ys"
  3.1033 -  and     len: "length xs = length ys"
  3.1034 -  shows        "xs = ys"
  3.1035 -proof -
  3.1036 -  from one
  3.1037 -  have "int_to_bv (bv_to_int xs) = int_to_bv (bv_to_int ys)" by simp
  3.1038 -  hence xsys: "norm_signed xs = norm_signed ys" by simp
  3.1039 -  hence xsys': "bv_msb xs = bv_msb ys"
  3.1040 -  proof -
  3.1041 -    have "bv_msb xs = bv_msb (norm_signed xs)" by simp
  3.1042 -    also have "... = bv_msb (norm_signed ys)" by (simp add: xsys)
  3.1043 -    also have "... = bv_msb ys" by simp
  3.1044 -    finally show ?thesis .
  3.1045 -  qed
  3.1046 -  have "xs = bv_extend (length xs) (bv_msb xs) (norm_signed xs)"
  3.1047 -    by (simp add: bv_extend_norm_signed)
  3.1048 -  also have "... = bv_extend (length ys) (bv_msb ys) (norm_signed ys)"
  3.1049 -    by (simp add: xsys xsys' len)
  3.1050 -  also have "... = ys"
  3.1051 -    by (simp add: bv_extend_norm_signed)
  3.1052 -  finally show ?thesis .
  3.1053 -qed
  3.1054 -
  3.1055 -lemma int_to_bv_returntype [simp]: "norm_signed (int_to_bv w) = int_to_bv w"
  3.1056 -  by (simp add: int_to_bv_def)
  3.1057 -
  3.1058 -lemma bv_to_int_msb0: "0 \<le> bv_to_int w1 ==> bv_msb w1 = \<zero>"
  3.1059 -  by (rule bit_list_cases,simp_all)
  3.1060 -
  3.1061 -lemma bv_to_int_msb1: "bv_to_int w1 < 0 ==> bv_msb w1 = \<one>"
  3.1062 -  by (rule bit_list_cases,simp_all)
  3.1063 -
  3.1064 -lemma bv_to_int_lower_limit_gt0:
  3.1065 -  assumes w0: "0 < bv_to_int w"
  3.1066 -  shows       "2 ^ (length (norm_signed w) - 2) \<le> bv_to_int w"
  3.1067 -proof -
  3.1068 -  from w0
  3.1069 -  have "0 \<le> bv_to_int w" by simp
  3.1070 -  hence [simp]: "bv_msb w = \<zero>" by (rule bv_to_int_msb0)
  3.1071 -  have "2 ^ (length (norm_signed w) - 2) \<le> bv_to_int (norm_signed w)"
  3.1072 -  proof (rule bit_list_cases [of w])
  3.1073 -    assume "w = []"
  3.1074 -    with w0 show ?thesis by simp
  3.1075 -  next
  3.1076 -    fix w'
  3.1077 -    assume weq: "w = \<zero> # w'"
  3.1078 -    thus ?thesis
  3.1079 -    proof (simp add: norm_signed_Cons,safe)
  3.1080 -      assume "norm_unsigned w' = []"
  3.1081 -      with weq and w0 show False
  3.1082 -        by (simp add: norm_empty_bv_to_nat_zero)
  3.1083 -    next
  3.1084 -      assume w'0: "norm_unsigned w' \<noteq> []"
  3.1085 -      have "0 < bv_to_nat w'"
  3.1086 -      proof (rule ccontr)
  3.1087 -        assume "~ (0 < bv_to_nat w')"
  3.1088 -        hence "bv_to_nat w' = 0"
  3.1089 -          by arith
  3.1090 -        hence "norm_unsigned w' = []"
  3.1091 -          by (simp add: bv_to_nat_zero_imp_empty)
  3.1092 -        with w'0
  3.1093 -        show False by simp
  3.1094 -      qed
  3.1095 -      with bv_to_nat_lower_limit [of w']
  3.1096 -      show "2 ^ (length (norm_unsigned w') - Suc 0) \<le> int (bv_to_nat w')"
  3.1097 -        by (simp add: int_nat_two_exp)
  3.1098 -    qed
  3.1099 -  next
  3.1100 -    fix w'
  3.1101 -    assume "w = \<one> # w'"
  3.1102 -    from w0 have "bv_msb w = \<zero>" by simp
  3.1103 -    with prems show ?thesis by simp
  3.1104 -  qed
  3.1105 -  also have "...  = bv_to_int w" by simp
  3.1106 -  finally show ?thesis .
  3.1107 -qed
  3.1108 -
  3.1109 -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))"
  3.1110 -  apply (rule bit_list_cases [of w],simp_all)
  3.1111 -  apply (case_tac "bs",simp_all)
  3.1112 -  apply (case_tac "a",simp_all)
  3.1113 -  apply (simp add: norm_signed_Cons)
  3.1114 -  apply safe
  3.1115 -  apply simp
  3.1116 -proof -
  3.1117 -  fix l
  3.1118 -  assume msb: "\<zero> = bv_msb (norm_unsigned l)"
  3.1119 -  assume "norm_unsigned l \<noteq> []"
  3.1120 -  with norm_unsigned_result [of l]
  3.1121 -  have "bv_msb (norm_unsigned l) = \<one>" by simp
  3.1122 -  with msb show False by simp
  3.1123 -next
  3.1124 -  fix xs
  3.1125 -  assume p: "\<one> = bv_msb (tl (norm_signed (\<one> # xs)))"
  3.1126 -  have "\<one> \<noteq> bv_msb (tl (norm_signed (\<one> # xs)))"
  3.1127 -    by (rule bit_list_induct [of _ xs],simp_all)
  3.1128 -  with p show False by simp
  3.1129 -qed
  3.1130 -
  3.1131 -lemma bv_to_int_upper_limit_lem1:
  3.1132 -  assumes w0: "bv_to_int w < -1"
  3.1133 -  shows       "bv_to_int w < - (2 ^ (length (norm_signed w) - 2))"
  3.1134 -proof -
  3.1135 -  from w0
  3.1136 -  have "bv_to_int w < 0" by simp
  3.1137 -  hence msbw [simp]: "bv_msb w = \<one>"
  3.1138 -    by (rule bv_to_int_msb1)
  3.1139 -  have "bv_to_int w = bv_to_int (norm_signed w)" by simp
  3.1140 -  also from norm_signed_result [of w]
  3.1141 -  have "... < - (2 ^ (length (norm_signed w) - 2))"
  3.1142 -  proof safe
  3.1143 -    assume "norm_signed w = []"
  3.1144 -    hence "bv_to_int (norm_signed w) = 0" by simp
  3.1145 -    with w0 show ?thesis by simp
  3.1146 -  next
  3.1147 -    assume "norm_signed w = [\<one>]"
  3.1148 -    hence "bv_to_int (norm_signed w) = -1" by simp
  3.1149 -    with w0 show ?thesis by simp
  3.1150 -  next
  3.1151 -    assume "bv_msb (norm_signed w) \<noteq> bv_msb (tl (norm_signed w))"
  3.1152 -    hence msb_tl: "\<one> \<noteq> bv_msb (tl (norm_signed w))" by simp
  3.1153 -    show "bv_to_int (norm_signed w) < - (2 ^ (length (norm_signed w) - 2))"
  3.1154 -    proof (rule bit_list_cases [of "norm_signed w"])
  3.1155 -      assume "norm_signed w = []"
  3.1156 -      hence "bv_to_int (norm_signed w) = 0" by simp
  3.1157 -      with w0 show ?thesis by simp
  3.1158 -    next
  3.1159 -      fix w'
  3.1160 -      assume nw: "norm_signed w = \<zero> # w'"
  3.1161 -      from msbw have "bv_msb (norm_signed w) = \<one>" by simp
  3.1162 -      with nw show ?thesis by simp
  3.1163 -    next
  3.1164 -      fix w'
  3.1165 -      assume weq: "norm_signed w = \<one> # w'"
  3.1166 -      show ?thesis
  3.1167 -      proof (rule bit_list_cases [of w'])
  3.1168 -        assume w'eq: "w' = []"
  3.1169 -        from w0 have "bv_to_int (norm_signed w) < -1" by simp
  3.1170 -        with w'eq and weq show ?thesis by simp
  3.1171 -      next
  3.1172 -        fix w''
  3.1173 -        assume w'eq: "w' = \<zero> # w''"
  3.1174 -        show ?thesis
  3.1175 -          apply (simp add: weq w'eq)
  3.1176 -          apply (subgoal_tac "- int (bv_to_nat (bv_not w'')) + -1 < 0 + 0")
  3.1177 -          apply (simp add: int_nat_two_exp)
  3.1178 -          apply (rule add_le_less_mono)
  3.1179 -          apply simp_all
  3.1180 -          done
  3.1181 -      next
  3.1182 -        fix w''
  3.1183 -        assume w'eq: "w' = \<one> # w''"
  3.1184 -        with weq and msb_tl show ?thesis by simp
  3.1185 -      qed
  3.1186 -    qed
  3.1187 -  qed
  3.1188 -  finally show ?thesis .
  3.1189 -qed
  3.1190 -
  3.1191 -lemma length_int_to_bv_upper_limit_gt0:
  3.1192 -  assumes w0: "0 < i"
  3.1193 -  and     wk: "i \<le> 2 ^ (k - 1) - 1"
  3.1194 -  shows       "length (int_to_bv i) \<le> k"
  3.1195 -proof (rule ccontr)
  3.1196 -  from w0 wk
  3.1197 -  have k1: "1 < k"
  3.1198 -    by (cases "k - 1",simp_all)
  3.1199 -  assume "~ length (int_to_bv i) \<le> k"
  3.1200 -  hence "k < length (int_to_bv i)" by simp
  3.1201 -  hence "k \<le> length (int_to_bv i) - 1" by arith
  3.1202 -  hence a: "k - 1 \<le> length (int_to_bv i) - 2" by arith
  3.1203 -  hence "(2::int) ^ (k - 1) \<le> 2 ^ (length (int_to_bv i) - 2)" by simp
  3.1204 -  also have "... \<le> i"
  3.1205 -  proof -
  3.1206 -    have "2 ^ (length (norm_signed (int_to_bv i)) - 2) \<le> bv_to_int (int_to_bv i)"
  3.1207 -    proof (rule bv_to_int_lower_limit_gt0)
  3.1208 -      from w0 show "0 < bv_to_int (int_to_bv i)" by simp
  3.1209 -    qed
  3.1210 -    thus ?thesis by simp
  3.1211 -  qed
  3.1212 -  finally have "2 ^ (k - 1) \<le> i" .
  3.1213 -  with wk show False by simp
  3.1214 -qed
  3.1215 -
  3.1216 -lemma pos_length_pos:
  3.1217 -  assumes i0: "0 < bv_to_int w"
  3.1218 -  shows       "0 < length w"
  3.1219 -proof -
  3.1220 -  from norm_signed_result [of w]
  3.1221 -  have "0 < length (norm_signed w)"
  3.1222 -  proof (auto)
  3.1223 -    assume ii: "norm_signed w = []"
  3.1224 -    have "bv_to_int (norm_signed w) = 0" by (subst ii) simp
  3.1225 -    hence "bv_to_int w = 0" by simp
  3.1226 -    with i0 show False by simp
  3.1227 -  next
  3.1228 -    assume ii: "norm_signed w = []"
  3.1229 -    assume jj: "bv_msb w \<noteq> \<zero>"
  3.1230 -    have "\<zero> = bv_msb (norm_signed w)"
  3.1231 -      by (subst ii) simp
  3.1232 -    also have "... \<noteq> \<zero>"
  3.1233 -      by (simp add: jj)
  3.1234 -    finally show False by simp
  3.1235 -  qed
  3.1236 -  also have "... \<le> length w"
  3.1237 -    by (rule norm_signed_length)
  3.1238 -  finally show ?thesis .
  3.1239 -qed
  3.1240 -
  3.1241 -lemma neg_length_pos:
  3.1242 -  assumes i0: "bv_to_int w < -1"
  3.1243 -  shows       "0 < length w"
  3.1244 -proof -
  3.1245 -  from norm_signed_result [of w]
  3.1246 -  have "0 < length (norm_signed w)"
  3.1247 -  proof (auto)
  3.1248 -    assume ii: "norm_signed w = []"
  3.1249 -    have "bv_to_int (norm_signed w) = 0"
  3.1250 -      by (subst ii) simp
  3.1251 -    hence "bv_to_int w = 0" by simp
  3.1252 -    with i0 show False by simp
  3.1253 -  next
  3.1254 -    assume ii: "norm_signed w = []"
  3.1255 -    assume jj: "bv_msb w \<noteq> \<zero>"
  3.1256 -    have "\<zero> = bv_msb (norm_signed w)" by (subst ii) simp
  3.1257 -    also have "... \<noteq> \<zero>" by (simp add: jj)
  3.1258 -    finally show False by simp
  3.1259 -  qed
  3.1260 -  also have "... \<le> length w"
  3.1261 -    by (rule norm_signed_length)
  3.1262 -  finally show ?thesis .
  3.1263 -qed
  3.1264 -
  3.1265 -lemma length_int_to_bv_lower_limit_gt0:
  3.1266 -  assumes wk: "2 ^ (k - 1) \<le> i"
  3.1267 -  shows       "k < length (int_to_bv i)"
  3.1268 -proof (rule ccontr)
  3.1269 -  have "0 < (2::int) ^ (k - 1)"
  3.1270 -    by (rule zero_less_power) simp
  3.1271 -  also have "... \<le> i" by (rule wk)
  3.1272 -  finally have i0: "0 < i" .
  3.1273 -  have lii0: "0 < length (int_to_bv i)"
  3.1274 -    apply (rule pos_length_pos)
  3.1275 -    apply (simp,rule i0)
  3.1276 -    done
  3.1277 -  assume "~ k < length (int_to_bv i)"
  3.1278 -  hence "length (int_to_bv i) \<le> k" by simp
  3.1279 -  with lii0
  3.1280 -  have a: "length (int_to_bv i) - 1 \<le> k - 1"
  3.1281 -    by arith
  3.1282 -  have "i < 2 ^ (length (int_to_bv i) - 1)"
  3.1283 -  proof -
  3.1284 -    have "i = bv_to_int (int_to_bv i)"
  3.1285 -      by simp
  3.1286 -    also have "... < 2 ^ (length (int_to_bv i) - 1)"
  3.1287 -      by (rule bv_to_int_upper_range)
  3.1288 -    finally show ?thesis .
  3.1289 -  qed
  3.1290 -  also have "(2::int) ^ (length (int_to_bv i) - 1) \<le> 2 ^ (k - 1)" using a
  3.1291 -    by simp
  3.1292 -  finally have "i < 2 ^ (k - 1)" .
  3.1293 -  with wk show False by simp
  3.1294 -qed
  3.1295 -
  3.1296 -lemma length_int_to_bv_upper_limit_lem1:
  3.1297 -  assumes w1: "i < -1"
  3.1298 -  and     wk: "- (2 ^ (k - 1)) \<le> i"
  3.1299 -  shows       "length (int_to_bv i) \<le> k"
  3.1300 -proof (rule ccontr)
  3.1301 -  from w1 wk
  3.1302 -  have k1: "1 < k" by (cases "k - 1") simp_all
  3.1303 -  assume "~ length (int_to_bv i) \<le> k"
  3.1304 -  hence "k < length (int_to_bv i)" by simp
  3.1305 -  hence "k \<le> length (int_to_bv i) - 1" by arith
  3.1306 -  hence a: "k - 1 \<le> length (int_to_bv i) - 2" by arith
  3.1307 -  have "i < - (2 ^ (length (int_to_bv i) - 2))"
  3.1308 -  proof -
  3.1309 -    have "i = bv_to_int (int_to_bv i)"
  3.1310 -      by simp
  3.1311 -    also have "... < - (2 ^ (length (norm_signed (int_to_bv i)) - 2))"
  3.1312 -      by (rule bv_to_int_upper_limit_lem1,simp,rule w1)
  3.1313 -    finally show ?thesis by simp
  3.1314 -  qed
  3.1315 -  also have "... \<le> -(2 ^ (k - 1))"
  3.1316 -  proof -
  3.1317 -    have "(2::int) ^ (k - 1) \<le> 2 ^ (length (int_to_bv i) - 2)" using a by simp
  3.1318 -    thus ?thesis by simp
  3.1319 -  qed
  3.1320 -  finally have "i < -(2 ^ (k - 1))" .
  3.1321 -  with wk show False by simp
  3.1322 -qed
  3.1323 -
  3.1324 -lemma length_int_to_bv_lower_limit_lem1:
  3.1325 -  assumes wk: "i < -(2 ^ (k - 1))"
  3.1326 -  shows       "k < length (int_to_bv i)"
  3.1327 -proof (rule ccontr)
  3.1328 -  from wk have "i \<le> -(2 ^ (k - 1)) - 1" by simp
  3.1329 -  also have "... < -1"
  3.1330 -  proof -
  3.1331 -    have "0 < (2::int) ^ (k - 1)"
  3.1332 -      by (rule zero_less_power) simp
  3.1333 -    hence "-((2::int) ^ (k - 1)) < 0" by simp
  3.1334 -    thus ?thesis by simp
  3.1335 -  qed
  3.1336 -  finally have i1: "i < -1" .
  3.1337 -  have lii0: "0 < length (int_to_bv i)"
  3.1338 -    apply (rule neg_length_pos)
  3.1339 -    apply (simp, rule i1)
  3.1340 -    done
  3.1341 -  assume "~ k < length (int_to_bv i)"
  3.1342 -  hence "length (int_to_bv i) \<le> k"
  3.1343 -    by simp
  3.1344 -  with lii0 have a: "length (int_to_bv i) - 1 \<le> k - 1" by arith
  3.1345 -  hence "(2::int) ^ (length (int_to_bv i) - 1) \<le> 2 ^ (k - 1)" by simp
  3.1346 -  hence "-((2::int) ^ (k - 1)) \<le> - (2 ^ (length (int_to_bv i) - 1))" by simp
  3.1347 -  also have "... \<le> i"
  3.1348 -  proof -
  3.1349 -    have "- (2 ^ (length (int_to_bv i) - 1)) \<le> bv_to_int (int_to_bv i)"
  3.1350 -      by (rule bv_to_int_lower_range)
  3.1351 -    also have "... = i"
  3.1352 -      by simp
  3.1353 -    finally show ?thesis .
  3.1354 -  qed
  3.1355 -  finally have "-(2 ^ (k - 1)) \<le> i" .
  3.1356 -  with wk show False by simp
  3.1357 -qed
  3.1358 -
  3.1359 -
  3.1360 -subsection {* Signed Arithmetic Operations *}
  3.1361 -
  3.1362 -subsubsection {* Conversion from unsigned to signed *}
  3.1363 -
  3.1364 -definition
  3.1365 -  utos :: "bit list => bit list" where
  3.1366 -  "utos w = norm_signed (\<zero> # w)"
  3.1367 -
  3.1368 -lemma utos_type [simp]: "utos (norm_unsigned w) = utos w"
  3.1369 -  by (simp add: utos_def norm_signed_Cons)
  3.1370 -
  3.1371 -lemma utos_returntype [simp]: "norm_signed (utos w) = utos w"
  3.1372 -  by (simp add: utos_def)
  3.1373 -
  3.1374 -lemma utos_length: "length (utos w) \<le> Suc (length w)"
  3.1375 -  by (simp add: utos_def norm_signed_Cons)
  3.1376 -
  3.1377 -lemma bv_to_int_utos: "bv_to_int (utos w) = int (bv_to_nat w)"
  3.1378 -proof (simp add: utos_def norm_signed_Cons, safe)
  3.1379 -  assume "norm_unsigned w = []"
  3.1380 -  hence "bv_to_nat (norm_unsigned w) = 0" by simp
  3.1381 -  thus "bv_to_nat w = 0" by simp
  3.1382 -qed
  3.1383 -
  3.1384 -
  3.1385 -subsubsection {* Unary minus *}
  3.1386 -
  3.1387 -definition
  3.1388 -  bv_uminus :: "bit list => bit list" where
  3.1389 -  "bv_uminus w = int_to_bv (- bv_to_int w)"
  3.1390 -
  3.1391 -lemma bv_uminus_type [simp]: "bv_uminus (norm_signed w) = bv_uminus w"
  3.1392 -  by (simp add: bv_uminus_def)
  3.1393 -
  3.1394 -lemma bv_uminus_returntype [simp]: "norm_signed (bv_uminus w) = bv_uminus w"
  3.1395 -  by (simp add: bv_uminus_def)
  3.1396 -
  3.1397 -lemma bv_uminus_length: "length (bv_uminus w) \<le> Suc (length w)"
  3.1398 -proof -
  3.1399 -  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"
  3.1400 -    by arith
  3.1401 -  thus ?thesis
  3.1402 -  proof safe
  3.1403 -    assume p: "1 < - bv_to_int w"
  3.1404 -    have lw: "0 < length w"
  3.1405 -      apply (rule neg_length_pos)
  3.1406 -      using p
  3.1407 -      apply simp
  3.1408 -      done
  3.1409 -    show ?thesis
  3.1410 -    proof (simp add: bv_uminus_def,rule length_int_to_bv_upper_limit_gt0,simp_all)
  3.1411 -      from prems show "bv_to_int w < 0" by simp
  3.1412 -    next
  3.1413 -      have "-(2^(length w - 1)) \<le> bv_to_int w"
  3.1414 -        by (rule bv_to_int_lower_range)
  3.1415 -      hence "- bv_to_int w \<le> 2^(length w - 1)" by simp
  3.1416 -      also from lw have "... < 2 ^ length w" by simp
  3.1417 -      finally show "- bv_to_int w < 2 ^ length w" by simp
  3.1418 -    qed
  3.1419 -  next
  3.1420 -    assume p: "- bv_to_int w = 1"
  3.1421 -    hence lw: "0 < length w" by (cases w) simp_all
  3.1422 -    from p
  3.1423 -    show ?thesis
  3.1424 -      apply (simp add: bv_uminus_def)
  3.1425 -      using lw
  3.1426 -      apply (simp (no_asm) add: nat_to_bv_non0)
  3.1427 -      done
  3.1428 -  next
  3.1429 -    assume "- bv_to_int w = 0"
  3.1430 -    thus ?thesis by (simp add: bv_uminus_def)
  3.1431 -  next
  3.1432 -    assume p: "- bv_to_int w = -1"
  3.1433 -    thus ?thesis by (simp add: bv_uminus_def)
  3.1434 -  next
  3.1435 -    assume p: "- bv_to_int w < -1"
  3.1436 -    show ?thesis
  3.1437 -      apply (simp add: bv_uminus_def)
  3.1438 -      apply (rule length_int_to_bv_upper_limit_lem1)
  3.1439 -      apply (rule p)
  3.1440 -      apply simp
  3.1441 -    proof -
  3.1442 -      have "bv_to_int w < 2 ^ (length w - 1)"
  3.1443 -        by (rule bv_to_int_upper_range)
  3.1444 -      also have "... \<le> 2 ^ length w" by simp
  3.1445 -      finally show "bv_to_int w \<le> 2 ^ length w" by simp
  3.1446 -    qed
  3.1447 -  qed
  3.1448 -qed
  3.1449 -
  3.1450 -lemma bv_uminus_length_utos: "length (bv_uminus (utos w)) \<le> Suc (length w)"
  3.1451 -proof -
  3.1452 -  have "-bv_to_int (utos w) = 0 \<or> -bv_to_int (utos w) = -1 \<or> -bv_to_int (utos w) < -1"
  3.1453 -    by (simp add: bv_to_int_utos, arith)
  3.1454 -  thus ?thesis
  3.1455 -  proof safe
  3.1456 -    assume "-bv_to_int (utos w) = 0"
  3.1457 -    thus ?thesis by (simp add: bv_uminus_def)
  3.1458 -  next
  3.1459 -    assume "-bv_to_int (utos w) = -1"
  3.1460 -    thus ?thesis by (simp add: bv_uminus_def)
  3.1461 -  next
  3.1462 -    assume p: "-bv_to_int (utos w) < -1"
  3.1463 -    show ?thesis
  3.1464 -      apply (simp add: bv_uminus_def)
  3.1465 -      apply (rule length_int_to_bv_upper_limit_lem1)
  3.1466 -      apply (rule p)
  3.1467 -      apply (simp add: bv_to_int_utos)
  3.1468 -      using bv_to_nat_upper_range [of w]
  3.1469 -      apply (simp add: int_nat_two_exp)
  3.1470 -      done
  3.1471 -  qed
  3.1472 -qed
  3.1473 -
  3.1474 -definition
  3.1475 -  bv_sadd :: "[bit list, bit list ] => bit list" where
  3.1476 -  "bv_sadd w1 w2 = int_to_bv (bv_to_int w1 + bv_to_int w2)"
  3.1477 -
  3.1478 -lemma bv_sadd_type1 [simp]: "bv_sadd (norm_signed w1) w2 = bv_sadd w1 w2"
  3.1479 -  by (simp add: bv_sadd_def)
  3.1480 -
  3.1481 -lemma bv_sadd_type2 [simp]: "bv_sadd w1 (norm_signed w2) = bv_sadd w1 w2"
  3.1482 -  by (simp add: bv_sadd_def)
  3.1483 -
  3.1484 -lemma bv_sadd_returntype [simp]: "norm_signed (bv_sadd w1 w2) = bv_sadd w1 w2"
  3.1485 -  by (simp add: bv_sadd_def)
  3.1486 -
  3.1487 -lemma adder_helper:
  3.1488 -  assumes lw: "0 < max (length w1) (length w2)"
  3.1489 -  shows   "((2::int) ^ (length w1 - 1)) + (2 ^ (length w2 - 1)) \<le> 2 ^ max (length w1) (length w2)"
  3.1490 -proof -
  3.1491 -  have "((2::int) ^ (length w1 - 1)) + (2 ^ (length w2 - 1)) \<le>
  3.1492 -      2 ^ (max (length w1) (length w2) - 1) + 2 ^ (max (length w1) (length w2) - 1)"
  3.1493 -    by (auto simp:max_def)
  3.1494 -  also have "... = 2 ^ max (length w1) (length w2)"
  3.1495 -  proof -
  3.1496 -    from lw
  3.1497 -    show ?thesis
  3.1498 -      apply simp
  3.1499 -      apply (subst power_Suc [symmetric])
  3.1500 -      apply simp
  3.1501 -      done
  3.1502 -  qed
  3.1503 -  finally show ?thesis .
  3.1504 -qed
  3.1505 -
  3.1506 -lemma bv_sadd_length: "length (bv_sadd w1 w2) \<le> Suc (max (length w1) (length w2))"
  3.1507 -proof -
  3.1508 -  let ?Q = "bv_to_int w1 + bv_to_int w2"
  3.1509 -
  3.1510 -  have helper: "?Q \<noteq> 0 ==> 0 < max (length w1) (length w2)"
  3.1511 -  proof -
  3.1512 -    assume p: "?Q \<noteq> 0"
  3.1513 -    show "0 < max (length w1) (length w2)"
  3.1514 -    proof (simp add: less_max_iff_disj,rule)
  3.1515 -      assume [simp]: "w1 = []"
  3.1516 -      show "w2 \<noteq> []"
  3.1517 -      proof (rule ccontr,simp)
  3.1518 -        assume [simp]: "w2 = []"
  3.1519 -        from p show False by simp
  3.1520 -      qed
  3.1521 -    qed
  3.1522 -  qed
  3.1523 -
  3.1524 -  have "0 < ?Q \<or> ?Q = 0 \<or> ?Q = -1 \<or> ?Q < -1" by arith
  3.1525 -  thus ?thesis
  3.1526 -  proof safe
  3.1527 -    assume "?Q = 0"
  3.1528 -    thus ?thesis
  3.1529 -      by (simp add: bv_sadd_def)
  3.1530 -  next
  3.1531 -    assume "?Q = -1"
  3.1532 -    thus ?thesis
  3.1533 -      by (simp add: bv_sadd_def)
  3.1534 -  next
  3.1535 -    assume p: "0 < ?Q"
  3.1536 -    show ?thesis
  3.1537 -      apply (simp add: bv_sadd_def)
  3.1538 -      apply (rule length_int_to_bv_upper_limit_gt0)
  3.1539 -      apply (rule p)
  3.1540 -    proof simp
  3.1541 -      from bv_to_int_upper_range [of w2]
  3.1542 -      have "bv_to_int w2 \<le> 2 ^ (length w2 - 1)"
  3.1543 -        by simp
  3.1544 -      with bv_to_int_upper_range [of w1]
  3.1545 -      have "bv_to_int w1 + bv_to_int w2 < (2 ^ (length w1 - 1)) + (2 ^ (length w2 - 1))"
  3.1546 -        by (rule zadd_zless_mono)
  3.1547 -      also have "... \<le> 2 ^ max (length w1) (length w2)"
  3.1548 -        apply (rule adder_helper)
  3.1549 -        apply (rule helper)
  3.1550 -        using p
  3.1551 -        apply simp
  3.1552 -        done
  3.1553 -      finally show "?Q < 2 ^ max (length w1) (length w2)" .
  3.1554 -    qed
  3.1555 -  next
  3.1556 -    assume p: "?Q < -1"
  3.1557 -    show ?thesis
  3.1558 -      apply (simp add: bv_sadd_def)
  3.1559 -      apply (rule length_int_to_bv_upper_limit_lem1,simp_all)
  3.1560 -      apply (rule p)
  3.1561 -    proof -
  3.1562 -      have "(2 ^ (length w1 - 1)) + 2 ^ (length w2 - 1) \<le> (2::int) ^ max (length w1) (length w2)"
  3.1563 -        apply (rule adder_helper)
  3.1564 -        apply (rule helper)
  3.1565 -        using p
  3.1566 -        apply simp
  3.1567 -        done
  3.1568 -      hence "-((2::int) ^ max (length w1) (length w2)) \<le> - (2 ^ (length w1 - 1)) + -(2 ^ (length w2 - 1))"
  3.1569 -        by simp
  3.1570 -      also have "- (2 ^ (length w1 - 1)) + -(2 ^ (length w2 - 1)) \<le> ?Q"
  3.1571 -        apply (rule add_mono)
  3.1572 -        apply (rule bv_to_int_lower_range [of w1])
  3.1573 -        apply (rule bv_to_int_lower_range [of w2])
  3.1574 -        done
  3.1575 -      finally show "- (2^max (length w1) (length w2)) \<le> ?Q" .
  3.1576 -    qed
  3.1577 -  qed
  3.1578 -qed
  3.1579 -
  3.1580 -definition
  3.1581 -  bv_sub :: "[bit list, bit list] => bit list" where
  3.1582 -  "bv_sub w1 w2 = bv_sadd w1 (bv_uminus w2)"
  3.1583 -
  3.1584 -lemma bv_sub_type1 [simp]: "bv_sub (norm_signed w1) w2 = bv_sub w1 w2"
  3.1585 -  by (simp add: bv_sub_def)
  3.1586 -
  3.1587 -lemma bv_sub_type2 [simp]: "bv_sub w1 (norm_signed w2) = bv_sub w1 w2"
  3.1588 -  by (simp add: bv_sub_def)
  3.1589 -
  3.1590 -lemma bv_sub_returntype [simp]: "norm_signed (bv_sub w1 w2) = bv_sub w1 w2"
  3.1591 -  by (simp add: bv_sub_def)
  3.1592 -
  3.1593 -lemma bv_sub_length: "length (bv_sub w1 w2) \<le> Suc (max (length w1) (length w2))"
  3.1594 -proof (cases "bv_to_int w2 = 0")
  3.1595 -  assume p: "bv_to_int w2 = 0"
  3.1596 -  show ?thesis
  3.1597 -  proof (simp add: bv_sub_def bv_sadd_def bv_uminus_def p)
  3.1598 -    have "length (norm_signed w1) \<le> length w1"
  3.1599 -      by (rule norm_signed_length)
  3.1600 -    also have "... \<le> max (length w1) (length w2)"
  3.1601 -      by (rule le_maxI1)
  3.1602 -    also have "... \<le> Suc (max (length w1) (length w2))"
  3.1603 -      by arith
  3.1604 -    finally show "length (norm_signed w1) \<le> Suc (max (length w1) (length w2))" .
  3.1605 -  qed
  3.1606 -next
  3.1607 -  assume "bv_to_int w2 \<noteq> 0"
  3.1608 -  hence "0 < length w2" by (cases w2,simp_all)
  3.1609 -  hence lmw: "0 < max (length w1) (length w2)" by arith
  3.1610 -
  3.1611 -  let ?Q = "bv_to_int w1 - bv_to_int w2"
  3.1612 -
  3.1613 -  have "0 < ?Q \<or> ?Q = 0 \<or> ?Q = -1 \<or> ?Q < -1" by arith
  3.1614 -  thus ?thesis
  3.1615 -  proof safe
  3.1616 -    assume "?Q = 0"
  3.1617 -    thus ?thesis
  3.1618 -      by (simp add: bv_sub_def bv_sadd_def bv_uminus_def)
  3.1619 -  next
  3.1620 -    assume "?Q = -1"
  3.1621 -    thus ?thesis
  3.1622 -      by (simp add: bv_sub_def bv_sadd_def bv_uminus_def)
  3.1623 -  next
  3.1624 -    assume p: "0 < ?Q"
  3.1625 -    show ?thesis
  3.1626 -      apply (simp add: bv_sub_def bv_sadd_def bv_uminus_def)
  3.1627 -      apply (rule length_int_to_bv_upper_limit_gt0)
  3.1628 -      apply (rule p)
  3.1629 -    proof simp
  3.1630 -      from bv_to_int_lower_range [of w2]
  3.1631 -      have v2: "- bv_to_int w2 \<le> 2 ^ (length w2 - 1)" by simp
  3.1632 -      have "bv_to_int w1 + - bv_to_int w2 < (2 ^ (length w1 - 1)) + (2 ^ (length w2 - 1))"
  3.1633 -        apply (rule zadd_zless_mono)
  3.1634 -        apply (rule bv_to_int_upper_range [of w1])
  3.1635 -        apply (rule v2)
  3.1636 -        done
  3.1637 -      also have "... \<le> 2 ^ max (length w1) (length w2)"
  3.1638 -        apply (rule adder_helper)
  3.1639 -        apply (rule lmw)
  3.1640 -        done
  3.1641 -      finally show "?Q < 2 ^ max (length w1) (length w2)" by simp
  3.1642 -    qed
  3.1643 -  next
  3.1644 -    assume p: "?Q < -1"
  3.1645 -    show ?thesis
  3.1646 -      apply (simp add: bv_sub_def bv_sadd_def bv_uminus_def)
  3.1647 -      apply (rule length_int_to_bv_upper_limit_lem1)
  3.1648 -      apply (rule p)
  3.1649 -    proof simp
  3.1650 -      have "(2 ^ (length w1 - 1)) + 2 ^ (length w2 - 1) \<le> (2::int) ^ max (length w1) (length w2)"
  3.1651 -        apply (rule adder_helper)
  3.1652 -        apply (rule lmw)
  3.1653 -        done
  3.1654 -      hence "-((2::int) ^ max (length w1) (length w2)) \<le> - (2 ^ (length w1 - 1)) + -(2 ^ (length w2 - 1))"
  3.1655 -        by simp
  3.1656 -      also have "- (2 ^ (length w1 - 1)) + -(2 ^ (length w2 - 1)) \<le> bv_to_int w1 + -bv_to_int w2"
  3.1657 -        apply (rule add_mono)
  3.1658 -        apply (rule bv_to_int_lower_range [of w1])
  3.1659 -        using bv_to_int_upper_range [of w2]
  3.1660 -        apply simp
  3.1661 -        done
  3.1662 -      finally show "- (2^max (length w1) (length w2)) \<le> ?Q" by simp
  3.1663 -    qed
  3.1664 -  qed
  3.1665 -qed
  3.1666 -
  3.1667 -definition
  3.1668 -  bv_smult :: "[bit list, bit list] => bit list" where
  3.1669 -  "bv_smult w1 w2 = int_to_bv (bv_to_int w1 * bv_to_int w2)"
  3.1670 -
  3.1671 -lemma bv_smult_type1 [simp]: "bv_smult (norm_signed w1) w2 = bv_smult w1 w2"
  3.1672 -  by (simp add: bv_smult_def)
  3.1673 -
  3.1674 -lemma bv_smult_type2 [simp]: "bv_smult w1 (norm_signed w2) = bv_smult w1 w2"
  3.1675 -  by (simp add: bv_smult_def)
  3.1676 -
  3.1677 -lemma bv_smult_returntype [simp]: "norm_signed (bv_smult w1 w2) = bv_smult w1 w2"
  3.1678 -  by (simp add: bv_smult_def)
  3.1679 -
  3.1680 -lemma bv_smult_length: "length (bv_smult w1 w2) \<le> length w1 + length w2"
  3.1681 -proof -
  3.1682 -  let ?Q = "bv_to_int w1 * bv_to_int w2"
  3.1683 -
  3.1684 -  have lmw: "?Q \<noteq> 0 ==> 0 < length w1 \<and> 0 < length w2" by auto
  3.1685 -
  3.1686 -  have "0 < ?Q \<or> ?Q = 0 \<or> ?Q = -1 \<or> ?Q < -1" by arith
  3.1687 -  thus ?thesis
  3.1688 -  proof (safe dest!: iffD1 [OF mult_eq_0_iff])
  3.1689 -    assume "bv_to_int w1 = 0"
  3.1690 -    thus ?thesis by (simp add: bv_smult_def)
  3.1691 -  next
  3.1692 -    assume "bv_to_int w2 = 0"
  3.1693 -    thus ?thesis by (simp add: bv_smult_def)
  3.1694 -  next
  3.1695 -    assume p: "?Q = -1"
  3.1696 -    show ?thesis
  3.1697 -      apply (simp add: bv_smult_def p)
  3.1698 -      apply (cut_tac lmw)
  3.1699 -      apply arith
  3.1700 -      using p
  3.1701 -      apply simp
  3.1702 -      done
  3.1703 -  next
  3.1704 -    assume p: "0 < ?Q"
  3.1705 -    thus ?thesis
  3.1706 -    proof (simp add: zero_less_mult_iff,safe)
  3.1707 -      assume bi1: "0 < bv_to_int w1"
  3.1708 -      assume bi2: "0 < bv_to_int w2"
  3.1709 -      show ?thesis
  3.1710 -        apply (simp add: bv_smult_def)
  3.1711 -        apply (rule length_int_to_bv_upper_limit_gt0)
  3.1712 -        apply (rule p)
  3.1713 -      proof simp
  3.1714 -        have "?Q < 2 ^ (length w1 - 1) * 2 ^ (length w2 - 1)"
  3.1715 -          apply (rule mult_strict_mono)
  3.1716 -          apply (rule bv_to_int_upper_range)
  3.1717 -          apply (rule bv_to_int_upper_range)
  3.1718 -          apply (rule zero_less_power)
  3.1719 -          apply simp
  3.1720 -          using bi2
  3.1721 -          apply simp
  3.1722 -          done
  3.1723 -        also have "... \<le> 2 ^ (length w1 + length w2 - Suc 0)"
  3.1724 -          apply simp
  3.1725 -          apply (subst zpower_zadd_distrib [symmetric])
  3.1726 -          apply simp
  3.1727 -          done
  3.1728 -        finally show "?Q < 2 ^ (length w1 + length w2 - Suc 0)" .
  3.1729 -      qed
  3.1730 -    next
  3.1731 -      assume bi1: "bv_to_int w1 < 0"
  3.1732 -      assume bi2: "bv_to_int w2 < 0"
  3.1733 -      show ?thesis
  3.1734 -        apply (simp add: bv_smult_def)
  3.1735 -        apply (rule length_int_to_bv_upper_limit_gt0)
  3.1736 -        apply (rule p)
  3.1737 -      proof simp
  3.1738 -        have "-bv_to_int w1 * -bv_to_int w2 \<le> 2 ^ (length w1 - 1) * 2 ^(length w2 - 1)"
  3.1739 -          apply (rule mult_mono)
  3.1740 -          using bv_to_int_lower_range [of w1]
  3.1741 -          apply simp
  3.1742 -          using bv_to_int_lower_range [of w2]
  3.1743 -          apply simp
  3.1744 -          apply (rule zero_le_power,simp)
  3.1745 -          using bi2
  3.1746 -          apply simp
  3.1747 -          done
  3.1748 -        hence "?Q \<le> 2 ^ (length w1 - 1) * 2 ^(length w2 - 1)"
  3.1749 -          by simp
  3.1750 -        also have "... < 2 ^ (length w1 + length w2 - Suc 0)"
  3.1751 -          apply simp
  3.1752 -          apply (subst zpower_zadd_distrib [symmetric])
  3.1753 -          apply simp
  3.1754 -          apply (cut_tac lmw)
  3.1755 -          apply arith
  3.1756 -          apply (cut_tac p)
  3.1757 -          apply arith
  3.1758 -          done
  3.1759 -        finally show "?Q < 2 ^ (length w1 + length w2 - Suc 0)" .
  3.1760 -      qed
  3.1761 -    qed
  3.1762 -  next
  3.1763 -    assume p: "?Q < -1"
  3.1764 -    show ?thesis
  3.1765 -      apply (subst bv_smult_def)
  3.1766 -      apply (rule length_int_to_bv_upper_limit_lem1)
  3.1767 -      apply (rule p)
  3.1768 -    proof simp
  3.1769 -      have "(2::int) ^ (length w1 - 1) * 2 ^(length w2 - 1) \<le> 2 ^ (length w1 + length w2 - Suc 0)"
  3.1770 -        apply simp
  3.1771 -        apply (subst zpower_zadd_distrib [symmetric])
  3.1772 -        apply simp
  3.1773 -        done
  3.1774 -      hence "-((2::int) ^ (length w1 + length w2 - Suc 0)) \<le> -(2^(length w1 - 1) * 2 ^ (length w2 - 1))"
  3.1775 -        by simp
  3.1776 -      also have "... \<le> ?Q"
  3.1777 -      proof -
  3.1778 -        from p
  3.1779 -        have q: "bv_to_int w1 * bv_to_int w2 < 0"
  3.1780 -          by simp
  3.1781 -        thus ?thesis
  3.1782 -        proof (simp add: mult_less_0_iff,safe)
  3.1783 -          assume bi1: "0 < bv_to_int w1"
  3.1784 -          assume bi2: "bv_to_int w2 < 0"
  3.1785 -          have "-bv_to_int w2 * bv_to_int w1 \<le> ((2::int)^(length w2 - 1)) * (2 ^ (length w1 - 1))"
  3.1786 -            apply (rule mult_mono)
  3.1787 -            using bv_to_int_lower_range [of w2]
  3.1788 -            apply simp
  3.1789 -            using bv_to_int_upper_range [of w1]
  3.1790 -            apply simp
  3.1791 -            apply (rule zero_le_power,simp)
  3.1792 -            using bi1
  3.1793 -            apply simp
  3.1794 -            done
  3.1795 -          hence "-?Q \<le> ((2::int)^(length w1 - 1)) * (2 ^ (length w2 - 1))"
  3.1796 -            by (simp add: zmult_ac)
  3.1797 -          thus "-(((2::int)^(length w1 - Suc 0)) * (2 ^ (length w2 - Suc 0))) \<le> ?Q"
  3.1798 -            by simp
  3.1799 -        next
  3.1800 -          assume bi1: "bv_to_int w1 < 0"
  3.1801 -          assume bi2: "0 < bv_to_int w2"
  3.1802 -          have "-bv_to_int w1 * bv_to_int w2 \<le> ((2::int)^(length w1 - 1)) * (2 ^ (length w2 - 1))"
  3.1803 -            apply (rule mult_mono)
  3.1804 -            using bv_to_int_lower_range [of w1]
  3.1805 -            apply simp
  3.1806 -            using bv_to_int_upper_range [of w2]
  3.1807 -            apply simp
  3.1808 -            apply (rule zero_le_power,simp)
  3.1809 -            using bi2
  3.1810 -            apply simp
  3.1811 -            done
  3.1812 -          hence "-?Q \<le> ((2::int)^(length w1 - 1)) * (2 ^ (length w2 - 1))"
  3.1813 -            by (simp add: zmult_ac)
  3.1814 -          thus "-(((2::int)^(length w1 - Suc 0)) * (2 ^ (length w2 - Suc 0))) \<le> ?Q"
  3.1815 -            by simp
  3.1816 -        qed
  3.1817 -      qed
  3.1818 -      finally show "-(2 ^ (length w1 + length w2 - Suc 0)) \<le> ?Q" .
  3.1819 -    qed
  3.1820 -  qed
  3.1821 -qed
  3.1822 -
  3.1823 -lemma bv_msb_one: "bv_msb w = \<one> ==> bv_to_nat w \<noteq> 0"
  3.1824 -by (cases w) simp_all
  3.1825 -
  3.1826 -lemma bv_smult_length_utos: "length (bv_smult (utos w1) w2) \<le> length w1 + length w2"
  3.1827 -proof -
  3.1828 -  let ?Q = "bv_to_int (utos w1) * bv_to_int w2"
  3.1829 -
  3.1830 -  have lmw: "?Q \<noteq> 0 ==> 0 < length (utos w1) \<and> 0 < length w2" by auto
  3.1831 -
  3.1832 -  have "0 < ?Q \<or> ?Q = 0 \<or> ?Q = -1 \<or> ?Q < -1" by arith
  3.1833 -  thus ?thesis
  3.1834 -  proof (safe dest!: iffD1 [OF mult_eq_0_iff])
  3.1835 -    assume "bv_to_int (utos w1) = 0"
  3.1836 -    thus ?thesis by (simp add: bv_smult_def)
  3.1837 -  next
  3.1838 -    assume "bv_to_int w2 = 0"
  3.1839 -    thus ?thesis by (simp add: bv_smult_def)
  3.1840 -  next
  3.1841 -    assume p: "0 < ?Q"
  3.1842 -    thus ?thesis
  3.1843 -    proof (simp add: zero_less_mult_iff,safe)
  3.1844 -      assume biw2: "0 < bv_to_int w2"
  3.1845 -      show ?thesis
  3.1846 -        apply (simp add: bv_smult_def)
  3.1847 -        apply (rule length_int_to_bv_upper_limit_gt0)
  3.1848 -        apply (rule p)
  3.1849 -      proof simp
  3.1850 -        have "?Q < 2 ^ length w1 * 2 ^ (length w2 - 1)"
  3.1851 -          apply (rule mult_strict_mono)
  3.1852 -          apply (simp add: bv_to_int_utos int_nat_two_exp)
  3.1853 -          apply (rule bv_to_nat_upper_range)
  3.1854 -          apply (rule bv_to_int_upper_range)
  3.1855 -          apply (rule zero_less_power,simp)
  3.1856 -          using biw2
  3.1857 -          apply simp
  3.1858 -          done
  3.1859 -        also have "... \<le> 2 ^ (length w1 + length w2 - Suc 0)"
  3.1860 -          apply simp
  3.1861 -          apply (subst zpower_zadd_distrib [symmetric])
  3.1862 -          apply simp
  3.1863 -          apply (cut_tac lmw)
  3.1864 -          apply arith
  3.1865 -          using p
  3.1866 -          apply auto
  3.1867 -          done
  3.1868 -        finally show "?Q < 2 ^ (length w1 + length w2 - Suc 0)" .
  3.1869 -      qed
  3.1870 -    next
  3.1871 -      assume "bv_to_int (utos w1) < 0"
  3.1872 -      thus ?thesis by (simp add: bv_to_int_utos)
  3.1873 -    qed
  3.1874 -  next
  3.1875 -    assume p: "?Q = -1"
  3.1876 -    thus ?thesis
  3.1877 -      apply (simp add: bv_smult_def)
  3.1878 -      apply (cut_tac lmw)
  3.1879 -      apply arith
  3.1880 -      apply simp
  3.1881 -      done
  3.1882 -  next
  3.1883 -    assume p: "?Q < -1"
  3.1884 -    show ?thesis
  3.1885 -      apply (subst bv_smult_def)
  3.1886 -      apply (rule length_int_to_bv_upper_limit_lem1)
  3.1887 -      apply (rule p)
  3.1888 -    proof simp
  3.1889 -      have "(2::int) ^ length w1 * 2 ^(length w2 - 1) \<le> 2 ^ (length w1 + length w2 - Suc 0)"
  3.1890 -        apply simp
  3.1891 -        apply (subst zpower_zadd_distrib [symmetric])
  3.1892 -        apply simp
  3.1893 -        apply (cut_tac lmw)
  3.1894 -        apply arith
  3.1895 -        apply (cut_tac p)
  3.1896 -        apply arith
  3.1897 -        done
  3.1898 -      hence "-((2::int) ^ (length w1 + length w2 - Suc 0)) \<le> -(2^ length w1 * 2 ^ (length w2 - 1))"
  3.1899 -        by simp
  3.1900 -      also have "... \<le> ?Q"
  3.1901 -      proof -
  3.1902 -        from p
  3.1903 -        have q: "bv_to_int (utos w1) * bv_to_int w2 < 0"
  3.1904 -          by simp
  3.1905 -        thus ?thesis
  3.1906 -        proof (simp add: mult_less_0_iff,safe)
  3.1907 -          assume bi1: "0 < bv_to_int (utos w1)"
  3.1908 -          assume bi2: "bv_to_int w2 < 0"
  3.1909 -          have "-bv_to_int w2 * bv_to_int (utos w1) \<le> ((2::int)^(length w2 - 1)) * (2 ^ length w1)"
  3.1910 -            apply (rule mult_mono)
  3.1911 -            using bv_to_int_lower_range [of w2]
  3.1912 -            apply simp
  3.1913 -            apply (simp add: bv_to_int_utos)
  3.1914 -            using bv_to_nat_upper_range [of w1]
  3.1915 -            apply (simp add: int_nat_two_exp)
  3.1916 -            apply (rule zero_le_power,simp)
  3.1917 -            using bi1
  3.1918 -            apply simp
  3.1919 -            done
  3.1920 -          hence "-?Q \<le> ((2::int)^length w1) * (2 ^ (length w2 - 1))"
  3.1921 -            by (simp add: zmult_ac)
  3.1922 -          thus "-(((2::int)^length w1) * (2 ^ (length w2 - Suc 0))) \<le> ?Q"
  3.1923 -            by simp
  3.1924 -        next
  3.1925 -          assume bi1: "bv_to_int (utos w1) < 0"
  3.1926 -          thus "-(((2::int)^length w1) * (2 ^ (length w2 - Suc 0))) \<le> ?Q"
  3.1927 -            by (simp add: bv_to_int_utos)
  3.1928 -        qed
  3.1929 -      qed
  3.1930 -      finally show "-(2 ^ (length w1 + length w2 - Suc 0)) \<le> ?Q" .
  3.1931 -    qed
  3.1932 -  qed
  3.1933 -qed
  3.1934 -
  3.1935 -lemma bv_smult_sym: "bv_smult w1 w2 = bv_smult w2 w1"
  3.1936 -  by (simp add: bv_smult_def zmult_ac)
  3.1937 -
  3.1938 -subsection {* Structural operations *}
  3.1939 -
  3.1940 -definition
  3.1941 -  bv_select :: "[bit list,nat] => bit" where
  3.1942 -  "bv_select w i = w ! (length w - 1 - i)"
  3.1943 -
  3.1944 -definition
  3.1945 -  bv_chop :: "[bit list,nat] => bit list * bit list" where
  3.1946 -  "bv_chop w i = (let len = length w in (take (len - i) w,drop (len - i) w))"
  3.1947 -
  3.1948 -definition
  3.1949 -  bv_slice :: "[bit list,nat*nat] => bit list" where
  3.1950 -  "bv_slice w = (\<lambda>(b,e). fst (bv_chop (snd (bv_chop w (b+1))) e))"
  3.1951 -
  3.1952 -lemma bv_select_rev:
  3.1953 -  assumes notnull: "n < length w"
  3.1954 -  shows            "bv_select w n = rev w ! n"
  3.1955 -proof -
  3.1956 -  have "\<forall>n. n < length w --> bv_select w n = rev w ! n"
  3.1957 -  proof (rule length_induct [of _ w],auto simp add: bv_select_def)
  3.1958 -    fix xs :: "bit list"
  3.1959 -    fix n
  3.1960 -    assume ind: "\<forall>ys::bit list. length ys < length xs --> (\<forall>n. n < length ys --> ys ! (length ys - Suc n) = rev ys ! n)"
  3.1961 -    assume notx: "n < length xs"
  3.1962 -    show "xs ! (length xs - Suc n) = rev xs ! n"
  3.1963 -    proof (cases xs)
  3.1964 -      assume "xs = []"
  3.1965 -      with notx show ?thesis by simp
  3.1966 -    next
  3.1967 -      fix y ys
  3.1968 -      assume [simp]: "xs = y # ys"
  3.1969 -      show ?thesis
  3.1970 -      proof (auto simp add: nth_append)
  3.1971 -        assume noty: "n < length ys"
  3.1972 -        from spec [OF ind,of ys]
  3.1973 -        have "\<forall>n. n < length ys --> ys ! (length ys - Suc n) = rev ys ! n"
  3.1974 -          by simp
  3.1975 -        hence "n < length ys --> ys ! (length ys - Suc n) = rev ys ! n" ..
  3.1976 -        from this and noty
  3.1977 -        have "ys ! (length ys - Suc n) = rev ys ! n" ..
  3.1978 -        thus "(y # ys) ! (length ys - n) = rev ys ! n"
  3.1979 -          by (simp add: nth_Cons' noty linorder_not_less [symmetric])
  3.1980 -      next
  3.1981 -        assume "~ n < length ys"
  3.1982 -        hence x: "length ys \<le> n" by simp
  3.1983 -        from notx have "n < Suc (length ys)" by simp
  3.1984 -        hence "n \<le> length ys" by simp
  3.1985 -        with x have "length ys = n" by simp
  3.1986 -        thus "y = [y] ! (n - length ys)" by simp
  3.1987 -      qed
  3.1988 -    qed
  3.1989 -  qed
  3.1990 -  then have "n < length w --> bv_select w n = rev w ! n" ..
  3.1991 -  from this and notnull show ?thesis ..
  3.1992 -qed
  3.1993 -
  3.1994 -lemma bv_chop_append: "bv_chop (w1 @ w2) (length w2) = (w1,w2)"
  3.1995 -  by (simp add: bv_chop_def Let_def)
  3.1996 -
  3.1997 -lemma append_bv_chop_id: "fst (bv_chop w l) @ snd (bv_chop w l) = w"
  3.1998 -  by (simp add: bv_chop_def Let_def)
  3.1999 -
  3.2000 -lemma bv_chop_length_fst [simp]: "length (fst (bv_chop w i)) = length w - i"
  3.2001 -  by (simp add: bv_chop_def Let_def)
  3.2002 -
  3.2003 -lemma bv_chop_length_snd [simp]: "length (snd (bv_chop w i)) = min i (length w)"
  3.2004 -  by (simp add: bv_chop_def Let_def)
  3.2005 -
  3.2006 -lemma bv_slice_length [simp]: "[| j \<le> i; i < length w |] ==> length (bv_slice w (i,j)) = i - j + 1"
  3.2007 -  by (auto simp add: bv_slice_def)
  3.2008 -
  3.2009 -definition
  3.2010 -  length_nat :: "nat => nat" where
  3.2011 -  [code del]: "length_nat x = (LEAST n. x < 2 ^ n)"
  3.2012 -
  3.2013 -lemma length_nat: "length (nat_to_bv n) = length_nat n"
  3.2014 -  apply (simp add: length_nat_def)
  3.2015 -  apply (rule Least_equality [symmetric])
  3.2016 -  prefer 2
  3.2017 -  apply (rule length_nat_to_bv_upper_limit)
  3.2018 -  apply arith
  3.2019 -  apply (rule ccontr)
  3.2020 -proof -
  3.2021 -  assume "~ n < 2 ^ length (nat_to_bv n)"
  3.2022 -  hence "2 ^ length (nat_to_bv n) \<le> n" by simp
  3.2023 -  hence "length (nat_to_bv n) < length (nat_to_bv n)"
  3.2024 -    by (rule length_nat_to_bv_lower_limit)
  3.2025 -  thus False by simp
  3.2026 -qed
  3.2027 -
  3.2028 -lemma length_nat_0 [simp]: "length_nat 0 = 0"
  3.2029 -  by (simp add: length_nat_def Least_equality)
  3.2030 -
  3.2031 -lemma length_nat_non0:
  3.2032 -  assumes n0: "n \<noteq> 0"
  3.2033 -  shows       "length_nat n = Suc (length_nat (n div 2))"
  3.2034 -  apply (simp add: length_nat [symmetric])
  3.2035 -  apply (subst nat_to_bv_non0 [of n])
  3.2036 -  apply (simp_all add: n0)
  3.2037 -  done
  3.2038 -
  3.2039 -definition
  3.2040 -  length_int :: "int => nat" where
  3.2041 -  "length_int x =
  3.2042 -    (if 0 < x then Suc (length_nat (nat x))
  3.2043 -    else if x = 0 then 0
  3.2044 -    else Suc (length_nat (nat (-x - 1))))"
  3.2045 -
  3.2046 -lemma length_int: "length (int_to_bv i) = length_int i"
  3.2047 -proof (cases "0 < i")
  3.2048 -  assume i0: "0 < i"
  3.2049 -  hence "length (int_to_bv i) =
  3.2050 -      length (norm_signed (\<zero> # norm_unsigned (nat_to_bv (nat i))))" by simp
  3.2051 -  also from norm_unsigned_result [of "nat_to_bv (nat i)"]
  3.2052 -  have "... = Suc (length_nat (nat i))"
  3.2053 -    apply safe
  3.2054 -    apply (simp del: norm_unsigned_nat_to_bv)
  3.2055 -    apply (drule norm_empty_bv_to_nat_zero)
  3.2056 -    using prems
  3.2057 -    apply simp
  3.2058 -    apply (cases "norm_unsigned (nat_to_bv (nat i))")
  3.2059 -    apply (drule norm_empty_bv_to_nat_zero [of "nat_to_bv (nat i)"])
  3.2060 -    using prems
  3.2061 -    apply simp
  3.2062 -    apply simp
  3.2063 -    using prems
  3.2064 -    apply (simp add: length_nat [symmetric])
  3.2065 -    done
  3.2066 -  finally show ?thesis
  3.2067 -    using i0
  3.2068 -    by (simp add: length_int_def)
  3.2069 -next
  3.2070 -  assume "~ 0 < i"
  3.2071 -  hence i0: "i \<le> 0" by simp
  3.2072 -  show ?thesis
  3.2073 -  proof (cases "i = 0")
  3.2074 -    assume "i = 0"
  3.2075 -    thus ?thesis by (simp add: length_int_def)
  3.2076 -  next
  3.2077 -    assume "i \<noteq> 0"
  3.2078 -    with i0 have i0: "i < 0" by simp
  3.2079 -    hence "length (int_to_bv i) =
  3.2080 -        length (norm_signed (\<one> # bv_not (norm_unsigned (nat_to_bv (nat (- i) - 1)))))"
  3.2081 -      by (simp add: int_to_bv_def nat_diff_distrib)
  3.2082 -    also from norm_unsigned_result [of "nat_to_bv (nat (- i) - 1)"]
  3.2083 -    have "... = Suc (length_nat (nat (- i) - 1))"
  3.2084 -      apply safe
  3.2085 -      apply (simp del: norm_unsigned_nat_to_bv)
  3.2086 -      apply (drule norm_empty_bv_to_nat_zero [of "nat_to_bv (nat (-i) - Suc 0)"])
  3.2087 -      using prems
  3.2088 -      apply simp
  3.2089 -      apply (cases "- i - 1 = 0")
  3.2090 -      apply simp
  3.2091 -      apply (simp add: length_nat [symmetric])
  3.2092 -      apply (cases "norm_unsigned (nat_to_bv (nat (- i) - 1))")
  3.2093 -      apply simp
  3.2094 -      apply simp
  3.2095 -      done
  3.2096 -    finally
  3.2097 -    show ?thesis
  3.2098 -      using i0 by (simp add: length_int_def nat_diff_distrib del: int_to_bv_lt0)
  3.2099 -  qed
  3.2100 -qed
  3.2101 -
  3.2102 -lemma length_int_0 [simp]: "length_int 0 = 0"
  3.2103 -  by (simp add: length_int_def)
  3.2104 -
  3.2105 -lemma length_int_gt0: "0 < i ==> length_int i = Suc (length_nat (nat i))"
  3.2106 -  by (simp add: length_int_def)
  3.2107 -
  3.2108 -lemma length_int_lt0: "i < 0 ==> length_int i = Suc (length_nat (nat (- i) - 1))"
  3.2109 -  by (simp add: length_int_def nat_diff_distrib)
  3.2110 -
  3.2111 -lemma bv_chopI: "[| w = w1 @ w2 ; i = length w2 |] ==> bv_chop w i = (w1,w2)"
  3.2112 -  by (simp add: bv_chop_def Let_def)
  3.2113 -
  3.2114 -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"
  3.2115 -  apply (simp add: bv_slice_def)
  3.2116 -  apply (subst bv_chopI [of "w1 @ w2 @ w3" w1 "w2 @ w3"])
  3.2117 -  apply simp
  3.2118 -  apply simp
  3.2119 -  apply simp
  3.2120 -  apply (subst bv_chopI [of "w2 @ w3" w2 w3],simp_all)
  3.2121 -  done
  3.2122 -
  3.2123 -lemma bv_slice_bv_slice:
  3.2124 -  assumes ki: "k \<le> i"
  3.2125 -  and     ij: "i \<le> j"
  3.2126 -  and     jl: "j \<le> l"
  3.2127 -  and     lw: "l < length w"
  3.2128 -  shows       "bv_slice w (j,i) = bv_slice (bv_slice w (l,k)) (j-k,i-k)"
  3.2129 -proof -
  3.2130 -  def w1  == "fst (bv_chop w (Suc l))"
  3.2131 -  and w2  == "fst (bv_chop (snd (bv_chop w (Suc l))) (Suc j))"
  3.2132 -  and w3  == "fst (bv_chop (snd (bv_chop (snd (bv_chop w (Suc l))) (Suc j))) i)"
  3.2133 -  and w4  == "fst (bv_chop (snd (bv_chop (snd (bv_chop (snd (bv_chop w (Suc l))) (Suc j))) i)) k)"
  3.2134 -  and w5  == "snd (bv_chop (snd (bv_chop (snd (bv_chop (snd (bv_chop w (Suc l))) (Suc j))) i)) k)"
  3.2135 -  note w_defs = this
  3.2136 -
  3.2137 -  have w_def: "w = w1 @ w2 @ w3 @ w4 @ w5"
  3.2138 -    by (simp add: w_defs append_bv_chop_id)
  3.2139 -
  3.2140 -  from ki ij jl lw
  3.2141 -  show ?thesis
  3.2142 -    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"])
  3.2143 -    apply simp_all
  3.2144 -    apply (rule w_def)
  3.2145 -    apply (simp add: w_defs)
  3.2146 -    apply (simp add: w_defs)
  3.2147 -    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])
  3.2148 -    apply simp_all
  3.2149 -    apply (rule w_def)
  3.2150 -    apply (simp add: w_defs)
  3.2151 -    apply (simp add: w_defs)
  3.2152 -    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])
  3.2153 -    apply simp_all
  3.2154 -    apply (simp_all add: w_defs)
  3.2155 -    done
  3.2156 -qed
  3.2157 -
  3.2158 -lemma bv_to_nat_extend [simp]: "bv_to_nat (bv_extend n \<zero> w) = bv_to_nat w"
  3.2159 -  apply (simp add: bv_extend_def)
  3.2160 -  apply (subst bv_to_nat_dist_append)
  3.2161 -  apply simp
  3.2162 -  apply (induct ("n - length w"))
  3.2163 -   apply simp_all
  3.2164 -  done
  3.2165 -
  3.2166 -lemma bv_msb_extend_same [simp]: "bv_msb w = b ==> bv_msb (bv_extend n b w) = b"
  3.2167 -  apply (simp add: bv_extend_def)
  3.2168 -  apply (cases "n - length w")
  3.2169 -   apply simp_all
  3.2170 -  done
  3.2171 -
  3.2172 -lemma bv_to_int_extend [simp]:
  3.2173 -  assumes a: "bv_msb w = b"
  3.2174 -  shows      "bv_to_int (bv_extend n b w) = bv_to_int w"
  3.2175 -proof (cases "bv_msb w")
  3.2176 -  assume [simp]: "bv_msb w = \<zero>"
  3.2177 -  with a have [simp]: "b = \<zero>" by simp
  3.2178 -  show ?thesis by (simp add: bv_to_int_def)
  3.2179 -next
  3.2180 -  assume [simp]: "bv_msb w = \<one>"
  3.2181 -  with a have [simp]: "b = \<one>" by simp
  3.2182 -  show ?thesis
  3.2183 -    apply (simp add: bv_to_int_def)
  3.2184 -    apply (simp add: bv_extend_def)
  3.2185 -    apply (induct ("n - length w"), simp_all)
  3.2186 -    done
  3.2187 -qed
  3.2188 -
  3.2189 -lemma length_nat_mono [simp]: "x \<le> y ==> length_nat x \<le> length_nat y"
  3.2190 -proof (rule ccontr)
  3.2191 -  assume xy: "x \<le> y"
  3.2192 -  assume "~ length_nat x \<le> length_nat y"
  3.2193 -  hence lxly: "length_nat y < length_nat x"
  3.2194 -    by simp
  3.2195 -  hence "length_nat y < (LEAST n. x < 2 ^ n)"
  3.2196 -    by (simp add: length_nat_def)
  3.2197 -  hence "~ x < 2 ^ length_nat y"
  3.2198 -    by (rule not_less_Least)
  3.2199 -  hence xx: "2 ^ length_nat y \<le> x"
  3.2200 -    by simp
  3.2201 -  have yy: "y < 2 ^ length_nat y"
  3.2202 -    apply (simp add: length_nat_def)
  3.2203 -    apply (rule LeastI)
  3.2204 -    apply (subgoal_tac "y < 2 ^ y",assumption)
  3.2205 -    apply (cases "0 \<le> y")
  3.2206 -    apply (induct y,simp_all)
  3.2207 -    done
  3.2208 -  with xx have "y < x" by simp
  3.2209 -  with xy show False by simp
  3.2210 -qed
  3.2211 -
  3.2212 -lemma length_nat_mono_int [simp]: "x \<le> y ==> length_nat x \<le> length_nat y"
  3.2213 -  by (rule length_nat_mono) arith
  3.2214 -
  3.2215 -lemma length_nat_pos [simp,intro!]: "0 < x ==> 0 < length_nat x"
  3.2216 -  by (simp add: length_nat_non0)
  3.2217 -
  3.2218 -lemma length_int_mono_gt0: "[| 0 \<le> x ; x \<le> y |] ==> length_int x \<le> length_int y"
  3.2219 -  by (cases "x = 0") (simp_all add: length_int_gt0 nat_le_eq_zle)
  3.2220 -
  3.2221 -lemma length_int_mono_lt0: "[| x \<le> y ; y \<le> 0 |] ==> length_int y \<le> length_int x"
  3.2222 -  by (cases "y = 0") (simp_all add: length_int_lt0)
  3.2223 -
  3.2224 -lemmas [simp] = length_nat_non0
  3.2225 -
  3.2226 -lemma "nat_to_bv (number_of Int.Pls) = []"
  3.2227 -  by simp
  3.2228 -
  3.2229 -primrec fast_bv_to_nat_helper :: "[bit list, int] => int" where
  3.2230 -    fast_bv_to_nat_Nil: "fast_bv_to_nat_helper [] k = k"
  3.2231 -  | fast_bv_to_nat_Cons: "fast_bv_to_nat_helper (b#bs) k =
  3.2232 -      fast_bv_to_nat_helper bs ((bit_case Int.Bit0 Int.Bit1 b) k)"
  3.2233 -
  3.2234 -declare fast_bv_to_nat_helper.simps [code del]
  3.2235 -
  3.2236 -lemma fast_bv_to_nat_Cons0: "fast_bv_to_nat_helper (\<zero>#bs) bin =
  3.2237 -    fast_bv_to_nat_helper bs (Int.Bit0 bin)"
  3.2238 -  by simp
  3.2239 -
  3.2240 -lemma fast_bv_to_nat_Cons1: "fast_bv_to_nat_helper (\<one>#bs) bin =
  3.2241 -    fast_bv_to_nat_helper bs (Int.Bit1 bin)"
  3.2242 -  by simp
  3.2243 -
  3.2244 -lemma fast_bv_to_nat_def:
  3.2245 -  "bv_to_nat bs == number_of (fast_bv_to_nat_helper bs Int.Pls)"
  3.2246 -proof (simp add: bv_to_nat_def)
  3.2247 -  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)"
  3.2248 -    apply (induct bs,simp)
  3.2249 -    apply (case_tac a,simp_all)
  3.2250 -    done
  3.2251 -  thus "foldl (\<lambda>bn b. 2 * bn + bitval b) 0 bs \<equiv> number_of (fast_bv_to_nat_helper bs Int.Pls)"
  3.2252 -    by (simp del: nat_numeral_0_eq_0 add: nat_numeral_0_eq_0 [symmetric])
  3.2253 -qed
  3.2254 -
  3.2255 -declare fast_bv_to_nat_Cons [simp del]
  3.2256 -declare fast_bv_to_nat_Cons0 [simp]
  3.2257 -declare fast_bv_to_nat_Cons1 [simp]
  3.2258 -
  3.2259 -setup {*
  3.2260 -(*comments containing lcp are the removal of fast_bv_of_nat*)
  3.2261 -let
  3.2262 -  fun is_const_bool (Const("True",_)) = true
  3.2263 -    | is_const_bool (Const("False",_)) = true
  3.2264 -    | is_const_bool _ = false
  3.2265 -  fun is_const_bit (Const("Word.bit.Zero",_)) = true
  3.2266 -    | is_const_bit (Const("Word.bit.One",_)) = true
  3.2267 -    | is_const_bit _ = false
  3.2268 -  fun num_is_usable (Const(@{const_name Int.Pls},_)) = true
  3.2269 -    | num_is_usable (Const(@{const_name Int.Min},_)) = false
  3.2270 -    | num_is_usable (Const(@{const_name Int.Bit0},_) $ w) =
  3.2271 -        num_is_usable w
  3.2272 -    | num_is_usable (Const(@{const_name Int.Bit1},_) $ w) =
  3.2273 -        num_is_usable w
  3.2274 -    | num_is_usable _ = false
  3.2275 -  fun vec_is_usable (Const("List.list.Nil",_)) = true
  3.2276 -    | vec_is_usable (Const("List.list.Cons",_) $ b $ bs) =
  3.2277 -        vec_is_usable bs andalso is_const_bit b
  3.2278 -    | vec_is_usable _ = false
  3.2279 -  (*lcp** val fast1_th = PureThy.get_thm thy "Word.fast_nat_to_bv_def"*)
  3.2280 -  val fast2_th = @{thm "Word.fast_bv_to_nat_def"};
  3.2281 -  (*lcp** fun f sg thms (Const("Word.nat_to_bv",_) $ (Const(@{const_name Int.number_of},_) $ t)) =
  3.2282 -    if num_is_usable t
  3.2283 -      then SOME (Drule.cterm_instantiate [(cterm_of sg (Var (("w", 0), @{typ int})), cterm_of sg t)] fast1_th)
  3.2284 -      else NONE
  3.2285 -    | f _ _ _ = NONE *)
  3.2286 -  fun g sg thms (Const("Word.bv_to_nat",_) $ (t as (Const("List.list.Cons",_) $ _ $ _))) =
  3.2287 -        if vec_is_usable t then
  3.2288 -          SOME (Drule.cterm_instantiate [(cterm_of sg (Var(("bs",0),Type("List.list",[Type("Word.bit",[])]))),cterm_of sg t)] fast2_th)
  3.2289 -        else NONE
  3.2290 -    | g _ _ _ = NONE
  3.2291 -  (*lcp** val simproc1 = Simplifier.simproc thy "nat_to_bv" ["Word.nat_to_bv (number_of w)"] f *)
  3.2292 -  val simproc2 = Simplifier.simproc @{theory} "bv_to_nat" ["Word.bv_to_nat (x # xs)"] g
  3.2293 -in
  3.2294 -  Simplifier.map_simpset (fn ss => ss addsimprocs [(*lcp*simproc1,*)simproc2])
  3.2295 -end*}
  3.2296 -
  3.2297 -declare bv_to_nat1 [simp del]
  3.2298 -declare bv_to_nat_helper [simp del]
  3.2299 -
  3.2300 -definition
  3.2301 -  bv_mapzip :: "[bit => bit => bit,bit list, bit list] => bit list" where
  3.2302 -  "bv_mapzip f w1 w2 =
  3.2303 -    (let g = bv_extend (max (length w1) (length w2)) \<zero>
  3.2304 -     in map (split f) (zip (g w1) (g w2)))"
  3.2305 -
  3.2306 -lemma bv_length_bv_mapzip [simp]:
  3.2307 -    "length (bv_mapzip f w1 w2) = max (length w1) (length w2)"
  3.2308 -  by (simp add: bv_mapzip_def Let_def split: split_max)
  3.2309 -
  3.2310 -lemma bv_mapzip_Nil [simp]: "bv_mapzip f [] [] = []"
  3.2311 -  by (simp add: bv_mapzip_def Let_def)
  3.2312 -
  3.2313 -lemma bv_mapzip_Cons [simp]: "length w1 = length w2 ==>
  3.2314 -    bv_mapzip f (x#w1) (y#w2) = f x y # bv_mapzip f w1 w2"
  3.2315 -  by (simp add: bv_mapzip_def Let_def)
  3.2316 -
  3.2317 -end
     4.1 --- a/src/HOL/ex/Codegenerator_Candidates.thy	Sun May 16 00:02:11 2010 +0200
     4.2 +++ b/src/HOL/ex/Codegenerator_Candidates.thy	Mon May 17 10:58:31 2010 +0200
     4.3 @@ -23,7 +23,6 @@
     4.4    RBT
     4.5    SetsAndFunctions
     4.6    While_Combinator
     4.7 -  Word
     4.8  begin
     4.9  
    4.10  inductive sublist :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool" where
     5.1 --- a/src/HOL/ex/ROOT.ML	Sun May 16 00:02:11 2010 +0200
     5.2 +++ b/src/HOL/ex/ROOT.ML	Mon May 17 10:58:31 2010 +0200
     5.3 @@ -7,7 +7,6 @@
     5.4    "State_Monad",
     5.5    "Efficient_Nat_examples",
     5.6    "FuncSet",
     5.7 -  "Word",
     5.8    "Eval_Examples",
     5.9    "Codegenerator_Test",
    5.10    "Codegenerator_Pretty_Test",
    5.11 @@ -46,7 +45,6 @@
    5.12    "Unification",
    5.13    "Primrec",
    5.14    "Tarski",
    5.15 -  "Adder",
    5.16    "Classical",
    5.17    "set",
    5.18    "Meson_Test",