instance ^ :: complete_space
authorhuffman
Tue Jun 02 23:49:46 2009 -0700 (2009-06-02)
changeset 31406e23dd3aac0fb
parent 31405 1f72869f1a2e
child 31407 689df1591793
instance ^ :: complete_space
src/HOL/Library/Euclidean_Space.thy
     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