Merge
authorpaulson <lp15@cam.ac.uk>
Mon May 23 15:46:30 2016 +0100 (2016-05-23 ago)
changeset 6311539dca4891601
parent 63114 27afe7af7379
parent 63113 fe31996e3898
child 63116 32492105b015
child 63120 547460dc5c1e
child 63125 f2d3f8427bc2
Merge
     1.1 --- a/NEWS	Mon May 23 15:33:24 2016 +0100
     1.2 +++ b/NEWS	Mon May 23 15:46:30 2016 +0100
     1.3 @@ -117,6 +117,9 @@
     1.4      INCOMPATIBILITY.
     1.5    - The "size" plugin has been made compatible again with locales.
     1.6  
     1.7 +* Removed obsolete theorem nat_less_cases. INCOMPATIBILITY, use
     1.8 +linorder_cases instead.
     1.9 +
    1.10  * Renamed split_if -> if_split and split_if_asm -> if_split_asm to
    1.11  resemble the f.split naming convention, INCOMPATIBILITY.
    1.12  
     2.1 --- a/src/HOL/Library/Omega_Words_Fun.thy	Mon May 23 15:33:24 2016 +0100
     2.2 +++ b/src/HOL/Library/Omega_Words_Fun.thy	Mon May 23 15:46:30 2016 +0100
     2.3 @@ -800,8 +800,8 @@
     2.4    assumes iseq: "idx_sequence idx"
     2.5      and eq: "idx m = idx n"
     2.6    shows "m = n"
     2.7 -proof (rule nat_less_cases)
     2.8 -  assume "n<m"
     2.9 +proof (cases m n rule: linorder_cases)
    2.10 +  case greater
    2.11    then obtain k where "m = Suc(n+k)"
    2.12      by (auto simp add: less_iff_Suc_add)
    2.13    with iseq have "idx n < idx m"
    2.14 @@ -809,14 +809,14 @@
    2.15    with eq show ?thesis
    2.16      by simp
    2.17  next
    2.18 -  assume "m<n"
    2.19 +  case less
    2.20    then obtain k where "n = Suc(m+k)"
    2.21      by (auto simp add: less_iff_Suc_add)
    2.22    with iseq have "idx m < idx n"
    2.23      by (simp add: idx_sequence_less)
    2.24    with eq show ?thesis
    2.25      by simp
    2.26 -qed (simp)
    2.27 +qed
    2.28  
    2.29  lemma idx_sequence_mono:
    2.30    assumes iseq: "idx_sequence idx"
    2.31 @@ -883,8 +883,8 @@
    2.32      and k: "n \<in> {idx k ..< idx (Suc k)}"
    2.33      and m: "n \<in> {idx m ..< idx (Suc m)}"
    2.34    shows "k = m"
    2.35 -proof (rule nat_less_cases)
    2.36 -  assume "k < m"
    2.37 +proof (cases k m rule: linorder_cases)
    2.38 +  case less
    2.39    hence "Suc k \<le> m" by simp
    2.40    with iseq have "idx (Suc k) \<le> idx m"
    2.41      by (rule idx_sequence_mono)
    2.42 @@ -894,7 +894,7 @@
    2.43      by simp
    2.44    thus ?thesis ..
    2.45  next
    2.46 -  assume "m < k"
    2.47 +  case greater
    2.48    hence "Suc m \<le> k" by simp
    2.49    with iseq have "idx (Suc m) \<le> idx k"
    2.50      by (rule idx_sequence_mono)
    2.51 @@ -903,7 +903,7 @@
    2.52    with m have "False"
    2.53      by simp
    2.54    thus ?thesis ..
    2.55 -qed (simp)
    2.56 +qed
    2.57  
    2.58  lemma idx_sequence_unique_interval:
    2.59    assumes iseq: "idx_sequence idx"
     3.1 --- a/src/HOL/Nat.thy	Mon May 23 15:33:24 2016 +0100
     3.2 +++ b/src/HOL/Nat.thy	Mon May 23 15:46:30 2016 +0100
     3.3 @@ -21,10 +21,10 @@
     3.4  
     3.5  typedecl ind
     3.6  
     3.7 -axiomatization Zero_Rep :: ind and Suc_Rep :: "ind => ind" where
     3.8 -  \<comment> \<open>the axiom of infinity in 2 parts\<close>
     3.9 -  Suc_Rep_inject:       "Suc_Rep x = Suc_Rep y ==> x = y" and
    3.10 -  Suc_Rep_not_Zero_Rep: "Suc_Rep x \<noteq> Zero_Rep"
    3.11 +axiomatization Zero_Rep :: ind and Suc_Rep :: "ind \<Rightarrow> ind"
    3.12 +  \<comment> \<open>The axiom of infinity in 2 parts:\<close>
    3.13 +where Suc_Rep_inject: "Suc_Rep x = Suc_Rep y \<Longrightarrow> x = y"
    3.14 +  and Suc_Rep_not_Zero_Rep: "Suc_Rep x \<noteq> Zero_Rep"
    3.15  
    3.16  subsection \<open>Type nat\<close>
    3.17  
    3.18 @@ -120,8 +120,8 @@
    3.19  
    3.20  setup \<open>Sign.parent_path\<close>
    3.21  
    3.22 -abbreviation rec_nat :: "'a \<Rightarrow> (nat \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> nat \<Rightarrow> 'a" where
    3.23 -  "rec_nat \<equiv> old.rec_nat"
    3.24 +abbreviation rec_nat :: "'a \<Rightarrow> (nat \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> nat \<Rightarrow> 'a"
    3.25 +  where "rec_nat \<equiv> old.rec_nat"
    3.26  
    3.27  declare nat.sel[code del]
    3.28  
    3.29 @@ -199,8 +199,12 @@
    3.30  text \<open>A special form of induction for reasoning
    3.31    about @{term "m < n"} and @{term "m - n"}\<close>
    3.32  
    3.33 -lemma diff_induct: "(!!x. P x 0) ==> (!!y. P 0 (Suc y)) ==>
    3.34 -    (!!x y. P x y ==> P (Suc x) (Suc y)) ==> P m n"
    3.35 +lemma diff_induct:
    3.36 +  assumes "\<And>x. P x 0"
    3.37 +    and "\<And>y. P 0 (Suc y)"
    3.38 +    and "\<And>x y. P x y \<Longrightarrow> P (Suc x) (Suc y)"
    3.39 +  shows "P m n"
    3.40 +  using assms
    3.41    apply (rule_tac x = m in spec)
    3.42    apply (induct n)
    3.43    prefer 2
    3.44 @@ -215,10 +219,10 @@
    3.45  begin
    3.46  
    3.47  primrec plus_nat where
    3.48 -  add_0:      "0 + n = (n::nat)"
    3.49 -| add_Suc:  "Suc m + n = Suc (m + n)"
    3.50 -
    3.51 -lemma add_0_right [simp]: "m + 0 = (m::nat)"
    3.52 +  add_0: "0 + n = (n::nat)"
    3.53 +| add_Suc: "Suc m + n = Suc (m + n)"
    3.54 +
    3.55 +lemma add_0_right [simp]: "m + 0 = m" for m :: nat
    3.56    by (induct m) simp_all
    3.57  
    3.58  lemma add_Suc_right [simp]: "m + Suc n = Suc (m + n)"
    3.59 @@ -231,17 +235,18 @@
    3.60  
    3.61  primrec minus_nat where
    3.62    diff_0 [code]: "m - 0 = (m::nat)"
    3.63 -| diff_Suc: "m - Suc n = (case m - n of 0 => 0 | Suc k => k)"
    3.64 +| diff_Suc: "m - Suc n = (case m - n of 0 \<Rightarrow> 0 | Suc k \<Rightarrow> k)"
    3.65  
    3.66  declare diff_Suc [simp del]
    3.67  
    3.68 -lemma diff_0_eq_0 [simp, code]: "0 - n = (0::nat)"
    3.69 +lemma diff_0_eq_0 [simp, code]: "0 - n = 0" for n :: nat
    3.70    by (induct n) (simp_all add: diff_Suc)
    3.71  
    3.72  lemma diff_Suc_Suc [simp, code]: "Suc m - Suc n = m - n"
    3.73    by (induct n) (simp_all add: diff_Suc)
    3.74  
    3.75 -instance proof
    3.76 +instance
    3.77 +proof
    3.78    fix n m q :: nat
    3.79    show "(n + m) + q = n + (m + q)" by (induct n) simp_all
    3.80    show "n + m = m + n" by (induct n) simp_all
    3.81 @@ -265,25 +270,24 @@
    3.82    mult_0: "0 * n = (0::nat)"
    3.83  | mult_Suc: "Suc m * n = n + (m * n)"
    3.84  
    3.85 -lemma mult_0_right [simp]: "(m::nat) * 0 = 0"
    3.86 +lemma mult_0_right [simp]: "m * 0 = 0" for m :: nat
    3.87    by (induct m) simp_all
    3.88  
    3.89  lemma mult_Suc_right [simp]: "m * Suc n = m + (m * n)"
    3.90    by (induct m) (simp_all add: add.left_commute)
    3.91  
    3.92 -lemma add_mult_distrib: "(m + n) * k = (m * k) + ((n * k)::nat)"
    3.93 +lemma add_mult_distrib: "(m + n) * k = (m * k) + (n * k)" for m n k :: nat
    3.94    by (induct m) (simp_all add: add.assoc)
    3.95  
    3.96 -instance proof
    3.97 -  fix n m q :: nat
    3.98 +instance
    3.99 +proof
   3.100 +  fix k n m q :: nat
   3.101    show "0 \<noteq> (1::nat)" unfolding One_nat_def by simp
   3.102    show "1 * n = n" unfolding One_nat_def by simp
   3.103    show "n * m = m * n" by (induct n) simp_all
   3.104    show "(n * m) * q = n * (m * q)" by (induct n) (simp_all add: add_mult_distrib)
   3.105    show "(n + m) * q = n * q + m * q" by (rule add_mult_distrib)
   3.106 -next
   3.107 -  fix k m n :: nat
   3.108 -  show "k * ((m::nat) - n) = (k * m) - (k * n)"
   3.109 +  show "k * (m - n) = (k * m) - (k * n)"
   3.110      by (induct m n rule: diff_induct) simp_all
   3.111  qed
   3.112  
   3.113 @@ -294,29 +298,23 @@
   3.114  
   3.115  text \<open>Reasoning about \<open>m + 0 = 0\<close>, etc.\<close>
   3.116  
   3.117 -lemma add_is_0 [iff]:
   3.118 -  fixes m n :: nat
   3.119 -  shows "(m + n = 0) = (m = 0 & n = 0)"
   3.120 +lemma add_is_0 [iff]: "(m + n = 0) = (m = 0 \<and> n = 0)" for m n :: nat
   3.121    by (cases m) simp_all
   3.122  
   3.123 -lemma add_is_1:
   3.124 -  "(m+n= Suc 0) = (m= Suc 0 & n=0 | m=0 & n= Suc 0)"
   3.125 +lemma add_is_1: "m + n = Suc 0 \<longleftrightarrow> m = Suc 0 \<and> n = 0 | m = 0 \<and> n = Suc 0"
   3.126    by (cases m) simp_all
   3.127  
   3.128 -lemma one_is_add:
   3.129 -  "(Suc 0 = m + n) = (m = Suc 0 & n = 0 | m = 0 & n = Suc 0)"
   3.130 +lemma one_is_add: "Suc 0 = m + n \<longleftrightarrow> m = Suc 0 \<and> n = 0 | m = 0 \<and> n = Suc 0"
   3.131    by (rule trans, rule eq_commute, rule add_is_1)
   3.132  
   3.133 -lemma add_eq_self_zero:
   3.134 -  fixes m n :: nat
   3.135 -  shows "m + n = m \<Longrightarrow> n = 0"
   3.136 +lemma add_eq_self_zero: "m + n = m \<Longrightarrow> n = 0" for m n :: nat
   3.137    by (induct m) simp_all
   3.138  
   3.139 -lemma inj_on_add_nat[simp]: "inj_on (%n::nat. n+k) N"
   3.140 +lemma inj_on_add_nat[simp]: "inj_on (\<lambda>n. n + k) N" for k :: nat
   3.141    apply (induct k)
   3.142     apply simp
   3.143 -  apply(drule comp_inj_on[OF _ inj_Suc])
   3.144 -  apply (simp add:o_def)
   3.145 +  apply (drule comp_inj_on[OF _ inj_Suc])
   3.146 +  apply (simp add: o_def)
   3.147    done
   3.148  
   3.149  lemma Suc_eq_plus1: "Suc n = n + 1"
   3.150 @@ -336,43 +334,45 @@
   3.151  
   3.152  subsubsection \<open>Multiplication\<close>
   3.153  
   3.154 -lemma mult_is_0 [simp]: "((m::nat) * n = 0) = (m=0 | n=0)"
   3.155 +lemma mult_is_0 [simp]: "m * n = 0 \<longleftrightarrow> m = 0 \<or> n = 0" for m n :: nat
   3.156    by (induct m) auto
   3.157  
   3.158 -lemma mult_eq_1_iff [simp]: "(m * n = Suc 0) = (m = Suc 0 & n = Suc 0)"
   3.159 +lemma mult_eq_1_iff [simp]: "m * n = Suc 0 \<longleftrightarrow> m = Suc 0 \<and> n = Suc 0"
   3.160    apply (induct m)
   3.161     apply simp
   3.162    apply (induct n)
   3.163     apply auto
   3.164    done
   3.165  
   3.166 -lemma one_eq_mult_iff [simp]: "(Suc 0 = m * n) = (m = Suc 0 & n = Suc 0)"
   3.167 +lemma one_eq_mult_iff [simp]: "Suc 0 = m * n \<longleftrightarrow> m = Suc 0 \<and> n = Suc 0"
   3.168    apply (rule trans)
   3.169    apply (rule_tac [2] mult_eq_1_iff, fastforce)
   3.170    done
   3.171  
   3.172 -lemma nat_mult_eq_1_iff [simp]: "m * n = (1::nat) \<longleftrightarrow> m = 1 \<and> n = 1"
   3.173 +lemma nat_mult_eq_1_iff [simp]: "m * n = 1 \<longleftrightarrow> m = 1 \<and> n = 1" for m n :: nat
   3.174    unfolding One_nat_def by (rule mult_eq_1_iff)
   3.175  
   3.176 -lemma nat_1_eq_mult_iff [simp]: "(1::nat) = m * n \<longleftrightarrow> m = 1 \<and> n = 1"
   3.177 +lemma nat_1_eq_mult_iff [simp]: "1 = m * n \<longleftrightarrow> m = 1 \<and> n = 1" for m n :: nat
   3.178    unfolding One_nat_def by (rule one_eq_mult_iff)
   3.179  
   3.180 -lemma mult_cancel1 [simp]: "(k * m = k * n) = (m = n | (k = (0::nat)))"
   3.181 +lemma mult_cancel1 [simp]: "k * m = k * n \<longleftrightarrow> m = n \<or> k = 0" for k m n :: nat
   3.182  proof -
   3.183    have "k \<noteq> 0 \<Longrightarrow> k * m = k * n \<Longrightarrow> m = n"
   3.184    proof (induct n arbitrary: m)
   3.185 -    case 0 then show "m = 0" by simp
   3.186 +    case 0
   3.187 +    then show "m = 0" by simp
   3.188    next
   3.189 -    case (Suc n) then show "m = Suc n"
   3.190 -      by (cases m) (simp_all add: eq_commute [of "0"])
   3.191 +    case (Suc n)
   3.192 +    then show "m = Suc n"
   3.193 +      by (cases m) (simp_all add: eq_commute [of 0])
   3.194    qed
   3.195    then show ?thesis by auto
   3.196  qed
   3.197  
   3.198 -lemma mult_cancel2 [simp]: "(m * k = n * k) = (m = n | (k = (0::nat)))"
   3.199 +lemma mult_cancel2 [simp]: "m * k = n * k \<longleftrightarrow> m = n \<or> k = 0" for k m n :: nat
   3.200    by (simp add: mult.commute)
   3.201  
   3.202 -lemma Suc_mult_cancel1: "(Suc k * m = Suc k * n) = (m = n)"
   3.203 +lemma Suc_mult_cancel1: "Suc k * m = Suc k * n \<longleftrightarrow> m = n"
   3.204    by (subst mult_cancel1) simp
   3.205  
   3.206  
   3.207 @@ -388,8 +388,12 @@
   3.208  | "Suc m \<le> n \<longleftrightarrow> (case n of 0 \<Rightarrow> False | Suc n \<Rightarrow> m \<le> n)"
   3.209  
   3.210  declare less_eq_nat.simps [simp del]
   3.211 -lemma le0 [iff]: "0 \<le> (n::nat)" by (simp add: less_eq_nat.simps)
   3.212 -lemma [code]: "(0::nat) \<le> n \<longleftrightarrow> True" by simp
   3.213 +
   3.214 +lemma le0 [iff]: "0 \<le> n" for n :: nat
   3.215 +  by (simp add: less_eq_nat.simps)
   3.216 +
   3.217 +lemma [code]: "0 \<le> n \<longleftrightarrow> True" for n :: nat
   3.218 +  by simp
   3.219  
   3.220  definition less_nat where
   3.221    less_eq_Suc_le: "n < m \<longleftrightarrow> Suc n \<le> m"
   3.222 @@ -400,13 +404,13 @@
   3.223  lemma Suc_le_eq [code]: "Suc m \<le> n \<longleftrightarrow> m < n"
   3.224    unfolding less_eq_Suc_le ..
   3.225  
   3.226 -lemma le_0_eq [iff]: "(n::nat) \<le> 0 \<longleftrightarrow> n = 0"
   3.227 +lemma le_0_eq [iff]: "n \<le> 0 \<longleftrightarrow> n = 0" for n :: nat
   3.228    by (induct n) (simp_all add: less_eq_nat.simps(2))
   3.229  
   3.230 -lemma not_less0 [iff]: "\<not> n < (0::nat)"
   3.231 +lemma not_less0 [iff]: "\<not> n < 0" for n :: nat
   3.232    by (simp add: less_eq_Suc_le)
   3.233  
   3.234 -lemma less_nat_zero_code [code]: "n < (0::nat) \<longleftrightarrow> False"
   3.235 +lemma less_nat_zero_code [code]: "n < 0 \<longleftrightarrow> False" for n :: nat
   3.236    by simp
   3.237  
   3.238  lemma Suc_less_eq [iff]: "Suc m < Suc n \<longleftrightarrow> m < n"
   3.239 @@ -419,8 +423,7 @@
   3.240    by (cases m) auto
   3.241  
   3.242  lemma le_SucI: "m \<le> n \<Longrightarrow> m \<le> Suc n"
   3.243 -  by (induct m arbitrary: n)
   3.244 -    (simp_all add: less_eq_nat.simps(2) split: nat.splits)
   3.245 +  by (induct m arbitrary: n) (simp_all add: less_eq_nat.simps(2) split: nat.splits)
   3.246  
   3.247  lemma Suc_leD: "Suc m \<le> n \<Longrightarrow> m \<le> n"
   3.248    by (cases n) (auto intro: le_SucI)
   3.249 @@ -433,33 +436,32 @@
   3.250  
   3.251  instance
   3.252  proof
   3.253 -  fix n m :: nat
   3.254 +  fix n m q :: nat
   3.255    show "n < m \<longleftrightarrow> n \<le> m \<and> \<not> m \<le> n"
   3.256    proof (induct n arbitrary: m)
   3.257 -    case 0 then show ?case by (cases m) (simp_all add: less_eq_Suc_le)
   3.258 +    case 0
   3.259 +    then show ?case by (cases m) (simp_all add: less_eq_Suc_le)
   3.260    next
   3.261 -    case (Suc n) then show ?case by (cases m) (simp_all add: less_eq_Suc_le)
   3.262 +    case (Suc n)
   3.263 +    then show ?case by (cases m) (simp_all add: less_eq_Suc_le)
   3.264    qed
   3.265 -next
   3.266 -  fix n :: nat show "n \<le> n" by (induct n) simp_all
   3.267 -next
   3.268 -  fix n m :: nat assume "n \<le> m" and "m \<le> n"
   3.269 -  then show "n = m"
   3.270 -    by (induct n arbitrary: m)
   3.271 +  show "n \<le> n" by (induct n) simp_all
   3.272 +  then show "n = m" if "n \<le> m" and "m \<le> n"
   3.273 +    using that by (induct n arbitrary: m)
   3.274        (simp_all add: less_eq_nat.simps(2) split: nat.splits)
   3.275 -next
   3.276 -  fix n m q :: nat assume "n \<le> m" and "m \<le> q"
   3.277 -  then show "n \<le> q"
   3.278 +  show "n \<le> q" if "n \<le> m" and "m \<le> q"
   3.279 +    using that
   3.280    proof (induct n arbitrary: m q)
   3.281 -    case 0 show ?case by simp
   3.282 +    case 0
   3.283 +    show ?case by simp
   3.284    next
   3.285 -    case (Suc n) then show ?case
   3.286 +    case (Suc n)
   3.287 +    then show ?case
   3.288        by (simp_all (no_asm_use) add: less_eq_nat.simps(2) split: nat.splits, clarify,
   3.289          simp_all (no_asm_use) add: less_eq_nat.simps(2) split: nat.splits, clarify,
   3.290          simp_all (no_asm_use) add: less_eq_nat.simps(2) split: nat.splits)
   3.291    qed
   3.292 -next
   3.293 -  fix n m :: nat show "n \<le> m \<or> m \<le> n"
   3.294 +  show "n \<le> m \<or> m \<le> n"
   3.295      by (induct n arbitrary: m)
   3.296        (simp_all add: less_eq_nat.simps(2) split: nat.splits)
   3.297  qed
   3.298 @@ -469,11 +471,9 @@
   3.299  instantiation nat :: order_bot
   3.300  begin
   3.301  
   3.302 -definition bot_nat :: nat where
   3.303 -  "bot_nat = 0"
   3.304 -
   3.305 -instance proof
   3.306 -qed (simp add: bot_nat_def)
   3.307 +definition bot_nat :: nat where "bot_nat = 0"
   3.308 +
   3.309 +instance by standard (simp add: bot_nat_def)
   3.310  
   3.311  end
   3.312  
   3.313 @@ -492,94 +492,91 @@
   3.314  
   3.315  subsubsection \<open>Elimination properties\<close>
   3.316  
   3.317 -lemma less_not_refl: "~ n < (n::nat)"
   3.318 +lemma less_not_refl: "\<not> n < n" for n :: nat
   3.319    by (rule order_less_irrefl)
   3.320  
   3.321 -lemma less_not_refl2: "n < m ==> m \<noteq> (n::nat)"
   3.322 +lemma less_not_refl2: "n < m \<Longrightarrow> m \<noteq> n" for m n :: nat
   3.323    by (rule not_sym) (rule less_imp_neq)
   3.324  
   3.325 -lemma less_not_refl3: "(s::nat) < t ==> s \<noteq> t"
   3.326 +lemma less_not_refl3: "s < t \<Longrightarrow> s \<noteq> t" for s t :: nat
   3.327    by (rule less_imp_neq)
   3.328  
   3.329 -lemma less_irrefl_nat: "(n::nat) < n ==> R"
   3.330 +lemma less_irrefl_nat: "n < n \<Longrightarrow> R" for n :: nat
   3.331    by (rule notE, rule less_not_refl)
   3.332  
   3.333 -lemma less_zeroE: "(n::nat) < 0 ==> R"
   3.334 +lemma less_zeroE: "n < 0 \<Longrightarrow> R" for n :: nat
   3.335    by (rule notE) (rule not_less0)
   3.336  
   3.337 -lemma less_Suc_eq: "(m < Suc n) = (m < n | m = n)"
   3.338 +lemma less_Suc_eq: "m < Suc n \<longleftrightarrow> m < n \<or> m = n"
   3.339    unfolding less_Suc_eq_le le_less ..
   3.340  
   3.341  lemma less_Suc0 [iff]: "(n < Suc 0) = (n = 0)"
   3.342    by (simp add: less_Suc_eq)
   3.343  
   3.344 -lemma less_one [iff]: "(n < (1::nat)) = (n = 0)"
   3.345 +lemma less_one [iff]: "n < 1 \<longleftrightarrow> n = 0" for n :: nat
   3.346    unfolding One_nat_def by (rule less_Suc0)
   3.347  
   3.348 -lemma Suc_mono: "m < n ==> Suc m < Suc n"
   3.349 +lemma Suc_mono: "m < n \<Longrightarrow> Suc m < Suc n"
   3.350    by simp
   3.351  
   3.352  text \<open>"Less than" is antisymmetric, sort of\<close>
   3.353  lemma less_antisym: "\<lbrakk> \<not> n < m; n < Suc m \<rbrakk> \<Longrightarrow> m = n"
   3.354    unfolding not_less less_Suc_eq_le by (rule antisym)
   3.355  
   3.356 -lemma nat_neq_iff: "((m::nat) \<noteq> n) = (m < n | n < m)"
   3.357 +lemma nat_neq_iff: "m \<noteq> n \<longleftrightarrow> m < n \<or> n < m" for m n :: nat
   3.358    by (rule linorder_neq_iff)
   3.359  
   3.360 -lemma nat_less_cases: assumes major: "(m::nat) < n ==> P n m"
   3.361 -  and eqCase: "m = n ==> P n m" and lessCase: "n<m ==> P n m"
   3.362 -  shows "P n m"
   3.363 -  apply (rule less_linear [THEN disjE])
   3.364 -  apply (erule_tac [2] disjE)
   3.365 -  apply (erule lessCase)
   3.366 -  apply (erule sym [THEN eqCase])
   3.367 -  apply (erule major)
   3.368 -  done
   3.369 -
   3.370  
   3.371  subsubsection \<open>Inductive (?) properties\<close>
   3.372  
   3.373 -lemma Suc_lessI: "m < n ==> Suc m \<noteq> n ==> Suc m < n"
   3.374 +lemma Suc_lessI: "m < n \<Longrightarrow> Suc m \<noteq> n \<Longrightarrow> Suc m < n"
   3.375    unfolding less_eq_Suc_le [of m] le_less by simp
   3.376  
   3.377  lemma lessE:
   3.378    assumes major: "i < k"
   3.379 -  and p1: "k = Suc i ==> P" and p2: "!!j. i < j ==> k = Suc j ==> P"
   3.380 +    and 1: "k = Suc i \<Longrightarrow> P"
   3.381 +    and 2: "\<And>j. i < j \<Longrightarrow> k = Suc j \<Longrightarrow> P"
   3.382    shows P
   3.383  proof -
   3.384    from major have "\<exists>j. i \<le> j \<and> k = Suc j"
   3.385      unfolding less_eq_Suc_le by (induct k) simp_all
   3.386    then have "(\<exists>j. i < j \<and> k = Suc j) \<or> k = Suc i"
   3.387 -    by (clarsimp simp add: less_le)
   3.388 -  with p1 p2 show P by auto
   3.389 +    by (auto simp add: less_le)
   3.390 +  with 1 2 show P by auto
   3.391  qed
   3.392  
   3.393 -lemma less_SucE: assumes major: "m < Suc n"
   3.394 -  and less: "m < n ==> P" and eq: "m = n ==> P" shows P
   3.395 +lemma less_SucE:
   3.396 +  assumes major: "m < Suc n"
   3.397 +    and less: "m < n \<Longrightarrow> P"
   3.398 +    and eq: "m = n \<Longrightarrow> P"
   3.399 +  shows P
   3.400    apply (rule major [THEN lessE])
   3.401    apply (rule eq, blast)
   3.402    apply (rule less, blast)
   3.403    done
   3.404  
   3.405 -lemma Suc_lessE: assumes major: "Suc i < k"
   3.406 -  and minor: "!!j. i < j ==> k = Suc j ==> P" shows P
   3.407 +lemma Suc_lessE:
   3.408 +  assumes major: "Suc i < k"
   3.409 +    and minor: "\<And>j. i < j \<Longrightarrow> k = Suc j \<Longrightarrow> P"
   3.410 +  shows P
   3.411    apply (rule major [THEN lessE])
   3.412    apply (erule lessI [THEN minor])
   3.413    apply (erule Suc_lessD [THEN minor], assumption)
   3.414    done
   3.415  
   3.416 -lemma Suc_less_SucD: "Suc m < Suc n ==> m < n"
   3.417 +lemma Suc_less_SucD: "Suc m < Suc n \<Longrightarrow> m < n"
   3.418    by simp
   3.419  
   3.420  lemma less_trans_Suc:
   3.421 -  assumes le: "i < j" shows "j < k ==> Suc i < k"
   3.422 +  assumes le: "i < j"
   3.423 +  shows "j < k \<Longrightarrow> Suc i < k"
   3.424    apply (induct k, simp_all)
   3.425 -  apply (insert le)
   3.426 +  using le
   3.427    apply (simp add: less_Suc_eq)
   3.428    apply (blast dest: Suc_lessD)
   3.429    done
   3.430  
   3.431 -text \<open>Can be used with \<open>less_Suc_eq\<close> to get @{term "n = m | n < m"}\<close>
   3.432 +text \<open>Can be used with \<open>less_Suc_eq\<close> to get @{prop "n = m \<or> n < m"}\<close>
   3.433  lemma not_less_eq: "\<not> m < n \<longleftrightarrow> n < Suc m"
   3.434    unfolding not_less less_Suc_eq_le ..
   3.435  
   3.436 @@ -588,138 +585,138 @@
   3.437  
   3.438  text \<open>Properties of "less than or equal"\<close>
   3.439  
   3.440 -lemma le_imp_less_Suc: "m \<le> n ==> m < Suc n"
   3.441 +lemma le_imp_less_Suc: "m \<le> n \<Longrightarrow> m < Suc n"
   3.442    unfolding less_Suc_eq_le .
   3.443  
   3.444 -lemma Suc_n_not_le_n: "~ Suc n \<le> n"
   3.445 +lemma Suc_n_not_le_n: "\<not> Suc n \<le> n"
   3.446    unfolding not_le less_Suc_eq_le ..
   3.447  
   3.448  lemma le_Suc_eq: "(m \<le> Suc n) = (m \<le> n | m = Suc n)"
   3.449    by (simp add: less_Suc_eq_le [symmetric] less_Suc_eq)
   3.450  
   3.451 -lemma le_SucE: "m \<le> Suc n ==> (m \<le> n ==> R) ==> (m = Suc n ==> R) ==> R"
   3.452 +lemma le_SucE: "m \<le> Suc n \<Longrightarrow> (m \<le> n \<Longrightarrow> R) \<Longrightarrow> (m = Suc n \<Longrightarrow> R) \<Longrightarrow> R"
   3.453    by (drule le_Suc_eq [THEN iffD1], iprover+)
   3.454  
   3.455 -lemma Suc_leI: "m < n ==> Suc(m) \<le> n"
   3.456 +lemma Suc_leI: "m < n \<Longrightarrow> Suc(m) \<le> n"
   3.457    unfolding Suc_le_eq .
   3.458  
   3.459  text \<open>Stronger version of \<open>Suc_leD\<close>\<close>
   3.460 -lemma Suc_le_lessD: "Suc m \<le> n ==> m < n"
   3.461 +lemma Suc_le_lessD: "Suc m \<le> n \<Longrightarrow> m < n"
   3.462    unfolding Suc_le_eq .
   3.463  
   3.464 -lemma less_imp_le_nat: "m < n ==> m \<le> (n::nat)"
   3.465 +lemma less_imp_le_nat: "m < n \<Longrightarrow> m \<le> n" for m n :: nat
   3.466    unfolding less_eq_Suc_le by (rule Suc_leD)
   3.467  
   3.468  text \<open>For instance, \<open>(Suc m < Suc n) = (Suc m \<le> n) = (m < n)\<close>\<close>
   3.469  lemmas le_simps = less_imp_le_nat less_Suc_eq_le Suc_le_eq
   3.470  
   3.471  
   3.472 -text \<open>Equivalence of @{term "m \<le> n"} and @{term "m < n | m = n"}\<close>
   3.473 -
   3.474 -lemma less_or_eq_imp_le: "m < n | m = n ==> m \<le> (n::nat)"
   3.475 +text \<open>Equivalence of \<open>m \<le> n\<close> and \<open>m < n \<or> m = n\<close>\<close>
   3.476 +
   3.477 +lemma less_or_eq_imp_le: "m < n \<or> m = n \<Longrightarrow> m \<le> n" for m n :: nat
   3.478    unfolding le_less .
   3.479  
   3.480 -lemma le_eq_less_or_eq: "(m \<le> (n::nat)) = (m < n | m=n)"
   3.481 +lemma le_eq_less_or_eq: "m \<le> n \<longleftrightarrow> m < n \<or> m = n" for m n :: nat
   3.482    by (rule le_less)
   3.483  
   3.484  text \<open>Useful with \<open>blast\<close>.\<close>
   3.485 -lemma eq_imp_le: "(m::nat) = n ==> m \<le> n"
   3.486 +lemma eq_imp_le: "m = n \<Longrightarrow> m \<le> n" for m n :: nat
   3.487    by auto
   3.488  
   3.489 -lemma le_refl: "n \<le> (n::nat)"
   3.490 +lemma le_refl: "n \<le> n" for n :: nat
   3.491    by simp
   3.492  
   3.493 -lemma le_trans: "[| i \<le> j; j \<le> k |] ==> i \<le> (k::nat)"
   3.494 +lemma le_trans: "i \<le> j \<Longrightarrow> j \<le> k \<Longrightarrow> i \<le> k" for i j k :: nat
   3.495    by (rule order_trans)
   3.496  
   3.497 -lemma le_antisym: "[| m \<le> n; n \<le> m |] ==> m = (n::nat)"
   3.498 +lemma le_antisym: "m \<le> n \<Longrightarrow> n \<le> m \<Longrightarrow> m = n" for m n :: nat
   3.499    by (rule antisym)
   3.500  
   3.501 -lemma nat_less_le: "((m::nat) < n) = (m \<le> n & m \<noteq> n)"
   3.502 +lemma nat_less_le: "m < n \<longleftrightarrow> m \<le> n \<and> m \<noteq> n" for m n :: nat
   3.503    by (rule less_le)
   3.504  
   3.505 -lemma le_neq_implies_less: "(m::nat) \<le> n ==> m \<noteq> n ==> m < n"
   3.506 +lemma le_neq_implies_less: "m \<le> n \<Longrightarrow> m \<noteq> n \<Longrightarrow> m < n" for m n :: nat
   3.507    unfolding less_le ..
   3.508  
   3.509 -lemma nat_le_linear: "(m::nat) \<le> n | n \<le> m"
   3.510 +lemma nat_le_linear: "m \<le> n | n \<le> m" for m n :: nat
   3.511    by (rule linear)
   3.512  
   3.513  lemmas linorder_neqE_nat = linorder_neqE [where 'a = nat]
   3.514  
   3.515 -lemma le_less_Suc_eq: "m \<le> n ==> (n < Suc m) = (n = m)"
   3.516 +lemma le_less_Suc_eq: "m \<le> n \<Longrightarrow> n < Suc m \<longleftrightarrow> n = m"
   3.517    unfolding less_Suc_eq_le by auto
   3.518  
   3.519 -lemma not_less_less_Suc_eq: "~ n < m ==> (n < Suc m) = (n = m)"
   3.520 +lemma not_less_less_Suc_eq: "\<not> n < m \<Longrightarrow> n < Suc m \<longleftrightarrow> n = m"
   3.521    unfolding not_less by (rule le_less_Suc_eq)
   3.522  
   3.523  lemmas not_less_simps = not_less_less_Suc_eq le_less_Suc_eq
   3.524  
   3.525 -lemma not0_implies_Suc: "n \<noteq> 0 ==> \<exists>m. n = Suc m"
   3.526 -by (cases n) simp_all
   3.527 -
   3.528 -lemma gr0_implies_Suc: "n > 0 ==> \<exists>m. n = Suc m"
   3.529 -by (cases n) simp_all
   3.530 -
   3.531 -lemma gr_implies_not0: fixes n :: nat shows "m<n ==> n \<noteq> 0"
   3.532 -by (cases n) simp_all
   3.533 -
   3.534 -lemma neq0_conv[iff]: fixes n :: nat shows "(n \<noteq> 0) = (0 < n)"
   3.535 -by (cases n) simp_all
   3.536 +lemma not0_implies_Suc: "n \<noteq> 0 \<Longrightarrow> \<exists>m. n = Suc m"
   3.537 +  by (cases n) simp_all
   3.538 +
   3.539 +lemma gr0_implies_Suc: "n > 0 \<Longrightarrow> \<exists>m. n = Suc m"
   3.540 +  by (cases n) simp_all
   3.541 +
   3.542 +lemma gr_implies_not0: "m < n \<Longrightarrow> n \<noteq> 0" for m n :: nat
   3.543 +  by (cases n) simp_all
   3.544 +
   3.545 +lemma neq0_conv[iff]: "n \<noteq> 0 \<longleftrightarrow> 0 < n" for n :: nat
   3.546 +  by (cases n) simp_all
   3.547  
   3.548  text \<open>This theorem is useful with \<open>blast\<close>\<close>
   3.549 -lemma gr0I: "((n::nat) = 0 ==> False) ==> 0 < n"
   3.550 -by (rule neq0_conv[THEN iffD1], iprover)
   3.551 -
   3.552 -lemma gr0_conv_Suc: "(0 < n) = (\<exists>m. n = Suc m)"
   3.553 -by (fast intro: not0_implies_Suc)
   3.554 -
   3.555 -lemma not_gr0 [iff]: "!!n::nat. (~ (0 < n)) = (n = 0)"
   3.556 -using neq0_conv by blast
   3.557 -
   3.558 -lemma Suc_le_D: "(Suc n \<le> m') ==> (? m. m' = Suc m)"
   3.559 -by (induct m') simp_all
   3.560 +lemma gr0I: "(n = 0 \<Longrightarrow> False) \<Longrightarrow> 0 < n" for n :: nat
   3.561 +  by (rule neq0_conv[THEN iffD1], iprover)
   3.562 +
   3.563 +lemma gr0_conv_Suc: "0 < n \<longleftrightarrow> (\<exists>m. n = Suc m)"
   3.564 +  by (fast intro: not0_implies_Suc)
   3.565 +
   3.566 +lemma not_gr0 [iff]: "\<not> 0 < n \<longleftrightarrow> n = 0" for n :: nat
   3.567 +  using neq0_conv by blast
   3.568 +
   3.569 +lemma Suc_le_D: "Suc n \<le> m' \<Longrightarrow> \<exists>m. m' = Suc m"
   3.570 +  by (induct m') simp_all
   3.571  
   3.572  text \<open>Useful in certain inductive arguments\<close>
   3.573 -lemma less_Suc_eq_0_disj: "(m < Suc n) = (m = 0 | (\<exists>j. m = Suc j & j < n))"
   3.574 -by (cases m) simp_all
   3.575 +lemma less_Suc_eq_0_disj: "m < Suc n \<longleftrightarrow> m = 0 \<or> (\<exists>j. m = Suc j \<and> j < n)"
   3.576 +  by (cases m) simp_all
   3.577  
   3.578  
   3.579  subsubsection \<open>Monotonicity of Addition\<close>
   3.580  
   3.581 -lemma Suc_pred [simp]: "n>0 ==> Suc (n - Suc 0) = n"
   3.582 -by (simp add: diff_Suc split: nat.split)
   3.583 -
   3.584 -lemma Suc_diff_1 [simp]: "0 < n ==> Suc (n - 1) = n"
   3.585 -unfolding One_nat_def by (rule Suc_pred)
   3.586 -
   3.587 -lemma nat_add_left_cancel_le [simp]: "(k + m \<le> k + n) = (m\<le>(n::nat))"
   3.588 -by (induct k) simp_all
   3.589 -
   3.590 -lemma nat_add_left_cancel_less [simp]: "(k + m < k + n) = (m<(n::nat))"
   3.591 -by (induct k) simp_all
   3.592 -
   3.593 -lemma add_gr_0 [iff]: "!!m::nat. (m + n > 0) = (m>0 | n>0)"
   3.594 -by(auto dest:gr0_implies_Suc)
   3.595 +lemma Suc_pred [simp]: "n > 0 \<Longrightarrow> Suc (n - Suc 0) = n"
   3.596 +  by (simp add: diff_Suc split: nat.split)
   3.597 +
   3.598 +lemma Suc_diff_1 [simp]: "0 < n \<Longrightarrow> Suc (n - 1) = n"
   3.599 +  unfolding One_nat_def by (rule Suc_pred)
   3.600 +
   3.601 +lemma nat_add_left_cancel_le [simp]: "k + m \<le> k + n \<longleftrightarrow> m \<le> n" for k m n :: nat
   3.602 +  by (induct k) simp_all
   3.603 +
   3.604 +lemma nat_add_left_cancel_less [simp]: "k + m < k + n \<longleftrightarrow> m < n" for k m n :: nat
   3.605 +  by (induct k) simp_all
   3.606 +
   3.607 +lemma add_gr_0 [iff]: "m + n > 0 \<longleftrightarrow> m > 0 \<or> n > 0" for m n :: nat
   3.608 +  by (auto dest: gr0_implies_Suc)
   3.609  
   3.610  text \<open>strict, in 1st argument\<close>
   3.611 -lemma add_less_mono1: "i < j ==> i + k < j + (k::nat)"
   3.612 -by (induct k) simp_all
   3.613 +lemma add_less_mono1: "i < j \<Longrightarrow> i + k < j + k" for i j k :: nat
   3.614 +  by (induct k) simp_all
   3.615  
   3.616  text \<open>strict, in both arguments\<close>
   3.617 -lemma add_less_mono: "[|i < j; k < l|] ==> i + k < j + (l::nat)"
   3.618 +lemma add_less_mono: "i < j \<Longrightarrow> k < l \<Longrightarrow> i + k < j + l" for i j k l :: nat
   3.619    apply (rule add_less_mono1 [THEN less_trans], assumption+)
   3.620    apply (induct j, simp_all)
   3.621    done
   3.622  
   3.623  text \<open>Deleted \<open>less_natE\<close>; use \<open>less_imp_Suc_add RS exE\<close>\<close>
   3.624 -lemma less_imp_Suc_add: "m < n ==> (\<exists>k. n = Suc (m + k))"
   3.625 +lemma less_imp_Suc_add: "m < n \<Longrightarrow> \<exists>k. n = Suc (m + k)"
   3.626    apply (induct n)
   3.627    apply (simp_all add: order_le_less)
   3.628    apply (blast elim!: less_SucE
   3.629                 intro!: Nat.add_0_right [symmetric] add_Suc_right [symmetric])
   3.630    done
   3.631  
   3.632 -lemma le_Suc_ex: "(k::nat) \<le> l \<Longrightarrow> (\<exists>n. l = k + n)"
   3.633 +lemma le_Suc_ex: "k \<le> l \<Longrightarrow> (\<exists>n. l = k + n)" for k l :: nat
   3.634    by (auto simp: less_Suc_eq_le[symmetric] dest: less_imp_Suc_add)
   3.635  
   3.636  text \<open>strict, in 1st argument; proof is by induction on \<open>k > 0\<close>\<close>
   3.637 @@ -727,173 +724,162 @@
   3.638    fixes i j :: nat
   3.639    assumes "i < j" and "0 < k"
   3.640    shows "k * i < k * j"
   3.641 -using \<open>0 < k\<close> proof (induct k)
   3.642 -  case 0 then show ?case by simp
   3.643 +  using \<open>0 < k\<close>
   3.644 +proof (induct k)
   3.645 +  case 0
   3.646 +  then show ?case by simp
   3.647  next
   3.648 -  case (Suc k) with \<open>i < j\<close> show ?case
   3.649 +  case (Suc k)
   3.650 +  with \<open>i < j\<close> show ?case
   3.651      by (cases k) (simp_all add: add_less_mono)
   3.652  qed
   3.653  
   3.654  text \<open>Addition is the inverse of subtraction:
   3.655    if @{term "n \<le> m"} then @{term "n + (m - n) = m"}.\<close>
   3.656 -lemma add_diff_inverse_nat: "~  m < n ==> n + (m - n) = (m::nat)"
   3.657 -by (induct m n rule: diff_induct) simp_all
   3.658 -
   3.659 -lemma nat_le_iff_add: "(m::nat) \<le> n = (\<exists>k. n = m + k)"
   3.660 -using nat_add_left_cancel_le[of m 0] by (auto dest: le_Suc_ex)
   3.661 +lemma add_diff_inverse_nat: "\<not> m < n \<Longrightarrow> n + (m - n) = m" for m n :: nat
   3.662 +  by (induct m n rule: diff_induct) simp_all
   3.663 +
   3.664 +lemma nat_le_iff_add: "m \<le> n \<longleftrightarrow> (\<exists>k. n = m + k)" for m n :: nat
   3.665 +  using nat_add_left_cancel_le[of m 0] by (auto dest: le_Suc_ex)
   3.666  
   3.667  text\<open>The naturals form an ordered \<open>semidom\<close> and a \<open>dioid\<close>\<close>
   3.668  
   3.669  instance nat :: linordered_semidom
   3.670  proof
   3.671 +  fix m n q :: nat
   3.672    show "0 < (1::nat)" by simp
   3.673 -  show "\<And>m n q :: nat. m \<le> n \<Longrightarrow> q + m \<le> q + n" by simp
   3.674 -  show "\<And>m n q :: nat. m < n \<Longrightarrow> 0 < q \<Longrightarrow> q * m < q * n" by (simp add: mult_less_mono2)
   3.675 -  show "\<And>m n :: nat. m \<noteq> 0 \<Longrightarrow> n \<noteq> 0 \<Longrightarrow> m * n \<noteq> 0" by simp
   3.676 -  show "\<And>m n :: nat. n \<le> m ==> (m - n) + n = (m::nat)"
   3.677 +  show "m \<le> n \<Longrightarrow> q + m \<le> q + n" by simp
   3.678 +  show "m < n \<Longrightarrow> 0 < q \<Longrightarrow> q * m < q * n" by (simp add: mult_less_mono2)
   3.679 +  show "m \<noteq> 0 \<Longrightarrow> n \<noteq> 0 \<Longrightarrow> m * n \<noteq> 0" by simp
   3.680 +  show "n \<le> m \<Longrightarrow> (m - n) + n = m"
   3.681      by (simp add: add_diff_inverse_nat add.commute linorder_not_less)
   3.682  qed
   3.683  
   3.684  instance nat :: dioid
   3.685 -  proof qed (rule nat_le_iff_add)
   3.686 +  by standard (rule nat_le_iff_add)
   3.687  declare le0[simp del] -- \<open>This is now @{thm zero_le}\<close>
   3.688  declare le_0_eq[simp del] -- \<open>This is now @{thm le_zero_eq}\<close>
   3.689  declare not_less0[simp del] -- \<open>This is now @{thm not_less_zero}\<close>
   3.690  declare not_gr0[simp del] -- \<open>This is now @{thm not_gr_zero}\<close>
   3.691  
   3.692 -instance nat :: ordered_cancel_comm_monoid_add
   3.693 -  proof qed
   3.694 -
   3.695 -instance nat :: ordered_cancel_comm_monoid_diff
   3.696 -  proof qed
   3.697 +instance nat :: ordered_cancel_comm_monoid_add ..
   3.698 +instance nat :: ordered_cancel_comm_monoid_diff ..
   3.699 +
   3.700  
   3.701  subsubsection \<open>@{term min} and @{term max}\<close>
   3.702  
   3.703  lemma mono_Suc: "mono Suc"
   3.704 -by (rule monoI) simp
   3.705 -
   3.706 -lemma min_0L [simp]: "min 0 n = (0::nat)"
   3.707 -by (rule min_absorb1) simp
   3.708 -
   3.709 -lemma min_0R [simp]: "min n 0 = (0::nat)"
   3.710 -by (rule min_absorb2) simp
   3.711 +  by (rule monoI) simp
   3.712 +
   3.713 +lemma min_0L [simp]: "min 0 n = 0" for n :: nat
   3.714 +  by (rule min_absorb1) simp
   3.715 +
   3.716 +lemma min_0R [simp]: "min n 0 = 0" for n :: nat
   3.717 +  by (rule min_absorb2) simp
   3.718  
   3.719  lemma min_Suc_Suc [simp]: "min (Suc m) (Suc n) = Suc (min m n)"
   3.720 -by (simp add: mono_Suc min_of_mono)
   3.721 -
   3.722 -lemma min_Suc1:
   3.723 -   "min (Suc n) m = (case m of 0 => 0 | Suc m' => Suc(min n m'))"
   3.724 -by (simp split: nat.split)
   3.725 -
   3.726 -lemma min_Suc2:
   3.727 -   "min m (Suc n) = (case m of 0 => 0 | Suc m' => Suc(min m' n))"
   3.728 -by (simp split: nat.split)
   3.729 -
   3.730 -lemma max_0L [simp]: "max 0 n = (n::nat)"
   3.731 -by (rule max_absorb2) simp
   3.732 -
   3.733 -lemma max_0R [simp]: "max n 0 = (n::nat)"
   3.734 -by (rule max_absorb1) simp
   3.735 -
   3.736 -lemma max_Suc_Suc [simp]: "max (Suc m) (Suc n) = Suc(max m n)"
   3.737 -by (simp add: mono_Suc max_of_mono)
   3.738 -
   3.739 -lemma max_Suc1:
   3.740 -   "max (Suc n) m = (case m of 0 => Suc n | Suc m' => Suc(max n m'))"
   3.741 -by (simp split: nat.split)
   3.742 -
   3.743 -lemma max_Suc2:
   3.744 -   "max m (Suc n) = (case m of 0 => Suc n | Suc m' => Suc(max m' n))"
   3.745 -by (simp split: nat.split)
   3.746 -
   3.747 -lemma nat_mult_min_left:
   3.748 -  fixes m n q :: nat
   3.749 -  shows "min m n * q = min (m * q) (n * q)"
   3.750 -  by (simp add: min_def not_le) (auto dest: mult_right_le_imp_le mult_right_less_imp_less le_less_trans)
   3.751 -
   3.752 -lemma nat_mult_min_right:
   3.753 -  fixes m n q :: nat
   3.754 -  shows "m * min n q = min (m * n) (m * q)"
   3.755 -  by (simp add: min_def not_le) (auto dest: mult_left_le_imp_le mult_left_less_imp_less le_less_trans)
   3.756 -
   3.757 -lemma nat_add_max_left:
   3.758 -  fixes m n q :: nat
   3.759 -  shows "max m n + q = max (m + q) (n + q)"
   3.760 +  by (simp add: mono_Suc min_of_mono)
   3.761 +
   3.762 +lemma min_Suc1: "min (Suc n) m = (case m of 0 \<Rightarrow> 0 | Suc m' \<Rightarrow> Suc(min n m'))"
   3.763 +  by (simp split: nat.split)
   3.764 +
   3.765 +lemma min_Suc2: "min m (Suc n) = (case m of 0 \<Rightarrow> 0 | Suc m' \<Rightarrow> Suc(min m' n))"
   3.766 +  by (simp split: nat.split)
   3.767 +
   3.768 +lemma max_0L [simp]: "max 0 n = n" for n :: nat
   3.769 +  by (rule max_absorb2) simp
   3.770 +
   3.771 +lemma max_0R [simp]: "max n 0 = n" for n :: nat
   3.772 +  by (rule max_absorb1) simp
   3.773 +
   3.774 +lemma max_Suc_Suc [simp]: "max (Suc m) (Suc n) = Suc (max m n)"
   3.775 +  by (simp add: mono_Suc max_of_mono)
   3.776 +
   3.777 +lemma max_Suc1: "max (Suc n) m = (case m of 0 \<Rightarrow> Suc n | Suc m' \<Rightarrow> Suc (max n m'))"
   3.778 +  by (simp split: nat.split)
   3.779 +
   3.780 +lemma max_Suc2: "max m (Suc n) = (case m of 0 \<Rightarrow> Suc n | Suc m' \<Rightarrow> Suc (max m' n))"
   3.781 +  by (simp split: nat.split)
   3.782 +
   3.783 +lemma nat_mult_min_left: "min m n * q = min (m * q) (n * q)" for m n q :: nat
   3.784 +  by (simp add: min_def not_le)
   3.785 +    (auto dest: mult_right_le_imp_le mult_right_less_imp_less le_less_trans)
   3.786 +
   3.787 +lemma nat_mult_min_right: "m * min n q = min (m * n) (m * q)" for m n q :: nat
   3.788 +  by (simp add: min_def not_le)
   3.789 +    (auto dest: mult_left_le_imp_le mult_left_less_imp_less le_less_trans)
   3.790 +
   3.791 +lemma nat_add_max_left: "max m n + q = max (m + q) (n + q)" for m n q :: nat
   3.792    by (simp add: max_def)
   3.793  
   3.794 -lemma nat_add_max_right:
   3.795 -  fixes m n q :: nat
   3.796 -  shows "m + max n q = max (m + n) (m + q)"
   3.797 +lemma nat_add_max_right: "m + max n q = max (m + n) (m + q)" for m n q :: nat
   3.798    by (simp add: max_def)
   3.799  
   3.800 -lemma nat_mult_max_left:
   3.801 -  fixes m n q :: nat
   3.802 -  shows "max m n * q = max (m * q) (n * q)"
   3.803 -  by (simp add: max_def not_le) (auto dest: mult_right_le_imp_le mult_right_less_imp_less le_less_trans)
   3.804 -
   3.805 -lemma nat_mult_max_right:
   3.806 -  fixes m n q :: nat
   3.807 -  shows "m * max n q = max (m * n) (m * q)"
   3.808 -  by (simp add: max_def not_le) (auto dest: mult_left_le_imp_le mult_left_less_imp_less le_less_trans)
   3.809 +lemma nat_mult_max_left: "max m n * q = max (m * q) (n * q)" for m n q :: nat
   3.810 +  by (simp add: max_def not_le)
   3.811 +    (auto dest: mult_right_le_imp_le mult_right_less_imp_less le_less_trans)
   3.812 +
   3.813 +lemma nat_mult_max_right: "m * max n q = max (m * n) (m * q)" for m n q :: nat
   3.814 +  by (simp add: max_def not_le)
   3.815 +    (auto dest: mult_left_le_imp_le mult_left_less_imp_less le_less_trans)
   3.816  
   3.817  
   3.818  subsubsection \<open>Additional theorems about @{term "op \<le>"}\<close>
   3.819  
   3.820  text \<open>Complete induction, aka course-of-values induction\<close>
   3.821  
   3.822 -instance nat :: wellorder proof
   3.823 +instance nat :: wellorder
   3.824 +proof
   3.825    fix P and n :: nat
   3.826 -  assume step: "\<And>n::nat. (\<And>m. m < n \<Longrightarrow> P m) \<Longrightarrow> P n"
   3.827 +  assume step: "(\<And>m. m < n \<Longrightarrow> P m) \<Longrightarrow> P n" for n :: nat
   3.828    have "\<And>q. q \<le> n \<Longrightarrow> P q"
   3.829    proof (induct n)
   3.830      case (0 n)
   3.831      have "P 0" by (rule step) auto
   3.832 -    thus ?case using 0 by auto
   3.833 +    then show ?case using 0 by auto
   3.834    next
   3.835      case (Suc m n)
   3.836      then have "n \<le> m \<or> n = Suc m" by (simp add: le_Suc_eq)
   3.837 -    thus ?case
   3.838 +    then show ?case
   3.839      proof
   3.840 -      assume "n \<le> m" thus "P n" by (rule Suc(1))
   3.841 +      assume "n \<le> m"
   3.842 +      then show "P n" by (rule Suc(1))
   3.843      next
   3.844        assume n: "n = Suc m"
   3.845 -      show "P n"
   3.846 -        by (rule step) (rule Suc(1), simp add: n le_simps)
   3.847 +      show "P n" by (rule step) (rule Suc(1), simp add: n le_simps)
   3.848      qed
   3.849    qed
   3.850    then show "P n" by auto
   3.851  qed
   3.852  
   3.853  
   3.854 -lemma Least_eq_0[simp]: "P(0::nat) \<Longrightarrow> Least P = 0"
   3.855 -by (rule Least_equality[OF _ le0])
   3.856 -
   3.857 -lemma Least_Suc:
   3.858 -     "[| P n; ~ P 0 |] ==> (LEAST n. P n) = Suc (LEAST m. P(Suc m))"
   3.859 +lemma Least_eq_0[simp]: "P 0 \<Longrightarrow> Least P = 0" for P :: "nat \<Rightarrow> bool"
   3.860 +  by (rule Least_equality[OF _ le0])
   3.861 +
   3.862 +lemma Least_Suc: "P n \<Longrightarrow> \<not> P 0 \<Longrightarrow> (LEAST n. P n) = Suc (LEAST m. P (Suc m))"
   3.863    apply (cases n, auto)
   3.864    apply (frule LeastI)
   3.865 -  apply (drule_tac P = "%x. P (Suc x) " in LeastI)
   3.866 +  apply (drule_tac P = "\<lambda>x. P (Suc x) " in LeastI)
   3.867    apply (subgoal_tac " (LEAST x. P x) \<le> Suc (LEAST x. P (Suc x))")
   3.868    apply (erule_tac [2] Least_le)
   3.869    apply (cases "LEAST x. P x", auto)
   3.870 -  apply (drule_tac P = "%x. P (Suc x) " in Least_le)
   3.871 +  apply (drule_tac P = "\<lambda>x. P (Suc x) " in Least_le)
   3.872    apply (blast intro: order_antisym)
   3.873    done
   3.874  
   3.875 -lemma Least_Suc2:
   3.876 -   "[|P n; Q m; ~P 0; !k. P (Suc k) = Q k|] ==> Least P = Suc (Least Q)"
   3.877 +lemma Least_Suc2: "P n \<Longrightarrow> Q m \<Longrightarrow> \<not> P 0 \<Longrightarrow> \<forall>k. P (Suc k) = Q k \<Longrightarrow> Least P = Suc (Least Q)"
   3.878    apply (erule (1) Least_Suc [THEN ssubst])
   3.879    apply simp
   3.880    done
   3.881  
   3.882 -lemma ex_least_nat_le: "\<not>P(0) \<Longrightarrow> P(n::nat) \<Longrightarrow> \<exists>k\<le>n. (\<forall>i<k. \<not>P i) & P(k)"
   3.883 +lemma ex_least_nat_le: "\<not> P 0 \<Longrightarrow> P n \<Longrightarrow> \<exists>k\<le>n. (\<forall>i<k. \<not> P i) \<and> P k" for P :: "nat \<Rightarrow> bool"
   3.884    apply (cases n)
   3.885     apply blast
   3.886 -  apply (rule_tac x="LEAST k. P(k)" in exI)
   3.887 +  apply (rule_tac x="LEAST k. P k" in exI)
   3.888    apply (blast intro: Least_le dest: not_less_Least intro: LeastI_ex)
   3.889    done
   3.890  
   3.891 -lemma ex_least_nat_less: "\<not>P(0) \<Longrightarrow> P(n::nat) \<Longrightarrow> \<exists>k<n. (\<forall>i\<le>k. \<not>P i) & P(k+1)"
   3.892 +lemma ex_least_nat_less: "\<not> P 0 \<Longrightarrow> P n \<Longrightarrow> \<exists>k<n. (\<forall>i\<le>k. \<not> P i) \<and> P (k + 1)" for P :: "nat \<Rightarrow> bool"
   3.893    unfolding One_nat_def
   3.894    apply (cases n)
   3.895     apply blast
   3.896 @@ -907,14 +893,16 @@
   3.897    done
   3.898  
   3.899  lemma nat_less_induct:
   3.900 -  assumes "!!n. \<forall>m::nat. m < n --> P m ==> P n" shows "P n"
   3.901 +  fixes P :: "nat \<Rightarrow> bool"
   3.902 +  assumes "\<And>n. \<forall>m. m < n \<longrightarrow> P m \<Longrightarrow> P n"
   3.903 +  shows "P n"
   3.904    using assms less_induct by blast
   3.905  
   3.906  lemma measure_induct_rule [case_names less]:
   3.907    fixes f :: "'a \<Rightarrow> nat"
   3.908    assumes step: "\<And>x. (\<And>y. f y < f x \<Longrightarrow> P y) \<Longrightarrow> P x"
   3.909    shows "P a"
   3.910 -by (induct m\<equiv>"f a" arbitrary: a rule: less_induct) (auto intro: step)
   3.911 +  by (induct m \<equiv> "f a" arbitrary: a rule: less_induct) (auto intro: step)
   3.912  
   3.913  text \<open>old style induction rules:\<close>
   3.914  lemma measure_induct:
   3.915 @@ -923,18 +911,19 @@
   3.916    by (rule measure_induct_rule [of f P a]) iprover
   3.917  
   3.918  lemma full_nat_induct:
   3.919 -  assumes step: "(!!n. (ALL m. Suc m <= n --> P m) ==> P n)"
   3.920 +  assumes step: "\<And>n. (\<forall>m. Suc m \<le> n \<longrightarrow> P m) \<Longrightarrow> P n"
   3.921    shows "P n"
   3.922    by (rule less_induct) (auto intro: step simp:le_simps)
   3.923  
   3.924 -text\<open>An induction rule for estabilishing binary relations\<close>
   3.925 +text\<open>An induction rule for establishing binary relations\<close>
   3.926  lemma less_Suc_induct [consumes 1]:
   3.927 -  assumes less:  "i < j"
   3.928 -     and  step:  "!!i. P i (Suc i)"
   3.929 -     and  trans: "!!i j k. i < j ==> j < k ==>  P i j ==> P j k ==> P i k"
   3.930 +  assumes less: "i < j"
   3.931 +    and step: "\<And>i. P i (Suc i)"
   3.932 +    and trans: "\<And>i j k. i < j \<Longrightarrow> j < k \<Longrightarrow> P i j \<Longrightarrow> P j k \<Longrightarrow> P i k"
   3.933    shows "P i j"
   3.934  proof -
   3.935 -  from less obtain k where j: "j = Suc (i + k)" by (auto dest: less_imp_Suc_add)
   3.936 +  from less obtain k where j: "j = Suc (i + k)"
   3.937 +    by (auto dest: less_imp_Suc_add)
   3.938    have "P i (Suc (i + k))"
   3.939    proof (induct k)
   3.940      case 0
   3.941 @@ -942,55 +931,60 @@
   3.942    next
   3.943      case (Suc k)
   3.944      have "0 + i < Suc k + i" by (rule add_less_mono1) simp
   3.945 -    hence "i < Suc (i + k)" by (simp add: add.commute)
   3.946 +    then have "i < Suc (i + k)" by (simp add: add.commute)
   3.947      from trans[OF this lessI Suc step]
   3.948      show ?case by simp
   3.949    qed
   3.950 -  thus "P i j" by (simp add: j)
   3.951 +  then show "P i j" by (simp add: j)
   3.952  qed
   3.953  
   3.954 -text \<open>The method of infinite descent, frequently used in number theory.
   3.955 -Provided by Roelof Oosterhuis.
   3.956 -$P(n)$ is true for all $n\in\mathbb{N}$ if
   3.957 -\begin{itemize}
   3.958 -  \item case ``0'': given $n=0$ prove $P(n)$,
   3.959 -  \item case ``smaller'': given $n>0$ and $\neg P(n)$ prove there exists
   3.960 -        a smaller integer $m$ such that $\neg P(m)$.
   3.961 -\end{itemize}\<close>
   3.962 -
   3.963 -text\<open>A compact version without explicit base case:\<close>
   3.964 -lemma infinite_descent:
   3.965 -  "\<lbrakk> !!n::nat. \<not> P n \<Longrightarrow>  \<exists>m<n. \<not>  P m \<rbrakk> \<Longrightarrow>  P n"
   3.966 -by (induct n rule: less_induct) auto
   3.967 -
   3.968 -lemma infinite_descent0[case_names 0 smaller]:
   3.969 -  "\<lbrakk> P 0; !!n. n>0 \<Longrightarrow> \<not> P n \<Longrightarrow> (\<exists>m::nat. m < n \<and> \<not>P m) \<rbrakk> \<Longrightarrow> P n"
   3.970 -by (rule infinite_descent) (case_tac "n>0", auto)
   3.971 -
   3.972  text \<open>
   3.973 -Infinite descent using a mapping to $\mathbb{N}$:
   3.974 -$P(x)$ is true for all $x\in D$ if there exists a $V: D \to \mathbb{N}$ and
   3.975 -\begin{itemize}
   3.976 -\item case ``0'': given $V(x)=0$ prove $P(x)$,
   3.977 -\item case ``smaller'': given $V(x)>0$ and $\neg P(x)$ prove there exists a $y \in D$ such that $V(y)<V(x)$ and $~\neg P(y)$.
   3.978 -\end{itemize}
   3.979 -NB: the proof also shows how to use the previous lemma.\<close>
   3.980 -
   3.981 +  The method of infinite descent, frequently used in number theory.
   3.982 +  Provided by Roelof Oosterhuis.
   3.983 +  \<open>P n\<close> is true for all natural numbers if
   3.984 +  \<^item> case ``0'': given \<open>n = 0\<close> prove \<open>P n\<close>
   3.985 +  \<^item> case ``smaller'': given \<open>n > 0\<close> and \<open>\<not> P n\<close> prove there exists
   3.986 +    a smaller natural number \<open>m\<close> such that \<open>\<not> P m\<close>.
   3.987 +\<close>
   3.988 +
   3.989 +lemma infinite_descent: "(\<And>n. \<not> P n \<Longrightarrow> \<exists>m<n. \<not> P m) \<Longrightarrow> P n" for P :: "nat \<Rightarrow> bool"
   3.990 +  \<comment> \<open>compact version without explicit base case\<close>
   3.991 +  by (induct n rule: less_induct) auto
   3.992 +
   3.993 +lemma infinite_descent0 [case_names 0 smaller]:
   3.994 +  fixes P :: "nat \<Rightarrow> bool"
   3.995 +  assumes "P 0"
   3.996 +    and "\<And>n. n > 0 \<Longrightarrow> \<not> P n \<Longrightarrow> \<exists>m. m < n \<and> \<not> P m"
   3.997 +  shows "P n"
   3.998 +  apply (rule infinite_descent)
   3.999 +  using assms
  3.1000 +  apply (case_tac "n > 0")
  3.1001 +  apply auto
  3.1002 +  done
  3.1003 +
  3.1004 +text \<open>
  3.1005 +  Infinite descent using a mapping to \<open>nat\<close>:
  3.1006 +  \<open>P x\<close> is true for all \<open>x \<in> D\<close> if there exists a \<open>V \<in> D \<Rightarrow> nat\<close> and
  3.1007 +  \<^item> case ``0'': given \<open>V x = 0\<close> prove \<open>P x\<close>
  3.1008 +  \<^item> ``smaller'': given \<open>V x > 0\<close> and \<open>\<not> P x\<close> prove
  3.1009 +  there exists a \<open>y \<in> D\<close> such that \<open>V y < V x\<close> and \<open>\<not> P y\<close>.
  3.1010 +\<close>
  3.1011  corollary infinite_descent0_measure [case_names 0 smaller]:
  3.1012 -  assumes A0: "!!x. V x = (0::nat) \<Longrightarrow> P x"
  3.1013 -    and   A1: "!!x. V x > 0 \<Longrightarrow> \<not>P x \<Longrightarrow> (\<exists>y. V y < V x \<and> \<not>P y)"
  3.1014 +  fixes V :: "'a \<Rightarrow> nat"
  3.1015 +  assumes 1: "\<And>x. V x = 0 \<Longrightarrow> P x"
  3.1016 +    and 2: "\<And>x. V x > 0 \<Longrightarrow> \<not> P x \<Longrightarrow> \<exists>y. V y < V x \<and> \<not> P y"
  3.1017    shows "P x"
  3.1018  proof -
  3.1019    obtain n where "n = V x" by auto
  3.1020    moreover have "\<And>x. V x = n \<Longrightarrow> P x"
  3.1021    proof (induct n rule: infinite_descent0)
  3.1022 -    case 0 \<comment> "i.e. $V(x) = 0$"
  3.1023 -    with A0 show "P x" by auto
  3.1024 -  next \<comment> "now $n>0$ and $P(x)$ does not hold for some $x$ with $V(x)=n$"
  3.1025 +    case 0
  3.1026 +    with 1 show "P x" by auto
  3.1027 +  next
  3.1028      case (smaller n)
  3.1029 -    then obtain x where vxn: "V x = n " and "V x > 0 \<and> \<not> P x" by auto
  3.1030 -    with A1 obtain y where "V y < V x \<and> \<not> P y" by auto
  3.1031 -    with vxn obtain m where "m = V y \<and> m<n \<and> \<not> P y" by auto
  3.1032 +    then obtain x where *: "V x = n " and "V x > 0 \<and> \<not> P x" by auto
  3.1033 +    with 2 obtain y where "V y < V x \<and> \<not> P y" by auto
  3.1034 +    with * obtain m where "m = V y \<and> m < n \<and> \<not> P y" by auto
  3.1035      then show ?case by auto
  3.1036    qed
  3.1037    ultimately show "P x" by auto
  3.1038 @@ -998,96 +992,96 @@
  3.1039  
  3.1040  text\<open>Again, without explicit base case:\<close>
  3.1041  lemma infinite_descent_measure:
  3.1042 -assumes "!!x. \<not> P x \<Longrightarrow> \<exists>y. (V::'a\<Rightarrow>nat) y < V x \<and> \<not> P y" shows "P x"
  3.1043 +  fixes V :: "'a \<Rightarrow> nat"
  3.1044 +  assumes "\<And>x. \<not> P x \<Longrightarrow> \<exists>y. V y < V x \<and> \<not> P y"
  3.1045 +  shows "P x"
  3.1046  proof -
  3.1047    from assms obtain n where "n = V x" by auto
  3.1048 -  moreover have "!!x. V x = n \<Longrightarrow> P x"
  3.1049 +  moreover have "\<And>x. V x = n \<Longrightarrow> P x"
  3.1050    proof (induct n rule: infinite_descent, auto)
  3.1051 -    fix x assume "\<not> P x"
  3.1052 -    with assms show "\<exists>m < V x. \<exists>y. V y = m \<and> \<not> P y" by auto
  3.1053 +    show "\<exists>m < V x. \<exists>y. V y = m \<and> \<not> P y" if "\<not> P x" for x
  3.1054 +      using assms and that by auto
  3.1055    qed
  3.1056    ultimately show "P x" by auto
  3.1057  qed
  3.1058  
  3.1059 -text \<open>A [clumsy] way of lifting \<open><\<close>
  3.1060 -  monotonicity to \<open>\<le>\<close> monotonicity\<close>
  3.1061 +text \<open>A (clumsy) way of lifting \<open><\<close> monotonicity to \<open>\<le>\<close> monotonicity\<close>
  3.1062  lemma less_mono_imp_le_mono:
  3.1063 -  "\<lbrakk> !!i j::nat. i < j \<Longrightarrow> f i < f j; i \<le> j \<rbrakk> \<Longrightarrow> f i \<le> ((f j)::nat)"
  3.1064 -by (simp add: order_le_less) (blast)
  3.1065 +  fixes f :: "nat \<Rightarrow> nat"
  3.1066 +    and i j :: nat
  3.1067 +  assumes "\<And>i j::nat. i < j \<Longrightarrow> f i < f j"
  3.1068 +    and "i \<le> j"
  3.1069 +  shows "f i \<le> f j"
  3.1070 +  using assms by (auto simp add: order_le_less)
  3.1071  
  3.1072  
  3.1073  text \<open>non-strict, in 1st argument\<close>
  3.1074 -lemma add_le_mono1: "i \<le> j ==> i + k \<le> j + (k::nat)"
  3.1075 -by (rule add_right_mono)
  3.1076 +lemma add_le_mono1: "i \<le> j \<Longrightarrow> i + k \<le> j + k" for i j k :: nat
  3.1077 +  by (rule add_right_mono)
  3.1078  
  3.1079  text \<open>non-strict, in both arguments\<close>
  3.1080 -lemma add_le_mono: "[| i \<le> j;  k \<le> l |] ==> i + k \<le> j + (l::nat)"
  3.1081 -by (rule add_mono)
  3.1082 -
  3.1083 -lemma le_add2: "n \<le> ((m + n)::nat)"
  3.1084 +lemma add_le_mono: "i \<le> j \<Longrightarrow> k \<le> l \<Longrightarrow> i + k \<le> j + l" for i j k l :: nat
  3.1085 +  by (rule add_mono)
  3.1086 +
  3.1087 +lemma le_add2: "n \<le> m + n" for m n :: nat
  3.1088    by simp
  3.1089  
  3.1090 -lemma le_add1: "n \<le> ((n + m)::nat)"
  3.1091 +lemma le_add1: "n \<le> n + m" for m n :: nat
  3.1092    by simp
  3.1093  
  3.1094  lemma less_add_Suc1: "i < Suc (i + m)"
  3.1095 -by (rule le_less_trans, rule le_add1, rule lessI)
  3.1096 +  by (rule le_less_trans, rule le_add1, rule lessI)
  3.1097  
  3.1098  lemma less_add_Suc2: "i < Suc (m + i)"
  3.1099 -by (rule le_less_trans, rule le_add2, rule lessI)
  3.1100 -
  3.1101 -lemma less_iff_Suc_add: "(m < n) = (\<exists>k. n = Suc (m + k))"
  3.1102 -by (iprover intro!: less_add_Suc1 less_imp_Suc_add)
  3.1103 -
  3.1104 -lemma trans_le_add1: "(i::nat) \<le> j ==> i \<le> j + m"
  3.1105 -by (rule le_trans, assumption, rule le_add1)
  3.1106 -
  3.1107 -lemma trans_le_add2: "(i::nat) \<le> j ==> i \<le> m + j"
  3.1108 -by (rule le_trans, assumption, rule le_add2)
  3.1109 -
  3.1110 -lemma trans_less_add1: "(i::nat) < j ==> i < j + m"
  3.1111 -by (rule less_le_trans, assumption, rule le_add1)
  3.1112 -
  3.1113 -lemma trans_less_add2: "(i::nat) < j ==> i < m + j"
  3.1114 -by (rule less_le_trans, assumption, rule le_add2)
  3.1115 -
  3.1116 -lemma add_lessD1: "i + j < (k::nat) ==> i < k"
  3.1117 -apply (rule le_less_trans [of _ "i+j"])
  3.1118 -apply (simp_all add: le_add1)
  3.1119 -done
  3.1120 -
  3.1121 -lemma not_add_less1 [iff]: "~ (i + j < (i::nat))"
  3.1122 -apply (rule notI)
  3.1123 -apply (drule add_lessD1)
  3.1124 -apply (erule less_irrefl [THEN notE])
  3.1125 -done
  3.1126 -
  3.1127 -lemma not_add_less2 [iff]: "~ (j + i < (i::nat))"
  3.1128 -by (simp add: add.commute)
  3.1129 -
  3.1130 -lemma add_leD1: "m + k \<le> n ==> m \<le> (n::nat)"
  3.1131 -apply (rule order_trans [of _ "m+k"])
  3.1132 -apply (simp_all add: le_add1)
  3.1133 -done
  3.1134 -
  3.1135 -lemma add_leD2: "m + k \<le> n ==> k \<le> (n::nat)"
  3.1136 -apply (simp add: add.commute)
  3.1137 -apply (erule add_leD1)
  3.1138 -done
  3.1139 -
  3.1140 -lemma add_leE: "(m::nat) + k \<le> n ==> (m \<le> n ==> k \<le> n ==> R) ==> R"
  3.1141 -by (blast dest: add_leD1 add_leD2)
  3.1142 -
  3.1143 -text \<open>needs \<open>!!k\<close> for \<open>ac_simps\<close> to work\<close>
  3.1144 -lemma less_add_eq_less: "!!k::nat. k < l ==> m + l = k + n ==> m < n"
  3.1145 -by (force simp del: add_Suc_right
  3.1146 -    simp add: less_iff_Suc_add add_Suc_right [symmetric] ac_simps)
  3.1147 +  by (rule le_less_trans, rule le_add2, rule lessI)
  3.1148 +
  3.1149 +lemma less_iff_Suc_add: "m < n \<longleftrightarrow> (\<exists>k. n = Suc (m + k))"
  3.1150 +  by (iprover intro!: less_add_Suc1 less_imp_Suc_add)
  3.1151 +
  3.1152 +lemma trans_le_add1: "i \<le> j \<Longrightarrow> i \<le> j + m" for i j m :: nat
  3.1153 +  by (rule le_trans, assumption, rule le_add1)
  3.1154 +
  3.1155 +lemma trans_le_add2: "i \<le> j \<Longrightarrow> i \<le> m + j" for i j m :: nat
  3.1156 +  by (rule le_trans, assumption, rule le_add2)
  3.1157 +
  3.1158 +lemma trans_less_add1: "i < j \<Longrightarrow> i < j + m" for i j m :: nat
  3.1159 +  by (rule less_le_trans, assumption, rule le_add1)
  3.1160 +
  3.1161 +lemma trans_less_add2: "i < j \<Longrightarrow> i < m + j" for i j m :: nat
  3.1162 +  by (rule less_le_trans, assumption, rule le_add2)
  3.1163 +
  3.1164 +lemma add_lessD1: "i + j < k \<Longrightarrow> i < k" for i j k :: nat
  3.1165 +  by (rule le_less_trans [of _ "i+j"]) (simp_all add: le_add1)
  3.1166 +
  3.1167 +lemma not_add_less1 [iff]: "\<not> i + j < i" for i j :: nat
  3.1168 +  apply (rule notI)
  3.1169 +  apply (drule add_lessD1)
  3.1170 +  apply (erule less_irrefl [THEN notE])
  3.1171 +  done
  3.1172 +
  3.1173 +lemma not_add_less2 [iff]: "\<not> j + i < i" for i j :: nat
  3.1174 +  by (simp add: add.commute)
  3.1175 +
  3.1176 +lemma add_leD1: "m + k \<le> n \<Longrightarrow> m \<le> n" for k m n :: nat
  3.1177 +  by (rule order_trans [of _ "m+k"]) (simp_all add: le_add1)
  3.1178 +
  3.1179 +lemma add_leD2: "m + k \<le> n \<Longrightarrow> k \<le> n" for k m n :: nat
  3.1180 +  apply (simp add: add.commute)
  3.1181 +  apply (erule add_leD1)
  3.1182 +  done
  3.1183 +
  3.1184 +lemma add_leE: "m + k \<le> n \<Longrightarrow> (m \<le> n \<Longrightarrow> k \<le> n \<Longrightarrow> R) \<Longrightarrow> R" for k m n :: nat
  3.1185 +  by (blast dest: add_leD1 add_leD2)
  3.1186 +
  3.1187 +text \<open>needs \<open>\<And>k\<close> for \<open>ac_simps\<close> to work\<close>
  3.1188 +lemma less_add_eq_less: "\<And>k::nat. k < l \<Longrightarrow> m + l = k + n \<Longrightarrow> m < n"
  3.1189 +  by (force simp del: add_Suc_right simp add: less_iff_Suc_add add_Suc_right [symmetric] ac_simps)
  3.1190  
  3.1191  
  3.1192  subsubsection \<open>More results about difference\<close>
  3.1193  
  3.1194 -lemma Suc_diff_le: "n \<le> m ==> Suc m - n = Suc (m - n)"
  3.1195 -by (induct m n rule: diff_induct) simp_all
  3.1196 +lemma Suc_diff_le: "n \<le> m \<Longrightarrow> Suc m - n = Suc (m - n)"
  3.1197 +  by (induct m n rule: diff_induct) simp_all
  3.1198  
  3.1199  lemma diff_less_Suc: "m - n < Suc m"
  3.1200  apply (induct m n rule: diff_induct)
  3.1201 @@ -1095,80 +1089,72 @@
  3.1202  apply (simp_all add: less_Suc_eq)
  3.1203  done
  3.1204  
  3.1205 -lemma diff_le_self [simp]: "m - n \<le> (m::nat)"
  3.1206 -by (induct m n rule: diff_induct) (simp_all add: le_SucI)
  3.1207 -
  3.1208 -lemma less_imp_diff_less: "(j::nat) < k ==> j - n < k"
  3.1209 -by (rule le_less_trans, rule diff_le_self)
  3.1210 -
  3.1211 -lemma diff_Suc_less [simp]: "0<n ==> n - Suc i < n"
  3.1212 -by (cases n) (auto simp add: le_simps)
  3.1213 -
  3.1214 -lemma diff_add_assoc: "k \<le> (j::nat) ==> (i + j) - k = i + (j - k)"
  3.1215 -by (induct j k rule: diff_induct) simp_all
  3.1216 -
  3.1217 -lemma add_diff_assoc [simp]:
  3.1218 -  fixes i j k :: nat
  3.1219 -  shows "k \<le> j \<Longrightarrow> i + (j - k) = i + j - k"
  3.1220 +lemma diff_le_self [simp]: "m - n \<le> m" for m n :: nat
  3.1221 +  by (induct m n rule: diff_induct) (simp_all add: le_SucI)
  3.1222 +
  3.1223 +lemma less_imp_diff_less: "j < k \<Longrightarrow> j - n < k" for j k n :: nat
  3.1224 +  by (rule le_less_trans, rule diff_le_self)
  3.1225 +
  3.1226 +lemma diff_Suc_less [simp]: "0 < n \<Longrightarrow> n - Suc i < n"
  3.1227 +  by (cases n) (auto simp add: le_simps)
  3.1228 +
  3.1229 +lemma diff_add_assoc: "k \<le> j \<Longrightarrow> (i + j) - k = i + (j - k)" for i j k :: nat
  3.1230 +  by (induct j k rule: diff_induct) simp_all
  3.1231 +
  3.1232 +lemma add_diff_assoc [simp]: "k \<le> j \<Longrightarrow> i + (j - k) = i + j - k" for i j k :: nat
  3.1233    by (fact diff_add_assoc [symmetric])
  3.1234  
  3.1235 -lemma diff_add_assoc2: "k \<le> (j::nat) ==> (j + i) - k = (j - k) + i"
  3.1236 +lemma diff_add_assoc2: "k \<le> j \<Longrightarrow> (j + i) - k = (j - k) + i" for i j k :: nat
  3.1237    by (simp add: ac_simps)
  3.1238  
  3.1239 -lemma add_diff_assoc2 [simp]:
  3.1240 -  fixes i j k :: nat
  3.1241 -  shows "k \<le> j \<Longrightarrow> j - k + i = j + i - k"
  3.1242 +lemma add_diff_assoc2 [simp]: "k \<le> j \<Longrightarrow> j - k + i = j + i - k" for i j k :: nat
  3.1243    by (fact diff_add_assoc2 [symmetric])
  3.1244  
  3.1245 -lemma le_imp_diff_is_add: "i \<le> (j::nat) ==> (j - i = k) = (j = k + i)"
  3.1246 -by auto
  3.1247 -
  3.1248 -lemma diff_is_0_eq [simp]: "((m::nat) - n = 0) = (m \<le> n)"
  3.1249 -by (induct m n rule: diff_induct) simp_all
  3.1250 -
  3.1251 -lemma diff_is_0_eq' [simp]: "m \<le> n ==> (m::nat) - n = 0"
  3.1252 -by (rule iffD2, rule diff_is_0_eq)
  3.1253 -
  3.1254 -lemma zero_less_diff [simp]: "(0 < n - (m::nat)) = (m < n)"
  3.1255 -by (induct m n rule: diff_induct) simp_all
  3.1256 +lemma le_imp_diff_is_add: "i \<le> j \<Longrightarrow> (j - i = k) = (j = k + i)" for i j k :: nat
  3.1257 +  by auto
  3.1258 +
  3.1259 +lemma diff_is_0_eq [simp]: "m - n = 0 \<longleftrightarrow> m \<le> n" for m n :: nat
  3.1260 +  by (induct m n rule: diff_induct) simp_all
  3.1261 +
  3.1262 +lemma diff_is_0_eq' [simp]: "m \<le> n \<Longrightarrow> m - n = 0" for m n :: nat
  3.1263 +  by (rule iffD2, rule diff_is_0_eq)
  3.1264 +
  3.1265 +lemma zero_less_diff [simp]: "0 < n - m \<longleftrightarrow> m < n" for m n :: nat
  3.1266 +  by (induct m n rule: diff_induct) simp_all
  3.1267  
  3.1268  lemma less_imp_add_positive:
  3.1269    assumes "i < j"
  3.1270 -  shows "\<exists>k::nat. 0 < k & i + k = j"
  3.1271 +  shows "\<exists>k::nat. 0 < k \<and> i + k = j"
  3.1272  proof
  3.1273 -  from assms show "0 < j - i & i + (j - i) = j"
  3.1274 +  from assms show "0 < j - i \<and> i + (j - i) = j"
  3.1275      by (simp add: order_less_imp_le)
  3.1276  qed
  3.1277  
  3.1278  text \<open>a nice rewrite for bounded subtraction\<close>
  3.1279 -lemma nat_minus_add_max:
  3.1280 -  fixes n m :: nat
  3.1281 -  shows "n - m + m = max n m"
  3.1282 +lemma nat_minus_add_max: "n - m + m = max n m" for m n :: nat
  3.1283      by (simp add: max_def not_le order_less_imp_le)
  3.1284  
  3.1285 -lemma nat_diff_split:
  3.1286 -  fixes a b :: nat
  3.1287 -  shows "P (a - b) \<longleftrightarrow> (a < b \<longrightarrow> P 0) \<and> (\<forall>d. a = b + d \<longrightarrow> P d)"
  3.1288 +lemma nat_diff_split: "P (a - b) \<longleftrightarrow> (a < b \<longrightarrow> P 0) \<and> (\<forall>d. a = b + d \<longrightarrow> P d)"
  3.1289 +  for a b :: nat
  3.1290      \<comment> \<open>elimination of \<open>-\<close> on \<open>nat\<close>\<close>
  3.1291    by (cases "a < b")
  3.1292      (auto simp add: not_less le_less dest!: add_eq_self_zero [OF sym])
  3.1293  
  3.1294 -lemma nat_diff_split_asm:
  3.1295 -  fixes a b :: nat
  3.1296 -  shows "P (a - b) \<longleftrightarrow> \<not> (a < b \<and> \<not> P 0 \<or> (\<exists>d. a = b + d \<and> \<not> P d))"
  3.1297 +lemma nat_diff_split_asm: "P (a - b) \<longleftrightarrow> \<not> (a < b \<and> \<not> P 0 \<or> (\<exists>d. a = b + d \<and> \<not> P d))"
  3.1298 +  for a b :: nat
  3.1299      \<comment> \<open>elimination of \<open>-\<close> on \<open>nat\<close> in assumptions\<close>
  3.1300    by (auto split: nat_diff_split)
  3.1301  
  3.1302 -lemma Suc_pred': "0 < n ==> n = Suc(n - 1)"
  3.1303 +lemma Suc_pred': "0 < n \<Longrightarrow> n = Suc(n - 1)"
  3.1304    by simp
  3.1305  
  3.1306 -lemma add_eq_if: "(m::nat) + n = (if m=0 then n else Suc ((m - 1) + n))"
  3.1307 +lemma add_eq_if: "m + n = (if m = 0 then n else Suc ((m - 1) + n))"
  3.1308    unfolding One_nat_def by (cases m) simp_all
  3.1309  
  3.1310 -lemma mult_eq_if: "(m::nat) * n = (if m=0 then 0 else n + ((m - 1) * n))"
  3.1311 +lemma mult_eq_if: "m * n = (if m = 0 then 0 else n + ((m - 1) * n))" for m n :: nat
  3.1312    unfolding One_nat_def by (cases m) simp_all
  3.1313  
  3.1314 -lemma Suc_diff_eq_diff_pred: "0 < n ==> Suc m - n = m - (n - 1)"
  3.1315 +lemma Suc_diff_eq_diff_pred: "0 < n \<Longrightarrow> Suc m - n = m - (n - 1)"
  3.1316    unfolding One_nat_def by (cases n) simp_all
  3.1317  
  3.1318  lemma diff_Suc_eq_diff_pred: "m - Suc n = (m - 1) - n"
  3.1319 @@ -1180,68 +1166,68 @@
  3.1320  
  3.1321  subsubsection \<open>Monotonicity of multiplication\<close>
  3.1322  
  3.1323 -lemma mult_le_mono1: "i \<le> (j::nat) ==> i * k \<le> j * k"
  3.1324 -by (simp add: mult_right_mono)
  3.1325 -
  3.1326 -lemma mult_le_mono2: "i \<le> (j::nat) ==> k * i \<le> k * j"
  3.1327 -by (simp add: mult_left_mono)
  3.1328 +lemma mult_le_mono1: "i \<le> j \<Longrightarrow> i * k \<le> j * k" for i j k :: nat
  3.1329 +  by (simp add: mult_right_mono)
  3.1330 +
  3.1331 +lemma mult_le_mono2: "i \<le> j \<Longrightarrow> k * i \<le> k * j" for i j k :: nat
  3.1332 +  by (simp add: mult_left_mono)
  3.1333  
  3.1334  text \<open>\<open>\<le>\<close> monotonicity, BOTH arguments\<close>
  3.1335 -lemma mult_le_mono: "i \<le> (j::nat) ==> k \<le> l ==> i * k \<le> j * l"
  3.1336 -by (simp add: mult_mono)
  3.1337 -
  3.1338 -lemma mult_less_mono1: "(i::nat) < j ==> 0 < k ==> i * k < j * k"
  3.1339 -by (simp add: mult_strict_right_mono)
  3.1340 +lemma mult_le_mono: "i \<le> j \<Longrightarrow> k \<le> l \<Longrightarrow> i * k \<le> j * l" for i j k l :: nat
  3.1341 +  by (simp add: mult_mono)
  3.1342 +
  3.1343 +lemma mult_less_mono1: "i < j \<Longrightarrow> 0 < k \<Longrightarrow> i * k < j * k" for i j k :: nat
  3.1344 +  by (simp add: mult_strict_right_mono)
  3.1345  
  3.1346  text\<open>Differs from the standard \<open>zero_less_mult_iff\<close> in that
  3.1347        there are no negative numbers.\<close>
  3.1348 -lemma nat_0_less_mult_iff [simp]: "(0 < (m::nat) * n) = (0 < m & 0 < n)"
  3.1349 +lemma nat_0_less_mult_iff [simp]: "0 < m * n \<longleftrightarrow> 0 < m \<and> 0 < n" for m n :: nat
  3.1350    apply (induct m)
  3.1351     apply simp
  3.1352    apply (case_tac n)
  3.1353     apply simp_all
  3.1354    done
  3.1355  
  3.1356 -lemma one_le_mult_iff [simp]: "(Suc 0 \<le> m * n) = (Suc 0 \<le> m & Suc 0 \<le> n)"
  3.1357 +lemma one_le_mult_iff [simp]: "Suc 0 \<le> m * n \<longleftrightarrow> Suc 0 \<le> m \<and> Suc 0 \<le> n"
  3.1358    apply (induct m)
  3.1359     apply simp
  3.1360    apply (case_tac n)
  3.1361     apply simp_all
  3.1362    done
  3.1363  
  3.1364 -lemma mult_less_cancel2 [simp]: "((m::nat) * k < n * k) = (0 < k & m < n)"
  3.1365 +lemma mult_less_cancel2 [simp]: "m * k < n * k \<longleftrightarrow> 0 < k \<and> m < n" for k m n :: nat
  3.1366    apply (safe intro!: mult_less_mono1)
  3.1367    apply (cases k, auto)
  3.1368 -  apply (simp del: le_0_eq add: linorder_not_le [symmetric])
  3.1369 +  apply (simp add: linorder_not_le [symmetric])
  3.1370    apply (blast intro: mult_le_mono1)
  3.1371    done
  3.1372  
  3.1373 -lemma mult_less_cancel1 [simp]: "(k * (m::nat) < k * n) = (0 < k & m < n)"
  3.1374 -by (simp add: mult.commute [of k])
  3.1375 -
  3.1376 -lemma mult_le_cancel1 [simp]: "(k * (m::nat) \<le> k * n) = (0 < k --> m \<le> n)"
  3.1377 -by (simp add: linorder_not_less [symmetric], auto)
  3.1378 -
  3.1379 -lemma mult_le_cancel2 [simp]: "((m::nat) * k \<le> n * k) = (0 < k --> m \<le> n)"
  3.1380 -by (simp add: linorder_not_less [symmetric], auto)
  3.1381 -
  3.1382 -lemma Suc_mult_less_cancel1: "(Suc k * m < Suc k * n) = (m < n)"
  3.1383 -by (subst mult_less_cancel1) simp
  3.1384 -
  3.1385 -lemma Suc_mult_le_cancel1: "(Suc k * m \<le> Suc k * n) = (m \<le> n)"
  3.1386 -by (subst mult_le_cancel1) simp
  3.1387 -
  3.1388 -lemma le_square: "m \<le> m * (m::nat)"
  3.1389 +lemma mult_less_cancel1 [simp]: "k * m < k * n \<longleftrightarrow> 0 < k \<and> m < n" for k m n :: nat
  3.1390 +  by (simp add: mult.commute [of k])
  3.1391 +
  3.1392 +lemma mult_le_cancel1 [simp]: "k * m \<le> k * n \<longleftrightarrow> (0 < k \<longrightarrow> m \<le> n)" for k m n :: nat
  3.1393 +  by (simp add: linorder_not_less [symmetric], auto)
  3.1394 +
  3.1395 +lemma mult_le_cancel2 [simp]: "m * k \<le> n * k \<longleftrightarrow> (0 < k \<longrightarrow> m \<le> n)" for k m n :: nat
  3.1396 +  by (simp add: linorder_not_less [symmetric], auto)
  3.1397 +
  3.1398 +lemma Suc_mult_less_cancel1: "Suc k * m < Suc k * n \<longleftrightarrow> m < n"
  3.1399 +  by (subst mult_less_cancel1) simp
  3.1400 +
  3.1401 +lemma Suc_mult_le_cancel1: "Suc k * m \<le> Suc k * n \<longleftrightarrow> m \<le> n"
  3.1402 +  by (subst mult_le_cancel1) simp
  3.1403 +
  3.1404 +lemma le_square: "m \<le> m * m" for m :: nat
  3.1405    by (cases m) (auto intro: le_add1)
  3.1406  
  3.1407 -lemma le_cube: "(m::nat) \<le> m * (m * m)"
  3.1408 +lemma le_cube: "m \<le> m * (m * m)" for m :: nat
  3.1409    by (cases m) (auto intro: le_add1)
  3.1410  
  3.1411  text \<open>Lemma for \<open>gcd\<close>\<close>
  3.1412 -lemma mult_eq_self_implies_10: "(m::nat) = m * n ==> n = 1 | m = 0"
  3.1413 +lemma mult_eq_self_implies_10: "m = m * n \<Longrightarrow> n = 1 \<or> m = 0" for m n :: nat
  3.1414    apply (drule sym)
  3.1415    apply (rule disjCI)
  3.1416 -  apply (rule nat_less_cases, erule_tac [2] _)
  3.1417 +  apply (rule linorder_cases, erule_tac [2] _)
  3.1418     apply (drule_tac [2] mult_less_mono2)
  3.1419      apply (auto)
  3.1420    done
  3.1421 @@ -1261,15 +1247,14 @@
  3.1422  instantiation nat :: distrib_lattice
  3.1423  begin
  3.1424  
  3.1425 -definition
  3.1426 -  "(inf :: nat \<Rightarrow> nat \<Rightarrow> nat) = min"
  3.1427 -
  3.1428 -definition
  3.1429 -  "(sup :: nat \<Rightarrow> nat \<Rightarrow> nat) = max"
  3.1430 -
  3.1431 -instance by intro_classes
  3.1432 -  (auto simp add: inf_nat_def sup_nat_def max_def not_le min_def
  3.1433 -    intro: order_less_imp_le antisym elim!: order_trans order_less_trans)
  3.1434 +definition "(inf :: nat \<Rightarrow> nat \<Rightarrow> nat) = min"
  3.1435 +
  3.1436 +definition "(sup :: nat \<Rightarrow> nat \<Rightarrow> nat) = max"
  3.1437 +
  3.1438 +instance
  3.1439 +  by intro_classes
  3.1440 +    (auto simp add: inf_nat_def sup_nat_def max_def not_le min_def
  3.1441 +      intro: order_less_imp_le antisym elim!: order_trans order_less_trans)
  3.1442  
  3.1443  end
  3.1444  
  3.1445 @@ -1283,8 +1268,8 @@
  3.1446  
  3.1447  consts compow :: "nat \<Rightarrow> 'a \<Rightarrow> 'a"
  3.1448  
  3.1449 -abbreviation compower :: "'a \<Rightarrow> nat \<Rightarrow> 'a" (infixr "^^" 80) where
  3.1450 -  "f ^^ n \<equiv> compow n f"
  3.1451 +abbreviation compower :: "'a \<Rightarrow> nat \<Rightarrow> 'a" (infixr "^^" 80)
  3.1452 +  where "f ^^ n \<equiv> compow n f"
  3.1453  
  3.1454  notation (latex output)
  3.1455    compower ("(_\<^bsup>_\<^esup>)" [1000] 1000)
  3.1456 @@ -1292,7 +1277,7 @@
  3.1457  text \<open>\<open>f ^^ n = f o ... o f\<close>, the n-fold composition of \<open>f\<close>\<close>
  3.1458  
  3.1459  overloading
  3.1460 -  funpow == "compow :: nat \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> ('a \<Rightarrow> 'a)"
  3.1461 +  funpow \<equiv> "compow :: nat \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> ('a \<Rightarrow> 'a)"
  3.1462  begin
  3.1463  
  3.1464  primrec funpow :: "nat \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a" where
  3.1465 @@ -1304,10 +1289,10 @@
  3.1466  lemma funpow_0 [simp]: "(f ^^ 0) x = x"
  3.1467    by simp
  3.1468  
  3.1469 -lemma funpow_Suc_right:
  3.1470 -  "f ^^ Suc n = f ^^ n \<circ> f"
  3.1471 +lemma funpow_Suc_right: "f ^^ Suc n = f ^^ n \<circ> f"
  3.1472  proof (induct n)
  3.1473 -  case 0 then show ?case by simp
  3.1474 +  case 0
  3.1475 +  then show ?case by simp
  3.1476  next
  3.1477    fix n
  3.1478    assume "f ^^ Suc n = f ^^ n \<circ> f"
  3.1479 @@ -1319,27 +1304,23 @@
  3.1480  
  3.1481  text \<open>for code generation\<close>
  3.1482  
  3.1483 -definition funpow :: "nat \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a" where
  3.1484 -  funpow_code_def [code_abbrev]: "funpow = compow"
  3.1485 +definition funpow :: "nat \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a"
  3.1486 +  where funpow_code_def [code_abbrev]: "funpow = compow"
  3.1487  
  3.1488  lemma [code]:
  3.1489 -  "funpow (Suc n) f = f o funpow n f"
  3.1490 +  "funpow (Suc n) f = f \<circ> funpow n f"
  3.1491    "funpow 0 f = id"
  3.1492    by (simp_all add: funpow_code_def)
  3.1493  
  3.1494  hide_const (open) funpow
  3.1495  
  3.1496 -lemma funpow_add:
  3.1497 -  "f ^^ (m + n) = f ^^ m \<circ> f ^^ n"
  3.1498 +lemma funpow_add: "f ^^ (m + n) = f ^^ m \<circ> f ^^ n"
  3.1499    by (induct m) simp_all
  3.1500  
  3.1501 -lemma funpow_mult:
  3.1502 -  fixes f :: "'a \<Rightarrow> 'a"
  3.1503 -  shows "(f ^^ m) ^^ n = f ^^ (m * n)"
  3.1504 +lemma funpow_mult: "(f ^^ m) ^^ n = f ^^ (m * n)" for f :: "'a \<Rightarrow> 'a"
  3.1505    by (induct n) (simp_all add: funpow_add)
  3.1506  
  3.1507 -lemma funpow_swap1:
  3.1508 -  "f ((f ^^ n) x) = (f ^^ n) (f x)"
  3.1509 +lemma funpow_swap1: "f ((f ^^ n) x) = (f ^^ n) (f x)"
  3.1510  proof -
  3.1511    have "f ((f ^^ n) x) = (f ^^ (n + 1)) x" by simp
  3.1512    also have "\<dots>  = (f ^^ n o f ^^ 1) x" by (simp only: funpow_add)
  3.1513 @@ -1347,9 +1328,7 @@
  3.1514    finally show ?thesis .
  3.1515  qed
  3.1516  
  3.1517 -lemma comp_funpow:
  3.1518 -  fixes f :: "'a \<Rightarrow> 'a"
  3.1519 -  shows "comp f ^^ n = comp (f ^^ n)"
  3.1520 +lemma comp_funpow: "comp f ^^ n = comp (f ^^ n)" for f :: "'a \<Rightarrow> 'a"
  3.1521    by (induct n) simp_all
  3.1522  
  3.1523  lemma Suc_funpow[simp]: "Suc ^^ n = (op + n)"
  3.1524 @@ -1358,43 +1337,46 @@
  3.1525  lemma id_funpow[simp]: "id ^^ n = id"
  3.1526    by (induct n) simp_all
  3.1527  
  3.1528 -lemma funpow_mono:
  3.1529 -  fixes f :: "'a \<Rightarrow> ('a::lattice)"
  3.1530 -  shows "mono f \<Longrightarrow> A \<le> B \<Longrightarrow> (f ^^ n) A \<le> (f ^^ n) B"
  3.1531 +lemma funpow_mono: "mono f \<Longrightarrow> A \<le> B \<Longrightarrow> (f ^^ n) A \<le> (f ^^ n) B"
  3.1532 +  for f :: "'a \<Rightarrow> ('a::lattice)"
  3.1533    by (induct n arbitrary: A B)
  3.1534       (auto simp del: funpow.simps(2) simp add: funpow_Suc_right mono_def)
  3.1535  
  3.1536 +
  3.1537  subsection \<open>Kleene iteration\<close>
  3.1538  
  3.1539  lemma Kleene_iter_lpfp:
  3.1540 -assumes "mono f" and "f p \<le> p" shows "(f^^k) (bot::'a::order_bot) \<le> p"
  3.1541 +  assumes "mono f"
  3.1542 +    and "f p \<le> p"
  3.1543 +  shows "(f^^k) (bot::'a::order_bot) \<le> p"
  3.1544  proof(induction k)
  3.1545 -  case 0 show ?case by simp
  3.1546 +  case 0
  3.1547 +  show ?case by simp
  3.1548  next
  3.1549    case Suc
  3.1550 -  from monoD[OF assms(1) Suc] assms(2)
  3.1551 -  show ?case by simp
  3.1552 +  from monoD[OF assms(1) Suc] assms(2) show ?case by simp
  3.1553  qed
  3.1554  
  3.1555 -lemma lfp_Kleene_iter: assumes "mono f" and "(f^^Suc k) bot = (f^^k) bot"
  3.1556 -shows "lfp f = (f^^k) bot"
  3.1557 -proof(rule antisym)
  3.1558 +lemma lfp_Kleene_iter:
  3.1559 +  assumes "mono f"
  3.1560 +    and "(f^^Suc k) bot = (f^^k) bot"
  3.1561 +  shows "lfp f = (f^^k) bot"
  3.1562 +proof (rule antisym)
  3.1563    show "lfp f \<le> (f^^k) bot"
  3.1564 -  proof(rule lfp_lowerbound)
  3.1565 -    show "f ((f^^k) bot) \<le> (f^^k) bot" using assms(2) by simp
  3.1566 +  proof (rule lfp_lowerbound)
  3.1567 +    show "f ((f^^k) bot) \<le> (f^^k) bot"
  3.1568 +      using assms(2) by simp
  3.1569    qed
  3.1570 -next
  3.1571    show "(f^^k) bot \<le> lfp f"
  3.1572      using Kleene_iter_lpfp[OF assms(1)] lfp_unfold[OF assms(1)] by simp
  3.1573  qed
  3.1574  
  3.1575 -lemma mono_pow:
  3.1576 -  fixes f :: "'a \<Rightarrow> 'a::complete_lattice"
  3.1577 -  shows "mono f \<Longrightarrow> mono (f ^^ n)"
  3.1578 -  by (induction n) (auto simp: mono_def)
  3.1579 +lemma mono_pow: "mono f \<Longrightarrow> mono (f ^^ n)" for f :: "'a \<Rightarrow> 'a::complete_lattice"
  3.1580 +  by (induct n) (auto simp: mono_def)
  3.1581  
  3.1582  lemma lfp_funpow:
  3.1583 -  assumes f: "mono f" shows "lfp (f ^^ Suc n) = lfp f"
  3.1584 +  assumes f: "mono f"
  3.1585 +  shows "lfp (f ^^ Suc n) = lfp f"
  3.1586  proof (rule antisym)
  3.1587    show "lfp f \<le> lfp (f ^^ Suc n)"
  3.1588    proof (rule lfp_lowerbound)
  3.1589 @@ -1404,13 +1386,14 @@
  3.1590        by (simp add: comp_def)
  3.1591    qed
  3.1592    have "(f^^n) (lfp f) = lfp f" for n
  3.1593 -    by (induction n) (auto intro: f lfp_unfold[symmetric])
  3.1594 +    by (induct n) (auto intro: f lfp_unfold[symmetric])
  3.1595    then show "lfp (f^^Suc n) \<le> lfp f"
  3.1596      by (intro lfp_lowerbound) (simp del: funpow.simps)
  3.1597  qed
  3.1598  
  3.1599  lemma gfp_funpow:
  3.1600 -  assumes f: "mono f" shows "gfp (f ^^ Suc n) = gfp f"
  3.1601 +  assumes f: "mono f"
  3.1602 +  shows "gfp (f ^^ Suc n) = gfp f"
  3.1603  proof (rule antisym)
  3.1604    show "gfp f \<ge> gfp (f ^^ Suc n)"
  3.1605    proof (rule gfp_upperbound)
  3.1606 @@ -1420,18 +1403,19 @@
  3.1607        by (simp add: comp_def)
  3.1608    qed
  3.1609    have "(f^^n) (gfp f) = gfp f" for n
  3.1610 -    by (induction n) (auto intro: f gfp_unfold[symmetric])
  3.1611 +    by (induct n) (auto intro: f gfp_unfold[symmetric])
  3.1612    then show "gfp (f^^Suc n) \<ge> gfp f"
  3.1613      by (intro gfp_upperbound) (simp del: funpow.simps)
  3.1614  qed
  3.1615  
  3.1616 +
  3.1617  subsection \<open>Embedding of the naturals into any \<open>semiring_1\<close>: @{term of_nat}\<close>
  3.1618  
  3.1619  context semiring_1
  3.1620  begin
  3.1621  
  3.1622 -definition of_nat :: "nat \<Rightarrow> 'a" where
  3.1623 -  "of_nat n = (plus 1 ^^ n) 0"
  3.1624 +definition of_nat :: "nat \<Rightarrow> 'a"
  3.1625 +  where "of_nat n = (plus 1 ^^ n) 0"
  3.1626  
  3.1627  lemma of_nat_simps [simp]:
  3.1628    shows of_nat_0: "of_nat 0 = 0"
  3.1629 @@ -1448,16 +1432,16 @@
  3.1630    by (induct m) (simp_all add: ac_simps distrib_right)
  3.1631  
  3.1632  lemma mult_of_nat_commute: "of_nat x * y = y * of_nat x"
  3.1633 -  by (induction x) (simp_all add: algebra_simps)
  3.1634 +  by (induct x) (simp_all add: algebra_simps)
  3.1635  
  3.1636  primrec of_nat_aux :: "('a \<Rightarrow> 'a) \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> 'a" where
  3.1637    "of_nat_aux inc 0 i = i"
  3.1638  | "of_nat_aux inc (Suc n) i = of_nat_aux inc n (inc i)" \<comment> \<open>tail recursive\<close>
  3.1639  
  3.1640 -lemma of_nat_code:
  3.1641 -  "of_nat n = of_nat_aux (\<lambda>i. i + 1) n 0"
  3.1642 +lemma of_nat_code: "of_nat n = of_nat_aux (\<lambda>i. i + 1) n 0"
  3.1643  proof (induct n)
  3.1644 -  case 0 then show ?case by simp
  3.1645 +  case 0
  3.1646 +  then show ?case by simp
  3.1647  next
  3.1648    case (Suc n)
  3.1649    have "\<And>i. of_nat_aux (\<lambda>i. i + 1) n (i + 1) = of_nat_aux (\<lambda>i. i + 1) n i + 1"
  3.1650 @@ -1475,11 +1459,11 @@
  3.1651  begin
  3.1652  
  3.1653  lemma of_nat_diff: "n \<le> m \<Longrightarrow> of_nat (m - n) = of_nat m - of_nat n"
  3.1654 -by (simp add: algebra_simps of_nat_add [symmetric])
  3.1655 +  by (simp add: algebra_simps of_nat_add [symmetric])
  3.1656  
  3.1657  end
  3.1658  
  3.1659 -text\<open>Class for unital semirings with characteristic zero.
  3.1660 +text \<open>Class for unital semirings with characteristic zero.
  3.1661   Includes non-ordered rings like the complex numbers.\<close>
  3.1662  
  3.1663  class semiring_char_0 = semiring_1 +
  3.1664 @@ -1489,7 +1473,7 @@
  3.1665  lemma of_nat_eq_iff [simp]: "of_nat m = of_nat n \<longleftrightarrow> m = n"
  3.1666    by (auto intro: inj_of_nat injD)
  3.1667  
  3.1668 -text\<open>Special cases where either operand is zero\<close>
  3.1669 +text \<open>Special cases where either operand is zero\<close>
  3.1670  
  3.1671  lemma of_nat_0_eq_iff [simp]: "0 = of_nat n \<longleftrightarrow> 0 = n"
  3.1672    by (fact of_nat_eq_iff [of 0 n, unfolded of_nat_0])
  3.1673 @@ -1530,12 +1514,12 @@
  3.1674  lemma of_nat_less_imp_less: "of_nat m < of_nat n \<Longrightarrow> m < n"
  3.1675    by simp
  3.1676  
  3.1677 -text\<open>Every \<open>linordered_semidom\<close> has characteristic zero.\<close>
  3.1678 -
  3.1679 -subclass semiring_char_0 proof
  3.1680 -qed (auto intro!: injI simp add: eq_iff)
  3.1681 -
  3.1682 -text\<open>Special cases where either operand is zero\<close>
  3.1683 +text \<open>Every \<open>linordered_semidom\<close> has characteristic zero.\<close>
  3.1684 +
  3.1685 +subclass semiring_char_0
  3.1686 +  by standard (auto intro!: injI simp add: eq_iff)
  3.1687 +
  3.1688 +text \<open>Special cases where either operand is zero\<close>
  3.1689  
  3.1690  lemma of_nat_le_0_iff [simp]: "of_nat m \<le> 0 \<longleftrightarrow> m = 0"
  3.1691    by (rule of_nat_le_iff [of _ 0, simplified])
  3.1692 @@ -1615,9 +1599,9 @@
  3.1693  subsection \<open>Further arithmetic facts concerning the natural numbers\<close>
  3.1694  
  3.1695  lemma subst_equals:
  3.1696 -  assumes 1: "t = s" and 2: "u = t"
  3.1697 +  assumes "t = s" and "u = t"
  3.1698    shows "u = s"
  3.1699 -  using 2 1 by (rule trans)
  3.1700 +  using assms(2,1) by (rule trans)
  3.1701  
  3.1702  ML_file "Tools/nat_arith.ML"
  3.1703  
  3.1704 @@ -1647,7 +1631,10 @@
  3.1705    case True
  3.1706    then show ?thesis
  3.1707      by (induct n n' rule: less_Suc_induct) (auto intro: mono)
  3.1708 -qed (insert \<open>n \<le> n'\<close>, auto) \<comment> \<open>trivial for @{prop "n = n'"}\<close>
  3.1709 +next
  3.1710 +  case False
  3.1711 +  with \<open>n \<le> n'\<close> show ?thesis by auto
  3.1712 +qed
  3.1713  
  3.1714  lemma lift_Suc_antimono_le:
  3.1715    assumes mono: "\<And>n. f n \<ge> f (Suc n)" and "n \<le> n'"
  3.1716 @@ -1656,27 +1643,26 @@
  3.1717    case True
  3.1718    then show ?thesis
  3.1719      by (induct n n' rule: less_Suc_induct) (auto intro: mono)
  3.1720 -qed (insert \<open>n \<le> n'\<close>, auto) \<comment> \<open>trivial for @{prop "n = n'"}\<close>
  3.1721 +next
  3.1722 +  case False
  3.1723 +  with \<open>n \<le> n'\<close> show ?thesis by auto
  3.1724 +qed
  3.1725  
  3.1726  lemma lift_Suc_mono_less:
  3.1727    assumes mono: "\<And>n. f n < f (Suc n)" and "n < n'"
  3.1728    shows "f n < f n'"
  3.1729 -using \<open>n < n'\<close>
  3.1730 -by (induct n n' rule: less_Suc_induct) (auto intro: mono)
  3.1731 -
  3.1732 -lemma lift_Suc_mono_less_iff:
  3.1733 -  "(\<And>n. f n < f (Suc n)) \<Longrightarrow> f n < f m \<longleftrightarrow> n < m"
  3.1734 +  using \<open>n < n'\<close> by (induct n n' rule: less_Suc_induct) (auto intro: mono)
  3.1735 +
  3.1736 +lemma lift_Suc_mono_less_iff: "(\<And>n. f n < f (Suc n)) \<Longrightarrow> f n < f m \<longleftrightarrow> n < m"
  3.1737    by (blast intro: less_asym' lift_Suc_mono_less [of f]
  3.1738      dest: linorder_not_less[THEN iffD1] le_eq_less_or_eq [THEN iffD1])
  3.1739  
  3.1740  end
  3.1741  
  3.1742 -lemma mono_iff_le_Suc:
  3.1743 -  "mono f \<longleftrightarrow> (\<forall>n. f n \<le> f (Suc n))"
  3.1744 +lemma mono_iff_le_Suc: "mono f \<longleftrightarrow> (\<forall>n. f n \<le> f (Suc n))"
  3.1745    unfolding mono_def by (auto intro: lift_Suc_mono_le [of f])
  3.1746  
  3.1747 -lemma antimono_iff_le_Suc:
  3.1748 -  "antimono f \<longleftrightarrow> (\<forall>n. f (Suc n) \<le> f n)"
  3.1749 +lemma antimono_iff_le_Suc: "antimono f \<longleftrightarrow> (\<forall>n. f (Suc n) \<le> f n)"
  3.1750    unfolding antimono_def by (auto intro: lift_Suc_antimono_le [of f])
  3.1751  
  3.1752  lemma mono_nat_linear_lb:
  3.1753 @@ -1684,7 +1670,8 @@
  3.1754    assumes "\<And>m n. m < n \<Longrightarrow> f m < f n"
  3.1755    shows "f m + k \<le> f (m + k)"
  3.1756  proof (induct k)
  3.1757 -  case 0 then show ?case by simp
  3.1758 +  case 0
  3.1759 +  then show ?case by simp
  3.1760  next
  3.1761    case (Suc k)
  3.1762    then have "Suc (f m + k) \<le> Suc (f (m + k))" by simp
  3.1763 @@ -1694,7 +1681,7 @@
  3.1764  qed
  3.1765  
  3.1766  
  3.1767 -text\<open>Subtraction laws, mostly by Clemens Ballarin\<close>
  3.1768 +text \<open>Subtraction laws, mostly by Clemens Ballarin\<close>
  3.1769  
  3.1770  lemma diff_less_mono:
  3.1771    fixes a b c :: nat
  3.1772 @@ -1706,105 +1693,73 @@
  3.1773    then show ?thesis by simp
  3.1774  qed
  3.1775  
  3.1776 -lemma less_diff_conv:
  3.1777 -  fixes i j k :: nat
  3.1778 -  shows "i < j - k \<longleftrightarrow> i + k < j" (is "?P \<longleftrightarrow> ?Q")
  3.1779 -  by (cases "k \<le> j")
  3.1780 -    (auto simp add: not_le dest: less_imp_Suc_add le_Suc_ex)
  3.1781 -
  3.1782 -lemma less_diff_conv2:
  3.1783 -  fixes j k i :: nat
  3.1784 -  assumes "k \<le> j"
  3.1785 -  shows "j - k < i \<longleftrightarrow> j < i + k" (is "?P \<longleftrightarrow> ?Q")
  3.1786 -  using assms by (auto dest: le_Suc_ex)
  3.1787 -
  3.1788 -lemma le_diff_conv:
  3.1789 -  fixes j k i :: nat
  3.1790 -  shows "j - k \<le> i \<longleftrightarrow> j \<le> i + k"
  3.1791 -  by (cases "k \<le> j")
  3.1792 -    (auto simp add: not_le dest!: less_imp_Suc_add le_Suc_ex)
  3.1793 -
  3.1794 -lemma diff_diff_cancel [simp]:
  3.1795 -  fixes i n :: nat
  3.1796 -  shows "i \<le> n \<Longrightarrow> n - (n - i) = i"
  3.1797 +lemma less_diff_conv: "i < j - k \<longleftrightarrow> i + k < j" for i j k :: nat
  3.1798 +  by (cases "k \<le> j") (auto simp add: not_le dest: less_imp_Suc_add le_Suc_ex)
  3.1799 +
  3.1800 +lemma less_diff_conv2: "k \<le> j \<Longrightarrow> j - k < i \<longleftrightarrow> j < i + k" for j k i :: nat
  3.1801    by (auto dest: le_Suc_ex)
  3.1802  
  3.1803 -lemma diff_less [simp]:
  3.1804 -  fixes i n :: nat
  3.1805 -  shows "0 < n \<Longrightarrow> 0 < m \<Longrightarrow> m - n < m"
  3.1806 +lemma le_diff_conv: "j - k \<le> i \<longleftrightarrow> j \<le> i + k" for j k i :: nat
  3.1807 +  by (cases "k \<le> j") (auto simp add: not_le dest!: less_imp_Suc_add le_Suc_ex)
  3.1808 +
  3.1809 +lemma diff_diff_cancel [simp]: "i \<le> n \<Longrightarrow> n - (n - i) = i" for i n :: nat
  3.1810 +  by (auto dest: le_Suc_ex)
  3.1811 +
  3.1812 +lemma diff_less [simp]: "0 < n \<Longrightarrow> 0 < m \<Longrightarrow> m - n < m" for i n :: nat
  3.1813    by (auto dest: less_imp_Suc_add)
  3.1814  
  3.1815  text \<open>Simplification of relational expressions involving subtraction\<close>
  3.1816  
  3.1817 -lemma diff_diff_eq:
  3.1818 -  fixes m n k :: nat
  3.1819 -  shows "k \<le> m \<Longrightarrow> k \<le> n \<Longrightarrow> m - k - (n - k) = m - n"
  3.1820 +lemma diff_diff_eq: "k \<le> m \<Longrightarrow> k \<le> n \<Longrightarrow> m - k - (n - k) = m - n" for m n k :: nat
  3.1821    by (auto dest!: le_Suc_ex)
  3.1822  
  3.1823  hide_fact (open) diff_diff_eq
  3.1824  
  3.1825 -lemma eq_diff_iff:
  3.1826 -  fixes m n k :: nat
  3.1827 -  shows "k \<le> m \<Longrightarrow> k \<le> n \<Longrightarrow> m - k = n - k \<longleftrightarrow> m = n"
  3.1828 +lemma eq_diff_iff: "k \<le> m \<Longrightarrow> k \<le> n \<Longrightarrow> m - k = n - k \<longleftrightarrow> m = n" for m n k :: nat
  3.1829    by (auto dest: le_Suc_ex)
  3.1830  
  3.1831 -lemma less_diff_iff:
  3.1832 -  fixes m n k :: nat
  3.1833 -  shows "k \<le> m \<Longrightarrow> k \<le> n \<Longrightarrow> m - k < n - k \<longleftrightarrow> m < n"
  3.1834 +lemma less_diff_iff: "k \<le> m \<Longrightarrow> k \<le> n \<Longrightarrow> m - k < n - k \<longleftrightarrow> m < n" for m n k :: nat
  3.1835    by (auto dest!: le_Suc_ex)
  3.1836  
  3.1837 -lemma le_diff_iff:
  3.1838 -  fixes m n k :: nat
  3.1839 -  shows "k \<le> m \<Longrightarrow> k \<le> n \<Longrightarrow> m - k \<le> n - k \<longleftrightarrow> m \<le> n"
  3.1840 +lemma le_diff_iff: "k \<le> m \<Longrightarrow> k \<le> n \<Longrightarrow> m - k \<le> n - k \<longleftrightarrow> m \<le> n" for m n k :: nat
  3.1841    by (auto dest!: le_Suc_ex)
  3.1842  
  3.1843 -lemma le_diff_iff': "a \<le> c \<Longrightarrow> b \<le> c \<Longrightarrow> c - a \<le> c - b \<longleftrightarrow> b \<le> (a::nat)"
  3.1844 +lemma le_diff_iff': "a \<le> c \<Longrightarrow> b \<le> c \<Longrightarrow> c - a \<le> c - b \<longleftrightarrow> b \<le> a" for a b c :: nat
  3.1845    by (force dest: le_Suc_ex)
  3.1846 -  
  3.1847 -
  3.1848 -text\<open>(Anti)Monotonicity of subtraction -- by Stephan Merz\<close>
  3.1849 -
  3.1850 -lemma diff_le_mono:
  3.1851 -  fixes m n l :: nat
  3.1852 -  shows "m \<le> n \<Longrightarrow> m - l \<le> n - l"
  3.1853 +
  3.1854 +
  3.1855 +text \<open>(Anti)Monotonicity of subtraction -- by Stephan Merz\<close>
  3.1856 +
  3.1857 +lemma diff_le_mono: "m \<le> n \<Longrightarrow> m - l \<le> n - l" for m n l :: nat
  3.1858    by (auto dest: less_imp_le less_imp_Suc_add split add: nat_diff_split)
  3.1859  
  3.1860 -lemma diff_le_mono2:
  3.1861 -  fixes m n l :: nat
  3.1862 -  shows "m \<le> n \<Longrightarrow> l - n \<le> l - m"
  3.1863 +lemma diff_le_mono2: "m \<le> n \<Longrightarrow> l - n \<le> l - m" for m n l :: nat
  3.1864    by (auto dest: less_imp_le le_Suc_ex less_imp_Suc_add less_le_trans split add: nat_diff_split)
  3.1865  
  3.1866 -lemma diff_less_mono2:
  3.1867 -  fixes m n l :: nat
  3.1868 -  shows "m < n \<Longrightarrow> m < l \<Longrightarrow> l - n < l - m"
  3.1869 +lemma diff_less_mono2: "m < n \<Longrightarrow> m < l \<Longrightarrow> l - n < l - m" for m n l :: nat
  3.1870    by (auto dest: less_imp_Suc_add split add: nat_diff_split)
  3.1871  
  3.1872 -lemma diffs0_imp_equal:
  3.1873 -  fixes m n :: nat
  3.1874 -  shows "m - n = 0 \<Longrightarrow> n - m = 0 \<Longrightarrow> m = n"
  3.1875 +lemma diffs0_imp_equal: "m - n = 0 \<Longrightarrow> n - m = 0 \<Longrightarrow> m = n" for m n :: nat
  3.1876    by (simp split add: nat_diff_split)
  3.1877  
  3.1878 -lemma min_diff:
  3.1879 -  fixes m n i :: nat
  3.1880 -  shows "min (m - i) (n - i) = min m n - i" (is "?lhs = ?rhs")
  3.1881 +lemma min_diff: "min (m - i) (n - i) = min m n - i" for m n i :: nat
  3.1882    by (cases m n rule: le_cases)
  3.1883      (auto simp add: not_le min.absorb1 min.absorb2 min.absorb_iff1 [symmetric] diff_le_mono)
  3.1884  
  3.1885  lemma inj_on_diff_nat:
  3.1886 -  assumes k_le_n: "\<forall>n \<in> N. k \<le> (n::nat)"
  3.1887 +  fixes k :: nat
  3.1888 +  assumes "\<forall>n \<in> N. k \<le> n"
  3.1889    shows "inj_on (\<lambda>n. n - k) N"
  3.1890  proof (rule inj_onI)
  3.1891    fix x y
  3.1892    assume a: "x \<in> N" "y \<in> N" "x - k = y - k"
  3.1893 -  with k_le_n have "x - k + k = y - k + k" by auto
  3.1894 -  with a k_le_n show "x = y" by (auto simp add: eq_diff_iff)
  3.1895 +  with assms have "x - k + k = y - k + k" by auto
  3.1896 +  with a assms show "x = y" by (auto simp add: eq_diff_iff)
  3.1897  qed
  3.1898  
  3.1899 -text\<open>Rewriting to pull differences out\<close>
  3.1900 -
  3.1901 -lemma diff_diff_right [simp]:
  3.1902 -  fixes i j k :: nat
  3.1903 -  shows "k \<le> j \<Longrightarrow> i - (j - k) = i + k - j"
  3.1904 +text \<open>Rewriting to pull differences out\<close>
  3.1905 +
  3.1906 +lemma diff_diff_right [simp]: "k \<le> j \<Longrightarrow> i - (j - k) = i + k - j" for i j k :: nat
  3.1907    by (fact diff_diff_right)
  3.1908  
  3.1909  lemma diff_Suc_diff_eq1 [simp]:
  3.1910 @@ -1842,24 +1797,22 @@
  3.1911    then show ?thesis by simp
  3.1912  qed
  3.1913  
  3.1914 -lemma one_less_mult:
  3.1915 -  "Suc 0 < n \<Longrightarrow> Suc 0 < m \<Longrightarrow> Suc 0 < m * n"
  3.1916 +lemma one_less_mult: "Suc 0 < n \<Longrightarrow> Suc 0 < m \<Longrightarrow> Suc 0 < m * n"
  3.1917    using less_1_mult [of n m] by (simp add: ac_simps)
  3.1918  
  3.1919 -lemma n_less_m_mult_n:
  3.1920 -  "0 < n \<Longrightarrow> Suc 0 < m \<Longrightarrow> n < m * n"
  3.1921 +lemma n_less_m_mult_n: "0 < n \<Longrightarrow> Suc 0 < m \<Longrightarrow> n < m * n"
  3.1922    using mult_strict_right_mono [of 1 m n] by simp
  3.1923  
  3.1924 -lemma n_less_n_mult_m:
  3.1925 -  "0 < n \<Longrightarrow> Suc 0 < m \<Longrightarrow> n < n * m"
  3.1926 +lemma n_less_n_mult_m: "0 < n \<Longrightarrow> Suc 0 < m \<Longrightarrow> n < n * m"
  3.1927    using mult_strict_left_mono [of 1 m n] by simp
  3.1928  
  3.1929 +
  3.1930  text \<open>Specialized induction principles that work "backwards":\<close>
  3.1931  
  3.1932  lemma inc_induct [consumes 1, case_names base step]:
  3.1933    assumes less: "i \<le> j"
  3.1934 -  assumes base: "P j"
  3.1935 -  assumes step: "\<And>n. i \<le> n \<Longrightarrow> n < j \<Longrightarrow> P (Suc n) \<Longrightarrow> P n"
  3.1936 +    and base: "P j"
  3.1937 +    and step: "\<And>n. i \<le> n \<Longrightarrow> n < j \<Longrightarrow> P (Suc n) \<Longrightarrow> P n"
  3.1938    shows "P i"
  3.1939    using less step
  3.1940  proof (induct "j - i" arbitrary: i)
  3.1941 @@ -1873,7 +1826,7 @@
  3.1942    from \<open>Suc d = j - n\<close> have "d + 1 = j - n" by simp
  3.1943    then have "d + 1 - 1 = j - n - 1" by simp
  3.1944    then have "d = j - n - 1" by simp
  3.1945 -  then have "d = j - (n + 1)" 
  3.1946 +  then have "d = j - (n + 1)"
  3.1947      by (simp add: diff_diff_eq)
  3.1948    then have "d = j - Suc n"
  3.1949      by simp
  3.1950 @@ -1892,11 +1845,11 @@
  3.1951    with order_refl \<open>n < j\<close> show "P n"
  3.1952      by (rule Suc.prems)
  3.1953  qed
  3.1954 -    
  3.1955 +
  3.1956  lemma strict_inc_induct [consumes 1, case_names base step]:
  3.1957    assumes less: "i < j"
  3.1958 -  assumes base: "\<And>i. j = Suc i \<Longrightarrow> P i"
  3.1959 -  assumes step: "\<And>i. i < j \<Longrightarrow> P (Suc i) \<Longrightarrow> P i"
  3.1960 +    and base: "\<And>i. j = Suc i \<Longrightarrow> P i"
  3.1961 +    and step: "\<And>i. i < j \<Longrightarrow> P (Suc i) \<Longrightarrow> P i"
  3.1962    shows "P i"
  3.1963  using less proof (induct "j - i - 1" arbitrary: i)
  3.1964    case (0 i)
  3.1965 @@ -1922,10 +1875,10 @@
  3.1966    with \<open>i < j\<close> show "P i" by (rule step)
  3.1967  qed
  3.1968  
  3.1969 -lemma zero_induct_lemma: "P k ==> (!!n. P (Suc n) ==> P n) ==> P (k - i)"
  3.1970 +lemma zero_induct_lemma: "P k \<Longrightarrow> (\<And>n. P (Suc n) \<Longrightarrow> P n) \<Longrightarrow> P (k - i)"
  3.1971    using inc_induct[of "k - i" k P, simplified] by blast
  3.1972  
  3.1973 -lemma zero_induct: "P k ==> (!!n. P (Suc n) ==> P n) ==> P 0"
  3.1974 +lemma zero_induct: "P k \<Longrightarrow> (\<And>n. P (Suc n) \<Longrightarrow> P n) \<Longrightarrow> P 0"
  3.1975    using inc_induct[of 0 k P] by blast
  3.1976  
  3.1977  text \<open>Further induction rule similar to @{thm inc_induct}\<close>
  3.1978 @@ -1933,13 +1886,15 @@
  3.1979  lemma dec_induct [consumes 1, case_names base step]:
  3.1980    "i \<le> j \<Longrightarrow> P i \<Longrightarrow> (\<And>n. i \<le> n \<Longrightarrow> n < j \<Longrightarrow> P n \<Longrightarrow> P (Suc n)) \<Longrightarrow> P j"
  3.1981  proof (induct j arbitrary: i)
  3.1982 -  case 0 then show ?case by simp
  3.1983 +  case 0
  3.1984 +  then show ?case by simp
  3.1985  next
  3.1986    case (Suc j)
  3.1987 -  from Suc.prems have "i \<le> j \<or> i = Suc j"
  3.1988 -    by (simp add: le_Suc_eq)
  3.1989 -  then show ?case proof
  3.1990 -    assume "i \<le> j"
  3.1991 +  from Suc.prems consider "i \<le> j" | "i = Suc j"
  3.1992 +    by (auto simp add: le_Suc_eq)
  3.1993 +  then show ?case
  3.1994 +  proof cases
  3.1995 +    case 1
  3.1996      moreover have "j < Suc j" by simp
  3.1997      moreover have "P j" using \<open>i \<le> j\<close> \<open>P i\<close>
  3.1998      proof (rule Suc.hyps)
  3.1999 @@ -1954,70 +1909,62 @@
  3.2000      ultimately show "P (Suc j)"
  3.2001        by (rule Suc.prems)
  3.2002    next
  3.2003 -    assume "i = Suc j"
  3.2004 +    case 2
  3.2005      with \<open>P i\<close> show "P (Suc j)" by simp
  3.2006    qed
  3.2007  qed
  3.2008  
  3.2009  
  3.2010 -subsection \<open> Monotonicity of funpow \<close>
  3.2011 +subsection \<open>Monotonicity of \<open>funpow\<close>\<close>
  3.2012  
  3.2013  lemma funpow_increasing:
  3.2014 -  fixes f :: "'a \<Rightarrow> ('a::{lattice, order_top})"
  3.2015 +  fixes f :: "'a \<Rightarrow> 'a::{lattice,order_top}"
  3.2016    shows "m \<le> n \<Longrightarrow> mono f \<Longrightarrow> (f ^^ n) \<top> \<le> (f ^^ m) \<top>"
  3.2017    by (induct rule: inc_induct)
  3.2018       (auto simp del: funpow.simps(2) simp add: funpow_Suc_right
  3.2019             intro: order_trans[OF _ funpow_mono])
  3.2020  
  3.2021  lemma funpow_decreasing:
  3.2022 -  fixes f :: "'a \<Rightarrow> ('a::{lattice, order_bot})"
  3.2023 +  fixes f :: "'a \<Rightarrow> 'a::{lattice,order_bot}"
  3.2024    shows "m \<le> n \<Longrightarrow> mono f \<Longrightarrow> (f ^^ m) \<bottom> \<le> (f ^^ n) \<bottom>"
  3.2025    by (induct rule: dec_induct)
  3.2026       (auto simp del: funpow.simps(2) simp add: funpow_Suc_right
  3.2027             intro: order_trans[OF _ funpow_mono])
  3.2028  
  3.2029  lemma mono_funpow:
  3.2030 -  fixes Q :: "'a::{lattice, order_bot} \<Rightarrow> 'a"
  3.2031 +  fixes Q :: "'a::{lattice,order_bot} \<Rightarrow> 'a"
  3.2032    shows "mono Q \<Longrightarrow> mono (\<lambda>i. (Q ^^ i) \<bottom>)"
  3.2033    by (auto intro!: funpow_decreasing simp: mono_def)
  3.2034  
  3.2035  lemma antimono_funpow:
  3.2036 -  fixes Q :: "'a::{lattice, order_top} \<Rightarrow> 'a"
  3.2037 +  fixes Q :: "'a::{lattice,order_top} \<Rightarrow> 'a"
  3.2038    shows "mono Q \<Longrightarrow> antimono (\<lambda>i. (Q ^^ i) \<top>)"
  3.2039    by (auto intro!: funpow_increasing simp: antimono_def)
  3.2040  
  3.2041 +
  3.2042  subsection \<open>The divides relation on @{typ nat}\<close>
  3.2043  
  3.2044 -lemma dvd_1_left [iff]:
  3.2045 -  "Suc 0 dvd k"
  3.2046 +lemma dvd_1_left [iff]: "Suc 0 dvd k"
  3.2047    by (simp add: dvd_def)
  3.2048  
  3.2049 -lemma dvd_1_iff_1 [simp]:
  3.2050 -  "m dvd Suc 0 \<longleftrightarrow> m = Suc 0"
  3.2051 +lemma dvd_1_iff_1 [simp]: "m dvd Suc 0 \<longleftrightarrow> m = Suc 0"
  3.2052    by (simp add: dvd_def)
  3.2053  
  3.2054 -lemma nat_dvd_1_iff_1 [simp]:
  3.2055 -  "m dvd (1::nat) \<longleftrightarrow> m = 1"
  3.2056 +lemma nat_dvd_1_iff_1 [simp]: "m dvd 1 \<longleftrightarrow> m = 1" for m :: nat
  3.2057    by (simp add: dvd_def)
  3.2058  
  3.2059 -lemma dvd_antisym:
  3.2060 -  "m dvd n \<Longrightarrow> n dvd m \<Longrightarrow> m = (n::nat)"
  3.2061 -  unfolding dvd_def
  3.2062 -  by (force dest: mult_eq_self_implies_10 simp add: mult.assoc)
  3.2063 -
  3.2064 -lemma dvd_diff_nat [simp]:
  3.2065 -  "k dvd m \<Longrightarrow> k dvd n \<Longrightarrow> k dvd (m - n :: nat)"
  3.2066 -  unfolding dvd_def
  3.2067 -  by (blast intro: right_diff_distrib' [symmetric])
  3.2068 -
  3.2069 -lemma dvd_diffD:
  3.2070 -  "k dvd m - n \<Longrightarrow> k dvd n \<Longrightarrow> n \<le> m \<Longrightarrow> k dvd (m::nat)"
  3.2071 +lemma dvd_antisym: "m dvd n \<Longrightarrow> n dvd m \<Longrightarrow> m = n" for m n :: nat
  3.2072 +  unfolding dvd_def by (force dest: mult_eq_self_implies_10 simp add: mult.assoc)
  3.2073 +
  3.2074 +lemma dvd_diff_nat [simp]: "k dvd m \<Longrightarrow> k dvd n \<Longrightarrow> k dvd (m - n)" for k m n :: nat
  3.2075 +  unfolding dvd_def by (blast intro: right_diff_distrib' [symmetric])
  3.2076 +
  3.2077 +lemma dvd_diffD: "k dvd m - n \<Longrightarrow> k dvd n \<Longrightarrow> n \<le> m \<Longrightarrow> k dvd m" for k m n :: nat
  3.2078    apply (erule linorder_not_less [THEN iffD2, THEN add_diff_inverse, THEN subst])
  3.2079    apply (blast intro: dvd_add)
  3.2080    done
  3.2081  
  3.2082 -lemma dvd_diffD1:
  3.2083 -  "k dvd m - n \<Longrightarrow> k dvd m \<Longrightarrow> n \<le> m \<Longrightarrow> k dvd (n::nat)"
  3.2084 +lemma dvd_diffD1: "k dvd m - n \<Longrightarrow> k dvd m \<Longrightarrow> n \<le> m \<Longrightarrow> k dvd n" for k m n :: nat
  3.2085    by (drule_tac m = m in dvd_diff_nat) auto
  3.2086  
  3.2087  lemma dvd_mult_cancel:
  3.2088 @@ -2030,25 +1977,20 @@
  3.2089    with \<open>0 < k\<close> have "n = m * q" by (auto simp add: mult_left_cancel)
  3.2090    then show ?thesis ..
  3.2091  qed
  3.2092 -  
  3.2093 -lemma dvd_mult_cancel1:
  3.2094 -  "0 < m \<Longrightarrow> m * n dvd m \<longleftrightarrow> n = (1::nat)"
  3.2095 +
  3.2096 +lemma dvd_mult_cancel1: "0 < m \<Longrightarrow> m * n dvd m \<longleftrightarrow> n = 1" for m n :: nat
  3.2097    apply auto
  3.2098 -   apply (subgoal_tac "m*n dvd m*1")
  3.2099 +   apply (subgoal_tac "m * n dvd m * 1")
  3.2100     apply (drule dvd_mult_cancel, auto)
  3.2101    done
  3.2102  
  3.2103 -lemma dvd_mult_cancel2:
  3.2104 -  "0 < m \<Longrightarrow> n * m dvd m \<longleftrightarrow> n = (1::nat)"
  3.2105 +lemma dvd_mult_cancel2: "0 < m \<Longrightarrow> n * m dvd m \<longleftrightarrow> n = 1" for m n :: nat
  3.2106    using dvd_mult_cancel1 [of m n] by (simp add: ac_simps)
  3.2107  
  3.2108 -lemma dvd_imp_le:
  3.2109 -  "k dvd n \<Longrightarrow> 0 < n \<Longrightarrow> k \<le> (n::nat)"
  3.2110 +lemma dvd_imp_le: "k dvd n \<Longrightarrow> 0 < n \<Longrightarrow> k \<le> n" for k n :: nat
  3.2111    by (auto elim!: dvdE) (auto simp add: gr0_conv_Suc)
  3.2112  
  3.2113 -lemma nat_dvd_not_less:
  3.2114 -  fixes m n :: nat
  3.2115 -  shows "0 < m \<Longrightarrow> m < n \<Longrightarrow> \<not> n dvd m"
  3.2116 +lemma nat_dvd_not_less: "0 < m \<Longrightarrow> m < n \<Longrightarrow> \<not> n dvd m" for m n :: nat
  3.2117    by (auto elim!: dvdE) (auto simp add: gr0_conv_Suc)
  3.2118  
  3.2119  lemma less_eq_dvd_minus:
  3.2120 @@ -2061,9 +2003,7 @@
  3.2121    then show ?thesis by (simp add: add.commute [of m])
  3.2122  qed
  3.2123  
  3.2124 -lemma dvd_minus_self:
  3.2125 -  fixes m n :: nat
  3.2126 -  shows "m dvd n - m \<longleftrightarrow> n < m \<or> m dvd n"
  3.2127 +lemma dvd_minus_self: "m dvd n - m \<longleftrightarrow> n < m \<or> m dvd n" for m n :: nat
  3.2128    by (cases "n < m") (auto elim!: dvdE simp add: not_less le_imp_diff_is_add dest: less_imp_le)
  3.2129  
  3.2130  lemma dvd_minus_add:
  3.2131 @@ -2082,61 +2022,55 @@
  3.2132  
  3.2133  subsection \<open>Aliasses\<close>
  3.2134  
  3.2135 -lemma nat_mult_1: "(1::nat) * n = n"
  3.2136 +lemma nat_mult_1: "1 * n = n" for n :: nat
  3.2137    by (fact mult_1_left)
  3.2138  
  3.2139 -lemma nat_mult_1_right: "n * (1::nat) = n"
  3.2140 +lemma nat_mult_1_right: "n * 1 = n" for n :: nat
  3.2141    by (fact mult_1_right)
  3.2142  
  3.2143 -lemma nat_add_left_cancel:
  3.2144 -  fixes k m n :: nat
  3.2145 -  shows "k + m = k + n \<longleftrightarrow> m = n"
  3.2146 +lemma nat_add_left_cancel: "k + m = k + n \<longleftrightarrow> m = n" for k m n :: nat
  3.2147    by (fact add_left_cancel)
  3.2148  
  3.2149 -lemma nat_add_right_cancel:
  3.2150 -  fixes k m n :: nat
  3.2151 -  shows "m + k = n + k \<longleftrightarrow> m = n"
  3.2152 +lemma nat_add_right_cancel: "m + k = n + k \<longleftrightarrow> m = n" for k m n :: nat
  3.2153    by (fact add_right_cancel)
  3.2154  
  3.2155 -lemma diff_mult_distrib:
  3.2156 -  "((m::nat) - n) * k = (m * k) - (n * k)"
  3.2157 +lemma diff_mult_distrib: "(m - n) * k = (m * k) - (n * k)" for k m n :: nat
  3.2158    by (fact left_diff_distrib')
  3.2159  
  3.2160 -lemma diff_mult_distrib2:
  3.2161 -  "k * ((m::nat) - n) = (k * m) - (k * n)"
  3.2162 +lemma diff_mult_distrib2: "k * (m - n) = (k * m) - (k * n)" for k m n :: nat
  3.2163    by (fact right_diff_distrib')
  3.2164  
  3.2165 -lemma le_add_diff: "k \<le> (n::nat) ==> m \<le> n + m - k"
  3.2166 -  by (fact le_add_diff) \<comment> \<open>FIXME delete\<close>
  3.2167 -
  3.2168 -lemma le_diff_conv2: "k \<le> j ==> (i \<le> j-k) = (i+k \<le> (j::nat))"
  3.2169 -  by (fact le_diff_conv2) \<comment> \<open>FIXME delete\<close>
  3.2170 -
  3.2171 -lemma diff_self_eq_0 [simp]: "(m::nat) - m = 0"
  3.2172 +lemma le_add_diff: "k \<le> n \<Longrightarrow> m \<le> n + m - k" for k m n :: nat
  3.2173 +  by (fact le_add_diff)  (* FIXME delete *)
  3.2174 +
  3.2175 +lemma le_diff_conv2: "k \<le> j \<Longrightarrow> (i \<le> j - k) = (i + k \<le> j)" for i j k :: nat
  3.2176 +  by (fact le_diff_conv2) (* FIXME delete *)
  3.2177 +
  3.2178 +lemma diff_self_eq_0 [simp]: "m - m = 0" for m :: nat
  3.2179    by (fact diff_cancel)
  3.2180  
  3.2181 -lemma diff_diff_left [simp]: "(i::nat) - j - k = i - (j + k)"
  3.2182 +lemma diff_diff_left [simp]: "i - j - k = i - (j + k)" for i j k :: nat
  3.2183    by (fact diff_diff_add)
  3.2184  
  3.2185 -lemma diff_commute: "(i::nat) - j - k = i - k - j"
  3.2186 +lemma diff_commute: "i - j - k = i - k - j" for i j k :: nat
  3.2187    by (fact diff_right_commute)
  3.2188  
  3.2189 -lemma diff_add_inverse: "(n + m) - n = (m::nat)"
  3.2190 +lemma diff_add_inverse: "(n + m) - n = m" for m n :: nat
  3.2191    by (fact add_diff_cancel_left')
  3.2192  
  3.2193 -lemma diff_add_inverse2: "(m + n) - n = (m::nat)"
  3.2194 +lemma diff_add_inverse2: "(m + n) - n = m" for m n :: nat
  3.2195    by (fact add_diff_cancel_right')
  3.2196  
  3.2197 -lemma diff_cancel: "(k + m) - (k + n) = m - (n::nat)"
  3.2198 +lemma diff_cancel: "(k + m) - (k + n) = m - n" for k m n :: nat
  3.2199    by (fact add_diff_cancel_left)
  3.2200  
  3.2201 -lemma diff_cancel2: "(m + k) - (n + k) = m - (n::nat)"
  3.2202 +lemma diff_cancel2: "(m + k) - (n + k) = m - n" for k m n :: nat
  3.2203    by (fact add_diff_cancel_right)
  3.2204  
  3.2205 -lemma diff_add_0: "n - (n + m) = (0::nat)"
  3.2206 +lemma diff_add_0: "n - (n + m) = 0" for m n :: nat
  3.2207    by (fact diff_add_zero)
  3.2208  
  3.2209 -lemma add_mult_distrib2: "k * (m + n) = (k * m) + ((k * n)::nat)"
  3.2210 +lemma add_mult_distrib2: "k * (m + n) = (k * m) + (k * n)" for k m n :: nat
  3.2211    by (fact distrib_left)
  3.2212  
  3.2213  lemmas nat_distrib =
  3.2214 @@ -2151,8 +2085,7 @@
  3.2215  instantiation nat :: size
  3.2216  begin
  3.2217  
  3.2218 -definition size_nat where
  3.2219 -  [simp, code]: "size (n::nat) = n"
  3.2220 +definition size_nat where [simp, code]: "size (n::nat) = n"
  3.2221  
  3.2222  instance ..
  3.2223  
     4.1 --- a/src/HOL/Wellfounded.thy	Mon May 23 15:33:24 2016 +0100
     4.2 +++ b/src/HOL/Wellfounded.thy	Mon May 23 15:46:30 2016 +0100
     4.3 @@ -14,34 +14,33 @@
     4.4  
     4.5  subsection \<open>Basic Definitions\<close>
     4.6  
     4.7 -definition wf :: "('a * 'a) set => bool" where
     4.8 -  "wf r \<longleftrightarrow> (!P. (!x. (!y. (y,x):r --> P(y)) --> P(x)) --> (!x. P(x)))"
     4.9 +definition wf :: "('a \<times> 'a) set \<Rightarrow> bool"
    4.10 +  where "wf r \<longleftrightarrow> (\<forall>P. (\<forall>x. (\<forall>y. (y, x) \<in> r \<longrightarrow> P y) \<longrightarrow> P x) \<longrightarrow> (\<forall>x. P x))"
    4.11  
    4.12 -definition wfP :: "('a => 'a => bool) => bool" where
    4.13 -  "wfP r \<longleftrightarrow> wf {(x, y). r x y}"
    4.14 +definition wfP :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool"
    4.15 +  where "wfP r \<longleftrightarrow> wf {(x, y). r x y}"
    4.16  
    4.17  lemma wfP_wf_eq [pred_set_conv]: "wfP (\<lambda>x y. (x, y) \<in> r) = wf r"
    4.18    by (simp add: wfP_def)
    4.19  
    4.20 -lemma wfUNIVI: 
    4.21 -   "(!!P x. (ALL x. (ALL y. (y,x) : r --> P(y)) --> P(x)) ==> P(x)) ==> wf(r)"
    4.22 +lemma wfUNIVI: "(\<And>P x. (\<forall>x. (\<forall>y. (y, x) \<in> r \<longrightarrow> P y) \<longrightarrow> P x) \<Longrightarrow> P x) \<Longrightarrow> wf r"
    4.23    unfolding wf_def by blast
    4.24  
    4.25  lemmas wfPUNIVI = wfUNIVI [to_pred]
    4.26  
    4.27 -text\<open>Restriction to domain @{term A} and range @{term B}.  If @{term r} is
    4.28 -    well-founded over their intersection, then @{term "wf r"}\<close>
    4.29 -lemma wfI: 
    4.30 - "[| r \<subseteq> A \<times> B; 
    4.31 -     !!x P. [|\<forall>x. (\<forall>y. (y,x) : r --> P y) --> P x;  x : A; x : B |] ==> P x |]
    4.32 -  ==>  wf r"
    4.33 -  unfolding wf_def by blast
    4.34 +text \<open>Restriction to domain \<open>A\<close> and range \<open>B\<close>.
    4.35 +  If \<open>r\<close> is well-founded over their intersection, then \<open>wf r\<close>.\<close>
    4.36 +lemma wfI:
    4.37 +  assumes "r \<subseteq> A \<times> B"
    4.38 +    and "\<And>x P. \<lbrakk>\<forall>x. (\<forall>y. (y, x) \<in> r \<longrightarrow> P y) \<longrightarrow> P x;  x \<in> A; x \<in> B\<rbrakk> \<Longrightarrow> P x"
    4.39 +  shows "wf r"
    4.40 +  using assms unfolding wf_def by blast
    4.41  
    4.42 -lemma wf_induct: 
    4.43 -    "[| wf(r);           
    4.44 -        !!x.[| ALL y. (y,x): r --> P(y) |] ==> P(x)  
    4.45 -     |]  ==>  P(a)"
    4.46 -  unfolding wf_def by blast
    4.47 +lemma wf_induct:
    4.48 +  assumes "wf r"
    4.49 +    and "\<And>x. \<forall>y. (y, x) \<in> r \<longrightarrow> P y \<Longrightarrow> P x"
    4.50 +  shows "P a"
    4.51 +  using assms unfolding wf_def by blast
    4.52  
    4.53  lemmas wfP_induct = wf_induct [to_pred]
    4.54  
    4.55 @@ -49,7 +48,7 @@
    4.56  
    4.57  lemmas wfP_induct_rule = wf_induct_rule [to_pred, induct set: wfP]
    4.58  
    4.59 -lemma wf_not_sym: "wf r ==> (a, x) : r ==> (x, a) ~: r"
    4.60 +lemma wf_not_sym: "wf r \<Longrightarrow> (a, x) \<in> r \<Longrightarrow> (x, a) \<notin> r"
    4.61    by (induct a arbitrary: x set: wf) blast
    4.62  
    4.63  lemma wf_asym:
    4.64 @@ -57,22 +56,25 @@
    4.65    obtains "(x, a) \<notin> r"
    4.66    by (drule wf_not_sym[OF assms])
    4.67  
    4.68 -lemma wf_not_refl [simp]: "wf r ==> (a, a) ~: r"
    4.69 +lemma wf_not_refl [simp]: "wf r \<Longrightarrow> (a, a) \<notin> r"
    4.70    by (blast elim: wf_asym)
    4.71  
    4.72  lemma wf_irrefl: assumes "wf r" obtains "(a, a) \<notin> r"
    4.73 -by (drule wf_not_refl[OF assms])
    4.74 +  by (drule wf_not_refl[OF assms])
    4.75  
    4.76  lemma wf_wellorderI:
    4.77    assumes wf: "wf {(x::'a::ord, y). x < y}"
    4.78    assumes lin: "OFCLASS('a::ord, linorder_class)"
    4.79    shows "OFCLASS('a::ord, wellorder_class)"
    4.80 -using lin by (rule wellorder_class.intro)
    4.81 -  (rule class.wellorder_axioms.intro, rule wf_induct_rule [OF wf], simp)
    4.82 +  using lin
    4.83 +  apply (rule wellorder_class.intro)
    4.84 +  apply (rule class.wellorder_axioms.intro)
    4.85 +  apply (rule wf_induct_rule [OF wf])
    4.86 +  apply simp
    4.87 +  done
    4.88  
    4.89 -lemma (in wellorder) wf:
    4.90 -  "wf {(x, y). x < y}"
    4.91 -unfolding wf_def by (blast intro: less_induct)
    4.92 +lemma (in wellorder) wf: "wf {(x, y). x < y}"
    4.93 +  unfolding wf_def by (blast intro: less_induct)
    4.94  
    4.95  
    4.96  subsection \<open>Basic Results\<close>
    4.97 @@ -84,14 +86,13 @@
    4.98    assumes a: "A \<subseteq> R `` A"
    4.99    shows "A = {}"
   4.100  proof -
   4.101 -  { fix x
   4.102 -    from wf have "x \<notin> A"
   4.103 -    proof induct
   4.104 -      fix x assume "\<And>y. (y, x) \<in> R \<Longrightarrow> y \<notin> A"
   4.105 -      then have "x \<notin> R `` A" by blast
   4.106 -      with a show "x \<notin> A" by blast
   4.107 -    qed
   4.108 -  } thus ?thesis by auto
   4.109 +  from wf have "x \<notin> A" for x
   4.110 +  proof induct
   4.111 +    fix x assume "\<And>y. (y, x) \<in> R \<Longrightarrow> y \<notin> A"
   4.112 +    then have "x \<notin> R `` A" by blast
   4.113 +    with a show "x \<notin> A" by blast
   4.114 +  qed
   4.115 +  then show ?thesis by auto
   4.116  qed
   4.117  
   4.118  lemma wfI_pf:
   4.119 @@ -105,7 +106,8 @@
   4.120    with a show "P x" by blast
   4.121  qed
   4.122  
   4.123 -text\<open>Minimal-element characterization of well-foundedness\<close>
   4.124 +
   4.125 +subsubsection \<open>Minimal-element characterization of well-foundedness\<close>
   4.126  
   4.127  lemma wfE_min:
   4.128    assumes wf: "wf R" and Q: "x \<in> Q"
   4.129 @@ -120,14 +122,14 @@
   4.130    assumes a: "\<And>x Q. x \<in> Q \<Longrightarrow> \<exists>z\<in>Q. \<forall>y. (y, z) \<in> R \<longrightarrow> y \<notin> Q"
   4.131    shows "wf R"
   4.132  proof (rule wfI_pf)
   4.133 -  fix A assume b: "A \<subseteq> R `` A"
   4.134 -  { fix x assume "x \<in> A"
   4.135 -    from a[OF this] b have "False" by blast
   4.136 -  }
   4.137 -  thus "A = {}" by blast
   4.138 +  fix A
   4.139 +  assume b: "A \<subseteq> R `` A"
   4.140 +  have False if "x \<in> A" for x
   4.141 +    using a[OF that] b by blast
   4.142 +  then show "A = {}" by blast
   4.143  qed
   4.144  
   4.145 -lemma wf_eq_minimal: "wf r = (\<forall>Q x. x\<in>Q --> (\<exists>z\<in>Q. \<forall>y. (y,z)\<in>r --> y\<notin>Q))"
   4.146 +lemma wf_eq_minimal: "wf r \<longleftrightarrow> (\<forall>Q x. x \<in> Q \<longrightarrow> (\<exists>z\<in>Q. \<forall>y. (y, z) \<in> r \<longrightarrow> y \<notin> Q))"
   4.147  apply auto
   4.148  apply (erule wfE_min, assumption, blast)
   4.149  apply (rule wfI_min, auto)
   4.150 @@ -135,51 +137,52 @@
   4.151  
   4.152  lemmas wfP_eq_minimal = wf_eq_minimal [to_pred]
   4.153  
   4.154 -text\<open>Well-foundedness of transitive closure\<close>
   4.155 +
   4.156 +subsubsection \<open>Well-foundedness of transitive closure\<close>
   4.157  
   4.158  lemma wf_trancl:
   4.159    assumes "wf r"
   4.160 -  shows "wf (r^+)"
   4.161 +  shows "wf (r\<^sup>+)"
   4.162  proof -
   4.163 -  {
   4.164 -    fix P and x
   4.165 -    assume induct_step: "!!x. (!!y. (y, x) : r^+ ==> P y) ==> P x"
   4.166 -    have "P x"
   4.167 -    proof (rule induct_step)
   4.168 -      fix y assume "(y, x) : r^+"
   4.169 -      with \<open>wf r\<close> show "P y"
   4.170 -      proof (induct x arbitrary: y)
   4.171 -        case (less x)
   4.172 -        note hyp = \<open>\<And>x' y'. (x', x) : r ==> (y', x') : r^+ ==> P y'\<close>
   4.173 -        from \<open>(y, x) : r^+\<close> show "P y"
   4.174 -        proof cases
   4.175 -          case base
   4.176 -          show "P y"
   4.177 -          proof (rule induct_step)
   4.178 -            fix y' assume "(y', y) : r^+"
   4.179 -            with \<open>(y, x) : r\<close> show "P y'" by (rule hyp [of y y'])
   4.180 -          qed
   4.181 -        next
   4.182 -          case step
   4.183 -          then obtain x' where "(x', x) : r" and "(y, x') : r^+" by simp
   4.184 -          then show "P y" by (rule hyp [of x' y])
   4.185 +  have "P x" if induct_step: "\<And>x. (\<And>y. (y, x) \<in> r\<^sup>+ \<Longrightarrow> P y) \<Longrightarrow> P x" for P x
   4.186 +  proof (rule induct_step)
   4.187 +    show "P y" if "(y, x) \<in> r\<^sup>+" for y
   4.188 +      using \<open>wf r\<close> and that
   4.189 +    proof (induct x arbitrary: y)
   4.190 +      case (less x)
   4.191 +      note hyp = \<open>\<And>x' y'. (x', x) \<in> r \<Longrightarrow> (y', x') \<in> r\<^sup>+ \<Longrightarrow> P y'\<close>
   4.192 +      from \<open>(y, x) \<in> r\<^sup>+\<close> show "P y"
   4.193 +      proof cases
   4.194 +        case base
   4.195 +        show "P y"
   4.196 +        proof (rule induct_step)
   4.197 +          fix y'
   4.198 +          assume "(y', y) \<in> r\<^sup>+"
   4.199 +          with \<open>(y, x) \<in> r\<close> show "P y'"
   4.200 +            by (rule hyp [of y y'])
   4.201          qed
   4.202 +      next
   4.203 +        case step
   4.204 +        then obtain x' where "(x', x) \<in> r" and "(y, x') \<in> r\<^sup>+"
   4.205 +          by simp
   4.206 +        then show "P y" by (rule hyp [of x' y])
   4.207        qed
   4.208      qed
   4.209 -  } then show ?thesis unfolding wf_def by blast
   4.210 +  qed
   4.211 +  then show ?thesis unfolding wf_def by blast
   4.212  qed
   4.213  
   4.214  lemmas wfP_trancl = wf_trancl [to_pred]
   4.215  
   4.216 -lemma wf_converse_trancl: "wf (r^-1) ==> wf ((r^+)^-1)"
   4.217 +lemma wf_converse_trancl: "wf (r\<inverse>) \<Longrightarrow> wf ((r\<^sup>+)\<inverse>)"
   4.218    apply (subst trancl_converse [symmetric])
   4.219    apply (erule wf_trancl)
   4.220    done
   4.221  
   4.222  text \<open>Well-foundedness of subsets\<close>
   4.223  
   4.224 -lemma wf_subset: "[| wf(r);  p<=r |] ==> wf(p)"
   4.225 -  apply (simp (no_asm_use) add: wf_eq_minimal)
   4.226 +lemma wf_subset: "wf r \<Longrightarrow> p \<subseteq> r \<Longrightarrow> wf p"
   4.227 +  apply (simp add: wf_eq_minimal)
   4.228    apply fast
   4.229    done
   4.230  
   4.231 @@ -197,15 +200,15 @@
   4.232    then show ?thesis by (simp add: bot_fun_def)
   4.233  qed
   4.234  
   4.235 -lemma wf_Int1: "wf r ==> wf (r Int r')"
   4.236 +lemma wf_Int1: "wf r \<Longrightarrow> wf (r Int r')"
   4.237    apply (erule wf_subset)
   4.238    apply (rule Int_lower1)
   4.239    done
   4.240  
   4.241 -lemma wf_Int2: "wf r ==> wf (r' Int r)"
   4.242 +lemma wf_Int2: "wf r \<Longrightarrow> wf (r' Int r)"
   4.243    apply (erule wf_subset)
   4.244    apply (rule Int_lower2)
   4.245 -  done  
   4.246 +  done
   4.247  
   4.248  text \<open>Exponentiation\<close>
   4.249  
   4.250 @@ -221,33 +224,34 @@
   4.251  
   4.252  text \<open>Well-foundedness of insert\<close>
   4.253  
   4.254 -lemma wf_insert [iff]: "wf(insert (y,x) r) = (wf(r) & (x,y) ~: r^*)"
   4.255 +lemma wf_insert [iff]: "wf (insert (y, x) r) \<longleftrightarrow> wf r \<and> (x, y) \<notin> r\<^sup>*"
   4.256  apply (rule iffI)
   4.257   apply (blast elim: wf_trancl [THEN wf_irrefl]
   4.258 -              intro: rtrancl_into_trancl1 wf_subset 
   4.259 +              intro: rtrancl_into_trancl1 wf_subset
   4.260                       rtrancl_mono [THEN [2] rev_subsetD])
   4.261  apply (simp add: wf_eq_minimal, safe)
   4.262 -apply (rule allE, assumption, erule impE, blast) 
   4.263 +apply (rule allE, assumption, erule impE, blast)
   4.264  apply (erule bexE)
   4.265  apply (rename_tac "a", case_tac "a = x")
   4.266   prefer 2
   4.267 -apply blast 
   4.268 -apply (case_tac "y:Q")
   4.269 +apply blast
   4.270 +apply (case_tac "y \<in> Q")
   4.271   prefer 2 apply blast
   4.272 -apply (rule_tac x = "{z. z:Q & (z,y) : r^*}" in allE)
   4.273 +apply (rule_tac x = "{z. z \<in> Q \<and> (z,y) \<in> r\<^sup>*}" in allE)
   4.274   apply assumption
   4.275 -apply (erule_tac V = "ALL Q. (EX x. x : Q) --> P Q" for P in thin_rl) 
   4.276 -  \<comment>\<open>essential for speed\<close>
   4.277 -txt\<open>Blast with new substOccur fails\<close>
   4.278 +apply (erule_tac V = "\<forall>Q. (\<exists>x. x \<in> Q) \<longrightarrow> P Q" for P in thin_rl)
   4.279 +  (*essential for speed*)
   4.280 +(*blast with new substOccur fails*)
   4.281  apply (fast intro: converse_rtrancl_into_rtrancl)
   4.282  done
   4.283  
   4.284 -text\<open>Well-foundedness of image\<close>
   4.285 +
   4.286 +subsubsection \<open>Well-foundedness of image\<close>
   4.287  
   4.288 -lemma wf_map_prod_image: "[| wf r; inj f |] ==> wf (map_prod f f ` r)"
   4.289 +lemma wf_map_prod_image: "wf r \<Longrightarrow> inj f \<Longrightarrow> wf (map_prod f f ` r)"
   4.290  apply (simp only: wf_eq_minimal, clarify)
   4.291 -apply (case_tac "EX p. f p : Q")
   4.292 -apply (erule_tac x = "{p. f p : Q}" in allE)
   4.293 +apply (case_tac "\<exists>p. f p \<in> Q")
   4.294 +apply (erule_tac x = "{p. f p \<in> Q}" in allE)
   4.295  apply (fast dest: inj_onD, blast)
   4.296  done
   4.297  
   4.298 @@ -259,25 +263,23 @@
   4.299    assumes "R O S \<subseteq> R"
   4.300    shows "wf (R \<union> S)"
   4.301  proof (rule wfI_min)
   4.302 -  fix x :: 'a and Q 
   4.303 +  fix x :: 'a and Q
   4.304    let ?Q' = "{x \<in> Q. \<forall>y. (y, x) \<in> R \<longrightarrow> y \<notin> Q}"
   4.305    assume "x \<in> Q"
   4.306    obtain a where "a \<in> ?Q'"
   4.307      by (rule wfE_min [OF \<open>wf R\<close> \<open>x \<in> Q\<close>]) blast
   4.308 -  with \<open>wf S\<close>
   4.309 -  obtain z where "z \<in> ?Q'" and zmin: "\<And>y. (y, z) \<in> S \<Longrightarrow> y \<notin> ?Q'" by (erule wfE_min)
   4.310 -  { 
   4.311 +  with \<open>wf S\<close> obtain z where "z \<in> ?Q'" and zmin: "\<And>y. (y, z) \<in> S \<Longrightarrow> y \<notin> ?Q'"
   4.312 +    by (erule wfE_min)
   4.313 +  {
   4.314      fix y assume "(y, z) \<in> S"
   4.315      then have "y \<notin> ?Q'" by (rule zmin)
   4.316 -
   4.317      have "y \<notin> Q"
   4.318 -    proof 
   4.319 +    proof
   4.320        assume "y \<in> Q"
   4.321 -      with \<open>y \<notin> ?Q'\<close> 
   4.322 -      obtain w where "(w, y) \<in> R" and "w \<in> Q" by auto
   4.323 +      with \<open>y \<notin> ?Q'\<close> obtain w where "(w, y) \<in> R" and "w \<in> Q" by auto
   4.324        from \<open>(w, y) \<in> R\<close> \<open>(y, z) \<in> S\<close> have "(w, z) \<in> R O S" by (rule relcompI)
   4.325        with \<open>R O S \<subseteq> R\<close> have "(w, z) \<in> R" ..
   4.326 -      with \<open>z \<in> ?Q'\<close> have "w \<notin> Q" by blast 
   4.327 +      with \<open>z \<in> ?Q'\<close> have "w \<notin> Q" by blast
   4.328        with \<open>w \<in> Q\<close> show False by contradiction
   4.329      qed
   4.330    }
   4.331 @@ -287,18 +289,21 @@
   4.332  
   4.333  text \<open>Well-foundedness of indexed union with disjoint domains and ranges\<close>
   4.334  
   4.335 -lemma wf_UN: "[| ALL i:I. wf(r i);  
   4.336 -         ALL i:I. ALL j:I. r i ~= r j --> Domain(r i) Int Range(r j) = {}  
   4.337 -      |] ==> wf(UN i:I. r i)"
   4.338 -apply (simp only: wf_eq_minimal, clarify)
   4.339 -apply (rename_tac A a, case_tac "EX i:I. EX a:A. EX b:A. (b,a) : r i")
   4.340 - prefer 2
   4.341 - apply force 
   4.342 -apply clarify
   4.343 -apply (drule bspec, assumption)  
   4.344 -apply (erule_tac x="{a. a:A & (EX b:A. (b,a) : r i) }" in allE)
   4.345 -apply (blast elim!: allE)  
   4.346 -done
   4.347 +lemma wf_UN:
   4.348 +  assumes "\<forall>i\<in>I. wf (r i)"
   4.349 +    and "\<forall>i\<in>I. \<forall>j\<in>I. r i \<noteq> r j \<longrightarrow> Domain (r i) \<inter> Range (r j) = {}"
   4.350 +  shows "wf (\<Union>i\<in>I. r i)"
   4.351 +  using assms
   4.352 +  apply (simp only: wf_eq_minimal)
   4.353 +  apply clarify
   4.354 +  apply (rename_tac A a, case_tac "\<exists>i\<in>I. \<exists>a\<in>A. \<exists>b\<in>A. (b, a) \<in> r i")
   4.355 +   prefer 2
   4.356 +   apply force
   4.357 +  apply clarify
   4.358 +  apply (drule bspec, assumption)
   4.359 +  apply (erule_tac x="{a. a \<in> A \<and> (\<exists>b\<in>A. (b, a) \<in> r i) }" in allE)
   4.360 +  apply (blast elim!: allE)
   4.361 +  done
   4.362  
   4.363  lemma wfP_SUP:
   4.364    "\<forall>i. wfP (r i) \<Longrightarrow> \<forall>i j. r i \<noteq> r j \<longrightarrow> inf (DomainP (r i)) (RangeP (r j)) = bot \<Longrightarrow> wfP (SUPREMUM UNIV r)"
   4.365 @@ -306,72 +311,66 @@
   4.366    apply simp_all
   4.367    done
   4.368  
   4.369 -lemma wf_Union: 
   4.370 - "[| ALL r:R. wf r;  
   4.371 -     ALL r:R. ALL s:R. r ~= s --> Domain r Int Range s = {}  
   4.372 -  |] ==> wf (\<Union> R)"
   4.373 -  using wf_UN[of R "\<lambda>i. i"] by simp
   4.374 +lemma wf_Union:
   4.375 +  assumes "\<forall>r\<in>R. wf r"
   4.376 +    and "\<forall>r\<in>R. \<forall>s\<in>R. r \<noteq> s \<longrightarrow> Domain r \<inter> Range s = {}"
   4.377 +  shows "wf (\<Union>R)"
   4.378 +  using assms wf_UN[of R "\<lambda>i. i"] by simp
   4.379  
   4.380 -(*Intuition: we find an (R u S)-min element of a nonempty subset A
   4.381 -             by case distinction.
   4.382 -  1. There is a step a -R-> b with a,b : A.
   4.383 -     Pick an R-min element z of the (nonempty) set {a:A | EX b:A. a -R-> b}.
   4.384 -     By definition, there is z':A s.t. z -R-> z'. Because z is R-min in the
   4.385 -     subset, z' must be R-min in A. Because z' has an R-predecessor, it cannot
   4.386 -     have an S-successor and is thus S-min in A as well.
   4.387 -  2. There is no such step.
   4.388 -     Pick an S-min element of A. In this case it must be an R-min
   4.389 -     element of A as well.
   4.390 -*)
   4.391 -lemma wf_Un:
   4.392 -     "[| wf r; wf s; Domain r Int Range s = {} |] ==> wf(r Un s)"
   4.393 -  using wf_union_compatible[of s r] 
   4.394 +text \<open>
   4.395 +  Intuition: We find an \<open>R \<union> S\<close>-min element of a nonempty subset \<open>A\<close> by case distinction.
   4.396 +  \<^enum> There is a step \<open>a \<midarrow>R\<rightarrow> b\<close> with \<open>a, b \<in> A\<close>.
   4.397 +    Pick an \<open>R\<close>-min element \<open>z\<close> of the (nonempty) set \<open>{a\<in>A | \<exists>b\<in>A. a \<midarrow>R\<rightarrow> b}\<close>.
   4.398 +    By definition, there is \<open>z' \<in> A\<close> s.t. \<open>z \<midarrow>R\<rightarrow> z'\<close>. Because \<open>z\<close> is \<open>R\<close>-min in the
   4.399 +    subset, \<open>z'\<close> must be \<open>R\<close>-min in \<open>A\<close>. Because \<open>z'\<close> has an \<open>R\<close>-predecessor, it cannot
   4.400 +    have an \<open>S\<close>-successor and is thus \<open>S\<close>-min in \<open>A\<close> as well.
   4.401 +  \<^enum> There is no such step.
   4.402 +    Pick an \<open>S\<close>-min element of \<open>A\<close>. In this case it must be an \<open>R\<close>-min
   4.403 +    element of \<open>A\<close> as well.
   4.404 +\<close>
   4.405 +lemma wf_Un: "wf r \<Longrightarrow> wf s \<Longrightarrow> Domain r \<inter> Range s = {} \<Longrightarrow> wf (r \<union> s)"
   4.406 +  using wf_union_compatible[of s r]
   4.407    by (auto simp: Un_ac)
   4.408  
   4.409 -lemma wf_union_merge: 
   4.410 -  "wf (R \<union> S) = wf (R O R \<union> S O R \<union> S)" (is "wf ?A = wf ?B")
   4.411 +lemma wf_union_merge: "wf (R \<union> S) = wf (R O R \<union> S O R \<union> S)"
   4.412 +  (is "wf ?A = wf ?B")
   4.413  proof
   4.414    assume "wf ?A"
   4.415 -  with wf_trancl have wfT: "wf (?A^+)" .
   4.416 -  moreover have "?B \<subseteq> ?A^+"
   4.417 +  with wf_trancl have wfT: "wf (?A\<^sup>+)" .
   4.418 +  moreover have "?B \<subseteq> ?A\<^sup>+"
   4.419      by (subst trancl_unfold, subst trancl_unfold) blast
   4.420    ultimately show "wf ?B" by (rule wf_subset)
   4.421  next
   4.422    assume "wf ?B"
   4.423 -
   4.424    show "wf ?A"
   4.425    proof (rule wfI_min)
   4.426 -    fix Q :: "'a set" and x 
   4.427 +    fix Q :: "'a set" and x
   4.428      assume "x \<in> Q"
   4.429 -
   4.430 -    with \<open>wf ?B\<close>
   4.431 -    obtain z where "z \<in> Q" and "\<And>y. (y, z) \<in> ?B \<Longrightarrow> y \<notin> Q" 
   4.432 +    with \<open>wf ?B\<close> obtain z where "z \<in> Q" and "\<And>y. (y, z) \<in> ?B \<Longrightarrow> y \<notin> Q"
   4.433        by (erule wfE_min)
   4.434 -    then have A1: "\<And>y. (y, z) \<in> R O R \<Longrightarrow> y \<notin> Q"
   4.435 -      and A2: "\<And>y. (y, z) \<in> S O R \<Longrightarrow> y \<notin> Q"
   4.436 -      and A3: "\<And>y. (y, z) \<in> S \<Longrightarrow> y \<notin> Q"
   4.437 +    then have 1: "\<And>y. (y, z) \<in> R O R \<Longrightarrow> y \<notin> Q"
   4.438 +      and 2: "\<And>y. (y, z) \<in> S O R \<Longrightarrow> y \<notin> Q"
   4.439 +      and 3: "\<And>y. (y, z) \<in> S \<Longrightarrow> y \<notin> Q"
   4.440        by auto
   4.441 -    
   4.442      show "\<exists>z\<in>Q. \<forall>y. (y, z) \<in> ?A \<longrightarrow> y \<notin> Q"
   4.443      proof (cases "\<forall>y. (y, z) \<in> R \<longrightarrow> y \<notin> Q")
   4.444        case True
   4.445 -      with \<open>z \<in> Q\<close> A3 show ?thesis by blast
   4.446 +      with \<open>z \<in> Q\<close> 3 show ?thesis by blast
   4.447      next
   4.448 -      case False 
   4.449 +      case False
   4.450        then obtain z' where "z'\<in>Q" "(z', z) \<in> R" by blast
   4.451 -
   4.452        have "\<forall>y. (y, z') \<in> ?A \<longrightarrow> y \<notin> Q"
   4.453        proof (intro allI impI)
   4.454          fix y assume "(y, z') \<in> ?A"
   4.455          then show "y \<notin> Q"
   4.456          proof
   4.457 -          assume "(y, z') \<in> R" 
   4.458 +          assume "(y, z') \<in> R"
   4.459            then have "(y, z) \<in> R O R" using \<open>(z', z) \<in> R\<close> ..
   4.460 -          with A1 show "y \<notin> Q" .
   4.461 +          with 1 show "y \<notin> Q" .
   4.462          next
   4.463 -          assume "(y, z') \<in> S" 
   4.464 +          assume "(y, z') \<in> S"
   4.465            then have "(y, z) \<in> S O R" using  \<open>(z', z) \<in> R\<close> ..
   4.466 -          with A2 show "y \<notin> Q" .
   4.467 +          with 2 show "y \<notin> Q" .
   4.468          qed
   4.469        qed
   4.470        with \<open>z' \<in> Q\<close> show ?thesis ..
   4.471 @@ -389,40 +388,55 @@
   4.472  
   4.473  lemma qc_wf_relto_iff:
   4.474    assumes "R O S \<subseteq> (R \<union> S)\<^sup>* O R" \<comment> \<open>R quasi-commutes over S\<close>
   4.475 -  shows "wf (S\<^sup>* O R O S\<^sup>*) \<longleftrightarrow> wf R" (is "wf ?S \<longleftrightarrow> _")
   4.476 +  shows "wf (S\<^sup>* O R O S\<^sup>*) \<longleftrightarrow> wf R"
   4.477 +  (is "wf ?S \<longleftrightarrow> _")
   4.478  proof
   4.479 -  assume "wf ?S"
   4.480 -  moreover have "R \<subseteq> ?S" by auto
   4.481 -  ultimately show "wf R" using wf_subset by auto
   4.482 +  show "wf R" if "wf ?S"
   4.483 +  proof -
   4.484 +    have "R \<subseteq> ?S" by auto
   4.485 +    with that show "wf R" using wf_subset by auto
   4.486 +  qed
   4.487  next
   4.488 -  assume "wf R"
   4.489 -  show "wf ?S"
   4.490 +  show "wf ?S" if "wf R"
   4.491    proof (rule wfI_pf)
   4.492 -    fix A assume A: "A \<subseteq> ?S `` A"
   4.493 +    fix A
   4.494 +    assume A: "A \<subseteq> ?S `` A"
   4.495      let ?X = "(R \<union> S)\<^sup>* `` A"
   4.496      have *: "R O (R \<union> S)\<^sup>* \<subseteq> (R \<union> S)\<^sup>* O R"
   4.497 -      proof -
   4.498 -        { fix x y z assume "(y, z) \<in> (R \<union> S)\<^sup>*" and "(x, y) \<in> R"
   4.499 -          then have "(x, z) \<in> (R \<union> S)\<^sup>* O R"
   4.500 -          proof (induct y z)
   4.501 -            case rtrancl_refl then show ?case by auto
   4.502 -          next
   4.503 -            case (rtrancl_into_rtrancl a b c)
   4.504 -            then have "(x, c) \<in> ((R \<union> S)\<^sup>* O (R \<union> S)\<^sup>*) O R" using assms by blast
   4.505 -            then show ?case by simp
   4.506 -          qed }
   4.507 -        then show ?thesis by auto
   4.508 +    proof -
   4.509 +      have "(x, z) \<in> (R \<union> S)\<^sup>* O R" if "(y, z) \<in> (R \<union> S)\<^sup>*" and "(x, y) \<in> R" for x y z
   4.510 +        using that
   4.511 +      proof (induct y z)
   4.512 +        case rtrancl_refl
   4.513 +        then show ?case by auto
   4.514 +      next
   4.515 +        case (rtrancl_into_rtrancl a b c)
   4.516 +        then have "(x, c) \<in> ((R \<union> S)\<^sup>* O (R \<union> S)\<^sup>*) O R"
   4.517 +          using assms by blast
   4.518 +        then show ?case by simp
   4.519        qed
   4.520 -    then have "R O S\<^sup>* \<subseteq> (R \<union> S)\<^sup>* O R" using rtrancl_Un_subset by blast
   4.521 -    then have "?S \<subseteq> (R \<union> S)\<^sup>* O (R \<union> S)\<^sup>* O R" by (simp add: relcomp_mono rtrancl_mono)
   4.522 -    also have "\<dots> = (R \<union> S)\<^sup>* O R" by (simp add: O_assoc[symmetric])
   4.523 -    finally have "?S O (R \<union> S)\<^sup>* \<subseteq> (R \<union> S)\<^sup>* O R O (R \<union> S)\<^sup>*" by (simp add: O_assoc[symmetric] relcomp_mono)
   4.524 -    also have "\<dots> \<subseteq> (R \<union> S)\<^sup>* O (R \<union> S)\<^sup>* O R" using * by (simp add: relcomp_mono)
   4.525 -    finally have "?S O (R \<union> S)\<^sup>* \<subseteq> (R \<union> S)\<^sup>* O R" by (simp add: O_assoc[symmetric])
   4.526 -    then have "(?S O (R \<union> S)\<^sup>*) `` A \<subseteq> ((R \<union> S)\<^sup>* O R) `` A" by (simp add: Image_mono)
   4.527 -    moreover have "?X \<subseteq> (?S O (R \<union> S)\<^sup>*) `` A" using A by (auto simp: relcomp_Image)
   4.528 -    ultimately have "?X \<subseteq> R `` ?X" by (auto simp: relcomp_Image)
   4.529 -    then have "?X = {}" using \<open>wf R\<close> by (simp add: wfE_pf)
   4.530 +      then show ?thesis by auto
   4.531 +    qed
   4.532 +    then have "R O S\<^sup>* \<subseteq> (R \<union> S)\<^sup>* O R"
   4.533 +      using rtrancl_Un_subset by blast
   4.534 +    then have "?S \<subseteq> (R \<union> S)\<^sup>* O (R \<union> S)\<^sup>* O R"
   4.535 +      by (simp add: relcomp_mono rtrancl_mono)
   4.536 +    also have "\<dots> = (R \<union> S)\<^sup>* O R"
   4.537 +      by (simp add: O_assoc[symmetric])
   4.538 +    finally have "?S O (R \<union> S)\<^sup>* \<subseteq> (R \<union> S)\<^sup>* O R O (R \<union> S)\<^sup>*"
   4.539 +      by (simp add: O_assoc[symmetric] relcomp_mono)
   4.540 +    also have "\<dots> \<subseteq> (R \<union> S)\<^sup>* O (R \<union> S)\<^sup>* O R"
   4.541 +      using * by (simp add: relcomp_mono)
   4.542 +    finally have "?S O (R \<union> S)\<^sup>* \<subseteq> (R \<union> S)\<^sup>* O R"
   4.543 +      by (simp add: O_assoc[symmetric])
   4.544 +    then have "(?S O (R \<union> S)\<^sup>*) `` A \<subseteq> ((R \<union> S)\<^sup>* O R) `` A"
   4.545 +      by (simp add: Image_mono)
   4.546 +    moreover have "?X \<subseteq> (?S O (R \<union> S)\<^sup>*) `` A"
   4.547 +      using A by (auto simp: relcomp_Image)
   4.548 +    ultimately have "?X \<subseteq> R `` ?X"
   4.549 +      by (auto simp: relcomp_Image)
   4.550 +    then have "?X = {}"
   4.551 +      using \<open>wf R\<close> by (simp add: wfE_pf)
   4.552      moreover have "A \<subseteq> ?X" by auto
   4.553      ultimately show "A = {}" by simp
   4.554    qed
   4.555 @@ -443,22 +457,23 @@
   4.556  
   4.557  subsection \<open>Acyclic relations\<close>
   4.558  
   4.559 -lemma wf_acyclic: "wf r ==> acyclic r"
   4.560 +lemma wf_acyclic: "wf r \<Longrightarrow> acyclic r"
   4.561  apply (simp add: acyclic_def)
   4.562  apply (blast elim: wf_trancl [THEN wf_irrefl])
   4.563  done
   4.564  
   4.565  lemmas wfP_acyclicP = wf_acyclic [to_pred]
   4.566  
   4.567 -text\<open>Wellfoundedness of finite acyclic relations\<close>
   4.568 +
   4.569 +subsubsection \<open>Wellfoundedness of finite acyclic relations\<close>
   4.570  
   4.571 -lemma finite_acyclic_wf [rule_format]: "finite r ==> acyclic r --> wf r"
   4.572 +lemma finite_acyclic_wf [rule_format]: "finite r \<Longrightarrow> acyclic r \<longrightarrow> wf r"
   4.573  apply (erule finite_induct, blast)
   4.574 -apply (simp (no_asm_simp) only: split_tupled_all)
   4.575 +apply (simp only: split_tupled_all)
   4.576  apply simp
   4.577  done
   4.578  
   4.579 -lemma finite_acyclic_wf_converse: "[|finite r; acyclic r|] ==> wf (r^-1)"
   4.580 +lemma finite_acyclic_wf_converse: "finite r \<Longrightarrow> acyclic r \<Longrightarrow> wf (r\<inverse>)"
   4.581  apply (erule finite_converse [THEN iffD2, THEN finite_acyclic_wf])
   4.582  apply (erule acyclic_converse [THEN iffD2])
   4.583  done
   4.584 @@ -477,44 +492,39 @@
   4.585    with \<open>finite r\<close> show ?thesis by (rule finite_acyclic_wf_converse)
   4.586  qed
   4.587  
   4.588 -lemma wf_iff_acyclic_if_finite: "finite r ==> wf r = acyclic r"
   4.589 +lemma wf_iff_acyclic_if_finite: "finite r \<Longrightarrow> wf r = acyclic r"
   4.590  by (blast intro: finite_acyclic_wf wf_acyclic)
   4.591  
   4.592  
   4.593  subsection \<open>@{typ nat} is well-founded\<close>
   4.594  
   4.595 -lemma less_nat_rel: "op < = (\<lambda>m n. n = Suc m)^++"
   4.596 +lemma less_nat_rel: "op < = (\<lambda>m n. n = Suc m)\<^sup>+\<^sup>+"
   4.597  proof (rule ext, rule ext, rule iffI)
   4.598    fix n m :: nat
   4.599 -  assume "m < n"
   4.600 -  then show "(\<lambda>m n. n = Suc m)^++ m n"
   4.601 +  show "(\<lambda>m n. n = Suc m)\<^sup>+\<^sup>+ m n" if "m < n"
   4.602 +    using that
   4.603    proof (induct n)
   4.604 -    case 0 then show ?case by auto
   4.605 +    case 0
   4.606 +    then show ?case by auto
   4.607    next
   4.608 -    case (Suc n) then show ?case
   4.609 +    case (Suc n)
   4.610 +    then show ?case
   4.611        by (auto simp add: less_Suc_eq_le le_less intro: tranclp.trancl_into_trancl)
   4.612    qed
   4.613 -next
   4.614 -  fix n m :: nat
   4.615 -  assume "(\<lambda>m n. n = Suc m)^++ m n"
   4.616 -  then show "m < n"
   4.617 -    by (induct n)
   4.618 -      (simp_all add: less_Suc_eq_le reflexive le_less)
   4.619 +  show "m < n" if "(\<lambda>m n. n = Suc m)\<^sup>+\<^sup>+ m n"
   4.620 +    using that by (induct n) (simp_all add: less_Suc_eq_le reflexive le_less)
   4.621  qed
   4.622  
   4.623 -definition
   4.624 -  pred_nat :: "(nat * nat) set" where
   4.625 -  "pred_nat = {(m, n). n = Suc m}"
   4.626 +definition pred_nat :: "(nat \<times> nat) set"
   4.627 +  where "pred_nat = {(m, n). n = Suc m}"
   4.628  
   4.629 -definition
   4.630 -  less_than :: "(nat * nat) set" where
   4.631 -  "less_than = pred_nat^+"
   4.632 +definition less_than :: "(nat \<times> nat) set"
   4.633 +  where "less_than = pred_nat\<^sup>+"
   4.634  
   4.635 -lemma less_eq: "(m, n) \<in> pred_nat^+ \<longleftrightarrow> m < n"
   4.636 +lemma less_eq: "(m, n) \<in> pred_nat\<^sup>+ \<longleftrightarrow> m < n"
   4.637    unfolding less_nat_rel pred_nat_def trancl_def by simp
   4.638  
   4.639 -lemma pred_nat_trancl_eq_le:
   4.640 -  "(m, n) \<in> pred_nat^* \<longleftrightarrow> m \<le> n"
   4.641 +lemma pred_nat_trancl_eq_le: "(m, n) \<in> pred_nat\<^sup>* \<longleftrightarrow> m \<le> n"
   4.642    unfolding less_eq rtrancl_eq_or_trancl by auto
   4.643  
   4.644  lemma wf_pred_nat: "wf pred_nat"
   4.645 @@ -528,7 +538,7 @@
   4.646  lemma trans_less_than [iff]: "trans less_than"
   4.647    by (simp add: less_than_def)
   4.648  
   4.649 -lemma less_than_iff [iff]: "((x,y): less_than) = (x<y)"
   4.650 +lemma less_than_iff [iff]: "((x,y) \<in> less_than) = (x<y)"
   4.651    by (simp add: less_than_def less_eq)
   4.652  
   4.653  lemma wf_less: "wf {(x, y::nat). x < y}"
   4.654 @@ -538,28 +548,22 @@
   4.655  subsection \<open>Accessible Part\<close>
   4.656  
   4.657  text \<open>
   4.658 - Inductive definition of the accessible part @{term "acc r"} of a
   4.659 - relation; see also @{cite "paulin-tlca"}.
   4.660 +  Inductive definition of the accessible part \<open>acc r\<close> of a
   4.661 +  relation; see also @{cite "paulin-tlca"}.
   4.662  \<close>
   4.663  
   4.664 -inductive_set
   4.665 -  acc :: "('a * 'a) set => 'a set"
   4.666 -  for r :: "('a * 'a) set"
   4.667 -  where
   4.668 -    accI: "(!!y. (y, x) : r ==> y : acc r) ==> x : acc r"
   4.669 +inductive_set acc :: "('a \<times> 'a) set \<Rightarrow> 'a set" for r :: "('a \<times> 'a) set"
   4.670 +  where accI: "(\<And>y. (y, x) \<in> r \<Longrightarrow> y \<in> acc r) \<Longrightarrow> x \<in> acc r"
   4.671  
   4.672 -abbreviation
   4.673 -  termip :: "('a => 'a => bool) => 'a => bool" where
   4.674 -  "termip r \<equiv> accp (r\<inverse>\<inverse>)"
   4.675 +abbreviation termip :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> bool"
   4.676 +  where "termip r \<equiv> accp (r\<inverse>\<inverse>)"
   4.677  
   4.678 -abbreviation
   4.679 -  termi :: "('a * 'a) set => 'a set" where
   4.680 -  "termi r \<equiv> acc (r\<inverse>)"
   4.681 +abbreviation termi :: "('a \<times> 'a) set \<Rightarrow> 'a set"
   4.682 +  where "termi r \<equiv> acc (r\<inverse>)"
   4.683  
   4.684  lemmas accpI = accp.accI
   4.685  
   4.686 -lemma accp_eq_acc [code]:
   4.687 -  "accp r = (\<lambda>x. x \<in> Wellfounded.acc {(x, y). r x y})"
   4.688 +lemma accp_eq_acc [code]: "accp r = (\<lambda>x. x \<in> Wellfounded.acc {(x, y). r x y})"
   4.689    by (simp add: acc_def)
   4.690  
   4.691  
   4.692 @@ -567,7 +571,7 @@
   4.693  
   4.694  theorem accp_induct:
   4.695    assumes major: "accp r a"
   4.696 -  assumes hyp: "!!x. accp r x ==> \<forall>y. r y x --> P y ==> P x"
   4.697 +  assumes hyp: "\<And>x. accp r x \<Longrightarrow> \<forall>y. r y x \<longrightarrow> P y \<Longrightarrow> P x"
   4.698    shows "P a"
   4.699    apply (rule major [THEN accp.induct])
   4.700    apply (rule hyp)
   4.701 @@ -578,7 +582,7 @@
   4.702  
   4.703  lemmas accp_induct_rule = accp_induct [rule_format, induct set: accp]
   4.704  
   4.705 -theorem accp_downward: "accp r b ==> r a b ==> accp r a"
   4.706 +theorem accp_downward: "accp r b \<Longrightarrow> r a b \<Longrightarrow> accp r a"
   4.707    apply (erule accp.cases)
   4.708    apply fast
   4.709    done
   4.710 @@ -588,13 +592,11 @@
   4.711    obtains z where "R z x" and "\<not> accp R z"
   4.712  proof -
   4.713    assume a: "\<And>z. \<lbrakk>R z x; \<not> accp R z\<rbrakk> \<Longrightarrow> thesis"
   4.714 -
   4.715    show thesis
   4.716    proof (cases "\<forall>z. R z x \<longrightarrow> accp R z")
   4.717      case True
   4.718 -    hence "\<And>z. R z x \<Longrightarrow> accp R z" by auto
   4.719 -    hence "accp R x"
   4.720 -      by (rule accp.accI)
   4.721 +    then have "\<And>z. R z x \<Longrightarrow> accp R z" by auto
   4.722 +    then have "accp R x" by (rule accp.accI)
   4.723      with na show thesis ..
   4.724    next
   4.725      case False then obtain z where "R z x" and "\<not> accp R z"
   4.726 @@ -603,24 +605,24 @@
   4.727    qed
   4.728  qed
   4.729  
   4.730 -lemma accp_downwards_aux: "r\<^sup>*\<^sup>* b a ==> accp r a --> accp r b"
   4.731 +lemma accp_downwards_aux: "r\<^sup>*\<^sup>* b a \<Longrightarrow> accp r a \<longrightarrow> accp r b"
   4.732    apply (erule rtranclp_induct)
   4.733     apply blast
   4.734    apply (blast dest: accp_downward)
   4.735    done
   4.736  
   4.737 -theorem accp_downwards: "accp r a ==> r\<^sup>*\<^sup>* b a ==> accp r b"
   4.738 +theorem accp_downwards: "accp r a \<Longrightarrow> r\<^sup>*\<^sup>* b a \<Longrightarrow> accp r b"
   4.739    apply (blast dest: accp_downwards_aux)
   4.740    done
   4.741  
   4.742 -theorem accp_wfPI: "\<forall>x. accp r x ==> wfP r"
   4.743 +theorem accp_wfPI: "\<forall>x. accp r x \<Longrightarrow> wfP r"
   4.744    apply (rule wfPUNIVI)
   4.745    apply (rule_tac P=P in accp_induct)
   4.746     apply blast
   4.747    apply blast
   4.748    done
   4.749  
   4.750 -theorem accp_wfPD: "wfP r ==> accp r x"
   4.751 +theorem accp_wfPD: "wfP r \<Longrightarrow> accp r x"
   4.752    apply (erule wfP_induct_rule)
   4.753    apply (rule accp.accI)
   4.754    apply blast
   4.755 @@ -673,25 +675,15 @@
   4.756  text \<open>Set versions of the above theorems\<close>
   4.757  
   4.758  lemmas acc_induct = accp_induct [to_set]
   4.759 -
   4.760  lemmas acc_induct_rule = acc_induct [rule_format, induct set: acc]
   4.761 -
   4.762  lemmas acc_downward = accp_downward [to_set]
   4.763 -
   4.764  lemmas not_acc_down = not_accp_down [to_set]
   4.765 -
   4.766  lemmas acc_downwards_aux = accp_downwards_aux [to_set]
   4.767 -
   4.768  lemmas acc_downwards = accp_downwards [to_set]
   4.769 -
   4.770  lemmas acc_wfI = accp_wfPI [to_set]
   4.771 -
   4.772  lemmas acc_wfD = accp_wfPD [to_set]
   4.773 -
   4.774  lemmas wf_acc_iff = wfP_accp_iff [to_set]
   4.775 -
   4.776  lemmas acc_subset = accp_subset [to_set]
   4.777 -
   4.778  lemmas acc_subset_induct = accp_subset_induct [to_set]
   4.779  
   4.780  
   4.781 @@ -699,10 +691,10 @@
   4.782  
   4.783  text \<open>Inverse Image\<close>
   4.784  
   4.785 -lemma wf_inv_image [simp,intro!]: "wf(r) ==> wf(inv_image r (f::'a=>'b))"
   4.786 -apply (simp (no_asm_use) add: inv_image_def wf_eq_minimal)
   4.787 +lemma wf_inv_image [simp,intro!]: "wf r \<Longrightarrow> wf (inv_image r f)" for f :: "'a \<Rightarrow> 'b"
   4.788 +apply (simp add: inv_image_def wf_eq_minimal)
   4.789  apply clarify
   4.790 -apply (subgoal_tac "EX (w::'b) . w : {w. EX (x::'a) . x: Q & (f x = w) }")
   4.791 +apply (subgoal_tac "\<exists>w::'b. w \<in> {w. \<exists>x::'a. x \<in> Q \<and> f x = w}")
   4.792  prefer 2 apply (blast del: allE)
   4.793  apply (erule allE)
   4.794  apply (erule (1) notE impE)
   4.795 @@ -711,10 +703,10 @@
   4.796  
   4.797  text \<open>Measure functions into @{typ nat}\<close>
   4.798  
   4.799 -definition measure :: "('a => nat) => ('a * 'a)set"
   4.800 -where "measure = inv_image less_than"
   4.801 +definition measure :: "('a \<Rightarrow> nat) \<Rightarrow> ('a \<times> 'a) set"
   4.802 +  where "measure = inv_image less_than"
   4.803  
   4.804 -lemma in_measure[simp, code_unfold]: "((x,y) : measure f) = (f x < f y)"
   4.805 +lemma in_measure[simp, code_unfold]: "(x, y) \<in> measure f \<longleftrightarrow> f x < f y"
   4.806    by (simp add:measure_def)
   4.807  
   4.808  lemma wf_measure [iff]: "wf (measure f)"
   4.809 @@ -722,8 +714,8 @@
   4.810  apply (rule wf_less_than [THEN wf_inv_image])
   4.811  done
   4.812  
   4.813 -lemma wf_if_measure: fixes f :: "'a \<Rightarrow> nat"
   4.814 -shows "(!!x. P x \<Longrightarrow> f(g x) < f x) \<Longrightarrow> wf {(y,x). P x \<and> y = g x}"
   4.815 +lemma wf_if_measure: "(\<And>x. P x \<Longrightarrow> f(g x) < f x) \<Longrightarrow> wf {(y,x). P x \<and> y = g x}"
   4.816 +  for f :: "'a \<Rightarrow> nat"
   4.817  apply(insert wf_measure[of f])
   4.818  apply(simp only: measure_def inv_image_def less_than_def less_eq)
   4.819  apply(erule wf_subset)
   4.820 @@ -731,69 +723,66 @@
   4.821  done
   4.822  
   4.823  
   4.824 -text\<open>Lexicographic combinations\<close>
   4.825 +subsubsection \<open>Lexicographic combinations\<close>
   4.826  
   4.827 -definition lex_prod :: "('a \<times>'a) set \<Rightarrow> ('b \<times> 'b) set \<Rightarrow> (('a \<times> 'b) \<times> ('a \<times> 'b)) set" (infixr "<*lex*>" 80) where
   4.828 -  "ra <*lex*> rb = {((a, b), (a', b')). (a, a') \<in> ra \<or> a = a' \<and> (b, b') \<in> rb}"
   4.829 +definition lex_prod :: "('a \<times>'a) set \<Rightarrow> ('b \<times> 'b) set \<Rightarrow> (('a \<times> 'b) \<times> ('a \<times> 'b)) set"
   4.830 +    (infixr "<*lex*>" 80)
   4.831 +  where "ra <*lex*> rb = {((a, b), (a', b')). (a, a') \<in> ra \<or> a = a' \<and> (b, b') \<in> rb}"
   4.832  
   4.833 -lemma wf_lex_prod [intro!]: "[| wf(ra); wf(rb) |] ==> wf(ra <*lex*> rb)"
   4.834 -apply (unfold wf_def lex_prod_def) 
   4.835 +lemma wf_lex_prod [intro!]: "wf ra \<Longrightarrow> wf rb \<Longrightarrow> wf (ra <*lex*> rb)"
   4.836 +apply (unfold wf_def lex_prod_def)
   4.837  apply (rule allI, rule impI)
   4.838 -apply (simp (no_asm_use) only: split_paired_All)
   4.839 -apply (drule spec, erule mp) 
   4.840 +apply (simp only: split_paired_All)
   4.841 +apply (drule spec, erule mp)
   4.842  apply (rule allI, rule impI)
   4.843 -apply (drule spec, erule mp, blast) 
   4.844 +apply (drule spec, erule mp, blast)
   4.845  done
   4.846  
   4.847 -lemma in_lex_prod[simp]: 
   4.848 -  "(((a,b),(a',b')): r <*lex*> s) = ((a,a'): r \<or> (a = a' \<and> (b, b') : s))"
   4.849 +lemma in_lex_prod[simp]: "((a, b), (a', b')) \<in> r <*lex*> s \<longleftrightarrow> (a, a') \<in> r \<or> a = a' \<and> (b, b') \<in> s"
   4.850    by (auto simp:lex_prod_def)
   4.851  
   4.852 -text\<open>@{term "op <*lex*>"} preserves transitivity\<close>
   4.853 +text \<open>\<open><*lex*>\<close> preserves transitivity\<close>
   4.854 +lemma trans_lex_prod [intro!]: "trans R1 \<Longrightarrow> trans R2 \<Longrightarrow> trans (R1 <*lex*> R2)"
   4.855 +  unfolding trans_def lex_prod_def by blast
   4.856  
   4.857 -lemma trans_lex_prod [intro!]: 
   4.858 -    "[| trans R1; trans R2 |] ==> trans (R1 <*lex*> R2)"
   4.859 -by (unfold trans_def lex_prod_def, blast) 
   4.860  
   4.861  text \<open>lexicographic combinations with measure functions\<close>
   4.862  
   4.863 -definition 
   4.864 -  mlex_prod :: "('a \<Rightarrow> nat) \<Rightarrow> ('a \<times> 'a) set \<Rightarrow> ('a \<times> 'a) set" (infixr "<*mlex*>" 80)
   4.865 -where
   4.866 -  "f <*mlex*> R = inv_image (less_than <*lex*> R) (%x. (f x, x))"
   4.867 +definition mlex_prod :: "('a \<Rightarrow> nat) \<Rightarrow> ('a \<times> 'a) set \<Rightarrow> ('a \<times> 'a) set" (infixr "<*mlex*>" 80)
   4.868 +  where "f <*mlex*> R = inv_image (less_than <*lex*> R) (\<lambda>x. (f x, x))"
   4.869  
   4.870  lemma wf_mlex: "wf R \<Longrightarrow> wf (f <*mlex*> R)"
   4.871 -unfolding mlex_prod_def
   4.872 -by auto
   4.873 +  unfolding mlex_prod_def
   4.874 +  by auto
   4.875  
   4.876  lemma mlex_less: "f x < f y \<Longrightarrow> (x, y) \<in> f <*mlex*> R"
   4.877 -unfolding mlex_prod_def by simp
   4.878 +  unfolding mlex_prod_def by simp
   4.879  
   4.880  lemma mlex_leq: "f x \<le> f y \<Longrightarrow> (x, y) \<in> R \<Longrightarrow> (x, y) \<in> f <*mlex*> R"
   4.881 -unfolding mlex_prod_def by auto
   4.882 +  unfolding mlex_prod_def by auto
   4.883  
   4.884  text \<open>proper subset relation on finite sets\<close>
   4.885  
   4.886 -definition finite_psubset  :: "('a set * 'a set) set"
   4.887 -where "finite_psubset = {(A,B). A < B & finite B}"
   4.888 +definition finite_psubset :: "('a set \<times> 'a set) set"
   4.889 +  where "finite_psubset = {(A,B). A < B \<and> finite B}"
   4.890  
   4.891 -lemma wf_finite_psubset[simp]: "wf(finite_psubset)"
   4.892 -apply (unfold finite_psubset_def)
   4.893 -apply (rule wf_measure [THEN wf_subset])
   4.894 -apply (simp add: measure_def inv_image_def less_than_def less_eq)
   4.895 -apply (fast elim!: psubset_card_mono)
   4.896 -done
   4.897 +lemma wf_finite_psubset[simp]: "wf finite_psubset"
   4.898 +  apply (unfold finite_psubset_def)
   4.899 +  apply (rule wf_measure [THEN wf_subset])
   4.900 +  apply (simp add: measure_def inv_image_def less_than_def less_eq)
   4.901 +  apply (fast elim!: psubset_card_mono)
   4.902 +  done
   4.903  
   4.904  lemma trans_finite_psubset: "trans finite_psubset"
   4.905 -by (simp add: finite_psubset_def less_le trans_def, blast)
   4.906 +  by (auto simp add: finite_psubset_def less_le trans_def)
   4.907  
   4.908 -lemma in_finite_psubset[simp]: "(A, B) \<in> finite_psubset = (A < B & finite B)"
   4.909 -unfolding finite_psubset_def by auto
   4.910 +lemma in_finite_psubset[simp]: "(A, B) \<in> finite_psubset \<longleftrightarrow> A < B \<and> finite B"
   4.911 +  unfolding finite_psubset_def by auto
   4.912  
   4.913  text \<open>max- and min-extension of order to finite sets\<close>
   4.914  
   4.915 -inductive_set max_ext :: "('a \<times> 'a) set \<Rightarrow> ('a set \<times> 'a set) set" 
   4.916 -for R :: "('a \<times> 'a) set"
   4.917 +inductive_set max_ext :: "('a \<times> 'a) set \<Rightarrow> ('a set \<times> 'a set) set"
   4.918 +  for R :: "('a \<times> 'a) set"
   4.919  where
   4.920    max_extI[intro]: "finite X \<Longrightarrow> finite Y \<Longrightarrow> Y \<noteq> {} \<Longrightarrow> (\<And>x. x \<in> X \<Longrightarrow> \<exists>y\<in>Y. (x, y) \<in> R) \<Longrightarrow> (X, Y) \<in> max_ext R"
   4.921  
   4.922 @@ -801,10 +790,11 @@
   4.923    assumes wf: "wf r"
   4.924    shows "wf (max_ext r)"
   4.925  proof (rule acc_wfI, intro allI)
   4.926 -  fix M show "M \<in> acc (max_ext r)" (is "_ \<in> ?W")
   4.927 +  fix M
   4.928 +  show "M \<in> acc (max_ext r)" (is "_ \<in> ?W")
   4.929    proof cases
   4.930      assume "finite M"
   4.931 -    thus ?thesis
   4.932 +    then show ?thesis
   4.933      proof (induct M)
   4.934        show "{} \<in> ?W"
   4.935          by (rule accI) (auto elim: max_ext.cases)
   4.936 @@ -815,42 +805,37 @@
   4.937          fix M a
   4.938          assume "M \<in> ?W"  and  [intro]: "finite M"
   4.939          assume hyp: "\<And>b M. (b, a) \<in> r \<Longrightarrow> M \<in> ?W \<Longrightarrow> finite M \<Longrightarrow> insert b M \<in> ?W"
   4.940 -        {
   4.941 -          fix N M :: "'a set"
   4.942 -          assume "finite N" "finite M"
   4.943 -          then
   4.944 -          have "\<lbrakk>M \<in> ?W ; (\<And>y. y \<in> N \<Longrightarrow> (y, a) \<in> r)\<rbrakk> \<Longrightarrow>  N \<union> M \<in> ?W"
   4.945 -            by (induct N arbitrary: M) (auto simp: hyp)
   4.946 -        }
   4.947 -        note add_less = this
   4.948 -        
   4.949 +        have add_less: "\<lbrakk>M \<in> ?W ; (\<And>y. y \<in> N \<Longrightarrow> (y, a) \<in> r)\<rbrakk> \<Longrightarrow> N \<union> M \<in> ?W"
   4.950 +          if "finite N" "finite M" for N M :: "'a set"
   4.951 +          using that by (induct N arbitrary: M) (auto simp: hyp)
   4.952 +
   4.953          show "insert a M \<in> ?W"
   4.954          proof (rule accI)
   4.955 -          fix N assume Nless: "(N, insert a M) \<in> max_ext r"
   4.956 -          hence asm1: "\<And>x. x \<in> N \<Longrightarrow> (x, a) \<in> r \<or> (\<exists>y \<in> M. (x, y) \<in> r)"
   4.957 +          fix N
   4.958 +          assume Nless: "(N, insert a M) \<in> max_ext r"
   4.959 +          then have *: "\<And>x. x \<in> N \<Longrightarrow> (x, a) \<in> r \<or> (\<exists>y \<in> M. (x, y) \<in> r)"
   4.960              by (auto elim!: max_ext.cases)
   4.961  
   4.962 -          let ?N1 = "{ n \<in> N. (n, a) \<in> r }"
   4.963 -          let ?N2 = "{ n \<in> N. (n, a) \<notin> r }"
   4.964 +          let ?N1 = "{n \<in> N. (n, a) \<in> r}"
   4.965 +          let ?N2 = "{n \<in> N. (n, a) \<notin> r}"
   4.966            have N: "?N1 \<union> ?N2 = N" by (rule set_eqI) auto
   4.967            from Nless have "finite N" by (auto elim: max_ext.cases)
   4.968            then have finites: "finite ?N1" "finite ?N2" by auto
   4.969 -          
   4.970 +
   4.971            have "?N2 \<in> ?W"
   4.972            proof cases
   4.973              assume [simp]: "M = {}"
   4.974              have Mw: "{} \<in> ?W" by (rule accI) (auto elim: max_ext.cases)
   4.975  
   4.976 -            from asm1 have "?N2 = {}" by auto
   4.977 +            from * have "?N2 = {}" by auto
   4.978              with Mw show "?N2 \<in> ?W" by (simp only:)
   4.979            next
   4.980              assume "M \<noteq> {}"
   4.981 -            from asm1 finites have N2: "(?N2, M) \<in> max_ext r" 
   4.982 +            from * finites have N2: "(?N2, M) \<in> max_ext r"
   4.983                by (rule_tac max_extI[OF _ _ \<open>M \<noteq> {}\<close>]) auto
   4.984 -
   4.985              with \<open>M \<in> ?W\<close> show "?N2 \<in> ?W" by (rule acc_downward)
   4.986            qed
   4.987 -          with finites have "?N1 \<union> ?N2 \<in> ?W" 
   4.988 +          with finites have "?N1 \<union> ?N2 \<in> ?W"
   4.989              by (rule add_less) simp
   4.990            then show "N \<in> ?W" by (simp only: N)
   4.991          qed
   4.992 @@ -863,32 +848,30 @@
   4.993    qed
   4.994  qed
   4.995  
   4.996 -lemma max_ext_additive: 
   4.997 - "(A, B) \<in> max_ext R \<Longrightarrow> (C, D) \<in> max_ext R \<Longrightarrow>
   4.998 -  (A \<union> C, B \<union> D) \<in> max_ext R"
   4.999 -by (force elim!: max_ext.cases)
  4.1000 +lemma max_ext_additive:
  4.1001 +  "(A, B) \<in> max_ext R \<Longrightarrow> (C, D) \<in> max_ext R \<Longrightarrow>
  4.1002 +    (A \<union> C, B \<union> D) \<in> max_ext R"
  4.1003 +  by (force elim!: max_ext.cases)
  4.1004  
  4.1005  
  4.1006 -definition min_ext :: "('a \<times> 'a) set \<Rightarrow> ('a set \<times> 'a set) set"  where
  4.1007 -  "min_ext r = {(X, Y) | X Y. X \<noteq> {} \<and> (\<forall>y \<in> Y. (\<exists>x \<in> X. (x, y) \<in> r))}"
  4.1008 +definition min_ext :: "('a \<times> 'a) set \<Rightarrow> ('a set \<times> 'a set) set"
  4.1009 +  where "min_ext r = {(X, Y) | X Y. X \<noteq> {} \<and> (\<forall>y \<in> Y. (\<exists>x \<in> X. (x, y) \<in> r))}"
  4.1010  
  4.1011  lemma min_ext_wf:
  4.1012    assumes "wf r"
  4.1013    shows "wf (min_ext r)"
  4.1014  proof (rule wfI_min)
  4.1015 -  fix Q :: "'a set set"
  4.1016 -  fix x
  4.1017 -  assume nonempty: "x \<in> Q"
  4.1018 -  show "\<exists>m \<in> Q. (\<forall> n. (n, m) \<in> min_ext r \<longrightarrow> n \<notin> Q)"
  4.1019 -  proof cases
  4.1020 -    assume "Q = {{}}" thus ?thesis by (simp add: min_ext_def)
  4.1021 +  show "\<exists>m \<in> Q. (\<forall> n. (n, m) \<in> min_ext r \<longrightarrow> n \<notin> Q)" if nonempty: "x \<in> Q"
  4.1022 +    for Q :: "'a set set" and x
  4.1023 +  proof (cases "Q = {{}}")
  4.1024 +    case True
  4.1025 +    then show ?thesis by (simp add: min_ext_def)
  4.1026    next
  4.1027 -    assume "Q \<noteq> {{}}"
  4.1028 -    with nonempty
  4.1029 -    obtain e x where "x \<in> Q" "e \<in> x" by force
  4.1030 +    case False
  4.1031 +    with nonempty obtain e x where "x \<in> Q" "e \<in> x" by force
  4.1032      then have eU: "e \<in> \<Union>Q" by auto
  4.1033 -    with \<open>wf r\<close> 
  4.1034 -    obtain z where z: "z \<in> \<Union>Q" "\<And>y. (y, z) \<in> r \<Longrightarrow> y \<notin> \<Union>Q" 
  4.1035 +    with \<open>wf r\<close>
  4.1036 +    obtain z where z: "z \<in> \<Union>Q" "\<And>y. (y, z) \<in> r \<Longrightarrow> y \<notin> \<Union>Q"
  4.1037        by (erule wfE_min)
  4.1038      from z obtain m where "m \<in> Q" "z \<in> m" by auto
  4.1039      from \<open>m \<in> Q\<close>
  4.1040 @@ -898,36 +881,38 @@
  4.1041        assume smaller: "(n, m) \<in> min_ext r"
  4.1042        with \<open>z \<in> m\<close> obtain y where y: "y \<in> n" "(y, z) \<in> r" by (auto simp: min_ext_def)
  4.1043        then show "n \<notin> Q" using z(2) by auto
  4.1044 -    qed      
  4.1045 +    qed
  4.1046    qed
  4.1047  qed
  4.1048  
  4.1049 -text\<open>Bounded increase must terminate:\<close>
  4.1050 +
  4.1051 +subsubsection \<open>Bounded increase must terminate\<close>
  4.1052  
  4.1053  lemma wf_bounded_measure:
  4.1054 -fixes ub :: "'a \<Rightarrow> nat" and f :: "'a \<Rightarrow> nat"
  4.1055 -assumes "!!a b. (b,a) : r \<Longrightarrow> ub b \<le> ub a & ub a \<ge> f b & f b > f a"
  4.1056 -shows "wf r"
  4.1057 -apply(rule wf_subset[OF wf_measure[of "%a. ub a - f a"]])
  4.1058 -apply (auto dest: assms)
  4.1059 -done
  4.1060 +  fixes ub :: "'a \<Rightarrow> nat"
  4.1061 +    and f :: "'a \<Rightarrow> nat"
  4.1062 +  assumes "\<And>a b. (b, a) \<in> r \<Longrightarrow> ub b \<le> ub a \<and> ub a \<ge> f b \<and> f b > f a"
  4.1063 +  shows "wf r"
  4.1064 +  apply (rule wf_subset[OF wf_measure[of "\<lambda>a. ub a - f a"]])
  4.1065 +  apply (auto dest: assms)
  4.1066 +  done
  4.1067  
  4.1068  lemma wf_bounded_set:
  4.1069 -fixes ub :: "'a \<Rightarrow> 'b set" and f :: "'a \<Rightarrow> 'b set"
  4.1070 -assumes "!!a b. (b,a) : r \<Longrightarrow>
  4.1071 -  finite(ub a) & ub b \<subseteq> ub a & ub a \<supseteq> f b & f b \<supset> f a"
  4.1072 -shows "wf r"
  4.1073 -apply(rule wf_bounded_measure[of r "%a. card(ub a)" "%a. card(f a)"])
  4.1074 -apply(drule assms)
  4.1075 -apply (blast intro: card_mono finite_subset psubset_card_mono dest: psubset_eq[THEN iffD2])
  4.1076 -done
  4.1077 +  fixes ub :: "'a \<Rightarrow> 'b set"
  4.1078 +    and f :: "'a \<Rightarrow> 'b set"
  4.1079 +  assumes "\<And>a b. (b,a) \<in> r \<Longrightarrow> finite (ub a) \<and> ub b \<subseteq> ub a \<and> ub a \<supseteq> f b \<and> f b \<supset> f a"
  4.1080 +  shows "wf r"
  4.1081 +  apply(rule wf_bounded_measure[of r "\<lambda>a. card(ub a)" "\<lambda>a. card(f a)"])
  4.1082 +  apply(drule assms)
  4.1083 +  apply (blast intro: card_mono finite_subset psubset_card_mono dest: psubset_eq[THEN iffD2])
  4.1084 +  done
  4.1085  
  4.1086  lemma finite_subset_wf:
  4.1087    assumes "finite A"
  4.1088    shows   "wf {(X,Y). X \<subset> Y \<and> Y \<subseteq> A}"
  4.1089  proof (intro finite_acyclic_wf)
  4.1090    have "{(X,Y). X \<subset> Y \<and> Y \<subseteq> A} \<subseteq> Pow A \<times> Pow A" by blast
  4.1091 -  thus "finite {(X,Y). X \<subset> Y \<and> Y \<subseteq> A}" 
  4.1092 +  then show "finite {(X,Y). X \<subset> Y \<and> Y \<subseteq> A}"
  4.1093      by (rule finite_subset) (auto simp: assms finite_cartesian_product)
  4.1094  next
  4.1095    have "{(X, Y). X \<subset> Y \<and> Y \<subseteq> A}\<^sup>+ = {(X, Y). X \<subset> Y \<and> Y \<subseteq> A}"