(* modified May 29, 1998: realorder is now called at the end *)

(* further modified Mar 5-7 1998 *)

(* August 19, 1997 (as part of general overhaul) *)

(* this file has further results in algebra and arithmetic plus some 
general-purpose tactics of an abstract algebraic character *)

script "naturals";
script "logicdefs2";

(*
ZEROORSUCC:

forall 
@ [(0 = Nat : ?1) | forsome 
   @ [(Nat : ?1) = 1 + Nat : ?2]] = 

true

["AND","ASSERT","BOOLDEF","CASEINTRO","CONVIF","EQBOOL","EQUATION","FNDIST","IF","IFF","INDUCTION","NONTRIV","NOT","ODDCHOICE","OR","PLUSTYPE","REFLEX","TYPES","XOR","forall","forsome"]



*)

s "forall@[(0=Nat:?1)| forsome@[(Nat:?1)=1+Nat:?2]]";
right(); right(); 
ri "BIND@Nat:?1";

top();
ri "INDUCTION"; ex();

left();
ri "EVAL"; ex();
ri "LEFT@REFLEX"; ex();
ri "DSYM"; ex();
ri "DZER"; ex();

up();right();

right();right();right();

ri "EVAL"; ex();

right();

ri "forsome"; ex();

right();

ri "forall"; ex();
ri "EQUATION"; ex();

right(); left();

ri "BIND@?1"; ex();
ri "LEFT@ $0|-|1"; ex();
ri "EVAL"; ex();
ri "RIGHT@REFLEX"; ex();
rri "FDEF"; ex();
up();up();
rri "CASEINTRO"; ex();
up();
ri "NEGF"; ex();
up();
ri "DZER"; ex();
up();
ri "IRZER"; ex();
up();up();
ri "forall**REFLEX"; ex();
up();
ri "CID"; ex();
ri "AT"; ex();

p "ZEROORSUCC";

(*

BREAKMINUS:

?x - ?y = 

?x +  -?y

["BUILTIN","CASEINTRO","MINUSTYPE","PLUSASSOC","PLUSCOMM","PLUSCOMP","PLUSID","PLUSMINUS","PLUSTYPE","REFLEX","TYPES"]


*)

initializecounter();
s "?x-?y";
ri "MINUSTYPE"; ex();
rri "PLUSID"; ex();
left();
ri "REALZERO"; ex();
rri "PLUSMINUS"; ex();
assign "?y_4" "?y";
up();
ri "PLUSASSOC"; ex();
right();
ri "PLUSCOMM"; ex();
ri "PLUSTYPE"; ex();
ri "EVERYWHERE@ $MINUSTYPE"; ex();
right();
ri "PLUSTYPE**(EVERYWHERE@TYPES)** $PLUSTYPE";ex();
ri "PLUSMINUS"; ex();
up();
ri "TYPES"; ex();
up();
ri "PLUSTYPE**(EVERYWHERE@TYPES)** $PLUSTYPE";ex();
ri "PLUSCOMM"; ex();
p "BREAKMINUS";

(*

MINUSPLUS:

(?x + ?y) - ?y = 

Real : ?x

["BUILTIN","CASEINTRO","MINUSTYPE","PLUSASSOC","PLUSCOMM","PLUSCOMP","PLUSID","PLUSMINUS","PLUSTYPE","REFLEX","TYPES"]

*)

s "(?x+?y)-?y";
ri "BREAKMINUS"; ex();
ri "PLUSASSOC"; ex();
right();
ri "PLUSCOMM**PLUSMINUS** $REALZERO"; ex();
up();
ri "COMMPLUSID"; ex();
p "MINUSPLUS";

(* a sublemma *)


(*

ADD_CANCEL:

(?z + ?x) = ?z + ?y = 

(Real : ?x) = Real : ?y


*)
initializecounter();
s "(?z+?x)=(?z+?y)";
ri "PCASEINTRO@(Real:?x)=Real:?y";ex();
right();left();
ri "RL@PLUSTYPE";
ri "EVERYWHERE@0|-|1"; ex();
ri "REFLEX"; ex();
up();right();
ri "EQUATION"; ex();
right();left();
ri "PCASEINTRO@((?z+?x) + -?z) = (?z+?y) + -?z"; ex();
right();left();
rri "1|-|3"; ex();
left();
ri "RL@PLUSCOMM**($PLUSASSOC)**(LEFT@PLUSMINUS** $REALZERO)**PLUSID";ex();
ri "EQUATION**1|-|1"; ex();
up();ex();
up();up();left();
ri "EVERYWHERE@0|-|2"; ex();
up();
ri "LEFT@REFLEX"; ex();
assign "?x_36" "false";
up();up();
rri "CASEINTRO"; ex();
up();up();
rri "EQUATION"; ex();
p "ADD_CANCEL";


(*

SUBTRACT_SUM:

?x - ?y + ?z = 

(?x - ?y) - ?z

["BUILTIN","CASEINTRO","MINUSTYPE","PLUSASSOC","PLUSCOMM","PLUSCOMP","PLUSID","PLUSMINUS","PLUSTYPE","REFLEX","TYPES"]

*)

initializecounter();
s "?x-?y+?z";
ri "MINUSTYPE"; ex();
rri "PLUSID"; ex();
right();
ri "TADDTOP@MINUSTYPE"; ex();
rri "MINUSTYPE"; ex();
ri "BREAKMINUS"; ex();
ri "PLUSCOMM"; ex();
top();
rri "PLUSASSOC"; ex();
left();left();
ri "REALNUMERAL"; ex();
rri "PLUSID";
ri "RL@REALNUMERAL** $PLUSMINUS"; ex();
assign "?y_39" "?y"; assign "?y_52" "?z";
ri "PLUSASSOC";ex(); right();
rri "PLUSASSOC"; ri "LEFT@PLUSCOMM"; ex();
ri "PLUSASSOC"; ex();
up();
rri "PLUSASSOC"; ex();
up();
ri "PLUSASSOC"; ex(); right();
ri "PLUSCOMM**PLUSMINUS";ex();
ri "REALNUMERAL2"; ex();
up();
ri "COMMPLUSID"; ex();
ri "TREMTOP@PLUSTYPE"; ex();
up();
ri "PLUSCOMM** $PLUSASSOC"; ex();
ri "(LEFT@ $BREAKMINUS)** $BREAKMINUS"; ex();
p "SUBTRACT_SUM";

s "-?x+?y";
ri "SUBTRACT_SUM"; ex();
ri "BREAKMINUS"; ex();
p "PLUSINVDIST";

dpt "PLUSINVDISTS";
s "-?x+?y";
ri "PLUSINVDIST"; ex();
right();ri "PLUSINVDISTS";
up();left();ri "PLUSINVDISTS";
p "PLUSINVDISTS";

(*

MINUSMINUS:

 - -?x = 

Real : ?x

["BUILTIN","CASEINTRO","MINUSTYPE","PLUSASSOC","PLUSCOMM","PLUSCOMP","PLUSID","PLUSMINUS","PLUSTYPE","REFLEX","TYPES"]

*)

initializecounter();
s "- -?x";
ri "MINUSTYPE"; ex();
rri "PLUSID"; ex();
ri "RIGHT@(TADDTOP@MINUSTYPE)** $MINUSTYPE"; ex();
left();
ri "REALNUMERAL";
rri "PLUSMINUS";ex();
assign "?y_25" "?x";
ri "PLUSCOMM"; ex();
top();
ri "PLUSASSOC"; ex();
right();
ri "PLUSCOMM**PLUSMINUS**REALNUMERAL2"; ex();
up();
ri "COMMPLUSID"; ex();
p "MINUSMINUS";

s "-0";
ri "BREAKMINUS**PLUSCOMM**PLUSMINUS"; ex();
ri "REALNUMERAL2"; ex();
p "MINUSZERO";

(*

SUBTRACT_DIFF:

?x - ?y - ?z = 

?x + ( -?y) + ?z

["BUILTIN","CASEINTRO","MINUSTYPE","PLUSASSOC","PLUSCOMM","PLUSCOMP","PLUSID","PLUSMINUS","PLUSTYPE","REFLEX","TYPES"]

*)

s "?x-(?y-?z)";
ri "BREAKMINUS"; ex();
right();right();
ri "BREAKMINUS"; ex();
up();
ri "PLUSINVDIST"; ex();
ri "RIGHT@MINUSMINUS"; ex();
ri "TREMRIGHT@PLUSTYPE"; ex();
p "SUBTRACT_DIFF";

(* some general purpose tactics; good examples of the programming power
of the tactic language *)

(* generalized associativity tactic *)

(* ASSOCS is actually an iterator for any theorem whatsoever *)

(* *> is the "on-success" control structure of the tactic language;
see the documentation or ask me *)

(*

ASSOCS @ ?thm:

?x = 

((ASSOCS @ ?thm) *> ?thm) => ?x

[]

*)

dpt "ASSOCS";
s "?x";
ri "(ASSOCS@?thm)*>?thm";
p "ASSOCS@?thm";

(*

ALLASSOCS @ ?thm:

?x = 

(RIGHT @ ALLASSOCS @ ?thm) => (ASSOCS @ ?thm) 
=> ?x

[]

*)

dpt "ALLASSOCS";
s "?x";
ri "ASSOCS@?thm";
ri "RIGHT@ALLASSOCS@?thm";
p "ALLASSOCS@?thm";

(* example *)

s "(?x|?y)|((?z|?w)|?u)|?q";
ri "ALLASSOCS@DASSOC"; ex();

(* get desired term using associative and commutative laws *)

s "?x ^+ ?y";
p "GET0@?x";

s "?y ^+ ?x";
ri "?comm";
p "GET1@?x,?comm";

s "?y ^+ ?x ^+ ?z";
rri "?assoc";
ri "LEFT@?comm";
ri "?assoc";
p "GET2@?x,?comm,?assoc";

dpt "GET";
s "?x";
ri "ASSOCS@?assoc";
ri "GET0@?y";
ari "RIGHT@GET@?y,?comm,?assoc";
ri "GET1@?y,?comm";
ari "GET2@?y,?comm,?assoc";
prove "GET@?y,?comm,?assoc";

(* example *)

s "?x + (?u + ?v + (?w+?e)+?f+?g) + ?q";
ri "GET@?e,PLUSCOMM,PLUSASSOC"; ex();

(* GET does not carry out all possible applications of associativity;
it only does enough applications to find its target *)



(* an extended example of programming; a tactic ALL_CANCEL is
developed which is good (but not perfect) at cancellations. *)

(* it now appears to be perfect *)

s "?x+?y";
ri "GET@?z,PLUSCOMM,PLUSASSOC";
prove "GETPLUS@?z";

s "0 + -?x";
ri "PLUSID"; ex();
ri "(RIGHT@MINUSTYPE)**TYPES**($MINUSTYPE)"; ex();
p "FIXBREAKMINUS";

s "(-?x)+?x";
ri "PLUSMINUS**REALNUMERAL2"; ex();
prove "ALL_CANCEL_1";

s "?x+ -?x";
ri "PLUSCOMM**ALL_CANCEL_1"; ex();
prove "ALL_CANCEL_2";

s "?x + (-?x) + ?y";
rri "PLUSASSOC";ex();
ri "(LEFT@PLUSCOMM**PLUSMINUS**REALNUMERAL2)**PLUSID"; ex();
prove "ALL_CANCEL_3";

s "(-?x) + ?x + ?y";
rri "PLUSASSOC";
ri "(LEFT@PLUSMINUS**REALNUMERAL2)**PLUSID"; ex();
prove "ALL_CANCEL_4";

s "(-?x)+?y";
right();
ri "GETPLUS@?x";
top();
ri "ALL_CANCEL_1";
ari "ALL_CANCEL_4";
prove "ALL_CANCEL_5";

s "?x+?y";
right();
ri "GETPLUS@ -?x";
top();
ri "ALL_CANCEL_2";
ari "ALL_CANCEL_3";
prove "ALL_CANCEL_6";

dpt "ALL_CANCEL_7";
s "?x";
ri "ALLASSOCS@PLUSASSOC";
ri "RIGHT@ALL_CANCEL_7";
ri "TREMRIGHT@PLUSTYPE";
ri "ALL_CANCEL_6";
ri "ALL_CANCEL_5";
prove "ALL_CANCEL_7";

s "?x";
ri "EVERYWHERE@BREAKMINUS**FIXBREAKMINUS";
ri "EVERYWHERE@PLUSINVDISTS";
ri "TOPDOWN@MINUSMINUS";
ri "EVERYWHERE@TYPES";
ri "EVERYWHERE@TREMLEFT@PLUSTYPE";
ri "EVERYWHERE@TREMRIGHT@PLUSTYPE";
ri "ALL_CANCEL_7";
ri "TREMTOP@PLUSTYPE";  (* June 26 change in TREMTOP allows this *)
ri "TREMTOP@MINUSTYPE";
prove "ALL_CANCEL";

s "(?x-?y) + (?y-?z) + (?z-?u) + (?u-?v)";
ri "ALL_CANCEL"; ex();

s "(?x + ?y - ?z) - (?y - ?z - ?x) - ?x + ?y + ?z"; 
ri "ALL_CANCEL"; ex();

(* the proof of a theorem from above redone with use of GET *)

initializecounter();
s "-?y+?z";
ri "MINUSTYPE"; ex();
rri "PLUSID"; ex();
ri "RIGHT@(TADDTOP@MINUSTYPE)** $MINUSTYPE"; ex();
left();
ri "REALNUMERAL"; ex();
rri "PLUSID";ex();
ri "RL@REALNUMERAL** $PLUSMINUS"; ex();
assign "?y_39" "?y"; assign "?y_52" "?z";
top();
ri "GETPLUS@ -?y + ?z"; ex();
right();
ri "GETPLUS@?y"; ex();
right();
ri "GETPLUS@?z"; ex();
up();
rri "PLUSASSOC";
up();
rri "PLUSASSOC";
ri "LEFT@PLUSMINUS**REALNUMERAL2"; ex();
ri "PLUSID";
ri "TREMTOP@PLUSTYPE"; ex();

(* draft typing tactics *)

s "?x";
ri "PLUSTYPE";
ari "(RIGHT@LEFT@TYPES** $REALZERO)*>MINUSTYPE";
ari "REALNUMERAL";
prove "REAL_TYPE_1";

s "?x";
ri "EVERYWHERE@REAL_TYPE_1";
ri "EVERYWHERE@TYPES";
prove "REAL_TYPE";

s "?x";
ri "TREMTOP@PLUSTYPE";
ri "TREMTOP@MINUSTYPE";
ri "TREMBOTH@MINUSTYPE";
ri "TREMBOTH@PLUSTYPE";
ri "TYPES";
prove "REAL_UNTYPE_1";



s "?x";
ri "EVERYWHERE@REAL_UNTYPE_1"; 
prove "REAL_UNTYPE";

(*

SIGNPULL:

?x * -?y = 

-?x * ?y

["BUILTIN","CASEINTRO","DIST","MINUSTYPE","PLUSASSOC","PLUSCOMM","PLUSCOMP","PLUSID","PLUSMINUS","PLUSTYPE","REFLEX","TIMESCOMM","TIMESTYPE","TYPES"]

*)


s "?x* -?y";
ri "TADDTOP@TIMESTYPE"; ex();
rri "PLUSID"; ex();
left();
initializecounter();
ri "REALZERO";
rri "PLUSMINUS"; ex();
assign "?y_2" "?x*?y";
top();
ri "PLUSASSOC"; ex();
right();
rri "DIST"; ex();
right();
ri "PLUSCOMM**PLUSMINUS** $REALZERO"; ex();
up();
ri "TIMESCOMM**TIMESZERO"; ex();
up();
ri "COMMPLUSID**TREMTOP@MINUSTYPE"; ex();
prove "SIGNPULL";

(* expansion algorithm *)

dpt "X";

s "?x+?y";
left();ri "X";
up();right(); ri "X";
top();
ri "ALLASSOCS@PLUSASSOC";
p "X1";

s "?x*?y";
left();ri "X";
up();right(); ri "X";
top();
ri "ALLASSOCS@TIMESASSOC";
ri "DIST";
ari "COMMDIST";
ri "X1";
p "X2";

s "?x";
ri "X1";
ari "X2";
p "X";

(* should create a term sorting algorithm, then aim for a pretty expansion
and collection algorithm *)

s "(Real:?m)=Real:?n";
initializecounter();
rri "ADD_CANCEL"; ex();
assign "?z_1" "-?n";
right(); ri "PLUSMINUS"; rri "REALZERO"; ex();
up();left(); ri "PLUSCOMM"; rri "BREAKMINUS"; ex();
p "EQUATION_TO_DIFFERENCE";

(* insert theory of order on the reals *)

script "realorder";

quit();