# HG changeset patch # User paulson # Date 1067440580 -3600 # Node ID 05382e257d9507efd5043cd7873070e0e829015b # Parent 399a3290936c3ee656affb52c6f2e8bcd26a1c8a tidying diff -r 399a3290936c -r 05382e257d95 src/HOL/ex/Classical.thy --- a/src/HOL/ex/Classical.thy Wed Oct 29 11:50:26 2003 +0100 +++ b/src/HOL/ex/Classical.thy Wed Oct 29 16:16:20 2003 +0100 @@ -10,8 +10,9 @@ subsection{*Traditional Classical Reasoner*} -text{*Taken from @{text "FOL/cla.ML"}. When porting examples from first-order -logic, beware of the precedence of @{text "="} versus @{text "\"}.*} +text{*Taken from @{text "FOL/Classical.thy"}. When porting examples from +first-order logic, beware of the precedence of @{text "="} versus @{text +"\"}.*} lemma "(P --> Q | R) --> (P-->Q) | (P-->R)" by blast @@ -25,8 +26,8 @@ by blast -text{*Sample problems from - F. J. Pelletier, +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. @@ -120,14 +121,14 @@ by blast text{*From Wishnu Prasetya*} -lemma "(\s. q(s) --> r(s)) & ~r(s) & (\s. ~r(s) & ~q(s) --> p(t) | q(t)) +lemma "(\s. q(s) --> r(s)) & ~r(s) & (\s. ~r(s) & ~q(s) --> p(t) | q(t)) --> p(t) | r(t)" by blast subsubsection{*Problems requiring quantifier duplication*} -text{*Theorem B of Peter Andrews, Theorem Proving via General Matings, +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 @@ -157,7 +158,7 @@ by blast text{*Problem 20*} -lemma "(\x y. \z. \w. (P(x)&Q(y)-->R(z)&S(w))) +lemma "(\x y. \z. \w. (P(x)&Q(y)-->R(z)&S(w))) --> (\x y. P(x) & Q(y)) --> (\z. R(z))" by blast @@ -174,76 +175,76 @@ 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)) +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))) +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))) +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))) +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))) +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))) = +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)) +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)) +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)) +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)) = +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)) = +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 @@ -252,26 +253,26 @@ 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)) +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)) +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) | +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!*) @@ -280,12 +281,12 @@ by blast text{*Problem 40. AMENDED*} -lemma "(\y. \x. F x y = F x x) +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)) +lemma "(\z. \y. \x. f x y = (f x z & ~ f x x)) --> ~ (\z. \x. f x z)" by blast @@ -294,23 +295,23 @@ by blast text{*Problem 43!!*} -lemma "(\x::'a. \y::'a. q x y = (\z. p z x = (p z y::bool))) +lemma "(\x::'a. \y::'a. 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*} -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)) +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)) +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 @@ -321,10 +322,10 @@ lemma "(a=b | c=d) & (a=c | b=d) --> a=d | b=c" by blast -text{*Problem 49 NOT PROVED AUTOMATICALLY*} -text{*Hard because it involves substitution for Vars +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) +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) @@ -336,12 +337,12 @@ by blast text{*Problem 51*} -lemma "(\z w. \x y. P x y = (x=z & y=w)) --> +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)) --> +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 @@ -349,14 +350,14 @@ text{*Non-equational version, from Manthey and Bry, CADE-9 (Springer, 1988). fast DISCOVERS 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) --> +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) --> killed ?who agatha" by fast @@ -365,7 +366,7 @@ by blast text{*Problem 57*} -lemma "P (f a b) (f b c) & P (f b c) (f a c) & +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 @@ -382,37 +383,37 @@ 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))) & +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))) & +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. +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))) & +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 +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)) +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) & +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 @@ -522,6 +523,10 @@ lemma "\z. P z --> (\x. P x)" by meson +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*} @@ -533,7 +538,7 @@ by meson text{*Problem 20*} -lemma "(\x y. \z. \w. (P x & Q y --> R z & S w)) +lemma "(\x y. \z. \w. (P x & Q y --> R z & S w)) --> (\x y. P x & Q y) --> (\z. R z)" by meson @@ -550,78 +555,75 @@ by meson 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) +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 meson 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)) +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 meson text{*Problem 26; has 24 Horn clauses*} -lemma "((\x. p x) = (\x. q x)) & - (\x. \y. p x & q y --> (r x = s y)) +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 meson 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)) +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 meson 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)) +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 meson -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)) = +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 meson text{*Problem 30*} -lemma "(\x. P x | Q x --> ~ R x) & (\x. (Q x --> ~ S x) --> P x & R x) +lemma "(\x. P x | Q x --> ~ R x) & (\x. (Q x --> ~ S x) --> P x & R x) --> (\x. S x)" by meson 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) +lemma "~(\x. P x & (Q x | R x)) & + (\x. L x & P x) & + (\x. ~ R x --> M x) --> (\x. L x & M x)" by meson 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) +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 meson text{*Problem 33; has 55 Horn clauses*} -lemma "(\x. P a & (P x --> P b)-->P c) = +lemma "(\x. P a & (P x --> P b)-->P c) = (\x. (~P a | P x | P c) & (~P a | ~P b | P c))" by meson -text{*Problem 34 AMENDED (TWICE!!); has 924 Horn clauses*} -text{*Andrews's challenge*} -lemma "((\x. \y. p x = p y) = - ((\x. q x) = (\y. p y))) = - ((\x. \y. q x = q y) = - ((\