|
%------------------------------------------------------------------------------
% 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
[ Seitenstruktur0.4Drucken
etwas mehr zur Ethik
]
|
