renamings and new material
authorpaulson <lp15@cam.ac.uk>
Tue Jan 22 12:00:16 2019 +0000 (4 months ago)
changeset 69712dc85b5b3a532
parent 69711 82a604715919
child 69714 b7e708ba7786
renamings and new material
src/HOL/Algebra/Complete_Lattice.thy
src/HOL/Algebra/Group_Action.thy
src/HOL/Algebra/Ideal.thy
src/HOL/Algebra/Polynomials.thy
src/HOL/Analysis/Abstract_Topology.thy
src/HOL/Analysis/Brouwer_Fixpoint.thy
src/HOL/Analysis/Caratheodory.thy
src/HOL/Analysis/Cauchy_Integral_Theorem.thy
src/HOL/Analysis/Conformal_Mappings.thy
src/HOL/Analysis/Derivative.thy
src/HOL/Analysis/Elementary_Metric_Spaces.thy
src/HOL/Analysis/Elementary_Normed_Spaces.thy
src/HOL/Analysis/Elementary_Topology.thy
src/HOL/Analysis/Further_Topology.thy
src/HOL/Analysis/Homotopy.thy
src/HOL/Analysis/Lebesgue_Integral_Substitution.thy
src/HOL/Analysis/Path_Connected.thy
src/HOL/Analysis/Sigma_Algebra.thy
src/HOL/Analysis/Starlike.thy
src/HOL/Analysis/Tagged_Division.thy
src/HOL/Analysis/Topology_Euclidean_Space.thy
src/HOL/Auth/Message.thy
src/HOL/Cardinals/Cardinal_Order_Relation.thy
src/HOL/Cardinals/Ordinal_Arithmetic.thy
src/HOL/Cardinals/Wellorder_Constructions.thy
src/HOL/Cardinals/Wellorder_Extension.thy
src/HOL/Datatype_Examples/Derivation_Trees/Gram_Lang.thy
src/HOL/IMP/Abs_Int2.thy
src/HOL/IMP/Collecting.thy
src/HOL/IMP/Live.thy
src/HOL/IMP/Live_True.thy
src/HOL/Library/Countable_Set_Type.thy
src/HOL/Library/Disjoint_Sets.thy
src/HOL/Library/FSet.thy
src/HOL/Metis_Examples/Abstraction.thy
src/HOL/Metis_Examples/Big_O.thy
src/HOL/Metis_Examples/Message.thy
src/HOL/Probability/Conditional_Expectation.thy
src/HOL/Probability/Fin_Map.thy
src/HOL/Probability/Projective_Limit.thy
src/HOL/Set.thy
src/HOL/Types_To_Sets/Examples/Linear_Algebra_On_With.thy
src/HOL/Vector_Spaces.thy
     1.1 --- a/src/HOL/Algebra/Complete_Lattice.thy	Tue Jan 22 10:50:47 2019 +0000
     1.2 +++ b/src/HOL/Algebra/Complete_Lattice.thy	Tue Jan 22 12:00:16 2019 +0000
     1.3 @@ -127,7 +127,7 @@
     1.4    have "least L b (Upper L A)"
     1.5    proof (rule least_UpperI)
     1.6      show "\<And>x. x \<in> A \<Longrightarrow> x \<sqsubseteq> b"
     1.7 -      by (meson L Lower_memI Upper_memD b_inf_B greatest_le set_mp)
     1.8 +      by (meson L Lower_memI Upper_memD b_inf_B greatest_le subsetD)
     1.9      show "\<And>y. y \<in> Upper L A \<Longrightarrow> b \<sqsubseteq> y"
    1.10        by (meson B_L b_inf_B greatest_Lower_below)
    1.11    qed (use bcarr L in auto)
    1.12 @@ -589,7 +589,7 @@
    1.13    have "least L b (Upper L A)"
    1.14    proof (rule least_UpperI)
    1.15      show "\<And>x. x \<in> A \<Longrightarrow> x \<sqsubseteq> b"
    1.16 -      by (meson L Lower_memI Upper_memD b_inf_B greatest_le set_rev_mp)
    1.17 +      by (meson L Lower_memI Upper_memD b_inf_B greatest_le rev_subsetD)
    1.18      show "\<And>y. y \<in> Upper L A \<Longrightarrow> b \<sqsubseteq> y"
    1.19        by (auto elim: greatest_Lower_below [OF b_inf_B])
    1.20    qed (use L bcarr in auto)
    1.21 @@ -692,7 +692,7 @@
    1.22            show 1: "\<Squnion>\<^bsub>L\<^esub>A \<in> carrier L"
    1.23              by (meson L.at_least_at_most_closed L.sup_closed subset_trans *)
    1.24            show "a \<sqsubseteq>\<^bsub>L\<^esub> \<Squnion>\<^bsub>L\<^esub>A"
    1.25 -            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)
    1.26 +            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)
    1.27            show "\<Squnion>\<^bsub>L\<^esub>A \<sqsubseteq>\<^bsub>L\<^esub> b"
    1.28            proof (rule L.sup_least)
    1.29              show "A \<subseteq> carrier L" "\<And>x. x \<in> A \<Longrightarrow> x \<sqsubseteq>\<^bsub>L\<^esub> b"
    1.30 @@ -723,7 +723,7 @@
    1.31            show "a \<sqsubseteq>\<^bsub>L\<^esub> \<Sqinter>\<^bsub>L\<^esub>A"
    1.32              by (meson "*" L.at_least_at_most_closed L.at_least_at_most_lower L.inf_greatest assms(2) subsetD subset_trans)
    1.33            show "\<Sqinter>\<^bsub>L\<^esub>A \<sqsubseteq>\<^bsub>L\<^esub> b"
    1.34 -            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)
    1.35 +            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)
    1.36          qed
    1.37        qed
    1.38      qed
    1.39 @@ -814,7 +814,7 @@
    1.40          have "LFP\<^bsub>?L'\<^esub> f \<sqsubseteq>\<^bsub>?L'\<^esub> x"
    1.41          proof (rule L'.LFP_lowerbound, simp_all)
    1.42            show "x \<in> \<lbrace>\<Squnion>\<^bsub>L\<^esub>A..\<top>\<^bsub>L\<^esub>\<rbrace>\<^bsub>L\<^esub>"
    1.43 -            using x by (auto simp add: Upper_def A AL L.at_least_at_most_member L.sup_least set_rev_mp)    
    1.44 +            using x by (auto simp add: Upper_def A AL L.at_least_at_most_member L.sup_least rev_subsetD)    
    1.45            with x show "f x \<sqsubseteq>\<^bsub>L\<^esub> x"
    1.46              by (simp add: Upper_def) (meson L.at_least_at_most_closed L.use_fps L.weak_refl subsetD f_top_chain imageI)
    1.47          qed
    1.48 @@ -884,7 +884,7 @@
    1.49              moreover have "\<Sqinter>\<^bsub>L\<^esub>A \<sqsubseteq>\<^bsub>L\<^esub> y"
    1.50                by (simp add: AL L.inf_lower c)
    1.51              ultimately show "f (\<Sqinter>\<^bsub>L\<^esub>A) \<sqsubseteq>\<^bsub>L\<^esub> y"
    1.52 -              by (meson AL L.inf_closed L.le_trans c pf_w set_rev_mp w)
    1.53 +              by (meson AL L.inf_closed L.le_trans c pf_w rev_subsetD w)
    1.54            qed
    1.55            thus ?thesis
    1.56              by (meson AL L.inf_closed L.le_trans assms(3) b(1) b(2) fx use_iso2 w)
     2.1 --- a/src/HOL/Algebra/Group_Action.thy	Tue Jan 22 10:50:47 2019 +0000
     2.2 +++ b/src/HOL/Algebra/Group_Action.thy	Tue Jan 22 12:00:16 2019 +0000
     2.3 @@ -902,7 +902,7 @@
     2.4    hence "\<phi>: H \<rightarrow> carrier (BijGroup E)"
     2.5      by (simp add: BijGroup_def bij_prop0 subset_eq)
     2.6    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)"
     2.7 -    by (simp add: S0  group_hom group_hom.hom_mult set_rev_mp)
     2.8 +    by (simp add: S0  group_hom group_hom.hom_mult rev_subsetD)
     2.9  qed
    2.10  
    2.11  theorem (in group_action) induced_action:
     3.1 --- a/src/HOL/Algebra/Ideal.thy	Tue Jan 22 10:50:47 2019 +0000
     3.2 +++ b/src/HOL/Algebra/Ideal.thy	Tue Jan 22 12:00:16 2019 +0000
     3.3 @@ -481,7 +481,7 @@
     3.4    qed
     3.5  next
     3.6    show "I <+> J \<subseteq> Idl (I \<union> J)"
     3.7 -    by (auto simp: set_add_defs genideal_def additive_subgroup.a_closed ideal_def set_mp)
     3.8 +    by (auto simp: set_add_defs genideal_def additive_subgroup.a_closed ideal_def subsetD)
     3.9  qed
    3.10  
    3.11  subsection \<open>Properties of Principal Ideals\<close>
     4.1 --- a/src/HOL/Algebra/Polynomials.thy	Tue Jan 22 10:50:47 2019 +0000
     4.2 +++ b/src/HOL/Algebra/Polynomials.thy	Tue Jan 22 12:00:16 2019 +0000
     4.3 @@ -413,7 +413,7 @@
     4.4          using A(2-3) subringE(2)[OF K] by auto
     4.5        hence "set (map2 (\<oplus>) p1 p2') \<subseteq> K"
     4.6          using A(1) subringE(7)[OF K]
     4.7 -        by (induct p1) (auto, metis set_ConsD set_mp set_zip_leftD set_zip_rightD)
     4.8 +        by (induct p1) (auto, metis set_ConsD subsetD set_zip_leftD set_zip_rightD)
     4.9        thus ?thesis
    4.10          unfolding p2'_def using normalize_gives_polynomial A(3) by simp
    4.11      qed }
     5.1 --- a/src/HOL/Analysis/Abstract_Topology.thy	Tue Jan 22 10:50:47 2019 +0000
     5.2 +++ b/src/HOL/Analysis/Abstract_Topology.thy	Tue Jan 22 12:00:16 2019 +0000
     5.3 @@ -665,6 +665,13 @@
     5.4     "S \<inter> X derived_set_of S = {} \<Longrightarrow> subtopology X S = discrete_topology(topspace X \<inter> S)"
     5.5    by (metis Int_lower1 derived_set_of_restrict inf_assoc inf_bot_right subtopology_eq_discrete_topology_eq subtopology_subtopology subtopology_topspace)
     5.6  
     5.7 +lemma subtopology_discrete_topology [simp]: "subtopology (discrete_topology U) S = discrete_topology(U \<inter> S)"
     5.8 +proof -
     5.9 +  have "(\<lambda>T. \<exists>Sa. T = Sa \<inter> S \<and> Sa \<subseteq> U) = (\<lambda>Sa. Sa \<subseteq> U \<and> Sa \<subseteq> S)"
    5.10 +    by force
    5.11 +  then show ?thesis
    5.12 +    by (simp add: subtopology_def) (simp add: discrete_topology_def)
    5.13 +qed
    5.14  lemma openin_Int_derived_set_of_subset:
    5.15     "openin X S \<Longrightarrow> S \<inter> X derived_set_of T \<subseteq> X derived_set_of (S \<inter> T)"
    5.16    by (auto simp: derived_set_of_def)
     6.1 --- a/src/HOL/Analysis/Brouwer_Fixpoint.thy	Tue Jan 22 10:50:47 2019 +0000
     6.2 +++ b/src/HOL/Analysis/Brouwer_Fixpoint.thy	Tue Jan 22 12:00:16 2019 +0000
     6.3 @@ -3720,7 +3720,7 @@
     6.4            by (auto simp: algebra_simps)
     6.5          have "x \<in> T" "x \<noteq> a" using that by auto
     6.6          then have axa: "a + (x - a) \<in> affine hull S"
     6.7 -           by (metis (no_types) add.commute affS diff_add_cancel set_rev_mp)
     6.8 +           by (metis (no_types) add.commute affS diff_add_cancel rev_subsetD)
     6.9          then have "\<not> dd (x - a) \<le> 0 \<and> a + dd (x - a) *\<^sub>R (x - a) \<in> rel_frontier S"
    6.10            using \<open>x \<noteq> a\<close> dd1 by fastforce
    6.11          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"
     7.1 --- a/src/HOL/Analysis/Caratheodory.thy	Tue Jan 22 10:50:47 2019 +0000
     7.2 +++ b/src/HOL/Analysis/Caratheodory.thy	Tue Jan 22 12:00:16 2019 +0000
     7.3 @@ -139,7 +139,7 @@
     7.4  lemma (in algebra) lambda_system_algebra:
     7.5    "positive M f \<Longrightarrow> algebra \<Omega> (lambda_system \<Omega> M f)"
     7.6    apply (auto simp add: algebra_iff_Un)
     7.7 -  apply (metis lambda_system_sets set_mp sets_into_space)
     7.8 +  apply (metis lambda_system_sets subsetD sets_into_space)
     7.9    apply (metis lambda_system_empty)
    7.10    apply (metis lambda_system_Compl)
    7.11    apply (metis lambda_system_Un)
     8.1 --- a/src/HOL/Analysis/Cauchy_Integral_Theorem.thy	Tue Jan 22 10:50:47 2019 +0000
     8.2 +++ b/src/HOL/Analysis/Cauchy_Integral_Theorem.thy	Tue Jan 22 12:00:16 2019 +0000
     8.3 @@ -3068,7 +3068,7 @@
     8.4      then have contfb: "continuous_on (ball z d) f"
     8.5        using contf continuous_on_subset by blast
     8.6      obtain h where "\<forall>y\<in>ball z d. (h has_field_derivative f y) (at y within ball z d)"
     8.7 -      by (metis holomorphic_convex_primitive [OF convex_ball k contfb fcd] d interior_subset Diff_iff set_mp)
     8.8 +      by (metis holomorphic_convex_primitive [OF convex_ball k contfb fcd] d interior_subset Diff_iff subsetD)
     8.9      then have "\<forall>y\<in>ball z d. (h has_field_derivative f y) (at y within s)"
    8.10        by (metis open_ball at_within_open d os subsetCE)
    8.11      then have "\<exists>h. (\<forall>y. cmod (y - z) < d \<longrightarrow> (h has_field_derivative f y) (at y within s))"
     9.1 --- a/src/HOL/Analysis/Conformal_Mappings.thy	Tue Jan 22 10:50:47 2019 +0000
     9.2 +++ b/src/HOL/Analysis/Conformal_Mappings.thy	Tue Jan 22 12:00:16 2019 +0000
     9.3 @@ -2849,7 +2849,7 @@
     9.4          using "2.prems"(8) that
     9.5          apply blast
     9.6          apply (metis Diff_iff Diff_insert2 contra_subsetD pg(4) that)
     9.7 -        by (meson DiffD2 cp(4) set_rev_mp subset_insertI that)
     9.8 +        by (meson DiffD2 cp(4) rev_subsetD subset_insertI that)
     9.9        have "winding_number g' p' = winding_number g p'
    9.10            + winding_number (pg +++ cp +++ reversepath pg) p'" unfolding g'_def
    9.11          apply (subst winding_number_join)
    10.1 --- a/src/HOL/Analysis/Derivative.thy	Tue Jan 22 10:50:47 2019 +0000
    10.2 +++ b/src/HOL/Analysis/Derivative.thy	Tue Jan 22 12:00:16 2019 +0000
    10.3 @@ -1400,7 +1400,7 @@
    10.4      apply auto
    10.5      done
    10.6    moreover have "f (g y) = y" if "y \<in> interior (f ` S)" for y
    10.7 -    by (metis gf imageE interiorE set_mp that)
    10.8 +    by (metis gf imageE interiorE subsetD that)
    10.9    ultimately show ?thesis using assms
   10.10      by (metis has_derivative_inverse_basic_x open_interior)
   10.11  qed
   10.12 @@ -2740,7 +2740,7 @@
   10.13      using f' g' closure_subset[of T] closure_subset[of S]
   10.14      unfolding has_derivative_within_If_eq
   10.15      by (intro conjI bl tendsto_If_within_closures x_in)
   10.16 -      (auto simp: has_derivative_within inverse_eq_divide connect connect' set_mp)
   10.17 +      (auto simp: has_derivative_within inverse_eq_divide connect connect' subsetD)
   10.18  qed
   10.19  
   10.20  lemma has_vector_derivative_If_within_closures:
    11.1 --- a/src/HOL/Analysis/Elementary_Metric_Spaces.thy	Tue Jan 22 10:50:47 2019 +0000
    11.2 +++ b/src/HOL/Analysis/Elementary_Metric_Spaces.thy	Tue Jan 22 12:00:16 2019 +0000
    11.3 @@ -2696,7 +2696,7 @@
    11.4          by (auto simp: closure_sequential)
    11.5        from continuous_on_tendsto_compose[OF cont_h xs(1)] xs(2) Y
    11.6        have hx: "(\<lambda>x. f (xs x)) \<longlonglongrightarrow> h x"
    11.7 -        by (auto simp: set_mp extension)
    11.8 +        by (auto simp: subsetD extension)
    11.9        then have "(\<lambda>x. f (xs x)) \<longlonglongrightarrow> y x"
   11.10          using \<open>x \<notin> X\<close> not_eventuallyD xs(2)
   11.11          by (force intro!: filterlim_compose[OF y[OF \<open>x \<in> closure X\<close>]] simp: filterlim_at xs)
    12.1 --- a/src/HOL/Analysis/Elementary_Normed_Spaces.thy	Tue Jan 22 10:50:47 2019 +0000
    12.2 +++ b/src/HOL/Analysis/Elementary_Normed_Spaces.thy	Tue Jan 22 12:00:16 2019 +0000
    12.3 @@ -1009,7 +1009,7 @@
    12.4        fix y
    12.5        assume "y \<in> S" and y: "\<forall>n. y \<in> closure (TF n)"
    12.6        then show "\<forall>T\<in>\<G>. y \<in> T"
    12.7 -        by (metis Int_iff from_nat_into_surj [OF \<open>countable \<G>\<close>] set_mp subg)
    12.8 +        by (metis Int_iff from_nat_into_surj [OF \<open>countable \<G>\<close>] subsetD subg)
    12.9        show "dist y x < e"
   12.10          by (metis y dist_commute mem_ball subball subsetCE)
   12.11      qed
    13.1 --- a/src/HOL/Analysis/Elementary_Topology.thy	Tue Jan 22 10:50:47 2019 +0000
    13.2 +++ b/src/HOL/Analysis/Elementary_Topology.thy	Tue Jan 22 12:00:16 2019 +0000
    13.3 @@ -1763,7 +1763,7 @@
    13.4      by auto
    13.5    moreover
    13.6    have ev_Z: "\<And>z. z \<in> Z \<Longrightarrow> eventually (\<lambda>x. x \<in> z) F"
    13.7 -    unfolding Z_def by (auto elim: eventually_mono intro: set_mp[OF closure_subset])
    13.8 +    unfolding Z_def by (auto elim: eventually_mono intro: subsetD[OF closure_subset])
    13.9    have "(\<forall>B \<subseteq> Z. finite B \<longrightarrow> U \<inter> \<Inter>B \<noteq> {})"
   13.10    proof (intro allI impI)
   13.11      fix B assume "finite B" "B \<subseteq> Z"
    14.1 --- a/src/HOL/Analysis/Further_Topology.thy	Tue Jan 22 10:50:47 2019 +0000
    14.2 +++ b/src/HOL/Analysis/Further_Topology.thy	Tue Jan 22 12:00:16 2019 +0000
    14.3 @@ -4738,7 +4738,7 @@
    14.4        fix T
    14.5        assume "connected T" and TB: "T \<subseteq> - frontier B" and "a \<in> T" and "b \<in> T"
    14.6        have "a \<notin> B"
    14.7 -        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)
    14.8 +        by (metis A_def B_def ComplD \<open>a \<in> A\<close> assms(1) closed_open connected_component_subset in_closure_connected_component subsetD)
    14.9        have "T \<inter> B \<noteq> {}"
   14.10          using \<open>b \<in> B\<close> \<open>b \<in> T\<close> by blast
   14.11        moreover have "T - B \<noteq> {}"
    15.1 --- a/src/HOL/Analysis/Homotopy.thy	Tue Jan 22 10:50:47 2019 +0000
    15.2 +++ b/src/HOL/Analysis/Homotopy.thy	Tue Jan 22 12:00:16 2019 +0000
    15.3 @@ -2470,7 +2470,7 @@
    15.4      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"
    15.5        using 1 \<open>y \<in> t\<close> by presburger
    15.6      have "G y t \<subseteq> path_component_set t y"
    15.7 -      using * path_component_maximal set_rev_mp by blast
    15.8 +      using * path_component_maximal rev_subsetD by blast
    15.9      then have "\<exists>A. openin ?SS A \<and> y \<in> A \<and> A \<subseteq> path_component_set t x"
   15.10        by (metis "*" \<open>G y t \<subseteq> path_component_set t y\<close> dual_order.trans path_component_eq y)
   15.11    }
    16.1 --- a/src/HOL/Analysis/Lebesgue_Integral_Substitution.thy	Tue Jan 22 10:50:47 2019 +0000
    16.2 +++ b/src/HOL/Analysis/Lebesgue_Integral_Substitution.thy	Tue Jan 22 12:00:16 2019 +0000
    16.3 @@ -69,7 +69,7 @@
    16.4              by (simp only: u'v' max_absorb2 min_absorb1)
    16.5                 (intro continuous_on_subset[OF contg'], insert u'v', auto)
    16.6          have "\<And>x. x \<in> {u'..v'} \<Longrightarrow> (g has_real_derivative g' x) (at x within {u'..v'})"
    16.7 -           using asm by (intro has_field_derivative_subset[OF derivg] set_mp[OF \<open>{u'..v'} \<subseteq> {a..b}\<close>]) auto
    16.8 +           using asm by (intro has_field_derivative_subset[OF derivg] subsetD[OF \<open>{u'..v'} \<subseteq> {a..b}\<close>]) auto
    16.9          hence B: "\<And>x. min u' v' \<le> x \<Longrightarrow> x \<le> max u' v' \<Longrightarrow>
   16.10                        (g has_vector_derivative g' x) (at x within {min u' v'..max u' v'})"
   16.11              by (simp only: u'v' max_absorb2 min_absorb1)
    17.1 --- a/src/HOL/Analysis/Path_Connected.thy	Tue Jan 22 10:50:47 2019 +0000
    17.2 +++ b/src/HOL/Analysis/Path_Connected.thy	Tue Jan 22 12:00:16 2019 +0000
    17.3 @@ -2851,7 +2851,7 @@
    17.4         and cc: "connected_component (- frontier s) x y"
    17.5      have "connected_component_set (- frontier s) x \<inter> frontier s \<noteq> {}"
    17.6        apply (rule connected_Int_frontier, simp)
    17.7 -      apply (metis IntI cc connected_component_in connected_component_refl empty_iff interiorE mem_Collect_eq set_rev_mp x)
    17.8 +      apply (metis IntI cc connected_component_in connected_component_refl empty_iff interiorE mem_Collect_eq rev_subsetD x)
    17.9        using  y cc
   17.10        by blast
   17.11      then have "bounded (connected_component_set (- frontier s) x)"
    18.1 --- a/src/HOL/Analysis/Sigma_Algebra.thy	Tue Jan 22 10:50:47 2019 +0000
    18.2 +++ b/src/HOL/Analysis/Sigma_Algebra.thy	Tue Jan 22 12:00:16 2019 +0000
    18.3 @@ -275,7 +275,7 @@
    18.4    hence "\<Union>X = (\<Union>n. from_nat_into X n)"
    18.5      using assms by (auto cong del: SUP_cong)
    18.6    also have "\<dots> \<in> M" using assms
    18.7 -    by (auto intro!: countable_nat_UN) (metis \<open>X \<noteq> {}\<close> from_nat_into set_mp)
    18.8 +    by (auto intro!: countable_nat_UN) (metis \<open>X \<noteq> {}\<close> from_nat_into subsetD)
    18.9    finally show ?thesis .
   18.10  qed simp
   18.11  
    19.1 --- a/src/HOL/Analysis/Starlike.thy	Tue Jan 22 10:50:47 2019 +0000
    19.2 +++ b/src/HOL/Analysis/Starlike.thy	Tue Jan 22 12:00:16 2019 +0000
    19.3 @@ -1588,7 +1588,7 @@
    19.4        apply (rule sum.cong)
    19.5        using \<open>i \<in> D\<close> \<open>finite D\<close> sum.delta'[of D i "(\<lambda>k. inverse (2 * real (card D)))"]
    19.6          d1 assms(2)
    19.7 -      by (auto simp: inner_Basis set_rev_mp[OF _ assms(2)])
    19.8 +      by (auto simp: inner_Basis rev_subsetD[OF _ assms(2)])
    19.9    }
   19.10    note ** = this
   19.11    show ?thesis
    20.1 --- a/src/HOL/Analysis/Tagged_Division.thy	Tue Jan 22 10:50:47 2019 +0000
    20.2 +++ b/src/HOL/Analysis/Tagged_Division.thy	Tue Jan 22 12:00:16 2019 +0000
    20.3 @@ -914,7 +914,7 @@
    20.4        have "interior m \<inter> interior (\<Union>p) = {}"
    20.5        proof (rule Int_interior_Union_intervals)
    20.6          show "\<And>T. T\<in>p \<Longrightarrow> interior m \<inter> interior T = {}"
    20.7 -          by (metis DiffD1 DiffD2 that r1(1) r1(7) set_rev_mp)
    20.8 +          by (metis DiffD1 DiffD2 that r1(1) r1(7) rev_subsetD)
    20.9        qed (use divp in auto)
   20.10        then show "interior S \<inter> interior m = {}"
   20.11          unfolding divp by auto
    21.1 --- a/src/HOL/Analysis/Topology_Euclidean_Space.thy	Tue Jan 22 10:50:47 2019 +0000
    21.2 +++ b/src/HOL/Analysis/Topology_Euclidean_Space.thy	Tue Jan 22 12:00:16 2019 +0000
    21.3 @@ -154,7 +154,7 @@
    21.4    proof
    21.5      assume ?lhs
    21.6      then have "0 < r'"
    21.7 -      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)
    21.8 +      by (metis (no_types) False \<open>?lhs\<close> centre_in_ball dist_norm le_less_trans mem_ball norm_ge_zero not_less subsetD)
    21.9      then have "(cball a r \<subseteq> cball a' r')"
   21.10        by (metis False\<open>?lhs\<close> closure_ball closure_mono not_less)
   21.11      then show ?rhs
    22.1 --- a/src/HOL/Auth/Message.thy	Tue Jan 22 10:50:47 2019 +0000
    22.2 +++ b/src/HOL/Auth/Message.thy	Tue Jan 22 12:00:16 2019 +0000
    22.3 @@ -243,7 +243,7 @@
    22.4  by (metis parts_idem parts_increasing parts_mono subset_trans)
    22.5  
    22.6  lemma parts_trans: "[| X\<in> parts G;  G \<subseteq> parts H |] ==> X\<in> parts H"
    22.7 -by (metis parts_subset_iff set_mp)
    22.8 +by (metis parts_subset_iff subsetD)
    22.9  
   22.10  text\<open>Cut\<close>
   22.11  lemma parts_cut:
   22.12 @@ -672,7 +672,7 @@
   22.13  lemma Fake_parts_insert_in_Un:
   22.14       "\<lbrakk>Z \<in> parts (insert X H);  X \<in> synth (analz H)\<rbrakk> 
   22.15        \<Longrightarrow> Z \<in> synth (analz H) \<union> parts H"
   22.16 -by (metis Fake_parts_insert set_mp)
   22.17 +by (metis Fake_parts_insert subsetD)
   22.18  
   22.19  text\<open>\<^term>\<open>H\<close> is sometimes \<^term>\<open>Key ` KK \<union> spies evs\<close>, so can't put 
   22.20    \<^term>\<open>G=H\<close>.\<close>
    23.1 --- a/src/HOL/Cardinals/Cardinal_Order_Relation.thy	Tue Jan 22 10:50:47 2019 +0000
    23.2 +++ b/src/HOL/Cardinals/Cardinal_Order_Relation.thy	Tue Jan 22 12:00:16 2019 +0000
    23.3 @@ -1643,7 +1643,7 @@
    23.4    unfolding wo_rel_def by (metis card_order_on_well_order_on cr)+
    23.5    have L: "isLimOrd r" using ir cr by (metis card_order_infinite_isLimOrd)
    23.6    have AsBs: "(\<Union>i \<in> Field r. As (succ r i)) \<subseteq> B"
    23.7 -  using AsB L apply safe by (metis "0" UN_I set_mp wo_rel.isLimOrd_succ)
    23.8 +  using AsB L apply safe by (metis "0" UN_I subsetD wo_rel.isLimOrd_succ)
    23.9    assume As_s: "\<forall>i\<in>Field r. As (succ r i) \<noteq> As i"
   23.10    have 1: "\<forall>i j. (i,j) \<in> r \<and> i \<noteq> j \<longrightarrow> As i \<subset> As j"
   23.11    proof safe
    24.1 --- a/src/HOL/Cardinals/Ordinal_Arithmetic.thy	Tue Jan 22 10:50:47 2019 +0000
    24.2 +++ b/src/HOL/Cardinals/Ordinal_Arithmetic.thy	Tue Jan 22 12:00:16 2019 +0000
    24.3 @@ -814,7 +814,7 @@
    24.4              with x0notzero zField have SUPP: "SUPP f0 = SUPP g0 \<union> {z}" unfolding support_def by auto
    24.5              from g0z have f0z: "f0(z := r.zero) = g0" unfolding f0_def fun_upd_upd by auto
    24.6              have f0: "f0 \<in> F" using x0min g0(1)
    24.7 -              Func_elim[OF set_mp[OF subset_trans[OF F(1)[unfolded FinFunc_def] Int_lower1]] zField]
    24.8 +              Func_elim[OF subsetD[OF subset_trans[OF F(1)[unfolded FinFunc_def] Int_lower1]] zField]
    24.9                unfolding f0_def r.isMinim_def G_def by (force simp: fun_upd_idem)
   24.10              from g0(1) maxF(1) have maxf0: "s.maxim (SUPP f0) = z" unfolding SUPP G_def
   24.11                by (intro s.maxim_equality) (auto simp: s.isMaxim_def)
   24.12 @@ -1409,7 +1409,7 @@
   24.13        from f \<open>t \<noteq> {}\<close> False have *: "Field r \<noteq> {}" "Field s \<noteq> {}" "Field t \<noteq> {}"
   24.14          unfolding Field_def embed_def under_def bij_betw_def by auto
   24.15        with f obtain x where "s.zero = f x" "x \<in> Field r" unfolding embed_def bij_betw_def
   24.16 -        using embed_in_Field[OF r.WELL f] s.zero_under set_mp[OF under_Field[of r]] by blast
   24.17 +        using embed_in_Field[OF r.WELL f] s.zero_under subsetD[OF under_Field[of r]] by blast
   24.18        with f have fz: "f r.zero = s.zero" and inj: "inj_on f (Field r)" and compat: "compat r s f"
   24.19          unfolding embed_iff_compat_inj_on_ofilter[OF r s] compat_def
   24.20          by (fastforce intro: s.leq_zero_imp)+
    25.1 --- a/src/HOL/Cardinals/Wellorder_Constructions.thy	Tue Jan 22 10:50:47 2019 +0000
    25.2 +++ b/src/HOL/Cardinals/Wellorder_Constructions.thy	Tue Jan 22 12:00:16 2019 +0000
    25.3 @@ -481,7 +481,7 @@
    25.4    have bb: "b \<in> Field r" using bA unfolding underS_def Field_def by auto
    25.5    assume "\<forall>a\<in>A.  b \<notin> under a"
    25.6    hence 0: "\<forall>a \<in> A. a \<in> underS b" using A bA unfolding underS_def
    25.7 -  by simp (metis (lifting) bb max2_def max2_greater mem_Collect_eq under_def set_rev_mp)
    25.8 +  by simp (metis (lifting) bb max2_def max2_greater mem_Collect_eq under_def rev_subsetD)
    25.9    have "(suc A, b) \<in> r" apply(rule suc_least[OF A bb]) using 0 unfolding underS_def by auto
   25.10    thus False using bA unfolding underS_def by simp (metis ANTISYM antisymD)
   25.11  qed
    26.1 --- a/src/HOL/Cardinals/Wellorder_Extension.thy	Tue Jan 22 10:50:47 2019 +0000
    26.2 +++ b/src/HOL/Cardinals/Wellorder_Extension.thy	Tue Jan 22 12:00:16 2019 +0000
    26.3 @@ -52,7 +52,7 @@
    26.4    shows "extension_on (Field (\<Union>R)) (\<Union>R) p"
    26.5    using assms
    26.6    by (simp add: chain_subset_def extension_on_def)
    26.7 -     (metis (no_types) mono_Field set_mp)
    26.8 +     (metis (no_types) mono_Field subsetD)
    26.9  
   26.10  lemma downset_on_empty [simp]: "downset_on {} p"
   26.11    by (auto simp: downset_on_def)
    27.1 --- a/src/HOL/Datatype_Examples/Derivation_Trees/Gram_Lang.thy	Tue Jan 22 10:50:47 2019 +0000
    27.2 +++ b/src/HOL/Datatype_Examples/Derivation_Trees/Gram_Lang.thy	Tue Jan 22 12:00:16 2019 +0000
    27.3 @@ -40,7 +40,7 @@
    27.4  assumes "inFr ns tr t" and "ns \<subseteq> ns'"
    27.5  shows "inFr ns' tr t"
    27.6  using assms apply(induct arbitrary: ns' rule: inFr.induct)
    27.7 -using Base Ind by (metis inFr.simps set_mp)+
    27.8 +using Base Ind by (metis inFr.simps subsetD)+
    27.9  
   27.10  lemma inFr_Ind_minus:
   27.11  assumes "inFr ns1 tr1 t" and "Inr tr1 \<in> cont tr"
   27.12 @@ -111,7 +111,7 @@
   27.13  assumes "inItr ns tr n" and "ns \<subseteq> ns'"
   27.14  shows "inItr ns' tr n"
   27.15  using assms apply(induct arbitrary: ns' rule: inItr.induct)
   27.16 -using Base Ind by (metis inItr.simps set_mp)+
   27.17 +using Base Ind by (metis inItr.simps subsetD)+
   27.18  
   27.19  
   27.20  (* The subtree relation *)
   27.21 @@ -137,7 +137,7 @@
   27.22  assumes "subtr ns tr1 tr2" and "ns \<subseteq> ns'"
   27.23  shows "subtr ns' tr1 tr2"
   27.24  using assms apply(induct arbitrary: ns' rule: subtr.induct)
   27.25 -using Refl Step by (metis subtr.simps set_mp)+
   27.26 +using Refl Step by (metis subtr.simps subsetD)+
   27.27  
   27.28  lemma subtr_trans_Un:
   27.29  assumes "subtr ns12 tr1 tr2" and "subtr ns23 tr2 tr3"
   27.30 @@ -188,7 +188,7 @@
   27.31  assumes "subtr2 ns tr1 tr2" and "ns \<subseteq> ns'"
   27.32  shows "subtr2 ns' tr1 tr2"
   27.33  using assms apply(induct arbitrary: ns' rule: subtr2.induct)
   27.34 -using Refl Step by (metis subtr2.simps set_mp)+
   27.35 +using Refl Step by (metis subtr2.simps subsetD)+
   27.36  
   27.37  lemma subtr2_trans_Un:
   27.38  assumes "subtr2 ns12 tr1 tr2" and "subtr2 ns23 tr2 tr3"
    28.1 --- a/src/HOL/IMP/Abs_Int2.thy	Tue Jan 22 10:50:47 2019 +0000
    28.2 +++ b/src/HOL/IMP/Abs_Int2.thy	Tue Jan 22 12:00:16 2019 +0000
    28.3 @@ -38,7 +38,7 @@
    28.4  begin
    28.5  
    28.6  lemma in_gamma_inf: "x \<in> \<gamma> a1 \<Longrightarrow> x \<in> \<gamma> a2 \<Longrightarrow> x \<in> \<gamma>(a1 \<sqinter> a2)"
    28.7 -by (metis IntI inter_gamma_subset_gamma_inf set_mp)
    28.8 +by (metis IntI inter_gamma_subset_gamma_inf subsetD)
    28.9  
   28.10  lemma gamma_inf: "\<gamma>(a1 \<sqinter> a2) = \<gamma> a1 \<inter> \<gamma> a2"
   28.11  by(rule equalityI[OF _ inter_gamma_subset_gamma_inf])
    29.1 --- a/src/HOL/IMP/Collecting.thy	Tue Jan 22 10:50:47 2019 +0000
    29.2 +++ b/src/HOL/IMP/Collecting.thy	Tue Jan 22 12:00:16 2019 +0000
    29.3 @@ -184,10 +184,10 @@
    29.4      by(fastforce simp: strip_eq_Seq step_def post_def last_append annos_ne)
    29.5  next
    29.6    case IfTrue thus ?case apply(auto simp: strip_eq_If step_def post_def)
    29.7 -    by (metis (lifting,full_types) mem_Collect_eq set_mp)
    29.8 +    by (metis (lifting,full_types) mem_Collect_eq subsetD)
    29.9  next
   29.10    case IfFalse thus ?case apply(auto simp: strip_eq_If step_def post_def)
   29.11 -    by (metis (lifting,full_types) mem_Collect_eq set_mp)
   29.12 +    by (metis (lifting,full_types) mem_Collect_eq subsetD)
   29.13  next
   29.14    case (WhileTrue b s1 c' s2 s3)
   29.15    from WhileTrue.prems(1) obtain I P C' Q where "C = {I} WHILE b DO {P} C' {Q}" "strip C' = c'"
    30.1 --- a/src/HOL/IMP/Live.thy	Tue Jan 22 10:50:47 2019 +0000
    30.2 +++ b/src/HOL/IMP/Live.thy	Tue Jan 22 12:00:16 2019 +0000
    30.3 @@ -87,13 +87,13 @@
    30.4  next
    30.5    case (WhileFalse b s c)
    30.6    hence "~ bval b t"
    30.7 -    by (metis L_While_vars bval_eq_if_eq_on_vars set_mp)
    30.8 -  thus ?case by(metis WhileFalse.prems L_While_X big_step.WhileFalse set_mp)
    30.9 +    by (metis L_While_vars bval_eq_if_eq_on_vars subsetD)
   30.10 +  thus ?case by(metis WhileFalse.prems L_While_X big_step.WhileFalse subsetD)
   30.11  next
   30.12    case (WhileTrue b s1 c s2 s3 X t1)
   30.13    let ?w = "WHILE b DO c"
   30.14    from \<open>bval b s1\<close> WhileTrue.prems have "bval b t1"
   30.15 -    by (metis L_While_vars bval_eq_if_eq_on_vars set_mp)
   30.16 +    by (metis L_While_vars bval_eq_if_eq_on_vars subsetD)
   30.17    have "s1 = t1 on L c (L ?w X)" using L_While_pfp WhileTrue.prems
   30.18      by (blast)
   30.19    from WhileTrue.IH(1)[OF this] obtain t2 where
   30.20 @@ -151,14 +151,14 @@
   30.21    thus ?case using \<open>~bval b t\<close> by auto
   30.22  next
   30.23    case (WhileFalse b s c)
   30.24 -  hence "~ bval b t" by (metis L_While_vars bval_eq_if_eq_on_vars set_mp)
   30.25 +  hence "~ bval b t" by (metis L_While_vars bval_eq_if_eq_on_vars subsetD)
   30.26    thus ?case
   30.27 -    by simp (metis L_While_X WhileFalse.prems big_step.WhileFalse set_mp)
   30.28 +    by simp (metis L_While_X WhileFalse.prems big_step.WhileFalse subsetD)
   30.29  next
   30.30    case (WhileTrue b s1 c s2 s3 X t1)
   30.31    let ?w = "WHILE b DO c"
   30.32    from \<open>bval b s1\<close> WhileTrue.prems have "bval b t1"
   30.33 -    by (metis L_While_vars bval_eq_if_eq_on_vars set_mp)
   30.34 +    by (metis L_While_vars bval_eq_if_eq_on_vars subsetD)
   30.35    have "s1 = t1 on L c (L ?w X)"
   30.36      using L_While_pfp WhileTrue.prems by blast
   30.37    from WhileTrue.IH(1)[OF this] obtain t2 where
   30.38 @@ -237,15 +237,15 @@
   30.39  next
   30.40    case (WhileFalse b s c)
   30.41    hence "~ bval b t"
   30.42 -    by auto (metis L_While_vars bval_eq_if_eq_on_vars set_rev_mp)
   30.43 +    by auto (metis L_While_vars bval_eq_if_eq_on_vars rev_subsetD)
   30.44    thus ?case using WhileFalse
   30.45 -    by auto (metis L_While_X big_step.WhileFalse set_mp)
   30.46 +    by auto (metis L_While_X big_step.WhileFalse subsetD)
   30.47  next
   30.48    case (WhileTrue b s1 bc' s2 s3 w X t1)
   30.49    then obtain c' where w: "w = WHILE b DO c'"
   30.50      and bc': "bc' = bury c' (L (WHILE b DO c') X)" by auto
   30.51    from \<open>bval b s1\<close> WhileTrue.prems w have "bval b t1"
   30.52 -    by auto (metis L_While_vars bval_eq_if_eq_on_vars set_mp)
   30.53 +    by auto (metis L_While_vars bval_eq_if_eq_on_vars subsetD)
   30.54    note IH = WhileTrue.hyps(3,5)
   30.55    have "s1 = t1 on L c' (L w X)"
   30.56      using L_While_pfp WhileTrue.prems w by blast
    31.1 --- a/src/HOL/IMP/Live_True.thy	Tue Jan 22 10:50:47 2019 +0000
    31.2 +++ b/src/HOL/IMP/Live_True.thy	Tue Jan 22 12:00:16 2019 +0000
    31.3 @@ -88,13 +88,13 @@
    31.4  next
    31.5    case (WhileFalse b s c)
    31.6    hence "~ bval b t"
    31.7 -    by (metis L_While_vars bval_eq_if_eq_on_vars set_mp)
    31.8 +    by (metis L_While_vars bval_eq_if_eq_on_vars subsetD)
    31.9    thus ?case using WhileFalse.prems L_While_X[of X b c] by auto
   31.10  next
   31.11    case (WhileTrue b s1 c s2 s3 X t1)
   31.12    let ?w = "WHILE b DO c"
   31.13    from \<open>bval b s1\<close> WhileTrue.prems have "bval b t1"
   31.14 -    by (metis L_While_vars bval_eq_if_eq_on_vars set_mp)
   31.15 +    by (metis L_While_vars bval_eq_if_eq_on_vars subsetD)
   31.16    have "s1 = t1 on L c (L ?w X)" using  L_While_pfp WhileTrue.prems
   31.17      by (blast)
   31.18    from WhileTrue.IH(1)[OF this] obtain t2 where
    32.1 --- a/src/HOL/Library/Countable_Set_Type.thy	Tue Jan 22 10:50:47 2019 +0000
    32.2 +++ b/src/HOL/Library/Countable_Set_Type.thy	Tue Jan 22 12:00:16 2019 +0000
    32.3 @@ -150,8 +150,8 @@
    32.4  lemmas contra_csubsetD[no_atp] = contra_subsetD[Transfer.transferred]
    32.5  lemmas csubset_refl = subset_refl[Transfer.transferred]
    32.6  lemmas csubset_trans = subset_trans[Transfer.transferred]
    32.7 -lemmas cset_rev_mp = set_rev_mp[Transfer.transferred]
    32.8 -lemmas cset_mp = set_mp[Transfer.transferred]
    32.9 +lemmas cset_rev_mp = rev_subsetD[Transfer.transferred]
   32.10 +lemmas cset_mp = subsetD[Transfer.transferred]
   32.11  lemmas csubset_not_fsubset_eq[code] = subset_not_subset_eq[Transfer.transferred]
   32.12  lemmas eq_cmem_trans = eq_mem_trans[Transfer.transferred]
   32.13  lemmas csubset_antisym[intro!] = subset_antisym[Transfer.transferred]
    33.1 --- a/src/HOL/Library/Disjoint_Sets.thy	Tue Jan 22 10:50:47 2019 +0000
    33.2 +++ b/src/HOL/Library/Disjoint_Sets.thy	Tue Jan 22 12:00:16 2019 +0000
    33.3 @@ -58,6 +58,49 @@
    33.4      by (auto simp flip: INT_Int_distrib)
    33.5  qed
    33.6  
    33.7 +lemma diff_Union_pairwise_disjoint:
    33.8 +  assumes "pairwise disjnt \<A>" "\<B> \<subseteq> \<A>"
    33.9 +  shows "\<Union>\<A> - \<Union>\<B> = \<Union>(\<A> - \<B>)"
   33.10 +proof -
   33.11 +  have "False"
   33.12 +    if x: "x \<in> A" "x \<in> B" and AB: "A \<in> \<A>" "A \<notin> \<B>" "B \<in> \<B>" for x A B
   33.13 +  proof -
   33.14 +    have "A \<inter> B = {}"
   33.15 +      using assms disjointD AB by blast
   33.16 +  with x show ?thesis
   33.17 +    by blast
   33.18 +  qed
   33.19 +  then show ?thesis by auto
   33.20 +qed
   33.21 +
   33.22 +lemma Int_Union_pairwise_disjoint:
   33.23 +  assumes "pairwise disjnt (\<A> \<union> \<B>)"
   33.24 +  shows "\<Union>\<A> \<inter> \<Union>\<B> = \<Union>(\<A> \<inter> \<B>)"
   33.25 +proof -
   33.26 +  have "False"
   33.27 +    if x: "x \<in> A" "x \<in> B" and AB: "A \<in> \<A>" "A \<notin> \<B>" "B \<in> \<B>" for x A B
   33.28 +  proof -
   33.29 +    have "A \<inter> B = {}"
   33.30 +      using assms disjointD AB by blast
   33.31 +  with x show ?thesis
   33.32 +    by blast
   33.33 +  qed
   33.34 +  then show ?thesis by auto
   33.35 +qed
   33.36 +
   33.37 +lemma psubset_Union_pairwise_disjoint:
   33.38 +  assumes \<B>: "pairwise disjnt \<B>" and "\<A> \<subset> \<B> - {{}}"
   33.39 +  shows "\<Union>\<A> \<subset> \<Union>\<B>"
   33.40 +  unfolding psubset_eq
   33.41 +proof
   33.42 +  show "\<Union>\<A> \<subseteq> \<Union>\<B>"
   33.43 +    using assms by blast
   33.44 +  have "\<A> \<subseteq> \<B>" "\<Union>(\<B> - \<A> \<inter> (\<B> - {{}})) \<noteq> {}"
   33.45 +    using assms by blast+
   33.46 +  then show "\<Union>\<A> \<noteq> \<Union>\<B>"
   33.47 +    using diff_Union_pairwise_disjoint [OF \<B>] by blast
   33.48 +qed
   33.49 +
   33.50  subsubsection "Family of Disjoint Sets"
   33.51  
   33.52  definition disjoint_family_on :: "('i \<Rightarrow> 'a set) \<Rightarrow> 'i set \<Rightarrow> bool" where
    34.1 --- a/src/HOL/Library/FSet.thy	Tue Jan 22 10:50:47 2019 +0000
    34.2 +++ b/src/HOL/Library/FSet.thy	Tue Jan 22 12:00:16 2019 +0000
    34.3 @@ -236,8 +236,8 @@
    34.4  lemmas contra_fsubsetD[no_atp] = contra_subsetD[Transfer.transferred]
    34.5  lemmas fsubset_refl = subset_refl[Transfer.transferred]
    34.6  lemmas fsubset_trans = subset_trans[Transfer.transferred]
    34.7 -lemmas fset_rev_mp = set_rev_mp[Transfer.transferred]
    34.8 -lemmas fset_mp = set_mp[Transfer.transferred]
    34.9 +lemmas fset_rev_mp = rev_subsetD[Transfer.transferred]
   34.10 +lemmas fset_mp = subsetD[Transfer.transferred]
   34.11  lemmas fsubset_not_fsubset_eq[code] = subset_not_subset_eq[Transfer.transferred]
   34.12  lemmas eq_fmem_trans = eq_mem_trans[Transfer.transferred]
   34.13  lemmas fsubset_antisym[intro!] = subset_antisym[Transfer.transferred]
    35.1 --- a/src/HOL/Metis_Examples/Abstraction.thy	Tue Jan 22 10:50:47 2019 +0000
    35.2 +++ b/src/HOL/Metis_Examples/Abstraction.thy	Tue Jan 22 12:00:16 2019 +0000
    35.3 @@ -154,7 +154,7 @@
    35.4  lemma
    35.5    "(\<lambda>x. f (f x)) ` ((\<lambda>x. Suc(f x)) ` {x. even x}) \<subseteq> A \<Longrightarrow>
    35.6     (\<forall>x. even x --> f (f (Suc(f x))) \<in> A)"
    35.7 -by (metis mem_Collect_eq imageI set_rev_mp)
    35.8 +by (metis mem_Collect_eq imageI rev_subsetD)
    35.9  
   35.10  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)"
   35.11  by (metis (lifting) imageE)
    36.1 --- a/src/HOL/Metis_Examples/Big_O.thy	Tue Jan 22 10:50:47 2019 +0000
    36.2 +++ b/src/HOL/Metis_Examples/Big_O.thy	Tue Jan 22 12:00:16 2019 +0000
    36.3 @@ -314,7 +314,7 @@
    36.4  by (metis bigo_mult bigo_refl set_times_mono3 subset_trans)
    36.5  
    36.6  lemma bigo_mult3: "f \<in> O(h) \<Longrightarrow> g \<in> O(j) \<Longrightarrow> f * g \<in> O(h * j)"
    36.7 -by (metis bigo_mult set_rev_mp set_times_intro)
    36.8 +by (metis bigo_mult rev_subsetD set_times_intro)
    36.9  
   36.10  lemma bigo_mult4 [intro]:"f \<in> k +o O(h) \<Longrightarrow> g * f \<in> (g * k) +o O(g * h)"
   36.11  by (metis bigo_mult2 set_plus_mono_b set_times_intro2 set_times_plus_distrib)
    37.1 --- a/src/HOL/Metis_Examples/Message.thy	Tue Jan 22 10:50:47 2019 +0000
    37.2 +++ b/src/HOL/Metis_Examples/Message.thy	Tue Jan 22 12:00:16 2019 +0000
    37.3 @@ -78,7 +78,7 @@
    37.4  lemma parts_mono: "G \<subseteq> H ==> parts(G) \<subseteq> parts(H)"
    37.5  apply auto
    37.6  apply (erule parts.induct)
    37.7 -   apply (metis parts.Inj set_rev_mp)
    37.8 +   apply (metis parts.Inj rev_subsetD)
    37.9    apply (metis parts.Fst)
   37.10   apply (metis parts.Snd)
   37.11  by (metis parts.Body)
    38.1 --- a/src/HOL/Probability/Conditional_Expectation.thy	Tue Jan 22 10:50:47 2019 +0000
    38.2 +++ b/src/HOL/Probability/Conditional_Expectation.thy	Tue Jan 22 12:00:16 2019 +0000
    38.3 @@ -438,7 +438,7 @@
    38.4  proof (rule nn_cond_exp_charact, auto)
    38.5    interpret G: sigma_finite_subalgebra M G by (rule nested_subalg_is_sigma_finite[OF assms(1) assms(2)])
    38.6    fix A assume [measurable]: "A \<in> sets F"
    38.7 -  then have [measurable]: "A \<in> sets G" using assms(2) by (meson set_mp subalgebra_def)
    38.8 +  then have [measurable]: "A \<in> sets G" using assms(2) by (meson subsetD subalgebra_def)
    38.9  
   38.10    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)"
   38.11      by (metis (no_types) mult.commute)
   38.12 @@ -1032,7 +1032,7 @@
   38.13    show "integrable M (real_cond_exp M G f)" by (auto simp add: assms G.real_cond_exp_int(1))
   38.14  
   38.15    fix A assume [measurable]: "A \<in> sets F"
   38.16 -  then have [measurable]: "A \<in> sets G" using assms(2) by (meson set_mp subalgebra_def)
   38.17 +  then have [measurable]: "A \<in> sets G" using assms(2) by (meson subsetD subalgebra_def)
   38.18    have "set_lebesgue_integral M A (real_cond_exp M G f) = set_lebesgue_integral M A f"
   38.19      by (rule G.real_cond_exp_intA[symmetric], auto simp add: assms(3))
   38.20    also have "... = set_lebesgue_integral M A (real_cond_exp M F f)"
   38.21 @@ -1046,7 +1046,7 @@
   38.22    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)"
   38.23  proof (rule real_cond_exp_charact)
   38.24    fix A assume [measurable]: "A \<in> sets F"
   38.25 -  then have A_meas [measurable]: "A \<in> sets M" by (meson set_mp subalg subalgebra_def)
   38.26 +  then have A_meas [measurable]: "A \<in> sets M" by (meson subsetD subalg subalgebra_def)
   38.27    have *: "integrable M (\<lambda>x. indicator A x * f i x)" for i
   38.28      using integrable_mult_indicator[OF \<open>A \<in> sets M\<close> assms(1)] by auto
   38.29    have **: "integrable M (\<lambda>x. indicator A x * real_cond_exp M F (f i) x)" for i
    39.1 --- a/src/HOL/Probability/Fin_Map.thy	Tue Jan 22 10:50:47 2019 +0000
    39.2 +++ b/src/HOL/Probability/Fin_Map.thy	Tue Jan 22 12:00:16 2019 +0000
    39.3 @@ -1094,7 +1094,7 @@
    39.4      show "range S' \<subseteq> Collect open"
    39.5        using S
    39.6        apply (auto simp add: from_nat_into countable_basis_proj S'_def)
    39.7 -      apply (metis UNIV_not_empty Union_empty from_nat_into set_mp topological_basis_open[OF basis_proj] basis_proj_def)
    39.8 +      apply (metis UNIV_not_empty Union_empty from_nat_into subsetD topological_basis_open[OF basis_proj] basis_proj_def)
    39.9        done
   39.10      show "Collect open \<subseteq> Pow (space borel)" by simp
   39.11      show "sets borel = sigma_sets (space borel) (Collect open)"
   39.12 @@ -1322,7 +1322,7 @@
   39.13    unfolding mapmeasure_def
   39.14  proof (subst emeasure_distr, subst measurable_cong_sets[OF s2 refl], rule fm_measurable)
   39.15    have "X \<subseteq> space (Pi\<^sub>M J (\<lambda>_. N))" using assms by (simp add: sets.sets_into_space)
   39.16 -  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"
   39.17 +  from assms inj_on_fm[of "\<lambda>_. N"] subsetD[OF this] have "fm -` fm ` X \<inter> space (Pi\<^sub>M J (\<lambda>_. N)) = X"
   39.18      by (auto simp: vimage_image_eq inj_on_def)
   39.19    thus "emeasure M X = emeasure M (fm -` fm ` X \<inter> space M)" using s1
   39.20      by simp
    40.1 --- a/src/HOL/Probability/Projective_Limit.thy	Tue Jan 22 10:50:47 2019 +0000
    40.2 +++ b/src/HOL/Probability/Projective_Limit.thy	Tue Jan 22 12:00:16 2019 +0000
    40.3 @@ -260,7 +260,7 @@
    40.4      have "\<mu>G (Z n) - \<mu>G (Y n) = \<mu>G (Z n - Y n)"
    40.5        using J J_mono K_sets \<open>n \<ge> 1\<close>
    40.6        by (simp only: emeasure_eq_measure Z_def)
    40.7 -         (auto dest!: bspec[where x=n] intro!: measure_Diff[symmetric] set_mp[OF K_B]
    40.8 +         (auto dest!: bspec[where x=n] intro!: measure_Diff[symmetric] subsetD[OF K_B]
    40.9                 intro!: arg_cong[where f=ennreal]
   40.10                 simp: extensional_restrict emeasure_eq_measure prod_emb_iff sets_P space_P
   40.11                       ennreal_minus measure_nonneg)
    41.1 --- a/src/HOL/Set.thy	Tue Jan 22 10:50:47 2019 +0000
    41.2 +++ b/src/HOL/Set.thy	Tue Jan 22 12:00:16 2019 +0000
    41.3 @@ -462,18 +462,18 @@
    41.4    by (simp add: less_eq_set_def le_fun_def)
    41.5    \<comment> \<open>Rule in Modus Ponens style.\<close>
    41.6  
    41.7 -lemma rev_subsetD [intro?]: "c \<in> A \<Longrightarrow> A \<subseteq> B \<Longrightarrow> c \<in> B"
    41.8 +lemma rev_subsetD [intro?,no_atp]: "c \<in> A \<Longrightarrow> A \<subseteq> B \<Longrightarrow> c \<in> B"
    41.9    \<comment> \<open>The same, with reversed premises for use with @{method erule} -- cf. @{thm rev_mp}.\<close>
   41.10    by (rule subsetD)
   41.11  
   41.12 -lemma subsetCE [elim]: "A \<subseteq> B \<Longrightarrow> (c \<notin> A \<Longrightarrow> P) \<Longrightarrow> (c \<in> B \<Longrightarrow> P) \<Longrightarrow> P"
   41.13 +lemma subsetCE [elim,no_atp]: "A \<subseteq> B \<Longrightarrow> (c \<notin> A \<Longrightarrow> P) \<Longrightarrow> (c \<in> B \<Longrightarrow> P) \<Longrightarrow> P"
   41.14    \<comment> \<open>Classical elimination rule.\<close>
   41.15    by (auto simp add: less_eq_set_def le_fun_def)
   41.16  
   41.17  lemma subset_eq: "A \<subseteq> B \<longleftrightarrow> (\<forall>x\<in>A. x \<in> B)"
   41.18    by blast
   41.19  
   41.20 -lemma contra_subsetD: "A \<subseteq> B \<Longrightarrow> c \<notin> B \<Longrightarrow> c \<notin> A"
   41.21 +lemma contra_subsetD [no_atp]: "A \<subseteq> B \<Longrightarrow> c \<notin> B \<Longrightarrow> c \<notin> A"
   41.22    by blast
   41.23  
   41.24  lemma subset_refl: "A \<subseteq> A"
   41.25 @@ -482,12 +482,6 @@
   41.26  lemma subset_trans: "A \<subseteq> B \<Longrightarrow> B \<subseteq> C \<Longrightarrow> A \<subseteq> C"
   41.27    by (fact order_trans)
   41.28  
   41.29 -lemma set_rev_mp: "x \<in> A \<Longrightarrow> A \<subseteq> B \<Longrightarrow> x \<in> B"
   41.30 -  by (rule subsetD)
   41.31 -
   41.32 -lemma set_mp: "A \<subseteq> B \<Longrightarrow> x \<in> A \<Longrightarrow> x \<in> B"
   41.33 -  by (rule subsetD)
   41.34 -
   41.35  lemma subset_not_subset_eq [code]: "A \<subset> B \<longleftrightarrow> A \<subseteq> B \<and> \<not> B \<subseteq> A"
   41.36    by (fact less_le_not_le)
   41.37  
   41.38 @@ -495,7 +489,7 @@
   41.39    by simp
   41.40  
   41.41  lemmas basic_trans_rules [trans] =
   41.42 -  order_trans_rules set_rev_mp set_mp eq_mem_trans
   41.43 +  order_trans_rules rev_subsetD subsetD eq_mem_trans
   41.44  
   41.45  
   41.46  subsubsection \<open>Equality\<close>
   41.47 @@ -1947,6 +1941,8 @@
   41.48  hide_const (open) member not_member
   41.49  
   41.50  lemmas equalityI = subset_antisym
   41.51 +lemmas set_mp = subsetD
   41.52 +lemmas set_rev_mp = rev_subsetD
   41.53  
   41.54  ML \<open>
   41.55  val Ball_def = @{thm Ball_def}
    42.1 --- a/src/HOL/Types_To_Sets/Examples/Linear_Algebra_On_With.thy	Tue Jan 22 10:50:47 2019 +0000
    42.2 +++ b/src/HOL/Types_To_Sets/Examples/Linear_Algebra_On_With.thy	Tue Jan 22 12:00:16 2019 +0000
    42.3 @@ -22,7 +22,7 @@
    42.4    assume transfer_rules[transfer_rule]: "(A ===> A ===> A) p p'" "A z z'" "((=) ===> A ===> A) s s'" "rel_set A X X'"
    42.5    have "Domainp A z" using \<open>A z z'\<close> by force
    42.6    have *: "t \<subseteq> X \<Longrightarrow> (\<forall>x\<in>t. Domainp A x)" for t
    42.7 -    by (meson Domainp.DomainI \<open>rel_set A X X'\<close> rel_setD1 set_mp)
    42.8 +    by (meson Domainp.DomainI \<open>rel_set A X X'\<close> rel_setD1 subsetD)
    42.9    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)]
   42.10    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
   42.11    proof cases
   42.12 @@ -59,7 +59,7 @@
   42.13    fix p p' z z' X X' and s s'::"'c \<Rightarrow> _"
   42.14    assume [transfer_rule]: "(A ===> A ===> A) p p'" "A z z'" "((=) ===> A ===> A) s s'" "rel_set A X X'"
   42.15    have *: "t \<subseteq> X \<Longrightarrow> (\<forall>x\<in>t. Domainp A x)" for t
   42.16 -    by (meson Domainp.DomainI \<open>rel_set A X X'\<close> rel_setD1 set_mp)
   42.17 +    by (meson Domainp.DomainI \<open>rel_set A X X'\<close> rel_setD1 subsetD)
   42.18    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)) =
   42.19      (\<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))"
   42.20      apply (transfer_prover_start, transfer_step+)
    43.1 --- a/src/HOL/Vector_Spaces.thy	Tue Jan 22 10:50:47 2019 +0000
    43.2 +++ b/src/HOL/Vector_Spaces.thy	Tue Jan 22 12:00:16 2019 +0000
    43.3 @@ -817,7 +817,7 @@
    43.4      by (simp add: vs1.extend_basis_superset[OF i] vs1.span_mono)
    43.5    then show "x \<in> range (construct B f)"
    43.6      using f2 x by (metis (no_types) construct_basis[OF i, of _ f]
    43.7 -        vs1.span_extend_basis[OF i] set_mp span_image spans_image)
    43.8 +        vs1.span_extend_basis[OF i] subsetD span_image spans_image)
    43.9  qed
   43.10  
   43.11  lemma range_construct_eq_span: