# HG changeset patch
# User huffman
# Date 1259086499 28800
# Node ID 22758f95e624e44117b85b4de0f27bb0fa2bd017
# Parent  9095ba4d2cd49dc41a3dc79399e72a17d32549cb
re-state lemmas using 'range'

diff -r 9095ba4d2cd4 -r 22758f95e624 src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Sun Nov 29 22:27:47 2009 -0800
+++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Tue Nov 24 10:14:59 2009 -0800
@@ -2437,7 +2437,7 @@
   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 (range s)"
 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
@@ -2448,7 +2448,7 @@
   ultimately show "?thesis"
     unfolding bounded_any_center [where a="s N"]
     apply(rule_tac x="max a 1" in exI) apply auto
-    apply(erule_tac x=n in allE) apply(erule_tac x=n in ballE) by auto
+    apply(erule_tac x=y in allE) apply(erule_tac x=y in ballE) by auto
 qed
 
 lemma compact_imp_complete: assumes "compact s" shows "complete s"
@@ -2474,12 +2474,12 @@
 instance heine_borel < complete_space
 proof
   fix f :: "nat \<Rightarrow> 'a" assume "Cauchy f"
-  hence "bounded (range f)" unfolding image_def
-    using cauchy_imp_bounded [of f] by auto
+  hence "bounded (range f)"
+    by (rule cauchy_imp_bounded)
   hence "compact (closure (range f))"
     using bounded_closed_imp_compact [of "closure (range f)"] by auto
   hence "complete (closure (range f))"
-    using compact_imp_complete by auto
+    by (rule compact_imp_complete)
   moreover have "\<forall>n. f n \<in> closure (range f)"
     using closure_subset [of "range f"] by auto
   ultimately have "\<exists>l\<in>closure (range f). (f ---> l) sequentially"
@@ -2732,10 +2732,10 @@
 lemma sequence_infinite_lemma:
   fixes l :: "'a::metric_space" (* TODO: generalize *)
   assumes "\<forall>n::nat. (f n  \<noteq> l)"  "(f ---> l) sequentially"
-  shows "infinite {y. (\<exists> n. y = f n)}"
-proof(rule ccontr)
-  let ?A = "(\<lambda>x. dist x l) ` {y. \<exists>n. y = f n}"
-  assume "\<not> infinite {y. \<exists>n. y = f n}"
+  shows "infinite (range f)"
+proof
+  let ?A = "(\<lambda>x. dist x l) ` range f"
+  assume "finite (range f)"
   hence **:"finite ?A" "?A \<noteq> {}" by auto
   obtain k where k:"dist (f k) l = Min ?A" using Min_in[OF **] by auto
   have "0 < Min ?A" using assms(1) unfolding dist_nz unfolding Min_gr_iff[OF **] by auto
@@ -2746,7 +2746,7 @@
 
 lemma sequence_unique_limpt:
   fixes l :: "'a::metric_space" (* TODO: generalize *)
-  assumes "\<forall>n::nat. (f n \<noteq> l)"  "(f ---> l) sequentially"  "l' islimpt {y.  (\<exists>n. y = f n)}"
+  assumes "\<forall>n::nat. (f n \<noteq> l)"  "(f ---> l) sequentially"  "l' islimpt (range f)"
   shows "l' = l"
 proof(rule ccontr)
   def e \<equiv> "dist l' l"
@@ -2773,8 +2773,8 @@
       case False thus "l\<in>s" using as(1) by auto
     next
       case True note cas = this
-      with as(2) have "infinite {y. \<exists>n. y = x n}" using sequence_infinite_lemma[of x l] by auto
-      then obtain l' where "l'\<in>s" "l' islimpt {y. \<exists>n. y = x n}" using assms[THEN spec[where x="{y. \<exists>n. y = x n}"]] as(1) by auto
+      with as(2) have "infinite (range x)" using sequence_infinite_lemma[of x l] by auto
+      then obtain l' where "l'\<in>s" "l' islimpt (range x)" using assms[THEN spec[where x="range x"]] as(1) by auto
       thus "l\<in>s" using sequence_unique_limpt[of x l l'] using as cas by auto
     qed  }
   thus ?thesis unfolding closed_sequential_limits by fast
@@ -3031,21 +3031,22 @@
 text{* Strengthen it to the intersection actually being a singleton.             *}
 
 lemma decreasing_closed_nest_sing:
+  fixes s :: "nat \<Rightarrow> 'a::heine_borel set"
   assumes "\<forall>n. closed(s n)"
           "\<forall>n. s n \<noteq> {}"
           "\<forall>m n. m \<le> n --> s n \<subseteq> s m"
           "\<forall>e>0. \<exists>n. \<forall>x \<in> (s n). \<forall> y\<in>(s n). dist x y < e"
-  shows "\<exists>a::'a::heine_borel. \<Inter> {t. (\<exists>n::nat. t = s n)} = {a}"
+  shows "\<exists>a. \<Inter>(range s) = {a}"
 proof-
   obtain a where a:"\<forall>n. a \<in> s n" using decreasing_closed_nest[of s] using assms by auto
-  { fix b assume b:"b \<in> \<Inter>{t. \<exists>n. t = s n}"
+  { fix b assume b:"b \<in> \<Inter>(range s)"
     { fix e::real assume "e>0"
       hence "dist a b < e" using assms(4 )using b using a by blast
     }
     hence "dist a b = 0" by (metis dist_eq_0_iff dist_nz real_less_def)
   }
-  with a have "\<Inter>{t. \<exists>n. t = s n} = {a}"  by auto
-  thus ?thesis by auto
+  with a have "\<Inter>(range s) = {a}" unfolding image_def by auto
+  thus ?thesis ..
 qed
 
 text{* Cauchy-type criteria for uniform convergence. *}