removed legacy input syntax
authorhaftmann
Sun Nov 18 18:07:51 2018 +0000 (3 weeks ago)
changeset 69313b021008c5397
parent 69312 e0f68a507683
child 69314 b367c22c3dd8
child 69316 248696d0a05f
removed legacy input syntax
src/Doc/Main/Main_Doc.thy
src/HOL/Algebra/FiniteProduct.thy
src/HOL/Analysis/Abstract_Topology.thy
src/HOL/Analysis/Arcwise_Connected.thy
src/HOL/Analysis/Binary_Product_Measure.thy
src/HOL/Analysis/Brouwer_Fixpoint.thy
src/HOL/Analysis/Caratheodory.thy
src/HOL/Analysis/Change_Of_Vars.thy
src/HOL/Analysis/Complete_Measure.thy
src/HOL/Analysis/Embed_Measure.thy
src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy
src/HOL/Analysis/Extended_Real_Limits.thy
src/HOL/Analysis/Finite_Product_Measure.thy
src/HOL/Analysis/Henstock_Kurzweil_Integration.thy
src/HOL/Analysis/Homeomorphism.thy
src/HOL/Analysis/Improper_Integral.thy
src/HOL/Analysis/Measure_Space.thy
src/HOL/Analysis/Nonnegative_Lebesgue_Integration.thy
src/HOL/Analysis/Path_Connected.thy
src/HOL/Analysis/Polytope.thy
src/HOL/Analysis/Set_Integral.thy
src/HOL/Analysis/Sigma_Algebra.thy
src/HOL/Analysis/Starlike.thy
src/HOL/Analysis/Topology_Euclidean_Space.thy
src/HOL/Analysis/Uniform_Limit.thy
src/HOL/Analysis/Vitali_Covering_Theorem.thy
src/HOL/Bali/Basis.thy
src/HOL/Computational_Algebra/Primes.thy
src/HOL/Decision_Procs/MIR.thy
src/HOL/Hoare_Parallel/RG_Hoare.thy
src/HOL/Library/Countable_Complete_Lattices.thy
src/HOL/Library/Countable_Set_Type.thy
src/HOL/Library/Disjoint_Sets.thy
src/HOL/Library/Extended_Nonnegative_Real.thy
src/HOL/Library/Extended_Real.thy
src/HOL/Library/Finite_Map.thy
src/HOL/Library/Indicator_Function.thy
src/HOL/Library/Liminf_Limsup.thy
src/HOL/Library/Option_ord.thy
src/HOL/Library/Order_Continuity.thy
src/HOL/Library/Product_Order.thy
src/HOL/Library/Set_Algebras.thy
src/HOL/Library/Set_Idioms.thy
src/HOL/Library/Stream.thy
src/HOL/Probability/Fin_Map.thy
src/HOL/Probability/Independent_Family.thy
src/HOL/Probability/Probability_Mass_Function.thy
src/HOL/Probability/Projective_Family.thy
src/HOL/Probability/Stopping_Time.thy
src/HOL/Probability/Tree_Space.thy
src/HOL/Probability/ex/Measure_Not_CCC.thy
src/HOL/UNITY/Comp/Alloc.thy
src/HOL/UNITY/Comp/AllocBase.thy
src/HOL/UNITY/Comp/AllocImpl.thy
src/HOL/UNITY/Constrains.thy
src/HOL/UNITY/Extend.thy
src/HOL/UNITY/Guar.thy
src/HOL/UNITY/Lift_prog.thy
src/HOL/UNITY/Simple/Reachability.thy
src/HOL/UNITY/Union.thy
     1.1 --- a/src/Doc/Main/Main_Doc.thy	Sun Nov 18 09:51:41 2018 +0100
     1.2 +++ b/src/Doc/Main/Main_Doc.thy	Sun Nov 18 18:07:51 2018 +0000
     1.3 @@ -112,8 +112,6 @@
     1.4  @{const Set.member} & @{term_type_only Set.member "'a\<Rightarrow>'a set\<Rightarrow>bool"} & (\<^verbatim>\<open>:\<close>)\\
     1.5  @{const Set.union} & @{term_type_only Set.union "'a set\<Rightarrow>'a set \<Rightarrow> 'a set"} & (\<^verbatim>\<open>Un\<close>)\\
     1.6  @{const Set.inter} & @{term_type_only Set.inter "'a set\<Rightarrow>'a set \<Rightarrow> 'a set"} & (\<^verbatim>\<open>Int\<close>)\\
     1.7 -@{const UNION} & @{term_type_only UNION "'a set\<Rightarrow>('a \<Rightarrow> 'b set) \<Rightarrow> 'b set"}\\
     1.8 -@{const INTER} & @{term_type_only INTER "'a set\<Rightarrow>('a \<Rightarrow> 'b set) \<Rightarrow> 'b set"}\\
     1.9  @{const Union} & @{term_type_only Union "'a set set\<Rightarrow>'a set"}\\
    1.10  @{const Inter} & @{term_type_only Inter "'a set set\<Rightarrow>'a set"}\\
    1.11  @{const Pow} & @{term_type_only Pow "'a set \<Rightarrow>'a set set"}\\
    1.12 @@ -134,10 +132,10 @@
    1.13  @{term[source]"A \<supset> B"} & @{term[source]"B < A"}\\
    1.14  @{term "{x. P}"} & @{term[source]"Collect (\<lambda>x. P)"}\\
    1.15  \<open>{t | x\<^sub>1 \<dots> x\<^sub>n. P}\<close> & \<open>{v. \<exists>x\<^sub>1 \<dots> x\<^sub>n. v = t \<and> P}\<close>\\
    1.16 -@{term[source]"\<Union>x\<in>I. A"} & @{term[source]"UNION I (\<lambda>x. A)"} & (\texttt{UN})\\
    1.17 -@{term[source]"\<Union>x. A"} & @{term[source]"UNION UNIV (\<lambda>x. A)"}\\
    1.18 -@{term[source]"\<Inter>x\<in>I. A"} & @{term[source]"INTER I (\<lambda>x. A)"} & (\texttt{INT})\\
    1.19 -@{term[source]"\<Inter>x. A"} & @{term[source]"INTER UNIV (\<lambda>x. A)"}\\
    1.20 +@{term[source]"\<Union>x\<in>I. A"} & @{term[source]"\<Union>((\<lambda>x. A) ` I)"} & (\texttt{UN})\\
    1.21 +@{term[source]"\<Union>x. A"} & @{term[source]"\<Union>((\<lambda>x. A) ` UNIV)"}\\
    1.22 +@{term[source]"\<Inter>x\<in>I. A"} & @{term[source]"\<Inter>((\<lambda>x. A) ` I)"} & (\texttt{INT})\\
    1.23 +@{term[source]"\<Inter>x. A"} & @{term[source]"\<Inter>((\<lambda>x. A) ` UNIV)"}\\
    1.24  @{term "\<forall>x\<in>A. P"} & @{term[source]"Ball A (\<lambda>x. P)"}\\
    1.25  @{term "\<exists>x\<in>A. P"} & @{term[source]"Bex A (\<lambda>x. P)"}\\
    1.26  @{term "range f"} & @{term[source]"f ` UNIV"}\\
     2.1 --- a/src/HOL/Algebra/FiniteProduct.thy	Sun Nov 18 09:51:41 2018 +0100
     2.2 +++ b/src/HOL/Algebra/FiniteProduct.thy	Sun Nov 18 18:07:51 2018 +0000
     2.3 @@ -576,7 +576,7 @@
     2.4    assumes
     2.5      "finite I" "\<And>i. i \<in> I \<Longrightarrow> finite (A i)" "pairwise (\<lambda>i j. disjnt (A i) (A j)) I"
     2.6      "\<And>i x. i \<in> I \<Longrightarrow> x \<in> A i \<Longrightarrow> g x \<in> carrier G"
     2.7 -shows "finprod G g (UNION I A) = finprod G (\<lambda>i. finprod G g (A i)) I"
     2.8 +shows "finprod G g (\<Union>(A ` I)) = finprod G (\<lambda>i. finprod G g (A i)) I"
     2.9    using assms
    2.10  proof (induction set: finite)
    2.11    case empty
     3.1 --- a/src/HOL/Analysis/Abstract_Topology.thy	Sun Nov 18 09:51:41 2018 +0100
     3.2 +++ b/src/HOL/Analysis/Abstract_Topology.thy	Sun Nov 18 18:07:51 2018 +0000
     3.3 @@ -2664,11 +2664,11 @@
     3.4            (\<forall>\<U>. \<U> \<subseteq> (\<lambda>T. S \<inter> T) ` {T. closedin X T} \<longrightarrow>
     3.5             (\<forall>\<F>. finite \<F> \<longrightarrow> \<F> \<subseteq> \<U> \<longrightarrow> \<Inter>\<F> \<noteq> {}) \<longrightarrow> \<Inter>\<U> \<noteq> {})"
     3.6        by (simp add: compact_space_fip compactin_subspace closedin_subtopology image_def subset_eq Int_commute imp_conjL)
     3.7 -    also have "\<dots> = (\<forall>\<U>\<subseteq>Collect (closedin X). (\<forall>\<F>. finite \<F> \<longrightarrow> \<F> \<subseteq> (\<inter>) S ` \<U> \<longrightarrow> \<Inter>\<F> \<noteq> {}) \<longrightarrow> INTER \<U> ((\<inter>) S) \<noteq> {})"
     3.8 +    also have "\<dots> = (\<forall>\<U>\<subseteq>Collect (closedin X). (\<forall>\<F>. finite \<F> \<longrightarrow> \<F> \<subseteq> (\<inter>) S ` \<U> \<longrightarrow> \<Inter>\<F> \<noteq> {}) \<longrightarrow> \<Inter> ((\<inter>) S ` \<U>) \<noteq> {})"
     3.9        by (simp add: all_subset_image)
    3.10      also have "\<dots> = (\<forall>\<U>. (\<forall>C\<in>\<U>. closedin X C) \<and> (\<forall>\<F>. finite \<F> \<and> \<F> \<subseteq> \<U> \<longrightarrow> S \<inter> \<Inter>\<F> \<noteq> {}) \<longrightarrow> S \<inter> \<Inter>\<U> \<noteq> {})"
    3.11      proof -
    3.12 -      have eq: "((\<forall>\<F>. finite \<F> \<and> \<F> \<subseteq> \<U> \<longrightarrow> INTER \<F> ((\<inter>) S) \<noteq> {}) \<longrightarrow> INTER \<U> ((\<inter>) S) \<noteq> {}) =
    3.13 +      have eq: "((\<forall>\<F>. finite \<F> \<and> \<F> \<subseteq> \<U> \<longrightarrow> \<Inter> ((\<inter>) S ` \<F>) \<noteq> {}) \<longrightarrow> \<Inter> ((\<inter>) S ` \<U>) \<noteq> {}) \<longleftrightarrow>
    3.14                  ((\<forall>\<F>. finite \<F> \<and> \<F> \<subseteq> \<U> \<longrightarrow> S \<inter> \<Inter>\<F> \<noteq> {}) \<longrightarrow> S \<inter> \<Inter>\<U> \<noteq> {})"  for \<U>
    3.15          by simp (use \<open>S \<noteq> {}\<close> in blast)
    3.16        show ?thesis
     4.1 --- a/src/HOL/Analysis/Arcwise_Connected.thy	Sun Nov 18 09:51:41 2018 +0100
     4.2 +++ b/src/HOL/Analysis/Arcwise_Connected.thy	Sun Nov 18 18:07:51 2018 +0000
     4.3 @@ -39,22 +39,22 @@
     4.4    proof
     4.5      show "\<Inter>range A \<subseteq> S"
     4.6        using \<open>\<And>n. A n \<subseteq> S\<close> by blast
     4.7 -    show "closed (INTER UNIV A)"
     4.8 +    show "closed (\<Inter>(A ` UNIV))"
     4.9        using clo by blast
    4.10 -    show "\<phi> (INTER UNIV A)"
    4.11 +    show "\<phi> (\<Inter>(A ` UNIV))"
    4.12        by (simp add: clo \<phi> sub)
    4.13 -    show "\<not> U \<subset> INTER UNIV A" if "U \<subseteq> S" "closed U" "\<phi> U" for U
    4.14 +    show "\<not> U \<subset> \<Inter>(A ` UNIV)" if "U \<subseteq> S" "closed U" "\<phi> U" for U
    4.15      proof -
    4.16        have "\<exists>y. x \<notin> A y" if "x \<notin> U" and Usub: "U \<subseteq> (\<Inter>x. A x)" for x
    4.17        proof -
    4.18          obtain e where "e > 0" and e: "ball x e \<subseteq> -U"
    4.19            using \<open>closed U\<close> \<open>x \<notin> U\<close> openE [of "-U"] by blast
    4.20 -        moreover obtain K where K: "ball x e = UNION K B"
    4.21 +        moreover obtain K where K: "ball x e = \<Union>(B ` K)"
    4.22            using open_cov [of "ball x e"] by auto
    4.23 -        ultimately have "UNION K B \<subseteq> -U"
    4.24 +        ultimately have "\<Union>(B ` K) \<subseteq> -U"
    4.25            by blast
    4.26          have "K \<noteq> {}"
    4.27 -          using \<open>0 < e\<close> \<open>ball x e = UNION K B\<close> by auto
    4.28 +          using \<open>0 < e\<close> \<open>ball x e = \<Union>(B ` K)\<close> by auto
    4.29          then obtain n where "n \<in> K" "x \<in> B n"
    4.30            by (metis K UN_E \<open>0 < e\<close> centre_in_ball)
    4.31          then have "U \<inter> B n = {}"
    4.32 @@ -89,16 +89,16 @@
    4.33    fix F
    4.34    assume cloF: "\<And>n. closed (F n)"
    4.35       and F: "\<And>n. F n \<noteq> {} \<and> F n \<subseteq> S \<and> \<phi> (F n)" and Fsub: "\<And>n. F (Suc n) \<subseteq> F n"
    4.36 -  show "INTER UNIV F \<noteq> {} \<and> INTER UNIV F \<subseteq> S \<and> \<phi> (INTER UNIV F)"
    4.37 +  show "\<Inter>(F ` UNIV) \<noteq> {} \<and> \<Inter>(F ` UNIV) \<subseteq> S \<and> \<phi> (\<Inter>(F ` UNIV))"
    4.38    proof (intro conjI)
    4.39 -    show "INTER UNIV F \<noteq> {}"
    4.40 +    show "\<Inter>(F ` UNIV) \<noteq> {}"
    4.41        apply (rule compact_nest)
    4.42        apply (meson F cloF \<open>compact S\<close> seq_compact_closed_subset seq_compact_eq_compact)
    4.43         apply (simp add: F)
    4.44        by (meson Fsub lift_Suc_antimono_le)
    4.45 -    show " INTER UNIV F \<subseteq> S"
    4.46 +    show " \<Inter>(F ` UNIV) \<subseteq> S"
    4.47        using F by blast
    4.48 -    show "\<phi> (INTER UNIV F)"
    4.49 +    show "\<phi> (\<Inter>(F ` UNIV))"
    4.50        by (metis F Fsub \<phi> \<open>compact S\<close> cloF closed_Int_compact inf.orderE)
    4.51    qed
    4.52  next
    4.53 @@ -1680,7 +1680,7 @@
    4.54        using that by auto
    4.55      show "\<phi> {0..1}"
    4.56        by (auto simp: \<phi>_def open_segment_eq_real_ivl *)
    4.57 -    show "\<phi> (INTER UNIV F)"
    4.58 +    show "\<phi> (\<Inter>(F ` UNIV))"
    4.59        if "\<And>n. closed (F n)" and \<phi>: "\<And>n. \<phi> (F n)" and Fsub: "\<And>n. F (Suc n) \<subseteq> F n" for F
    4.60      proof -
    4.61        have F01: "\<And>n. F n \<subseteq> {0..1} \<and> 0 \<in> F n \<and> 1 \<in> F n"
    4.62 @@ -1706,13 +1706,13 @@
    4.63            using minxy \<open>0 < e\<close> less by simp_all
    4.64          have Fclo: "\<And>T. T \<in> range F \<Longrightarrow> closed T"
    4.65            by (metis \<open>\<And>n. closed (F n)\<close> image_iff)
    4.66 -        have eq: "{w..z} \<inter> INTER UNIV F = {}"
    4.67 +        have eq: "{w..z} \<inter> \<Inter>(F ` UNIV) = {}"
    4.68            using less w z apply (auto simp: open_segment_eq_real_ivl)
    4.69            by (metis (no_types, hide_lams) INT_I IntI empty_iff greaterThanLessThan_iff not_le order.trans)
    4.70          then obtain K where "finite K" and K: "{w..z} \<inter> (\<Inter> (F ` K)) = {}"
    4.71            by (metis finite_subset_image compact_imp_fip [OF compact_interval Fclo])
    4.72          then have "K \<noteq> {}"
    4.73 -          using \<open>w < z\<close> \<open>{w..z} \<inter> INTER K F = {}\<close> by auto
    4.74 +          using \<open>w < z\<close> \<open>{w..z} \<inter> \<Inter>(F ` K) = {}\<close> by auto
    4.75          define n where "n \<equiv> Max K"
    4.76          have "n \<in> K" unfolding n_def by (metis \<open>K \<noteq> {}\<close> \<open>finite K\<close> Max_in)
    4.77          have "F n \<subseteq> \<Inter> (F ` K)"
     5.1 --- a/src/HOL/Analysis/Binary_Product_Measure.thy	Sun Nov 18 09:51:41 2018 +0100
     5.2 +++ b/src/HOL/Analysis/Binary_Product_Measure.thy	Sun Nov 18 18:07:51 2018 +0000
     5.3 @@ -1118,7 +1118,7 @@
     5.4          unfolding * by auto
     5.5      next
     5.6        case (Union A)
     5.7 -      moreover have *: "(UNION UNIV A) \<times> UNIV = UNION UNIV (\<lambda>i. A i \<times> UNIV)"
     5.8 +      moreover have *: "(\<Union>(A ` UNIV)) \<times> UNIV = \<Union>((\<lambda>i. A i \<times> UNIV) ` UNIV)"
     5.9          by auto
    5.10        ultimately show ?case
    5.11          unfolding * by auto
    5.12 @@ -1137,7 +1137,7 @@
    5.13          unfolding * by auto
    5.14      next
    5.15        case (Union B)
    5.16 -      moreover have *: "UNIV \<times> (UNION UNIV B) = UNION UNIV (\<lambda>i. UNIV \<times> B i)"
    5.17 +      moreover have *: "UNIV \<times> (\<Union>(B ` UNIV)) = \<Union>((\<lambda>i. UNIV \<times> B i) ` UNIV)"
    5.18          by auto
    5.19        ultimately show ?case
    5.20          unfolding * by auto
     6.1 --- a/src/HOL/Analysis/Brouwer_Fixpoint.thy	Sun Nov 18 09:51:41 2018 +0100
     6.2 +++ b/src/HOL/Analysis/Brouwer_Fixpoint.thy	Sun Nov 18 18:07:51 2018 +0000
     6.3 @@ -4779,11 +4779,11 @@
     6.4      by metis
     6.5    show ?thesis
     6.6    proof
     6.7 -    show "openin (subtopology euclidean T') (UNION T F)"
     6.8 +    show "openin (subtopology euclidean T') (\<Union>(F ` T))"
     6.9        using F by blast
    6.10 -    show "T \<subseteq> UNION T F"
    6.11 +    show "T \<subseteq> \<Union>(F ` T)"
    6.12        using F by blast
    6.13 -    show "S \<times> UNION T F \<subseteq> U"
    6.14 +    show "S \<times> \<Union>(F ` T) \<subseteq> U"
    6.15        using F by auto
    6.16    qed
    6.17  qed
    6.18 @@ -4882,23 +4882,23 @@
    6.19        by (simp add: homotopic_with) metis
    6.20      have wop: "b \<in> V x \<Longrightarrow> \<exists>k. b \<in> V k \<and> (\<forall>j<k. b \<notin> V j)" for b x
    6.21          using nat_less_induct [where P = "\<lambda>i. b \<notin> V i"] by meson
    6.22 -    obtain \<zeta> where cont: "continuous_on ({0..1} \<times> UNION UNIV V) \<zeta>"
    6.23 -              and eq: "\<And>x i. \<lbrakk>x \<in> {0..1} \<times> UNION UNIV V \<inter>
    6.24 +    obtain \<zeta> where cont: "continuous_on ({0..1} \<times> \<Union>(V ` UNIV)) \<zeta>"
    6.25 +              and eq: "\<And>x i. \<lbrakk>x \<in> {0..1} \<times> \<Union>(V ` UNIV) \<inter>
    6.26                                     {0..1} \<times> (V i - (\<Union>m<i. V m))\<rbrakk> \<Longrightarrow> \<zeta> x = h i x"
    6.27      proof (rule pasting_lemma_exists)
    6.28 -      show "{0..1} \<times> UNION UNIV V \<subseteq> (\<Union>i. {0..1::real} \<times> (V i - (\<Union>m<i. V m)))"
    6.29 +      show "{0..1} \<times> \<Union>(V ` UNIV) \<subseteq> (\<Union>i. {0..1::real} \<times> (V i - (\<Union>m<i. V m)))"
    6.30          by (force simp: Ball_def dest: wop)
    6.31 -      show "openin (subtopology euclidean ({0..1} \<times> UNION UNIV V)) 
    6.32 +      show "openin (subtopology euclidean ({0..1} \<times> \<Union>(V ` UNIV))) 
    6.33                     ({0..1::real} \<times> (V i - (\<Union>m<i. V m)))" for i
    6.34        proof (intro openin_Times openin_subtopology_self openin_diff)
    6.35 -        show "openin (subtopology euclidean (UNION UNIV V)) (V i)"
    6.36 +        show "openin (subtopology euclidean (\<Union>(V ` UNIV))) (V i)"
    6.37            using ope V eqU by auto
    6.38 -        show "closedin (subtopology euclidean (UNION UNIV V)) (\<Union>m<i. V m)"
    6.39 +        show "closedin (subtopology euclidean (\<Union>(V ` UNIV))) (\<Union>m<i. V m)"
    6.40            using V clo eqU by (force intro: closedin_Union)
    6.41        qed
    6.42        show "continuous_on ({0..1} \<times> (V i - (\<Union>m<i. V m))) (h i)" for i
    6.43          by (rule continuous_on_subset [OF conth]) auto
    6.44 -      show "\<And>i j x. x \<in> {0..1} \<times> UNION UNIV V \<inter>
    6.45 +      show "\<And>i j x. x \<in> {0..1} \<times> \<Union>(V ` UNIV) \<inter>
    6.46                      {0..1} \<times> (V i - (\<Union>m<i. V m)) \<inter> {0..1} \<times> (V j - (\<Union>m<j. V m))
    6.47                      \<Longrightarrow> h i x = h j x"
    6.48          by clarsimp (metis lessThan_iff linorder_neqE_nat)
     7.1 --- a/src/HOL/Analysis/Caratheodory.thy	Sun Nov 18 09:51:41 2018 +0100
     7.2 +++ b/src/HOL/Analysis/Caratheodory.thy	Sun Nov 18 18:07:51 2018 +0000
     7.3 @@ -321,7 +321,7 @@
     7.4  next
     7.5    have "(\<Sum>i. f (if i = 0 then s else {})) \<le> f s"
     7.6      using positiveD1[OF posf] by (subst suminf_finite[of "{0}"]) auto
     7.7 -  with s show "(INF A\<in>{A. range A \<subseteq> M \<and> disjoint_family A \<and> s \<subseteq> UNION UNIV A}. \<Sum>i. f (A i)) \<le> f s"
     7.8 +  with s show "(INF A\<in>{A. range A \<subseteq> M \<and> disjoint_family A \<and> s \<subseteq> \<Union>(A ` UNIV)}. \<Sum>i. f (A i)) \<le> f s"
     7.9      by (intro INF_lower2[of "\<lambda>i. if i = 0 then s else {}"])
    7.10         (auto simp: disjoint_family_on_def)
    7.11  qed
    7.12 @@ -521,8 +521,8 @@
    7.13  
    7.14  lemma%unimportant volume_finite_additive:
    7.15    assumes "volume M f"
    7.16 -  assumes A: "\<And>i. i \<in> I \<Longrightarrow> A i \<in> M" "disjoint_family_on A I" "finite I" "UNION I A \<in> M"
    7.17 -  shows "f (UNION I A) = (\<Sum>i\<in>I. f (A i))"
    7.18 +  assumes A: "\<And>i. i \<in> I \<Longrightarrow> A i \<in> M" "disjoint_family_on A I" "finite I" "\<Union>(A ` I) \<in> M"
    7.19 +  shows "f (\<Union>(A ` I)) = (\<Sum>i\<in>I. f (A i))"
    7.20  proof -
    7.21    have "A`I \<subseteq> M" "disjoint (A`I)" "finite (A`I)" "\<Union>(A`I) \<in> M"
    7.22      using A by (auto simp: disjoint_family_on_disjoint_image)
    7.23 @@ -536,7 +536,7 @@
    7.24      then show "f (A i) = 0"
    7.25        using volume_empty[OF \<open>volume M f\<close>] by simp
    7.26    qed (auto intro: \<open>finite I\<close>)
    7.27 -  finally show "f (UNION I A) = (\<Sum>i\<in>I. f (A i))"
    7.28 +  finally show "f (\<Union>(A ` I)) = (\<Sum>i\<in>I. f (A i))"
    7.29      by simp
    7.30  qed
    7.31  
     8.1 --- a/src/HOL/Analysis/Change_Of_Vars.thy	Sun Nov 18 09:51:41 2018 +0100
     8.2 +++ b/src/HOL/Analysis/Change_Of_Vars.thy	Sun Nov 18 18:07:51 2018 +0000
     8.3 @@ -629,26 +629,26 @@
     8.4  
     8.5  (*https://en.wikipedia.org/wiki/F\<sigma>_set*)
     8.6  inductive%important fsigma :: "'a::topological_space set \<Rightarrow> bool" where
     8.7 -  "(\<And>n::nat. closed (F n)) \<Longrightarrow> fsigma (UNION UNIV F)"
     8.8 +  "(\<And>n::nat. closed (F n)) \<Longrightarrow> fsigma (\<Union>(F ` UNIV))"
     8.9  
    8.10  inductive%important gdelta :: "'a::topological_space set \<Rightarrow> bool" where
    8.11 -  "(\<And>n::nat. open (F n)) \<Longrightarrow> gdelta (INTER UNIV F)"
    8.12 +  "(\<And>n::nat. open (F n)) \<Longrightarrow> gdelta (\<Inter>(F ` UNIV))"
    8.13  
    8.14  lemma%important fsigma_Union_compact:
    8.15    fixes S :: "'a::{real_normed_vector,heine_borel} set"
    8.16 -  shows "fsigma S \<longleftrightarrow> (\<exists>F::nat \<Rightarrow> 'a set. range F \<subseteq> Collect compact \<and> S = UNION UNIV F)"
    8.17 +  shows "fsigma S \<longleftrightarrow> (\<exists>F::nat \<Rightarrow> 'a set. range F \<subseteq> Collect compact \<and> S = \<Union>(F ` UNIV))"
    8.18  proof%unimportant safe
    8.19    assume "fsigma S"
    8.20 -  then obtain F :: "nat \<Rightarrow> 'a set" where F: "range F \<subseteq> Collect closed" "S = UNION UNIV F"
    8.21 +  then obtain F :: "nat \<Rightarrow> 'a set" where F: "range F \<subseteq> Collect closed" "S = \<Union>(F ` UNIV)"
    8.22      by (meson fsigma.cases image_subsetI mem_Collect_eq)
    8.23 -  then have "\<exists>D::nat \<Rightarrow> 'a set. range D \<subseteq> Collect compact \<and> UNION UNIV D = F i" for i
    8.24 +  then have "\<exists>D::nat \<Rightarrow> 'a set. range D \<subseteq> Collect compact \<and> \<Union>(D ` UNIV) = F i" for i
    8.25      using closed_Union_compact_subsets [of "F i"]
    8.26      by (metis image_subsetI mem_Collect_eq range_subsetD)
    8.27    then obtain D :: "nat \<Rightarrow> nat \<Rightarrow> 'a set"
    8.28 -    where D: "\<And>i. range (D i) \<subseteq> Collect compact \<and> UNION UNIV (D i) = F i"
    8.29 +    where D: "\<And>i. range (D i) \<subseteq> Collect compact \<and> \<Union>((D i) ` UNIV) = F i"
    8.30      by metis
    8.31    let ?DD = "\<lambda>n. (\<lambda>(i,j). D i j) (prod_decode n)"
    8.32 -  show "\<exists>F::nat \<Rightarrow> 'a set. range F \<subseteq> Collect compact \<and> S = UNION UNIV F"
    8.33 +  show "\<exists>F::nat \<Rightarrow> 'a set. range F \<subseteq> Collect compact \<and> S = \<Union>(F ` UNIV)"
    8.34    proof (intro exI conjI)
    8.35      show "range ?DD \<subseteq> Collect compact"
    8.36        using D by clarsimp (metis mem_Collect_eq rangeI split_conv subsetCE surj_pair)
    8.37 @@ -663,15 +663,15 @@
    8.38    qed
    8.39  next
    8.40    fix F :: "nat \<Rightarrow> 'a set"
    8.41 -  assume "range F \<subseteq> Collect compact" and "S = UNION UNIV F"
    8.42 -  then show "fsigma (UNION UNIV F)"
    8.43 +  assume "range F \<subseteq> Collect compact" and "S = \<Union>(F ` UNIV)"
    8.44 +  then show "fsigma (\<Union>(F ` UNIV))"
    8.45      by (simp add: compact_imp_closed fsigma.intros image_subset_iff)
    8.46  qed
    8.47  
    8.48  lemma%unimportant gdelta_imp_fsigma: "gdelta S \<Longrightarrow> fsigma (- S)"
    8.49  proof (induction rule: gdelta.induct)
    8.50    case (1 F)
    8.51 -  have "- INTER UNIV F = (\<Union>i. -(F i))"
    8.52 +  have "- \<Inter>(F ` UNIV) = (\<Union>i. -(F i))"
    8.53      by auto
    8.54    then show ?case
    8.55      by (simp add: fsigma.intros closed_Compl 1)
    8.56 @@ -680,7 +680,7 @@
    8.57  lemma%unimportant fsigma_imp_gdelta: "fsigma S \<Longrightarrow> gdelta (- S)"
    8.58  proof (induction rule: fsigma.induct)
    8.59    case (1 F)
    8.60 -  have "- UNION UNIV F = (\<Inter>i. -(F i))"
    8.61 +  have "- \<Union>(F ` UNIV) = (\<Inter>i. -(F i))"
    8.62      by auto
    8.63    then show ?case
    8.64      by (simp add: 1 gdelta.intros open_closed)
    8.65 @@ -701,7 +701,7 @@
    8.66    }
    8.67    then obtain F where F: "\<And>n::nat. closed (F n) \<and> F n \<subseteq> S \<and> S - F n \<in> lmeasurable \<and> measure lebesgue (S - F n) < 1 / Suc n"
    8.68      by metis
    8.69 -  let ?C = "UNION UNIV F"
    8.70 +  let ?C = "\<Union>(F ` UNIV)"
    8.71    show thesis
    8.72    proof
    8.73      show "fsigma ?C"
    8.74 @@ -3730,13 +3730,13 @@
    8.75      unfolding Ceq
    8.76    proof (rule has_absolute_integral_change_of_variables_compact_family)
    8.77      fix n x
    8.78 -    assume "x \<in> UNION UNIV F"
    8.79 -    then show "(g has_derivative g' x) (at x within UNION UNIV F)"
    8.80 +    assume "x \<in> \<Union>(F ` UNIV)"
    8.81 +    then show "(g has_derivative g' x) (at x within \<Union>(F ` UNIV))"
    8.82        using Ceq \<open>C \<union> N = S\<close> der_g has_derivative_within_subset by blast
    8.83    next
    8.84 -    have "UNION UNIV F \<subseteq> S"
    8.85 +    have "\<Union>(F ` UNIV) \<subseteq> S"
    8.86        using Ceq \<open>C \<union> N = S\<close> by blast
    8.87 -    then show "inj_on g (UNION UNIV F)"
    8.88 +    then show "inj_on g (\<Union>(F ` UNIV))"
    8.89        using inj by (meson inj_on_subset)
    8.90    qed (use F in auto)
    8.91    moreover
     9.1 --- a/src/HOL/Analysis/Complete_Measure.thy	Sun Nov 18 09:51:41 2018 +0100
     9.2 +++ b/src/HOL/Analysis/Complete_Measure.thy	Sun Nov 18 18:07:51 2018 +0000
     9.3 @@ -62,9 +62,9 @@
     9.4    from choice[OF this] guess S ..
     9.5    from choice[OF this] guess N ..
     9.6    from choice[OF this] guess N' ..
     9.7 -  then show "UNION UNIV A \<in> ?A"
     9.8 +  then show "\<Union>(A ` UNIV) \<in> ?A"
     9.9      using null_sets_UN[of N']
    9.10 -    by (intro completionI[of _ "UNION UNIV S" "UNION UNIV N" "UNION UNIV N'"]) auto
    9.11 +    by (intro completionI[of _ "\<Union>(S ` UNIV)" "\<Union>(N ` UNIV)" "\<Union>(N' ` UNIV)"]) auto
    9.12  qed
    9.13  
    9.14  lemma sets_completion:
    9.15 @@ -199,7 +199,7 @@
    9.16      qed
    9.17      then have "(\<Sum>n. emeasure M (main_part M (A n))) = emeasure M (\<Union>i. main_part M (A i))"
    9.18        using A by (auto intro!: suminf_emeasure)
    9.19 -    then show "(\<Sum>n. ?\<mu> (A n)) = ?\<mu> (UNION UNIV A)"
    9.20 +    then show "(\<Sum>n. ?\<mu> (A n)) = ?\<mu> (\<Union>(A ` UNIV))"
    9.21        by (simp add: completion_def emeasure_main_part_UN[OF A(1)])
    9.22    qed
    9.23  qed
    10.1 --- a/src/HOL/Analysis/Embed_Measure.thy	Sun Nov 18 09:51:41 2018 +0100
    10.2 +++ b/src/HOL/Analysis/Embed_Measure.thy	Sun Nov 18 18:07:51 2018 +0000
    10.3 @@ -401,7 +401,7 @@
    10.4    also have "\<dots> = (SUP i\<in>Y. \<integral>\<^sup>+ x. f i (from_nat_into B (to_nat_on B x)) \<partial>count_space B)"
    10.5      by(simp add: embed_measure_count_space'[symmetric] inj_on_to_nat_on countable nn_integral_embed_measure' measurable_embed_measure1)
    10.6    also have "\<dots> = ?rhs"
    10.7 -    by(intro arg_cong2[where f="SUPREMUM"] ext nn_integral_cong_AE)(simp_all add: AE_count_space countable)
    10.8 +    by(intro arg_cong2[where f = "\<lambda>A f. Sup (f ` A)"] ext nn_integral_cong_AE)(simp_all add: AE_count_space countable)
    10.9    finally show ?thesis .
   10.10  qed
   10.11  
    11.1 --- a/src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy	Sun Nov 18 09:51:41 2018 +0100
    11.2 +++ b/src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy	Sun Nov 18 18:07:51 2018 +0000
    11.3 @@ -253,7 +253,7 @@
    11.4            using \<open>E \<subseteq> space ?L\<close> by (auto simp: space_restrict_space)
    11.5          then obtain z k where "(z, k) \<in> p" "v \<in> k"
    11.6            using tagged_division_ofD(6)[OF p(1), symmetric] by auto
    11.7 -        with not show "v \<in> UNION (p - s) snd"
    11.8 +        with not show "v \<in> \<Union>(snd ` (p - s))"
    11.9            by (auto intro!: bexI[of _ "(z, k)"] elim: ballE[of _ _ "(z, k)"])
   11.10        qed (auto intro!: sets.Int sets.finite_UN ennreal_mono_minus intro: p_in_L)
   11.11        also have "\<dots> = measure ?L (\<Union>x\<in>p \<inter> s. snd x)"
   11.12 @@ -299,9 +299,9 @@
   11.13    define B :: "nat \<Rightarrow> 'a set" where "B n = cbox (- real n *\<^sub>R One) (real n *\<^sub>R One)" for n
   11.14    show "(\<lambda>x. f x * indicator \<Omega> x) \<in> lebesgue \<rightarrow>\<^sub>M borel"
   11.15    proof (rule measurable_piecewise_restrict)
   11.16 -    have "(\<Union>n. box (- real n *\<^sub>R One) (real n *\<^sub>R One)) \<subseteq> UNION UNIV B"
   11.17 +    have "(\<Union>n. box (- real n *\<^sub>R One) (real n *\<^sub>R One)) \<subseteq> \<Union>(B ` UNIV)"
   11.18        unfolding B_def by (intro UN_mono box_subset_cbox order_refl)
   11.19 -    then show "countable (range B)" "space lebesgue \<subseteq> UNION UNIV B"
   11.20 +    then show "countable (range B)" "space lebesgue \<subseteq> \<Union>(B ` UNIV)"
   11.21        by (auto simp: B_def UN_box_eq_UNIV)
   11.22    next
   11.23      fix \<Omega>' assume "\<Omega>' \<in> range B"
   11.24 @@ -398,7 +398,7 @@
   11.25        case (union F)
   11.26        then have [measurable]: "\<And>i. F i \<in> sets borel"
   11.27          by (simp add: borel_eq_box subset_eq)
   11.28 -      have "((\<lambda>x. if x \<in> UNION UNIV F \<inter> box a b then 1 else 0) has_integral ?M (\<Union>i. F i)) (box a b)"
   11.29 +      have "((\<lambda>x. if x \<in> \<Union>(F ` UNIV) \<inter> box a b then 1 else 0) has_integral ?M (\<Union>i. F i)) (box a b)"
   11.30        proof (rule has_integral_monotone_convergence_increasing)
   11.31          let ?f = "\<lambda>k x. \<Sum>i<k. if x \<in> F i \<inter> box a b then 1 else 0 :: real"
   11.32          show "\<And>k. (?f k has_integral (\<Sum>i<k. ?M (F i))) (box a b)"
   11.33 @@ -407,7 +407,7 @@
   11.34            by (intro sum_mono2) auto
   11.35          from union(1) have *: "\<And>x i j. x \<in> F i \<Longrightarrow> x \<in> F j \<longleftrightarrow> j = i"
   11.36            by (auto simp add: disjoint_family_on_def)
   11.37 -        show "\<And>x. (\<lambda>k. ?f k x) \<longlonglongrightarrow> (if x \<in> UNION UNIV F \<inter> box a b then 1 else 0)"
   11.38 +        show "\<And>x. (\<lambda>k. ?f k x) \<longlonglongrightarrow> (if x \<in> \<Union>(F ` UNIV) \<inter> box a b then 1 else 0)"
   11.39            apply (auto simp: * sum.If_cases Iio_Int_singleton)
   11.40            apply (rule_tac k="Suc xa" in LIMSEQ_offset)
   11.41            apply simp
   11.42 @@ -1915,7 +1915,7 @@
   11.43      using S measurable_integrable by blast
   11.44    have 2: "\<And>n x::'a. indicat_real (S n) x \<le> (indicat_real (S (Suc n)) x)"
   11.45      by (simp add: indicator_leI nest rev_subsetD)
   11.46 -  have 3: "\<And>x. (\<lambda>n. indicat_real (S n) x) \<longlonglongrightarrow> (indicat_real (UNION UNIV S) x)"
   11.47 +  have 3: "\<And>x. (\<lambda>n. indicat_real (S n) x) \<longlonglongrightarrow> (indicat_real (\<Union>(S ` UNIV)) x)"
   11.48      apply (rule Lim_eventually)
   11.49      apply (simp add: indicator_def)
   11.50      by (metis eventually_sequentiallyI lift_Suc_mono_le nest subsetCE)
   11.51 @@ -2046,13 +2046,13 @@
   11.52      and cov: "\<And>x. x \<in> S \<Longrightarrow> x \<in> U x"
   11.53      and neg: "\<And>x. x \<in> S \<Longrightarrow> negligible (U x)"
   11.54      by metis
   11.55 -  obtain \<F> where "\<F> \<subseteq> U ` S" "countable \<F>" and eq: "\<Union>\<F> = UNION S U"
   11.56 +  obtain \<F> where "\<F> \<subseteq> U ` S" "countable \<F>" and eq: "\<Union>\<F> = \<Union>(U ` S)"
   11.57      using ope by (force intro: Lindelof_openin [of "U ` S" S])
   11.58    then have "negligible (\<Union>\<F>)"
   11.59      by (metis imageE neg negligible_countable_Union subset_eq)
   11.60 -  with eq have "negligible (UNION S U)"
   11.61 +  with eq have "negligible (\<Union>(U ` S))"
   11.62      by metis
   11.63 -  moreover have "S \<subseteq> UNION S U"
   11.64 +  moreover have "S \<subseteq> \<Union>(U ` S)"
   11.65      using cov by blast
   11.66    ultimately show "negligible S"
   11.67      using negligible_subset by blast
   11.68 @@ -2558,9 +2558,9 @@
   11.69          using prems by auto
   11.70      qed
   11.71      then obtain d K where ddiv: "d division_of \<Union>d" and "K = (\<Sum>k\<in>d. norm (integral k f))"
   11.72 -      "SUPREMUM {d. d division_of \<Union>d} (sum (\<lambda>k. norm (integral k f))) - e < K"
   11.73 +      "Sup (sum (\<lambda>k. norm (integral k f)) ` {d. d division_of \<Union> d}) - e < K"
   11.74        by (auto simp add: image_iff not_le)
   11.75 -    then have d: "SUPREMUM {d. d division_of \<Union>d} (sum (\<lambda>k. norm (integral k f))) - e 
   11.76 +    then have d: "Sup (sum (\<lambda>k. norm (integral k f)) ` {d. d division_of \<Union> d}) - e 
   11.77                    < (\<Sum>k\<in>d. norm (integral k f))"
   11.78        by auto
   11.79      note d'=division_ofD[OF ddiv]
   11.80 @@ -2917,11 +2917,11 @@
   11.81              by (metis bounded_linear_image linear_linear assms(1) image_Union range_composition)
   11.82            have "(\<lambda>n. ?\<mu> (X n)) sums ?\<mu> (\<Union>n. X n)"
   11.83              by (rule measure_countable_negligible_Union_bounded [OF 1 2 3])
   11.84 -          have meq: "?\<mu> (\<Union>n. f ` X n) = m * ?\<mu> (UNION UNIV X)"
   11.85 +          have meq: "?\<mu> (\<Union>n. f ` X n) = m * ?\<mu> (\<Union>(X ` UNIV))"
   11.86            proof (rule sums_unique2 [OF measure_countable_negligible_Union_bounded [OF f1 f2 f3]])
   11.87              have m: "\<And>n. ?\<mu> (f ` X n) = (m * ?\<mu> (X n))"
   11.88                using S unfolding bij_betw_def by (metis cbox im rangeI)
   11.89 -            show "(\<lambda>n. ?\<mu> (f ` X n)) sums (m * ?\<mu> (UNION UNIV X))"
   11.90 +            show "(\<lambda>n. ?\<mu> (f ` X n)) sums (m * ?\<mu> (\<Union>(X ` UNIV)))"
   11.91                unfolding m
   11.92                using measure_countable_negligible_Union_bounded [OF 1 2 3] sums_mult by blast
   11.93            qed
   11.94 @@ -3679,24 +3679,24 @@
   11.95    assumes f: "f absolutely_integrable_on (\<Union>(range s))"
   11.96      and s: "\<And>m. s m \<in> sets lebesgue"
   11.97    shows "\<And>n. f absolutely_integrable_on (\<Union>m\<le>n. s m)"
   11.98 -    and "(\<lambda>n. integral (\<Union>m\<le>n. s m) f) \<longlonglongrightarrow> integral (UNION UNIV s) f" (is "?F \<longlonglongrightarrow> ?I")
   11.99 +    and "(\<lambda>n. integral (\<Union>m\<le>n. s m) f) \<longlonglongrightarrow> integral (\<Union>(s ` UNIV)) f" (is "?F \<longlonglongrightarrow> ?I")
  11.100  proof -
  11.101    show fU: "f absolutely_integrable_on (\<Union>m\<le>n. s m)" for n
  11.102      using assms by (blast intro: set_integrable_subset [OF f])
  11.103    have fint: "f integrable_on (\<Union> (range s))"
  11.104      using absolutely_integrable_on_def f by blast
  11.105 -  let ?h = "\<lambda>x. if x \<in> UNION UNIV s then norm(f x) else 0"
  11.106 +  let ?h = "\<lambda>x. if x \<in> \<Union>(s ` UNIV) then norm(f x) else 0"
  11.107    have "(\<lambda>n. integral UNIV (\<lambda>x. if x \<in> (\<Union>m\<le>n. s m) then f x else 0))
  11.108 -        \<longlonglongrightarrow> integral UNIV (\<lambda>x. if x \<in> UNION UNIV s then f x else 0)"
  11.109 +        \<longlonglongrightarrow> integral UNIV (\<lambda>x. if x \<in> \<Union>(s ` UNIV) then f x else 0)"
  11.110    proof (rule dominated_convergence)
  11.111      show "(\<lambda>x. if x \<in> (\<Union>m\<le>n. s m) then f x else 0) integrable_on UNIV" for n
  11.112        unfolding integrable_restrict_UNIV
  11.113        using fU absolutely_integrable_on_def by blast
  11.114 -    show "(\<lambda>x. if x \<in> UNION UNIV s then norm(f x) else 0) integrable_on UNIV"
  11.115 +    show "(\<lambda>x. if x \<in> \<Union>(s ` UNIV) then norm(f x) else 0) integrable_on UNIV"
  11.116        by (metis (no_types) absolutely_integrable_on_def f integrable_restrict_UNIV)
  11.117      show "\<forall>x\<in>UNIV.
  11.118           (\<lambda>n. if x \<in> (\<Union>m\<le>n. s m) then f x else 0)
  11.119 -         \<longlonglongrightarrow> (if x \<in> UNION UNIV s then f x else 0)"
  11.120 +         \<longlonglongrightarrow> (if x \<in> \<Union>(s ` UNIV) then f x else 0)"
  11.121        by (force intro: Lim_eventually eventually_sequentiallyI)
  11.122    qed auto
  11.123    then show "?F \<longlonglongrightarrow> ?I"
    12.1 --- a/src/HOL/Analysis/Extended_Real_Limits.thy	Sun Nov 18 09:51:41 2018 +0100
    12.2 +++ b/src/HOL/Analysis/Extended_Real_Limits.thy	Sun Nov 18 18:07:51 2018 +0000
    12.3 @@ -305,13 +305,13 @@
    12.4    assume "0 < d" and "\<forall>y. y \<in> S \<longrightarrow> y \<noteq> x \<and> dist y x < d \<longrightarrow> P y"
    12.5    then have "S \<inter> ball x d - {x} \<subseteq> {x. P x}"
    12.6      by (auto simp: zero_less_dist_iff dist_commute)
    12.7 -  then show "\<exists>r>0. INFIMUM (Collect P) f \<le> INFIMUM (S \<inter> ball x r - {x}) f"
    12.8 +  then show "\<exists>r>0. Inf (f ` (Collect P)) \<le> Inf (f ` (S \<inter> ball x r - {x}))"
    12.9      by (intro exI[of _ d] INF_mono conjI \<open>0 < d\<close>) auto
   12.10  next
   12.11    fix d :: real
   12.12    assume "0 < d"
   12.13    then show "\<exists>P. (\<exists>d>0. \<forall>xa. xa \<in> S \<longrightarrow> xa \<noteq> x \<and> dist xa x < d \<longrightarrow> P xa) \<and>
   12.14 -    INFIMUM (S \<inter> ball x d - {x}) f \<le> INFIMUM (Collect P) f"
   12.15 +    Inf (f ` (S \<inter> ball x d - {x})) \<le> Inf (f ` (Collect P))"
   12.16      by (intro exI[of _ "\<lambda>y. y \<in> S \<inter> ball x d - {x}"])
   12.17         (auto intro!: INF_mono exI[of _ d] simp: dist_commute)
   12.18  qed
   12.19 @@ -325,13 +325,13 @@
   12.20    assume "0 < d" and "\<forall>y. y \<in> S \<longrightarrow> y \<noteq> x \<and> dist y x < d \<longrightarrow> P y"
   12.21    then have "S \<inter> ball x d - {x} \<subseteq> {x. P x}"
   12.22      by (auto simp: zero_less_dist_iff dist_commute)
   12.23 -  then show "\<exists>r>0. SUPREMUM (S \<inter> ball x r - {x}) f \<le> SUPREMUM (Collect P) f"
   12.24 +  then show "\<exists>r>0. Sup (f ` (S \<inter> ball x r - {x})) \<le> Sup (f ` (Collect P))"
   12.25      by (intro exI[of _ d] SUP_mono conjI \<open>0 < d\<close>) auto
   12.26  next
   12.27    fix d :: real
   12.28    assume "0 < d"
   12.29    then show "\<exists>P. (\<exists>d>0. \<forall>xa. xa \<in> S \<longrightarrow> xa \<noteq> x \<and> dist xa x < d \<longrightarrow> P xa) \<and>
   12.30 -    SUPREMUM (Collect P) f \<le> SUPREMUM (S \<inter> ball x d - {x}) f"
   12.31 +    Sup (f ` (Collect P)) \<le> Sup (f ` (S \<inter> ball x d - {x}))"
   12.32      by (intro exI[of _ "\<lambda>y. y \<in> S \<inter> ball x d - {x}"])
   12.33         (auto intro!: SUP_mono exI[of _ d] simp: dist_commute)
   12.34  qed
   12.35 @@ -1055,11 +1055,11 @@
   12.36    fix P
   12.37    assume P: "eventually P net"
   12.38    fix S
   12.39 -  assume S: "mono_set S" "INFIMUM (Collect P) f \<in> S"
   12.40 +  assume S: "mono_set S" "Inf (f ` (Collect P)) \<in> S"
   12.41    {
   12.42      fix x
   12.43      assume "P x"
   12.44 -    then have "INFIMUM (Collect P) f \<le> f x"
   12.45 +    then have "Inf (f ` (Collect P)) \<le> f x"
   12.46        by (intro complete_lattice_class.INF_lower) simp
   12.47      with S have "f x \<in> S"
   12.48        by (simp add: mono_set)
   12.49 @@ -1069,16 +1069,16 @@
   12.50  next
   12.51    fix y l
   12.52    assume S: "\<forall>S. open S \<longrightarrow> mono_set S \<longrightarrow> l \<in> S \<longrightarrow> eventually  (\<lambda>x. f x \<in> S) net"
   12.53 -  assume P: "\<forall>P. eventually P net \<longrightarrow> INFIMUM (Collect P) f \<le> y"
   12.54 +  assume P: "\<forall>P. eventually P net \<longrightarrow> Inf (f ` (Collect P)) \<le> y"
   12.55    show "l \<le> y"
   12.56    proof (rule dense_le)
   12.57      fix B
   12.58      assume "B < l"
   12.59      then have "eventually (\<lambda>x. f x \<in> {B <..}) net"
   12.60        by (intro S[rule_format]) auto
   12.61 -    then have "INFIMUM {x. B < f x} f \<le> y"
   12.62 +    then have "Inf (f ` {x. B < f x}) \<le> y"
   12.63        using P by auto
   12.64 -    moreover have "B \<le> INFIMUM {x. B < f x} f"
   12.65 +    moreover have "B \<le> Inf (f ` {x. B < f x})"
   12.66        by (intro INF_greatest) auto
   12.67      ultimately show "B \<le> y"
   12.68        by simp
   12.69 @@ -1094,13 +1094,13 @@
   12.70    fix P
   12.71    assume P: "eventually P net"
   12.72    fix S
   12.73 -  assume S: "mono_set (uminus`S)" "SUPREMUM (Collect P) f \<in> S"
   12.74 +  assume S: "mono_set (uminus`S)" "Sup (f ` (Collect P)) \<in> S"
   12.75    {
   12.76      fix x
   12.77      assume "P x"
   12.78 -    then have "f x \<le> SUPREMUM (Collect P) f"
   12.79 +    then have "f x \<le> Sup (f ` (Collect P))"
   12.80        by (intro complete_lattice_class.SUP_upper) simp
   12.81 -    with S(1)[unfolded mono_set, rule_format, of "- SUPREMUM (Collect P) f" "- f x"] S(2)
   12.82 +    with S(1)[unfolded mono_set, rule_format, of "- Sup (f ` (Collect P))" "- f x"] S(2)
   12.83      have "f x \<in> S"
   12.84        by (simp add: inj_image_mem_iff) }
   12.85    with P show "eventually (\<lambda>x. f x \<in> S) net"
   12.86 @@ -1108,16 +1108,16 @@
   12.87  next
   12.88    fix y l
   12.89    assume S: "\<forall>S. open S \<longrightarrow> mono_set (uminus ` S) \<longrightarrow> l \<in> S \<longrightarrow> eventually  (\<lambda>x. f x \<in> S) net"
   12.90 -  assume P: "\<forall>P. eventually P net \<longrightarrow> y \<le> SUPREMUM (Collect P) f"
   12.91 +  assume P: "\<forall>P. eventually P net \<longrightarrow> y \<le> Sup (f ` (Collect P))"
   12.92    show "y \<le> l"
   12.93    proof (rule dense_ge)
   12.94      fix B
   12.95      assume "l < B"
   12.96      then have "eventually (\<lambda>x. f x \<in> {..< B}) net"
   12.97        by (intro S[rule_format]) auto
   12.98 -    then have "y \<le> SUPREMUM {x. f x < B} f"
   12.99 +    then have "y \<le> Sup (f ` {x. f x < B})"
  12.100        using P by auto
  12.101 -    moreover have "SUPREMUM {x. f x < B} f \<le> B"
  12.102 +    moreover have "Sup (f ` {x. f x < B}) \<le> B"
  12.103        by (intro SUP_least) auto
  12.104      ultimately show "y \<le> B"
  12.105        by simp
  12.106 @@ -1240,7 +1240,7 @@
  12.107      apply (rule INF_eq) using \<open>decseq v\<close> decseq_Suc_iff by auto
  12.108    moreover have "decseq (\<lambda>n. (SUP m\<in>{n..}. u m))" by (simp add: SUP_subset_mono decseq_def)
  12.109    ultimately have c: "(INF n\<in>{1..}. (SUP m\<in>{n..}. u m)) = (INF n. (SUP m\<in>{n..}. u m))" by simp
  12.110 -  have "(INF n. SUPREMUM {n..} u) = (INF n. SUP m\<in>{n..}. u (m + 1))" using a b c by simp
  12.111 +  have "(INF n. Sup (u ` {n..})) = (INF n. SUP m\<in>{n..}. u (m + 1))" using a b c by simp
  12.112    then show ?thesis by (auto cong: limsup_INF_SUP)
  12.113  qed
  12.114  
  12.115 @@ -1264,7 +1264,7 @@
  12.116      apply (rule SUP_eq) using \<open>incseq v\<close> incseq_Suc_iff by auto
  12.117    moreover have "incseq (\<lambda>n. (INF m\<in>{n..}. u m))" by (simp add: INF_superset_mono mono_def)
  12.118    ultimately have c: "(SUP n\<in>{1..}. (INF m\<in>{n..}. u m)) = (SUP n. (INF m\<in>{n..}. u m))" by simp
  12.119 -  have "(SUP n. INFIMUM {n..} u) = (SUP n. INF m\<in>{n..}. u (m + 1))" using a b c by simp
  12.120 +  have "(SUP n. Inf (u ` {n..})) = (SUP n. INF m\<in>{n..}. u (m + 1))" using a b c by simp
  12.121    then show ?thesis by (auto cong: liminf_SUP_INF)
  12.122  qed
  12.123  
  12.124 @@ -1753,12 +1753,12 @@
  12.125    fix v u :: "nat \<Rightarrow> ereal" assume *: "\<forall>x. 0 \<le> v x" "\<forall>x. 0 \<le> u x" "\<And>n. v n \<le> u n"
  12.126    moreover have "0 \<le> limsup u - limsup v"
  12.127      using * by (intro ereal_diff_positive Limsup_mono always_eventually) simp
  12.128 -  moreover have "0 \<le> (SUPREMUM {x..} v)" for x
  12.129 +  moreover have "0 \<le> Sup (u ` {x..})" for x
  12.130      using * by (intro SUP_upper2[of x]) auto
  12.131 -  moreover have "0 \<le> (SUPREMUM {x..} u)" for x
  12.132 +  moreover have "0 \<le> Sup (v ` {x..})" for x
  12.133      using * by (intro SUP_upper2[of x]) auto
  12.134    ultimately show "(SUP n. INF n\<in>{n..}. max 0 (u n - v n))
  12.135 -            \<le> max 0 ((INF x. max 0 (SUPREMUM {x..} u)) - (INF x. max 0 (SUPREMUM {x..} v)))"
  12.136 +            \<le> max 0 ((INF x. max 0 (Sup (u ` {x..}))) - (INF x. max 0 (Sup (v ` {x..}))))"
  12.137      by (auto simp: * ereal_diff_positive max.absorb2 liminf_SUP_INF[symmetric] limsup_INF_SUP[symmetric] ereal_liminf_limsup_minus)
  12.138  qed
  12.139  
    13.1 --- a/src/HOL/Analysis/Finite_Product_Measure.thy	Sun Nov 18 09:51:41 2018 +0100
    13.2 +++ b/src/HOL/Analysis/Finite_Product_Measure.thy	Sun Nov 18 18:07:51 2018 +0000
    13.3 @@ -779,7 +779,7 @@
    13.4    show ?case
    13.5    proof (intro exI[of _ "\<Union>i. J i"] bexI[of _ "\<Union>i. prod_emb (\<Union>i. J i) M (J i) (X i)"] conjI)
    13.6      show "(\<Union>i. J i) \<subseteq> I" "countable (\<Union>i. J i)" using J by auto
    13.7 -    with J show "UNION UNIV K = prod_emb I M (\<Union>i. J i) (\<Union>i. prod_emb (\<Union>i. J i) M (J i) (X i))"
    13.8 +    with J show "\<Union>(K ` UNIV) = prod_emb I M (\<Union>i. J i) (\<Union>i. prod_emb (\<Union>i. J i) M (J i) (X i))"
    13.9        by (simp add: K[abs_def] SUP_upper)
   13.10    qed(auto intro: X)
   13.11  qed
    14.1 --- a/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy	Sun Nov 18 09:51:41 2018 +0100
    14.2 +++ b/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy	Sun Nov 18 18:07:51 2018 +0000
    14.3 @@ -5635,15 +5635,15 @@
    14.4          using qq by auto
    14.5        show "\<And>i1 i2. \<lbrakk>i1 \<in> r; i2 \<in> r; i1 \<noteq> i2\<rbrakk> \<Longrightarrow> interior i1 \<inter> interior i2 = {}"
    14.6          by (simp add: q'(5) r_def)
    14.7 -      show "interior (UNION p snd) \<inter> interior (\<Union>r) = {}"
    14.8 +      show "interior (\<Union>(snd ` p)) \<inter> interior (\<Union>r) = {}"
    14.9        proof (rule Int_interior_Union_intervals [OF \<open>finite r\<close>])
   14.10 -        show "open (interior (UNION p snd))"
   14.11 +        show "open (interior (\<Union>(snd ` p)))"
   14.12            by blast
   14.13          show "\<And>T. T \<in> r \<Longrightarrow> \<exists>a b. T = cbox a b"
   14.14            by (simp add: q'(4) r_def)
   14.15          have "finite (snd ` p)"
   14.16            by (simp add: p'(1))
   14.17 -        then show "\<And>T. T \<in> r \<Longrightarrow> interior (UNION p snd) \<inter> interior T = {}"
   14.18 +        then show "\<And>T. T \<in> r \<Longrightarrow> interior (\<Union>(snd ` p)) \<inter> interior T = {}"
   14.19            apply (subst Int_commute)
   14.20            apply (rule Int_interior_Union_intervals)
   14.21            using r_def q'(5) q(1) apply auto
   14.22 @@ -5672,7 +5672,7 @@
   14.23        then show "content L *\<^sub>R f x = 0"
   14.24          unfolding uv content_eq_0_interior[symmetric] by auto
   14.25      qed
   14.26 -    show "finite (UNION r qq)"
   14.27 +    show "finite (\<Union>(qq ` r))"
   14.28        by (meson finite_UN qq \<open>finite r\<close> tagged_division_of_finite)
   14.29    qed
   14.30    moreover have "content M *\<^sub>R f x = 0" 
    15.1 --- a/src/HOL/Analysis/Homeomorphism.thy	Sun Nov 18 09:51:41 2018 +0100
    15.2 +++ b/src/HOL/Analysis/Homeomorphism.thy	Sun Nov 18 18:07:51 2018 +0000
    15.3 @@ -1020,13 +1020,13 @@
    15.4          tv: "\<And>x. x \<in> S
    15.5               \<Longrightarrow> v x \<subseteq> S \<and> open (t x) \<and> compact (v x) \<and> (\<exists>u. x \<in> u \<and> u \<subseteq> v x \<and> u = S \<inter> t x)"
    15.6      by metis
    15.7 -  then have o: "open (UNION S t)"
    15.8 +  then have o: "open (\<Union>(t ` S))"
    15.9      by blast
   15.10    have "S = \<Union> (v ` S)"
   15.11      using tv by blast
   15.12 -  also have "... = UNION S t \<inter> closure S"
   15.13 +  also have "... = \<Union>(t ` S) \<inter> closure S"
   15.14    proof
   15.15 -    show "UNION S v \<subseteq> UNION S t \<inter> closure S"
   15.16 +    show "\<Union>(v ` S) \<subseteq> \<Union>(t ` S) \<inter> closure S"
   15.17        apply safe
   15.18         apply (metis Int_iff subsetD UN_iff tv)
   15.19        apply (simp add: closure_def rev_subsetD tv)
   15.20 @@ -1039,10 +1039,10 @@
   15.21          by (metis Int_commute closure_minimal compact_imp_closed that tv)
   15.22        finally show ?thesis .
   15.23      qed
   15.24 -    then show "UNION S t \<inter> closure S \<subseteq> UNION S v"
   15.25 +    then show "\<Union>(t ` S) \<inter> closure S \<subseteq> \<Union>(v ` S)"
   15.26        by blast
   15.27    qed
   15.28 -  finally have e: "S = UNION S t \<inter> closure S" .
   15.29 +  finally have e: "S = \<Union>(t ` S) \<inter> closure S" .
   15.30    show ?thesis
   15.31      by (rule that [OF o e])
   15.32  qed
   15.33 @@ -1624,7 +1624,7 @@
   15.34        by (metis (no_types, lifting) finite_subset_image)
   15.35      then have "tk \<noteq> {}"
   15.36        by auto
   15.37 -    define n where "n = INTER tk NN"
   15.38 +    define n where "n = \<Inter>(NN ` tk)"
   15.39      have "y \<in> n" "open n"
   15.40        using inUS NN \<open>tk \<subseteq> {0..1}\<close> \<open>finite tk\<close>
   15.41        by (auto simp: n_def open_INT subset_iff)
   15.42 @@ -1632,7 +1632,7 @@
   15.43      proof (rule Lebesgue_number_lemma [of "{0..1}" "K ` tk"])
   15.44        show "K ` tk \<noteq> {}"
   15.45          using \<open>tk \<noteq> {}\<close> by auto
   15.46 -      show "{0..1} \<subseteq> UNION tk K"
   15.47 +      show "{0..1} \<subseteq> \<Union>(K ` tk)"
   15.48          using tk by auto
   15.49        show "\<And>B. B \<in> K ` tk \<Longrightarrow> open B"
   15.50          using \<open>tk \<subseteq> {0..1}\<close> K by auto
    16.1 --- a/src/HOL/Analysis/Improper_Integral.thy	Sun Nov 18 09:51:41 2018 +0100
    16.2 +++ b/src/HOL/Analysis/Improper_Integral.thy	Sun Nov 18 18:07:51 2018 +0000
    16.3 @@ -793,7 +793,7 @@
    16.4          proof (rule sum_content_area_over_thin_division)
    16.5            show "snd ` S division_of \<Union>(snd ` S)"
    16.6              by (auto intro: S tagged_partial_division_of_Union_self division_of_tagged_division)
    16.7 -          show "UNION S snd \<subseteq> cbox a b"
    16.8 +          show "\<Union>(snd ` S) \<subseteq> cbox a b"
    16.9              using S by force
   16.10            show "a \<bullet> i \<le> c \<bullet> i" "c \<bullet> i \<le> b \<bullet> i"
   16.11              using mem_box(2) that by blast+
   16.12 @@ -987,7 +987,7 @@
   16.13                    proof -
   16.14                      obtain u v where uv: "L = cbox u v"
   16.15                        using T'_tagged \<open>(x, L) \<in> A\<close> \<open>A \<subseteq> T''\<close> \<open>T'' \<subseteq> T'\<close> by blast
   16.16 -                    have "A tagged_division_of UNION A snd"
   16.17 +                    have "A tagged_division_of \<Union>(snd ` A)"
   16.18                        using A_tagged tagged_partial_division_of_Union_self by auto
   16.19                      then have "interior (K \<inter> {x. x \<bullet> i \<le> c}) = {}"
   16.20                        apply (rule tagged_division_split_left_inj [OF _ \<open>(x,K) \<in> A\<close> \<open>(x,L) \<in> A\<close>])
   16.21 @@ -1016,7 +1016,7 @@
   16.22                    proof -
   16.23                      obtain u v where uv: "L = cbox u v"
   16.24                        using T'_tagged \<open>(x, L) \<in> B\<close> \<open>B \<subseteq> T''\<close> \<open>T'' \<subseteq> T'\<close> by blast
   16.25 -                    have "B tagged_division_of UNION B snd"
   16.26 +                    have "B tagged_division_of \<Union>(snd ` B)"
   16.27                        using B_tagged tagged_partial_division_of_Union_self by auto
   16.28                      then have "interior (K \<inter> {x. c \<le> x \<bullet> i}) = {}"
   16.29                        apply (rule tagged_division_split_right_inj [OF _ \<open>(x,K) \<in> B\<close> \<open>(x,L) \<in> B\<close>])
    17.1 --- a/src/HOL/Analysis/Measure_Space.thy	Sun Nov 18 09:51:41 2018 +0100
    17.2 +++ b/src/HOL/Analysis/Measure_Space.thy	Sun Nov 18 18:07:51 2018 +0000
    17.3 @@ -317,7 +317,7 @@
    17.4      (\<forall>A. range A \<subseteq> M \<longrightarrow> incseq A \<longrightarrow> (\<Union>i. A i) \<in> M \<longrightarrow> (\<lambda>i. f (A i)) \<longlonglongrightarrow> f (\<Union>i. A i))"
    17.5    unfolding countably_additive_def
    17.6  proof safe
    17.7 -  assume count_sum: "\<forall>A. range A \<subseteq> M \<longrightarrow> disjoint_family A \<longrightarrow> UNION UNIV A \<in> M \<longrightarrow> (\<Sum>i. f (A i)) = f (UNION UNIV A)"
    17.8 +  assume count_sum: "\<forall>A. range A \<subseteq> M \<longrightarrow> disjoint_family A \<longrightarrow> \<Union>(A ` UNIV) \<in> M \<longrightarrow> (\<Sum>i. f (A i)) = f (\<Union>(A ` UNIV))"
    17.9    fix A :: "nat \<Rightarrow> 'a set" assume A: "range A \<subseteq> M" "incseq A" "(\<Union>i. A i) \<in> M"
   17.10    then have dA: "range (disjointed A) \<subseteq> M" by (auto simp: range_disjointed_sets)
   17.11    with count_sum[THEN spec, of "disjointed A"] A(3)
   17.12 @@ -1834,7 +1834,7 @@
   17.13    using I
   17.14  proof (induction I rule: finite_induct)
   17.15    case (insert x I)
   17.16 -  have "measure M (F x \<union> UNION I F) = measure M (F x) + measure M (UNION I F)"
   17.17 +  have "measure M (F x \<union> \<Union>(F ` I)) = measure M (F x) + measure M (\<Union>(F ` I))"
   17.18      by (rule measure_Un_AE) (use insert in \<open>auto simp: pairwise_insert\<close>)
   17.19      with insert show ?case
   17.20        by (simp add: pairwise_insert )
   17.21 @@ -3132,7 +3132,7 @@
   17.22  lemma le_measureD3: "A \<le> B \<Longrightarrow> sets A = sets B \<Longrightarrow> emeasure A X \<le> emeasure B X"
   17.23    by (auto simp: le_measure_iff le_fun_def dest: sets_eq_imp_space_eq split: if_split_asm)
   17.24  
   17.25 -lemma UN_space_closed: "UNION S sets \<subseteq> Pow (UNION S space)"
   17.26 +lemma UN_space_closed: "\<Union>(sets ` S) \<subseteq> Pow (\<Union>(space ` S))"
   17.27    using sets.space_closed by auto
   17.28  
   17.29  definition Sup_lexord :: "('a \<Rightarrow> 'b::complete_lattice) \<Rightarrow> ('a set \<Rightarrow> 'a) \<Rightarrow> ('a set \<Rightarrow> 'a) \<Rightarrow> 'a set \<Rightarrow> 'a"
   17.30 @@ -3245,10 +3245,10 @@
   17.31        with ij show "\<exists>k\<in>{P. finite P \<and> P \<subseteq> M}. \<forall>n\<in>N. ?\<mu> i (F n) \<le> ?\<mu> k (F n) \<and> ?\<mu> j (F n) \<le> ?\<mu> k (F n)"
   17.32          by (safe intro!: bexI[of _ "i \<union> j"]) auto
   17.33      next
   17.34 -      show "(SUP P \<in> {P. finite P \<and> P \<subseteq> M}. \<Sum>n. ?\<mu> P (F n)) = (SUP P \<in> {P. finite P \<and> P \<subseteq> M}. ?\<mu> P (UNION UNIV F))"
   17.35 +      show "(SUP P \<in> {P. finite P \<and> P \<subseteq> M}. \<Sum>n. ?\<mu> P (F n)) = (SUP P \<in> {P. finite P \<and> P \<subseteq> M}. ?\<mu> P (\<Union>(F ` UNIV)))"
   17.36        proof (intro SUP_cong refl)
   17.37          fix i assume i: "i \<in> {P. finite P \<and> P \<subseteq> M}"
   17.38 -        show "(\<Sum>n. ?\<mu> i (F n)) = ?\<mu> i (UNION UNIV F)"
   17.39 +        show "(\<Sum>n. ?\<mu> i (F n)) = ?\<mu> i (\<Union>(F ` UNIV))"
   17.40          proof cases
   17.41            assume "i \<noteq> {}" with i ** show ?thesis
   17.42              apply (intro suminf_emeasure \<open>disjoint_family F\<close>)
   17.43 @@ -3294,9 +3294,9 @@
   17.44    next
   17.45      fix a S assume "a \<in> A" and a: "space a = (\<Union>a\<in>A. space a)" and S: "S = {a' \<in> A. space a' = space a}"
   17.46        and neq: "\<And>aa. aa \<in> S \<Longrightarrow> sets aa \<noteq> (\<Union>a\<in>S. sets a)"
   17.47 -    have sp_a: "space a = (UNION S space)"
   17.48 +    have sp_a: "space a = (\<Union>(space ` S))"
   17.49        using \<open>a\<in>A\<close> by (auto simp: S)
   17.50 -    show "x \<le> sigma (UNION S space) (UNION S sets)"
   17.51 +    show "x \<le> sigma (\<Union>(space ` S)) (\<Union>(sets ` S))"
   17.52      proof cases
   17.53        assume [simp]: "space x = space a"
   17.54        have "sets x \<subset> (\<Union>a\<in>S. sets a)"
   17.55 @@ -3363,19 +3363,19 @@
   17.56      unfolding Sup_measure_def
   17.57    proof (intro Sup_lexord[where P="\<lambda>y. y \<le> x"])
   17.58      assume "\<And>a. a \<in> A \<Longrightarrow> space a \<noteq> (\<Union>a\<in>A. space a)"
   17.59 -    show "sigma (UNION A space) {} \<le> x"
   17.60 +    show "sigma (\<Union>(space ` A)) {} \<le> x"
   17.61        using x[THEN le_measureD1] by (subst sigma_le_iff) auto
   17.62    next
   17.63      fix a S assume "a \<in> A" "space a = (\<Union>a\<in>A. space a)" and S: "S = {a' \<in> A. space a' = space a}"
   17.64        "\<And>a. a \<in> S \<Longrightarrow> sets a \<noteq> (\<Union>a\<in>S. sets a)"
   17.65 -    have "UNION S space \<subseteq> space x"
   17.66 +    have "\<Union>(space ` S) \<subseteq> space x"
   17.67        using S le_measureD1[OF x] by auto
   17.68      moreover
   17.69 -    have "UNION S space = space a"
   17.70 +    have "\<Union>(space ` S) = space a"
   17.71        using \<open>a\<in>A\<close> S by auto
   17.72 -    then have "space x = UNION S space \<Longrightarrow> UNION S sets \<subseteq> sets x"
   17.73 +    then have "space x = \<Union>(space ` S) \<Longrightarrow> \<Union>(sets ` S) \<subseteq> sets x"
   17.74        using \<open>a \<in> A\<close> le_measureD2[OF x] by (auto simp: S)
   17.75 -    ultimately show "sigma (UNION S space) (UNION S sets) \<le> x"
   17.76 +    ultimately show "sigma (\<Union>(space ` S)) (\<Union>(sets ` S)) \<le> x"
   17.77        by (subst sigma_le_iff) simp_all
   17.78    next
   17.79      fix a b S S' assume "a \<in> A" and a: "space a = (\<Union>a\<in>A. space a)" and S: "S = {a' \<in> A. space a' = space a}"
   17.80 @@ -3504,17 +3504,17 @@
   17.81    assumes ch: "Complete_Partial_Order.chain (\<le>) (M ` A)" and "A \<noteq> {}"
   17.82    shows "emeasure (SUP i\<in>A. M i) X = (SUP i\<in>A. emeasure (M i) X)"
   17.83  proof (subst emeasure_SUP[OF sets \<open>A \<noteq> {}\<close>])
   17.84 -  show "(SUP J\<in>{J. J \<noteq> {} \<and> finite J \<and> J \<subseteq> A}. emeasure (SUPREMUM J M) X) = (SUP i\<in>A. emeasure (M i) X)"
   17.85 +  show "(SUP J\<in>{J. J \<noteq> {} \<and> finite J \<and> J \<subseteq> A}. emeasure (Sup (M ` J)) X) = (SUP i\<in>A. emeasure (M i) X)"
   17.86    proof (rule SUP_eq)
   17.87      fix J assume "J \<in> {J. J \<noteq> {} \<and> finite J \<and> J \<subseteq> A}"
   17.88      then have J: "Complete_Partial_Order.chain (\<le>) (M ` J)" "finite J" "J \<noteq> {}" and "J \<subseteq> A"
   17.89        using ch[THEN chain_subset, of "M`J"] by auto
   17.90      with in_chain_finite[OF J(1)] obtain j where "j \<in> J" "(SUP j\<in>J. M j) = M j"
   17.91        by auto
   17.92 -    with \<open>J \<subseteq> A\<close> show "\<exists>j\<in>A. emeasure (SUPREMUM J M) X \<le> emeasure (M j) X"
   17.93 +    with \<open>J \<subseteq> A\<close> show "\<exists>j\<in>A. emeasure (Sup (M ` J)) X \<le> emeasure (M j) X"
   17.94        by auto
   17.95    next
   17.96 -    fix j assume "j\<in>A" then show "\<exists>i\<in>{J. J \<noteq> {} \<and> finite J \<and> J \<subseteq> A}. emeasure (M j) X \<le> emeasure (SUPREMUM i M) X"
   17.97 +    fix j assume "j\<in>A" then show "\<exists>i\<in>{J. J \<noteq> {} \<and> finite J \<and> J \<subseteq> A}. emeasure (M j) X \<le> emeasure (Sup (M ` i)) X"
   17.98        by (intro bexI[of _ "{j}"]) auto
   17.99    qed
  17.100  qed
  17.101 @@ -3584,7 +3584,7 @@
  17.102    assumes "\<And>m. m \<in> M \<Longrightarrow> sets m \<subseteq> sets N"
  17.103    shows "sets (Sup M) \<subseteq> sets N"
  17.104  proof -
  17.105 -  have *: "UNION M space = space N"
  17.106 +  have *: "\<Union>(space ` M) = space N"
  17.107      using assms by auto
  17.108    show ?thesis
  17.109      unfolding * using assms by (subst sets_Sup_eq[of M "space N"]) (auto intro!: sets.sigma_sets_subset)
  17.110 @@ -3612,7 +3612,7 @@
  17.111      by (intro const_space \<open>m \<in> M\<close>)
  17.112    have "f \<in> measurable N (sigma (\<Union>m\<in>M. space m) (\<Union>m\<in>M. sets m))"
  17.113    proof (rule measurable_measure_of)
  17.114 -    show "f \<in> space N \<rightarrow> UNION M space"
  17.115 +    show "f \<in> space N \<rightarrow> \<Union>(space ` M)"
  17.116        using measurable_space[OF f] M by auto
  17.117    qed (auto intro: measurable_sets f dest: sets.sets_into_space)
  17.118    also have "measurable N (sigma (\<Union>m\<in>M. space m) (\<Union>m\<in>M. sets m)) = measurable N (Sup M)"
    18.1 --- a/src/HOL/Analysis/Nonnegative_Lebesgue_Integration.thy	Sun Nov 18 09:51:41 2018 +0100
    18.2 +++ b/src/HOL/Analysis/Nonnegative_Lebesgue_Integration.thy	Sun Nov 18 18:07:51 2018 +0000
    18.3 @@ -821,12 +821,12 @@
    18.4  
    18.5  lemma nn_integral_def_finite:
    18.6    "integral\<^sup>N M f = (SUP g \<in> {g. simple_function M g \<and> g \<le> f \<and> (\<forall>x. g x < top)}. integral\<^sup>S M g)"
    18.7 -    (is "_ = SUPREMUM ?A ?f")
    18.8 +    (is "_ = Sup (?A ` ?f)")
    18.9    unfolding nn_integral_def
   18.10  proof (safe intro!: antisym SUP_least)
   18.11    fix g assume g[measurable]: "simple_function M g" "g \<le> f"
   18.12  
   18.13 -  show "integral\<^sup>S M g \<le> SUPREMUM ?A ?f"
   18.14 +  show "integral\<^sup>S M g \<le> Sup (?A ` ?f)"
   18.15    proof cases
   18.16      assume ae: "AE x in M. g x \<noteq> top"
   18.17      let ?G = "{x \<in> space M. g x \<noteq> top}"
   18.18 @@ -835,7 +835,7 @@
   18.19        show "AE x in M. g x = g x * indicator ?G x"
   18.20          using ae AE_space by eventually_elim auto
   18.21      qed (insert g, auto)
   18.22 -    also have "\<dots> \<le> SUPREMUM ?A ?f"
   18.23 +    also have "\<dots> \<le> Sup (?A ` ?f)"
   18.24        using g by (intro SUP_upper) (auto simp: le_fun_def less_top split: split_indicator)
   18.25      finally show ?thesis .
   18.26    next
   18.27 @@ -844,7 +844,7 @@
   18.28        by (subst (asm) AE_iff_measurable[OF _ refl]) auto
   18.29      then have "top = (SUP n. (\<integral>\<^sup>Sx. of_nat n * indicator ?G x \<partial>M))"
   18.30        by (simp add: ennreal_SUP_of_nat_eq_top ennreal_top_eq_mult_iff SUP_mult_right_ennreal[symmetric])
   18.31 -    also have "\<dots> \<le> SUPREMUM ?A ?f"
   18.32 +    also have "\<dots> \<le> Sup (?A ` ?f)"
   18.33        using g
   18.34        by (safe intro!: SUP_least SUP_upper)
   18.35           (auto simp: le_fun_def of_nat_less_top top_unique[symmetric] split: split_indicator
   18.36 @@ -990,7 +990,7 @@
   18.37    unfolding sup_continuous_def
   18.38  proof safe
   18.39    fix C :: "nat \<Rightarrow> 'b" assume C: "incseq C"
   18.40 -  with sup_continuous_mono[OF f] show "(\<integral>\<^sup>+ y. f y (SUPREMUM UNIV C) \<partial>M) = (SUP i. \<integral>\<^sup>+ y. f y (C i) \<partial>M)"
   18.41 +  with sup_continuous_mono[OF f] show "(\<integral>\<^sup>+ y. f y (Sup (C ` UNIV)) \<partial>M) = (SUP i. \<integral>\<^sup>+ y. f y (C i) \<partial>M)"
   18.42      unfolding sup_continuousD[OF f C]
   18.43      by (subst nn_integral_monotone_convergence_SUP) (auto simp: mono_def le_fun_def)
   18.44  qed
   18.45 @@ -1013,7 +1013,7 @@
   18.46          using f N(3) by (intro measurable_If_set) auto }
   18.47    qed
   18.48    also have "\<dots> = (SUP i. (\<integral>\<^sup>+ x. f i x \<partial>M))"
   18.49 -    using f_eq by (force intro!: arg_cong[where f="SUPREMUM UNIV"] nn_integral_cong_AE ext)
   18.50 +    using f_eq by (force intro!: arg_cong[where f = "\<lambda>f. Sup (range f)"] nn_integral_cong_AE ext)
   18.51    finally show ?thesis .
   18.52  qed
   18.53  
   18.54 @@ -1027,7 +1027,7 @@
   18.55    and g: "incseq g" "\<And>i. simple_function M (g i)"
   18.56    and eq: "AE x in M. (SUP i. f i x) = (SUP i. g i x)"
   18.57    shows "(SUP i. integral\<^sup>S M (f i)) = (SUP i. integral\<^sup>S M (g i))"
   18.58 -    (is "SUPREMUM _ ?F = SUPREMUM _ ?G")
   18.59 +    (is "Sup (?F ` _) = Sup (?G ` _)")
   18.60  proof -
   18.61    have "(SUP i. integral\<^sup>S M (f i)) = (\<integral>\<^sup>+x. (SUP i. f i x) \<partial>M)"
   18.62      using f by (rule nn_integral_monotone_convergence_simple)
   18.63 @@ -1414,7 +1414,7 @@
   18.64    unfolding inf_continuous_def
   18.65  proof safe
   18.66    fix C :: "nat \<Rightarrow> 'b" assume C: "decseq C"
   18.67 -  then show "(\<integral>\<^sup>+ y. f y (INFIMUM UNIV C) \<partial>M) = (INF i. \<integral>\<^sup>+ y. f y (C i) \<partial>M)"
   18.68 +  then show "(\<integral>\<^sup>+ y. f y (Inf (C ` UNIV)) \<partial>M) = (INF i. \<integral>\<^sup>+ y. f y (C i) \<partial>M)"
   18.69      using inf_continuous_mono[OF f] bnd
   18.70      by (auto simp add: inf_continuousD[OF f C] fun_eq_iff antimono_def mono_def le_fun_def less_top
   18.71               intro!: nn_integral_monotone_convergence_INF_decseq)
   18.72 @@ -1609,7 +1609,7 @@
   18.73               cong del: if_weak_cong intro!: monoD[OF inf_continuous_mono[OF g], THEN le_funD])
   18.74  next
   18.75    fix C assume "\<And>i::nat. C i \<in> borel_measurable N \<and> (\<forall>s. integral\<^sup>N (M s) (C i) < \<infinity>)" "decseq C"
   18.76 -  with bound show "INFIMUM UNIV C \<in> borel_measurable N \<and> (\<forall>s. integral\<^sup>N (M s) (INFIMUM UNIV C) < \<infinity>)"
   18.77 +  with bound show "Inf (C ` UNIV) \<in> borel_measurable N \<and> (\<forall>s. integral\<^sup>N (M s) (Inf (C ` UNIV)) < \<infinity>)"
   18.78      unfolding INF_apply[abs_def]
   18.79      by (subst nn_integral_monotone_convergence_INF_decseq)
   18.80         (auto simp: INF_less_iff cong: measurable_cong_sets intro!: borel_measurable_INF)
   18.81 @@ -1801,11 +1801,11 @@
   18.82  lemma emeasure_UN_countable:
   18.83    assumes sets[measurable]: "\<And>i. i \<in> I \<Longrightarrow> X i \<in> sets M" and I[simp]: "countable I"
   18.84    assumes disj: "disjoint_family_on X I"
   18.85 -  shows "emeasure M (UNION I X) = (\<integral>\<^sup>+i. emeasure M (X i) \<partial>count_space I)"
   18.86 +  shows "emeasure M (\<Union>(X ` I)) = (\<integral>\<^sup>+i. emeasure M (X i) \<partial>count_space I)"
   18.87  proof -
   18.88 -  have eq: "\<And>x. indicator (UNION I X) x = \<integral>\<^sup>+ i. indicator (X i) x \<partial>count_space I"
   18.89 +  have eq: "\<And>x. indicator (\<Union>(X ` I)) x = \<integral>\<^sup>+ i. indicator (X i) x \<partial>count_space I"
   18.90    proof cases
   18.91 -    fix x assume x: "x \<in> UNION I X"
   18.92 +    fix x assume x: "x \<in> \<Union>(X ` I)"
   18.93      then obtain j where j: "x \<in> X j" "j \<in> I"
   18.94        by auto
   18.95      with disj have "\<And>i. i \<in> I \<Longrightarrow> indicator (X i) x = (indicator {j} i::ennreal)"
   18.96 @@ -1815,7 +1815,7 @@
   18.97    qed (auto simp: nn_integral_0_iff_AE)
   18.98  
   18.99    note sets.countable_UN'[unfolded subset_eq, measurable]
  18.100 -  have "emeasure M (UNION I X) = (\<integral>\<^sup>+x. indicator (UNION I X) x \<partial>M)"
  18.101 +  have "emeasure M (\<Union>(X ` I)) = (\<integral>\<^sup>+x. indicator (\<Union>(X ` I)) x \<partial>M)"
  18.102      by simp
  18.103    also have "\<dots> = (\<integral>\<^sup>+i. \<integral>\<^sup>+x. indicator (X i) x \<partial>M \<partial>count_space I)"
  18.104      by (simp add: eq nn_integral_count_space_nn_integral)
    19.1 --- a/src/HOL/Analysis/Path_Connected.thy	Sun Nov 18 09:51:41 2018 +0100
    19.2 +++ b/src/HOL/Analysis/Path_Connected.thy	Sun Nov 18 18:07:51 2018 +0000
    19.3 @@ -5272,7 +5272,7 @@
    19.4        by metis
    19.5      then obtain T where T: "T \<subseteq> k" "finite T" "k \<subseteq> \<Union>((\<lambda>x. k \<inter> u x) ` T)"
    19.6        by (metis finite_subset_image)
    19.7 -    have Tuv: "UNION T u \<subseteq> UNION T v"
    19.8 +    have Tuv: "\<Union>(u ` T) \<subseteq> \<Union>(v ` T)"
    19.9        using T that by (force simp: dest!: uv)
   19.10      show ?thesis
   19.11        apply (rule_tac x="\<Union>(u ` T)" in exI)
    20.1 --- a/src/HOL/Analysis/Polytope.thy	Sun Nov 18 09:51:41 2018 +0100
    20.2 +++ b/src/HOL/Analysis/Polytope.thy	Sun Nov 18 18:07:51 2018 +0000
    20.3 @@ -3232,7 +3232,7 @@
    20.4      have TU: "convex (T \<inter> U)"
    20.5        by (simp add: \<open>convex T\<close> \<open>convex U\<close> convex_Int)
    20.6      have "(\<Union>x\<in>T. closed_segment z x) \<inter> (\<Union>x\<in>U. closed_segment z x)
    20.7 -          \<subseteq> (if T \<inter> U = {} then {z} else UNION (T \<inter> U) (closed_segment z))" (is "_ \<subseteq> ?IF")
    20.8 +          \<subseteq> (if T \<inter> U = {} then {z} else \<Union>((closed_segment z) ` (T \<inter> U)))" (is "_ \<subseteq> ?IF")
    20.9      proof clarify
   20.10        fix x t u
   20.11        assume xt: "x \<in> closed_segment z t"
    21.1 --- a/src/HOL/Analysis/Set_Integral.thy	Sun Nov 18 09:51:41 2018 +0100
    21.2 +++ b/src/HOL/Analysis/Set_Integral.thy	Sun Nov 18 18:07:51 2018 +0000
    21.3 @@ -368,7 +368,7 @@
    21.4    using assms
    21.5  proof%unimportant induction
    21.6    case (insert x F)
    21.7 -  then have "A x \<inter> UNION F A = {}"
    21.8 +  then have "A x \<inter> \<Union>(A ` F) = {}"
    21.9      by (meson disjoint_family_on_insert)
   21.10    with insert show ?case
   21.11      by (simp add: set_integral_Un set_integrable_Un set_integrable_UN disjoint_family_on_insert)
   21.12 @@ -453,7 +453,7 @@
   21.13        set_lebesgue_integral M (\<Union>i. A i) (\<lambda>x. norm (f x))"
   21.14        by simp
   21.15    qed
   21.16 -  show "LINT x|M. indicator (UNION UNIV A) x *\<^sub>R f x = LINT x|M. (\<Sum>i. indicator (A i) x *\<^sub>R f x)"
   21.17 +  show "LINT x|M. indicator (\<Union>(A ` UNIV)) x *\<^sub>R f x = LINT x|M. (\<Sum>i. indicator (A i) x *\<^sub>R f x)"
   21.18      apply (rule Bochner_Integration.integral_cong[OF refl])
   21.19      apply (subst suminf_scaleR_left[OF sums_summable[OF indicator_sums, OF disj], symmetric])
   21.20      using sums_unique[OF indicator_sums[OF disj]]
   21.21 @@ -472,7 +472,7 @@
   21.22      using intgbl by (rule set_integrable_subset) auto
   21.23    show "\<And>i. (\<lambda>x. indicator (A i) x *\<^sub>R f x) \<in> borel_measurable M"
   21.24      using int_A integrable_iff_bounded set_integrable_def by blast
   21.25 -  show "(\<lambda>x. indicator (UNION UNIV A) x *\<^sub>R f x) \<in> borel_measurable M"
   21.26 +  show "(\<lambda>x. indicator (\<Union>(A ` UNIV)) x *\<^sub>R f x) \<in> borel_measurable M"
   21.27      using integrable_iff_bounded intgbl set_integrable_def by blast
   21.28    show "integrable M (\<lambda>x. indicator (\<Union>i. A i) x *\<^sub>R norm (f x))"
   21.29      using int_A intgbl integrable_norm unfolding set_integrable_def 
   21.30 @@ -501,7 +501,7 @@
   21.31      by force
   21.32    have "set_integrable M (\<Inter>i. A i) f"
   21.33      using int0 by (rule set_integrable_subset) (insert A, auto simp: decseq_def)
   21.34 -  with int_A show "(\<lambda>x. indicat_real (INTER UNIV A) x *\<^sub>R f x) \<in> borel_measurable M"
   21.35 +  with int_A show "(\<lambda>x. indicat_real (\<Inter>(A ` UNIV)) x *\<^sub>R f x) \<in> borel_measurable M"
   21.36                    "\<And>i. (\<lambda>x. indicat_real (A i) x *\<^sub>R f x) \<in> borel_measurable M"
   21.37      by (auto simp: set_integrable_def)
   21.38    show "\<And>i. AE x in M. norm (indicator (A i) x *\<^sub>R f x) \<le> indicator (A 0) x *\<^sub>R norm (f x)"
    22.1 --- a/src/HOL/Analysis/Sigma_Algebra.thy	Sun Nov 18 09:51:41 2018 +0100
    22.2 +++ b/src/HOL/Analysis/Sigma_Algebra.thy	Sun Nov 18 18:07:51 2018 +0000
    22.3 @@ -841,7 +841,7 @@
    22.4    using assms by (induct A) (auto simp: disjoint_def intro!: generated_ring_disjoint_Un generated_ring_empty)
    22.5  
    22.6  lemma (in semiring_of_sets) generated_ring_disjoint_UNION:
    22.7 -  "finite I \<Longrightarrow> disjoint (A ` I) \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> A i \<in> generated_ring) \<Longrightarrow> UNION I A \<in> generated_ring"
    22.8 +  "finite I \<Longrightarrow> disjoint (A ` I) \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> A i \<in> generated_ring) \<Longrightarrow> \<Union>(A ` I) \<in> generated_ring"
    22.9    by (intro generated_ring_disjoint_Union) auto
   22.10  
   22.11  lemma (in semiring_of_sets) generated_ring_Int:
   22.12 @@ -879,7 +879,7 @@
   22.13    using assms by (induct A rule: finite_ne_induct) (auto intro: generated_ring_Int)
   22.14  
   22.15  lemma (in semiring_of_sets) generated_ring_INTER:
   22.16 -  "finite I \<Longrightarrow> I \<noteq> {} \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> A i \<in> generated_ring) \<Longrightarrow> INTER I A \<in> generated_ring"
   22.17 +  "finite I \<Longrightarrow> I \<noteq> {} \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> A i \<in> generated_ring) \<Longrightarrow> \<Inter>(A ` I) \<in> generated_ring"
   22.18    by (intro generated_ring_Inter) auto
   22.19  
   22.20  lemma (in semiring_of_sets) generating_ring:
    23.1 --- a/src/HOL/Analysis/Starlike.thy	Sun Nov 18 09:51:41 2018 +0100
    23.2 +++ b/src/HOL/Analysis/Starlike.thy	Sun Nov 18 18:07:51 2018 +0000
    23.3 @@ -7494,9 +7494,9 @@
    23.4                      and clos: "closure (G x) \<subseteq> F x" and Fin: "F x \<in> \<C>"
    23.5           if "x \<in> S" for x
    23.6      by metis
    23.7 -  then obtain \<F> where "\<F> \<subseteq> G ` S" "countable \<F>" "\<Union>\<F> = UNION S G"
    23.8 +  then obtain \<F> where "\<F> \<subseteq> G ` S" "countable \<F>" "\<Union>\<F> = \<Union>(G ` S)"
    23.9      using Lindelof [of "G ` S"] by (metis image_iff)
   23.10 -  then obtain K where K: "K \<subseteq> S" "countable K" and eq: "UNION K G = UNION S G"
   23.11 +  then obtain K where K: "K \<subseteq> S" "countable K" and eq: "\<Union>(G ` K) = \<Union>(G ` S)"
   23.12      by (metis countable_subset_image)
   23.13    with False Gin have "K \<noteq> {}" by force
   23.14    then obtain a :: "nat \<Rightarrow> 'a" where "range a = K"
   23.15 @@ -7885,7 +7885,7 @@
   23.16      obtain I where "finite I" and I: "K \<subseteq> (\<Union>i\<in>I. interior (f i))"
   23.17      proof (rule compactE_image [OF \<open>compact K\<close>])
   23.18        show "K \<subseteq> (\<Union>n. interior (f n))"
   23.19 -        using \<open>K \<subseteq> S\<close> \<open>UNION UNIV f = S\<close> * by blast
   23.20 +        using \<open>K \<subseteq> S\<close> \<open>\<Union>(f ` UNIV) = S\<close> * by blast
   23.21      qed auto
   23.22      { fix n
   23.23        assume n: "Max I \<le> n"
    24.1 --- a/src/HOL/Analysis/Topology_Euclidean_Space.thy	Sun Nov 18 09:51:41 2018 +0100
    24.2 +++ b/src/HOL/Analysis/Topology_Euclidean_Space.thy	Sun Nov 18 18:07:51 2018 +0000
    24.3 @@ -440,8 +440,8 @@
    24.4          show ?case by (intro exI[of _ "{{}}"]) simp
    24.5        next
    24.6          case (Int a b)
    24.7 -        then obtain x y where x: "a = UNION x Inter" "\<And>i. i \<in> x \<Longrightarrow> finite i \<and> i \<subseteq> B"
    24.8 -          and y: "b = UNION y Inter" "\<And>i. i \<in> y \<Longrightarrow> finite i \<and> i \<subseteq> B"
    24.9 +        then obtain x y where x: "a = \<Union>(Inter ` x)" "\<And>i. i \<in> x \<Longrightarrow> finite i \<and> i \<subseteq> B"
   24.10 +          and y: "b = \<Union>(Inter ` y)" "\<And>i. i \<in> y \<Longrightarrow> finite i \<and> i \<subseteq> B"
   24.11            by blast
   24.12          show ?case
   24.13            unfolding x y Int_UN_distrib2
   24.14 @@ -450,10 +450,10 @@
   24.15          case (UN K)
   24.16          then have "\<forall>k\<in>K. \<exists>B'\<subseteq>{b. finite b \<and> b \<subseteq> B}. UNION B' Inter = k" by auto
   24.17          then obtain k where
   24.18 -            "\<forall>ka\<in>K. k ka \<subseteq> {b. finite b \<and> b \<subseteq> B} \<and> UNION (k ka) Inter = ka"
   24.19 +            "\<forall>ka\<in>K. k ka \<subseteq> {b. finite b \<and> b \<subseteq> B} \<and> \<Union>(Inter ` (k ka)) = ka"
   24.20            unfolding bchoice_iff ..
   24.21          then show "\<exists>B'\<subseteq>{b. finite b \<and> b \<subseteq> B}. UNION B' Inter = \<Union>K"
   24.22 -          by (intro exI[of _ "UNION K k"]) auto
   24.23 +          by (intro exI[of _ "\<Union>(k ` K)"]) auto
   24.24        next
   24.25          case (Basis S)
   24.26          then show ?case
    25.1 --- a/src/HOL/Analysis/Uniform_Limit.thy	Sun Nov 18 09:51:41 2018 +0100
    25.2 +++ b/src/HOL/Analysis/Uniform_Limit.thy	Sun Nov 18 18:07:51 2018 +0000
    25.3 @@ -654,7 +654,7 @@
    25.4  lemma uniform_limit_on_UNION:
    25.5    assumes "finite S"
    25.6    assumes "\<And>s. s \<in> S \<Longrightarrow> uniform_limit (h s) f g F"
    25.7 -  shows "uniform_limit (UNION S h) f g F"
    25.8 +  shows "uniform_limit (\<Union>(h ` S)) f g F"
    25.9    using assms
   25.10    by induct (auto intro: uniform_limit_on_empty uniform_limit_on_Un)
   25.11  
    26.1 --- a/src/HOL/Analysis/Vitali_Covering_Theorem.thy	Sun Nov 18 09:51:41 2018 +0100
    26.2 +++ b/src/HOL/Analysis/Vitali_Covering_Theorem.thy	Sun Nov 18 18:07:51 2018 +0000
    26.3 @@ -617,13 +617,13 @@
    26.4                by (metis mult.commute mult.left_neutral real_mult_le_cancel_iff1 \<open>e > 0\<close> le1)
    26.5              finally show ?thesis .
    26.6            qed
    26.7 -          have "UNION C U \<in> lmeasurable" "?\<mu> (\<Union>(U ` C)) \<le> e"
    26.8 +          have "\<Union>(U ` C) \<in> lmeasurable" "?\<mu> (\<Union>(U ` C)) \<le> e"
    26.9              using \<open>e > 0\<close> Um lee
   26.10              by(auto intro!: fmeasurable_UN_bound [OF \<open>countable C\<close>] measure_UN_bound [OF \<open>countable C\<close>])
   26.11          }
   26.12 -        moreover have "?\<mu> ?T = ?\<mu> (UNION C U)"
   26.13 -        proof (rule measure_negligible_symdiff [OF \<open>UNION C U \<in> lmeasurable\<close>])
   26.14 -          show "negligible((UNION C U - ?T) \<union> (?T - UNION C U))"
   26.15 +        moreover have "?\<mu> ?T = ?\<mu> (\<Union>(U ` C))"
   26.16 +        proof (rule measure_negligible_symdiff [OF \<open>\<Union>(U ` C) \<in> lmeasurable\<close>])
   26.17 +          show "negligible((\<Union>(U ` C) - ?T) \<union> (?T - \<Union>(U ` C)))"
   26.18              by (force intro!: negligible_subset [OF negC])
   26.19          qed
   26.20          ultimately show "?T \<in> lmeasurable"  "?\<mu> ?T \<le> e"
    27.1 --- a/src/HOL/Bali/Basis.thy	Sun Nov 18 09:51:41 2018 +0100
    27.2 +++ b/src/HOL/Bali/Basis.thy	Sun Nov 18 18:07:51 2018 +0000
    27.3 @@ -87,14 +87,13 @@
    27.4    by auto
    27.5  
    27.6  lemma finite_SetCompr2:
    27.7 -  "finite (Collect P) \<Longrightarrow> \<forall>y. P y \<longrightarrow> finite (range (f y)) \<Longrightarrow>
    27.8 -    finite {f y x |x y. P y}"
    27.9 -  apply (subgoal_tac "{f y x |x y. P y} = UNION (Collect P) (\<lambda>y. range (f y))")
   27.10 -   prefer 2 apply fast
   27.11 -  apply (erule ssubst)
   27.12 -  apply (erule finite_UN_I)
   27.13 -  apply fast
   27.14 -  done
   27.15 +  "finite {f y x |x y. P y}" if "finite (Collect P)"
   27.16 +    "\<forall>y. P y \<longrightarrow> finite (range (f y))"
   27.17 +proof -
   27.18 +  have "{f y x |x y. P y} = (\<Union>y\<in>Collect P. range (f y))"
   27.19 +    by auto
   27.20 +  with that show ?thesis by simp
   27.21 +qed
   27.22  
   27.23  lemma list_all2_trans: "\<forall>a b c. P1 a b \<longrightarrow> P2 b c \<longrightarrow> P3 a c \<Longrightarrow>
   27.24      \<forall>xs2 xs3. list_all2 P1 xs1 xs2 \<longrightarrow> list_all2 P2 xs2 xs3 \<longrightarrow> list_all2 P3 xs1 xs3"
    28.1 --- a/src/HOL/Computational_Algebra/Primes.thy	Sun Nov 18 09:51:41 2018 +0100
    28.2 +++ b/src/HOL/Computational_Algebra/Primes.thy	Sun Nov 18 18:07:51 2018 +0000
    28.3 @@ -756,7 +756,7 @@
    28.4  
    28.5  lemma prime_factors_prod:
    28.6    assumes "finite A" and "0 \<notin> f ` A"
    28.7 -  shows "prime_factors (prod f A) = UNION A (prime_factors \<circ> f)"
    28.8 +  shows "prime_factors (prod f A) = \<Union>((prime_factors \<circ> f) ` A)"
    28.9    using assms by (simp add: prod_unfold_prod_mset prime_factorization_prod_mset)
   28.10  
   28.11  lemma prime_factors_fact:
    29.1 --- a/src/HOL/Decision_Procs/MIR.thy	Sun Nov 18 09:51:41 2018 +0100
    29.2 +++ b/src/HOL/Decision_Procs/MIR.thy	Sun Nov 18 18:07:51 2018 +0000
    29.3 @@ -3377,22 +3377,23 @@
    29.4    proof-
    29.5      fix M :: "('a\<times>'b\<times>'c) set" and f :: "('a\<times>'b\<times>'c) \<Rightarrow> 'd list" and g
    29.6      assume "\<forall> (a,b,c) \<in> M. f (a,b,c) = g a b c"
    29.7 -    thus "(UNION M (\<lambda> (a,b,c). set (f (a,b,c)))) = (UNION M (\<lambda> (a,b,c). set (g a b c)))"
    29.8 +    thus "(\<Union>(a, b, c)\<in>M. set (f (a, b, c))) = (\<Union>(a, b, c)\<in>M. set (g a b c))"
    29.9        by (auto simp add: split_def)
   29.10    qed
   29.11    have U3': "\<forall> (p,n,s) \<in> {(p,n,s). (p,n,s) \<in> ?SS a \<and> n<0}. ?ff (p,n,s) = map (?f(p,n,s)) [n..0]"
   29.12      by auto
   29.13 -  hence U3: "(UNION {(p,n,s). (p,n,s) \<in> ?SS a \<and> n<0} (\<lambda> (p,n,s). set (?ff (p,n,s)))) =
   29.14 -    (UNION {(p,n,s). (p,n,s)\<in> ?SS a\<and>n<0} (\<lambda>(p,n,s). set (map (?f(p,n,s)) [n..0])))"
   29.15 -      proof-
   29.16 +  hence U3: "(\<Union> ((\<lambda>(p,n,s). set (?ff (p,n,s))) ` {(p,n,s). (p,n,s) \<in> ?SS a \<and> n<0})) =
   29.17 +    (\<Union> ((\<lambda>(p,n,s). set (map (?f(p,n,s)) [n..0])) ` {(p,n,s). (p,n,s)\<in> ?SS a\<and>n<0}))"
   29.18 +  proof -
   29.19      fix M :: "('a\<times>'b\<times>'c) set" and f :: "('a\<times>'b\<times>'c) \<Rightarrow> 'd list" and g
   29.20      assume "\<forall> (a,b,c) \<in> M. f (a,b,c) = g a b c"
   29.21 -    thus "(UNION M (\<lambda> (a,b,c). set (f (a,b,c)))) = (UNION M (\<lambda> (a,b,c). set (g a b c)))"
   29.22 +    thus "(\<Union>(a, b, c)\<in>M. set (f (a, b, c))) = (\<Union>(a, b, c)\<in>M. set (g a b c))"
   29.23        by (auto simp add: split_def)
   29.24    qed
   29.25 -  have "?SS (Floor a) = UNION (?SS a) (\<lambda>x. set (?ff x))"
   29.26 +  have "?SS (Floor a) = \<Union> ((\<lambda>x. set (?ff x)) ` ?SS a)"
   29.27      by auto
   29.28 -  also have "\<dots> = UNION (?SS a) (\<lambda> (p,n,s). set (?ff (p,n,s)))" by blast
   29.29 +  also have "\<dots> = \<Union> ((\<lambda> (p,n,s). set (?ff (p,n,s))) ` ?SS a)"
   29.30 +    by blast
   29.31    also have "\<dots> =
   29.32      ((UNION {(p,n,s). (p,n,s) \<in> ?SS a \<and> n=0} (\<lambda> (p,n,s). set (?ff (p,n,s)))) Un
   29.33      (UNION {(p,n,s). (p,n,s) \<in> ?SS a \<and> n>0} (\<lambda> (p,n,s). set (?ff (p,n,s)))) Un
   29.34 @@ -3535,7 +3536,7 @@
   29.35    proof-
   29.36      fix M :: "('a\<times>'b\<times>'c) set" and f :: "('a\<times>'b\<times>'c) \<Rightarrow> 'd list" and g
   29.37      assume "\<forall> (a,b,c) \<in> M. f (a,b,c) = g a b c"
   29.38 -    thus "(UNION M (\<lambda> (a,b,c). set (f (a,b,c)))) = (UNION M (\<lambda> (a,b,c). set (g a b c)))"
   29.39 +    thus "(\<Union>(a, b, c)\<in>M. set (f (a, b, c))) = (\<Union>(a, b, c)\<in>M. set (g a b c))"
   29.40        by (auto simp add: split_def)
   29.41    qed
   29.42    have U3': "\<forall> (p,n,s) \<in> {(p,n,s). (p,n,s) \<in> ?SS a \<and> n<0}. ?ff (p,n,s) = map (?f(p,n,s)) [n..0]"
   29.43 @@ -3544,12 +3545,12 @@
   29.44    proof-
   29.45      fix M :: "('a\<times>'b\<times>'c) set" and f :: "('a\<times>'b\<times>'c) \<Rightarrow> 'd list" and g
   29.46      assume "\<forall> (a,b,c) \<in> M. f (a,b,c) = g a b c"
   29.47 -    thus "(UNION M (\<lambda> (a,b,c). set (f (a,b,c)))) = (UNION M (\<lambda> (a,b,c). set (g a b c)))"
   29.48 +    thus "(\<Union>(a, b, c)\<in>M. set (f (a, b, c))) = (\<Union>(a, b, c)\<in>M. set (g a b c))"
   29.49        by (auto simp add: split_def)
   29.50    qed
   29.51  
   29.52 -  have "?SS (Floor a) = UNION (?SS a) (\<lambda>x. set (?ff x))" by auto
   29.53 -  also have "\<dots> = UNION (?SS a) (\<lambda> (p,n,s). set (?ff (p,n,s)))" by blast
   29.54 +  have "?SS (Floor a) = \<Union> ((\<lambda>x. set (?ff x)) ` ?SS a)" by auto
   29.55 +  also have "\<dots> = \<Union> ((\<lambda> (p,n,s). set (?ff (p,n,s))) ` ?SS a)" by blast
   29.56    also have "\<dots> =
   29.57      ((UNION {(p,n,s). (p,n,s) \<in> ?SS a \<and> n=0} (\<lambda> (p,n,s). set (?ff (p,n,s)))) Un
   29.58      (UNION {(p,n,s). (p,n,s) \<in> ?SS a \<and> n>0} (\<lambda> (p,n,s). set (?ff (p,n,s)))) Un
    30.1 --- a/src/HOL/Hoare_Parallel/RG_Hoare.thy	Sun Nov 18 09:51:41 2018 +0100
    30.2 +++ b/src/HOL/Hoare_Parallel/RG_Hoare.thy	Sun Nov 18 18:07:51 2018 +0000
    30.3 @@ -1134,7 +1134,7 @@
    30.4   apply(drule_tac c="s" in subsetD,simp)
    30.5   apply simp
    30.6  apply clarify
    30.7 -apply(erule_tac x=i and P="\<lambda>j. H j \<longrightarrow> M \<union> UNION (S j) (T j) \<subseteq> (L j)" for H M S T L in allE)
    30.8 +apply(erule_tac x=i and P="\<lambda>j. H j \<longrightarrow> M \<union> \<Union>((T j) ` (S j)) \<subseteq> (L j)" for H M S T L in allE)
    30.9  apply simp
   30.10  apply(erule subsetD)
   30.11  apply simp
    31.1 --- a/src/HOL/Library/Countable_Complete_Lattices.thy	Sun Nov 18 09:51:41 2018 +0100
    31.2 +++ b/src/HOL/Library/Countable_Complete_Lattices.thy	Sun Nov 18 18:07:51 2018 +0000
    31.3 @@ -66,13 +66,13 @@
    31.4  lemma ccInf_insert [simp]: "countable A \<Longrightarrow> Inf (insert a A) = inf a (Inf A)"
    31.5    by (force intro: le_infI le_infI1 le_infI2 antisym ccInf_greatest ccInf_lower)
    31.6  
    31.7 -lemma ccINF_insert [simp]: "countable A \<Longrightarrow> (INF x\<in>insert a A. f x) = inf (f a) (INFIMUM A f)"
    31.8 +lemma ccINF_insert [simp]: "countable A \<Longrightarrow> (INF x\<in>insert a A. f x) = inf (f a) (Inf (f ` A))"
    31.9    unfolding image_insert by simp
   31.10  
   31.11  lemma ccSup_insert [simp]: "countable A \<Longrightarrow> Sup (insert a A) = sup a (Sup A)"
   31.12    by (force intro: le_supI le_supI1 le_supI2 antisym ccSup_least ccSup_upper)
   31.13  
   31.14 -lemma ccSUP_insert [simp]: "countable A \<Longrightarrow> (SUP x\<in>insert a A. f x) = sup (f a) (SUPREMUM A f)"
   31.15 +lemma ccSUP_insert [simp]: "countable A \<Longrightarrow> (SUP x\<in>insert a A. f x) = sup (f a) (Sup (f ` A))"
   31.16    unfolding image_insert by simp
   31.17  
   31.18  lemma ccINF_empty [simp]: "(INF x\<in>{}. f x) = top"
    32.1 --- a/src/HOL/Library/Countable_Set_Type.thy	Sun Nov 18 09:51:41 2018 +0100
    32.2 +++ b/src/HOL/Library/Countable_Set_Type.thy	Sun Nov 18 18:07:51 2018 +0000
    32.3 @@ -117,13 +117,13 @@
    32.4    is "UNION" parametric UNION_transfer by simp
    32.5  definition cUnion :: "'a cset cset \<Rightarrow> 'a cset" where "cUnion A = cUNION A id"
    32.6  
    32.7 -lemma Union_conv_UNION: "\<Union>A = UNION A id"
    32.8 +lemma Union_conv_UNION: "\<Union>A = \<Union>(id ` A)"
    32.9  by auto
   32.10  
   32.11  lemma cUnion_transfer [transfer_rule]:
   32.12    "rel_fun (pcr_cset (pcr_cset A)) (pcr_cset A) Union cUnion"
   32.13  proof -
   32.14 -  have "rel_fun (pcr_cset (pcr_cset A)) (pcr_cset A) (\<lambda>A. UNION A id) (\<lambda>A. cUNION A id)"
   32.15 +  have "rel_fun (pcr_cset (pcr_cset A)) (pcr_cset A) (\<lambda>A. \<Union>(id ` A)) (\<lambda>A. cUNION A id)"
   32.16      by transfer_prover
   32.17    then show ?thesis by (simp flip: cUnion_def)
   32.18  qed
    33.1 --- a/src/HOL/Library/Disjoint_Sets.thy	Sun Nov 18 09:51:41 2018 +0100
    33.2 +++ b/src/HOL/Library/Disjoint_Sets.thy	Sun Nov 18 18:07:51 2018 +0000
    33.3 @@ -158,9 +158,9 @@
    33.4    shows   "bij_betw f (\<Union>i\<in>I. A i) (\<Union>i\<in>I. A' i)"
    33.5  unfolding bij_betw_def
    33.6  proof
    33.7 -  from bij show eq: "f ` UNION I A = UNION I A'"
    33.8 +  from bij show eq: "f ` \<Union>(A ` I) = \<Union>(A' ` I)"
    33.9      by (auto simp: bij_betw_def image_UN)
   33.10 -  show "inj_on f (UNION I A)"
   33.11 +  show "inj_on f (\<Union>(A ` I))"
   33.12    proof (rule inj_onI, clarify)
   33.13      fix i j x y assume A: "i \<in> I" "j \<in> I" "x \<in> A i" "y \<in> A j" and B: "f x = f y"
   33.14      from A bij[of i] bij[of j] have "f x \<in> A' i" "f y \<in> A' j"
   33.15 @@ -179,7 +179,7 @@
   33.16  \<close>
   33.17  lemma infinite_disjoint_family_imp_infinite_UNION:
   33.18    assumes "\<not>finite A" "\<And>x. x \<in> A \<Longrightarrow> f x \<noteq> {}" "disjoint_family_on f A"
   33.19 -  shows   "\<not>finite (UNION A f)"
   33.20 +  shows   "\<not>finite (\<Union>(f ` A))"
   33.21  proof -
   33.22    define g where "g x = (SOME y. y \<in> f x)" for x
   33.23    have g: "g x \<in> f x" if "x \<in> A" for x
   33.24 @@ -191,7 +191,7 @@
   33.25      with A \<open>x \<noteq> y\<close> assms show False
   33.26        by (auto simp: disjoint_family_on_def inj_on_def)
   33.27    qed
   33.28 -  from g have "g ` A \<subseteq> UNION A f" by blast
   33.29 +  from g have "g ` A \<subseteq> \<Union>(f ` A)" by blast
   33.30    moreover from inj_on_g \<open>\<not>finite A\<close> have "\<not>finite (g ` A)"
   33.31      using finite_imageD by blast
   33.32    ultimately show ?thesis using finite_subset by blast
    34.1 --- a/src/HOL/Library/Extended_Nonnegative_Real.thy	Sun Nov 18 09:51:41 2018 +0100
    34.2 +++ b/src/HOL/Library/Extended_Nonnegative_Real.thy	Sun Nov 18 18:07:51 2018 +0000
    34.3 @@ -1501,7 +1501,7 @@
    34.4  
    34.5  lemma ennreal_SUP_add:
    34.6    fixes f g :: "nat \<Rightarrow> ennreal"
    34.7 -  shows "incseq f \<Longrightarrow> incseq g \<Longrightarrow> (SUP i. f i + g i) = SUPREMUM UNIV f + SUPREMUM UNIV g"
    34.8 +  shows "incseq f \<Longrightarrow> incseq g \<Longrightarrow> (SUP i. f i + g i) = Sup (f ` UNIV) + Sup (g ` UNIV)"
    34.9    unfolding incseq_def le_fun_def
   34.10    by transfer
   34.11       (simp add: SUP_ereal_add incseq_def le_fun_def max_absorb2 SUP_upper2)
   34.12 @@ -1591,7 +1591,7 @@
   34.13    done
   34.14  
   34.15  lemma ennreal_SUP_countable_SUP:
   34.16 -  "A \<noteq> {} \<Longrightarrow> \<exists>f::nat \<Rightarrow> ennreal. range f \<subseteq> g`A \<and> SUPREMUM A g = SUPREMUM UNIV f"
   34.17 +  "A \<noteq> {} \<Longrightarrow> \<exists>f::nat \<Rightarrow> ennreal. range f \<subseteq> g`A \<and> Sup (g ` A) = Sup (f ` UNIV)"
   34.18    using ennreal_Sup_countable_SUP [of "g`A"] by auto
   34.19  
   34.20  lemma of_nat_tendsto_top_ennreal: "(\<lambda>n::nat. of_nat n :: ennreal) \<longlonglongrightarrow> top"
    35.1 --- a/src/HOL/Library/Extended_Real.thy	Sun Nov 18 09:51:41 2018 +0100
    35.2 +++ b/src/HOL/Library/Extended_Real.thy	Sun Nov 18 18:07:51 2018 +0000
    35.3 @@ -2215,15 +2215,15 @@
    35.4  
    35.5  lemma ereal_SUP_not_infty:
    35.6    fixes f :: "_ \<Rightarrow> ereal"
    35.7 -  shows "A \<noteq> {} \<Longrightarrow> l \<noteq> -\<infinity> \<Longrightarrow> u \<noteq> \<infinity> \<Longrightarrow> \<forall>a\<in>A. l \<le> f a \<and> f a \<le> u \<Longrightarrow> \<bar>SUPREMUM A f\<bar> \<noteq> \<infinity>"
    35.8 +  shows "A \<noteq> {} \<Longrightarrow> l \<noteq> -\<infinity> \<Longrightarrow> u \<noteq> \<infinity> \<Longrightarrow> \<forall>a\<in>A. l \<le> f a \<and> f a \<le> u \<Longrightarrow> \<bar>Sup (f ` A)\<bar> \<noteq> \<infinity>"
    35.9    using SUP_upper2[of _ A l f] SUP_least[of A f u]
   35.10 -  by (cases "SUPREMUM A f") auto
   35.11 +  by (cases "Sup (f ` A)") auto
   35.12  
   35.13  lemma ereal_INF_not_infty:
   35.14    fixes f :: "_ \<Rightarrow> ereal"
   35.15 -  shows "A \<noteq> {} \<Longrightarrow> l \<noteq> -\<infinity> \<Longrightarrow> u \<noteq> \<infinity> \<Longrightarrow> \<forall>a\<in>A. l \<le> f a \<and> f a \<le> u \<Longrightarrow> \<bar>INFIMUM A f\<bar> \<noteq> \<infinity>"
   35.16 +  shows "A \<noteq> {} \<Longrightarrow> l \<noteq> -\<infinity> \<Longrightarrow> u \<noteq> \<infinity> \<Longrightarrow> \<forall>a\<in>A. l \<le> f a \<and> f a \<le> u \<Longrightarrow> \<bar>Inf (f ` A)\<bar> \<noteq> \<infinity>"
   35.17    using INF_lower2[of _ A f u] INF_greatest[of A l f]
   35.18 -  by (cases "INFIMUM A f") auto
   35.19 +  by (cases "Inf (f ` A)") auto
   35.20  
   35.21  lemma ereal_image_uminus_shift:
   35.22    fixes X Y :: "ereal set"
   35.23 @@ -2332,7 +2332,7 @@
   35.24  lemma SUP_ereal_le_addI:
   35.25    fixes f :: "'i \<Rightarrow> ereal"
   35.26    assumes "\<And>i. f i + y \<le> z" and "y \<noteq> -\<infinity>"
   35.27 -  shows "SUPREMUM UNIV f + y \<le> z"
   35.28 +  shows "Sup (f ` UNIV) + y \<le> z"
   35.29    unfolding SUP_ereal_add_left[OF UNIV_not_empty \<open>y \<noteq> -\<infinity>\<close>, symmetric]
   35.30    by (rule SUP_least assms)+
   35.31  
   35.32 @@ -2351,7 +2351,7 @@
   35.33    fixes f g :: "nat \<Rightarrow> ereal"
   35.34    assumes inc: "incseq f" "incseq g"
   35.35      and pos: "\<And>i. f i \<noteq> -\<infinity>" "\<And>i. g i \<noteq> -\<infinity>"
   35.36 -  shows "(SUP i. f i + g i) = SUPREMUM UNIV f + SUPREMUM UNIV g"
   35.37 +  shows "(SUP i. f i + g i) = Sup (f ` UNIV) + Sup (g ` UNIV)"
   35.38    apply (subst SUP_ereal_add_left[symmetric, OF UNIV_not_empty])
   35.39    apply (metis SUP_upper UNIV_I assms(4) ereal_infty_less_eq(2))
   35.40    apply (subst (2) add.commute)
   35.41 @@ -2408,7 +2408,7 @@
   35.42    fixes f :: "nat \<Rightarrow> ereal"
   35.43    assumes "decseq f" "decseq g"
   35.44      and fin: "\<And>i. f i \<noteq> \<infinity>" "\<And>i. g i \<noteq> \<infinity>"
   35.45 -  shows "(INF i. f i + g i) = INFIMUM UNIV f + INFIMUM UNIV g"
   35.46 +  shows "(INF i. f i + g i) = Inf (f ` UNIV) + Inf (g ` UNIV)"
   35.47  proof -
   35.48    have INF_less: "(INF i. f i) < \<infinity>" "(INF i. g i) < \<infinity>"
   35.49      using assms unfolding INF_less_iff by auto
   35.50 @@ -2418,7 +2418,7 @@
   35.51    note * = this
   35.52    have "(INF i. f i + g i) = (INF i. - ((- f i) + (- g i)))"
   35.53      by (simp add: fin *)
   35.54 -  also have "\<dots> = INFIMUM UNIV f + INFIMUM UNIV g"
   35.55 +  also have "\<dots> = Inf (f ` UNIV) + Inf (g ` UNIV)"
   35.56      unfolding ereal_INF_uminus_eq
   35.57      using assms INF_less
   35.58      by (subst SUP_ereal_add) (auto simp: ereal_SUP_uminus fin *)
   35.59 @@ -2429,7 +2429,7 @@
   35.60    fixes f g :: "nat \<Rightarrow> ereal"
   35.61    assumes inc: "incseq f" "incseq g"
   35.62      and pos: "\<And>i. 0 \<le> f i" "\<And>i. 0 \<le> g i"
   35.63 -  shows "(SUP i. f i + g i) = SUPREMUM UNIV f + SUPREMUM UNIV g"
   35.64 +  shows "(SUP i. f i + g i) = Sup (f ` UNIV) + Sup (g ` UNIV)"
   35.65  proof (intro SUP_ereal_add inc)
   35.66    fix i
   35.67    show "f i \<noteq> -\<infinity>" "g i \<noteq> -\<infinity>"
   35.68 @@ -2440,7 +2440,7 @@
   35.69    fixes f g :: "'a \<Rightarrow> nat \<Rightarrow> ereal"
   35.70    assumes "\<And>n. n \<in> A \<Longrightarrow> incseq (f n)"
   35.71      and pos: "\<And>n i. n \<in> A \<Longrightarrow> 0 \<le> f n i"
   35.72 -  shows "(SUP i. \<Sum>n\<in>A. f n i) = (\<Sum>n\<in>A. SUPREMUM UNIV (f n))"
   35.73 +  shows "(SUP i. \<Sum>n\<in>A. f n i) = (\<Sum>n\<in>A. Sup ((f n) ` UNIV))"
   35.74  proof (cases "finite A")
   35.75    case True
   35.76    then show ?thesis using assms
   35.77 @@ -2537,7 +2537,7 @@
   35.78  qed
   35.79  
   35.80  lemma SUP_countable_SUP:
   35.81 -  "A \<noteq> {} \<Longrightarrow> \<exists>f::nat \<Rightarrow> ereal. range f \<subseteq> g`A \<and> SUPREMUM A g = SUPREMUM UNIV f"
   35.82 +  "A \<noteq> {} \<Longrightarrow> \<exists>f::nat \<Rightarrow> ereal. range f \<subseteq> g`A \<and> Sup (g ` A) = Sup (f ` UNIV)"
   35.83    using Sup_countable_SUP [of "g`A"] by auto
   35.84  
   35.85  subsection "Relation to @{typ enat}"
   35.86 @@ -3222,7 +3222,7 @@
   35.87    unfolding Liminf_def
   35.88  proof (subst SUP_ereal_add_left[symmetric])
   35.89    let ?F = "{P. eventually P F}"
   35.90 -  let ?INF = "\<lambda>P g. INFIMUM (Collect P) g"
   35.91 +  let ?INF = "\<lambda>P g. Inf (g ` (Collect P))"
   35.92    show "?F \<noteq> {}"
   35.93      by (auto intro: eventually_True)
   35.94    show "(SUP P\<in>?F. ?INF P g) \<noteq> - \<infinity>"
   35.95 @@ -3238,7 +3238,7 @@
   35.96        by (intro add_mono INF_mono) auto
   35.97      also have "\<dots> = (SUP P'\<in>?F. ?INF ?P' f + ?INF P' g)"
   35.98      proof (rule SUP_ereal_add_right[symmetric])
   35.99 -      show "INFIMUM {x. P x \<and> 0 \<le> f x} f \<noteq> - \<infinity>"
  35.100 +      show "Inf (f ` {x. P x \<and> 0 \<le> f x}) \<noteq> - \<infinity>"
  35.101          unfolding bot_ereal_def[symmetric] INF_eq_bot_iff
  35.102          by (auto intro!: exI[of _ 0] ev simp: bot_ereal_def)
  35.103      qed fact
    36.1 --- a/src/HOL/Library/Finite_Map.thy	Sun Nov 18 09:51:41 2018 +0100
    36.2 +++ b/src/HOL/Library/Finite_Map.thy	Sun Nov 18 18:07:51 2018 +0000
    36.3 @@ -818,7 +818,7 @@
    36.4    by (rule rel_funI ext)+ (auto simp: fmap.Abs_fmap_inverse fmap.pcr_cr_eq cr_fmap_def)
    36.5  
    36.6  lemma fmran'_transfer[transfer_rule]:
    36.7 -  "(pcr_fmap (=) (=) ===> (=)) (\<lambda>x. UNION (range x) set_option) fmran'"
    36.8 +  "(pcr_fmap (=) (=) ===> (=)) (\<lambda>x. \<Union>(set_option ` (range x))) fmran'"
    36.9    unfolding fmran'_def fmap.pcr_cr_eq cr_fmap_def by fastforce
   36.10  
   36.11  lemma fmrel_transfer[transfer_rule]:
    37.1 --- a/src/HOL/Library/Indicator_Function.thy	Sun Nov 18 09:51:41 2018 +0100
    37.2 +++ b/src/HOL/Library/Indicator_Function.thy	Sun Nov 18 18:07:51 2018 +0000
    37.3 @@ -191,7 +191,7 @@
    37.4  \<close>
    37.5  
    37.6  lemma indicator_UN_disjoint:
    37.7 -  "finite A \<Longrightarrow> disjoint_family_on f A \<Longrightarrow> indicator (UNION A f) x = (\<Sum>y\<in>A. indicator (f y) x)"
    37.8 +  "finite A \<Longrightarrow> disjoint_family_on f A \<Longrightarrow> indicator (\<Union>(f ` A)) x = (\<Sum>y\<in>A. indicator (f y) x)"
    37.9    by (induct A rule: finite_induct)
   37.10      (auto simp: disjoint_family_on_def indicator_def split: if_splits)
   37.11  
    38.1 --- a/src/HOL/Library/Liminf_Limsup.thy	Sun Nov 18 09:51:41 2018 +0100
    38.2 +++ b/src/HOL/Library/Liminf_Limsup.thy	Sun Nov 18 18:07:51 2018 +0000
    38.3 @@ -20,7 +20,7 @@
    38.4  qed (auto elim!: allE[of _ "Sup A"] simp add: not_le[symmetric] cSup_upper assms)
    38.5  
    38.6  lemma (in conditionally_complete_linorder) le_cSUP_iff:
    38.7 -  "A \<noteq> {} \<Longrightarrow> bdd_above (f`A) \<Longrightarrow> x \<le> SUPREMUM A f \<longleftrightarrow> (\<forall>y<x. \<exists>i\<in>A. y < f i)"
    38.8 +  "A \<noteq> {} \<Longrightarrow> bdd_above (f`A) \<Longrightarrow> x \<le> Sup (f ` A) \<longleftrightarrow> (\<forall>y<x. \<exists>i\<in>A. y < f i)"
    38.9    using le_cSup_iff [of "f ` A"] by simp
   38.10  
   38.11  lemma le_cSup_iff_less:
   38.12 @@ -46,7 +46,7 @@
   38.13  qed (auto elim!: allE[of _ "Inf A"] simp add: not_le[symmetric] cInf_lower assms)
   38.14  
   38.15  lemma (in conditionally_complete_linorder) cINF_le_iff:
   38.16 -  "A \<noteq> {} \<Longrightarrow> bdd_below (f`A) \<Longrightarrow> INFIMUM A f \<le> x \<longleftrightarrow> (\<forall>y>x. \<exists>i\<in>A. y > f i)"
   38.17 +  "A \<noteq> {} \<Longrightarrow> bdd_below (f`A) \<Longrightarrow> Inf (f ` A) \<le> x \<longleftrightarrow> (\<forall>y>x. \<exists>i\<in>A. y > f i)"
   38.18    using cInf_le_iff [of "f ` A"] by simp
   38.19  
   38.20  lemma cInf_le_iff_less:
   38.21 @@ -89,13 +89,13 @@
   38.22  abbreviation "limsup \<equiv> Limsup sequentially"
   38.23  
   38.24  lemma Liminf_eqI:
   38.25 -  "(\<And>P. eventually P F \<Longrightarrow> INFIMUM (Collect P) f \<le> x) \<Longrightarrow>
   38.26 -    (\<And>y. (\<And>P. eventually P F \<Longrightarrow> INFIMUM (Collect P) f \<le> y) \<Longrightarrow> x \<le> y) \<Longrightarrow> Liminf F f = x"
   38.27 +  "(\<And>P. eventually P F \<Longrightarrow> Inf (f ` (Collect P)) \<le> x) \<Longrightarrow>
   38.28 +    (\<And>y. (\<And>P. eventually P F \<Longrightarrow> Inf (f ` (Collect P)) \<le> y) \<Longrightarrow> x \<le> y) \<Longrightarrow> Liminf F f = x"
   38.29    unfolding Liminf_def by (auto intro!: SUP_eqI)
   38.30  
   38.31  lemma Limsup_eqI:
   38.32 -  "(\<And>P. eventually P F \<Longrightarrow> x \<le> SUPREMUM (Collect P) f) \<Longrightarrow>
   38.33 -    (\<And>y. (\<And>P. eventually P F \<Longrightarrow> y \<le> SUPREMUM (Collect P) f) \<Longrightarrow> y \<le> x) \<Longrightarrow> Limsup F f = x"
   38.34 +  "(\<And>P. eventually P F \<Longrightarrow> x \<le> Sup (f ` (Collect P))) \<Longrightarrow>
   38.35 +    (\<And>y. (\<And>P. eventually P F \<Longrightarrow> y \<le> Sup (f ` (Collect P))) \<Longrightarrow> y \<le> x) \<Longrightarrow> Limsup F f = x"
   38.36    unfolding Limsup_def by (auto intro!: INF_eqI)
   38.37  
   38.38  lemma liminf_SUP_INF: "liminf f = (SUP n. INF m\<in>{n..}. f m)"
   38.39 @@ -139,7 +139,7 @@
   38.40  proof (safe intro!: SUP_mono)
   38.41    fix P assume "eventually P F"
   38.42    with ev have "eventually (\<lambda>x. f x \<le> g x \<and> P x) F" (is "eventually ?Q F") by (rule eventually_conj)
   38.43 -  then show "\<exists>Q\<in>{P. eventually P F}. INFIMUM (Collect P) f \<le> INFIMUM (Collect Q) g"
   38.44 +  then show "\<exists>Q\<in>{P. eventually P F}. Inf (f ` (Collect P)) \<le> Inf (g ` (Collect Q))"
   38.45      by (intro bexI[of _ ?Q]) (auto intro!: INF_mono)
   38.46  qed
   38.47  
   38.48 @@ -155,7 +155,7 @@
   38.49  proof (safe intro!: INF_mono)
   38.50    fix P assume "eventually P F"
   38.51    with ev have "eventually (\<lambda>x. f x \<le> g x \<and> P x) F" (is "eventually ?Q F") by (rule eventually_conj)
   38.52 -  then show "\<exists>Q\<in>{P. eventually P F}. SUPREMUM (Collect Q) f \<le> SUPREMUM (Collect P) g"
   38.53 +  then show "\<exists>Q\<in>{P. eventually P F}. Sup (f ` (Collect Q)) \<le> Sup (g ` (Collect P))"
   38.54      by (intro bexI[of _ ?Q]) (auto intro!: SUP_mono)
   38.55  qed
   38.56  
   38.57 @@ -183,13 +183,13 @@
   38.58    then have "eventually (\<lambda>x. P x \<and> Q x) F" (is "eventually ?C F") by (rule eventually_conj)
   38.59    then have not_False: "(\<lambda>x. P x \<and> Q x) \<noteq> (\<lambda>x. False)"
   38.60      using ntriv by (auto simp add: eventually_False)
   38.61 -  have "INFIMUM (Collect P) f \<le> INFIMUM (Collect ?C) f"
   38.62 +  have "Inf (f ` (Collect P)) \<le> Inf (f ` (Collect ?C))"
   38.63      by (rule INF_mono) auto
   38.64 -  also have "\<dots> \<le> SUPREMUM (Collect ?C) f"
   38.65 +  also have "\<dots> \<le> Sup (f ` (Collect ?C))"
   38.66      using not_False by (intro INF_le_SUP) auto
   38.67 -  also have "\<dots> \<le> SUPREMUM (Collect Q) f"
   38.68 +  also have "\<dots> \<le> Sup (f ` (Collect Q))"
   38.69      by (rule SUP_mono) auto
   38.70 -  finally show "INFIMUM (Collect P) f \<le> SUPREMUM (Collect Q) f" .
   38.71 +  finally show "Inf (f ` (Collect P)) \<le> Sup (f ` (Collect Q))" .
   38.72  qed
   38.73  
   38.74  lemma Liminf_bounded:
   38.75 @@ -219,21 +219,21 @@
   38.76    shows "C \<le> Liminf F X \<longleftrightarrow> (\<forall>y<C. eventually (\<lambda>x. y < X x) F)"
   38.77  proof -
   38.78    have "eventually (\<lambda>x. y < X x) F"
   38.79 -    if "eventually P F" "y < INFIMUM (Collect P) X" for y P
   38.80 +    if "eventually P F" "y < Inf (X ` (Collect P))" for y P
   38.81      using that by (auto elim!: eventually_mono dest: less_INF_D)
   38.82    moreover
   38.83 -  have "\<exists>P. eventually P F \<and> y < INFIMUM (Collect P) X"
   38.84 +  have "\<exists>P. eventually P F \<and> y < Inf (X ` (Collect P))"
   38.85      if "y < C" and y: "\<forall>y<C. eventually (\<lambda>x. y < X x) F" for y P
   38.86    proof (cases "\<exists>z. y < z \<and> z < C")
   38.87      case True
   38.88      then obtain z where z: "y < z \<and> z < C" ..
   38.89 -    moreover from z have "z \<le> INFIMUM {x. z < X x} X"
   38.90 +    moreover from z have "z \<le> Inf (X ` {x. z < X x})"
   38.91        by (auto intro!: INF_greatest)
   38.92      ultimately show ?thesis
   38.93        using y by (intro exI[of _ "\<lambda>x. z < X x"]) auto
   38.94    next
   38.95      case False
   38.96 -    then have "C \<le> INFIMUM {x. y < X x} X"
   38.97 +    then have "C \<le> Inf (X ` {x. y < X x})"
   38.98        by (intro INF_greatest) auto
   38.99      with \<open>y < C\<close> show ?thesis
  38.100        using y by (intro exI[of _ "\<lambda>x. y < X x"]) auto
  38.101 @@ -246,22 +246,22 @@
  38.102    fixes X :: "_ \<Rightarrow> _ :: complete_linorder"
  38.103    shows "C \<ge> Limsup F X \<longleftrightarrow> (\<forall>y>C. eventually (\<lambda>x. y > X x) F)"
  38.104  proof -
  38.105 -  { fix y P assume "eventually P F" "y > SUPREMUM (Collect P) X"
  38.106 +  { fix y P assume "eventually P F" "y > Sup (X ` (Collect P))"
  38.107      then have "eventually (\<lambda>x. y > X x) F"
  38.108        by (auto elim!: eventually_mono dest: SUP_lessD) }
  38.109    moreover
  38.110    { fix y P assume "y > C" and y: "\<forall>y>C. eventually (\<lambda>x. y > X x) F"
  38.111 -    have "\<exists>P. eventually P F \<and> y > SUPREMUM (Collect P) X"
  38.112 +    have "\<exists>P. eventually P F \<and> y > Sup (X ` (Collect P))"
  38.113      proof (cases "\<exists>z. C < z \<and> z < y")
  38.114        case True
  38.115        then obtain z where z: "C < z \<and> z < y" ..
  38.116 -      moreover from z have "z \<ge> SUPREMUM {x. z > X x} X"
  38.117 +      moreover from z have "z \<ge> Sup (X ` {x. X x < z})"
  38.118          by (auto intro!: SUP_least)
  38.119        ultimately show ?thesis
  38.120          using y by (intro exI[of _ "\<lambda>x. z > X x"]) auto
  38.121      next
  38.122        case False
  38.123 -      then have "C \<ge> SUPREMUM {x. y > X x} X"
  38.124 +      then have "C \<ge> Sup (X ` {x. X x < y})"
  38.125          by (intro SUP_least) (auto simp: not_less)
  38.126        with \<open>y > C\<close> show ?thesis
  38.127          using y by (intro exI[of _ "\<lambda>x. y > X x"]) auto
  38.128 @@ -285,17 +285,17 @@
  38.129    shows "Liminf F f = f0"
  38.130  proof (intro Liminf_eqI)
  38.131    fix P assume P: "eventually P F"
  38.132 -  then have "eventually (\<lambda>x. INFIMUM (Collect P) f \<le> f x) F"
  38.133 +  then have "eventually (\<lambda>x. Inf (f ` (Collect P)) \<le> f x) F"
  38.134      by eventually_elim (auto intro!: INF_lower)
  38.135 -  then show "INFIMUM (Collect P) f \<le> f0"
  38.136 +  then show "Inf (f ` (Collect P)) \<le> f0"
  38.137      by (rule tendsto_le[OF ntriv lim tendsto_const])
  38.138  next
  38.139 -  fix y assume upper: "\<And>P. eventually P F \<Longrightarrow> INFIMUM (Collect P) f \<le> y"
  38.140 +  fix y assume upper: "\<And>P. eventually P F \<Longrightarrow> Inf (f ` (Collect P)) \<le> y"
  38.141    show "f0 \<le> y"
  38.142    proof cases
  38.143      assume "\<exists>z. y < z \<and> z < f0"
  38.144      then obtain z where "y < z \<and> z < f0" ..
  38.145 -    moreover have "z \<le> INFIMUM {x. z < f x} f"
  38.146 +    moreover have "z \<le> Inf (f ` {x. z < f x})"
  38.147        by (rule INF_greatest) simp
  38.148      ultimately show ?thesis
  38.149        using lim[THEN topological_tendstoD, THEN upper, of "{z <..}"] by auto
  38.150 @@ -308,9 +308,9 @@
  38.151          using lim[THEN topological_tendstoD, of "{y <..}"] by auto
  38.152        then have "eventually (\<lambda>x. f0 \<le> f x) F"
  38.153          using discrete by (auto elim!: eventually_mono)
  38.154 -      then have "INFIMUM {x. f0 \<le> f x} f \<le> y"
  38.155 +      then have "Inf (f ` {x. f0 \<le> f x}) \<le> y"
  38.156          by (rule upper)
  38.157 -      moreover have "f0 \<le> INFIMUM {x. f0 \<le> f x} f"
  38.158 +      moreover have "f0 \<le> Inf (f ` {x. f0 \<le> f x})"
  38.159          by (intro INF_greatest) simp
  38.160        ultimately show "f0 \<le> y" by simp
  38.161      qed
  38.162 @@ -324,17 +324,17 @@
  38.163    shows "Limsup F f = f0"
  38.164  proof (intro Limsup_eqI)
  38.165    fix P assume P: "eventually P F"
  38.166 -  then have "eventually (\<lambda>x. f x \<le> SUPREMUM (Collect P) f) F"
  38.167 +  then have "eventually (\<lambda>x. f x \<le> Sup (f ` (Collect P))) F"
  38.168      by eventually_elim (auto intro!: SUP_upper)
  38.169 -  then show "f0 \<le> SUPREMUM (Collect P) f"
  38.170 +  then show "f0 \<le> Sup (f ` (Collect P))"
  38.171      by (rule tendsto_le[OF ntriv tendsto_const lim])
  38.172  next
  38.173 -  fix y assume lower: "\<And>P. eventually P F \<Longrightarrow> y \<le> SUPREMUM (Collect P) f"
  38.174 +  fix y assume lower: "\<And>P. eventually P F \<Longrightarrow> y \<le> Sup (f ` (Collect P))"
  38.175    show "y \<le> f0"
  38.176    proof (cases "\<exists>z. f0 < z \<and> z < y")
  38.177      case True
  38.178      then obtain z where "f0 < z \<and> z < y" ..
  38.179 -    moreover have "SUPREMUM {x. f x < z} f \<le> z"
  38.180 +    moreover have "Sup (f ` {x. f x < z}) \<le> z"
  38.181        by (rule SUP_least) simp
  38.182      ultimately show ?thesis
  38.183        using lim[THEN topological_tendstoD, THEN lower, of "{..< z}"] by auto
  38.184 @@ -347,9 +347,9 @@
  38.185          using lim[THEN topological_tendstoD, of "{..< y}"] by auto
  38.186        then have "eventually (\<lambda>x. f x \<le> f0) F"
  38.187          using False by (auto elim!: eventually_mono simp: not_less)
  38.188 -      then have "y \<le> SUPREMUM {x. f x \<le> f0} f"
  38.189 +      then have "y \<le> Sup (f ` {x. f x \<le> f0})"
  38.190          by (rule lower)
  38.191 -      moreover have "SUPREMUM {x. f x \<le> f0} f \<le> f0"
  38.192 +      moreover have "Sup (f ` {x. f x \<le> f0}) \<le> f0"
  38.193          by (intro SUP_least) simp
  38.194        ultimately show "y \<le> f0" by simp
  38.195      qed
  38.196 @@ -364,14 +364,14 @@
  38.197  proof (rule order_tendstoI)
  38.198    fix a assume "f0 < a"
  38.199    with assms have "Limsup F f < a" by simp
  38.200 -  then obtain P where "eventually P F" "SUPREMUM (Collect P) f < a"
  38.201 +  then obtain P where "eventually P F" "Sup (f ` (Collect P)) < a"
  38.202      unfolding Limsup_def INF_less_iff by auto
  38.203    then show "eventually (\<lambda>x. f x < a) F"
  38.204      by (auto elim!: eventually_mono dest: SUP_lessD)
  38.205  next
  38.206    fix a assume "a < f0"
  38.207    with assms have "a < Liminf F f" by simp
  38.208 -  then obtain P where "eventually P F" "a < INFIMUM (Collect P) f"
  38.209 +  then obtain P where "eventually P F" "a < Inf (f ` (Collect P))"
  38.210      unfolding Liminf_def less_SUP_iff by auto
  38.211    then show "eventually (\<lambda>x. a < f x) F"
  38.212      by (auto elim!: eventually_mono dest: less_INF_D)
  38.213 @@ -435,7 +435,7 @@
  38.214      unfolding Liminf_def
  38.215      by (subst continuous_at_Sup_mono[OF am continuous_on_imp_continuous_within[OF c]])
  38.216         (auto intro: eventually_True)
  38.217 -  also have "\<dots> = (SUP P \<in> {P. eventually P F}. INFIMUM (g ` Collect P) f)"
  38.218 +  also have "\<dots> = (SUP P \<in> {P. eventually P F}. Inf (f ` (g ` Collect P)))"
  38.219      by (intro SUP_cong refl continuous_at_Inf_mono[OF am continuous_on_imp_continuous_within[OF c]])
  38.220         (auto dest!: eventually_happens simp: F)
  38.221    finally show ?thesis by (auto simp: Liminf_def)
  38.222 @@ -460,7 +460,7 @@
  38.223      unfolding Limsup_def
  38.224      by (subst continuous_at_Inf_mono[OF am continuous_on_imp_continuous_within[OF c]])
  38.225         (auto intro: eventually_True)
  38.226 -  also have "\<dots> = (INF P \<in> {P. eventually P F}. SUPREMUM (g ` Collect P) f)"
  38.227 +  also have "\<dots> = (INF P \<in> {P. eventually P F}. Sup (f ` (g ` Collect P)))"
  38.228      by (intro INF_cong refl continuous_at_Sup_mono[OF am continuous_on_imp_continuous_within[OF c]])
  38.229         (auto dest!: eventually_happens simp: F)
  38.230    finally show ?thesis by (auto simp: Limsup_def)
  38.231 @@ -484,7 +484,7 @@
  38.232      unfolding Limsup_def
  38.233      by (subst continuous_at_Inf_antimono[OF am continuous_on_imp_continuous_within[OF c]])
  38.234         (auto intro: eventually_True)
  38.235 -  also have "\<dots> = (SUP P \<in> {P. eventually P F}. INFIMUM (g ` Collect P) f)"
  38.236 +  also have "\<dots> = (SUP P \<in> {P. eventually P F}. Inf (f ` (g ` Collect P)))"
  38.237      by (intro SUP_cong refl continuous_at_Sup_antimono[OF am continuous_on_imp_continuous_within[OF c]])
  38.238         (auto dest!: eventually_happens simp: F)
  38.239    finally show ?thesis
  38.240 @@ -510,7 +510,7 @@
  38.241      unfolding Liminf_def
  38.242      by (subst continuous_at_Sup_antimono[OF am continuous_on_imp_continuous_within[OF c]])
  38.243         (auto intro: eventually_True)
  38.244 -  also have "\<dots> = (INF P \<in> {P. eventually P F}. SUPREMUM (g ` Collect P) f)"
  38.245 +  also have "\<dots> = (INF P \<in> {P. eventually P F}. Sup (f ` (g ` Collect P)))"
  38.246      by (intro INF_cong refl continuous_at_Inf_antimono[OF am continuous_on_imp_continuous_within[OF c]])
  38.247         (auto dest!: eventually_happens simp: F)
  38.248    finally show ?thesis
    39.1 --- a/src/HOL/Library/Option_ord.thy	Sun Nov 18 09:51:41 2018 +0100
    39.2 +++ b/src/HOL/Library/Option_ord.thy	Sun Nov 18 18:07:51 2018 +0000
    39.3 @@ -283,7 +283,8 @@
    39.4    "A \<noteq> {} \<Longrightarrow> Some (\<Squnion>x\<in>A. f x) = (\<Squnion>x\<in>A. Some (f x))"
    39.5    using Some_Sup [of "f ` A"] by (simp add: comp_def)
    39.6  
    39.7 -lemma option_Inf_Sup: "INFIMUM (A::('a::complete_distrib_lattice option) set set) Sup \<le> SUPREMUM {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y} Inf"
    39.8 +lemma option_Inf_Sup: "\<Sqinter>(Sup ` A) \<le> \<Squnion>(Inf ` {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y})"
    39.9 +  for A :: "('a::complete_distrib_lattice option) set set"
   39.10  proof (cases "{} \<in> A")
   39.11    case True
   39.12    then show ?thesis
   39.13 @@ -438,8 +439,8 @@
   39.14      also have "... = Some (\<Squnion>x\<in>{f ` {the ` (y - {None}) |y. y \<in> A} |f. \<forall>Y. (\<exists>y. Y = the ` (y - {None}) \<and> y \<in> A) \<longrightarrow> f Y \<in> Y}. \<Sqinter>x) "
   39.15        by (simp add: Inf_Sup)
   39.16    
   39.17 -    also have "... \<le> SUPREMUM {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y} Inf"
   39.18 -    proof (cases "SUPREMUM {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y} Inf")
   39.19 +    also have "... \<le> \<Squnion> (Inf ` {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y})"
   39.20 +    proof (cases "\<Squnion> (Inf ` {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y})")
   39.21        case None
   39.22        then show ?thesis by (simp add: less_eq_option_def)
   39.23      next
    40.1 --- a/src/HOL/Library/Order_Continuity.thy	Sun Nov 18 09:51:41 2018 +0100
    40.2 +++ b/src/HOL/Library/Order_Continuity.thy	Sun Nov 18 18:07:51 2018 +0000
    40.3 @@ -76,7 +76,7 @@
    40.4    assume M: "mono M"
    40.5    then have "mono (\<lambda>i. g (M i))"
    40.6      using sup_continuous_mono[OF g] by (auto simp: mono_def)
    40.7 -  with M show "f (g (SUPREMUM UNIV M)) = (SUP i. f (g (M i)))"
    40.8 +  with M show "f (g (Sup (M ` UNIV))) = (SUP i. f (g (M i)))"
    40.9      by (auto simp: sup_continuous_def g[THEN sup_continuousD] f[THEN sup_continuousD])
   40.10  qed
   40.11  
   40.12 @@ -274,7 +274,7 @@
   40.13    assume M: "antimono M"
   40.14    then have "antimono (\<lambda>i. g (M i))"
   40.15      using inf_continuous_mono[OF g] by (auto simp: mono_def antimono_def)
   40.16 -  with M show "f (g (INFIMUM UNIV M)) = (INF i. f (g (M i)))"
   40.17 +  with M show "f (g (Inf (M ` UNIV))) = (INF i. f (g (M i)))"
   40.18      by (auto simp: inf_continuous_def g[THEN inf_continuousD] f[THEN inf_continuousD])
   40.19  qed
   40.20  
    41.1 --- a/src/HOL/Library/Product_Order.thy	Sun Nov 18 09:51:41 2018 +0100
    41.2 +++ b/src/HOL/Library/Product_Order.thy	Sun Nov 18 18:07:51 2018 +0000
    41.3 @@ -220,11 +220,11 @@
    41.4  of two complete lattices:\<close>
    41.5  
    41.6  lemma INF_prod_alt_def:
    41.7 -  "INFIMUM A f = (INFIMUM A (fst \<circ> f), INFIMUM A (snd \<circ> f))"
    41.8 +  "Inf (f ` A) = (Inf ((fst \<circ> f) ` A), Inf ((snd \<circ> f) ` A))"
    41.9    unfolding Inf_prod_def by simp
   41.10  
   41.11  lemma SUP_prod_alt_def:
   41.12 -  "SUPREMUM A f = (SUPREMUM A (fst \<circ> f), SUPREMUM A (snd \<circ> f))"
   41.13 +  "Sup (f ` A) = (Sup ((fst \<circ> f) ` A), Sup((snd \<circ> f) ` A))"
   41.14    unfolding Sup_prod_def by simp
   41.15  
   41.16  
   41.17 @@ -235,7 +235,7 @@
   41.18  instance prod :: (complete_distrib_lattice, complete_distrib_lattice) complete_distrib_lattice
   41.19  proof
   41.20    fix A::"('a\<times>'b) set set"
   41.21 -  show "INFIMUM A Sup \<le> SUPREMUM {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y} Inf"
   41.22 +  show "Inf (Sup ` A) \<le> Sup (Inf ` {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y})"
   41.23      by (simp add: Sup_prod_def Inf_prod_def INF_SUP_set)
   41.24  qed
   41.25  
    42.1 --- a/src/HOL/Library/Set_Algebras.thy	Sun Nov 18 09:51:41 2018 +0100
    42.2 +++ b/src/HOL/Library/Set_Algebras.thy	Sun Nov 18 18:07:51 2018 +0000
    42.3 @@ -408,8 +408,8 @@
    42.4    by (auto simp: set_times_def)
    42.5  
    42.6  lemma set_times_UNION_distrib:
    42.7 -  "A * UNION I M = (\<Union>i\<in>I. A * M i)"
    42.8 -  "UNION I M * A = (\<Union>i\<in>I. M i * A)"
    42.9 +  "A * \<Union>(M ` I) = (\<Union>i\<in>I. A * M i)"
   42.10 +  "\<Union>(M ` I) * A = (\<Union>i\<in>I. M i * A)"
   42.11    by (auto simp: set_times_def)
   42.12  
   42.13  end
    43.1 --- a/src/HOL/Library/Set_Idioms.thy	Sun Nov 18 09:51:41 2018 +0100
    43.2 +++ b/src/HOL/Library/Set_Idioms.thy	Sun Nov 18 18:07:51 2018 +0000
    43.3 @@ -468,13 +468,13 @@
    43.4        using R unfolding relative_to_def intersection_of_def  by auto
    43.5      then obtain f where f: "\<And>T. T \<in> \<U> \<Longrightarrow> P (f T)" "\<And>T. T \<in> \<U> \<Longrightarrow> U \<inter> (f T) = T"
    43.6        by metis
    43.7 -    then have "\<exists>\<U>'\<subseteq>Collect P. \<Inter>\<U>' = INTER \<U> f"
    43.8 -      by (metis image_subset_iff mem_Collect_eq)
    43.9 -    moreover have eq: "U \<inter> INTER \<U> f = U \<inter> \<Inter>\<U>"
   43.10 +    then have "f `  \<U> \<subseteq> Collect P"
   43.11 +      by auto
   43.12 +    moreover have eq: "U \<inter> \<Inter>(f ` \<U>) = U \<inter> \<Inter>\<U>"
   43.13        using f by auto
   43.14      ultimately show ?thesis
   43.15        unfolding relative_to_def intersection_of_def arbitrary_def \<open>S = U \<inter> \<Inter>\<U>\<close>
   43.16 -      by metis
   43.17 +      by auto
   43.18    qed
   43.19    ultimately show ?thesis
   43.20      by blast
   43.21 @@ -502,13 +502,14 @@
   43.22        using R unfolding relative_to_def intersection_of_def  by auto
   43.23      then obtain f where f: "\<And>T. T \<in> \<U> \<Longrightarrow> P (f T)" "\<And>T. T \<in> \<U> \<Longrightarrow> U \<inter> (f T) = T"
   43.24        by metis
   43.25 -    then have "\<exists>\<U>'\<subseteq>Collect P. \<Inter>\<U>' = INTER \<U> f"
   43.26 -      by (metis image_subset_iff mem_Collect_eq)
   43.27 -    moreover have eq: "U \<inter> INTER \<U> f = U \<inter> \<Inter>\<U>"
   43.28 +    then have "f `  \<U> \<subseteq> Collect P"
   43.29 +      by auto
   43.30 +    moreover have eq: "U \<inter> \<Inter> (f ` \<U>) = U \<inter> \<Inter> \<U>"
   43.31        using f by auto
   43.32      ultimately show ?thesis
   43.33        unfolding relative_to_def intersection_of_def \<open>S = U \<inter> \<Inter>\<U>\<close>
   43.34 -      by (metis (no_types, hide_lams) \<open>finite \<U>\<close> f(1) finite_imageI image_subset_iff mem_Collect_eq)
   43.35 +      using \<open>finite \<U>\<close>
   43.36 +      by auto
   43.37    qed
   43.38    ultimately show ?thesis
   43.39      by blast
   43.40 @@ -536,13 +537,14 @@
   43.41        using R unfolding relative_to_def intersection_of_def  by auto
   43.42      then obtain f where f: "\<And>T. T \<in> \<U> \<Longrightarrow> P (f T)" "\<And>T. T \<in> \<U> \<Longrightarrow> U \<inter> (f T) = T"
   43.43        by metis
   43.44 -    then have "\<exists>\<U>'\<subseteq>Collect P. \<Inter>\<U>' = INTER \<U> f"
   43.45 -      by (metis image_subset_iff mem_Collect_eq)
   43.46 -    moreover have eq: "U \<inter> INTER \<U> f = U \<inter> \<Inter>\<U>"
   43.47 +    then have "f `  \<U> \<subseteq> Collect P"
   43.48 +      by auto
   43.49 +    moreover have eq: "U \<inter> \<Inter> (f ` \<U>) = U \<inter> \<Inter> \<U>"
   43.50        using f by auto
   43.51      ultimately show ?thesis
   43.52        unfolding relative_to_def intersection_of_def \<open>S = U \<inter> \<Inter>\<U>\<close>
   43.53 -      by (metis (no_types, hide_lams) \<open>countable \<U>\<close> f(1) countable_image image_subset_iff mem_Collect_eq)
   43.54 +      using \<open>countable \<U>\<close> countable_image
   43.55 +      by auto
   43.56    qed
   43.57    ultimately show ?thesis
   43.58      by blast
    44.1 --- a/src/HOL/Library/Stream.thy	Sun Nov 18 09:51:41 2018 +0100
    44.2 +++ b/src/HOL/Library/Stream.thy	Sun Nov 18 18:07:51 2018 +0000
    44.3 @@ -510,10 +510,10 @@
    44.4          intro!: exI[of _ m, OF disjI1] bexI[of _ "ss !! n"] exI[of _ n, OF mp])
    44.5  qed
    44.6  
    44.7 -lemma sset_smerge: "sset (smerge ss) = UNION (sset ss) sset"
    44.8 +lemma sset_smerge: "sset (smerge ss) = \<Union>(sset ` (sset ss))"
    44.9  proof safe
   44.10    fix x assume "x \<in> sset (smerge ss)"
   44.11 -  thus "x \<in> UNION (sset ss) sset"
   44.12 +  thus "x \<in> \<Union>(sset ` (sset ss))"
   44.13      unfolding smerge_def by (subst (asm) sset_flat)
   44.14        (auto simp: stream.set_map in_set_conv_nth sset_range simp del: stake.simps, fast+)
   44.15  next
    45.1 --- a/src/HOL/Probability/Fin_Map.thy	Sun Nov 18 09:51:41 2018 +0100
    45.2 +++ b/src/HOL/Probability/Fin_Map.thy	Sun Nov 18 18:07:51 2018 +0000
    45.3 @@ -807,7 +807,7 @@
    45.4    qed
    45.5  next
    45.6    case (Union a)
    45.7 -  have "UNION UNIV a \<inter> {m. domain m \<in> J} = (\<Union>i. (a i \<inter> {m. domain m \<in> J}))"
    45.8 +  have "\<Union>(a ` UNIV) \<inter> {m. domain m \<in> J} = (\<Union>i. (a i \<inter> {m. domain m \<in> J}))"
    45.9      by simp
   45.10    also have "\<dots> \<in> sets (PiF J M)" using Union by (intro sets.countable_nat_UN) auto
   45.11    finally show ?case .
    46.1 --- a/src/HOL/Probability/Independent_Family.thy	Sun Nov 18 09:51:41 2018 +0100
    46.2 +++ b/src/HOL/Probability/Independent_Family.thy	Sun Nov 18 18:07:51 2018 +0000
    46.3 @@ -542,7 +542,7 @@
    46.4            by auto
    46.5          { interpret sigma_algebra "space M" "?UN j"
    46.6              by (rule sigma_algebra_sigma_sets) auto
    46.7 -          have "\<And>A. (\<And>i. i \<in> J \<Longrightarrow> A i \<in> ?UN j) \<Longrightarrow> INTER J A \<in> ?UN j"
    46.8 +          have "\<And>A. (\<And>i. i \<in> J \<Longrightarrow> A i \<in> ?UN j) \<Longrightarrow> \<Inter>(A ` J) \<in> ?UN j"
    46.9              using \<open>finite J\<close> \<open>J \<noteq> {}\<close> by (rule finite_INT) blast }
   46.10          note INT = this
   46.11  
   46.12 @@ -620,7 +620,7 @@
   46.13    fix X assume X: "X \<in> tail_events A"
   46.14    let ?A = "(\<Inter>n. sigma_sets (space M) (UNION {n..} A))"
   46.15    from X have "\<And>n::nat. X \<in> sigma_sets (space M) (UNION {n..} A)" by (auto simp: tail_events_def)
   46.16 -  from this[of 0] have "X \<in> sigma_sets (space M) (UNION UNIV A)" by simp
   46.17 +  from this[of 0] have "X \<in> sigma_sets (space M) (\<Union>(A ` UNIV))" by simp
   46.18    then show "X \<in> events"
   46.19      by induct (insert A, auto)
   46.20  qed
   46.21 @@ -634,12 +634,12 @@
   46.22    interpret A: sigma_algebra "space M" "A i" for i by fact
   46.23    { fix X x assume "X \<in> ?A" "x \<in> X"
   46.24      then have "\<And>n. X \<in> sigma_sets (space M) (UNION {n..} A)" by auto
   46.25 -    from this[of 0] have "X \<in> sigma_sets (space M) (UNION UNIV A)" by simp
   46.26 +    from this[of 0] have "X \<in> sigma_sets (space M) (\<Union>(A ` UNIV))" by simp
   46.27      then have "X \<subseteq> space M"
   46.28        by induct (insert A.sets_into_space, auto)
   46.29      with \<open>x \<in> X\<close> show "x \<in> space M" by auto }
   46.30    { fix F :: "nat \<Rightarrow> 'a set" and n assume "range F \<subseteq> ?A"
   46.31 -    then show "(UNION UNIV F) \<in> sigma_sets (space M) (UNION {n..} A)"
   46.32 +    then show "(\<Union>(F ` UNIV)) \<in> sigma_sets (space M) (UNION {n..} A)"
   46.33        by (intro sigma_sets.Union) auto }
   46.34  qed (auto intro!: sigma_sets.Compl sigma_sets.Empty)
   46.35  
   46.36 @@ -906,7 +906,7 @@
   46.37        by (auto intro!: exI[of _ "space (M' i)"]) }
   46.38    note indep_sets_finite_X = indep_sets_finite[OF I this]
   46.39  
   46.40 -  have "(\<forall>A\<in>\<Pi> i\<in>I. {X i -` A \<inter> space M |A. A \<in> E i}. prob (INTER I A) = (\<Prod>j\<in>I. prob (A j))) =
   46.41 +  have "(\<forall>A\<in>\<Pi> i\<in>I. {X i -` A \<inter> space M |A. A \<in> E i}. prob (\<Inter>(A ` I)) = (\<Prod>j\<in>I. prob (A j))) =
   46.42      (\<forall>A\<in>\<Pi> i\<in>I. E i. prob ((\<Inter>j\<in>I. X j -` A j) \<inter> space M) = (\<Prod>x\<in>I. prob (X x -` A x \<inter> space M)))"
   46.43      (is "?L = ?R")
   46.44    proof safe
   46.45 @@ -920,7 +920,7 @@
   46.46      from bchoice[OF this] obtain B where B: "\<forall>i\<in>I. A i = X i -` B i \<inter> space M"
   46.47        "B \<in> (\<Pi> i\<in>I. E i)" by auto
   46.48      from \<open>?R\<close>[THEN bspec, OF B(2)] B(1) \<open>I \<noteq> {}\<close>
   46.49 -    show "prob (INTER I A) = (\<Prod>j\<in>I. prob (A j))"
   46.50 +    show "prob (\<Inter>(A ` I)) = (\<Prod>j\<in>I. prob (A j))"
   46.51        by simp
   46.52    qed
   46.53    then show ?thesis using \<open>I \<noteq> {}\<close>
    47.1 --- a/src/HOL/Probability/Probability_Mass_Function.thy	Sun Nov 18 09:51:41 2018 +0100
    47.2 +++ b/src/HOL/Probability/Probability_Mass_Function.thy	Sun Nov 18 18:07:51 2018 +0000
    47.3 @@ -1851,15 +1851,15 @@
    47.4    uniformly at random.
    47.5  \<close>
    47.6  lemma pmf_of_set_UN:
    47.7 -  assumes "finite (UNION A f)" "A \<noteq> {}" "\<And>x. x \<in> A \<Longrightarrow> f x \<noteq> {}"
    47.8 +  assumes "finite (\<Union>(f ` A))" "A \<noteq> {}" "\<And>x. x \<in> A \<Longrightarrow> f x \<noteq> {}"
    47.9            "\<And>x. x \<in> A \<Longrightarrow> card (f x) = n" "disjoint_family_on f A"
   47.10 -  shows   "pmf_of_set (UNION A f) = do {x \<leftarrow> pmf_of_set A; pmf_of_set (f x)}"
   47.11 +  shows   "pmf_of_set (\<Union>(f ` A)) = do {x \<leftarrow> pmf_of_set A; pmf_of_set (f x)}"
   47.12              (is "?lhs = ?rhs")
   47.13  proof (intro pmf_eqI)
   47.14    fix x
   47.15    from assms have [simp]: "finite A"
   47.16      using infinite_disjoint_family_imp_infinite_UNION[of A f] by blast
   47.17 -  from assms have "ereal (pmf (pmf_of_set (UNION A f)) x) =
   47.18 +  from assms have "ereal (pmf (pmf_of_set (\<Union>(f ` A))) x) =
   47.19      ereal (indicator (\<Union>x\<in>A. f x) x / real (card (\<Union>x\<in>A. f x)))"
   47.20      by (subst pmf_of_set) auto
   47.21    also from assms have "card (\<Union>x\<in>A. f x) = card A * n"
    48.1 --- a/src/HOL/Probability/Projective_Family.thy	Sun Nov 18 09:51:41 2018 +0100
    48.2 +++ b/src/HOL/Probability/Projective_Family.thy	Sun Nov 18 18:07:51 2018 +0000
    48.3 @@ -641,7 +641,7 @@
    48.4        proof (subst distr_distr)
    48.5          have "(\<lambda>\<omega>. \<omega> (t x)) \<in> measurable (Pi\<^sub>M UNIV (\<lambda>x. M (f x))) (M x)" if x: "x \<in> J i" for x i
    48.6            using measurable_component_singleton[of "t x" "UNIV" "\<lambda>x. M (f x)"] unfolding ft[OF x] by simp
    48.7 -        then show "(\<lambda>\<omega>. \<lambda>x\<in>\<Union>i. J i. \<omega> (t x)) \<in> measurable IT.PF.lim (Pi\<^sub>M (UNION UNIV J) M)"
    48.8 +        then show "(\<lambda>\<omega>. \<lambda>x\<in>\<Union>i. J i. \<omega> (t x)) \<in> measurable IT.PF.lim (Pi\<^sub>M (\<Union>(J ` UNIV)) M)"
    48.9            by (auto intro!: measurable_restrict simp: measurable_cong_sets[OF IT.PF.sets_lim refl])
   48.10        qed (auto intro!: distr_cong measurable_restrict measurable_component_singleton)
   48.11        also have "\<dots> = distr (distr IT.PF.lim (PiM (t`J i) (\<lambda>x. M (f x))) (\<lambda>\<omega>. restrict \<omega> (t`J i))) (Pi\<^sub>M (J i) M) (\<lambda>\<omega>. \<lambda>n\<in>J i. \<omega> (t n))"
    49.1 --- a/src/HOL/Probability/Stopping_Time.thy	Sun Nov 18 09:51:41 2018 +0100
    49.2 +++ b/src/HOL/Probability/Stopping_Time.thy	Sun Nov 18 18:07:51 2018 +0000
    49.3 @@ -87,9 +87,9 @@
    49.4    fix AA :: "nat \<Rightarrow> 'a set" and t assume "range AA \<subseteq> {A. \<forall>t. {\<omega> \<in> A. T \<omega> \<le> t} \<in> sets (F t)}"
    49.5    then have "(\<Union>i. {\<omega> \<in> AA i. T \<omega> \<le> t}) \<in> sets (F t)" for t
    49.6      by auto
    49.7 -  also have "(\<Union>i. {\<omega> \<in> AA i. T \<omega> \<le> t}) = {\<omega> \<in> UNION UNIV AA. T \<omega> \<le> t}"
    49.8 +  also have "(\<Union>i. {\<omega> \<in> AA i. T \<omega> \<le> t}) = {\<omega> \<in> \<Union>(AA ` UNIV). T \<omega> \<le> t}"
    49.9      by auto
   49.10 -  finally show "{\<omega> \<in> UNION UNIV AA. T \<omega> \<le> t} \<in> sets (F t)" .
   49.11 +  finally show "{\<omega> \<in> \<Union>(AA ` UNIV). T \<omega> \<le> t} \<in> sets (F t)" .
   49.12  qed auto
   49.13  
   49.14  lemma sets_pre_sigma: "stopping_time F T \<Longrightarrow> sets (pre_sigma T) = {A. \<forall>t. {\<omega>\<in>A. T \<omega> \<le> t} \<in> sets (F t)}"
    50.1 --- a/src/HOL/Probability/Tree_Space.thy	Sun Nov 18 09:51:41 2018 +0100
    50.2 +++ b/src/HOL/Probability/Tree_Space.thy	Sun Nov 18 18:07:51 2018 +0000
    50.3 @@ -197,7 +197,7 @@
    50.4      finally show ?case .
    50.5    next
    50.6      case (Union I)
    50.7 -    have *: "{Node l v r |l v r. (v, l, r) \<in> UNION UNIV I} =
    50.8 +    have *: "{Node l v r |l v r. (v, l, r) \<in> \<Union>(I ` UNIV)} =
    50.9        (\<Union>i. {Node l v r |l v r. (v, l, r) \<in> I i})" by auto
   50.10      show ?case unfolding * using Union(2) by (intro sets.countable_UN) auto
   50.11    qed
    51.1 --- a/src/HOL/Probability/ex/Measure_Not_CCC.thy	Sun Nov 18 09:51:41 2018 +0100
    51.2 +++ b/src/HOL/Probability/ex/Measure_Not_CCC.thy	Sun Nov 18 18:07:51 2018 +0000
    51.3 @@ -109,7 +109,7 @@
    51.4      define G where "G j = (\<Union>i. if j \<in> J i then F i j else X i)" for j
    51.5      show "(\<Union>i. X i) \<in> sets M" "countable (\<Union>i. J i)" "G \<in> (\<Union>i. J i) \<rightarrow> sets M"
    51.6        using XFJ by (auto simp: G_def Pi_iff)
    51.7 -    show "UNION UNIV A = (UNIV - (\<Union>i. J i)) \<times> (\<Union>i. X i) \<union> (SIGMA j:\<Union>i. J i. \<Union>i. if j \<in> J i then F i j else X i)"
    51.8 +    show "\<Union>(A ` UNIV) = (UNIV - (\<Union>i. J i)) \<times> (\<Union>i. X i) \<union> (SIGMA j:\<Union>i. J i. \<Union>i. if j \<in> J i then F i j else X i)"
    51.9        unfolding A_eq by (auto split: if_split_asm)
   51.10    qed
   51.11  qed
    52.1 --- a/src/HOL/UNITY/Comp/Alloc.thy	Sun Nov 18 09:51:41 2018 +0100
    52.2 +++ b/src/HOL/UNITY/Comp/Alloc.thy	Sun Nov 18 18:07:51 2018 +0000
    52.3 @@ -163,7 +163,7 @@
    52.4    alloc_allowed_acts :: "'a allocState_d program set"
    52.5    where "alloc_allowed_acts =
    52.6         {F. AllowedActs F =
    52.7 -            insert Id (UNION (preserves allocGiv) Acts)}"
    52.8 +            insert Id (\<Union>(Acts ` (preserves allocGiv)))}"
    52.9  
   52.10  definition
   52.11    alloc_spec :: "'a allocState_d program set"
    53.1 --- a/src/HOL/UNITY/Comp/AllocBase.thy	Sun Nov 18 09:51:41 2018 +0100
    53.2 +++ b/src/HOL/UNITY/Comp/AllocBase.thy	Sun Nov 18 18:07:51 2018 +0000
    53.3 @@ -77,7 +77,7 @@
    53.4  
    53.5  lemma bag_of_nths_UN_disjoint [rule_format]:
    53.6       "[| finite I; \<forall>i\<in>I. \<forall>j\<in>I. i\<noteq>j \<longrightarrow> A i Int A j = {} |]  
    53.7 -      ==> bag_of (nths l (UNION I A)) =   
    53.8 +      ==> bag_of (nths l (\<Union>(A ` I))) =   
    53.9            (\<Sum>i\<in>I. bag_of (nths l (A i)))"
   53.10  apply (auto simp add: bag_of_nths)
   53.11  unfolding UN_simps [symmetric]
    54.1 --- a/src/HOL/UNITY/Comp/AllocImpl.thy	Sun Nov 18 09:51:41 2018 +0100
    54.2 +++ b/src/HOL/UNITY/Comp/AllocImpl.thy	Sun Nov 18 18:07:51 2018 +0000
    54.3 @@ -116,7 +116,7 @@
    54.4  definition
    54.5    distr_allowed_acts :: "('a,'b) distr_d program set"
    54.6    where "distr_allowed_acts =
    54.7 -       {D. AllowedActs D = insert Id (UNION (preserves distr.Out) Acts)}"
    54.8 +       {D. AllowedActs D = insert Id (\<Union>(Acts ` (preserves distr.Out)))}"
    54.9  
   54.10  definition
   54.11    distr_spec :: "('a,'b) distr_d program set"
   54.12 @@ -160,7 +160,7 @@
   54.13    (*environmental constraints*)
   54.14    alloc_allowed_acts :: "'a allocState_d program set"
   54.15    where "alloc_allowed_acts =
   54.16 -       {F. AllowedActs F = insert Id (UNION (preserves giv) Acts)}"
   54.17 +       {F. AllowedActs F = insert Id (\<Union>(Acts ` (preserves giv)))}"
   54.18  
   54.19  definition
   54.20    alloc_spec :: "'a allocState_d program set"
    55.1 --- a/src/HOL/UNITY/Constrains.thy	Sun Nov 18 09:51:41 2018 +0100
    55.2 +++ b/src/HOL/UNITY/Constrains.thy	Sun Nov 18 18:07:51 2018 +0000
    55.3 @@ -373,7 +373,7 @@
    55.4  lemma Always_Int_distrib: "Always (A \<inter> B) = Always A \<inter> Always B"
    55.5  by (auto simp add: Always_eq_includes_reachable)
    55.6  
    55.7 -lemma Always_INT_distrib: "Always (INTER I A) = (\<Inter>i \<in> I. Always (A i))"
    55.8 +lemma Always_INT_distrib: "Always (\<Inter>(A ` I)) = (\<Inter>i \<in> I. Always (A i))"
    55.9  by (auto simp add: Always_eq_includes_reachable)
   55.10  
   55.11  lemma Always_Int_I:
    56.1 --- a/src/HOL/UNITY/Extend.thy	Sun Nov 18 09:51:41 2018 +0100
    56.2 +++ b/src/HOL/UNITY/Extend.thy	Sun Nov 18 18:07:51 2018 +0000
    56.3 @@ -249,7 +249,7 @@
    56.4  lemma extend_set_Int_distrib: "extend_set h (A \<inter> B) = extend_set h A \<inter> extend_set h B"
    56.5    by auto
    56.6  
    56.7 -lemma extend_set_INT_distrib: "extend_set h (INTER A B) = (\<Inter>x \<in> A. extend_set h (B x))"
    56.8 +lemma extend_set_INT_distrib: "extend_set h (\<Inter>(B ` A)) = (\<Inter>x \<in> A. extend_set h (B x))"
    56.9    by auto
   56.10  
   56.11  lemma extend_set_Diff_distrib: "extend_set h (A - B) = extend_set h A - extend_set h B"
    57.1 --- a/src/HOL/UNITY/Guar.thy	Sun Nov 18 09:51:41 2018 +0100
    57.2 +++ b/src/HOL/UNITY/Guar.thy	Sun Nov 18 18:07:51 2018 +0000
    57.3 @@ -215,7 +215,7 @@
    57.4  by (simp add: guarantees_Int_right)
    57.5  
    57.6  lemma guarantees_INT_right_iff:
    57.7 -     "(F \<in> X guarantees (INTER I Y)) = (\<forall>i\<in>I. F \<in> X guarantees (Y i))"
    57.8 +     "(F \<in> X guarantees (\<Inter>(Y ` I))) = (\<forall>i\<in>I. F \<in> X guarantees (Y i))"
    57.9  by (simp add: guarantees_INT_right)
   57.10  
   57.11  lemma shunting: "(X guarantees Y) = (UNIV guarantees (-X \<union> Y))"
   57.12 @@ -276,7 +276,7 @@
   57.13  
   57.14  lemma guarantees_JN_INT: 
   57.15       "[| \<forall>i\<in>I. F i \<in> X i guarantees Y i;  OK I F |]  
   57.16 -      ==> (JOIN I F) \<in> (INTER I X) guarantees (INTER I Y)"
   57.17 +      ==> (JOIN I F) \<in> (\<Inter>(X ` I)) guarantees (\<Inter>(Y ` I))"
   57.18  apply (unfold guar_def, auto)
   57.19  apply (drule bspec, assumption)
   57.20  apply (rename_tac "i")
   57.21 @@ -287,7 +287,7 @@
   57.22  
   57.23  lemma guarantees_JN_UN: 
   57.24      "[| \<forall>i\<in>I. F i \<in> X i guarantees Y i;  OK I F |]  
   57.25 -     ==> (JOIN I F) \<in> (UNION I X) guarantees (UNION I Y)"
   57.26 +     ==> (JOIN I F) \<in> (\<Union>(X ` I)) guarantees (\<Union>(Y ` I))"
   57.27  apply (unfold guar_def, auto)
   57.28  apply (drule bspec, assumption)
   57.29  apply (rename_tac "i")
    58.1 --- a/src/HOL/UNITY/Lift_prog.thy	Sun Nov 18 09:51:41 2018 +0100
    58.2 +++ b/src/HOL/UNITY/Lift_prog.thy	Sun Nov 18 18:07:51 2018 +0000
    58.3 @@ -378,14 +378,14 @@
    58.4  subsection\<open>OK and "lift"\<close>
    58.5  
    58.6  lemma act_in_UNION_preserves_fst:
    58.7 -     "act \<subseteq> {(x,x'). fst x = fst x'} ==> act \<in> UNION (preserves fst) Acts"
    58.8 +     "act \<subseteq> {(x,x'). fst x = fst x'} ==> act \<in> \<Union>(Acts ` (preserves fst))"
    58.9  apply (rule_tac a = "mk_program (UNIV,{act},UNIV) " in UN_I)
   58.10  apply (auto simp add: preserves_def stable_def constrains_def)
   58.11  done
   58.12  
   58.13  lemma UNION_OK_lift_I:
   58.14       "[| \<forall>i \<in> I. F i \<in> preserves snd;   
   58.15 -         \<forall>i \<in> I. UNION (preserves fst) Acts \<subseteq> AllowedActs (F i) |]  
   58.16 +         \<forall>i \<in> I. \<Union>(Acts ` (preserves fst)) \<subseteq> AllowedActs (F i) |]  
   58.17        ==> OK I (%i. lift i (F i))"
   58.18  apply (auto simp add: OK_def lift_def rename_def Extend.Acts_extend)
   58.19  apply (simp add: Extend.AllowedActs_extend project_act_extend_act)
    59.1 --- a/src/HOL/UNITY/Simple/Reachability.thy	Sun Nov 18 09:51:41 2018 +0100
    59.2 +++ b/src/HOL/UNITY/Simple/Reachability.thy	Sun Nov 18 18:07:51 2018 +0000
    59.3 @@ -42,7 +42,7 @@
    59.4  
    59.5  definition final :: "state set" where
    59.6    "final == (\<Inter>v\<in>V. reachable v <==> {s. (root, v) \<in> REACHABLE}) \<inter> 
    59.7 -            (INTER E (nmsg_eq 0))"
    59.8 +            (\<Inter>((nmsg_eq 0) ` E))"
    59.9  
   59.10  axiomatization
   59.11  where
    60.1 --- a/src/HOL/UNITY/Union.thy	Sun Nov 18 09:51:41 2018 +0100
    60.2 +++ b/src/HOL/UNITY/Union.thy	Sun Nov 18 18:07:51 2018 +0000
    60.3 @@ -36,7 +36,7 @@
    60.4    (*Characterizes safety properties.  Used with specifying Allowed*)
    60.5  definition
    60.6    safety_prop :: "'a program set => bool"
    60.7 -  where "safety_prop X \<longleftrightarrow> SKIP \<in> X \<and> (\<forall>G. Acts G \<subseteq> UNION X Acts \<longrightarrow> G \<in> X)"
    60.8 +  where "safety_prop X \<longleftrightarrow> SKIP \<in> X \<and> (\<forall>G. Acts G \<subseteq> \<Union>(Acts ` X) \<longrightarrow> G \<in> X)"
    60.9  
   60.10  syntax
   60.11    "_JOIN1" :: "[pttrns, 'b set] => 'b set"              ("(3\<Squnion>_./ _)" 10)
   60.12 @@ -376,15 +376,15 @@
   60.13   given instances of "ok"\<close>
   60.14  
   60.15  lemma safety_prop_Acts_iff:
   60.16 -     "safety_prop X ==> (Acts G \<subseteq> insert Id (UNION X Acts)) = (G \<in> X)"
   60.17 +     "safety_prop X ==> (Acts G \<subseteq> insert Id (\<Union>(Acts ` X))) = (G \<in> X)"
   60.18  by (auto simp add: safety_prop_def)
   60.19  
   60.20  lemma safety_prop_AllowedActs_iff_Allowed:
   60.21 -     "safety_prop X ==> (UNION X Acts \<subseteq> AllowedActs F) = (X \<subseteq> Allowed F)"
   60.22 +     "safety_prop X ==> (\<Union>(Acts ` X) \<subseteq> AllowedActs F) = (X \<subseteq> Allowed F)"
   60.23  by (auto simp add: Allowed_def safety_prop_Acts_iff [symmetric])
   60.24  
   60.25  lemma Allowed_eq:
   60.26 -     "safety_prop X ==> Allowed (mk_program (init, acts, UNION X Acts)) = X"
   60.27 +     "safety_prop X ==> Allowed (mk_program (init, acts, \<Union>(Acts ` X))) = X"
   60.28  by (simp add: Allowed_def safety_prop_Acts_iff)
   60.29  
   60.30  (*For safety_prop to hold, the property must be satisfiable!*)
   60.31 @@ -426,7 +426,7 @@
   60.32    by (rule safety_prop_INTER) simp
   60.33  
   60.34  lemma def_prg_Allowed:
   60.35 -     "[| F == mk_program (init, acts, UNION X Acts) ; safety_prop X |]  
   60.36 +     "[| F == mk_program (init, acts, \<Union>(Acts ` X)) ; safety_prop X |]  
   60.37        ==> Allowed F = X"
   60.38  by (simp add: Allowed_eq)
   60.39  
   60.40 @@ -434,12 +434,12 @@
   60.41  by (simp add: Allowed_def) 
   60.42  
   60.43  lemma def_total_prg_Allowed:
   60.44 -     "[| F = mk_total_program (init, acts, UNION X Acts) ; safety_prop X |]  
   60.45 +     "[| F = mk_total_program (init, acts, \<Union>(Acts ` X)) ; safety_prop X |]  
   60.46        ==> Allowed F = X"
   60.47  by (simp add: mk_total_program_def def_prg_Allowed) 
   60.48  
   60.49  lemma def_UNION_ok_iff:
   60.50 -     "[| F = mk_program(init,acts,UNION X Acts); safety_prop X |]  
   60.51 +     "[| F = mk_program(init,acts,\<Union>(Acts ` X)); safety_prop X |]  
   60.52        ==> F ok G = (G \<in> X & acts \<subseteq> AllowedActs G)"
   60.53  by (auto simp add: ok_def safety_prop_Acts_iff)
   60.54