Quelle Classical.thy Sprache: Isabelle

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

section\<open>Classical Predicate Calculus Problems\<close>

theory Classical imports Main begin

subsection\<open>Traditional Classical Reasoner\<close>

text\<open>The machine "griffon" mentioned below is a 2.5GHz Power Mac G5.\<close>

text\<open>Taken from \<open>FOL/Classical.thy\<close>. When porting examples from
first-order logic, beware of the precedence of \<open>=\<close> versus \<open>\<leftrightarrow>\<close>.\<close>

lemma "(P \ Q \ R) \ (P\Q) \ (P\R)"
by blast

text\<open>If and only if\<close>

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

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

text\<open>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.
\<close>

subsubsection\<open>Pelletier's examples\<close>

text\<open>1\<close>
lemma "(P\Q) = (\Q \ \P)"
by blast

text\<open>2\<close>
lemma "(\ \ P) = P"
by blast

text\<open>3\<close>
lemma "\(P\Q) \ (Q\P)"
by blast

text\<open>4\<close>
lemma "(\P\Q) = (\Q \ P)"
by blast

text\<open>5\<close>
lemma "((P\Q)\(P\R)) \ (P\(Q\R))"
by blast

text\<open>6\<close>
lemma "P \ \ P"
by blast

text\<open>7\<close>
lemma "P \ \ \ \ P"
by blast

text\<open>8.  Peirce's law\<close>
lemma "((P\Q) \ P) \ P"
by blast

text\<open>9\<close>
lemma "((P\Q) \ (\P\Q) \ (P\ \Q)) \ \ (\P \ \Q)"
by blast

text\<open>10\<close>
lemma "(Q\R) \ (R\P\Q) \ (P\Q\R) \ (P=Q)"
by blast

text\<open>11.  Proved in each direction (incorrectly, says Pelletier!!)\<close>
lemma "P=(P::bool)"
by blast

text\<open>12.  "Dijkstra's law"\<close>
lemma "((P = Q) = R) = (P = (Q = R))"
by blast

text\<open>13.  Distributive law\<close>
lemma "(P \ (Q \ R)) = ((P \ Q) \ (P \ R))"
by blast

text\<open>14\<close>
lemma "(P = Q) = ((Q \ \P) \ (\Q\P))"
by blast

text\<open>15\<close>
lemma "(P \ Q) = (\P \ Q)"
by blast

text\<open>16\<close>
lemma "(P\Q) \ (Q\P)"
by blast

text\<open>17\<close>
lemma "((P \ (Q\R))\S) = ((\P \ Q \ S) \ (\P \ \R \ S))"
by blast

subsubsection\<open>Classical Logic: examples with quantifiers\<close>

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\<open>From Wishnu Prasetya\<close>
lemma "(\x. Q(x) \ R(x)) \ \R(a) \ (\x. \R(x) \ \Q(x) \ P(b) \ Q(b))
    \<longrightarrow> P(b) \<or> R(b)"
by blast

subsubsection\<open>Problems requiring quantifier duplication\<close>

text\<open>Theorem B of Peter Andrews, Theorem Proving via General Matings,
  JACM 28 (1981).\<close>
lemma "(\x. \y. P(x) = P(y)) \ ((\x. P(x)) = (\y. P(y)))"
by blast

text\<open>Needs multiple instantiation of the quantifier.\<close>
lemma "(\x. P(x)\P(f(x))) \ P(d)\P(f(f(f(d))))"
by blast

text\<open>Needs double instantiation of the quantifier\<close>
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\<open>Hard examples with quantifiers\<close>

text\<open>Problem 18\<close>
lemma "\y. \x. P(y)\P(x)"
by blast

text\<open>Problem 19\<close>
lemma "\x. \y z. (P(y)\Q(z)) \ (P(x)\Q(x))"
by blast

text\<open>Problem 20\<close>
lemma "(\x y. \z. \w. (P(x)\Q(y)\R(z)\S(w)))
    \<longrightarrow> (\<exists>x y. P(x) \<and> Q(y)) \<longrightarrow> (\<exists>z. R(z))"
by blast

text\<open>Problem 21\<close>
lemma "(\x. P\Q(x)) \ (\x. Q(x)\P) \ (\x. P=Q(x))"
by blast

text\<open>Problem 22\<close>
lemma "(\x. P = Q(x)) \ (P = (\x. Q(x)))"
by blast

text\<open>Problem 23\<close>
lemma "(\x. P \ Q(x)) = (P \ (\x. Q(x)))"
by blast

text\<open>Problem 24\<close>
lemma "\(\x. S(x)\Q(x)) \ (\x. P(x) \ Q(x)\R(x)) \
     (\<not>(\<exists>x. P(x)) \<longrightarrow> (\<exists>x. Q(x))) \<and> (\<forall>x. Q(x)\<or>R(x) \<longrightarrow> S(x))
    \<longrightarrow> (\<exists>x. P(x)\<and>R(x))"
by blast

text\<open>Problem 25\<close>
lemma "(\x. P(x)) \
        (\<forall>x. L(x) \<longrightarrow> \<not> (M(x) \<and> R(x))) \<and>
        (\<forall>x. P(x) \<longrightarrow> (M(x) \<and> L(x))) \<and>
        ((\<forall>x. P(x)\<longrightarrow>Q(x)) \<or> (\<exists>x. P(x)\<and>R(x)))
    \<longrightarrow> (\<exists>x. Q(x)\<and>P(x))"
by blast

text\<open>Problem 26\<close>
lemma "((\x. p(x)) = (\x. q(x))) \
      (\<forall>x. \<forall>y. p(x) \<and> q(y) \<longrightarrow> (r(x) = s(y)))
  \<longrightarrow> ((\<forall>x. p(x)\<longrightarrow>r(x)) = (\<forall>x. q(x)\<longrightarrow>s(x)))"
by blast

text\<open>Problem 27\<close>
lemma "(\x. P(x) \ \Q(x)) \
              (\<forall>x. P(x) \<longrightarrow> R(x)) \<and>
              (\<forall>x. M(x) \<and> L(x) \<longrightarrow> P(x)) \<and>
              ((\<exists>x. R(x) \<and> \<not> Q(x)) \<longrightarrow> (\<forall>x. L(x) \<longrightarrow> \<not> R(x)))
          \<longrightarrow> (\<forall>x. M(x) \<longrightarrow> \<not>L(x))"
by blast

text\<open>Problem 28.  AMENDED\<close>
lemma "(\x. P(x) \ (\x. Q(x))) \
        ((\<forall>x. Q(x)\<or>R(x)) \<longrightarrow> (\<exists>x. Q(x)\<and>S(x))) \<and>
        ((\<exists>x. S(x)) \<longrightarrow> (\<forall>x. L(x) \<longrightarrow> M(x)))
    \<longrightarrow> (\<forall>x. P(x) \<and> L(x) \<longrightarrow> M(x))"
by blast

text\<open>Problem 29.  Essentially the same as Principia Mathematica *11.71\<close>
lemma "(\x. F(x)) \ (\y. G(y))
    \<longrightarrow> ( ((\<forall>x. F(x)\<longrightarrow>H(x)) \<and> (\<forall>y. G(y)\<longrightarrow>J(y)))  =
          (\<forall>x y. F(x) \<and> G(y) \<longrightarrow> H(x) \<and> J(y)))"
by blast

text\<open>Problem 30\<close>
lemma "(\x. P(x) \ Q(x) \ \ R(x)) \
        (\<forall>x. (Q(x) \<longrightarrow> \<not> S(x)) \<longrightarrow> P(x) \<and> R(x))
    \<longrightarrow> (\<forall>x. S(x))"
by blast

text\<open>Problem 31\<close>
lemma "\(\x. P(x) \ (Q(x) \ R(x))) \
        (\<exists>x. L(x) \<and> P(x)) \<and>
        (\<forall>x. \<not> R(x) \<longrightarrow> M(x))
    \<longrightarrow> (\<exists>x. L(x) \<and> M(x))"
by blast

text\<open>Problem 32\<close>
lemma "(\x. P(x) \ (Q(x)\R(x))\S(x)) \
        (\<forall>x. S(x) \<and> R(x) \<longrightarrow> L(x)) \<and>
        (\<forall>x. M(x) \<longrightarrow> R(x))
    \<longrightarrow> (\<forall>x. P(x) \<and> M(x) \<longrightarrow> L(x))"
by blast

text\<open>Problem 33\<close>
lemma "(\x. P(a) \ (P(x)\P(b))\P(c)) =
     (\<forall>x. (\<not>P(a) \<or> P(x) \<or> P(c)) \<and> (\<not>P(a) \<or> \<not>P(b) \<or> P(c)))"
by blast

text\<open>Problem 34  AMENDED (TWICE!!)\<close>
text\<open>Andrews's challenge\<close>
lemma "((\x. \y. p(x) = p(y)) =
               ((\<exists>x. q(x)) = (\<forall>y. p(y))))   =
              ((\<exists>x. \<forall>y. q(x) = q(y))  =
               ((\<exists>x. p(x)) = (\<forall>y. q(y))))"
by blast

text\<open>Problem 35\<close>
lemma "\x y. P x y \ (\u v. P u v)"
by blast

text\<open>Problem 36\<close>
lemma "(\x. \y. J x y) \
        (\<forall>x. \<exists>y. G x y) \<and>
        (\<forall>x y. J x y \<or> G x y \<longrightarrow>
        (\<forall>z. J y z \<or> G y z \<longrightarrow> H x z))
    \<longrightarrow> (\<forall>x. \<exists>y. H x y)"
by blast

text\<open>Problem 37\<close>
lemma "(\z. \w. \x. \y.
           (P x z \<longrightarrow>P y w) \<and> P y z \<and> (P y w \<longrightarrow> (\<exists>u. Q u w))) \<and>
        (\<forall>x z. \<not>(P x z) \<longrightarrow> (\<exists>y. Q y z)) \<and>
        ((\<exists>x y. Q x y) \<longrightarrow> (\<forall>x. R x x))
    \<longrightarrow> (\<forall>x. \<exists>y. R x y)"
by blast

text\<open>Problem 38\<close>
lemma "(\x. p(a) \ (p(x) \ (\y. p(y) \ r x y)) \
           (\<exists>z. \<exists>w. p(z) \<and> r x w \<and> r w z))  =
     (\<forall>x. (\<not>p(a) \<or> p(x) \<or> (\<exists>z. \<exists>w. p(z) \<and> r x w \<and> r w z)) \<and>
           (\<not>p(a) \<or> \<not>(\<exists>y. p(y) \<and> r x y) \<or>
            (\<exists>z. \<exists>w. p(z) \<and> r x w \<and> r w z)))"
by blast (*beats fast!*)

text\<open>Problem 39\<close>
lemma "\ (\x. \y. F y x = (\ F y y))"
by blast

text\<open>Problem 40.  AMENDED\<close>
lemma "(\y. \x. F x y = F x x)
        \<longrightarrow>  \<not> (\<forall>x. \<exists>y. \<forall>z. F z y = (\<not> F z x))"
by blast

text\<open>Problem 41\<close>
lemma "(\z. \y. \x. f x y = (f x z \ \ f x x))
               \<longrightarrow> \<not> (\<exists>z. \<forall>x. f x z)"
by blast

text\<open>Problem 42\<close>
lemma "\ (\y. \x. p x y = (\ (\z. p x z \ p z x)))"
by blast

text\<open>Problem 43!!\<close>
lemma "(\x::'a. \y::'a. q x y = (\z. p z x \ (p z y)))
  \<longrightarrow> (\<forall>x. (\<forall>y. q x y \<longleftrightarrow> (q y x)))"
by blast

text\<open>Problem 44\<close>
lemma "(\x. f(x) \
              (\<exists>y. g(y) \<and> h x y \<and> (\<exists>y. g(y) \<and> \<not> h x y)))  \<and>
              (\<exists>x. j(x) \<and> (\<forall>y. g(y) \<longrightarrow> h x y))
              \<longrightarrow> (\<exists>x. j(x) \<and> \<not>f(x))"
by blast

text\<open>Problem 45\<close>
lemma "(\x. f(x) \ (\y. g(y) \ h x y \ j x y)
                      \<longrightarrow> (\<forall>y. g(y) \<and> h x y \<longrightarrow> k(y))) \<and>
     \<not> (\<exists>y. l(y) \<and> k(y)) \<and>
     (\<exists>x. f(x) \<and> (\<forall>y. h x y \<longrightarrow> l(y))
                \<and> (\<forall>y. g(y) \<and> h x y \<longrightarrow> j x y))
      \<longrightarrow> (\<exists>x. f(x) \<and> \<not> (\<exists>y. g(y) \<and> h x y))"
by blast

subsubsection\<open>Problems (mainly) involving equality or functions\<close>

text\<open>Problem 48\<close>
lemma "(a=b \ c=d) \ (a=c \ b=d) \ a=d \ b=c"
by blast

text\<open>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.\<close>
lemma "(\x y::'a. \z. z=x \ z=y) \ P(a) \ P(b) \ (\a=b)
                \<longrightarrow> (\<forall>u::'a. P(u))"
by metis

text\<open>Problem 50.  (What has this to do with equality?)\<close>
lemma "(\x. P a x \ (\y. P x y)) \ (\x. \y. P x y)"
by blast

text\<open>Problem 51\<close>
lemma "(\z w. \x y. P x y = (x=z \ y=w)) \
     (\<exists>z. \<forall>x. \<exists>w. (\<forall>y. P x y = (y=w)) = (x=z))"
by blast

text\<open>Problem 52. Almost the same as 51.\<close>
lemma "(\z w. \x y. P x y = (x=z \ y=w)) \
     (\<exists>w. \<forall>y. \<exists>z. (\<forall>x. P x y = (x=z)) = (y=w))"
by blast

text\<open>Problem 55\<close>

text\<open>Non-equational version, from Manthey and Bry, CADE-9 (Springer, 1988).
  fast DISCOVERS who killed Agatha.\<close>
schematic_goal "lives(agatha) \ lives(butler) \ lives(charles) \
   (killed agatha agatha \<or> killed butler agatha \<or> killed charles agatha) \<and>
   (\<forall>x y. killed x y \<longrightarrow> hates x y \<and> \<not>richer x y) \<and>
   (\<forall>x. hates agatha x \<longrightarrow> \<not>hates charles x) \<and>
   (hates agatha agatha \<and> hates agatha charles) \<and>
   (\<forall>x. lives(x) \<and> \<not>richer x agatha \<longrightarrow> hates butler x) \<and>
   (\<forall>x. hates agatha x \<longrightarrow> hates butler x) \<and>
   (\<forall>x. \<not>hates x agatha \<or> \<not>hates x butler \<or> \<not>hates x charles) \<longrightarrow>
    killed ?who agatha"
by fast

text\<open>Problem 56\<close>
lemma "(\x. (\y. P(y) \ x=f(y)) \ P(x)) = (\x. P(x) \ P(f(x)))"
by blast

text\<open>Problem 57\<close>
lemma "P (f a b) (f b c) \ P (f b c) (f a c) \
     (\<forall>x y z. P x y \<and> P y z \<longrightarrow> P x z)    \<longrightarrow>   P (f a b) (f a c)"
by blast

text\<open>Problem 58  NOT PROVED AUTOMATICALLY\<close>
lemma "(\x y. f(x)=g(y)) \ (\x y. f(f(x))=f(g(y)))"
by (fast intro: arg_cong [of concl: f])

text\<open>Problem 59\<close>
lemma "(\x. P(x) = (\P(f(x)))) \ (\x. P(x) \ \P(f(x)))"
by blast

text\<open>Problem 60\<close>
lemma "\x. P x (f x) = (\y. (\z. P z y \ P z (f x)) \ P x y)"
by blast

text\<open>Problem 62 as corrected in JAR 18 (1997), page 135\<close>
lemma "(\x. p a \ (p x \ p(f x)) \ p(f(f x))) =
      (\<forall>x. (\<not> p a \<or> p x \<or> p(f(f x))) \<and>
              (\<not> p a \<or> \<not> p(f x) \<or> p(f(f x))))"
by blast

text\<open>From Davis, Obvious Logical Inferences, IJCAI-81, 530-531
  fast indeed copes!\<close>
lemma "(\x. F(x) \ \G(x) \ (\y. H(x,y) \ J(y))) \
       (\<exists>x. K(x) \<and> F(x) \<and> (\<forall>y. H(x,y) \<longrightarrow> K(y))) \<and>
       (\<forall>x. K(x) \<longrightarrow> \<not>G(x))  \<longrightarrow>  (\<exists>x. K(x) \<and> J(x))"
by fast

text\<open>From Rudnicki, Obvious Inferences, JAR 3 (1987), 383-393.
  It does seem obvious!\<close>
lemma "(\x. F(x) \ \G(x) \ (\y. H(x,y) \ J(y))) \
       (\<exists>x. K(x) \<and> F(x) \<and> (\<forall>y. H(x,y) \<longrightarrow> K(y)))  \<and>
       (\<forall>x. K(x) \<longrightarrow> \<not>G(x))   \<longrightarrow>   (\<exists>x. K(x) \<longrightarrow> \<not>G(x))"
by fast

text\<open>Attributed to Lewis Carroll by S. G. Pulman.  The first or last
assumption can be deleted.\<close>
lemma "(\x. honest(x) \ industrious(x) \ healthy(x)) \
      \<not> (\<exists>x. grocer(x) \<and> healthy(x)) \<and>
      (\<forall>x. industrious(x) \<and> grocer(x) \<longrightarrow> honest(x)) \<and>
      (\<forall>x. cyclist(x) \<longrightarrow> industrious(x)) \<and>
      (\<forall>x. \<not>healthy(x) \<and> cyclist(x) \<longrightarrow> \<not>honest(x))
      \<longrightarrow> (\<forall>x. grocer(x) \<longrightarrow> \<not>cyclist(x))"
by blast

lemma "(\x y. R(x,y) \ R(y,x)) \
       (\<forall>x y. S(x,y) \<and> S(y,x) \<longrightarrow> x=y) \<and>
       (\<forall>x y. R(x,y) \<longrightarrow> S(x,y))    \<longrightarrow>   (\<forall>x y. S(x,y) \<longrightarrow> R(x,y))"
by blast

subsection\<open>Model Elimination Prover\<close>

text\<open>Trying out meson with arguments\<close>
lemma "x < y \ y < z \ \ (z < (x::nat))"
by (meson order_less_irrefl order_less_trans)

text\<open>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\<close>
lemma "(\x y z. R(x,y) \ R(y,z) \ R(x,z)) \
       (\<forall>x. \<exists>y. R(x,y)) \<longrightarrow>
       \<not> (\<forall>x. P x = (\<forall>y. R(x,y) \<longrightarrow> \<not> P y))"
by (tactic\<open>Meson.safe_best_meson_tac \<^context> 1\<close>)
    \<comment> \<open>In contrast, \<open>meson\<close> is SLOW: 7.6s on griffon\<close>

subsubsection\<open>Pelletier's examples\<close>
text\<open>1\<close>
lemma "(P \ Q) = (\Q \ \P)"
by blast

text\<open>2\<close>
lemma "(\ \ P) = P"
by blast

text\<open>3\<close>
lemma "\(P\Q) \ (Q\P)"
by blast

text\<open>4\<close>
lemma "(\P\Q) = (\Q \ P)"
by blast

text\<open>5\<close>
lemma "((P\Q)\(P\R)) \ (P\(Q\R))"
by blast

text\<open>6\<close>
lemma "P \ \ P"
by blast

text\<open>7\<close>
lemma "P \ \ \ \ P"
by blast

text\<open>8.  Peirce's law\<close>
lemma "((P\Q) \ P) \ P"
by blast

text\<open>9\<close>
lemma "((P\Q) \ (\P\Q) \ (P\ \Q)) \ \ (\P \ \Q)"
by blast

text\<open>10\<close>
lemma "(Q\R) \ (R\P\Q) \ (P\Q\R) \ (P=Q)"
by blast

text\<open>11.  Proved in each direction (incorrectly, says Pelletier!!)\<close>
lemma "P=(P::bool)"
by blast

text\<open>12.  "Dijkstra's law"\<close>
lemma "((P = Q) = R) = (P = (Q = R))"
by blast

text\<open>13.  Distributive law\<close>
lemma "(P \ (Q \ R)) = ((P \ Q) \ (P \ R))"
by blast

text\<open>14\<close>
lemma "(P = Q) = ((Q \ \P) \ (\Q\P))"
by blast

text\<open>15\<close>
lemma "(P \ Q) = (\P \ Q)"
by blast

text\<open>16\<close>
lemma "(P\Q) \ (Q\P)"
by blast

text\<open>17\<close>
lemma "((P \ (Q\R))\S) = ((\P \ Q \ S) \ (\P \ \R \ S))"
by blast

subsubsection\<open>Classical Logic: examples with quantifiers\<close>

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\<open>Needs double instantiation of EXISTS\<close>
lemma "\x. P x \ P a \ P b"
by blast

lemma "\z. P z \ (\x. P x)"
by blast

text\<open>From a paper by Claire Quigley\<close>
lemma "\y. ((P c \ Q y) \ (\z. \ Q z)) \ (\x. \ P x \ Q d)"
by fast

subsubsection\<open>Hard examples with quantifiers\<close>

text\<open>Problem 18\<close>
lemma "\y. \x. P y \ P x"
by blast

text\<open>Problem 19\<close>
lemma "\x. \y z. (P y \ Q z) \ (P x \ Q x)"
by blast

text\<open>Problem 20\<close>
lemma "(\x y. \z. \w. (P x \ Q y \ R z \ S w))
    \<longrightarrow> (\<exists>x y. P x \<and> Q y) \<longrightarrow> (\<exists>z. R z)"
by blast

text\<open>Problem 21\<close>
lemma "(\x. P \ Q x) \ (\x. Q x \ P) \ (\x. P=Q x)"
by blast

text\<open>Problem 22\<close>
lemma "(\x. P = Q x) \ (P = (\x. Q x))"
by blast

text\<open>Problem 23\<close>
lemma "(\x. P \ Q x) = (P \ (\x. Q x))"
by blast

text\<open>Problem 24\<close>  (*The first goal clause is useless*)
lemma "\(\x. S x \ Q x) \ (\x. P x \ Q x \ R x) \
      (\<not>(\<exists>x. P x) \<longrightarrow> (\<exists>x. Q x)) \<and> (\<forall>x. Q x \<or> R x \<longrightarrow> S x)
    \<longrightarrow> (\<exists>x. P x \<and> R x)"
by blast

text\<open>Problem 25\<close>
lemma "(\x. P x) \
      (\<forall>x. L x \<longrightarrow> \<not> (M x \<and> R x)) \<and>
      (\<forall>x. P x \<longrightarrow> (M x \<and> L x)) \<and>
      ((\<forall>x. P x \<longrightarrow> Q x) \<or> (\<exists>x. P x \<and> R x))
    \<longrightarrow> (\<exists>x. Q x \<and> P x)"
by blast

text\<open>Problem 26; has 24 Horn clauses\<close>
lemma "((\x. p x) = (\x. q x)) \
      (\<forall>x. \<forall>y. p x \<and> q y \<longrightarrow> (r x = s y))
  \<longrightarrow> ((\<forall>x. p x \<longrightarrow> r x) = (\<forall>x. q x \<longrightarrow> s x))"
by blast

text\<open>Problem 27; has 13 Horn clauses\<close>
lemma "(\x. P x \ \Q x) \
      (\<forall>x. P x \<longrightarrow> R x) \<and>
      (\<forall>x. M x \<and> L x \<longrightarrow> P x) \<and>
      ((\<exists>x. R x \<and> \<not> Q x) \<longrightarrow> (\<forall>x. L x \<longrightarrow> \<not> R x))
      \<longrightarrow> (\<forall>x. M x \<longrightarrow> \<not>L x)"
by blast

text\<open>Problem 28.  AMENDED; has 14 Horn clauses\<close>
lemma "(\x. P x \ (\x. Q x)) \
      ((\<forall>x. Q x \<or> R x) \<longrightarrow> (\<exists>x. Q x \<and> S x)) \<and>
      ((\<exists>x. S x) \<longrightarrow> (\<forall>x. L x \<longrightarrow> M x))
    \<longrightarrow> (\<forall>x. P x \<and> L x \<longrightarrow> M x)"
by blast

text\<open>Problem 29.  Essentially the same as Principia Mathematica *11.71.
      62 Horn clauses\<close>
lemma "(\x. F x) \ (\y. G y)
    \<longrightarrow> ( ((\<forall>x. F x \<longrightarrow> H x) \<and> (\<forall>y. G y \<longrightarrow> J y))  =
          (\<forall>x y. F x \<and> G y \<longrightarrow> H x \<and> J y))"
by blast

text\<open>Problem 30\<close>
lemma "(\x. P x \ Q x \ \ R x) \ (\x. (Q x \ \ S x) \ P x \ R x)
       \<longrightarrow> (\<forall>x. S x)"
by blast

text\<open>Problem 31; has 10 Horn clauses; first negative clauses is useless\<close>
lemma "\(\x. P x \ (Q x \ R x)) \
      (\<exists>x. L x \<and> P x) \<and>
      (\<forall>x. \<not> R x \<longrightarrow> M x)
    \<longrightarrow> (\<exists>x. L x \<and> M x)"
by blast

text\<open>Problem 32\<close>
lemma "(\x. P x \ (Q x \ R x)\S x) \
      (\<forall>x. S x \<and> R x \<longrightarrow> L x) \<and>
      (\<forall>x. M x \<longrightarrow> R x)
    \<longrightarrow> (\<forall>x. P x \<and> M x \<longrightarrow> L x)"
by blast

text\<open>Problem 33; has 55 Horn clauses\<close>
lemma "(\x. P a \ (P x \ P b)\P c) =
      (\<forall>x. (\<not>P a \<or> P x \<or> P c) \<and> (\<not>P a \<or> \<not>P b \<or> P c))"
by blast

text\<open>Problem 34: Andrews's challenge has 924 Horn clauses\<close>
lemma "((\x. \y. p x = p y) = ((\x. q x) = (\y. p y))) =
      ((\<exists>x. \<forall>y. q x = q y)  = ((\<exists>x. p x) = (\<forall>y. q y)))"
by blast

text\<open>Problem 35\<close>
lemma "\x y. P x y \ (\u v. P u v)"
by blast

text\<open>Problem 36; has 15 Horn clauses\<close>
lemma "(\x. \y. J x y) \ (\x. \y. G x y) \
       (\<forall>x y. J x y \<or> G x y \<longrightarrow> (\<forall>z. J y z \<or> G y z \<longrightarrow> H x z))
       \<longrightarrow> (\<forall>x. \<exists>y. H x y)"
by blast

text\<open>Problem 37; has 10 Horn clauses\<close>
lemma "(\z. \w. \x. \y.
           (P x z \<longrightarrow> P y w) \<and> P y z \<and> (P y w \<longrightarrow> (\<exists>u. Q u w))) \<and>
      (\<forall>x z. \<not>P x z \<longrightarrow> (\<exists>y. Q y z)) \<and>
      ((\<exists>x y. Q x y) \<longrightarrow> (\<forall>x. R x x))
    \<longrightarrow> (\<forall>x. \<exists>y. R x y)"
by blast \<comment> \<open>causes unification tracing messages\<close>

text\<open>Problem 38\<close>  text\<open>Quite hard: 422 Horn clauses!!\<close>
lemma "(\x. p a \ (p x \ (\y. p y \ r x y)) \
           (\<exists>z. \<exists>w. p z \<and> r x w \<and> r w z))  =
      (\<forall>x. (\<not>p a \<or> p x \<or> (\<exists>z. \<exists>w. p z \<and> r x w \<and> r w z)) \<and>
            (\<not>p a \<or> \<not>(\<exists>y. p y \<and> r x y) \<or>
             (\<exists>z. \<exists>w. p z \<and> r x w \<and> r w z)))"
by blast

text\<open>Problem 39\<close>
lemma "\ (\x. \y. F y x = (\F y y))"
by blast

text\<open>Problem 40.  AMENDED\<close>
lemma "(\y. \x. F x y = F x x)
      \<longrightarrow>  \<not> (\<forall>x. \<exists>y. \<forall>z. F z y = (\<not>F z x))"
by blast

text\<open>Problem 41\<close>
lemma "(\z. (\y. (\x. f x y = (f x z \ \ f x x))))
      \<longrightarrow> \<not> (\<exists>z. \<forall>x. f x z)"
by blast

text\<open>Problem 42\<close>
lemma "\ (\y. \x. p x y = (\ (\z. p x z \ p z x)))"
by blast

text\<open>Problem 43  NOW PROVED AUTOMATICALLY!!\<close>
lemma "(\x. \y. q x y = (\z. p z x = (p z y::bool)))
      \<longrightarrow> (\<forall>x. (\<forall>y. q x y = (q y x::bool)))"
by blast

text\<open>Problem 44: 13 Horn clauses; 7-step proof\<close>
lemma "(\x. f x \ (\y. g y \ h x y \ (\y. g y \ \ h x y))) \
       (\<exists>x. j x \<and> (\<forall>y. g y \<longrightarrow> h x y))
       \<longrightarrow> (\<exists>x. j x \<and> \<not>f x)"
by blast

text\<open>Problem 45; has 27 Horn clauses; 54-step proof\<close>
lemma "(\x. f x \ (\y. g y \ h x y \ j x y)
            \<longrightarrow> (\<forall>y. g y \<and> h x y \<longrightarrow> k y)) \<and>
      \<not> (\<exists>y. l y \<and> k y) \<and>
      (\<exists>x. f x \<and> (\<forall>y. h x y \<longrightarrow> l y)
                \<and> (\<forall>y. g y \<and> h x y \<longrightarrow> j x y))
      \<longrightarrow> (\<exists>x. f x \<and> \<not> (\<exists>y. g y \<and> h x y))"
by blast

text\<open>Problem 46; has 26 Horn clauses; 21-step proof\<close>
lemma "(\x. f x \ (\y. f y \ h y x \ g y) \ g x) \
       ((\<exists>x. f x \<and> \<not>g x) \<longrightarrow>
       (\<exists>x. f x \<and> \<not>g x \<and> (\<forall>y. f y \<and> \<not>g y \<longrightarrow> j x y))) \<and>
       (\<forall>x y. f x \<and> f y \<and> h x y \<longrightarrow> \<not>j y x)
       \<longrightarrow> (\<forall>x. f x \<longrightarrow> g x)"
by blast

text\<open>Problem 47.  Schubert's Steamroller.
      26 clauses; 63 Horn clauses.
      87094 inferences so far.  Searching to depth 36\<close>
lemma "(\x. wolf x \ animal x) \ (\x. wolf x) \
       (\<forall>x. fox x \<longrightarrow> animal x) \<and> (\<exists>x. fox x) \<and>
       (\<forall>x. bird x \<longrightarrow> animal x) \<and> (\<exists>x. bird x) \<and>
       (\<forall>x. caterpillar x \<longrightarrow> animal x) \<and> (\<exists>x. caterpillar x) \<and>
       (\<forall>x. snail x \<longrightarrow> animal x) \<and> (\<exists>x. snail x) \<and>
       (\<forall>x. grain x \<longrightarrow> plant x) \<and> (\<exists>x. grain x) \<and>
       (\<forall>x. animal x \<longrightarrow>
             ((\<forall>y. plant y \<longrightarrow> eats x y)  \<or>
              (\<forall>y. animal y \<and> smaller_than y x \<and>
                    (\<exists>z. plant z \<and> eats y z) \<longrightarrow> eats x y))) \<and>
       (\<forall>x y. bird y \<and> (snail x \<or> caterpillar x) \<longrightarrow> smaller_than x y) \<and>
       (\<forall>x y. bird x \<and> fox y \<longrightarrow> smaller_than x y) \<and>
       (\<forall>x y. fox x \<and> wolf y \<longrightarrow> smaller_than x y) \<and>
       (\<forall>x y. wolf x \<and> (fox y \<or> grain y) \<longrightarrow> \<not>eats x y) \<and>
       (\<forall>x y. bird x \<and> caterpillar y \<longrightarrow> eats x y) \<and>
       (\<forall>x y. bird x \<and> snail y \<longrightarrow> \<not>eats x y) \<and>
       (\<forall>x. (caterpillar x \<or> snail x) \<longrightarrow> (\<exists>y. plant y \<and> eats x y))
       \<longrightarrow> (\<exists>x y. animal x \<and> animal y \<and> (\<exists>z. grain z \<and> eats y z \<and> eats x y))"
by (tactic\<open>Meson.safe_best_meson_tac \<^context> 1\<close>)
    \<comment> \<open>Nearly twice as fast as \<open>meson\<close>,
        which performs iterative deepening rather than best-first search\<close>

text\<open>The Los problem. Circulated by John Harrison\<close>
lemma "(\x y z. P x y \ P y z \ P x z) \
       (\<forall>x y z. Q x y \<and> Q y z \<longrightarrow> Q x z) \<and>
       (\<forall>x y. P x y \<longrightarrow> P y x) \<and>
       (\<forall>x y. P x y \<or> Q x y)
       \<longrightarrow> (\<forall>x y. P x y) \<or> (\<forall>x y. Q x y)"
by meson

text\<open>A similar example, suggested by Johannes Schumann and
credited to Pelletier\<close>
lemma "(\x y z. P x y \ P y z \ P x z) \
       (\<forall>x y z. Q x y \<longrightarrow> Q y z \<longrightarrow> Q x z) \<longrightarrow>
       (\<forall>x y. Q x y \<longrightarrow> Q y x) \<longrightarrow>  (\<forall>x y. P x y \<or> Q x y) \<longrightarrow>
       (\<forall>x y. P x y) \<or> (\<forall>x y. Q x y)"
by meson

text\<open>Problem 50.  What has this to do with equality?\<close>
lemma "(\x. P a x \ (\y. P x y)) \ (\x. \y. P x y)"
by blast

text\<open>Problem 54: NOT PROVED\<close>
lemma "(\y::'a. \z. \x. F x z = (x=y)) \
      \<not> (\<exists>w. \<forall>x. F x w = (\<forall>u. F x u \<longrightarrow> (\<exists>y. F y u \<and> \<not> (\<exists>z. F z u \<and> F z y))))"
oops

text\<open>Problem 55\<close>

text\<open>Non-equational version, from Manthey and Bry, CADE-9 (Springer, 1988).
  \<open>meson\<close> cannot report who killed Agatha.\<close>
lemma "lives agatha \ lives butler \ lives charles \
       (killed agatha agatha \<or> killed butler agatha \<or> killed charles agatha) \<and>
       (\<forall>x y. killed x y \<longrightarrow> hates x y \<and> \<not>richer x y) \<and>
       (\<forall>x. hates agatha x \<longrightarrow> \<not>hates charles x) \<and>
       (hates agatha agatha \<and> hates agatha charles) \<and>
       (\<forall>x. lives x \<and> \<not>richer x agatha \<longrightarrow> hates butler x) \<and>
       (\<forall>x. hates agatha x \<longrightarrow> hates butler x) \<and>
       (\<forall>x. \<not>hates x agatha \<or> \<not>hates x butler \<or> \<not>hates x charles) \<longrightarrow>
       (\<exists>x. killed x agatha)"
by meson

text\<open>Problem 57\<close>
lemma "P (f a b) (f b c) \ P (f b c) (f a c) \
      (\<forall>x y z. P x y \<and> P y z \<longrightarrow> P x z)    \<longrightarrow>   P (f a b) (f a c)"
by blast

text\<open>Problem 58: Challenge found on info-hol\<close>
lemma "\P Q R x. \v w. \y z. P x \ Q y \ (P v \ R w) \ (R z \ Q v)"
by blast

text\<open>Problem 59\<close>
lemma "(\x. P x = (\P(f x))) \ (\x. P x \ \P(f x))"
by blast

text\<open>Problem 60\<close>
lemma "\x. P x (f x) = (\y. (\z. P z y \ P z (f x)) \ P x y)"
by blast

text\<open>Problem 62 as corrected in JAR 18 (1997), page 135\<close>
lemma "(\x. p a \ (p x \ p(f x)) \ p(f(f x))) =
       (\<forall>x. (\<not> p a \<or> p x \<or> p(f(f x))) \<and>
            (\<not> p a \<or> \<not> p(f x) \<or> p(f(f x))))"
by blast

text\<open>Charles Morgan's problems\<close>
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 \<comment> \<open>4.9s on griffon. 51061 inferences, depth 21\<close>

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\<open>Problem 71, as found in TPTP (SYN007+1.005)\<close>
lemma "p1 = (p2 = (p3 = (p4 = (p5 = (p1 = (p2 = (p3 = (p4 = p5))))))))"
  by blast

end

quality97%

¤ Dauer der Verarbeitung: 0.19 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.