|
%------------------------------------------------------------------------------
% 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
¤ Dauer der Verarbeitung: 0.17 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.
|
