1464

1 
(* Title: FOLP/ex/quant.ML

0

2 
ID: $Id$

1459

3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory

0

4 
Copyright 1991 University of Cambridge


5 


6 
FirstOrder Logic: quantifier examples (intuitionistic and classical)


7 
Needs declarations of the theory "thy" and the tactic "tac"


8 
*)


9 

1464

10 
writeln"File FOLP/ex/quant.ML";

0

11 

3836

12 
goal thy "?p : (ALL x y. P(x,y)) > (ALL y x. P(x,y))";

0

13 
by tac;


14 
result();


15 


16 

3836

17 
goal thy "?p : (EX x y. P(x,y)) > (EX y x. P(x,y))";

0

18 
by tac;


19 
result();


20 


21 


22 
(*Converse is false*)

3836

23 
goal thy "?p : (ALL x. P(x))  (ALL x. Q(x)) > (ALL x. P(x)  Q(x))";

0

24 
by tac;


25 
result();


26 

3836

27 
goal thy "?p : (ALL x. P>Q(x)) <> (P> (ALL x. Q(x)))";

0

28 
by tac;


29 
result();


30 


31 

3836

32 
goal thy "?p : (ALL x. P(x)>Q) <> ((EX x. P(x)) > Q)";

0

33 
by tac;


34 
result();


35 


36 


37 
writeln"Some harder ones";


38 

3836

39 
goal thy "?p : (EX x. P(x)  Q(x)) <> (EX x. P(x))  (EX x. Q(x))";

0

40 
by tac;


41 
result();


42 
(*6 secs*)


43 


44 
(*Converse is false*)

3836

45 
goal thy "?p : (EX x. P(x)&Q(x)) > (EX x. P(x)) & (EX x. Q(x))";

0

46 
by tac;


47 
result();


48 


49 


50 
writeln"Basic test of quantifier reasoning";


51 
(*TRUE*)


52 
goal thy "?p : (EX y. ALL x. Q(x,y)) > (ALL x. EX y. Q(x,y))";


53 
by tac;


54 
result();


55 


56 


57 
goal thy "?p : (ALL x. Q(x)) > (EX x. Q(x))";


58 
by tac;


59 
result();


60 


61 


62 
writeln"The following should fail, as they are false!";


63 


64 
goal thy "?p : (ALL x. EX y. Q(x,y)) > (EX y. ALL x. Q(x,y))";


65 
by tac handle ERROR => writeln"Failed, as expected";


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


67 
getgoal 1;


68 


69 
goal thy "?p : (EX x. Q(x)) > (ALL x. Q(x))";


70 
by tac handle ERROR => writeln"Failed, as expected";


71 
getgoal 1;


72 

3836

73 
goal thy "?p : P(?a) > (ALL x. P(x))";

0

74 
by tac handle ERROR => writeln"Failed, as expected";


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


76 
getgoal 1;


77 


78 
goal thy

3836

79 
"?p : (P(?a) > (ALL x. Q(x))) > (ALL x. P(x) > Q(x))";

0

80 
by tac handle ERROR => writeln"Failed, as expected";


81 
getgoal 1;


82 


83 


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


85 

3836

86 
goal thy "?p : (ALL x. P(x)>Q(x)) & (EX x. P(x)) > (EX x. Q(x))";

0

87 
by tac;


88 
result();


89 


90 


91 
(*An example of why exI should be delayed as long as possible*)

3836

92 
goal thy "?p : (P > (EX x. Q(x))) & P > (EX x. Q(x))";

0

93 
by tac;


94 
result();


95 


96 
goal thy "?p : (ALL x. P(x)>Q(f(x))) & (ALL x. Q(x)>R(g(x))) & P(d) > R(?a)";


97 
by tac;


98 
(*Verify that no subgoals remain.*)


99 
uresult();


100 


101 


102 
goal thy "?p : (ALL x. Q(x)) > (EX x. Q(x))";


103 
by tac;


104 
result();


105 


106 


107 
writeln"Some slow ones";


108 


109 


110 
(*Principia Mathematica *11.53 *)


111 
goal thy "?p : (ALL x y. P(x) > Q(y)) <> ((EX x. P(x)) > (ALL y. Q(y)))";


112 
by tac;


113 
result();


114 
(*6 secs*)


115 


116 
(*Principia Mathematica *11.55 *)


117 
goal thy "?p : (EX x y. P(x) & Q(x,y)) <> (EX x. P(x) & (EX y. Q(x,y)))";


118 
by tac;


119 
result();


120 
(*9 secs*)


121 


122 
(*Principia Mathematica *11.61 *)


123 
goal thy "?p : (EX y. ALL x. P(x) > Q(x,y)) > (ALL x. P(x) > (EX y. Q(x,y)))";


124 
by tac;


125 
result();


126 
(*3 secs*)


127 


128 
writeln"Reached end of file.";


129 
