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