# HG changeset patch
# User wenzelm
# Date 1181752216 -7200
# Node ID 45cd7db985b38ca2d698436b901f0b0172a0f214
# Parent  a2f492c599e09f8224b50a65711f4346b00d8ff7
tuned proofs: avoid implicit prems;
major cleanup of proofs/document;

diff -r a2f492c599e0 -r 45cd7db985b3 src/HOL/Library/Word.thy
--- a/src/HOL/Library/Word.thy	Wed Jun 13 18:30:15 2007 +0200
+++ b/src/HOL/Library/Word.thy	Wed Jun 13 18:30:16 2007 +0200
@@ -20,31 +20,28 @@
   shows       "max (f x) (f y) \<le> f (max x y)"
 proof -
   from mf and le_maxI1 [of x y]
-  have fx: "f x \<le> f (max x y)"
-    by (rule monoD)
+  have fx: "f x \<le> f (max x y)" by (rule monoD)
   from mf and le_maxI2 [of y x]
-  have fy: "f y \<le> f (max x y)"
-    by (rule monoD)
+  have fy: "f y \<le> f (max x y)" by (rule monoD)
   from fx and fy
-  show "max (f x) (f y) \<le> f (max x y)"
-    by auto
+  show "max (f x) (f y) \<le> f (max x y)" by auto
 qed
 
 declare zero_le_power [intro]
-    and zero_less_power [intro]
+  and zero_less_power [intro]
 
 lemma int_nat_two_exp: "2 ^ k = int (2 ^ k)"
   by (simp add: zpower_int [symmetric])
 
+
 subsection {* Bits *}
 
-datatype bit
-  = Zero ("\<zero>")
+datatype bit =
+    Zero ("\<zero>")
   | One ("\<one>")
 
 consts
   bitval :: "bit => nat"
-
 primrec
   "bitval \<zero> = 0"
   "bitval \<one> = 1"
@@ -84,16 +81,17 @@
   bitxor_one:  "(\<one> bitxor y) = (bitnot y)"
 
 lemma bitnot_bitnot [simp]: "(bitnot (bitnot b)) = b"
-  by (cases b,simp_all)
+  by (cases b) simp_all
 
 lemma bitand_cancel [simp]: "(b bitand b) = b"
-  by (cases b,simp_all)
+  by (cases b) simp_all
 
 lemma bitor_cancel [simp]: "(b bitor b) = b"
-  by (cases b,simp_all)
+  by (cases b) simp_all
 
 lemma bitxor_cancel [simp]: "(b bitxor b) = \<zero>"
-  by (cases b,simp_all)
+  by (cases b) simp_all
+
 
 subsection {* Bit Vectors *}
 
@@ -107,24 +105,19 @@
   shows   "P w"
 proof (cases w)
   assume "w = []"
-  thus ?thesis
-    by (rule empty)
+  thus ?thesis by (rule empty)
 next
   fix b bs
   assume [simp]: "w = b # bs"
   show "P w"
   proof (cases b)
     assume "b = \<zero>"
-    hence "w = \<zero> # bs"
-      by simp
-    thus ?thesis
-      by (rule zero)
+    hence "w = \<zero> # bs" by simp
+    thus ?thesis by (rule zero)
   next
     assume "b = \<one>"
-    hence "w = \<one> # bs"
-      by simp
-    thus ?thesis
-      by (rule one)
+    hence "w = \<one> # bs" by simp
+    thus ?thesis by (rule one)
   qed
 qed
 
@@ -133,11 +126,11 @@
   and     zero:  "!!bs. P bs ==> P (\<zero>#bs)"
   and     one:   "!!bs. P bs ==> P (\<one>#bs)"
   shows   "P w"
-proof (induct w,simp_all add: empty)
+proof (induct w, simp_all add: empty)
   fix b bs
-  assume [intro!]: "P bs"
-  show "P (b#bs)"
-    by (cases b,auto intro!: zero one)
+  assume "P bs"
+  then show "P (b#bs)"
+    by (cases b) (auto intro!: zero one)
 qed
 
 definition
@@ -162,7 +155,7 @@
   by (simp add: bv_not_def)
 
 lemma bv_not_bv_not [simp]: "bv_not (bv_not w) = w"
-  by (rule bit_list_induct [of _ w],simp_all)
+  by (rule bit_list_induct [of _ w]) simp_all
 
 lemma bv_msb_Nil [simp]: "bv_msb [] = \<zero>"
   by (simp add: bv_msb_def)
@@ -171,13 +164,13 @@
   by (simp add: bv_msb_def)
 
 lemma bv_msb_bv_not [simp]: "0 < length w ==> bv_msb (bv_not w) = (bitnot (bv_msb w))"
-  by (cases w,simp_all)
+  by (cases w) simp_all
 
 lemma bv_msb_one_length [simp,intro]: "bv_msb w = \<one> ==> 0 < length w"
-  by (cases w,simp_all)
+  by (cases w) simp_all
 
 lemma length_bv_not [simp]: "length (bv_not w) = length w"
-  by (induct w,simp_all)
+  by (induct w) simp_all
 
 definition
   bv_to_nat :: "bit list => nat" where
@@ -191,7 +184,8 @@
   let ?bv_to_nat' = "foldl (\<lambda>bn b. 2 * bn + bitval b)"
   have helper: "\<And>base. ?bv_to_nat' base bs = base * 2 ^ length bs + ?bv_to_nat' 0 bs"
   proof (induct bs)
-    case Nil show ?case by simp
+    case Nil
+    show ?case by simp
   next
     case (Cons x xs base)
     show ?case
@@ -212,26 +206,19 @@
   by simp
 
 lemma bv_to_nat_upper_range: "bv_to_nat w < 2 ^ length w"
-proof (induct w,simp_all)
+proof (induct w, simp_all)
   fix b bs
   assume "bv_to_nat bs < 2 ^ length bs"
   show "bitval b * 2 ^ length bs + bv_to_nat bs < 2 * 2 ^ length bs"
-  proof (cases b,simp_all)
-    have "bv_to_nat bs < 2 ^ length bs"
-      .
-    also have "... < 2 * 2 ^ length bs"
-      by auto
-    finally show "bv_to_nat bs < 2 * 2 ^ length bs"
-      by simp
+  proof (cases b, simp_all)
+    have "bv_to_nat bs < 2 ^ length bs" by fact
+    also have "... < 2 * 2 ^ length bs" by auto
+    finally show "bv_to_nat bs < 2 * 2 ^ length bs" by simp
   next
-    have "bv_to_nat bs < 2 ^ length bs"
-      .
-    hence "2 ^ length bs + bv_to_nat bs < 2 ^ length bs + 2 ^ length bs"
-      by arith
-    also have "... = 2 * (2 ^ length bs)"
-      by simp
-    finally show "bv_to_nat bs < 2 ^ length bs"
-      by simp
+    have "bv_to_nat bs < 2 ^ length bs" by fact
+    hence "2 ^ length bs + bv_to_nat bs < 2 ^ length bs + 2 ^ length bs" by arith
+    also have "... = 2 * (2 ^ length bs)" by simp
+    finally show "bv_to_nat bs < 2 ^ length bs" by simp
   qed
 qed
 
@@ -250,20 +237,18 @@
   have "bv_extend n b w = replicate (n - length w) b @ w"
     by (simp add: bv_extend_def)
   also have "... = replicate (n - Suc (length w) + 1) b @ w"
-    by (subst s,rule)
+    by (subst s) rule
   also have "... = (replicate (n - Suc (length w)) b @ replicate 1 b) @ w"
-    by (subst replicate_add,rule)
+    by (subst replicate_add) rule
   also have "... = replicate (n - Suc (length w)) b @ b # w"
     by simp
   also have "... = bv_extend n b (b#w)"
     by (simp add: bv_extend_def)
-  finally show "bv_extend n b w = bv_extend n b (b#w)"
-    .
+  finally show "bv_extend n b w = bv_extend n b (b#w)" .
 qed
 
 consts
   rem_initial :: "bit => bit list => bit list"
-
 primrec
   "rem_initial b [] = []"
   "rem_initial b (x#xs) = (if b = x then rem_initial b xs else x#xs)"
@@ -276,7 +261,7 @@
   shows      "rem_initial b w = w"
 proof -
   have "length (rem_initial b w) = length w --> rem_initial b w = w"
-  proof (induct w,simp_all,clarify)
+  proof (induct w, simp_all, clarify)
     fix xs
     assume "length (rem_initial b xs) = length xs --> rem_initial b xs = xs"
     assume f: "length (rem_initial b xs) = Suc (length xs)"
@@ -284,50 +269,42 @@
     show "rem_initial b xs = b#xs"
       by auto
   qed
-  thus ?thesis
-    ..
+  from this and p show ?thesis ..
 qed
 
 lemma bv_extend_rem_initial: "bv_extend (length w) b (rem_initial b w) = w"
-proof (induct w,simp_all,safe)
+proof (induct w, simp_all, safe)
   fix xs
   assume ind: "bv_extend (length xs) b (rem_initial b xs) = xs"
   from rem_initial_length [of b xs]
-  have [simp]: "Suc (length xs) - length (rem_initial b xs) = 1 + (length xs - length (rem_initial b xs))"
+  have [simp]: "Suc (length xs) - length (rem_initial b xs) =
+      1 + (length xs - length (rem_initial b xs))"
     by arith
-  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)"
+  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)"
     by (simp add: bv_extend_def)
-  also have "... = replicate (1 + (length xs - length (rem_initial b xs))) b @ rem_initial b xs"
+  also have "... =
+      replicate (1 + (length xs - length (rem_initial b xs))) b @ rem_initial b xs"
     by simp
-  also have "... = (replicate 1 b @ replicate (length xs - length (rem_initial b xs)) b) @ rem_initial b xs"
-    by (subst replicate_add,rule refl)
+  also have "... =
+      (replicate 1 b @ replicate (length xs - length (rem_initial b xs)) b) @ rem_initial b xs"
+    by (subst replicate_add) (rule refl)
   also have "... = b # bv_extend (length xs) b (rem_initial b xs)"
     by (auto simp add: bv_extend_def [symmetric])
   also have "... = b # xs"
     by (simp add: ind)
-  finally show "bv_extend (Suc (length xs)) b (rem_initial b xs) = b # xs"
-    .
+  finally show "bv_extend (Suc (length xs)) b (rem_initial b xs) = b # xs" .
 qed
 
 lemma rem_initial_append1:
   assumes "rem_initial b xs ~= []"
   shows   "rem_initial b (xs @ ys) = rem_initial b xs @ ys"
-proof -
-  have "rem_initial b xs ~= [] --> rem_initial b (xs @ ys) = rem_initial b xs @ ys" (is "?P xs ys")
-    by (induct xs,auto)
-  thus ?thesis
-    ..
-qed
+  using assms by (induct xs) auto
 
 lemma rem_initial_append2:
   assumes "rem_initial b xs = []"
   shows   "rem_initial b (xs @ ys) = rem_initial b ys"
-proof -
-  have "rem_initial b xs = [] --> rem_initial b (xs @ ys) = rem_initial b ys" (is "?P xs ys")
-    by (induct xs,auto)
-  thus ?thesis
-    ..
-qed
+  using assms by (induct xs) auto
 
 definition
   norm_unsigned :: "bit list => bit list" where
@@ -347,7 +324,6 @@
 
 consts
   nat_to_bv_helper :: "nat => bit list => bit list"
-
 recdef nat_to_bv_helper "measure (\<lambda>n. n)"
   "nat_to_bv_helper n = (%bs. (if n = 0 then bs
                                else nat_to_bv_helper (n div 2) ((if n mod 2 = 0 then \<zero> else \<one>)#bs)))"
@@ -367,17 +343,12 @@
   shows         "R"
 proof (cases "n = 0")
   assume "n = 0"
-  thus R
-    by (rule zero)
+  thus R by (rule zero)
 next
   assume "n ~= 0"
-  hence nn0: "0 < n"
-    by simp
-  hence "n div 2 < n"
-    by arith
-  from this and nn0
-  show R
-    by (rule div)
+  hence "0 < n" by simp
+  hence "n div 2 < n" by arith
+  from this and `0 < n` show R by (rule div)
 qed
 
 lemma int_wf_ge_induct:
@@ -387,7 +358,7 @@
   fix x
   assume ih: "(\<And>y\<Colon>int. (y, x) \<in> int_ge_less_than k \<Longrightarrow> P y)"
   thus "P x"
-    by (rule ind, simp add: int_ge_less_than_def) 
+    by (rule ind) (simp add: int_ge_less_than_def)
 qed
 
 lemma unfold_nat_to_bv_helper:
@@ -438,8 +409,7 @@
       qed
     qed
   qed
-  thus ?thesis
-    ..
+  thus ?thesis ..
 qed
 
 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>]"
@@ -478,8 +448,7 @@
       qed
     qed
   qed
-  thus ?thesis
-    ..
+  thus ?thesis ..
 qed
 
 lemma bv_nat_bv [simp]: "bv_to_nat (nat_to_bv n) = n"
@@ -488,17 +457,14 @@
   assume ind: "!!j. j < n \<Longrightarrow> bv_to_nat (nat_to_bv j) = j"
   show "bv_to_nat (nat_to_bv n) = n"
   proof (rule n_div_2_cases [of n])
-    assume [simp]: "n = 0"
-    show ?thesis
-      by simp
+    assume "n = 0"
+    then show ?thesis by simp
   next
     assume nn: "n div 2 < n"
     assume n0: "0 < n"
     from ind and nn
-    have ind': "bv_to_nat (nat_to_bv (n div 2)) = n div 2"
-      by blast
-    from n0 have n0': "n \<noteq> 0"
-      by simp
+    have ind': "bv_to_nat (nat_to_bv (n div 2)) = n div 2" by blast
+    from n0 have n0': "n \<noteq> 0" by simp
     show ?thesis
       apply (subst nat_to_bv_def)
       apply (simp only: nat_to_bv_helper.simps [of n])
@@ -523,13 +489,13 @@
 qed
 
 lemma bv_to_nat_type [simp]: "bv_to_nat (norm_unsigned w) = bv_to_nat w"
-  by (rule bit_list_induct,simp_all)
+  by (rule bit_list_induct) simp_all
 
 lemma length_norm_unsigned_le [simp]: "length (norm_unsigned w) \<le> length w"
-  by (rule bit_list_induct,simp_all)
+  by (rule bit_list_induct) simp_all
 
 lemma bv_to_nat_rew_msb: "bv_msb w = \<one> ==> bv_to_nat w = 2 ^ (length w - 1) + bv_to_nat (tl w)"
-  by (rule bit_list_cases [of w],simp_all)
+  by (rule bit_list_cases [of w]) simp_all
 
 lemma norm_unsigned_result: "norm_unsigned xs = [] \<or> bv_msb (norm_unsigned xs) = \<one>"
 proof (rule length_induct [of _ xs])
@@ -540,10 +506,8 @@
     fix bs
     assume [simp]: "xs = \<zero>#bs"
     from ind
-    have "length bs < length xs --> norm_unsigned bs = [] \<or> bv_msb (norm_unsigned bs) = \<one>"
-      ..
-    thus "norm_unsigned bs = [] \<or> bv_msb (norm_unsigned bs) = \<one>"
-      by simp
+    have "length bs < length xs --> norm_unsigned bs = [] \<or> bv_msb (norm_unsigned bs) = \<one>" ..
+    thus "norm_unsigned bs = [] \<or> bv_msb (norm_unsigned bs) = \<one>" by simp
   qed
 qed
 
@@ -551,26 +515,22 @@
   assumes nw: "norm_unsigned w = []"
   shows       "bv_to_nat w = 0"
 proof -
-  have "bv_to_nat w = bv_to_nat (norm_unsigned w)"
-    by simp
-  also have "... = bv_to_nat []"
-    by (subst nw,rule)
-  also have "... = 0"
-    by simp
+  have "bv_to_nat w = bv_to_nat (norm_unsigned w)" by simp
+  also have "... = bv_to_nat []" by (subst nw) (rule refl)
+  also have "... = 0" by simp
   finally show ?thesis .
 qed
 
 lemma bv_to_nat_lower_limit:
   assumes w0: "0 < bv_to_nat w"
-  shows         "2 ^ (length (norm_unsigned w) - 1) \<le> bv_to_nat w"
+  shows "2 ^ (length (norm_unsigned w) - 1) \<le> bv_to_nat w"
 proof -
   from w0 and norm_unsigned_result [of w]
   have msbw: "bv_msb (norm_unsigned w) = \<one>"
     by (auto simp add: norm_empty_bv_to_nat_zero)
   have "2 ^ (length (norm_unsigned w) - 1) \<le> bv_to_nat (norm_unsigned w)"
     by (subst bv_to_nat_rew_msb [OF msbw],simp)
-  thus ?thesis
-    by simp
+  thus ?thesis by simp
 qed
 
 lemmas [simp del] = nat_to_bv_non0
@@ -584,25 +544,21 @@
 lemma bv_extend_norm_unsigned: "bv_extend (length w) \<zero> (norm_unsigned w) = w"
   by (simp add: norm_unsigned_def,rule bv_extend_rem_initial)
 
-lemma norm_unsigned_append1 [simp]: "norm_unsigned xs \<noteq> [] ==> norm_unsigned (xs @ ys) = norm_unsigned xs @ ys"
+lemma norm_unsigned_append1 [simp]:
+    "norm_unsigned xs \<noteq> [] ==> norm_unsigned (xs @ ys) = norm_unsigned xs @ ys"
   by (simp add: norm_unsigned_def,rule rem_initial_append1)
 
-lemma norm_unsigned_append2 [simp]: "norm_unsigned xs = [] ==> norm_unsigned (xs @ ys) = norm_unsigned ys"
+lemma norm_unsigned_append2 [simp]:
+    "norm_unsigned xs = [] ==> norm_unsigned (xs @ ys) = norm_unsigned ys"
   by (simp add: norm_unsigned_def,rule rem_initial_append2)
 
-lemma bv_to_nat_zero_imp_empty [rule_format]:
-  "bv_to_nat w = 0 \<longrightarrow> norm_unsigned w = []"
-  by (rule bit_list_induct [of _ w],simp_all)
+lemma bv_to_nat_zero_imp_empty:
+    "bv_to_nat w = 0 \<Longrightarrow> norm_unsigned w = []"
+  by (atomize (full), induct w rule: bit_list_induct) simp_all
 
 lemma bv_to_nat_nzero_imp_nempty:
-  assumes "bv_to_nat w \<noteq> 0"
-  shows   "norm_unsigned w \<noteq> []"
-proof -
-  have "bv_to_nat w \<noteq> 0 --> norm_unsigned w \<noteq> []"
-    by (rule bit_list_induct [of _ w],simp_all)
-  thus ?thesis
-    ..
-qed
+  "bv_to_nat w \<noteq> 0 \<Longrightarrow> norm_unsigned w \<noteq> []"
+  by (induct w rule: bit_list_induct) simp_all
 
 lemma nat_helper1:
   assumes ass: "nat_to_bv (bv_to_nat w) = norm_unsigned w"
@@ -622,22 +578,21 @@
     also have "... = 1"
       by (subst mod_add1_eq) simp
     finally have eq1: "?lhs = 1" .
-    have "?rhs  = 0"
-      by simp
+    have "?rhs  = 0" by simp
     with orig and eq1
     show "nat_to_bv (Suc (2 * bv_to_nat w) div 2) @ [\<zero>] = norm_unsigned (w @ [\<one>])"
       by simp
   next
-    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>]"
+    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>]"
       by (simp add: add_commute)
     also have "... = nat_to_bv (bv_to_nat w) @ [\<one>]"
-      by (subst div_add1_eq,simp)
+      by (subst div_add1_eq) simp
     also have "... = norm_unsigned w @ [\<one>]"
-      by (subst ass,rule refl)
+      by (subst ass) (rule refl)
     also have "... = norm_unsigned (w @ [\<one>])"
-      by (cases "norm_unsigned w",simp_all)
-    finally show "nat_to_bv (Suc (2 * bv_to_nat w) div 2) @ [\<one>] = norm_unsigned (w @ [\<one>])"
-      .
+      by (cases "norm_unsigned w") simp_all
+    finally show "nat_to_bv (Suc (2 * bv_to_nat w) div 2) @ [\<one>] = norm_unsigned (w @ [\<one>])" .
   qed
 next
   assume [simp]: "x = \<zero>"
@@ -671,9 +626,8 @@
       assume ind: "\<forall>ys. length ys < length xs --> ?P ys"
       show "?P xs"
       proof (cases xs)
-        assume [simp]: "xs = []"
-        show ?thesis
-          by (simp add: nat_to_bv_non0)
+        assume "xs = []"
+        then show ?thesis by (simp add: nat_to_bv_non0)
       next
         fix y ys
         assume [simp]: "xs = y # ys"
@@ -703,24 +657,22 @@
             by simp
           also have "... = \<one> # rev ys @ [y]"
             by simp
-          finally show "nat_to_bv (2 * 2 ^ length ys + (bv_to_nat (rev ys) * 2 + bitval y)) = \<one> # rev ys @ [y]"
-            .
+          finally show "nat_to_bv (2 * 2 ^ length ys + (bv_to_nat (rev ys) * 2 + bitval y)) =
+	      \<one> # rev ys @ [y]" .
         qed
       qed
     qed
   qed
-  hence "nat_to_bv (2 ^ length (rev (rev xs)) + bv_to_nat (rev (rev xs))) = \<one> # rev (rev xs)"
-    ..
-  thus ?thesis
-    by simp
+  hence "nat_to_bv (2 ^ length (rev (rev xs)) + bv_to_nat (rev (rev xs))) =
+      \<one> # rev (rev xs)" ..
+  thus ?thesis by simp
 qed
 
 lemma nat_bv_nat [simp]: "nat_to_bv (bv_to_nat w) = norm_unsigned w"
 proof (rule bit_list_induct [of _ w],simp_all)
   fix xs
   assume "nat_to_bv (bv_to_nat xs) = norm_unsigned xs"
-  have "bv_to_nat xs = bv_to_nat (norm_unsigned xs)"
-    by simp
+  have "bv_to_nat xs = bv_to_nat (norm_unsigned xs)" by simp
   have "bv_to_nat xs < 2 ^ length xs"
     by (rule bv_to_nat_upper_range)
   show "nat_to_bv (2 ^ length xs + bv_to_nat xs) = \<one> # xs"
@@ -750,9 +702,8 @@
   "norm_unsigned (nat_to_bv n) = nat_to_bv n"
 proof -
   have "norm_unsigned (nat_to_bv n) = nat_to_bv (bv_to_nat (norm_unsigned (nat_to_bv n)))"
-    by (subst nat_bv_nat,simp)
-  also have "... = nat_to_bv n"
-    by simp
+    by (subst nat_bv_nat) simp
+  also have "... = nat_to_bv n" by simp
   finally show ?thesis .
 qed
 
@@ -769,25 +720,16 @@
   show ?thesis
   proof (rule ccontr)
     assume "~ length (nat_to_bv n) \<le> k"
-    hence "k < length (nat_to_bv n)"
-      by simp
-    hence "k \<le> length (nat_to_bv n) - 1"
-      by arith
-    hence "(2::nat) ^ k \<le> 2 ^ (length (nat_to_bv n) - 1)"
-      by simp
-    also have "... = 2 ^ (length (norm_unsigned (nat_to_bv n)) - 1)"
-      by simp
+    hence "k < length (nat_to_bv n)" by simp
+    hence "k \<le> length (nat_to_bv n) - 1" by arith
+    hence "(2::nat) ^ k \<le> 2 ^ (length (nat_to_bv n) - 1)" by simp
+    also have "... = 2 ^ (length (norm_unsigned (nat_to_bv n)) - 1)" by simp
     also have "... \<le> bv_to_nat (nat_to_bv n)"
-      by (rule bv_to_nat_lower_limit,simp add: n0)
-    also have "... = n"
-      by simp
+      by (rule bv_to_nat_lower_limit) (simp add: n0)
+    also have "... = n" by simp
     finally have "2 ^ k \<le> n" .
-    with n0
-    have "2 ^ k - 1 < n"
-      by arith
-    with nk
-    show False
-      by simp
+    with n0 have "2 ^ k - 1 < n" by arith
+    with nk show False by simp
   qed
 qed
 
@@ -796,20 +738,16 @@
   shows       "k < length (nat_to_bv n)"
 proof (rule ccontr)
   assume "~ k < length (nat_to_bv n)"
-  hence lnk: "length (nat_to_bv n) \<le> k"
-    by simp
-  have "n = bv_to_nat (nat_to_bv n)"
-    by simp
+  hence lnk: "length (nat_to_bv n) \<le> k" by simp
+  have "n = bv_to_nat (nat_to_bv n)" by simp
   also have "... < 2 ^ length (nat_to_bv n)"
     by (rule bv_to_nat_upper_range)
-  also from lnk have "... \<le> 2 ^ k"
-    by simp
+  also from lnk have "... \<le> 2 ^ k" by simp
   finally have "n < 2 ^ k" .
-  with nk
-  show False
-    by simp
+  with nk show False by simp
 qed
 
+
 subsection {* Unsigned Arithmetic Operations *}
 
 definition
@@ -830,17 +768,15 @@
   from bv_to_nat_upper_range [of w1] and bv_to_nat_upper_range [of w2]
   have "bv_to_nat w1 + bv_to_nat w2 \<le> (2 ^ length w1 - 1) + (2 ^ length w2 - 1)"
     by arith
-  also have "... \<le> max (2 ^ length w1 - 1) (2 ^ length w2 - 1) + max (2 ^ length w1 - 1) (2 ^ length w2 - 1)"
+  also have "... \<le>
+      max (2 ^ length w1 - 1) (2 ^ length w2 - 1) + max (2 ^ length w1 - 1) (2 ^ length w2 - 1)"
     by (rule add_mono,safe intro!: le_maxI1 le_maxI2)
-  also have "... = 2 * max (2 ^ length w1 - 1) (2 ^ length w2 - 1)"
-    by simp
+  also have "... = 2 * max (2 ^ length w1 - 1) (2 ^ length w2 - 1)" by simp
   also have "... \<le> 2 ^ Suc (max (length w1) (length w2)) - 2"
   proof (cases "length w1 \<le> length w2")
     assume w1w2: "length w1 \<le> length w2"
-    hence "(2::nat) ^ length w1 \<le> 2 ^ length w2"
-      by simp
-    hence "(2::nat) ^ length w1 - 1 \<le> 2 ^ length w2 - 1"
-      by arith
+    hence "(2::nat) ^ length w1 \<le> 2 ^ length w2" by simp
+    hence "(2::nat) ^ length w1 - 1 \<le> 2 ^ length w2 - 1" by arith
     with w1w2 show ?thesis
       by (simp add: diff_mult_distrib2 split: split_max)
   next
@@ -850,12 +786,9 @@
       assume "(2::nat) ^ length w1 - 1 \<le> 2 ^ length w2 - 1"
       hence "((2::nat) ^ length w1 - 1) + 1 \<le> (2 ^ length w2 - 1) + 1"
         by (rule add_right_mono)
-      hence "(2::nat) ^ length w1 \<le> 2 ^ length w2"
-        by simp
-      hence "length w1 \<le> length w2"
-        by simp
-      thus False
-        by simp
+      hence "(2::nat) ^ length w1 \<le> 2 ^ length w2" by simp
+      hence "length w1 \<le> length w2" by simp
+      thus False by simp
     qed
     thus ?thesis
       by (simp add: diff_mult_distrib2 split: split_max)
@@ -899,10 +832,12 @@
 
 consts
   norm_signed :: "bit list => bit list"
-
 primrec
   norm_signed_Nil: "norm_signed [] = []"
-  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)"
+  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)"
 
 lemma norm_signed0 [simp]: "norm_signed [\<zero>] = []"
   by simp
@@ -933,27 +868,30 @@
 lemma int_to_bv_ge0 [simp]: "0 \<le> n ==> int_to_bv n = norm_signed (\<zero> # nat_to_bv (nat n))"
   by (simp add: int_to_bv_def)
 
-lemma int_to_bv_lt0 [simp]: "n < 0 ==> int_to_bv n = norm_signed (bv_not (\<zero>#nat_to_bv (nat (-n- 1))))"
+lemma int_to_bv_lt0 [simp]:
+    "n < 0 ==> int_to_bv n = norm_signed (bv_not (\<zero>#nat_to_bv (nat (-n- 1))))"
   by (simp add: int_to_bv_def)
 
 lemma norm_signed_idem [simp]: "norm_signed (norm_signed w) = norm_signed w"
-proof (rule bit_list_induct [of _ w],simp_all)
+proof (rule bit_list_induct [of _ w], simp_all)
   fix xs
-  assume "norm_signed (norm_signed xs) = norm_signed xs"
+  assume eq: "norm_signed (norm_signed xs) = norm_signed xs"
   show "norm_signed (norm_signed (\<zero>#xs)) = norm_signed (\<zero>#xs)"
   proof (rule bit_list_cases [of xs],simp_all)
     fix ys
-    assume [symmetric,simp]: "xs = \<zero>#ys"
+    assume "xs = \<zero>#ys"
+    from this [symmetric] and eq
     show "norm_signed (norm_signed (\<zero>#ys)) = norm_signed (\<zero>#ys)"
       by simp
   qed
 next
   fix xs
-  assume "norm_signed (norm_signed xs) = norm_signed xs"
+  assume eq: "norm_signed (norm_signed xs) = norm_signed xs"
   show "norm_signed (norm_signed (\<one>#xs)) = norm_signed (\<one>#xs)"
   proof (rule bit_list_cases [of xs],simp_all)
     fix ys
-    assume [symmetric,simp]: "xs = \<one>#ys"
+    assume "xs = \<one>#ys"
+    from this [symmetric] and eq
     show "norm_signed (norm_signed (\<one>#ys)) = norm_signed (\<one>#ys)"
       by simp
   qed
@@ -975,11 +913,11 @@
   by (simp add: bv_to_int_def)
 
 lemma bv_to_int_type [simp]: "bv_to_int (norm_signed w) = bv_to_int w"
-proof (rule bit_list_induct [of _ w],simp_all)
+proof (rule bit_list_induct [of _ w], simp_all)
   fix xs
   assume ind: "bv_to_int (norm_signed xs) = bv_to_int xs"
   show "bv_to_int (norm_signed (\<zero>#xs)) = int (bv_to_nat xs)"
-  proof (rule bit_list_cases [of xs],simp_all)
+  proof (rule bit_list_cases [of xs], simp_all)
     fix ys
     assume [simp]: "xs = \<zero>#ys"
     from ind
@@ -990,7 +928,7 @@
   fix xs
   assume ind: "bv_to_int (norm_signed xs) = bv_to_int xs"
   show "bv_to_int (norm_signed (\<one>#xs)) = - int (bv_to_nat (bv_not xs)) + -1"
-  proof (rule bit_list_cases [of xs],simp_all)
+  proof (rule bit_list_cases [of xs], simp_all)
     fix ys
     assume [simp]: "xs = \<one>#ys"
     from ind
@@ -1007,23 +945,17 @@
     by (simp add: int_nat_two_exp)
 next
   fix bs
-  have "- int (bv_to_nat (bv_not bs)) + -1 \<le> 0"
-    by simp
-  also have "... < 2 ^ length bs"
-    by (induct bs,simp_all)
-  finally show "- int (bv_to_nat (bv_not bs)) + -1 < 2 ^ length bs"
-    .
+  have "- int (bv_to_nat (bv_not bs)) + -1 \<le> 0" by simp
+  also have "... < 2 ^ length bs" by (induct bs) simp_all
+  finally show "- int (bv_to_nat (bv_not bs)) + -1 < 2 ^ length bs" .
 qed
 
 lemma bv_to_int_lower_range: "- (2 ^ (length w - 1)) \<le> bv_to_int w"
 proof (rule bit_list_cases [of w],simp_all)
   fix bs :: "bit list"
-  have "- (2 ^ length bs) \<le> (0::int)"
-    by (induct bs,simp_all)
-  also have "... \<le> int (bv_to_nat bs)"
-    by simp
-  finally show "- (2 ^ length bs) \<le> int (bv_to_nat bs)"
-    .
+  have "- (2 ^ length bs) \<le> (0::int)" by (induct bs) simp_all
+  also have "... \<le> int (bv_to_nat bs)" by simp
+  finally show "- (2 ^ length bs) \<le> int (bv_to_nat bs)" .
 next
   fix bs
   from bv_to_nat_upper_range [of "bv_not bs"]
@@ -1063,20 +995,20 @@
 qed
 
 lemma bv_int_bv [simp]: "bv_to_int (int_to_bv i) = i"
-  by (cases "0 \<le> i",simp_all)
+  by (cases "0 \<le> i") simp_all
 
 lemma bv_msb_norm [simp]: "bv_msb (norm_signed w) = bv_msb w"
-  by (rule bit_list_cases [of w],simp_all add: norm_signed_Cons)
+  by (rule bit_list_cases [of w]) (simp_all add: norm_signed_Cons)
 
 lemma norm_signed_length: "length (norm_signed w) \<le> length w"
-  apply (cases w,simp_all)
+  apply (cases w, simp_all)
   apply (subst norm_signed_Cons)
-  apply (case_tac "a",simp_all)
+  apply (case_tac a, simp_all)
   apply (rule rem_initial_length)
   done
 
 lemma norm_signed_equal: "length (norm_signed w) = length w ==> norm_signed w = w"
-proof (rule bit_list_cases [of w],simp_all)
+proof (rule bit_list_cases [of w], simp_all)
   fix xs
   assume "length (norm_signed (\<zero>#xs)) = Suc (length xs)"
   thus "norm_signed (\<zero>#xs) = \<zero>#xs"
@@ -1135,18 +1067,13 @@
   shows        "xs = ys"
 proof -
   from one
-  have "int_to_bv (bv_to_int xs) = int_to_bv (bv_to_int ys)"
-    by simp
-  hence xsys: "norm_signed xs = norm_signed ys"
-    by simp
+  have "int_to_bv (bv_to_int xs) = int_to_bv (bv_to_int ys)" by simp
+  hence xsys: "norm_signed xs = norm_signed ys" by simp
   hence xsys': "bv_msb xs = bv_msb ys"
   proof -
-    have "bv_msb xs = bv_msb (norm_signed xs)"
-      by simp
-    also have "... = bv_msb (norm_signed ys)"
-      by (simp add: xsys)
-    also have "... = bv_msb ys"
-      by simp
+    have "bv_msb xs = bv_msb (norm_signed xs)" by simp
+    also have "... = bv_msb (norm_signed ys)" by (simp add: xsys)
+    also have "... = bv_msb ys" by simp
     finally show ?thesis .
   qed
   have "xs = bv_extend (length xs) (bv_msb xs) (norm_signed xs)"
@@ -1172,25 +1099,20 @@
   shows       "2 ^ (length (norm_signed w) - 2) \<le> bv_to_int w"
 proof -
   from w0
-  have "0 \<le> bv_to_int w"
-    by simp
-  hence [simp]: "bv_msb w = \<zero>"
-    by (rule bv_to_int_msb0)
+  have "0 \<le> bv_to_int w" by simp
+  hence [simp]: "bv_msb w = \<zero>" by (rule bv_to_int_msb0)
   have "2 ^ (length (norm_signed w) - 2) \<le> bv_to_int (norm_signed w)"
   proof (rule bit_list_cases [of w])
     assume "w = []"
-    with w0
-    show ?thesis
-      by simp
+    with w0 show ?thesis by simp
   next
     fix w'
     assume weq: "w = \<zero> # w'"
     thus ?thesis
     proof (simp add: norm_signed_Cons,safe)
       assume "norm_unsigned w' = []"
-      with weq and w0
-      show False
-        by (simp add: norm_empty_bv_to_nat_zero)
+      with weq and w0 show False
+	by (simp add: norm_empty_bv_to_nat_zero)
     next
       assume w'0: "norm_unsigned w' \<noteq> []"
       have "0 < bv_to_nat w'"
@@ -1201,8 +1123,7 @@
         hence "norm_unsigned w' = []"
           by (simp add: bv_to_nat_zero_imp_empty)
         with w'0
-        show False
-          by simp
+        show False by simp
       qed
       with bv_to_nat_lower_limit [of w']
       show "2 ^ (length (norm_unsigned w') - Suc 0) \<le> int (bv_to_nat w')"
@@ -1211,15 +1132,10 @@
   next
     fix w'
     assume "w = \<one> # w'"
-    from w0
-    have "bv_msb w = \<zero>"
-      by simp
-    with prems
-    show ?thesis
-      by simp
+    from w0 have "bv_msb w = \<zero>" by simp
+    with prems show ?thesis by simp
   qed
-  also have "...  = bv_to_int w"
-    by simp
+  also have "...  = bv_to_int w" by simp
   finally show ?thesis .
 qed
 
@@ -1235,19 +1151,14 @@
   assume msb: "\<zero> = bv_msb (norm_unsigned l)"
   assume "norm_unsigned l \<noteq> []"
   with norm_unsigned_result [of l]
-  have "bv_msb (norm_unsigned l) = \<one>"
-    by simp
-  with msb
-  show False
-    by simp
+  have "bv_msb (norm_unsigned l) = \<one>" by simp
+  with msb show False by simp
 next
   fix xs
   assume p: "\<one> = bv_msb (tl (norm_signed (\<one> # xs)))"
   have "\<one> \<noteq> bv_msb (tl (norm_signed (\<one> # xs)))"
     by (rule bit_list_induct [of _ xs],simp_all)
-  with p
-  show False
-    by simp
+  with p show False by simp
 qed
 
 lemma bv_to_int_upper_limit_lem1:
@@ -1255,61 +1166,41 @@
   shows       "bv_to_int w < - (2 ^ (length (norm_signed w) - 2))"
 proof -
   from w0
-  have "bv_to_int w < 0"
-    by simp
+  have "bv_to_int w < 0" by simp
   hence msbw [simp]: "bv_msb w = \<one>"
     by (rule bv_to_int_msb1)
-  have "bv_to_int w = bv_to_int (norm_signed w)"
-    by simp
+  have "bv_to_int w = bv_to_int (norm_signed w)" by simp
   also from norm_signed_result [of w]
   have "... < - (2 ^ (length (norm_signed w) - 2))"
-  proof (safe)
+  proof safe
     assume "norm_signed w = []"
-    hence "bv_to_int (norm_signed w) = 0"
-      by simp
-    with w0
-    show ?thesis
-      by simp
+    hence "bv_to_int (norm_signed w) = 0" by simp
+    with w0 show ?thesis by simp
   next
     assume "norm_signed w = [\<one>]"
-    hence "bv_to_int (norm_signed w) = -1"
-      by simp
-    with w0
-    show ?thesis
-      by simp
+    hence "bv_to_int (norm_signed w) = -1" by simp
+    with w0 show ?thesis by simp
   next
     assume "bv_msb (norm_signed w) \<noteq> bv_msb (tl (norm_signed w))"
-    hence msb_tl: "\<one> \<noteq> bv_msb (tl (norm_signed w))"
-      by simp
+    hence msb_tl: "\<one> \<noteq> bv_msb (tl (norm_signed w))" by simp
     show "bv_to_int (norm_signed w) < - (2 ^ (length (norm_signed w) - 2))"
     proof (rule bit_list_cases [of "norm_signed w"])
       assume "norm_signed w = []"
-      hence "bv_to_int (norm_signed w) = 0"
-        by simp
-      with w0
-      show ?thesis
-        by simp
+      hence "bv_to_int (norm_signed w) = 0" by simp
+      with w0 show ?thesis by simp
     next
       fix w'
       assume nw: "norm_signed w = \<zero> # w'"
-      from msbw
-      have "bv_msb (norm_signed w) = \<one>"
-        by simp
-      with nw
-      show ?thesis
-        by simp
+      from msbw have "bv_msb (norm_signed w) = \<one>" by simp
+      with nw show ?thesis by simp
     next
       fix w'
       assume weq: "norm_signed w = \<one> # w'"
       show ?thesis
       proof (rule bit_list_cases [of w'])
         assume w'eq: "w' = []"
-        from w0
-        have "bv_to_int (norm_signed w) < -1"
-          by simp
-        with w'eq and weq
-        show ?thesis
-          by simp
+        from w0 have "bv_to_int (norm_signed w) < -1" by simp
+        with w'eq and weq show ?thesis by simp
       next
         fix w''
         assume w'eq: "w' = \<zero> # w''"
@@ -1323,9 +1214,7 @@
       next
         fix w''
         assume w'eq: "w' = \<one> # w''"
-        with weq and msb_tl
-        show ?thesis
-          by simp
+        with weq and msb_tl show ?thesis by simp
       qed
     qed
   qed
@@ -1341,28 +1230,20 @@
   have k1: "1 < k"
     by (cases "k - 1",simp_all)
   assume "~ length (int_to_bv i) \<le> k"
-  hence "k < length (int_to_bv i)"
-    by simp
-  hence "k \<le> length (int_to_bv i) - 1"
-    by arith
-  hence a: "k - 1 \<le> length (int_to_bv i) - 2"
-    by arith
+  hence "k < length (int_to_bv i)" by simp
+  hence "k \<le> length (int_to_bv i) - 1" by arith
+  hence a: "k - 1 \<le> length (int_to_bv i) - 2" by arith
   hence "(2::int) ^ (k - 1) \<le> 2 ^ (length (int_to_bv i) - 2)" by simp
   also have "... \<le> i"
   proof -
     have "2 ^ (length (norm_signed (int_to_bv i)) - 2) \<le> bv_to_int (int_to_bv i)"
     proof (rule bv_to_int_lower_limit_gt0)
-      from w0
-      show "0 < bv_to_int (int_to_bv i)"
-        by simp
+      from w0 show "0 < bv_to_int (int_to_bv i)" by simp
     qed
-    thus ?thesis
-      by simp
+    thus ?thesis by simp
   qed
   finally have "2 ^ (k - 1) \<le> i" .
-  with wk
-  show False
-    by simp
+  with wk show False by simp
 qed
 
 lemma pos_length_pos:
@@ -1373,26 +1254,21 @@
   have "0 < length (norm_signed w)"
   proof (auto)
     assume ii: "norm_signed w = []"
-    have "bv_to_int (norm_signed w) = 0"
-      by (subst ii,simp)
-    hence "bv_to_int w = 0"
-      by simp
-    with i0
-    show False
-      by simp
+    have "bv_to_int (norm_signed w) = 0" by (subst ii) simp
+    hence "bv_to_int w = 0" by simp
+    with i0 show False by simp
   next
     assume ii: "norm_signed w = []"
     assume jj: "bv_msb w \<noteq> \<zero>"
     have "\<zero> = bv_msb (norm_signed w)"
-      by (subst ii,simp)
+      by (subst ii) simp
     also have "... \<noteq> \<zero>"
       by (simp add: jj)
     finally show False by simp
   qed
   also have "... \<le> length w"
     by (rule norm_signed_length)
-  finally show ?thesis
-    .
+  finally show ?thesis .
 qed
 
 lemma neg_length_pos:
@@ -1404,25 +1280,19 @@
   proof (auto)
     assume ii: "norm_signed w = []"
     have "bv_to_int (norm_signed w) = 0"
-      by (subst ii,simp)
-    hence "bv_to_int w = 0"
-      by simp
-    with i0
-    show False
-      by simp
+      by (subst ii) simp
+    hence "bv_to_int w = 0" by simp
+    with i0 show False by simp
   next
     assume ii: "norm_signed w = []"
     assume jj: "bv_msb w \<noteq> \<zero>"
-    have "\<zero> = bv_msb (norm_signed w)"
-      by (subst ii,simp)
-    also have "... \<noteq> \<zero>"
-      by (simp add: jj)
+    have "\<zero> = bv_msb (norm_signed w)" by (subst ii) simp
+    also have "... \<noteq> \<zero>" by (simp add: jj)
     finally show False by simp
   qed
   also have "... \<le> length w"
     by (rule norm_signed_length)
-  finally show ?thesis
-    .
+  finally show ?thesis .
 qed
 
 lemma length_int_to_bv_lower_limit_gt0:
@@ -1430,18 +1300,15 @@
   shows       "k < length (int_to_bv i)"
 proof (rule ccontr)
   have "0 < (2::int) ^ (k - 1)"
-    by (rule zero_less_power,simp)
-  also have "... \<le> i"
-    by (rule wk)
-  finally have i0: "0 < i"
-    .
+    by (rule zero_less_power) simp
+  also have "... \<le> i" by (rule wk)
+  finally have i0: "0 < i" .
   have lii0: "0 < length (int_to_bv i)"
     apply (rule pos_length_pos)
     apply (simp,rule i0)
     done
   assume "~ k < length (int_to_bv i)"
-  hence "length (int_to_bv i) \<le> k"
-    by simp
+  hence "length (int_to_bv i) \<le> k" by simp
   with lii0
   have a: "length (int_to_bv i) - 1 \<le> k - 1"
     by arith
@@ -1454,11 +1321,9 @@
     finally show ?thesis .
   qed
   also have "(2::int) ^ (length (int_to_bv i) - 1) \<le> 2 ^ (k - 1)" using a
-         by simp
+    by simp
   finally have "i < 2 ^ (k - 1)" .
-  with wk
-  show False
-    by simp
+  with wk show False by simp
 qed
 
 lemma length_int_to_bv_upper_limit_lem1:
@@ -1467,15 +1332,11 @@
   shows       "length (int_to_bv i) \<le> k"
 proof (rule ccontr)
   from w1 wk
-  have k1: "1 < k"
-    by (cases "k - 1",simp_all)
+  have k1: "1 < k" by (cases "k - 1") simp_all
   assume "~ length (int_to_bv i) \<le> k"
-  hence "k < length (int_to_bv i)"
-    by simp
-  hence "k \<le> length (int_to_bv i) - 1"
-    by arith
-  hence a: "k - 1 \<le> length (int_to_bv i) - 2"
-    by arith
+  hence "k < length (int_to_bv i)" by simp
+  hence "k \<le> length (int_to_bv i) - 1" by arith
+  hence a: "k - 1 \<le> length (int_to_bv i) - 2" by arith
   have "i < - (2 ^ (length (int_to_bv i) - 2))"
   proof -
     have "i = bv_to_int (int_to_bv i)"
@@ -1486,46 +1347,36 @@
   qed
   also have "... \<le> -(2 ^ (k - 1))"
   proof -
-    have "(2::int) ^ (k - 1) \<le> 2 ^ (length (int_to_bv i) - 2)" using a
-      by simp
-    thus ?thesis
-      by simp
+    have "(2::int) ^ (k - 1) \<le> 2 ^ (length (int_to_bv i) - 2)" using a by simp
+    thus ?thesis by simp
   qed
   finally have "i < -(2 ^ (k - 1))" .
-  with wk
-  show False
-    by simp
+  with wk show False by simp
 qed
 
 lemma length_int_to_bv_lower_limit_lem1:
   assumes wk: "i < -(2 ^ (k - 1))"
   shows       "k < length (int_to_bv i)"
 proof (rule ccontr)
-  from wk
-  have "i \<le> -(2 ^ (k - 1)) - 1"
-    by simp
+  from wk have "i \<le> -(2 ^ (k - 1)) - 1" by simp
   also have "... < -1"
   proof -
     have "0 < (2::int) ^ (k - 1)"
-      by (rule zero_less_power,simp)
-    hence "-((2::int) ^ (k - 1)) < 0"
-      by simp
+      by (rule zero_less_power) simp
+    hence "-((2::int) ^ (k - 1)) < 0" by simp
     thus ?thesis by simp
   qed
   finally have i1: "i < -1" .
   have lii0: "0 < length (int_to_bv i)"
     apply (rule neg_length_pos)
-    apply (simp,rule i1)
+    apply (simp, rule i1)
     done
   assume "~ k < length (int_to_bv i)"
   hence "length (int_to_bv i) \<le> k"
     by simp
-  with lii0
-  have a: "length (int_to_bv i) - 1 \<le> k - 1"
-    by arith
+  with lii0 have a: "length (int_to_bv i) - 1 \<le> k - 1" by arith
   hence "(2::int) ^ (length (int_to_bv i) - 1) \<le> 2 ^ (k - 1)" by simp
-  hence "-((2::int) ^ (k - 1)) \<le> - (2 ^ (length (int_to_bv i) - 1))"
-    by simp
+  hence "-((2::int) ^ (k - 1)) \<le> - (2 ^ (length (int_to_bv i) - 1))" by simp
   also have "... \<le> i"
   proof -
     have "- (2 ^ (length (int_to_bv i) - 1)) \<le> bv_to_int (int_to_bv i)"
@@ -1535,11 +1386,10 @@
     finally show ?thesis .
   qed
   finally have "-(2 ^ (k - 1)) \<le> i" .
-  with wk
-  show False
-    by simp
+  with wk show False by simp
 qed
 
+
 subsection {* Signed Arithmetic Operations *}
 
 subsubsection {* Conversion from unsigned to signed *}
@@ -1558,14 +1408,13 @@
   by (simp add: utos_def norm_signed_Cons)
 
 lemma bv_to_int_utos: "bv_to_int (utos w) = int (bv_to_nat w)"
-proof (simp add: utos_def norm_signed_Cons,safe)
+proof (simp add: utos_def norm_signed_Cons, safe)
   assume "norm_unsigned w = []"
-  hence "bv_to_nat (norm_unsigned w) = 0"
-    by simp
-  thus "bv_to_nat w = 0"
-    by simp
+  hence "bv_to_nat (norm_unsigned w) = 0" by simp
+  thus "bv_to_nat w = 0" by simp
 qed
 
+
 subsubsection {* Unary minus *}
 
 definition
@@ -1592,23 +1441,17 @@
       done
     show ?thesis
     proof (simp add: bv_uminus_def,rule length_int_to_bv_upper_limit_gt0,simp_all)
-      from prems
-      show "bv_to_int w < 0"
-        by simp
+      from prems show "bv_to_int w < 0" by simp
     next
       have "-(2^(length w - 1)) \<le> bv_to_int w"
         by (rule bv_to_int_lower_range)
-      hence "- bv_to_int w \<le> 2^(length w - 1)"
-        by simp
-      also from lw have "... < 2 ^ length w"
-        by simp
-      finally show "- bv_to_int w < 2 ^ length w"
-        by simp
+      hence "- bv_to_int w \<le> 2^(length w - 1)" by simp
+      also from lw have "... < 2 ^ length w" by simp
+      finally show "- bv_to_int w < 2 ^ length w" by simp
     qed
   next
     assume p: "- bv_to_int w = 1"
-    hence lw: "0 < length w"
-      by (cases w,simp_all)
+    hence lw: "0 < length w" by (cases w) simp_all
     from p
     show ?thesis
       apply (simp add: bv_uminus_def)
@@ -1617,12 +1460,10 @@
       done
   next
     assume "- bv_to_int w = 0"
-    thus ?thesis
-      by (simp add: bv_uminus_def)
+    thus ?thesis by (simp add: bv_uminus_def)
   next
     assume p: "- bv_to_int w = -1"
-    thus ?thesis
-      by (simp add: bv_uminus_def)
+    thus ?thesis by (simp add: bv_uminus_def)
   next
     assume p: "- bv_to_int w < -1"
     show ?thesis
@@ -1634,8 +1475,7 @@
       have "bv_to_int w < 2 ^ (length w - 1)"
         by (rule bv_to_int_upper_range)
       also have "... \<le> 2 ^ length w" by simp
-      finally show "bv_to_int w \<le> 2 ^ length w"
-        by simp
+      finally show "bv_to_int w \<le> 2 ^ length w" by simp
     qed
   qed
 qed
@@ -1643,17 +1483,14 @@
 lemma bv_uminus_length_utos: "length (bv_uminus (utos w)) \<le> Suc (length w)"
 proof -
   have "-bv_to_int (utos w) = 0 \<or> -bv_to_int (utos w) = -1 \<or> -bv_to_int (utos w) < -1"
-    apply (simp add: bv_to_int_utos)
-    by arith
+    by (simp add: bv_to_int_utos, arith)
   thus ?thesis
   proof safe
     assume "-bv_to_int (utos w) = 0"
-    thus ?thesis
-      by (simp add: bv_uminus_def)
+    thus ?thesis by (simp add: bv_uminus_def)
   next
     assume "-bv_to_int (utos w) = -1"
-    thus ?thesis
-      by (simp add: bv_uminus_def)
+    thus ?thesis by (simp add: bv_uminus_def)
   next
     assume p: "-bv_to_int (utos w) < -1"
     show ?thesis
@@ -1684,7 +1521,8 @@
   assumes lw: "0 < max (length w1) (length w2)"
   shows   "((2::int) ^ (length w1 - 1)) + (2 ^ (length w2 - 1)) \<le> 2 ^ max (length w1) (length w2)"
 proof -
-  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)"
+  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)"
     apply (cases "length w1 \<le> length w2")
     apply (auto simp add: max_def)
     done
@@ -1713,15 +1551,12 @@
       show "w2 \<noteq> []"
       proof (rule ccontr,simp)
         assume [simp]: "w2 = []"
-        from p
-        show False
-          by simp
+        from p show False by simp
       qed
     qed
   qed
 
-  have "0 < ?Q \<or> ?Q = 0 \<or> ?Q = -1 \<or> ?Q < -1"
-    by arith
+  have "0 < ?Q \<or> ?Q = 0 \<or> ?Q = -1 \<or> ?Q < -1" by arith
   thus ?thesis
   proof safe
     assume "?Q = 0"
@@ -1750,8 +1585,7 @@
         using p
         apply simp
         done
-      finally show "?Q < 2 ^ max (length w1) (length w2)"
-        .
+      finally show "?Q < 2 ^ max (length w1) (length w2)" .
     qed
   next
     assume p: "?Q < -1"
@@ -1802,20 +1636,16 @@
       by (rule le_maxI1)
     also have "... \<le> Suc (max (length w1) (length w2))"
       by arith
-    finally show "length (norm_signed w1) \<le> Suc (max (length w1) (length w2))"
-      .
+    finally show "length (norm_signed w1) \<le> Suc (max (length w1) (length w2))" .
   qed
 next
   assume "bv_to_int w2 \<noteq> 0"
-  hence "0 < length w2"
-    by (cases w2,simp_all)
-  hence lmw: "0 < max (length w1) (length w2)"
-    by arith
+  hence "0 < length w2" by (cases w2,simp_all)
+  hence lmw: "0 < max (length w1) (length w2)" by arith
 
   let ?Q = "bv_to_int w1 - bv_to_int w2"
 
-  have "0 < ?Q \<or> ?Q = 0 \<or> ?Q = -1 \<or> ?Q < -1"
-    by arith
+  have "0 < ?Q \<or> ?Q = 0 \<or> ?Q = -1 \<or> ?Q < -1" by arith
   thus ?thesis
   proof safe
     assume "?Q = 0"
@@ -1833,8 +1663,7 @@
       apply (rule p)
     proof simp
       from bv_to_int_lower_range [of w2]
-      have v2: "- bv_to_int w2 \<le> 2 ^ (length w2 - 1)"
-        by simp
+      have v2: "- bv_to_int w2 \<le> 2 ^ (length w2 - 1)" by simp
       have "bv_to_int w1 + - bv_to_int w2 < (2 ^ (length w1 - 1)) + (2 ^ (length w2 - 1))"
         apply (rule zadd_zless_mono)
         apply (rule bv_to_int_upper_range [of w1])
@@ -1844,8 +1673,7 @@
         apply (rule adder_helper)
         apply (rule lmw)
         done
-      finally show "?Q < 2 ^ max (length w1) (length w2)"
-        by simp
+      finally show "?Q < 2 ^ max (length w1) (length w2)" by simp
     qed
   next
     assume p: "?Q < -1"
@@ -1866,8 +1694,7 @@
         using bv_to_int_upper_range [of w2]
         apply simp
         done
-      finally show "- (2^max (length w1) (length w2)) \<le> ?Q"
-        by simp
+      finally show "- (2^max (length w1) (length w2)) \<le> ?Q" by simp
     qed
   qed
 qed
@@ -1889,20 +1716,16 @@
 proof -
   let ?Q = "bv_to_int w1 * bv_to_int w2"
 
-  have lmw: "?Q \<noteq> 0 ==> 0 < length w1 \<and> 0 < length w2"
-    by auto
+  have lmw: "?Q \<noteq> 0 ==> 0 < length w1 \<and> 0 < length w2" by auto
 
-  have "0 < ?Q \<or> ?Q = 0 \<or> ?Q = -1 \<or> ?Q < -1"
-    by arith
+  have "0 < ?Q \<or> ?Q = 0 \<or> ?Q = -1 \<or> ?Q < -1" by arith
   thus ?thesis
   proof (safe dest!: iffD1 [OF mult_eq_0_iff])
     assume "bv_to_int w1 = 0"
-    thus ?thesis
-      by (simp add: bv_smult_def)
+    thus ?thesis by (simp add: bv_smult_def)
   next
     assume "bv_to_int w2 = 0"
-    thus ?thesis
-      by (simp add: bv_smult_def)
+    thus ?thesis by (simp add: bv_smult_def)
   next
     assume p: "?Q = -1"
     show ?thesis
@@ -1937,8 +1760,7 @@
           apply (subst zpower_zadd_distrib [symmetric])
           apply simp
           done
-        finally show "?Q < 2 ^ (length w1 + length w2 - Suc 0)"
-          .
+        finally show "?Q < 2 ^ (length w1 + length w2 - Suc 0)" .
       qed
     next
       assume bi1: "bv_to_int w1 < 0"
@@ -2028,33 +1850,28 @@
             by simp
         qed
       qed
-      finally show "-(2 ^ (length w1 + length w2 - Suc 0)) \<le> ?Q"
-        .
+      finally show "-(2 ^ (length w1 + length w2 - Suc 0)) \<le> ?Q" .
     qed
   qed
 qed
 
 lemma bv_msb_one: "bv_msb w = \<one> ==> 0 < bv_to_nat w"
-  by (cases w,simp_all)
+  by (cases w) simp_all
 
 lemma bv_smult_length_utos: "length (bv_smult (utos w1) w2) \<le> length w1 + length w2"
 proof -
   let ?Q = "bv_to_int (utos w1) * bv_to_int w2"
 
-  have lmw: "?Q \<noteq> 0 ==> 0 < length (utos w1) \<and> 0 < length w2"
-    by auto
+  have lmw: "?Q \<noteq> 0 ==> 0 < length (utos w1) \<and> 0 < length w2" by auto
 
-  have "0 < ?Q \<or> ?Q = 0 \<or> ?Q = -1 \<or> ?Q < -1"
-    by arith
+  have "0 < ?Q \<or> ?Q = 0 \<or> ?Q = -1 \<or> ?Q < -1" by arith
   thus ?thesis
   proof (safe dest!: iffD1 [OF mult_eq_0_iff])
     assume "bv_to_int (utos w1) = 0"
-    thus ?thesis
-      by (simp add: bv_smult_def)
+    thus ?thesis by (simp add: bv_smult_def)
   next
     assume "bv_to_int w2 = 0"
-    thus ?thesis
-      by (simp add: bv_smult_def)
+    thus ?thesis by (simp add: bv_smult_def)
   next
     assume p: "0 < ?Q"
     thus ?thesis
@@ -2083,13 +1900,11 @@
           using p
           apply auto
           done
-        finally show "?Q < 2 ^ (length w1 + length w2 - Suc 0)"
-          .
+        finally show "?Q < 2 ^ (length w1 + length w2 - Suc 0)" .
       qed
     next
       assume "bv_to_int (utos w1) < 0"
-      thus ?thesis
-        by (simp add: bv_to_int_utos)
+      thus ?thesis by (simp add: bv_to_int_utos)
     qed
   next
     assume p: "?Q = -1"
@@ -2147,8 +1962,7 @@
             by (simp add: bv_to_int_utos)
         qed
       qed
-      finally show "-(2 ^ (length w1 + length w2 - Suc 0)) \<le> ?Q"
-        .
+      finally show "-(2 ^ (length w1 + length w2 - Suc 0)) \<le> ?Q" .
     qed
   qed
 qed
@@ -2183,9 +1997,7 @@
     show "xs ! (length xs - Suc n) = rev xs ! n"
     proof (cases xs)
       assume "xs = []"
-      with notx
-      show ?thesis
-        by simp
+      with notx show ?thesis by simp
     next
       fix y ys
       assume [simp]: "xs = y # ys"
@@ -2195,33 +2007,23 @@
         from spec [OF ind,of ys]
         have "\<forall>n. n < length ys --> ys ! (length ys - Suc n) = rev ys ! n"
           by simp
-        hence "n < length ys --> ys ! (length ys - Suc n) = rev ys ! n"
-          ..
-        hence "ys ! (length ys - Suc n) = rev ys ! n"
-          ..
+        hence "n < length ys --> ys ! (length ys - Suc n) = rev ys ! n" ..
+	from this and noty
+        have "ys ! (length ys - Suc n) = rev ys ! n" ..
         thus "(y # ys) ! (length ys - n) = rev ys ! n"
           by (simp add: nth_Cons' noty linorder_not_less [symmetric])
       next
         assume "~ n < length ys"
-        hence x: "length ys \<le> n"
-          by simp
-        from notx
-        have "n < Suc (length ys)"
-          by simp
-        hence "n \<le> length ys"
-          by simp
-        with x
-        have "length ys = n"
-          by simp
-        thus "y = [y] ! (n - length ys)"
-          by simp
+        hence x: "length ys \<le> n" by simp
+        from notx have "n < Suc (length ys)" by simp
+        hence "n \<le> length ys" by simp
+        with x have "length ys = n" by simp
+        thus "y = [y] ! (n - length ys)" by simp
       qed
     qed
   qed
-  hence "n < length w --> bv_select w n = rev w ! n"
-    ..
-  thus ?thesis
-    ..
+  then have "n < length w --> bv_select w n = rev w ! n" ..
+  from this and notnull show ?thesis ..
 qed
 
 lemma bv_chop_append: "bv_chop (w1 @ w2) (length w2) = (w1,w2)"
@@ -2252,12 +2054,10 @@
   apply (rule ccontr)
 proof -
   assume "~ n < 2 ^ length (nat_to_bv n)"
-  hence "2 ^ length (nat_to_bv n) \<le> n"
-    by simp
+  hence "2 ^ length (nat_to_bv n) \<le> n" by simp
   hence "length (nat_to_bv n) < length (nat_to_bv n)"
     by (rule length_nat_to_bv_lower_limit)
-  thus False
-    by simp
+  thus False by simp
 qed
 
 lemma length_nat_0 [simp]: "length_nat 0 = 0"
@@ -2281,8 +2081,8 @@
 lemma length_int: "length (int_to_bv i) = length_int i"
 proof (cases "0 < i")
   assume i0: "0 < i"
-  hence "length (int_to_bv i) = length (norm_signed (\<zero> # norm_unsigned (nat_to_bv (nat i))))"
-    by simp
+  hence "length (int_to_bv i) =
+      length (norm_signed (\<zero> # norm_unsigned (nat_to_bv (nat i))))" by simp
   also from norm_unsigned_result [of "nat_to_bv (nat i)"]
   have "... = Suc (length_nat (nat i))"
     apply safe
@@ -2303,19 +2103,16 @@
     by (simp add: length_int_def)
 next
   assume "~ 0 < i"
-  hence i0: "i \<le> 0"
-    by simp
+  hence i0: "i \<le> 0" by simp
   show ?thesis
   proof (cases "i = 0")
     assume "i = 0"
-    thus ?thesis
-      by (simp add: length_int_def)
+    thus ?thesis by (simp add: length_int_def)
   next
     assume "i \<noteq> 0"
-    with i0
-    have i0: "i < 0"
-      by simp
-    hence "length (int_to_bv i) = length (norm_signed (\<one> # bv_not (norm_unsigned (nat_to_bv (nat (- i) - 1)))))"
+    with i0 have i0: "i < 0" by simp
+    hence "length (int_to_bv i) =
+        length (norm_signed (\<one> # bv_not (norm_unsigned (nat_to_bv (nat (- i) - 1)))))"
       by (simp add: int_to_bv_def nat_diff_distrib)
     also from norm_unsigned_result [of "nat_to_bv (nat (- i) - 1)"]
     have "... = Suc (length_nat (nat (- i) - 1))"
@@ -2333,8 +2130,7 @@
       done
     finally
     show ?thesis
-      using i0
-      by (simp add: length_int_def nat_diff_distrib del: int_to_bv_lt0)
+      using i0 by (simp add: length_int_def nat_diff_distrib del: int_to_bv_lt0)
   qed
 qed
 
@@ -2413,14 +2209,11 @@
   shows      "bv_to_int (bv_extend n b w) = bv_to_int w"
 proof (cases "bv_msb w")
   assume [simp]: "bv_msb w = \<zero>"
-  with a have [simp]: "b = \<zero>"
-    by simp
-  show ?thesis
-    by (simp add: bv_to_int_def)
+  with a have [simp]: "b = \<zero>" by simp
+  show ?thesis by (simp add: bv_to_int_def)
 next
   assume [simp]: "bv_msb w = \<one>"
-  with a have [simp]: "b = \<one>"
-    by simp
+  with a have [simp]: "b = \<one>" by simp
   show ?thesis
     apply (simp add: bv_to_int_def)
     apply (simp add: bv_extend_def)
@@ -2447,26 +2240,21 @@
     apply (cases "0 \<le> y")
     apply (induct y,simp_all)
     done
-  with xx
-  have "y < x" by simp
-  with xy
-  show False
-    by simp
+  with xx have "y < x" by simp
+  with xy show False by simp
 qed
 
 lemma length_nat_mono_int [simp]: "x \<le> y ==> length_nat x \<le> length_nat y"
-  apply (rule length_nat_mono)
-  apply arith
-  done
+  by (rule length_nat_mono) arith
 
 lemma length_nat_pos [simp,intro!]: "0 < x ==> 0 < length_nat x"
   by (simp add: length_nat_non0)
 
 lemma length_int_mono_gt0: "[| 0 \<le> x ; x \<le> y |] ==> length_int x \<le> length_int y"
-  by (cases "x = 0",simp_all add: length_int_gt0 nat_le_eq_zle)
+  by (cases "x = 0") (simp_all add: length_int_gt0 nat_le_eq_zle)
 
-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)
-  done
+lemma length_int_mono_lt0: "[| x \<le> y ; y \<le> 0 |] ==> length_int y \<le> length_int x"
+  by (cases "y = 0") (simp_all add: length_int_lt0)
 
 lemmas [simp] = length_nat_non0
 
@@ -2475,18 +2263,21 @@
 
 consts
   fast_bv_to_nat_helper :: "[bit list, int] => int"
-
 primrec
   fast_bv_to_nat_Nil: "fast_bv_to_nat_helper [] k = k"
-  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))"
+  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))"
 
-lemma fast_bv_to_nat_Cons0: "fast_bv_to_nat_helper (\<zero>#bs) bin = fast_bv_to_nat_helper bs (bin BIT bit.B0)"
+lemma fast_bv_to_nat_Cons0: "fast_bv_to_nat_helper (\<zero>#bs) bin =
+    fast_bv_to_nat_helper bs (bin BIT bit.B0)"
   by simp
 
-lemma fast_bv_to_nat_Cons1: "fast_bv_to_nat_helper (\<one>#bs) bin = fast_bv_to_nat_helper bs (bin BIT bit.B1)"
+lemma fast_bv_to_nat_Cons1: "fast_bv_to_nat_helper (\<one>#bs) bin =
+    fast_bv_to_nat_helper bs (bin BIT bit.B1)"
   by simp
 
-lemma fast_bv_to_nat_def: "bv_to_nat bs == number_of (fast_bv_to_nat_helper bs Numeral.Pls)"
+lemma fast_bv_to_nat_def:
+  "bv_to_nat bs == number_of (fast_bv_to_nat_helper bs Numeral.Pls)"
 proof (simp add: bv_to_nat_def)
   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)"
     apply (induct bs,simp)
@@ -2547,7 +2338,7 @@
      in map (split f) (zip (g w1) (g w2)))"
 
 lemma bv_length_bv_mapzip [simp]:
-  "length (bv_mapzip f w1 w2) = max (length w1) (length w2)"
+    "length (bv_mapzip f w1 w2) = max (length w1) (length w2)"
   by (simp add: bv_mapzip_def Let_def split: split_max)
 
 lemma bv_mapzip_Nil [simp]: "bv_mapzip f [] [] = []"