(* further modified Mar 5-7 1998 *) (* Modifications May 22, 1998 wrt natural number subtraction *) (* August 19, 1997 (as part of general overhaul) *) (* Proof script with preliminaries for a theory of the natural numbers, integrated with the built-in arithmetic of Mark2 *) script "logicdefs"; (* script with basic logical definitions *) script "typestuff"; (* algorithms for handling type labels *) (* the naturals are a subtype of the reals, and arithmetic operations on the naturals coincide with the built-in arithmetic operations of the prover *) declareconstant "Nat"; (* type label for naturals *) declareconstant "Real"; (* type label for reals *) axiom "BUILTIN" "0+!?x" "Nat:?x"; (* implements fact that built-in numerals are of type Nat *) (* 0 and 1 are natural numbers *) start "Nat:1"; rri "BUILTIN"; ex(); workback(); prove "ONENAT"; start "Nat:0"; rri "BUILTIN"; ex(); workback(); prove "ZERONAT"; declareinfix "+"; declareinfix "*"; declareinfix "-"; (* this is _real_ subtraction *) declareprefix "-" "0"; declareinfix "/"; (* this is _integer_ division *) declareinfix "%"; declareinfix "<"; (* some familiar arithmetic operations *) axiom "PLUSTYPE" "?x+?y" "Real:(Real:?x)+Real:?y"; (* addition takes real inputs to a real output *) axiom "PLUSTYPE2" "(Nat:?x)+Nat:?y" "Nat:(Nat:?x)+Nat:?y"; (* a sum of natural numbers is a natural number *) axiom "PLUSCOMP" "(Nat:?x)+Nat:?y" "?x+!?y"; (* the built-in operation of addition coincides with natural number addition *) s "?x+?y"; ri "PLUSTYPE"; ex(); right(); left(); rri "TYPES"; ex(); up();right();rri "TYPES"; ex(); top();rri "PLUSTYPE"; ex(); p "PLUSSCIN"; makescin "+" "PLUSSCIN"; (* commands to establish that addition has s.c. input *) axiom "MINUSTYPE" "?x-?y" "Real:(Real:?x)-Real:?y"; axiom "MINUSCOMP" "(Nat:?x)-Nat:?y" "(?x> PLUSID => ?x + ?y ["PLUSCOMM","PLUSID"] *) s "?x+?y"; ri "PLUSID"; ari "COMMPLUSID"; p "EPLUSID"; (* COMMDIST: (?x + ?y) * ?z = (?x * ?z) + ?y * ?z *) s "(?x+?y)*?z"; ri "TIMESCOMM"; ri "DIST"; ex(); ri "RL@TIMESCOMM"; ex(); p "COMMDIST"; (* TIMESZERO: 0 * ?x = 0 ["BUILTIN","CASEINTRO","DIST","PLUSASSOC","PLUSCOMP","PLUSID","PLUSMINUS","PLUSTYPE","REFLEX","TIMESCOMM","TIMESTYPE","TYPES"] *) initializecounter(); s "0"; ri "REALZERO"; ex(); rri "PLUSMINUS";ex(); assign "?y_2" "0*?x"; right();left(); ri "REALZERO"; rri "PLUSID"; ex(); up(); ri "COMMDIST"; ex(); top(); rri "PLUSASSOC"; ex(); ri "LEFT@PLUSMINUS"; ex(); ri "LEFT@ \$REALZERO";ex(); ri "PLUSID"; ex(); ri "TREMTOP@TIMESTYPE"; ex(); workback(); p "TIMESZERO"; (* FACTORZERO: 0 = ?y * ?z = (0 = Real : ?y) | 0 = Real : ?z ["AND","BUILTIN","CASEINTRO","DIST","EQUATION","NONTRIV","NOT","ODDCHOICE","OR","PLUSASSOC","PLUSCOMP","PLUSID","PLUSMINUS","PLUSTYPE","REALDIVTYPE","REFLEX","TIMESASSOC","TIMESCOMM","TIMESDIV","TIMESTYPE","TYPES"] *) initializecounter(); s "0=?y*?z"; ri "CASEINTRO";ex(); assign "?y_1" "0=Real:?y"; right();left();right(); ri "TADDBOTH@TIMESTYPE"; ex(); left(); rri "0|-|1"; ex(); up(); ri "TIMESZERO"; ex(); up(); ri "REFLEX"; ex(); up();right(); ri "CASEINTRO"; ex(); assign "?y_17" "0=Real:?z"; right();left();right(); ri "TADDRIGHT@TIMESTYPE"; ex(); right(); rri "0|-|2"; ex(); up(); ri "TIMESCOMM"; ri "TIMESZERO"; ex(); up(); ri "REFLEX"; ex(); up();right(); ri "EQUATION"; ex(); right();left(); (* always work in the impossible case! *) rri "REFLEX"; ex(); assign "?a_31" "(((?y./.?y)./.?z)*?z)*?y"; left(); ri "TIMESASSOC"; ex(); right(); ri "TIMESCOMM"; ex(); rri "0|-|3"; ex();up(); ri "TIMESCOMM**TIMESZERO";ex(); up();right();left(); ri "TIMESDIV"; ex(); ri "1|-|2"; ex(); ri "TREMTOP@REALDIVTYPE"; ex(); up(); ri "TIMESDIV"; ex(); ri "1|-|1"; ex(); up(); ri "EQUATION**1|-|1"; ex(); uptors "CASEINTRO"; rri "CASEINTRO"; ex(); uptors "EQUATION"; ri "ODDCHOICE"; rri "EQUATION"; ex(); top(); ri "ODDCHOICE"; rri "ALTORDEF"; ex(); p "FACTORZERO"; (* More is needed; properties of order, for example *) (* Peano axioms *) axiom "SUCCNOTZERO" "0=1+Nat:?x" "false"; axiom "SAMESUCC" "(Nat:?x)=(Nat:?y)" "(1+Nat:?x)=(1+Nat:?y)"; axiom "INDUCTION" "forall@[?P@Nat:?1]" "(?P@0)&forall@[(?P@Nat:?1)->(?P@1+Nat:?1)]"; (* develop induction tactic *) s "forall@[?P@?1]"; right();right(); ri "BIND@Nat:?1"; p "INDUCT_TAC_1"; s "forall@[?P@Nat:?1]"; ri "INDUCTION"; ex(); left(); ri "EVAL"; up();right(); right();right(); left();ri "EVAL"; up();right();ri "EVAL"; p "INDUCT_TAC_2"; s "forall@[?P@?1]"; ri "INDUCT_TAC_1"; ri "INDUCT_TAC_2"; p "INDUCT_TAC"; (* define the notions "even" and "odd" *) defineconstant "even@?x" "forsome@[(Nat:?x)=(Nat:?1)+(Nat:?1)]"; defineconstant "odd@?x" "forsome@[(Nat:?x)=1+(Nat:?1)+(Nat:?1)]"; (* "axioms" for greatest common denominator *) declareconstant "gcd"; axiom "GCD1" "gcd @ ?a,0" "Nat:?a"; axiom "GCD2" "gcd @ ?a,?b" "gcd @?b,?a%?b"; axiom "GCDTYPE" "gcd @ ?a,?b" "gcd@(Nat:?a),Nat:?b"; (* EQEVAL2: (Nat : ?a) = 0 = ?a =! 0 ["BUILTIN","EVALEQ"] *) s "Nat:0"; rri "BUILTIN"; ex(); saveenv "ZeroLemma"; s "(Nat:?a)=0"; right(); applyconvenv "ZeroLemma"; top(); rri "EVALEQ"; ex(); p "EQEVAL2"; dropenv "ZeroLemma"; (* algorithm for computing GCD's *) initializecounter(); s "gcd@?a,?b"; ri "GCDTYPE"; ex(); ri "CASEINTRO"; ex(); assign "?y_2" "(Nat:?b)=0"; right();left();right();right(); ri "0|-|1"; ex(); up();up(); ri "GCD1"; ri "TYPES"; rri "BUILTIN"; ri "BUILTIN"; up();right(); rri "GCDTYPE"; ex(); ri "GCD2";ex(); dpt "GCD"; ri "GCD"; right();right();right();ri "MODCOMP"; up();up();up(); top();left();ri "EQEVAL2"; p "GCD"; (* s "gcd@10,14"; ri "GCD"; steps(); *) (* put type labels on numerals *) (* a "lemma" tactic *) (* TEMP_PIVOT: ?a || ?b , ?c = ?a || ((0 |-| 1) <= ?b) , ?c [] *) s "?a||?b,?c"; right();left(); rri "0|-|1"; p "TEMP_PIVOT"; (* duplicates NATCALC, alas *) (* TYPENUMERAL: ?n = (TEMP_PIVOT ** \$CASEINTRO) => (REFLEX => ?n = BUILTIN => BUILTIN <= Nat : ?n) || (Nat : ?n) , ?n ["BUILTIN","CASEINTRO","REFLEX"] *) s "?n"; ri "PCASEINTRO@?n=Nat:?n"; ex(); right();left(); ri "0|-|1"; ex(); up();up(); left(); ri "REFLEX"; right();right(); rri "BUILTIN";ri "BUILTIN"; top(); ri "TEMP_PIVOT** \$CASEINTRO"; p "TYPENUMERAL"; (* REALNUMERAL: ?n = (RIGHT @ \$BUILTIN) => REALNAT => TYPENUMERAL => ?n ["BUILTIN","CASEINTRO","PLUSCOMP","PLUSTYPE","REFLEX","TYPES"] *) s "?n"; ri "TYPENUMERAL"; ri "REALNAT"; ri "RIGHT@ \$BUILTIN"; p "REALNUMERAL"; (* REALNUMERAL2: Real : ?n = BUILTIN <= REALNAT <= (RIGHT @ TYPENUMERAL) => Real : ?n ["BUILTIN","CASEINTRO","PLUSCOMP","PLUSTYPE","REFLEX","TYPES"] *) s "Real:?n"; ri "RIGHT@TYPENUMERAL"; rri "REALNAT"; rri "BUILTIN"; p "REALNUMERAL2"; (* a new GCD tactic from Parvin *) dpt "FINDGCD"; s "gcd @ ?a,?b"; ri "GCD1";ari "GCD2**(RIGHT@RIGHT@MODCOMP)**FINDGCD"; p "FINDGCD"; (* definition of "less than"; beginning of theory of order *) axiom "LESS1" "(Nat:?x) < Nat:?y" "forsome @ [ (forall @ [(?1@1+Nat:?2) -> ?1@Nat:?2]) & (?1@Nat:?x) & ~(?1@Nat:?y)]"; (* definition of natural number subtraction *) defineinfix "NAT_SUB" "?x.-.?y" "((Nat:?x)