--- a/src/Doc/Main/Main_Doc.thy Sun Nov 18 09:51:41 2018 +0100
+++ b/src/Doc/Main/Main_Doc.thy Sun Nov 18 18:07:51 2018 +0000
@@ -112,8 +112,6 @@
@{const Set.member} & @{term_type_only Set.member "'a\<Rightarrow>'a set\<Rightarrow>bool"} & (\<^verbatim>\<open>:\<close>)\\
@{const Set.union} & @{term_type_only Set.union "'a set\<Rightarrow>'a set \<Rightarrow> 'a set"} & (\<^verbatim>\<open>Un\<close>)\\
@{const Set.inter} & @{term_type_only Set.inter "'a set\<Rightarrow>'a set \<Rightarrow> 'a set"} & (\<^verbatim>\<open>Int\<close>)\\
-@{const UNION} & @{term_type_only UNION "'a set\<Rightarrow>('a \<Rightarrow> 'b set) \<Rightarrow> 'b set"}\\
-@{const INTER} & @{term_type_only INTER "'a set\<Rightarrow>('a \<Rightarrow> 'b set) \<Rightarrow> 'b set"}\\
@{const Union} & @{term_type_only Union "'a set set\<Rightarrow>'a set"}\\
@{const Inter} & @{term_type_only Inter "'a set set\<Rightarrow>'a set"}\\
@{const Pow} & @{term_type_only Pow "'a set \<Rightarrow>'a set set"}\\
@@ -134,10 +132,10 @@
@{term[source]"A \<supset> B"} & @{term[source]"B < A"}\\
@{term "{x. P}"} & @{term[source]"Collect (\<lambda>x. P)"}\\
\<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>\\
-@{term[source]"\<Union>x\<in>I. A"} & @{term[source]"UNION I (\<lambda>x. A)"} & (\texttt{UN})\\
-@{term[source]"\<Union>x. A"} & @{term[source]"UNION UNIV (\<lambda>x. A)"}\\
-@{term[source]"\<Inter>x\<in>I. A"} & @{term[source]"INTER I (\<lambda>x. A)"} & (\texttt{INT})\\
-@{term[source]"\<Inter>x. A"} & @{term[source]"INTER UNIV (\<lambda>x. A)"}\\
+@{term[source]"\<Union>x\<in>I. A"} & @{term[source]"\<Union>((\<lambda>x. A) ` I)"} & (\texttt{UN})\\
+@{term[source]"\<Union>x. A"} & @{term[source]"\<Union>((\<lambda>x. A) ` UNIV)"}\\
+@{term[source]"\<Inter>x\<in>I. A"} & @{term[source]"\<Inter>((\<lambda>x. A) ` I)"} & (\texttt{INT})\\
+@{term[source]"\<Inter>x. A"} & @{term[source]"\<Inter>((\<lambda>x. A) ` UNIV)"}\\
@{term "\<forall>x\<in>A. P"} & @{term[source]"Ball A (\<lambda>x. P)"}\\
@{term "\<exists>x\<in>A. P"} & @{term[source]"Bex A (\<lambda>x. P)"}\\
@{term "range f"} & @{term[source]"f ` UNIV"}\\
--- a/src/HOL/Algebra/FiniteProduct.thy Sun Nov 18 09:51:41 2018 +0100
+++ b/src/HOL/Algebra/FiniteProduct.thy Sun Nov 18 18:07:51 2018 +0000
@@ -576,7 +576,7 @@
assumes
"finite I" "\<And>i. i \<in> I \<Longrightarrow> finite (A i)" "pairwise (\<lambda>i j. disjnt (A i) (A j)) I"
"\<And>i x. i \<in> I \<Longrightarrow> x \<in> A i \<Longrightarrow> g x \<in> carrier G"
-shows "finprod G g (UNION I A) = finprod G (\<lambda>i. finprod G g (A i)) I"
+shows "finprod G g (\<Union>(A ` I)) = finprod G (\<lambda>i. finprod G g (A i)) I"
using assms
proof (induction set: finite)
case empty
--- a/src/HOL/Analysis/Abstract_Topology.thy Sun Nov 18 09:51:41 2018 +0100
+++ b/src/HOL/Analysis/Abstract_Topology.thy Sun Nov 18 18:07:51 2018 +0000
@@ -2664,11 +2664,11 @@
(\<forall>\<U>. \<U> \<subseteq> (\<lambda>T. S \<inter> T) ` {T. closedin X T} \<longrightarrow>
(\<forall>\<F>. finite \<F> \<longrightarrow> \<F> \<subseteq> \<U> \<longrightarrow> \<Inter>\<F> \<noteq> {}) \<longrightarrow> \<Inter>\<U> \<noteq> {})"
by (simp add: compact_space_fip compactin_subspace closedin_subtopology image_def subset_eq Int_commute imp_conjL)
- 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> {})"
+ 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> {})"
by (simp add: all_subset_image)
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> {})"
proof -
- have eq: "((\<forall>\<F>. finite \<F> \<and> \<F> \<subseteq> \<U> \<longrightarrow> INTER \<F> ((\<inter>) S) \<noteq> {}) \<longrightarrow> INTER \<U> ((\<inter>) S) \<noteq> {}) =
+ have eq: "((\<forall>\<F>. finite \<F> \<and> \<F> \<subseteq> \<U> \<longrightarrow> \<Inter> ((\<inter>) S ` \<F>) \<noteq> {}) \<longrightarrow> \<Inter> ((\<inter>) S ` \<U>) \<noteq> {}) \<longleftrightarrow>
((\<forall>\<F>. finite \<F> \<and> \<F> \<subseteq> \<U> \<longrightarrow> S \<inter> \<Inter>\<F> \<noteq> {}) \<longrightarrow> S \<inter> \<Inter>\<U> \<noteq> {})" for \<U>
by simp (use \<open>S \<noteq> {}\<close> in blast)
show ?thesis
--- a/src/HOL/Analysis/Arcwise_Connected.thy Sun Nov 18 09:51:41 2018 +0100
+++ b/src/HOL/Analysis/Arcwise_Connected.thy Sun Nov 18 18:07:51 2018 +0000
@@ -39,22 +39,22 @@
proof
show "\<Inter>range A \<subseteq> S"
using \<open>\<And>n. A n \<subseteq> S\<close> by blast
- show "closed (INTER UNIV A)"
+ show "closed (\<Inter>(A ` UNIV))"
using clo by blast
- show "\<phi> (INTER UNIV A)"
+ show "\<phi> (\<Inter>(A ` UNIV))"
by (simp add: clo \<phi> sub)
- show "\<not> U \<subset> INTER UNIV A" if "U \<subseteq> S" "closed U" "\<phi> U" for U
+ show "\<not> U \<subset> \<Inter>(A ` UNIV)" if "U \<subseteq> S" "closed U" "\<phi> U" for U
proof -
have "\<exists>y. x \<notin> A y" if "x \<notin> U" and Usub: "U \<subseteq> (\<Inter>x. A x)" for x
proof -
obtain e where "e > 0" and e: "ball x e \<subseteq> -U"
using \<open>closed U\<close> \<open>x \<notin> U\<close> openE [of "-U"] by blast
- moreover obtain K where K: "ball x e = UNION K B"
+ moreover obtain K where K: "ball x e = \<Union>(B ` K)"
using open_cov [of "ball x e"] by auto
- ultimately have "UNION K B \<subseteq> -U"
+ ultimately have "\<Union>(B ` K) \<subseteq> -U"
by blast
have "K \<noteq> {}"
- using \<open>0 < e\<close> \<open>ball x e = UNION K B\<close> by auto
+ using \<open>0 < e\<close> \<open>ball x e = \<Union>(B ` K)\<close> by auto
then obtain n where "n \<in> K" "x \<in> B n"
by (metis K UN_E \<open>0 < e\<close> centre_in_ball)
then have "U \<inter> B n = {}"
@@ -89,16 +89,16 @@
fix F
assume cloF: "\<And>n. closed (F n)"
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"
- show "INTER UNIV F \<noteq> {} \<and> INTER UNIV F \<subseteq> S \<and> \<phi> (INTER UNIV F)"
+ show "\<Inter>(F ` UNIV) \<noteq> {} \<and> \<Inter>(F ` UNIV) \<subseteq> S \<and> \<phi> (\<Inter>(F ` UNIV))"
proof (intro conjI)
- show "INTER UNIV F \<noteq> {}"
+ show "\<Inter>(F ` UNIV) \<noteq> {}"
apply (rule compact_nest)
apply (meson F cloF \<open>compact S\<close> seq_compact_closed_subset seq_compact_eq_compact)
apply (simp add: F)
by (meson Fsub lift_Suc_antimono_le)
- show " INTER UNIV F \<subseteq> S"
+ show " \<Inter>(F ` UNIV) \<subseteq> S"
using F by blast
- show "\<phi> (INTER UNIV F)"
+ show "\<phi> (\<Inter>(F ` UNIV))"
by (metis F Fsub \<phi> \<open>compact S\<close> cloF closed_Int_compact inf.orderE)
qed
next
@@ -1680,7 +1680,7 @@
using that by auto
show "\<phi> {0..1}"
by (auto simp: \<phi>_def open_segment_eq_real_ivl *)
- show "\<phi> (INTER UNIV F)"
+ show "\<phi> (\<Inter>(F ` UNIV))"
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
proof -
have F01: "\<And>n. F n \<subseteq> {0..1} \<and> 0 \<in> F n \<and> 1 \<in> F n"
@@ -1706,13 +1706,13 @@
using minxy \<open>0 < e\<close> less by simp_all
have Fclo: "\<And>T. T \<in> range F \<Longrightarrow> closed T"
by (metis \<open>\<And>n. closed (F n)\<close> image_iff)
- have eq: "{w..z} \<inter> INTER UNIV F = {}"
+ have eq: "{w..z} \<inter> \<Inter>(F ` UNIV) = {}"
using less w z apply (auto simp: open_segment_eq_real_ivl)
by (metis (no_types, hide_lams) INT_I IntI empty_iff greaterThanLessThan_iff not_le order.trans)
then obtain K where "finite K" and K: "{w..z} \<inter> (\<Inter> (F ` K)) = {}"
by (metis finite_subset_image compact_imp_fip [OF compact_interval Fclo])
then have "K \<noteq> {}"
- using \<open>w < z\<close> \<open>{w..z} \<inter> INTER K F = {}\<close> by auto
+ using \<open>w < z\<close> \<open>{w..z} \<inter> \<Inter>(F ` K) = {}\<close> by auto
define n where "n \<equiv> Max K"
have "n \<in> K" unfolding n_def by (metis \<open>K \<noteq> {}\<close> \<open>finite K\<close> Max_in)
have "F n \<subseteq> \<Inter> (F ` K)"
--- a/src/HOL/Analysis/Binary_Product_Measure.thy Sun Nov 18 09:51:41 2018 +0100
+++ b/src/HOL/Analysis/Binary_Product_Measure.thy Sun Nov 18 18:07:51 2018 +0000
@@ -1118,7 +1118,7 @@
unfolding * by auto
next
case (Union A)
- moreover have *: "(UNION UNIV A) \<times> UNIV = UNION UNIV (\<lambda>i. A i \<times> UNIV)"
+ moreover have *: "(\<Union>(A ` UNIV)) \<times> UNIV = \<Union>((\<lambda>i. A i \<times> UNIV) ` UNIV)"
by auto
ultimately show ?case
unfolding * by auto
@@ -1137,7 +1137,7 @@
unfolding * by auto
next
case (Union B)
- moreover have *: "UNIV \<times> (UNION UNIV B) = UNION UNIV (\<lambda>i. UNIV \<times> B i)"
+ moreover have *: "UNIV \<times> (\<Union>(B ` UNIV)) = \<Union>((\<lambda>i. UNIV \<times> B i) ` UNIV)"
by auto
ultimately show ?case
unfolding * by auto
--- a/src/HOL/Analysis/Brouwer_Fixpoint.thy Sun Nov 18 09:51:41 2018 +0100
+++ b/src/HOL/Analysis/Brouwer_Fixpoint.thy Sun Nov 18 18:07:51 2018 +0000
@@ -4779,11 +4779,11 @@
by metis
show ?thesis
proof
- show "openin (subtopology euclidean T') (UNION T F)"
+ show "openin (subtopology euclidean T') (\<Union>(F ` T))"
using F by blast
- show "T \<subseteq> UNION T F"
+ show "T \<subseteq> \<Union>(F ` T)"
using F by blast
- show "S \<times> UNION T F \<subseteq> U"
+ show "S \<times> \<Union>(F ` T) \<subseteq> U"
using F by auto
qed
qed
@@ -4882,23 +4882,23 @@
by (simp add: homotopic_with) metis
have wop: "b \<in> V x \<Longrightarrow> \<exists>k. b \<in> V k \<and> (\<forall>j<k. b \<notin> V j)" for b x
using nat_less_induct [where P = "\<lambda>i. b \<notin> V i"] by meson
- obtain \<zeta> where cont: "continuous_on ({0..1} \<times> UNION UNIV V) \<zeta>"
- and eq: "\<And>x i. \<lbrakk>x \<in> {0..1} \<times> UNION UNIV V \<inter>
+ obtain \<zeta> where cont: "continuous_on ({0..1} \<times> \<Union>(V ` UNIV)) \<zeta>"
+ and eq: "\<And>x i. \<lbrakk>x \<in> {0..1} \<times> \<Union>(V ` UNIV) \<inter>
{0..1} \<times> (V i - (\<Union>m<i. V m))\<rbrakk> \<Longrightarrow> \<zeta> x = h i x"
proof (rule pasting_lemma_exists)
- show "{0..1} \<times> UNION UNIV V \<subseteq> (\<Union>i. {0..1::real} \<times> (V i - (\<Union>m<i. V m)))"
+ show "{0..1} \<times> \<Union>(V ` UNIV) \<subseteq> (\<Union>i. {0..1::real} \<times> (V i - (\<Union>m<i. V m)))"
by (force simp: Ball_def dest: wop)
- show "openin (subtopology euclidean ({0..1} \<times> UNION UNIV V))
+ show "openin (subtopology euclidean ({0..1} \<times> \<Union>(V ` UNIV)))
({0..1::real} \<times> (V i - (\<Union>m<i. V m)))" for i
proof (intro openin_Times openin_subtopology_self openin_diff)
- show "openin (subtopology euclidean (UNION UNIV V)) (V i)"
+ show "openin (subtopology euclidean (\<Union>(V ` UNIV))) (V i)"
using ope V eqU by auto
- show "closedin (subtopology euclidean (UNION UNIV V)) (\<Union>m<i. V m)"
+ show "closedin (subtopology euclidean (\<Union>(V ` UNIV))) (\<Union>m<i. V m)"
using V clo eqU by (force intro: closedin_Union)
qed
show "continuous_on ({0..1} \<times> (V i - (\<Union>m<i. V m))) (h i)" for i
by (rule continuous_on_subset [OF conth]) auto
- show "\<And>i j x. x \<in> {0..1} \<times> UNION UNIV V \<inter>
+ show "\<And>i j x. x \<in> {0..1} \<times> \<Union>(V ` UNIV) \<inter>
{0..1} \<times> (V i - (\<Union>m<i. V m)) \<inter> {0..1} \<times> (V j - (\<Union>m<j. V m))
\<Longrightarrow> h i x = h j x"
by clarsimp (metis lessThan_iff linorder_neqE_nat)
--- a/src/HOL/Analysis/Caratheodory.thy Sun Nov 18 09:51:41 2018 +0100
+++ b/src/HOL/Analysis/Caratheodory.thy Sun Nov 18 18:07:51 2018 +0000
@@ -321,7 +321,7 @@
next
have "(\<Sum>i. f (if i = 0 then s else {})) \<le> f s"
using positiveD1[OF posf] by (subst suminf_finite[of "{0}"]) auto
- 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"
+ 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"
by (intro INF_lower2[of "\<lambda>i. if i = 0 then s else {}"])
(auto simp: disjoint_family_on_def)
qed
@@ -521,8 +521,8 @@
lemma%unimportant volume_finite_additive:
assumes "volume M f"
- assumes A: "\<And>i. i \<in> I \<Longrightarrow> A i \<in> M" "disjoint_family_on A I" "finite I" "UNION I A \<in> M"
- shows "f (UNION I A) = (\<Sum>i\<in>I. f (A i))"
+ assumes A: "\<And>i. i \<in> I \<Longrightarrow> A i \<in> M" "disjoint_family_on A I" "finite I" "\<Union>(A ` I) \<in> M"
+ shows "f (\<Union>(A ` I)) = (\<Sum>i\<in>I. f (A i))"
proof -
have "A`I \<subseteq> M" "disjoint (A`I)" "finite (A`I)" "\<Union>(A`I) \<in> M"
using A by (auto simp: disjoint_family_on_disjoint_image)
@@ -536,7 +536,7 @@
then show "f (A i) = 0"
using volume_empty[OF \<open>volume M f\<close>] by simp
qed (auto intro: \<open>finite I\<close>)
- finally show "f (UNION I A) = (\<Sum>i\<in>I. f (A i))"
+ finally show "f (\<Union>(A ` I)) = (\<Sum>i\<in>I. f (A i))"
by simp
qed
--- a/src/HOL/Analysis/Change_Of_Vars.thy Sun Nov 18 09:51:41 2018 +0100
+++ b/src/HOL/Analysis/Change_Of_Vars.thy Sun Nov 18 18:07:51 2018 +0000
@@ -629,26 +629,26 @@
(*https://en.wikipedia.org/wiki/F\<sigma>_set*)
inductive%important fsigma :: "'a::topological_space set \<Rightarrow> bool" where
- "(\<And>n::nat. closed (F n)) \<Longrightarrow> fsigma (UNION UNIV F)"
+ "(\<And>n::nat. closed (F n)) \<Longrightarrow> fsigma (\<Union>(F ` UNIV))"
inductive%important gdelta :: "'a::topological_space set \<Rightarrow> bool" where
- "(\<And>n::nat. open (F n)) \<Longrightarrow> gdelta (INTER UNIV F)"
+ "(\<And>n::nat. open (F n)) \<Longrightarrow> gdelta (\<Inter>(F ` UNIV))"
lemma%important fsigma_Union_compact:
fixes S :: "'a::{real_normed_vector,heine_borel} set"
- shows "fsigma S \<longleftrightarrow> (\<exists>F::nat \<Rightarrow> 'a set. range F \<subseteq> Collect compact \<and> S = UNION UNIV F)"
+ shows "fsigma S \<longleftrightarrow> (\<exists>F::nat \<Rightarrow> 'a set. range F \<subseteq> Collect compact \<and> S = \<Union>(F ` UNIV))"
proof%unimportant safe
assume "fsigma S"
- then obtain F :: "nat \<Rightarrow> 'a set" where F: "range F \<subseteq> Collect closed" "S = UNION UNIV F"
+ then obtain F :: "nat \<Rightarrow> 'a set" where F: "range F \<subseteq> Collect closed" "S = \<Union>(F ` UNIV)"
by (meson fsigma.cases image_subsetI mem_Collect_eq)
- then have "\<exists>D::nat \<Rightarrow> 'a set. range D \<subseteq> Collect compact \<and> UNION UNIV D = F i" for i
+ then have "\<exists>D::nat \<Rightarrow> 'a set. range D \<subseteq> Collect compact \<and> \<Union>(D ` UNIV) = F i" for i
using closed_Union_compact_subsets [of "F i"]
by (metis image_subsetI mem_Collect_eq range_subsetD)
then obtain D :: "nat \<Rightarrow> nat \<Rightarrow> 'a set"
- where D: "\<And>i. range (D i) \<subseteq> Collect compact \<and> UNION UNIV (D i) = F i"
+ where D: "\<And>i. range (D i) \<subseteq> Collect compact \<and> \<Union>((D i) ` UNIV) = F i"
by metis
let ?DD = "\<lambda>n. (\<lambda>(i,j). D i j) (prod_decode n)"
- show "\<exists>F::nat \<Rightarrow> 'a set. range F \<subseteq> Collect compact \<and> S = UNION UNIV F"
+ show "\<exists>F::nat \<Rightarrow> 'a set. range F \<subseteq> Collect compact \<and> S = \<Union>(F ` UNIV)"
proof (intro exI conjI)
show "range ?DD \<subseteq> Collect compact"
using D by clarsimp (metis mem_Collect_eq rangeI split_conv subsetCE surj_pair)
@@ -663,15 +663,15 @@
qed
next
fix F :: "nat \<Rightarrow> 'a set"
- assume "range F \<subseteq> Collect compact" and "S = UNION UNIV F"
- then show "fsigma (UNION UNIV F)"
+ assume "range F \<subseteq> Collect compact" and "S = \<Union>(F ` UNIV)"
+ then show "fsigma (\<Union>(F ` UNIV))"
by (simp add: compact_imp_closed fsigma.intros image_subset_iff)
qed
lemma%unimportant gdelta_imp_fsigma: "gdelta S \<Longrightarrow> fsigma (- S)"
proof (induction rule: gdelta.induct)
case (1 F)
- have "- INTER UNIV F = (\<Union>i. -(F i))"
+ have "- \<Inter>(F ` UNIV) = (\<Union>i. -(F i))"
by auto
then show ?case
by (simp add: fsigma.intros closed_Compl 1)
@@ -680,7 +680,7 @@
lemma%unimportant fsigma_imp_gdelta: "fsigma S \<Longrightarrow> gdelta (- S)"
proof (induction rule: fsigma.induct)
case (1 F)
- have "- UNION UNIV F = (\<Inter>i. -(F i))"
+ have "- \<Union>(F ` UNIV) = (\<Inter>i. -(F i))"
by auto
then show ?case
by (simp add: 1 gdelta.intros open_closed)
@@ -701,7 +701,7 @@
}
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"
by metis
- let ?C = "UNION UNIV F"
+ let ?C = "\<Union>(F ` UNIV)"
show thesis
proof
show "fsigma ?C"
@@ -3730,13 +3730,13 @@
unfolding Ceq
proof (rule has_absolute_integral_change_of_variables_compact_family)
fix n x
- assume "x \<in> UNION UNIV F"
- then show "(g has_derivative g' x) (at x within UNION UNIV F)"
+ assume "x \<in> \<Union>(F ` UNIV)"
+ then show "(g has_derivative g' x) (at x within \<Union>(F ` UNIV))"
using Ceq \<open>C \<union> N = S\<close> der_g has_derivative_within_subset by blast
next
- have "UNION UNIV F \<subseteq> S"
+ have "\<Union>(F ` UNIV) \<subseteq> S"
using Ceq \<open>C \<union> N = S\<close> by blast
- then show "inj_on g (UNION UNIV F)"
+ then show "inj_on g (\<Union>(F ` UNIV))"
using inj by (meson inj_on_subset)
qed (use F in auto)
moreover
--- a/src/HOL/Analysis/Complete_Measure.thy Sun Nov 18 09:51:41 2018 +0100
+++ b/src/HOL/Analysis/Complete_Measure.thy Sun Nov 18 18:07:51 2018 +0000
@@ -62,9 +62,9 @@
from choice[OF this] guess S ..
from choice[OF this] guess N ..
from choice[OF this] guess N' ..
- then show "UNION UNIV A \<in> ?A"
+ then show "\<Union>(A ` UNIV) \<in> ?A"
using null_sets_UN[of N']
- by (intro completionI[of _ "UNION UNIV S" "UNION UNIV N" "UNION UNIV N'"]) auto
+ by (intro completionI[of _ "\<Union>(S ` UNIV)" "\<Union>(N ` UNIV)" "\<Union>(N' ` UNIV)"]) auto
qed
lemma sets_completion:
@@ -199,7 +199,7 @@
qed
then have "(\<Sum>n. emeasure M (main_part M (A n))) = emeasure M (\<Union>i. main_part M (A i))"
using A by (auto intro!: suminf_emeasure)
- then show "(\<Sum>n. ?\<mu> (A n)) = ?\<mu> (UNION UNIV A)"
+ then show "(\<Sum>n. ?\<mu> (A n)) = ?\<mu> (\<Union>(A ` UNIV))"
by (simp add: completion_def emeasure_main_part_UN[OF A(1)])
qed
qed
--- a/src/HOL/Analysis/Embed_Measure.thy Sun Nov 18 09:51:41 2018 +0100
+++ b/src/HOL/Analysis/Embed_Measure.thy Sun Nov 18 18:07:51 2018 +0000
@@ -401,7 +401,7 @@
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)"
by(simp add: embed_measure_count_space'[symmetric] inj_on_to_nat_on countable nn_integral_embed_measure' measurable_embed_measure1)
also have "\<dots> = ?rhs"
- by(intro arg_cong2[where f="SUPREMUM"] ext nn_integral_cong_AE)(simp_all add: AE_count_space countable)
+ by(intro arg_cong2[where f = "\<lambda>A f. Sup (f ` A)"] ext nn_integral_cong_AE)(simp_all add: AE_count_space countable)
finally show ?thesis .
qed
--- a/src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy Sun Nov 18 09:51:41 2018 +0100
+++ b/src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy Sun Nov 18 18:07:51 2018 +0000
@@ -253,7 +253,7 @@
using \<open>E \<subseteq> space ?L\<close> by (auto simp: space_restrict_space)
then obtain z k where "(z, k) \<in> p" "v \<in> k"
using tagged_division_ofD(6)[OF p(1), symmetric] by auto
- with not show "v \<in> UNION (p - s) snd"
+ with not show "v \<in> \<Union>(snd ` (p - s))"
by (auto intro!: bexI[of _ "(z, k)"] elim: ballE[of _ _ "(z, k)"])
qed (auto intro!: sets.Int sets.finite_UN ennreal_mono_minus intro: p_in_L)
also have "\<dots> = measure ?L (\<Union>x\<in>p \<inter> s. snd x)"
@@ -299,9 +299,9 @@
define B :: "nat \<Rightarrow> 'a set" where "B n = cbox (- real n *\<^sub>R One) (real n *\<^sub>R One)" for n
show "(\<lambda>x. f x * indicator \<Omega> x) \<in> lebesgue \<rightarrow>\<^sub>M borel"
proof (rule measurable_piecewise_restrict)
- have "(\<Union>n. box (- real n *\<^sub>R One) (real n *\<^sub>R One)) \<subseteq> UNION UNIV B"
+ have "(\<Union>n. box (- real n *\<^sub>R One) (real n *\<^sub>R One)) \<subseteq> \<Union>(B ` UNIV)"
unfolding B_def by (intro UN_mono box_subset_cbox order_refl)
- then show "countable (range B)" "space lebesgue \<subseteq> UNION UNIV B"
+ then show "countable (range B)" "space lebesgue \<subseteq> \<Union>(B ` UNIV)"
by (auto simp: B_def UN_box_eq_UNIV)
next
fix \<Omega>' assume "\<Omega>' \<in> range B"
@@ -398,7 +398,7 @@
case (union F)
then have [measurable]: "\<And>i. F i \<in> sets borel"
by (simp add: borel_eq_box subset_eq)
- 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)"
+ 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)"
proof (rule has_integral_monotone_convergence_increasing)
let ?f = "\<lambda>k x. \<Sum>i<k. if x \<in> F i \<inter> box a b then 1 else 0 :: real"
show "\<And>k. (?f k has_integral (\<Sum>i<k. ?M (F i))) (box a b)"
@@ -407,7 +407,7 @@
by (intro sum_mono2) auto
from union(1) have *: "\<And>x i j. x \<in> F i \<Longrightarrow> x \<in> F j \<longleftrightarrow> j = i"
by (auto simp add: disjoint_family_on_def)
- show "\<And>x. (\<lambda>k. ?f k x) \<longlonglongrightarrow> (if x \<in> UNION UNIV F \<inter> box a b then 1 else 0)"
+ show "\<And>x. (\<lambda>k. ?f k x) \<longlonglongrightarrow> (if x \<in> \<Union>(F ` UNIV) \<inter> box a b then 1 else 0)"
apply (auto simp: * sum.If_cases Iio_Int_singleton)
apply (rule_tac k="Suc xa" in LIMSEQ_offset)
apply simp
@@ -1915,7 +1915,7 @@
using S measurable_integrable by blast
have 2: "\<And>n x::'a. indicat_real (S n) x \<le> (indicat_real (S (Suc n)) x)"
by (simp add: indicator_leI nest rev_subsetD)
- have 3: "\<And>x. (\<lambda>n. indicat_real (S n) x) \<longlonglongrightarrow> (indicat_real (UNION UNIV S) x)"
+ have 3: "\<And>x. (\<lambda>n. indicat_real (S n) x) \<longlonglongrightarrow> (indicat_real (\<Union>(S ` UNIV)) x)"
apply (rule Lim_eventually)
apply (simp add: indicator_def)
by (metis eventually_sequentiallyI lift_Suc_mono_le nest subsetCE)
@@ -2046,13 +2046,13 @@
and cov: "\<And>x. x \<in> S \<Longrightarrow> x \<in> U x"
and neg: "\<And>x. x \<in> S \<Longrightarrow> negligible (U x)"
by metis
- obtain \<F> where "\<F> \<subseteq> U ` S" "countable \<F>" and eq: "\<Union>\<F> = UNION S U"
+ obtain \<F> where "\<F> \<subseteq> U ` S" "countable \<F>" and eq: "\<Union>\<F> = \<Union>(U ` S)"
using ope by (force intro: Lindelof_openin [of "U ` S" S])
then have "negligible (\<Union>\<F>)"
by (metis imageE neg negligible_countable_Union subset_eq)
- with eq have "negligible (UNION S U)"
+ with eq have "negligible (\<Union>(U ` S))"
by metis
- moreover have "S \<subseteq> UNION S U"
+ moreover have "S \<subseteq> \<Union>(U ` S)"
using cov by blast
ultimately show "negligible S"
using negligible_subset by blast
@@ -2558,9 +2558,9 @@
using prems by auto
qed
then obtain d K where ddiv: "d division_of \<Union>d" and "K = (\<Sum>k\<in>d. norm (integral k f))"
- "SUPREMUM {d. d division_of \<Union>d} (sum (\<lambda>k. norm (integral k f))) - e < K"
+ "Sup (sum (\<lambda>k. norm (integral k f)) ` {d. d division_of \<Union> d}) - e < K"
by (auto simp add: image_iff not_le)
- then have d: "SUPREMUM {d. d division_of \<Union>d} (sum (\<lambda>k. norm (integral k f))) - e
+ then have d: "Sup (sum (\<lambda>k. norm (integral k f)) ` {d. d division_of \<Union> d}) - e
< (\<Sum>k\<in>d. norm (integral k f))"
by auto
note d'=division_ofD[OF ddiv]
@@ -2917,11 +2917,11 @@
by (metis bounded_linear_image linear_linear assms(1) image_Union range_composition)
have "(\<lambda>n. ?\<mu> (X n)) sums ?\<mu> (\<Union>n. X n)"
by (rule measure_countable_negligible_Union_bounded [OF 1 2 3])
- have meq: "?\<mu> (\<Union>n. f ` X n) = m * ?\<mu> (UNION UNIV X)"
+ have meq: "?\<mu> (\<Union>n. f ` X n) = m * ?\<mu> (\<Union>(X ` UNIV))"
proof (rule sums_unique2 [OF measure_countable_negligible_Union_bounded [OF f1 f2 f3]])
have m: "\<And>n. ?\<mu> (f ` X n) = (m * ?\<mu> (X n))"
using S unfolding bij_betw_def by (metis cbox im rangeI)
- show "(\<lambda>n. ?\<mu> (f ` X n)) sums (m * ?\<mu> (UNION UNIV X))"
+ show "(\<lambda>n. ?\<mu> (f ` X n)) sums (m * ?\<mu> (\<Union>(X ` UNIV)))"
unfolding m
using measure_countable_negligible_Union_bounded [OF 1 2 3] sums_mult by blast
qed
@@ -3679,24 +3679,24 @@
assumes f: "f absolutely_integrable_on (\<Union>(range s))"
and s: "\<And>m. s m \<in> sets lebesgue"
shows "\<And>n. f absolutely_integrable_on (\<Union>m\<le>n. s m)"
- and "(\<lambda>n. integral (\<Union>m\<le>n. s m) f) \<longlonglongrightarrow> integral (UNION UNIV s) f" (is "?F \<longlonglongrightarrow> ?I")
+ and "(\<lambda>n. integral (\<Union>m\<le>n. s m) f) \<longlonglongrightarrow> integral (\<Union>(s ` UNIV)) f" (is "?F \<longlonglongrightarrow> ?I")
proof -
show fU: "f absolutely_integrable_on (\<Union>m\<le>n. s m)" for n
using assms by (blast intro: set_integrable_subset [OF f])
have fint: "f integrable_on (\<Union> (range s))"
using absolutely_integrable_on_def f by blast
- let ?h = "\<lambda>x. if x \<in> UNION UNIV s then norm(f x) else 0"
+ let ?h = "\<lambda>x. if x \<in> \<Union>(s ` UNIV) then norm(f x) else 0"
have "(\<lambda>n. integral UNIV (\<lambda>x. if x \<in> (\<Union>m\<le>n. s m) then f x else 0))
- \<longlonglongrightarrow> integral UNIV (\<lambda>x. if x \<in> UNION UNIV s then f x else 0)"
+ \<longlonglongrightarrow> integral UNIV (\<lambda>x. if x \<in> \<Union>(s ` UNIV) then f x else 0)"
proof (rule dominated_convergence)
show "(\<lambda>x. if x \<in> (\<Union>m\<le>n. s m) then f x else 0) integrable_on UNIV" for n
unfolding integrable_restrict_UNIV
using fU absolutely_integrable_on_def by blast
- show "(\<lambda>x. if x \<in> UNION UNIV s then norm(f x) else 0) integrable_on UNIV"
+ show "(\<lambda>x. if x \<in> \<Union>(s ` UNIV) then norm(f x) else 0) integrable_on UNIV"
by (metis (no_types) absolutely_integrable_on_def f integrable_restrict_UNIV)
show "\<forall>x\<in>UNIV.
(\<lambda>n. if x \<in> (\<Union>m\<le>n. s m) then f x else 0)
- \<longlonglongrightarrow> (if x \<in> UNION UNIV s then f x else 0)"
+ \<longlonglongrightarrow> (if x \<in> \<Union>(s ` UNIV) then f x else 0)"
by (force intro: Lim_eventually eventually_sequentiallyI)
qed auto
then show "?F \<longlonglongrightarrow> ?I"
--- a/src/HOL/Analysis/Extended_Real_Limits.thy Sun Nov 18 09:51:41 2018 +0100
+++ b/src/HOL/Analysis/Extended_Real_Limits.thy Sun Nov 18 18:07:51 2018 +0000
@@ -305,13 +305,13 @@
assume "0 < d" and "\<forall>y. y \<in> S \<longrightarrow> y \<noteq> x \<and> dist y x < d \<longrightarrow> P y"
then have "S \<inter> ball x d - {x} \<subseteq> {x. P x}"
by (auto simp: zero_less_dist_iff dist_commute)
- then show "\<exists>r>0. INFIMUM (Collect P) f \<le> INFIMUM (S \<inter> ball x r - {x}) f"
+ then show "\<exists>r>0. Inf (f ` (Collect P)) \<le> Inf (f ` (S \<inter> ball x r - {x}))"
by (intro exI[of _ d] INF_mono conjI \<open>0 < d\<close>) auto
next
fix d :: real
assume "0 < d"
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>
- INFIMUM (S \<inter> ball x d - {x}) f \<le> INFIMUM (Collect P) f"
+ Inf (f ` (S \<inter> ball x d - {x})) \<le> Inf (f ` (Collect P))"
by (intro exI[of _ "\<lambda>y. y \<in> S \<inter> ball x d - {x}"])
(auto intro!: INF_mono exI[of _ d] simp: dist_commute)
qed
@@ -325,13 +325,13 @@
assume "0 < d" and "\<forall>y. y \<in> S \<longrightarrow> y \<noteq> x \<and> dist y x < d \<longrightarrow> P y"
then have "S \<inter> ball x d - {x} \<subseteq> {x. P x}"
by (auto simp: zero_less_dist_iff dist_commute)
- then show "\<exists>r>0. SUPREMUM (S \<inter> ball x r - {x}) f \<le> SUPREMUM (Collect P) f"
+ then show "\<exists>r>0. Sup (f ` (S \<inter> ball x r - {x})) \<le> Sup (f ` (Collect P))"
by (intro exI[of _ d] SUP_mono conjI \<open>0 < d\<close>) auto
next
fix d :: real
assume "0 < d"
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>
- SUPREMUM (Collect P) f \<le> SUPREMUM (S \<inter> ball x d - {x}) f"
+ Sup (f ` (Collect P)) \<le> Sup (f ` (S \<inter> ball x d - {x}))"
by (intro exI[of _ "\<lambda>y. y \<in> S \<inter> ball x d - {x}"])
(auto intro!: SUP_mono exI[of _ d] simp: dist_commute)
qed
@@ -1055,11 +1055,11 @@
fix P
assume P: "eventually P net"
fix S
- assume S: "mono_set S" "INFIMUM (Collect P) f \<in> S"
+ assume S: "mono_set S" "Inf (f ` (Collect P)) \<in> S"
{
fix x
assume "P x"
- then have "INFIMUM (Collect P) f \<le> f x"
+ then have "Inf (f ` (Collect P)) \<le> f x"
by (intro complete_lattice_class.INF_lower) simp
with S have "f x \<in> S"
by (simp add: mono_set)
@@ -1069,16 +1069,16 @@
next
fix y l
assume S: "\<forall>S. open S \<longrightarrow> mono_set S \<longrightarrow> l \<in> S \<longrightarrow> eventually (\<lambda>x. f x \<in> S) net"
- assume P: "\<forall>P. eventually P net \<longrightarrow> INFIMUM (Collect P) f \<le> y"
+ assume P: "\<forall>P. eventually P net \<longrightarrow> Inf (f ` (Collect P)) \<le> y"
show "l \<le> y"
proof (rule dense_le)
fix B
assume "B < l"
then have "eventually (\<lambda>x. f x \<in> {B <..}) net"
by (intro S[rule_format]) auto
- then have "INFIMUM {x. B < f x} f \<le> y"
+ then have "Inf (f ` {x. B < f x}) \<le> y"
using P by auto
- moreover have "B \<le> INFIMUM {x. B < f x} f"
+ moreover have "B \<le> Inf (f ` {x. B < f x})"
by (intro INF_greatest) auto
ultimately show "B \<le> y"
by simp
@@ -1094,13 +1094,13 @@
fix P
assume P: "eventually P net"
fix S
- assume S: "mono_set (uminus`S)" "SUPREMUM (Collect P) f \<in> S"
+ assume S: "mono_set (uminus`S)" "Sup (f ` (Collect P)) \<in> S"
{
fix x
assume "P x"
- then have "f x \<le> SUPREMUM (Collect P) f"
+ then have "f x \<le> Sup (f ` (Collect P))"
by (intro complete_lattice_class.SUP_upper) simp
- with S(1)[unfolded mono_set, rule_format, of "- SUPREMUM (Collect P) f" "- f x"] S(2)
+ with S(1)[unfolded mono_set, rule_format, of "- Sup (f ` (Collect P))" "- f x"] S(2)
have "f x \<in> S"
by (simp add: inj_image_mem_iff) }
with P show "eventually (\<lambda>x. f x \<in> S) net"
@@ -1108,16 +1108,16 @@
next
fix y l
assume S: "\<forall>S. open S \<longrightarrow> mono_set (uminus ` S) \<longrightarrow> l \<in> S \<longrightarrow> eventually (\<lambda>x. f x \<in> S) net"
- assume P: "\<forall>P. eventually P net \<longrightarrow> y \<le> SUPREMUM (Collect P) f"
+ assume P: "\<forall>P. eventually P net \<longrightarrow> y \<le> Sup (f ` (Collect P))"
show "y \<le> l"
proof (rule dense_ge)
fix B
assume "l < B"
then have "eventually (\<lambda>x. f x \<in> {..< B}) net"
by (intro S[rule_format]) auto
- then have "y \<le> SUPREMUM {x. f x < B} f"
+ then have "y \<le> Sup (f ` {x. f x < B})"
using P by auto
- moreover have "SUPREMUM {x. f x < B} f \<le> B"
+ moreover have "Sup (f ` {x. f x < B}) \<le> B"
by (intro SUP_least) auto
ultimately show "y \<le> B"
by simp
@@ -1240,7 +1240,7 @@
apply (rule INF_eq) using \<open>decseq v\<close> decseq_Suc_iff by auto
moreover have "decseq (\<lambda>n. (SUP m\<in>{n..}. u m))" by (simp add: SUP_subset_mono decseq_def)
ultimately have c: "(INF n\<in>{1..}. (SUP m\<in>{n..}. u m)) = (INF n. (SUP m\<in>{n..}. u m))" by simp
- have "(INF n. SUPREMUM {n..} u) = (INF n. SUP m\<in>{n..}. u (m + 1))" using a b c by simp
+ have "(INF n. Sup (u ` {n..})) = (INF n. SUP m\<in>{n..}. u (m + 1))" using a b c by simp
then show ?thesis by (auto cong: limsup_INF_SUP)
qed
@@ -1264,7 +1264,7 @@
apply (rule SUP_eq) using \<open>incseq v\<close> incseq_Suc_iff by auto
moreover have "incseq (\<lambda>n. (INF m\<in>{n..}. u m))" by (simp add: INF_superset_mono mono_def)
ultimately have c: "(SUP n\<in>{1..}. (INF m\<in>{n..}. u m)) = (SUP n. (INF m\<in>{n..}. u m))" by simp
- have "(SUP n. INFIMUM {n..} u) = (SUP n. INF m\<in>{n..}. u (m + 1))" using a b c by simp
+ have "(SUP n. Inf (u ` {n..})) = (SUP n. INF m\<in>{n..}. u (m + 1))" using a b c by simp
then show ?thesis by (auto cong: liminf_SUP_INF)
qed
@@ -1753,12 +1753,12 @@
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"
moreover have "0 \<le> limsup u - limsup v"
using * by (intro ereal_diff_positive Limsup_mono always_eventually) simp
- moreover have "0 \<le> (SUPREMUM {x..} v)" for x
+ moreover have "0 \<le> Sup (u ` {x..})" for x
using * by (intro SUP_upper2[of x]) auto
- moreover have "0 \<le> (SUPREMUM {x..} u)" for x
+ moreover have "0 \<le> Sup (v ` {x..})" for x
using * by (intro SUP_upper2[of x]) auto
ultimately show "(SUP n. INF n\<in>{n..}. max 0 (u n - v n))
- \<le> max 0 ((INF x. max 0 (SUPREMUM {x..} u)) - (INF x. max 0 (SUPREMUM {x..} v)))"
+ \<le> max 0 ((INF x. max 0 (Sup (u ` {x..}))) - (INF x. max 0 (Sup (v ` {x..}))))"
by (auto simp: * ereal_diff_positive max.absorb2 liminf_SUP_INF[symmetric] limsup_INF_SUP[symmetric] ereal_liminf_limsup_minus)
qed
--- a/src/HOL/Analysis/Finite_Product_Measure.thy Sun Nov 18 09:51:41 2018 +0100
+++ b/src/HOL/Analysis/Finite_Product_Measure.thy Sun Nov 18 18:07:51 2018 +0000
@@ -779,7 +779,7 @@
show ?case
proof (intro exI[of _ "\<Union>i. J i"] bexI[of _ "\<Union>i. prod_emb (\<Union>i. J i) M (J i) (X i)"] conjI)
show "(\<Union>i. J i) \<subseteq> I" "countable (\<Union>i. J i)" using J by auto
- 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))"
+ 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))"
by (simp add: K[abs_def] SUP_upper)
qed(auto intro: X)
qed
--- a/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy Sun Nov 18 09:51:41 2018 +0100
+++ b/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy Sun Nov 18 18:07:51 2018 +0000
@@ -5635,15 +5635,15 @@
using qq by auto
show "\<And>i1 i2. \<lbrakk>i1 \<in> r; i2 \<in> r; i1 \<noteq> i2\<rbrakk> \<Longrightarrow> interior i1 \<inter> interior i2 = {}"
by (simp add: q'(5) r_def)
- show "interior (UNION p snd) \<inter> interior (\<Union>r) = {}"
+ show "interior (\<Union>(snd ` p)) \<inter> interior (\<Union>r) = {}"
proof (rule Int_interior_Union_intervals [OF \<open>finite r\<close>])
- show "open (interior (UNION p snd))"
+ show "open (interior (\<Union>(snd ` p)))"
by blast
show "\<And>T. T \<in> r \<Longrightarrow> \<exists>a b. T = cbox a b"
by (simp add: q'(4) r_def)
have "finite (snd ` p)"
by (simp add: p'(1))
- then show "\<And>T. T \<in> r \<Longrightarrow> interior (UNION p snd) \<inter> interior T = {}"
+ then show "\<And>T. T \<in> r \<Longrightarrow> interior (\<Union>(snd ` p)) \<inter> interior T = {}"
apply (subst Int_commute)
apply (rule Int_interior_Union_intervals)
using r_def q'(5) q(1) apply auto
@@ -5672,7 +5672,7 @@
then show "content L *\<^sub>R f x = 0"
unfolding uv content_eq_0_interior[symmetric] by auto
qed
- show "finite (UNION r qq)"
+ show "finite (\<Union>(qq ` r))"
by (meson finite_UN qq \<open>finite r\<close> tagged_division_of_finite)
qed
moreover have "content M *\<^sub>R f x = 0"
--- a/src/HOL/Analysis/Homeomorphism.thy Sun Nov 18 09:51:41 2018 +0100
+++ b/src/HOL/Analysis/Homeomorphism.thy Sun Nov 18 18:07:51 2018 +0000
@@ -1020,13 +1020,13 @@
tv: "\<And>x. x \<in> S
\<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)"
by metis
- then have o: "open (UNION S t)"
+ then have o: "open (\<Union>(t ` S))"
by blast
have "S = \<Union> (v ` S)"
using tv by blast
- also have "... = UNION S t \<inter> closure S"
+ also have "... = \<Union>(t ` S) \<inter> closure S"
proof
- show "UNION S v \<subseteq> UNION S t \<inter> closure S"
+ show "\<Union>(v ` S) \<subseteq> \<Union>(t ` S) \<inter> closure S"
apply safe
apply (metis Int_iff subsetD UN_iff tv)
apply (simp add: closure_def rev_subsetD tv)
@@ -1039,10 +1039,10 @@
by (metis Int_commute closure_minimal compact_imp_closed that tv)
finally show ?thesis .
qed
- then show "UNION S t \<inter> closure S \<subseteq> UNION S v"
+ then show "\<Union>(t ` S) \<inter> closure S \<subseteq> \<Union>(v ` S)"
by blast
qed
- finally have e: "S = UNION S t \<inter> closure S" .
+ finally have e: "S = \<Union>(t ` S) \<inter> closure S" .
show ?thesis
by (rule that [OF o e])
qed
@@ -1624,7 +1624,7 @@
by (metis (no_types, lifting) finite_subset_image)
then have "tk \<noteq> {}"
by auto
- define n where "n = INTER tk NN"
+ define n where "n = \<Inter>(NN ` tk)"
have "y \<in> n" "open n"
using inUS NN \<open>tk \<subseteq> {0..1}\<close> \<open>finite tk\<close>
by (auto simp: n_def open_INT subset_iff)
@@ -1632,7 +1632,7 @@
proof (rule Lebesgue_number_lemma [of "{0..1}" "K ` tk"])
show "K ` tk \<noteq> {}"
using \<open>tk \<noteq> {}\<close> by auto
- show "{0..1} \<subseteq> UNION tk K"
+ show "{0..1} \<subseteq> \<Union>(K ` tk)"
using tk by auto
show "\<And>B. B \<in> K ` tk \<Longrightarrow> open B"
using \<open>tk \<subseteq> {0..1}\<close> K by auto
--- a/src/HOL/Analysis/Improper_Integral.thy Sun Nov 18 09:51:41 2018 +0100
+++ b/src/HOL/Analysis/Improper_Integral.thy Sun Nov 18 18:07:51 2018 +0000
@@ -793,7 +793,7 @@
proof (rule sum_content_area_over_thin_division)
show "snd ` S division_of \<Union>(snd ` S)"
by (auto intro: S tagged_partial_division_of_Union_self division_of_tagged_division)
- show "UNION S snd \<subseteq> cbox a b"
+ show "\<Union>(snd ` S) \<subseteq> cbox a b"
using S by force
show "a \<bullet> i \<le> c \<bullet> i" "c \<bullet> i \<le> b \<bullet> i"
using mem_box(2) that by blast+
@@ -987,7 +987,7 @@
proof -
obtain u v where uv: "L = cbox u v"
using T'_tagged \<open>(x, L) \<in> A\<close> \<open>A \<subseteq> T''\<close> \<open>T'' \<subseteq> T'\<close> by blast
- have "A tagged_division_of UNION A snd"
+ have "A tagged_division_of \<Union>(snd ` A)"
using A_tagged tagged_partial_division_of_Union_self by auto
then have "interior (K \<inter> {x. x \<bullet> i \<le> c}) = {}"
apply (rule tagged_division_split_left_inj [OF _ \<open>(x,K) \<in> A\<close> \<open>(x,L) \<in> A\<close>])
@@ -1016,7 +1016,7 @@
proof -
obtain u v where uv: "L = cbox u v"
using T'_tagged \<open>(x, L) \<in> B\<close> \<open>B \<subseteq> T''\<close> \<open>T'' \<subseteq> T'\<close> by blast
- have "B tagged_division_of UNION B snd"
+ have "B tagged_division_of \<Union>(snd ` B)"
using B_tagged tagged_partial_division_of_Union_self by auto
then have "interior (K \<inter> {x. c \<le> x \<bullet> i}) = {}"
apply (rule tagged_division_split_right_inj [OF _ \<open>(x,K) \<in> B\<close> \<open>(x,L) \<in> B\<close>])
--- a/src/HOL/Analysis/Measure_Space.thy Sun Nov 18 09:51:41 2018 +0100
+++ b/src/HOL/Analysis/Measure_Space.thy Sun Nov 18 18:07:51 2018 +0000
@@ -317,7 +317,7 @@
(\<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))"
unfolding countably_additive_def
proof safe
- 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)"
+ 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))"
fix A :: "nat \<Rightarrow> 'a set" assume A: "range A \<subseteq> M" "incseq A" "(\<Union>i. A i) \<in> M"
then have dA: "range (disjointed A) \<subseteq> M" by (auto simp: range_disjointed_sets)
with count_sum[THEN spec, of "disjointed A"] A(3)
@@ -1834,7 +1834,7 @@
using I
proof (induction I rule: finite_induct)
case (insert x I)
- have "measure M (F x \<union> UNION I F) = measure M (F x) + measure M (UNION I F)"
+ have "measure M (F x \<union> \<Union>(F ` I)) = measure M (F x) + measure M (\<Union>(F ` I))"
by (rule measure_Un_AE) (use insert in \<open>auto simp: pairwise_insert\<close>)
with insert show ?case
by (simp add: pairwise_insert )
@@ -3132,7 +3132,7 @@
lemma le_measureD3: "A \<le> B \<Longrightarrow> sets A = sets B \<Longrightarrow> emeasure A X \<le> emeasure B X"
by (auto simp: le_measure_iff le_fun_def dest: sets_eq_imp_space_eq split: if_split_asm)
-lemma UN_space_closed: "UNION S sets \<subseteq> Pow (UNION S space)"
+lemma UN_space_closed: "\<Union>(sets ` S) \<subseteq> Pow (\<Union>(space ` S))"
using sets.space_closed by auto
definition Sup_lexord :: "('a \<Rightarrow> 'b::complete_lattice) \<Rightarrow> ('a set \<Rightarrow> 'a) \<Rightarrow> ('a set \<Rightarrow> 'a) \<Rightarrow> 'a set \<Rightarrow> 'a"
@@ -3245,10 +3245,10 @@
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)"
by (safe intro!: bexI[of _ "i \<union> j"]) auto
next
- 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))"
+ 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)))"
proof (intro SUP_cong refl)
fix i assume i: "i \<in> {P. finite P \<and> P \<subseteq> M}"
- show "(\<Sum>n. ?\<mu> i (F n)) = ?\<mu> i (UNION UNIV F)"
+ show "(\<Sum>n. ?\<mu> i (F n)) = ?\<mu> i (\<Union>(F ` UNIV))"
proof cases
assume "i \<noteq> {}" with i ** show ?thesis
apply (intro suminf_emeasure \<open>disjoint_family F\<close>)
@@ -3294,9 +3294,9 @@
next
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}"
and neq: "\<And>aa. aa \<in> S \<Longrightarrow> sets aa \<noteq> (\<Union>a\<in>S. sets a)"
- have sp_a: "space a = (UNION S space)"
+ have sp_a: "space a = (\<Union>(space ` S))"
using \<open>a\<in>A\<close> by (auto simp: S)
- show "x \<le> sigma (UNION S space) (UNION S sets)"
+ show "x \<le> sigma (\<Union>(space ` S)) (\<Union>(sets ` S))"
proof cases
assume [simp]: "space x = space a"
have "sets x \<subset> (\<Union>a\<in>S. sets a)"
@@ -3363,19 +3363,19 @@
unfolding Sup_measure_def
proof (intro Sup_lexord[where P="\<lambda>y. y \<le> x"])
assume "\<And>a. a \<in> A \<Longrightarrow> space a \<noteq> (\<Union>a\<in>A. space a)"
- show "sigma (UNION A space) {} \<le> x"
+ show "sigma (\<Union>(space ` A)) {} \<le> x"
using x[THEN le_measureD1] by (subst sigma_le_iff) auto
next
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}"
"\<And>a. a \<in> S \<Longrightarrow> sets a \<noteq> (\<Union>a\<in>S. sets a)"
- have "UNION S space \<subseteq> space x"
+ have "\<Union>(space ` S) \<subseteq> space x"
using S le_measureD1[OF x] by auto
moreover
- have "UNION S space = space a"
+ have "\<Union>(space ` S) = space a"
using \<open>a\<in>A\<close> S by auto
- then have "space x = UNION S space \<Longrightarrow> UNION S sets \<subseteq> sets x"
+ then have "space x = \<Union>(space ` S) \<Longrightarrow> \<Union>(sets ` S) \<subseteq> sets x"
using \<open>a \<in> A\<close> le_measureD2[OF x] by (auto simp: S)
- ultimately show "sigma (UNION S space) (UNION S sets) \<le> x"
+ ultimately show "sigma (\<Union>(space ` S)) (\<Union>(sets ` S)) \<le> x"
by (subst sigma_le_iff) simp_all
next
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}"
@@ -3504,17 +3504,17 @@
assumes ch: "Complete_Partial_Order.chain (\<le>) (M ` A)" and "A \<noteq> {}"
shows "emeasure (SUP i\<in>A. M i) X = (SUP i\<in>A. emeasure (M i) X)"
proof (subst emeasure_SUP[OF sets \<open>A \<noteq> {}\<close>])
- 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)"
+ 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)"
proof (rule SUP_eq)
fix J assume "J \<in> {J. J \<noteq> {} \<and> finite J \<and> J \<subseteq> A}"
then have J: "Complete_Partial_Order.chain (\<le>) (M ` J)" "finite J" "J \<noteq> {}" and "J \<subseteq> A"
using ch[THEN chain_subset, of "M`J"] by auto
with in_chain_finite[OF J(1)] obtain j where "j \<in> J" "(SUP j\<in>J. M j) = M j"
by auto
- with \<open>J \<subseteq> A\<close> show "\<exists>j\<in>A. emeasure (SUPREMUM J M) X \<le> emeasure (M j) X"
+ with \<open>J \<subseteq> A\<close> show "\<exists>j\<in>A. emeasure (Sup (M ` J)) X \<le> emeasure (M j) X"
by auto
next
- 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"
+ 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"
by (intro bexI[of _ "{j}"]) auto
qed
qed
@@ -3584,7 +3584,7 @@
assumes "\<And>m. m \<in> M \<Longrightarrow> sets m \<subseteq> sets N"
shows "sets (Sup M) \<subseteq> sets N"
proof -
- have *: "UNION M space = space N"
+ have *: "\<Union>(space ` M) = space N"
using assms by auto
show ?thesis
unfolding * using assms by (subst sets_Sup_eq[of M "space N"]) (auto intro!: sets.sigma_sets_subset)
@@ -3612,7 +3612,7 @@
by (intro const_space \<open>m \<in> M\<close>)
have "f \<in> measurable N (sigma (\<Union>m\<in>M. space m) (\<Union>m\<in>M. sets m))"
proof (rule measurable_measure_of)
- show "f \<in> space N \<rightarrow> UNION M space"
+ show "f \<in> space N \<rightarrow> \<Union>(space ` M)"
using measurable_space[OF f] M by auto
qed (auto intro: measurable_sets f dest: sets.sets_into_space)
also have "measurable N (sigma (\<Union>m\<in>M. space m) (\<Union>m\<in>M. sets m)) = measurable N (Sup M)"
--- a/src/HOL/Analysis/Nonnegative_Lebesgue_Integration.thy Sun Nov 18 09:51:41 2018 +0100
+++ b/src/HOL/Analysis/Nonnegative_Lebesgue_Integration.thy Sun Nov 18 18:07:51 2018 +0000
@@ -821,12 +821,12 @@
lemma nn_integral_def_finite:
"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)"
- (is "_ = SUPREMUM ?A ?f")
+ (is "_ = Sup (?A ` ?f)")
unfolding nn_integral_def
proof (safe intro!: antisym SUP_least)
fix g assume g[measurable]: "simple_function M g" "g \<le> f"
- show "integral\<^sup>S M g \<le> SUPREMUM ?A ?f"
+ show "integral\<^sup>S M g \<le> Sup (?A ` ?f)"
proof cases
assume ae: "AE x in M. g x \<noteq> top"
let ?G = "{x \<in> space M. g x \<noteq> top}"
@@ -835,7 +835,7 @@
show "AE x in M. g x = g x * indicator ?G x"
using ae AE_space by eventually_elim auto
qed (insert g, auto)
- also have "\<dots> \<le> SUPREMUM ?A ?f"
+ also have "\<dots> \<le> Sup (?A ` ?f)"
using g by (intro SUP_upper) (auto simp: le_fun_def less_top split: split_indicator)
finally show ?thesis .
next
@@ -844,7 +844,7 @@
by (subst (asm) AE_iff_measurable[OF _ refl]) auto
then have "top = (SUP n. (\<integral>\<^sup>Sx. of_nat n * indicator ?G x \<partial>M))"
by (simp add: ennreal_SUP_of_nat_eq_top ennreal_top_eq_mult_iff SUP_mult_right_ennreal[symmetric])
- also have "\<dots> \<le> SUPREMUM ?A ?f"
+ also have "\<dots> \<le> Sup (?A ` ?f)"
using g
by (safe intro!: SUP_least SUP_upper)
(auto simp: le_fun_def of_nat_less_top top_unique[symmetric] split: split_indicator
@@ -990,7 +990,7 @@
unfolding sup_continuous_def
proof safe
fix C :: "nat \<Rightarrow> 'b" assume C: "incseq C"
- 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)"
+ 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)"
unfolding sup_continuousD[OF f C]
by (subst nn_integral_monotone_convergence_SUP) (auto simp: mono_def le_fun_def)
qed
@@ -1013,7 +1013,7 @@
using f N(3) by (intro measurable_If_set) auto }
qed
also have "\<dots> = (SUP i. (\<integral>\<^sup>+ x. f i x \<partial>M))"
- using f_eq by (force intro!: arg_cong[where f="SUPREMUM UNIV"] nn_integral_cong_AE ext)
+ using f_eq by (force intro!: arg_cong[where f = "\<lambda>f. Sup (range f)"] nn_integral_cong_AE ext)
finally show ?thesis .
qed
@@ -1027,7 +1027,7 @@
and g: "incseq g" "\<And>i. simple_function M (g i)"
and eq: "AE x in M. (SUP i. f i x) = (SUP i. g i x)"
shows "(SUP i. integral\<^sup>S M (f i)) = (SUP i. integral\<^sup>S M (g i))"
- (is "SUPREMUM _ ?F = SUPREMUM _ ?G")
+ (is "Sup (?F ` _) = Sup (?G ` _)")
proof -
have "(SUP i. integral\<^sup>S M (f i)) = (\<integral>\<^sup>+x. (SUP i. f i x) \<partial>M)"
using f by (rule nn_integral_monotone_convergence_simple)
@@ -1414,7 +1414,7 @@
unfolding inf_continuous_def
proof safe
fix C :: "nat \<Rightarrow> 'b" assume C: "decseq C"
- then show "(\<integral>\<^sup>+ y. f y (INFIMUM UNIV C) \<partial>M) = (INF i. \<integral>\<^sup>+ y. f y (C i) \<partial>M)"
+ then show "(\<integral>\<^sup>+ y. f y (Inf (C ` UNIV)) \<partial>M) = (INF i. \<integral>\<^sup>+ y. f y (C i) \<partial>M)"
using inf_continuous_mono[OF f] bnd
by (auto simp add: inf_continuousD[OF f C] fun_eq_iff antimono_def mono_def le_fun_def less_top
intro!: nn_integral_monotone_convergence_INF_decseq)
@@ -1609,7 +1609,7 @@
cong del: if_weak_cong intro!: monoD[OF inf_continuous_mono[OF g], THEN le_funD])
next
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"
- with bound show "INFIMUM UNIV C \<in> borel_measurable N \<and> (\<forall>s. integral\<^sup>N (M s) (INFIMUM UNIV C) < \<infinity>)"
+ with bound show "Inf (C ` UNIV) \<in> borel_measurable N \<and> (\<forall>s. integral\<^sup>N (M s) (Inf (C ` UNIV)) < \<infinity>)"
unfolding INF_apply[abs_def]
by (subst nn_integral_monotone_convergence_INF_decseq)
(auto simp: INF_less_iff cong: measurable_cong_sets intro!: borel_measurable_INF)
@@ -1801,11 +1801,11 @@
lemma emeasure_UN_countable:
assumes sets[measurable]: "\<And>i. i \<in> I \<Longrightarrow> X i \<in> sets M" and I[simp]: "countable I"
assumes disj: "disjoint_family_on X I"
- shows "emeasure M (UNION I X) = (\<integral>\<^sup>+i. emeasure M (X i) \<partial>count_space I)"
+ shows "emeasure M (\<Union>(X ` I)) = (\<integral>\<^sup>+i. emeasure M (X i) \<partial>count_space I)"
proof -
- have eq: "\<And>x. indicator (UNION I X) x = \<integral>\<^sup>+ i. indicator (X i) x \<partial>count_space I"
+ have eq: "\<And>x. indicator (\<Union>(X ` I)) x = \<integral>\<^sup>+ i. indicator (X i) x \<partial>count_space I"
proof cases
- fix x assume x: "x \<in> UNION I X"
+ fix x assume x: "x \<in> \<Union>(X ` I)"
then obtain j where j: "x \<in> X j" "j \<in> I"
by auto
with disj have "\<And>i. i \<in> I \<Longrightarrow> indicator (X i) x = (indicator {j} i::ennreal)"
@@ -1815,7 +1815,7 @@
qed (auto simp: nn_integral_0_iff_AE)
note sets.countable_UN'[unfolded subset_eq, measurable]
- have "emeasure M (UNION I X) = (\<integral>\<^sup>+x. indicator (UNION I X) x \<partial>M)"
+ have "emeasure M (\<Union>(X ` I)) = (\<integral>\<^sup>+x. indicator (\<Union>(X ` I)) x \<partial>M)"
by simp
also have "\<dots> = (\<integral>\<^sup>+i. \<integral>\<^sup>+x. indicator (X i) x \<partial>M \<partial>count_space I)"
by (simp add: eq nn_integral_count_space_nn_integral)
--- a/src/HOL/Analysis/Path_Connected.thy Sun Nov 18 09:51:41 2018 +0100
+++ b/src/HOL/Analysis/Path_Connected.thy Sun Nov 18 18:07:51 2018 +0000
@@ -5272,7 +5272,7 @@
by metis
then obtain T where T: "T \<subseteq> k" "finite T" "k \<subseteq> \<Union>((\<lambda>x. k \<inter> u x) ` T)"
by (metis finite_subset_image)
- have Tuv: "UNION T u \<subseteq> UNION T v"
+ have Tuv: "\<Union>(u ` T) \<subseteq> \<Union>(v ` T)"
using T that by (force simp: dest!: uv)
show ?thesis
apply (rule_tac x="\<Union>(u ` T)" in exI)
--- a/src/HOL/Analysis/Polytope.thy Sun Nov 18 09:51:41 2018 +0100
+++ b/src/HOL/Analysis/Polytope.thy Sun Nov 18 18:07:51 2018 +0000
@@ -3232,7 +3232,7 @@
have TU: "convex (T \<inter> U)"
by (simp add: \<open>convex T\<close> \<open>convex U\<close> convex_Int)
have "(\<Union>x\<in>T. closed_segment z x) \<inter> (\<Union>x\<in>U. closed_segment z x)
- \<subseteq> (if T \<inter> U = {} then {z} else UNION (T \<inter> U) (closed_segment z))" (is "_ \<subseteq> ?IF")
+ \<subseteq> (if T \<inter> U = {} then {z} else \<Union>((closed_segment z) ` (T \<inter> U)))" (is "_ \<subseteq> ?IF")
proof clarify
fix x t u
assume xt: "x \<in> closed_segment z t"
--- a/src/HOL/Analysis/Set_Integral.thy Sun Nov 18 09:51:41 2018 +0100
+++ b/src/HOL/Analysis/Set_Integral.thy Sun Nov 18 18:07:51 2018 +0000
@@ -368,7 +368,7 @@
using assms
proof%unimportant induction
case (insert x F)
- then have "A x \<inter> UNION F A = {}"
+ then have "A x \<inter> \<Union>(A ` F) = {}"
by (meson disjoint_family_on_insert)
with insert show ?case
by (simp add: set_integral_Un set_integrable_Un set_integrable_UN disjoint_family_on_insert)
@@ -453,7 +453,7 @@
set_lebesgue_integral M (\<Union>i. A i) (\<lambda>x. norm (f x))"
by simp
qed
- 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)"
+ 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)"
apply (rule Bochner_Integration.integral_cong[OF refl])
apply (subst suminf_scaleR_left[OF sums_summable[OF indicator_sums, OF disj], symmetric])
using sums_unique[OF indicator_sums[OF disj]]
@@ -472,7 +472,7 @@
using intgbl by (rule set_integrable_subset) auto
show "\<And>i. (\<lambda>x. indicator (A i) x *\<^sub>R f x) \<in> borel_measurable M"
using int_A integrable_iff_bounded set_integrable_def by blast
- show "(\<lambda>x. indicator (UNION UNIV A) x *\<^sub>R f x) \<in> borel_measurable M"
+ show "(\<lambda>x. indicator (\<Union>(A ` UNIV)) x *\<^sub>R f x) \<in> borel_measurable M"
using integrable_iff_bounded intgbl set_integrable_def by blast
show "integrable M (\<lambda>x. indicator (\<Union>i. A i) x *\<^sub>R norm (f x))"
using int_A intgbl integrable_norm unfolding set_integrable_def
@@ -501,7 +501,7 @@
by force
have "set_integrable M (\<Inter>i. A i) f"
using int0 by (rule set_integrable_subset) (insert A, auto simp: decseq_def)
- with int_A show "(\<lambda>x. indicat_real (INTER UNIV A) x *\<^sub>R f x) \<in> borel_measurable M"
+ with int_A show "(\<lambda>x. indicat_real (\<Inter>(A ` UNIV)) x *\<^sub>R f x) \<in> borel_measurable M"
"\<And>i. (\<lambda>x. indicat_real (A i) x *\<^sub>R f x) \<in> borel_measurable M"
by (auto simp: set_integrable_def)
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)"
--- a/src/HOL/Analysis/Sigma_Algebra.thy Sun Nov 18 09:51:41 2018 +0100
+++ b/src/HOL/Analysis/Sigma_Algebra.thy Sun Nov 18 18:07:51 2018 +0000
@@ -841,7 +841,7 @@
using assms by (induct A) (auto simp: disjoint_def intro!: generated_ring_disjoint_Un generated_ring_empty)
lemma (in semiring_of_sets) generated_ring_disjoint_UNION:
- "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"
+ "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"
by (intro generated_ring_disjoint_Union) auto
lemma (in semiring_of_sets) generated_ring_Int:
@@ -879,7 +879,7 @@
using assms by (induct A rule: finite_ne_induct) (auto intro: generated_ring_Int)
lemma (in semiring_of_sets) generated_ring_INTER:
- "finite I \<Longrightarrow> I \<noteq> {} \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> A i \<in> generated_ring) \<Longrightarrow> INTER I A \<in> generated_ring"
+ "finite I \<Longrightarrow> I \<noteq> {} \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> A i \<in> generated_ring) \<Longrightarrow> \<Inter>(A ` I) \<in> generated_ring"
by (intro generated_ring_Inter) auto
lemma (in semiring_of_sets) generating_ring:
--- a/src/HOL/Analysis/Starlike.thy Sun Nov 18 09:51:41 2018 +0100
+++ b/src/HOL/Analysis/Starlike.thy Sun Nov 18 18:07:51 2018 +0000
@@ -7494,9 +7494,9 @@
and clos: "closure (G x) \<subseteq> F x" and Fin: "F x \<in> \<C>"
if "x \<in> S" for x
by metis
- then obtain \<F> where "\<F> \<subseteq> G ` S" "countable \<F>" "\<Union>\<F> = UNION S G"
+ then obtain \<F> where "\<F> \<subseteq> G ` S" "countable \<F>" "\<Union>\<F> = \<Union>(G ` S)"
using Lindelof [of "G ` S"] by (metis image_iff)
- then obtain K where K: "K \<subseteq> S" "countable K" and eq: "UNION K G = UNION S G"
+ then obtain K where K: "K \<subseteq> S" "countable K" and eq: "\<Union>(G ` K) = \<Union>(G ` S)"
by (metis countable_subset_image)
with False Gin have "K \<noteq> {}" by force
then obtain a :: "nat \<Rightarrow> 'a" where "range a = K"
@@ -7885,7 +7885,7 @@
obtain I where "finite I" and I: "K \<subseteq> (\<Union>i\<in>I. interior (f i))"
proof (rule compactE_image [OF \<open>compact K\<close>])
show "K \<subseteq> (\<Union>n. interior (f n))"
- using \<open>K \<subseteq> S\<close> \<open>UNION UNIV f = S\<close> * by blast
+ using \<open>K \<subseteq> S\<close> \<open>\<Union>(f ` UNIV) = S\<close> * by blast
qed auto
{ fix n
assume n: "Max I \<le> n"
--- a/src/HOL/Analysis/Topology_Euclidean_Space.thy Sun Nov 18 09:51:41 2018 +0100
+++ b/src/HOL/Analysis/Topology_Euclidean_Space.thy Sun Nov 18 18:07:51 2018 +0000
@@ -440,8 +440,8 @@
show ?case by (intro exI[of _ "{{}}"]) simp
next
case (Int a b)
- then obtain x y where x: "a = UNION x Inter" "\<And>i. i \<in> x \<Longrightarrow> finite i \<and> i \<subseteq> B"
- and y: "b = UNION y Inter" "\<And>i. i \<in> y \<Longrightarrow> finite i \<and> i \<subseteq> B"
+ then obtain x y where x: "a = \<Union>(Inter ` x)" "\<And>i. i \<in> x \<Longrightarrow> finite i \<and> i \<subseteq> B"
+ and y: "b = \<Union>(Inter ` y)" "\<And>i. i \<in> y \<Longrightarrow> finite i \<and> i \<subseteq> B"
by blast
show ?case
unfolding x y Int_UN_distrib2
@@ -450,10 +450,10 @@
case (UN K)
then have "\<forall>k\<in>K. \<exists>B'\<subseteq>{b. finite b \<and> b \<subseteq> B}. UNION B' Inter = k" by auto
then obtain k where
- "\<forall>ka\<in>K. k ka \<subseteq> {b. finite b \<and> b \<subseteq> B} \<and> UNION (k ka) Inter = ka"
+ "\<forall>ka\<in>K. k ka \<subseteq> {b. finite b \<and> b \<subseteq> B} \<and> \<Union>(Inter ` (k ka)) = ka"
unfolding bchoice_iff ..
then show "\<exists>B'\<subseteq>{b. finite b \<and> b \<subseteq> B}. UNION B' Inter = \<Union>K"
- by (intro exI[of _ "UNION K k"]) auto
+ by (intro exI[of _ "\<Union>(k ` K)"]) auto
next
case (Basis S)
then show ?case
--- a/src/HOL/Analysis/Uniform_Limit.thy Sun Nov 18 09:51:41 2018 +0100
+++ b/src/HOL/Analysis/Uniform_Limit.thy Sun Nov 18 18:07:51 2018 +0000
@@ -654,7 +654,7 @@
lemma uniform_limit_on_UNION:
assumes "finite S"
assumes "\<And>s. s \<in> S \<Longrightarrow> uniform_limit (h s) f g F"
- shows "uniform_limit (UNION S h) f g F"
+ shows "uniform_limit (\<Union>(h ` S)) f g F"
using assms
by induct (auto intro: uniform_limit_on_empty uniform_limit_on_Un)
--- a/src/HOL/Analysis/Vitali_Covering_Theorem.thy Sun Nov 18 09:51:41 2018 +0100
+++ b/src/HOL/Analysis/Vitali_Covering_Theorem.thy Sun Nov 18 18:07:51 2018 +0000
@@ -617,13 +617,13 @@
by (metis mult.commute mult.left_neutral real_mult_le_cancel_iff1 \<open>e > 0\<close> le1)
finally show ?thesis .
qed
- have "UNION C U \<in> lmeasurable" "?\<mu> (\<Union>(U ` C)) \<le> e"
+ have "\<Union>(U ` C) \<in> lmeasurable" "?\<mu> (\<Union>(U ` C)) \<le> e"
using \<open>e > 0\<close> Um lee
by(auto intro!: fmeasurable_UN_bound [OF \<open>countable C\<close>] measure_UN_bound [OF \<open>countable C\<close>])
}
- moreover have "?\<mu> ?T = ?\<mu> (UNION C U)"
- proof (rule measure_negligible_symdiff [OF \<open>UNION C U \<in> lmeasurable\<close>])
- show "negligible((UNION C U - ?T) \<union> (?T - UNION C U))"
+ moreover have "?\<mu> ?T = ?\<mu> (\<Union>(U ` C))"
+ proof (rule measure_negligible_symdiff [OF \<open>\<Union>(U ` C) \<in> lmeasurable\<close>])
+ show "negligible((\<Union>(U ` C) - ?T) \<union> (?T - \<Union>(U ` C)))"
by (force intro!: negligible_subset [OF negC])
qed
ultimately show "?T \<in> lmeasurable" "?\<mu> ?T \<le> e"
--- a/src/HOL/Bali/Basis.thy Sun Nov 18 09:51:41 2018 +0100
+++ b/src/HOL/Bali/Basis.thy Sun Nov 18 18:07:51 2018 +0000
@@ -87,14 +87,13 @@
by auto
lemma finite_SetCompr2:
- "finite (Collect P) \<Longrightarrow> \<forall>y. P y \<longrightarrow> finite (range (f y)) \<Longrightarrow>
- finite {f y x |x y. P y}"
- apply (subgoal_tac "{f y x |x y. P y} = UNION (Collect P) (\<lambda>y. range (f y))")
- prefer 2 apply fast
- apply (erule ssubst)
- apply (erule finite_UN_I)
- apply fast
- done
+ "finite {f y x |x y. P y}" if "finite (Collect P)"
+ "\<forall>y. P y \<longrightarrow> finite (range (f y))"
+proof -
+ have "{f y x |x y. P y} = (\<Union>y\<in>Collect P. range (f y))"
+ by auto
+ with that show ?thesis by simp
+qed
lemma list_all2_trans: "\<forall>a b c. P1 a b \<longrightarrow> P2 b c \<longrightarrow> P3 a c \<Longrightarrow>
\<forall>xs2 xs3. list_all2 P1 xs1 xs2 \<longrightarrow> list_all2 P2 xs2 xs3 \<longrightarrow> list_all2 P3 xs1 xs3"
--- a/src/HOL/Computational_Algebra/Primes.thy Sun Nov 18 09:51:41 2018 +0100
+++ b/src/HOL/Computational_Algebra/Primes.thy Sun Nov 18 18:07:51 2018 +0000
@@ -756,7 +756,7 @@
lemma prime_factors_prod:
assumes "finite A" and "0 \<notin> f ` A"
- shows "prime_factors (prod f A) = UNION A (prime_factors \<circ> f)"
+ shows "prime_factors (prod f A) = \<Union>((prime_factors \<circ> f) ` A)"
using assms by (simp add: prod_unfold_prod_mset prime_factorization_prod_mset)
lemma prime_factors_fact:
--- a/src/HOL/Decision_Procs/MIR.thy Sun Nov 18 09:51:41 2018 +0100
+++ b/src/HOL/Decision_Procs/MIR.thy Sun Nov 18 18:07:51 2018 +0000
@@ -3377,22 +3377,23 @@
proof-
fix M :: "('a\<times>'b\<times>'c) set" and f :: "('a\<times>'b\<times>'c) \<Rightarrow> 'd list" and g
assume "\<forall> (a,b,c) \<in> M. f (a,b,c) = g a b c"
- thus "(UNION M (\<lambda> (a,b,c). set (f (a,b,c)))) = (UNION M (\<lambda> (a,b,c). set (g a b c)))"
+ thus "(\<Union>(a, b, c)\<in>M. set (f (a, b, c))) = (\<Union>(a, b, c)\<in>M. set (g a b c))"
by (auto simp add: split_def)
qed
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]"
by auto
- hence U3: "(UNION {(p,n,s). (p,n,s) \<in> ?SS a \<and> n<0} (\<lambda> (p,n,s). set (?ff (p,n,s)))) =
- (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])))"
- proof-
+ hence U3: "(\<Union> ((\<lambda>(p,n,s). set (?ff (p,n,s))) ` {(p,n,s). (p,n,s) \<in> ?SS a \<and> n<0})) =
+ (\<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}))"
+ proof -
fix M :: "('a\<times>'b\<times>'c) set" and f :: "('a\<times>'b\<times>'c) \<Rightarrow> 'd list" and g
assume "\<forall> (a,b,c) \<in> M. f (a,b,c) = g a b c"
- thus "(UNION M (\<lambda> (a,b,c). set (f (a,b,c)))) = (UNION M (\<lambda> (a,b,c). set (g a b c)))"
+ thus "(\<Union>(a, b, c)\<in>M. set (f (a, b, c))) = (\<Union>(a, b, c)\<in>M. set (g a b c))"
by (auto simp add: split_def)
qed
- have "?SS (Floor a) = UNION (?SS a) (\<lambda>x. set (?ff x))"
+ have "?SS (Floor a) = \<Union> ((\<lambda>x. set (?ff x)) ` ?SS a)"
by auto
- also have "\<dots> = UNION (?SS a) (\<lambda> (p,n,s). set (?ff (p,n,s)))" by blast
+ also have "\<dots> = \<Union> ((\<lambda> (p,n,s). set (?ff (p,n,s))) ` ?SS a)"
+ by blast
also have "\<dots> =
((UNION {(p,n,s). (p,n,s) \<in> ?SS a \<and> n=0} (\<lambda> (p,n,s). set (?ff (p,n,s)))) Un
(UNION {(p,n,s). (p,n,s) \<in> ?SS a \<and> n>0} (\<lambda> (p,n,s). set (?ff (p,n,s)))) Un
@@ -3535,7 +3536,7 @@
proof-
fix M :: "('a\<times>'b\<times>'c) set" and f :: "('a\<times>'b\<times>'c) \<Rightarrow> 'd list" and g
assume "\<forall> (a,b,c) \<in> M. f (a,b,c) = g a b c"
- thus "(UNION M (\<lambda> (a,b,c). set (f (a,b,c)))) = (UNION M (\<lambda> (a,b,c). set (g a b c)))"
+ thus "(\<Union>(a, b, c)\<in>M. set (f (a, b, c))) = (\<Union>(a, b, c)\<in>M. set (g a b c))"
by (auto simp add: split_def)
qed
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]"
@@ -3544,12 +3545,12 @@
proof-
fix M :: "('a\<times>'b\<times>'c) set" and f :: "('a\<times>'b\<times>'c) \<Rightarrow> 'd list" and g
assume "\<forall> (a,b,c) \<in> M. f (a,b,c) = g a b c"
- thus "(UNION M (\<lambda> (a,b,c). set (f (a,b,c)))) = (UNION M (\<lambda> (a,b,c). set (g a b c)))"
+ thus "(\<Union>(a, b, c)\<in>M. set (f (a, b, c))) = (\<Union>(a, b, c)\<in>M. set (g a b c))"
by (auto simp add: split_def)
qed
- have "?SS (Floor a) = UNION (?SS a) (\<lambda>x. set (?ff x))" by auto
- also have "\<dots> = UNION (?SS a) (\<lambda> (p,n,s). set (?ff (p,n,s)))" by blast
+ have "?SS (Floor a) = \<Union> ((\<lambda>x. set (?ff x)) ` ?SS a)" by auto
+ also have "\<dots> = \<Union> ((\<lambda> (p,n,s). set (?ff (p,n,s))) ` ?SS a)" by blast
also have "\<dots> =
((UNION {(p,n,s). (p,n,s) \<in> ?SS a \<and> n=0} (\<lambda> (p,n,s). set (?ff (p,n,s)))) Un
(UNION {(p,n,s). (p,n,s) \<in> ?SS a \<and> n>0} (\<lambda> (p,n,s). set (?ff (p,n,s)))) Un
--- a/src/HOL/Hoare_Parallel/RG_Hoare.thy Sun Nov 18 09:51:41 2018 +0100
+++ b/src/HOL/Hoare_Parallel/RG_Hoare.thy Sun Nov 18 18:07:51 2018 +0000
@@ -1134,7 +1134,7 @@
apply(drule_tac c="s" in subsetD,simp)
apply simp
apply clarify
-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)
+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)
apply simp
apply(erule subsetD)
apply simp
--- a/src/HOL/Library/Countable_Complete_Lattices.thy Sun Nov 18 09:51:41 2018 +0100
+++ b/src/HOL/Library/Countable_Complete_Lattices.thy Sun Nov 18 18:07:51 2018 +0000
@@ -66,13 +66,13 @@
lemma ccInf_insert [simp]: "countable A \<Longrightarrow> Inf (insert a A) = inf a (Inf A)"
by (force intro: le_infI le_infI1 le_infI2 antisym ccInf_greatest ccInf_lower)
-lemma ccINF_insert [simp]: "countable A \<Longrightarrow> (INF x\<in>insert a A. f x) = inf (f a) (INFIMUM A f)"
+lemma ccINF_insert [simp]: "countable A \<Longrightarrow> (INF x\<in>insert a A. f x) = inf (f a) (Inf (f ` A))"
unfolding image_insert by simp
lemma ccSup_insert [simp]: "countable A \<Longrightarrow> Sup (insert a A) = sup a (Sup A)"
by (force intro: le_supI le_supI1 le_supI2 antisym ccSup_least ccSup_upper)
-lemma ccSUP_insert [simp]: "countable A \<Longrightarrow> (SUP x\<in>insert a A. f x) = sup (f a) (SUPREMUM A f)"
+lemma ccSUP_insert [simp]: "countable A \<Longrightarrow> (SUP x\<in>insert a A. f x) = sup (f a) (Sup (f ` A))"
unfolding image_insert by simp
lemma ccINF_empty [simp]: "(INF x\<in>{}. f x) = top"
--- a/src/HOL/Library/Countable_Set_Type.thy Sun Nov 18 09:51:41 2018 +0100
+++ b/src/HOL/Library/Countable_Set_Type.thy Sun Nov 18 18:07:51 2018 +0000
@@ -117,13 +117,13 @@
is "UNION" parametric UNION_transfer by simp
definition cUnion :: "'a cset cset \<Rightarrow> 'a cset" where "cUnion A = cUNION A id"
-lemma Union_conv_UNION: "\<Union>A = UNION A id"
+lemma Union_conv_UNION: "\<Union>A = \<Union>(id ` A)"
by auto
lemma cUnion_transfer [transfer_rule]:
"rel_fun (pcr_cset (pcr_cset A)) (pcr_cset A) Union cUnion"
proof -
- have "rel_fun (pcr_cset (pcr_cset A)) (pcr_cset A) (\<lambda>A. UNION A id) (\<lambda>A. cUNION A id)"
+ have "rel_fun (pcr_cset (pcr_cset A)) (pcr_cset A) (\<lambda>A. \<Union>(id ` A)) (\<lambda>A. cUNION A id)"
by transfer_prover
then show ?thesis by (simp flip: cUnion_def)
qed
--- a/src/HOL/Library/Disjoint_Sets.thy Sun Nov 18 09:51:41 2018 +0100
+++ b/src/HOL/Library/Disjoint_Sets.thy Sun Nov 18 18:07:51 2018 +0000
@@ -158,9 +158,9 @@
shows "bij_betw f (\<Union>i\<in>I. A i) (\<Union>i\<in>I. A' i)"
unfolding bij_betw_def
proof
- from bij show eq: "f ` UNION I A = UNION I A'"
+ from bij show eq: "f ` \<Union>(A ` I) = \<Union>(A' ` I)"
by (auto simp: bij_betw_def image_UN)
- show "inj_on f (UNION I A)"
+ show "inj_on f (\<Union>(A ` I))"
proof (rule inj_onI, clarify)
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"
from A bij[of i] bij[of j] have "f x \<in> A' i" "f y \<in> A' j"
@@ -179,7 +179,7 @@
\<close>
lemma infinite_disjoint_family_imp_infinite_UNION:
assumes "\<not>finite A" "\<And>x. x \<in> A \<Longrightarrow> f x \<noteq> {}" "disjoint_family_on f A"
- shows "\<not>finite (UNION A f)"
+ shows "\<not>finite (\<Union>(f ` A))"
proof -
define g where "g x = (SOME y. y \<in> f x)" for x
have g: "g x \<in> f x" if "x \<in> A" for x
@@ -191,7 +191,7 @@
with A \<open>x \<noteq> y\<close> assms show False
by (auto simp: disjoint_family_on_def inj_on_def)
qed
- from g have "g ` A \<subseteq> UNION A f" by blast
+ from g have "g ` A \<subseteq> \<Union>(f ` A)" by blast
moreover from inj_on_g \<open>\<not>finite A\<close> have "\<not>finite (g ` A)"
using finite_imageD by blast
ultimately show ?thesis using finite_subset by blast
--- a/src/HOL/Library/Extended_Nonnegative_Real.thy Sun Nov 18 09:51:41 2018 +0100
+++ b/src/HOL/Library/Extended_Nonnegative_Real.thy Sun Nov 18 18:07:51 2018 +0000
@@ -1501,7 +1501,7 @@
lemma ennreal_SUP_add:
fixes f g :: "nat \<Rightarrow> ennreal"
- shows "incseq f \<Longrightarrow> incseq g \<Longrightarrow> (SUP i. f i + g i) = SUPREMUM UNIV f + SUPREMUM UNIV g"
+ shows "incseq f \<Longrightarrow> incseq g \<Longrightarrow> (SUP i. f i + g i) = Sup (f ` UNIV) + Sup (g ` UNIV)"
unfolding incseq_def le_fun_def
by transfer
(simp add: SUP_ereal_add incseq_def le_fun_def max_absorb2 SUP_upper2)
@@ -1591,7 +1591,7 @@
done
lemma ennreal_SUP_countable_SUP:
- "A \<noteq> {} \<Longrightarrow> \<exists>f::nat \<Rightarrow> ennreal. range f \<subseteq> g`A \<and> SUPREMUM A g = SUPREMUM UNIV f"
+ "A \<noteq> {} \<Longrightarrow> \<exists>f::nat \<Rightarrow> ennreal. range f \<subseteq> g`A \<and> Sup (g ` A) = Sup (f ` UNIV)"
using ennreal_Sup_countable_SUP [of "g`A"] by auto
lemma of_nat_tendsto_top_ennreal: "(\<lambda>n::nat. of_nat n :: ennreal) \<longlonglongrightarrow> top"
--- a/src/HOL/Library/Extended_Real.thy Sun Nov 18 09:51:41 2018 +0100
+++ b/src/HOL/Library/Extended_Real.thy Sun Nov 18 18:07:51 2018 +0000
@@ -2215,15 +2215,15 @@
lemma ereal_SUP_not_infty:
fixes f :: "_ \<Rightarrow> ereal"
- 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>"
+ 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>"
using SUP_upper2[of _ A l f] SUP_least[of A f u]
- by (cases "SUPREMUM A f") auto
+ by (cases "Sup (f ` A)") auto
lemma ereal_INF_not_infty:
fixes f :: "_ \<Rightarrow> ereal"
- 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>"
+ 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>"
using INF_lower2[of _ A f u] INF_greatest[of A l f]
- by (cases "INFIMUM A f") auto
+ by (cases "Inf (f ` A)") auto
lemma ereal_image_uminus_shift:
fixes X Y :: "ereal set"
@@ -2332,7 +2332,7 @@
lemma SUP_ereal_le_addI:
fixes f :: "'i \<Rightarrow> ereal"
assumes "\<And>i. f i + y \<le> z" and "y \<noteq> -\<infinity>"
- shows "SUPREMUM UNIV f + y \<le> z"
+ shows "Sup (f ` UNIV) + y \<le> z"
unfolding SUP_ereal_add_left[OF UNIV_not_empty \<open>y \<noteq> -\<infinity>\<close>, symmetric]
by (rule SUP_least assms)+
@@ -2351,7 +2351,7 @@
fixes f g :: "nat \<Rightarrow> ereal"
assumes inc: "incseq f" "incseq g"
and pos: "\<And>i. f i \<noteq> -\<infinity>" "\<And>i. g i \<noteq> -\<infinity>"
- shows "(SUP i. f i + g i) = SUPREMUM UNIV f + SUPREMUM UNIV g"
+ shows "(SUP i. f i + g i) = Sup (f ` UNIV) + Sup (g ` UNIV)"
apply (subst SUP_ereal_add_left[symmetric, OF UNIV_not_empty])
apply (metis SUP_upper UNIV_I assms(4) ereal_infty_less_eq(2))
apply (subst (2) add.commute)
@@ -2408,7 +2408,7 @@
fixes f :: "nat \<Rightarrow> ereal"
assumes "decseq f" "decseq g"
and fin: "\<And>i. f i \<noteq> \<infinity>" "\<And>i. g i \<noteq> \<infinity>"
- shows "(INF i. f i + g i) = INFIMUM UNIV f + INFIMUM UNIV g"
+ shows "(INF i. f i + g i) = Inf (f ` UNIV) + Inf (g ` UNIV)"
proof -
have INF_less: "(INF i. f i) < \<infinity>" "(INF i. g i) < \<infinity>"
using assms unfolding INF_less_iff by auto
@@ -2418,7 +2418,7 @@
note * = this
have "(INF i. f i + g i) = (INF i. - ((- f i) + (- g i)))"
by (simp add: fin *)
- also have "\<dots> = INFIMUM UNIV f + INFIMUM UNIV g"
+ also have "\<dots> = Inf (f ` UNIV) + Inf (g ` UNIV)"
unfolding ereal_INF_uminus_eq
using assms INF_less
by (subst SUP_ereal_add) (auto simp: ereal_SUP_uminus fin *)
@@ -2429,7 +2429,7 @@
fixes f g :: "nat \<Rightarrow> ereal"
assumes inc: "incseq f" "incseq g"
and pos: "\<And>i. 0 \<le> f i" "\<And>i. 0 \<le> g i"
- shows "(SUP i. f i + g i) = SUPREMUM UNIV f + SUPREMUM UNIV g"
+ shows "(SUP i. f i + g i) = Sup (f ` UNIV) + Sup (g ` UNIV)"
proof (intro SUP_ereal_add inc)
fix i
show "f i \<noteq> -\<infinity>" "g i \<noteq> -\<infinity>"
@@ -2440,7 +2440,7 @@
fixes f g :: "'a \<Rightarrow> nat \<Rightarrow> ereal"
assumes "\<And>n. n \<in> A \<Longrightarrow> incseq (f n)"
and pos: "\<And>n i. n \<in> A \<Longrightarrow> 0 \<le> f n i"
- shows "(SUP i. \<Sum>n\<in>A. f n i) = (\<Sum>n\<in>A. SUPREMUM UNIV (f n))"
+ shows "(SUP i. \<Sum>n\<in>A. f n i) = (\<Sum>n\<in>A. Sup ((f n) ` UNIV))"
proof (cases "finite A")
case True
then show ?thesis using assms
@@ -2537,7 +2537,7 @@
qed
lemma SUP_countable_SUP:
- "A \<noteq> {} \<Longrightarrow> \<exists>f::nat \<Rightarrow> ereal. range f \<subseteq> g`A \<and> SUPREMUM A g = SUPREMUM UNIV f"
+ "A \<noteq> {} \<Longrightarrow> \<exists>f::nat \<Rightarrow> ereal. range f \<subseteq> g`A \<and> Sup (g ` A) = Sup (f ` UNIV)"
using Sup_countable_SUP [of "g`A"] by auto
subsection "Relation to @{typ enat}"
@@ -3222,7 +3222,7 @@
unfolding Liminf_def
proof (subst SUP_ereal_add_left[symmetric])
let ?F = "{P. eventually P F}"
- let ?INF = "\<lambda>P g. INFIMUM (Collect P) g"
+ let ?INF = "\<lambda>P g. Inf (g ` (Collect P))"
show "?F \<noteq> {}"
by (auto intro: eventually_True)
show "(SUP P\<in>?F. ?INF P g) \<noteq> - \<infinity>"
@@ -3238,7 +3238,7 @@
by (intro add_mono INF_mono) auto
also have "\<dots> = (SUP P'\<in>?F. ?INF ?P' f + ?INF P' g)"
proof (rule SUP_ereal_add_right[symmetric])
- show "INFIMUM {x. P x \<and> 0 \<le> f x} f \<noteq> - \<infinity>"
+ show "Inf (f ` {x. P x \<and> 0 \<le> f x}) \<noteq> - \<infinity>"
unfolding bot_ereal_def[symmetric] INF_eq_bot_iff
by (auto intro!: exI[of _ 0] ev simp: bot_ereal_def)
qed fact
--- a/src/HOL/Library/Finite_Map.thy Sun Nov 18 09:51:41 2018 +0100
+++ b/src/HOL/Library/Finite_Map.thy Sun Nov 18 18:07:51 2018 +0000
@@ -818,7 +818,7 @@
by (rule rel_funI ext)+ (auto simp: fmap.Abs_fmap_inverse fmap.pcr_cr_eq cr_fmap_def)
lemma fmran'_transfer[transfer_rule]:
- "(pcr_fmap (=) (=) ===> (=)) (\<lambda>x. UNION (range x) set_option) fmran'"
+ "(pcr_fmap (=) (=) ===> (=)) (\<lambda>x. \<Union>(set_option ` (range x))) fmran'"
unfolding fmran'_def fmap.pcr_cr_eq cr_fmap_def by fastforce
lemma fmrel_transfer[transfer_rule]:
--- a/src/HOL/Library/Indicator_Function.thy Sun Nov 18 09:51:41 2018 +0100
+++ b/src/HOL/Library/Indicator_Function.thy Sun Nov 18 18:07:51 2018 +0000
@@ -191,7 +191,7 @@
\<close>
lemma indicator_UN_disjoint:
- "finite A \<Longrightarrow> disjoint_family_on f A \<Longrightarrow> indicator (UNION A f) x = (\<Sum>y\<in>A. indicator (f y) x)"
+ "finite A \<Longrightarrow> disjoint_family_on f A \<Longrightarrow> indicator (\<Union>(f ` A)) x = (\<Sum>y\<in>A. indicator (f y) x)"
by (induct A rule: finite_induct)
(auto simp: disjoint_family_on_def indicator_def split: if_splits)
--- a/src/HOL/Library/Liminf_Limsup.thy Sun Nov 18 09:51:41 2018 +0100
+++ b/src/HOL/Library/Liminf_Limsup.thy Sun Nov 18 18:07:51 2018 +0000
@@ -20,7 +20,7 @@
qed (auto elim!: allE[of _ "Sup A"] simp add: not_le[symmetric] cSup_upper assms)
lemma (in conditionally_complete_linorder) le_cSUP_iff:
- "A \<noteq> {} \<Longrightarrow> bdd_above (f`A) \<Longrightarrow> x \<le> SUPREMUM A f \<longleftrightarrow> (\<forall>y<x. \<exists>i\<in>A. y < f i)"
+ "A \<noteq> {} \<Longrightarrow> bdd_above (f`A) \<Longrightarrow> x \<le> Sup (f ` A) \<longleftrightarrow> (\<forall>y<x. \<exists>i\<in>A. y < f i)"
using le_cSup_iff [of "f ` A"] by simp
lemma le_cSup_iff_less:
@@ -46,7 +46,7 @@
qed (auto elim!: allE[of _ "Inf A"] simp add: not_le[symmetric] cInf_lower assms)
lemma (in conditionally_complete_linorder) cINF_le_iff:
- "A \<noteq> {} \<Longrightarrow> bdd_below (f`A) \<Longrightarrow> INFIMUM A f \<le> x \<longleftrightarrow> (\<forall>y>x. \<exists>i\<in>A. y > f i)"
+ "A \<noteq> {} \<Longrightarrow> bdd_below (f`A) \<Longrightarrow> Inf (f ` A) \<le> x \<longleftrightarrow> (\<forall>y>x. \<exists>i\<in>A. y > f i)"
using cInf_le_iff [of "f ` A"] by simp
lemma cInf_le_iff_less:
@@ -89,13 +89,13 @@
abbreviation "limsup \<equiv> Limsup sequentially"
lemma Liminf_eqI:
- "(\<And>P. eventually P F \<Longrightarrow> INFIMUM (Collect P) f \<le> x) \<Longrightarrow>
- (\<And>y. (\<And>P. eventually P F \<Longrightarrow> INFIMUM (Collect P) f \<le> y) \<Longrightarrow> x \<le> y) \<Longrightarrow> Liminf F f = x"
+ "(\<And>P. eventually P F \<Longrightarrow> Inf (f ` (Collect P)) \<le> x) \<Longrightarrow>
+ (\<And>y. (\<And>P. eventually P F \<Longrightarrow> Inf (f ` (Collect P)) \<le> y) \<Longrightarrow> x \<le> y) \<Longrightarrow> Liminf F f = x"
unfolding Liminf_def by (auto intro!: SUP_eqI)
lemma Limsup_eqI:
- "(\<And>P. eventually P F \<Longrightarrow> x \<le> SUPREMUM (Collect P) f) \<Longrightarrow>
- (\<And>y. (\<And>P. eventually P F \<Longrightarrow> y \<le> SUPREMUM (Collect P) f) \<Longrightarrow> y \<le> x) \<Longrightarrow> Limsup F f = x"
+ "(\<And>P. eventually P F \<Longrightarrow> x \<le> Sup (f ` (Collect P))) \<Longrightarrow>
+ (\<And>y. (\<And>P. eventually P F \<Longrightarrow> y \<le> Sup (f ` (Collect P))) \<Longrightarrow> y \<le> x) \<Longrightarrow> Limsup F f = x"
unfolding Limsup_def by (auto intro!: INF_eqI)
lemma liminf_SUP_INF: "liminf f = (SUP n. INF m\<in>{n..}. f m)"
@@ -139,7 +139,7 @@
proof (safe intro!: SUP_mono)
fix P assume "eventually P F"
with ev have "eventually (\<lambda>x. f x \<le> g x \<and> P x) F" (is "eventually ?Q F") by (rule eventually_conj)
- then show "\<exists>Q\<in>{P. eventually P F}. INFIMUM (Collect P) f \<le> INFIMUM (Collect Q) g"
+ then show "\<exists>Q\<in>{P. eventually P F}. Inf (f ` (Collect P)) \<le> Inf (g ` (Collect Q))"
by (intro bexI[of _ ?Q]) (auto intro!: INF_mono)
qed
@@ -155,7 +155,7 @@
proof (safe intro!: INF_mono)
fix P assume "eventually P F"
with ev have "eventually (\<lambda>x. f x \<le> g x \<and> P x) F" (is "eventually ?Q F") by (rule eventually_conj)
- then show "\<exists>Q\<in>{P. eventually P F}. SUPREMUM (Collect Q) f \<le> SUPREMUM (Collect P) g"
+ then show "\<exists>Q\<in>{P. eventually P F}. Sup (f ` (Collect Q)) \<le> Sup (g ` (Collect P))"
by (intro bexI[of _ ?Q]) (auto intro!: SUP_mono)
qed
@@ -183,13 +183,13 @@
then have "eventually (\<lambda>x. P x \<and> Q x) F" (is "eventually ?C F") by (rule eventually_conj)
then have not_False: "(\<lambda>x. P x \<and> Q x) \<noteq> (\<lambda>x. False)"
using ntriv by (auto simp add: eventually_False)
- have "INFIMUM (Collect P) f \<le> INFIMUM (Collect ?C) f"
+ have "Inf (f ` (Collect P)) \<le> Inf (f ` (Collect ?C))"
by (rule INF_mono) auto
- also have "\<dots> \<le> SUPREMUM (Collect ?C) f"
+ also have "\<dots> \<le> Sup (f ` (Collect ?C))"
using not_False by (intro INF_le_SUP) auto
- also have "\<dots> \<le> SUPREMUM (Collect Q) f"
+ also have "\<dots> \<le> Sup (f ` (Collect Q))"
by (rule SUP_mono) auto
- finally show "INFIMUM (Collect P) f \<le> SUPREMUM (Collect Q) f" .
+ finally show "Inf (f ` (Collect P)) \<le> Sup (f ` (Collect Q))" .
qed
lemma Liminf_bounded:
@@ -219,21 +219,21 @@
shows "C \<le> Liminf F X \<longleftrightarrow> (\<forall>y<C. eventually (\<lambda>x. y < X x) F)"
proof -
have "eventually (\<lambda>x. y < X x) F"
- if "eventually P F" "y < INFIMUM (Collect P) X" for y P
+ if "eventually P F" "y < Inf (X ` (Collect P))" for y P
using that by (auto elim!: eventually_mono dest: less_INF_D)
moreover
- have "\<exists>P. eventually P F \<and> y < INFIMUM (Collect P) X"
+ have "\<exists>P. eventually P F \<and> y < Inf (X ` (Collect P))"
if "y < C" and y: "\<forall>y<C. eventually (\<lambda>x. y < X x) F" for y P
proof (cases "\<exists>z. y < z \<and> z < C")
case True
then obtain z where z: "y < z \<and> z < C" ..
- moreover from z have "z \<le> INFIMUM {x. z < X x} X"
+ moreover from z have "z \<le> Inf (X ` {x. z < X x})"
by (auto intro!: INF_greatest)
ultimately show ?thesis
using y by (intro exI[of _ "\<lambda>x. z < X x"]) auto
next
case False
- then have "C \<le> INFIMUM {x. y < X x} X"
+ then have "C \<le> Inf (X ` {x. y < X x})"
by (intro INF_greatest) auto
with \<open>y < C\<close> show ?thesis
using y by (intro exI[of _ "\<lambda>x. y < X x"]) auto
@@ -246,22 +246,22 @@
fixes X :: "_ \<Rightarrow> _ :: complete_linorder"
shows "C \<ge> Limsup F X \<longleftrightarrow> (\<forall>y>C. eventually (\<lambda>x. y > X x) F)"
proof -
- { fix y P assume "eventually P F" "y > SUPREMUM (Collect P) X"
+ { fix y P assume "eventually P F" "y > Sup (X ` (Collect P))"
then have "eventually (\<lambda>x. y > X x) F"
by (auto elim!: eventually_mono dest: SUP_lessD) }
moreover
{ fix y P assume "y > C" and y: "\<forall>y>C. eventually (\<lambda>x. y > X x) F"
- have "\<exists>P. eventually P F \<and> y > SUPREMUM (Collect P) X"
+ have "\<exists>P. eventually P F \<and> y > Sup (X ` (Collect P))"
proof (cases "\<exists>z. C < z \<and> z < y")
case True
then obtain z where z: "C < z \<and> z < y" ..
- moreover from z have "z \<ge> SUPREMUM {x. z > X x} X"
+ moreover from z have "z \<ge> Sup (X ` {x. X x < z})"
by (auto intro!: SUP_least)
ultimately show ?thesis
using y by (intro exI[of _ "\<lambda>x. z > X x"]) auto
next
case False
- then have "C \<ge> SUPREMUM {x. y > X x} X"
+ then have "C \<ge> Sup (X ` {x. X x < y})"
by (intro SUP_least) (auto simp: not_less)
with \<open>y > C\<close> show ?thesis
using y by (intro exI[of _ "\<lambda>x. y > X x"]) auto
@@ -285,17 +285,17 @@
shows "Liminf F f = f0"
proof (intro Liminf_eqI)
fix P assume P: "eventually P F"
- then have "eventually (\<lambda>x. INFIMUM (Collect P) f \<le> f x) F"
+ then have "eventually (\<lambda>x. Inf (f ` (Collect P)) \<le> f x) F"
by eventually_elim (auto intro!: INF_lower)
- then show "INFIMUM (Collect P) f \<le> f0"
+ then show "Inf (f ` (Collect P)) \<le> f0"
by (rule tendsto_le[OF ntriv lim tendsto_const])
next
- fix y assume upper: "\<And>P. eventually P F \<Longrightarrow> INFIMUM (Collect P) f \<le> y"
+ fix y assume upper: "\<And>P. eventually P F \<Longrightarrow> Inf (f ` (Collect P)) \<le> y"
show "f0 \<le> y"
proof cases
assume "\<exists>z. y < z \<and> z < f0"
then obtain z where "y < z \<and> z < f0" ..
- moreover have "z \<le> INFIMUM {x. z < f x} f"
+ moreover have "z \<le> Inf (f ` {x. z < f x})"
by (rule INF_greatest) simp
ultimately show ?thesis
using lim[THEN topological_tendstoD, THEN upper, of "{z <..}"] by auto
@@ -308,9 +308,9 @@
using lim[THEN topological_tendstoD, of "{y <..}"] by auto
then have "eventually (\<lambda>x. f0 \<le> f x) F"
using discrete by (auto elim!: eventually_mono)
- then have "INFIMUM {x. f0 \<le> f x} f \<le> y"
+ then have "Inf (f ` {x. f0 \<le> f x}) \<le> y"
by (rule upper)
- moreover have "f0 \<le> INFIMUM {x. f0 \<le> f x} f"
+ moreover have "f0 \<le> Inf (f ` {x. f0 \<le> f x})"
by (intro INF_greatest) simp
ultimately show "f0 \<le> y" by simp
qed
@@ -324,17 +324,17 @@
shows "Limsup F f = f0"
proof (intro Limsup_eqI)
fix P assume P: "eventually P F"
- then have "eventually (\<lambda>x. f x \<le> SUPREMUM (Collect P) f) F"
+ then have "eventually (\<lambda>x. f x \<le> Sup (f ` (Collect P))) F"
by eventually_elim (auto intro!: SUP_upper)
- then show "f0 \<le> SUPREMUM (Collect P) f"
+ then show "f0 \<le> Sup (f ` (Collect P))"
by (rule tendsto_le[OF ntriv tendsto_const lim])
next
- fix y assume lower: "\<And>P. eventually P F \<Longrightarrow> y \<le> SUPREMUM (Collect P) f"
+ fix y assume lower: "\<And>P. eventually P F \<Longrightarrow> y \<le> Sup (f ` (Collect P))"
show "y \<le> f0"
proof (cases "\<exists>z. f0 < z \<and> z < y")
case True
then obtain z where "f0 < z \<and> z < y" ..
- moreover have "SUPREMUM {x. f x < z} f \<le> z"
+ moreover have "Sup (f ` {x. f x < z}) \<le> z"
by (rule SUP_least) simp
ultimately show ?thesis
using lim[THEN topological_tendstoD, THEN lower, of "{..< z}"] by auto
@@ -347,9 +347,9 @@
using lim[THEN topological_tendstoD, of "{..< y}"] by auto
then have "eventually (\<lambda>x. f x \<le> f0) F"
using False by (auto elim!: eventually_mono simp: not_less)
- then have "y \<le> SUPREMUM {x. f x \<le> f0} f"
+ then have "y \<le> Sup (f ` {x. f x \<le> f0})"
by (rule lower)
- moreover have "SUPREMUM {x. f x \<le> f0} f \<le> f0"
+ moreover have "Sup (f ` {x. f x \<le> f0}) \<le> f0"
by (intro SUP_least) simp
ultimately show "y \<le> f0" by simp
qed
@@ -364,14 +364,14 @@
proof (rule order_tendstoI)
fix a assume "f0 < a"
with assms have "Limsup F f < a" by simp
- then obtain P where "eventually P F" "SUPREMUM (Collect P) f < a"
+ then obtain P where "eventually P F" "Sup (f ` (Collect P)) < a"
unfolding Limsup_def INF_less_iff by auto
then show "eventually (\<lambda>x. f x < a) F"
by (auto elim!: eventually_mono dest: SUP_lessD)
next
fix a assume "a < f0"
with assms have "a < Liminf F f" by simp
- then obtain P where "eventually P F" "a < INFIMUM (Collect P) f"
+ then obtain P where "eventually P F" "a < Inf (f ` (Collect P))"
unfolding Liminf_def less_SUP_iff by auto
then show "eventually (\<lambda>x. a < f x) F"
by (auto elim!: eventually_mono dest: less_INF_D)
@@ -435,7 +435,7 @@
unfolding Liminf_def
by (subst continuous_at_Sup_mono[OF am continuous_on_imp_continuous_within[OF c]])
(auto intro: eventually_True)
- also have "\<dots> = (SUP P \<in> {P. eventually P F}. INFIMUM (g ` Collect P) f)"
+ also have "\<dots> = (SUP P \<in> {P. eventually P F}. Inf (f ` (g ` Collect P)))"
by (intro SUP_cong refl continuous_at_Inf_mono[OF am continuous_on_imp_continuous_within[OF c]])
(auto dest!: eventually_happens simp: F)
finally show ?thesis by (auto simp: Liminf_def)
@@ -460,7 +460,7 @@
unfolding Limsup_def
by (subst continuous_at_Inf_mono[OF am continuous_on_imp_continuous_within[OF c]])
(auto intro: eventually_True)
- also have "\<dots> = (INF P \<in> {P. eventually P F}. SUPREMUM (g ` Collect P) f)"
+ also have "\<dots> = (INF P \<in> {P. eventually P F}. Sup (f ` (g ` Collect P)))"
by (intro INF_cong refl continuous_at_Sup_mono[OF am continuous_on_imp_continuous_within[OF c]])
(auto dest!: eventually_happens simp: F)
finally show ?thesis by (auto simp: Limsup_def)
@@ -484,7 +484,7 @@
unfolding Limsup_def
by (subst continuous_at_Inf_antimono[OF am continuous_on_imp_continuous_within[OF c]])
(auto intro: eventually_True)
- also have "\<dots> = (SUP P \<in> {P. eventually P F}. INFIMUM (g ` Collect P) f)"
+ also have "\<dots> = (SUP P \<in> {P. eventually P F}. Inf (f ` (g ` Collect P)))"
by (intro SUP_cong refl continuous_at_Sup_antimono[OF am continuous_on_imp_continuous_within[OF c]])
(auto dest!: eventually_happens simp: F)
finally show ?thesis
@@ -510,7 +510,7 @@
unfolding Liminf_def
by (subst continuous_at_Sup_antimono[OF am continuous_on_imp_continuous_within[OF c]])
(auto intro: eventually_True)
- also have "\<dots> = (INF P \<in> {P. eventually P F}. SUPREMUM (g ` Collect P) f)"
+ also have "\<dots> = (INF P \<in> {P. eventually P F}. Sup (f ` (g ` Collect P)))"
by (intro INF_cong refl continuous_at_Inf_antimono[OF am continuous_on_imp_continuous_within[OF c]])
(auto dest!: eventually_happens simp: F)
finally show ?thesis
--- a/src/HOL/Library/Option_ord.thy Sun Nov 18 09:51:41 2018 +0100
+++ b/src/HOL/Library/Option_ord.thy Sun Nov 18 18:07:51 2018 +0000
@@ -283,7 +283,8 @@
"A \<noteq> {} \<Longrightarrow> Some (\<Squnion>x\<in>A. f x) = (\<Squnion>x\<in>A. Some (f x))"
using Some_Sup [of "f ` A"] by (simp add: comp_def)
-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"
+lemma option_Inf_Sup: "\<Sqinter>(Sup ` A) \<le> \<Squnion>(Inf ` {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y})"
+ for A :: "('a::complete_distrib_lattice option) set set"
proof (cases "{} \<in> A")
case True
then show ?thesis
@@ -438,8 +439,8 @@
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) "
by (simp add: Inf_Sup)
- also have "... \<le> SUPREMUM {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y} Inf"
- proof (cases "SUPREMUM {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y} Inf")
+ also have "... \<le> \<Squnion> (Inf ` {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y})"
+ proof (cases "\<Squnion> (Inf ` {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y})")
case None
then show ?thesis by (simp add: less_eq_option_def)
next
--- a/src/HOL/Library/Order_Continuity.thy Sun Nov 18 09:51:41 2018 +0100
+++ b/src/HOL/Library/Order_Continuity.thy Sun Nov 18 18:07:51 2018 +0000
@@ -76,7 +76,7 @@
assume M: "mono M"
then have "mono (\<lambda>i. g (M i))"
using sup_continuous_mono[OF g] by (auto simp: mono_def)
- with M show "f (g (SUPREMUM UNIV M)) = (SUP i. f (g (M i)))"
+ with M show "f (g (Sup (M ` UNIV))) = (SUP i. f (g (M i)))"
by (auto simp: sup_continuous_def g[THEN sup_continuousD] f[THEN sup_continuousD])
qed
@@ -274,7 +274,7 @@
assume M: "antimono M"
then have "antimono (\<lambda>i. g (M i))"
using inf_continuous_mono[OF g] by (auto simp: mono_def antimono_def)
- with M show "f (g (INFIMUM UNIV M)) = (INF i. f (g (M i)))"
+ with M show "f (g (Inf (M ` UNIV))) = (INF i. f (g (M i)))"
by (auto simp: inf_continuous_def g[THEN inf_continuousD] f[THEN inf_continuousD])
qed
--- a/src/HOL/Library/Product_Order.thy Sun Nov 18 09:51:41 2018 +0100
+++ b/src/HOL/Library/Product_Order.thy Sun Nov 18 18:07:51 2018 +0000
@@ -220,11 +220,11 @@
of two complete lattices:\<close>
lemma INF_prod_alt_def:
- "INFIMUM A f = (INFIMUM A (fst \<circ> f), INFIMUM A (snd \<circ> f))"
+ "Inf (f ` A) = (Inf ((fst \<circ> f) ` A), Inf ((snd \<circ> f) ` A))"
unfolding Inf_prod_def by simp
lemma SUP_prod_alt_def:
- "SUPREMUM A f = (SUPREMUM A (fst \<circ> f), SUPREMUM A (snd \<circ> f))"
+ "Sup (f ` A) = (Sup ((fst \<circ> f) ` A), Sup((snd \<circ> f) ` A))"
unfolding Sup_prod_def by simp
@@ -235,7 +235,7 @@
instance prod :: (complete_distrib_lattice, complete_distrib_lattice) complete_distrib_lattice
proof
fix A::"('a\<times>'b) set set"
- show "INFIMUM A Sup \<le> SUPREMUM {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y} Inf"
+ show "Inf (Sup ` A) \<le> Sup (Inf ` {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y})"
by (simp add: Sup_prod_def Inf_prod_def INF_SUP_set)
qed
--- a/src/HOL/Library/Set_Algebras.thy Sun Nov 18 09:51:41 2018 +0100
+++ b/src/HOL/Library/Set_Algebras.thy Sun Nov 18 18:07:51 2018 +0000
@@ -408,8 +408,8 @@
by (auto simp: set_times_def)
lemma set_times_UNION_distrib:
- "A * UNION I M = (\<Union>i\<in>I. A * M i)"
- "UNION I M * A = (\<Union>i\<in>I. M i * A)"
+ "A * \<Union>(M ` I) = (\<Union>i\<in>I. A * M i)"
+ "\<Union>(M ` I) * A = (\<Union>i\<in>I. M i * A)"
by (auto simp: set_times_def)
end
--- a/src/HOL/Library/Set_Idioms.thy Sun Nov 18 09:51:41 2018 +0100
+++ b/src/HOL/Library/Set_Idioms.thy Sun Nov 18 18:07:51 2018 +0000
@@ -468,13 +468,13 @@
using R unfolding relative_to_def intersection_of_def by auto
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"
by metis
- then have "\<exists>\<U>'\<subseteq>Collect P. \<Inter>\<U>' = INTER \<U> f"
- by (metis image_subset_iff mem_Collect_eq)
- moreover have eq: "U \<inter> INTER \<U> f = U \<inter> \<Inter>\<U>"
+ then have "f ` \<U> \<subseteq> Collect P"
+ by auto
+ moreover have eq: "U \<inter> \<Inter>(f ` \<U>) = U \<inter> \<Inter>\<U>"
using f by auto
ultimately show ?thesis
unfolding relative_to_def intersection_of_def arbitrary_def \<open>S = U \<inter> \<Inter>\<U>\<close>
- by metis
+ by auto
qed
ultimately show ?thesis
by blast
@@ -502,13 +502,14 @@
using R unfolding relative_to_def intersection_of_def by auto
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"
by metis
- then have "\<exists>\<U>'\<subseteq>Collect P. \<Inter>\<U>' = INTER \<U> f"
- by (metis image_subset_iff mem_Collect_eq)
- moreover have eq: "U \<inter> INTER \<U> f = U \<inter> \<Inter>\<U>"
+ then have "f ` \<U> \<subseteq> Collect P"
+ by auto
+ moreover have eq: "U \<inter> \<Inter> (f ` \<U>) = U \<inter> \<Inter> \<U>"
using f by auto
ultimately show ?thesis
unfolding relative_to_def intersection_of_def \<open>S = U \<inter> \<Inter>\<U>\<close>
- by (metis (no_types, hide_lams) \<open>finite \<U>\<close> f(1) finite_imageI image_subset_iff mem_Collect_eq)
+ using \<open>finite \<U>\<close>
+ by auto
qed
ultimately show ?thesis
by blast
@@ -536,13 +537,14 @@
using R unfolding relative_to_def intersection_of_def by auto
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"
by metis
- then have "\<exists>\<U>'\<subseteq>Collect P. \<Inter>\<U>' = INTER \<U> f"
- by (metis image_subset_iff mem_Collect_eq)
- moreover have eq: "U \<inter> INTER \<U> f = U \<inter> \<Inter>\<U>"
+ then have "f ` \<U> \<subseteq> Collect P"
+ by auto
+ moreover have eq: "U \<inter> \<Inter> (f ` \<U>) = U \<inter> \<Inter> \<U>"
using f by auto
ultimately show ?thesis
unfolding relative_to_def intersection_of_def \<open>S = U \<inter> \<Inter>\<U>\<close>
- by (metis (no_types, hide_lams) \<open>countable \<U>\<close> f(1) countable_image image_subset_iff mem_Collect_eq)
+ using \<open>countable \<U>\<close> countable_image
+ by auto
qed
ultimately show ?thesis
by blast
--- a/src/HOL/Library/Stream.thy Sun Nov 18 09:51:41 2018 +0100
+++ b/src/HOL/Library/Stream.thy Sun Nov 18 18:07:51 2018 +0000
@@ -510,10 +510,10 @@
intro!: exI[of _ m, OF disjI1] bexI[of _ "ss !! n"] exI[of _ n, OF mp])
qed
-lemma sset_smerge: "sset (smerge ss) = UNION (sset ss) sset"
+lemma sset_smerge: "sset (smerge ss) = \<Union>(sset ` (sset ss))"
proof safe
fix x assume "x \<in> sset (smerge ss)"
- thus "x \<in> UNION (sset ss) sset"
+ thus "x \<in> \<Union>(sset ` (sset ss))"
unfolding smerge_def by (subst (asm) sset_flat)
(auto simp: stream.set_map in_set_conv_nth sset_range simp del: stake.simps, fast+)
next
--- a/src/HOL/Probability/Fin_Map.thy Sun Nov 18 09:51:41 2018 +0100
+++ b/src/HOL/Probability/Fin_Map.thy Sun Nov 18 18:07:51 2018 +0000
@@ -807,7 +807,7 @@
qed
next
case (Union a)
- have "UNION UNIV a \<inter> {m. domain m \<in> J} = (\<Union>i. (a i \<inter> {m. domain m \<in> J}))"
+ have "\<Union>(a ` UNIV) \<inter> {m. domain m \<in> J} = (\<Union>i. (a i \<inter> {m. domain m \<in> J}))"
by simp
also have "\<dots> \<in> sets (PiF J M)" using Union by (intro sets.countable_nat_UN) auto
finally show ?case .
--- a/src/HOL/Probability/Independent_Family.thy Sun Nov 18 09:51:41 2018 +0100
+++ b/src/HOL/Probability/Independent_Family.thy Sun Nov 18 18:07:51 2018 +0000
@@ -542,7 +542,7 @@
by auto
{ interpret sigma_algebra "space M" "?UN j"
by (rule sigma_algebra_sigma_sets) auto
- have "\<And>A. (\<And>i. i \<in> J \<Longrightarrow> A i \<in> ?UN j) \<Longrightarrow> INTER J A \<in> ?UN j"
+ have "\<And>A. (\<And>i. i \<in> J \<Longrightarrow> A i \<in> ?UN j) \<Longrightarrow> \<Inter>(A ` J) \<in> ?UN j"
using \<open>finite J\<close> \<open>J \<noteq> {}\<close> by (rule finite_INT) blast }
note INT = this
@@ -620,7 +620,7 @@
fix X assume X: "X \<in> tail_events A"
let ?A = "(\<Inter>n. sigma_sets (space M) (UNION {n..} A))"
from X have "\<And>n::nat. X \<in> sigma_sets (space M) (UNION {n..} A)" by (auto simp: tail_events_def)
- from this[of 0] have "X \<in> sigma_sets (space M) (UNION UNIV A)" by simp
+ from this[of 0] have "X \<in> sigma_sets (space M) (\<Union>(A ` UNIV))" by simp
then show "X \<in> events"
by induct (insert A, auto)
qed
@@ -634,12 +634,12 @@
interpret A: sigma_algebra "space M" "A i" for i by fact
{ fix X x assume "X \<in> ?A" "x \<in> X"
then have "\<And>n. X \<in> sigma_sets (space M) (UNION {n..} A)" by auto
- from this[of 0] have "X \<in> sigma_sets (space M) (UNION UNIV A)" by simp
+ from this[of 0] have "X \<in> sigma_sets (space M) (\<Union>(A ` UNIV))" by simp
then have "X \<subseteq> space M"
by induct (insert A.sets_into_space, auto)
with \<open>x \<in> X\<close> show "x \<in> space M" by auto }
{ fix F :: "nat \<Rightarrow> 'a set" and n assume "range F \<subseteq> ?A"
- then show "(UNION UNIV F) \<in> sigma_sets (space M) (UNION {n..} A)"
+ then show "(\<Union>(F ` UNIV)) \<in> sigma_sets (space M) (UNION {n..} A)"
by (intro sigma_sets.Union) auto }
qed (auto intro!: sigma_sets.Compl sigma_sets.Empty)
@@ -906,7 +906,7 @@
by (auto intro!: exI[of _ "space (M' i)"]) }
note indep_sets_finite_X = indep_sets_finite[OF I this]
- 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))) =
+ 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))) =
(\<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)))"
(is "?L = ?R")
proof safe
@@ -920,7 +920,7 @@
from bchoice[OF this] obtain B where B: "\<forall>i\<in>I. A i = X i -` B i \<inter> space M"
"B \<in> (\<Pi> i\<in>I. E i)" by auto
from \<open>?R\<close>[THEN bspec, OF B(2)] B(1) \<open>I \<noteq> {}\<close>
- show "prob (INTER I A) = (\<Prod>j\<in>I. prob (A j))"
+ show "prob (\<Inter>(A ` I)) = (\<Prod>j\<in>I. prob (A j))"
by simp
qed
then show ?thesis using \<open>I \<noteq> {}\<close>
--- a/src/HOL/Probability/Probability_Mass_Function.thy Sun Nov 18 09:51:41 2018 +0100
+++ b/src/HOL/Probability/Probability_Mass_Function.thy Sun Nov 18 18:07:51 2018 +0000
@@ -1851,15 +1851,15 @@
uniformly at random.
\<close>
lemma pmf_of_set_UN:
- assumes "finite (UNION A f)" "A \<noteq> {}" "\<And>x. x \<in> A \<Longrightarrow> f x \<noteq> {}"
+ assumes "finite (\<Union>(f ` A))" "A \<noteq> {}" "\<And>x. x \<in> A \<Longrightarrow> f x \<noteq> {}"
"\<And>x. x \<in> A \<Longrightarrow> card (f x) = n" "disjoint_family_on f A"
- shows "pmf_of_set (UNION A f) = do {x \<leftarrow> pmf_of_set A; pmf_of_set (f x)}"
+ shows "pmf_of_set (\<Union>(f ` A)) = do {x \<leftarrow> pmf_of_set A; pmf_of_set (f x)}"
(is "?lhs = ?rhs")
proof (intro pmf_eqI)
fix x
from assms have [simp]: "finite A"
using infinite_disjoint_family_imp_infinite_UNION[of A f] by blast
- from assms have "ereal (pmf (pmf_of_set (UNION A f)) x) =
+ from assms have "ereal (pmf (pmf_of_set (\<Union>(f ` A))) x) =
ereal (indicator (\<Union>x\<in>A. f x) x / real (card (\<Union>x\<in>A. f x)))"
by (subst pmf_of_set) auto
also from assms have "card (\<Union>x\<in>A. f x) = card A * n"
--- a/src/HOL/Probability/Projective_Family.thy Sun Nov 18 09:51:41 2018 +0100
+++ b/src/HOL/Probability/Projective_Family.thy Sun Nov 18 18:07:51 2018 +0000
@@ -641,7 +641,7 @@
proof (subst distr_distr)
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
using measurable_component_singleton[of "t x" "UNIV" "\<lambda>x. M (f x)"] unfolding ft[OF x] by simp
- 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)"
+ 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)"
by (auto intro!: measurable_restrict simp: measurable_cong_sets[OF IT.PF.sets_lim refl])
qed (auto intro!: distr_cong measurable_restrict measurable_component_singleton)
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))"
--- a/src/HOL/Probability/Stopping_Time.thy Sun Nov 18 09:51:41 2018 +0100
+++ b/src/HOL/Probability/Stopping_Time.thy Sun Nov 18 18:07:51 2018 +0000
@@ -87,9 +87,9 @@
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)}"
then have "(\<Union>i. {\<omega> \<in> AA i. T \<omega> \<le> t}) \<in> sets (F t)" for t
by auto
- also have "(\<Union>i. {\<omega> \<in> AA i. T \<omega> \<le> t}) = {\<omega> \<in> UNION UNIV AA. T \<omega> \<le> t}"
+ also have "(\<Union>i. {\<omega> \<in> AA i. T \<omega> \<le> t}) = {\<omega> \<in> \<Union>(AA ` UNIV). T \<omega> \<le> t}"
by auto
- finally show "{\<omega> \<in> UNION UNIV AA. T \<omega> \<le> t} \<in> sets (F t)" .
+ finally show "{\<omega> \<in> \<Union>(AA ` UNIV). T \<omega> \<le> t} \<in> sets (F t)" .
qed auto
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)}"
--- a/src/HOL/Probability/Tree_Space.thy Sun Nov 18 09:51:41 2018 +0100
+++ b/src/HOL/Probability/Tree_Space.thy Sun Nov 18 18:07:51 2018 +0000
@@ -197,7 +197,7 @@
finally show ?case .
next
case (Union I)
- have *: "{Node l v r |l v r. (v, l, r) \<in> UNION UNIV I} =
+ have *: "{Node l v r |l v r. (v, l, r) \<in> \<Union>(I ` UNIV)} =
(\<Union>i. {Node l v r |l v r. (v, l, r) \<in> I i})" by auto
show ?case unfolding * using Union(2) by (intro sets.countable_UN) auto
qed
--- a/src/HOL/Probability/ex/Measure_Not_CCC.thy Sun Nov 18 09:51:41 2018 +0100
+++ b/src/HOL/Probability/ex/Measure_Not_CCC.thy Sun Nov 18 18:07:51 2018 +0000
@@ -109,7 +109,7 @@
define G where "G j = (\<Union>i. if j \<in> J i then F i j else X i)" for j
show "(\<Union>i. X i) \<in> sets M" "countable (\<Union>i. J i)" "G \<in> (\<Union>i. J i) \<rightarrow> sets M"
using XFJ by (auto simp: G_def Pi_iff)
- 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)"
+ 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)"
unfolding A_eq by (auto split: if_split_asm)
qed
qed
--- a/src/HOL/UNITY/Comp/Alloc.thy Sun Nov 18 09:51:41 2018 +0100
+++ b/src/HOL/UNITY/Comp/Alloc.thy Sun Nov 18 18:07:51 2018 +0000
@@ -163,7 +163,7 @@
alloc_allowed_acts :: "'a allocState_d program set"
where "alloc_allowed_acts =
{F. AllowedActs F =
- insert Id (UNION (preserves allocGiv) Acts)}"
+ insert Id (\<Union>(Acts ` (preserves allocGiv)))}"
definition
alloc_spec :: "'a allocState_d program set"
--- a/src/HOL/UNITY/Comp/AllocBase.thy Sun Nov 18 09:51:41 2018 +0100
+++ b/src/HOL/UNITY/Comp/AllocBase.thy Sun Nov 18 18:07:51 2018 +0000
@@ -77,7 +77,7 @@
lemma bag_of_nths_UN_disjoint [rule_format]:
"[| finite I; \<forall>i\<in>I. \<forall>j\<in>I. i\<noteq>j \<longrightarrow> A i Int A j = {} |]
- ==> bag_of (nths l (UNION I A)) =
+ ==> bag_of (nths l (\<Union>(A ` I))) =
(\<Sum>i\<in>I. bag_of (nths l (A i)))"
apply (auto simp add: bag_of_nths)
unfolding UN_simps [symmetric]
--- a/src/HOL/UNITY/Comp/AllocImpl.thy Sun Nov 18 09:51:41 2018 +0100
+++ b/src/HOL/UNITY/Comp/AllocImpl.thy Sun Nov 18 18:07:51 2018 +0000
@@ -116,7 +116,7 @@
definition
distr_allowed_acts :: "('a,'b) distr_d program set"
where "distr_allowed_acts =
- {D. AllowedActs D = insert Id (UNION (preserves distr.Out) Acts)}"
+ {D. AllowedActs D = insert Id (\<Union>(Acts ` (preserves distr.Out)))}"
definition
distr_spec :: "('a,'b) distr_d program set"
@@ -160,7 +160,7 @@
(*environmental constraints*)
alloc_allowed_acts :: "'a allocState_d program set"
where "alloc_allowed_acts =
- {F. AllowedActs F = insert Id (UNION (preserves giv) Acts)}"
+ {F. AllowedActs F = insert Id (\<Union>(Acts ` (preserves giv)))}"
definition
alloc_spec :: "'a allocState_d program set"
--- a/src/HOL/UNITY/Constrains.thy Sun Nov 18 09:51:41 2018 +0100
+++ b/src/HOL/UNITY/Constrains.thy Sun Nov 18 18:07:51 2018 +0000
@@ -373,7 +373,7 @@
lemma Always_Int_distrib: "Always (A \<inter> B) = Always A \<inter> Always B"
by (auto simp add: Always_eq_includes_reachable)
-lemma Always_INT_distrib: "Always (INTER I A) = (\<Inter>i \<in> I. Always (A i))"
+lemma Always_INT_distrib: "Always (\<Inter>(A ` I)) = (\<Inter>i \<in> I. Always (A i))"
by (auto simp add: Always_eq_includes_reachable)
lemma Always_Int_I:
--- a/src/HOL/UNITY/Extend.thy Sun Nov 18 09:51:41 2018 +0100
+++ b/src/HOL/UNITY/Extend.thy Sun Nov 18 18:07:51 2018 +0000
@@ -249,7 +249,7 @@
lemma extend_set_Int_distrib: "extend_set h (A \<inter> B) = extend_set h A \<inter> extend_set h B"
by auto
-lemma extend_set_INT_distrib: "extend_set h (INTER A B) = (\<Inter>x \<in> A. extend_set h (B x))"
+lemma extend_set_INT_distrib: "extend_set h (\<Inter>(B ` A)) = (\<Inter>x \<in> A. extend_set h (B x))"
by auto
lemma extend_set_Diff_distrib: "extend_set h (A - B) = extend_set h A - extend_set h B"
--- a/src/HOL/UNITY/Guar.thy Sun Nov 18 09:51:41 2018 +0100
+++ b/src/HOL/UNITY/Guar.thy Sun Nov 18 18:07:51 2018 +0000
@@ -215,7 +215,7 @@
by (simp add: guarantees_Int_right)
lemma guarantees_INT_right_iff:
- "(F \<in> X guarantees (INTER I Y)) = (\<forall>i\<in>I. F \<in> X guarantees (Y i))"
+ "(F \<in> X guarantees (\<Inter>(Y ` I))) = (\<forall>i\<in>I. F \<in> X guarantees (Y i))"
by (simp add: guarantees_INT_right)
lemma shunting: "(X guarantees Y) = (UNIV guarantees (-X \<union> Y))"
@@ -276,7 +276,7 @@
lemma guarantees_JN_INT:
"[| \<forall>i\<in>I. F i \<in> X i guarantees Y i; OK I F |]
- ==> (JOIN I F) \<in> (INTER I X) guarantees (INTER I Y)"
+ ==> (JOIN I F) \<in> (\<Inter>(X ` I)) guarantees (\<Inter>(Y ` I))"
apply (unfold guar_def, auto)
apply (drule bspec, assumption)
apply (rename_tac "i")
@@ -287,7 +287,7 @@
lemma guarantees_JN_UN:
"[| \<forall>i\<in>I. F i \<in> X i guarantees Y i; OK I F |]
- ==> (JOIN I F) \<in> (UNION I X) guarantees (UNION I Y)"
+ ==> (JOIN I F) \<in> (\<Union>(X ` I)) guarantees (\<Union>(Y ` I))"
apply (unfold guar_def, auto)
apply (drule bspec, assumption)
apply (rename_tac "i")
--- a/src/HOL/UNITY/Lift_prog.thy Sun Nov 18 09:51:41 2018 +0100
+++ b/src/HOL/UNITY/Lift_prog.thy Sun Nov 18 18:07:51 2018 +0000
@@ -378,14 +378,14 @@
subsection\<open>OK and "lift"\<close>
lemma act_in_UNION_preserves_fst:
- "act \<subseteq> {(x,x'). fst x = fst x'} ==> act \<in> UNION (preserves fst) Acts"
+ "act \<subseteq> {(x,x'). fst x = fst x'} ==> act \<in> \<Union>(Acts ` (preserves fst))"
apply (rule_tac a = "mk_program (UNIV,{act},UNIV) " in UN_I)
apply (auto simp add: preserves_def stable_def constrains_def)
done
lemma UNION_OK_lift_I:
"[| \<forall>i \<in> I. F i \<in> preserves snd;
- \<forall>i \<in> I. UNION (preserves fst) Acts \<subseteq> AllowedActs (F i) |]
+ \<forall>i \<in> I. \<Union>(Acts ` (preserves fst)) \<subseteq> AllowedActs (F i) |]
==> OK I (%i. lift i (F i))"
apply (auto simp add: OK_def lift_def rename_def Extend.Acts_extend)
apply (simp add: Extend.AllowedActs_extend project_act_extend_act)
--- a/src/HOL/UNITY/Simple/Reachability.thy Sun Nov 18 09:51:41 2018 +0100
+++ b/src/HOL/UNITY/Simple/Reachability.thy Sun Nov 18 18:07:51 2018 +0000
@@ -42,7 +42,7 @@
definition final :: "state set" where
"final == (\<Inter>v\<in>V. reachable v <==> {s. (root, v) \<in> REACHABLE}) \<inter>
- (INTER E (nmsg_eq 0))"
+ (\<Inter>((nmsg_eq 0) ` E))"
axiomatization
where
--- a/src/HOL/UNITY/Union.thy Sun Nov 18 09:51:41 2018 +0100
+++ b/src/HOL/UNITY/Union.thy Sun Nov 18 18:07:51 2018 +0000
@@ -36,7 +36,7 @@
(*Characterizes safety properties. Used with specifying Allowed*)
definition
safety_prop :: "'a program set => bool"
- where "safety_prop X \<longleftrightarrow> SKIP \<in> X \<and> (\<forall>G. Acts G \<subseteq> UNION X Acts \<longrightarrow> G \<in> X)"
+ where "safety_prop X \<longleftrightarrow> SKIP \<in> X \<and> (\<forall>G. Acts G \<subseteq> \<Union>(Acts ` X) \<longrightarrow> G \<in> X)"
syntax
"_JOIN1" :: "[pttrns, 'b set] => 'b set" ("(3\<Squnion>_./ _)" 10)
@@ -376,15 +376,15 @@
given instances of "ok"\<close>
lemma safety_prop_Acts_iff:
- "safety_prop X ==> (Acts G \<subseteq> insert Id (UNION X Acts)) = (G \<in> X)"
+ "safety_prop X ==> (Acts G \<subseteq> insert Id (\<Union>(Acts ` X))) = (G \<in> X)"
by (auto simp add: safety_prop_def)
lemma safety_prop_AllowedActs_iff_Allowed:
- "safety_prop X ==> (UNION X Acts \<subseteq> AllowedActs F) = (X \<subseteq> Allowed F)"
+ "safety_prop X ==> (\<Union>(Acts ` X) \<subseteq> AllowedActs F) = (X \<subseteq> Allowed F)"
by (auto simp add: Allowed_def safety_prop_Acts_iff [symmetric])
lemma Allowed_eq:
- "safety_prop X ==> Allowed (mk_program (init, acts, UNION X Acts)) = X"
+ "safety_prop X ==> Allowed (mk_program (init, acts, \<Union>(Acts ` X))) = X"
by (simp add: Allowed_def safety_prop_Acts_iff)
(*For safety_prop to hold, the property must be satisfiable!*)
@@ -426,7 +426,7 @@
by (rule safety_prop_INTER) simp
lemma def_prg_Allowed:
- "[| F == mk_program (init, acts, UNION X Acts) ; safety_prop X |]
+ "[| F == mk_program (init, acts, \<Union>(Acts ` X)) ; safety_prop X |]
==> Allowed F = X"
by (simp add: Allowed_eq)
@@ -434,12 +434,12 @@
by (simp add: Allowed_def)
lemma def_total_prg_Allowed:
- "[| F = mk_total_program (init, acts, UNION X Acts) ; safety_prop X |]
+ "[| F = mk_total_program (init, acts, \<Union>(Acts ` X)) ; safety_prop X |]
==> Allowed F = X"
by (simp add: mk_total_program_def def_prg_Allowed)
lemma def_UNION_ok_iff:
- "[| F = mk_program(init,acts,UNION X Acts); safety_prop X |]
+ "[| F = mk_program(init,acts,\<Union>(Acts ` X)); safety_prop X |]
==> F ok G = (G \<in> X & acts \<subseteq> AllowedActs G)"
by (auto simp add: ok_def safety_prop_Acts_iff)