rename subset_{interior,closure} to {interior,closure}_mono;
remove some legacy theorem names;
--- 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 ***
--- 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
--- 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
--- 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)
--- 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