|
%------------------------------------------------------------------------------
% Multiplication/division by 2^n
%
% Author: David Lester, Manchester University
%
% Version 1.0 18/2/09 Initial Release Version
%------------------------------------------------------------------------------
shift: THEORY
BEGIN
IMPORTING prelude_aux, appendix, cauchy
x: VAR real
cx: VAR cauchy_real
n,p: VAR nat
div2n(x,n):real = x/2^n
mul2n(x,n):real = x*2^n
cauchy_div2n(cx,n):cauchy_real
= (LAMBDA p: IF p >= n THEN cx (p-n) ELSE round (cx(p)/2^n) ENDIF)
cauchy_mul2n(cx,n):cauchy_real = (LAMBDA p: cx(p+n))
lemma_div2n: LEMMA cauchy_prop(x,cx) =>
cauchy_prop(div2n(x,n),cauchy_div2n(cx,n))
lemma_mul2n: LEMMA cauchy_prop(x,cx) =>
cauchy_prop(mul2n(x,n),cauchy_mul2n(cx,n))
END shift
¤ Dauer der Verarbeitung: 0.0 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.
|
