Theory Classical

(*  Title:      HOL/ex/Classical.thy
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    Copyright   1994  University of Cambridge
*)

section‹Classical Predicate Calculus Problems›

theory Classical imports Main begin

subsection‹Traditional Classical Reasoner›

text‹The machine "griffon" mentioned below is a 2.5GHz Power Mac G5.›

text‹Taken from ‹FOL/Classical.thy›. When porting examples from
first-order logic, beware of the precedence of ‹=› versus ‹↔›.›

lemma "(P ⟶ Q ∨ R) ⟶ (P⟶Q) ∨ (P⟶R)"
by blast

text‹If and only if›

lemma "(P=Q) = (Q = (P::bool))"
by blast

lemma "¬ (P = (¬P))"
by blast


text‹Sample problems from
  F. J. Pelletier,
  Seventy-Five Problems for Testing Automatic Theorem Provers,
  J. Automated Reasoning 2 (1986), 191-216.
  Errata, JAR 4 (1988), 236-236.

The hardest problems -- judging by experience with several theorem provers,
including matrix ones -- are 34 and 43.
›

subsubsection‹Pelletier's examples›

text‹1›
lemma "(P⟶Q)  =  (¬Q ⟶ ¬P)"
by blast

text‹2›
lemma "(¬ ¬ P) =  P"
by blast

text‹3›
lemma "¬(P⟶Q) ⟶ (Q⟶P)"
by blast

text‹4›
lemma "(¬P⟶Q)  =  (¬Q ⟶ P)"
by blast

text‹5›
lemma "((P∨Q)⟶(P∨R)) ⟶ (P∨(Q⟶R))"
by blast

text‹6›
lemma "P ∨ ¬ P"
by blast

text‹7›
lemma "P ∨ ¬ ¬ ¬ P"
by blast

text‹8.  Peirce's law›
lemma "((P⟶Q) ⟶ P)  ⟶  P"
by blast

text‹9›
lemma "((P∨Q) ∧ (¬P∨Q) ∧ (P∨ ¬Q)) ⟶ ¬ (¬P ∨ ¬Q)"
by blast

text‹10›
lemma "(Q⟶R) ∧ (R⟶P∧Q) ∧ (P⟶Q∨R) ⟶ (P=Q)"
by blast

text‹11.  Proved in each direction (incorrectly, says Pelletier!!)›
lemma "P=(P::bool)"
by blast

text‹12.  "Dijkstra's law"›
lemma "((P = Q) = R) = (P = (Q = R))"
by blast

text‹13.  Distributive law›
lemma "(P ∨ (Q ∧ R)) = ((P ∨ Q) ∧ (P ∨ R))"
by blast

text‹14›
lemma "(P = Q) = ((Q ∨ ¬P) ∧ (¬Q∨P))"
by blast

text‹15›
lemma "(P ⟶ Q) = (¬P ∨ Q)"
by blast

text‹16›
lemma "(P⟶Q) ∨ (Q⟶P)"
by blast

text‹17›
lemma "((P ∧ (Q⟶R))⟶S)  =  ((¬P ∨ Q ∨ S) ∧ (¬P ∨ ¬R ∨ S))"
by blast

subsubsection‹Classical Logic: examples with quantifiers›

lemma "(∀x. P(x) ∧ Q(x)) = ((∀x. P(x)) ∧ (∀x. Q(x)))"
by blast

lemma "(∃x. P⟶Q(x))  =  (P ⟶ (∃x. Q(x)))"
by blast

lemma "(∃x. P(x)⟶Q) = ((∀x. P(x)) ⟶ Q)"
by blast

lemma "((∀x. P(x)) ∨ Q)  =  (∀x. P(x) ∨ Q)"
by blast

text‹From Wishnu Prasetya›
lemma "(∀x. Q(x) ⟶ R(x)) ∧ ¬R(a) ∧ (∀x. ¬R(x) ∧ ¬Q(x) ⟶ P(b) ∨ Q(b))
    ⟶ P(b) ∨ R(b)"
by blast


subsubsection‹Problems requiring quantifier duplication›

text‹Theorem B of Peter Andrews, Theorem Proving via General Matings,
  JACM 28 (1981).›
lemma "(∃x. ∀y. P(x) = P(y)) ⟶ ((∃x. P(x)) = (∀y. P(y)))"
by blast

text‹Needs multiple instantiation of the quantifier.›
lemma "(∀x. P(x)⟶P(f(x)))  ∧  P(d)⟶P(f(f(f(d))))"
by blast

text‹Needs double instantiation of the quantifier›
lemma "∃x. P(x) ⟶ P(a) ∧ P(b)"
by blast

lemma "∃z. P(z) ⟶ (∀x. P(x))"
by blast

lemma "∃x. (∃y. P(y)) ⟶ P(x)"
by blast

subsubsection‹Hard examples with quantifiers›

text‹Problem 18›
lemma "∃y. ∀x. P(y)⟶P(x)"
by blast

text‹Problem 19›
lemma "∃x. ∀y z. (P(y)⟶Q(z)) ⟶ (P(x)⟶Q(x))"
by blast

text‹Problem 20›
lemma "(∀x y. ∃z. ∀w. (P(x)∧Q(y)⟶R(z)∧S(w)))
    ⟶ (∃x y. P(x) ∧ Q(y)) ⟶ (∃z. R(z))"
by blast

text‹Problem 21›
lemma "(∃x. P⟶Q(x)) ∧ (∃x. Q(x)⟶P) ⟶ (∃x. P=Q(x))"
by blast

text‹Problem 22›
lemma "(∀x. P = Q(x))  ⟶  (P = (∀x. Q(x)))"
by blast

text‹Problem 23›
lemma "(∀x. P ∨ Q(x))  =  (P ∨ (∀x. Q(x)))"
by blast

text‹Problem 24›
lemma "¬(∃x. S(x)∧Q(x)) ∧ (∀x. P(x) ⟶ Q(x)∨R(x)) ∧
     (¬(∃x. P(x)) ⟶ (∃x. Q(x))) ∧ (∀x. Q(x)∨R(x) ⟶ S(x))
    ⟶ (∃x. P(x)∧R(x))"
by blast

text‹Problem 25›
lemma "(∃x. P(x)) ∧
        (∀x. L(x) ⟶ ¬ (M(x) ∧ R(x))) ∧
        (∀x. P(x) ⟶ (M(x) ∧ L(x))) ∧
        ((∀x. P(x)⟶Q(x)) ∨ (∃x. P(x)∧R(x)))
    ⟶ (∃x. Q(x)∧P(x))"
by blast

text‹Problem 26›
lemma "((∃x. p(x)) = (∃x. q(x))) ∧
      (∀x. ∀y. p(x) ∧ q(y) ⟶ (r(x) = s(y)))
  ⟶ ((∀x. p(x)⟶r(x)) = (∀x. q(x)⟶s(x)))"
by blast

text‹Problem 27›
lemma "(∃x. P(x) ∧ ¬Q(x)) ∧
              (∀x. P(x) ⟶ R(x)) ∧
              (∀x. M(x) ∧ L(x) ⟶ P(x)) ∧
              ((∃x. R(x) ∧ ¬ Q(x)) ⟶ (∀x. L(x) ⟶ ¬ R(x)))
          ⟶ (∀x. M(x) ⟶ ¬L(x))"
by blast

text‹Problem 28.  AMENDED›
lemma "(∀x. P(x) ⟶ (∀x. Q(x))) ∧
        ((∀x. Q(x)∨R(x)) ⟶ (∃x. Q(x)∧S(x))) ∧
        ((∃x. S(x)) ⟶ (∀x. L(x) ⟶ M(x)))
    ⟶ (∀x. P(x) ∧ L(x) ⟶ M(x))"
by blast

text‹Problem 29.  Essentially the same as Principia Mathematica *11.71›
lemma "(∃x. F(x)) ∧ (∃y. G(y))
    ⟶ ( ((∀x. F(x)⟶H(x)) ∧ (∀y. G(y)⟶J(y)))  =
          (∀x y. F(x) ∧ G(y) ⟶ H(x) ∧ J(y)))"
by blast

text‹Problem 30›
lemma "(∀x. P(x) ∨ Q(x) ⟶ ¬ R(x)) ∧
        (∀x. (Q(x) ⟶ ¬ S(x)) ⟶ P(x) ∧ R(x))
    ⟶ (∀x. S(x))"
by blast

text‹Problem 31›
lemma "¬(∃x. P(x) ∧ (Q(x) ∨ R(x))) ∧
        (∃x. L(x) ∧ P(x)) ∧
        (∀x. ¬ R(x) ⟶ M(x))
    ⟶ (∃x. L(x) ∧ M(x))"
by blast

text‹Problem 32›
lemma "(∀x. P(x) ∧ (Q(x)∨R(x))⟶S(x)) ∧
        (∀x. S(x) ∧ R(x) ⟶ L(x)) ∧
        (∀x. M(x) ⟶ R(x))
    ⟶ (∀x. P(x) ∧ M(x) ⟶ L(x))"
by blast

text‹Problem 33›
lemma "(∀x. P(a) ∧ (P(x)⟶P(b))⟶P(c))  =
     (∀x. (¬P(a) ∨ P(x) ∨ P(c)) ∧ (¬P(a) ∨ ¬P(b) ∨ P(c)))"
by blast

text‹Problem 34  AMENDED (TWICE!!)›
text‹Andrews's challenge›
lemma "((∃x. ∀y. p(x) = p(y))  =
               ((∃x. q(x)) = (∀y. p(y))))   =
              ((∃x. ∀y. q(x) = q(y))  =
               ((∃x. p(x)) = (∀y. q(y))))"
by blast

text‹Problem 35›
lemma "∃x y. P x y ⟶  (∀u v. P u v)"
by blast

text‹Problem 36›
lemma "(∀x. ∃y. J x y) ∧
        (∀x. ∃y. G x y) ∧
        (∀x y. J x y ∨ G x y ⟶
        (∀z. J y z ∨ G y z ⟶ H x z))
    ⟶ (∀x. ∃y. H x y)"
by blast

text‹Problem 37›
lemma "(∀z. ∃w. ∀x. ∃y.
           (P x z ⟶P y w) ∧ P y z ∧ (P y w ⟶ (∃u. Q u w))) ∧
        (∀x z. ¬(P x z) ⟶ (∃y. Q y z)) ∧
        ((∃x y. Q x y) ⟶ (∀x. R x x))
    ⟶ (∀x. ∃y. R x y)"
by blast

text‹Problem 38›
lemma "(∀x. p(a) ∧ (p(x) ⟶ (∃y. p(y) ∧ r x y)) ⟶
           (∃z. ∃w. p(z) ∧ r x w ∧ r w z))  =
     (∀x. (¬p(a) ∨ p(x) ∨ (∃z. ∃w. p(z) ∧ r x w ∧ r w z)) ∧
           (¬p(a) ∨ ¬(∃y. p(y) ∧ r x y) ∨
            (∃z. ∃w. p(z) ∧ r x w ∧ r w z)))"
by blast (*beats fast!*)

text‹Problem 39›
lemma "¬ (∃x. ∀y. F y x = (¬ F y y))"
by blast

text‹Problem 40.  AMENDED›
lemma "(∃y. ∀x. F x y = F x x)
        ⟶  ¬ (∀x. ∃y. ∀z. F z y = (¬ F z x))"
by blast

text‹Problem 41›
lemma "(∀z. ∃y. ∀x. f x y = (f x z ∧ ¬ f x x))
               ⟶ ¬ (∃z. ∀x. f x z)"
by blast

text‹Problem 42›
lemma "¬ (∃y. ∀x. p x y = (¬ (∃z. p x z ∧ p z x)))"
by blast

text‹Problem 43!!›
lemma "(∀x::'a. ∀y::'a. q x y = (∀z. p z x ⟷ (p z y)))
  ⟶ (∀x. (∀y. q x y ⟷ (q y x)))"
by blast

text‹Problem 44›
lemma "(∀x. f(x) ⟶
              (∃y. g(y) ∧ h x y ∧ (∃y. g(y) ∧ ¬ h x y)))  ∧
              (∃x. j(x) ∧ (∀y. g(y) ⟶ h x y))
              ⟶ (∃x. j(x) ∧ ¬f(x))"
by blast

text‹Problem 45›
lemma "(∀x. f(x) ∧ (∀y. g(y) ∧ h x y ⟶ j x y)
                      ⟶ (∀y. g(y) ∧ h x y ⟶ k(y))) ∧
     ¬ (∃y. l(y) ∧ k(y)) ∧
     (∃x. f(x) ∧ (∀y. h x y ⟶ l(y))
                ∧ (∀y. g(y) ∧ h x y ⟶ j x y))
      ⟶ (∃x. f(x) ∧ ¬ (∃y. g(y) ∧ h x y))"
by blast


subsubsection‹Problems (mainly) involving equality or functions›

text‹Problem 48›
lemma "(a=b ∨ c=d) ∧ (a=c ∨ b=d) ⟶ a=d ∨ b=c"
by blast

text‹Problem 49  NOT PROVED AUTOMATICALLY.
     Hard because it involves substitution for Vars
  the type constraint ensures that x,y,z have the same type as a,b,u.›
lemma "(∃x y::'a. ∀z. z=x ∨ z=y) ∧ P(a) ∧ P(b) ∧ (¬a=b)
                ⟶ (∀u::'a. P(u))"
by metis

text‹Problem 50.  (What has this to do with equality?)›
lemma "(∀x. P a x ∨ (∀y. P x y)) ⟶ (∃x. ∀y. P x y)"
by blast

text‹Problem 51›
lemma "(∃z w. ∀x y. P x y = (x=z ∧ y=w)) ⟶
     (∃z. ∀x. ∃w. (∀y. P x y = (y=w)) = (x=z))"
by blast

text‹Problem 52. Almost the same as 51.›
lemma "(∃z w. ∀x y. P x y = (x=z ∧ y=w)) ⟶
     (∃w. ∀y. ∃z. (∀x. P x y = (x=z)) = (y=w))"
by blast

text‹Problem 55›

text‹Non-equational version, from Manthey and Bry, CADE-9 (Springer, 1988).
  fast DISCOVERS who killed Agatha.›
schematic_goal "lives(agatha) ∧ lives(butler) ∧ lives(charles) ∧
   (killed agatha agatha ∨ killed butler agatha ∨ killed charles agatha) ∧
   (∀x y. killed x y ⟶ hates x y ∧ ¬richer x y) ∧
   (∀x. hates agatha x ⟶ ¬hates charles x) ∧
   (hates agatha agatha ∧ hates agatha charles) ∧
   (∀x. lives(x) ∧ ¬richer x agatha ⟶ hates butler x) ∧
   (∀x. hates agatha x ⟶ hates butler x) ∧
   (∀x. ¬hates x agatha ∨ ¬hates x butler ∨ ¬hates x charles) ⟶
    killed ?who agatha"
by fast

text‹Problem 56›
lemma "(∀x. (∃y. P(y) ∧ x=f(y)) ⟶ P(x)) = (∀x. P(x) ⟶ P(f(x)))"
by blast

text‹Problem 57›
lemma "P (f a b) (f b c) ∧ P (f b c) (f a c) ∧
     (∀x y z. P x y ∧ P y z ⟶ P x z)    ⟶   P (f a b) (f a c)"
by blast

text‹Problem 58  NOT PROVED AUTOMATICALLY›
lemma "(∀x y. f(x)=g(y)) ⟶ (∀x y. f(f(x))=f(g(y)))"
by (fast intro: arg_cong [of concl: f])

text‹Problem 59›
lemma "(∀x. P(x) = (¬P(f(x)))) ⟶ (∃x. P(x) ∧ ¬P(f(x)))"
by blast

text‹Problem 60›
lemma "∀x. P x (f x) = (∃y. (∀z. P z y ⟶ P z (f x)) ∧ P x y)"
by blast

text‹Problem 62 as corrected in JAR 18 (1997), page 135›
lemma "(∀x. p a ∧ (p x ⟶ p(f x)) ⟶ p(f(f x)))  =
      (∀x. (¬ p a ∨ p x ∨ p(f(f x))) ∧
              (¬ p a ∨ ¬ p(f x) ∨ p(f(f x))))"
by blast

text‹From Davis, Obvious Logical Inferences, IJCAI-81, 530-531
  fast indeed copes!›
lemma "(∀x. F(x) ∧ ¬G(x) ⟶ (∃y. H(x,y) ∧ J(y))) ∧
       (∃x. K(x) ∧ F(x) ∧ (∀y. H(x,y) ⟶ K(y))) ∧
       (∀x. K(x) ⟶ ¬G(x))  ⟶  (∃x. K(x) ∧ J(x))"
by fast

text‹From Rudnicki, Obvious Inferences, JAR 3 (1987), 383-393.
  It does seem obvious!›
lemma "(∀x. F(x) ∧ ¬G(x) ⟶ (∃y. H(x,y) ∧ J(y))) ∧
       (∃x. K(x) ∧ F(x) ∧ (∀y. H(x,y) ⟶ K(y)))  ∧
       (∀x. K(x) ⟶ ¬G(x))   ⟶   (∃x. K(x) ⟶ ¬G(x))"
by fast

text‹Attributed to Lewis Carroll by S. G. Pulman.  The first or last
assumption can be deleted.›
lemma "(∀x. honest(x) ∧ industrious(x) ⟶ healthy(x)) ∧
      ¬ (∃x. grocer(x) ∧ healthy(x)) ∧
      (∀x. industrious(x) ∧ grocer(x) ⟶ honest(x)) ∧
      (∀x. cyclist(x) ⟶ industrious(x)) ∧
      (∀x. ¬healthy(x) ∧ cyclist(x) ⟶ ¬honest(x))
      ⟶ (∀x. grocer(x) ⟶ ¬cyclist(x))"
by blast

lemma "(∀x y. R(x,y) ∨ R(y,x)) ∧
       (∀x y. S(x,y) ∧ S(y,x) ⟶ x=y) ∧
       (∀x y. R(x,y) ⟶ S(x,y))    ⟶   (∀x y. S(x,y) ⟶ R(x,y))"
by blast


subsection‹Model Elimination Prover›


text‹Trying out meson with arguments›
lemma "x < y ∧ y < z ⟶ ¬ (z < (x::nat))"
by (meson order_less_irrefl order_less_trans)

text‹The "small example" from Bezem, Hendriks and de Nivelle,
Automatic Proof Construction in Type Theory Using Resolution,
JAR 29: 3-4 (2002), pages 253-275›
lemma "(∀x y z. R(x,y) ∧ R(y,z) ⟶ R(x,z)) ∧
       (∀x. ∃y. R(x,y)) ⟶
       ¬ (∀x. P x = (∀y. R(x,y) ⟶ ¬ P y))"
by (tactic‹Meson.safe_best_meson_tac \<^context> 1›)
    ― ‹In contrast, ‹meson› is SLOW: 7.6s on griffon›


subsubsection‹Pelletier's examples›
text‹1›
lemma "(P ⟶ Q)  =  (¬Q ⟶ ¬P)"
by blast

text‹2›
lemma "(¬ ¬ P) =  P"
by blast

text‹3›
lemma "¬(P⟶Q) ⟶ (Q⟶P)"
by blast

text‹4›
lemma "(¬P⟶Q)  =  (¬Q ⟶ P)"
by blast

text‹5›
lemma "((P∨Q)⟶(P∨R)) ⟶ (P∨(Q⟶R))"
by blast

text‹6›
lemma "P ∨ ¬ P"
by blast

text‹7›
lemma "P ∨ ¬ ¬ ¬ P"
by blast

text‹8.  Peirce's law›
lemma "((P⟶Q) ⟶ P)  ⟶  P"
by blast

text‹9›
lemma "((P∨Q) ∧ (¬P∨Q) ∧ (P∨ ¬Q)) ⟶ ¬ (¬P ∨ ¬Q)"
by blast

text‹10›
lemma "(Q⟶R) ∧ (R⟶P∧Q) ∧ (P⟶Q∨R) ⟶ (P=Q)"
by blast

text‹11.  Proved in each direction (incorrectly, says Pelletier!!)›
lemma "P=(P::bool)"
by blast

text‹12.  "Dijkstra's law"›
lemma "((P = Q) = R) = (P = (Q = R))"
by blast

text‹13.  Distributive law›
lemma "(P ∨ (Q ∧ R)) = ((P ∨ Q) ∧ (P ∨ R))"
by blast

text‹14›
lemma "(P = Q) = ((Q ∨ ¬P) ∧ (¬Q∨P))"
by blast

text‹15›
lemma "(P ⟶ Q) = (¬P ∨ Q)"
by blast

text‹16›
lemma "(P⟶Q) ∨ (Q⟶P)"
by blast

text‹17›
lemma "((P ∧ (Q⟶R))⟶S)  =  ((¬P ∨ Q ∨ S) ∧ (¬P ∨ ¬R ∨ S))"
by blast

subsubsection‹Classical Logic: examples with quantifiers›

lemma "(∀x. P x ∧ Q x) = ((∀x. P x) ∧ (∀x. Q x))"
by blast

lemma "(∃x. P ⟶ Q x)  =  (P ⟶ (∃x. Q x))"
by blast

lemma "(∃x. P x ⟶ Q) = ((∀x. P x) ⟶ Q)"
by blast

lemma "((∀x. P x) ∨ Q)  =  (∀x. P x ∨ Q)"
by blast

lemma "(∀x. P x ⟶ P(f x))  ∧  P d ⟶ P(f(f(f d)))"
by blast

text‹Needs double instantiation of EXISTS›
lemma "∃x. P x ⟶ P a ∧ P b"
by blast

lemma "∃z. P z ⟶ (∀x. P x)"
by blast

text‹From a paper by Claire Quigley›
lemma "∃y. ((P c ∧ Q y) ∨ (∃z. ¬ Q z)) ∨ (∃x. ¬ P x ∧ Q d)"
by fast

subsubsection‹Hard examples with quantifiers›

text‹Problem 18›
lemma "∃y. ∀x. P y ⟶ P x"
by blast

text‹Problem 19›
lemma "∃x. ∀y z. (P y ⟶ Q z) ⟶ (P x ⟶ Q x)"
by blast

text‹Problem 20›
lemma "(∀x y. ∃z. ∀w. (P x ∧ Q y ⟶ R z ∧ S w))
    ⟶ (∃x y. P x ∧ Q y) ⟶ (∃z. R z)"
by blast

text‹Problem 21›
lemma "(∃x. P ⟶ Q x) ∧ (∃x. Q x ⟶ P) ⟶ (∃x. P=Q x)"
by blast

text‹Problem 22›
lemma "(∀x. P = Q x)  ⟶  (P = (∀x. Q x))"
by blast

text‹Problem 23›
lemma "(∀x. P ∨ Q x)  =  (P ∨ (∀x. Q x))"
by blast

text‹Problem 24›  (*The first goal clause is useless*)
lemma "¬(∃x. S x ∧ Q x) ∧ (∀x. P x ⟶ Q x ∨ R x) ∧
      (¬(∃x. P x) ⟶ (∃x. Q x)) ∧ (∀x. Q x ∨ R x ⟶ S x)
    ⟶ (∃x. P x ∧ R x)"
by blast

text‹Problem 25›
lemma "(∃x. P x) ∧
      (∀x. L x ⟶ ¬ (M x ∧ R x)) ∧
      (∀x. P x ⟶ (M x ∧ L x)) ∧
      ((∀x. P x ⟶ Q x) ∨ (∃x. P x ∧ R x))
    ⟶ (∃x. Q x ∧ P x)"
by blast

text‹Problem 26; has 24 Horn clauses›
lemma "((∃x. p x) = (∃x. q x)) ∧
      (∀x. ∀y. p x ∧ q y ⟶ (r x = s y))
  ⟶ ((∀x. p x ⟶ r x) = (∀x. q x ⟶ s x))"
by blast

text‹Problem 27; has 13 Horn clauses›
lemma "(∃x. P x ∧ ¬Q x) ∧
      (∀x. P x ⟶ R x) ∧
      (∀x. M x ∧ L x ⟶ P x) ∧
      ((∃x. R x ∧ ¬ Q x) ⟶ (∀x. L x ⟶ ¬ R x))
      ⟶ (∀x. M x ⟶ ¬L x)"
by blast

text‹Problem 28.  AMENDED; has 14 Horn clauses›
lemma "(∀x. P x ⟶ (∀x. Q x)) ∧
      ((∀x. Q x ∨ R x) ⟶ (∃x. Q x ∧ S x)) ∧
      ((∃x. S x) ⟶ (∀x. L x ⟶ M x))
    ⟶ (∀x. P x ∧ L x ⟶ M x)"
by blast

text‹Problem 29.  Essentially the same as Principia Mathematica *11.71.
      62 Horn clauses›
lemma "(∃x. F x) ∧ (∃y. G y)
    ⟶ ( ((∀x. F x ⟶ H x) ∧ (∀y. G y ⟶ J y))  =
          (∀x y. F x ∧ G y ⟶ H x ∧ J y))"
by blast


text‹Problem 30›
lemma "(∀x. P x ∨ Q x ⟶ ¬ R x) ∧ (∀x. (Q x ⟶ ¬ S x) ⟶ P x ∧ R x)
       ⟶ (∀x. S x)"
by blast

text‹Problem 31; has 10 Horn clauses; first negative clauses is useless›
lemma "¬(∃x. P x ∧ (Q x ∨ R x)) ∧
      (∃x. L x ∧ P x) ∧
      (∀x. ¬ R x ⟶ M x)
    ⟶ (∃x. L x ∧ M x)"
by blast

text‹Problem 32›
lemma "(∀x. P x ∧ (Q x ∨ R x)⟶S x) ∧
      (∀x. S x ∧ R x ⟶ L x) ∧
      (∀x. M x ⟶ R x)
    ⟶ (∀x. P x ∧ M x ⟶ L x)"
by blast

text‹Problem 33; has 55 Horn clauses›
lemma "(∀x. P a ∧ (P x ⟶ P b)⟶P c)  =
      (∀x. (¬P a ∨ P x ∨ P c) ∧ (¬P a ∨ ¬P b ∨ P c))"
by blast

text‹Problem 34: Andrews's challenge has 924 Horn clauses›
lemma "((∃x. ∀y. p x = p y)  = ((∃x. q x) = (∀y. p y)))     =
      ((∃x. ∀y. q x = q y)  = ((∃x. p x) = (∀y. q y)))"
by blast

text‹Problem 35›
lemma "∃x y. P x y ⟶  (∀u v. P u v)"
by blast

text‹Problem 36; has 15 Horn clauses›
lemma "(∀x. ∃y. J x y) ∧ (∀x. ∃y. G x y) ∧
       (∀x y. J x y ∨ G x y ⟶ (∀z. J y z ∨ G y z ⟶ H x z))
       ⟶ (∀x. ∃y. H x y)"
by blast

text‹Problem 37; has 10 Horn clauses›
lemma "(∀z. ∃w. ∀x. ∃y.
           (P x z ⟶ P y w) ∧ P y z ∧ (P y w ⟶ (∃u. Q u w))) ∧
      (∀x z. ¬P x z ⟶ (∃y. Q y z)) ∧
      ((∃x y. Q x y) ⟶ (∀x. R x x))
    ⟶ (∀x. ∃y. R x y)"
by blast ― ‹causes unification tracing messages›


text‹Problem 38›  text‹Quite hard: 422 Horn clauses!!›
lemma "(∀x. p a ∧ (p x ⟶ (∃y. p y ∧ r x y)) ⟶
           (∃z. ∃w. p z ∧ r x w ∧ r w z))  =
      (∀x. (¬p a ∨ p x ∨ (∃z. ∃w. p z ∧ r x w ∧ r w z)) ∧
            (¬p a ∨ ¬(∃y. p y ∧ r x y) ∨
             (∃z. ∃w. p z ∧ r x w ∧ r w z)))"
by blast

text‹Problem 39›
lemma "¬ (∃x. ∀y. F y x = (¬F y y))"
by blast

text‹Problem 40.  AMENDED›
lemma "(∃y. ∀x. F x y = F x x)
      ⟶  ¬ (∀x. ∃y. ∀z. F z y = (¬F z x))"
by blast

text‹Problem 41›
lemma "(∀z. (∃y. (∀x. f x y = (f x z ∧ ¬ f x x))))
      ⟶ ¬ (∃z. ∀x. f x z)"
by blast

text‹Problem 42›
lemma "¬ (∃y. ∀x. p x y = (¬ (∃z. p x z ∧ p z x)))"
by blast

text‹Problem 43  NOW PROVED AUTOMATICALLY!!›
lemma "(∀x. ∀y. q x y = (∀z. p z x = (p z y::bool)))
      ⟶ (∀x. (∀y. q x y = (q y x::bool)))"
by blast

text‹Problem 44: 13 Horn clauses; 7-step proof›
lemma "(∀x. f x ⟶ (∃y. g y ∧ h x y ∧ (∃y. g y ∧ ¬ h x y)))  ∧
       (∃x. j x ∧ (∀y. g y ⟶ h x y))
       ⟶ (∃x. j x ∧ ¬f x)"
by blast

text‹Problem 45; has 27 Horn clauses; 54-step proof›
lemma "(∀x. f x ∧ (∀y. g y ∧ h x y ⟶ j x y)
            ⟶ (∀y. g y ∧ h x y ⟶ k y)) ∧
      ¬ (∃y. l y ∧ k y) ∧
      (∃x. f x ∧ (∀y. h x y ⟶ l y)
                ∧ (∀y. g y ∧ h x y ⟶ j x y))
      ⟶ (∃x. f x ∧ ¬ (∃y. g y ∧ h x y))"
by blast

text‹Problem 46; has 26 Horn clauses; 21-step proof›
lemma "(∀x. f x ∧ (∀y. f y ∧ h y x ⟶ g y) ⟶ g x) ∧
       ((∃x. f x ∧ ¬g x) ⟶
       (∃x. f x ∧ ¬g x ∧ (∀y. f y ∧ ¬g y ⟶ j x y))) ∧
       (∀x y. f x ∧ f y ∧ h x y ⟶ ¬j y x)
       ⟶ (∀x. f x ⟶ g x)"
by blast

text‹Problem 47.  Schubert's Steamroller.
      26 clauses; 63 Horn clauses.
      87094 inferences so far.  Searching to depth 36›
lemma "(∀x. wolf x ⟶ animal x) ∧ (∃x. wolf x) ∧
       (∀x. fox x ⟶ animal x) ∧ (∃x. fox x) ∧
       (∀x. bird x ⟶ animal x) ∧ (∃x. bird x) ∧
       (∀x. caterpillar x ⟶ animal x) ∧ (∃x. caterpillar x) ∧
       (∀x. snail x ⟶ animal x) ∧ (∃x. snail x) ∧
       (∀x. grain x ⟶ plant x) ∧ (∃x. grain x) ∧
       (∀x. animal x ⟶
             ((∀y. plant y ⟶ eats x y)  ∨ 
              (∀y. animal y ∧ smaller_than y x ∧
                    (∃z. plant z ∧ eats y z) ⟶ eats x y))) ∧
       (∀x y. bird y ∧ (snail x ∨ caterpillar x) ⟶ smaller_than x y) ∧
       (∀x y. bird x ∧ fox y ⟶ smaller_than x y) ∧
       (∀x y. fox x ∧ wolf y ⟶ smaller_than x y) ∧
       (∀x y. wolf x ∧ (fox y ∨ grain y) ⟶ ¬eats x y) ∧
       (∀x y. bird x ∧ caterpillar y ⟶ eats x y) ∧
       (∀x y. bird x ∧ snail y ⟶ ¬eats x y) ∧
       (∀x. (caterpillar x ∨ snail x) ⟶ (∃y. plant y ∧ eats x y))
       ⟶ (∃x y. animal x ∧ animal y ∧ (∃z. grain z ∧ eats y z ∧ eats x y))"
by (tactic‹Meson.safe_best_meson_tac \<^context> 1›)
    ― ‹Nearly twice as fast as ‹meson›,
        which performs iterative deepening rather than best-first search›

text‹The Los problem. Circulated by John Harrison›
lemma "(∀x y z. P x y ∧ P y z ⟶ P x z) ∧
       (∀x y z. Q x y ∧ Q y z ⟶ Q x z) ∧
       (∀x y. P x y ⟶ P y x) ∧
       (∀x y. P x y ∨ Q x y)
       ⟶ (∀x y. P x y) ∨ (∀x y. Q x y)"
by meson

text‹A similar example, suggested by Johannes Schumann and
 credited to Pelletier›
lemma "(∀x y z. P x y ⟶ P y z ⟶ P x z) ⟶
       (∀x y z. Q x y ⟶ Q y z ⟶ Q x z) ⟶
       (∀x y. Q x y ⟶ Q y x) ⟶  (∀x y. P x y ∨ Q x y) ⟶
       (∀x y. P x y) ∨ (∀x y. Q x y)"
by meson

text‹Problem 50.  What has this to do with equality?›
lemma "(∀x. P a x ∨ (∀y. P x y)) ⟶ (∃x. ∀y. P x y)"
by blast

text‹Problem 54: NOT PROVED›
lemma "(∀y::'a. ∃z. ∀x. F x z = (x=y)) ⟶
      ¬ (∃w. ∀x. F x w = (∀u. F x u ⟶ (∃y. F y u ∧ ¬ (∃z. F z u ∧ F z y))))"
oops 


text‹Problem 55›

text‹Non-equational version, from Manthey and Bry, CADE-9 (Springer, 1988).
  ‹meson› cannot report who killed Agatha.›
lemma "lives agatha ∧ lives butler ∧ lives charles ∧
       (killed agatha agatha ∨ killed butler agatha ∨ killed charles agatha) ∧
       (∀x y. killed x y ⟶ hates x y ∧ ¬richer x y) ∧
       (∀x. hates agatha x ⟶ ¬hates charles x) ∧
       (hates agatha agatha ∧ hates agatha charles) ∧
       (∀x. lives x ∧ ¬richer x agatha ⟶ hates butler x) ∧
       (∀x. hates agatha x ⟶ hates butler x) ∧
       (∀x. ¬hates x agatha ∨ ¬hates x butler ∨ ¬hates x charles) ⟶
       (∃x. killed x agatha)"
by meson

text‹Problem 57›
lemma "P (f a b) (f b c) ∧ P (f b c) (f a c) ∧
      (∀x y z. P x y ∧ P y z ⟶ P x z)    ⟶   P (f a b) (f a c)"
by blast

text‹Problem 58: Challenge found on info-hol›
lemma "∀P Q R x. ∃v w. ∀y z. P x ∧ Q y ⟶ (P v ∨ R w) ∧ (R z ⟶ Q v)"
by blast

text‹Problem 59›
lemma "(∀x. P x = (¬P(f x))) ⟶ (∃x. P x ∧ ¬P(f x))"
by blast

text‹Problem 60›
lemma "∀x. P x (f x) = (∃y. (∀z. P z y ⟶ P z (f x)) ∧ P x y)"
by blast

text‹Problem 62 as corrected in JAR 18 (1997), page 135›
lemma "(∀x. p a ∧ (p x ⟶ p(f x)) ⟶ p(f(f x)))  =
       (∀x. (¬ p a ∨ p x ∨ p(f(f x))) ∧
            (¬ p a ∨ ¬ p(f x) ∨ p(f(f x))))"
by blast

text‹Charles Morgan's problems›
context
  fixes T i n
  assumes a: "∀x y. T(i x(i y x))"
    and b: "∀x y z. T(i (i x (i y z)) (i (i x y) (i x z)))"
    and c: "∀x y. T(i (i (n x) (n y)) (i y x))"
    and c': "∀x y. T(i (i y x) (i (n x) (n y)))"
    and d: "∀x y. T(i x y) ∧ T x ⟶ T y"
begin

lemma "∀x. T(i x x)"
  using a b d by blast

lemma "∀x. T(i x (n(n x)))" ― ‹Problem 66›
  using a b c d by metis

lemma "∀x. T(i (n(n x)) x)" ― ‹Problem 67›
  using a b c d by meson ― ‹4.9s on griffon. 51061 inferences, depth 21›

lemma "∀x. T(i x (n(n x)))" ― ‹Problem 68: not proved.  Listed as satisfiable in TPTP (LCL078-1)›
  using a b c' d oops

end

text‹Problem 71, as found in TPTP (SYN007+1.005)›
lemma "p1 = (p2 = (p3 = (p4 = (p5 = (p1 = (p2 = (p3 = (p4 = p5))))))))"
  by blast

end