author huffman Thu, 11 Jun 2009 11:51:12 -0700 changeset 31565 da5a5589418e parent 31564 d2abf6f6f619 child 31566 eff95000aae7
theorem attribute [tendsto_intros]
 src/HOL/Library/Convex_Euclidean_Space.thy file | annotate | diff | comparison | revisions src/HOL/Library/Product_Vector.thy file | annotate | diff | comparison | revisions src/HOL/Library/Topology_Euclidean_Space.thy file | annotate | diff | comparison | revisions src/HOL/Limits.thy file | annotate | diff | comparison | revisions src/HOL/RealVector.thy file | annotate | diff | comparison | revisions
--- 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

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"

-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"

-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"