Quellcode-Bibliothek rational_props_aux.pvs

%------------------------------------------------------------------------------
% Extensions for prelude library: rational_props
%
%     Author: David Lester, Manchester University & NIA
%
%     Version 1.0            19/08/08   Initial version (DRL)
%
% Extensions to standard prelude library "rational_props"
%
% Note to Sam:
%
% It may be that "min" is declared _after_ rational_props, in which
% case this will not work. Otherwise it ought to be fine.
%
%------------------------------------------------------------------------------

rational_props_aux: THEORY

BEGIN

  p: VAR posnat
  r: VAR rat
  i: VAR int

  denominator(r):posnat = min({p | integer_pred(r*p)}) 
  numerator(r):int      = r*denominator(r)

  rational_def:      LEMMA numerator(r)/denominator(r) = r

  denominator_int:   LEMMA denominator(i) = 1
  numerator_int:     LEMMA numerator(i)   = i

  numerator_is_zero: LEMMA numerator(r) = 0 IFF r = 0
  numerator_pos:     LEMMA numerator(r) > 0 IFF r > 0
  numerator_neg:     LEMMA numerator(r) < 0 IFF r < 0

END rational_props_aux