11 |
11 |
12 goal LK.thy "|- (ALL x. P) <-> P"; |
12 goal LK.thy "|- (ALL x. P) <-> P"; |
13 by (fast_tac LK_pack 1); |
13 by (fast_tac LK_pack 1); |
14 result(); |
14 result(); |
15 |
15 |
16 goal LK.thy "|- (ALL x y.P(x,y)) <-> (ALL y x.P(x,y))"; |
16 goal LK.thy "|- (ALL x y. P(x,y)) <-> (ALL y x. P(x,y))"; |
17 by (fast_tac LK_pack 1); |
17 by (fast_tac LK_pack 1); |
18 result(); |
18 result(); |
19 |
19 |
20 goal LK.thy "ALL u.P(u), ALL v.Q(v) |- ALL u v. P(u) & Q(v)"; |
20 goal LK.thy "ALL u. P(u), ALL v. Q(v) |- ALL u v. P(u) & Q(v)"; |
21 by (fast_tac LK_pack 1); |
21 by (fast_tac LK_pack 1); |
22 result(); |
22 result(); |
23 |
23 |
24 writeln"Permutation of existential quantifier."; |
24 writeln"Permutation of existential quantifier."; |
25 goal LK.thy "|- (EX x y.P(x,y)) <-> (EX y x.P(x,y))"; |
25 goal LK.thy "|- (EX x y. P(x,y)) <-> (EX y x. P(x,y))"; |
26 by (fast_tac LK_pack 1); |
26 by (fast_tac LK_pack 1); |
27 result(); |
27 result(); |
28 |
28 |
29 goal LK.thy "|- (ALL x. P(x) & Q(x)) <-> (ALL x.P(x)) & (ALL x.Q(x))"; |
29 goal LK.thy "|- (ALL x. P(x) & Q(x)) <-> (ALL x. P(x)) & (ALL x. Q(x))"; |
30 by (fast_tac LK_pack 1); |
30 by (fast_tac LK_pack 1); |
31 result(); |
31 result(); |
32 |
32 |
33 |
33 |
34 (*Converse is invalid*) |
34 (*Converse is invalid*) |
41 goal LK.thy "|- (ALL x. P --> Q(x)) <-> (P --> (ALL x. Q(x)))"; |
41 goal LK.thy "|- (ALL x. P --> Q(x)) <-> (P --> (ALL x. Q(x)))"; |
42 by (fast_tac LK_pack 1); |
42 by (fast_tac LK_pack 1); |
43 result(); |
43 result(); |
44 |
44 |
45 |
45 |
46 goal LK.thy "|- (ALL x.P(x)-->Q) <-> ((EX x.P(x)) --> Q)"; |
46 goal LK.thy "|- (ALL x. P(x)-->Q) <-> ((EX x. P(x)) --> Q)"; |
47 by (fast_tac LK_pack 1); |
47 by (fast_tac LK_pack 1); |
48 result(); |
48 result(); |
49 |
49 |
50 |
50 |
51 goal LK.thy "|- (EX x. P) <-> P"; |
51 goal LK.thy "|- (EX x. P) <-> P"; |
65 result(); |
65 result(); |
66 |
66 |
67 |
67 |
68 writeln"Harder examples: classical theorems."; |
68 writeln"Harder examples: classical theorems."; |
69 |
69 |
70 goal LK.thy "|- (EX x. P-->Q(x)) <-> (P --> (EX x.Q(x)))"; |
70 goal LK.thy "|- (EX x. P-->Q(x)) <-> (P --> (EX x. Q(x)))"; |
71 by (fast_tac LK_pack 1); |
71 by (fast_tac LK_pack 1); |
72 result(); |
72 result(); |
73 (*3 secs*) |
73 (*3 secs*) |
74 |
74 |
75 |
75 |
76 goal LK.thy "|- (EX x.P(x)-->Q) <-> (ALL x.P(x)) --> Q"; |
76 goal LK.thy "|- (EX x. P(x)-->Q) <-> (ALL x. P(x)) --> Q"; |
77 by (fast_tac LK_pack 1); |
77 by (fast_tac LK_pack 1); |
78 result(); |
78 result(); |
79 (*5 secs*) |
79 (*5 secs*) |
80 |
80 |
81 |
81 |
82 goal LK.thy "|- (ALL x.P(x)) | Q <-> (ALL x. P(x) | Q)"; |
82 goal LK.thy "|- (ALL x. P(x)) | Q <-> (ALL x. P(x) | Q)"; |
83 by (fast_tac LK_pack 1); |
83 by (fast_tac LK_pack 1); |
84 result(); |
84 result(); |
85 |
85 |
86 |
86 |
87 writeln"Basic test of quantifier reasoning"; |
87 writeln"Basic test of quantifier reasoning"; |
107 (*INVALID*) |
107 (*INVALID*) |
108 goal LK.thy "|- (EX x. Q(x)) --> (ALL x. Q(x))"; |
108 goal LK.thy "|- (EX x. Q(x)) --> (ALL x. Q(x))"; |
109 by (fast_tac LK_pack 1) handle ERROR => writeln"Failed, as expected"; |
109 by (fast_tac LK_pack 1) handle ERROR => writeln"Failed, as expected"; |
110 getgoal 1; |
110 getgoal 1; |
111 |
111 |
112 goal LK.thy "|- P(?a) --> (ALL x.P(x))"; |
112 goal LK.thy "|- P(?a) --> (ALL x. P(x))"; |
113 by (fast_tac LK_pack 1) handle ERROR => writeln"Failed, as expected"; |
113 by (fast_tac LK_pack 1) handle ERROR => writeln"Failed, as expected"; |
114 (*Check that subgoals remain: proof failed.*) |
114 (*Check that subgoals remain: proof failed.*) |
115 getgoal 1; |
115 getgoal 1; |
116 |
116 |
117 goal LK.thy "|- (P(?a) --> (ALL x.Q(x))) --> (ALL x. P(x) --> Q(x))"; |
117 goal LK.thy "|- (P(?a) --> (ALL x. Q(x))) --> (ALL x. P(x) --> Q(x))"; |
118 by (fast_tac LK_pack 1) handle ERROR => writeln"Failed, as expected"; |
118 by (fast_tac LK_pack 1) handle ERROR => writeln"Failed, as expected"; |
119 getgoal 1; |
119 getgoal 1; |
120 |
120 |
121 |
121 |
122 writeln"Back to things that are provable..."; |
122 writeln"Back to things that are provable..."; |
123 |
123 |
124 goal LK.thy "|- (ALL x. P(x)-->Q(x)) & (EX x.P(x)) --> (EX x.Q(x))"; |
124 goal LK.thy "|- (ALL x. P(x)-->Q(x)) & (EX x. P(x)) --> (EX x. Q(x))"; |
125 by (fast_tac LK_pack 1); |
125 by (fast_tac LK_pack 1); |
126 result(); |
126 result(); |
127 |
127 |
128 (*An example of why exR should be delayed as long as possible*) |
128 (*An example of why exR should be delayed as long as possible*) |
129 goal LK.thy "|- (P--> (EX x.Q(x))) & P--> (EX x.Q(x))"; |
129 goal LK.thy "|- (P--> (EX x. Q(x))) & P--> (EX x. Q(x))"; |
130 by (fast_tac LK_pack 1); |
130 by (fast_tac LK_pack 1); |
131 result(); |
131 result(); |
132 |
132 |
133 writeln"Solving for a Var"; |
133 writeln"Solving for a Var"; |
134 goal LK.thy |
134 goal LK.thy |
143 by (fast_tac LK_pack 1); |
143 by (fast_tac LK_pack 1); |
144 result(); |
144 result(); |
145 |
145 |
146 |
146 |
147 writeln"Principia Mathematica *11.55"; |
147 writeln"Principia Mathematica *11.55"; |
148 goal LK.thy "|- (EX x y. P(x) & Q(x,y)) <-> (EX x. P(x) & (EX y.Q(x,y)))"; |
148 goal LK.thy "|- (EX x y. P(x) & Q(x,y)) <-> (EX x. P(x) & (EX y. Q(x,y)))"; |
149 by (fast_tac LK_pack 1); |
149 by (fast_tac LK_pack 1); |
150 result(); |
150 result(); |
151 |
151 |
152 writeln"Principia Mathematica *11.61"; |
152 writeln"Principia Mathematica *11.61"; |
153 goal LK.thy |
153 goal LK.thy |