Quelle  complete_product.pvs   Sprache: PVS

%------------------------------------------------------------------------------
% Product of Complete Metric Spaces
%
%     Author: David Lester, Manchester University
%
%     Version 1.0            20/12/07  Initial Version
%------------------------------------------------------------------------------

complete_product[T0,T1:TYPE, (IMPORTING metric_def)
                 d0:metric[T0],d1:metric[T1]]: THEORY

BEGIN

  z0,z1: VAR [T0,T1]

  IMPORTING reals@sqrt,
            metric_space_def[T0,d0],
            metric_space_def[T1,d1],
            metric_space_def,
            metric_def

  d2: MACRO metric[[T0,T1]] =
       (LAMBDA (z0,z1): sqrt(sq(d0(z0`1,z1`1))+sq(d1(z0`2,z1`2))))

  complete_d2: LEMMA metric_complete?(fullset[T0]) AND
                     metric_complete?(fullset[T1]) =>
                     metric_complete?[[T0,T1],d2](fullset[[T0,T1]])

END complete_product