Structure metricTheory

signature metricTheory =
sig
  type thm = Thm.thm
  
  (*  Definitions  *)
    val ball : thm
    val bounded_metric_def : thm
    val fsigma_in : thm
    val gdelta_in : thm
    val ismet : thm
    val metric_TY_DEF : thm
    val metric_tybij : thm
    val metrizable_space : thm
    val mr1 : thm
    val mr2 : thm
    val mspace : thm
    val mtop : thm
  
  (*  Theorems  *)
    val BALL_NEIGH : thm
    val BALL_OPEN : thm
    val CLOSED_IMP_FSIGMA_IN : thm
    val CLOSED_IMP_GDELTA_IN : thm
    val EXISTS_METRIZABLE_SPACE : thm
    val FORALL_METRIC_TOPOLOGY : thm
    val FORALL_METRIZABLE_SPACE : thm
    val FORALL_POS_MONO : thm
    val FORALL_POS_MONO_1 : thm
    val FORALL_POS_MONO_1_EQ : thm
    val FORALL_POS_MONO_EQ : thm
    val FORALL_SUC : thm
    val FSIGMA_IN_ASCENDING : thm
    val FSIGMA_IN_DIFF : thm
    val FSIGMA_IN_EMPTY : thm
    val FSIGMA_IN_FSIGMA_SUBTOPOLOGY : thm
    val FSIGMA_IN_GDELTA_IN : thm
    val FSIGMA_IN_INTER : thm
    val FSIGMA_IN_RELATIVE_TO : thm
    val FSIGMA_IN_RELATIVE_TO_TOPSPACE : thm
    val FSIGMA_IN_SUBSET : thm
    val FSIGMA_IN_SUBTOPOLOGY : thm
    val FSIGMA_IN_TOPSPACE : thm
    val FSIGMA_IN_UNION : thm
    val FSIGMA_IN_UNIONS : thm
    val GDELTA_IN_ALT : thm
    val GDELTA_IN_DESCENDING : thm
    val GDELTA_IN_DIFF : thm
    val GDELTA_IN_EMPTY : thm
    val GDELTA_IN_FSIGMA_IN : thm
    val GDELTA_IN_GDELTA_SUBTOPOLOGY : thm
    val GDELTA_IN_INTER : thm
    val GDELTA_IN_INTERS : thm
    val GDELTA_IN_RELATIVE_TO : thm
    val GDELTA_IN_SUBSET : thm
    val GDELTA_IN_SUBTOPOLOGY : thm
    val GDELTA_IN_TOPSPACE : thm
    val GDELTA_IN_UNION : thm
    val IN_MBALL : thm
    val ISMET_R1 : thm
    val ISMET_R2 : thm
    val IS_TOPOLOGY_METRIC_TOPOLOGY : thm
    val MDIST_REFL : thm
    val METRIC_ISMET : thm
    val METRIC_NZ : thm
    val METRIC_POS : thm
    val METRIC_SAME : thm
    val METRIC_SYM : thm
    val METRIC_TRIANGLE : thm
    val METRIC_ZERO : thm
    val METRIZABLE_SPACE_MTOPOLOGY : thm
    val MR1_ADD : thm
    val MR1_ADD_LT : thm
    val MR1_ADD_POS : thm
    val MR1_BETWEEN1 : thm
    val MR1_DEF : thm
    val MR1_LIMPT : thm
    val MR1_SUB : thm
    val MR1_SUB_LE : thm
    val MR1_SUB_LT : thm
    val MR2_DEF : thm
    val MR2_MIRROR : thm
    val MTOP_LIMPT : thm
    val MTOP_OPEN : thm
    val OPEN_IMP_FSIGMA_IN : thm
    val OPEN_IMP_GDELTA_IN : thm
    val OPEN_IN_MTOPOLOGY : thm
    val TOPSPACE_MTOP : thm
    val TOPSPACE_MTOPOLOGY : thm
    val bounded_metric_ismet : thm
    val bounded_metric_lt_1 : thm
    val bounded_metric_thm : thm
    val mball : thm
    val mtop_istopology : thm
    val mtopology : thm
  
  val metric_grammars : type_grammar.grammar * term_grammar.grammar
(*
   [real] Parent theory of "metric"
   
   [topology] Parent theory of "metric"
   
   [ball]  Definition
      
      ⊢ ∀m x e. mball m (x,e) = (λy. dist m (x,y) < e)
   
   [bounded_metric_def]  Definition
      
      ⊢ ∀m. bounded_metric m =
            metric (λ(x,y). dist m (x,y) / (1 + dist m (x,y)))
   
   [fsigma_in]  Definition
      
      ⊢ ∀top. fsigma_in top = countable UNION_OF closed_in top
   
   [gdelta_in]  Definition
      
      ⊢ ∀top.
          gdelta_in top =
          countable INTERSECTION_OF open_in top relative_to topspace top
   
   [ismet]  Definition
      
      ⊢ ∀m. ismet m ⇔
            (∀x y. m (x,y) = 0 ⇔ x = y) ∧
            ∀x y z. m (y,z) ≤ m (x,y) + m (x,z)
   
   [metric_TY_DEF]  Definition
      
      ⊢ ∃rep. TYPE_DEFINITION ismet rep
   
   [metric_tybij]  Definition
      
      ⊢ (∀a. metric (dist a) = a) ∧ ∀r. ismet r ⇔ dist (metric r) = r
   
   [metrizable_space]  Definition
      
      ⊢ ∀top. metrizable_space top ⇔ ∃m. top = mtop m
   
   [mr1]  Definition
      
      ⊢ mr1 = metric (λ(x,y). abs (y − x))
   
   [mr2]  Definition
      
      ⊢ mr2 = metric (λ((x1,x2),y1,y2). sqrt ((x1 − y1)² + (x2 − y2)²))
   
   [mspace]  Definition
      
      ⊢ ∀m. mspace m = topspace (mtop m)
   
   [mtop]  Definition
      
      ⊢ ∀m. mtop m =
            topology
              (λS'. ∀x. S' x ⇒ ∃e. 0 < e ∧ ∀y. dist m (x,y) < e ⇒ S' y)
   
   [BALL_NEIGH]  Theorem
      
      ⊢ ∀m x e. 0 < e ⇒ neigh (mtop m) (mball m (x,e),x)
   
   [BALL_OPEN]  Theorem
      
      ⊢ ∀m x e. 0 < e ⇒ open_in (mtop m) (mball m (x,e))
   
   [CLOSED_IMP_FSIGMA_IN]  Theorem
      
      ⊢ ∀top s. closed_in top s ⇒ fsigma_in top s
   
   [CLOSED_IMP_GDELTA_IN]  Theorem
      
      ⊢ ∀top s. metrizable_space top ∧ closed_in top s ⇒ gdelta_in top s
   
   [EXISTS_METRIZABLE_SPACE]  Theorem
      
      ⊢ ∀P. (∃top. metrizable_space top ∧ P top (topspace top)) ⇔
            ∃m. P (mtop m) (mspace m)
   
   [FORALL_METRIC_TOPOLOGY]  Theorem
      
      ⊢ ∀P. (∀m. P (mtop m) (mspace m)) ⇔
            ∀top. metrizable_space top ⇒ P top (topspace top)
   
   [FORALL_METRIZABLE_SPACE]  Theorem
      
      ⊢ ∀P. (∀top. metrizable_space top ⇒ P top (topspace top)) ⇔
            ∀m. P (mtop m) (mspace m)
   
   [FORALL_POS_MONO]  Theorem
      
      ⊢ ∀P. (∀d e. d < e ∧ P d ⇒ P e) ∧ (∀n. n ≠ 0 ⇒ P (&n)⁻¹) ⇒
            ∀e. 0 < e ⇒ P e
   
   [FORALL_POS_MONO_1]  Theorem
      
      ⊢ ∀P. (∀d e. d < e ∧ P d ⇒ P e) ∧ (∀n. P (&n + 1)⁻¹) ⇒
            ∀e. 0 < e ⇒ P e
   
   [FORALL_POS_MONO_1_EQ]  Theorem
      
      ⊢ ∀P. (∀d e. d < e ∧ P d ⇒ P e) ⇒
            ((∀e. 0 < e ⇒ P e) ⇔ ∀n. P (&n + 1)⁻¹)
   
   [FORALL_POS_MONO_EQ]  Theorem
      
      ⊢ ∀P. (∀d e. d < e ∧ P d ⇒ P e) ⇒
            ((∀e. 0 < e ⇒ P e) ⇔ ∀n. n ≠ 0 ⇒ P (&n)⁻¹)
   
   [FORALL_SUC]  Theorem
      
      ⊢ (∀n. n ≠ 0 ⇒ P n) ⇔ ∀n. P (SUC n)
   
   [FSIGMA_IN_ASCENDING]  Theorem
      
      ⊢ ∀top s.
          fsigma_in top s ⇔
          ∃c. (∀n. closed_in top (c n)) ∧ (∀n. c n ⊆ c (n + 1)) ∧
              BIGUNION {c n | n ∈ 𝕌(:num)} = s
   
   [FSIGMA_IN_DIFF]  Theorem
      
      ⊢ ∀top s t.
          fsigma_in top s ∧ gdelta_in top t ⇒ fsigma_in top (s DIFF t)
   
   [FSIGMA_IN_EMPTY]  Theorem
      
      ⊢ ∀top. fsigma_in top ∅
   
   [FSIGMA_IN_FSIGMA_SUBTOPOLOGY]  Theorem
      
      ⊢ ∀top s t.
          fsigma_in top s ⇒
          (fsigma_in (subtopology top s) t ⇔ fsigma_in top t ∧ t ⊆ s)
   
   [FSIGMA_IN_GDELTA_IN]  Theorem
      
      ⊢ ∀top s.
          fsigma_in top s ⇔
          s ⊆ topspace top ∧ gdelta_in top (topspace top DIFF s)
   
   [FSIGMA_IN_INTER]  Theorem
      
      ⊢ ∀top s t. fsigma_in top s ∧ fsigma_in top t ⇒ fsigma_in top (s ∩ t)
   
   [FSIGMA_IN_RELATIVE_TO]  Theorem
      
      ⊢ ∀top s. fsigma_in top relative_to s = fsigma_in (subtopology top s)
   
   [FSIGMA_IN_RELATIVE_TO_TOPSPACE]  Theorem
      
      ⊢ ∀top. fsigma_in top relative_to topspace top = fsigma_in top
   
   [FSIGMA_IN_SUBSET]  Theorem
      
      ⊢ ∀top s. fsigma_in top s ⇒ s ⊆ topspace top
   
   [FSIGMA_IN_SUBTOPOLOGY]  Theorem
      
      ⊢ ∀top u s.
          fsigma_in (subtopology top u) s ⇔ ∃t. fsigma_in top t ∧ s = t ∩ u
   
   [FSIGMA_IN_TOPSPACE]  Theorem
      
      ⊢ ∀top. fsigma_in top (topspace top)
   
   [FSIGMA_IN_UNION]  Theorem
      
      ⊢ ∀top s t. fsigma_in top s ∧ fsigma_in top t ⇒ fsigma_in top (s ∪ t)
   
   [FSIGMA_IN_UNIONS]  Theorem
      
      ⊢ ∀top t.
          countable t ∧ (∀s. s ∈ t ⇒ fsigma_in top s) ⇒
          fsigma_in top (BIGUNION t)
   
   [GDELTA_IN_ALT]  Theorem
      
      ⊢ ∀top s.
          gdelta_in top s ⇔
          s ⊆ topspace top ∧ (countable INTERSECTION_OF open_in top) s
   
   [GDELTA_IN_DESCENDING]  Theorem
      
      ⊢ ∀top s.
          gdelta_in top s ⇔
          ∃c. (∀n. open_in top (c n)) ∧ (∀n. c (n + 1) ⊆ c n) ∧
              BIGINTER {c n | n ∈ 𝕌(:num)} = s
   
   [GDELTA_IN_DIFF]  Theorem
      
      ⊢ ∀top s t.
          gdelta_in top s ∧ fsigma_in top t ⇒ gdelta_in top (s DIFF t)
   
   [GDELTA_IN_EMPTY]  Theorem
      
      ⊢ ∀top. gdelta_in top ∅
   
   [GDELTA_IN_FSIGMA_IN]  Theorem
      
      ⊢ ∀top s.
          gdelta_in top s ⇔
          s ⊆ topspace top ∧ fsigma_in top (topspace top DIFF s)
   
   [GDELTA_IN_GDELTA_SUBTOPOLOGY]  Theorem
      
      ⊢ ∀top s t.
          gdelta_in top s ⇒
          (gdelta_in (subtopology top s) t ⇔ gdelta_in top t ∧ t ⊆ s)
   
   [GDELTA_IN_INTER]  Theorem
      
      ⊢ ∀top s t. gdelta_in top s ∧ gdelta_in top t ⇒ gdelta_in top (s ∩ t)
   
   [GDELTA_IN_INTERS]  Theorem
      
      ⊢ ∀top t.
          countable t ∧ t ≠ ∅ ∧ (∀s. s ∈ t ⇒ gdelta_in top s) ⇒
          gdelta_in top (BIGINTER t)
   
   [GDELTA_IN_RELATIVE_TO]  Theorem
      
      ⊢ ∀top s. gdelta_in top relative_to s = gdelta_in (subtopology top s)
   
   [GDELTA_IN_SUBSET]  Theorem
      
      ⊢ ∀top s. gdelta_in top s ⇒ s ⊆ topspace top
   
   [GDELTA_IN_SUBTOPOLOGY]  Theorem
      
      ⊢ ∀top u s.
          gdelta_in (subtopology top u) s ⇔ ∃t. gdelta_in top t ∧ s = t ∩ u
   
   [GDELTA_IN_TOPSPACE]  Theorem
      
      ⊢ ∀top. gdelta_in top (topspace top)
   
   [GDELTA_IN_UNION]  Theorem
      
      ⊢ ∀top s t. gdelta_in top s ∧ gdelta_in top t ⇒ gdelta_in top (s ∪ t)
   
   [IN_MBALL]  Theorem
      
      ⊢ ∀m x y r.
          y ∈ mball m (x,r) ⇔
          x ∈ mspace m ∧ y ∈ mspace m ∧ dist m (x,y) < r
   
   [ISMET_R1]  Theorem
      
      ⊢ ismet (λ(x,y). abs (y − x))
   
   [ISMET_R2]  Theorem
      
      ⊢ ismet (λ((x1,x2),y1,y2). sqrt ((x1 − y1)² + (x2 − y2)²))
   
   [IS_TOPOLOGY_METRIC_TOPOLOGY]  Theorem
      
      ⊢ ∀m. istopology
              {u | u ⊆ mspace m ∧ ∀x. x ∈ u ⇒ ∃r. 0 < r ∧ mball m (x,r) ⊆ u}
   
   [MDIST_REFL]  Theorem
      
      ⊢ ∀m x. x ∈ mspace m ⇒ dist m (x,x) = 0
   
   [METRIC_ISMET]  Theorem
      
      ⊢ ∀m. ismet (dist m)
   
   [METRIC_NZ]  Theorem
      
      ⊢ ∀m x y. x ≠ y ⇒ 0 < dist m (x,y)
   
   [METRIC_POS]  Theorem
      
      ⊢ ∀m x y. 0 ≤ dist m (x,y)
   
   [METRIC_SAME]  Theorem
      
      ⊢ ∀m x. dist m (x,x) = 0
   
   [METRIC_SYM]  Theorem
      
      ⊢ ∀m x y. dist m (x,y) = dist m (y,x)
   
   [METRIC_TRIANGLE]  Theorem
      
      ⊢ ∀m x y z. dist m (x,z) ≤ dist m (x,y) + dist m (y,z)
   
   [METRIC_ZERO]  Theorem
      
      ⊢ ∀m x y. dist m (x,y) = 0 ⇔ x = y
   
   [METRIZABLE_SPACE_MTOPOLOGY]  Theorem
      
      ⊢ ∀m. metrizable_space (mtop m)
   
   [MR1_ADD]  Theorem
      
      ⊢ ∀x d. dist mr1 (x,x + d) = abs d
   
   [MR1_ADD_LT]  Theorem
      
      ⊢ ∀x d. 0 < d ⇒ dist mr1 (x,x + d) = d
   
   [MR1_ADD_POS]  Theorem
      
      ⊢ ∀x d. 0 ≤ d ⇒ dist mr1 (x,x + d) = d
   
   [MR1_BETWEEN1]  Theorem
      
      ⊢ ∀x y z. x < z ∧ dist mr1 (x,y) < z − x ⇒ y < z
   
   [MR1_DEF]  Theorem
      
      ⊢ ∀x y. dist mr1 (x,y) = abs (y − x)
   
   [MR1_LIMPT]  Theorem
      
      ⊢ ∀x. limpt (mtop mr1) x 𝕌(:real)
   
   [MR1_SUB]  Theorem
      
      ⊢ ∀x d. dist mr1 (x,x − d) = abs d
   
   [MR1_SUB_LE]  Theorem
      
      ⊢ ∀x d. 0 ≤ d ⇒ dist mr1 (x,x − d) = d
   
   [MR1_SUB_LT]  Theorem
      
      ⊢ ∀x d. 0 < d ⇒ dist mr1 (x,x − d) = d
   
   [MR2_DEF]  Theorem
      
      ⊢ ∀x1 x2 y1 y2.
          dist mr2 ((x1,x2),y1,y2) = sqrt ((x1 − y1)² + (x2 − y2)²)
   
   [MR2_MIRROR]  Theorem
      
      ⊢ ∀x1 x2 y1 y2.
          dist mr2 ((-x1,-x2),-y1,-y2) = dist mr2 ((x1,x2),y1,y2)
   
   [MTOP_LIMPT]  Theorem
      
      ⊢ ∀m x S'.
          limpt (mtop m) x S' ⇔
          ∀e. 0 < e ⇒ ∃y. x ≠ y ∧ S' y ∧ dist m (x,y) < e
   
   [MTOP_OPEN]  Theorem
      
      ⊢ ∀S' m.
          open_in (mtop m) S' ⇔
          ∀x. S' x ⇒ ∃e. 0 < e ∧ ∀y. dist m (x,y) < e ⇒ S' y
   
   [OPEN_IMP_FSIGMA_IN]  Theorem
      
      ⊢ ∀top s. metrizable_space top ∧ open_in top s ⇒ fsigma_in top s
   
   [OPEN_IMP_GDELTA_IN]  Theorem
      
      ⊢ ∀top s. open_in top s ⇒ gdelta_in top s
   
   [OPEN_IN_MTOPOLOGY]  Theorem
      
      ⊢ ∀m u.
          open_in (mtop m) u ⇔
          u ⊆ mspace m ∧ ∀x. x ∈ u ⇒ ∃r. 0 < r ∧ mball m (x,r) ⊆ u
   
   [TOPSPACE_MTOP]  Theorem
      
      ⊢ topspace (mtop m) = 𝕌(:α)
   
   [TOPSPACE_MTOPOLOGY]  Theorem
      
      ⊢ ∀m. topspace (mtop m) = mspace m
   
   [bounded_metric_ismet]  Theorem
      
      ⊢ ∀m. ismet (λ(x,y). dist m (x,y) / (1 + dist m (x,y)))
   
   [bounded_metric_lt_1]  Theorem
      
      ⊢ ∀m x y. dist (bounded_metric m) (x,y) < 1
   
   [bounded_metric_thm]  Theorem
      
      ⊢ ∀m x y.
          dist (bounded_metric m) (x,y) = dist m (x,y) / (1 + dist m (x,y))
   
   [mball]  Theorem
      
      ⊢ ∀m x r.
          mball m (x,r) =
          {y | x ∈ mspace m ∧ y ∈ mspace m ∧ dist m (x,y) < r}
   
   [mtop_istopology]  Theorem
      
      ⊢ ∀m. istopology
              (λS'. ∀x. S' x ⇒ ∃e. 0 < e ∧ ∀y. dist m (x,y) < e ⇒ S' y)
   
   [mtopology]  Theorem
      
      ⊢ ∀m. mtop m =
            topology
              {u | u ⊆ mspace m ∧ ∀x. x ∈ u ⇒ ∃r. 0 < r ∧ mball m (x,r) ⊆ u}
   
   
*)
end

HOL 4, Trindemossen-1