# HG changeset patch
# User huffman
# Date 1314301435 25200
# Node ID 2f7e9d890efed96a59ee0a8c12a9ba95ab305a66
# Parent  083eedb37a37fac247b7ebb4a28af8b6e74657aa
rename subset_{interior,closure} to {interior,closure}_mono;
remove some legacy theorem names;

diff -r 083eedb37a37 -r 2f7e9d890efe NEWS
--- a/NEWS	Thu Aug 25 11:57:42 2011 -0700
+++ b/NEWS	Thu Aug 25 12:43:55 2011 -0700
@@ -200,6 +200,28 @@
   tendsto_vector   ~> vec_tendstoI
   Cauchy_vector    ~> vec_CauchyI
 
+* Session Multivariate_Analysis: Several duplicate theorems have been
+removed, and other theorems have been renamed. INCOMPATIBILITY.
+
+  eventually_conjI ~> eventually_conj
+  eventually_and ~> eventually_conj_iff
+  eventually_false ~> eventually_False
+  Lim_ident_at ~> LIM_ident
+  Lim_const ~> tendsto_const
+  Lim_cmul ~> tendsto_scaleR [OF tendsto_const]
+  Lim_neg ~> tendsto_minus
+  Lim_add ~> tendsto_add
+  Lim_sub ~> tendsto_diff
+  Lim_mul ~> tendsto_scaleR
+  Lim_vmul ~> tendsto_scaleR [OF _ tendsto_const]
+  Lim_null_norm ~> tendsto_norm_zero_iff [symmetric]
+  Lim_linear ~> bounded_linear.tendsto
+  Lim_component ~> tendsto_euclidean_component
+  Lim_component_cart ~> tendsto_vec_nth
+  subset_interior ~> interior_mono
+  subset_closure ~> closure_mono
+  closure_univ ~> closure_UNIV
+
 * Complex_Main: The locale interpretations for the bounded_linear and
 bounded_bilinear locales have been removed, in order to reduce the
 number of duplicate lemmas. Users must use the original names for
@@ -213,6 +235,16 @@
   mult_right.setsum ~> setsum_right_distrib
   mult_left.diff ~> left_diff_distrib
 
+* Complex_Main: Several redundant theorems about real numbers have
+been removed or generalized and renamed. INCOMPATIBILITY.
+
+  real_0_le_divide_iff ~> zero_le_divide_iff
+  realpow_two_disj ~> power2_eq_iff
+  real_squared_diff_one_factored ~> square_diff_one_factored
+  realpow_two_diff ~> square_diff_square_factored
+  exp_ln_eq ~> ln_unique
+  lemma_DERIV_subst ~> DERIV_cong
+
 
 *** Document preparation ***
 
diff -r 083eedb37a37 -r 2f7e9d890efe src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy	Thu Aug 25 11:57:42 2011 -0700
+++ b/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy	Thu Aug 25 12:43:55 2011 -0700
@@ -2001,8 +2001,4 @@
     apply(erule_tac x=e in allE,safe) apply(rule_tac x=d in exI,safe)
     apply(erule_tac x=p in allE,safe) unfolding * norm_vector_1 by auto qed
 
-text {* Legacy theorem names *}
-
-lemmas Lim_component_cart = tendsto_vec_nth
-
 end
diff -r 083eedb37a37 -r 2f7e9d890efe src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Thu Aug 25 11:57:42 2011 -0700
+++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Thu Aug 25 12:43:55 2011 -0700
@@ -2311,7 +2311,7 @@
   fixes S :: "('n::euclidean_space) set"
   shows "closure S <= affine hull S"
 proof-
-have "closure S <= closure (affine hull S)" using subset_closure by auto
+have "closure S <= closure (affine hull S)" using closure_mono by auto
 moreover have "closure (affine hull S) = affine hull S" 
    using affine_affine_hull affine_closed[of "affine hull S"] closure_eq by auto
 ultimately show ?thesis by auto  
@@ -4047,7 +4047,7 @@
   then obtain y where "y\<in>s" and y:"norm (y - x) * (1 - e) < e * d" by auto
   def z \<equiv> "c + ((1 - e) / e) *\<^sub>R (x - y)"
   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)
-  have "z\<in>interior s" apply(rule subset_interior[OF d,unfolded subset_eq,rule_format])
+  have "z\<in>interior s" apply(rule interior_mono[OF d,unfolded subset_eq,rule_format])
     unfolding interior_open[OF open_ball] mem_ball z_def dist_norm using y and assms(4,5)
     by(auto simp add:field_simps norm_minus_commute)
   thus ?thesis unfolding * apply - apply(rule mem_interior_convex_shrink) 
@@ -4385,7 +4385,7 @@
 shows "closure(rel_interior S) = closure S"
 proof-
 have h1: "closure(rel_interior S) <= closure S" 
-   using subset_closure[of "rel_interior S" S] rel_interior_subset[of S] by auto
+   using closure_mono[of "rel_interior S" S] rel_interior_subset[of S] by auto
 { assume "S ~= {}" from this obtain a where a_def: "a : rel_interior S" 
     using rel_interior_convex_nonempty assms by auto
   { fix x assume x_def: "x : closure S"
@@ -4522,7 +4522,7 @@
 proof-
 have "?A --> ?B" by (metis assms closure_subset convex_rel_interior_closure rel_interior_subset)
 moreover have "?B --> (closure S1 <= closure S2)" 
-     by (metis assms(1) convex_closure_rel_interior subset_closure)
+     by (metis assms(1) convex_closure_rel_interior closure_mono)
 moreover have "?B --> (closure S1 >= closure S2)" by (metis closed_closure closure_minimal)
 ultimately show ?thesis by blast
 qed
@@ -4782,7 +4782,7 @@
   using convex_closure_rel_interior_inter assms by auto
 moreover have "closure (Inter {rel_interior S |S. S : I}) <= closure (Inter I)" 
     using rel_interior_inter_aux 
-          subset_closure[of "Inter {rel_interior S |S. S : I}" "Inter I"] by auto
+          closure_mono[of "Inter {rel_interior S |S. S : I}" "Inter I"] by auto
 ultimately show ?thesis using closure_inter[of I] by auto
 qed
 
@@ -4795,7 +4795,7 @@
   using convex_closure_rel_interior_inter assms by auto
 moreover have "closure (Inter {rel_interior S |S. S : I}) <= closure (Inter I)" 
     using rel_interior_inter_aux 
-          subset_closure[of "Inter {rel_interior S |S. S : I}" "Inter I"] by auto
+          closure_mono[of "Inter {rel_interior S |S. S : I}" "Inter I"] by auto
 ultimately show ?thesis using closure_inter[of I] by auto
 qed
 
@@ -4891,7 +4891,7 @@
 proof-
 have *: "S Int closure T = S" using assms by auto
 have "~(rel_interior S <= rel_frontier T)"
-     using subset_closure[of "rel_interior S" "rel_frontier T"] closed_rel_frontier[of T] 
+     using closure_mono[of "rel_interior S" "rel_frontier T"] closed_rel_frontier[of T] 
      closure_closed convex_closure_rel_interior[of S] closure_subset[of S] assms by auto
 hence "(rel_interior S) Int (rel_interior (closure T)) ~= {}" 
      using assms rel_frontier_def[of T] rel_interior_subset convex_rel_interior_closure[of T] by auto
@@ -4916,8 +4916,8 @@
 also have "... = f ` (closure (rel_interior S))" using convex_closure_rel_interior assms by auto  
 also have "... <= closure (f ` (rel_interior S))" using closure_linear_image assms by auto 
 finally have "closure (f ` S) = closure (f ` rel_interior S)"
-   using subset_closure[of "f ` S" "closure (f ` rel_interior S)"] closure_closure 
-         subset_closure[of "f ` rel_interior S" "f ` S"] * by auto
+   using closure_mono[of "f ` S" "closure (f ` rel_interior S)"] closure_closure 
+         closure_mono[of "f ` rel_interior S" "f ` S"] * by auto
 hence "rel_interior (f ` S) = rel_interior (f ` rel_interior S)" using assms convex_rel_interior
    linear_conv_bounded_linear[of f] convex_linear_image[of S] convex_linear_image[of "rel_interior S"] 
    closure_eq_rel_interior_eq[of "f ` S" "f ` rel_interior S"] by auto
diff -r 083eedb37a37 -r 2f7e9d890efe src/HOL/Multivariate_Analysis/Integration.thy
--- a/src/HOL/Multivariate_Analysis/Integration.thy	Thu Aug 25 11:57:42 2011 -0700
+++ b/src/HOL/Multivariate_Analysis/Integration.thy	Thu Aug 25 12:43:55 2011 -0700
@@ -378,7 +378,7 @@
       interior(x1 \<inter> y1) \<subseteq> interior(x1) \<Longrightarrow> interior(x1 \<inter> y1) \<subseteq> interior(y1) \<Longrightarrow>
       interior(x2 \<inter> y2) \<subseteq> interior(x2) \<Longrightarrow> interior(x2 \<inter> y2) \<subseteq> interior(y2)
       \<Longrightarrow> interior(x1 \<inter> y1) \<inter> interior(x2 \<inter> y2) = {}" by auto
-  show "interior k1 \<inter> interior k2 = {}" unfolding k1 k2 apply(rule *) defer apply(rule_tac[1-4] subset_interior)
+  show "interior k1 \<inter> interior k2 = {}" unfolding k1 k2 apply(rule *) defer apply(rule_tac[1-4] interior_mono)
     using division_ofD(5)[OF assms(1) k1(2) k2(2)]
     using division_ofD(5)[OF assms(2) k1(3) k2(3)] using th by auto qed qed
 
@@ -407,9 +407,9 @@
   show "finite (p1 \<union> p2)" using d1(1) d2(1) by auto
   show "\<Union>(p1 \<union> p2) = s1 \<union> s2" using d1(6) d2(6) by auto
   { 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 = {}"
-  { 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)]]
+  { 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)]]
       using assms(3) by blast } moreover
-  { 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)]]
+  { 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)]]
       using assms(3) by blast} ultimately
   show ?g using d1(5)[OF _ _ as(3)] and d2(5)[OF _ _ as(3)] by auto }
   fix k assume k:"k \<in> p1 \<union> p2"  show "k \<subseteq> s1 \<union> s2" using k d1(2) d2(2) by auto
@@ -573,7 +573,7 @@
         show "finite (q k - {k})" "open (interior k)"  "\<forall>t\<in>q k - {k}. \<exists>a b. t = {a..b}" using qk by auto
         show "\<forall>t\<in>q k - {k}. interior k \<inter> interior t = {}" using qk(5) using q(2)[OF k] by auto
         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}))"
-          apply(rule subset_interior *)+ using k by auto qed qed qed auto qed
+          apply(rule interior_mono *)+ using k by auto qed qed qed auto qed
 
 lemma elementary_bounded[dest]: "p division_of s \<Longrightarrow> bounded (s::('a::ordered_euclidean_space) set)"
   unfolding division_of_def by(metis bounded_Union bounded_interval) 
@@ -823,7 +823,7 @@
   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
   show "k\<subseteq>s1\<union>s2" using xk p1(3) p2(3) by blast
   fix x' k' assume xk':"(x',k')\<in>p1\<union>p2" "(x,k) \<noteq> (x',k')"
-  have *:"\<And>a b. a\<subseteq> s1 \<Longrightarrow> b\<subseteq> s2 \<Longrightarrow> interior a \<inter> interior b = {}" using assms(3) subset_interior by blast
+  have *:"\<And>a b. a\<subseteq> s1 \<Longrightarrow> b\<subseteq> s2 \<Longrightarrow> interior a \<inter> interior b = {}" using assms(3) interior_mono by blast
   show "interior k \<inter> interior k' = {}" apply(cases "(x,k)\<in>p1", case_tac[!] "(x',k')\<in>p1")
     apply(rule p1(5)) prefer 4 apply(rule *) prefer 6 apply(subst Int_commute,rule *) prefer 8 apply(rule p2(5))
     using p1(3) p2(3) using xk xk' by auto qed 
@@ -842,7 +842,7 @@
   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
   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
   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)
-    using assms(3)[rule_format] subset_interior by blast
+    using assms(3)[rule_format] interior_mono by blast
   show "interior k \<inter> interior k' = {}" apply(cases "i=i'")
     using assm(5)[OF i _ xk'(2)]  i'(2) using assm(3)[OF i] assm(3)[OF i'] defer apply-apply(rule *) by auto
 qed
@@ -1703,7 +1703,7 @@
           by(rule le_less_trans[OF norm_le_l1])
         hence "x + (\<chi>\<chi> i. if i = k then e/2 else 0) \<in> {x. x$$k = c}" using e by auto
         thus False unfolding mem_Collect_eq using e x k by auto
-      qed ultimately have "content b = 0" unfolding uv content_eq_0_interior apply-apply(drule subset_interior) by auto
+      qed ultimately have "content b = 0" unfolding uv content_eq_0_interior apply-apply(drule interior_mono) by auto
       thus "content b *\<^sub>R f a = 0" by auto
     qed auto
     also have "\<dots> < e" by(rule k d(2) p12 fine_union p1 p2)+
@@ -2563,7 +2563,7 @@
         proof(rule,rule,rule,rule,rule,rule,rule,erule conjE) fix m n u v
           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}"
           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
-          note subset_interior[OF this, unfolded division_ofD(5)[OF p'' as(1-3)] interior_inter[of "{m..n}"]]
+          note interior_mono[OF this, unfolded division_ofD(5)[OF p'' as(1-3)] interior_inter[of "{m..n}"]]
           hence "interior ({m..n} \<inter> {x. \<bar>x $$ k - c\<bar> \<le> d}) = {}" unfolding as Int_absorb by auto
           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] .
         qed qed
@@ -3516,7 +3516,7 @@
             proof- fix x k k' assume k:"( a, k) \<in> p" "( a, k') \<in> p" "content k \<noteq> 0" "content k' \<noteq> 0"
               guess v using pa[OF k(1)] .. note v = conjunctD2[OF this]
               guess v' using pa[OF k(2)] .. note v' = conjunctD2[OF this] let ?v = " (min (v) (v'))"
-              have "{ a <..< ?v} \<subseteq> k \<inter> k'" unfolding v v' by(auto simp add:) note subset_interior[OF this,unfolded interior_inter]
+              have "{ a <..< ?v} \<subseteq> k \<inter> k'" unfolding v v' by(auto simp add:) note interior_mono[OF this,unfolded interior_inter]
               moreover have " ((a + ?v)/2) \<in> { a <..< ?v}" using k(3-)
                 unfolding v v' content_eq_0 not_le by(auto simp add:not_le)
               ultimately have " ((a + ?v)/2) \<in> interior k \<inter> interior k'" unfolding interior_open[OF open_interval] by auto
@@ -3528,7 +3528,7 @@
             proof- fix x k k' assume k:"( b, k) \<in> p" "( b, k') \<in> p" "content k \<noteq> 0" "content k' \<noteq> 0"
               guess v using pb[OF k(1)] .. note v = conjunctD2[OF this]
               guess v' using pb[OF k(2)] .. note v' = conjunctD2[OF this] let ?v = " (max (v) (v'))"
-              have "{?v <..<  b} \<subseteq> k \<inter> k'" unfolding v v' by(auto simp add:) note subset_interior[OF this,unfolded interior_inter]
+              have "{?v <..<  b} \<subseteq> k \<inter> k'" unfolding v v' by(auto simp add:) note interior_mono[OF this,unfolded interior_inter]
               moreover have " ((b + ?v)/2) \<in> {?v <..<  b}" using k(3-) unfolding v v' content_eq_0 not_le by auto
               ultimately have " ((b + ?v)/2) \<in> interior k \<inter> interior k'" unfolding interior_open[OF open_interval] by auto
               hence *:"k = k'" apply- apply(rule ccontr) using p(5)[OF k(1-2)] by auto
@@ -4390,7 +4390,7 @@
     from this(2) guess u v apply-by(erule exE)+ note uv=this
     have "l\<in>snd ` p" unfolding image_iff apply(rule_tac x="(x,l)" in bexI) using as by auto
     hence "l\<in>q" "k\<in>q" "l\<noteq>k" using as(1,3) q(1) unfolding r_def by auto
-    note q'(5)[OF this] hence "interior l = {}" using subset_interior[OF `l \<subseteq> k`] by blast
+    note q'(5)[OF this] hence "interior l = {}" using interior_mono[OF `l \<subseteq> k`] by blast
     thus "content l *\<^sub>R f x = 0" unfolding uv content_eq_0_interior[THEN sym] by auto qed auto
 
   hence "norm ((\<Sum>(x, k)\<in>p. content k *\<^sub>R f x) + setsum (setsum (\<lambda>(x, k). content k *\<^sub>R f x))
@@ -4403,7 +4403,7 @@
     have *:"interior (k \<inter> l) = {}" unfolding interior_inter apply(rule q')
       using as unfolding r_def by auto
     have "interior m = {}" unfolding subset_empty[THEN sym] unfolding *[THEN sym]
-      apply(rule subset_interior) using kl(1)[OF as(4,1)] kl(1)[OF as(5,2)] by auto
+      apply(rule interior_mono) using kl(1)[OF as(4,1)] kl(1)[OF as(5,2)] by auto
     thus "content m *\<^sub>R f x = 0" unfolding uv content_eq_0_interior[THEN sym] by auto 
   qed(insert qq, auto)
 
diff -r 083eedb37a37 -r 2f7e9d890efe src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Thu Aug 25 11:57:42 2011 -0700
+++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Thu Aug 25 12:43:55 2011 -0700
@@ -588,11 +588,14 @@
 lemma interior_empty [simp]: "interior {} = {}"
   using open_empty by (rule interior_open)
 
+lemma interior_UNIV [simp]: "interior UNIV = UNIV"
+  using open_UNIV by (rule interior_open)
+
 lemma interior_interior [simp]: "interior (interior S) = interior S"
   using open_interior by (rule interior_open)
 
-lemma subset_interior: "S \<subseteq> T \<Longrightarrow> interior S \<subseteq> interior T"
-  by (auto simp add: interior_def) (* TODO: rename to interior_mono *)
+lemma interior_mono: "S \<subseteq> T \<Longrightarrow> interior S \<subseteq> interior T"
+  by (auto simp add: interior_def)
 
 lemma interior_unique:
   assumes "T \<subseteq> S" and "open T"
@@ -601,7 +604,7 @@
   by (intro equalityI assms interior_subset open_interior interior_maximal)
 
 lemma interior_inter [simp]: "interior (S \<inter> T) = interior S \<inter> interior T"
-  by (intro equalityI Int_mono Int_greatest subset_interior Int_lower1
+  by (intro equalityI Int_mono Int_greatest interior_mono Int_lower1
     Int_lower2 interior_maximal interior_subset open_Int open_interior)
 
 lemma mem_interior: "x \<in> interior S \<longleftrightarrow> (\<exists>e>0. ball x e \<subseteq> S)"
@@ -623,7 +626,7 @@
   shows "interior (S \<union> T) = interior S"
 proof
   show "interior S \<subseteq> interior (S \<union> T)"
-    by (rule subset_interior, rule Un_upper1)
+    by (rule interior_mono, rule Un_upper1)
 next
   show "interior (S \<union> T) \<subseteq> interior S"
   proof
@@ -689,7 +692,7 @@
 lemma closure_closure [simp]: "closure (closure S) = closure S"
   unfolding closure_hull by (rule hull_hull)
 
-lemma subset_closure: "S \<subseteq> T \<Longrightarrow> closure S \<subseteq> closure T"
+lemma closure_mono: "S \<subseteq> T \<Longrightarrow> closure S \<subseteq> closure T"
   unfolding closure_hull by (rule hull_mono)
 
 lemma closure_minimal: "S \<subseteq> T \<Longrightarrow> closed T \<Longrightarrow> closure S \<subseteq> T"
@@ -704,7 +707,7 @@
 lemma closure_empty [simp]: "closure {} = {}"
   using closed_empty by (rule closure_closed)
 
-lemma closure_univ [simp]: "closure UNIV = UNIV"
+lemma closure_UNIV [simp]: "closure UNIV = UNIV"
   using closed_UNIV by (rule closure_closed)
 
 lemma closure_union [simp]: "closure (S \<union> T) = closure S \<union> closure T"
@@ -5990,19 +5993,4 @@
 
 declare tendsto_const [intro] (* FIXME: move *)
 
-text {* Legacy theorem names *}
-
-lemmas Lim_ident_at = LIM_ident
-lemmas Lim_const = tendsto_const
-lemmas Lim_cmul = tendsto_scaleR [OF tendsto_const]
-lemmas Lim_neg = tendsto_minus
-lemmas Lim_add = tendsto_add
-lemmas Lim_sub = tendsto_diff
-lemmas Lim_mul = tendsto_scaleR
-lemmas Lim_vmul = tendsto_scaleR [OF _ tendsto_const]
-lemmas Lim_null_norm = tendsto_norm_zero_iff [symmetric]
-lemmas Lim_linear = bounded_linear.tendsto [COMP swap_prems_rl]
-lemmas Lim_component = tendsto_euclidean_component
-lemmas Lim_intros = Lim_add Lim_const Lim_sub Lim_cmul Lim_vmul Lim_within_id
-
 end