author wenzelm Tue, 01 Aug 2017 17:30:02 +0200 changeset 66303 210dae34b8bc parent 66302 fd89f97c80c2 child 66304 cde6ceffcbc7
misc tuning and modernization;
 src/HOL/ex/Classical.thy file | annotate | diff | comparison | revisions
```--- a/src/HOL/ex/Classical.thy	Tue Aug 01 10:28:42 2017 +0200
+++ b/src/HOL/ex/Classical.thy	Tue Aug 01 17:30:02 2017 +0200
@@ -790,28 +790,32 @@
(~ p a | ~ p(f x) | p(f(f x))))"
by blast

-text\<open>* Charles Morgan's problems *\<close>
+text\<open>Charles Morgan's problems\<close>
+context
+  fixes T i n
+  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"
+begin

-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)))" \<comment>\<open>Problem 66\<close>
-    by metis
-  from a b c d have "\<forall>x. T(i (n(n x)) x)" \<comment>\<open>Problem 67\<close>
-    by meson
-      \<comment>\<open>4.9s on griffon. 51061 inferences, depth 21\<close>
-  from a b c' d have "\<forall>x. T(i x (n(n x)))"
-      \<comment>\<open>Problem 68: not proved.  Listed as satisfiable in TPTP (LCL078-1)\<close>
-oops
+lemma "\<forall>x. T(i x x)"
+  using a b d by blast
+
+lemma "\<forall>x. T(i x (n(n x)))" \<comment>\<open>Problem 66\<close>
+  using a b c d by metis
+
+lemma "\<forall>x. T(i (n(n x)) x)" \<comment>\<open>Problem 67\<close>
+  using a b c d by meson \<comment>\<open>4.9s on griffon. 51061 inferences, depth 21\<close>
+
+lemma "\<forall>x. T(i x (n(n x)))" \<comment>\<open>Problem 68: not proved.  Listed as satisfiable in TPTP (LCL078-1)\<close>
+  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
+  by blast

end```