%------------------------------------------------------------------------------
% Metric Spaces Basics
%
%     Author: David Lester, Manchester University
%
% All references are to WA Sutherland "Introduction to Metric and
% Topological Spaces", OUP, 1981
%
%     Version 1.0            5/12/04  Initial Version DRL
%------------------------------------------------------------------------------

metric_space_def[T:TYPE, d:[T,T -> nnreal]]: THEORY

BEGIN

  x,y:   VAR T
  r:     VAR posreal
  S,X,Y: VAR set[T]

  metric_zero?(S)     :bool = FORALL (x,y:(S)):   d(x,y)  = 0 <=> x = y
  metric_symmetric?(S):bool = FORALL (x,y:(S)):   d(x,y)  = d(y,x)
  metric_triangle?(S) :bool = FORALL (x,y,z:(S)): d(x,z) <= d(x,y) + d(y,z)

  metric_space?(S):bool
    = metric_zero?(S) AND metric_symmetric?(S) AND metric_triangle?(S)

  % The above defines a metric space, and is therefore all that _needs_
  % to be in this file. However, we will be interested in particular
  % specialized spaces, so we take this opportunity to define various
  % predicates on metric spaces that we will need later.

% ball(x,r) is the open set, "centre" x, "radius" r.

  ball(x,r): set[T]     = {y | d(x,y) < r}

  metric_open?(S):   bool = FORALL x: (S(x) <=> EXISTS r: subset?(ball(x,r),S))

  metric_closed?(S): bool = metric_open?(complement(S))

  metric_induced_topology:setofsets[T] = {S | metric_open?(S)}

  metric_adherent?(x,S): bool = FORALL r: nonempty?(intersection(S,ball(x,r)))

  metric_limit?(x,S):    bool = metric_adherent?(x,S) AND NOT member(x,S)

  metric_closure(S): set[T]  = {x:T | metric_adherent?(x,S)}

  dense_in?(X,S): bool = subset?(X,S) AND subset?(S,metric_closure(X))

  IMPORTING sets_aux@countable_props

  separable?(S): bool
    = EXISTS X: subset?(X,S) AND is_countable(X) AND dense_in?(X,S)

  bounded?(S): bool   = EXISTS x,r: subset?(S,ball(x,r))

  epsilon_net?(S,X,r): bool
    = is_finite(X) AND subset?(X,S) AND
      subset?(S,Union(image[T,set[T]](lambda x: ball(x,r),X)))

  totally_bounded?(S): bool = FORALL r: EXISTS X: epsilon_net?(S,X,r)

  u:     VAR sequence[T]
  i,j,n: VAR nat

  metric_converges_to(u,x):bool
    = FORALL r: EXISTS n: FORALL i: i >= n => member(u(i),ball(x,r))

  metric_convergent?(S:set[T],u:sequence[(S)]):bool
    = EXISTS (x:(S)): metric_converges_to(u,x)

  metric_convergent?(u):bool = EXISTS x: metric_converges_to(u,x)

  cauchy?(u):bool = FORALL r: EXISTS n: FORALL i,j: i >= n AND j >= n
                                      => member(u(i),ball(u(j),r))

  metric_complete?(S): bool
    = FORALL (u:sequence[(S)]): cauchy?(u) => metric_convergent?(S,u)

  complete_metric_space?(S):bool = metric_space?(S) AND metric_complete?(S)

% Alternative naming

  accumulation_point?: MACRO [T,set[T]->bool] = metric_limit?

END metric_space_def