Quelle  rat.pvs

%------------------------------------------------------------------------------
% Rationals
%
%     Author: David Lester, Manchester University
%
%     Version 1.0            18/2/09   Initial Release Version
%------------------------------------------------------------------------------

rat: THEORY

BEGIN

  IMPORTING cauchy, int, div

  x:   VAR rat
  i:   VAR int
  pn:  VAR posnat
  pns: VAR (nonempty?[posnat])

  denominators(x):(nonempty?[posnat]) = {pn | EXISTS i: x = i/pn}
  denominator(x):posnat = min(denominators(x))

  numerator(x):int      = x*denominator(x)

  cauchy_rat(x):cauchy_real
   = cauchy_div(cauchy_int(numerator(x)),cauchy_int(denominator(x)))

  rat_lemma: LEMMA cauchy_prop(x, cauchy_rat(x))

END rat