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",