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 

5061

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

0

13 
by tac;


14 
result();


15 


16 

5061

17 
Goal "?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*)

5061

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

0

24 
by tac;


25 
result();


26 

5061

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

0

28 
by tac;


29 
result();


30 


31 

5061

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

0

33 
by tac;


34 
result();


35 


36 

15531

37 
writeln"SOME harder ones";

0

38 

5061

39 
Goal "?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*)

5061

45 
Goal "?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*)

5061

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

0

53 
by tac;


54 
result();


55 


56 

5061

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

0

58 
by tac;


59 
result();


60 


61 


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


63 

5061

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

0

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


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


67 
getgoal 1;


68 

5061

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

0

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


71 
getgoal 1;


72 

5061

73 
Goal "?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 

5061

78 
Goal

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 

5061

86 
Goal "?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*)

5061

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

0

93 
by tac;


94 
result();


95 

5061

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

0

97 
by tac;


98 
(*Verify that no subgoals remain.*)


99 
uresult();


100 


101 

5061

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

0

103 
by tac;


104 
result();


105 


106 

15531

107 
writeln"SOME slow ones";

0

108 


109 


110 
(*Principia Mathematica *11.53 *)

5061

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

0

112 
by tac;


113 
result();


114 
(*6 secs*)


115 


116 
(*Principia Mathematica *11.55 *)

5061

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

0

118 
by tac;


119 
result();


120 
(*9 secs*)


121 


122 
(*Principia Mathematica *11.61 *)

5061

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

0

124 
by tac;


125 
result();


126 
(*3 secs*)


127 


128 
writeln"Reached end of file.";


129 
