(* August 20th, 1997 (added more comments) *)

(* this file contains "structural" tactics; these tactics enable
applications of theorems and tactics to subexpressions of expressions
under consideration, and allow program constructions such as composition
and looping to be applied to tactics *)

(* this construction is used to attach labels to terms and to
make copies of terms *)

(* there is also a development of abstraction algorithms and
algorithms for manipulation of case expressions predating the development
of hard-wired abstraction and local hypothesis manipulation *)

defineinfix "IGNOREFIRST" "?x.?y" "?y";

(* adapts to change in preamble; proves redundant "axioms"
in preamble *)

ae "P1";  prove "PI1";

ae "P2"; prove "PI2";

ae "Id"; prove "ID";

(* parameterized "CASEINTRO" *)

initializecounter();
s "?x";
ri "CASEINTRO"; ex();
assign "?y_1" "?p";
prove "PCASEINTRO@?p";

(* elimination of FNDIST *)

s "?f@?x||?y,?z";
ri "PCASEINTRO@?x"; ex();
right();left();right();
ri "1|-|1"; ex();
up();up();right();right();
ri "1|-|1"; ex();
proveanaxiom "FNDIST";

(* elimination of HYP *)

s "(?a=?b)||(?f@?a),?c";
right();left();right();
ri "0|-|1"; ex();
proveanaxiom "HYP";


(* Structural tactics taken from Parvin's file *)

(* these allow application of theorems to left and right subterms,
reversal of the direction of a theorem, and composition of theorems *)

(* ************************ methods ****************************** *)

(* theorem/tactic composition *)

(*

?thm1 ** ?thm2:

?x = 

?thm2 => ?thm1 => ?x

[]

*)

s "?x"; ri "?thm1"; ri "?thm2"; p "?thm1**?thm2";

(* reverse direction of theorem *)

(*

$?thm:

?x = 

?thm <= ?x

*)

s "?x"; rri "?thm"; p "$?thm";

(* apply theorem to left subterm *)

(*

LEFT @ ?thm:

?p ^+ ?q = 

(?thm => ?p) ^+ ?q

[]

*)

s "?p ^+ ?q"; left(); ri "?thm"; p "LEFT@?thm";

(* apply theorem to right subterm *)

(*

RIGHT @ ?thm:

?p ^+ ?q = 

?p ^+ ?thm => ?q

[]

*)

s "?p ^+ ?q"; right(); ri "?thm"; p "RIGHT@?thm";

(* apply theorem to both left and right subterms *)

(*

RL @ ?thm:

?p ^+ ?q = 

(?thm => ?p) ^+ ?thm => ?q

[]

*)

s "?p ^+ ?q"; left(); ri "?thm"; up(); right(); ri "?thm"; p "RL@?thm";

s "?x||?y,?z";
right();left(); ri "?thm";
p "LEFT_CASE@?thm";
s "?x||?y,?z";
right();right(); ri "?thm";
p "RIGHT_CASE@?thm";



(* this section develops tactics for implementation of aggressive rewriting *)

(* development of EVERYWHERE tactic *)

(* this tactic does not rewrite inside abstractions or inside the
defining equation or other proposition of a case expression *)

(* EVERYWHERE rewrites from the bottom up, while the new TOPDOWN
rewrites from the top down; this distinction can be important *)

(* EVERYWHERE comes in two flavors: EVERYWHERE itself does not rewrite
into defining equations of case expressions or into brackets, while
EVERYWHERE2 rewrites into these contexts as well *)

(* the structure of EVERYWHERE and EVERYWHERE2 exemplifies a way that
recursively defined tactics can share code *)

(* subtactics of EVERYWHERE and EVERYWHERE2 *)

s "?a||?x,?y";  (* changed Apr. 17 *)
right();left();
ri "?EVERYWHERE@?thm";
up();right();
ri "?EVERYWHERE@?thm";
top();
ri "?thm";
prove "EVERYWHERE_CASE@?EVERYWHERE,?thm";

s "?a||?x,?y";  (* new Aug. 15 '97 *)
right();left();
ri "?EVERYWHERE@?thm";
up();right();
ri "?EVERYWHERE@?thm";
top();
left(); ri "?EVERYWHERE@?thm"; up();
ri "?thm";
p "STRONG_EVERYWHERE_CASE@?EVERYWHERE,?thm";

s "[?f@?1]";
right(); ri "?EVERYWHERE@?thm";
up(); 
ri "?thm";
p "EVERYWHERE_ABS@?EVERYWHERE,?thm";
 

declareopaque "^+";

s "?x^+?y";
right();
ri "?EVERYWHERE@?thm";
up();left();
ri "?EVERYWHERE@?thm";
top();
ri "?thm";
p "EVERYWHERE_INFIX@?EVERYWHERE,?thm";

dpt "EVERYWHERE";

(* apply theorem to all subterms, bottom-up,
excluding defining equations of case expressions
and innards of abstraction terms *)

(*

EVERYWHERE @ ?thm:

?x = 

?thm =>> (EVERYWHERE_INFIX @ EVERYWHERE , ?thm) 
=>> (EVERYWHERE_CASE @ EVERYWHERE , ?thm) => ?x

[]


*)

s "?x";
ri "EVERYWHERE_CASE@EVERYWHERE,?thm";
ari "EVERYWHERE_INFIX@EVERYWHERE,?thm";
ari "?thm";  (* changed from ri on June 24th *)
prove "EVERYWHERE@?thm";

dpt "EVERYWHERE2";

(* as EVERYWHERE, without subterm restriction *)

(*

EVERYWHERE2 @ ?thm:

?x = 

?thm =>> (EVERYWHERE_ABS @ EVERYWHERE2 , ?thm) 
=>> (EVERYWHERE_INFIX @ EVERYWHERE2 , ?thm) 
=>> (STRONG_EVERYWHERE_CASE @ EVERYWHERE2 , ?thm) 
=> ?x

[]

*)

s "?x";
ri "STRONG_EVERYWHERE_CASE@EVERYWHERE2,?thm";
ari "EVERYWHERE_INFIX@EVERYWHERE2,?thm";
ari "EVERYWHERE_ABS@EVERYWHERE2,?thm";
ari "?thm";
prove "EVERYWHERE2@?thm";

(* apply theorem everywhere, top-down, restricted as EVERYWHERE *)

(* development of TOPDOWN tactic *)

dpt "TOPDOWN";

s "?a||?x,?y";
ri "?thm";
ri "RIGHT@RL@TOPDOWN@?thm";
prove "TOPDOWN_CASE@?thm";

s "?x^+?y";
ri "?thm";
ri "RL@TOPDOWN@?thm";
prove "TOPDOWN_INFIX@?thm";

s "?x";
ri "TOPDOWN_CASE@?thm";
ari "TOPDOWN_INFIX@?thm";
ari "?thm";
prove "TOPDOWN@?thm";


(* development of a synthetic abstraction algorithm *)

(* this is what I used to use before introducing variable binding *)

axiom "RSFN" "?f:^+?g" "[(?f:^+?g)@?1]";

(* this axiom ensures that objects introduced by RAISE are functions *)

(* I might not necessarily want this to be true; in some contexts, it is
better to suppose that the raised abstractions are intensional objects *)

declaretypedinfix 0 0 "^&";

(*

RAISE0:

(?f @ ?x) ^& ?g @ ?x = 

(?f :^& ?g) @ ?x

[]

*)

s "(?f@?x)^&(?g@?x)";
ri "RAISE"; ex();
p "RAISE0";

dpt "ABSTRACT";

(*

ABSTRACT1 @ ?x:

?x = 

Id @ ?x

["ID"]

*)

s "?x";
rri "ID";ex();
p "ABSTRACT1@?x";

(*

ABSTRACT2 @ ?x:

?f @ ?a = 

COMP <= ?f @ (ABSTRACT @ ?x) => ?a

["COMP"]

*)

s "?f@?a";
rri "COMP";
right(); right(); ri "ABSTRACT@?x";
prove "ABSTRACT2@?x";

(*

ABSTRACT3 @ ?x:

?a ^& ?b = 

RAISE0 => ((ABSTRACT @ ?x) => ?a) 
^& (ABSTRACT @ ?x) => ?b

[]

*)

s "?a^&?b";
right();
ri "ABSTRACT@?x";
up();left();
ri "ABSTRACT@?x";
top();
ri "RAISE0";
prove "ABSTRACT3@?x";

(*

ABSTRACT4 @ ?x:

?a = 

[?a] @ ?x

[]

*)

s "?a";
ri "BIND@?x"; ex();
p "ABSTRACT4@?x";

(* ABSTRACT@term will (attempt to) express a target term as a function
of its parameter "term" *)

(*

ABSTRACT @ ?x:

?a = 

(ABSTRACT4 @ ?x) =>> (ABSTRACT3 @ ?x) 
=>> (ABSTRACT2 @ ?x) =>> (ABSTRACT1 @ ?x) => ?a

["COMP","ID"]

*)

s "?a";
ri "ABSTRACT1@?x";
ari "ABSTRACT2@?x";
ari "ABSTRACT3@?x";
ari "ABSTRACT4@?x";
p "ABSTRACT@?x";

(* REDUCE will reverse the effect of ABSTRACT; it will "evaluate"
functions built by ABSTRACT *)

(*

REDUCE:

?f @ ?x = 

(ABSTRACT4 @ ?x) <<= ((RL @ REDUCE) *> RAISE0) 
<<= ((RIGHT @ REDUCE) *> COMP) =>> ID => ?f @ ?x

["COMP","ID"]

*)

dpt "REDUCE";
s "?f@?x";
ri "ID";
ari "(RIGHT@REDUCE)*>COMP";
arri "(RL@REDUCE)*>RAISE0";
arri "ABSTRACT4@?x";
prove "REDUCE";

(* impredicative synthetic abstraction and reduction is 
under development in the file lambda.mk2 *)

(* old approach to hypotheses *)

(*

PIVOT:

(?a = ?b) || ?T , ?U = 

(RIGHT @ LEFT @ EVAL) => HYP => (?a = ?b) 
|| ((BIND @ ?a) => ?T) , ?U

["HYP"]

*)

s "(?a=?b)||?T,?U";
right();left();
ri "BIND@?a";
top();
ri "HYP";
ri "LEFT_CASE@EVAL";
p "PIVOT";

(*

REVPIVOT:

(?a = ?b) || ?T , ?U = 

(LEFT_CASE @ EVAL) => HYP <= (?a = ?b) 
|| ((BIND @ ?b) => ?T) , ?U

["HYP"]

*)

s "(?a=?b)||?T,?U";
right();left();
ri "BIND@?b";
top();
rri "HYP";
ri "LEFT_CASE@EVAL";
p "REVPIVOT";

(* reverse forms of projection axioms *)

s "?x"; 
initializecounter();
rri "PI1"; ex();
assign "?y_1" "?y";
p "PI1F@?y";

s "?x"; 
initializecounter();
rri "PI2"; ex();
assign "?x_1" "?y";
p "PI2F@?y";

(* tool for expressing a term as a function of a pair *)

s "?t";
ri "BIND@?x,?y";
ri "LEFT@VALUE@[BIND@?x]";
ri "LEFT@VALUE@[RIGHT@PI1F@?y]";
ri "LEFT@VALUE@[LEFT@VALUE@[BIND@?y]]";
ri "LEFT@VALUE@[LEFT@VALUE@[RIGHT@PI2F@?x]]";
ri "LEFT@VALUE@[LEFT@VALUE@[EVAL]]";
ri "LEFT@VALUE@[EVAL]";
ri "EVAL";
ri "BIND@?x,?y";
prove "PAIRBIND@?x,?y";

(* example *)

s "(?f@?x)=(?g@?y)=(?h@?x,?y)";
ri "PAIRBIND@?x,?y"; ex();

(* tool for expressing a term as a function of a list *)

dpt "LISTBIND";

s "?t";
ri "EVAL*>LISTBIND@?y";
ri "EVAL*>PAIRBIND@?y";
ri "PAIRBIND@?x,?y";
prove "LISTBIND@?x,?y";

(* example -- note the format of the argument list *)

s "?x=?y=?z";
ri "LISTBIND@?x,?y,?z,0"; ex();

(* development of loop tactic *)


(* STARTLOOP:

?x = 

?x . ?x

["IGNOREFIRST"]
  *)


initializecounter();
s "?x";
rri "IGNOREFIRST"; ex();
assign "?x_1" "?x";
p "STARTLOOP";


(* STOPLOOP:

?x . ?x = 

?x

["IGNOREFIRST"]
  *)

s "?x.?x";
ri "IGNOREFIRST"; ex();
p "STOPLOOP";

(* the loop body *)

dpt "ALL_STEPS";

(* ALL_STEPS:

?x . ?y = 

ALL_STEPS =>> STOPLOOP => (RIGHT @ ?ONE_STEP) 
=> STARTLOOP => IGNOREFIRST => ?x . ?y

["AND","BOOLDEF","CASEINTRO","CONVIF","EQUATION","IF","IFF","IGNOREFIRST","NONTRIV","NOT","ODDCHOICE","OR","REFLEX","XOR"]
  *)

s "?x.?y";
ri "IGNOREFIRST";
ri "STARTLOOP";
ri "RIGHT@?ONE_STEP";
ri "STOPLOOP";
ari "ALL_STEPS@?ONE_STEP";
prove "ALL_STEPS@?ONE_STEP";

(* the loop itself *)

s "?x";
ri "STARTLOOP";
ri "ALL_STEPS@?ONE_STEP";
p "LOOP_TAC@?ONE_STEP";





quit();