%Patch files loaded: patch2 version 2.414 \$\$\$rsa.pvs rsa : THEORY BEGIN IMPORTING fermat p: prime_nat q: { x: prime_nat | p /= x } p1: posnat = p - 1 q1: posnat = q - 1 %------------------ % public modulus %------------------ N: posnat = p * q N_not_one: LEMMA N /= 1 m: posnat = p1 * q1 m_not_one: LEMMA m /= 1 %-------------------------------- % private and public exponents %-------------------------------- a: { x: posnat | prime(x, m) } b: { x: posnat | rem(m)(a * x) = 1} %--------------- % Main lemmas %--------------- x: VAR posnat prime_with_N: LEMMA prime(x, N) IFF prime(x, p) AND prime(x, q) fermat_p: LEMMA prime(x, p) IMPLIES rem(p)(expt(x, p1 * q1)) = 1 fermat_q: LEMMA prime(x, q) IMPLIES rem(q)(expt(x, p1 * q1)) = 1 rsa_aux1: LEMMA rem(p)(expt(x, a * b)) = rem(p)(x) rsa_aux2: LEMMA rem(q)(expt(x, a * b)) = rem(q)(x) rsa_prop: LEMMA rem(N)(expt(x, a * b)) = rem(N)(x) %------------------- % Encrypt/Decrypt %------------------- y: VAR mod(N) private(y): mod(N) = rem(N)(expt(y, a)) public(y): mod(N) = rem(N)(expt(y, b)) private_zero: LEMMA private(0) = 0 public_zero: LEMMA public(0) = 0 inverse_rsa1: LEMMA public(private(y)) = y inverse_rsa2: LEMMA private(public(y)) = y END rsa \$\$\$rsa.prf (|rsa| (|q_TCC1| "" (LEMMA "unbounded_primes" ("x" "p")) (("" (SKOLEM!) (("" (INST + "p!1") (("" (ASSERT) NIL))))))) (|p1_TCC1| "" (SUBTYPE-TCC) NIL) (|q1_TCC1| "" (SUBTYPE-TCC) NIL) (|N_not_one| "" (FLATTEN) (("" (EXPAND "N") (("" (REWRITE "product_one") (("" (GROUND) NIL))))))) (|m_not_one| "" (FLATTEN) (("" (EXPAND "m") (("" (REWRITE "product_one") (("" (EXPAND* "p1" "q1") (("" (GROUND) NIL))))))))) (|a_TCC1| "" (INST + "1 + m") (("" (REWRITE "mutual_primes_equiv") (("" (INST + "1" "-1") (("" (ASSERT) NIL))))))) (|b_TCC1| "" (LEMMA "rem_inverse2") (("" (INST - "m" "a") (("" (LEMMA "m_not_one") (("" (ASSERT) (("" (GROUND) (("" (SKOLEM!) (("" (INST + "py!1") NIL))))))))))))) (|prime_with_N_TCC1| "" (ASSERT) (("" (SKOSIMP) (("" (ASSERT) NIL))))) (|prime_with_N| "" (SKOLEM!) (("" (EXPAND "N") (("" (REWRITE "mutual_primes_commutes") (("" (REWRITE "mutual_prime_prod") (("" (USE "mutual_primes_commutes" ("a" "p")) (("" (USE "mutual_primes_commutes" ("a" "q")) (("" (REPLACE*) (("" (GROUND) NIL))))))))))))))) (|fermat_p| "" (SKOSIMP) (("" (AUTO-REWRITE "expt_times_aux" "rem_one" "expt_1n_aux") (("" (FORWARD-CHAIN "fermat_theorem2") (("" (REWRITE "p1" :DIR RL) (("" (ASSERT) (("" (REWRITE "rem_expt1" 1 :DIR RL) (("" (REPLACE*) (("" (ASSERT) NIL))))))))))))))) (|fermat_q_TCC1| "" (ASSERT) NIL) (|fermat_q| "" (SKOSIMP) (("" (AUTO-REWRITE "rem_one" "expt_1n_aux") (("" (FORWARD-CHAIN "fermat_theorem2") (("" (REWRITE "q1" :DIR RL) (("" (USE "expt_times_aux" ("m" "q1" "n" "p1")) (("" (REPLACE -1) (("" (REWRITE "rem_expt1" 1 :DIR RL) (("" (REPLACE*) (("" (ASSERT) NIL))))))))))))))))) (|rsa_aux1| "" (SKOSIMP) (("" (USE "non_multiple_of_prime" ("p" "p" "a" "x!1")) (("" (GROUND) (("1" (AUTO-REWRITE "expt" "zero_times1" "rem_zero") (("1" (REWRITE "rem_expt1" :DIR RL) (("1" (CASE-REPLACE "rem(p)(x!1) = 0") (("1" (ASSERT) NIL) ("2" (REWRITE "rem_def2") NIL))))))) ("2" (REWRITE "mutual_primes_commutes") (("2" (TYPEPRED "b") (("2" (ASSERT) (("2" (REWRITE "rem_def") (("2" (SKOLEM!) (("2" (CASE "q!1 >= 0") (("1" (ASSERT) (("1" (REPLACE*) (("1" (DELETE -1 -2 -3) (("1" (AUTO-REWRITE "expt_1n_aux" "rem_one" "fermat_p") (("1" (EXPAND "expt") (("1" (REWRITE "expt_times_aux") (("1" (REWRITE "rem_prod2" :DIR RL) (("1" (REWRITE "rem_expt1" :DIR RL) (("1" (EXPAND "m") (("1" (ASSERT) NIL))))))))))))))))))) ("2" (DELETE -3 2) (("2" (USE "pos_times_le" ("x" "m" "y" "q!1")) (("2" (GROUND) NIL))))))))))))))))))))))) (|rsa_aux2| "" (SKOSIMP) (("" (USE "non_multiple_of_prime" ("p" "q" "a" "x!1")) (("" (GROUND) (("1" (AUTO-REWRITE "expt" "zero_times1" "rem_zero") (("1" (REWRITE "rem_expt1" :DIR RL) (("1" (CASE-REPLACE "rem(q)(x!1) = 0") (("1" (ASSERT) NIL) ("2" (REWRITE "rem_def2") NIL))))))) ("2" (REWRITE "mutual_primes_commutes") (("2" (TYPEPRED "b") (("2" (ASSERT) (("2" (REWRITE "rem_def") (("2" (SKOLEM!) (("2" (CASE "q!1 >= 0") (("1" (ASSERT) (("1" (REPLACE*) (("1" (DELETE -1 -2 -3) (("1" (AUTO-REWRITE "expt_1n_aux" "rem_one" "fermat_q") (("1" (EXPAND "expt") (("1" (REWRITE "expt_times_aux") (("1" (REWRITE "rem_prod2" :DIR RL) (("1" (REWRITE "rem_expt1" :DIR RL) (("1" (EXPAND "m") (("1" (ASSERT) NIL))))))))))))))))))) ("2" (DELETE -3 2) (("2" (USE "pos_times_le" ("x" "m" "y" "q!1")) (("2" (GROUND) NIL))))))))))))))))))))))) (|rsa_prop| "" (SKOLEM!) (("" (AUTO-REWRITE "same_remainder" "distinct_primes" "divides_zero") (("" (USE* "rsa_aux1" "rsa_aux2") (("" (ASSERT) (("" (EXPAND "N") (("" (REWRITE "common_multiple_primes") (("" (FLATTEN) (("" (REPLACE*) (("" (ASSERT) NIL))))))))))))))))) (|private_zero_TCC1| "" (SUBTYPE-TCC) NIL) (|private_zero| "" (AUTO-REWRITE "private" "expt" "zero_times1" "rem_zero") (("" (ASSERT) (("" (ASSERT) NIL))))) (|public_zero| "" (AUTO-REWRITE "public" "expt" "zero_times1" "rem_zero") (("" (ASSERT) (("" (ASSERT) NIL))))) (|inverse_rsa1| "" (AUTO-REWRITE "private_zero" "public_zero" "rem_expt1" "rem_mod" "rsa_prop") (("" (SKOLEM!) (("" (CASE-REPLACE "y!1 = 0") (("1" (ASSERT) NIL) ("2" (EXPAND "public") (("2" (EXPAND "private") (("2" (ASSERT) (("2" (REWRITE "expt_times_aux" :DIR RL) (("2" (ASSERT) NIL))))))))))))))) (|inverse_rsa2| "" (AUTO-REWRITE "private_zero" "public_zero" "rem_expt1" "rem_mod" "rsa_prop") (("" (SKOLEM!) (("" (CASE-REPLACE "y!1 = 0") (("1" (ASSERT) NIL) ("2" (EXPAND "public") (("2" (EXPAND "private") (("2" (ASSERT) (("2" (REWRITE "expt_times_aux" :DIR RL) (("2" (REWRITE "commutative_mult") (("2" (ASSERT) NIL)))))))))))))))))) \$\$\$product_modulo.pvs product_modulo : THEORY BEGIN IMPORTING product_nat, modulo_arithmetic u, v: VAR [nat -> nat] n, m: VAR nat p: VAR posnat equivalent_product: LEMMA n <= m AND (FORALL (i: idx(n, m)): rem(p)(u(i)) = rem(p)(v(i))) IMPLIES rem(p)(prod(n, m)(u)) = rem(p)(prod(n, m)(v)) END product_modulo \$\$\$product_modulo.prf (|product_modulo| (|equivalent_product_TCC1| "" (SUBTYPE-TCC) NIL) (|equivalent_product| "" (SKOSIMP) (("" (ASSERT) (("" (CASE "FORALL (j : nat): j <= m!1 - n!1 IMPLIES rem(p!1)(prod(n!1, n!1 + j)(u!1)) = rem(p!1)(prod(n!1, n!1+j)(v!1))") (("1" (INST - "m!1 - n!1") (("1" (ASSERT) NIL))) ("2" (DELETE 2) (("2" (INDUCT-AND-REWRITE "j" 1 "prod_once" "prod_step" "rem_prod") NIL)))))))))) \$\$\$modulo_arithmetic.pvs modulo_arithmetic : THEORY BEGIN IMPORTING euclidean_division, divides, mutual_primes x, y, z, t, q : VAR int n0x : VAR nzint px, py, b: VAR posnat n: VAR nat %--------------------- % Remainder of x/b %--------------------- rem(b)(x): mod(b) = epsilon! (r: mod(b)): EXISTS q: x = b * q + r rem_def: LEMMA FORALL (r : mod(b)): rem(b)(x) = r IFF EXISTS q: x = b * q + r rem_def2: LEMMA FORALL (r : mod(b)): rem(b)(x) = r IFF divides(b, x - r) rem_def3: LEMMA FORALL (r : mod(b)): rem(b)(x) = r IFF divides(b, r - x) %------------------------ % Remainder for easy x %------------------------ rem_mod: LEMMA FORALL (r : mod(b)): rem(b)(r) = r rem_mod2: LEMMA 0 <= x AND x < b IMPLIES rem(b)(x) = x rem_zero: LEMMA rem(b)(0) = 0 rem_self: LEMMA rem(b)(b) = 0 rem_multiple1: LEMMA rem(b)(b * x) = 0 rem_multiple2: LEMMA rem(b)(x * b) = 0 rem_one: LEMMA b /= 1 IMPLIES rem(b)(1) = 1 %------------------------- % Congruence properties %------------------------- same_remainder: LEMMA rem(b)(x) = rem(b)(y) IFF divides(b, x - y) rem_rem: LEMMA rem(b)(rem(b)(x)) = rem(b)(x) rem_sum: LEMMA rem(b)(x) = rem(b)(y) AND rem(b)(z) = rem(b)(t) IMPLIES rem(b)(x + z) = rem(b)(y + t) rem_sum1: LEMMA rem(b)(rem(b)(x) + y) = rem(b)(x + y) rem_sum2: LEMMA rem(b)(x + rem(b)(y)) = rem(b)(x + y) rem_diff: LEMMA rem(b)(x) = rem(b)(y) AND rem(b)(z) = rem(b)(t) IMPLIES rem(b)(x - z) = rem(b)(y - t) rem_diff1: LEMMA rem(b)(rem(b)(x) - y) = rem(b)(x - y) rem_diff2: LEMMA rem(b)(x - rem(b)(y)) = rem(b)(x - y) rem_prod1: LEMMA rem(b)(rem(b)(x) * y) = rem(b)(x * y) rem_prod2: LEMMA rem(b)(x * rem(b)(y)) = rem(b)(x * y) rem_prod: LEMMA rem(b)(x) = rem(b)(y) AND rem(b)(z) = rem(b)(t) IMPLIES rem(b)(x * z) = rem(b)(y * t) rem_expt: LEMMA rem(b)(x) = rem(b)(y) IMPLIES rem(b)(expt(x, n)) = rem(b)(expt(y, n)) rem_expt1: LEMMA rem(b)(expt(rem(b)(x), n)) = rem(b)(expt(x, n)) rem_sum_elim1: LEMMA rem(b)(x + y) = rem(b)(x + z) IFF rem(b)(y) = rem(b)(z) rem_sum_elim2: LEMMA rem(b)(y + x) = rem(b)(z + x) IFF rem(b)(y) = rem(b)(z) rem_diff_elim1: LEMMA rem(b)(x - y) = rem(b)(x - z) IFF rem(b)(y) = rem(b)(z) rem_diff_elim2: LEMMA rem(b)(y - x) = rem(b)(z - x) IFF rem(b)(y) = rem(b)(z) rem_opposite_elim: LEMMA rem(b)(- x) = rem(b)(- y) IFF rem(b)(x) = rem(b)(y) %------------------------------------ % Existence of an inverse modulo b %------------------------------------ rem_inverse: LEMMA (EXISTS y : rem(b)(x * y) = 1) IFF x/=0 AND b/=1 AND prime(x, b) rem_inverse2: LEMMA (EXISTS py: rem(b)(x * py) = 1) IFF x/=0 AND b/=1 AND prime(x, b) END modulo_arithmetic \$\$\$modulo_arithmetic.prf (|modulo_arithmetic| (|rem_def| "" (SKOLEM!) (("" (CASE "EXISTS q: x!1 = b!1 * q + rem(b!1)(x!1)") (("1" (GROUND) (("1" (SKOSIMP*) (("1" (USE "unique_remainder") (("1" (ASSERT) NIL))))))) ("2" (DELETE 2) (("2" (EXPAND "rem") (("2" (LEMMA "epsilon_ax" ("p" "lambda (r : mod(b!1)) : EXISTS (q: int): x!1 = r + b!1 * q")) (("2" (GROUND) (("2" (USE "euclide_int" ("b" "b!1")) (("2" (SKOSIMP) (("2" (INST + "r!2") (("2" (INST?) (("2" (ASSERT) NIL))))))))))))))))))))) (|rem_def2| "" (SKOLEM!) (("" (REWRITE "rem_def") (("" (EXPAND "divides") (("" (GROUND) (("1" (SKOLEM!) (("1" (INST?) (("1" (ASSERT) NIL))))) ("2" (SKOLEM!) (("2" (INST?) (("2" (ASSERT) NIL))))))))))))) (|rem_def3| "" (SKOLEM!) (("" (REWRITE "rem_def2") (("" (GROUND) (("1" (REWRITE "divides_opposite" :DIR RL) NIL) ("2" (REWRITE "divides_opposite" :DIR RL) NIL))))))) (|rem_mod| "" (AUTO-REWRITE "divides_zero") (("" (SKOLEM!) (("" (REWRITE "rem_def2") NIL))))) (|rem_mod2| "" (SKOSIMP) (("" (ASSERT) (("" (REWRITE "rem_mod") NIL))))) (|rem_zero| "" (AUTO-REWRITE "divides_zero" "rem_def2") (("" (SKOLEM!) (("" (ASSERT) NIL))))) (|rem_self| "" (AUTO-REWRITE "divides_reflexive" "rem_def2") (("" (SKOLEM!) (("" (ASSERT) NIL))))) (|rem_multiple1| "" (AUTO-REWRITE "divides_prod1" "divides_prod2" "divides_reflexive" "rem_def2") (("" (SKOLEM!) (("" (ASSERT) NIL))))) (|rem_multiple2| "" (AUTO-REWRITE "divides_prod1" "divides_prod2" "divides_reflexive" "rem_def2") (("" (SKOLEM!) (("" (ASSERT) NIL))))) (|rem_one| "" (SKOSIMP) (("" (REWRITE "rem_def") (("" (INST + "0") (("" (ASSERT) NIL))))))) (|same_remainder| "" (SKOLEM!) (("" (NAME-REPLACE "r!1" "rem(b!1)(y!1)" :HIDE? NIL) (("" (REWRITE "rem_def2") (("" (REWRITE "rem_def2") (("" (GROUND) (("1" (USE "divides_diff" ("n" "x!1 - r!1" "m" "y!1 - r!1")) (("1" (ASSERT) NIL))) ("2" (USE "divides_sum" ("n" "x!1 - y!1" "m" "y!1 - r!1")) (("2" (ASSERT) NIL))))))))))))) (|rem_rem| "" (SKOLEM!) (("" (REWRITE "same_remainder") (("" (NAME-REPLACE "r!1" "rem(b!1)(x!1)" :HIDE? NIL) (("" (REWRITE "rem_def3") NIL))))))) (|rem_sum| "" (AUTO-REWRITE "same_remainder") (("" (SKOSIMP) (("" (ASSERT) (("" (USE "divides_sum" ("n" "x!1 - y!1" "m" "z!1 - t!1")) (("" (ASSERT) NIL))))))))) (|rem_sum1| "" (SKOLEM!) (("" (REWRITE "same_remainder") (("" (REWRITE "rem_def3" :DIR RL) NIL))))) (|rem_sum2| "" (SKOLEM!) (("" (USE "rem_sum1" ("x" "y!1" "y" "x!1")) (("" (ASSERT) NIL))))) (|rem_diff| "" (AUTO-REWRITE "same_remainder") (("" (SKOSIMP) (("" (ASSERT) (("" (USE "divides_diff" ("n" "x!1 - y!1" "m" "z!1 - t!1")) (("" (ASSERT) NIL))))))))) (|rem_diff1| "" (SKOLEM!) (("" (REWRITE "same_remainder") (("" (REWRITE "rem_def3" :DIR RL) NIL))))) (|rem_diff2| "" (SKOLEM!) (("" (REWRITE "same_remainder") (("" (REWRITE "rem_def2" :DIR RL) NIL))))) (|rem_prod1| "" (SKOLEM!) (("" (REWRITE "same_remainder") (("" (USE "divides_prod1" ("n" "rem(b!1)(x!1) - x!1" "m" "y!1")) (("" (ASSERT) (("" (REWRITE "rem_def3" :DIR RL) NIL))))))))) (|rem_prod2| "" (SKOLEM!) (("" (USE "rem_prod1" ("x" "y!1" "y" "x!1")) (("" (ASSERT) NIL))))) (|rem_prod| "" (SKOSIMP) (("" (AUTO-REWRITE "rem_prod1" "rem_prod2") (("" (CASE "rem(b!1)(rem(b!1)(x!1) * rem(b!1)(z!1)) = rem(b!1)(y!1 * t!1)") (("1" (ASSERT) NIL) ("2" (REPLACE*) (("2" (ASSERT) NIL))))))))) (|rem_expt| "" (SKOLEM 1 ("b!1" _ "x!1" "y!1")) (("" (INDUCT-AND-SIMPLIFY "n" :EXCLUDE "rem" :REWRITES ("rem_prod")) NIL))) (|rem_expt1| "" (SKOLEM!) (("" (REWRITE "rem_expt") (("" (REWRITE "rem_rem") NIL))))) (|rem_sum_elim1| "" (AUTO-REWRITE "same_remainder") (("" (SKOLEM!) (("" (ASSERT) NIL))))) (|rem_sum_elim2| "" (AUTO-REWRITE "same_remainder") (("" (SKOLEM!) (("" (ASSERT) NIL))))) (|rem_diff_elim1| "" (AUTO-REWRITE "same_remainder") (("" (SKOLEM!) (("" (ASSERT) (("" (PROP) (("1" (REWRITE "divides_opposite" :DIR RL) (("1" (ASSERT) NIL))) ("2" (REWRITE "divides_opposite" :DIR RL) (("2" (ASSERT) NIL))))))))))) (|rem_diff_elim2| "" (AUTO-REWRITE "same_remainder") (("" (SKOLEM!) (("" (ASSERT) NIL))))) (|rem_opposite_elim| "" (AUTO-REWRITE "same_remainder") (("" (SKOLEM!) (("" (ASSERT) (("" (REWRITE "divides_opposite" :DIR RL) (("" (GROUND) NIL))))))))) (|rem_inverse| "" (SKOLEM!) (("" (CASE-REPLACE "x!1=0") (("1" (AUTO-REWRITE "rem_zero") (("1" (ASSERT) NIL))) ("2" (ASSERT) (("2" (AUTO-REWRITE "mutual_primes_equiv" "rem_def") (("2" (ASSERT) (("2" (PROP) (("1" (SKOLEM!) (("1" (ASSERT) NIL))) ("2" (SKOLEM!) (("2" (ASSERT) (("2" (ASSERT) (("2" (SKOLEM!) (("2" (INST + "y!1" "-q!1") (("2" (ASSERT) NIL))))))))))) ("3" (SKOLEM!) (("3" (INST + "n!1") (("3" (ASSERT) (("3" (INST + "- m!1") (("3" (ASSERT) NIL))))))))))))))))))))) (|rem_inverse2| "" (SKOLEM!) (("" (REWRITE "rem_inverse" :DIR RL) (("" (PROP) (("1" (SKOLEM!) (("1" (INST?) NIL))) ("2" (SKOLEM!) (("2" (REWRITE "rem_prod2" :DIR RL) (("2" (AUTO-REWRITE "rem_zero") (("2" (CASE-REPLACE "rem(b!1)(y!1) = 0") (("1" (ASSERT) NIL) ("2" (INST?) (("2" (ASSERT) NIL)))))))))))))))))) \$\$\$euclidean_division.pvs euclidean_division : THEORY BEGIN a, i : VAR nat b : VAR posnat n : VAR int %----------------------------------------------- % Type mod(b) = 0.. b-1 % (replace below[b] to reduce number of TCCs) %----------------------------------------------- mod(b) : NONEMPTY_TYPE = { i | i < b} %----------------------- % Euclidean division %----------------------- euclide_nat : LEMMA EXISTS (q : nat), (r : mod(b)) : a = b * q + r euclide_int : PROPOSITION EXISTS (q : int), (r : mod(b)) : n = b * q + r unique_quotient : PROPOSITION FORALL (q1, q2 : int), (r1, r2 : mod(b)) : b * q1 + r1 = b * q2 + r2 IMPLIES q1 = q2 unique_remainder : COROLLARY FORALL (q1, q2 : int), (r1, r2 : mod(b)) : b * q1 + r1 = b * q2 + r2 IMPLIES r1 = r2 unique_division : COROLLARY FORALL (q1, q2 : int), (r1, r2 : mod(b)) : b * q1 + r1 = b * q2 + r2 IMPLIES q1 = q2 AND r1 = r2 END euclidean_division \$\$\$euclidean_division.prf (|euclidean_division| (|mod_TCC1| "" (SKOLEM!) (("" (INST + "0") NIL))) (|euclide_nat| "" (SKOLEM 1 (_ "b!1")) (("" (INDUCT "a") (("1" (INST + "0" "0") (("1" (ASSERT) NIL))) ("2" (SKOSIMP*) (("2" (CASE "r!1 = b!1-1") (("1" (INST + "q!1+1" "0") (("1" (ASSERT) NIL))) ("2" (ASSERT) (("2" (INST + "q!1" "r!1+1") (("2" (ASSERT) NIL))))))))))))) (|euclide_int| "" (SKOLEM!) (("" (CASE "n!1 >= 0") (("1" (USE "euclide_nat" ("a" "n!1")) (("1" (SKOLEM!) (("1" (INST?) NIL))))) ("2" (ASSERT) (("2" (USE "euclide_nat" ("a" "- n!1")) (("2" (SKOLEM!) (("2" (CASE "r!1 = 0") (("1" (INST + "-q!1" "0") (("1" (ASSERT) NIL))) ("2" (INST + "- q!1 - 1" "b!1 - r!1") (("1" (ASSERT) NIL) ("2" (ASSERT) NIL))))))))))))))) (|unique_quotient| "" (SKOSIMP) (("" (LEMMA "both_sides_times_pos_le1") (("" (INST-CP -1 "b!1" "q1!1+1" "q2!1") (("" (INST -1 "b!1" "q2!1 + 1" "q1!1") (("" (ASSERT) NIL))))))))) (|unique_remainder| "" (SKOSIMP) (("" (FORWARD-CHAIN "unique_quotient") (("" (ASSERT) NIL))))) (|unique_division| "" (SKOSIMP) (("" (SPLIT) (("1" (FORWARD-CHAIN "unique_quotient") NIL) ("2" (FORWARD-CHAIN "unique_remainder") NIL))))) (|rem_def| "" (SKOLEM!) (("" (CASE "EXISTS (q: int): n!1 = b!1 * q + rem(n!1, b!1)") (("1" (GROUND) (("1" (SKOSIMP*) (("1" (LEMMA "unique_remainder" ("b" "b!1" "q1" "q!1" "r1" "r!1" "q2" "q!2" "r2" "rem(n!1, b!1)")) (("1" (ASSERT) NIL))))))) ("2" (DELETE 2) (("2" (EXPAND "rem") (("2" (LEMMA "epsilon_ax" ("p" "lambda (r : mod(b!1)) : EXISTS (q: int): n!1 = r + b!1 * q")) (("2" (GROUND) (("2" (USE "euclide_int" ("b" "b!1")) (("2" (SKOSIMP) (("2" (INST + "r!2") (("2" (INST?) (("2" (ASSERT) NIL)))))))))))))))))))))) \$\$\$divides.pvs % % Divisibility relation % % For integers and natural numbers % divides : THEORY BEGIN n, m, l, x, y : VAR int p, q : VAR nat nz : VAR nzint %-------------------- % Divides relation %-------------------- divides(n, m): bool = EXISTS x : m = n * x %---------------- % Easy lemmas %---------------- divides_sum : LEMMA divides(x, n) AND divides(x, m) IMPLIES divides(x, n + m) divides_diff : LEMMA divides(x, n) AND divides(x, m) IMPLIES divides(x, n - m) divides_opposite : LEMMA divides(x, - n) IFF divides(x, n) opposite_divides : LEMMA divides(- x, n) IFF divides(x, n) divides_prod1 : LEMMA divides(x, n) IMPLIES divides(x, n * m) divides_prod2 : LEMMA divides(x, n) IMPLIES divides(x, m * n) %--------------- % Elimination %--------------- divides_prod_elim1 : LEMMA divides(nz * n, nz * m) IFF divides(n, m) divides_prod_elim2 : LEMMA divides(n* nz, m * nz) IFF divides(n, m) %------------------------------------ % Reflexivity and transitivity %------------------------------------ divides_reflexive: LEMMA divides(n, n) divides_transitive: LEMMA divides(n, m) AND divides(m, l) IMPLIES divides(n, l) %----------------------------------------- % Mutual divisors are equal or opposite %----------------------------------------- product_one : LEMMA x * y = 1 IFF (x = 1 AND y = 1) OR (x = -1 AND y = -1) mutual_divisors : LEMMA divides(n, m) AND divides(m, n) IMPLIES n = m OR n = - m mutual_divisors_nat: LEMMA divides(p, q) AND divides(q, p) IMPLIES p = q %-------------------------------------- % special properties of zero and one %-------------------------------------- one_divides : LEMMA divides(1, n) divides_zero : LEMMA divides(n, 0) zero_div_zero : LEMMA divides(0, n) IFF n = 0 divisors_of_one : LEMMA divides(n, 1) IFF n = 1 OR n = -1 one_div_one : LEMMA divides(p, 1) IFF p = 1 %-------------------------------- % comparisons divisor/multiple %-------------------------------- divisor_smaller: LEMMA divides(p, q) IMPLIES q=0 OR p <= q END divides \$\$\$divides.prf (|divides| (|divides_sum| "" (EXPAND "divides") (("" (SKOSIMP*) (("" (INST + "x!2+x!3") (("" (ASSERT) NIL))))))) (|divides_diff| "" (EXPAND "divides") (("" (SKOSIMP*) (("" (INST + "x!2 - x!3") (("" (ASSERT) NIL))))))) (|divides_opposite| "" (EXPAND "divides") (("" (SKOLEM!) (("" (GROUND) (("1" (SKOLEM!) (("1" (INST + "-x!2") (("1" (ASSERT) NIL))))) ("2" (SKOLEM!) (("2" (INST + "-x!2") (("2" (ASSERT) NIL))))))))))) (|opposite_divides| "" (EXPAND "divides") (("" (SKOLEM!) (("" (PROP) (("1" (SKOLEM!) (("1" (INST + "-x!2") (("1" (ASSERT) NIL))))) ("2" (SKOLEM!) (("2" (INST + "-x!2") (("2" (ASSERT) NIL))))))))))) (|divides_prod1| "" (EXPAND "divides") (("" (SKOSIMP*) (("" (INST + "x!2 * m!1") (("" (ASSERT) NIL))))))) (|divides_prod2| "" (EXPAND "divides") (("" (SKOSIMP*) (("" (INST + "x!2 * m!1") (("" (ASSERT) NIL))))))) (|divides_prod_elim1| "" (EXPAND "divides") (("" (SKOLEM!) (("" (GROUND) (("1" (SKOLEM!) (("1" (LEMMA "both_sides_times2" ("n0z" "nz!1" "x" "m!1" "y" "x!1 * n!1")) (("1" (ASSERT) (("1" (INST + "x!1") (("1" (ASSERT) NIL))))))))) ("2" (SKOLEM!) (("2" (INST + "x!1") (("2" (ASSERT) NIL))))))))))) (|divides_prod_elim2| "" (SKOLEM!) (("" (LEMMA "divides_prod_elim1" ("n" "n!1" "m" "m!1" "nz" "nz!1")) (("" (GROUND) NIL))))) (|divides_reflexive| "" (EXPAND "divides") (("" (SKOLEM!) (("" (INST + "1") (("" (ASSERT) NIL))))))) (|divides_transitive| "" (EXPAND "divides") (("" (SKOSIMP*) (("" (INST + "x!1 * x!2") (("" (ASSERT) NIL))))))) (|product_one| "" (SKOLEM!) (("" (SPLIT) (("1" (FLATTEN) (("1" (HIDE 1 2) (("1" (USE "pos_times_lt") (("1" (ASSERT) (("1" (GROUND) (("1" (REVEAL 1) (("1" (LEMMA "both_sides_times_pos_le1" ("x" "1" "y" "x!1" "pz" "y!1")) (("1" (GROUND) NIL))))) ("2" (REVEAL 2) (("2" (LEMMA "both_sides_times_neg_le1" ("x" "-1" "y" "x!1" "nz" "y!1")) (("2" (GROUND) NIL))))))))))))))) ("2" (GROUND) NIL))))) (|mutual_divisors| "" (EXPAND "divides") (("" (SKOSIMP*) (("" (CASE "n!1 = 0") (("1" (ASSERT) NIL) ("2" (ASSERT) (("2" (LEMMA "both_sides_times1" ("n0z" "n!1" "x" "x!1 * x!2" "y" "1")) (("2" (GROUND) (("2" (REWRITE "product_one") NIL))))))))))))) (|mutual_divisors_nat| "" (SKOSIMP) (("" (FORWARD-CHAIN "mutual_divisors") (("" (ASSERT) NIL))))) (|one_divides| "" (GRIND) NIL) (|divides_zero| "" (GRIND :IF-MATCH ALL) NIL) (|zero_div_zero| "" (GRIND :IF-MATCH ALL) NIL) (|divisors_of_one| "" (AUTO-REWRITE "one_divides" "opposite_divides") (("" (REDUCE) (("" (EXPAND "divides") (("" (SKOLEM!) (("" (USE "product_one") (("" (GROUND) NIL))))))))))) (|one_div_one| "" (SKOLEM!) (("" (REWRITE "divisors_of_one") NIL))) (|divisor_smaller| "" (EXPAND "divides") (("" (SKOSIMP*) (("" (ASSERT) (("" (USE "pos_times_lt") (("" (GROUND) (("" (USE "both_sides_times_pos_le1" ("pz" "p!1" "x" "1" "y" "x!1")) (("" (ASSERT) NIL)))))))))))))) \$\$\$min_nat.pvs % % Smallest element of a nonempty set[T] % min_nat[T: TYPE FROM nat]: THEORY BEGIN S: VAR (nonempty?[T]) a, x: VAR T min(S): {a | S(a) AND (FORALL x: S(x) IMPLIES a <= x)} minimum?(a, S) : bool = S(a) AND (FORALL x: S(x) IMPLIES a <= x) min_def : LEMMA FORALL (S: (nonempty?[T])) : min(S) = a IFF minimum?(a, S) END min_nat \$\$\$min_nat.prf (|min_nat| (|min_TCC1| "" (INST + "lambda S: epsilon(lambda (n: nat): T_pred(n) AND S(n) AND FORALL x: S(x) IMPLIES n <= x)") (("" (SKOLEM!) (("" (USE "epsilon_ax[nat]") (("" (SPLIT -) (("1" (ASSERT) NIL) ("2" (DELETE 2) (("2" (ASSERT) (("2" (LEMMA "wf_nat") (("2" (EXPAND "well_founded?") (("2" (INST - "lambda (x: nat): T_pred(x) AND S!1(x)") (("2" (GROUND) (("1" (SKOLEM!) (("1" (INST? +) (("1" (ASSERT) (("1" (SKOSIMP) (("1" (INST?) (("1" (ASSERT) NIL))))))))))) ("2" (DELETE 2) (("2" (TYPEPRED "S!1") (("2" (GRIND) NIL))))))))))))))))))))))))) (|min_def| "" (SKOLEM!) (("" (TYPEPRED "min(S!1)") (("" (EXPAND "minimum?") (("" (GROUND) (("1" (REPLACE*) NIL) ("2" (INST? -2 :WHERE -4) (("2" (INST? - :WHERE -1) (("2" (ASSERT) NIL)))))))))))))) \$\$\$common_divisor.pvs common_divisor : THEORY BEGIN IMPORTING min_nat, divides, euclidean_division a, b: VAR nzint c, d, x: VAR posnat n, m: VAR int E(a, b) : (nonempty?[posnat]) = { x | EXISTS n, m: x = a * n + b * m } gcd(a, b): posnat = min(E(a, b)) gcd_decomp: LEMMA EXISTS n, m: gcd(a, b) = a * n + b * m gcd_commutes: LEMMA gcd(b, a) = gcd(a, b) gcd_divides1: LEMMA divides(gcd(a, b), a) gcd_divides2: LEMMA divides(gcd(a, b), b) greatest_common_divisor: LEMMA divides(x, a) AND divides(x, b) IMPLIES divides(x, gcd(a, b)) gcd_def: LEMMA gcd(a, b) = d IFF (divides(d, a) AND divides(d, b) AND (FORALL x: divides(x, a) AND divides(x, b) IMPLIES divides(x, d))) gcd_self: LEMMA gcd(c, c) = c gcd_opp1: LEMMA gcd(-a, b) = gcd(a, b) gcd_opp2: LEMMA gcd(a, -b) = gcd(a, b) gcd_one1: LEMMA gcd(1, a) = 1 gcd_one2: LEMMA gcd(a, 1) = 1 gcd_rule1: LEMMA a + b * x /= 0 IMPLIES gcd(a + b * x, b) = gcd(a, b) gcd_rule2: LEMMA b + a * x /= 0 IMPLIES gcd(a, b + a * x) = gcd(a, b) gcd_multiple1: LEMMA gcd(c * a, c) = c gcd_multiple2: LEMMA gcd(c, c * a) = c gcd_multiple3: LEMMA gcd(c, b) = c IFF divides(c, b) gcd_multiple4: LEMMA gcd(a, c) = c IFF divides(c, a) gcd_bound1: LEMMA gcd(c, b) <= c gcd_bound2: LEMMA gcd(a, c) <= c END common_divisor \$\$\$common_divisor.prf (|common_divisor| (E_TCC1 "" (GRIND :IF-MATCH NIL) (("" (CASE "a!1 < 0") (("1" (ASSERT) (("1" (INST - "- a!1") (("1" (INST + "-1" "0") (("1" (ASSERT) NIL))))))) ("2" (ASSERT) (("2" (INST - "a!1") (("2" (INST + "1" "0") (("2" (ASSERT) NIL))))))))))) (|gcd_decomp| "" (SKOLEM!) (("" (EXPAND "gcd") (("" (TYPEPRED "min(E(a!1, b!1))") (("" (EXPAND "E" -2 1) (("" (PROPAX) NIL))))))))) (|gcd_commutes| "" (SKOLEM!) (("" (EXPAND "gcd") (("" (CASE-REPLACE "E(b!1, a!1) = E(a!1, b!1)") (("" (APPLY-EXTENSIONALITY :HIDE? T) (("" (GRIND :IF-MATCH NIL) (("1" (INST?) NIL) ("2" (INST?) NIL))))))))))) (|gcd_divides1| "" (SKOLEM!) (("" (LEMMA "euclide_int" ("n" "a!1" "b" "gcd(a!1, b!1)")) (("" (SKOLEM!) (("" (CASE-REPLACE "r!1 = 0") (("1" (EXPAND "divides") (("1" (INST?) (("1" (ASSERT) NIL))))) ("2" (DELETE 2) (("2" (ASSERT) (("2" (CASE "E(a!1, b!1)(r!1)") (("1" (TYPEPRED "r!1") (("1" (DELETE -3 1) (("1" (EXPAND "gcd") (("1" (TYPEPRED "min(E(a!1, b!1))") (("1" (INST? :WHERE -5) (("1" (ASSERT) NIL))))))))))) ("2" (USE "gcd_decomp") (("2" (SKOLEM!) (("2" (REPLACE -1) (("2" (EXPAND "E") (("2" (INST + "1 - n!1 * q!1" "-m!1 * q!1") (("2" (ASSERT) NIL))))))))))))))))))))))))) (|gcd_divides2| "" (SKOLEM!) (("" (REWRITE "gcd_commutes") (("" (REWRITE "gcd_divides1") NIL))))) (|greatest_common_divisor| "" (SKOSIMP) (("" (AUTO-REWRITE "divides_sum" "divides_prod1" "divides_prod2") (("" (USE "gcd_decomp") (("" (SKOLEM!) (("" (REPLACE*) (("" (ASSERT) NIL))))))))))) (|gcd_def| "" (SKOLEM!) (("" (AUTO-REWRITE "gcd_divides1" "gcd_divides2" "mutual_divisors_nat") (("" (LEMMA "greatest_common_divisor" ("a" "a!1" "b" "b!1")) (("" (GROUND) (("1" (REPLACE -1 + RL) (("1" (ASSERT) NIL))) ("2" (REPLACE -1 + RL) (("2" (ASSERT) NIL))) ("3" (REPLACE*) NIL) ("4" (INST - "gcd(a!1, b!1)") (("4" (INST - "d!1") (("4" (ASSERT) (("4" (ASSERT) NIL))))))))))))))) (|gcd_self| "" (SKOLEM!) (("" (AUTO-REWRITE "divides_reflexive") (("" (REWRITE "gcd_def") (("" (SKOSIMP) NIL))))))) (|gcd_opp1| "" (AUTO-REWRITE "opposite_divides" "divides_opposite" "gcd_divides1" "gcd_divides2" "greatest_common_divisor") (("" (SKOLEM!) (("" (REWRITE "gcd_def") (("" (SKOSIMP) (("" (ASSERT) NIL))))))))) (|gcd_opp2| "" (SKOLEM!) (("" (REWRITE "gcd_commutes") (("" (REWRITE "gcd_opp1") (("" (REWRITE "gcd_commutes") NIL))))))) (|gcd_one1| "" (AUTO-REWRITE "one_divides" "one_div_one" "gcd_def") (("" (SKOLEM!) (("" (ASSERT) (("" (SKOSIMP) NIL))))))) (|gcd_one2| "" (SKOLEM!) (("" (REWRITE "gcd_commutes") (("" (REWRITE "gcd_one1") NIL))))) (|gcd_rule1| "" (AUTO-REWRITE "gcd_divides1" "gcd_divides2" "divides_sum" "divides_prod1" "divides_prod2") (("" (SKOSIMP) (("" (ASSERT) (("" (REWRITE "gcd_def") (("" (SKOSIMP) (("" (USE "gcd_decomp") (("" (SKOLEM!) (("" (REPLACE*) (("" (CASE "divides(x!2, (b!1 * x!1 + a!1) - b!1 * x!1)") (("1" (ASSERT) NIL) ("2" (REWRITE "divides_diff") (("2" (ASSERT) NIL))))))))))))))))))))) (|gcd_rule2| "" (SKOSIMP) (("" (NAME-REPLACE "d!1" "gcd(a!1, b!1)" :HIDE? NIL) (("" (REWRITE "gcd_commutes" +) (("" (USE "gcd_rule1") (("" (REWRITE "gcd_commutes" -2) (("" (ASSERT) NIL))))))))))) (|gcd_multiple1| "" (AUTO-REWRITE "divides_reflexive" "divides_prod1" "divides_prod2" "gcd_def") (("" (SKOLEM!) (("" (ASSERT) (("" (SKOSIMP) NIL))))))) (|gcd_multiple2| "" (SKOLEM!) (("" (REWRITE "gcd_commutes") (("" (REWRITE "gcd_multiple1") NIL))))) (|gcd_multiple3| "" (AUTO-REWRITE "divides_reflexive") (("" (SKOLEM!) (("" (REWRITE "gcd_def") (("" (GROUND) (("" (SKOSIMP) NIL))))))))) (|gcd_multiple4| "" (SKOLEM!) (("" (REWRITE "gcd_commutes") (("" (REWRITE "gcd_multiple3") NIL))))) (|gcd_bound1| "" (SKOLEM!) (("" (USE "gcd_divides1") (("" (FORWARD-CHAIN "divisor_smaller") (("" (ASSERT) NIL))))))) (|gcd_bound2| "" (SKOLEM!) (("" (REWRITE "gcd_commutes") (("" (REWRITE "gcd_bound1") NIL)))))) \$\$\$mutual_primes.pvs mutual_primes : THEORY BEGIN IMPORTING common_divisor a, b, c: VAR nzint d: VAR posnat n, m: VAR int prime(a, b): bool = gcd(a, b) = 1 mutual_primes_commutes: LEMMA prime(a, b) IFF prime(b, a) mutual_primes_equiv: LEMMA prime(a, b) IFF EXISTS n, m: a * n + b * m = 1 common_div_of_primes: LEMMA prime(a, b) AND divides(d, a) AND divides(d, b) IMPLIES d=1 mutual_primes_equiv2: LEMMA prime(a, b) IFF (FORALL d: divides(d, a) AND divides(d, b) IMPLIES d=1) divides_prod_prime1: LEMMA divides(c, a * b) AND prime(a, c) IMPLIES divides(c, b) divides_prod_prime2: LEMMA divides(c, a * b) AND prime(b, c) IMPLIES divides(c, a) common_multiple_primes: LEMMA divides(a, c) AND divides(b, c) AND prime(a, b) IMPLIES divides(a * b, c) mutual_prime_prod: LEMMA prime(a * b, c) IFF prime(a, c) AND prime(b, c) END mutual_primes \$\$\$mutual_primes.prf (|mutual_primes| (|mutual_primes_commutes| "" (SKOLEM!) (("" (EXPAND "prime") (("" (REWRITE "gcd_commutes") (("" (ASSERT) NIL))))))) (|mutual_primes_equiv| "" (SKOLEM!) (("" (EXPAND "prime") (("" (GROUND) (("1" (USE "gcd_decomp") (("1" (SKOLEM!) (("1" (INST?) (("1" (ASSERT) NIL))))))) ("2" (REWRITE "gcd_def") (("2" (AUTO-REWRITE "one_divides" "divides_sum" "divides_prod1" "divides_prod2") (("2" (ASSERT) (("2" (SKOSIMP*) (("2" (CASE "divides(x!1, a!1 * n!1 + b!1 * m!1)") (("1" (ASSERT) NIL) ("2" (ASSERT) (("2" (ASSERT) NIL))))))))))))))))))) (|common_div_of_primes| "" (AUTO-REWRITE "prime" "one_div_one") (("" (SKOSIMP) (("" (USE "greatest_common_divisor" ("b" "b!1")) (("" (ASSERT) (("" (REPLACE*) (("" (ASSERT) NIL))))))))))) (|mutual_primes_equiv2| "" (AUTO-REWRITE "one_divides" "prime" "gcd_def" "one_div_one") (("" (SKOLEM!) (("" (ASSERT) NIL))))) (|divides_prod_prime1| "" (AUTO-REWRITE "mutual_primes_equiv" "divides_sum" "divides_diff" "divides_prod1" "divides_prod2" "divides_reflexive") (("" (SKOSIMP) (("" (ASSERT) (("" (SKOLEM!) (("" (CASE "divides(c!1, b!1 * (a!1 * n!1 + c!1 * m!1))") (("1" (REPLACE*) NIL) ("2" (ASSERT) NIL))))))))))) (|divides_prod_prime2| "" (SKOSIMP) (("" (USE "divides_prod_prime1" ("a" "b!1" "b" "a!1")) (("" (ASSERT) NIL))))) (|common_multiple_primes| "" (SKOSIMP) (("" (EXPAND "divides" -1) (("" (SKOLEM!) (("" (REPLACE*) (("" (ASSERT) (("" (FORWARD-CHAIN "divides_prod_prime1") (("" (REWRITE "divides_prod_elim1") NIL))))))))))))) (|mutual_prime_prod| "" (SKOLEM!) (("" (GROUND) (("1" (AUTO-REWRITE "mutual_primes_equiv") (("1" (ASSERT) (("1" (SKOLEM!) (("1" (INST + "n!1 * b!1" "m!1") (("1" (ASSERT) NIL))))))))) ("2" (AUTO-REWRITE "mutual_primes_equiv") (("2" (ASSERT) (("2" (SKOLEM!) (("2" (INST + "n!1 * a!1" "m!1") (("2" (ASSERT) NIL))))))))) ("3" (REWRITE "mutual_primes_equiv2" +) (("3" (SKOSIMP) (("3" (CASE "prime(a!1, d!1)") (("1" (FORWARD-CHAIN "divides_prod_prime1") (("1" (FORWARD-CHAIN "common_div_of_primes") NIL))) ("2" (EXPAND "prime" +) (("2" (DELETE -2 -3) (("2" (AUTO-REWRITE "gcd_divides1" "gcd_divides2") (("2" (USE "common_div_of_primes" ("d" "gcd(a!1, d!1)")) (("2" (ASSERT) (("2" (USE "divides_transitive" ("m" "d!1")) (("2" (ASSERT) NIL)))))))))))))))))))))))) \$\$\$prime_numbers.pvs prime_numbers : THEORY BEGIN IMPORTING mutual_primes a: VAR nzint x, d: VAR posnat i, n: VAR nat %-------------------------------------- % Definition and first prime numbers %-------------------------------------- prime(x): bool = x /= 1 AND FORALL d: divides(d, x) IMPLIES d=x OR d=1 two_is_prime: LEMMA prime(2) three_is_prime: LEMMA prime(3) smallest_prime: LEMMA prime(x) IMPLIES 2 <= x %------------------------- % Type of prime numbers %------------------------- prime_nat: NONEMPTY_TYPE = { x | 2 <= x AND prime(x) } %% JUDGEMENT prime_nat SUBTYPE_OF nzint p, q: VAR prime_nat %----------------- % Simple lemmas %----------------- divisors_of_prime: LEMMA divides(d, p) IFF d=p OR d=1 gcd_with_prime: LEMMA gcd(a, p) = 1 OR gcd(a, p) = p non_multiple_of_prime: LEMMA divides(p, a) OR prime(p, a) smaller_than_prime: LEMMA x < p IMPLIES prime(x, p) distinct_primes: LEMMA p /= q IMPLIES prime(p, q) %-------------------------------------------- % There are infinitely many prime numbers %-------------------------------------------- IMPORTING product_nat prime_divisor: LEMMA FORALL n: 2 <= n IMPLIES EXISTS p: divides(p, n) factorial(x): posnat = prod(1, x)(lambda i: i) divisor_factorial: LEMMA d <= x IMPLIES divides(d, factorial(x)) unbounded_primes: LEMMA FORALL x: EXISTS p: x < p END prime_numbers \$\$\$prime_numbers.prf (|prime_numbers| (|two_is_prime| "" (EXPAND "prime") (("" (SKOSIMP) (("" (FORWARD-CHAIN "divisor_smaller") (("1" (ASSERT) NIL) ("2" (ASSERT) NIL))))))) (|three_is_prime| "" (EXPAND "prime") (("" (SKOSIMP) (("" (FORWARD-CHAIN "divisor_smaller") (("1" (ASSERT) NIL) ("2" (CASE-REPLACE "d!1=2") (("1" (EXPAND "divides") (("1" (PROPAX) NIL))) ("2" (ASSERT) NIL))))))))) (|smallest_prime| "" (GRIND) NIL) (|prime_nat_TCC1| "" (INST + "2") (("" (REWRITE "two_is_prime") NIL))) (SUBTYPE_TCC1 "" (SUBTYPE-TCC) NIL) (|divisors_of_prime| "" (AUTO-REWRITE "divides_reflexive" "one_divides" "prime") (("" (SKOLEM-TYPEPRED) (("" (ASSERT) (("" (REDUCE) NIL))))))) (|gcd_with_prime| "" (SKOSIMP) (("" (USE "gcd_divides2") (("" (REWRITE "divisors_of_prime") (("" (GROUND) NIL))))))) (|non_multiple_of_prime| "" (SKOSIMP) (("" (AUTO-REWRITE "gcd_multiple4" "prime") (("" (LEMMA "gcd_with_prime" ("a" "a!1" "p" "p!1")) (("" (GROUND) (("" (REWRITE "gcd_commutes") NIL))))))))) (|smaller_than_prime| "" (SKOSIMP) (("" (REWRITE "mutual_primes_commutes") (("" (USE "non_multiple_of_prime") (("" (ASSERT) (("" (FORWARD-CHAIN "divisor_smaller") (("1" (ASSERT) NIL) ("2" (ASSERT) NIL))))))))))) (|distinct_primes| "" (SKOSIMP) (("" (USE "non_multiple_of_prime") (("" (ASSERT) (("" (REWRITE "divisors_of_prime") NIL))))))) (|prime_divisor| "" (INDUCT "n" :NAME "NAT_induction") (("" (SKOSIMP) (("" (AUTO-REWRITE "divides_reflexive") (("" (ASSERT) (("" (CASE "prime(j!1)") (("1" (INST? +) (("1" (ASSERT) NIL))) ("2" (EXPAND "prime") (("2" (SKOSIMP) (("2" (FORWARD-CHAIN "divisor_smaller") (("1" (ASSERT) NIL) ("2" (INST - "d!1") (("2" (ASSERT) (("2" (SKOLEM!) (("2" (INST + "p!1") (("2" (FORWARD-CHAIN "divides_transitive") NIL))))))))))))))))))))))))) (|factorial_TCC1| "" (SUBTYPE-TCC) NIL) (|factorial_TCC2| "" (SKOLEM!) (("" (REWRITE "prod_positive") NIL))) (|divisor_factorial| "" (CASE "FORALL d, n: d <= n+1 IMPLIES divides(d, factorial(n+1))") (("1" (SKOSIMP) (("1" (INST?) (("1" (ASSERT) NIL))))) ("2" (DELETE 2) (("2" (EXPAND "factorial") (("2" (NAME-REPLACE "u!1" "lambda i:i" :HIDE? NIL) (("2" (INDUCT-AND-REWRITE "n" 1 "prod_once" "prod_step" "divides_prod1" "divides_prod2" "divides_reflexive" "one_div_one") (("1" (REPLACE -2 + RL) (("1" (ASSERT) NIL))) ("2" (CASE-REPLACE "d!1 = u!1(2 + j!1)") (("1" (ASSERT) NIL) ("2" (REPLACE -2 + RL) (("2" (ASSERT) NIL))))))))))))))) (|unbounded_primes| "" (SKOLEM!) (("" (USE "prime_divisor" ("n" "factorial(x!1) + 1")) (("" (GROUND) (("" (SKOLEM!) (("" (INST?) (("" (USE "divisor_factorial") (("" (ASSERT) (("" (USE "divides_diff" ("n" "1 + factorial(x!1)" "m" "factorial(x!1)")) (("" (AUTO-REWRITE "one_div_one") (("" (USE "smallest_prime") (("" (ASSERT) NIL)))))))))))))))))))))) \$\$\$index_range.pvs index_range : THEORY BEGIN i, n, m: VAR nat idx(n, m): TYPE = {i | n <= i AND i <= m} END index_range \$\$\$nat_fun_props.pvs nat_fun_props : THEORY BEGIN n, m : VAR nat injection_n_to_m : THEOREM (EXISTS (f : [below(n) -> below(m)]) : injective?(f)) IMPLIES n <= m surjection_n_to_m : THEOREM (EXISTS (f : [below(n) -> below(m)]) : surjective?(f)) IMPLIES m <= n bijection_n_to_m : THEOREM (EXISTS (f : [below(n) -> below(m)]) : bijective?(f)) IFF n = m injection_n_to_m2: THEOREM (EXISTS (f : [upto(n) -> upto(m)]) : injective?(f)) IFF n <= m surjection_n_to_m2: THEOREM (EXISTS (f : [upto(n) -> upto(m)]) : surjective?(f)) IFF m <= n bijection_n_to_m2: THEOREM (EXISTS (f : [upto(n) -> upto(m)]) : bijective?(f)) IFF n = m surj_equiv_inj: THEOREM FORALL (f : [below(n) -> below(n)]) : surjective?(f) IFF injective?(f) inj_equiv_bij: THEOREM FORALL (f : [below(n) -> below(n)]) : bijective?(f) IFF injective?(f) surj_equiv_bij: THEOREM FORALL (f : [below(n) -> below(n)]) : bijective?(f) IFF surjective?(f) surj_equiv_inj2: THEOREM FORALL (f : [upto(n) -> upto(n)]) : surjective?(f) IFF injective?(f) inj_equiv_bij2: THEOREM FORALL (f : [upto(n) -> upto(n)]) : bijective?(f) IFF injective?(f) surj_equiv_bij2: THEOREM FORALL (f : [upto(n) -> upto(n)]) : bijective?(f) IFF surjective?(f) END nat_fun_props \$\$\$nat_fun_props.prf (|nat_fun_props| (|injection_n_to_m| "" (INDUCT "n") (("1" (ASSERT) NIL) ("2" (SKOSIMP*) (("2" (TYPEPRED "f!1(0)") (("2" (ASSERT) (("2" (HIDE -1) (("2" (INST -1 "m!1 - 1") (("2" (ASSERT) (("2" (DELETE 2) (("2" (INST + "LAMBDA (x : below(j!1)) : IF f!1(x) = m!1 - 1 THEN f!1(j!1) ELSE f!1(x) ENDIF") (("1" (EXPAND "injective?") (("1" (SKOSIMP) (("1" (LIFT-IF) (("1" (LIFT-IF) (("1" (INST-CP -2 "x1!1" "j!1") (("1" (INST-CP -2 "x2!1" "j!1") (("1" (INST -2 "x1!1" "x2!1") (("1" (ASSERT) (("1" (ASSERT) NIL))))))))))))))))) ("2" (SKOSIMP) (("2" (ASSERT) NIL))) ("3" (SKOSIMP) (("3" (EXPAND "injective?") (("3" (INST -2 "x!1" "j!1") (("3" (ASSERT) NIL))))))))))))))))))))))))) (|surjection_n_to_m| "" (SKOSIMP*) (("" (REWRITE "injection_n_to_m") (("" (EXPAND "surjective?") (("" (INST -1 "0") (("" (SKOSIMP) (("" (ASSERT) (("" (INST 1 "inverse(f!1)") (("1" (REWRITE "inj_inv") (("1" (INST 1 "x!1") NIL))) ("2" (INST 1 "x!1") NIL))))))))))))))) (|bijection_n_to_m| "" (SKOLEM!) (("" (PROP) (("1" (EXPAND "bijective?") (("1" (SKOSIMP) (("1" (LEMMA "injection_n_to_m" ("n" "n!1" "m" "m!1")) (("1" (LEMMA "surjection_n_to_m" ("n" "n!1" "m" "m!1")) (("1" (SPLIT) (("1" (ASSERT) (("1" (INST?) NIL))) ("2" (INST?) NIL))))))))))) ("2" (INST 1 "LAMBDA (x : below(n!1)) : x") (("1" (GRIND) NIL) ("2" (SKOLEM!) (("2" (ASSERT) NIL))))))))) (|injection_n_to_m2| "" (SKOLEM!) (("" (GROUND) (("1" (LEMMA "injection_n_to_m" ("n" "n!1+1" "m" "m!1+1")) (("1" (ASSERT) (("1" (SKOLEM!) (("1" (INST + "lambda (i : below(1 + n!1)) : f!1(i)") (("1" (GRIND :IF-MATCH NIL) (("1" (INST? :WHERE +) (("1" (ASSERT) NIL))))) ("2" (SKOLEM!) (("2" (ASSERT) NIL))))))))))) ("2" (INST + "lambda (i : upto(n!1)): i") (("2" (GRIND) NIL))))))) (|surjection_n_to_m2| "" (SKOLEM!) (("" (GROUND) (("1" (LEMMA "surjection_n_to_m" ("n" "n!1+1" "m" "m!1+1")) (("1" (ASSERT) (("1" (SKOLEM!) (("1" (INST + "lambda (i: below(1 + n!1)): f!1(i)") (("1" (GRIND :IF-MATCH NIL) (("1" (INST? -) (("1" (SKOLEM!) (("1" (INST?) NIL))))))) ("2" (SKOLEM!) (("2" (ASSERT) NIL))))))))))) ("2" (INST + "lambda (i : upto(n!1)): IF i <= m!1 THEN i ELSE 0 ENDIF") (("2" (GRIND) NIL))))))) (|bijection_n_to_m2| "" (SKOLEM!) (("" (GROUND) (("1" (EXPAND "bijective?") (("1" (SKOSIMP) (("1" (LEMMA "injection_n_to_m2" ("n" "n!1" "m" "m!1")) (("1" (LEMMA "surjection_n_to_m2" ("n" "n!1" "m" "m!1")) (("1" (GROUND) (("1" (INST?) NIL) ("2" (INST?) NIL))))))))))) ("2" (INST + "lambda (i : upto(n!1)): i") (("2" (GRIND) NIL))))))) (|surj_equiv_inj| "" (SKOLEM!) (("" (CASE "n!1 = 0") (("1" (GRIND) NIL) ("2" (GROUND) (("1" (USE "surjection_n_to_m" ("n" "n!1 - 1" "m" "n!1")) (("1" (ASSERT) (("1" (EXPAND* "surjective?" "injective?") (("1" (SKOSIMP) (("1" (INST + "lambda (i : below(n!1 - 1)): IF i < x1!1 THEN f!1(i) ELSE f!1(i+1) ENDIF") (("1" (ASSERT) (("1" (SKOLEM!) (("1" (INST - "y!1") (("1" (SKOLEM!) (("1" (CASE "x!1 = x1!1") (("1" (INST + "IF x2!1 < x!1 THEN x2!1 ELSE x2!1-1 ENDIF") (("1" (LIFT-IF) (("1" (ASSERT) NIL))) ("2" (GROUND) NIL) ("3" (GROUND) NIL))) ("2" (INST + "IF x!1 < x1!1 THEN x!1 ELSE x!1 - 1 ENDIF") (("1" (LIFT-IF) (("1" (ASSERT) NIL))) ("2" (GROUND) NIL) ("3" (GROUND) NIL))))))))))))))))))))))) ("2" (USE "injection_n_to_m" ("n" "n!1" "m" "n!1-1")) (("2" (ASSERT) (("2" (EXPAND* "injective?" "surjective?") (("2" (SKOLEM!) (("2" (INST + "lambda (i : below(n!1)) : IF f!1(i) = n!1 - 1 THEN y!1 ELSE f!1(i) ENDIF") (("1" (ASSERT) (("1" (SKOSIMP) (("1" (INST? - :WHERE +) (("1" (LIFT-IF) (("1" (LIFT-IF) (("1" (GROUND) (("1" (INST?) NIL) ("2" (INST + "x2!1") (("2" (ASSERT) NIL))))))))))))))) ("2" (SKOSIMP) (("2" (ASSERT) NIL))) ("3" (SKOSIMP) (("3" (INST? +) (("3" (ASSERT) NIL))))))))))))))))))))) (|inj_equiv_bij| "" (SKOLEM!) (("" (EXPAND "bijective?") (("" (GROUND) (("" (REWRITE "surj_equiv_inj") NIL))))))) (|surj_equiv_bij| "" (SKOLEM!) (("" (EXPAND "bijective?") (("" (GROUND) (("" (REWRITE "surj_equiv_inj") NIL))))))) (|surj_equiv_inj2| "" (SKOLEM!) (("" (LEMMA "surj_equiv_inj" ("n" "n!1+1" "f" "lambda (i : below(n!1 + 1)): f!1(i)")) (("1" (EXPAND* "surjective?" "injective?") (("1" (REDUCE :IF-MATCH NIL) (("1" (INST? -4 :WHERE +) (("1" (ASSERT) NIL))) ("2" (INST? -2) (("2" (SKOLEM!) (("2" (INST? +) NIL))))) ("3" (INST - "y!1") (("3" (SKOLEM!) (("3" (INST + "x!1") NIL))))) ("4" (INST? - :WHERE +) (("4" (ASSERT) NIL))))))) ("2" (SKOLEM!) (("2" (ASSERT) NIL))))))) (|inj_equiv_bij2| "" (SKOLEM!) (("" (EXPAND "bijective?") (("" (GROUND) (("" (REWRITE "surj_equiv_inj2") NIL))))))) (|surj_equiv_bij2| "" (SKOLEM!) (("" (EXPAND "bijective?") (("" (GROUND) (("" (REWRITE "surj_equiv_inj2") NIL)))))))) \$\$\$iterations.pvs iterations [ T : TYPE ] : THEORY BEGIN IMPORTING nat_fun_props, index_range f : VAR [T, T -> T] u, v: VAR [nat -> T] n, m, p, q, i, j, k: VAR nat x, y, z, t: VAR T %-------------------------------------------- % Iterated application of f to u(n)...u(m) %-------------------------------------------- iter(f, n, (m | n <= m), u): RECURSIVE T = IF n=m THEN u(n) ELSE f(iter(f, n, m-1, u), u(m)) ENDIF MEASURE m iter_once: LEMMA iter(f, n, n, u) = u(n) iter_induct: LEMMA FORALL n, (m | n <= m): iter(f, n, m + 1, u) = f(iter(f, n, m, u), u(m + 1)) iter_same_elements: LEMMA FORALL n, (m | n <= m): (FORALL i: n <= i AND i <= m IMPLIES u(i) = v(i)) IMPLIES iter(f, n, m, u) = iter(f, n, m, v) % New proof; measure-induct does not work anymore iter_same_elements2: LEMMA FORALL n, (m | n <= m): (FORALL i: n <= i AND i <= m IMPLIES u(i) = v(i)) IMPLIES iter(f, n, m, u) = iter(f, n, m, v) %---------------------------------------- % Iteration of an associative function %---------------------------------------- g : VAR { f | associative?(f) } associativity: LEMMA g(x, g(y, z)) = g(g(x, y), z) iter_assoc_split: LEMMA n <= m AND m < p IMPLIES g(iter(g, n, m, u), iter(g, m + 1, p, u)) = iter(g, n, p, u) %-------------------------------------------------------- % Iteration of an associative and commutative function %-------------------------------------------------------- h : VAR { g | commutative?(g) } commutativity: LEMMA h(x, y) = h(y, x) commut_assoc1: LEMMA h(h(x, y), h(z, t)) = h(h(x, z), h(y, t)) commut_assoc2: LEMMA h(h(x, y), z) = h(h(z, y), x) %-------------------------------------------- % iteration on h(u(n),v(n))...h(u(m),v(m)) %-------------------------------------------- iter_split: LEMMA FORALL n, (m | n <= m): iter(h, n, m, lambda i: h(u(i), v(i))) = h(iter(h, n, m, u), iter(h, n, m, v)) %------------------------------------------- % Invariance if two elements are swapped %------------------------------------------- swap(u, n, m)(i): T = IF i=m THEN u(n) ELSIF i=n THEN u(m) ELSE u(i) ENDIF swap_unchanged: LEMMA swap(u, n, n) = u swap_commutes: LEMMA swap(u, n, m) = swap(u, m, n) swap_inverse: LEMMA swap(swap(u, n, m), n, m) = u iter_swap_first_last: LEMMA n <= m IMPLIES iter(h, n, m, swap(u, n, m)) = iter(h, n, m, u) iter_swap_last: LEMMA n <= i AND i <= m IMPLIES iter(h, n, m, swap(u, i, m)) = iter(h, n, m, u) iter_swap: LEMMA n <= i AND i <= j AND j <= m IMPLIES iter(h, n, m, swap(u, i, j)) = iter(h, n, m, u) %-------------------------------------------- % IF u[n..m] is a permutation of v[p..q] % then iter(h, n, m, u) = iter(h, p, q, v) %-------------------------------------------- permutation(u, n, m, v, p, q): bool = EXISTS (a: [idx(n, m) -> idx(p, q)]): bijective?(a) AND FORALL (i: idx(n, m)): u(i) = v(a(i)) perm_range: LEMMA n <= m AND permutation(u, n, m, v, p, q) IMPLIES m - n = q - p perm_equiv: LEMMA permutation(u, n, n+m, v, p, p+m) IFF EXISTS (a: [idx(n, n+m) -> idx(p, p+m)]): injective?(a) AND FORALL (i: idx(n, n+m)): u(i) = v(a(i)) iter_permutation: LEMMA permutation(u, n, n + m, v, p, p + m) IMPLIES iter(h, n, n + m, u) = iter(h, p, p + m, v) iter_permutation2: LEMMA n <= m AND permutation(u, n, m, v, p, q) IMPLIES iter(h, n, m, u) = iter(h, p, q, v) iter_permutation3: LEMMA FORALL (a : [idx(n, n + m) -> idx(p, p + m)]): injective?(a) AND (FORALL (i: idx(n, n + m)): u(i) = v(a(i))) IMPLIES iter(h, n, n + m, u) = iter(h, p, p + m, v) END iterations \$\$\$iterations.prf (|iterations| (|iter_TCC1| "" (SUBTYPE-TCC) NIL) (|iter_TCC2| "" (TERMINATION-TCC) NIL) (|iter_TCC3| "" (TERMINATION-TCC) NIL) (|iter_once_TCC1| "" (SUBTYPE-TCC) NIL) (|iter_once| "" (GRIND) NIL) (|iter_induct_TCC1| "" (SUBTYPE-TCC) NIL) (|iter_induct| "" (GRIND) NIL) (|iter_same_elements| "" (SKOSIMP) (("" (CASE "FORALL (x: nat): n!1 + x <= m!1 IMPLIES iter(f!1, n!1, n!1 + x, u!1) = iter(f!1, n!1, n!1 + x, v!1)") (("1" (INST - "m!1 - n!1") (("1" (ASSERT) NIL))) ("2" (DELETE 2) (("2" (INDUCT-AND-SIMPLIFY "x") NIL))))))) (|iter_same_elements2| "" (AUTO-REWRITE "iter") (("" (SKOLEM + ("f!1" "u!1" "v!1" "n!1" _)) (("" (MEASURE-INDUCT "m - n!1" ("m")) (("" (SKOSIMP*) (("" (CASE "x!1 = n!1") (("1" (ASSERT) (("1" (INST?) (("1" (ASSERT) NIL))))) ("2" (ASSERT) (("2" (INST? -1) (("2" (GROUND) (("1" (INST?) (("1" (ASSERT) NIL))) ("2" (SKOSIMP) (("2" (INST?) (("2" (ASSERT) NIL))))))))))))))))))))) (|associativity| "" (SKOLEM-TYPEPRED) (("" (EXPAND "associative?") (("" (INST?) (("" (ASSERT) NIL))))))) (|iter_assoc_split_TCC1| "" (SUBTYPE-TCC) NIL) (|iter_assoc_split_TCC2| "" (SUBTYPE-TCC) NIL) (|iter_assoc_split_TCC3| "" (SUBTYPE-TCC) NIL) (|iter_assoc_split| "" (SKOLEM 1 ("g!1" "m!1" "n!1" _ "u!1")) (("" (AUTO-REWRITE "iter") (("" (INDUCT "p") (("1" (SKOSIMP) (("1" (ASSERT) NIL))) ("2" (SKOSIMP) (("2" (CASE "m!1 < j!1") (("1" (ASSERT) (("1" (REWRITE "associativity" 1) (("1" (ASSERT) NIL))))) ("2" (ASSERT) NIL))))) ("3" (SKOSIMP) (("3" (ASSERT) NIL))) ("4" (SKOSIMP) (("4" (ASSERT) NIL))) ("5" (SKOSIMP) NIL))))))) (|commutativity| "" (GRIND) NIL) (|commut_assoc1| "" (SKOLEM!) (("" (NAME-REPLACE "x!2" "h!1(h!1(x!1, z!1), h!1(y!1, t!1))" :HIDE? NIL) (("" (REWRITE "associativity") (("" (REWRITE "associativity") (("" (REWRITE "associativity" :DIR RL) (("" (REWRITE "associativity" :DIR RL +) (("" (USE "commutativity" ("x" "z!1" "y" "y!1")) (("" (ASSERT) NIL))))))))))))))) (|commut_assoc2| "" (SKOLEM!) (("" (USE "commutativity" ("x" "z!1" "y" "y!1")) (("" (USE "commutativity" ("x" "x!1" "y" "y!1")) (("" (REPLACE*) (("" (DELETE -) (("" (REWRITE "associativity" :DIR RL) (("" (REWRITE "associativity" :DIR RL) (("" (USE "commutativity" ("x" "x!1" "y" "z!1")) (("" (ASSERT) NIL))))))))))))))))) (|iter_split| "" (SKOSIMP) (("" (CASE "FORALL (x: nat): iter(h!1, n!1, n!1 + x, lambda i: h!1(u!1(i), v!1(i))) = h!1(iter(h!1, n!1, n!1 + x, u!1), iter(h!1, n!1, n!1 + x, v!1))") (("1" (INST - "m!1 - n!1") (("1" (ASSERT) NIL))) ("2" (DELETE 2) (("2" (AUTO-REWRITE "iter") (("2" (INDUCT "x") (("1" (ASSERT) NIL) ("2" (SKOSIMP) (("2" (ASSERT) (("2" (REPLACE*) (("2" (REWRITE "commut_assoc1") NIL))))))))))))))))) (|swap_unchanged| "" (SKOLEM!) (("" (APPLY-EXTENSIONALITY :HIDE? T) (("" (GRIND) NIL))))) (|swap_commutes| "" (SKOLEM!) (("" (APPLY-EXTENSIONALITY :HIDE? T) (("" (GRIND) NIL))))) (|swap_inverse| "" (SKOLEM!) (("" (APPLY-EXTENSIONALITY :HIDE? T) (("" (GRIND) NIL))))) (|iter_swap_first_last| "" (SKOSIMP) (("" (ASSERT) (("" (CASE-REPLACE "m!1 = n!1") (("1" (REWRITE "swap_unchanged") NIL) ("2" (AUTO-REWRITE "iter_once" "iter" "swap") (("2" (ASSERT) (("2" (CASE-REPLACE "m!1 - 1 = n!1") (("1" (ASSERT) (("1" (REWRITE "commutativity") NIL))) ("2" (STOP-REWRITE "iter") (("2" (USE "iter_assoc_split" ("m" "n!1" "u" "u!1")) (("2" (USE "iter_assoc_split" ("m" "n!1" "u" "swap(u!1, n!1, m!1)")) (("2" (ASSERT) (("2" (REPLACE -1 + RL) (("2" (REPLACE -2 + RL) (("2" (DELETE -1 -2) (("2" (CASE-REPLACE "iter(h!1, 1 + n!1, m!1 - 1, swap(u!1, n!1, m!1)) = iter(h!1, 1 + n!1, m!1 - 1, u!1)") (("1" (REWRITE "commut_assoc2") NIL) ("2" (REWRITE "iter_same_elements") (("2" (DELETE 2 5) (("2" (REDUCE) NIL))))))))))))))))))))))))))))))))) (|iter_swap_last_TCC1| "" (SUBTYPE-TCC) NIL) (|iter_swap_last| "" (SKOSIMP) (("" (AUTO-REWRITE "iter_swap_first_last") (("" (CASE-REPLACE "i!1 = n!1") (("1" (ASSERT) NIL) ("2" (ASSERT) (("2" (USE "iter_assoc_split" ("m" "i!1 - 1" "u" "swap(u!1, i!1, m!1)")) (("2" (USE "iter_assoc_split" ("m" "i!1 - 1" "u" "u!1")) (("2" (ASSERT) (("2" (CASE-REPLACE "iter(h!1, n!1, i!1 - 1, swap(u!1, i!1, m!1)) = iter(h!1, n!1, i!1 - 1, u!1)") (("1" (ASSERT) NIL) ("2" (REWRITE "iter_same_elements") (("2" (DELETE -1 -2 2 4) (("2" (GRIND) NIL))))))))))))))))))))) (|iter_swap_TCC1| "" (SUBTYPE-TCC) NIL) (|iter_swap| "" (SKOSIMP) (("" (AUTO-REWRITE "iter_swap_last") (("" (CASE-REPLACE "j!1 = m!1") (("1" (ASSERT) NIL) ("2" (USE "iter_assoc_split" ("m" "j!1" "u" "swap(u!1, i!1, j!1)")) (("2" (USE "iter_assoc_split" ("m" "j!1" "u" "u!1")) (("2" (ASSERT) (("2" (CASE-REPLACE "iter(h!1, 1 + j!1, m!1, swap(u!1, i!1, j!1)) = iter(h!1, 1+j!1, m!1, u!1)") (("1" (ASSERT) NIL) ("2" (REWRITE "iter_same_elements") (("2" (DELETE -1 -2 2 4) (("2" (GRIND) NIL))))))))))))))))))) (|perm_range| "" (EXPAND "permutation") (("" (SKOSIMP*) (("" (ASSERT) (("" (TYPEPRED "a!1(n!1)") (("" (ASSERT) (("" (DELETE -1 -2 -3 -5) (("" (REWRITE "bijection_n_to_m2" :DIR RL) (("" (INST + "lambda (i : upto(m!1 - n!1)): a!1(n!1 + i) - p!1") (("1" (GRIND :IF-MATCH NIL) (("1" (INST -3 "p!1 + y!1") (("1" (SKOLEM!) (("1" (INST + "x!1 - n!1") (("1" (ASSERT) NIL))))))) ("2" (INST -3 "n!1 + x1!1" "n!1 + x2!1") (("2" (ASSERT) NIL))))) ("2" (SKOSIMP) (("2" (GROUND) NIL))))))))))))))))))) (|perm_equiv| "" (SKOSIMP) (("" (EXPAND "permutation") (("" (EXPAND "bijective?") (("" (GROUND) (("1" (SKOSIMP) (("1" (INST?) (("1" (ASSERT) NIL))))) ("2" (SKOSIMP) (("2" (INST?) (("2" (GROUND) (("2" (DELETE -2) (("2" (USE "surj_equiv_inj2" ("n" "m!1" "f" "lambda (i : upto(m!1)): a!1(i + n!1) - p!1")) (("1" (GRIND :IF-MATCH NIL) (("1" (INST - "y!1 - p!1") (("1" (SKOLEM!) (("1" (INST? +) (("1" (ASSERT) NIL))))))) ("2" (INST - "n!1 + x1!1" "n!1 + x2!1") (("2" (ASSERT) NIL))))) ("2" (SKOSIMP) (("2" (GROUND) NIL))))))))))))))))))))) (|iter_permutation_TCC1| "" (SUBTYPE-TCC) NIL) (|iter_permutation_TCC2| "" (SUBTYPE-TCC) NIL) (|iter_permutation| "" (SKOLEM 1 ("h!1" _ "n!1" "p!1" _ _)) (("" (AUTO-REWRITE "iter" "swap") (("" (INDUCT "m") (("1" (SKOSIMP) (("1" (EXPAND "permutation") (("1" (SKOSIMP) (("1" (ASSERT) (("1" (INST?) (("1" (ASSERT) NIL))))))))))) ("2" (AUTO-REWRITE "perm_equiv") (("2" (SKOSIMP*) (("2" (ASSERT) (("2" (SKOSIMP) (("2" (INST - "u!1" "swap(v!1, a!1(1 + j!1 + n!1), j!1 + 1 + p!1)") (("2" (GROUND) (("1" (USE "iter_swap_last" ("n" "p!1" "i" "a!1(1 + j!1 + n!1)" "m" "1 + j!1 + p!1")) (("1" (ASSERT) (("1" (REPLACE -1 + RL) (("1" (DELETE -1) (("1" (INST?) (("1" (ASSERT) NIL))))))))))) ("2" (DELETE 2) (("2" (INST + "lambda (i : idx(n!1, j!1+n!1)): IF a!1(i) = 1 + j!1 + p!1 THEN a!1(1 + j!1 + n!1) ELSE a!1(i) ENDIF") (("1" (GROUND) (("1" (DELETE -2) (("1" (EXPAND "injective?") (("1" (SKOSIMP) (("1" (INST-CP - "x1!1" "x2!1") (("1" (INST-CP - "x1!1" "1+j!1+n!1") (("1" (INST - "x2!1" "1+j!1+n!1") (("1" (ASSERT) (("1" (LIFT-IF) (("1" (LIFT-IF) (("1" (GROUND) NIL))))))))))))))))))) ("2" (SKOLEM!) (("2" (LIFT-IF) (("2" (GROUND) (("1" (INST?) (("1" (ASSERT) (("1" (EXPAND "swap") (("1" (LIFT-IF) (("1" (GROUND) NIL))))))))) ("2" (INST?) (("2" (EXPAND "injective?") (("2" (INST - "i!1" "1 + j!1 + n!1") (("2" (ASSERT) (("2" (ASSERT) NIL))))))))))))))))) ("2" (SKOSIMP) (("2" (GROUND) NIL))) ("3" (SKOSIMP) (("3" (GROUND) (("3" (EXPAND "injective?") (("3" (INST - "i!1" "1 + j!1 + n!1") (("3" (ASSERT) NIL))))))))))))))))))))))))))))))) (|iter_permutation2_TCC1| "" (SUBTYPE-TCC) NIL) (|iter_permutation2_TCC2| "" (SKOSIMP) (("" (FORWARD-CHAIN "perm_range") (("" (ASSERT) NIL))))) (|iter_permutation2| "" (SKOSIMP) (("" (FORWARD-CHAIN "perm_range") (("" (ASSERT) (("" (USE "iter_permutation" ("m" "m!1 - n!1" "p" "p!1" "v" "v!1")) (("" (ASSERT) NIL))))))))) (|iter_permutation3_TCC1| "" (SUBTYPE-TCC) NIL) (|iter_permutation3_TCC2| "" (SUBTYPE-TCC) NIL) (|iter_permutation3| "" (SKOSIMP) (("" (REWRITE "iter_permutation") (("" (REWRITE "perm_equiv") (("" (INST?) (("" (ASSERT) NIL)))))))))) \$\$\$product_nat.pvs product_nat : THEORY BEGIN IMPORTING iterations i, j, n, m, p, q: VAR nat u, v : VAR [nat -> nat] x, y, z: VAR nat f : VAR [nat, nat -> nat] mult : { f | associative?(f) AND commutative?(f) } = lambda i, j: i * j prod(n, (m | n <= m))(u): nat = iter(mult, n, m, u) prod_once: LEMMA prod(n, n)(u) = u(n) prod_step: LEMMA n <= m IMPLIES prod(n, m+1)(u) = prod(n, m)(u) * u(m+1) prod_same_elements: LEMMA n <= m AND (FORALL (i : idx(n, m)) : u(i) = v(i)) IMPLIES prod(n, m)(u) = prod(n, m)(v) prod_split: LEMMA n <= m AND m < p IMPLIES prod(n, m)(u) * prod(m+1, p)(u) = prod(n, p)(u) prod_split2: LEMMA n <= m IMPLIES prod(n, m)(lambda i : u(i) * v(i)) = prod(n, m)(u) * prod(n, m)(v) prod_permutation: LEMMA permutation(u, n, n + m, v, p, p + m) IMPLIES prod(n, n + m)(u) = prod(p, p + m)(v) prod_const: LEMMA prod(n, n + m)(lambda i: x) = expt(x, m + 1) prod_positive: LEMMA n <= m AND (FORALL (i: idx(n, m)): u(i) > 0) IMPLIES prod(n, m)(u) > 0 prod_null: LEMMA n <= m AND (EXISTS (i: idx(n, m)): u(i) = 0) IMPLIES prod(n, m)(u) = 0 END product_nat \$\$\$product_nat.prf (|product_nat| (|mult_TCC1| "" (SUBTYPE-TCC) NIL) (|prod_once_TCC1| "" (SUBTYPE-TCC) NIL) (|prod_once| "" (GRIND) NIL) (|prod_step_TCC1| "" (SUBTYPE-TCC) NIL) (|prod_step| "" (AUTO-REWRITE "prod" "iter_induct[nat]" "mult") (("" (SKOSIMP) (("" (ASSERT) NIL))))) (|prod_same_elements_TCC1| "" (SUBTYPE-TCC) NIL) (|prod_same_elements| "" (EXPAND "prod") (("" (SKOSIMP) (("" (REWRITE "iter_same_elements") (("" (DELETE 2) (("" (SKOSIMP) (("" (INST?) (("" (ASSERT) NIL))))))))))))) (|prod_split_TCC1| "" (SUBTYPE-TCC) NIL) (|prod_split_TCC2| "" (SUBTYPE-TCC) NIL) (|prod_split_TCC3| "" (SUBTYPE-TCC) NIL) (|prod_split| "" (SKOSIMP) (("" (EXPAND "prod") (("" (REWRITE "mult" :DIR RL) (("" (USE "iter_assoc_split[nat]") (("" (ASSERT) NIL))))))))) (|prod_split2| "" (SKOSIMP) (("" (AUTO-REWRITE "prod" "mult") (("" (ASSERT) (("" (USE "iter_split" ("u" "u!1" "v" "v!1")) (("" (ASSERT) NIL))))))))) (|prod_permutation_TCC1| "" (SUBTYPE-TCC) NIL) (|prod_permutation_TCC2| "" (SUBTYPE-TCC) NIL) (|prod_permutation| "" (SKOSIMP) (("" (EXPAND "prod") (("" (REWRITE "iter_permutation") NIL))))) (|prod_const_TCC1| "" (SUBTYPE-TCC) NIL) (|prod_const| "" (SKOLEM + (_ "n!1" "x!1")) (("" (INDUCT-AND-REWRITE "m" 1 "prod_once" "prod_step" "expt") NIL))) (|prod_positive_TCC1| "" (SUBTYPE-TCC) NIL) (|prod_positive| "" (SKOSIMP) (("" (CASE "FORALL i: i <= m!1 - n!1 IMPLIES prod(n!1, n!1 + i)(u!1) > 0") (("1" (INST - "m!1 -n!1") (("1" (ASSERT) NIL) ("2" (ASSERT) NIL))) ("2" (DELETE 2) (("2" (INDUCT-AND-REWRITE "i" 1 "prod_once" "prod_step" "pos_times_gt") NIL))))))) (|prod_null_TCC1| "" (SUBTYPE-TCC) NIL) (|prod_null| "" (SKOSIMP*) (("" (EXPAND "prod") (("" (ASSERT) (("" (USE "iter_swap_last[nat]" ("i" "i!1")) (("" (ASSERT) (("" (REPLACE -1 + RL) (("" (DELETE -1) (("" (AUTO-REWRITE "iter" "mult" "swap") (("" (CASE "n!1 = m!1") (("1" (ASSERT) NIL) ("2" (ASSERT) NIL)))))))))))))))))))) \$\$\$fermat.pvs fermat : THEORY BEGIN IMPORTING product_nat, prime_numbers, modulo_arithmetic, product_modulo a : VAR posnat n : VAR {a | 2 <= a} i, j: VAR nat p: VAR prime_nat F(n): posnat = prod(1, n - 1)(lambda i: i) G(n, a): nat = prod(1, n - 1)(lambda i: rem(n)(a * i)) %--------------------- % G(n, a) modulo n %--------------------- decomp_G: LEMMA rem(n)(G(n, a)) = rem(n)(expt(a, n - 1) * F(n)) %------------------------------------------------ % G(n, a) = F(n) if n and a are mutually prime %------------------------------------------------ div_diff_mod: LEMMA FORALL (x, y: mod(n)): divides(n, x - y) IFF x= y aux_prop: LEMMA prime(a, n) IMPLIES FORALL (x, y: mod(n)): rem(n)(a * x) = rem(n)(a * y) IFF x=y equal_products: LEMMA prime(a, n) IMPLIES G(n, a) = F(n) %------------------------------------- % (p - 1)! and p are mutually prime %------------------------------------- fact_prime: LEMMA prime(F(p), p) %-------------------------- % Fermat little theorem %-------------------------- fermat_theorem1: LEMMA prime(a, p) IMPLIES divides(p, expt(a, p - 1) - 1) fermat_theorem2: LEMMA prime(a, p) IMPLIES rem(p)(expt(a, p - 1)) = 1 fermat_theorem3: LEMMA rem(p)(expt(a, p)) = rem(p)(a) END fermat \$\$\$fermat.prf (|fermat| (F_TCC1 "" (SUBTYPE-TCC) NIL) (F_TCC2 "" (SKOLEM!) (("" (REWRITE "prod_positive") NIL))) (|decomp_G_TCC1| "" (SUBTYPE-TCC) NIL) (|decomp_G| "" (SKOLEM!) (("" (EXPAND "G") (("" (CASE-REPLACE "rem(n!1)(prod(1, n!1 - 1)(LAMBDA (i: nat): rem(n!1)(a!1 * i))) = rem(n!1)(prod(1, n!1 -1)(lambda i: a!1 * i))") (("1" (REWRITE "prod_split2") (("1" (REWRITE "F" :DIR RL) (("1" (USE "prod_const" ("m" "n!1 - 2")) (("1" (ASSERT) NIL))))))) ("2" (DELETE 2) (("2" (REWRITE "equivalent_product") (("2" (AUTO-REWRITE "rem_rem") (("2" (SKOLEM!) (("2" (ASSERT) NIL))))))))))))))) (|div_diff_mod| "" (SKOLEM!) (("" (GROUND) (("1" (FORWARD-CHAIN "divisor_smaller") (("1" (ASSERT) NIL) ("2" (ASSERT) NIL) ("3" (REWRITE "divides_opposite" :DIR RL) (("3" (ASSERT) (("3" (FORWARD-CHAIN "divisor_smaller") (("1" (ASSERT) NIL) ("2" (ASSERT) NIL))))))))) ("2" (REPLACE*) (("2" (ASSERT) (("2" (REWRITE "divides_zero") NIL))))))))) (|aux_prop_TCC1| "" (SUBTYPE-TCC) NIL) (|aux_prop| "" (SKOSIMP*) (("" (GROUND) (("" (REWRITE "same_remainder") (("" (USE "divides_prod_prime1" ("b" "x!1 - y!1")) (("" (ASSERT) (("" (REWRITE "div_diff_mod") NIL))))))))))) (|equal_products| "" (SKOSIMP) (("" (EXPAND "G") (("" (EXPAND "F") (("" (ASSERT) (("" (USE "prod_permutation" ("m" "n!1 - 2")) (("" (GROUND) (("" (DELETE 2) (("" (USE "perm_equiv[nat]" ("m" "n!1 - 2")) (("" (ASSERT) (("" (DELETE 2) (("" (FORWARD-CHAIN "aux_prop") (("" (INST + "lambda (i: idx(1, n!1 - 1)): rem(n!1)(a!1 * i)") (("1" (GROUND) (("1" (EXPAND "injective?") (("1" (SKOSIMP) (("1" (INST?) (("1" (ASSERT) NIL))))))))) ("2" (SKOSIMP) (("2" (INST - "0" "i!1") (("2" (AUTO-REWRITE "rem_zero") (("2" (ASSERT) (("2" (GROUND) NIL))))))))))))))))))))))))))))))))) (|fact_prime_TCC1| "" (SUBTYPE-TCC) NIL) (|fact_prime| "" (SKOLEM!) (("" (EXPAND "F") (("" (NAME-REPLACE "u!1" "lambda i: i" :HIDE? NIL) (("" (CASE "FORALL (j: nat): j <= p!1 - 2 IMPLIES prod(1, 1 + j)(u!1) > 0 AND prime(prod(1, 1 + j)(u!1), p!1)") (("1" (INST - "p!1-2") (("1" (ASSERT) NIL) ("2" (TYPEPRED "p!1") (("2" (DELETE 2) (("2" (EXPAND "prime") (("2" (ASSERT) NIL))))))))) ("2" (DELETE 2) (("2" (INDUCT-AND-REWRITE "j" 1 "prod_once" "prod_step" "pos_times_gt" "smaller_than_prime") (("1" (REPLACE -2 + RL) (("1" (ASSERT) NIL))) ("2" (REPLACE -2 + RL) (("2" (ASSERT) NIL))) ("3" (REWRITE "mutual_prime_prod") (("1" (REPLACE -4 + RL) (("1" (ASSERT) NIL))) ("2" (REPLACE -4 + RL) (("2" (ASSERT) NIL))))) ("4" (REPLACE -4 + RL) (("4" (ASSERT) NIL))))))) ("3" (SKOSIMP) (("3" (ASSERT) NIL))))))))))) (|fermat_theorem1_TCC1| "" (SUBTYPE-TCC) NIL) (|fermat_theorem1| "" (AUTO-REWRITE "fact_prime" "equal_products" "fact_prime_TCC1") (("" (SKOSIMP) (("" (USE "decomp_G" ("n" "p!1")) (("" (ASSERT) (("" (ASSERT) (("" (REWRITE "same_remainder") (("" (USE "divides_prod_prime1" ("a" "F(p!1)" "b" "1 - expt(a!1, p!1 - 1)")) (("1" (ASSERT) (("1" (REWRITE "divides_opposite" :DIR RL +) NIL))) ("2" (ASSERT) NIL))))))))))))))) (|fermat_theorem2| "" (AUTO-REWRITE "rem_one") (("" (SKOSIMP :PREDS? T) (("" (EXPAND "prime" -3) (("" (GROUND) (("" (DELETE -1 -2 -3 1) (("" (FORWARD-CHAIN "fermat_theorem1") (("" (REWRITE "same_remainder" :DIR RL) NIL))))))))))))) (|fermat_theorem3| "" (SKOLEM!) (("" (USE "non_multiple_of_prime" ("p" "p!1" "a" "a!1")) (("" (GROUND) (("1" (REWRITE "rem_expt1" :DIR RL) (("1" (AUTO-REWRITE "expt" "zero_times1" "rem_zero") (("1" (CASE-REPLACE "rem(p!1)(a!1) = 0") (("1" (ASSERT) NIL) ("2" (REWRITE "rem_def2") NIL))))))) ("2" (REWRITE "mutual_primes_commutes") (("2" (EXPAND "expt") (("2" (REWRITE "rem_prod2" :DIR RL) (("2" (REWRITE "fermat_theorem2") (("2" (ASSERT) NIL))))))))))))))))