author | wenzelm |

Wed Jun 13 18:30:16 2007 +0200 (2007-06-13) | |

changeset 23375 | 45cd7db985b3 |

parent 23374 | a2f492c599e0 |

child 23376 | 53317a1ec8b2 |

tuned proofs: avoid implicit prems;

major cleanup of proofs/document;

major cleanup of proofs/document;

1.1 --- a/src/HOL/Library/Word.thy Wed Jun 13 18:30:15 2007 +0200 1.2 +++ b/src/HOL/Library/Word.thy Wed Jun 13 18:30:16 2007 +0200 1.3 @@ -20,31 +20,28 @@ 1.4 shows "max (f x) (f y) \<le> f (max x y)" 1.5 proof - 1.6 from mf and le_maxI1 [of x y] 1.7 - have fx: "f x \<le> f (max x y)" 1.8 - by (rule monoD) 1.9 + have fx: "f x \<le> f (max x y)" by (rule monoD) 1.10 from mf and le_maxI2 [of y x] 1.11 - have fy: "f y \<le> f (max x y)" 1.12 - by (rule monoD) 1.13 + have fy: "f y \<le> f (max x y)" by (rule monoD) 1.14 from fx and fy 1.15 - show "max (f x) (f y) \<le> f (max x y)" 1.16 - by auto 1.17 + show "max (f x) (f y) \<le> f (max x y)" by auto 1.18 qed 1.19 1.20 declare zero_le_power [intro] 1.21 - and zero_less_power [intro] 1.22 + and zero_less_power [intro] 1.23 1.24 lemma int_nat_two_exp: "2 ^ k = int (2 ^ k)" 1.25 by (simp add: zpower_int [symmetric]) 1.26 1.27 + 1.28 subsection {* Bits *} 1.29 1.30 -datatype bit 1.31 - = Zero ("\<zero>") 1.32 +datatype bit = 1.33 + Zero ("\<zero>") 1.34 | One ("\<one>") 1.35 1.36 consts 1.37 bitval :: "bit => nat" 1.38 - 1.39 primrec 1.40 "bitval \<zero> = 0" 1.41 "bitval \<one> = 1" 1.42 @@ -84,16 +81,17 @@ 1.43 bitxor_one: "(\<one> bitxor y) = (bitnot y)" 1.44 1.45 lemma bitnot_bitnot [simp]: "(bitnot (bitnot b)) = b" 1.46 - by (cases b,simp_all) 1.47 + by (cases b) simp_all 1.48 1.49 lemma bitand_cancel [simp]: "(b bitand b) = b" 1.50 - by (cases b,simp_all) 1.51 + by (cases b) simp_all 1.52 1.53 lemma bitor_cancel [simp]: "(b bitor b) = b" 1.54 - by (cases b,simp_all) 1.55 + by (cases b) simp_all 1.56 1.57 lemma bitxor_cancel [simp]: "(b bitxor b) = \<zero>" 1.58 - by (cases b,simp_all) 1.59 + by (cases b) simp_all 1.60 + 1.61 1.62 subsection {* Bit Vectors *} 1.63 1.64 @@ -107,24 +105,19 @@ 1.65 shows "P w" 1.66 proof (cases w) 1.67 assume "w = []" 1.68 - thus ?thesis 1.69 - by (rule empty) 1.70 + thus ?thesis by (rule empty) 1.71 next 1.72 fix b bs 1.73 assume [simp]: "w = b # bs" 1.74 show "P w" 1.75 proof (cases b) 1.76 assume "b = \<zero>" 1.77 - hence "w = \<zero> # bs" 1.78 - by simp 1.79 - thus ?thesis 1.80 - by (rule zero) 1.81 + hence "w = \<zero> # bs" by simp 1.82 + thus ?thesis by (rule zero) 1.83 next 1.84 assume "b = \<one>" 1.85 - hence "w = \<one> # bs" 1.86 - by simp 1.87 - thus ?thesis 1.88 - by (rule one) 1.89 + hence "w = \<one> # bs" by simp 1.90 + thus ?thesis by (rule one) 1.91 qed 1.92 qed 1.93 1.94 @@ -133,11 +126,11 @@ 1.95 and zero: "!!bs. P bs ==> P (\<zero>#bs)" 1.96 and one: "!!bs. P bs ==> P (\<one>#bs)" 1.97 shows "P w" 1.98 -proof (induct w,simp_all add: empty) 1.99 +proof (induct w, simp_all add: empty) 1.100 fix b bs 1.101 - assume [intro!]: "P bs" 1.102 - show "P (b#bs)" 1.103 - by (cases b,auto intro!: zero one) 1.104 + assume "P bs" 1.105 + then show "P (b#bs)" 1.106 + by (cases b) (auto intro!: zero one) 1.107 qed 1.108 1.109 definition 1.110 @@ -162,7 +155,7 @@ 1.111 by (simp add: bv_not_def) 1.112 1.113 lemma bv_not_bv_not [simp]: "bv_not (bv_not w) = w" 1.114 - by (rule bit_list_induct [of _ w],simp_all) 1.115 + by (rule bit_list_induct [of _ w]) simp_all 1.116 1.117 lemma bv_msb_Nil [simp]: "bv_msb [] = \<zero>" 1.118 by (simp add: bv_msb_def) 1.119 @@ -171,13 +164,13 @@ 1.120 by (simp add: bv_msb_def) 1.121 1.122 lemma bv_msb_bv_not [simp]: "0 < length w ==> bv_msb (bv_not w) = (bitnot (bv_msb w))" 1.123 - by (cases w,simp_all) 1.124 + by (cases w) simp_all 1.125 1.126 lemma bv_msb_one_length [simp,intro]: "bv_msb w = \<one> ==> 0 < length w" 1.127 - by (cases w,simp_all) 1.128 + by (cases w) simp_all 1.129 1.130 lemma length_bv_not [simp]: "length (bv_not w) = length w" 1.131 - by (induct w,simp_all) 1.132 + by (induct w) simp_all 1.133 1.134 definition 1.135 bv_to_nat :: "bit list => nat" where 1.136 @@ -191,7 +184,8 @@ 1.137 let ?bv_to_nat' = "foldl (\<lambda>bn b. 2 * bn + bitval b)" 1.138 have helper: "\<And>base. ?bv_to_nat' base bs = base * 2 ^ length bs + ?bv_to_nat' 0 bs" 1.139 proof (induct bs) 1.140 - case Nil show ?case by simp 1.141 + case Nil 1.142 + show ?case by simp 1.143 next 1.144 case (Cons x xs base) 1.145 show ?case 1.146 @@ -212,26 +206,19 @@ 1.147 by simp 1.148 1.149 lemma bv_to_nat_upper_range: "bv_to_nat w < 2 ^ length w" 1.150 -proof (induct w,simp_all) 1.151 +proof (induct w, simp_all) 1.152 fix b bs 1.153 assume "bv_to_nat bs < 2 ^ length bs" 1.154 show "bitval b * 2 ^ length bs + bv_to_nat bs < 2 * 2 ^ length bs" 1.155 - proof (cases b,simp_all) 1.156 - have "bv_to_nat bs < 2 ^ length bs" 1.157 - . 1.158 - also have "... < 2 * 2 ^ length bs" 1.159 - by auto 1.160 - finally show "bv_to_nat bs < 2 * 2 ^ length bs" 1.161 - by simp 1.162 + proof (cases b, simp_all) 1.163 + have "bv_to_nat bs < 2 ^ length bs" by fact 1.164 + also have "... < 2 * 2 ^ length bs" by auto 1.165 + finally show "bv_to_nat bs < 2 * 2 ^ length bs" by simp 1.166 next 1.167 - have "bv_to_nat bs < 2 ^ length bs" 1.168 - . 1.169 - hence "2 ^ length bs + bv_to_nat bs < 2 ^ length bs + 2 ^ length bs" 1.170 - by arith 1.171 - also have "... = 2 * (2 ^ length bs)" 1.172 - by simp 1.173 - finally show "bv_to_nat bs < 2 ^ length bs" 1.174 - by simp 1.175 + have "bv_to_nat bs < 2 ^ length bs" by fact 1.176 + hence "2 ^ length bs + bv_to_nat bs < 2 ^ length bs + 2 ^ length bs" by arith 1.177 + also have "... = 2 * (2 ^ length bs)" by simp 1.178 + finally show "bv_to_nat bs < 2 ^ length bs" by simp 1.179 qed 1.180 qed 1.181 1.182 @@ -250,20 +237,18 @@ 1.183 have "bv_extend n b w = replicate (n - length w) b @ w" 1.184 by (simp add: bv_extend_def) 1.185 also have "... = replicate (n - Suc (length w) + 1) b @ w" 1.186 - by (subst s,rule) 1.187 + by (subst s) rule 1.188 also have "... = (replicate (n - Suc (length w)) b @ replicate 1 b) @ w" 1.189 - by (subst replicate_add,rule) 1.190 + by (subst replicate_add) rule 1.191 also have "... = replicate (n - Suc (length w)) b @ b # w" 1.192 by simp 1.193 also have "... = bv_extend n b (b#w)" 1.194 by (simp add: bv_extend_def) 1.195 - finally show "bv_extend n b w = bv_extend n b (b#w)" 1.196 - . 1.197 + finally show "bv_extend n b w = bv_extend n b (b#w)" . 1.198 qed 1.199 1.200 consts 1.201 rem_initial :: "bit => bit list => bit list" 1.202 - 1.203 primrec 1.204 "rem_initial b [] = []" 1.205 "rem_initial b (x#xs) = (if b = x then rem_initial b xs else x#xs)" 1.206 @@ -276,7 +261,7 @@ 1.207 shows "rem_initial b w = w" 1.208 proof - 1.209 have "length (rem_initial b w) = length w --> rem_initial b w = w" 1.210 - proof (induct w,simp_all,clarify) 1.211 + proof (induct w, simp_all, clarify) 1.212 fix xs 1.213 assume "length (rem_initial b xs) = length xs --> rem_initial b xs = xs" 1.214 assume f: "length (rem_initial b xs) = Suc (length xs)" 1.215 @@ -284,50 +269,42 @@ 1.216 show "rem_initial b xs = b#xs" 1.217 by auto 1.218 qed 1.219 - thus ?thesis 1.220 - .. 1.221 + from this and p show ?thesis .. 1.222 qed 1.223 1.224 lemma bv_extend_rem_initial: "bv_extend (length w) b (rem_initial b w) = w" 1.225 -proof (induct w,simp_all,safe) 1.226 +proof (induct w, simp_all, safe) 1.227 fix xs 1.228 assume ind: "bv_extend (length xs) b (rem_initial b xs) = xs" 1.229 from rem_initial_length [of b xs] 1.230 - have [simp]: "Suc (length xs) - length (rem_initial b xs) = 1 + (length xs - length (rem_initial b xs))" 1.231 + have [simp]: "Suc (length xs) - length (rem_initial b xs) = 1.232 + 1 + (length xs - length (rem_initial b xs))" 1.233 by arith 1.234 - have "bv_extend (Suc (length xs)) b (rem_initial b xs) = replicate (Suc (length xs) - length (rem_initial b xs)) b @ (rem_initial b xs)" 1.235 + have "bv_extend (Suc (length xs)) b (rem_initial b xs) = 1.236 + replicate (Suc (length xs) - length (rem_initial b xs)) b @ (rem_initial b xs)" 1.237 by (simp add: bv_extend_def) 1.238 - also have "... = replicate (1 + (length xs - length (rem_initial b xs))) b @ rem_initial b xs" 1.239 + also have "... = 1.240 + replicate (1 + (length xs - length (rem_initial b xs))) b @ rem_initial b xs" 1.241 by simp 1.242 - also have "... = (replicate 1 b @ replicate (length xs - length (rem_initial b xs)) b) @ rem_initial b xs" 1.243 - by (subst replicate_add,rule refl) 1.244 + also have "... = 1.245 + (replicate 1 b @ replicate (length xs - length (rem_initial b xs)) b) @ rem_initial b xs" 1.246 + by (subst replicate_add) (rule refl) 1.247 also have "... = b # bv_extend (length xs) b (rem_initial b xs)" 1.248 by (auto simp add: bv_extend_def [symmetric]) 1.249 also have "... = b # xs" 1.250 by (simp add: ind) 1.251 - finally show "bv_extend (Suc (length xs)) b (rem_initial b xs) = b # xs" 1.252 - . 1.253 + finally show "bv_extend (Suc (length xs)) b (rem_initial b xs) = b # xs" . 1.254 qed 1.255 1.256 lemma rem_initial_append1: 1.257 assumes "rem_initial b xs ~= []" 1.258 shows "rem_initial b (xs @ ys) = rem_initial b xs @ ys" 1.259 -proof - 1.260 - have "rem_initial b xs ~= [] --> rem_initial b (xs @ ys) = rem_initial b xs @ ys" (is "?P xs ys") 1.261 - by (induct xs,auto) 1.262 - thus ?thesis 1.263 - .. 1.264 -qed 1.265 + using assms by (induct xs) auto 1.266 1.267 lemma rem_initial_append2: 1.268 assumes "rem_initial b xs = []" 1.269 shows "rem_initial b (xs @ ys) = rem_initial b ys" 1.270 -proof - 1.271 - have "rem_initial b xs = [] --> rem_initial b (xs @ ys) = rem_initial b ys" (is "?P xs ys") 1.272 - by (induct xs,auto) 1.273 - thus ?thesis 1.274 - .. 1.275 -qed 1.276 + using assms by (induct xs) auto 1.277 1.278 definition 1.279 norm_unsigned :: "bit list => bit list" where 1.280 @@ -347,7 +324,6 @@ 1.281 1.282 consts 1.283 nat_to_bv_helper :: "nat => bit list => bit list" 1.284 - 1.285 recdef nat_to_bv_helper "measure (\<lambda>n. n)" 1.286 "nat_to_bv_helper n = (%bs. (if n = 0 then bs 1.287 else nat_to_bv_helper (n div 2) ((if n mod 2 = 0 then \<zero> else \<one>)#bs)))" 1.288 @@ -367,17 +343,12 @@ 1.289 shows "R" 1.290 proof (cases "n = 0") 1.291 assume "n = 0" 1.292 - thus R 1.293 - by (rule zero) 1.294 + thus R by (rule zero) 1.295 next 1.296 assume "n ~= 0" 1.297 - hence nn0: "0 < n" 1.298 - by simp 1.299 - hence "n div 2 < n" 1.300 - by arith 1.301 - from this and nn0 1.302 - show R 1.303 - by (rule div) 1.304 + hence "0 < n" by simp 1.305 + hence "n div 2 < n" by arith 1.306 + from this and `0 < n` show R by (rule div) 1.307 qed 1.308 1.309 lemma int_wf_ge_induct: 1.310 @@ -387,7 +358,7 @@ 1.311 fix x 1.312 assume ih: "(\<And>y\<Colon>int. (y, x) \<in> int_ge_less_than k \<Longrightarrow> P y)" 1.313 thus "P x" 1.314 - by (rule ind, simp add: int_ge_less_than_def) 1.315 + by (rule ind) (simp add: int_ge_less_than_def) 1.316 qed 1.317 1.318 lemma unfold_nat_to_bv_helper: 1.319 @@ -438,8 +409,7 @@ 1.320 qed 1.321 qed 1.322 qed 1.323 - thus ?thesis 1.324 - .. 1.325 + thus ?thesis .. 1.326 qed 1.327 1.328 lemma nat_to_bv_non0 [simp]: "0 < n ==> nat_to_bv n = nat_to_bv (n div 2) @ [if n mod 2 = 0 then \<zero> else \<one>]" 1.329 @@ -478,8 +448,7 @@ 1.330 qed 1.331 qed 1.332 qed 1.333 - thus ?thesis 1.334 - .. 1.335 + thus ?thesis .. 1.336 qed 1.337 1.338 lemma bv_nat_bv [simp]: "bv_to_nat (nat_to_bv n) = n" 1.339 @@ -488,17 +457,14 @@ 1.340 assume ind: "!!j. j < n \<Longrightarrow> bv_to_nat (nat_to_bv j) = j" 1.341 show "bv_to_nat (nat_to_bv n) = n" 1.342 proof (rule n_div_2_cases [of n]) 1.343 - assume [simp]: "n = 0" 1.344 - show ?thesis 1.345 - by simp 1.346 + assume "n = 0" 1.347 + then show ?thesis by simp 1.348 next 1.349 assume nn: "n div 2 < n" 1.350 assume n0: "0 < n" 1.351 from ind and nn 1.352 - have ind': "bv_to_nat (nat_to_bv (n div 2)) = n div 2" 1.353 - by blast 1.354 - from n0 have n0': "n \<noteq> 0" 1.355 - by simp 1.356 + have ind': "bv_to_nat (nat_to_bv (n div 2)) = n div 2" by blast 1.357 + from n0 have n0': "n \<noteq> 0" by simp 1.358 show ?thesis 1.359 apply (subst nat_to_bv_def) 1.360 apply (simp only: nat_to_bv_helper.simps [of n]) 1.361 @@ -523,13 +489,13 @@ 1.362 qed 1.363 1.364 lemma bv_to_nat_type [simp]: "bv_to_nat (norm_unsigned w) = bv_to_nat w" 1.365 - by (rule bit_list_induct,simp_all) 1.366 + by (rule bit_list_induct) simp_all 1.367 1.368 lemma length_norm_unsigned_le [simp]: "length (norm_unsigned w) \<le> length w" 1.369 - by (rule bit_list_induct,simp_all) 1.370 + by (rule bit_list_induct) simp_all 1.371 1.372 lemma bv_to_nat_rew_msb: "bv_msb w = \<one> ==> bv_to_nat w = 2 ^ (length w - 1) + bv_to_nat (tl w)" 1.373 - by (rule bit_list_cases [of w],simp_all) 1.374 + by (rule bit_list_cases [of w]) simp_all 1.375 1.376 lemma norm_unsigned_result: "norm_unsigned xs = [] \<or> bv_msb (norm_unsigned xs) = \<one>" 1.377 proof (rule length_induct [of _ xs]) 1.378 @@ -540,10 +506,8 @@ 1.379 fix bs 1.380 assume [simp]: "xs = \<zero>#bs" 1.381 from ind 1.382 - have "length bs < length xs --> norm_unsigned bs = [] \<or> bv_msb (norm_unsigned bs) = \<one>" 1.383 - .. 1.384 - thus "norm_unsigned bs = [] \<or> bv_msb (norm_unsigned bs) = \<one>" 1.385 - by simp 1.386 + have "length bs < length xs --> norm_unsigned bs = [] \<or> bv_msb (norm_unsigned bs) = \<one>" .. 1.387 + thus "norm_unsigned bs = [] \<or> bv_msb (norm_unsigned bs) = \<one>" by simp 1.388 qed 1.389 qed 1.390 1.391 @@ -551,26 +515,22 @@ 1.392 assumes nw: "norm_unsigned w = []" 1.393 shows "bv_to_nat w = 0" 1.394 proof - 1.395 - have "bv_to_nat w = bv_to_nat (norm_unsigned w)" 1.396 - by simp 1.397 - also have "... = bv_to_nat []" 1.398 - by (subst nw,rule) 1.399 - also have "... = 0" 1.400 - by simp 1.401 + have "bv_to_nat w = bv_to_nat (norm_unsigned w)" by simp 1.402 + also have "... = bv_to_nat []" by (subst nw) (rule refl) 1.403 + also have "... = 0" by simp 1.404 finally show ?thesis . 1.405 qed 1.406 1.407 lemma bv_to_nat_lower_limit: 1.408 assumes w0: "0 < bv_to_nat w" 1.409 - shows "2 ^ (length (norm_unsigned w) - 1) \<le> bv_to_nat w" 1.410 + shows "2 ^ (length (norm_unsigned w) - 1) \<le> bv_to_nat w" 1.411 proof - 1.412 from w0 and norm_unsigned_result [of w] 1.413 have msbw: "bv_msb (norm_unsigned w) = \<one>" 1.414 by (auto simp add: norm_empty_bv_to_nat_zero) 1.415 have "2 ^ (length (norm_unsigned w) - 1) \<le> bv_to_nat (norm_unsigned w)" 1.416 by (subst bv_to_nat_rew_msb [OF msbw],simp) 1.417 - thus ?thesis 1.418 - by simp 1.419 + thus ?thesis by simp 1.420 qed 1.421 1.422 lemmas [simp del] = nat_to_bv_non0 1.423 @@ -584,25 +544,21 @@ 1.424 lemma bv_extend_norm_unsigned: "bv_extend (length w) \<zero> (norm_unsigned w) = w" 1.425 by (simp add: norm_unsigned_def,rule bv_extend_rem_initial) 1.426 1.427 -lemma norm_unsigned_append1 [simp]: "norm_unsigned xs \<noteq> [] ==> norm_unsigned (xs @ ys) = norm_unsigned xs @ ys" 1.428 +lemma norm_unsigned_append1 [simp]: 1.429 + "norm_unsigned xs \<noteq> [] ==> norm_unsigned (xs @ ys) = norm_unsigned xs @ ys" 1.430 by (simp add: norm_unsigned_def,rule rem_initial_append1) 1.431 1.432 -lemma norm_unsigned_append2 [simp]: "norm_unsigned xs = [] ==> norm_unsigned (xs @ ys) = norm_unsigned ys" 1.433 +lemma norm_unsigned_append2 [simp]: 1.434 + "norm_unsigned xs = [] ==> norm_unsigned (xs @ ys) = norm_unsigned ys" 1.435 by (simp add: norm_unsigned_def,rule rem_initial_append2) 1.436 1.437 -lemma bv_to_nat_zero_imp_empty [rule_format]: 1.438 - "bv_to_nat w = 0 \<longrightarrow> norm_unsigned w = []" 1.439 - by (rule bit_list_induct [of _ w],simp_all) 1.440 +lemma bv_to_nat_zero_imp_empty: 1.441 + "bv_to_nat w = 0 \<Longrightarrow> norm_unsigned w = []" 1.442 + by (atomize (full), induct w rule: bit_list_induct) simp_all 1.443 1.444 lemma bv_to_nat_nzero_imp_nempty: 1.445 - assumes "bv_to_nat w \<noteq> 0" 1.446 - shows "norm_unsigned w \<noteq> []" 1.447 -proof - 1.448 - have "bv_to_nat w \<noteq> 0 --> norm_unsigned w \<noteq> []" 1.449 - by (rule bit_list_induct [of _ w],simp_all) 1.450 - thus ?thesis 1.451 - .. 1.452 -qed 1.453 + "bv_to_nat w \<noteq> 0 \<Longrightarrow> norm_unsigned w \<noteq> []" 1.454 + by (induct w rule: bit_list_induct) simp_all 1.455 1.456 lemma nat_helper1: 1.457 assumes ass: "nat_to_bv (bv_to_nat w) = norm_unsigned w" 1.458 @@ -622,22 +578,21 @@ 1.459 also have "... = 1" 1.460 by (subst mod_add1_eq) simp 1.461 finally have eq1: "?lhs = 1" . 1.462 - have "?rhs = 0" 1.463 - by simp 1.464 + have "?rhs = 0" by simp 1.465 with orig and eq1 1.466 show "nat_to_bv (Suc (2 * bv_to_nat w) div 2) @ [\<zero>] = norm_unsigned (w @ [\<one>])" 1.467 by simp 1.468 next 1.469 - have "nat_to_bv (Suc (2 * bv_to_nat w) div 2) @ [\<one>] = nat_to_bv ((1 + 2 * bv_to_nat w) div 2) @ [\<one>]" 1.470 + have "nat_to_bv (Suc (2 * bv_to_nat w) div 2) @ [\<one>] = 1.471 + nat_to_bv ((1 + 2 * bv_to_nat w) div 2) @ [\<one>]" 1.472 by (simp add: add_commute) 1.473 also have "... = nat_to_bv (bv_to_nat w) @ [\<one>]" 1.474 - by (subst div_add1_eq,simp) 1.475 + by (subst div_add1_eq) simp 1.476 also have "... = norm_unsigned w @ [\<one>]" 1.477 - by (subst ass,rule refl) 1.478 + by (subst ass) (rule refl) 1.479 also have "... = norm_unsigned (w @ [\<one>])" 1.480 - by (cases "norm_unsigned w",simp_all) 1.481 - finally show "nat_to_bv (Suc (2 * bv_to_nat w) div 2) @ [\<one>] = norm_unsigned (w @ [\<one>])" 1.482 - . 1.483 + by (cases "norm_unsigned w") simp_all 1.484 + finally show "nat_to_bv (Suc (2 * bv_to_nat w) div 2) @ [\<one>] = norm_unsigned (w @ [\<one>])" . 1.485 qed 1.486 next 1.487 assume [simp]: "x = \<zero>" 1.488 @@ -671,9 +626,8 @@ 1.489 assume ind: "\<forall>ys. length ys < length xs --> ?P ys" 1.490 show "?P xs" 1.491 proof (cases xs) 1.492 - assume [simp]: "xs = []" 1.493 - show ?thesis 1.494 - by (simp add: nat_to_bv_non0) 1.495 + assume "xs = []" 1.496 + then show ?thesis by (simp add: nat_to_bv_non0) 1.497 next 1.498 fix y ys 1.499 assume [simp]: "xs = y # ys" 1.500 @@ -703,24 +657,22 @@ 1.501 by simp 1.502 also have "... = \<one> # rev ys @ [y]" 1.503 by simp 1.504 - finally show "nat_to_bv (2 * 2 ^ length ys + (bv_to_nat (rev ys) * 2 + bitval y)) = \<one> # rev ys @ [y]" 1.505 - . 1.506 + finally show "nat_to_bv (2 * 2 ^ length ys + (bv_to_nat (rev ys) * 2 + bitval y)) = 1.507 + \<one> # rev ys @ [y]" . 1.508 qed 1.509 qed 1.510 qed 1.511 qed 1.512 - hence "nat_to_bv (2 ^ length (rev (rev xs)) + bv_to_nat (rev (rev xs))) = \<one> # rev (rev xs)" 1.513 - .. 1.514 - thus ?thesis 1.515 - by simp 1.516 + hence "nat_to_bv (2 ^ length (rev (rev xs)) + bv_to_nat (rev (rev xs))) = 1.517 + \<one> # rev (rev xs)" .. 1.518 + thus ?thesis by simp 1.519 qed 1.520 1.521 lemma nat_bv_nat [simp]: "nat_to_bv (bv_to_nat w) = norm_unsigned w" 1.522 proof (rule bit_list_induct [of _ w],simp_all) 1.523 fix xs 1.524 assume "nat_to_bv (bv_to_nat xs) = norm_unsigned xs" 1.525 - have "bv_to_nat xs = bv_to_nat (norm_unsigned xs)" 1.526 - by simp 1.527 + have "bv_to_nat xs = bv_to_nat (norm_unsigned xs)" by simp 1.528 have "bv_to_nat xs < 2 ^ length xs" 1.529 by (rule bv_to_nat_upper_range) 1.530 show "nat_to_bv (2 ^ length xs + bv_to_nat xs) = \<one> # xs" 1.531 @@ -750,9 +702,8 @@ 1.532 "norm_unsigned (nat_to_bv n) = nat_to_bv n" 1.533 proof - 1.534 have "norm_unsigned (nat_to_bv n) = nat_to_bv (bv_to_nat (norm_unsigned (nat_to_bv n)))" 1.535 - by (subst nat_bv_nat,simp) 1.536 - also have "... = nat_to_bv n" 1.537 - by simp 1.538 + by (subst nat_bv_nat) simp 1.539 + also have "... = nat_to_bv n" by simp 1.540 finally show ?thesis . 1.541 qed 1.542 1.543 @@ -769,25 +720,16 @@ 1.544 show ?thesis 1.545 proof (rule ccontr) 1.546 assume "~ length (nat_to_bv n) \<le> k" 1.547 - hence "k < length (nat_to_bv n)" 1.548 - by simp 1.549 - hence "k \<le> length (nat_to_bv n) - 1" 1.550 - by arith 1.551 - hence "(2::nat) ^ k \<le> 2 ^ (length (nat_to_bv n) - 1)" 1.552 - by simp 1.553 - also have "... = 2 ^ (length (norm_unsigned (nat_to_bv n)) - 1)" 1.554 - by simp 1.555 + hence "k < length (nat_to_bv n)" by simp 1.556 + hence "k \<le> length (nat_to_bv n) - 1" by arith 1.557 + hence "(2::nat) ^ k \<le> 2 ^ (length (nat_to_bv n) - 1)" by simp 1.558 + also have "... = 2 ^ (length (norm_unsigned (nat_to_bv n)) - 1)" by simp 1.559 also have "... \<le> bv_to_nat (nat_to_bv n)" 1.560 - by (rule bv_to_nat_lower_limit,simp add: n0) 1.561 - also have "... = n" 1.562 - by simp 1.563 + by (rule bv_to_nat_lower_limit) (simp add: n0) 1.564 + also have "... = n" by simp 1.565 finally have "2 ^ k \<le> n" . 1.566 - with n0 1.567 - have "2 ^ k - 1 < n" 1.568 - by arith 1.569 - with nk 1.570 - show False 1.571 - by simp 1.572 + with n0 have "2 ^ k - 1 < n" by arith 1.573 + with nk show False by simp 1.574 qed 1.575 qed 1.576 1.577 @@ -796,20 +738,16 @@ 1.578 shows "k < length (nat_to_bv n)" 1.579 proof (rule ccontr) 1.580 assume "~ k < length (nat_to_bv n)" 1.581 - hence lnk: "length (nat_to_bv n) \<le> k" 1.582 - by simp 1.583 - have "n = bv_to_nat (nat_to_bv n)" 1.584 - by simp 1.585 + hence lnk: "length (nat_to_bv n) \<le> k" by simp 1.586 + have "n = bv_to_nat (nat_to_bv n)" by simp 1.587 also have "... < 2 ^ length (nat_to_bv n)" 1.588 by (rule bv_to_nat_upper_range) 1.589 - also from lnk have "... \<le> 2 ^ k" 1.590 - by simp 1.591 + also from lnk have "... \<le> 2 ^ k" by simp 1.592 finally have "n < 2 ^ k" . 1.593 - with nk 1.594 - show False 1.595 - by simp 1.596 + with nk show False by simp 1.597 qed 1.598 1.599 + 1.600 subsection {* Unsigned Arithmetic Operations *} 1.601 1.602 definition 1.603 @@ -830,17 +768,15 @@ 1.604 from bv_to_nat_upper_range [of w1] and bv_to_nat_upper_range [of w2] 1.605 have "bv_to_nat w1 + bv_to_nat w2 \<le> (2 ^ length w1 - 1) + (2 ^ length w2 - 1)" 1.606 by arith 1.607 - also have "... \<le> max (2 ^ length w1 - 1) (2 ^ length w2 - 1) + max (2 ^ length w1 - 1) (2 ^ length w2 - 1)" 1.608 + also have "... \<le> 1.609 + max (2 ^ length w1 - 1) (2 ^ length w2 - 1) + max (2 ^ length w1 - 1) (2 ^ length w2 - 1)" 1.610 by (rule add_mono,safe intro!: le_maxI1 le_maxI2) 1.611 - also have "... = 2 * max (2 ^ length w1 - 1) (2 ^ length w2 - 1)" 1.612 - by simp 1.613 + also have "... = 2 * max (2 ^ length w1 - 1) (2 ^ length w2 - 1)" by simp 1.614 also have "... \<le> 2 ^ Suc (max (length w1) (length w2)) - 2" 1.615 proof (cases "length w1 \<le> length w2") 1.616 assume w1w2: "length w1 \<le> length w2" 1.617 - hence "(2::nat) ^ length w1 \<le> 2 ^ length w2" 1.618 - by simp 1.619 - hence "(2::nat) ^ length w1 - 1 \<le> 2 ^ length w2 - 1" 1.620 - by arith 1.621 + hence "(2::nat) ^ length w1 \<le> 2 ^ length w2" by simp 1.622 + hence "(2::nat) ^ length w1 - 1 \<le> 2 ^ length w2 - 1" by arith 1.623 with w1w2 show ?thesis 1.624 by (simp add: diff_mult_distrib2 split: split_max) 1.625 next 1.626 @@ -850,12 +786,9 @@ 1.627 assume "(2::nat) ^ length w1 - 1 \<le> 2 ^ length w2 - 1" 1.628 hence "((2::nat) ^ length w1 - 1) + 1 \<le> (2 ^ length w2 - 1) + 1" 1.629 by (rule add_right_mono) 1.630 - hence "(2::nat) ^ length w1 \<le> 2 ^ length w2" 1.631 - by simp 1.632 - hence "length w1 \<le> length w2" 1.633 - by simp 1.634 - thus False 1.635 - by simp 1.636 + hence "(2::nat) ^ length w1 \<le> 2 ^ length w2" by simp 1.637 + hence "length w1 \<le> length w2" by simp 1.638 + thus False by simp 1.639 qed 1.640 thus ?thesis 1.641 by (simp add: diff_mult_distrib2 split: split_max) 1.642 @@ -899,10 +832,12 @@ 1.643 1.644 consts 1.645 norm_signed :: "bit list => bit list" 1.646 - 1.647 primrec 1.648 norm_signed_Nil: "norm_signed [] = []" 1.649 - norm_signed_Cons: "norm_signed (b#bs) = (case b of \<zero> => if norm_unsigned bs = [] then [] else b#norm_unsigned bs | \<one> => b#rem_initial b bs)" 1.650 + norm_signed_Cons: "norm_signed (b#bs) = 1.651 + (case b of 1.652 + \<zero> => if norm_unsigned bs = [] then [] else b#norm_unsigned bs 1.653 + | \<one> => b#rem_initial b bs)" 1.654 1.655 lemma norm_signed0 [simp]: "norm_signed [\<zero>] = []" 1.656 by simp 1.657 @@ -933,27 +868,30 @@ 1.658 lemma int_to_bv_ge0 [simp]: "0 \<le> n ==> int_to_bv n = norm_signed (\<zero> # nat_to_bv (nat n))" 1.659 by (simp add: int_to_bv_def) 1.660 1.661 -lemma int_to_bv_lt0 [simp]: "n < 0 ==> int_to_bv n = norm_signed (bv_not (\<zero>#nat_to_bv (nat (-n- 1))))" 1.662 +lemma int_to_bv_lt0 [simp]: 1.663 + "n < 0 ==> int_to_bv n = norm_signed (bv_not (\<zero>#nat_to_bv (nat (-n- 1))))" 1.664 by (simp add: int_to_bv_def) 1.665 1.666 lemma norm_signed_idem [simp]: "norm_signed (norm_signed w) = norm_signed w" 1.667 -proof (rule bit_list_induct [of _ w],simp_all) 1.668 +proof (rule bit_list_induct [of _ w], simp_all) 1.669 fix xs 1.670 - assume "norm_signed (norm_signed xs) = norm_signed xs" 1.671 + assume eq: "norm_signed (norm_signed xs) = norm_signed xs" 1.672 show "norm_signed (norm_signed (\<zero>#xs)) = norm_signed (\<zero>#xs)" 1.673 proof (rule bit_list_cases [of xs],simp_all) 1.674 fix ys 1.675 - assume [symmetric,simp]: "xs = \<zero>#ys" 1.676 + assume "xs = \<zero>#ys" 1.677 + from this [symmetric] and eq 1.678 show "norm_signed (norm_signed (\<zero>#ys)) = norm_signed (\<zero>#ys)" 1.679 by simp 1.680 qed 1.681 next 1.682 fix xs 1.683 - assume "norm_signed (norm_signed xs) = norm_signed xs" 1.684 + assume eq: "norm_signed (norm_signed xs) = norm_signed xs" 1.685 show "norm_signed (norm_signed (\<one>#xs)) = norm_signed (\<one>#xs)" 1.686 proof (rule bit_list_cases [of xs],simp_all) 1.687 fix ys 1.688 - assume [symmetric,simp]: "xs = \<one>#ys" 1.689 + assume "xs = \<one>#ys" 1.690 + from this [symmetric] and eq 1.691 show "norm_signed (norm_signed (\<one>#ys)) = norm_signed (\<one>#ys)" 1.692 by simp 1.693 qed 1.694 @@ -975,11 +913,11 @@ 1.695 by (simp add: bv_to_int_def) 1.696 1.697 lemma bv_to_int_type [simp]: "bv_to_int (norm_signed w) = bv_to_int w" 1.698 -proof (rule bit_list_induct [of _ w],simp_all) 1.699 +proof (rule bit_list_induct [of _ w], simp_all) 1.700 fix xs 1.701 assume ind: "bv_to_int (norm_signed xs) = bv_to_int xs" 1.702 show "bv_to_int (norm_signed (\<zero>#xs)) = int (bv_to_nat xs)" 1.703 - proof (rule bit_list_cases [of xs],simp_all) 1.704 + proof (rule bit_list_cases [of xs], simp_all) 1.705 fix ys 1.706 assume [simp]: "xs = \<zero>#ys" 1.707 from ind 1.708 @@ -990,7 +928,7 @@ 1.709 fix xs 1.710 assume ind: "bv_to_int (norm_signed xs) = bv_to_int xs" 1.711 show "bv_to_int (norm_signed (\<one>#xs)) = - int (bv_to_nat (bv_not xs)) + -1" 1.712 - proof (rule bit_list_cases [of xs],simp_all) 1.713 + proof (rule bit_list_cases [of xs], simp_all) 1.714 fix ys 1.715 assume [simp]: "xs = \<one>#ys" 1.716 from ind 1.717 @@ -1007,23 +945,17 @@ 1.718 by (simp add: int_nat_two_exp) 1.719 next 1.720 fix bs 1.721 - have "- int (bv_to_nat (bv_not bs)) + -1 \<le> 0" 1.722 - by simp 1.723 - also have "... < 2 ^ length bs" 1.724 - by (induct bs,simp_all) 1.725 - finally show "- int (bv_to_nat (bv_not bs)) + -1 < 2 ^ length bs" 1.726 - . 1.727 + have "- int (bv_to_nat (bv_not bs)) + -1 \<le> 0" by simp 1.728 + also have "... < 2 ^ length bs" by (induct bs) simp_all 1.729 + finally show "- int (bv_to_nat (bv_not bs)) + -1 < 2 ^ length bs" . 1.730 qed 1.731 1.732 lemma bv_to_int_lower_range: "- (2 ^ (length w - 1)) \<le> bv_to_int w" 1.733 proof (rule bit_list_cases [of w],simp_all) 1.734 fix bs :: "bit list" 1.735 - have "- (2 ^ length bs) \<le> (0::int)" 1.736 - by (induct bs,simp_all) 1.737 - also have "... \<le> int (bv_to_nat bs)" 1.738 - by simp 1.739 - finally show "- (2 ^ length bs) \<le> int (bv_to_nat bs)" 1.740 - . 1.741 + have "- (2 ^ length bs) \<le> (0::int)" by (induct bs) simp_all 1.742 + also have "... \<le> int (bv_to_nat bs)" by simp 1.743 + finally show "- (2 ^ length bs) \<le> int (bv_to_nat bs)" . 1.744 next 1.745 fix bs 1.746 from bv_to_nat_upper_range [of "bv_not bs"] 1.747 @@ -1063,20 +995,20 @@ 1.748 qed 1.749 1.750 lemma bv_int_bv [simp]: "bv_to_int (int_to_bv i) = i" 1.751 - by (cases "0 \<le> i",simp_all) 1.752 + by (cases "0 \<le> i") simp_all 1.753 1.754 lemma bv_msb_norm [simp]: "bv_msb (norm_signed w) = bv_msb w" 1.755 - by (rule bit_list_cases [of w],simp_all add: norm_signed_Cons) 1.756 + by (rule bit_list_cases [of w]) (simp_all add: norm_signed_Cons) 1.757 1.758 lemma norm_signed_length: "length (norm_signed w) \<le> length w" 1.759 - apply (cases w,simp_all) 1.760 + apply (cases w, simp_all) 1.761 apply (subst norm_signed_Cons) 1.762 - apply (case_tac "a",simp_all) 1.763 + apply (case_tac a, simp_all) 1.764 apply (rule rem_initial_length) 1.765 done 1.766 1.767 lemma norm_signed_equal: "length (norm_signed w) = length w ==> norm_signed w = w" 1.768 -proof (rule bit_list_cases [of w],simp_all) 1.769 +proof (rule bit_list_cases [of w], simp_all) 1.770 fix xs 1.771 assume "length (norm_signed (\<zero>#xs)) = Suc (length xs)" 1.772 thus "norm_signed (\<zero>#xs) = \<zero>#xs" 1.773 @@ -1135,18 +1067,13 @@ 1.774 shows "xs = ys" 1.775 proof - 1.776 from one 1.777 - have "int_to_bv (bv_to_int xs) = int_to_bv (bv_to_int ys)" 1.778 - by simp 1.779 - hence xsys: "norm_signed xs = norm_signed ys" 1.780 - by simp 1.781 + have "int_to_bv (bv_to_int xs) = int_to_bv (bv_to_int ys)" by simp 1.782 + hence xsys: "norm_signed xs = norm_signed ys" by simp 1.783 hence xsys': "bv_msb xs = bv_msb ys" 1.784 proof - 1.785 - have "bv_msb xs = bv_msb (norm_signed xs)" 1.786 - by simp 1.787 - also have "... = bv_msb (norm_signed ys)" 1.788 - by (simp add: xsys) 1.789 - also have "... = bv_msb ys" 1.790 - by simp 1.791 + have "bv_msb xs = bv_msb (norm_signed xs)" by simp 1.792 + also have "... = bv_msb (norm_signed ys)" by (simp add: xsys) 1.793 + also have "... = bv_msb ys" by simp 1.794 finally show ?thesis . 1.795 qed 1.796 have "xs = bv_extend (length xs) (bv_msb xs) (norm_signed xs)" 1.797 @@ -1172,25 +1099,20 @@ 1.798 shows "2 ^ (length (norm_signed w) - 2) \<le> bv_to_int w" 1.799 proof - 1.800 from w0 1.801 - have "0 \<le> bv_to_int w" 1.802 - by simp 1.803 - hence [simp]: "bv_msb w = \<zero>" 1.804 - by (rule bv_to_int_msb0) 1.805 + have "0 \<le> bv_to_int w" by simp 1.806 + hence [simp]: "bv_msb w = \<zero>" by (rule bv_to_int_msb0) 1.807 have "2 ^ (length (norm_signed w) - 2) \<le> bv_to_int (norm_signed w)" 1.808 proof (rule bit_list_cases [of w]) 1.809 assume "w = []" 1.810 - with w0 1.811 - show ?thesis 1.812 - by simp 1.813 + with w0 show ?thesis by simp 1.814 next 1.815 fix w' 1.816 assume weq: "w = \<zero> # w'" 1.817 thus ?thesis 1.818 proof (simp add: norm_signed_Cons,safe) 1.819 assume "norm_unsigned w' = []" 1.820 - with weq and w0 1.821 - show False 1.822 - by (simp add: norm_empty_bv_to_nat_zero) 1.823 + with weq and w0 show False 1.824 + by (simp add: norm_empty_bv_to_nat_zero) 1.825 next 1.826 assume w'0: "norm_unsigned w' \<noteq> []" 1.827 have "0 < bv_to_nat w'" 1.828 @@ -1201,8 +1123,7 @@ 1.829 hence "norm_unsigned w' = []" 1.830 by (simp add: bv_to_nat_zero_imp_empty) 1.831 with w'0 1.832 - show False 1.833 - by simp 1.834 + show False by simp 1.835 qed 1.836 with bv_to_nat_lower_limit [of w'] 1.837 show "2 ^ (length (norm_unsigned w') - Suc 0) \<le> int (bv_to_nat w')" 1.838 @@ -1211,15 +1132,10 @@ 1.839 next 1.840 fix w' 1.841 assume "w = \<one> # w'" 1.842 - from w0 1.843 - have "bv_msb w = \<zero>" 1.844 - by simp 1.845 - with prems 1.846 - show ?thesis 1.847 - by simp 1.848 + from w0 have "bv_msb w = \<zero>" by simp 1.849 + with prems show ?thesis by simp 1.850 qed 1.851 - also have "... = bv_to_int w" 1.852 - by simp 1.853 + also have "... = bv_to_int w" by simp 1.854 finally show ?thesis . 1.855 qed 1.856 1.857 @@ -1235,19 +1151,14 @@ 1.858 assume msb: "\<zero> = bv_msb (norm_unsigned l)" 1.859 assume "norm_unsigned l \<noteq> []" 1.860 with norm_unsigned_result [of l] 1.861 - have "bv_msb (norm_unsigned l) = \<one>" 1.862 - by simp 1.863 - with msb 1.864 - show False 1.865 - by simp 1.866 + have "bv_msb (norm_unsigned l) = \<one>" by simp 1.867 + with msb show False by simp 1.868 next 1.869 fix xs 1.870 assume p: "\<one> = bv_msb (tl (norm_signed (\<one> # xs)))" 1.871 have "\<one> \<noteq> bv_msb (tl (norm_signed (\<one> # xs)))" 1.872 by (rule bit_list_induct [of _ xs],simp_all) 1.873 - with p 1.874 - show False 1.875 - by simp 1.876 + with p show False by simp 1.877 qed 1.878 1.879 lemma bv_to_int_upper_limit_lem1: 1.880 @@ -1255,61 +1166,41 @@ 1.881 shows "bv_to_int w < - (2 ^ (length (norm_signed w) - 2))" 1.882 proof - 1.883 from w0 1.884 - have "bv_to_int w < 0" 1.885 - by simp 1.886 + have "bv_to_int w < 0" by simp 1.887 hence msbw [simp]: "bv_msb w = \<one>" 1.888 by (rule bv_to_int_msb1) 1.889 - have "bv_to_int w = bv_to_int (norm_signed w)" 1.890 - by simp 1.891 + have "bv_to_int w = bv_to_int (norm_signed w)" by simp 1.892 also from norm_signed_result [of w] 1.893 have "... < - (2 ^ (length (norm_signed w) - 2))" 1.894 - proof (safe) 1.895 + proof safe 1.896 assume "norm_signed w = []" 1.897 - hence "bv_to_int (norm_signed w) = 0" 1.898 - by simp 1.899 - with w0 1.900 - show ?thesis 1.901 - by simp 1.902 + hence "bv_to_int (norm_signed w) = 0" by simp 1.903 + with w0 show ?thesis by simp 1.904 next 1.905 assume "norm_signed w = [\<one>]" 1.906 - hence "bv_to_int (norm_signed w) = -1" 1.907 - by simp 1.908 - with w0 1.909 - show ?thesis 1.910 - by simp 1.911 + hence "bv_to_int (norm_signed w) = -1" by simp 1.912 + with w0 show ?thesis by simp 1.913 next 1.914 assume "bv_msb (norm_signed w) \<noteq> bv_msb (tl (norm_signed w))" 1.915 - hence msb_tl: "\<one> \<noteq> bv_msb (tl (norm_signed w))" 1.916 - by simp 1.917 + hence msb_tl: "\<one> \<noteq> bv_msb (tl (norm_signed w))" by simp 1.918 show "bv_to_int (norm_signed w) < - (2 ^ (length (norm_signed w) - 2))" 1.919 proof (rule bit_list_cases [of "norm_signed w"]) 1.920 assume "norm_signed w = []" 1.921 - hence "bv_to_int (norm_signed w) = 0" 1.922 - by simp 1.923 - with w0 1.924 - show ?thesis 1.925 - by simp 1.926 + hence "bv_to_int (norm_signed w) = 0" by simp 1.927 + with w0 show ?thesis by simp 1.928 next 1.929 fix w' 1.930 assume nw: "norm_signed w = \<zero> # w'" 1.931 - from msbw 1.932 - have "bv_msb (norm_signed w) = \<one>" 1.933 - by simp 1.934 - with nw 1.935 - show ?thesis 1.936 - by simp 1.937 + from msbw have "bv_msb (norm_signed w) = \<one>" by simp 1.938 + with nw show ?thesis by simp 1.939 next 1.940 fix w' 1.941 assume weq: "norm_signed w = \<one> # w'" 1.942 show ?thesis 1.943 proof (rule bit_list_cases [of w']) 1.944 assume w'eq: "w' = []" 1.945 - from w0 1.946 - have "bv_to_int (norm_signed w) < -1" 1.947 - by simp 1.948 - with w'eq and weq 1.949 - show ?thesis 1.950 - by simp 1.951 + from w0 have "bv_to_int (norm_signed w) < -1" by simp 1.952 + with w'eq and weq show ?thesis by simp 1.953 next 1.954 fix w'' 1.955 assume w'eq: "w' = \<zero> # w''" 1.956 @@ -1323,9 +1214,7 @@ 1.957 next 1.958 fix w'' 1.959 assume w'eq: "w' = \<one> # w''" 1.960 - with weq and msb_tl 1.961 - show ?thesis 1.962 - by simp 1.963 + with weq and msb_tl show ?thesis by simp 1.964 qed 1.965 qed 1.966 qed 1.967 @@ -1341,28 +1230,20 @@ 1.968 have k1: "1 < k" 1.969 by (cases "k - 1",simp_all) 1.970 assume "~ length (int_to_bv i) \<le> k" 1.971 - hence "k < length (int_to_bv i)" 1.972 - by simp 1.973 - hence "k \<le> length (int_to_bv i) - 1" 1.974 - by arith 1.975 - hence a: "k - 1 \<le> length (int_to_bv i) - 2" 1.976 - by arith 1.977 + hence "k < length (int_to_bv i)" by simp 1.978 + hence "k \<le> length (int_to_bv i) - 1" by arith 1.979 + hence a: "k - 1 \<le> length (int_to_bv i) - 2" by arith 1.980 hence "(2::int) ^ (k - 1) \<le> 2 ^ (length (int_to_bv i) - 2)" by simp 1.981 also have "... \<le> i" 1.982 proof - 1.983 have "2 ^ (length (norm_signed (int_to_bv i)) - 2) \<le> bv_to_int (int_to_bv i)" 1.984 proof (rule bv_to_int_lower_limit_gt0) 1.985 - from w0 1.986 - show "0 < bv_to_int (int_to_bv i)" 1.987 - by simp 1.988 + from w0 show "0 < bv_to_int (int_to_bv i)" by simp 1.989 qed 1.990 - thus ?thesis 1.991 - by simp 1.992 + thus ?thesis by simp 1.993 qed 1.994 finally have "2 ^ (k - 1) \<le> i" . 1.995 - with wk 1.996 - show False 1.997 - by simp 1.998 + with wk show False by simp 1.999 qed 1.1000 1.1001 lemma pos_length_pos: 1.1002 @@ -1373,26 +1254,21 @@ 1.1003 have "0 < length (norm_signed w)" 1.1004 proof (auto) 1.1005 assume ii: "norm_signed w = []" 1.1006 - have "bv_to_int (norm_signed w) = 0" 1.1007 - by (subst ii,simp) 1.1008 - hence "bv_to_int w = 0" 1.1009 - by simp 1.1010 - with i0 1.1011 - show False 1.1012 - by simp 1.1013 + have "bv_to_int (norm_signed w) = 0" by (subst ii) simp 1.1014 + hence "bv_to_int w = 0" by simp 1.1015 + with i0 show False by simp 1.1016 next 1.1017 assume ii: "norm_signed w = []" 1.1018 assume jj: "bv_msb w \<noteq> \<zero>" 1.1019 have "\<zero> = bv_msb (norm_signed w)" 1.1020 - by (subst ii,simp) 1.1021 + by (subst ii) simp 1.1022 also have "... \<noteq> \<zero>" 1.1023 by (simp add: jj) 1.1024 finally show False by simp 1.1025 qed 1.1026 also have "... \<le> length w" 1.1027 by (rule norm_signed_length) 1.1028 - finally show ?thesis 1.1029 - . 1.1030 + finally show ?thesis . 1.1031 qed 1.1032 1.1033 lemma neg_length_pos: 1.1034 @@ -1404,25 +1280,19 @@ 1.1035 proof (auto) 1.1036 assume ii: "norm_signed w = []" 1.1037 have "bv_to_int (norm_signed w) = 0" 1.1038 - by (subst ii,simp) 1.1039 - hence "bv_to_int w = 0" 1.1040 - by simp 1.1041 - with i0 1.1042 - show False 1.1043 - by simp 1.1044 + by (subst ii) simp 1.1045 + hence "bv_to_int w = 0" by simp 1.1046 + with i0 show False by simp 1.1047 next 1.1048 assume ii: "norm_signed w = []" 1.1049 assume jj: "bv_msb w \<noteq> \<zero>" 1.1050 - have "\<zero> = bv_msb (norm_signed w)" 1.1051 - by (subst ii,simp) 1.1052 - also have "... \<noteq> \<zero>" 1.1053 - by (simp add: jj) 1.1054 + have "\<zero> = bv_msb (norm_signed w)" by (subst ii) simp 1.1055 + also have "... \<noteq> \<zero>" by (simp add: jj) 1.1056 finally show False by simp 1.1057 qed 1.1058 also have "... \<le> length w" 1.1059 by (rule norm_signed_length) 1.1060 - finally show ?thesis 1.1061 - . 1.1062 + finally show ?thesis . 1.1063 qed 1.1064 1.1065 lemma length_int_to_bv_lower_limit_gt0: 1.1066 @@ -1430,18 +1300,15 @@ 1.1067 shows "k < length (int_to_bv i)" 1.1068 proof (rule ccontr) 1.1069 have "0 < (2::int) ^ (k - 1)" 1.1070 - by (rule zero_less_power,simp) 1.1071 - also have "... \<le> i" 1.1072 - by (rule wk) 1.1073 - finally have i0: "0 < i" 1.1074 - . 1.1075 + by (rule zero_less_power) simp 1.1076 + also have "... \<le> i" by (rule wk) 1.1077 + finally have i0: "0 < i" . 1.1078 have lii0: "0 < length (int_to_bv i)" 1.1079 apply (rule pos_length_pos) 1.1080 apply (simp,rule i0) 1.1081 done 1.1082 assume "~ k < length (int_to_bv i)" 1.1083 - hence "length (int_to_bv i) \<le> k" 1.1084 - by simp 1.1085 + hence "length (int_to_bv i) \<le> k" by simp 1.1086 with lii0 1.1087 have a: "length (int_to_bv i) - 1 \<le> k - 1" 1.1088 by arith 1.1089 @@ -1454,11 +1321,9 @@ 1.1090 finally show ?thesis . 1.1091 qed 1.1092 also have "(2::int) ^ (length (int_to_bv i) - 1) \<le> 2 ^ (k - 1)" using a 1.1093 - by simp 1.1094 + by simp 1.1095 finally have "i < 2 ^ (k - 1)" . 1.1096 - with wk 1.1097 - show False 1.1098 - by simp 1.1099 + with wk show False by simp 1.1100 qed 1.1101 1.1102 lemma length_int_to_bv_upper_limit_lem1: 1.1103 @@ -1467,15 +1332,11 @@ 1.1104 shows "length (int_to_bv i) \<le> k" 1.1105 proof (rule ccontr) 1.1106 from w1 wk 1.1107 - have k1: "1 < k" 1.1108 - by (cases "k - 1",simp_all) 1.1109 + have k1: "1 < k" by (cases "k - 1") simp_all 1.1110 assume "~ length (int_to_bv i) \<le> k" 1.1111 - hence "k < length (int_to_bv i)" 1.1112 - by simp 1.1113 - hence "k \<le> length (int_to_bv i) - 1" 1.1114 - by arith 1.1115 - hence a: "k - 1 \<le> length (int_to_bv i) - 2" 1.1116 - by arith 1.1117 + hence "k < length (int_to_bv i)" by simp 1.1118 + hence "k \<le> length (int_to_bv i) - 1" by arith 1.1119 + hence a: "k - 1 \<le> length (int_to_bv i) - 2" by arith 1.1120 have "i < - (2 ^ (length (int_to_bv i) - 2))" 1.1121 proof - 1.1122 have "i = bv_to_int (int_to_bv i)" 1.1123 @@ -1486,46 +1347,36 @@ 1.1124 qed 1.1125 also have "... \<le> -(2 ^ (k - 1))" 1.1126 proof - 1.1127 - have "(2::int) ^ (k - 1) \<le> 2 ^ (length (int_to_bv i) - 2)" using a 1.1128 - by simp 1.1129 - thus ?thesis 1.1130 - by simp 1.1131 + have "(2::int) ^ (k - 1) \<le> 2 ^ (length (int_to_bv i) - 2)" using a by simp 1.1132 + thus ?thesis by simp 1.1133 qed 1.1134 finally have "i < -(2 ^ (k - 1))" . 1.1135 - with wk 1.1136 - show False 1.1137 - by simp 1.1138 + with wk show False by simp 1.1139 qed 1.1140 1.1141 lemma length_int_to_bv_lower_limit_lem1: 1.1142 assumes wk: "i < -(2 ^ (k - 1))" 1.1143 shows "k < length (int_to_bv i)" 1.1144 proof (rule ccontr) 1.1145 - from wk 1.1146 - have "i \<le> -(2 ^ (k - 1)) - 1" 1.1147 - by simp 1.1148 + from wk have "i \<le> -(2 ^ (k - 1)) - 1" by simp 1.1149 also have "... < -1" 1.1150 proof - 1.1151 have "0 < (2::int) ^ (k - 1)" 1.1152 - by (rule zero_less_power,simp) 1.1153 - hence "-((2::int) ^ (k - 1)) < 0" 1.1154 - by simp 1.1155 + by (rule zero_less_power) simp 1.1156 + hence "-((2::int) ^ (k - 1)) < 0" by simp 1.1157 thus ?thesis by simp 1.1158 qed 1.1159 finally have i1: "i < -1" . 1.1160 have lii0: "0 < length (int_to_bv i)" 1.1161 apply (rule neg_length_pos) 1.1162 - apply (simp,rule i1) 1.1163 + apply (simp, rule i1) 1.1164 done 1.1165 assume "~ k < length (int_to_bv i)" 1.1166 hence "length (int_to_bv i) \<le> k" 1.1167 by simp 1.1168 - with lii0 1.1169 - have a: "length (int_to_bv i) - 1 \<le> k - 1" 1.1170 - by arith 1.1171 + with lii0 have a: "length (int_to_bv i) - 1 \<le> k - 1" by arith 1.1172 hence "(2::int) ^ (length (int_to_bv i) - 1) \<le> 2 ^ (k - 1)" by simp 1.1173 - hence "-((2::int) ^ (k - 1)) \<le> - (2 ^ (length (int_to_bv i) - 1))" 1.1174 - by simp 1.1175 + hence "-((2::int) ^ (k - 1)) \<le> - (2 ^ (length (int_to_bv i) - 1))" by simp 1.1176 also have "... \<le> i" 1.1177 proof - 1.1178 have "- (2 ^ (length (int_to_bv i) - 1)) \<le> bv_to_int (int_to_bv i)" 1.1179 @@ -1535,11 +1386,10 @@ 1.1180 finally show ?thesis . 1.1181 qed 1.1182 finally have "-(2 ^ (k - 1)) \<le> i" . 1.1183 - with wk 1.1184 - show False 1.1185 - by simp 1.1186 + with wk show False by simp 1.1187 qed 1.1188 1.1189 + 1.1190 subsection {* Signed Arithmetic Operations *} 1.1191 1.1192 subsubsection {* Conversion from unsigned to signed *} 1.1193 @@ -1558,14 +1408,13 @@ 1.1194 by (simp add: utos_def norm_signed_Cons) 1.1195 1.1196 lemma bv_to_int_utos: "bv_to_int (utos w) = int (bv_to_nat w)" 1.1197 -proof (simp add: utos_def norm_signed_Cons,safe) 1.1198 +proof (simp add: utos_def norm_signed_Cons, safe) 1.1199 assume "norm_unsigned w = []" 1.1200 - hence "bv_to_nat (norm_unsigned w) = 0" 1.1201 - by simp 1.1202 - thus "bv_to_nat w = 0" 1.1203 - by simp 1.1204 + hence "bv_to_nat (norm_unsigned w) = 0" by simp 1.1205 + thus "bv_to_nat w = 0" by simp 1.1206 qed 1.1207 1.1208 + 1.1209 subsubsection {* Unary minus *} 1.1210 1.1211 definition 1.1212 @@ -1592,23 +1441,17 @@ 1.1213 done 1.1214 show ?thesis 1.1215 proof (simp add: bv_uminus_def,rule length_int_to_bv_upper_limit_gt0,simp_all) 1.1216 - from prems 1.1217 - show "bv_to_int w < 0" 1.1218 - by simp 1.1219 + from prems show "bv_to_int w < 0" by simp 1.1220 next 1.1221 have "-(2^(length w - 1)) \<le> bv_to_int w" 1.1222 by (rule bv_to_int_lower_range) 1.1223 - hence "- bv_to_int w \<le> 2^(length w - 1)" 1.1224 - by simp 1.1225 - also from lw have "... < 2 ^ length w" 1.1226 - by simp 1.1227 - finally show "- bv_to_int w < 2 ^ length w" 1.1228 - by simp 1.1229 + hence "- bv_to_int w \<le> 2^(length w - 1)" by simp 1.1230 + also from lw have "... < 2 ^ length w" by simp 1.1231 + finally show "- bv_to_int w < 2 ^ length w" by simp 1.1232 qed 1.1233 next 1.1234 assume p: "- bv_to_int w = 1" 1.1235 - hence lw: "0 < length w" 1.1236 - by (cases w,simp_all) 1.1237 + hence lw: "0 < length w" by (cases w) simp_all 1.1238 from p 1.1239 show ?thesis 1.1240 apply (simp add: bv_uminus_def) 1.1241 @@ -1617,12 +1460,10 @@ 1.1242 done 1.1243 next 1.1244 assume "- bv_to_int w = 0" 1.1245 - thus ?thesis 1.1246 - by (simp add: bv_uminus_def) 1.1247 + thus ?thesis by (simp add: bv_uminus_def) 1.1248 next 1.1249 assume p: "- bv_to_int w = -1" 1.1250 - thus ?thesis 1.1251 - by (simp add: bv_uminus_def) 1.1252 + thus ?thesis by (simp add: bv_uminus_def) 1.1253 next 1.1254 assume p: "- bv_to_int w < -1" 1.1255 show ?thesis 1.1256 @@ -1634,8 +1475,7 @@ 1.1257 have "bv_to_int w < 2 ^ (length w - 1)" 1.1258 by (rule bv_to_int_upper_range) 1.1259 also have "... \<le> 2 ^ length w" by simp 1.1260 - finally show "bv_to_int w \<le> 2 ^ length w" 1.1261 - by simp 1.1262 + finally show "bv_to_int w \<le> 2 ^ length w" by simp 1.1263 qed 1.1264 qed 1.1265 qed 1.1266 @@ -1643,17 +1483,14 @@ 1.1267 lemma bv_uminus_length_utos: "length (bv_uminus (utos w)) \<le> Suc (length w)" 1.1268 proof - 1.1269 have "-bv_to_int (utos w) = 0 \<or> -bv_to_int (utos w) = -1 \<or> -bv_to_int (utos w) < -1" 1.1270 - apply (simp add: bv_to_int_utos) 1.1271 - by arith 1.1272 + by (simp add: bv_to_int_utos, arith) 1.1273 thus ?thesis 1.1274 proof safe 1.1275 assume "-bv_to_int (utos w) = 0" 1.1276 - thus ?thesis 1.1277 - by (simp add: bv_uminus_def) 1.1278 + thus ?thesis by (simp add: bv_uminus_def) 1.1279 next 1.1280 assume "-bv_to_int (utos w) = -1" 1.1281 - thus ?thesis 1.1282 - by (simp add: bv_uminus_def) 1.1283 + thus ?thesis by (simp add: bv_uminus_def) 1.1284 next 1.1285 assume p: "-bv_to_int (utos w) < -1" 1.1286 show ?thesis 1.1287 @@ -1684,7 +1521,8 @@ 1.1288 assumes lw: "0 < max (length w1) (length w2)" 1.1289 shows "((2::int) ^ (length w1 - 1)) + (2 ^ (length w2 - 1)) \<le> 2 ^ max (length w1) (length w2)" 1.1290 proof - 1.1291 - have "((2::int) ^ (length w1 - 1)) + (2 ^ (length w2 - 1)) \<le> 2 ^ (max (length w1) (length w2) - 1) + 2 ^ (max (length w1) (length w2) - 1)" 1.1292 + have "((2::int) ^ (length w1 - 1)) + (2 ^ (length w2 - 1)) \<le> 1.1293 + 2 ^ (max (length w1) (length w2) - 1) + 2 ^ (max (length w1) (length w2) - 1)" 1.1294 apply (cases "length w1 \<le> length w2") 1.1295 apply (auto simp add: max_def) 1.1296 done 1.1297 @@ -1713,15 +1551,12 @@ 1.1298 show "w2 \<noteq> []" 1.1299 proof (rule ccontr,simp) 1.1300 assume [simp]: "w2 = []" 1.1301 - from p 1.1302 - show False 1.1303 - by simp 1.1304 + from p show False by simp 1.1305 qed 1.1306 qed 1.1307 qed 1.1308 1.1309 - have "0 < ?Q \<or> ?Q = 0 \<or> ?Q = -1 \<or> ?Q < -1" 1.1310 - by arith 1.1311 + have "0 < ?Q \<or> ?Q = 0 \<or> ?Q = -1 \<or> ?Q < -1" by arith 1.1312 thus ?thesis 1.1313 proof safe 1.1314 assume "?Q = 0" 1.1315 @@ -1750,8 +1585,7 @@ 1.1316 using p 1.1317 apply simp 1.1318 done 1.1319 - finally show "?Q < 2 ^ max (length w1) (length w2)" 1.1320 - . 1.1321 + finally show "?Q < 2 ^ max (length w1) (length w2)" . 1.1322 qed 1.1323 next 1.1324 assume p: "?Q < -1" 1.1325 @@ -1802,20 +1636,16 @@ 1.1326 by (rule le_maxI1) 1.1327 also have "... \<le> Suc (max (length w1) (length w2))" 1.1328 by arith 1.1329 - finally show "length (norm_signed w1) \<le> Suc (max (length w1) (length w2))" 1.1330 - . 1.1331 + finally show "length (norm_signed w1) \<le> Suc (max (length w1) (length w2))" . 1.1332 qed 1.1333 next 1.1334 assume "bv_to_int w2 \<noteq> 0" 1.1335 - hence "0 < length w2" 1.1336 - by (cases w2,simp_all) 1.1337 - hence lmw: "0 < max (length w1) (length w2)" 1.1338 - by arith 1.1339 + hence "0 < length w2" by (cases w2,simp_all) 1.1340 + hence lmw: "0 < max (length w1) (length w2)" by arith 1.1341 1.1342 let ?Q = "bv_to_int w1 - bv_to_int w2" 1.1343 1.1344 - have "0 < ?Q \<or> ?Q = 0 \<or> ?Q = -1 \<or> ?Q < -1" 1.1345 - by arith 1.1346 + have "0 < ?Q \<or> ?Q = 0 \<or> ?Q = -1 \<or> ?Q < -1" by arith 1.1347 thus ?thesis 1.1348 proof safe 1.1349 assume "?Q = 0" 1.1350 @@ -1833,8 +1663,7 @@ 1.1351 apply (rule p) 1.1352 proof simp 1.1353 from bv_to_int_lower_range [of w2] 1.1354 - have v2: "- bv_to_int w2 \<le> 2 ^ (length w2 - 1)" 1.1355 - by simp 1.1356 + have v2: "- bv_to_int w2 \<le> 2 ^ (length w2 - 1)" by simp 1.1357 have "bv_to_int w1 + - bv_to_int w2 < (2 ^ (length w1 - 1)) + (2 ^ (length w2 - 1))" 1.1358 apply (rule zadd_zless_mono) 1.1359 apply (rule bv_to_int_upper_range [of w1]) 1.1360 @@ -1844,8 +1673,7 @@ 1.1361 apply (rule adder_helper) 1.1362 apply (rule lmw) 1.1363 done 1.1364 - finally show "?Q < 2 ^ max (length w1) (length w2)" 1.1365 - by simp 1.1366 + finally show "?Q < 2 ^ max (length w1) (length w2)" by simp 1.1367 qed 1.1368 next 1.1369 assume p: "?Q < -1" 1.1370 @@ -1866,8 +1694,7 @@ 1.1371 using bv_to_int_upper_range [of w2] 1.1372 apply simp 1.1373 done 1.1374 - finally show "- (2^max (length w1) (length w2)) \<le> ?Q" 1.1375 - by simp 1.1376 + finally show "- (2^max (length w1) (length w2)) \<le> ?Q" by simp 1.1377 qed 1.1378 qed 1.1379 qed 1.1380 @@ -1889,20 +1716,16 @@ 1.1381 proof - 1.1382 let ?Q = "bv_to_int w1 * bv_to_int w2" 1.1383 1.1384 - have lmw: "?Q \<noteq> 0 ==> 0 < length w1 \<and> 0 < length w2" 1.1385 - by auto 1.1386 + have lmw: "?Q \<noteq> 0 ==> 0 < length w1 \<and> 0 < length w2" by auto 1.1387 1.1388 - have "0 < ?Q \<or> ?Q = 0 \<or> ?Q = -1 \<or> ?Q < -1" 1.1389 - by arith 1.1390 + have "0 < ?Q \<or> ?Q = 0 \<or> ?Q = -1 \<or> ?Q < -1" by arith 1.1391 thus ?thesis 1.1392 proof (safe dest!: iffD1 [OF mult_eq_0_iff]) 1.1393 assume "bv_to_int w1 = 0" 1.1394 - thus ?thesis 1.1395 - by (simp add: bv_smult_def) 1.1396 + thus ?thesis by (simp add: bv_smult_def) 1.1397 next 1.1398 assume "bv_to_int w2 = 0" 1.1399 - thus ?thesis 1.1400 - by (simp add: bv_smult_def) 1.1401 + thus ?thesis by (simp add: bv_smult_def) 1.1402 next 1.1403 assume p: "?Q = -1" 1.1404 show ?thesis 1.1405 @@ -1937,8 +1760,7 @@ 1.1406 apply (subst zpower_zadd_distrib [symmetric]) 1.1407 apply simp 1.1408 done 1.1409 - finally show "?Q < 2 ^ (length w1 + length w2 - Suc 0)" 1.1410 - . 1.1411 + finally show "?Q < 2 ^ (length w1 + length w2 - Suc 0)" . 1.1412 qed 1.1413 next 1.1414 assume bi1: "bv_to_int w1 < 0" 1.1415 @@ -2028,33 +1850,28 @@ 1.1416 by simp 1.1417 qed 1.1418 qed 1.1419 - finally show "-(2 ^ (length w1 + length w2 - Suc 0)) \<le> ?Q" 1.1420 - . 1.1421 + finally show "-(2 ^ (length w1 + length w2 - Suc 0)) \<le> ?Q" . 1.1422 qed 1.1423 qed 1.1424 qed 1.1425 1.1426 lemma bv_msb_one: "bv_msb w = \<one> ==> 0 < bv_to_nat w" 1.1427 - by (cases w,simp_all) 1.1428 + by (cases w) simp_all 1.1429 1.1430 lemma bv_smult_length_utos: "length (bv_smult (utos w1) w2) \<le> length w1 + length w2" 1.1431 proof - 1.1432 let ?Q = "bv_to_int (utos w1) * bv_to_int w2" 1.1433 1.1434 - have lmw: "?Q \<noteq> 0 ==> 0 < length (utos w1) \<and> 0 < length w2" 1.1435 - by auto 1.1436 + have lmw: "?Q \<noteq> 0 ==> 0 < length (utos w1) \<and> 0 < length w2" by auto 1.1437 1.1438 - have "0 < ?Q \<or> ?Q = 0 \<or> ?Q = -1 \<or> ?Q < -1" 1.1439 - by arith 1.1440 + have "0 < ?Q \<or> ?Q = 0 \<or> ?Q = -1 \<or> ?Q < -1" by arith 1.1441 thus ?thesis 1.1442 proof (safe dest!: iffD1 [OF mult_eq_0_iff]) 1.1443 assume "bv_to_int (utos w1) = 0" 1.1444 - thus ?thesis 1.1445 - by (simp add: bv_smult_def) 1.1446 + thus ?thesis by (simp add: bv_smult_def) 1.1447 next 1.1448 assume "bv_to_int w2 = 0" 1.1449 - thus ?thesis 1.1450 - by (simp add: bv_smult_def) 1.1451 + thus ?thesis by (simp add: bv_smult_def) 1.1452 next 1.1453 assume p: "0 < ?Q" 1.1454 thus ?thesis 1.1455 @@ -2083,13 +1900,11 @@ 1.1456 using p 1.1457 apply auto 1.1458 done 1.1459 - finally show "?Q < 2 ^ (length w1 + length w2 - Suc 0)" 1.1460 - . 1.1461 + finally show "?Q < 2 ^ (length w1 + length w2 - Suc 0)" . 1.1462 qed 1.1463 next 1.1464 assume "bv_to_int (utos w1) < 0" 1.1465 - thus ?thesis 1.1466 - by (simp add: bv_to_int_utos) 1.1467 + thus ?thesis by (simp add: bv_to_int_utos) 1.1468 qed 1.1469 next 1.1470 assume p: "?Q = -1" 1.1471 @@ -2147,8 +1962,7 @@ 1.1472 by (simp add: bv_to_int_utos) 1.1473 qed 1.1474 qed 1.1475 - finally show "-(2 ^ (length w1 + length w2 - Suc 0)) \<le> ?Q" 1.1476 - . 1.1477 + finally show "-(2 ^ (length w1 + length w2 - Suc 0)) \<le> ?Q" . 1.1478 qed 1.1479 qed 1.1480 qed 1.1481 @@ -2183,9 +1997,7 @@ 1.1482 show "xs ! (length xs - Suc n) = rev xs ! n" 1.1483 proof (cases xs) 1.1484 assume "xs = []" 1.1485 - with notx 1.1486 - show ?thesis 1.1487 - by simp 1.1488 + with notx show ?thesis by simp 1.1489 next 1.1490 fix y ys 1.1491 assume [simp]: "xs = y # ys" 1.1492 @@ -2195,33 +2007,23 @@ 1.1493 from spec [OF ind,of ys] 1.1494 have "\<forall>n. n < length ys --> ys ! (length ys - Suc n) = rev ys ! n" 1.1495 by simp 1.1496 - hence "n < length ys --> ys ! (length ys - Suc n) = rev ys ! n" 1.1497 - .. 1.1498 - hence "ys ! (length ys - Suc n) = rev ys ! n" 1.1499 - .. 1.1500 + hence "n < length ys --> ys ! (length ys - Suc n) = rev ys ! n" .. 1.1501 + from this and noty 1.1502 + have "ys ! (length ys - Suc n) = rev ys ! n" .. 1.1503 thus "(y # ys) ! (length ys - n) = rev ys ! n" 1.1504 by (simp add: nth_Cons' noty linorder_not_less [symmetric]) 1.1505 next 1.1506 assume "~ n < length ys" 1.1507 - hence x: "length ys \<le> n" 1.1508 - by simp 1.1509 - from notx 1.1510 - have "n < Suc (length ys)" 1.1511 - by simp 1.1512 - hence "n \<le> length ys" 1.1513 - by simp 1.1514 - with x 1.1515 - have "length ys = n" 1.1516 - by simp 1.1517 - thus "y = [y] ! (n - length ys)" 1.1518 - by simp 1.1519 + hence x: "length ys \<le> n" by simp 1.1520 + from notx have "n < Suc (length ys)" by simp 1.1521 + hence "n \<le> length ys" by simp 1.1522 + with x have "length ys = n" by simp 1.1523 + thus "y = [y] ! (n - length ys)" by simp 1.1524 qed 1.1525 qed 1.1526 qed 1.1527 - hence "n < length w --> bv_select w n = rev w ! n" 1.1528 - .. 1.1529 - thus ?thesis 1.1530 - .. 1.1531 + then have "n < length w --> bv_select w n = rev w ! n" .. 1.1532 + from this and notnull show ?thesis .. 1.1533 qed 1.1534 1.1535 lemma bv_chop_append: "bv_chop (w1 @ w2) (length w2) = (w1,w2)" 1.1536 @@ -2252,12 +2054,10 @@ 1.1537 apply (rule ccontr) 1.1538 proof - 1.1539 assume "~ n < 2 ^ length (nat_to_bv n)" 1.1540 - hence "2 ^ length (nat_to_bv n) \<le> n" 1.1541 - by simp 1.1542 + hence "2 ^ length (nat_to_bv n) \<le> n" by simp 1.1543 hence "length (nat_to_bv n) < length (nat_to_bv n)" 1.1544 by (rule length_nat_to_bv_lower_limit) 1.1545 - thus False 1.1546 - by simp 1.1547 + thus False by simp 1.1548 qed 1.1549 1.1550 lemma length_nat_0 [simp]: "length_nat 0 = 0" 1.1551 @@ -2281,8 +2081,8 @@ 1.1552 lemma length_int: "length (int_to_bv i) = length_int i" 1.1553 proof (cases "0 < i") 1.1554 assume i0: "0 < i" 1.1555 - hence "length (int_to_bv i) = length (norm_signed (\<zero> # norm_unsigned (nat_to_bv (nat i))))" 1.1556 - by simp 1.1557 + hence "length (int_to_bv i) = 1.1558 + length (norm_signed (\<zero> # norm_unsigned (nat_to_bv (nat i))))" by simp 1.1559 also from norm_unsigned_result [of "nat_to_bv (nat i)"] 1.1560 have "... = Suc (length_nat (nat i))" 1.1561 apply safe 1.1562 @@ -2303,19 +2103,16 @@ 1.1563 by (simp add: length_int_def) 1.1564 next 1.1565 assume "~ 0 < i" 1.1566 - hence i0: "i \<le> 0" 1.1567 - by simp 1.1568 + hence i0: "i \<le> 0" by simp 1.1569 show ?thesis 1.1570 proof (cases "i = 0") 1.1571 assume "i = 0" 1.1572 - thus ?thesis 1.1573 - by (simp add: length_int_def) 1.1574 + thus ?thesis by (simp add: length_int_def) 1.1575 next 1.1576 assume "i \<noteq> 0" 1.1577 - with i0 1.1578 - have i0: "i < 0" 1.1579 - by simp 1.1580 - hence "length (int_to_bv i) = length (norm_signed (\<one> # bv_not (norm_unsigned (nat_to_bv (nat (- i) - 1)))))" 1.1581 + with i0 have i0: "i < 0" by simp 1.1582 + hence "length (int_to_bv i) = 1.1583 + length (norm_signed (\<one> # bv_not (norm_unsigned (nat_to_bv (nat (- i) - 1)))))" 1.1584 by (simp add: int_to_bv_def nat_diff_distrib) 1.1585 also from norm_unsigned_result [of "nat_to_bv (nat (- i) - 1)"] 1.1586 have "... = Suc (length_nat (nat (- i) - 1))" 1.1587 @@ -2333,8 +2130,7 @@ 1.1588 done 1.1589 finally 1.1590 show ?thesis 1.1591 - using i0 1.1592 - by (simp add: length_int_def nat_diff_distrib del: int_to_bv_lt0) 1.1593 + using i0 by (simp add: length_int_def nat_diff_distrib del: int_to_bv_lt0) 1.1594 qed 1.1595 qed 1.1596 1.1597 @@ -2413,14 +2209,11 @@ 1.1598 shows "bv_to_int (bv_extend n b w) = bv_to_int w" 1.1599 proof (cases "bv_msb w") 1.1600 assume [simp]: "bv_msb w = \<zero>" 1.1601 - with a have [simp]: "b = \<zero>" 1.1602 - by simp 1.1603 - show ?thesis 1.1604 - by (simp add: bv_to_int_def) 1.1605 + with a have [simp]: "b = \<zero>" by simp 1.1606 + show ?thesis by (simp add: bv_to_int_def) 1.1607 next 1.1608 assume [simp]: "bv_msb w = \<one>" 1.1609 - with a have [simp]: "b = \<one>" 1.1610 - by simp 1.1611 + with a have [simp]: "b = \<one>" by simp 1.1612 show ?thesis 1.1613 apply (simp add: bv_to_int_def) 1.1614 apply (simp add: bv_extend_def) 1.1615 @@ -2447,26 +2240,21 @@ 1.1616 apply (cases "0 \<le> y") 1.1617 apply (induct y,simp_all) 1.1618 done 1.1619 - with xx 1.1620 - have "y < x" by simp 1.1621 - with xy 1.1622 - show False 1.1623 - by simp 1.1624 + with xx have "y < x" by simp 1.1625 + with xy show False by simp 1.1626 qed 1.1627 1.1628 lemma length_nat_mono_int [simp]: "x \<le> y ==> length_nat x \<le> length_nat y" 1.1629 - apply (rule length_nat_mono) 1.1630 - apply arith 1.1631 - done 1.1632 + by (rule length_nat_mono) arith 1.1633 1.1634 lemma length_nat_pos [simp,intro!]: "0 < x ==> 0 < length_nat x" 1.1635 by (simp add: length_nat_non0) 1.1636 1.1637 lemma length_int_mono_gt0: "[| 0 \<le> x ; x \<le> y |] ==> length_int x \<le> length_int y" 1.1638 - by (cases "x = 0",simp_all add: length_int_gt0 nat_le_eq_zle) 1.1639 + by (cases "x = 0") (simp_all add: length_int_gt0 nat_le_eq_zle) 1.1640 1.1641 -lemma length_int_mono_lt0: "[| x \<le> y ; y \<le> 0 |] ==> length_int y \<le> length_int x" apply (cases "y = 0",simp_all add: length_int_lt0) 1.1642 - done 1.1643 +lemma length_int_mono_lt0: "[| x \<le> y ; y \<le> 0 |] ==> length_int y \<le> length_int x" 1.1644 + by (cases "y = 0") (simp_all add: length_int_lt0) 1.1645 1.1646 lemmas [simp] = length_nat_non0 1.1647 1.1648 @@ -2475,18 +2263,21 @@ 1.1649 1.1650 consts 1.1651 fast_bv_to_nat_helper :: "[bit list, int] => int" 1.1652 - 1.1653 primrec 1.1654 fast_bv_to_nat_Nil: "fast_bv_to_nat_helper [] k = k" 1.1655 - fast_bv_to_nat_Cons: "fast_bv_to_nat_helper (b#bs) k = fast_bv_to_nat_helper bs (k BIT (bit_case bit.B0 bit.B1 b))" 1.1656 + fast_bv_to_nat_Cons: "fast_bv_to_nat_helper (b#bs) k = 1.1657 + fast_bv_to_nat_helper bs (k BIT (bit_case bit.B0 bit.B1 b))" 1.1658 1.1659 -lemma fast_bv_to_nat_Cons0: "fast_bv_to_nat_helper (\<zero>#bs) bin = fast_bv_to_nat_helper bs (bin BIT bit.B0)" 1.1660 +lemma fast_bv_to_nat_Cons0: "fast_bv_to_nat_helper (\<zero>#bs) bin = 1.1661 + fast_bv_to_nat_helper bs (bin BIT bit.B0)" 1.1662 by simp 1.1663 1.1664 -lemma fast_bv_to_nat_Cons1: "fast_bv_to_nat_helper (\<one>#bs) bin = fast_bv_to_nat_helper bs (bin BIT bit.B1)" 1.1665 +lemma fast_bv_to_nat_Cons1: "fast_bv_to_nat_helper (\<one>#bs) bin = 1.1666 + fast_bv_to_nat_helper bs (bin BIT bit.B1)" 1.1667 by simp 1.1668 1.1669 -lemma fast_bv_to_nat_def: "bv_to_nat bs == number_of (fast_bv_to_nat_helper bs Numeral.Pls)" 1.1670 +lemma fast_bv_to_nat_def: 1.1671 + "bv_to_nat bs == number_of (fast_bv_to_nat_helper bs Numeral.Pls)" 1.1672 proof (simp add: bv_to_nat_def) 1.1673 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)" 1.1674 apply (induct bs,simp) 1.1675 @@ -2547,7 +2338,7 @@ 1.1676 in map (split f) (zip (g w1) (g w2)))" 1.1677 1.1678 lemma bv_length_bv_mapzip [simp]: 1.1679 - "length (bv_mapzip f w1 w2) = max (length w1) (length w2)" 1.1680 + "length (bv_mapzip f w1 w2) = max (length w1) (length w2)" 1.1681 by (simp add: bv_mapzip_def Let_def split: split_max) 1.1682 1.1683 lemma bv_mapzip_Nil [simp]: "bv_mapzip f [] [] = []"