author wenzelm 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)"
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"

+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"
-
-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
+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"
+
+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"
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 (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"
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"
-  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"

@@ -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])
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))"

-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)"

-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
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'"
-    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)

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

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
-     (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
+  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 @@
\<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:```