author paulson Fri, 20 May 2005 18:34:14 +0200 changeset 16011 237aafbdb1f4 parent 16010 0705c8d1f107 child 16012 4ae42d8f2fea
converted some problems to Isar format
 src/HOL/ex/Classical.thy file | annotate | diff | comparison | revisions src/HOL/ex/mesontest2.ML file | annotate | diff | comparison | revisions
```--- a/src/HOL/ex/Classical.thy	Thu May 19 18:07:05 2005 +0200
+++ b/src/HOL/ex/Classical.thy	Fri May 20 18:34:14 2005 +0200
@@ -10,6 +10,8 @@

+text{*The machine "griffon" mentioned below is a 2.5GHz Power Mac G5.*}
+
text{*Taken from @{text "FOL/Classical.thy"}. When porting examples from
first-order logic, beware of the precedence of @{text "="} versus @{text
"\<leftrightarrow>"}.*}
@@ -427,101 +429,101 @@
(\<forall>x. \<exists>y. R(x,y)) -->
~ (\<forall>x. P x = (\<forall>y. R(x,y) --> ~ P y))"
by (tactic{*safe_best_meson_tac 1*})
-    --{*In contrast, @{text meson} is SLOW: 15s on a 1.8GHz machine!*}
+    --{*In contrast, @{text meson} is SLOW: 7.6s on griffon*}

subsubsection{*Pelletier's examples*}
text{*1*}
lemma "(P --> Q)  =  (~Q --> ~P)"
-by meson
+by blast

text{*2*}
lemma "(~ ~ P) =  P"
-by meson
+by blast

text{*3*}
lemma "~(P-->Q) --> (Q-->P)"
-by meson
+by blast

text{*4*}
lemma "(~P-->Q)  =  (~Q --> P)"
-by meson
+by blast

text{*5*}
lemma "((P|Q)-->(P|R)) --> (P|(Q-->R))"
-by meson
+by blast

text{*6*}
lemma "P | ~ P"
-by meson
+by blast

text{*7*}
lemma "P | ~ ~ ~ P"
-by meson
+by blast

text{*8.  Peirce's law*}
lemma "((P-->Q) --> P)  -->  P"
-by meson
+by blast

text{*9*}
lemma "((P|Q) & (~P|Q) & (P| ~Q)) --> ~ (~P | ~Q)"
-by meson
+by blast

text{*10*}
lemma "(Q-->R) & (R-->P&Q) & (P-->Q|R) --> (P=Q)"
-by meson
+by blast

text{*11.  Proved in each direction (incorrectly, says Pelletier!!)  *}
lemma "P=(P::bool)"
-by meson
+by blast

text{*12.  "Dijkstra's law"*}
lemma "((P = Q) = R) = (P = (Q = R))"
-by meson
+by blast

text{*13.  Distributive law*}
lemma "(P | (Q & R)) = ((P | Q) & (P | R))"
-by meson
+by blast

text{*14*}
lemma "(P = Q) = ((Q | ~P) & (~Q|P))"
-by meson
+by blast

text{*15*}
lemma "(P --> Q) = (~P | Q)"
-by meson
+by blast

text{*16*}
lemma "(P-->Q) | (Q-->P)"
-by meson
+by blast

text{*17*}
lemma "((P & (Q-->R))-->S)  =  ((~P | Q | S) & (~P | ~R | S))"
-by meson
+by blast

subsubsection{*Classical Logic: examples with quantifiers*}

lemma "(\<forall>x. P x & Q x) = ((\<forall>x. P x) & (\<forall>x. Q x))"
-by meson
+by blast

lemma "(\<exists>x. P --> Q x)  =  (P --> (\<exists>x. Q x))"
-by meson
+by blast

lemma "(\<exists>x. P x --> Q) = ((\<forall>x. P x) --> Q)"
-by meson
+by blast

lemma "((\<forall>x. P x) | Q)  =  (\<forall>x. P x | Q)"
-by meson
+by blast

lemma "(\<forall>x. P x --> P(f x))  &  P d --> P(f(f(f d)))"
-by meson
+by blast

text{*Needs double instantiation of EXISTS*}
lemma "\<exists>x. P x --> P a & P b"
-by meson
+by blast

lemma "\<exists>z. P z --> (\<forall>x. P x)"
-by meson
+by blast

text{*From a paper by Claire Quigley*}
lemma "\<exists>y. ((P c & Q y) | (\<exists>z. ~ Q z)) | (\<exists>x. ~ P x & Q d)"
@@ -531,34 +533,34 @@

text{*Problem 18*}
lemma "\<exists>y. \<forall>x. P y --> P x"
-by meson
+by blast

text{*Problem 19*}
lemma "\<exists>x. \<forall>y z. (P y --> Q z) --> (P x --> Q x)"
-by meson
+by blast

text{*Problem 20*}
lemma "(\<forall>x y. \<exists>z. \<forall>w. (P x & Q y --> R z & S w))
--> (\<exists>x y. P x & Q y) --> (\<exists>z. R z)"
-by meson
+by blast

text{*Problem 21*}
lemma "(\<exists>x. P --> Q x) & (\<exists>x. Q x --> P) --> (\<exists>x. P=Q x)"
-by meson
+by blast

text{*Problem 22*}
lemma "(\<forall>x. P = Q x)  -->  (P = (\<forall>x. Q x))"
-by meson
+by blast

text{*Problem 23*}
lemma "(\<forall>x. P | Q x)  =  (P | (\<forall>x. Q x))"
-by meson
+by blast

text{*Problem 24*}  (*The first goal clause is useless*)
lemma "~(\<exists>x. S x & Q x) & (\<forall>x. P x --> Q x | R x) &
(~(\<exists>x. P x) --> (\<exists>x. Q x)) & (\<forall>x. Q x | R x --> S x)
--> (\<exists>x. P x & R x)"
-by meson
+by blast

text{*Problem 25*}
lemma "(\<exists>x. P x) &
@@ -566,13 +568,13 @@
(\<forall>x. P x --> (M x & L x)) &
((\<forall>x. P x --> Q x) | (\<exists>x. P x & R x))
--> (\<exists>x. Q x & P x)"
-by meson
+by blast

text{*Problem 26; has 24 Horn clauses*}
lemma "((\<exists>x. p x) = (\<exists>x. q x)) &
(\<forall>x. \<forall>y. p x & q y --> (r x = s y))
--> ((\<forall>x. p x --> r x) = (\<forall>x. q x --> s x))"
-by meson
+by blast

text{*Problem 27; has 13 Horn clauses*}
lemma "(\<exists>x. P x & ~Q x) &
@@ -580,61 +582,61 @@
(\<forall>x. M x & L x --> P x) &
((\<exists>x. R x & ~ Q x) --> (\<forall>x. L x --> ~ R x))
--> (\<forall>x. M x --> ~L x)"
-by meson
+by blast

text{*Problem 28.  AMENDED; has 14 Horn clauses*}
lemma "(\<forall>x. P x --> (\<forall>x. Q x)) &
((\<forall>x. Q x | R x) --> (\<exists>x. Q x & S x)) &
((\<exists>x. S x) --> (\<forall>x. L x --> M x))
--> (\<forall>x. P x & L x --> M x)"
-by meson
+by blast

text{*Problem 29.  Essentially the same as Principia Mathematica *11.71.
62 Horn clauses*}
lemma "(\<exists>x. F x) & (\<exists>y. G y)
--> ( ((\<forall>x. F x --> H x) & (\<forall>y. G y --> J y))  =
(\<forall>x y. F x & G y --> H x & J y))"
-by meson
+by blast

text{*Problem 30*}
lemma "(\<forall>x. P x | Q x --> ~ R x) & (\<forall>x. (Q x --> ~ S x) --> P x & R x)
--> (\<forall>x. S x)"
-by meson
+by blast

text{*Problem 31; has 10 Horn clauses; first negative clauses is useless*}
lemma "~(\<exists>x. P x & (Q x | R x)) &
(\<exists>x. L x & P x) &
(\<forall>x. ~ R x --> M x)
--> (\<exists>x. L x & M x)"
-by meson
+by blast

text{*Problem 32*}
lemma "(\<forall>x. P x & (Q x | R x)-->S x) &
(\<forall>x. S x & R x --> L x) &
(\<forall>x. M x --> R x)
--> (\<forall>x. P x & M x --> L x)"
-by meson
+by blast

text{*Problem 33; has 55 Horn clauses*}
lemma "(\<forall>x. P a & (P x --> P b)-->P c)  =
(\<forall>x. (~P a | P x | P c) & (~P a | ~P b | P c))"
-by meson
+by blast

text{*Problem 34: Andrews's challenge has 924 Horn clauses*}
lemma "((\<exists>x. \<forall>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 meson
+by blast

text{*Problem 35*}
lemma "\<exists>x y. P x y -->  (\<forall>u v. P u v)"
-by meson
+by blast

text{*Problem 36; has 15 Horn clauses*}
lemma "(\<forall>x. \<exists>y. J x y) & (\<forall>x. \<exists>y. G x y) &
(\<forall>x y. J x y | G x y --> (\<forall>z. J y z | G y z --> H x z))
--> (\<forall>x. \<exists>y. H x y)"
-by meson
+by blast

text{*Problem 37; has 10 Horn clauses*}
lemma "(\<forall>z. \<exists>w. \<forall>x. \<exists>y.
@@ -642,7 +644,7 @@
(\<forall>x z. ~P x z --> (\<exists>y. Q y z)) &
((\<exists>x y. Q x y) --> (\<forall>x. R x x))
--> (\<forall>x. \<exists>y. R x y)"
-by meson --{*causes unification tracing messages*}
+by blast --{*causes unification tracing messages*}

text{*Problem 38*}  text{*Quite hard: 422 Horn clauses!!*}
@@ -651,36 +653,36 @@
(\<forall>x. (~p a | p x | (\<exists>z. \<exists>w. p z & r x w & r w z)) &
(~p a | ~(\<exists>y. p y & r x y) |
(\<exists>z. \<exists>w. p z & r x w & r w z)))"
-by meson
+by blast

text{*Problem 39*}
lemma "~ (\<exists>x. \<forall>y. F y x = (~F y y))"
-by meson
+by blast

text{*Problem 40.  AMENDED*}
lemma "(\<exists>y. \<forall>x. F x y = F x x)
-->  ~ (\<forall>x. \<exists>y. \<forall>z. F z y = (~F z x))"
-by meson
+by blast

text{*Problem 41*}
lemma "(\<forall>z. (\<exists>y. (\<forall>x. f x y = (f x z & ~ f x x))))
--> ~ (\<exists>z. \<forall>x. f x z)"
-by meson
+by blast

text{*Problem 42*}
lemma "~ (\<exists>y. \<forall>x. p x y = (~ (\<exists>z. p x z & p z x)))"
-by meson
+by blast

text{*Problem 43  NOW PROVED AUTOMATICALLY!!*}
lemma "(\<forall>x. \<forall>y. q x y = (\<forall>z. p z x = (p z y::bool)))
--> (\<forall>x. (\<forall>y. q x y = (q y x::bool)))"
-by meson
+by blast

text{*Problem 44: 13 Horn clauses; 7-step proof*}
lemma "(\<forall>x. f x --> (\<exists>y. g y & h x y & (\<exists>y. g y & ~ h x y)))  &
(\<exists>x. j x & (\<forall>y. g y --> h x y))
--> (\<exists>x. j x & ~f x)"
-by meson
+by blast

text{*Problem 45; has 27 Horn clauses; 54-step proof*}
lemma "(\<forall>x. f x & (\<forall>y. g y & h x y --> j x y)
@@ -689,7 +691,7 @@
(\<exists>x. f x & (\<forall>y. h x y --> l y)
& (\<forall>y. g y & h x y --> j x y))
--> (\<exists>x. f x & ~ (\<exists>y. g y & h x y))"
-by meson
+by blast

text{*Problem 46; has 26 Horn clauses; 21-step proof*}
lemma "(\<forall>x. f x & (\<forall>y. f y & h y x --> g y) --> g x) &
@@ -697,7 +699,7 @@
(\<exists>x. f x & ~g x & (\<forall>y. f y & ~g y --> j x y))) &
(\<forall>x y. f x & f y & h x y --> ~j y x)
--> (\<forall>x. f x --> g x)"
-by meson
+by blast

text{*Problem 47.  Schubert's Steamroller*}
text{*26 clauses; 63 Horn clauses
@@ -741,11 +743,12 @@

text{*Problem 50.  What has this to do with equality?*}
lemma "(\<forall>x. P a x | (\<forall>y. P x y)) --> (\<exists>x. \<forall>y. P x y)"
-by meson
+by blast

text{*Problem 54: NOT PROVED*}
lemma "(\<forall>y::'a. \<exists>z. \<forall>x. F x z = (x=y)) -->
-      ~ (\<exists>w. \<forall>x. F x w = (\<forall>u. F x u --> (\<exists>y. F y u & ~ (\<exists>z. F z u & F z y))))"oops
+      ~ (\<exists>w. \<forall>x. F x w = (\<forall>u. F x u --> (\<exists>y. F y u & ~ (\<exists>z. F z u & F z y))))"
+oops

text{*Problem 55*}
@@ -766,25 +769,50 @@
text{*Problem 57*}
lemma "P (f a b) (f b c) & P (f b c) (f a c) &
(\<forall>x y z. P x y & P y z --> P x z)    -->   P (f a b) (f a c)"
-by meson
+by blast

text{*Problem 58: Challenge found on info-hol *}
lemma "\<forall>P Q R x. \<exists>v w. \<forall>y z. P x & Q y --> (P v | R w) & (R z --> Q v)"
-by meson
+by blast

text{*Problem 59*}
lemma "(\<forall>x. P x = (~P(f x))) --> (\<exists>x. P x & ~P(f x))"
-by meson
+by blast

text{*Problem 60*}
lemma "\<forall>x. P x (f x) = (\<exists>y. (\<forall>z. P z y --> P z (f x)) & P x y)"
-by meson
+by blast

text{*Problem 62 as corrected in JAR 18 (1997), page 135*}
lemma "(\<forall>x. p a & (p x --> p(f x)) --> p(f(f x)))  =
(\<forall>x. (~ p a | p x | p(f(f x))) &
(~ p a | ~ p(f x) | p(f(f x))))"
-by meson
+by blast
+
+text{** Charles Morgan's problems **}
+
+lemma
+  assumes a: "\<forall>x y.  T(i x(i y x))"
+      and b: "\<forall>x y z. T(i (i x (i y z)) (i (i x y) (i x z)))"
+      and c: "\<forall>x y.   T(i (i (n x) (n y)) (i y x))"
+      and c': "\<forall>x y.   T(i (i y x) (i (n x) (n y)))"
+      and d: "\<forall>x y.   T(i x y) & T x --> T y"
+ shows True
+proof -
+  from a b d have "\<forall>x. T(i x x)" by blast
+  from a b c d have "\<forall>x. T(i x (n(n x)))" --{*Problem 66*}
+    by meson
+      --{*SLOW: 18s on griffon. 208346 inferences, depth 23 *}
+  from a b c d have "\<forall>x. T(i (n(n x)) x)" --{*Problem 67*}
+    by meson
+      --{*4.9s on griffon. 51061 inferences, depth 21 *}
+  from a b c' d have "\<forall>x. T(i x (n(n x)))"
+      --{*Problem 68: not proved.  Listed as satisfiable in TPTP (LCL078-1)*}
+oops
+
+text{*Problem 71, as found in TPTP (SYN007+1.005)*}
+lemma "p1 = (p2 = (p3 = (p4 = (p5 = (p1 = (p2 = (p3 = (p4 = p5))))))))"
+by blast

text{*A manual resolution proof of problem 19.*}
lemma "\<exists>x. \<forall>y z. (P(y)-->Q(z)) --> (P(x)-->Q(x))"```
```--- a/src/HOL/ex/mesontest2.ML	Thu May 19 18:07:05 2005 +0200
+++ b/src/HOL/ex/mesontest2.ML	Fri May 20 18:34:14 2005 +0200
@@ -139,36 +139,6 @@
(*Restore variable name preservation*)
Logic.auto_rename := false;

-
-(** Charles Morgan's problems **)
-
-val axa = "\\<forall>x y.   T(i x(i y x))";
-val axb = "\\<forall>x y z. T(i(i x(i y z))(i(i x y)(i x z)))";
-val axc = "\\<forall>x y.   T(i(i(n x)(n y))(i y x))";
-val axd = "\\<forall>x y.   T(i x y) & T x --> T y";
-
-fun axjoin ([],   q) = q
-  | axjoin (p::ps, q) = "(" ^ p ^ ") --> (" ^ axjoin(ps,q) ^ ")";
-
-Goal (axjoin([axa,axb,axd], "\\<forall>x. T(i x x)"));
-by (meson_tac 1);
-result();
-
-writeln"Problem 66";
-Goal (axjoin([axa,axb,axc,axd], "\\<forall>x. T(i x(n(n x)))"));
-by (meson_tac 1);
-result();
-(*SLOW: 17s on griffon
-     208346 inferences so far.  Searching to depth 23 *)
-
-writeln"Problem 67";
-Goal (axjoin([axa,axb,axc,axd], "\\<forall>x. T(i(n(n x)) x)"));
-by (meson_tac 1);
-result();
-(*10s on a 1.8MHz machine
-  51061 inferences so far.  Searching to depth 21 *)
-
-
(*MORE and MUCH HARDER test data for the MESON proof procedure

Courtesy John Harrison ```