# HG changeset patch # User hoelzl # Date 1363945303 -3600 # Node ID adb441e4b9e992cc93b5c6adfbe4afe795fd1952 # Parent cad22a3cc09c7c4cce65dea6cf8e7bf131718122 move metric_space to its own theory diff -r cad22a3cc09c -r adb441e4b9e9 src/HOL/Lim.thy --- a/src/HOL/Lim.thy Fri Mar 22 10:41:42 2013 +0100 +++ b/src/HOL/Lim.thy Fri Mar 22 10:41:43 2013 +0100 @@ -10,22 +10,8 @@ imports SEQ begin -definition - isUCont :: "['a::metric_space \ 'b::metric_space] \ bool" where - "isUCont f = (\r>0. \s>0. \x y. dist x y < s \ dist (f x) (f y) < r)" - subsection {* Limits of Functions *} -lemma metric_LIM_I: - "(\r. 0 < r \ \s>0. \x. x \ a \ dist x a < s \ dist (f x) L < r) - \ f -- a --> L" -by (simp add: LIM_def) - -lemma metric_LIM_D: - "\f -- a --> L; 0 < r\ - \ \s>0. \x. x \ a \ dist x a < s \ dist (f x) L < r" -by (simp add: LIM_def) - lemma LIM_eq: fixes a :: "'a::real_normed_vector" and L :: "'b::real_normed_vector" shows "f -- a --> L = @@ -80,13 +66,6 @@ shows "((\x. f x - l) ---> 0) F = (f ---> l) F" unfolding tendsto_iff dist_norm by simp -lemma metric_LIM_imp_LIM: - assumes f: "f -- a --> l" - assumes le: "\x. x \ a \ dist (g x) m \ dist (f x) l" - shows "g -- a --> m" - by (rule metric_tendsto_imp_tendsto [OF f], - auto simp add: eventually_at_topological le) - lemma LIM_imp_LIM: fixes f :: "'a::topological_space \ 'b::real_normed_vector" fixes g :: "'a::topological_space \ 'c::real_normed_vector" @@ -96,18 +75,6 @@ by (rule metric_LIM_imp_LIM [OF f], simp add: dist_norm le) -lemma metric_LIM_equal2: - assumes 1: "0 < R" - assumes 2: "\x. \x \ a; dist x a < R\ \ f x = g x" - shows "g -- a --> l \ f -- a --> l" -apply (rule topological_tendstoI) -apply (drule (2) topological_tendstoD) -apply (simp add: eventually_at, safe) -apply (rule_tac x="min d R" in exI, safe) -apply (simp add: 1) -apply (simp add: 2) -done - lemma LIM_equal2: fixes f g :: "'a::real_normed_vector \ 'b::topological_space" assumes 1: "0 < R" @@ -115,14 +82,6 @@ shows "g -- a --> l \ f -- a --> l" by (rule metric_LIM_equal2 [OF 1 2], simp_all add: dist_norm) -lemma metric_LIM_compose2: - assumes f: "f -- a --> b" - assumes g: "g -- b --> c" - assumes inj: "\d>0. \x. x \ a \ dist x a < d \ f x \ b" - shows "(\x. g (f x)) -- a --> c" - using g f inj [folded eventually_at] - by (rule tendsto_compose_eventually) - lemma LIM_compose2: fixes a :: "'a::real_normed_vector" assumes f: "f -- a --> b" @@ -199,13 +158,6 @@ shows "\isCont f a; isCont g a; g a \ 0\ \ isCont (\x. f x / g x) a" unfolding isCont_def by (rule tendsto_divide) -lemma metric_isCont_LIM_compose2: - assumes f [unfolded isCont_def]: "isCont f a" - assumes g: "g -- f a --> l" - assumes inj: "\d>0. \x. x \ a \ dist x a < d \ f x \ f a" - shows "(\x. g (f x)) -- a --> l" -by (rule metric_LIM_compose2 [OF f g inj]) - lemma isCont_LIM_compose2: fixes a :: "'a::real_normed_vector" assumes f [unfolded isCont_def]: "isCont f a" @@ -251,18 +203,6 @@ subsection {* Uniform Continuity *} -lemma isUCont_isCont: "isUCont f ==> isCont f x" -by (simp add: isUCont_def isCont_def LIM_def, force) - -lemma isUCont_Cauchy: - "\isUCont f; Cauchy X\ \ Cauchy (\n. f (X n))" -unfolding isUCont_def -apply (rule metric_CauchyI) -apply (drule_tac x=e in spec, safe) -apply (drule_tac e=s in metric_CauchyD, safe) -apply (rule_tac x=M in exI, simp) -done - lemma (in bounded_linear) isUCont: "isUCont f" unfolding isUCont_def dist_norm proof (intro allI impI) diff -r cad22a3cc09c -r adb441e4b9e9 src/HOL/Limits.thy --- a/src/HOL/Limits.thy Fri Mar 22 10:41:42 2013 +0100 +++ b/src/HOL/Limits.thy Fri Mar 22 10:41:43 2013 +0100 @@ -11,31 +11,6 @@ definition at_infinity :: "'a::real_normed_vector filter" where "at_infinity = Abs_filter (\P. \r. \x. r \ norm x \ P x)" - -lemma eventually_nhds_metric: - "eventually P (nhds a) \ (\d>0. \x. dist x a < d \ P x)" -unfolding eventually_nhds open_dist -apply safe -apply fast -apply (rule_tac x="{x. dist x a < d}" in exI, simp) -apply clarsimp -apply (rule_tac x="d - dist x a" in exI, clarsimp) -apply (simp only: less_diff_eq) -apply (erule le_less_trans [OF dist_triangle]) -done - -lemma eventually_at: - fixes a :: "'a::metric_space" - shows "eventually P (at a) \ (\d>0. \x. x \ a \ dist x a < d \ P x)" -unfolding at_def eventually_within eventually_nhds_metric by auto -lemma eventually_within_less: (* COPY FROM Topo/eventually_within *) - "eventually P (at a within S) \ (\d>0. \x\S. 0 < dist x a \ dist x a < d \ P x)" - unfolding eventually_within eventually_at dist_nz by auto - -lemma eventually_within_le: (* COPY FROM Topo/eventually_within_le *) - "eventually P (at a within S) \ (\d>0. \x\S. 0 < dist x a \ dist x a <= d \ P x)" - unfolding eventually_within_less by auto (metis dense order_le_less_trans) - lemma eventually_at_infinity: "eventually P at_infinity \ (\b. \x. b \ norm x \ P x)" unfolding at_infinity_def @@ -246,39 +221,8 @@ lemma tendsto_Zfun_iff: "(f ---> a) F = Zfun (\x. f x - a) F" by (simp only: tendsto_iff Zfun_def dist_norm) - -lemma metric_tendsto_imp_tendsto: - assumes f: "(f ---> a) F" - assumes le: "eventually (\x. dist (g x) b \ dist (f x) a) F" - shows "(g ---> b) F" -proof (rule tendstoI) - fix e :: real assume "0 < e" - with f have "eventually (\x. dist (f x) a < e) F" by (rule tendstoD) - with le show "eventually (\x. dist (g x) b < e) F" - using le_less_trans by (rule eventually_elim2) -qed subsubsection {* Distance and norms *} -lemma tendsto_dist [tendsto_intros]: - assumes f: "(f ---> l) F" and g: "(g ---> m) F" - shows "((\x. dist (f x) (g x)) ---> dist l m) F" -proof (rule tendstoI) - fix e :: real assume "0 < e" - hence e2: "0 < e/2" by simp - from tendstoD [OF f e2] tendstoD [OF g e2] - show "eventually (\x. dist (dist (f x) (g x)) (dist l m) < e) F" - proof (eventually_elim) - case (elim x) - then show "dist (dist (f x) (g x)) (dist l m) < e" - unfolding dist_real_def - using dist_triangle2 [of "f x" "g x" "l"] - using dist_triangle2 [of "g x" "l" "m"] - using dist_triangle3 [of "l" "m" "f x"] - using dist_triangle [of "f x" "m" "g x"] - by arith - qed -qed - lemma norm_conv_dist: "norm x = dist x 0" unfolding dist_norm by simp @@ -544,50 +488,6 @@ shows "\(f ---> l) F; l \ 0\ \ ((\x. sgn (f x)) ---> sgn l) F" unfolding sgn_div_norm by (simp add: tendsto_intros) -lemma filterlim_at_bot_at_right: - fixes f :: "real \ 'b::linorder" - assumes mono: "\x y. Q x \ Q y \ x \ y \ f x \ f y" - assumes bij: "\x. P x \ f (g x) = x" "\x. P x \ Q (g x)" - assumes Q: "eventually Q (at_right a)" and bound: "\b. Q b \ a < b" - assumes P: "eventually P at_bot" - shows "filterlim f at_bot (at_right a)" -proof - - from P obtain x where x: "\y. y \ x \ P y" - unfolding eventually_at_bot_linorder by auto - show ?thesis - proof (intro filterlim_at_bot_le[THEN iffD2] allI impI) - fix z assume "z \ x" - with x have "P z" by auto - have "eventually (\x. x \ g z) (at_right a)" - using bound[OF bij(2)[OF `P z`]] - by (auto simp add: eventually_within_less dist_real_def intro!: exI[of _ "g z - a"]) - with Q show "eventually (\x. f x \ z) (at_right a)" - by eventually_elim (metis bij `P z` mono) - qed -qed - -lemma filterlim_at_top_at_left: - fixes f :: "real \ 'b::linorder" - assumes mono: "\x y. Q x \ Q y \ x \ y \ f x \ f y" - assumes bij: "\x. P x \ f (g x) = x" "\x. P x \ Q (g x)" - assumes Q: "eventually Q (at_left a)" and bound: "\b. Q b \ b < a" - assumes P: "eventually P at_top" - shows "filterlim f at_top (at_left a)" -proof - - from P obtain x where x: "\y. x \ y \ P y" - unfolding eventually_at_top_linorder by auto - show ?thesis - proof (intro filterlim_at_top_ge[THEN iffD2] allI impI) - fix z assume "x \ z" - with x have "P z" by auto - have "eventually (\x. g z \ x) (at_left a)" - using bound[OF bij(2)[OF `P z`]] - by (auto simp add: eventually_within_less dist_real_def intro!: exI[of _ "a - g z"]) - with Q show "eventually (\x. z \ f x) (at_left a)" - by eventually_elim (metis bij `P z` mono) - qed -qed - lemma filterlim_at_infinity: fixes f :: "_ \ 'a\real_normed_vector" assumes "0 \ c" @@ -607,13 +507,6 @@ qed qed force -lemma filterlim_real_sequentially: "LIM x sequentially. real x :> at_top" - unfolding filterlim_at_top - apply (intro allI) - apply (rule_tac c="natceiling (Z + 1)" in eventually_sequentiallyI) - apply (auto simp: natceiling_le_eq) - done - subsection {* Relate @{const at}, @{const at_left} and @{const at_right} *} text {* diff -r cad22a3cc09c -r adb441e4b9e9 src/HOL/Metric_Spaces.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Metric_Spaces.thy Fri Mar 22 10:41:43 2013 +0100 @@ -0,0 +1,573 @@ +(* Title: HOL/Metric_Spaces.thy + Author: Brian Huffman + Author: Johannes Hölzl +*) + +header {* Metric Spaces *} + +theory Metric_Spaces +imports RComplete Topological_Spaces +begin + + +subsection {* Metric spaces *} + +class dist = + fixes dist :: "'a \ 'a \ real" + +class open_dist = "open" + dist + + assumes open_dist: "open S \ (\x\S. \e>0. \y. dist y x < e \ y \ S)" + +class metric_space = open_dist + + assumes dist_eq_0_iff [simp]: "dist x y = 0 \ x = y" + assumes dist_triangle2: "dist x y \ dist x z + dist y z" +begin + +lemma dist_self [simp]: "dist x x = 0" +by simp + +lemma zero_le_dist [simp]: "0 \ dist x y" +using dist_triangle2 [of x x y] by simp + +lemma zero_less_dist_iff: "0 < dist x y \ x \ y" +by (simp add: less_le) + +lemma dist_not_less_zero [simp]: "\ dist x y < 0" +by (simp add: not_less) + +lemma dist_le_zero_iff [simp]: "dist x y \ 0 \ x = y" +by (simp add: le_less) + +lemma dist_commute: "dist x y = dist y x" +proof (rule order_antisym) + show "dist x y \ dist y x" + using dist_triangle2 [of x y x] by simp + show "dist y x \ dist x y" + using dist_triangle2 [of y x y] by simp +qed + +lemma dist_triangle: "dist x z \ dist x y + dist y z" +using dist_triangle2 [of x z y] by (simp add: dist_commute) + +lemma dist_triangle3: "dist x y \ dist a x + dist a y" +using dist_triangle2 [of x y a] by (simp add: dist_commute) + +lemma dist_triangle_alt: + shows "dist y z <= dist x y + dist x z" +by (rule dist_triangle3) + +lemma dist_pos_lt: + shows "x \ y ==> 0 < dist x y" +by (simp add: zero_less_dist_iff) + +lemma dist_nz: + shows "x \ y \ 0 < dist x y" +by (simp add: zero_less_dist_iff) + +lemma dist_triangle_le: + shows "dist x z + dist y z <= e \ dist x y <= e" +by (rule order_trans [OF dist_triangle2]) + +lemma dist_triangle_lt: + shows "dist x z + dist y z < e ==> dist x y < e" +by (rule le_less_trans [OF dist_triangle2]) + +lemma dist_triangle_half_l: + shows "dist x1 y < e / 2 \ dist x2 y < e / 2 \ dist x1 x2 < e" +by (rule dist_triangle_lt [where z=y], simp) + +lemma dist_triangle_half_r: + shows "dist y x1 < e / 2 \ dist y x2 < e / 2 \ dist x1 x2 < e" +by (rule dist_triangle_half_l, simp_all add: dist_commute) + +subclass topological_space +proof + have "\e::real. 0 < e" + by (fast intro: zero_less_one) + then show "open UNIV" + unfolding open_dist by simp +next + fix S T assume "open S" "open T" + then show "open (S \ T)" + unfolding open_dist + apply clarify + apply (drule (1) bspec)+ + apply (clarify, rename_tac r s) + apply (rule_tac x="min r s" in exI, simp) + done +next + fix K assume "\S\K. open S" thus "open (\K)" + unfolding open_dist by fast +qed + +lemma (in metric_space) open_ball: "open {y. dist x y < d}" +proof (unfold open_dist, intro ballI) + fix y assume *: "y \ {y. dist x y < d}" + then show "\e>0. \z. dist z y < e \ z \ {y. dist x y < d}" + by (auto intro!: exI[of _ "d - dist x y"] simp: field_simps dist_triangle_lt) +qed + +end + +instance metric_space \ t2_space +proof + fix x y :: "'a::metric_space" + assume xy: "x \ y" + let ?U = "{y'. dist x y' < dist x y / 2}" + let ?V = "{x'. dist y x' < dist x y / 2}" + have th0: "\d x y z. (d x z :: real) \ d x y + d y z \ d y z = d z y + \ \(d x y * 2 < d x z \ d z y * 2 < d x z)" by arith + have "open ?U \ open ?V \ x \ ?U \ y \ ?V \ ?U \ ?V = {}" + using dist_pos_lt[OF xy] th0[of dist, OF dist_triangle dist_commute] + using open_ball[of _ "dist x y / 2"] by auto + then show "\U V. open U \ open V \ x \ U \ y \ V \ U \ V = {}" + by blast +qed + +lemma eventually_nhds_metric: + fixes a :: "'a :: metric_space" + shows "eventually P (nhds a) \ (\d>0. \x. dist x a < d \ P x)" +unfolding eventually_nhds open_dist +apply safe +apply fast +apply (rule_tac x="{x. dist x a < d}" in exI, simp) +apply clarsimp +apply (rule_tac x="d - dist x a" in exI, clarsimp) +apply (simp only: less_diff_eq) +apply (erule le_less_trans [OF dist_triangle]) +done + +lemma eventually_at: + fixes a :: "'a::metric_space" + shows "eventually P (at a) \ (\d>0. \x. x \ a \ dist x a < d \ P x)" +unfolding at_def eventually_within eventually_nhds_metric by auto + +lemma eventually_within_less: (* COPY FROM Topo/eventually_within *) + fixes a :: "'a :: metric_space" + shows "eventually P (at a within S) \ (\d>0. \x\S. 0 < dist x a \ dist x a < d \ P x)" + unfolding eventually_within eventually_at dist_nz by auto + +lemma eventually_within_le: (* COPY FROM Topo/eventually_within_le *) + fixes a :: "'a :: metric_space" + shows "eventually P (at a within S) \ (\d>0. \x\S. 0 < dist x a \ dist x a <= d \ P x)" + unfolding eventually_within_less by auto (metis dense order_le_less_trans) + +lemma tendstoI: + fixes l :: "'a :: metric_space" + assumes "\e. 0 < e \ eventually (\x. dist (f x) l < e) F" + shows "(f ---> l) F" + apply (rule topological_tendstoI) + apply (simp add: open_dist) + apply (drule (1) bspec, clarify) + apply (drule assms) + apply (erule eventually_elim1, simp) + done + +lemma tendstoD: + fixes l :: "'a :: metric_space" + shows "(f ---> l) F \ 0 < e \ eventually (\x. dist (f x) l < e) F" + apply (drule_tac S="{x. dist x l < e}" in topological_tendstoD) + apply (clarsimp simp add: open_dist) + apply (rule_tac x="e - dist x l" in exI, clarsimp) + apply (simp only: less_diff_eq) + apply (erule le_less_trans [OF dist_triangle]) + apply simp + apply simp + done + +lemma tendsto_iff: + fixes l :: "'a :: metric_space" + shows "(f ---> l) F \ (\e>0. eventually (\x. dist (f x) l < e) F)" + using tendstoI tendstoD by fast + +lemma metric_tendsto_imp_tendsto: + fixes a :: "'a :: metric_space" and b :: "'b :: metric_space" + assumes f: "(f ---> a) F" + assumes le: "eventually (\x. dist (g x) b \ dist (f x) a) F" + shows "(g ---> b) F" +proof (rule tendstoI) + fix e :: real assume "0 < e" + with f have "eventually (\x. dist (f x) a < e) F" by (rule tendstoD) + with le show "eventually (\x. dist (g x) b < e) F" + using le_less_trans by (rule eventually_elim2) +qed + +lemma filterlim_real_sequentially: "LIM x sequentially. real x :> at_top" + unfolding filterlim_at_top + apply (intro allI) + apply (rule_tac c="natceiling (Z + 1)" in eventually_sequentiallyI) + apply (auto simp: natceiling_le_eq) + done + +subsubsection {* Limits of Sequences *} + +lemma LIMSEQ_def: "X ----> (L::'a::metric_space) \ (\r>0. \no. \n\no. dist (X n) L < r)" + unfolding tendsto_iff eventually_sequentially .. + +lemma LIMSEQ_iff_nz: "X ----> (L::'a::metric_space) = (\r>0. \no>0. \n\no. dist (X n) L < r)" + unfolding LIMSEQ_def by (metis Suc_leD zero_less_Suc) + +lemma metric_LIMSEQ_I: + "(\r. 0 < r \ \no. \n\no. dist (X n) L < r) \ X ----> (L::'a::metric_space)" +by (simp add: LIMSEQ_def) + +lemma metric_LIMSEQ_D: + "\X ----> (L::'a::metric_space); 0 < r\ \ \no. \n\no. dist (X n) L < r" +by (simp add: LIMSEQ_def) + + +subsubsection {* Limits of Functions *} + +lemma LIM_def: "f -- (a::'a::metric_space) --> (L::'b::metric_space) = + (\r > 0. \s > 0. \x. x \ a & dist x a < s + --> dist (f x) L < r)" +unfolding tendsto_iff eventually_at .. + +lemma metric_LIM_I: + "(\r. 0 < r \ \s>0. \x. x \ a \ dist x a < s \ dist (f x) L < r) + \ f -- (a::'a::metric_space) --> (L::'b::metric_space)" +by (simp add: LIM_def) + +lemma metric_LIM_D: + "\f -- (a::'a::metric_space) --> (L::'b::metric_space); 0 < r\ + \ \s>0. \x. x \ a \ dist x a < s \ dist (f x) L < r" +by (simp add: LIM_def) + +lemma metric_LIM_imp_LIM: + assumes f: "f -- a --> (l::'a::metric_space)" + assumes le: "\x. x \ a \ dist (g x) m \ dist (f x) l" + shows "g -- a --> (m::'b::metric_space)" + by (rule metric_tendsto_imp_tendsto [OF f]) (auto simp add: eventually_at_topological le) + +lemma metric_LIM_equal2: + assumes 1: "0 < R" + assumes 2: "\x. \x \ a; dist x a < R\ \ f x = g x" + shows "g -- a --> l \ f -- (a::'a::metric_space) --> l" +apply (rule topological_tendstoI) +apply (drule (2) topological_tendstoD) +apply (simp add: eventually_at, safe) +apply (rule_tac x="min d R" in exI, safe) +apply (simp add: 1) +apply (simp add: 2) +done + +lemma metric_LIM_compose2: + assumes f: "f -- (a::'a::metric_space) --> b" + assumes g: "g -- b --> c" + assumes inj: "\d>0. \x. x \ a \ dist x a < d \ f x \ b" + shows "(\x. g (f x)) -- a --> c" + using g f inj [folded eventually_at] + by (rule tendsto_compose_eventually) + +lemma metric_isCont_LIM_compose2: + fixes f :: "'a :: metric_space \ _" + assumes f [unfolded isCont_def]: "isCont f a" + assumes g: "g -- f a --> l" + assumes inj: "\d>0. \x. x \ a \ dist x a < d \ f x \ f a" + shows "(\x. g (f x)) -- a --> l" +by (rule metric_LIM_compose2 [OF f g inj]) + +subsection {* Complete metric spaces *} + +subsection {* Cauchy sequences *} + +definition (in metric_space) Cauchy :: "(nat \ 'a) \ bool" where + "Cauchy X = (\e>0. \M. \m \ M. \n \ M. dist (X m) (X n) < e)" + +subsection {* Cauchy Sequences *} + +lemma metric_CauchyI: + "(\e. 0 < e \ \M. \m\M. \n\M. dist (X m) (X n) < e) \ Cauchy X" + by (simp add: Cauchy_def) + +lemma metric_CauchyD: + "Cauchy X \ 0 < e \ \M. \m\M. \n\M. dist (X m) (X n) < e" + by (simp add: Cauchy_def) + +lemma metric_Cauchy_iff2: + "Cauchy X = (\j. (\M. \m \ M. \n \ M. dist (X m) (X n) < inverse(real (Suc j))))" +apply (simp add: Cauchy_def, auto) +apply (drule reals_Archimedean, safe) +apply (drule_tac x = n in spec, auto) +apply (rule_tac x = M in exI, auto) +apply (drule_tac x = m in spec, simp) +apply (drule_tac x = na in spec, auto) +done + +lemma Cauchy_subseq_Cauchy: + "\ Cauchy X; subseq f \ \ Cauchy (X o f)" +apply (auto simp add: Cauchy_def) +apply (drule_tac x=e in spec, clarify) +apply (rule_tac x=M in exI, clarify) +apply (blast intro: le_trans [OF _ seq_suble] dest!: spec) +done + + +subsubsection {* Cauchy Sequences are Convergent *} + +class complete_space = metric_space + + assumes Cauchy_convergent: "Cauchy X \ convergent X" + +theorem LIMSEQ_imp_Cauchy: + assumes X: "X ----> a" shows "Cauchy X" +proof (rule metric_CauchyI) + fix e::real assume "0 < e" + hence "0 < e/2" by simp + with X have "\N. \n\N. dist (X n) a < e/2" by (rule metric_LIMSEQ_D) + then obtain N where N: "\n\N. dist (X n) a < e/2" .. + show "\N. \m\N. \n\N. dist (X m) (X n) < e" + proof (intro exI allI impI) + fix m assume "N \ m" + hence m: "dist (X m) a < e/2" using N by fast + fix n assume "N \ n" + hence n: "dist (X n) a < e/2" using N by fast + have "dist (X m) (X n) \ dist (X m) a + dist (X n) a" + by (rule dist_triangle2) + also from m n have "\ < e" by simp + finally show "dist (X m) (X n) < e" . + qed +qed + +lemma convergent_Cauchy: "convergent X \ Cauchy X" +unfolding convergent_def +by (erule exE, erule LIMSEQ_imp_Cauchy) + +lemma Cauchy_convergent_iff: + fixes X :: "nat \ 'a::complete_space" + shows "Cauchy X = convergent X" +by (fast intro: Cauchy_convergent convergent_Cauchy) + +subsection {* Uniform Continuity *} + +definition + isUCont :: "['a::metric_space \ 'b::metric_space] \ bool" where + "isUCont f = (\r>0. \s>0. \x y. dist x y < s \ dist (f x) (f y) < r)" + +lemma isUCont_isCont: "isUCont f ==> isCont f x" +by (simp add: isUCont_def isCont_def LIM_def, force) + +lemma isUCont_Cauchy: + "\isUCont f; Cauchy X\ \ Cauchy (\n. f (X n))" +unfolding isUCont_def +apply (rule metric_CauchyI) +apply (drule_tac x=e in spec, safe) +apply (drule_tac e=s in metric_CauchyD, safe) +apply (rule_tac x=M in exI, simp) +done + +subsection {* The set of real numbers is a complete metric space *} + +instantiation real :: metric_space +begin + +definition dist_real_def: + "dist x y = \x - y\" + +definition open_real_def: + "open (S :: real set) \ (\x\S. \e>0. \y. dist y x < e \ y \ S)" + +instance + by default (auto simp: open_real_def dist_real_def) +end + +instance real :: linorder_topology +proof + show "(open :: real set \ bool) = generate_topology (range lessThan \ range greaterThan)" + proof (rule ext, safe) + fix S :: "real set" assume "open S" + then guess f unfolding open_real_def bchoice_iff .. + then have *: "S = (\x\S. {x - f x <..} \ {..< x + f x})" + by (fastforce simp: dist_real_def) + show "generate_topology (range lessThan \ range greaterThan) S" + apply (subst *) + apply (intro generate_topology_Union generate_topology.Int) + apply (auto intro: generate_topology.Basis) + done + next + fix S :: "real set" assume "generate_topology (range lessThan \ range greaterThan) S" + moreover have "\a::real. open {.. (\y. \y - x\ < a - x \ y \ {..e>0. \y. \y - x\ < e \ y \ {..