mod_lems: THEORY
%------------------------------------------------------------------------
% Develops useful lemmas about mod
%
%
% 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 mod %% in prelude NOW
i,j,k: VAR int
m: VAR posnat
n,a,b,c,x: VAR nat
jj: VAR nzint
% The following rule characterizes the property that incrementing
% modulo m wraps around the zero point.
mod_0 : LEMMA mod(0,jj) = 0
mod_1 : LEMMA j > 1 IMPLIES mod(1,j) = 1
mod_by1 : LEMMA mod(i,1) = 0
mod_to_rem : LEMMA mod(i,m) = rem(m)(i)
mod_0_divides : LEMMA mod(i,jj) = 0 IFF divides(jj,i)
mod_wrap_around : LEMMA n < m & (c <= m & c >= m-n) =>
mod(n+c, m) = n - (m-c)
mod_wrap2 : LEMMA c < m IMPLIES mod(m+c, m) = c
% Injection-like properties for mod for limited ranges
mod_inj1 : LEMMA x < m AND n < m AND c < m AND
mod(x + n, m) = mod(x + c, m) IMPLIES n = c
mod_inj2 : LEMMA x < m AND n < m AND c < m AND
mod(x - n, m) = mod(x - c, m) IMPLIES n = c
mod_wrap_inj : LEMMA
x < m AND a < m AND b < m AND a > 0
IMPLIES (mod(x + a, m) = mod(x - b, m)) = (a + b = m)
kk, vv: VAR nat
mod_neg_limited : LEMMA 0 <= kk AND kk < m AND vv < m AND
vv - kk < 0 IMPLIES mod(vv - kk,m) = m + vv - kk
mod_int_quot: LEMMA FORALL (k:nat, n:posnat):
integer_pred((k-mod(k,n))/n) AND (k-mod(k,n))/n>=0
floor_div_prod: LEMMA FORALL (n,m:posnat,i:nat):
floor(i / (n*m)) = floor(floor(i / m) / n)
mod_mult_quot: LEMMA FORALL (n,m:posnat,i:nat):
mod(i, n * m) = mod(i, m) + m * mod((i - mod(i, m)) / m, n)
AUTO_REWRITE+ mod_0
AUTO_REWRITE+ mod_1
AUTO_REWRITE+ mod_by1
AUTO_REWRITE+ mod_eq_arg %% mod(j,j) = 0
AUTO_REWRITE+ mod_sum %% mod(i+k*j,j) = mod(i,j)
AUTO_REWRITE+ mod_of_mod %% mod(i + mod(k,m), m) = mod(i+k, m)
END mod_lems
¤ Dauer der Verarbeitung: 0.69 Sekunden
(vorverarbeitet)
¤
|
Laden
Fehler beim Verzeichnis:
in der Quellcodebibliothek suchen
Die farbliche Syntaxdarstellung ist noch experimentell.
|
