(* August 19, 1997 (as part of general overhaul) *)
script "logic_tools";
script "tableau2";
(* this file begins the development of Gries chapter 9 *)
(* quantifiers with range *)
defineconstant "forallr@?x" "forall@[((P1@?x)@?1)->((P2@?x)@?1)]";
(* the definition has to have universal range to be made scout *)
s "forallr@?x";
ri "forallr";
ri "FORALLBOOL"; ex();
right();
rri "forallr"; ex();
p "FORALLRBOOL";
makescout "forallr" "FORALLRBOOL";
(* version of forallr with pairs and which won't pop brackets off *)
(*
forallr2:
forallr @ [?R @ ?1] , [?P @ ?1] =
forall @ [(?R @ ?1) -> ?P @ ?1]
["BOOLDEF","CASEINTRO","EQBOOL","EQUATION","IF","NONTRIV","NOT","OR","P1","P2","REFLEX","forallr"]
*)
s "forallr@[?R@?1],[?P@?1]";
ri "forallr"; ex();
right();right();
ri "EVERYWHERE@PI1**PI2**EVAL"; ex();
p "forallr2";
defineconstant "forsomer@?x" "~forallr@(P1@?x),[~(P2@?x)@?1]";
(* the definition has to have universal range to be made scout *)
s "forsomer@?x";
ri "forsomer";
ri "NOTBOOL"; ex();
right();
rri "forsomer"; ex();
p "FORSOMERBOOL";
makescout "forsomer" "FORSOMERBOOL";
(* version of forsomer with pairs and which won't pop brackets off *)
(*
forsomer2:
forsomer @ [?R @ ?1] , [?P @ ?1] =
~forallr @ [?R @ ?1] , [~?P @ ?1]
["CASEINTRO","EQBOOL","NONTRIV","NOT","P1","P2","REFLEX","forsomer"]
*)
s "forsomer@[?R@?1],[?P@?1]";
ri "forsomer"; ex();
ri "EVERYWHERE@PI1**EVAL"; ex();
right();right();right();right();
ri "EVERYWHERE@PI2**EVAL"; ex();
p "forsomer2";
(* the natural theorem for ranged existential quantification *)
(*
forsomer3:
forsomer @ [?R @ ?1] , [?P @ ?1] =
forsome @ [(?R @ ?1) & ?P @ ?1]
["AND","ASSERT","BOOLDEF","CASEINTRO","CONVIF","EQBOOL","EQUATION","FNDIST","IF","IFF","IGNOREFIRST","NONTRIV","NOT","ODDCHOICE","OR","REFLEX","TYPES","XOR","forallr","forsome","forsomer"]
*)
s "forsomer@[?R@?1],[?P@?1]";
ri "forsomer2"; ex();
right();
ri "forallr2"; ex();
right();right();
ri "IDEF2"; ex();
ri "DEMa"; ex();
uptors "forsome2";
rri "forsome2"; ex();
p "forsomer3";
(* [true] is the universal range *)
(*
UNIV_RANGE_1:
forallr @ [true] , [?P @ ?1] =
forall @ [?P @ ?1]
["AND","ASSERT","BOOLDEF","CASEINTRO","CONVIF","EQBOOL","EQUATION","IF","IFF","IGNOREFIRST","NONTRIV","NOT","ODDCHOICE","OR","P1","P2","REFLEX","TYPES","XOR","forall","forallr"]
*)
s "forallr@[true],[?P@?1]";
ri "forallr2"; ex();
right();right();
ri "ILID"; ex();
ri "ASSERT"; ex();
top();
ri "FORALLBOOL2"; ex();
p "UNIV_RANGE_1";
(* a proof of Gries's One-Point Rule for universal quantification;
there really ought to be a shorter proof! *)
(*
ONEPOINT:
forallr @ [?1 = ?e] , [?P @ ?1] =
|-EVAL => ?P @ ?e
["AND","ASSERT","BOOLDEF","CASEINTRO","CONVIF","EQBOOL","EQUATION","IF","IFF","IGNOREFIRST","NONTRIV","NOT","ODDCHOICE","OR","P1","P2","REFLEX","TYPES","XOR","forall","forallr"]
*)
s "forallr@[?1=?e],[?P@?1]";
ri "forallr2"; ex();
right();right();
ri "TAB_IF"; ex();
right();left();left();right();
ri "0|-|1"; ex();
upto "[?P@?1]"; right();
rri "TAB_IF"; ex();
top();
ri "PCASEINTRO@(true=?P@?e)"; ex();
right();left();
right();right();right();
rri "0|-|1"; ex();
up();
ri "TAB_IF** $CASEINTRO"; ex();
up();up();
ri "FORALLDROP**AT"; ex();
up();right();
initializecounter();
rri "INSTANTIATE"; ex();
assign "?x_1" "?e";
left();
ri "EVAL"; ex();
ri "(LEFT@REFLEX)**TAB_IF"; ex();
ri "ODDCHOICE"; ex();
ri "1|-|1"; ex();
up();
ri "TAB_AND"; ex();
up();up();
rri "ODDCHOICE"; ex();
ri "ASSERT_UNEXP"; ex();
right(); ri "EVAL";
p "ONEPOINT";
(* tactics which convert between theorems of the forms
(|-?p) = ?p&?q and (?p->?q)=true *)
(* ?thm is expected to be of the form (|-?p) = ?p&?q *)
s "?p->?q";
ri "$IRULE2";
ri "LEFT@?thm";
ri "3pt76b";
prove "CONVERT_IMP_1@?thm";
(* ?thm is expected to be of the form (?p->?q) = true
Note that ?q needs to be supplied as a parameter along with ?thm *)
s "|-?p";
rri "CID"; ex();
right();
ri "DXMF@?q"; ex();
top();
ri "CDISD"; ex();
right();
rri "CRULE2"; ex();
ri "LEFT@ $DUBNEG2"; ex();
ri "DEMb"; ex();
right();
rri "IDEF2"; ex();
ri "?thm";
up();
rri "FDEF";
up();
ri "DID";
ri "CRULE1";
p "CONVERT_IMP_2@?thm,?q";
(* I will prove the "range free" form of Gries's theorem 9.12 *)
(*
PRE9pt12:
(forall @ [(?P @ ?1) -> ?Q @ ?1])
-> (forall @ [?P @ ?1]) -> forall @ [?Q @ ?1] =
true
["AND","ASSERT","BOOLDEF","CASEINTRO","CONVIF","EQBOOL","EQUATION","IF","IFF","IGNOREFIRST","NONTRIV","NOT","ODDCHOICE","OR","REFLEX","TYPES","XOR","forall"]
*)
s "(forall@[(?P@?1)->?Q@?1])->(forall@[?P@?1])->forall@[?Q@?1]";
ri "3pt65"; ex();
left();
rri "FORALLDIST"; ex();
right();right();
ri "CSYM";
ri "3pt66"; ex();
up();up();
ri "FORALLDIST"; ex();
up();
ri "(LEFT@CSYM)**3pt76b"; ex();
p "PRE9pt12";
(* implementation of Gries metatheorem 9.16 as a pair of tactics *)
(* here is a tactic for one direction of 9.16;
?thm is presumed to be a theorem of the form forall@[?P@?1] = true *)
(* 9pt16a1 is a subtactic of 9pt16a (and does most of its work) *)
(*
9pt16a1 @ ?thm:
?P @ ?x =
(LEFT @ ?thm) => (forall @ [?P @ ?1]) || true
, [?P @ ?1] @ ?x
["CASEINTRO","forall"]
*)
s "?P@?x";
ri "BIND@?x"; ex();
ri "PCASEINTRO@[?P@?1]=[true]"; ex();
right();left();
ri "(LEFT@0|-|1)**EVAL"; ex();
top();
ri "LEFT@ $forall2"; ex();
ri "LEFT@?thm";
prove "9pt16a1@?thm";
(*
9pt16a @ ?x , ?thm:
?y =
(9pt16a1 @ ?thm) => (BIND @ ?x) => ?y
["CASEINTRO","forall"]
*)
s "?y";
ri "BIND@?x";
ri "9pt16a1@?thm";
prove "9pt16a@?x,?thm";
(* the first parameter is the variable on which we are to quantify *)
(* the other direction of 9.16; here ?thm is assumed to be of the form
?P@?x = true *)
(*
9pt16b @ ?thm:
forall @ [?P @ ?1] =
(FORALLDROP ** AT) => forall @ [?thm => ?P @ ?1]
["AND","ASSERT","BOOLDEF","CASEINTRO","CONVIF","EQBOOL","EQUATION","FNDIST","IF","IFF","NONTRIV","NOT","ODDCHOICE","OR","REFLEX","TYPES","XOR","forall"]
*)
s "forall@[?P@?1]";
right();right();
ri "?thm";
top();
ri "FORALLDROP**AT";
p "9pt16b@?thm";
(* tactics implementing Gries 9.30 *)
(* we assume that ?thm is a theorem of the form (forsome @ [?P @ ?1])
-> ?Q = true *)
s "(?P@?x)->?Q";
ri "BIND@?x"; ex();
ri "PCASEINTRO@[(?P @ ?1) -> ?Q]=[true]";ex();
right();left();
ri "(LEFT@0|-|1)**EVAL"; ex();
top();left();
rri "forall"; ex();
ri "FORALL_IMP_FORSOME_EQ"; ex();
top();
ri "LEFT@?thm";
p "9pt30a@?thm";
(* here, we assume that ?thm is a theorem of the form ((?P@?x)->?Q)=true *)
s "(forsome @ [?P @ ?1]) -> ?Q";
rri "FORALL_IMP_FORSOME_EQ"; ex();
right();right();
ri "?thm";
top();
ri "FORALLDROP**AT";
p "9pt30b@?thm";
(* the point is that the tactics allow theorems of each of these
forms to be converted to theorems of the other form *)
quit();