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