misc tuning and modernization;
authorwenzelm
Sun Dec 03 18:53:49 2017 +0100 (10 months ago)
changeset 67120491fd7f0b5df
parent 67119 acb0807ddb56
child 67121 116968454d70
misc tuning and modernization;
src/HOL/Word/Bit_Comparison.thy
src/HOL/Word/Bits_Bit.thy
src/HOL/Word/Bits_Int.thy
src/HOL/Word/Bool_List_Representation.thy
src/HOL/Word/Misc_Typedef.thy
src/HOL/Word/WordBitwise.thy
src/HOL/Word/Word_Miscellaneous.thy
     1.1 --- a/src/HOL/Word/Bit_Comparison.thy	Sun Dec 03 13:22:09 2017 +0100
     1.2 +++ b/src/HOL/Word/Bit_Comparison.thy	Sun Dec 03 18:53:49 2017 +0100
     1.3 @@ -6,15 +6,21 @@
     1.4  *)
     1.5  
     1.6  theory Bit_Comparison
     1.7 -imports Bits_Int
     1.8 +  imports Bits_Int
     1.9  begin
    1.10  
    1.11  lemma AND_lower [simp]:
    1.12 -  fixes x :: int and y :: int
    1.13 +  fixes x y :: int
    1.14    assumes "0 \<le> x"
    1.15    shows "0 \<le> x AND y"
    1.16    using assms
    1.17  proof (induct x arbitrary: y rule: bin_induct)
    1.18 +  case 1
    1.19 +  then show ?case by simp
    1.20 +next
    1.21 +  case 2
    1.22 +  then show ?case by (simp only: Min_def)
    1.23 +next
    1.24    case (3 bin bit)
    1.25    show ?case
    1.26    proof (cases y rule: bin_exhaust)
    1.27 @@ -25,13 +31,10 @@
    1.28      with 1 show ?thesis
    1.29        by simp (simp add: Bit_def)
    1.30    qed
    1.31 -next
    1.32 -  case 2
    1.33 -  then show ?case by (simp only: Min_def)
    1.34 -qed simp
    1.35 +qed
    1.36  
    1.37  lemma OR_lower [simp]:
    1.38 -  fixes x :: int and y :: int
    1.39 +  fixes x y :: int
    1.40    assumes "0 \<le> x" "0 \<le> y"
    1.41    shows "0 \<le> x OR y"
    1.42    using assms
    1.43 @@ -51,7 +54,7 @@
    1.44  qed simp_all
    1.45  
    1.46  lemma XOR_lower [simp]:
    1.47 -  fixes x :: int and y :: int
    1.48 +  fixes x y :: int
    1.49    assumes "0 \<le> x" "0 \<le> y"
    1.50    shows "0 \<le> x XOR y"
    1.51    using assms
    1.52 @@ -74,7 +77,7 @@
    1.53  qed simp
    1.54  
    1.55  lemma AND_upper1 [simp]:
    1.56 -  fixes x :: int and y :: int
    1.57 +  fixes x y :: int
    1.58    assumes "0 \<le> x"
    1.59    shows "x AND y \<le> x"
    1.60    using assms
    1.61 @@ -98,11 +101,17 @@
    1.62  lemmas AND_upper1'' [simp] = order_le_less_trans [OF AND_upper1]
    1.63  
    1.64  lemma AND_upper2 [simp]:
    1.65 -  fixes x :: int and y :: int
    1.66 +  fixes x y :: int
    1.67    assumes "0 \<le> y"
    1.68    shows "x AND y \<le> y"
    1.69    using assms
    1.70  proof (induct y arbitrary: x rule: bin_induct)
    1.71 +  case 1
    1.72 +  then show ?case by simp
    1.73 +next
    1.74 +  case 2
    1.75 +  then show ?case by (simp only: Min_def)
    1.76 +next
    1.77    case (3 bin bit)
    1.78    show ?case
    1.79    proof (cases x rule: bin_exhaust)
    1.80 @@ -113,16 +122,13 @@
    1.81      with 1 show ?thesis
    1.82        by simp (simp add: Bit_def)
    1.83    qed
    1.84 -next
    1.85 -  case 2
    1.86 -  then show ?case by (simp only: Min_def)
    1.87 -qed simp
    1.88 +qed
    1.89  
    1.90  lemmas AND_upper2' [simp] = order_trans [OF AND_upper2]
    1.91  lemmas AND_upper2'' [simp] = order_le_less_trans [OF AND_upper2]
    1.92  
    1.93  lemma OR_upper:
    1.94 -  fixes x :: int and y :: int
    1.95 +  fixes x y :: int
    1.96    assumes "0 \<le> x" "x < 2 ^ n" "y < 2 ^ n"
    1.97    shows "x OR y < 2 ^ n"
    1.98    using assms
    1.99 @@ -155,11 +161,17 @@
   1.100  qed simp_all
   1.101  
   1.102  lemma XOR_upper:
   1.103 -  fixes x :: int and y :: int
   1.104 +  fixes x y :: int
   1.105    assumes "0 \<le> x" "x < 2 ^ n" "y < 2 ^ n"
   1.106    shows "x XOR y < 2 ^ n"
   1.107    using assms
   1.108  proof (induct x arbitrary: y n rule: bin_induct)
   1.109 +  case 1
   1.110 +  then show ?case by simp
   1.111 +next
   1.112 +  case 2
   1.113 +  then show ?case by (simp only: Min_def)
   1.114 +next
   1.115    case (3 bin bit)
   1.116    show ?case
   1.117    proof (cases y rule: bin_exhaust)
   1.118 @@ -185,9 +197,6 @@
   1.119          by simp (simp add: Bit_def)
   1.120      qed
   1.121    qed
   1.122 -next
   1.123 -  case 2
   1.124 -  then show ?case by (simp only: Min_def)
   1.125 -qed simp
   1.126 +qed
   1.127  
   1.128  end
     2.1 --- a/src/HOL/Word/Bits_Bit.thy	Sun Dec 03 13:22:09 2017 +0100
     2.2 +++ b/src/HOL/Word/Bits_Bit.thy	Sun Dec 03 18:53:49 2017 +0100
     2.3 @@ -5,7 +5,7 @@
     2.4  section \<open>Bit operations in $\cal Z_2$\<close>
     2.5  
     2.6  theory Bits_Bit
     2.7 -imports Bits "HOL-Library.Bit"
     2.8 +  imports Bits "HOL-Library.Bit"
     2.9  begin
    2.10  
    2.11  instantiation bit :: bit
    2.12 @@ -46,21 +46,21 @@
    2.13    "x XOR 1 = NOT x"
    2.14    "x XOR 0 = x"
    2.15    for x :: bit
    2.16 -  by (cases x, auto)+
    2.17 +  by (cases x; auto)+
    2.18  
    2.19  lemma bit_ops_comm:
    2.20    "x AND y = y AND x"
    2.21    "x OR y = y OR x"
    2.22    "x XOR y = y XOR x"
    2.23    for x :: bit
    2.24 -  by (cases y, auto)+
    2.25 +  by (cases y; auto)+
    2.26  
    2.27  lemma bit_ops_same [simp]:
    2.28    "x AND x = x"
    2.29    "x OR x = x"
    2.30    "x XOR x = 0"
    2.31    for x :: bit
    2.32 -  by (cases x, auto)+
    2.33 +  by (cases x; auto)+
    2.34  
    2.35  lemma bit_not_not [simp]: "NOT (NOT x) = x"
    2.36    for x :: bit
     3.1 --- a/src/HOL/Word/Bits_Int.thy	Sun Dec 03 13:22:09 2017 +0100
     3.2 +++ b/src/HOL/Word/Bits_Int.thy	Sun Dec 03 18:53:49 2017 +0100
     3.3 @@ -32,11 +32,9 @@
     3.4  
     3.5  declare bitAND_int.simps [simp del]
     3.6  
     3.7 -definition int_or_def:
     3.8 -  "bitOR = (\<lambda>x y::int. NOT (NOT x AND NOT y))"
     3.9 +definition int_or_def: "bitOR = (\<lambda>x y::int. NOT (NOT x AND NOT y))"
    3.10  
    3.11 -definition int_xor_def:
    3.12 -  "bitXOR = (\<lambda>x y::int. (x AND NOT y) OR (NOT x AND y))"
    3.13 +definition int_xor_def: "bitXOR = (\<lambda>x y::int. (x AND NOT y) OR (NOT x AND y))"
    3.14  
    3.15  instance ..
    3.16  
    3.17 @@ -44,9 +42,8 @@
    3.18  
    3.19  subsubsection \<open>Basic simplification rules\<close>
    3.20  
    3.21 -lemma int_not_BIT [simp]:
    3.22 -  "NOT (w BIT b) = (NOT w) BIT (\<not> b)"
    3.23 -  unfolding int_not_def Bit_def by (cases b, simp_all)
    3.24 +lemma int_not_BIT [simp]: "NOT (w BIT b) = (NOT w) BIT (\<not> b)"
    3.25 +  by (cases b) (simp_all add: int_not_def Bit_def)
    3.26  
    3.27  lemma int_not_simps [simp]:
    3.28    "NOT (0::int) = -1"
    3.29 @@ -57,160 +54,172 @@
    3.30    "NOT (- numeral (Num.Bit1 w)::int) = numeral (Num.Bit0 w)"
    3.31    unfolding int_not_def by simp_all
    3.32  
    3.33 -lemma int_not_not [simp]: "NOT (NOT (x::int)) = x"
    3.34 +lemma int_not_not [simp]: "NOT (NOT x) = x"
    3.35 +  for x :: int
    3.36    unfolding int_not_def by simp
    3.37  
    3.38 -lemma int_and_0 [simp]: "(0::int) AND x = 0"
    3.39 +lemma int_and_0 [simp]: "0 AND x = 0"
    3.40 +  for x :: int
    3.41    by (simp add: bitAND_int.simps)
    3.42  
    3.43 -lemma int_and_m1 [simp]: "(-1::int) AND x = x"
    3.44 +lemma int_and_m1 [simp]: "-1 AND x = x"
    3.45 +  for x :: int
    3.46    by (simp add: bitAND_int.simps)
    3.47  
    3.48 -lemma int_and_Bits [simp]:
    3.49 -  "(x BIT b) AND (y BIT c) = (x AND y) BIT (b \<and> c)"
    3.50 -  by (subst bitAND_int.simps, simp add: Bit_eq_0_iff Bit_eq_m1_iff)
    3.51 +lemma int_and_Bits [simp]: "(x BIT b) AND (y BIT c) = (x AND y) BIT (b \<and> c)"
    3.52 +  by (subst bitAND_int.simps) (simp add: Bit_eq_0_iff Bit_eq_m1_iff)
    3.53  
    3.54 -lemma int_or_zero [simp]: "(0::int) OR x = x"
    3.55 -  unfolding int_or_def by simp
    3.56 +lemma int_or_zero [simp]: "0 OR x = x"
    3.57 +  for x :: int
    3.58 +  by (simp add: int_or_def)
    3.59  
    3.60 -lemma int_or_minus1 [simp]: "(-1::int) OR x = -1"
    3.61 -  unfolding int_or_def by simp
    3.62 +lemma int_or_minus1 [simp]: "-1 OR x = -1"
    3.63 +  for x :: int
    3.64 +  by (simp add: int_or_def)
    3.65  
    3.66 -lemma int_or_Bits [simp]:
    3.67 -  "(x BIT b) OR (y BIT c) = (x OR y) BIT (b \<or> c)"
    3.68 -  unfolding int_or_def by simp
    3.69 +lemma int_or_Bits [simp]: "(x BIT b) OR (y BIT c) = (x OR y) BIT (b \<or> c)"
    3.70 +  by (simp add: int_or_def)
    3.71  
    3.72 -lemma int_xor_zero [simp]: "(0::int) XOR x = x"
    3.73 -  unfolding int_xor_def by simp
    3.74 +lemma int_xor_zero [simp]: "0 XOR x = x"
    3.75 +  for x :: int
    3.76 +  by (simp add: int_xor_def)
    3.77  
    3.78 -lemma int_xor_Bits [simp]:
    3.79 -  "(x BIT b) XOR (y BIT c) = (x XOR y) BIT ((b \<or> c) \<and> \<not> (b \<and> c))"
    3.80 +lemma int_xor_Bits [simp]: "(x BIT b) XOR (y BIT c) = (x XOR y) BIT ((b \<or> c) \<and> \<not> (b \<and> c))"
    3.81    unfolding int_xor_def by auto
    3.82  
    3.83 +
    3.84  subsubsection \<open>Binary destructors\<close>
    3.85  
    3.86  lemma bin_rest_NOT [simp]: "bin_rest (NOT x) = NOT (bin_rest x)"
    3.87 -  by (cases x rule: bin_exhaust, simp)
    3.88 +  by (cases x rule: bin_exhaust) simp
    3.89  
    3.90  lemma bin_last_NOT [simp]: "bin_last (NOT x) \<longleftrightarrow> \<not> bin_last x"
    3.91 -  by (cases x rule: bin_exhaust, simp)
    3.92 +  by (cases x rule: bin_exhaust) simp
    3.93  
    3.94  lemma bin_rest_AND [simp]: "bin_rest (x AND y) = bin_rest x AND bin_rest y"
    3.95 -  by (cases x rule: bin_exhaust, cases y rule: bin_exhaust, simp)
    3.96 +  by (cases x rule: bin_exhaust, cases y rule: bin_exhaust) simp
    3.97  
    3.98  lemma bin_last_AND [simp]: "bin_last (x AND y) \<longleftrightarrow> bin_last x \<and> bin_last y"
    3.99 -  by (cases x rule: bin_exhaust, cases y rule: bin_exhaust, simp)
   3.100 +  by (cases x rule: bin_exhaust, cases y rule: bin_exhaust) simp
   3.101  
   3.102  lemma bin_rest_OR [simp]: "bin_rest (x OR y) = bin_rest x OR bin_rest y"
   3.103 -  by (cases x rule: bin_exhaust, cases y rule: bin_exhaust, simp)
   3.104 +  by (cases x rule: bin_exhaust, cases y rule: bin_exhaust) simp
   3.105  
   3.106  lemma bin_last_OR [simp]: "bin_last (x OR y) \<longleftrightarrow> bin_last x \<or> bin_last y"
   3.107 -  by (cases x rule: bin_exhaust, cases y rule: bin_exhaust, simp)
   3.108 +  by (cases x rule: bin_exhaust, cases y rule: bin_exhaust) simp
   3.109  
   3.110  lemma bin_rest_XOR [simp]: "bin_rest (x XOR y) = bin_rest x XOR bin_rest y"
   3.111 -  by (cases x rule: bin_exhaust, cases y rule: bin_exhaust, simp)
   3.112 +  by (cases x rule: bin_exhaust, cases y rule: bin_exhaust) simp
   3.113  
   3.114 -lemma bin_last_XOR [simp]: "bin_last (x XOR y) \<longleftrightarrow> (bin_last x \<or> bin_last y) \<and> \<not> (bin_last x \<and> bin_last y)"
   3.115 -  by (cases x rule: bin_exhaust, cases y rule: bin_exhaust, simp)
   3.116 +lemma bin_last_XOR [simp]:
   3.117 +  "bin_last (x XOR y) \<longleftrightarrow> (bin_last x \<or> bin_last y) \<and> \<not> (bin_last x \<and> bin_last y)"
   3.118 +  by (cases x rule: bin_exhaust, cases y rule: bin_exhaust) simp
   3.119  
   3.120  lemma bin_nth_ops:
   3.121 -  "!!x y. bin_nth (x AND y) n = (bin_nth x n & bin_nth y n)"
   3.122 -  "!!x y. bin_nth (x OR y) n = (bin_nth x n | bin_nth y n)"
   3.123 -  "!!x y. bin_nth (x XOR y) n = (bin_nth x n ~= bin_nth y n)"
   3.124 -  "!!x. bin_nth (NOT x) n = (~ bin_nth x n)"
   3.125 +  "\<And>x y. bin_nth (x AND y) n \<longleftrightarrow> bin_nth x n \<and> bin_nth y n"
   3.126 +  "\<And>x y. bin_nth (x OR y) n \<longleftrightarrow> bin_nth x n \<or> bin_nth y n"
   3.127 +  "\<And>x y. bin_nth (x XOR y) n \<longleftrightarrow> bin_nth x n \<noteq> bin_nth y n"
   3.128 +  "\<And>x. bin_nth (NOT x) n \<longleftrightarrow> \<not> bin_nth x n"
   3.129    by (induct n) auto
   3.130  
   3.131 +
   3.132  subsubsection \<open>Derived properties\<close>
   3.133  
   3.134 -lemma int_xor_minus1 [simp]: "(-1::int) XOR x = NOT x"
   3.135 +lemma int_xor_minus1 [simp]: "-1 XOR x = NOT x"
   3.136 +  for x :: int
   3.137    by (auto simp add: bin_eq_iff bin_nth_ops)
   3.138  
   3.139  lemma int_xor_extra_simps [simp]:
   3.140 -  "w XOR (0::int) = w"
   3.141 -  "w XOR (-1::int) = NOT w"
   3.142 +  "w XOR 0 = w"
   3.143 +  "w XOR -1 = NOT w"
   3.144 +  for w :: int
   3.145    by (auto simp add: bin_eq_iff bin_nth_ops)
   3.146  
   3.147  lemma int_or_extra_simps [simp]:
   3.148 -  "w OR (0::int) = w"
   3.149 -  "w OR (-1::int) = -1"
   3.150 +  "w OR 0 = w"
   3.151 +  "w OR -1 = -1"
   3.152 +  for w :: int
   3.153    by (auto simp add: bin_eq_iff bin_nth_ops)
   3.154  
   3.155  lemma int_and_extra_simps [simp]:
   3.156 -  "w AND (0::int) = 0"
   3.157 -  "w AND (-1::int) = w"
   3.158 +  "w AND 0 = 0"
   3.159 +  "w AND -1 = w"
   3.160 +  for w :: int
   3.161    by (auto simp add: bin_eq_iff bin_nth_ops)
   3.162  
   3.163 -(* commutativity of the above *)
   3.164 +text \<open>Commutativity of the above.\<close>
   3.165  lemma bin_ops_comm:
   3.166 -  shows
   3.167 -  int_and_comm: "!!y::int. x AND y = y AND x" and
   3.168 -  int_or_comm:  "!!y::int. x OR y = y OR x" and
   3.169 -  int_xor_comm: "!!y::int. x XOR y = y XOR x"
   3.170 +  fixes x y :: int
   3.171 +  shows int_and_comm: "x AND y = y AND x"
   3.172 +    and int_or_comm:  "x OR y = y OR x"
   3.173 +    and int_xor_comm: "x XOR y = y XOR x"
   3.174    by (auto simp add: bin_eq_iff bin_nth_ops)
   3.175  
   3.176  lemma bin_ops_same [simp]:
   3.177 -  "(x::int) AND x = x"
   3.178 -  "(x::int) OR x = x"
   3.179 -  "(x::int) XOR x = 0"
   3.180 +  "x AND x = x"
   3.181 +  "x OR x = x"
   3.182 +  "x XOR x = 0"
   3.183 +  for x :: int
   3.184    by (auto simp add: bin_eq_iff bin_nth_ops)
   3.185  
   3.186  lemmas bin_log_esimps =
   3.187    int_and_extra_simps  int_or_extra_simps  int_xor_extra_simps
   3.188    int_and_0 int_and_m1 int_or_zero int_or_minus1 int_xor_zero int_xor_minus1
   3.189  
   3.190 -(* basic properties of logical (bit-wise) operations *)
   3.191  
   3.192 -lemma bbw_ao_absorb:
   3.193 -  "!!y::int. x AND (y OR x) = x & x OR (y AND x) = x"
   3.194 +subsubsection \<open>Basic properties of logical (bit-wise) operations\<close>
   3.195 +
   3.196 +lemma bbw_ao_absorb: "x AND (y OR x) = x \<and> x OR (y AND x) = x"
   3.197 +  for x y :: int
   3.198    by (auto simp add: bin_eq_iff bin_nth_ops)
   3.199  
   3.200  lemma bbw_ao_absorbs_other:
   3.201 -  "x AND (x OR y) = x \<and> (y AND x) OR x = (x::int)"
   3.202 -  "(y OR x) AND x = x \<and> x OR (x AND y) = (x::int)"
   3.203 -  "(x OR y) AND x = x \<and> (x AND y) OR x = (x::int)"
   3.204 +  "x AND (x OR y) = x \<and> (y AND x) OR x = x"
   3.205 +  "(y OR x) AND x = x \<and> x OR (x AND y) = x"
   3.206 +  "(x OR y) AND x = x \<and> (x AND y) OR x = x"
   3.207 +  for x y :: int
   3.208    by (auto simp add: bin_eq_iff bin_nth_ops)
   3.209  
   3.210  lemmas bbw_ao_absorbs [simp] = bbw_ao_absorb bbw_ao_absorbs_other
   3.211  
   3.212 -lemma int_xor_not:
   3.213 -  "!!y::int. (NOT x) XOR y = NOT (x XOR y) &
   3.214 -        x XOR (NOT y) = NOT (x XOR y)"
   3.215 +lemma int_xor_not: "(NOT x) XOR y = NOT (x XOR y) \<and> x XOR (NOT y) = NOT (x XOR y)"
   3.216 +  for x y :: int
   3.217    by (auto simp add: bin_eq_iff bin_nth_ops)
   3.218  
   3.219 -lemma int_and_assoc:
   3.220 -  "(x AND y) AND (z::int) = x AND (y AND z)"
   3.221 +lemma int_and_assoc: "(x AND y) AND z = x AND (y AND z)"
   3.222 +  for x y z :: int
   3.223    by (auto simp add: bin_eq_iff bin_nth_ops)
   3.224  
   3.225 -lemma int_or_assoc:
   3.226 -  "(x OR y) OR (z::int) = x OR (y OR z)"
   3.227 +lemma int_or_assoc: "(x OR y) OR z = x OR (y OR z)"
   3.228 +  for x y z :: int
   3.229    by (auto simp add: bin_eq_iff bin_nth_ops)
   3.230  
   3.231 -lemma int_xor_assoc:
   3.232 -  "(x XOR y) XOR (z::int) = x XOR (y XOR z)"
   3.233 +lemma int_xor_assoc: "(x XOR y) XOR z = x XOR (y XOR z)"
   3.234 +  for x y z :: int
   3.235    by (auto simp add: bin_eq_iff bin_nth_ops)
   3.236  
   3.237  lemmas bbw_assocs = int_and_assoc int_or_assoc int_xor_assoc
   3.238  
   3.239  (* BH: Why are these declared as simp rules??? *)
   3.240  lemma bbw_lcs [simp]:
   3.241 -  "(y::int) AND (x AND z) = x AND (y AND z)"
   3.242 -  "(y::int) OR (x OR z) = x OR (y OR z)"
   3.243 -  "(y::int) XOR (x XOR z) = x XOR (y XOR z)"
   3.244 +  "y AND (x AND z) = x AND (y AND z)"
   3.245 +  "y OR (x OR z) = x OR (y OR z)"
   3.246 +  "y XOR (x XOR z) = x XOR (y XOR z)"
   3.247 +  for x y :: int
   3.248    by (auto simp add: bin_eq_iff bin_nth_ops)
   3.249  
   3.250  lemma bbw_not_dist:
   3.251 -  "!!y::int. NOT (x OR y) = (NOT x) AND (NOT y)"
   3.252 -  "!!y::int. NOT (x AND y) = (NOT x) OR (NOT y)"
   3.253 +  "NOT (x OR y) = (NOT x) AND (NOT y)"
   3.254 +  "NOT (x AND y) = (NOT x) OR (NOT y)"
   3.255 +  for x y :: int
   3.256    by (auto simp add: bin_eq_iff bin_nth_ops)
   3.257  
   3.258 -lemma bbw_oa_dist:
   3.259 -  "!!y z::int. (x AND y) OR z =
   3.260 -          (x OR z) AND (y OR z)"
   3.261 +lemma bbw_oa_dist: "(x AND y) OR z = (x OR z) AND (y OR z)"
   3.262 +  for x y z :: int
   3.263    by (auto simp add: bin_eq_iff bin_nth_ops)
   3.264  
   3.265 -lemma bbw_ao_dist:
   3.266 -  "!!y z::int. (x OR y) AND z =
   3.267 -          (x AND z) OR (y AND z)"
   3.268 +lemma bbw_ao_dist: "(x OR y) AND z = (x AND z) OR (y AND z)"
   3.269 +  for x y z :: int
   3.270    by (auto simp add: bin_eq_iff bin_nth_ops)
   3.271  
   3.272  (*
   3.273 @@ -218,10 +227,10 @@
   3.274  declare bin_ops_comm [simp] bbw_assocs [simp]
   3.275  *)
   3.276  
   3.277 +
   3.278  subsubsection \<open>Simplification with numerals\<close>
   3.279  
   3.280 -text \<open>Cases for \<open>0\<close> and \<open>-1\<close> are already covered by
   3.281 -  other simp rules.\<close>
   3.282 +text \<open>Cases for \<open>0\<close> and \<open>-1\<close> are already covered by other simp rules.\<close>
   3.283  
   3.284  lemma bin_rl_eqI: "\<lbrakk>bin_rest x = bin_rest y; bin_last x = bin_last y\<rbrakk> \<Longrightarrow> x = y"
   3.285    by (metis (mono_tags) BIT_eq_iff bin_ex_rl bin_last_BIT bin_rest_BIT)
   3.286 @@ -234,8 +243,8 @@
   3.287    "bin_last (- numeral (Num.BitM w))"
   3.288    by (simp only: BIT_bin_simps [symmetric] bin_last_BIT)
   3.289  
   3.290 -text \<open>FIXME: The rule sets below are very large (24 rules for each
   3.291 -  operator). Is there a simpler way to do this?\<close>
   3.292 +(* FIXME: The rule sets below are very large (24 rules for each
   3.293 +  operator). Is there a simpler way to do this? *)
   3.294  
   3.295  lemma int_and_numerals [simp]:
   3.296    "numeral (Num.Bit0 x) AND numeral (Num.Bit0 y) = (numeral x AND numeral y) BIT False"
   3.297 @@ -262,7 +271,7 @@
   3.298    "numeral (Num.Bit1 x) AND (1::int) = 1"
   3.299    "- numeral (Num.Bit0 x) AND (1::int) = 0"
   3.300    "- numeral (Num.Bit1 x) AND (1::int) = 1"
   3.301 -  by (rule bin_rl_eqI, simp, simp)+
   3.302 +  by (rule bin_rl_eqI; simp)+
   3.303  
   3.304  lemma int_or_numerals [simp]:
   3.305    "numeral (Num.Bit0 x) OR numeral (Num.Bit0 y) = (numeral x OR numeral y) BIT False"
   3.306 @@ -289,7 +298,7 @@
   3.307    "numeral (Num.Bit1 x) OR (1::int) = numeral (Num.Bit1 x)"
   3.308    "- numeral (Num.Bit0 x) OR (1::int) = - numeral (Num.BitM x)"
   3.309    "- numeral (Num.Bit1 x) OR (1::int) = - numeral (Num.Bit1 x)"
   3.310 -  by (rule bin_rl_eqI, simp, simp)+
   3.311 +  by (rule bin_rl_eqI; simp)+
   3.312  
   3.313  lemma int_xor_numerals [simp]:
   3.314    "numeral (Num.Bit0 x) XOR numeral (Num.Bit0 y) = (numeral x XOR numeral y) BIT False"
   3.315 @@ -316,12 +325,12 @@
   3.316    "numeral (Num.Bit1 x) XOR (1::int) = numeral (Num.Bit0 x)"
   3.317    "- numeral (Num.Bit0 x) XOR (1::int) = - numeral (Num.BitM x)"
   3.318    "- numeral (Num.Bit1 x) XOR (1::int) = - numeral (Num.Bit0 (x + Num.One))"
   3.319 -  by (rule bin_rl_eqI, simp, simp)+
   3.320 +  by (rule bin_rl_eqI; simp)+
   3.321 +
   3.322  
   3.323  subsubsection \<open>Interactions with arithmetic\<close>
   3.324  
   3.325 -lemma plus_and_or [rule_format]:
   3.326 -  "ALL y::int. (x AND y) + (x OR y) = x + y"
   3.327 +lemma plus_and_or [rule_format]: "\<forall>y::int. (x AND y) + (x OR y) = x + y"
   3.328    apply (induct x rule: bin_induct)
   3.329      apply clarsimp
   3.330     apply clarsimp
   3.331 @@ -334,8 +343,8 @@
   3.332    apply simp
   3.333    done
   3.334  
   3.335 -lemma le_int_or:
   3.336 -  "bin_sign (y::int) = 0 ==> x <= x OR y"
   3.337 +lemma le_int_or: "bin_sign y = 0 \<Longrightarrow> x \<le> x OR y"
   3.338 +  for x y :: int
   3.339    apply (induct y arbitrary: x rule: bin_induct)
   3.340      apply clarsimp
   3.341     apply clarsimp
   3.342 @@ -348,8 +357,7 @@
   3.343  lemmas int_and_le =
   3.344    xtrans(3) [OF bbw_ao_absorbs (2) [THEN conjunct2, symmetric] le_int_or]
   3.345  
   3.346 -(* interaction between bit-wise and arithmetic *)
   3.347 -(* good example of bin_induction *)
   3.348 +text \<open>Interaction between bit-wise and arithmetic: good example of \<open>bin_induction\<close>.\<close>
   3.349  lemma bin_add_not: "x + NOT x = (-1::int)"
   3.350    apply (induct x rule: bin_induct)
   3.351      apply clarsimp
   3.352 @@ -357,91 +365,77 @@
   3.353    apply (case_tac bit, auto)
   3.354    done
   3.355  
   3.356 +
   3.357  subsubsection \<open>Truncating results of bit-wise operations\<close>
   3.358  
   3.359  lemma bin_trunc_ao:
   3.360 -  "!!x y. (bintrunc n x) AND (bintrunc n y) = bintrunc n (x AND y)"
   3.361 -  "!!x y. (bintrunc n x) OR (bintrunc n y) = bintrunc n (x OR y)"
   3.362 +  "bintrunc n x AND bintrunc n y = bintrunc n (x AND y)"
   3.363 +  "bintrunc n x OR bintrunc n y = bintrunc n (x OR y)"
   3.364    by (auto simp add: bin_eq_iff bin_nth_ops nth_bintr)
   3.365  
   3.366 -lemma bin_trunc_xor:
   3.367 -  "!!x y. bintrunc n (bintrunc n x XOR bintrunc n y) =
   3.368 -          bintrunc n (x XOR y)"
   3.369 +lemma bin_trunc_xor: "bintrunc n (bintrunc n x XOR bintrunc n y) = bintrunc n (x XOR y)"
   3.370    by (auto simp add: bin_eq_iff bin_nth_ops nth_bintr)
   3.371  
   3.372 -lemma bin_trunc_not:
   3.373 -  "!!x. bintrunc n (NOT (bintrunc n x)) = bintrunc n (NOT x)"
   3.374 +lemma bin_trunc_not: "bintrunc n (NOT (bintrunc n x)) = bintrunc n (NOT x)"
   3.375    by (auto simp add: bin_eq_iff bin_nth_ops nth_bintr)
   3.376  
   3.377 -(* want theorems of the form of bin_trunc_xor *)
   3.378 -lemma bintr_bintr_i:
   3.379 -  "x = bintrunc n y ==> bintrunc n x = bintrunc n y"
   3.380 +text \<open>Want theorems of the form of \<open>bin_trunc_xor\<close>.\<close>
   3.381 +lemma bintr_bintr_i: "x = bintrunc n y \<Longrightarrow> bintrunc n x = bintrunc n y"
   3.382    by auto
   3.383  
   3.384  lemmas bin_trunc_and = bin_trunc_ao(1) [THEN bintr_bintr_i]
   3.385  lemmas bin_trunc_or = bin_trunc_ao(2) [THEN bintr_bintr_i]
   3.386  
   3.387 +
   3.388  subsection \<open>Setting and clearing bits\<close>
   3.389  
   3.390 -(** nth bit, set/clear **)
   3.391 +text \<open>nth bit, set/clear\<close>
   3.392  
   3.393 -primrec
   3.394 -  bin_sc :: "nat => bool => int => int"
   3.395 -where
   3.396 -  Z: "bin_sc 0 b w = bin_rest w BIT b"
   3.397 +primrec bin_sc :: "nat \<Rightarrow> bool \<Rightarrow> int \<Rightarrow> int"
   3.398 +  where
   3.399 +    Z: "bin_sc 0 b w = bin_rest w BIT b"
   3.400    | Suc: "bin_sc (Suc n) b w = bin_sc n b (bin_rest w) BIT bin_last w"
   3.401  
   3.402 -lemma bin_nth_sc [simp]:
   3.403 -  "bin_nth (bin_sc n b w) n \<longleftrightarrow> b"
   3.404 +lemma bin_nth_sc [simp]: "bin_nth (bin_sc n b w) n \<longleftrightarrow> b"
   3.405    by (induct n arbitrary: w) auto
   3.406  
   3.407 -lemma bin_sc_sc_same [simp]:
   3.408 -  "bin_sc n c (bin_sc n b w) = bin_sc n c w"
   3.409 +lemma bin_sc_sc_same [simp]: "bin_sc n c (bin_sc n b w) = bin_sc n c w"
   3.410    by (induct n arbitrary: w) auto
   3.411  
   3.412 -lemma bin_sc_sc_diff:
   3.413 -  "m ~= n ==>
   3.414 -    bin_sc m c (bin_sc n b w) = bin_sc n b (bin_sc m c w)"
   3.415 +lemma bin_sc_sc_diff: "m \<noteq> n \<Longrightarrow> bin_sc m c (bin_sc n b w) = bin_sc n b (bin_sc m c w)"
   3.416    apply (induct n arbitrary: w m)
   3.417     apply (case_tac [!] m)
   3.418       apply auto
   3.419    done
   3.420  
   3.421 -lemma bin_nth_sc_gen:
   3.422 -  "bin_nth (bin_sc n b w) m = (if m = n then b else bin_nth w m)"
   3.423 +lemma bin_nth_sc_gen: "bin_nth (bin_sc n b w) m = (if m = n then b else bin_nth w m)"
   3.424    by (induct n arbitrary: w m) (case_tac [!] m, auto)
   3.425  
   3.426 -lemma bin_sc_nth [simp]:
   3.427 -  "(bin_sc n (bin_nth w n) w) = w"
   3.428 +lemma bin_sc_nth [simp]: "bin_sc n (bin_nth w n) w = w"
   3.429    by (induct n arbitrary: w) auto
   3.430  
   3.431 -lemma bin_sign_sc [simp]:
   3.432 -  "bin_sign (bin_sc n b w) = bin_sign w"
   3.433 +lemma bin_sign_sc [simp]: "bin_sign (bin_sc n b w) = bin_sign w"
   3.434    by (induct n arbitrary: w) auto
   3.435  
   3.436 -lemma bin_sc_bintr [simp]:
   3.437 -  "bintrunc m (bin_sc n x (bintrunc m (w))) = bintrunc m (bin_sc n x w)"
   3.438 +lemma bin_sc_bintr [simp]: "bintrunc m (bin_sc n x (bintrunc m (w))) = bintrunc m (bin_sc n x w)"
   3.439    apply (induct n arbitrary: w m)
   3.440     apply (case_tac [!] w rule: bin_exhaust)
   3.441     apply (case_tac [!] m, auto)
   3.442    done
   3.443  
   3.444 -lemma bin_clr_le:
   3.445 -  "bin_sc n False w <= w"
   3.446 +lemma bin_clr_le: "bin_sc n False w \<le> w"
   3.447    apply (induct n arbitrary: w)
   3.448     apply (case_tac [!] w rule: bin_exhaust)
   3.449     apply (auto simp: le_Bits)
   3.450    done
   3.451  
   3.452 -lemma bin_set_ge:
   3.453 -  "bin_sc n True w >= w"
   3.454 +lemma bin_set_ge: "bin_sc n True w \<ge> w"
   3.455    apply (induct n arbitrary: w)
   3.456     apply (case_tac [!] w rule: bin_exhaust)
   3.457     apply (auto simp: le_Bits)
   3.458    done
   3.459  
   3.460 -lemma bintr_bin_clr_le:
   3.461 -  "bintrunc n (bin_sc m False w) <= bintrunc n w"
   3.462 +lemma bintr_bin_clr_le: "bintrunc n (bin_sc m False w) \<le> bintrunc n w"
   3.463    apply (induct n arbitrary: w m)
   3.464     apply simp
   3.465    apply (case_tac w rule: bin_exhaust)
   3.466 @@ -449,8 +443,7 @@
   3.467     apply (auto simp: le_Bits)
   3.468    done
   3.469  
   3.470 -lemma bintr_bin_set_ge:
   3.471 -  "bintrunc n (bin_sc m True w) >= bintrunc n w"
   3.472 +lemma bintr_bin_set_ge: "bintrunc n (bin_sc m True w) \<ge> bintrunc n w"
   3.473    apply (induct n arbitrary: w m)
   3.474     apply simp
   3.475    apply (case_tac w rule: bin_exhaust)
   3.476 @@ -466,8 +459,7 @@
   3.477  
   3.478  lemmas bin_sc_simps = bin_sc.Z bin_sc.Suc bin_sc_TM bin_sc_FP
   3.479  
   3.480 -lemma bin_sc_minus:
   3.481 -  "0 < n ==> bin_sc (Suc (n - 1)) b w = bin_sc n b w"
   3.482 +lemma bin_sc_minus: "0 < n \<Longrightarrow> bin_sc (Suc (n - 1)) b w = bin_sc n b w"
   3.483    by auto
   3.484  
   3.485  lemmas bin_sc_Suc_minus =
   3.486 @@ -482,40 +474,35 @@
   3.487  subsection \<open>Splitting and concatenation\<close>
   3.488  
   3.489  definition bin_rcat :: "nat \<Rightarrow> int list \<Rightarrow> int"
   3.490 -where
   3.491 -  "bin_rcat n = foldl (\<lambda>u v. bin_cat u n v) 0"
   3.492 +  where "bin_rcat n = foldl (\<lambda>u v. bin_cat u n v) 0"
   3.493  
   3.494  fun bin_rsplit_aux :: "nat \<Rightarrow> nat \<Rightarrow> int \<Rightarrow> int list \<Rightarrow> int list"
   3.495 -where
   3.496 -  "bin_rsplit_aux n m c bs =
   3.497 -    (if m = 0 | n = 0 then bs else
   3.498 +  where "bin_rsplit_aux n m c bs =
   3.499 +    (if m = 0 \<or> n = 0 then bs
   3.500 +     else
   3.501        let (a, b) = bin_split n c
   3.502        in bin_rsplit_aux n (m - n) a (b # bs))"
   3.503  
   3.504  definition bin_rsplit :: "nat \<Rightarrow> nat \<times> int \<Rightarrow> int list"
   3.505 -where
   3.506 -  "bin_rsplit n w = bin_rsplit_aux n (fst w) (snd w) []"
   3.507 +  where "bin_rsplit n w = bin_rsplit_aux n (fst w) (snd w) []"
   3.508  
   3.509  fun bin_rsplitl_aux :: "nat \<Rightarrow> nat \<Rightarrow> int \<Rightarrow> int list \<Rightarrow> int list"
   3.510 -where
   3.511 -  "bin_rsplitl_aux n m c bs =
   3.512 -    (if m = 0 | n = 0 then bs else
   3.513 +  where "bin_rsplitl_aux n m c bs =
   3.514 +    (if m = 0 \<or> n = 0 then bs
   3.515 +     else
   3.516        let (a, b) = bin_split (min m n) c
   3.517        in bin_rsplitl_aux n (m - n) a (b # bs))"
   3.518  
   3.519  definition bin_rsplitl :: "nat \<Rightarrow> nat \<times> int \<Rightarrow> int list"
   3.520 -where
   3.521 -  "bin_rsplitl n w = bin_rsplitl_aux n (fst w) (snd w) []"
   3.522 +  where "bin_rsplitl n w = bin_rsplitl_aux n (fst w) (snd w) []"
   3.523  
   3.524  declare bin_rsplit_aux.simps [simp del]
   3.525  declare bin_rsplitl_aux.simps [simp del]
   3.526  
   3.527 -lemma bin_sign_cat:
   3.528 -  "bin_sign (bin_cat x n y) = bin_sign x"
   3.529 +lemma bin_sign_cat: "bin_sign (bin_cat x n y) = bin_sign x"
   3.530    by (induct n arbitrary: y) auto
   3.531  
   3.532 -lemma bin_cat_Suc_Bit:
   3.533 -  "bin_cat w (Suc n) (v BIT b) = bin_cat w n v BIT b"
   3.534 +lemma bin_cat_Suc_Bit: "bin_cat w (Suc n) (v BIT b) = bin_cat w n v BIT b"
   3.535    by auto
   3.536  
   3.537  lemma bin_nth_cat:
   3.538 @@ -527,9 +514,9 @@
   3.539    done
   3.540  
   3.541  lemma bin_nth_split:
   3.542 -  "bin_split n c = (a, b) ==>
   3.543 -    (ALL k. bin_nth a k = bin_nth c (n + k)) &
   3.544 -    (ALL k. bin_nth b k = (k < n & bin_nth c k))"
   3.545 +  "bin_split n c = (a, b) \<Longrightarrow>
   3.546 +    (\<forall>k. bin_nth a k = bin_nth c (n + k)) \<and>
   3.547 +    (\<forall>k. bin_nth b k = (k < n \<and> bin_nth c k))"
   3.548    apply (induct n arbitrary: b c)
   3.549     apply clarsimp
   3.550    apply (clarsimp simp: Let_def split: prod.split_asm)
   3.551 @@ -537,45 +524,38 @@
   3.552    apply auto
   3.553    done
   3.554  
   3.555 -lemma bin_cat_assoc:
   3.556 -  "bin_cat (bin_cat x m y) n z = bin_cat x (m + n) (bin_cat y n z)"
   3.557 +lemma bin_cat_assoc: "bin_cat (bin_cat x m y) n z = bin_cat x (m + n) (bin_cat y n z)"
   3.558    by (induct n arbitrary: z) auto
   3.559  
   3.560 -lemma bin_cat_assoc_sym:
   3.561 -  "bin_cat x m (bin_cat y n z) = bin_cat (bin_cat x (m - n) y) (min m n) z"
   3.562 -  apply (induct n arbitrary: z m, clarsimp)
   3.563 +lemma bin_cat_assoc_sym: "bin_cat x m (bin_cat y n z) = bin_cat (bin_cat x (m - n) y) (min m n) z"
   3.564 +  apply (induct n arbitrary: z m)
   3.565 +   apply clarsimp
   3.566    apply (case_tac m, auto)
   3.567    done
   3.568  
   3.569  lemma bin_cat_zero [simp]: "bin_cat 0 n w = bintrunc n w"
   3.570    by (induct n arbitrary: w) auto
   3.571  
   3.572 -lemma bintr_cat1:
   3.573 -  "bintrunc (k + n) (bin_cat a n b) = bin_cat (bintrunc k a) n b"
   3.574 +lemma bintr_cat1: "bintrunc (k + n) (bin_cat a n b) = bin_cat (bintrunc k a) n b"
   3.575    by (induct n arbitrary: b) auto
   3.576  
   3.577  lemma bintr_cat: "bintrunc m (bin_cat a n b) =
   3.578      bin_cat (bintrunc (m - n) a) n (bintrunc (min m n) b)"
   3.579    by (rule bin_eqI) (auto simp: bin_nth_cat nth_bintr)
   3.580  
   3.581 -lemma bintr_cat_same [simp]:
   3.582 -  "bintrunc n (bin_cat a n b) = bintrunc n b"
   3.583 +lemma bintr_cat_same [simp]: "bintrunc n (bin_cat a n b) = bintrunc n b"
   3.584    by (auto simp add : bintr_cat)
   3.585  
   3.586 -lemma cat_bintr [simp]:
   3.587 -  "bin_cat a n (bintrunc n b) = bin_cat a n b"
   3.588 +lemma cat_bintr [simp]: "bin_cat a n (bintrunc n b) = bin_cat a n b"
   3.589    by (induct n arbitrary: b) auto
   3.590  
   3.591 -lemma split_bintrunc:
   3.592 -  "bin_split n c = (a, b) ==> b = bintrunc n c"
   3.593 +lemma split_bintrunc: "bin_split n c = (a, b) \<Longrightarrow> b = bintrunc n c"
   3.594    by (induct n arbitrary: b c) (auto simp: Let_def split: prod.split_asm)
   3.595  
   3.596 -lemma bin_cat_split:
   3.597 -  "bin_split n w = (u, v) ==> w = bin_cat u n v"
   3.598 +lemma bin_cat_split: "bin_split n w = (u, v) \<Longrightarrow> w = bin_cat u n v"
   3.599    by (induct n arbitrary: v w) (auto simp: Let_def split: prod.split_asm)
   3.600  
   3.601 -lemma bin_split_cat:
   3.602 -  "bin_split n (bin_cat v n w) = (v, bintrunc n w)"
   3.603 +lemma bin_split_cat: "bin_split n (bin_cat v n w) = (v, bintrunc n w)"
   3.604    by (induct n arbitrary: w) auto
   3.605  
   3.606  lemma bin_split_zero [simp]: "bin_split n 0 = (0, 0)"
   3.607 @@ -586,7 +566,7 @@
   3.608    by (induct n) auto
   3.609  
   3.610  lemma bin_split_trunc:
   3.611 -  "bin_split (min m n) c = (a, b) ==>
   3.612 +  "bin_split (min m n) c = (a, b) \<Longrightarrow>
   3.613      bin_split n (bintrunc m c) = (bintrunc (m - n) a, b)"
   3.614    apply (induct n arbitrary: m b c, clarsimp)
   3.615    apply (simp add: bin_rest_trunc Let_def split: prod.split_asm)
   3.616 @@ -595,7 +575,7 @@
   3.617    done
   3.618  
   3.619  lemma bin_split_trunc1:
   3.620 -  "bin_split n c = (a, b) ==>
   3.621 +  "bin_split n c = (a, b) \<Longrightarrow>
   3.622      bin_split n (bintrunc m c) = (bintrunc (m - n) a, bintrunc m b)"
   3.623    apply (induct n arbitrary: m b c, clarsimp)
   3.624    apply (simp add: bin_rest_trunc Let_def split: prod.split_asm)
   3.625 @@ -603,25 +583,25 @@
   3.626     apply (auto simp: Let_def split: prod.split_asm)
   3.627    done
   3.628  
   3.629 -lemma bin_cat_num:
   3.630 -  "bin_cat a n b = a * 2 ^ n + bintrunc n b"
   3.631 -  apply (induct n arbitrary: b, clarsimp)
   3.632 +lemma bin_cat_num: "bin_cat a n b = a * 2 ^ n + bintrunc n b"
   3.633 +  apply (induct n arbitrary: b)
   3.634 +   apply clarsimp
   3.635    apply (simp add: Bit_def)
   3.636    done
   3.637  
   3.638 -lemma bin_split_num:
   3.639 -  "bin_split n b = (b div 2 ^ n, b mod 2 ^ n)"
   3.640 -  apply (induct n arbitrary: b, simp)
   3.641 +lemma bin_split_num: "bin_split n b = (b div 2 ^ n, b mod 2 ^ n)"
   3.642 +  apply (induct n arbitrary: b)
   3.643 +   apply simp
   3.644    apply (simp add: bin_rest_def zdiv_zmult2_eq)
   3.645    apply (case_tac b rule: bin_exhaust)
   3.646    apply simp
   3.647    apply (simp add: Bit_def mod_mult_mult1 p1mod22k)
   3.648    done
   3.649  
   3.650 +
   3.651  subsection \<open>Miscellaneous lemmas\<close>
   3.652  
   3.653 -lemma nth_2p_bin:
   3.654 -  "bin_nth (2 ^ n) m = (m = n)"
   3.655 +lemma nth_2p_bin: "bin_nth (2 ^ n) m = (m = n)"
   3.656    apply (induct n arbitrary: m)
   3.657     apply clarsimp
   3.658     apply safe
   3.659 @@ -629,18 +609,14 @@
   3.660      apply (auto simp: Bit_B0_2t [symmetric])
   3.661    done
   3.662  
   3.663 -(* for use when simplifying with bin_nth_Bit *)
   3.664 -
   3.665 -lemma ex_eq_or:
   3.666 -  "(EX m. n = Suc m & (m = k | P m)) = (n = Suc k | (EX m. n = Suc m & P m))"
   3.667 +(*for use when simplifying with bin_nth_Bit*)
   3.668 +lemma ex_eq_or: "(\<exists>m. n = Suc m \<and> (m = k \<or> P m)) \<longleftrightarrow> n = Suc k \<or> (\<exists>m. n = Suc m \<and> P m)"
   3.669    by auto
   3.670  
   3.671  lemma power_BIT: "2 ^ (Suc n) - 1 = (2 ^ n - 1) BIT True"
   3.672 -  unfolding Bit_B1
   3.673 -  by (induct n) simp_all
   3.674 +  by (induct n) (simp_all add: Bit_B1)
   3.675  
   3.676 -lemma mod_BIT:
   3.677 -  "bin BIT bit mod 2 ^ Suc n = (bin mod 2 ^ n) BIT bit"
   3.678 +lemma mod_BIT: "bin BIT bit mod 2 ^ Suc n = (bin mod 2 ^ n) BIT bit"
   3.679  proof -
   3.680    have "2 * (bin mod 2 ^ n) + 1 = (2 * bin mod 2 ^ Suc n) + 1"
   3.681      by (simp add: mod_mult_mult1)
   3.682 @@ -652,9 +628,8 @@
   3.683      by (auto simp add: Bit_def)
   3.684  qed
   3.685  
   3.686 -lemma AND_mod:
   3.687 -  fixes x :: int
   3.688 -  shows "x AND 2 ^ n - 1 = x mod 2 ^ n"
   3.689 +lemma AND_mod: "x AND 2 ^ n - 1 = x mod 2 ^ n"
   3.690 +  for x :: int
   3.691  proof (induct x arbitrary: n rule: bin_induct)
   3.692    case 1
   3.693    then show ?case
     4.1 --- a/src/HOL/Word/Bool_List_Representation.thy	Sun Dec 03 13:22:09 2017 +0100
     4.2 +++ b/src/HOL/Word/Bool_List_Representation.thy	Sun Dec 03 18:53:49 2017 +0100
     4.3 @@ -117,7 +117,7 @@
     4.4      bin_to_bl_aux n (numeral (Num.Bit1 w)) bl = bin_to_bl_aux (n - 1) (numeral w) (True # bl)"
     4.5    by (cases n) auto
     4.6  
     4.7 -text \<open>Link between bin and bool list.\<close>
     4.8 +text \<open>Link between \<open>bin\<close> and \<open>bool list\<close>.\<close>
     4.9  
    4.10  lemma bl_to_bin_aux_append: "bl_to_bin_aux (bs @ cs) w = bl_to_bin_aux cs (bl_to_bin_aux bs w)"
    4.11    by (induct bs arbitrary: w) auto
    4.12 @@ -238,7 +238,7 @@
    4.13  
    4.14  lemma bin_nth_of_bl_aux:
    4.15    "bin_nth (bl_to_bin_aux bl w) n =
    4.16 -    (n < size bl \<and> rev bl ! n | n \<ge> length bl \<and> bin_nth w (n - size bl))"
    4.17 +    (n < size bl \<and> rev bl ! n \<or> n \<ge> length bl \<and> bin_nth w (n - size bl))"
    4.18    apply (induct bl arbitrary: w)
    4.19     apply clarsimp
    4.20    apply clarsimp
    4.21 @@ -298,8 +298,9 @@
    4.22    case Nil
    4.23    then show ?case by simp
    4.24  next
    4.25 -  case (Cons b bs) with bl_to_bin_lt2p_aux[where w=1]
    4.26 -  show ?case unfolding bl_to_bin_def by simp
    4.27 +  case (Cons b bs)
    4.28 +  with bl_to_bin_lt2p_aux[where w=1] show ?case
    4.29 +    by (simp add: bl_to_bin_def)
    4.30  qed
    4.31  
    4.32  lemma bl_to_bin_lt2p: "bl_to_bin bs < 2 ^ length bs"
    4.33 @@ -509,11 +510,11 @@
    4.34  lemma length_takefill [simp]: "length (takefill fill n l) = n"
    4.35    by (simp add: takefill_alt)
    4.36  
    4.37 -lemma take_takefill': "\<And>w n.  n = k + m \<Longrightarrow> take k (takefill fill n w) = takefill fill k w"
    4.38 -  by (induct k) (auto split: list.split)
    4.39 +lemma take_takefill': "n = k + m \<Longrightarrow> take k (takefill fill n w) = takefill fill k w"
    4.40 +  by (induct k arbitrary: w n) (auto split: list.split)
    4.41  
    4.42 -lemma drop_takefill: "\<And>w. drop k (takefill fill (m + k) w) = takefill fill m (drop k w)"
    4.43 -  by (induct k) (auto split: list.split)
    4.44 +lemma drop_takefill: "drop k (takefill fill (m + k) w) = takefill fill m (drop k w)"
    4.45 +  by (induct k arbitrary: w) (auto split: list.split)
    4.46  
    4.47  lemma takefill_le [simp]: "m \<le> n \<Longrightarrow> takefill x m (takefill x n l) = takefill x m l"
    4.48    by (auto simp: le_iff_add takefill_le')
    4.49 @@ -715,7 +716,7 @@
    4.50    done
    4.51  
    4.52  lemma rbl_add_take2:
    4.53 -  "length blb >= length bla ==> rbl_add bla (take (length bla) blb) = rbl_add bla blb"
    4.54 +  "length blb \<ge> length bla \<Longrightarrow> rbl_add bla (take (length bla) blb) = rbl_add bla blb"
    4.55    apply (induct bla arbitrary: blb)
    4.56     apply simp
    4.57    apply clarsimp
    4.58 @@ -1023,7 +1024,8 @@
    4.59      with \<open>length bs = length cs\<close> show ?thesis by simp
    4.60    next
    4.61      case False
    4.62 -    from "1.hyps" \<open>m \<noteq> 0\<close> \<open>n \<noteq> 0\<close> have hyp: "\<And>v bs. length bs = Suc (length cs) \<Longrightarrow>
    4.63 +    from "1.hyps" \<open>m \<noteq> 0\<close> \<open>n \<noteq> 0\<close>
    4.64 +    have hyp: "\<And>v bs. length bs = Suc (length cs) \<Longrightarrow>
    4.65        length (bin_rsplit_aux n (m - n) v bs) =
    4.66        length (bin_rsplit_aux n (m - n) (fst (bin_split n w)) (snd (bin_split n w) # cs))"
    4.67        by auto
     5.1 --- a/src/HOL/Word/Misc_Typedef.thy	Sun Dec 03 13:22:09 2017 +0100
     5.2 +++ b/src/HOL/Word/Misc_Typedef.thy	Sun Dec 03 18:53:49 2017 +0100
     5.3 @@ -7,19 +7,17 @@
     5.4  section \<open>Type Definition Theorems\<close>
     5.5  
     5.6  theory Misc_Typedef
     5.7 -imports Main
     5.8 +  imports Main
     5.9  begin
    5.10  
    5.11  section "More lemmas about normal type definitions"
    5.12  
    5.13 -lemma
    5.14 -  tdD1: "type_definition Rep Abs A \<Longrightarrow> \<forall>x. Rep x \<in> A" and
    5.15 -  tdD2: "type_definition Rep Abs A \<Longrightarrow> \<forall>x. Abs (Rep x) = x" and
    5.16 -  tdD3: "type_definition Rep Abs A \<Longrightarrow> \<forall>y. y \<in> A \<longrightarrow> Rep (Abs y) = y"
    5.17 +lemma tdD1: "type_definition Rep Abs A \<Longrightarrow> \<forall>x. Rep x \<in> A"
    5.18 +  and tdD2: "type_definition Rep Abs A \<Longrightarrow> \<forall>x. Abs (Rep x) = x"
    5.19 +  and tdD3: "type_definition Rep Abs A \<Longrightarrow> \<forall>y. y \<in> A \<longrightarrow> Rep (Abs y) = y"
    5.20    by (auto simp: type_definition_def)
    5.21  
    5.22 -lemma td_nat_int:
    5.23 -  "type_definition int nat (Collect (op <= 0))"
    5.24 +lemma td_nat_int: "type_definition int nat (Collect (op \<le> 0))"
    5.25    unfolding type_definition_def by auto
    5.26  
    5.27  context type_definition
    5.28 @@ -27,39 +25,33 @@
    5.29  
    5.30  declare Rep [iff] Rep_inverse [simp] Rep_inject [simp]
    5.31  
    5.32 -lemma Abs_eqD: "Abs x = Abs y ==> x \<in> A ==> y \<in> A ==> x = y"
    5.33 +lemma Abs_eqD: "Abs x = Abs y \<Longrightarrow> x \<in> A \<Longrightarrow> y \<in> A \<Longrightarrow> x = y"
    5.34    by (simp add: Abs_inject)
    5.35  
    5.36 -lemma Abs_inverse':
    5.37 -  "r : A ==> Abs r = a ==> Rep a = r"
    5.38 +lemma Abs_inverse': "r \<in> A \<Longrightarrow> Abs r = a \<Longrightarrow> Rep a = r"
    5.39    by (safe elim!: Abs_inverse)
    5.40  
    5.41 -lemma Rep_comp_inverse:
    5.42 -  "Rep \<circ> f = g ==> Abs \<circ> g = f"
    5.43 +lemma Rep_comp_inverse: "Rep \<circ> f = g \<Longrightarrow> Abs \<circ> g = f"
    5.44    using Rep_inverse by auto
    5.45  
    5.46 -lemma Rep_eqD [elim!]: "Rep x = Rep y ==> x = y"
    5.47 +lemma Rep_eqD [elim!]: "Rep x = Rep y \<Longrightarrow> x = y"
    5.48    by simp
    5.49  
    5.50 -lemma Rep_inverse': "Rep a = r ==> Abs r = a"
    5.51 +lemma Rep_inverse': "Rep a = r \<Longrightarrow> Abs r = a"
    5.52    by (safe intro!: Rep_inverse)
    5.53  
    5.54 -lemma comp_Abs_inverse:
    5.55 -  "f \<circ> Abs = g ==> g \<circ> Rep = f"
    5.56 +lemma comp_Abs_inverse: "f \<circ> Abs = g \<Longrightarrow> g \<circ> Rep = f"
    5.57    using Rep_inverse by auto
    5.58  
    5.59 -lemma set_Rep:
    5.60 -  "A = range Rep"
    5.61 +lemma set_Rep: "A = range Rep"
    5.62  proof (rule set_eqI)
    5.63 -  fix x
    5.64 -  show "(x \<in> A) = (x \<in> range Rep)"
    5.65 +  show "x \<in> A \<longleftrightarrow> x \<in> range Rep" for x
    5.66      by (auto dest: Abs_inverse [of x, symmetric])
    5.67  qed
    5.68  
    5.69  lemma set_Rep_Abs: "A = range (Rep \<circ> Abs)"
    5.70  proof (rule set_eqI)
    5.71 -  fix x
    5.72 -  show "(x \<in> A) = (x \<in> range (Rep \<circ> Abs))"
    5.73 +  show "x \<in> A \<longleftrightarrow> x \<in> range (Rep \<circ> Abs)" for x
    5.74      by (auto dest: Abs_inverse [of x, symmetric])
    5.75  qed
    5.76  
    5.77 @@ -72,21 +64,18 @@
    5.78  
    5.79  lemmas td_thm = type_definition_axioms
    5.80  
    5.81 -lemma fns1:
    5.82 -  "Rep \<circ> fa = fr \<circ> Rep | fa \<circ> Abs = Abs \<circ> fr ==> Abs \<circ> fr \<circ> Rep = fa"
    5.83 +lemma fns1: "Rep \<circ> fa = fr \<circ> Rep \<or> fa \<circ> Abs = Abs \<circ> fr \<Longrightarrow> Abs \<circ> fr \<circ> Rep = fa"
    5.84    by (auto dest: Rep_comp_inverse elim: comp_Abs_inverse simp: o_assoc)
    5.85  
    5.86  lemmas fns1a = disjI1 [THEN fns1]
    5.87  lemmas fns1b = disjI2 [THEN fns1]
    5.88  
    5.89 -lemma fns4:
    5.90 -  "Rep \<circ> fa \<circ> Abs = fr ==>
    5.91 -   Rep \<circ> fa = fr \<circ> Rep & fa \<circ> Abs = Abs \<circ> fr"
    5.92 +lemma fns4: "Rep \<circ> fa \<circ> Abs = fr \<Longrightarrow> Rep \<circ> fa = fr \<circ> Rep \<and> fa \<circ> Abs = Abs \<circ> fr"
    5.93    by auto
    5.94  
    5.95  end
    5.96  
    5.97 -interpretation nat_int: type_definition int nat "Collect (op <= 0)"
    5.98 +interpretation nat_int: type_definition int nat "Collect (op \<le> 0)"
    5.99    by (rule td_nat_int)
   5.100  
   5.101  declare
   5.102 @@ -99,15 +88,14 @@
   5.103  subsection "Extended form of type definition predicate"
   5.104  
   5.105  lemma td_conds:
   5.106 -  "norm \<circ> norm = norm ==> (fr \<circ> norm = norm \<circ> fr) =
   5.107 -    (norm \<circ> fr \<circ> norm = fr \<circ> norm & norm \<circ> fr \<circ> norm = norm \<circ> fr)"
   5.108 +  "norm \<circ> norm = norm \<Longrightarrow>
   5.109 +    fr \<circ> norm = norm \<circ> fr \<longleftrightarrow> norm \<circ> fr \<circ> norm = fr \<circ> norm \<and> norm \<circ> fr \<circ> norm = norm \<circ> fr"
   5.110    apply safe
   5.111      apply (simp_all add: comp_assoc)
   5.112     apply (simp_all add: o_assoc)
   5.113    done
   5.114  
   5.115 -lemma fn_comm_power:
   5.116 -  "fa \<circ> tr = tr \<circ> fr ==> fa ^^ n \<circ> tr = tr \<circ> fr ^^ n"
   5.117 +lemma fn_comm_power: "fa \<circ> tr = tr \<circ> fr \<Longrightarrow> fa ^^ n \<circ> tr = tr \<circ> fr ^^ n"
   5.118    apply (rule ext)
   5.119    apply (induct n)
   5.120     apply (auto dest: fun_cong)
   5.121 @@ -122,12 +110,10 @@
   5.122    assumes eq_norm: "\<And>x. Rep (Abs x) = norm x"
   5.123  begin
   5.124  
   5.125 -lemma Abs_norm [simp]:
   5.126 -  "Abs (norm x) = Abs x"
   5.127 +lemma Abs_norm [simp]: "Abs (norm x) = Abs x"
   5.128    using eq_norm [of x] by (auto elim: Rep_inverse')
   5.129  
   5.130 -lemma td_th:
   5.131 -  "g \<circ> Abs = f ==> f (Rep x) = g x"
   5.132 +lemma td_th: "g \<circ> Abs = f \<Longrightarrow> f (Rep x) = g x"
   5.133    by (drule comp_Abs_inverse [symmetric]) simp
   5.134  
   5.135  lemma eq_norm': "Rep \<circ> Abs = norm"
   5.136 @@ -141,15 +127,13 @@
   5.137  lemma set_iff_norm: "w : A \<longleftrightarrow> w = norm w"
   5.138    by (auto simp: set_Rep_Abs eq_norm' eq_norm [symmetric])
   5.139  
   5.140 -lemma inverse_norm:
   5.141 -  "(Abs n = w) = (Rep w = norm n)"
   5.142 +lemma inverse_norm: "Abs n = w \<longleftrightarrow> Rep w = norm n"
   5.143    apply (rule iffI)
   5.144     apply (clarsimp simp add: eq_norm)
   5.145    apply (simp add: eq_norm' [symmetric])
   5.146    done
   5.147  
   5.148 -lemma norm_eq_iff:
   5.149 -  "(norm x = norm y) = (Abs x = Abs y)"
   5.150 +lemma norm_eq_iff: "norm x = norm y \<longleftrightarrow> Abs x = Abs y"
   5.151    by (simp add: eq_norm' [symmetric])
   5.152  
   5.153  lemma norm_comps:
   5.154 @@ -160,9 +144,7 @@
   5.155  
   5.156  lemmas norm_norm [simp] = norm_comps
   5.157  
   5.158 -lemma fns5:
   5.159 -  "Rep \<circ> fa \<circ> Abs = fr ==>
   5.160 -  fr \<circ> norm = fr & norm \<circ> fr = fr"
   5.161 +lemma fns5: "Rep \<circ> fa \<circ> Abs = fr \<Longrightarrow> fr \<circ> norm = fr \<and> norm \<circ> fr = fr"
   5.162    by (fold eq_norm') auto
   5.163  
   5.164  (* following give conditions for converses to td_fns1
   5.165 @@ -174,9 +156,7 @@
   5.166    takes norm-equivalent arguments to the same result, and
   5.167    (norm \<circ> fr = fr) says that fr takes any argument to a normalised result
   5.168    *)
   5.169 -lemma fns2:
   5.170 -  "Abs \<circ> fr \<circ> Rep = fa ==>
   5.171 -   (norm \<circ> fr \<circ> norm = fr \<circ> norm) = (Rep \<circ> fa = fr \<circ> Rep)"
   5.172 +lemma fns2: "Abs \<circ> fr \<circ> Rep = fa \<Longrightarrow> norm \<circ> fr \<circ> norm = fr \<circ> norm \<longleftrightarrow> Rep \<circ> fa = fr \<circ> Rep"
   5.173    apply (fold eq_norm')
   5.174    apply safe
   5.175     prefer 2
   5.176 @@ -186,9 +166,7 @@
   5.177    apply auto
   5.178    done
   5.179  
   5.180 -lemma fns3:
   5.181 -  "Abs \<circ> fr \<circ> Rep = fa ==>
   5.182 -   (norm \<circ> fr \<circ> norm = norm \<circ> fr) = (fa \<circ> Abs = Abs \<circ> fr)"
   5.183 +lemma fns3: "Abs \<circ> fr \<circ> Rep = fa \<Longrightarrow> norm \<circ> fr \<circ> norm = norm \<circ> fr \<longleftrightarrow> fa \<circ> Abs = Abs \<circ> fr"
   5.184    apply (fold eq_norm')
   5.185    apply safe
   5.186     prefer 2
   5.187 @@ -198,9 +176,7 @@
   5.188    apply simp
   5.189    done
   5.190  
   5.191 -lemma fns:
   5.192 -  "fr \<circ> norm = norm \<circ> fr ==>
   5.193 -    (fa \<circ> Abs = Abs \<circ> fr) = (Rep \<circ> fa = fr \<circ> Rep)"
   5.194 +lemma fns: "fr \<circ> norm = norm \<circ> fr \<Longrightarrow> fa \<circ> Abs = Abs \<circ> fr \<longleftrightarrow> Rep \<circ> fa = fr \<circ> Rep"
   5.195    apply safe
   5.196     apply (frule fns1b)
   5.197     prefer 2
   5.198 @@ -212,8 +188,7 @@
   5.199     apply (simp_all add: o_assoc)
   5.200    done
   5.201  
   5.202 -lemma range_norm:
   5.203 -  "range (Rep \<circ> Abs) = A"
   5.204 +lemma range_norm: "range (Rep \<circ> Abs) = A"
   5.205    by (simp add: set_Rep_Abs)
   5.206  
   5.207  end
     6.1 --- a/src/HOL/Word/WordBitwise.thy	Sun Dec 03 13:22:09 2017 +0100
     6.2 +++ b/src/HOL/Word/WordBitwise.thy	Sun Dec 03 18:53:49 2017 +0100
     6.3 @@ -415,9 +415,10 @@
     6.4  
     6.5  val word_ss = simpset_of @{theory_context Word};
     6.6  
     6.7 -fun mk_nat_clist ns = List.foldr
     6.8 -  (uncurry (Thm.mk_binop @{cterm "Cons :: nat => _"}))
     6.9 -  @{cterm "[] :: nat list"} ns;
    6.10 +fun mk_nat_clist ns =
    6.11 +  List.foldr
    6.12 +    (uncurry (Thm.mk_binop @{cterm "Cons :: nat \<Rightarrow> _"}))
    6.13 +    @{cterm "[] :: nat list"} ns;
    6.14  
    6.15  fun upt_conv ctxt ct =
    6.16    case Thm.term_of ct of
    6.17 @@ -426,8 +427,9 @@
    6.18          val (i, j) = apply2 (snd o HOLogic.dest_number) (n, m);
    6.19          val ns = map (Numeral.mk_cnumber @{ctyp nat}) (i upto (j - 1))
    6.20            |> mk_nat_clist;
    6.21 -        val prop = Thm.mk_binop @{cterm "op = :: nat list => _"} ct ns
    6.22 -                     |> Thm.apply @{cterm Trueprop};
    6.23 +        val prop =
    6.24 +          Thm.mk_binop @{cterm "op = :: nat list \<Rightarrow> _"} ct ns
    6.25 +          |> Thm.apply @{cterm Trueprop};
    6.26        in
    6.27          try (fn () =>
    6.28            Goal.prove_internal ctxt [] prop
    6.29 @@ -441,16 +443,19 @@
    6.30     {lhss = [@{term "upt x y"}], proc = K upt_conv};
    6.31  
    6.32  fun word_len_simproc_fn ctxt ct =
    6.33 -  case Thm.term_of ct of
    6.34 -    Const (@{const_name len_of}, _) $ t => (let
    6.35 +  (case Thm.term_of ct of
    6.36 +    Const (@{const_name len_of}, _) $ t =>
    6.37 +     (let
    6.38          val T = fastype_of t |> dest_Type |> snd |> the_single
    6.39          val n = Numeral.mk_cnumber @{ctyp nat} (Word_Lib.dest_binT T);
    6.40 -        val prop = Thm.mk_binop @{cterm "op = :: nat => _"} ct n
    6.41 -                 |> Thm.apply @{cterm Trueprop};
    6.42 -      in Goal.prove_internal ctxt [] prop (K (simp_tac (put_simpset word_ss ctxt) 1))
    6.43 -             |> mk_meta_eq |> SOME end
    6.44 -    handle TERM _ => NONE | TYPE _ => NONE)
    6.45 -  | _ => NONE;
    6.46 +        val prop =
    6.47 +          Thm.mk_binop @{cterm "op = :: nat \<Rightarrow> _"} ct n
    6.48 +          |> Thm.apply @{cterm Trueprop};
    6.49 +      in
    6.50 +        Goal.prove_internal ctxt [] prop (K (simp_tac (put_simpset word_ss ctxt) 1))
    6.51 +        |> mk_meta_eq |> SOME
    6.52 +      end handle TERM _ => NONE | TYPE _ => NONE)
    6.53 +  | _ => NONE);
    6.54  
    6.55  val word_len_simproc =
    6.56    Simplifier.make_simproc @{context} "word_len"
    6.57 @@ -462,21 +467,24 @@
    6.58  fun nat_get_Suc_simproc_fn n_sucs ctxt ct =
    6.59    let
    6.60      val (f $ arg) = Thm.term_of ct;
    6.61 -    val n = (case arg of @{term nat} $ n => n | n => n)
    6.62 +    val n =
    6.63 +      (case arg of @{term nat} $ n => n | n => n)
    6.64        |> HOLogic.dest_number |> snd;
    6.65 -    val (i, j) = if n > n_sucs then (n_sucs, n - n_sucs)
    6.66 -      else (n, 0);
    6.67 -    val arg' = List.foldr (op $) (HOLogic.mk_number @{typ nat} j)
    6.68 -        (replicate i @{term Suc});
    6.69 +    val (i, j) = if n > n_sucs then (n_sucs, n - n_sucs) else (n, 0);
    6.70 +    val arg' =
    6.71 +      List.foldr (op $) (HOLogic.mk_number @{typ nat} j) (replicate i @{term Suc});
    6.72      val _ = if arg = arg' then raise TERM ("", []) else ();
    6.73 -    fun propfn g = HOLogic.mk_eq (g arg, g arg')
    6.74 +    fun propfn g =
    6.75 +      HOLogic.mk_eq (g arg, g arg')
    6.76        |> HOLogic.mk_Trueprop |> Thm.cterm_of ctxt;
    6.77 -    val eq1 = Goal.prove_internal ctxt [] (propfn I)
    6.78 -      (K (simp_tac (put_simpset word_ss ctxt) 1));
    6.79 -  in Goal.prove_internal ctxt [] (propfn (curry (op $) f))
    6.80 +    val eq1 =
    6.81 +      Goal.prove_internal ctxt [] (propfn I)
    6.82 +        (K (simp_tac (put_simpset word_ss ctxt) 1));
    6.83 +  in
    6.84 +    Goal.prove_internal ctxt [] (propfn (curry (op $) f))
    6.85        (K (simp_tac (put_simpset HOL_ss ctxt addsimps [eq1]) 1))
    6.86 -       |> mk_meta_eq |> SOME end
    6.87 -    handle TERM _ => NONE;
    6.88 +    |> mk_meta_eq |> SOME
    6.89 +  end handle TERM _ => NONE;
    6.90  
    6.91  fun nat_get_Suc_simproc n_sucs ts =
    6.92    Simplifier.make_simproc @{context} "nat_get_Suc"
     7.1 --- a/src/HOL/Word/Word_Miscellaneous.thy	Sun Dec 03 13:22:09 2017 +0100
     7.2 +++ b/src/HOL/Word/Word_Miscellaneous.thy	Sun Dec 03 18:53:49 2017 +0100
     7.3 @@ -28,19 +28,19 @@
     7.4    done
     7.5  
     7.6  lemma list_exhaust_size_gt0:
     7.7 -  assumes y: "\<And>a list. y = a # list \<Longrightarrow> P"
     7.8 +  assumes "\<And>a list. y = a # list \<Longrightarrow> P"
     7.9    shows "0 < length y \<Longrightarrow> P"
    7.10    apply (cases y)
    7.11     apply simp
    7.12 -  apply (rule y)
    7.13 +  apply (rule assms)
    7.14    apply fastforce
    7.15    done
    7.16  
    7.17  lemma list_exhaust_size_eq0:
    7.18 -  assumes y: "y = [] \<Longrightarrow> P"
    7.19 +  assumes "y = [] \<Longrightarrow> P"
    7.20    shows "length y = 0 \<Longrightarrow> P"
    7.21    apply (cases y)
    7.22 -   apply (rule y)
    7.23 +   apply (rule assms)
    7.24     apply simp
    7.25    apply simp
    7.26    done
    7.27 @@ -307,7 +307,7 @@
    7.28  
    7.29  lemmas td_gal_lt = td_gal [simplified not_less [symmetric], simplified]
    7.30  
    7.31 -lemmas div_mult_le = div_times_less_eq_dividend 
    7.32 +lemmas div_mult_le = div_times_less_eq_dividend
    7.33  
    7.34  lemmas sdl = div_nat_eqI
    7.35