Quellcode-Bibliothek
© Kompilation durch diese Firma
[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]
Datei:
tmod.pvs
Sprache: Unknown
tmod: THEORY
%------------------------------------------------------------------------
%
% mod function for number theory
%
% This has been defined using "tdiv"
%
% 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 tdiv
i,k,cc: VAR int
m: VAR posnat
n,a,b,c: VAR nat
j: VAR nonzero_integer
ml3: LEMMA abs(i - m * floor(i/m)) < m
ml4: LEMMA abs(i + m * floor(-i/m)) < m
mod(i,j): {k| abs(k) < abs(j)} = i-j*tdiv(i,j)
mod_even: LEMMA integer?(i/j) IMPLIES mod(i,j) = 0
mod_neg: LEMMA mod(-i,j) = IF integer?(i/j) THEN 0
ELSE j - mod(i,j)
ENDIF
mod_neg_d: LEMMA mod(i,-j) = IF integer?(i/j) THEN 0
ELSE mod(i,j) - j
ENDIF
mod_eq_arg: LEMMA mod(j,j) = 0
mod_lt: LEMMA abs(i) < abs(j) IMPLIES mod(i,j) =
IF sgn(i) = sgn(j) OR i = 0 THEN i
ELSE i + j
ENDIF
mod_lt_nat: LEMMA n < m IMPLIES mod(n,m) = n
mod_sum_pos: LEMMA mod(i+k*m,m) = mod(i,m)
mod_sum: LEMMA mod(i+k*j,j) = mod(i,j)
mod_it_is: LEMMA a = b + m*c AND b < m IMPLIES b = mod(a,m)
mod_zero: LEMMA mod(0,j) = 0
mod_0 : LEMMA mod(0,j) = 0
mod_one: LEMMA mod(1,j) = IF abs(j) = 1 THEN 0
ELSIF j > 0 THEN 1
ELSE j + 1
ENDIF
mod_of_mod: LEMMA mod(i + mod(k,m), m) = mod(i+k, m)
mod_pos: LEMMA mod(i,m) >= 0 AND mod(i,m) < m
JUDGEMENT mod(i,m) HAS_TYPE below(m)
% ------- connection with prelude rem --------------
mod_to_rem: LEMMA mod(i,m) = rem(m)(i)
mod_0_divides: LEMMA mod(i,j) = 0 IFF divides(j,i)
AUTO_REWRITE+ mod_pos
AUTO_REWRITE+ mod_0
AUTO_REWRITE+ mod_eq_arg
AUTO_REWRITE+ mod_sum_pos
AUTO_REWRITE+ mod_of_mod
AUTO_REWRITE+ mod_sum
END tmod
[ Dauer der Verarbeitung: 0.2 Sekunden
(vorverarbeitet)
]
|
|
