Theory Metric_Completion

(*  Author:  Sébastien Gouëzel   sebastien.gouezel@univ-rennes1.fr
    License: BSD
*)

section ‹The metric completion of a metric space›

theory Metric_Completion
  imports Isometries
begin

text ‹Any metric space can be completed, by adding the missing limits of Cauchy sequences.
Formally, there exists an isometric embedding of the space in a complete space, with dense image.
In this paragraph, we construct this metric completion. This is exactly the same construction
as the way in which real numbers are constructed from rational numbers.›

subsection ‹Definition of the metric completion›

quotient_type (overloaded) 'a metric_completion =
  "nat ⇒ ('a::metric_space)" / partial: "λu v. (Cauchy u) ∧ (Cauchy v) ∧ (λn. dist (u n) (v n)) ⇢ 0"
unfolding part_equivp_def proof(auto intro!: ext)
  show "∃x. Cauchy x"
    by (rule exI[of _ "λ_. undefined"]) (simp add: convergent_Cauchy convergent_const)
  fix x y z::"nat ⇒ 'a" assume H: "(λn. dist (x n) (y n)) ⇢ 0"
                                   "(λn. dist (x n) (z n)) ⇢ 0"
  have *: "(λn. dist (x n) (y n) + dist (x n) (z n)) ⇢ 0 + 0"
    by (rule tendsto_add) (auto simp add: H)
  show "(λn. dist (y n) (z n)) ⇢ 0"
    apply (rule tendsto_sandwich[of "λ_. 0" _ _ "λn. dist (x n) (y n) + dist (x n) (z n)"])
    using * by (auto simp add: dist_triangle3)
next
  fix x y z::"nat ⇒ 'a" assume H: "(λn. dist (x n) (y n)) ⇢ 0"
                                   "(λn. dist (y n) (z n)) ⇢ 0"
  have *: "(λn. dist (x n) (y n) + dist (y n) (z n)) ⇢ 0 + 0"
    by (rule tendsto_add) (auto simp add: H)
  show "(λn. dist (x n) (z n)) ⇢ 0"
    apply (rule tendsto_sandwich[of "λ_. 0" _ _ "λn. dist (x n) (y n) + dist (y n) (z n)"])
    using * by (auto simp add: dist_triangle)
next
  fix x y::"nat ⇒ 'a" assume H: "Cauchy x"
    "(λv. Cauchy v ∧ (λn. dist (x n) (v n)) ⇢ 0) = (λv. Cauchy v ∧ (λn. dist (y n) (v n)) ⇢ 0)"
  have "Cauchy x ∧ (λn. dist (x n) (x n)) ⇢ 0" using H by auto
  then have "(λn. dist (y n) (x n))⇢ 0" using H by meson
  moreover have "dist (x n) (y n) = dist (y n) (x n)" for n using dist_commute by auto
  ultimately show "(λn. dist (x n) (y n)) ⇢ 0" by auto
qed

text ‹We have to show that the metric completion is indeed a metric space, that
the original space embeds isometrically into it, and that it is complete. Before we prove these
statements, we start with two simple lemmas that will be needed later on.›

lemma convergent_Cauchy_dist:
  fixes u v::"nat ⇒ ('a::metric_space)"
  assumes "Cauchy u" "Cauchy v"
  shows "convergent (λn. dist (u n) (v n))"
proof (rule real_Cauchy_convergent, intro CauchyI)
  fix e::real assume "e > 0"
  obtain Nu where Nu: "∀n ≥ Nu. ∀m ≥ Nu. dist (u n) (u m) < e/2" using assms(1)
    by (metis ‹0 < e› less_divide_eq_numeral1(1) metric_CauchyD mult_zero_left)
  obtain Nv where Nv: "∀n ≥ Nv. ∀m ≥ Nv. dist (v n) (v m) < e/2" using assms(2)
    by (metis ‹0 < e› less_divide_eq_numeral1(1) metric_CauchyD mult_zero_left)
  define M where "M = max Nu Nv"
  {
    fix n m assume H: "n ≥ M" "m ≥ M"
    have *: "dist (u n) (u m) < e/2" "dist (v n) (v m) < e/2"
      using Nu Nv H unfolding M_def by auto
    have "dist (u m) (v m) - dist (u n) (v n) ≤ dist (u m) (u n) + dist (v n) (v m)"
      by (simp add: algebra_simps) (metis add_le_cancel_left dist_commute dist_triangle2 dist_triangle_le)
    also have "... < e/2 + e/2"
      using * by (simp add: dist_commute)
    finally have A: "dist (u m) (v m) - dist (u n) (v n) < e" by simp

    have "dist (u n) (v n) - dist (u m) (v m) ≤ dist (u m) (u n) + dist (v n) (v m)"
      by (simp add: algebra_simps) (metis add_le_cancel_left dist_commute dist_triangle2 dist_triangle_le)
    also have "... < e/2 + e/2"
      using * by (simp add: dist_commute)
    finally have "dist (u n) (v n) - dist (u m) (v m) < e" by simp
    then have "norm(dist (u m) (v m) - dist (u n) (v n)) < e" using A by auto
  }
  then show "∃M. ∀m ≥ M. ∀n ≥ M. norm (dist (u m) (v m) - dist (u n) (v n)) < e"
    by auto
qed

lemma convergent_add_null:
  fixes u v::"nat ⇒ ('a::real_normed_vector)"
  assumes "convergent u"
          "(λn. v n - u n) ⇢ 0"
  shows "convergent v" "lim v = lim u"
proof -
  have "(λn. u n + (v n - u n)) ⇢ lim u + 0"
    apply (rule tendsto_add) using assms convergent_LIMSEQ_iff by auto
  then have *: "v ⇢ lim u" by auto
  show "convergent v" using * by (simp add: Lim_def convergentI)
  show "lim v = lim u" using * by (simp add: limI)
qed

text ‹Let us now prove that the metric completion is a metric space: the distance between two
Cauchy sequences is the limit of the distances of points in the sequence. The convergence follows
from Lemma~\verb+convergent_Cauchy_dist+ above.›

instantiation metric_completion :: (metric_space) metric_space
begin

lift_definition dist_metric_completion::"('a::metric_space) metric_completion ⇒ 'a metric_completion ⇒ real"
  is "λx y. lim (λn. dist (x n) (y n))"
proof -
  fix x y z t::"nat ⇒ 'a" assume H: "Cauchy x ∧ Cauchy y ∧ (λn. dist (x n) (y n)) ⇢ 0"
                                     "Cauchy z ∧ Cauchy t ∧ (λn. dist (z n) (t n)) ⇢ 0"
  show "lim (λn. dist (x n) (z n)) = lim (λn. dist (y n) (t n))"
  proof (rule convergent_add_null(2))
    show "convergent (λn. dist (y n) (t n))"
      apply (rule convergent_Cauchy_dist) using H by auto

    have a: "(λn. - dist (t n) (z n) - dist (x n) (y n)) ⇢ -0 -0"
      apply (intro tendsto_intros) using H by (auto simp add: dist_commute)
    have b:"(λn. dist (t n) (z n) + dist (x n) (y n)) ⇢ 0 + 0"
      apply (rule tendsto_add) using H by (auto simp add: dist_commute)
    have I: "dist (x n) (z n) ≤ dist (t n) (y n) + (dist (t n) (z n) + dist (x n) (y n))" for n
      using dist_triangle[of "x n" "z n" "y n"] dist_triangle[of "y n" "z n" "t n"]
      by (auto simp add: dist_commute add.commute)
    show "(λn. dist (x n) (z n) - dist (y n) (t n)) ⇢ 0"
      apply (rule tendsto_sandwich[of "λn. -(dist (x n) (y n) + dist (z n) (t n))" _ _ "λn. dist (x n) (y n) + dist (z n) (t n)"])
      apply (auto intro!: always_eventually simp add: algebra_simps dist_commute I)
      apply (meson add_left_mono dist_triangle3 dist_triangle_le)
      using a b by auto
  qed
qed

lemma dist_metric_completion_limit:
  fixes x y::"'a metric_completion"
  shows "(λn. dist (rep_metric_completion x n) (rep_metric_completion y n)) ⇢ dist x y"
proof -
  have C: "Cauchy (rep_metric_completion x)" "Cauchy (rep_metric_completion y)"
    using Quotient3_metric_completion Quotient3_rep_reflp by fastforce+
  show ?thesis
    unfolding dist_metric_completion_def using C apply auto
    using convergent_Cauchy_dist[OF C] convergent_LIMSEQ_iff by force
qed

lemma dist_metric_completion_limit':
  fixes x y::"nat ⇒ 'a"
  assumes "Cauchy x" "Cauchy y"
  shows "(λn. dist (x n) (y n)) ⇢ dist (abs_metric_completion x) (abs_metric_completion y)"
apply (subst dist_metric_completion.abs_eq)
using assms convergent_Cauchy_dist[OF assms] by (auto simp add: convergent_LIMSEQ_iff)

text ‹To define a metric space in the current library of Isabelle/HOL, one should also introduce
a uniformity structure and a topology, as follows (they are prescribed by the distance):›

definition uniformity_metric_completion::"(('a metric_completion) × ('a metric_completion)) filter"
  where "uniformity_metric_completion = (INF e∈{0 <..}. principal {(x, y). dist x y < e})"

definition open_metric_completion :: "'a metric_completion set ⇒ bool"
  where "open_metric_completion U = (∀x∈U. eventually (λ(x', y). x' = x ⟶ y ∈ U) uniformity)"

instance proof
  fix x y::"'a metric_completion"
  have C: "Cauchy (rep_metric_completion x)" "Cauchy (rep_metric_completion y)"
    using Quotient3_metric_completion Quotient3_rep_reflp by fastforce+
  show "(dist x y = 0) = (x = y)"
    apply (subst Quotient3_rel_rep[OF Quotient3_metric_completion, symmetric])
    unfolding dist_metric_completion_def using C apply auto
    using convergent_Cauchy_dist[OF C] convergent_LIMSEQ_iff apply force
    by (simp add: limI)
next
  fix x y z::"'a metric_completion"
  have a: "(λn. dist (rep_metric_completion x n) (rep_metric_completion y n)) ⇢ dist x y"
    using dist_metric_completion_limit by auto
  have b: "(λn. dist (rep_metric_completion x n) (rep_metric_completion z n) + dist (rep_metric_completion y n) (rep_metric_completion z n))
      ⇢ dist x z + dist y z"
    apply (rule tendsto_add) using dist_metric_completion_limit by auto
  show "dist x y ≤ dist x z + dist y z"
    by (rule LIMSEQ_le[OF a b], rule exI[of _ 0], auto simp add: dist_triangle2)
qed (auto simp add: uniformity_metric_completion_def open_metric_completion_def)
end

text ‹Let us now show that the distance thus defined on the metric completion is indeed complete.
This is essentially by design.›

instance metric_completion :: (metric_space) complete_space
proof
  fix X::"nat ⇒ 'a metric_completion" assume "Cauchy X"
  have *: "∃N. ∀n ≥ N. dist (rep_metric_completion (X k) N) (rep_metric_completion (X k) n) < (1/Suc k)" for k
  proof -
    have "Cauchy (rep_metric_completion (X k))"
      using Quotient3_metric_completion Quotient3_rep_reflp by fastforce+
    then have "∃N. ∀m ≥ N. ∀n ≥ N. dist (rep_metric_completion (X k) m) (rep_metric_completion (X k) n) < (1/Suc k)"
      unfolding Cauchy_def by auto
    then show ?thesis by auto
  qed
  have "∃N. ∀k. ∀n ≥ N k. dist (rep_metric_completion (X k) (N k)) (rep_metric_completion (X k) n) < (1/Suc k)"
    apply (rule choice) using * by auto
  then obtain N::"nat ⇒ nat" where
    N: "dist (rep_metric_completion (X k) (N k)) (rep_metric_completion (X k) n) < (1/Suc k)" if "n ≥ N k" for n k
    by auto
  define u where "u = (λk. rep_metric_completion (X k) (N k))"

  have "Cauchy u"
  proof (rule metric_CauchyI)
    fix e::real assume "e > 0"
    obtain K::nat where "K > 4/e" using reals_Archimedean2 by blast
    obtain L::nat where L: "∀m ≥ L. ∀n ≥ L. dist (X m) (X n) < e/2"
      using metric_CauchyD[OF ‹Cauchy X›, of "e/2"] ‹e > 0› by auto
    {
      fix m n assume "m ≥ max K L" "n ≥ max K L"
      then have "dist (X m) (X n) < e/2" using L by auto
      then have "eventually (λp. dist (rep_metric_completion (X m) p) (rep_metric_completion (X n) p) < e/2) sequentially"
        using dist_metric_completion_limit[of "X m" "X n"] by (metis order_tendsto_iff)
      then obtain p where p: "p ≥ max (N m) (N n)" "dist (rep_metric_completion (X m) p) (rep_metric_completion (X n) p) < e/2"
        using eventually_False_sequentially eventually_elim2 eventually_ge_at_top by blast
      have "dist (u m) (rep_metric_completion (X m) p) < 1 / real (Suc m)"
        unfolding u_def using N[of m p] p(1) by auto
      also have "... < e/4"
        using ‹m ≥ max K L› ‹K > 4/e› ‹e > 0› apply (auto simp add: divide_simps algebra_simps)
        by (metis leD le_less_trans less_add_same_cancel2 linear of_nat_le_iff mult_le_cancel_left_pos)
      finally have Im: "dist (u m) (rep_metric_completion (X m) p) < e/4" by simp
      have "dist (u n) (rep_metric_completion (X n) p) < 1 / real (Suc n)"
        unfolding u_def using N[of n p] p(1) by auto
      also have "... < e/4"
        using ‹n ≥ max K L› ‹K > 4/e› ‹e > 0› apply (auto simp add: divide_simps algebra_simps)
        by (metis leD le_less_trans less_add_same_cancel2 linear of_nat_le_iff mult_le_cancel_left_pos)
      finally have In: "dist (u n) (rep_metric_completion (X n) p) < e/4" by simp

      have "dist (u m) (u n) ≤ dist (u m) (rep_metric_completion (X m) p)
          + dist (rep_metric_completion (X m) p) (rep_metric_completion (X n) p) + dist (rep_metric_completion (X n) p) (u n)"
        by (metis add.commute add_left_mono dist_commute dist_triangle_le dist_triangle)
      also have "... < e/4 + e/2 + e/4"
        using In Im p(2) by (simp add: dist_commute)
      also have "... = e" by auto
      finally have "dist (u m) (u n) < e" by auto
    }
    then show "∃M. ∀m ≥ M. ∀n ≥ M. dist (u m) (u n) < e" by meson
  qed
  have *: "(λn. dist (abs_metric_completion u) (X n)) ⇢ 0"
  proof (rule order_tendstoI, auto simp add: less_le_trans eventually_sequentially)
    fix e::real assume "e > 0"
    obtain K::nat where "K > 4/e" using reals_Archimedean2 by blast
    obtain L::nat where L: "∀m ≥ L. ∀n ≥ L. dist (u m) (u n) < e/4"
      using metric_CauchyD[OF ‹Cauchy u›, of "e/4"] ‹e > 0› by auto
    {
      fix n assume n: "n ≥ max K L"
      {
        fix p assume p: "p ≥ max (N n) L"
        have "dist (u n) (rep_metric_completion (X n) p) < 1/(Suc n)"
          unfolding u_def using N p by simp
        also have "... < e/4"
          using ‹n ≥ max K L› ‹K > 4/e› ‹e > 0› apply (auto simp add: divide_simps algebra_simps)
          by (metis leD le_less_trans less_add_same_cancel2 linear of_nat_le_iff mult_le_cancel_left_pos)
        finally have *: "dist (u n) (rep_metric_completion (X n) p) < e/4"
          by fastforce

        have "dist (u p) (rep_metric_completion (X n) p) ≤ dist (u p) (u n) + dist (u n) (rep_metric_completion (X n) p)"
          using dist_triangle by auto
        also have "... < e/4 + e/4" using * L n p by force
        finally have "dist (u p) (rep_metric_completion (X n) p) ≤ e/2" by auto
      }
      then have A: "eventually (λp. dist (u p) (rep_metric_completion (X n) p) ≤ e/2) sequentially"
        using eventually_at_top_linorder by blast
      have B: "(λp. dist (u p) (rep_metric_completion (X n) p)) ⇢ dist (abs_metric_completion u) (X n)"
        using dist_metric_completion_limit'[OF ‹Cauchy u›, of "rep_metric_completion (X n)"]
        unfolding Quotient3_abs_rep[OF Quotient3_metric_completion, of "X n"]
        using Quotient3_rep_reflp[OF Quotient3_metric_completion] by auto
      have "dist (abs_metric_completion u) (X n) ≤ e/2"
        apply (rule LIMSEQ_le_const2[OF B]) using A unfolding eventually_sequentially by auto
      then have "dist (abs_metric_completion u) (X n) < e" using ‹e > 0› by auto
    }
    then show "∃N. ∀n ≥ N. dist (abs_metric_completion u) (X n) < e"
      by blast
  qed
  have "X ⇢ abs_metric_completion u"
    apply (rule tendstoI) using * by (auto simp add: order_tendsto_iff dist_commute)
  then show "convergent X" unfolding convergent_def by auto
qed

subsection ‹Isometric embedding of a space in its metric completion›

text ‹The canonical embedding of a space into its metric completion is obtained by taking
the Cauchy sequence which is constant, equal to the given point. This is indeed an isometric
embedding with dense image, as we prove in the lemmas below.›

definition to_metric_completion::"('a::metric_space) ⇒ 'a metric_completion"
  where "to_metric_completion x = abs_metric_completion (λn. x)"

lemma to_metric_completion_isometry:
  "isometry_on UNIV to_metric_completion"
proof (rule isometry_onI)
  fix x y::'a
  have "(λn. dist (x) (y)) ⇢ dist (to_metric_completion x) (to_metric_completion y)"
    unfolding to_metric_completion_def apply (rule dist_metric_completion_limit')
    unfolding Cauchy_def by auto
  then show "dist (to_metric_completion x) (to_metric_completion y) = dist x y"
    by (simp add: LIMSEQ_const_iff)
qed

lemma to_metric_completion_dense:
  assumes "open U" "U ≠ {}"
  shows "∃x. to_metric_completion x ∈ U"
proof -
  obtain y where "y ∈ U" using ‹U ≠ {}› by auto
  obtain e::real where e: "e > 0" "⋀z. dist z y < e ⟹ z ∈ U"
    using ‹y ∈ U› ‹open U› by (metis open_dist)
  have *: "Cauchy (rep_metric_completion y)"
    using Quotient3_metric_completion Quotient3_rep_reflp by fastforce
  then obtain N where N: "∀n ≥ N. ∀m ≥ N. dist (rep_metric_completion y n) (rep_metric_completion y m) < e/2"
    using ‹e > 0› unfolding Cauchy_def by (meson divide_pos_pos zero_less_numeral)
  define x where "x = rep_metric_completion y N"
  have "(λn. dist x (rep_metric_completion y n)) ⇢ dist (to_metric_completion x) (abs_metric_completion (rep_metric_completion y))"
    unfolding to_metric_completion_def apply (rule dist_metric_completion_limit')
    using * unfolding Cauchy_def by auto
  then have "(λn. dist x (rep_metric_completion y n)) ⇢ dist (to_metric_completion x) y"
    unfolding Quotient3_abs_rep[OF Quotient3_metric_completion] by simp
  moreover have "eventually (λn. dist x (rep_metric_completion y n) ≤ e/2) sequentially"
    unfolding eventually_sequentially x_def apply (rule exI[of _ N]) using N less_imp_le by auto
  ultimately have "dist (to_metric_completion x) y ≤ e/2"
    using LIMSEQ_le_const2 unfolding eventually_sequentially by metis
  then have "to_metric_completion x ∈ U"
    using e by auto
  then show ?thesis by auto
qed

lemma to_metric_completion_dense':
  "closure (range to_metric_completion) = UNIV"
apply (auto simp add: closure_iff_nhds_not_empty) using to_metric_completion_dense by fastforce

text ‹The main feature of the completion is that a uniformly continuous function on the original space can be extended
to a uniformly continuous function on the completion, i.e., it can be written as the composition of
a new function and of the inclusion \verb+to_metric_completion+.›

lemma lift_to_metric_completion:
  fixes f::"('a::metric_space) ⇒ ('b::complete_space)"
  assumes "uniformly_continuous_on UNIV f"
  shows "∃g. (uniformly_continuous_on UNIV g)
            ∧ (f = g o to_metric_completion)
            ∧ (∀x ∈ range to_metric_completion. g x = f (inv to_metric_completion x))"
proof -
  define I::"'a metric_completion ⇒ 'a" where "I = inv to_metric_completion"
  have "uniformly_continuous_on (range to_metric_completion) I"
    using isometry_on_uniformly_continuous[OF isometry_on_inverse(1)[OF to_metric_completion_isometry]] I_def
    by auto
  then have UC: "uniformly_continuous_on (range to_metric_completion) (λx. f (I x))"
    using assms uniformly_continuous_on_compose
    by (metis I_def bij_betw_imp_surj_on bij_betw_inv_into isometry_on_inverse(4) to_metric_completion_isometry)
  obtain g where g: "uniformly_continuous_on (closure(range to_metric_completion)) g"
                    "⋀x. x ∈ range to_metric_completion ⟹ f (I x) = g x"
    using uniformly_continuous_on_extension_on_closure[OF UC] by metis
  have "uniformly_continuous_on UNIV g"
    using to_metric_completion_dense' g(1) by metis
  moreover have "f x = g (to_metric_completion x)" for x
    using g(2) by (metis I_def UNIV_I isometry_on_inverse(2) range_eqI to_metric_completion_isometry)
  moreover have "g x = f (inv to_metric_completion x)" if "x ∈ range to_metric_completion" for x
    using I_def g(2) that by auto
  ultimately show ?thesis unfolding comp_def by auto
qed

text ‹When the function is an isometry, the lifted function is also an isometry (and its range is
the closure of the range of the original function).
This shows that the metric completion is unique, up to isometry:›

lemma lift_to_metric_completion_isometry:
  fixes f::"('a::metric_space) ⇒ ('b::complete_space)"
  assumes "isometry_on UNIV f"
  shows "∃g. isometry_on UNIV g
          ∧ range g = closure(range f)
          ∧ f = g o to_metric_completion
          ∧ (∀x ∈ range to_metric_completion. g x = f (inv to_metric_completion x))"
proof -
  have *: "uniformly_continuous_on UNIV f" using assms isometry_on_uniformly_continuous by force
  obtain g where g: "uniformly_continuous_on UNIV g"
                    "f = g o to_metric_completion"
                    "⋀x. x ∈ range to_metric_completion ⟹ g x = f (inv to_metric_completion x)"
    using lift_to_metric_completion[OF *] by blast
  have *: "isometry_on (range to_metric_completion) g"
    apply (rule isometry_on_cong[OF _ g(3)], rule isometry_on_compose[of _ _ f])
    using assms isometry_on_inverse[OF to_metric_completion_isometry] isometry_on_subset by (auto) (fastforce)
  then have "isometry_on UNIV g"
    unfolding to_metric_completion_dense'[symmetric] apply (rule isometry_on_closure)
    using continuous_on_subset[OF uniformly_continuous_imp_continuous[OF g(1)]] by auto

  have "g`(range to_metric_completion) ⊆ range f"
    using g unfolding comp_def by auto
  moreover have "g`(closure (range to_metric_completion)) ⊆ closure (g`(range to_metric_completion))"
    using uniformly_continuous_imp_continuous[OF g(1)]
    by (meson closed_closure closure_subset continuous_on_subset image_closure_subset top_greatest)
  ultimately have "range g ⊆ closure (range f)"
    unfolding to_metric_completion_dense' by (simp add: g(2) image_comp)

  have "range f ⊆ range g"
    using g(2) by auto
  moreover have "closed (range g)"
    using isometry_on_complete_image[OF ‹isometry_on UNIV g›] by (simp add: complete_eq_closed)
  ultimately have "closure (range f) ⊆ range g"
    by (simp add: closure_minimal)
  then have "range g = closure (range f)"
    using ‹range g ⊆ closure (range f)› by auto
  then show ?thesis using ‹isometry_on UNIV g› g by metis
qed

subsection ‹The metric completion of a second countable space is second countable›

text ‹We want to show that the metric completion of a second countable space is still
second countable. This is most easily expressed using the fact that a metric
space is second countable if and only if there exists a dense countable subset. We prove
the equivalence in the next lemma, and use it then to prove that the metric completion is
still second countable.›

lemma second_countable_iff_dense_countable_subset:
  "(∃B::'a::metric_space set set. countable B ∧ topological_basis B)
    ⟷ (∃A::'a set. countable A ∧ closure A = UNIV)"
proof
  assume "∃B::'a set set. countable B ∧ topological_basis B"
  then obtain B::"'a set set" where "countable B" "topological_basis B" by auto
  define A where "A = (λU. SOME x. x ∈ U)`B"
  have "countable A" unfolding A_def using ‹countable B› by auto
  moreover have "closure A = UNIV"
  proof (auto simp add: closure_approachable)
    fix x::'a and e::real assume "e > 0"
    obtain U where "U ∈ B" "x ∈ U" "U ⊆ ball x e"
      by (rule topological_basisE[OF ‹topological_basis B›, of "ball x e" x], auto simp add: ‹e > 0›)
    define y where "y = (λU. SOME x. x ∈ U) U"
    have "y ∈ U" unfolding y_def using ‹x ∈ U› some_in_eq by fastforce
    then have "dist y x < e"
      using ‹U ⊆ ball x e› by (metis dist_commute mem_ball subset_iff)
    moreover have "y ∈ A" unfolding A_def y_def using ‹U ∈ B› by auto
    ultimately show "∃y∈A. dist y x < e" by auto
  qed
  ultimately show "∃A::'a set. countable A ∧ closure A = UNIV" by auto
next
  assume "∃A::'a set. countable A ∧ closure A = UNIV"
  then obtain A::"'a set" where "countable A" "closure A = UNIV" by auto
  define B where "B = (λ(x, (n::nat)). ball x (1/n))`(A × UNIV)"
  have "countable B" unfolding B_def using ‹countable A› by auto
  moreover have "topological_basis B"
  proof (rule topological_basisI)
    fix x::'a and U assume "x ∈ U" "open U"
    then obtain e where "e > 0" "ball x e ⊆ U"
      using openE by blast
    obtain n::nat where "n > 2/e" using reals_Archimedean2 by auto
    then have "n > 0" using ‹e > 0› not_less by fastforce
    then have "1/n > 0" using zero_less_divide_iff by fastforce
    then obtain y where y: "y ∈ A" "dist x y < 1/n"
      by (metis ‹closure A = UNIV› UNIV_I closure_approachable dist_commute)
    then have "ball y (1/n) ∈ B" unfolding B_def by auto
    moreover have "x ∈ ball y (1/n)" using y(2) by (auto simp add: dist_commute)
    moreover have "ball y (1/n) ⊆ U"
    proof (auto)
      fix z assume z: "dist y z < 1/n"
      have "dist z x ≤ dist z y + dist y x" using dist_triangle by auto
      also have "... < 1/n + 1/n" using z y(2) by (auto simp add: dist_commute)
      also have "... < e"
        using ‹n > 2/e› ‹e > 0› ‹n > 0› by (auto simp add: divide_simps mult.commute)
      finally have "z ∈ ball x e" by (auto simp add: dist_commute)
      then show "z ∈ U" using ‹ball x e ⊆ U› by auto
    qed
    ultimately show "∃V∈B. x ∈ V ∧ V ⊆ U" by metis
  qed (auto simp add: B_def)
  ultimately show "∃B::'a set set. countable B ∧ topological_basis B" by auto
qed

lemma second_countable_metric_dense_subset:
  "∃A::'a::{metric_space, second_countable_topology} set. countable A ∧ closure A = UNIV"
using ex_countable_basis by (auto simp add: second_countable_iff_dense_countable_subset[symmetric])

instance metric_completion::("{metric_space, second_countable_topology}") second_countable_topology
proof
  obtain A::"'a set" where "countable A" "closure A = UNIV"
    using second_countable_metric_dense_subset by auto
  define Ab where "Ab = to_metric_completion`A"
  have "range to_metric_completion ⊆ closure Ab"
    unfolding Ab_def
    by (metis ‹closure A = UNIV› isometry_on_continuous[OF to_metric_completion_isometry] closed_closure closure_subset image_closure_subset)
  then have "closure Ab = UNIV"
    by (metis (no_types) to_metric_completion_dense'[symmetric] ‹range to_metric_completion ⊆ closure Ab› closure_closure closure_mono top.extremum_uniqueI)
  moreover have "countable Ab" unfolding Ab_def using ‹countable A› by auto
  ultimately have "∃Ab::'a metric_completion set. countable Ab ∧ closure Ab = UNIV"
    by auto
  then show "∃B::'a metric_completion set set. countable B ∧ open = generate_topology B"
    using second_countable_iff_dense_countable_subset topological_basis_imp_subbasis by auto
qed

instance metric_completion::("{metric_space, second_countable_topology}") polish_space
by standard

end (*of theory Metric_Completion*)