# HG changeset patch
# User hoelzl
# Date 1358535701 -3600
# Node ID d2c6a0a7fcdf7626c1405e0063818d51906fdea3
# Parent  5e3d3d6909753513bd05e7a801526d07162265aa
tuned proof

diff -r 5e3d3d690975 -r d2c6a0a7fcdf src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Fri Jan 18 20:00:59 2013 +0100
+++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Fri Jan 18 20:01:41 2013 +0100
@@ -16,9 +16,18 @@
   Norm_Arith
 begin
 
+lemma dist_0_norm:
+  fixes x :: "'a::real_normed_vector"
+  shows "dist 0 x = norm x"
+unfolding dist_norm by simp
+
 lemma dist_double: "dist x y < d / 2 \<Longrightarrow> dist x z < d / 2 \<Longrightarrow> dist y z < d"
   using dist_triangle[of y z x] by (simp add: dist_commute)
 
+(* LEGACY *)
+lemma lim_subseq: "subseq r \<Longrightarrow> s ----> l \<Longrightarrow> (s o r) ----> l"
+  by (rule LIMSEQ_subseq_LIMSEQ)
+
 (* TODO: Move this to RComplete.thy -- would need to include Glb into RComplete *)
 lemma real_isGlb_unique: "[| isGlb R S x; isGlb R S y |] ==> x = (y::real)"
   apply (frule isGlb_isLb)
@@ -2222,6 +2231,9 @@
   apply (subgoal_tac "\<And>x (y::real). 0 < 1 + abs y \<and> (x <= y \<longrightarrow> x <= 1 + abs y)")
   by metis arith
 
+lemma Bseq_eq_bounded: "Bseq f \<longleftrightarrow> bounded (range f)"
+  unfolding Bseq_def bounded_pos by auto
+
 lemma bounded_Int[intro]: "bounded S \<or> bounded T \<Longrightarrow> bounded (S \<inter> T)"
   by (metis Int_lower1 Int_lower2 bounded_subset)
 
@@ -3218,88 +3230,24 @@
     using bounded_closed_imp_seq_compact[of s] unfolding compact_eq_seq_compact_metric by auto
 qed
 
-lemma lim_subseq:
-  "subseq r \<Longrightarrow> (s ---> l) sequentially \<Longrightarrow> ((s o r) ---> l) sequentially"
-unfolding tendsto_def eventually_sequentially o_def
-by (metis seq_suble le_trans)
-
-lemma num_Axiom: "EX! g. g 0 = e \<and> (\<forall>n. g (Suc n) = f n (g n))"
-  unfolding Ex1_def
-  apply (rule_tac x="nat_rec e f" in exI)
-  apply (rule conjI)+
-apply (rule def_nat_rec_0, simp)
-apply (rule allI, rule def_nat_rec_Suc, simp)
-apply (rule allI, rule impI, rule ext)
-apply (erule conjE)
-apply (induct_tac x)
-apply simp
-apply (erule_tac x="n" in allE)
-apply (simp)
-done
-
-lemma convergent_bounded_increasing: fixes s ::"nat\<Rightarrow>real"
-  assumes "incseq s" and "\<forall>n. abs(s n) \<le> b"
-  shows "\<exists> l. \<forall>e::real>0. \<exists> N. \<forall>n \<ge> N.  abs(s n - l) < e"
-proof-
-  have "isUb UNIV (range s) b" using assms(2) and abs_le_D1 unfolding isUb_def and setle_def by auto
-  then obtain t where t:"isLub UNIV (range s) t" using reals_complete[of "range s" ] by auto
-  { fix e::real assume "e>0" and as:"\<forall>N. \<exists>n\<ge>N. \<not> \<bar>s n - t\<bar> < e"
-    { fix n::nat
-      obtain N where "N\<ge>n" and n:"\<bar>s N - t\<bar> \<ge> e" using as[THEN spec[where x=n]] by auto
-      have "t \<ge> s N" using isLub_isUb[OF t, unfolded isUb_def setle_def] by auto
-      with n have "s N \<le> t - e" using `e>0` by auto
-      hence "s n \<le> t - e" using assms(1)[unfolded incseq_def, THEN spec[where x=n], THEN spec[where x=N]] using `n\<le>N` by auto  }
-    hence "isUb UNIV (range s) (t - e)" unfolding isUb_def and setle_def by auto
-    hence False using isLub_le_isUb[OF t, of "t - e"] and `e>0` by auto  }
-  thus ?thesis by blast
-qed
-
-lemma convergent_bounded_monotone: fixes s::"nat \<Rightarrow> real"
-  assumes "\<forall>n. abs(s n) \<le> b" and "monoseq s"
-  shows "\<exists>l. \<forall>e::real>0. \<exists>N. \<forall>n\<ge>N. abs(s n - l) < e"
-  using convergent_bounded_increasing[of s b] assms using convergent_bounded_increasing[of "\<lambda>n. - s n" b]
-  unfolding monoseq_def incseq_def
-  apply auto unfolding minus_add_distrib[THEN sym, unfolded diff_minus[THEN sym]]
-  unfolding abs_minus_cancel by(rule_tac x="-l" in exI)auto
-
 (* TODO: merge this lemma with the ones above *)
-lemma bounded_increasing_convergent: fixes s::"nat \<Rightarrow> real"
-  assumes "bounded {s n| n::nat. True}"  "\<forall>n. (s n) \<le>(s(Suc n))"
-  shows "\<exists>l. (s ---> l) sequentially"
-proof-
-  obtain a where a:"\<forall>n. \<bar> (s n)\<bar> \<le>  a" using assms(1)[unfolded bounded_iff] by auto
-  { fix m::nat
-    have "\<And> n. n\<ge>m \<longrightarrow>  (s m) \<le> (s n)"
-      apply(induct_tac n) apply simp using assms(2) apply(erule_tac x="na" in allE)
-      apply(case_tac "m \<le> na") unfolding not_less_eq_eq by(auto simp add: not_less_eq_eq)  }
-  hence "\<forall>m n. m \<le> n \<longrightarrow> (s m) \<le> (s n)" by auto
-  then obtain l where "\<forall>e>0. \<exists>N. \<forall>n\<ge>N. \<bar> (s n) - l\<bar> < e" using convergent_bounded_monotone[OF a]
-    unfolding monoseq_def by auto
-  thus ?thesis unfolding LIMSEQ_def apply(rule_tac x="l" in exI)
-    unfolding dist_norm  by auto
-qed
-
-lemma compact_real_lemma:
-  assumes "\<forall>n::nat. abs(s n) \<le> b"
-  shows "\<exists>(l::real) r. subseq r \<and> ((s \<circ> r) ---> l) sequentially"
-proof-
-  obtain r where r:"subseq r" "monoseq (\<lambda>n. s (r n))"
-    using seq_monosub[of s] by auto
-  thus ?thesis using convergent_bounded_monotone[of "\<lambda>n. s (r n)" b] and assms
-    unfolding tendsto_iff dist_norm eventually_sequentially by auto
-qed
+lemma bounded_increasing_convergent:
+  fixes s :: "nat \<Rightarrow> real"
+  shows "bounded {s n| n. True} \<Longrightarrow> \<forall>n. s n \<le> s(Suc n) \<Longrightarrow> \<exists>l. s ----> l"
+  using Bseq_mono_convergent[of s] incseq_Suc_iff[of s]
+  by (auto simp: image_def Bseq_eq_bounded convergent_def incseq_def)
 
 instance real :: heine_borel
 proof
   fix s :: "real set" and f :: "nat \<Rightarrow> real"
   assume s: "bounded s" and f: "\<forall>n. f n \<in> s"
-  then obtain b where b: "\<forall>n. abs (f n) \<le> b"
-    unfolding bounded_iff by auto
-  obtain l :: real and r :: "nat \<Rightarrow> nat" where
-    r: "subseq r" and l: "((f \<circ> r) ---> l) sequentially"
-    using compact_real_lemma [OF b] by auto
-  thus "\<exists>l r. subseq r \<and> ((f \<circ> r) ---> l) sequentially"
-    by auto
+  obtain r where r: "subseq r" "monoseq (f \<circ> r)"
+    unfolding comp_def by (metis seq_monosub)
+  moreover
+  then have "Bseq (f \<circ> r)"
+    unfolding Bseq_eq_bounded using s f by (auto intro: bounded_subset)
+  ultimately show "\<exists>l r. subseq r \<and> (f \<circ> r) ----> l"
+    using Bseq_monoseq_convergent[of "f \<circ> r"] by (auto simp: convergent_def)
 qed
 
 lemma compact_lemma:
@@ -3405,7 +3353,7 @@
     using bounded_imp_convergent_subsequence [OF s2 f2]
     unfolding o_def by fast
   have l1': "((\<lambda>n. fst (f (r1 (r2 n)))) ---> l1) sequentially"
-    using lim_subseq [OF r2 l1] unfolding o_def .
+    using LIMSEQ_subseq_LIMSEQ [OF l1 r2] unfolding o_def .
   have l: "((f \<circ> (r1 \<circ> r2)) ---> (l1, l2)) sequentially"
     using tendsto_Pair [OF l1' l2] unfolding o_def by simp
   have r: "subseq (r1 \<circ> r2)"
@@ -5083,7 +5031,7 @@
 apply (rule_tac x="(l1, l2)" in rev_bexI, simp)
 apply (rule_tac x="r1 \<circ> r2" in exI)
 apply (rule conjI, simp add: subseq_def)
-apply (drule_tac r=r2 in lim_subseq [rotated], assumption)
+apply (drule_tac f=r2 in LIMSEQ_subseq_LIMSEQ, assumption)
 apply (drule (1) tendsto_Pair) back
 apply (simp add: o_def)
 done
@@ -5267,7 +5215,7 @@
     obtain l' r where "l'\<in>s" and r:"subseq r" and lr:"(((\<lambda>n. fst (f n)) \<circ> r) ---> l') sequentially"
       using assms(1)[unfolded compact_def, THEN spec[where x="\<lambda> n. fst (f n)"]] using f(2) by auto
     have "((\<lambda>n. snd (f (r n))) ---> l - l') sequentially"
-      using tendsto_diff[OF lim_subseq[OF r as(2)] lr] and f(1) unfolding o_def by auto
+      using tendsto_diff[OF LIMSEQ_subseq_LIMSEQ[OF as(2) r] lr] and f(1) unfolding o_def by auto
     hence "l - l' \<in> t"
       using assms(2)[unfolded closed_sequential_limits, THEN spec[where x="\<lambda> n. snd (f (r n))"], THEN spec[where x="l - l'"]]
       using f(3) by auto
@@ -6261,11 +6209,6 @@
   thus ?thesis unfolding complete_def by auto
 qed
 
-lemma dist_0_norm:
-  fixes x :: "'a::real_normed_vector"
-  shows "dist 0 x = norm x"
-unfolding dist_norm by simp
-
 lemma injective_imp_isometric: fixes f::"'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
   assumes s:"closed s"  "subspace s"  and f:"bounded_linear f" "\<forall>x\<in>s. (f x = 0) \<longrightarrow> (x = 0)"
   shows "\<exists>e>0. \<forall>x\<in>s. norm (f x) \<ge> e * norm(x)"