--- a/src/HOL/Analysis/Abstract_Topology.thy Thu Nov 22 10:06:30 2018 +0000
+++ b/src/HOL/Analysis/Abstract_Topology.thy Thu Nov 22 10:06:31 2018 +0000
@@ -2792,7 +2792,7 @@
show "U ` \<F> \<subseteq> \<U>"
using \<open>\<F> \<subseteq> \<V>\<close> U by auto
next
- show "f ` S \<subseteq> UNION \<F> U"
+ show "f ` S \<subseteq> \<Union> (U ` \<F>)"
using \<F>(2-3) U UnionE subset_eq U by fastforce
qed
qed
--- a/src/HOL/Analysis/Brouwer_Fixpoint.thy Thu Nov 22 10:06:30 2018 +0000
+++ b/src/HOL/Analysis/Brouwer_Fixpoint.thy Thu Nov 22 10:06:31 2018 +0000
@@ -4991,11 +4991,11 @@
and ope\<phi>: "\<And>C. C \<in> components S \<Longrightarrow> openin (subtopology euclidean S) (\<phi> C)"
and hom\<phi>: "\<And>C. C \<in> components S \<Longrightarrow> homotopic_with (\<lambda>x. True) (\<phi> C) T f g"
by metis
- have Seq: "S = UNION (components S) \<phi>"
+ have Seq: "S = \<Union> (\<phi> ` components S)"
proof
- show "S \<subseteq> UNION (components S) \<phi>"
+ show "S \<subseteq> \<Union> (\<phi> ` components S)"
by (metis Sup_mono Union_components \<phi> imageI)
- show "UNION (components S) \<phi> \<subseteq> S"
+ show "\<Union> (\<phi> ` components S) \<subseteq> S"
using ope\<phi> openin_imp_subset by fastforce
qed
show ?lhs
--- a/src/HOL/Analysis/Caratheodory.thy Thu Nov 22 10:06:30 2018 +0000
+++ b/src/HOL/Analysis/Caratheodory.thy Thu Nov 22 10:06:31 2018 +0000
@@ -187,13 +187,13 @@
case 0 show ?case using f by (simp add: positive_def)
next
case (Suc n)
- have 2: "A n \<inter> UNION {0..<n} A = {}" using disj
+ have 2: "A n \<inter> \<Union> (A ` {0..<n}) = {}" using disj
by (force simp add: disjoint_family_on_def neq_iff)
have 3: "A n \<in> lambda_system \<Omega> M f" using A
by blast
interpret l: algebra \<Omega> "lambda_system \<Omega> M f"
using f by (rule lambda_system_algebra)
- have 4: "UNION {0..<n} A \<in> lambda_system \<Omega> M f"
+ have 4: "\<Union> (A ` {0..<n}) \<in> lambda_system \<Omega> M f"
using A l.UNION_in_sets by simp
from Suc.hyps show ?case
by (simp add: atLeastLessThanSuc lambda_system_strong_additive [OF a 2 3 4])
@@ -250,7 +250,7 @@
fix n
have UNION_in: "(\<Union>i\<in>{0..<n}. A i) \<in> M"
by (metis A'' UNION_in_sets)
- have le_fa: "f (UNION {0..<n} A \<inter> a) \<le> f a" using A''
+ have le_fa: "f (\<Union> (A ` {0..<n}) \<inter> a) \<le> f a" using A''
by (blast intro: increasingD [OF inc] A'' UNION_in_sets)
have ls: "(\<Union>i\<in>{0..<n}. A i) \<in> lambda_system \<Omega> M f"
using ls.UNION_in_sets by (simp add: A)
--- a/src/HOL/Analysis/Change_Of_Vars.thy Thu Nov 22 10:06:30 2018 +0000
+++ b/src/HOL/Analysis/Change_Of_Vars.thy Thu Nov 22 10:06:31 2018 +0000
@@ -652,12 +652,12 @@
proof (intro exI conjI)
show "range ?DD \<subseteq> Collect compact"
using D by clarsimp (metis mem_Collect_eq rangeI split_conv subsetCE surj_pair)
- show "S = UNION UNIV ?DD"
+ show "S = \<Union> (range ?DD)"
proof
- show "S \<subseteq> UNION UNIV ?DD"
+ show "S \<subseteq> \<Union> (range ?DD)"
using D F
by clarsimp (metis UN_iff old.prod.case prod_decode_inverse prod_encode_eq)
- show "UNION UNIV ?DD \<subseteq> S"
+ show "\<Union> (range ?DD) \<subseteq> S"
using D F by fastforce
qed
qed
@@ -2713,11 +2713,11 @@
qed
show "\<exists>T. f ` S \<subseteq> T \<and> T \<in> lmeasurable \<and> ?\<mu> T \<le> e"
proof (intro exI conjI)
- show "f ` S \<subseteq> UNION \<D> g"
+ show "f ` S \<subseteq> \<Union> (g ` \<D>)"
using covers sub_g by force
- show "UNION \<D> g \<in> lmeasurable"
+ show "\<Union> (g ` \<D>) \<in> lmeasurable"
by (rule fmeasurable_UN_bound [OF \<open>countable \<D>\<close> meas_g le_e])
- show "?\<mu> (UNION \<D> g) \<le> e"
+ show "?\<mu> (\<Union> (g ` \<D>)) \<le> e"
by (rule measure_UN_bound [OF \<open>countable \<D>\<close> meas_g le_e])
qed
qed
@@ -3594,7 +3594,7 @@
show "norm (integral (?U k) (norm \<circ> ?D)) \<le> integral (\<Union>n. F n) (norm \<circ> ?D)"
unfolding integral_restrict_UNIV [of _ "norm \<circ> ?D", symmetric]
proof (rule integral_norm_bound_integral)
- show "(\<lambda>x. if x \<in> UNION {..k} F then (norm \<circ> ?D) x else 0) integrable_on UNIV"
+ show "(\<lambda>x. if x \<in> \<Union> (F ` {..k}) then (norm \<circ> ?D) x else 0) integrable_on UNIV"
"(\<lambda>x. if x \<in> (\<Union>n. F n) then (norm \<circ> ?D) x else 0) integrable_on UNIV"
using DU(1) DS
unfolding absolutely_integrable_on_def o_def integrable_restrict_UNIV by auto
--- a/src/HOL/Analysis/Connected.thy Thu Nov 22 10:06:30 2018 +0000
+++ b/src/HOL/Analysis/Connected.thy Thu Nov 22 10:06:31 2018 +0000
@@ -4762,7 +4762,7 @@
moreover have "\<Union>\<D> \<subseteq> \<Union>\<F>"
using \<D>_def by blast
ultimately have eq1: "\<Union>\<F> = \<Union>\<D>" ..
- have eq2: "\<Union>\<D> = UNION \<D> G"
+ have eq2: "\<Union>\<D> = \<Union> (G ` \<D>)"
using G eq1 by auto
show ?thesis
apply (rule_tac \<F>' = "G ` \<D>" in that)
@@ -4781,7 +4781,7 @@
by metis
have [simp]: "\<And>\<F>'. \<F>' \<subseteq> \<F> \<Longrightarrow> \<Union>\<F>' = U \<inter> \<Union>(tf ` \<F>')"
using tf by fastforce
- obtain \<G> where "countable \<G> \<and> \<G> \<subseteq> tf ` \<F>" "\<Union>\<G> = UNION \<F> tf"
+ obtain \<G> where "countable \<G> \<and> \<G> \<subseteq> tf ` \<F>" "\<Union>\<G> = \<Union>(tf ` \<F>)"
using tf by (force intro: Lindelof [of "tf ` \<F>"])
then obtain \<F>' where \<F>': "\<F>' \<subseteq> \<F>" "countable \<F>'" "\<Union>\<F>' = \<Union>\<F>"
by (clarsimp simp add: countable_subset_image)
--- a/src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy Thu Nov 22 10:06:30 2018 +0000
+++ b/src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy Thu Nov 22 10:06:31 2018 +0000
@@ -1937,25 +1937,25 @@
shows measurable_countable_negligible_Union: "(\<Union>n. S n) \<in> lmeasurable"
and measure_countable_negligible_Union: "(\<lambda>n. (measure lebesgue (S n))) sums measure lebesgue (\<Union>n. S n)" (is ?Sums)
proof -
- have 1: "UNION {..n} S \<in> lmeasurable" for n
+ have 1: "\<Union> (S ` {..n}) \<in> lmeasurable" for n
using S by blast
- have 2: "measure lebesgue (UNION {..n} S) \<le> B" for n
+ have 2: "measure lebesgue (\<Union> (S ` {..n})) \<le> B" for n
proof -
- have "measure lebesgue (UNION {..n} S) \<le> (\<Sum>k\<le>n. measure lebesgue (S k))"
+ have "measure lebesgue (\<Union> (S ` {..n})) \<le> (\<Sum>k\<le>n. measure lebesgue (S k))"
by (simp add: S fmeasurableD measure_UNION_le)
with leB show ?thesis
using order_trans by blast
qed
- have 3: "\<And>n. UNION {..n} S \<subseteq> UNION {..Suc n} S"
+ have 3: "\<And>n. \<Union> (S ` {..n}) \<subseteq> \<Union> (S ` {..Suc n})"
by (simp add: SUP_subset_mono)
- have eqS: "(\<Union>n. S n) = (\<Union>n. UNION {..n} S)"
+ have eqS: "(\<Union>n. S n) = (\<Union>n. \<Union> (S ` {..n}))"
using atLeastAtMost_iff by blast
- also have "(\<Union>n. UNION {..n} S) \<in> lmeasurable"
+ also have "(\<Union>n. \<Union> (S ` {..n})) \<in> lmeasurable"
by (intro measurable_nested_Union [OF 1 2] 3)
finally show "(\<Union>n. S n) \<in> lmeasurable" .
- have eqm: "(\<Sum>i\<le>n. measure lebesgue (S i)) = measure lebesgue (UNION {..n} S)" for n
+ have eqm: "(\<Sum>i\<le>n. measure lebesgue (S i)) = measure lebesgue (\<Union> (S ` {..n}))" for n
using assms by (simp add: measure_negligible_finite_Union_image pairwise_mono)
- have "(\<lambda>n. (measure lebesgue (S n))) sums measure lebesgue (\<Union>n. UNION {..n} S)"
+ have "(\<lambda>n. (measure lebesgue (S n))) sums measure lebesgue (\<Union>n. \<Union> (S ` {..n}))"
by (simp add: sums_def' eqm atLeast0AtMost) (intro measure_nested_Union [OF 1 2] 3)
then show ?Sums
by (simp add: eqS)
@@ -1981,7 +1981,7 @@
using bo bounded_subset_cbox_symmetric by metis
then have B: "(\<Sum>k\<le>n. measure lebesgue (S k)) \<le> measure lebesgue (cbox a b)" for n
proof -
- have "(\<Sum>k\<le>n. measure lebesgue (S k)) = measure lebesgue (UNION {..n} S)"
+ have "(\<Sum>k\<le>n. measure lebesgue (S k)) = measure lebesgue (\<Union> (S ` {..n}))"
using measure_negligible_finite_Union_image [OF _ _ pairwise_subset] djointish
by (metis S finite_atMost subset_UNIV)
also have "\<dots> \<le> measure lebesgue (cbox a b)"
@@ -2024,7 +2024,7 @@
have eq: "(\<Union>n. \<Union>k\<le>n. from_nat_into \<D> k) = (\<Union>\<D>)"
using \<open>countable \<D>\<close> False
by (auto intro: from_nat_into dest: from_nat_into_surj [OF \<open>countable \<D>\<close>])
- show "measure lebesgue (\<Union>\<D>) - e < measure lebesgue (UNION {..N} (from_nat_into \<D>))"
+ show "measure lebesgue (\<Union>\<D>) - e < measure lebesgue (\<Union> (from_nat_into \<D> ` {..N}))"
using N [OF order_refl]
by (auto simp: eq algebra_simps dist_norm)
qed auto
@@ -2779,9 +2779,9 @@
by (simp add: False \<D>(1) from_nat_into infinite_imp_nonempty negl_int)
have TB: "(\<Sum>k\<le>n. ?\<mu> (?T k)) \<le> ?\<mu> S + e" for n
proof -
- have "(\<Sum>k\<le>n. ?\<mu> (?T k)) = ?\<mu> (UNION {..n} ?T)"
+ have "(\<Sum>k\<le>n. ?\<mu> (?T k)) = ?\<mu> (\<Union> (?T ` {..n}))"
by (simp add: pairwise_def TM TN measure_negligible_finite_Union_image)
- also have "?\<mu> (UNION {..n} ?T) \<le> ?\<mu> S + e"
+ also have "?\<mu> (\<Union> (?T ` {..n})) \<le> ?\<mu> S + e"
using fincase [of "?T ` {..n}"] T by (auto simp: bij_betw_def)
finally show ?thesis .
qed
--- a/src/HOL/Analysis/Improper_Integral.thy Thu Nov 22 10:06:30 2018 +0000
+++ b/src/HOL/Analysis/Improper_Integral.thy Thu Nov 22 10:06:31 2018 +0000
@@ -398,11 +398,11 @@
qed
also have "... \<le> ?rhs"
proof (rule subadditive_content_division)
- show "extend ` \<D> division_of UNION \<D> extend"
+ show "extend ` \<D> division_of \<Union> (extend ` \<D>)"
using int_extend_disjoint apply (auto simp: division_of_def \<open>finite \<D>\<close> extend)
using extend_def apply blast
done
- show "UNION \<D> extend \<subseteq> cbox a b"
+ show "\<Union> (extend ` \<D>) \<subseteq> cbox a b"
using extend by fastforce
qed
finally show ?thesis .
--- a/src/HOL/Analysis/Starlike.thy Thu Nov 22 10:06:30 2018 +0000
+++ b/src/HOL/Analysis/Starlike.thy Thu Nov 22 10:06:31 2018 +0000
@@ -5128,7 +5128,7 @@
by auto
next
assume "N - X \<subseteq> N - J"
- with J have "N - X \<union> UNION \<H> ((-) N) \<subseteq> N - J"
+ with J have "N - X \<union> \<Union> ((-) N ` \<H>) \<subseteq> N - J"
by auto
with \<open>J \<in> \<H>\<close> show ?thesis
by blast
@@ -7920,7 +7920,7 @@
finally show "closure (\<Union>x\<in>- S. \<Union>y\<in>ball 0 (1 / (2 + real n)). {x + y})
\<subseteq> (\<Union>x \<in> -S. \<Union>y\<in>ball 0 (1 / (1 + real n)). {x + y})" .
qed
- have "S \<subseteq> UNION UNIV ?C"
+ have "S \<subseteq> \<Union> (range ?C)"
proof
fix x
assume x: "x \<in> S"
@@ -7947,10 +7947,10 @@
with that show ?thesis
by auto
qed
- with N2 show "x \<in> UNION UNIV ?C"
+ with N2 show "x \<in> \<Union> (range ?C)"
by (rule_tac a = "N1+N2" in UN_I) (auto simp: dist_norm norm_minus_commute)
qed
- then show "UNION UNIV ?C = S" by auto
+ then show "\<Union> (range ?C) = S" by auto
qed
ultimately show ?thesis
using that by metis
--- a/src/HOL/Analysis/Topology_Euclidean_Space.thy Thu Nov 22 10:06:30 2018 +0000
+++ b/src/HOL/Analysis/Topology_Euclidean_Space.thy Thu Nov 22 10:06:31 2018 +0000
@@ -448,11 +448,11 @@
by (intro exI[of _ "{i \<union> j| i j. i \<in> x \<and> j \<in> y}"]) (auto dest: x(2) y(2))
next
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 have "\<forall>k\<in>K. \<exists>B'\<subseteq>{b. finite b \<and> b \<subseteq> B}. \<Union> (Inter ` B') = k" by auto
then obtain k where
"\<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"
+ then show "\<exists>B'\<subseteq>{b. finite b \<and> b \<subseteq> B}. \<Union> (Inter ` B') = \<Union>K"
by (intro exI[of _ "\<Union>(k ` K)"]) auto
next
case (Basis S)
--- a/src/HOL/Computational_Algebra/Formal_Power_Series.thy Thu Nov 22 10:06:30 2018 +0000
+++ b/src/HOL/Computational_Algebra/Formal_Power_Series.thy Thu Nov 22 10:06:31 2018 +0000
@@ -3378,8 +3378,8 @@
(is "?l = ?r")
proof -
let ?KM = "{(k,m). k + m \<le> n}"
- let ?f = "\<lambda>s. UNION {(0::nat)..s} (\<lambda>i. {(i,s - i)})"
- have th0: "?KM = UNION {0..n} ?f"
+ let ?f = "\<lambda>s. \<Union>i\<in>{0..s}. {(i, s - i)}"
+ have th0: "?KM = \<Union> (?f ` {0..n})"
by auto
show "?l = ?r "
unfolding th0
--- a/src/HOL/Decision_Procs/MIR.thy Thu Nov 22 10:06:30 2018 +0000
+++ b/src/HOL/Decision_Procs/MIR.thy Thu Nov 22 10:06:31 2018 +0000
@@ -7,6 +7,12 @@
"HOL-Library.Code_Target_Numeral" "HOL-Library.Old_Recdef"
begin
+section \<open>Prelude\<close>
+
+abbreviation (input) UNION :: "'a set \<Rightarrow> ('a \<Rightarrow> 'b set) \<Rightarrow> 'b set"
+ where "UNION A f \<equiv> \<Union> (f ` A)" \<comment> \<open>legacy\<close>
+
+
section \<open>Quantifier elimination for \<open>\<real> (0, 1, +, floor, <)\<close>\<close>
declare of_int_floor_cancel [simp del]
--- a/src/HOL/Library/Countable_Set_Type.thy Thu Nov 22 10:06:30 2018 +0000
+++ b/src/HOL/Library/Countable_Set_Type.thy Thu Nov 22 10:06:31 2018 +0000
@@ -440,7 +440,7 @@
lemma rel_cset_cUNION:
"\<lbrakk> rel_cset Q A B; rel_fun Q (rel_cset R) f g \<rbrakk>
- \<Longrightarrow> rel_cset R (cUNION A f) (cUNION B g)"
+ \<Longrightarrow> rel_cset R (cUnion (cimage f A)) (cUnion (cimage g B))"
unfolding rel_fun_def by transfer(erule rel_set_UNION, simp add: rel_fun_def)
lemma rel_cset_csingle_iff [simp]: "rel_cset R (csingle x) (csingle y) \<longleftrightarrow> R x y"
--- a/src/HOL/Library/Set_Idioms.thy Thu Nov 22 10:06:30 2018 +0000
+++ b/src/HOL/Library/Set_Idioms.thy Thu Nov 22 10:06:31 2018 +0000
@@ -375,9 +375,9 @@
using R unfolding relative_to_def union_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. \<Union>\<U>' = UNION \<U> f"
+ then have "\<exists>\<U>'\<subseteq>Collect P. \<Union>\<U>' = \<Union> (f ` \<U>)"
by (metis image_subset_iff mem_Collect_eq)
- moreover have eq: "U \<inter> UNION \<U> f = \<Union>\<U>"
+ moreover have eq: "U \<inter> \<Union> (f ` \<U>) = \<Union>\<U>"
using f by auto
ultimately show ?thesis
unfolding relative_to_def union_of_def arbitrary_def \<open>S = \<Union>\<U>\<close>
@@ -404,14 +404,14 @@
using R unfolding relative_to_def union_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. \<Union>\<U>' = UNION \<U> f"
+ then have "\<exists>\<U>'\<subseteq>Collect P. \<Union>\<U>' = \<Union> (f ` \<U>)"
by (metis image_subset_iff mem_Collect_eq)
- moreover have eq: "U \<inter> UNION \<U> f = \<Union>\<U>"
+ moreover have eq: "U \<inter> \<Union> (f ` \<U>) = \<Union>\<U>"
using f by auto
ultimately show ?thesis
using \<open>finite \<U>\<close> f
unfolding relative_to_def union_of_def \<open>S = \<Union>\<U>\<close>
- by (rule_tac x="UNION \<U> f" in exI) (metis finite_imageI image_subsetI mem_Collect_eq)
+ by (rule_tac x="\<Union> (f ` \<U>)" in exI) (metis finite_imageI image_subsetI mem_Collect_eq)
qed
ultimately show ?thesis
by blast
@@ -434,14 +434,14 @@
using R unfolding relative_to_def union_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. \<Union>\<U>' = UNION \<U> f"
+ then have "\<exists>\<U>'\<subseteq>Collect P. \<Union>\<U>' = \<Union> (f ` \<U>)"
by (metis image_subset_iff mem_Collect_eq)
- moreover have eq: "U \<inter> UNION \<U> f = \<Union>\<U>"
+ moreover have eq: "U \<inter> \<Union> (f ` \<U>) = \<Union>\<U>"
using f by auto
ultimately show ?thesis
using \<open>countable \<U>\<close> f
unfolding relative_to_def union_of_def \<open>S = \<Union>\<U>\<close>
- by (rule_tac x="UNION \<U> f" in exI) (metis countable_image image_subsetI mem_Collect_eq)
+ by (rule_tac x="\<Union> (f ` \<U>)" in exI) (metis countable_image image_subsetI mem_Collect_eq)
qed
ultimately show ?thesis
by blast
--- a/src/HOL/Probability/Independent_Family.thy Thu Nov 22 10:06:30 2018 +0000
+++ b/src/HOL/Probability/Independent_Family.thy Thu Nov 22 10:06:31 2018 +0000
@@ -611,15 +611,15 @@
unfolding indep_vars_def2 by (intro conj_cong indep_sets_cong) auto
definition (in prob_space) tail_events where
- "tail_events A = (\<Inter>n. sigma_sets (space M) (UNION {n..} A))"
+ "tail_events A = (\<Inter>n. sigma_sets (space M) (\<Union> (A ` {n..})))"
lemma (in prob_space) tail_events_sets:
assumes A: "\<And>i::nat. A i \<subseteq> events"
shows "tail_events A \<subseteq> events"
proof
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)
+ let ?A = "(\<Inter>n. sigma_sets (space M) (\<Union> (A ` {n..})))"
+ from X have "\<And>n::nat. X \<in> sigma_sets (space M) (\<Union> (A ` {n..}))" by (auto simp: tail_events_def)
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)
@@ -630,16 +630,16 @@
shows "sigma_algebra (space M) (tail_events A)"
unfolding tail_events_def
proof (simp add: sigma_algebra_iff2, safe)
- let ?A = "(\<Inter>n. sigma_sets (space M) (UNION {n..} A))"
+ let ?A = "(\<Inter>n. sigma_sets (space M) (\<Union> (A ` {n..})))"
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
+ then have "\<And>n. X \<in> sigma_sets (space M) (\<Union> (A ` {n..}))" by auto
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>(F ` UNIV)) \<in> sigma_sets (space M) (UNION {n..} A)"
+ then show "(\<Union>(F ` UNIV)) \<in> sigma_sets (space M) (\<Union> (A ` {n..}))"
by (intro sigma_sets.Union) auto }
qed (auto intro!: sigma_sets.Compl sigma_sets.Empty)
--- a/src/HOL/UNITY/Comp/Alloc.thy Thu Nov 22 10:06:30 2018 +0000
+++ b/src/HOL/UNITY/Comp/Alloc.thy Thu Nov 22 10:06:31 2018 +0000
@@ -99,7 +99,7 @@
client_allowed_acts :: "'a clientState_d program set"
where "client_allowed_acts =
{F. AllowedActs F =
- insert Id (UNION (preserves (funPair rel ask)) Acts)}"
+ insert Id (\<Union> (Acts ` preserves (funPair rel ask)))}"
definition
client_spec :: "'a clientState_d program set"
@@ -208,11 +208,9 @@
\<comment> \<open>environmental constraints\<close>
network_allowed_acts :: "'a systemState program set"
where "network_allowed_acts =
- {F. AllowedActs F =
- insert Id
- (UNION (preserves allocRel Int
- (INT i: lessThan Nclients. preserves(giv o sub i o client)))
- Acts)}"
+ {F. AllowedActs F = insert Id
+ (\<Union> (Acts ` (preserves allocRel \<inter> (\<Inter>i<Nclients.
+ preserves (giv \<circ> sub i \<circ> client)))))}"
definition
network_spec :: "'a systemState program set"
--- a/src/HOL/UNITY/Comp/AllocImpl.thy Thu Nov 22 10:06:30 2018 +0000
+++ b/src/HOL/UNITY/Comp/AllocImpl.thy Thu Nov 22 10:06:31 2018 +0000
@@ -92,7 +92,7 @@
merge_allowed_acts :: "('a,'b) merge_d program set"
where "merge_allowed_acts =
{F. AllowedActs F =
- insert Id (UNION (preserves (funPair merge.Out merge.iOut)) Acts)}"
+ insert Id (\<Union> (Acts ` preserves (funPair merge.Out iOut)))}"
definition
merge_spec :: "('a,'b) merge_d program set"