tuned proofs: avoid implicit prems;
authorwenzelm
Wed Jun 13 18:30:16 2007 +0200 (2007-06-13)
changeset 2337545cd7db985b3
parent 23374 a2f492c599e0
child 23376 53317a1ec8b2
tuned proofs: avoid implicit prems;
major cleanup of proofs/document;
src/HOL/Library/Word.thy
     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 [] [] = []"