author  paulson 
Fri, 05 Oct 2007 09:59:03 +0200  
changeset 24854  0ebcd575d3c6 
parent 18678  dd0c569fa43d 
permissions  rwrr 
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 

5061  10 
Goal "?p : (ALL x y. P(x,y)) > (ALL y x. P(x,y))"; 
0  11 
by tac; 
17480  12 
result(); 
0  13 

14 

5061  15 
Goal "?p : (EX x y. P(x,y)) > (EX y x. P(x,y))"; 
0  16 
by tac; 
17480  17 
result(); 
0  18 

19 

20 
(*Converse is false*) 

5061  21 
Goal "?p : (ALL x. P(x))  (ALL x. Q(x)) > (ALL x. P(x)  Q(x))"; 
0  22 
by tac; 
17480  23 
result(); 
0  24 

5061  25 
Goal "?p : (ALL x. P>Q(x)) <> (P> (ALL x. Q(x)))"; 
0  26 
by tac; 
17480  27 
result(); 
0  28 

29 

5061  30 
Goal "?p : (ALL x. P(x)>Q) <> ((EX x. P(x)) > Q)"; 
0  31 
by tac; 
17480  32 
result(); 
0  33 

34 

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

35 
writeln"Some harder ones"; 
0  36 

5061  37 
Goal "?p : (EX x. P(x)  Q(x)) <> (EX x. P(x))  (EX x. Q(x))"; 
0  38 
by tac; 
17480  39 
result(); 
0  40 
(*6 secs*) 
41 

42 
(*Converse is false*) 

5061  43 
Goal "?p : (EX x. P(x)&Q(x)) > (EX x. P(x)) & (EX x. Q(x))"; 
0  44 
by tac; 
17480  45 
result(); 
0  46 

47 

48 
writeln"Basic test of quantifier reasoning"; 

49 
(*TRUE*) 

5061  50 
Goal "?p : (EX y. ALL x. Q(x,y)) > (ALL x. EX y. Q(x,y))"; 
17480  51 
by tac; 
52 
result(); 

0  53 

54 

5061  55 
Goal "?p : (ALL x. Q(x)) > (EX x. Q(x))"; 
17480  56 
by tac; 
57 
result(); 

0  58 

59 

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

61 

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

5061  67 
Goal "?p : (EX x. Q(x)) > (ALL x. Q(x))"; 
18678  68 
by tac handle ERROR _ => writeln"Failed, as expected"; 
17480  69 
getgoal 1; 
0  70 

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

5061  76 
Goal 
3836  77 
"?p : (P(?a) > (ALL x. Q(x))) > (ALL x. P(x) > Q(x))"; 
18678  78 
by tac handle ERROR _ => writeln"Failed, as expected"; 
17480  79 
getgoal 1; 
0  80 

81 

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

83 

5061  84 
Goal "?p : (ALL x. P(x)>Q(x)) & (EX x. P(x)) > (EX x. Q(x))"; 
17480  85 
by tac; 
86 
result(); 

0  87 

88 

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

5061  90 
Goal "?p : (P > (EX x. Q(x))) & P > (EX x. Q(x))"; 
17480  91 
by tac; 
92 
result(); 

0  93 

5061  94 
Goal "?p : (ALL x. P(x)>Q(f(x))) & (ALL x. Q(x)>R(g(x))) & P(d) > R(?a)"; 
17480  95 
by tac; 
96 
(*Verify that no subgoals remain.*) 

97 
uresult(); 

0  98 

99 

5061  100 
Goal "?p : (ALL x. Q(x)) > (EX x. Q(x))"; 
0  101 
by tac; 
17480  102 
result(); 
0  103 

104 

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

105 
writeln"Some slow ones"; 
0  106 

107 

108 
(*Principia Mathematica *11.53 *) 

5061  109 
Goal "?p : (ALL x y. P(x) > Q(y)) <> ((EX x. P(x)) > (ALL y. Q(y)))"; 
0  110 
by tac; 
17480  111 
result(); 
0  112 
(*6 secs*) 
113 

114 
(*Principia Mathematica *11.55 *) 

5061  115 
Goal "?p : (EX x y. P(x) & Q(x,y)) <> (EX x. P(x) & (EX y. Q(x,y)))"; 
0  116 
by tac; 
17480  117 
result(); 
0  118 
(*9 secs*) 
119 

120 
(*Principia Mathematica *11.61 *) 

5061  121 
Goal "?p : (EX y. ALL x. P(x) > Q(x,y)) > (ALL x. P(x) > (EX y. Q(x,y)))"; 
0  122 
by tac; 
17480  123 
result(); 
0  124 
(*3 secs*) 