--- a/src/HOL/Library/Convex_Euclidean_Space.thy Thu Jun 11 10:37:02 2009 -0700
+++ b/src/HOL/Library/Convex_Euclidean_Space.thy Thu Jun 11 11:51:12 2009 -0700
@@ -1217,7 +1217,8 @@
unfolding open_vector_def all_1
by (auto simp add: dest_vec1_def)
-lemma tendsto_dest_vec1: "(f ---> l) net \<Longrightarrow> ((\<lambda>x. dest_vec1 (f x)) ---> dest_vec1 l) net"
+lemma tendsto_dest_vec1 [tendsto_intros]:
+ "(f ---> l) net \<Longrightarrow> ((\<lambda>x. dest_vec1 (f x)) ---> dest_vec1 l) net"
unfolding tendsto_def
apply clarify
apply (drule_tac x="dest_vec1 -` S" in spec)
@@ -1276,19 +1277,13 @@
apply (rule_tac x=u in rev_bexI, simp)
apply (erule rev_bexI, erule rev_bexI, simp)
by auto
- { fix u::"real" fix x y assume as:"0 \<le> u" "u \<le> 1" "x \<in> s" "y \<in> t"
- hence "continuous (at (u, x, y))
- (\<lambda>z. fst (snd z) - fst z *s fst (snd z) + fst z *s snd (snd z))"
- apply (auto intro!: continuous_add continuous_sub continuous_mul)
- unfolding continuous_at
- by (safe intro!: tendsto_fst tendsto_snd Lim_at_id [unfolded id_def])
- }
- hence "continuous_on ({0..1} \<times> s \<times> t)
+ have "continuous_on ({0..1} \<times> s \<times> t)
(\<lambda>z. (1 - fst z) *s fst (snd z) + fst z *s snd (snd z))"
- apply(rule_tac continuous_at_imp_continuous_on) by auto
- thus ?thesis unfolding * apply(rule compact_continuous_image)
- defer apply(rule compact_Times) defer apply(rule compact_Times)
- using compact_real_interval assms by auto
+ unfolding continuous_on by (rule ballI) (intro tendsto_intros)
+ thus ?thesis unfolding *
+ apply (rule compact_continuous_image)
+ apply (intro compact_Times compact_real_interval assms)
+ done
qed
lemma compact_convex_hull: fixes s::"(real^'n::finite) set"
--- a/src/HOL/Library/Product_Vector.thy Thu Jun 11 10:37:02 2009 -0700
+++ b/src/HOL/Library/Product_Vector.thy Thu Jun 11 11:51:12 2009 -0700
@@ -177,7 +177,7 @@
lemma dist_snd_le: "dist (snd x) (snd y) \<le> dist x y"
unfolding dist_prod_def by simp
-lemma tendsto_fst:
+lemma tendsto_fst [tendsto_intros]:
assumes "(f ---> a) net"
shows "((\<lambda>x. fst (f x)) ---> fst a) net"
proof (rule topological_tendstoI)
@@ -196,7 +196,7 @@
by simp
qed
-lemma tendsto_snd:
+lemma tendsto_snd [tendsto_intros]:
assumes "(f ---> a) net"
shows "((\<lambda>x. snd (f x)) ---> snd a) net"
proof (rule topological_tendstoI)
@@ -215,7 +215,7 @@
by simp
qed
-lemma tendsto_Pair:
+lemma tendsto_Pair [tendsto_intros]:
assumes "(f ---> a) net" and "(g ---> b) net"
shows "((\<lambda>x. (f x, g x)) ---> (a, b)) net"
proof (rule topological_tendstoI)
--- a/src/HOL/Library/Topology_Euclidean_Space.thy Thu Jun 11 10:37:02 2009 -0700
+++ b/src/HOL/Library/Topology_Euclidean_Space.thy Thu Jun 11 11:51:12 2009 -0700
@@ -1274,39 +1274,6 @@
shows "(f ---> l) net \<Longrightarrow> (g ---> m) net \<Longrightarrow> ((\<lambda>x. f(x) - g(x)) ---> l - m) net"
by (rule tendsto_diff)
-lemma dist_triangle3: (* TODO: move *)
- fixes x y :: "'a::metric_space"
- shows "dist x y \<le> dist a x + dist a y"
-using dist_triangle2 [of x y a]
-by (simp add: dist_commute)
-
-lemma tendsto_dist: (* TODO: move *)
- assumes f: "(f ---> l) net" and g: "(g ---> m) net"
- shows "((\<lambda>x. dist (f x) (g x)) ---> dist l m) net"
-proof (rule tendstoI)
- fix e :: real assume "0 < e"
- hence e2: "0 < e/2" by simp
- from tendstoD [OF f e2] tendstoD [OF g e2]
- show "eventually (\<lambda>x. dist (dist (f x) (g x)) (dist l m) < e) net"
- proof (rule eventually_elim2)
- fix x assume x: "dist (f x) l < e/2" "dist (g x) m < e/2"
- have "dist (f x) (g x) - dist l m \<le> dist (f x) l + dist (g x) m"
- using dist_triangle2 [of "f x" "g x" "l"]
- using dist_triangle2 [of "g x" "l" "m"]
- by arith
- moreover
- have "dist l m - dist (f x) (g x) \<le> dist (f x) l + dist (g x) m"
- using dist_triangle3 [of "l" "m" "f x"]
- using dist_triangle [of "f x" "m" "g x"]
- by arith
- ultimately
- have "dist (dist (f x) (g x)) (dist l m) \<le> dist (f x) l + dist (g x) m"
- unfolding dist_norm real_norm_def by arith
- with x show "dist (dist (f x) (g x)) (dist l m) < e"
- by arith
- qed
-qed
-
lemma Lim_null:
fixes f :: "'a \<Rightarrow> 'b::real_normed_vector"
shows "(f ---> l) net \<longleftrightarrow> ((\<lambda>x. f(x) - l) ---> 0) net" by (simp add: Lim dist_norm)
@@ -4265,7 +4232,7 @@
subsection{* We can now extend limit compositions to consider the scalar multiplier. *}
-lemma Lim_mul:
+lemma Lim_mul [tendsto_intros]:
fixes f :: "'a \<Rightarrow> real ^ _"
assumes "(c ---> d) net" "(f ---> l) net"
shows "((\<lambda>x. c(x) *s f x) ---> (d *s l)) net"
--- a/src/HOL/Limits.thy Thu Jun 11 10:37:02 2009 -0700
+++ b/src/HOL/Limits.thy Thu Jun 11 11:51:12 2009 -0700
@@ -358,6 +358,14 @@
where [code del]:
"(f ---> l) net \<longleftrightarrow> (\<forall>S. open S \<longrightarrow> l \<in> S \<longrightarrow> eventually (\<lambda>x. f x \<in> S) net)"
+ML{*
+structure TendstoIntros =
+ NamedThmsFun(val name = "tendsto_intros"
+ val description = "introduction rules for tendsto");
+*}
+
+setup TendstoIntros.setup
+
lemma topological_tendstoI:
"(\<And>S. open S \<Longrightarrow> l \<in> S \<Longrightarrow> eventually (\<lambda>x. f x \<in> S) net)
\<Longrightarrow> (f ---> l) net"
@@ -395,12 +403,38 @@
lemma tendsto_Zfun_iff: "(f ---> a) net = Zfun (\<lambda>x. f x - a) net"
by (simp only: tendsto_iff Zfun_def dist_norm)
-lemma tendsto_const: "((\<lambda>x. k) ---> k) net"
+lemma tendsto_ident_at [tendsto_intros]: "((\<lambda>x. x) ---> a) (at a)"
+unfolding tendsto_def eventually_at_topological by auto
+
+lemma tendsto_ident_at_within [tendsto_intros]:
+ "a \<in> S \<Longrightarrow> ((\<lambda>x. x) ---> a) (at a within S)"
+unfolding tendsto_def eventually_within eventually_at_topological by auto
+
+lemma tendsto_const [tendsto_intros]: "((\<lambda>x. k) ---> k) net"
by (simp add: tendsto_def)
-lemma tendsto_norm:
- fixes a :: "'a::real_normed_vector"
- shows "(f ---> a) net \<Longrightarrow> ((\<lambda>x. norm (f x)) ---> norm a) net"
+lemma tendsto_dist [tendsto_intros]:
+ assumes f: "(f ---> l) net" and g: "(g ---> m) net"
+ shows "((\<lambda>x. dist (f x) (g x)) ---> dist l m) net"
+proof (rule tendstoI)
+ fix e :: real assume "0 < e"
+ hence e2: "0 < e/2" by simp
+ from tendstoD [OF f e2] tendstoD [OF g e2]
+ show "eventually (\<lambda>x. dist (dist (f x) (g x)) (dist l m) < e) net"
+ proof (rule eventually_elim2)
+ fix x assume "dist (f x) l < e/2" "dist (g x) m < e/2"
+ then show "dist (dist (f x) (g x)) (dist l m) < e"
+ unfolding dist_real_def
+ using dist_triangle2 [of "f x" "g x" "l"]
+ using dist_triangle2 [of "g x" "l" "m"]
+ using dist_triangle3 [of "l" "m" "f x"]
+ using dist_triangle [of "f x" "m" "g x"]
+ by arith
+ qed
+qed
+
+lemma tendsto_norm [tendsto_intros]:
+ "(f ---> a) net \<Longrightarrow> ((\<lambda>x. norm (f x)) ---> norm a) net"
apply (simp add: tendsto_iff dist_norm, safe)
apply (drule_tac x="e" in spec, safe)
apply (erule eventually_elim1)
@@ -417,12 +451,12 @@
shows "(- a) - (- b) = - (a - b)"
by simp
-lemma tendsto_add:
+lemma tendsto_add [tendsto_intros]:
fixes a b :: "'a::real_normed_vector"
shows "\<lbrakk>(f ---> a) net; (g ---> b) net\<rbrakk> \<Longrightarrow> ((\<lambda>x. f x + g x) ---> a + b) net"
by (simp only: tendsto_Zfun_iff add_diff_add Zfun_add)
-lemma tendsto_minus:
+lemma tendsto_minus [tendsto_intros]:
fixes a :: "'a::real_normed_vector"
shows "(f ---> a) net \<Longrightarrow> ((\<lambda>x. - f x) ---> - a) net"
by (simp only: tendsto_Zfun_iff minus_diff_minus Zfun_minus)
@@ -432,16 +466,16 @@
shows "((\<lambda>x. - f x) ---> - a) net \<Longrightarrow> (f ---> a) net"
by (drule tendsto_minus, simp)
-lemma tendsto_diff:
+lemma tendsto_diff [tendsto_intros]:
fixes a b :: "'a::real_normed_vector"
shows "\<lbrakk>(f ---> a) net; (g ---> b) net\<rbrakk> \<Longrightarrow> ((\<lambda>x. f x - g x) ---> a - b) net"
by (simp add: diff_minus tendsto_add tendsto_minus)
-lemma (in bounded_linear) tendsto:
+lemma (in bounded_linear) tendsto [tendsto_intros]:
"(g ---> a) net \<Longrightarrow> ((\<lambda>x. f (g x)) ---> f a) net"
by (simp only: tendsto_Zfun_iff diff [symmetric] Zfun)
-lemma (in bounded_bilinear) tendsto:
+lemma (in bounded_bilinear) tendsto [tendsto_intros]:
"\<lbrakk>(f ---> a) net; (g ---> b) net\<rbrakk> \<Longrightarrow> ((\<lambda>x. f x ** g x) ---> a ** b) net"
by (simp only: tendsto_Zfun_iff prod_diff_prod
Zfun_add Zfun Zfun_left Zfun_right)
@@ -556,7 +590,7 @@
apply (simp add: tendsto_Zfun_iff)
done
-lemma tendsto_inverse:
+lemma tendsto_inverse [tendsto_intros]:
fixes a :: "'a::real_normed_div_algebra"
assumes f: "(f ---> a) net"
assumes a: "a \<noteq> 0"
@@ -571,7 +605,7 @@
by (rule tendsto_inverse_lemma)
qed
-lemma tendsto_divide:
+lemma tendsto_divide [tendsto_intros]:
fixes a b :: "'a::real_normed_field"
shows "\<lbrakk>(f ---> a) net; (g ---> b) net; b \<noteq> 0\<rbrakk>
\<Longrightarrow> ((\<lambda>x. f x / g x) ---> a / b) net"
--- a/src/HOL/RealVector.thy Thu Jun 11 10:37:02 2009 -0700
+++ b/src/HOL/RealVector.thy Thu Jun 11 11:51:12 2009 -0700
@@ -530,6 +530,9 @@
lemma dist_triangle: "dist x z \<le> dist x y + dist y z"
using dist_triangle2 [of x z y] by (simp add: dist_commute)
+lemma dist_triangle3: "dist x y \<le> dist a x + dist a y"
+using dist_triangle2 [of x y a] by (simp add: dist_commute)
+
subclass topological_space
proof
have "\<exists>e::real. 0 < e"