| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/PVS/ints/ (Beweissystem der NASA Version 6.0.9©) Datei vom 28.9.2014 mit Größe 3 kB |
|
Quellcode-Bibliothek gcd.pvs Sprache: PVS |
|||||||||
|
gcd: THEORY
%------------------------------------------------------------------------------ % Author: Alfons Geser, HTWK Leipzig, Germany % Ricky W. Butler, NASA Langley % Date: May, 2009 % % Anthony N (March 2012) %------------------------------------------------------------------------------ BEGIN IMPORTING divides_lems, mod_lems IMPORTING div %% for proof n,m: VAR nat nn,mm: VAR posnat p, q, l: VAR posint i,j,k,ip,jp: VAR int ii,jj,kk: VAR nzint gcd(i:int,j: {jj:int| i=0 => jj /= 0}): {k: posnat | divides(k,i) AND divides(k,j)} = max({k: posnat | divides(k,i) AND divides(k,j)}) gcd_divides: LEMMA (i /= 0 OR j /= 0) IMPLIES divides(gcd(i,j),i) AND divides(gcd(i,j),j) gcd_is_max: LEMMA (i /= 0 OR j /= 0) AND divides(kk,i) AND divides(kk,j) IMPLIES kk <= gcd(i,j) gcd_def : LEMMA (i /= 0 OR j /= 0) IMPLIES (gcd(i,j) = nn IFF ( (divides(nn,i) AND divides(nn,j)) AND (FORALL mm: divides(mm,i) AND divides(mm,j) IMPLIES mm <= nn))) gcd_0_pos : LEMMA gcd(0,mm) = mm gcd_abs : LEMMA (i /= 0 OR j /= 0) IMPLIES gcd(i,j) = gcd(abs(i),abs(j)) gcd_0_neg : LEMMA gcd(0,-mm) = mm gcd_sym : LEMMA (i /= 0 OR j /= 0) IMPLIES gcd(i,j) = gcd(j,i) gcd_lt_nat : LEMMA (n /= 0) IMPLIES gcd(n,m) <= n gcd_lt : LEMMA (i /= 0 AND j /= 0) IMPLIES gcd(i,j) <= min(abs(i),abs(j)) gcd_0 : LEMMA gcd(0,ii) = abs(ii) gcd_mod : LEMMA (i /= 0) IMPLIES gcd(mod(j,i),i) = gcd(i,j) gcd_mod_div: LEMMA (i /= 0) IMPLIES divides(gcd(i,j),mod(j,i)) gcd_factors_nat: LEMMA (n /= 0 OR m /= 0) IMPLIES EXISTS ip,jp: gcd(n,m) = ip*n + jp*m gcd_factors: LEMMA (i /= 0 OR j /= 0) IMPLIES EXISTS ip,jp: gcd(i,j) = ip*i + jp*j divides_gcd: LEMMA (i /= 0 OR j /= 0) AND divides(kk,i) AND divides(kk,j) IMPLIES divides(kk,gcd(i,j)) gcd_same : LEMMA gcd(p, p) = p gcd_minus: LEMMA p /= q IMPLIES gcd(p, q) = gcd(p, q - p) gcd_times: LEMMA gcd(p * l, q * l) = gcd(p, q) * l % % relatively_prime % rel_prime(i:int,j: {jj:int| i=0 => jj /= 0}): bool = (gcd(i,j) = 1) rel_prime_lem: LEMMA (i /= 0 OR j /= 0) IMPLIES ( rel_prime(i,j) IFF (EXISTS (n,m: int): 1 = m*i + n*j) ) % Bezouts: LEMMA gcd(a,b) = d IMPLIES % EXISTS (j,k: int): a*j+b*k = d rel_prime_div_prod: LEMMA (i/=0 OR j/=0) IMPLIES rel_prime(i,j) AND divides(i,j*k) IMPLIES divides(i,k) rel_prime_sym: LEMMA (i/=0 OR j/=0) IMPLIES rel_prime(i,j) = rel_prime(j,i) rel_prime_mult_right: LEMMA (i/=0 OR j/=0) AND (i/=0 OR k/=0) AND rel_prime(i,j) AND rel_prime(i,k) IMPLIES rel_prime(i,j*k) rel_prime_mult_left: LEMMA (i/=0 OR j/=0) AND (j/=0 OR k/=0) AND rel_prime(i,j) AND rel_prime(k,j) IMPLIES rel_prime(i*k,j) % % Euclid's algorithm % compute_gcd(i:int,j:{jj:int| i=0 => jj /= 0}): RECURSIVE {kj: posnat | kj = gcd(i,j)} = IF i<0 THEN compute_gcd(-i,j) ELSIF j<0 THEN compute_gcd(i,-j) ELSIF i=0 THEN j ELSIF j=0 THEN i ELSIF i<j THEN compute_gcd(j,i) ELSE (LET rem = mod(i,j) IN IF rem = 0 THEN j ELSE compute_gcd(j,rem) ENDIF) ENDIF MEASURE (IF i<0 AND j<0 THEN -i-j+3 ELSIF i<0 THEN -i+j+2 ELSIF j<0 THEN i-j+2 ELSIF i<j THEN i+j+1 ELSE i+j ENDIF) % Inverse IMPORTING pigeonhole rel_prime_inverse: LEMMA m>1 AND rel_prime(n,m) IMPLIES FORALL (q:below(m)): EXISTS (k:below(m)): mod(n*k,m) = q END gcd ¤ 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.0.3Bemerkung: ¤*© Formatika GbR, Deutschland |
|
