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