add uniform spaces
authorhoelzl
Fri Jan 08 17:40:59 2016 +0100 (2016-01-08)
changeset 6210126c0a70f78a3
parent 62100 7a5754afe170
child 62102 877463945ce9
add uniform spaces
NEWS
src/HOL/Complex.thy
src/HOL/Filter.thy
src/HOL/Library/Extended_Real.thy
src/HOL/Library/Formal_Power_Series.thy
src/HOL/Library/Inner_Product.thy
src/HOL/Library/Product_Vector.thy
src/HOL/Limits.thy
src/HOL/Multivariate_Analysis/Bounded_Continuous_Function.thy
src/HOL/Multivariate_Analysis/Bounded_Linear_Function.thy
src/HOL/Multivariate_Analysis/Cauchy_Integral_Thm.thy
src/HOL/Multivariate_Analysis/Derivative.thy
src/HOL/Multivariate_Analysis/Finite_Cartesian_Product.thy
src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
src/HOL/Probability/Discrete_Topology.thy
src/HOL/Probability/Fin_Map.thy
src/HOL/Product_Type.thy
src/HOL/Real_Vector_Spaces.thy
src/HOL/Topological_Spaces.thy
     1.1 --- a/NEWS	Fri Jan 08 16:37:56 2016 +0100
     1.2 +++ b/NEWS	Fri Jan 08 17:40:59 2016 +0100
     1.3 @@ -606,6 +606,14 @@
     1.4  terms for sup and inf. For example, "sup x (sup y (- x))" simplifies to
     1.5  "top". INCOMPATIBILITY.
     1.6  
     1.7 +* Class uniform_space introduces uniform spaces btw topological spaces
     1.8 +and metric spaces. Minor INCOMPATIBILITY: open_<type>_def needs to be
     1.9 +introduced in the form of an uniformity. Some constants are more
    1.10 +general now, it may be necessary to add type class constraints.
    1.11 +
    1.12 +  open_real_def \<leadsto> open_dist
    1.13 +  open_complex_def \<leadsto> open_dist
    1.14 +
    1.15  * Library/Monad_Syntax: notation uses symbols \<bind> and \<then>. INCOMPATIBILITY.
    1.16  
    1.17  * Library/Multiset:
     2.1 --- a/src/HOL/Complex.thy	Fri Jan 08 16:37:56 2016 +0100
     2.2 +++ b/src/HOL/Complex.thy	Fri Jan 08 17:40:59 2016 +0100
     2.3 @@ -264,8 +264,11 @@
     2.4  definition dist_complex_def:
     2.5    "dist x y = cmod (x - y)"
     2.6  
     2.7 -definition open_complex_def:
     2.8 -  "open (S :: complex set) \<longleftrightarrow> (\<forall>x\<in>S. \<exists>e>0. \<forall>y. dist y x < e \<longrightarrow> y \<in> S)"
     2.9 +definition uniformity_complex_def [code del]:
    2.10 +  "(uniformity :: (complex \<times> complex) filter) = (INF e:{0 <..}. principal {(x, y). dist x y < e})"
    2.11 +
    2.12 +definition open_complex_def [code del]:
    2.13 +  "open (U :: complex set) \<longleftrightarrow> (\<forall>x\<in>U. eventually (\<lambda>(x', y). x' = x \<longrightarrow> y \<in> U) uniformity)"
    2.14  
    2.15  instance proof
    2.16    fix r :: real and x y :: complex and S :: "complex set"
    2.17 @@ -277,7 +280,7 @@
    2.18      by (simp add: norm_complex_def complex_eq_iff power_mult_distrib distrib_left [symmetric] real_sqrt_mult)
    2.19    show "norm (x * y) = norm x * norm y"
    2.20      by (simp add: norm_complex_def complex_eq_iff real_sqrt_mult [symmetric] power2_eq_square algebra_simps)
    2.21 -qed (rule complex_sgn_def dist_complex_def open_complex_def)+
    2.22 +qed (rule complex_sgn_def dist_complex_def open_complex_def uniformity_complex_def)+
    2.23  
    2.24  end
    2.25  
     3.1 --- a/src/HOL/Filter.thy	Fri Jan 08 16:37:56 2016 +0100
     3.2 +++ b/src/HOL/Filter.thy	Fri Jan 08 17:40:59 2016 +0100
     3.3 @@ -529,6 +529,8 @@
     3.4      unfolding le_filter_def eventually_filtermap
     3.5      by (subst (1 2) eventually_INF) auto
     3.6  qed
     3.7 +
     3.8 +
     3.9  subsubsection \<open>Standard filters\<close>
    3.10  
    3.11  definition principal :: "'a set \<Rightarrow> 'a filter" where
    3.12 @@ -743,6 +745,52 @@
    3.13      by (blast intro: finite_subset)
    3.14  qed
    3.15  
    3.16 +subsubsection \<open>Product of filters\<close>
    3.17 +
    3.18 +lemma filtermap_sequentually_ne_bot: "filtermap f sequentially \<noteq> bot"
    3.19 +  by (auto simp add: filter_eq_iff eventually_filtermap eventually_sequentially)
    3.20 +
    3.21 +definition prod_filter :: "'a filter \<Rightarrow> 'b filter \<Rightarrow> ('a \<times> 'b) filter" (infixr "\<times>\<^sub>F" 80) where
    3.22 +  "prod_filter F G =
    3.23 +    (INF (P, Q):{(P, Q). eventually P F \<and> eventually Q G}. principal {(x, y). P x \<and> Q y})"
    3.24 +
    3.25 +lemma eventually_prod_filter: "eventually P (F \<times>\<^sub>F G) \<longleftrightarrow>
    3.26 +  (\<exists>Pf Pg. eventually Pf F \<and> eventually Pg G \<and> (\<forall>x y. Pf x \<longrightarrow> Pg y \<longrightarrow> P (x, y)))"
    3.27 +  unfolding prod_filter_def
    3.28 +proof (subst eventually_INF_base, goal_cases)
    3.29 +  case 2
    3.30 +  moreover have "eventually Pf F \<Longrightarrow> eventually Qf F \<Longrightarrow> eventually Pg G \<Longrightarrow> eventually Qg G \<Longrightarrow>
    3.31 +    \<exists>P Q. eventually P F \<and> eventually Q G \<and>
    3.32 +      Collect P \<times> Collect Q \<subseteq> Collect Pf \<times> Collect Pg \<inter> Collect Qf \<times> Collect Qg" for Pf Pg Qf Qg
    3.33 +    by (intro conjI exI[of _ "inf Pf Qf"] exI[of _ "inf Pg Qg"])
    3.34 +       (auto simp: inf_fun_def eventually_conj)
    3.35 +  ultimately show ?case
    3.36 +    by auto
    3.37 +qed (auto simp: eventually_principal intro: eventually_True)
    3.38 +
    3.39 +lemma prod_filter_mono: "F \<le> F' \<Longrightarrow> G \<le> G' \<Longrightarrow> F \<times>\<^sub>F G \<le> F' \<times>\<^sub>F G'"
    3.40 +  by (auto simp: le_filter_def eventually_prod_filter)
    3.41 +
    3.42 +lemma eventually_prod_same: "eventually P (F \<times>\<^sub>F F) \<longleftrightarrow>
    3.43 +    (\<exists>Q. eventually Q F \<and> (\<forall>x y. Q x \<longrightarrow> Q y \<longrightarrow> P (x, y)))"
    3.44 +  unfolding eventually_prod_filter
    3.45 +  apply safe
    3.46 +  apply (rule_tac x="inf Pf Pg" in exI)
    3.47 +  apply (auto simp: inf_fun_def intro!: eventually_conj)
    3.48 +  done
    3.49 +
    3.50 +lemma eventually_prod_sequentially:
    3.51 +  "eventually P (sequentially \<times>\<^sub>F sequentially) \<longleftrightarrow> (\<exists>N. \<forall>m \<ge> N. \<forall>n \<ge> N. P (n, m))"
    3.52 +  unfolding eventually_prod_same eventually_sequentially by auto
    3.53 +
    3.54 +lemma principal_prod_principal: "principal A \<times>\<^sub>F principal B = principal (A \<times> B)"
    3.55 +  apply (simp add: filter_eq_iff eventually_prod_filter eventually_principal)
    3.56 +  apply safe
    3.57 +  apply blast
    3.58 +  apply (intro conjI exI[of _ "\<lambda>x. x \<in> A"] exI[of _ "\<lambda>x. x \<in> B"])
    3.59 +  apply auto
    3.60 +  done
    3.61 +
    3.62  subsection \<open>Limits\<close>
    3.63  
    3.64  definition filterlim :: "('a \<Rightarrow> 'b) \<Rightarrow> 'b filter \<Rightarrow> 'a filter \<Rightarrow> bool" where
     4.1 --- a/src/HOL/Library/Extended_Real.thy	Fri Jan 08 16:37:56 2016 +0100
     4.2 +++ b/src/HOL/Library/Extended_Real.thy	Fri Jan 08 17:40:59 2016 +0100
     4.3 @@ -2769,7 +2769,7 @@
     4.4    then have "open (ereal -` S)"
     4.5      unfolding open_ereal_def by auto
     4.6    with \<open>x \<in> S\<close> obtain r where "0 < r" and dist: "\<And>y. dist y rx < r \<Longrightarrow> ereal y \<in> S"
     4.7 -    unfolding open_real_def rx by auto
     4.8 +    unfolding open_dist rx by auto
     4.9    then obtain n where
    4.10      upper: "\<And>N. n \<le> N \<Longrightarrow> u N < x + ereal r" and
    4.11      lower: "\<And>N. n \<le> N \<Longrightarrow> x < u N + ereal r"
     5.1 --- a/src/HOL/Library/Formal_Power_Series.thy	Fri Jan 08 16:37:56 2016 +0100
     5.2 +++ b/src/HOL/Library/Formal_Power_Series.thy	Fri Jan 08 17:40:59 2016 +0100
     5.3 @@ -815,13 +815,14 @@
     5.4  instantiation fps :: (comm_ring_1) metric_space
     5.5  begin
     5.6  
     5.7 -definition open_fps_def: "open (S :: 'a fps set) = (\<forall>a \<in> S. \<exists>r. r >0 \<and> ball a r \<subseteq> S)"
     5.8 -
     5.9 +definition uniformity_fps_def [code del]:
    5.10 +  "(uniformity :: ('a fps \<times> 'a fps) filter) = (INF e:{0 <..}. principal {(x, y). dist x y < e})"
    5.11 +
    5.12 +definition open_fps_def' [code del]:
    5.13 +  "open (U :: 'a fps set) \<longleftrightarrow> (\<forall>x\<in>U. eventually (\<lambda>(x', y). x' = x \<longrightarrow> y \<in> U) uniformity)"
    5.14  
    5.15  instance
    5.16  proof
    5.17 -  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"
    5.18 -    by (auto simp add: open_fps_def ball_def subset_eq)
    5.19    show th: "dist a b = 0 \<longleftrightarrow> a = b" for a b :: "'a fps"
    5.20      by (simp add: dist_fps_def split: split_if_asm)
    5.21    then have th'[simp]: "dist a a = 0" for a :: "'a fps" by simp
    5.22 @@ -853,10 +854,12 @@
    5.23      qed
    5.24      thus ?thesis by (auto simp add: not_le[symmetric])
    5.25    qed
    5.26 -qed
    5.27 +qed (rule open_fps_def' uniformity_fps_def)+
    5.28  
    5.29  end
    5.30  
    5.31 +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)"
    5.32 +  unfolding open_dist ball_def subset_eq by simp
    5.33  
    5.34  text \<open>The infinite sums and justification of the notation in textbooks.\<close>
    5.35  
     6.1 --- a/src/HOL/Library/Inner_Product.thy	Fri Jan 08 16:37:56 2016 +0100
     6.2 +++ b/src/HOL/Library/Inner_Product.thy	Fri Jan 08 17:40:59 2016 +0100
     6.3 @@ -11,7 +11,7 @@
     6.4  subsection \<open>Real inner product spaces\<close>
     6.5  
     6.6  text \<open>
     6.7 -  Temporarily relax type constraints for @{term "open"},
     6.8 +  Temporarily relax type constraints for @{term "open"}, @{term "uniformity"},
     6.9    @{term dist}, and @{term norm}.
    6.10  \<close>
    6.11  
    6.12 @@ -22,9 +22,12 @@
    6.13    (@{const_name dist}, SOME @{typ "'a::dist \<Rightarrow> 'a \<Rightarrow> real"})\<close>
    6.14  
    6.15  setup \<open>Sign.add_const_constraint
    6.16 +  (@{const_name uniformity}, SOME @{typ "('a::uniformity \<times> 'a) filter"})\<close>
    6.17 +
    6.18 +setup \<open>Sign.add_const_constraint
    6.19    (@{const_name norm}, SOME @{typ "'a::norm \<Rightarrow> real"})\<close>
    6.20  
    6.21 -class real_inner = real_vector + sgn_div_norm + dist_norm + open_dist +
    6.22 +class real_inner = real_vector + sgn_div_norm + dist_norm + uniformity_dist + open_uniformity +
    6.23    fixes inner :: "'a \<Rightarrow> 'a \<Rightarrow> real"
    6.24    assumes inner_commute: "inner x y = inner y x"
    6.25    and inner_add_left: "inner (x + y) z = inner x z + inner y z"
    6.26 @@ -166,7 +169,7 @@
    6.27    by (metis inner_commute inner_divide_left)
    6.28  
    6.29  text \<open>
    6.30 -  Re-enable constraints for @{term "open"},
    6.31 +  Re-enable constraints for @{term "open"}, @{term "uniformity"},
    6.32    @{term dist}, and @{term norm}.
    6.33  \<close>
    6.34  
    6.35 @@ -174,6 +177,9 @@
    6.36    (@{const_name "open"}, SOME @{typ "'a::topological_space set \<Rightarrow> bool"})\<close>
    6.37  
    6.38  setup \<open>Sign.add_const_constraint
    6.39 +  (@{const_name uniformity}, SOME @{typ "('a::uniform_space \<times> 'a) filter"})\<close>
    6.40 +
    6.41 +setup \<open>Sign.add_const_constraint
    6.42    (@{const_name dist}, SOME @{typ "'a::metric_space \<Rightarrow> 'a \<Rightarrow> real"})\<close>
    6.43  
    6.44  setup \<open>Sign.add_const_constraint
     7.1 --- a/src/HOL/Library/Product_Vector.thy	Fri Jan 08 16:37:56 2016 +0100
     7.2 +++ b/src/HOL/Library/Product_Vector.thy	Fri Jan 08 17:40:59 2016 +0100
     7.3 @@ -229,9 +229,6 @@
     7.4  
     7.5  subsubsection \<open>Separation axioms\<close>
     7.6  
     7.7 -lemma mem_Times_iff: "x \<in> A \<times> B \<longleftrightarrow> fst x \<in> A \<and> snd x \<in> B"
     7.8 -  by (induct x) simp (* TODO: move elsewhere *)
     7.9 -
    7.10  instance prod :: (t0_space, t0_space) t0_space
    7.11  proof
    7.12    fix x y :: "'a \<times> 'b" assume "x \<noteq> y"
    7.13 @@ -264,12 +261,31 @@
    7.14  
    7.15  subsection \<open>Product is a metric space\<close>
    7.16  
    7.17 -instantiation prod :: (metric_space, metric_space) metric_space
    7.18 +(* TODO: Product of uniform spaces and compatibility with metric_spaces! *)
    7.19 +
    7.20 +instantiation prod :: (metric_space, metric_space) dist
    7.21  begin
    7.22  
    7.23  definition dist_prod_def[code del]:
    7.24    "dist x y = sqrt ((dist (fst x) (fst y))\<^sup>2 + (dist (snd x) (snd y))\<^sup>2)"
    7.25  
    7.26 +instance ..
    7.27 +end
    7.28 +
    7.29 +instantiation prod :: (metric_space, metric_space) uniformity_dist
    7.30 +begin
    7.31 +
    7.32 +definition [code del]:
    7.33 +  "(uniformity :: (('a \<times> 'b) \<times> ('a \<times> 'b)) filter) = 
    7.34 +    (INF e:{0 <..}. principal {(x, y). dist x y < e})"
    7.35 +
    7.36 +instance 
    7.37 +  by standard (rule uniformity_prod_def)
    7.38 +end
    7.39 +
    7.40 +instantiation prod :: (metric_space, metric_space) metric_space
    7.41 +begin
    7.42 +
    7.43  lemma dist_Pair_Pair: "dist (a, b) (c, d) = sqrt ((dist a c)\<^sup>2 + (dist b d)\<^sup>2)"
    7.44    unfolding dist_prod_def by simp
    7.45  
    7.46 @@ -292,7 +308,7 @@
    7.47          real_sqrt_le_mono add_mono power_mono dist_triangle2 zero_le_dist)
    7.48  next
    7.49    fix S :: "('a \<times> 'b) set"
    7.50 -  show "open S \<longleftrightarrow> (\<forall>x\<in>S. \<exists>e>0. \<forall>y. dist y x < e \<longrightarrow> y \<in> S)"
    7.51 +  have *: "open S \<longleftrightarrow> (\<forall>x\<in>S. \<exists>e>0. \<forall>y. dist y x < e \<longrightarrow> y \<in> S)"
    7.52    proof
    7.53      assume "open S" show "\<forall>x\<in>S. \<exists>e>0. \<forall>y. dist y x < e \<longrightarrow> y \<in> S"
    7.54      proof
    7.55 @@ -351,6 +367,9 @@
    7.56        ultimately show "\<exists>A B. open A \<and> open B \<and> x \<in> A \<times> B \<and> A \<times> B \<subseteq> S" by fast
    7.57      qed
    7.58    qed
    7.59 +  show "open S = (\<forall>x\<in>S. \<forall>\<^sub>F (x', y) in uniformity. x' = x \<longrightarrow> y \<in> S)"
    7.60 +    unfolding * eventually_uniformity_metric
    7.61 +    by (simp del: split_paired_All add: dist_prod_def dist_commute)
    7.62  qed
    7.63  
    7.64  end
     8.1 --- a/src/HOL/Limits.thy	Fri Jan 08 16:37:56 2016 +0100
     8.2 +++ b/src/HOL/Limits.thy	Fri Jan 08 17:40:59 2016 +0100
     8.3 @@ -1624,16 +1624,6 @@
     8.4    using tendsto_mult [OF tendsto_const LIMSEQ_inverse_real_of_nat_add_minus [of 1]]
     8.5    by auto
     8.6  
     8.7 -lemma lim_1_over_n: "((\<lambda>n. 1 / of_nat n) \<longlongrightarrow> (0::'a::real_normed_field)) sequentially"
     8.8 -proof (subst lim_sequentially, intro allI impI exI)
     8.9 -  fix e :: real assume e: "e > 0"
    8.10 -  fix n :: nat assume n: "n \<ge> nat \<lceil>inverse e + 1\<rceil>"
    8.11 -  have "inverse e < of_nat (nat \<lceil>inverse e + 1\<rceil>)" by linarith
    8.12 -  also note n
    8.13 -  finally show "dist (1 / of_nat n :: 'a) 0 < e" using e
    8.14 -    by (simp add: divide_simps mult.commute norm_conv_dist[symmetric] norm_divide)
    8.15 -qed
    8.16 -
    8.17  lemma lim_inverse_n: "((\<lambda>n. inverse(of_nat n)) \<longlongrightarrow> (0::'a::real_normed_field)) sequentially"
    8.18    using lim_1_over_n by (simp add: inverse_eq_divide)
    8.19  
    8.20 @@ -2236,7 +2226,7 @@
    8.21      then have "x \<in> \<Union>C" using C by auto
    8.22      with C(2) obtain c where "x \<in> c" "open c" "c \<in> C" by auto
    8.23      then obtain e where "0 < e" "{x - e <..< x + e} \<subseteq> c"
    8.24 -      by (auto simp: open_real_def dist_real_def subset_eq Ball_def abs_less_iff)
    8.25 +      by (auto simp: open_dist dist_real_def subset_eq Ball_def abs_less_iff)
    8.26      with \<open>c \<in> C\<close> show ?case
    8.27        by (safe intro!: exI[of _ "e/2"] exI[of _ "{c}"]) auto
    8.28    qed
     9.1 --- a/src/HOL/Multivariate_Analysis/Bounded_Continuous_Function.thy	Fri Jan 08 16:37:56 2016 +0100
     9.2 +++ b/src/HOL/Multivariate_Analysis/Bounded_Continuous_Function.thy	Fri Jan 08 17:40:59 2016 +0100
     9.3 @@ -36,14 +36,18 @@
     9.4    using Rep_bcontfun[of x]
     9.5    by (auto simp: bcontfun_def intro: continuous_on_subset)
     9.6  
     9.7 +(* TODO: Generalize to uniform spaces? *)
     9.8  instantiation bcontfun :: (topological_space, metric_space) metric_space
     9.9  begin
    9.10  
    9.11  definition dist_bcontfun :: "('a, 'b) bcontfun \<Rightarrow> ('a, 'b) bcontfun \<Rightarrow> real"
    9.12    where "dist_bcontfun f g = (SUP x. dist (Rep_bcontfun f x) (Rep_bcontfun g x))"
    9.13  
    9.14 +definition uniformity_bcontfun :: "(('a, 'b) bcontfun \<times> ('a, 'b) bcontfun) filter"
    9.15 +  where "uniformity_bcontfun = (INF e:{0 <..}. principal {(x, y). dist x y < e})"
    9.16 +
    9.17  definition open_bcontfun :: "('a, 'b) bcontfun set \<Rightarrow> bool"
    9.18 -  where "open_bcontfun S = (\<forall>x\<in>S. \<exists>e>0. \<forall>y. dist y x < e \<longrightarrow> y \<in> S)"
    9.19 +  where "open_bcontfun S = (\<forall>x\<in>S. \<forall>\<^sub>F (x', y) in uniformity. x' = x \<longrightarrow> y \<in> S)"
    9.20  
    9.21  lemma dist_bounded:
    9.22    fixes f :: "('a, 'b) bcontfun"
    9.23 @@ -126,7 +130,7 @@
    9.24      finally show "dist (Rep_bcontfun f x) (Rep_bcontfun g x) \<le> dist f h + dist g h"
    9.25        by simp
    9.26    qed
    9.27 -qed (simp add: open_bcontfun_def)
    9.28 +qed (rule open_bcontfun_def uniformity_bcontfun_def)+
    9.29  
    9.30  end
    9.31  
    10.1 --- a/src/HOL/Multivariate_Analysis/Bounded_Linear_Function.thy	Fri Jan 08 16:37:56 2016 +0100
    10.2 +++ b/src/HOL/Multivariate_Analysis/Bounded_Linear_Function.thy	Fri Jan 08 17:40:59 2016 +0100
    10.3 @@ -122,8 +122,11 @@
    10.4  definition dist_blinfun :: "'a \<Rightarrow>\<^sub>L 'b \<Rightarrow> 'a \<Rightarrow>\<^sub>L 'b \<Rightarrow> real"
    10.5    where "dist_blinfun a b = norm (a - b)"
    10.6  
    10.7 +definition [code del]:
    10.8 +  "(uniformity :: (('a \<Rightarrow>\<^sub>L 'b) \<times> ('a \<Rightarrow>\<^sub>L 'b)) filter) = (INF e:{0 <..}. principal {(x, y). dist x y < e})"
    10.9 +
   10.10  definition open_blinfun :: "('a \<Rightarrow>\<^sub>L 'b) set \<Rightarrow> bool"
   10.11 -  where "open_blinfun S \<longleftrightarrow> (\<forall>x\<in>S. \<exists>e>0. \<forall>y. dist y x < e \<longrightarrow> y \<in> S)"
   10.12 +  where [code del]: "open_blinfun S = (\<forall>x\<in>S. \<forall>\<^sub>F (x', y) in uniformity. x' = x \<longrightarrow> y \<in> S)"
   10.13  
   10.14  lift_definition uminus_blinfun :: "'a \<Rightarrow>\<^sub>L 'b \<Rightarrow> 'a \<Rightarrow>\<^sub>L 'b" is "\<lambda>f x. - f x"
   10.15    by (rule bounded_linear_minus)
   10.16 @@ -143,8 +146,8 @@
   10.17  
   10.18  instance
   10.19    apply standard
   10.20 -  unfolding dist_blinfun_def open_blinfun_def sgn_blinfun_def
   10.21 -  apply (transfer, force simp: onorm_triangle onorm_scaleR onorm_eq_0 algebra_simps)+
   10.22 +  unfolding dist_blinfun_def open_blinfun_def sgn_blinfun_def uniformity_blinfun_def
   10.23 +  apply (rule refl | (transfer, force simp: onorm_triangle onorm_scaleR onorm_eq_0 algebra_simps))+
   10.24    done
   10.25  
   10.26  end
    11.1 --- a/src/HOL/Multivariate_Analysis/Cauchy_Integral_Thm.thy	Fri Jan 08 16:37:56 2016 +0100
    11.2 +++ b/src/HOL/Multivariate_Analysis/Cauchy_Integral_Thm.thy	Fri Jan 08 17:40:59 2016 +0100
    11.3 @@ -4106,7 +4106,7 @@
    11.4        done
    11.5    } then
    11.6    show ?thesis
    11.7 -    by (auto simp: Complex.open_complex_def)
    11.8 +    by (auto simp: open_dist)
    11.9  qed
   11.10  
   11.11  subsection\<open>Winding number is zero "outside" a curve, in various senses\<close>
    12.1 --- a/src/HOL/Multivariate_Analysis/Derivative.thy	Fri Jan 08 16:37:56 2016 +0100
    12.2 +++ b/src/HOL/Multivariate_Analysis/Derivative.thy	Fri Jan 08 17:40:59 2016 +0100
    12.3 @@ -874,8 +874,7 @@
    12.4            unfolding eventually_at_topological
    12.5            by metis
    12.6          from \<open>open S\<close> obtain d where d: "\<And>x. dist x y < d \<Longrightarrow> x \<in> S" "d > 0"
    12.7 -          by (force simp: dist_commute open_real_def ball_def
    12.8 -            dest!: bspec[OF _ \<open>y \<in> S\<close>])
    12.9 +          by (force simp: dist_commute open_dist ball_def dest!: bspec[OF _ \<open>y \<in> S\<close>])
   12.10          def d' \<equiv> "min ((y + b)/2) (y + (d/2))"
   12.11          have "d' \<in> A"
   12.12            unfolding A_def
   12.13 @@ -939,8 +938,7 @@
   12.14        where S: "open S" "y \<in> S" "\<And>x. x\<in>S \<Longrightarrow> x \<in> {y..b} \<Longrightarrow> ?le x"
   12.15          by metis
   12.16        from \<open>open S\<close> obtain d where d: "\<And>x. dist x y < d \<Longrightarrow> x \<in> S" "d > 0"
   12.17 -        by (force simp: dist_commute open_real_def ball_def
   12.18 -          dest!: bspec[OF _ \<open>y \<in> S\<close>])
   12.19 +        by (force simp: dist_commute open_dist ball_def dest!: bspec[OF _ \<open>y \<in> S\<close>])
   12.20        def d' \<equiv> "min b (y + (d/2))"
   12.21        have "d' \<in> A"
   12.22          unfolding A_def
    13.1 --- a/src/HOL/Multivariate_Analysis/Finite_Cartesian_Product.thy	Fri Jan 08 16:37:56 2016 +0100
    13.2 +++ b/src/HOL/Multivariate_Analysis/Finite_Cartesian_Product.thy	Fri Jan 08 17:40:59 2016 +0100
    13.3 @@ -142,7 +142,7 @@
    13.4  instantiation vec :: (topological_space, finite) topological_space
    13.5  begin
    13.6  
    13.7 -definition
    13.8 +definition [code del]:
    13.9    "open (S :: ('a ^ 'b) set) \<longleftrightarrow>
   13.10      (\<forall>x\<in>S. \<exists>A. (\<forall>i. open (A i) \<and> x$i \<in> A i) \<and>
   13.11        (\<forall>y. (\<forall>i. y$i \<in> A i) \<longrightarrow> y \<in> S))"
   13.12 @@ -260,13 +260,31 @@
   13.13  
   13.14  
   13.15  subsection \<open>Metric space\<close>
   13.16 +(* TODO: Product of uniform spaces and compatibility with metric_spaces! *)
   13.17  
   13.18 -instantiation vec :: (metric_space, finite) metric_space
   13.19 +instantiation vec :: (metric_space, finite) dist
   13.20  begin
   13.21  
   13.22  definition
   13.23    "dist x y = setL2 (\<lambda>i. dist (x$i) (y$i)) UNIV"
   13.24  
   13.25 +instance ..
   13.26 +end
   13.27 +
   13.28 +instantiation vec :: (metric_space, finite) uniformity_dist
   13.29 +begin
   13.30 +
   13.31 +definition [code del]:
   13.32 +  "(uniformity :: (('a, 'b) vec \<times> ('a, 'b) vec) filter) = 
   13.33 +    (INF e:{0 <..}. principal {(x, y). dist x y < e})"
   13.34 +
   13.35 +instance 
   13.36 +  by standard (rule uniformity_vec_def)
   13.37 +end
   13.38 +
   13.39 +instantiation vec :: (metric_space, finite) metric_space
   13.40 +begin
   13.41 +
   13.42  lemma dist_vec_nth_le: "dist (x $ i) (y $ i) \<le> dist x y"
   13.43    unfolding dist_vec_def by (rule member_le_setL2) simp_all
   13.44  
   13.45 @@ -284,7 +302,7 @@
   13.46      done
   13.47  next
   13.48    fix S :: "('a ^ 'b) set"
   13.49 -  show "open S \<longleftrightarrow> (\<forall>x\<in>S. \<exists>e>0. \<forall>y. dist y x < e \<longrightarrow> y \<in> S)"
   13.50 +  have *: "open S \<longleftrightarrow> (\<forall>x\<in>S. \<exists>e>0. \<forall>y. dist y x < e \<longrightarrow> y \<in> S)"
   13.51    proof
   13.52      assume "open S" show "\<forall>x\<in>S. \<exists>e>0. \<forall>y. dist y x < e \<longrightarrow> y \<in> S"
   13.53      proof
   13.54 @@ -322,6 +340,9 @@
   13.55          (\<forall>y. (\<forall>i. y $ i \<in> A i) \<longrightarrow> y \<in> S)" by metis
   13.56      qed
   13.57    qed
   13.58 +  show "open S = (\<forall>x\<in>S. \<forall>\<^sub>F (x', y) in uniformity. x' = x \<longrightarrow> y \<in> S)"
   13.59 +    unfolding * eventually_uniformity_metric
   13.60 +    by (simp del: split_paired_All add: dist_vec_def dist_commute)
   13.61  qed
   13.62  
   13.63  end
    14.1 --- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Fri Jan 08 16:37:56 2016 +0100
    14.2 +++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Fri Jan 08 17:40:59 2016 +0100
    14.3 @@ -13,7 +13,6 @@
    14.4    "~~/src/HOL/Library/FuncSet"
    14.5    Linear_Algebra
    14.6    Norm_Arith
    14.7 -
    14.8  begin
    14.9  
   14.10  lemma image_affinity_interval:
   14.11 @@ -4573,20 +4572,19 @@
   14.12  
   14.13  subsubsection \<open>Completeness\<close>
   14.14  
   14.15 -definition complete :: "'a::metric_space set \<Rightarrow> bool"
   14.16 -  where "complete s \<longleftrightarrow> (\<forall>f. (\<forall>n. f n \<in> s) \<and> Cauchy f \<longrightarrow> (\<exists>l\<in>s. f \<longlonglongrightarrow> l))"
   14.17 -
   14.18 -lemma completeI:
   14.19 +lemma (in metric_space) completeI:
   14.20    assumes "\<And>f. \<forall>n. f n \<in> s \<Longrightarrow> Cauchy f \<Longrightarrow> \<exists>l\<in>s. f \<longlonglongrightarrow> l"
   14.21    shows "complete s"
   14.22    using assms unfolding complete_def by fast
   14.23  
   14.24 -lemma completeE:
   14.25 +lemma (in metric_space) completeE:
   14.26    assumes "complete s" and "\<forall>n. f n \<in> s" and "Cauchy f"
   14.27    obtains l where "l \<in> s" and "f \<longlonglongrightarrow> l"
   14.28    using assms unfolding complete_def by fast
   14.29  
   14.30 +(* TODO: generalize to uniform spaces *)
   14.31  lemma compact_imp_complete:
   14.32 +  fixes s :: "'a::metric_space set"
   14.33    assumes "compact s"
   14.34    shows "complete s"
   14.35  proof -
   14.36 @@ -4816,6 +4814,7 @@
   14.37  qed
   14.38  
   14.39  lemma complete_imp_closed:
   14.40 +  fixes s :: "'a::metric_space set"
   14.41    assumes "complete s"
   14.42    shows "closed s"
   14.43  proof (unfold closed_sequential_limits, clarify)
   14.44 @@ -4831,6 +4830,7 @@
   14.45  qed
   14.46  
   14.47  lemma complete_inter_closed:
   14.48 +  fixes s :: "'a::metric_space set"
   14.49    assumes "complete s" and "closed t"
   14.50    shows "complete (s \<inter> t)"
   14.51  proof (rule completeI)
   14.52 @@ -4846,6 +4846,7 @@
   14.53  qed
   14.54  
   14.55  lemma complete_closed_subset:
   14.56 +  fixes s :: "'a::metric_space set"
   14.57    assumes "closed s" and "s \<subseteq> t" and "complete t"
   14.58    shows "complete s"
   14.59    using assms complete_inter_closed [of t s] by (simp add: Int_absorb1)
   14.60 @@ -5225,9 +5226,13 @@
   14.61    unfolding continuous_on_def Lim_within
   14.62    by (metis dist_pos_lt dist_self)
   14.63  
   14.64 -definition uniformly_continuous_on :: "'a set \<Rightarrow> ('a::metric_space \<Rightarrow> 'b::metric_space) \<Rightarrow> bool"
   14.65 -  where "uniformly_continuous_on s f \<longleftrightarrow>
   14.66 +lemma uniformly_continuous_on_def:
   14.67 +  fixes f :: "'a::metric_space \<Rightarrow> 'b::metric_space"
   14.68 +  shows "uniformly_continuous_on s f \<longleftrightarrow>
   14.69      (\<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)"
   14.70 +  unfolding uniformly_continuous_on_uniformity
   14.71 +    uniformity_dist filterlim_INF filterlim_principal eventually_inf_principal
   14.72 +  by (force simp: Ball_def uniformity_dist[symmetric] eventually_uniformity_metric)
   14.73  
   14.74  text\<open>Some simple consequential lemmas.\<close>
   14.75  
   14.76 @@ -5242,10 +5247,6 @@
   14.77  using assms
   14.78  by (auto simp: uniformly_continuous_on_def)
   14.79  
   14.80 -lemma uniformly_continuous_imp_continuous:
   14.81 -  "uniformly_continuous_on s f \<Longrightarrow> continuous_on s f"
   14.82 -  unfolding uniformly_continuous_on_def continuous_on_iff by blast
   14.83 -
   14.84  lemma continuous_at_imp_continuous_within:
   14.85    "continuous (at x) f \<Longrightarrow> continuous (at x within s) f"
   14.86    unfolding continuous_within continuous_at using Lim_at_imp_Lim_at_within by auto
   14.87 @@ -5331,8 +5332,7 @@
   14.88  
   14.89  lemma uniformly_continuous_on_sequentially:
   14.90    "uniformly_continuous_on s f \<longleftrightarrow> (\<forall>x y. (\<forall>n. x n \<in> s) \<and> (\<forall>n. y n \<in> s) \<and>
   14.91 -                    ((\<lambda>n. dist (x n) (y n)) \<longlongrightarrow> 0) sequentially
   14.92 -                    \<longrightarrow> ((\<lambda>n. dist (f(x n)) (f(y n))) \<longlongrightarrow> 0) sequentially)" (is "?lhs = ?rhs")
   14.93 +    (\<lambda>n. dist (x n) (y n)) \<longlonglongrightarrow> 0 \<longrightarrow> (\<lambda>n. dist (f(x n)) (f(y n))) \<longlonglongrightarrow> 0)" (is "?lhs = ?rhs")
   14.94  proof
   14.95    assume ?lhs
   14.96    {
   14.97 @@ -5421,7 +5421,7 @@
   14.98    using assms
   14.99    unfolding continuous_within
  14.100    by (force simp add: intro: Lim_transform_within)
  14.101 - 
  14.102 +
  14.103  
  14.104  subsubsection \<open>Structural rules for pointwise continuity\<close>
  14.105  
  14.106 @@ -5462,14 +5462,6 @@
  14.107  
  14.108  subsubsection \<open>Structural rules for uniform continuity\<close>
  14.109  
  14.110 -lemma uniformly_continuous_on_id[continuous_intros]:
  14.111 -  "uniformly_continuous_on s (\<lambda>x. x)"
  14.112 -  unfolding uniformly_continuous_on_def by auto
  14.113 -
  14.114 -lemma uniformly_continuous_on_const[continuous_intros]:
  14.115 -  "uniformly_continuous_on s (\<lambda>x. c)"
  14.116 -  unfolding uniformly_continuous_on_def by simp
  14.117 -
  14.118  lemma uniformly_continuous_on_dist[continuous_intros]:
  14.119    fixes f g :: "'a::metric_space \<Rightarrow> 'b::metric_space"
  14.120    assumes "uniformly_continuous_on s f"
  14.121 @@ -5497,12 +5489,14 @@
  14.122  qed
  14.123  
  14.124  lemma uniformly_continuous_on_norm[continuous_intros]:
  14.125 +  fixes f :: "'a :: metric_space \<Rightarrow> 'b :: real_normed_vector"
  14.126    assumes "uniformly_continuous_on s f"
  14.127    shows "uniformly_continuous_on s (\<lambda>x. norm (f x))"
  14.128    unfolding norm_conv_dist using assms
  14.129    by (intro uniformly_continuous_on_dist uniformly_continuous_on_const)
  14.130  
  14.131  lemma (in bounded_linear) uniformly_continuous_on[continuous_intros]:
  14.132 +  fixes g :: "_::metric_space \<Rightarrow> _"
  14.133    assumes "uniformly_continuous_on s g"
  14.134    shows "uniformly_continuous_on s (\<lambda>x. f (g x))"
  14.135    using assms unfolding uniformly_continuous_on_sequentially
  14.136 @@ -5544,30 +5538,9 @@
  14.137    using assms uniformly_continuous_on_add [of s f "- g"]
  14.138      by (simp add: fun_Compl_def uniformly_continuous_on_minus)
  14.139  
  14.140 -text\<open>Continuity of all kinds is preserved under composition.\<close>
  14.141 -
  14.142  lemmas continuous_at_compose = isCont_o
  14.143  
  14.144 -lemma uniformly_continuous_on_compose[continuous_intros]:
  14.145 -  assumes "uniformly_continuous_on s f"  "uniformly_continuous_on (f ` s) g"
  14.146 -  shows "uniformly_continuous_on s (g \<circ> f)"
  14.147 -proof -
  14.148 -  {
  14.149 -    fix e :: real
  14.150 -    assume "e > 0"
  14.151 -    then obtain d where "d > 0"
  14.152 -      and d: "\<forall>x\<in>f ` s. \<forall>x'\<in>f ` s. dist x' x < d \<longrightarrow> dist (g x') (g x) < e"
  14.153 -      using assms(2) unfolding uniformly_continuous_on_def by auto
  14.154 -    obtain d' where "d'>0" "\<forall>x\<in>s. \<forall>x'\<in>s. dist x' x < d' \<longrightarrow> dist (f x') (f x) < d"
  14.155 -      using \<open>d > 0\<close> using assms(1) unfolding uniformly_continuous_on_def by auto
  14.156 -    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"
  14.157 -      using \<open>d>0\<close> using d by auto
  14.158 -  }
  14.159 -  then show ?thesis
  14.160 -    using assms unfolding uniformly_continuous_on_def by auto
  14.161 -qed
  14.162 -
  14.163 -text\<open>Continuity in terms of open preimages.\<close>
  14.164 +text \<open>Continuity in terms of open preimages.\<close>
  14.165  
  14.166  lemma continuous_at_open:
  14.167    "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)))"
  14.168 @@ -6124,6 +6097,7 @@
  14.169  text \<open>Continuity implies uniform continuity on a compact domain.\<close>
  14.170  
  14.171  lemma compact_uniformly_continuous:
  14.172 +  fixes f :: "'a :: metric_space \<Rightarrow> 'b :: metric_space"
  14.173    assumes f: "continuous_on s f"
  14.174      and s: "compact s"
  14.175    shows "uniformly_continuous_on s f"
    15.1 --- a/src/HOL/Probability/Discrete_Topology.thy	Fri Jan 08 16:37:56 2016 +0100
    15.2 +++ b/src/HOL/Probability/Discrete_Topology.thy	Fri Jan 08 17:40:59 2016 +0100
    15.3 @@ -12,24 +12,24 @@
    15.4  morphisms of_discrete discrete
    15.5  ..
    15.6  
    15.7 -instantiation discrete :: (type) topological_space
    15.8 -begin
    15.9 -
   15.10 -definition open_discrete::"'a discrete set \<Rightarrow> bool"
   15.11 -  where "open_discrete s = True"
   15.12 -
   15.13 -instance proof qed (auto simp: open_discrete_def)
   15.14 -end
   15.15 -
   15.16  instantiation discrete :: (type) metric_space
   15.17  begin
   15.18  
   15.19 -definition dist_discrete::"'a discrete \<Rightarrow> 'a discrete \<Rightarrow> real"
   15.20 +definition dist_discrete :: "'a discrete \<Rightarrow> 'a discrete \<Rightarrow> real"
   15.21    where "dist_discrete n m = (if n = m then 0 else 1)"
   15.22  
   15.23 -instance proof qed (auto simp: open_discrete_def dist_discrete_def intro: exI[where x=1])
   15.24 +definition uniformity_discrete :: "('a discrete \<times> 'a discrete) filter" where
   15.25 +  "(uniformity::('a discrete \<times> 'a discrete) filter) = (INF e:{0 <..}. principal {(x, y). dist x y < e})"
   15.26 +
   15.27 +definition "open_discrete" :: "'a discrete set \<Rightarrow> bool" where
   15.28 +  "(open::'a discrete set \<Rightarrow> bool) U \<longleftrightarrow> (\<forall>x\<in>U. eventually (\<lambda>(x', y). x' = x \<longrightarrow> y \<in> U) uniformity)"
   15.29 +
   15.30 +instance proof qed (auto simp: uniformity_discrete_def open_discrete_def dist_discrete_def intro: exI[where x=1])
   15.31  end
   15.32  
   15.33 +lemma open_discrete: "open (S :: 'a discrete set)"
   15.34 +  unfolding open_dist dist_discrete_def by (auto intro!: exI[of _ "1 / 2"])
   15.35 +
   15.36  instance discrete :: (type) complete_space
   15.37  proof
   15.38    fix X::"nat\<Rightarrow>'a discrete" assume "Cauchy X"
   15.39 @@ -54,7 +54,7 @@
   15.40    have "\<And>S. generate_topology ?B (\<Union>x\<in>S. {x})"
   15.41      by (intro generate_topology_Union) (auto intro: generate_topology.intros)
   15.42    then have "open = generate_topology ?B"
   15.43 -    by (auto intro!: ext simp: open_discrete_def)
   15.44 +    by (auto intro!: ext simp: open_discrete)
   15.45    moreover have "countable ?B" by simp
   15.46    ultimately show "\<exists>B::'a discrete set set. countable B \<and> open = generate_topology B" by blast
   15.47  qed
    16.1 --- a/src/HOL/Probability/Fin_Map.thy	Fri Jan 08 16:37:56 2016 +0100
    16.2 +++ b/src/HOL/Probability/Fin_Map.thy	Fri Jan 08 17:40:59 2016 +0100
    16.3 @@ -150,7 +150,7 @@
    16.4  begin
    16.5  
    16.6  definition open_finmap :: "('a \<Rightarrow>\<^sub>F 'b) set \<Rightarrow> bool" where
    16.7 -  "open_finmap = generate_topology {Pi' a b|a b. \<forall>i\<in>a. open (b i)}"
    16.8 +   [code del]: "open_finmap = generate_topology {Pi' a b|a b. \<forall>i\<in>a. open (b i)}"
    16.9  
   16.10  lemma open_Pi'I: "(\<And>i. i \<in> I \<Longrightarrow> open (A i)) \<Longrightarrow> open (Pi' I A)"
   16.11    by (auto intro: generate_topology.Basis simp: open_finmap_def)
   16.12 @@ -254,12 +254,31 @@
   16.13  
   16.14  subsection \<open>Metric Space of Finite Maps\<close>
   16.15  
   16.16 -instantiation finmap :: (type, metric_space) metric_space
   16.17 +(* TODO: Product of uniform spaces and compatibility with metric_spaces! *)
   16.18 +
   16.19 +instantiation finmap :: (type, metric_space) dist
   16.20  begin
   16.21  
   16.22  definition dist_finmap where
   16.23    "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)"
   16.24  
   16.25 +instance ..
   16.26 +end
   16.27 +
   16.28 +instantiation finmap :: (type, metric_space) uniformity_dist
   16.29 +begin
   16.30 +
   16.31 +definition [code del]:
   16.32 +  "(uniformity :: (('a, 'b) finmap \<times> ('a, 'b) finmap) filter) = 
   16.33 +    (INF e:{0 <..}. principal {(x, y). dist x y < e})"
   16.34 +
   16.35 +instance 
   16.36 +  by standard (rule uniformity_finmap_def)
   16.37 +end
   16.38 +
   16.39 +instantiation finmap :: (type, metric_space) metric_space
   16.40 +begin
   16.41 +
   16.42  lemma finite_proj_image': "x \<notin> domain P \<Longrightarrow> finite ((P)\<^sub>F ` S)"
   16.43    by (rule finite_subset[of _ "proj P ` (domain P \<inter> S \<union> {x})"]) auto
   16.44  
   16.45 @@ -308,7 +327,7 @@
   16.46  instance
   16.47  proof
   16.48    fix S::"('a \<Rightarrow>\<^sub>F 'b) set"
   16.49 -  show "open S = (\<forall>x\<in>S. \<exists>e>0. \<forall>y. dist y x < e \<longrightarrow> y \<in> S)" (is "_ = ?od")
   16.50 +  have *: "open S = (\<forall>x\<in>S. \<exists>e>0. \<forall>y. dist y x < e \<longrightarrow> y \<in> S)" (is "_ = ?od")
   16.51    proof
   16.52      assume "open S"
   16.53      thus ?od
   16.54 @@ -387,6 +406,9 @@
   16.55        by (intro generate_topology.UN) (auto intro: generate_topology.Basis)
   16.56      finally show "open S" .
   16.57    qed
   16.58 +  show "open S = (\<forall>x\<in>S. \<forall>\<^sub>F (x', y) in uniformity. x' = x \<longrightarrow> y \<in> S)"
   16.59 +    unfolding * eventually_uniformity_metric
   16.60 +    by (simp del: split_paired_All add: dist_finmap_def dist_commute eq_commute)
   16.61  next
   16.62    fix P Q::"'a \<Rightarrow>\<^sub>F 'b"
   16.63    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))"
    17.1 --- a/src/HOL/Product_Type.thy	Fri Jan 08 16:37:56 2016 +0100
    17.2 +++ b/src/HOL/Product_Type.thy	Fri Jan 08 17:40:59 2016 +0100
    17.3 @@ -1068,6 +1068,9 @@
    17.4  lemma mem_Sigma_iff [iff]: "((a,b): Sigma A B) = (a:A & b:B(a))"
    17.5    by blast
    17.6  
    17.7 +lemma mem_Times_iff: "x \<in> A \<times> B \<longleftrightarrow> fst x \<in> A \<and> snd x \<in> B"
    17.8 +  by (induct x) simp
    17.9 +
   17.10  lemma Sigma_empty_iff: "(SIGMA i:I. X i) = {} \<longleftrightarrow> (\<forall>i\<in>I. X i = {})"
   17.11    by auto
   17.12  
    18.1 --- a/src/HOL/Real_Vector_Spaces.thy	Fri Jan 08 16:37:56 2016 +0100
    18.2 +++ b/src/HOL/Real_Vector_Spaces.thy	Fri Jan 08 17:40:59 2016 +0100
    18.3 @@ -191,7 +191,7 @@
    18.4    fixes x :: "'a::real_vector"
    18.5    shows "scaleR (-1) x = - x"
    18.6    using scaleR_minus_left [of 1 x] by simp
    18.7 -  
    18.8 +
    18.9  class real_algebra = real_vector + ring +
   18.10    assumes mult_scaleR_left [simp]: "scaleR a x * y = scaleR a (x * y)"
   18.11    and mult_scaleR_right [simp]: "x * scaleR a y = scaleR a (x * y)"
   18.12 @@ -662,10 +662,19 @@
   18.13  class dist_norm = dist + norm + minus +
   18.14    assumes dist_norm: "dist x y = norm (x - y)"
   18.15  
   18.16 -class open_dist = "open" + dist +
   18.17 -  assumes open_dist: "open S \<longleftrightarrow> (\<forall>x\<in>S. \<exists>e>0. \<forall>y. dist y x < e \<longrightarrow> y \<in> S)"
   18.18 +class uniformity_dist = dist + uniformity +
   18.19 +  assumes uniformity_dist: "uniformity = (INF e:{0 <..}. principal {(x, y). dist x y < e})"
   18.20 +begin
   18.21  
   18.22 -class real_normed_vector = real_vector + sgn_div_norm + dist_norm + open_dist +
   18.23 +lemma eventually_uniformity_metric:
   18.24 +  "eventually P uniformity \<longleftrightarrow> (\<exists>e>0. \<forall>x y. dist x y < e \<longrightarrow> P (x, y))"
   18.25 +  unfolding uniformity_dist
   18.26 +  by (subst eventually_INF_base)
   18.27 +     (auto simp: eventually_principal subset_eq intro: bexI[of _ "min _ _"])
   18.28 +
   18.29 +end
   18.30 +
   18.31 +class real_normed_vector = real_vector + sgn_div_norm + dist_norm + uniformity_dist + open_uniformity +
   18.32    assumes norm_eq_zero [simp]: "norm x = 0 \<longleftrightarrow> x = 0"
   18.33    and norm_triangle_ineq: "norm (x + y) \<le> norm x + norm y"
   18.34    and norm_scaleR [simp]: "norm (scaleR a x) = \<bar>a\<bar> * norm x"
   18.35 @@ -686,8 +695,8 @@
   18.36  
   18.37  class real_normed_algebra_1 = real_algebra_1 + real_normed_algebra +
   18.38    assumes norm_one [simp]: "norm 1 = 1"
   18.39 -  
   18.40 -lemma (in real_normed_algebra_1) scaleR_power [simp]: 
   18.41 +
   18.42 +lemma (in real_normed_algebra_1) scaleR_power [simp]:
   18.43    "(scaleR x y) ^ n = scaleR (x^n) (y^n)"
   18.44    by (induction n) (simp_all add: scaleR_one scaleR_scaleR mult_ac)
   18.45  
   18.46 @@ -1010,7 +1019,7 @@
   18.47  
   18.48  subsection \<open>Metric spaces\<close>
   18.49  
   18.50 -class metric_space = open_dist +
   18.51 +class metric_space = uniformity_dist + open_uniformity +
   18.52    assumes dist_eq_0_iff [simp]: "dist x y = 0 \<longleftrightarrow> x = y"
   18.53    assumes dist_triangle2: "dist x y \<le> dist x z + dist y z"
   18.54  begin
   18.55 @@ -1074,26 +1083,23 @@
   18.56    shows "dist y x1 < e / 2 \<Longrightarrow> dist y x2 < e / 2 \<Longrightarrow> dist x1 x2 < e"
   18.57  by (rule dist_triangle_half_l, simp_all add: dist_commute)
   18.58  
   18.59 -subclass topological_space
   18.60 +subclass uniform_space
   18.61  proof
   18.62 -  have "\<exists>e::real. 0 < e"
   18.63 -    by (blast intro: zero_less_one)
   18.64 -  then show "open UNIV"
   18.65 -    unfolding open_dist by simp
   18.66 -next
   18.67 -  fix S T assume "open S" "open T"
   18.68 -  then show "open (S \<inter> T)"
   18.69 -    unfolding open_dist
   18.70 -    apply clarify
   18.71 -    apply (drule (1) bspec)+
   18.72 -    apply (clarify, rename_tac r s)
   18.73 -    apply (rule_tac x="min r s" in exI, simp)
   18.74 -    done
   18.75 -next
   18.76 -  fix K assume "\<forall>S\<in>K. open S" thus "open (\<Union>K)"
   18.77 -    unfolding open_dist by (meson UnionE UnionI) 
   18.78 +  fix E x assume "eventually E uniformity"
   18.79 +  then obtain e where E: "0 < e" "\<And>x y. dist x y < e \<Longrightarrow> E (x, y)"
   18.80 +    unfolding eventually_uniformity_metric by auto
   18.81 +  then show "E (x, x)" "\<forall>\<^sub>F (x, y) in uniformity. E (y, x)"
   18.82 +    unfolding eventually_uniformity_metric by (auto simp: dist_commute)
   18.83 +
   18.84 +  show "\<exists>D. eventually D uniformity \<and> (\<forall>x y z. D (x, y) \<longrightarrow> D (y, z) \<longrightarrow> E (x, z))"
   18.85 +    using E dist_triangle_half_l[where e=e] unfolding eventually_uniformity_metric
   18.86 +    by (intro exI[of _ "\<lambda>(x, y). dist x y < e / 2"] exI[of _ "e/2"] conjI)
   18.87 +       (auto simp: dist_commute)
   18.88  qed
   18.89  
   18.90 +lemma open_dist: "open S \<longleftrightarrow> (\<forall>x\<in>S. \<exists>e>0. \<forall>y. dist y x < e \<longrightarrow> y \<in> S)"
   18.91 +  unfolding open_uniformity eventually_uniformity_metric by (simp add: dist_commute)
   18.92 +
   18.93  lemma open_ball: "open {y. dist x y < d}"
   18.94  proof (unfold open_dist, intro ballI)
   18.95    fix y assume *: "y \<in> {y. dist x y < d}"
   18.96 @@ -1156,8 +1162,11 @@
   18.97  definition dist_real_def:
   18.98    "dist x y = \<bar>x - y\<bar>"
   18.99  
  18.100 +definition uniformity_real_def [code del]:
  18.101 +  "(uniformity :: (real \<times> real) filter) = (INF e:{0 <..}. principal {(x, y). dist x y < e})"
  18.102 +
  18.103  definition open_real_def [code del]:
  18.104 -  "open (S :: real set) \<longleftrightarrow> (\<forall>x\<in>S. \<exists>e>0. \<forall>y. dist y x < e \<longrightarrow> y \<in> S)"
  18.105 +  "open (U :: real set) \<longleftrightarrow> (\<forall>x\<in>U. eventually (\<lambda>(x', y). x' = x \<longrightarrow> y \<in> U) uniformity)"
  18.106  
  18.107  definition real_norm_def [simp]:
  18.108    "norm r = \<bar>r\<bar>"
  18.109 @@ -1165,8 +1174,9 @@
  18.110  instance
  18.111  apply (intro_classes, unfold real_norm_def real_scaleR_def)
  18.112  apply (rule dist_real_def)
  18.113 +apply (simp add: sgn_real_def)
  18.114 +apply (rule uniformity_real_def)
  18.115  apply (rule open_real_def)
  18.116 -apply (simp add: sgn_real_def)
  18.117  apply (rule abs_eq_0)
  18.118  apply (rule abs_triangle_ineq)
  18.119  apply (rule abs_mult)
  18.120 @@ -1188,7 +1198,7 @@
  18.121    proof (rule ext, safe)
  18.122      fix S :: "real set" assume "open S"
  18.123      then obtain f where "\<forall>x\<in>S. 0 < f x \<and> (\<forall>y. dist y x < f x \<longrightarrow> y \<in> S)"
  18.124 -      unfolding open_real_def bchoice_iff ..
  18.125 +      unfolding open_dist bchoice_iff ..
  18.126      then have *: "S = (\<Union>x\<in>S. {x - f x <..} \<inter> {..< x + f x})"
  18.127        by (fastforce simp: dist_real_def)
  18.128      show "generate_topology (range lessThan \<union> range greaterThan) S"
  18.129 @@ -1199,14 +1209,14 @@
  18.130    next
  18.131      fix S :: "real set" assume "generate_topology (range lessThan \<union> range greaterThan) S"
  18.132      moreover have "\<And>a::real. open {..<a}"
  18.133 -      unfolding open_real_def dist_real_def
  18.134 +      unfolding open_dist dist_real_def
  18.135      proof clarify
  18.136        fix x a :: real assume "x < a"
  18.137        hence "0 < a - x \<and> (\<forall>y. \<bar>y - x\<bar> < a - x \<longrightarrow> y \<in> {..<a})" by auto
  18.138        thus "\<exists>e>0. \<forall>y. \<bar>y - x\<bar> < e \<longrightarrow> y \<in> {..<a}" ..
  18.139      qed
  18.140      moreover have "\<And>a::real. open {a <..}"
  18.141 -      unfolding open_real_def dist_real_def
  18.142 +      unfolding open_dist dist_real_def
  18.143      proof clarify
  18.144        fix x a :: real assume "a < x"
  18.145        hence "0 < x - a \<and> (\<forall>y. \<bar>y - x\<bar> < x - a \<longrightarrow> y \<in> {a<..})" by auto
  18.146 @@ -1233,6 +1243,11 @@
  18.147  setup \<open>Sign.add_const_constraint
  18.148    (@{const_name "open"}, SOME @{typ "'a::topological_space set \<Rightarrow> bool"})\<close>
  18.149  
  18.150 +text \<open>Only allow @{term "uniformity"} in class \<open>uniform_space\<close>.\<close>
  18.151 +
  18.152 +setup \<open>Sign.add_const_constraint
  18.153 +  (@{const_name "uniformity"}, SOME @{typ "('a::uniformity \<times> 'a) filter"})\<close>
  18.154 +
  18.155  text \<open>Only allow @{term dist} in class \<open>metric_space\<close>.\<close>
  18.156  
  18.157  setup \<open>Sign.add_const_constraint
  18.158 @@ -1786,10 +1801,22 @@
  18.159  
  18.160  subsection \<open>Cauchy sequences\<close>
  18.161  
  18.162 -definition (in metric_space) Cauchy :: "(nat \<Rightarrow> 'a) \<Rightarrow> bool" where
  18.163 -  "Cauchy X = (\<forall>e>0. \<exists>M. \<forall>m \<ge> M. \<forall>n \<ge> M. dist (X m) (X n) < e)"
  18.164 +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)"
  18.165 +proof -
  18.166 +  have *: "eventually P (INF M. principal {(X m, X n) | n m. m \<ge> M \<and> n \<ge> M}) =
  18.167 +    (\<exists>M. \<forall>m\<ge>M. \<forall>n\<ge>M. P (X m, X n))" for P
  18.168 +  proof (subst eventually_INF_base, goal_cases)
  18.169 +    case (2 a b) then show ?case
  18.170 +      by (intro bexI[of _ "max a b"]) (auto simp: eventually_principal subset_eq)
  18.171 +  qed (auto simp: eventually_principal, blast)
  18.172 +  have "Cauchy X \<longleftrightarrow> (INF M. principal {(X m, X n) | n m. m \<ge> M \<and> n \<ge> M}) \<le> uniformity"
  18.173 +    unfolding Cauchy_uniform_iff le_filter_def * ..
  18.174 +  also have "\<dots> = (\<forall>e>0. \<exists>M. \<forall>m\<ge>M. \<forall>n\<ge>M. dist (X m) (X n) < e)"
  18.175 +    unfolding uniformity_dist le_INF_iff by (auto simp: * le_principal)
  18.176 +  finally show ?thesis .
  18.177 +qed
  18.178  
  18.179 -lemma Cauchy_altdef:
  18.180 +lemma (in metric_space) Cauchy_altdef:
  18.181    "Cauchy f = (\<forall>e>0. \<exists>M. \<forall>m\<ge>M. \<forall>n>m. dist (f m) (f n) < e)"
  18.182  proof
  18.183    assume A: "\<forall>e>0. \<exists>M. \<forall>m\<ge>M. \<forall>n>m. dist (f m) (f n) < e"
  18.184 @@ -1812,18 +1839,18 @@
  18.185    qed
  18.186  qed
  18.187  
  18.188 -lemma metric_CauchyI:
  18.189 +lemma (in metric_space) metric_CauchyI:
  18.190    "(\<And>e. 0 < e \<Longrightarrow> \<exists>M. \<forall>m\<ge>M. \<forall>n\<ge>M. dist (X m) (X n) < e) \<Longrightarrow> Cauchy X"
  18.191    by (simp add: Cauchy_def)
  18.192  
  18.193 -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"
  18.194 +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"
  18.195    unfolding Cauchy_altdef by blast
  18.196  
  18.197 -lemma metric_CauchyD:
  18.198 +lemma (in metric_space) metric_CauchyD:
  18.199    "Cauchy X \<Longrightarrow> 0 < e \<Longrightarrow> \<exists>M. \<forall>m\<ge>M. \<forall>n\<ge>M. dist (X m) (X n) < e"
  18.200    by (simp add: Cauchy_def)
  18.201  
  18.202 -lemma metric_Cauchy_iff2:
  18.203 +lemma (in metric_space) metric_Cauchy_iff2:
  18.204    "Cauchy X = (\<forall>j. (\<exists>M. \<forall>m \<ge> M. \<forall>n \<ge> M. dist (X m) (X n) < inverse(real (Suc j))))"
  18.205  apply (simp add: Cauchy_def, auto)
  18.206  apply (drule reals_Archimedean, safe)
  18.207 @@ -1837,40 +1864,118 @@
  18.208    "Cauchy X = (\<forall>j. (\<exists>M. \<forall>m \<ge> M. \<forall>n \<ge> M. \<bar>X m - X n\<bar> < inverse(real (Suc j))))"
  18.209    unfolding metric_Cauchy_iff2 dist_real_def ..
  18.210  
  18.211 -lemma Cauchy_subseq_Cauchy:
  18.212 -  "\<lbrakk> Cauchy X; subseq f \<rbrakk> \<Longrightarrow> Cauchy (X o f)"
  18.213 -apply (auto simp add: Cauchy_def)
  18.214 -apply (drule_tac x=e in spec, clarify)
  18.215 -apply (rule_tac x=M in exI, clarify)
  18.216 -apply (blast intro: le_trans [OF _ seq_suble] dest!: spec)
  18.217 -done
  18.218 -
  18.219 -theorem LIMSEQ_imp_Cauchy:
  18.220 -  assumes X: "X \<longlonglongrightarrow> a" shows "Cauchy X"
  18.221 -proof (rule metric_CauchyI)
  18.222 -  fix e::real assume "0 < e"
  18.223 -  hence "0 < e/2" by simp
  18.224 -  with X have "\<exists>N. \<forall>n\<ge>N. dist (X n) a < e/2" by (rule metric_LIMSEQ_D)
  18.225 -  then obtain N where N: "\<forall>n\<ge>N. dist (X n) a < e/2" ..
  18.226 -  show "\<exists>N. \<forall>m\<ge>N. \<forall>n\<ge>N. dist (X m) (X n) < e"
  18.227 -  proof (intro exI allI impI)
  18.228 -    fix m assume "N \<le> m"
  18.229 -    hence m: "dist (X m) a < e/2" using N by blast
  18.230 -    fix n assume "N \<le> n"
  18.231 -    hence n: "dist (X n) a < e/2" using N by blast
  18.232 -    have "dist (X m) (X n) \<le> dist (X m) a + dist (X n) a"
  18.233 -      by (rule dist_triangle2)
  18.234 -    also from m n have "\<dots> < e" by simp
  18.235 -    finally show "dist (X m) (X n) < e" .
  18.236 -  qed
  18.237 +lemma lim_1_over_n: "((\<lambda>n. 1 / of_nat n) \<longlongrightarrow> (0::'a::real_normed_field)) sequentially"
  18.238 +proof (subst lim_sequentially, intro allI impI exI)
  18.239 +  fix e :: real assume e: "e > 0"
  18.240 +  fix n :: nat assume n: "n \<ge> nat \<lceil>inverse e + 1\<rceil>"
  18.241 +  have "inverse e < of_nat (nat \<lceil>inverse e + 1\<rceil>)" by linarith
  18.242 +  also note n
  18.243 +  finally show "dist (1 / of_nat n :: 'a) 0 < e" using e
  18.244 +    by (simp add: divide_simps mult.commute norm_conv_dist[symmetric] norm_divide)
  18.245  qed
  18.246  
  18.247 -lemma convergent_Cauchy: "convergent X \<Longrightarrow> Cauchy X"
  18.248 -unfolding convergent_def
  18.249 -by (erule exE, erule LIMSEQ_imp_Cauchy)
  18.250 +lemma (in metric_space) complete_def:
  18.251 +  shows "complete S = (\<forall>f. (\<forall>n. f n \<in> S) \<and> Cauchy f \<longrightarrow> (\<exists>l\<in>S. f \<longlonglongrightarrow> l))"
  18.252 +  unfolding complete_uniform
  18.253 +proof safe
  18.254 +  fix f :: "nat \<Rightarrow> 'a" assume f: "\<forall>n. f n \<in> S" "Cauchy f"
  18.255 +    and *: "\<forall>F\<le>principal S. F \<noteq> bot \<longrightarrow> cauchy_filter F \<longrightarrow> (\<exists>x\<in>S. F \<le> nhds x)"
  18.256 +  then show "\<exists>l\<in>S. f \<longlonglongrightarrow> l"
  18.257 +    unfolding filterlim_def using f
  18.258 +    by (intro *[rule_format])
  18.259 +       (auto simp: filtermap_sequentually_ne_bot le_principal eventually_filtermap Cauchy_uniform)
  18.260 +next
  18.261 +  fix F :: "'a filter" assume "F \<le> principal S" "F \<noteq> bot" "cauchy_filter F"
  18.262 +  assume seq: "\<forall>f. (\<forall>n. f n \<in> S) \<and> Cauchy f \<longrightarrow> (\<exists>l\<in>S. f \<longlonglongrightarrow> l)"
  18.263 +
  18.264 +  from \<open>F \<le> principal S\<close> \<open>cauchy_filter F\<close> have FF_le: "F \<times>\<^sub>F F \<le> uniformity_on S"
  18.265 +    by (simp add: cauchy_filter_def principal_prod_principal[symmetric] prod_filter_mono)
  18.266 +
  18.267 +  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)"
  18.268 +
  18.269 +  { fix \<epsilon> :: real assume "0 < \<epsilon>"
  18.270 +    then have "eventually (\<lambda>(x, y). x \<in> S \<and> y \<in> S \<and> dist x y < \<epsilon>) (uniformity_on S)"
  18.271 +      unfolding eventually_inf_principal eventually_uniformity_metric by auto
  18.272 +    from filter_leD[OF FF_le this] have "\<exists>P. ?P P \<epsilon>"
  18.273 +      unfolding eventually_prod_same by auto }
  18.274 +  note P = this
  18.275 +
  18.276 +  have "\<exists>P. \<forall>n. ?P (P n) (1 / Suc n) \<and> P (Suc n) \<le> P n"
  18.277 +  proof (rule dependent_nat_choice)
  18.278 +    show "\<exists>P. ?P P (1 / Suc 0)"
  18.279 +      using P[of 1] by auto
  18.280 +  next
  18.281 +    fix P n assume "?P P (1/Suc n)"
  18.282 +    moreover obtain Q where "?P Q (1 / Suc (Suc n))"
  18.283 +      using P[of "1/Suc (Suc n)"] by auto
  18.284 +    ultimately show "\<exists>Q. ?P Q (1 / Suc (Suc n)) \<and> Q \<le> P"
  18.285 +      by (intro exI[of _ "\<lambda>x. P x \<and> Q x"]) (auto simp: eventually_conj_iff)
  18.286 +  qed
  18.287 +  then obtain P where P: "\<And>n. eventually (P n) F" "\<And>n x. P n x \<Longrightarrow> x \<in> S"
  18.288 +    "\<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"
  18.289 +    by metis
  18.290 +  have "antimono P"
  18.291 +    using P(4) unfolding decseq_Suc_iff le_fun_def by blast
  18.292 +
  18.293 +  obtain X where X: "\<And>n. P n (X n)"
  18.294 +    using P(1)[THEN eventually_happens'[OF \<open>F \<noteq> bot\<close>]] by metis
  18.295 +  have "Cauchy X"
  18.296 +    unfolding metric_Cauchy_iff2 inverse_eq_divide
  18.297 +  proof (intro exI allI impI)
  18.298 +    fix j m n :: nat assume "j \<le> m" "j \<le> n"
  18.299 +    with \<open>antimono P\<close> X have "P j (X m)" "P j (X n)"
  18.300 +      by (auto simp: antimono_def)
  18.301 +    then show "dist (X m) (X n) < 1 / Suc j"
  18.302 +      by (rule P)
  18.303 +  qed
  18.304 +  moreover have "\<forall>n. X n \<in> S"
  18.305 +    using P(2) X by auto
  18.306 +  ultimately obtain x where "X \<longlonglongrightarrow> x" "x \<in> S"
  18.307 +    using seq by blast
  18.308 +
  18.309 +  show "\<exists>x\<in>S. F \<le> nhds x"
  18.310 +  proof (rule bexI)
  18.311 +    { fix e :: real assume "0 < e"
  18.312 +      then have "(\<lambda>n. 1 / Suc n :: real) \<longlonglongrightarrow> 0 \<and> 0 < e / 2"
  18.313 +        by (subst LIMSEQ_Suc_iff) (auto intro!: lim_1_over_n)
  18.314 +      then have "\<forall>\<^sub>F n in sequentially. dist (X n) x < e / 2 \<and> 1 / Suc n < e / 2"
  18.315 +        using \<open>X \<longlonglongrightarrow> x\<close> unfolding tendsto_iff order_tendsto_iff[where 'a=real] eventually_conj_iff by blast
  18.316 +      then obtain n where "dist x (X n) < e / 2" "1 / Suc n < e / 2"
  18.317 +        by (auto simp: eventually_sequentially dist_commute)
  18.318 +      have "eventually (\<lambda>y. dist y x < e) F"
  18.319 +        using \<open>eventually (P n) F\<close>
  18.320 +      proof eventually_elim
  18.321 +        fix y assume "P n y"
  18.322 +        then have "dist y (X n) < 1 / Suc n"
  18.323 +          by (intro X P)
  18.324 +        also have "\<dots> < e / 2" by fact
  18.325 +        finally show "dist y x < e"
  18.326 +          by (rule dist_triangle_half_l) fact
  18.327 +      qed }
  18.328 +    then show "F \<le> nhds x"
  18.329 +      unfolding nhds_metric le_INF_iff le_principal by auto
  18.330 +  qed fact
  18.331 +qed
  18.332 +
  18.333 +lemma (in metric_space) totally_bounded_metric:
  18.334 +  "totally_bounded S \<longleftrightarrow> (\<forall>e>0. \<exists>k. finite k \<and> S \<subseteq> (\<Union>x\<in>k. {y. dist x y < e}))"
  18.335 +  unfolding totally_bounded_def eventually_uniformity_metric imp_ex
  18.336 +  apply (subst all_comm)
  18.337 +  apply (intro arg_cong[where f=All] ext)
  18.338 +  apply safe
  18.339 +  subgoal for e
  18.340 +    apply (erule allE[of _ "\<lambda>(x, y). dist x y < e"])
  18.341 +    apply auto
  18.342 +    done
  18.343 +  subgoal for e P k
  18.344 +    apply (intro exI[of _ k])
  18.345 +    apply (force simp: subset_eq)
  18.346 +    done
  18.347 +  done
  18.348  
  18.349  subsubsection \<open>Cauchy Sequences are Convergent\<close>
  18.350  
  18.351 +(* TODO: update to uniform_space *)
  18.352  class complete_space = metric_space +
  18.353    assumes Cauchy_convergent: "Cauchy X \<Longrightarrow> convergent X"
  18.354  
    19.1 --- a/src/HOL/Topological_Spaces.thy	Fri Jan 08 16:37:56 2016 +0100
    19.2 +++ b/src/HOL/Topological_Spaces.thy	Fri Jan 08 17:40:59 2016 +0100
    19.3 @@ -11,7 +11,6 @@
    19.4  
    19.5  named_theorems continuous_intros "structural introduction rules for continuity"
    19.6  
    19.7 -
    19.8  subsection \<open>Topological space\<close>
    19.9  
   19.10  class "open" =
   19.11 @@ -693,8 +692,6 @@
   19.12    by (rule tendsto_le [OF F tendsto_const x a])
   19.13  
   19.14  
   19.15 -
   19.16 -
   19.17  subsubsection \<open>Rules about @{const Lim}\<close>
   19.18  
   19.19  lemma tendsto_Lim:
   19.20 @@ -2435,4 +2432,173 @@
   19.21    qed
   19.22  qed (intro cSUP_least \<open>antimono f\<close>[THEN antimonoD] cInf_lower S)
   19.23  
   19.24 +subsection \<open>Uniform spaces\<close>
   19.25 +
   19.26 +class uniformity = 
   19.27 +  fixes uniformity :: "('a \<times> 'a) filter"
   19.28 +begin
   19.29 +
   19.30 +abbreviation uniformity_on :: "'a set \<Rightarrow> ('a \<times> 'a) filter" where
   19.31 +  "uniformity_on s \<equiv> inf uniformity (principal (s\<times>s))"
   19.32 +
   19.33  end
   19.34 +
   19.35 +class open_uniformity = "open" + uniformity +
   19.36 +  assumes open_uniformity: "\<And>U. open U \<longleftrightarrow> (\<forall>x\<in>U. eventually (\<lambda>(x', y). x' = x \<longrightarrow> y \<in> U) uniformity)"
   19.37 +
   19.38 +class uniform_space = open_uniformity +
   19.39 +  assumes uniformity_refl: "eventually E uniformity \<Longrightarrow> E (x, x)"
   19.40 +  assumes uniformity_sym: "eventually E uniformity \<Longrightarrow> eventually (\<lambda>(x, y). E (y, x)) uniformity"
   19.41 +  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))"
   19.42 +begin
   19.43 +
   19.44 +subclass topological_space
   19.45 +  proof qed (force elim: eventually_mono eventually_elim2 simp: split_beta' open_uniformity)+
   19.46 +
   19.47 +lemma uniformity_bot: "uniformity \<noteq> bot"
   19.48 +  using uniformity_refl by auto
   19.49 +
   19.50 +lemma uniformity_trans':
   19.51 +  "eventually E uniformity \<Longrightarrow> eventually (\<lambda>((x, y), (y', z)). y = y' \<longrightarrow> E (x, z)) (uniformity \<times>\<^sub>F uniformity)"
   19.52 +  by (drule uniformity_trans) (auto simp add: eventually_prod_same)
   19.53 +
   19.54 +lemma uniformity_transE:
   19.55 +  assumes E: "eventually E uniformity"
   19.56 +  obtains D where "eventually D uniformity" "\<And>x y z. D (x, y) \<Longrightarrow> D (y, z) \<Longrightarrow> E (x, z)"
   19.57 +  using uniformity_trans[OF E] by auto
   19.58 +
   19.59 +lemma eventually_nhds_uniformity:
   19.60 +  "eventually P (nhds x) \<longleftrightarrow> eventually (\<lambda>(x', y). x' = x \<longrightarrow> P y) uniformity" (is "_ \<longleftrightarrow> ?N P x")
   19.61 +  unfolding eventually_nhds
   19.62 +proof safe
   19.63 +  assume *: "?N P x"
   19.64 +  { fix x assume "?N P x"
   19.65 +    then guess D by (rule uniformity_transE) note D = this
   19.66 +    from D(1) have "?N (?N P) x"
   19.67 +      by eventually_elim (insert D, force elim: eventually_mono split: prod.split) }
   19.68 +  then have "open {x. ?N P x}"
   19.69 +    by (simp add: open_uniformity)
   19.70 +  then show "\<exists>S. open S \<and> x \<in> S \<and> (\<forall>x\<in>S. P x)"
   19.71 +    by (intro exI[of _ "{x. ?N P x}"]) (auto dest: uniformity_refl simp: *)
   19.72 +qed (force simp add: open_uniformity elim: eventually_mono)
   19.73 +
   19.74 +subsubsection \<open>Totally bounded sets\<close>
   19.75 +
   19.76 +definition totally_bounded :: "'a set \<Rightarrow> bool" where
   19.77 +  "totally_bounded S \<longleftrightarrow>
   19.78 +    (\<forall>E. eventually E uniformity \<longrightarrow> (\<exists>X. finite X \<and> (\<forall>s\<in>S. \<exists>x\<in>X. E (x, s))))"
   19.79 +
   19.80 +lemma totally_bounded_empty[iff]: "totally_bounded {}"
   19.81 +  by (auto simp add: totally_bounded_def)
   19.82 +
   19.83 +lemma totally_bounded_subset: "totally_bounded S \<Longrightarrow> T \<subseteq> S \<Longrightarrow> totally_bounded T"
   19.84 +  by (force simp add: totally_bounded_def)
   19.85 +
   19.86 +lemma totally_bounded_Union[intro]: 
   19.87 +  assumes M: "finite M" "\<And>S. S \<in> M \<Longrightarrow> totally_bounded S" shows "totally_bounded (\<Union>M)"
   19.88 +  unfolding totally_bounded_def
   19.89 +proof safe
   19.90 +  fix E assume "eventually E uniformity"
   19.91 +  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))"
   19.92 +    by (metis totally_bounded_def)
   19.93 +  with `finite M` show "\<exists>X. finite X \<and> (\<forall>s\<in>\<Union>M. \<exists>x\<in>X. E (x, s))"
   19.94 +    by (intro exI[of _ "\<Union>S\<in>M. X S"]) force
   19.95 +qed
   19.96 +
   19.97 +subsubsection \<open>Cauchy filter\<close>
   19.98 +
   19.99 +definition cauchy_filter :: "'a filter \<Rightarrow> bool" where
  19.100 +  "cauchy_filter F \<longleftrightarrow> F \<times>\<^sub>F F \<le> uniformity"
  19.101 +
  19.102 +definition Cauchy :: "(nat \<Rightarrow> 'a) \<Rightarrow> bool" where
  19.103 +  Cauchy_uniform: "Cauchy X = cauchy_filter (filtermap X sequentially)"
  19.104 +
  19.105 +lemma Cauchy_uniform_iff:
  19.106 +  "Cauchy X \<longleftrightarrow> (\<forall>P. eventually P uniformity \<longrightarrow> (\<exists>N. \<forall>n\<ge>N. \<forall>m\<ge>N. P (X n, X m)))"
  19.107 +  unfolding Cauchy_uniform cauchy_filter_def le_filter_def eventually_prod_same
  19.108 +    eventually_filtermap eventually_sequentially
  19.109 +proof safe
  19.110 +  let ?U = "\<lambda>P. eventually P uniformity"
  19.111 +  { 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)))"
  19.112 +    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)"
  19.113 +      by metis
  19.114 +    then show "\<exists>N. \<forall>n\<ge>N. \<forall>m\<ge>N. P (X n, X m)"
  19.115 +      by blast }
  19.116 +  { 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))"
  19.117 +    then obtain Q where "?U Q" and Q: "\<And>x y z. Q (x, y) \<Longrightarrow> Q (y, z) \<Longrightarrow> P (x, z)"
  19.118 +      by (auto elim: uniformity_transE)
  19.119 +    then have "?U (\<lambda>x. Q x \<and> (\<lambda>(x, y). Q (y, x)) x)"
  19.120 +      unfolding eventually_conj_iff by (simp add: uniformity_sym)
  19.121 +    from P[rule_format, OF this]
  19.122 +    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)"
  19.123 +      by auto
  19.124 +    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))"
  19.125 +    proof (safe intro!: exI[of _ "\<lambda>x. \<forall>n\<ge>N. Q (x, X n) \<and> Q (X n, x)"] exI[of _ N] N)
  19.126 +      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)"
  19.127 +      then have "Q (x, X N)" "Q (X N, y)" by auto
  19.128 +      then show "P (x, y)"
  19.129 +        by (rule Q)
  19.130 +    qed }
  19.131 +qed
  19.132 +
  19.133 +lemma nhds_imp_cauchy_filter:
  19.134 +  assumes *: "F \<le> nhds x" shows "cauchy_filter F"
  19.135 +proof -
  19.136 +  have "F \<times>\<^sub>F F \<le> nhds x \<times>\<^sub>F nhds x"
  19.137 +    by (intro prod_filter_mono *)
  19.138 +  also have "\<dots> \<le> uniformity"
  19.139 +    unfolding le_filter_def eventually_nhds_uniformity eventually_prod_same
  19.140 +  proof safe
  19.141 +    fix P assume "eventually P uniformity"
  19.142 +    then guess Ql by (rule uniformity_transE) note Ql = this
  19.143 +    moreover note Ql(1)[THEN uniformity_sym]
  19.144 +    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))"
  19.145 +      by (rule_tac exI[of _ "\<lambda>y. Ql (y, x) \<and> Ql (x, y)"]) (fastforce elim: eventually_elim2)
  19.146 +  qed
  19.147 +  finally show ?thesis
  19.148 +    by (simp add: cauchy_filter_def)
  19.149 +qed
  19.150 +
  19.151 +lemma LIMSEQ_imp_Cauchy: "X \<longlonglongrightarrow> x \<Longrightarrow> Cauchy X"
  19.152 +  unfolding Cauchy_uniform filterlim_def by (intro nhds_imp_cauchy_filter)
  19.153 +
  19.154 +lemma Cauchy_subseq_Cauchy: assumes "Cauchy X" "subseq f" shows "Cauchy (X \<circ> f)"
  19.155 +  unfolding Cauchy_uniform comp_def filtermap_filtermap[symmetric] cauchy_filter_def
  19.156 +  by (rule order_trans[OF _ \<open>Cauchy X\<close>[unfolded Cauchy_uniform cauchy_filter_def]])
  19.157 +     (intro prod_filter_mono filtermap_mono filterlim_subseq[OF \<open>subseq f\<close>, unfolded filterlim_def])
  19.158 +
  19.159 +lemma convergent_Cauchy: "convergent X \<Longrightarrow> Cauchy X"
  19.160 +  unfolding convergent_def by (erule exE, erule LIMSEQ_imp_Cauchy)
  19.161 +
  19.162 +definition complete :: "'a set \<Rightarrow> bool" where
  19.163 +  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))"
  19.164 +
  19.165 +end
  19.166 +
  19.167 +subsubsection \<open>Uniformly continuous functions\<close>
  19.168 +
  19.169 +definition uniformly_continuous_on :: "'a set \<Rightarrow> ('a::uniform_space \<Rightarrow> 'b::uniform_space) \<Rightarrow> bool" where
  19.170 +  uniformly_continuous_on_uniformity: "uniformly_continuous_on s f \<longleftrightarrow> 
  19.171 +    (LIM (x, y) (uniformity_on s). (f x, f y) :> uniformity)"
  19.172 +
  19.173 +lemma uniformly_continuous_onD:
  19.174 +  "uniformly_continuous_on s f \<Longrightarrow> eventually E uniformity
  19.175 +    \<Longrightarrow> eventually (\<lambda>(x, y). x \<in> s \<longrightarrow> y \<in> s \<longrightarrow> E (f x, f y)) uniformity"
  19.176 +  by (simp add: uniformly_continuous_on_uniformity filterlim_iff eventually_inf_principal split_beta' mem_Times_iff imp_conjL)
  19.177 +
  19.178 +lemma uniformly_continuous_on_const[continuous_intros]: "uniformly_continuous_on s (\<lambda>x. c)"
  19.179 +  by (auto simp: uniformly_continuous_on_uniformity filterlim_iff uniformity_refl)
  19.180 +
  19.181 +lemma uniformly_continuous_on_id[continuous_intros]: "uniformly_continuous_on s (\<lambda>x. x)"
  19.182 +  by (auto simp: uniformly_continuous_on_uniformity filterlim_def)
  19.183 +
  19.184 +lemma uniformly_continuous_on_compose[continuous_intros]:
  19.185 +  "uniformly_continuous_on s g \<Longrightarrow> uniformly_continuous_on (g`s) f \<Longrightarrow> uniformly_continuous_on s (\<lambda>x. f (g x))"
  19.186 +  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"]
  19.187 +  by (simp add: split_beta' uniformly_continuous_on_uniformity filterlim_inf filterlim_principal eventually_inf_principal mem_Times_iff)
  19.188 +
  19.189 +lemma uniformly_continuous_imp_continuous: assumes f: "uniformly_continuous_on s f" shows "continuous_on s f"
  19.190 +  by (auto simp: filterlim_iff eventually_at_filter eventually_nhds_uniformity continuous_on_def
  19.191 +           elim: eventually_mono dest!: uniformly_continuous_onD[OF f])
  19.192 +
  19.193 +end