31 *) |
31 *) |
32 |
32 |
33 text "Pelletier's examples" |
33 text "Pelletier's examples" |
34 (*1*) |
34 (*1*) |
35 schematic_goal "?p : (P-->Q) <-> (~Q --> ~P)" |
35 schematic_goal "?p : (P-->Q) <-> (~Q --> ~P)" |
36 by (tactic "fast_tac @{context} FOLP_cs 1") |
36 by (tactic "fast_tac \<^context> FOLP_cs 1") |
37 |
37 |
38 (*2*) |
38 (*2*) |
39 schematic_goal "?p : ~ ~ P <-> P" |
39 schematic_goal "?p : ~ ~ P <-> P" |
40 by (tactic "fast_tac @{context} FOLP_cs 1") |
40 by (tactic "fast_tac \<^context> FOLP_cs 1") |
41 |
41 |
42 (*3*) |
42 (*3*) |
43 schematic_goal "?p : ~(P-->Q) --> (Q-->P)" |
43 schematic_goal "?p : ~(P-->Q) --> (Q-->P)" |
44 by (tactic "fast_tac @{context} FOLP_cs 1") |
44 by (tactic "fast_tac \<^context> FOLP_cs 1") |
45 |
45 |
46 (*4*) |
46 (*4*) |
47 schematic_goal "?p : (~P-->Q) <-> (~Q --> P)" |
47 schematic_goal "?p : (~P-->Q) <-> (~Q --> P)" |
48 by (tactic "fast_tac @{context} FOLP_cs 1") |
48 by (tactic "fast_tac \<^context> FOLP_cs 1") |
49 |
49 |
50 (*5*) |
50 (*5*) |
51 schematic_goal "?p : ((P|Q)-->(P|R)) --> (P|(Q-->R))" |
51 schematic_goal "?p : ((P|Q)-->(P|R)) --> (P|(Q-->R))" |
52 by (tactic "fast_tac @{context} FOLP_cs 1") |
52 by (tactic "fast_tac \<^context> FOLP_cs 1") |
53 |
53 |
54 (*6*) |
54 (*6*) |
55 schematic_goal "?p : P | ~ P" |
55 schematic_goal "?p : P | ~ P" |
56 by (tactic "fast_tac @{context} FOLP_cs 1") |
56 by (tactic "fast_tac \<^context> FOLP_cs 1") |
57 |
57 |
58 (*7*) |
58 (*7*) |
59 schematic_goal "?p : P | ~ ~ ~ P" |
59 schematic_goal "?p : P | ~ ~ ~ P" |
60 by (tactic "fast_tac @{context} FOLP_cs 1") |
60 by (tactic "fast_tac \<^context> FOLP_cs 1") |
61 |
61 |
62 (*8. Peirce's law*) |
62 (*8. Peirce's law*) |
63 schematic_goal "?p : ((P-->Q) --> P) --> P" |
63 schematic_goal "?p : ((P-->Q) --> P) --> P" |
64 by (tactic "fast_tac @{context} FOLP_cs 1") |
64 by (tactic "fast_tac \<^context> FOLP_cs 1") |
65 |
65 |
66 (*9*) |
66 (*9*) |
67 schematic_goal "?p : ((P|Q) & (~P|Q) & (P| ~Q)) --> ~ (~P | ~Q)" |
67 schematic_goal "?p : ((P|Q) & (~P|Q) & (P| ~Q)) --> ~ (~P | ~Q)" |
68 by (tactic "fast_tac @{context} FOLP_cs 1") |
68 by (tactic "fast_tac \<^context> FOLP_cs 1") |
69 |
69 |
70 (*10*) |
70 (*10*) |
71 schematic_goal "?p : (Q-->R) & (R-->P&Q) & (P-->Q|R) --> (P<->Q)" |
71 schematic_goal "?p : (Q-->R) & (R-->P&Q) & (P-->Q|R) --> (P<->Q)" |
72 by (tactic "fast_tac @{context} FOLP_cs 1") |
72 by (tactic "fast_tac \<^context> FOLP_cs 1") |
73 |
73 |
74 (*11. Proved in each direction (incorrectly, says Pelletier!!) *) |
74 (*11. Proved in each direction (incorrectly, says Pelletier!!) *) |
75 schematic_goal "?p : P<->P" |
75 schematic_goal "?p : P<->P" |
76 by (tactic "fast_tac @{context} FOLP_cs 1") |
76 by (tactic "fast_tac \<^context> FOLP_cs 1") |
77 |
77 |
78 (*12. "Dijkstra's law"*) |
78 (*12. "Dijkstra's law"*) |
79 schematic_goal "?p : ((P <-> Q) <-> R) <-> (P <-> (Q <-> R))" |
79 schematic_goal "?p : ((P <-> Q) <-> R) <-> (P <-> (Q <-> R))" |
80 by (tactic "fast_tac @{context} FOLP_cs 1") |
80 by (tactic "fast_tac \<^context> FOLP_cs 1") |
81 |
81 |
82 (*13. Distributive law*) |
82 (*13. Distributive law*) |
83 schematic_goal "?p : P | (Q & R) <-> (P | Q) & (P | R)" |
83 schematic_goal "?p : P | (Q & R) <-> (P | Q) & (P | R)" |
84 by (tactic "fast_tac @{context} FOLP_cs 1") |
84 by (tactic "fast_tac \<^context> FOLP_cs 1") |
85 |
85 |
86 (*14*) |
86 (*14*) |
87 schematic_goal "?p : (P <-> Q) <-> ((Q | ~P) & (~Q|P))" |
87 schematic_goal "?p : (P <-> Q) <-> ((Q | ~P) & (~Q|P))" |
88 by (tactic "fast_tac @{context} FOLP_cs 1") |
88 by (tactic "fast_tac \<^context> FOLP_cs 1") |
89 |
89 |
90 (*15*) |
90 (*15*) |
91 schematic_goal "?p : (P --> Q) <-> (~P | Q)" |
91 schematic_goal "?p : (P --> Q) <-> (~P | Q)" |
92 by (tactic "fast_tac @{context} FOLP_cs 1") |
92 by (tactic "fast_tac \<^context> FOLP_cs 1") |
93 |
93 |
94 (*16*) |
94 (*16*) |
95 schematic_goal "?p : (P-->Q) | (Q-->P)" |
95 schematic_goal "?p : (P-->Q) | (Q-->P)" |
96 by (tactic "fast_tac @{context} FOLP_cs 1") |
96 by (tactic "fast_tac \<^context> FOLP_cs 1") |
97 |
97 |
98 (*17*) |
98 (*17*) |
99 schematic_goal "?p : ((P & (Q-->R))-->S) <-> ((~P | Q | S) & (~P | ~R | S))" |
99 schematic_goal "?p : ((P & (Q-->R))-->S) <-> ((~P | Q | S) & (~P | ~R | S))" |
100 by (tactic "fast_tac @{context} FOLP_cs 1") |
100 by (tactic "fast_tac \<^context> FOLP_cs 1") |
101 |
101 |
102 |
102 |
103 text "Classical Logic: examples with quantifiers" |
103 text "Classical Logic: examples with quantifiers" |
104 |
104 |
105 schematic_goal "?p : (ALL x. P(x) & Q(x)) <-> (ALL x. P(x)) & (ALL x. Q(x))" |
105 schematic_goal "?p : (ALL x. P(x) & Q(x)) <-> (ALL x. P(x)) & (ALL x. Q(x))" |
106 by (tactic "fast_tac @{context} FOLP_cs 1") |
106 by (tactic "fast_tac \<^context> FOLP_cs 1") |
107 |
107 |
108 schematic_goal "?p : (EX x. P-->Q(x)) <-> (P --> (EX x. Q(x)))" |
108 schematic_goal "?p : (EX x. P-->Q(x)) <-> (P --> (EX x. Q(x)))" |
109 by (tactic "fast_tac @{context} FOLP_cs 1") |
109 by (tactic "fast_tac \<^context> FOLP_cs 1") |
110 |
110 |
111 schematic_goal "?p : (EX x. P(x)-->Q) <-> (ALL x. P(x)) --> Q" |
111 schematic_goal "?p : (EX x. P(x)-->Q) <-> (ALL x. P(x)) --> Q" |
112 by (tactic "fast_tac @{context} FOLP_cs 1") |
112 by (tactic "fast_tac \<^context> FOLP_cs 1") |
113 |
113 |
114 schematic_goal "?p : (ALL x. P(x)) | Q <-> (ALL x. P(x) | Q)" |
114 schematic_goal "?p : (ALL x. P(x)) | Q <-> (ALL x. P(x) | Q)" |
115 by (tactic "fast_tac @{context} FOLP_cs 1") |
115 by (tactic "fast_tac \<^context> FOLP_cs 1") |
116 |
116 |
117 |
117 |
118 text "Problems requiring quantifier duplication" |
118 text "Problems requiring quantifier duplication" |
119 |
119 |
120 (*Needs multiple instantiation of ALL.*) |
120 (*Needs multiple instantiation of ALL.*) |
121 schematic_goal "?p : (ALL x. P(x)-->P(f(x))) & P(d)-->P(f(f(f(d))))" |
121 schematic_goal "?p : (ALL x. P(x)-->P(f(x))) & P(d)-->P(f(f(f(d))))" |
122 by (tactic "best_tac @{context} FOLP_dup_cs 1") |
122 by (tactic "best_tac \<^context> FOLP_dup_cs 1") |
123 |
123 |
124 (*Needs double instantiation of the quantifier*) |
124 (*Needs double instantiation of the quantifier*) |
125 schematic_goal "?p : EX x. P(x) --> P(a) & P(b)" |
125 schematic_goal "?p : EX x. P(x) --> P(a) & P(b)" |
126 by (tactic "best_tac @{context} FOLP_dup_cs 1") |
126 by (tactic "best_tac \<^context> FOLP_dup_cs 1") |
127 |
127 |
128 schematic_goal "?p : EX z. P(z) --> (ALL x. P(x))" |
128 schematic_goal "?p : EX z. P(z) --> (ALL x. P(x))" |
129 by (tactic "best_tac @{context} FOLP_dup_cs 1") |
129 by (tactic "best_tac \<^context> FOLP_dup_cs 1") |
130 |
130 |
131 |
131 |
132 text "Hard examples with quantifiers" |
132 text "Hard examples with quantifiers" |
133 |
133 |
134 text "Problem 18" |
134 text "Problem 18" |
135 schematic_goal "?p : EX y. ALL x. P(y)-->P(x)" |
135 schematic_goal "?p : EX y. ALL x. P(y)-->P(x)" |
136 by (tactic "best_tac @{context} FOLP_dup_cs 1") |
136 by (tactic "best_tac \<^context> FOLP_dup_cs 1") |
137 |
137 |
138 text "Problem 19" |
138 text "Problem 19" |
139 schematic_goal "?p : EX x. ALL y z. (P(y)-->Q(z)) --> (P(x)-->Q(x))" |
139 schematic_goal "?p : EX x. ALL y z. (P(y)-->Q(z)) --> (P(x)-->Q(x))" |
140 by (tactic "best_tac @{context} FOLP_dup_cs 1") |
140 by (tactic "best_tac \<^context> FOLP_dup_cs 1") |
141 |
141 |
142 text "Problem 20" |
142 text "Problem 20" |
143 schematic_goal "?p : (ALL x y. EX z. ALL w. (P(x)&Q(y)-->R(z)&S(w))) |
143 schematic_goal "?p : (ALL x y. EX z. ALL w. (P(x)&Q(y)-->R(z)&S(w))) |
144 --> (EX x y. P(x) & Q(y)) --> (EX z. R(z))" |
144 --> (EX x y. P(x) & Q(y)) --> (EX z. R(z))" |
145 by (tactic "fast_tac @{context} FOLP_cs 1") |
145 by (tactic "fast_tac \<^context> FOLP_cs 1") |
146 |
146 |
147 text "Problem 21" |
147 text "Problem 21" |
148 schematic_goal "?p : (EX x. P-->Q(x)) & (EX x. Q(x)-->P) --> (EX x. P<->Q(x))" |
148 schematic_goal "?p : (EX x. P-->Q(x)) & (EX x. Q(x)-->P) --> (EX x. P<->Q(x))" |
149 by (tactic "best_tac @{context} FOLP_dup_cs 1") |
149 by (tactic "best_tac \<^context> FOLP_dup_cs 1") |
150 |
150 |
151 text "Problem 22" |
151 text "Problem 22" |
152 schematic_goal "?p : (ALL x. P <-> Q(x)) --> (P <-> (ALL x. Q(x)))" |
152 schematic_goal "?p : (ALL x. P <-> Q(x)) --> (P <-> (ALL x. Q(x)))" |
153 by (tactic "fast_tac @{context} FOLP_cs 1") |
153 by (tactic "fast_tac \<^context> FOLP_cs 1") |
154 |
154 |
155 text "Problem 23" |
155 text "Problem 23" |
156 schematic_goal "?p : (ALL x. P | Q(x)) <-> (P | (ALL x. Q(x)))" |
156 schematic_goal "?p : (ALL x. P | Q(x)) <-> (P | (ALL x. Q(x)))" |
157 by (tactic "best_tac @{context} FOLP_dup_cs 1") |
157 by (tactic "best_tac \<^context> FOLP_dup_cs 1") |
158 |
158 |
159 text "Problem 24" |
159 text "Problem 24" |
160 schematic_goal "?p : ~(EX x. S(x)&Q(x)) & (ALL x. P(x) --> Q(x)|R(x)) & |
160 schematic_goal "?p : ~(EX x. S(x)&Q(x)) & (ALL x. P(x) --> Q(x)|R(x)) & |
161 (~(EX x. P(x)) --> (EX x. Q(x))) & (ALL x. Q(x)|R(x) --> S(x)) |
161 (~(EX x. P(x)) --> (EX x. Q(x))) & (ALL x. Q(x)|R(x) --> S(x)) |
162 --> (EX x. P(x)&R(x))" |
162 --> (EX x. P(x)&R(x))" |
163 by (tactic "fast_tac @{context} FOLP_cs 1") |
163 by (tactic "fast_tac \<^context> FOLP_cs 1") |
164 |
164 |
165 text "Problem 25" |
165 text "Problem 25" |
166 schematic_goal "?p : (EX x. P(x)) & |
166 schematic_goal "?p : (EX x. P(x)) & |
167 (ALL x. L(x) --> ~ (M(x) & R(x))) & |
167 (ALL x. L(x) --> ~ (M(x) & R(x))) & |
168 (ALL x. P(x) --> (M(x) & L(x))) & |
168 (ALL x. P(x) --> (M(x) & L(x))) & |
172 |
172 |
173 text "Problem 26" |
173 text "Problem 26" |
174 schematic_goal "?u : ((EX x. p(x)) <-> (EX x. q(x))) & |
174 schematic_goal "?u : ((EX x. p(x)) <-> (EX x. q(x))) & |
175 (ALL x. ALL y. p(x) & q(y) --> (r(x) <-> s(y))) |
175 (ALL x. ALL y. p(x) & q(y) --> (r(x) <-> s(y))) |
176 --> ((ALL x. p(x)-->r(x)) <-> (ALL x. q(x)-->s(x)))" |
176 --> ((ALL x. p(x)-->r(x)) <-> (ALL x. q(x)-->s(x)))" |
177 by (tactic "fast_tac @{context} FOLP_cs 1") |
177 by (tactic "fast_tac \<^context> FOLP_cs 1") |
178 |
178 |
179 text "Problem 27" |
179 text "Problem 27" |
180 schematic_goal "?p : (EX x. P(x) & ~Q(x)) & |
180 schematic_goal "?p : (EX x. P(x) & ~Q(x)) & |
181 (ALL x. P(x) --> R(x)) & |
181 (ALL x. P(x) --> R(x)) & |
182 (ALL x. M(x) & L(x) --> P(x)) & |
182 (ALL x. M(x) & L(x) --> P(x)) & |
183 ((EX x. R(x) & ~ Q(x)) --> (ALL x. L(x) --> ~ R(x))) |
183 ((EX x. R(x) & ~ Q(x)) --> (ALL x. L(x) --> ~ R(x))) |
184 --> (ALL x. M(x) --> ~L(x))" |
184 --> (ALL x. M(x) --> ~L(x))" |
185 by (tactic "fast_tac @{context} FOLP_cs 1") |
185 by (tactic "fast_tac \<^context> FOLP_cs 1") |
186 |
186 |
187 text "Problem 28. AMENDED" |
187 text "Problem 28. AMENDED" |
188 schematic_goal "?p : (ALL x. P(x) --> (ALL x. Q(x))) & |
188 schematic_goal "?p : (ALL x. P(x) --> (ALL x. Q(x))) & |
189 ((ALL x. Q(x)|R(x)) --> (EX x. Q(x)&S(x))) & |
189 ((ALL x. Q(x)|R(x)) --> (EX x. Q(x)&S(x))) & |
190 ((EX x. S(x)) --> (ALL x. L(x) --> M(x))) |
190 ((EX x. S(x)) --> (ALL x. L(x) --> M(x))) |
191 --> (ALL x. P(x) & L(x) --> M(x))" |
191 --> (ALL x. P(x) & L(x) --> M(x))" |
192 by (tactic "fast_tac @{context} FOLP_cs 1") |
192 by (tactic "fast_tac \<^context> FOLP_cs 1") |
193 |
193 |
194 text "Problem 29. Essentially the same as Principia Mathematica *11.71" |
194 text "Problem 29. Essentially the same as Principia Mathematica *11.71" |
195 schematic_goal "?p : (EX x. P(x)) & (EX y. Q(y)) |
195 schematic_goal "?p : (EX x. P(x)) & (EX y. Q(y)) |
196 --> ((ALL x. P(x)-->R(x)) & (ALL y. Q(y)-->S(y)) <-> |
196 --> ((ALL x. P(x)-->R(x)) & (ALL y. Q(y)-->S(y)) <-> |
197 (ALL x y. P(x) & Q(y) --> R(x) & S(y)))" |
197 (ALL x y. P(x) & Q(y) --> R(x) & S(y)))" |
198 by (tactic "fast_tac @{context} FOLP_cs 1") |
198 by (tactic "fast_tac \<^context> FOLP_cs 1") |
199 |
199 |
200 text "Problem 30" |
200 text "Problem 30" |
201 schematic_goal "?p : (ALL x. P(x) | Q(x) --> ~ R(x)) & |
201 schematic_goal "?p : (ALL x. P(x) | Q(x) --> ~ R(x)) & |
202 (ALL x. (Q(x) --> ~ S(x)) --> P(x) & R(x)) |
202 (ALL x. (Q(x) --> ~ S(x)) --> P(x) & R(x)) |
203 --> (ALL x. S(x))" |
203 --> (ALL x. S(x))" |
204 by (tactic "fast_tac @{context} FOLP_cs 1") |
204 by (tactic "fast_tac \<^context> FOLP_cs 1") |
205 |
205 |
206 text "Problem 31" |
206 text "Problem 31" |
207 schematic_goal "?p : ~(EX x. P(x) & (Q(x) | R(x))) & |
207 schematic_goal "?p : ~(EX x. P(x) & (Q(x) | R(x))) & |
208 (EX x. L(x) & P(x)) & |
208 (EX x. L(x) & P(x)) & |
209 (ALL x. ~ R(x) --> M(x)) |
209 (ALL x. ~ R(x) --> M(x)) |
210 --> (EX x. L(x) & M(x))" |
210 --> (EX x. L(x) & M(x))" |
211 by (tactic "fast_tac @{context} FOLP_cs 1") |
211 by (tactic "fast_tac \<^context> FOLP_cs 1") |
212 |
212 |
213 text "Problem 32" |
213 text "Problem 32" |
214 schematic_goal "?p : (ALL x. P(x) & (Q(x)|R(x))-->S(x)) & |
214 schematic_goal "?p : (ALL x. P(x) & (Q(x)|R(x))-->S(x)) & |
215 (ALL x. S(x) & R(x) --> L(x)) & |
215 (ALL x. S(x) & R(x) --> L(x)) & |
216 (ALL x. M(x) --> R(x)) |
216 (ALL x. M(x) --> R(x)) |
217 --> (ALL x. P(x) & M(x) --> L(x))" |
217 --> (ALL x. P(x) & M(x) --> L(x))" |
218 by (tactic "best_tac @{context} FOLP_dup_cs 1") |
218 by (tactic "best_tac \<^context> FOLP_dup_cs 1") |
219 |
219 |
220 text "Problem 33" |
220 text "Problem 33" |
221 schematic_goal "?p : (ALL x. P(a) & (P(x)-->P(b))-->P(c)) <-> |
221 schematic_goal "?p : (ALL x. P(a) & (P(x)-->P(b))-->P(c)) <-> |
222 (ALL x. (~P(a) | P(x) | P(c)) & (~P(a) | ~P(b) | P(c)))" |
222 (ALL x. (~P(a) | P(x) | P(c)) & (~P(a) | ~P(b) | P(c)))" |
223 by (tactic "best_tac @{context} FOLP_dup_cs 1") |
223 by (tactic "best_tac \<^context> FOLP_dup_cs 1") |
224 |
224 |
225 text "Problem 35" |
225 text "Problem 35" |
226 schematic_goal "?p : EX x y. P(x,y) --> (ALL u v. P(u,v))" |
226 schematic_goal "?p : EX x y. P(x,y) --> (ALL u v. P(u,v))" |
227 by (tactic "best_tac @{context} FOLP_dup_cs 1") |
227 by (tactic "best_tac \<^context> FOLP_dup_cs 1") |
228 |
228 |
229 text "Problem 36" |
229 text "Problem 36" |
230 schematic_goal |
230 schematic_goal |
231 "?p : (ALL x. EX y. J(x,y)) & |
231 "?p : (ALL x. EX y. J(x,y)) & |
232 (ALL x. EX y. G(x,y)) & |
232 (ALL x. EX y. G(x,y)) & |
233 (ALL x y. J(x,y) | G(x,y) --> (ALL z. J(y,z) | G(y,z) --> H(x,z))) |
233 (ALL x y. J(x,y) | G(x,y) --> (ALL z. J(y,z) | G(y,z) --> H(x,z))) |
234 --> (ALL x. EX y. H(x,y))" |
234 --> (ALL x. EX y. H(x,y))" |
235 by (tactic "fast_tac @{context} FOLP_cs 1") |
235 by (tactic "fast_tac \<^context> FOLP_cs 1") |
236 |
236 |
237 text "Problem 37" |
237 text "Problem 37" |
238 schematic_goal "?p : (ALL z. EX w. ALL x. EX y. |
238 schematic_goal "?p : (ALL z. EX w. ALL x. EX y. |
239 (P(x,z)-->P(y,w)) & P(y,z) & (P(y,w) --> (EX u. Q(u,w)))) & |
239 (P(x,z)-->P(y,w)) & P(y,z) & (P(y,w) --> (EX u. Q(u,w)))) & |
240 (ALL x z. ~P(x,z) --> (EX y. Q(y,z))) & |
240 (ALL x z. ~P(x,z) --> (EX y. Q(y,z))) & |
241 ((EX x y. Q(x,y)) --> (ALL x. R(x,x))) |
241 ((EX x y. Q(x,y)) --> (ALL x. R(x,x))) |
242 --> (ALL x. EX y. R(x,y))" |
242 --> (ALL x. EX y. R(x,y))" |
243 by (tactic "fast_tac @{context} FOLP_cs 1") |
243 by (tactic "fast_tac \<^context> FOLP_cs 1") |
244 |
244 |
245 text "Problem 39" |
245 text "Problem 39" |
246 schematic_goal "?p : ~ (EX x. ALL y. F(y,x) <-> ~F(y,y))" |
246 schematic_goal "?p : ~ (EX x. ALL y. F(y,x) <-> ~F(y,y))" |
247 by (tactic "fast_tac @{context} FOLP_cs 1") |
247 by (tactic "fast_tac \<^context> FOLP_cs 1") |
248 |
248 |
249 text "Problem 40. AMENDED" |
249 text "Problem 40. AMENDED" |
250 schematic_goal "?p : (EX y. ALL x. F(x,y) <-> F(x,x)) --> |
250 schematic_goal "?p : (EX y. ALL x. F(x,y) <-> F(x,x)) --> |
251 ~(ALL x. EX y. ALL z. F(z,y) <-> ~ F(z,x))" |
251 ~(ALL x. EX y. ALL z. F(z,y) <-> ~ F(z,x))" |
252 by (tactic "fast_tac @{context} FOLP_cs 1") |
252 by (tactic "fast_tac \<^context> FOLP_cs 1") |
253 |
253 |
254 text "Problem 41" |
254 text "Problem 41" |
255 schematic_goal "?p : (ALL z. EX y. ALL x. f(x,y) <-> f(x,z) & ~ f(x,x)) |
255 schematic_goal "?p : (ALL z. EX y. ALL x. f(x,y) <-> f(x,z) & ~ f(x,x)) |
256 --> ~ (EX z. ALL x. f(x,z))" |
256 --> ~ (EX z. ALL x. f(x,z))" |
257 by (tactic "best_tac @{context} FOLP_dup_cs 1") |
257 by (tactic "best_tac \<^context> FOLP_dup_cs 1") |
258 |
258 |
259 text "Problem 44" |
259 text "Problem 44" |
260 schematic_goal "?p : (ALL x. f(x) --> |
260 schematic_goal "?p : (ALL x. f(x) --> |
261 (EX y. g(y) & h(x,y) & (EX y. g(y) & ~ h(x,y)))) & |
261 (EX y. g(y) & h(x,y) & (EX y. g(y) & ~ h(x,y)))) & |
262 (EX x. j(x) & (ALL y. g(y) --> h(x,y))) |
262 (EX x. j(x) & (ALL y. g(y) --> h(x,y))) |
263 --> (EX x. j(x) & ~f(x))" |
263 --> (EX x. j(x) & ~f(x))" |
264 by (tactic "fast_tac @{context} FOLP_cs 1") |
264 by (tactic "fast_tac \<^context> FOLP_cs 1") |
265 |
265 |
266 text "Problems (mainly) involving equality or functions" |
266 text "Problems (mainly) involving equality or functions" |
267 |
267 |
268 text "Problem 48" |
268 text "Problem 48" |
269 schematic_goal "?p : (a=b | c=d) & (a=c | b=d) --> a=d | b=c" |
269 schematic_goal "?p : (a=b | c=d) & (a=c | b=d) --> a=d | b=c" |
270 by (tactic "fast_tac @{context} FOLP_cs 1") |
270 by (tactic "fast_tac \<^context> FOLP_cs 1") |
271 |
271 |
272 text "Problem 50" |
272 text "Problem 50" |
273 (*What has this to do with equality?*) |
273 (*What has this to do with equality?*) |
274 schematic_goal "?p : (ALL x. P(a,x) | (ALL y. P(x,y))) --> (EX x. ALL y. P(x,y))" |
274 schematic_goal "?p : (ALL x. P(a,x) | (ALL y. P(x,y))) --> (EX x. ALL y. P(x,y))" |
275 by (tactic "best_tac @{context} FOLP_dup_cs 1") |
275 by (tactic "best_tac \<^context> FOLP_dup_cs 1") |
276 |
276 |
277 text "Problem 56" |
277 text "Problem 56" |
278 schematic_goal |
278 schematic_goal |
279 "?p : (ALL x. (EX y. P(y) & x=f(y)) --> P(x)) <-> (ALL x. P(x) --> P(f(x)))" |
279 "?p : (ALL x. (EX y. P(y) & x=f(y)) --> P(x)) <-> (ALL x. P(x) --> P(f(x)))" |
280 by (tactic "fast_tac @{context} FOLP_cs 1") |
280 by (tactic "fast_tac \<^context> FOLP_cs 1") |
281 |
281 |
282 text "Problem 57" |
282 text "Problem 57" |
283 schematic_goal |
283 schematic_goal |
284 "?p : P(f(a,b), f(b,c)) & P(f(b,c), f(a,c)) & |
284 "?p : P(f(a,b), f(b,c)) & P(f(b,c), f(a,c)) & |
285 (ALL x y z. P(x,y) & P(y,z) --> P(x,z)) --> P(f(a,b), f(a,c))" |
285 (ALL x y z. P(x,y) & P(y,z) --> P(x,z)) --> P(f(a,b), f(a,c))" |
286 by (tactic "fast_tac @{context} FOLP_cs 1") |
286 by (tactic "fast_tac \<^context> FOLP_cs 1") |
287 |
287 |
288 text "Problem 58 NOT PROVED AUTOMATICALLY" |
288 text "Problem 58 NOT PROVED AUTOMATICALLY" |
289 schematic_goal "?p : (ALL x y. f(x)=g(y)) --> (ALL x y. f(f(x))=f(g(y)))" |
289 schematic_goal "?p : (ALL x y. f(x)=g(y)) --> (ALL x y. f(f(x))=f(g(y)))" |
290 supply f_cong = subst_context [where t = f] |
290 supply f_cong = subst_context [where t = f] |
291 by (tactic \<open>fast_tac @{context} (FOLP_cs addSIs [@{thm f_cong}]) 1\<close>) |
291 by (tactic \<open>fast_tac \<^context> (FOLP_cs addSIs [@{thm f_cong}]) 1\<close>) |
292 |
292 |
293 text "Problem 59" |
293 text "Problem 59" |
294 schematic_goal "?p : (ALL x. P(x) <-> ~P(f(x))) --> (EX x. P(x) & ~P(f(x)))" |
294 schematic_goal "?p : (ALL x. P(x) <-> ~P(f(x))) --> (EX x. P(x) & ~P(f(x)))" |
295 by (tactic "best_tac @{context} FOLP_dup_cs 1") |
295 by (tactic "best_tac \<^context> FOLP_dup_cs 1") |
296 |
296 |
297 text "Problem 60" |
297 text "Problem 60" |
298 schematic_goal "?p : ALL x. P(x,f(x)) <-> (EX y. (ALL z. P(z,y) --> P(z,f(x))) & P(x,y))" |
298 schematic_goal "?p : ALL x. P(x,f(x)) <-> (EX y. (ALL z. P(z,y) --> P(z,f(x))) & P(x,y))" |
299 by (tactic "fast_tac @{context} FOLP_cs 1") |
299 by (tactic "fast_tac \<^context> FOLP_cs 1") |
300 |
300 |
301 end |
301 end |