|
%------------------------------------------------------------------------------
% 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
¤ Dauer der Verarbeitung: 0.15 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
