--- a/NEWS Fri Jan 08 16:37:56 2016 +0100
+++ b/NEWS Fri Jan 08 17:40:59 2016 +0100
@@ -606,6 +606,14 @@
terms for sup and inf. For example, "sup x (sup y (- x))" simplifies to
"top". INCOMPATIBILITY.
+* Class uniform_space introduces uniform spaces btw topological spaces
+and metric spaces. Minor INCOMPATIBILITY: open_<type>_def needs to be
+introduced in the form of an uniformity. Some constants are more
+general now, it may be necessary to add type class constraints.
+
+ open_real_def \<leadsto> open_dist
+ open_complex_def \<leadsto> open_dist
+
* Library/Monad_Syntax: notation uses symbols \<bind> and \<then>. INCOMPATIBILITY.
* Library/Multiset:
--- a/src/HOL/Complex.thy Fri Jan 08 16:37:56 2016 +0100
+++ b/src/HOL/Complex.thy Fri Jan 08 17:40:59 2016 +0100
@@ -264,8 +264,11 @@
definition dist_complex_def:
"dist x y = cmod (x - y)"
-definition open_complex_def:
- "open (S :: complex set) \<longleftrightarrow> (\<forall>x\<in>S. \<exists>e>0. \<forall>y. dist y x < e \<longrightarrow> y \<in> S)"
+definition uniformity_complex_def [code del]:
+ "(uniformity :: (complex \<times> complex) filter) = (INF e:{0 <..}. principal {(x, y). dist x y < e})"
+
+definition open_complex_def [code del]:
+ "open (U :: complex set) \<longleftrightarrow> (\<forall>x\<in>U. eventually (\<lambda>(x', y). x' = x \<longrightarrow> y \<in> U) uniformity)"
instance proof
fix r :: real and x y :: complex and S :: "complex set"
@@ -277,7 +280,7 @@
by (simp add: norm_complex_def complex_eq_iff power_mult_distrib distrib_left [symmetric] real_sqrt_mult)
show "norm (x * y) = norm x * norm y"
by (simp add: norm_complex_def complex_eq_iff real_sqrt_mult [symmetric] power2_eq_square algebra_simps)
-qed (rule complex_sgn_def dist_complex_def open_complex_def)+
+qed (rule complex_sgn_def dist_complex_def open_complex_def uniformity_complex_def)+
end
--- a/src/HOL/Filter.thy Fri Jan 08 16:37:56 2016 +0100
+++ b/src/HOL/Filter.thy Fri Jan 08 17:40:59 2016 +0100
@@ -529,6 +529,8 @@
unfolding le_filter_def eventually_filtermap
by (subst (1 2) eventually_INF) auto
qed
+
+
subsubsection \<open>Standard filters\<close>
definition principal :: "'a set \<Rightarrow> 'a filter" where
@@ -743,6 +745,52 @@
by (blast intro: finite_subset)
qed
+subsubsection \<open>Product of filters\<close>
+
+lemma filtermap_sequentually_ne_bot: "filtermap f sequentially \<noteq> bot"
+ by (auto simp add: filter_eq_iff eventually_filtermap eventually_sequentially)
+
+definition prod_filter :: "'a filter \<Rightarrow> 'b filter \<Rightarrow> ('a \<times> 'b) filter" (infixr "\<times>\<^sub>F" 80) where
+ "prod_filter F G =
+ (INF (P, Q):{(P, Q). eventually P F \<and> eventually Q G}. principal {(x, y). P x \<and> Q y})"
+
+lemma eventually_prod_filter: "eventually P (F \<times>\<^sub>F G) \<longleftrightarrow>
+ (\<exists>Pf Pg. eventually Pf F \<and> eventually Pg G \<and> (\<forall>x y. Pf x \<longrightarrow> Pg y \<longrightarrow> P (x, y)))"
+ unfolding prod_filter_def
+proof (subst eventually_INF_base, goal_cases)
+ case 2
+ moreover have "eventually Pf F \<Longrightarrow> eventually Qf F \<Longrightarrow> eventually Pg G \<Longrightarrow> eventually Qg G \<Longrightarrow>
+ \<exists>P Q. eventually P F \<and> eventually Q G \<and>
+ Collect P \<times> Collect Q \<subseteq> Collect Pf \<times> Collect Pg \<inter> Collect Qf \<times> Collect Qg" for Pf Pg Qf Qg
+ by (intro conjI exI[of _ "inf Pf Qf"] exI[of _ "inf Pg Qg"])
+ (auto simp: inf_fun_def eventually_conj)
+ ultimately show ?case
+ by auto
+qed (auto simp: eventually_principal intro: eventually_True)
+
+lemma prod_filter_mono: "F \<le> F' \<Longrightarrow> G \<le> G' \<Longrightarrow> F \<times>\<^sub>F G \<le> F' \<times>\<^sub>F G'"
+ by (auto simp: le_filter_def eventually_prod_filter)
+
+lemma eventually_prod_same: "eventually P (F \<times>\<^sub>F F) \<longleftrightarrow>
+ (\<exists>Q. eventually Q F \<and> (\<forall>x y. Q x \<longrightarrow> Q y \<longrightarrow> P (x, y)))"
+ unfolding eventually_prod_filter
+ apply safe
+ apply (rule_tac x="inf Pf Pg" in exI)
+ apply (auto simp: inf_fun_def intro!: eventually_conj)
+ done
+
+lemma eventually_prod_sequentially:
+ "eventually P (sequentially \<times>\<^sub>F sequentially) \<longleftrightarrow> (\<exists>N. \<forall>m \<ge> N. \<forall>n \<ge> N. P (n, m))"
+ unfolding eventually_prod_same eventually_sequentially by auto
+
+lemma principal_prod_principal: "principal A \<times>\<^sub>F principal B = principal (A \<times> B)"
+ apply (simp add: filter_eq_iff eventually_prod_filter eventually_principal)
+ apply safe
+ apply blast
+ apply (intro conjI exI[of _ "\<lambda>x. x \<in> A"] exI[of _ "\<lambda>x. x \<in> B"])
+ apply auto
+ done
+
subsection \<open>Limits\<close>
definition filterlim :: "('a \<Rightarrow> 'b) \<Rightarrow> 'b filter \<Rightarrow> 'a filter \<Rightarrow> bool" where
--- a/src/HOL/Library/Extended_Real.thy Fri Jan 08 16:37:56 2016 +0100
+++ b/src/HOL/Library/Extended_Real.thy Fri Jan 08 17:40:59 2016 +0100
@@ -2769,7 +2769,7 @@
then have "open (ereal -` S)"
unfolding open_ereal_def by auto
with \<open>x \<in> S\<close> obtain r where "0 < r" and dist: "\<And>y. dist y rx < r \<Longrightarrow> ereal y \<in> S"
- unfolding open_real_def rx by auto
+ unfolding open_dist rx by auto
then obtain n where
upper: "\<And>N. n \<le> N \<Longrightarrow> u N < x + ereal r" and
lower: "\<And>N. n \<le> N \<Longrightarrow> x < u N + ereal r"
--- a/src/HOL/Library/Formal_Power_Series.thy Fri Jan 08 16:37:56 2016 +0100
+++ b/src/HOL/Library/Formal_Power_Series.thy Fri Jan 08 17:40:59 2016 +0100
@@ -815,13 +815,14 @@
instantiation fps :: (comm_ring_1) metric_space
begin
-definition open_fps_def: "open (S :: 'a fps set) = (\<forall>a \<in> S. \<exists>r. r >0 \<and> ball a r \<subseteq> S)"
-
+definition uniformity_fps_def [code del]:
+ "(uniformity :: ('a fps \<times> 'a fps) filter) = (INF e:{0 <..}. principal {(x, y). dist x y < e})"
+
+definition open_fps_def' [code del]:
+ "open (U :: 'a fps set) \<longleftrightarrow> (\<forall>x\<in>U. eventually (\<lambda>(x', y). x' = x \<longrightarrow> y \<in> U) uniformity)"
instance
proof
- show "open S = (\<forall>x\<in>S. \<exists>e>0. \<forall>y. dist y x < e \<longrightarrow> y \<in> S)" for S :: "'a fps set"
- by (auto simp add: open_fps_def ball_def subset_eq)
show th: "dist a b = 0 \<longleftrightarrow> a = b" for a b :: "'a fps"
by (simp add: dist_fps_def split: split_if_asm)
then have th'[simp]: "dist a a = 0" for a :: "'a fps" by simp
@@ -853,10 +854,12 @@
qed
thus ?thesis by (auto simp add: not_le[symmetric])
qed
-qed
+qed (rule open_fps_def' uniformity_fps_def)+
end
+lemma open_fps_def: "open (S :: 'a::comm_ring_1 fps set) = (\<forall>a \<in> S. \<exists>r. r >0 \<and> ball a r \<subseteq> S)"
+ unfolding open_dist ball_def subset_eq by simp
text \<open>The infinite sums and justification of the notation in textbooks.\<close>
--- a/src/HOL/Library/Inner_Product.thy Fri Jan 08 16:37:56 2016 +0100
+++ b/src/HOL/Library/Inner_Product.thy Fri Jan 08 17:40:59 2016 +0100
@@ -11,7 +11,7 @@
subsection \<open>Real inner product spaces\<close>
text \<open>
- Temporarily relax type constraints for @{term "open"},
+ Temporarily relax type constraints for @{term "open"}, @{term "uniformity"},
@{term dist}, and @{term norm}.
\<close>
@@ -22,9 +22,12 @@
(@{const_name dist}, SOME @{typ "'a::dist \<Rightarrow> 'a \<Rightarrow> real"})\<close>
setup \<open>Sign.add_const_constraint
+ (@{const_name uniformity}, SOME @{typ "('a::uniformity \<times> 'a) filter"})\<close>
+
+setup \<open>Sign.add_const_constraint
(@{const_name norm}, SOME @{typ "'a::norm \<Rightarrow> real"})\<close>
-class real_inner = real_vector + sgn_div_norm + dist_norm + open_dist +
+class real_inner = real_vector + sgn_div_norm + dist_norm + uniformity_dist + open_uniformity +
fixes inner :: "'a \<Rightarrow> 'a \<Rightarrow> real"
assumes inner_commute: "inner x y = inner y x"
and inner_add_left: "inner (x + y) z = inner x z + inner y z"
@@ -166,7 +169,7 @@
by (metis inner_commute inner_divide_left)
text \<open>
- Re-enable constraints for @{term "open"},
+ Re-enable constraints for @{term "open"}, @{term "uniformity"},
@{term dist}, and @{term norm}.
\<close>
@@ -174,6 +177,9 @@
(@{const_name "open"}, SOME @{typ "'a::topological_space set \<Rightarrow> bool"})\<close>
setup \<open>Sign.add_const_constraint
+ (@{const_name uniformity}, SOME @{typ "('a::uniform_space \<times> 'a) filter"})\<close>
+
+setup \<open>Sign.add_const_constraint
(@{const_name dist}, SOME @{typ "'a::metric_space \<Rightarrow> 'a \<Rightarrow> real"})\<close>
setup \<open>Sign.add_const_constraint
--- a/src/HOL/Library/Product_Vector.thy Fri Jan 08 16:37:56 2016 +0100
+++ b/src/HOL/Library/Product_Vector.thy Fri Jan 08 17:40:59 2016 +0100
@@ -229,9 +229,6 @@
subsubsection \<open>Separation axioms\<close>
-lemma mem_Times_iff: "x \<in> A \<times> B \<longleftrightarrow> fst x \<in> A \<and> snd x \<in> B"
- by (induct x) simp (* TODO: move elsewhere *)
-
instance prod :: (t0_space, t0_space) t0_space
proof
fix x y :: "'a \<times> 'b" assume "x \<noteq> y"
@@ -264,12 +261,31 @@
subsection \<open>Product is a metric space\<close>
-instantiation prod :: (metric_space, metric_space) metric_space
+(* TODO: Product of uniform spaces and compatibility with metric_spaces! *)
+
+instantiation prod :: (metric_space, metric_space) dist
begin
definition dist_prod_def[code del]:
"dist x y = sqrt ((dist (fst x) (fst y))\<^sup>2 + (dist (snd x) (snd y))\<^sup>2)"
+instance ..
+end
+
+instantiation prod :: (metric_space, metric_space) uniformity_dist
+begin
+
+definition [code del]:
+ "(uniformity :: (('a \<times> 'b) \<times> ('a \<times> 'b)) filter) =
+ (INF e:{0 <..}. principal {(x, y). dist x y < e})"
+
+instance
+ by standard (rule uniformity_prod_def)
+end
+
+instantiation prod :: (metric_space, metric_space) metric_space
+begin
+
lemma dist_Pair_Pair: "dist (a, b) (c, d) = sqrt ((dist a c)\<^sup>2 + (dist b d)\<^sup>2)"
unfolding dist_prod_def by simp
@@ -292,7 +308,7 @@
real_sqrt_le_mono add_mono power_mono dist_triangle2 zero_le_dist)
next
fix S :: "('a \<times> 'b) set"
- show "open S \<longleftrightarrow> (\<forall>x\<in>S. \<exists>e>0. \<forall>y. dist y x < e \<longrightarrow> y \<in> S)"
+ have *: "open S \<longleftrightarrow> (\<forall>x\<in>S. \<exists>e>0. \<forall>y. dist y x < e \<longrightarrow> y \<in> S)"
proof
assume "open S" show "\<forall>x\<in>S. \<exists>e>0. \<forall>y. dist y x < e \<longrightarrow> y \<in> S"
proof
@@ -351,6 +367,9 @@
ultimately show "\<exists>A B. open A \<and> open B \<and> x \<in> A \<times> B \<and> A \<times> B \<subseteq> S" by fast
qed
qed
+ show "open S = (\<forall>x\<in>S. \<forall>\<^sub>F (x', y) in uniformity. x' = x \<longrightarrow> y \<in> S)"
+ unfolding * eventually_uniformity_metric
+ by (simp del: split_paired_All add: dist_prod_def dist_commute)
qed
end
--- a/src/HOL/Limits.thy Fri Jan 08 16:37:56 2016 +0100
+++ b/src/HOL/Limits.thy Fri Jan 08 17:40:59 2016 +0100
@@ -1624,16 +1624,6 @@
using tendsto_mult [OF tendsto_const LIMSEQ_inverse_real_of_nat_add_minus [of 1]]
by auto
-lemma lim_1_over_n: "((\<lambda>n. 1 / of_nat n) \<longlongrightarrow> (0::'a::real_normed_field)) sequentially"
-proof (subst lim_sequentially, intro allI impI exI)
- fix e :: real assume e: "e > 0"
- fix n :: nat assume n: "n \<ge> nat \<lceil>inverse e + 1\<rceil>"
- have "inverse e < of_nat (nat \<lceil>inverse e + 1\<rceil>)" by linarith
- also note n
- finally show "dist (1 / of_nat n :: 'a) 0 < e" using e
- by (simp add: divide_simps mult.commute norm_conv_dist[symmetric] norm_divide)
-qed
-
lemma lim_inverse_n: "((\<lambda>n. inverse(of_nat n)) \<longlongrightarrow> (0::'a::real_normed_field)) sequentially"
using lim_1_over_n by (simp add: inverse_eq_divide)
@@ -2236,7 +2226,7 @@
then have "x \<in> \<Union>C" using C by auto
with C(2) obtain c where "x \<in> c" "open c" "c \<in> C" by auto
then obtain e where "0 < e" "{x - e <..< x + e} \<subseteq> c"
- by (auto simp: open_real_def dist_real_def subset_eq Ball_def abs_less_iff)
+ by (auto simp: open_dist dist_real_def subset_eq Ball_def abs_less_iff)
with \<open>c \<in> C\<close> show ?case
by (safe intro!: exI[of _ "e/2"] exI[of _ "{c}"]) auto
qed
--- a/src/HOL/Multivariate_Analysis/Bounded_Continuous_Function.thy Fri Jan 08 16:37:56 2016 +0100
+++ b/src/HOL/Multivariate_Analysis/Bounded_Continuous_Function.thy Fri Jan 08 17:40:59 2016 +0100
@@ -36,14 +36,18 @@
using Rep_bcontfun[of x]
by (auto simp: bcontfun_def intro: continuous_on_subset)
+(* TODO: Generalize to uniform spaces? *)
instantiation bcontfun :: (topological_space, metric_space) metric_space
begin
definition dist_bcontfun :: "('a, 'b) bcontfun \<Rightarrow> ('a, 'b) bcontfun \<Rightarrow> real"
where "dist_bcontfun f g = (SUP x. dist (Rep_bcontfun f x) (Rep_bcontfun g x))"
+definition uniformity_bcontfun :: "(('a, 'b) bcontfun \<times> ('a, 'b) bcontfun) filter"
+ where "uniformity_bcontfun = (INF e:{0 <..}. principal {(x, y). dist x y < e})"
+
definition open_bcontfun :: "('a, 'b) bcontfun set \<Rightarrow> bool"
- where "open_bcontfun S = (\<forall>x\<in>S. \<exists>e>0. \<forall>y. dist y x < e \<longrightarrow> y \<in> S)"
+ where "open_bcontfun S = (\<forall>x\<in>S. \<forall>\<^sub>F (x', y) in uniformity. x' = x \<longrightarrow> y \<in> S)"
lemma dist_bounded:
fixes f :: "('a, 'b) bcontfun"
@@ -126,7 +130,7 @@
finally show "dist (Rep_bcontfun f x) (Rep_bcontfun g x) \<le> dist f h + dist g h"
by simp
qed
-qed (simp add: open_bcontfun_def)
+qed (rule open_bcontfun_def uniformity_bcontfun_def)+
end
--- a/src/HOL/Multivariate_Analysis/Bounded_Linear_Function.thy Fri Jan 08 16:37:56 2016 +0100
+++ b/src/HOL/Multivariate_Analysis/Bounded_Linear_Function.thy Fri Jan 08 17:40:59 2016 +0100
@@ -122,8 +122,11 @@
definition dist_blinfun :: "'a \<Rightarrow>\<^sub>L 'b \<Rightarrow> 'a \<Rightarrow>\<^sub>L 'b \<Rightarrow> real"
where "dist_blinfun a b = norm (a - b)"
+definition [code del]:
+ "(uniformity :: (('a \<Rightarrow>\<^sub>L 'b) \<times> ('a \<Rightarrow>\<^sub>L 'b)) filter) = (INF e:{0 <..}. principal {(x, y). dist x y < e})"
+
definition open_blinfun :: "('a \<Rightarrow>\<^sub>L 'b) set \<Rightarrow> bool"
- where "open_blinfun S \<longleftrightarrow> (\<forall>x\<in>S. \<exists>e>0. \<forall>y. dist y x < e \<longrightarrow> y \<in> S)"
+ where [code del]: "open_blinfun S = (\<forall>x\<in>S. \<forall>\<^sub>F (x', y) in uniformity. x' = x \<longrightarrow> y \<in> S)"
lift_definition uminus_blinfun :: "'a \<Rightarrow>\<^sub>L 'b \<Rightarrow> 'a \<Rightarrow>\<^sub>L 'b" is "\<lambda>f x. - f x"
by (rule bounded_linear_minus)
@@ -143,8 +146,8 @@
instance
apply standard
- unfolding dist_blinfun_def open_blinfun_def sgn_blinfun_def
- apply (transfer, force simp: onorm_triangle onorm_scaleR onorm_eq_0 algebra_simps)+
+ unfolding dist_blinfun_def open_blinfun_def sgn_blinfun_def uniformity_blinfun_def
+ apply (rule refl | (transfer, force simp: onorm_triangle onorm_scaleR onorm_eq_0 algebra_simps))+
done
end
--- a/src/HOL/Multivariate_Analysis/Cauchy_Integral_Thm.thy Fri Jan 08 16:37:56 2016 +0100
+++ b/src/HOL/Multivariate_Analysis/Cauchy_Integral_Thm.thy Fri Jan 08 17:40:59 2016 +0100
@@ -4106,7 +4106,7 @@
done
} then
show ?thesis
- by (auto simp: Complex.open_complex_def)
+ by (auto simp: open_dist)
qed
subsection\<open>Winding number is zero "outside" a curve, in various senses\<close>
--- a/src/HOL/Multivariate_Analysis/Derivative.thy Fri Jan 08 16:37:56 2016 +0100
+++ b/src/HOL/Multivariate_Analysis/Derivative.thy Fri Jan 08 17:40:59 2016 +0100
@@ -874,8 +874,7 @@
unfolding eventually_at_topological
by metis
from \<open>open S\<close> obtain d where d: "\<And>x. dist x y < d \<Longrightarrow> x \<in> S" "d > 0"
- by (force simp: dist_commute open_real_def ball_def
- dest!: bspec[OF _ \<open>y \<in> S\<close>])
+ by (force simp: dist_commute open_dist ball_def dest!: bspec[OF _ \<open>y \<in> S\<close>])
def d' \<equiv> "min ((y + b)/2) (y + (d/2))"
have "d' \<in> A"
unfolding A_def
@@ -939,8 +938,7 @@
where S: "open S" "y \<in> S" "\<And>x. x\<in>S \<Longrightarrow> x \<in> {y..b} \<Longrightarrow> ?le x"
by metis
from \<open>open S\<close> obtain d where d: "\<And>x. dist x y < d \<Longrightarrow> x \<in> S" "d > 0"
- by (force simp: dist_commute open_real_def ball_def
- dest!: bspec[OF _ \<open>y \<in> S\<close>])
+ by (force simp: dist_commute open_dist ball_def dest!: bspec[OF _ \<open>y \<in> S\<close>])
def d' \<equiv> "min b (y + (d/2))"
have "d' \<in> A"
unfolding A_def
--- a/src/HOL/Multivariate_Analysis/Finite_Cartesian_Product.thy Fri Jan 08 16:37:56 2016 +0100
+++ b/src/HOL/Multivariate_Analysis/Finite_Cartesian_Product.thy Fri Jan 08 17:40:59 2016 +0100
@@ -142,7 +142,7 @@
instantiation vec :: (topological_space, finite) topological_space
begin
-definition
+definition [code del]:
"open (S :: ('a ^ 'b) set) \<longleftrightarrow>
(\<forall>x\<in>S. \<exists>A. (\<forall>i. open (A i) \<and> x$i \<in> A i) \<and>
(\<forall>y. (\<forall>i. y$i \<in> A i) \<longrightarrow> y \<in> S))"
@@ -260,13 +260,31 @@
subsection \<open>Metric space\<close>
+(* TODO: Product of uniform spaces and compatibility with metric_spaces! *)
-instantiation vec :: (metric_space, finite) metric_space
+instantiation vec :: (metric_space, finite) dist
begin
definition
"dist x y = setL2 (\<lambda>i. dist (x$i) (y$i)) UNIV"
+instance ..
+end
+
+instantiation vec :: (metric_space, finite) uniformity_dist
+begin
+
+definition [code del]:
+ "(uniformity :: (('a, 'b) vec \<times> ('a, 'b) vec) filter) =
+ (INF e:{0 <..}. principal {(x, y). dist x y < e})"
+
+instance
+ by standard (rule uniformity_vec_def)
+end
+
+instantiation vec :: (metric_space, finite) metric_space
+begin
+
lemma dist_vec_nth_le: "dist (x $ i) (y $ i) \<le> dist x y"
unfolding dist_vec_def by (rule member_le_setL2) simp_all
@@ -284,7 +302,7 @@
done
next
fix S :: "('a ^ 'b) set"
- show "open S \<longleftrightarrow> (\<forall>x\<in>S. \<exists>e>0. \<forall>y. dist y x < e \<longrightarrow> y \<in> S)"
+ have *: "open S \<longleftrightarrow> (\<forall>x\<in>S. \<exists>e>0. \<forall>y. dist y x < e \<longrightarrow> y \<in> S)"
proof
assume "open S" show "\<forall>x\<in>S. \<exists>e>0. \<forall>y. dist y x < e \<longrightarrow> y \<in> S"
proof
@@ -322,6 +340,9 @@
(\<forall>y. (\<forall>i. y $ i \<in> A i) \<longrightarrow> y \<in> S)" by metis
qed
qed
+ show "open S = (\<forall>x\<in>S. \<forall>\<^sub>F (x', y) in uniformity. x' = x \<longrightarrow> y \<in> S)"
+ unfolding * eventually_uniformity_metric
+ by (simp del: split_paired_All add: dist_vec_def dist_commute)
qed
end
--- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Fri Jan 08 16:37:56 2016 +0100
+++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Fri Jan 08 17:40:59 2016 +0100
@@ -13,7 +13,6 @@
"~~/src/HOL/Library/FuncSet"
Linear_Algebra
Norm_Arith
-
begin
lemma image_affinity_interval:
@@ -4573,20 +4572,19 @@
subsubsection \<open>Completeness\<close>
-definition complete :: "'a::metric_space set \<Rightarrow> bool"
- where "complete s \<longleftrightarrow> (\<forall>f. (\<forall>n. f n \<in> s) \<and> Cauchy f \<longrightarrow> (\<exists>l\<in>s. f \<longlonglongrightarrow> l))"
-
-lemma completeI:
+lemma (in metric_space) completeI:
assumes "\<And>f. \<forall>n. f n \<in> s \<Longrightarrow> Cauchy f \<Longrightarrow> \<exists>l\<in>s. f \<longlonglongrightarrow> l"
shows "complete s"
using assms unfolding complete_def by fast
-lemma completeE:
+lemma (in metric_space) completeE:
assumes "complete s" and "\<forall>n. f n \<in> s" and "Cauchy f"
obtains l where "l \<in> s" and "f \<longlonglongrightarrow> l"
using assms unfolding complete_def by fast
+(* TODO: generalize to uniform spaces *)
lemma compact_imp_complete:
+ fixes s :: "'a::metric_space set"
assumes "compact s"
shows "complete s"
proof -
@@ -4816,6 +4814,7 @@
qed
lemma complete_imp_closed:
+ fixes s :: "'a::metric_space set"
assumes "complete s"
shows "closed s"
proof (unfold closed_sequential_limits, clarify)
@@ -4831,6 +4830,7 @@
qed
lemma complete_inter_closed:
+ fixes s :: "'a::metric_space set"
assumes "complete s" and "closed t"
shows "complete (s \<inter> t)"
proof (rule completeI)
@@ -4846,6 +4846,7 @@
qed
lemma complete_closed_subset:
+ fixes s :: "'a::metric_space set"
assumes "closed s" and "s \<subseteq> t" and "complete t"
shows "complete s"
using assms complete_inter_closed [of t s] by (simp add: Int_absorb1)
@@ -5225,9 +5226,13 @@
unfolding continuous_on_def Lim_within
by (metis dist_pos_lt dist_self)
-definition uniformly_continuous_on :: "'a set \<Rightarrow> ('a::metric_space \<Rightarrow> 'b::metric_space) \<Rightarrow> bool"
- where "uniformly_continuous_on s f \<longleftrightarrow>
+lemma uniformly_continuous_on_def:
+ fixes f :: "'a::metric_space \<Rightarrow> 'b::metric_space"
+ shows "uniformly_continuous_on s f \<longleftrightarrow>
(\<forall>e>0. \<exists>d>0. \<forall>x\<in>s. \<forall>x'\<in>s. dist x' x < d \<longrightarrow> dist (f x') (f x) < e)"
+ unfolding uniformly_continuous_on_uniformity
+ uniformity_dist filterlim_INF filterlim_principal eventually_inf_principal
+ by (force simp: Ball_def uniformity_dist[symmetric] eventually_uniformity_metric)
text\<open>Some simple consequential lemmas.\<close>
@@ -5242,10 +5247,6 @@
using assms
by (auto simp: uniformly_continuous_on_def)
-lemma uniformly_continuous_imp_continuous:
- "uniformly_continuous_on s f \<Longrightarrow> continuous_on s f"
- unfolding uniformly_continuous_on_def continuous_on_iff by blast
-
lemma continuous_at_imp_continuous_within:
"continuous (at x) f \<Longrightarrow> continuous (at x within s) f"
unfolding continuous_within continuous_at using Lim_at_imp_Lim_at_within by auto
@@ -5331,8 +5332,7 @@
lemma uniformly_continuous_on_sequentially:
"uniformly_continuous_on s f \<longleftrightarrow> (\<forall>x y. (\<forall>n. x n \<in> s) \<and> (\<forall>n. y n \<in> s) \<and>
- ((\<lambda>n. dist (x n) (y n)) \<longlongrightarrow> 0) sequentially
- \<longrightarrow> ((\<lambda>n. dist (f(x n)) (f(y n))) \<longlongrightarrow> 0) sequentially)" (is "?lhs = ?rhs")
+ (\<lambda>n. dist (x n) (y n)) \<longlonglongrightarrow> 0 \<longrightarrow> (\<lambda>n. dist (f(x n)) (f(y n))) \<longlonglongrightarrow> 0)" (is "?lhs = ?rhs")
proof
assume ?lhs
{
@@ -5421,7 +5421,7 @@
using assms
unfolding continuous_within
by (force simp add: intro: Lim_transform_within)
-
+
subsubsection \<open>Structural rules for pointwise continuity\<close>
@@ -5462,14 +5462,6 @@
subsubsection \<open>Structural rules for uniform continuity\<close>
-lemma uniformly_continuous_on_id[continuous_intros]:
- "uniformly_continuous_on s (\<lambda>x. x)"
- unfolding uniformly_continuous_on_def by auto
-
-lemma uniformly_continuous_on_const[continuous_intros]:
- "uniformly_continuous_on s (\<lambda>x. c)"
- unfolding uniformly_continuous_on_def by simp
-
lemma uniformly_continuous_on_dist[continuous_intros]:
fixes f g :: "'a::metric_space \<Rightarrow> 'b::metric_space"
assumes "uniformly_continuous_on s f"
@@ -5497,12 +5489,14 @@
qed
lemma uniformly_continuous_on_norm[continuous_intros]:
+ fixes f :: "'a :: metric_space \<Rightarrow> 'b :: real_normed_vector"
assumes "uniformly_continuous_on s f"
shows "uniformly_continuous_on s (\<lambda>x. norm (f x))"
unfolding norm_conv_dist using assms
by (intro uniformly_continuous_on_dist uniformly_continuous_on_const)
lemma (in bounded_linear) uniformly_continuous_on[continuous_intros]:
+ fixes g :: "_::metric_space \<Rightarrow> _"
assumes "uniformly_continuous_on s g"
shows "uniformly_continuous_on s (\<lambda>x. f (g x))"
using assms unfolding uniformly_continuous_on_sequentially
@@ -5544,30 +5538,9 @@
using assms uniformly_continuous_on_add [of s f "- g"]
by (simp add: fun_Compl_def uniformly_continuous_on_minus)
-text\<open>Continuity of all kinds is preserved under composition.\<close>
-
lemmas continuous_at_compose = isCont_o
-lemma uniformly_continuous_on_compose[continuous_intros]:
- assumes "uniformly_continuous_on s f" "uniformly_continuous_on (f ` s) g"
- shows "uniformly_continuous_on s (g \<circ> f)"
-proof -
- {
- fix e :: real
- assume "e > 0"
- then obtain d where "d > 0"
- and d: "\<forall>x\<in>f ` s. \<forall>x'\<in>f ` s. dist x' x < d \<longrightarrow> dist (g x') (g x) < e"
- using assms(2) unfolding uniformly_continuous_on_def by auto
- obtain d' where "d'>0" "\<forall>x\<in>s. \<forall>x'\<in>s. dist x' x < d' \<longrightarrow> dist (f x') (f x) < d"
- using \<open>d > 0\<close> using assms(1) unfolding uniformly_continuous_on_def by auto
- then have "\<exists>d>0. \<forall>x\<in>s. \<forall>x'\<in>s. dist x' x < d \<longrightarrow> dist ((g \<circ> f) x') ((g \<circ> f) x) < e"
- using \<open>d>0\<close> using d by auto
- }
- then show ?thesis
- using assms unfolding uniformly_continuous_on_def by auto
-qed
-
-text\<open>Continuity in terms of open preimages.\<close>
+text \<open>Continuity in terms of open preimages.\<close>
lemma continuous_at_open:
"continuous (at x) f \<longleftrightarrow> (\<forall>t. open t \<and> f x \<in> t --> (\<exists>s. open s \<and> x \<in> s \<and> (\<forall>x' \<in> s. (f x') \<in> t)))"
@@ -6124,6 +6097,7 @@
text \<open>Continuity implies uniform continuity on a compact domain.\<close>
lemma compact_uniformly_continuous:
+ fixes f :: "'a :: metric_space \<Rightarrow> 'b :: metric_space"
assumes f: "continuous_on s f"
and s: "compact s"
shows "uniformly_continuous_on s f"
--- a/src/HOL/Probability/Discrete_Topology.thy Fri Jan 08 16:37:56 2016 +0100
+++ b/src/HOL/Probability/Discrete_Topology.thy Fri Jan 08 17:40:59 2016 +0100
@@ -12,24 +12,24 @@
morphisms of_discrete discrete
..
-instantiation discrete :: (type) topological_space
-begin
-
-definition open_discrete::"'a discrete set \<Rightarrow> bool"
- where "open_discrete s = True"
-
-instance proof qed (auto simp: open_discrete_def)
-end
-
instantiation discrete :: (type) metric_space
begin
-definition dist_discrete::"'a discrete \<Rightarrow> 'a discrete \<Rightarrow> real"
+definition dist_discrete :: "'a discrete \<Rightarrow> 'a discrete \<Rightarrow> real"
where "dist_discrete n m = (if n = m then 0 else 1)"
-instance proof qed (auto simp: open_discrete_def dist_discrete_def intro: exI[where x=1])
+definition uniformity_discrete :: "('a discrete \<times> 'a discrete) filter" where
+ "(uniformity::('a discrete \<times> 'a discrete) filter) = (INF e:{0 <..}. principal {(x, y). dist x y < e})"
+
+definition "open_discrete" :: "'a discrete set \<Rightarrow> bool" where
+ "(open::'a discrete set \<Rightarrow> bool) U \<longleftrightarrow> (\<forall>x\<in>U. eventually (\<lambda>(x', y). x' = x \<longrightarrow> y \<in> U) uniformity)"
+
+instance proof qed (auto simp: uniformity_discrete_def open_discrete_def dist_discrete_def intro: exI[where x=1])
end
+lemma open_discrete: "open (S :: 'a discrete set)"
+ unfolding open_dist dist_discrete_def by (auto intro!: exI[of _ "1 / 2"])
+
instance discrete :: (type) complete_space
proof
fix X::"nat\<Rightarrow>'a discrete" assume "Cauchy X"
@@ -54,7 +54,7 @@
have "\<And>S. generate_topology ?B (\<Union>x\<in>S. {x})"
by (intro generate_topology_Union) (auto intro: generate_topology.intros)
then have "open = generate_topology ?B"
- by (auto intro!: ext simp: open_discrete_def)
+ by (auto intro!: ext simp: open_discrete)
moreover have "countable ?B" by simp
ultimately show "\<exists>B::'a discrete set set. countable B \<and> open = generate_topology B" by blast
qed
--- a/src/HOL/Probability/Fin_Map.thy Fri Jan 08 16:37:56 2016 +0100
+++ b/src/HOL/Probability/Fin_Map.thy Fri Jan 08 17:40:59 2016 +0100
@@ -150,7 +150,7 @@
begin
definition open_finmap :: "('a \<Rightarrow>\<^sub>F 'b) set \<Rightarrow> bool" where
- "open_finmap = generate_topology {Pi' a b|a b. \<forall>i\<in>a. open (b i)}"
+ [code del]: "open_finmap = generate_topology {Pi' a b|a b. \<forall>i\<in>a. open (b i)}"
lemma open_Pi'I: "(\<And>i. i \<in> I \<Longrightarrow> open (A i)) \<Longrightarrow> open (Pi' I A)"
by (auto intro: generate_topology.Basis simp: open_finmap_def)
@@ -254,12 +254,31 @@
subsection \<open>Metric Space of Finite Maps\<close>
-instantiation finmap :: (type, metric_space) metric_space
+(* TODO: Product of uniform spaces and compatibility with metric_spaces! *)
+
+instantiation finmap :: (type, metric_space) dist
begin
definition dist_finmap where
"dist P Q = Max (range (\<lambda>i. dist ((P)\<^sub>F i) ((Q)\<^sub>F i))) + (if domain P = domain Q then 0 else 1)"
+instance ..
+end
+
+instantiation finmap :: (type, metric_space) uniformity_dist
+begin
+
+definition [code del]:
+ "(uniformity :: (('a, 'b) finmap \<times> ('a, 'b) finmap) filter) =
+ (INF e:{0 <..}. principal {(x, y). dist x y < e})"
+
+instance
+ by standard (rule uniformity_finmap_def)
+end
+
+instantiation finmap :: (type, metric_space) metric_space
+begin
+
lemma finite_proj_image': "x \<notin> domain P \<Longrightarrow> finite ((P)\<^sub>F ` S)"
by (rule finite_subset[of _ "proj P ` (domain P \<inter> S \<union> {x})"]) auto
@@ -308,7 +327,7 @@
instance
proof
fix S::"('a \<Rightarrow>\<^sub>F 'b) set"
- show "open S = (\<forall>x\<in>S. \<exists>e>0. \<forall>y. dist y x < e \<longrightarrow> y \<in> S)" (is "_ = ?od")
+ have *: "open S = (\<forall>x\<in>S. \<exists>e>0. \<forall>y. dist y x < e \<longrightarrow> y \<in> S)" (is "_ = ?od")
proof
assume "open S"
thus ?od
@@ -387,6 +406,9 @@
by (intro generate_topology.UN) (auto intro: generate_topology.Basis)
finally show "open S" .
qed
+ show "open S = (\<forall>x\<in>S. \<forall>\<^sub>F (x', y) in uniformity. x' = x \<longrightarrow> y \<in> S)"
+ unfolding * eventually_uniformity_metric
+ by (simp del: split_paired_All add: dist_finmap_def dist_commute eq_commute)
next
fix P Q::"'a \<Rightarrow>\<^sub>F 'b"
have Max_eq_iff: "\<And>A m. finite A \<Longrightarrow> A \<noteq> {} \<Longrightarrow> (Max A = m) = (m \<in> A \<and> (\<forall>a\<in>A. a \<le> m))"
--- a/src/HOL/Product_Type.thy Fri Jan 08 16:37:56 2016 +0100
+++ b/src/HOL/Product_Type.thy Fri Jan 08 17:40:59 2016 +0100
@@ -1068,6 +1068,9 @@
lemma mem_Sigma_iff [iff]: "((a,b): Sigma A B) = (a:A & b:B(a))"
by blast
+lemma mem_Times_iff: "x \<in> A \<times> B \<longleftrightarrow> fst x \<in> A \<and> snd x \<in> B"
+ by (induct x) simp
+
lemma Sigma_empty_iff: "(SIGMA i:I. X i) = {} \<longleftrightarrow> (\<forall>i\<in>I. X i = {})"
by auto
--- a/src/HOL/Real_Vector_Spaces.thy Fri Jan 08 16:37:56 2016 +0100
+++ b/src/HOL/Real_Vector_Spaces.thy Fri Jan 08 17:40:59 2016 +0100
@@ -191,7 +191,7 @@
fixes x :: "'a::real_vector"
shows "scaleR (-1) x = - x"
using scaleR_minus_left [of 1 x] by simp
-
+
class real_algebra = real_vector + ring +
assumes mult_scaleR_left [simp]: "scaleR a x * y = scaleR a (x * y)"
and mult_scaleR_right [simp]: "x * scaleR a y = scaleR a (x * y)"
@@ -662,10 +662,19 @@
class dist_norm = dist + norm + minus +
assumes dist_norm: "dist x y = norm (x - y)"
-class open_dist = "open" + dist +
- assumes open_dist: "open S \<longleftrightarrow> (\<forall>x\<in>S. \<exists>e>0. \<forall>y. dist y x < e \<longrightarrow> y \<in> S)"
+class uniformity_dist = dist + uniformity +
+ assumes uniformity_dist: "uniformity = (INF e:{0 <..}. principal {(x, y). dist x y < e})"
+begin
-class real_normed_vector = real_vector + sgn_div_norm + dist_norm + open_dist +
+lemma eventually_uniformity_metric:
+ "eventually P uniformity \<longleftrightarrow> (\<exists>e>0. \<forall>x y. dist x y < e \<longrightarrow> P (x, y))"
+ unfolding uniformity_dist
+ by (subst eventually_INF_base)
+ (auto simp: eventually_principal subset_eq intro: bexI[of _ "min _ _"])
+
+end
+
+class real_normed_vector = real_vector + sgn_div_norm + dist_norm + uniformity_dist + open_uniformity +
assumes norm_eq_zero [simp]: "norm x = 0 \<longleftrightarrow> x = 0"
and norm_triangle_ineq: "norm (x + y) \<le> norm x + norm y"
and norm_scaleR [simp]: "norm (scaleR a x) = \<bar>a\<bar> * norm x"
@@ -686,8 +695,8 @@
class real_normed_algebra_1 = real_algebra_1 + real_normed_algebra +
assumes norm_one [simp]: "norm 1 = 1"
-
-lemma (in real_normed_algebra_1) scaleR_power [simp]:
+
+lemma (in real_normed_algebra_1) scaleR_power [simp]:
"(scaleR x y) ^ n = scaleR (x^n) (y^n)"
by (induction n) (simp_all add: scaleR_one scaleR_scaleR mult_ac)
@@ -1010,7 +1019,7 @@
subsection \<open>Metric spaces\<close>
-class metric_space = open_dist +
+class metric_space = uniformity_dist + open_uniformity +
assumes dist_eq_0_iff [simp]: "dist x y = 0 \<longleftrightarrow> x = y"
assumes dist_triangle2: "dist x y \<le> dist x z + dist y z"
begin
@@ -1074,26 +1083,23 @@
shows "dist y x1 < e / 2 \<Longrightarrow> dist y x2 < e / 2 \<Longrightarrow> dist x1 x2 < e"
by (rule dist_triangle_half_l, simp_all add: dist_commute)
-subclass topological_space
+subclass uniform_space
proof
- have "\<exists>e::real. 0 < e"
- by (blast 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 \<inter> 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 "\<forall>S\<in>K. open S" thus "open (\<Union>K)"
- unfolding open_dist by (meson UnionE UnionI)
+ fix E x assume "eventually E uniformity"
+ then obtain e where E: "0 < e" "\<And>x y. dist x y < e \<Longrightarrow> E (x, y)"
+ unfolding eventually_uniformity_metric by auto
+ then show "E (x, x)" "\<forall>\<^sub>F (x, y) in uniformity. E (y, x)"
+ unfolding eventually_uniformity_metric by (auto simp: dist_commute)
+
+ show "\<exists>D. eventually D uniformity \<and> (\<forall>x y z. D (x, y) \<longrightarrow> D (y, z) \<longrightarrow> E (x, z))"
+ using E dist_triangle_half_l[where e=e] unfolding eventually_uniformity_metric
+ by (intro exI[of _ "\<lambda>(x, y). dist x y < e / 2"] exI[of _ "e/2"] conjI)
+ (auto simp: dist_commute)
qed
+lemma open_dist: "open S \<longleftrightarrow> (\<forall>x\<in>S. \<exists>e>0. \<forall>y. dist y x < e \<longrightarrow> y \<in> S)"
+ unfolding open_uniformity eventually_uniformity_metric by (simp add: dist_commute)
+
lemma open_ball: "open {y. dist x y < d}"
proof (unfold open_dist, intro ballI)
fix y assume *: "y \<in> {y. dist x y < d}"
@@ -1156,8 +1162,11 @@
definition dist_real_def:
"dist x y = \<bar>x - y\<bar>"
+definition uniformity_real_def [code del]:
+ "(uniformity :: (real \<times> real) filter) = (INF e:{0 <..}. principal {(x, y). dist x y < e})"
+
definition open_real_def [code del]:
- "open (S :: real set) \<longleftrightarrow> (\<forall>x\<in>S. \<exists>e>0. \<forall>y. dist y x < e \<longrightarrow> y \<in> S)"
+ "open (U :: real set) \<longleftrightarrow> (\<forall>x\<in>U. eventually (\<lambda>(x', y). x' = x \<longrightarrow> y \<in> U) uniformity)"
definition real_norm_def [simp]:
"norm r = \<bar>r\<bar>"
@@ -1165,8 +1174,9 @@
instance
apply (intro_classes, unfold real_norm_def real_scaleR_def)
apply (rule dist_real_def)
+apply (simp add: sgn_real_def)
+apply (rule uniformity_real_def)
apply (rule open_real_def)
-apply (simp add: sgn_real_def)
apply (rule abs_eq_0)
apply (rule abs_triangle_ineq)
apply (rule abs_mult)
@@ -1188,7 +1198,7 @@
proof (rule ext, safe)
fix S :: "real set" assume "open S"
then obtain f where "\<forall>x\<in>S. 0 < f x \<and> (\<forall>y. dist y x < f x \<longrightarrow> y \<in> S)"
- unfolding open_real_def bchoice_iff ..
+ unfolding open_dist bchoice_iff ..
then have *: "S = (\<Union>x\<in>S. {x - f x <..} \<inter> {..< x + f x})"
by (fastforce simp: dist_real_def)
show "generate_topology (range lessThan \<union> range greaterThan) S"
@@ -1199,14 +1209,14 @@
next
fix S :: "real set" assume "generate_topology (range lessThan \<union> range greaterThan) S"
moreover have "\<And>a::real. open {..<a}"
- unfolding open_real_def dist_real_def
+ unfolding open_dist dist_real_def
proof clarify
fix x a :: real assume "x < a"
hence "0 < a - x \<and> (\<forall>y. \<bar>y - x\<bar> < a - x \<longrightarrow> y \<in> {..<a})" by auto
thus "\<exists>e>0. \<forall>y. \<bar>y - x\<bar> < e \<longrightarrow> y \<in> {..<a}" ..
qed
moreover have "\<And>a::real. open {a <..}"
- unfolding open_real_def dist_real_def
+ unfolding open_dist dist_real_def
proof clarify
fix x a :: real assume "a < x"
hence "0 < x - a \<and> (\<forall>y. \<bar>y - x\<bar> < x - a \<longrightarrow> y \<in> {a<..})" by auto
@@ -1233,6 +1243,11 @@
setup \<open>Sign.add_const_constraint
(@{const_name "open"}, SOME @{typ "'a::topological_space set \<Rightarrow> bool"})\<close>
+text \<open>Only allow @{term "uniformity"} in class \<open>uniform_space\<close>.\<close>
+
+setup \<open>Sign.add_const_constraint
+ (@{const_name "uniformity"}, SOME @{typ "('a::uniformity \<times> 'a) filter"})\<close>
+
text \<open>Only allow @{term dist} in class \<open>metric_space\<close>.\<close>
setup \<open>Sign.add_const_constraint
@@ -1786,10 +1801,22 @@
subsection \<open>Cauchy sequences\<close>
-definition (in metric_space) Cauchy :: "(nat \<Rightarrow> 'a) \<Rightarrow> bool" where
- "Cauchy X = (\<forall>e>0. \<exists>M. \<forall>m \<ge> M. \<forall>n \<ge> M. dist (X m) (X n) < e)"
+lemma (in metric_space) Cauchy_def: "Cauchy X = (\<forall>e>0. \<exists>M. \<forall>m\<ge>M. \<forall>n\<ge>M. dist (X m) (X n) < e)"
+proof -
+ have *: "eventually P (INF M. principal {(X m, X n) | n m. m \<ge> M \<and> n \<ge> M}) =
+ (\<exists>M. \<forall>m\<ge>M. \<forall>n\<ge>M. P (X m, X n))" for P
+ proof (subst eventually_INF_base, goal_cases)
+ case (2 a b) then show ?case
+ by (intro bexI[of _ "max a b"]) (auto simp: eventually_principal subset_eq)
+ qed (auto simp: eventually_principal, blast)
+ have "Cauchy X \<longleftrightarrow> (INF M. principal {(X m, X n) | n m. m \<ge> M \<and> n \<ge> M}) \<le> uniformity"
+ unfolding Cauchy_uniform_iff le_filter_def * ..
+ also have "\<dots> = (\<forall>e>0. \<exists>M. \<forall>m\<ge>M. \<forall>n\<ge>M. dist (X m) (X n) < e)"
+ unfolding uniformity_dist le_INF_iff by (auto simp: * le_principal)
+ finally show ?thesis .
+qed
-lemma Cauchy_altdef:
+lemma (in metric_space) Cauchy_altdef:
"Cauchy f = (\<forall>e>0. \<exists>M. \<forall>m\<ge>M. \<forall>n>m. dist (f m) (f n) < e)"
proof
assume A: "\<forall>e>0. \<exists>M. \<forall>m\<ge>M. \<forall>n>m. dist (f m) (f n) < e"
@@ -1812,18 +1839,18 @@
qed
qed
-lemma metric_CauchyI:
+lemma (in metric_space) metric_CauchyI:
"(\<And>e. 0 < e \<Longrightarrow> \<exists>M. \<forall>m\<ge>M. \<forall>n\<ge>M. dist (X m) (X n) < e) \<Longrightarrow> Cauchy X"
by (simp add: Cauchy_def)
-lemma CauchyI': "(\<And>e. 0 < e \<Longrightarrow> \<exists>M. \<forall>m\<ge>M. \<forall>n>m. dist (X m) (X n) < e) \<Longrightarrow> Cauchy X"
+lemma (in metric_space) CauchyI': "(\<And>e. 0 < e \<Longrightarrow> \<exists>M. \<forall>m\<ge>M. \<forall>n>m. dist (X m) (X n) < e) \<Longrightarrow> Cauchy X"
unfolding Cauchy_altdef by blast
-lemma metric_CauchyD:
+lemma (in metric_space) metric_CauchyD:
"Cauchy X \<Longrightarrow> 0 < e \<Longrightarrow> \<exists>M. \<forall>m\<ge>M. \<forall>n\<ge>M. dist (X m) (X n) < e"
by (simp add: Cauchy_def)
-lemma metric_Cauchy_iff2:
+lemma (in metric_space) metric_Cauchy_iff2:
"Cauchy X = (\<forall>j. (\<exists>M. \<forall>m \<ge> M. \<forall>n \<ge> M. dist (X m) (X n) < inverse(real (Suc j))))"
apply (simp add: Cauchy_def, auto)
apply (drule reals_Archimedean, safe)
@@ -1837,40 +1864,118 @@
"Cauchy X = (\<forall>j. (\<exists>M. \<forall>m \<ge> M. \<forall>n \<ge> M. \<bar>X m - X n\<bar> < inverse(real (Suc j))))"
unfolding metric_Cauchy_iff2 dist_real_def ..
-lemma Cauchy_subseq_Cauchy:
- "\<lbrakk> Cauchy X; subseq f \<rbrakk> \<Longrightarrow> 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
-
-theorem LIMSEQ_imp_Cauchy:
- assumes X: "X \<longlonglongrightarrow> a" shows "Cauchy X"
-proof (rule metric_CauchyI)
- fix e::real assume "0 < e"
- hence "0 < e/2" by simp
- with X have "\<exists>N. \<forall>n\<ge>N. dist (X n) a < e/2" by (rule metric_LIMSEQ_D)
- then obtain N where N: "\<forall>n\<ge>N. dist (X n) a < e/2" ..
- show "\<exists>N. \<forall>m\<ge>N. \<forall>n\<ge>N. dist (X m) (X n) < e"
- proof (intro exI allI impI)
- fix m assume "N \<le> m"
- hence m: "dist (X m) a < e/2" using N by blast
- fix n assume "N \<le> n"
- hence n: "dist (X n) a < e/2" using N by blast
- have "dist (X m) (X n) \<le> dist (X m) a + dist (X n) a"
- by (rule dist_triangle2)
- also from m n have "\<dots> < e" by simp
- finally show "dist (X m) (X n) < e" .
- qed
+lemma lim_1_over_n: "((\<lambda>n. 1 / of_nat n) \<longlongrightarrow> (0::'a::real_normed_field)) sequentially"
+proof (subst lim_sequentially, intro allI impI exI)
+ fix e :: real assume e: "e > 0"
+ fix n :: nat assume n: "n \<ge> nat \<lceil>inverse e + 1\<rceil>"
+ have "inverse e < of_nat (nat \<lceil>inverse e + 1\<rceil>)" by linarith
+ also note n
+ finally show "dist (1 / of_nat n :: 'a) 0 < e" using e
+ by (simp add: divide_simps mult.commute norm_conv_dist[symmetric] norm_divide)
qed
-lemma convergent_Cauchy: "convergent X \<Longrightarrow> Cauchy X"
-unfolding convergent_def
-by (erule exE, erule LIMSEQ_imp_Cauchy)
+lemma (in metric_space) complete_def:
+ shows "complete S = (\<forall>f. (\<forall>n. f n \<in> S) \<and> Cauchy f \<longrightarrow> (\<exists>l\<in>S. f \<longlonglongrightarrow> l))"
+ unfolding complete_uniform
+proof safe
+ fix f :: "nat \<Rightarrow> 'a" assume f: "\<forall>n. f n \<in> S" "Cauchy f"
+ and *: "\<forall>F\<le>principal S. F \<noteq> bot \<longrightarrow> cauchy_filter F \<longrightarrow> (\<exists>x\<in>S. F \<le> nhds x)"
+ then show "\<exists>l\<in>S. f \<longlonglongrightarrow> l"
+ unfolding filterlim_def using f
+ by (intro *[rule_format])
+ (auto simp: filtermap_sequentually_ne_bot le_principal eventually_filtermap Cauchy_uniform)
+next
+ fix F :: "'a filter" assume "F \<le> principal S" "F \<noteq> bot" "cauchy_filter F"
+ assume seq: "\<forall>f. (\<forall>n. f n \<in> S) \<and> Cauchy f \<longrightarrow> (\<exists>l\<in>S. f \<longlonglongrightarrow> l)"
+
+ from \<open>F \<le> principal S\<close> \<open>cauchy_filter F\<close> have FF_le: "F \<times>\<^sub>F F \<le> uniformity_on S"
+ by (simp add: cauchy_filter_def principal_prod_principal[symmetric] prod_filter_mono)
+
+ let ?P = "\<lambda>P e. eventually P F \<and> (\<forall>x. P x \<longrightarrow> x \<in> S) \<and> (\<forall>x y. P x \<longrightarrow> P y \<longrightarrow> dist x y < e)"
+
+ { fix \<epsilon> :: real assume "0 < \<epsilon>"
+ then have "eventually (\<lambda>(x, y). x \<in> S \<and> y \<in> S \<and> dist x y < \<epsilon>) (uniformity_on S)"
+ unfolding eventually_inf_principal eventually_uniformity_metric by auto
+ from filter_leD[OF FF_le this] have "\<exists>P. ?P P \<epsilon>"
+ unfolding eventually_prod_same by auto }
+ note P = this
+
+ have "\<exists>P. \<forall>n. ?P (P n) (1 / Suc n) \<and> P (Suc n) \<le> P n"
+ proof (rule dependent_nat_choice)
+ show "\<exists>P. ?P P (1 / Suc 0)"
+ using P[of 1] by auto
+ next
+ fix P n assume "?P P (1/Suc n)"
+ moreover obtain Q where "?P Q (1 / Suc (Suc n))"
+ using P[of "1/Suc (Suc n)"] by auto
+ ultimately show "\<exists>Q. ?P Q (1 / Suc (Suc n)) \<and> Q \<le> P"
+ by (intro exI[of _ "\<lambda>x. P x \<and> Q x"]) (auto simp: eventually_conj_iff)
+ qed
+ then obtain P where P: "\<And>n. eventually (P n) F" "\<And>n x. P n x \<Longrightarrow> x \<in> S"
+ "\<And>n x y. P n x \<Longrightarrow> P n y \<Longrightarrow> dist x y < 1 / Suc n" "\<And>n. P (Suc n) \<le> P n"
+ by metis
+ have "antimono P"
+ using P(4) unfolding decseq_Suc_iff le_fun_def by blast
+
+ obtain X where X: "\<And>n. P n (X n)"
+ using P(1)[THEN eventually_happens'[OF \<open>F \<noteq> bot\<close>]] by metis
+ have "Cauchy X"
+ unfolding metric_Cauchy_iff2 inverse_eq_divide
+ proof (intro exI allI impI)
+ fix j m n :: nat assume "j \<le> m" "j \<le> n"
+ with \<open>antimono P\<close> X have "P j (X m)" "P j (X n)"
+ by (auto simp: antimono_def)
+ then show "dist (X m) (X n) < 1 / Suc j"
+ by (rule P)
+ qed
+ moreover have "\<forall>n. X n \<in> S"
+ using P(2) X by auto
+ ultimately obtain x where "X \<longlonglongrightarrow> x" "x \<in> S"
+ using seq by blast
+
+ show "\<exists>x\<in>S. F \<le> nhds x"
+ proof (rule bexI)
+ { fix e :: real assume "0 < e"
+ then have "(\<lambda>n. 1 / Suc n :: real) \<longlonglongrightarrow> 0 \<and> 0 < e / 2"
+ by (subst LIMSEQ_Suc_iff) (auto intro!: lim_1_over_n)
+ then have "\<forall>\<^sub>F n in sequentially. dist (X n) x < e / 2 \<and> 1 / Suc n < e / 2"
+ using \<open>X \<longlonglongrightarrow> x\<close> unfolding tendsto_iff order_tendsto_iff[where 'a=real] eventually_conj_iff by blast
+ then obtain n where "dist x (X n) < e / 2" "1 / Suc n < e / 2"
+ by (auto simp: eventually_sequentially dist_commute)
+ have "eventually (\<lambda>y. dist y x < e) F"
+ using \<open>eventually (P n) F\<close>
+ proof eventually_elim
+ fix y assume "P n y"
+ then have "dist y (X n) < 1 / Suc n"
+ by (intro X P)
+ also have "\<dots> < e / 2" by fact
+ finally show "dist y x < e"
+ by (rule dist_triangle_half_l) fact
+ qed }
+ then show "F \<le> nhds x"
+ unfolding nhds_metric le_INF_iff le_principal by auto
+ qed fact
+qed
+
+lemma (in metric_space) totally_bounded_metric:
+ "totally_bounded S \<longleftrightarrow> (\<forall>e>0. \<exists>k. finite k \<and> S \<subseteq> (\<Union>x\<in>k. {y. dist x y < e}))"
+ unfolding totally_bounded_def eventually_uniformity_metric imp_ex
+ apply (subst all_comm)
+ apply (intro arg_cong[where f=All] ext)
+ apply safe
+ subgoal for e
+ apply (erule allE[of _ "\<lambda>(x, y). dist x y < e"])
+ apply auto
+ done
+ subgoal for e P k
+ apply (intro exI[of _ k])
+ apply (force simp: subset_eq)
+ done
+ done
subsubsection \<open>Cauchy Sequences are Convergent\<close>
+(* TODO: update to uniform_space *)
class complete_space = metric_space +
assumes Cauchy_convergent: "Cauchy X \<Longrightarrow> convergent X"
--- a/src/HOL/Topological_Spaces.thy Fri Jan 08 16:37:56 2016 +0100
+++ b/src/HOL/Topological_Spaces.thy Fri Jan 08 17:40:59 2016 +0100
@@ -11,7 +11,6 @@
named_theorems continuous_intros "structural introduction rules for continuity"
-
subsection \<open>Topological space\<close>
class "open" =
@@ -693,8 +692,6 @@
by (rule tendsto_le [OF F tendsto_const x a])
-
-
subsubsection \<open>Rules about @{const Lim}\<close>
lemma tendsto_Lim:
@@ -2435,4 +2432,173 @@
qed
qed (intro cSUP_least \<open>antimono f\<close>[THEN antimonoD] cInf_lower S)
+subsection \<open>Uniform spaces\<close>
+
+class uniformity =
+ fixes uniformity :: "('a \<times> 'a) filter"
+begin
+
+abbreviation uniformity_on :: "'a set \<Rightarrow> ('a \<times> 'a) filter" where
+ "uniformity_on s \<equiv> inf uniformity (principal (s\<times>s))"
+
end
+
+class open_uniformity = "open" + uniformity +
+ assumes open_uniformity: "\<And>U. open U \<longleftrightarrow> (\<forall>x\<in>U. eventually (\<lambda>(x', y). x' = x \<longrightarrow> y \<in> U) uniformity)"
+
+class uniform_space = open_uniformity +
+ assumes uniformity_refl: "eventually E uniformity \<Longrightarrow> E (x, x)"
+ assumes uniformity_sym: "eventually E uniformity \<Longrightarrow> eventually (\<lambda>(x, y). E (y, x)) uniformity"
+ assumes uniformity_trans: "eventually E uniformity \<Longrightarrow> \<exists>D. eventually D uniformity \<and> (\<forall>x y z. D (x, y) \<longrightarrow> D (y, z) \<longrightarrow> E (x, z))"
+begin
+
+subclass topological_space
+ proof qed (force elim: eventually_mono eventually_elim2 simp: split_beta' open_uniformity)+
+
+lemma uniformity_bot: "uniformity \<noteq> bot"
+ using uniformity_refl by auto
+
+lemma uniformity_trans':
+ "eventually E uniformity \<Longrightarrow> eventually (\<lambda>((x, y), (y', z)). y = y' \<longrightarrow> E (x, z)) (uniformity \<times>\<^sub>F uniformity)"
+ by (drule uniformity_trans) (auto simp add: eventually_prod_same)
+
+lemma uniformity_transE:
+ assumes E: "eventually E uniformity"
+ obtains D where "eventually D uniformity" "\<And>x y z. D (x, y) \<Longrightarrow> D (y, z) \<Longrightarrow> E (x, z)"
+ using uniformity_trans[OF E] by auto
+
+lemma eventually_nhds_uniformity:
+ "eventually P (nhds x) \<longleftrightarrow> eventually (\<lambda>(x', y). x' = x \<longrightarrow> P y) uniformity" (is "_ \<longleftrightarrow> ?N P x")
+ unfolding eventually_nhds
+proof safe
+ assume *: "?N P x"
+ { fix x assume "?N P x"
+ then guess D by (rule uniformity_transE) note D = this
+ from D(1) have "?N (?N P) x"
+ by eventually_elim (insert D, force elim: eventually_mono split: prod.split) }
+ then have "open {x. ?N P x}"
+ by (simp add: open_uniformity)
+ then show "\<exists>S. open S \<and> x \<in> S \<and> (\<forall>x\<in>S. P x)"
+ by (intro exI[of _ "{x. ?N P x}"]) (auto dest: uniformity_refl simp: *)
+qed (force simp add: open_uniformity elim: eventually_mono)
+
+subsubsection \<open>Totally bounded sets\<close>
+
+definition totally_bounded :: "'a set \<Rightarrow> bool" where
+ "totally_bounded S \<longleftrightarrow>
+ (\<forall>E. eventually E uniformity \<longrightarrow> (\<exists>X. finite X \<and> (\<forall>s\<in>S. \<exists>x\<in>X. E (x, s))))"
+
+lemma totally_bounded_empty[iff]: "totally_bounded {}"
+ by (auto simp add: totally_bounded_def)
+
+lemma totally_bounded_subset: "totally_bounded S \<Longrightarrow> T \<subseteq> S \<Longrightarrow> totally_bounded T"
+ by (force simp add: totally_bounded_def)
+
+lemma totally_bounded_Union[intro]:
+ assumes M: "finite M" "\<And>S. S \<in> M \<Longrightarrow> totally_bounded S" shows "totally_bounded (\<Union>M)"
+ unfolding totally_bounded_def
+proof safe
+ fix E assume "eventually E uniformity"
+ with M obtain X where "\<forall>S\<in>M. finite (X S) \<and> (\<forall>s\<in>S. \<exists>x\<in>X S. E (x, s))"
+ by (metis totally_bounded_def)
+ with `finite M` show "\<exists>X. finite X \<and> (\<forall>s\<in>\<Union>M. \<exists>x\<in>X. E (x, s))"
+ by (intro exI[of _ "\<Union>S\<in>M. X S"]) force
+qed
+
+subsubsection \<open>Cauchy filter\<close>
+
+definition cauchy_filter :: "'a filter \<Rightarrow> bool" where
+ "cauchy_filter F \<longleftrightarrow> F \<times>\<^sub>F F \<le> uniformity"
+
+definition Cauchy :: "(nat \<Rightarrow> 'a) \<Rightarrow> bool" where
+ Cauchy_uniform: "Cauchy X = cauchy_filter (filtermap X sequentially)"
+
+lemma Cauchy_uniform_iff:
+ "Cauchy X \<longleftrightarrow> (\<forall>P. eventually P uniformity \<longrightarrow> (\<exists>N. \<forall>n\<ge>N. \<forall>m\<ge>N. P (X n, X m)))"
+ unfolding Cauchy_uniform cauchy_filter_def le_filter_def eventually_prod_same
+ eventually_filtermap eventually_sequentially
+proof safe
+ let ?U = "\<lambda>P. eventually P uniformity"
+ { fix P assume "?U P" "\<forall>P. ?U P \<longrightarrow> (\<exists>Q. (\<exists>N. \<forall>n\<ge>N. Q (X n)) \<and> (\<forall>x y. Q x \<longrightarrow> Q y \<longrightarrow> P (x, y)))"
+ then obtain Q N where "\<And>n. n \<ge> N \<Longrightarrow> Q (X n)" "\<And>x y. Q x \<Longrightarrow> Q y \<Longrightarrow> P (x, y)"
+ by metis
+ then show "\<exists>N. \<forall>n\<ge>N. \<forall>m\<ge>N. P (X n, X m)"
+ by blast }
+ { fix P assume "?U P" and P: "\<forall>P. ?U P \<longrightarrow> (\<exists>N. \<forall>n\<ge>N. \<forall>m\<ge>N. P (X n, X m))"
+ then obtain Q where "?U Q" and Q: "\<And>x y z. Q (x, y) \<Longrightarrow> Q (y, z) \<Longrightarrow> P (x, z)"
+ by (auto elim: uniformity_transE)
+ then have "?U (\<lambda>x. Q x \<and> (\<lambda>(x, y). Q (y, x)) x)"
+ unfolding eventually_conj_iff by (simp add: uniformity_sym)
+ from P[rule_format, OF this]
+ obtain N where N: "\<And>n m. n \<ge> N \<Longrightarrow> m \<ge> N \<Longrightarrow> Q (X n, X m) \<and> Q (X m, X n)"
+ by auto
+ show "\<exists>Q. (\<exists>N. \<forall>n\<ge>N. Q (X n)) \<and> (\<forall>x y. Q x \<longrightarrow> Q y \<longrightarrow> P (x, y))"
+ proof (safe intro!: exI[of _ "\<lambda>x. \<forall>n\<ge>N. Q (x, X n) \<and> Q (X n, x)"] exI[of _ N] N)
+ fix x y assume "\<forall>n\<ge>N. Q (x, X n) \<and> Q (X n, x)" "\<forall>n\<ge>N. Q (y, X n) \<and> Q (X n, y)"
+ then have "Q (x, X N)" "Q (X N, y)" by auto
+ then show "P (x, y)"
+ by (rule Q)
+ qed }
+qed
+
+lemma nhds_imp_cauchy_filter:
+ assumes *: "F \<le> nhds x" shows "cauchy_filter F"
+proof -
+ have "F \<times>\<^sub>F F \<le> nhds x \<times>\<^sub>F nhds x"
+ by (intro prod_filter_mono *)
+ also have "\<dots> \<le> uniformity"
+ unfolding le_filter_def eventually_nhds_uniformity eventually_prod_same
+ proof safe
+ fix P assume "eventually P uniformity"
+ then guess Ql by (rule uniformity_transE) note Ql = this
+ moreover note Ql(1)[THEN uniformity_sym]
+ ultimately show "\<exists>Q. eventually (\<lambda>(x', y). x' = x \<longrightarrow> Q y) uniformity \<and> (\<forall>x y. Q x \<longrightarrow> Q y \<longrightarrow> P (x, y))"
+ by (rule_tac exI[of _ "\<lambda>y. Ql (y, x) \<and> Ql (x, y)"]) (fastforce elim: eventually_elim2)
+ qed
+ finally show ?thesis
+ by (simp add: cauchy_filter_def)
+qed
+
+lemma LIMSEQ_imp_Cauchy: "X \<longlonglongrightarrow> x \<Longrightarrow> Cauchy X"
+ unfolding Cauchy_uniform filterlim_def by (intro nhds_imp_cauchy_filter)
+
+lemma Cauchy_subseq_Cauchy: assumes "Cauchy X" "subseq f" shows "Cauchy (X \<circ> f)"
+ unfolding Cauchy_uniform comp_def filtermap_filtermap[symmetric] cauchy_filter_def
+ by (rule order_trans[OF _ \<open>Cauchy X\<close>[unfolded Cauchy_uniform cauchy_filter_def]])
+ (intro prod_filter_mono filtermap_mono filterlim_subseq[OF \<open>subseq f\<close>, unfolded filterlim_def])
+
+lemma convergent_Cauchy: "convergent X \<Longrightarrow> Cauchy X"
+ unfolding convergent_def by (erule exE, erule LIMSEQ_imp_Cauchy)
+
+definition complete :: "'a set \<Rightarrow> bool" where
+ complete_uniform: "complete S \<longleftrightarrow> (\<forall>F \<le> principal S. F \<noteq> bot \<longrightarrow> cauchy_filter F \<longrightarrow> (\<exists>x\<in>S. F \<le> nhds x))"
+
+end
+
+subsubsection \<open>Uniformly continuous functions\<close>
+
+definition uniformly_continuous_on :: "'a set \<Rightarrow> ('a::uniform_space \<Rightarrow> 'b::uniform_space) \<Rightarrow> bool" where
+ uniformly_continuous_on_uniformity: "uniformly_continuous_on s f \<longleftrightarrow>
+ (LIM (x, y) (uniformity_on s). (f x, f y) :> uniformity)"
+
+lemma uniformly_continuous_onD:
+ "uniformly_continuous_on s f \<Longrightarrow> eventually E uniformity
+ \<Longrightarrow> eventually (\<lambda>(x, y). x \<in> s \<longrightarrow> y \<in> s \<longrightarrow> E (f x, f y)) uniformity"
+ by (simp add: uniformly_continuous_on_uniformity filterlim_iff eventually_inf_principal split_beta' mem_Times_iff imp_conjL)
+
+lemma uniformly_continuous_on_const[continuous_intros]: "uniformly_continuous_on s (\<lambda>x. c)"
+ by (auto simp: uniformly_continuous_on_uniformity filterlim_iff uniformity_refl)
+
+lemma uniformly_continuous_on_id[continuous_intros]: "uniformly_continuous_on s (\<lambda>x. x)"
+ by (auto simp: uniformly_continuous_on_uniformity filterlim_def)
+
+lemma uniformly_continuous_on_compose[continuous_intros]:
+ "uniformly_continuous_on s g \<Longrightarrow> uniformly_continuous_on (g`s) f \<Longrightarrow> uniformly_continuous_on s (\<lambda>x. f (g x))"
+ using filterlim_compose[of "\<lambda>(x, y). (f x, f y)" uniformity "uniformity_on (g`s)" "\<lambda>(x, y). (g x, g y)" "uniformity_on s"]
+ by (simp add: split_beta' uniformly_continuous_on_uniformity filterlim_inf filterlim_principal eventually_inf_principal mem_Times_iff)
+
+lemma uniformly_continuous_imp_continuous: assumes f: "uniformly_continuous_on s f" shows "continuous_on s f"
+ by (auto simp: filterlim_iff eventually_at_filter eventually_nhds_uniformity continuous_on_def
+ elim: eventually_mono dest!: uniformly_continuous_onD[OF f])
+
+end