merged
authorwenzelm
Tue, 22 Jan 2019 13:57:01 +0100
changeset 69714 b7e708ba7786
parent 69712 dc85b5b3a532 (diff)
parent 69713 81ca77cb7c8c (current diff)
child 69715 1bc422c08209
merged
--- 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 "\<And>x. x \<in> A \<Longrightarrow> x \<sqsubseteq> 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 "\<And>y. y \<in> Upper L A \<Longrightarrow> b \<sqsubseteq> 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 "\<And>x. x \<in> A \<Longrightarrow> x \<sqsubseteq> 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 "\<And>y. y \<in> Upper L A \<Longrightarrow> b \<sqsubseteq> y"
       by (auto elim: greatest_Lower_below [OF b_inf_B])
   qed (use L bcarr in auto)
@@ -692,7 +692,7 @@
           show 1: "\<Squnion>\<^bsub>L\<^esub>A \<in> carrier L"
             by (meson L.at_least_at_most_closed L.sup_closed subset_trans *)
           show "a \<sqsubseteq>\<^bsub>L\<^esub> \<Squnion>\<^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 "\<Squnion>\<^bsub>L\<^esub>A \<sqsubseteq>\<^bsub>L\<^esub> b"
           proof (rule L.sup_least)
             show "A \<subseteq> carrier L" "\<And>x. x \<in> A \<Longrightarrow> x \<sqsubseteq>\<^bsub>L\<^esub> b"
@@ -723,7 +723,7 @@
           show "a \<sqsubseteq>\<^bsub>L\<^esub> \<Sqinter>\<^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 "\<Sqinter>\<^bsub>L\<^esub>A \<sqsubseteq>\<^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 \<sqsubseteq>\<^bsub>?L'\<^esub> x"
         proof (rule L'.LFP_lowerbound, simp_all)
           show "x \<in> \<lbrace>\<Squnion>\<^bsub>L\<^esub>A..\<top>\<^bsub>L\<^esub>\<rbrace>\<^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 \<sqsubseteq>\<^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 "\<Sqinter>\<^bsub>L\<^esub>A \<sqsubseteq>\<^bsub>L\<^esub> y"
               by (simp add: AL L.inf_lower c)
             ultimately show "f (\<Sqinter>\<^bsub>L\<^esub>A) \<sqsubseteq>\<^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)
--- 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 "\<phi>: H \<rightarrow> carrier (BijGroup E)"
     by (simp add: BijGroup_def bij_prop0 subset_eq)
   thus "\<phi>: H \<rightarrow> carrier (BijGroup E) \<and> (\<forall>x \<in> H. \<forall>y \<in> H. \<phi> (x \<otimes> y) = \<phi> x \<otimes>\<^bsub>BijGroup E\<^esub> \<phi> 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:
--- 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 \<subseteq> Idl (I \<union> 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 \<open>Properties of Principal Ideals\<close>
--- 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 (\<oplus>) p1 p2') \<subseteq> 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 }
--- 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 \<Longrightarrow> openin (topology U) = U"
   using topology_inverse[unfolded mem_Collect_eq] .
 
@@ -290,6 +293,10 @@
 lemma topspace_subtopology: "topspace (subtopology U V) = topspace U \<inter> V"
   by (auto simp: topspace_def openin_subtopology)
 
+lemma topspace_subtopology_subset:
+   "S \<subseteq> topspace X \<Longrightarrow> topspace(subtopology X S) = S"
+  by (simp add: inf.absorb_iff2 topspace_subtopology)
+
 lemma closedin_subtopology: "closedin (subtopology U V) S \<longleftrightarrow> (\<exists>T. closedin U T \<and> S = T \<inter> 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 \<inter> S) = subtopology X S"
+  by (metis subtopology_subtopology subtopology_topspace)
+
 lemma openin_subtopology_empty:
    "openin (subtopology U {}) S \<longleftrightarrow> S = {}"
 by (metis Int_empty_right openin_empty openin_subtopology)
@@ -395,11 +406,13 @@
 
 subsection \<open>The standard Euclidean topology\<close>
 
-definition%important euclidean :: "'a::topological_space topology"
-  where "euclidean = topology open"
+abbreviation%important euclidean :: "'a::topological_space topology"
+  where "euclidean \<equiv> topology open"
+
+abbreviation top_of_set :: "'a::topological_space set \<Rightarrow> 'a topology"
+  where "top_of_set \<equiv> subtopology (topology open)"
 
 lemma open_openin: "open S \<longleftrightarrow> 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 \<equiv> 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 \<open>Basic "localization" results are handy for connectedness.\<close>
 
 lemma openin_open: "openin (subtopology euclidean U) S \<longleftrightarrow> (\<exists>T. open T \<and> (S = U \<inter> T))"
@@ -569,7 +569,7 @@
 lemma openin_trans[trans]:
   "openin (subtopology euclidean T) S \<Longrightarrow> openin (subtopology euclidean U) T \<Longrightarrow>
     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 \<Longrightarrow> open T \<Longrightarrow> open S"
   by (auto simp: openin_open intro: openin_trans)
@@ -665,6 +665,13 @@
    "S \<inter> X derived_set_of S = {} \<Longrightarrow> subtopology X S = discrete_topology(topspace X \<inter> 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 \<inter> S)"
+proof -
+  have "(\<lambda>T. \<exists>Sa. T = Sa \<inter> S \<and> Sa \<subseteq> U) = (\<lambda>Sa. Sa \<subseteq> U \<and> Sa \<subseteq> 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 \<Longrightarrow> S \<inter> X derived_set_of T \<subseteq> X derived_set_of (S \<inter> 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 \<Longrightarrow> ((\<forall>S. openin X S \<longrightarrow> openin Y S) \<longleftrightarrow> 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>Open and closed maps (not a priori assumed continuous)\<close>
 
--- 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 \<in> T" "x \<noteq> a" using that by auto
         then have axa: "a + (x - a) \<in> 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 "\<not> dd (x - a) \<le> 0 \<and> a + dd (x - a) *\<^sub>R (x - a) \<in> rel_frontier S"
           using \<open>x \<noteq> a\<close> dd1 by fastforce
         with \<open>x \<noteq> a\<close> show "(1 - u) *\<^sub>R x + u *\<^sub>R (a + dd (x - a) *\<^sub>R (x - a)) \<noteq> a"
--- 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 \<Longrightarrow> algebra \<Omega> (lambda_system \<Omega> 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)
--- 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 "\<forall>y\<in>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 "\<forall>y\<in>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 "\<exists>h. (\<forall>y. cmod (y - z) < d \<longrightarrow> (h has_field_derivative f y) (at y within s))"
--- 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)
--- 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] \<open>e > 0\<close> 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 \<open>x \<in> {c..d}\<close> by auto
 qed
 
-lemma interior_real_semiline':
+lemma interior_real_atMost [simp]:
   fixes a :: real
   shows "interior {..a} = {..<a}"
 proof -
@@ -592,27 +592,36 @@
 proof-
   have "{a..b} = {a..} \<inter> {..b}" by auto
   also have "interior \<dots> = {a<..} \<inter> {..<b}"
-    by (simp add: interior_real_semiline interior_real_semiline')
+    by (simp add: interior_real_atLeast interior_real_atMost)
   also have "\<dots> = {a<..<b}" by auto
   finally show ?thesis .
 qed
 
 lemma interior_atLeastLessThan [simp]:
   fixes a::real shows "interior {a..<b} = {a<..<b}"
-  by (metis atLeastLessThan_def greaterThanLessThan_def interior_atLeastAtMost_real interior_Int interior_interior interior_real_semiline)
+  by (metis atLeastLessThan_def greaterThanLessThan_def interior_atLeastAtMost_real interior_Int interior_interior interior_real_atLeast)
 
 lemma interior_lessThanAtMost [simp]:
   fixes a::real shows "interior {a<..b} = {a<..<b}"
   by (metis atLeastAtMost_def greaterThanAtMost_def interior_atLeastAtMost_real interior_Int
-            interior_interior interior_real_semiline)
+            interior_interior interior_real_atLeast)
 
 lemma interior_greaterThanLessThan_real [simp]: "interior {a<..<b} = {a<..<b :: real}"
   by (metis interior_atLeastAtMost_real interior_interior)
 
-lemma frontier_real_Iic [simp]:
+lemma frontier_real_atMost [simp]:
   fixes a :: real
   shows "frontier {..a} = {a}"
-  unfolding frontier_def by (auto simp: interior_real_semiline')
+  unfolding frontier_def by (auto simp: interior_real_atMost)
+
+lemma frontier_real_atLeast [simp]: "frontier {a..} = {a::real}"
+  by (auto simp: frontier_def)
+
+lemma frontier_real_greaterThan [simp]: "frontier {a<..} = {a::real}"
+  by (auto simp: interior_open frontier_def)
+
+lemma frontier_real_lessThan [simp]: "frontier {..<a} = {a::real}"
+  by (auto simp: interior_open frontier_def)
 
 lemma rel_interior_real_box [simp]:
   fixes a b :: real
@@ -634,7 +643,7 @@
 proof -
   have *: "{a<..} \<noteq> {}"
     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
 
--- 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 \<in> 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:
--- 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: "(\<lambda>x. f (xs x)) \<longlonglongrightarrow> h x"
-        by (auto simp: set_mp extension)
+        by (auto simp: subsetD extension)
       then have "(\<lambda>x. f (xs x)) \<longlonglongrightarrow> y x"
         using \<open>x \<notin> X\<close> not_eventuallyD xs(2)
         by (force intro!: filterlim_compose[OF y[OF \<open>x \<in> closure X\<close>]] simp: filterlim_at xs)
--- 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 \<in> S" and y: "\<forall>n. y \<in> closure (TF n)"
       then show "\<forall>T\<in>\<G>. y \<in> T"
-        by (metis Int_iff from_nat_into_surj [OF \<open>countable \<G>\<close>] set_mp subg)
+        by (metis Int_iff from_nat_into_surj [OF \<open>countable \<G>\<close>] subsetD subg)
       show "dist y x < e"
         by (metis y dist_commute mem_ball subball subsetCE)
     qed
--- 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: "\<And>z. z \<in> Z \<Longrightarrow> eventually (\<lambda>x. x \<in> 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 "(\<forall>B \<subseteq> Z. finite B \<longrightarrow> U \<inter> \<Inter>B \<noteq> {})"
   proof (intro allI impI)
     fix B assume "finite B" "B \<subseteq> Z"
--- 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 \<longleftrightarrow> 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 \<longleftrightarrow> continuous_on_topo euclidean euclidean f"
@@ -843,8 +842,8 @@
   have **: "finite {i. X i \<noteq> 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. \<forall>i\<in>I. f (x i) \<in> U i}"
     apply (auto simp add: PiE_iff) unfolding X_def V_def J_def
     proof (auto)
@@ -995,7 +994,7 @@
       using \<open>open U \<and> x \<in> U\<close> unfolding open_fun_def by auto
     with product_topology_open_contains_basis[OF this]
     have "\<exists>X. x \<in> (\<Pi>\<^sub>E i\<in>UNIV. X i) \<and> (\<forall>i. open (X i)) \<and> finite {i. X i \<noteq> UNIV} \<and> (\<Pi>\<^sub>E i\<in>UNIV. X i) \<subseteq> U"
-      unfolding topspace_euclidean open_openin by simp
+      by simp
     then obtain X where H: "x \<in> (\<Pi>\<^sub>E i\<in>UNIV. X i)"
                            "\<And>i. open (X i)"
                            "finite {i. X i \<noteq> UNIV}"
@@ -1064,7 +1063,7 @@
       unfolding open_fun_def by auto
     with product_topology_open_contains_basis[OF this \<open>x \<in> U\<close>]
     have "\<exists>X. x \<in> (\<Pi>\<^sub>E i\<in>UNIV. X i) \<and> (\<forall>i. open (X i)) \<and> finite {i. X i \<noteq> UNIV} \<and> (\<Pi>\<^sub>E i\<in>UNIV. X i) \<subseteq> U"
-      unfolding topspace_euclidean open_openin by simp
+      by simp
     then obtain X where H: "x \<in> (\<Pi>\<^sub>E i\<in>UNIV. X i)"
                            "\<And>i. open (X i)"
                            "finite {i. X i \<noteq> UNIV}"
@@ -1104,8 +1103,7 @@
     show "open U"
       using \<open>U \<in> K\<close> unfolding open_fun_def K_def apply (auto)
       apply (rule product_topology_basis)
-      using \<open>\<And>V. V \<in> B2 \<Longrightarrow> open V\<close> open_UNIV unfolding topspace_euclidean open_openin[symmetric]
-      by auto
+      using \<open>\<And>V. V \<in> B2 \<Longrightarrow> open V\<close> open_UNIV by auto
   qed
 
   show ?thesis using i ii iii by auto
@@ -1155,7 +1153,7 @@
                 = blinfun_apply-`{g::('a\<Rightarrow>'b). \<forall>i\<in>I. g (x i) \<in> U i} \<inter> 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:
--- 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 \<subseteq> - frontier B" and "a \<in> T" and "b \<in> T"
       have "a \<notin> B"
-        by (metis A_def B_def ComplD \<open>a \<in> A\<close> assms(1) closed_open connected_component_subset in_closure_connected_component set_mp)
+        by (metis A_def B_def ComplD \<open>a \<in> A\<close> assms(1) closed_open connected_component_subset in_closure_connected_component subsetD)
       have "T \<inter> B \<noteq> {}"
         using \<open>b \<in> B\<close> \<open>b \<in> T\<close> by blast
       moreover have "T - B \<noteq> {}"
--- 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) \<and> path_connected (G y t) \<and> y \<in> F y t \<and> F y t \<subseteq> G y t \<and> G y t \<subseteq> t"
       using 1 \<open>y \<in> t\<close> by presburger
     have "G y t \<subseteq> path_component_set t y"
-      using * path_component_maximal set_rev_mp by blast
+      using * path_component_maximal rev_subsetD by blast
     then have "\<exists>A. openin ?SS A \<and> y \<in> A \<and> A \<subseteq> path_component_set t x"
       by (metis "*" \<open>G y t \<subseteq> path_component_set t y\<close> dual_order.trans path_component_eq y)
   }
--- 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 \<in> sets M" .
 next
   fix X assume "X \<in> sets M"
-  from sets.sets_into_space[OF this] and assms 
+  from sets.sets_into_space[OF this] and assms
     show "X \<in> 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: "\<And>x. x \<in> A \<Longrightarrow> {x} \<in> sets M" "\<And>x. x \<in> A \<Longrightarrow> {x} \<in> sets N"
   assumes A: "countable A"
   assumes eq: "\<And>a. a \<in> A \<Longrightarrow> emeasure M {a} = emeasure N {a}"
@@ -39,32 +39,19 @@
     by (intro sets_eq_countable assms)
 qed fact+
 
-lemma PiE_singleton: 
-  assumes "f \<in> extensional A"
-  shows   "PiE A (\<lambda>x. {f x}) = {f}"
-proof -
-  {
-    fix g assume "g \<in> PiE A (\<lambda>x. {f x})"
-    hence "g x = f x" for x
-      using assms by (cases "x \<in> 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 \<Rightarrow> 'b set"
   assumes "finite A" "\<And>i. countable (B i)"
   shows   "PiM A (\<lambda>i. count_space (B i)) = count_space (PiE A B)"
 proof (rule measure_eqI_countable')
-  show "space (PiM A (\<lambda>i. count_space (B i))) = PiE A B" 
+  show "space (PiM A (\<lambda>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 \<in> PiE A B"
   hence "PiE A (\<lambda>x. {f x}) \<in> sets (Pi\<^sub>M A (\<lambda>i. count_space (B i)))"
     by (intro sets_PiM_I_finite assms) auto
-  also from f have "PiE A (\<lambda>x. {f x}) = {f}" 
+  also from f have "PiE A (\<lambda>x. {f x}) = {f}"
     by (intro PiE_singleton) (auto simp: PiE_def)
   finally show "{f} \<in> sets (Pi\<^sub>M A (\<lambda>i. count_space (B i)))" .
 next
@@ -74,7 +61,7 @@
   fix f assume f: "f \<in> PiE A B"
   hence "{f} = PiE A (\<lambda>x. {f x})"
     by (intro PiE_singleton [symmetric]) (auto simp: PiE_def)
-  also have "emeasure (Pi\<^sub>M A (\<lambda>i. count_space (B i))) \<dots> = 
+  also have "emeasure (Pi\<^sub>M A (\<lambda>i. count_space (B i))) \<dots> =
                (\<Prod>i\<in>A. emeasure (count_space (B i)) {f i})"
     using f assms by (subst emeasure_PiM) auto
   also have "\<dots> = (\<Prod>i\<in>A. 1)"
@@ -88,7 +75,7 @@
 
 
 definition%important abs_summable_on ::
-    "('a \<Rightarrow> 'b :: {banach, second_countable_topology}) \<Rightarrow> 'a set \<Rightarrow> bool" 
+    "('a \<Rightarrow> 'b :: {banach, second_countable_topology}) \<Rightarrow> 'a set \<Rightarrow> bool"
     (infix "abs'_summable'_on" 50)
  where
    "f abs_summable_on A \<longleftrightarrow> integrable (count_space A) f"
@@ -100,28 +87,28 @@
    "infsetsum f A = lebesgue_integral (count_space A) f"
 
 syntax (ASCII)
-  "_infsetsum" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b::{banach, second_countable_topology}" 
+  "_infsetsum" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b::{banach, second_countable_topology}"
   ("(3INFSETSUM _:_./ _)" [0, 51, 10] 10)
 syntax
-  "_infsetsum" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b::{banach, second_countable_topology}" 
+  "_infsetsum" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b::{banach, second_countable_topology}"
   ("(2\<Sum>\<^sub>a_\<in>_./ _)" [0, 51, 10] 10)
 translations \<comment> \<open>Beware of argument permutation!\<close>
   "\<Sum>\<^sub>ai\<in>A. b" \<rightleftharpoons> "CONST infsetsum (\<lambda>i. b) A"
 
 syntax (ASCII)
-  "_uinfsetsum" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b::{banach, second_countable_topology}" 
+  "_uinfsetsum" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b::{banach, second_countable_topology}"
   ("(3INFSETSUM _:_./ _)" [0, 51, 10] 10)
 syntax
-  "_uinfsetsum" :: "pttrn \<Rightarrow> 'b \<Rightarrow> 'b::{banach, second_countable_topology}" 
+  "_uinfsetsum" :: "pttrn \<Rightarrow> 'b \<Rightarrow> 'b::{banach, second_countable_topology}"
   ("(2\<Sum>\<^sub>a_./ _)" [0, 10] 10)
 translations \<comment> \<open>Beware of argument permutation!\<close>
   "\<Sum>\<^sub>ai. b" \<rightleftharpoons> "CONST infsetsum (\<lambda>i. b) (CONST UNIV)"
 
 syntax (ASCII)
-  "_qinfsetsum" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a::{banach, second_countable_topology}" 
+  "_qinfsetsum" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a::{banach, second_countable_topology}"
   ("(3INFSETSUM _ |/ _./ _)" [0, 0, 10] 10)
 syntax
-  "_qinfsetsum" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a::{banach, second_countable_topology}" 
+  "_qinfsetsum" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a::{banach, second_countable_topology}"
   ("(2\<Sum>\<^sub>a_ | (_)./ _)" [0, 0, 10] 10)
 translations
   "\<Sum>\<^sub>ax|P. t" => "CONST infsetsum (\<lambda>x. t) {x. P}"
@@ -156,7 +143,7 @@
     by (rule restrict_count_space_subset [symmetric]) fact+
   also have "integrable \<dots> f \<longleftrightarrow> 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 \<subseteq> B \<Longrightarrow> f abs_summable_on A \<longleftrightarrow> 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]:
   "(\<lambda>x. norm (f x)) abs_summable_on A \<longleftrightarrow> 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 "\<And>x. x \<in> A \<Longrightarrow> norm (f x) \<le> 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) \<longleftrightarrow> summable (\<lambda>n. if n \<in> A then norm (f n) else 0)"
 proof -
   have "f abs_summable_on A \<longleftrightarrow> summable (\<lambda>x. norm (if x \<in> A then f x else 0))"
-    by (subst abs_summable_on_restrict'[of _ UNIV]) 
+    by (subst abs_summable_on_restrict'[of _ UNIV])
        (simp_all add: abs_summable_on_def integrable_count_space_nat_iff)
   also have "(\<lambda>x. norm (if x \<in> A then f x else 0)) = (\<lambda>x. if x \<in> A then norm (f x) else 0)"
     by auto
@@ -277,7 +264,7 @@
     show "f abs_summable_on insert x A" by simp
 qed
 
-lemma abs_summable_sum: 
+lemma abs_summable_sum:
   assumes "\<And>x. x \<in> A \<Longrightarrow> f x abs_summable_on B"
   shows   "(\<lambda>y. \<Sum>x\<in>A. f x y) abs_summable_on B"
   using assms unfolding abs_summable_on_def by (intro Bochner_Integration.integrable_sum)
@@ -305,7 +292,7 @@
   have *: "count_space B = distr (count_space A) (count_space B) g"
     by (rule distr_bij_count_space [symmetric]) fact
   show ?thesis unfolding abs_summable_on_def
-    by (subst *, subst integrable_distr_eq[of _ _ "count_space B"]) 
+    by (subst *, subst integrable_distr_eq[of _ _ "count_space B"])
        (insert assms, auto simp: bij_betw_def)
 qed
 
@@ -314,7 +301,7 @@
   shows   "f abs_summable_on (g ` A)"
 proof -
   define g' where "g' = inv_into A g"
-  from assms have "(\<lambda>x. f (g x)) abs_summable_on (g' ` g ` A)" 
+  from assms have "(\<lambda>x. f (g x)) abs_summable_on (g' ` g ` A)"
     by (rule abs_summable_on_subset) (auto simp: g'_def inv_into_into)
   also have "?this \<longleftrightarrow> (\<lambda>x. f (g (g' x))) abs_summable_on (g ` A)" unfolding g'_def
     by (intro abs_summable_on_reindex_bij_betw [symmetric] inj_on_imp_bij_betw inj_on_inv_into) auto
@@ -323,7 +310,7 @@
   finally show ?thesis .
 qed
 
-lemma abs_summable_on_reindex_iff: 
+lemma abs_summable_on_reindex_iff:
   "inj_on g A \<Longrightarrow> (\<lambda>x. f (g x)) abs_summable_on A \<longleftrightarrow> f abs_summable_on (g ` A)"
   by (intro abs_summable_on_reindex_bij_betw inj_on_imp_bij_betw)
 
@@ -465,9 +452,9 @@
 lemma Im_infsetsum: "f abs_summable_on A \<Longrightarrow> Im (infsetsum f A) = (\<Sum>\<^sub>ax\<in>A. Im (f x))"
   by (simp add: infsetsum_def abs_summable_on_def)
 
-lemma infsetsum_of_real: 
-  shows "infsetsum (\<lambda>x. of_real (f x) 
-           :: 'a :: {real_normed_algebra_1,banach,second_countable_topology,real_inner}) A = 
+lemma infsetsum_of_real:
+  shows "infsetsum (\<lambda>x. of_real (f x)
+           :: 'a :: {real_normed_algebra_1,banach,second_countable_topology,real_inner}) A =
              of_real (infsetsum f A)"
   unfolding infsetsum_def
   by (rule integral_bounded_linear'[OF bounded_linear_of_real bounded_linear_inner_left[of 1]]) auto
@@ -475,7 +462,7 @@
 lemma infsetsum_finite [simp]: "finite A \<Longrightarrow> infsetsum f A = (\<Sum>x\<in>A. f x)"
   by (simp add: infsetsum_def lebesgue_integral_count_space_finite)
 
-lemma infsetsum_nat: 
+lemma infsetsum_nat:
   assumes "f abs_summable_on A"
   shows   "infsetsum f A = (\<Sum>n. if n \<in> A then f n else 0)"
 proof -
@@ -487,7 +474,7 @@
   finally show ?thesis .
 qed
 
-lemma infsetsum_nat': 
+lemma infsetsum_nat':
   assumes "f abs_summable_on UNIV"
   shows   "infsetsum f UNIV = (\<Sum>n. f n)"
   using assms by (subst infsetsum_nat) auto
@@ -539,7 +526,7 @@
     by (intro infsetsum_Un_disjoint abs_summable_on_subset[OF assms]) auto
   also have "infsetsum f (B - A \<inter> B) = infsetsum f B - infsetsum f (A \<inter> B)"
     by (intro infsetsum_Diff abs_summable_on_subset[OF assms]) auto
-  finally show ?thesis 
+  finally show ?thesis
     by (simp add: algebra_simps)
 qed
 
@@ -550,8 +537,8 @@
   have *: "count_space B = distr (count_space A) (count_space B) g"
     by (rule distr_bij_count_space [symmetric]) fact
   show ?thesis unfolding infsetsum_def
-    by (subst *, subst integral_distr[of _ _ "count_space B"]) 
-       (insert assms, auto simp: bij_betw_def)    
+    by (subst *, subst integral_distr[of _ _ "count_space B"])
+       (insert assms, auto simp: bij_betw_def)
 qed
 
 theorem infsetsum_reindex:
@@ -615,7 +602,7 @@
   shows   "infsetsum f (Sigma A B) = infsetsum (\<lambda>x. infsetsum (\<lambda>y. f (x, y)) (B x)) A"
 proof -
   define B' where "B' = (\<Union>i\<in>A. B i)"
-  have [simp]: "countable B'" 
+  have [simp]: "countable B'"
     unfolding B'_def by (intro countable_UN assms)
   interpret pair_sigma_finite "count_space A" "count_space B'"
     by (intro pair_sigma_finite.intro sigma_finite_measure_count_space_countable) fact+
@@ -627,7 +614,7 @@
     by (intro Bochner_Integration.integrable_cong)
        (auto simp: pair_measure_countable indicator_def split: if_splits)
   finally have integrable: \<dots> .
-  
+
   have "infsetsum (\<lambda>x. infsetsum (\<lambda>y. f (x, y)) (B x)) A =
           (\<integral>x. infsetsum (\<lambda>y. f (x, y)) (B x) \<partial>count_space A)"
     unfolding infsetsum_def by simp
@@ -635,9 +622,9 @@
   proof (rule Bochner_Integration.integral_cong [OF refl])
     show "\<And>x. x \<in> space (count_space A) \<Longrightarrow>
          (\<Sum>\<^sub>ay\<in>B x. f (x, y)) = LINT y|count_space B'. indicat_real (B x) y *\<^sub>R f (x, y)"
-      using infsetsum_altdef'[of _ B'] 
+      using infsetsum_altdef'[of _ B']
       unfolding set_lebesgue_integral_def B'_def
-      by auto 
+      by auto
   qed
   also have "\<dots> = (\<integral>(x,y). indicator (B x) y *\<^sub>R f (x, y) \<partial>(count_space A \<Otimes>\<^sub>M count_space B'))"
     by (subst integral_fst [OF integrable]) auto
@@ -695,12 +682,12 @@
 
 theorem abs_summable_on_Sigma_iff:
   assumes [simp]: "countable A" and "\<And>x. x \<in> A \<Longrightarrow> countable (B x)"
-  shows   "f abs_summable_on Sigma A B \<longleftrightarrow> 
+  shows   "f abs_summable_on Sigma A B \<longleftrightarrow>
              (\<forall>x\<in>A. (\<lambda>y. f (x, y)) abs_summable_on B x) \<and>
              ((\<lambda>x. infsetsum (\<lambda>y. norm (f (x, y))) (B x)) abs_summable_on A)"
 proof safe
   define B' where "B' = (\<Union>x\<in>A. B x)"
-  have [simp]: "countable B'" 
+  have [simp]: "countable B'"
     unfolding B'_def using assms by auto
   interpret pair_sigma_finite "count_space A" "count_space B'"
     by (intro pair_sigma_finite.intro sigma_finite_measure_count_space_countable) fact+
@@ -714,12 +701,12 @@
       by (subst abs_summable_on_altdef' [symmetric]) (auto simp: B'_def)
     also have "count_space (A \<times> B') = count_space A \<Otimes>\<^sub>M count_space B'"
       by (simp add: pair_measure_countable)
-    finally have "integrable (count_space A) 
-                    (\<lambda>x. lebesgue_integral (count_space B') 
+    finally have "integrable (count_space A)
+                    (\<lambda>x. lebesgue_integral (count_space B')
                       (\<lambda>y. indicator (Sigma A B) (x, y) *\<^sub>R norm (f (x, y))))"
       unfolding set_integrable_def by (rule integrable_fst')
     also have "?this \<longleftrightarrow> integrable (count_space A)
-                    (\<lambda>x. lebesgue_integral (count_space B') 
+                    (\<lambda>x. lebesgue_integral (count_space B')
                       (\<lambda>y. indicator (B x) y *\<^sub>R norm (f (x, y))))"
       by (intro integrable_cong refl) (simp_all add: indicator_def)
     also have "\<dots> \<longleftrightarrow> integrable (count_space A) (\<lambda>x. infsetsum (\<lambda>y. norm (f (x, y))) (B x))"
@@ -749,11 +736,11 @@
         fix x assume x: "x \<in> A"
         with * have "(\<lambda>y. f (x, y)) abs_summable_on B x"
           by blast
-        also have "?this \<longleftrightarrow> integrable (count_space B') 
+        also have "?this \<longleftrightarrow> integrable (count_space B')
                       (\<lambda>y. indicator (B x) y *\<^sub>R f (x, y))"
           unfolding set_integrable_def [symmetric]
          using x by (intro abs_summable_on_altdef') (auto simp: B'_def)
-        also have "(\<lambda>y. indicator (B x) y *\<^sub>R f (x, y)) = 
+        also have "(\<lambda>y. indicator (B x) y *\<^sub>R f (x, y)) =
                      (\<lambda>y. indicator (Sigma A B) (x, y) *\<^sub>R f (x, y))"
           using x by (auto simp: indicator_def)
         finally have "integrable (count_space B')
@@ -805,7 +792,7 @@
   also have "\<dots> = PiM A (count_space \<circ> B')"
     unfolding o_def using finite by (intro count_space_PiM_finite [symmetric]) simp_all
   also have "(\<integral>g. (\<Prod>x\<in>A. f x (g x)) \<partial>\<dots>) = (\<Prod>x\<in>A. infsetsum (f x) (B' x))"
-    by (subst product_integral_prod) 
+    by (subst product_integral_prod)
        (insert summable finite, simp_all add: infsetsum_def B'_def abs_summable_on_def)
   also have "\<dots> = (\<Prod>x\<in>A. infsetsum (f x) (B x))"
     by (intro prod.cong refl) (simp_all add: B'_def)
@@ -813,44 +800,44 @@
 qed
 
 lemma infsetsum_uminus: "infsetsum (\<lambda>x. -f x) A = -infsetsum f A"
-  unfolding infsetsum_def abs_summable_on_def 
+  unfolding infsetsum_def abs_summable_on_def
   by (rule Bochner_Integration.integral_minus)
 
 lemma infsetsum_add:
   assumes "f abs_summable_on A" and "g abs_summable_on A"
   shows   "infsetsum (\<lambda>x. f x + g x) A = infsetsum f A + infsetsum g A"
-  using assms unfolding infsetsum_def abs_summable_on_def 
+  using assms unfolding infsetsum_def abs_summable_on_def
   by (rule Bochner_Integration.integral_add)
 
 lemma infsetsum_diff:
   assumes "f abs_summable_on A" and "g abs_summable_on A"
   shows   "infsetsum (\<lambda>x. f x - g x) A = infsetsum f A - infsetsum g A"
-  using assms unfolding infsetsum_def abs_summable_on_def 
+  using assms unfolding infsetsum_def abs_summable_on_def
   by (rule Bochner_Integration.integral_diff)
 
 lemma infsetsum_scaleR_left:
   assumes "c \<noteq> 0 \<Longrightarrow> f abs_summable_on A"
   shows   "infsetsum (\<lambda>x. f x *\<^sub>R c) A = infsetsum f A *\<^sub>R c"
-  using assms unfolding infsetsum_def abs_summable_on_def 
+  using assms unfolding infsetsum_def abs_summable_on_def
   by (rule Bochner_Integration.integral_scaleR_left)
 
 lemma infsetsum_scaleR_right:
   "infsetsum (\<lambda>x. c *\<^sub>R f x) A = c *\<^sub>R infsetsum f A"
-  unfolding infsetsum_def abs_summable_on_def 
+  unfolding infsetsum_def abs_summable_on_def
   by (subst Bochner_Integration.integral_scaleR_right) auto
 
 lemma infsetsum_cmult_left:
   fixes f :: "'a \<Rightarrow> 'b :: {banach, real_normed_algebra, second_countable_topology}"
   assumes "c \<noteq> 0 \<Longrightarrow> f abs_summable_on A"
   shows   "infsetsum (\<lambda>x. f x * c) A = infsetsum f A * c"
-  using assms unfolding infsetsum_def abs_summable_on_def 
+  using assms unfolding infsetsum_def abs_summable_on_def
   by (rule Bochner_Integration.integral_mult_left)
 
 lemma infsetsum_cmult_right:
   fixes f :: "'a \<Rightarrow> 'b :: {banach, real_normed_algebra, second_countable_topology}"
   assumes "c \<noteq> 0 \<Longrightarrow> f abs_summable_on A"
   shows   "infsetsum (\<lambda>x. c * f x) A = c * infsetsum f A"
-  using assms unfolding infsetsum_def abs_summable_on_def 
+  using assms unfolding infsetsum_def abs_summable_on_def
   by (rule Bochner_Integration.integral_mult_right)
 
 lemma infsetsum_cdiv:
--- a/src/HOL/Analysis/Lebesgue_Integral_Substitution.thy	Tue Jan 22 12:28:41 2019 +0100
+++ b/src/HOL/Analysis/Lebesgue_Integral_Substitution.thy	Tue Jan 22 13:57:01 2019 +0100
@@ -69,7 +69,7 @@
             by (simp only: u'v' max_absorb2 min_absorb1)
                (intro continuous_on_subset[OF contg'], insert u'v', auto)
         have "\<And>x. x \<in> {u'..v'} \<Longrightarrow> (g has_real_derivative g' x) (at x within {u'..v'})"
-           using asm by (intro has_field_derivative_subset[OF derivg] set_mp[OF \<open>{u'..v'} \<subseteq> {a..b}\<close>]) auto
+           using asm by (intro has_field_derivative_subset[OF derivg] subsetD[OF \<open>{u'..v'} \<subseteq> {a..b}\<close>]) auto
         hence B: "\<And>x. min u' v' \<le> x \<Longrightarrow> x \<le> max u' v' \<Longrightarrow>
                       (g has_vector_derivative g' x) (at x within {min u' v'..max u' v'})"
             by (simp only: u'v' max_absorb2 min_absorb1)
--- a/src/HOL/Analysis/Path_Connected.thy	Tue Jan 22 12:28:41 2019 +0100
+++ b/src/HOL/Analysis/Path_Connected.thy	Tue Jan 22 13:57:01 2019 +0100
@@ -2851,7 +2851,7 @@
        and cc: "connected_component (- frontier s) x y"
     have "connected_component_set (- frontier s) x \<inter> frontier s \<noteq> {}"
       apply (rule connected_Int_frontier, simp)
-      apply (metis IntI cc connected_component_in connected_component_refl empty_iff interiorE mem_Collect_eq set_rev_mp x)
+      apply (metis IntI cc connected_component_in connected_component_refl empty_iff interiorE mem_Collect_eq rev_subsetD x)
       using  y cc
       by blast
     then have "bounded (connected_component_set (- frontier s) x)"
--- a/src/HOL/Analysis/Sigma_Algebra.thy	Tue Jan 22 12:28:41 2019 +0100
+++ b/src/HOL/Analysis/Sigma_Algebra.thy	Tue Jan 22 13:57:01 2019 +0100
@@ -275,7 +275,7 @@
   hence "\<Union>X = (\<Union>n. from_nat_into X n)"
     using assms by (auto cong del: SUP_cong)
   also have "\<dots> \<in> M" using assms
-    by (auto intro!: countable_nat_UN) (metis \<open>X \<noteq> {}\<close> from_nat_into set_mp)
+    by (auto intro!: countable_nat_UN) (metis \<open>X \<noteq> {}\<close> from_nat_into subsetD)
   finally show ?thesis .
 qed simp
 
--- a/src/HOL/Analysis/Starlike.thy	Tue Jan 22 12:28:41 2019 +0100
+++ b/src/HOL/Analysis/Starlike.thy	Tue Jan 22 13:57:01 2019 +0100
@@ -1588,7 +1588,7 @@
       apply (rule sum.cong)
       using \<open>i \<in> D\<close> \<open>finite D\<close> sum.delta'[of D i "(\<lambda>k. inverse (2 * real (card D)))"]
         d1 assms(2)
-      by (auto simp: inner_Basis set_rev_mp[OF _ assms(2)])
+      by (auto simp: inner_Basis rev_subsetD[OF _ assms(2)])
   }
   note ** = this
   show ?thesis
--- a/src/HOL/Analysis/Tagged_Division.thy	Tue Jan 22 12:28:41 2019 +0100
+++ b/src/HOL/Analysis/Tagged_Division.thy	Tue Jan 22 13:57:01 2019 +0100
@@ -914,7 +914,7 @@
       have "interior m \<inter> interior (\<Union>p) = {}"
       proof (rule Int_interior_Union_intervals)
         show "\<And>T. T\<in>p \<Longrightarrow> interior m \<inter> interior T = {}"
-          by (metis DiffD1 DiffD2 that r1(1) r1(7) set_rev_mp)
+          by (metis DiffD1 DiffD2 that r1(1) r1(7) rev_subsetD)
       qed (use divp in auto)
       then show "interior S \<inter> interior m = {}"
         unfolding divp by auto
--- a/src/HOL/Analysis/Topology_Euclidean_Space.thy	Tue Jan 22 12:28:41 2019 +0100
+++ b/src/HOL/Analysis/Topology_Euclidean_Space.thy	Tue Jan 22 13:57:01 2019 +0100
@@ -154,7 +154,7 @@
   proof
     assume ?lhs
     then have "0 < r'"
-      by (metis (no_types) False \<open>?lhs\<close> centre_in_ball dist_norm le_less_trans mem_ball norm_ge_zero not_less set_mp)
+      by (metis (no_types) False \<open>?lhs\<close> centre_in_ball dist_norm le_less_trans mem_ball norm_ge_zero not_less subsetD)
     then have "(cball a r \<subseteq> cball a' r')"
       by (metis False\<open>?lhs\<close> closure_ball closure_mono not_less)
     then show ?rhs
--- a/src/HOL/Auth/Message.thy	Tue Jan 22 12:28:41 2019 +0100
+++ b/src/HOL/Auth/Message.thy	Tue Jan 22 13:57:01 2019 +0100
@@ -243,7 +243,7 @@
 by (metis parts_idem parts_increasing parts_mono subset_trans)
 
 lemma parts_trans: "[| X\<in> parts G;  G \<subseteq> parts H |] ==> X\<in> parts H"
-by (metis parts_subset_iff set_mp)
+by (metis parts_subset_iff subsetD)
 
 text\<open>Cut\<close>
 lemma parts_cut:
@@ -672,7 +672,7 @@
 lemma Fake_parts_insert_in_Un:
      "\<lbrakk>Z \<in> parts (insert X H);  X \<in> synth (analz H)\<rbrakk> 
       \<Longrightarrow> Z \<in> synth (analz H) \<union> parts H"
-by (metis Fake_parts_insert set_mp)
+by (metis Fake_parts_insert subsetD)
 
 text\<open>\<^term>\<open>H\<close> is sometimes \<^term>\<open>Key ` KK \<union> spies evs\<close>, so can't put 
   \<^term>\<open>G=H\<close>.\<close>
--- a/src/HOL/Cardinals/Cardinal_Order_Relation.thy	Tue Jan 22 12:28:41 2019 +0100
+++ b/src/HOL/Cardinals/Cardinal_Order_Relation.thy	Tue Jan 22 13:57:01 2019 +0100
@@ -1643,7 +1643,7 @@
   unfolding wo_rel_def by (metis card_order_on_well_order_on cr)+
   have L: "isLimOrd r" using ir cr by (metis card_order_infinite_isLimOrd)
   have AsBs: "(\<Union>i \<in> Field r. As (succ r i)) \<subseteq> B"
-  using AsB L apply safe by (metis "0" UN_I set_mp wo_rel.isLimOrd_succ)
+  using AsB L apply safe by (metis "0" UN_I subsetD wo_rel.isLimOrd_succ)
   assume As_s: "\<forall>i\<in>Field r. As (succ r i) \<noteq> As i"
   have 1: "\<forall>i j. (i,j) \<in> r \<and> i \<noteq> j \<longrightarrow> As i \<subset> As j"
   proof safe
--- a/src/HOL/Cardinals/Ordinal_Arithmetic.thy	Tue Jan 22 12:28:41 2019 +0100
+++ b/src/HOL/Cardinals/Ordinal_Arithmetic.thy	Tue Jan 22 13:57:01 2019 +0100
@@ -814,7 +814,7 @@
             with x0notzero zField have SUPP: "SUPP f0 = SUPP g0 \<union> {z}" unfolding support_def by auto
             from g0z have f0z: "f0(z := r.zero) = g0" unfolding f0_def fun_upd_upd by auto
             have f0: "f0 \<in> F" using x0min g0(1)
-              Func_elim[OF set_mp[OF subset_trans[OF F(1)[unfolded FinFunc_def] Int_lower1]] zField]
+              Func_elim[OF subsetD[OF subset_trans[OF F(1)[unfolded FinFunc_def] Int_lower1]] zField]
               unfolding f0_def r.isMinim_def G_def by (force simp: fun_upd_idem)
             from g0(1) maxF(1) have maxf0: "s.maxim (SUPP f0) = z" unfolding SUPP G_def
               by (intro s.maxim_equality) (auto simp: s.isMaxim_def)
@@ -1409,7 +1409,7 @@
       from f \<open>t \<noteq> {}\<close> False have *: "Field r \<noteq> {}" "Field s \<noteq> {}" "Field t \<noteq> {}"
         unfolding Field_def embed_def under_def bij_betw_def by auto
       with f obtain x where "s.zero = f x" "x \<in> Field r" unfolding embed_def bij_betw_def
-        using embed_in_Field[OF r.WELL f] s.zero_under set_mp[OF under_Field[of r]] by blast
+        using embed_in_Field[OF r.WELL f] s.zero_under subsetD[OF under_Field[of r]] by blast
       with f have fz: "f r.zero = s.zero" and inj: "inj_on f (Field r)" and compat: "compat r s f"
         unfolding embed_iff_compat_inj_on_ofilter[OF r s] compat_def
         by (fastforce intro: s.leq_zero_imp)+
--- a/src/HOL/Cardinals/Wellorder_Constructions.thy	Tue Jan 22 12:28:41 2019 +0100
+++ b/src/HOL/Cardinals/Wellorder_Constructions.thy	Tue Jan 22 13:57:01 2019 +0100
@@ -481,7 +481,7 @@
   have bb: "b \<in> Field r" using bA unfolding underS_def Field_def by auto
   assume "\<forall>a\<in>A.  b \<notin> under a"
   hence 0: "\<forall>a \<in> A. a \<in> underS b" using A bA unfolding underS_def
-  by simp (metis (lifting) bb max2_def max2_greater mem_Collect_eq under_def set_rev_mp)
+  by simp (metis (lifting) bb max2_def max2_greater mem_Collect_eq under_def rev_subsetD)
   have "(suc A, b) \<in> r" apply(rule suc_least[OF A bb]) using 0 unfolding underS_def by auto
   thus False using bA unfolding underS_def by simp (metis ANTISYM antisymD)
 qed
--- a/src/HOL/Cardinals/Wellorder_Extension.thy	Tue Jan 22 12:28:41 2019 +0100
+++ b/src/HOL/Cardinals/Wellorder_Extension.thy	Tue Jan 22 13:57:01 2019 +0100
@@ -52,7 +52,7 @@
   shows "extension_on (Field (\<Union>R)) (\<Union>R) p"
   using assms
   by (simp add: chain_subset_def extension_on_def)
-     (metis (no_types) mono_Field set_mp)
+     (metis (no_types) mono_Field subsetD)
 
 lemma downset_on_empty [simp]: "downset_on {} p"
   by (auto simp: downset_on_def)
--- a/src/HOL/Datatype_Examples/Derivation_Trees/Gram_Lang.thy	Tue Jan 22 12:28:41 2019 +0100
+++ b/src/HOL/Datatype_Examples/Derivation_Trees/Gram_Lang.thy	Tue Jan 22 13:57:01 2019 +0100
@@ -40,7 +40,7 @@
 assumes "inFr ns tr t" and "ns \<subseteq> ns'"
 shows "inFr ns' tr t"
 using assms apply(induct arbitrary: ns' rule: inFr.induct)
-using Base Ind by (metis inFr.simps set_mp)+
+using Base Ind by (metis inFr.simps subsetD)+
 
 lemma inFr_Ind_minus:
 assumes "inFr ns1 tr1 t" and "Inr tr1 \<in> cont tr"
@@ -111,7 +111,7 @@
 assumes "inItr ns tr n" and "ns \<subseteq> ns'"
 shows "inItr ns' tr n"
 using assms apply(induct arbitrary: ns' rule: inItr.induct)
-using Base Ind by (metis inItr.simps set_mp)+
+using Base Ind by (metis inItr.simps subsetD)+
 
 
 (* The subtree relation *)
@@ -137,7 +137,7 @@
 assumes "subtr ns tr1 tr2" and "ns \<subseteq> ns'"
 shows "subtr ns' tr1 tr2"
 using assms apply(induct arbitrary: ns' rule: subtr.induct)
-using Refl Step by (metis subtr.simps set_mp)+
+using Refl Step by (metis subtr.simps subsetD)+
 
 lemma subtr_trans_Un:
 assumes "subtr ns12 tr1 tr2" and "subtr ns23 tr2 tr3"
@@ -188,7 +188,7 @@
 assumes "subtr2 ns tr1 tr2" and "ns \<subseteq> ns'"
 shows "subtr2 ns' tr1 tr2"
 using assms apply(induct arbitrary: ns' rule: subtr2.induct)
-using Refl Step by (metis subtr2.simps set_mp)+
+using Refl Step by (metis subtr2.simps subsetD)+
 
 lemma subtr2_trans_Un:
 assumes "subtr2 ns12 tr1 tr2" and "subtr2 ns23 tr2 tr3"
--- a/src/HOL/IMP/Abs_Int2.thy	Tue Jan 22 12:28:41 2019 +0100
+++ b/src/HOL/IMP/Abs_Int2.thy	Tue Jan 22 13:57:01 2019 +0100
@@ -38,7 +38,7 @@
 begin
 
 lemma in_gamma_inf: "x \<in> \<gamma> a1 \<Longrightarrow> x \<in> \<gamma> a2 \<Longrightarrow> x \<in> \<gamma>(a1 \<sqinter> a2)"
-by (metis IntI inter_gamma_subset_gamma_inf set_mp)
+by (metis IntI inter_gamma_subset_gamma_inf subsetD)
 
 lemma gamma_inf: "\<gamma>(a1 \<sqinter> a2) = \<gamma> a1 \<inter> \<gamma> a2"
 by(rule equalityI[OF _ inter_gamma_subset_gamma_inf])
--- a/src/HOL/IMP/Collecting.thy	Tue Jan 22 12:28:41 2019 +0100
+++ b/src/HOL/IMP/Collecting.thy	Tue Jan 22 13:57:01 2019 +0100
@@ -184,10 +184,10 @@
     by(fastforce simp: strip_eq_Seq step_def post_def last_append annos_ne)
 next
   case IfTrue thus ?case apply(auto simp: strip_eq_If step_def post_def)
-    by (metis (lifting,full_types) mem_Collect_eq set_mp)
+    by (metis (lifting,full_types) mem_Collect_eq subsetD)
 next
   case IfFalse thus ?case apply(auto simp: strip_eq_If step_def post_def)
-    by (metis (lifting,full_types) mem_Collect_eq set_mp)
+    by (metis (lifting,full_types) mem_Collect_eq subsetD)
 next
   case (WhileTrue b s1 c' s2 s3)
   from WhileTrue.prems(1) obtain I P C' Q where "C = {I} WHILE b DO {P} C' {Q}" "strip C' = c'"
--- a/src/HOL/IMP/Live.thy	Tue Jan 22 12:28:41 2019 +0100
+++ b/src/HOL/IMP/Live.thy	Tue Jan 22 13:57:01 2019 +0100
@@ -87,13 +87,13 @@
 next
   case (WhileFalse b s c)
   hence "~ bval b t"
-    by (metis L_While_vars bval_eq_if_eq_on_vars set_mp)
-  thus ?case by(metis WhileFalse.prems L_While_X big_step.WhileFalse set_mp)
+    by (metis L_While_vars bval_eq_if_eq_on_vars subsetD)
+  thus ?case by(metis WhileFalse.prems L_While_X big_step.WhileFalse subsetD)
 next
   case (WhileTrue b s1 c s2 s3 X t1)
   let ?w = "WHILE b DO c"
   from \<open>bval b s1\<close> WhileTrue.prems have "bval b t1"
-    by (metis L_While_vars bval_eq_if_eq_on_vars set_mp)
+    by (metis L_While_vars bval_eq_if_eq_on_vars subsetD)
   have "s1 = t1 on L c (L ?w X)" using L_While_pfp WhileTrue.prems
     by (blast)
   from WhileTrue.IH(1)[OF this] obtain t2 where
@@ -151,14 +151,14 @@
   thus ?case using \<open>~bval b t\<close> by auto
 next
   case (WhileFalse b s c)
-  hence "~ bval b t" by (metis L_While_vars bval_eq_if_eq_on_vars set_mp)
+  hence "~ bval b t" by (metis L_While_vars bval_eq_if_eq_on_vars subsetD)
   thus ?case
-    by simp (metis L_While_X WhileFalse.prems big_step.WhileFalse set_mp)
+    by simp (metis L_While_X WhileFalse.prems big_step.WhileFalse subsetD)
 next
   case (WhileTrue b s1 c s2 s3 X t1)
   let ?w = "WHILE b DO c"
   from \<open>bval b s1\<close> WhileTrue.prems have "bval b t1"
-    by (metis L_While_vars bval_eq_if_eq_on_vars set_mp)
+    by (metis L_While_vars bval_eq_if_eq_on_vars subsetD)
   have "s1 = t1 on L c (L ?w X)"
     using L_While_pfp WhileTrue.prems by blast
   from WhileTrue.IH(1)[OF this] obtain t2 where
@@ -237,15 +237,15 @@
 next
   case (WhileFalse b s c)
   hence "~ bval b t"
-    by auto (metis L_While_vars bval_eq_if_eq_on_vars set_rev_mp)
+    by auto (metis L_While_vars bval_eq_if_eq_on_vars rev_subsetD)
   thus ?case using WhileFalse
-    by auto (metis L_While_X big_step.WhileFalse set_mp)
+    by auto (metis L_While_X big_step.WhileFalse subsetD)
 next
   case (WhileTrue b s1 bc' s2 s3 w X t1)
   then obtain c' where w: "w = WHILE b DO c'"
     and bc': "bc' = bury c' (L (WHILE b DO c') X)" by auto
   from \<open>bval b s1\<close> WhileTrue.prems w have "bval b t1"
-    by auto (metis L_While_vars bval_eq_if_eq_on_vars set_mp)
+    by auto (metis L_While_vars bval_eq_if_eq_on_vars subsetD)
   note IH = WhileTrue.hyps(3,5)
   have "s1 = t1 on L c' (L w X)"
     using L_While_pfp WhileTrue.prems w by blast
--- a/src/HOL/IMP/Live_True.thy	Tue Jan 22 12:28:41 2019 +0100
+++ b/src/HOL/IMP/Live_True.thy	Tue Jan 22 13:57:01 2019 +0100
@@ -88,13 +88,13 @@
 next
   case (WhileFalse b s c)
   hence "~ bval b t"
-    by (metis L_While_vars bval_eq_if_eq_on_vars set_mp)
+    by (metis L_While_vars bval_eq_if_eq_on_vars subsetD)
   thus ?case using WhileFalse.prems L_While_X[of X b c] by auto
 next
   case (WhileTrue b s1 c s2 s3 X t1)
   let ?w = "WHILE b DO c"
   from \<open>bval b s1\<close> WhileTrue.prems have "bval b t1"
-    by (metis L_While_vars bval_eq_if_eq_on_vars set_mp)
+    by (metis L_While_vars bval_eq_if_eq_on_vars subsetD)
   have "s1 = t1 on L c (L ?w X)" using  L_While_pfp WhileTrue.prems
     by (blast)
   from WhileTrue.IH(1)[OF this] obtain t2 where
--- a/src/HOL/Library/Countable_Set_Type.thy	Tue Jan 22 12:28:41 2019 +0100
+++ b/src/HOL/Library/Countable_Set_Type.thy	Tue Jan 22 13:57:01 2019 +0100
@@ -150,8 +150,8 @@
 lemmas contra_csubsetD[no_atp] = contra_subsetD[Transfer.transferred]
 lemmas csubset_refl = subset_refl[Transfer.transferred]
 lemmas csubset_trans = subset_trans[Transfer.transferred]
-lemmas cset_rev_mp = set_rev_mp[Transfer.transferred]
-lemmas cset_mp = set_mp[Transfer.transferred]
+lemmas cset_rev_mp = rev_subsetD[Transfer.transferred]
+lemmas cset_mp = subsetD[Transfer.transferred]
 lemmas csubset_not_fsubset_eq[code] = subset_not_subset_eq[Transfer.transferred]
 lemmas eq_cmem_trans = eq_mem_trans[Transfer.transferred]
 lemmas csubset_antisym[intro!] = subset_antisym[Transfer.transferred]
--- a/src/HOL/Library/Disjoint_Sets.thy	Tue Jan 22 12:28:41 2019 +0100
+++ b/src/HOL/Library/Disjoint_Sets.thy	Tue Jan 22 13:57:01 2019 +0100
@@ -58,6 +58,49 @@
     by (auto simp flip: INT_Int_distrib)
 qed
 
+lemma diff_Union_pairwise_disjoint:
+  assumes "pairwise disjnt \<A>" "\<B> \<subseteq> \<A>"
+  shows "\<Union>\<A> - \<Union>\<B> = \<Union>(\<A> - \<B>)"
+proof -
+  have "False"
+    if x: "x \<in> A" "x \<in> B" and AB: "A \<in> \<A>" "A \<notin> \<B>" "B \<in> \<B>" for x A B
+  proof -
+    have "A \<inter> B = {}"
+      using assms disjointD AB by blast
+  with x show ?thesis
+    by blast
+  qed
+  then show ?thesis by auto
+qed
+
+lemma Int_Union_pairwise_disjoint:
+  assumes "pairwise disjnt (\<A> \<union> \<B>)"
+  shows "\<Union>\<A> \<inter> \<Union>\<B> = \<Union>(\<A> \<inter> \<B>)"
+proof -
+  have "False"
+    if x: "x \<in> A" "x \<in> B" and AB: "A \<in> \<A>" "A \<notin> \<B>" "B \<in> \<B>" for x A B
+  proof -
+    have "A \<inter> B = {}"
+      using assms disjointD AB by blast
+  with x show ?thesis
+    by blast
+  qed
+  then show ?thesis by auto
+qed
+
+lemma psubset_Union_pairwise_disjoint:
+  assumes \<B>: "pairwise disjnt \<B>" and "\<A> \<subset> \<B> - {{}}"
+  shows "\<Union>\<A> \<subset> \<Union>\<B>"
+  unfolding psubset_eq
+proof
+  show "\<Union>\<A> \<subseteq> \<Union>\<B>"
+    using assms by blast
+  have "\<A> \<subseteq> \<B>" "\<Union>(\<B> - \<A> \<inter> (\<B> - {{}})) \<noteq> {}"
+    using assms by blast+
+  then show "\<Union>\<A> \<noteq> \<Union>\<B>"
+    using diff_Union_pairwise_disjoint [OF \<B>] by blast
+qed
+
 subsubsection "Family of Disjoint Sets"
 
 definition disjoint_family_on :: "('i \<Rightarrow> 'a set) \<Rightarrow> 'i set \<Rightarrow> bool" where
--- a/src/HOL/Library/FSet.thy	Tue Jan 22 12:28:41 2019 +0100
+++ b/src/HOL/Library/FSet.thy	Tue Jan 22 13:57:01 2019 +0100
@@ -236,8 +236,8 @@
 lemmas contra_fsubsetD[no_atp] = contra_subsetD[Transfer.transferred]
 lemmas fsubset_refl = subset_refl[Transfer.transferred]
 lemmas fsubset_trans = subset_trans[Transfer.transferred]
-lemmas fset_rev_mp = set_rev_mp[Transfer.transferred]
-lemmas fset_mp = set_mp[Transfer.transferred]
+lemmas fset_rev_mp = rev_subsetD[Transfer.transferred]
+lemmas fset_mp = subsetD[Transfer.transferred]
 lemmas fsubset_not_fsubset_eq[code] = subset_not_subset_eq[Transfer.transferred]
 lemmas eq_fmem_trans = eq_mem_trans[Transfer.transferred]
 lemmas fsubset_antisym[intro!] = subset_antisym[Transfer.transferred]
--- a/src/HOL/Library/FuncSet.thy	Tue Jan 22 12:28:41 2019 +0100
+++ b/src/HOL/Library/FuncSet.thy	Tue Jan 22 13:57:01 2019 +0100
@@ -534,6 +534,49 @@
     by auto
 qed
 
+lemma PiE_singleton: 
+  assumes "f \<in> extensional A"
+  shows   "PiE A (\<lambda>x. {f x}) = {f}"
+proof -
+  {
+    fix g assume "g \<in> PiE A (\<lambda>x. {f x})"
+    hence "g x = f x" for x
+      using assms by (cases "x \<in> 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 PiE_eq_singleton: "(\<Pi>\<^sub>E i\<in>I. S i) = {\<lambda>i\<in>I. f i} \<longleftrightarrow> (\<forall>i\<in>I. S i = {f i})"
+  by (metis (mono_tags, lifting) PiE_eq PiE_singleton insert_not_empty restrict_apply' restrict_extensional)
+
+lemma all_PiE_elements:
+   "(\<forall>z \<in> PiE I S. \<forall>i \<in> I. P i (z i)) \<longleftrightarrow> PiE I S = {} \<or> (\<forall>i \<in> I. \<forall>x \<in> S i. P i x)" (is "?lhs = ?rhs")
+proof (cases "PiE I S = {}")
+  case False
+  then obtain f where f: "\<And>i. i \<in> I \<Longrightarrow> f i \<in> S i"
+    by fastforce
+  show ?thesis
+  proof
+    assume L: ?lhs
+    have "P i x"
+      if "i \<in> I" "x \<in> S i" for i x
+    proof -
+      have "(\<lambda>j \<in> I. if j=i then x else f j) \<in> PiE I S"
+        by (simp add: f that(2))
+      then have "P i ((\<lambda>j \<in> I. if j=i then x else f j) i)"
+        using L that(1) by blast
+      with that show ?thesis
+        by simp
+    qed
+    then show ?rhs
+      by (simp add: False)
+  qed fastforce
+qed simp
+
+lemma PiE_ext: "\<lbrakk>x \<in> PiE k s; y \<in> PiE k s; \<And>i. i \<in> k \<Longrightarrow> x i = y i\<rbrakk> \<Longrightarrow> x = y"
+  by (metis ext PiE_E)
+
 
 subsubsection \<open>Injective Extensional Function Spaces\<close>
 
--- a/src/HOL/Metis_Examples/Abstraction.thy	Tue Jan 22 12:28:41 2019 +0100
+++ b/src/HOL/Metis_Examples/Abstraction.thy	Tue Jan 22 13:57:01 2019 +0100
@@ -154,7 +154,7 @@
 lemma
   "(\<lambda>x. f (f x)) ` ((\<lambda>x. Suc(f x)) ` {x. even x}) \<subseteq> A \<Longrightarrow>
    (\<forall>x. even x --> f (f (Suc(f x))) \<in> A)"
-by (metis mem_Collect_eq imageI set_rev_mp)
+by (metis mem_Collect_eq imageI rev_subsetD)
 
 lemma "f \<in> (\<lambda>u v. b \<times> u \<times> v) ` A \<Longrightarrow> \<forall>u v. P (b \<times> u \<times> v) \<Longrightarrow> P(f y)"
 by (metis (lifting) imageE)
--- a/src/HOL/Metis_Examples/Big_O.thy	Tue Jan 22 12:28:41 2019 +0100
+++ b/src/HOL/Metis_Examples/Big_O.thy	Tue Jan 22 13:57:01 2019 +0100
@@ -314,7 +314,7 @@
 by (metis bigo_mult bigo_refl set_times_mono3 subset_trans)
 
 lemma bigo_mult3: "f \<in> O(h) \<Longrightarrow> g \<in> O(j) \<Longrightarrow> f * g \<in> O(h * j)"
-by (metis bigo_mult set_rev_mp set_times_intro)
+by (metis bigo_mult rev_subsetD set_times_intro)
 
 lemma bigo_mult4 [intro]:"f \<in> k +o O(h) \<Longrightarrow> g * f \<in> (g * k) +o O(g * h)"
 by (metis bigo_mult2 set_plus_mono_b set_times_intro2 set_times_plus_distrib)
--- a/src/HOL/Metis_Examples/Message.thy	Tue Jan 22 12:28:41 2019 +0100
+++ b/src/HOL/Metis_Examples/Message.thy	Tue Jan 22 13:57:01 2019 +0100
@@ -78,7 +78,7 @@
 lemma parts_mono: "G \<subseteq> H ==> parts(G) \<subseteq> parts(H)"
 apply auto
 apply (erule parts.induct)
-   apply (metis parts.Inj set_rev_mp)
+   apply (metis parts.Inj rev_subsetD)
   apply (metis parts.Fst)
  apply (metis parts.Snd)
 by (metis parts.Body)
--- a/src/HOL/Probability/Conditional_Expectation.thy	Tue Jan 22 12:28:41 2019 +0100
+++ b/src/HOL/Probability/Conditional_Expectation.thy	Tue Jan 22 13:57:01 2019 +0100
@@ -438,7 +438,7 @@
 proof (rule nn_cond_exp_charact, auto)
   interpret G: sigma_finite_subalgebra M G by (rule nested_subalg_is_sigma_finite[OF assms(1) assms(2)])
   fix A assume [measurable]: "A \<in> sets F"
-  then have [measurable]: "A \<in> sets G" using assms(2) by (meson set_mp subalgebra_def)
+  then have [measurable]: "A \<in> sets G" using assms(2) by (meson subsetD subalgebra_def)
 
   have "set_nn_integral M A (nn_cond_exp M G f) = (\<integral>\<^sup>+ x. indicator A x * nn_cond_exp M G f x\<partial>M)"
     by (metis (no_types) mult.commute)
@@ -1032,7 +1032,7 @@
   show "integrable M (real_cond_exp M G f)" by (auto simp add: assms G.real_cond_exp_int(1))
 
   fix A assume [measurable]: "A \<in> sets F"
-  then have [measurable]: "A \<in> sets G" using assms(2) by (meson set_mp subalgebra_def)
+  then have [measurable]: "A \<in> sets G" using assms(2) by (meson subsetD subalgebra_def)
   have "set_lebesgue_integral M A (real_cond_exp M G f) = set_lebesgue_integral M A f"
     by (rule G.real_cond_exp_intA[symmetric], auto simp add: assms(3))
   also have "... = set_lebesgue_integral M A (real_cond_exp M F f)"
@@ -1046,7 +1046,7 @@
   shows "AE x in M. real_cond_exp M F (\<lambda>x. \<Sum>i\<in>I. f i x) x = (\<Sum>i\<in>I. real_cond_exp M F (f i) x)"
 proof (rule real_cond_exp_charact)
   fix A assume [measurable]: "A \<in> sets F"
-  then have A_meas [measurable]: "A \<in> sets M" by (meson set_mp subalg subalgebra_def)
+  then have A_meas [measurable]: "A \<in> sets M" by (meson subsetD subalg subalgebra_def)
   have *: "integrable M (\<lambda>x. indicator A x * f i x)" for i
     using integrable_mult_indicator[OF \<open>A \<in> sets M\<close> assms(1)] by auto
   have **: "integrable M (\<lambda>x. indicator A x * real_cond_exp M F (f i) x)" for i
--- a/src/HOL/Probability/Fin_Map.thy	Tue Jan 22 12:28:41 2019 +0100
+++ b/src/HOL/Probability/Fin_Map.thy	Tue Jan 22 13:57:01 2019 +0100
@@ -1094,7 +1094,7 @@
     show "range S' \<subseteq> Collect open"
       using S
       apply (auto simp add: from_nat_into countable_basis_proj S'_def)
-      apply (metis UNIV_not_empty Union_empty from_nat_into set_mp topological_basis_open[OF basis_proj] basis_proj_def)
+      apply (metis UNIV_not_empty Union_empty from_nat_into subsetD topological_basis_open[OF basis_proj] basis_proj_def)
       done
     show "Collect open \<subseteq> Pow (space borel)" by simp
     show "sets borel = sigma_sets (space borel) (Collect open)"
@@ -1322,7 +1322,7 @@
   unfolding mapmeasure_def
 proof (subst emeasure_distr, subst measurable_cong_sets[OF s2 refl], rule fm_measurable)
   have "X \<subseteq> space (Pi\<^sub>M J (\<lambda>_. N))" using assms by (simp add: sets.sets_into_space)
-  from assms inj_on_fm[of "\<lambda>_. N"] set_mp[OF this] have "fm -` fm ` X \<inter> space (Pi\<^sub>M J (\<lambda>_. N)) = X"
+  from assms inj_on_fm[of "\<lambda>_. N"] subsetD[OF this] have "fm -` fm ` X \<inter> space (Pi\<^sub>M J (\<lambda>_. N)) = X"
     by (auto simp: vimage_image_eq inj_on_def)
   thus "emeasure M X = emeasure M (fm -` fm ` X \<inter> space M)" using s1
     by simp
--- a/src/HOL/Probability/Projective_Limit.thy	Tue Jan 22 12:28:41 2019 +0100
+++ b/src/HOL/Probability/Projective_Limit.thy	Tue Jan 22 13:57:01 2019 +0100
@@ -260,7 +260,7 @@
     have "\<mu>G (Z n) - \<mu>G (Y n) = \<mu>G (Z n - Y n)"
       using J J_mono K_sets \<open>n \<ge> 1\<close>
       by (simp only: emeasure_eq_measure Z_def)
-         (auto dest!: bspec[where x=n] intro!: measure_Diff[symmetric] set_mp[OF K_B]
+         (auto dest!: bspec[where x=n] intro!: measure_Diff[symmetric] subsetD[OF K_B]
                intro!: arg_cong[where f=ennreal]
                simp: extensional_restrict emeasure_eq_measure prod_emb_iff sets_P space_P
                      ennreal_minus measure_nonneg)
--- a/src/HOL/Probability/Weak_Convergence.thy	Tue Jan 22 12:28:41 2019 +0100
+++ b/src/HOL/Probability/Weak_Convergence.thy	Tue Jan 22 13:57:01 2019 +0100
@@ -359,7 +359,7 @@
 proof -
   interpret real_distribution M by simp
   show ?thesis
-    by (auto intro!: * simp: frontier_real_Iic isCont_cdf emeasure_eq_measure weak_conv_m_def weak_conv_def cdf_def2)
+    by (auto intro!: * simp: frontier_real_atMost isCont_cdf emeasure_eq_measure weak_conv_m_def weak_conv_def cdf_def2)
 qed
 
 theorem integral_cts_step_conv_imp_weak_conv:
--- a/src/HOL/Set.thy	Tue Jan 22 12:28:41 2019 +0100
+++ b/src/HOL/Set.thy	Tue Jan 22 13:57:01 2019 +0100
@@ -462,18 +462,18 @@
   by (simp add: less_eq_set_def le_fun_def)
   \<comment> \<open>Rule in Modus Ponens style.\<close>
 
-lemma rev_subsetD [intro?]: "c \<in> A \<Longrightarrow> A \<subseteq> B \<Longrightarrow> c \<in> B"
+lemma rev_subsetD [intro?,no_atp]: "c \<in> A \<Longrightarrow> A \<subseteq> B \<Longrightarrow> c \<in> B"
   \<comment> \<open>The same, with reversed premises for use with @{method erule} -- cf. @{thm rev_mp}.\<close>
   by (rule subsetD)
 
-lemma subsetCE [elim]: "A \<subseteq> B \<Longrightarrow> (c \<notin> A \<Longrightarrow> P) \<Longrightarrow> (c \<in> B \<Longrightarrow> P) \<Longrightarrow> P"
+lemma subsetCE [elim,no_atp]: "A \<subseteq> B \<Longrightarrow> (c \<notin> A \<Longrightarrow> P) \<Longrightarrow> (c \<in> B \<Longrightarrow> P) \<Longrightarrow> P"
   \<comment> \<open>Classical elimination rule.\<close>
   by (auto simp add: less_eq_set_def le_fun_def)
 
 lemma subset_eq: "A \<subseteq> B \<longleftrightarrow> (\<forall>x\<in>A. x \<in> B)"
   by blast
 
-lemma contra_subsetD: "A \<subseteq> B \<Longrightarrow> c \<notin> B \<Longrightarrow> c \<notin> A"
+lemma contra_subsetD [no_atp]: "A \<subseteq> B \<Longrightarrow> c \<notin> B \<Longrightarrow> c \<notin> A"
   by blast
 
 lemma subset_refl: "A \<subseteq> A"
@@ -482,12 +482,6 @@
 lemma subset_trans: "A \<subseteq> B \<Longrightarrow> B \<subseteq> C \<Longrightarrow> A \<subseteq> C"
   by (fact order_trans)
 
-lemma set_rev_mp: "x \<in> A \<Longrightarrow> A \<subseteq> B \<Longrightarrow> x \<in> B"
-  by (rule subsetD)
-
-lemma set_mp: "A \<subseteq> B \<Longrightarrow> x \<in> A \<Longrightarrow> x \<in> B"
-  by (rule subsetD)
-
 lemma subset_not_subset_eq [code]: "A \<subset> B \<longleftrightarrow> A \<subseteq> B \<and> \<not> B \<subseteq> A"
   by (fact less_le_not_le)
 
@@ -495,7 +489,7 @@
   by simp
 
 lemmas basic_trans_rules [trans] =
-  order_trans_rules set_rev_mp set_mp eq_mem_trans
+  order_trans_rules rev_subsetD subsetD eq_mem_trans
 
 
 subsubsection \<open>Equality\<close>
@@ -1947,6 +1941,8 @@
 hide_const (open) member not_member
 
 lemmas equalityI = subset_antisym
+lemmas set_mp = subsetD
+lemmas set_rev_mp = rev_subsetD
 
 ML \<open>
 val Ball_def = @{thm Ball_def}
--- a/src/HOL/Types_To_Sets/Examples/Linear_Algebra_On_With.thy	Tue Jan 22 12:28:41 2019 +0100
+++ b/src/HOL/Types_To_Sets/Examples/Linear_Algebra_On_With.thy	Tue Jan 22 13:57:01 2019 +0100
@@ -22,7 +22,7 @@
   assume transfer_rules[transfer_rule]: "(A ===> A ===> A) p p'" "A z z'" "((=) ===> A ===> A) s s'" "rel_set A X X'"
   have "Domainp A z" using \<open>A z z'\<close> by force
   have *: "t \<subseteq> X \<Longrightarrow> (\<forall>x\<in>t. Domainp A x)" for t
-    by (meson Domainp.DomainI \<open>rel_set A X X'\<close> rel_setD1 set_mp)
+    by (meson Domainp.DomainI \<open>rel_set A X X'\<close> rel_setD1 subsetD)
   note swt=sum_with_transfer[OF assms(1,2,2), THEN rel_funD, THEN rel_funD, THEN rel_funD, THEN rel_funD, OF transfer_rules(1,2)]
   have DsI: "Domainp A (sum_with p z r t)" if "\<And>x. x \<in> t \<Longrightarrow> Domainp A (r x)" "t \<subseteq> Collect (Domainp A)" for r t
   proof cases
@@ -59,7 +59,7 @@
   fix p p' z z' X X' and s s'::"'c \<Rightarrow> _"
   assume [transfer_rule]: "(A ===> A ===> A) p p'" "A z z'" "((=) ===> A ===> A) s s'" "rel_set A X X'"
   have *: "t \<subseteq> X \<Longrightarrow> (\<forall>x\<in>t. Domainp A x)" for t
-    by (meson Domainp.DomainI \<open>rel_set A X X'\<close> rel_setD1 set_mp)
+    by (meson Domainp.DomainI \<open>rel_set A X X'\<close> rel_setD1 subsetD)
   show "(\<exists>t u. finite t \<and> t \<subseteq> X \<and> sum_with p z (\<lambda>v. s (u v) v) t = z \<and> (\<exists>v\<in>t. u v \<noteq> 0)) =
     (\<exists>t u. finite t \<and> t \<subseteq> X' \<and> sum_with p' z' (\<lambda>v. s' (u v) v) t = z' \<and> (\<exists>v\<in>t. u v \<noteq> 0))"
     apply (transfer_prover_start, transfer_step+)
--- a/src/HOL/Vector_Spaces.thy	Tue Jan 22 12:28:41 2019 +0100
+++ b/src/HOL/Vector_Spaces.thy	Tue Jan 22 13:57:01 2019 +0100
@@ -817,7 +817,7 @@
     by (simp add: vs1.extend_basis_superset[OF i] vs1.span_mono)
   then show "x \<in> range (construct B f)"
     using f2 x by (metis (no_types) construct_basis[OF i, of _ f]
-        vs1.span_extend_basis[OF i] set_mp span_image spans_image)
+        vs1.span_extend_basis[OF i] subsetD span_image spans_image)
 qed
 
 lemma range_construct_eq_span: