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