misc tuning and modernization;

--- a/src/HOL/Fun.thy	Tue Jul 05 22:47:48 2016 +0200
+++ b/src/HOL/Fun.thy	Tue Jul 05 23:39:49 2016 +0200
@@ -21,6 +21,7 @@
 lemma b_uniq_choice: "\<forall>x\<in>S. \<exists>!y. Q x y \<Longrightarrow> \<exists>f. \<forall>x\<in>S. Q x (f x)"
   by (force intro: theI')
 
+
 subsection \<open>The Identity Function \<open>id\<close>\<close>
 
 definition id :: "'a \<Rightarrow> 'a"
@@ -283,9 +284,8 @@
   shows "inj f"
   \<comment> \<open>Courtesy of Stephan Merz\<close>
 proof (rule inj_onI)
-  fix x y
-  assume f_eq: "f x = f y"
-  show "x = y" by (rule linorder_cases) (auto dest: hyp simp: f_eq)
+  show "x = y" if "f x = f y" for x y
+   by (rule linorder_cases) (auto dest: hyp simp: that)
 qed
 
 lemma surj_def: "surj f \<longleftrightarrow> (\<forall>y. \<exists>x. y = f x)"
@@ -427,9 +427,8 @@
   by (auto simp add: bij_betw_def)
 
 lemma bij_betw_combine:
-  assumes "bij_betw f A B" "bij_betw f C D" "B \<inter> D = {}"
-  shows "bij_betw f (A \<union> C) (B \<union> D)"
-  using assms unfolding bij_betw_def inj_on_Un image_Un by auto
+  "bij_betw f A B \<Longrightarrow> bij_betw f C D \<Longrightarrow> B \<inter> D = {} \<Longrightarrow> bij_betw f (A \<union> C) (B \<union> D)"
+  unfolding bij_betw_def inj_on_Un image_Un by auto
 
 lemma bij_betw_subset: "bij_betw f A A' \<Longrightarrow> B \<le> A \<Longrightarrow> f ` B = B' \<Longrightarrow> bij_betw f B B'"
   by (auto simp add: bij_betw_def inj_on_def)
@@ -531,14 +530,15 @@
     and img2: "f' ` A' \<le> A"
   shows "bij_betw f A A'"
   using assms
-proof (unfold bij_betw_def inj_on_def, safe)
+  unfolding bij_betw_def inj_on_def
+proof safe
   fix a b
   assume *: "a \<in> A" "b \<in> A" and **: "f a = f b"
   have "a = f' (f a) \<and> b = f'(f b)" using * left by simp
   with ** show "a = b" by simp
 next
   fix a' assume *: "a' \<in> A'"
-  hence "f' a' \<in> A" using img2 by blast
+  then have "f' a' \<in> A" using img2 by blast
   moreover
   have "a' = f (f' a')" using * right by simp
   ultimately show "a' \<in> f ` A" by blast
@@ -823,7 +823,7 @@
 
 subsubsection \<open>Proof tools\<close>
 
-text \<open>Simplify terms of the form f(...,x:=y,...,x:=z,...) to f(...,x:=z,...)\<close>
+text \<open>Simplify terms of the form \<open>f(\<dots>,x:=y,\<dots>,x:=z,\<dots>)\<close> to \<open>f(\<dots>,x:=z,\<dots>)\<close>\<close>
 
 simproc_setup fun_upd2 ("f(v := w, x := y)") = \<open>fn _ =>
   let
@@ -843,14 +843,14 @@
       let
         val t = Thm.term_of ct
       in
-        case find_double t of
+        (case find_double t of
           (T, NONE) => NONE
         | (T, SOME rhs) =>
             SOME (Goal.prove ctxt [] [] (Logic.mk_equals (t, rhs))
               (fn _ =>
                 resolve_tac ctxt [eq_reflection] 1 THEN
                 resolve_tac ctxt @{thms ext} 1 THEN
-                simp_tac (put_simpset ss ctxt) 1))
+                simp_tac (put_simpset ss ctxt) 1)))
       end
   in proc end
 \<close>

--- a/src/HOL/Inductive.thy	Tue Jul 05 22:47:48 2016 +0200
+++ b/src/HOL/Inductive.thy	Tue Jul 05 23:39:49 2016 +0200
@@ -19,48 +19,45 @@
 context complete_lattice
 begin
 
-definition
-  lfp :: "('a \<Rightarrow> 'a) \<Rightarrow> 'a" where
-  "lfp f = Inf {u. f u \<le> u}"    \<comment>\<open>least fixed point\<close>
+definition lfp :: "('a \<Rightarrow> 'a) \<Rightarrow> 'a"  \<comment> \<open>least fixed point\<close>
+  where "lfp f = Inf {u. f u \<le> u}"
 
-definition
-  gfp :: "('a \<Rightarrow> 'a) \<Rightarrow> 'a" where
-  "gfp f = Sup {u. u \<le> f u}"    \<comment>\<open>greatest fixed point\<close>
+definition gfp :: "('a \<Rightarrow> 'a) \<Rightarrow> 'a"  \<comment> \<open>greatest fixed point\<close>
+  where "gfp f = Sup {u. u \<le> f u}"
 
 
-subsection\<open>Proof of Knaster-Tarski Theorem using @{term lfp}\<close>
+subsection \<open>Proof of Knaster-Tarski Theorem using @{term lfp}\<close>
 
-text\<open>@{term "lfp f"} is the least upper bound of
-      the set @{term "{u. f(u) \<le> u}"}\<close>
+text \<open>@{term "lfp f"} is the least upper bound of the set @{term "{u. f u \<le> u}"}\<close>
 
-lemma lfp_lowerbound: "f A \<le> A ==> lfp f \<le> A"
+lemma lfp_lowerbound: "f A \<le> A \<Longrightarrow> lfp f \<le> A"
   by (auto simp add: lfp_def intro: Inf_lower)
 
-lemma lfp_greatest: "(!!u. f u \<le> u ==> A \<le> u) ==> A \<le> lfp f"
+lemma lfp_greatest: "(\<And>u. f u \<le> u \<Longrightarrow> A \<le> u) \<Longrightarrow> A \<le> lfp f"
   by (auto simp add: lfp_def intro: Inf_greatest)
 
 end
 
-lemma lfp_lemma2: "mono f ==> f (lfp f) \<le> lfp f"
+lemma lfp_lemma2: "mono f \<Longrightarrow> f (lfp f) \<le> lfp f"
   by (iprover intro: lfp_greatest order_trans monoD lfp_lowerbound)
 
-lemma lfp_lemma3: "mono f ==> lfp f \<le> f (lfp f)"
+lemma lfp_lemma3: "mono f \<Longrightarrow> lfp f \<le> f (lfp f)"
   by (iprover intro: lfp_lemma2 monoD lfp_lowerbound)
 
-lemma lfp_unfold: "mono f ==> lfp f = f (lfp f)"
+lemma lfp_unfold: "mono f \<Longrightarrow> lfp f = f (lfp f)"
   by (iprover intro: order_antisym lfp_lemma2 lfp_lemma3)
 
 lemma lfp_const: "lfp (\<lambda>x. t) = t"
-  by (rule lfp_unfold) (simp add:mono_def)
+  by (rule lfp_unfold) (simp add: mono_def)
 
 
 subsection \<open>General induction rules for least fixed points\<close>
 
-lemma lfp_ordinal_induct[case_names mono step union]:
+lemma lfp_ordinal_induct [case_names mono step union]:
   fixes f :: "'a::complete_lattice \<Rightarrow> 'a"
   assumes mono: "mono f"
-  and P_f: "\<And>S. P S \<Longrightarrow> S \<le> lfp f \<Longrightarrow> P (f S)"
-  and P_Union: "\<And>M. \<forall>S\<in>M. P S \<Longrightarrow> P (Sup M)"
+    and P_f: "\<And>S. P S \<Longrightarrow> S \<le> lfp f \<Longrightarrow> P (f S)"
+    and P_Union: "\<And>M. \<forall>S\<in>M. P S \<Longrightarrow> P (Sup M)"
   shows "P (lfp f)"
 proof -
   let ?M = "{S. S \<le> lfp f \<and> P S}"
@@ -68,96 +65,94 @@
   also have "Sup ?M = lfp f"
   proof (rule antisym)
     show "Sup ?M \<le> lfp f" by (blast intro: Sup_least)
-    hence "f (Sup ?M) \<le> f (lfp f)" by (rule mono [THEN monoD])
-    hence "f (Sup ?M) \<le> lfp f" using mono [THEN lfp_unfold] by simp
-    hence "f (Sup ?M) \<in> ?M" using P_Union by simp (intro P_f Sup_least, auto)
-    hence "f (Sup ?M) \<le> Sup ?M" by (rule Sup_upper)
-    thus "lfp f \<le> Sup ?M" by (rule lfp_lowerbound)
+    then have "f (Sup ?M) \<le> f (lfp f)"
+      by (rule mono [THEN monoD])
+    then have "f (Sup ?M) \<le> lfp f"
+      using mono [THEN lfp_unfold] by simp
+    then have "f (Sup ?M) \<in> ?M"
+      using P_Union by simp (intro P_f Sup_least, auto)
+    then have "f (Sup ?M) \<le> Sup ?M"
+      by (rule Sup_upper)
+    then show "lfp f \<le> Sup ?M"
+      by (rule lfp_lowerbound)
   qed
   finally show ?thesis .
-qed 
+qed
 
 theorem lfp_induct:
-  assumes mono: "mono f" and ind: "f (inf (lfp f) P) \<le> P"
+  assumes mono: "mono f"
+    and ind: "f (inf (lfp f) P) \<le> P"
   shows "lfp f \<le> P"
 proof (induction rule: lfp_ordinal_induct)
-  case (step S) then show ?case
+  case (step S)
+  then show ?case
     by (intro order_trans[OF _ ind] monoD[OF mono]) auto
 qed (auto intro: mono Sup_least)
 
 lemma lfp_induct_set:
-  assumes lfp: "a: lfp(f)"
-    and mono: "mono(f)"
-    and indhyp: "!!x. [| x: f(lfp(f) Int {x. P(x)}) |] ==> P(x)"
-  shows "P(a)"
-  by (rule lfp_induct [THEN subsetD, THEN CollectD, OF mono _ lfp])
-     (auto simp: intro: indhyp)
+  assumes lfp: "a \<in> lfp f"
+    and mono: "mono f"
+    and hyp: "\<And>x. x \<in> f (lfp f \<inter> {x. P x}) \<Longrightarrow> P x"
+  shows "P a"
+  by (rule lfp_induct [THEN subsetD, THEN CollectD, OF mono _ lfp]) (auto intro: hyp)
 
-lemma lfp_ordinal_induct_set: 
+lemma lfp_ordinal_induct_set:
   assumes mono: "mono f"
-    and P_f: "!!S. P S ==> P(f S)"
-    and P_Union: "!!M. !S:M. P S ==> P (\<Union>M)"
-  shows "P(lfp f)"
+    and P_f: "\<And>S. P S \<Longrightarrow> P (f S)"
+    and P_Union: "\<And>M. \<forall>S\<in>M. P S \<Longrightarrow> P (\<Union>M)"
+  shows "P (lfp f)"
   using assms by (rule lfp_ordinal_induct)
 
 
-text\<open>Definition forms of \<open>lfp_unfold\<close> and \<open>lfp_induct\<close>, 
-    to control unfolding\<close>
+text \<open>Definition forms of \<open>lfp_unfold\<close> and \<open>lfp_induct\<close>, to control unfolding.\<close>
 
-lemma def_lfp_unfold: "[| h==lfp(f);  mono(f) |] ==> h = f(h)"
+lemma def_lfp_unfold: "h \<equiv> lfp f \<Longrightarrow> mono f \<Longrightarrow> h = f h"
   by (auto intro!: lfp_unfold)
 
-lemma def_lfp_induct: 
-    "[| A == lfp(f); mono(f);
-        f (inf A P) \<le> P
-     |] ==> A \<le> P"
+lemma def_lfp_induct: "A \<equiv> lfp f \<Longrightarrow> mono f \<Longrightarrow> f (inf A P) \<le> P \<Longrightarrow> A \<le> P"
   by (blast intro: lfp_induct)
 
-lemma def_lfp_induct_set: 
-    "[| A == lfp(f);  mono(f);   a:A;                    
-        !!x. [| x: f(A Int {x. P(x)}) |] ==> P(x)         
-     |] ==> P(a)"
+lemma def_lfp_induct_set:
+  "A \<equiv> lfp f \<Longrightarrow> mono f \<Longrightarrow> a \<in> A \<Longrightarrow> (\<And>x. x \<in> f (A \<inter> {x. P x}) \<Longrightarrow> P x) \<Longrightarrow> P a"
   by (blast intro: lfp_induct_set)
 
-(*Monotonicity of lfp!*)
-lemma lfp_mono: "(!!Z. f Z \<le> g Z) ==> lfp f \<le> lfp g"
-  by (rule lfp_lowerbound [THEN lfp_greatest], blast intro: order_trans)
+text \<open>Monotonicity of \<open>lfp\<close>!\<close>
+lemma lfp_mono: "(\<And>Z. f Z \<le> g Z) \<Longrightarrow> lfp f \<le> lfp g"
+  by (rule lfp_lowerbound [THEN lfp_greatest]) (blast intro: order_trans)
 
 
-subsection \<open>Proof of Knaster-Tarski Theorem using @{term gfp}\<close>
+subsection \<open>Proof of Knaster-Tarski Theorem using \<open>gfp\<close>\<close>
 
-text\<open>@{term "gfp f"} is the greatest lower bound of 
-      the set @{term "{u. u \<le> f(u)}"}\<close>
+text \<open>@{term "gfp f"} is the greatest lower bound of the set @{term "{u. u \<le> f u}"}\<close>
 
-lemma gfp_upperbound: "X \<le> f X ==> X \<le> gfp f"
+lemma gfp_upperbound: "X \<le> f X \<Longrightarrow> X \<le> gfp f"
   by (auto simp add: gfp_def intro: Sup_upper)
 
-lemma gfp_least: "(!!u. u \<le> f u ==> u \<le> X) ==> gfp f \<le> X"
+lemma gfp_least: "(\<And>u. u \<le> f u \<Longrightarrow> u \<le> X) \<Longrightarrow> gfp f \<le> X"
   by (auto simp add: gfp_def intro: Sup_least)
 
-lemma gfp_lemma2: "mono f ==> gfp f \<le> f (gfp f)"
+lemma gfp_lemma2: "mono f \<Longrightarrow> gfp f \<le> f (gfp f)"
   by (iprover intro: gfp_least order_trans monoD gfp_upperbound)
 
-lemma gfp_lemma3: "mono f ==> f (gfp f) \<le> gfp f"
+lemma gfp_lemma3: "mono f \<Longrightarrow> f (gfp f) \<le> gfp f"
   by (iprover intro: gfp_lemma2 monoD gfp_upperbound)
 
-lemma gfp_unfold: "mono f ==> gfp f = f (gfp f)"
+lemma gfp_unfold: "mono f \<Longrightarrow> gfp f = f (gfp f)"
   by (iprover intro: order_antisym gfp_lemma2 gfp_lemma3)
 
 
 subsection \<open>Coinduction rules for greatest fixed points\<close>
 
-text\<open>weak version\<close>
-lemma weak_coinduct: "[| a: X;  X \<subseteq> f(X) |] ==> a : gfp(f)"
+text \<open>Weak version.\<close>
+lemma weak_coinduct: "a \<in> X \<Longrightarrow> X \<subseteq> f X \<Longrightarrow> a \<in> gfp f"
   by (rule gfp_upperbound [THEN subsetD]) auto
 
-lemma weak_coinduct_image: "!!X. [| a : X; g`X \<subseteq> f (g`X) |] ==> g a : gfp f"
+lemma weak_coinduct_image: "a \<in> X \<Longrightarrow> g`X \<subseteq> f (g`X) \<Longrightarrow> g a \<in> gfp f"
   apply (erule gfp_upperbound [THEN subsetD])
   apply (erule imageI)
   done
 
-lemma coinduct_lemma:
-     "[| X \<le> f (sup X (gfp f));  mono f |] ==> sup X (gfp f) \<le> f (sup X (gfp f))"
+lemma coinduct_lemma: "X \<le> f (sup X (gfp f)) \<Longrightarrow> mono f \<Longrightarrow> sup X (gfp f) \<le> f (sup X (gfp f))"
   apply (frule gfp_lemma2)
   apply (drule mono_sup)
   apply (rule le_supI)
@@ -169,112 +164,113 @@
   apply assumption
   done
 
-text\<open>strong version, thanks to Coen and Frost\<close>
-lemma coinduct_set: "[| mono(f);  a: X;  X \<subseteq> f(X Un gfp(f)) |] ==> a : gfp(f)"
+text \<open>Strong version, thanks to Coen and Frost.\<close>
+lemma coinduct_set: "mono f \<Longrightarrow> a \<in> X \<Longrightarrow> X \<subseteq> f (X \<union> gfp f) \<Longrightarrow> a \<in> gfp f"
   by (rule weak_coinduct[rotated], rule coinduct_lemma) blast+
 
-lemma gfp_fun_UnI2: "[| mono(f);  a: gfp(f) |] ==> a: f(X Un gfp(f))"
+lemma gfp_fun_UnI2: "mono f \<Longrightarrow> a \<in> gfp f \<Longrightarrow> a \<in> f (X \<union> gfp f)"
   by (blast dest: gfp_lemma2 mono_Un)
 
 lemma gfp_ordinal_induct[case_names mono step union]:
   fixes f :: "'a::complete_lattice \<Rightarrow> 'a"
   assumes mono: "mono f"
-  and P_f: "\<And>S. P S \<Longrightarrow> gfp f \<le> S \<Longrightarrow> P (f S)"
-  and P_Union: "\<And>M. \<forall>S\<in>M. P S \<Longrightarrow> P (Inf M)"
+    and P_f: "\<And>S. P S \<Longrightarrow> gfp f \<le> S \<Longrightarrow> P (f S)"
+    and P_Union: "\<And>M. \<forall>S\<in>M. P S \<Longrightarrow> P (Inf M)"
   shows "P (gfp f)"
 proof -
   let ?M = "{S. gfp f \<le> S \<and> P S}"
   have "P (Inf ?M)" using P_Union by simp
   also have "Inf ?M = gfp f"
   proof (rule antisym)
-    show "gfp f \<le> Inf ?M" by (blast intro: Inf_greatest)
-    hence "f (gfp f) \<le> f (Inf ?M)" by (rule mono [THEN monoD])
-    hence "gfp f \<le> f (Inf ?M)" using mono [THEN gfp_unfold] by simp
-    hence "f (Inf ?M) \<in> ?M" using P_Union by simp (intro P_f Inf_greatest, auto)
-    hence "Inf ?M \<le> f (Inf ?M)" by (rule Inf_lower)
-    thus "Inf ?M \<le> gfp f" by (rule gfp_upperbound)
+    show "gfp f \<le> Inf ?M"
+      by (blast intro: Inf_greatest)
+    then have "f (gfp f) \<le> f (Inf ?M)"
+      by (rule mono [THEN monoD])
+    then have "gfp f \<le> f (Inf ?M)"
+      using mono [THEN gfp_unfold] by simp
+    then have "f (Inf ?M) \<in> ?M"
+      using P_Union by simp (intro P_f Inf_greatest, auto)
+    then have "Inf ?M \<le> f (Inf ?M)"
+      by (rule Inf_lower)
+    then show "Inf ?M \<le> gfp f"
+      by (rule gfp_upperbound)
   qed
   finally show ?thesis .
-qed 
+qed
 
-lemma coinduct: assumes mono: "mono f" and ind: "X \<le> f (sup X (gfp f))" shows "X \<le> gfp f"
+lemma coinduct:
+  assumes mono: "mono f"
+    and ind: "X \<le> f (sup X (gfp f))"
+  shows "X \<le> gfp f"
 proof (induction rule: gfp_ordinal_induct)
   case (step S) then show ?case
     by (intro order_trans[OF ind _] monoD[OF mono]) auto
 qed (auto intro: mono Inf_greatest)
 
+
 subsection \<open>Even Stronger Coinduction Rule, by Martin Coen\<close>
 
-text\<open>Weakens the condition @{term "X \<subseteq> f(X)"} to one expressed using both
+text \<open>Weakens the condition @{term "X \<subseteq> f X"} to one expressed using both
   @{term lfp} and @{term gfp}\<close>
-
-lemma coinduct3_mono_lemma: "mono(f) ==> mono(%x. f(x) Un X Un B)"
-by (iprover intro: subset_refl monoI Un_mono monoD)
+lemma coinduct3_mono_lemma: "mono f \<Longrightarrow> mono (\<lambda>x. f x \<union> X \<union> B)"
+  by (iprover intro: subset_refl monoI Un_mono monoD)
 
 lemma coinduct3_lemma:
-     "[| X \<subseteq> f(lfp(%x. f(x) Un X Un gfp(f)));  mono(f) |]
-      ==> lfp(%x. f(x) Un X Un gfp(f)) \<subseteq> f(lfp(%x. f(x) Un X Un gfp(f)))"
-apply (rule subset_trans)
-apply (erule coinduct3_mono_lemma [THEN lfp_lemma3])
-apply (rule Un_least [THEN Un_least])
-apply (rule subset_refl, assumption)
-apply (rule gfp_unfold [THEN equalityD1, THEN subset_trans], assumption)
-apply (rule monoD, assumption)
-apply (subst coinduct3_mono_lemma [THEN lfp_unfold], auto)
-done
+  "X \<subseteq> f (lfp (\<lambda>x. f x \<union> X \<union> gfp f)) \<Longrightarrow> mono f \<Longrightarrow>
+    lfp (\<lambda>x. f x \<union> X \<union> gfp f) \<subseteq> f (lfp (\<lambda>x. f x \<union> X \<union> gfp f))"
+  apply (rule subset_trans)
+  apply (erule coinduct3_mono_lemma [THEN lfp_lemma3])
+  apply (rule Un_least [THEN Un_least])
+  apply (rule subset_refl, assumption)
+  apply (rule gfp_unfold [THEN equalityD1, THEN subset_trans], assumption)
+  apply (rule monoD, assumption)
+  apply (subst coinduct3_mono_lemma [THEN lfp_unfold], auto)
+  done
 
-lemma coinduct3: 
-  "[| mono(f);  a:X;  X \<subseteq> f(lfp(%x. f(x) Un X Un gfp(f))) |] ==> a : gfp(f)"
-apply (rule coinduct3_lemma [THEN [2] weak_coinduct])
-apply (rule coinduct3_mono_lemma [THEN lfp_unfold, THEN ssubst])
-apply (simp_all)
-done
+lemma coinduct3: "mono f \<Longrightarrow> a \<in> X \<Longrightarrow> X \<subseteq> f (lfp (\<lambda>x. f x \<union> X \<union> gfp f)) \<Longrightarrow> a \<in> gfp f"
+  apply (rule coinduct3_lemma [THEN [2] weak_coinduct])
+  apply (rule coinduct3_mono_lemma [THEN lfp_unfold, THEN ssubst])
+  apply simp_all
+  done
 
-text\<open>Definition forms of \<open>gfp_unfold\<close> and \<open>coinduct\<close>, 
-    to control unfolding\<close>
+text  \<open>Definition forms of \<open>gfp_unfold\<close> and \<open>coinduct\<close>, to control unfolding.\<close>
 
-lemma def_gfp_unfold: "[| A==gfp(f);  mono(f) |] ==> A = f(A)"
+lemma def_gfp_unfold: "A \<equiv> gfp f \<Longrightarrow> mono f \<Longrightarrow> A = f A"
   by (auto intro!: gfp_unfold)
 
-lemma def_coinduct:
-     "[| A==gfp(f);  mono(f);  X \<le> f(sup X A) |] ==> X \<le> A"
+lemma def_coinduct: "A \<equiv> gfp f \<Longrightarrow> mono f \<Longrightarrow> X \<le> f (sup X A) \<Longrightarrow> X \<le> A"
   by (iprover intro!: coinduct)
 
-lemma def_coinduct_set:
-     "[| A==gfp(f);  mono(f);  a:X;  X \<subseteq> f(X Un A) |] ==> a: A"
+lemma def_coinduct_set: "A \<equiv> gfp f \<Longrightarrow> mono f \<Longrightarrow> a \<in> X \<Longrightarrow> X \<subseteq> f (X \<union> A) \<Longrightarrow> a \<in> A"
   by (auto intro!: coinduct_set)
 
-(*The version used in the induction/coinduction package*)
 lemma def_Collect_coinduct:
-    "[| A == gfp(%w. Collect(P(w)));  mono(%w. Collect(P(w)));   
-        a: X;  !!z. z: X ==> P (X Un A) z |] ==>  
-     a : A"
+  "A \<equiv> gfp (\<lambda>w. Collect (P w)) \<Longrightarrow> mono (\<lambda>w. Collect (P w)) \<Longrightarrow> a \<in> X \<Longrightarrow>
+    (\<And>z. z \<in> X \<Longrightarrow> P (X \<union> A) z) \<Longrightarrow> a \<in> A"
   by (erule def_coinduct_set) auto
 
-lemma def_coinduct3:
-    "[| A==gfp(f); mono(f);  a:X;  X \<subseteq> f(lfp(%x. f(x) Un X Un A)) |] ==> a: A"
+lemma def_coinduct3: "A \<equiv> gfp f \<Longrightarrow> mono f \<Longrightarrow> a \<in> X \<Longrightarrow> X \<subseteq> f (lfp (\<lambda>x. f x \<union> X \<union> A)) \<Longrightarrow> a \<in> A"
   by (auto intro!: coinduct3)
 
-text\<open>Monotonicity of @{term gfp}!\<close>
-lemma gfp_mono: "(!!Z. f Z \<le> g Z) ==> gfp f \<le> gfp g"
-  by (rule gfp_upperbound [THEN gfp_least], blast intro: order_trans)
+text \<open>Monotonicity of @{term gfp}!\<close>
+lemma gfp_mono: "(\<And>Z. f Z \<le> g Z) \<Longrightarrow> gfp f \<le> gfp g"
+  by (rule gfp_upperbound [THEN gfp_least]) (blast intro: order_trans)
+
 
 subsection \<open>Rules for fixed point calculus\<close>
 
-
 lemma lfp_rolling:
   assumes "mono g" "mono f"
   shows "g (lfp (\<lambda>x. f (g x))) = lfp (\<lambda>x. g (f x))"
 proof (rule antisym)
   have *: "mono (\<lambda>x. f (g x))"
     using assms by (auto simp: mono_def)
-
   show "lfp (\<lambda>x. g (f x)) \<le> g (lfp (\<lambda>x. f (g x)))"
     by (rule lfp_lowerbound) (simp add: lfp_unfold[OF *, symmetric])
-
   show "g (lfp (\<lambda>x. f (g x))) \<le> lfp (\<lambda>x. g (f x))"
   proof (rule lfp_greatest)
-    fix u assume "g (f u) \<le> u"
+    fix u
+    assume "g (f u) \<le> u"
     moreover then have "g (lfp (\<lambda>x. f (g x))) \<le> g (f u)"
       by (intro assms[THEN monoD] lfp_lowerbound)
     ultimately show "g (lfp (\<lambda>x. f (g x))) \<le> u"
@@ -309,7 +305,6 @@
     using assms by (auto simp: mono_def)
   show "g (gfp (\<lambda>x. f (g x))) \<le> gfp (\<lambda>x. g (f x))"
     by (rule gfp_upperbound) (simp add: gfp_unfold[OF *, symmetric])
-
   show "gfp (\<lambda>x. g (f x)) \<le> g (gfp (\<lambda>x. f (g x)))"
   proof (rule gfp_least)
     fix u assume "u \<le> g (f u)"
@@ -339,6 +334,7 @@
   qed
 qed
 
+
 subsection \<open>Inductive predicates and sets\<close>
 
 text \<open>Package setup.\<close>

--- a/src/HOL/Product_Type.thy	Tue Jul 05 22:47:48 2016 +0200
+++ b/src/HOL/Product_Type.thy	Tue Jul 05 23:39:49 2016 +0200
@@ -37,12 +37,11 @@
 declare case_split [cases type: bool]
   \<comment> "prefer plain propositional version"
 
-lemma
-  shows [code]: "HOL.equal False P \<longleftrightarrow> \<not> P"
-    and [code]: "HOL.equal True P \<longleftrightarrow> P" 
-    and [code]: "HOL.equal P False \<longleftrightarrow> \<not> P"
-    and [code]: "HOL.equal P True \<longleftrightarrow> P"
-    and [code nbe]: "HOL.equal P P \<longleftrightarrow> True"
+lemma [code]: "HOL.equal False P \<longleftrightarrow> \<not> P"
+  and [code]: "HOL.equal True P \<longleftrightarrow> P" 
+  and [code]: "HOL.equal P False \<longleftrightarrow> \<not> P"
+  and [code]: "HOL.equal P True \<longleftrightarrow> P"
+  and [code nbe]: "HOL.equal P P \<longleftrightarrow> True"
   by (simp_all add: equal)
 
 lemma If_case_cert:
@@ -101,23 +100,23 @@
 
 setup \<open>Sign.parent_path\<close>
 
-lemma unit_all_eq1: "(!!x::unit. PROP P x) == PROP P ()"
+lemma unit_all_eq1: "(\<And>x::unit. PROP P x) \<equiv> PROP P ()"
   by simp
 
-lemma unit_all_eq2: "(!!x::unit. PROP P) == PROP P"
+lemma unit_all_eq2: "(\<And>x::unit. PROP P) \<equiv> PROP P"
   by (rule triv_forall_equality)
 
 text \<open>
   This rewrite counters the effect of simproc \<open>unit_eq\<close> on @{term
-  [source] "%u::unit. f u"}, replacing it by @{term [source]
-  f} rather than by @{term [source] "%u. f ()"}.
+  [source] "\<lambda>u::unit. f u"}, replacing it by @{term [source]
+  f} rather than by @{term [source] "\<lambda>u. f ()"}.
 \<close>
 
-lemma unit_abs_eta_conv [simp]: "(%u::unit. f ()) = f"
+lemma unit_abs_eta_conv [simp]: "(\<lambda>u::unit. f ()) = f"
   by (rule ext) simp
 
-lemma UNIV_unit:
-  "UNIV = {()}" by auto
+lemma UNIV_unit: "UNIV = {()}"
+  by auto
 
 instantiation unit :: default
 begin
@@ -128,52 +127,41 @@
 
 end
 
-instantiation unit :: "{complete_boolean_algebra, complete_linorder, wellorder}"
+instantiation unit :: "{complete_boolean_algebra,complete_linorder,wellorder}"
 begin
 
 definition less_eq_unit :: "unit \<Rightarrow> unit \<Rightarrow> bool"
-where
-  "(_::unit) \<le> _ \<longleftrightarrow> True"
+  where "(_::unit) \<le> _ \<longleftrightarrow> True"
 
-lemma less_eq_unit [iff]:
-  "(u::unit) \<le> v"
+lemma less_eq_unit [iff]: "u \<le> v" for u v :: unit
   by (simp add: less_eq_unit_def)
 
 definition less_unit :: "unit \<Rightarrow> unit \<Rightarrow> bool"
-where
-  "(_::unit) < _ \<longleftrightarrow> False"
+  where "(_::unit) < _ \<longleftrightarrow> False"
 
-lemma less_unit [iff]:
-  "\<not> (u::unit) < v"
+lemma less_unit [iff]: "\<not> u < v" for u v :: unit
   by (simp_all add: less_eq_unit_def less_unit_def)
 
 definition bot_unit :: unit
-where
-  [code_unfold]: "\<bottom> = ()"
+  where [code_unfold]: "\<bottom> = ()"
 
 definition top_unit :: unit
-where
-  [code_unfold]: "\<top> = ()"
+  where [code_unfold]: "\<top> = ()"
 
 definition inf_unit :: "unit \<Rightarrow> unit \<Rightarrow> unit"
-where
-  [simp]: "_ \<sqinter> _ = ()"
+  where [simp]: "_ \<sqinter> _ = ()"
 
 definition sup_unit :: "unit \<Rightarrow> unit \<Rightarrow> unit"
-where
-  [simp]: "_ \<squnion> _ = ()"
+  where [simp]: "_ \<squnion> _ = ()"
 
 definition Inf_unit :: "unit set \<Rightarrow> unit"
-where
-  [simp]: "\<Sqinter>_ = ()"
+  where [simp]: "\<Sqinter>_ = ()"
 
 definition Sup_unit :: "unit set \<Rightarrow> unit"
-where
-  [simp]: "\<Squnion>_ = ()"
+  where [simp]: "\<Squnion>_ = ()"
 
 definition uminus_unit :: "unit \<Rightarrow> unit"
-where
-  [simp]: "- _ = ()"
+  where [simp]: "- _ = ()"
 
 declare less_eq_unit_def [abs_def, code_unfold]
   less_unit_def [abs_def, code_unfold]
@@ -188,8 +176,8 @@
 
 end
 
-lemma [code]:
-  "HOL.equal (u::unit) v \<longleftrightarrow> True" unfolding equal unit_eq [of u] unit_eq [of v] by rule+
+lemma [code]: "HOL.equal u v \<longleftrightarrow> True" for u v :: unit
+  unfolding equal unit_eq [of u] unit_eq [of v] by rule+
 
 code_printing
   type_constructor unit \<rightharpoonup>
@@ -221,8 +209,8 @@
 
 subsubsection \<open>Type definition\<close>
 
-definition Pair_Rep :: "'a \<Rightarrow> 'b \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> bool" where
-  "Pair_Rep a b = (\<lambda>x y. x = a \<and> y = b)"
+definition Pair_Rep :: "'a \<Rightarrow> 'b \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> bool"
+  where "Pair_Rep a b = (\<lambda>x y. x = a \<and> y = b)"
 
 definition "prod = {f. \<exists>a b. f = Pair_Rep (a::'a) (b::'b)}"
 
@@ -232,8 +220,8 @@
 type_notation (ASCII)
   prod  (infixr "*" 20)
 
-definition Pair :: "'a \<Rightarrow> 'b \<Rightarrow> 'a \<times> 'b" where
-  "Pair a b = Abs_prod (Pair_Rep a b)"
+definition Pair :: "'a \<Rightarrow> 'b \<Rightarrow> 'a \<times> 'b"
+  where "Pair a b = Abs_prod (Pair_Rep a b)"
 
 lemma prod_cases: "(\<And>a b. P (Pair a b)) \<Longrightarrow> P p"
   by (cases p) (auto simp add: prod_def Pair_def Pair_Rep_def)
@@ -258,7 +246,7 @@
 setup \<open>Sign.mandatory_path "old"\<close>
 
 old_rep_datatype Pair
-by (erule prod_cases) (rule prod.inject)
+  by (erule prod_cases) (rule prod.inject)
 
 setup \<open>Sign.parent_path\<close>
 
@@ -297,16 +285,14 @@
 \<close>
 
 nonterminal tuple_args and patterns
-
 syntax
-  "_tuple"      :: "'a => tuple_args => 'a * 'b"        ("(1'(_,/ _'))")
-  "_tuple_arg"  :: "'a => tuple_args"                   ("_")
-  "_tuple_args" :: "'a => tuple_args => tuple_args"     ("_,/ _")
-  "_pattern"    :: "[pttrn, patterns] => pttrn"         ("'(_,/ _')")
-  ""            :: "pttrn => patterns"                  ("_")
-  "_patterns"   :: "[pttrn, patterns] => patterns"      ("_,/ _")
+  "_tuple"      :: "'a \<Rightarrow> tuple_args \<Rightarrow> 'a \<times> 'b"        ("(1'(_,/ _'))")
+  "_tuple_arg"  :: "'a \<Rightarrow> tuple_args"                   ("_")
+  "_tuple_args" :: "'a \<Rightarrow> tuple_args \<Rightarrow> tuple_args"     ("_,/ _")
+  "_pattern"    :: "pttrn \<Rightarrow> patterns \<Rightarrow> pttrn"         ("'(_,/ _')")
+  ""            :: "pttrn \<Rightarrow> patterns"                  ("_")
+  "_patterns"   :: "pttrn \<Rightarrow> patterns \<Rightarrow> patterns"      ("_,/ _")
   "_unit"       :: pttrn                                ("'(')")
-
 translations
   "(x, y)" \<rightleftharpoons> "CONST Pair x y"
   "_pattern x y" \<rightleftharpoons> "CONST Pair x y"
@@ -356,9 +342,9 @@
   in [(@{const_syntax case_prod}, K case_prod_guess_names_tr')] end
 \<close>
 
-text \<open>reconstruct pattern from (nested) @{const case_prod}s,
+text \<open>Reconstruct pattern from (nested) @{const case_prod}s,
   avoiding eta-contraction of body; required for enclosing "let",
-  if "let" does not avoid eta-contraction, which has been observed to occur\<close>
+  if "let" does not avoid eta-contraction, which has been observed to occur.\<close>
 
 print_translation \<open>
   let
@@ -421,19 +407,16 @@
 
 subsubsection \<open>Fundamental operations and properties\<close>
 
-lemma Pair_inject:
-  assumes "(a, b) = (a', b')"
-    and "a = a' \<Longrightarrow> b = b' \<Longrightarrow> R"
-  shows R
-  using assms by simp
+lemma Pair_inject: "(a, b) = (a', b') \<Longrightarrow> (a = a' \<Longrightarrow> b = b' \<Longrightarrow> R) \<Longrightarrow> R"
+  by simp
 
-lemma surj_pair [simp]: "EX x y. p = (x, y)"
+lemma surj_pair [simp]: "\<exists>x y. p = (x, y)"
   by (cases p) simp
 
-lemma fst_eqD: "fst (x, y) = a ==> x = a"
+lemma fst_eqD: "fst (x, y) = a \<Longrightarrow> x = a"
   by simp
 
-lemma snd_eqD: "snd (x, y) = a ==> y = a"
+lemma snd_eqD: "snd (x, y) = a \<Longrightarrow> y = a"
   by simp
 
 lemma case_prod_unfold [nitpick_unfold]: "case_prod = (\<lambda>c p. c (fst p) (snd p))"
@@ -469,25 +452,25 @@
 lemma The_case_prod: "The (case_prod P) = (THE xy. P (fst xy) (snd xy))"
   by (simp add: case_prod_unfold)
 
-lemma cond_case_prod_eta: "(!!x y. f x y = g (x, y)) ==> (%(x, y). f x y) = g"
+lemma cond_case_prod_eta: "(\<And>x y. f x y = g (x, y)) \<Longrightarrow> (\<lambda>(x, y). f x y) = g"
   by (simp add: case_prod_eta)
 
-lemma split_paired_all [no_atp]: "(!!x. PROP P x) == (!!a b. PROP P (a, b))"
+lemma split_paired_all [no_atp]: "(\<And>x. PROP P x) \<equiv> (\<And>a b. PROP P (a, b))"
 proof
   fix a b
-  assume "!!x. PROP P x"
+  assume "\<And>x. PROP P x"
   then show "PROP P (a, b)" .
 next
   fix x
-  assume "!!a b. PROP P (a, b)"
+  assume "\<And>a b. PROP P (a, b)"
   from \<open>PROP P (fst x, snd x)\<close> show "PROP P x" by simp
 qed
 
 text \<open>
   The rule @{thm [source] split_paired_all} does not work with the
   Simplifier because it also affects premises in congrence rules,
-  where this can lead to premises of the form \<open>!!a b. ... =
-  ?P(a, b)\<close> which cannot be solved by reflexivity.
+  where this can lead to premises of the form \<open>\<And>a b. \<dots> = ?P(a, b)\<close>
+  which cannot be solved by reflexivity.
 \<close>
 
 lemmas split_tupled_all = split_paired_all unit_all_eq2
@@ -520,11 +503,11 @@
 
 setup \<open>map_theory_claset (fn ctxt => ctxt addSbefore ("split_all_tac", split_all_tac))\<close>
 
-lemma split_paired_All [simp, no_atp]: "(ALL x. P x) = (ALL a b. P (a, b))"
+lemma split_paired_All [simp, no_atp]: "(\<forall>x. P x) \<longleftrightarrow> (\<forall>a b. P (a, b))"
   \<comment> \<open>\<open>[iff]\<close> is not a good idea because it makes \<open>blast\<close> loop\<close>
   by fast
 
-lemma split_paired_Ex [simp, no_atp]: "(EX x. P x) = (EX a b. P (a, b))"
+lemma split_paired_Ex [simp, no_atp]: "(\<exists>x. P x) \<longleftrightarrow> (\<exists>a b. P (a, b))"
   by fast
 
 lemma split_paired_The [no_atp]: "(THE x. P x) = (THE (a, b). P (a, b))"
@@ -590,9 +573,9 @@
   by (auto simp: fun_eq_iff)
 
 text \<open>
-  \medskip @{const case_prod} used as a logical connective or set former.
+  \<^medskip> @{const case_prod} used as a logical connective or set former.
 
-  \medskip These rules are for use with \<open>blast\<close>; could instead
+  \<^medskip> These rules are for use with \<open>blast\<close>; could instead
   call \<open>simp\<close> using @{thm [source] prod.split} as rewrite.\<close>
 
 lemma case_prodI2:
@@ -621,12 +604,10 @@
     using q by (simp add: case_prod_unfold)
 qed
 
-lemma case_prodD':
-  "(case (a, b) of (c, d) \<Rightarrow> R c d) c \<Longrightarrow> R a b c"
+lemma case_prodD': "(case (a, b) of (c, d) \<Rightarrow> R c d) c \<Longrightarrow> R a b c"
   by simp
 
-lemma mem_case_prodI:
-  "z \<in> c a b \<Longrightarrow> z \<in> (case (a, b) of (d, e) \<Rightarrow> c d e)"
+lemma mem_case_prodI: "z \<in> c a b \<Longrightarrow> z \<in> (case (a, b) of (d, e) \<Rightarrow> c d e)"
   by simp
 
 lemma mem_case_prodI2 [intro!]:
@@ -661,13 +642,13 @@
    to quite time-consuming computations (in particular for nested tuples) *)
 setup \<open>map_theory_claset (fn ctxt => ctxt addSbefore ("split_conv_tac", split_conv_tac))\<close>
 
-lemma split_eta_SetCompr [simp, no_atp]: "(%u. EX x y. u = (x, y) & P (x, y)) = P"
+lemma split_eta_SetCompr [simp, no_atp]: "(\<lambda>u. \<exists>x y. u = (x, y) \<and> P (x, y)) = P"
   by (rule ext) fast
 
-lemma split_eta_SetCompr2 [simp, no_atp]: "(%u. EX x y. u = (x, y) & P x y) = case_prod P"
+lemma split_eta_SetCompr2 [simp, no_atp]: "(\<lambda>u. \<exists>x y. u = (x, y) \<and> P x y) = case_prod P"
   by (rule ext) fast
 
-lemma split_part [simp]: "(%(a,b). P & Q a b) = (%ab. P & case_prod Q ab)"
+lemma split_part [simp]: "(\<lambda>(a,b). P \<and> Q a b) = (\<lambda>ab. P \<and> case_prod Q ab)"
   \<comment> \<open>Allows simplifications of nested splits in case of independent predicates.\<close>
   by (rule ext) blast
 
@@ -676,16 +657,15 @@
    b) can lead to nontermination in the presence of split_def
 *)
 lemma split_comp_eq: 
-  fixes f :: "'a => 'b => 'c" and g :: "'d => 'a"
-  shows "(%u. f (g (fst u)) (snd u)) = (case_prod (%x. f (g x)))"
+  fixes f :: "'a \<Rightarrow> 'b \<Rightarrow> 'c"
+    and g :: "'d \<Rightarrow> 'a"
+  shows "(\<lambda>u. f (g (fst u)) (snd u)) = case_prod (\<lambda>x. f (g x))"
   by (rule ext) auto
 
-lemma pair_imageI [intro]: "(a, b) : A ==> f a b : (%(a, b). f a b) ` A"
-  apply (rule_tac x = "(a, b)" in image_eqI)
-   apply auto
-  done
+lemma pair_imageI [intro]: "(a, b) \<in> A \<Longrightarrow> f a b \<in> (\<lambda>(a, b). f a b) ` A"
+  by (rule image_eqI [where x = "(a, b)"]) auto
 
-lemma The_split_eq [simp]: "(THE (x',y'). x = x' & y = y') = (x, y)"
+lemma The_split_eq [simp]: "(THE (x',y'). x = x' \<and> y = y') = (x, y)"
   by blast
 
 (*
@@ -701,8 +681,7 @@
 qed "The_split_eq";
 *)
 
-lemma case_prod_beta:
-  "case_prod f p = f (fst p) (snd p)"
+lemma case_prod_beta: "case_prod f p = f (fst p) (snd p)"
   by (fact prod.case_eq_if)
 
 lemma prod_cases3 [cases type]:
@@ -710,7 +689,7 @@
   by (cases y, case_tac b) blast
 
 lemma prod_induct3 [case_names fields, induct type]:
-    "(!!a b c. P (a, b, c)) ==> P x"
+  "(\<And>a b c. P (a, b, c)) \<Longrightarrow> P x"
   by (cases x) blast
 
 lemma prod_cases4 [cases type]:
@@ -718,7 +697,7 @@
   by (cases y, case_tac c) blast
 
 lemma prod_induct4 [case_names fields, induct type]:
-    "(!!a b c d. P (a, b, c, d)) ==> P x"
+  "(\<And>a b c d. P (a, b, c, d)) \<Longrightarrow> P x"
   by (cases x) blast
 
 lemma prod_cases5 [cases type]:
@@ -726,7 +705,7 @@
   by (cases y, case_tac d) blast
 
 lemma prod_induct5 [case_names fields, induct type]:
-    "(!!a b c d e. P (a, b, c, d, e)) ==> P x"
+  "(\<And>a b c d e. P (a, b, c, d, e)) \<Longrightarrow> P x"
   by (cases x) blast
 
 lemma prod_cases6 [cases type]:
@@ -734,7 +713,7 @@
   by (cases y, case_tac e) blast
 
 lemma prod_induct6 [case_names fields, induct type]:
-    "(!!a b c d e f. P (a, b, c, d, e, f)) ==> P x"
+  "(\<And>a b c d e f. P (a, b, c, d, e, f)) \<Longrightarrow> P x"
   by (cases x) blast
 
 lemma prod_cases7 [cases type]:
@@ -742,11 +721,11 @@
   by (cases y, case_tac f) blast
 
 lemma prod_induct7 [case_names fields, induct type]:
-    "(!!a b c d e f g. P (a, b, c, d, e, f, g)) ==> P x"
+  "(\<And>a b c d e f g. P (a, b, c, d, e, f, g)) \<Longrightarrow> P x"
   by (cases x) blast
 
-definition internal_case_prod :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'a \<times> 'b \<Rightarrow> 'c" where
-  "internal_case_prod == case_prod"
+definition internal_case_prod :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'a \<times> 'b \<Rightarrow> 'c"
+  where "internal_case_prod \<equiv> case_prod"
 
 lemma internal_case_prod_conv: "internal_case_prod c (a, b) = c a b"
   by (simp only: internal_case_prod_def case_prod_conv)
@@ -758,8 +737,8 @@
 
 subsubsection \<open>Derived operations\<close>
 
-definition curry :: "('a \<times> 'b \<Rightarrow> 'c) \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'c" where
-  "curry = (\<lambda>c x y. c (x, y))"
+definition curry :: "('a \<times> 'b \<Rightarrow> 'c) \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'c"
+  where "curry = (\<lambda>c x y. c (x, y))"
 
 lemma curry_conv [simp, code]: "curry f a b = f (a, b)"
   by (simp add: curry_def)
@@ -780,16 +759,14 @@
   by (simp add: curry_def case_prod_unfold)
 
 lemma curry_K: "curry (\<lambda>x. c) = (\<lambda>x y. c)"
-by(simp add: fun_eq_iff)
+  by (simp add: fun_eq_iff)
 
-text \<open>
-  The composition-uncurry combinator.
-\<close>
+text \<open>The composition-uncurry combinator.\<close>
 
 notation fcomp (infixl "\<circ>>" 60)
 
-definition scomp :: "('a \<Rightarrow> 'b \<times> 'c) \<Rightarrow> ('b \<Rightarrow> 'c \<Rightarrow> 'd) \<Rightarrow> 'a \<Rightarrow> 'd" (infixl "\<circ>\<rightarrow>" 60) where
-  "f \<circ>\<rightarrow> g = (\<lambda>x. case_prod g (f x))"
+definition scomp :: "('a \<Rightarrow> 'b \<times> 'c) \<Rightarrow> ('b \<Rightarrow> 'c \<Rightarrow> 'd) \<Rightarrow> 'a \<Rightarrow> 'd"  (infixl "\<circ>\<rightarrow>" 60)
+  where "f \<circ>\<rightarrow> g = (\<lambda>x. case_prod g (f x))"
 
 lemma scomp_unfold: "scomp = (\<lambda>f g x. g (fst (f x)) (snd (f x)))"
   by (simp add: fun_eq_iff scomp_def case_prod_unfold)
@@ -819,46 +796,37 @@
 no_notation scomp (infixl "\<circ>\<rightarrow>" 60)
 
 text \<open>
-  @{term map_prod} --- action of the product functor upon
-  functions.
+  @{term map_prod} --- action of the product functor upon functions.
 \<close>
 
-definition map_prod :: "('a \<Rightarrow> 'c) \<Rightarrow> ('b \<Rightarrow> 'd) \<Rightarrow> 'a \<times> 'b \<Rightarrow> 'c \<times> 'd" where
-  "map_prod f g = (\<lambda>(x, y). (f x, g y))"
+definition map_prod :: "('a \<Rightarrow> 'c) \<Rightarrow> ('b \<Rightarrow> 'd) \<Rightarrow> 'a \<times> 'b \<Rightarrow> 'c \<times> 'd"
+  where "map_prod f g = (\<lambda>(x, y). (f x, g y))"
 
-lemma map_prod_simp [simp, code]:
-  "map_prod f g (a, b) = (f a, g b)"
+lemma map_prod_simp [simp, code]: "map_prod f g (a, b) = (f a, g b)"
   by (simp add: map_prod_def)
 
 functor map_prod: map_prod
   by (auto simp add: split_paired_all)
 
-lemma fst_map_prod [simp]:
-  "fst (map_prod f g x) = f (fst x)"
+lemma fst_map_prod [simp]: "fst (map_prod f g x) = f (fst x)"
   by (cases x) simp_all
 
-lemma snd_map_prod [simp]:
-  "snd (map_prod f g x) = g (snd x)"
+lemma snd_map_prod [simp]: "snd (map_prod f g x) = g (snd x)"
   by (cases x) simp_all
 
-lemma fst_comp_map_prod [simp]:
-  "fst \<circ> map_prod f g = f \<circ> fst"
+lemma fst_comp_map_prod [simp]: "fst \<circ> map_prod f g = f \<circ> fst"
   by (rule ext) simp_all
 
-lemma snd_comp_map_prod [simp]:
-  "snd \<circ> map_prod f g = g \<circ> snd"
+lemma snd_comp_map_prod [simp]: "snd \<circ> map_prod f g = g \<circ> snd"
   by (rule ext) simp_all
 
-lemma map_prod_compose:
-  "map_prod (f1 o f2) (g1 o g2) = (map_prod f1 g1 o map_prod f2 g2)"
+lemma map_prod_compose: "map_prod (f1 \<circ> f2) (g1 \<circ> g2) = (map_prod f1 g1 \<circ> map_prod f2 g2)"
   by (rule ext) (simp add: map_prod.compositionality comp_def)
 
-lemma map_prod_ident [simp]:
-  "map_prod (%x. x) (%y. y) = (%z. z)"
+lemma map_prod_ident [simp]: "map_prod (\<lambda>x. x) (\<lambda>y. y) = (\<lambda>z. z)"
   by (rule ext) (simp add: map_prod.identity)
 
-lemma map_prod_imageI [intro]:
-  "(a, b) \<in> R \<Longrightarrow> (f a, g b) \<in> map_prod f g ` R"
+lemma map_prod_imageI [intro]: "(a, b) \<in> R \<Longrightarrow> (f a, g b) \<in> map_prod f g ` R"
   by (rule image_eqI) simp_all
 
 lemma prod_fun_imageE [elim!]:
@@ -871,86 +839,67 @@
   apply simp_all
   done
 
-definition apfst :: "('a \<Rightarrow> 'c) \<Rightarrow> 'a \<times> 'b \<Rightarrow> 'c \<times> 'b" where
-  "apfst f = map_prod f id"
+definition apfst :: "('a \<Rightarrow> 'c) \<Rightarrow> 'a \<times> 'b \<Rightarrow> 'c \<times> 'b"
+  where "apfst f = map_prod f id"
 
-definition apsnd :: "('b \<Rightarrow> 'c) \<Rightarrow> 'a \<times> 'b \<Rightarrow> 'a \<times> 'c" where
-  "apsnd f = map_prod id f"
+definition apsnd :: "('b \<Rightarrow> 'c) \<Rightarrow> 'a \<times> 'b \<Rightarrow> 'a \<times> 'c"
+  where "apsnd f = map_prod id f"
 
-lemma apfst_conv [simp, code]:
-  "apfst f (x, y) = (f x, y)" 
+lemma apfst_conv [simp, code]: "apfst f (x, y) = (f x, y)" 
   by (simp add: apfst_def)
 
-lemma apsnd_conv [simp, code]:
-  "apsnd f (x, y) = (x, f y)" 
+lemma apsnd_conv [simp, code]: "apsnd f (x, y) = (x, f y)" 
   by (simp add: apsnd_def)
 
-lemma fst_apfst [simp]:
-  "fst (apfst f x) = f (fst x)"
+lemma fst_apfst [simp]: "fst (apfst f x) = f (fst x)"
   by (cases x) simp
 
-lemma fst_comp_apfst [simp]:
-  "fst \<circ> apfst f = f \<circ> fst"
+lemma fst_comp_apfst [simp]: "fst \<circ> apfst f = f \<circ> fst"
   by (simp add: fun_eq_iff)
 
-lemma fst_apsnd [simp]:
-  "fst (apsnd f x) = fst x"
+lemma fst_apsnd [simp]: "fst (apsnd f x) = fst x"
   by (cases x) simp
 
-lemma fst_comp_apsnd [simp]:
-  "fst \<circ> apsnd f = fst"
+lemma fst_comp_apsnd [simp]: "fst \<circ> apsnd f = fst"
   by (simp add: fun_eq_iff)
 
-lemma snd_apfst [simp]:
-  "snd (apfst f x) = snd x"
+lemma snd_apfst [simp]: "snd (apfst f x) = snd x"
   by (cases x) simp
 
-lemma snd_comp_apfst [simp]:
-  "snd \<circ> apfst f = snd"
+lemma snd_comp_apfst [simp]: "snd \<circ> apfst f = snd"
   by (simp add: fun_eq_iff)
 
-lemma snd_apsnd [simp]:
-  "snd (apsnd f x) = f (snd x)"
+lemma snd_apsnd [simp]: "snd (apsnd f x) = f (snd x)"
   by (cases x) simp
 
-lemma snd_comp_apsnd [simp]:
-  "snd \<circ> apsnd f = f \<circ> snd"
+lemma snd_comp_apsnd [simp]: "snd \<circ> apsnd f = f \<circ> snd"
   by (simp add: fun_eq_iff)
 
-lemma apfst_compose:
-  "apfst f (apfst g x) = apfst (f \<circ> g) x"
+lemma apfst_compose: "apfst f (apfst g x) = apfst (f \<circ> g) x"
   by (cases x) simp
 
-lemma apsnd_compose:
-  "apsnd f (apsnd g x) = apsnd (f \<circ> g) x"
+lemma apsnd_compose: "apsnd f (apsnd g x) = apsnd (f \<circ> g) x"
   by (cases x) simp
 
-lemma apfst_apsnd [simp]:
-  "apfst f (apsnd g x) = (f (fst x), g (snd x))"
+lemma apfst_apsnd [simp]: "apfst f (apsnd g x) = (f (fst x), g (snd x))"
   by (cases x) simp
 
-lemma apsnd_apfst [simp]:
-  "apsnd f (apfst g x) = (g (fst x), f (snd x))"
+lemma apsnd_apfst [simp]: "apsnd f (apfst g x) = (g (fst x), f (snd x))"
   by (cases x) simp
 
-lemma apfst_id [simp] :
-  "apfst id = id"
+lemma apfst_id [simp]: "apfst id = id"
   by (simp add: fun_eq_iff)
 
-lemma apsnd_id [simp] :
-  "apsnd id = id"
+lemma apsnd_id [simp]: "apsnd id = id"
   by (simp add: fun_eq_iff)
 
-lemma apfst_eq_conv [simp]:
-  "apfst f x = apfst g x \<longleftrightarrow> f (fst x) = g (fst x)"
+lemma apfst_eq_conv [simp]: "apfst f x = apfst g x \<longleftrightarrow> f (fst x) = g (fst x)"
   by (cases x) simp
 
-lemma apsnd_eq_conv [simp]:
-  "apsnd f x = apsnd g x \<longleftrightarrow> f (snd x) = g (snd x)"
+lemma apsnd_eq_conv [simp]: "apsnd f x = apsnd g x \<longleftrightarrow> f (snd x) = g (snd x)"
   by (cases x) simp
 
-lemma apsnd_apfst_commute:
-  "apsnd f (apfst g p) = apfst g (apsnd f p)"
+lemma apsnd_apfst_commute: "apsnd f (apfst g p) = apfst g (apsnd f p)"
   by simp
 
 context
@@ -959,104 +908,83 @@
 local_setup \<open>Local_Theory.map_background_naming (Name_Space.mandatory_path "prod")\<close>
 
 definition swap :: "'a \<times> 'b \<Rightarrow> 'b \<times> 'a"
-where
-  "swap p = (snd p, fst p)"
+  where "swap p = (snd p, fst p)"
 
 end
 
-lemma swap_simp [simp]:
-  "prod.swap (x, y) = (y, x)"
+lemma swap_simp [simp]: "prod.swap (x, y) = (y, x)"
   by (simp add: prod.swap_def)
 
-lemma swap_swap [simp]:
-  "prod.swap (prod.swap p) = p"
+lemma swap_swap [simp]: "prod.swap (prod.swap p) = p"
   by (cases p) simp
 
-lemma swap_comp_swap [simp]:
-  "prod.swap \<circ> prod.swap = id"
+lemma swap_comp_swap [simp]: "prod.swap \<circ> prod.swap = id"
   by (simp add: fun_eq_iff)
 
-lemma pair_in_swap_image [simp]:
-  "(y, x) \<in> prod.swap ` A \<longleftrightarrow> (x, y) \<in> A"
+lemma pair_in_swap_image [simp]: "(y, x) \<in> prod.swap ` A \<longleftrightarrow> (x, y) \<in> A"
   by (auto intro!: image_eqI)
 
-lemma inj_swap [simp]:
-  "inj_on prod.swap A"
+lemma inj_swap [simp]: "inj_on prod.swap A"
   by (rule inj_onI) auto
 
-lemma swap_inj_on:
-  "inj_on (\<lambda>(i, j). (j, i)) A"
+lemma swap_inj_on: "inj_on (\<lambda>(i, j). (j, i)) A"
   by (rule inj_onI) auto
 
-lemma surj_swap [simp]:
-  "surj prod.swap"
+lemma surj_swap [simp]: "surj prod.swap"
   by (rule surjI [of _ prod.swap]) simp
 
-lemma bij_swap [simp]:
-  "bij prod.swap"
+lemma bij_swap [simp]: "bij prod.swap"
   by (simp add: bij_def)
 
-lemma case_swap [simp]:
-  "(case prod.swap p of (y, x) \<Rightarrow> f x y) = (case p of (x, y) \<Rightarrow> f x y)"
+lemma case_swap [simp]: "(case prod.swap p of (y, x) \<Rightarrow> f x y) = (case p of (x, y) \<Rightarrow> f x y)"
   by (cases p) simp
 
 lemma fst_swap [simp]: "fst (prod.swap x) = snd x"
-by(cases x) simp
+  by (cases x) simp
 
 lemma snd_swap [simp]: "snd (prod.swap x) = fst x"
-by(cases x) simp
+  by (cases x) simp
 
-text \<open>
-  Disjoint union of a family of sets -- Sigma.
-\<close>
+text \<open>Disjoint union of a family of sets -- Sigma.\<close>
 
-definition Sigma :: "'a set \<Rightarrow> ('a \<Rightarrow> 'b set) \<Rightarrow> ('a \<times> 'b) set" where
-  Sigma_def: "Sigma A B == UN x:A. UN y:B x. {Pair x y}"
+definition Sigma :: "'a set \<Rightarrow> ('a \<Rightarrow> 'b set) \<Rightarrow> ('a \<times> 'b) set"
+  where "Sigma A B \<equiv> \<Union>x\<in>A. \<Union>y\<in>B x. {Pair x y}"
 
-abbreviation
-  Times :: "'a set \<Rightarrow> 'b set \<Rightarrow> ('a \<times> 'b) set"  (infixr "\<times>" 80) where
-  "A \<times> B == Sigma A (%_. B)"
+abbreviation Times :: "'a set \<Rightarrow> 'b set \<Rightarrow> ('a \<times> 'b) set"  (infixr "\<times>" 80)
+  where "A \<times> B \<equiv> Sigma A (\<lambda>_. B)"
 
 hide_const (open) Times
 
 syntax
-  "_Sigma" :: "[pttrn, 'a set, 'b set] => ('a * 'b) set"  ("(3SIGMA _:_./ _)" [0, 0, 10] 10)
+  "_Sigma" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b set \<Rightarrow> ('a \<times> 'b) set"  ("(3SIGMA _:_./ _)" [0, 0, 10] 10)
 translations
-  "SIGMA x:A. B" == "CONST Sigma A (%x. B)"
-
-lemma SigmaI [intro!]: "[| a:A;  b:B(a) |] ==> (a,b) : Sigma A B"
-  by (unfold Sigma_def) blast
+  "SIGMA x:A. B" \<rightleftharpoons> "CONST Sigma A (\<lambda>x. B)"
 
-lemma SigmaE [elim!]:
-    "[| c: Sigma A B;
-        !!x y.[| x:A;  y:B(x);  c=(x,y) |] ==> P
-     |] ==> P"
+lemma SigmaI [intro!]: "a \<in> A \<Longrightarrow> b \<in> B a \<Longrightarrow> (a, b) \<in> Sigma A B"
+  unfolding Sigma_def by blast
+
+lemma SigmaE [elim!]: "c \<in> Sigma A B \<Longrightarrow> (\<And>x y. x \<in> A \<Longrightarrow> y \<in> B x \<Longrightarrow> c = (x, y) \<Longrightarrow> P) \<Longrightarrow> P"
   \<comment> \<open>The general elimination rule.\<close>
-  by (unfold Sigma_def) blast
+  unfolding Sigma_def by blast
 
 text \<open>
-  Elimination of @{term "(a, b) : A \<times> B"} -- introduces no
+  Elimination of @{term "(a, b) \<in> A \<times> B"} -- introduces no
   eigenvariables.
 \<close>
 
-lemma SigmaD1: "(a, b) : Sigma A B ==> a : A"
+lemma SigmaD1: "(a, b) \<in> Sigma A B \<Longrightarrow> a \<in> A"
   by blast
 
-lemma SigmaD2: "(a, b) : Sigma A B ==> b : B a"
+lemma SigmaD2: "(a, b) \<in> Sigma A B \<Longrightarrow> b \<in> B a"
   by blast
 
-lemma SigmaE2:
-    "[| (a, b) : Sigma A B;
-        [| a:A;  b:B(a) |] ==> P
-     |] ==> P"
+lemma SigmaE2: "(a, b) \<in> Sigma A B \<Longrightarrow> (a \<in> A \<Longrightarrow> b \<in> B a \<Longrightarrow> P) \<Longrightarrow> P"
   by blast
 
-lemma Sigma_cong:
-     "\<lbrakk>A = B; !!x. x \<in> B \<Longrightarrow> C x = D x\<rbrakk>
-      \<Longrightarrow> (SIGMA x: A. C x) = (SIGMA x: B. D x)"
+lemma Sigma_cong: "A = B \<Longrightarrow> (\<And>x. x \<in> B \<Longrightarrow> C x = D x) \<Longrightarrow> (SIGMA x:A. C x) = (SIGMA x:B. D x)"
   by auto
 
-lemma Sigma_mono: "[| A <= C; !!x. x:A ==> B x <= D x |] ==> Sigma A B <= Sigma C D"
+lemma Sigma_mono: "A \<subseteq> C \<Longrightarrow> (\<And>x. x \<in> A \<Longrightarrow> B x \<subseteq> D x) \<Longrightarrow> Sigma A B \<subseteq> Sigma C D"
   by blast
 
 lemma Sigma_empty1 [simp]: "Sigma {} B = {}"
@@ -1074,7 +1002,7 @@
 lemma Compl_Times_UNIV2 [simp]: "- (A \<times> UNIV) = (-A) \<times> UNIV"
   by auto
 
-lemma mem_Sigma_iff [iff]: "((a,b): Sigma A B) = (a:A & b:B(a))"
+lemma mem_Sigma_iff [iff]: "(a, b) \<in> Sigma A B \<longleftrightarrow> a \<in> A \<and> b \<in> B a"
   by blast
 
 lemma mem_Times_iff: "x \<in> A \<times> B \<longleftrightarrow> fst x \<in> A \<and> snd x \<in> B"
@@ -1083,26 +1011,22 @@
 lemma Sigma_empty_iff: "(SIGMA i:I. X i) = {} \<longleftrightarrow> (\<forall>i\<in>I. X i = {})"
   by auto
 
-lemma Times_subset_cancel2: "x:C ==> (A \<times> C <= B \<times> C) = (A <= B)"
-  by blast
-
-lemma Times_eq_cancel2: "x:C ==> (A \<times> C = B \<times> C) = (A = B)"
-  by (blast elim: equalityE)
-
-lemma Collect_case_prod_Sigma:
-  "{(x, y). P x \<and> Q x y} = (SIGMA x:Collect P. Collect (Q x))"
+lemma Times_subset_cancel2: "x \<in> C \<Longrightarrow> A \<times> C \<subseteq> B \<times> C \<longleftrightarrow> A \<subseteq> B"
   by blast
 
-lemma Collect_case_prod [simp]:
-  "{(a, b). P a \<and> Q b} = Collect P \<times> Collect Q "
+lemma Times_eq_cancel2: "x \<in> C \<Longrightarrow> A \<times> C = B \<times> C \<longleftrightarrow> A = B"
+  by (blast elim: equalityE)
+
+lemma Collect_case_prod_Sigma: "{(x, y). P x \<and> Q x y} = (SIGMA x:Collect P. Collect (Q x))"
+  by blast
+
+lemma Collect_case_prod [simp]: "{(a, b). P a \<and> Q b} = Collect P \<times> Collect Q "
   by (fact Collect_case_prod_Sigma)
 
-lemma Collect_case_prodD:
-  "x \<in> Collect (case_prod A) \<Longrightarrow> A (fst x) (snd x)"
+lemma Collect_case_prodD: "x \<in> Collect (case_prod A) \<Longrightarrow> A (fst x) (snd x)"
   by auto
 
-lemma Collect_case_prod_mono:
-  "A \<le> B \<Longrightarrow> Collect (case_prod A) \<subseteq> Collect (case_prod B)"
+lemma Collect_case_prod_mono: "A \<le> B \<Longrightarrow> Collect (case_prod A) \<subseteq> Collect (case_prod B)"
   by auto (auto elim!: le_funE)
 
 lemma Collect_split_mono_strong: 
@@ -1110,45 +1034,35 @@
     \<Longrightarrow> A \<subseteq> Collect (case_prod P) \<Longrightarrow> A \<subseteq> Collect (case_prod Q)"
   by fastforce
   
-lemma UN_Times_distrib:
-  "(\<Union>(a, b)\<in>A \<times> B. E a \<times> F b) = UNION A E \<times> UNION B F"
+lemma UN_Times_distrib: "(\<Union>(a, b)\<in>A \<times> B. E a \<times> F b) = UNION A E \<times> UNION B F"
   \<comment> \<open>Suggested by Pierre Chartier\<close>
   by blast
 
-lemma split_paired_Ball_Sigma [simp, no_atp]:
-  "(\<forall>z\<in>Sigma A B. P z) \<longleftrightarrow> (\<forall>x\<in>A. \<forall>y\<in>B x. P (x, y))"
+lemma split_paired_Ball_Sigma [simp, no_atp]: "(\<forall>z\<in>Sigma A B. P z) \<longleftrightarrow> (\<forall>x\<in>A. \<forall>y\<in>B x. P (x, y))"
   by blast
 
-lemma split_paired_Bex_Sigma [simp, no_atp]:
-  "(\<exists>z\<in>Sigma A B. P z) \<longleftrightarrow> (\<exists>x\<in>A. \<exists>y\<in>B x. P (x, y))"
+lemma split_paired_Bex_Sigma [simp, no_atp]: "(\<exists>z\<in>Sigma A B. P z) \<longleftrightarrow> (\<exists>x\<in>A. \<exists>y\<in>B x. P (x, y))"
   by blast
 
-lemma Sigma_Un_distrib1:
-  "Sigma (I \<union> J) C = Sigma I C \<union> Sigma J C"
+lemma Sigma_Un_distrib1: "Sigma (I \<union> J) C = Sigma I C \<union> Sigma J C"
   by blast
 
-lemma Sigma_Un_distrib2:
-  "(SIGMA i:I. A i \<union> B i) = Sigma I A \<union> Sigma I B"
+lemma Sigma_Un_distrib2: "(SIGMA i:I. A i \<union> B i) = Sigma I A \<union> Sigma I B"
   by blast
 
-lemma Sigma_Int_distrib1:
-  "Sigma (I \<inter> J) C = Sigma I C \<inter> Sigma J C"
+lemma Sigma_Int_distrib1: "Sigma (I \<inter> J) C = Sigma I C \<inter> Sigma J C"
   by blast
 
-lemma Sigma_Int_distrib2:
-  "(SIGMA i:I. A i \<inter> B i) = Sigma I A \<inter> Sigma I B"
+lemma Sigma_Int_distrib2: "(SIGMA i:I. A i \<inter> B i) = Sigma I A \<inter> Sigma I B"
   by blast
 
-lemma Sigma_Diff_distrib1:
-  "Sigma (I - J) C = Sigma I C - Sigma J C"
+lemma Sigma_Diff_distrib1: "Sigma (I - J) C = Sigma I C - Sigma J C"
   by blast
 
-lemma Sigma_Diff_distrib2:
-  "(SIGMA i:I. A i - B i) = Sigma I A - Sigma I B"
+lemma Sigma_Diff_distrib2: "(SIGMA i:I. A i - B i) = Sigma I A - Sigma I B"
   by blast
 
-lemma Sigma_Union:
-  "Sigma (\<Union>X) B = (\<Union>A\<in>X. Sigma A B)"
+lemma Sigma_Union: "Sigma (\<Union>X) B = (\<Union>A\<in>X. Sigma A B)"
   by blast
 
 lemma Pair_vimage_Sigma: "Pair x -` Sigma A f = (if x \<in> A then f x else {})"
@@ -1159,79 +1073,62 @@
   matching, especially when the rules are re-oriented.
 \<close>
 
-lemma Times_Un_distrib1:
-  "(A \<union> B) \<times> C = A \<times> C \<union> B \<times> C "
+lemma Times_Un_distrib1: "(A \<union> B) \<times> C = A \<times> C \<union> B \<times> C "
   by (fact Sigma_Un_distrib1)
 
-lemma Times_Int_distrib1:
-  "(A \<inter> B) \<times> C = A \<times> C \<inter> B \<times> C "
+lemma Times_Int_distrib1: "(A \<inter> B) \<times> C = A \<times> C \<inter> B \<times> C "
   by (fact Sigma_Int_distrib1)
 
-lemma Times_Diff_distrib1:
-  "(A - B) \<times> C = A \<times> C - B \<times> C "
+lemma Times_Diff_distrib1: "(A - B) \<times> C = A \<times> C - B \<times> C "
   by (fact Sigma_Diff_distrib1)
 
-lemma Times_empty [simp]:
-  "A \<times> B = {} \<longleftrightarrow> A = {} \<or> B = {}"
+lemma Times_empty [simp]: "A \<times> B = {} \<longleftrightarrow> A = {} \<or> B = {}"
   by auto
 
-lemma times_eq_iff:
-  "A \<times> B = C \<times> D \<longleftrightarrow> A = C \<and> B = D \<or> (A = {} \<or> B = {}) \<and> (C = {} \<or> D = {})"
+lemma times_eq_iff: "A \<times> B = C \<times> D \<longleftrightarrow> A = C \<and> B = D \<or> (A = {} \<or> B = {}) \<and> (C = {} \<or> D = {})"
   by auto
 
-lemma fst_image_times [simp]:
-  "fst ` (A \<times> B) = (if B = {} then {} else A)"
+lemma fst_image_times [simp]: "fst ` (A \<times> B) = (if B = {} then {} else A)"
   by force
 
-lemma snd_image_times [simp]:
-  "snd ` (A \<times> B) = (if A = {} then {} else B)"
+lemma snd_image_times [simp]: "snd ` (A \<times> B) = (if A = {} then {} else B)"
   by force
 
-lemma fst_image_Sigma:
-  "fst ` (Sigma A B) = {x \<in> A. B(x) \<noteq> {}}"
+lemma fst_image_Sigma: "fst ` (Sigma A B) = {x \<in> A. B(x) \<noteq> {}}"
   by force
 
-lemma snd_image_Sigma:
-  "snd ` (Sigma A B) = (\<Union> x \<in> A. B x)"
+lemma snd_image_Sigma: "snd ` (Sigma A B) = (\<Union> x \<in> A. B x)"
   by force
 
-lemma vimage_fst:
-  "fst -` A = A \<times> UNIV"
+lemma vimage_fst: "fst -` A = A \<times> UNIV"
   by auto
 
-lemma vimage_snd:
-  "snd -` A = UNIV \<times> A"
+lemma vimage_snd: "snd -` A = UNIV \<times> A"
   by auto
 
-lemma insert_times_insert[simp]:
-  "insert a A \<times> insert b B =
-   insert (a,b) (A \<times> insert b B \<union> insert a A \<times> B)"
+lemma insert_times_insert [simp]:
+  "insert a A \<times> insert b B = insert (a,b) (A \<times> insert b B \<union> insert a A \<times> B)"
   by blast
 
-lemma vimage_Times:
-  "f -` (A \<times> B) = (fst \<circ> f) -` A \<inter> (snd \<circ> f) -` B"
+lemma vimage_Times: "f -` (A \<times> B) = (fst \<circ> f) -` A \<inter> (snd \<circ> f) -` B"
 proof (rule set_eqI)
-  fix x
-  show "x \<in> f -` (A \<times> B) \<longleftrightarrow> x \<in> (fst \<circ> f) -` A \<inter> (snd \<circ> f) -` B"
+  show "x \<in> f -` (A \<times> B) \<longleftrightarrow> x \<in> (fst \<circ> f) -` A \<inter> (snd \<circ> f) -` B" for x
     by (cases "f x") (auto split: prod.split)
 qed
 
-lemma times_Int_times:
-  "A \<times> B \<inter> C \<times> D = (A \<inter> C) \<times> (B \<inter> D)"
+lemma times_Int_times: "A \<times> B \<inter> C \<times> D = (A \<inter> C) \<times> (B \<inter> D)"
   by auto
 
-lemma product_swap:
-  "prod.swap ` (A \<times> B) = B \<times> A"
+lemma product_swap: "prod.swap ` (A \<times> B) = B \<times> A"
   by (auto simp add: set_eq_iff)
 
-lemma swap_product:
-  "(\<lambda>(i, j). (j, i)) ` (A \<times> B) = B \<times> A"
+lemma swap_product: "(\<lambda>(i, j). (j, i)) ` (A \<times> B) = B \<times> A"
   by (auto simp add: set_eq_iff)
 
-lemma image_split_eq_Sigma:
-  "(\<lambda>x. (f x, g x)) ` A = Sigma (f ` A) (\<lambda>x. g ` (f -` {x} \<inter> A))"
+lemma image_split_eq_Sigma: "(\<lambda>x. (f x, g x)) ` A = Sigma (f ` A) (\<lambda>x. g ` (f -` {x} \<inter> A))"
 proof (safe intro!: imageI)
-  fix a b assume *: "a \<in> A" "b \<in> A" and eq: "f a = f b"
+  fix a b
+  assume *: "a \<in> A" "b \<in> A" and eq: "f a = f b"
   show "(f b, g a) \<in> (\<lambda>x. (f x, g x)) ` A"
     using * eq[symmetric] by auto
 qed simp_all
@@ -1240,16 +1137,16 @@
   by force
 
 lemma inj_on_apfst [simp]: "inj_on (apfst f) (A \<times> UNIV) \<longleftrightarrow> inj_on f A"
-by(auto simp add: inj_on_def)
+  by (auto simp add: inj_on_def)
 
 lemma inj_apfst [simp]: "inj (apfst f) \<longleftrightarrow> inj f"
-using inj_on_apfst[of f UNIV] by simp
+  using inj_on_apfst[of f UNIV] by simp
 
 lemma inj_on_apsnd [simp]: "inj_on (apsnd f) (UNIV \<times> A) \<longleftrightarrow> inj_on f A"
-by(auto simp add: inj_on_def)
+  by (auto simp add: inj_on_def)
 
 lemma inj_apsnd [simp]: "inj (apsnd f) \<longleftrightarrow> inj f"
-using inj_on_apsnd[of f UNIV] by simp
+  using inj_on_apsnd[of f UNIV] by simp
 
 context
 begin
@@ -1257,9 +1154,8 @@
 qualified definition product :: "'a set \<Rightarrow> 'b set \<Rightarrow> ('a \<times> 'b) set" where
   [code_abbrev]: "product A B = A \<times> B"
 
-lemma member_product:
-  "x \<in> Product_Type.product A B \<longleftrightarrow> x \<in> A \<times> B"
-  by (simp add: Product_Type.product_def)
+lemma member_product: "x \<in> Product_Type.product A B \<longleftrightarrow> x \<in> A \<times> B"
+  by (simp add: product_def)
 
 end
   
@@ -1269,59 +1165,80 @@
   assumes "inj_on f A" and "inj_on g B"
   shows "inj_on (map_prod f g) (A \<times> B)"
 proof (rule inj_onI)
-  fix x :: "'a \<times> 'c" and y :: "'a \<times> 'c"
-  assume "x \<in> A \<times> B" hence "fst x \<in> A" and "snd x \<in> B" by auto
-  assume "y \<in> A \<times> B" hence "fst y \<in> A" and "snd y \<in> B" by auto
+  fix x :: "'a \<times> 'c"
+  fix y :: "'a \<times> 'c"
+  assume "x \<in> A \<times> B"
+  then have "fst x \<in> A" and "snd x \<in> B" by auto
+  assume "y \<in> A \<times> B"
+  then have "fst y \<in> A" and "snd y \<in> B" by auto
   assume "map_prod f g x = map_prod f g y"
-  hence "fst (map_prod f g x) = fst (map_prod f g y)" by (auto)
-  hence "f (fst x) = f (fst y)" by (cases x,cases y,auto)
-  with \<open>inj_on f A\<close> and \<open>fst x \<in> A\<close> and \<open>fst y \<in> A\<close>
-  have "fst x = fst y" by (auto dest:dest:inj_onD)
+  then have "fst (map_prod f g x) = fst (map_prod f g y)" by auto
+  then have "f (fst x) = f (fst y)" by (cases x, cases y) auto
+  with \<open>inj_on f A\<close> and \<open>fst x \<in> A\<close> and \<open>fst y \<in> A\<close> have "fst x = fst y"
+    by (auto dest: inj_onD)
   moreover from \<open>map_prod f g x = map_prod f g y\<close>
-  have "snd (map_prod f g x) = snd (map_prod f g y)" by (auto)
-  hence "g (snd x) = g (snd y)" by (cases x,cases y,auto)
-  with \<open>inj_on g B\<close> and \<open>snd x \<in> B\<close> and \<open>snd y \<in> B\<close>
-  have "snd x = snd y" by (auto dest:dest:inj_onD)
-  ultimately show "x = y" by(rule prod_eqI)
+  have "snd (map_prod f g x) = snd (map_prod f g y)" by auto
+  then have "g (snd x) = g (snd y)" by (cases x, cases y) auto
+  with \<open>inj_on g B\<close> and \<open>snd x \<in> B\<close> and \<open>snd y \<in> B\<close> have "snd x = snd y"
+    by (auto dest: inj_onD)
+  ultimately show "x = y" by (rule prod_eqI)
 qed
 
 lemma map_prod_surj:
-  fixes f :: "'a \<Rightarrow> 'b" and g :: "'c \<Rightarrow> 'd"
+  fixes f :: "'a \<Rightarrow> 'b"
+    and g :: "'c \<Rightarrow> 'd"
   assumes "surj f" and "surj g"
   shows "surj (map_prod f g)"
-unfolding surj_def
+  unfolding surj_def
 proof
   fix y :: "'b \<times> 'd"
-  from \<open>surj f\<close> obtain a where "fst y = f a" by (auto elim:surjE)
+  from \<open>surj f\<close> obtain a where "fst y = f a"
+    by (auto elim: surjE)
   moreover
-  from \<open>surj g\<close> obtain b where "snd y = g b" by (auto elim:surjE)
-  ultimately have "(fst y, snd y) = map_prod f g (a,b)" by auto
-  thus "\<exists>x. y = map_prod f g x" by auto
+  from \<open>surj g\<close> obtain b where "snd y = g b"
+    by (auto elim: surjE)
+  ultimately have "(fst y, snd y) = map_prod f g (a,b)"
+    by auto
+  then show "\<exists>x. y = map_prod f g x"
+    by auto
 qed
 
 lemma map_prod_surj_on:
   assumes "f ` A = A'" and "g ` B = B'"
   shows "map_prod f g ` (A \<times> B) = A' \<times> B'"
-unfolding image_def
-proof(rule set_eqI,rule iffI)
+  unfolding image_def
+proof (rule set_eqI, rule iffI)
   fix x :: "'a \<times> 'c"
   assume "x \<in> {y::'a \<times> 'c. \<exists>x::'b \<times> 'd\<in>A \<times> B. y = map_prod f g x}"
-  then obtain y where "y \<in> A \<times> B" and "x = map_prod f g y" by blast
-  from \<open>image f A = A'\<close> and \<open>y \<in> A \<times> B\<close> have "f (fst y) \<in> A'" by auto
-  moreover from \<open>image g B = B'\<close> and \<open>y \<in> A \<times> B\<close> have "g (snd y) \<in> B'" by auto
-  ultimately have "(f (fst y), g (snd y)) \<in> (A' \<times> B')" by auto
-  with \<open>x = map_prod f g y\<close> show "x \<in> A' \<times> B'" by (cases y, auto)
+  then obtain y where "y \<in> A \<times> B" and "x = map_prod f g y"
+    by blast
+  from \<open>image f A = A'\<close> and \<open>y \<in> A \<times> B\<close> have "f (fst y) \<in> A'"
+    by auto
+  moreover from \<open>image g B = B'\<close> and \<open>y \<in> A \<times> B\<close> have "g (snd y) \<in> B'"
+    by auto
+  ultimately have "(f (fst y), g (snd y)) \<in> (A' \<times> B')"
+    by auto
+  with \<open>x = map_prod f g y\<close> show "x \<in> A' \<times> B'"
+    by (cases y) auto
 next
   fix x :: "'a \<times> 'c"
-  assume "x \<in> A' \<times> B'" hence "fst x \<in> A'" and "snd x \<in> B'" by auto
-  from \<open>image f A = A'\<close> and \<open>fst x \<in> A'\<close> have "fst x \<in> image f A" by auto
-  then obtain a where "a \<in> A" and "fst x = f a" by (rule imageE)
-  moreover from \<open>image g B = B'\<close> and \<open>snd x \<in> B'\<close>
-  obtain b where "b \<in> B" and "snd x = g b" by auto
-  ultimately have "(fst x, snd x) = map_prod f g (a,b)" by auto
-  moreover from \<open>a \<in> A\<close> and  \<open>b \<in> B\<close> have "(a , b) \<in> A \<times> B" by auto
-  ultimately have "\<exists>y \<in> A \<times> B. x = map_prod f g y" by auto
-  thus "x \<in> {x. \<exists>y \<in> A \<times> B. x = map_prod f g y}" by auto
+  assume "x \<in> A' \<times> B'"
+  then have "fst x \<in> A'" and "snd x \<in> B'"
+    by auto
+  from \<open>image f A = A'\<close> and \<open>fst x \<in> A'\<close> have "fst x \<in> image f A"
+    by auto
+  then obtain a where "a \<in> A" and "fst x = f a"
+    by (rule imageE)
+  moreover from \<open>image g B = B'\<close> and \<open>snd x \<in> B'\<close> obtain b where "b \<in> B" and "snd x = g b"
+    by auto
+  ultimately have "(fst x, snd x) = map_prod f g (a, b)"
+    by auto
+  moreover from \<open>a \<in> A\<close> and  \<open>b \<in> B\<close> have "(a , b) \<in> A \<times> B"
+    by auto
+  ultimately have "\<exists>y \<in> A \<times> B. x = map_prod f g y"
+    by auto
+  then show "x \<in> {x. \<exists>y \<in> A \<times> B. x = map_prod f g y}"
+    by auto
 qed
 
 

--- a/src/HOL/Set.thy	Tue Jul 05 22:47:48 2016 +0200
+++ b/src/HOL/Set.thy	Tue Jul 05 23:39:49 2016 +0200
@@ -466,7 +466,7 @@
   \<comment> \<open>Classical elimination rule.\<close>
   by (auto simp add: less_eq_set_def le_fun_def)
 
-lemma subset_eq: "A \<subseteq> B = (\<forall>x\<in>A. x \<in> B)"
+lemma subset_eq: "A \<subseteq> B \<longleftrightarrow> (\<forall>x\<in>A. x \<in> B)"
   by blast
 
 lemma contra_subsetD: "A \<subseteq> B \<Longrightarrow> c \<notin> B \<Longrightarrow> c \<notin> A"

--- a/src/HOL/Sum_Type.thy	Tue Jul 05 22:47:48 2016 +0200
+++ b/src/HOL/Sum_Type.thy	Tue Jul 05 23:39:49 2016 +0200
@@ -11,15 +11,15 @@
 
 subsection \<open>Construction of the sum type and its basic abstract operations\<close>
 
-definition Inl_Rep :: "'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> bool \<Rightarrow> bool" where
-  "Inl_Rep a x y p \<longleftrightarrow> x = a \<and> p"
+definition Inl_Rep :: "'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> bool \<Rightarrow> bool"
+  where "Inl_Rep a x y p \<longleftrightarrow> x = a \<and> p"
 
-definition Inr_Rep :: "'b \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> bool \<Rightarrow> bool" where
-  "Inr_Rep b x y p \<longleftrightarrow> y = b \<and> \<not> p"
+definition Inr_Rep :: "'b \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> bool \<Rightarrow> bool"
+  where "Inr_Rep b x y p \<longleftrightarrow> y = b \<and> \<not> p"
 
 definition "sum = {f. (\<exists>a. f = Inl_Rep (a::'a)) \<or> (\<exists>b. f = Inr_Rep (b::'b))}"
 
-typedef ('a, 'b) sum (infixr "+" 10) = "sum :: ('a => 'b => bool => bool) set"
+typedef ('a, 'b) sum (infixr "+" 10) = "sum :: ('a \<Rightarrow> 'b \<Rightarrow> bool \<Rightarrow> bool) set"
   unfolding sum_def by auto
 
 lemma Inl_RepI: "Inl_Rep a \<in> sum"
@@ -46,48 +46,51 @@
 lemma Inl_Rep_not_Inr_Rep: "Inl_Rep a \<noteq> Inr_Rep b"
   by (auto simp add: Inl_Rep_def Inr_Rep_def fun_eq_iff)
 
-definition Inl :: "'a \<Rightarrow> 'a + 'b" where
-  "Inl = Abs_sum \<circ> Inl_Rep"
+definition Inl :: "'a \<Rightarrow> 'a + 'b"
+  where "Inl = Abs_sum \<circ> Inl_Rep"
 
-definition Inr :: "'b \<Rightarrow> 'a + 'b" where
-  "Inr = Abs_sum \<circ> Inr_Rep"
+definition Inr :: "'b \<Rightarrow> 'a + 'b"
+  where "Inr = Abs_sum \<circ> Inr_Rep"
 
 lemma inj_Inl [simp]: "inj_on Inl A"
-by (auto simp add: Inl_def intro!: comp_inj_on Inl_Rep_inject inj_on_Abs_sum Inl_RepI)
+  by (auto simp add: Inl_def intro!: comp_inj_on Inl_Rep_inject inj_on_Abs_sum Inl_RepI)
 
 lemma Inl_inject: "Inl x = Inl y \<Longrightarrow> x = y"
-using inj_Inl by (rule injD)
+  using inj_Inl by (rule injD)
 
 lemma inj_Inr [simp]: "inj_on Inr A"
-by (auto simp add: Inr_def intro!: comp_inj_on Inr_Rep_inject inj_on_Abs_sum Inr_RepI)
+  by (auto simp add: Inr_def intro!: comp_inj_on Inr_Rep_inject inj_on_Abs_sum Inr_RepI)
 
 lemma Inr_inject: "Inr x = Inr y \<Longrightarrow> x = y"
-using inj_Inr by (rule injD)
+  using inj_Inr by (rule injD)
 
 lemma Inl_not_Inr: "Inl a \<noteq> Inr b"
 proof -
-  from Inl_RepI [of a] Inr_RepI [of b] have "{Inl_Rep a, Inr_Rep b} \<subseteq> sum" by auto
+  have "{Inl_Rep a, Inr_Rep b} \<subseteq> sum"
+    using Inl_RepI [of a] Inr_RepI [of b] by auto
   with inj_on_Abs_sum have "inj_on Abs_sum {Inl_Rep a, Inr_Rep b}" .
-  with Inl_Rep_not_Inr_Rep [of a b] inj_on_contraD have "Abs_sum (Inl_Rep a) \<noteq> Abs_sum (Inr_Rep b)" by auto
-  then show ?thesis by (simp add: Inl_def Inr_def)
+  with Inl_Rep_not_Inr_Rep [of a b] inj_on_contraD have "Abs_sum (Inl_Rep a) \<noteq> Abs_sum (Inr_Rep b)"
+    by auto
+  then show ?thesis
+    by (simp add: Inl_def Inr_def)
 qed
 
-lemma Inr_not_Inl: "Inr b \<noteq> Inl a" 
+lemma Inr_not_Inl: "Inr b \<noteq> Inl a"
   using Inl_not_Inr by (rule not_sym)
 
-lemma sumE: 
+lemma sumE:
   assumes "\<And>x::'a. s = Inl x \<Longrightarrow> P"
     and "\<And>y::'b. s = Inr y \<Longrightarrow> P"
   shows P
 proof (rule Abs_sum_cases [of s])
-  fix f 
+  fix f
   assume "s = Abs_sum f" and "f \<in> sum"
   with assms show P by (auto simp add: sum_def Inl_def Inr_def)
 qed
 
 free_constructors case_sum for
-    isl: Inl projl
-  | Inr projr
+  isl: Inl projl
+| Inr projr
   by (erule sumE, assumption) (auto dest: Inl_inject Inr_inject simp add: Inl_not_Inr)
 
 text \<open>Avoid name clashes by prefixing the output of \<open>old_rep_datatype\<close> with \<open>old\<close>.\<close>
@@ -119,24 +122,21 @@
 
 setup \<open>Sign.parent_path\<close>
 
-primrec map_sum :: "('a \<Rightarrow> 'c) \<Rightarrow> ('b \<Rightarrow> 'd) \<Rightarrow> 'a + 'b \<Rightarrow> 'c + 'd" where
+primrec map_sum :: "('a \<Rightarrow> 'c) \<Rightarrow> ('b \<Rightarrow> 'd) \<Rightarrow> 'a + 'b \<Rightarrow> 'c + 'd"
+where
   "map_sum f1 f2 (Inl a) = Inl (f1 a)"
 | "map_sum f1 f2 (Inr a) = Inr (f2 a)"
 
-functor map_sum: map_sum proof -
-  fix f g h i
-  show "map_sum f g \<circ> map_sum h i = map_sum (f \<circ> h) (g \<circ> i)"
+functor map_sum: map_sum
+proof -
+  show "map_sum f g \<circ> map_sum h i = map_sum (f \<circ> h) (g \<circ> i)" for f g h i
   proof
-    fix s
-    show "(map_sum f g \<circ> map_sum h i) s = map_sum (f \<circ> h) (g \<circ> i) s"
+    show "(map_sum f g \<circ> map_sum h i) s = map_sum (f \<circ> h) (g \<circ> i) s" for s
       by (cases s) simp_all
   qed
-next
-  fix s
   show "map_sum id id = id"
   proof
-    fix s
-    show "map_sum id id s = id s" 
+    show "map_sum id id s = id s" for s
       by (cases s) simp_all
   qed
 qed
@@ -145,7 +145,8 @@
   by (auto intro: sum.induct)
 
 lemma split_sum_ex: "(\<exists>x. P x) \<longleftrightarrow> (\<exists>x. P (Inl x)) \<or> (\<exists>x. P (Inr x))"
-using split_sum_all[of "\<lambda>x. \<not>P x"] by blast
+  using split_sum_all[of "\<lambda>x. \<not>P x"] by blast
+
 
 subsection \<open>Projections\<close>
 
@@ -161,29 +162,32 @@
 
 lemma case_sum_inject:
   assumes a: "case_sum f1 f2 = case_sum g1 g2"
-  assumes r: "f1 = g1 \<Longrightarrow> f2 = g2 \<Longrightarrow> P"
+    and r: "f1 = g1 \<Longrightarrow> f2 = g2 \<Longrightarrow> P"
   shows P
 proof (rule r)
-  show "f1 = g1" proof
+  show "f1 = g1"
+  proof
     fix x :: 'a
     from a have "case_sum f1 f2 (Inl x) = case_sum g1 g2 (Inl x)" by simp
     then show "f1 x = g1 x" by simp
   qed
-  show "f2 = g2" proof
+  show "f2 = g2"
+  proof
     fix y :: 'b
     from a have "case_sum f1 f2 (Inr y) = case_sum g1 g2 (Inr y)" by simp
     then show "f2 y = g2 y" by simp
   qed
 qed
 
-primrec Suml :: "('a \<Rightarrow> 'c) \<Rightarrow> 'a + 'b \<Rightarrow> 'c" where
-  "Suml f (Inl x) = f x"
+primrec Suml :: "('a \<Rightarrow> 'c) \<Rightarrow> 'a + 'b \<Rightarrow> 'c"
+  where "Suml f (Inl x) = f x"
 
-primrec Sumr :: "('b \<Rightarrow> 'c) \<Rightarrow> 'a + 'b \<Rightarrow> 'c" where
-  "Sumr f (Inr x) = f x"
+primrec Sumr :: "('b \<Rightarrow> 'c) \<Rightarrow> 'a + 'b \<Rightarrow> 'c"
+  where "Sumr f (Inr x) = f x"
 
 lemma Suml_inject:
-  assumes "Suml f = Suml g" shows "f = g"
+  assumes "Suml f = Suml g"
+  shows "f = g"
 proof
   fix x :: 'a
   let ?s = "Inl x :: 'a + 'b"
@@ -192,7 +196,8 @@
 qed
 
 lemma Sumr_inject:
-  assumes "Sumr f = Sumr g" shows "f = g"
+  assumes "Sumr f = Sumr g"
+  shows "f = g"
 proof
   fix x :: 'b
   let ?s = "Inr x :: 'a + 'b"
@@ -203,25 +208,25 @@
 
 subsection \<open>The Disjoint Sum of Sets\<close>
 
-definition Plus :: "'a set \<Rightarrow> 'b set \<Rightarrow> ('a + 'b) set" (infixr "<+>" 65) where
-  "A <+> B = Inl ` A \<union> Inr ` B"
+definition Plus :: "'a set \<Rightarrow> 'b set \<Rightarrow> ('a + 'b) set"  (infixr "<+>" 65)
+  where "A <+> B = Inl ` A \<union> Inr ` B"
 
-hide_const (open) Plus \<comment>"Valuable identifier"
+hide_const (open) Plus \<comment> "Valuable identifier"
 
 lemma InlI [intro!]: "a \<in> A \<Longrightarrow> Inl a \<in> A <+> B"
-by (simp add: Plus_def)
+  by (simp add: Plus_def)
 
 lemma InrI [intro!]: "b \<in> B \<Longrightarrow> Inr b \<in> A <+> B"
-by (simp add: Plus_def)
+  by (simp add: Plus_def)
 
 text \<open>Exhaustion rule for sums, a degenerate form of induction\<close>
 
-lemma PlusE [elim!]: 
+lemma PlusE [elim!]:
   "u \<in> A <+> B \<Longrightarrow> (\<And>x. x \<in> A \<Longrightarrow> u = Inl x \<Longrightarrow> P) \<Longrightarrow> (\<And>y. y \<in> B \<Longrightarrow> u = Inr y \<Longrightarrow> P) \<Longrightarrow> P"
-by (auto simp add: Plus_def)
+  by (auto simp add: Plus_def)
 
 lemma Plus_eq_empty_conv [simp]: "A <+> B = {} \<longleftrightarrow> A = {} \<and> B = {}"
-by auto
+  by auto
 
 lemma UNIV_Plus_UNIV [simp]: "UNIV <+> UNIV = UNIV"
 proof (rule set_eqI)
@@ -229,14 +234,11 @@
   show "u \<in> UNIV <+> UNIV \<longleftrightarrow> u \<in> UNIV" by (cases u) auto
 qed
 
-lemma UNIV_sum:
-  "UNIV = Inl ` UNIV \<union> Inr ` UNIV"
+lemma UNIV_sum: "UNIV = Inl ` UNIV \<union> Inr ` UNIV"
 proof -
-  { fix x :: "'a + 'b"
-    assume "x \<notin> range Inr"
-    then have "x \<in> range Inl"
-    by (cases x) simp_all
-  } then show ?thesis by auto
+  have "x \<in> range Inl" if "x \<notin> range Inr" for x :: "'a + 'b"
+    using that by (cases x) simp_all
+  then show ?thesis by auto
 qed
 
 hide_const (open) Suml Sumr sum