author huffman Tue Jun 02 23:49:46 2009 -0700 (2009-06-02) changeset 31406 e23dd3aac0fb parent 31405 1f72869f1a2e child 31407 689df1591793
instance ^ :: complete_space
```     1.1 --- a/src/HOL/Library/Euclidean_Space.thy	Tue Jun 02 23:35:52 2009 -0700
1.2 +++ b/src/HOL/Library/Euclidean_Space.thy	Tue Jun 02 23:49:46 2009 -0700
1.3 @@ -553,26 +553,8 @@
1.4  unfolding LIM_conv_tendsto by (rule tendsto_Cart_nth)
1.5
1.6  lemma Cauchy_Cart_nth:
1.7 -  fixes X :: "nat \<Rightarrow> 'a::metric_space ^ 'n::finite"
1.8 -  assumes "Cauchy (\<lambda>n. X n)"
1.9 -  shows "Cauchy (\<lambda>n. X n \$ i)"
1.10 -proof (rule metric_CauchyI)
1.11 -  fix e :: real assume "0 < e"
1.12 -  obtain M where "\<forall>m\<ge>M. \<forall>n\<ge>M. dist (X m) (X n) < e"
1.13 -    using metric_CauchyD [OF `Cauchy X` `0 < e`] by fast
1.14 -  moreover
1.15 -  {
1.16 -    fix m n
1.17 -    assume "M \<le> m" "M \<le> n"
1.18 -    have "dist (X m \$ i) (X n \$ i) \<le> dist (X m) (X n)"
1.19 -      by (rule dist_nth_le)
1.20 -    also assume "dist (X m) (X n) < e"
1.21 -    finally have "dist (X m \$ i) (X n \$ i) < e" .
1.22 -  }
1.23 -  ultimately
1.24 -  have "\<forall>m\<ge>M. \<forall>n\<ge>M. dist (X m \$ i) (X n \$ i) < e" by fast
1.25 -  thus "\<exists>M. \<forall>m\<ge>M. \<forall>n\<ge>M. dist (X m \$ i) (X n \$ i) < e" ..
1.26 -qed
1.27 +  "Cauchy (\<lambda>n. X n) \<Longrightarrow> Cauchy (\<lambda>n. X n \$ i)"
1.28 +unfolding Cauchy_def by (fast intro: le_less_trans [OF dist_nth_le])
1.29
1.30  lemma LIMSEQ_vector:
1.31    fixes X :: "nat \<Rightarrow> 'a::metric_space ^ 'n::finite"
1.32 @@ -641,6 +623,18 @@
1.33    then show "\<exists>M. \<forall>m\<ge>M. \<forall>n\<ge>M. dist (X m) (X n) < r" ..
1.34  qed
1.35
1.36 +instance "^" :: (complete_space, finite) complete_space
1.37 +proof
1.38 +  fix X :: "nat \<Rightarrow> 'a ^ 'b" assume "Cauchy X"
1.39 +  have "\<And>i. (\<lambda>n. X n \$ i) ----> lim (\<lambda>n. X n \$ i)"
1.40 +    using Cauchy_Cart_nth [OF `Cauchy X`]
1.41 +    by (simp add: Cauchy_convergent_iff convergent_LIMSEQ_iff)
1.42 +  hence "X ----> Cart_lambda (\<lambda>i. lim (\<lambda>n. X n \$ i))"
1.43 +    by (simp add: LIMSEQ_vector)
1.44 +  then show "convergent X"
1.45 +    by (rule convergentI)
1.46 +qed
1.47 +
1.48  subsection {* Norms *}
1.49
1.50  instantiation "^" :: (real_normed_vector, finite) real_normed_vector
1.51 @@ -688,6 +682,8 @@
1.52  apply (rule_tac x="1" in exI, simp add: norm_nth_le)
1.53  done
1.54
1.55 +instance "^" :: (banach, finite) banach ..
1.56 +
1.57  subsection {* Inner products *}
1.58
1.59  instantiation "^" :: (real_inner, finite) real_inner
```