Quelle  metric_def.pvs

%------------------------------------------------------------------------------
% Metric Spaces Definitions
%
%     Author: David Lester, Manchester University
%
% All references are to WA Sutherland "Introduction to Metric and
% Topological Spaces", OUP, 1981
%
%     Version 1.0            17/08/07  Initial Version
%------------------------------------------------------------------------------

metric_def[T:TYPE]: THEORY

BEGIN

  x,y,z: VAR T
  d:     VAR [T,T->nnreal]

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

  metric?(d):bool
    = metric_zero?(d) AND metric_symmetric?(d) AND metric_triangle?(d)

  discrete_metric(x,y):[nnreal] = IF x = y THEN 0 ELSE 1 ENDIF

  metric: TYPE+ = (metric?) CONTAINING discrete_metric

  discrete_metric_is_metric: JUDGEMENT discrete_metric HAS_TYPE metric

END metric_def