(* 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();