1.1 --- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Fri Jan 18 20:00:59 2013 +0100
     1.2 +++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Fri Jan 18 20:01:41 2013 +0100
     1.3 @@ -16,9 +16,18 @@
     1.4    Norm_Arith
     1.5  begin
     1.6  
     1.7 +lemma dist_0_norm:
     1.8 +  fixes x :: "'a::real_normed_vector"
     1.9 +  shows "dist 0 x = norm x"
    1.10 +unfolding dist_norm by simp
    1.11 +
    1.12  lemma dist_double: "dist x y < d / 2 \<Longrightarrow> dist x z < d / 2 \<Longrightarrow> dist y z < d"
    1.13    using dist_triangle[of y z x] by (simp add: dist_commute)
    1.14  
    1.15 +(* LEGACY *)
    1.16 +lemma lim_subseq: "subseq r \<Longrightarrow> s ----> l \<Longrightarrow> (s o r) ----> l"
    1.17 +  by (rule LIMSEQ_subseq_LIMSEQ)
    1.18 +
    1.19  (* TODO: Move this to RComplete.thy -- would need to include Glb into RComplete *)
    1.20  lemma real_isGlb_unique: "[| isGlb R S x; isGlb R S y |] ==> x = (y::real)"
    1.21    apply (frule isGlb_isLb)
    1.22 @@ -2222,6 +2231,9 @@
    1.23    apply (subgoal_tac "\<And>x (y::real). 0 < 1 + abs y \<and> (x <= y \<longrightarrow> x <= 1 + abs y)")
    1.24    by metis arith
    1.25  
    1.26 +lemma Bseq_eq_bounded: "Bseq f \<longleftrightarrow> bounded (range f)"
    1.27 +  unfolding Bseq_def bounded_pos by auto
    1.28 +
    1.29  lemma bounded_Int[intro]: "bounded S \<or> bounded T \<Longrightarrow> bounded (S \<inter> T)"
    1.30    by (metis Int_lower1 Int_lower2 bounded_subset)
    1.31  
    1.32 @@ -3218,88 +3230,24 @@
    1.33      using bounded_closed_imp_seq_compact[of s] unfolding compact_eq_seq_compact_metric by auto
    1.34  qed
    1.35  
    1.36 -lemma lim_subseq:
    1.37 -  "subseq r \<Longrightarrow> (s ---> l) sequentially \<Longrightarrow> ((s o r) ---> l) sequentially"
    1.38 -unfolding tendsto_def eventually_sequentially o_def
    1.39 -by (metis seq_suble le_trans)
    1.40 -
    1.41 -lemma num_Axiom: "EX! g. g 0 = e \<and> (\<forall>n. g (Suc n) = f n (g n))"
    1.42 -  unfolding Ex1_def
    1.43 -  apply (rule_tac x="nat_rec e f" in exI)
    1.44 -  apply (rule conjI)+
    1.45 -apply (rule def_nat_rec_0, simp)
    1.46 -apply (rule allI, rule def_nat_rec_Suc, simp)
    1.47 -apply (rule allI, rule impI, rule ext)
    1.48 -apply (erule conjE)
    1.49 -apply (induct_tac x)
    1.50 -apply simp
    1.51 -apply (erule_tac x="n" in allE)
    1.52 -apply (simp)
    1.53 -done
    1.54 -
    1.55 -lemma convergent_bounded_increasing: fixes s ::"nat\<Rightarrow>real"
    1.56 -  assumes "incseq s" and "\<forall>n. abs(s n) \<le> b"
    1.57 -  shows "\<exists> l. \<forall>e::real>0. \<exists> N. \<forall>n \<ge> N.  abs(s n - l) < e"
    1.58 -proof-
    1.59 -  have "isUb UNIV (range s) b" using assms(2) and abs_le_D1 unfolding isUb_def and setle_def by auto
    1.60 -  then obtain t where t:"isLub UNIV (range s) t" using reals_complete[of "range s" ] by auto
    1.61 -  { fix e::real assume "e>0" and as:"\<forall>N. \<exists>n\<ge>N. \<not> \<bar>s n - t\<bar> < e"
    1.62 -    { fix n::nat
    1.63 -      obtain N where "N\<ge>n" and n:"\<bar>s N - t\<bar> \<ge> e" using as[THEN spec[where x=n]] by auto
    1.64 -      have "t \<ge> s N" using isLub_isUb[OF t, unfolded isUb_def setle_def] by auto
    1.65 -      with n have "s N \<le> t - e" using `e>0` by auto
    1.66 -      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  }
    1.67 -    hence "isUb UNIV (range s) (t - e)" unfolding isUb_def and setle_def by auto
    1.68 -    hence False using isLub_le_isUb[OF t, of "t - e"] and `e>0` by auto  }
    1.69 -  thus ?thesis by blast
    1.70 -qed
    1.71 -
    1.72 -lemma convergent_bounded_monotone: fixes s::"nat \<Rightarrow> real"
    1.73 -  assumes "\<forall>n. abs(s n) \<le> b" and "monoseq s"
    1.74 -  shows "\<exists>l. \<forall>e::real>0. \<exists>N. \<forall>n\<ge>N. abs(s n - l) < e"
    1.75 -  using convergent_bounded_increasing[of s b] assms using convergent_bounded_increasing[of "\<lambda>n. - s n" b]
    1.76 -  unfolding monoseq_def incseq_def
    1.77 -  apply auto unfolding minus_add_distrib[THEN sym, unfolded diff_minus[THEN sym]]
    1.78 -  unfolding abs_minus_cancel by(rule_tac x="-l" in exI)auto
    1.79 -
    1.80  (* TODO: merge this lemma with the ones above *)
    1.81 -lemma bounded_increasing_convergent: fixes s::"nat \<Rightarrow> real"
    1.82 -  assumes "bounded {s n| n::nat. True}"  "\<forall>n. (s n) \<le>(s(Suc n))"
    1.83 -  shows "\<exists>l. (s ---> l) sequentially"
    1.84 -proof-
    1.85 -  obtain a where a:"\<forall>n. \<bar> (s n)\<bar> \<le>  a" using assms(1)[unfolded bounded_iff] by auto
    1.86 -  { fix m::nat
    1.87 -    have "\<And> n. n\<ge>m \<longrightarrow>  (s m) \<le> (s n)"
    1.88 -      apply(induct_tac n) apply simp using assms(2) apply(erule_tac x="na" in allE)
    1.89 -      apply(case_tac "m \<le> na") unfolding not_less_eq_eq by(auto simp add: not_less_eq_eq)  }
    1.90 -  hence "\<forall>m n. m \<le> n \<longrightarrow> (s m) \<le> (s n)" by auto
    1.91 -  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]
    1.92 -    unfolding monoseq_def by auto
    1.93 -  thus ?thesis unfolding LIMSEQ_def apply(rule_tac x="l" in exI)
    1.94 -    unfolding dist_norm  by auto
    1.95 -qed
    1.96 -
    1.97 -lemma compact_real_lemma:
    1.98 -  assumes "\<forall>n::nat. abs(s n) \<le> b"
    1.99 -  shows "\<exists>(l::real) r. subseq r \<and> ((s \<circ> r) ---> l) sequentially"
   1.100 -proof-
   1.101 -  obtain r where r:"subseq r" "monoseq (\<lambda>n. s (r n))"
   1.102 -    using seq_monosub[of s] by auto
   1.103 -  thus ?thesis using convergent_bounded_monotone[of "\<lambda>n. s (r n)" b] and assms
   1.104 -    unfolding tendsto_iff dist_norm eventually_sequentially by auto
   1.105 -qed
   1.106 +lemma bounded_increasing_convergent:
   1.107 +  fixes s :: "nat \<Rightarrow> real"
   1.108 +  shows "bounded {s n| n. True} \<Longrightarrow> \<forall>n. s n \<le> s(Suc n) \<Longrightarrow> \<exists>l. s ----> l"
   1.109 +  using Bseq_mono_convergent[of s] incseq_Suc_iff[of s]
   1.110 +  by (auto simp: image_def Bseq_eq_bounded convergent_def incseq_def)
   1.111  
   1.112  instance real :: heine_borel
   1.113  proof
   1.114    fix s :: "real set" and f :: "nat \<Rightarrow> real"
   1.115    assume s: "bounded s" and f: "\<forall>n. f n \<in> s"
   1.116 -  then obtain b where b: "\<forall>n. abs (f n) \<le> b"
   1.117 -    unfolding bounded_iff by auto
   1.118 -  obtain l :: real and r :: "nat \<Rightarrow> nat" where
   1.119 -    r: "subseq r" and l: "((f \<circ> r) ---> l) sequentially"
   1.120 -    using compact_real_lemma [OF b] by auto
   1.121 -  thus "\<exists>l r. subseq r \<and> ((f \<circ> r) ---> l) sequentially"
   1.122 -    by auto
   1.123 +  obtain r where r: "subseq r" "monoseq (f \<circ> r)"
   1.124 +    unfolding comp_def by (metis seq_monosub)
   1.125 +  moreover
   1.126 +  then have "Bseq (f \<circ> r)"
   1.127 +    unfolding Bseq_eq_bounded using s f by (auto intro: bounded_subset)
   1.128 +  ultimately show "\<exists>l r. subseq r \<and> (f \<circ> r) ----> l"
   1.129 +    using Bseq_monoseq_convergent[of "f \<circ> r"] by (auto simp: convergent_def)
   1.130  qed
   1.131  
   1.132  lemma compact_lemma:
   1.133 @@ -3405,7 +3353,7 @@
   1.134      using bounded_imp_convergent_subsequence [OF s2 f2]
   1.135      unfolding o_def by fast
   1.136    have l1': "((\<lambda>n. fst (f (r1 (r2 n)))) ---> l1) sequentially"
   1.137 -    using lim_subseq [OF r2 l1] unfolding o_def .
   1.138 +    using LIMSEQ_subseq_LIMSEQ [OF l1 r2] unfolding o_def .
   1.139    have l: "((f \<circ> (r1 \<circ> r2)) ---> (l1, l2)) sequentially"
   1.140      using tendsto_Pair [OF l1' l2] unfolding o_def by simp
   1.141    have r: "subseq (r1 \<circ> r2)"
   1.142 @@ -5083,7 +5031,7 @@
   1.143  apply (rule_tac x="(l1, l2)" in rev_bexI, simp)
   1.144  apply (rule_tac x="r1 \<circ> r2" in exI)
   1.145  apply (rule conjI, simp add: subseq_def)
   1.146 -apply (drule_tac r=r2 in lim_subseq [rotated], assumption)
   1.147 +apply (drule_tac f=r2 in LIMSEQ_subseq_LIMSEQ, assumption)
   1.148  apply (drule (1) tendsto_Pair) back
   1.149  apply (simp add: o_def)
   1.150  done
   1.151 @@ -5267,7 +5215,7 @@
   1.152      obtain l' r where "l'\<in>s" and r:"subseq r" and lr:"(((\<lambda>n. fst (f n)) \<circ> r) ---> l') sequentially"
   1.153        using assms(1)[unfolded compact_def, THEN spec[where x="\<lambda> n. fst (f n)"]] using f(2) by auto
   1.154      have "((\<lambda>n. snd (f (r n))) ---> l - l') sequentially"
   1.155 -      using tendsto_diff[OF lim_subseq[OF r as(2)] lr] and f(1) unfolding o_def by auto
   1.156 +      using tendsto_diff[OF LIMSEQ_subseq_LIMSEQ[OF as(2) r] lr] and f(1) unfolding o_def by auto
   1.157      hence "l - l' \<in> t"
   1.158        using assms(2)[unfolded closed_sequential_limits, THEN spec[where x="\<lambda> n. snd (f (r n))"], THEN spec[where x="l - l'"]]
   1.159        using f(3) by auto
   1.160 @@ -6261,11 +6209,6 @@
   1.161    thus ?thesis unfolding complete_def by auto
   1.162  qed
   1.163  
   1.164 -lemma dist_0_norm:
   1.165 -  fixes x :: "'a::real_normed_vector"
   1.166 -  shows "dist 0 x = norm x"
   1.167 -unfolding dist_norm by simp
   1.168 -
   1.169  lemma injective_imp_isometric: fixes f::"'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
   1.170    assumes s:"closed s"  "subspace s"  and f:"bounded_linear f" "\<forall>x\<in>s. (f x = 0) \<longrightarrow> (x = 0)"
   1.171    shows "\<exists>e>0. \<forall>x\<in>s. norm (f x) \<ge> e * norm(x)"