div: THEORY
%------------------------------------------------------------------------
% Defines natural and integer division (Ada Style)
%
% There is no universally agreed semantics for integer division for a
% negative argument. For a negative argument, division can be defined
% with truncation towards or away from zero. The definition in this
% theory truncates toward zero (i.e. div(-7,3) = -2). This is
% simpler to compute because div(-i,m) = -div(i,m) and is the
% method defined in tha Ada reference manual. The alternate method
% (i.e. truncation away from zero: div(-7,3) = -3) is the approach
% used in most number theory books. This approach has the
% advantage that div(i,m) = the greatest integer less than i/m.
%
% AUTHOR
% ------
%
% Ricky W. Butler email: [email protected]
% Mail Stop 130 fax: (804) 864-4234
% NASA Langley Research Center phone: (804) 864-6198
% Hampton, Virginia 23681-0001
%------------------------------------------------------------------------
BEGIN
IMPORTING floor_div_lems, abs_rews
i,k: VAR int
n: VAR nat
m: VAR posnat
j: VAR nonzero_integer
x: VAR real
div(i,j): integer = sgn(i)*sgn(j)*floor(abs(i)/abs(j))
div_nat: LEMMA div(n,m) = floor(n/m)
div_rew: LEMMA div(n,m) = IF n < m THEN 0 ELSE 1 + div(n-m,m) ENDIF
div_def: LEMMA div(i,j) = IF i/j >= 0 THEN floor(i/j)
ELSE ceiling(i/j)
ENDIF
div_value: LEMMA IF sgn(i) = sgn(j) THEN
i >= k*j AND i < (k+1)*j IMPLIES div(i,j) = k
ELSE
i > (k-1)*j AND i <= k*j IMPLIES div(i,j) = k
ENDIF
div_neg: LEMMA div(-i,j) = -div(i,j)
div_neg_d: LEMMA div(i,-j) = -div(i,j)
% ================== div for special values =============================
div_zero: LEMMA div(0,j) = 0
div_one: LEMMA abs(j) > 1 IMPLIES div(1,j) = 0
div_minus1: LEMMA abs(j) > 1 IMPLIES div(-1, j) = 0
div_eq_arg: LEMMA div(j,j) = 1
div_by_one: LEMMA div(i,1) = i
div_eq_0: LEMMA div(i,j) = 0 IMPLIES abs(i) < abs(j)
div_lt: LEMMA abs(i) < abs(j) IMPLIES div(i,j) = 0
div_lt_nat: LEMMA n < m IMPLIES div(n,m) = 0
div_is_0: LEMMA div(i,j) = 0 IFF abs(i) < abs(j)
div_parity: LEMMA (sgn(i) = sgn(j) AND abs(i) >= abs(j)) IMPLIES
div(i,j) > 0
div_parity_neg: LEMMA (sgn(i) /= sgn(j) AND abs(i) >= abs(j)) IMPLIES
div(i,j) < 0
div_ge_0: LEMMA (sgn(i) = sgn(j) IMPLIES div(i,j) >= 0) AND
(div(i,j) >= 0 IMPLIES
abs(i) < abs(j) OR sgn(i) = sgn(j))
div_le_0: LEMMA (sgn(i) /= sgn(j) IMPLIES div(i,j) <= 0) AND
(div(i,j) <= 0 IMPLIES
abs(i) < abs(j) OR sgn(i) /= sgn(j))
div_smaller: LEMMA m * div(n,m) <= n
div_abs: LEMMA abs(div(i,j)) = div(abs(i),abs(j))
div_max: LEMMA abs(j)*abs(div(i,j)) <= abs(i)
% ================== div over addition =================================
div_multiple: LEMMA div(k*j,j) = k
div_even: LEMMA integer_pred(i/j) IMPLIES i - j*div(i,j) = 0
div_sum: LEMMA IF integer_pred(i/j) OR sgn(i+k*j) = sgn(i) THEN
div(i+k*j,j) = div(i,j) + k
ELSE
div(i+k*j,j) = div(i,j) + k + sgn(i)*sgn(j)
ENDIF
b: VAR nat
div_sum_nat: LEMMA div(n+b*m,m) = div(n,m) + b
nonposint: TYPE = {i: int | i <= 0} CONTAINING -1
negint: TYPE = {i: int | i < 0} CONTAINING -1
npi: VAR nonposint
negi: VAR negint
JUDGEMENT div(n,m) HAS_TYPE nat
JUDGEMENT div(npi,m) HAS_TYPE nonposint
JUDGEMENT div(npi,negi) HAS_TYPE nat
JUDGEMENT div(m,negi) HAS_TYPE nonposint
div_0: LEMMA div(0,j) = 0
AUTO_REWRITE+ div_0
AUTO_REWRITE+ div_eq_arg % LEMMA div(j,j) = 1
AUTO_REWRITE+ div_by_one % LEMMA div(i,1) = i
AUTO_REWRITE+ div_multiple % LEMMA div(k*j,j) = k
AUTO_REWRITE+ div_lt_nat % LEMMA n < m IMPLIES div(n,m) = 0
AUTO_REWRITE+ div_nat % LEMMA div(n,m) = floor(n/m)
END div
¤ Dauer der Verarbeitung: 0.6 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.
|
