6252

1 
(* Title: LK/ex/quant


2 
ID: $Id$


3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory


4 
Copyright 1992 University of Cambridge


5 


6 
Classical sequent calculus: examples with quantifiers.


7 
*)


8 


9 


10 
writeln"LK/ex/quant: Examples with quantifiers";


11 


12 
goal LK.thy " (ALL x. P) <> P";


13 
by (fast_tac LK_pack 1);


14 
result();


15 


16 
goal LK.thy " (ALL x y. P(x,y)) <> (ALL y x. P(x,y))";


17 
by (fast_tac LK_pack 1);


18 
result();


19 


20 
goal LK.thy "ALL u. P(u), ALL v. Q(v)  ALL u v. P(u) & Q(v)";


21 
by (fast_tac LK_pack 1);


22 
result();


23 


24 
writeln"Permutation of existential quantifier.";


25 
goal LK.thy " (EX x y. P(x,y)) <> (EX y x. P(x,y))";


26 
by (fast_tac LK_pack 1);


27 
result();


28 


29 
goal LK.thy " (ALL x. P(x) & Q(x)) <> (ALL x. P(x)) & (ALL x. Q(x))";


30 
by (fast_tac LK_pack 1);


31 
result();


32 


33 


34 
(*Converse is invalid*)


35 
goal LK.thy " (ALL x. P(x))  (ALL x. Q(x)) > (ALL x. P(x)Q(x))";


36 
by (fast_tac LK_pack 1);


37 
result();


38 


39 


40 
writeln"Pushing ALL into an implication.";


41 
goal LK.thy " (ALL x. P > Q(x)) <> (P > (ALL x. Q(x)))";


42 
by (fast_tac LK_pack 1);


43 
result();


44 


45 


46 
goal LK.thy " (ALL x. P(x)>Q) <> ((EX x. P(x)) > Q)";


47 
by (fast_tac LK_pack 1);


48 
result();


49 


50 


51 
goal LK.thy " (EX x. P) <> P";


52 
by (fast_tac LK_pack 1);


53 
result();


54 


55 


56 
writeln"Distribution of EX over disjunction.";


57 
goal LK.thy " (EX x. P(x)  Q(x)) <> (EX x. P(x))  (EX x. Q(x))";


58 
by (fast_tac LK_pack 1);


59 
result();


60 
(*5 secs*)


61 


62 
(*Converse is invalid*)


63 
goal LK.thy " (EX x. P(x) & Q(x)) > (EX x. P(x)) & (EX x. Q(x))";


64 
by (fast_tac LK_pack 1);


65 
result();


66 


67 


68 
writeln"Harder examples: classical theorems.";


69 


70 
goal LK.thy " (EX x. P>Q(x)) <> (P > (EX x. Q(x)))";


71 
by (fast_tac LK_pack 1);


72 
result();


73 
(*3 secs*)


74 


75 


76 
goal LK.thy " (EX x. P(x)>Q) <> (ALL x. P(x)) > Q";


77 
by (fast_tac LK_pack 1);


78 
result();


79 
(*5 secs*)


80 


81 


82 
goal LK.thy " (ALL x. P(x))  Q <> (ALL x. P(x)  Q)";


83 
by (fast_tac LK_pack 1);


84 
result();


85 


86 


87 
writeln"Basic test of quantifier reasoning";


88 
goal LK.thy


89 
" (EX y. ALL x. Q(x,y)) > (ALL x. EX y. Q(x,y))";


90 
by (fast_tac LK_pack 1);


91 
result();


92 


93 


94 
goal LK.thy " (ALL x. Q(x)) > (EX x. Q(x))";


95 
by (fast_tac LK_pack 1);


96 
result();


97 


98 


99 
writeln"The following are invalid!";


100 


101 
(*INVALID*)


102 
goal LK.thy " (ALL x. EX y. Q(x,y)) > (EX y. ALL x. Q(x,y))";


103 
by (fast_tac LK_pack 1) handle ERROR => writeln"Failed, as expected";


104 
(*Check that subgoals remain: proof failed.*)


105 
getgoal 1;


106 


107 
(*INVALID*)


108 
goal LK.thy " (EX x. Q(x)) > (ALL x. Q(x))";


109 
by (fast_tac LK_pack 1) handle ERROR => writeln"Failed, as expected";


110 
getgoal 1;


111 


112 
goal LK.thy " P(?a) > (ALL x. P(x))";


113 
by (fast_tac LK_pack 1) handle ERROR => writeln"Failed, as expected";


114 
(*Check that subgoals remain: proof failed.*)


115 
getgoal 1;


116 


117 
goal LK.thy " (P(?a) > (ALL x. Q(x))) > (ALL x. P(x) > Q(x))";


118 
by (fast_tac LK_pack 1) handle ERROR => writeln"Failed, as expected";


119 
getgoal 1;


120 


121 


122 
writeln"Back to things that are provable...";


123 


124 
goal LK.thy " (ALL x. P(x)>Q(x)) & (EX x. P(x)) > (EX x. Q(x))";


125 
by (fast_tac LK_pack 1);


126 
result();


127 


128 
(*An example of why exR should be delayed as long as possible*)


129 
goal LK.thy " (P> (EX x. Q(x))) & P> (EX x. Q(x))";


130 
by (fast_tac LK_pack 1);


131 
result();


132 


133 
writeln"Solving for a Var";


134 
goal LK.thy


135 
" (ALL x. P(x)>Q(f(x))) & (ALL x. Q(x)>R(g(x))) & P(d) > R(?a)";


136 
by (fast_tac LK_pack 1);


137 
result();


138 


139 


140 
writeln"Principia Mathematica *11.53";


141 
goal LK.thy


142 
" (ALL x y. P(x) > Q(y)) <> ((EX x. P(x)) > (ALL y. Q(y)))";


143 
by (fast_tac LK_pack 1);


144 
result();


145 


146 


147 
writeln"Principia Mathematica *11.55";


148 
goal LK.thy " (EX x y. P(x) & Q(x,y)) <> (EX x. P(x) & (EX y. Q(x,y)))";


149 
by (fast_tac LK_pack 1);


150 
result();


151 


152 
writeln"Principia Mathematica *11.61";


153 
goal LK.thy


154 
" (EX y. ALL x. P(x) > Q(x,y)) > (ALL x. P(x) > (EX y. Q(x,y)))";


155 
by (fast_tac LK_pack 1);


156 
result();


157 


158 
writeln"Reached end of file.";


159 


160 
(*21 August 88: loaded in 45.7 secs*)
