Quelle  Classical.thy   Sprache: Isabelle

(*  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 🍋 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 🍋 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