author huffman Wed Aug 31 13:28:29 2011 -0700 (2011-08-31 ago) changeset 44632 076a45f65e12 parent 44631 6820684c7a58 child 44633 8a2fd7418435
simplify/generalize some proofs
```     1.1 --- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Wed Aug 31 10:42:31 2011 -0700
1.2 +++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Wed Aug 31 13:28:29 2011 -0700
1.3 @@ -2242,6 +2242,8 @@
1.4      unfolding convergent_def by auto
1.5  qed
1.6
1.7 +instance euclidean_space \<subseteq> banach ..
1.8 +
1.9  lemma complete_univ: "complete (UNIV :: 'a::complete_space set)"
1.10  proof(simp add: complete_def, rule, rule)
1.11    fix f :: "nat \<Rightarrow> 'a" assume "Cauchy f"
1.12 @@ -2276,21 +2278,13 @@
1.13
1.14  lemma convergent_eq_cauchy:
1.15    fixes s :: "nat \<Rightarrow> 'a::complete_space"
1.16 -  shows "(\<exists>l. (s ---> l) sequentially) \<longleftrightarrow> Cauchy s" (is "?lhs = ?rhs")
1.17 -proof
1.18 -  assume ?lhs then obtain l where "(s ---> l) sequentially" by auto
1.19 -  thus ?rhs using convergent_imp_cauchy by auto
1.20 -next
1.21 -  assume ?rhs thus ?lhs using complete_univ[unfolded complete_def, THEN spec[where x=s]] by auto
1.22 -qed
1.23 +  shows "(\<exists>l. (s ---> l) sequentially) \<longleftrightarrow> Cauchy s"
1.24 +  unfolding Cauchy_convergent_iff convergent_def ..
1.25
1.26  lemma convergent_imp_bounded:
1.27    fixes s :: "nat \<Rightarrow> 'a::metric_space"
1.28 -  shows "(s ---> l) sequentially ==> bounded (s ` (UNIV::(nat set)))"
1.29 -  using convergent_imp_cauchy[of s]
1.30 -  using cauchy_imp_bounded[of s]
1.31 -  unfolding image_def
1.32 -  by auto
1.33 +  shows "(s ---> l) sequentially \<Longrightarrow> bounded (range s)"
1.34 +  by (intro cauchy_imp_bounded convergent_imp_cauchy)
1.35
1.36  subsubsection{* Total boundedness *}
1.37
1.38 @@ -2943,7 +2937,7 @@
1.39            "\<forall>n. (s n \<noteq> {})"
1.40            "\<forall>m n. m \<le> n --> s n \<subseteq> s m"
1.41            "\<forall>e>0. \<exists>n. \<forall>x \<in> (s n). \<forall> y \<in> (s n). dist x y < e"
1.42 -  shows "\<exists>a::'a::heine_borel. \<forall>n::nat. a \<in> s n"
1.43 +  shows "\<exists>a::'a::complete_space. \<forall>n::nat. a \<in> s n"
1.44  proof-
1.45    have "\<forall>n. \<exists> x. x\<in>s n" using assms(2) by auto
1.46    hence "\<exists>t. \<forall>n. t n \<in> s n" using choice[of "\<lambda> n x. x \<in> s n"] by auto
1.47 @@ -2972,7 +2966,7 @@
1.48  text {* Strengthen it to the intersection actually being a singleton. *}
1.49
1.50  lemma decreasing_closed_nest_sing:
1.51 -  fixes s :: "nat \<Rightarrow> 'a::heine_borel set"
1.52 +  fixes s :: "nat \<Rightarrow> 'a::complete_space set"
1.53    assumes "\<forall>n. closed(s n)"
1.54            "\<forall>n. s n \<noteq> {}"
1.55            "\<forall>m n. m \<le> n --> s n \<subseteq> s m"
1.56 @@ -5864,10 +5858,6 @@
1.57    ultimately show "\<exists>!x\<in>s. g x = x" using `a\<in>s` by blast
1.58  qed
1.59
1.60 -
1.61 -(** TODO move this someplace else within this theory **)
1.62 -instance euclidean_space \<subseteq> banach ..
1.63 -
1.64  declare tendsto_const [intro] (* FIXME: move *)
1.65
1.66  end
```