# HG changeset patch
# User wenzelm
# Date 1491253964 -7200
# Node ID db7c97cdcfe7ffa59bb370f5f576e45dacbc0210
# Parent  4ff2ba82d6681143c26924f604eecd0f88a43b0a# Parent  5eb619751b14699131118defab42550597016bb9
merged

diff -r 4ff2ba82d668 -r db7c97cdcfe7 src/HOL/Word/Bit_Representation.thy
--- a/src/HOL/Word/Bit_Representation.thy	Mon Apr 03 22:18:56 2017 +0200
+++ b/src/HOL/Word/Bit_Representation.thy	Mon Apr 03 23:12:44 2017 +0200
@@ -1,27 +1,24 @@
-(* 
-  Author: Jeremy Dawson, NICTA
-*) 
+(*  Title:      HOL/Word/Bit_Representation.thy
+    Author:     Jeremy Dawson, NICTA
+*)
 
 section \<open>Integers as implict bit strings\<close>
 
 theory Bit_Representation
-imports Misc_Numeric
+  imports Misc_Numeric
 begin
 
 subsection \<open>Constructors and destructors for binary integers\<close>
 
-definition Bit :: "int \<Rightarrow> bool \<Rightarrow> int" (infixl "BIT" 90)
-where
-  "k BIT b = (if b then 1 else 0) + k + k"
+definition Bit :: "int \<Rightarrow> bool \<Rightarrow> int"  (infixl "BIT" 90)
+  where "k BIT b = (if b then 1 else 0) + k + k"
 
-lemma Bit_B0:
-  "k BIT False = k + k"
-   by (unfold Bit_def) simp
+lemma Bit_B0: "k BIT False = k + k"
+   by (simp add: Bit_def)
 
-lemma Bit_B1:
-  "k BIT True = k + k + 1"
-   by (unfold Bit_def) simp
-  
+lemma Bit_B1: "k BIT True = k + k + 1"
+   by (simp add: Bit_def)
+
 lemma Bit_B0_2t: "k BIT False = 2 * k"
   by (rule trans, rule Bit_B0) simp
 
@@ -29,36 +26,28 @@
   by (rule trans, rule Bit_B1) simp
 
 definition bin_last :: "int \<Rightarrow> bool"
-where
-  "bin_last w \<longleftrightarrow> w mod 2 = 1"
+  where "bin_last w \<longleftrightarrow> w mod 2 = 1"
 
-lemma bin_last_odd:
-  "bin_last = odd"
+lemma bin_last_odd: "bin_last = odd"
   by (rule ext) (simp add: bin_last_def even_iff_mod_2_eq_zero)
 
 definition bin_rest :: "int \<Rightarrow> int"
-where
-  "bin_rest w = w div 2"
+  where "bin_rest w = w div 2"
 
-lemma bin_rl_simp [simp]:
-  "bin_rest w BIT bin_last w = w"
+lemma bin_rl_simp [simp]: "bin_rest w BIT bin_last w = w"
   unfolding bin_rest_def bin_last_def Bit_def
-  using div_mult_mod_eq [of w 2]
-  by (cases "w mod 2 = 0", simp_all)
+  by (cases "w mod 2 = 0") (use div_mult_mod_eq [of w 2] in simp_all)
 
 lemma bin_rest_BIT [simp]: "bin_rest (x BIT b) = x"
   unfolding bin_rest_def Bit_def
-  by (cases b, simp_all)
+  by (cases b) simp_all
 
 lemma bin_last_BIT [simp]: "bin_last (x BIT b) = b"
   unfolding bin_last_def Bit_def
   by (cases b) simp_all
 
 lemma BIT_eq_iff [iff]: "u BIT b = v BIT c \<longleftrightarrow> u = v \<and> b = c"
-  apply (auto simp add: Bit_def)
-  apply arith
-  apply arith
-  done
+  by (auto simp: Bit_def) arith+
 
 lemma BIT_bin_simps [simp]:
   "numeral k BIT False = numeral (Num.Bit0 k)"
@@ -66,34 +55,32 @@
   "(- numeral k) BIT False = - numeral (Num.Bit0 k)"
   "(- numeral k) BIT True = - numeral (Num.BitM k)"
   unfolding numeral.simps numeral_BitM
-  unfolding Bit_def
-  by (simp_all del: arith_simps add_numeral_special diff_numeral_special)
+  by (simp_all add: Bit_def del: arith_simps add_numeral_special diff_numeral_special)
 
 lemma BIT_special_simps [simp]:
-  shows "0 BIT False = 0" and "0 BIT True = 1"
-  and "1 BIT False = 2" and "1 BIT True = 3"
-  and "(- 1) BIT False = - 2" and "(- 1) BIT True = - 1"
-  unfolding Bit_def by simp_all
+  shows "0 BIT False = 0"
+    and "0 BIT True = 1"
+    and "1 BIT False = 2"
+    and "1 BIT True = 3"
+    and "(- 1) BIT False = - 2"
+    and "(- 1) BIT True = - 1"
+  by (simp_all add: Bit_def)
 
 lemma Bit_eq_0_iff: "w BIT b = 0 \<longleftrightarrow> w = 0 \<and> \<not> b"
-  apply (auto simp add: Bit_def)
-  apply arith
-  done
+  by (auto simp: Bit_def) arith
 
 lemma Bit_eq_m1_iff: "w BIT b = -1 \<longleftrightarrow> w = -1 \<and> b"
-  apply (auto simp add: Bit_def)
-  apply arith
-  done
+  by (auto simp: Bit_def) arith
 
 lemma BitM_inc: "Num.BitM (Num.inc w) = Num.Bit1 w"
-  by (induct w, simp_all)
+  by (induct w) simp_all
 
 lemma expand_BIT:
   "numeral (Num.Bit0 w) = numeral w BIT False"
   "numeral (Num.Bit1 w) = numeral w BIT True"
   "- numeral (Num.Bit0 w) = (- numeral w) BIT False"
   "- numeral (Num.Bit1 w) = (- numeral (w + Num.One)) BIT True"
-  unfolding add_One by (simp_all add: BitM_inc)
+  by (simp_all add: add_One BitM_inc)
 
 lemma bin_last_numeral_simps [simp]:
   "\<not> bin_last 0"
@@ -117,13 +104,11 @@
   "bin_rest (- numeral (Num.Bit1 w)) = - numeral (w + Num.One)"
   by (simp_all add: bin_rest_def zdiv_zminus1_eq_if) (auto simp add: divmod_def)
 
-lemma less_Bits: 
-  "v BIT b < w BIT c \<longleftrightarrow> v < w \<or> v \<le> w \<and> \<not> b \<and> c"
-  unfolding Bit_def by auto
+lemma less_Bits: "v BIT b < w BIT c \<longleftrightarrow> v < w \<or> v \<le> w \<and> \<not> b \<and> c"
+  by (auto simp: Bit_def)
 
-lemma le_Bits: 
-  "v BIT b \<le> w BIT c \<longleftrightarrow> v < w \<or> v \<le> w \<and> (\<not> b \<or> c)" 
-  unfolding Bit_def by auto
+lemma le_Bits: "v BIT b \<le> w BIT c \<longleftrightarrow> v < w \<or> v \<le> w \<and> (\<not> b \<or> c)"
+  by (auto simp: Bit_def)
 
 lemma pred_BIT_simps [simp]:
   "x BIT False - 1 = (x - 1) BIT True"
@@ -148,31 +133,27 @@
   "x BIT True * y = (x * y) BIT False + y"
   by (simp_all add: Bit_B0_2t Bit_B1_2t algebra_simps)
 
-lemma B_mod_2': 
-  "X = 2 ==> (w BIT True) mod X = 1 & (w BIT False) mod X = 0"
-  apply (simp (no_asm) only: Bit_B0 Bit_B1)
-  apply simp
-  done
+lemma B_mod_2': "X = 2 \<Longrightarrow> (w BIT True) mod X = 1 \<and> (w BIT False) mod X = 0"
+  by (simp add: Bit_B0 Bit_B1)
 
-lemma bin_ex_rl: "EX w b. w BIT b = bin"
+lemma bin_ex_rl: "\<exists>w b. w BIT b = bin"
   by (metis bin_rl_simp)
 
 lemma bin_exhaust:
-  assumes Q: "\<And>x b. bin = x BIT b \<Longrightarrow> Q"
+  assumes that: "\<And>x b. bin = x BIT b \<Longrightarrow> Q"
   shows "Q"
-  apply (insert bin_ex_rl [of bin])  
+  apply (insert bin_ex_rl [of bin])
   apply (erule exE)+
-  apply (rule Q)
+  apply (rule that)
   apply force
   done
 
-primrec bin_nth where
-  Z: "bin_nth w 0 \<longleftrightarrow> bin_last w"
+primrec bin_nth
+  where
+    Z: "bin_nth w 0 \<longleftrightarrow> bin_last w"
   | Suc: "bin_nth w (Suc n) \<longleftrightarrow> bin_nth (bin_rest w) n"
 
-lemma bin_abs_lem:
-  "bin = (w BIT b) ==> bin ~= -1 --> bin ~= 0 -->
-    nat \<bar>w\<bar> < nat \<bar>bin\<bar>"
+lemma bin_abs_lem: "bin = (w BIT b) \<Longrightarrow> bin \<noteq> -1 \<longrightarrow> bin \<noteq> 0 \<longrightarrow> nat \<bar>w\<bar> < nat \<bar>bin\<bar>"
   apply clarsimp
   apply (unfold Bit_def)
   apply (cases b)
@@ -183,10 +164,9 @@
 lemma bin_induct:
   assumes PPls: "P 0"
     and PMin: "P (- 1)"
-    and PBit: "!!bin bit. P bin ==> P (bin BIT bit)"
+    and PBit: "\<And>bin bit. P bin \<Longrightarrow> P (bin BIT bit)"
   shows "P bin"
-  apply (rule_tac P=P and a=bin and f1="nat o abs" 
-                  in wf_measure [THEN wf_induct])
+  apply (rule_tac P=P and a=bin and f1="nat \<circ> abs" in wf_measure [THEN wf_induct])
   apply (simp add: measure_def inv_image_def)
   apply (case_tac x rule: bin_exhaust)
   apply (frule bin_abs_lem)
@@ -196,26 +176,23 @@
 lemma Bit_div2 [simp]: "(w BIT b) div 2 = w"
   unfolding bin_rest_def [symmetric] by (rule bin_rest_BIT)
 
-lemma bin_nth_eq_iff:
-  "bin_nth x = bin_nth y \<longleftrightarrow> x = y"
+lemma bin_nth_eq_iff: "bin_nth x = bin_nth y \<longleftrightarrow> x = y"
 proof -
-  have bin_nth_lem [rule_format]: "ALL y. bin_nth x = bin_nth y --> x = y"
+  have bin_nth_lem [rule_format]: "\<forall>y. bin_nth x = bin_nth y \<longrightarrow> x = y"
     apply (induct x rule: bin_induct)
       apply safe
       apply (erule rev_mp)
       apply (induct_tac y rule: bin_induct)
         apply safe
         apply (drule_tac x=0 in fun_cong, force)
-       apply (erule notE, rule ext, 
-            drule_tac x="Suc x" in fun_cong, force)
+       apply (erule notE, rule ext, drule_tac x="Suc x" in fun_cong, force)
       apply (drule_tac x=0 in fun_cong, force)
      apply (erule rev_mp)
      apply (induct_tac y rule: bin_induct)
        apply safe
        apply (drule_tac x=0 in fun_cong, force)
-      apply (erule notE, rule ext, 
-           drule_tac x="Suc x" in fun_cong, force)
-      apply (metis Bit_eq_m1_iff Z bin_last_BIT)
+      apply (erule notE, rule ext, drule_tac x="Suc x" in fun_cong, force)
+     apply (metis Bit_eq_m1_iff Z bin_last_BIT)
     apply (case_tac y rule: bin_exhaust)
     apply clarify
     apply (erule allE)
@@ -227,13 +204,12 @@
     apply (drule_tac x="Suc x" for x in fun_cong, force)
     done
   show ?thesis
-  by (auto elim: bin_nth_lem)
+    by (auto elim: bin_nth_lem)
 qed
 
 lemmas bin_eqI = ext [THEN bin_nth_eq_iff [THEN iffD1]]
 
-lemma bin_eq_iff:
-  "x = y \<longleftrightarrow> (\<forall>n. bin_nth x n = bin_nth y n)"
+lemma bin_eq_iff: "x = y \<longleftrightarrow> (\<forall>n. bin_nth x n = bin_nth y n)"
   using bin_nth_eq_iff by auto
 
 lemma bin_nth_zero [simp]: "\<not> bin_nth 0 n"
@@ -251,11 +227,10 @@
 lemma bin_nth_Suc_BIT: "bin_nth (w BIT b) (Suc n) = bin_nth w n"
   by auto
 
-lemma bin_nth_minus [simp]: "0 < n ==> bin_nth (w BIT b) n = bin_nth w (n - 1)"
+lemma bin_nth_minus [simp]: "0 < n \<Longrightarrow> bin_nth (w BIT b) n = bin_nth w (n - 1)"
   by (cases n) auto
 
-lemma bin_nth_numeral:
-  "bin_rest x = y \<Longrightarrow> bin_nth x (numeral n) = bin_nth y (pred_numeral n)"
+lemma bin_nth_numeral: "bin_rest x = y \<Longrightarrow> bin_nth x (numeral n) = bin_nth y (pred_numeral n)"
   by (simp add: numeral_eq_Suc)
 
 lemmas bin_nth_numeral_simps [simp] =
@@ -265,7 +240,7 @@
   bin_nth_numeral [OF bin_rest_numeral_simps(7)]
   bin_nth_numeral [OF bin_rest_numeral_simps(8)]
 
-lemmas bin_nth_simps = 
+lemmas bin_nth_simps =
   bin_nth.Z bin_nth.Suc bin_nth_zero bin_nth_minus1
   bin_nth_numeral_simps
 
@@ -273,8 +248,7 @@
 subsection \<open>Truncating binary integers\<close>
 
 definition bin_sign :: "int \<Rightarrow> int"
-where
-  bin_sign_def: "bin_sign k = (if k \<ge> 0 then 0 else - 1)"
+  where "bin_sign k = (if k \<ge> 0 then 0 else - 1)"
 
 lemma bin_sign_simps [simp]:
   "bin_sign 0 = 0"
@@ -283,28 +257,26 @@
   "bin_sign (numeral k) = 0"
   "bin_sign (- numeral k) = -1"
   "bin_sign (w BIT b) = bin_sign w"
-  unfolding bin_sign_def Bit_def
-  by simp_all
+  by (simp_all add: bin_sign_def Bit_def)
 
-lemma bin_sign_rest [simp]: 
-  "bin_sign (bin_rest w) = bin_sign w"
+lemma bin_sign_rest [simp]: "bin_sign (bin_rest w) = bin_sign w"
   by (cases w rule: bin_exhaust) auto
 
-primrec bintrunc :: "nat \<Rightarrow> int \<Rightarrow> int" where
-  Z : "bintrunc 0 bin = 0"
-| Suc : "bintrunc (Suc n) bin = bintrunc n (bin_rest bin) BIT (bin_last bin)"
+primrec bintrunc :: "nat \<Rightarrow> int \<Rightarrow> int"
+  where
+    Z : "bintrunc 0 bin = 0"
+  | Suc : "bintrunc (Suc n) bin = bintrunc n (bin_rest bin) BIT (bin_last bin)"
 
-primrec sbintrunc :: "nat => int => int" where
-  Z : "sbintrunc 0 bin = (if bin_last bin then -1 else 0)"
-| Suc : "sbintrunc (Suc n) bin = sbintrunc n (bin_rest bin) BIT (bin_last bin)"
+primrec sbintrunc :: "nat \<Rightarrow> int \<Rightarrow> int"
+  where
+    Z : "sbintrunc 0 bin = (if bin_last bin then -1 else 0)"
+  | Suc : "sbintrunc (Suc n) bin = sbintrunc n (bin_rest bin) BIT (bin_last bin)"
 
 lemma sign_bintr: "bin_sign (bintrunc n w) = 0"
   by (induct n arbitrary: w) auto
 
-lemma bintrunc_mod2p: "bintrunc n w = (w mod 2 ^ n)"
-  apply (induct n arbitrary: w, clarsimp)
-  apply (simp add: bin_last_def bin_rest_def Bit_def zmod_zmult2_eq)
-  done
+lemma bintrunc_mod2p: "bintrunc n w = w mod 2 ^ n"
+  by (induct n arbitrary: w) (auto simp add: bin_last_def bin_rest_def Bit_def zmod_zmult2_eq)
 
 lemma sbintrunc_mod2p: "sbintrunc n w = (w + 2 ^ n) mod 2 ^ (Suc n) - 2 ^ n"
   apply (induct n arbitrary: w)
@@ -330,10 +302,8 @@
   "bintrunc (Suc n) (- 1) = bintrunc n (- 1) BIT True"
   "bintrunc (Suc n) (numeral (Num.Bit0 w)) = bintrunc n (numeral w) BIT False"
   "bintrunc (Suc n) (numeral (Num.Bit1 w)) = bintrunc n (numeral w) BIT True"
-  "bintrunc (Suc n) (- numeral (Num.Bit0 w)) =
-    bintrunc n (- numeral w) BIT False"
-  "bintrunc (Suc n) (- numeral (Num.Bit1 w)) =
-    bintrunc n (- numeral (w + Num.One)) BIT True"
+  "bintrunc (Suc n) (- numeral (Num.Bit0 w)) = bintrunc n (- numeral w) BIT False"
+  "bintrunc (Suc n) (- numeral (Num.Bit1 w)) = bintrunc n (- numeral (w + Num.One)) BIT True"
   by simp_all
 
 lemma sbintrunc_0_numeral [simp]:
@@ -346,14 +316,10 @@
 
 lemma sbintrunc_Suc_numeral:
   "sbintrunc (Suc n) 1 = 1"
-  "sbintrunc (Suc n) (numeral (Num.Bit0 w)) =
-    sbintrunc n (numeral w) BIT False"
-  "sbintrunc (Suc n) (numeral (Num.Bit1 w)) =
-    sbintrunc n (numeral w) BIT True"
-  "sbintrunc (Suc n) (- numeral (Num.Bit0 w)) =
-    sbintrunc n (- numeral w) BIT False"
-  "sbintrunc (Suc n) (- numeral (Num.Bit1 w)) =
-    sbintrunc n (- numeral (w + Num.One)) BIT True"
+  "sbintrunc (Suc n) (numeral (Num.Bit0 w)) = sbintrunc n (numeral w) BIT False"
+  "sbintrunc (Suc n) (numeral (Num.Bit1 w)) = sbintrunc n (numeral w) BIT True"
+  "sbintrunc (Suc n) (- numeral (Num.Bit0 w)) = sbintrunc n (- numeral w) BIT False"
+  "sbintrunc (Suc n) (- numeral (Num.Bit1 w)) = sbintrunc n (- numeral (w + Num.One)) BIT True"
   by simp_all
 
 lemma bin_sign_lem: "(bin_sign (sbintrunc n bin) = -1) = bin_nth bin n"
@@ -361,24 +327,21 @@
   apply (case_tac bin rule: bin_exhaust, case_tac b, auto)
   done
 
-lemma nth_bintr: "bin_nth (bintrunc m w) n = (n < m & bin_nth w n)"
+lemma nth_bintr: "bin_nth (bintrunc m w) n \<longleftrightarrow> n < m \<and> bin_nth w n"
   apply (induct n arbitrary: w m)
    apply (case_tac m, auto)[1]
   apply (case_tac m, auto)[1]
   done
 
-lemma nth_sbintr:
-  "bin_nth (sbintrunc m w) n = 
-          (if n < m then bin_nth w n else bin_nth w m)"
+lemma nth_sbintr: "bin_nth (sbintrunc m w) n = (if n < m then bin_nth w n else bin_nth w m)"
   apply (induct n arbitrary: w m)
+   apply (case_tac m)
+    apply simp_all
   apply (case_tac m)
-  apply simp_all
-  apply (case_tac m)
-  apply simp_all
+   apply simp_all
   done
 
-lemma bin_nth_Bit:
-  "bin_nth (w BIT b) n = (n = 0 & b | (EX m. n = Suc m & bin_nth w m))"
+lemma bin_nth_Bit: "bin_nth (w BIT b) n \<longleftrightarrow> n = 0 \<and> b \<or> (\<exists>m. n = Suc m \<and> bin_nth w m)"
   by (cases n) auto
 
 lemma bin_nth_Bit0:
@@ -391,69 +354,58 @@
     n = 0 \<or> (\<exists>m. n = Suc m \<and> bin_nth (numeral w) m)"
   using bin_nth_Bit [where w="numeral w" and b="True"] by simp
 
-lemma bintrunc_bintrunc_l:
-  "n <= m ==> (bintrunc m (bintrunc n w) = bintrunc n w)"
-  by (rule bin_eqI) (auto simp add : nth_bintr)
+lemma bintrunc_bintrunc_l: "n \<le> m \<Longrightarrow> bintrunc m (bintrunc n w) = bintrunc n w"
+  by (rule bin_eqI) (auto simp: nth_bintr)
 
-lemma sbintrunc_sbintrunc_l:
-  "n <= m ==> (sbintrunc m (sbintrunc n w) = sbintrunc n w)"
+lemma sbintrunc_sbintrunc_l: "n \<le> m \<Longrightarrow> sbintrunc m (sbintrunc n w) = sbintrunc n w"
   by (rule bin_eqI) (auto simp: nth_sbintr)
 
-lemma bintrunc_bintrunc_ge:
-  "n <= m ==> (bintrunc n (bintrunc m w) = bintrunc n w)"
+lemma bintrunc_bintrunc_ge: "n \<le> m \<Longrightarrow> bintrunc n (bintrunc m w) = bintrunc n w"
   by (rule bin_eqI) (auto simp: nth_bintr)
 
-lemma bintrunc_bintrunc_min [simp]:
-  "bintrunc m (bintrunc n w) = bintrunc (min m n) w"
-  apply (rule bin_eqI)
-  apply (auto simp: nth_bintr)
-  done
+lemma bintrunc_bintrunc_min [simp]: "bintrunc m (bintrunc n w) = bintrunc (min m n) w"
+  by (rule bin_eqI) (auto simp: nth_bintr)
 
-lemma sbintrunc_sbintrunc_min [simp]:
-  "sbintrunc m (sbintrunc n w) = sbintrunc (min m n) w"
-  apply (rule bin_eqI)
-  apply (auto simp: nth_sbintr min.absorb1 min.absorb2)
-  done
+lemma sbintrunc_sbintrunc_min [simp]: "sbintrunc m (sbintrunc n w) = sbintrunc (min m n) w"
+  by (rule bin_eqI) (auto simp: nth_sbintr min.absorb1 min.absorb2)
 
-lemmas bintrunc_Pls = 
+lemmas bintrunc_Pls =
   bintrunc.Suc [where bin="0", simplified bin_last_numeral_simps bin_rest_numeral_simps]
 
-lemmas bintrunc_Min [simp] = 
+lemmas bintrunc_Min [simp] =
   bintrunc.Suc [where bin="-1", simplified bin_last_numeral_simps bin_rest_numeral_simps]
 
-lemmas bintrunc_BIT  [simp] = 
+lemmas bintrunc_BIT  [simp] =
   bintrunc.Suc [where bin="w BIT b", simplified bin_last_BIT bin_rest_BIT] for w b
 
 lemmas bintrunc_Sucs = bintrunc_Pls bintrunc_Min bintrunc_BIT
   bintrunc_Suc_numeral
 
-lemmas sbintrunc_Suc_Pls = 
+lemmas sbintrunc_Suc_Pls =
   sbintrunc.Suc [where bin="0", simplified bin_last_numeral_simps bin_rest_numeral_simps]
 
-lemmas sbintrunc_Suc_Min = 
+lemmas sbintrunc_Suc_Min =
   sbintrunc.Suc [where bin="-1", simplified bin_last_numeral_simps bin_rest_numeral_simps]
 
-lemmas sbintrunc_Suc_BIT [simp] = 
+lemmas sbintrunc_Suc_BIT [simp] =
   sbintrunc.Suc [where bin="w BIT b", simplified bin_last_BIT bin_rest_BIT] for w b
 
 lemmas sbintrunc_Sucs = sbintrunc_Suc_Pls sbintrunc_Suc_Min sbintrunc_Suc_BIT
   sbintrunc_Suc_numeral
 
-lemmas sbintrunc_Pls = 
-  sbintrunc.Z [where bin="0", 
-               simplified bin_last_numeral_simps bin_rest_numeral_simps]
+lemmas sbintrunc_Pls =
+  sbintrunc.Z [where bin="0", simplified bin_last_numeral_simps bin_rest_numeral_simps]
 
-lemmas sbintrunc_Min = 
-  sbintrunc.Z [where bin="-1",
-               simplified bin_last_numeral_simps bin_rest_numeral_simps]
+lemmas sbintrunc_Min =
+  sbintrunc.Z [where bin="-1", simplified bin_last_numeral_simps bin_rest_numeral_simps]
 
-lemmas sbintrunc_0_BIT_B0 [simp] = 
-  sbintrunc.Z [where bin="w BIT False", 
-               simplified bin_last_numeral_simps bin_rest_numeral_simps] for w
+lemmas sbintrunc_0_BIT_B0 [simp] =
+  sbintrunc.Z [where bin="w BIT False", simplified bin_last_numeral_simps bin_rest_numeral_simps]
+  for w
 
-lemmas sbintrunc_0_BIT_B1 [simp] = 
-  sbintrunc.Z [where bin="w BIT True", 
-               simplified bin_last_BIT bin_rest_numeral_simps] for w
+lemmas sbintrunc_0_BIT_B1 [simp] =
+  sbintrunc.Z [where bin="w BIT True", simplified bin_last_BIT bin_rest_numeral_simps]
+  for w
 
 lemmas sbintrunc_0_simps =
   sbintrunc_Pls sbintrunc_Min sbintrunc_0_BIT_B0 sbintrunc_0_BIT_B1
@@ -461,20 +413,18 @@
 lemmas bintrunc_simps = bintrunc.Z bintrunc_Sucs
 lemmas sbintrunc_simps = sbintrunc_0_simps sbintrunc_Sucs
 
-lemma bintrunc_minus:
-  "0 < n ==> bintrunc (Suc (n - 1)) w = bintrunc n w"
+lemma bintrunc_minus: "0 < n \<Longrightarrow> bintrunc (Suc (n - 1)) w = bintrunc n w"
+  by auto
+
+lemma sbintrunc_minus: "0 < n \<Longrightarrow> sbintrunc (Suc (n - 1)) w = sbintrunc n w"
   by auto
 
-lemma sbintrunc_minus:
-  "0 < n ==> sbintrunc (Suc (n - 1)) w = sbintrunc n w"
-  by auto
-
-lemmas bintrunc_minus_simps = 
+lemmas bintrunc_minus_simps =
   bintrunc_Sucs [THEN [2] bintrunc_minus [symmetric, THEN trans]]
-lemmas sbintrunc_minus_simps = 
+lemmas sbintrunc_minus_simps =
   sbintrunc_Sucs [THEN [2] sbintrunc_minus [symmetric, THEN trans]]
 
-lemmas thobini1 = arg_cong [where f = "%w. w BIT b"] for b
+lemmas thobini1 = arg_cong [where f = "\<lambda>w. w BIT b"] for b
 
 lemmas bintrunc_BIT_I = trans [OF bintrunc_BIT thobini1]
 lemmas bintrunc_Min_I = trans [OF bintrunc_Min thobini1]
@@ -484,35 +434,31 @@
 lemmas bintrunc_Min_minus_I = bmsts(2)
 lemmas bintrunc_BIT_minus_I = bmsts(3)
 
-lemma bintrunc_Suc_lem:
-  "bintrunc (Suc n) x = y ==> m = Suc n ==> bintrunc m x = y"
+lemma bintrunc_Suc_lem: "bintrunc (Suc n) x = y \<Longrightarrow> m = Suc n \<Longrightarrow> bintrunc m x = y"
   by auto
 
-lemmas bintrunc_Suc_Ialts = 
+lemmas bintrunc_Suc_Ialts =
   bintrunc_Min_I [THEN bintrunc_Suc_lem]
   bintrunc_BIT_I [THEN bintrunc_Suc_lem]
 
 lemmas sbintrunc_BIT_I = trans [OF sbintrunc_Suc_BIT thobini1]
 
-lemmas sbintrunc_Suc_Is = 
+lemmas sbintrunc_Suc_Is =
   sbintrunc_Sucs(1-3) [THEN thobini1 [THEN [2] trans]]
 
-lemmas sbintrunc_Suc_minus_Is = 
+lemmas sbintrunc_Suc_minus_Is =
   sbintrunc_minus_simps(1-3) [THEN thobini1 [THEN [2] trans]]
 
-lemma sbintrunc_Suc_lem:
-  "sbintrunc (Suc n) x = y ==> m = Suc n ==> sbintrunc m x = y"
+lemma sbintrunc_Suc_lem: "sbintrunc (Suc n) x = y \<Longrightarrow> m = Suc n \<Longrightarrow> sbintrunc m x = y"
   by auto
 
-lemmas sbintrunc_Suc_Ialts = 
+lemmas sbintrunc_Suc_Ialts =
   sbintrunc_Suc_Is [THEN sbintrunc_Suc_lem]
 
-lemma sbintrunc_bintrunc_lt:
-  "m > n ==> sbintrunc n (bintrunc m w) = sbintrunc n w"
+lemma sbintrunc_bintrunc_lt: "m > n \<Longrightarrow> sbintrunc n (bintrunc m w) = sbintrunc n w"
   by (rule bin_eqI) (auto simp: nth_sbintr nth_bintr)
 
-lemma bintrunc_sbintrunc_le:
-  "m <= Suc n ==> bintrunc m (sbintrunc n w) = bintrunc m w"
+lemma bintrunc_sbintrunc_le: "m \<le> Suc n \<Longrightarrow> bintrunc m (sbintrunc n w) = bintrunc m w"
   apply (rule bin_eqI)
   apply (auto simp: nth_sbintr nth_bintr)
    apply (subgoal_tac "x=n", safe, arith+)[1]
@@ -522,19 +468,15 @@
 lemmas bintrunc_sbintrunc [simp] = order_refl [THEN bintrunc_sbintrunc_le]
 lemmas sbintrunc_bintrunc [simp] = lessI [THEN sbintrunc_bintrunc_lt]
 lemmas bintrunc_bintrunc [simp] = order_refl [THEN bintrunc_bintrunc_l]
-lemmas sbintrunc_sbintrunc [simp] = order_refl [THEN sbintrunc_sbintrunc_l] 
+lemmas sbintrunc_sbintrunc [simp] = order_refl [THEN sbintrunc_sbintrunc_l]
 
-lemma bintrunc_sbintrunc' [simp]:
-  "0 < n \<Longrightarrow> bintrunc n (sbintrunc (n - 1) w) = bintrunc n w"
+lemma bintrunc_sbintrunc' [simp]: "0 < n \<Longrightarrow> bintrunc n (sbintrunc (n - 1) w) = bintrunc n w"
   by (cases n) (auto simp del: bintrunc.Suc)
 
-lemma sbintrunc_bintrunc' [simp]:
-  "0 < n \<Longrightarrow> sbintrunc (n - 1) (bintrunc n w) = sbintrunc (n - 1) w"
+lemma sbintrunc_bintrunc' [simp]: "0 < n \<Longrightarrow> sbintrunc (n - 1) (bintrunc n w) = sbintrunc (n - 1) w"
   by (cases n) (auto simp del: bintrunc.Suc)
 
-lemma bin_sbin_eq_iff: 
-  "bintrunc (Suc n) x = bintrunc (Suc n) y \<longleftrightarrow> 
-   sbintrunc n x = sbintrunc n y"
+lemma bin_sbin_eq_iff: "bintrunc (Suc n) x = bintrunc (Suc n) y \<longleftrightarrow> sbintrunc n x = sbintrunc n y"
   apply (rule iffI)
    apply (rule box_equals [OF _ sbintrunc_bintrunc sbintrunc_bintrunc])
    apply simp
@@ -543,8 +485,7 @@
   done
 
 lemma bin_sbin_eq_iff':
-  "0 < n \<Longrightarrow> bintrunc n x = bintrunc n y \<longleftrightarrow> 
-            sbintrunc (n - 1) x = sbintrunc (n - 1) y"
+  "0 < n \<Longrightarrow> bintrunc n x = bintrunc n y \<longleftrightarrow> sbintrunc (n - 1) x = sbintrunc (n - 1) y"
   by (cases n) (simp_all add: bin_sbin_eq_iff del: bintrunc.Suc)
 
 lemmas bintrunc_sbintruncS0 [simp] = bintrunc_sbintrunc' [unfolded One_nat_def]
@@ -557,36 +498,29 @@
   tends to get applied where it's not wanted in developing the theories,
   we get a version for when the word length is given literally *)
 
-lemmas nat_non0_gr = 
+lemmas nat_non0_gr =
   trans [OF iszero_def [THEN Not_eq_iff [THEN iffD2]] refl]
 
 lemma bintrunc_numeral:
-  "bintrunc (numeral k) x =
-    bintrunc (pred_numeral k) (bin_rest x) BIT bin_last x"
+  "bintrunc (numeral k) x = bintrunc (pred_numeral k) (bin_rest x) BIT bin_last x"
   by (simp add: numeral_eq_Suc)
 
 lemma sbintrunc_numeral:
-  "sbintrunc (numeral k) x =
-    sbintrunc (pred_numeral k) (bin_rest x) BIT bin_last x"
+  "sbintrunc (numeral k) x = sbintrunc (pred_numeral k) (bin_rest x) BIT bin_last x"
   by (simp add: numeral_eq_Suc)
 
 lemma bintrunc_numeral_simps [simp]:
-  "bintrunc (numeral k) (numeral (Num.Bit0 w)) =
-    bintrunc (pred_numeral k) (numeral w) BIT False"
-  "bintrunc (numeral k) (numeral (Num.Bit1 w)) =
-    bintrunc (pred_numeral k) (numeral w) BIT True"
-  "bintrunc (numeral k) (- numeral (Num.Bit0 w)) =
-    bintrunc (pred_numeral k) (- numeral w) BIT False"
+  "bintrunc (numeral k) (numeral (Num.Bit0 w)) = bintrunc (pred_numeral k) (numeral w) BIT False"
+  "bintrunc (numeral k) (numeral (Num.Bit1 w)) = bintrunc (pred_numeral k) (numeral w) BIT True"
+  "bintrunc (numeral k) (- numeral (Num.Bit0 w)) = bintrunc (pred_numeral k) (- numeral w) BIT False"
   "bintrunc (numeral k) (- numeral (Num.Bit1 w)) =
     bintrunc (pred_numeral k) (- numeral (w + Num.One)) BIT True"
   "bintrunc (numeral k) 1 = 1"
   by (simp_all add: bintrunc_numeral)
 
 lemma sbintrunc_numeral_simps [simp]:
-  "sbintrunc (numeral k) (numeral (Num.Bit0 w)) =
-    sbintrunc (pred_numeral k) (numeral w) BIT False"
-  "sbintrunc (numeral k) (numeral (Num.Bit1 w)) =
-    sbintrunc (pred_numeral k) (numeral w) BIT True"
+  "sbintrunc (numeral k) (numeral (Num.Bit0 w)) = sbintrunc (pred_numeral k) (numeral w) BIT False"
+  "sbintrunc (numeral k) (numeral (Num.Bit1 w)) = sbintrunc (pred_numeral k) (numeral w) BIT True"
   "sbintrunc (numeral k) (- numeral (Num.Bit0 w)) =
     sbintrunc (pred_numeral k) (- numeral w) BIT False"
   "sbintrunc (numeral k) (- numeral (Num.Bit1 w)) =
@@ -597,49 +531,45 @@
 lemma no_bintr_alt1: "bintrunc n = (\<lambda>w. w mod 2 ^ n :: int)"
   by (rule ext) (rule bintrunc_mod2p)
 
-lemma range_bintrunc: "range (bintrunc n) = {i. 0 <= i & i < 2 ^ n}"
+lemma range_bintrunc: "range (bintrunc n) = {i. 0 \<le> i \<and> i < 2 ^ n}"
   apply (unfold no_bintr_alt1)
   apply (auto simp add: image_iff)
   apply (rule exI)
   apply (auto intro: int_mod_lem [THEN iffD1, symmetric])
   done
 
-lemma no_sbintr_alt2: 
-  "sbintrunc n = (%w. (w + 2 ^ n) mod 2 ^ Suc n - 2 ^ n :: int)"
+lemma no_sbintr_alt2: "sbintrunc n = (\<lambda>w. (w + 2 ^ n) mod 2 ^ Suc n - 2 ^ n :: int)"
   by (rule ext) (simp add : sbintrunc_mod2p)
 
-lemma range_sbintrunc: 
-  "range (sbintrunc n) = {i. - (2 ^ n) <= i & i < 2 ^ n}"
+lemma range_sbintrunc: "range (sbintrunc n) = {i. - (2 ^ n) \<le> i \<and> i < 2 ^ n}"
   apply (unfold no_sbintr_alt2)
   apply (auto simp add: image_iff eq_diff_eq)
   apply (rule exI)
   apply (auto intro: int_mod_lem [THEN iffD1, symmetric])
   done
 
-lemma sb_inc_lem:
-  "(a::int) + 2^k < 0 \<Longrightarrow> a + 2^k + 2^(Suc k) <= (a + 2^k) mod 2^(Suc k)"
+lemma sb_inc_lem: "a + 2^k < 0 \<Longrightarrow> a + 2^k + 2^(Suc k) \<le> (a + 2^k) mod 2^(Suc k)"
+  for a :: int
   apply (erule int_mod_ge' [where n = "2 ^ (Suc k)" and b = "a + 2 ^ k", simplified zless2p])
   apply (rule TrueI)
   done
 
-lemma sb_inc_lem':
-  "(a::int) < - (2^k) \<Longrightarrow> a + 2^k + 2^(Suc k) <= (a + 2^k) mod 2^(Suc k)"
+lemma sb_inc_lem': "a < - (2^k) \<Longrightarrow> a + 2^k + 2^(Suc k) \<le> (a + 2^k) mod 2^(Suc k)"
+  for a :: int
   by (rule sb_inc_lem) simp
 
-lemma sbintrunc_inc:
-  "x < - (2^n) ==> x + 2^(Suc n) <= sbintrunc n x"
+lemma sbintrunc_inc: "x < - (2^n) \<Longrightarrow> x + 2^(Suc n) \<le> sbintrunc n x"
   unfolding no_sbintr_alt2 by (drule sb_inc_lem') simp
 
-lemma sb_dec_lem:
-  "(0::int) \<le> - (2 ^ k) + a \<Longrightarrow> (a + 2 ^ k) mod (2 * 2 ^ k) \<le> - (2 ^ k) + a"
+lemma sb_dec_lem: "0 \<le> - (2 ^ k) + a \<Longrightarrow> (a + 2 ^ k) mod (2 * 2 ^ k) \<le> - (2 ^ k) + a"
+  for a :: int
   using int_mod_le'[where n = "2 ^ (Suc k)" and b = "a + 2 ^ k"] by simp
 
-lemma sb_dec_lem':
-  "(2::int) ^ k \<le> a \<Longrightarrow> (a + 2 ^ k) mod (2 * 2 ^ k) \<le> - (2 ^ k) + a"
+lemma sb_dec_lem': "2 ^ k \<le> a \<Longrightarrow> (a + 2 ^ k) mod (2 * 2 ^ k) \<le> - (2 ^ k) + a"
+  for a :: int
   by (rule sb_dec_lem) simp
 
-lemma sbintrunc_dec:
-  "x >= (2 ^ n) ==> x - 2 ^ (Suc n) >= sbintrunc n x"
+lemma sbintrunc_dec: "x \<ge> (2 ^ n) \<Longrightarrow> x - 2 ^ (Suc n) >= sbintrunc n x"
   unfolding no_sbintr_alt2 by (drule sb_dec_lem') simp
 
 lemmas m2pths = pos_mod_sign pos_mod_bound [OF zless2p]
@@ -659,55 +589,48 @@
 lemma sbintr_lt: "sbintrunc n w < 2 ^ n"
   by (simp add: sbintrunc_mod2p)
 
-lemma sign_Pls_ge_0: 
-  "(bin_sign bin = 0) = (bin >= (0 :: int))"
-  unfolding bin_sign_def by simp
+lemma sign_Pls_ge_0: "bin_sign bin = 0 \<longleftrightarrow> bin \<ge> 0"
+  for bin :: int
+  by (simp add: bin_sign_def)
 
-lemma sign_Min_lt_0: 
-  "(bin_sign bin = -1) = (bin < (0 :: int))"
-  unfolding bin_sign_def by simp
+lemma sign_Min_lt_0: "bin_sign bin = -1 \<longleftrightarrow> bin < 0"
+  for bin :: int
+  by (simp add: bin_sign_def)
 
-lemma bin_rest_trunc:
-  "(bin_rest (bintrunc n bin)) = bintrunc (n - 1) (bin_rest bin)"
+lemma bin_rest_trunc: "bin_rest (bintrunc n bin) = bintrunc (n - 1) (bin_rest bin)"
   by (induct n arbitrary: bin) auto
 
 lemma bin_rest_power_trunc:
-  "(bin_rest ^^ k) (bintrunc n bin) = 
-    bintrunc (n - k) ((bin_rest ^^ k) bin)"
+  "(bin_rest ^^ k) (bintrunc n bin) = bintrunc (n - k) ((bin_rest ^^ k) bin)"
   by (induct k) (auto simp: bin_rest_trunc)
 
-lemma bin_rest_trunc_i:
-  "bintrunc n (bin_rest bin) = bin_rest (bintrunc (Suc n) bin)"
+lemma bin_rest_trunc_i: "bintrunc n (bin_rest bin) = bin_rest (bintrunc (Suc n) bin)"
   by auto
 
-lemma bin_rest_strunc:
-  "bin_rest (sbintrunc (Suc n) bin) = sbintrunc n (bin_rest bin)"
+lemma bin_rest_strunc: "bin_rest (sbintrunc (Suc n) bin) = sbintrunc n (bin_rest bin)"
   by (induct n arbitrary: bin) auto
 
-lemma bintrunc_rest [simp]: 
-  "bintrunc n (bin_rest (bintrunc n bin)) = bin_rest (bintrunc n bin)"
-  apply (induct n arbitrary: bin, simp)
+lemma bintrunc_rest [simp]: "bintrunc n (bin_rest (bintrunc n bin)) = bin_rest (bintrunc n bin)"
+  apply (induct n arbitrary: bin)
+   apply simp
   apply (case_tac bin rule: bin_exhaust)
   apply (auto simp: bintrunc_bintrunc_l)
   done
 
-lemma sbintrunc_rest [simp]:
-  "sbintrunc n (bin_rest (sbintrunc n bin)) = bin_rest (sbintrunc n bin)"
-  apply (induct n arbitrary: bin, simp)
+lemma sbintrunc_rest [simp]: "sbintrunc n (bin_rest (sbintrunc n bin)) = bin_rest (sbintrunc n bin)"
+  apply (induct n arbitrary: bin)
+   apply simp
   apply (case_tac bin rule: bin_exhaust)
   apply (auto simp: bintrunc_bintrunc_l split: bool.splits)
   done
 
-lemma bintrunc_rest':
-  "bintrunc n o bin_rest o bintrunc n = bin_rest o bintrunc n"
+lemma bintrunc_rest': "bintrunc n \<circ> bin_rest \<circ> bintrunc n = bin_rest \<circ> bintrunc n"
   by (rule ext) auto
 
-lemma sbintrunc_rest' :
-  "sbintrunc n o bin_rest o sbintrunc n = bin_rest o sbintrunc n"
+lemma sbintrunc_rest': "sbintrunc n \<circ> bin_rest \<circ> sbintrunc n = bin_rest \<circ> sbintrunc n"
   by (rule ext) auto
 
-lemma rco_lem:
-  "f o g o f = g o f ==> f o (g o f) ^^ n = g ^^ n o f"
+lemma rco_lem: "f \<circ> g \<circ> f = g \<circ> f \<Longrightarrow> f \<circ> (g \<circ> f) ^^ n = g ^^ n \<circ> f"
   apply (rule ext)
   apply (induct_tac n)
    apply (simp_all (no_asm))
@@ -717,27 +640,29 @@
   apply simp
   done
 
-lemmas rco_bintr = bintrunc_rest' 
+lemmas rco_bintr = bintrunc_rest'
   [THEN rco_lem [THEN fun_cong], unfolded o_def]
-lemmas rco_sbintr = sbintrunc_rest' 
+lemmas rco_sbintr = sbintrunc_rest'
   [THEN rco_lem [THEN fun_cong], unfolded o_def]
 
-  
+
 subsection \<open>Splitting and concatenation\<close>
 
-primrec bin_split :: "nat \<Rightarrow> int \<Rightarrow> int \<times> int" where
-  Z: "bin_split 0 w = (w, 0)"
-  | Suc: "bin_split (Suc n) w = (let (w1, w2) = bin_split n (bin_rest w)
-        in (w1, w2 BIT bin_last w))"
+primrec bin_split :: "nat \<Rightarrow> int \<Rightarrow> int \<times> int"
+  where
+    Z: "bin_split 0 w = (w, 0)"
+  | Suc: "bin_split (Suc n) w =
+      (let (w1, w2) = bin_split n (bin_rest w)
+       in (w1, w2 BIT bin_last w))"
 
 lemma [code]:
   "bin_split (Suc n) w = (let (w1, w2) = bin_split n (bin_rest w) in (w1, w2 BIT bin_last w))"
   "bin_split 0 w = (w, 0)"
   by simp_all
 
-primrec bin_cat :: "int \<Rightarrow> nat \<Rightarrow> int \<Rightarrow> int" where
-  Z: "bin_cat w 0 v = w"
+primrec bin_cat :: "int \<Rightarrow> nat \<Rightarrow> int \<Rightarrow> int"
+  where
+    Z: "bin_cat w 0 v = w"
   | Suc: "bin_cat w (Suc n) v = bin_cat w n (bin_rest v) BIT bin_last v"
 
 end
-
diff -r 4ff2ba82d668 -r db7c97cdcfe7 src/HOL/Word/Bits.thy
--- a/src/HOL/Word/Bits.thy	Mon Apr 03 22:18:56 2017 +0200
+++ b/src/HOL/Word/Bits.thy	Mon Apr 03 23:12:44 2017 +0200
@@ -5,35 +5,32 @@
 section \<open>Syntactic classes for bitwise operations\<close>
 
 theory Bits
-imports Main
+  imports Main
 begin
 
 class bit =
-  fixes bitNOT :: "'a \<Rightarrow> 'a"       ("NOT _" [70] 71)
-    and bitAND :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixr "AND" 64)
-    and bitOR  :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixr "OR"  59)
-    and bitXOR :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixr "XOR" 59)
+  fixes bitNOT :: "'a \<Rightarrow> 'a"  ("NOT _" [70] 71)
+    and bitAND :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"  (infixr "AND" 64)
+    and bitOR :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"  (infixr "OR"  59)
+    and bitXOR :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"  (infixr "XOR" 59)
 
 text \<open>
   We want the bitwise operations to bind slightly weaker
-  than \<open>+\<close> and \<open>-\<close>, but \<open>~~\<close> to 
+  than \<open>+\<close> and \<open>-\<close>, but \<open>~~\<close> to
   bind slightly stronger than \<open>*\<close>.
 \<close>
 
-text \<open>
-  Testing and shifting operations.
-\<close>
+text \<open>Testing and shifting operations.\<close>
 
 class bits = bit +
-  fixes test_bit :: "'a \<Rightarrow> nat \<Rightarrow> bool" (infixl "!!" 100)
-    and lsb      :: "'a \<Rightarrow> bool"
-    and set_bit  :: "'a \<Rightarrow> nat \<Rightarrow> bool \<Rightarrow> 'a"
-    and set_bits :: "(nat \<Rightarrow> bool) \<Rightarrow> 'a" (binder "BITS " 10)
-    and shiftl   :: "'a \<Rightarrow> nat \<Rightarrow> 'a" (infixl "<<" 55)
-    and shiftr   :: "'a \<Rightarrow> nat \<Rightarrow> 'a" (infixl ">>" 55)
+  fixes test_bit :: "'a \<Rightarrow> nat \<Rightarrow> bool"  (infixl "!!" 100)
+    and lsb :: "'a \<Rightarrow> bool"
+    and set_bit :: "'a \<Rightarrow> nat \<Rightarrow> bool \<Rightarrow> 'a"
+    and set_bits :: "(nat \<Rightarrow> bool) \<Rightarrow> 'a"  (binder "BITS " 10)
+    and shiftl :: "'a \<Rightarrow> nat \<Rightarrow> 'a"  (infixl "<<" 55)
+    and shiftr :: "'a \<Rightarrow> nat \<Rightarrow> 'a"  (infixl ">>" 55)
 
 class bitss = bits +
-  fixes msb      :: "'a \<Rightarrow> bool"
+  fixes msb :: "'a \<Rightarrow> bool"
 
 end
-
diff -r 4ff2ba82d668 -r db7c97cdcfe7 src/HOL/Word/Bits_Bit.thy
--- a/src/HOL/Word/Bits_Bit.thy	Mon Apr 03 22:18:56 2017 +0200
+++ b/src/HOL/Word/Bits_Bit.thy	Mon Apr 03 23:12:44 2017 +0200
@@ -11,20 +11,24 @@
 instantiation bit :: bit
 begin
 
-primrec bitNOT_bit where
-  "NOT 0 = (1::bit)"
+primrec bitNOT_bit
+  where
+    "NOT 0 = (1::bit)"
   | "NOT 1 = (0::bit)"
 
-primrec bitAND_bit where
-  "0 AND y = (0::bit)"
+primrec bitAND_bit
+  where
+    "0 AND y = (0::bit)"
   | "1 AND y = (y::bit)"
 
-primrec bitOR_bit where
-  "0 OR y = (y::bit)"
+primrec bitOR_bit
+  where
+    "0 OR y = (y::bit)"
   | "1 OR y = (1::bit)"
 
-primrec bitXOR_bit where
-  "0 XOR y = (y::bit)"
+primrec bitXOR_bit
+  where
+    "0 XOR y = (y::bit)"
   | "1 XOR y = (NOT y :: bit)"
 
 instance  ..
@@ -34,40 +38,48 @@
 lemmas bit_simps =
   bitNOT_bit.simps bitAND_bit.simps bitOR_bit.simps bitXOR_bit.simps
 
-lemma bit_extra_simps [simp]: 
-  "x AND 0 = (0::bit)"
-  "x AND 1 = (x::bit)"
-  "x OR 1 = (1::bit)"
-  "x OR 0 = (x::bit)"
-  "x XOR 1 = NOT (x::bit)"
-  "x XOR 0 = (x::bit)"
+lemma bit_extra_simps [simp]:
+  "x AND 0 = 0"
+  "x AND 1 = x"
+  "x OR 1 = 1"
+  "x OR 0 = x"
+  "x XOR 1 = NOT x"
+  "x XOR 0 = x"
+  for x :: bit
   by (cases x, auto)+
 
-lemma bit_ops_comm: 
-  "(x::bit) AND y = y AND x"
-  "(x::bit) OR y = y OR x"
-  "(x::bit) XOR y = y XOR x"
+lemma bit_ops_comm:
+  "x AND y = y AND x"
+  "x OR y = y OR x"
+  "x XOR y = y XOR x"
+  for x :: bit
   by (cases y, auto)+
 
-lemma bit_ops_same [simp]: 
-  "(x::bit) AND x = x"
-  "(x::bit) OR x = x"
-  "(x::bit) XOR x = 0"
+lemma bit_ops_same [simp]:
+  "x AND x = x"
+  "x OR x = x"
+  "x XOR x = 0"
+  for x :: bit
   by (cases x, auto)+
 
-lemma bit_not_not [simp]: "NOT (NOT (x::bit)) = x"
+lemma bit_not_not [simp]: "NOT (NOT x) = x"
+  for x :: bit
   by (cases x) auto
 
-lemma bit_or_def: "(b::bit) OR c = NOT (NOT b AND NOT c)"
-  by (induct b, simp_all)
+lemma bit_or_def: "b OR c = NOT (NOT b AND NOT c)"
+  for b c :: bit
+  by (induct b) simp_all
 
-lemma bit_xor_def: "(b::bit) XOR c = (b AND NOT c) OR (NOT b AND c)"
-  by (induct b, simp_all)
+lemma bit_xor_def: "b XOR c = (b AND NOT c) OR (NOT b AND c)"
+  for b c :: bit
+  by (induct b) simp_all
 
-lemma bit_NOT_eq_1_iff [simp]: "NOT (b::bit) = 1 \<longleftrightarrow> b = 0"
-  by (induct b, simp_all)
+lemma bit_NOT_eq_1_iff [simp]: "NOT b = 1 \<longleftrightarrow> b = 0"
+  for b :: bit
+  by (induct b) simp_all
 
-lemma bit_AND_eq_1_iff [simp]: "(a::bit) AND b = 1 \<longleftrightarrow> a = 1 \<and> b = 1"
-  by (induct a, simp_all)
+lemma bit_AND_eq_1_iff [simp]: "a AND b = 1 \<longleftrightarrow> a = 1 \<and> b = 1"
+  for a b :: bit
+  by (induct a) simp_all
 
 end
diff -r 4ff2ba82d668 -r db7c97cdcfe7 src/HOL/Word/Bits_Int.thy
--- a/src/HOL/Word/Bits_Int.thy	Mon Apr 03 22:18:56 2017 +0200
+++ b/src/HOL/Word/Bits_Int.thy	Mon Apr 03 23:12:44 2017 +0200
@@ -1,15 +1,15 @@
-(* 
-  Author: Jeremy Dawson and Gerwin Klein, NICTA
+(*  Title:      HOL/Word/Bits_Int.thy
+    Author:     Jeremy Dawson and Gerwin Klein, NICTA
 
-  Definitions and basic theorems for bit-wise logical operations 
-  for integers expressed using Pls, Min, BIT,
-  and converting them to and from lists of bools.
-*) 
+Definitions and basic theorems for bit-wise logical operations
+for integers expressed using Pls, Min, BIT,
+and converting them to and from lists of bools.
+*)
 
 section \<open>Bitwise Operations on Binary Integers\<close>
 
 theory Bits_Int
-imports Bits Bit_Representation
+  imports Bits Bit_Representation
 begin
 
 subsection \<open>Logical operations\<close>
@@ -19,17 +19,16 @@
 instantiation int :: bit
 begin
 
-definition int_not_def:
-  "bitNOT = (\<lambda>x::int. - x - 1)"
+definition int_not_def: "bitNOT = (\<lambda>x::int. - x - 1)"
 
-function bitAND_int where
-  "bitAND_int x y =
-    (if x = 0 then 0 else if x = -1 then y else
-      (bin_rest x AND bin_rest y) BIT (bin_last x \<and> bin_last y))"
+function bitAND_int
+  where "bitAND_int x y =
+    (if x = 0 then 0 else if x = -1 then y
+     else (bin_rest x AND bin_rest y) BIT (bin_last x \<and> bin_last y))"
   by pat_completeness simp
 
 termination
-  by (relation "measure (nat o abs o fst)", simp_all add: bin_rest_def)
+  by (relation "measure (nat \<circ> abs \<circ> fst)", simp_all add: bin_rest_def)
 
 declare bitAND_int.simps [simp del]
 
@@ -67,8 +66,8 @@
 lemma int_and_m1 [simp]: "(-1::int) AND x = x"
   by (simp add: bitAND_int.simps)
 
-lemma int_and_Bits [simp]: 
-  "(x BIT b) AND (y BIT c) = (x AND y) BIT (b \<and> c)" 
+lemma int_and_Bits [simp]:
+  "(x BIT b) AND (y BIT c) = (x AND y) BIT (b \<and> c)"
   by (subst bitAND_int.simps, simp add: Bit_eq_0_iff Bit_eq_m1_iff)
 
 lemma int_or_zero [simp]: "(0::int) OR x = x"
@@ -77,14 +76,14 @@
 lemma int_or_minus1 [simp]: "(-1::int) OR x = -1"
   unfolding int_or_def by simp
 
-lemma int_or_Bits [simp]: 
+lemma int_or_Bits [simp]:
   "(x BIT b) OR (y BIT c) = (x OR y) BIT (b \<or> c)"
   unfolding int_or_def by simp
 
 lemma int_xor_zero [simp]: "(0::int) XOR x = x"
   unfolding int_xor_def by simp
 
-lemma int_xor_Bits [simp]: 
+lemma int_xor_Bits [simp]:
   "(x BIT b) XOR (y BIT c) = (x XOR y) BIT ((b \<or> c) \<and> \<not> (b \<and> c))"
   unfolding int_xor_def by auto
 
@@ -115,9 +114,9 @@
   by (cases x rule: bin_exhaust, cases y rule: bin_exhaust, simp)
 
 lemma bin_nth_ops:
-  "!!x y. bin_nth (x AND y) n = (bin_nth x n & bin_nth y n)" 
+  "!!x y. bin_nth (x AND y) n = (bin_nth x n & bin_nth y n)"
   "!!x y. bin_nth (x OR y) n = (bin_nth x n | bin_nth y n)"
-  "!!x y. bin_nth (x XOR y) n = (bin_nth x n ~= bin_nth y n)" 
+  "!!x y. bin_nth (x XOR y) n = (bin_nth x n ~= bin_nth y n)"
   "!!x. bin_nth (NOT x) n = (~ bin_nth x n)"
   by (induct n) auto
 
@@ -150,18 +149,18 @@
   by (auto simp add: bin_eq_iff bin_nth_ops)
 
 lemma bin_ops_same [simp]:
-  "(x::int) AND x = x" 
-  "(x::int) OR x = x" 
+  "(x::int) AND x = x"
+  "(x::int) OR x = x"
   "(x::int) XOR x = 0"
   by (auto simp add: bin_eq_iff bin_nth_ops)
 
-lemmas bin_log_esimps = 
+lemmas bin_log_esimps =
   int_and_extra_simps  int_or_extra_simps  int_xor_extra_simps
   int_and_0 int_and_m1 int_or_zero int_or_minus1 int_xor_zero int_xor_minus1
 
 (* basic properties of logical (bit-wise) operations *)
 
-lemma bbw_ao_absorb: 
+lemma bbw_ao_absorb:
   "!!y::int. x AND (y OR x) = x & x OR (y AND x) = x"
   by (auto simp add: bin_eq_iff bin_nth_ops)
 
@@ -174,7 +173,7 @@
 lemmas bbw_ao_absorbs [simp] = bbw_ao_absorb bbw_ao_absorbs_other
 
 lemma int_xor_not:
-  "!!y::int. (NOT x) XOR y = NOT (x XOR y) & 
+  "!!y::int. (NOT x) XOR y = NOT (x XOR y) &
         x XOR (NOT y) = NOT (x XOR y)"
   by (auto simp add: bin_eq_iff bin_nth_ops)
 
@@ -193,30 +192,30 @@
 lemmas bbw_assocs = int_and_assoc int_or_assoc int_xor_assoc
 
 (* BH: Why are these declared as simp rules??? *)
-lemma bbw_lcs [simp]: 
+lemma bbw_lcs [simp]:
   "(y::int) AND (x AND z) = x AND (y AND z)"
   "(y::int) OR (x OR z) = x OR (y OR z)"
-  "(y::int) XOR (x XOR z) = x XOR (y XOR z)" 
+  "(y::int) XOR (x XOR z) = x XOR (y XOR z)"
   by (auto simp add: bin_eq_iff bin_nth_ops)
 
-lemma bbw_not_dist: 
-  "!!y::int. NOT (x OR y) = (NOT x) AND (NOT y)" 
+lemma bbw_not_dist:
+  "!!y::int. NOT (x OR y) = (NOT x) AND (NOT y)"
   "!!y::int. NOT (x AND y) = (NOT x) OR (NOT y)"
   by (auto simp add: bin_eq_iff bin_nth_ops)
 
-lemma bbw_oa_dist: 
-  "!!y z::int. (x AND y) OR z = 
+lemma bbw_oa_dist:
+  "!!y z::int. (x AND y) OR z =
           (x OR z) AND (y OR z)"
   by (auto simp add: bin_eq_iff bin_nth_ops)
 
-lemma bbw_ao_dist: 
-  "!!y z::int. (x OR y) AND z = 
+lemma bbw_ao_dist:
+  "!!y z::int. (x OR y) AND z =
           (x AND z) OR (y AND z)"
   by (auto simp add: bin_eq_iff bin_nth_ops)
 
 (*
 Why were these declared simp???
-declare bin_ops_comm [simp] bbw_assocs [simp] 
+declare bin_ops_comm [simp] bbw_assocs [simp]
 *)
 
 subsubsection \<open>Simplification with numerals\<close>
@@ -360,17 +359,17 @@
 
 subsubsection \<open>Truncating results of bit-wise operations\<close>
 
-lemma bin_trunc_ao: 
-  "!!x y. (bintrunc n x) AND (bintrunc n y) = bintrunc n (x AND y)" 
+lemma bin_trunc_ao:
+  "!!x y. (bintrunc n x) AND (bintrunc n y) = bintrunc n (x AND y)"
   "!!x y. (bintrunc n x) OR (bintrunc n y) = bintrunc n (x OR y)"
   by (auto simp add: bin_eq_iff bin_nth_ops nth_bintr)
 
-lemma bin_trunc_xor: 
-  "!!x y. bintrunc n (bintrunc n x XOR bintrunc n y) = 
+lemma bin_trunc_xor:
+  "!!x y. bintrunc n (bintrunc n x XOR bintrunc n y) =
           bintrunc n (x XOR y)"
   by (auto simp add: bin_eq_iff bin_nth_ops nth_bintr)
 
-lemma bin_trunc_not: 
+lemma bin_trunc_not:
   "!!x. bintrunc n (NOT (bintrunc n x)) = bintrunc n (NOT x)"
   by (auto simp add: bin_eq_iff bin_nth_ops nth_bintr)
 
@@ -392,26 +391,26 @@
   Z: "bin_sc 0 b w = bin_rest w BIT b"
   | Suc: "bin_sc (Suc n) b w = bin_sc n b (bin_rest w) BIT bin_last w"
 
-lemma bin_nth_sc [simp]: 
+lemma bin_nth_sc [simp]:
   "bin_nth (bin_sc n b w) n \<longleftrightarrow> b"
   by (induct n arbitrary: w) auto
 
-lemma bin_sc_sc_same [simp]: 
+lemma bin_sc_sc_same [simp]:
   "bin_sc n c (bin_sc n b w) = bin_sc n c w"
   by (induct n arbitrary: w) auto
 
 lemma bin_sc_sc_diff:
-  "m ~= n ==> 
+  "m ~= n ==>
     bin_sc m c (bin_sc n b w) = bin_sc n b (bin_sc m c w)"
   apply (induct n arbitrary: w m)
    apply (case_tac [!] m)
      apply auto
   done
 
-lemma bin_nth_sc_gen: 
+lemma bin_nth_sc_gen:
   "bin_nth (bin_sc n b w) m = (if m = n then b else bin_nth w m)"
   by (induct n arbitrary: w m) (case_tac [!] m, auto)
-  
+
 lemma bin_sc_nth [simp]:
   "(bin_sc n (bin_nth w n) w) = w"
   by (induct n arbitrary: w) auto
@@ -419,8 +418,8 @@
 lemma bin_sign_sc [simp]:
   "bin_sign (bin_sc n b w) = bin_sign w"
   by (induct n arbitrary: w) auto
-  
-lemma bin_sc_bintr [simp]: 
+
+lemma bin_sc_bintr [simp]:
   "bintrunc m (bin_sc n x (bintrunc m (w))) = bintrunc m (bin_sc n x w)"
   apply (induct n arbitrary: w m)
    apply (case_tac [!] w rule: bin_exhaust)
@@ -464,14 +463,14 @@
 
 lemma bin_sc_TM [simp]: "bin_sc n True (- 1) = - 1"
   by (induct n) auto
-  
+
 lemmas bin_sc_simps = bin_sc.Z bin_sc.Suc bin_sc_TM bin_sc_FP
 
 lemma bin_sc_minus:
   "0 < n ==> bin_sc (Suc (n - 1)) b w = bin_sc n b w"
   by auto
 
-lemmas bin_sc_Suc_minus = 
+lemmas bin_sc_Suc_minus =
   trans [OF bin_sc_minus [symmetric] bin_sc.Suc]
 
 lemma bin_sc_numeral [simp]:
@@ -490,7 +489,7 @@
 where
   "bin_rsplit_aux n m c bs =
     (if m = 0 | n = 0 then bs else
-      let (a, b) = bin_split n c 
+      let (a, b) = bin_split n c
       in bin_rsplit_aux n (m - n) a (b # bs))"
 
 definition bin_rsplit :: "nat \<Rightarrow> nat \<times> int \<Rightarrow> int list"
@@ -501,7 +500,7 @@
 where
   "bin_rsplitl_aux n m c bs =
     (if m = 0 | n = 0 then bs else
-      let (a, b) = bin_split (min m n) c 
+      let (a, b) = bin_split (min m n) c
       in bin_rsplitl_aux n (m - n) a (b # bs))"
 
 definition bin_rsplitl :: "nat \<Rightarrow> nat \<times> int \<Rightarrow> int list"
@@ -511,7 +510,7 @@
 declare bin_rsplit_aux.simps [simp del]
 declare bin_rsplitl_aux.simps [simp del]
 
-lemma bin_sign_cat: 
+lemma bin_sign_cat:
   "bin_sign (bin_cat x n y) = bin_sign x"
   by (induct n arbitrary: y) auto
 
@@ -519,8 +518,8 @@
   "bin_cat w (Suc n) (v BIT b) = bin_cat w n v BIT b"
   by auto
 
-lemma bin_nth_cat: 
-  "bin_nth (bin_cat x k y) n = 
+lemma bin_nth_cat:
+  "bin_nth (bin_cat x k y) n =
     (if n < k then bin_nth y n else bin_nth x (n - k))"
   apply (induct k arbitrary: n y)
    apply clarsimp
@@ -528,8 +527,8 @@
   done
 
 lemma bin_nth_split:
-  "bin_split n c = (a, b) ==> 
-    (ALL k. bin_nth a k = bin_nth c (n + k)) & 
+  "bin_split n c = (a, b) ==>
+    (ALL k. bin_nth a k = bin_nth c (n + k)) &
     (ALL k. bin_nth b k = (k < n & bin_nth c k))"
   apply (induct n arbitrary: b c)
    apply clarsimp
@@ -538,8 +537,8 @@
   apply auto
   done
 
-lemma bin_cat_assoc: 
-  "bin_cat (bin_cat x m y) n z = bin_cat x (m + n) (bin_cat y n z)" 
+lemma bin_cat_assoc:
+  "bin_cat (bin_cat x m y) n z = bin_cat x (m + n) (bin_cat y n z)"
   by (induct n arbitrary: z) auto
 
 lemma bin_cat_assoc_sym:
@@ -551,23 +550,23 @@
 lemma bin_cat_zero [simp]: "bin_cat 0 n w = bintrunc n w"
   by (induct n arbitrary: w) auto
 
-lemma bintr_cat1: 
+lemma bintr_cat1:
   "bintrunc (k + n) (bin_cat a n b) = bin_cat (bintrunc k a) n b"
   by (induct n arbitrary: b) auto
-    
-lemma bintr_cat: "bintrunc m (bin_cat a n b) = 
+
+lemma bintr_cat: "bintrunc m (bin_cat a n b) =
     bin_cat (bintrunc (m - n) a) n (bintrunc (min m n) b)"
   by (rule bin_eqI) (auto simp: bin_nth_cat nth_bintr)
-    
-lemma bintr_cat_same [simp]: 
+
+lemma bintr_cat_same [simp]:
   "bintrunc n (bin_cat a n b) = bintrunc n b"
   by (auto simp add : bintr_cat)
 
-lemma cat_bintr [simp]: 
+lemma cat_bintr [simp]:
   "bin_cat a n (bintrunc n b) = bin_cat a n b"
   by (induct n arbitrary: b) auto
 
-lemma split_bintrunc: 
+lemma split_bintrunc:
   "bin_split n c = (a, b) ==> b = bintrunc n c"
   by (induct n arbitrary: b c) (auto simp: Let_def split: prod.split_asm)
 
@@ -587,7 +586,7 @@
   by (induct n) auto
 
 lemma bin_split_trunc:
-  "bin_split (min m n) c = (a, b) ==> 
+  "bin_split (min m n) c = (a, b) ==>
     bin_split n (bintrunc m c) = (bintrunc (m - n) a, b)"
   apply (induct n arbitrary: m b c, clarsimp)
   apply (simp add: bin_rest_trunc Let_def split: prod.split_asm)
@@ -596,7 +595,7 @@
   done
 
 lemma bin_split_trunc1:
-  "bin_split n c = (a, b) ==> 
+  "bin_split n c = (a, b) ==>
     bin_split n (bintrunc m c) = (bintrunc (m - n) a, bintrunc m b)"
   apply (induct n arbitrary: m b c, clarsimp)
   apply (simp add: bin_rest_trunc Let_def split: prod.split_asm)
@@ -621,12 +620,12 @@
 
 subsection \<open>Miscellaneous lemmas\<close>
 
-lemma nth_2p_bin: 
+lemma nth_2p_bin:
   "bin_nth (2 ^ n) m = (m = n)"
   apply (induct n arbitrary: m)
    apply clarsimp
    apply safe
-   apply (case_tac m) 
+   apply (case_tac m)
     apply (auto simp: Bit_B0_2t [symmetric])
   done
 
diff -r 4ff2ba82d668 -r db7c97cdcfe7 src/HOL/Word/Bool_List_Representation.thy
--- a/src/HOL/Word/Bool_List_Representation.thy	Mon Apr 03 22:18:56 2017 +0200
+++ b/src/HOL/Word/Bool_List_Representation.thy	Mon Apr 03 23:12:44 2017 +0200
@@ -1,177 +1,156 @@
-(* 
-  Author: Jeremy Dawson, NICTA
+(*  Title:      HOL/Word/Bool_List_Representation.thy
+    Author:     Jeremy Dawson, NICTA
 
-  Theorems to do with integers, expressed using Pls, Min, BIT,
-  theorems linking them to lists of booleans, and repeated splitting 
-  and concatenation.
-*) 
+Theorems to do with integers, expressed using Pls, Min, BIT,
+theorems linking them to lists of booleans, and repeated splitting
+and concatenation.
+*)
 
 section "Bool lists and integers"
 
 theory Bool_List_Representation
-imports Main Bits_Int
+  imports Bits_Int
 begin
 
 definition map2 :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'a list \<Rightarrow> 'b list \<Rightarrow> 'c list"
-where
-  "map2 f as bs = map (case_prod f) (zip as bs)"
+  where "map2 f as bs = map (case_prod f) (zip as bs)"
 
-lemma map2_Nil [simp, code]:
-  "map2 f [] ys = []"
-  unfolding map2_def by auto
+lemma map2_Nil [simp, code]: "map2 f [] ys = []"
+  by (auto simp: map2_def)
 
-lemma map2_Nil2 [simp, code]:
-  "map2 f xs [] = []"
-  unfolding map2_def by auto
+lemma map2_Nil2 [simp, code]: "map2 f xs [] = []"
+  by (auto simp: map2_def)
 
-lemma map2_Cons [simp, code]:
-  "map2 f (x # xs) (y # ys) = f x y # map2 f xs ys"
-  unfolding map2_def by auto
+lemma map2_Cons [simp, code]: "map2 f (x # xs) (y # ys) = f x y # map2 f xs ys"
+  by (auto simp: map2_def)
 
 
 subsection \<open>Operations on lists of booleans\<close>
 
 primrec bl_to_bin_aux :: "bool list \<Rightarrow> int \<Rightarrow> int"
-where
-  Nil: "bl_to_bin_aux [] w = w"
-  | Cons: "bl_to_bin_aux (b # bs) w = 
-      bl_to_bin_aux bs (w BIT b)"
+  where
+    Nil: "bl_to_bin_aux [] w = w"
+  | Cons: "bl_to_bin_aux (b # bs) w = bl_to_bin_aux bs (w BIT b)"
 
 definition bl_to_bin :: "bool list \<Rightarrow> int"
-where
-  bl_to_bin_def: "bl_to_bin bs = bl_to_bin_aux bs 0"
+  where "bl_to_bin bs = bl_to_bin_aux bs 0"
 
 primrec bin_to_bl_aux :: "nat \<Rightarrow> int \<Rightarrow> bool list \<Rightarrow> bool list"
-where
-  Z: "bin_to_bl_aux 0 w bl = bl"
-  | Suc: "bin_to_bl_aux (Suc n) w bl =
-      bin_to_bl_aux n (bin_rest w) ((bin_last w) # bl)"
+  where
+    Z: "bin_to_bl_aux 0 w bl = bl"
+  | Suc: "bin_to_bl_aux (Suc n) w bl = bin_to_bl_aux n (bin_rest w) ((bin_last w) # bl)"
 
 definition bin_to_bl :: "nat \<Rightarrow> int \<Rightarrow> bool list"
-where
-  bin_to_bl_def : "bin_to_bl n w = bin_to_bl_aux n w []"
+  where "bin_to_bl n w = bin_to_bl_aux n w []"
 
 primrec bl_of_nth :: "nat \<Rightarrow> (nat \<Rightarrow> bool) \<Rightarrow> bool list"
-where
-  Suc: "bl_of_nth (Suc n) f = f n # bl_of_nth n f"
+  where
+    Suc: "bl_of_nth (Suc n) f = f n # bl_of_nth n f"
   | Z: "bl_of_nth 0 f = []"
 
 primrec takefill :: "'a \<Rightarrow> nat \<Rightarrow> 'a list \<Rightarrow> 'a list"
 where
-  Z: "takefill fill 0 xs = []"
-  | Suc: "takefill fill (Suc n) xs = (
-      case xs of [] => fill # takefill fill n xs
-        | y # ys => y # takefill fill n ys)"
+    Z: "takefill fill 0 xs = []"
+  | Suc: "takefill fill (Suc n) xs =
+      (case xs of
+        [] \<Rightarrow> fill # takefill fill n xs
+      | y # ys \<Rightarrow> y # takefill fill n ys)"
 
 
 subsection "Arithmetic in terms of bool lists"
 
 text \<open>
   Arithmetic operations in terms of the reversed bool list,
-  assuming input list(s) the same length, and don't extend them. 
+  assuming input list(s) the same length, and don't extend them.
 \<close>
 
-primrec rbl_succ :: "bool list => bool list"
-where
-  Nil: "rbl_succ Nil = Nil"
+primrec rbl_succ :: "bool list \<Rightarrow> bool list"
+  where
+    Nil: "rbl_succ Nil = Nil"
   | Cons: "rbl_succ (x # xs) = (if x then False # rbl_succ xs else True # xs)"
 
-primrec rbl_pred :: "bool list => bool list"
-where
-  Nil: "rbl_pred Nil = Nil"
+primrec rbl_pred :: "bool list \<Rightarrow> bool list"
+  where
+    Nil: "rbl_pred Nil = Nil"
   | Cons: "rbl_pred (x # xs) = (if x then False # xs else True # rbl_pred xs)"
 
-primrec rbl_add :: "bool list => bool list => bool list"
-where
-  \<comment> "result is length of first arg, second arg may be longer"
-  Nil: "rbl_add Nil x = Nil"
-  | Cons: "rbl_add (y # ys) x = (let ws = rbl_add ys (tl x) in 
-    (y ~= hd x) # (if hd x & y then rbl_succ ws else ws))"
+primrec rbl_add :: "bool list \<Rightarrow> bool list \<Rightarrow> bool list"
+  where \<comment> "result is length of first arg, second arg may be longer"
+    Nil: "rbl_add Nil x = Nil"
+  | Cons: "rbl_add (y # ys) x =
+      (let ws = rbl_add ys (tl x)
+       in (y \<noteq> hd x) # (if hd x \<and> y then rbl_succ ws else ws))"
 
-primrec rbl_mult :: "bool list => bool list => bool list"
-where
-  \<comment> "result is length of first arg, second arg may be longer"
-  Nil: "rbl_mult Nil x = Nil"
-  | Cons: "rbl_mult (y # ys) x = (let ws = False # rbl_mult ys x in 
-    if y then rbl_add ws x else ws)"
+primrec rbl_mult :: "bool list \<Rightarrow> bool list \<Rightarrow> bool list"
+  where \<comment> "result is length of first arg, second arg may be longer"
+    Nil: "rbl_mult Nil x = Nil"
+  | Cons: "rbl_mult (y # ys) x =
+      (let ws = False # rbl_mult ys x
+       in if y then rbl_add ws x else ws)"
 
-lemma butlast_power:
-  "(butlast ^^ n) bl = take (length bl - n) bl"
+lemma butlast_power: "(butlast ^^ n) bl = take (length bl - n) bl"
   by (induct n) (auto simp: butlast_take)
 
 lemma bin_to_bl_aux_zero_minus_simp [simp]:
-  "0 < n \<Longrightarrow> bin_to_bl_aux n 0 bl = 
-    bin_to_bl_aux (n - 1) 0 (False # bl)"
+  "0 < n \<Longrightarrow> bin_to_bl_aux n 0 bl = bin_to_bl_aux (n - 1) 0 (False # bl)"
   by (cases n) auto
 
 lemma bin_to_bl_aux_minus1_minus_simp [simp]:
-  "0 < n ==> bin_to_bl_aux n (- 1) bl = 
-    bin_to_bl_aux (n - 1) (- 1) (True # bl)"
+  "0 < n \<Longrightarrow> bin_to_bl_aux n (- 1) bl = bin_to_bl_aux (n - 1) (- 1) (True # bl)"
   by (cases n) auto
 
 lemma bin_to_bl_aux_one_minus_simp [simp]:
-  "0 < n \<Longrightarrow> bin_to_bl_aux n 1 bl = 
-    bin_to_bl_aux (n - 1) 0 (True # bl)"
+  "0 < n \<Longrightarrow> bin_to_bl_aux n 1 bl = bin_to_bl_aux (n - 1) 0 (True # bl)"
   by (cases n) auto
 
 lemma bin_to_bl_aux_Bit_minus_simp [simp]:
-  "0 < n ==> bin_to_bl_aux n (w BIT b) bl = 
-    bin_to_bl_aux (n - 1) w (b # bl)"
+  "0 < n \<Longrightarrow> bin_to_bl_aux n (w BIT b) bl = bin_to_bl_aux (n - 1) w (b # bl)"
   by (cases n) auto
 
 lemma bin_to_bl_aux_Bit0_minus_simp [simp]:
-  "0 < n ==> bin_to_bl_aux n (numeral (Num.Bit0 w)) bl = 
-    bin_to_bl_aux (n - 1) (numeral w) (False # bl)"
+  "0 < n \<Longrightarrow>
+    bin_to_bl_aux n (numeral (Num.Bit0 w)) bl = bin_to_bl_aux (n - 1) (numeral w) (False # bl)"
   by (cases n) auto
 
 lemma bin_to_bl_aux_Bit1_minus_simp [simp]:
-  "0 < n ==> bin_to_bl_aux n (numeral (Num.Bit1 w)) bl = 
-    bin_to_bl_aux (n - 1) (numeral w) (True # bl)"
+  "0 < n \<Longrightarrow>
+    bin_to_bl_aux n (numeral (Num.Bit1 w)) bl = bin_to_bl_aux (n - 1) (numeral w) (True # bl)"
   by (cases n) auto
 
 text \<open>Link between bin and bool list.\<close>
 
-lemma bl_to_bin_aux_append: 
-  "bl_to_bin_aux (bs @ cs) w = bl_to_bin_aux cs (bl_to_bin_aux bs w)"
+lemma bl_to_bin_aux_append: "bl_to_bin_aux (bs @ cs) w = bl_to_bin_aux cs (bl_to_bin_aux bs w)"
   by (induct bs arbitrary: w) auto
 
-lemma bin_to_bl_aux_append: 
-  "bin_to_bl_aux n w bs @ cs = bin_to_bl_aux n w (bs @ cs)"
+lemma bin_to_bl_aux_append: "bin_to_bl_aux n w bs @ cs = bin_to_bl_aux n w (bs @ cs)"
   by (induct n arbitrary: w bs) auto
 
-lemma bl_to_bin_append: 
-  "bl_to_bin (bs @ cs) = bl_to_bin_aux cs (bl_to_bin bs)"
+lemma bl_to_bin_append: "bl_to_bin (bs @ cs) = bl_to_bin_aux cs (bl_to_bin bs)"
   unfolding bl_to_bin_def by (rule bl_to_bin_aux_append)
 
-lemma bin_to_bl_aux_alt: 
-  "bin_to_bl_aux n w bs = bin_to_bl n w @ bs" 
-  unfolding bin_to_bl_def by (simp add : bin_to_bl_aux_append)
+lemma bin_to_bl_aux_alt: "bin_to_bl_aux n w bs = bin_to_bl n w @ bs"
+  by (simp add: bin_to_bl_def bin_to_bl_aux_append)
 
 lemma bin_to_bl_0 [simp]: "bin_to_bl 0 bs = []"
-  unfolding bin_to_bl_def by auto
+  by (auto simp: bin_to_bl_def)
 
-lemma size_bin_to_bl_aux: 
-  "size (bin_to_bl_aux n w bs) = n + length bs"
+lemma size_bin_to_bl_aux: "size (bin_to_bl_aux n w bs) = n + length bs"
   by (induct n arbitrary: w bs) auto
 
-lemma size_bin_to_bl [simp]: "size (bin_to_bl n w) = n" 
-  unfolding bin_to_bl_def by (simp add : size_bin_to_bl_aux)
+lemma size_bin_to_bl [simp]: "size (bin_to_bl n w) = n"
+  by (simp add: bin_to_bl_def size_bin_to_bl_aux)
 
-lemma bin_bl_bin': 
-  "bl_to_bin (bin_to_bl_aux n w bs) = 
-    bl_to_bin_aux bs (bintrunc n w)"
-  by (induct n arbitrary: w bs) (auto simp add : bl_to_bin_def)
+lemma bin_bl_bin': "bl_to_bin (bin_to_bl_aux n w bs) = bl_to_bin_aux bs (bintrunc n w)"
+  by (induct n arbitrary: w bs) (auto simp: bl_to_bin_def)
 
 lemma bin_bl_bin [simp]: "bl_to_bin (bin_to_bl n w) = bintrunc n w"
-  unfolding bin_to_bl_def bin_bl_bin' by auto
+  by (auto simp: bin_to_bl_def bin_bl_bin')
 
-lemma bl_bin_bl':
-  "bin_to_bl (n + length bs) (bl_to_bin_aux bs w) = 
-    bin_to_bl_aux n w bs"
+lemma bl_bin_bl': "bin_to_bl (n + length bs) (bl_to_bin_aux bs w) = bin_to_bl_aux n w bs"
   apply (induct bs arbitrary: w n)
    apply auto
-    apply (simp_all only : add_Suc [symmetric])
-    apply (auto simp add : bin_to_bl_def)
+    apply (simp_all only: add_Suc [symmetric])
+    apply (auto simp add: bin_to_bl_def)
   done
 
 lemma bl_bin_bl [simp]: "bin_to_bl (length bs) (bl_to_bin bs) = bs"
@@ -182,9 +161,8 @@
    apply (rule bin_to_bl_aux.Z)
   apply simp
   done
-  
-lemma bl_to_bin_inj:
-  "bl_to_bin bs = bl_to_bin cs ==> length bs = length cs ==> bs = cs"
+
+lemma bl_to_bin_inj: "bl_to_bin bs = bl_to_bin cs \<Longrightarrow> length bs = length cs \<Longrightarrow> bs = cs"
   apply (rule_tac box_equals)
     defer
     apply (rule bl_bin_bl)
@@ -193,86 +171,74 @@
   done
 
 lemma bl_to_bin_False [simp]: "bl_to_bin (False # bl) = bl_to_bin bl"
-  unfolding bl_to_bin_def by auto
+  by (auto simp: bl_to_bin_def)
 
 lemma bl_to_bin_Nil [simp]: "bl_to_bin [] = 0"
-  unfolding bl_to_bin_def by auto
+  by (auto simp: bl_to_bin_def)
 
-lemma bin_to_bl_zero_aux: 
-  "bin_to_bl_aux n 0 bl = replicate n False @ bl"
+lemma bin_to_bl_zero_aux: "bin_to_bl_aux n 0 bl = replicate n False @ bl"
   by (induct n arbitrary: bl) (auto simp: replicate_app_Cons_same)
 
 lemma bin_to_bl_zero: "bin_to_bl n 0 = replicate n False"
-  unfolding bin_to_bl_def by (simp add: bin_to_bl_zero_aux)
+  by (simp add: bin_to_bl_def bin_to_bl_zero_aux)
 
-lemma bin_to_bl_minus1_aux:
-  "bin_to_bl_aux n (- 1) bl = replicate n True @ bl"
+lemma bin_to_bl_minus1_aux: "bin_to_bl_aux n (- 1) bl = replicate n True @ bl"
   by (induct n arbitrary: bl) (auto simp: replicate_app_Cons_same)
 
 lemma bin_to_bl_minus1: "bin_to_bl n (- 1) = replicate n True"
-  unfolding bin_to_bl_def by (simp add: bin_to_bl_minus1_aux)
+  by (simp add: bin_to_bl_def bin_to_bl_minus1_aux)
 
-lemma bl_to_bin_rep_F: 
-  "bl_to_bin (replicate n False @ bl) = bl_to_bin bl"
-  apply (simp add: bin_to_bl_zero_aux [symmetric] bin_bl_bin')
-  apply (simp add: bl_to_bin_def)
-  done
+lemma bl_to_bin_rep_F: "bl_to_bin (replicate n False @ bl) = bl_to_bin bl"
+  by (simp add: bin_to_bl_zero_aux [symmetric] bin_bl_bin') (simp add: bl_to_bin_def)
 
-lemma bin_to_bl_trunc [simp]:
-  "n <= m ==> bin_to_bl n (bintrunc m w) = bin_to_bl n w"
+lemma bin_to_bl_trunc [simp]: "n \<le> m \<Longrightarrow> bin_to_bl n (bintrunc m w) = bin_to_bl n w"
   by (auto intro: bl_to_bin_inj)
 
 lemma bin_to_bl_aux_bintr:
-  "bin_to_bl_aux n (bintrunc m bin) bl = 
+  "bin_to_bl_aux n (bintrunc m bin) bl =
     replicate (n - m) False @ bin_to_bl_aux (min n m) bin bl"
   apply (induct n arbitrary: m bin bl)
    apply clarsimp
   apply clarsimp
   apply (case_tac "m")
-   apply (clarsimp simp: bin_to_bl_zero_aux) 
+   apply (clarsimp simp: bin_to_bl_zero_aux)
    apply (erule thin_rl)
-   apply (induct_tac n)   
+   apply (induct_tac n)
     apply auto
   done
 
 lemma bin_to_bl_bintr:
-  "bin_to_bl n (bintrunc m bin) =
-    replicate (n - m) False @ bin_to_bl (min n m) bin"
+  "bin_to_bl n (bintrunc m bin) = replicate (n - m) False @ bin_to_bl (min n m) bin"
   unfolding bin_to_bl_def by (rule bin_to_bl_aux_bintr)
 
 lemma bl_to_bin_rep_False: "bl_to_bin (replicate n False) = 0"
   by (induct n) auto
 
-lemma len_bin_to_bl_aux: 
-  "length (bin_to_bl_aux n w bs) = n + length bs"
+lemma len_bin_to_bl_aux: "length (bin_to_bl_aux n w bs) = n + length bs"
   by (fact size_bin_to_bl_aux)
 
-lemma len_bin_to_bl [simp]: "length (bin_to_bl n w) = n"
+lemma len_bin_to_bl: "length (bin_to_bl n w) = n"
   by (fact size_bin_to_bl) (* FIXME: duplicate *)
-  
-lemma sign_bl_bin': 
-  "bin_sign (bl_to_bin_aux bs w) = bin_sign w"
+
+lemma sign_bl_bin': "bin_sign (bl_to_bin_aux bs w) = bin_sign w"
   by (induct bs arbitrary: w) auto
-  
+
 lemma sign_bl_bin: "bin_sign (bl_to_bin bs) = 0"
-  unfolding bl_to_bin_def by (simp add : sign_bl_bin')
-  
-lemma bl_sbin_sign_aux: 
-  "hd (bin_to_bl_aux (Suc n) w bs) = 
-    (bin_sign (sbintrunc n w) = -1)"
+  by (simp add: bl_to_bin_def sign_bl_bin')
+
+lemma bl_sbin_sign_aux: "hd (bin_to_bl_aux (Suc n) w bs) = (bin_sign (sbintrunc n w) = -1)"
   apply (induct n arbitrary: w bs)
    apply clarsimp
    apply (cases w rule: bin_exhaust)
    apply simp
   done
-    
-lemma bl_sbin_sign: 
-  "hd (bin_to_bl (Suc n) w) = (bin_sign (sbintrunc n w) = -1)"
+
+lemma bl_sbin_sign: "hd (bin_to_bl (Suc n) w) = (bin_sign (sbintrunc n w) = -1)"
   unfolding bin_to_bl_def by (rule bl_sbin_sign_aux)
 
 lemma bin_nth_of_bl_aux:
-  "bin_nth (bl_to_bin_aux bl w) n = 
-    (n < size bl & rev bl ! n | n >= length bl & bin_nth w (n - size bl))"
+  "bin_nth (bl_to_bin_aux bl w) n =
+    (n < size bl \<and> rev bl ! n | n \<ge> length bl \<and> bin_nth w (n - size bl))"
   apply (induct bl arbitrary: w)
    apply clarsimp
   apply clarsimp
@@ -281,8 +247,8 @@
   apply auto
   done
 
-lemma bin_nth_of_bl: "bin_nth (bl_to_bin bl) n = (n < length bl & rev bl ! n)"
-  unfolding bl_to_bin_def by (simp add : bin_nth_of_bl_aux)
+lemma bin_nth_of_bl: "bin_nth (bl_to_bin bl) n = (n < length bl \<and> rev bl ! n)"
+  by (simp add: bl_to_bin_def bin_nth_of_bl_aux)
 
 lemma bin_nth_bl: "n < m \<Longrightarrow> bin_nth w n = nth (rev (bin_to_bl m w)) n"
   apply (induct n arbitrary: m w)
@@ -296,11 +262,10 @@
   apply (simp add: bin_to_bl_aux_alt)
   done
 
-lemma nth_rev:
-  "n < length xs \<Longrightarrow> rev xs ! n = xs ! (length xs - 1 - n)"
+lemma nth_rev: "n < length xs \<Longrightarrow> rev xs ! n = xs ! (length xs - 1 - n)"
   apply (induct xs)
    apply simp
-  apply (clarsimp simp add : nth_append nth.simps split: nat.split)
+  apply (clarsimp simp add: nth_append nth.simps split: nat.split)
   apply (rule_tac f = "\<lambda>n. xs ! n" in arg_cong)
   apply arith
   done
@@ -309,7 +274,7 @@
   by (simp add: nth_rev)
 
 lemma nth_bin_to_bl_aux:
-  "n < m + length bl \<Longrightarrow> (bin_to_bl_aux m w bl) ! n = 
+  "n < m + length bl \<Longrightarrow> (bin_to_bl_aux m w bl) ! n =
     (if n < m then bin_nth w (m - 1 - n) else bl ! (n - m))"
   apply (induct m arbitrary: w n bl)
    apply clarsimp
@@ -318,29 +283,29 @@
   apply simp
   done
 
-lemma nth_bin_to_bl: "n < m ==> (bin_to_bl m w) ! n = bin_nth w (m - Suc n)"
-  unfolding bin_to_bl_def by (simp add : nth_bin_to_bl_aux)
+lemma nth_bin_to_bl: "n < m \<Longrightarrow> (bin_to_bl m w) ! n = bin_nth w (m - Suc n)"
+  by (simp add: bin_to_bl_def nth_bin_to_bl_aux)
 
-lemma bl_to_bin_lt2p_aux:
-  "bl_to_bin_aux bs w < (w + 1) * (2 ^ length bs)"
+lemma bl_to_bin_lt2p_aux: "bl_to_bin_aux bs w < (w + 1) * (2 ^ length bs)"
   apply (induct bs arbitrary: w)
    apply clarsimp
   apply clarsimp
   apply (drule meta_spec, erule xtrans(8) [rotated], simp add: Bit_def)+
   done
 
-lemma bl_to_bin_lt2p_drop:
-  "bl_to_bin bs < 2 ^ length (dropWhile Not bs)"
+lemma bl_to_bin_lt2p_drop: "bl_to_bin bs < 2 ^ length (dropWhile Not bs)"
 proof (induct bs)
+  case Nil
+  then show ?case by simp
+next
   case (Cons b bs) with bl_to_bin_lt2p_aux[where w=1]
   show ?case unfolding bl_to_bin_def by simp
-qed simp
+qed
 
 lemma bl_to_bin_lt2p: "bl_to_bin bs < 2 ^ length bs"
   by (metis bin_bl_bin bintr_lt2p bl_bin_bl)
 
-lemma bl_to_bin_ge2p_aux:
-  "bl_to_bin_aux bs w >= w * (2 ^ length bs)"
+lemma bl_to_bin_ge2p_aux: "bl_to_bin_aux bs w \<ge> w * (2 ^ length bs)"
   apply (induct bs arbitrary: w)
    apply clarsimp
   apply clarsimp
@@ -349,15 +314,14 @@
    apply (simp add: Bit_def)
   done
 
-lemma bl_to_bin_ge0: "bl_to_bin bs >= 0"
+lemma bl_to_bin_ge0: "bl_to_bin bs \<ge> 0"
   apply (unfold bl_to_bin_def)
   apply (rule xtrans(4))
    apply (rule bl_to_bin_ge2p_aux)
   apply simp
   done
 
-lemma butlast_rest_bin: 
-  "butlast (bin_to_bl n w) = bin_to_bl (n - 1) (bin_rest w)"
+lemma butlast_rest_bin: "butlast (bin_to_bl n w) = bin_to_bl (n - 1) (bin_rest w)"
   apply (unfold bin_to_bl_def)
   apply (cases w rule: bin_exhaust)
   apply (cases n, clarsimp)
@@ -365,180 +329,154 @@
   apply (auto simp add: bin_to_bl_aux_alt)
   done
 
-lemma butlast_bin_rest:
-  "butlast bl = bin_to_bl (length bl - Suc 0) (bin_rest (bl_to_bin bl))"
+lemma butlast_bin_rest: "butlast bl = bin_to_bl (length bl - Suc 0) (bin_rest (bl_to_bin bl))"
   using butlast_rest_bin [where w="bl_to_bin bl" and n="length bl"] by simp
 
 lemma butlast_rest_bl2bin_aux:
-  "bl ~= [] \<Longrightarrow>
-    bl_to_bin_aux (butlast bl) w = bin_rest (bl_to_bin_aux bl w)"
+  "bl \<noteq> [] \<Longrightarrow> bl_to_bin_aux (butlast bl) w = bin_rest (bl_to_bin_aux bl w)"
   by (induct bl arbitrary: w) auto
-  
-lemma butlast_rest_bl2bin: 
-  "bl_to_bin (butlast bl) = bin_rest (bl_to_bin bl)"
-  apply (unfold bl_to_bin_def)
-  apply (cases bl)
-   apply (auto simp add: butlast_rest_bl2bin_aux)
-  done
+
+lemma butlast_rest_bl2bin: "bl_to_bin (butlast bl) = bin_rest (bl_to_bin bl)"
+  by (cases bl) (auto simp: bl_to_bin_def butlast_rest_bl2bin_aux)
 
 lemma trunc_bl2bin_aux:
-  "bintrunc m (bl_to_bin_aux bl w) = 
+  "bintrunc m (bl_to_bin_aux bl w) =
     bl_to_bin_aux (drop (length bl - m) bl) (bintrunc (m - length bl) w)"
 proof (induct bl arbitrary: w)
-  case Nil show ?case by simp
+  case Nil
+  show ?case by simp
 next
-  case (Cons b bl) show ?case
+  case (Cons b bl)
+  show ?case
   proof (cases "m - length bl")
-    case 0 then have "Suc (length bl) - m = Suc (length bl - m)" by simp
+    case 0
+    then have "Suc (length bl) - m = Suc (length bl - m)" by simp
     with Cons show ?thesis by simp
   next
-    case (Suc n) then have *: "m - Suc (length bl) = n" by simp
-    with Suc Cons show ?thesis by simp
+    case (Suc n)
+    then have "m - Suc (length bl) = n" by simp
+    with Cons Suc show ?thesis by simp
   qed
 qed
 
-lemma trunc_bl2bin: 
-  "bintrunc m (bl_to_bin bl) = bl_to_bin (drop (length bl - m) bl)"
-  unfolding bl_to_bin_def by (simp add : trunc_bl2bin_aux)
-  
-lemma trunc_bl2bin_len [simp]:
-  "bintrunc (length bl) (bl_to_bin bl) = bl_to_bin bl"
+lemma trunc_bl2bin: "bintrunc m (bl_to_bin bl) = bl_to_bin (drop (length bl - m) bl)"
+  by (simp add: bl_to_bin_def trunc_bl2bin_aux)
+
+lemma trunc_bl2bin_len [simp]: "bintrunc (length bl) (bl_to_bin bl) = bl_to_bin bl"
   by (simp add: trunc_bl2bin)
 
-lemma bl2bin_drop: 
-  "bl_to_bin (drop k bl) = bintrunc (length bl - k) (bl_to_bin bl)"
+lemma bl2bin_drop: "bl_to_bin (drop k bl) = bintrunc (length bl - k) (bl_to_bin bl)"
   apply (rule trans)
    prefer 2
    apply (rule trunc_bl2bin [symmetric])
-  apply (cases "k <= length bl")
+  apply (cases "k \<le> length bl")
    apply auto
   done
 
-lemma nth_rest_power_bin:
-  "bin_nth ((bin_rest ^^ k) w) n = bin_nth w (n + k)"
-  apply (induct k arbitrary: n, clarsimp)
+lemma nth_rest_power_bin: "bin_nth ((bin_rest ^^ k) w) n = bin_nth w (n + k)"
+  apply (induct k arbitrary: n)
+   apply clarsimp
   apply clarsimp
   apply (simp only: bin_nth.Suc [symmetric] add_Suc)
   done
 
-lemma take_rest_power_bin:
-  "m <= n ==> take m (bin_to_bl n w) = bin_to_bl m ((bin_rest ^^ (n - m)) w)" 
+lemma take_rest_power_bin: "m \<le> n \<Longrightarrow> take m (bin_to_bl n w) = bin_to_bl m ((bin_rest ^^ (n - m)) w)"
   apply (rule nth_equalityI)
    apply simp
   apply (clarsimp simp add: nth_bin_to_bl nth_rest_power_bin)
   done
 
-lemma hd_butlast: "size xs > 1 ==> hd (butlast xs) = hd xs"
+lemma hd_butlast: "size xs > 1 \<Longrightarrow> hd (butlast xs) = hd xs"
   by (cases xs) auto
 
-lemma last_bin_last': 
-  "size xs > 0 \<Longrightarrow> last xs \<longleftrightarrow> bin_last (bl_to_bin_aux xs w)" 
+lemma last_bin_last': "size xs > 0 \<Longrightarrow> last xs \<longleftrightarrow> bin_last (bl_to_bin_aux xs w)"
   by (induct xs arbitrary: w) auto
 
-lemma last_bin_last: 
-  "size xs > 0 ==> last xs \<longleftrightarrow> bin_last (bl_to_bin xs)" 
+lemma last_bin_last: "size xs > 0 \<Longrightarrow> last xs \<longleftrightarrow> bin_last (bl_to_bin xs)"
   unfolding bl_to_bin_def by (erule last_bin_last')
-  
-lemma bin_last_last: 
-  "bin_last w \<longleftrightarrow> last (bin_to_bl (Suc n) w)" 
-  apply (unfold bin_to_bl_def)
-  apply simp
-  apply (auto simp add: bin_to_bl_aux_alt)
-  done
+
+lemma bin_last_last: "bin_last w \<longleftrightarrow> last (bin_to_bl (Suc n) w)"
+  by (simp add: bin_to_bl_def) (auto simp: bin_to_bl_aux_alt)
+
 
-(** links between bit-wise operations and operations on bool lists **)
-    
+subsection \<open>Links between bit-wise operations and operations on bool lists\<close>
+
 lemma bl_xor_aux_bin:
-  "map2 (%x y. x ~= y) (bin_to_bl_aux n v bs) (bin_to_bl_aux n w cs) = 
-    bin_to_bl_aux n (v XOR w) (map2 (%x y. x ~= y) bs cs)"
+  "map2 (\<lambda>x y. x \<noteq> y) (bin_to_bl_aux n v bs) (bin_to_bl_aux n w cs) =
+    bin_to_bl_aux n (v XOR w) (map2 (\<lambda>x y. x \<noteq> y) bs cs)"
   apply (induct n arbitrary: v w bs cs)
    apply simp
   apply (case_tac v rule: bin_exhaust)
   apply (case_tac w rule: bin_exhaust)
   apply clarsimp
   apply (case_tac b)
-  apply auto
+   apply auto
   done
 
 lemma bl_or_aux_bin:
-  "map2 (op | ) (bin_to_bl_aux n v bs) (bin_to_bl_aux n w cs) = 
-    bin_to_bl_aux n (v OR w) (map2 (op | ) bs cs)"
+  "map2 (op \<or>) (bin_to_bl_aux n v bs) (bin_to_bl_aux n w cs) =
+    bin_to_bl_aux n (v OR w) (map2 (op \<or>) bs cs)"
   apply (induct n arbitrary: v w bs cs)
    apply simp
   apply (case_tac v rule: bin_exhaust)
   apply (case_tac w rule: bin_exhaust)
   apply clarsimp
   done
-    
+
 lemma bl_and_aux_bin:
-  "map2 (op & ) (bin_to_bl_aux n v bs) (bin_to_bl_aux n w cs) = 
-    bin_to_bl_aux n (v AND w) (map2 (op & ) bs cs)" 
+  "map2 (op \<and>) (bin_to_bl_aux n v bs) (bin_to_bl_aux n w cs) =
+    bin_to_bl_aux n (v AND w) (map2 (op \<and>) bs cs)"
   apply (induct n arbitrary: v w bs cs)
    apply simp
   apply (case_tac v rule: bin_exhaust)
   apply (case_tac w rule: bin_exhaust)
   apply clarsimp
   done
-    
-lemma bl_not_aux_bin:
-  "map Not (bin_to_bl_aux n w cs) = 
-    bin_to_bl_aux n (NOT w) (map Not cs)"
-  apply (induct n arbitrary: w cs)
-   apply clarsimp
-  apply clarsimp
-  done
+
+lemma bl_not_aux_bin: "map Not (bin_to_bl_aux n w cs) = bin_to_bl_aux n (NOT w) (map Not cs)"
+  by (induct n arbitrary: w cs) auto
 
 lemma bl_not_bin: "map Not (bin_to_bl n w) = bin_to_bl n (NOT w)"
-  unfolding bin_to_bl_def by (simp add: bl_not_aux_bin)
+  by (simp add: bin_to_bl_def bl_not_aux_bin)
 
-lemma bl_and_bin:
-  "map2 (op \<and>) (bin_to_bl n v) (bin_to_bl n w) = bin_to_bl n (v AND w)"
-  unfolding bin_to_bl_def by (simp add: bl_and_aux_bin)
+lemma bl_and_bin: "map2 (op \<and>) (bin_to_bl n v) (bin_to_bl n w) = bin_to_bl n (v AND w)"
+  by (simp add: bin_to_bl_def bl_and_aux_bin)
 
-lemma bl_or_bin:
-  "map2 (op \<or>) (bin_to_bl n v) (bin_to_bl n w) = bin_to_bl n (v OR w)"
-  unfolding bin_to_bl_def by (simp add: bl_or_aux_bin)
+lemma bl_or_bin: "map2 (op \<or>) (bin_to_bl n v) (bin_to_bl n w) = bin_to_bl n (v OR w)"
+  by (simp add: bin_to_bl_def bl_or_aux_bin)
 
-lemma bl_xor_bin:
-  "map2 (\<lambda>x y. x \<noteq> y) (bin_to_bl n v) (bin_to_bl n w) = bin_to_bl n (v XOR w)"
-  unfolding bin_to_bl_def by (simp only: bl_xor_aux_bin map2_Nil)
+lemma bl_xor_bin: "map2 (\<lambda>x y. x \<noteq> y) (bin_to_bl n v) (bin_to_bl n w) = bin_to_bl n (v XOR w)"
+  by (simp only: bin_to_bl_def bl_xor_aux_bin map2_Nil)
 
 lemma drop_bin2bl_aux:
-  "drop m (bin_to_bl_aux n bin bs) = 
+  "drop m (bin_to_bl_aux n bin bs) =
     bin_to_bl_aux (n - m) bin (drop (m - n) bs)"
   apply (induct n arbitrary: m bin bs, clarsimp)
   apply clarsimp
   apply (case_tac bin rule: bin_exhaust)
-  apply (case_tac "m <= n", simp)
+  apply (case_tac "m \<le> n", simp)
   apply (case_tac "m - n", simp)
   apply simp
-  apply (rule_tac f = "%nat. drop nat bs" in arg_cong) 
+  apply (rule_tac f = "\<lambda>nat. drop nat bs" in arg_cong)
   apply simp
   done
 
 lemma drop_bin2bl: "drop m (bin_to_bl n bin) = bin_to_bl (n - m) bin"
-  unfolding bin_to_bl_def by (simp add : drop_bin2bl_aux)
+  by (simp add: bin_to_bl_def drop_bin2bl_aux)
 
-lemma take_bin2bl_lem1:
-  "take m (bin_to_bl_aux m w bs) = bin_to_bl m w"
-  apply (induct m arbitrary: w bs, clarsimp)
+lemma take_bin2bl_lem1: "take m (bin_to_bl_aux m w bs) = bin_to_bl m w"
+  apply (induct m arbitrary: w bs)
+   apply clarsimp
   apply clarsimp
   apply (simp add: bin_to_bl_aux_alt)
   apply (simp add: bin_to_bl_def)
   apply (simp add: bin_to_bl_aux_alt)
   done
 
-lemma take_bin2bl_lem:
-  "take m (bin_to_bl_aux (m + n) w bs) = 
-    take m (bin_to_bl (m + n) w)"
-  apply (induct n arbitrary: w bs)
-   apply (simp_all (no_asm) add: bin_to_bl_def take_bin2bl_lem1)
-  apply simp
-  done
+lemma take_bin2bl_lem: "take m (bin_to_bl_aux (m + n) w bs) = take m (bin_to_bl (m + n) w)"
+  by (induct n arbitrary: w bs) (simp_all (no_asm) add: bin_to_bl_def take_bin2bl_lem1, simp)
 
-lemma bin_split_take:
-  "bin_split n c = (a, b) \<Longrightarrow>
-    bin_to_bl m a = take m (bin_to_bl (m + n) c)"
+lemma bin_split_take: "bin_split n c = (a, b) \<Longrightarrow> bin_to_bl m a = take m (bin_to_bl (m + n) c)"
   apply (induct n arbitrary: b c)
    apply clarsimp
   apply (clarsimp simp: Let_def split: prod.split_asm)
@@ -546,71 +484,59 @@
   apply (simp add: take_bin2bl_lem)
   done
 
-lemma bin_split_take1: 
-  "k = m + n ==> bin_split n c = (a, b) ==> 
-    bin_to_bl m a = take m (bin_to_bl k c)"
+lemma bin_split_take1:
+  "k = m + n \<Longrightarrow> bin_split n c = (a, b) \<Longrightarrow> bin_to_bl m a = take m (bin_to_bl k c)"
   by (auto elim: bin_split_take)
-  
-lemma nth_takefill: "m < n \<Longrightarrow>
-    takefill fill n l ! m = (if m < length l then l ! m else fill)"
-  apply (induct n arbitrary: m l, clarsimp)
+
+lemma nth_takefill: "m < n \<Longrightarrow> takefill fill n l ! m = (if m < length l then l ! m else fill)"
+  apply (induct n arbitrary: m l)
+   apply clarsimp
   apply clarsimp
   apply (case_tac m)
    apply (simp split: list.split)
   apply (simp split: list.split)
   done
 
-lemma takefill_alt:
-  "takefill fill n l = take n l @ replicate (n - length l) fill"
+lemma takefill_alt: "takefill fill n l = take n l @ replicate (n - length l) fill"
   by (induct n arbitrary: l) (auto split: list.split)
 
-lemma takefill_replicate [simp]:
-  "takefill fill n (replicate m fill) = replicate n fill"
-  by (simp add : takefill_alt replicate_add [symmetric])
+lemma takefill_replicate [simp]: "takefill fill n (replicate m fill) = replicate n fill"
+  by (simp add: takefill_alt replicate_add [symmetric])
 
-lemma takefill_le':
-  "n = m + k \<Longrightarrow> takefill x m (takefill x n l) = takefill x m l"
+lemma takefill_le': "n = m + k \<Longrightarrow> takefill x m (takefill x n l) = takefill x m l"
   by (induct m arbitrary: l n) (auto split: list.split)
 
 lemma length_takefill [simp]: "length (takefill fill n l) = n"
-  by (simp add : takefill_alt)
+  by (simp add: takefill_alt)
 
-lemma take_takefill':
-  "!!w n.  n = k + m ==> take k (takefill fill n w) = takefill fill k w"
-  by (induct k) (auto split: list.split) 
+lemma take_takefill': "\<And>w n.  n = k + m \<Longrightarrow> take k (takefill fill n w) = takefill fill k w"
+  by (induct k) (auto split: list.split)
 
-lemma drop_takefill:
-  "!!w. drop k (takefill fill (m + k) w) = takefill fill m (drop k w)"
-  by (induct k) (auto split: list.split) 
+lemma drop_takefill: "\<And>w. drop k (takefill fill (m + k) w) = takefill fill m (drop k w)"
+  by (induct k) (auto split: list.split)
 
-lemma takefill_le [simp]:
-  "m \<le> n \<Longrightarrow> takefill x m (takefill x n l) = takefill x m l"
+lemma takefill_le [simp]: "m \<le> n \<Longrightarrow> takefill x m (takefill x n l) = takefill x m l"
   by (auto simp: le_iff_add takefill_le')
 
-lemma take_takefill [simp]:
-  "m \<le> n \<Longrightarrow> take m (takefill fill n w) = takefill fill m w"
+lemma take_takefill [simp]: "m \<le> n \<Longrightarrow> take m (takefill fill n w) = takefill fill m w"
   by (auto simp: le_iff_add take_takefill')
- 
-lemma takefill_append:
-  "takefill fill (m + length xs) (xs @ w) = xs @ (takefill fill m w)"
+
+lemma takefill_append: "takefill fill (m + length xs) (xs @ w) = xs @ (takefill fill m w)"
   by (induct xs) auto
 
-lemma takefill_same': 
-  "l = length xs ==> takefill fill l xs = xs"
-  by (induct xs arbitrary: l, auto)
- 
+lemma takefill_same': "l = length xs \<Longrightarrow> takefill fill l xs = xs"
+  by (induct xs arbitrary: l) auto
+
 lemmas takefill_same [simp] = takefill_same' [OF refl]
 
-lemma takefill_bintrunc:
-  "takefill False n bl = rev (bin_to_bl n (bl_to_bin (rev bl)))"
+lemma takefill_bintrunc: "takefill False n bl = rev (bin_to_bl n (bl_to_bin (rev bl)))"
   apply (rule nth_equalityI)
    apply simp
   apply (clarsimp simp: nth_takefill nth_rev nth_bin_to_bl bin_nth_of_bl)
   done
 
-lemma bl_bin_bl_rtf:
-  "bin_to_bl n (bl_to_bin bl) = rev (takefill False n (rev bl))"
-  by (simp add : takefill_bintrunc)
+lemma bl_bin_bl_rtf: "bin_to_bl n (bl_to_bin bl) = rev (takefill False n (rev bl))"
+  by (simp add: takefill_bintrunc)
 
 lemma bl_bin_bl_rep_drop:
   "bin_to_bl n (bl_to_bin bl) =
@@ -618,25 +544,24 @@
   by (simp add: bl_bin_bl_rtf takefill_alt rev_take)
 
 lemma tf_rev:
-  "n + k = m + length bl ==> takefill x m (rev (takefill y n bl)) = 
+  "n + k = m + length bl \<Longrightarrow> takefill x m (rev (takefill y n bl)) =
     rev (takefill y m (rev (takefill x k (rev bl))))"
   apply (rule nth_equalityI)
    apply (auto simp add: nth_takefill nth_rev)
-  apply (rule_tac f = "%n. bl ! n" in arg_cong) 
-  apply arith 
+  apply (rule_tac f = "\<lambda>n. bl ! n" in arg_cong)
+  apply arith
   done
 
-lemma takefill_minus:
-  "0 < n ==> takefill fill (Suc (n - 1)) w = takefill fill n w"
+lemma takefill_minus: "0 < n \<Longrightarrow> takefill fill (Suc (n - 1)) w = takefill fill n w"
   by auto
 
-lemmas takefill_Suc_cases = 
+lemmas takefill_Suc_cases =
   list.cases [THEN takefill.Suc [THEN trans]]
 
 lemmas takefill_Suc_Nil = takefill_Suc_cases (1)
 lemmas takefill_Suc_Cons = takefill_Suc_cases (2)
 
-lemmas takefill_minus_simps = takefill_Suc_cases [THEN [2] 
+lemmas takefill_minus_simps = takefill_Suc_cases [THEN [2]
   takefill_minus [symmetric, THEN trans]]
 
 lemma takefill_numeral_Nil [simp]:
@@ -647,32 +572,29 @@
   "takefill fill (numeral k) (x # xs) = x # takefill fill (pred_numeral k) xs"
   by (simp add: numeral_eq_Suc)
 
-(* links with function bl_to_bin *)
+
+subsection \<open>Links with function \<open>bl_to_bin\<close>\<close>
 
-lemma bl_to_bin_aux_cat: 
-  "!!nv v. bl_to_bin_aux bs (bin_cat w nv v) = 
+lemma bl_to_bin_aux_cat:
+  "\<And>nv v. bl_to_bin_aux bs (bin_cat w nv v) =
     bin_cat w (nv + length bs) (bl_to_bin_aux bs v)"
-  apply (induct bs)
-   apply simp
-  apply (simp add: bin_cat_Suc_Bit [symmetric] del: bin_cat.simps)
-  done
+  by (induct bs) (simp, simp add: bin_cat_Suc_Bit [symmetric] del: bin_cat.simps)
 
-lemma bin_to_bl_aux_cat: 
-  "!!w bs. bin_to_bl_aux (nv + nw) (bin_cat v nw w) bs = 
+lemma bin_to_bl_aux_cat:
+  "\<And>w bs. bin_to_bl_aux (nv + nw) (bin_cat v nw w) bs =
     bin_to_bl_aux nv v (bin_to_bl_aux nw w bs)"
-  by (induct nw) auto 
+  by (induct nw) auto
 
-lemma bl_to_bin_aux_alt:
-  "bl_to_bin_aux bs w = bin_cat w (length bs) (bl_to_bin bs)"
+lemma bl_to_bin_aux_alt: "bl_to_bin_aux bs w = bin_cat w (length bs) (bl_to_bin bs)"
   using bl_to_bin_aux_cat [where nv = "0" and v = "0"]
-  unfolding bl_to_bin_def [symmetric] by simp
+  by (simp add: bl_to_bin_def [symmetric])
 
 lemma bin_to_bl_cat:
   "bin_to_bl (nv + nw) (bin_cat v nw w) =
     bin_to_bl_aux nv v (bin_to_bl nw w)"
-  unfolding bin_to_bl_def by (simp add: bin_to_bl_aux_cat)
+  by (simp add: bin_to_bl_def bin_to_bl_aux_cat)
 
-lemmas bl_to_bin_aux_app_cat = 
+lemmas bl_to_bin_aux_app_cat =
   trans [OF bl_to_bin_aux_append bl_to_bin_aux_alt]
 
 lemmas bin_to_bl_aux_cat_app =
@@ -686,49 +608,46 @@
   "bin_to_bl (n + nw) (bin_cat w nw wa) = bin_to_bl n w @ bin_to_bl nw wa"
   by (simp only: bin_to_bl_def bin_to_bl_aux_cat_app)
 
-(* bl_to_bin_app_cat_alt and bl_to_bin_app_cat are easily interderivable *)
-lemma bl_to_bin_app_cat_alt: 
-  "bin_cat (bl_to_bin cs) n w = bl_to_bin (cs @ bin_to_bl n w)"
-  by (simp add : bl_to_bin_app_cat)
+text \<open>\<open>bl_to_bin_app_cat_alt\<close> and \<open>bl_to_bin_app_cat\<close> are easily interderivable.\<close>
+lemma bl_to_bin_app_cat_alt: "bin_cat (bl_to_bin cs) n w = bl_to_bin (cs @ bin_to_bl n w)"
+  by (simp add: bl_to_bin_app_cat)
 
-lemma mask_lem: "(bl_to_bin (True # replicate n False)) = 
-    (bl_to_bin (replicate n True)) + 1"
+lemma mask_lem: "(bl_to_bin (True # replicate n False)) = bl_to_bin (replicate n True) + 1"
   apply (unfold bl_to_bin_def)
   apply (induct n)
    apply simp
-  apply (simp only: Suc_eq_plus1 replicate_add
-                    append_Cons [symmetric] bl_to_bin_aux_append)
+  apply (simp only: Suc_eq_plus1 replicate_add append_Cons [symmetric] bl_to_bin_aux_append)
   apply (simp add: Bit_B0_2t Bit_B1_2t)
   done
 
-(* function bl_of_nth *)
+
+subsection \<open>Function \<open>bl_of_nth\<close>\<close>
+
 lemma length_bl_of_nth [simp]: "length (bl_of_nth n f) = n"
   by (induct n)  auto
 
-lemma nth_bl_of_nth [simp]:
-  "m < n \<Longrightarrow> rev (bl_of_nth n f) ! m = f m"
+lemma nth_bl_of_nth [simp]: "m < n \<Longrightarrow> rev (bl_of_nth n f) ! m = f m"
   apply (induct n)
    apply simp
-  apply (clarsimp simp add : nth_append)
-  apply (rule_tac f = "f" in arg_cong) 
+  apply (clarsimp simp add: nth_append)
+  apply (rule_tac f = "f" in arg_cong)
   apply simp
   done
 
-lemma bl_of_nth_inj: 
-  "(!!k. k < n ==> f k = g k) ==> bl_of_nth n f = bl_of_nth n g"
+lemma bl_of_nth_inj: "(\<And>k. k < n \<Longrightarrow> f k = g k) \<Longrightarrow> bl_of_nth n f = bl_of_nth n g"
   by (induct n)  auto
 
-lemma bl_of_nth_nth_le:
-  "n \<le> length xs \<Longrightarrow> bl_of_nth n (nth (rev xs)) = drop (length xs - n) xs"
-  apply (induct n arbitrary: xs, clarsimp)
+lemma bl_of_nth_nth_le: "n \<le> length xs \<Longrightarrow> bl_of_nth n (nth (rev xs)) = drop (length xs - n) xs"
+  apply (induct n arbitrary: xs)
+   apply clarsimp
   apply clarsimp
   apply (rule trans [OF _ hd_Cons_tl])
    apply (frule Suc_le_lessD)
    apply (simp add: nth_rev trans [OF drop_Suc drop_tl, symmetric])
    apply (subst hd_drop_conv_nth)
-     apply force
-    apply simp_all
-  apply (rule_tac f = "%n. drop n xs" in arg_cong) 
+    apply force
+   apply simp_all
+  apply (rule_tac f = "\<lambda>n. drop n xs" in arg_cong)
   apply simp
   done
 
@@ -741,45 +660,44 @@
 lemma size_rbl_succ: "length (rbl_succ bl) = length bl"
   by (induct bl) auto
 
-lemma size_rbl_add:
-  "!!cl. length (rbl_add bl cl) = length bl"
-  by (induct bl) (auto simp: Let_def size_rbl_succ)
+lemma size_rbl_add: "length (rbl_add bl cl) = length bl"
+  by (induct bl arbitrary: cl) (auto simp: Let_def size_rbl_succ)
 
-lemma size_rbl_mult: 
-  "!!cl. length (rbl_mult bl cl) = length bl"
-  by (induct bl) (auto simp add : Let_def size_rbl_add)
+lemma size_rbl_mult: "length (rbl_mult bl cl) = length bl"
+  by (induct bl arbitrary: cl) (auto simp add: Let_def size_rbl_add)
 
-lemmas rbl_sizes [simp] = 
+lemmas rbl_sizes [simp] =
   size_rbl_pred size_rbl_succ size_rbl_add size_rbl_mult
 
 lemmas rbl_Nils =
   rbl_pred.Nil rbl_succ.Nil rbl_add.Nil rbl_mult.Nil
 
-lemma rbl_pred:
-  "rbl_pred (rev (bin_to_bl n bin)) = rev (bin_to_bl n (bin - 1))"
-  apply (induct n arbitrary: bin, simp)
+lemma rbl_pred: "rbl_pred (rev (bin_to_bl n bin)) = rev (bin_to_bl n (bin - 1))"
   apply (unfold bin_to_bl_def)
+  apply (induct n arbitrary: bin)
+   apply simp
   apply clarsimp
   apply (case_tac bin rule: bin_exhaust)
   apply (case_tac b)
    apply (clarsimp simp: bin_to_bl_aux_alt)+
   done
 
-lemma rbl_succ: 
-  "rbl_succ (rev (bin_to_bl n bin)) = rev (bin_to_bl n (bin + 1))"
-  apply (induct n arbitrary: bin, simp)
+lemma rbl_succ: "rbl_succ (rev (bin_to_bl n bin)) = rev (bin_to_bl n (bin + 1))"
   apply (unfold bin_to_bl_def)
+  apply (induct n arbitrary: bin)
+   apply simp
   apply clarsimp
   apply (case_tac bin rule: bin_exhaust)
   apply (case_tac b)
    apply (clarsimp simp: bin_to_bl_aux_alt)+
   done
 
-lemma rbl_add: 
-  "!!bina binb. rbl_add (rev (bin_to_bl n bina)) (rev (bin_to_bl n binb)) = 
+lemma rbl_add:
+  "\<And>bina binb. rbl_add (rev (bin_to_bl n bina)) (rev (bin_to_bl n binb)) =
     rev (bin_to_bl n (bina + binb))"
-  apply (induct n, simp)
   apply (unfold bin_to_bl_def)
+  apply (induct n)
+   apply simp
   apply clarsimp
   apply (case_tac bina rule: bin_exhaust)
   apply (case_tac binb rule: bin_exhaust)
@@ -788,82 +706,77 @@
      apply (auto simp: rbl_succ bin_to_bl_aux_alt Let_def ac_simps)
   done
 
-lemma rbl_add_app2: 
-  "!!blb. length blb >= length bla ==> 
-    rbl_add bla (blb @ blc) = rbl_add bla blb"
-  apply (induct bla, simp)
+lemma rbl_add_app2: "length blb \<ge> length bla \<Longrightarrow> rbl_add bla (blb @ blc) = rbl_add bla blb"
+  apply (induct bla arbitrary: blb)
+   apply simp
   apply clarsimp
   apply (case_tac blb, clarsimp)
   apply (clarsimp simp: Let_def)
   done
 
-lemma rbl_add_take2: 
-  "!!blb. length blb >= length bla ==> 
-    rbl_add bla (take (length bla) blb) = rbl_add bla blb"
-  apply (induct bla, simp)
+lemma rbl_add_take2:
+  "length blb >= length bla ==> rbl_add bla (take (length bla) blb) = rbl_add bla blb"
+  apply (induct bla arbitrary: blb)
+   apply simp
   apply clarsimp
   apply (case_tac blb, clarsimp)
   apply (clarsimp simp: Let_def)
   done
 
-lemma rbl_add_long: 
-  "m >= n ==> rbl_add (rev (bin_to_bl n bina)) (rev (bin_to_bl m binb)) = 
+lemma rbl_add_long:
+  "m \<ge> n \<Longrightarrow> rbl_add (rev (bin_to_bl n bina)) (rev (bin_to_bl m binb)) =
     rev (bin_to_bl n (bina + binb))"
   apply (rule box_equals [OF _ rbl_add_take2 rbl_add])
-   apply (rule_tac f = "rbl_add (rev (bin_to_bl n bina))" in arg_cong) 
+   apply (rule_tac f = "rbl_add (rev (bin_to_bl n bina))" in arg_cong)
    apply (rule rev_swap [THEN iffD1])
    apply (simp add: rev_take drop_bin2bl)
   apply simp
   done
 
-lemma rbl_mult_app2:
-  "!!blb. length blb >= length bla ==> 
-    rbl_mult bla (blb @ blc) = rbl_mult bla blb"
-  apply (induct bla, simp)
+lemma rbl_mult_app2: "length blb \<ge> length bla \<Longrightarrow> rbl_mult bla (blb @ blc) = rbl_mult bla blb"
+  apply (induct bla arbitrary: blb)
+   apply simp
   apply clarsimp
   apply (case_tac blb, clarsimp)
   apply (clarsimp simp: Let_def rbl_add_app2)
   done
 
-lemma rbl_mult_take2: 
-  "length blb >= length bla ==> 
-    rbl_mult bla (take (length bla) blb) = rbl_mult bla blb"
+lemma rbl_mult_take2:
+  "length blb \<ge> length bla \<Longrightarrow> rbl_mult bla (take (length bla) blb) = rbl_mult bla blb"
   apply (rule trans)
    apply (rule rbl_mult_app2 [symmetric])
    apply simp
-  apply (rule_tac f = "rbl_mult bla" in arg_cong) 
+  apply (rule_tac f = "rbl_mult bla" in arg_cong)
   apply (rule append_take_drop_id)
   done
-    
-lemma rbl_mult_gt1: 
-  "m >= length bl ==> rbl_mult bl (rev (bin_to_bl m binb)) = 
+
+lemma rbl_mult_gt1:
+  "m \<ge> length bl \<Longrightarrow>
+    rbl_mult bl (rev (bin_to_bl m binb)) =
     rbl_mult bl (rev (bin_to_bl (length bl) binb))"
   apply (rule trans)
    apply (rule rbl_mult_take2 [symmetric])
    apply simp_all
-  apply (rule_tac f = "rbl_mult bl" in arg_cong) 
+  apply (rule_tac f = "rbl_mult bl" in arg_cong)
   apply (rule rev_swap [THEN iffD1])
   apply (simp add: rev_take drop_bin2bl)
   done
-    
-lemma rbl_mult_gt: 
-  "m > n ==> rbl_mult (rev (bin_to_bl n bina)) (rev (bin_to_bl m binb)) = 
+
+lemma rbl_mult_gt:
+  "m > n \<Longrightarrow>
+    rbl_mult (rev (bin_to_bl n bina)) (rev (bin_to_bl m binb)) =
     rbl_mult (rev (bin_to_bl n bina)) (rev (bin_to_bl n binb))"
   by (auto intro: trans [OF rbl_mult_gt1])
-  
+
 lemmas rbl_mult_Suc = lessI [THEN rbl_mult_gt]
 
-lemma rbbl_Cons: 
-  "b # rev (bin_to_bl n x) = rev (bin_to_bl (Suc n) (x BIT b))"
-  apply (unfold bin_to_bl_def)
-  apply simp
-  apply (simp add: bin_to_bl_aux_alt)
-  done
+lemma rbbl_Cons: "b # rev (bin_to_bl n x) = rev (bin_to_bl (Suc n) (x BIT b))"
+  by (simp add: bin_to_bl_def) (simp add: bin_to_bl_aux_alt)
 
-lemma rbl_mult: "!!bina binb. 
-    rbl_mult (rev (bin_to_bl n bina)) (rev (bin_to_bl n binb)) = 
+lemma rbl_mult:
+  "rbl_mult (rev (bin_to_bl n bina)) (rev (bin_to_bl n binb)) =
     rev (bin_to_bl n (bina * binb))"
-  apply (induct n)
+  apply (induct n arbitrary: bina binb)
    apply simp
   apply (unfold bin_to_bl_def)
   apply clarsimp
@@ -875,32 +788,28 @@
      apply (auto simp: rbbl_Cons rbl_mult_Suc rbl_add)
   done
 
-lemma rbl_add_split: 
-  "P (rbl_add (y # ys) (x # xs)) = 
-    (ALL ws. length ws = length ys --> ws = rbl_add ys xs --> 
-    (y --> ((x --> P (False # rbl_succ ws)) & (~ x -->  P (True # ws)))) &
-    (~ y --> P (x # ws)))"
-  apply (auto simp add: Let_def)
-   apply (case_tac [!] "y")
-     apply auto
-  done
+lemma rbl_add_split:
+  "P (rbl_add (y # ys) (x # xs)) =
+    (\<forall>ws. length ws = length ys \<longrightarrow> ws = rbl_add ys xs \<longrightarrow>
+      (y \<longrightarrow> ((x \<longrightarrow> P (False # rbl_succ ws)) \<and> (\<not> x \<longrightarrow> P (True # ws)))) \<and>
+      (\<not> y \<longrightarrow> P (x # ws)))"
+  by (cases y) (auto simp: Let_def)
 
-lemma rbl_mult_split: 
-  "P (rbl_mult (y # ys) xs) = 
-    (ALL ws. length ws = Suc (length ys) --> ws = False # rbl_mult ys xs --> 
-    (y --> P (rbl_add ws xs)) & (~ y -->  P ws))"
-  by (clarsimp simp add : Let_def)
-  
+lemma rbl_mult_split:
+  "P (rbl_mult (y # ys) xs) =
+    (\<forall>ws. length ws = Suc (length ys) \<longrightarrow> ws = False # rbl_mult ys xs \<longrightarrow>
+      (y \<longrightarrow> P (rbl_add ws xs)) \<and> (\<not> y \<longrightarrow> P ws))"
+  by (auto simp: Let_def)
 
-subsection "Repeated splitting or concatenation"
 
-lemma sclem:
-  "size (concat (map (bin_to_bl n) xs)) = length xs * n"
+subsection \<open>Repeated splitting or concatenation\<close>
+
+lemma sclem: "size (concat (map (bin_to_bl n) xs)) = length xs * n"
   by (induct xs) auto
 
 lemma bin_cat_foldl_lem:
-  "foldl (%u. bin_cat u n) x xs = 
-    bin_cat x (size xs * n) (foldl (%u. bin_cat u n) y xs)"
+  "foldl (\<lambda>u. bin_cat u n) x xs =
+    bin_cat x (size xs * n) (foldl (\<lambda>u. bin_cat u n) y xs)"
   apply (induct xs arbitrary: x)
    apply simp
   apply (simp (no_asm))
@@ -908,17 +817,16 @@
   apply (drule meta_spec)
   apply (erule trans)
   apply (drule_tac x = "bin_cat y n a" in meta_spec)
-  apply (simp add : bin_cat_assoc_sym min.absorb2)
+  apply (simp add: bin_cat_assoc_sym min.absorb2)
   done
 
-lemma bin_rcat_bl:
-  "(bin_rcat n wl) = bl_to_bin (concat (map (bin_to_bl n) wl))"
+lemma bin_rcat_bl: "bin_rcat n wl = bl_to_bin (concat (map (bin_to_bl n) wl))"
   apply (unfold bin_rcat_def)
   apply (rule sym)
   apply (induct wl)
-   apply (auto simp add : bl_to_bin_append)
-  apply (simp add : bl_to_bin_aux_alt sclem)
-  apply (simp add : bin_cat_foldl_lem [symmetric])
+   apply (auto simp add: bl_to_bin_append)
+  apply (simp add: bl_to_bin_aux_alt sclem)
+  apply (simp add: bin_cat_foldl_lem [symmetric])
   done
 
 lemmas bin_rsplit_aux_simps = bin_rsplit_aux.simps bin_rsplitl_aux.simps
@@ -934,19 +842,17 @@
 lemmas bin_rsplit_aux_simp2s [simp] = rsplit_aux_simp2ls [unfolded Let_def]
 lemmas rbscl = bin_rsplit_aux_simp2s (2)
 
-lemmas rsplit_aux_0_simps [simp] = 
+lemmas rsplit_aux_0_simps [simp] =
   rsplit_aux_simp1s [OF disjI1] rsplit_aux_simp1s [OF disjI2]
 
-lemma bin_rsplit_aux_append:
-  "bin_rsplit_aux n m c (bs @ cs) = bin_rsplit_aux n m c bs @ cs"
+lemma bin_rsplit_aux_append: "bin_rsplit_aux n m c (bs @ cs) = bin_rsplit_aux n m c bs @ cs"
   apply (induct n m c bs rule: bin_rsplit_aux.induct)
   apply (subst bin_rsplit_aux.simps)
   apply (subst bin_rsplit_aux.simps)
   apply (clarsimp split: prod.split)
   done
 
-lemma bin_rsplitl_aux_append:
-  "bin_rsplitl_aux n m c (bs @ cs) = bin_rsplitl_aux n m c bs @ cs"
+lemma bin_rsplitl_aux_append: "bin_rsplitl_aux n m c (bs @ cs) = bin_rsplitl_aux n m c bs @ cs"
   apply (induct n m c bs rule: bin_rsplitl_aux.induct)
   apply (subst bin_rsplitl_aux.simps)
   apply (subst bin_rsplitl_aux.simps)
@@ -958,41 +864,38 @@
 
 lemmas rsplit_def_auxs = bin_rsplit_def bin_rsplitl_def
 
-lemmas rsplit_aux_alts = rsplit_aux_apps 
+lemmas rsplit_aux_alts = rsplit_aux_apps
   [unfolded append_Nil rsplit_def_auxs [symmetric]]
 
-lemma bin_split_minus: "0 < n ==> bin_split (Suc (n - 1)) w = bin_split n w"
+lemma bin_split_minus: "0 < n \<Longrightarrow> bin_split (Suc (n - 1)) w = bin_split n w"
   by auto
 
 lemmas bin_split_minus_simp =
   bin_split.Suc [THEN [2] bin_split_minus [symmetric, THEN trans]]
 
-lemma bin_split_pred_simp [simp]: 
+lemma bin_split_pred_simp [simp]:
   "(0::nat) < numeral bin \<Longrightarrow>
-  bin_split (numeral bin) w =
-  (let (w1, w2) = bin_split (numeral bin - 1) (bin_rest w)
-   in (w1, w2 BIT bin_last w))" 
+    bin_split (numeral bin) w =
+      (let (w1, w2) = bin_split (numeral bin - 1) (bin_rest w)
+       in (w1, w2 BIT bin_last w))"
   by (simp only: bin_split_minus_simp)
 
 lemma bin_rsplit_aux_simp_alt:
   "bin_rsplit_aux n m c bs =
-   (if m = 0 \<or> n = 0 
-   then bs
-   else let (a, b) = bin_split n c in bin_rsplit n (m - n, a) @ b # bs)"
-  unfolding bin_rsplit_aux.simps [of n m c bs]
-  apply simp
+    (if m = 0 \<or> n = 0 then bs
+     else let (a, b) = bin_split n c in bin_rsplit n (m - n, a) @ b # bs)"
+  apply (simp add: bin_rsplit_aux.simps [of n m c bs])
   apply (subst rsplit_aux_alts)
   apply (simp add: bin_rsplit_def)
   done
 
-lemmas bin_rsplit_simp_alt = 
+lemmas bin_rsplit_simp_alt =
   trans [OF bin_rsplit_def bin_rsplit_aux_simp_alt]
 
 lemmas bthrs = bin_rsplit_simp_alt [THEN [2] trans]
 
-lemma bin_rsplit_size_sign' [rule_format] : 
-  "\<lbrakk>n > 0; rev sw = bin_rsplit n (nw, w)\<rbrakk> \<Longrightarrow> 
-    (ALL v: set sw. bintrunc n v = v)"
+lemma bin_rsplit_size_sign' [rule_format]:
+  "n > 0 \<Longrightarrow> rev sw = bin_rsplit n (nw, w) \<Longrightarrow> \<forall>v\<in>set sw. bintrunc n v = v"
   apply (induct sw arbitrary: nw w)
    apply clarsimp
   apply clarsimp
@@ -1003,12 +906,14 @@
   apply simp
   done
 
-lemmas bin_rsplit_size_sign = bin_rsplit_size_sign' [OF asm_rl 
+lemmas bin_rsplit_size_sign = bin_rsplit_size_sign' [OF asm_rl
   rev_rev_ident [THEN trans] set_rev [THEN equalityD2 [THEN subsetD]]]
 
 lemma bin_nth_rsplit [rule_format] :
-  "n > 0 ==> m < n ==> (ALL w k nw. rev sw = bin_rsplit n (nw, w) --> 
-       k < size sw --> bin_nth (sw ! k) m = bin_nth w (k * n + m))"
+  "n > 0 \<Longrightarrow> m < n \<Longrightarrow>
+    \<forall>w k nw.
+      rev sw = bin_rsplit n (nw, w) \<longrightarrow>
+      k < size sw \<longrightarrow> bin_nth (sw ! k) m = bin_nth w (k * n + m)"
   apply (induct sw)
    apply clarsimp
   apply clarsimp
@@ -1017,24 +922,21 @@
   apply clarify
   apply (erule allE, erule impE, erule exI)
   apply (case_tac k)
-   apply clarsimp   
+   apply clarsimp
    prefer 2
    apply clarsimp
    apply (erule allE)
    apply (erule (1) impE)
-   apply (drule bin_nth_split, erule conjE, erule allE,
-          erule trans, simp add : ac_simps)+
+   apply (drule bin_nth_split, erule conjE, erule allE, erule trans, simp add: ac_simps)+
   done
 
-lemma bin_rsplit_all:
-  "0 < nw ==> nw <= n ==> bin_rsplit n (nw, w) = [bintrunc n w]"
-  unfolding bin_rsplit_def
-  by (clarsimp dest!: split_bintrunc simp: rsplit_aux_simp2ls split: prod.split)
+lemma bin_rsplit_all: "0 < nw \<Longrightarrow> nw \<le> n \<Longrightarrow> bin_rsplit n (nw, w) = [bintrunc n w]"
+  by (auto simp: bin_rsplit_def rsplit_aux_simp2ls split: prod.split dest!: split_bintrunc)
 
-lemma bin_rsplit_l [rule_format] :
-  "ALL bin. bin_rsplitl n (m, bin) = bin_rsplit n (m, bintrunc m bin)"
+lemma bin_rsplit_l [rule_format]:
+  "\<forall>bin. bin_rsplitl n (m, bin) = bin_rsplit n (m, bintrunc m bin)"
   apply (rule_tac a = "m" in wf_less_than [THEN wf_induct])
-  apply (simp (no_asm) add : bin_rsplitl_def bin_rsplit_def)
+  apply (simp (no_asm) add: bin_rsplitl_def bin_rsplit_def)
   apply (rule allI)
   apply (subst bin_rsplitl_aux.simps)
   apply (subst bin_rsplit_aux.simps)
@@ -1048,10 +950,10 @@
   apply simp
   done
 
-lemma bin_rsplit_rcat [rule_format] :
-  "n > 0 --> bin_rsplit n (n * size ws, bin_rcat n ws) = map (bintrunc n) ws"
+lemma bin_rsplit_rcat [rule_format]:
+  "n > 0 \<longrightarrow> bin_rsplit n (n * size ws, bin_rcat n ws) = map (bintrunc n) ws"
   apply (unfold bin_rsplit_def bin_rcat_def)
-  apply (rule_tac xs = "ws" in rev_induct)
+  apply (rule_tac xs = ws in rev_induct)
    apply clarsimp
   apply clarsimp
   apply (subst rsplit_aux_alts)
@@ -1063,78 +965,75 @@
   "\<forall>ws m. n \<noteq> 0 \<longrightarrow> ws = bin_rsplit_aux n nw w bs \<longrightarrow>
     length ws \<le> m \<longleftrightarrow> nw + length bs * n \<le> m * n"
 proof -
-  { fix i j j' k k' m :: nat and R
-    assume d: "(i::nat) \<le> j \<or> m < j'"
-    assume R1: "i * k \<le> j * k \<Longrightarrow> R"
-    assume R2: "Suc m * k' \<le> j' * k' \<Longrightarrow> R"
-    have "R" using d
-      apply safe
-       apply (rule R1, erule mult_le_mono1)
-      apply (rule R2, erule Suc_le_eq [THEN iffD2 [THEN mult_le_mono1]])
-      done
-  } note A = this
-  { fix sc m n lb :: nat
-    have "(0::nat) < sc \<Longrightarrow> sc - n + (n + lb * n) \<le> m * n \<longleftrightarrow> sc + lb * n \<le> m * n"
-      apply safe
-       apply arith
-      apply (case_tac "sc >= n")
-       apply arith
-      apply (insert linorder_le_less_linear [of m lb])
-      apply (erule_tac k2=n and k'2=n in A)
-       apply arith
-      apply simp
-      done
-  } note B = this
+  have *: R
+    if d: "i \<le> j \<or> m < j'"
+    and R1: "i * k \<le> j * k \<Longrightarrow> R"
+    and R2: "Suc m * k' \<le> j' * k' \<Longrightarrow> R"
+    for i j j' k k' m :: nat and R
+    using d
+    apply safe
+    apply (rule R1, erule mult_le_mono1)
+    apply (rule R2, erule Suc_le_eq [THEN iffD2 [THEN mult_le_mono1]])
+    done
+  have **: "0 < sc \<Longrightarrow> sc - n + (n + lb * n) \<le> m * n \<longleftrightarrow> sc + lb * n \<le> m * n"
+    for sc m n lb :: nat
+    apply safe
+     apply arith
+    apply (case_tac "sc \<ge> n")
+     apply arith
+    apply (insert linorder_le_less_linear [of m lb])
+    apply (erule_tac k=n and k'=n in *)
+     apply arith
+    apply simp
+    done
   show ?thesis
     apply (induct n nw w bs rule: bin_rsplit_aux.induct)
     apply (subst bin_rsplit_aux.simps)
-    apply (simp add: B Let_def split: prod.split)
+    apply (simp add: ** Let_def split: prod.split)
     done
 qed
 
-lemma bin_rsplit_len_le: 
-  "n \<noteq> 0 --> ws = bin_rsplit n (nw, w) --> (length ws <= m) = (nw <= m * n)"
-  unfolding bin_rsplit_def by (clarsimp simp add : bin_rsplit_aux_len_le)
- 
+lemma bin_rsplit_len_le: "n \<noteq> 0 \<longrightarrow> ws = bin_rsplit n (nw, w) \<longrightarrow> length ws \<le> m \<longleftrightarrow> nw \<le> m * n"
+  by (auto simp: bin_rsplit_def bin_rsplit_aux_len_le)
+
 lemma bin_rsplit_aux_len:
-  "n \<noteq> 0 \<Longrightarrow> length (bin_rsplit_aux n nw w cs) =
-    (nw + n - 1) div n + length cs"
+  "n \<noteq> 0 \<Longrightarrow> length (bin_rsplit_aux n nw w cs) = (nw + n - 1) div n + length cs"
   apply (induct n nw w cs rule: bin_rsplit_aux.induct)
   apply (subst bin_rsplit_aux.simps)
   apply (clarsimp simp: Let_def split: prod.split)
   apply (erule thin_rl)
   apply (case_tac m)
-  apply simp
-  apply (case_tac "m <= n")
+   apply simp
+  apply (case_tac "m \<le> n")
    apply (auto simp add: div_add_self2)
   done
 
-lemma bin_rsplit_len: 
-  "n\<noteq>0 ==> length (bin_rsplit n (nw, w)) = (nw + n - 1) div n"
-  unfolding bin_rsplit_def by (clarsimp simp add : bin_rsplit_aux_len)
+lemma bin_rsplit_len: "n \<noteq> 0 \<Longrightarrow> length (bin_rsplit n (nw, w)) = (nw + n - 1) div n"
+  by (auto simp: bin_rsplit_def bin_rsplit_aux_len)
 
 lemma bin_rsplit_aux_len_indep:
   "n \<noteq> 0 \<Longrightarrow> length bs = length cs \<Longrightarrow>
     length (bin_rsplit_aux n nw v bs) =
     length (bin_rsplit_aux n nw w cs)"
 proof (induct n nw w cs arbitrary: v bs rule: bin_rsplit_aux.induct)
-  case (1 n m w cs v bs) show ?case
+  case (1 n m w cs v bs)
+  show ?case
   proof (cases "m = 0")
-    case True then show ?thesis using \<open>length bs = length cs\<close> by simp
+    case True
+    with \<open>length bs = length cs\<close> show ?thesis by simp
   next
     case False
     from "1.hyps" \<open>m \<noteq> 0\<close> \<open>n \<noteq> 0\<close> have hyp: "\<And>v bs. length bs = Suc (length cs) \<Longrightarrow>
       length (bin_rsplit_aux n (m - n) v bs) =
       length (bin_rsplit_aux n (m - n) (fst (bin_split n w)) (snd (bin_split n w) # cs))"
-    by auto
-    show ?thesis using \<open>length bs = length cs\<close> \<open>n \<noteq> 0\<close>
-      by (auto simp add: bin_rsplit_aux_simp_alt Let_def bin_rsplit_len
-        split: prod.split)
+      by auto
+    from \<open>length bs = length cs\<close> \<open>n \<noteq> 0\<close> show ?thesis
+      by (auto simp add: bin_rsplit_aux_simp_alt Let_def bin_rsplit_len split: prod.split)
   qed
 qed
 
-lemma bin_rsplit_len_indep: 
-  "n\<noteq>0 ==> length (bin_rsplit n (nw, v)) = length (bin_rsplit n (nw, w))"
+lemma bin_rsplit_len_indep:
+  "n \<noteq> 0 \<Longrightarrow> length (bin_rsplit n (nw, v)) = length (bin_rsplit n (nw, w))"
   apply (unfold bin_rsplit_def)
   apply (simp (no_asm))
   apply (erule bin_rsplit_aux_len_indep)
@@ -1147,33 +1046,27 @@
 instantiation int :: bitss
 begin
 
-definition [iff]:
-  "i !! n \<longleftrightarrow> bin_nth i n"
+definition [iff]: "i !! n \<longleftrightarrow> bin_nth i n"
 
-definition
-  "lsb i = (i :: int) !! 0"
+definition "lsb i = i !! 0" for i :: int
 
-definition
-  "set_bit i n b = bin_sc n b i"
+definition "set_bit i n b = bin_sc n b i"
 
 definition
   "set_bits f =
-  (if \<exists>n. \<forall>n'\<ge>n. \<not> f n' then 
-     let n = LEAST n. \<forall>n'\<ge>n. \<not> f n'
-     in bl_to_bin (rev (map f [0..<n]))
-   else if \<exists>n. \<forall>n'\<ge>n. f n' then
-     let n = LEAST n. \<forall>n'\<ge>n. f n'
-     in sbintrunc n (bl_to_bin (True # rev (map f [0..<n])))
-   else 0 :: int)"
+    (if \<exists>n. \<forall>n'\<ge>n. \<not> f n' then
+      let n = LEAST n. \<forall>n'\<ge>n. \<not> f n'
+      in bl_to_bin (rev (map f [0..<n]))
+     else if \<exists>n. \<forall>n'\<ge>n. f n' then
+      let n = LEAST n. \<forall>n'\<ge>n. f n'
+      in sbintrunc n (bl_to_bin (True # rev (map f [0..<n])))
+     else 0 :: int)"
 
-definition
-  "shiftl x n = (x :: int) * 2 ^ n"
+definition "shiftl x n = x * 2 ^ n" for x :: int
 
-definition
-  "shiftr x n = (x :: int) div 2 ^ n"
+definition "shiftr x n = x div 2 ^ n" for x :: int
 
-definition
-  "msb x \<longleftrightarrow> (x :: int) < 0"
+definition "msb x \<longleftrightarrow> x < 0" for x :: int
 
 instance ..
 
diff -r 4ff2ba82d668 -r db7c97cdcfe7 src/HOL/Word/Examples/WordExamples.thy
--- a/src/HOL/Word/Examples/WordExamples.thy	Mon Apr 03 22:18:56 2017 +0200
+++ b/src/HOL/Word/Examples/WordExamples.thy	Mon Apr 03 23:12:44 2017 +0200
@@ -1,13 +1,13 @@
-(* 
-  Authors: Gerwin Klein and Thomas Sewell, NICTA
+(*  Title:      HOL/Word/Examples/WordExamples.thy
+    Authors:    Gerwin Klein and Thomas Sewell, NICTA
 
-  Examples demonstrating and testing various word operations.
+Examples demonstrating and testing various word operations.
 *)
 
 section "Examples of word operations"
 
 theory WordExamples
-imports "../Word" "../WordBitwise"
+  imports "../Word" "../WordBitwise"
 begin
 
 type_synonym word32 = "32 word"
@@ -28,7 +28,7 @@
 
 text "number ring simps"
 
-lemma 
+lemma
   "27 + 11 = (38::'a::len word)"
   "27 + 11 = (6::5 word)"
   "7 * 3 = (21::'a::len word)"
@@ -40,7 +40,7 @@
 lemma "word_pred 2 = 1" by simp
 
 lemma "word_succ (- 3) = -2" by simp
-  
+
 lemma "23 < (27::8 word)" by simp
 lemma "23 \<le> (27::8 word)" by simp
 lemma "\<not> 23 < (27::2 word)" by simp
@@ -69,8 +69,10 @@
 lemma "ucast (1 :: 4 word) = (1 :: 2 word)" by simp
 
 text "reducing goals to nat or int and arith:"
-lemma "i < x ==> i < (i + 1 :: 'a :: len word)" by unat_arith
-lemma "i < x ==> i < (i + 1 :: 'a :: len word)" by uint_arith
+lemma "i < x \<Longrightarrow> i < i + 1" for i x :: "'a::len word"
+  by unat_arith
+lemma "i < x \<Longrightarrow> i < i + 1" for i x :: "'a::len word"
+  by unat_arith
 
 text "bool lists"
 
@@ -111,7 +113,7 @@
 lemma "\<not> (0b1000 :: 3 word) !! 4" by simp
 lemma "\<not> (1 :: 3 word) !! 2" by simp
 
-lemma "(0b11000 :: 10 word) !! n = (n = 4 \<or> n = 3)" 
+lemma "(0b11000 :: 10 word) !! n = (n = 4 \<or> n = 3)"
   by (auto simp add: bin_nth_Bit0 bin_nth_Bit1)
 
 lemma "set_bit 55 7 True = (183::'a::len0 word)" by simp
@@ -133,7 +135,7 @@
 lemma "\<not> msb (0::4 word)" by simp
 
 lemma "word_cat (27::4 word) (27::8 word) = (2843::'a::len word)" by simp
-lemma "word_cat (0b0011::4 word) (0b1111::6word) = (0b0011001111 :: 10 word)" 
+lemma "word_cat (0b0011::4 word) (0b1111::6word) = (0b0011001111 :: 10 word)"
   by simp
 
 lemma "0b1011 << 2 = (0b101100::'a::len0 word)" by simp
@@ -171,20 +173,24 @@
 
 text "more proofs using bitwise expansion"
 
-lemma "((x :: 10 word) AND NOT 3) >> 4 << 2 = ((x >> 2) AND NOT 3)"
+lemma "(x AND NOT 3) >> 4 << 2 = ((x >> 2) AND NOT 3)"
+  for x :: "10 word"
   by word_bitwise
 
-lemma "(((x :: 12 word) AND -8) >> 3) AND 7 = (x AND 56) >> 3"
+lemma "((x AND -8) >> 3) AND 7 = (x AND 56) >> 3"
+  for x :: "12 word"
   by word_bitwise
 
 text "some problems require further reasoning after bit expansion"
 
-lemma "x \<le> (42 :: 8 word) \<Longrightarrow> x \<le> 89"
+lemma "x \<le> 42 \<Longrightarrow> x \<le> 89"
+  for x :: "8 word"
   apply word_bitwise
   apply blast
   done
 
-lemma "((x :: word32) AND 1023) = 0 \<Longrightarrow> x \<le> -1024"
+lemma "(x AND 1023) = 0 \<Longrightarrow> x \<le> -1024"
+  for x :: word32
   apply word_bitwise
   apply clarsimp
   done
@@ -192,11 +198,10 @@
 text "operations like shifts by non-numerals will expose some internal list
  representations but may still be easy to solve"
 
-lemma shiftr_overflow:
-  "32 \<le> a \<Longrightarrow> (b::word32) >> a = 0"
-  apply (word_bitwise)
+lemma shiftr_overflow: "32 \<le> a \<Longrightarrow> b >> a = 0"
+  for b :: word32
+  apply word_bitwise
   apply simp
   done
 
-
 end
diff -r 4ff2ba82d668 -r db7c97cdcfe7 src/HOL/Word/Misc_Numeric.thy
--- a/src/HOL/Word/Misc_Numeric.thy	Mon Apr 03 22:18:56 2017 +0200
+++ b/src/HOL/Word/Misc_Numeric.thy	Mon Apr 03 23:12:44 2017 +0200
@@ -1,76 +1,66 @@
-(* 
-  Author:  Jeremy Dawson, NICTA
-*) 
+(*  Title:      HOL/Word/Misc_Numeric.thy
+    Author:     Jeremy Dawson, NICTA
+*)
 
 section \<open>Useful Numerical Lemmas\<close>
 
 theory Misc_Numeric
-imports Main
+  imports Main
 begin
 
-lemma one_mod_exp_eq_one [simp]:
-  "1 mod (2 * 2 ^ n) = (1::int)"
+lemma one_mod_exp_eq_one [simp]: "1 mod (2 * 2 ^ n) = (1::int)"
   by (smt mod_pos_pos_trivial zero_less_power)
 
-lemma mod_2_neq_1_eq_eq_0:
-  fixes k :: int
-  shows "k mod 2 \<noteq> 1 \<longleftrightarrow> k mod 2 = 0"
+lemma mod_2_neq_1_eq_eq_0: "k mod 2 \<noteq> 1 \<longleftrightarrow> k mod 2 = 0"
+  for k :: int
   by (fact not_mod_2_eq_1_eq_0)
 
-lemma z1pmod2:
-  fixes b :: int
-  shows "(2 * b + 1) mod 2 = (1::int)"
+lemma z1pmod2: "(2 * b + 1) mod 2 = (1::int)"
+  for b :: int
   by arith
 
-lemma diff_le_eq':
-  "a - b \<le> c \<longleftrightarrow> a \<le> b + (c::int)"
+lemma diff_le_eq': "a - b \<le> c \<longleftrightarrow> a \<le> b + c"
+  for a b c :: int
   by arith
 
-lemma emep1:
-  fixes n d :: int
-  shows "even n \<Longrightarrow> even d \<Longrightarrow> 0 \<le> d \<Longrightarrow> (n + 1) mod d = (n mod d) + 1"
+lemma emep1: "even n \<Longrightarrow> even d \<Longrightarrow> 0 \<le> d \<Longrightarrow> (n + 1) mod d = (n mod d) + 1"
+  for n d :: int
   by (auto simp add: pos_zmod_mult_2 add.commute dvd_def)
 
-lemma int_mod_ge:
-  "a < n \<Longrightarrow> 0 < (n :: int) \<Longrightarrow> a \<le> a mod n"
+lemma int_mod_ge: "a < n \<Longrightarrow> 0 < n \<Longrightarrow> a \<le> a mod n"
+  for a n :: int
   by (metis dual_order.trans le_cases mod_pos_pos_trivial pos_mod_conj)
 
-lemma int_mod_ge':
-  "b < 0 \<Longrightarrow> 0 < (n :: int) \<Longrightarrow> b + n \<le> b mod n"
+lemma int_mod_ge': "b < 0 \<Longrightarrow> 0 < n \<Longrightarrow> b + n \<le> b mod n"
+  for b n :: int
   by (metis add_less_same_cancel2 int_mod_ge mod_add_self2)
 
-lemma int_mod_le':
-  "(0::int) \<le> b - n \<Longrightarrow> b mod n \<le> b - n"
+lemma int_mod_le': "0 \<le> b - n \<Longrightarrow> b mod n \<le> b - n"
+  for b n :: int
   by (metis minus_mod_self2 zmod_le_nonneg_dividend)
 
-lemma zless2:
-  "0 < (2 :: int)"
+lemma zless2: "0 < (2 :: int)"
   by (fact zero_less_numeral)
 
-lemma zless2p:
-  "0 < (2 ^ n :: int)"
+lemma zless2p: "0 < (2 ^ n :: int)"
   by arith
 
-lemma zle2p:
-  "0 \<le> (2 ^ n :: int)"
+lemma zle2p: "0 \<le> (2 ^ n :: int)"
   by arith
 
-lemma m1mod2k:
-  "- 1 mod 2 ^ n = (2 ^ n - 1 :: int)"
+lemma m1mod2k: "- 1 mod 2 ^ n = (2 ^ n - 1 :: int)"
   using zless2p by (rule zmod_minus1)
 
-lemma p1mod22k':
-  fixes b :: int
-  shows "(1 + 2 * b) mod (2 * 2 ^ n) = 1 + 2 * (b mod 2 ^ n)"
-  using zle2p by (rule pos_zmod_mult_2) 
+lemma p1mod22k': "(1 + 2 * b) mod (2 * 2 ^ n) = 1 + 2 * (b mod 2 ^ n)"
+  for b :: int
+  using zle2p by (rule pos_zmod_mult_2)
 
-lemma p1mod22k:
-  fixes b :: int
-  shows "(2 * b + 1) mod (2 * 2 ^ n) = 2 * (b mod 2 ^ n) + 1"
+lemma p1mod22k: "(2 * b + 1) mod (2 * 2 ^ n) = 2 * (b mod 2 ^ n) + 1"
+  for b :: int
   by (simp add: p1mod22k' add.commute)
 
-lemma int_mod_lem: 
-  "(0 :: int) < n ==> (0 <= b & b < n) = (b mod n = b)"
+lemma int_mod_lem: "0 < n \<Longrightarrow> 0 \<le> b \<and> b < n \<longleftrightarrow> b mod n = b"
+  for b n :: int
   apply safe
     apply (erule (1) mod_pos_pos_trivial)
    apply (erule_tac [!] subst)
@@ -78,4 +68,3 @@
   done
 
 end
-
diff -r 4ff2ba82d668 -r db7c97cdcfe7 src/HOL/Word/Misc_Typedef.thy
--- a/src/HOL/Word/Misc_Typedef.thy	Mon Apr 03 22:18:56 2017 +0200
+++ b/src/HOL/Word/Misc_Typedef.thy	Mon Apr 03 23:12:44 2017 +0200
@@ -1,4 +1,4 @@
-(* 
+(*
   Author:     Jeremy Dawson and Gerwin Klein, NICTA
 
   Consequences of type definition theorems, and of extended type definition.
@@ -18,7 +18,7 @@
   tdD3: "type_definition Rep Abs A \<Longrightarrow> \<forall>y. y \<in> A \<longrightarrow> Rep (Abs y) = y"
   by (auto simp: type_definition_def)
 
-lemma td_nat_int: 
+lemma td_nat_int:
   "type_definition int nat (Collect (op <= 0))"
   unfolding type_definition_def by auto
 
@@ -29,13 +29,13 @@
 
 lemma Abs_eqD: "Abs x = Abs y ==> x \<in> A ==> y \<in> A ==> x = y"
   by (simp add: Abs_inject)
-   
-lemma Abs_inverse': 
+
+lemma Abs_inverse':
   "r : A ==> Abs r = a ==> Rep a = r"
   by (safe elim!: Abs_inverse)
 
-lemma Rep_comp_inverse: 
-  "Rep o f = g ==> Abs o g = f"
+lemma Rep_comp_inverse:
+  "Rep \<circ> f = g ==> Abs \<circ> g = f"
   using Rep_inverse by auto
 
 lemma Rep_eqD [elim!]: "Rep x = Rep y ==> x = y"
@@ -44,27 +44,27 @@
 lemma Rep_inverse': "Rep a = r ==> Abs r = a"
   by (safe intro!: Rep_inverse)
 
-lemma comp_Abs_inverse: 
-  "f o Abs = g ==> g o Rep = f"
+lemma comp_Abs_inverse:
+  "f \<circ> Abs = g ==> g \<circ> Rep = f"
   using Rep_inverse by auto
 
-lemma set_Rep: 
+lemma set_Rep:
   "A = range Rep"
 proof (rule set_eqI)
   fix x
   show "(x \<in> A) = (x \<in> range Rep)"
     by (auto dest: Abs_inverse [of x, symmetric])
-qed  
+qed
 
-lemma set_Rep_Abs: "A = range (Rep o Abs)"
+lemma set_Rep_Abs: "A = range (Rep \<circ> Abs)"
 proof (rule set_eqI)
   fix x
-  show "(x \<in> A) = (x \<in> range (Rep o Abs))"
+  show "(x \<in> A) = (x \<in> range (Rep \<circ> Abs))"
     by (auto dest: Abs_inverse [of x, symmetric])
-qed  
+qed
 
 lemma Abs_inj_on: "inj_on Abs A"
-  unfolding inj_on_def 
+  unfolding inj_on_def
   by (auto dest: Abs_inject [THEN iffD1])
 
 lemma image: "Abs ` A = UNIV"
@@ -72,16 +72,16 @@
 
 lemmas td_thm = type_definition_axioms
 
-lemma fns1: 
-  "Rep o fa = fr o Rep | fa o Abs = Abs o fr ==> Abs o fr o Rep = fa"
+lemma fns1:
+  "Rep \<circ> fa = fr \<circ> Rep | fa \<circ> Abs = Abs \<circ> fr ==> Abs \<circ> fr \<circ> Rep = fa"
   by (auto dest: Rep_comp_inverse elim: comp_Abs_inverse simp: o_assoc)
 
 lemmas fns1a = disjI1 [THEN fns1]
 lemmas fns1b = disjI2 [THEN fns1]
 
 lemma fns4:
-  "Rep o fa o Abs = fr ==> 
-   Rep o fa = fr o Rep & fa o Abs = Abs o fr"
+  "Rep \<circ> fa \<circ> Abs = fr ==>
+   Rep \<circ> fa = fr \<circ> Rep & fa \<circ> Abs = Abs \<circ> fr"
   by auto
 
 end
@@ -99,16 +99,16 @@
 subsection "Extended form of type definition predicate"
 
 lemma td_conds:
-  "norm o norm = norm ==> (fr o norm = norm o fr) = 
-    (norm o fr o norm = fr o norm & norm o fr o norm = norm o fr)"
+  "norm \<circ> norm = norm ==> (fr \<circ> norm = norm \<circ> fr) =
+    (norm \<circ> fr \<circ> norm = fr \<circ> norm & norm \<circ> fr \<circ> norm = norm \<circ> fr)"
   apply safe
     apply (simp_all add: comp_assoc)
    apply (simp_all add: o_assoc)
   done
 
 lemma fn_comm_power:
-  "fa o tr = tr o fr ==> fa ^^ n o tr = tr o fr ^^ n" 
-  apply (rule ext) 
+  "fa \<circ> tr = tr \<circ> fr ==> fa ^^ n \<circ> tr = tr \<circ> fr ^^ n"
+  apply (rule ext)
   apply (induct n)
    apply (auto dest: fun_cong)
   done
@@ -122,15 +122,15 @@
   assumes eq_norm: "\<And>x. Rep (Abs x) = norm x"
 begin
 
-lemma Abs_norm [simp]: 
+lemma Abs_norm [simp]:
   "Abs (norm x) = Abs x"
   using eq_norm [of x] by (auto elim: Rep_inverse')
 
 lemma td_th:
-  "g o Abs = f ==> f (Rep x) = g x"
+  "g \<circ> Abs = f ==> f (Rep x) = g x"
   by (drule comp_Abs_inverse [symmetric]) simp
 
-lemma eq_norm': "Rep o Abs = norm"
+lemma eq_norm': "Rep \<circ> Abs = norm"
   by (auto simp: eq_norm)
 
 lemma norm_Rep [simp]: "norm (Rep x) = Rep x"
@@ -141,42 +141,42 @@
 lemma set_iff_norm: "w : A \<longleftrightarrow> w = norm w"
   by (auto simp: set_Rep_Abs eq_norm' eq_norm [symmetric])
 
-lemma inverse_norm: 
+lemma inverse_norm:
   "(Abs n = w) = (Rep w = norm n)"
   apply (rule iffI)
    apply (clarsimp simp add: eq_norm)
   apply (simp add: eq_norm' [symmetric])
   done
 
-lemma norm_eq_iff: 
+lemma norm_eq_iff:
   "(norm x = norm y) = (Abs x = Abs y)"
   by (simp add: eq_norm' [symmetric])
 
-lemma norm_comps: 
-  "Abs o norm = Abs" 
-  "norm o Rep = Rep" 
-  "norm o norm = norm"
+lemma norm_comps:
+  "Abs \<circ> norm = Abs"
+  "norm \<circ> Rep = Rep"
+  "norm \<circ> norm = norm"
   by (auto simp: eq_norm' [symmetric] o_def)
 
 lemmas norm_norm [simp] = norm_comps
 
-lemma fns5: 
-  "Rep o fa o Abs = fr ==> 
-  fr o norm = fr & norm o fr = fr"
+lemma fns5:
+  "Rep \<circ> fa \<circ> Abs = fr ==>
+  fr \<circ> norm = fr & norm \<circ> fr = fr"
   by (fold eq_norm') auto
 
 (* following give conditions for converses to td_fns1
-  the condition (norm o fr o norm = fr o norm) says that 
+  the condition (norm \<circ> fr \<circ> norm = fr \<circ> norm) says that
   fr takes normalised arguments to normalised results,
-  (norm o fr o norm = norm o fr) says that fr 
+  (norm \<circ> fr \<circ> norm = norm \<circ> fr) says that fr
   takes norm-equivalent arguments to norm-equivalent results,
-  (fr o norm = fr) says that fr 
-  takes norm-equivalent arguments to the same result, and 
-  (norm o fr = fr) says that fr takes any argument to a normalised result 
+  (fr \<circ> norm = fr) says that fr
+  takes norm-equivalent arguments to the same result, and
+  (norm \<circ> fr = fr) says that fr takes any argument to a normalised result
   *)
-lemma fns2: 
-  "Abs o fr o Rep = fa ==> 
-   (norm o fr o norm = fr o norm) = (Rep o fa = fr o Rep)"
+lemma fns2:
+  "Abs \<circ> fr \<circ> Rep = fa ==>
+   (norm \<circ> fr \<circ> norm = fr \<circ> norm) = (Rep \<circ> fa = fr \<circ> Rep)"
   apply (fold eq_norm')
   apply safe
    prefer 2
@@ -186,25 +186,25 @@
   apply auto
   done
 
-lemma fns3: 
-  "Abs o fr o Rep = fa ==> 
-   (norm o fr o norm = norm o fr) = (fa o Abs = Abs o fr)"
+lemma fns3:
+  "Abs \<circ> fr \<circ> Rep = fa ==>
+   (norm \<circ> fr \<circ> norm = norm \<circ> fr) = (fa \<circ> Abs = Abs \<circ> fr)"
   apply (fold eq_norm')
   apply safe
    prefer 2
    apply (simp add: comp_assoc)
   apply (rule ext)
-  apply (drule_tac f="a o b" for a b in fun_cong)
+  apply (drule_tac f="a \<circ> b" for a b in fun_cong)
   apply simp
   done
 
-lemma fns: 
-  "fr o norm = norm o fr ==> 
-    (fa o Abs = Abs o fr) = (Rep o fa = fr o Rep)"
+lemma fns:
+  "fr \<circ> norm = norm \<circ> fr ==>
+    (fa \<circ> Abs = Abs \<circ> fr) = (Rep \<circ> fa = fr \<circ> Rep)"
   apply safe
    apply (frule fns1b)
-   prefer 2 
-   apply (frule fns1a) 
+   prefer 2
+   apply (frule fns1a)
    apply (rule fns3 [THEN iffD1])
      prefer 3
      apply (rule fns2 [THEN iffD1])
@@ -213,7 +213,7 @@
   done
 
 lemma range_norm:
-  "range (Rep o Abs) = A"
+  "range (Rep \<circ> Abs) = A"
   by (simp add: set_Rep_Abs)
 
 end
diff -r 4ff2ba82d668 -r db7c97cdcfe7 src/HOL/Word/Word.thy
--- a/src/HOL/Word/Word.thy	Mon Apr 03 22:18:56 2017 +0200
+++ b/src/HOL/Word/Word.thy	Mon Apr 03 23:12:44 2017 +0200
@@ -1827,8 +1827,8 @@
   by (auto simp: unat_word_ariths intro!: trans [OF _ nat_mod_lem])
 
 lemma unat_mult_lem:
-  "unat x * unat y < 2 ^ len_of TYPE('a) \<longleftrightarrow>
-    unat (x * y :: 'a::len word) = unat x * unat y"
+  "unat x * unat y < 2 ^ len_of TYPE('a) \<longleftrightarrow> unat (x * y) = unat x * unat y"
+  for x y :: "'a::len word"
   by (auto simp: unat_word_ariths intro!: trans [OF _ nat_mod_lem])
 
 lemmas unat_plus_if' =
@@ -2002,7 +2002,7 @@
 
 lemmas div_lt_uint'' = order_less_imp_le [THEN div_lt_uint']
 
-lemma word_le_exists': "x \<le> y \<Longrightarrow> (\<exists>z. y = x + z \<and> uint x + uint z < 2 ^ len_of TYPE('a))"
+lemma word_le_exists': "x \<le> y \<Longrightarrow> \<exists>z. y = x + z \<and> uint x + uint z < 2 ^ len_of TYPE('a)"
   for x y z :: "'a::len0 word"
   apply (rule exI)
   apply (rule conjI)
@@ -2330,13 +2330,15 @@
   unfolding to_bl_def word_log_defs bl_and_bin
   by (simp add: word_ubin.eq_norm)
 
-lemma word_lsb_alt: "lsb (w::'a::len0 word) = test_bit w 0"
+lemma word_lsb_alt: "lsb w = test_bit w 0"
+  for w :: "'a::len0 word"
   by (auto simp: word_test_bit_def word_lsb_def)
 
 lemma word_lsb_1_0 [simp]: "lsb (1::'a::len word) \<and> \<not> lsb (0::'b::len0 word)"
   unfolding word_lsb_def uint_eq_0 uint_1 by simp
 
-lemma word_lsb_last: "lsb (w::'a::len word) = last (to_bl w)"
+lemma word_lsb_last: "lsb w = last (to_bl w)"
+  for w :: "'a::len word"
   apply (unfold word_lsb_def uint_bl bin_to_bl_def)
   apply (rule_tac bin="uint w" in bin_exhaust)
   apply (cases "size w")
@@ -2419,7 +2421,7 @@
   done
 
 lemma of_bl_rep_False: "of_bl (replicate n False @ bs) = of_bl bs"
-  unfolding of_bl_def bl_to_bin_rep_F by auto
+  by (auto simp: of_bl_def bl_to_bin_rep_F)
 
 lemma msb_nth: "msb w = w !! (len_of TYPE('a) - 1)"
   for w :: "'a::len word"
@@ -2762,7 +2764,8 @@
 lemma shiftl1_of_bl: "shiftl1 (of_bl bl) = of_bl (bl @ [False])"
   by (simp add: of_bl_def bl_to_bin_append)
 
-lemma shiftl1_bl: "shiftl1 (w::'a::len0 word) = of_bl (to_bl w @ [False])"
+lemma shiftl1_bl: "shiftl1 w = of_bl (to_bl w @ [False])"
+  for w :: "'a::len0 word"
 proof -
   have "shiftl1 w = shiftl1 (of_bl (to_bl w))"
     by simp
@@ -2970,7 +2973,7 @@
   for x :: "'a::len0 word"
   using shiftr_bl_of [where 'a='a, of "to_bl x"] by simp
 
-lemma msb_shift: "msb w \<longleftrightarrow> (w >> (len_of TYPE('a) - 1)) \<noteq> 0"
+lemma msb_shift: "msb w \<longleftrightarrow> w >> (len_of TYPE('a) - 1) \<noteq> 0"
   for w :: "'a::len word"
   apply (unfold shiftr_bl word_msb_alt)
   apply (simp add: word_size Suc_le_eq take_Suc)
@@ -3091,10 +3094,11 @@
    apply auto
   done
 
-lemma eq_mod_iff: "0 < (n::int) \<Longrightarrow> b = b mod n \<longleftrightarrow> 0 \<le> b \<and> b < n"
+lemma eq_mod_iff: "0 < n \<Longrightarrow> b = b mod n \<longleftrightarrow> 0 \<le> b \<and> b < n"
+  for b n :: int
   by (simp add: int_mod_lem eq_sym_conv)
 
-lemma mask_eq_iff: "(w AND mask n) = w \<longleftrightarrow> uint w < 2 ^ n"
+lemma mask_eq_iff: "w AND mask n = w \<longleftrightarrow> uint w < 2 ^ n"
   apply (simp add: and_mask_bintr)
   apply (simp add: word_ubin.inverse_norm)
   apply (simp add: eq_mod_iff bintrunc_mod2p min_def)
@@ -3632,8 +3636,9 @@
       split: prod.split)
 
 lemma test_bit_rsplit:
-  "sw = word_rsplit w \<Longrightarrow> m < size (hd sw :: 'a::len word) \<Longrightarrow>
-    k < length sw \<Longrightarrow> (rev sw ! k) !! m = (w !! (k * size (hd sw) + m))"
+  "sw = word_rsplit w \<Longrightarrow> m < size (hd sw) \<Longrightarrow>
+    k < length sw \<Longrightarrow> (rev sw ! k) !! m = w !! (k * size (hd sw) + m)"
+  for sw :: "'a::len word list"
   apply (unfold word_rsplit_def word_test_bit_def)
   apply (rule trans)
    apply (rule_tac f = "\<lambda>x. bin_nth x m" in arg_cong)
@@ -3673,8 +3678,9 @@
   done
 
 lemma test_bit_rcat:
-  "sw = size (hd wl :: 'a::len word) \<Longrightarrow> rc = word_rcat wl \<Longrightarrow> rc !! n =
+  "sw = size (hd wl) \<Longrightarrow> rc = word_rcat wl \<Longrightarrow> rc !! n =
     (n < size rc \<and> n div sw < size wl \<and> (rev wl) ! (n div sw) !! (n mod sw))"
+  for wl :: "'a::len word list"
   apply (unfold word_rcat_bl word_size)
   apply (clarsimp simp add: test_bit_of_bl size_rcat_lem word_size td_gal_lt_len)
   apply safe
@@ -4266,10 +4272,11 @@
   by (simp add: word_arith_wis int_word_uint mod_add_if_z word_size)
 
 lemma unat_plus_if_size:
-  "unat (x + (y::'a::len word)) =
+  "unat (x + y) =
     (if unat x + unat y < 2^size x
      then unat x + unat y
      else unat x + unat y - 2^size x)"
+  for x y :: "'a::len word"
   apply (subst word_arith_nat_defs)
   apply (subst unat_of_nat)
   apply (simp add:  mod_nat_add word_size)
@@ -4339,7 +4346,7 @@
   shows "(x - y) mod b = z' mod b'"
   using assms [symmetric] by (auto intro: mod_diff_cong)
 
-lemma word_induct_less: "\<lbrakk>P 0; \<And>n. \<lbrakk>n < m; P n\<rbrakk> \<Longrightarrow> P (1 + n)\<rbrakk> \<Longrightarrow> P m"
+lemma word_induct_less: "P 0 \<Longrightarrow> (\<And>n. n < m \<Longrightarrow> P n \<Longrightarrow> P (1 + n)) \<Longrightarrow> P m"
   for P :: "'a::len word \<Rightarrow> bool"
   apply (cases m)
   apply atomize
@@ -4362,11 +4369,11 @@
   apply simp
   done
 
-lemma word_induct: "\<lbrakk>P 0; \<And>n. P n \<Longrightarrow> P (1 + n)\<rbrakk> \<Longrightarrow> P m"
+lemma word_induct: "P 0 \<Longrightarrow> (\<And>n. P n \<Longrightarrow> P (1 + n)) \<Longrightarrow> P m"
   for P :: "'a::len word \<Rightarrow> bool"
   by (erule word_induct_less) simp
 
-lemma word_induct2 [induct type]: "\<lbrakk>P 0; \<And>n. \<lbrakk>1 + n \<noteq> 0; P n\<rbrakk> \<Longrightarrow> P (1 + n)\<rbrakk> \<Longrightarrow> P n"
+lemma word_induct2 [induct type]: "P 0 \<Longrightarrow> (\<And>n. 1 + n \<noteq> 0 \<Longrightarrow> P n \<Longrightarrow> P (1 + n)) \<Longrightarrow> P n"
   for P :: "'b::len word \<Rightarrow> bool"
   apply (rule word_induct)
    apply simp
@@ -4383,16 +4390,15 @@
 lemma word_rec_0: "word_rec z s 0 = z"
   by (simp add: word_rec_def)
 
-lemma word_rec_Suc:
-  "1 + n \<noteq> (0::'a::len word) \<Longrightarrow> word_rec z s (1 + n) = s n (word_rec z s n)"
+lemma word_rec_Suc: "1 + n \<noteq> 0 \<Longrightarrow> word_rec z s (1 + n) = s n (word_rec z s n)"
+  for n :: "'a::len word"
   apply (simp add: word_rec_def unat_word_ariths)
   apply (subst nat_mod_eq')
    apply (metis Suc_eq_plus1_left Suc_lessI of_nat_2p unat_1 unat_lt2p word_arith_nat_add)
   apply simp
   done
 
-lemma word_rec_Pred:
-  "n \<noteq> 0 \<Longrightarrow> word_rec z s n = s (n - 1) (word_rec z s (n - 1))"
+lemma word_rec_Pred: "n \<noteq> 0 \<Longrightarrow> word_rec z s n = s (n - 1) (word_rec z s (n - 1))"
   apply (rule subst[where t="n" and s="1 + (n - 1)"])
    apply simp
   apply (subst word_rec_Suc)
@@ -4468,7 +4474,8 @@
   apply simp
   done
 
-lemma unatSuc: "1 + n \<noteq> (0::'a::len word) \<Longrightarrow> unat (1 + n) = Suc (unat n)"
+lemma unatSuc: "1 + n \<noteq> 0 \<Longrightarrow> unat (1 + n) = Suc (unat n)"
+  for n :: "'a::len word"
   by unat_arith
 
 declare bin_to_bl_def [simp]
diff -r 4ff2ba82d668 -r db7c97cdcfe7 src/HOL/Word/WordBitwise.thy
--- a/src/HOL/Word/WordBitwise.thy	Mon Apr 03 22:18:56 2017 +0200
+++ b/src/HOL/Word/WordBitwise.thy	Mon Apr 03 23:12:44 2017 +0200
@@ -2,24 +2,17 @@
     Authors:    Thomas Sewell, NICTA and Sascha Boehme, TU Muenchen
 *)
 
-
 theory WordBitwise
-
-imports Word
-
+  imports Word
 begin
 
 text \<open>Helper constants used in defining addition\<close>
 
-definition
-  xor3 :: "bool \<Rightarrow> bool \<Rightarrow> bool \<Rightarrow> bool"
-where
- "xor3 a b c = (a = (b = c))"
+definition xor3 :: "bool \<Rightarrow> bool \<Rightarrow> bool \<Rightarrow> bool"
+  where "xor3 a b c = (a = (b = c))"
 
-definition
-  carry :: "bool \<Rightarrow> bool \<Rightarrow> bool \<Rightarrow> bool"
-where
- "carry a b c = ((a \<and> (b \<or> c)) \<or> (b \<and> c))"
+definition carry :: "bool \<Rightarrow> bool \<Rightarrow> bool \<Rightarrow> bool"
+  where "carry a b c = ((a \<and> (b \<or> c)) \<or> (b \<and> c))"
 
 lemma carry_simps:
   "carry True a b = (a \<or> b)"
@@ -40,36 +33,28 @@
   by (simp_all add: xor3_def)
 
 text \<open>Breaking up word equalities into equalities on their
-bit lists. Equalities are generated and manipulated in the
-reverse order to to_bl.\<close>
+  bit lists. Equalities are generated and manipulated in the
+  reverse order to to_bl.\<close>
 
-lemma word_eq_rbl_eq:
-  "(x = y) = (rev (to_bl x) = rev (to_bl y))"
+lemma word_eq_rbl_eq: "x = y \<longleftrightarrow> rev (to_bl x) = rev (to_bl y)"
   by simp
 
-lemma rbl_word_or:
-  "rev (to_bl (x OR y)) = map2 op \<or> (rev (to_bl x)) (rev (to_bl y))"
+lemma rbl_word_or: "rev (to_bl (x OR y)) = map2 op \<or> (rev (to_bl x)) (rev (to_bl y))"
   by (simp add: map2_def zip_rev bl_word_or rev_map)
 
-lemma rbl_word_and:
-  "rev (to_bl (x AND y)) = map2 op \<and> (rev (to_bl x)) (rev (to_bl y))"
+lemma rbl_word_and: "rev (to_bl (x AND y)) = map2 op \<and> (rev (to_bl x)) (rev (to_bl y))"
   by (simp add: map2_def zip_rev bl_word_and rev_map)
 
-lemma rbl_word_xor:
-  "rev (to_bl (x XOR y)) = map2 op \<noteq> (rev (to_bl x)) (rev (to_bl y))"
+lemma rbl_word_xor: "rev (to_bl (x XOR y)) = map2 op \<noteq> (rev (to_bl x)) (rev (to_bl y))"
   by (simp add: map2_def zip_rev bl_word_xor rev_map)
 
-lemma rbl_word_not:
-  "rev (to_bl (NOT x)) = map Not (rev (to_bl x))"
+lemma rbl_word_not: "rev (to_bl (NOT x)) = map Not (rev (to_bl x))"
   by (simp add: bl_word_not rev_map)
 
-lemma bl_word_sub:
-  "to_bl (x - y) = to_bl (x + (- y))"
+lemma bl_word_sub: "to_bl (x - y) = to_bl (x + (- y))"
   by simp
 
-lemma rbl_word_1:
-  "rev (to_bl (1 :: ('a :: len0) word))
-     = takefill False (len_of TYPE('a)) [True]"
+lemma rbl_word_1: "rev (to_bl (1 :: 'a::len0 word)) = takefill False (len_of TYPE('a)) [True]"
   apply (rule_tac s="rev (to_bl (word_succ (0 :: 'a word)))" in trans)
    apply simp
   apply (simp only: rtb_rbl_ariths(1)[OF refl])
@@ -79,22 +64,18 @@
   apply (simp add: takefill_alt)
   done
 
-lemma rbl_word_if:
-  "rev (to_bl (if P then x else y))
-      = map2 (If P) (rev (to_bl x)) (rev (to_bl y))"
+lemma rbl_word_if: "rev (to_bl (if P then x else y)) = map2 (If P) (rev (to_bl x)) (rev (to_bl y))"
   by (simp add: map2_def split_def)
 
 lemma rbl_add_carry_Cons:
-  "(if car then rbl_succ else id) (rbl_add (x # xs) (y # ys))
-        = xor3 x y car # (if carry x y car then rbl_succ else id)
-             (rbl_add xs ys)"
+  "(if car then rbl_succ else id) (rbl_add (x # xs) (y # ys)) =
+    xor3 x y car # (if carry x y car then rbl_succ else id) (rbl_add xs ys)"
   by (simp add: carry_def xor3_def)
 
 lemma rbl_add_suc_carry_fold:
   "length xs = length ys \<Longrightarrow>
-   \<forall>car. (if car then rbl_succ else id) (rbl_add xs ys)
-        = (foldr (\<lambda>(x, y) res car. xor3 x y car # res (carry x y car))
-                 (zip xs ys) (\<lambda>_. [])) car"
+    \<forall>car. (if car then rbl_succ else id) (rbl_add xs ys) =
+      (foldr (\<lambda>(x, y) res car. xor3 x y car # res (carry x y car)) (zip xs ys) (\<lambda>_. [])) car"
   apply (erule list_induct2)
    apply simp
   apply (simp only: rbl_add_carry_Cons)
@@ -102,84 +83,70 @@
   done
 
 lemma to_bl_plus_carry:
-  "to_bl (x + y)
-     = rev (foldr (\<lambda>(x, y) res car. xor3 x y car # res (carry x y car))
-                 (rev (zip (to_bl x) (to_bl y))) (\<lambda>_. []) False)"
+  "to_bl (x + y) =
+    rev (foldr (\<lambda>(x, y) res car. xor3 x y car # res (carry x y car))
+      (rev (zip (to_bl x) (to_bl y))) (\<lambda>_. []) False)"
   using rbl_add_suc_carry_fold[where xs="rev (to_bl x)" and ys="rev (to_bl y)"]
   apply (simp add: word_add_rbl[OF refl refl])
   apply (drule_tac x=False in spec)
   apply (simp add: zip_rev)
   done
 
-definition
- "rbl_plus cin xs ys = foldr
-       (\<lambda>(x, y) res car. xor3 x y car # res (carry x y car))
-       (zip xs ys) (\<lambda>_. []) cin"
+definition "rbl_plus cin xs ys =
+  foldr (\<lambda>(x, y) res car. xor3 x y car # res (carry x y car)) (zip xs ys) (\<lambda>_. []) cin"
 
 lemma rbl_plus_simps:
-  "rbl_plus cin (x # xs) (y # ys)
-      = xor3 x y cin # rbl_plus (carry x y cin) xs ys"
+  "rbl_plus cin (x # xs) (y # ys) = xor3 x y cin # rbl_plus (carry x y cin) xs ys"
   "rbl_plus cin [] ys = []"
   "rbl_plus cin xs [] = []"
   by (simp_all add: rbl_plus_def)
 
-lemma rbl_word_plus:
-  "rev (to_bl (x + y)) = rbl_plus False (rev (to_bl x)) (rev (to_bl y))"
+lemma rbl_word_plus: "rev (to_bl (x + y)) = rbl_plus False (rev (to_bl x)) (rev (to_bl y))"
   by (simp add: rbl_plus_def to_bl_plus_carry zip_rev)
 
-definition
- "rbl_succ2 b xs = (if b then rbl_succ xs else xs)"
+definition "rbl_succ2 b xs = (if b then rbl_succ xs else xs)"
 
 lemma rbl_succ2_simps:
   "rbl_succ2 b [] = []"
   "rbl_succ2 b (x # xs) = (b \<noteq> x) # rbl_succ2 (x \<and> b) xs"
   by (simp_all add: rbl_succ2_def)
 
-lemma twos_complement:
-  "- x = word_succ (NOT x)"
+lemma twos_complement: "- x = word_succ (NOT x)"
   using arg_cong[OF word_add_not[where x=x], where f="\<lambda>a. a - x + 1"]
-  by (simp add: word_succ_p1 word_sp_01[unfolded word_succ_p1]
-           del: word_add_not)
+  by (simp add: word_succ_p1 word_sp_01[unfolded word_succ_p1] del: word_add_not)
 
-lemma rbl_word_neg:
-  "rev (to_bl (- x)) = rbl_succ2 True (map Not (rev (to_bl x)))"
-  by (simp add: twos_complement word_succ_rbl[OF refl]
-                bl_word_not rev_map rbl_succ2_def)
+lemma rbl_word_neg: "rev (to_bl (- x)) = rbl_succ2 True (map Not (rev (to_bl x)))"
+  by (simp add: twos_complement word_succ_rbl[OF refl] bl_word_not rev_map rbl_succ2_def)
 
 lemma rbl_word_cat:
-  "rev (to_bl (word_cat x y :: ('a :: len0) word))
-     = takefill False (len_of TYPE('a)) (rev (to_bl y) @ rev (to_bl x))"
+  "rev (to_bl (word_cat x y :: 'a::len0 word)) =
+    takefill False (len_of TYPE('a)) (rev (to_bl y) @ rev (to_bl x))"
   by (simp add: word_cat_bl word_rev_tf)
 
 lemma rbl_word_slice:
-  "rev (to_bl (slice n w :: ('a :: len0) word))
-     = takefill False (len_of TYPE('a)) (drop n (rev (to_bl w)))"
+  "rev (to_bl (slice n w :: 'a::len0 word)) =
+    takefill False (len_of TYPE('a)) (drop n (rev (to_bl w)))"
   apply (simp add: slice_take word_rev_tf rev_take)
   apply (cases "n < len_of TYPE('b)", simp_all)
   done
 
 lemma rbl_word_ucast:
-  "rev (to_bl (ucast x :: ('a :: len0) word))
-     = takefill False (len_of TYPE('a)) (rev (to_bl x))"
+  "rev (to_bl (ucast x :: 'a::len0 word)) = takefill False (len_of TYPE('a)) (rev (to_bl x))"
   apply (simp add: to_bl_ucast takefill_alt)
   apply (simp add: rev_drop)
-  apply (case_tac "len_of TYPE('a) < len_of TYPE('b)")
+  apply (cases "len_of TYPE('a) < len_of TYPE('b)")
    apply simp_all
   done
 
 lemma rbl_shiftl:
-  "rev (to_bl (w << n)) = takefill False (size w)
-     (replicate n False @ rev (to_bl w))"
+  "rev (to_bl (w << n)) = takefill False (size w) (replicate n False @ rev (to_bl w))"
   by (simp add: bl_shiftl takefill_alt word_size rev_drop)
 
 lemma rbl_shiftr:
-  "rev (to_bl (w >> n)) = takefill False (size w)
-     (drop n (rev (to_bl w)))"
+  "rev (to_bl (w >> n)) = takefill False (size w) (drop n (rev (to_bl w)))"
   by (simp add: shiftr_slice rbl_word_slice word_size)
 
-definition
- "drop_nonempty v n xs
-     = (if n < length xs then drop n xs else [last (v # xs)])"
+definition "drop_nonempty v n xs = (if n < length xs then drop n xs else [last (v # xs)])"
 
 lemma drop_nonempty_simps:
   "drop_nonempty v (Suc n) (x # xs) = drop_nonempty x n xs"
@@ -187,86 +154,69 @@
   "drop_nonempty v n [] = [v]"
   by (simp_all add: drop_nonempty_def)
 
-definition
-  "takefill_last x n xs = takefill (last (x # xs)) n xs"
+definition "takefill_last x n xs = takefill (last (x # xs)) n xs"
 
 lemma takefill_last_simps:
   "takefill_last z (Suc n) (x # xs) = x # takefill_last x n xs"
   "takefill_last z 0 xs = []"
   "takefill_last z n [] = replicate n z"
-  apply (simp_all add: takefill_last_def)
-  apply (simp_all add: takefill_alt)
-  done
+  by (simp_all add: takefill_last_def) (simp_all add: takefill_alt)
 
 lemma rbl_sshiftr:
-  "rev (to_bl (w >>> n)) = 
-     takefill_last False (size w) 
-        (drop_nonempty False n (rev (to_bl w)))"
+  "rev (to_bl (w >>> n)) = takefill_last False (size w) (drop_nonempty False n (rev (to_bl w)))"
   apply (cases "n < size w")
    apply (simp add: bl_sshiftr takefill_last_def word_size
-                    takefill_alt rev_take last_rev
-                    drop_nonempty_def)
+      takefill_alt rev_take last_rev
+      drop_nonempty_def)
   apply (subgoal_tac "(w >>> n) = of_bl (replicate (size w) (msb w))")
    apply (simp add: word_size takefill_last_def takefill_alt
-                    last_rev word_msb_alt word_rev_tf
-                    drop_nonempty_def take_Cons')
+      last_rev word_msb_alt word_rev_tf
+      drop_nonempty_def take_Cons')
    apply (case_tac "len_of TYPE('a)", simp_all)
   apply (rule word_eqI)
   apply (simp add: nth_sshiftr word_size test_bit_of_bl
-                   msb_nth)
+      msb_nth)
   done
 
 lemma nth_word_of_int:
-  "(word_of_int x :: ('a :: len0) word) !! n
-      = (n < len_of TYPE('a) \<and> bin_nth x n)"
+  "(word_of_int x :: 'a::len0 word) !! n = (n < len_of TYPE('a) \<and> bin_nth x n)"
   apply (simp add: test_bit_bl word_size to_bl_of_bin)
   apply (subst conj_cong[OF refl], erule bin_nth_bl)
-  apply (auto)
+  apply auto
   done
 
 lemma nth_scast:
-  "(scast (x :: ('a :: len) word) :: ('b :: len) word) !! n
-     = (n < len_of TYPE('b) \<and>
-          (if n < len_of TYPE('a) - 1 then x !! n
-           else x !! (len_of TYPE('a) - 1)))"
-  by (simp add: scast_def nth_word_of_int nth_sint)
+  "(scast (x :: 'a::len word) :: 'b::len word) !! n =
+    (n < len_of TYPE('b) \<and>
+    (if n < len_of TYPE('a) - 1 then x !! n
+     else x !! (len_of TYPE('a) - 1)))"
+  by (simp add: scast_def nth_sint)
 
 lemma rbl_word_scast:
-  "rev (to_bl (scast x :: ('a :: len) word))
-     = takefill_last False (len_of TYPE('a))
-           (rev (to_bl x))"
+  "rev (to_bl (scast x :: 'a::len word)) = takefill_last False (len_of TYPE('a)) (rev (to_bl x))"
   apply (rule nth_equalityI)
    apply (simp add: word_size takefill_last_def)
   apply (clarsimp simp: nth_scast takefill_last_def
-                        nth_takefill word_size nth_rev to_bl_nth)
+      nth_takefill word_size nth_rev to_bl_nth)
   apply (cases "len_of TYPE('b)")
    apply simp
   apply (clarsimp simp: less_Suc_eq_le linorder_not_less
-                        last_rev word_msb_alt[symmetric]
-                        msb_nth)
+      last_rev word_msb_alt[symmetric]
+      msb_nth)
   done
 
-definition
-  rbl_mul :: "bool list \<Rightarrow> bool list \<Rightarrow> bool list"
-where
- "rbl_mul xs ys = foldr (\<lambda>x sm. rbl_plus False (map (op \<and> x) ys) (False # sm))
-    xs []"
+definition rbl_mul :: "bool list \<Rightarrow> bool list \<Rightarrow> bool list"
+  where "rbl_mul xs ys = foldr (\<lambda>x sm. rbl_plus False (map (op \<and> x) ys) (False # sm)) xs []"
 
 lemma rbl_mul_simps:
-  "rbl_mul (x # xs) ys
-     = rbl_plus False (map (op \<and> x) ys) (False # rbl_mul xs ys)"
+  "rbl_mul (x # xs) ys = rbl_plus False (map (op \<and> x) ys) (False # rbl_mul xs ys)"
   "rbl_mul [] ys = []"
   by (simp_all add: rbl_mul_def)
 
-lemma takefill_le2:
-  "length xs \<le> n \<Longrightarrow>
-   takefill x m (takefill x n xs)
-     = takefill x m xs"
+lemma takefill_le2: "length xs \<le> n \<Longrightarrow> takefill x m (takefill x n xs) = takefill x m xs"
   by (simp add: takefill_alt replicate_add[symmetric])
 
-lemma take_rbl_plus:
-  "\<forall>n b. take n (rbl_plus b xs ys)
-    = rbl_plus b (take n xs) (take n ys)"
+lemma take_rbl_plus: "\<forall>n b. take n (rbl_plus b xs ys) = rbl_plus b (take n xs) (take n ys)"
   apply (simp add: rbl_plus_def take_zip[symmetric])
   apply (rule_tac list="zip xs ys" in list.induct)
    apply simp
@@ -275,52 +225,39 @@
   done
 
 lemma word_rbl_mul_induct:
-  fixes y :: "'a :: len word" shows
-  "length xs \<le> size y
-   \<Longrightarrow> rbl_mul xs (rev (to_bl y))
-     = take (length xs) (rev (to_bl (of_bl (rev xs) * y)))"
+  "length xs \<le> size y \<Longrightarrow>
+    rbl_mul xs (rev (to_bl y)) = take (length xs) (rev (to_bl (of_bl (rev xs) * y)))"
+  for y :: "'a::len word"
 proof (induct xs)
   case Nil
-  show ?case
-    by (simp add: rbl_mul_simps)
+  show ?case by (simp add: rbl_mul_simps)
 next
   case (Cons z zs)
 
-  have rbl_word_plus':
-    "\<And>(x :: 'a word) y.
-      to_bl (x + y) = rev (rbl_plus False (rev (to_bl x)) (rev (to_bl y)))"
+  have rbl_word_plus': "to_bl (x + y) = rev (rbl_plus False (rev (to_bl x)) (rev (to_bl y)))"
+    for x y :: "'a word"
     by (simp add: rbl_word_plus[symmetric])
-  
+
   have mult_bit: "to_bl (of_bl [z] * y) = map (op \<and> z) (to_bl y)"
-    apply (cases z)
-     apply (simp cong: map_cong)
-    apply (simp add: map_replicate_const cong: map_cong)
-    done
- 
-  have shiftl: "\<And>xs. of_bl xs * 2 * y = (of_bl xs * y) << 1"
+    by (cases z) (simp cong: map_cong, simp add: map_replicate_const cong: map_cong)
+
+  have shiftl: "of_bl xs * 2 * y = (of_bl xs * y) << 1" for xs
     by (simp add: shiftl_t2n)
 
-  have zip_take_triv: "\<And>xs ys n. n = length ys
-      \<Longrightarrow> zip (take n xs) ys = zip xs ys"
-    by (rule nth_equalityI, simp_all)
+  have zip_take_triv: "\<And>xs ys n. n = length ys \<Longrightarrow> zip (take n xs) ys = zip xs ys"
+    by (rule nth_equalityI) simp_all
 
-  show ?case
-    using Cons
+  from Cons show ?case
     apply (simp add: trans [OF of_bl_append add.commute]
-                     rbl_mul_simps rbl_word_plus'
-                     Cons.hyps distrib_right mult_bit
-                     shiftl rbl_shiftl)
-    apply (simp add: takefill_alt word_size rev_map take_rbl_plus
-                     min_def)
+        rbl_mul_simps rbl_word_plus' distrib_right mult_bit shiftl rbl_shiftl)
+    apply (simp add: takefill_alt word_size rev_map take_rbl_plus min_def)
     apply (simp add: rbl_plus_def zip_take_triv)
     done
 qed
 
-lemma rbl_word_mul:
-  fixes x :: "'a :: len word"
-  shows "rev (to_bl (x * y)) = rbl_mul (rev (to_bl x)) (rev (to_bl y))"
-  using word_rbl_mul_induct[where xs="rev (to_bl x)" and y=y]
-  by (simp add: word_size)
+lemma rbl_word_mul: "rev (to_bl (x * y)) = rbl_mul (rev (to_bl x)) (rev (to_bl y))"
+  for x :: "'a::len word"
+  using word_rbl_mul_induct[where xs="rev (to_bl x)" and y=y] by (simp add: word_size)
 
 text \<open>Breaking up inequalities into bitlist properties.\<close>
 
@@ -333,9 +270,8 @@
 
 lemma rev_bl_order_simps:
   "rev_bl_order F [] [] = F"
-  "rev_bl_order F (x # xs) (y # ys)
-     = rev_bl_order ((y \<and> \<not> x) \<or> ((y \<or> \<not> x) \<and> F)) xs ys"
-  apply (simp_all add: rev_bl_order_def)
+  "rev_bl_order F (x # xs) (y # ys) = rev_bl_order ((y \<and> \<not> x) \<or> ((y \<or> \<not> x) \<and> F)) xs ys"
+   apply (simp_all add: rev_bl_order_def)
   apply (rule conj_cong[OF refl])
   apply (cases "xs = ys")
    apply (simp add: nth_Cons')
@@ -350,39 +286,30 @@
 
 lemma rev_bl_order_rev_simp:
   "length xs = length ys \<Longrightarrow>
-   rev_bl_order F (xs @ [x]) (ys @ [y])
-     = ((y \<and> \<not> x) \<or> ((y \<or> \<not> x) \<and> rev_bl_order F xs ys))"
-  apply (induct arbitrary: F rule: list_induct2)
-   apply (auto simp add: rev_bl_order_simps)
-  done
+   rev_bl_order F (xs @ [x]) (ys @ [y]) = ((y \<and> \<not> x) \<or> ((y \<or> \<not> x) \<and> rev_bl_order F xs ys))"
+  by (induct arbitrary: F rule: list_induct2) (auto simp: rev_bl_order_simps)
 
 lemma rev_bl_order_bl_to_bin:
-  "length xs = length ys
-     \<Longrightarrow> rev_bl_order True xs ys
-            = (bl_to_bin (rev xs) \<le> bl_to_bin (rev ys))
-       \<and> rev_bl_order False xs ys
-            = (bl_to_bin (rev xs) < bl_to_bin (rev ys))"
+  "length xs = length ys \<Longrightarrow>
+    rev_bl_order True xs ys = (bl_to_bin (rev xs) \<le> bl_to_bin (rev ys)) \<and>
+    rev_bl_order False xs ys = (bl_to_bin (rev xs) < bl_to_bin (rev ys))"
   apply (induct xs ys rule: list_induct2)
    apply (simp_all add: rev_bl_order_simps bl_to_bin_app_cat)
   apply (auto simp add: bl_to_bin_def Bit_B0 Bit_B1 add1_zle_eq Bit_def)
   done
 
-lemma word_le_rbl:
-  fixes x :: "('a :: len0) word"
-  shows "(x \<le> y) = rev_bl_order True (rev (to_bl x)) (rev (to_bl y))"
+lemma word_le_rbl: "x \<le> y \<longleftrightarrow> rev_bl_order True (rev (to_bl x)) (rev (to_bl y))"
+  for x y :: "'a::len0 word"
   by (simp add: rev_bl_order_bl_to_bin word_le_def)
 
-lemma word_less_rbl:
-  fixes x :: "('a :: len0) word"
-  shows "(x < y) = rev_bl_order False (rev (to_bl x)) (rev (to_bl y))"
+lemma word_less_rbl: "x < y \<longleftrightarrow> rev_bl_order False (rev (to_bl x)) (rev (to_bl y))"
+  for x y :: "'a::len0 word"
   by (simp add: word_less_alt rev_bl_order_bl_to_bin)
 
-lemma word_sint_msb_eq:
-  "sint x = uint x - (if msb x then 2 ^ size x else 0)"
+lemma word_sint_msb_eq: "sint x = uint x - (if msb x then 2 ^ size x else 0)"
   apply (cases "msb x")
    apply (rule word_sint.Abs_eqD[where 'a='a], simp_all)
-    apply (simp add: word_size wi_hom_syms
-                     word_of_int_2p_len)
+    apply (simp add: word_size wi_hom_syms word_of_int_2p_len)
    apply (simp add: sints_num word_size)
    apply (rule conjI)
     apply (simp add: le_diff_eq')
@@ -398,11 +325,8 @@
   apply simp
   done
 
-lemma word_sle_msb_le:
-  "(x <=s y) = ((msb y --> msb x) \<and> 
-                  ((msb x \<and> \<not> msb y) \<or> (x <= y)))"
-  apply (simp add: word_sle_def word_sint_msb_eq word_size
-                   word_le_def)
+lemma word_sle_msb_le: "x <=s y \<longleftrightarrow> (msb y \<longrightarrow> msb x) \<and> ((msb x \<and> \<not> msb y) \<or> x \<le> y)"
+  apply (simp add: word_sle_def word_sint_msb_eq word_size word_le_def)
   apply safe
    apply (rule order_trans[OF _ uint_ge_0])
    apply (simp add: order_less_imp_le)
@@ -411,13 +335,10 @@
   apply simp
   done
 
-lemma word_sless_msb_less:
-  "(x <s y) = ((msb y --> msb x) \<and> 
-                  ((msb x \<and> \<not> msb y) \<or> (x < y)))"
+lemma word_sless_msb_less: "x <s y \<longleftrightarrow> (msb y \<longrightarrow> msb x) \<and> ((msb x \<and> \<not> msb y) \<or> x < y)"
   by (auto simp add: word_sless_def word_sle_msb_le)
 
-definition
-  "map_last f xs = (if xs = [] then [] else butlast xs @ [f (last xs)])"
+definition "map_last f xs = (if xs = [] then [] else butlast xs @ [f (last xs)])"
 
 lemma map_last_simps:
   "map_last f [] = []"
@@ -426,8 +347,7 @@
   by (simp_all add: map_last_def)
 
 lemma word_sle_rbl:
-  "(x <=s y) = rev_bl_order True (map_last Not (rev (to_bl x)))
-     (map_last Not (rev (to_bl y)))"
+  "x <=s y \<longleftrightarrow> rev_bl_order True (map_last Not (rev (to_bl x))) (map_last Not (rev (to_bl y)))"
   using word_msb_alt[where w=x] word_msb_alt[where w=y]
   apply (simp add: word_sle_msb_le word_le_rbl)
   apply (subgoal_tac "length (to_bl x) = length (to_bl y)")
@@ -438,8 +358,7 @@
   done
 
 lemma word_sless_rbl:
-  "(x <s y) = rev_bl_order False (map_last Not (rev (to_bl x)))
-     (map_last Not (rev (to_bl y)))"
+  "x <s y \<longleftrightarrow> rev_bl_order False (map_last Not (rev (to_bl x))) (map_last Not (rev (to_bl y)))"
   using word_msb_alt[where w=x] word_msb_alt[where w=y]
   apply (simp add: word_sless_msb_less word_less_rbl)
   apply (subgoal_tac "length (to_bl x) = length (to_bl y)")
@@ -450,51 +369,45 @@
   done
 
 text \<open>Lemmas for unpacking rev (to_bl n) for numerals n and also
-for irreducible values and expressions.\<close>
+  for irreducible values and expressions.\<close>
 
 lemma rev_bin_to_bl_simps:
   "rev (bin_to_bl 0 x) = []"
-  "rev (bin_to_bl (Suc n) (numeral (num.Bit0 nm)))
-    = False # rev (bin_to_bl n (numeral nm))"
-  "rev (bin_to_bl (Suc n) (numeral (num.Bit1 nm)))
-    = True # rev (bin_to_bl n (numeral nm))"
-  "rev (bin_to_bl (Suc n) (numeral (num.One)))
-    = True # replicate n False"
-  "rev (bin_to_bl (Suc n) (- numeral (num.Bit0 nm)))
-    = False # rev (bin_to_bl n (- numeral nm))"
-  "rev (bin_to_bl (Suc n) (- numeral (num.Bit1 nm)))
-    = True # rev (bin_to_bl n (- numeral (nm + num.One)))"
-  "rev (bin_to_bl (Suc n) (- numeral (num.One)))
-    = True # replicate n True"
-  "rev (bin_to_bl (Suc n) (- numeral (num.Bit0 nm + num.One)))
-    = True # rev (bin_to_bl n (- numeral (nm + num.One)))"
-  "rev (bin_to_bl (Suc n) (- numeral (num.Bit1 nm + num.One)))
-    = False # rev (bin_to_bl n (- numeral (nm + num.One)))"
-  "rev (bin_to_bl (Suc n) (- numeral (num.One + num.One)))
-    = False # rev (bin_to_bl n (- numeral num.One))"
-  apply (simp_all add: bin_to_bl_def)
+  "rev (bin_to_bl (Suc n) (numeral (num.Bit0 nm))) = False # rev (bin_to_bl n (numeral nm))"
+  "rev (bin_to_bl (Suc n) (numeral (num.Bit1 nm))) = True # rev (bin_to_bl n (numeral nm))"
+  "rev (bin_to_bl (Suc n) (numeral (num.One))) = True # replicate n False"
+  "rev (bin_to_bl (Suc n) (- numeral (num.Bit0 nm))) = False # rev (bin_to_bl n (- numeral nm))"
+  "rev (bin_to_bl (Suc n) (- numeral (num.Bit1 nm))) =
+    True # rev (bin_to_bl n (- numeral (nm + num.One)))"
+  "rev (bin_to_bl (Suc n) (- numeral (num.One))) = True # replicate n True"
+  "rev (bin_to_bl (Suc n) (- numeral (num.Bit0 nm + num.One))) =
+    True # rev (bin_to_bl n (- numeral (nm + num.One)))"
+  "rev (bin_to_bl (Suc n) (- numeral (num.Bit1 nm + num.One))) =
+    False # rev (bin_to_bl n (- numeral (nm + num.One)))"
+  "rev (bin_to_bl (Suc n) (- numeral (num.One + num.One))) =
+    False # rev (bin_to_bl n (- numeral num.One))"
+  apply simp_all
   apply (simp_all only: bin_to_bl_aux_alt)
   apply (simp_all)
   apply (simp_all add: bin_to_bl_zero_aux bin_to_bl_minus1_aux)
   done
 
-lemma to_bl_upt:
-  "to_bl x = rev (map (op !! x) [0 ..< size x])"
+lemma to_bl_upt: "to_bl x = rev (map (op !! x) [0 ..< size x])"
   apply (rule nth_equalityI)
    apply (simp add: word_size)
-  apply (clarsimp simp: to_bl_nth word_size nth_rev)
+  apply (auto simp: to_bl_nth word_size nth_rev)
   done
 
-lemma rev_to_bl_upt:
-  "rev (to_bl x) = map (op !! x) [0 ..< size x]"
+lemma rev_to_bl_upt: "rev (to_bl x) = map (op !! x) [0 ..< size x]"
   by (simp add: to_bl_upt)
 
 lemma upt_eq_list_intros:
-  "j <= i \<Longrightarrow> [i ..< j] = []"
-  "\<lbrakk> i = x; x < j; [x + 1 ..< j] = xs \<rbrakk> \<Longrightarrow> [i ..< j] = (x # xs)"
-  by (simp_all add: upt_eq_Nil_conv upt_eq_Cons_conv)
+  "j \<le> i \<Longrightarrow> [i ..< j] = []"
+  "i = x \<Longrightarrow> x < j \<Longrightarrow> [x + 1 ..< j] = xs \<Longrightarrow> [i ..< j] = (x # xs)"
+  by (simp_all add: upt_eq_Cons_conv)
 
-text \<open>Tactic definition\<close>
+
+subsection \<open>Tactic definition\<close>
 
 ML \<open>
 structure Word_Bitwise_Tac =
@@ -517,7 +430,7 @@
                      |> Thm.apply @{cterm Trueprop};
       in
         try (fn () =>
-          Goal.prove_internal ctxt [] prop 
+          Goal.prove_internal ctxt [] prop
             (K (REPEAT_DETERM (resolve_tac ctxt @{thms upt_eq_list_intros} 1
                 ORELSE simp_tac (put_simpset word_ss ctxt) 1))) |> mk_meta_eq) ()
       end
@@ -616,7 +529,6 @@
   end;
 
 end
-
 \<close>
 
 method_setup word_bitwise =
diff -r 4ff2ba82d668 -r db7c97cdcfe7 src/HOL/Word/Word_Miscellaneous.thy
--- a/src/HOL/Word/Word_Miscellaneous.thy	Mon Apr 03 22:18:56 2017 +0200
+++ b/src/HOL/Word/Word_Miscellaneous.thy	Mon Apr 03 23:12:44 2017 +0200
@@ -1,34 +1,27 @@
-(*  Title:      HOL/Word/Word_Miscellaneous.thy
-    Author:     Miscellaneous
-*)
+(*  Title:      HOL/Word/Word_Miscellaneous.thy  *)
 
 section \<open>Miscellaneous lemmas, of at least doubtful value\<close>
 
 theory Word_Miscellaneous
-imports Main "~~/src/HOL/Library/Bit" Misc_Numeric
+  imports "~~/src/HOL/Library/Bit" Misc_Numeric
 begin
 
-lemma power_minus_simp:
-  "0 < n \<Longrightarrow> a ^ n = a * a ^ (n - 1)"
+lemma power_minus_simp: "0 < n \<Longrightarrow> a ^ n = a * a ^ (n - 1)"
   by (auto dest: gr0_implies_Suc)
 
-lemma funpow_minus_simp:
-  "0 < n \<Longrightarrow> f ^^ n = f \<circ> f ^^ (n - 1)"
+lemma funpow_minus_simp: "0 < n \<Longrightarrow> f ^^ n = f \<circ> f ^^ (n - 1)"
   by (auto dest: gr0_implies_Suc)
 
-lemma power_numeral:
-  "a ^ numeral k = a * a ^ (pred_numeral k)"
+lemma power_numeral: "a ^ numeral k = a * a ^ (pred_numeral k)"
   by (simp add: numeral_eq_Suc)
 
-lemma funpow_numeral [simp]:
-  "f ^^ numeral k = f \<circ> f ^^ (pred_numeral k)"
+lemma funpow_numeral [simp]: "f ^^ numeral k = f \<circ> f ^^ (pred_numeral k)"
   by (simp add: numeral_eq_Suc)
 
-lemma replicate_numeral [simp]:
-  "replicate (numeral k) x = x # replicate (pred_numeral k) x"
+lemma replicate_numeral [simp]: "replicate (numeral k) x = x # replicate (pred_numeral k) x"
   by (simp add: numeral_eq_Suc)
 
-lemma rco_alt: "(f o g) ^^ n o f = f o (g o f) ^^ n"
+lemma rco_alt: "(f \<circ> g) ^^ n \<circ> f = f \<circ> (g \<circ> f) ^^ n"
   apply (rule ext)
   apply (induct n)
    apply (simp_all add: o_def)
@@ -37,7 +30,8 @@
 lemma list_exhaust_size_gt0:
   assumes y: "\<And>a list. y = a # list \<Longrightarrow> P"
   shows "0 < length y \<Longrightarrow> P"
-  apply (cases y, simp)
+  apply (cases y)
+   apply simp
   apply (rule y)
   apply fastforce
   done
@@ -46,22 +40,24 @@
   assumes y: "y = [] \<Longrightarrow> P"
   shows "length y = 0 \<Longrightarrow> P"
   apply (cases y)
-   apply (rule y, simp)
+   apply (rule y)
+   apply simp
   apply simp
   done
 
-lemma size_Cons_lem_eq:
-  "y = xa # list ==> size y = Suc k ==> size list = k"
+lemma size_Cons_lem_eq: "y = xa # list \<Longrightarrow> size y = Suc k \<Longrightarrow> size list = k"
   by auto
 
 lemmas ls_splits = prod.split prod.split_asm if_split_asm
 
-lemma not_B1_is_B0: "y \<noteq> (1::bit) \<Longrightarrow> y = (0::bit)"
+lemma not_B1_is_B0: "y \<noteq> 1 \<Longrightarrow> y = 0"
+  for y :: bit
   by (cases y) auto
 
-lemma B1_ass_B0: 
-  assumes y: "y = (0::bit) \<Longrightarrow> y = (1::bit)"
-  shows "y = (1::bit)"
+lemma B1_ass_B0:
+  fixes y :: bit
+  assumes y: "y = 0 \<Longrightarrow> y = 1"
+  shows "y = 1"
   apply (rule classical)
   apply (drule not_B1_is_B0)
   apply (erule y)
@@ -72,7 +68,7 @@
 
 lemmas s2n_ths = n2s_ths [symmetric]
 
-lemma and_len: "xs = ys ==> xs = ys & length xs = length ys"
+lemma and_len: "xs = ys \<Longrightarrow> xs = ys \<and> length xs = length ys"
   by auto
 
 lemma size_if: "size (if p then xs else ys) = (if p then size xs else size ys)"
@@ -84,20 +80,19 @@
 lemma hd_if: "hd (if p then xs else ys) = (if p then hd xs else hd ys)"
   by auto
 
-lemma if_Not_x: "(if p then ~ x else x) = (p = (~ x))"
+lemma if_Not_x: "(if p then \<not> x else x) = (p = (\<not> x))"
   by auto
 
-lemma if_x_Not: "(if p then x else ~ x) = (p = x)"
+lemma if_x_Not: "(if p then x else \<not> x) = (p = x)"
   by auto
 
-lemma if_same_and: "(If p x y & If p u v) = (if p then x & u else y & v)"
+lemma if_same_and: "(If p x y \<and> If p u v) = (if p then x \<and> u else y \<and> v)"
   by auto
 
-lemma if_same_eq: "(If p x y  = (If p u v)) = (if p then x = (u) else y = (v))"
+lemma if_same_eq: "(If p x y  = (If p u v)) = (if p then x = u else y = v)"
   by auto
 
-lemma if_same_eq_not:
-  "(If p x y  = (~ If p u v)) = (if p then x = (~u) else y = (~v))"
+lemma if_same_eq_not: "(If p x y = (\<not> If p u v)) = (if p then x = (\<not> u) else y = (\<not> v))"
   by auto
 
 (* note - if_Cons can cause blowup in the size, if p is complex,
@@ -105,25 +100,28 @@
 lemma if_Cons: "(if p then x # xs else y # ys) = If p x y # If p xs ys"
   by auto
 
-lemma if_single:
-  "(if xc then [xab] else [an]) = [if xc then xab else an]"
+lemma if_single: "(if xc then [xab] else [an]) = [if xc then xab else an]"
   by auto
 
 lemma if_bool_simps:
-  "If p True y = (p | y) & If p False y = (~p & y) & 
-    If p y True = (p --> y) & If p y False = (p & y)"
+  "If p True y = (p \<or> y) \<and> If p False y = (\<not> p \<and> y) \<and>
+    If p y True = (p \<longrightarrow> y) \<and> If p y False = (p \<and> y)"
   by auto
 
-lemmas if_simps = if_x_Not if_Not_x if_cancel if_True if_False if_bool_simps
+lemmas if_simps =
+  if_x_Not if_Not_x if_cancel if_True if_False if_bool_simps
 
 lemmas seqr = eq_reflection [where x = "size w"] for w (* FIXME: delete *)
 
-lemma the_elemI: "y = {x} ==> the_elem y = x" 
+lemma the_elemI: "y = {x} \<Longrightarrow> the_elem y = x"
   by simp
 
-lemma nonemptyE: "S ~= {} ==> (!!x. x : S ==> R) ==> R" by auto
+lemma nonemptyE: "S \<noteq> {} \<Longrightarrow> (\<And>x. x \<in> S \<Longrightarrow> R) \<Longrightarrow> R"
+  by auto
 
-lemma gt_or_eq_0: "0 < y \<or> 0 = (y::nat)" by arith 
+lemma gt_or_eq_0: "0 < y \<or> 0 = y"
+  for y :: nat
+  by arith
 
 lemmas xtr1 = xtrans(1)
 lemmas xtr2 = xtrans(2)
@@ -137,63 +135,76 @@
 lemmas nat_simps = diff_add_inverse2 diff_add_inverse
 lemmas nat_iffs = le_add1 le_add2
 
-lemma sum_imp_diff: "j = k + i ==> j - i = (k :: nat)" by arith
+lemma sum_imp_diff: "j = k + i \<Longrightarrow> j - i = k"
+  for k :: nat
+  by arith
 
 lemmas pos_mod_sign2 = zless2 [THEN pos_mod_sign [where b = "2::int"]]
 lemmas pos_mod_bound2 = zless2 [THEN pos_mod_bound [where b = "2::int"]]
 
-lemma nmod2: "n mod (2::int) = 0 | n mod 2 = 1"
+lemma nmod2: "n mod 2 = 0 \<or> n mod 2 = 1"
+  for n :: int
   by arith
 
 lemmas eme1p = emep1 [simplified add.commute]
 
-lemma le_diff_eq': "(a \<le> c - b) = (b + a \<le> (c::int))" by arith
+lemma le_diff_eq': "a \<le> c - b \<longleftrightarrow> b + a \<le> c"
+  for a b c :: int
+  by arith
 
-lemma less_diff_eq': "(a < c - b) = (b + a < (c::int))" by arith
+lemma less_diff_eq': "a < c - b \<longleftrightarrow> b + a < c"
+  for a b c :: int
+  by arith
 
-lemma diff_less_eq': "(a - b < c) = (a < b + (c::int))" by arith
+lemma diff_less_eq': "a - b < c \<longleftrightarrow> a < b + c"
+  for a b c :: int
+  by arith
 
 lemmas m1mod22k = mult_pos_pos [OF zless2 zless2p, THEN zmod_minus1]
 
-lemma z1pdiv2:
-  "(2 * b + 1) div 2 = (b::int)" by arith
+lemma z1pdiv2: "(2 * b + 1) div 2 = b"
+  for b :: int
+  by arith
 
 lemmas zdiv_le_dividend = xtr3 [OF div_by_1 [symmetric] zdiv_mono2,
   simplified int_one_le_iff_zero_less, simplified]
-  
-lemma axxbyy:
-  "a + m + m = b + n + n ==> (a = 0 | a = 1) ==> (b = 0 | b = 1) ==>  
-   a = b & m = (n :: int)" by arith
 
-lemma axxmod2:
-  "(1 + x + x) mod 2 = (1 :: int) & (0 + x + x) mod 2 = (0 :: int)" by arith
+lemma axxbyy: "a + m + m = b + n + n \<Longrightarrow> a = 0 \<or> a = 1 \<Longrightarrow> b = 0 \<or> b = 1 \<Longrightarrow> a = b \<and> m = n"
+  for a b m n :: int
+  by arith
+
+lemma axxmod2: "(1 + x + x) mod 2 = 1 \<and> (0 + x + x) mod 2 = 0"
+  for x :: int
+  by arith
 
-lemma axxdiv2:
-  "(1 + x + x) div 2 = (x :: int) & (0 + x + x) div 2 = (x :: int)"  by arith
+lemma axxdiv2: "(1 + x + x) div 2 = x \<and> (0 + x + x) div 2 = x"
+  for x :: int
+  by arith
 
-lemmas iszero_minus = trans [THEN trans,
-  OF iszero_def neg_equal_0_iff_equal iszero_def [symmetric]]
+lemmas iszero_minus =
+  trans [THEN trans, OF iszero_def neg_equal_0_iff_equal iszero_def [symmetric]]
 
-lemmas zadd_diff_inverse = trans [OF diff_add_cancel [symmetric] add.commute]
+lemmas zadd_diff_inverse =
+  trans [OF diff_add_cancel [symmetric] add.commute]
 
-lemmas add_diff_cancel2 = add.commute [THEN diff_eq_eq [THEN iffD2]]
+lemmas add_diff_cancel2 =
+  add.commute [THEN diff_eq_eq [THEN iffD2]]
 
 lemmas rdmods [symmetric] = mod_minus_eq
   mod_diff_left_eq mod_diff_right_eq mod_add_left_eq
   mod_add_right_eq mod_mult_right_eq mod_mult_left_eq
 
-lemma mod_plus_right:
-  "((a + x) mod m = (b + x) mod m) = (a mod m = b mod (m :: nat))"
-  apply (induct x)
-   apply (simp_all add: mod_Suc)
-  apply arith
-  done
+lemma mod_plus_right: "(a + x) mod m = (b + x) mod m \<longleftrightarrow> a mod m = b mod m"
+  for a b m x :: nat
+  by (induct x) (simp_all add: mod_Suc, arith)
 
-lemma nat_minus_mod: "(n - n mod m) mod m = (0 :: nat)"
-  by (induct n) (simp_all add : mod_Suc)
+lemma nat_minus_mod: "(n - n mod m) mod m = 0"
+  for m n :: nat
+  by (induct n) (simp_all add: mod_Suc)
 
-lemmas nat_minus_mod_plus_right = trans [OF nat_minus_mod mod_0 [symmetric],
-  THEN mod_plus_right [THEN iffD2], simplified]
+lemmas nat_minus_mod_plus_right =
+  trans [OF nat_minus_mod mod_0 [symmetric],
+    THEN mod_plus_right [THEN iffD2], simplified]
 
 lemmas push_mods' = mod_add_eq
   mod_mult_eq mod_diff_eq
@@ -202,23 +213,22 @@
 lemmas push_mods = push_mods' [THEN eq_reflection]
 lemmas pull_mods = push_mods [symmetric] rdmods [THEN eq_reflection]
 
-lemma nat_mod_eq:
-  "!!b. b < n ==> a mod n = b mod n ==> a mod n = (b :: nat)" 
+lemma nat_mod_eq: "b < n \<Longrightarrow> a mod n = b mod n \<Longrightarrow> a mod n = b"
+  for a b n :: nat
   by (induct a) auto
 
 lemmas nat_mod_eq' = refl [THEN [2] nat_mod_eq]
 
-lemma nat_mod_lem: 
-  "(0 :: nat) < n ==> b < n = (b mod n = b)"
+lemma nat_mod_lem: "0 < n \<Longrightarrow> b < n \<longleftrightarrow> b mod n = b"
+  for b n :: nat
   apply safe
    apply (erule nat_mod_eq')
   apply (erule subst)
   apply (erule mod_less_divisor)
   done
 
-lemma mod_nat_add: 
-  "(x :: nat) < z ==> y < z ==> 
-   (x + y) mod z = (if x + y < z then x + y else x + y - z)"
+lemma mod_nat_add: "x < z \<Longrightarrow> y < z \<Longrightarrow> (x + y) mod z = (if x + y < z then x + y else x + y - z)"
+  for x y z :: nat
   apply (rule nat_mod_eq)
    apply auto
   apply (rule trans)
@@ -228,42 +238,46 @@
   apply arith
   done
 
-lemma mod_nat_sub: 
-  "(x :: nat) < z ==> (x - y) mod z = x - y"
+lemma mod_nat_sub: "x < z \<Longrightarrow> (x - y) mod z = x - y"
+  for x y :: nat
   by (rule nat_mod_eq') arith
 
-lemma int_mod_eq:
-  "(0 :: int) <= b ==> b < n ==> a mod n = b mod n ==> a mod n = b"
+lemma int_mod_eq: "0 \<le> b \<Longrightarrow> b < n \<Longrightarrow> a mod n = b mod n \<Longrightarrow> a mod n = b"
+  for a b n :: int
   by (metis mod_pos_pos_trivial)
 
 lemmas int_mod_eq' = mod_pos_pos_trivial (* FIXME delete *)
 
-lemma int_mod_le: "(0::int) <= a ==> a mod n <= a"
+lemma int_mod_le: "0 \<le> a \<Longrightarrow> a mod n \<le> a"
+  for a :: int
   by (fact Divides.semiring_numeral_div_class.mod_less_eq_dividend) (* FIXME: delete *)
 
 lemma mod_add_if_z:
-  "(x :: int) < z ==> y < z ==> 0 <= y ==> 0 <= x ==> 0 <= z ==> 
-   (x + y) mod z = (if x + y < z then x + y else x + y - z)"
+  "x < z \<Longrightarrow> y < z \<Longrightarrow> 0 \<le> y \<Longrightarrow> 0 \<le> x \<Longrightarrow> 0 \<le> z \<Longrightarrow>
+    (x + y) mod z = (if x + y < z then x + y else x + y - z)"
+  for x y z :: int
   by (auto intro: int_mod_eq)
 
 lemma mod_sub_if_z:
-  "(x :: int) < z ==> y < z ==> 0 <= y ==> 0 <= x ==> 0 <= z ==> 
-   (x - y) mod z = (if y <= x then x - y else x - y + z)"
+  "x < z \<Longrightarrow> y < z \<Longrightarrow> 0 \<le> y \<Longrightarrow> 0 \<le> x \<Longrightarrow> 0 \<le> z \<Longrightarrow>
+    (x - y) mod z = (if y \<le> x then x - y else x - y + z)"
+  for x y z :: int
   by (auto intro: int_mod_eq)
 
 lemmas zmde = mult_div_mod_eq [symmetric, THEN diff_eq_eq [THEN iffD2], symmetric]
 lemmas mcl = mult_cancel_left [THEN iffD1, THEN make_pos_rule]
 
 (* already have this for naturals, div_mult_self1/2, but not for ints *)
-lemma zdiv_mult_self: "m ~= (0 :: int) ==> (a + m * n) div m = a div m + n"
+lemma zdiv_mult_self: "m \<noteq> 0 \<Longrightarrow> (a + m * n) div m = a div m + n"
+  for a m n :: int
   apply (rule mcl)
    prefer 2
    apply (erule asm_rl)
   apply (simp add: zmde ring_distribs)
   done
 
-lemma mod_power_lem:
-  "a > 1 ==> a ^ n mod a ^ m = (if m <= n then 0 else (a :: int) ^ n)"
+lemma mod_power_lem: "a > 1 \<Longrightarrow> a ^ n mod a ^ m = (if m \<le> n then 0 else a ^ n)"
+  for a :: int
   apply clarsimp
   apply safe
    apply (simp add: dvd_eq_mod_eq_0 [symmetric])
@@ -275,15 +289,19 @@
    apply auto
   done
 
-lemma pl_pl_rels: 
-  "a + b = c + d ==> 
-   a >= c & b <= d | a <= c & b >= (d :: nat)" by arith
+lemma pl_pl_rels: "a + b = c + d \<Longrightarrow> a \<ge> c \<and> b \<le> d \<or> a \<le> c \<and> b \<ge> d"
+  for a b c d :: nat
+  by arith
 
 lemmas pl_pl_rels' = add.commute [THEN [2] trans, THEN pl_pl_rels]
 
-lemma minus_eq: "(m - k = m) = (k = 0 | m = (0 :: nat))"  by arith
+lemma minus_eq: "m - k = m \<longleftrightarrow> k = 0 \<or> m = 0"
+  for k m :: nat
+  by arith
 
-lemma pl_pl_mm: "(a :: nat) + b = c + d ==> a - c = d - b"  by arith
+lemma pl_pl_mm: "a + b = c + d \<Longrightarrow> a - c = d - b"
+  for a b c d :: nat
+  by arith
 
 lemmas pl_pl_mm' = add.commute [THEN [2] trans, THEN pl_pl_mm]
 
@@ -291,33 +309,37 @@
 lemmas dtle = xtr3 [OF dme [symmetric] le_add1]
 lemmas th2 = order_trans [OF order_refl [THEN [2] mult_le_mono] dtle]
 
-lemma td_gal: 
-  "0 < c ==> (a >= b * c) = (a div c >= (b :: nat))"
+lemma td_gal: "0 < c \<Longrightarrow> a \<ge> b * c \<longleftrightarrow> a div c \<ge> b"
+  for a b c :: nat
   apply safe
    apply (erule (1) xtr4 [OF div_le_mono div_mult_self_is_m])
   apply (erule th2)
   done
-  
+
 lemmas td_gal_lt = td_gal [simplified not_less [symmetric], simplified]
 
-lemma div_mult_le: "(a :: nat) div b * b <= a"
+lemma div_mult_le: "a div b * b \<le> a"
+  for a b :: nat
   by (fact dtle)
 
 lemmas sdl = split_div_lemma [THEN iffD1, symmetric]
 
-lemma given_quot: "f > (0 :: nat) ==> (f * l + (f - 1)) div f = l"
+lemma given_quot: "f > 0 \<Longrightarrow> (f * l + (f - 1)) div f = l"
+  for f l :: nat
   by (rule sdl, assumption) (simp (no_asm))
 
-lemma given_quot_alt: "f > (0 :: nat) ==> (l * f + f - Suc 0) div f = l"
+lemma given_quot_alt: "f > 0 \<Longrightarrow> (l * f + f - Suc 0) div f = l"
+  for f l :: nat
   apply (frule given_quot)
   apply (rule trans)
    prefer 2
    apply (erule asm_rl)
-  apply (rule_tac f="%n. n div f" in arg_cong)
+  apply (rule_tac f="\<lambda>n. n div f" in arg_cong)
   apply (simp add : ac_simps)
   done
-    
-lemma diff_mod_le: "(a::nat) < d ==> b dvd d ==> a - a mod b <= d - b"
+
+lemma diff_mod_le: "a < d \<Longrightarrow> b dvd d \<Longrightarrow> a - a mod b \<le> d - b"
+  for a b d :: nat
   apply (unfold dvd_def)
   apply clarify
   apply (case_tac k)
@@ -332,57 +354,56 @@
       apply auto
   done
 
-lemma less_le_mult':
-  "w * c < b * c ==> 0 \<le> c ==> (w + 1) * c \<le> b * (c::int)"
+lemma less_le_mult': "w * c < b * c \<Longrightarrow> 0 \<le> c \<Longrightarrow> (w + 1) * c \<le> b * c"
+  for b c w :: int
   apply (rule mult_right_mono)
    apply (rule zless_imp_add1_zle)
    apply (erule (1) mult_right_less_imp_less)
   apply assumption
   done
 
-lemma less_le_mult:
-  "w * c < b * c \<Longrightarrow> 0 \<le> c \<Longrightarrow> w * c + c \<le> b * (c::int)"
+lemma less_le_mult: "w * c < b * c \<Longrightarrow> 0 \<le> c \<Longrightarrow> w * c + c \<le> b * c"
+  for b c w :: int
   using less_le_mult' [of w c b] by (simp add: algebra_simps)
 
-lemmas less_le_mult_minus = iffD2 [OF le_diff_eq less_le_mult, 
+lemmas less_le_mult_minus = iffD2 [OF le_diff_eq less_le_mult,
   simplified left_diff_distrib]
 
-lemma gen_minus: "0 < n ==> f n = f (Suc (n - 1))"
+lemma gen_minus: "0 < n \<Longrightarrow> f n = f (Suc (n - 1))"
   by auto
 
-lemma mpl_lem: "j <= (i :: nat) ==> k < j ==> i - j + k < i" by arith
+lemma mpl_lem: "j \<le> i \<Longrightarrow> k < j \<Longrightarrow> i - j + k < i"
+  for i j k :: nat
+  by arith
 
-lemma nonneg_mod_div:
-  "0 <= a ==> 0 <= b ==> 0 <= (a mod b :: int) & 0 <= a div b"
-  apply (cases "b = 0", clarsimp)
-  apply (auto intro: pos_imp_zdiv_nonneg_iff [THEN iffD2])
-  done
+lemma nonneg_mod_div: "0 \<le> a \<Longrightarrow> 0 \<le> b \<Longrightarrow> 0 \<le> (a mod b) \<and> 0 \<le> a div b"
+  for a b :: int
+  by (cases "b = 0") (auto intro: pos_imp_zdiv_nonneg_iff [THEN iffD2])
 
 declare iszero_0 [intro]
 
-lemma min_pm [simp]:
-  "min a b + (a - b) = (a :: nat)"
+lemma min_pm [simp]: "min a b + (a - b) = a"
+  for a b :: nat
   by arith
-  
-lemma min_pm1 [simp]:
-  "a - b + min a b = (a :: nat)"
+
+lemma min_pm1 [simp]: "a - b + min a b = a"
+  for a b :: nat
   by arith
 
-lemma rev_min_pm [simp]:
-  "min b a + (a - b) = (a :: nat)"
+lemma rev_min_pm [simp]: "min b a + (a - b) = a"
+  for a b :: nat
   by arith
 
-lemma rev_min_pm1 [simp]:
-  "a - b + min b a = (a :: nat)"
+lemma rev_min_pm1 [simp]: "a - b + min b a = a"
+  for a b :: nat
   by arith
 
-lemma min_minus [simp]:
-  "min m (m - k) = (m - k :: nat)"
+lemma min_minus [simp]: "min m (m - k) = m - k"
+  for m k :: nat
   by arith
-  
-lemma min_minus' [simp]:
-  "min (m - k) m = (m - k :: nat)"
+
+lemma min_minus' [simp]: "min (m - k) m = m - k"
+  for m k :: nat
   by arith
 
 end
-
diff -r 4ff2ba82d668 -r db7c97cdcfe7 src/Pure/General/long_name.ML
--- a/src/Pure/General/long_name.ML	Mon Apr 03 22:18:56 2017 +0200
+++ b/src/Pure/General/long_name.ML	Mon Apr 03 23:12:44 2017 +0200
@@ -64,4 +64,3 @@
       in implode (nth_map (length names - 1) f names) end;
 
 end;
-
diff -r 4ff2ba82d668 -r db7c97cdcfe7 src/Pure/General/long_name.scala
--- a/src/Pure/General/long_name.scala	Mon Apr 03 22:18:56 2017 +0200
+++ b/src/Pure/General/long_name.scala	Mon Apr 03 23:12:44 2017 +0200
@@ -25,4 +25,3 @@
     if (name == "") ""
     else explode(name).last
 }
-
diff -r 4ff2ba82d668 -r db7c97cdcfe7 src/Pure/PIDE/command.scala
--- a/src/Pure/PIDE/command.scala	Mon Apr 03 22:18:56 2017 +0200
+++ b/src/Pure/PIDE/command.scala	Mon Apr 03 23:12:44 2017 +0200
@@ -435,7 +435,7 @@
       // inlined errors
       case Thy_Header.THEORY =>
         val reader = Scan.char_reader(Token.implode(span.content))
-        val header = resources.check_thy_reader("", node_name, reader)
+        val header = resources.check_thy_reader(node_name, reader)
         val errors =
           for ((imp, pos) <- header.imports if !can_import(imp)) yield {
             val msg =
diff -r 4ff2ba82d668 -r db7c97cdcfe7 src/Pure/PIDE/document.ML
--- a/src/Pure/PIDE/document.ML	Mon Apr 03 22:18:56 2017 +0200
+++ b/src/Pure/PIDE/document.ML	Mon Apr 03 23:12:44 2017 +0200
@@ -178,9 +178,7 @@
   | NONE => false);
 
 fun loaded_theory name =
-  (case try (unsuffix ".thy") name of
-    SOME a => get_first Thy_Info.lookup_theory [a, Long_Name.base_name a]
-  | NONE => NONE);
+  get_first Thy_Info.lookup_theory [name, Long_Name.base_name name];
 
 fun get_node nodes name = String_Graph.get_node nodes name
   handle String_Graph.UNDEF _ => empty_node;
diff -r 4ff2ba82d668 -r db7c97cdcfe7 src/Pure/PIDE/document.scala
--- a/src/Pure/PIDE/document.scala	Mon Apr 03 22:18:56 2017 +0200
+++ b/src/Pure/PIDE/document.scala	Mon Apr 03 23:12:44 2017 +0200
@@ -98,6 +98,7 @@
     object Name
     {
       val empty = Name("")
+      def theory(theory: String): Name = Name(theory, "", theory)
 
       object Ordering extends scala.math.Ordering[Name]
       {
@@ -486,12 +487,12 @@
     def is_stable: Boolean
     def snapshot(): Snapshot
 
-    def node_name: Document.Node.Name
+    def node_name: Node.Name
     def is_theory: Boolean = node_name.is_theory
     override def toString: String = node_name.toString
 
     def node_required: Boolean
-    def get_blob: Option[Document.Blob]
+    def get_blob: Option[Blob]
 
     def node_edits(
       node_header: Node.Header,
@@ -502,13 +503,12 @@
         get_blob match {
           case None =>
             List(
-              Document.Node.Deps(
-                if (session.resources.base.loaded_theories(node_name.theory))
+              Node.Deps(
+                if (session.resources.session_base.loaded_theory(node_name))
                   node_header.error("Cannot update finished theory " + quote(node_name.theory))
                 else node_header),
-              Document.Node.Edits(text_edits), perspective)
-          case Some(blob) =>
-            List(Document.Node.Blob(blob), Document.Node.Edits(text_edits))
+              Node.Edits(text_edits), perspective)
+          case Some(blob) => List(Node.Blob(blob), Node.Edits(text_edits))
         }
       edits.flatMap(edit => if (edit.is_void) None else Some(node_name -> edit))
     }
diff -r 4ff2ba82d668 -r db7c97cdcfe7 src/Pure/PIDE/resources.scala
--- a/src/Pure/PIDE/resources.scala	Mon Apr 03 22:18:56 2017 +0200
+++ b/src/Pure/PIDE/resources.scala	Mon Apr 03 23:12:44 2017 +0200
@@ -13,26 +13,16 @@
 import java.io.{File => JFile}
 
 
-class Resources(val base: Sessions.Base, val log: Logger = No_Logger)
+class Resources(
+  val session_name: String,
+  val session_base: Sessions.Base,
+  val log: Logger = No_Logger)
 {
   val thy_info = new Thy_Info(this)
 
   def thy_path(path: Path): Path = path.ext("thy")
 
 
-  /* document node names */
-
-  def node_name(qualifier: String, raw_path: Path): Document.Node.Name =
-  {
-    val no_qualifier = "" // FIXME
-    val path = raw_path.expand
-    val node = path.implode
-    val theory = Long_Name.qualify(no_qualifier, Thy_Header.thy_name(node).getOrElse(""))
-    val master_dir = if (theory == "") "" else path.dir.implode
-    Document.Node.Name(node, master_dir, theory)
-  }
-
-
   /* file-system operations */
 
   def append(dir: String, source_path: Path): String =
@@ -77,28 +67,38 @@
     }
     else Nil
 
-  private def dummy_name(theory: String): Document.Node.Name =
-    Document.Node.Name(theory + ".thy", "", theory)
+  def init_name(global: Boolean, raw_path: Path): Document.Node.Name =
+  {
+    val path = raw_path.expand
+    val node = path.implode
+    val qualifier = if (global) "" else session_name
+    val theory = Long_Name.qualify(qualifier, Thy_Header.thy_name(node).getOrElse(""))
+    val master_dir = if (theory == "") "" else path.dir.implode
+    Document.Node.Name(node, master_dir, theory)
+  }
 
-  def import_name(qualifier: String, master: Document.Node.Name, s: String): Document.Node.Name =
+  def import_name(master: Document.Node.Name, s: String): Document.Node.Name =
   {
-    val no_qualifier = "" // FIXME
-    val thy1 = Thy_Header.base_name(s)
-    val thy2 = if (Long_Name.is_qualified(thy1)) thy1 else Long_Name.qualify(no_qualifier, thy1)
-    (base.known_theories.get(thy1) orElse
-     base.known_theories.get(thy2) orElse
-     base.known_theories.get(Long_Name.base_name(thy1))) match {
-      case Some(name) if base.loaded_theories(name.theory) => dummy_name(name.theory)
+    val theory = Thy_Header.base_name(s)
+    val is_base_name = Thy_Header.is_base_name(s)
+    val is_qualified = is_base_name && Long_Name.is_qualified(s)
+
+    val known_theory =
+      if (is_base_name)
+        session_base.known_theories.get(theory) orElse
+        (if (is_qualified) session_base.known_theories.get(Long_Name.base_name(theory))
+         else session_base.known_theories.get(Long_Name.qualify(session_name, theory)))
+      else None
+
+    known_theory match {
+      case Some(name) if session_base.loaded_theory(name) => Document.Node.Name.theory(name.theory)
       case Some(name) => name
+      case None if is_qualified => Document.Node.Name.theory(theory)
       case None =>
         val path = Path.explode(s)
-        val theory = path.base.implode
-        if (Long_Name.is_qualified(theory)) dummy_name(theory)
-        else {
-          val node = append(master.master_dir, thy_path(path))
-          val master_dir = append(master.master_dir, path.dir)
-          Document.Node.Name(node, master_dir, Long_Name.qualify(no_qualifier, theory))
-        }
+        val node = append(master.master_dir, thy_path(path))
+        val master_dir = append(master.master_dir, path.dir)
+        Document.Node.Name(node, master_dir, Long_Name.qualify(session_name, theory))
     }
   }
 
@@ -111,9 +111,8 @@
     try { f(reader) } finally { reader.close }
   }
 
-  def check_thy_reader(qualifier: String, node_name: Document.Node.Name,
-      reader: Reader[Char], start: Token.Pos = Token.Pos.command, strict: Boolean = true)
-    : Document.Node.Header =
+  def check_thy_reader(node_name: Document.Node.Name, reader: Reader[Char],
+    start: Token.Pos = Token.Pos.command, strict: Boolean = true): Document.Node.Header =
   {
     if (node_name.is_theory && reader.source.length > 0) {
       try {
@@ -127,7 +126,7 @@
             Completion.report_names(pos, 1, List((base_name, ("theory", base_name)))))
 
         val imports =
-          header.imports.map({ case (s, pos) => (import_name(qualifier, node_name, s), pos) })
+          header.imports.map({ case (s, pos) => (import_name(node_name, s), pos) })
         Document.Node.Header(imports, header.keywords, header.abbrevs)
       }
       catch { case exn: Throwable => Document.Node.bad_header(Exn.message(exn)) }
@@ -135,18 +134,18 @@
     else Document.Node.no_header
   }
 
-  def check_thy(qualifier: String, name: Document.Node.Name,
-      start: Token.Pos = Token.Pos.command, strict: Boolean = true): Document.Node.Header =
-    with_thy_reader(name, check_thy_reader(qualifier, name, _, start, strict))
+  def check_thy(name: Document.Node.Name, start: Token.Pos = Token.Pos.command,
+      strict: Boolean = true): Document.Node.Header =
+    with_thy_reader(name, check_thy_reader(name, _, start, strict))
 
 
   /* special header */
 
   def special_header(name: Document.Node.Name): Option[Document.Node.Header] =
     if (Thy_Header.is_ml_root(name.theory))
-      Some(Document.Node.Header(List((import_name("", name, Thy_Header.ML_BOOTSTRAP), Position.none))))
+      Some(Document.Node.Header(List((import_name(name, Thy_Header.ML_BOOTSTRAP), Position.none))))
     else if (Thy_Header.is_bootstrap(name.theory))
-      Some(Document.Node.Header(List((import_name("", name, Thy_Header.PURE), Position.none))))
+      Some(Document.Node.Header(List((import_name(name, Thy_Header.PURE), Position.none))))
     else None
 
 
@@ -155,7 +154,7 @@
   def undefined_blobs(nodes: Document.Nodes): List[Document.Node.Name] =
     (for {
       (node_name, node) <- nodes.iterator
-      if !base.loaded_theories(node_name.theory)
+      if !session_base.loaded_theory(node_name)
       cmd <- node.load_commands.iterator
       name <- cmd.blobs_undefined.iterator
     } yield name).toList
diff -r 4ff2ba82d668 -r db7c97cdcfe7 src/Pure/PIDE/session.scala
--- a/src/Pure/PIDE/session.scala	Mon Apr 03 22:18:56 2017 +0200
+++ b/src/Pure/PIDE/session.scala	Mon Apr 03 23:12:44 2017 +0200
@@ -191,7 +191,7 @@
 
   def recent_syntax(name: Document.Node.Name): Outer_Syntax =
     global_state.value.recent_finished.version.get_finished.nodes(name).syntax getOrElse
-    resources.base.syntax
+    resources.session_base.syntax
 
 
   /* pipelined change parsing */
diff -r 4ff2ba82d668 -r db7c97cdcfe7 src/Pure/Thy/sessions.scala
--- a/src/Pure/Thy/sessions.scala	Mon Apr 03 22:18:56 2017 +0200
+++ b/src/Pure/Thy/sessions.scala	Mon Apr 03 23:12:44 2017 +0200
@@ -17,25 +17,14 @@
 
 object Sessions
 {
-  /* Pure */
-
-  def pure_name(name: String): Boolean = name == Thy_Header.PURE
+  /* base info and source dependencies */
 
-  def pure_files(resources: Resources, syntax: Outer_Syntax, dir: Path): List[Path] =
-  {
-    val roots = Thy_Header.ml_roots.map(_._1)
-    val loaded_files =
-      roots.flatMap(root => resources.loaded_files(syntax, File.read(dir + Path.explode(root))))
-    (roots ::: loaded_files).map(file => dir + Path.explode(file))
-  }
-
-  def pure_base(options: Options): Base = session_base(options, Thy_Header.PURE)
-
-
-  /* base info and source dependencies */
+  def is_pure(name: String): Boolean = name == Thy_Header.PURE
 
   object Base
   {
+    def pure(options: Options): Base = session_base(options, Thy_Header.PURE)
+
     lazy val bootstrap: Base =
       Base(keywords = Thy_Header.bootstrap_header, syntax = Thy_Header.bootstrap_syntax)
   }
@@ -47,6 +36,10 @@
     syntax: Outer_Syntax = Outer_Syntax.empty,
     sources: List[(Path, SHA1.Digest)] = Nil,
     session_graph: Graph_Display.Graph = Graph_Display.empty_graph)
+  {
+    def loaded_theory(name: Document.Node.Name): Boolean =
+      loaded_theories.contains(name.theory)
+  }
 
   sealed case class Deps(deps: Map[String, Base])
   {
@@ -67,12 +60,12 @@
           if (progress.stopped) throw Exn.Interrupt()
 
           try {
-            val resources =
-              new Resources(
-                info.parent match {
-                  case None => Base.bootstrap
-                  case Some(parent) => deps(parent)
-                })
+            val parent_base =
+              info.parent match {
+                case None => Base.bootstrap
+                case Some(parent) => deps(parent)
+              }
+            val resources = new Resources(name, parent_base)
 
             if (verbose || list_files) {
               val groups =
@@ -87,10 +80,9 @@
                 info.theories.flatMap({
                   case (global, _, thys) =>
                     thys.map(thy =>
-                      (resources.node_name(
-                        if (global) "" else name, info.dir + resources.thy_path(thy)), info.pos))
+                      (resources.init_name(global, info.dir + resources.thy_path(thy)), info.pos))
                 })
-              val thy_deps = resources.thy_info.dependencies(name, root_theories)
+              val thy_deps = resources.thy_info.dependencies(root_theories)
 
               thy_deps.errors match {
                 case Nil => thy_deps
@@ -99,7 +91,7 @@
             }
 
             val known_theories =
-              (resources.base.known_theories /: thy_deps.deps)({ case (known, dep) =>
+              (parent_base.known_theories /: thy_deps.deps)({ case (known, dep) =>
                 val name = dep.name
                 known.get(name.theory) match {
                   case Some(name1) if name != name1 =>
@@ -117,7 +109,13 @@
             val loaded_files =
               if (inlined_files) {
                 val pure_files =
-                  if (pure_name(name)) Sessions.pure_files(resources, syntax, info.dir)
+                  if (is_pure(name)) {
+                    val roots = Thy_Header.ml_roots.map(p => info.dir + Path.explode(p._1))
+                    val files =
+                      roots.flatMap(root => resources.loaded_files(syntax, File.read(root))).
+                        map(file => info.dir + Path.explode(file))
+                    roots ::: files
+                  }
                   else Nil
                 pure_files ::: thy_deps.loaded_files
               }
@@ -138,7 +136,7 @@
 
             val session_graph =
               Present.session_graph(info.parent getOrElse "",
-                resources.base.loaded_theories, thy_deps.deps)
+                parent_base.loaded_theories, thy_deps.deps)
 
             val base =
               Base(loaded_theories, known_theories, keywords, syntax, sources, session_graph)
@@ -365,8 +363,8 @@
           val name = entry.name
 
           if (name == "") error("Bad session name")
-          if (pure_name(name) && entry.parent.isDefined) error("Illegal parent session")
-          if (!pure_name(name) && !entry.parent.isDefined) error("Missing parent session")
+          if (is_pure(name) && entry.parent.isDefined) error("Illegal parent session")
+          if (!is_pure(name) && !entry.parent.isDefined) error("Missing parent session")
 
           val session_options = options ++ entry.options
 
diff -r 4ff2ba82d668 -r db7c97cdcfe7 src/Pure/Thy/thy_header.scala
--- a/src/Pure/Thy/thy_header.scala	Mon Apr 03 22:18:56 2017 +0200
+++ b/src/Pure/Thy/thy_header.scala	Mon Apr 03 23:12:44 2017 +0200
@@ -80,6 +80,9 @@
   private val Base_Name = new Regex(""".*?([^/\\:]+)""")
   private val Thy_Name = new Regex(""".*?([^/\\:]+)\.thy""")
 
+  def is_base_name(s: String): Boolean =
+    s != "" && !s.exists("/\\:".contains(_))
+
   def base_name(s: String): String =
     s match { case Base_Name(name) => name case _ => error("Malformed import: " + quote(s)) }
 
diff -r 4ff2ba82d668 -r db7c97cdcfe7 src/Pure/Thy/thy_info.scala
--- a/src/Pure/Thy/thy_info.scala	Mon Apr 03 22:18:56 2017 +0200
+++ b/src/Pure/Thy/thy_info.scala	Mon Apr 03 23:12:44 2017 +0200
@@ -71,7 +71,7 @@
       val import_errors =
         (for {
           (theory, names) <- seen_names.iterator_list
-          if !resources.base.loaded_theories(theory)
+          if !resources.session_base.loaded_theories(theory)
           if names.length > 1
         } yield
           "Incoherent imports for theory " + quote(theory) + ":\n" +
@@ -83,10 +83,12 @@
     }
 
     lazy val syntax: Outer_Syntax =
-      resources.base.syntax.add_keywords(keywords).add_abbrevs(abbrevs)
+      resources.session_base.syntax.add_keywords(keywords).add_abbrevs(abbrevs)
 
     def loaded_theories: Set[String] =
-      (resources.base.loaded_theories /: rev_deps) { case (loaded, dep) => loaded + dep.name.theory }
+      (resources.session_base.loaded_theories /: rev_deps) {
+        case (loaded, dep) => loaded + dep.name.theory
+      }
 
     def loaded_files: List[Path] =
     {
@@ -104,12 +106,12 @@
     override def toString: String = deps.toString
   }
 
-  private def require_thys(session: String, initiators: List[Document.Node.Name],
-      required: Dependencies, thys: List[(Document.Node.Name, Position.T)]): Dependencies =
-    (required /: thys)(require_thy(session, initiators, _, _))
+  private def require_thys(initiators: List[Document.Node.Name], required: Dependencies,
+      thys: List[(Document.Node.Name, Position.T)]): Dependencies =
+    (required /: thys)(require_thy(initiators, _, _))
 
-  private def require_thy(session: String, initiators: List[Document.Node.Name],
-      required: Dependencies, thy: (Document.Node.Name, Position.T)): Dependencies =
+  private def require_thy(initiators: List[Document.Node.Name], required: Dependencies,
+    thy: (Document.Node.Name, Position.T)): Dependencies =
   {
     val (name, require_pos) = thy
 
@@ -118,15 +120,14 @@
         required_by(initiators) + Position.here(require_pos)
 
     val required1 = required + thy
-    if (required.seen(name) || resources.base.loaded_theories(name.theory)) required1
+    if (required.seen(name) || resources.session_base.loaded_theory(name)) required1
     else {
       try {
         if (initiators.contains(name)) error(cycle_msg(initiators))
         val header =
-          try { resources.check_thy(session, name, Token.Pos.file(name.node)).cat_errors(message) }
+          try { resources.check_thy(name, Token.Pos.file(name.node)).cat_errors(message) }
           catch { case ERROR(msg) => cat_error(msg, message) }
-        Thy_Info.Dep(name, header) ::
-          require_thys(session, name :: initiators, required1, header.imports)
+        Thy_Info.Dep(name, header) :: require_thys(name :: initiators, required1, header.imports)
       }
       catch {
         case e: Throwable =>
@@ -135,6 +136,6 @@
     }
   }
 
-  def dependencies(session: String, thys: List[(Document.Node.Name, Position.T)]): Dependencies =
-    require_thys(session, Nil, Dependencies.empty, thys)
+  def dependencies(thys: List[(Document.Node.Name, Position.T)]): Dependencies =
+    require_thys(Nil, Dependencies.empty, thys)
 }
diff -r 4ff2ba82d668 -r db7c97cdcfe7 src/Pure/Thy/thy_syntax.scala
--- a/src/Pure/Thy/thy_syntax.scala	Mon Apr 03 22:18:56 2017 +0200
+++ b/src/Pure/Thy/thy_syntax.scala	Mon Apr 03 23:12:44 2017 +0200
@@ -101,7 +101,7 @@
         else {
           val header = node.header
           val imports_syntax = header.imports.flatMap(a => nodes(a._1).syntax)
-          Some((resources.base.syntax /: imports_syntax)(_ ++ _)
+          Some((resources.session_base.syntax /: imports_syntax)(_ ++ _)
             .add_keywords(header.keywords).add_abbrevs(header.abbrevs))
         }
       nodes += (name -> node.update_syntax(syntax))
@@ -300,7 +300,7 @@
       doc_blobs.get(name) orElse previous.nodes(name).get_blob
 
     def can_import(name: Document.Node.Name): Boolean =
-      resources.base.loaded_theories(name.theory) || nodes0(name).has_header
+      resources.session_base.loaded_theory(name) || nodes0(name).has_header
 
     val (doc_edits, version) =
       if (edits.isEmpty) (Nil, Document.Version.make(previous.nodes))
@@ -324,7 +324,7 @@
         node_edits foreach {
           case (name, edits) =>
             val node = nodes(name)
-            val syntax = node.syntax getOrElse resources.base.syntax
+            val syntax = node.syntax getOrElse resources.session_base.syntax
             val commands = node.commands
 
             val node1 =
diff -r 4ff2ba82d668 -r db7c97cdcfe7 src/Pure/Tools/build.scala
--- a/src/Pure/Tools/build.scala	Mon Apr 03 22:18:56 2017 +0200
+++ b/src/Pure/Tools/build.scala	Mon Apr 03 23:12:44 2017 +0200
@@ -219,8 +219,8 @@
           "ML_Heap.share_common_data (); ML_Heap.save_child " +
             ML_Syntax.print_string0(File.platform_path(output))
 
-        if (pide && !Sessions.pure_name(name)) {
-          val resources = new Resources(deps(parent))
+        if (pide && !Sessions.is_pure(name)) {
+          val resources = new Resources(name, deps(parent))
           val session = new Session(options, resources)
           val handler = new Handler(progress, session, name)
           session.init_protocol_handler(handler)
@@ -255,7 +255,7 @@
             (if (do_output) "; " + save_heap else "") + "));"
 
           val process =
-            if (Sessions.pure_name(name)) {
+            if (Sessions.is_pure(name)) {
               ML_Process(options, raw_ml_system = true, cwd = info.dir.file,
                 args =
                   (for ((root, _) <- Thy_Header.ml_roots) yield List("--use", root)).flatten :::
@@ -519,7 +519,7 @@
                 val ancestor_results = selected_tree.ancestors(name).map(results(_))
                 val ancestor_heaps = ancestor_results.flatMap(_.heap_stamp)
 
-                val do_output = build_heap || Sessions.pure_name(name) || queue.is_inner(name)
+                val do_output = build_heap || Sessions.is_pure(name) || queue.is_inner(name)
 
                 val (current, heap_stamp) =
                 {
diff -r 4ff2ba82d668 -r db7c97cdcfe7 src/Tools/VSCode/src/document_model.scala
--- a/src/Tools/VSCode/src/document_model.scala	Mon Apr 03 22:18:56 2017 +0200
+++ b/src/Tools/VSCode/src/document_model.scala	Mon Apr 03 23:12:44 2017 +0200
@@ -73,7 +73,7 @@
 
   def node_header: Document.Node.Header =
     resources.special_header(node_name) getOrElse
-      resources.check_thy_reader("", node_name, Scan.char_reader(content.text))
+      resources.check_thy_reader(node_name, Scan.char_reader(content.text))
 
 
   /* perspective */
diff -r 4ff2ba82d668 -r db7c97cdcfe7 src/Tools/VSCode/src/server.scala
--- a/src/Tools/VSCode/src/server.scala	Mon Apr 03 22:18:56 2017 +0200
+++ b/src/Tools/VSCode/src/server.scala	Mon Apr 03 23:12:44 2017 +0200
@@ -225,8 +225,8 @@
           }
         }
 
-        val base = Sessions.session_base(options, session_name, session_dirs)
-        val resources = new VSCode_Resources(options, base, log)
+        val session_base = Sessions.session_base(options, session_name, session_dirs)
+        val resources = new VSCode_Resources(options, session_base, log)
           {
             override def commit(change: Session.Change): Unit =
               if (change.deps_changed || undefined_blobs(change.version.nodes).nonEmpty)
diff -r 4ff2ba82d668 -r db7c97cdcfe7 src/Tools/VSCode/src/vscode_resources.scala
--- a/src/Tools/VSCode/src/vscode_resources.scala	Mon Apr 03 22:18:56 2017 +0200
+++ b/src/Tools/VSCode/src/vscode_resources.scala	Mon Apr 03 23:12:44 2017 +0200
@@ -40,9 +40,10 @@
 }
 
 class VSCode_Resources(
-  val options: Options,
-  base: Sessions.Base,
-  log: Logger = No_Logger) extends Resources(base, log)
+    val options: Options,
+    session_base: Sessions.Base,
+    log: Logger = No_Logger)
+  extends Resources(session_name = "", session_base, log)
 {
   private val state = Synchronized(VSCode_Resources.State())
 
@@ -165,7 +166,7 @@
           (for ((_, model) <- st.models.iterator if model.is_theory)
            yield (model.node_name, Position.none)).toList
 
-        val thy_files = thy_info.dependencies("", thys).deps.map(_.name)
+        val thy_files = thy_info.dependencies(thys).deps.map(_.name)
 
 
         /* auxiliary files */
diff -r 4ff2ba82d668 -r db7c97cdcfe7 src/Tools/jEdit/src/document_model.scala
--- a/src/Tools/jEdit/src/document_model.scala	Mon Apr 03 22:18:56 2017 +0200
+++ b/src/Tools/jEdit/src/document_model.scala	Mon Apr 03 23:12:44 2017 +0200
@@ -235,7 +235,7 @@
               val pending_nodes = for ((node_name, None) <- purged) yield node_name
               (open_nodes ::: touched_nodes ::: pending_nodes).map((_, Position.none))
             }
-            val retain = PIDE.resources.thy_info.dependencies("", imports).deps.map(_.name).toSet
+            val retain = PIDE.resources.thy_info.dependencies(imports).deps.map(_.name).toSet
 
             for ((node_name, Some(edits)) <- purged; if !retain(node_name); edit <- edits)
               yield edit
@@ -331,7 +331,7 @@
 
   def node_header: Document.Node.Header =
     PIDE.resources.special_header(node_name) getOrElse
-      PIDE.resources.check_thy_reader("", node_name, Scan.char_reader(content.text), strict = false)
+      PIDE.resources.check_thy_reader(node_name, Scan.char_reader(content.text), strict = false)
 
 
   /* content */
@@ -396,8 +396,7 @@
 
     PIDE.resources.special_header(node_name) getOrElse
       JEdit_Lib.buffer_lock(buffer) {
-        PIDE.resources.check_thy_reader(
-          "", node_name, JEdit_Lib.buffer_reader(buffer), strict = false)
+        PIDE.resources.check_thy_reader(node_name, JEdit_Lib.buffer_reader(buffer), strict = false)
       }
   }
 
diff -r 4ff2ba82d668 -r db7c97cdcfe7 src/Tools/jEdit/src/isabelle.scala
--- a/src/Tools/jEdit/src/isabelle.scala	Mon Apr 03 22:18:56 2017 +0200
+++ b/src/Tools/jEdit/src/isabelle.scala	Mon Apr 03 23:12:44 2017 +0200
@@ -50,7 +50,7 @@
 
   def mode_syntax(mode: String): Option[Outer_Syntax] =
     mode match {
-      case "isabelle" => Some(PIDE.resources.base.syntax)
+      case "isabelle" => Some(PIDE.resources.session_base.syntax)
       case "isabelle-options" => Some(Options.options_syntax)
       case "isabelle-root" => Some(Sessions.root_syntax)
       case "isabelle-ml" => Some(ml_syntax)
diff -r 4ff2ba82d668 -r db7c97cdcfe7 src/Tools/jEdit/src/jedit_resources.scala
--- a/src/Tools/jEdit/src/jedit_resources.scala	Mon Apr 03 22:18:56 2017 +0200
+++ b/src/Tools/jEdit/src/jedit_resources.scala	Mon Apr 03 23:12:44 2017 +0200
@@ -21,7 +21,8 @@
 import org.gjt.sp.jedit.bufferio.BufferIORequest
 
 
-class JEdit_Resources(base: Sessions.Base) extends Resources(base)
+class JEdit_Resources(session_base: Sessions.Base)
+  extends Resources(session_name = "", session_base)
 {
   /* document node name */
 
diff -r 4ff2ba82d668 -r db7c97cdcfe7 src/Tools/jEdit/src/plugin.scala
--- a/src/Tools/jEdit/src/plugin.scala	Mon Apr 03 22:18:56 2017 +0200
+++ b/src/Tools/jEdit/src/plugin.scala	Mon Apr 03 23:12:44 2017 +0200
@@ -74,7 +74,7 @@
     val session_name = JEdit_Sessions.session_name(options)
     val session_base =
       try { Sessions.session_base(options, session_name, JEdit_Sessions.session_dirs()) }
-      catch { case ERROR(_) => Sessions.pure_base(options) }
+      catch { case ERROR(_) => Sessions.Base.pure(options) }
 
     _resources =
       new JEdit_Resources(session_base.copy(known_theories =
@@ -135,7 +135,7 @@
           val thys =
             (for ((node_name, model) <- models.iterator if model.is_theory)
               yield (node_name, Position.none)).toList
-          val thy_files = resources.thy_info.dependencies("", thys).deps.map(_.name)
+          val thy_files = resources.thy_info.dependencies(thys).deps.map(_.name)
 
           val aux_files =
             if (options.bool("jedit_auto_resolve")) {
diff -r 4ff2ba82d668 -r db7c97cdcfe7 src/Tools/jEdit/src/theories_dockable.scala
--- a/src/Tools/jEdit/src/theories_dockable.scala	Mon Apr 03 22:18:56 2017 +0200
+++ b/src/Tools/jEdit/src/theories_dockable.scala	Mon Apr 03 23:12:44 2017 +0200
@@ -192,7 +192,7 @@
       }
     val nodes_status1 =
       (nodes_status /: iterator)({ case (status, (name, node)) =>
-          if (!name.is_theory || PIDE.resources.base.loaded_theories(name.theory) || node.is_empty)
+          if (!name.is_theory || PIDE.resources.session_base.loaded_theory(name) || node.is_empty)
             status
           else status + (name -> Protocol.node_status(snapshot.state, snapshot.version, node)) })
 
diff -r 4ff2ba82d668 -r db7c97cdcfe7 src/Tools/jEdit/src/timing_dockable.scala
--- a/src/Tools/jEdit/src/timing_dockable.scala	Mon Apr 03 22:18:56 2017 +0200
+++ b/src/Tools/jEdit/src/timing_dockable.scala	Mon Apr 03 23:12:44 2017 +0200
@@ -187,7 +187,7 @@
       }
     val nodes_timing1 =
       (nodes_timing /: iterator)({ case (timing1, (name, node)) =>
-          if (PIDE.resources.base.loaded_theories(name.theory)) timing1
+          if (PIDE.resources.session_base.loaded_theory(name)) timing1
           else {
             val node_timing =
               Protocol.node_timing(snapshot.state, snapshot.version, node, timing_threshold)