author  haftmann 
Tue, 10 Jul 2007 17:30:50 +0200  
changeset 23709  fd31da8f752a 
parent 18678  dd0c569fa43d 
permissions  rwrr 
1459  1 
(* Title: FOL/ex/quant 
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 

10 
writeln"File FOL/ex/quant."; 

11 

5050  12 
Goal "(ALL x y. P(x,y)) > (ALL y x. P(x,y))"; 
0  13 
by tac; 
14 
result(); 

15 

16 

5050  17 
Goal "(EX x y. P(x,y)) > (EX y x. P(x,y))"; 
0  18 
by tac; 
19 
result(); 

20 

21 

22 
(*Converse is false*) 

5050  23 
Goal "(ALL x. P(x))  (ALL x. Q(x)) > (ALL x. P(x)  Q(x))"; 
0  24 
by tac; 
25 
result(); 

26 

5050  27 
Goal "(ALL x. P>Q(x)) <> (P> (ALL x. Q(x)))"; 
0  28 
by tac; 
29 
result(); 

30 

31 

5050  32 
Goal "(ALL x. P(x)>Q) <> ((EX x. P(x)) > Q)"; 
0  33 
by tac; 
34 
result(); 

35 

36 

15661
9ef583b08647
reverted renaming of Some/None in comments and strings;
wenzelm
parents:
15531
diff
changeset

37 
writeln"Some harder ones"; 
0  38 

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

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

5050  52 
Goal "(EX y. ALL x. Q(x,y)) > (ALL x. EX y. Q(x,y))"; 
0  53 
by tac; 
54 
result(); 

55 

56 

5050  57 
Goal "(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 

5050  64 
Goal "(ALL x. EX y. Q(x,y)) > (EX y. ALL x. Q(x,y))"; 
18678  65 
by tac handle ERROR _ => writeln"Failed, as expected"; 
0  66 
(*Check that subgoals remain: proof failed.*) 
67 
getgoal 1; 

68 

5050  69 
Goal "(EX x. Q(x)) > (ALL x. Q(x))"; 
18678  70 
by tac handle ERROR _ => writeln"Failed, as expected"; 
0  71 
getgoal 1; 
72 

5050  73 
Goal "P(?a) > (ALL x. P(x))"; 
18678  74 
by tac handle ERROR _ => writeln"Failed, as expected"; 
0  75 
(*Check that subgoals remain: proof failed.*) 
76 
getgoal 1; 

77 

5050  78 
Goal 
3835  79 
"(P(?a) > (ALL x. Q(x))) > (ALL x. P(x) > Q(x))"; 
18678  80 
by tac handle ERROR _ => writeln"Failed, as expected"; 
0  81 
getgoal 1; 
82 

83 

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

85 

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

5050  92 
Goal "(P > (EX x. Q(x))) & P > (EX x. Q(x))"; 
0  93 
by tac; 
94 
result(); 

95 

5050  96 
Goal "(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 

5050  102 
Goal "(ALL x. Q(x)) > (EX x. Q(x))"; 
0  103 
by tac; 
104 
result(); 

105 

106 

15661
9ef583b08647
reverted renaming of Some/None in comments and strings;
wenzelm
parents:
15531
diff
changeset

107 
writeln"Some slow ones"; 
0  108 

109 

110 
(*Principia Mathematica *11.53 *) 

5050  111 
Goal "(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 *) 

5050  117 
Goal "(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 *) 

5050  123 
Goal "(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 