SSL eq_mod.pvs

eq_mod: THEORY
%-------------------------------------------------------------------------------


%-------------------------------------------------------------------------------
BEGIN

    p: VAR nat
    a,b,c,d: VAR int
    j,k: VAR int

    IMPORTING ints@primes

    eq_mod(p)(a,b): bool = (EXISTS k: a = k*p + b)

    eq_mod_equiv: LEMMA equivalence?(eq_mod(p))

    eq_mod_mult : LEMMA eq_mod(p)(a,b) AND
                        eq_mod(p)(c,d) 
                       IMPLIES
                           eq_mod(p)(a*c,b*d)

    eq_mod_rem  : LEMMA p > 0 IMPLIES eq_mod(p)(j, rem(p)(j))


    IMPORTING ints@gcd   

    gcd_is_1: LEMMA prime?(p) AND NOT divides(p,a) IMPLIES
                    gcd(a,p) = 1

    Euclids_30: LEMMA prime?(p) AND divides(p,a*b) IMPLIES
                      divides(p,a) OR divides(p,b)

    eq_mod_cancel: LEMMA prime?(p) AND
                         NOT divides(p, c)
                    IMPLIES
                         eq_mod(p)(a*c,b*c) IMPLIES
                         eq_mod(p)(a,b)


END eq_mod