(* 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<!?y)||(0-(?y-!?x)),?x-!?y";

(* MINUSCOMP relates the builtin natural number subtraction to real
subtraction -- be careful! *)

s "?x-?y";
ri  "MINUSTYPE"; ex();
right(); left();
rri "TYPES"; ex();
up();right();rri "TYPES"; ex();
top();rri "MINUSTYPE"; ex();
p "MINUSSCIN"; makescin "-" "MINUSSCIN";


(* naturals are a subtype of reals *)

s "Nat:?x";
rri "BUILTIN";ex();
rri "PLUSCOMP"; ex();
ri "PLUSTYPE"; ex();
saveenv "SubtypeLemma";
rri "TYPES"; ex();
right(); applyconvenv "SubtypeLemma";
p "REALNAT";
dropenv "SubtypeLemma";

(* commands to establish that subtraction has s.c. input *)
(* created by simple editing of commands for addition *)

axiom "TIMESTYPE" "?x*?y" "Real:(Real:?x)*Real:?y";
axiom "TIMESTYPE2" "(Nat:?x)*Nat:?y" "Nat:(Nat:?x)*Nat:?y";
axiom "TIMESCOMP" "(Nat:?x)*(Nat:?y)" "?x*!?y";
s "?x*?y";
ri  "TIMESTYPE"; ex();
right(); left();
rri "TYPES"; ex();
up();right();rri "TYPES"; ex();
top();rri "TIMESTYPE"; ex();
p "TIMESSCIN"; makescin "*" "TIMESSCIN";

(* ditto for multiplication *)

(* division and remainder as integer operations *)

axiom "DIVTYPE" "?x/?y" "Nat:(Nat:?x)/Nat:?y";
axiom "DIVCOMP" "?x/?y" "?x/!?y";
s "?x/?y";
ri  "DIVTYPE"; ex();
right(); left();
rri "TYPES"; ex();
up();right();rri "TYPES"; ex();
top();rri "DIVTYPE"; ex();
p "DIVSCIN"; makescin "/" "DIVSCIN";

(* ditto for division *)

axiom "MODTYPE" "?x%?y" "Nat:(Nat:?x)%Nat:?y";
axiom "MODCOMP" "?x%?y" "?x%!?y";
s "?x%?y";
ri  "MODTYPE"; ex();
right(); left();
rri "TYPES"; ex();
up();right();rri "TYPES"; ex();
top();rri "MODTYPE"; ex();
p "MODSCIN"; makescin "%" "MODSCIN";

(* ditto for remainder *)

axiom "LESSTYPE" "?x<?y" "(Real:?x)<Real:?y";
axiom "LESSCOMP" "(Nat:?x)<(Nat:?y)" "?x<!?y";
makescin "<" "LESSTYPE";

axiom "EVALEQ" "?x=!?y" "(Nat:?x)=Nat:?y";

(*

ZERONOTONE:

0 = 1 = 

false

*)

s "0=1";
ri "(LEFT@ZERONAT)**RIGHT@ONENAT";
rri "EVALEQ"; ex();
p "ZERONOTONE";

(* the preceding axioms handle built-in relations on naturals *)

(* real division *)

declareinfix "./.";
axiom "REALDIVTYPE" "?x./.?y" "Real:(Real:?x)./.Real:?y";
axiom "REALDIVCOMP" "(Nat:?x)./.Nat:?y" "(?x/!?y)+(?x%!?y)./.?y";
s "?x./.?y";
ri  "REALDIVTYPE"; ex();
right(); left();
rri "TYPES"; ex();
up();right();rri "TYPES"; ex();
top();rri "REALDIVTYPE"; ex();
p "REALDIVSCIN"; makescin "./." "REALDIVSCIN";

initializecounter();
s "?x"; ri "CASEINTRO"; ex();
assign "?y_1" "?x=Nat:?x";
right();left();ri"0|-|1";ex();
p "NATCALCEXPAND";
top(); ri "LEFT@(RIGHT@ $BUILTIN)**REFLEX**(RIGHT@BUILTIN)";
rri "NATCALCEXPAND";
p "NATCALC";

(* NATCALC is a hack to attach type label NAT to built in numerals *)
(* TYPENUMERAL below does the same thing *)

(* The application is to enable use of the axioms like PLUSCOMP *)

s "2 + 2";  ri "(RL@NATCALC)**PLUSCOMP"; ex();

(* example of carrying out a calculation *)

s "3 ./. 2"; ri "(RL@NATCALC)**REALDIVCOMP";

(* a perhaps more striking example *)

(* this ends a section in which the foundation is provided for recognizing
natural numbers as a type which includes the built-in numerals and whose
basic operations coincide with the built-in operations on numerals *)

(* axioms of real algebra *)

axiom "PLUSCOMM" "?x+?y" "?y+?x";
axiom "PLUSASSOC" "(?x+?y)+?z" "?x+?y+?z";
axiom "PLUSID" "0+?x" "Real:?x";
axiom "PLUSMINUS" "(?x-?y)+?y" "Real:?x";

axiom "TIMESCOMM" "?x*?y" "?y*?x";
axiom "TIMESASSOC" "(?x*?y)*?z" "?x*?y*?z";
axiom "TIMESID" "1*?x" "Real:?x";
axiom "TIMESINTDIV" "(?x%?y)+(?x/?y)*?y" "Nat:?x";
axiom "TIMESDIV" "(?x./.?y)*?y" "(0=Real:?y)||0,Real:?x";

axiom "DIST" "?x*?y+?z" "(?x*?y)+?x*?z";

(* some basic algebra theorems *)

(*

REALZERO:

0 = 

Real : 0

["BUILTIN","CASEINTRO","PLUSCOMP","PLUSTYPE","REFLEX","TYPES"]

*)

s "0";
ri "NATCALC"; ri "REALNAT"; ri "RIGHT@ $BUILTIN"; ex();
p "REALZERO";

(*

COMMPLUSID:

?x + 0 = 

Real : ?x

["PLUSCOMM","PLUSID"]

*)

s "?x+0";
ri "PLUSCOMM"; ri "PLUSID"; ex();
p "COMMPLUSID";

(*

EPLUSID:

?x + ?y = 

COMMPLUSID =>> 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)<Nat:?y)||0,Nat:(Nat:?x)-Nat:?y";


axiom "NATMINUSCOMP" "(Nat:?x).-.(Nat:?y)" "?x-!?y";

s "(Nat:?x).-.Nat:?y";
ri "NAT_SUB"; ex();
ri "EVERYWHERE2@TYPES"; ex();
rri "NAT_SUB"; ex();
wb();
p "NATMINUSSCIN";
makescin ".-." "NATMINUSSCIN";

s "Nat:(Nat:?x).-.(Nat:?y)";
ri "RIGHT@NAT_SUB"; ex();
ri "EVERYWHERE2@TYPES"; ex();
ri "PCASEINTRO@((Nat : ?x) < Nat : ?y)";ex();
right(); left(); ri "RIGHT@1|-|1"; ex();
up(); right(); ri "RIGHT@1|-|1"; ex();
ri "TYPES"; ex();
up(); left(); rri "ZERONAT"; ex();
top(); rri "NAT_SUB"; ex();
wb();
p "NATMINUSTYPE";

(* The old version of NAT_SUB *)

s "((Nat:?x)<Nat:?y)||0,(Nat:?x)-Nat:?y";
drls "MINUSCOMP"; ri "MINUSCOMP"; ex();
ri "LEFT@ $LESSCOMP"; ri "1|-|1"; ex();
rri "NATMINUSCOMP"; ri "NAT_SUB"; ex();
ri "EVERYWHERE2@TYPES"; ri "1|-|1"; ex();
top(); rri "NAT_SUB"; ex();
wb();
p "NAT__SUB";

defineconstant "Pred@?x" "?x.-.1";
s "Pred@?x";
ri "Pred"; ex();
ri "NATMINUSSCIN"; ri "RIGHT@ $ONENAT"; rri "Pred"; ex();
p "PREDSCIN";
makescin "Pred" "PREDSCIN";

s "Pred@?x";
ri "PREDSCIN"; ex();
ri "Pred"; ex();
ri "TADDTOP@NATMINUSTYPE"; ex();
ri "RIGHT@ $Pred"; ex();
p "PREDTYPE";

quit();