# Theory Classical

theory Classical
imports FOL
```(*  Title:      FOL/ex/Classical.thy
Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
*)

section ‹Classical Predicate Calculus Problems›

theory Classical
imports FOL
begin

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

subsubsection ‹If and only if›

lemma "(P ⟷ Q) ⟷ (Q ⟷ P)"
by blast

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

subsection ‹Pelletier's examples›

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.
›

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"
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

subsection ‹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‹Discussed in Avron, Gentzen-Type Systems, Resolution and Tableaux,
JAR 10 (265-281), 1993.  Proof is trivial!›
lemma "¬ ((∃x. ¬ P(x)) ∧ ((∃x. P(x)) ∨ (∃x. P(x) ∧ Q(x))) ∧ ¬ (∃x. P(x)))"
by blast

subsection ‹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 ALL.›
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

text‹V. Lifschitz, What Is the Inverse Method?, JAR 5 (1989), 1--23. NOT PROVED.›
lemma
"∃x x'. ∀y. ∃z z'.
(¬ P(y,y) ∨ P(x,x) ∨ ¬ S(z,x)) ∧
(S(x,y) ∨ ¬ S(y,z) ∨ Q(z',z')) ∧
(Q(x',y) ∨ ¬ Q(y,z') ∨ S(x',x'))"
oops

subsection ‹Hard examples with quantifiers›

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

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

text‹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‹21›
lemma "(∃x. P ⟶ Q(x)) ∧ (∃x. Q(x) ⟶ P) ⟶ (∃x. P ⟷ Q(x))"
by blast

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

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

text‹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‹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‹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‹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‹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‹29. Essentially the same as Principia Mathematica *11.71›
lemma
"(∃x. P(x)) ∧ (∃y. Q(y))
⟶ ((∀x. P(x) ⟶ R(x)) ∧ (∀y. Q(y) ⟶ S(y)) ⟷
(∀x y. P(x) ∧ Q(y) ⟶ R(x) ∧ S(y)))"
by blast

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

text‹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‹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‹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‹34. AMENDED (TWICE!!). 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‹35›
lemma "∃x y. P(x,y) ⟶ (∀u v. P(u,v))"
by blast

text‹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‹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‹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

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

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

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

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

text‹43›
lemma
"(∀x. ∀y. q(x,y) ⟷ (∀z. p(z,x) ⟷ p(z,y)))
⟶ (∀x. ∀y. q(x,y) ⟷ q(y,x))"
by blast

text ‹
Other proofs: Can use ‹auto›, which cheats by using rewriting!
‹Deepen_tac› alone requires 253 secs.  Or
‹by (mini_tac 1 THEN Deepen_tac 5 1)›.
›

text‹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‹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

text‹46›
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

subsection ‹Problems (mainly) involving equality or functions›

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

text‹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))"
apply safe
apply (rule_tac x = a in allE, assumption)
apply (rule_tac x = b in allE, assumption)
apply fast  ― ‹blast's treatment of equality can't do it›
done

text‹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‹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‹52›
text‹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‹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  ― ‹MUCH faster than blast›

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

text‹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‹58  NOT PROVED AUTOMATICALLY›
lemma "(∀x y. f(x) = g(y)) ⟶ (∀x y. f(f(x)) = f(g(y)))"
by (slow elim: subst_context)

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

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

text‹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 ‹Halting problem: Formulation of Li Dafa (AAR Newsletter 27, Oct 1994.)
author U. Egly.›
lemma
"((∃x. A(x) ∧ (∀y. C(y) ⟶ (∀z. D(x,y,z)))) ⟶
(∃w. C(w) ∧ (∀y. C(y) ⟶ (∀z. D(w,y,z)))))
∧
(∀w. C(w) ∧ (∀u. C(u) ⟶ (∀v. D(w,u,v))) ⟶
(∀y z.
(C(y) ∧ P(y,z) ⟶ Q(w,y,z) ∧ OO(w,g)) ∧
(C(y) ∧ ¬ P(y,z) ⟶ Q(w,y,z) ∧ OO(w,b))))
∧
(∀w. C(w) ∧
(∀y z.
(C(y) ∧ P(y,z) ⟶ Q(w,y,z) ∧ OO(w,g)) ∧
(C(y) ∧ ¬ P(y,z) ⟶ Q(w,y,z) ∧ OO(w,b))) ⟶
(∃v. C(v) ∧
(∀y. ((C(y) ∧ Q(w,y,y)) ∧ OO(w,g) ⟶ ¬ P(v,y)) ∧
((C(y) ∧ Q(w,y,y)) ∧ OO(w,b) ⟶ P(v,y) ∧ OO(v,b)))))
⟶ ¬ (∃x. A(x) ∧ (∀y. C(y) ⟶ (∀z. D(x,y,z))))"
by (blast 12)
― ‹Needed because the search for depths below 12 is very slow.›

text ‹
Halting problem II: credited to M. Bruschi by Li Dafa in JAR 18(1),
p. 105.
›
lemma
"((∃x. A(x) ∧ (∀y. C(y) ⟶ (∀z. D(x,y,z)))) ⟶
(∃w. C(w) ∧ (∀y. C(y) ⟶ (∀z. D(w,y,z)))))
∧
(∀w. C(w) ∧ (∀u. C(u) ⟶ (∀v. D(w,u,v))) ⟶
(∀y z.
(C(y) ∧ P(y,z) ⟶ Q(w,y,z) ∧ OO(w,g)) ∧
(C(y) ∧ ¬ P(y,z) ⟶ Q(w,y,z) ∧ OO(w,b))))
∧
((∃w. C(w) ∧ (∀y. (C(y) ∧ P(y,y) ⟶ Q(w,y,y) ∧ OO(w,g)) ∧
(C(y) ∧ ¬ P(y,y) ⟶ Q(w,y,y) ∧ OO(w,b))))
⟶
(∃v. C(v) ∧ (∀y. (C(y) ∧ P(y,y) ⟶ P(v,y) ∧ OO(v,g)) ∧
(C(y) ∧ ¬ P(y,y) ⟶ P(v,y) ∧ OO(v,b)))))
⟶
((∃v. C(v) ∧ (∀y. (C(y) ∧ P(y,y) ⟶ P(v,y) ∧ OO(v,g)) ∧
(C(y) ∧ ¬ P(y,y) ⟶ P(v,y) ∧ OO(v,b))))
⟶
(∃u. C(u) ∧ (∀y. (C(y) ∧ P(y,y) ⟶ ¬ P(u,y)) ∧
(C(y) ∧ ¬ P(y,y) ⟶ P(u,y) ∧ OO(u,b)))))
⟶ ¬ (∃x. A(x) ∧ (∀y. C(y) ⟶ (∀z. D(x,y,z))))"
by blast

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

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

(*Runtimes for old versions of this file:
Thu Jul 23 1992: loaded in 467s using iffE [on SPARC2]
Mon Nov 14 1994: loaded in 144s [on SPARC10, with deepen_tac]
Mon Nov 21 1994: loaded in 131s [DEPTH_FIRST suppressing repetitions]

Further runtimes on a Sun-4
Tue Mar  4 1997: loaded in 93s (version 94-7)
Tue Mar  4 1997: loaded in 89s
Thu Apr  3 1997: loaded in 44s--using mostly Blast_tac