Quellcode-Bibliothek general_properties.pvs   Sprache: PVS

%%-------------------** Properties of divides and gcd **----------
%%                                                                          
%% Author          : André Luiz Galdino 
%%                   Universidade Federal de Goiás - Brasil
%%                    
%% Last Modified On: November 28, 2011
%%                                                                          
%%----------------------------------------------------------------


general_properties: THEORY

BEGIN


  IMPORTING ints@gcd,
            ints@gcd_fractions,
            numbers@unique_factorization,
            numbers@product_perm_lems,
            numbers@eq_mod,
            structures@fseqs[posnat],
            structures@fseqs_ops_def

      x, y, z, m: VAR int
      i, p, q, k: VAR posnat
            j, n: VAR nat
              fs: VAR fseq

  
%%%%% Definitions %%%%%

   seq_power(p,i): fseq = (# length := i,
                                seq := (LAMBDA (j: nat): IF j < i THEN p ELSE default ENDIF) #)

   only_power_p(fs, p):  bool = FORALL (j: below(fs`length)): EXISTS (i: nat): fs`seq(j) = p^i


%%%%% Properties %%%%%

   divides_element: LEMMA
     divides(x, y + z) AND divides(x, y) IMPLIES  divides(x, z)

   divides_rel_primes: LEMMA divides(x,k*y) AND gcd(x,k) = 1 IMPLIES divides(x,y)

   divides_product: LEMMA FORALL (j: below(fs`length)): divides(fs`seq(j), product(fs))

   product_power: LEMMA p^i = product(seq_power(p,i))

   product_only_power: LEMMA only_power_p(fs, p) IMPLIES 
                              EXISTS (n: nat): product(fs) = p^n

   divides_power: LEMMA  divides(p, p^i) 
                                    
   divides_prime_power: LEMMA prime?(p) AND divides(q, p^j) 
                                      IMPLIES (EXISTS (i: nat): i <= j AND q = p^i)


   gcd_1: LEMMA gcd(m,1) = 1

   gcd_1_nd: LEMMA prime?(p) AND gcd(m,p) = 1 IMPLIES (NOT divides(p,m))

   gcd_1_ndp: LEMMA prime?(p) AND gcd(m,p) = 1 AND m = x*y IMPLIES (NOT divides(p,x) AND NOT divides(p,y))
   
   gcd_1_gcd_1: LEMMA prime?(p) AND gcd(m,p) = 1 AND m = x*y IMPLIES gcd(x,p) = 1 AND gcd(y,p) = 1


END general_properties