%Patch files loaded: patch2 version 2.417 % patch2-test version 1.929 \$\$\$newtop.pvs newtop : THEORY BEGIN IMPORTING fermat, prime_decomposition, chinese_remainder END newtop \$\$\$posnat_induction.pvs posnat_induction : THEORY BEGIN n: VAR posnat P: VAR [posnat -> bool] posnat_induction: PROPOSITION P(1) AND (FORALL n: P(n) => P(n+1)) IMPLIES (FORALL n: P(n)) END posnat_induction \$\$\$posnat_induction.prf (|posnat_induction| (|posnat_induction| "" (SKOSIMP) (("" (CASE "FORALL (i: nat): P!1(i+1)") (("1" (SKOLEM!) (("1" (INST - "n!1 - 1") (("1" (ASSERT) NIL))))) ("2" (DELETE 2) (("2" (INDUCT "i") (("1" (ASSERT) NIL) ("2" (SKOSIMP) (("2" (INST - "j!1+1") (("2" (ASSERT) NIL)))))))))))))) \$\$\$chinese_remainder.pvs chinese_remainder : THEORY BEGIN IMPORTING modulo_arithmetic, posnat_induction, product_nat p, q: VAR nzint p1, q1: VAR posnat a, b, x, y: VAR int %------------------ % Simple version %------------------ chinese_remainder1: LEMMA prime(p, q) IMPLIES EXISTS x: divides(p, x - a) AND divides(q, x - b) chinese_remainder2: LEMMA prime(p1, q1) IMPLIES EXISTS x: rem(p1)(x) = rem(p1)(a) AND rem(q1)(x) = rem(q1)(b) chinese_remainder3: LEMMA prime(p1, q1) IMPLIES FORALL (a : mod(p1)), (b: mod(q1)): EXISTS (x: mod(p1 * q1)): rem(p1)(x) = a AND rem(q1)(x) = b equal_remainders: LEMMA prime(p1, q1) IMPLIES (rem(p1 * q1)(x) = rem(p1 * q1)(y) IFF rem(p1)(x) = rem(p1)(y) AND rem(q1)(x) = rem(q1)(y)) %--------------------------------------------- % Same property with p(0)...p(n-1) numbers %--------------------------------------------- n: VAR posnat mutual_primes(n): TYPE = { x: [below(n) -> posnat] | FORALL (i, j: below(n)): i /= j => prime(x(i), x(j)) } chinese_remainder: PROPOSITION FORALL n, (p: mutual_primes(n)), (a: [i:below(n) -> mod(p(i))]): EXISTS (x: mod(prod(n)(p))): FORALL (i: below(n)): rem(p(i))(x) = a(i) prime_partial_product: LEMMA FORALL n, (p: mutual_primes(n)): prime(prod(n-1)(lambda (i: below(n-1)): p(i)), p(n-1)) equal_remainders2: PROPOSITION FORALL n, (p: mutual_primes(n)): rem(prod(n)(p))(x) = rem(prod(n)(p))(y) IFF (FORALL (i: below(n)): rem(p(i))(x) = rem(p(i))(y)) END chinese_remainder \$\$\$chinese_remainder.prf (|chinese_remainder| (|chinese_remainder1| "" (SKOSIMP) (("" (REWRITE "mutual_primes_equiv") (("" (SKOLEM!) (("" (CASE "divides(p!1, q!1 * m!1 - 1) AND divides(q!1, p!1 * n!1 - 1)") (("1" (GROUND) (("1" (NAME-REPLACE "AA" "q!1 * m!1 - 1" :HIDE? NIL) (("1" (NAME-REPLACE "BB" "p!1 * n!1 - 1" :HIDE? NIL) (("1" (AUTO-REWRITE "divides_reflexive" "divides_prod1" "divides_prod2" "divides_sum") (("1" (INST + "a!1 * q!1 * m!1 + b!1 * p!1 * n!1") (("1" (SPLIT) (("1" (CASE-REPLACE "a!1 * m!1 * q!1 - a!1 + b!1 * n!1 * p!1 = a!1 * AA + b!1 * n!1 * p!1") (("1" (ASSERT) (("1" (ASSERT) NIL))) ("2" (REPLACE -2 + RL) (("2" (ASSERT) NIL))))) ("2" (CASE-REPLACE "a!1 * m!1 * q!1 - b!1 + b!1 * n!1 * p!1 = a!1 * m!1 * q!1 + b!1 * BB") (("1" (ASSERT) (("1" (ASSERT) NIL))) ("2" (ASSERT) NIL))))))))))))))) ("2" (DELETE 2) (("2" (EXPAND "divides") (("2" (GROUND) (("1" (INST + "-n!1") (("1" (ASSERT) NIL))) ("2" (INST + "-m!1") (("2" (ASSERT) NIL))))))))))))))))) (|chinese_remainder2| "" (SKOSIMP) (("" (REWRITE "mutual_primes_equiv") (("" (SKOLEM!) (("" (AUTO-REWRITE "rem_multiple1" "rem_multiple2" "rem_rem" "rem_zero") (("" (INST + "a!1 * (q1!1 * m!1) + b!1 * (p1!1 * n!1)") (("" (SPLIT) (("1" (CASE-REPLACE "q1!1 * m!1 = 1 - p1!1 * n!1") (("1" (ASSERT) (("1" (REWRITE "rem_sum1" :DIR RL) (("1" (REWRITE "rem_diff2" :DIR RL) (("1" (REWRITE "rem_prod2" :DIR RL) (("1" (ASSERT) NIL))))))))) ("2" (ASSERT) NIL))) ("2" (CASE-REPLACE "p1!1 * n!1 = 1 - q1!1 * m!1") (("1" (ASSERT) (("1" (REWRITE "rem_sum1" :DIR RL) (("1" (REWRITE "rem_diff2" :DIR RL) (("1" (REWRITE "rem_prod2" :DIR RL) (("1" (ASSERT) NIL))))))))) ("2" (ASSERT) NIL))))))))))))))) (|chinese_remainder3| "" (SKOSIMP*) (("" (AUTO-REWRITE "rem_mod") (("" (USE "chinese_remainder2" ("a" "a!1" "b" "b!1")) (("" (GROUND) (("" (SKOSIMP) (("" (NAME "y!1" "rem(p1!1 * q1!1)(x!1)") (("" (INST + "y!1") (("" (AUTO-REWRITE "rem_def") (("" (GROUND) (("1" (DELETE -3 -4) (("1" (SKOSIMP*) (("1" (INST + "q!2 - q!1 * q1!1") (("1" (ASSERT) NIL))))))) ("2" (DELETE -2 -4) (("2" (SKOSIMP*) (("2" (INST + "q!2 - q!1 * p1!1") (("2" (ASSERT) NIL))))))))))))))))))))))))) (|equal_remainders| "" (SKOSIMP) (("" (AUTO-REWRITE "same_remainder" "divides_zero" "common_multiple_primes") (("" (GROUND) (("1" (EXPAND "divides") (("1" (SKOLEM!) (("1" (INST + "x!2 * q1!1") (("1" (ASSERT) NIL))))))) ("2" (EXPAND "divides") (("2" (SKOLEM!) (("2" (INST + "x!2 * p1!1") (("2" (ASSERT) NIL))))))) ("3" (CASE-REPLACE "x!1 - y!1 = 0") (("1" (ASSERT) NIL) ("2" (ASSERT) NIL))))))))) (|chinese_remainder_TCC1| "" (SKOSIMP) (("" (REWRITE "variant_prod_posnat") NIL))) (|chinese_remainder| "" (AUTO-REWRITE "rem_mod" "mutual_prime_prod") (("" (INDUCT "n" :NAME "posnat_induction") (("1" (SKOSIMP*) (("1" (INST + "a!1(0)") (("1" (SKOLEM!) (("1" (ASSERT) (("1" (ASSERT) NIL))))) ("2" (REWRITE "variant_prod_one") (("2" (ASSERT) NIL))))))) ("2" (SKOSIMP*) (("2" (ASSERT) (("2" (TYPEPRED "p!1") (("2" (USE "chinese_remainder3" ("p1" "p!1(n!1)" "q1" "p!1(n!1-1)")) (("2" (INST-CP -2 "n!1" "n!1-1") (("2" (GROUND) (("2" (INST - "a!1(n!1)" "a!1(n!1-1)") (("2" (SKOSIMP) (("2" (ASSERT) (("2" (INST -5 "lambda (i: below(n!1)): IF i nat] a,b,c: VAR bag n: VAR nat insert(x,b) : bag = (LAMBDA t: IF x = t THEN b(t) + 1 ELSE b(t) ENDIF) purge(x,b) : bag = (LAMBDA t: IF x = t THEN 0 ELSE b(t) ENDIF) delete(x,b,n) : bag = (LAMBDA t: IF x = t THEN IF b(t) >= n THEN b(t) - n ELSE 0 ENDIF ELSE b(t) ENDIF) plus(a,b) : bag = (LAMBDA t: a(t) + b(t)) union(a,b) : bag = (LAMBDA t: max(a(t),b(t))) intersection(a,b): bag = (LAMBDA t: min(a(t),b(t))) % --------- some predicates over bags ------------ member(x,b) : bool = b(x) > 0 empty?(b) : bool = (FORALL x: b(x) = 0) nonempty_bag?(b) : bool = NOT empty?(b) eqmult(x,a,b) : bool = (a(x) = b(x)) subbag?(a,b) : bool = (FORALL x: a(x) <= b(x)) proper_subbag?(a,b): bool = subbag?(a, b) AND a /= b disjoint?(a, b) : bool = empty?(intersection(a, b)) END bags \$\$\$bags.prf (|bags| (|delete_TCC1| "" (SUBTYPE-TCC) NIL)) \$\$\$inductive_bags.pvs inductive_bags [T : TYPE] : THEORY BEGIN IMPORTING bags S, U, V: VAR bag[T] x, y, z: VAR T i, j, n, m: VAR nat %------------------------------------- % Finite bags: inductive definition %------------------------------------- indbag(S): INDUCTIVE bool = empty?(S) OR (EXISTS x, U: indbag(U) AND S = insert(x, U)) finite_bag: NONEMPTY_TYPE = (indbag) A, B, C: VAR finite_bag P, Q: VAR [finite_bag -> bool] emptybag: finite_bag = LAMBDA x: 0 JUDGEMENT insert HAS_TYPE [T, finite_bag -> finite_bag] %---------------------------- % Basic properties of bags %---------------------------- emptybag_is_empty: LEMMA empty?(S) IFF S = emptybag subbag_emptybag: LEMMA subbag?(S, emptybag) IFF S = emptybag subbag_insert: LEMMA subbag?(insert(x, S), insert(x, U)) IFF subbag?(S, U) subbag_insert2: LEMMA subbag?(S, U) IMPLIES subbag?(S, insert(x, U)) subbag_insert3: LEMMA subbag?(insert(x, S), U) IMPLIES subbag?(S, U) insert_not_empty: LEMMA not insert(x, S) = emptybag insert_or_empty: LEMMA empty?(S) OR (EXISTS x, U: S = insert(x, U)) insert_exchange: LEMMA insert(x, insert(y, S)) = insert(y, insert(x, S)) equal_insert: LEMMA insert(x, S) = insert(y, U) IFF (x = y AND S = U) OR (EXISTS V: S = insert(y, V) AND U = insert(x, V)) remove_element: LEMMA S(x) > 0 IFF EXISTS U: S = insert(x, U) insert_finite: LEMMA indbag(insert(x, S)) IFF indbag(S) equal_insert_finite: LEMMA insert(x, A) = insert(y, B) IFF (x = y AND A = B) OR (EXISTS C: A = insert(y, C) AND B = insert(x, C)) insert_or_empty_finite: LEMMA A = emptybag OR (EXISTS x, B: A = insert(x, B)) remove_element_finite: LEMMA A(x) > 0 IFF EXISTS B: A = insert(x, B) %----------------------------- % Induction for finite bags %----------------------------- bag_induction: PROPOSITION P(emptybag) AND (FORALL x, A: P(A) IMPLIES P(insert(x, A))) IMPLIES FORALL A: P(A) %------------------------------------------- % Closure under intersection, union, etc. %------------------------------------------- finite_bag_plus: LEMMA indbag(plus(A, B)) finite_bag_subbag: LEMMA subbag?(S, A) IMPLIES indbag(S) finite_bag_union: LEMMA indbag(union(A, B)) finite_bag_intersection: LEMMA indbag(intersection(A, B)) JUDGEMENT plus, union, intersection HAS_TYPE [finite_bag, finite_bag -> finite_bag] %------------- % Cardinal %------------- Card(A, n): INDUCTIVE bool = (A = emptybag AND n = 0) OR (EXISTS x, B, m: Card(B, m) AND A = insert(x, B) AND n = m + 1) Card_emptybag: LEMMA Card(emptybag, n) IFF n = 0 Card_insert: LEMMA Card(insert(x, A), n) IFF n > 0 AND Card(A, n-1) Card_unique: LEMMA Card(A, n) AND Card(A, m) IMPLIES n = m Card_total: LEMMA FORALL A: EXISTS n: Card(A, n) %--------------------- % derived function %--------------------- card(A): { n | Card(A, n) } card_def: LEMMA card(A) = n IFF Card(A, n) card_emptybag: LEMMA card(emptybag) = 0 card_zero: LEMMA card(A) = 0 IFF A = emptybag card_insert: LEMMA card(insert(x, A)) = card(A) + 1 card_positive: LEMMA card(A) > 0 IFF EXISTS x, B: A = insert(x, B) %----------------------------------- % Lemma for induction on cardinal %----------------------------------- card_induction: LEMMA (FORALL n, A: card(A) = n IMPLIES P(A)) IMPLIES (FORALL A: P(A)) END inductive_bags \$\$\$inductive_bags.prf (|inductive_bags| (|finite_bag_TCC1| "" (INST + "LAMBDA x: 0") (("" (EXPAND "indbag") (("" (EXPAND "empty?") (("" (PROPAX) NIL))))))) (|emptybag_TCC1| "" (EXPAND* "indbag" "empty?") NIL) (|insert_TCC1| "" (SKOLEM!) (("" (EXPAND "indbag") (("" (GROUND) (("" (INST?) (("" (ASSERT) NIL))))))))) (|emptybag_is_empty| "" (GRIND) (("" (APPLY-EXTENSIONALITY :HIDE? T) (("" (INST?) NIL))))) (|subbag_emptybag| "" (GRIND) (("" (APPLY-EXTENSIONALITY :HIDE? T) (("" (INST?) (("" (ASSERT) NIL))))))) (|subbag_insert| "" (GRIND :IF-MATCH NIL) (("1" (INST?) (("1" (LIFT-IF) (("1" (GROUND) NIL))))) ("2" (INST?) (("2" (ASSERT) NIL))) ("3" (INST?) NIL))) (|subbag_insert2| "" (GRIND) NIL) (|subbag_insert3| "" (GRIND) NIL) (|insert_not_empty| "" (SKOLEM!) (("" (REWRITE "emptybag_is_empty" :DIR RL) (("" (GRIND) NIL))))) (|insert_or_empty| "" (GRIND :IF-MATCH NIL) (("" (INST + "x!1" "lambda y: IF y=x!1 THEN S!1(x!1)-1 ELSE S!1(y) ENDIF") (("" (APPLY-EXTENSIONALITY :HIDE? T :FNUM 2) (("" (LIFT-IF) (("" (GROUND) NIL))))))))) (|insert_exchange| "" (SKOLEM!) (("" (APPLY-EXTENSIONALITY :HIDE? T) (("" (GRIND) NIL))))) (|equal_insert| "" (SKOLEM!) (("" (SPLIT) (("1" (FLATTEN) (("1" (CASE "x!1 = y!1") (("1" (DELETE 2) (("1" (GROUND) (("1" (APPLY-EXTENSIONALITY :HIDE? T) (("1" (CASE "insert(x!1, S!1)(x!2) = insert(y!1, U!1)(x!2)") (("1" (DELETE -3) (("1" (GRIND) NIL))) ("2" (ASSERT) NIL))))))))) ("2" (ASSERT) (("2" (DELETE 2) (("2" (INST + "lambda z: IF z=y!1 THEN U!1(z) ELSE S!1(z) ENDIF") (("2" (GROUND) (("1" (APPLY-EXTENSIONALITY :HIDE? T) (("1" (CASE "insert(x!1, S!1)(x!2) = insert(y!1, U!1)(x!2)") (("1" (GRIND) NIL) ("2" (ASSERT) NIL))))) ("2" (APPLY-EXTENSIONALITY :HIDE? T) (("2" (CASE "insert(x!1, S!1)(x!2) = insert(y!1, U!1)(x!2)") (("1" (GRIND) NIL) ("2" (ASSERT) NIL))))))))))))))))) ("2" (GROUND) (("2" (SKOSIMP) (("2" (REPLACE*) (("2" (REWRITE "insert_exchange") NIL))))))))))) (|remove_element| "" (GRIND :IF-MATCH NIL) (("" (INST + "lambda x: IF x=x!1 THEN S!1(x!1)-1 ELSE S!1(x) ENDIF") (("" (APPLY-EXTENSIONALITY :HIDE? T) (("" (LIFT-IF) (("" (ASSERT) NIL))))))))) (|insert_finite| "" (SKOLEM!) (("" (GROUND) (("1" (LEMMA "indbag_induction" ("P" "lambda S: FORALL x, U: S=insert(x, U) IMPLIES indbag(U)")) (("1" (AUTO-REWRITE "emptybag_is_empty" "insert_not_empty") (("1" (GROUND) (("1" (REDUCE) NIL) ("2" (DELETE -1 2) (("2" (REDUCE :IF-MATCH NIL) (("2" (REWRITE "equal_insert") (("2" (EXPAND "indbag" +) (("2" (REDUCE :IF-MATCH NIL) (("2" (INST?) (("2" (INST + "x!3" "V!1") (("2" (ASSERT) NIL))))))))))))))))))))) ("2" (EXPAND "indbag" +) (("2" (GROUND) (("2" (INST?) (("2" (ASSERT) NIL))))))))))) (|equal_insert_finite| "" (SKOLEM!) (("" (SPLIT) (("1" (FLATTEN) (("1" (REWRITE "equal_insert") (("1" (SPLIT -) (("1" (PROPAX) NIL) ("2" (DELETE 1) (("2" (SKOSIMP) (("2" (USE "insert_finite") (("2" (ASSERT) (("2" (INST?) (("2" (ASSERT) NIL))))))))))))))))) ("2" (GROUND) (("2" (SKOSIMP) (("2" (REWRITE "equal_insert") (("2" (FLATTEN) (("2" (INST?) (("2" (ASSERT) NIL))))))))))))))) (|insert_or_empty_finite| "" (SKOSIMP) (("" (AUTO-REWRITE "emptybag_is_empty") (("" (USE "insert_or_empty") (("" (ASSERT) (("" (SKOLEM!) (("" (USE "insert_finite") (("" (ASSERT) (("" (INST?) NIL))))))))))))))) (|remove_element_finite| "" (SKOLEM!) (("" (REWRITE "remove_element") (("" (GROUND) (("1" (SKOLEM!) (("1" (USE "insert_finite") (("1" (ASSERT) (("1" (INST?) NIL))))))) ("2" (SKOLEM!) (("2" (INST?) NIL))))))))) (|bag_induction| "" (SKOSIMP) (("" (LEMMA "indbag_induction" ("P" "LAMBDA S: indbag(S) AND P!1(S)")) (("" (GROUND) (("1" (SKOLEM!) (("1" (INST - "A!1") (("1" (ASSERT) NIL))))) ("2" (DELETE 2) (("2" (SKOSIMP) (("2" (AUTO-REWRITE "emptybag_is_empty" "insert_not_empty") (("2" (SPLIT -) (("1" (ASSERT) NIL) ("2" (SKOSIMP) (("2" (INST?) (("2" (GROUND) NIL))))))))))))))))))) (|finite_bag_plus| "" (SKOLEM 1 ("A!1" _)) (("" (INDUCT "B" :NAME "bag_induction") (("1" (CASE-REPLACE "plus(A!1, emptybag) = A!1") (("1" (ASSERT) NIL) ("2" (DELETE 2) (("2" (APPLY-EXTENSIONALITY :HIDE? T) (("2" (GRIND) NIL))))))) ("2" (SKOSIMP) (("2" (CASE-REPLACE "plus(A!1, insert(x!1, A!2)) = insert(x!1, plus(A!1, A!2))") (("1" (REWRITE "insert_finite") NIL) ("2" (DELETE -1 2) (("2" (APPLY-EXTENSIONALITY :HIDE? T) (("2" (GRIND) NIL))))))))))))) (|finite_bag_subbag| "" (INDUCT "A" :NAME "bag_induction") (("1" (AUTO-REWRITE "subbag_emptybag") (("1" (SKOSIMP) (("1" (ASSERT) NIL))))) ("2" (SKOSIMP*) (("2" (CASE "S!1(x!1) > 0") (("1" (REWRITE "remove_element") (("1" (AUTO-REWRITE "subbag_insert") (("1" (REDUCE :IF-MATCH NIL) (("1" (INST - "U!1") (("1" (EXPAND "indbag" +) (("1" (REDUCE) NIL))))))))))) ("2" (INST?) (("2" (GROUND) (("2" (DELETE 3) (("2" (GRIND :IF-MATCH NIL) (("2" (INST?) (("2" (LIFT-IF) (("2" (GROUND) NIL))))))))))))))))))) (|finite_bag_union| "" (SKOLEM!) (("" (AUTO-REWRITE "finite_bag_plus") (("" (USE "finite_bag_subbag" ("A" "plus(A!1, B!1)")) (("" (GROUND) (("" (DELETE 2) (("" (GRIND) NIL))))))))))) (|finite_bag_intersection| "" (SKOLEM!) (("" (USE "finite_bag_subbag") (("" (ASSERT) (("" (DELETE 2) (("" (GRIND) NIL))))))))) (|plus_TCC1| "" (LEMMA "finite_bag_plus") (("" (PROPAX) NIL))) (|union_TCC1| "" (LEMMA "finite_bag_union") (("" (PROPAX) NIL))) (|intersection_TCC1| "" (LEMMA "finite_bag_intersection") (("" (PROPAX) NIL))) (|Card_emptybag| "" (SKOLEM!) (("" (EXPAND "Card") (("" (GROUND) (("" (SKOSIMP) (("" (USE "insert_not_empty") (("" (ASSERT) NIL))))))))))) (|Card_insert_TCC1| "" (SUBTYPE-TCC) NIL) (|Card_insert| "" (CASE "FORALL A, n, x: Card(insert(x, A), n) IMPLIES n > 0 AND Card(A, n-1)") (("1" (SKOLEM!) (("1" (INST?) (("1" (SPLIT +) (("1" (PROPAX) NIL) ("2" (DELETE -) (("2" (GROUND) (("2" (EXPAND "Card" +) (("2" (INST + "x!1" "A!1" "n!1-1") (("2" (GROUND) NIL))))))))))))))) ("2" (DELETE 2) (("2" (AUTO-REWRITE "equal_insert_finite" "insert_not_empty") (("2" (INDUCT "n") (("1" (EXPAND "Card") (("1" (SKOLEM!) (("1" (ASSERT) NIL))))) ("2" (SKOSIMP*) (("2" (ASSERT) (("2" (EXPAND "Card" -2) (("2" (REDUCE :IF-MATCH NIL) (("2" (INST - "C!1" "x!1") (("2" (GROUND) (("2" (EXPAND "Card" +) (("2" (INST + "x!2" "C!1" "j!1 - 1") (("2" (ASSERT) NIL))))))))))))))))) ("3" (SKOSIMP) (("3" (ASSERT) NIL))))))))) ("3" (SKOSIMP) (("3" (ASSERT) NIL))))) (|Card_unique| "" (AUTO-REWRITE "Card_emptybag" "Card_insert") (("" (INDUCT "A" :NAME "bag_induction") (("1" (SKOSIMP) (("1" (ASSERT) NIL))) ("2" (SKOSIMP*) (("2" (ASSERT) (("2" (GROUND) (("2" (INST - "n!1 - 1" "m!1 -1") (("2" (ASSERT) NIL))))))))))))) (|Card_total| "" (AUTO-REWRITE "Card_emptybag" "Card_insert") (("" (INDUCT "A" :NAME "bag_induction") (("1" (INST + "0") (("1" (ASSERT) NIL))) ("2" (SKOSIMP*) (("2" (INST + "n!1+1") (("2" (ASSERT) NIL))))))))) (|card_TCC1| "" (INST + "lambda A: epsilon! n: Card(A, n)") (("" (SKOLEM!) (("" (USE "epsilon_ax[nat]") (("" (USE "Card_total") (("" (GROUND) NIL))))))))) (|card_def| "" (SKOLEM!) (("" (GROUND) (("" (USE "Card_unique") (("" (ASSERT) NIL))))))) (|card_emptybag| "" (AUTO-REWRITE "card_def" "Card_emptybag") (("" (ASSERT) NIL))) (|card_zero| "" (SKOLEM!) (("" (GROUND) (("1" (TYPEPRED "card(A!1)") (("1" (EXPAND "Card") (("1" (PROPAX) NIL))))) ("2" (REPLACE*) (("2" (REWRITE "card_emptybag") NIL))))))) (|card_insert| "" (SKOLEM!) (("" (AUTO-REWRITE "card_def" "Card_insert") (("" (ASSERT) (("" (GROUND) NIL))))))) (|card_positive| "" (SKOLEM!) (("" (GROUND) (("1" (TYPEPRED "card(A!1)") (("1" (EXPAND "Card") (("1" (SKOSIMP) (("1" (INST?) NIL))))))) ("2" (SKOLEM!) (("2" (REPLACE*) (("2" (REWRITE "card_insert") (("2" (ASSERT) NIL))))))))))) (|card_induction| "" (REDUCE) NIL)) \$\$\$inductive_bag_functions.pvs inductive_bag_functions [ T, U: TYPE] : THEORY BEGIN IMPORTING inductive_bags[T] %----------------------------- % Recursion for finite bags %----------------------------- f: VAR [T, U -> U] a: VAR U x, y: VAR T exchange?(f): bool = FORALL x, y, a: f(x, f(y, a)) = f(y, f(x, a)) g: VAR (exchange?) %---------------------------------------------- % Choice function: pick an arbitrary element %---------------------------------------------- A: VAR finite_bag B: VAR { A | not empty?(A) } choose(B): { x | B(x) > 0 } rest(B): finite_bag = delete(choose(B), B, 1) insert_choose: LEMMA insert(choose(B), rest(B)) = B card_rest: LEMMA card(rest(B)) = card(B) - 1 recur(a, g)(A): RECURSIVE U = IF empty?(A) THEN a ELSE g(choose(A), recur(a, g)(rest(A))) ENDIF MEASURE card(A) %--------------------------- % The two essential rules %--------------------------- recur_emptybag: LEMMA recur(a, g)(emptybag) = a recur_insert: LEMMA recur(a, g)(insert(x, A)) = g(x, recur(a, g)(A)) END inductive_bag_functions \$\$\$inductive_bag_functions.prf (|inductive_bag_functions| (|choose_TCC1| "" (INST + "lambda B: epsilon! x: B(x) > 0") (("1" (SKOLEM!) (("1" (TYPEPRED "B!1") (("1" (DELETE -1) (("1" (EXPAND "empty?") (("1" (SKOLEM!) (("1" (USE "epsilon_ax[T]") (("1" (GROUND) (("1" (INST + "x!1") (("1" (ASSERT) NIL))))) ("2" (INST + "x!1") NIL))))))))))))) ("2" (GRIND) NIL))) (|rest_TCC1| "" (SKOLEM!) (("" (USE "finite_bag_subbag" ("A" "B!1")) (("" (GROUND) (("" (DELETE 2) (("" (GRIND) NIL))))))))) (|insert_choose| "" (SKOLEM!) (("" (APPLY-EXTENSIONALITY :HIDE? T) (("" (GRIND) NIL))))) (|card_rest| "" (SKOSIMP) (("" (USE "card_insert" ("x" "choose(B!1)" "A" "rest(B!1)")) (("" (REWRITE "insert_choose") (("" (ASSERT) NIL))))))) (|recur_TCC1| "" (AUTO-REWRITE "card_rest") (("" (SKOSIMP) (("" (ASSERT) NIL))))) (|recur_emptybag| "" (AUTO-REWRITE "recur" "emptybag_is_empty") (("" (SKOLEM!) (("" (ASSERT) NIL))))) (|recur_insert| "" (SKOLEM + (_ "a!1" "g!1" _)) (("" (MEASURE-INDUCT "card(A)" "A") (("" (SKOSIMP*) (("" (AUTO-REWRITE "card_insert" "insert_not_empty" "emptybag_is_empty") (("" (EXPAND "recur" 1 1) (("" (ASSERT) (("" (USE "insert_choose") (("" (NAME-REPLACE "zzz" "choose(insert(x!2, x!1))") (("" (NAME-REPLACE "yyy" "rest(insert(x!2, x!1))") (("" (REWRITE "equal_insert_finite") (("" (GROUND) (("" (SKOSIMP) (("" (REPLACE*) (("" (INST - "C!1") (("" (ASSERT) (("" (INST? :COPY? T) (("" (INST - "zzz") (("" (REPLACE*) (("" (TYPEPRED "g!1") (("" (EXPAND "exchange?") (("" (INST?) NIL)))))))))))))))))))))))))))))))))))))))))) \$\$\$prime_decomposition.pvs prime_decomposition : THEORY BEGIN IMPORTING prime_numbers, inductive_bag_functions[prime_nat, posnat] n, i, j: VAR nat x, y, z: VAR posnat p, p1, p2, q: VAR prime_nat A, B: VAR finite_bag[prime_nat] %-------------------------------------------------- % prime decompositions = finite bags of primes %-------------------------------------------------- prod: [finite_bag[prime_nat] -> posnat] = recur(1, lambda p, x: p * x) product_emptybag: LEMMA prod(emptybag) = 1 product_insert: LEMMA prod(insert(p, A)) = p * prod(A) product_plus: LEMMA prod(plus(A, B)) = prod(A) * prod(B) product_one: LEMMA prod(A) = 1 IFF A = emptybag %-------------------------------------------- % Existence of a prime decomposition of x %-------------------------------------------- decomposition_exists: LEMMA FORALL x: EXISTS A: prod(A) = x %---------------- % Uniqueness %---------------- product_prime: LEMMA A(p)=0 IMPLIES prime(p, prod(A)) division_product: LEMMA divides(prod(A), prod(B)) IFF subbag?(A, B) unique_decomposition: LEMMA prod(A) = prod(B) IFF A = B %------------------------------------------- % Function: posnat -> prime decomposition %------------------------------------------- prime_fact(x): { A | prod(A) = x } factorisation_def: LEMMA prime_fact(x) = A IFF prod(A) = x factors_prod: LEMMA prime_fact(prod(A)) = A factorisation_one: LEMMA prime_fact(1) = emptybag factorisation_empty: LEMMA prime_fact(x) = emptybag IFF x = 1 factorisation_prime: LEMMA prime_fact(p) = insert(p, emptybag) factorisation_prod: LEMMA prime_fact(x * y) = plus(prime_fact(x), prime_fact(y)) factorisation_divides: LEMMA divides(x, y) IFF subbag?(prime_fact(x), prime_fact(y)) factorisation_gcd: LEMMA prime_fact(gcd(x, y)) = intersection(prime_fact(x), prime_fact(y)) factorisation_primes: LEMMA prime(x, y) IFF disjoint?(prime_fact(x), prime_fact(y)) END prime_decomposition \$\$\$prime_decomposition.prf (|prime_decomposition| (|prod_TCC1| "" (GRIND) NIL) (|product_emptybag| "" (AUTO-REWRITE "recur_emptybag" "prod" "prod_TCC1") (("" (ASSERT) NIL))) (|product_insert| "" (AUTO-REWRITE "recur_insert" "prod" "prod_TCC1") (("" (ASSERT) NIL))) (|product_plus| "" (SKOLEM + ("A!1" _)) (("" (AUTO-REWRITE "product_emptybag" "product_insert") (("" (INDUCT "B" :NAME "bag_induction") (("1" (CASE-REPLACE "plus(A!1, emptybag) = A!1") (("1" (ASSERT) NIL) ("2" (DELETE 2) (("2" (APPLY-EXTENSIONALITY :HIDE? T) (("2" (AUTO-REWRITE "plus" "emptybag") (("2" (ASSERT) NIL))))))))) ("2" (SKOSIMP) (("2" (ASSERT) (("2" (CASE-REPLACE "plus(A!1, insert(x!1, A!2)) = insert(x!1, plus(A!1, A!2))") (("1" (ASSERT) NIL) ("2" (AUTO-REWRITE "plus" "insert") (("2" (DELETE -1 2) (("2" (APPLY-EXTENSIONALITY :HIDE? T) (("2" (CASE "x!2 = x!1") (("1" (ASSERT) NIL) ("2" (ASSERT) NIL))))))))))))))))))))) (|product_one| "" (SKOLEM!) (("" (AUTO-REWRITE "product_emptybag" "product_insert" "product_one") (("" (GROUND) (("1" (USE "insert_or_empty_finite") (("1" (ASSERT) (("1" (SKOLEM!) (("1" (REPLACE*) (("1" (ASSERT) NIL))))))))) ("2" (REPLACE*) (("2" (ASSERT) NIL))))))))) (|decomposition_exists| "" (MEASURE-INDUCT "x-1" "x") (("" (SKOSIMP) (("" (AUTO-REWRITE "product_insert" "product_emptybag" "divides") (("" (USE "prime_divisor" ("n" "x!1")) (("" (GROUND) (("1" (SKOSIMP*) (("1" (USE "pos_times_lt") (("1" (ASSERT) (("1" (LEMMA "both_sides_times_pos_le1" ("pz" "x!2" "x" "2" "y" "p!1")) (("1" (ASSERT) (("1" (INST - "x!2") (("1" (GROUND) (("1" (SKOLEM!) (("1" (INST + "insert(p!1, A!1)") (("1" (ASSERT) NIL))))))))))))))))))) ("2" (INST + "emptybag") (("2" (ASSERT) NIL))))))))))))) (|product_prime| "" (AUTO-REWRITE "product_emptybag" "product_insert") (("" (SKOLEM + (_ "p!1")) (("" (INDUCT "A" :NAME "bag_induction") (("1" (GROUND) (("1" (AUTO-REWRITE "prime" "gcd_one1" "gcd_one2") (("1" (ASSERT) NIL))))) ("2" (SKOSIMP) (("2" (GROUND) (("1" (REWRITE "mutual_primes_commutes" +) (("1" (REWRITE "mutual_primes_commutes" -) (("1" (REWRITE "mutual_prime_prod") (("1" (ASSERT) (("1" (REWRITE "distinct_primes" +) (("1" (EXPAND "insert") (("1" (ASSERT) NIL))))))))))))) ("2" (EXPAND "insert") (("2" (LIFT-IF) (("2" (GROUND) NIL))))))))))))))) (|division_product| "" (AUTO-REWRITE "product_emptybag" "product_insert" "product_one" "one_divides" "one_div_one" "subbag_emptybag" "subbag_insert" "subbag_insert2" "divides_prod_elim1" "divides_prod2") (("" (INDUCT "B" :NAME "bag_induction") (("1" (SKOLEM!) (("1" (ASSERT) NIL))) ("2" (SKOSIMP*) (("2" (GROUND) (("1" (USE "product_prime" ("p" "x!1" "A" "A!2")) (("1" (GROUND) (("1" (USE "divides_prod_prime1") (("1" (REDUCE) NIL))) ("2" (USE "remove_element_finite" ("A" "A!2")) (("2" (REDUCE :IF-MATCH NIL) (("2" (INST?) (("2" (ASSERT) NIL))))))))))) ("2" (CASE "A!2(x!1) > 0") (("1" (REWRITE "remove_element_finite") (("1" (REDUCE :IF-MATCH NIL) (("1" (INST?) (("1" (ASSERT) NIL))))))) ("2" (INST?) (("2" (GROUND) (("2" (DELETE 2 4) (("2" (GRIND :DEFS NIL :REWRITES ("subbag?" "insert") :IF-MATCH NIL) (("2" (INST?) (("2" (ASSERT) NIL))))))))))))))))))))) (|unique_decomposition| "" (SKOLEM!) (("" (GROUND) (("" (AUTO-REWRITE "divides_reflexive") (("" (USE "division_product" ("A" "A!1" "B" "B!1")) (("" (USE "division_product" ("A" "B!1" "B" "A!1")) (("" (REPLACE*) (("" (ASSERT) (("" (DELETE -3) (("" (APPLY-EXTENSIONALITY :HIDE? T) (("" (GRIND) NIL))))))))))))))))))) (|prime_fact_TCC1| "" (INST + "lambda x: epsilon! A: prod(A) = x") (("" (SKOLEM!) (("" (USE "epsilon_ax[finite_bag[prime_nat]]") (("" (ASSERT) (("" (USE "decomposition_exists") NIL))))))))) (|factorisation_def| "" (SKOLEM!) (("" (GROUND) (("" (USE "unique_decomposition") (("" (ASSERT) NIL))))))) (|factors_prod| "" (SKOLEM!) (("" (ASSERT) (("" (REWRITE "factorisation_def") NIL))))) (|factorisation_one| "" (AUTO-REWRITE "factorisation_def" "product_one") (("" (ASSERT) NIL))) (|factorisation_empty| "" (SKOLEM!) (("" (AUTO-REWRITE "factorisation_def" "product_emptybag") (("" (ASSERT) (("" (GROUND) NIL))))))) (|factorisation_prime| "" (AUTO-REWRITE "product_insert" "product_emptybag" "factorisation_def") (("" (SKOLEM!) (("" (ASSERT) NIL))))) (|factorisation_prod| "" (AUTO-REWRITE "factorisation_def" "product_plus") (("" (SKOLEM!) (("" (ASSERT) NIL))))) (|factorisation_divides| "" (SKOLEM!) (("" (REWRITE "division_product" :DIR RL) (("" (GROUND) NIL))))) (|factorisation_gcd| "" (SKOLEM!) (("" (NAME-REPLACE "zzz" "gcd(x!1, y!1)" :HIDE? NIL) (("" (REWRITE "gcd_def") (("" (AUTO-REWRITE "factorisation_divides" "factorisation_prime" "factors_prod") (("" (GROUND) (("" (NAME-REPLACE "AA" "prime_fact(zzz)") (("" (NAME-REPLACE "BB" "prime_fact(x!1)") (("" (NAME-REPLACE "CC" "prime_fact(y!1)") (("" (INST - "prod(intersection(BB, CC))") (("" (ASSERT) (("" (AUTO-REWRITE "intersection" "subbag?") (("" (GROUND) (("1" (APPLY-EXTENSIONALITY :HIDE? T) (("1" (EXPAND "min") (("1" (REDUCE) NIL))))) ("2" (SKOLEM!) (("2" (ASSERT) NIL))) ("3" (SKOLEM!) (("3" (ASSERT) NIL))))))))))))))))))))))))))) (|factorisation_primes| "" (SKOLEM!) (("" (EXPAND "prime") (("" (EXPAND "disjoint?") (("" (REWRITE "emptybag_is_empty") (("" (REWRITE "factorisation_gcd" :DIR RL) (("" (REWRITE "factorisation_empty") (("" (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 rem_minus_one: LEMMA rem(b)(-1) = b-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))))))) (|rem_minus_one| "" (SKOLEM!) (("" (REWRITE "rem_def") (("" (INST + "-1") (("" (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_opposite| "" (SKOLEM!) (("" (NAME-REPLACE "y!1" "rem(b!1)(x!1)" :HIDE? NIL) (("" (ASSERT) (("" (REWRITE "rem_def") (("" (REWRITE "rem_def") (("1" (SKOLEM!) (("1" (POSTPONE) NIL))) ("2" (POSTPONE) 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) prime_with_one: LEMMA prime(1, a) prime_with_one2: LEMMA prime(a, 1) 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_with_one| "" (SKOLEM!) (("" (REWRITE "mutual_primes_equiv") (("" (INST + "1" "0") (("" (ASSERT) NIL))))))) (|prime_with_one2| "" (SKOLEM!) (("" (REWRITE "mutual_primes_commutes") (("" (REWRITE "prime_with_one") 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 %-------------------------------------------------- % prod(n, m)(u) = u(n) * u(n+1) * ... * u(m) % (requires n <= m AND u: [nat -> 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 %------------------------------------ % prod(n)(a) = a(0) * ... * a(n-1) % requires a : [below(n) -> nat] %------------------------------------ prod(n)(a:[below(n) -> nat]): RECURSIVE nat = IF n=0 THEN 1 ELSE prod(n-1)(lambda (i: below(n-1)): a(i)) * a(n-1) ENDIF MEASURE n variant_prod_zero: LEMMA FORALL (a: [below(0) -> nat]): prod(0)(a) = 1 variant_prod_one: LEMMA FORALL (a: [below(1) -> nat]): prod(1)(a) = a(0) variant_prod_two: LEMMA FORALL (a: [below(2) -> nat]): prod(2)(a) = a(0) * a(1) variant_prod_positive: LEMMA FORALL (a: [below(n) -> nat]): (FORALL (i: below(n)): a(i) > 0) IMPLIES prod(n)(a) > 0 variant_prod_posnat: LEMMA FORALL (a: [below(n) -> posnat]): prod(n)(a) > 0 variant_prod_null: LEMMA FORALL (a: [below(n) -> nat]): (EXISTS (i: below(n)): a(i) = 0) IMPLIES prod(n)(a) = 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))))))))))))))))))) (|prod_TCC1| "" (SUBTYPE-TCC) NIL) (|prod_TCC2| "" (TERMINATION-TCC) NIL) (|prod_TCC3| "" (SUBTYPE-TCC) NIL) (|prod_TCC4| "" (SUBTYPE-TCC) NIL) (|prod_TCC5| "" (SUBTYPE-TCC) NIL) (|variant_prod_zero| "" (GRIND) NIL) (|variant_prod_one_TCC1| "" (SUBTYPE-TCC) NIL) (|variant_prod_one| "" (GRIND) NIL) (|variant_prod_two_TCC1| "" (SUBTYPE-TCC) NIL) (|variant_prod_two_TCC2| "" (SUBTYPE-TCC) NIL) (|variant_prod_two| "" (GRIND) NIL) (|variant_prod_positive| "" (INDUCT-AND-REWRITE "n" 1 "prod" "pos_times_gt") NIL) (|variant_prod_posnat| "" (SKOLEM!) (("" (REWRITE "variant_prod_positive") (("" (SKOLEM!) (("" (ASSERT) NIL))))))) (|variant_prod_null| "" (INDUCT "n") (("1" (EXPAND "prod") (("1" (REDUCE) NIL))) ("2" (SKOSIMP*) (("2" (EXPAND "prod" +) (("2" (INST?) (("2" (GROUND) (("2" (INST?) 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" (CASE "x!1 > y!1") (("1" (ASSERT) (("1" (APPLY (THEN (FORWARD-CHAIN "divisor_smaller") (ASSERT))) NIL))) ("2" (REWRITE "divides_opposite" :DIR RL) (("2" (ASSERT) (("2" (APPLY (THEN (FORWARD-CHAIN "divisor_smaller") (ASSERT))) NIL))))))) ("2" (AUTO-REWRITE "divides_zero") (("2" (REPLACE*) (("2" (ASSERT) 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" "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" (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) (("" (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))))))))))))))))