# HG changeset patch
# User wenzelm
# Date 1470413668 -7200
# Node ID 7195acc2fe935ad710bf32c842754d93543c78fd
# Parent  fb63942e470eeceddb53b8fcd55dfade24b7e7ef
misc tuning and modernization;

diff -r fb63942e470e -r 7195acc2fe93 src/HOL/Complete_Partial_Order.thy
--- a/src/HOL/Complete_Partial_Order.thy	Fri Aug 05 16:36:03 2016 +0200
+++ b/src/HOL/Complete_Partial_Order.thy	Fri Aug 05 18:14:28 2016 +0200
@@ -1,12 +1,12 @@
-(* Title:    HOL/Complete_Partial_Order.thy
-   Author:   Brian Huffman, Portland State University
-   Author:   Alexander Krauss, TU Muenchen
+(*  Title:      HOL/Complete_Partial_Order.thy
+    Author:     Brian Huffman, Portland State University
+    Author:     Alexander Krauss, TU Muenchen
 *)
 
 section \<open>Chain-complete partial orders and their fixpoints\<close>
 
 theory Complete_Partial_Order
-imports Product_Type
+  imports Product_Type
 begin
 
 subsection \<open>Monotone functions\<close>
@@ -14,131 +14,139 @@
 text \<open>Dictionary-passing version of @{const Orderings.mono}.\<close>
 
 definition monotone :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> ('b \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> bool"
-where "monotone orda ordb f \<longleftrightarrow> (\<forall>x y. orda x y \<longrightarrow> ordb (f x) (f y))"
+  where "monotone orda ordb f \<longleftrightarrow> (\<forall>x y. orda x y \<longrightarrow> ordb (f x) (f y))"
 
-lemma monotoneI[intro?]: "(\<And>x y. orda x y \<Longrightarrow> ordb (f x) (f y))
- \<Longrightarrow> monotone orda ordb f"
-unfolding monotone_def by iprover
+lemma monotoneI[intro?]: "(\<And>x y. orda x y \<Longrightarrow> ordb (f x) (f y)) \<Longrightarrow> monotone orda ordb f"
+  unfolding monotone_def by iprover
 
 lemma monotoneD[dest?]: "monotone orda ordb f \<Longrightarrow> orda x y \<Longrightarrow> ordb (f x) (f y)"
-unfolding monotone_def by iprover
+  unfolding monotone_def by iprover
 
 
 subsection \<open>Chains\<close>
 
-text \<open>A chain is a totally-ordered set. Chains are parameterized over
+text \<open>
+  A chain is a totally-ordered set. Chains are parameterized over
   the order for maximal flexibility, since type classes are not enough.
 \<close>
 
-definition
-  chain :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a set \<Rightarrow> bool"
-where
-  "chain ord S \<longleftrightarrow> (\<forall>x\<in>S. \<forall>y\<in>S. ord x y \<or> ord y x)"
+definition chain :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a set \<Rightarrow> bool"
+  where "chain ord S \<longleftrightarrow> (\<forall>x\<in>S. \<forall>y\<in>S. ord x y \<or> ord y x)"
 
 lemma chainI:
   assumes "\<And>x y. x \<in> S \<Longrightarrow> y \<in> S \<Longrightarrow> ord x y \<or> ord y x"
   shows "chain ord S"
-using assms unfolding chain_def by fast
+  using assms unfolding chain_def by fast
 
 lemma chainD:
   assumes "chain ord S" and "x \<in> S" and "y \<in> S"
   shows "ord x y \<or> ord y x"
-using assms unfolding chain_def by fast
+  using assms unfolding chain_def by fast
 
 lemma chainE:
   assumes "chain ord S" and "x \<in> S" and "y \<in> S"
   obtains "ord x y" | "ord y x"
-using assms unfolding chain_def by fast
+  using assms unfolding chain_def by fast
 
 lemma chain_empty: "chain ord {}"
-by(simp add: chain_def)
+  by (simp add: chain_def)
 
 lemma chain_equality: "chain op = A \<longleftrightarrow> (\<forall>x\<in>A. \<forall>y\<in>A. x = y)"
-by(auto simp add: chain_def)
+  by (auto simp add: chain_def)
+
+lemma chain_subset: "chain ord A \<Longrightarrow> B \<subseteq> A \<Longrightarrow> chain ord B"
+  by (rule chainI) (blast dest: chainD)
 
-lemma chain_subset:
-  "\<lbrakk> chain ord A; B \<subseteq> A \<rbrakk>
-  \<Longrightarrow> chain ord B"
-by(rule chainI)(blast dest: chainD)
+lemma chain_imageI:
+  assumes chain: "chain le_a Y"
+    and mono: "\<And>x y. x \<in> Y \<Longrightarrow> y \<in> Y \<Longrightarrow> le_a x y \<Longrightarrow> le_b (f x) (f y)"
+  shows "chain le_b (f ` Y)"
+  by (blast intro: chainI dest: chainD[OF chain] mono)
 
-lemma chain_imageI: 
-  assumes chain: "chain le_a Y"
-  and mono: "\<And>x y. \<lbrakk> x \<in> Y; y \<in> Y; le_a x y \<rbrakk> \<Longrightarrow> le_b (f x) (f y)"
-  shows "chain le_b (f ` Y)"
-by(blast intro: chainI dest: chainD[OF chain] mono)
 
 subsection \<open>Chain-complete partial orders\<close>
 
 text \<open>
-  A ccpo has a least upper bound for any chain.  In particular, the
-  empty set is a chain, so every ccpo must have a bottom element.
+  A \<open>ccpo\<close> has a least upper bound for any chain.  In particular, the
+  empty set is a chain, so every \<open>ccpo\<close> must have a bottom element.
 \<close>
 
 class ccpo = order + Sup +
-  assumes ccpo_Sup_upper: "\<lbrakk>chain (op \<le>) A; x \<in> A\<rbrakk> \<Longrightarrow> x \<le> Sup A"
-  assumes ccpo_Sup_least: "\<lbrakk>chain (op \<le>) A; \<And>x. x \<in> A \<Longrightarrow> x \<le> z\<rbrakk> \<Longrightarrow> Sup A \<le> z"
+  assumes ccpo_Sup_upper: "chain (op \<le>) A \<Longrightarrow> x \<in> A \<Longrightarrow> x \<le> Sup A"
+  assumes ccpo_Sup_least: "chain (op \<le>) A \<Longrightarrow> (\<And>x. x \<in> A \<Longrightarrow> x \<le> z) \<Longrightarrow> Sup A \<le> z"
 begin
 
 lemma chain_singleton: "Complete_Partial_Order.chain op \<le> {x}"
-by(rule chainI) simp
+  by (rule chainI) simp
 
 lemma ccpo_Sup_singleton [simp]: "\<Squnion>{x} = x"
-by(rule antisym)(auto intro: ccpo_Sup_least ccpo_Sup_upper simp add: chain_singleton)
+  by (rule antisym)(auto intro: ccpo_Sup_least ccpo_Sup_upper simp add: chain_singleton)
+
 
 subsection \<open>Transfinite iteration of a function\<close>
 
-context notes [[inductive_internals]] begin
+context notes [[inductive_internals]]
+begin
 
 inductive_set iterates :: "('a \<Rightarrow> 'a) \<Rightarrow> 'a set"
-for f :: "'a \<Rightarrow> 'a"
-where
-  step: "x \<in> iterates f \<Longrightarrow> f x \<in> iterates f"
-| Sup: "chain (op \<le>) M \<Longrightarrow> \<forall>x\<in>M. x \<in> iterates f \<Longrightarrow> Sup M \<in> iterates f"
+  for f :: "'a \<Rightarrow> 'a"
+  where
+    step: "x \<in> iterates f \<Longrightarrow> f x \<in> iterates f"
+  | Sup: "chain (op \<le>) M \<Longrightarrow> \<forall>x\<in>M. x \<in> iterates f \<Longrightarrow> Sup M \<in> iterates f"
 
 end
 
-lemma iterates_le_f:
-  "x \<in> iterates f \<Longrightarrow> monotone (op \<le>) (op \<le>) f \<Longrightarrow> x \<le> f x"
-by (induct x rule: iterates.induct)
-  (force dest: monotoneD intro!: ccpo_Sup_upper ccpo_Sup_least)+
+lemma iterates_le_f: "x \<in> iterates f \<Longrightarrow> monotone (op \<le>) (op \<le>) f \<Longrightarrow> x \<le> f x"
+  by (induct x rule: iterates.induct)
+    (force dest: monotoneD intro!: ccpo_Sup_upper ccpo_Sup_least)+
 
 lemma chain_iterates:
   assumes f: "monotone (op \<le>) (op \<le>) f"
   shows "chain (op \<le>) (iterates f)" (is "chain _ ?C")
 proof (rule chainI)
-  fix x y assume "x \<in> ?C" "y \<in> ?C"
+  fix x y
+  assume "x \<in> ?C" "y \<in> ?C"
   then show "x \<le> y \<or> y \<le> x"
   proof (induct x arbitrary: y rule: iterates.induct)
-    fix x y assume y: "y \<in> ?C"
-    and IH: "\<And>z. z \<in> ?C \<Longrightarrow> x \<le> z \<or> z \<le> x"
+    fix x y
+    assume y: "y \<in> ?C"
+      and IH: "\<And>z. z \<in> ?C \<Longrightarrow> x \<le> z \<or> z \<le> x"
     from y show "f x \<le> y \<or> y \<le> f x"
     proof (induct y rule: iterates.induct)
-      case (step y) with IH f show ?case by (auto dest: monotoneD)
+      case (step y)
+      with IH f show ?case by (auto dest: monotoneD)
     next
       case (Sup M)
       then have chM: "chain (op \<le>) M"
         and IH': "\<And>z. z \<in> M \<Longrightarrow> f x \<le> z \<or> z \<le> f x" by auto
       show "f x \<le> Sup M \<or> Sup M \<le> f x"
       proof (cases "\<exists>z\<in>M. f x \<le> z")
-        case True then have "f x \<le> Sup M"
+        case True
+        then have "f x \<le> Sup M"
           apply rule
           apply (erule order_trans)
-          by (rule ccpo_Sup_upper[OF chM])
-        thus ?thesis ..
+          apply (rule ccpo_Sup_upper[OF chM])
+          apply assumption
+          done
+        then show ?thesis ..
       next
-        case False with IH'
-        show ?thesis by (auto intro: ccpo_Sup_least[OF chM])
+        case False
+        with IH' show ?thesis
+          by (auto intro: ccpo_Sup_least[OF chM])
       qed
     qed
   next
     case (Sup M y)
     show ?case
     proof (cases "\<exists>x\<in>M. y \<le> x")
-      case True then have "y \<le> Sup M"
+      case True
+      then have "y \<le> Sup M"
         apply rule
         apply (erule order_trans)
-        by (rule ccpo_Sup_upper[OF Sup(1)])
-      thus ?thesis ..
+        apply (rule ccpo_Sup_upper[OF Sup(1)])
+        apply assumption
+        done
+      then show ?thesis ..
     next
       case False with Sup
       show ?thesis by (auto intro: ccpo_Sup_least)
@@ -147,19 +155,19 @@
 qed
 
 lemma bot_in_iterates: "Sup {} \<in> iterates f"
-by(auto intro: iterates.Sup simp add: chain_empty)
+  by (auto intro: iterates.Sup simp add: chain_empty)
+
 
 subsection \<open>Fixpoint combinator\<close>
 
-definition
-  fixp :: "('a \<Rightarrow> 'a) \<Rightarrow> 'a"
-where
-  "fixp f = Sup (iterates f)"
+definition fixp :: "('a \<Rightarrow> 'a) \<Rightarrow> 'a"
+  where "fixp f = Sup (iterates f)"
 
 lemma iterates_fixp:
-  assumes f: "monotone (op \<le>) (op \<le>) f" shows "fixp f \<in> iterates f"
-unfolding fixp_def
-by (simp add: iterates.Sup chain_iterates f)
+  assumes f: "monotone (op \<le>) (op \<le>) f"
+  shows "fixp f \<in> iterates f"
+  unfolding fixp_def
+  by (simp add: iterates.Sup chain_iterates f)
 
 lemma fixp_unfold:
   assumes f: "monotone (op \<le>) (op \<le>) f"
@@ -169,35 +177,45 @@
     by (intro iterates_le_f iterates_fixp f)
   have "f (fixp f) \<le> Sup (iterates f)"
     by (intro ccpo_Sup_upper chain_iterates f iterates.step iterates_fixp)
-  thus "f (fixp f) \<le> fixp f"
-    unfolding fixp_def .
+  then show "f (fixp f) \<le> fixp f"
+    by (simp only: fixp_def)
 qed
 
 lemma fixp_lowerbound:
-  assumes f: "monotone (op \<le>) (op \<le>) f" and z: "f z \<le> z" shows "fixp f \<le> z"
-unfolding fixp_def
+  assumes f: "monotone (op \<le>) (op \<le>) f"
+    and z: "f z \<le> z"
+  shows "fixp f \<le> z"
+  unfolding fixp_def
 proof (rule ccpo_Sup_least[OF chain_iterates[OF f]])
-  fix x assume "x \<in> iterates f"
-  thus "x \<le> z"
+  fix x
+  assume "x \<in> iterates f"
+  then show "x \<le> z"
   proof (induct x rule: iterates.induct)
-    fix x assume "x \<le> z" with f have "f x \<le> f z" by (rule monotoneD)
-    also note z finally show "f x \<le> z" .
-  qed (auto intro: ccpo_Sup_least)
+    case (step x)
+    from f \<open>x \<le> z\<close> have "f x \<le> f z" by (rule monotoneD)
+    also note z
+    finally show "f x \<le> z" .
+  next
+    case (Sup M)
+    then show ?case
+      by (auto intro: ccpo_Sup_least)
+  qed
 qed
 
 end
 
+
 subsection \<open>Fixpoint induction\<close>
 
 setup \<open>Sign.map_naming (Name_Space.mandatory_path "ccpo")\<close>
 
 definition admissible :: "('a set \<Rightarrow> 'a) \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool"
-where "admissible lub ord P = (\<forall>A. chain ord A \<longrightarrow> (A \<noteq> {}) \<longrightarrow> (\<forall>x\<in>A. P x) \<longrightarrow> P (lub A))"
+  where "admissible lub ord P \<longleftrightarrow> (\<forall>A. chain ord A \<longrightarrow> A \<noteq> {} \<longrightarrow> (\<forall>x\<in>A. P x) \<longrightarrow> P (lub A))"
 
 lemma admissibleI:
   assumes "\<And>A. chain ord A \<Longrightarrow> A \<noteq> {} \<Longrightarrow> \<forall>x\<in>A. P x \<Longrightarrow> P (lub A)"
   shows "ccpo.admissible lub ord P"
-using assms unfolding ccpo.admissible_def by fast
+  using assms unfolding ccpo.admissible_def by fast
 
 lemma admissibleD:
   assumes "ccpo.admissible lub ord P"
@@ -205,7 +223,7 @@
   assumes "A \<noteq> {}"
   assumes "\<And>x. x \<in> A \<Longrightarrow> P x"
   shows "P (lub A)"
-using assms by (auto simp: ccpo.admissible_def)
+  using assms by (auto simp: ccpo.admissible_def)
 
 setup \<open>Sign.map_naming Name_Space.parent_path\<close>
 
@@ -215,44 +233,54 @@
   assumes bot: "P (Sup {})"
   assumes step: "\<And>x. P x \<Longrightarrow> P (f x)"
   shows "P (fixp f)"
-unfolding fixp_def using adm chain_iterates[OF mono]
+  unfolding fixp_def
+  using adm chain_iterates[OF mono]
 proof (rule ccpo.admissibleD)
-  show "iterates f \<noteq> {}" using bot_in_iterates by auto
-  fix x assume "x \<in> iterates f"
-  thus "P x"
-    by (induct rule: iterates.induct)
-      (case_tac "M = {}", auto intro: step bot ccpo.admissibleD adm)
+  show "iterates f \<noteq> {}"
+    using bot_in_iterates by auto
+next
+  fix x
+  assume "x \<in> iterates f"
+  then show "P x"
+  proof (induct rule: iterates.induct)
+    case prems: (step x)
+    from this(2) show ?case by (rule step)
+  next
+    case (Sup M)
+    then show ?case by (cases "M = {}") (auto intro: step bot ccpo.admissibleD adm)
+  qed
 qed
 
 lemma admissible_True: "ccpo.admissible lub ord (\<lambda>x. True)"
-unfolding ccpo.admissible_def by simp
+  unfolding ccpo.admissible_def by simp
 
 (*lemma admissible_False: "\<not> ccpo.admissible lub ord (\<lambda>x. False)"
 unfolding ccpo.admissible_def chain_def by simp
 *)
 lemma admissible_const: "ccpo.admissible lub ord (\<lambda>x. t)"
-by(auto intro: ccpo.admissibleI)
+  by (auto intro: ccpo.admissibleI)
 
 lemma admissible_conj:
   assumes "ccpo.admissible lub ord (\<lambda>x. P x)"
   assumes "ccpo.admissible lub ord (\<lambda>x. Q x)"
   shows "ccpo.admissible lub ord (\<lambda>x. P x \<and> Q x)"
-using assms unfolding ccpo.admissible_def by simp
+  using assms unfolding ccpo.admissible_def by simp
 
 lemma admissible_all:
   assumes "\<And>y. ccpo.admissible lub ord (\<lambda>x. P x y)"
   shows "ccpo.admissible lub ord (\<lambda>x. \<forall>y. P x y)"
-using assms unfolding ccpo.admissible_def by fast
+  using assms unfolding ccpo.admissible_def by fast
 
 lemma admissible_ball:
   assumes "\<And>y. y \<in> A \<Longrightarrow> ccpo.admissible lub ord (\<lambda>x. P x y)"
   shows "ccpo.admissible lub ord (\<lambda>x. \<forall>y\<in>A. P x y)"
-using assms unfolding ccpo.admissible_def by fast
+  using assms unfolding ccpo.admissible_def by fast
 
 lemma chain_compr: "chain ord A \<Longrightarrow> chain ord {x \<in> A. P x}"
-unfolding chain_def by fast
+  unfolding chain_def by fast
 
-context ccpo begin
+context ccpo
+begin
 
 lemma admissible_disj_lemma:
   assumes A: "chain (op \<le>)A"
@@ -280,17 +308,24 @@
   assumes Q: "ccpo.admissible Sup (op \<le>) (\<lambda>x. Q x)"
   shows "ccpo.admissible Sup (op \<le>) (\<lambda>x. P x \<or> Q x)"
 proof (rule ccpo.admissibleI)
-  fix A :: "'a set" assume A: "chain (op \<le>) A"
-  assume "A \<noteq> {}"
-    and "\<forall>x\<in>A. P x \<or> Q x"
-  hence "(\<exists>x\<in>A. P x) \<and> (\<forall>x\<in>A. \<exists>y\<in>A. x \<le> y \<and> P y) \<or> (\<exists>x\<in>A. Q x) \<and> (\<forall>x\<in>A. \<exists>y\<in>A. x \<le> y \<and> Q y)"
-    using chainD[OF A] by blast
-  hence "(\<exists>x. x \<in> A \<and> P x) \<and> Sup A = Sup {x \<in> A. P x} \<or> (\<exists>x. x \<in> A \<and> Q x) \<and> Sup A = Sup {x \<in> A. Q x}"
+  fix A :: "'a set"
+  assume A: "chain (op \<le>) A"
+  assume "A \<noteq> {}" and "\<forall>x\<in>A. P x \<or> Q x"
+  then have "(\<exists>x\<in>A. P x) \<and> (\<forall>x\<in>A. \<exists>y\<in>A. x \<le> y \<and> P y) \<or> (\<exists>x\<in>A. Q x) \<and> (\<forall>x\<in>A. \<exists>y\<in>A. x \<le> y \<and> Q y)"
+    using chainD[OF A] by blast  (* slow *)
+  then have "(\<exists>x. x \<in> A \<and> P x) \<and> Sup A = Sup {x \<in> A. P x} \<or> (\<exists>x. x \<in> A \<and> Q x) \<and> Sup A = Sup {x \<in> A. Q x}"
     using admissible_disj_lemma [OF A] by blast
-  thus "P (Sup A) \<or> Q (Sup A)"
-    apply (rule disjE, simp_all)
-    apply (rule disjI1, rule ccpo.admissibleD [OF P chain_compr [OF A]], simp, simp)
-    apply (rule disjI2, rule ccpo.admissibleD [OF Q chain_compr [OF A]], simp, simp)
+  then show "P (Sup A) \<or> Q (Sup A)"
+    apply (rule disjE)
+     apply simp_all
+     apply (rule disjI1)
+     apply (rule ccpo.admissibleD [OF P chain_compr [OF A]])
+      apply simp
+     apply simp
+    apply (rule disjI2)
+    apply (rule ccpo.admissibleD [OF Q chain_compr [OF A]])
+     apply simp
+    apply simp
     done
 qed
 
@@ -300,7 +335,8 @@
   by standard (fast intro: Sup_upper Sup_least)+
 
 lemma lfp_eq_fixp:
-  assumes f: "mono f" shows "lfp f = fixp f"
+  assumes f: "mono f"
+  shows "lfp f = fixp f"
 proof (rule antisym)
   from f have f': "monotone (op \<le>) (op \<le>) f"
     unfolding mono_def monotone_def .
diff -r fb63942e470e -r 7195acc2fe93 src/HOL/Finite_Set.thy
--- a/src/HOL/Finite_Set.thy	Fri Aug 05 16:36:03 2016 +0200
+++ b/src/HOL/Finite_Set.thy	Fri Aug 05 18:14:28 2016 +0200
@@ -1,24 +1,26 @@
 (*  Title:      HOL/Finite_Set.thy
-    Author:     Tobias Nipkow, Lawrence C Paulson and Markus Wenzel
-                with contributions by Jeremy Avigad and Andrei Popescu
+    Author:     Tobias Nipkow
+    Author:     Lawrence C Paulson
+    Author:     Markus Wenzel
+    Author:     Jeremy Avigad
+    Author:     Andrei Popescu
 *)
 
 section \<open>Finite sets\<close>
 
 theory Finite_Set
-imports Product_Type Sum_Type Fields
+  imports Product_Type Sum_Type Fields
 begin
 
 subsection \<open>Predicate for finite sets\<close>
 
-context
-  notes [[inductive_internals]]
+context notes [[inductive_internals]]
 begin
 
 inductive finite :: "'a set \<Rightarrow> bool"
-where
-  emptyI [simp, intro!]: "finite {}"
-| insertI [simp, intro!]: "finite A \<Longrightarrow> finite (insert a A)"
+  where
+    emptyI [simp, intro!]: "finite {}"
+  | insertI [simp, intro!]: "finite A \<Longrightarrow> finite (insert a A)"
 
 end
 
@@ -145,7 +147,7 @@
   shows "\<exists>f n::nat. f ` A = {i. i < n} \<and> inj_on f A"
 proof -
   from finite_imp_nat_seg_image_inj_on [OF \<open>finite A\<close>]
-  obtain f and n::nat where bij: "bij_betw f {i. i<n} A"
+  obtain f and n :: nat where bij: "bij_betw f {i. i<n} A"
     by (auto simp: bij_betw_def)
   let ?f = "the_inv_into {i. i<n} f"
   have "inj_on ?f A \<and> ?f ` A = {i. i<n}"
@@ -317,7 +319,7 @@
 next
   case insert
   then show ?case
-    by (clarsimp simp del: image_insert simp add: image_insert [symmetric]) blast
+    by (clarsimp simp del: image_insert simp add: image_insert [symmetric]) blast  (* slow *)
 qed
 
 lemma finite_vimage_IntI: "finite F \<Longrightarrow> inj_on h A \<Longrightarrow> finite (h -` F \<inter> A)"
@@ -328,7 +330,8 @@
   done
 
 lemma finite_finite_vimage_IntI:
-  assumes "finite F" and "\<And>y. y \<in> F \<Longrightarrow> finite ((h -` {y}) \<inter> A)"
+  assumes "finite F"
+    and "\<And>y. y \<in> F \<Longrightarrow> finite ((h -` {y}) \<inter> A)"
   shows "finite (h -` F \<inter> A)"
 proof -
   have *: "h -` F \<inter> A = (\<Union> y\<in>F. (h -` {y}) \<inter> A)"
@@ -464,7 +467,7 @@
 proof
   assume "finite (Pow A)"
   then have "finite ((\<lambda>x. {x}) ` A)"
-    by (blast intro: finite_subset)
+    by (blast intro: finite_subset)  (* somewhat slow *)
   then show "finite A"
     by (rule finite_imageD [unfolded inj_on_def]) simp
 next
@@ -492,7 +495,7 @@
   from finite_subset[OF this] assms have 1: "finite (?F ` ?S)"
     by simp
   have 2: "inj_on ?F ?S"
-    by (fastforce simp add: inj_on_def set_eq_iff fun_eq_iff)
+    by (fastforce simp add: inj_on_def set_eq_iff fun_eq_iff)  (* somewhat slow *)
   show ?thesis
     by (rule finite_imageD [OF 1 2])
 qed
@@ -524,7 +527,7 @@
 
 lemma finite_subset_induct [consumes 2, case_names empty insert]:
   assumes "finite F" and "F \<subseteq> A"
-  assumes empty: "P {}"
+    and empty: "P {}"
     and insert: "\<And>a F. finite F \<Longrightarrow> a \<in> A \<Longrightarrow> a \<notin> F \<Longrightarrow> P F \<Longrightarrow> P (insert a F)"
   shows "P F"
   using \<open>finite F\<close> \<open>F \<subseteq> A\<close>
@@ -545,7 +548,7 @@
 
 lemma finite_empty_induct:
   assumes "finite A"
-  assumes "P A"
+    and "P A"
     and remove: "\<And>a A. finite A \<Longrightarrow> a \<in> A \<Longrightarrow> P A \<Longrightarrow> P (A - {a})"
   shows "P {}"
 proof -
@@ -604,8 +607,8 @@
 
 lemma finite_subset_induct' [consumes 2, case_names empty insert]:
   assumes "finite F" and "F \<subseteq> A"
-  and empty: "P {}"
-  and insert: "\<And>a F. \<lbrakk>finite F; a \<in> A; F \<subseteq> A; a \<notin> F; P F \<rbrakk> \<Longrightarrow> P (insert a F)"
+    and empty: "P {}"
+    and insert: "\<And>a F. \<lbrakk>finite F; a \<in> A; F \<subseteq> A; a \<notin> F; P F \<rbrakk> \<Longrightarrow> P (insert a F)"
   shows "P F"
 proof -
   from \<open>finite F\<close>
@@ -632,7 +635,8 @@
 
 subsection \<open>Class \<open>finite\<close>\<close>
 
-class finite = assumes finite_UNIV: "finite (UNIV :: 'a set)"
+class finite =
+  assumes finite_UNIV: "finite (UNIV :: 'a set)"
 begin
 
 lemma finite [simp]: "finite (A :: 'a set)"
@@ -700,9 +704,9 @@
 
 inductive fold_graph :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'b \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> bool"
   for f :: "'a \<Rightarrow> 'b \<Rightarrow> 'b" and z :: 'b
-where
-  emptyI [intro]: "fold_graph f z {} z"
-| insertI [intro]: "x \<notin> A \<Longrightarrow> fold_graph f z A y \<Longrightarrow> fold_graph f z (insert x A) (f x y)"
+  where
+    emptyI [intro]: "fold_graph f z {} z"
+  | insertI [intro]: "x \<notin> A \<Longrightarrow> fold_graph f z A y \<Longrightarrow> fold_graph f z (insert x A) (f x y)"
 
 inductive_cases empty_fold_graphE [elim!]: "fold_graph f z {} x"
 
@@ -1069,7 +1073,7 @@
   interpret comp_fun_idem Set.remove
     by (fact comp_fun_idem_remove)
   from \<open>finite A\<close> have "fold Set.remove B A = B - A"
-    by (induct A arbitrary: B) auto
+    by (induct A arbitrary: B) auto  (* slow *)
   then show ?thesis ..
 qed
 
@@ -1124,7 +1128,7 @@
 qed
 
 lemma comp_fun_commute_Pow_fold: "comp_fun_commute (\<lambda>x A. A \<union> Set.insert x ` A)"
-  by (clarsimp simp: fun_eq_iff comp_fun_commute_def) blast
+  by (clarsimp simp: fun_eq_iff comp_fun_commute_def) blast  (* somewhat slow *)
 
 lemma Pow_fold:
   assumes "finite A"
@@ -1222,13 +1226,12 @@
 subsubsection \<open>The natural case\<close>
 
 locale folding =
-  fixes f :: "'a \<Rightarrow> 'b \<Rightarrow> 'b"
-  fixes z :: "'b"
+  fixes f :: "'a \<Rightarrow> 'b \<Rightarrow> 'b" and z :: "'b"
   assumes comp_fun_commute: "f y \<circ> f x = f x \<circ> f y"
 begin
 
 interpretation fold?: comp_fun_commute f
-  by standard (insert comp_fun_commute, simp add: fun_eq_iff)
+  by standard (use comp_fun_commute in \<open>simp add: fun_eq_iff\<close>)
 
 definition F :: "'a set \<Rightarrow> 'b"
   where eq_fold: "F A = fold f z A"
@@ -1332,14 +1335,14 @@
 
 lemma card_Suc_Diff1: "finite A \<Longrightarrow> x \<in> A \<Longrightarrow> Suc (card (A - {x})) = card A"
   apply (rule insert_Diff [THEN subst, where t = A])
-  apply assumption
+   apply assumption
   apply (simp del: insert_Diff_single)
   done
 
 lemma card_insert_le_m1: "n > 0 \<Longrightarrow> card y \<le> n - 1 \<Longrightarrow> card (insert x y) \<le> n"
   apply (cases "finite y")
-  apply (cases "x \<in> y")
-  apply (auto simp: insert_absorb)
+   apply (cases "x \<in> y")
+    apply (auto simp: insert_absorb)
   done
 
 lemma card_Diff_singleton: "finite A \<Longrightarrow> x \<in> A \<Longrightarrow> card (A - {x}) = card A - 1"
@@ -1397,7 +1400,7 @@
 
 lemma card_seteq: "finite B \<Longrightarrow> (\<And>A. A \<subseteq> B \<Longrightarrow> card B \<le> card A \<Longrightarrow> A = B)"
   apply (induct rule: finite_induct)
-  apply simp
+   apply simp
   apply clarify
   apply (subgoal_tac "finite A \<and> A - {x} \<subseteq> F")
    prefer 2 apply (blast intro: finite_subset, atomize)
@@ -1430,7 +1433,7 @@
 lemma card_Un_le: "card (A \<union> B) \<le> card A + card B"
   apply (cases "finite A")
    apply (cases "finite B")
-    using le_iff_add card_Un_Int apply blast
+    apply (use le_iff_add card_Un_Int in blast)
    apply simp
   apply simp
   done
@@ -1539,7 +1542,7 @@
 
 lemma insert_partition:
   "x \<notin> F \<Longrightarrow> \<forall>c1 \<in> insert x F. \<forall>c2 \<in> insert x F. c1 \<noteq> c2 \<longrightarrow> c1 \<inter> c2 = {} \<Longrightarrow> x \<inter> \<Union>F = {}"
-  by auto
+  by auto  (* somewhat slow *)
 
 lemma finite_psubset_induct [consumes 1, case_names psubset]:
   assumes finite: "finite A"
@@ -1597,13 +1600,13 @@
     and remove: "\<And>A. finite A \<Longrightarrow> A \<noteq> {} \<Longrightarrow> A \<subseteq> B \<Longrightarrow> (\<And>x. x \<in> A \<Longrightarrow> P (A - {x})) \<Longrightarrow> P A"
   shows "P B"
 proof (cases "finite B")
-  assume "\<not>finite B"
+  case False
   then show ?thesis by (rule infinite)
 next
+  case True
   define A where "A = B"
-  assume "finite B"
-  then have "finite A" "A \<subseteq> B"
-    by (simp_all add: A_def)
+  with True have "finite A" "A \<subseteq> B"
+    by simp_all
   then show "P A"
   proof (induct "card A" arbitrary: A)
     case 0
@@ -1623,9 +1626,9 @@
 
 lemma finite_remove_induct [consumes 1, case_names empty remove]:
   fixes P :: "'a set \<Rightarrow> bool"
-  assumes finite: "finite B"
-    and empty: "P {}"
-    and rm: "\<And>A. finite A \<Longrightarrow> A \<noteq> {} \<Longrightarrow> A \<subseteq> B \<Longrightarrow> (\<And>x. x \<in> A \<Longrightarrow> P (A - {x})) \<Longrightarrow> P A"
+  assumes "finite B"
+    and "P {}"
+    and "\<And>A. finite A \<Longrightarrow> A \<noteq> {} \<Longrightarrow> A \<subseteq> B \<Longrightarrow> (\<And>x. x \<in> A \<Longrightarrow> P (A - {x})) \<Longrightarrow> P A"
   defines "B' \<equiv> B"
   shows "P B'"
   by (induct B' rule: remove_induct) (simp_all add: assms)
@@ -1636,10 +1639,14 @@
   "finite C \<Longrightarrow> finite (\<Union>C) \<Longrightarrow> (\<forall>c\<in>C. card c = k) \<Longrightarrow>
     (\<forall>c1 \<in> C. \<forall>c2 \<in> C. c1 \<noteq> c2 \<longrightarrow> c1 \<inter> c2 = {}) \<Longrightarrow>
     k * card C = card (\<Union>C)"
-  apply (induct rule: finite_induct)
-  apply simp
-  apply (simp add: card_Un_disjoint insert_partition finite_subset [of _ "\<Union>(insert x F)"])
-  done
+proof (induct rule: finite_induct)
+  case empty
+  then show ?case by simp
+next
+  case (insert x F)
+  then show ?case
+    by (simp add: card_Un_disjoint insert_partition finite_subset [of _ "\<Union>(insert _ _)"])
+qed
 
 lemma card_eq_UNIV_imp_eq_UNIV:
   assumes fin: "finite (UNIV :: 'a set)"
@@ -1679,7 +1686,7 @@
     show "b \<notin> A - {b}"
       by blast
     show "card (A - {b}) = k" and "k = 0 \<longrightarrow> A - {b} = {}"
-      using assms b fin by(fastforce dest:mk_disjoint_insert)+
+      using assms b fin by (fastforce dest: mk_disjoint_insert)+
   qed
 qed
 
@@ -1688,7 +1695,7 @@
     (\<exists>b B. A = insert b B \<and> b \<notin> B \<and> card B = k \<and> (k = 0 \<longrightarrow> B = {}))"
   apply (auto elim!: card_eq_SucD)
   apply (subst card.insert)
-  apply (auto simp add: intro:ccontr)
+    apply (auto simp add: intro:ccontr)
   done
 
 lemma card_1_singletonE:
@@ -1761,7 +1768,7 @@
 qed
 
 lemma bij_betw_same_card: "bij_betw f A B \<Longrightarrow> card A = card B"
-  by(auto simp: card_image bij_betw_def)
+  by (auto simp: card_image bij_betw_def)
 
 lemma endo_inj_surj: "finite A \<Longrightarrow> f ` A \<subseteq> A \<Longrightarrow> inj_on f A \<Longrightarrow> f ` A = A"
   by (simp add: card_seteq card_image)
@@ -1852,12 +1859,12 @@
   from finite_Pow_iff[THEN iffD2, OF \<open>finite B\<close>] have "finite (?F ` A)"
     by (blast intro: rev_finite_subset)
   from pigeonhole_infinite [where f = ?F, OF assms(1) this]
-  obtain a0 where "a0 \<in> A" and 1: "\<not> finite {a\<in>A. ?F a = ?F a0}" ..
+  obtain a0 where "a0 \<in> A" and infinite: "\<not> finite {a\<in>A. ?F a = ?F a0}" ..
   obtain b0 where "b0 \<in> B" and "R a0 b0"
     using \<open>a0 \<in> A\<close> assms(3) by blast
-  have "finite {a\<in>A. ?F a = ?F a0}" if "finite{a:A. R a b0}"
+  have "finite {a\<in>A. ?F a = ?F a0}" if "finite {a\<in>A. R a b0}"
     using \<open>b0 \<in> B\<close> \<open>R a0 b0\<close> that by (blast intro: rev_finite_subset)
-  with 1 \<open>b0 : B\<close> show ?thesis
+  with infinite \<open>b0 \<in> B\<close> show ?thesis
     by blast
 qed
 
@@ -1896,7 +1903,7 @@
     then show ?case
       apply simp
       apply (subst card_Un_disjoint)
-      apply (auto simp add: disjoint_eq_subset_Compl)
+         apply (auto simp add: disjoint_eq_subset_Compl)
       done
   qed
 qed
@@ -1914,10 +1921,12 @@
     by (simp add: eq_card_imp_inj_on)
 qed
 
-lemma finite_UNIV_surj_inj: "finite(UNIV:: 'a set) \<Longrightarrow> surj f \<Longrightarrow> inj f" for f :: "'a \<Rightarrow> 'a"
+lemma finite_UNIV_surj_inj: "finite(UNIV:: 'a set) \<Longrightarrow> surj f \<Longrightarrow> inj f"
+  for f :: "'a \<Rightarrow> 'a"
   by (blast intro: finite_surj_inj subset_UNIV)
 
-lemma finite_UNIV_inj_surj: "finite(UNIV:: 'a set) \<Longrightarrow> inj f \<Longrightarrow> surj f" for f :: "'a \<Rightarrow> 'a"
+lemma finite_UNIV_inj_surj: "finite(UNIV:: 'a set) \<Longrightarrow> inj f \<Longrightarrow> surj f"
+  for f :: "'a \<Rightarrow> 'a"
   by (fastforce simp:surj_def dest!: endo_inj_surj)
 
 corollary infinite_UNIV_nat [iff]: "\<not> finite (UNIV :: nat set)"
@@ -2013,7 +2022,7 @@
       using psubset.hyps by blast
     show False
       apply (rule psubset.IH [where B = "A - {x}"])
-      using \<open>x \<in> A\<close> apply blast
+       apply (use \<open>x \<in> A\<close> in blast)
       apply (simp add: \<open>X (A - {x})\<close>)
       done
   qed
diff -r fb63942e470e -r 7195acc2fe93 src/HOL/Hilbert_Choice.thy
--- a/src/HOL/Hilbert_Choice.thy	Fri Aug 05 16:36:03 2016 +0200
+++ b/src/HOL/Hilbert_Choice.thy	Fri Aug 05 18:14:28 2016 +0200
@@ -6,23 +6,23 @@
 section \<open>Hilbert's Epsilon-Operator and the Axiom of Choice\<close>
 
 theory Hilbert_Choice
-imports Wellfounded
-keywords "specification" :: thy_goal
+  imports Wellfounded
+  keywords "specification" :: thy_goal
 begin
 
 subsection \<open>Hilbert's epsilon\<close>
 
-axiomatization Eps :: "('a => bool) => 'a" where
-  someI: "P x ==> P (Eps P)"
+axiomatization Eps :: "('a \<Rightarrow> bool) \<Rightarrow> 'a"
+  where someI: "P x \<Longrightarrow> P (Eps P)"
 
 syntax (epsilon)
-  "_Eps"        :: "[pttrn, bool] => 'a"    ("(3\<some>_./ _)" [0, 10] 10)
+  "_Eps" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a"  ("(3\<some>_./ _)" [0, 10] 10)
 syntax (input)
-  "_Eps"        :: "[pttrn, bool] => 'a"    ("(3@ _./ _)" [0, 10] 10)
+  "_Eps" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a"  ("(3@ _./ _)" [0, 10] 10)
 syntax
-  "_Eps"        :: "[pttrn, bool] => 'a"    ("(3SOME _./ _)" [0, 10] 10)
+  "_Eps" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a"  ("(3SOME _./ _)" [0, 10] 10)
 translations
-  "SOME x. P" == "CONST Eps (%x. P)"
+  "SOME x. P" \<rightleftharpoons> "CONST Eps (\<lambda>x. P)"
 
 print_translation \<open>
   [(@{const_syntax Eps}, fn _ => fn [Abs abs] =>
@@ -30,90 +30,92 @@
       in Syntax.const @{syntax_const "_Eps"} $ x $ t end)]
 \<close> \<comment> \<open>to avoid eta-contraction of body\<close>
 
-definition inv_into :: "'a set => ('a => 'b) => ('b => 'a)" where
-"inv_into A f == %x. SOME y. y : A & f y = x"
+definition inv_into :: "'a set \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> ('b \<Rightarrow> 'a)"
+  where "inv_into A f \<equiv> \<lambda>x. SOME y. y \<in> A \<and> f y = x"
 
-abbreviation inv :: "('a => 'b) => ('b => 'a)" where
-"inv == inv_into UNIV"
+abbreviation inv :: "('a \<Rightarrow> 'b) \<Rightarrow> ('b \<Rightarrow> 'a)"
+  where "inv \<equiv> inv_into UNIV"
 
 
 subsection \<open>Hilbert's Epsilon-operator\<close>
 
-text\<open>Easier to apply than \<open>someI\<close> if the witness comes from an
-existential formula\<close>
-lemma someI_ex [elim?]: "\<exists>x. P x ==> P (SOME x. P x)"
-apply (erule exE)
-apply (erule someI)
-done
+text \<open>
+  Easier to apply than \<open>someI\<close> if the witness comes from an
+  existential formula.
+\<close>
+lemma someI_ex [elim?]: "\<exists>x. P x \<Longrightarrow> P (SOME x. P x)"
+  apply (erule exE)
+  apply (erule someI)
+  done
 
-text\<open>Easier to apply than \<open>someI\<close> because the conclusion has only one
-occurrence of @{term P}.\<close>
-lemma someI2: "[| P a;  !!x. P x ==> Q x |] ==> Q (SOME x. P x)"
+text \<open>
+  Easier to apply than \<open>someI\<close> because the conclusion has only one
+  occurrence of @{term P}.
+\<close>
+lemma someI2: "P a \<Longrightarrow> (\<And>x. P x \<Longrightarrow> Q x) \<Longrightarrow> Q (SOME x. P x)"
   by (blast intro: someI)
 
-text\<open>Easier to apply than \<open>someI2\<close> if the witness comes from an
-existential formula\<close>
-
-lemma someI2_ex: "[| \<exists>a. P a; !!x. P x ==> Q x |] ==> Q (SOME x. P x)"
-  by (blast intro: someI2)
-
-lemma someI2_bex: "[| \<exists>a\<in>A. P a; !!x. x \<in> A \<and> P x ==> Q x |] ==> Q (SOME x. x \<in> A \<and> P x)"
+text \<open>
+  Easier to apply than \<open>someI2\<close> if the witness comes from an
+  existential formula.
+\<close>
+lemma someI2_ex: "\<exists>a. P a \<Longrightarrow> (\<And>x. P x \<Longrightarrow> Q x) \<Longrightarrow> Q (SOME x. P x)"
   by (blast intro: someI2)
 
-lemma some_equality [intro]:
-     "[| P a;  !!x. P x ==> x=a |] ==> (SOME x. P x) = a"
-by (blast intro: someI2)
+lemma someI2_bex: "\<exists>a\<in>A. P a \<Longrightarrow> (\<And>x. x \<in> A \<and> P x \<Longrightarrow> Q x) \<Longrightarrow> Q (SOME x. x \<in> A \<and> P x)"
+  by (blast intro: someI2)
+
+lemma some_equality [intro]: "P a \<Longrightarrow> (\<And>x. P x \<Longrightarrow> x = a) \<Longrightarrow> (SOME x. P x) = a"
+  by (blast intro: someI2)
 
-lemma some1_equality: "[| EX!x. P x; P a |] ==> (SOME x. P x) = a"
-by blast
+lemma some1_equality: "EX!x. P x \<Longrightarrow> P a \<Longrightarrow> (SOME x. P x) = a"
+  by blast
 
-lemma some_eq_ex: "P (SOME x. P x) =  (\<exists>x. P x)"
-by (blast intro: someI)
+lemma some_eq_ex: "P (SOME x. P x) \<longleftrightarrow> (\<exists>x. P x)"
+  by (blast intro: someI)
 
 lemma some_in_eq: "(SOME x. x \<in> A) \<in> A \<longleftrightarrow> A \<noteq> {}"
   unfolding ex_in_conv[symmetric] by (rule some_eq_ex)
 
-lemma some_eq_trivial [simp]: "(SOME y. y=x) = x"
-apply (rule some_equality)
-apply (rule refl, assumption)
-done
+lemma some_eq_trivial [simp]: "(SOME y. y = x) = x"
+  by (rule some_equality) (rule refl)
 
-lemma some_sym_eq_trivial [simp]: "(SOME y. x=y) = x"
-apply (rule some_equality)
-apply (rule refl)
-apply (erule sym)
-done
+lemma some_sym_eq_trivial [simp]: "(SOME y. x = y) = x"
+  apply (rule some_equality)
+   apply (rule refl)
+  apply (erule sym)
+  done
 
 
-subsection\<open>Axiom of Choice, Proved Using the Description Operator\<close>
+subsection \<open>Axiom of Choice, Proved Using the Description Operator\<close>
 
-lemma choice: "\<forall>x. \<exists>y. Q x y ==> \<exists>f. \<forall>x. Q x (f x)"
-by (fast elim: someI)
+lemma choice: "\<forall>x. \<exists>y. Q x y \<Longrightarrow> \<exists>f. \<forall>x. Q x (f x)"
+  by (fast elim: someI)
 
-lemma bchoice: "\<forall>x\<in>S. \<exists>y. Q x y ==> \<exists>f. \<forall>x\<in>S. Q x (f x)"
-by (fast elim: someI)
+lemma bchoice: "\<forall>x\<in>S. \<exists>y. Q x y \<Longrightarrow> \<exists>f. \<forall>x\<in>S. Q x (f x)"
+  by (fast elim: someI)
 
 lemma choice_iff: "(\<forall>x. \<exists>y. Q x y) \<longleftrightarrow> (\<exists>f. \<forall>x. Q x (f x))"
-by (fast elim: someI)
+  by (fast elim: someI)
 
 lemma choice_iff': "(\<forall>x. P x \<longrightarrow> (\<exists>y. Q x y)) \<longleftrightarrow> (\<exists>f. \<forall>x. P x \<longrightarrow> Q x (f x))"
-by (fast elim: someI)
+  by (fast elim: someI)
 
 lemma bchoice_iff: "(\<forall>x\<in>S. \<exists>y. Q x y) \<longleftrightarrow> (\<exists>f. \<forall>x\<in>S. Q x (f x))"
-by (fast elim: someI)
+  by (fast elim: someI)
 
 lemma bchoice_iff': "(\<forall>x\<in>S. P x \<longrightarrow> (\<exists>y. Q x y)) \<longleftrightarrow> (\<exists>f. \<forall>x\<in>S. P x \<longrightarrow> Q x (f x))"
-by (fast elim: someI)
+  by (fast elim: someI)
 
 lemma dependent_nat_choice:
-  assumes  1: "\<exists>x. P 0 x" and
-           2: "\<And>x n. P n x \<Longrightarrow> \<exists>y. P (Suc n) y \<and> Q n x y"
+  assumes 1: "\<exists>x. P 0 x"
+    and 2: "\<And>x n. P n x \<Longrightarrow> \<exists>y. P (Suc n) y \<and> Q n x y"
   shows "\<exists>f. \<forall>n. P n (f n) \<and> Q n (f n) (f (Suc n))"
 proof (intro exI allI conjI)
   fix n
   define f where "f = rec_nat (SOME x. P 0 x) (\<lambda>n x. SOME y. P (Suc n) y \<and> Q n x y)"
-  have "P 0 (f 0)" "\<And>n. P n (f n) \<Longrightarrow> P (Suc n) (f (Suc n)) \<and> Q n (f n) (f (Suc n))"
-    using someI_ex[OF 1] someI_ex[OF 2] by (simp_all add: f_def)
+  then have "P 0 (f 0)" "\<And>n. P n (f n) \<Longrightarrow> P (Suc n) (f (Suc n)) \<and> Q n (f n) (f (Suc n))"
+    using someI_ex[OF 1] someI_ex[OF 2] by simp_all
   then show "P n (f n)" "Q n (f n) (f (Suc n))"
     by (induct n) auto
 qed
@@ -121,181 +123,172 @@
 
 subsection \<open>Function Inverse\<close>
 
-lemma inv_def: "inv f = (%y. SOME x. f x = y)"
-by(simp add: inv_into_def)
+lemma inv_def: "inv f = (\<lambda>y. SOME x. f x = y)"
+  by (simp add: inv_into_def)
 
-lemma inv_into_into: "x : f ` A ==> inv_into A f x : A"
-apply (simp add: inv_into_def)
-apply (fast intro: someI2)
-done
+lemma inv_into_into: "x \<in> f ` A \<Longrightarrow> inv_into A f x \<in> A"
+  by (simp add: inv_into_def) (fast intro: someI2)
 
-lemma inv_identity [simp]:
-  "inv (\<lambda>a. a) = (\<lambda>a. a)"
+lemma inv_identity [simp]: "inv (\<lambda>a. a) = (\<lambda>a. a)"
   by (simp add: inv_def)
 
-lemma inv_id [simp]:
-  "inv id = id"
+lemma inv_id [simp]: "inv id = id"
   by (simp add: id_def)
 
-lemma inv_into_f_f [simp]:
-  "[| inj_on f A;  x : A |] ==> inv_into A f (f x) = x"
-apply (simp add: inv_into_def inj_on_def)
-apply (blast intro: someI2)
-done
+lemma inv_into_f_f [simp]: "inj_on f A \<Longrightarrow> x \<in> A \<Longrightarrow> inv_into A f (f x) = x"
+  by (simp add: inv_into_def inj_on_def) (blast intro: someI2)
 
-lemma inv_f_f: "inj f ==> inv f (f x) = x"
-by simp
+lemma inv_f_f: "inj f \<Longrightarrow> inv f (f x) = x"
+  by simp
 
-lemma f_inv_into_f: "y : f`A  ==> f (inv_into A f y) = y"
-apply (simp add: inv_into_def)
-apply (fast intro: someI2)
-done
+lemma f_inv_into_f: "y : f`A \<Longrightarrow> f (inv_into A f y) = y"
+  by (simp add: inv_into_def) (fast intro: someI2)
 
-lemma inv_into_f_eq: "[| inj_on f A; x : A; f x = y |] ==> inv_into A f y = x"
-apply (erule subst)
-apply (fast intro: inv_into_f_f)
-done
+lemma inv_into_f_eq: "inj_on f A \<Longrightarrow> x \<in> A \<Longrightarrow> f x = y \<Longrightarrow> inv_into A f y = x"
+  by (erule subst) (fast intro: inv_into_f_f)
 
-lemma inv_f_eq: "[| inj f; f x = y |] ==> inv f y = x"
-by (simp add:inv_into_f_eq)
+lemma inv_f_eq: "inj f \<Longrightarrow> f x = y \<Longrightarrow> inv f y = x"
+  by (simp add:inv_into_f_eq)
 
-lemma inj_imp_inv_eq: "[| inj f; ALL x. f(g x) = x |] ==> inv f = g"
+lemma inj_imp_inv_eq: "inj f \<Longrightarrow> \<forall>x. f (g x) = x \<Longrightarrow> inv f = g"
   by (blast intro: inv_into_f_eq)
 
-text\<open>But is it useful?\<close>
+text \<open>But is it useful?\<close>
 lemma inj_transfer:
-  assumes injf: "inj f" and minor: "!!y. y \<in> range(f) ==> P(inv f y)"
+  assumes inj: "inj f"
+    and minor: "\<And>y. y \<in> range f \<Longrightarrow> P (inv f y)"
   shows "P x"
 proof -
   have "f x \<in> range f" by auto
-  hence "P(inv f (f x))" by (rule minor)
-  thus "P x" by (simp add: inv_into_f_f [OF injf])
+  then have "P(inv f (f x))" by (rule minor)
+  then show "P x" by (simp add: inv_into_f_f [OF inj])
 qed
 
-lemma inj_iff: "(inj f) = (inv f o f = id)"
-apply (simp add: o_def fun_eq_iff)
-apply (blast intro: inj_on_inverseI inv_into_f_f)
-done
+lemma inj_iff: "inj f \<longleftrightarrow> inv f \<circ> f = id"
+  by (simp add: o_def fun_eq_iff) (blast intro: inj_on_inverseI inv_into_f_f)
 
-lemma inv_o_cancel[simp]: "inj f ==> inv f o f = id"
-by (simp add: inj_iff)
+lemma inv_o_cancel[simp]: "inj f \<Longrightarrow> inv f \<circ> f = id"
+  by (simp add: inj_iff)
+
+lemma o_inv_o_cancel[simp]: "inj f \<Longrightarrow> g \<circ> inv f \<circ> f = g"
+  by (simp add: comp_assoc)
 
-lemma o_inv_o_cancel[simp]: "inj f ==> g o inv f o f = g"
-by (simp add: comp_assoc)
+lemma inv_into_image_cancel[simp]: "inj_on f A \<Longrightarrow> S \<subseteq> A \<Longrightarrow> inv_into A f ` f ` S = S"
+  by (fastforce simp: image_def)
 
-lemma inv_into_image_cancel[simp]:
-  "inj_on f A ==> S <= A ==> inv_into A f ` f ` S = S"
-by(fastforce simp: image_def)
+lemma inj_imp_surj_inv: "inj f \<Longrightarrow> surj (inv f)"
+  by (blast intro!: surjI inv_into_f_f)
 
-lemma inj_imp_surj_inv: "inj f ==> surj (inv f)"
-by (blast intro!: surjI inv_into_f_f)
-
-lemma surj_f_inv_f: "surj f ==> f(inv f y) = y"
-by (simp add: f_inv_into_f)
+lemma surj_f_inv_f: "surj f \<Longrightarrow> f (inv f y) = y"
+  by (simp add: f_inv_into_f)
 
 lemma inv_into_injective:
   assumes eq: "inv_into A f x = inv_into A f y"
-      and x: "x: f`A"
-      and y: "y: f`A"
-  shows "x=y"
+    and x: "x \<in> f`A"
+    and y: "y \<in> f`A"
+  shows "x = y"
 proof -
-  have "f (inv_into A f x) = f (inv_into A f y)" using eq by simp
-  thus ?thesis by (simp add: f_inv_into_f x y)
+  from eq have "f (inv_into A f x) = f (inv_into A f y)"
+    by simp
+  with x y show ?thesis
+    by (simp add: f_inv_into_f)
 qed
 
-lemma inj_on_inv_into: "B <= f`A ==> inj_on (inv_into A f) B"
-by (blast intro: inj_onI dest: inv_into_injective injD)
+lemma inj_on_inv_into: "B \<subseteq> f`A \<Longrightarrow> inj_on (inv_into A f) B"
+  by (blast intro: inj_onI dest: inv_into_injective injD)
 
-lemma bij_betw_inv_into: "bij_betw f A B ==> bij_betw (inv_into A f) B A"
-by (auto simp add: bij_betw_def inj_on_inv_into)
+lemma bij_betw_inv_into: "bij_betw f A B \<Longrightarrow> bij_betw (inv_into A f) B A"
+  by (auto simp add: bij_betw_def inj_on_inv_into)
 
-lemma surj_imp_inj_inv: "surj f ==> inj (inv f)"
-by (simp add: inj_on_inv_into)
+lemma surj_imp_inj_inv: "surj f \<Longrightarrow> inj (inv f)"
+  by (simp add: inj_on_inv_into)
 
-lemma surj_iff: "(surj f) = (f o inv f = id)"
-by (auto intro!: surjI simp: surj_f_inv_f fun_eq_iff[where 'b='a])
+lemma surj_iff: "surj f \<longleftrightarrow> f \<circ> inv f = id"
+  by (auto intro!: surjI simp: surj_f_inv_f fun_eq_iff[where 'b='a])
 
 lemma surj_iff_all: "surj f \<longleftrightarrow> (\<forall>x. f (inv f x) = x)"
-  unfolding surj_iff by (simp add: o_def fun_eq_iff)
+  by (simp add: o_def surj_iff fun_eq_iff)
 
-lemma surj_imp_inv_eq: "[| surj f; \<forall>x. g(f x) = x |] ==> inv f = g"
-apply (rule ext)
-apply (drule_tac x = "inv f x" in spec)
-apply (simp add: surj_f_inv_f)
-done
+lemma surj_imp_inv_eq: "surj f \<Longrightarrow> \<forall>x. g (f x) = x \<Longrightarrow> inv f = g"
+  apply (rule ext)
+  apply (drule_tac x = "inv f x" in spec)
+  apply (simp add: surj_f_inv_f)
+  done
 
-lemma bij_imp_bij_inv: "bij f ==> bij (inv f)"
-by (simp add: bij_def inj_imp_surj_inv surj_imp_inj_inv)
+lemma bij_imp_bij_inv: "bij f \<Longrightarrow> bij (inv f)"
+  by (simp add: bij_def inj_imp_surj_inv surj_imp_inj_inv)
 
-lemma inv_equality: "[| !!x. g (f x) = x;  !!y. f (g y) = y |] ==> inv f = g"
-apply (rule ext)
-apply (auto simp add: inv_into_def)
-done
+lemma inv_equality: "(\<And>x. g (f x) = x) \<Longrightarrow> (\<And>y. f (g y) = y) \<Longrightarrow> inv f = g"
+  by (rule ext) (auto simp add: inv_into_def)
+
+lemma inv_inv_eq: "bij f \<Longrightarrow> inv (inv f) = f"
+  by (rule inv_equality) (auto simp add: bij_def surj_f_inv_f)
 
-lemma inv_inv_eq: "bij f ==> inv (inv f) = f"
-apply (rule inv_equality)
-apply (auto simp add: bij_def surj_f_inv_f)
-done
-
-(** bij(inv f) implies little about f.  Consider f::bool=>bool such that
-    f(True)=f(False)=True.  Then it's consistent with axiom someI that
-    inv f could be any function at all, including the identity function.
-    If inv f=id then inv f is a bijection, but inj f, surj(f) and
-    inv(inv f)=f all fail.
-**)
+text \<open>
+  \<open>bij (inv f)\<close> implies little about \<open>f\<close>. Consider \<open>f :: bool \<Rightarrow> bool\<close> such
+  that \<open>f True = f False = True\<close>. Then it ia consistent with axiom \<open>someI\<close>
+  that \<open>inv f\<close> could be any function at all, including the identity function.
+  If \<open>inv f = id\<close> then \<open>inv f\<close> is a bijection, but \<open>inj f\<close>, \<open>surj f\<close> and \<open>inv
+  (inv f) = f\<close> all fail.
+\<close>
 
 lemma inv_into_comp:
-  "[| inj_on f (g ` A); inj_on g A; x : f ` g ` A |] ==>
-  inv_into A (f o g) x = (inv_into A g o inv_into (g ` A) f) x"
-apply (rule inv_into_f_eq)
-  apply (fast intro: comp_inj_on)
- apply (simp add: inv_into_into)
-apply (simp add: f_inv_into_f inv_into_into)
-done
+  "inj_on f (g ` A) \<Longrightarrow> inj_on g A \<Longrightarrow> x \<in> f ` g ` A \<Longrightarrow>
+    inv_into A (f \<circ> g) x = (inv_into A g \<circ> inv_into (g ` A) f) x"
+  apply (rule inv_into_f_eq)
+    apply (fast intro: comp_inj_on)
+   apply (simp add: inv_into_into)
+  apply (simp add: f_inv_into_f inv_into_into)
+  done
 
-lemma o_inv_distrib: "[| bij f; bij g |] ==> inv (f o g) = inv g o inv f"
-apply (rule inv_equality)
-apply (auto simp add: bij_def surj_f_inv_f)
-done
+lemma o_inv_distrib: "bij f \<Longrightarrow> bij g \<Longrightarrow> inv (f \<circ> g) = inv g \<circ> inv f"
+  by (rule inv_equality) (auto simp add: bij_def surj_f_inv_f)
 
-lemma image_surj_f_inv_f: "surj f ==> f ` (inv f ` A) = A"
+lemma image_surj_f_inv_f: "surj f \<Longrightarrow> f ` (inv f ` A) = A"
   by (simp add: surj_f_inv_f image_comp comp_def)
 
-lemma image_inv_f_f: "inj f ==> inv f ` (f ` A) = A"
+lemma image_inv_f_f: "inj f \<Longrightarrow> inv f ` (f ` A) = A"
   by simp
 
-lemma inv_image_comp: "inj f ==> inv f ` (f ` X) = X"
+lemma inv_image_comp: "inj f \<Longrightarrow> inv f ` (f ` X) = X"
   by (fact image_inv_f_f)
 
-lemma bij_image_Collect_eq: "bij f ==> f ` Collect P = {y. P (inv f y)}"
-apply auto
-apply (force simp add: bij_is_inj)
-apply (blast intro: bij_is_surj [THEN surj_f_inv_f, symmetric])
-done
+lemma bij_image_Collect_eq: "bij f \<Longrightarrow> f ` Collect P = {y. P (inv f y)}"
+  apply auto
+   apply (force simp add: bij_is_inj)
+  apply (blast intro: bij_is_surj [THEN surj_f_inv_f, symmetric])
+  done
 
-lemma bij_vimage_eq_inv_image: "bij f ==> f -` A = inv f ` A"
-apply (auto simp add: bij_is_surj [THEN surj_f_inv_f])
-apply (blast intro: bij_is_inj [THEN inv_into_f_f, symmetric])
-done
+lemma bij_vimage_eq_inv_image: "bij f \<Longrightarrow> f -` A = inv f ` A"
+  apply (auto simp add: bij_is_surj [THEN surj_f_inv_f])
+  apply (blast intro: bij_is_inj [THEN inv_into_f_f, symmetric])
+  done
 
 lemma finite_fun_UNIVD1:
   assumes fin: "finite (UNIV :: ('a \<Rightarrow> 'b) set)"
-  and card: "card (UNIV :: 'b set) \<noteq> Suc 0"
+    and card: "card (UNIV :: 'b set) \<noteq> Suc 0"
   shows "finite (UNIV :: 'a set)"
 proof -
-  from fin have finb: "finite (UNIV :: 'b set)" by (rule finite_fun_UNIVD2)
+  from fin have finb: "finite (UNIV :: 'b set)"
+    by (rule finite_fun_UNIVD2)
   with card have "card (UNIV :: 'b set) \<ge> Suc (Suc 0)"
     by (cases "card (UNIV :: 'b set)") (auto simp add: card_eq_0_iff)
-  then obtain n where "card (UNIV :: 'b set) = Suc (Suc n)" "n = card (UNIV :: 'b set) - Suc (Suc 0)" by auto
-  then obtain b1 b2 where b1b2: "(b1 :: 'b) \<noteq> (b2 :: 'b)" by (auto simp add: card_Suc_eq)
-  from fin have "finite (range (\<lambda>f :: 'a \<Rightarrow> 'b. inv f b1))" by (rule finite_imageI)
+  then obtain n where "card (UNIV :: 'b set) = Suc (Suc n)" "n = card (UNIV :: 'b set) - Suc (Suc 0)"
+    by auto
+  then obtain b1 b2 where b1b2: "(b1 :: 'b) \<noteq> (b2 :: 'b)"
+    by (auto simp add: card_Suc_eq)
+  from fin have "finite (range (\<lambda>f :: 'a \<Rightarrow> 'b. inv f b1))"
+    by (rule finite_imageI)
   moreover have "UNIV = range (\<lambda>f :: 'a \<Rightarrow> 'b. inv f b1)"
   proof (rule UNIV_eq_I)
     fix x :: 'a
-    from b1b2 have "x = inv (\<lambda>y. if y = x then b1 else b2) b1" by (simp add: inv_into_def)
-    thus "x \<in> range (\<lambda>f::'a \<Rightarrow> 'b. inv f b1)" by blast
+    from b1b2 have "x = inv (\<lambda>y. if y = x then b1 else b2) b1"
+      by (simp add: inv_into_def)
+    then show "x \<in> range (\<lambda>f::'a \<Rightarrow> 'b. inv f b1)"
+      by blast
   qed
-  ultimately show "finite (UNIV :: 'a set)" by simp
+  ultimately show "finite (UNIV :: 'a set)"
+    by simp
 qed
 
 text \<open>
@@ -318,18 +311,18 @@
   define Sseq where "Sseq = rec_nat S (\<lambda>n T. T - {SOME e. e \<in> T})"
   define pick where "pick n = (SOME e. e \<in> Sseq n)" for n
   have *: "Sseq n \<subseteq> S" "\<not> finite (Sseq n)" for n
-    by (induct n) (auto simp add: Sseq_def inf)
+    by (induct n) (auto simp: Sseq_def inf)
   then have **: "\<And>n. pick n \<in> Sseq n"
     unfolding pick_def by (subst (asm) finite.simps) (auto simp add: ex_in_conv intro: someI_ex)
   with * have "range pick \<subseteq> S" by auto
-  moreover
-  {
-    fix n m
+  moreover have "pick n \<noteq> pick (n + Suc m)" for m n
+  proof -
     have "pick n \<notin> Sseq (n + Suc m)"
       by (induct m) (auto simp add: Sseq_def pick_def)
-    with ** have "pick n \<noteq> pick (n + Suc m)" by auto
-  }
-  then have "inj pick" by (intro linorder_injI) (auto simp add: less_iff_Suc_add)
+    with ** show ?thesis by auto
+  qed
+  then have "inj pick"
+    by (intro linorder_injI) (auto simp add: less_iff_Suc_add)
   ultimately show ?thesis by blast
 qed
 
@@ -338,31 +331,35 @@
   using finite_imageD finite_subset infinite_UNIV_char_0 infinite_countable_subset by auto
 
 lemma image_inv_into_cancel:
-  assumes SURJ: "f`A=A'" and SUB: "B' \<le> A'"
+  assumes surj: "f`A = A'"
+    and sub: "B' \<subseteq> A'"
   shows "f `((inv_into A f)`B') = B'"
   using assms
-proof (auto simp add: f_inv_into_f)
-  let ?f' = "(inv_into A f)"
-  fix a' assume *: "a' \<in> B'"
-  then have "a' \<in> A'" using SUB by auto
-  then have "a' = f (?f' a')"
-    using SURJ by (auto simp add: f_inv_into_f)
-  then show "a' \<in> f ` (?f' ` B')" using * by blast
+proof (auto simp: f_inv_into_f)
+  let ?f' = "inv_into A f"
+  fix a'
+  assume *: "a' \<in> B'"
+  with sub have "a' \<in> A'" by auto
+  with surj have "a' = f (?f' a')"
+    by (auto simp: f_inv_into_f)
+  with * show "a' \<in> f ` (?f' ` B')" by blast
 qed
 
 lemma inv_into_inv_into_eq:
-  assumes "bij_betw f A A'" "a \<in> A"
+  assumes "bij_betw f A A'"
+    and a: "a \<in> A"
   shows "inv_into A' (inv_into A f) a = f a"
 proof -
-  let ?f' = "inv_into A f"   let ?f'' = "inv_into A' ?f'"
-  have 1: "bij_betw ?f' A' A" using assms
-  by (auto simp add: bij_betw_inv_into)
-  obtain a' where 2: "a' \<in> A'" and 3: "?f' a' = a"
-    using 1 \<open>a \<in> A\<close> unfolding bij_betw_def by force
-  hence "?f'' a = a'"
-    using \<open>a \<in> A\<close> 1 3 by (auto simp add: f_inv_into_f bij_betw_def)
-  moreover have "f a = a'" using assms 2 3
-    by (auto simp add: bij_betw_def)
+  let ?f' = "inv_into A f"
+  let ?f'' = "inv_into A' ?f'"
+  from assms have *: "bij_betw ?f' A' A"
+    by (auto simp: bij_betw_inv_into)
+  with a obtain a' where a': "a' \<in> A'" "?f' a' = a"
+    unfolding bij_betw_def by force
+  with a * have "?f'' a = a'"
+    by (auto simp: f_inv_into_f bij_betw_def)
+  moreover from assms a' have "f a = a'"
+    by (auto simp: bij_betw_def)
   ultimately show "?f'' a = f a" by simp
 qed
 
@@ -370,72 +367,82 @@
   assumes "A \<noteq> {}"
   shows "(\<exists>f. inj_on f A \<and> f ` A \<le> A') \<longleftrightarrow> (\<exists>g. g ` A' = A)"
 proof safe
-  fix f assume INJ: "inj_on f A" and INCL: "f ` A \<le> A'"
-  let ?phi = "\<lambda>a' a. a \<in> A \<and> f a = a'"  let ?csi = "\<lambda>a. a \<in> A"
+  fix f
+  assume inj: "inj_on f A" and incl: "f ` A \<subseteq> A'"
+  let ?phi = "\<lambda>a' a. a \<in> A \<and> f a = a'"
+  let ?csi = "\<lambda>a. a \<in> A"
   let ?g = "\<lambda>a'. if a' \<in> f ` A then (SOME a. ?phi a' a) else (SOME a. ?csi a)"
   have "?g ` A' = A"
   proof
-    show "?g ` A' \<le> A"
+    show "?g ` A' \<subseteq> A"
     proof clarify
-      fix a' assume *: "a' \<in> A'"
+      fix a'
+      assume *: "a' \<in> A'"
       show "?g a' \<in> A"
-      proof cases
-        assume Case1: "a' \<in> f ` A"
+      proof (cases "a' \<in> f ` A")
+        case True
         then obtain a where "?phi a' a" by blast
-        hence "?phi a' (SOME a. ?phi a' a)" using someI[of "?phi a'" a] by blast
-        with Case1 show ?thesis by auto
+        then have "?phi a' (SOME a. ?phi a' a)"
+          using someI[of "?phi a'" a] by blast
+        with True show ?thesis by auto
       next
-        assume Case2: "a' \<notin> f ` A"
-        hence "?csi (SOME a. ?csi a)" using assms someI_ex[of ?csi] by blast
-        with Case2 show ?thesis by auto
+        case False
+        with assms have "?csi (SOME a. ?csi a)"
+          using someI_ex[of ?csi] by blast
+        with False show ?thesis by auto
       qed
     qed
   next
-    show "A \<le> ?g ` A'"
-    proof-
-      {fix a assume *: "a \<in> A"
-       let ?b = "SOME aa. ?phi (f a) aa"
-       have "?phi (f a) a" using * by auto
-       hence 1: "?phi (f a) ?b" using someI[of "?phi(f a)" a] by blast
-       hence "?g(f a) = ?b" using * by auto
-       moreover have "a = ?b" using 1 INJ * by (auto simp add: inj_on_def)
-       ultimately have "?g(f a) = a" by simp
-       with INCL * have "?g(f a) = a \<and> f a \<in> A'" by auto
-      }
-      thus ?thesis by force
+    show "A \<subseteq> ?g ` A'"
+    proof -
+      have "?g (f a) = a \<and> f a \<in> A'" if a: "a \<in> A" for a
+      proof -
+        let ?b = "SOME aa. ?phi (f a) aa"
+        from a have "?phi (f a) a" by auto
+        then have *: "?phi (f a) ?b"
+          using someI[of "?phi(f a)" a] by blast
+        then have "?g (f a) = ?b" using a by auto
+        moreover from inj * a have "a = ?b"
+          by (auto simp add: inj_on_def)
+        ultimately have "?g(f a) = a" by simp
+        with incl a show ?thesis by auto
+      qed
+      then show ?thesis by force
     qed
   qed
-  thus "\<exists>g. g ` A' = A" by blast
+  then show "\<exists>g. g ` A' = A" by blast
 next
-  fix g  let ?f = "inv_into A' g"
+  fix g
+  let ?f = "inv_into A' g"
   have "inj_on ?f (g ` A')"
-    by (auto simp add: inj_on_inv_into)
-  moreover
-  {fix a' assume *: "a' \<in> A'"
-   let ?phi = "\<lambda> b'. b' \<in> A' \<and> g b' = g a'"
-   have "?phi a'" using * by auto
-   hence "?phi(SOME b'. ?phi b')" using someI[of ?phi] by blast
-   hence "?f(g a') \<in> A'" unfolding inv_into_def by auto
-  }
-  ultimately show "\<exists>f. inj_on f (g ` A') \<and> f ` g ` A' \<subseteq> A'" by auto
+    by (auto simp: inj_on_inv_into)
+  moreover have "?f (g a') \<in> A'" if a': "a' \<in> A'" for a'
+  proof -
+    let ?phi = "\<lambda> b'. b' \<in> A' \<and> g b' = g a'"
+    from a' have "?phi a'" by auto
+    then have "?phi (SOME b'. ?phi b')"
+      using someI[of ?phi] by blast
+    then show ?thesis by (auto simp: inv_into_def)
+  qed
+  ultimately show "\<exists>f. inj_on f (g ` A') \<and> f ` g ` A' \<subseteq> A'"
+    by auto
 qed
 
 lemma Ex_inj_on_UNION_Sigma:
   "\<exists>f. (inj_on f (\<Union>i \<in> I. A i) \<and> f ` (\<Union>i \<in> I. A i) \<le> (SIGMA i : I. A i))"
 proof
-  let ?phi = "\<lambda> a i. i \<in> I \<and> a \<in> A i"
-  let ?sm = "\<lambda> a. SOME i. ?phi a i"
+  let ?phi = "\<lambda>a i. i \<in> I \<and> a \<in> A i"
+  let ?sm = "\<lambda>a. SOME i. ?phi a i"
   let ?f = "\<lambda>a. (?sm a, a)"
-  have "inj_on ?f (\<Union>i \<in> I. A i)" unfolding inj_on_def by auto
+  have "inj_on ?f (\<Union>i \<in> I. A i)"
+    by (auto simp: inj_on_def)
   moreover
-  { { fix i a assume "i \<in> I" and "a \<in> A i"
-      hence "?sm a \<in> I \<and> a \<in> A(?sm a)" using someI[of "?phi a" i] by auto
-    }
-    hence "?f ` (\<Union>i \<in> I. A i) \<le> (SIGMA i : I. A i)" by auto
-  }
-  ultimately
-  show "inj_on ?f (\<Union>i \<in> I. A i) \<and> ?f ` (\<Union>i \<in> I. A i) \<le> (SIGMA i : I. A i)"
-  by auto
+  have "?sm a \<in> I \<and> a \<in> A(?sm a)" if "i \<in> I" and "a \<in> A i" for i a
+    using that someI[of "?phi a" i] by auto
+  then have "?f ` (\<Union>i \<in> I. A i) \<le> (SIGMA i : I. A i)"
+    by auto
+  ultimately show "inj_on ?f (\<Union>i \<in> I. A i) \<and> ?f ` (\<Union>i \<in> I. A i) \<le> (SIGMA i : I. A i)"
+    by auto
 qed
 
 lemma inv_unique_comp:
@@ -448,190 +455,199 @@
 subsection \<open>The Cantor-Bernstein Theorem\<close>
 
 lemma Cantor_Bernstein_aux:
-  shows "\<exists>A' h. A' \<le> A \<and>
-                (\<forall>a \<in> A'. a \<notin> g`(B - f ` A')) \<and>
-                (\<forall>a \<in> A'. h a = f a) \<and>
-                (\<forall>a \<in> A - A'. h a \<in> B - (f ` A') \<and> a = g(h a))"
-proof-
-  obtain H where H_def: "H = (\<lambda> A'. A - (g`(B - (f ` A'))))" by blast
-  have 0: "mono H" unfolding mono_def H_def by blast
-  then obtain A' where 1: "H A' = A'" using lfp_unfold by blast
-  hence 2: "A' = A - (g`(B - (f ` A')))" unfolding H_def by simp
-  hence 3: "A' \<le> A" by blast
-  have 4: "\<forall>a \<in> A'.  a \<notin> g`(B - f ` A')"
-  using 2 by blast
-  have 5: "\<forall>a \<in> A - A'. \<exists>b \<in> B - (f ` A'). a = g b"
-  using 2 by blast
-  (*  *)
-  obtain h where h_def:
-  "h = (\<lambda> a. if a \<in> A' then f a else (SOME b. b \<in> B - (f ` A') \<and> a = g b))" by blast
-  hence "\<forall>a \<in> A'. h a = f a" by auto
-  moreover
-  have "\<forall>a \<in> A - A'. h a \<in> B - (f ` A') \<and> a = g(h a)"
+  "\<exists>A' h. A' \<subseteq> A \<and>
+    (\<forall>a \<in> A'. a \<notin> g ` (B - f ` A')) \<and>
+    (\<forall>a \<in> A'. h a = f a) \<and>
+    (\<forall>a \<in> A - A'. h a \<in> B - (f ` A') \<and> a = g (h a))"
+proof -
+  define H where "H A' = A - (g ` (B - (f ` A')))" for A'
+  have "mono H" unfolding mono_def H_def by blast
+  from lfp_unfold [OF this] obtain A' where "H A' = A'" by blast
+  then have "A' = A - (g ` (B - (f ` A')))" by (simp add: H_def)
+  then have 1: "A' \<subseteq> A"
+    and 2: "\<forall>a \<in> A'.  a \<notin> g ` (B - f ` A')"
+    and 3: "\<forall>a \<in> A - A'. \<exists>b \<in> B - (f ` A'). a = g b"
+    by blast+
+  define h where "h a = (if a \<in> A' then f a else (SOME b. b \<in> B - (f ` A') \<and> a = g b))" for a
+  then have 4: "\<forall>a \<in> A'. h a = f a" by simp
+  have "\<forall>a \<in> A - A'. h a \<in> B - (f ` A') \<and> a = g (h a)"
   proof
-    fix a assume *: "a \<in> A - A'"
-    let ?phi = "\<lambda> b. b \<in> B - (f ` A') \<and> a = g b"
-    have "h a = (SOME b. ?phi b)" using h_def * by auto
-    moreover have "\<exists>b. ?phi b" using 5 *  by auto
-    ultimately show  "?phi (h a)" using someI_ex[of ?phi] by auto
+    fix a
+    let ?phi = "\<lambda>b. b \<in> B - (f ` A') \<and> a = g b"
+    assume *: "a \<in> A - A'"
+    from * have "h a = (SOME b. ?phi b)" by (auto simp: h_def)
+    moreover from 3 * have "\<exists>b. ?phi b" by auto
+    ultimately show "?phi (h a)"
+      using someI_ex[of ?phi] by auto
   qed
-  ultimately show ?thesis using 3 4 by blast
+  with 1 2 4 show ?thesis by blast
 qed
 
 theorem Cantor_Bernstein:
-  assumes INJ1: "inj_on f A" and SUB1: "f ` A \<le> B" and
-          INJ2: "inj_on g B" and SUB2: "g ` B \<le> A"
+  assumes inj1: "inj_on f A" and sub1: "f ` A \<subseteq> B"
+    and inj2: "inj_on g B" and sub2: "g ` B \<subseteq> A"
   shows "\<exists>h. bij_betw h A B"
 proof-
-  obtain A' and h where 0: "A' \<le> A" and
-  1: "\<forall>a \<in> A'. a \<notin> g`(B - f ` A')" and
-  2: "\<forall>a \<in> A'. h a = f a" and
-  3: "\<forall>a \<in> A - A'. h a \<in> B - (f ` A') \<and> a = g(h a)"
-  using Cantor_Bernstein_aux[of A g B f] by blast
+  obtain A' and h where "A' \<subseteq> A"
+    and 1: "\<forall>a \<in> A'. a \<notin> g ` (B - f ` A')"
+    and 2: "\<forall>a \<in> A'. h a = f a"
+    and 3: "\<forall>a \<in> A - A'. h a \<in> B - (f ` A') \<and> a = g (h a)"
+    using Cantor_Bernstein_aux [of A g B f] by blast
   have "inj_on h A"
   proof (intro inj_onI)
     fix a1 a2
     assume 4: "a1 \<in> A" and 5: "a2 \<in> A" and 6: "h a1 = h a2"
     show "a1 = a2"
-    proof(cases "a1 \<in> A'")
-      assume Case1: "a1 \<in> A'"
+    proof (cases "a1 \<in> A'")
+      case True
       show ?thesis
-      proof(cases "a2 \<in> A'")
-        assume Case11: "a2 \<in> A'"
-        hence "f a1 = f a2" using Case1 2 6 by auto
-        thus ?thesis using INJ1 Case1 Case11 0
-        unfolding inj_on_def by blast
+      proof (cases "a2 \<in> A'")
+        case True': True
+        with True 2 6 have "f a1 = f a2" by auto
+        with inj1 \<open>A' \<subseteq> A\<close> True True' show ?thesis
+          unfolding inj_on_def by blast
       next
-        assume Case12: "a2 \<notin> A'"
-        hence False using 3 5 2 6 Case1 by force
-        thus ?thesis by simp
+        case False
+        with 2 3 5 6 True have False by force
+        then show ?thesis ..
       qed
     next
-    assume Case2: "a1 \<notin> A'"
+      case False
       show ?thesis
-      proof(cases "a2 \<in> A'")
-        assume Case21: "a2 \<in> A'"
-        hence False using 3 4 2 6 Case2 by auto
-        thus ?thesis by simp
+      proof (cases "a2 \<in> A'")
+        case True
+        with 2 3 4 6 False have False by auto
+        then show ?thesis ..
       next
-        assume Case22: "a2 \<notin> A'"
-        hence "a1 = g(h a1) \<and> a2 = g(h a2)" using Case2 4 5 3 by auto
-        thus ?thesis using 6 by simp
+        case False': False
+        with False 3 4 5 have "a1 = g (h a1)" "a2 = g (h a2)" by auto
+        with 6 show ?thesis by simp
       qed
     qed
   qed
-  (*  *)
-  moreover
-  have "h ` A = B"
+  moreover have "h ` A = B"
   proof safe
-    fix a assume "a \<in> A"
-    thus "h a \<in> B" using SUB1 2 3 by (cases "a \<in> A'") auto
+    fix a
+    assume "a \<in> A"
+    with sub1 2 3 show "h a \<in> B" by (cases "a \<in> A'") auto
   next
-    fix b assume *: "b \<in> B"
+    fix b
+    assume *: "b \<in> B"
     show "b \<in> h ` A"
-    proof(cases "b \<in> f ` A'")
-      assume Case1: "b \<in> f ` A'"
-      then obtain a where "a \<in> A' \<and> b = f a" by blast
-      thus ?thesis using 2 0 by force
+    proof (cases "b \<in> f ` A'")
+      case True
+      then obtain a where "a \<in> A'" "b = f a" by blast
+      with \<open>A' \<subseteq> A\<close> 2 show ?thesis by force
     next
-      assume Case2: "b \<notin> f ` A'"
-      hence "g b \<notin> A'" using 1 * by auto
-      hence 4: "g b \<in> A - A'" using * SUB2 by auto
-      hence "h(g b) \<in> B \<and> g(h(g b)) = g b"
-      using 3 by auto
-      hence "h(g b) = b" using * INJ2 unfolding inj_on_def by auto
-      thus ?thesis using 4 by force
+      case False
+      with 1 * have "g b \<notin> A'" by auto
+      with sub2 * have 4: "g b \<in> A - A'" by auto
+      with 3 have "h (g b) \<in> B" "g (h (g b)) = g b" by auto
+      with inj2 * have "h (g b) = b" by (auto simp: inj_on_def)
+      with 4 show ?thesis by force
     qed
   qed
-  (*  *)
-  ultimately show ?thesis unfolding bij_betw_def by auto
+  ultimately show ?thesis
+    by (auto simp: bij_betw_def)
 qed
 
+
 subsection \<open>Other Consequences of Hilbert's Epsilon\<close>
 
 text \<open>Hilbert's Epsilon and the @{term split} Operator\<close>
 
-text\<open>Looping simprule\<close>
-lemma split_paired_Eps: "(SOME x. P x) = (SOME (a,b). P(a,b))"
+text \<open>Looping simprule!\<close>
+lemma split_paired_Eps: "(SOME x. P x) = (SOME (a, b). P (a, b))"
   by simp
 
 lemma Eps_case_prod: "Eps (case_prod P) = (SOME xy. P (fst xy) (snd xy))"
   by (simp add: split_def)
 
-lemma Eps_case_prod_eq [simp]: "(@(x',y'). x = x' & y = y') = (x,y)"
+lemma Eps_case_prod_eq [simp]: "(SOME (x', y'). x = x' \<and> y = y') = (x, y)"
   by blast
 
 
-text\<open>A relation is wellfounded iff it has no infinite descending chain\<close>
-lemma wf_iff_no_infinite_down_chain:
-  "wf r = (~(\<exists>f. \<forall>i. (f(Suc i),f i) \<in> r))"
-apply (simp only: wf_eq_minimal)
-apply (rule iffI)
- apply (rule notI)
- apply (erule exE)
- apply (erule_tac x = "{w. \<exists>i. w=f i}" in allE, blast)
-apply (erule contrapos_np, simp, clarify)
-apply (subgoal_tac "\<forall>n. rec_nat x (%i y. @z. z:Q & (z,y) :r) n \<in> Q")
- apply (rule_tac x = "rec_nat x (%i y. @z. z:Q & (z,y) :r)" in exI)
- apply (rule allI, simp)
- apply (rule someI2_ex, blast, blast)
-apply (rule allI)
-apply (induct_tac "n", simp_all)
-apply (rule someI2_ex, blast+)
-done
+text \<open>A relation is wellfounded iff it has no infinite descending chain.\<close>
+lemma wf_iff_no_infinite_down_chain: "wf r \<longleftrightarrow> (\<not> (\<exists>f. \<forall>i. (f (Suc i), f i) \<in> r))"
+  apply (simp only: wf_eq_minimal)
+  apply (rule iffI)
+   apply (rule notI)
+   apply (erule exE)
+   apply (erule_tac x = "{w. \<exists>i. w = f i}" in allE)
+   apply blast
+  apply (erule contrapos_np)
+  apply simp
+  apply clarify
+  apply (subgoal_tac "\<forall>n. rec_nat x (\<lambda>i y. SOME z. z \<in> Q \<and> (z, y) \<in> r) n \<in> Q")
+   apply (rule_tac x = "rec_nat x (\<lambda>i y. SOME z. z \<in> Q \<and> (z, y) \<in> r)" in exI)
+   apply (rule allI)
+   apply simp
+   apply (rule someI2_ex)
+    apply blast
+   apply blast
+  apply (rule allI)
+  apply (induct_tac n)
+   apply simp_all
+  apply (rule someI2_ex)
+   apply blast
+  apply blast
+  done
 
 lemma wf_no_infinite_down_chainE:
-  assumes "wf r" obtains k where "(f (Suc k), f k) \<notin> r"
-using \<open>wf r\<close> wf_iff_no_infinite_down_chain[of r] by blast
+  assumes "wf r"
+  obtains k where "(f (Suc k), f k) \<notin> r"
+  using assms wf_iff_no_infinite_down_chain[of r] by blast
 
 
-text\<open>A dynamically-scoped fact for TFL\<close>
-lemma tfl_some: "\<forall>P x. P x --> P (Eps P)"
+text \<open>A dynamically-scoped fact for TFL\<close>
+lemma tfl_some: "\<forall>P x. P x \<longrightarrow> P (Eps P)"
   by (blast intro: someI)
 
 
 subsection \<open>Least value operator\<close>
 
-definition
-  LeastM :: "['a => 'b::ord, 'a => bool] => 'a" where
-  "LeastM m P == SOME x. P x & (\<forall>y. P y --> m x <= m y)"
+definition LeastM :: "('a \<Rightarrow> 'b::ord) \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> 'a"
+  where "LeastM m P \<equiv> (SOME x. P x \<and> (\<forall>y. P y \<longrightarrow> m x \<le> m y))"
 
 syntax
-  "_LeastM" :: "[pttrn, 'a => 'b::ord, bool] => 'a"    ("LEAST _ WRT _. _" [0, 4, 10] 10)
+  "_LeastM" :: "pttrn \<Rightarrow> ('a \<Rightarrow> 'b::ord) \<Rightarrow> bool \<Rightarrow> 'a"  ("LEAST _ WRT _. _" [0, 4, 10] 10)
 translations
-  "LEAST x WRT m. P" == "CONST LeastM m (%x. P)"
+  "LEAST x WRT m. P" \<rightleftharpoons> "CONST LeastM m (\<lambda>x. P)"
 
 lemma LeastMI2:
-  "P x ==> (!!y. P y ==> m x <= m y)
-    ==> (!!x. P x ==> \<forall>y. P y --> m x \<le> m y ==> Q x)
-    ==> Q (LeastM m P)"
+  "P x \<Longrightarrow>
+    (\<And>y. P y \<Longrightarrow> m x \<le> m y) \<Longrightarrow>
+    (\<And>x. P x \<Longrightarrow> \<forall>y. P y \<longrightarrow> m x \<le> m y \<Longrightarrow> Q x) \<Longrightarrow>
+    Q (LeastM m P)"
   apply (simp add: LeastM_def)
-  apply (rule someI2_ex, blast, blast)
+  apply (rule someI2_ex)
+   apply blast
+  apply blast
   done
 
 lemma LeastM_equality:
-  "P k ==> (!!x. P x ==> m k <= m x)
-    ==> m (LEAST x WRT m. P x) = (m k::'a::order)"
-  apply (rule LeastMI2, assumption, blast)
+  "P k \<Longrightarrow> (\<And>x. P x \<Longrightarrow> m k \<le> m x) \<Longrightarrow> m (LEAST x WRT m. P x) = (m k :: 'a::order)"
+  apply (rule LeastMI2)
+    apply assumption
+   apply blast
   apply (blast intro!: order_antisym)
   done
 
 lemma wf_linord_ex_has_least:
-  "wf r ==> \<forall>x y. ((x,y):r^+) = ((y,x)~:r^*) ==> P k
-    ==> \<exists>x. P x & (!y. P y --> (m x,m y):r^*)"
+  "wf r \<Longrightarrow> \<forall>x y. (x, y) \<in> r\<^sup>+ \<longleftrightarrow> (y, x) \<notin> r\<^sup>* \<Longrightarrow> P k \<Longrightarrow> \<exists>x. P x \<and> (\<forall>y. P y \<longrightarrow> (m x, m y) \<in> r\<^sup>*)"
   apply (drule wf_trancl [THEN wf_eq_minimal [THEN iffD1]])
-  apply (drule_tac x = "m`Collect P" in spec, force)
+  apply (drule_tac x = "m ` Collect P" in spec)
+  apply force
   done
 
-lemma ex_has_least_nat:
-    "P k ==> \<exists>x. P x & (\<forall>y. P y --> m x <= (m y::nat))"
+lemma ex_has_least_nat: "P k \<Longrightarrow> \<exists>x. P x \<and> (\<forall>y. P y \<longrightarrow> m x \<le> (m y :: nat))"
   apply (simp only: pred_nat_trancl_eq_le [symmetric])
   apply (rule wf_pred_nat [THEN wf_linord_ex_has_least])
-   apply (simp add: less_eq linorder_not_le pred_nat_trancl_eq_le, assumption)
+   apply (simp add: less_eq linorder_not_le pred_nat_trancl_eq_le)
+  apply assumption
   done
 
-lemma LeastM_nat_lemma:
-    "P k ==> P (LeastM m P) & (\<forall>y. P y --> m (LeastM m P) <= (m y::nat))"
+lemma LeastM_nat_lemma: "P k \<Longrightarrow> P (LeastM m P) \<and> (\<forall>y. P y \<longrightarrow> m (LeastM m P) \<le> (m y :: nat))"
   apply (simp add: LeastM_def)
   apply (rule someI_ex)
   apply (erule ex_has_least_nat)
@@ -639,91 +655,87 @@
 
 lemmas LeastM_natI = LeastM_nat_lemma [THEN conjunct1]
 
-lemma LeastM_nat_le: "P x ==> m (LeastM m P) <= (m x::nat)"
-by (rule LeastM_nat_lemma [THEN conjunct2, THEN spec, THEN mp], assumption, assumption)
+lemma LeastM_nat_le: "P x \<Longrightarrow> m (LeastM m P) \<le> (m x :: nat)"
+  by (rule LeastM_nat_lemma [THEN conjunct2, THEN spec, THEN mp])
 
 
 subsection \<open>Greatest value operator\<close>
 
-definition
-  GreatestM :: "['a => 'b::ord, 'a => bool] => 'a" where
-  "GreatestM m P == SOME x. P x & (\<forall>y. P y --> m y <= m x)"
+definition GreatestM :: "('a \<Rightarrow> 'b::ord) \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> 'a"
+  where "GreatestM m P \<equiv> SOME x. P x \<and> (\<forall>y. P y \<longrightarrow> m y \<le> m x)"
 
-definition
-  Greatest :: "('a::ord => bool) => 'a" (binder "GREATEST " 10) where
-  "Greatest == GreatestM (%x. x)"
+definition Greatest :: "('a::ord \<Rightarrow> bool) \<Rightarrow> 'a"  (binder "GREATEST " 10)
+  where "Greatest \<equiv> GreatestM (\<lambda>x. x)"
 
 syntax
-  "_GreatestM" :: "[pttrn, 'a => 'b::ord, bool] => 'a"
-      ("GREATEST _ WRT _. _" [0, 4, 10] 10)
+  "_GreatestM" :: "pttrn \<Rightarrow> ('a \<Rightarrow> 'b::ord) \<Rightarrow> bool \<Rightarrow> 'a"  ("GREATEST _ WRT _. _" [0, 4, 10] 10)
 translations
-  "GREATEST x WRT m. P" == "CONST GreatestM m (%x. P)"
+  "GREATEST x WRT m. P" \<rightleftharpoons> "CONST GreatestM m (\<lambda>x. P)"
 
 lemma GreatestMI2:
-  "P x ==> (!!y. P y ==> m y <= m x)
-    ==> (!!x. P x ==> \<forall>y. P y --> m y \<le> m x ==> Q x)
-    ==> Q (GreatestM m P)"
+  "P x \<Longrightarrow>
+    (\<And>y. P y \<Longrightarrow> m y \<le> m x) \<Longrightarrow>
+    (\<And>x. P x \<Longrightarrow> \<forall>y. P y \<longrightarrow> m y \<le> m x \<Longrightarrow> Q x) \<Longrightarrow>
+    Q (GreatestM m P)"
   apply (simp add: GreatestM_def)
-  apply (rule someI2_ex, blast, blast)
+  apply (rule someI2_ex)
+   apply blast
+  apply blast
   done
 
 lemma GreatestM_equality:
- "P k ==> (!!x. P x ==> m x <= m k)
-    ==> m (GREATEST x WRT m. P x) = (m k::'a::order)"
-  apply (rule_tac m = m in GreatestMI2, assumption, blast)
+  "P k \<Longrightarrow>
+    (\<And>x. P x \<Longrightarrow> m x \<le> m k) \<Longrightarrow>
+    m (GREATEST x WRT m. P x) = (m k :: 'a::order)"
+  apply (rule GreatestMI2 [where m = m])
+    apply assumption
+   apply blast
   apply (blast intro!: order_antisym)
   done
 
-lemma Greatest_equality:
-  "P (k::'a::order) ==> (!!x. P x ==> x <= k) ==> (GREATEST x. P x) = k"
+lemma Greatest_equality: "P k \<Longrightarrow> (\<And>x. P x \<Longrightarrow> x \<le> k) \<Longrightarrow> (GREATEST x. P x) = k"
+  for k :: "'a::order"
   apply (simp add: Greatest_def)
-  apply (erule GreatestM_equality, blast)
+  apply (erule GreatestM_equality)
+  apply blast
   done
 
 lemma ex_has_greatest_nat_lemma:
-  "P k ==> \<forall>x. P x --> (\<exists>y. P y & ~ ((m y::nat) <= m x))
-    ==> \<exists>y. P y & ~ (m y < m k + n)"
-  apply (induct n, force)
-  apply (force simp add: le_Suc_eq)
-  done
+  "P k \<Longrightarrow> \<forall>x. P x \<longrightarrow> (\<exists>y. P y \<and> \<not> m y \<le> (m x :: nat)) \<Longrightarrow> \<exists>y. P y \<and> \<not> m y < m k + n"
+  by (induct n) (force simp: le_Suc_eq)+
 
 lemma ex_has_greatest_nat:
-  "P k ==> \<forall>y. P y --> m y < b
-    ==> \<exists>x. P x & (\<forall>y. P y --> (m y::nat) <= m x)"
+  "P k \<Longrightarrow> \<forall>y. P y \<longrightarrow> m y < b \<Longrightarrow> \<exists>x. P x \<and> (\<forall>y. P y \<longrightarrow> m y \<le> (m x :: nat))"
   apply (rule ccontr)
   apply (cut_tac P = P and n = "b - m k" in ex_has_greatest_nat_lemma)
-    apply (subgoal_tac [3] "m k <= b", auto)
+    apply (subgoal_tac [3] "m k \<le> b")
+     apply auto
   done
 
 lemma GreatestM_nat_lemma:
-  "P k ==> \<forall>y. P y --> m y < b
-    ==> P (GreatestM m P) & (\<forall>y. P y --> (m y::nat) <= m (GreatestM m P))"
+  "P k \<Longrightarrow> \<forall>y. P y \<longrightarrow> m y < b \<Longrightarrow>
+    P (GreatestM m P) \<and> (\<forall>y. P y \<longrightarrow> (m y :: nat) \<le> m (GreatestM m P))"
   apply (simp add: GreatestM_def)
   apply (rule someI_ex)
-  apply (erule ex_has_greatest_nat, assumption)
+  apply (erule ex_has_greatest_nat)
+  apply assumption
   done
 
 lemmas GreatestM_natI = GreatestM_nat_lemma [THEN conjunct1]
 
-lemma GreatestM_nat_le:
-  "P x ==> \<forall>y. P y --> m y < b
-    ==> (m x::nat) <= m (GreatestM m P)"
-  apply (blast dest: GreatestM_nat_lemma [THEN conjunct2, THEN spec, of P])
-  done
+lemma GreatestM_nat_le: "P x \<Longrightarrow> \<forall>y. P y \<longrightarrow> m y < b \<Longrightarrow> (m x :: nat) \<le> m (GreatestM m P)"
+  by (blast dest: GreatestM_nat_lemma [THEN conjunct2, THEN spec, of P])
 
 
-text \<open>\medskip Specialization to \<open>GREATEST\<close>.\<close>
+text \<open>\<^medskip> Specialization to \<open>GREATEST\<close>.\<close>
 
-lemma GreatestI: "P (k::nat) ==> \<forall>y. P y --> y < b ==> P (GREATEST x. P x)"
-  apply (simp add: Greatest_def)
-  apply (rule GreatestM_natI, auto)
-  done
+lemma GreatestI: "P k \<Longrightarrow> \<forall>y. P y \<longrightarrow> y < b \<Longrightarrow> P (GREATEST x. P x)"
+  for k :: nat
+  unfolding Greatest_def by (rule GreatestM_natI) auto
 
-lemma Greatest_le:
-    "P x ==> \<forall>y. P y --> y < b ==> (x::nat) <= (GREATEST x. P x)"
-  apply (simp add: Greatest_def)
-  apply (rule GreatestM_nat_le, auto)
-  done
+lemma Greatest_le: "P x \<Longrightarrow> \<forall>y. P y \<longrightarrow> y < b \<Longrightarrow> x \<le> (GREATEST x. P x)"
+  for x :: nat
+  unfolding Greatest_def by (rule GreatestM_nat_le) auto
 
 
 subsection \<open>An aside: bounded accessible part\<close>
@@ -732,7 +744,8 @@
 
 lemma finite_mono_remains_stable_implies_strict_prefix:
   fixes f :: "nat \<Rightarrow> 'a::order"
-  assumes S: "finite (range f)" "mono f" and eq: "\<forall>n. f n = f (Suc n) \<longrightarrow> f (Suc n) = f (Suc (Suc n))"
+  assumes S: "finite (range f)" "mono f"
+    and eq: "\<forall>n. f n = f (Suc n) \<longrightarrow> f (Suc n) = f (Suc (Suc n))"
   shows "\<exists>N. (\<forall>n\<le>N. \<forall>m\<le>N. m < n \<longrightarrow> f m < f n) \<and> (\<forall>n\<ge>N. f N = f n)"
   using assms
 proof -
@@ -740,15 +753,16 @@
   proof (rule ccontr)
     assume "\<not> ?thesis"
     then have "\<And>n. f n \<noteq> f (Suc n)" by auto
-    then have "\<And>n. f n < f (Suc n)"
-      using  \<open>mono f\<close> by (auto simp: le_less mono_iff_le_Suc)
-    with lift_Suc_mono_less_iff[of f]
-    have *: "\<And>n m. n < m \<Longrightarrow> f n < f m" by auto
+    with \<open>mono f\<close> have "\<And>n. f n < f (Suc n)"
+      by (auto simp: le_less mono_iff_le_Suc)
+    with lift_Suc_mono_less_iff[of f] have *: "\<And>n m. n < m \<Longrightarrow> f n < f m"
+      by auto
     have "inj f"
     proof (intro injI)
       fix x y
       assume "f x = f y"
-      then show "x = y" by (cases x y rule: linorder_cases) (auto dest: *)
+      then show "x = y"
+        by (cases x y rule: linorder_cases) (auto dest: *)
     qed
     with \<open>finite (range f)\<close> have "finite (UNIV::nat set)"
       by (rule finite_imageD)
@@ -760,16 +774,22 @@
     unfolding N_def using n by (rule LeastI)
   show ?thesis
   proof (intro exI[of _ N] conjI allI impI)
-    fix n assume "N \<le> n"
+    fix n
+    assume "N \<le> n"
     then have "\<And>m. N \<le> m \<Longrightarrow> m \<le> n \<Longrightarrow> f m = f N"
     proof (induct rule: dec_induct)
-      case (step n) then show ?case
-        using eq[rule_format, of "n - 1"] N
+      case base
+      then show ?case by simp
+    next
+      case (step n)
+      then show ?case
+        using eq [rule_format, of "n - 1"] N
         by (cases n) (auto simp add: le_Suc_eq)
-    qed simp
+    qed
     from this[of n] \<open>N \<le> n\<close> show "f N = f n" by auto
   next
-    fix n m :: nat assume "m < n" "n \<le> N"
+    fix n m :: nat
+    assume "m < n" "n \<le> N"
     then show "f m < f n"
     proof (induct rule: less_Suc_induct)
       case (1 i)
@@ -777,37 +797,41 @@
       then have "f i \<noteq> f (Suc i)"
         unfolding N_def by (rule not_less_Least)
       with \<open>mono f\<close> show ?case by (simp add: mono_iff_le_Suc less_le)
-    qed auto
+    next
+      case 2
+      then show ?case by simp
+    qed
   qed
 qed
 
 lemma finite_mono_strict_prefix_implies_finite_fixpoint:
   fixes f :: "nat \<Rightarrow> 'a set"
   assumes S: "\<And>i. f i \<subseteq> S" "finite S"
-    and inj: "\<exists>N. (\<forall>n\<le>N. \<forall>m\<le>N. m < n \<longrightarrow> f m \<subset> f n) \<and> (\<forall>n\<ge>N. f N = f n)"
+    and ex: "\<exists>N. (\<forall>n\<le>N. \<forall>m\<le>N. m < n \<longrightarrow> f m \<subset> f n) \<and> (\<forall>n\<ge>N. f N = f n)"
   shows "f (card S) = (\<Union>n. f n)"
 proof -
-  from inj obtain N where inj: "(\<forall>n\<le>N. \<forall>m\<le>N. m < n \<longrightarrow> f m \<subset> f n)" and eq: "(\<forall>n\<ge>N. f N = f n)" by auto
-
-  { fix i have "i \<le> N \<Longrightarrow> i \<le> card (f i)"
-    proof (induct i)
-      case 0 then show ?case by simp
-    next
-      case (Suc i)
-      with inj[rule_format, of "Suc i" i]
-      have "(f i) \<subset> (f (Suc i))" by auto
-      moreover have "finite (f (Suc i))" using S by (rule finite_subset)
-      ultimately have "card (f i) < card (f (Suc i))" by (intro psubset_card_mono)
-      with Suc show ?case using inj by auto
-    qed
-  }
+  from ex obtain N where inj: "\<And>n m. n \<le> N \<Longrightarrow> m \<le> N \<Longrightarrow> m < n \<Longrightarrow> f m \<subset> f n"
+    and eq: "\<forall>n\<ge>N. f N = f n"
+    by atomize auto
+  have "i \<le> N \<Longrightarrow> i \<le> card (f i)" for i
+  proof (induct i)
+    case 0
+    then show ?case by simp
+  next
+    case (Suc i)
+    with inj [of "Suc i" i] have "(f i) \<subset> (f (Suc i))" by auto
+    moreover have "finite (f (Suc i))" using S by (rule finite_subset)
+    ultimately have "card (f i) < card (f (Suc i))" by (intro psubset_card_mono)
+    with Suc inj show ?case by auto
+  qed
   then have "N \<le> card (f N)" by simp
   also have "\<dots> \<le> card S" using S by (intro card_mono)
   finally have "f (card S) = f N" using eq by auto
-  then show ?thesis using eq inj[rule_format, of N]
+  then show ?thesis
+    using eq inj [of N]
     apply auto
     apply (case_tac "n < N")
-    apply (auto simp: not_less)
+     apply (auto simp: not_less)
     done
 qed
 
@@ -819,183 +843,174 @@
   assumes bij: "bij f"
 begin
 
-lemma bij_inv:
-  "bij (inv f)"
+lemma bij_inv: "bij (inv f)"
   using bij by (rule bij_imp_bij_inv)
 
-lemma surj [simp]:
-  "surj f"
+lemma surj [simp]: "surj f"
   using bij by (rule bij_is_surj)
 
-lemma inj:
-  "inj f"
+lemma inj: "inj f"
   using bij by (rule bij_is_inj)
 
-lemma surj_inv [simp]:
-  "surj (inv f)"
+lemma surj_inv [simp]: "surj (inv f)"
   using inj by (rule inj_imp_surj_inv)
 
-lemma inj_inv:
-  "inj (inv f)"
+lemma inj_inv: "inj (inv f)"
   using surj by (rule surj_imp_inj_inv)
 
-lemma eqI:
-  "f a = f b \<Longrightarrow> a = b"
+lemma eqI: "f a = f b \<Longrightarrow> a = b"
   using inj by (rule injD)
 
-lemma eq_iff [simp]:
-  "f a = f b \<longleftrightarrow> a = b"
+lemma eq_iff [simp]: "f a = f b \<longleftrightarrow> a = b"
   by (auto intro: eqI)
 
-lemma eq_invI:
-  "inv f a = inv f b \<Longrightarrow> a = b"
+lemma eq_invI: "inv f a = inv f b \<Longrightarrow> a = b"
   using inj_inv by (rule injD)
 
-lemma eq_inv_iff [simp]:
-  "inv f a = inv f b \<longleftrightarrow> a = b"
+lemma eq_inv_iff [simp]: "inv f a = inv f b \<longleftrightarrow> a = b"
   by (auto intro: eq_invI)
 
-lemma inv_left [simp]:
-  "inv f (f a) = a"
+lemma inv_left [simp]: "inv f (f a) = a"
   using inj by (simp add: inv_f_eq)
 
-lemma inv_comp_left [simp]:
-  "inv f \<circ> f = id"
+lemma inv_comp_left [simp]: "inv f \<circ> f = id"
   by (simp add: fun_eq_iff)
 
-lemma inv_right [simp]:
-  "f (inv f a) = a"
+lemma inv_right [simp]: "f (inv f a) = a"
   using surj by (simp add: surj_f_inv_f)
 
-lemma inv_comp_right [simp]:
-  "f \<circ> inv f = id"
+lemma inv_comp_right [simp]: "f \<circ> inv f = id"
   by (simp add: fun_eq_iff)
 
-lemma inv_left_eq_iff [simp]:
-  "inv f a = b \<longleftrightarrow> f b = a"
+lemma inv_left_eq_iff [simp]: "inv f a = b \<longleftrightarrow> f b = a"
   by auto
 
-lemma inv_right_eq_iff [simp]:
-  "b = inv f a \<longleftrightarrow> f b = a"
+lemma inv_right_eq_iff [simp]: "b = inv f a \<longleftrightarrow> f b = a"
   by auto
 
 end
 
 lemma infinite_imp_bij_betw:
-assumes INF: "\<not> finite A"
-shows "\<exists>h. bij_betw h A (A - {a})"
-proof(cases "a \<in> A")
-  assume Case1: "a \<notin> A"  hence "A - {a} = A" by blast
-  thus ?thesis using bij_betw_id[of A] by auto
+  assumes infinite: "\<not> finite A"
+  shows "\<exists>h. bij_betw h A (A - {a})"
+proof (cases "a \<in> A")
+  case False
+  then have "A - {a} = A" by blast
+  then show ?thesis
+    using bij_betw_id[of A] by auto
 next
-  assume Case2: "a \<in> A"
-  have "\<not> finite (A - {a})" using INF by auto
-  with infinite_iff_countable_subset[of "A - {a}"] obtain f::"nat \<Rightarrow> 'a"
-  where 1: "inj f" and 2: "f ` UNIV \<le> A - {a}" by blast
-  obtain g where g_def: "g = (\<lambda> n. if n = 0 then a else f (Suc n))" by blast
-  obtain A' where A'_def: "A' = g ` UNIV" by blast
-  have temp: "\<forall>y. f y \<noteq> a" using 2 by blast
-  have 3: "inj_on g UNIV \<and> g ` UNIV \<le> A \<and> a \<in> g ` UNIV"
-  proof(auto simp add: Case2 g_def, unfold inj_on_def, intro ballI impI,
-        case_tac "x = 0", auto simp add: 2)
-    fix y  assume "a = (if y = 0 then a else f (Suc y))"
-    thus "y = 0" using temp by (case_tac "y = 0", auto)
+  case True
+  with infinite have "\<not> finite (A - {a})" by auto
+  with infinite_iff_countable_subset[of "A - {a}"]
+  obtain f :: "nat \<Rightarrow> 'a" where 1: "inj f" and 2: "f ` UNIV \<subseteq> A - {a}" by blast
+  define g where "g n = (if n = 0 then a else f (Suc n))" for n
+  define A' where "A' = g ` UNIV"
+  have *: "\<forall>y. f y \<noteq> a" using 2 by blast
+  have 3: "inj_on g UNIV \<and> g ` UNIV \<subseteq> A \<and> a \<in> g ` UNIV"
+    apply (auto simp add: True g_def [abs_def])
+     apply (unfold inj_on_def)
+     apply (intro ballI impI)
+     apply (case_tac "x = 0")
+      apply (auto simp add: 2)
+  proof -
+    fix y
+    assume "a = (if y = 0 then a else f (Suc y))"
+    then show "y = 0" by (cases "y = 0") (use * in auto)
   next
     fix x y
     assume "f (Suc x) = (if y = 0 then a else f (Suc y))"
-    thus "x = y" using 1 temp unfolding inj_on_def by (case_tac "y = 0", auto)
+    with 1 * show "x = y" by (cases "y = 0") (auto simp: inj_on_def)
   next
-    fix n show "f (Suc n) \<in> A" using 2 by blast
+    fix n
+    from 2 show "f (Suc n) \<in> A" by blast
   qed
-  hence 4: "bij_betw g UNIV A' \<and> a \<in> A' \<and> A' \<le> A"
-  using inj_on_imp_bij_betw[of g] unfolding A'_def by auto
-  hence 5: "bij_betw (inv g) A' UNIV"
-  by (auto simp add: bij_betw_inv_into)
-  (*  *)
-  obtain n where "g n = a" using 3 by auto
-  hence 6: "bij_betw g (UNIV - {n}) (A' - {a})"
-  using 3 4 unfolding A'_def
-  by clarify (rule bij_betw_subset, auto simp: image_set_diff)
-  (*  *)
-  obtain v where v_def: "v = (\<lambda> m. if m < n then m else Suc m)" by blast
+  then have 4: "bij_betw g UNIV A' \<and> a \<in> A' \<and> A' \<subseteq> A"
+    using inj_on_imp_bij_betw[of g] by (auto simp: A'_def)
+  then have 5: "bij_betw (inv g) A' UNIV"
+    by (auto simp add: bij_betw_inv_into)
+  from 3 obtain n where n: "g n = a" by auto
+  have 6: "bij_betw g (UNIV - {n}) (A' - {a})"
+    by (rule bij_betw_subset) (use 3 4 n in \<open>auto simp: image_set_diff A'_def\<close>)
+  define v where "v m = (if m < n then m else Suc m)" for m
   have 7: "bij_betw v UNIV (UNIV - {n})"
-  proof(unfold bij_betw_def inj_on_def, intro conjI, clarify)
-    fix m1 m2 assume "v m1 = v m2"
-    thus "m1 = m2"
-    by(case_tac "m1 < n", case_tac "m2 < n",
-       auto simp add: inj_on_def v_def, case_tac "m2 < n", auto)
+  proof (unfold bij_betw_def inj_on_def, intro conjI, clarify)
+    fix m1 m2
+    assume "v m1 = v m2"
+    then show "m1 = m2"
+      apply (cases "m1 < n")
+       apply (cases "m2 < n")
+        apply (auto simp: inj_on_def v_def [abs_def])
+      apply (cases "m2 < n")
+       apply auto
+      done
   next
     show "v ` UNIV = UNIV - {n}"
-    proof(auto simp add: v_def)
-      fix m assume *: "m \<noteq> n" and **: "m \<notin> Suc ` {m'. \<not> m' < n}"
-      {assume "n \<le> m" with * have 71: "Suc n \<le> m" by auto
-       then obtain m' where 72: "m = Suc m'" using Suc_le_D by auto
-       with 71 have "n \<le> m'" by auto
-       with 72 ** have False by auto
-      }
-      thus "m < n" by force
+    proof (auto simp: v_def [abs_def])
+      fix m
+      assume "m \<noteq> n"
+      assume *: "m \<notin> Suc ` {m'. \<not> m' < n}"
+      have False if "n \<le> m"
+      proof -
+        from \<open>m \<noteq> n\<close> that have **: "Suc n \<le> m" by auto
+        from Suc_le_D [OF this] obtain m' where m': "m = Suc m'" ..
+        with ** have "n \<le> m'" by auto
+        with m' * show ?thesis by auto
+      qed
+      then show "m < n" by force
     qed
   qed
-  (*  *)
-  obtain h' where h'_def: "h' = g o v o (inv g)" by blast
-  hence 8: "bij_betw h' A' (A' - {a})" using 5 7 6
-  by (auto simp add: bij_betw_trans)
-  (*  *)
-  obtain h where h_def: "h = (\<lambda> b. if b \<in> A' then h' b else b)" by blast
-  have "\<forall>b \<in> A'. h b = h' b" unfolding h_def by auto
-  hence "bij_betw h  A' (A' - {a})" using 8 bij_betw_cong[of A' h] by auto
+  define h' where "h' = g \<circ> v \<circ> (inv g)"
+  with 5 6 7 have 8: "bij_betw h' A' (A' - {a})"
+    by (auto simp add: bij_betw_trans)
+  define h where "h b = (if b \<in> A' then h' b else b)" for b
+  then have "\<forall>b \<in> A'. h b = h' b" by simp
+  with 8 have "bij_betw h  A' (A' - {a})"
+    using bij_betw_cong[of A' h] by auto
   moreover
-  {have "\<forall>b \<in> A - A'. h b = b" unfolding h_def by auto
-   hence "bij_betw h  (A - A') (A - A')"
-   using bij_betw_cong[of "A - A'" h id] bij_betw_id[of "A - A'"] by auto
-  }
+  have "\<forall>b \<in> A - A'. h b = b" by (auto simp: h_def)
+  then have "bij_betw h  (A - A') (A - A')"
+    using bij_betw_cong[of "A - A'" h id] bij_betw_id[of "A - A'"] by auto
   moreover
-  have "(A' Int (A - A') = {} \<and> A' \<union> (A - A') = A) \<and>
-        ((A' - {a}) Int (A - A') = {} \<and> (A' - {a}) \<union> (A - A') = A - {a})"
-  using 4 by blast
+  from 4 have "(A' \<inter> (A - A') = {} \<and> A' \<union> (A - A') = A) \<and>
+    ((A' - {a}) \<inter> (A - A') = {} \<and> (A' - {a}) \<union> (A - A') = A - {a})"
+    by blast
   ultimately have "bij_betw h A (A - {a})"
-  using bij_betw_combine[of h A' "A' - {a}" "A - A'" "A - A'"] by simp
-  thus ?thesis by blast
+    using bij_betw_combine[of h A' "A' - {a}" "A - A'" "A - A'"] by simp
+  then show ?thesis by blast
 qed
 
 lemma infinite_imp_bij_betw2:
-assumes INF: "\<not> finite A"
-shows "\<exists>h. bij_betw h A (A \<union> {a})"
-proof(cases "a \<in> A")
-  assume Case1: "a \<in> A"  hence "A \<union> {a} = A" by blast
-  thus ?thesis using bij_betw_id[of A] by auto
+  assumes "\<not> finite A"
+  shows "\<exists>h. bij_betw h A (A \<union> {a})"
+proof (cases "a \<in> A")
+  case True
+  then have "A \<union> {a} = A" by blast
+  then show ?thesis using bij_betw_id[of A] by auto
 next
+  case False
   let ?A' = "A \<union> {a}"
-  assume Case2: "a \<notin> A" hence "A = ?A' - {a}" by blast
-  moreover have "\<not> finite ?A'" using INF by auto
+  from False have "A = ?A' - {a}" by blast
+  moreover from assms have "\<not> finite ?A'" by auto
   ultimately obtain f where "bij_betw f ?A' A"
-  using infinite_imp_bij_betw[of ?A' a] by auto
-  hence "bij_betw(inv_into ?A' f) A ?A'" using bij_betw_inv_into by blast
-  thus ?thesis by auto
+    using infinite_imp_bij_betw[of ?A' a] by auto
+  then have "bij_betw (inv_into ?A' f) A ?A'" by (rule bij_betw_inv_into)
+  then show ?thesis by auto
 qed
 
-lemma bij_betw_inv_into_left:
-assumes BIJ: "bij_betw f A A'" and IN: "a \<in> A"
-shows "(inv_into A f) (f a) = a"
-using assms unfolding bij_betw_def
-by clarify (rule inv_into_f_f)
+lemma bij_betw_inv_into_left: "bij_betw f A A' \<Longrightarrow> a \<in> A \<Longrightarrow> inv_into A f (f a) = a"
+  unfolding bij_betw_def by clarify (rule inv_into_f_f)
 
-lemma bij_betw_inv_into_right:
-assumes "bij_betw f A A'" "a' \<in> A'"
-shows "f(inv_into A f a') = a'"
-using assms unfolding bij_betw_def using f_inv_into_f by force
+lemma bij_betw_inv_into_right: "bij_betw f A A' \<Longrightarrow> a' \<in> A' \<Longrightarrow> f (inv_into A f a') = a'"
+  unfolding bij_betw_def using f_inv_into_f by force
 
 lemma bij_betw_inv_into_subset:
-assumes BIJ: "bij_betw f A A'" and
-        SUB: "B \<le> A" and IM: "f ` B = B'"
-shows "bij_betw (inv_into A f) B' B"
-using assms unfolding bij_betw_def
-by (auto intro: inj_on_inv_into)
+  "bij_betw f A A' \<Longrightarrow> B \<subseteq> A \<Longrightarrow> f ` B = B' \<Longrightarrow> bij_betw (inv_into A f) B' B"
+  by (auto simp: bij_betw_def intro: inj_on_inv_into)
 
 
 subsection \<open>Specification package -- Hilbertized version\<close>
 
-lemma exE_some: "[| Ex P ; c == Eps P |] ==> P c"
+lemma exE_some: "Ex P \<Longrightarrow> c \<equiv> Eps P \<Longrightarrow> P c"
   by (simp only: someI_ex)
 
 ML_file "Tools/choice_specification.ML"
diff -r fb63942e470e -r 7195acc2fe93 src/HOL/Relation.thy
--- a/src/HOL/Relation.thy	Fri Aug 05 16:36:03 2016 +0200
+++ b/src/HOL/Relation.thy	Fri Aug 05 18:14:28 2016 +0200
@@ -1,11 +1,12 @@
 (*  Title:      HOL/Relation.thy
-    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory; Stefan Berghofer, TU Muenchen
+    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
+    Author:     Stefan Berghofer, TU Muenchen
 *)
 
 section \<open>Relations -- as sets of pairs, and binary predicates\<close>
 
 theory Relation
-imports Finite_Set
+  imports Finite_Set
 begin
 
 text \<open>A preliminary: classical rules for reasoning on predicates\<close>
@@ -400,16 +401,17 @@
   by (auto intro: transpI)
 
 lemma trans_empty [simp]: "trans {}"
-by (blast intro: transI)
+  by (blast intro: transI)
 
 lemma transp_empty [simp]: "transp (\<lambda>x y. False)"
-using trans_empty[to_pred] by(simp add: bot_fun_def)
+  using trans_empty[to_pred] by (simp add: bot_fun_def)
 
 lemma trans_singleton [simp]: "trans {(a, a)}"
-by (blast intro: transI)
+  by (blast intro: transI)
 
 lemma transp_singleton [simp]: "transp (\<lambda>x y. x = a \<and> y = a)"
-by(simp add: transp_def)
+  by (simp add: transp_def)
+
 
 subsubsection \<open>Totality\<close>
 
@@ -418,7 +420,7 @@
 
 lemma total_onI [intro?]:
   "(\<And>x y. \<lbrakk>x \<in> A; y \<in> A; x \<noteq> y\<rbrakk> \<Longrightarrow> (x, y) \<in> r \<or> (y, x) \<in> r) \<Longrightarrow> total_on A r"
-unfolding total_on_def by blast
+  unfolding total_on_def by blast
 
 abbreviation "total \<equiv> total_on UNIV"
 
@@ -426,7 +428,8 @@
   by (simp add: total_on_def)
 
 lemma total_on_singleton [simp]: "total_on {x} {(x, x)}"
-unfolding total_on_def by blast
+  unfolding total_on_def by blast
+
 
 subsubsection \<open>Single valued relations\<close>
 
@@ -496,7 +499,7 @@
 
 subsubsection \<open>Diagonal: identity over a set\<close>
 
-definition Id_on  :: "'a set \<Rightarrow> 'a rel"
+definition Id_on :: "'a set \<Rightarrow> 'a rel"
   where "Id_on A = (\<Union>x\<in>A. {(x, x)})"
 
 lemma Id_on_empty [simp]: "Id_on {} = {}"
@@ -633,7 +636,7 @@
 lemma relcompp_apply: "(R OO S) a c \<longleftrightarrow> (\<exists>b. R a b \<and> S b c)"
   unfolding relcomp_unfold [to_pred] ..
 
-lemma eq_OO: "op= OO R = R"
+lemma eq_OO: "op = OO R = R"
   by blast
 
 lemma OO_eq: "R OO op = = R"
@@ -728,10 +731,10 @@
 lemma conversep_inject[simp]: "r\<inverse>\<inverse> = s \<inverse>\<inverse> \<longleftrightarrow> r = s"
   by (fact converse_inject[to_pred])
 
-lemma converse_subset_swap: "r \<subseteq> s \<inverse> = (r \<inverse> \<subseteq> s)"
+lemma converse_subset_swap: "r \<subseteq> s \<inverse> \<longleftrightarrow> r \<inverse> \<subseteq> s"
   by auto
 
-lemma conversep_le_swap: "r \<le> s \<inverse>\<inverse> = (r \<inverse>\<inverse> \<le> s)"
+lemma conversep_le_swap: "r \<le> s \<inverse>\<inverse> \<longleftrightarrow> r \<inverse>\<inverse> \<le> s"
   by (fact converse_subset_swap[to_pred])
 
 lemma converse_Id [simp]: "Id\<inverse> = Id"
@@ -800,7 +803,7 @@
   where "Field r = Domain r \<union> Range r"
 
 lemma FieldI1: "(i, j) \<in> R \<Longrightarrow> i \<in> Field R"
-unfolding Field_def by blast
+  unfolding Field_def by blast
 
 lemma FieldI2: "(i, j) \<in> R \<Longrightarrow> j \<in> Field R"
   unfolding Field_def by auto
@@ -932,7 +935,7 @@
   by blast
 
 lemma Field_square [simp]: "Field (x \<times> x) = x"
-unfolding Field_def by blast
+  unfolding Field_def by blast
 
 
 subsubsection \<open>Image of a set under a relation\<close>
@@ -972,7 +975,7 @@
   by blast
 
 lemma Image_Int_eq: "single_valued (converse R) \<Longrightarrow> R `` (A \<inter> B) = R `` A \<inter> R `` B"
-  by (simp add: single_valued_def, blast)
+  by (auto simp: single_valued_def)
 
 lemma Image_Un: "R `` (A \<union> B) = R `` A \<union> R `` B"
   by blast
@@ -1079,7 +1082,7 @@
   interpret comp_fun_idem Set.insert
     by (fact comp_fun_idem_insert)
   show ?thesis
-    by standard (auto simp add: fun_eq_iff comp_fun_commute split: prod.split)
+    by standard (auto simp: fun_eq_iff comp_fun_commute split: prod.split)
 qed
 
 lemma Image_fold:
diff -r fb63942e470e -r 7195acc2fe93 src/HOL/Transitive_Closure.thy
--- a/src/HOL/Transitive_Closure.thy	Fri Aug 05 16:36:03 2016 +0200
+++ b/src/HOL/Transitive_Closure.thy	Fri Aug 05 18:14:28 2016 +0200
@@ -6,7 +6,7 @@
 section \<open>Reflexive and Transitive closure of a relation\<close>
 
 theory Transitive_Closure
-imports Relation
+  imports Relation
 begin
 
 ML_file "~~/src/Provers/trancl.ML"
@@ -16,25 +16,24 @@
   \<open>trancl\<close> is transitive closure,
   \<open>reflcl\<close> is reflexive closure.
 
-  These postfix operators have \emph{maximum priority}, forcing their
+  These postfix operators have \<^emph>\<open>maximum priority\<close>, forcing their
   operands to be atomic.
 \<close>
 
-context
-  notes [[inductive_internals]]
+context notes [[inductive_internals]]
 begin
 
 inductive_set rtrancl :: "('a \<times> 'a) set \<Rightarrow> ('a \<times> 'a) set"  ("(_\<^sup>*)" [1000] 999)
   for r :: "('a \<times> 'a) set"
-where
-  rtrancl_refl [intro!, Pure.intro!, simp]: "(a, a) \<in> r\<^sup>*"
-| rtrancl_into_rtrancl [Pure.intro]: "(a, b) \<in> r\<^sup>* \<Longrightarrow> (b, c) \<in> r \<Longrightarrow> (a, c) \<in> r\<^sup>*"
+  where
+    rtrancl_refl [intro!, Pure.intro!, simp]: "(a, a) \<in> r\<^sup>*"
+  | rtrancl_into_rtrancl [Pure.intro]: "(a, b) \<in> r\<^sup>* \<Longrightarrow> (b, c) \<in> r \<Longrightarrow> (a, c) \<in> r\<^sup>*"
 
 inductive_set trancl :: "('a \<times> 'a) set \<Rightarrow> ('a \<times> 'a) set"  ("(_\<^sup>+)" [1000] 999)
   for r :: "('a \<times> 'a) set"
-where
-  r_into_trancl [intro, Pure.intro]: "(a, b) \<in> r \<Longrightarrow> (a, b) \<in> r\<^sup>+"
-| trancl_into_trancl [Pure.intro]: "(a, b) \<in> r\<^sup>+ \<Longrightarrow> (b, c) \<in> r \<Longrightarrow> (a, c) \<in> r\<^sup>+"
+  where
+    r_into_trancl [intro, Pure.intro]: "(a, b) \<in> r \<Longrightarrow> (a, b) \<in> r\<^sup>+"
+  | trancl_into_trancl [Pure.intro]: "(a, b) \<in> r\<^sup>+ \<Longrightarrow> (b, c) \<in> r \<Longrightarrow> (a, c) \<in> r\<^sup>+"
 
 notation
   rtranclp  ("(_\<^sup>*\<^sup>*)" [1000] 1000) and
@@ -215,7 +214,9 @@
 
 lemma rtrancl_r_diff_Id: "(r - Id)\<^sup>* = r\<^sup>*"
   apply (rule sym)
-  apply (rule rtrancl_subset, blast, clarify)
+  apply (rule rtrancl_subset)
+   apply blast
+  apply clarify
   apply (rename_tac a b)
   apply (case_tac "a = b")
    apply blast
@@ -258,10 +259,10 @@
 lemmas converse_rtrancl_induct = converse_rtranclp_induct [to_set]
 
 lemmas converse_rtranclp_induct2 =
-  converse_rtranclp_induct [of _ "(ax,ay)" "(bx,by)", split_rule, consumes 1, case_names refl step]
+  converse_rtranclp_induct [of _ "(ax, ay)" "(bx, by)", split_rule, consumes 1, case_names refl step]
 
 lemmas converse_rtrancl_induct2 =
-  converse_rtrancl_induct [of "(ax,ay)" "(bx,by)", split_format (complete),
+  converse_rtrancl_induct [of "(ax, ay)" "(bx, by)", split_format (complete),
     consumes 1, case_names refl step]
 
 lemma converse_rtranclpE [consumes 1, case_names base step]:
@@ -283,24 +284,30 @@
 
 lemma r_comp_rtrancl_eq: "r O r\<^sup>* = r\<^sup>* O r"
   by (blast elim: rtranclE converse_rtranclE
-    intro: rtrancl_into_rtrancl converse_rtrancl_into_rtrancl)
+      intro: rtrancl_into_rtrancl converse_rtrancl_into_rtrancl)
 
 lemma rtrancl_unfold: "r\<^sup>* = Id \<union> r\<^sup>* O r"
   by (auto intro: rtrancl_into_rtrancl elim: rtranclE)
 
 lemma rtrancl_Un_separatorE:
   "(a, b) \<in> (P \<union> Q)\<^sup>* \<Longrightarrow> \<forall>x y. (a, x) \<in> P\<^sup>* \<longrightarrow> (x, y) \<in> Q \<longrightarrow> x = y \<Longrightarrow> (a, b) \<in> P\<^sup>*"
-  apply (induct rule:rtrancl.induct)
-   apply blast
-  apply (blast intro:rtrancl_trans)
-  done
+proof (induct rule: rtrancl.induct)
+  case rtrancl_refl
+  then show ?case by blast
+next
+  case rtrancl_into_rtrancl
+  then show ?case by (blast intro: rtrancl_trans)
+qed
 
 lemma rtrancl_Un_separator_converseE:
   "(a, b) \<in> (P \<union> Q)\<^sup>* \<Longrightarrow> \<forall>x y. (x, b) \<in> P\<^sup>* \<longrightarrow> (y, x) \<in> Q \<longrightarrow> y = x \<Longrightarrow> (a, b) \<in> P\<^sup>*"
-  apply (induct rule:converse_rtrancl_induct)
-   apply blast
-  apply (blast intro:rtrancl_trans)
-  done
+proof (induct rule: converse_rtrancl_induct)
+  case base
+  then show ?case by blast
+next
+  case step
+  then show ?case by (blast intro: rtrancl_trans)
+qed
 
 lemma Image_closed_trancl:
   assumes "r `` X \<subseteq> X"
@@ -368,10 +375,10 @@
 lemmas trancl_induct [induct set: trancl] = tranclp_induct [to_set]
 
 lemmas tranclp_induct2 =
-  tranclp_induct [of _ "(ax,ay)" "(bx,by)", split_rule, consumes 1, case_names base step]
+  tranclp_induct [of _ "(ax, ay)" "(bx, by)", split_rule, consumes 1, case_names base step]
 
 lemmas trancl_induct2 =
-  trancl_induct [of "(ax,ay)" "(bx,by)", split_format (complete),
+  trancl_induct [of "(ax, ay)" "(bx, by)", split_format (complete),
     consumes 1, case_names base step]
 
 lemma tranclp_trans_induct:
@@ -394,7 +401,7 @@
   apply (rule subsetI)
   apply auto
   apply (erule trancl_induct)
-  apply auto
+   apply auto
   done
 
 lemma trancl_unfold: "r\<^sup>+ = r \<union> r\<^sup>+ O r"
@@ -449,7 +456,7 @@
 lemma tranclp_converseI: "(r\<^sup>+\<^sup>+)\<inverse>\<inverse> x y \<Longrightarrow> (r\<inverse>\<inverse>)\<^sup>+\<^sup>+ x y"
   apply (drule conversepD)
   apply (erule tranclp_induct)
-  apply (iprover intro: conversepI tranclp_trans)+
+   apply (iprover intro: conversepI tranclp_trans)+
   done
 
 lemmas trancl_converseI = tranclp_converseI [to_set]
@@ -457,7 +464,7 @@
 lemma tranclp_converseD: "(r\<inverse>\<inverse>)\<^sup>+\<^sup>+ x y \<Longrightarrow> (r\<^sup>+\<^sup>+)\<inverse>\<inverse> x y"
   apply (rule conversepI)
   apply (erule tranclp_induct)
-  apply (iprover dest: conversepD intro: tranclp_trans)+
+   apply (iprover dest: conversepD intro: tranclp_trans)+
   done
 
 lemmas trancl_converseD = tranclp_converseD [to_set]
@@ -493,7 +500,7 @@
 lemma converse_tranclpE:
   assumes major: "tranclp r x z"
     and base: "r x z \<Longrightarrow> P"
-    and step: "\<And> y. r x y \<Longrightarrow> tranclp r y z \<Longrightarrow> P"
+    and step: "\<And>y. r x y \<Longrightarrow> tranclp r y z \<Longrightarrow> P"
   shows P
 proof -
   from tranclpD [OF major] obtain y where "r x y" and "rtranclp r y z"
@@ -582,7 +589,7 @@
    apply (blast intro: rtrancl_into_trancl1 trancl_into_rtrancl trancl_trans)
   apply (rule subsetI)
   apply (blast intro: trancl_mono rtrancl_mono
-    [THEN [2] rev_subsetD] rtrancl_trancl_trancl rtrancl_into_trancl2)
+      [THEN [2] rev_subsetD] rtrancl_trancl_trancl rtrancl_into_trancl2)
   done
 
 lemma trancl_insert2:
@@ -655,26 +662,23 @@
 lemma single_valued_confluent:
   "single_valued r \<Longrightarrow> (x, y) \<in> r\<^sup>* \<Longrightarrow> (x, z) \<in> r\<^sup>* \<Longrightarrow> (y, z) \<in> r\<^sup>* \<or> (z, y) \<in> r\<^sup>*"
   apply (erule rtrancl_induct)
-  apply simp
+   apply simp
   apply (erule disjE)
    apply (blast elim:converse_rtranclE dest:single_valuedD)
-  apply(blast intro:rtrancl_trans)
+  apply (blast intro:rtrancl_trans)
   done
 
 lemma r_r_into_trancl: "(a, b) \<in> R \<Longrightarrow> (b, c) \<in> R \<Longrightarrow> (a, c) \<in> R\<^sup>+"
   by (fast intro: trancl_trans)
 
 lemma trancl_into_trancl: "(a, b) \<in> r\<^sup>+ \<Longrightarrow> (b, c) \<in> r \<Longrightarrow> (a, c) \<in> r\<^sup>+"
-  apply (induct rule: trancl_induct)
-   apply (fast intro: r_r_into_trancl)
-  apply (fast intro: r_r_into_trancl trancl_trans)
-  done
+  by (induct rule: trancl_induct) (fast intro: r_r_into_trancl trancl_trans)+
 
 lemma tranclp_rtranclp_tranclp: "r\<^sup>+\<^sup>+ a b \<Longrightarrow> r\<^sup>*\<^sup>* b c \<Longrightarrow> r\<^sup>+\<^sup>+ a c"
   apply (drule tranclpD)
   apply (elim exE conjE)
   apply (drule rtranclp_trans, assumption)
-  apply (drule rtranclp_into_tranclp2, assumption, assumption)
+  apply (drule (2) rtranclp_into_tranclp2)
   done
 
 lemmas trancl_rtrancl_trancl = tranclp_rtranclp_tranclp [to_set]
@@ -704,14 +708,14 @@
 begin
 
 primrec relpow :: "nat \<Rightarrow> ('a \<times> 'a) set \<Rightarrow> ('a \<times> 'a) set"
-where
-  "relpow 0 R = Id"
-| "relpow (Suc n) R = (R ^^ n) O R"
+  where
+    "relpow 0 R = Id"
+  | "relpow (Suc n) R = (R ^^ n) O R"
 
 primrec relpowp :: "nat \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> bool)"
-where
-  "relpowp 0 R = HOL.eq"
-| "relpowp (Suc n) R = (R ^^ n) OO R"
+  where
+    "relpowp 0 R = HOL.eq"
+  | "relpowp (Suc n) R = (R ^^ n) OO R"
 
 end
 
@@ -740,10 +744,12 @@
 hide_const (open) relpow
 hide_const (open) relpowp
 
-lemma relpow_1 [simp]: "R ^^ 1 = R" for R :: "('a \<times> 'a) set"
+lemma relpow_1 [simp]: "R ^^ 1 = R"
+  for R :: "('a \<times> 'a) set"
   by simp
 
-lemma relpowp_1 [simp]: "P ^^ 1 = P" for P :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
+lemma relpowp_1 [simp]: "P ^^ 1 = P"
+  for P :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
   by (fact relpow_1 [to_pred])
 
 lemma relpow_0_I: "(x, x) \<in> R ^^ 0"
@@ -777,22 +783,20 @@
   by (fact relpow_Suc_E [to_pred])
 
 lemma relpow_E:
-  "(x, z) \<in>  R ^^ n \<Longrightarrow>  (n = 0 \<Longrightarrow> x = z \<Longrightarrow> P)
-   \<Longrightarrow> (\<And>y m. n = Suc m \<Longrightarrow> (x, y) \<in>  R ^^ m \<Longrightarrow> (y, z) \<in> R \<Longrightarrow> P)
-   \<Longrightarrow> P"
+  "(x, z) \<in>  R ^^ n \<Longrightarrow>
+    (n = 0 \<Longrightarrow> x = z \<Longrightarrow> P) \<Longrightarrow>
+    (\<And>y m. n = Suc m \<Longrightarrow> (x, y) \<in>  R ^^ m \<Longrightarrow> (y, z) \<in> R \<Longrightarrow> P) \<Longrightarrow> P"
   by (cases n) auto
 
 lemma relpowp_E:
-  "(P ^^ n) x z \<Longrightarrow> (n = 0 \<Longrightarrow> x = z \<Longrightarrow> Q)
-  \<Longrightarrow> (\<And>y m. n = Suc m \<Longrightarrow> (P ^^ m) x y \<Longrightarrow> P y z \<Longrightarrow> Q)
-  \<Longrightarrow> Q"
+  "(P ^^ n) x z \<Longrightarrow>
+    (n = 0 \<Longrightarrow> x = z \<Longrightarrow> Q) \<Longrightarrow>
+    (\<And>y m. n = Suc m \<Longrightarrow> (P ^^ m) x y \<Longrightarrow> P y z \<Longrightarrow> Q) \<Longrightarrow> Q"
   by (fact relpow_E [to_pred])
 
 lemma relpow_Suc_D2: "(x, z) \<in> R ^^ Suc n \<Longrightarrow> (\<exists>y. (x, y) \<in> R \<and> (y, z) \<in> R ^^ n)"
-  apply (induct n arbitrary: x z)
-   apply (blast intro: relpow_0_I elim: relpow_0_E relpow_Suc_E)
-  apply (blast intro: relpow_Suc_I elim: relpow_0_E relpow_Suc_E)
-  done
+  by (induct n arbitrary: x z)
+    (blast intro: relpow_0_I relpow_Suc_I elim: relpow_0_E relpow_Suc_E)+
 
 lemma relpowp_Suc_D2: "(P ^^ Suc n) x z \<Longrightarrow> \<exists>y. P x y \<and> (P ^^ n) y z"
   by (fact relpow_Suc_D2 [to_pred])
@@ -810,18 +814,21 @@
   by (fact relpow_Suc_D2' [to_pred])
 
 lemma relpow_E2:
-  "(x, z) \<in> R ^^ n \<Longrightarrow>  (n = 0 \<Longrightarrow> x = z \<Longrightarrow> P)
-     \<Longrightarrow> (\<And>y m. n = Suc m \<Longrightarrow> (x, y) \<in> R \<Longrightarrow> (y, z) \<in> R ^^ m \<Longrightarrow> P)
-   \<Longrightarrow> P"
-  apply (cases n, simp)
+  "(x, z) \<in> R ^^ n \<Longrightarrow>
+    (n = 0 \<Longrightarrow> x = z \<Longrightarrow> P) \<Longrightarrow>
+    (\<And>y m. n = Suc m \<Longrightarrow> (x, y) \<in> R \<Longrightarrow> (y, z) \<in> R ^^ m \<Longrightarrow> P) \<Longrightarrow> P"
+  apply (cases n)
+   apply simp
   apply (rename_tac nat)
-  apply (cut_tac n=nat and R=R in relpow_Suc_D2', simp, blast)
+  apply (cut_tac n=nat and R=R in relpow_Suc_D2')
+  apply simp
+  apply blast
   done
 
 lemma relpowp_E2:
-  "(P ^^ n) x z \<Longrightarrow> (n = 0 \<Longrightarrow> x = z \<Longrightarrow> Q)
-    \<Longrightarrow> (\<And>y m. n = Suc m \<Longrightarrow> P x y \<Longrightarrow> (P ^^ m) y z \<Longrightarrow> Q)
-  \<Longrightarrow> Q"
+  "(P ^^ n) x z \<Longrightarrow>
+    (n = 0 \<Longrightarrow> x = z \<Longrightarrow> Q) \<Longrightarrow>
+    (\<And>y m. n = Suc m \<Longrightarrow> P x y \<Longrightarrow> (P ^^ m) y z \<Longrightarrow> Q) \<Longrightarrow> Q"
   by (fact relpow_E2 [to_pred])
 
 lemma relpow_add: "R ^^ (m + n) = R^^m O R^^n"
@@ -848,7 +855,8 @@
 proof (cases p)
   case (Pair x y)
   with assms have "(x, y) \<in> R\<^sup>*" by simp
-  then have "(x, y) \<in> (\<Union>n. R ^^ n)" proof induct
+  then have "(x, y) \<in> (\<Union>n. R ^^ n)"
+  proof induct
     case base
     show ?case by (blast intro: relpow_0_I)
   next
@@ -869,7 +877,8 @@
 proof (cases p)
   case (Pair x y)
   with assms have "(x, y) \<in> R ^^ n" by simp
-  then have "(x, y) \<in> R\<^sup>*" proof (induct n arbitrary: x y)
+  then have "(x, y) \<in> R\<^sup>*"
+  proof (induct n arbitrary: x y)
     case 0
     then show ?case by simp
   next
@@ -905,10 +914,12 @@
    apply (clarsimp simp: relcomp_unfold)
    apply fastforce
   apply clarsimp
-  apply (case_tac n, simp)
+  apply (case_tac n)
+   apply simp
   apply clarsimp
   apply (drule relpow_imp_rtrancl)
-  apply (drule rtrancl_into_trancl1) apply auto
+  apply (drule rtrancl_into_trancl1)
+   apply auto
   done
 
 lemma tranclp_power: "(P\<^sup>+\<^sup>+) x y \<longleftrightarrow> (\<exists>n > 0. (P ^^ n) x y)"
@@ -954,7 +965,8 @@
 lemma relpow_finite_bounded1:
   fixes R :: "('a \<times> 'a) set"
   assumes "finite R" and "k > 0"
-  shows "R^^k \<subseteq> (\<Union>n\<in>{n. 0 < n \<and> n \<le> card R}. R^^n)" (is "_ \<subseteq> ?r")
+  shows "R^^k \<subseteq> (\<Union>n\<in>{n. 0 < n \<and> n \<le> card R}. R^^n)"
+    (is "_ \<subseteq> ?r")
 proof -
   have "(a, b) \<in> R^^(Suc k) \<Longrightarrow> \<exists>n. 0 < n \<and> n \<le> card R \<and> (a, b) \<in> R^^n" for a b k
   proof (induct k arbitrary: b)
@@ -1050,8 +1062,7 @@
   shows "R^^k \<subseteq> (UN n:{n. n \<le> card R}. R^^n)"
   apply (cases k)
    apply force
-  using relpow_finite_bounded1[OF assms, of k]
-  apply auto
+  apply (use relpow_finite_bounded1[OF assms, of k] in auto)
   done
 
 lemma rtrancl_finite_eq_relpow: "finite R \<Longrightarrow> R\<^sup>* = (\<Union>n\<in>{n. n \<le> card R}. R^^n)"
@@ -1076,20 +1087,26 @@
   fixes R :: "('a \<times> 'a) set"
   assumes "finite R"
   shows "n > 0 \<Longrightarrow> finite (R^^n)"
-  apply (induct n)
-   apply simp
-  apply (case_tac n)
-   apply (simp_all add: assms)
-  done
+proof (induct n)
+  case 0
+  then show ?case by simp
+next
+  case (Suc n)
+  then show ?case by (cases n) (use assms in simp_all)
+qed
 
 lemma single_valued_relpow:
   fixes R :: "('a \<times> 'a) set"
   shows "single_valued R \<Longrightarrow> single_valued (R ^^ n)"
-  apply (induct n arbitrary: R)
-  apply simp_all
-  apply (rule single_valuedI)
-  apply (fast dest: single_valuedD elim: relpow_Suc_E)
-  done
+proof (induct n arbitrary: R)
+  case 0
+  then show ?case by simp
+next
+  case (Suc n)
+  show ?case
+    by (rule single_valuedI)
+      (use Suc in \<open>fast dest: single_valuedD elim: relpow_Suc_E\<close>)
+qed
 
 
 subsection \<open>Bounded transitive closure\<close>
@@ -1101,7 +1118,6 @@
 proof
   show "R \<subseteq> ntrancl 0 R"
     unfolding ntrancl_def by fastforce
-next
   have "0 < i \<and> i \<le> Suc 0 \<longleftrightarrow> i = 1" for i
     by auto
   then show "ntrancl 0 R \<le> R"
@@ -1110,31 +1126,30 @@
 
 lemma ntrancl_Suc [simp]: "ntrancl (Suc n) R = ntrancl n R O (Id \<union> R)"
 proof
-  {
-    fix a b
-    assume "(a, b) \<in> ntrancl (Suc n) R"
-    from this obtain i where "0 < i" "i \<le> Suc (Suc n)" "(a, b) \<in> R ^^ i"
+  have "(a, b) \<in> ntrancl n R O (Id \<union> R)" if "(a, b) \<in> ntrancl (Suc n) R" for a b
+  proof -
+    from that obtain i where "0 < i" "i \<le> Suc (Suc n)" "(a, b) \<in> R ^^ i"
       unfolding ntrancl_def by auto
-    have "(a, b) \<in> ntrancl n R O (Id \<union> R)"
+    show ?thesis
     proof (cases "i = 1")
       case True
       from this \<open>(a, b) \<in> R ^^ i\<close> show ?thesis
-        unfolding ntrancl_def by auto
+        by (auto simp: ntrancl_def)
     next
       case False
-      from this \<open>0 < i\<close> obtain j where j: "i = Suc j" "0 < j"
+      with \<open>0 < i\<close> obtain j where j: "i = Suc j" "0 < j"
         by (cases i) auto
-      from this \<open>(a, b) \<in> R ^^ i\<close> obtain c where c1: "(a, c) \<in> R ^^ j" and c2:"(c, b) \<in> R"
+      with \<open>(a, b) \<in> R ^^ i\<close> obtain c where c1: "(a, c) \<in> R ^^ j" and c2: "(c, b) \<in> R"
         by auto
       from c1 j \<open>i \<le> Suc (Suc n)\<close> have "(a, c) \<in> ntrancl n R"
-        unfolding ntrancl_def by fastforce
-      from this c2 show ?thesis by fastforce
+        by (fastforce simp: ntrancl_def)
+      with c2 show ?thesis by fastforce
     qed
-  }
+  qed
   then show "ntrancl (Suc n) R \<subseteq> ntrancl n R O (Id \<union> R)"
     by auto
   show "ntrancl n R O (Id \<union> R) \<subseteq> ntrancl (Suc n) R"
-    unfolding ntrancl_def by fastforce
+    by (fastforce simp: ntrancl_def)
 qed
 
 lemma [code]: "ntrancl (Suc n) r = (let r' = ntrancl n r in r' \<union> r' O r)"
@@ -1169,9 +1184,7 @@
 qed
 
 lemma acyclic_insert [iff]: "acyclic (insert (y, x) r) \<longleftrightarrow> acyclic r \<and> (x, y) \<notin> r\<^sup>*"
-  apply (simp add: acyclic_def trancl_insert)
-  apply (blast intro: rtrancl_trans)
-  done
+  by (simp add: acyclic_def trancl_insert) (blast intro: rtrancl_trans)
 
 lemma acyclic_converse [iff]: "acyclic (r\<inverse>) \<longleftrightarrow> acyclic r"
   by (simp add: acyclic_def trancl_converse)
@@ -1179,9 +1192,8 @@
 lemmas acyclicP_converse [iff] = acyclic_converse [to_pred]
 
 lemma acyclic_impl_antisym_rtrancl: "acyclic r \<Longrightarrow> antisym (r\<^sup>*)"
-  apply (simp add: acyclic_def antisym_def)
-  apply (blast elim: rtranclE intro: rtrancl_into_trancl1 rtrancl_trancl_trancl)
-  done
+  by (simp add: acyclic_def antisym_def)
+    (blast elim: rtranclE intro: rtrancl_into_trancl1 rtrancl_trancl_trancl)
 
 (* Other direction:
 acyclic = no loops
@@ -1197,7 +1209,6 @@
 subsection \<open>Setup of transitivity reasoner\<close>
 
 ML \<open>
-
 structure Trancl_Tac = Trancl_Tac
 (
   val r_into_trancl = @{thm trancl.r_into_trancl};
diff -r fb63942e470e -r 7195acc2fe93 src/HOL/Wellfounded.thy
--- a/src/HOL/Wellfounded.thy	Fri Aug 05 16:36:03 2016 +0200
+++ b/src/HOL/Wellfounded.thy	Fri Aug 05 18:14:28 2016 +0200
@@ -187,9 +187,7 @@
 text \<open>Well-foundedness of subsets\<close>
 
 lemma wf_subset: "wf r \<Longrightarrow> p \<subseteq> r \<Longrightarrow> wf p"
-  apply (simp add: wf_eq_minimal)
-  apply fast
-  done
+  by (simp add: wf_eq_minimal) fast
 
 lemmas wfP_subset = wf_subset [to_pred]
 
@@ -198,11 +196,12 @@
 lemma wf_empty [iff]: "wf {}"
   by (simp add: wf_def)
 
-lemma wfP_empty [iff]:
-  "wfP (\<lambda>x y. False)"
+lemma wfP_empty [iff]: "wfP (\<lambda>x y. False)"
 proof -
-  have "wfP bot" by (fact wf_empty [to_pred bot_empty_eq2])
-  then show ?thesis by (simp add: bot_fun_def)
+  have "wfP bot"
+    by (fact wf_empty [to_pred bot_empty_eq2])
+  then show ?thesis
+    by (simp add: bot_fun_def)
 qed
 
 lemma wf_Int1: "wf r \<Longrightarrow> wf (r \<inter> r')"
@@ -217,9 +216,10 @@
   shows "wf R"
 proof (rule wfI_pf)
   fix A assume "A \<subseteq> R `` A"
-  then have "A \<subseteq> (R ^^ n) `` A" by (induct n) force+
-  with \<open>wf (R ^^ n)\<close>
-  show "A = {}" by (rule wfE_pf)
+  then have "A \<subseteq> (R ^^ n) `` A"
+    by (induct n) force+
+  with \<open>wf (R ^^ n)\<close> show "A = {}"
+    by (rule wfE_pf)
 qed
 
 text \<open>Well-foundedness of \<open>insert\<close>.\<close>
@@ -257,7 +257,7 @@
   apply (case_tac "\<exists>p. f p \<in> Q")
    apply (erule_tac x = "{p. f p \<in> Q}" in allE)
    apply (fast dest: inj_onD)
-apply blast
+  apply blast
   done
 
 
@@ -379,7 +379,7 @@
   qed
 qed
 
-lemma wf_comp_self: "wf R = wf (R O R)"  \<comment> \<open>special case\<close>
+lemma wf_comp_self: "wf R \<longleftrightarrow> wf (R O R)"  \<comment> \<open>special case\<close>
   by (rule wf_union_merge [where S = "{}", simplified])
 
 
@@ -390,12 +390,13 @@
 lemma qc_wf_relto_iff:
   assumes "R O S \<subseteq> (R \<union> S)\<^sup>* O R" \<comment> \<open>R quasi-commutes over S\<close>
   shows "wf (S\<^sup>* O R O S\<^sup>*) \<longleftrightarrow> wf R"
-  (is "wf ?S \<longleftrightarrow> _")
+    (is "wf ?S \<longleftrightarrow> _")
 proof
   show "wf R" if "wf ?S"
   proof -
     have "R \<subseteq> ?S" by auto
-    with that show "wf R" using wf_subset by auto
+    with wf_subset [of ?S] that show "wf R"
+      by auto
   qed
 next
   show "wf ?S" if "wf R"
@@ -607,10 +608,7 @@
 qed
 
 lemma accp_downwards_aux: "r\<^sup>*\<^sup>* b a \<Longrightarrow> accp r a \<longrightarrow> accp r b"
-  apply (erule rtranclp_induct)
-   apply blast
-  apply (blast dest: accp_downward)
-  done
+  by (erule rtranclp_induct) (blast dest: accp_downward)+
 
 theorem accp_downwards: "accp r a \<Longrightarrow> r\<^sup>*\<^sup>* b a \<Longrightarrow> accp r b"
   by (blast dest: accp_downwards_aux)
@@ -691,7 +689,7 @@
 text \<open>Inverse Image\<close>
 
 lemma wf_inv_image [simp,intro!]: "wf r \<Longrightarrow> wf (inv_image r f)"
- for f :: "'a \<Rightarrow> 'b"
+  for f :: "'a \<Rightarrow> 'b"
   apply (simp add: inv_image_def wf_eq_minimal)
   apply clarify
   apply (subgoal_tac "\<exists>w::'b. w \<in> {w. \<exists>x::'a. x \<in> Q \<and> f x = w}")
@@ -776,7 +774,7 @@
   done
 
 lemma trans_finite_psubset: "trans finite_psubset"
-  by (auto simp add: finite_psubset_def less_le trans_def)
+  by (auto simp: finite_psubset_def less_le trans_def)
 
 lemma in_finite_psubset[simp]: "(A, B) \<in> finite_psubset \<longleftrightarrow> A \<subset> B \<and> finite B"
   unfolding finite_psubset_def by auto