# HG changeset patch # User haftmann # Date 1542564471 0 # Node ID b021008c5397c4def58be3da5d2023ae9e846199 # Parent e0f68a50768354df48675231028de075c7d42e53 removed legacy input syntax diff -r e0f68a507683 -r b021008c5397 src/Doc/Main/Main_Doc.thy --- 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\'a set\bool"} & (\<^verbatim>\:\)\\ @{const Set.union} & @{term_type_only Set.union "'a set\'a set \ 'a set"} & (\<^verbatim>\Un\)\\ @{const Set.inter} & @{term_type_only Set.inter "'a set\'a set \ 'a set"} & (\<^verbatim>\Int\)\\ -@{const UNION} & @{term_type_only UNION "'a set\('a \ 'b set) \ 'b set"}\\ -@{const INTER} & @{term_type_only INTER "'a set\('a \ 'b set) \ 'b set"}\\ @{const Union} & @{term_type_only Union "'a set set\'a set"}\\ @{const Inter} & @{term_type_only Inter "'a set set\'a set"}\\ @{const Pow} & @{term_type_only Pow "'a set \'a set set"}\\ @@ -134,10 +132,10 @@ @{term[source]"A \ B"} & @{term[source]"B < A"}\\ @{term "{x. P}"} & @{term[source]"Collect (\x. P)"}\\ \{t | x\<^sub>1 \ x\<^sub>n. P}\ & \{v. \x\<^sub>1 \ x\<^sub>n. v = t \ P}\\\ -@{term[source]"\x\I. A"} & @{term[source]"UNION I (\x. A)"} & (\texttt{UN})\\ -@{term[source]"\x. A"} & @{term[source]"UNION UNIV (\x. A)"}\\ -@{term[source]"\x\I. A"} & @{term[source]"INTER I (\x. A)"} & (\texttt{INT})\\ -@{term[source]"\x. A"} & @{term[source]"INTER UNIV (\x. A)"}\\ +@{term[source]"\x\I. A"} & @{term[source]"\((\x. A) ` I)"} & (\texttt{UN})\\ +@{term[source]"\x. A"} & @{term[source]"\((\x. A) ` UNIV)"}\\ +@{term[source]"\x\I. A"} & @{term[source]"\((\x. A) ` I)"} & (\texttt{INT})\\ +@{term[source]"\x. A"} & @{term[source]"\((\x. A) ` UNIV)"}\\ @{term "\x\A. P"} & @{term[source]"Ball A (\x. P)"}\\ @{term "\x\A. P"} & @{term[source]"Bex A (\x. P)"}\\ @{term "range f"} & @{term[source]"f ` UNIV"}\\ diff -r e0f68a507683 -r b021008c5397 src/HOL/Algebra/FiniteProduct.thy --- 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" "\i. i \ I \ finite (A i)" "pairwise (\i j. disjnt (A i) (A j)) I" "\i x. i \ I \ x \ A i \ g x \ carrier G" -shows "finprod G g (UNION I A) = finprod G (\i. finprod G g (A i)) I" +shows "finprod G g (\(A ` I)) = finprod G (\i. finprod G g (A i)) I" using assms proof (induction set: finite) case empty diff -r e0f68a507683 -r b021008c5397 src/HOL/Analysis/Abstract_Topology.thy --- 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 @@ (\\. \ \ (\T. S \ T) ` {T. closedin X T} \ (\\. finite \ \ \ \ \ \ \\ \ {}) \ \\ \ {})" by (simp add: compact_space_fip compactin_subspace closedin_subtopology image_def subset_eq Int_commute imp_conjL) - also have "\ = (\\\Collect (closedin X). (\\. finite \ \ \ \ (\) S ` \ \ \\ \ {}) \ INTER \ ((\) S) \ {})" + also have "\ = (\\\Collect (closedin X). (\\. finite \ \ \ \ (\) S ` \ \ \\ \ {}) \ \ ((\) S ` \) \ {})" by (simp add: all_subset_image) also have "\ = (\\. (\C\\. closedin X C) \ (\\. finite \ \ \ \ \ \ S \ \\ \ {}) \ S \ \\ \ {})" proof - - have eq: "((\\. finite \ \ \ \ \ \ INTER \ ((\) S) \ {}) \ INTER \ ((\) S) \ {}) = + have eq: "((\\. finite \ \ \ \ \ \ \ ((\) S ` \) \ {}) \ \ ((\) S ` \) \ {}) \ ((\\. finite \ \ \ \ \ \ S \ \\ \ {}) \ S \ \\ \ {})" for \ by simp (use \S \ {}\ in blast) show ?thesis diff -r e0f68a507683 -r b021008c5397 src/HOL/Analysis/Arcwise_Connected.thy --- 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 "\range A \ S" using \\n. A n \ S\ by blast - show "closed (INTER UNIV A)" + show "closed (\(A ` UNIV))" using clo by blast - show "\ (INTER UNIV A)" + show "\ (\(A ` UNIV))" by (simp add: clo \ sub) - show "\ U \ INTER UNIV A" if "U \ S" "closed U" "\ U" for U + show "\ U \ \(A ` UNIV)" if "U \ S" "closed U" "\ U" for U proof - have "\y. x \ A y" if "x \ U" and Usub: "U \ (\x. A x)" for x proof - obtain e where "e > 0" and e: "ball x e \ -U" using \closed U\ \x \ U\ openE [of "-U"] by blast - moreover obtain K where K: "ball x e = UNION K B" + moreover obtain K where K: "ball x e = \(B ` K)" using open_cov [of "ball x e"] by auto - ultimately have "UNION K B \ -U" + ultimately have "\(B ` K) \ -U" by blast have "K \ {}" - using \0 < e\ \ball x e = UNION K B\ by auto + using \0 < e\ \ball x e = \(B ` K)\ by auto then obtain n where "n \ K" "x \ B n" by (metis K UN_E \0 < e\ centre_in_ball) then have "U \ B n = {}" @@ -89,16 +89,16 @@ fix F assume cloF: "\n. closed (F n)" and F: "\n. F n \ {} \ F n \ S \ \ (F n)" and Fsub: "\n. F (Suc n) \ F n" - show "INTER UNIV F \ {} \ INTER UNIV F \ S \ \ (INTER UNIV F)" + show "\(F ` UNIV) \ {} \ \(F ` UNIV) \ S \ \ (\(F ` UNIV))" proof (intro conjI) - show "INTER UNIV F \ {}" + show "\(F ` UNIV) \ {}" apply (rule compact_nest) apply (meson F cloF \compact S\ seq_compact_closed_subset seq_compact_eq_compact) apply (simp add: F) by (meson Fsub lift_Suc_antimono_le) - show " INTER UNIV F \ S" + show " \(F ` UNIV) \ S" using F by blast - show "\ (INTER UNIV F)" + show "\ (\(F ` UNIV))" by (metis F Fsub \ \compact S\ cloF closed_Int_compact inf.orderE) qed next @@ -1680,7 +1680,7 @@ using that by auto show "\ {0..1}" by (auto simp: \_def open_segment_eq_real_ivl *) - show "\ (INTER UNIV F)" + show "\ (\(F ` UNIV))" if "\n. closed (F n)" and \: "\n. \ (F n)" and Fsub: "\n. F (Suc n) \ F n" for F proof - have F01: "\n. F n \ {0..1} \ 0 \ F n \ 1 \ F n" @@ -1706,13 +1706,13 @@ using minxy \0 < e\ less by simp_all have Fclo: "\T. T \ range F \ closed T" by (metis \\n. closed (F n)\ image_iff) - have eq: "{w..z} \ INTER UNIV F = {}" + have eq: "{w..z} \ \(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} \ (\ (F ` K)) = {}" by (metis finite_subset_image compact_imp_fip [OF compact_interval Fclo]) then have "K \ {}" - using \w < z\ \{w..z} \ INTER K F = {}\ by auto + using \w < z\ \{w..z} \ \(F ` K) = {}\ by auto define n where "n \ Max K" have "n \ K" unfolding n_def by (metis \K \ {}\ \finite K\ Max_in) have "F n \ \ (F ` K)" diff -r e0f68a507683 -r b021008c5397 src/HOL/Analysis/Binary_Product_Measure.thy --- 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) \ UNIV = UNION UNIV (\i. A i \ UNIV)" + moreover have *: "(\(A ` UNIV)) \ UNIV = \((\i. A i \ UNIV) ` UNIV)" by auto ultimately show ?case unfolding * by auto @@ -1137,7 +1137,7 @@ unfolding * by auto next case (Union B) - moreover have *: "UNIV \ (UNION UNIV B) = UNION UNIV (\i. UNIV \ B i)" + moreover have *: "UNIV \ (\(B ` UNIV)) = \((\i. UNIV \ B i) ` UNIV)" by auto ultimately show ?case unfolding * by auto diff -r e0f68a507683 -r b021008c5397 src/HOL/Analysis/Brouwer_Fixpoint.thy --- 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') (\(F ` T))" using F by blast - show "T \ UNION T F" + show "T \ \(F ` T)" using F by blast - show "S \ UNION T F \ U" + show "S \ \(F ` T) \ U" using F by auto qed qed @@ -4882,23 +4882,23 @@ by (simp add: homotopic_with) metis have wop: "b \ V x \ \k. b \ V k \ (\j V j)" for b x using nat_less_induct [where P = "\i. b \ V i"] by meson - obtain \ where cont: "continuous_on ({0..1} \ UNION UNIV V) \" - and eq: "\x i. \x \ {0..1} \ UNION UNIV V \ + obtain \ where cont: "continuous_on ({0..1} \ \(V ` UNIV)) \" + and eq: "\x i. \x \ {0..1} \ \(V ` UNIV) \ {0..1} \ (V i - (\m \ \ x = h i x" proof (rule pasting_lemma_exists) - show "{0..1} \ UNION UNIV V \ (\i. {0..1::real} \ (V i - (\m \(V ` UNIV) \ (\i. {0..1::real} \ (V i - (\m UNION UNIV V)) + show "openin (subtopology euclidean ({0..1} \ \(V ` UNIV))) ({0..1::real} \ (V i - (\m(V ` UNIV))) (V i)" using ope V eqU by auto - show "closedin (subtopology euclidean (UNION UNIV V)) (\m(V ` UNIV))) (\m (V i - (\mi j x. x \ {0..1} \ UNION UNIV V \ + show "\i j x. x \ {0..1} \ \(V ` UNIV) \ {0..1} \ (V i - (\m {0..1} \ (V j - (\m h i x = h j x" by clarsimp (metis lessThan_iff linorder_neqE_nat) diff -r e0f68a507683 -r b021008c5397 src/HOL/Analysis/Caratheodory.thy --- 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 "(\i. f (if i = 0 then s else {})) \ f s" using positiveD1[OF posf] by (subst suminf_finite[of "{0}"]) auto - with s show "(INF A\{A. range A \ M \ disjoint_family A \ s \ UNION UNIV A}. \i. f (A i)) \ f s" + with s show "(INF A\{A. range A \ M \ disjoint_family A \ s \ \(A ` UNIV)}. \i. f (A i)) \ f s" by (intro INF_lower2[of "\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: "\i. i \ I \ A i \ M" "disjoint_family_on A I" "finite I" "UNION I A \ M" - shows "f (UNION I A) = (\i\I. f (A i))" + assumes A: "\i. i \ I \ A i \ M" "disjoint_family_on A I" "finite I" "\(A ` I) \ M" + shows "f (\(A ` I)) = (\i\I. f (A i))" proof - have "A`I \ M" "disjoint (A`I)" "finite (A`I)" "\(A`I) \ 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 \volume M f\] by simp qed (auto intro: \finite I\) - finally show "f (UNION I A) = (\i\I. f (A i))" + finally show "f (\(A ` I)) = (\i\I. f (A i))" by simp qed diff -r e0f68a507683 -r b021008c5397 src/HOL/Analysis/Change_Of_Vars.thy --- 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\_set*) inductive%important fsigma :: "'a::topological_space set \ bool" where - "(\n::nat. closed (F n)) \ fsigma (UNION UNIV F)" + "(\n::nat. closed (F n)) \ fsigma (\(F ` UNIV))" inductive%important gdelta :: "'a::topological_space set \ bool" where - "(\n::nat. open (F n)) \ gdelta (INTER UNIV F)" + "(\n::nat. open (F n)) \ gdelta (\(F ` UNIV))" lemma%important fsigma_Union_compact: fixes S :: "'a::{real_normed_vector,heine_borel} set" - shows "fsigma S \ (\F::nat \ 'a set. range F \ Collect compact \ S = UNION UNIV F)" + shows "fsigma S \ (\F::nat \ 'a set. range F \ Collect compact \ S = \(F ` UNIV))" proof%unimportant safe assume "fsigma S" - then obtain F :: "nat \ 'a set" where F: "range F \ Collect closed" "S = UNION UNIV F" + then obtain F :: "nat \ 'a set" where F: "range F \ Collect closed" "S = \(F ` UNIV)" by (meson fsigma.cases image_subsetI mem_Collect_eq) - then have "\D::nat \ 'a set. range D \ Collect compact \ UNION UNIV D = F i" for i + then have "\D::nat \ 'a set. range D \ Collect compact \ \(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 \ nat \ 'a set" - where D: "\i. range (D i) \ Collect compact \ UNION UNIV (D i) = F i" + where D: "\i. range (D i) \ Collect compact \ \((D i) ` UNIV) = F i" by metis let ?DD = "\n. (\(i,j). D i j) (prod_decode n)" - show "\F::nat \ 'a set. range F \ Collect compact \ S = UNION UNIV F" + show "\F::nat \ 'a set. range F \ Collect compact \ S = \(F ` UNIV)" proof (intro exI conjI) show "range ?DD \ 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 \ 'a set" - assume "range F \ Collect compact" and "S = UNION UNIV F" - then show "fsigma (UNION UNIV F)" + assume "range F \ Collect compact" and "S = \(F ` UNIV)" + then show "fsigma (\(F ` UNIV))" by (simp add: compact_imp_closed fsigma.intros image_subset_iff) qed lemma%unimportant gdelta_imp_fsigma: "gdelta S \ fsigma (- S)" proof (induction rule: gdelta.induct) case (1 F) - have "- INTER UNIV F = (\i. -(F i))" + have "- \(F ` UNIV) = (\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 \ gdelta (- S)" proof (induction rule: fsigma.induct) case (1 F) - have "- UNION UNIV F = (\i. -(F i))" + have "- \(F ` UNIV) = (\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: "\n::nat. closed (F n) \ F n \ S \ S - F n \ lmeasurable \ measure lebesgue (S - F n) < 1 / Suc n" by metis - let ?C = "UNION UNIV F" + let ?C = "\(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 \ UNION UNIV F" - then show "(g has_derivative g' x) (at x within UNION UNIV F)" + assume "x \ \(F ` UNIV)" + then show "(g has_derivative g' x) (at x within \(F ` UNIV))" using Ceq \C \ N = S\ der_g has_derivative_within_subset by blast next - have "UNION UNIV F \ S" + have "\(F ` UNIV) \ S" using Ceq \C \ N = S\ by blast - then show "inj_on g (UNION UNIV F)" + then show "inj_on g (\(F ` UNIV))" using inj by (meson inj_on_subset) qed (use F in auto) moreover diff -r e0f68a507683 -r b021008c5397 src/HOL/Analysis/Complete_Measure.thy --- 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 \ ?A" + then show "\(A ` UNIV) \ ?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 _ "\(S ` UNIV)" "\(N ` UNIV)" "\(N' ` UNIV)"]) auto qed lemma sets_completion: @@ -199,7 +199,7 @@ qed then have "(\n. emeasure M (main_part M (A n))) = emeasure M (\i. main_part M (A i))" using A by (auto intro!: suminf_emeasure) - then show "(\n. ?\ (A n)) = ?\ (UNION UNIV A)" + then show "(\n. ?\ (A n)) = ?\ (\(A ` UNIV))" by (simp add: completion_def emeasure_main_part_UN[OF A(1)]) qed qed diff -r e0f68a507683 -r b021008c5397 src/HOL/Analysis/Embed_Measure.thy --- 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 "\ = (SUP i\Y. \\<^sup>+ x. f i (from_nat_into B (to_nat_on B x)) \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 "\ = ?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 = "\A f. Sup (f ` A)"] ext nn_integral_cong_AE)(simp_all add: AE_count_space countable) finally show ?thesis . qed diff -r e0f68a507683 -r b021008c5397 src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy --- 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 \E \ space ?L\ by (auto simp: space_restrict_space) then obtain z k where "(z, k) \ p" "v \ k" using tagged_division_ofD(6)[OF p(1), symmetric] by auto - with not show "v \ UNION (p - s) snd" + with not show "v \ \(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 "\ = measure ?L (\x\p \ s. snd x)" @@ -299,9 +299,9 @@ define B :: "nat \ 'a set" where "B n = cbox (- real n *\<^sub>R One) (real n *\<^sub>R One)" for n show "(\x. f x * indicator \ x) \ lebesgue \\<^sub>M borel" proof (rule measurable_piecewise_restrict) - have "(\n. box (- real n *\<^sub>R One) (real n *\<^sub>R One)) \ UNION UNIV B" + have "(\n. box (- real n *\<^sub>R One) (real n *\<^sub>R One)) \ \(B ` UNIV)" unfolding B_def by (intro UN_mono box_subset_cbox order_refl) - then show "countable (range B)" "space lebesgue \ UNION UNIV B" + then show "countable (range B)" "space lebesgue \ \(B ` UNIV)" by (auto simp: B_def UN_box_eq_UNIV) next fix \' assume "\' \ range B" @@ -398,7 +398,7 @@ case (union F) then have [measurable]: "\i. F i \ sets borel" by (simp add: borel_eq_box subset_eq) - have "((\x. if x \ UNION UNIV F \ box a b then 1 else 0) has_integral ?M (\i. F i)) (box a b)" + have "((\x. if x \ \(F ` UNIV) \ box a b then 1 else 0) has_integral ?M (\i. F i)) (box a b)" proof (rule has_integral_monotone_convergence_increasing) let ?f = "\k x. \i F i \ box a b then 1 else 0 :: real" show "\k. (?f k has_integral (\ix i j. x \ F i \ x \ F j \ j = i" by (auto simp add: disjoint_family_on_def) - show "\x. (\k. ?f k x) \ (if x \ UNION UNIV F \ box a b then 1 else 0)" + show "\x. (\k. ?f k x) \ (if x \ \(F ` UNIV) \ 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: "\n x::'a. indicat_real (S n) x \ (indicat_real (S (Suc n)) x)" by (simp add: indicator_leI nest rev_subsetD) - have 3: "\x. (\n. indicat_real (S n) x) \ (indicat_real (UNION UNIV S) x)" + have 3: "\x. (\n. indicat_real (S n) x) \ (indicat_real (\(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: "\x. x \ S \ x \ U x" and neg: "\x. x \ S \ negligible (U x)" by metis - obtain \ where "\ \ U ` S" "countable \" and eq: "\\ = UNION S U" + obtain \ where "\ \ U ` S" "countable \" and eq: "\\ = \(U ` S)" using ope by (force intro: Lindelof_openin [of "U ` S" S]) then have "negligible (\\)" by (metis imageE neg negligible_countable_Union subset_eq) - with eq have "negligible (UNION S U)" + with eq have "negligible (\(U ` S))" by metis - moreover have "S \ UNION S U" + moreover have "S \ \(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 \d" and "K = (\k\d. norm (integral k f))" - "SUPREMUM {d. d division_of \d} (sum (\k. norm (integral k f))) - e < K" + "Sup (sum (\k. norm (integral k f)) ` {d. d division_of \ d}) - e < K" by (auto simp add: image_iff not_le) - then have d: "SUPREMUM {d. d division_of \d} (sum (\k. norm (integral k f))) - e + then have d: "Sup (sum (\k. norm (integral k f)) ` {d. d division_of \ d}) - e < (\k\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 "(\n. ?\ (X n)) sums ?\ (\n. X n)" by (rule measure_countable_negligible_Union_bounded [OF 1 2 3]) - have meq: "?\ (\n. f ` X n) = m * ?\ (UNION UNIV X)" + have meq: "?\ (\n. f ` X n) = m * ?\ (\(X ` UNIV))" proof (rule sums_unique2 [OF measure_countable_negligible_Union_bounded [OF f1 f2 f3]]) have m: "\n. ?\ (f ` X n) = (m * ?\ (X n))" using S unfolding bij_betw_def by (metis cbox im rangeI) - show "(\n. ?\ (f ` X n)) sums (m * ?\ (UNION UNIV X))" + show "(\n. ?\ (f ` X n)) sums (m * ?\ (\(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 (\(range s))" and s: "\m. s m \ sets lebesgue" shows "\n. f absolutely_integrable_on (\m\n. s m)" - and "(\n. integral (\m\n. s m) f) \ integral (UNION UNIV s) f" (is "?F \ ?I") + and "(\n. integral (\m\n. s m) f) \ integral (\(s ` UNIV)) f" (is "?F \ ?I") proof - show fU: "f absolutely_integrable_on (\m\n. s m)" for n using assms by (blast intro: set_integrable_subset [OF f]) have fint: "f integrable_on (\ (range s))" using absolutely_integrable_on_def f by blast - let ?h = "\x. if x \ UNION UNIV s then norm(f x) else 0" + let ?h = "\x. if x \ \(s ` UNIV) then norm(f x) else 0" have "(\n. integral UNIV (\x. if x \ (\m\n. s m) then f x else 0)) - \ integral UNIV (\x. if x \ UNION UNIV s then f x else 0)" + \ integral UNIV (\x. if x \ \(s ` UNIV) then f x else 0)" proof (rule dominated_convergence) show "(\x. if x \ (\m\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 "(\x. if x \ UNION UNIV s then norm(f x) else 0) integrable_on UNIV" + show "(\x. if x \ \(s ` UNIV) then norm(f x) else 0) integrable_on UNIV" by (metis (no_types) absolutely_integrable_on_def f integrable_restrict_UNIV) show "\x\UNIV. (\n. if x \ (\m\n. s m) then f x else 0) - \ (if x \ UNION UNIV s then f x else 0)" + \ (if x \ \(s ` UNIV) then f x else 0)" by (force intro: Lim_eventually eventually_sequentiallyI) qed auto then show "?F \ ?I" diff -r e0f68a507683 -r b021008c5397 src/HOL/Analysis/Extended_Real_Limits.thy --- 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 "\y. y \ S \ y \ x \ dist y x < d \ P y" then have "S \ ball x d - {x} \ {x. P x}" by (auto simp: zero_less_dist_iff dist_commute) - then show "\r>0. INFIMUM (Collect P) f \ INFIMUM (S \ ball x r - {x}) f" + then show "\r>0. Inf (f ` (Collect P)) \ Inf (f ` (S \ ball x r - {x}))" by (intro exI[of _ d] INF_mono conjI \0 < d\) auto next fix d :: real assume "0 < d" then show "\P. (\d>0. \xa. xa \ S \ xa \ x \ dist xa x < d \ P xa) \ - INFIMUM (S \ ball x d - {x}) f \ INFIMUM (Collect P) f" + Inf (f ` (S \ ball x d - {x})) \ Inf (f ` (Collect P))" by (intro exI[of _ "\y. y \ S \ ball x d - {x}"]) (auto intro!: INF_mono exI[of _ d] simp: dist_commute) qed @@ -325,13 +325,13 @@ assume "0 < d" and "\y. y \ S \ y \ x \ dist y x < d \ P y" then have "S \ ball x d - {x} \ {x. P x}" by (auto simp: zero_less_dist_iff dist_commute) - then show "\r>0. SUPREMUM (S \ ball x r - {x}) f \ SUPREMUM (Collect P) f" + then show "\r>0. Sup (f ` (S \ ball x r - {x})) \ Sup (f ` (Collect P))" by (intro exI[of _ d] SUP_mono conjI \0 < d\) auto next fix d :: real assume "0 < d" then show "\P. (\d>0. \xa. xa \ S \ xa \ x \ dist xa x < d \ P xa) \ - SUPREMUM (Collect P) f \ SUPREMUM (S \ ball x d - {x}) f" + Sup (f ` (Collect P)) \ Sup (f ` (S \ ball x d - {x}))" by (intro exI[of _ "\y. y \ S \ 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 \ S" + assume S: "mono_set S" "Inf (f ` (Collect P)) \ S" { fix x assume "P x" - then have "INFIMUM (Collect P) f \ f x" + then have "Inf (f ` (Collect P)) \ f x" by (intro complete_lattice_class.INF_lower) simp with S have "f x \ S" by (simp add: mono_set) @@ -1069,16 +1069,16 @@ next fix y l assume S: "\S. open S \ mono_set S \ l \ S \ eventually (\x. f x \ S) net" - assume P: "\P. eventually P net \ INFIMUM (Collect P) f \ y" + assume P: "\P. eventually P net \ Inf (f ` (Collect P)) \ y" show "l \ y" proof (rule dense_le) fix B assume "B < l" then have "eventually (\x. f x \ {B <..}) net" by (intro S[rule_format]) auto - then have "INFIMUM {x. B < f x} f \ y" + then have "Inf (f ` {x. B < f x}) \ y" using P by auto - moreover have "B \ INFIMUM {x. B < f x} f" + moreover have "B \ Inf (f ` {x. B < f x})" by (intro INF_greatest) auto ultimately show "B \ 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 \ S" + assume S: "mono_set (uminus`S)" "Sup (f ` (Collect P)) \ S" { fix x assume "P x" - then have "f x \ SUPREMUM (Collect P) f" + then have "f x \ 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 \ S" by (simp add: inj_image_mem_iff) } with P show "eventually (\x. f x \ S) net" @@ -1108,16 +1108,16 @@ next fix y l assume S: "\S. open S \ mono_set (uminus ` S) \ l \ S \ eventually (\x. f x \ S) net" - assume P: "\P. eventually P net \ y \ SUPREMUM (Collect P) f" + assume P: "\P. eventually P net \ y \ Sup (f ` (Collect P))" show "y \ l" proof (rule dense_ge) fix B assume "l < B" then have "eventually (\x. f x \ {..< B}) net" by (intro S[rule_format]) auto - then have "y \ SUPREMUM {x. f x < B} f" + then have "y \ Sup (f ` {x. f x < B})" using P by auto - moreover have "SUPREMUM {x. f x < B} f \ B" + moreover have "Sup (f ` {x. f x < B}) \ B" by (intro SUP_least) auto ultimately show "y \ B" by simp @@ -1240,7 +1240,7 @@ apply (rule INF_eq) using \decseq v\ decseq_Suc_iff by auto moreover have "decseq (\n. (SUP m\{n..}. u m))" by (simp add: SUP_subset_mono decseq_def) ultimately have c: "(INF n\{1..}. (SUP m\{n..}. u m)) = (INF n. (SUP m\{n..}. u m))" by simp - have "(INF n. SUPREMUM {n..} u) = (INF n. SUP m\{n..}. u (m + 1))" using a b c by simp + have "(INF n. Sup (u ` {n..})) = (INF n. SUP m\{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 \incseq v\ incseq_Suc_iff by auto moreover have "incseq (\n. (INF m\{n..}. u m))" by (simp add: INF_superset_mono mono_def) ultimately have c: "(SUP n\{1..}. (INF m\{n..}. u m)) = (SUP n. (INF m\{n..}. u m))" by simp - have "(SUP n. INFIMUM {n..} u) = (SUP n. INF m\{n..}. u (m + 1))" using a b c by simp + have "(SUP n. Inf (u ` {n..})) = (SUP n. INF m\{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 \ ereal" assume *: "\x. 0 \ v x" "\x. 0 \ u x" "\n. v n \ u n" moreover have "0 \ limsup u - limsup v" using * by (intro ereal_diff_positive Limsup_mono always_eventually) simp - moreover have "0 \ (SUPREMUM {x..} v)" for x + moreover have "0 \ Sup (u ` {x..})" for x using * by (intro SUP_upper2[of x]) auto - moreover have "0 \ (SUPREMUM {x..} u)" for x + moreover have "0 \ Sup (v ` {x..})" for x using * by (intro SUP_upper2[of x]) auto ultimately show "(SUP n. INF n\{n..}. max 0 (u n - v n)) - \ max 0 ((INF x. max 0 (SUPREMUM {x..} u)) - (INF x. max 0 (SUPREMUM {x..} v)))" + \ 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 diff -r e0f68a507683 -r b021008c5397 src/HOL/Analysis/Finite_Product_Measure.thy --- 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 _ "\i. J i"] bexI[of _ "\i. prod_emb (\i. J i) M (J i) (X i)"] conjI) show "(\i. J i) \ I" "countable (\i. J i)" using J by auto - with J show "UNION UNIV K = prod_emb I M (\i. J i) (\i. prod_emb (\i. J i) M (J i) (X i))" + with J show "\(K ` UNIV) = prod_emb I M (\i. J i) (\i. prod_emb (\i. J i) M (J i) (X i))" by (simp add: K[abs_def] SUP_upper) qed(auto intro: X) qed diff -r e0f68a507683 -r b021008c5397 src/HOL/Analysis/Henstock_Kurzweil_Integration.thy --- 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 "\i1 i2. \i1 \ r; i2 \ r; i1 \ i2\ \ interior i1 \ interior i2 = {}" by (simp add: q'(5) r_def) - show "interior (UNION p snd) \ interior (\r) = {}" + show "interior (\(snd ` p)) \ interior (\r) = {}" proof (rule Int_interior_Union_intervals [OF \finite r\]) - show "open (interior (UNION p snd))" + show "open (interior (\(snd ` p)))" by blast show "\T. T \ r \ \a b. T = cbox a b" by (simp add: q'(4) r_def) have "finite (snd ` p)" by (simp add: p'(1)) - then show "\T. T \ r \ interior (UNION p snd) \ interior T = {}" + then show "\T. T \ r \ interior (\(snd ` p)) \ 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 (\(qq ` r))" by (meson finite_UN qq \finite r\ tagged_division_of_finite) qed moreover have "content M *\<^sub>R f x = 0" diff -r e0f68a507683 -r b021008c5397 src/HOL/Analysis/Homeomorphism.thy --- 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: "\x. x \ S \ v x \ S \ open (t x) \ compact (v x) \ (\u. x \ u \ u \ v x \ u = S \ t x)" by metis - then have o: "open (UNION S t)" + then have o: "open (\(t ` S))" by blast have "S = \ (v ` S)" using tv by blast - also have "... = UNION S t \ closure S" + also have "... = \(t ` S) \ closure S" proof - show "UNION S v \ UNION S t \ closure S" + show "\(v ` S) \ \(t ` S) \ 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 \ closure S \ UNION S v" + then show "\(t ` S) \ closure S \ \(v ` S)" by blast qed - finally have e: "S = UNION S t \ closure S" . + finally have e: "S = \(t ` S) \ 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 \ {}" by auto - define n where "n = INTER tk NN" + define n where "n = \(NN ` tk)" have "y \ n" "open n" using inUS NN \tk \ {0..1}\ \finite tk\ 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 \ {}" using \tk \ {}\ by auto - show "{0..1} \ UNION tk K" + show "{0..1} \ \(K ` tk)" using tk by auto show "\B. B \ K ` tk \ open B" using \tk \ {0..1}\ K by auto diff -r e0f68a507683 -r b021008c5397 src/HOL/Analysis/Improper_Integral.thy --- 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 \(snd ` S)" by (auto intro: S tagged_partial_division_of_Union_self division_of_tagged_division) - show "UNION S snd \ cbox a b" + show "\(snd ` S) \ cbox a b" using S by force show "a \ i \ c \ i" "c \ i \ b \ 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 \(x, L) \ A\ \A \ T''\ \T'' \ T'\ by blast - have "A tagged_division_of UNION A snd" + have "A tagged_division_of \(snd ` A)" using A_tagged tagged_partial_division_of_Union_self by auto then have "interior (K \ {x. x \ i \ c}) = {}" apply (rule tagged_division_split_left_inj [OF _ \(x,K) \ A\ \(x,L) \ A\]) @@ -1016,7 +1016,7 @@ proof - obtain u v where uv: "L = cbox u v" using T'_tagged \(x, L) \ B\ \B \ T''\ \T'' \ T'\ by blast - have "B tagged_division_of UNION B snd" + have "B tagged_division_of \(snd ` B)" using B_tagged tagged_partial_division_of_Union_self by auto then have "interior (K \ {x. c \ x \ i}) = {}" apply (rule tagged_division_split_right_inj [OF _ \(x,K) \ B\ \(x,L) \ B\]) diff -r e0f68a507683 -r b021008c5397 src/HOL/Analysis/Measure_Space.thy --- 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 @@ (\A. range A \ M \ incseq A \ (\i. A i) \ M \ (\i. f (A i)) \ f (\i. A i))" unfolding countably_additive_def proof safe - assume count_sum: "\A. range A \ M \ disjoint_family A \ UNION UNIV A \ M \ (\i. f (A i)) = f (UNION UNIV A)" + assume count_sum: "\A. range A \ M \ disjoint_family A \ \(A ` UNIV) \ M \ (\i. f (A i)) = f (\(A ` UNIV))" fix A :: "nat \ 'a set" assume A: "range A \ M" "incseq A" "(\i. A i) \ M" then have dA: "range (disjointed A) \ 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 I F) = measure M (F x) + measure M (UNION I F)" + have "measure M (F x \ \(F ` I)) = measure M (F x) + measure M (\(F ` I))" by (rule measure_Un_AE) (use insert in \auto simp: pairwise_insert\) with insert show ?case by (simp add: pairwise_insert ) @@ -3132,7 +3132,7 @@ lemma le_measureD3: "A \ B \ sets A = sets B \ emeasure A X \ 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 \ Pow (UNION S space)" +lemma UN_space_closed: "\(sets ` S) \ Pow (\(space ` S))" using sets.space_closed by auto definition Sup_lexord :: "('a \ 'b::complete_lattice) \ ('a set \ 'a) \ ('a set \ 'a) \ 'a set \ 'a" @@ -3245,10 +3245,10 @@ with ij show "\k\{P. finite P \ P \ M}. \n\N. ?\ i (F n) \ ?\ k (F n) \ ?\ j (F n) \ ?\ k (F n)" by (safe intro!: bexI[of _ "i \ j"]) auto next - show "(SUP P \ {P. finite P \ P \ M}. \n. ?\ P (F n)) = (SUP P \ {P. finite P \ P \ M}. ?\ P (UNION UNIV F))" + show "(SUP P \ {P. finite P \ P \ M}. \n. ?\ P (F n)) = (SUP P \ {P. finite P \ P \ M}. ?\ P (\(F ` UNIV)))" proof (intro SUP_cong refl) fix i assume i: "i \ {P. finite P \ P \ M}" - show "(\n. ?\ i (F n)) = ?\ i (UNION UNIV F)" + show "(\n. ?\ i (F n)) = ?\ i (\(F ` UNIV))" proof cases assume "i \ {}" with i ** show ?thesis apply (intro suminf_emeasure \disjoint_family F\) @@ -3294,9 +3294,9 @@ next fix a S assume "a \ A" and a: "space a = (\a\A. space a)" and S: "S = {a' \ A. space a' = space a}" and neq: "\aa. aa \ S \ sets aa \ (\a\S. sets a)" - have sp_a: "space a = (UNION S space)" + have sp_a: "space a = (\(space ` S))" using \a\A\ by (auto simp: S) - show "x \ sigma (UNION S space) (UNION S sets)" + show "x \ sigma (\(space ` S)) (\(sets ` S))" proof cases assume [simp]: "space x = space a" have "sets x \ (\a\S. sets a)" @@ -3363,19 +3363,19 @@ unfolding Sup_measure_def proof (intro Sup_lexord[where P="\y. y \ x"]) assume "\a. a \ A \ space a \ (\a\A. space a)" - show "sigma (UNION A space) {} \ x" + show "sigma (\(space ` A)) {} \ x" using x[THEN le_measureD1] by (subst sigma_le_iff) auto next fix a S assume "a \ A" "space a = (\a\A. space a)" and S: "S = {a' \ A. space a' = space a}" "\a. a \ S \ sets a \ (\a\S. sets a)" - have "UNION S space \ space x" + have "\(space ` S) \ space x" using S le_measureD1[OF x] by auto moreover - have "UNION S space = space a" + have "\(space ` S) = space a" using \a\A\ S by auto - then have "space x = UNION S space \ UNION S sets \ sets x" + then have "space x = \(space ` S) \ \(sets ` S) \ sets x" using \a \ A\ le_measureD2[OF x] by (auto simp: S) - ultimately show "sigma (UNION S space) (UNION S sets) \ x" + ultimately show "sigma (\(space ` S)) (\(sets ` S)) \ x" by (subst sigma_le_iff) simp_all next fix a b S S' assume "a \ A" and a: "space a = (\a\A. space a)" and S: "S = {a' \ A. space a' = space a}" @@ -3504,17 +3504,17 @@ assumes ch: "Complete_Partial_Order.chain (\) (M ` A)" and "A \ {}" shows "emeasure (SUP i\A. M i) X = (SUP i\A. emeasure (M i) X)" proof (subst emeasure_SUP[OF sets \A \ {}\]) - show "(SUP J\{J. J \ {} \ finite J \ J \ A}. emeasure (SUPREMUM J M) X) = (SUP i\A. emeasure (M i) X)" + show "(SUP J\{J. J \ {} \ finite J \ J \ A}. emeasure (Sup (M ` J)) X) = (SUP i\A. emeasure (M i) X)" proof (rule SUP_eq) fix J assume "J \ {J. J \ {} \ finite J \ J \ A}" then have J: "Complete_Partial_Order.chain (\) (M ` J)" "finite J" "J \ {}" and "J \ A" using ch[THEN chain_subset, of "M`J"] by auto with in_chain_finite[OF J(1)] obtain j where "j \ J" "(SUP j\J. M j) = M j" by auto - with \J \ A\ show "\j\A. emeasure (SUPREMUM J M) X \ emeasure (M j) X" + with \J \ A\ show "\j\A. emeasure (Sup (M ` J)) X \ emeasure (M j) X" by auto next - fix j assume "j\A" then show "\i\{J. J \ {} \ finite J \ J \ A}. emeasure (M j) X \ emeasure (SUPREMUM i M) X" + fix j assume "j\A" then show "\i\{J. J \ {} \ finite J \ J \ A}. emeasure (M j) X \ emeasure (Sup (M ` i)) X" by (intro bexI[of _ "{j}"]) auto qed qed @@ -3584,7 +3584,7 @@ assumes "\m. m \ M \ sets m \ sets N" shows "sets (Sup M) \ sets N" proof - - have *: "UNION M space = space N" + have *: "\(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 \m \ M\) have "f \ measurable N (sigma (\m\M. space m) (\m\M. sets m))" proof (rule measurable_measure_of) - show "f \ space N \ UNION M space" + show "f \ space N \ \(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 (\m\M. space m) (\m\M. sets m)) = measurable N (Sup M)" diff -r e0f68a507683 -r b021008c5397 src/HOL/Analysis/Nonnegative_Lebesgue_Integration.thy --- 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 \ {g. simple_function M g \ g \ f \ (\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 \ f" - show "integral\<^sup>S M g \ SUPREMUM ?A ?f" + show "integral\<^sup>S M g \ Sup (?A ` ?f)" proof cases assume ae: "AE x in M. g x \ top" let ?G = "{x \ space M. g x \ 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 "\ \ SUPREMUM ?A ?f" + also have "\ \ 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. (\\<^sup>Sx. of_nat n * indicator ?G x \M))" by (simp add: ennreal_SUP_of_nat_eq_top ennreal_top_eq_mult_iff SUP_mult_right_ennreal[symmetric]) - also have "\ \ SUPREMUM ?A ?f" + also have "\ \ 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 \ 'b" assume C: "incseq C" - with sup_continuous_mono[OF f] show "(\\<^sup>+ y. f y (SUPREMUM UNIV C) \M) = (SUP i. \\<^sup>+ y. f y (C i) \M)" + with sup_continuous_mono[OF f] show "(\\<^sup>+ y. f y (Sup (C ` UNIV)) \M) = (SUP i. \\<^sup>+ y. f y (C i) \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 "\ = (SUP i. (\\<^sup>+ x. f i x \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 = "\f. Sup (range f)"] nn_integral_cong_AE ext) finally show ?thesis . qed @@ -1027,7 +1027,7 @@ and g: "incseq g" "\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)) = (\\<^sup>+x. (SUP i. f i x) \M)" using f by (rule nn_integral_monotone_convergence_simple) @@ -1414,7 +1414,7 @@ unfolding inf_continuous_def proof safe fix C :: "nat \ 'b" assume C: "decseq C" - then show "(\\<^sup>+ y. f y (INFIMUM UNIV C) \M) = (INF i. \\<^sup>+ y. f y (C i) \M)" + then show "(\\<^sup>+ y. f y (Inf (C ` UNIV)) \M) = (INF i. \\<^sup>+ y. f y (C i) \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 "\i::nat. C i \ borel_measurable N \ (\s. integral\<^sup>N (M s) (C i) < \)" "decseq C" - with bound show "INFIMUM UNIV C \ borel_measurable N \ (\s. integral\<^sup>N (M s) (INFIMUM UNIV C) < \)" + with bound show "Inf (C ` UNIV) \ borel_measurable N \ (\s. integral\<^sup>N (M s) (Inf (C ` UNIV)) < \)" 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]: "\i. i \ I \ X i \ sets M" and I[simp]: "countable I" assumes disj: "disjoint_family_on X I" - shows "emeasure M (UNION I X) = (\\<^sup>+i. emeasure M (X i) \count_space I)" + shows "emeasure M (\(X ` I)) = (\\<^sup>+i. emeasure M (X i) \count_space I)" proof - - have eq: "\x. indicator (UNION I X) x = \\<^sup>+ i. indicator (X i) x \count_space I" + have eq: "\x. indicator (\(X ` I)) x = \\<^sup>+ i. indicator (X i) x \count_space I" proof cases - fix x assume x: "x \ UNION I X" + fix x assume x: "x \ \(X ` I)" then obtain j where j: "x \ X j" "j \ I" by auto with disj have "\i. i \ I \ 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) = (\\<^sup>+x. indicator (UNION I X) x \M)" + have "emeasure M (\(X ` I)) = (\\<^sup>+x. indicator (\(X ` I)) x \M)" by simp also have "\ = (\\<^sup>+i. \\<^sup>+x. indicator (X i) x \M \count_space I)" by (simp add: eq nn_integral_count_space_nn_integral) diff -r e0f68a507683 -r b021008c5397 src/HOL/Analysis/Path_Connected.thy --- 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 \ k" "finite T" "k \ \((\x. k \ u x) ` T)" by (metis finite_subset_image) - have Tuv: "UNION T u \ UNION T v" + have Tuv: "\(u ` T) \ \(v ` T)" using T that by (force simp: dest!: uv) show ?thesis apply (rule_tac x="\(u ` T)" in exI) diff -r e0f68a507683 -r b021008c5397 src/HOL/Analysis/Polytope.thy --- 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 \ U)" by (simp add: \convex T\ \convex U\ convex_Int) have "(\x\T. closed_segment z x) \ (\x\U. closed_segment z x) - \ (if T \ U = {} then {z} else UNION (T \ U) (closed_segment z))" (is "_ \ ?IF") + \ (if T \ U = {} then {z} else \((closed_segment z) ` (T \ U)))" (is "_ \ ?IF") proof clarify fix x t u assume xt: "x \ closed_segment z t" diff -r e0f68a507683 -r b021008c5397 src/HOL/Analysis/Set_Integral.thy --- 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 \ UNION F A = {}" + then have "A x \ \(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 (\i. A i) (\x. norm (f x))" by simp qed - show "LINT x|M. indicator (UNION UNIV A) x *\<^sub>R f x = LINT x|M. (\i. indicator (A i) x *\<^sub>R f x)" + show "LINT x|M. indicator (\(A ` UNIV)) x *\<^sub>R f x = LINT x|M. (\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 "\i. (\x. indicator (A i) x *\<^sub>R f x) \ borel_measurable M" using int_A integrable_iff_bounded set_integrable_def by blast - show "(\x. indicator (UNION UNIV A) x *\<^sub>R f x) \ borel_measurable M" + show "(\x. indicator (\(A ` UNIV)) x *\<^sub>R f x) \ borel_measurable M" using integrable_iff_bounded intgbl set_integrable_def by blast show "integrable M (\x. indicator (\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 (\i. A i) f" using int0 by (rule set_integrable_subset) (insert A, auto simp: decseq_def) - with int_A show "(\x. indicat_real (INTER UNIV A) x *\<^sub>R f x) \ borel_measurable M" + with int_A show "(\x. indicat_real (\(A ` UNIV)) x *\<^sub>R f x) \ borel_measurable M" "\i. (\x. indicat_real (A i) x *\<^sub>R f x) \ borel_measurable M" by (auto simp: set_integrable_def) show "\i. AE x in M. norm (indicator (A i) x *\<^sub>R f x) \ indicator (A 0) x *\<^sub>R norm (f x)" diff -r e0f68a507683 -r b021008c5397 src/HOL/Analysis/Sigma_Algebra.thy --- 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 \ disjoint (A ` I) \ (\i. i \ I \ A i \ generated_ring) \ UNION I A \ generated_ring" + "finite I \ disjoint (A ` I) \ (\i. i \ I \ A i \ generated_ring) \ \(A ` I) \ 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 \ I \ {} \ (\i. i \ I \ A i \ generated_ring) \ INTER I A \ generated_ring" + "finite I \ I \ {} \ (\i. i \ I \ A i \ generated_ring) \ \(A ` I) \ generated_ring" by (intro generated_ring_Inter) auto lemma (in semiring_of_sets) generating_ring: diff -r e0f68a507683 -r b021008c5397 src/HOL/Analysis/Starlike.thy --- 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) \ F x" and Fin: "F x \ \" if "x \ S" for x by metis - then obtain \ where "\ \ G ` S" "countable \" "\\ = UNION S G" + then obtain \ where "\ \ G ` S" "countable \" "\\ = \(G ` S)" using Lindelof [of "G ` S"] by (metis image_iff) - then obtain K where K: "K \ S" "countable K" and eq: "UNION K G = UNION S G" + then obtain K where K: "K \ S" "countable K" and eq: "\(G ` K) = \(G ` S)" by (metis countable_subset_image) with False Gin have "K \ {}" by force then obtain a :: "nat \ 'a" where "range a = K" @@ -7885,7 +7885,7 @@ obtain I where "finite I" and I: "K \ (\i\I. interior (f i))" proof (rule compactE_image [OF \compact K\]) show "K \ (\n. interior (f n))" - using \K \ S\ \UNION UNIV f = S\ * by blast + using \K \ S\ \\(f ` UNIV) = S\ * by blast qed auto { fix n assume n: "Max I \ n" diff -r e0f68a507683 -r b021008c5397 src/HOL/Analysis/Topology_Euclidean_Space.thy --- 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" "\i. i \ x \ finite i \ i \ B" - and y: "b = UNION y Inter" "\i. i \ y \ finite i \ i \ B" + then obtain x y where x: "a = \(Inter ` x)" "\i. i \ x \ finite i \ i \ B" + and y: "b = \(Inter ` y)" "\i. i \ y \ finite i \ i \ B" by blast show ?case unfolding x y Int_UN_distrib2 @@ -450,10 +450,10 @@ case (UN K) then have "\k\K. \B'\{b. finite b \ b \ B}. UNION B' Inter = k" by auto then obtain k where - "\ka\K. k ka \ {b. finite b \ b \ B} \ UNION (k ka) Inter = ka" + "\ka\K. k ka \ {b. finite b \ b \ B} \ \(Inter ` (k ka)) = ka" unfolding bchoice_iff .. then show "\B'\{b. finite b \ b \ B}. UNION B' Inter = \K" - by (intro exI[of _ "UNION K k"]) auto + by (intro exI[of _ "\(k ` K)"]) auto next case (Basis S) then show ?case diff -r e0f68a507683 -r b021008c5397 src/HOL/Analysis/Uniform_Limit.thy --- 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 "\s. s \ S \ uniform_limit (h s) f g F" - shows "uniform_limit (UNION S h) f g F" + shows "uniform_limit (\(h ` S)) f g F" using assms by induct (auto intro: uniform_limit_on_empty uniform_limit_on_Un) diff -r e0f68a507683 -r b021008c5397 src/HOL/Analysis/Vitali_Covering_Theorem.thy --- 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 \e > 0\ le1) finally show ?thesis . qed - have "UNION C U \ lmeasurable" "?\ (\(U ` C)) \ e" + have "\(U ` C) \ lmeasurable" "?\ (\(U ` C)) \ e" using \e > 0\ Um lee by(auto intro!: fmeasurable_UN_bound [OF \countable C\] measure_UN_bound [OF \countable C\]) } - moreover have "?\ ?T = ?\ (UNION C U)" - proof (rule measure_negligible_symdiff [OF \UNION C U \ lmeasurable\]) - show "negligible((UNION C U - ?T) \ (?T - UNION C U))" + moreover have "?\ ?T = ?\ (\(U ` C))" + proof (rule measure_negligible_symdiff [OF \\(U ` C) \ lmeasurable\]) + show "negligible((\(U ` C) - ?T) \ (?T - \(U ` C)))" by (force intro!: negligible_subset [OF negC]) qed ultimately show "?T \ lmeasurable" "?\ ?T \ e" diff -r e0f68a507683 -r b021008c5397 src/HOL/Bali/Basis.thy --- 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) \ \y. P y \ finite (range (f y)) \ - finite {f y x |x y. P y}" - apply (subgoal_tac "{f y x |x y. P y} = UNION (Collect P) (\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)" + "\y. P y \ finite (range (f y))" +proof - + have "{f y x |x y. P y} = (\y\Collect P. range (f y))" + by auto + with that show ?thesis by simp +qed lemma list_all2_trans: "\a b c. P1 a b \ P2 b c \ P3 a c \ \xs2 xs3. list_all2 P1 xs1 xs2 \ list_all2 P2 xs2 xs3 \ list_all2 P3 xs1 xs3" diff -r e0f68a507683 -r b021008c5397 src/HOL/Computational_Algebra/Primes.thy --- 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 \ f ` A" - shows "prime_factors (prod f A) = UNION A (prime_factors \ f)" + shows "prime_factors (prod f A) = \((prime_factors \ f) ` A)" using assms by (simp add: prod_unfold_prod_mset prime_factorization_prod_mset) lemma prime_factors_fact: diff -r e0f68a507683 -r b021008c5397 src/HOL/Decision_Procs/MIR.thy --- 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\'b\'c) set" and f :: "('a\'b\'c) \ 'd list" and g assume "\ (a,b,c) \ M. f (a,b,c) = g a b c" - thus "(UNION M (\ (a,b,c). set (f (a,b,c)))) = (UNION M (\ (a,b,c). set (g a b c)))" + thus "(\(a, b, c)\M. set (f (a, b, c))) = (\(a, b, c)\M. set (g a b c))" by (auto simp add: split_def) qed have U3': "\ (p,n,s) \ {(p,n,s). (p,n,s) \ ?SS a \ n<0}. ?ff (p,n,s) = map (?f(p,n,s)) [n..0]" by auto - hence U3: "(UNION {(p,n,s). (p,n,s) \ ?SS a \ n<0} (\ (p,n,s). set (?ff (p,n,s)))) = - (UNION {(p,n,s). (p,n,s)\ ?SS a\n<0} (\(p,n,s). set (map (?f(p,n,s)) [n..0])))" - proof- + hence U3: "(\ ((\(p,n,s). set (?ff (p,n,s))) ` {(p,n,s). (p,n,s) \ ?SS a \ n<0})) = + (\ ((\(p,n,s). set (map (?f(p,n,s)) [n..0])) ` {(p,n,s). (p,n,s)\ ?SS a\n<0}))" + proof - fix M :: "('a\'b\'c) set" and f :: "('a\'b\'c) \ 'd list" and g assume "\ (a,b,c) \ M. f (a,b,c) = g a b c" - thus "(UNION M (\ (a,b,c). set (f (a,b,c)))) = (UNION M (\ (a,b,c). set (g a b c)))" + thus "(\(a, b, c)\M. set (f (a, b, c))) = (\(a, b, c)\M. set (g a b c))" by (auto simp add: split_def) qed - have "?SS (Floor a) = UNION (?SS a) (\x. set (?ff x))" + have "?SS (Floor a) = \ ((\x. set (?ff x)) ` ?SS a)" by auto - also have "\ = UNION (?SS a) (\ (p,n,s). set (?ff (p,n,s)))" by blast + also have "\ = \ ((\ (p,n,s). set (?ff (p,n,s))) ` ?SS a)" + by blast also have "\ = ((UNION {(p,n,s). (p,n,s) \ ?SS a \ n=0} (\ (p,n,s). set (?ff (p,n,s)))) Un (UNION {(p,n,s). (p,n,s) \ ?SS a \ n>0} (\ (p,n,s). set (?ff (p,n,s)))) Un @@ -3535,7 +3536,7 @@ proof- fix M :: "('a\'b\'c) set" and f :: "('a\'b\'c) \ 'd list" and g assume "\ (a,b,c) \ M. f (a,b,c) = g a b c" - thus "(UNION M (\ (a,b,c). set (f (a,b,c)))) = (UNION M (\ (a,b,c). set (g a b c)))" + thus "(\(a, b, c)\M. set (f (a, b, c))) = (\(a, b, c)\M. set (g a b c))" by (auto simp add: split_def) qed have U3': "\ (p,n,s) \ {(p,n,s). (p,n,s) \ ?SS a \ n<0}. ?ff (p,n,s) = map (?f(p,n,s)) [n..0]" @@ -3544,12 +3545,12 @@ proof- fix M :: "('a\'b\'c) set" and f :: "('a\'b\'c) \ 'd list" and g assume "\ (a,b,c) \ M. f (a,b,c) = g a b c" - thus "(UNION M (\ (a,b,c). set (f (a,b,c)))) = (UNION M (\ (a,b,c). set (g a b c)))" + thus "(\(a, b, c)\M. set (f (a, b, c))) = (\(a, b, c)\M. set (g a b c))" by (auto simp add: split_def) qed - have "?SS (Floor a) = UNION (?SS a) (\x. set (?ff x))" by auto - also have "\ = UNION (?SS a) (\ (p,n,s). set (?ff (p,n,s)))" by blast + have "?SS (Floor a) = \ ((\x. set (?ff x)) ` ?SS a)" by auto + also have "\ = \ ((\ (p,n,s). set (?ff (p,n,s))) ` ?SS a)" by blast also have "\ = ((UNION {(p,n,s). (p,n,s) \ ?SS a \ n=0} (\ (p,n,s). set (?ff (p,n,s)))) Un (UNION {(p,n,s). (p,n,s) \ ?SS a \ n>0} (\ (p,n,s). set (?ff (p,n,s)))) Un diff -r e0f68a507683 -r b021008c5397 src/HOL/Hoare_Parallel/RG_Hoare.thy --- 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="\j. H j \ M \ UNION (S j) (T j) \ (L j)" for H M S T L in allE) +apply(erule_tac x=i and P="\j. H j \ M \ \((T j) ` (S j)) \ (L j)" for H M S T L in allE) apply simp apply(erule subsetD) apply simp diff -r e0f68a507683 -r b021008c5397 src/HOL/Library/Countable_Complete_Lattices.thy --- 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 \ 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 \ (INF x\insert a A. f x) = inf (f a) (INFIMUM A f)" +lemma ccINF_insert [simp]: "countable A \ (INF x\insert a A. f x) = inf (f a) (Inf (f ` A))" unfolding image_insert by simp lemma ccSup_insert [simp]: "countable A \ 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 \ (SUP x\insert a A. f x) = sup (f a) (SUPREMUM A f)" +lemma ccSUP_insert [simp]: "countable A \ (SUP x\insert a A. f x) = sup (f a) (Sup (f ` A))" unfolding image_insert by simp lemma ccINF_empty [simp]: "(INF x\{}. f x) = top" diff -r e0f68a507683 -r b021008c5397 src/HOL/Library/Countable_Set_Type.thy --- 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 \ 'a cset" where "cUnion A = cUNION A id" -lemma Union_conv_UNION: "\A = UNION A id" +lemma Union_conv_UNION: "\A = \(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) (\A. UNION A id) (\A. cUNION A id)" + have "rel_fun (pcr_cset (pcr_cset A)) (pcr_cset A) (\A. \(id ` A)) (\A. cUNION A id)" by transfer_prover then show ?thesis by (simp flip: cUnion_def) qed diff -r e0f68a507683 -r b021008c5397 src/HOL/Library/Disjoint_Sets.thy --- 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 (\i\I. A i) (\i\I. A' i)" unfolding bij_betw_def proof - from bij show eq: "f ` UNION I A = UNION I A'" + from bij show eq: "f ` \(A ` I) = \(A' ` I)" by (auto simp: bij_betw_def image_UN) - show "inj_on f (UNION I A)" + show "inj_on f (\(A ` I))" proof (rule inj_onI, clarify) fix i j x y assume A: "i \ I" "j \ I" "x \ A i" "y \ A j" and B: "f x = f y" from A bij[of i] bij[of j] have "f x \ A' i" "f y \ A' j" @@ -179,7 +179,7 @@ \ lemma infinite_disjoint_family_imp_infinite_UNION: assumes "\finite A" "\x. x \ A \ f x \ {}" "disjoint_family_on f A" - shows "\finite (UNION A f)" + shows "\finite (\(f ` A))" proof - define g where "g x = (SOME y. y \ f x)" for x have g: "g x \ f x" if "x \ A" for x @@ -191,7 +191,7 @@ with A \x \ y\ assms show False by (auto simp: disjoint_family_on_def inj_on_def) qed - from g have "g ` A \ UNION A f" by blast + from g have "g ` A \ \(f ` A)" by blast moreover from inj_on_g \\finite A\ have "\finite (g ` A)" using finite_imageD by blast ultimately show ?thesis using finite_subset by blast diff -r e0f68a507683 -r b021008c5397 src/HOL/Library/Extended_Nonnegative_Real.thy --- 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 \ ennreal" - shows "incseq f \ incseq g \ (SUP i. f i + g i) = SUPREMUM UNIV f + SUPREMUM UNIV g" + shows "incseq f \ incseq g \ (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 \ {} \ \f::nat \ ennreal. range f \ g`A \ SUPREMUM A g = SUPREMUM UNIV f" + "A \ {} \ \f::nat \ ennreal. range f \ g`A \ Sup (g ` A) = Sup (f ` UNIV)" using ennreal_Sup_countable_SUP [of "g`A"] by auto lemma of_nat_tendsto_top_ennreal: "(\n::nat. of_nat n :: ennreal) \ top" diff -r e0f68a507683 -r b021008c5397 src/HOL/Library/Extended_Real.thy --- 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 :: "_ \ ereal" - shows "A \ {} \ l \ -\ \ u \ \ \ \a\A. l \ f a \ f a \ u \ \SUPREMUM A f\ \ \" + shows "A \ {} \ l \ -\ \ u \ \ \ \a\A. l \ f a \ f a \ u \ \Sup (f ` A)\ \ \" 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 :: "_ \ ereal" - shows "A \ {} \ l \ -\ \ u \ \ \ \a\A. l \ f a \ f a \ u \ \INFIMUM A f\ \ \" + shows "A \ {} \ l \ -\ \ u \ \ \ \a\A. l \ f a \ f a \ u \ \Inf (f ` A)\ \ \" 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 \ ereal" assumes "\i. f i + y \ z" and "y \ -\" - shows "SUPREMUM UNIV f + y \ z" + shows "Sup (f ` UNIV) + y \ z" unfolding SUP_ereal_add_left[OF UNIV_not_empty \y \ -\\, symmetric] by (rule SUP_least assms)+ @@ -2351,7 +2351,7 @@ fixes f g :: "nat \ ereal" assumes inc: "incseq f" "incseq g" and pos: "\i. f i \ -\" "\i. 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)" 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 \ ereal" assumes "decseq f" "decseq g" and fin: "\i. f i \ \" "\i. g i \ \" - 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) < \" "(INF i. g i) < \" 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 "\ = INFIMUM UNIV f + INFIMUM UNIV g" + also have "\ = 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 \ ereal" assumes inc: "incseq f" "incseq g" and pos: "\i. 0 \ f i" "\i. 0 \ 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 \ -\" "g i \ -\" @@ -2440,7 +2440,7 @@ fixes f g :: "'a \ nat \ ereal" assumes "\n. n \ A \ incseq (f n)" and pos: "\n i. n \ A \ 0 \ f n i" - shows "(SUP i. \n\A. f n i) = (\n\A. SUPREMUM UNIV (f n))" + shows "(SUP i. \n\A. f n i) = (\n\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 \ {} \ \f::nat \ ereal. range f \ g`A \ SUPREMUM A g = SUPREMUM UNIV f" + "A \ {} \ \f::nat \ ereal. range f \ g`A \ 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 = "\P g. INFIMUM (Collect P) g" + let ?INF = "\P g. Inf (g ` (Collect P))" show "?F \ {}" by (auto intro: eventually_True) show "(SUP P\?F. ?INF P g) \ - \" @@ -3238,7 +3238,7 @@ by (intro add_mono INF_mono) auto also have "\ = (SUP P'\?F. ?INF ?P' f + ?INF P' g)" proof (rule SUP_ereal_add_right[symmetric]) - show "INFIMUM {x. P x \ 0 \ f x} f \ - \" + show "Inf (f ` {x. P x \ 0 \ f x}) \ - \" unfolding bot_ereal_def[symmetric] INF_eq_bot_iff by (auto intro!: exI[of _ 0] ev simp: bot_ereal_def) qed fact diff -r e0f68a507683 -r b021008c5397 src/HOL/Library/Finite_Map.thy --- 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 (=) (=) ===> (=)) (\x. UNION (range x) set_option) fmran'" + "(pcr_fmap (=) (=) ===> (=)) (\x. \(set_option ` (range x))) fmran'" unfolding fmran'_def fmap.pcr_cr_eq cr_fmap_def by fastforce lemma fmrel_transfer[transfer_rule]: diff -r e0f68a507683 -r b021008c5397 src/HOL/Library/Indicator_Function.thy --- 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 @@ \ lemma indicator_UN_disjoint: - "finite A \ disjoint_family_on f A \ indicator (UNION A f) x = (\y\A. indicator (f y) x)" + "finite A \ disjoint_family_on f A \ indicator (\(f ` A)) x = (\y\A. indicator (f y) x)" by (induct A rule: finite_induct) (auto simp: disjoint_family_on_def indicator_def split: if_splits) diff -r e0f68a507683 -r b021008c5397 src/HOL/Library/Liminf_Limsup.thy --- 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 \ {} \ bdd_above (f`A) \ x \ SUPREMUM A f \ (\yi\A. y < f i)" + "A \ {} \ bdd_above (f`A) \ x \ Sup (f ` A) \ (\yi\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 \ {} \ bdd_below (f`A) \ INFIMUM A f \ x \ (\y>x. \i\A. y > f i)" + "A \ {} \ bdd_below (f`A) \ Inf (f ` A) \ x \ (\y>x. \i\A. y > f i)" using cInf_le_iff [of "f ` A"] by simp lemma cInf_le_iff_less: @@ -89,13 +89,13 @@ abbreviation "limsup \ Limsup sequentially" lemma Liminf_eqI: - "(\P. eventually P F \ INFIMUM (Collect P) f \ x) \ - (\y. (\P. eventually P F \ INFIMUM (Collect P) f \ y) \ x \ y) \ Liminf F f = x" + "(\P. eventually P F \ Inf (f ` (Collect P)) \ x) \ + (\y. (\P. eventually P F \ Inf (f ` (Collect P)) \ y) \ x \ y) \ Liminf F f = x" unfolding Liminf_def by (auto intro!: SUP_eqI) lemma Limsup_eqI: - "(\P. eventually P F \ x \ SUPREMUM (Collect P) f) \ - (\y. (\P. eventually P F \ y \ SUPREMUM (Collect P) f) \ y \ x) \ Limsup F f = x" + "(\P. eventually P F \ x \ Sup (f ` (Collect P))) \ + (\y. (\P. eventually P F \ y \ Sup (f ` (Collect P))) \ y \ x) \ Limsup F f = x" unfolding Limsup_def by (auto intro!: INF_eqI) lemma liminf_SUP_INF: "liminf f = (SUP n. INF m\{n..}. f m)" @@ -139,7 +139,7 @@ proof (safe intro!: SUP_mono) fix P assume "eventually P F" with ev have "eventually (\x. f x \ g x \ P x) F" (is "eventually ?Q F") by (rule eventually_conj) - then show "\Q\{P. eventually P F}. INFIMUM (Collect P) f \ INFIMUM (Collect Q) g" + then show "\Q\{P. eventually P F}. Inf (f ` (Collect P)) \ 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 (\x. f x \ g x \ P x) F" (is "eventually ?Q F") by (rule eventually_conj) - then show "\Q\{P. eventually P F}. SUPREMUM (Collect Q) f \ SUPREMUM (Collect P) g" + then show "\Q\{P. eventually P F}. Sup (f ` (Collect Q)) \ Sup (g ` (Collect P))" by (intro bexI[of _ ?Q]) (auto intro!: SUP_mono) qed @@ -183,13 +183,13 @@ then have "eventually (\x. P x \ Q x) F" (is "eventually ?C F") by (rule eventually_conj) then have not_False: "(\x. P x \ Q x) \ (\x. False)" using ntriv by (auto simp add: eventually_False) - have "INFIMUM (Collect P) f \ INFIMUM (Collect ?C) f" + have "Inf (f ` (Collect P)) \ Inf (f ` (Collect ?C))" by (rule INF_mono) auto - also have "\ \ SUPREMUM (Collect ?C) f" + also have "\ \ Sup (f ` (Collect ?C))" using not_False by (intro INF_le_SUP) auto - also have "\ \ SUPREMUM (Collect Q) f" + also have "\ \ Sup (f ` (Collect Q))" by (rule SUP_mono) auto - finally show "INFIMUM (Collect P) f \ SUPREMUM (Collect Q) f" . + finally show "Inf (f ` (Collect P)) \ Sup (f ` (Collect Q))" . qed lemma Liminf_bounded: @@ -219,21 +219,21 @@ shows "C \ Liminf F X \ (\yx. y < X x) F)" proof - have "eventually (\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 "\P. eventually P F \ y < INFIMUM (Collect P) X" + have "\P. eventually P F \ y < Inf (X ` (Collect P))" if "y < C" and y: "\yx. y < X x) F" for y P proof (cases "\z. y < z \ z < C") case True then obtain z where z: "y < z \ z < C" .. - moreover from z have "z \ INFIMUM {x. z < X x} X" + moreover from z have "z \ Inf (X ` {x. z < X x})" by (auto intro!: INF_greatest) ultimately show ?thesis using y by (intro exI[of _ "\x. z < X x"]) auto next case False - then have "C \ INFIMUM {x. y < X x} X" + then have "C \ Inf (X ` {x. y < X x})" by (intro INF_greatest) auto with \y < C\ show ?thesis using y by (intro exI[of _ "\x. y < X x"]) auto @@ -246,22 +246,22 @@ fixes X :: "_ \ _ :: complete_linorder" shows "C \ Limsup F X \ (\y>C. eventually (\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 (\x. y > X x) F" by (auto elim!: eventually_mono dest: SUP_lessD) } moreover { fix y P assume "y > C" and y: "\y>C. eventually (\x. y > X x) F" - have "\P. eventually P F \ y > SUPREMUM (Collect P) X" + have "\P. eventually P F \ y > Sup (X ` (Collect P))" proof (cases "\z. C < z \ z < y") case True then obtain z where z: "C < z \ z < y" .. - moreover from z have "z \ SUPREMUM {x. z > X x} X" + moreover from z have "z \ Sup (X ` {x. X x < z})" by (auto intro!: SUP_least) ultimately show ?thesis using y by (intro exI[of _ "\x. z > X x"]) auto next case False - then have "C \ SUPREMUM {x. y > X x} X" + then have "C \ Sup (X ` {x. X x < y})" by (intro SUP_least) (auto simp: not_less) with \y > C\ show ?thesis using y by (intro exI[of _ "\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 (\x. INFIMUM (Collect P) f \ f x) F" + then have "eventually (\x. Inf (f ` (Collect P)) \ f x) F" by eventually_elim (auto intro!: INF_lower) - then show "INFIMUM (Collect P) f \ f0" + then show "Inf (f ` (Collect P)) \ f0" by (rule tendsto_le[OF ntriv lim tendsto_const]) next - fix y assume upper: "\P. eventually P F \ INFIMUM (Collect P) f \ y" + fix y assume upper: "\P. eventually P F \ Inf (f ` (Collect P)) \ y" show "f0 \ y" proof cases assume "\z. y < z \ z < f0" then obtain z where "y < z \ z < f0" .. - moreover have "z \ INFIMUM {x. z < f x} f" + moreover have "z \ 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 (\x. f0 \ f x) F" using discrete by (auto elim!: eventually_mono) - then have "INFIMUM {x. f0 \ f x} f \ y" + then have "Inf (f ` {x. f0 \ f x}) \ y" by (rule upper) - moreover have "f0 \ INFIMUM {x. f0 \ f x} f" + moreover have "f0 \ Inf (f ` {x. f0 \ f x})" by (intro INF_greatest) simp ultimately show "f0 \ 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 (\x. f x \ SUPREMUM (Collect P) f) F" + then have "eventually (\x. f x \ Sup (f ` (Collect P))) F" by eventually_elim (auto intro!: SUP_upper) - then show "f0 \ SUPREMUM (Collect P) f" + then show "f0 \ Sup (f ` (Collect P))" by (rule tendsto_le[OF ntriv tendsto_const lim]) next - fix y assume lower: "\P. eventually P F \ y \ SUPREMUM (Collect P) f" + fix y assume lower: "\P. eventually P F \ y \ Sup (f ` (Collect P))" show "y \ f0" proof (cases "\z. f0 < z \ z < y") case True then obtain z where "f0 < z \ z < y" .. - moreover have "SUPREMUM {x. f x < z} f \ z" + moreover have "Sup (f ` {x. f x < z}) \ 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 (\x. f x \ f0) F" using False by (auto elim!: eventually_mono simp: not_less) - then have "y \ SUPREMUM {x. f x \ f0} f" + then have "y \ Sup (f ` {x. f x \ f0})" by (rule lower) - moreover have "SUPREMUM {x. f x \ f0} f \ f0" + moreover have "Sup (f ` {x. f x \ f0}) \ f0" by (intro SUP_least) simp ultimately show "y \ 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 (\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 (\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 "\ = (SUP P \ {P. eventually P F}. INFIMUM (g ` Collect P) f)" + also have "\ = (SUP P \ {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 "\ = (INF P \ {P. eventually P F}. SUPREMUM (g ` Collect P) f)" + also have "\ = (INF P \ {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 "\ = (SUP P \ {P. eventually P F}. INFIMUM (g ` Collect P) f)" + also have "\ = (SUP P \ {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 "\ = (INF P \ {P. eventually P F}. SUPREMUM (g ` Collect P) f)" + also have "\ = (INF P \ {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 diff -r e0f68a507683 -r b021008c5397 src/HOL/Library/Option_ord.thy --- 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 \ {} \ Some (\x\A. f x) = (\x\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 \ SUPREMUM {f ` A |f. \Y\A. f Y \ Y} Inf" +lemma option_Inf_Sup: "\(Sup ` A) \ \(Inf ` {f ` A |f. \Y\A. f Y \ Y})" + for A :: "('a::complete_distrib_lattice option) set set" proof (cases "{} \ A") case True then show ?thesis @@ -438,8 +439,8 @@ also have "... = Some (\x\{f ` {the ` (y - {None}) |y. y \ A} |f. \Y. (\y. Y = the ` (y - {None}) \ y \ A) \ f Y \ Y}. \x) " by (simp add: Inf_Sup) - also have "... \ SUPREMUM {f ` A |f. \Y\A. f Y \ Y} Inf" - proof (cases "SUPREMUM {f ` A |f. \Y\A. f Y \ Y} Inf") + also have "... \ \ (Inf ` {f ` A |f. \Y\A. f Y \ Y})" + proof (cases "\ (Inf ` {f ` A |f. \Y\A. f Y \ Y})") case None then show ?thesis by (simp add: less_eq_option_def) next diff -r e0f68a507683 -r b021008c5397 src/HOL/Library/Order_Continuity.thy --- 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 (\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 (\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 diff -r e0f68a507683 -r b021008c5397 src/HOL/Library/Product_Order.thy --- 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:\ lemma INF_prod_alt_def: - "INFIMUM A f = (INFIMUM A (fst \ f), INFIMUM A (snd \ f))" + "Inf (f ` A) = (Inf ((fst \ f) ` A), Inf ((snd \ f) ` A))" unfolding Inf_prod_def by simp lemma SUP_prod_alt_def: - "SUPREMUM A f = (SUPREMUM A (fst \ f), SUPREMUM A (snd \ f))" + "Sup (f ` A) = (Sup ((fst \ f) ` A), Sup((snd \ 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\'b) set set" - show "INFIMUM A Sup \ SUPREMUM {f ` A |f. \Y\A. f Y \ Y} Inf" + show "Inf (Sup ` A) \ Sup (Inf ` {f ` A |f. \Y\A. f Y \ Y})" by (simp add: Sup_prod_def Inf_prod_def INF_SUP_set) qed diff -r e0f68a507683 -r b021008c5397 src/HOL/Library/Set_Algebras.thy --- 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 = (\i\I. A * M i)" - "UNION I M * A = (\i\I. M i * A)" + "A * \(M ` I) = (\i\I. A * M i)" + "\(M ` I) * A = (\i\I. M i * A)" by (auto simp: set_times_def) end diff -r e0f68a507683 -r b021008c5397 src/HOL/Library/Set_Idioms.thy --- 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: "\T. T \ \ \ P (f T)" "\T. T \ \ \ U \ (f T) = T" by metis - then have "\\'\Collect P. \\' = INTER \ f" - by (metis image_subset_iff mem_Collect_eq) - moreover have eq: "U \ INTER \ f = U \ \\" + then have "f ` \ \ Collect P" + by auto + moreover have eq: "U \ \(f ` \) = U \ \\" using f by auto ultimately show ?thesis unfolding relative_to_def intersection_of_def arbitrary_def \S = U \ \\\ - 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: "\T. T \ \ \ P (f T)" "\T. T \ \ \ U \ (f T) = T" by metis - then have "\\'\Collect P. \\' = INTER \ f" - by (metis image_subset_iff mem_Collect_eq) - moreover have eq: "U \ INTER \ f = U \ \\" + then have "f ` \ \ Collect P" + by auto + moreover have eq: "U \ \ (f ` \) = U \ \ \" using f by auto ultimately show ?thesis unfolding relative_to_def intersection_of_def \S = U \ \\\ - by (metis (no_types, hide_lams) \finite \\ f(1) finite_imageI image_subset_iff mem_Collect_eq) + using \finite \\ + 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: "\T. T \ \ \ P (f T)" "\T. T \ \ \ U \ (f T) = T" by metis - then have "\\'\Collect P. \\' = INTER \ f" - by (metis image_subset_iff mem_Collect_eq) - moreover have eq: "U \ INTER \ f = U \ \\" + then have "f ` \ \ Collect P" + by auto + moreover have eq: "U \ \ (f ` \) = U \ \ \" using f by auto ultimately show ?thesis unfolding relative_to_def intersection_of_def \S = U \ \\\ - by (metis (no_types, hide_lams) \countable \\ f(1) countable_image image_subset_iff mem_Collect_eq) + using \countable \\ countable_image + by auto qed ultimately show ?thesis by blast diff -r e0f68a507683 -r b021008c5397 src/HOL/Library/Stream.thy --- 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) = \(sset ` (sset ss))" proof safe fix x assume "x \ sset (smerge ss)" - thus "x \ UNION (sset ss) sset" + thus "x \ \(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 diff -r e0f68a507683 -r b021008c5397 src/HOL/Probability/Fin_Map.thy --- 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 \ {m. domain m \ J} = (\i. (a i \ {m. domain m \ J}))" + have "\(a ` UNIV) \ {m. domain m \ J} = (\i. (a i \ {m. domain m \ J}))" by simp also have "\ \ sets (PiF J M)" using Union by (intro sets.countable_nat_UN) auto finally show ?case . diff -r e0f68a507683 -r b021008c5397 src/HOL/Probability/Independent_Family.thy --- 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 "\A. (\i. i \ J \ A i \ ?UN j) \ INTER J A \ ?UN j" + have "\A. (\i. i \ J \ A i \ ?UN j) \ \(A ` J) \ ?UN j" using \finite J\ \J \ {}\ by (rule finite_INT) blast } note INT = this @@ -620,7 +620,7 @@ fix X assume X: "X \ tail_events A" let ?A = "(\n. sigma_sets (space M) (UNION {n..} A))" from X have "\n::nat. X \ sigma_sets (space M) (UNION {n..} A)" by (auto simp: tail_events_def) - from this[of 0] have "X \ sigma_sets (space M) (UNION UNIV A)" by simp + from this[of 0] have "X \ sigma_sets (space M) (\(A ` UNIV))" by simp then show "X \ 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 \ ?A" "x \ X" then have "\n. X \ sigma_sets (space M) (UNION {n..} A)" by auto - from this[of 0] have "X \ sigma_sets (space M) (UNION UNIV A)" by simp + from this[of 0] have "X \ sigma_sets (space M) (\(A ` UNIV))" by simp then have "X \ space M" by induct (insert A.sets_into_space, auto) with \x \ X\ show "x \ space M" by auto } { fix F :: "nat \ 'a set" and n assume "range F \ ?A" - then show "(UNION UNIV F) \ sigma_sets (space M) (UNION {n..} A)" + then show "(\(F ` UNIV)) \ 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 "(\A\\ i\I. {X i -` A \ space M |A. A \ E i}. prob (INTER I A) = (\j\I. prob (A j))) = + have "(\A\\ i\I. {X i -` A \ space M |A. A \ E i}. prob (\(A ` I)) = (\j\I. prob (A j))) = (\A\\ i\I. E i. prob ((\j\I. X j -` A j) \ space M) = (\x\I. prob (X x -` A x \ space M)))" (is "?L = ?R") proof safe @@ -920,7 +920,7 @@ from bchoice[OF this] obtain B where B: "\i\I. A i = X i -` B i \ space M" "B \ (\ i\I. E i)" by auto from \?R\[THEN bspec, OF B(2)] B(1) \I \ {}\ - show "prob (INTER I A) = (\j\I. prob (A j))" + show "prob (\(A ` I)) = (\j\I. prob (A j))" by simp qed then show ?thesis using \I \ {}\ diff -r e0f68a507683 -r b021008c5397 src/HOL/Probability/Probability_Mass_Function.thy --- 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. \ lemma pmf_of_set_UN: - assumes "finite (UNION A f)" "A \ {}" "\x. x \ A \ f x \ {}" + assumes "finite (\(f ` A))" "A \ {}" "\x. x \ A \ f x \ {}" "\x. x \ A \ card (f x) = n" "disjoint_family_on f A" - shows "pmf_of_set (UNION A f) = do {x \ pmf_of_set A; pmf_of_set (f x)}" + shows "pmf_of_set (\(f ` A)) = do {x \ 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 (\(f ` A))) x) = ereal (indicator (\x\A. f x) x / real (card (\x\A. f x)))" by (subst pmf_of_set) auto also from assms have "card (\x\A. f x) = card A * n" diff -r e0f68a507683 -r b021008c5397 src/HOL/Probability/Projective_Family.thy --- 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 "(\\. \ (t x)) \ measurable (Pi\<^sub>M UNIV (\x. M (f x))) (M x)" if x: "x \ J i" for x i using measurable_component_singleton[of "t x" "UNIV" "\x. M (f x)"] unfolding ft[OF x] by simp - then show "(\\. \x\\i. J i. \ (t x)) \ measurable IT.PF.lim (Pi\<^sub>M (UNION UNIV J) M)" + then show "(\\. \x\\i. J i. \ (t x)) \ measurable IT.PF.lim (Pi\<^sub>M (\(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 "\ = distr (distr IT.PF.lim (PiM (t`J i) (\x. M (f x))) (\\. restrict \ (t`J i))) (Pi\<^sub>M (J i) M) (\\. \n\J i. \ (t n))" diff -r e0f68a507683 -r b021008c5397 src/HOL/Probability/Stopping_Time.thy --- 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 \ 'a set" and t assume "range AA \ {A. \t. {\ \ A. T \ \ t} \ sets (F t)}" then have "(\i. {\ \ AA i. T \ \ t}) \ sets (F t)" for t by auto - also have "(\i. {\ \ AA i. T \ \ t}) = {\ \ UNION UNIV AA. T \ \ t}" + also have "(\i. {\ \ AA i. T \ \ t}) = {\ \ \(AA ` UNIV). T \ \ t}" by auto - finally show "{\ \ UNION UNIV AA. T \ \ t} \ sets (F t)" . + finally show "{\ \ \(AA ` UNIV). T \ \ t} \ sets (F t)" . qed auto lemma sets_pre_sigma: "stopping_time F T \ sets (pre_sigma T) = {A. \t. {\\A. T \ \ t} \ sets (F t)}" diff -r e0f68a507683 -r b021008c5397 src/HOL/Probability/Tree_Space.thy --- 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) \ UNION UNIV I} = + have *: "{Node l v r |l v r. (v, l, r) \ \(I ` UNIV)} = (\i. {Node l v r |l v r. (v, l, r) \ I i})" by auto show ?case unfolding * using Union(2) by (intro sets.countable_UN) auto qed diff -r e0f68a507683 -r b021008c5397 src/HOL/Probability/ex/Measure_Not_CCC.thy --- 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 = (\i. if j \ J i then F i j else X i)" for j show "(\i. X i) \ sets M" "countable (\i. J i)" "G \ (\i. J i) \ sets M" using XFJ by (auto simp: G_def Pi_iff) - show "UNION UNIV A = (UNIV - (\i. J i)) \ (\i. X i) \ (SIGMA j:\i. J i. \i. if j \ J i then F i j else X i)" + show "\(A ` UNIV) = (UNIV - (\i. J i)) \ (\i. X i) \ (SIGMA j:\i. J i. \i. if j \ J i then F i j else X i)" unfolding A_eq by (auto split: if_split_asm) qed qed diff -r e0f68a507683 -r b021008c5397 src/HOL/UNITY/Comp/Alloc.thy --- 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 (\(Acts ` (preserves allocGiv)))}" definition alloc_spec :: "'a allocState_d program set" diff -r e0f68a507683 -r b021008c5397 src/HOL/UNITY/Comp/AllocBase.thy --- 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; \i\I. \j\I. i\j \ A i Int A j = {} |] - ==> bag_of (nths l (UNION I A)) = + ==> bag_of (nths l (\(A ` I))) = (\i\I. bag_of (nths l (A i)))" apply (auto simp add: bag_of_nths) unfolding UN_simps [symmetric] diff -r e0f68a507683 -r b021008c5397 src/HOL/UNITY/Comp/AllocImpl.thy --- 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 (\(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 (\(Acts ` (preserves giv)))}" definition alloc_spec :: "'a allocState_d program set" diff -r e0f68a507683 -r b021008c5397 src/HOL/UNITY/Constrains.thy --- 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 \ B) = Always A \ Always B" by (auto simp add: Always_eq_includes_reachable) -lemma Always_INT_distrib: "Always (INTER I A) = (\i \ I. Always (A i))" +lemma Always_INT_distrib: "Always (\(A ` I)) = (\i \ I. Always (A i))" by (auto simp add: Always_eq_includes_reachable) lemma Always_Int_I: diff -r e0f68a507683 -r b021008c5397 src/HOL/UNITY/Extend.thy --- 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 \ B) = extend_set h A \ extend_set h B" by auto -lemma extend_set_INT_distrib: "extend_set h (INTER A B) = (\x \ A. extend_set h (B x))" +lemma extend_set_INT_distrib: "extend_set h (\(B ` A)) = (\x \ 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" diff -r e0f68a507683 -r b021008c5397 src/HOL/UNITY/Guar.thy --- 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 \ X guarantees (INTER I Y)) = (\i\I. F \ X guarantees (Y i))" + "(F \ X guarantees (\(Y ` I))) = (\i\I. F \ X guarantees (Y i))" by (simp add: guarantees_INT_right) lemma shunting: "(X guarantees Y) = (UNIV guarantees (-X \ Y))" @@ -276,7 +276,7 @@ lemma guarantees_JN_INT: "[| \i\I. F i \ X i guarantees Y i; OK I F |] - ==> (JOIN I F) \ (INTER I X) guarantees (INTER I Y)" + ==> (JOIN I F) \ (\(X ` I)) guarantees (\(Y ` I))" apply (unfold guar_def, auto) apply (drule bspec, assumption) apply (rename_tac "i") @@ -287,7 +287,7 @@ lemma guarantees_JN_UN: "[| \i\I. F i \ X i guarantees Y i; OK I F |] - ==> (JOIN I F) \ (UNION I X) guarantees (UNION I Y)" + ==> (JOIN I F) \ (\(X ` I)) guarantees (\(Y ` I))" apply (unfold guar_def, auto) apply (drule bspec, assumption) apply (rename_tac "i") diff -r e0f68a507683 -r b021008c5397 src/HOL/UNITY/Lift_prog.thy --- 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\OK and "lift"\ lemma act_in_UNION_preserves_fst: - "act \ {(x,x'). fst x = fst x'} ==> act \ UNION (preserves fst) Acts" + "act \ {(x,x'). fst x = fst x'} ==> act \ \(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: "[| \i \ I. F i \ preserves snd; - \i \ I. UNION (preserves fst) Acts \ AllowedActs (F i) |] + \i \ I. \(Acts ` (preserves fst)) \ 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) diff -r e0f68a507683 -r b021008c5397 src/HOL/UNITY/Simple/Reachability.thy --- 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 == (\v\V. reachable v <==> {s. (root, v) \ REACHABLE}) \ - (INTER E (nmsg_eq 0))" + (\((nmsg_eq 0) ` E))" axiomatization where diff -r e0f68a507683 -r b021008c5397 src/HOL/UNITY/Union.thy --- 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 \ SKIP \ X \ (\G. Acts G \ UNION X Acts \ G \ X)" + where "safety_prop X \ SKIP \ X \ (\G. Acts G \ \(Acts ` X) \ G \ X)" syntax "_JOIN1" :: "[pttrns, 'b set] => 'b set" ("(3\_./ _)" 10) @@ -376,15 +376,15 @@ given instances of "ok"\ lemma safety_prop_Acts_iff: - "safety_prop X ==> (Acts G \ insert Id (UNION X Acts)) = (G \ X)" + "safety_prop X ==> (Acts G \ insert Id (\(Acts ` X))) = (G \ X)" by (auto simp add: safety_prop_def) lemma safety_prop_AllowedActs_iff_Allowed: - "safety_prop X ==> (UNION X Acts \ AllowedActs F) = (X \ Allowed F)" + "safety_prop X ==> (\(Acts ` X) \ AllowedActs F) = (X \ 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, \(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, \(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, \(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,\(Acts ` X)); safety_prop X |] ==> F ok G = (G \ X & acts \ AllowedActs G)" by (auto simp add: ok_def safety_prop_Acts_iff)