tuned
authornipkow
Sun Nov 11 16:08:59 2018 +0100 (6 months ago)
changeset 69286e4d5a07fecb6
parent 69285 b9dd40e2c470
child 69287 0fde0dca6744
tuned
src/HOL/Analysis/Abstract_Topology.thy
src/HOL/Analysis/Brouwer_Fixpoint.thy
src/HOL/Analysis/Complex_Analysis_Basics.thy
src/HOL/Analysis/Continuous_Extension.thy
src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy
src/HOL/Analysis/Measure_Space.thy
src/HOL/Analysis/Starlike.thy
src/HOL/Analysis/Topology_Euclidean_Space.thy
src/HOL/Finite_Set.thy
     1.1 --- a/src/HOL/Analysis/Abstract_Topology.thy	Sun Nov 11 14:34:02 2018 +0100
     1.2 +++ b/src/HOL/Analysis/Abstract_Topology.thy	Sun Nov 11 16:08:59 2018 +0100
     1.3 @@ -1190,13 +1190,13 @@
     1.4      assume *[rule_format]: "\<forall>U\<subseteq>topspace X'. openin X {x \<in> topspace X. f x \<in> U} = openin X' U"
     1.5        and U': "U' \<subseteq> topspace X'"
     1.6      show "closedin X {x \<in> topspace X. f x \<in> U'} = closedin X' U'"
     1.7 -      using U'  by (auto simp add: closedin_def Diff_subset simp flip: * [of "topspace X' - U'"] eq [OF that])
     1.8 +      using U'  by (auto simp add: closedin_def simp flip: * [of "topspace X' - U'"] eq [OF that])
     1.9    next
    1.10      fix U' :: "'b set"
    1.11      assume *[rule_format]: "\<forall>U\<subseteq>topspace X'. closedin X {x \<in> topspace X. f x \<in> U} = closedin X' U"
    1.12        and U': "U' \<subseteq> topspace X'"
    1.13      show "openin X {x \<in> topspace X. f x \<in> U'} = openin X' U'"
    1.14 -      using U'  by (auto simp add: openin_closedin_eq Diff_subset simp flip: * [of "topspace X' - U'"] eq [OF that])
    1.15 +      using U'  by (auto simp add: openin_closedin_eq simp flip: * [of "topspace X' - U'"] eq [OF that])
    1.16    qed
    1.17    then show ?thesis
    1.18      unfolding quotient_map_def by force
    1.19 @@ -1491,7 +1491,7 @@
    1.20  
    1.21  lemma separatedin_closedin_diff:
    1.22       "\<lbrakk>closedin X S; closedin X T\<rbrakk> \<Longrightarrow> separatedin X (S - T) (T - S)"
    1.23 -  apply (simp add: separatedin_def Diff_Int_distrib2 Diff_subset closure_of_minimal inf_absorb2)
    1.24 +  apply (simp add: separatedin_def Diff_Int_distrib2 closure_of_minimal inf_absorb2)
    1.25    apply (meson Diff_subset closedin_subset subset_trans)
    1.26    done
    1.27  
     2.1 --- a/src/HOL/Analysis/Brouwer_Fixpoint.thy	Sun Nov 11 14:34:02 2018 +0100
     2.2 +++ b/src/HOL/Analysis/Brouwer_Fixpoint.thy	Sun Nov 11 16:08:59 2018 +0100
     2.3 @@ -1728,7 +1728,7 @@
     2.4    have "f ` (A - {a}) = g ` (A - {a})"
     2.5      by (intro image_cong) (simp_all add: eq)
     2.6    then have "B - {f a} = B - {g a}"
     2.7 -    using f g a  by (auto simp: bij_betw_def inj_on_image_set_diff set_eq_iff Diff_subset)
     2.8 +    using f g a  by (auto simp: bij_betw_def inj_on_image_set_diff set_eq_iff)
     2.9    moreover have "f a \<in> B" "g a \<in> B"
    2.10      using f g a by (auto simp: bij_betw_def)
    2.11    ultimately show ?thesis
    2.12 @@ -1884,9 +1884,9 @@
    2.13      moreover obtain a where "rl a = Suc n" "a \<in> s"
    2.14        by (metis atMost_iff image_iff le_Suc_eq rl)
    2.15      ultimately have n: "{..n} = rl ` (s - {a})"
    2.16 -      by (auto simp: inj_on_image_set_diff Diff_subset rl)
    2.17 +      by (auto simp: inj_on_image_set_diff rl)
    2.18      have "{a\<in>s. rl ` (s - {a}) = {..n}} = {a}"
    2.19 -      using inj_rl \<open>a \<in> s\<close> by (auto simp: n inj_on_image_eq_iff[OF inj_rl] Diff_subset)
    2.20 +      using inj_rl \<open>a \<in> s\<close> by (auto simp: n inj_on_image_eq_iff[OF inj_rl])
    2.21      then show "card ?S = 1"
    2.22        unfolding card_S by simp }
    2.23  
    2.24 @@ -1907,7 +1907,7 @@
    2.25  
    2.26        { fix x assume "x \<in> s" "x \<notin> {a, b}"
    2.27          then have "rl ` s - {rl x} = rl ` ((s - {a}) - {x})"
    2.28 -          by (auto simp: eq Diff_subset inj_on_image_set_diff[OF inj])
    2.29 +          by (auto simp: eq inj_on_image_set_diff[OF inj])
    2.30          also have "\<dots> = rl ` (s - {x})"
    2.31            using ab \<open>x \<notin> {a, b}\<close> by auto
    2.32          also assume "\<dots> = rl ` s"
    2.33 @@ -2448,7 +2448,7 @@
    2.34        by auto
    2.35      finally have eq: "s - {a} = f' ` {.. n} - {f' n}"
    2.36        unfolding s_eq \<open>a = enum i\<close> \<open>i = 0\<close>
    2.37 -      by (simp add: Diff_subset inj_on_image_set_diff[OF inj_enum] inj_on_image_set_diff[OF inj_f'])
    2.38 +      by (simp add: inj_on_image_set_diff[OF inj_enum] inj_on_image_set_diff[OF inj_f'])
    2.39  
    2.40      have "enum 0 < f' 0"
    2.41        using \<open>n \<noteq> 0\<close> by (simp add: enum_strict_mono f'_eq_enum)
     3.1 --- a/src/HOL/Analysis/Complex_Analysis_Basics.thy	Sun Nov 11 14:34:02 2018 +0100
     3.2 +++ b/src/HOL/Analysis/Complex_Analysis_Basics.thy	Sun Nov 11 16:08:59 2018 +0100
     3.3 @@ -761,7 +761,7 @@
     3.4    show ?rhs
     3.5      apply (rule_tac x="s \<inter> t" in exI)
     3.6      using st
     3.7 -    apply (auto simp: Diff_subset holomorphic_on_subset)
     3.8 +    apply (auto simp: holomorphic_on_subset)
     3.9      done
    3.10  next
    3.11    assume ?rhs
     4.1 --- a/src/HOL/Analysis/Continuous_Extension.thy	Sun Nov 11 14:34:02 2018 +0100
     4.2 +++ b/src/HOL/Analysis/Continuous_Extension.thy	Sun Nov 11 16:08:59 2018 +0100
     4.3 @@ -36,7 +36,7 @@
     4.4      have sd_pos: "0 < setdist {x} (S - V)" if "V \<in> \<C>" "x \<in> S" "x \<in> V" for V x
     4.5      proof -
     4.6        have "closedin (subtopology euclidean S) (S - V)"
     4.7 -        by (simp add: Diff_Diff_Int Diff_subset closedin_def opC openin_open_Int \<open>V \<in> \<C>\<close>)
     4.8 +        by (simp add: Diff_Diff_Int closedin_def opC openin_open_Int \<open>V \<in> \<C>\<close>)
     4.9        with that False setdist_eq_0_closedin [of S "S-V" x] setdist_pos_le [of "{x}" "S - V"]
    4.10          show ?thesis
    4.11            by (simp add: order_class.order.order_iff_strict)
     5.1 --- a/src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy	Sun Nov 11 14:34:02 2018 +0100
     5.2 +++ b/src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy	Sun Nov 11 16:08:59 2018 +0100
     5.3 @@ -1246,7 +1246,7 @@
     5.4        case 1
     5.5        show ?thesis
     5.6          by (rule negligible_subset [of "closure S"])
     5.7 -           (simp_all add: Diff_subset frontier_def negligible_lowdim 1)
     5.8 +           (simp_all add: frontier_def negligible_lowdim 1)
     5.9      next
    5.10        case 2
    5.11        obtain a where a: "a \<in> interior S"
     6.1 --- a/src/HOL/Analysis/Measure_Space.thy	Sun Nov 11 14:34:02 2018 +0100
     6.2 +++ b/src/HOL/Analysis/Measure_Space.thy	Sun Nov 11 16:08:59 2018 +0100
     6.3 @@ -1528,7 +1528,7 @@
     6.4  
     6.5    show "a \<in> {A \<in> sets M. emeasure M A \<noteq> top} \<Longrightarrow> b \<in> {A \<in> sets M. emeasure M A \<noteq> top} \<Longrightarrow>
     6.6      a - b \<in> {A \<in> sets M. emeasure M A \<noteq> top}" for a b
     6.7 -    using emeasure_mono[of "a - b" a M] by (auto simp: Diff_subset top_unique)
     6.8 +    using emeasure_mono[of "a - b" a M] by (auto simp: top_unique)
     6.9  qed (auto dest: sets.sets_into_space)
    6.10  
    6.11  lemma measure_nonneg[simp]: "0 \<le> measure M A"
    6.12 @@ -1746,7 +1746,7 @@
    6.13    finally show  "a \<union> b \<in> fmeasurable M"
    6.14      using * by (auto intro: fmeasurableI)
    6.15    show "a - b \<in> fmeasurable M"
    6.16 -    using emeasure_mono[of "a - b" a M] * by (auto simp: fmeasurable_def Diff_subset)
    6.17 +    using emeasure_mono[of "a - b" a M] * by (auto simp: fmeasurable_def)
    6.18  qed
    6.19  
    6.20  subsection\<open>Measurable sets formed by unions and intersections\<close>
     7.1 --- a/src/HOL/Analysis/Starlike.thy	Sun Nov 11 14:34:02 2018 +0100
     7.2 +++ b/src/HOL/Analysis/Starlike.thy	Sun Nov 11 16:08:59 2018 +0100
     7.3 @@ -5726,7 +5726,7 @@
     7.4    shows "k \<in> Basis \<Longrightarrow> dim {x. k \<bullet> x = 0} = DIM('n) - 1"
     7.5  apply (simp add: special_hyperplane_span)
     7.6  apply (rule dim_unique [OF subset_refl])
     7.7 -apply (auto simp: Diff_subset independent_substdbasis)
     7.8 +apply (auto simp: independent_substdbasis)
     7.9  apply (metis member_remove remove_def span_base)
    7.10  done
    7.11  
    7.12 @@ -6823,7 +6823,7 @@
    7.13      using assms orthogonal_spanningset_subspace by blast
    7.14    then show ?thesis
    7.15      apply (rule_tac B = "B - {0}" in that)
    7.16 -    apply (auto simp: indep_card_eq_dim_span pairwise_subset Diff_subset pairwise_orthogonal_independent elim: pairwise_subset)
    7.17 +    apply (auto simp: indep_card_eq_dim_span pairwise_subset pairwise_orthogonal_independent elim: pairwise_subset)
    7.18      done
    7.19  qed
    7.20  
    7.21 @@ -7178,7 +7178,7 @@
    7.22        have "closed S"
    7.23          by (simp add: \<open>subspace S\<close> closed_subspace)
    7.24        then show "closure (S - U) \<subseteq> S"
    7.25 -        by (simp add: Diff_subset closure_minimal)
    7.26 +        by (simp add: closure_minimal)
    7.27        show "S \<subseteq> closure (S - U)"
    7.28        proof (clarsimp simp: closure_approachable)
    7.29          fix x and e::real
    7.30 @@ -7258,7 +7258,7 @@
    7.31      shows "closure(S - T) = closure S"
    7.32  proof
    7.33    show "closure (S - T) \<subseteq> closure S"
    7.34 -    by (simp add: Diff_subset closure_mono)
    7.35 +    by (simp add: closure_mono)
    7.36    have "closure (rel_interior S - T) = closure (rel_interior S)"
    7.37      apply (rule dense_complement_openin_affine_hull)
    7.38      apply (simp add: assms rel_interior_aff_dim)
     8.1 --- a/src/HOL/Analysis/Topology_Euclidean_Space.thy	Sun Nov 11 14:34:02 2018 +0100
     8.2 +++ b/src/HOL/Analysis/Topology_Euclidean_Space.thy	Sun Nov 11 16:08:59 2018 +0100
     8.3 @@ -794,7 +794,7 @@
     8.4    by (meson openin_discrete_topology openin_subset openin_topspace order_refl subset_antisym)
     8.5  
     8.6  lemma closedin_discrete_topology [simp]: "closedin (discrete_topology U) S \<longleftrightarrow> S \<subseteq> U"
     8.7 -  by (simp add: Diff_subset closedin_def)
     8.8 +  by (simp add: closedin_def)
     8.9  
    8.10  lemma discrete_topology_unique:
    8.11     "discrete_topology U = X \<longleftrightarrow> topspace X = U \<and> (\<forall>x \<in> U. openin X {x})" (is "?lhs = ?rhs")
     9.1 --- a/src/HOL/Finite_Set.thy	Sun Nov 11 14:34:02 2018 +0100
     9.2 +++ b/src/HOL/Finite_Set.thy	Sun Nov 11 16:08:59 2018 +0100
     9.3 @@ -291,7 +291,7 @@
     9.4    from B_A \<open>x \<notin> B\<close> have "B = f ` A - {x}"
     9.5      by blast
     9.6    with B_A \<open>x \<notin> B\<close> \<open>x = f y\<close> \<open>inj_on f A\<close> \<open>y \<in> A\<close> have "B = f ` (A - {y})"
     9.7 -    by (simp add: inj_on_image_set_diff Set.Diff_subset)
     9.8 +    by (simp add: inj_on_image_set_diff)
     9.9    moreover from \<open>inj_on f A\<close> have "inj_on f (A - {y})"
    9.10      by (rule inj_on_diff)
    9.11    ultimately have "finite (A - {y})"