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