# HG changeset patch
# User huffman
# Date 1243631398 25200
# Node ID 9983f648f9bbaba759b8845da272e33cbde67817
# Parent  b7941738e3a1cbc9d2886a87d0ea62593cab3f58
generalize tendsto and related constants to class metric_space

diff -r b7941738e3a1 -r 9983f648f9bb src/HOL/Library/Topology_Euclidean_Space.thy
--- a/src/HOL/Library/Topology_Euclidean_Space.thy	Fri May 29 10:31:35 2009 -0700
+++ b/src/HOL/Library/Topology_Euclidean_Space.thy	Fri May 29 14:09:58 2009 -0700
@@ -1161,7 +1161,7 @@
 
 subsection{* Limits, defined as vacuously true when the limit is trivial. *}
 
-definition tendsto:: "('a \<Rightarrow> real ^'n::finite) \<Rightarrow> real ^'n \<Rightarrow> 'a net \<Rightarrow> bool" (infixr "--->" 55) where
+definition tendsto:: "('a \<Rightarrow> 'b::metric_space) \<Rightarrow> 'b \<Rightarrow> 'a net \<Rightarrow> bool" (infixr "--->" 55) where
   tendsto_def: "(f ---> l) net  \<longleftrightarrow> (\<forall>e>0. eventually (\<lambda>x. dist (f x) l < e) net)"
 
 lemma tendstoD: "(f ---> l) net \<Longrightarrow> e>0 \<Longrightarrow> eventually (\<lambda>x. dist (f x) l < e) net"
@@ -1325,19 +1325,23 @@
 lemma Lim_const: "((\<lambda>x. a) ---> a) net"
   by (auto simp add: Lim trivial_limit_def)
 
-lemma Lim_cmul: "(f ---> l) net ==> ((\<lambda>x. c *s f x) ---> c *s l) net"
+lemma Lim_cmul:
+  fixes f :: "'a \<Rightarrow> real ^ 'n::finite"
+  shows "(f ---> l) net ==> ((\<lambda>x. c *s f x) ---> c *s l) net"
   apply (rule Lim_linear[where f = f])
   apply simp
   apply (rule linear_compose_cmul)
   apply (rule linear_id[unfolded id_def])
   done
 
-lemma Lim_neg: "(f ---> l) net ==> ((\<lambda>x. -(f x)) ---> -l) net"
+lemma Lim_neg:
+  fixes f :: "'a \<Rightarrow> 'b::real_normed_vector"
+  shows "(f ---> l) net ==> ((\<lambda>x. -(f x)) ---> -l) net"
   apply (simp add: Lim dist_norm  group_simps)
   apply (subst minus_diff_eq[symmetric])
   unfolding norm_minus_cancel by simp
 
-lemma Lim_add: fixes f :: "'a \<Rightarrow> real^'n::finite" shows
+lemma Lim_add: fixes f :: "'a \<Rightarrow> 'b::real_normed_vector" shows
  "(f ---> l) net \<Longrightarrow> (g ---> m) net \<Longrightarrow> ((\<lambda>x. f(x) + g(x)) ---> l + m) net"
 proof-
   assume as:"(f ---> l) net" "(g ---> m) net"
@@ -1366,15 +1370,23 @@
   thus ?thesis unfolding tendsto_def by auto
 qed
 
-lemma Lim_sub: "(f ---> l) net \<Longrightarrow> (g ---> m) net \<Longrightarrow> ((\<lambda>x. f(x) - g(x)) ---> l - m) net"
+lemma Lim_sub:
+  fixes f :: "'a \<Rightarrow> 'b::real_normed_vector"
+  shows "(f ---> l) net \<Longrightarrow> (g ---> m) net \<Longrightarrow> ((\<lambda>x. f(x) - g(x)) ---> l - m) net"
   unfolding diff_minus
   by (simp add: Lim_add Lim_neg)
 
-lemma Lim_null: "(f ---> l) net \<longleftrightarrow> ((\<lambda>x. f(x) - l) ---> 0) net" by (simp add: Lim dist_norm)
-lemma Lim_null_norm: "(f ---> 0) net \<longleftrightarrow> ((\<lambda>x. vec1(norm(f x))) ---> 0) net"
+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)
+
+lemma Lim_null_norm:
+  fixes f :: "'a \<Rightarrow> 'b::real_normed_vector"
+  shows "(f ---> 0) net \<longleftrightarrow> ((\<lambda>x. vec1(norm(f x))) ---> 0) net"
   by (simp add: Lim dist_norm norm_vec1)
 
 lemma Lim_null_comparison:
+  fixes f :: "'a \<Rightarrow> 'b::real_normed_vector"
   assumes "eventually (\<lambda>x. norm(f x) <= g x) net" "((\<lambda>x. vec1(g x)) ---> 0) net"
   shows "(f ---> 0) net"
 proof(simp add: tendsto_def, rule+)
@@ -1403,13 +1415,15 @@
   by auto
 
 lemma Lim_transform_bound:
+  fixes f :: "'a \<Rightarrow> 'b::real_normed_vector"
+  fixes g :: "'a \<Rightarrow> 'c::real_normed_vector"
   assumes "eventually (\<lambda>n. norm(f n) <= norm(g n)) net"  "(g ---> 0) net"
   shows "(f ---> 0) net"
 proof(simp add: tendsto_def, rule+)
   fix e::real assume "e>0"
   { fix x
     assume "norm (f x) \<le> norm (g x)" "dist (g x) 0 < e"
-    hence "dist (f x) 0 < e" by norm}
+    hence "dist (f x) 0 < e" by (simp add: dist_norm)}
   thus "eventually (\<lambda>x. dist (f x) 0 < e) net"
     using eventually_and[of "\<lambda>x. norm (f x) \<le> norm (g x)" "\<lambda>x. dist (g x) 0 < e" net]
     using eventually_mono[of "\<lambda>x. norm (f x) \<le> norm (g x) \<and> dist (g x) 0 < e" "\<lambda>x. dist (f x) 0 < e" net]
@@ -1438,6 +1452,7 @@
 text{* Need to prove closed(cball(x,e)) before deducing this as a corollary. *}
 
 lemma Lim_norm_ubound:
+  fixes f :: "'a \<Rightarrow> 'b::real_normed_vector"
   assumes "\<not>(trivial_limit net)" "(f ---> l) net" "eventually (\<lambda>x. norm(f x) <= e) net"
   shows "norm(l) <= e"
 proof-
@@ -1449,11 +1464,15 @@
       using assms(2)[unfolded Lim] using assms(1) apply simp apply(erule_tac x="norm l - e" in allE) by auto
     obtain w where w:"netord net w z"  "netord net w y" using net[of net] using z(1) y(1) by blast
     hence "dist (f w) l < norm l - e \<and> norm (f w) <= e" using z(2) y(2) by auto
-    thus False using `\<not> norm l \<le> e` by norm
+    hence "norm (f w - l) < norm l - e" "norm (f w) \<le> e" by (simp_all add: dist_norm)
+    hence "norm (f w - l) + norm (f w) < norm l" by simp
+    hence "norm (f w - l - f w) < norm l" by (rule le_less_trans [OF norm_triangle_ineq4])
+    thus False using `\<not> norm l \<le> e` by simp
   qed
 qed
 
 lemma Lim_norm_lbound:
+  fixes f :: "'a \<Rightarrow> 'b::real_normed_vector"
   assumes "\<not> (trivial_limit net)"  "(f ---> l) net"  "eventually (\<lambda>x. e <= norm(f x)) net"
   shows "e \<le> norm l"
 proof-
@@ -1465,7 +1484,10 @@
       using assms(2)[unfolded Lim] using assms(1) apply simp apply(erule_tac x="e - norm l" in allE) by auto
     obtain w where w:"netord net w z"  "netord net w y" using net[of net] using z(1) y(1) by blast
     hence "dist (f w) l < e - norm l \<and> e \<le> norm (f w)" using z(2) y(2) by auto
-    thus False using `\<not> e \<le> norm l` by norm
+    hence "norm (f w - l) + norm l < e" "e \<le> norm (f w)" by (simp_all add: dist_norm)
+    hence "norm (f w - l) + norm l < norm (f w)" by (rule less_le_trans)
+    hence "norm (f w - l + l) < norm (f w)" by (rule le_less_trans [OF norm_triangle_ineq])
+    thus False by simp
   qed
 qed
 
@@ -1488,7 +1510,8 @@
 qed
 
 lemma tendsto_Lim:
- "~(trivial_limit (net::('b::zero_neq_one net))) \<Longrightarrow> (f ---> l) net ==> Lim net f = l"
+  fixes f :: "'a::zero_neq_one \<Rightarrow> real ^ 'n::finite"
+  shows "~(trivial_limit net) \<Longrightarrow> (f ---> l) net ==> Lim net f = l"
   unfolding Lim_def using Lim_unique[of net f] by auto
 
 text{* Limit under bilinear function (surprisingly tedious, but important) *}
@@ -1614,17 +1637,22 @@
 
 text{* Transformation of limit. *}
 
-lemma Lim_transform: assumes "((\<lambda>x. f x - g x) ---> 0) net" "(f ---> l) net"
+lemma Lim_transform:
+  fixes f g :: "'a::type \<Rightarrow> 'b::real_normed_vector"
+  assumes "((\<lambda>x. f x - g x) ---> 0) net" "(f ---> l) net"
   shows "(g ---> l) net"
 proof-
   from assms have "((\<lambda>x. f x - g x - f x) ---> 0 - l) net" using Lim_sub[of "\<lambda>x. f x - g x" 0 net f l] by auto
   thus "?thesis" using Lim_neg [of "\<lambda> x. - g x" "-l" net] by auto
 qed
 
-lemma Lim_transform_eventually:  "eventually (\<lambda>x. f x = g x) net \<Longrightarrow> (f ---> l) net ==> (g ---> l) net"
+lemma Lim_transform_eventually:
+  fixes f g :: "'a::type \<Rightarrow> 'b::real_normed_vector"
+  shows "eventually (\<lambda>x. f x = g x) net \<Longrightarrow> (f ---> l) net ==> (g ---> l) net"
   using Lim_eventually[of "\<lambda>x. f x - g x" 0 net] Lim_transform[of f g net l] by auto
 
 lemma Lim_transform_within:
+  fixes f g :: "real ^ 'n::finite \<Rightarrow> 'b::real_normed_vector"
   fixes x :: "real ^ 'n::finite"
   assumes "0 < d" "(\<forall>x'\<in>S. 0 < dist x' x \<and> dist x' x < d \<longrightarrow> f x' = g x')"
           "(f ---> l) (at x within S)"
@@ -1634,7 +1662,9 @@
   thus ?thesis using Lim_transform[of f g "at x within S" l] using assms(3) by auto
 qed
 
-lemma Lim_transform_at: "0 < d \<Longrightarrow> (\<forall>x'. 0 < dist x' x \<and> dist x' x < d \<longrightarrow> f x' = g x') \<Longrightarrow>
+lemma Lim_transform_at:
+  fixes f g :: "real ^ 'n::finite \<Rightarrow> 'b::real_normed_vector"
+  shows "0 < d \<Longrightarrow> (\<forall>x'. 0 < dist x' x \<and> dist x' x < d \<longrightarrow> f x' = g x') \<Longrightarrow>
   (f ---> l) (at x) ==> (g ---> l) (at x)"
   apply (subst within_UNIV[symmetric])
   using Lim_transform_within[of d UNIV x f g l]
@@ -1643,7 +1673,7 @@
 text{* Common case assuming being away from some crucial point like 0. *}
 
 lemma Lim_transform_away_within:
-  fixes f:: "real ^'m::finite \<Rightarrow> real ^'n::finite"
+  fixes f:: "real ^'m::finite \<Rightarrow> 'b::real_normed_vector"
   assumes "a\<noteq>b" "\<forall>x\<in> S. x \<noteq> a \<and> x \<noteq> b \<longrightarrow> f x = g x"
   and "(f ---> l) (at a within S)"
   shows "(g ---> l) (at a within S)"
@@ -1654,7 +1684,7 @@
 qed
 
 lemma Lim_transform_away_at:
-  fixes f:: "real ^'m::finite \<Rightarrow> real ^'n::finite"
+  fixes f:: "real ^'m::finite \<Rightarrow> 'b::real_normed_vector"
   assumes ab: "a\<noteq>b" and fg: "\<forall>x. x \<noteq> a \<and> x \<noteq> b \<longrightarrow> f x = g x"
   and fl: "(f ---> l) (at a)"
   shows "(g ---> l) (at a)"
@@ -1664,7 +1694,7 @@
 text{* Alternatively, within an open set. *}
 
 lemma Lim_transform_within_open:
-  fixes f:: "real ^'m::finite \<Rightarrow> real ^'n::finite"
+  fixes f:: "real ^'m::finite \<Rightarrow> 'b::real_normed_vector"
   assumes "open S"  "a \<in> S"  "\<forall>x\<in>S. x \<noteq> a \<longrightarrow> f x = g x"  "(f ---> l) (at a)"
   shows "(g ---> l) (at a)"
 proof-
@@ -2385,7 +2415,9 @@
   thus ?lhs unfolding complete_def by auto
 qed
 
-lemma convergent_eq_cauchy: "(\<exists>l. (s ---> l) sequentially) \<longleftrightarrow> Cauchy s" (is "?lhs = ?rhs")
+lemma convergent_eq_cauchy:
+  fixes s :: "nat \<Rightarrow> real ^ 'n::finite"
+  shows "(\<exists>l. (s ---> l) sequentially) \<longleftrightarrow> Cauchy s" (is "?lhs = ?rhs")
 proof
   assume ?lhs then obtain l where "(s ---> l) sequentially" by auto
   thus ?rhs using convergent_imp_cauchy by auto
@@ -3170,6 +3202,7 @@
 text{* The usual transformation theorems. *}
 
 lemma continuous_transform_within:
+  fixes f g :: "real ^ 'n::finite \<Rightarrow> 'b::real_normed_vector"
   assumes "0 < d" "x \<in> s" "\<forall>x' \<in> s. dist x' x < d --> f x' = g x'"
           "continuous (at x within s) f"
   shows "continuous (at x within s) g"
@@ -3185,6 +3218,7 @@
 qed
 
 lemma continuous_transform_at:
+  fixes f g :: "real ^ 'n::finite \<Rightarrow> 'b::real_normed_vector"
   assumes "0 < d" "\<forall>x'. dist x' x < d --> f x' = g x'"
           "continuous (at x) f"
   shows "continuous (at x) g"
@@ -3204,25 +3238,27 @@
 text{* Combination results for pointwise continuity. *}
 
 lemma continuous_const: "continuous net (\<lambda>x::'a::zero_neq_one. c)"
-  by(auto simp add: continuous_def Lim_const)
+  by (auto simp add: continuous_def Lim_const)
 
 lemma continuous_cmul:
- "continuous net f ==> continuous net (\<lambda>x. c *s f x)"
- by(auto simp add: continuous_def Lim_cmul)
+  fixes f :: "'a \<Rightarrow> real ^ 'n::finite"
+  shows "continuous net f ==> continuous net (\<lambda>x. c *s f x)"
+  by (auto simp add: continuous_def Lim_cmul)
 
 lemma continuous_neg:
- "continuous net f ==> continuous net (\<lambda>x. -(f x))"
- by(auto simp add: continuous_def Lim_neg)
+  fixes f :: "'a \<Rightarrow> 'b::real_normed_vector"
+  shows "continuous net f ==> continuous net (\<lambda>x. -(f x))"
+  by (auto simp add: continuous_def Lim_neg)
 
 lemma continuous_add:
- "continuous net f \<Longrightarrow> continuous net g
-           ==> continuous net (\<lambda>x. f x + g x)"
- by(auto simp add: continuous_def Lim_add)
+  fixes f g :: "'a \<Rightarrow> 'b::real_normed_vector"
+  shows "continuous net f \<Longrightarrow> continuous net g \<Longrightarrow> continuous net (\<lambda>x. f x + g x)"
+  by (auto simp add: continuous_def Lim_add)
 
 lemma continuous_sub:
- "continuous net f \<Longrightarrow> continuous net g
-           ==> continuous net (\<lambda>x. f(x) - g(x))"
- by(auto simp add: continuous_def Lim_sub)
+  fixes f g :: "'a \<Rightarrow> 'b::real_normed_vector"
+  shows "continuous net f \<Longrightarrow> continuous net g \<Longrightarrow> continuous net (\<lambda>x. f x - g x)"
+  by (auto simp add: continuous_def Lim_sub)
 
 text{* Same thing for setwise continuity. *}
 
@@ -3776,12 +3812,14 @@
 text{* Also bilinear functions, in composition form.                             *}
 
 lemma bilinear_continuous_at_compose:
- "continuous (at x) f \<Longrightarrow> continuous (at x) g \<Longrightarrow> bilinear h
+  fixes f :: "real ^ _ \<Rightarrow> real ^ _"
+  shows "continuous (at x) f \<Longrightarrow> continuous (at x) g \<Longrightarrow> bilinear h
         ==> continuous (at x) (\<lambda>x. h (f x) (g x))"
   unfolding continuous_at using Lim_bilinear[of f "f x" "(at x)" g "g x" h] by auto
 
 lemma bilinear_continuous_within_compose:
- "continuous (at x within s) f \<Longrightarrow> continuous (at x within s) g \<Longrightarrow> bilinear h
+  fixes f :: "real ^ _ \<Rightarrow> real ^ _"
+  shows "continuous (at x within s) f \<Longrightarrow> continuous (at x within s) g \<Longrightarrow> bilinear h
         ==> continuous (at x within s) (\<lambda>x. h (f x) (g x))"
   unfolding continuous_within using Lim_bilinear[of f "f x"] by auto
 
@@ -3812,7 +3850,8 @@
   unfolding dist_vec1 vec1_in_image_vec1 abs_minus_commute by auto
 
 lemma continuous_at_vec1_range:
- "continuous (at x) (vec1 o f) \<longleftrightarrow> (\<forall>e>0. \<exists>d>0.
+  fixes f :: "real ^ _ \<Rightarrow> real"
+  shows "continuous (at x) (vec1 o f) \<longleftrightarrow> (\<forall>e>0. \<exists>d>0.
         \<forall>x'. norm(x' - x) < d --> abs(f x' - f x) < e)"
   unfolding continuous_at unfolding Lim_at apply simp unfolding dist_vec1 unfolding dist_nz[THEN sym] unfolding dist_norm apply auto
   apply(erule_tac x=e in allE) apply auto apply (rule_tac x=d in exI) apply auto apply (erule_tac x=x' in allE) apply auto
@@ -3937,6 +3976,7 @@
 subsection{* We can now extend limit compositions to consider the scalar multiplier.   *}
 
 lemma Lim_mul:
+  fixes f :: "'a \<Rightarrow> real ^ _"
   assumes "((vec1 o c) ---> vec1 d) net"  "(f ---> l) net"
   shows "((\<lambda>x. c(x) *s f x) ---> (d *s l)) net"
 proof-
@@ -3947,15 +3987,18 @@
 qed
 
 lemma Lim_vmul:
- "((vec1 o c) ---> vec1 d) net ==> ((\<lambda>x. c(x) *s v) ---> d *s v) net"
+  fixes c :: "'a \<Rightarrow> real"
+  shows "((vec1 o c) ---> vec1 d) net ==> ((\<lambda>x. c(x) *s v) ---> d *s v) net"
   using Lim_mul[of c d net "\<lambda>x. v" v] using Lim_const[of v] by auto
 
 lemma continuous_vmul:
- "continuous net (vec1 o c) ==> continuous net (\<lambda>x. c(x) *s v)"
+  fixes c :: "'a \<Rightarrow> real"
+  shows "continuous net (vec1 o c) ==> continuous net (\<lambda>x. c(x) *s v)"
   unfolding continuous_def using Lim_vmul[of c] by auto
 
 lemma continuous_mul:
- "continuous net (vec1 o c) \<Longrightarrow> continuous net f
+  fixes c :: "'a \<Rightarrow> real"
+  shows "continuous net (vec1 o c) \<Longrightarrow> continuous net f
              ==> continuous net (\<lambda>x. c(x) *s f x) "
   unfolding continuous_def using Lim_mul[of c] by auto
 
@@ -3971,6 +4014,7 @@
 text{* And so we have continuity of inverse.                                     *}
 
 lemma Lim_inv:
+  fixes f :: "'a \<Rightarrow> real"
   assumes "((vec1 o f) ---> vec1 l) (net::'a net)"  "l \<noteq> 0"
   shows "((vec1 o inverse o f) ---> vec1(inverse l)) net"
 proof(cases "trivial_limit net")
@@ -4007,11 +4051,13 @@
 qed
 
 lemma continuous_inv:
- "continuous net (vec1 o f) \<Longrightarrow> f(netlimit net) \<noteq> 0
+  fixes f :: "'a \<Rightarrow> real"
+  shows "continuous net (vec1 o f) \<Longrightarrow> f(netlimit net) \<noteq> 0
            ==> continuous net (vec1 o inverse o f)"
   unfolding continuous_def using Lim_inv by auto
 
 lemma continuous_at_within_inv:
+  fixes f :: "real ^ _ \<Rightarrow> real"
   assumes "continuous (at a within s) (vec1 o f)" "f a \<noteq> 0"
   shows "continuous (at a within s) (vec1 o inverse o f)"
 proof(cases "trivial_limit (at a within s)")
@@ -4022,7 +4068,8 @@
 qed
 
 lemma continuous_at_inv:
- "continuous (at a) (vec1 o f) \<Longrightarrow> f a \<noteq> 0
+  fixes f :: "real ^ _ \<Rightarrow> real"
+  shows "continuous (at a) (vec1 o f) \<Longrightarrow> f a \<noteq> 0
          ==> continuous (at a) (vec1 o inverse o f) "
   using within_UNIV[THEN sym, of a] using continuous_at_within_inv[of a UNIV] by auto