(* August 18, 1997 (as part of general overhaul) *) (* this file includes definitions and scin/scout results for the logical connectives and the quantifiers--it also includes some very simple basic theorems about these operators, proven "by hand" *) (* include prerequisite files *) script "structural"; script "lambda"; (* symmetry of equality -- one of those basic results! *) (* EQSYMM: ?x = ?y = ?y = ?x ["CASEINTRO","EQUATION","REFLEX"] *) initializecounter(); s "?x=?y"; ri "CASEINTRO"; ex(); assign "?y_1" "?y=?x"; right();left();right(); ri "0|-|1"; ex(); up(); ri "REFLEX"; ex(); up();right(); ri "EQUATION"; ex(); right();left(); rri "REFLEX";ex(); assign "?a_4" "?x"; left(); ri "0|-|2"; ex(); up(); ri "EQUATION"; ri "1|-|1"; ex(); up();up(); rri "CASEINTRO"; ex(); top(); rri "EQUATION";ex(); p "EQSYMM"; (* definition of the boolean type *) declareconstant "bool"; axiom "EQBOOL" "?x=?y" "bool:?x=?y"; makescout "=" "EQBOOL"; (* quantifiers *) defineconstant "forall@?P" "[?P@?1] = [true]"; s "forall@?P"; ri "forall";ex(); ri "EQBOOL";ex(); right(); rri "forall";ex(); p "FORALLBOOL"; makescout "forall" "FORALLBOOL"; (* forall2 is used to prevent "losing the brackets" when the theorem is applied in reverse *) (* forall2: forall @ [?P @ ?1] = [?P @ ?1] = [true] ["forall"] *) s "forall@[?P@?1]"; ri "forall"; ex(); p "forall2"; defineinfix "NOT" "?x~?y" "(true=?y)||false,true"; declareprefix "~" "true"; s "~?x"; left(); up(); ri "NOT"; ex(); initializecounter(); s "(true=?y)||false,true"; rri "NOT"; ex(); (* NOT1: ~?y = (true = ?y) || false , true ["NOT"] *) assign "?x_1" "true"; workback(); p "NOT1"; initializecounter(); s "?x~?y"; ri "NOT"; ex(); right();left(); rri "NONTRIV"; ri "EQBOOL"; ex(); right(); ri "NONTRIV"; ex(); up(); ri "BIND@false"; ex(); up();right(); rri "REFLEX"; ri "EQBOOL"; ex(); right(); ri "REFLEX"; ex(); up(); ri "BIND@true"; ex(); top(); rri "FNDIST"; ex(); ri "EVAL";ex(); right(); rri "NOT"; ex(); assign "?x_9" "?x"; p "NOTBOOL"; makescout "~" "NOTBOOL"; (* Note that it is necessary to treat a prefix operator as a binary operator to declare it "scout" *) (* The point here is to tell the prover that ~ has "output" in the boolean type *) defineconstant "forsome@?P" "~forall@[~?P@?1]"; s "forsome@?P"; ri "forsome"; ri "NOTBOOL"; ex(); right(); rri "forsome"; ex(); p "FORSOMEBOOL"; makescout "forsome" "FORSOMEBOOL"; (* used to prevent loss of brackets, as "forall2" *) (* forsome2: forsome @ [?P @ ?1] = ~forall @ [ ~?P @ ?1] *) s "forsome@[?P@?1]"; ri "forsome"; ex(); p "forsome2"; (* "true" and "false" are boolean *) s "true"; rri "REFLEX"; ri "EQBOOL"; ex(); right(); ri "REFLEX"; ex(); p "TRUEBOOL"; s "false"; rri "NONTRIV"; ri "EQBOOL"; ex(); right(); ri "NONTRIV"; ex(); p "FALSEBOOL"; axiom "BOOLDEF" "bool:?x" "true=?x"; (* the axiom EQBOOL is redundant, given BOOLDEF *) s "?x=?y"; ri "EQUATION"; ri "ODDCHOICE"; rri "EQUATION"; rri "BOOLDEF"; ex(); proveanaxiom "EQBOOL"; defineinfix "AND" "?x&?y" "(true=?x)||(true=?y),false"; s "?x&?y"; ri "AND"; ex(); right();left(); ri "EQBOOL"; ri "BIND@true=?y"; ex(); up();right();ri "FALSEBOOL"; ri "BIND@false"; ex(); top(); rri "FNDIST"; ri "EVAL"; ex(); right(); rri "AND"; ex(); p "ANDBOOL"; makescout "&" "ANDBOOL"; (* After this, the typing declarations get easier *) defineinfix "OR" "?x|?y" "~(~?x)& ~?y"; s "?x|?y"; ri "OR";ex(); ri "NOTBOOL";ex(); right(); rri "OR";ex(); p "ORBOOL"; makescout "|" "ORBOOL"; (* an alternative definition of "or", more similar to that of "and" *) (* ALTORDEF: ?x | ?y = (true = ?x) || true , true = ?y ["AND","CASEINTRO","EQUATION","NONTRIV","NOT","OR","REFLEX"] *) initializecounter(); s "?x|?y"; ri "OR"; ex(); ri "CASEINTRO"; ex(); assign "?y_2" "true=?x"; right(); left(); right();left();right(); rri "0|-|1"; ex(); up(); ri "NOT"; ri "LEFT@REFLEX"; ex(); up(); ri "NOT"; ri "LEFT@NONTRIV"; ex(); ri "AND"; ri "LEFT@NONTRIV"; ex(); up(); ri "NOT"; ri "LEFT@NONTRIV"; ex(); up(); right(); right();left(); ri "NOT"; ri "1|-|1"; ex(); up(); ri "AND"; ri "LEFT@REFLEX"; ex(); up(); ri "CASEINTRO"; ex(); assign "?y_17" "true=?y"; right();left(); right();right(); ri "NOT"; ri "1|-|2"; ex(); up(); ri "NONTRIV"; ex(); up(); ri "NOT"; ri "LEFT@NONTRIV"; ex(); up(); right(); right(); right(); ri "NOT"; ri "1|-|2"; ex(); up(); ri "REFLEX"; ex(); up(); ri "NOT"; ri "LEFT@REFLEX"; ex(); up();up(); rri "EQUATION"; ex(); p "ALTORDEF"; defineinfix "IF" "?x->?y" "(~?x)|?y"; s "?x->?y"; ri "IF"; ri "ORBOOL"; ex(); right(); rri "IF"; ex(); p "IFBOOL"; makescout "->" "IFBOOL"; defineinfix "IFF" "?x==?y" "(bool:?x)=(bool:?y)"; s "?x==?y"; ri "IFF"; ri "EQBOOL"; ex(); right(); rri "IFF"; ex(); p "IFFBOOL"; makescout "==" "IFFBOOL"; (* (* the basic set notion *) defineconstant "Set@?x" "[bool:?x@?1]"; (* prove that the set operator is a retraction, and so can be used as a sort of type label *) (* SETRETRACT: Set @ Set @ ?x = Set @ ?x ["Set","TYPES"] *) s "Set@Set@?x"; ri "EVERYWHERE@Set"; ex(); ri "EVERYWHERE2@TYPES"; ex(); rri "Set"; ex(); p "SETRETRACT"; (* this is a new definition of the membership relation (Aug 20th) *) definetypedinfix "IN" 0 1 "?x<(bool:?y)"; ri "IF";ex(); dlls "NOTBOOLDROP"; ri "NOTBOOLDROP"; ex(); ri "NOTBOOL"; ex(); top(); ri "ORSCIN"; ex(); rri "IF"; ex(); p "IFSCIN"; makescin "->" "IFSCIN"; s "(bool:?x)==(bool:?y)"; ri "IFF"; ex(); dlls "TYPES"; ri "TYPES"; ex(); top(); dlls "TYPES"; ri "TYPES"; ex(); top(); rri "IFF"; ex(); p "IFFSCIN"; makescin "==" "IFFSCIN"; (* define the assertion operator *) defineinfix "ASSERT" "?y|-?x" "bool:?x"; (* show that the assertion operator is "scout" *) initializecounter(); s "?y|-?x"; ri "ASSERT"; ex(); rri "TYPES"; ex(); ri "RIGHT@ \$ASSERT"; ex(); assign "?y_5" "?y"; p "ASSERTSCOUT"; makescout "|-" "ASSERTSCOUT"; declareprefix "|-" "true"; (* the assert symbol is a retraction *) (* TWOASSERTS: |-|-?p = |-?p ["ASSERT","TYPES"] *) initializecounter(); s "|- |- ?p"; ri "(RIGHT@ASSERT)**ASSERT"; ex(); ri "TYPES"; ex(); rri "ASSERT"; ex(); assign "?y_6" "true"; p "TWOASSERTS"; (* ASSERT2: bool : ?x = |-?x ["ASSERT"] *) s "|-?x"; ri "ASSERT";ex(); workback(); p "ASSERT2"; (* typing lemmas for propositional connectives *) s "?p==?q"; ri "IFF"; ex(); ri "RL@ \$TYPES"; ex(); ri "EQBOOL"; ex(); ri "RIGHT@ \$IFF"; ex(); ri "(RIGHT@RL@ASSERT2)**ASSERT2"; ex(); p "BTYPE"; dpt "ALLASSERTS"; s "|- |-?x"; ri "TWOASSERTS"; ex(); ri "ALLASSERTS"; p "ALLASSERTS"; defineinfix "XOR" "?x =/= ?y" "~?x==?y"; s "?x=/=?y"; ri "XOR"; ex(); ri "RIGHT@ \$IFFSCIN"; ex(); ri "NOTBOOL"; ex(); ri "RIGHT@ \$XOR"; ex(); ri "(RIGHT@RL@ASSERT2)**ASSERT2"; ex(); p "XORTYPE"; (* new on March 9; make =/= "scin" *) s "(bool:?x)=/=(bool:?y)"; ri "RL@ASSERT2"; ri "XORTYPE"; ex(); right(); ri "RL@TWOASSERTS"; up(); rri "XORTYPE"; ex(); p "XORSCIN"; makescin "=/=" "XORSCIN"; s "?x=/=?y"; ri "XOR**NOTBOOL**RIGHT@ \$XOR"; ex(); p "XORBOOL"; s "~?p"; ri "NOTBOOL**ASSERT2"; ex(); right(); ri "(\$NOTBOOLDROP)**RIGHT@ASSERT2"; ex(); p "NTYPE"; s "?p|?q"; ri "(\$ORSCIN)**RL@ASSERT2"; ex(); ri "ORBOOL**ASSERT2"; ex(); p "DTYPE"; s "?p&?q"; ri "(\$ANDSCIN)**RL@ASSERT2"; ex(); ri "ANDBOOL**ASSERT2"; ex(); p "CTYPE"; s "?p->?q"; rri "IFSCIN"; ri "RL@ASSERT2"; ex(); ri "IFBOOL"; ri "ASSERT2"; ex(); p "IMPTYPE"; defineinfix "CONVIF" "?p<-?q" "?q->?p"; s "?p<-?q"; ri "CONVIF"; ri "IMPTYPE"; ri "RIGHT@ \$CONVIF"; ex(); p "CONTYPE"; (* new March 9: show that <- is scin *) s "(bool:?x)<-(bool:?y)"; ri "RL@ASSERT2"; ri "CONTYPE"; ex(); right(); ri "RL@TWOASSERTS"; up(); rri "CONTYPE"; ex(); p "CONSCIN"; makescin "<-" "CONSCIN"; s "?x<-?y"; ri "CONVIF**IFBOOL**RIGHT@ \$CONVIF"; ex(); p "CNBOOL"; (* an example with quantifiers *) s "forall@[forsome@[?1=?2]]"; (* this is "for all x, for some y, x=y" *) (* this would not be stratified without the assistance of the scin/scout feature *) (* start with definitional expansions *) ri "forall"; ex(); dlls "forsome"; ri "forsome"; ex(); dlls "forall"; ri "forall"; ex(); ri "NOT"; ex(); ri "EQUATION"; ex(); right();left(); ri "BIND@?1"; ex(); ri "LEFT@ \$0|-|1"; ex(); ri "EVAL"; ex(); ri "RIGHT@REFLEX"; ex(); ri "NOT"; ex(); ri "LEFT@REFLEX"; ex(); uptors "CASEINTRO"; rri "CASEINTRO"; ex(); up(); ri "NOT"; ri "LEFT@NONTRIV"; ex(); top(); ri "REFLEX"; ex(); p "EXAMPLE1"; (* double negation result *) (* DUBNEG: ~~?p = bool : ?p ["BOOLDEF","CASEINTRO","EQUATION","NONTRIV","NOT","REFLEX"] *) initializecounter(); s "~ ~?p"; ri "CASEINTRO"; ex(); assign "?y_1" "true=?p"; right();left(); right();right(); rri "0|-|1";ex(); up(); ri "NOT"; ex(); ri "LEFT@REFLEX"; ex(); up(); ri "NOT"; ex(); ri "LEFT@NONTRIV"; ex(); up();right(); right(); ri "NOT"; ex(); ri "1|-|1"; ex(); up(); ri "NOT";ex(); ri "LEFT@REFLEX"; ex(); top(); rri "EQUATION"; ex(); rri "BOOLDEF"; ex(); p "DUBNEG"; (* some frequently used utilities for dealing with nested case expressions *) (* UNPACK: (?x || ?y , ?z) || ?u , ?v = ?x || (?y || ?u , ?v) , ?z || ?u , ?v ["CASEINTRO"] *) initializecounter(); start "(?x||?y,?z)||?u,?v"; ri "CASEINTRO";ex(); assign "?y_1" "?x"; right(); left(); ri "LEFT@1|-|1"; ex(); up();right(); ri "LEFT@1|-|1"; ex(); p "UNPACK"; (* ANDUNPACK: (?P & ?Q) || ?x , ?y = (true = ?P) || ((true = ?Q) || ?x , ?y) , ?y ["AND","CASEINTRO"] *) s "(?P&?Q)||?x,?y"; ri "(LEFT@AND)**UNPACK"; ex(); p "ANDUNPACK"; (* ASSERT_UNEXP: ?p || true , false = |-?p ["ASSERT","BOOLDEF","EQUATION","ODDCHOICE"] *) s "?p||true,false"; ri "ODDCHOICE"; ex(); rri "EQUATION"; ex(); rri "BOOLDEF"; ex(); ri "ASSERT2"; ex(); p "ASSERT_UNEXP"; (* the arguments of forall and forsome2 can be labelled as boolean *) (* FORALLBOOL2: forall @ [bool : ?P @ ?1] = forall @ [?P @ ?1] ["BOOLDEF","CASEINTRO","EQBOOL","EQUATION","REFLEX","forall"] *) initializecounter(); start "forall@[bool:?P@?1]"; ri "forall"; ex(); ri "CASEINTRO"; ex(); assign "?y_2" "[?P@?1]=[true]"; right();left(); left();right();right(); ri "BIND@?1";ex(); ri "LEFT@0|-|1"; ex(); ri "EVAL"; ex(); up(); rri "TRUEBOOL"; ex(); up();up(); ri "REFLEX"; ex(); up();right(); ri "EQUATION"; ex(); right();left(); rri "1|-|1"; ex(); assign "?x_7" "false"; left();left();left(); ri "CASEINTRO"; ex(); assign "[?y_8@?1]" "[true = ?P@?1]"; right();left(); rri "0|-|3"; ex(); ri "TRUEBOOL"; ri "RIGHT@0|-|3"; ex(); up();up();left(); rri "BOOLDEF"; ex(); ri "(BIND@?1)**(LEFT@0|-|2)**EVAL"; ex(); up();ex(); up();up();up(); ri "1|-|2"; ex(); up();up(); rri "CASEINTRO"; ex(); top(); ri "(\$EQUATION)**(\$forall)"; ex(); assign "?P" "[?P@?1]"; p "FORALLBOOL2"; (* FORSOMEBOOL2: forsome @ [bool : ?P @ ?1] = forsome @ [?P @ ?1] *) s "forsome@[bool:?P@?1]"; ri "forsome"; ex(); right();right();right(); ri "NOTBOOLDROP";ex(); top(); rri "forsome2"; ex(); p "FORSOMEBOOL2"; quit();