rename subset_{interior,closure} to {interior,closure}_mono;
authorhuffman
Thu Aug 25 12:43:55 2011 -0700 (2011-08-25)
changeset 445222f7e9d890efe
parent 44521 083eedb37a37
child 44523 d55161d67821
rename subset_{interior,closure} to {interior,closure}_mono;
remove some legacy theorem names;
NEWS
src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy
src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy
src/HOL/Multivariate_Analysis/Integration.thy
src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
     1.1 --- a/NEWS	Thu Aug 25 11:57:42 2011 -0700
     1.2 +++ b/NEWS	Thu Aug 25 12:43:55 2011 -0700
     1.3 @@ -200,6 +200,28 @@
     1.4    tendsto_vector   ~> vec_tendstoI
     1.5    Cauchy_vector    ~> vec_CauchyI
     1.6  
     1.7 +* Session Multivariate_Analysis: Several duplicate theorems have been
     1.8 +removed, and other theorems have been renamed. INCOMPATIBILITY.
     1.9 +
    1.10 +  eventually_conjI ~> eventually_conj
    1.11 +  eventually_and ~> eventually_conj_iff
    1.12 +  eventually_false ~> eventually_False
    1.13 +  Lim_ident_at ~> LIM_ident
    1.14 +  Lim_const ~> tendsto_const
    1.15 +  Lim_cmul ~> tendsto_scaleR [OF tendsto_const]
    1.16 +  Lim_neg ~> tendsto_minus
    1.17 +  Lim_add ~> tendsto_add
    1.18 +  Lim_sub ~> tendsto_diff
    1.19 +  Lim_mul ~> tendsto_scaleR
    1.20 +  Lim_vmul ~> tendsto_scaleR [OF _ tendsto_const]
    1.21 +  Lim_null_norm ~> tendsto_norm_zero_iff [symmetric]
    1.22 +  Lim_linear ~> bounded_linear.tendsto
    1.23 +  Lim_component ~> tendsto_euclidean_component
    1.24 +  Lim_component_cart ~> tendsto_vec_nth
    1.25 +  subset_interior ~> interior_mono
    1.26 +  subset_closure ~> closure_mono
    1.27 +  closure_univ ~> closure_UNIV
    1.28 +
    1.29  * Complex_Main: The locale interpretations for the bounded_linear and
    1.30  bounded_bilinear locales have been removed, in order to reduce the
    1.31  number of duplicate lemmas. Users must use the original names for
    1.32 @@ -213,6 +235,16 @@
    1.33    mult_right.setsum ~> setsum_right_distrib
    1.34    mult_left.diff ~> left_diff_distrib
    1.35  
    1.36 +* Complex_Main: Several redundant theorems about real numbers have
    1.37 +been removed or generalized and renamed. INCOMPATIBILITY.
    1.38 +
    1.39 +  real_0_le_divide_iff ~> zero_le_divide_iff
    1.40 +  realpow_two_disj ~> power2_eq_iff
    1.41 +  real_squared_diff_one_factored ~> square_diff_one_factored
    1.42 +  realpow_two_diff ~> square_diff_square_factored
    1.43 +  exp_ln_eq ~> ln_unique
    1.44 +  lemma_DERIV_subst ~> DERIV_cong
    1.45 +
    1.46  
    1.47  *** Document preparation ***
    1.48  
     2.1 --- a/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy	Thu Aug 25 11:57:42 2011 -0700
     2.2 +++ b/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy	Thu Aug 25 12:43:55 2011 -0700
     2.3 @@ -2001,8 +2001,4 @@
     2.4      apply(erule_tac x=e in allE,safe) apply(rule_tac x=d in exI,safe)
     2.5      apply(erule_tac x=p in allE,safe) unfolding * norm_vector_1 by auto qed
     2.6  
     2.7 -text {* Legacy theorem names *}
     2.8 -
     2.9 -lemmas Lim_component_cart = tendsto_vec_nth
    2.10 -
    2.11  end
     3.1 --- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Thu Aug 25 11:57:42 2011 -0700
     3.2 +++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Thu Aug 25 12:43:55 2011 -0700
     3.3 @@ -2311,7 +2311,7 @@
     3.4    fixes S :: "('n::euclidean_space) set"
     3.5    shows "closure S <= affine hull S"
     3.6  proof-
     3.7 -have "closure S <= closure (affine hull S)" using subset_closure by auto
     3.8 +have "closure S <= closure (affine hull S)" using closure_mono by auto
     3.9  moreover have "closure (affine hull S) = affine hull S" 
    3.10     using affine_affine_hull affine_closed[of "affine hull S"] closure_eq by auto
    3.11  ultimately show ?thesis by auto  
    3.12 @@ -4047,7 +4047,7 @@
    3.13    then obtain y where "y\<in>s" and y:"norm (y - x) * (1 - e) < e * d" by auto
    3.14    def z \<equiv> "c + ((1 - e) / e) *\<^sub>R (x - y)"
    3.15    have *:"x - e *\<^sub>R (x - c) = y - e *\<^sub>R (y - z)" unfolding z_def using `e>0` by (auto simp add: scaleR_right_diff_distrib scaleR_right_distrib scaleR_left_diff_distrib)
    3.16 -  have "z\<in>interior s" apply(rule subset_interior[OF d,unfolded subset_eq,rule_format])
    3.17 +  have "z\<in>interior s" apply(rule interior_mono[OF d,unfolded subset_eq,rule_format])
    3.18      unfolding interior_open[OF open_ball] mem_ball z_def dist_norm using y and assms(4,5)
    3.19      by(auto simp add:field_simps norm_minus_commute)
    3.20    thus ?thesis unfolding * apply - apply(rule mem_interior_convex_shrink) 
    3.21 @@ -4385,7 +4385,7 @@
    3.22  shows "closure(rel_interior S) = closure S"
    3.23  proof-
    3.24  have h1: "closure(rel_interior S) <= closure S" 
    3.25 -   using subset_closure[of "rel_interior S" S] rel_interior_subset[of S] by auto
    3.26 +   using closure_mono[of "rel_interior S" S] rel_interior_subset[of S] by auto
    3.27  { assume "S ~= {}" from this obtain a where a_def: "a : rel_interior S" 
    3.28      using rel_interior_convex_nonempty assms by auto
    3.29    { fix x assume x_def: "x : closure S"
    3.30 @@ -4522,7 +4522,7 @@
    3.31  proof-
    3.32  have "?A --> ?B" by (metis assms closure_subset convex_rel_interior_closure rel_interior_subset)
    3.33  moreover have "?B --> (closure S1 <= closure S2)" 
    3.34 -     by (metis assms(1) convex_closure_rel_interior subset_closure)
    3.35 +     by (metis assms(1) convex_closure_rel_interior closure_mono)
    3.36  moreover have "?B --> (closure S1 >= closure S2)" by (metis closed_closure closure_minimal)
    3.37  ultimately show ?thesis by blast
    3.38  qed
    3.39 @@ -4782,7 +4782,7 @@
    3.40    using convex_closure_rel_interior_inter assms by auto
    3.41  moreover have "closure (Inter {rel_interior S |S. S : I}) <= closure (Inter I)" 
    3.42      using rel_interior_inter_aux 
    3.43 -          subset_closure[of "Inter {rel_interior S |S. S : I}" "Inter I"] by auto
    3.44 +          closure_mono[of "Inter {rel_interior S |S. S : I}" "Inter I"] by auto
    3.45  ultimately show ?thesis using closure_inter[of I] by auto
    3.46  qed
    3.47  
    3.48 @@ -4795,7 +4795,7 @@
    3.49    using convex_closure_rel_interior_inter assms by auto
    3.50  moreover have "closure (Inter {rel_interior S |S. S : I}) <= closure (Inter I)" 
    3.51      using rel_interior_inter_aux 
    3.52 -          subset_closure[of "Inter {rel_interior S |S. S : I}" "Inter I"] by auto
    3.53 +          closure_mono[of "Inter {rel_interior S |S. S : I}" "Inter I"] by auto
    3.54  ultimately show ?thesis using closure_inter[of I] by auto
    3.55  qed
    3.56  
    3.57 @@ -4891,7 +4891,7 @@
    3.58  proof-
    3.59  have *: "S Int closure T = S" using assms by auto
    3.60  have "~(rel_interior S <= rel_frontier T)"
    3.61 -     using subset_closure[of "rel_interior S" "rel_frontier T"] closed_rel_frontier[of T] 
    3.62 +     using closure_mono[of "rel_interior S" "rel_frontier T"] closed_rel_frontier[of T] 
    3.63       closure_closed convex_closure_rel_interior[of S] closure_subset[of S] assms by auto
    3.64  hence "(rel_interior S) Int (rel_interior (closure T)) ~= {}" 
    3.65       using assms rel_frontier_def[of T] rel_interior_subset convex_rel_interior_closure[of T] by auto
    3.66 @@ -4916,8 +4916,8 @@
    3.67  also have "... = f ` (closure (rel_interior S))" using convex_closure_rel_interior assms by auto  
    3.68  also have "... <= closure (f ` (rel_interior S))" using closure_linear_image assms by auto 
    3.69  finally have "closure (f ` S) = closure (f ` rel_interior S)"
    3.70 -   using subset_closure[of "f ` S" "closure (f ` rel_interior S)"] closure_closure 
    3.71 -         subset_closure[of "f ` rel_interior S" "f ` S"] * by auto
    3.72 +   using closure_mono[of "f ` S" "closure (f ` rel_interior S)"] closure_closure 
    3.73 +         closure_mono[of "f ` rel_interior S" "f ` S"] * by auto
    3.74  hence "rel_interior (f ` S) = rel_interior (f ` rel_interior S)" using assms convex_rel_interior
    3.75     linear_conv_bounded_linear[of f] convex_linear_image[of S] convex_linear_image[of "rel_interior S"] 
    3.76     closure_eq_rel_interior_eq[of "f ` S" "f ` rel_interior S"] by auto
     4.1 --- a/src/HOL/Multivariate_Analysis/Integration.thy	Thu Aug 25 11:57:42 2011 -0700
     4.2 +++ b/src/HOL/Multivariate_Analysis/Integration.thy	Thu Aug 25 12:43:55 2011 -0700
     4.3 @@ -378,7 +378,7 @@
     4.4        interior(x1 \<inter> y1) \<subseteq> interior(x1) \<Longrightarrow> interior(x1 \<inter> y1) \<subseteq> interior(y1) \<Longrightarrow>
     4.5        interior(x2 \<inter> y2) \<subseteq> interior(x2) \<Longrightarrow> interior(x2 \<inter> y2) \<subseteq> interior(y2)
     4.6        \<Longrightarrow> interior(x1 \<inter> y1) \<inter> interior(x2 \<inter> y2) = {}" by auto
     4.7 -  show "interior k1 \<inter> interior k2 = {}" unfolding k1 k2 apply(rule *) defer apply(rule_tac[1-4] subset_interior)
     4.8 +  show "interior k1 \<inter> interior k2 = {}" unfolding k1 k2 apply(rule *) defer apply(rule_tac[1-4] interior_mono)
     4.9      using division_ofD(5)[OF assms(1) k1(2) k2(2)]
    4.10      using division_ofD(5)[OF assms(2) k1(3) k2(3)] using th by auto qed qed
    4.11  
    4.12 @@ -407,9 +407,9 @@
    4.13    show "finite (p1 \<union> p2)" using d1(1) d2(1) by auto
    4.14    show "\<Union>(p1 \<union> p2) = s1 \<union> s2" using d1(6) d2(6) by auto
    4.15    { fix k1 k2 assume as:"k1 \<in> p1 \<union> p2" "k2 \<in> p1 \<union> p2" "k1 \<noteq> k2" moreover let ?g="interior k1 \<inter> interior k2 = {}"
    4.16 -  { assume as:"k1\<in>p1" "k2\<in>p2" have ?g using subset_interior[OF d1(2)[OF as(1)]] subset_interior[OF d2(2)[OF as(2)]]
    4.17 +  { assume as:"k1\<in>p1" "k2\<in>p2" have ?g using interior_mono[OF d1(2)[OF as(1)]] interior_mono[OF d2(2)[OF as(2)]]
    4.18        using assms(3) by blast } moreover
    4.19 -  { assume as:"k1\<in>p2" "k2\<in>p1" have ?g using subset_interior[OF d1(2)[OF as(2)]] subset_interior[OF d2(2)[OF as(1)]]
    4.20 +  { assume as:"k1\<in>p2" "k2\<in>p1" have ?g using interior_mono[OF d1(2)[OF as(2)]] interior_mono[OF d2(2)[OF as(1)]]
    4.21        using assms(3) by blast} ultimately
    4.22    show ?g using d1(5)[OF _ _ as(3)] and d2(5)[OF _ _ as(3)] by auto }
    4.23    fix k assume k:"k \<in> p1 \<union> p2"  show "k \<subseteq> s1 \<union> s2" using k d1(2) d2(2) by auto
    4.24 @@ -573,7 +573,7 @@
    4.25          show "finite (q k - {k})" "open (interior k)"  "\<forall>t\<in>q k - {k}. \<exists>a b. t = {a..b}" using qk by auto
    4.26          show "\<forall>t\<in>q k - {k}. interior k \<inter> interior t = {}" using qk(5) using q(2)[OF k] by auto
    4.27          have *:"\<And>x s. x \<in> s \<Longrightarrow> \<Inter>s \<subseteq> x" by auto show "interior (\<Inter>(\<lambda>i. \<Union>(q i - {i})) ` p) \<subseteq> interior (\<Union>(q k - {k}))"
    4.28 -          apply(rule subset_interior *)+ using k by auto qed qed qed auto qed
    4.29 +          apply(rule interior_mono *)+ using k by auto qed qed qed auto qed
    4.30  
    4.31  lemma elementary_bounded[dest]: "p division_of s \<Longrightarrow> bounded (s::('a::ordered_euclidean_space) set)"
    4.32    unfolding division_of_def by(metis bounded_Union bounded_interval) 
    4.33 @@ -823,7 +823,7 @@
    4.34    fix x k assume xk:"(x,k)\<in>p1\<union>p2" show "x\<in>k" "\<exists>a b. k = {a..b}" using xk p1(2,4) p2(2,4) by auto
    4.35    show "k\<subseteq>s1\<union>s2" using xk p1(3) p2(3) by blast
    4.36    fix x' k' assume xk':"(x',k')\<in>p1\<union>p2" "(x,k) \<noteq> (x',k')"
    4.37 -  have *:"\<And>a b. a\<subseteq> s1 \<Longrightarrow> b\<subseteq> s2 \<Longrightarrow> interior a \<inter> interior b = {}" using assms(3) subset_interior by blast
    4.38 +  have *:"\<And>a b. a\<subseteq> s1 \<Longrightarrow> b\<subseteq> s2 \<Longrightarrow> interior a \<inter> interior b = {}" using assms(3) interior_mono by blast
    4.39    show "interior k \<inter> interior k' = {}" apply(cases "(x,k)\<in>p1", case_tac[!] "(x',k')\<in>p1")
    4.40      apply(rule p1(5)) prefer 4 apply(rule *) prefer 6 apply(subst Int_commute,rule *) prefer 8 apply(rule p2(5))
    4.41      using p1(3) p2(3) using xk xk' by auto qed 
    4.42 @@ -842,7 +842,7 @@
    4.43    show "x\<in>k" "\<exists>a b. k = {a..b}" "k \<subseteq> \<Union>iset" using assm(2-4)[OF i] using i(1) by auto
    4.44    fix x' k' assume xk':"(x',k')\<in>\<Union>pfn ` iset" "(x, k) \<noteq> (x', k')" then obtain i' where i':"i' \<in> iset" "(x', k') \<in> pfn i'" by auto
    4.45    have *:"\<And>a b. i\<noteq>i' \<Longrightarrow> a\<subseteq> i \<Longrightarrow> b\<subseteq> i' \<Longrightarrow> interior a \<inter> interior b = {}" using i(1) i'(1)
    4.46 -    using assms(3)[rule_format] subset_interior by blast
    4.47 +    using assms(3)[rule_format] interior_mono by blast
    4.48    show "interior k \<inter> interior k' = {}" apply(cases "i=i'")
    4.49      using assm(5)[OF i _ xk'(2)]  i'(2) using assm(3)[OF i] assm(3)[OF i'] defer apply-apply(rule *) by auto
    4.50  qed
    4.51 @@ -1703,7 +1703,7 @@
    4.52            by(rule le_less_trans[OF norm_le_l1])
    4.53          hence "x + (\<chi>\<chi> i. if i = k then e/2 else 0) \<in> {x. x$$k = c}" using e by auto
    4.54          thus False unfolding mem_Collect_eq using e x k by auto
    4.55 -      qed ultimately have "content b = 0" unfolding uv content_eq_0_interior apply-apply(drule subset_interior) by auto
    4.56 +      qed ultimately have "content b = 0" unfolding uv content_eq_0_interior apply-apply(drule interior_mono) by auto
    4.57        thus "content b *\<^sub>R f a = 0" by auto
    4.58      qed auto
    4.59      also have "\<dots> < e" by(rule k d(2) p12 fine_union p1 p2)+
    4.60 @@ -2563,7 +2563,7 @@
    4.61          proof(rule,rule,rule,rule,rule,rule,rule,erule conjE) fix m n u v
    4.62            assume as:"{m..n} \<in> snd ` p" "{u..v} \<in> snd ` p" "{m..n} \<noteq> {u..v}"  "{m..n} \<inter> {x. \<bar>x $$ k - c\<bar> \<le> d} = {u..v} \<inter> {x. \<bar>x $$ k - c\<bar> \<le> d}"
    4.63            have "({m..n} \<inter> {x. \<bar>x $$ k - c\<bar> \<le> d}) \<inter> ({u..v} \<inter> {x. \<bar>x $$ k - c\<bar> \<le> d}) \<subseteq> {m..n} \<inter> {u..v}" by blast
    4.64 -          note subset_interior[OF this, unfolded division_ofD(5)[OF p'' as(1-3)] interior_inter[of "{m..n}"]]
    4.65 +          note interior_mono[OF this, unfolded division_ofD(5)[OF p'' as(1-3)] interior_inter[of "{m..n}"]]
    4.66            hence "interior ({m..n} \<inter> {x. \<bar>x $$ k - c\<bar> \<le> d}) = {}" unfolding as Int_absorb by auto
    4.67            thus "content ({m..n} \<inter> {x. \<bar>x $$ k - c\<bar> \<le> d}) = 0" unfolding interval_doublesplit[OF k] content_eq_0_interior[THEN sym] .
    4.68          qed qed
    4.69 @@ -3516,7 +3516,7 @@
    4.70              proof- fix x k k' assume k:"( a, k) \<in> p" "( a, k') \<in> p" "content k \<noteq> 0" "content k' \<noteq> 0"
    4.71                guess v using pa[OF k(1)] .. note v = conjunctD2[OF this]
    4.72                guess v' using pa[OF k(2)] .. note v' = conjunctD2[OF this] let ?v = " (min (v) (v'))"
    4.73 -              have "{ a <..< ?v} \<subseteq> k \<inter> k'" unfolding v v' by(auto simp add:) note subset_interior[OF this,unfolded interior_inter]
    4.74 +              have "{ a <..< ?v} \<subseteq> k \<inter> k'" unfolding v v' by(auto simp add:) note interior_mono[OF this,unfolded interior_inter]
    4.75                moreover have " ((a + ?v)/2) \<in> { a <..< ?v}" using k(3-)
    4.76                  unfolding v v' content_eq_0 not_le by(auto simp add:not_le)
    4.77                ultimately have " ((a + ?v)/2) \<in> interior k \<inter> interior k'" unfolding interior_open[OF open_interval] by auto
    4.78 @@ -3528,7 +3528,7 @@
    4.79              proof- fix x k k' assume k:"( b, k) \<in> p" "( b, k') \<in> p" "content k \<noteq> 0" "content k' \<noteq> 0"
    4.80                guess v using pb[OF k(1)] .. note v = conjunctD2[OF this]
    4.81                guess v' using pb[OF k(2)] .. note v' = conjunctD2[OF this] let ?v = " (max (v) (v'))"
    4.82 -              have "{?v <..<  b} \<subseteq> k \<inter> k'" unfolding v v' by(auto simp add:) note subset_interior[OF this,unfolded interior_inter]
    4.83 +              have "{?v <..<  b} \<subseteq> k \<inter> k'" unfolding v v' by(auto simp add:) note interior_mono[OF this,unfolded interior_inter]
    4.84                moreover have " ((b + ?v)/2) \<in> {?v <..<  b}" using k(3-) unfolding v v' content_eq_0 not_le by auto
    4.85                ultimately have " ((b + ?v)/2) \<in> interior k \<inter> interior k'" unfolding interior_open[OF open_interval] by auto
    4.86                hence *:"k = k'" apply- apply(rule ccontr) using p(5)[OF k(1-2)] by auto
    4.87 @@ -4390,7 +4390,7 @@
    4.88      from this(2) guess u v apply-by(erule exE)+ note uv=this
    4.89      have "l\<in>snd ` p" unfolding image_iff apply(rule_tac x="(x,l)" in bexI) using as by auto
    4.90      hence "l\<in>q" "k\<in>q" "l\<noteq>k" using as(1,3) q(1) unfolding r_def by auto
    4.91 -    note q'(5)[OF this] hence "interior l = {}" using subset_interior[OF `l \<subseteq> k`] by blast
    4.92 +    note q'(5)[OF this] hence "interior l = {}" using interior_mono[OF `l \<subseteq> k`] by blast
    4.93      thus "content l *\<^sub>R f x = 0" unfolding uv content_eq_0_interior[THEN sym] by auto qed auto
    4.94  
    4.95    hence "norm ((\<Sum>(x, k)\<in>p. content k *\<^sub>R f x) + setsum (setsum (\<lambda>(x, k). content k *\<^sub>R f x))
    4.96 @@ -4403,7 +4403,7 @@
    4.97      have *:"interior (k \<inter> l) = {}" unfolding interior_inter apply(rule q')
    4.98        using as unfolding r_def by auto
    4.99      have "interior m = {}" unfolding subset_empty[THEN sym] unfolding *[THEN sym]
   4.100 -      apply(rule subset_interior) using kl(1)[OF as(4,1)] kl(1)[OF as(5,2)] by auto
   4.101 +      apply(rule interior_mono) using kl(1)[OF as(4,1)] kl(1)[OF as(5,2)] by auto
   4.102      thus "content m *\<^sub>R f x = 0" unfolding uv content_eq_0_interior[THEN sym] by auto 
   4.103    qed(insert qq, auto)
   4.104  
     5.1 --- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Thu Aug 25 11:57:42 2011 -0700
     5.2 +++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Thu Aug 25 12:43:55 2011 -0700
     5.3 @@ -588,11 +588,14 @@
     5.4  lemma interior_empty [simp]: "interior {} = {}"
     5.5    using open_empty by (rule interior_open)
     5.6  
     5.7 +lemma interior_UNIV [simp]: "interior UNIV = UNIV"
     5.8 +  using open_UNIV by (rule interior_open)
     5.9 +
    5.10  lemma interior_interior [simp]: "interior (interior S) = interior S"
    5.11    using open_interior by (rule interior_open)
    5.12  
    5.13 -lemma subset_interior: "S \<subseteq> T \<Longrightarrow> interior S \<subseteq> interior T"
    5.14 -  by (auto simp add: interior_def) (* TODO: rename to interior_mono *)
    5.15 +lemma interior_mono: "S \<subseteq> T \<Longrightarrow> interior S \<subseteq> interior T"
    5.16 +  by (auto simp add: interior_def)
    5.17  
    5.18  lemma interior_unique:
    5.19    assumes "T \<subseteq> S" and "open T"
    5.20 @@ -601,7 +604,7 @@
    5.21    by (intro equalityI assms interior_subset open_interior interior_maximal)
    5.22  
    5.23  lemma interior_inter [simp]: "interior (S \<inter> T) = interior S \<inter> interior T"
    5.24 -  by (intro equalityI Int_mono Int_greatest subset_interior Int_lower1
    5.25 +  by (intro equalityI Int_mono Int_greatest interior_mono Int_lower1
    5.26      Int_lower2 interior_maximal interior_subset open_Int open_interior)
    5.27  
    5.28  lemma mem_interior: "x \<in> interior S \<longleftrightarrow> (\<exists>e>0. ball x e \<subseteq> S)"
    5.29 @@ -623,7 +626,7 @@
    5.30    shows "interior (S \<union> T) = interior S"
    5.31  proof
    5.32    show "interior S \<subseteq> interior (S \<union> T)"
    5.33 -    by (rule subset_interior, rule Un_upper1)
    5.34 +    by (rule interior_mono, rule Un_upper1)
    5.35  next
    5.36    show "interior (S \<union> T) \<subseteq> interior S"
    5.37    proof
    5.38 @@ -689,7 +692,7 @@
    5.39  lemma closure_closure [simp]: "closure (closure S) = closure S"
    5.40    unfolding closure_hull by (rule hull_hull)
    5.41  
    5.42 -lemma subset_closure: "S \<subseteq> T \<Longrightarrow> closure S \<subseteq> closure T"
    5.43 +lemma closure_mono: "S \<subseteq> T \<Longrightarrow> closure S \<subseteq> closure T"
    5.44    unfolding closure_hull by (rule hull_mono)
    5.45  
    5.46  lemma closure_minimal: "S \<subseteq> T \<Longrightarrow> closed T \<Longrightarrow> closure S \<subseteq> T"
    5.47 @@ -704,7 +707,7 @@
    5.48  lemma closure_empty [simp]: "closure {} = {}"
    5.49    using closed_empty by (rule closure_closed)
    5.50  
    5.51 -lemma closure_univ [simp]: "closure UNIV = UNIV"
    5.52 +lemma closure_UNIV [simp]: "closure UNIV = UNIV"
    5.53    using closed_UNIV by (rule closure_closed)
    5.54  
    5.55  lemma closure_union [simp]: "closure (S \<union> T) = closure S \<union> closure T"
    5.56 @@ -5990,19 +5993,4 @@
    5.57  
    5.58  declare tendsto_const [intro] (* FIXME: move *)
    5.59  
    5.60 -text {* Legacy theorem names *}
    5.61 -
    5.62 -lemmas Lim_ident_at = LIM_ident
    5.63 -lemmas Lim_const = tendsto_const
    5.64 -lemmas Lim_cmul = tendsto_scaleR [OF tendsto_const]
    5.65 -lemmas Lim_neg = tendsto_minus
    5.66 -lemmas Lim_add = tendsto_add
    5.67 -lemmas Lim_sub = tendsto_diff
    5.68 -lemmas Lim_mul = tendsto_scaleR
    5.69 -lemmas Lim_vmul = tendsto_scaleR [OF _ tendsto_const]
    5.70 -lemmas Lim_null_norm = tendsto_norm_zero_iff [symmetric]
    5.71 -lemmas Lim_linear = bounded_linear.tendsto [COMP swap_prems_rl]
    5.72 -lemmas Lim_component = tendsto_euclidean_component
    5.73 -lemmas Lim_intros = Lim_add Lim_const Lim_sub Lim_cmul Lim_vmul Lim_within_id
    5.74 -
    5.75  end