7 Needs declarations of the theory "thy" and the tactic "tac" |
7 Needs declarations of the theory "thy" and the tactic "tac" |
8 *) |
8 *) |
9 |
9 |
10 writeln"File FOLP/ex/quant.ML"; |
10 writeln"File FOLP/ex/quant.ML"; |
11 |
11 |
12 goal thy "?p : (ALL x y.P(x,y)) --> (ALL y x.P(x,y))"; |
12 goal thy "?p : (ALL x y. P(x,y)) --> (ALL y x. P(x,y))"; |
13 by tac; |
13 by tac; |
14 result(); |
14 result(); |
15 |
15 |
16 |
16 |
17 goal thy "?p : (EX x y.P(x,y)) --> (EX y x.P(x,y))"; |
17 goal thy "?p : (EX x y. P(x,y)) --> (EX y x. P(x,y))"; |
18 by tac; |
18 by tac; |
19 result(); |
19 result(); |
20 |
20 |
21 |
21 |
22 (*Converse is false*) |
22 (*Converse is false*) |
23 goal thy "?p : (ALL x.P(x)) | (ALL x.Q(x)) --> (ALL x. P(x) | Q(x))"; |
23 goal thy "?p : (ALL x. P(x)) | (ALL x. Q(x)) --> (ALL x. P(x) | Q(x))"; |
24 by tac; |
24 by tac; |
25 result(); |
25 result(); |
26 |
26 |
27 goal thy "?p : (ALL x. P-->Q(x)) <-> (P--> (ALL x.Q(x)))"; |
27 goal thy "?p : (ALL x. P-->Q(x)) <-> (P--> (ALL x. Q(x)))"; |
28 by tac; |
28 by tac; |
29 result(); |
29 result(); |
30 |
30 |
31 |
31 |
32 goal thy "?p : (ALL x.P(x)-->Q) <-> ((EX x.P(x)) --> Q)"; |
32 goal thy "?p : (ALL x. P(x)-->Q) <-> ((EX x. P(x)) --> Q)"; |
33 by tac; |
33 by tac; |
34 result(); |
34 result(); |
35 |
35 |
36 |
36 |
37 writeln"Some harder ones"; |
37 writeln"Some harder ones"; |
38 |
38 |
39 goal thy "?p : (EX x. P(x) | Q(x)) <-> (EX x.P(x)) | (EX x.Q(x))"; |
39 goal thy "?p : (EX x. P(x) | Q(x)) <-> (EX x. P(x)) | (EX x. Q(x))"; |
40 by tac; |
40 by tac; |
41 result(); |
41 result(); |
42 (*6 secs*) |
42 (*6 secs*) |
43 |
43 |
44 (*Converse is false*) |
44 (*Converse is false*) |
45 goal thy "?p : (EX x. P(x)&Q(x)) --> (EX x.P(x)) & (EX x.Q(x))"; |
45 goal thy "?p : (EX x. P(x)&Q(x)) --> (EX x. P(x)) & (EX x. Q(x))"; |
46 by tac; |
46 by tac; |
47 result(); |
47 result(); |
48 |
48 |
49 |
49 |
50 writeln"Basic test of quantifier reasoning"; |
50 writeln"Basic test of quantifier reasoning"; |
68 |
68 |
69 goal thy "?p : (EX x. Q(x)) --> (ALL x. Q(x))"; |
69 goal thy "?p : (EX x. Q(x)) --> (ALL x. Q(x))"; |
70 by tac handle ERROR => writeln"Failed, as expected"; |
70 by tac handle ERROR => writeln"Failed, as expected"; |
71 getgoal 1; |
71 getgoal 1; |
72 |
72 |
73 goal thy "?p : P(?a) --> (ALL x.P(x))"; |
73 goal thy "?p : P(?a) --> (ALL x. P(x))"; |
74 by tac handle ERROR => writeln"Failed, as expected"; |
74 by tac handle ERROR => writeln"Failed, as expected"; |
75 (*Check that subgoals remain: proof failed.*) |
75 (*Check that subgoals remain: proof failed.*) |
76 getgoal 1; |
76 getgoal 1; |
77 |
77 |
78 goal thy |
78 goal thy |
79 "?p : (P(?a) --> (ALL x.Q(x))) --> (ALL x. P(x) --> Q(x))"; |
79 "?p : (P(?a) --> (ALL x. Q(x))) --> (ALL x. P(x) --> Q(x))"; |
80 by tac handle ERROR => writeln"Failed, as expected"; |
80 by tac handle ERROR => writeln"Failed, as expected"; |
81 getgoal 1; |
81 getgoal 1; |
82 |
82 |
83 |
83 |
84 writeln"Back to things that are provable..."; |
84 writeln"Back to things that are provable..."; |
85 |
85 |
86 goal thy "?p : (ALL x.P(x)-->Q(x)) & (EX x.P(x)) --> (EX x.Q(x))"; |
86 goal thy "?p : (ALL x. P(x)-->Q(x)) & (EX x. P(x)) --> (EX x. Q(x))"; |
87 by tac; |
87 by tac; |
88 result(); |
88 result(); |
89 |
89 |
90 |
90 |
91 (*An example of why exI should be delayed as long as possible*) |
91 (*An example of why exI should be delayed as long as possible*) |
92 goal thy "?p : (P --> (EX x.Q(x))) & P --> (EX x.Q(x))"; |
92 goal thy "?p : (P --> (EX x. Q(x))) & P --> (EX x. Q(x))"; |
93 by tac; |
93 by tac; |
94 result(); |
94 result(); |
95 |
95 |
96 goal thy "?p : (ALL x. P(x)-->Q(f(x))) & (ALL x. Q(x)-->R(g(x))) & P(d) --> R(?a)"; |
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; |
97 by tac; |