|
1 (* Title: HOL/ex/Classical |
|
2 ID: $Id$ |
|
3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
|
4 Copyright 1994 University of Cambridge |
|
5 *) |
|
6 |
|
7 header{*Classical Predicate Calculus Problems*} |
|
8 |
|
9 theory Classical = Main: |
|
10 |
|
11 subsection{*Traditional Classical Reasoner*} |
|
12 |
|
13 text{*Taken from @{text "FOL/cla.ML"}. When porting examples from first-order |
|
14 logic, beware of the precedence of @{text "="} versus @{text "\<leftrightarrow>"}.*} |
|
15 |
|
16 lemma "(P --> Q | R) --> (P-->Q) | (P-->R)" |
|
17 by blast |
|
18 |
|
19 text{*If and only if*} |
|
20 |
|
21 lemma "(P=Q) = (Q = (P::bool))" |
|
22 by blast |
|
23 |
|
24 lemma "~ (P = (~P))" |
|
25 by blast |
|
26 |
|
27 |
|
28 text{*Sample problems from |
|
29 F. J. Pelletier, |
|
30 Seventy-Five Problems for Testing Automatic Theorem Provers, |
|
31 J. Automated Reasoning 2 (1986), 191-216. |
|
32 Errata, JAR 4 (1988), 236-236. |
|
33 |
|
34 The hardest problems -- judging by experience with several theorem provers, |
|
35 including matrix ones -- are 34 and 43. |
|
36 *} |
|
37 |
|
38 subsubsection{*Pelletier's examples*} |
|
39 |
|
40 text{*1*} |
|
41 lemma "(P-->Q) = (~Q --> ~P)" |
|
42 by blast |
|
43 |
|
44 text{*2*} |
|
45 lemma "(~ ~ P) = P" |
|
46 by blast |
|
47 |
|
48 text{*3*} |
|
49 lemma "~(P-->Q) --> (Q-->P)" |
|
50 by blast |
|
51 |
|
52 text{*4*} |
|
53 lemma "(~P-->Q) = (~Q --> P)" |
|
54 by blast |
|
55 |
|
56 text{*5*} |
|
57 lemma "((P|Q)-->(P|R)) --> (P|(Q-->R))" |
|
58 by blast |
|
59 |
|
60 text{*6*} |
|
61 lemma "P | ~ P" |
|
62 by blast |
|
63 |
|
64 text{*7*} |
|
65 lemma "P | ~ ~ ~ P" |
|
66 by blast |
|
67 |
|
68 text{*8. Peirce's law*} |
|
69 lemma "((P-->Q) --> P) --> P" |
|
70 by blast |
|
71 |
|
72 text{*9*} |
|
73 lemma "((P|Q) & (~P|Q) & (P| ~Q)) --> ~ (~P | ~Q)" |
|
74 by blast |
|
75 |
|
76 text{*10*} |
|
77 lemma "(Q-->R) & (R-->P&Q) & (P-->Q|R) --> (P=Q)" |
|
78 by blast |
|
79 |
|
80 text{*11. Proved in each direction (incorrectly, says Pelletier!!) *} |
|
81 lemma "P=(P::bool)" |
|
82 by blast |
|
83 |
|
84 text{*12. "Dijkstra's law"*} |
|
85 lemma "((P = Q) = R) = (P = (Q = R))" |
|
86 by blast |
|
87 |
|
88 text{*13. Distributive law*} |
|
89 lemma "(P | (Q & R)) = ((P | Q) & (P | R))" |
|
90 by blast |
|
91 |
|
92 text{*14*} |
|
93 lemma "(P = Q) = ((Q | ~P) & (~Q|P))" |
|
94 by blast |
|
95 |
|
96 text{*15*} |
|
97 lemma "(P --> Q) = (~P | Q)" |
|
98 by blast |
|
99 |
|
100 text{*16*} |
|
101 lemma "(P-->Q) | (Q-->P)" |
|
102 by blast |
|
103 |
|
104 text{*17*} |
|
105 lemma "((P & (Q-->R))-->S) = ((~P | Q | S) & (~P | ~R | S))" |
|
106 by blast |
|
107 |
|
108 subsubsection{*Classical Logic: examples with quantifiers*} |
|
109 |
|
110 lemma "(\<forall>x. P(x) & Q(x)) = ((\<forall>x. P(x)) & (\<forall>x. Q(x)))" |
|
111 by blast |
|
112 |
|
113 lemma "(\<exists>x. P-->Q(x)) = (P --> (\<exists>x. Q(x)))" |
|
114 by blast |
|
115 |
|
116 lemma "(\<exists>x. P(x)-->Q) = ((\<forall>x. P(x)) --> Q)" |
|
117 by blast |
|
118 |
|
119 lemma "((\<forall>x. P(x)) | Q) = (\<forall>x. P(x) | Q)" |
|
120 by blast |
|
121 |
|
122 text{*From Wishnu Prasetya*} |
|
123 lemma "(\<forall>s. q(s) --> r(s)) & ~r(s) & (\<forall>s. ~r(s) & ~q(s) --> p(t) | q(t)) |
|
124 --> p(t) | r(t)" |
|
125 by blast |
|
126 |
|
127 |
|
128 subsubsection{*Problems requiring quantifier duplication*} |
|
129 |
|
130 text{*Theorem B of Peter Andrews, Theorem Proving via General Matings, |
|
131 JACM 28 (1981).*} |
|
132 lemma "(\<exists>x. \<forall>y. P(x) = P(y)) --> ((\<exists>x. P(x)) = (\<forall>y. P(y)))" |
|
133 by blast |
|
134 |
|
135 text{*Needs multiple instantiation of the quantifier.*} |
|
136 lemma "(\<forall>x. P(x)-->P(f(x))) & P(d)-->P(f(f(f(d))))" |
|
137 by blast |
|
138 |
|
139 text{*Needs double instantiation of the quantifier*} |
|
140 lemma "\<exists>x. P(x) --> P(a) & P(b)" |
|
141 by blast |
|
142 |
|
143 lemma "\<exists>z. P(z) --> (\<forall>x. P(x))" |
|
144 by blast |
|
145 |
|
146 lemma "\<exists>x. (\<exists>y. P(y)) --> P(x)" |
|
147 by blast |
|
148 |
|
149 subsubsection{*Hard examples with quantifiers*} |
|
150 |
|
151 text{*Problem 18*} |
|
152 lemma "\<exists>y. \<forall>x. P(y)-->P(x)" |
|
153 by blast |
|
154 |
|
155 text{*Problem 19*} |
|
156 lemma "\<exists>x. \<forall>y z. (P(y)-->Q(z)) --> (P(x)-->Q(x))" |
|
157 by blast |
|
158 |
|
159 text{*Problem 20*} |
|
160 lemma "(\<forall>x y. \<exists>z. \<forall>w. (P(x)&Q(y)-->R(z)&S(w))) |
|
161 --> (\<exists>x y. P(x) & Q(y)) --> (\<exists>z. R(z))" |
|
162 by blast |
|
163 |
|
164 text{*Problem 21*} |
|
165 lemma "(\<exists>x. P-->Q(x)) & (\<exists>x. Q(x)-->P) --> (\<exists>x. P=Q(x))" |
|
166 by blast |
|
167 |
|
168 text{*Problem 22*} |
|
169 lemma "(\<forall>x. P = Q(x)) --> (P = (\<forall>x. Q(x)))" |
|
170 by blast |
|
171 |
|
172 text{*Problem 23*} |
|
173 lemma "(\<forall>x. P | Q(x)) = (P | (\<forall>x. Q(x)))" |
|
174 by blast |
|
175 |
|
176 text{*Problem 24*} |
|
177 lemma "~(\<exists>x. S(x)&Q(x)) & (\<forall>x. P(x) --> Q(x)|R(x)) & |
|
178 (~(\<exists>x. P(x)) --> (\<exists>x. Q(x))) & (\<forall>x. Q(x)|R(x) --> S(x)) |
|
179 --> (\<exists>x. P(x)&R(x))" |
|
180 by blast |
|
181 |
|
182 text{*Problem 25*} |
|
183 lemma "(\<exists>x. P(x)) & |
|
184 (\<forall>x. L(x) --> ~ (M(x) & R(x))) & |
|
185 (\<forall>x. P(x) --> (M(x) & L(x))) & |
|
186 ((\<forall>x. P(x)-->Q(x)) | (\<exists>x. P(x)&R(x))) |
|
187 --> (\<exists>x. Q(x)&P(x))" |
|
188 by blast |
|
189 |
|
190 text{*Problem 26*} |
|
191 lemma "((\<exists>x. p(x)) = (\<exists>x. q(x))) & |
|
192 (\<forall>x. \<forall>y. p(x) & q(y) --> (r(x) = s(y))) |
|
193 --> ((\<forall>x. p(x)-->r(x)) = (\<forall>x. q(x)-->s(x)))" |
|
194 by blast |
|
195 |
|
196 text{*Problem 27*} |
|
197 lemma "(\<exists>x. P(x) & ~Q(x)) & |
|
198 (\<forall>x. P(x) --> R(x)) & |
|
199 (\<forall>x. M(x) & L(x) --> P(x)) & |
|
200 ((\<exists>x. R(x) & ~ Q(x)) --> (\<forall>x. L(x) --> ~ R(x))) |
|
201 --> (\<forall>x. M(x) --> ~L(x))" |
|
202 by blast |
|
203 |
|
204 text{*Problem 28. AMENDED*} |
|
205 lemma "(\<forall>x. P(x) --> (\<forall>x. Q(x))) & |
|
206 ((\<forall>x. Q(x)|R(x)) --> (\<exists>x. Q(x)&S(x))) & |
|
207 ((\<exists>x. S(x)) --> (\<forall>x. L(x) --> M(x))) |
|
208 --> (\<forall>x. P(x) & L(x) --> M(x))" |
|
209 by blast |
|
210 |
|
211 text{*Problem 29. Essentially the same as Principia Mathematica *11.71*} |
|
212 lemma "(\<exists>x. F(x)) & (\<exists>y. G(y)) |
|
213 --> ( ((\<forall>x. F(x)-->H(x)) & (\<forall>y. G(y)-->J(y))) = |
|
214 (\<forall>x y. F(x) & G(y) --> H(x) & J(y)))" |
|
215 by blast |
|
216 |
|
217 text{*Problem 30*} |
|
218 lemma "(\<forall>x. P(x) | Q(x) --> ~ R(x)) & |
|
219 (\<forall>x. (Q(x) --> ~ S(x)) --> P(x) & R(x)) |
|
220 --> (\<forall>x. S(x))" |
|
221 by blast |
|
222 |
|
223 text{*Problem 31*} |
|
224 lemma "~(\<exists>x. P(x) & (Q(x) | R(x))) & |
|
225 (\<exists>x. L(x) & P(x)) & |
|
226 (\<forall>x. ~ R(x) --> M(x)) |
|
227 --> (\<exists>x. L(x) & M(x))" |
|
228 by blast |
|
229 |
|
230 text{*Problem 32*} |
|
231 lemma "(\<forall>x. P(x) & (Q(x)|R(x))-->S(x)) & |
|
232 (\<forall>x. S(x) & R(x) --> L(x)) & |
|
233 (\<forall>x. M(x) --> R(x)) |
|
234 --> (\<forall>x. P(x) & M(x) --> L(x))" |
|
235 by blast |
|
236 |
|
237 text{*Problem 33*} |
|
238 lemma "(\<forall>x. P(a) & (P(x)-->P(b))-->P(c)) = |
|
239 (\<forall>x. (~P(a) | P(x) | P(c)) & (~P(a) | ~P(b) | P(c)))" |
|
240 by blast |
|
241 |
|
242 text{*Problem 34 AMENDED (TWICE!!)*} |
|
243 text{*Andrews's challenge*} |
|
244 lemma "((\<exists>x. \<forall>y. p(x) = p(y)) = |
|
245 ((\<exists>x. q(x)) = (\<forall>y. p(y)))) = |
|
246 ((\<exists>x. \<forall>y. q(x) = q(y)) = |
|
247 ((\<exists>x. p(x)) = (\<forall>y. q(y))))" |
|
248 by blast |
|
249 |
|
250 text{*Problem 35*} |
|
251 lemma "\<exists>x y. P x y --> (\<forall>u v. P u v)" |
|
252 by blast |
|
253 |
|
254 text{*Problem 36*} |
|
255 lemma "(\<forall>x. \<exists>y. J x y) & |
|
256 (\<forall>x. \<exists>y. G x y) & |
|
257 (\<forall>x y. J x y | G x y --> |
|
258 (\<forall>z. J y z | G y z --> H x z)) |
|
259 --> (\<forall>x. \<exists>y. H x y)" |
|
260 by blast |
|
261 |
|
262 text{*Problem 37*} |
|
263 lemma "(\<forall>z. \<exists>w. \<forall>x. \<exists>y. |
|
264 (P x z -->P y w) & P y z & (P y w --> (\<exists>u. Q u w))) & |
|
265 (\<forall>x z. ~(P x z) --> (\<exists>y. Q y z)) & |
|
266 ((\<exists>x y. Q x y) --> (\<forall>x. R x x)) |
|
267 --> (\<forall>x. \<exists>y. R x y)" |
|
268 by blast |
|
269 |
|
270 text{*Problem 38*} |
|
271 lemma "(\<forall>x. p(a) & (p(x) --> (\<exists>y. p(y) & r x y)) --> |
|
272 (\<exists>z. \<exists>w. p(z) & r x w & r w z)) = |
|
273 (\<forall>x. (~p(a) | p(x) | (\<exists>z. \<exists>w. p(z) & r x w & r w z)) & |
|
274 (~p(a) | ~(\<exists>y. p(y) & r x y) | |
|
275 (\<exists>z. \<exists>w. p(z) & r x w & r w z)))" |
|
276 by blast (*beats fast!*) |
|
277 |
|
278 text{*Problem 39*} |
|
279 lemma "~ (\<exists>x. \<forall>y. F y x = (~ F y y))" |
|
280 by blast |
|
281 |
|
282 text{*Problem 40. AMENDED*} |
|
283 lemma "(\<exists>y. \<forall>x. F x y = F x x) |
|
284 --> ~ (\<forall>x. \<exists>y. \<forall>z. F z y = (~ F z x))" |
|
285 by blast |
|
286 |
|
287 text{*Problem 41*} |
|
288 lemma "(\<forall>z. \<exists>y. \<forall>x. f x y = (f x z & ~ f x x)) |
|
289 --> ~ (\<exists>z. \<forall>x. f x z)" |
|
290 by blast |
|
291 |
|
292 text{*Problem 42*} |
|
293 lemma "~ (\<exists>y. \<forall>x. p x y = (~ (\<exists>z. p x z & p z x)))" |
|
294 by blast |
|
295 |
|
296 text{*Problem 43!!*} |
|
297 lemma "(\<forall>x::'a. \<forall>y::'a. q x y = (\<forall>z. p z x = (p z y::bool))) |
|
298 --> (\<forall>x. (\<forall>y. q x y = (q y x::bool)))" |
|
299 by blast |
|
300 |
|
301 text{*Problem 44*} |
|
302 lemma "(\<forall>x. f(x) --> |
|
303 (\<exists>y. g(y) & h x y & (\<exists>y. g(y) & ~ h x y))) & |
|
304 (\<exists>x. j(x) & (\<forall>y. g(y) --> h x y)) |
|
305 --> (\<exists>x. j(x) & ~f(x))" |
|
306 by blast |
|
307 |
|
308 text{*Problem 45*} |
|
309 lemma "(\<forall>x. f(x) & (\<forall>y. g(y) & h x y --> j x y) |
|
310 --> (\<forall>y. g(y) & h x y --> k(y))) & |
|
311 ~ (\<exists>y. l(y) & k(y)) & |
|
312 (\<exists>x. f(x) & (\<forall>y. h x y --> l(y)) |
|
313 & (\<forall>y. g(y) & h x y --> j x y)) |
|
314 --> (\<exists>x. f(x) & ~ (\<exists>y. g(y) & h x y))" |
|
315 by blast |
|
316 |
|
317 |
|
318 subsubsection{*Problems (mainly) involving equality or functions*} |
|
319 |
|
320 text{*Problem 48*} |
|
321 lemma "(a=b | c=d) & (a=c | b=d) --> a=d | b=c" |
|
322 by blast |
|
323 |
|
324 text{*Problem 49 NOT PROVED AUTOMATICALLY*} |
|
325 text{*Hard because it involves substitution for Vars |
|
326 the type constraint ensures that x,y,z have the same type as a,b,u. *} |
|
327 lemma "(\<exists>x y::'a. \<forall>z. z=x | z=y) & P(a) & P(b) & (~a=b) |
|
328 --> (\<forall>u::'a. P(u))" |
|
329 apply safe |
|
330 apply (rule_tac x = a in allE, assumption) |
|
331 apply (rule_tac x = b in allE, assumption, fast) --{*blast's treatment of equality can't do it*} |
|
332 done |
|
333 |
|
334 text{*Problem 50. (What has this to do with equality?) *} |
|
335 lemma "(\<forall>x. P a x | (\<forall>y. P x y)) --> (\<exists>x. \<forall>y. P x y)" |
|
336 by blast |
|
337 |
|
338 text{*Problem 51*} |
|
339 lemma "(\<exists>z w. \<forall>x y. P x y = (x=z & y=w)) --> |
|
340 (\<exists>z. \<forall>x. \<exists>w. (\<forall>y. P x y = (y=w)) = (x=z))" |
|
341 by blast |
|
342 |
|
343 text{*Problem 52. Almost the same as 51. *} |
|
344 lemma "(\<exists>z w. \<forall>x y. P x y = (x=z & y=w)) --> |
|
345 (\<exists>w. \<forall>y. \<exists>z. (\<forall>x. P x y = (x=z)) = (y=w))" |
|
346 by blast |
|
347 |
|
348 text{*Problem 55*} |
|
349 |
|
350 text{*Non-equational version, from Manthey and Bry, CADE-9 (Springer, 1988). |
|
351 fast DISCOVERS who killed Agatha. *} |
|
352 lemma "lives(agatha) & lives(butler) & lives(charles) & |
|
353 (killed agatha agatha | killed butler agatha | killed charles agatha) & |
|
354 (\<forall>x y. killed x y --> hates x y & ~richer x y) & |
|
355 (\<forall>x. hates agatha x --> ~hates charles x) & |
|
356 (hates agatha agatha & hates agatha charles) & |
|
357 (\<forall>x. lives(x) & ~richer x agatha --> hates butler x) & |
|
358 (\<forall>x. hates agatha x --> hates butler x) & |
|
359 (\<forall>x. ~hates x agatha | ~hates x butler | ~hates x charles) --> |
|
360 killed ?who agatha" |
|
361 by fast |
|
362 |
|
363 text{*Problem 56*} |
|
364 lemma "(\<forall>x. (\<exists>y. P(y) & x=f(y)) --> P(x)) = (\<forall>x. P(x) --> P(f(x)))" |
|
365 by blast |
|
366 |
|
367 text{*Problem 57*} |
|
368 lemma "P (f a b) (f b c) & P (f b c) (f a c) & |
|
369 (\<forall>x y z. P x y & P y z --> P x z) --> P (f a b) (f a c)" |
|
370 by blast |
|
371 |
|
372 text{*Problem 58 NOT PROVED AUTOMATICALLY*} |
|
373 lemma "(\<forall>x y. f(x)=g(y)) --> (\<forall>x y. f(f(x))=f(g(y)))" |
|
374 by (fast intro: arg_cong [of concl: f]) |
|
375 |
|
376 text{*Problem 59*} |
|
377 lemma "(\<forall>x. P(x) = (~P(f(x)))) --> (\<exists>x. P(x) & ~P(f(x)))" |
|
378 by blast |
|
379 |
|
380 text{*Problem 60*} |
|
381 lemma "\<forall>x. P x (f x) = (\<exists>y. (\<forall>z. P z y --> P z (f x)) & P x y)" |
|
382 by blast |
|
383 |
|
384 text{*Problem 62 as corrected in JAR 18 (1997), page 135*} |
|
385 lemma "(\<forall>x. p a & (p x --> p(f x)) --> p(f(f x))) = |
|
386 (\<forall>x. (~ p a | p x | p(f(f x))) & |
|
387 (~ p a | ~ p(f x) | p(f(f x))))" |
|
388 by blast |
|
389 |
|
390 text{*From Davis, Obvious Logical Inferences, IJCAI-81, 530-531 |
|
391 fast indeed copes!*} |
|
392 lemma "(\<forall>x. F(x) & ~G(x) --> (\<exists>y. H(x,y) & J(y))) & |
|
393 (\<exists>x. K(x) & F(x) & (\<forall>y. H(x,y) --> K(y))) & |
|
394 (\<forall>x. K(x) --> ~G(x)) --> (\<exists>x. K(x) & J(x))" |
|
395 by fast |
|
396 |
|
397 text{*From Rudnicki, Obvious Inferences, JAR 3 (1987), 383-393. |
|
398 It does seem obvious!*} |
|
399 lemma "(\<forall>x. F(x) & ~G(x) --> (\<exists>y. H(x,y) & J(y))) & |
|
400 (\<exists>x. K(x) & F(x) & (\<forall>y. H(x,y) --> K(y))) & |
|
401 (\<forall>x. K(x) --> ~G(x)) --> (\<exists>x. K(x) --> ~G(x))" |
|
402 by fast |
|
403 |
|
404 text{*Attributed to Lewis Carroll by S. G. Pulman. The first or last |
|
405 assumption can be deleted.*} |
|
406 lemma "(\<forall>x. honest(x) & industrious(x) --> healthy(x)) & |
|
407 ~ (\<exists>x. grocer(x) & healthy(x)) & |
|
408 (\<forall>x. industrious(x) & grocer(x) --> honest(x)) & |
|
409 (\<forall>x. cyclist(x) --> industrious(x)) & |
|
410 (\<forall>x. ~healthy(x) & cyclist(x) --> ~honest(x)) |
|
411 --> (\<forall>x. grocer(x) --> ~cyclist(x))" |
|
412 by blast |
|
413 |
|
414 lemma "(\<forall>x y. R(x,y) | R(y,x)) & |
|
415 (\<forall>x y. S(x,y) & S(y,x) --> x=y) & |
|
416 (\<forall>x y. R(x,y) --> S(x,y)) --> (\<forall>x y. S(x,y) --> R(x,y))" |
|
417 by blast |
|
418 |
|
419 |
|
420 subsection{*Model Elimination Prover*} |
|
421 |
|
422 text{*The "small example" from Bezem, Hendriks and de Nivelle, |
|
423 Automatic Proof Construction in Type Theory Using Resolution, |
|
424 JAR 29: 3-4 (2002), pages 253-275 *} |
|
425 lemma "(\<forall>x y z. R(x,y) & R(y,z) --> R(x,z)) & |
|
426 (\<forall>x. \<exists>y. R(x,y)) --> |
|
427 ~ (\<forall>x. P x = (\<forall>y. R(x,y) --> ~ P y))" |
|
428 by (tactic{*safe_best_meson_tac 1*}) |
|
429 --{*In contrast, @{text meson} is SLOW: 15s on a 1.8GHz machine!*} |
|
430 |
|
431 |
|
432 subsubsection{*Pelletier's examples*} |
|
433 text{*1*} |
|
434 lemma "(P --> Q) = (~Q --> ~P)" |
|
435 by meson |
|
436 |
|
437 text{*2*} |
|
438 lemma "(~ ~ P) = P" |
|
439 by meson |
|
440 |
|
441 text{*3*} |
|
442 lemma "~(P-->Q) --> (Q-->P)" |
|
443 by meson |
|
444 |
|
445 text{*4*} |
|
446 lemma "(~P-->Q) = (~Q --> P)" |
|
447 by meson |
|
448 |
|
449 text{*5*} |
|
450 lemma "((P|Q)-->(P|R)) --> (P|(Q-->R))" |
|
451 by meson |
|
452 |
|
453 text{*6*} |
|
454 lemma "P | ~ P" |
|
455 by meson |
|
456 |
|
457 text{*7*} |
|
458 lemma "P | ~ ~ ~ P" |
|
459 by meson |
|
460 |
|
461 text{*8. Peirce's law*} |
|
462 lemma "((P-->Q) --> P) --> P" |
|
463 by meson |
|
464 |
|
465 text{*9*} |
|
466 lemma "((P|Q) & (~P|Q) & (P| ~Q)) --> ~ (~P | ~Q)" |
|
467 by meson |
|
468 |
|
469 text{*10*} |
|
470 lemma "(Q-->R) & (R-->P&Q) & (P-->Q|R) --> (P=Q)" |
|
471 by meson |
|
472 |
|
473 text{*11. Proved in each direction (incorrectly, says Pelletier!!) *} |
|
474 lemma "P=(P::bool)" |
|
475 by meson |
|
476 |
|
477 text{*12. "Dijkstra's law"*} |
|
478 lemma "((P = Q) = R) = (P = (Q = R))" |
|
479 by meson |
|
480 |
|
481 text{*13. Distributive law*} |
|
482 lemma "(P | (Q & R)) = ((P | Q) & (P | R))" |
|
483 by meson |
|
484 |
|
485 text{*14*} |
|
486 lemma "(P = Q) = ((Q | ~P) & (~Q|P))" |
|
487 by meson |
|
488 |
|
489 text{*15*} |
|
490 lemma "(P --> Q) = (~P | Q)" |
|
491 by meson |
|
492 |
|
493 text{*16*} |
|
494 lemma "(P-->Q) | (Q-->P)" |
|
495 by meson |
|
496 |
|
497 text{*17*} |
|
498 lemma "((P & (Q-->R))-->S) = ((~P | Q | S) & (~P | ~R | S))" |
|
499 by meson |
|
500 |
|
501 subsubsection{*Classical Logic: examples with quantifiers*} |
|
502 |
|
503 lemma "(\<forall>x. P x & Q x) = ((\<forall>x. P x) & (\<forall>x. Q x))" |
|
504 by meson |
|
505 |
|
506 lemma "(\<exists>x. P --> Q x) = (P --> (\<exists>x. Q x))" |
|
507 by meson |
|
508 |
|
509 lemma "(\<exists>x. P x --> Q) = ((\<forall>x. P x) --> Q)" |
|
510 by meson |
|
511 |
|
512 lemma "((\<forall>x. P x) | Q) = (\<forall>x. P x | Q)" |
|
513 by meson |
|
514 |
|
515 lemma "(\<forall>x. P x --> P(f x)) & P d --> P(f(f(f d)))" |
|
516 by meson |
|
517 |
|
518 text{*Needs double instantiation of EXISTS*} |
|
519 lemma "\<exists>x. P x --> P a & P b" |
|
520 by meson |
|
521 |
|
522 lemma "\<exists>z. P z --> (\<forall>x. P x)" |
|
523 by meson |
|
524 |
|
525 subsubsection{*Hard examples with quantifiers*} |
|
526 |
|
527 text{*Problem 18*} |
|
528 lemma "\<exists>y. \<forall>x. P y --> P x" |
|
529 by meson |
|
530 |
|
531 text{*Problem 19*} |
|
532 lemma "\<exists>x. \<forall>y z. (P y --> Q z) --> (P x --> Q x)" |
|
533 by meson |
|
534 |
|
535 text{*Problem 20*} |
|
536 lemma "(\<forall>x y. \<exists>z. \<forall>w. (P x & Q y --> R z & S w)) |
|
537 --> (\<exists>x y. P x & Q y) --> (\<exists>z. R z)" |
|
538 by meson |
|
539 |
|
540 text{*Problem 21*} |
|
541 lemma "(\<exists>x. P --> Q x) & (\<exists>x. Q x --> P) --> (\<exists>x. P=Q x)" |
|
542 by meson |
|
543 |
|
544 text{*Problem 22*} |
|
545 lemma "(\<forall>x. P = Q x) --> (P = (\<forall>x. Q x))" |
|
546 by meson |
|
547 |
|
548 text{*Problem 23*} |
|
549 lemma "(\<forall>x. P | Q x) = (P | (\<forall>x. Q x))" |
|
550 by meson |
|
551 |
|
552 text{*Problem 24*} (*The first goal clause is useless*) |
|
553 lemma "~(\<exists>x. S x & Q x) & (\<forall>x. P x --> Q x | R x) & |
|
554 (~(\<exists>x. P x) --> (\<exists>x. Q x)) & (\<forall>x. Q x | R x --> S x) |
|
555 --> (\<exists>x. P x & R x)" |
|
556 by meson |
|
557 |
|
558 text{*Problem 25*} |
|
559 lemma "(\<exists>x. P x) & |
|
560 (\<forall>x. L x --> ~ (M x & R x)) & |
|
561 (\<forall>x. P x --> (M x & L x)) & |
|
562 ((\<forall>x. P x --> Q x) | (\<exists>x. P x & R x)) |
|
563 --> (\<exists>x. Q x & P x)" |
|
564 by meson |
|
565 |
|
566 text{*Problem 26; has 24 Horn clauses*} |
|
567 lemma "((\<exists>x. p x) = (\<exists>x. q x)) & |
|
568 (\<forall>x. \<forall>y. p x & q y --> (r x = s y)) |
|
569 --> ((\<forall>x. p x --> r x) = (\<forall>x. q x --> s x))" |
|
570 by meson |
|
571 |
|
572 text{*Problem 27; has 13 Horn clauses*} |
|
573 lemma "(\<exists>x. P x & ~Q x) & |
|
574 (\<forall>x. P x --> R x) & |
|
575 (\<forall>x. M x & L x --> P x) & |
|
576 ((\<exists>x. R x & ~ Q x) --> (\<forall>x. L x --> ~ R x)) |
|
577 --> (\<forall>x. M x --> ~L x)" |
|
578 by meson |
|
579 |
|
580 text{*Problem 28. AMENDED; has 14 Horn clauses*} |
|
581 lemma "(\<forall>x. P x --> (\<forall>x. Q x)) & |
|
582 ((\<forall>x. Q x | R x) --> (\<exists>x. Q x & S x)) & |
|
583 ((\<exists>x. S x) --> (\<forall>x. L x --> M x)) |
|
584 --> (\<forall>x. P x & L x --> M x)" |
|
585 by meson |
|
586 |
|
587 text{*Problem 29. Essentially the same as Principia Mathematica |
|
588 *11.71. 62 Horn clauses*} |
|
589 lemma "(\<exists>x. F x) & (\<exists>y. G y) |
|
590 --> ( ((\<forall>x. F x --> H x) & (\<forall>y. G y --> J y)) = |
|
591 (\<forall>x y. F x & G y --> H x & J y))" |
|
592 by meson |
|
593 |
|
594 |
|
595 text{*Problem 30*} |
|
596 lemma "(\<forall>x. P x | Q x --> ~ R x) & (\<forall>x. (Q x --> ~ S x) --> P x & R x) |
|
597 --> (\<forall>x. S x)" |
|
598 by meson |
|
599 |
|
600 text{*Problem 31; has 10 Horn clauses; first negative clauses is useless*} |
|
601 lemma "~(\<exists>x. P x & (Q x | R x)) & |
|
602 (\<exists>x. L x & P x) & |
|
603 (\<forall>x. ~ R x --> M x) |
|
604 --> (\<exists>x. L x & M x)" |
|
605 by meson |
|
606 |
|
607 text{*Problem 32*} |
|
608 lemma "(\<forall>x. P x & (Q x | R x)-->S x) & |
|
609 (\<forall>x. S x & R x --> L x) & |
|
610 (\<forall>x. M x --> R x) |
|
611 --> (\<forall>x. P x & M x --> L x)" |
|
612 by meson |
|
613 |
|
614 text{*Problem 33; has 55 Horn clauses*} |
|
615 lemma "(\<forall>x. P a & (P x --> P b)-->P c) = |
|
616 (\<forall>x. (~P a | P x | P c) & (~P a | ~P b | P c))" |
|
617 by meson |
|
618 |
|
619 text{*Problem 34 AMENDED (TWICE!!); has 924 Horn clauses*} |
|
620 text{*Andrews's challenge*} |
|
621 lemma "((\<exists>x. \<forall>y. p x = p y) = |
|
622 ((\<exists>x. q x) = (\<forall>y. p y))) = |
|
623 ((\<exists>x. \<forall>y. q x = q y) = |
|
624 ((\<exists>x. p x) = (\<forall>y. q y)))" |
|
625 by meson |
|
626 |
|
627 text{*Problem 35*} |
|
628 lemma "\<exists>x y. P x y --> (\<forall>u v. P u v)" |
|
629 by meson |
|
630 |
|
631 text{*Problem 36; has 15 Horn clauses*} |
|
632 lemma "(\<forall>x. \<exists>y. J x y) & |
|
633 (\<forall>x. \<exists>y. G x y) & |
|
634 (\<forall>x y. J x y | G x y --> |
|
635 (\<forall>z. J y z | G y z --> H x z)) |
|
636 --> (\<forall>x. \<exists>y. H x y)" |
|
637 by meson |
|
638 |
|
639 text{*Problem 37; has 10 Horn clauses*} |
|
640 lemma "(\<forall>z. \<exists>w. \<forall>x. \<exists>y. |
|
641 (P x z --> P y w) & P y z & (P y w --> (\<exists>u. Q u w))) & |
|
642 (\<forall>x z. ~P x z --> (\<exists>y. Q y z)) & |
|
643 ((\<exists>x y. Q x y) --> (\<forall>x. R x x)) |
|
644 --> (\<forall>x. \<exists>y. R x y)" |
|
645 by meson --{*causes unification tracing messages*} |
|
646 |
|
647 |
|
648 text{*Problem 38*} text{*Quite hard: 422 Horn clauses!!*} |
|
649 lemma "(\<forall>x. p a & (p x --> (\<exists>y. p y & r x y)) --> |
|
650 (\<exists>z. \<exists>w. p z & r x w & r w z)) = |
|
651 (\<forall>x. (~p a | p x | (\<exists>z. \<exists>w. p z & r x w & r w z)) & |
|
652 (~p a | ~(\<exists>y. p y & r x y) | |
|
653 (\<exists>z. \<exists>w. p z & r x w & r w z)))" |
|
654 by meson |
|
655 |
|
656 text{*Problem 39*} |
|
657 lemma "~ (\<exists>x. \<forall>y. F y x = (~F y y))" |
|
658 by meson |
|
659 |
|
660 text{*Problem 40. AMENDED*} |
|
661 lemma "(\<exists>y. \<forall>x. F x y = F x x) |
|
662 --> ~ (\<forall>x. \<exists>y. \<forall>z. F z y = (~F z x))" |
|
663 by meson |
|
664 |
|
665 text{*Problem 41*} |
|
666 lemma "(\<forall>z. (\<exists>y. (\<forall>x. f x y = (f x z & ~ f x x)))) |
|
667 --> ~ (\<exists>z. \<forall>x. f x z)" |
|
668 by meson |
|
669 |
|
670 text{*Problem 42*} |
|
671 lemma "~ (\<exists>y. \<forall>x. p x y = (~ (\<exists>z. p x z & p z x)))" |
|
672 by meson |
|
673 |
|
674 text{*Problem 43 NOW PROVED AUTOMATICALLY!!*} |
|
675 lemma "(\<forall>x. \<forall>y. q x y = (\<forall>z. p z x = (p z y::bool))) |
|
676 --> (\<forall>x. (\<forall>y. q x y = (q y x::bool)))" |
|
677 by meson |
|
678 |
|
679 text{*Problem 44: 13 Horn clauses; 7-step proof*} |
|
680 lemma "(\<forall>x. f x --> |
|
681 (\<exists>y. g y & h x y & (\<exists>y. g y & ~ h x y))) & |
|
682 (\<exists>x. j x & (\<forall>y. g y --> h x y)) |
|
683 --> (\<exists>x. j x & ~f x)" |
|
684 by meson |
|
685 |
|
686 text{*Problem 45; has 27 Horn clauses; 54-step proof*} |
|
687 lemma "(\<forall>x. f x & (\<forall>y. g y & h x y --> j x y) |
|
688 --> (\<forall>y. g y & h x y --> k y)) & |
|
689 ~ (\<exists>y. l y & k y) & |
|
690 (\<exists>x. f x & (\<forall>y. h x y --> l y) |
|
691 & (\<forall>y. g y & h x y --> j x y)) |
|
692 --> (\<exists>x. f x & ~ (\<exists>y. g y & h x y))" |
|
693 by meson |
|
694 |
|
695 text{*Problem 46; has 26 Horn clauses; 21-step proof*} |
|
696 lemma "(\<forall>x. f x & (\<forall>y. f y & h y x --> g y) --> g x) & |
|
697 ((\<exists>x. f x & ~g x) --> |
|
698 (\<exists>x. f x & ~g x & (\<forall>y. f y & ~g y --> j x y))) & |
|
699 (\<forall>x y. f x & f y & h x y --> ~j y x) |
|
700 --> (\<forall>x. f x --> g x)" |
|
701 by meson |
|
702 |
|
703 text{*Problem 47. Schubert's Steamroller*} |
|
704 text{*26 clauses; 63 Horn clauses |
|
705 87094 inferences so far. Searching to depth 36*} |
|
706 lemma "(\<forall>x. P1 x --> P0 x) & (\<exists>x. P1 x) & |
|
707 (\<forall>x. P2 x --> P0 x) & (\<exists>x. P2 x) & |
|
708 (\<forall>x. P3 x --> P0 x) & (\<exists>x. P3 x) & |
|
709 (\<forall>x. P4 x --> P0 x) & (\<exists>x. P4 x) & |
|
710 (\<forall>x. P5 x --> P0 x) & (\<exists>x. P5 x) & |
|
711 (\<forall>x. Q1 x --> Q0 x) & (\<exists>x. Q1 x) & |
|
712 (\<forall>x. P0 x --> ((\<forall>y. Q0 y-->R x y) | |
|
713 (\<forall>y. P0 y & S y x & |
|
714 (\<exists>z. Q0 z&R y z) --> R x y))) & |
|
715 (\<forall>x y. P3 y & (P5 x|P4 x) --> S x y) & |
|
716 (\<forall>x y. P3 x & P2 y --> S x y) & |
|
717 (\<forall>x y. P2 x & P1 y --> S x y) & |
|
718 (\<forall>x y. P1 x & (P2 y|Q1 y) --> ~R x y) & |
|
719 (\<forall>x y. P3 x & P4 y --> R x y) & |
|
720 (\<forall>x y. P3 x & P5 y --> ~R x y) & |
|
721 (\<forall>x. (P4 x|P5 x) --> (\<exists>y. Q0 y & R x y)) |
|
722 --> (\<exists>x y. P0 x & P0 y & (\<exists>z. Q1 z & R y z & R x y))" |
|
723 by (tactic{*safe_best_meson_tac 1*}) |
|
724 --{*Considerably faster than @{text meson}, |
|
725 which does iterative deepening rather than best-first search*} |
|
726 |
|
727 text{*The Los problem. Circulated by John Harrison*} |
|
728 lemma "(\<forall>x y z. P x y & P y z --> P x z) & |
|
729 (\<forall>x y z. Q x y & Q y z --> Q x z) & |
|
730 (\<forall>x y. P x y --> P y x) & |
|
731 (\<forall>x y. P x y | Q x y) |
|
732 --> (\<forall>x y. P x y) | (\<forall>x y. Q x y)" |
|
733 by meson |
|
734 |
|
735 text{*A similar example, suggested by Johannes Schumann and |
|
736 credited to Pelletier*} |
|
737 lemma "(\<forall>x y z. P x y --> P y z --> P x z) --> |
|
738 (\<forall>x y z. Q x y --> Q y z --> Q x z) --> |
|
739 (\<forall>x y. Q x y --> Q y x) --> (\<forall>x y. P x y | Q x y) --> |
|
740 (\<forall>x y. P x y) | (\<forall>x y. Q x y)" |
|
741 by meson |
|
742 |
|
743 text{*Problem 50. What has this to do with equality?*} |
|
744 lemma "(\<forall>x. P a x | (\<forall>y. P x y)) --> (\<exists>x. \<forall>y. P x y)" |
|
745 by meson |
|
746 |
|
747 text{*Problem 55*} |
|
748 |
|
749 text{*Non-equational version, from Manthey and Bry, CADE-9 (Springer, 1988). |
|
750 @{text meson} cannot report who killed Agatha. *} |
|
751 lemma "lives agatha & lives butler & lives charles & |
|
752 (killed agatha agatha | killed butler agatha | killed charles agatha) & |
|
753 (\<forall>x y. killed x y --> hates x y & ~richer x y) & |
|
754 (\<forall>x. hates agatha x --> ~hates charles x) & |
|
755 (hates agatha agatha & hates agatha charles) & |
|
756 (\<forall>x. lives x & ~richer x agatha --> hates butler x) & |
|
757 (\<forall>x. hates agatha x --> hates butler x) & |
|
758 (\<forall>x. ~hates x agatha | ~hates x butler | ~hates x charles) --> |
|
759 (\<exists>x. killed x agatha)" |
|
760 by meson |
|
761 |
|
762 text{*Problem 57*} |
|
763 lemma "P (f a b) (f b c) & P (f b c) (f a c) & |
|
764 (\<forall>x y z. P x y & P y z --> P x z) --> P (f a b) (f a c)" |
|
765 by meson |
|
766 |
|
767 text{*Problem 58*} |
|
768 text{* Challenge found on info-hol *} |
|
769 lemma "\<forall>P Q R x. \<exists>v w. \<forall>y z. P x & Q y --> (P v | R w) & (R z --> Q v)" |
|
770 by meson |
|
771 |
|
772 text{*Problem 59*} |
|
773 lemma "(\<forall>x. P x = (~P(f x))) --> (\<exists>x. P x & ~P(f x))" |
|
774 by meson |
|
775 |
|
776 text{*Problem 60*} |
|
777 lemma "\<forall>x. P x (f x) = (\<exists>y. (\<forall>z. P z y --> P z (f x)) & P x y)" |
|
778 by meson |
|
779 |
|
780 text{*Problem 62 as corrected in JAR 18 (1997), page 135*} |
|
781 lemma "(\<forall>x. p a & (p x --> p(f x)) --> p(f(f x))) = |
|
782 (\<forall>x. (~ p a | p x | p(f(f x))) & |
|
783 (~ p a | ~ p(f x) | p(f(f x))))" |
|
784 by meson |
|
785 |
|
786 end |