# HG changeset patch
# User huffman
# Date 1243617996 25200
# Node ID c13b080bfb34127d06bfa025db7e8cddbd5ef2b1
# Parent  5cddd98abe147f835f8f0b3c268b33f0c21b35a4
remove duplicate cauchy constant

diff -r 5cddd98abe14 -r c13b080bfb34 src/HOL/Library/Topology_Euclidean_Space.thy
--- a/src/HOL/Library/Topology_Euclidean_Space.thy	Fri May 29 10:02:47 2009 -0700
+++ b/src/HOL/Library/Topology_Euclidean_Space.thy	Fri May 29 10:26:36 2009 -0700
@@ -2270,16 +2270,14 @@
 
 subsection{* Completeness. *}
 
-  (* FIXME: Unify this with Cauchy from SEQ!!!!!*)
-
-definition
-  cauchy :: "(nat \<Rightarrow> real ^ 'n::finite) \<Rightarrow> bool" where
-  "cauchy s \<longleftrightarrow> (\<forall>e>0. \<exists>N. \<forall>m n. m \<ge> N \<and> n \<ge> N --> dist(s m)(s n) < e)"
-
-definition complete_def:"complete s \<longleftrightarrow> (\<forall>f::(nat=>real^'a::finite). (\<forall>n. f n \<in> s) \<and> cauchy f
+lemma cauchy_def:
+  "Cauchy s \<longleftrightarrow> (\<forall>e>0. \<exists>N. \<forall>m n. m \<ge> N \<and> n \<ge> N --> dist(s m)(s n) < e)"
+unfolding Cauchy_def by blast
+
+definition complete_def:"complete s \<longleftrightarrow> (\<forall>f::(nat=>real^'a::finite). (\<forall>n. f n \<in> s) \<and> Cauchy f
                       --> (\<exists>l \<in> s. (f ---> l) sequentially))"
 
-lemma cauchy: "cauchy s \<longleftrightarrow> (\<forall>e>0.\<exists> N::nat. \<forall>n\<ge>N. dist(s n)(s N) < e)" (is "?lhs = ?rhs")
+lemma cauchy: "Cauchy s \<longleftrightarrow> (\<forall>e>0.\<exists> N::nat. \<forall>n\<ge>N. dist(s n)(s N) < e)" (is "?lhs = ?rhs")
 proof-
   { assume ?rhs
     { fix e::real
@@ -2306,14 +2304,14 @@
 qed
 
 lemma convergent_imp_cauchy:
- "(s ---> l) sequentially ==> cauchy s"
+ "(s ---> l) sequentially ==> Cauchy s"
 proof(simp only: cauchy_def, rule, rule)
   fix e::real assume "e>0" "(s ---> l) sequentially"
   then obtain N::nat where N:"\<forall>n\<ge>N. dist (s n) l < e/2" unfolding Lim_sequentially by(erule_tac x="e/2" in allE) auto
   thus "\<exists>N. \<forall>m n. N \<le> m \<and> N \<le> n \<longrightarrow> dist (s m) (s n) < e"  using dist_triangle_half_l[of _ l e _] by (rule_tac x=N in exI) auto
 qed
 
-lemma cauchy_imp_bounded: assumes "cauchy s" shows "bounded {y. (\<exists>n::nat. y = s n)}"
+lemma cauchy_imp_bounded: assumes "Cauchy s" shows "bounded {y. (\<exists>n::nat. y = s n)}"
 proof-
   from assms obtain N::nat where "\<forall>m n. N \<le> m \<and> N \<le> n \<longrightarrow> dist (s m) (s n) < 1" unfolding cauchy_def apply(erule_tac x= 1 in allE) by auto
   hence N:"\<forall>n. N \<le> n \<longrightarrow> dist (s N) (s n) < 1" by auto
@@ -2332,7 +2330,7 @@
 
 lemma compact_imp_complete: assumes "compact s" shows "complete s"
 proof-
-  { fix f assume as: "(\<forall>n::nat. f n \<in> s)" "cauchy f"
+  { fix f assume as: "(\<forall>n::nat. f n \<in> s)" "Cauchy f"
     from as(1) obtain l r where lr: "l\<in>s" "(\<forall>m n. m < n \<longrightarrow> r m < r n)" "((f \<circ> r) ---> l) sequentially" using assms unfolding compact_def by blast
 
     { fix n :: nat have lr':"n \<le> r n"
@@ -2358,11 +2356,11 @@
 lemma complete_univ:
  "complete UNIV"
 proof(simp add: complete_def, rule, rule)
-  fix f::"nat \<Rightarrow> real^'n::finite" assume "cauchy f"
+  fix f::"nat \<Rightarrow> real^'n::finite" assume "Cauchy f"
   hence "bounded (f`UNIV)" using cauchy_imp_bounded[of f] unfolding image_def by auto
   hence "compact (closure (f`UNIV))"  using bounded_closed_imp_compact[of "closure (range f)"] by auto
   hence "complete (closure (range f))" using compact_imp_complete by auto
-  thus "\<exists>l. (f ---> l) sequentially" unfolding complete_def[of "closure (range f)"] using `cauchy f` unfolding closure_def  by auto
+  thus "\<exists>l. (f ---> l) sequentially" unfolding complete_def[of "closure (range f)"] using `Cauchy f` unfolding closure_def  by auto
 qed
 
 lemma complete_eq_closed: "complete s \<longleftrightarrow> closed s" (is "?lhs = ?rhs")
@@ -2375,13 +2373,13 @@
   thus ?rhs unfolding closed_limpt by auto
 next
   assume ?rhs
-  { fix f assume as:"\<forall>n::nat. f n \<in> s" "cauchy f"
+  { fix f assume as:"\<forall>n::nat. f n \<in> s" "Cauchy f"
     then obtain l where "(f ---> l) sequentially" using complete_univ[unfolded complete_def, THEN spec[where x=f]] by auto
     hence "\<exists>l\<in>s. (f ---> l) sequentially" using `?rhs`[unfolded closed_sequential_limits, THEN spec[where x=f], THEN spec[where x=l]] using as(1) by auto  }
   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: "(\<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
@@ -2420,7 +2418,7 @@
     qed }
   hence "\<forall>n::nat. x n \<in> s" and x:"\<forall>n. \<forall>m < n. \<not> (dist (x m) (x n) < e)" by blast+
   then obtain l r where "l\<in>s" and r:"\<forall>m n. m < n \<longrightarrow> r m < r n" and "((x \<circ> r) ---> l) sequentially" using assms(1)[unfolded compact_def, THEN spec[where x=x]] by auto
-  from this(3) have "cauchy (x \<circ> r)" using convergent_imp_cauchy by auto
+  from this(3) have "Cauchy (x \<circ> r)" using convergent_imp_cauchy by auto
   then obtain N::nat where N:"\<forall>m n. N \<le> m \<and> N \<le> n \<longrightarrow> dist ((x \<circ> r) m) ((x \<circ> r) n) < e" unfolding cauchy_def using `e>0` by auto
   show False
     using N[THEN spec[where x=N], THEN spec[where x="N+1"]]
@@ -2824,7 +2822,7 @@
     }
     hence "\<exists>N. \<forall>m n. N \<le> m \<and> N \<le> n \<longrightarrow> dist (t m) (t n) < e" by auto
   }
-  hence  "cauchy t" unfolding cauchy_def by auto
+  hence  "Cauchy t" unfolding cauchy_def by auto
   then obtain l where l:"(t ---> l) sequentially" using complete_univ unfolding complete_def by auto
   { fix n::nat
     { fix e::real assume "e>0"
@@ -2876,7 +2874,7 @@
   thus ?rhs by auto
 next
   assume ?rhs
-  hence "\<forall>x. P x \<longrightarrow> cauchy (\<lambda>n. s n x)" unfolding cauchy_def apply auto by (erule_tac x=e in allE)auto
+  hence "\<forall>x. P x \<longrightarrow> Cauchy (\<lambda>n. s n x)" unfolding cauchy_def apply auto by (erule_tac x=e in allE)auto
   then obtain l where l:"\<forall>x. P x \<longrightarrow> ((\<lambda>n. s n x) ---> l x) sequentially" unfolding convergent_eq_cauchy[THEN sym]
     using choice[of "\<lambda>x l. P x \<longrightarrow> ((\<lambda>n. s n x) ---> l) sequentially"] by auto
   { fix e::real assume "e>0"
@@ -4738,7 +4736,7 @@
 using set_eq_subset[of "{a .. b}" "{c .. d}"]
 using subset_interval_1(1)[of a b c d]
 using subset_interval_1(1)[of c d a b]
-by auto
+by auto (* FIXME: slow *)
 
 lemma disjoint_interval_1: fixes a :: "real^1" shows
   "{a .. b} \<inter> {c .. d} = {} \<longleftrightarrow> dest_vec1 b < dest_vec1 a \<or> dest_vec1 d < dest_vec1 c  \<or>  dest_vec1 b < dest_vec1 c \<or> dest_vec1 d < dest_vec1 a"
@@ -5145,8 +5143,9 @@
 text{* "Isometry" (up to constant bounds) of injective linear map etc.           *}
 
 lemma cauchy_isometric:
-  assumes e:"0 < e" and s:"subspace s" and f:"linear f" and normf:"\<forall>x\<in>s. norm(f x) \<ge> e * norm(x)" and xs:"\<forall>n::nat. x n \<in> s" and cf:"cauchy(f o x)"
-  shows "cauchy x"
+  fixes x :: "nat \<Rightarrow> real ^ 'n::finite"
+  assumes e:"0 < e" and s:"subspace s" and f:"linear f" and normf:"\<forall>x\<in>s. norm(f x) \<ge> e * norm(x)" and xs:"\<forall>n::nat. x n \<in> s" and cf:"Cauchy(f o x)"
+  shows "Cauchy x"
 proof-
   { fix d::real assume "d>0"
     then obtain N where N:"\<forall>n\<ge>N. norm (f (x n) - f (x N)) < e * d"
@@ -5166,7 +5165,7 @@
   assumes "0 < e" and s:"subspace s" and f:"linear f" and normf:"\<forall>x\<in>s. norm(f x) \<ge> e * norm(x)" and cs:"complete s"
   shows "complete(f ` s)"
 proof-
-  { fix g assume as:"\<forall>n::nat. g n \<in> f ` s" and cfg:"cauchy g"
+  { fix g assume as:"\<forall>n::nat. g n \<in> f ` s" and cfg:"Cauchy g"
     then obtain x where "\<forall>n. x n \<in> s \<and> g n = f (x n)" unfolding image_iff and Bex_def
       using choice[of "\<lambda> n xa. xa \<in> s \<and> g n = f xa"] by auto
     hence x:"\<forall>n. x n \<in> s"  "\<forall>n. g n = f (x n)" by auto
@@ -5559,7 +5558,7 @@
       thus ?thesis by auto
     qed
   }
-  hence "cauchy z" unfolding cauchy_def by auto
+  hence "Cauchy z" unfolding cauchy_def by auto
   then obtain x where "x\<in>s" and x:"(z ---> x) sequentially" using s(1)[unfolded compact_def complete_def, THEN spec[where x=z]] and z_in_s by auto
 
   def e \<equiv> "dist (f x) x"