--- a/src/HOL/Algebra/Complete_Lattice.thy Tue Jan 22 10:50:47 2019 +0000
+++ b/src/HOL/Algebra/Complete_Lattice.thy Tue Jan 22 12:00:16 2019 +0000
@@ -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 10:50:47 2019 +0000
+++ b/src/HOL/Algebra/Group_Action.thy Tue Jan 22 12:00:16 2019 +0000
@@ -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 10:50:47 2019 +0000
+++ b/src/HOL/Algebra/Ideal.thy Tue Jan 22 12:00:16 2019 +0000
@@ -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 10:50:47 2019 +0000
+++ b/src/HOL/Algebra/Polynomials.thy Tue Jan 22 12:00:16 2019 +0000
@@ -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 10:50:47 2019 +0000
+++ b/src/HOL/Analysis/Abstract_Topology.thy Tue Jan 22 12:00:16 2019 +0000
@@ -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)
--- a/src/HOL/Analysis/Brouwer_Fixpoint.thy Tue Jan 22 10:50:47 2019 +0000
+++ b/src/HOL/Analysis/Brouwer_Fixpoint.thy Tue Jan 22 12:00:16 2019 +0000
@@ -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 10:50:47 2019 +0000
+++ b/src/HOL/Analysis/Caratheodory.thy Tue Jan 22 12:00:16 2019 +0000
@@ -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 10:50:47 2019 +0000
+++ b/src/HOL/Analysis/Cauchy_Integral_Theorem.thy Tue Jan 22 12:00:16 2019 +0000
@@ -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 10:50:47 2019 +0000
+++ b/src/HOL/Analysis/Conformal_Mappings.thy Tue Jan 22 12:00:16 2019 +0000
@@ -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/Derivative.thy Tue Jan 22 10:50:47 2019 +0000
+++ b/src/HOL/Analysis/Derivative.thy Tue Jan 22 12:00:16 2019 +0000
@@ -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 10:50:47 2019 +0000
+++ b/src/HOL/Analysis/Elementary_Metric_Spaces.thy Tue Jan 22 12:00:16 2019 +0000
@@ -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 10:50:47 2019 +0000
+++ b/src/HOL/Analysis/Elementary_Normed_Spaces.thy Tue Jan 22 12:00:16 2019 +0000
@@ -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 10:50:47 2019 +0000
+++ b/src/HOL/Analysis/Elementary_Topology.thy Tue Jan 22 12:00:16 2019 +0000
@@ -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/Further_Topology.thy Tue Jan 22 10:50:47 2019 +0000
+++ b/src/HOL/Analysis/Further_Topology.thy Tue Jan 22 12:00:16 2019 +0000
@@ -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 10:50:47 2019 +0000
+++ b/src/HOL/Analysis/Homotopy.thy Tue Jan 22 12:00:16 2019 +0000
@@ -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/Lebesgue_Integral_Substitution.thy Tue Jan 22 10:50:47 2019 +0000
+++ b/src/HOL/Analysis/Lebesgue_Integral_Substitution.thy Tue Jan 22 12:00:16 2019 +0000
@@ -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 10:50:47 2019 +0000
+++ b/src/HOL/Analysis/Path_Connected.thy Tue Jan 22 12:00:16 2019 +0000
@@ -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 10:50:47 2019 +0000
+++ b/src/HOL/Analysis/Sigma_Algebra.thy Tue Jan 22 12:00:16 2019 +0000
@@ -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 10:50:47 2019 +0000
+++ b/src/HOL/Analysis/Starlike.thy Tue Jan 22 12:00:16 2019 +0000
@@ -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 10:50:47 2019 +0000
+++ b/src/HOL/Analysis/Tagged_Division.thy Tue Jan 22 12:00:16 2019 +0000
@@ -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 10:50:47 2019 +0000
+++ b/src/HOL/Analysis/Topology_Euclidean_Space.thy Tue Jan 22 12:00:16 2019 +0000
@@ -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 10:50:47 2019 +0000
+++ b/src/HOL/Auth/Message.thy Tue Jan 22 12:00:16 2019 +0000
@@ -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 10:50:47 2019 +0000
+++ b/src/HOL/Cardinals/Cardinal_Order_Relation.thy Tue Jan 22 12:00:16 2019 +0000
@@ -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 10:50:47 2019 +0000
+++ b/src/HOL/Cardinals/Ordinal_Arithmetic.thy Tue Jan 22 12:00:16 2019 +0000
@@ -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 10:50:47 2019 +0000
+++ b/src/HOL/Cardinals/Wellorder_Constructions.thy Tue Jan 22 12:00:16 2019 +0000
@@ -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 10:50:47 2019 +0000
+++ b/src/HOL/Cardinals/Wellorder_Extension.thy Tue Jan 22 12:00:16 2019 +0000
@@ -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 10:50:47 2019 +0000
+++ b/src/HOL/Datatype_Examples/Derivation_Trees/Gram_Lang.thy Tue Jan 22 12:00:16 2019 +0000
@@ -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 10:50:47 2019 +0000
+++ b/src/HOL/IMP/Abs_Int2.thy Tue Jan 22 12:00:16 2019 +0000
@@ -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 10:50:47 2019 +0000
+++ b/src/HOL/IMP/Collecting.thy Tue Jan 22 12:00:16 2019 +0000
@@ -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 10:50:47 2019 +0000
+++ b/src/HOL/IMP/Live.thy Tue Jan 22 12:00:16 2019 +0000
@@ -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 10:50:47 2019 +0000
+++ b/src/HOL/IMP/Live_True.thy Tue Jan 22 12:00:16 2019 +0000
@@ -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 10:50:47 2019 +0000
+++ b/src/HOL/Library/Countable_Set_Type.thy Tue Jan 22 12:00:16 2019 +0000
@@ -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 10:50:47 2019 +0000
+++ b/src/HOL/Library/Disjoint_Sets.thy Tue Jan 22 12:00:16 2019 +0000
@@ -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 10:50:47 2019 +0000
+++ b/src/HOL/Library/FSet.thy Tue Jan 22 12:00:16 2019 +0000
@@ -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/Metis_Examples/Abstraction.thy Tue Jan 22 10:50:47 2019 +0000
+++ b/src/HOL/Metis_Examples/Abstraction.thy Tue Jan 22 12:00:16 2019 +0000
@@ -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 10:50:47 2019 +0000
+++ b/src/HOL/Metis_Examples/Big_O.thy Tue Jan 22 12:00:16 2019 +0000
@@ -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 10:50:47 2019 +0000
+++ b/src/HOL/Metis_Examples/Message.thy Tue Jan 22 12:00:16 2019 +0000
@@ -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 10:50:47 2019 +0000
+++ b/src/HOL/Probability/Conditional_Expectation.thy Tue Jan 22 12:00:16 2019 +0000
@@ -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 10:50:47 2019 +0000
+++ b/src/HOL/Probability/Fin_Map.thy Tue Jan 22 12:00:16 2019 +0000
@@ -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 10:50:47 2019 +0000
+++ b/src/HOL/Probability/Projective_Limit.thy Tue Jan 22 12:00:16 2019 +0000
@@ -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/Set.thy Tue Jan 22 10:50:47 2019 +0000
+++ b/src/HOL/Set.thy Tue Jan 22 12:00:16 2019 +0000
@@ -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 10:50:47 2019 +0000
+++ b/src/HOL/Types_To_Sets/Examples/Linear_Algebra_On_With.thy Tue Jan 22 12:00:16 2019 +0000
@@ -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 10:50:47 2019 +0000
+++ b/src/HOL/Vector_Spaces.thy Tue Jan 22 12:00:16 2019 +0000
@@ -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: