misc tuning and modernization;
authorwenzelm
Tue Jul 05 23:39:49 2016 +0200 (2016-07-05)
changeset 63400249fa34faba2
parent 63399 d1742d1b7f0f
child 63401 28cc90b0e9c2
child 63402 f199837304d7
misc tuning and modernization;
src/HOL/Fun.thy
src/HOL/Inductive.thy
src/HOL/Product_Type.thy
src/HOL/Set.thy
src/HOL/Sum_Type.thy
     1.1 --- a/src/HOL/Fun.thy	Tue Jul 05 22:47:48 2016 +0200
     1.2 +++ b/src/HOL/Fun.thy	Tue Jul 05 23:39:49 2016 +0200
     1.3 @@ -21,6 +21,7 @@
     1.4  lemma b_uniq_choice: "\<forall>x\<in>S. \<exists>!y. Q x y \<Longrightarrow> \<exists>f. \<forall>x\<in>S. Q x (f x)"
     1.5    by (force intro: theI')
     1.6  
     1.7 +
     1.8  subsection \<open>The Identity Function \<open>id\<close>\<close>
     1.9  
    1.10  definition id :: "'a \<Rightarrow> 'a"
    1.11 @@ -283,9 +284,8 @@
    1.12    shows "inj f"
    1.13    \<comment> \<open>Courtesy of Stephan Merz\<close>
    1.14  proof (rule inj_onI)
    1.15 -  fix x y
    1.16 -  assume f_eq: "f x = f y"
    1.17 -  show "x = y" by (rule linorder_cases) (auto dest: hyp simp: f_eq)
    1.18 +  show "x = y" if "f x = f y" for x y
    1.19 +   by (rule linorder_cases) (auto dest: hyp simp: that)
    1.20  qed
    1.21  
    1.22  lemma surj_def: "surj f \<longleftrightarrow> (\<forall>y. \<exists>x. y = f x)"
    1.23 @@ -427,9 +427,8 @@
    1.24    by (auto simp add: bij_betw_def)
    1.25  
    1.26  lemma bij_betw_combine:
    1.27 -  assumes "bij_betw f A B" "bij_betw f C D" "B \<inter> D = {}"
    1.28 -  shows "bij_betw f (A \<union> C) (B \<union> D)"
    1.29 -  using assms unfolding bij_betw_def inj_on_Un image_Un by auto
    1.30 +  "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)"
    1.31 +  unfolding bij_betw_def inj_on_Un image_Un by auto
    1.32  
    1.33  lemma bij_betw_subset: "bij_betw f A A' \<Longrightarrow> B \<le> A \<Longrightarrow> f ` B = B' \<Longrightarrow> bij_betw f B B'"
    1.34    by (auto simp add: bij_betw_def inj_on_def)
    1.35 @@ -531,14 +530,15 @@
    1.36      and img2: "f' ` A' \<le> A"
    1.37    shows "bij_betw f A A'"
    1.38    using assms
    1.39 -proof (unfold bij_betw_def inj_on_def, safe)
    1.40 +  unfolding bij_betw_def inj_on_def
    1.41 +proof safe
    1.42    fix a b
    1.43    assume *: "a \<in> A" "b \<in> A" and **: "f a = f b"
    1.44    have "a = f' (f a) \<and> b = f'(f b)" using * left by simp
    1.45    with ** show "a = b" by simp
    1.46  next
    1.47    fix a' assume *: "a' \<in> A'"
    1.48 -  hence "f' a' \<in> A" using img2 by blast
    1.49 +  then have "f' a' \<in> A" using img2 by blast
    1.50    moreover
    1.51    have "a' = f (f' a')" using * right by simp
    1.52    ultimately show "a' \<in> f ` A" by blast
    1.53 @@ -823,7 +823,7 @@
    1.54  
    1.55  subsubsection \<open>Proof tools\<close>
    1.56  
    1.57 -text \<open>Simplify terms of the form f(...,x:=y,...,x:=z,...) to f(...,x:=z,...)\<close>
    1.58 +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>
    1.59  
    1.60  simproc_setup fun_upd2 ("f(v := w, x := y)") = \<open>fn _ =>
    1.61    let
    1.62 @@ -843,14 +843,14 @@
    1.63        let
    1.64          val t = Thm.term_of ct
    1.65        in
    1.66 -        case find_double t of
    1.67 +        (case find_double t of
    1.68            (T, NONE) => NONE
    1.69          | (T, SOME rhs) =>
    1.70              SOME (Goal.prove ctxt [] [] (Logic.mk_equals (t, rhs))
    1.71                (fn _ =>
    1.72                  resolve_tac ctxt [eq_reflection] 1 THEN
    1.73                  resolve_tac ctxt @{thms ext} 1 THEN
    1.74 -                simp_tac (put_simpset ss ctxt) 1))
    1.75 +                simp_tac (put_simpset ss ctxt) 1)))
    1.76        end
    1.77    in proc end
    1.78  \<close>
     2.1 --- a/src/HOL/Inductive.thy	Tue Jul 05 22:47:48 2016 +0200
     2.2 +++ b/src/HOL/Inductive.thy	Tue Jul 05 23:39:49 2016 +0200
     2.3 @@ -19,48 +19,45 @@
     2.4  context complete_lattice
     2.5  begin
     2.6  
     2.7 -definition
     2.8 -  lfp :: "('a \<Rightarrow> 'a) \<Rightarrow> 'a" where
     2.9 -  "lfp f = Inf {u. f u \<le> u}"    \<comment>\<open>least fixed point\<close>
    2.10 +definition lfp :: "('a \<Rightarrow> 'a) \<Rightarrow> 'a"  \<comment> \<open>least fixed point\<close>
    2.11 +  where "lfp f = Inf {u. f u \<le> u}"
    2.12  
    2.13 -definition
    2.14 -  gfp :: "('a \<Rightarrow> 'a) \<Rightarrow> 'a" where
    2.15 -  "gfp f = Sup {u. u \<le> f u}"    \<comment>\<open>greatest fixed point\<close>
    2.16 +definition gfp :: "('a \<Rightarrow> 'a) \<Rightarrow> 'a"  \<comment> \<open>greatest fixed point\<close>
    2.17 +  where "gfp f = Sup {u. u \<le> f u}"
    2.18  
    2.19  
    2.20 -subsection\<open>Proof of Knaster-Tarski Theorem using @{term lfp}\<close>
    2.21 +subsection \<open>Proof of Knaster-Tarski Theorem using @{term lfp}\<close>
    2.22  
    2.23 -text\<open>@{term "lfp f"} is the least upper bound of
    2.24 -      the set @{term "{u. f(u) \<le> u}"}\<close>
    2.25 +text \<open>@{term "lfp f"} is the least upper bound of the set @{term "{u. f u \<le> u}"}\<close>
    2.26  
    2.27 -lemma lfp_lowerbound: "f A \<le> A ==> lfp f \<le> A"
    2.28 +lemma lfp_lowerbound: "f A \<le> A \<Longrightarrow> lfp f \<le> A"
    2.29    by (auto simp add: lfp_def intro: Inf_lower)
    2.30  
    2.31 -lemma lfp_greatest: "(!!u. f u \<le> u ==> A \<le> u) ==> A \<le> lfp f"
    2.32 +lemma lfp_greatest: "(\<And>u. f u \<le> u \<Longrightarrow> A \<le> u) \<Longrightarrow> A \<le> lfp f"
    2.33    by (auto simp add: lfp_def intro: Inf_greatest)
    2.34  
    2.35  end
    2.36  
    2.37 -lemma lfp_lemma2: "mono f ==> f (lfp f) \<le> lfp f"
    2.38 +lemma lfp_lemma2: "mono f \<Longrightarrow> f (lfp f) \<le> lfp f"
    2.39    by (iprover intro: lfp_greatest order_trans monoD lfp_lowerbound)
    2.40  
    2.41 -lemma lfp_lemma3: "mono f ==> lfp f \<le> f (lfp f)"
    2.42 +lemma lfp_lemma3: "mono f \<Longrightarrow> lfp f \<le> f (lfp f)"
    2.43    by (iprover intro: lfp_lemma2 monoD lfp_lowerbound)
    2.44  
    2.45 -lemma lfp_unfold: "mono f ==> lfp f = f (lfp f)"
    2.46 +lemma lfp_unfold: "mono f \<Longrightarrow> lfp f = f (lfp f)"
    2.47    by (iprover intro: order_antisym lfp_lemma2 lfp_lemma3)
    2.48  
    2.49  lemma lfp_const: "lfp (\<lambda>x. t) = t"
    2.50 -  by (rule lfp_unfold) (simp add:mono_def)
    2.51 +  by (rule lfp_unfold) (simp add: mono_def)
    2.52  
    2.53  
    2.54  subsection \<open>General induction rules for least fixed points\<close>
    2.55  
    2.56 -lemma lfp_ordinal_induct[case_names mono step union]:
    2.57 +lemma lfp_ordinal_induct [case_names mono step union]:
    2.58    fixes f :: "'a::complete_lattice \<Rightarrow> 'a"
    2.59    assumes mono: "mono f"
    2.60 -  and P_f: "\<And>S. P S \<Longrightarrow> S \<le> lfp f \<Longrightarrow> P (f S)"
    2.61 -  and P_Union: "\<And>M. \<forall>S\<in>M. P S \<Longrightarrow> P (Sup M)"
    2.62 +    and P_f: "\<And>S. P S \<Longrightarrow> S \<le> lfp f \<Longrightarrow> P (f S)"
    2.63 +    and P_Union: "\<And>M. \<forall>S\<in>M. P S \<Longrightarrow> P (Sup M)"
    2.64    shows "P (lfp f)"
    2.65  proof -
    2.66    let ?M = "{S. S \<le> lfp f \<and> P S}"
    2.67 @@ -68,96 +65,94 @@
    2.68    also have "Sup ?M = lfp f"
    2.69    proof (rule antisym)
    2.70      show "Sup ?M \<le> lfp f" by (blast intro: Sup_least)
    2.71 -    hence "f (Sup ?M) \<le> f (lfp f)" by (rule mono [THEN monoD])
    2.72 -    hence "f (Sup ?M) \<le> lfp f" using mono [THEN lfp_unfold] by simp
    2.73 -    hence "f (Sup ?M) \<in> ?M" using P_Union by simp (intro P_f Sup_least, auto)
    2.74 -    hence "f (Sup ?M) \<le> Sup ?M" by (rule Sup_upper)
    2.75 -    thus "lfp f \<le> Sup ?M" by (rule lfp_lowerbound)
    2.76 +    then have "f (Sup ?M) \<le> f (lfp f)"
    2.77 +      by (rule mono [THEN monoD])
    2.78 +    then have "f (Sup ?M) \<le> lfp f"
    2.79 +      using mono [THEN lfp_unfold] by simp
    2.80 +    then have "f (Sup ?M) \<in> ?M"
    2.81 +      using P_Union by simp (intro P_f Sup_least, auto)
    2.82 +    then have "f (Sup ?M) \<le> Sup ?M"
    2.83 +      by (rule Sup_upper)
    2.84 +    then show "lfp f \<le> Sup ?M"
    2.85 +      by (rule lfp_lowerbound)
    2.86    qed
    2.87    finally show ?thesis .
    2.88 -qed 
    2.89 +qed
    2.90  
    2.91  theorem lfp_induct:
    2.92 -  assumes mono: "mono f" and ind: "f (inf (lfp f) P) \<le> P"
    2.93 +  assumes mono: "mono f"
    2.94 +    and ind: "f (inf (lfp f) P) \<le> P"
    2.95    shows "lfp f \<le> P"
    2.96  proof (induction rule: lfp_ordinal_induct)
    2.97 -  case (step S) then show ?case
    2.98 +  case (step S)
    2.99 +  then show ?case
   2.100      by (intro order_trans[OF _ ind] monoD[OF mono]) auto
   2.101  qed (auto intro: mono Sup_least)
   2.102  
   2.103  lemma lfp_induct_set:
   2.104 -  assumes lfp: "a: lfp(f)"
   2.105 -    and mono: "mono(f)"
   2.106 -    and indhyp: "!!x. [| x: f(lfp(f) Int {x. P(x)}) |] ==> P(x)"
   2.107 -  shows "P(a)"
   2.108 -  by (rule lfp_induct [THEN subsetD, THEN CollectD, OF mono _ lfp])
   2.109 -     (auto simp: intro: indhyp)
   2.110 +  assumes lfp: "a \<in> lfp f"
   2.111 +    and mono: "mono f"
   2.112 +    and hyp: "\<And>x. x \<in> f (lfp f \<inter> {x. P x}) \<Longrightarrow> P x"
   2.113 +  shows "P a"
   2.114 +  by (rule lfp_induct [THEN subsetD, THEN CollectD, OF mono _ lfp]) (auto intro: hyp)
   2.115  
   2.116 -lemma lfp_ordinal_induct_set: 
   2.117 +lemma lfp_ordinal_induct_set:
   2.118    assumes mono: "mono f"
   2.119 -    and P_f: "!!S. P S ==> P(f S)"
   2.120 -    and P_Union: "!!M. !S:M. P S ==> P (\<Union>M)"
   2.121 -  shows "P(lfp f)"
   2.122 +    and P_f: "\<And>S. P S \<Longrightarrow> P (f S)"
   2.123 +    and P_Union: "\<And>M. \<forall>S\<in>M. P S \<Longrightarrow> P (\<Union>M)"
   2.124 +  shows "P (lfp f)"
   2.125    using assms by (rule lfp_ordinal_induct)
   2.126  
   2.127  
   2.128 -text\<open>Definition forms of \<open>lfp_unfold\<close> and \<open>lfp_induct\<close>, 
   2.129 -    to control unfolding\<close>
   2.130 +text \<open>Definition forms of \<open>lfp_unfold\<close> and \<open>lfp_induct\<close>, to control unfolding.\<close>
   2.131  
   2.132 -lemma def_lfp_unfold: "[| h==lfp(f);  mono(f) |] ==> h = f(h)"
   2.133 +lemma def_lfp_unfold: "h \<equiv> lfp f \<Longrightarrow> mono f \<Longrightarrow> h = f h"
   2.134    by (auto intro!: lfp_unfold)
   2.135  
   2.136 -lemma def_lfp_induct: 
   2.137 -    "[| A == lfp(f); mono(f);
   2.138 -        f (inf A P) \<le> P
   2.139 -     |] ==> A \<le> P"
   2.140 +lemma def_lfp_induct: "A \<equiv> lfp f \<Longrightarrow> mono f \<Longrightarrow> f (inf A P) \<le> P \<Longrightarrow> A \<le> P"
   2.141    by (blast intro: lfp_induct)
   2.142  
   2.143 -lemma def_lfp_induct_set: 
   2.144 -    "[| A == lfp(f);  mono(f);   a:A;                    
   2.145 -        !!x. [| x: f(A Int {x. P(x)}) |] ==> P(x)         
   2.146 -     |] ==> P(a)"
   2.147 +lemma def_lfp_induct_set:
   2.148 +  "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"
   2.149    by (blast intro: lfp_induct_set)
   2.150  
   2.151 -(*Monotonicity of lfp!*)
   2.152 -lemma lfp_mono: "(!!Z. f Z \<le> g Z) ==> lfp f \<le> lfp g"
   2.153 -  by (rule lfp_lowerbound [THEN lfp_greatest], blast intro: order_trans)
   2.154 +text \<open>Monotonicity of \<open>lfp\<close>!\<close>
   2.155 +lemma lfp_mono: "(\<And>Z. f Z \<le> g Z) \<Longrightarrow> lfp f \<le> lfp g"
   2.156 +  by (rule lfp_lowerbound [THEN lfp_greatest]) (blast intro: order_trans)
   2.157  
   2.158  
   2.159 -subsection \<open>Proof of Knaster-Tarski Theorem using @{term gfp}\<close>
   2.160 +subsection \<open>Proof of Knaster-Tarski Theorem using \<open>gfp\<close>\<close>
   2.161  
   2.162 -text\<open>@{term "gfp f"} is the greatest lower bound of 
   2.163 -      the set @{term "{u. u \<le> f(u)}"}\<close>
   2.164 +text \<open>@{term "gfp f"} is the greatest lower bound of the set @{term "{u. u \<le> f u}"}\<close>
   2.165  
   2.166 -lemma gfp_upperbound: "X \<le> f X ==> X \<le> gfp f"
   2.167 +lemma gfp_upperbound: "X \<le> f X \<Longrightarrow> X \<le> gfp f"
   2.168    by (auto simp add: gfp_def intro: Sup_upper)
   2.169  
   2.170 -lemma gfp_least: "(!!u. u \<le> f u ==> u \<le> X) ==> gfp f \<le> X"
   2.171 +lemma gfp_least: "(\<And>u. u \<le> f u \<Longrightarrow> u \<le> X) \<Longrightarrow> gfp f \<le> X"
   2.172    by (auto simp add: gfp_def intro: Sup_least)
   2.173  
   2.174 -lemma gfp_lemma2: "mono f ==> gfp f \<le> f (gfp f)"
   2.175 +lemma gfp_lemma2: "mono f \<Longrightarrow> gfp f \<le> f (gfp f)"
   2.176    by (iprover intro: gfp_least order_trans monoD gfp_upperbound)
   2.177  
   2.178 -lemma gfp_lemma3: "mono f ==> f (gfp f) \<le> gfp f"
   2.179 +lemma gfp_lemma3: "mono f \<Longrightarrow> f (gfp f) \<le> gfp f"
   2.180    by (iprover intro: gfp_lemma2 monoD gfp_upperbound)
   2.181  
   2.182 -lemma gfp_unfold: "mono f ==> gfp f = f (gfp f)"
   2.183 +lemma gfp_unfold: "mono f \<Longrightarrow> gfp f = f (gfp f)"
   2.184    by (iprover intro: order_antisym gfp_lemma2 gfp_lemma3)
   2.185  
   2.186  
   2.187  subsection \<open>Coinduction rules for greatest fixed points\<close>
   2.188  
   2.189 -text\<open>weak version\<close>
   2.190 -lemma weak_coinduct: "[| a: X;  X \<subseteq> f(X) |] ==> a : gfp(f)"
   2.191 +text \<open>Weak version.\<close>
   2.192 +lemma weak_coinduct: "a \<in> X \<Longrightarrow> X \<subseteq> f X \<Longrightarrow> a \<in> gfp f"
   2.193    by (rule gfp_upperbound [THEN subsetD]) auto
   2.194  
   2.195 -lemma weak_coinduct_image: "!!X. [| a : X; g`X \<subseteq> f (g`X) |] ==> g a : gfp f"
   2.196 +lemma weak_coinduct_image: "a \<in> X \<Longrightarrow> g`X \<subseteq> f (g`X) \<Longrightarrow> g a \<in> gfp f"
   2.197    apply (erule gfp_upperbound [THEN subsetD])
   2.198    apply (erule imageI)
   2.199    done
   2.200  
   2.201 -lemma coinduct_lemma:
   2.202 -     "[| X \<le> f (sup X (gfp f));  mono f |] ==> sup X (gfp f) \<le> f (sup X (gfp f))"
   2.203 +lemma coinduct_lemma: "X \<le> f (sup X (gfp f)) \<Longrightarrow> mono f \<Longrightarrow> sup X (gfp f) \<le> f (sup X (gfp f))"
   2.204    apply (frule gfp_lemma2)
   2.205    apply (drule mono_sup)
   2.206    apply (rule le_supI)
   2.207 @@ -169,112 +164,113 @@
   2.208    apply assumption
   2.209    done
   2.210  
   2.211 -text\<open>strong version, thanks to Coen and Frost\<close>
   2.212 -lemma coinduct_set: "[| mono(f);  a: X;  X \<subseteq> f(X Un gfp(f)) |] ==> a : gfp(f)"
   2.213 +text \<open>Strong version, thanks to Coen and Frost.\<close>
   2.214 +lemma coinduct_set: "mono f \<Longrightarrow> a \<in> X \<Longrightarrow> X \<subseteq> f (X \<union> gfp f) \<Longrightarrow> a \<in> gfp f"
   2.215    by (rule weak_coinduct[rotated], rule coinduct_lemma) blast+
   2.216  
   2.217 -lemma gfp_fun_UnI2: "[| mono(f);  a: gfp(f) |] ==> a: f(X Un gfp(f))"
   2.218 +lemma gfp_fun_UnI2: "mono f \<Longrightarrow> a \<in> gfp f \<Longrightarrow> a \<in> f (X \<union> gfp f)"
   2.219    by (blast dest: gfp_lemma2 mono_Un)
   2.220  
   2.221  lemma gfp_ordinal_induct[case_names mono step union]:
   2.222    fixes f :: "'a::complete_lattice \<Rightarrow> 'a"
   2.223    assumes mono: "mono f"
   2.224 -  and P_f: "\<And>S. P S \<Longrightarrow> gfp f \<le> S \<Longrightarrow> P (f S)"
   2.225 -  and P_Union: "\<And>M. \<forall>S\<in>M. P S \<Longrightarrow> P (Inf M)"
   2.226 +    and P_f: "\<And>S. P S \<Longrightarrow> gfp f \<le> S \<Longrightarrow> P (f S)"
   2.227 +    and P_Union: "\<And>M. \<forall>S\<in>M. P S \<Longrightarrow> P (Inf M)"
   2.228    shows "P (gfp f)"
   2.229  proof -
   2.230    let ?M = "{S. gfp f \<le> S \<and> P S}"
   2.231    have "P (Inf ?M)" using P_Union by simp
   2.232    also have "Inf ?M = gfp f"
   2.233    proof (rule antisym)
   2.234 -    show "gfp f \<le> Inf ?M" by (blast intro: Inf_greatest)
   2.235 -    hence "f (gfp f) \<le> f (Inf ?M)" by (rule mono [THEN monoD])
   2.236 -    hence "gfp f \<le> f (Inf ?M)" using mono [THEN gfp_unfold] by simp
   2.237 -    hence "f (Inf ?M) \<in> ?M" using P_Union by simp (intro P_f Inf_greatest, auto)
   2.238 -    hence "Inf ?M \<le> f (Inf ?M)" by (rule Inf_lower)
   2.239 -    thus "Inf ?M \<le> gfp f" by (rule gfp_upperbound)
   2.240 +    show "gfp f \<le> Inf ?M"
   2.241 +      by (blast intro: Inf_greatest)
   2.242 +    then have "f (gfp f) \<le> f (Inf ?M)"
   2.243 +      by (rule mono [THEN monoD])
   2.244 +    then have "gfp f \<le> f (Inf ?M)"
   2.245 +      using mono [THEN gfp_unfold] by simp
   2.246 +    then have "f (Inf ?M) \<in> ?M"
   2.247 +      using P_Union by simp (intro P_f Inf_greatest, auto)
   2.248 +    then have "Inf ?M \<le> f (Inf ?M)"
   2.249 +      by (rule Inf_lower)
   2.250 +    then show "Inf ?M \<le> gfp f"
   2.251 +      by (rule gfp_upperbound)
   2.252    qed
   2.253    finally show ?thesis .
   2.254 -qed 
   2.255 +qed
   2.256  
   2.257 -lemma coinduct: assumes mono: "mono f" and ind: "X \<le> f (sup X (gfp f))" shows "X \<le> gfp f"
   2.258 +lemma coinduct:
   2.259 +  assumes mono: "mono f"
   2.260 +    and ind: "X \<le> f (sup X (gfp f))"
   2.261 +  shows "X \<le> gfp f"
   2.262  proof (induction rule: gfp_ordinal_induct)
   2.263    case (step S) then show ?case
   2.264      by (intro order_trans[OF ind _] monoD[OF mono]) auto
   2.265  qed (auto intro: mono Inf_greatest)
   2.266  
   2.267 +
   2.268  subsection \<open>Even Stronger Coinduction Rule, by Martin Coen\<close>
   2.269  
   2.270 -text\<open>Weakens the condition @{term "X \<subseteq> f(X)"} to one expressed using both
   2.271 +text \<open>Weakens the condition @{term "X \<subseteq> f X"} to one expressed using both
   2.272    @{term lfp} and @{term gfp}\<close>
   2.273 -
   2.274 -lemma coinduct3_mono_lemma: "mono(f) ==> mono(%x. f(x) Un X Un B)"
   2.275 -by (iprover intro: subset_refl monoI Un_mono monoD)
   2.276 +lemma coinduct3_mono_lemma: "mono f \<Longrightarrow> mono (\<lambda>x. f x \<union> X \<union> B)"
   2.277 +  by (iprover intro: subset_refl monoI Un_mono monoD)
   2.278  
   2.279  lemma coinduct3_lemma:
   2.280 -     "[| X \<subseteq> f(lfp(%x. f(x) Un X Un gfp(f)));  mono(f) |]
   2.281 -      ==> lfp(%x. f(x) Un X Un gfp(f)) \<subseteq> f(lfp(%x. f(x) Un X Un gfp(f)))"
   2.282 -apply (rule subset_trans)
   2.283 -apply (erule coinduct3_mono_lemma [THEN lfp_lemma3])
   2.284 -apply (rule Un_least [THEN Un_least])
   2.285 -apply (rule subset_refl, assumption)
   2.286 -apply (rule gfp_unfold [THEN equalityD1, THEN subset_trans], assumption)
   2.287 -apply (rule monoD, assumption)
   2.288 -apply (subst coinduct3_mono_lemma [THEN lfp_unfold], auto)
   2.289 -done
   2.290 +  "X \<subseteq> f (lfp (\<lambda>x. f x \<union> X \<union> gfp f)) \<Longrightarrow> mono f \<Longrightarrow>
   2.291 +    lfp (\<lambda>x. f x \<union> X \<union> gfp f) \<subseteq> f (lfp (\<lambda>x. f x \<union> X \<union> gfp f))"
   2.292 +  apply (rule subset_trans)
   2.293 +  apply (erule coinduct3_mono_lemma [THEN lfp_lemma3])
   2.294 +  apply (rule Un_least [THEN Un_least])
   2.295 +  apply (rule subset_refl, assumption)
   2.296 +  apply (rule gfp_unfold [THEN equalityD1, THEN subset_trans], assumption)
   2.297 +  apply (rule monoD, assumption)
   2.298 +  apply (subst coinduct3_mono_lemma [THEN lfp_unfold], auto)
   2.299 +  done
   2.300  
   2.301 -lemma coinduct3: 
   2.302 -  "[| mono(f);  a:X;  X \<subseteq> f(lfp(%x. f(x) Un X Un gfp(f))) |] ==> a : gfp(f)"
   2.303 -apply (rule coinduct3_lemma [THEN [2] weak_coinduct])
   2.304 -apply (rule coinduct3_mono_lemma [THEN lfp_unfold, THEN ssubst])
   2.305 -apply (simp_all)
   2.306 -done
   2.307 +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"
   2.308 +  apply (rule coinduct3_lemma [THEN [2] weak_coinduct])
   2.309 +  apply (rule coinduct3_mono_lemma [THEN lfp_unfold, THEN ssubst])
   2.310 +  apply simp_all
   2.311 +  done
   2.312  
   2.313 -text\<open>Definition forms of \<open>gfp_unfold\<close> and \<open>coinduct\<close>, 
   2.314 -    to control unfolding\<close>
   2.315 +text  \<open>Definition forms of \<open>gfp_unfold\<close> and \<open>coinduct\<close>, to control unfolding.\<close>
   2.316  
   2.317 -lemma def_gfp_unfold: "[| A==gfp(f);  mono(f) |] ==> A = f(A)"
   2.318 +lemma def_gfp_unfold: "A \<equiv> gfp f \<Longrightarrow> mono f \<Longrightarrow> A = f A"
   2.319    by (auto intro!: gfp_unfold)
   2.320  
   2.321 -lemma def_coinduct:
   2.322 -     "[| A==gfp(f);  mono(f);  X \<le> f(sup X A) |] ==> X \<le> A"
   2.323 +lemma def_coinduct: "A \<equiv> gfp f \<Longrightarrow> mono f \<Longrightarrow> X \<le> f (sup X A) \<Longrightarrow> X \<le> A"
   2.324    by (iprover intro!: coinduct)
   2.325  
   2.326 -lemma def_coinduct_set:
   2.327 -     "[| A==gfp(f);  mono(f);  a:X;  X \<subseteq> f(X Un A) |] ==> a: A"
   2.328 +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"
   2.329    by (auto intro!: coinduct_set)
   2.330  
   2.331 -(*The version used in the induction/coinduction package*)
   2.332  lemma def_Collect_coinduct:
   2.333 -    "[| A == gfp(%w. Collect(P(w)));  mono(%w. Collect(P(w)));   
   2.334 -        a: X;  !!z. z: X ==> P (X Un A) z |] ==>  
   2.335 -     a : A"
   2.336 +  "A \<equiv> gfp (\<lambda>w. Collect (P w)) \<Longrightarrow> mono (\<lambda>w. Collect (P w)) \<Longrightarrow> a \<in> X \<Longrightarrow>
   2.337 +    (\<And>z. z \<in> X \<Longrightarrow> P (X \<union> A) z) \<Longrightarrow> a \<in> A"
   2.338    by (erule def_coinduct_set) auto
   2.339  
   2.340 -lemma def_coinduct3:
   2.341 -    "[| A==gfp(f); mono(f);  a:X;  X \<subseteq> f(lfp(%x. f(x) Un X Un A)) |] ==> a: A"
   2.342 +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"
   2.343    by (auto intro!: coinduct3)
   2.344  
   2.345 -text\<open>Monotonicity of @{term gfp}!\<close>
   2.346 -lemma gfp_mono: "(!!Z. f Z \<le> g Z) ==> gfp f \<le> gfp g"
   2.347 -  by (rule gfp_upperbound [THEN gfp_least], blast intro: order_trans)
   2.348 +text \<open>Monotonicity of @{term gfp}!\<close>
   2.349 +lemma gfp_mono: "(\<And>Z. f Z \<le> g Z) \<Longrightarrow> gfp f \<le> gfp g"
   2.350 +  by (rule gfp_upperbound [THEN gfp_least]) (blast intro: order_trans)
   2.351 +
   2.352  
   2.353  subsection \<open>Rules for fixed point calculus\<close>
   2.354  
   2.355 -
   2.356  lemma lfp_rolling:
   2.357    assumes "mono g" "mono f"
   2.358    shows "g (lfp (\<lambda>x. f (g x))) = lfp (\<lambda>x. g (f x))"
   2.359  proof (rule antisym)
   2.360    have *: "mono (\<lambda>x. f (g x))"
   2.361      using assms by (auto simp: mono_def)
   2.362 -
   2.363    show "lfp (\<lambda>x. g (f x)) \<le> g (lfp (\<lambda>x. f (g x)))"
   2.364      by (rule lfp_lowerbound) (simp add: lfp_unfold[OF *, symmetric])
   2.365 -
   2.366    show "g (lfp (\<lambda>x. f (g x))) \<le> lfp (\<lambda>x. g (f x))"
   2.367    proof (rule lfp_greatest)
   2.368 -    fix u assume "g (f u) \<le> u"
   2.369 +    fix u
   2.370 +    assume "g (f u) \<le> u"
   2.371      moreover then have "g (lfp (\<lambda>x. f (g x))) \<le> g (f u)"
   2.372        by (intro assms[THEN monoD] lfp_lowerbound)
   2.373      ultimately show "g (lfp (\<lambda>x. f (g x))) \<le> u"
   2.374 @@ -309,7 +305,6 @@
   2.375      using assms by (auto simp: mono_def)
   2.376    show "g (gfp (\<lambda>x. f (g x))) \<le> gfp (\<lambda>x. g (f x))"
   2.377      by (rule gfp_upperbound) (simp add: gfp_unfold[OF *, symmetric])
   2.378 -
   2.379    show "gfp (\<lambda>x. g (f x)) \<le> g (gfp (\<lambda>x. f (g x)))"
   2.380    proof (rule gfp_least)
   2.381      fix u assume "u \<le> g (f u)"
   2.382 @@ -339,6 +334,7 @@
   2.383    qed
   2.384  qed
   2.385  
   2.386 +
   2.387  subsection \<open>Inductive predicates and sets\<close>
   2.388  
   2.389  text \<open>Package setup.\<close>
     3.1 --- a/src/HOL/Product_Type.thy	Tue Jul 05 22:47:48 2016 +0200
     3.2 +++ b/src/HOL/Product_Type.thy	Tue Jul 05 23:39:49 2016 +0200
     3.3 @@ -37,12 +37,11 @@
     3.4  declare case_split [cases type: bool]
     3.5    \<comment> "prefer plain propositional version"
     3.6  
     3.7 -lemma
     3.8 -  shows [code]: "HOL.equal False P \<longleftrightarrow> \<not> P"
     3.9 -    and [code]: "HOL.equal True P \<longleftrightarrow> P" 
    3.10 -    and [code]: "HOL.equal P False \<longleftrightarrow> \<not> P"
    3.11 -    and [code]: "HOL.equal P True \<longleftrightarrow> P"
    3.12 -    and [code nbe]: "HOL.equal P P \<longleftrightarrow> True"
    3.13 +lemma [code]: "HOL.equal False P \<longleftrightarrow> \<not> P"
    3.14 +  and [code]: "HOL.equal True P \<longleftrightarrow> P" 
    3.15 +  and [code]: "HOL.equal P False \<longleftrightarrow> \<not> P"
    3.16 +  and [code]: "HOL.equal P True \<longleftrightarrow> P"
    3.17 +  and [code nbe]: "HOL.equal P P \<longleftrightarrow> True"
    3.18    by (simp_all add: equal)
    3.19  
    3.20  lemma If_case_cert:
    3.21 @@ -101,23 +100,23 @@
    3.22  
    3.23  setup \<open>Sign.parent_path\<close>
    3.24  
    3.25 -lemma unit_all_eq1: "(!!x::unit. PROP P x) == PROP P ()"
    3.26 +lemma unit_all_eq1: "(\<And>x::unit. PROP P x) \<equiv> PROP P ()"
    3.27    by simp
    3.28  
    3.29 -lemma unit_all_eq2: "(!!x::unit. PROP P) == PROP P"
    3.30 +lemma unit_all_eq2: "(\<And>x::unit. PROP P) \<equiv> PROP P"
    3.31    by (rule triv_forall_equality)
    3.32  
    3.33  text \<open>
    3.34    This rewrite counters the effect of simproc \<open>unit_eq\<close> on @{term
    3.35 -  [source] "%u::unit. f u"}, replacing it by @{term [source]
    3.36 -  f} rather than by @{term [source] "%u. f ()"}.
    3.37 +  [source] "\<lambda>u::unit. f u"}, replacing it by @{term [source]
    3.38 +  f} rather than by @{term [source] "\<lambda>u. f ()"}.
    3.39  \<close>
    3.40  
    3.41 -lemma unit_abs_eta_conv [simp]: "(%u::unit. f ()) = f"
    3.42 +lemma unit_abs_eta_conv [simp]: "(\<lambda>u::unit. f ()) = f"
    3.43    by (rule ext) simp
    3.44  
    3.45 -lemma UNIV_unit:
    3.46 -  "UNIV = {()}" by auto
    3.47 +lemma UNIV_unit: "UNIV = {()}"
    3.48 +  by auto
    3.49  
    3.50  instantiation unit :: default
    3.51  begin
    3.52 @@ -128,52 +127,41 @@
    3.53  
    3.54  end
    3.55  
    3.56 -instantiation unit :: "{complete_boolean_algebra, complete_linorder, wellorder}"
    3.57 +instantiation unit :: "{complete_boolean_algebra,complete_linorder,wellorder}"
    3.58  begin
    3.59  
    3.60  definition less_eq_unit :: "unit \<Rightarrow> unit \<Rightarrow> bool"
    3.61 -where
    3.62 -  "(_::unit) \<le> _ \<longleftrightarrow> True"
    3.63 +  where "(_::unit) \<le> _ \<longleftrightarrow> True"
    3.64  
    3.65 -lemma less_eq_unit [iff]:
    3.66 -  "(u::unit) \<le> v"
    3.67 +lemma less_eq_unit [iff]: "u \<le> v" for u v :: unit
    3.68    by (simp add: less_eq_unit_def)
    3.69  
    3.70  definition less_unit :: "unit \<Rightarrow> unit \<Rightarrow> bool"
    3.71 -where
    3.72 -  "(_::unit) < _ \<longleftrightarrow> False"
    3.73 +  where "(_::unit) < _ \<longleftrightarrow> False"
    3.74  
    3.75 -lemma less_unit [iff]:
    3.76 -  "\<not> (u::unit) < v"
    3.77 +lemma less_unit [iff]: "\<not> u < v" for u v :: unit
    3.78    by (simp_all add: less_eq_unit_def less_unit_def)
    3.79  
    3.80  definition bot_unit :: unit
    3.81 -where
    3.82 -  [code_unfold]: "\<bottom> = ()"
    3.83 +  where [code_unfold]: "\<bottom> = ()"
    3.84  
    3.85  definition top_unit :: unit
    3.86 -where
    3.87 -  [code_unfold]: "\<top> = ()"
    3.88 +  where [code_unfold]: "\<top> = ()"
    3.89  
    3.90  definition inf_unit :: "unit \<Rightarrow> unit \<Rightarrow> unit"
    3.91 -where
    3.92 -  [simp]: "_ \<sqinter> _ = ()"
    3.93 +  where [simp]: "_ \<sqinter> _ = ()"
    3.94  
    3.95  definition sup_unit :: "unit \<Rightarrow> unit \<Rightarrow> unit"
    3.96 -where
    3.97 -  [simp]: "_ \<squnion> _ = ()"
    3.98 +  where [simp]: "_ \<squnion> _ = ()"
    3.99  
   3.100  definition Inf_unit :: "unit set \<Rightarrow> unit"
   3.101 -where
   3.102 -  [simp]: "\<Sqinter>_ = ()"
   3.103 +  where [simp]: "\<Sqinter>_ = ()"
   3.104  
   3.105  definition Sup_unit :: "unit set \<Rightarrow> unit"
   3.106 -where
   3.107 -  [simp]: "\<Squnion>_ = ()"
   3.108 +  where [simp]: "\<Squnion>_ = ()"
   3.109  
   3.110  definition uminus_unit :: "unit \<Rightarrow> unit"
   3.111 -where
   3.112 -  [simp]: "- _ = ()"
   3.113 +  where [simp]: "- _ = ()"
   3.114  
   3.115  declare less_eq_unit_def [abs_def, code_unfold]
   3.116    less_unit_def [abs_def, code_unfold]
   3.117 @@ -188,8 +176,8 @@
   3.118  
   3.119  end
   3.120  
   3.121 -lemma [code]:
   3.122 -  "HOL.equal (u::unit) v \<longleftrightarrow> True" unfolding equal unit_eq [of u] unit_eq [of v] by rule+
   3.123 +lemma [code]: "HOL.equal u v \<longleftrightarrow> True" for u v :: unit
   3.124 +  unfolding equal unit_eq [of u] unit_eq [of v] by rule+
   3.125  
   3.126  code_printing
   3.127    type_constructor unit \<rightharpoonup>
   3.128 @@ -221,8 +209,8 @@
   3.129  
   3.130  subsubsection \<open>Type definition\<close>
   3.131  
   3.132 -definition Pair_Rep :: "'a \<Rightarrow> 'b \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> bool" where
   3.133 -  "Pair_Rep a b = (\<lambda>x y. x = a \<and> y = b)"
   3.134 +definition Pair_Rep :: "'a \<Rightarrow> 'b \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> bool"
   3.135 +  where "Pair_Rep a b = (\<lambda>x y. x = a \<and> y = b)"
   3.136  
   3.137  definition "prod = {f. \<exists>a b. f = Pair_Rep (a::'a) (b::'b)}"
   3.138  
   3.139 @@ -232,8 +220,8 @@
   3.140  type_notation (ASCII)
   3.141    prod  (infixr "*" 20)
   3.142  
   3.143 -definition Pair :: "'a \<Rightarrow> 'b \<Rightarrow> 'a \<times> 'b" where
   3.144 -  "Pair a b = Abs_prod (Pair_Rep a b)"
   3.145 +definition Pair :: "'a \<Rightarrow> 'b \<Rightarrow> 'a \<times> 'b"
   3.146 +  where "Pair a b = Abs_prod (Pair_Rep a b)"
   3.147  
   3.148  lemma prod_cases: "(\<And>a b. P (Pair a b)) \<Longrightarrow> P p"
   3.149    by (cases p) (auto simp add: prod_def Pair_def Pair_Rep_def)
   3.150 @@ -258,7 +246,7 @@
   3.151  setup \<open>Sign.mandatory_path "old"\<close>
   3.152  
   3.153  old_rep_datatype Pair
   3.154 -by (erule prod_cases) (rule prod.inject)
   3.155 +  by (erule prod_cases) (rule prod.inject)
   3.156  
   3.157  setup \<open>Sign.parent_path\<close>
   3.158  
   3.159 @@ -297,16 +285,14 @@
   3.160  \<close>
   3.161  
   3.162  nonterminal tuple_args and patterns
   3.163 -
   3.164  syntax
   3.165 -  "_tuple"      :: "'a => tuple_args => 'a * 'b"        ("(1'(_,/ _'))")
   3.166 -  "_tuple_arg"  :: "'a => tuple_args"                   ("_")
   3.167 -  "_tuple_args" :: "'a => tuple_args => tuple_args"     ("_,/ _")
   3.168 -  "_pattern"    :: "[pttrn, patterns] => pttrn"         ("'(_,/ _')")
   3.169 -  ""            :: "pttrn => patterns"                  ("_")
   3.170 -  "_patterns"   :: "[pttrn, patterns] => patterns"      ("_,/ _")
   3.171 +  "_tuple"      :: "'a \<Rightarrow> tuple_args \<Rightarrow> 'a \<times> 'b"        ("(1'(_,/ _'))")
   3.172 +  "_tuple_arg"  :: "'a \<Rightarrow> tuple_args"                   ("_")
   3.173 +  "_tuple_args" :: "'a \<Rightarrow> tuple_args \<Rightarrow> tuple_args"     ("_,/ _")
   3.174 +  "_pattern"    :: "pttrn \<Rightarrow> patterns \<Rightarrow> pttrn"         ("'(_,/ _')")
   3.175 +  ""            :: "pttrn \<Rightarrow> patterns"                  ("_")
   3.176 +  "_patterns"   :: "pttrn \<Rightarrow> patterns \<Rightarrow> patterns"      ("_,/ _")
   3.177    "_unit"       :: pttrn                                ("'(')")
   3.178 -
   3.179  translations
   3.180    "(x, y)" \<rightleftharpoons> "CONST Pair x y"
   3.181    "_pattern x y" \<rightleftharpoons> "CONST Pair x y"
   3.182 @@ -356,9 +342,9 @@
   3.183    in [(@{const_syntax case_prod}, K case_prod_guess_names_tr')] end
   3.184  \<close>
   3.185  
   3.186 -text \<open>reconstruct pattern from (nested) @{const case_prod}s,
   3.187 +text \<open>Reconstruct pattern from (nested) @{const case_prod}s,
   3.188    avoiding eta-contraction of body; required for enclosing "let",
   3.189 -  if "let" does not avoid eta-contraction, which has been observed to occur\<close>
   3.190 +  if "let" does not avoid eta-contraction, which has been observed to occur.\<close>
   3.191  
   3.192  print_translation \<open>
   3.193    let
   3.194 @@ -421,19 +407,16 @@
   3.195  
   3.196  subsubsection \<open>Fundamental operations and properties\<close>
   3.197  
   3.198 -lemma Pair_inject:
   3.199 -  assumes "(a, b) = (a', b')"
   3.200 -    and "a = a' \<Longrightarrow> b = b' \<Longrightarrow> R"
   3.201 -  shows R
   3.202 -  using assms by simp
   3.203 +lemma Pair_inject: "(a, b) = (a', b') \<Longrightarrow> (a = a' \<Longrightarrow> b = b' \<Longrightarrow> R) \<Longrightarrow> R"
   3.204 +  by simp
   3.205  
   3.206 -lemma surj_pair [simp]: "EX x y. p = (x, y)"
   3.207 +lemma surj_pair [simp]: "\<exists>x y. p = (x, y)"
   3.208    by (cases p) simp
   3.209  
   3.210 -lemma fst_eqD: "fst (x, y) = a ==> x = a"
   3.211 +lemma fst_eqD: "fst (x, y) = a \<Longrightarrow> x = a"
   3.212    by simp
   3.213  
   3.214 -lemma snd_eqD: "snd (x, y) = a ==> y = a"
   3.215 +lemma snd_eqD: "snd (x, y) = a \<Longrightarrow> y = a"
   3.216    by simp
   3.217  
   3.218  lemma case_prod_unfold [nitpick_unfold]: "case_prod = (\<lambda>c p. c (fst p) (snd p))"
   3.219 @@ -469,25 +452,25 @@
   3.220  lemma The_case_prod: "The (case_prod P) = (THE xy. P (fst xy) (snd xy))"
   3.221    by (simp add: case_prod_unfold)
   3.222  
   3.223 -lemma cond_case_prod_eta: "(!!x y. f x y = g (x, y)) ==> (%(x, y). f x y) = g"
   3.224 +lemma cond_case_prod_eta: "(\<And>x y. f x y = g (x, y)) \<Longrightarrow> (\<lambda>(x, y). f x y) = g"
   3.225    by (simp add: case_prod_eta)
   3.226  
   3.227 -lemma split_paired_all [no_atp]: "(!!x. PROP P x) == (!!a b. PROP P (a, b))"
   3.228 +lemma split_paired_all [no_atp]: "(\<And>x. PROP P x) \<equiv> (\<And>a b. PROP P (a, b))"
   3.229  proof
   3.230    fix a b
   3.231 -  assume "!!x. PROP P x"
   3.232 +  assume "\<And>x. PROP P x"
   3.233    then show "PROP P (a, b)" .
   3.234  next
   3.235    fix x
   3.236 -  assume "!!a b. PROP P (a, b)"
   3.237 +  assume "\<And>a b. PROP P (a, b)"
   3.238    from \<open>PROP P (fst x, snd x)\<close> show "PROP P x" by simp
   3.239  qed
   3.240  
   3.241  text \<open>
   3.242    The rule @{thm [source] split_paired_all} does not work with the
   3.243    Simplifier because it also affects premises in congrence rules,
   3.244 -  where this can lead to premises of the form \<open>!!a b. ... =
   3.245 -  ?P(a, b)\<close> which cannot be solved by reflexivity.
   3.246 +  where this can lead to premises of the form \<open>\<And>a b. \<dots> = ?P(a, b)\<close>
   3.247 +  which cannot be solved by reflexivity.
   3.248  \<close>
   3.249  
   3.250  lemmas split_tupled_all = split_paired_all unit_all_eq2
   3.251 @@ -520,11 +503,11 @@
   3.252  
   3.253  setup \<open>map_theory_claset (fn ctxt => ctxt addSbefore ("split_all_tac", split_all_tac))\<close>
   3.254  
   3.255 -lemma split_paired_All [simp, no_atp]: "(ALL x. P x) = (ALL a b. P (a, b))"
   3.256 +lemma split_paired_All [simp, no_atp]: "(\<forall>x. P x) \<longleftrightarrow> (\<forall>a b. P (a, b))"
   3.257    \<comment> \<open>\<open>[iff]\<close> is not a good idea because it makes \<open>blast\<close> loop\<close>
   3.258    by fast
   3.259  
   3.260 -lemma split_paired_Ex [simp, no_atp]: "(EX x. P x) = (EX a b. P (a, b))"
   3.261 +lemma split_paired_Ex [simp, no_atp]: "(\<exists>x. P x) \<longleftrightarrow> (\<exists>a b. P (a, b))"
   3.262    by fast
   3.263  
   3.264  lemma split_paired_The [no_atp]: "(THE x. P x) = (THE (a, b). P (a, b))"
   3.265 @@ -590,9 +573,9 @@
   3.266    by (auto simp: fun_eq_iff)
   3.267  
   3.268  text \<open>
   3.269 -  \medskip @{const case_prod} used as a logical connective or set former.
   3.270 +  \<^medskip> @{const case_prod} used as a logical connective or set former.
   3.271  
   3.272 -  \medskip These rules are for use with \<open>blast\<close>; could instead
   3.273 +  \<^medskip> These rules are for use with \<open>blast\<close>; could instead
   3.274    call \<open>simp\<close> using @{thm [source] prod.split} as rewrite.\<close>
   3.275  
   3.276  lemma case_prodI2:
   3.277 @@ -621,12 +604,10 @@
   3.278      using q by (simp add: case_prod_unfold)
   3.279  qed
   3.280  
   3.281 -lemma case_prodD':
   3.282 -  "(case (a, b) of (c, d) \<Rightarrow> R c d) c \<Longrightarrow> R a b c"
   3.283 +lemma case_prodD': "(case (a, b) of (c, d) \<Rightarrow> R c d) c \<Longrightarrow> R a b c"
   3.284    by simp
   3.285  
   3.286 -lemma mem_case_prodI:
   3.287 -  "z \<in> c a b \<Longrightarrow> z \<in> (case (a, b) of (d, e) \<Rightarrow> c d e)"
   3.288 +lemma mem_case_prodI: "z \<in> c a b \<Longrightarrow> z \<in> (case (a, b) of (d, e) \<Rightarrow> c d e)"
   3.289    by simp
   3.290  
   3.291  lemma mem_case_prodI2 [intro!]:
   3.292 @@ -661,13 +642,13 @@
   3.293     to quite time-consuming computations (in particular for nested tuples) *)
   3.294  setup \<open>map_theory_claset (fn ctxt => ctxt addSbefore ("split_conv_tac", split_conv_tac))\<close>
   3.295  
   3.296 -lemma split_eta_SetCompr [simp, no_atp]: "(%u. EX x y. u = (x, y) & P (x, y)) = P"
   3.297 +lemma split_eta_SetCompr [simp, no_atp]: "(\<lambda>u. \<exists>x y. u = (x, y) \<and> P (x, y)) = P"
   3.298    by (rule ext) fast
   3.299  
   3.300 -lemma split_eta_SetCompr2 [simp, no_atp]: "(%u. EX x y. u = (x, y) & P x y) = case_prod P"
   3.301 +lemma split_eta_SetCompr2 [simp, no_atp]: "(\<lambda>u. \<exists>x y. u = (x, y) \<and> P x y) = case_prod P"
   3.302    by (rule ext) fast
   3.303  
   3.304 -lemma split_part [simp]: "(%(a,b). P & Q a b) = (%ab. P & case_prod Q ab)"
   3.305 +lemma split_part [simp]: "(\<lambda>(a,b). P \<and> Q a b) = (\<lambda>ab. P \<and> case_prod Q ab)"
   3.306    \<comment> \<open>Allows simplifications of nested splits in case of independent predicates.\<close>
   3.307    by (rule ext) blast
   3.308  
   3.309 @@ -676,16 +657,15 @@
   3.310     b) can lead to nontermination in the presence of split_def
   3.311  *)
   3.312  lemma split_comp_eq: 
   3.313 -  fixes f :: "'a => 'b => 'c" and g :: "'d => 'a"
   3.314 -  shows "(%u. f (g (fst u)) (snd u)) = (case_prod (%x. f (g x)))"
   3.315 +  fixes f :: "'a \<Rightarrow> 'b \<Rightarrow> 'c"
   3.316 +    and g :: "'d \<Rightarrow> 'a"
   3.317 +  shows "(\<lambda>u. f (g (fst u)) (snd u)) = case_prod (\<lambda>x. f (g x))"
   3.318    by (rule ext) auto
   3.319  
   3.320 -lemma pair_imageI [intro]: "(a, b) : A ==> f a b : (%(a, b). f a b) ` A"
   3.321 -  apply (rule_tac x = "(a, b)" in image_eqI)
   3.322 -   apply auto
   3.323 -  done
   3.324 +lemma pair_imageI [intro]: "(a, b) \<in> A \<Longrightarrow> f a b \<in> (\<lambda>(a, b). f a b) ` A"
   3.325 +  by (rule image_eqI [where x = "(a, b)"]) auto
   3.326  
   3.327 -lemma The_split_eq [simp]: "(THE (x',y'). x = x' & y = y') = (x, y)"
   3.328 +lemma The_split_eq [simp]: "(THE (x',y'). x = x' \<and> y = y') = (x, y)"
   3.329    by blast
   3.330  
   3.331  (*
   3.332 @@ -701,8 +681,7 @@
   3.333  qed "The_split_eq";
   3.334  *)
   3.335  
   3.336 -lemma case_prod_beta:
   3.337 -  "case_prod f p = f (fst p) (snd p)"
   3.338 +lemma case_prod_beta: "case_prod f p = f (fst p) (snd p)"
   3.339    by (fact prod.case_eq_if)
   3.340  
   3.341  lemma prod_cases3 [cases type]:
   3.342 @@ -710,7 +689,7 @@
   3.343    by (cases y, case_tac b) blast
   3.344  
   3.345  lemma prod_induct3 [case_names fields, induct type]:
   3.346 -    "(!!a b c. P (a, b, c)) ==> P x"
   3.347 +  "(\<And>a b c. P (a, b, c)) \<Longrightarrow> P x"
   3.348    by (cases x) blast
   3.349  
   3.350  lemma prod_cases4 [cases type]:
   3.351 @@ -718,7 +697,7 @@
   3.352    by (cases y, case_tac c) blast
   3.353  
   3.354  lemma prod_induct4 [case_names fields, induct type]:
   3.355 -    "(!!a b c d. P (a, b, c, d)) ==> P x"
   3.356 +  "(\<And>a b c d. P (a, b, c, d)) \<Longrightarrow> P x"
   3.357    by (cases x) blast
   3.358  
   3.359  lemma prod_cases5 [cases type]:
   3.360 @@ -726,7 +705,7 @@
   3.361    by (cases y, case_tac d) blast
   3.362  
   3.363  lemma prod_induct5 [case_names fields, induct type]:
   3.364 -    "(!!a b c d e. P (a, b, c, d, e)) ==> P x"
   3.365 +  "(\<And>a b c d e. P (a, b, c, d, e)) \<Longrightarrow> P x"
   3.366    by (cases x) blast
   3.367  
   3.368  lemma prod_cases6 [cases type]:
   3.369 @@ -734,7 +713,7 @@
   3.370    by (cases y, case_tac e) blast
   3.371  
   3.372  lemma prod_induct6 [case_names fields, induct type]:
   3.373 -    "(!!a b c d e f. P (a, b, c, d, e, f)) ==> P x"
   3.374 +  "(\<And>a b c d e f. P (a, b, c, d, e, f)) \<Longrightarrow> P x"
   3.375    by (cases x) blast
   3.376  
   3.377  lemma prod_cases7 [cases type]:
   3.378 @@ -742,11 +721,11 @@
   3.379    by (cases y, case_tac f) blast
   3.380  
   3.381  lemma prod_induct7 [case_names fields, induct type]:
   3.382 -    "(!!a b c d e f g. P (a, b, c, d, e, f, g)) ==> P x"
   3.383 +  "(\<And>a b c d e f g. P (a, b, c, d, e, f, g)) \<Longrightarrow> P x"
   3.384    by (cases x) blast
   3.385  
   3.386 -definition internal_case_prod :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'a \<times> 'b \<Rightarrow> 'c" where
   3.387 -  "internal_case_prod == case_prod"
   3.388 +definition internal_case_prod :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'a \<times> 'b \<Rightarrow> 'c"
   3.389 +  where "internal_case_prod \<equiv> case_prod"
   3.390  
   3.391  lemma internal_case_prod_conv: "internal_case_prod c (a, b) = c a b"
   3.392    by (simp only: internal_case_prod_def case_prod_conv)
   3.393 @@ -758,8 +737,8 @@
   3.394  
   3.395  subsubsection \<open>Derived operations\<close>
   3.396  
   3.397 -definition curry :: "('a \<times> 'b \<Rightarrow> 'c) \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'c" where
   3.398 -  "curry = (\<lambda>c x y. c (x, y))"
   3.399 +definition curry :: "('a \<times> 'b \<Rightarrow> 'c) \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'c"
   3.400 +  where "curry = (\<lambda>c x y. c (x, y))"
   3.401  
   3.402  lemma curry_conv [simp, code]: "curry f a b = f (a, b)"
   3.403    by (simp add: curry_def)
   3.404 @@ -780,16 +759,14 @@
   3.405    by (simp add: curry_def case_prod_unfold)
   3.406  
   3.407  lemma curry_K: "curry (\<lambda>x. c) = (\<lambda>x y. c)"
   3.408 -by(simp add: fun_eq_iff)
   3.409 +  by (simp add: fun_eq_iff)
   3.410  
   3.411 -text \<open>
   3.412 -  The composition-uncurry combinator.
   3.413 -\<close>
   3.414 +text \<open>The composition-uncurry combinator.\<close>
   3.415  
   3.416  notation fcomp (infixl "\<circ>>" 60)
   3.417  
   3.418 -definition scomp :: "('a \<Rightarrow> 'b \<times> 'c) \<Rightarrow> ('b \<Rightarrow> 'c \<Rightarrow> 'd) \<Rightarrow> 'a \<Rightarrow> 'd" (infixl "\<circ>\<rightarrow>" 60) where
   3.419 -  "f \<circ>\<rightarrow> g = (\<lambda>x. case_prod g (f x))"
   3.420 +definition scomp :: "('a \<Rightarrow> 'b \<times> 'c) \<Rightarrow> ('b \<Rightarrow> 'c \<Rightarrow> 'd) \<Rightarrow> 'a \<Rightarrow> 'd"  (infixl "\<circ>\<rightarrow>" 60)
   3.421 +  where "f \<circ>\<rightarrow> g = (\<lambda>x. case_prod g (f x))"
   3.422  
   3.423  lemma scomp_unfold: "scomp = (\<lambda>f g x. g (fst (f x)) (snd (f x)))"
   3.424    by (simp add: fun_eq_iff scomp_def case_prod_unfold)
   3.425 @@ -819,46 +796,37 @@
   3.426  no_notation scomp (infixl "\<circ>\<rightarrow>" 60)
   3.427  
   3.428  text \<open>
   3.429 -  @{term map_prod} --- action of the product functor upon
   3.430 -  functions.
   3.431 +  @{term map_prod} --- action of the product functor upon functions.
   3.432  \<close>
   3.433  
   3.434 -definition map_prod :: "('a \<Rightarrow> 'c) \<Rightarrow> ('b \<Rightarrow> 'd) \<Rightarrow> 'a \<times> 'b \<Rightarrow> 'c \<times> 'd" where
   3.435 -  "map_prod f g = (\<lambda>(x, y). (f x, g y))"
   3.436 +definition map_prod :: "('a \<Rightarrow> 'c) \<Rightarrow> ('b \<Rightarrow> 'd) \<Rightarrow> 'a \<times> 'b \<Rightarrow> 'c \<times> 'd"
   3.437 +  where "map_prod f g = (\<lambda>(x, y). (f x, g y))"
   3.438  
   3.439 -lemma map_prod_simp [simp, code]:
   3.440 -  "map_prod f g (a, b) = (f a, g b)"
   3.441 +lemma map_prod_simp [simp, code]: "map_prod f g (a, b) = (f a, g b)"
   3.442    by (simp add: map_prod_def)
   3.443  
   3.444  functor map_prod: map_prod
   3.445    by (auto simp add: split_paired_all)
   3.446  
   3.447 -lemma fst_map_prod [simp]:
   3.448 -  "fst (map_prod f g x) = f (fst x)"
   3.449 +lemma fst_map_prod [simp]: "fst (map_prod f g x) = f (fst x)"
   3.450    by (cases x) simp_all
   3.451  
   3.452 -lemma snd_map_prod [simp]:
   3.453 -  "snd (map_prod f g x) = g (snd x)"
   3.454 +lemma snd_map_prod [simp]: "snd (map_prod f g x) = g (snd x)"
   3.455    by (cases x) simp_all
   3.456  
   3.457 -lemma fst_comp_map_prod [simp]:
   3.458 -  "fst \<circ> map_prod f g = f \<circ> fst"
   3.459 +lemma fst_comp_map_prod [simp]: "fst \<circ> map_prod f g = f \<circ> fst"
   3.460    by (rule ext) simp_all
   3.461  
   3.462 -lemma snd_comp_map_prod [simp]:
   3.463 -  "snd \<circ> map_prod f g = g \<circ> snd"
   3.464 +lemma snd_comp_map_prod [simp]: "snd \<circ> map_prod f g = g \<circ> snd"
   3.465    by (rule ext) simp_all
   3.466  
   3.467 -lemma map_prod_compose:
   3.468 -  "map_prod (f1 o f2) (g1 o g2) = (map_prod f1 g1 o map_prod f2 g2)"
   3.469 +lemma map_prod_compose: "map_prod (f1 \<circ> f2) (g1 \<circ> g2) = (map_prod f1 g1 \<circ> map_prod f2 g2)"
   3.470    by (rule ext) (simp add: map_prod.compositionality comp_def)
   3.471  
   3.472 -lemma map_prod_ident [simp]:
   3.473 -  "map_prod (%x. x) (%y. y) = (%z. z)"
   3.474 +lemma map_prod_ident [simp]: "map_prod (\<lambda>x. x) (\<lambda>y. y) = (\<lambda>z. z)"
   3.475    by (rule ext) (simp add: map_prod.identity)
   3.476  
   3.477 -lemma map_prod_imageI [intro]:
   3.478 -  "(a, b) \<in> R \<Longrightarrow> (f a, g b) \<in> map_prod f g ` R"
   3.479 +lemma map_prod_imageI [intro]: "(a, b) \<in> R \<Longrightarrow> (f a, g b) \<in> map_prod f g ` R"
   3.480    by (rule image_eqI) simp_all
   3.481  
   3.482  lemma prod_fun_imageE [elim!]:
   3.483 @@ -871,86 +839,67 @@
   3.484    apply simp_all
   3.485    done
   3.486  
   3.487 -definition apfst :: "('a \<Rightarrow> 'c) \<Rightarrow> 'a \<times> 'b \<Rightarrow> 'c \<times> 'b" where
   3.488 -  "apfst f = map_prod f id"
   3.489 +definition apfst :: "('a \<Rightarrow> 'c) \<Rightarrow> 'a \<times> 'b \<Rightarrow> 'c \<times> 'b"
   3.490 +  where "apfst f = map_prod f id"
   3.491  
   3.492 -definition apsnd :: "('b \<Rightarrow> 'c) \<Rightarrow> 'a \<times> 'b \<Rightarrow> 'a \<times> 'c" where
   3.493 -  "apsnd f = map_prod id f"
   3.494 +definition apsnd :: "('b \<Rightarrow> 'c) \<Rightarrow> 'a \<times> 'b \<Rightarrow> 'a \<times> 'c"
   3.495 +  where "apsnd f = map_prod id f"
   3.496  
   3.497 -lemma apfst_conv [simp, code]:
   3.498 -  "apfst f (x, y) = (f x, y)" 
   3.499 +lemma apfst_conv [simp, code]: "apfst f (x, y) = (f x, y)" 
   3.500    by (simp add: apfst_def)
   3.501  
   3.502 -lemma apsnd_conv [simp, code]:
   3.503 -  "apsnd f (x, y) = (x, f y)" 
   3.504 +lemma apsnd_conv [simp, code]: "apsnd f (x, y) = (x, f y)" 
   3.505    by (simp add: apsnd_def)
   3.506  
   3.507 -lemma fst_apfst [simp]:
   3.508 -  "fst (apfst f x) = f (fst x)"
   3.509 +lemma fst_apfst [simp]: "fst (apfst f x) = f (fst x)"
   3.510    by (cases x) simp
   3.511  
   3.512 -lemma fst_comp_apfst [simp]:
   3.513 -  "fst \<circ> apfst f = f \<circ> fst"
   3.514 +lemma fst_comp_apfst [simp]: "fst \<circ> apfst f = f \<circ> fst"
   3.515    by (simp add: fun_eq_iff)
   3.516  
   3.517 -lemma fst_apsnd [simp]:
   3.518 -  "fst (apsnd f x) = fst x"
   3.519 +lemma fst_apsnd [simp]: "fst (apsnd f x) = fst x"
   3.520    by (cases x) simp
   3.521  
   3.522 -lemma fst_comp_apsnd [simp]:
   3.523 -  "fst \<circ> apsnd f = fst"
   3.524 +lemma fst_comp_apsnd [simp]: "fst \<circ> apsnd f = fst"
   3.525    by (simp add: fun_eq_iff)
   3.526  
   3.527 -lemma snd_apfst [simp]:
   3.528 -  "snd (apfst f x) = snd x"
   3.529 +lemma snd_apfst [simp]: "snd (apfst f x) = snd x"
   3.530    by (cases x) simp
   3.531  
   3.532 -lemma snd_comp_apfst [simp]:
   3.533 -  "snd \<circ> apfst f = snd"
   3.534 +lemma snd_comp_apfst [simp]: "snd \<circ> apfst f = snd"
   3.535    by (simp add: fun_eq_iff)
   3.536  
   3.537 -lemma snd_apsnd [simp]:
   3.538 -  "snd (apsnd f x) = f (snd x)"
   3.539 +lemma snd_apsnd [simp]: "snd (apsnd f x) = f (snd x)"
   3.540    by (cases x) simp
   3.541  
   3.542 -lemma snd_comp_apsnd [simp]:
   3.543 -  "snd \<circ> apsnd f = f \<circ> snd"
   3.544 +lemma snd_comp_apsnd [simp]: "snd \<circ> apsnd f = f \<circ> snd"
   3.545    by (simp add: fun_eq_iff)
   3.546  
   3.547 -lemma apfst_compose:
   3.548 -  "apfst f (apfst g x) = apfst (f \<circ> g) x"
   3.549 +lemma apfst_compose: "apfst f (apfst g x) = apfst (f \<circ> g) x"
   3.550    by (cases x) simp
   3.551  
   3.552 -lemma apsnd_compose:
   3.553 -  "apsnd f (apsnd g x) = apsnd (f \<circ> g) x"
   3.554 +lemma apsnd_compose: "apsnd f (apsnd g x) = apsnd (f \<circ> g) x"
   3.555    by (cases x) simp
   3.556  
   3.557 -lemma apfst_apsnd [simp]:
   3.558 -  "apfst f (apsnd g x) = (f (fst x), g (snd x))"
   3.559 +lemma apfst_apsnd [simp]: "apfst f (apsnd g x) = (f (fst x), g (snd x))"
   3.560    by (cases x) simp
   3.561  
   3.562 -lemma apsnd_apfst [simp]:
   3.563 -  "apsnd f (apfst g x) = (g (fst x), f (snd x))"
   3.564 +lemma apsnd_apfst [simp]: "apsnd f (apfst g x) = (g (fst x), f (snd x))"
   3.565    by (cases x) simp
   3.566  
   3.567 -lemma apfst_id [simp] :
   3.568 -  "apfst id = id"
   3.569 +lemma apfst_id [simp]: "apfst id = id"
   3.570    by (simp add: fun_eq_iff)
   3.571  
   3.572 -lemma apsnd_id [simp] :
   3.573 -  "apsnd id = id"
   3.574 +lemma apsnd_id [simp]: "apsnd id = id"
   3.575    by (simp add: fun_eq_iff)
   3.576  
   3.577 -lemma apfst_eq_conv [simp]:
   3.578 -  "apfst f x = apfst g x \<longleftrightarrow> f (fst x) = g (fst x)"
   3.579 +lemma apfst_eq_conv [simp]: "apfst f x = apfst g x \<longleftrightarrow> f (fst x) = g (fst x)"
   3.580    by (cases x) simp
   3.581  
   3.582 -lemma apsnd_eq_conv [simp]:
   3.583 -  "apsnd f x = apsnd g x \<longleftrightarrow> f (snd x) = g (snd x)"
   3.584 +lemma apsnd_eq_conv [simp]: "apsnd f x = apsnd g x \<longleftrightarrow> f (snd x) = g (snd x)"
   3.585    by (cases x) simp
   3.586  
   3.587 -lemma apsnd_apfst_commute:
   3.588 -  "apsnd f (apfst g p) = apfst g (apsnd f p)"
   3.589 +lemma apsnd_apfst_commute: "apsnd f (apfst g p) = apfst g (apsnd f p)"
   3.590    by simp
   3.591  
   3.592  context
   3.593 @@ -959,104 +908,83 @@
   3.594  local_setup \<open>Local_Theory.map_background_naming (Name_Space.mandatory_path "prod")\<close>
   3.595  
   3.596  definition swap :: "'a \<times> 'b \<Rightarrow> 'b \<times> 'a"
   3.597 -where
   3.598 -  "swap p = (snd p, fst p)"
   3.599 +  where "swap p = (snd p, fst p)"
   3.600  
   3.601  end
   3.602  
   3.603 -lemma swap_simp [simp]:
   3.604 -  "prod.swap (x, y) = (y, x)"
   3.605 +lemma swap_simp [simp]: "prod.swap (x, y) = (y, x)"
   3.606    by (simp add: prod.swap_def)
   3.607  
   3.608 -lemma swap_swap [simp]:
   3.609 -  "prod.swap (prod.swap p) = p"
   3.610 +lemma swap_swap [simp]: "prod.swap (prod.swap p) = p"
   3.611    by (cases p) simp
   3.612  
   3.613 -lemma swap_comp_swap [simp]:
   3.614 -  "prod.swap \<circ> prod.swap = id"
   3.615 +lemma swap_comp_swap [simp]: "prod.swap \<circ> prod.swap = id"
   3.616    by (simp add: fun_eq_iff)
   3.617  
   3.618 -lemma pair_in_swap_image [simp]:
   3.619 -  "(y, x) \<in> prod.swap ` A \<longleftrightarrow> (x, y) \<in> A"
   3.620 +lemma pair_in_swap_image [simp]: "(y, x) \<in> prod.swap ` A \<longleftrightarrow> (x, y) \<in> A"
   3.621    by (auto intro!: image_eqI)
   3.622  
   3.623 -lemma inj_swap [simp]:
   3.624 -  "inj_on prod.swap A"
   3.625 +lemma inj_swap [simp]: "inj_on prod.swap A"
   3.626    by (rule inj_onI) auto
   3.627  
   3.628 -lemma swap_inj_on:
   3.629 -  "inj_on (\<lambda>(i, j). (j, i)) A"
   3.630 +lemma swap_inj_on: "inj_on (\<lambda>(i, j). (j, i)) A"
   3.631    by (rule inj_onI) auto
   3.632  
   3.633 -lemma surj_swap [simp]:
   3.634 -  "surj prod.swap"
   3.635 +lemma surj_swap [simp]: "surj prod.swap"
   3.636    by (rule surjI [of _ prod.swap]) simp
   3.637  
   3.638 -lemma bij_swap [simp]:
   3.639 -  "bij prod.swap"
   3.640 +lemma bij_swap [simp]: "bij prod.swap"
   3.641    by (simp add: bij_def)
   3.642  
   3.643 -lemma case_swap [simp]:
   3.644 -  "(case prod.swap p of (y, x) \<Rightarrow> f x y) = (case p of (x, y) \<Rightarrow> f x y)"
   3.645 +lemma case_swap [simp]: "(case prod.swap p of (y, x) \<Rightarrow> f x y) = (case p of (x, y) \<Rightarrow> f x y)"
   3.646    by (cases p) simp
   3.647  
   3.648  lemma fst_swap [simp]: "fst (prod.swap x) = snd x"
   3.649 -by(cases x) simp
   3.650 +  by (cases x) simp
   3.651  
   3.652  lemma snd_swap [simp]: "snd (prod.swap x) = fst x"
   3.653 -by(cases x) simp
   3.654 +  by (cases x) simp
   3.655  
   3.656 -text \<open>
   3.657 -  Disjoint union of a family of sets -- Sigma.
   3.658 -\<close>
   3.659 +text \<open>Disjoint union of a family of sets -- Sigma.\<close>
   3.660  
   3.661 -definition Sigma :: "'a set \<Rightarrow> ('a \<Rightarrow> 'b set) \<Rightarrow> ('a \<times> 'b) set" where
   3.662 -  Sigma_def: "Sigma A B == UN x:A. UN y:B x. {Pair x y}"
   3.663 +definition Sigma :: "'a set \<Rightarrow> ('a \<Rightarrow> 'b set) \<Rightarrow> ('a \<times> 'b) set"
   3.664 +  where "Sigma A B \<equiv> \<Union>x\<in>A. \<Union>y\<in>B x. {Pair x y}"
   3.665  
   3.666 -abbreviation
   3.667 -  Times :: "'a set \<Rightarrow> 'b set \<Rightarrow> ('a \<times> 'b) set"  (infixr "\<times>" 80) where
   3.668 -  "A \<times> B == Sigma A (%_. B)"
   3.669 +abbreviation Times :: "'a set \<Rightarrow> 'b set \<Rightarrow> ('a \<times> 'b) set"  (infixr "\<times>" 80)
   3.670 +  where "A \<times> B \<equiv> Sigma A (\<lambda>_. B)"
   3.671  
   3.672  hide_const (open) Times
   3.673  
   3.674  syntax
   3.675 -  "_Sigma" :: "[pttrn, 'a set, 'b set] => ('a * 'b) set"  ("(3SIGMA _:_./ _)" [0, 0, 10] 10)
   3.676 +  "_Sigma" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b set \<Rightarrow> ('a \<times> 'b) set"  ("(3SIGMA _:_./ _)" [0, 0, 10] 10)
   3.677  translations
   3.678 -  "SIGMA x:A. B" == "CONST Sigma A (%x. B)"
   3.679 -
   3.680 -lemma SigmaI [intro!]: "[| a:A;  b:B(a) |] ==> (a,b) : Sigma A B"
   3.681 -  by (unfold Sigma_def) blast
   3.682 +  "SIGMA x:A. B" \<rightleftharpoons> "CONST Sigma A (\<lambda>x. B)"
   3.683  
   3.684 -lemma SigmaE [elim!]:
   3.685 -    "[| c: Sigma A B;
   3.686 -        !!x y.[| x:A;  y:B(x);  c=(x,y) |] ==> P
   3.687 -     |] ==> P"
   3.688 +lemma SigmaI [intro!]: "a \<in> A \<Longrightarrow> b \<in> B a \<Longrightarrow> (a, b) \<in> Sigma A B"
   3.689 +  unfolding Sigma_def by blast
   3.690 +
   3.691 +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"
   3.692    \<comment> \<open>The general elimination rule.\<close>
   3.693 -  by (unfold Sigma_def) blast
   3.694 +  unfolding Sigma_def by blast
   3.695  
   3.696  text \<open>
   3.697 -  Elimination of @{term "(a, b) : A \<times> B"} -- introduces no
   3.698 +  Elimination of @{term "(a, b) \<in> A \<times> B"} -- introduces no
   3.699    eigenvariables.
   3.700  \<close>
   3.701  
   3.702 -lemma SigmaD1: "(a, b) : Sigma A B ==> a : A"
   3.703 +lemma SigmaD1: "(a, b) \<in> Sigma A B \<Longrightarrow> a \<in> A"
   3.704    by blast
   3.705  
   3.706 -lemma SigmaD2: "(a, b) : Sigma A B ==> b : B a"
   3.707 +lemma SigmaD2: "(a, b) \<in> Sigma A B \<Longrightarrow> b \<in> B a"
   3.708    by blast
   3.709  
   3.710 -lemma SigmaE2:
   3.711 -    "[| (a, b) : Sigma A B;
   3.712 -        [| a:A;  b:B(a) |] ==> P
   3.713 -     |] ==> P"
   3.714 +lemma SigmaE2: "(a, b) \<in> Sigma A B \<Longrightarrow> (a \<in> A \<Longrightarrow> b \<in> B a \<Longrightarrow> P) \<Longrightarrow> P"
   3.715    by blast
   3.716  
   3.717 -lemma Sigma_cong:
   3.718 -     "\<lbrakk>A = B; !!x. x \<in> B \<Longrightarrow> C x = D x\<rbrakk>
   3.719 -      \<Longrightarrow> (SIGMA x: A. C x) = (SIGMA x: B. D x)"
   3.720 +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)"
   3.721    by auto
   3.722  
   3.723 -lemma Sigma_mono: "[| A <= C; !!x. x:A ==> B x <= D x |] ==> Sigma A B <= Sigma C D"
   3.724 +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"
   3.725    by blast
   3.726  
   3.727  lemma Sigma_empty1 [simp]: "Sigma {} B = {}"
   3.728 @@ -1074,7 +1002,7 @@
   3.729  lemma Compl_Times_UNIV2 [simp]: "- (A \<times> UNIV) = (-A) \<times> UNIV"
   3.730    by auto
   3.731  
   3.732 -lemma mem_Sigma_iff [iff]: "((a,b): Sigma A B) = (a:A & b:B(a))"
   3.733 +lemma mem_Sigma_iff [iff]: "(a, b) \<in> Sigma A B \<longleftrightarrow> a \<in> A \<and> b \<in> B a"
   3.734    by blast
   3.735  
   3.736  lemma mem_Times_iff: "x \<in> A \<times> B \<longleftrightarrow> fst x \<in> A \<and> snd x \<in> B"
   3.737 @@ -1083,26 +1011,22 @@
   3.738  lemma Sigma_empty_iff: "(SIGMA i:I. X i) = {} \<longleftrightarrow> (\<forall>i\<in>I. X i = {})"
   3.739    by auto
   3.740  
   3.741 -lemma Times_subset_cancel2: "x:C ==> (A \<times> C <= B \<times> C) = (A <= B)"
   3.742 -  by blast
   3.743 -
   3.744 -lemma Times_eq_cancel2: "x:C ==> (A \<times> C = B \<times> C) = (A = B)"
   3.745 -  by (blast elim: equalityE)
   3.746 -
   3.747 -lemma Collect_case_prod_Sigma:
   3.748 -  "{(x, y). P x \<and> Q x y} = (SIGMA x:Collect P. Collect (Q x))"
   3.749 +lemma Times_subset_cancel2: "x \<in> C \<Longrightarrow> A \<times> C \<subseteq> B \<times> C \<longleftrightarrow> A \<subseteq> B"
   3.750    by blast
   3.751  
   3.752 -lemma Collect_case_prod [simp]:
   3.753 -  "{(a, b). P a \<and> Q b} = Collect P \<times> Collect Q "
   3.754 +lemma Times_eq_cancel2: "x \<in> C \<Longrightarrow> A \<times> C = B \<times> C \<longleftrightarrow> A = B"
   3.755 +  by (blast elim: equalityE)
   3.756 +
   3.757 +lemma Collect_case_prod_Sigma: "{(x, y). P x \<and> Q x y} = (SIGMA x:Collect P. Collect (Q x))"
   3.758 +  by blast
   3.759 +
   3.760 +lemma Collect_case_prod [simp]: "{(a, b). P a \<and> Q b} = Collect P \<times> Collect Q "
   3.761    by (fact Collect_case_prod_Sigma)
   3.762  
   3.763 -lemma Collect_case_prodD:
   3.764 -  "x \<in> Collect (case_prod A) \<Longrightarrow> A (fst x) (snd x)"
   3.765 +lemma Collect_case_prodD: "x \<in> Collect (case_prod A) \<Longrightarrow> A (fst x) (snd x)"
   3.766    by auto
   3.767  
   3.768 -lemma Collect_case_prod_mono:
   3.769 -  "A \<le> B \<Longrightarrow> Collect (case_prod A) \<subseteq> Collect (case_prod B)"
   3.770 +lemma Collect_case_prod_mono: "A \<le> B \<Longrightarrow> Collect (case_prod A) \<subseteq> Collect (case_prod B)"
   3.771    by auto (auto elim!: le_funE)
   3.772  
   3.773  lemma Collect_split_mono_strong: 
   3.774 @@ -1110,45 +1034,35 @@
   3.775      \<Longrightarrow> A \<subseteq> Collect (case_prod P) \<Longrightarrow> A \<subseteq> Collect (case_prod Q)"
   3.776    by fastforce
   3.777    
   3.778 -lemma UN_Times_distrib:
   3.779 -  "(\<Union>(a, b)\<in>A \<times> B. E a \<times> F b) = UNION A E \<times> UNION B F"
   3.780 +lemma UN_Times_distrib: "(\<Union>(a, b)\<in>A \<times> B. E a \<times> F b) = UNION A E \<times> UNION B F"
   3.781    \<comment> \<open>Suggested by Pierre Chartier\<close>
   3.782    by blast
   3.783  
   3.784 -lemma split_paired_Ball_Sigma [simp, no_atp]:
   3.785 -  "(\<forall>z\<in>Sigma A B. P z) \<longleftrightarrow> (\<forall>x\<in>A. \<forall>y\<in>B x. P (x, y))"
   3.786 +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))"
   3.787    by blast
   3.788  
   3.789 -lemma split_paired_Bex_Sigma [simp, no_atp]:
   3.790 -  "(\<exists>z\<in>Sigma A B. P z) \<longleftrightarrow> (\<exists>x\<in>A. \<exists>y\<in>B x. P (x, y))"
   3.791 +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))"
   3.792    by blast
   3.793  
   3.794 -lemma Sigma_Un_distrib1:
   3.795 -  "Sigma (I \<union> J) C = Sigma I C \<union> Sigma J C"
   3.796 +lemma Sigma_Un_distrib1: "Sigma (I \<union> J) C = Sigma I C \<union> Sigma J C"
   3.797    by blast
   3.798  
   3.799 -lemma Sigma_Un_distrib2:
   3.800 -  "(SIGMA i:I. A i \<union> B i) = Sigma I A \<union> Sigma I B"
   3.801 +lemma Sigma_Un_distrib2: "(SIGMA i:I. A i \<union> B i) = Sigma I A \<union> Sigma I B"
   3.802    by blast
   3.803  
   3.804 -lemma Sigma_Int_distrib1:
   3.805 -  "Sigma (I \<inter> J) C = Sigma I C \<inter> Sigma J C"
   3.806 +lemma Sigma_Int_distrib1: "Sigma (I \<inter> J) C = Sigma I C \<inter> Sigma J C"
   3.807    by blast
   3.808  
   3.809 -lemma Sigma_Int_distrib2:
   3.810 -  "(SIGMA i:I. A i \<inter> B i) = Sigma I A \<inter> Sigma I B"
   3.811 +lemma Sigma_Int_distrib2: "(SIGMA i:I. A i \<inter> B i) = Sigma I A \<inter> Sigma I B"
   3.812    by blast
   3.813  
   3.814 -lemma Sigma_Diff_distrib1:
   3.815 -  "Sigma (I - J) C = Sigma I C - Sigma J C"
   3.816 +lemma Sigma_Diff_distrib1: "Sigma (I - J) C = Sigma I C - Sigma J C"
   3.817    by blast
   3.818  
   3.819 -lemma Sigma_Diff_distrib2:
   3.820 -  "(SIGMA i:I. A i - B i) = Sigma I A - Sigma I B"
   3.821 +lemma Sigma_Diff_distrib2: "(SIGMA i:I. A i - B i) = Sigma I A - Sigma I B"
   3.822    by blast
   3.823  
   3.824 -lemma Sigma_Union:
   3.825 -  "Sigma (\<Union>X) B = (\<Union>A\<in>X. Sigma A B)"
   3.826 +lemma Sigma_Union: "Sigma (\<Union>X) B = (\<Union>A\<in>X. Sigma A B)"
   3.827    by blast
   3.828  
   3.829  lemma Pair_vimage_Sigma: "Pair x -` Sigma A f = (if x \<in> A then f x else {})"
   3.830 @@ -1159,79 +1073,62 @@
   3.831    matching, especially when the rules are re-oriented.
   3.832  \<close>
   3.833  
   3.834 -lemma Times_Un_distrib1:
   3.835 -  "(A \<union> B) \<times> C = A \<times> C \<union> B \<times> C "
   3.836 +lemma Times_Un_distrib1: "(A \<union> B) \<times> C = A \<times> C \<union> B \<times> C "
   3.837    by (fact Sigma_Un_distrib1)
   3.838  
   3.839 -lemma Times_Int_distrib1:
   3.840 -  "(A \<inter> B) \<times> C = A \<times> C \<inter> B \<times> C "
   3.841 +lemma Times_Int_distrib1: "(A \<inter> B) \<times> C = A \<times> C \<inter> B \<times> C "
   3.842    by (fact Sigma_Int_distrib1)
   3.843  
   3.844 -lemma Times_Diff_distrib1:
   3.845 -  "(A - B) \<times> C = A \<times> C - B \<times> C "
   3.846 +lemma Times_Diff_distrib1: "(A - B) \<times> C = A \<times> C - B \<times> C "
   3.847    by (fact Sigma_Diff_distrib1)
   3.848  
   3.849 -lemma Times_empty [simp]:
   3.850 -  "A \<times> B = {} \<longleftrightarrow> A = {} \<or> B = {}"
   3.851 +lemma Times_empty [simp]: "A \<times> B = {} \<longleftrightarrow> A = {} \<or> B = {}"
   3.852    by auto
   3.853  
   3.854 -lemma times_eq_iff:
   3.855 -  "A \<times> B = C \<times> D \<longleftrightarrow> A = C \<and> B = D \<or> (A = {} \<or> B = {}) \<and> (C = {} \<or> D = {})"
   3.856 +lemma times_eq_iff: "A \<times> B = C \<times> D \<longleftrightarrow> A = C \<and> B = D \<or> (A = {} \<or> B = {}) \<and> (C = {} \<or> D = {})"
   3.857    by auto
   3.858  
   3.859 -lemma fst_image_times [simp]:
   3.860 -  "fst ` (A \<times> B) = (if B = {} then {} else A)"
   3.861 +lemma fst_image_times [simp]: "fst ` (A \<times> B) = (if B = {} then {} else A)"
   3.862    by force
   3.863  
   3.864 -lemma snd_image_times [simp]:
   3.865 -  "snd ` (A \<times> B) = (if A = {} then {} else B)"
   3.866 +lemma snd_image_times [simp]: "snd ` (A \<times> B) = (if A = {} then {} else B)"
   3.867    by force
   3.868  
   3.869 -lemma fst_image_Sigma:
   3.870 -  "fst ` (Sigma A B) = {x \<in> A. B(x) \<noteq> {}}"
   3.871 +lemma fst_image_Sigma: "fst ` (Sigma A B) = {x \<in> A. B(x) \<noteq> {}}"
   3.872    by force
   3.873  
   3.874 -lemma snd_image_Sigma:
   3.875 -  "snd ` (Sigma A B) = (\<Union> x \<in> A. B x)"
   3.876 +lemma snd_image_Sigma: "snd ` (Sigma A B) = (\<Union> x \<in> A. B x)"
   3.877    by force
   3.878  
   3.879 -lemma vimage_fst:
   3.880 -  "fst -` A = A \<times> UNIV"
   3.881 +lemma vimage_fst: "fst -` A = A \<times> UNIV"
   3.882    by auto
   3.883  
   3.884 -lemma vimage_snd:
   3.885 -  "snd -` A = UNIV \<times> A"
   3.886 +lemma vimage_snd: "snd -` A = UNIV \<times> A"
   3.887    by auto
   3.888  
   3.889 -lemma insert_times_insert[simp]:
   3.890 -  "insert a A \<times> insert b B =
   3.891 -   insert (a,b) (A \<times> insert b B \<union> insert a A \<times> B)"
   3.892 +lemma insert_times_insert [simp]:
   3.893 +  "insert a A \<times> insert b B = insert (a,b) (A \<times> insert b B \<union> insert a A \<times> B)"
   3.894    by blast
   3.895  
   3.896 -lemma vimage_Times:
   3.897 -  "f -` (A \<times> B) = (fst \<circ> f) -` A \<inter> (snd \<circ> f) -` B"
   3.898 +lemma vimage_Times: "f -` (A \<times> B) = (fst \<circ> f) -` A \<inter> (snd \<circ> f) -` B"
   3.899  proof (rule set_eqI)
   3.900 -  fix x
   3.901 -  show "x \<in> f -` (A \<times> B) \<longleftrightarrow> x \<in> (fst \<circ> f) -` A \<inter> (snd \<circ> f) -` B"
   3.902 +  show "x \<in> f -` (A \<times> B) \<longleftrightarrow> x \<in> (fst \<circ> f) -` A \<inter> (snd \<circ> f) -` B" for x
   3.903      by (cases "f x") (auto split: prod.split)
   3.904  qed
   3.905  
   3.906 -lemma times_Int_times:
   3.907 -  "A \<times> B \<inter> C \<times> D = (A \<inter> C) \<times> (B \<inter> D)"
   3.908 +lemma times_Int_times: "A \<times> B \<inter> C \<times> D = (A \<inter> C) \<times> (B \<inter> D)"
   3.909    by auto
   3.910  
   3.911 -lemma product_swap:
   3.912 -  "prod.swap ` (A \<times> B) = B \<times> A"
   3.913 +lemma product_swap: "prod.swap ` (A \<times> B) = B \<times> A"
   3.914    by (auto simp add: set_eq_iff)
   3.915  
   3.916 -lemma swap_product:
   3.917 -  "(\<lambda>(i, j). (j, i)) ` (A \<times> B) = B \<times> A"
   3.918 +lemma swap_product: "(\<lambda>(i, j). (j, i)) ` (A \<times> B) = B \<times> A"
   3.919    by (auto simp add: set_eq_iff)
   3.920  
   3.921 -lemma image_split_eq_Sigma:
   3.922 -  "(\<lambda>x. (f x, g x)) ` A = Sigma (f ` A) (\<lambda>x. g ` (f -` {x} \<inter> A))"
   3.923 +lemma image_split_eq_Sigma: "(\<lambda>x. (f x, g x)) ` A = Sigma (f ` A) (\<lambda>x. g ` (f -` {x} \<inter> A))"
   3.924  proof (safe intro!: imageI)
   3.925 -  fix a b assume *: "a \<in> A" "b \<in> A" and eq: "f a = f b"
   3.926 +  fix a b
   3.927 +  assume *: "a \<in> A" "b \<in> A" and eq: "f a = f b"
   3.928    show "(f b, g a) \<in> (\<lambda>x. (f x, g x)) ` A"
   3.929      using * eq[symmetric] by auto
   3.930  qed simp_all
   3.931 @@ -1240,16 +1137,16 @@
   3.932    by force
   3.933  
   3.934  lemma inj_on_apfst [simp]: "inj_on (apfst f) (A \<times> UNIV) \<longleftrightarrow> inj_on f A"
   3.935 -by(auto simp add: inj_on_def)
   3.936 +  by (auto simp add: inj_on_def)
   3.937  
   3.938  lemma inj_apfst [simp]: "inj (apfst f) \<longleftrightarrow> inj f"
   3.939 -using inj_on_apfst[of f UNIV] by simp
   3.940 +  using inj_on_apfst[of f UNIV] by simp
   3.941  
   3.942  lemma inj_on_apsnd [simp]: "inj_on (apsnd f) (UNIV \<times> A) \<longleftrightarrow> inj_on f A"
   3.943 -by(auto simp add: inj_on_def)
   3.944 +  by (auto simp add: inj_on_def)
   3.945  
   3.946  lemma inj_apsnd [simp]: "inj (apsnd f) \<longleftrightarrow> inj f"
   3.947 -using inj_on_apsnd[of f UNIV] by simp
   3.948 +  using inj_on_apsnd[of f UNIV] by simp
   3.949  
   3.950  context
   3.951  begin
   3.952 @@ -1257,9 +1154,8 @@
   3.953  qualified definition product :: "'a set \<Rightarrow> 'b set \<Rightarrow> ('a \<times> 'b) set" where
   3.954    [code_abbrev]: "product A B = A \<times> B"
   3.955  
   3.956 -lemma member_product:
   3.957 -  "x \<in> Product_Type.product A B \<longleftrightarrow> x \<in> A \<times> B"
   3.958 -  by (simp add: Product_Type.product_def)
   3.959 +lemma member_product: "x \<in> Product_Type.product A B \<longleftrightarrow> x \<in> A \<times> B"
   3.960 +  by (simp add: product_def)
   3.961  
   3.962  end
   3.963    
   3.964 @@ -1269,59 +1165,80 @@
   3.965    assumes "inj_on f A" and "inj_on g B"
   3.966    shows "inj_on (map_prod f g) (A \<times> B)"
   3.967  proof (rule inj_onI)
   3.968 -  fix x :: "'a \<times> 'c" and y :: "'a \<times> 'c"
   3.969 -  assume "x \<in> A \<times> B" hence "fst x \<in> A" and "snd x \<in> B" by auto
   3.970 -  assume "y \<in> A \<times> B" hence "fst y \<in> A" and "snd y \<in> B" by auto
   3.971 +  fix x :: "'a \<times> 'c"
   3.972 +  fix y :: "'a \<times> 'c"
   3.973 +  assume "x \<in> A \<times> B"
   3.974 +  then have "fst x \<in> A" and "snd x \<in> B" by auto
   3.975 +  assume "y \<in> A \<times> B"
   3.976 +  then have "fst y \<in> A" and "snd y \<in> B" by auto
   3.977    assume "map_prod f g x = map_prod f g y"
   3.978 -  hence "fst (map_prod f g x) = fst (map_prod f g y)" by (auto)
   3.979 -  hence "f (fst x) = f (fst y)" by (cases x,cases y,auto)
   3.980 -  with \<open>inj_on f A\<close> and \<open>fst x \<in> A\<close> and \<open>fst y \<in> A\<close>
   3.981 -  have "fst x = fst y" by (auto dest:dest:inj_onD)
   3.982 +  then have "fst (map_prod f g x) = fst (map_prod f g y)" by auto
   3.983 +  then have "f (fst x) = f (fst y)" by (cases x, cases y) auto
   3.984 +  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"
   3.985 +    by (auto dest: inj_onD)
   3.986    moreover from \<open>map_prod f g x = map_prod f g y\<close>
   3.987 -  have "snd (map_prod f g x) = snd (map_prod f g y)" by (auto)
   3.988 -  hence "g (snd x) = g (snd y)" by (cases x,cases y,auto)
   3.989 -  with \<open>inj_on g B\<close> and \<open>snd x \<in> B\<close> and \<open>snd y \<in> B\<close>
   3.990 -  have "snd x = snd y" by (auto dest:dest:inj_onD)
   3.991 -  ultimately show "x = y" by(rule prod_eqI)
   3.992 +  have "snd (map_prod f g x) = snd (map_prod f g y)" by auto
   3.993 +  then have "g (snd x) = g (snd y)" by (cases x, cases y) auto
   3.994 +  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"
   3.995 +    by (auto dest: inj_onD)
   3.996 +  ultimately show "x = y" by (rule prod_eqI)
   3.997  qed
   3.998  
   3.999  lemma map_prod_surj:
  3.1000 -  fixes f :: "'a \<Rightarrow> 'b" and g :: "'c \<Rightarrow> 'd"
  3.1001 +  fixes f :: "'a \<Rightarrow> 'b"
  3.1002 +    and g :: "'c \<Rightarrow> 'd"
  3.1003    assumes "surj f" and "surj g"
  3.1004    shows "surj (map_prod f g)"
  3.1005 -unfolding surj_def
  3.1006 +  unfolding surj_def
  3.1007  proof
  3.1008    fix y :: "'b \<times> 'd"
  3.1009 -  from \<open>surj f\<close> obtain a where "fst y = f a" by (auto elim:surjE)
  3.1010 +  from \<open>surj f\<close> obtain a where "fst y = f a"
  3.1011 +    by (auto elim: surjE)
  3.1012    moreover
  3.1013 -  from \<open>surj g\<close> obtain b where "snd y = g b" by (auto elim:surjE)
  3.1014 -  ultimately have "(fst y, snd y) = map_prod f g (a,b)" by auto
  3.1015 -  thus "\<exists>x. y = map_prod f g x" by auto
  3.1016 +  from \<open>surj g\<close> obtain b where "snd y = g b"
  3.1017 +    by (auto elim: surjE)
  3.1018 +  ultimately have "(fst y, snd y) = map_prod f g (a,b)"
  3.1019 +    by auto
  3.1020 +  then show "\<exists>x. y = map_prod f g x"
  3.1021 +    by auto
  3.1022  qed
  3.1023  
  3.1024  lemma map_prod_surj_on:
  3.1025    assumes "f ` A = A'" and "g ` B = B'"
  3.1026    shows "map_prod f g ` (A \<times> B) = A' \<times> B'"
  3.1027 -unfolding image_def
  3.1028 -proof(rule set_eqI,rule iffI)
  3.1029 +  unfolding image_def
  3.1030 +proof (rule set_eqI, rule iffI)
  3.1031    fix x :: "'a \<times> 'c"
  3.1032    assume "x \<in> {y::'a \<times> 'c. \<exists>x::'b \<times> 'd\<in>A \<times> B. y = map_prod f g x}"
  3.1033 -  then obtain y where "y \<in> A \<times> B" and "x = map_prod f g y" by blast
  3.1034 -  from \<open>image f A = A'\<close> and \<open>y \<in> A \<times> B\<close> have "f (fst y) \<in> A'" by auto
  3.1035 -  moreover from \<open>image g B = B'\<close> and \<open>y \<in> A \<times> B\<close> have "g (snd y) \<in> B'" by auto
  3.1036 -  ultimately have "(f (fst y), g (snd y)) \<in> (A' \<times> B')" by auto
  3.1037 -  with \<open>x = map_prod f g y\<close> show "x \<in> A' \<times> B'" by (cases y, auto)
  3.1038 +  then obtain y where "y \<in> A \<times> B" and "x = map_prod f g y"
  3.1039 +    by blast
  3.1040 +  from \<open>image f A = A'\<close> and \<open>y \<in> A \<times> B\<close> have "f (fst y) \<in> A'"
  3.1041 +    by auto
  3.1042 +  moreover from \<open>image g B = B'\<close> and \<open>y \<in> A \<times> B\<close> have "g (snd y) \<in> B'"
  3.1043 +    by auto
  3.1044 +  ultimately have "(f (fst y), g (snd y)) \<in> (A' \<times> B')"
  3.1045 +    by auto
  3.1046 +  with \<open>x = map_prod f g y\<close> show "x \<in> A' \<times> B'"
  3.1047 +    by (cases y) auto
  3.1048  next
  3.1049    fix x :: "'a \<times> 'c"
  3.1050 -  assume "x \<in> A' \<times> B'" hence "fst x \<in> A'" and "snd x \<in> B'" by auto
  3.1051 -  from \<open>image f A = A'\<close> and \<open>fst x \<in> A'\<close> have "fst x \<in> image f A" by auto
  3.1052 -  then obtain a where "a \<in> A" and "fst x = f a" by (rule imageE)
  3.1053 -  moreover from \<open>image g B = B'\<close> and \<open>snd x \<in> B'\<close>
  3.1054 -  obtain b where "b \<in> B" and "snd x = g b" by auto
  3.1055 -  ultimately have "(fst x, snd x) = map_prod f g (a,b)" by auto
  3.1056 -  moreover from \<open>a \<in> A\<close> and  \<open>b \<in> B\<close> have "(a , b) \<in> A \<times> B" by auto
  3.1057 -  ultimately have "\<exists>y \<in> A \<times> B. x = map_prod f g y" by auto
  3.1058 -  thus "x \<in> {x. \<exists>y \<in> A \<times> B. x = map_prod f g y}" by auto
  3.1059 +  assume "x \<in> A' \<times> B'"
  3.1060 +  then have "fst x \<in> A'" and "snd x \<in> B'"
  3.1061 +    by auto
  3.1062 +  from \<open>image f A = A'\<close> and \<open>fst x \<in> A'\<close> have "fst x \<in> image f A"
  3.1063 +    by auto
  3.1064 +  then obtain a where "a \<in> A" and "fst x = f a"
  3.1065 +    by (rule imageE)
  3.1066 +  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"
  3.1067 +    by auto
  3.1068 +  ultimately have "(fst x, snd x) = map_prod f g (a, b)"
  3.1069 +    by auto
  3.1070 +  moreover from \<open>a \<in> A\<close> and  \<open>b \<in> B\<close> have "(a , b) \<in> A \<times> B"
  3.1071 +    by auto
  3.1072 +  ultimately have "\<exists>y \<in> A \<times> B. x = map_prod f g y"
  3.1073 +    by auto
  3.1074 +  then show "x \<in> {x. \<exists>y \<in> A \<times> B. x = map_prod f g y}"
  3.1075 +    by auto
  3.1076  qed
  3.1077  
  3.1078  
     4.1 --- a/src/HOL/Set.thy	Tue Jul 05 22:47:48 2016 +0200
     4.2 +++ b/src/HOL/Set.thy	Tue Jul 05 23:39:49 2016 +0200
     4.3 @@ -466,7 +466,7 @@
     4.4    \<comment> \<open>Classical elimination rule.\<close>
     4.5    by (auto simp add: less_eq_set_def le_fun_def)
     4.6  
     4.7 -lemma subset_eq: "A \<subseteq> B = (\<forall>x\<in>A. x \<in> B)"
     4.8 +lemma subset_eq: "A \<subseteq> B \<longleftrightarrow> (\<forall>x\<in>A. x \<in> B)"
     4.9    by blast
    4.10  
    4.11  lemma contra_subsetD: "A \<subseteq> B \<Longrightarrow> c \<notin> B \<Longrightarrow> c \<notin> A"
     5.1 --- a/src/HOL/Sum_Type.thy	Tue Jul 05 22:47:48 2016 +0200
     5.2 +++ b/src/HOL/Sum_Type.thy	Tue Jul 05 23:39:49 2016 +0200
     5.3 @@ -11,15 +11,15 @@
     5.4  
     5.5  subsection \<open>Construction of the sum type and its basic abstract operations\<close>
     5.6  
     5.7 -definition Inl_Rep :: "'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> bool \<Rightarrow> bool" where
     5.8 -  "Inl_Rep a x y p \<longleftrightarrow> x = a \<and> p"
     5.9 +definition Inl_Rep :: "'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> bool \<Rightarrow> bool"
    5.10 +  where "Inl_Rep a x y p \<longleftrightarrow> x = a \<and> p"
    5.11  
    5.12 -definition Inr_Rep :: "'b \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> bool \<Rightarrow> bool" where
    5.13 -  "Inr_Rep b x y p \<longleftrightarrow> y = b \<and> \<not> p"
    5.14 +definition Inr_Rep :: "'b \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> bool \<Rightarrow> bool"
    5.15 +  where "Inr_Rep b x y p \<longleftrightarrow> y = b \<and> \<not> p"
    5.16  
    5.17  definition "sum = {f. (\<exists>a. f = Inl_Rep (a::'a)) \<or> (\<exists>b. f = Inr_Rep (b::'b))}"
    5.18  
    5.19 -typedef ('a, 'b) sum (infixr "+" 10) = "sum :: ('a => 'b => bool => bool) set"
    5.20 +typedef ('a, 'b) sum (infixr "+" 10) = "sum :: ('a \<Rightarrow> 'b \<Rightarrow> bool \<Rightarrow> bool) set"
    5.21    unfolding sum_def by auto
    5.22  
    5.23  lemma Inl_RepI: "Inl_Rep a \<in> sum"
    5.24 @@ -46,48 +46,51 @@
    5.25  lemma Inl_Rep_not_Inr_Rep: "Inl_Rep a \<noteq> Inr_Rep b"
    5.26    by (auto simp add: Inl_Rep_def Inr_Rep_def fun_eq_iff)
    5.27  
    5.28 -definition Inl :: "'a \<Rightarrow> 'a + 'b" where
    5.29 -  "Inl = Abs_sum \<circ> Inl_Rep"
    5.30 +definition Inl :: "'a \<Rightarrow> 'a + 'b"
    5.31 +  where "Inl = Abs_sum \<circ> Inl_Rep"
    5.32  
    5.33 -definition Inr :: "'b \<Rightarrow> 'a + 'b" where
    5.34 -  "Inr = Abs_sum \<circ> Inr_Rep"
    5.35 +definition Inr :: "'b \<Rightarrow> 'a + 'b"
    5.36 +  where "Inr = Abs_sum \<circ> Inr_Rep"
    5.37  
    5.38  lemma inj_Inl [simp]: "inj_on Inl A"
    5.39 -by (auto simp add: Inl_def intro!: comp_inj_on Inl_Rep_inject inj_on_Abs_sum Inl_RepI)
    5.40 +  by (auto simp add: Inl_def intro!: comp_inj_on Inl_Rep_inject inj_on_Abs_sum Inl_RepI)
    5.41  
    5.42  lemma Inl_inject: "Inl x = Inl y \<Longrightarrow> x = y"
    5.43 -using inj_Inl by (rule injD)
    5.44 +  using inj_Inl by (rule injD)
    5.45  
    5.46  lemma inj_Inr [simp]: "inj_on Inr A"
    5.47 -by (auto simp add: Inr_def intro!: comp_inj_on Inr_Rep_inject inj_on_Abs_sum Inr_RepI)
    5.48 +  by (auto simp add: Inr_def intro!: comp_inj_on Inr_Rep_inject inj_on_Abs_sum Inr_RepI)
    5.49  
    5.50  lemma Inr_inject: "Inr x = Inr y \<Longrightarrow> x = y"
    5.51 -using inj_Inr by (rule injD)
    5.52 +  using inj_Inr by (rule injD)
    5.53  
    5.54  lemma Inl_not_Inr: "Inl a \<noteq> Inr b"
    5.55  proof -
    5.56 -  from Inl_RepI [of a] Inr_RepI [of b] have "{Inl_Rep a, Inr_Rep b} \<subseteq> sum" by auto
    5.57 +  have "{Inl_Rep a, Inr_Rep b} \<subseteq> sum"
    5.58 +    using Inl_RepI [of a] Inr_RepI [of b] by auto
    5.59    with inj_on_Abs_sum have "inj_on Abs_sum {Inl_Rep a, Inr_Rep b}" .
    5.60 -  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
    5.61 -  then show ?thesis by (simp add: Inl_def Inr_def)
    5.62 +  with Inl_Rep_not_Inr_Rep [of a b] inj_on_contraD have "Abs_sum (Inl_Rep a) \<noteq> Abs_sum (Inr_Rep b)"
    5.63 +    by auto
    5.64 +  then show ?thesis
    5.65 +    by (simp add: Inl_def Inr_def)
    5.66  qed
    5.67  
    5.68 -lemma Inr_not_Inl: "Inr b \<noteq> Inl a" 
    5.69 +lemma Inr_not_Inl: "Inr b \<noteq> Inl a"
    5.70    using Inl_not_Inr by (rule not_sym)
    5.71  
    5.72 -lemma sumE: 
    5.73 +lemma sumE:
    5.74    assumes "\<And>x::'a. s = Inl x \<Longrightarrow> P"
    5.75      and "\<And>y::'b. s = Inr y \<Longrightarrow> P"
    5.76    shows P
    5.77  proof (rule Abs_sum_cases [of s])
    5.78 -  fix f 
    5.79 +  fix f
    5.80    assume "s = Abs_sum f" and "f \<in> sum"
    5.81    with assms show P by (auto simp add: sum_def Inl_def Inr_def)
    5.82  qed
    5.83  
    5.84  free_constructors case_sum for
    5.85 -    isl: Inl projl
    5.86 -  | Inr projr
    5.87 +  isl: Inl projl
    5.88 +| Inr projr
    5.89    by (erule sumE, assumption) (auto dest: Inl_inject Inr_inject simp add: Inl_not_Inr)
    5.90  
    5.91  text \<open>Avoid name clashes by prefixing the output of \<open>old_rep_datatype\<close> with \<open>old\<close>.\<close>
    5.92 @@ -119,24 +122,21 @@
    5.93  
    5.94  setup \<open>Sign.parent_path\<close>
    5.95  
    5.96 -primrec map_sum :: "('a \<Rightarrow> 'c) \<Rightarrow> ('b \<Rightarrow> 'd) \<Rightarrow> 'a + 'b \<Rightarrow> 'c + 'd" where
    5.97 +primrec map_sum :: "('a \<Rightarrow> 'c) \<Rightarrow> ('b \<Rightarrow> 'd) \<Rightarrow> 'a + 'b \<Rightarrow> 'c + 'd"
    5.98 +where
    5.99    "map_sum f1 f2 (Inl a) = Inl (f1 a)"
   5.100  | "map_sum f1 f2 (Inr a) = Inr (f2 a)"
   5.101  
   5.102 -functor map_sum: map_sum proof -
   5.103 -  fix f g h i
   5.104 -  show "map_sum f g \<circ> map_sum h i = map_sum (f \<circ> h) (g \<circ> i)"
   5.105 +functor map_sum: map_sum
   5.106 +proof -
   5.107 +  show "map_sum f g \<circ> map_sum h i = map_sum (f \<circ> h) (g \<circ> i)" for f g h i
   5.108    proof
   5.109 -    fix s
   5.110 -    show "(map_sum f g \<circ> map_sum h i) s = map_sum (f \<circ> h) (g \<circ> i) s"
   5.111 +    show "(map_sum f g \<circ> map_sum h i) s = map_sum (f \<circ> h) (g \<circ> i) s" for s
   5.112        by (cases s) simp_all
   5.113    qed
   5.114 -next
   5.115 -  fix s
   5.116    show "map_sum id id = id"
   5.117    proof
   5.118 -    fix s
   5.119 -    show "map_sum id id s = id s" 
   5.120 +    show "map_sum id id s = id s" for s
   5.121        by (cases s) simp_all
   5.122    qed
   5.123  qed
   5.124 @@ -145,7 +145,8 @@
   5.125    by (auto intro: sum.induct)
   5.126  
   5.127  lemma split_sum_ex: "(\<exists>x. P x) \<longleftrightarrow> (\<exists>x. P (Inl x)) \<or> (\<exists>x. P (Inr x))"
   5.128 -using split_sum_all[of "\<lambda>x. \<not>P x"] by blast
   5.129 +  using split_sum_all[of "\<lambda>x. \<not>P x"] by blast
   5.130 +
   5.131  
   5.132  subsection \<open>Projections\<close>
   5.133  
   5.134 @@ -161,29 +162,32 @@
   5.135  
   5.136  lemma case_sum_inject:
   5.137    assumes a: "case_sum f1 f2 = case_sum g1 g2"
   5.138 -  assumes r: "f1 = g1 \<Longrightarrow> f2 = g2 \<Longrightarrow> P"
   5.139 +    and r: "f1 = g1 \<Longrightarrow> f2 = g2 \<Longrightarrow> P"
   5.140    shows P
   5.141  proof (rule r)
   5.142 -  show "f1 = g1" proof
   5.143 +  show "f1 = g1"
   5.144 +  proof
   5.145      fix x :: 'a
   5.146      from a have "case_sum f1 f2 (Inl x) = case_sum g1 g2 (Inl x)" by simp
   5.147      then show "f1 x = g1 x" by simp
   5.148    qed
   5.149 -  show "f2 = g2" proof
   5.150 +  show "f2 = g2"
   5.151 +  proof
   5.152      fix y :: 'b
   5.153      from a have "case_sum f1 f2 (Inr y) = case_sum g1 g2 (Inr y)" by simp
   5.154      then show "f2 y = g2 y" by simp
   5.155    qed
   5.156  qed
   5.157  
   5.158 -primrec Suml :: "('a \<Rightarrow> 'c) \<Rightarrow> 'a + 'b \<Rightarrow> 'c" where
   5.159 -  "Suml f (Inl x) = f x"
   5.160 +primrec Suml :: "('a \<Rightarrow> 'c) \<Rightarrow> 'a + 'b \<Rightarrow> 'c"
   5.161 +  where "Suml f (Inl x) = f x"
   5.162  
   5.163 -primrec Sumr :: "('b \<Rightarrow> 'c) \<Rightarrow> 'a + 'b \<Rightarrow> 'c" where
   5.164 -  "Sumr f (Inr x) = f x"
   5.165 +primrec Sumr :: "('b \<Rightarrow> 'c) \<Rightarrow> 'a + 'b \<Rightarrow> 'c"
   5.166 +  where "Sumr f (Inr x) = f x"
   5.167  
   5.168  lemma Suml_inject:
   5.169 -  assumes "Suml f = Suml g" shows "f = g"
   5.170 +  assumes "Suml f = Suml g"
   5.171 +  shows "f = g"
   5.172  proof
   5.173    fix x :: 'a
   5.174    let ?s = "Inl x :: 'a + 'b"
   5.175 @@ -192,7 +196,8 @@
   5.176  qed
   5.177  
   5.178  lemma Sumr_inject:
   5.179 -  assumes "Sumr f = Sumr g" shows "f = g"
   5.180 +  assumes "Sumr f = Sumr g"
   5.181 +  shows "f = g"
   5.182  proof
   5.183    fix x :: 'b
   5.184    let ?s = "Inr x :: 'a + 'b"
   5.185 @@ -203,25 +208,25 @@
   5.186  
   5.187  subsection \<open>The Disjoint Sum of Sets\<close>
   5.188  
   5.189 -definition Plus :: "'a set \<Rightarrow> 'b set \<Rightarrow> ('a + 'b) set" (infixr "<+>" 65) where
   5.190 -  "A <+> B = Inl ` A \<union> Inr ` B"
   5.191 +definition Plus :: "'a set \<Rightarrow> 'b set \<Rightarrow> ('a + 'b) set"  (infixr "<+>" 65)
   5.192 +  where "A <+> B = Inl ` A \<union> Inr ` B"
   5.193  
   5.194 -hide_const (open) Plus \<comment>"Valuable identifier"
   5.195 +hide_const (open) Plus \<comment> "Valuable identifier"
   5.196  
   5.197  lemma InlI [intro!]: "a \<in> A \<Longrightarrow> Inl a \<in> A <+> B"
   5.198 -by (simp add: Plus_def)
   5.199 +  by (simp add: Plus_def)
   5.200  
   5.201  lemma InrI [intro!]: "b \<in> B \<Longrightarrow> Inr b \<in> A <+> B"
   5.202 -by (simp add: Plus_def)
   5.203 +  by (simp add: Plus_def)
   5.204  
   5.205  text \<open>Exhaustion rule for sums, a degenerate form of induction\<close>
   5.206  
   5.207 -lemma PlusE [elim!]: 
   5.208 +lemma PlusE [elim!]:
   5.209    "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"
   5.210 -by (auto simp add: Plus_def)
   5.211 +  by (auto simp add: Plus_def)
   5.212  
   5.213  lemma Plus_eq_empty_conv [simp]: "A <+> B = {} \<longleftrightarrow> A = {} \<and> B = {}"
   5.214 -by auto
   5.215 +  by auto
   5.216  
   5.217  lemma UNIV_Plus_UNIV [simp]: "UNIV <+> UNIV = UNIV"
   5.218  proof (rule set_eqI)
   5.219 @@ -229,14 +234,11 @@
   5.220    show "u \<in> UNIV <+> UNIV \<longleftrightarrow> u \<in> UNIV" by (cases u) auto
   5.221  qed
   5.222  
   5.223 -lemma UNIV_sum:
   5.224 -  "UNIV = Inl ` UNIV \<union> Inr ` UNIV"
   5.225 +lemma UNIV_sum: "UNIV = Inl ` UNIV \<union> Inr ` UNIV"
   5.226  proof -
   5.227 -  { fix x :: "'a + 'b"
   5.228 -    assume "x \<notin> range Inr"
   5.229 -    then have "x \<in> range Inl"
   5.230 -    by (cases x) simp_all
   5.231 -  } then show ?thesis by auto
   5.232 +  have "x \<in> range Inl" if "x \<notin> range Inr" for x :: "'a + 'b"
   5.233 +    using that by (cases x) simp_all
   5.234 +  then show ?thesis by auto
   5.235  qed
   5.236  
   5.237  hide_const (open) Suml Sumr sum