# HG changeset patch
# User huffman
# Date 1244746272 25200
# Node ID da5a5589418e176505f70f90c958e9a2326eb80b
# Parent  d2abf6f6f619b087e98096cd147259adff4ae783
theorem attribute [tendsto_intros]

diff -r d2abf6f6f619 -r da5a5589418e src/HOL/Library/Convex_Euclidean_Space.thy
--- 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"
diff -r d2abf6f6f619 -r da5a5589418e src/HOL/Library/Product_Vector.thy
--- 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)
diff -r d2abf6f6f619 -r da5a5589418e src/HOL/Library/Topology_Euclidean_Space.thy
--- 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"
diff -r d2abf6f6f619 -r da5a5589418e src/HOL/Limits.thy
--- 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"
diff -r d2abf6f6f619 -r da5a5589418e src/HOL/RealVector.thy
--- 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"