move metric_space to its own theory
authorhoelzl
Fri Mar 22 10:41:43 2013 +0100 (2013-03-22)
changeset 51472adb441e4b9e9
parent 51471 cad22a3cc09c
child 51473 1210309fddab
move metric_space to its own theory
src/HOL/Lim.thy
src/HOL/Limits.thy
src/HOL/Metric_Spaces.thy
src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
src/HOL/RealVector.thy
src/HOL/SEQ.thy
     1.1 --- a/src/HOL/Lim.thy	Fri Mar 22 10:41:42 2013 +0100
     1.2 +++ b/src/HOL/Lim.thy	Fri Mar 22 10:41:43 2013 +0100
     1.3 @@ -10,22 +10,8 @@
     1.4  imports SEQ
     1.5  begin
     1.6  
     1.7 -definition
     1.8 -  isUCont :: "['a::metric_space \<Rightarrow> 'b::metric_space] \<Rightarrow> bool" where
     1.9 -  "isUCont f = (\<forall>r>0. \<exists>s>0. \<forall>x y. dist x y < s \<longrightarrow> dist (f x) (f y) < r)"
    1.10 -
    1.11  subsection {* Limits of Functions *}
    1.12  
    1.13 -lemma metric_LIM_I:
    1.14 -  "(\<And>r. 0 < r \<Longrightarrow> \<exists>s>0. \<forall>x. x \<noteq> a \<and> dist x a < s \<longrightarrow> dist (f x) L < r)
    1.15 -    \<Longrightarrow> f -- a --> L"
    1.16 -by (simp add: LIM_def)
    1.17 -
    1.18 -lemma metric_LIM_D:
    1.19 -  "\<lbrakk>f -- a --> L; 0 < r\<rbrakk>
    1.20 -    \<Longrightarrow> \<exists>s>0. \<forall>x. x \<noteq> a \<and> dist x a < s \<longrightarrow> dist (f x) L < r"
    1.21 -by (simp add: LIM_def)
    1.22 -
    1.23  lemma LIM_eq:
    1.24    fixes a :: "'a::real_normed_vector" and L :: "'b::real_normed_vector"
    1.25    shows "f -- a --> L =
    1.26 @@ -80,13 +66,6 @@
    1.27    shows "((\<lambda>x. f x - l) ---> 0) F = (f ---> l) F"
    1.28  unfolding tendsto_iff dist_norm by simp
    1.29  
    1.30 -lemma metric_LIM_imp_LIM:
    1.31 -  assumes f: "f -- a --> l"
    1.32 -  assumes le: "\<And>x. x \<noteq> a \<Longrightarrow> dist (g x) m \<le> dist (f x) l"
    1.33 -  shows "g -- a --> m"
    1.34 -  by (rule metric_tendsto_imp_tendsto [OF f],
    1.35 -    auto simp add: eventually_at_topological le)
    1.36 -
    1.37  lemma LIM_imp_LIM:
    1.38    fixes f :: "'a::topological_space \<Rightarrow> 'b::real_normed_vector"
    1.39    fixes g :: "'a::topological_space \<Rightarrow> 'c::real_normed_vector"
    1.40 @@ -96,18 +75,6 @@
    1.41    by (rule metric_LIM_imp_LIM [OF f],
    1.42      simp add: dist_norm le)
    1.43  
    1.44 -lemma metric_LIM_equal2:
    1.45 -  assumes 1: "0 < R"
    1.46 -  assumes 2: "\<And>x. \<lbrakk>x \<noteq> a; dist x a < R\<rbrakk> \<Longrightarrow> f x = g x"
    1.47 -  shows "g -- a --> l \<Longrightarrow> f -- a --> l"
    1.48 -apply (rule topological_tendstoI)
    1.49 -apply (drule (2) topological_tendstoD)
    1.50 -apply (simp add: eventually_at, safe)
    1.51 -apply (rule_tac x="min d R" in exI, safe)
    1.52 -apply (simp add: 1)
    1.53 -apply (simp add: 2)
    1.54 -done
    1.55 -
    1.56  lemma LIM_equal2:
    1.57    fixes f g :: "'a::real_normed_vector \<Rightarrow> 'b::topological_space"
    1.58    assumes 1: "0 < R"
    1.59 @@ -115,14 +82,6 @@
    1.60    shows "g -- a --> l \<Longrightarrow> f -- a --> l"
    1.61  by (rule metric_LIM_equal2 [OF 1 2], simp_all add: dist_norm)
    1.62  
    1.63 -lemma metric_LIM_compose2:
    1.64 -  assumes f: "f -- a --> b"
    1.65 -  assumes g: "g -- b --> c"
    1.66 -  assumes inj: "\<exists>d>0. \<forall>x. x \<noteq> a \<and> dist x a < d \<longrightarrow> f x \<noteq> b"
    1.67 -  shows "(\<lambda>x. g (f x)) -- a --> c"
    1.68 -  using g f inj [folded eventually_at]
    1.69 -  by (rule tendsto_compose_eventually)
    1.70 -
    1.71  lemma LIM_compose2:
    1.72    fixes a :: "'a::real_normed_vector"
    1.73    assumes f: "f -- a --> b"
    1.74 @@ -199,13 +158,6 @@
    1.75    shows "\<lbrakk>isCont f a; isCont g a; g a \<noteq> 0\<rbrakk> \<Longrightarrow> isCont (\<lambda>x. f x / g x) a"
    1.76    unfolding isCont_def by (rule tendsto_divide)
    1.77  
    1.78 -lemma metric_isCont_LIM_compose2:
    1.79 -  assumes f [unfolded isCont_def]: "isCont f a"
    1.80 -  assumes g: "g -- f a --> l"
    1.81 -  assumes inj: "\<exists>d>0. \<forall>x. x \<noteq> a \<and> dist x a < d \<longrightarrow> f x \<noteq> f a"
    1.82 -  shows "(\<lambda>x. g (f x)) -- a --> l"
    1.83 -by (rule metric_LIM_compose2 [OF f g inj])
    1.84 -
    1.85  lemma isCont_LIM_compose2:
    1.86    fixes a :: "'a::real_normed_vector"
    1.87    assumes f [unfolded isCont_def]: "isCont f a"
    1.88 @@ -251,18 +203,6 @@
    1.89  
    1.90  subsection {* Uniform Continuity *}
    1.91  
    1.92 -lemma isUCont_isCont: "isUCont f ==> isCont f x"
    1.93 -by (simp add: isUCont_def isCont_def LIM_def, force)
    1.94 -
    1.95 -lemma isUCont_Cauchy:
    1.96 -  "\<lbrakk>isUCont f; Cauchy X\<rbrakk> \<Longrightarrow> Cauchy (\<lambda>n. f (X n))"
    1.97 -unfolding isUCont_def
    1.98 -apply (rule metric_CauchyI)
    1.99 -apply (drule_tac x=e in spec, safe)
   1.100 -apply (drule_tac e=s in metric_CauchyD, safe)
   1.101 -apply (rule_tac x=M in exI, simp)
   1.102 -done
   1.103 -
   1.104  lemma (in bounded_linear) isUCont: "isUCont f"
   1.105  unfolding isUCont_def dist_norm
   1.106  proof (intro allI impI)
     2.1 --- a/src/HOL/Limits.thy	Fri Mar 22 10:41:42 2013 +0100
     2.2 +++ b/src/HOL/Limits.thy	Fri Mar 22 10:41:43 2013 +0100
     2.3 @@ -11,31 +11,6 @@
     2.4  definition at_infinity :: "'a::real_normed_vector filter" where
     2.5    "at_infinity = Abs_filter (\<lambda>P. \<exists>r. \<forall>x. r \<le> norm x \<longrightarrow> P x)"
     2.6  
     2.7 -
     2.8 -lemma eventually_nhds_metric:
     2.9 -  "eventually P (nhds a) \<longleftrightarrow> (\<exists>d>0. \<forall>x. dist x a < d \<longrightarrow> P x)"
    2.10 -unfolding eventually_nhds open_dist
    2.11 -apply safe
    2.12 -apply fast
    2.13 -apply (rule_tac x="{x. dist x a < d}" in exI, simp)
    2.14 -apply clarsimp
    2.15 -apply (rule_tac x="d - dist x a" in exI, clarsimp)
    2.16 -apply (simp only: less_diff_eq)
    2.17 -apply (erule le_less_trans [OF dist_triangle])
    2.18 -done
    2.19 -
    2.20 -lemma eventually_at:
    2.21 -  fixes a :: "'a::metric_space"
    2.22 -  shows "eventually P (at a) \<longleftrightarrow> (\<exists>d>0. \<forall>x. x \<noteq> a \<and> dist x a < d \<longrightarrow> P x)"
    2.23 -unfolding at_def eventually_within eventually_nhds_metric by auto
    2.24 -lemma eventually_within_less: (* COPY FROM Topo/eventually_within *)
    2.25 -  "eventually P (at a within S) \<longleftrightarrow> (\<exists>d>0. \<forall>x\<in>S. 0 < dist x a \<and> dist x a < d \<longrightarrow> P x)"
    2.26 -  unfolding eventually_within eventually_at dist_nz by auto
    2.27 -
    2.28 -lemma eventually_within_le: (* COPY FROM Topo/eventually_within_le *)
    2.29 -  "eventually P (at a within S) \<longleftrightarrow> (\<exists>d>0. \<forall>x\<in>S. 0 < dist x a \<and> dist x a <= d \<longrightarrow> P x)"
    2.30 -  unfolding eventually_within_less by auto (metis dense order_le_less_trans)
    2.31 -
    2.32  lemma eventually_at_infinity:
    2.33    "eventually P at_infinity \<longleftrightarrow> (\<exists>b. \<forall>x. b \<le> norm x \<longrightarrow> P x)"
    2.34  unfolding at_infinity_def
    2.35 @@ -246,39 +221,8 @@
    2.36  lemma tendsto_Zfun_iff: "(f ---> a) F = Zfun (\<lambda>x. f x - a) F"
    2.37    by (simp only: tendsto_iff Zfun_def dist_norm)
    2.38  
    2.39 -
    2.40 -lemma metric_tendsto_imp_tendsto:
    2.41 -  assumes f: "(f ---> a) F"
    2.42 -  assumes le: "eventually (\<lambda>x. dist (g x) b \<le> dist (f x) a) F"
    2.43 -  shows "(g ---> b) F"
    2.44 -proof (rule tendstoI)
    2.45 -  fix e :: real assume "0 < e"
    2.46 -  with f have "eventually (\<lambda>x. dist (f x) a < e) F" by (rule tendstoD)
    2.47 -  with le show "eventually (\<lambda>x. dist (g x) b < e) F"
    2.48 -    using le_less_trans by (rule eventually_elim2)
    2.49 -qed
    2.50  subsubsection {* Distance and norms *}
    2.51  
    2.52 -lemma tendsto_dist [tendsto_intros]:
    2.53 -  assumes f: "(f ---> l) F" and g: "(g ---> m) F"
    2.54 -  shows "((\<lambda>x. dist (f x) (g x)) ---> dist l m) F"
    2.55 -proof (rule tendstoI)
    2.56 -  fix e :: real assume "0 < e"
    2.57 -  hence e2: "0 < e/2" by simp
    2.58 -  from tendstoD [OF f e2] tendstoD [OF g e2]
    2.59 -  show "eventually (\<lambda>x. dist (dist (f x) (g x)) (dist l m) < e) F"
    2.60 -  proof (eventually_elim)
    2.61 -    case (elim x)
    2.62 -    then show "dist (dist (f x) (g x)) (dist l m) < e"
    2.63 -      unfolding dist_real_def
    2.64 -      using dist_triangle2 [of "f x" "g x" "l"]
    2.65 -      using dist_triangle2 [of "g x" "l" "m"]
    2.66 -      using dist_triangle3 [of "l" "m" "f x"]
    2.67 -      using dist_triangle [of "f x" "m" "g x"]
    2.68 -      by arith
    2.69 -  qed
    2.70 -qed
    2.71 -
    2.72  lemma norm_conv_dist: "norm x = dist x 0"
    2.73    unfolding dist_norm by simp
    2.74  
    2.75 @@ -544,50 +488,6 @@
    2.76    shows "\<lbrakk>(f ---> l) F; l \<noteq> 0\<rbrakk> \<Longrightarrow> ((\<lambda>x. sgn (f x)) ---> sgn l) F"
    2.77    unfolding sgn_div_norm by (simp add: tendsto_intros)
    2.78  
    2.79 -lemma filterlim_at_bot_at_right:
    2.80 -  fixes f :: "real \<Rightarrow> 'b::linorder"
    2.81 -  assumes mono: "\<And>x y. Q x \<Longrightarrow> Q y \<Longrightarrow> x \<le> y \<Longrightarrow> f x \<le> f y"
    2.82 -  assumes bij: "\<And>x. P x \<Longrightarrow> f (g x) = x" "\<And>x. P x \<Longrightarrow> Q (g x)"
    2.83 -  assumes Q: "eventually Q (at_right a)" and bound: "\<And>b. Q b \<Longrightarrow> a < b"
    2.84 -  assumes P: "eventually P at_bot"
    2.85 -  shows "filterlim f at_bot (at_right a)"
    2.86 -proof -
    2.87 -  from P obtain x where x: "\<And>y. y \<le> x \<Longrightarrow> P y"
    2.88 -    unfolding eventually_at_bot_linorder by auto
    2.89 -  show ?thesis
    2.90 -  proof (intro filterlim_at_bot_le[THEN iffD2] allI impI)
    2.91 -    fix z assume "z \<le> x"
    2.92 -    with x have "P z" by auto
    2.93 -    have "eventually (\<lambda>x. x \<le> g z) (at_right a)"
    2.94 -      using bound[OF bij(2)[OF `P z`]]
    2.95 -      by (auto simp add: eventually_within_less dist_real_def intro!:  exI[of _ "g z - a"])
    2.96 -    with Q show "eventually (\<lambda>x. f x \<le> z) (at_right a)"
    2.97 -      by eventually_elim (metis bij `P z` mono)
    2.98 -  qed
    2.99 -qed
   2.100 -
   2.101 -lemma filterlim_at_top_at_left:
   2.102 -  fixes f :: "real \<Rightarrow> 'b::linorder"
   2.103 -  assumes mono: "\<And>x y. Q x \<Longrightarrow> Q y \<Longrightarrow> x \<le> y \<Longrightarrow> f x \<le> f y"
   2.104 -  assumes bij: "\<And>x. P x \<Longrightarrow> f (g x) = x" "\<And>x. P x \<Longrightarrow> Q (g x)"
   2.105 -  assumes Q: "eventually Q (at_left a)" and bound: "\<And>b. Q b \<Longrightarrow> b < a"
   2.106 -  assumes P: "eventually P at_top"
   2.107 -  shows "filterlim f at_top (at_left a)"
   2.108 -proof -
   2.109 -  from P obtain x where x: "\<And>y. x \<le> y \<Longrightarrow> P y"
   2.110 -    unfolding eventually_at_top_linorder by auto
   2.111 -  show ?thesis
   2.112 -  proof (intro filterlim_at_top_ge[THEN iffD2] allI impI)
   2.113 -    fix z assume "x \<le> z"
   2.114 -    with x have "P z" by auto
   2.115 -    have "eventually (\<lambda>x. g z \<le> x) (at_left a)"
   2.116 -      using bound[OF bij(2)[OF `P z`]]
   2.117 -      by (auto simp add: eventually_within_less dist_real_def intro!:  exI[of _ "a - g z"])
   2.118 -    with Q show "eventually (\<lambda>x. z \<le> f x) (at_left a)"
   2.119 -      by eventually_elim (metis bij `P z` mono)
   2.120 -  qed
   2.121 -qed
   2.122 -
   2.123  lemma filterlim_at_infinity:
   2.124    fixes f :: "_ \<Rightarrow> 'a\<Colon>real_normed_vector"
   2.125    assumes "0 \<le> c"
   2.126 @@ -607,13 +507,6 @@
   2.127    qed
   2.128  qed force
   2.129  
   2.130 -lemma filterlim_real_sequentially: "LIM x sequentially. real x :> at_top"
   2.131 -  unfolding filterlim_at_top
   2.132 -  apply (intro allI)
   2.133 -  apply (rule_tac c="natceiling (Z + 1)" in eventually_sequentiallyI)
   2.134 -  apply (auto simp: natceiling_le_eq)
   2.135 -  done
   2.136 -
   2.137  subsection {* Relate @{const at}, @{const at_left} and @{const at_right} *}
   2.138  
   2.139  text {*
     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/src/HOL/Metric_Spaces.thy	Fri Mar 22 10:41:43 2013 +0100
     3.3 @@ -0,0 +1,573 @@
     3.4 +(*  Title:      HOL/Metric_Spaces.thy
     3.5 +    Author:     Brian Huffman
     3.6 +    Author:     Johannes Hölzl
     3.7 +*)
     3.8 +
     3.9 +header {* Metric Spaces *}
    3.10 +
    3.11 +theory Metric_Spaces
    3.12 +imports RComplete Topological_Spaces
    3.13 +begin
    3.14 +
    3.15 +
    3.16 +subsection {* Metric spaces *}
    3.17 +
    3.18 +class dist =
    3.19 +  fixes dist :: "'a \<Rightarrow> 'a \<Rightarrow> real"
    3.20 +
    3.21 +class open_dist = "open" + dist +
    3.22 +  assumes open_dist: "open S \<longleftrightarrow> (\<forall>x\<in>S. \<exists>e>0. \<forall>y. dist y x < e \<longrightarrow> y \<in> S)"
    3.23 +
    3.24 +class metric_space = open_dist +
    3.25 +  assumes dist_eq_0_iff [simp]: "dist x y = 0 \<longleftrightarrow> x = y"
    3.26 +  assumes dist_triangle2: "dist x y \<le> dist x z + dist y z"
    3.27 +begin
    3.28 +
    3.29 +lemma dist_self [simp]: "dist x x = 0"
    3.30 +by simp
    3.31 +
    3.32 +lemma zero_le_dist [simp]: "0 \<le> dist x y"
    3.33 +using dist_triangle2 [of x x y] by simp
    3.34 +
    3.35 +lemma zero_less_dist_iff: "0 < dist x y \<longleftrightarrow> x \<noteq> y"
    3.36 +by (simp add: less_le)
    3.37 +
    3.38 +lemma dist_not_less_zero [simp]: "\<not> dist x y < 0"
    3.39 +by (simp add: not_less)
    3.40 +
    3.41 +lemma dist_le_zero_iff [simp]: "dist x y \<le> 0 \<longleftrightarrow> x = y"
    3.42 +by (simp add: le_less)
    3.43 +
    3.44 +lemma dist_commute: "dist x y = dist y x"
    3.45 +proof (rule order_antisym)
    3.46 +  show "dist x y \<le> dist y x"
    3.47 +    using dist_triangle2 [of x y x] by simp
    3.48 +  show "dist y x \<le> dist x y"
    3.49 +    using dist_triangle2 [of y x y] by simp
    3.50 +qed
    3.51 +
    3.52 +lemma dist_triangle: "dist x z \<le> dist x y + dist y z"
    3.53 +using dist_triangle2 [of x z y] by (simp add: dist_commute)
    3.54 +
    3.55 +lemma dist_triangle3: "dist x y \<le> dist a x + dist a y"
    3.56 +using dist_triangle2 [of x y a] by (simp add: dist_commute)
    3.57 +
    3.58 +lemma dist_triangle_alt:
    3.59 +  shows "dist y z <= dist x y + dist x z"
    3.60 +by (rule dist_triangle3)
    3.61 +
    3.62 +lemma dist_pos_lt:
    3.63 +  shows "x \<noteq> y ==> 0 < dist x y"
    3.64 +by (simp add: zero_less_dist_iff)
    3.65 +
    3.66 +lemma dist_nz:
    3.67 +  shows "x \<noteq> y \<longleftrightarrow> 0 < dist x y"
    3.68 +by (simp add: zero_less_dist_iff)
    3.69 +
    3.70 +lemma dist_triangle_le:
    3.71 +  shows "dist x z + dist y z <= e \<Longrightarrow> dist x y <= e"
    3.72 +by (rule order_trans [OF dist_triangle2])
    3.73 +
    3.74 +lemma dist_triangle_lt:
    3.75 +  shows "dist x z + dist y z < e ==> dist x y < e"
    3.76 +by (rule le_less_trans [OF dist_triangle2])
    3.77 +
    3.78 +lemma dist_triangle_half_l:
    3.79 +  shows "dist x1 y < e / 2 \<Longrightarrow> dist x2 y < e / 2 \<Longrightarrow> dist x1 x2 < e"
    3.80 +by (rule dist_triangle_lt [where z=y], simp)
    3.81 +
    3.82 +lemma dist_triangle_half_r:
    3.83 +  shows "dist y x1 < e / 2 \<Longrightarrow> dist y x2 < e / 2 \<Longrightarrow> dist x1 x2 < e"
    3.84 +by (rule dist_triangle_half_l, simp_all add: dist_commute)
    3.85 +
    3.86 +subclass topological_space
    3.87 +proof
    3.88 +  have "\<exists>e::real. 0 < e"
    3.89 +    by (fast intro: zero_less_one)
    3.90 +  then show "open UNIV"
    3.91 +    unfolding open_dist by simp
    3.92 +next
    3.93 +  fix S T assume "open S" "open T"
    3.94 +  then show "open (S \<inter> T)"
    3.95 +    unfolding open_dist
    3.96 +    apply clarify
    3.97 +    apply (drule (1) bspec)+
    3.98 +    apply (clarify, rename_tac r s)
    3.99 +    apply (rule_tac x="min r s" in exI, simp)
   3.100 +    done
   3.101 +next
   3.102 +  fix K assume "\<forall>S\<in>K. open S" thus "open (\<Union>K)"
   3.103 +    unfolding open_dist by fast
   3.104 +qed
   3.105 +
   3.106 +lemma (in metric_space) open_ball: "open {y. dist x y < d}"
   3.107 +proof (unfold open_dist, intro ballI)
   3.108 +  fix y assume *: "y \<in> {y. dist x y < d}"
   3.109 +  then show "\<exists>e>0. \<forall>z. dist z y < e \<longrightarrow> z \<in> {y. dist x y < d}"
   3.110 +    by (auto intro!: exI[of _ "d - dist x y"] simp: field_simps dist_triangle_lt)
   3.111 +qed
   3.112 +
   3.113 +end
   3.114 +
   3.115 +instance metric_space \<subseteq> t2_space
   3.116 +proof
   3.117 +  fix x y :: "'a::metric_space"
   3.118 +  assume xy: "x \<noteq> y"
   3.119 +  let ?U = "{y'. dist x y' < dist x y / 2}"
   3.120 +  let ?V = "{x'. dist y x' < dist x y / 2}"
   3.121 +  have th0: "\<And>d x y z. (d x z :: real) \<le> d x y + d y z \<Longrightarrow> d y z = d z y
   3.122 +               \<Longrightarrow> \<not>(d x y * 2 < d x z \<and> d z y * 2 < d x z)" by arith
   3.123 +  have "open ?U \<and> open ?V \<and> x \<in> ?U \<and> y \<in> ?V \<and> ?U \<inter> ?V = {}"
   3.124 +    using dist_pos_lt[OF xy] th0[of dist, OF dist_triangle dist_commute]
   3.125 +    using open_ball[of _ "dist x y / 2"] by auto
   3.126 +  then show "\<exists>U V. open U \<and> open V \<and> x \<in> U \<and> y \<in> V \<and> U \<inter> V = {}"
   3.127 +    by blast
   3.128 +qed
   3.129 +
   3.130 +lemma eventually_nhds_metric:
   3.131 +  fixes a :: "'a :: metric_space"
   3.132 +  shows "eventually P (nhds a) \<longleftrightarrow> (\<exists>d>0. \<forall>x. dist x a < d \<longrightarrow> P x)"
   3.133 +unfolding eventually_nhds open_dist
   3.134 +apply safe
   3.135 +apply fast
   3.136 +apply (rule_tac x="{x. dist x a < d}" in exI, simp)
   3.137 +apply clarsimp
   3.138 +apply (rule_tac x="d - dist x a" in exI, clarsimp)
   3.139 +apply (simp only: less_diff_eq)
   3.140 +apply (erule le_less_trans [OF dist_triangle])
   3.141 +done
   3.142 +
   3.143 +lemma eventually_at:
   3.144 +  fixes a :: "'a::metric_space"
   3.145 +  shows "eventually P (at a) \<longleftrightarrow> (\<exists>d>0. \<forall>x. x \<noteq> a \<and> dist x a < d \<longrightarrow> P x)"
   3.146 +unfolding at_def eventually_within eventually_nhds_metric by auto
   3.147 +
   3.148 +lemma eventually_within_less: (* COPY FROM Topo/eventually_within *)
   3.149 +  fixes a :: "'a :: metric_space"
   3.150 +  shows "eventually P (at a within S) \<longleftrightarrow> (\<exists>d>0. \<forall>x\<in>S. 0 < dist x a \<and> dist x a < d \<longrightarrow> P x)"
   3.151 +  unfolding eventually_within eventually_at dist_nz by auto
   3.152 +
   3.153 +lemma eventually_within_le: (* COPY FROM Topo/eventually_within_le *)
   3.154 +  fixes a :: "'a :: metric_space"
   3.155 +  shows "eventually P (at a within S) \<longleftrightarrow> (\<exists>d>0. \<forall>x\<in>S. 0 < dist x a \<and> dist x a <= d \<longrightarrow> P x)"
   3.156 +  unfolding eventually_within_less by auto (metis dense order_le_less_trans)
   3.157 +
   3.158 +lemma tendstoI:
   3.159 +  fixes l :: "'a :: metric_space"
   3.160 +  assumes "\<And>e. 0 < e \<Longrightarrow> eventually (\<lambda>x. dist (f x) l < e) F"
   3.161 +  shows "(f ---> l) F"
   3.162 +  apply (rule topological_tendstoI)
   3.163 +  apply (simp add: open_dist)
   3.164 +  apply (drule (1) bspec, clarify)
   3.165 +  apply (drule assms)
   3.166 +  apply (erule eventually_elim1, simp)
   3.167 +  done
   3.168 +
   3.169 +lemma tendstoD:
   3.170 +  fixes l :: "'a :: metric_space"
   3.171 +  shows "(f ---> l) F \<Longrightarrow> 0 < e \<Longrightarrow> eventually (\<lambda>x. dist (f x) l < e) F"
   3.172 +  apply (drule_tac S="{x. dist x l < e}" in topological_tendstoD)
   3.173 +  apply (clarsimp simp add: open_dist)
   3.174 +  apply (rule_tac x="e - dist x l" in exI, clarsimp)
   3.175 +  apply (simp only: less_diff_eq)
   3.176 +  apply (erule le_less_trans [OF dist_triangle])
   3.177 +  apply simp
   3.178 +  apply simp
   3.179 +  done
   3.180 +
   3.181 +lemma tendsto_iff:
   3.182 +  fixes l :: "'a :: metric_space"
   3.183 +  shows "(f ---> l) F \<longleftrightarrow> (\<forall>e>0. eventually (\<lambda>x. dist (f x) l < e) F)"
   3.184 +  using tendstoI tendstoD by fast
   3.185 +
   3.186 +lemma metric_tendsto_imp_tendsto:
   3.187 +  fixes a :: "'a :: metric_space" and b :: "'b :: metric_space"
   3.188 +  assumes f: "(f ---> a) F"
   3.189 +  assumes le: "eventually (\<lambda>x. dist (g x) b \<le> dist (f x) a) F"
   3.190 +  shows "(g ---> b) F"
   3.191 +proof (rule tendstoI)
   3.192 +  fix e :: real assume "0 < e"
   3.193 +  with f have "eventually (\<lambda>x. dist (f x) a < e) F" by (rule tendstoD)
   3.194 +  with le show "eventually (\<lambda>x. dist (g x) b < e) F"
   3.195 +    using le_less_trans by (rule eventually_elim2)
   3.196 +qed
   3.197 +
   3.198 +lemma filterlim_real_sequentially: "LIM x sequentially. real x :> at_top"
   3.199 +  unfolding filterlim_at_top
   3.200 +  apply (intro allI)
   3.201 +  apply (rule_tac c="natceiling (Z + 1)" in eventually_sequentiallyI)
   3.202 +  apply (auto simp: natceiling_le_eq)
   3.203 +  done
   3.204 +
   3.205 +subsubsection {* Limits of Sequences *}
   3.206 +
   3.207 +lemma LIMSEQ_def: "X ----> (L::'a::metric_space) \<longleftrightarrow> (\<forall>r>0. \<exists>no. \<forall>n\<ge>no. dist (X n) L < r)"
   3.208 +  unfolding tendsto_iff eventually_sequentially ..
   3.209 +
   3.210 +lemma LIMSEQ_iff_nz: "X ----> (L::'a::metric_space) = (\<forall>r>0. \<exists>no>0. \<forall>n\<ge>no. dist (X n) L < r)"
   3.211 +  unfolding LIMSEQ_def by (metis Suc_leD zero_less_Suc)
   3.212 +
   3.213 +lemma metric_LIMSEQ_I:
   3.214 +  "(\<And>r. 0 < r \<Longrightarrow> \<exists>no. \<forall>n\<ge>no. dist (X n) L < r) \<Longrightarrow> X ----> (L::'a::metric_space)"
   3.215 +by (simp add: LIMSEQ_def)
   3.216 +
   3.217 +lemma metric_LIMSEQ_D:
   3.218 +  "\<lbrakk>X ----> (L::'a::metric_space); 0 < r\<rbrakk> \<Longrightarrow> \<exists>no. \<forall>n\<ge>no. dist (X n) L < r"
   3.219 +by (simp add: LIMSEQ_def)
   3.220 +
   3.221 +
   3.222 +subsubsection {* Limits of Functions *}
   3.223 +
   3.224 +lemma LIM_def: "f -- (a::'a::metric_space) --> (L::'b::metric_space) =
   3.225 +     (\<forall>r > 0. \<exists>s > 0. \<forall>x. x \<noteq> a & dist x a < s
   3.226 +        --> dist (f x) L < r)"
   3.227 +unfolding tendsto_iff eventually_at ..
   3.228 +
   3.229 +lemma metric_LIM_I:
   3.230 +  "(\<And>r. 0 < r \<Longrightarrow> \<exists>s>0. \<forall>x. x \<noteq> a \<and> dist x a < s \<longrightarrow> dist (f x) L < r)
   3.231 +    \<Longrightarrow> f -- (a::'a::metric_space) --> (L::'b::metric_space)"
   3.232 +by (simp add: LIM_def)
   3.233 +
   3.234 +lemma metric_LIM_D:
   3.235 +  "\<lbrakk>f -- (a::'a::metric_space) --> (L::'b::metric_space); 0 < r\<rbrakk>
   3.236 +    \<Longrightarrow> \<exists>s>0. \<forall>x. x \<noteq> a \<and> dist x a < s \<longrightarrow> dist (f x) L < r"
   3.237 +by (simp add: LIM_def)
   3.238 +
   3.239 +lemma metric_LIM_imp_LIM:
   3.240 +  assumes f: "f -- a --> (l::'a::metric_space)"
   3.241 +  assumes le: "\<And>x. x \<noteq> a \<Longrightarrow> dist (g x) m \<le> dist (f x) l"
   3.242 +  shows "g -- a --> (m::'b::metric_space)"
   3.243 +  by (rule metric_tendsto_imp_tendsto [OF f]) (auto simp add: eventually_at_topological le)
   3.244 +
   3.245 +lemma metric_LIM_equal2:
   3.246 +  assumes 1: "0 < R"
   3.247 +  assumes 2: "\<And>x. \<lbrakk>x \<noteq> a; dist x a < R\<rbrakk> \<Longrightarrow> f x = g x"
   3.248 +  shows "g -- a --> l \<Longrightarrow> f -- (a::'a::metric_space) --> l"
   3.249 +apply (rule topological_tendstoI)
   3.250 +apply (drule (2) topological_tendstoD)
   3.251 +apply (simp add: eventually_at, safe)
   3.252 +apply (rule_tac x="min d R" in exI, safe)
   3.253 +apply (simp add: 1)
   3.254 +apply (simp add: 2)
   3.255 +done
   3.256 +
   3.257 +lemma metric_LIM_compose2:
   3.258 +  assumes f: "f -- (a::'a::metric_space) --> b"
   3.259 +  assumes g: "g -- b --> c"
   3.260 +  assumes inj: "\<exists>d>0. \<forall>x. x \<noteq> a \<and> dist x a < d \<longrightarrow> f x \<noteq> b"
   3.261 +  shows "(\<lambda>x. g (f x)) -- a --> c"
   3.262 +  using g f inj [folded eventually_at]
   3.263 +  by (rule tendsto_compose_eventually)
   3.264 +
   3.265 +lemma metric_isCont_LIM_compose2:
   3.266 +  fixes f :: "'a :: metric_space \<Rightarrow> _"
   3.267 +  assumes f [unfolded isCont_def]: "isCont f a"
   3.268 +  assumes g: "g -- f a --> l"
   3.269 +  assumes inj: "\<exists>d>0. \<forall>x. x \<noteq> a \<and> dist x a < d \<longrightarrow> f x \<noteq> f a"
   3.270 +  shows "(\<lambda>x. g (f x)) -- a --> l"
   3.271 +by (rule metric_LIM_compose2 [OF f g inj])
   3.272 +
   3.273 +subsection {* Complete metric spaces *}
   3.274 +
   3.275 +subsection {* Cauchy sequences *}
   3.276 +
   3.277 +definition (in metric_space) Cauchy :: "(nat \<Rightarrow> 'a) \<Rightarrow> bool" where
   3.278 +  "Cauchy X = (\<forall>e>0. \<exists>M. \<forall>m \<ge> M. \<forall>n \<ge> M. dist (X m) (X n) < e)"
   3.279 +
   3.280 +subsection {* Cauchy Sequences *}
   3.281 +
   3.282 +lemma metric_CauchyI:
   3.283 +  "(\<And>e. 0 < e \<Longrightarrow> \<exists>M. \<forall>m\<ge>M. \<forall>n\<ge>M. dist (X m) (X n) < e) \<Longrightarrow> Cauchy X"
   3.284 +  by (simp add: Cauchy_def)
   3.285 +
   3.286 +lemma metric_CauchyD:
   3.287 +  "Cauchy X \<Longrightarrow> 0 < e \<Longrightarrow> \<exists>M. \<forall>m\<ge>M. \<forall>n\<ge>M. dist (X m) (X n) < e"
   3.288 +  by (simp add: Cauchy_def)
   3.289 +
   3.290 +lemma metric_Cauchy_iff2:
   3.291 +  "Cauchy X = (\<forall>j. (\<exists>M. \<forall>m \<ge> M. \<forall>n \<ge> M. dist (X m) (X n) < inverse(real (Suc j))))"
   3.292 +apply (simp add: Cauchy_def, auto)
   3.293 +apply (drule reals_Archimedean, safe)
   3.294 +apply (drule_tac x = n in spec, auto)
   3.295 +apply (rule_tac x = M in exI, auto)
   3.296 +apply (drule_tac x = m in spec, simp)
   3.297 +apply (drule_tac x = na in spec, auto)
   3.298 +done
   3.299 +
   3.300 +lemma Cauchy_subseq_Cauchy:
   3.301 +  "\<lbrakk> Cauchy X; subseq f \<rbrakk> \<Longrightarrow> Cauchy (X o f)"
   3.302 +apply (auto simp add: Cauchy_def)
   3.303 +apply (drule_tac x=e in spec, clarify)
   3.304 +apply (rule_tac x=M in exI, clarify)
   3.305 +apply (blast intro: le_trans [OF _ seq_suble] dest!: spec)
   3.306 +done
   3.307 +
   3.308 +
   3.309 +subsubsection {* Cauchy Sequences are Convergent *}
   3.310 +
   3.311 +class complete_space = metric_space +
   3.312 +  assumes Cauchy_convergent: "Cauchy X \<Longrightarrow> convergent X"
   3.313 +
   3.314 +theorem LIMSEQ_imp_Cauchy:
   3.315 +  assumes X: "X ----> a" shows "Cauchy X"
   3.316 +proof (rule metric_CauchyI)
   3.317 +  fix e::real assume "0 < e"
   3.318 +  hence "0 < e/2" by simp
   3.319 +  with X have "\<exists>N. \<forall>n\<ge>N. dist (X n) a < e/2" by (rule metric_LIMSEQ_D)
   3.320 +  then obtain N where N: "\<forall>n\<ge>N. dist (X n) a < e/2" ..
   3.321 +  show "\<exists>N. \<forall>m\<ge>N. \<forall>n\<ge>N. dist (X m) (X n) < e"
   3.322 +  proof (intro exI allI impI)
   3.323 +    fix m assume "N \<le> m"
   3.324 +    hence m: "dist (X m) a < e/2" using N by fast
   3.325 +    fix n assume "N \<le> n"
   3.326 +    hence n: "dist (X n) a < e/2" using N by fast
   3.327 +    have "dist (X m) (X n) \<le> dist (X m) a + dist (X n) a"
   3.328 +      by (rule dist_triangle2)
   3.329 +    also from m n have "\<dots> < e" by simp
   3.330 +    finally show "dist (X m) (X n) < e" .
   3.331 +  qed
   3.332 +qed
   3.333 +
   3.334 +lemma convergent_Cauchy: "convergent X \<Longrightarrow> Cauchy X"
   3.335 +unfolding convergent_def
   3.336 +by (erule exE, erule LIMSEQ_imp_Cauchy)
   3.337 +
   3.338 +lemma Cauchy_convergent_iff:
   3.339 +  fixes X :: "nat \<Rightarrow> 'a::complete_space"
   3.340 +  shows "Cauchy X = convergent X"
   3.341 +by (fast intro: Cauchy_convergent convergent_Cauchy)
   3.342 +
   3.343 +subsection {* Uniform Continuity *}
   3.344 +
   3.345 +definition
   3.346 +  isUCont :: "['a::metric_space \<Rightarrow> 'b::metric_space] \<Rightarrow> bool" where
   3.347 +  "isUCont f = (\<forall>r>0. \<exists>s>0. \<forall>x y. dist x y < s \<longrightarrow> dist (f x) (f y) < r)"
   3.348 +
   3.349 +lemma isUCont_isCont: "isUCont f ==> isCont f x"
   3.350 +by (simp add: isUCont_def isCont_def LIM_def, force)
   3.351 +
   3.352 +lemma isUCont_Cauchy:
   3.353 +  "\<lbrakk>isUCont f; Cauchy X\<rbrakk> \<Longrightarrow> Cauchy (\<lambda>n. f (X n))"
   3.354 +unfolding isUCont_def
   3.355 +apply (rule metric_CauchyI)
   3.356 +apply (drule_tac x=e in spec, safe)
   3.357 +apply (drule_tac e=s in metric_CauchyD, safe)
   3.358 +apply (rule_tac x=M in exI, simp)
   3.359 +done
   3.360 +
   3.361 +subsection {* The set of real numbers is a complete metric space *}
   3.362 +
   3.363 +instantiation real :: metric_space
   3.364 +begin
   3.365 +
   3.366 +definition dist_real_def:
   3.367 +  "dist x y = \<bar>x - y\<bar>"
   3.368 +
   3.369 +definition open_real_def:
   3.370 +  "open (S :: real set) \<longleftrightarrow> (\<forall>x\<in>S. \<exists>e>0. \<forall>y. dist y x < e \<longrightarrow> y \<in> S)"
   3.371 +
   3.372 +instance
   3.373 +  by default (auto simp: open_real_def dist_real_def)
   3.374 +end
   3.375 +
   3.376 +instance real :: linorder_topology
   3.377 +proof
   3.378 +  show "(open :: real set \<Rightarrow> bool) = generate_topology (range lessThan \<union> range greaterThan)"
   3.379 +  proof (rule ext, safe)
   3.380 +    fix S :: "real set" assume "open S"
   3.381 +    then guess f unfolding open_real_def bchoice_iff ..
   3.382 +    then have *: "S = (\<Union>x\<in>S. {x - f x <..} \<inter> {..< x + f x})"
   3.383 +      by (fastforce simp: dist_real_def)
   3.384 +    show "generate_topology (range lessThan \<union> range greaterThan) S"
   3.385 +      apply (subst *)
   3.386 +      apply (intro generate_topology_Union generate_topology.Int)
   3.387 +      apply (auto intro: generate_topology.Basis)
   3.388 +      done
   3.389 +  next
   3.390 +    fix S :: "real set" assume "generate_topology (range lessThan \<union> range greaterThan) S"
   3.391 +    moreover have "\<And>a::real. open {..<a}"
   3.392 +      unfolding open_real_def dist_real_def
   3.393 +    proof clarify
   3.394 +      fix x a :: real assume "x < a"
   3.395 +      hence "0 < a - x \<and> (\<forall>y. \<bar>y - x\<bar> < a - x \<longrightarrow> y \<in> {..<a})" by auto
   3.396 +      thus "\<exists>e>0. \<forall>y. \<bar>y - x\<bar> < e \<longrightarrow> y \<in> {..<a}" ..
   3.397 +    qed
   3.398 +    moreover have "\<And>a::real. open {a <..}"
   3.399 +      unfolding open_real_def dist_real_def
   3.400 +    proof clarify
   3.401 +      fix x a :: real assume "a < x"
   3.402 +      hence "0 < x - a \<and> (\<forall>y. \<bar>y - x\<bar> < x - a \<longrightarrow> y \<in> {a<..})" by auto
   3.403 +      thus "\<exists>e>0. \<forall>y. \<bar>y - x\<bar> < e \<longrightarrow> y \<in> {a<..}" ..
   3.404 +    qed
   3.405 +    ultimately show "open S"
   3.406 +      by induct auto
   3.407 +  qed
   3.408 +qed
   3.409 +
   3.410 +lemmas open_real_greaterThan = open_greaterThan[where 'a=real]
   3.411 +lemmas open_real_lessThan = open_lessThan[where 'a=real]
   3.412 +lemmas open_real_greaterThanLessThan = open_greaterThanLessThan[where 'a=real]
   3.413 +lemmas closed_real_atMost = closed_atMost[where 'a=real]
   3.414 +lemmas closed_real_atLeast = closed_atLeast[where 'a=real]
   3.415 +lemmas closed_real_atLeastAtMost = closed_atLeastAtMost[where 'a=real]
   3.416 +
   3.417 +text {*
   3.418 +Proof that Cauchy sequences converge based on the one from
   3.419 +http://pirate.shu.edu/~wachsmut/ira/numseq/proofs/cauconv.html
   3.420 +*}
   3.421 +
   3.422 +text {*
   3.423 +  If sequence @{term "X"} is Cauchy, then its limit is the lub of
   3.424 +  @{term "{r::real. \<exists>N. \<forall>n\<ge>N. r < X n}"}
   3.425 +*}
   3.426 +
   3.427 +lemma isUb_UNIV_I: "(\<And>y. y \<in> S \<Longrightarrow> y \<le> u) \<Longrightarrow> isUb UNIV S u"
   3.428 +by (simp add: isUbI setleI)
   3.429 +
   3.430 +lemma increasing_LIMSEQ:
   3.431 +  fixes f :: "nat \<Rightarrow> real"
   3.432 +  assumes inc: "\<And>n. f n \<le> f (Suc n)"
   3.433 +      and bdd: "\<And>n. f n \<le> l"
   3.434 +      and en: "\<And>e. 0 < e \<Longrightarrow> \<exists>n. l \<le> f n + e"
   3.435 +  shows "f ----> l"
   3.436 +proof (rule increasing_tendsto)
   3.437 +  fix x assume "x < l"
   3.438 +  with dense[of 0 "l - x"] obtain e where "0 < e" "e < l - x"
   3.439 +    by auto
   3.440 +  from en[OF `0 < e`] obtain n where "l - e \<le> f n"
   3.441 +    by (auto simp: field_simps)
   3.442 +  with `e < l - x` `0 < e` have "x < f n" by simp
   3.443 +  with incseq_SucI[of f, OF inc] show "eventually (\<lambda>n. x < f n) sequentially"
   3.444 +    by (auto simp: eventually_sequentially incseq_def intro: less_le_trans)
   3.445 +qed (insert bdd, auto)
   3.446 +
   3.447 +lemma real_Cauchy_convergent:
   3.448 +  fixes X :: "nat \<Rightarrow> real"
   3.449 +  assumes X: "Cauchy X"
   3.450 +  shows "convergent X"
   3.451 +proof -
   3.452 +  def S \<equiv> "{x::real. \<exists>N. \<forall>n\<ge>N. x < X n}"
   3.453 +  then have mem_S: "\<And>N x. \<forall>n\<ge>N. x < X n \<Longrightarrow> x \<in> S" by auto
   3.454 +
   3.455 +  { fix N x assume N: "\<forall>n\<ge>N. X n < x"
   3.456 +  have "isUb UNIV S x"
   3.457 +  proof (rule isUb_UNIV_I)
   3.458 +  fix y::real assume "y \<in> S"
   3.459 +  hence "\<exists>M. \<forall>n\<ge>M. y < X n"
   3.460 +    by (simp add: S_def)
   3.461 +  then obtain M where "\<forall>n\<ge>M. y < X n" ..
   3.462 +  hence "y < X (max M N)" by simp
   3.463 +  also have "\<dots> < x" using N by simp
   3.464 +  finally show "y \<le> x"
   3.465 +    by (rule order_less_imp_le)
   3.466 +  qed }
   3.467 +  note bound_isUb = this 
   3.468 +
   3.469 +  have "\<exists>u. isLub UNIV S u"
   3.470 +  proof (rule reals_complete)
   3.471 +  obtain N where "\<forall>m\<ge>N. \<forall>n\<ge>N. dist (X m) (X n) < 1"
   3.472 +    using X[THEN metric_CauchyD, OF zero_less_one] by auto
   3.473 +  hence N: "\<forall>n\<ge>N. dist (X n) (X N) < 1" by simp
   3.474 +  show "\<exists>x. x \<in> S"
   3.475 +  proof
   3.476 +    from N have "\<forall>n\<ge>N. X N - 1 < X n"
   3.477 +      by (simp add: abs_diff_less_iff dist_real_def)
   3.478 +    thus "X N - 1 \<in> S" by (rule mem_S)
   3.479 +  qed
   3.480 +  show "\<exists>u. isUb UNIV S u"
   3.481 +  proof
   3.482 +    from N have "\<forall>n\<ge>N. X n < X N + 1"
   3.483 +      by (simp add: abs_diff_less_iff dist_real_def)
   3.484 +    thus "isUb UNIV S (X N + 1)"
   3.485 +      by (rule bound_isUb)
   3.486 +  qed
   3.487 +  qed
   3.488 +  then obtain x where x: "isLub UNIV S x" ..
   3.489 +  have "X ----> x"
   3.490 +  proof (rule metric_LIMSEQ_I)
   3.491 +  fix r::real assume "0 < r"
   3.492 +  hence r: "0 < r/2" by simp
   3.493 +  obtain N where "\<forall>n\<ge>N. \<forall>m\<ge>N. dist (X n) (X m) < r/2"
   3.494 +    using metric_CauchyD [OF X r] by auto
   3.495 +  hence "\<forall>n\<ge>N. dist (X n) (X N) < r/2" by simp
   3.496 +  hence N: "\<forall>n\<ge>N. X N - r/2 < X n \<and> X n < X N + r/2"
   3.497 +    by (simp only: dist_real_def abs_diff_less_iff)
   3.498 +
   3.499 +  from N have "\<forall>n\<ge>N. X N - r/2 < X n" by fast
   3.500 +  hence "X N - r/2 \<in> S" by (rule mem_S)
   3.501 +  hence 1: "X N - r/2 \<le> x" using x isLub_isUb isUbD by fast
   3.502 +
   3.503 +  from N have "\<forall>n\<ge>N. X n < X N + r/2" by fast
   3.504 +  hence "isUb UNIV S (X N + r/2)" by (rule bound_isUb)
   3.505 +  hence 2: "x \<le> X N + r/2" using x isLub_le_isUb by fast
   3.506 +
   3.507 +  show "\<exists>N. \<forall>n\<ge>N. dist (X n) x < r"
   3.508 +  proof (intro exI allI impI)
   3.509 +    fix n assume n: "N \<le> n"
   3.510 +    from N n have "X n < X N + r/2" and "X N - r/2 < X n" by simp+
   3.511 +    thus "dist (X n) x < r" using 1 2
   3.512 +      by (simp add: abs_diff_less_iff dist_real_def)
   3.513 +  qed
   3.514 +  qed
   3.515 +  then show ?thesis unfolding convergent_def by auto
   3.516 +qed
   3.517 +
   3.518 +instance real :: complete_space
   3.519 +  by intro_classes (rule real_Cauchy_convergent)
   3.520 +
   3.521 +lemma tendsto_dist [tendsto_intros]:
   3.522 +  fixes l m :: "'a :: metric_space"
   3.523 +  assumes f: "(f ---> l) F" and g: "(g ---> m) F"
   3.524 +  shows "((\<lambda>x. dist (f x) (g x)) ---> dist l m) F"
   3.525 +proof (rule tendstoI)
   3.526 +  fix e :: real assume "0 < e"
   3.527 +  hence e2: "0 < e/2" by simp
   3.528 +  from tendstoD [OF f e2] tendstoD [OF g e2]
   3.529 +  show "eventually (\<lambda>x. dist (dist (f x) (g x)) (dist l m) < e) F"
   3.530 +  proof (eventually_elim)
   3.531 +    case (elim x)
   3.532 +    then show "dist (dist (f x) (g x)) (dist l m) < e"
   3.533 +      unfolding dist_real_def
   3.534 +      using dist_triangle2 [of "f x" "g x" "l"]
   3.535 +      using dist_triangle2 [of "g x" "l" "m"]
   3.536 +      using dist_triangle3 [of "l" "m" "f x"]
   3.537 +      using dist_triangle [of "f x" "m" "g x"]
   3.538 +      by arith
   3.539 +  qed
   3.540 +qed
   3.541 +
   3.542 +lemma tendsto_at_topI_sequentially:
   3.543 +  fixes f :: "real \<Rightarrow> real"
   3.544 +  assumes mono: "mono f"
   3.545 +  assumes limseq: "(\<lambda>n. f (real n)) ----> y"
   3.546 +  shows "(f ---> y) at_top"
   3.547 +proof (rule tendstoI)
   3.548 +  fix e :: real assume "0 < e"
   3.549 +  with limseq obtain N :: nat where N: "\<And>n. N \<le> n \<Longrightarrow> \<bar>f (real n) - y\<bar> < e"
   3.550 +    by (auto simp: LIMSEQ_def dist_real_def)
   3.551 +  { fix x :: real
   3.552 +    from ex_le_of_nat[of x] guess n ..
   3.553 +    note monoD[OF mono this]
   3.554 +    also have "f (real_of_nat n) \<le> y"
   3.555 +      by (rule LIMSEQ_le_const[OF limseq])
   3.556 +         (auto intro: exI[of _ n] monoD[OF mono] simp: real_eq_of_nat[symmetric])
   3.557 +    finally have "f x \<le> y" . }
   3.558 +  note le = this
   3.559 +  have "eventually (\<lambda>x. real N \<le> x) at_top"
   3.560 +    by (rule eventually_ge_at_top)
   3.561 +  then show "eventually (\<lambda>x. dist (f x) y < e) at_top"
   3.562 +  proof eventually_elim
   3.563 +    fix x assume N': "real N \<le> x"
   3.564 +    with N[of N] le have "y - f (real N) < e" by auto
   3.565 +    moreover note monoD[OF mono N']
   3.566 +    ultimately show "dist (f x) y < e"
   3.567 +      using le[of x] by (auto simp: dist_real_def field_simps)
   3.568 +  qed
   3.569 +qed
   3.570 +
   3.571 +lemma Cauchy_iff2:
   3.572 +  "Cauchy X = (\<forall>j. (\<exists>M. \<forall>m \<ge> M. \<forall>n \<ge> M. \<bar>X m - X n\<bar> < inverse(real (Suc j))))"
   3.573 +  unfolding metric_Cauchy_iff2 dist_real_def ..
   3.574 +
   3.575 +end
   3.576 +
     4.1 --- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Fri Mar 22 10:41:42 2013 +0100
     4.2 +++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Fri Mar 22 10:41:43 2013 +0100
     4.3 @@ -1416,7 +1416,7 @@
     4.4    unfolding tendsto_def Limits.eventually_within by simp
     4.5  
     4.6  lemma Lim_within_subset: "(f ---> l) (net within S) \<Longrightarrow> T \<subseteq> S \<Longrightarrow> (f ---> l) (net within T)"
     4.7 -  unfolding tendsto_def Limits.eventually_within
     4.8 +  unfolding tendsto_def Topological_Spaces.eventually_within
     4.9    by (auto elim!: eventually_elim1)
    4.10  
    4.11  lemma Lim_Un: assumes "(f ---> l) (net within S)" "(f ---> l) (net within T)"
    4.12 @@ -4667,7 +4667,7 @@
    4.13    hence "eventually (\<lambda>y. f y \<noteq> a) (at x within s)"
    4.14      using `a \<notin> U` by (fast elim: eventually_mono [rotated])
    4.15    thus ?thesis
    4.16 -    unfolding Limits.eventually_within Limits.eventually_at
    4.17 +    unfolding Limits.eventually_within Metric_Spaces.eventually_at
    4.18      by (rule ex_forward, cut_tac `f x \<noteq> a`, auto simp: dist_commute)
    4.19  qed
    4.20  
     5.1 --- a/src/HOL/RealVector.thy	Fri Mar 22 10:41:42 2013 +0100
     5.2 +++ b/src/HOL/RealVector.thy	Fri Mar 22 10:41:43 2013 +0100
     5.3 @@ -5,7 +5,7 @@
     5.4  header {* Vector Spaces and Algebras over the Reals *}
     5.5  
     5.6  theory RealVector
     5.7 -imports RComplete
     5.8 +imports RComplete Metric_Spaces
     5.9  begin
    5.10  
    5.11  subsection {* Locale for additive functions *}
    5.12 @@ -434,106 +434,6 @@
    5.13    by (rule Reals_cases) auto
    5.14  
    5.15  
    5.16 -subsection {* Metric spaces *}
    5.17 -
    5.18 -class dist =
    5.19 -  fixes dist :: "'a \<Rightarrow> 'a \<Rightarrow> real"
    5.20 -
    5.21 -class open_dist = "open" + dist +
    5.22 -  assumes open_dist: "open S \<longleftrightarrow> (\<forall>x\<in>S. \<exists>e>0. \<forall>y. dist y x < e \<longrightarrow> y \<in> S)"
    5.23 -
    5.24 -class metric_space = open_dist +
    5.25 -  assumes dist_eq_0_iff [simp]: "dist x y = 0 \<longleftrightarrow> x = y"
    5.26 -  assumes dist_triangle2: "dist x y \<le> dist x z + dist y z"
    5.27 -begin
    5.28 -
    5.29 -lemma dist_self [simp]: "dist x x = 0"
    5.30 -by simp
    5.31 -
    5.32 -lemma zero_le_dist [simp]: "0 \<le> dist x y"
    5.33 -using dist_triangle2 [of x x y] by simp
    5.34 -
    5.35 -lemma zero_less_dist_iff: "0 < dist x y \<longleftrightarrow> x \<noteq> y"
    5.36 -by (simp add: less_le)
    5.37 -
    5.38 -lemma dist_not_less_zero [simp]: "\<not> dist x y < 0"
    5.39 -by (simp add: not_less)
    5.40 -
    5.41 -lemma dist_le_zero_iff [simp]: "dist x y \<le> 0 \<longleftrightarrow> x = y"
    5.42 -by (simp add: le_less)
    5.43 -
    5.44 -lemma dist_commute: "dist x y = dist y x"
    5.45 -proof (rule order_antisym)
    5.46 -  show "dist x y \<le> dist y x"
    5.47 -    using dist_triangle2 [of x y x] by simp
    5.48 -  show "dist y x \<le> dist x y"
    5.49 -    using dist_triangle2 [of y x y] by simp
    5.50 -qed
    5.51 -
    5.52 -lemma dist_triangle: "dist x z \<le> dist x y + dist y z"
    5.53 -using dist_triangle2 [of x z y] by (simp add: dist_commute)
    5.54 -
    5.55 -lemma dist_triangle3: "dist x y \<le> dist a x + dist a y"
    5.56 -using dist_triangle2 [of x y a] by (simp add: dist_commute)
    5.57 -
    5.58 -lemma dist_triangle_alt:
    5.59 -  shows "dist y z <= dist x y + dist x z"
    5.60 -by (rule dist_triangle3)
    5.61 -
    5.62 -lemma dist_pos_lt:
    5.63 -  shows "x \<noteq> y ==> 0 < dist x y"
    5.64 -by (simp add: zero_less_dist_iff)
    5.65 -
    5.66 -lemma dist_nz:
    5.67 -  shows "x \<noteq> y \<longleftrightarrow> 0 < dist x y"
    5.68 -by (simp add: zero_less_dist_iff)
    5.69 -
    5.70 -lemma dist_triangle_le:
    5.71 -  shows "dist x z + dist y z <= e \<Longrightarrow> dist x y <= e"
    5.72 -by (rule order_trans [OF dist_triangle2])
    5.73 -
    5.74 -lemma dist_triangle_lt:
    5.75 -  shows "dist x z + dist y z < e ==> dist x y < e"
    5.76 -by (rule le_less_trans [OF dist_triangle2])
    5.77 -
    5.78 -lemma dist_triangle_half_l:
    5.79 -  shows "dist x1 y < e / 2 \<Longrightarrow> dist x2 y < e / 2 \<Longrightarrow> dist x1 x2 < e"
    5.80 -by (rule dist_triangle_lt [where z=y], simp)
    5.81 -
    5.82 -lemma dist_triangle_half_r:
    5.83 -  shows "dist y x1 < e / 2 \<Longrightarrow> dist y x2 < e / 2 \<Longrightarrow> dist x1 x2 < e"
    5.84 -by (rule dist_triangle_half_l, simp_all add: dist_commute)
    5.85 -
    5.86 -subclass topological_space
    5.87 -proof
    5.88 -  have "\<exists>e::real. 0 < e"
    5.89 -    by (fast intro: zero_less_one)
    5.90 -  then show "open UNIV"
    5.91 -    unfolding open_dist by simp
    5.92 -next
    5.93 -  fix S T assume "open S" "open T"
    5.94 -  then show "open (S \<inter> T)"
    5.95 -    unfolding open_dist
    5.96 -    apply clarify
    5.97 -    apply (drule (1) bspec)+
    5.98 -    apply (clarify, rename_tac r s)
    5.99 -    apply (rule_tac x="min r s" in exI, simp)
   5.100 -    done
   5.101 -next
   5.102 -  fix K assume "\<forall>S\<in>K. open S" thus "open (\<Union>K)"
   5.103 -    unfolding open_dist by fast
   5.104 -qed
   5.105 -
   5.106 -lemma (in metric_space) open_ball: "open {y. dist x y < d}"
   5.107 -proof (unfold open_dist, intro ballI)
   5.108 -  fix y assume *: "y \<in> {y. dist x y < d}"
   5.109 -  then show "\<exists>e>0. \<forall>z. dist z y < e \<longrightarrow> z \<in> {y. dist x y < d}"
   5.110 -    by (auto intro!: exI[of _ "d - dist x y"] simp: field_simps dist_triangle_lt)
   5.111 -qed
   5.112 -
   5.113 -end
   5.114 -
   5.115 -
   5.116  subsection {* Real normed vector spaces *}
   5.117  
   5.118  class norm =
   5.119 @@ -774,16 +674,9 @@
   5.120  definition real_norm_def [simp]:
   5.121    "norm r = \<bar>r\<bar>"
   5.122  
   5.123 -definition dist_real_def:
   5.124 -  "dist x y = \<bar>x - y\<bar>"
   5.125 -
   5.126 -definition open_real_def:
   5.127 -  "open (S :: real set) \<longleftrightarrow> (\<forall>x\<in>S. \<exists>e>0. \<forall>y. dist y x < e \<longrightarrow> y \<in> S)"
   5.128 -
   5.129  instance
   5.130  apply (intro_classes, unfold real_norm_def real_scaleR_def)
   5.131  apply (rule dist_real_def)
   5.132 -apply (rule open_real_def)
   5.133  apply (simp add: sgn_real_def)
   5.134  apply (rule abs_eq_0)
   5.135  apply (rule abs_triangle_ineq)
   5.136 @@ -793,47 +686,6 @@
   5.137  
   5.138  end
   5.139  
   5.140 -instance real :: linorder_topology
   5.141 -proof
   5.142 -  show "(open :: real set \<Rightarrow> bool) = generate_topology (range lessThan \<union> range greaterThan)"
   5.143 -  proof (rule ext, safe)
   5.144 -    fix S :: "real set" assume "open S"
   5.145 -    then guess f unfolding open_real_def bchoice_iff ..
   5.146 -    then have *: "S = (\<Union>x\<in>S. {x - f x <..} \<inter> {..< x + f x})"
   5.147 -      by (fastforce simp: dist_real_def)
   5.148 -    show "generate_topology (range lessThan \<union> range greaterThan) S"
   5.149 -      apply (subst *)
   5.150 -      apply (intro generate_topology_Union generate_topology.Int)
   5.151 -      apply (auto intro: generate_topology.Basis)
   5.152 -      done
   5.153 -  next
   5.154 -    fix S :: "real set" assume "generate_topology (range lessThan \<union> range greaterThan) S"
   5.155 -    moreover have "\<And>a::real. open {..<a}"
   5.156 -      unfolding open_real_def dist_real_def
   5.157 -    proof clarify
   5.158 -      fix x a :: real assume "x < a"
   5.159 -      hence "0 < a - x \<and> (\<forall>y. \<bar>y - x\<bar> < a - x \<longrightarrow> y \<in> {..<a})" by auto
   5.160 -      thus "\<exists>e>0. \<forall>y. \<bar>y - x\<bar> < e \<longrightarrow> y \<in> {..<a}" ..
   5.161 -    qed
   5.162 -    moreover have "\<And>a::real. open {a <..}"
   5.163 -      unfolding open_real_def dist_real_def
   5.164 -    proof clarify
   5.165 -      fix x a :: real assume "a < x"
   5.166 -      hence "0 < x - a \<and> (\<forall>y. \<bar>y - x\<bar> < x - a \<longrightarrow> y \<in> {a<..})" by auto
   5.167 -      thus "\<exists>e>0. \<forall>y. \<bar>y - x\<bar> < e \<longrightarrow> y \<in> {a<..}" ..
   5.168 -    qed
   5.169 -    ultimately show "open S"
   5.170 -      by induct auto
   5.171 -  qed
   5.172 -qed
   5.173 -
   5.174 -lemmas open_real_greaterThan = open_greaterThan[where 'a=real]
   5.175 -lemmas open_real_lessThan = open_lessThan[where 'a=real]
   5.176 -lemmas open_real_greaterThanLessThan = open_greaterThanLessThan[where 'a=real]
   5.177 -lemmas closed_real_atMost = closed_atMost[where 'a=real]
   5.178 -lemmas closed_real_atLeast = closed_atLeast[where 'a=real]
   5.179 -lemmas closed_real_atLeastAtMost = closed_atLeastAtMost[where 'a=real]
   5.180 -
   5.181  subsection {* Extra type constraints *}
   5.182  
   5.183  text {* Only allow @{term "open"} in class @{text topological_space}. *}
   5.184 @@ -851,7 +703,6 @@
   5.185  setup {* Sign.add_const_constraint
   5.186    (@{const_name norm}, SOME @{typ "'a::real_normed_vector \<Rightarrow> real"}) *}
   5.187  
   5.188 -
   5.189  subsection {* Sign function *}
   5.190  
   5.191  lemma norm_sgn:
   5.192 @@ -1057,21 +908,6 @@
   5.193  lemma bounded_linear_of_real: "bounded_linear (\<lambda>r. of_real r)"
   5.194    unfolding of_real_def by (rule bounded_linear_scaleR_left)
   5.195  
   5.196 -
   5.197 -instance metric_space \<subseteq> t2_space
   5.198 -proof
   5.199 -  fix x y :: "'a::metric_space"
   5.200 -  assume xy: "x \<noteq> y"
   5.201 -  let ?U = "{y'. dist x y' < dist x y / 2}"
   5.202 -  let ?V = "{x'. dist y x' < dist x y / 2}"
   5.203 -  have th0: "\<And>d x y z. (d x z :: real) \<le> d x y + d y z \<Longrightarrow> d y z = d z y
   5.204 -               \<Longrightarrow> \<not>(d x y * 2 < d x z \<and> d z y * 2 < d x z)" by arith
   5.205 -  have "open ?U \<and> open ?V \<and> x \<in> ?U \<and> y \<in> ?V \<and> ?U \<inter> ?V = {}"
   5.206 -    using dist_pos_lt[OF xy] th0[of dist, OF dist_triangle dist_commute]
   5.207 -    using open_ball[of _ "dist x y / 2"] by auto
   5.208 -  then show "\<exists>U V. open U \<and> open V \<and> x \<in> U \<and> y \<in> V \<and> U \<inter> V = {}"
   5.209 -    by blast
   5.210 -qed
   5.211  instance real_normed_algebra_1 \<subseteq> perfect_space
   5.212  proof
   5.213    fix x::'a
     6.1 --- a/src/HOL/SEQ.thy	Fri Mar 22 10:41:42 2013 +0100
     6.2 +++ b/src/HOL/SEQ.thy	Fri Mar 22 10:41:43 2013 +0100
     6.3 @@ -20,10 +20,6 @@
     6.4      --{*Standard definition for bounded sequence*}
     6.5    "Bseq X = (\<exists>K>0.\<forall>n. norm (X n) \<le> K)"
     6.6  
     6.7 -definition (in metric_space) Cauchy :: "(nat \<Rightarrow> 'a) \<Rightarrow> bool" where
     6.8 -  "Cauchy X = (\<forall>e>0. \<exists>M. \<forall>m \<ge> M. \<forall>n \<ge> M. dist (X m) (X n) < e)"
     6.9 -
    6.10 -
    6.11  subsection {* Bounded Sequences *}
    6.12  
    6.13  lemma BseqI': assumes K: "\<And>n. norm (X n) \<le> K" shows "Bseq X"
    6.14 @@ -80,25 +76,11 @@
    6.15  lemma [trans]: "X=Y ==> Y ----> z ==> X ----> z"
    6.16    by simp
    6.17  
    6.18 -lemma LIMSEQ_def: "X ----> L = (\<forall>r>0. \<exists>no. \<forall>n\<ge>no. dist (X n) L < r)"
    6.19 -unfolding tendsto_iff eventually_sequentially ..
    6.20 -
    6.21  lemma LIMSEQ_iff:
    6.22    fixes L :: "'a::real_normed_vector"
    6.23    shows "(X ----> L) = (\<forall>r>0. \<exists>no. \<forall>n \<ge> no. norm (X n - L) < r)"
    6.24  unfolding LIMSEQ_def dist_norm ..
    6.25  
    6.26 -lemma LIMSEQ_iff_nz: "X ----> L = (\<forall>r>0. \<exists>no>0. \<forall>n\<ge>no. dist (X n) L < r)"
    6.27 -  unfolding LIMSEQ_def by (metis Suc_leD zero_less_Suc)
    6.28 -
    6.29 -lemma metric_LIMSEQ_I:
    6.30 -  "(\<And>r. 0 < r \<Longrightarrow> \<exists>no. \<forall>n\<ge>no. dist (X n) L < r) \<Longrightarrow> X ----> L"
    6.31 -by (simp add: LIMSEQ_def)
    6.32 -
    6.33 -lemma metric_LIMSEQ_D:
    6.34 -  "\<lbrakk>X ----> L; 0 < r\<rbrakk> \<Longrightarrow> \<exists>no. \<forall>n\<ge>no. dist (X n) L < r"
    6.35 -by (simp add: LIMSEQ_def)
    6.36 -
    6.37  lemma LIMSEQ_I:
    6.38    fixes L :: "'a::real_normed_vector"
    6.39    shows "(\<And>r. 0 < r \<Longrightarrow> \<exists>no. \<forall>n\<ge>no. norm (X n - L) < r) \<Longrightarrow> X ----> L"
    6.40 @@ -344,31 +326,11 @@
    6.41    by (metis monoseq_iff incseq_def decseq_eq_incseq convergent_minus_iff Bseq_minus_iff
    6.42              Bseq_mono_convergent)
    6.43  
    6.44 -subsection {* Cauchy Sequences *}
    6.45 -
    6.46 -lemma metric_CauchyI:
    6.47 -  "(\<And>e. 0 < e \<Longrightarrow> \<exists>M. \<forall>m\<ge>M. \<forall>n\<ge>M. dist (X m) (X n) < e) \<Longrightarrow> Cauchy X"
    6.48 -  by (simp add: Cauchy_def)
    6.49 -
    6.50 -lemma metric_CauchyD:
    6.51 -  "Cauchy X \<Longrightarrow> 0 < e \<Longrightarrow> \<exists>M. \<forall>m\<ge>M. \<forall>n\<ge>M. dist (X m) (X n) < e"
    6.52 -  by (simp add: Cauchy_def)
    6.53 -
    6.54  lemma Cauchy_iff:
    6.55    fixes X :: "nat \<Rightarrow> 'a::real_normed_vector"
    6.56    shows "Cauchy X \<longleftrightarrow> (\<forall>e>0. \<exists>M. \<forall>m\<ge>M. \<forall>n\<ge>M. norm (X m - X n) < e)"
    6.57    unfolding Cauchy_def dist_norm ..
    6.58  
    6.59 -lemma Cauchy_iff2:
    6.60 -  "Cauchy X = (\<forall>j. (\<exists>M. \<forall>m \<ge> M. \<forall>n \<ge> M. \<bar>X m - X n\<bar> < inverse(real (Suc j))))"
    6.61 -apply (simp add: Cauchy_iff, auto)
    6.62 -apply (drule reals_Archimedean, safe)
    6.63 -apply (drule_tac x = n in spec, auto)
    6.64 -apply (rule_tac x = M in exI, auto)
    6.65 -apply (drule_tac x = m in spec, simp)
    6.66 -apply (drule_tac x = na in spec, auto)
    6.67 -done
    6.68 -
    6.69  lemma CauchyI:
    6.70    fixes X :: "nat \<Rightarrow> 'a::real_normed_vector"
    6.71    shows "(\<And>e. 0 < e \<Longrightarrow> \<exists>M. \<forall>m\<ge>M. \<forall>n\<ge>M. norm (X m - X n) < e) \<Longrightarrow> Cauchy X"
    6.72 @@ -379,14 +341,6 @@
    6.73    shows "\<lbrakk>Cauchy X; 0 < e\<rbrakk> \<Longrightarrow> \<exists>M. \<forall>m\<ge>M. \<forall>n\<ge>M. norm (X m - X n) < e"
    6.74  by (simp add: Cauchy_iff)
    6.75  
    6.76 -lemma Cauchy_subseq_Cauchy:
    6.77 -  "\<lbrakk> Cauchy X; subseq f \<rbrakk> \<Longrightarrow> Cauchy (X o f)"
    6.78 -apply (auto simp add: Cauchy_def)
    6.79 -apply (drule_tac x=e in spec, clarify)
    6.80 -apply (rule_tac x=M in exI, clarify)
    6.81 -apply (blast intro: le_trans [OF _ seq_suble] dest!: spec)
    6.82 -done
    6.83 -
    6.84  subsubsection {* Cauchy Sequences are Bounded *}
    6.85  
    6.86  text{*A Cauchy sequence is bounded -- this is the standard
    6.87 @@ -412,129 +366,9 @@
    6.88  apply (simp add: order_less_imp_le)
    6.89  done
    6.90  
    6.91 -subsubsection {* Cauchy Sequences are Convergent *}
    6.92 -
    6.93 -class complete_space = metric_space +
    6.94 -  assumes Cauchy_convergent: "Cauchy X \<Longrightarrow> convergent X"
    6.95 -
    6.96  class banach = real_normed_vector + complete_space
    6.97  
    6.98 -theorem LIMSEQ_imp_Cauchy:
    6.99 -  assumes X: "X ----> a" shows "Cauchy X"
   6.100 -proof (rule metric_CauchyI)
   6.101 -  fix e::real assume "0 < e"
   6.102 -  hence "0 < e/2" by simp
   6.103 -  with X have "\<exists>N. \<forall>n\<ge>N. dist (X n) a < e/2" by (rule metric_LIMSEQ_D)
   6.104 -  then obtain N where N: "\<forall>n\<ge>N. dist (X n) a < e/2" ..
   6.105 -  show "\<exists>N. \<forall>m\<ge>N. \<forall>n\<ge>N. dist (X m) (X n) < e"
   6.106 -  proof (intro exI allI impI)
   6.107 -    fix m assume "N \<le> m"
   6.108 -    hence m: "dist (X m) a < e/2" using N by fast
   6.109 -    fix n assume "N \<le> n"
   6.110 -    hence n: "dist (X n) a < e/2" using N by fast
   6.111 -    have "dist (X m) (X n) \<le> dist (X m) a + dist (X n) a"
   6.112 -      by (rule dist_triangle2)
   6.113 -    also from m n have "\<dots> < e" by simp
   6.114 -    finally show "dist (X m) (X n) < e" .
   6.115 -  qed
   6.116 -qed
   6.117 -
   6.118 -lemma convergent_Cauchy: "convergent X \<Longrightarrow> Cauchy X"
   6.119 -unfolding convergent_def
   6.120 -by (erule exE, erule LIMSEQ_imp_Cauchy)
   6.121 -
   6.122 -lemma Cauchy_convergent_iff:
   6.123 -  fixes X :: "nat \<Rightarrow> 'a::complete_space"
   6.124 -  shows "Cauchy X = convergent X"
   6.125 -by (fast intro: Cauchy_convergent convergent_Cauchy)
   6.126 -
   6.127 -text {*
   6.128 -Proof that Cauchy sequences converge based on the one from
   6.129 -http://pirate.shu.edu/~wachsmut/ira/numseq/proofs/cauconv.html
   6.130 -*}
   6.131 -
   6.132 -text {*
   6.133 -  If sequence @{term "X"} is Cauchy, then its limit is the lub of
   6.134 -  @{term "{r::real. \<exists>N. \<forall>n\<ge>N. r < X n}"}
   6.135 -*}
   6.136 -
   6.137 -lemma isUb_UNIV_I: "(\<And>y. y \<in> S \<Longrightarrow> y \<le> u) \<Longrightarrow> isUb UNIV S u"
   6.138 -by (simp add: isUbI setleI)
   6.139 -
   6.140 -lemma real_Cauchy_convergent:
   6.141 -  fixes X :: "nat \<Rightarrow> real"
   6.142 -  assumes X: "Cauchy X"
   6.143 -  shows "convergent X"
   6.144 -proof -
   6.145 -  def S \<equiv> "{x::real. \<exists>N. \<forall>n\<ge>N. x < X n}"
   6.146 -  then have mem_S: "\<And>N x. \<forall>n\<ge>N. x < X n \<Longrightarrow> x \<in> S" by auto
   6.147 -
   6.148 -  { fix N x assume N: "\<forall>n\<ge>N. X n < x"
   6.149 -  have "isUb UNIV S x"
   6.150 -  proof (rule isUb_UNIV_I)
   6.151 -  fix y::real assume "y \<in> S"
   6.152 -  hence "\<exists>M. \<forall>n\<ge>M. y < X n"
   6.153 -    by (simp add: S_def)
   6.154 -  then obtain M where "\<forall>n\<ge>M. y < X n" ..
   6.155 -  hence "y < X (max M N)" by simp
   6.156 -  also have "\<dots> < x" using N by simp
   6.157 -  finally show "y \<le> x"
   6.158 -    by (rule order_less_imp_le)
   6.159 -  qed }
   6.160 -  note bound_isUb = this 
   6.161 -
   6.162 -  have "\<exists>u. isLub UNIV S u"
   6.163 -  proof (rule reals_complete)
   6.164 -  obtain N where "\<forall>m\<ge>N. \<forall>n\<ge>N. norm (X m - X n) < 1"
   6.165 -    using CauchyD [OF X zero_less_one] by auto
   6.166 -  hence N: "\<forall>n\<ge>N. norm (X n - X N) < 1" by simp
   6.167 -  show "\<exists>x. x \<in> S"
   6.168 -  proof
   6.169 -    from N have "\<forall>n\<ge>N. X N - 1 < X n"
   6.170 -      by (simp add: abs_diff_less_iff)
   6.171 -    thus "X N - 1 \<in> S" by (rule mem_S)
   6.172 -  qed
   6.173 -  show "\<exists>u. isUb UNIV S u"
   6.174 -  proof
   6.175 -    from N have "\<forall>n\<ge>N. X n < X N + 1"
   6.176 -      by (simp add: abs_diff_less_iff)
   6.177 -    thus "isUb UNIV S (X N + 1)"
   6.178 -      by (rule bound_isUb)
   6.179 -  qed
   6.180 -  qed
   6.181 -  then obtain x where x: "isLub UNIV S x" ..
   6.182 -  have "X ----> x"
   6.183 -  proof (rule LIMSEQ_I)
   6.184 -  fix r::real assume "0 < r"
   6.185 -  hence r: "0 < r/2" by simp
   6.186 -  obtain N where "\<forall>n\<ge>N. \<forall>m\<ge>N. norm (X n - X m) < r/2"
   6.187 -    using CauchyD [OF X r] by auto
   6.188 -  hence "\<forall>n\<ge>N. norm (X n - X N) < r/2" by simp
   6.189 -  hence N: "\<forall>n\<ge>N. X N - r/2 < X n \<and> X n < X N + r/2"
   6.190 -    by (simp only: real_norm_def abs_diff_less_iff)
   6.191 -
   6.192 -  from N have "\<forall>n\<ge>N. X N - r/2 < X n" by fast
   6.193 -  hence "X N - r/2 \<in> S" by (rule mem_S)
   6.194 -  hence 1: "X N - r/2 \<le> x" using x isLub_isUb isUbD by fast
   6.195 -
   6.196 -  from N have "\<forall>n\<ge>N. X n < X N + r/2" by fast
   6.197 -  hence "isUb UNIV S (X N + r/2)" by (rule bound_isUb)
   6.198 -  hence 2: "x \<le> X N + r/2" using x isLub_le_isUb by fast
   6.199 -
   6.200 -  show "\<exists>N. \<forall>n\<ge>N. norm (X n - x) < r"
   6.201 -  proof (intro exI allI impI)
   6.202 -    fix n assume n: "N \<le> n"
   6.203 -    from N n have "X n < X N + r/2" and "X N - r/2 < X n" by simp+
   6.204 -    thus "norm (X n - x) < r" using 1 2
   6.205 -      by (simp add: abs_diff_less_iff)
   6.206 -  qed
   6.207 -  qed
   6.208 -  then show ?thesis unfolding convergent_def by auto
   6.209 -qed
   6.210 -
   6.211 -instance real :: banach
   6.212 -  by intro_classes (rule real_Cauchy_convergent)
   6.213 -
   6.214 +instance real :: banach by default
   6.215  
   6.216  subsection {* Power Sequences *}
   6.217  
   6.218 @@ -593,33 +427,4 @@
   6.219  lemma LIMSEQ_rabs_realpow_zero2: "\<bar>c\<bar> < 1 \<Longrightarrow> (\<lambda>n. c ^ n :: real) ----> 0"
   6.220    by (rule LIMSEQ_power_zero) simp
   6.221  
   6.222 -lemma tendsto_at_topI_sequentially:
   6.223 -  fixes f :: "real \<Rightarrow> real"
   6.224 -  assumes mono: "mono f"
   6.225 -  assumes limseq: "(\<lambda>n. f (real n)) ----> y"
   6.226 -  shows "(f ---> y) at_top"
   6.227 -proof (rule tendstoI)
   6.228 -  fix e :: real assume "0 < e"
   6.229 -  with limseq obtain N :: nat where N: "\<And>n. N \<le> n \<Longrightarrow> \<bar>f (real n) - y\<bar> < e"
   6.230 -    by (auto simp: LIMSEQ_def dist_real_def)
   6.231 -  { fix x :: real
   6.232 -    from ex_le_of_nat[of x] guess n ..
   6.233 -    note monoD[OF mono this]
   6.234 -    also have "f (real_of_nat n) \<le> y"
   6.235 -      by (rule LIMSEQ_le_const[OF limseq])
   6.236 -         (auto intro: exI[of _ n] monoD[OF mono] simp: real_eq_of_nat[symmetric])
   6.237 -    finally have "f x \<le> y" . }
   6.238 -  note le = this
   6.239 -  have "eventually (\<lambda>x. real N \<le> x) at_top"
   6.240 -    by (rule eventually_ge_at_top)
   6.241 -  then show "eventually (\<lambda>x. dist (f x) y < e) at_top"
   6.242 -  proof eventually_elim
   6.243 -    fix x assume N': "real N \<le> x"
   6.244 -    with N[of N] le have "y - f (real N) < e" by auto
   6.245 -    moreover note monoD[OF mono N']
   6.246 -    ultimately show "dist (f x) y < e"
   6.247 -      using le[of x] by (auto simp: dist_real_def field_simps)
   6.248 -  qed
   6.249 -qed
   6.250 -
   6.251  end