# HG changeset patch # User wenzelm # Date 1548161821 -3600 # Node ID b7e708ba77866e3ad609c4d38e8d1c71d5a9cb83 # Parent dc85b5b3a532bbe2702a48c3ce81ba1befbb5426# Parent 81ca77cb7c8c2409bc42e286aea2a596cdf3048d merged diff -r 81ca77cb7c8c -r b7e708ba7786 src/HOL/Algebra/Complete_Lattice.thy --- a/src/HOL/Algebra/Complete_Lattice.thy Tue Jan 22 12:28:41 2019 +0100 +++ b/src/HOL/Algebra/Complete_Lattice.thy Tue Jan 22 13:57:01 2019 +0100 @@ -127,7 +127,7 @@ have "least L b (Upper L A)" proof (rule least_UpperI) show "\x. x \ A \ x \ b" - by (meson L Lower_memI Upper_memD b_inf_B greatest_le set_mp) + by (meson L Lower_memI Upper_memD b_inf_B greatest_le subsetD) show "\y. y \ Upper L A \ b \ y" by (meson B_L b_inf_B greatest_Lower_below) qed (use bcarr L in auto) @@ -589,7 +589,7 @@ have "least L b (Upper L A)" proof (rule least_UpperI) show "\x. x \ A \ x \ b" - by (meson L Lower_memI Upper_memD b_inf_B greatest_le set_rev_mp) + by (meson L Lower_memI Upper_memD b_inf_B greatest_le rev_subsetD) show "\y. y \ Upper L A \ b \ y" by (auto elim: greatest_Lower_below [OF b_inf_B]) qed (use L bcarr in auto) @@ -692,7 +692,7 @@ show 1: "\\<^bsub>L\<^esub>A \ carrier L" by (meson L.at_least_at_most_closed L.sup_closed subset_trans *) show "a \\<^bsub>L\<^esub> \\<^bsub>L\<^esub>A" - by (meson "*" False L.at_least_at_most_closed L.at_least_at_most_lower L.le_trans L.sup_upper 1 all_not_in_conv assms(2) set_mp subset_trans) + by (meson "*" False L.at_least_at_most_closed L.at_least_at_most_lower L.le_trans L.sup_upper 1 all_not_in_conv assms(2) subsetD subset_trans) show "\\<^bsub>L\<^esub>A \\<^bsub>L\<^esub> b" proof (rule L.sup_least) show "A \ carrier L" "\x. x \ A \ x \\<^bsub>L\<^esub> b" @@ -723,7 +723,7 @@ show "a \\<^bsub>L\<^esub> \\<^bsub>L\<^esub>A" by (meson "*" L.at_least_at_most_closed L.at_least_at_most_lower L.inf_greatest assms(2) subsetD subset_trans) show "\\<^bsub>L\<^esub>A \\<^bsub>L\<^esub> b" - by (meson * 1 False L.at_least_at_most_closed L.at_least_at_most_upper L.inf_lower L.le_trans all_not_in_conv assms(3) set_mp subset_trans) + by (meson * 1 False L.at_least_at_most_closed L.at_least_at_most_upper L.inf_lower L.le_trans all_not_in_conv assms(3) subsetD subset_trans) qed qed qed @@ -814,7 +814,7 @@ have "LFP\<^bsub>?L'\<^esub> f \\<^bsub>?L'\<^esub> x" proof (rule L'.LFP_lowerbound, simp_all) show "x \ \\\<^bsub>L\<^esub>A..\\<^bsub>L\<^esub>\\<^bsub>L\<^esub>" - using x by (auto simp add: Upper_def A AL L.at_least_at_most_member L.sup_least set_rev_mp) + using x by (auto simp add: Upper_def A AL L.at_least_at_most_member L.sup_least rev_subsetD) with x show "f x \\<^bsub>L\<^esub> x" by (simp add: Upper_def) (meson L.at_least_at_most_closed L.use_fps L.weak_refl subsetD f_top_chain imageI) qed @@ -884,7 +884,7 @@ moreover have "\\<^bsub>L\<^esub>A \\<^bsub>L\<^esub> y" by (simp add: AL L.inf_lower c) ultimately show "f (\\<^bsub>L\<^esub>A) \\<^bsub>L\<^esub> y" - by (meson AL L.inf_closed L.le_trans c pf_w set_rev_mp w) + by (meson AL L.inf_closed L.le_trans c pf_w rev_subsetD w) qed thus ?thesis by (meson AL L.inf_closed L.le_trans assms(3) b(1) b(2) fx use_iso2 w) diff -r 81ca77cb7c8c -r b7e708ba7786 src/HOL/Algebra/Group_Action.thy --- a/src/HOL/Algebra/Group_Action.thy Tue Jan 22 12:28:41 2019 +0100 +++ b/src/HOL/Algebra/Group_Action.thy Tue Jan 22 13:57:01 2019 +0100 @@ -902,7 +902,7 @@ hence "\: H \ carrier (BijGroup E)" by (simp add: BijGroup_def bij_prop0 subset_eq) thus "\: H \ carrier (BijGroup E) \ (\x \ H. \y \ H. \ (x \ y) = \ x \\<^bsub>BijGroup E\<^esub> \ y)" - by (simp add: S0 group_hom group_hom.hom_mult set_rev_mp) + by (simp add: S0 group_hom group_hom.hom_mult rev_subsetD) qed theorem (in group_action) induced_action: diff -r 81ca77cb7c8c -r b7e708ba7786 src/HOL/Algebra/Ideal.thy --- a/src/HOL/Algebra/Ideal.thy Tue Jan 22 12:28:41 2019 +0100 +++ b/src/HOL/Algebra/Ideal.thy Tue Jan 22 13:57:01 2019 +0100 @@ -481,7 +481,7 @@ qed next show "I <+> J \ Idl (I \ J)" - by (auto simp: set_add_defs genideal_def additive_subgroup.a_closed ideal_def set_mp) + by (auto simp: set_add_defs genideal_def additive_subgroup.a_closed ideal_def subsetD) qed subsection \Properties of Principal Ideals\ diff -r 81ca77cb7c8c -r b7e708ba7786 src/HOL/Algebra/Polynomials.thy --- a/src/HOL/Algebra/Polynomials.thy Tue Jan 22 12:28:41 2019 +0100 +++ b/src/HOL/Algebra/Polynomials.thy Tue Jan 22 13:57:01 2019 +0100 @@ -413,7 +413,7 @@ using A(2-3) subringE(2)[OF K] by auto hence "set (map2 (\) p1 p2') \ K" using A(1) subringE(7)[OF K] - by (induct p1) (auto, metis set_ConsD set_mp set_zip_leftD set_zip_rightD) + by (induct p1) (auto, metis set_ConsD subsetD set_zip_leftD set_zip_rightD) thus ?thesis unfolding p2'_def using normalize_gives_polynomial A(3) by simp qed } diff -r 81ca77cb7c8c -r b7e708ba7786 src/HOL/Analysis/Abstract_Topology.thy --- a/src/HOL/Analysis/Abstract_Topology.thy Tue Jan 22 12:28:41 2019 +0100 +++ b/src/HOL/Analysis/Abstract_Topology.thy Tue Jan 22 13:57:01 2019 +0100 @@ -24,6 +24,9 @@ lemma istopology_openin[intro]: "istopology(openin U)" using openin[of U] by blast +lemma istopology_open: "istopology open" + by (auto simp: istopology_def) + lemma topology_inverse': "istopology U \ openin (topology U) = U" using topology_inverse[unfolded mem_Collect_eq] . @@ -290,6 +293,10 @@ lemma topspace_subtopology: "topspace (subtopology U V) = topspace U \ V" by (auto simp: topspace_def openin_subtopology) +lemma topspace_subtopology_subset: + "S \ topspace X \ topspace(subtopology X S) = S" + by (simp add: inf.absorb_iff2 topspace_subtopology) + lemma closedin_subtopology: "closedin (subtopology U V) S \ (\T. closedin U T \ S = T \ V)" unfolding closedin_def topspace_subtopology by (auto simp: openin_subtopology) @@ -351,6 +358,10 @@ lemma subtopology_UNIV[simp]: "subtopology U UNIV = U" by (simp add: subtopology_superset) +lemma subtopology_restrict: + "subtopology X (topspace X \ S) = subtopology X S" + by (metis subtopology_subtopology subtopology_topspace) + lemma openin_subtopology_empty: "openin (subtopology U {}) S \ S = {}" by (metis Int_empty_right openin_empty openin_subtopology) @@ -395,11 +406,13 @@ subsection \The standard Euclidean topology\ -definition%important euclidean :: "'a::topological_space topology" - where "euclidean = topology open" +abbreviation%important euclidean :: "'a::topological_space topology" + where "euclidean \ topology open" + +abbreviation top_of_set :: "'a::topological_space set \ 'a topology" + where "top_of_set \ subtopology (topology open)" lemma open_openin: "open S \ openin euclidean S" - unfolding euclidean_def apply (rule cong[where x=S and y=S]) apply (rule topology_inverse[symmetric]) apply (auto simp: istopology_def) @@ -426,19 +439,6 @@ abbreviation euclideanreal :: "real topology" where "euclideanreal \ topology open" -lemma real_openin [simp]: "openin euclideanreal S = open S" - by (simp add: euclidean_def open_openin) - -lemma topspace_euclideanreal [simp]: "topspace euclideanreal = UNIV" - using openin_subset open_UNIV real_openin by blast - -lemma topspace_euclideanreal_subtopology [simp]: - "topspace (subtopology euclideanreal S) = S" - by (simp add: topspace_subtopology) - -lemma real_closedin [simp]: "closedin euclideanreal S = closed S" - by (simp add: closed_closedin euclidean_def) - subsection \Basic "localization" results are handy for connectedness.\ lemma openin_open: "openin (subtopology euclidean U) S \ (\T. open T \ (S = U \ T))" @@ -569,7 +569,7 @@ lemma openin_trans[trans]: "openin (subtopology euclidean T) S \ openin (subtopology euclidean U) T \ openin (subtopology euclidean U) S" - unfolding open_openin openin_open by blast + by (metis openin_Int_open openin_open) lemma openin_open_trans: "openin (subtopology euclidean T) S \ open T \ open S" by (auto simp: openin_open intro: openin_trans) @@ -665,6 +665,13 @@ "S \ X derived_set_of S = {} \ subtopology X S = discrete_topology(topspace X \ S)" by (metis Int_lower1 derived_set_of_restrict inf_assoc inf_bot_right subtopology_eq_discrete_topology_eq subtopology_subtopology subtopology_topspace) +lemma subtopology_discrete_topology [simp]: "subtopology (discrete_topology U) S = discrete_topology(U \ S)" +proof - + have "(\T. \Sa. T = Sa \ S \ Sa \ U) = (\Sa. Sa \ U \ Sa \ S)" + by force + then show ?thesis + by (simp add: subtopology_def) (simp add: discrete_topology_def) +qed lemma openin_Int_derived_set_of_subset: "openin X S \ S \ X derived_set_of T \ X derived_set_of (S \ T)" by (auto simp: derived_set_of_def) @@ -1435,9 +1442,6 @@ by (auto simp: frontier_of_closures) qed -lemma continuous_map_id [simp]: "continuous_map X X id" - unfolding continuous_map_def using openin_subopen topspace_def by fastforce - lemma topology_finer_continuous_id: "topspace X = topspace Y \ ((\S. openin X S \ openin Y S) \ continuous_map Y X id)" unfolding continuous_map_def @@ -1541,6 +1545,16 @@ lemma continuous_map_iff_continuous_real [simp]: "continuous_map (subtopology euclideanreal S) euclideanreal g = continuous_on S g" by (force simp: continuous_map openin_subtopology continuous_on_open_invariant) +lemma continuous_map_id [simp]: "continuous_map X X id" + unfolding continuous_map_def using openin_subopen topspace_def by fastforce + +declare continuous_map_id [unfolded id_def, simp] + +lemma continuous_map_id_subt [simp]: "continuous_map (subtopology X S) X id" + by (simp add: continuous_map_from_subtopology) + +declare continuous_map_id_subt [unfolded id_def, simp] + subsection\Open and closed maps (not a priori assumed continuous)\ diff -r 81ca77cb7c8c -r b7e708ba7786 src/HOL/Analysis/Brouwer_Fixpoint.thy --- a/src/HOL/Analysis/Brouwer_Fixpoint.thy Tue Jan 22 12:28:41 2019 +0100 +++ b/src/HOL/Analysis/Brouwer_Fixpoint.thy Tue Jan 22 13:57:01 2019 +0100 @@ -3720,7 +3720,7 @@ by (auto simp: algebra_simps) have "x \ T" "x \ a" using that by auto then have axa: "a + (x - a) \ affine hull S" - by (metis (no_types) add.commute affS diff_add_cancel set_rev_mp) + by (metis (no_types) add.commute affS diff_add_cancel rev_subsetD) then have "\ dd (x - a) \ 0 \ a + dd (x - a) *\<^sub>R (x - a) \ rel_frontier S" using \x \ a\ dd1 by fastforce with \x \ a\ show "(1 - u) *\<^sub>R x + u *\<^sub>R (a + dd (x - a) *\<^sub>R (x - a)) \ a" diff -r 81ca77cb7c8c -r b7e708ba7786 src/HOL/Analysis/Caratheodory.thy --- a/src/HOL/Analysis/Caratheodory.thy Tue Jan 22 12:28:41 2019 +0100 +++ b/src/HOL/Analysis/Caratheodory.thy Tue Jan 22 13:57:01 2019 +0100 @@ -139,7 +139,7 @@ lemma (in algebra) lambda_system_algebra: "positive M f \ algebra \ (lambda_system \ M f)" apply (auto simp add: algebra_iff_Un) - apply (metis lambda_system_sets set_mp sets_into_space) + apply (metis lambda_system_sets subsetD sets_into_space) apply (metis lambda_system_empty) apply (metis lambda_system_Compl) apply (metis lambda_system_Un) diff -r 81ca77cb7c8c -r b7e708ba7786 src/HOL/Analysis/Cauchy_Integral_Theorem.thy --- a/src/HOL/Analysis/Cauchy_Integral_Theorem.thy Tue Jan 22 12:28:41 2019 +0100 +++ b/src/HOL/Analysis/Cauchy_Integral_Theorem.thy Tue Jan 22 13:57:01 2019 +0100 @@ -3068,7 +3068,7 @@ then have contfb: "continuous_on (ball z d) f" using contf continuous_on_subset by blast obtain h where "\y\ball z d. (h has_field_derivative f y) (at y within ball z d)" - by (metis holomorphic_convex_primitive [OF convex_ball k contfb fcd] d interior_subset Diff_iff set_mp) + by (metis holomorphic_convex_primitive [OF convex_ball k contfb fcd] d interior_subset Diff_iff subsetD) then have "\y\ball z d. (h has_field_derivative f y) (at y within s)" by (metis open_ball at_within_open d os subsetCE) then have "\h. (\y. cmod (y - z) < d \ (h has_field_derivative f y) (at y within s))" diff -r 81ca77cb7c8c -r b7e708ba7786 src/HOL/Analysis/Conformal_Mappings.thy --- a/src/HOL/Analysis/Conformal_Mappings.thy Tue Jan 22 12:28:41 2019 +0100 +++ b/src/HOL/Analysis/Conformal_Mappings.thy Tue Jan 22 13:57:01 2019 +0100 @@ -2849,7 +2849,7 @@ using "2.prems"(8) that apply blast apply (metis Diff_iff Diff_insert2 contra_subsetD pg(4) that) - by (meson DiffD2 cp(4) set_rev_mp subset_insertI that) + by (meson DiffD2 cp(4) rev_subsetD subset_insertI that) have "winding_number g' p' = winding_number g p' + winding_number (pg +++ cp +++ reversepath pg) p'" unfolding g'_def apply (subst winding_number_join) diff -r 81ca77cb7c8c -r b7e708ba7786 src/HOL/Analysis/Convex_Euclidean_Space.thy --- a/src/HOL/Analysis/Convex_Euclidean_Space.thy Tue Jan 22 12:28:41 2019 +0100 +++ b/src/HOL/Analysis/Convex_Euclidean_Space.thy Tue Jan 22 13:57:01 2019 +0100 @@ -521,7 +521,7 @@ using mem_rel_interior_ball[of "x - e *\<^sub>R (x - c)" S] \e > 0\ by auto qed -lemma interior_real_semiline: +lemma interior_real_atLeast [simp]: fixes a :: real shows "interior {a..} = {a<..}" proof - @@ -561,7 +561,7 @@ finally show ?thesis using \x \ {c..d}\ by auto qed -lemma interior_real_semiline': +lemma interior_real_atMost [simp]: fixes a :: real shows "interior {..a} = {.. {..b}" by auto also have "interior \ = {a<..} \ {.. = {a<.. {}" unfolding set_eq_iff by (auto intro!: exI[of _ "a + 1"]) - then show ?thesis using interior_real_semiline interior_rel_interior_gen[of "{a..}"] + then show ?thesis using interior_real_atLeast interior_rel_interior_gen[of "{a..}"] by (auto split: if_split_asm) qed diff -r 81ca77cb7c8c -r b7e708ba7786 src/HOL/Analysis/Derivative.thy --- a/src/HOL/Analysis/Derivative.thy Tue Jan 22 12:28:41 2019 +0100 +++ b/src/HOL/Analysis/Derivative.thy Tue Jan 22 13:57:01 2019 +0100 @@ -1400,7 +1400,7 @@ apply auto done moreover have "f (g y) = y" if "y \ interior (f ` S)" for y - by (metis gf imageE interiorE set_mp that) + by (metis gf imageE interiorE subsetD that) ultimately show ?thesis using assms by (metis has_derivative_inverse_basic_x open_interior) qed @@ -2740,7 +2740,7 @@ using f' g' closure_subset[of T] closure_subset[of S] unfolding has_derivative_within_If_eq by (intro conjI bl tendsto_If_within_closures x_in) - (auto simp: has_derivative_within inverse_eq_divide connect connect' set_mp) + (auto simp: has_derivative_within inverse_eq_divide connect connect' subsetD) qed lemma has_vector_derivative_If_within_closures: diff -r 81ca77cb7c8c -r b7e708ba7786 src/HOL/Analysis/Elementary_Metric_Spaces.thy --- a/src/HOL/Analysis/Elementary_Metric_Spaces.thy Tue Jan 22 12:28:41 2019 +0100 +++ b/src/HOL/Analysis/Elementary_Metric_Spaces.thy Tue Jan 22 13:57:01 2019 +0100 @@ -2696,7 +2696,7 @@ by (auto simp: closure_sequential) from continuous_on_tendsto_compose[OF cont_h xs(1)] xs(2) Y have hx: "(\x. f (xs x)) \ h x" - by (auto simp: set_mp extension) + by (auto simp: subsetD extension) then have "(\x. f (xs x)) \ y x" using \x \ X\ not_eventuallyD xs(2) by (force intro!: filterlim_compose[OF y[OF \x \ closure X\]] simp: filterlim_at xs) diff -r 81ca77cb7c8c -r b7e708ba7786 src/HOL/Analysis/Elementary_Normed_Spaces.thy --- a/src/HOL/Analysis/Elementary_Normed_Spaces.thy Tue Jan 22 12:28:41 2019 +0100 +++ b/src/HOL/Analysis/Elementary_Normed_Spaces.thy Tue Jan 22 13:57:01 2019 +0100 @@ -1009,7 +1009,7 @@ fix y assume "y \ S" and y: "\n. y \ closure (TF n)" then show "\T\\. y \ T" - by (metis Int_iff from_nat_into_surj [OF \countable \\] set_mp subg) + by (metis Int_iff from_nat_into_surj [OF \countable \\] subsetD subg) show "dist y x < e" by (metis y dist_commute mem_ball subball subsetCE) qed diff -r 81ca77cb7c8c -r b7e708ba7786 src/HOL/Analysis/Elementary_Topology.thy --- a/src/HOL/Analysis/Elementary_Topology.thy Tue Jan 22 12:28:41 2019 +0100 +++ b/src/HOL/Analysis/Elementary_Topology.thy Tue Jan 22 13:57:01 2019 +0100 @@ -1763,7 +1763,7 @@ by auto moreover have ev_Z: "\z. z \ Z \ eventually (\x. x \ z) F" - unfolding Z_def by (auto elim: eventually_mono intro: set_mp[OF closure_subset]) + unfolding Z_def by (auto elim: eventually_mono intro: subsetD[OF closure_subset]) have "(\B \ Z. finite B \ U \ \B \ {})" proof (intro allI impI) fix B assume "finite B" "B \ Z" diff -r 81ca77cb7c8c -r b7e708ba7786 src/HOL/Analysis/Function_Topology.thy --- a/src/HOL/Analysis/Function_Topology.thy Tue Jan 22 12:28:41 2019 +0100 +++ b/src/HOL/Analysis/Function_Topology.thy Tue Jan 22 13:57:01 2019 +0100 @@ -268,8 +268,7 @@ lemma continuous_on_continuous_on_topo: "continuous_on s f \ continuous_on_topo (subtopology euclidean s) euclidean f" - unfolding continuous_on_open_invariant openin_open vimage_def continuous_on_topo_def -topspace_euclidean_subtopology open_openin topspace_euclidean by fast + by (auto simp: continuous_on_topo_def Int_commute continuous_openin_preimage_eq) lemma continuous_on_topo_UNIV: "continuous_on UNIV f \ continuous_on_topo euclidean euclidean f" @@ -843,8 +842,8 @@ have **: "finite {i. X i \ UNIV}" unfolding X_def V_def J_def using assms(1) by auto have "open (Pi\<^sub>E UNIV X)" - unfolding open_fun_def apply (rule product_topology_basis) - using * ** unfolding open_openin topspace_euclidean by auto + unfolding open_fun_def + by (simp_all add: * ** product_topology_basis) moreover have "Pi\<^sub>E UNIV X = {f. \i\I. f (x i) \ U i}" apply (auto simp add: PiE_iff) unfolding X_def V_def J_def proof (auto) @@ -995,7 +994,7 @@ using \open U \ x \ U\ unfolding open_fun_def by auto with product_topology_open_contains_basis[OF this] have "\X. x \ (\\<^sub>E i\UNIV. X i) \ (\i. open (X i)) \ finite {i. X i \ UNIV} \ (\\<^sub>E i\UNIV. X i) \ U" - unfolding topspace_euclidean open_openin by simp + by simp then obtain X where H: "x \ (\\<^sub>E i\UNIV. X i)" "\i. open (X i)" "finite {i. X i \ UNIV}" @@ -1064,7 +1063,7 @@ unfolding open_fun_def by auto with product_topology_open_contains_basis[OF this \x \ U\] have "\X. x \ (\\<^sub>E i\UNIV. X i) \ (\i. open (X i)) \ finite {i. X i \ UNIV} \ (\\<^sub>E i\UNIV. X i) \ U" - unfolding topspace_euclidean open_openin by simp + by simp then obtain X where H: "x \ (\\<^sub>E i\UNIV. X i)" "\i. open (X i)" "finite {i. X i \ UNIV}" @@ -1104,8 +1103,7 @@ show "open U" using \U \ K\ unfolding open_fun_def K_def apply (auto) apply (rule product_topology_basis) - using \\V. V \ B2 \ open V\ open_UNIV unfolding topspace_euclidean open_openin[symmetric] - by auto + using \\V. V \ B2 \ open V\ open_UNIV by auto qed show ?thesis using i ii iii by auto @@ -1155,7 +1153,7 @@ = blinfun_apply-`{g::('a\'b). \i\I. g (x i) \ U i} \ UNIV" by auto ultimately show ?thesis - unfolding strong_operator_topology_def open_openin apply (subst openin_pullback_topology) by auto + unfolding strong_operator_topology_def by (subst openin_pullback_topology) auto qed lemma strong_operator_topology_continuous_evaluation: diff -r 81ca77cb7c8c -r b7e708ba7786 src/HOL/Analysis/Further_Topology.thy --- a/src/HOL/Analysis/Further_Topology.thy Tue Jan 22 12:28:41 2019 +0100 +++ b/src/HOL/Analysis/Further_Topology.thy Tue Jan 22 13:57:01 2019 +0100 @@ -4738,7 +4738,7 @@ fix T assume "connected T" and TB: "T \ - frontier B" and "a \ T" and "b \ T" have "a \ B" - by (metis A_def B_def ComplD \a \ A\ assms(1) closed_open connected_component_subset in_closure_connected_component set_mp) + by (metis A_def B_def ComplD \a \ A\ assms(1) closed_open connected_component_subset in_closure_connected_component subsetD) have "T \ B \ {}" using \b \ B\ \b \ T\ by blast moreover have "T - B \ {}" diff -r 81ca77cb7c8c -r b7e708ba7786 src/HOL/Analysis/Homotopy.thy --- a/src/HOL/Analysis/Homotopy.thy Tue Jan 22 12:28:41 2019 +0100 +++ b/src/HOL/Analysis/Homotopy.thy Tue Jan 22 13:57:01 2019 +0100 @@ -2470,7 +2470,7 @@ then have *: "openin ?SS (F y t) \ path_connected (G y t) \ y \ F y t \ F y t \ G y t \ G y t \ t" using 1 \y \ t\ by presburger have "G y t \ path_component_set t y" - using * path_component_maximal set_rev_mp by blast + using * path_component_maximal rev_subsetD by blast then have "\A. openin ?SS A \ y \ A \ A \ path_component_set t x" by (metis "*" \G y t \ path_component_set t y\ dual_order.trans path_component_eq y) } diff -r 81ca77cb7c8c -r b7e708ba7786 src/HOL/Analysis/Infinite_Set_Sum.thy --- a/src/HOL/Analysis/Infinite_Set_Sum.thy Tue Jan 22 12:28:41 2019 +0100 +++ b/src/HOL/Analysis/Infinite_Set_Sum.thy Tue Jan 22 13:57:01 2019 +0100 @@ -1,4 +1,4 @@ -(* +(* Title: HOL/Analysis/Infinite_Set_Sum.thy Author: Manuel Eberl, TU München @@ -22,12 +22,12 @@ finally show "X \ sets M" . next fix X assume "X \ sets M" - from sets.sets_into_space[OF this] and assms + from sets.sets_into_space[OF this] and assms show "X \ Pow A" by simp qed lemma measure_eqI_countable': - assumes spaces: "space M = A" "space N = A" + assumes spaces: "space M = A" "space N = A" assumes sets: "\x. x \ A \ {x} \ sets M" "\x. x \ A \ {x} \ sets N" assumes A: "countable A" assumes eq: "\a. a \ A \ emeasure M {a} = emeasure N {a}" @@ -39,32 +39,19 @@ by (intro sets_eq_countable assms) qed fact+ -lemma PiE_singleton: - assumes "f \ extensional A" - shows "PiE A (\x. {f x}) = {f}" -proof - - { - fix g assume "g \ PiE A (\x. {f x})" - hence "g x = f x" for x - using assms by (cases "x \ A") (auto simp: extensional_def) - hence "g = f" by (simp add: fun_eq_iff) - } - thus ?thesis using assms by (auto simp: extensional_def) -qed - lemma count_space_PiM_finite: fixes B :: "'a \ 'b set" assumes "finite A" "\i. countable (B i)" shows "PiM A (\i. count_space (B i)) = count_space (PiE A B)" proof (rule measure_eqI_countable') - show "space (PiM A (\i. count_space (B i))) = PiE A B" + show "space (PiM A (\i. count_space (B i))) = PiE A B" by (simp add: space_PiM) show "space (count_space (PiE A B)) = PiE A B" by simp next fix f assume f: "f \ PiE A B" hence "PiE A (\x. {f x}) \ sets (Pi\<^sub>M A (\i. count_space (B i)))" by (intro sets_PiM_I_finite assms) auto - also from f have "PiE A (\x. {f x}) = {f}" + also from f have "PiE A (\x. {f x}) = {f}" by (intro PiE_singleton) (auto simp: PiE_def) finally show "{f} \ sets (Pi\<^sub>M A (\i. count_space (B i)))" . next @@ -74,7 +61,7 @@ fix f assume f: "f \ PiE A B" hence "{f} = PiE A (\x. {f x})" by (intro PiE_singleton [symmetric]) (auto simp: PiE_def) - also have "emeasure (Pi\<^sub>M A (\i. count_space (B i))) \ = + also have "emeasure (Pi\<^sub>M A (\i. count_space (B i))) \ = (\i\A. emeasure (count_space (B i)) {f i})" using f assms by (subst emeasure_PiM) auto also have "\ = (\i\A. 1)" @@ -88,7 +75,7 @@ definition%important abs_summable_on :: - "('a \ 'b :: {banach, second_countable_topology}) \ 'a set \ bool" + "('a \ 'b :: {banach, second_countable_topology}) \ 'a set \ bool" (infix "abs'_summable'_on" 50) where "f abs_summable_on A \ integrable (count_space A) f" @@ -100,28 +87,28 @@ "infsetsum f A = lebesgue_integral (count_space A) f" syntax (ASCII) - "_infsetsum" :: "pttrn \ 'a set \ 'b \ 'b::{banach, second_countable_topology}" + "_infsetsum" :: "pttrn \ 'a set \ 'b \ 'b::{banach, second_countable_topology}" ("(3INFSETSUM _:_./ _)" [0, 51, 10] 10) syntax - "_infsetsum" :: "pttrn \ 'a set \ 'b \ 'b::{banach, second_countable_topology}" + "_infsetsum" :: "pttrn \ 'a set \ 'b \ 'b::{banach, second_countable_topology}" ("(2\\<^sub>a_\_./ _)" [0, 51, 10] 10) translations \ \Beware of argument permutation!\ "\\<^sub>ai\A. b" \ "CONST infsetsum (\i. b) A" syntax (ASCII) - "_uinfsetsum" :: "pttrn \ 'a set \ 'b \ 'b::{banach, second_countable_topology}" + "_uinfsetsum" :: "pttrn \ 'a set \ 'b \ 'b::{banach, second_countable_topology}" ("(3INFSETSUM _:_./ _)" [0, 51, 10] 10) syntax - "_uinfsetsum" :: "pttrn \ 'b \ 'b::{banach, second_countable_topology}" + "_uinfsetsum" :: "pttrn \ 'b \ 'b::{banach, second_countable_topology}" ("(2\\<^sub>a_./ _)" [0, 10] 10) translations \ \Beware of argument permutation!\ "\\<^sub>ai. b" \ "CONST infsetsum (\i. b) (CONST UNIV)" syntax (ASCII) - "_qinfsetsum" :: "pttrn \ bool \ 'a \ 'a::{banach, second_countable_topology}" + "_qinfsetsum" :: "pttrn \ bool \ 'a \ 'a::{banach, second_countable_topology}" ("(3INFSETSUM _ |/ _./ _)" [0, 0, 10] 10) syntax - "_qinfsetsum" :: "pttrn \ bool \ 'a \ 'a::{banach, second_countable_topology}" + "_qinfsetsum" :: "pttrn \ bool \ 'a \ 'a::{banach, second_countable_topology}" ("(2\\<^sub>a_ | (_)./ _)" [0, 0, 10] 10) translations "\\<^sub>ax|P. t" => "CONST infsetsum (\x. t) {x. P}" @@ -156,7 +143,7 @@ by (rule restrict_count_space_subset [symmetric]) fact+ also have "integrable \ f \ set_integrable (count_space B) A f" by (simp add: integrable_restrict_space set_integrable_def) - finally show ?thesis + finally show ?thesis unfolding abs_summable_on_def set_integrable_def . qed @@ -164,12 +151,12 @@ unfolding abs_summable_on_def set_integrable_def by (metis (no_types) inf_top.right_neutral integrable_restrict_space restrict_count_space sets_UNIV) -lemma abs_summable_on_altdef': +lemma abs_summable_on_altdef': "A \ B \ f abs_summable_on A \ set_integrable (count_space B) A f" unfolding abs_summable_on_def set_integrable_def by (metis (no_types) Pow_iff abs_summable_on_def inf.orderE integrable_restrict_space restrict_count_space_subset set_integrable_def sets_count_space space_count_space) -lemma abs_summable_on_norm_iff [simp]: +lemma abs_summable_on_norm_iff [simp]: "(\x. norm (f x)) abs_summable_on A \ f abs_summable_on A" by (simp add: abs_summable_on_def integrable_norm_iff) @@ -183,8 +170,8 @@ assumes "g abs_summable_on A" assumes "\x. x \ A \ norm (f x) \ norm (g x)" shows "f abs_summable_on A" - using assms Bochner_Integration.integrable_bound[of "count_space A" g f] - unfolding abs_summable_on_def by (auto simp: AE_count_space) + using assms Bochner_Integration.integrable_bound[of "count_space A" g f] + unfolding abs_summable_on_def by (auto simp: AE_count_space) lemma abs_summable_on_comparison_test': assumes "g abs_summable_on A" @@ -220,7 +207,7 @@ "f abs_summable_on (A :: nat set) \ summable (\