\$\$\$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)))))))))))))) \$\$\$inverse_modulo.pvs inverse_modulo : THEORY BEGIN IMPORTING mutual_primes x, y: VAR int py, b: VAR posnat %------------------------------------ % 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 inverse_modulo \$\$\$inverse_modulo.prf (|inverse_modulo| (|rem_inverse| "" (SKOLEM!) (("" (CASE-REPLACE "x!1=0") (("1" (AUTO-REWRITE "rem_zero") (("1" (ASSERT) NIL NIL)) NIL) ("2" (ASSERT) (("2" (AUTO-REWRITE "mutual_primes_equiv" "rem_def") (("2" (ASSERT) (("2" (REDUCE :INSTANTIATOR INST!) (("1" (INST + "y!1" "-q!1") (("1" (ASSERT) NIL NIL)) NIL) ("2" (INST + "n!1") (("2" (INST + "- m!1") (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|rem_inverse2| "" (SKOLEM!) (("" (REWRITE "rem_inverse" :DIR RL) (("" (PROP) (("1" (SKOLEM!) (("1" (INST?) NIL NIL)) 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 NIL) ("2" (INST?) (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) \$\$\$chinese_remainder.pvs chinese_remainder : THEORY BEGIN IMPORTING inverse_modulo, posnat_induction, products 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_remainder0: PROPOSITION FORALL n, (p: mutual_primes(n)), (a: [below(n) -> int]): EXISTS (x: mod(prod(n)(p))): FORALL (i: below(n)): rem(p(i))(x) = rem(p(i))(a(i)) 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 NIL)) NIL) ("2" (REPLACE -2 + RL) (("2" (ASSERT) NIL NIL)) NIL)) 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 NIL)) NIL) ("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (DELETE 2) (("2" (EXPAND "divides") (("2" (GROUND) (("1" (INST + "-n!1") (("1" (ASSERT) NIL NIL)) NIL) ("2" (INST + "-m!1") (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) 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 "associative_mult") (("1" (REWRITE "rem_sum1" :DIR RL) (("1" (REWRITE "rem_diff2" :DIR RL) (("1" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL) ("2" (ASSERT) NIL NIL)) NIL) ("2" (CASE-REPLACE "p1!1 * n!1 = 1 - q1!1 * m!1") (("1" (ASSERT) (("1" (REWRITE "associative_mult") (("1" (REWRITE "rem_sum1" :DIR RL) (("1" (REWRITE "rem_diff2" :DIR RL) (("1" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL) ("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) 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 NIL)) NIL)) NIL)) NIL) ("2" (DELETE -2 -4) (("2" (SKOSIMP*) (("2" (INST + "q!2 - q!1 * p1!1") (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) 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 NIL)) NIL)) NIL)) NIL) ("2" (EXPAND "divides") (("2" (SKOLEM!) (("2" (INST + "x!2 * p1!1") (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL) ("3" (CASE-REPLACE "x!1 - y!1 = 0") (("1" (ASSERT) NIL NIL) ("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL) (|chinese_remainder0| "" (AUTO-REWRITE "rem_mod" "rem_rem" "mutual_prime_prod") (("" (INDUCT "n" :NAME "posnat_induction") (("1" (SKOSIMP*) (("1" (INST + "rem(p!1(0))(a!1(0))") (("1" (SKOLEM!) (("1" (ASSERT) (("1" (ASSERT) NIL NIL)) NIL)) NIL) ("2" (REWRITE "variant_prod_one") (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL) ("2" (SKOSIMP*) (("2" (TYPEPRED "p!1") (("2" (INST-CP - "n!1" "n!1-1") (("2" (ASSERT) (("2" (USE "chinese_remainder2" ("a" "a!1(n!1)" "b" "a!1(n!1-1)")) (("2" (ASSERT) (("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| (:NEW-GROUND? NIL) "" (SUBTYPE-TCC) NIL NIL) (|delete_TCC2| (:NEW-GROUND? NIL) "" (SUBTYPE-TCC) NIL 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 finite_insert_bag: JUDGEMENT insert(x, A) HAS_TYPE 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) %---------------------------- % Variants for finite bags %---------------------------- 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_subbag: LEMMA subbag?(S, A) IMPLIES indbag(S) finite_bag_plus: JUDGEMENT plus(A, B) HAS_TYPE finite_bag finite_bag_union: JUDGEMENT union(A, B) HAS_TYPE finite_bag finite_bag_inter1: JUDGEMENT intersection(A, S) HAS_TYPE finite_bag finite_bag_inter2: JUDGEMENT intersection(S, A) HAS_TYPE finite_bag finite_bag_purge: JUDGEMENT purge(x, A) HAS_TYPE finite_bag finite_bag_delete: JUDGEMENT delete(x, A, n) HAS_TYPE 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 NIL)) NIL)) NIL)) NIL) (|emptybag_TCC1| "" (EXPAND* "indbag" "empty?") NIL NIL) (|finite_insert_bag| "" (SKOLEM!) (("" (EXPAND "indbag") (("" (REDUCE) NIL NIL)) NIL)) NIL) (|emptybag_is_empty| "" (GRIND) (("" (APPLY-EXTENSIONALITY :HIDE? T) (("" (INST?) NIL NIL)) NIL)) NIL) (|subbag_emptybag| "" (GRIND) (("" (APPLY-EXTENSIONALITY :HIDE? T) (("" (INST?) (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL) (|subbag_insert| "" (GRIND :IF-MATCH NIL) (("1" (INST?) (("1" (LIFT-IF) (("1" (GROUND) NIL NIL)) NIL)) NIL) ("2" (INST?) (("2" (ASSERT) NIL NIL)) NIL) ("3" (INST?) NIL NIL)) NIL) (|subbag_insert2| "" (GRIND) NIL NIL) (|subbag_insert3| "" (GRIND) NIL NIL) (|insert_not_empty| "" (SKOLEM!) (("" (REWRITE "emptybag_is_empty" :DIR RL) (("" (GRIND) NIL NIL)) NIL)) 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 NIL)) NIL)) NIL)) NIL)) NIL) (|insert_exchange| "" (SKOLEM!) (("" (APPLY-EXTENSIONALITY :HIDE? T) (("" (GRIND) NIL NIL)) NIL)) 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 NIL)) NIL) ("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) 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 NIL) ("2" (ASSERT) NIL NIL)) NIL)) 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 NIL) ("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (GROUND) (("2" (SKOSIMP) (("2" (REPLACE*) (("2" (REWRITE "insert_exchange") NIL NIL)) NIL)) NIL)) NIL)) NIL)) 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 NIL)) NIL)) NIL)) NIL)) 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 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 NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (EXPAND "indbag" +) (("2" (GROUND) (("2" (INST?) (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|equal_insert_finite| "" (SKOLEM!) (("" (GROUND) (("1" (REWRITE "equal_insert") (("1" (SKOLEM!) (("1" (INST?) (("1" (USE "insert_finite") (("1" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL) ("2" (REWRITE "equal_insert") (("2" (SKOLEM!) (("2" (INST?) (("2" (USE "insert_finite") (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL) ("3" (SKOSIMP) (("3" (REPLACE*) (("3" (REWRITE "insert_exchange") NIL NIL)) NIL)) NIL)) NIL)) NIL) (|insert_or_empty_finite| "" (SKOSIMP) (("" (AUTO-REWRITE "emptybag_is_empty") (("" (USE "insert_or_empty") (("" (ASSERT) (("" (SKOLEM!) (("" (INST?) (("" (USE "insert_finite") (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|remove_element_finite| "" (SKOLEM!) (("" (REWRITE "remove_element") (("" (APPLY (THEN (GROUND) (SKOLEM!) (INST?))) (("" (USE "insert_finite") (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) 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 NIL)) NIL)) NIL) ("2" (DELETE 2) (("2" (SKOSIMP) (("2" (AUTO-REWRITE "emptybag_is_empty" "insert_not_empty") (("2" (SPLIT -) (("1" (ASSERT) NIL NIL) ("2" (SKOSIMP) (("2" (INST?) (("2" (GROUND) (("2" (REPLACE*) (("2" (REWRITE "finite_insert_bag") NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|finite_bag_subbag| "" (INDUCT "A" :NAME "bag_induction") (("1" (AUTO-REWRITE "subbag_emptybag") (("1" (SKOSIMP) (("1" (ASSERT) NIL NIL)) NIL)) 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 NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (INST?) (("2" (GROUND) (("2" (DELETE 3) (("2" (GRIND :IF-MATCH NIL) (("2" (INST?) (("2" (LIFT-IF) (("2" (GROUND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) 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 NIL) ("2" (DELETE 2) (("2" (APPLY-EXTENSIONALITY :HIDE? T) (("2" (GRIND) NIL NIL)) NIL)) NIL)) 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 NIL) ("2" (DELETE -1 2) (("2" (APPLY-EXTENSIONALITY :HIDE? T) (("2" (GRIND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) 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 NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|finite_bag_inter1| "" (SKOLEM!) (("" (USE "finite_bag_subbag") (("" (ASSERT) (("" (DELETE 2) (("" (GRIND) NIL NIL)) NIL)) NIL)) NIL)) NIL) (|finite_bag_inter2| "" (SKOLEM!) (("" (USE "finite_bag_subbag") (("" (ASSERT) (("" (DELETE 2) (("" (GRIND) NIL NIL)) NIL)) NIL)) NIL)) NIL) (|finite_bag_purge| "" (SKOLEM!) (("" (USE "finite_bag_subbag") (("" (ASSERT) (("" (DELETE 2) (("" (GRIND) NIL NIL)) NIL)) NIL)) NIL)) NIL) (|finite_bag_delete| "" (SKOLEM!) (("" (USE "finite_bag_subbag") (("" (ASSERT) (("" (DELETE 2) (("" (GRIND) NIL NIL)) NIL)) NIL)) NIL)) NIL) (|Card_emptybag| "" (SKOLEM!) (("" (EXPAND "Card") (("" (GROUND) (("" (SKOSIMP) (("" (USE "insert_not_empty") (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|Card_insert_TCC1| "" (SUBTYPE-TCC) NIL NIL) (|Card_insert| "" (CASE "FORALL A, n, x: Card(insert(x, A), n) IMPLIES n > 0 AND Card(A, n-1)") (("1" (SKOLEM!) (("1" (REDUCE) (("1" (EXPAND "Card" +) (("1" (INST + "x!1" "A!1" "n!1-1") (("1" (GROUND) NIL NIL)) NIL)) NIL)) NIL)) NIL) ("2" (DELETE 2) (("2" (AUTO-REWRITE "equal_insert_finite" "insert_not_empty") (("2" (INDUCT "n") (("1" (EXPAND "Card") (("1" (SKOLEM!) (("1" (ASSERT) NIL NIL)) NIL)) NIL) ("2" (SKOSIMP*) (("2" (ASSERT) (("2" (EXPAND "Card" -2) (("2" (REDUCE :POLARITY? T) (("2" (EXPAND "Card" +) (("2" (INST + "x!2" "C!1" "j!1 - 1") (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("3" (SKOSIMP) (("3" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL) ("3" (SKOSIMP) (("3" (ASSERT) NIL NIL)) NIL)) NIL) (|Card_unique| "" (AUTO-REWRITE "Card_emptybag" "Card_insert") (("" (INDUCT "A" :NAME "bag_induction") (("1" (SKOSIMP) (("1" (ASSERT) NIL NIL)) NIL) ("2" (SKOSIMP*) (("2" (ASSERT) (("2" (GROUND) (("2" (INST - "n!1 - 1" "m!1 -1") (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|Card_total| "" (AUTO-REWRITE "Card_emptybag" "Card_insert") (("" (INDUCT "A" :NAME "bag_induction") (("1" (INST + "0") (("1" (ASSERT) NIL NIL)) NIL) ("2" (SKOSIMP*) (("2" (INST + "n!1+1") (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL) (|card_TCC1| "" (INST + "lambda A: epsilon! n: Card(A, n)") (("" (SKOLEM!) (("" (USE "epsilon_ax[nat]") (("" (USE "Card_total") (("" (GROUND) NIL NIL)) NIL)) NIL)) NIL)) NIL) (|card_def| "" (SKOLEM!) (("" (GROUND) (("" (USE "Card_unique") (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL) (|card_emptybag| "" (AUTO-REWRITE "card_def" "Card_emptybag") (("" (ASSERT) NIL NIL)) NIL) (|card_zero| "" (SKOLEM!) (("" (GROUND) (("1" (TYPEPRED "card(A!1)") (("1" (EXPAND "Card") (("1" (PROPAX) NIL NIL)) NIL)) NIL) ("2" (REPLACE*) (("2" (REWRITE "card_emptybag") NIL NIL)) NIL)) NIL)) NIL) (|card_insert| "" (SKOLEM!) (("" (AUTO-REWRITE "card_def" "Card_insert") (("" (ASSERT) (("" (GROUND) NIL NIL)) NIL)) NIL)) NIL) (|card_positive| "" (SKOLEM!) (("" (GROUND) (("1" (TYPEPRED "card(A!1)") (("1" (EXPAND "Card") (("1" (SKOSIMP) (("1" (INST?) NIL NIL)) NIL)) NIL)) NIL) ("2" (SKOLEM!) (("2" (REPLACE*) (("2" (REWRITE "card_insert") (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|card_induction| "" (REDUCE) NIL 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)::T, B, 1) insert_choose: LEMMA insert(choose(B)::T, 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-TYPEPRED) (("1" (DELETE -1) (("1" (EXPAND "empty?") (("1" (SKOLEM!) (("1" (USE "epsilon_ax[T]") (("1" (GROUND) (("1" (INST + "x!1") (("1" (ASSERT) NIL NIL)) NIL)) NIL) ("2" (INST + "x!1") NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (GRIND) NIL NIL)) NIL) (|insert_choose| "" (SKOLEM!) (("" (APPLY-EXTENSIONALITY :HIDE? T) (("" (GRIND) NIL NIL)) NIL)) NIL) (|card_rest| "" (SKOSIMP) (("" (USE "card_insert" ("x" "choose(B!1)" "A" "rest(B!1)")) (("" (REWRITE "insert_choose") (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL) (|recur_TCC1| "" (AUTO-REWRITE "card_rest") (("" (SKOSIMP) (("" (ASSERT) NIL NIL)) NIL)) NIL) (|recur_emptybag| "" (AUTO-REWRITE "recur" "emptybag_is_empty") (("" (SKOLEM!) (("" (ASSERT) NIL NIL)) NIL)) 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 NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) 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 NIL) (|product_emptybag| "" (AUTO-REWRITE "recur_emptybag" "prod" "prod_TCC1") (("" (ASSERT) NIL NIL)) NIL) (|product_insert| "" (AUTO-REWRITE "recur_insert" "prod" "prod_TCC1") (("" (ASSERT) NIL NIL)) 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 NIL) ("2" (DELETE 2) (("2" (APPLY-EXTENSIONALITY :HIDE? T) (("2" (AUTO-REWRITE "plus" "emptybag") (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) 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 NIL) ("2" (AUTO-REWRITE "plus" "insert") (("2" (DELETE -1 2) (("2" (APPLY-EXTENSIONALITY :HIDE? T) (("2" (CASE "x!2 = x!1") (("1" (ASSERT) NIL NIL) ("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) 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 NIL)) NIL)) NIL)) NIL)) NIL) ("2" (REPLACE*) (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) 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 NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (INST + "emptybag") (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) 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 NIL)) NIL)) 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 NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (EXPAND "insert") (("2" (LIFT-IF) (("2" (GROUND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) 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 NIL)) 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 NIL)) NIL) ("2" (USE "remove_element_finite" ("A" "A!2")) (("2" (REDUCE :IF-MATCH NIL) (("2" (INST?) (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (CASE "A!2(x!1) > 0") (("1" (REWRITE "remove_element_finite") (("1" (REDUCE :IF-MATCH NIL) (("1" (INST?) (("1" (ASSERT) NIL NIL)) NIL)) NIL)) NIL) ("2" (INST?) (("2" (GROUND) (("2" (DELETE 2 4) (("2" (GRIND :DEFS NIL :REWRITES ("subbag?" "insert") :IF-MATCH NIL) (("2" (INST?) (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) 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 NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) 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 NIL)) NIL)) NIL)) NIL)) NIL) (|factorisation_def| "" (SKOLEM!) (("" (GROUND) (("" (USE "unique_decomposition") (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL) (|factors_prod| "" (SKOLEM!) (("" (ASSERT) (("" (REWRITE "factorisation_def") NIL NIL)) NIL)) NIL) (|factorisation_one| "" (AUTO-REWRITE "factorisation_def" "product_one") (("" (ASSERT) NIL NIL)) NIL) (|factorisation_empty| "" (SKOLEM!) (("" (AUTO-REWRITE "factorisation_def" "product_emptybag") (("" (ASSERT) (("" (GROUND) NIL NIL)) NIL)) NIL)) NIL) (|factorisation_prime| "" (AUTO-REWRITE "product_insert" "product_emptybag" "factorisation_def") (("" (SKOLEM!) (("" (ASSERT) NIL NIL)) NIL)) NIL) (|factorisation_prod| "" (AUTO-REWRITE "factorisation_def" "product_plus") (("" (SKOLEM!) (("" (ASSERT) NIL NIL)) NIL)) NIL) (|factorisation_divides| "" (SKOLEM!) (("" (REWRITE "division_product" :DIR RL) (("" (GROUND) NIL NIL)) NIL)) 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 NIL)) NIL)) NIL) ("2" (SKOLEM!) (("2" (ASSERT) NIL NIL)) NIL) ("3" (SKOLEM!) (("3" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|factorisation_primes| "" (SKOLEM!) (("" (EXPAND "prime") (("" (EXPAND "disjoint?") (("" (REWRITE "emptybag_is_empty") (("" (REWRITE "factorisation_gcd" :DIR RL) (("" (REWRITE "factorisation_empty") (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) \$\$\$product_modulo.pvs product_modulo : THEORY BEGIN IMPORTING products, mutual_primes 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)) equivalent_varprod: LEMMA FORALL (a, b: [below(n) -> nat]): (FORALL (i: below(n)): rem(p)(a(i)) = rem(p)(b(i))) IMPLIES rem(p)(prod(n)(a)) = rem(p)(prod(n)(b)) nz: VAR [nat -> nzint] x : VAR nzint mutual_prime_product: LEMMA n <= m IMPLIES (prime(prod(n, m)(nz), x) IFF FORALL (i: idx(n, m)): prime(nz(i), x)) mutual_prime_varprod: LEMMA FORALL (a: [below(n) -> nzint]): prime(prod(n)(a), x) IFF FORALL (i: below(n)): prime(a(i), x) END product_modulo \$\$\$product_modulo.prf (|product_modulo| (|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 NIL)) NIL) ("2" (DELETE 2) (("2" (INDUCT-AND-REWRITE "j" 1 "prod_once" "prod_step" "rem_prod") NIL NIL)) NIL)) NIL)) NIL)) NIL) (|equivalent_varprod| "" (AUTO-REWRITE "prod") (("" (INDUCT "n") (("1" (REDUCE) NIL NIL) ("2" (REDUCE :IF-MATCH NIL) (("2" (REWRITE "rem_prod") (("1" (DELETE 2) (("1" (REDUCE :POLARITY? T) NIL NIL)) NIL) ("2" (INST? -4) NIL NIL)) NIL)) NIL)) NIL)) NIL) (|mutual_prime_product| "" (SKOSIMP) (("" (ASSERT) (("" (CASE "FORALL (j: nat): j <= m!1 - n!1 IMPLIES (prime(prod(n!1, n!1+j)(nz!1), x!1) IFF FORALL (i: upto(j)): prime(nz!1(n!1 + i), x!1))") (("1" (INST - "m!1 - n!1") (("1" (ASSERT) (("1" (REPLACE*) (("1" (DELETE -1) (("1" (REDUCE :IF-MATCH NIL) (("1" (INST - "i!1 - n!1") (("1" (ASSERT) NIL NIL)) NIL) ("2" (INST?) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (DELETE 2) (("2" (AUTO-REWRITE "prod_once" "prod_step" "mutual_prime_prod") (("2" (INDUCT "j") (("1" (REDUCE) NIL NIL) ("2" (REDUCE :IF-MATCH NIL) (("1" (INST? :POLARITY? T) NIL NIL) ("2" (INST? -5) NIL NIL) ("3" (INST?) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|mutual_prime_varprod| "" (AUTO-REWRITE "prod" "mutual_prime_prod" "prime_with_one") (("" (INDUCT "n") (("1" (REDUCE) NIL NIL) ("2" (SKOSIMP*) (("2" (ASSERT) (("2" (INST?) (("2" (ASSERT) (("2" (REPLACE*) (("2" (DELETE -) (("2" (REDUCE :POLARITY? T) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) \$\$\$parity.pvs %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % A few lemmas about odd or even numbers % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% parity : THEORY BEGIN i : VAR int incr_odd : LEMMA odd?(i + 1) IFF even?(i) incr_even : LEMMA even?(i + 1) IFF odd?(i) opposite_odd : LEMMA odd?(- i) IFF odd?(i) opposite_even : LEMMA even?(- i) IFF even?(i) parity1 : LEMMA odd?(i) OR odd?(i + 1) parity2 : LEMMA even?(i) OR even?(i + 1) odd_not_even : LEMMA odd?(i) IFF not even?(i) even_not_odd : LEMMA even?(i) IFF not odd?(i) even_2i : LEMMA even?(2 * i) odd_2i_plus1 : LEMMA odd?(2 * i + 1) odd_2i_minus1 : LEMMA odd?(2 * i - 1) %------------------------------------- % Rewrite rules for small constants %------------------------------------- parity_zero: LEMMA even?(0) parity_one: LEMMA odd?(1) parity_two: LEMMA even?(2) parity_three: LEMMA odd?(3) parity_minus_one: LEMMA odd?(-1) parity_minus_two: LEMMA even?(-2) parity_minus_three: LEMMA odd?(-3) END parity \$\$\$parity.prf (|parity| (|incr_odd| (:NEW-GROUND? NIL) "" (GRIND :IF-MATCH NIL) NIL NIL) (|incr_even| (:NEW-GROUND? NIL) "" (GRIND :IF-MATCH NIL) (("1" (INST + "j!1 - 1") (("1" (ASSERT) NIL NIL)) NIL) ("2" (INST + "j!1 + 1") (("2" (ASSERT) NIL NIL)) NIL)) NIL) (|opposite_odd| (:NEW-GROUND? NIL) "" (GRIND :IF-MATCH NIL) (("1" (INST + "-j!1-1") (("1" (ASSERT) NIL NIL)) NIL) ("2" (INST + "- j!1 -1") (("2" (ASSERT) NIL NIL)) NIL)) NIL) (|opposite_even| (:NEW-GROUND? NIL) "" (GRIND :IF-MATCH NIL) (("1" (INST + "-j!1") (("1" (ASSERT) NIL NIL)) NIL) ("2" (INST + "-j!1") (("2" (ASSERT) NIL NIL)) NIL)) NIL) (|parity1| (:NEW-GROUND? NIL) "" (CASE "FORALL (n : nat) : odd?(n) OR odd?(n + 1)") (("1" (SKOSIMP) (("1" (CASE "i!1 >= 0") (("1" (INST?) (("1" (ASSERT) NIL NIL)) NIL) ("2" (ASSERT) (("2" (INST - "- (1 + i!1)") (("2" (REWRITE "opposite_odd" 2 :DIR RL) (("2" (REWRITE "opposite_odd" 3 :DIR RL) (("2" (GROUND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (DELETE 2) (("2" (INDUCT "n") (("1" (GRIND) NIL NIL) ("2" (SKOLEM!) (("2" (GROUND) (("2" (DELETE 1) (("2" (EXPAND "odd?") (("2" (SKOLEM!) (("2" (INST + "j!2 + 1") (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|parity2| (:NEW-GROUND? NIL) "" (AUTO-REWRITE "incr_even") (("" (SKOSIMP) (("" (ASSERT) (("" (USE "parity1") (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL) (|odd_not_even| (:NEW-GROUND? NIL) "" (SKOLEM!) (("" (GROUND) (("1" (GRIND) NIL NIL) ("2" (USE "parity1") (("2" (ASSERT) (("2" (REWRITE "incr_odd" -1) NIL NIL)) NIL)) NIL)) NIL)) NIL) (|even_not_odd| (:NEW-GROUND? NIL) "" (SKOLEM!) (("" (GROUND) (("1" (GRIND) NIL NIL) ("2" (USE "parity1") (("2" (ASSERT) (("2" (REWRITE "incr_odd" -1) NIL NIL)) NIL)) NIL)) NIL)) NIL) (|even_2i| (:NEW-GROUND? NIL) "" (GRIND) NIL NIL) (|odd_2i_plus1| (:NEW-GROUND? NIL) "" (GRIND) NIL NIL) (|odd_2i_minus1| (:NEW-GROUND? NIL) "" (SKOLEM!) (("" (REWRITE "incr_even" :DIR RL) (("" (REWRITE "even_2i") NIL NIL)) NIL)) NIL) (|parity_zero| (:NEW-GROUND? NIL) "" (GRIND) NIL NIL) (|parity_one| (:NEW-GROUND? NIL) "" (REWRITE "incr_odd") (("" (REWRITE "parity_zero") NIL NIL)) NIL) (|parity_two| (:NEW-GROUND? NIL) "" (REWRITE "incr_even") (("" (REWRITE "parity_one") NIL NIL)) NIL) (|parity_three| (:NEW-GROUND? NIL) "" (REWRITE "incr_odd") (("" (REWRITE "parity_two") NIL NIL)) NIL) (|parity_minus_one_TCC1| (:NEW-GROUND? NIL) "" (SUBTYPE-TCC) NIL NIL) (|parity_minus_one| (:NEW-GROUND? NIL) "" (REWRITE "opposite_odd") (("" (REWRITE "parity_one") NIL NIL)) NIL) (|parity_minus_two_TCC1| (:NEW-GROUND? NIL) "" (SUBTYPE-TCC) NIL NIL) (|parity_minus_two| (:NEW-GROUND? NIL) "" (REWRITE "opposite_even") (("" (REWRITE "parity_two") NIL NIL)) NIL) (|parity_minus_three_TCC1| (:NEW-GROUND? NIL) "" (SUBTYPE-TCC) NIL NIL) (|parity_minus_three| (:NEW-GROUND? NIL) "" (REWRITE "opposite_odd") (("" (REWRITE "parity_three") NIL NIL)) 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 injection_n_to_m_var: THEOREM (EXISTS (f: [below(n) -> below(m)]): injective?(f)) IFF n <= m surjection_n_to_m: THEOREM (EXISTS (f: [below(n) -> below(m)]): surjective?(f)) IMPLIES m <= n surjection_n_to_m_var: THEOREM (EXISTS (f: [below(n) -> below(m)]): surjective?(f)) IFF (m > 0 AND m <= n) OR (m = 0 AND n = 0) 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 NIL) ("2" (SKOSIMP*) (("2" (TYPEPRED "f!1(0)") (("2" (ASSERT) (("2" (INST - "m!1 - 1") (("2" (GROUND) (("2" (DELETE -1 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" (INST-CP - "x1!1" "j!1") (("1" (INST-CP - "x2!1" "j!1") (("1" (INST - "x1!1" "x2!1") (("1" (SMASH) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (SKOSIMP) (("2" (ASSERT) NIL NIL)) NIL) ("3" (SKOSIMP) (("3" (EXPAND "injective?") (("3" (INST - "x!1" "j!1") (("3" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|injection_n_to_m_var| "" (SKOLEM!) (("" (GROUND) (("1" (REWRITE "injection_n_to_m") NIL NIL) ("2" (INST + "lambda (i: below(n!1)): i") (("2" (GRIND) NIL NIL)) NIL)) NIL)) NIL) (|surjection_n_to_m| "" (SKOSIMP*) (("" (ASSERT) (("" (REWRITE "injection_n_to_m") (("" (EXPAND "surjective?" -1) (("" (INST -1 "0") (("" (SKOSIMP) (("" (ASSERT) (("" (INST + "inverse(f!1)") (("1" (REWRITE "inj_inv") (("1" (INST?) NIL NIL)) NIL) ("2" (INST?) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|surjection_n_to_m_var| "" (SKOLEM!) (("" (APPLY (THEN (SPLIT) (FLATTEN))) (("1" (FORWARD-CHAIN "surjection_n_to_m") (("1" (ASSERT) (("1" (SKOSIMP) (("1" (TYPEPRED "f!1(0)") (("1" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL) ("2" (INST + "lambda (i: below(n!1)): IF i < m!1 THEN i ELSE 0 ENDIF") (("1" (GRIND) NIL NIL) ("2" (REDUCE) NIL NIL)) NIL)) NIL)) 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 NIL)) NIL) ("2" (INST?) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (INST 1 "LAMBDA (x : below(n!1)) : x") (("1" (GRIND) NIL NIL) ("2" (SKOLEM!) (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) 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 NIL)) NIL)) NIL) ("2" (SKOLEM!) (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (INST + "lambda (i : upto(n!1)): i") (("2" (GRIND) NIL NIL)) NIL)) NIL)) 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 NIL)) NIL)) NIL)) NIL) ("2" (SKOLEM!) (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (INST + "lambda (i : upto(n!1)): IF i <= m!1 THEN i ELSE 0 ENDIF") (("2" (GRIND) NIL NIL)) NIL)) NIL)) 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 NIL) ("2" (INST?) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (INST + "lambda (i : upto(n!1)): i") (("2" (GRIND) NIL NIL)) NIL)) NIL)) NIL) (|surj_equiv_inj| "" (SKOLEM!) (("" (CASE "n!1 = 0") (("1" (GRIND) NIL 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" (SMASH) NIL NIL) ("2" (GROUND) NIL NIL) ("3" (GROUND) NIL NIL)) NIL) ("2" (INST + "IF x!1 < x1!1 THEN x!1 ELSE x!1 - 1 ENDIF") (("1" (SMASH) NIL NIL) ("2" (GROUND) NIL NIL) ("3" (GROUND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) 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" (SMASH) (("1" (INST + "x2!1") (("1" (ASSERT) NIL NIL)) NIL) ("2" (INST?) NIL NIL)) NIL)) NIL)) NIL)) NIL) ("2" (SKOSIMP) (("2" (ASSERT) NIL NIL)) NIL) ("3" (SKOSIMP) (("3" (INST? +) (("3" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|inj_equiv_bij| "" (SKOLEM!) (("" (EXPAND "bijective?") (("" (GROUND) (("" (REWRITE "surj_equiv_inj") NIL NIL)) NIL)) NIL)) NIL) (|surj_equiv_bij| "" (SKOLEM!) (("" (EXPAND "bijective?") (("" (GROUND) (("" (REWRITE "surj_equiv_inj") NIL NIL)) NIL)) NIL)) 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 NIL)) NIL) ("2" (INST? -2) (("2" (SKOLEM!) (("2" (INST? +) NIL NIL)) NIL)) NIL) ("3" (INST - "y!1") (("3" (SKOLEM!) (("3" (INST + "x!1") NIL NIL)) NIL)) NIL) ("4" (INST? - :WHERE +) (("4" (ASSERT) NIL NIL)) NIL)) NIL)) NIL) ("2" (SKOLEM!) (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL) (|inj_equiv_bij2| "" (SKOLEM!) (("" (EXPAND "bijective?") (("" (GROUND) (("" (REWRITE "surj_equiv_inj2") NIL NIL)) NIL)) NIL)) NIL) (|surj_equiv_bij2| "" (SKOLEM!) (("" (EXPAND "bijective?") (("" (GROUND) (("" (REWRITE "surj_equiv_inj2") NIL NIL)) NIL)) NIL)) 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) %---------------------------------------- % 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 NIL) (|iter_TCC2| "" (TERMINATION-TCC) NIL NIL) (|iter_once_TCC1| "" (SUBTYPE-TCC) NIL NIL) (|iter_once| "" (GRIND) NIL NIL) (|iter_induct_TCC1| "" (SUBTYPE-TCC) NIL NIL) (|iter_induct| "" (GRIND) NIL 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 NIL)) NIL) ("2" (DELETE 2) (("2" (INDUCT-AND-SIMPLIFY "x") NIL NIL)) NIL)) NIL)) NIL) (|associativity| "" (SKOLEM-TYPEPRED) (("" (EXPAND "associative?") (("" (INST?) (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL) (|iter_assoc_split_TCC1| "" (SUBTYPE-TCC) NIL NIL) (|iter_assoc_split_TCC2| "" (SUBTYPE-TCC) NIL NIL) (|iter_assoc_split| "" (SKOLEM + ("g!1" "m!1" "n!1" _ "u!1")) (("" (INDUCT-AND-REWRITE "p" 1 "iter") (("" (CASE "m!1 < j!1") (("1" (ASSERT) (("1" (REWRITE "associativity" 1) (("1" (ASSERT) NIL NIL)) NIL)) NIL) ("2" (STOP-REWRITE "iter") (("2" (CASE-REPLACE "m!1 = j!1") (("1" (REWRITE "iter_once") NIL NIL) ("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|commutativity| "" (GRIND) NIL 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 NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) 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 NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) 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 NIL)) NIL) ("2" (DELETE 2) (("2" (AUTO-REWRITE "iter") (("2" (INDUCT "x") (("1" (ASSERT) NIL NIL) ("2" (SKOSIMP) (("2" (ASSERT) (("2" (REPLACE*) (("2" (REWRITE "commut_assoc1") NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|swap_unchanged| "" (SKOLEM!) (("" (APPLY-EXTENSIONALITY :HIDE? T) (("" (GRIND) NIL NIL)) NIL)) NIL) (|swap_commutes| "" (SKOLEM!) (("" (APPLY-EXTENSIONALITY :HIDE? T) (("" (GRIND) NIL NIL)) NIL)) NIL) (|swap_inverse| "" (SKOLEM!) (("" (APPLY-EXTENSIONALITY :HIDE? T) (("" (GRIND) NIL NIL)) NIL)) NIL) (|iter_swap_first_last| "" (SKOSIMP) (("" (CASE-REPLACE "m!1 = n!1") (("1" (REWRITE "swap_unchanged") NIL NIL) ("2" (AUTO-REWRITE "iter_once" "iter" "swap") (("2" (ASSERT) (("2" (CASE-REPLACE "m!1 - 1 = n!1") (("1" (ASSERT) (("1" (REWRITE "commutativity") NIL NIL)) 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 NIL) ("2" (REWRITE "iter_same_elements") (("2" (DELETE 2 5) (("2" (REDUCE) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|iter_swap_last_TCC1| "" (SUBTYPE-TCC) NIL NIL) (|iter_swap_last| "" (SKOSIMP) (("" (AUTO-REWRITE "iter_swap_first_last") (("" (CASE-REPLACE "i!1 = n!1") (("1" (ASSERT) NIL NIL) ("2" (USE "iter_assoc_split" ("m" "i!1 - 1" "u" "swap(u!1, i!1, m!1)")) (("1" (USE "iter_assoc_split" ("m" "i!1 - 1" "u" "u!1")) (("1" (ASSERT) (("1" (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 NIL) ("2" (REWRITE "iter_same_elements") (("2" (DELETE -1 -2 2 4) (("2" (GRIND) NIL NIL)) NIL)) NIL)) NIL)) NIL) ("2" (ASSERT) NIL NIL)) NIL) ("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL) (|iter_swap_TCC1| "" (SUBTYPE-TCC) NIL NIL) (|iter_swap| "" (SKOSIMP) (("" (AUTO-REWRITE "iter_swap_last") (("" (CASE-REPLACE "j!1 = m!1") (("1" (ASSERT) NIL 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 NIL) ("2" (REWRITE "iter_same_elements") (("2" (DELETE -1 -2 2 4) (("2" (GRIND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) 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 NIL)) NIL)) NIL)) NIL) ("2" (INST -3 "n!1 + x1!1" "n!1 + x2!1") (("2" (ASSERT) NIL NIL)) NIL)) NIL) ("2" (SKOSIMP) (("2" (GROUND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|perm_equiv| "" (SKOSIMP) (("" (EXPAND "permutation") (("" (EXPAND "bijective?") (("" (GROUND) (("1" (SKOSIMP) (("1" (INST?) (("1" (ASSERT) NIL NIL)) NIL)) 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 NIL)) NIL)) NIL)) NIL) ("2" (INST - "n!1 + x1!1" "n!1 + x2!1") (("2" (ASSERT) NIL NIL)) NIL)) NIL) ("2" (SKOSIMP) (("2" (GROUND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|iter_permutation_TCC1| "" (SUBTYPE-TCC) NIL NIL) (|iter_permutation_TCC2| "" (SUBTYPE-TCC) NIL 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 NIL)) NIL)) NIL)) NIL)) NIL)) 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 NIL)) NIL)) NIL)) NIL)) NIL)) 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 NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (SKOLEM!) (("2" (LIFT-IF) (("2" (GROUND) (("1" (INST?) (("1" (EXPAND "swap") (("1" (LIFT-IF) (("1" (GROUND) NIL NIL)) NIL)) NIL)) NIL) ("2" (INST?) (("2" (EXPAND "injective?") (("2" (INST - "i!1" "1 + j!1 + n!1") (("2" (ASSERT) (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (SKOSIMP) (("2" (ASSERT) NIL NIL)) NIL) ("3" (SKOSIMP) (("3" (GROUND) (("3" (EXPAND "injective?") (("3" (INST - "i!1" "1 + j!1 + n!1") (("3" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|iter_permutation2_TCC1| "" (GRIND :IF-MATCH ALL) NIL 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 NIL)) NIL)) NIL)) NIL)) NIL) (|iter_permutation3_TCC1| "" (SUBTYPE-TCC) NIL NIL) (|iter_permutation3_TCC2| "" (SUBTYPE-TCC) NIL NIL) (|iter_permutation3| "" (SKOSIMP) (("" (REWRITE "iter_permutation") (("" (REWRITE "perm_equiv") (("" (INST?) (("" (GROUND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) \$\$\$products.pvs products : THEORY BEGIN IMPORTING iterations, parity i, j, n, m, p, q: VAR nat u, v : VAR [nat -> real] x, y, z: VAR real %-------------------------------------------------- % prod(n, m)(u) = u(n) * u(n+1) * ... * u(m) % (requires n <= m AND u: [nat -> real]) %-------------------------------------------------- f: VAR [real, real -> real] times_assoc_commutes: JUDGEMENT * HAS_TYPE { f | associative?(f) AND commutative?(f) } prod(n, (m | n <= m))(u): real = iter(*, 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_permutation2: LEMMA n <= m AND permutation(u, n, m, v, p, q) IMPLIES prod(n, m)(u) = prod(p, q)(v) prod_const: LEMMA prod(n, n + m)(lambda i: x) = expt(x, m + 1) %----------------------- % Sign of the product %----------------------- P: VAR { R: [real -> bool] | FORALL x, y: R(x) AND R(y) IMPLIES R(x * y) } prod_closure: LEMMA n <= m AND (FORALL (i: idx(n, m)): P(u(i))) IMPLIES P(prod(n, m)(u)) prod_positive: LEMMA n <= m AND (FORALL (i: idx(n, m)): u(i) > 0) IMPLIES prod(n, m)(u) > 0 prod_negative: LEMMA n <= m AND (FORALL (i: idx(n, m)): u(i) < 0) IMPLIES IF even?(m - n) THEN prod(n, m)(u) < 0 ELSE prod(n, m)(u) > 0 ENDIF prod_negative1: LEMMA n <= m AND even?(m - n) AND (FORALL (i: idx(n, m)): u(i) < 0) IMPLIES prod(n, m)(u) < 0 prod_negative2: LEMMA n <= m AND odd?(m - n) 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_null2: LEMMA n <= m IMPLIES (prod(n, m)(u) = 0 IFF EXISTS (i: idx(n, m)): u(i) = 0) posu: VAR [nat -> posreal] nzu: VAR [nat -> nzreal] nnu: VAR [nat -> nonneg_real] prod_posreal_seq_is_posreal: JUDGEMENT prod(n, (m | n <= m))(posu) HAS_TYPE posreal prod_nzreal_seq_is_nzreal: JUDGEMENT prod(n, (m | n <= m))(nzu) HAS_TYPE nzreal prod_nnreal_seq_is_nnreal: JUDGEMENT prod(n, (m | n <= m))(nnu) HAS_TYPE nonneg_real ru: VAR [nat -> rat] posru: VAR [nat -> posrat] nzru: VAR [nat -> nzrat] nnru: VAR [nat -> nonneg_rat] prod_rat_seq_is_rat: JUDGEMENT prod(n, (m | n <= m))(ru) HAS_TYPE rat prod_posrat_seq_is_posrat: JUDGEMENT prod(n, (m | n <= m))(posru) HAS_TYPE posrat prod_nzrat_seq_is_nzrat: JUDGEMENT prod(n, (m | n <= m))(nzru) HAS_TYPE nzrat prod_nnrat_seq_is_nnrat: JUDGEMENT prod(n, (m | n <= m))(nnru) HAS_TYPE nonneg_rat iu: VAR [nat -> int] nu: VAR [nat -> nat] posnu: VAR [nat -> posnat] nziu: VAR [nat -> nzint] prod_int_seq_is_int: JUDGEMENT prod(n, (m | n <= m))(iu) HAS_TYPE int prod_posnat_seq_is_posnat: JUDGEMENT prod(n, (m | n <= m))(posnu) HAS_TYPE posnat prod_nzint_seq_is_nzint: JUDGEMENT prod(n, (m | n <= m))(nziu) HAS_TYPE nzint prod_nat_seq_is_nat: JUDGEMENT prod(n, (m | n <= m))(nu) HAS_TYPE nat %------------------------------------ % prod(n)(a) = a(0) * ... * a(n-1) % requires a : [below(n) -> real] %------------------------------------ prod(n)(a:[below(n) -> real]): RECURSIVE real = 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) -> real]): prod(0)(a) = 1 variant_prod_one: LEMMA FORALL (a: [below(1) -> real]): prod(1)(a) = a(0) variant_prod_two: LEMMA FORALL (a: [below(2) -> real]): prod(2)(a) = a(0) * a(1) variant_prod_equiv: LEMMA FORALL (a: [below(n) -> real]): prod(n)(a) = prod(0, n)(lambda i: IF i real]): prod(n)(lambda (i: below(n)): a(i) * b(i)) = prod(n)(a) * prod(n)(b) variant_prod_permutation: LEMMA FORALL (a, b: [below(n) -> real]), (h: [below(n) -> below(n)]): injective?(h) AND a = b o h IMPLIES prod(n)(a) = prod(n)(b) variant_prod_const: LEMMA prod(n)(lambda (i: below(n)): x) = expt(x, n) %-------- % Sign %-------- Q: VAR { R: [real -> bool] | R(1) AND FORALL x, y: R(x) AND R(y) IMPLIES R(x * y) } variant_prod_closure: LEMMA FORALL (a: [below(n) -> real]): (FORALL (i: below(n)): Q(a(i))) IMPLIES Q(prod(n)(a)) variant_prod_positive: LEMMA FORALL (a: [below(n) -> real]): (FORALL (i: below(n)): a(i) > 0) IMPLIES prod(n)(a) > 0 variant_prod_negative: LEMMA FORALL (a: [below(n) -> real]): (FORALL (i: below(n)): a(i) < 0) IMPLIES IF even?(n) THEN prod(n)(a) > 0 ELSE prod(n)(a) < 0 ENDIF variant_prod_negative1: LEMMA FORALL (a: [below(n) -> real]): even?(n) AND (FORALL (i: below(n)): a(i) < 0) IMPLIES prod(n)(a) > 0 variant_prod_negative2: LEMMA FORALL (a: [below(n) -> real]): odd?(n) AND (FORALL (i: below(n)): a(i) < 0) IMPLIES prod(n)(a) < 0 variant_prod_null: LEMMA FORALL (a: [below(n) -> real]): (EXISTS (i: below(n)): a(i) = 0) IMPLIES prod(n)(a) = 0 variant_prod_null2: LEMMA FORALL (a: [below(n) -> real]): prod(n)(a) = 0 IFF EXISTS (i: below(n)): a(i) = 0 on: VAR { n | odd?(n) } en: VAR { n | even?(n) } pn: VAR posnat varprod_posreal_seq: JUDGEMENT prod(n)(a: [below(n) -> posreal]) HAS_TYPE posreal varprod_nzreal_seq: JUDGEMENT prod(n)(a: [below(n) -> nzreal]) HAS_TYPE nzreal varprod_nnreal_seq: JUDGEMENT prod(n)(a: [below(n) -> nonneg_real]) HAS_TYPE nonneg_real varprod_negreal_seq1: JUDGEMENT prod(en)(a: [below(en) -> negreal]) HAS_TYPE posreal varprod_negreal_seq2: JUDGEMENT prod(on)(a: [below(on) -> negreal]) HAS_TYPE negreal varprod_rat_seq: JUDGEMENT prod(n)(a: [below(n) -> rat]) HAS_TYPE rat varprod_posrat_seq: JUDGEMENT prod(n)(a: [below(n) -> posrat]) HAS_TYPE posrat varprod_nzrat_seq: JUDGEMENT prod(n)(a: [below(n) -> nzrat]) HAS_TYPE nzrat varprod_nnrat_seq: JUDGEMENT prod(n)(a: [below(n) -> nonneg_rat]) HAS_TYPE nonneg_rat varprod_negrat_seq1: JUDGEMENT prod(en)(a: [below(en) -> negrat]) HAS_TYPE posrat varprod_negrat_seq2: JUDGEMENT prod(on)(a: [below(on) -> negrat]) HAS_TYPE negrat varprod_int_seq: JUDGEMENT prod(n)(a: [below(n) -> int]) HAS_TYPE int varprod_posint_seq: JUDGEMENT prod(n)(a: [below(n) -> posint]) HAS_TYPE posint varprod_nzint_seq: JUDGEMENT prod(n)(a: [below(n) -> nzint]) HAS_TYPE nzint varprod_nat_seq: JUDGEMENT prod(n)(a: [below(n) -> nat]) HAS_TYPE nat varprod_negint_seq1: JUDGEMENT prod(en)(a: [below(en) -> negint]) HAS_TYPE posint varprod_negint_seq2: JUDGEMENT prod(on)(a: [below(on) -> negint]) HAS_TYPE negint END products \$\$\$products.prf (|products| (|times_assoc_commutes| "" (GRIND) NIL NIL) (|prod_once_TCC1| "" (SUBTYPE-TCC) NIL NIL) (|prod_once| "" (GRIND) NIL NIL) (|prod_step_TCC1| "" (SUBTYPE-TCC) NIL NIL) (|prod_step| "" (AUTO-REWRITE "prod" "iter_induct[real]" "mult") (("" (SKOSIMP) (("" (ASSERT) NIL NIL)) NIL)) NIL) (|prod_same_elements| "" (EXPAND "prod") (("" (SKOSIMP) (("" (REWRITE "iter_same_elements") (("" (DELETE 2) (("" (SKOSIMP) (("" (INST?) (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|prod_split_TCC1| "" (SUBTYPE-TCC) NIL NIL) (|prod_split_TCC2| "" (SUBTYPE-TCC) NIL NIL) (|prod_split| "" (SKOSIMP) (("" (EXPAND "prod") (("" (USE "iter_assoc_split[real]") (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL) (|prod_split2| "" (SKOSIMP) (("" (AUTO-REWRITE "prod") (("" (ASSERT) (("" (USE "iter_split" ("u" "u!1" "v" "v!1")) NIL NIL)) NIL)) NIL)) NIL) (|prod_permutation_TCC1| "" (SUBTYPE-TCC) NIL NIL) (|prod_permutation_TCC2| "" (SUBTYPE-TCC) NIL NIL) (|prod_permutation| "" (SKOSIMP) (("" (EXPAND "prod") (("" (REWRITE "iter_permutation") NIL NIL)) NIL)) NIL) (|prod_permutation2_TCC1| "" (GRIND :IF-MATCH ALL) NIL NIL) (|prod_permutation2| "" (EXPAND "prod") (("" (SKOSIMP) (("" (REWRITE "iter_permutation2") NIL NIL)) NIL)) NIL) (|prod_const_TCC1| "" (SUBTYPE-TCC) NIL NIL) (|prod_const| "" (SKOLEM + (_ "n!1" "x!1")) (("" (INDUCT-AND-REWRITE "m" 1 "prod_once" "prod_step" "expt") NIL NIL)) NIL) (|prod_closure| "" (SKOSIMP) (("" (CASE "FORALL i: i <= m!1 - n!1 IMPLIES P!1(prod(n!1, n!1+i)(u!1))") (("1" (INST - "m!1 -n!1") (("1" (ASSERT) NIL NIL) ("2" (ASSERT) NIL NIL)) NIL) ("2" (DELETE 2) (("2" (INDUCT-AND-REWRITE "i" 1 "prod_once" "prod_step") (("2" (TYPEPRED "P!1") (("2" (INST?) (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) 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 NIL) ("2" (ASSERT) NIL NIL)) NIL) ("2" (DELETE 2) (("2" (INDUCT-AND-REWRITE "i" 1 "prod_once" "prod_step" "pos_times_gt") NIL NIL)) NIL)) NIL)) NIL) (|prod_negative| "" (SKOSIMP) (("" (ASSERT) (("" (CASE "FORALL i: i <= m!1 - n!1 IMPLIES IF even?(i) THEN prod(n!1, n!1 + i)(u!1) < 0 ELSE prod(n!1, n!1 + i)(u!1) > 0 ENDIF") (("1" (INST - "m!1 - n!1") (("1" (ASSERT) NIL NIL)) NIL) ("2" (DELETE 2) (("2" (AUTO-REWRITE "prod_once" "prod_step" "pos_times_gt" "neg_times_lt" "parity_zero") (("2" (INDUCT "i") (("1" (REDUCE) NIL NIL) ("2" (SKOSIMP) (("2" (REWRITE "incr_even" +) (("2" (REWRITE "odd_not_even" +) (("2" (ASSERT) (("2" (STOP-REWRITE "prod_step") (("2" (REDUCE) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|prod_negative1| "" (SKOSIMP) (("" (USE "prod_negative") (("" (ASSERT) NIL NIL)) NIL)) NIL) (|prod_negative2| "" (SKOSIMP) (("" (REWRITE "odd_not_even") (("" (USE "prod_negative") (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL) (|prod_null| "" (SKOSIMP*) (("" (EXPAND "prod") (("" (ASSERT) (("" (USE "iter_swap_last[real]" ("i" "i!1")) (("" (ASSERT) (("" (REPLACE -1 + RL) (("" (DELETE -1) (("" (AUTO-REWRITE "iter" "swap") (("" (CASE "n!1 = m!1") (("1" (ASSERT) NIL NIL) ("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|prod_null2| "" (SKOSIMP) (("" (GROUND) (("1" (USE "prod_closure" ("P" "lambda x: x /= 0")) (("1" (GROUND) (("1" (DELETE -) (("1" (SKOSIMP) (("1" (INST?) NIL NIL)) NIL)) NIL)) NIL) ("2" (SKOSIMP) (("2" (ASSERT) (("2" (REWRITE "zero_times3") NIL NIL)) NIL)) NIL)) NIL) ("2" (FORWARD-CHAIN "prod_null") NIL NIL)) NIL)) NIL) (|prod_posreal_seq_is_posreal| "" (SKOLEM!) (("" (USE "prod_positive") (("" (SPLIT -) (("1" (ASSERT) NIL NIL) ("2" (ASSERT) NIL NIL) ("3" (DELETE 2) (("3" (REDUCE) NIL NIL)) NIL)) NIL)) NIL)) NIL) (|prod_nzreal_seq_is_nzreal| "" (SKOSIMP) (("" (REWRITE "prod_null2") (("" (REDUCE) NIL NIL)) NIL)) NIL) (|prod_nnreal_seq_is_nnreal| "" (SKOSIMP) (("" (USE* "prod_positive" "prod_null") (("" (GROUND) (("" (SKOLEM!) (("" (INST?) (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|prod_rat_seq_is_rat| "" (SKOLEM!) (("" (AUTO-REWRITE "rationals.closed_times") (("" (REWRITE "prod_closure") (("" (SKOSIMP) (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL) (|prod_posrat_seq_is_posrat| "" (SKOLEM!) (("" (USE* "prod_rat_seq_is_rat" "prod_posreal_seq_is_posreal") (("" (ASSERT) NIL NIL)) NIL)) NIL) (|prod_nzrat_seq_is_nzrat| "" (SKOLEM!) (("" (USE* "prod_rat_seq_is_rat" "prod_nzreal_seq_is_nzreal") NIL NIL)) NIL) (|prod_nnrat_seq_is_nnrat| "" (SKOLEM!) (("" (USE* "prod_rat_seq_is_rat" "prod_nnreal_seq_is_nnreal") NIL NIL)) NIL) (|prod_int_seq_is_int| "" (SKOLEM!) (("" (ASSERT) (("" (USE "prod_closure" ("P" "lambda x: rational_pred(x) AND integer_pred(x)")) (("1" (ASSERT) NIL NIL) ("2" (AUTO-REWRITE "closed_times") (("2" (SKOSIMP) (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|prod_posnat_seq_is_posnat| "" (SKOLEM!) (("" (USE* "prod_int_seq_is_int" "prod_posreal_seq_is_posreal") (("" (GROUND) NIL NIL)) NIL)) NIL) (|prod_nzint_seq_is_nzint| "" (SKOLEM!) (("" (USE* "prod_int_seq_is_int" "prod_nzreal_seq_is_nzreal") NIL NIL)) NIL) (|prod_nat_seq_is_nat| "" (SKOLEM!) (("" (USE* "prod_int_seq_is_int" "prod_nnreal_seq_is_nnreal") NIL NIL)) NIL) (|prod_TCC1| "" (SUBTYPE-TCC) NIL NIL) (|prod_TCC2| "" (SUBTYPE-TCC) NIL NIL) (|prod_TCC3| "" (TERMINATION-TCC) NIL NIL) (|prod_TCC4| "" (SUBTYPE-TCC) NIL NIL) (|variant_prod_zero| "" (GRIND) NIL NIL) (|variant_prod_one| "" (GRIND) NIL NIL) (|variant_prod_two| "" (GRIND) NIL NIL) (|variant_prod_equiv| "" (INDUCT "n") (("1" (GRIND) NIL NIL) ("2" (SKOSIMP*) (("2" (CASE-REPLACE "j!1 = 0") (("1" (DELETE -) (("1" (GRIND) NIL NIL)) NIL) ("2" (AUTO-REWRITE "prod_step") (("2" (ASSERT) (("2" (EXPAND "prod" 2 1) (("2" (INST?) (("2" (CASE "prod(0, j!1 - 1)((LAMBDA (i: nat): IF i < j!1 THEN a!1(i) ELSE 1 ENDIF)) = prod(0, j!1 - 1)(LAMBDA (i: nat): IF i < 1 + j!1 THEN a!1(i) ELSE 1 ENDIF)") (("1" (ASSERT) NIL NIL) ("2" (DELETE -1 3) (("2" (REWRITE "prod_same_elements") NIL NIL)) NIL) ("3" (SKOSIMP) (("3" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|variant_prod_split| "" (INDUCT-AND-REWRITE "n" 1 "prod") NIL NIL) (|variant_prod_permutation| "" (SKOSIMP) (("" (REWRITE "variant_prod_equiv") (("" (REWRITE "variant_prod_equiv") (("" (USE "prod_permutation" ("n" "0" "m" "n!1")) (("" (GROUND) (("" (DELETE 2) (("" (USE "perm_equiv[real]") (("" (ASSERT) (("" (DELETE 2) (("" (INST + "lambda (i: idx(0, n!1)): IF i