# HG changeset patch
# User paulson
# Date 1161595130 -7200
# Node ID 5a59f8ff96cc854006af52e7e948075b13a53544
# Parent  8f3dffd52db227b9b328418d8e2150ea9fa09ccf
new single-step proofs

diff -r 8f3dffd52db2 -r 5a59f8ff96cc src/HOL/ex/Classical.thy
--- a/src/HOL/ex/Classical.thy	Mon Oct 23 11:18:25 2006 +0200
+++ b/src/HOL/ex/Classical.thy	Mon Oct 23 11:18:50 2006 +0200
@@ -837,39 +837,68 @@
 qed
 
 
-text{*A lengthy proof of a significant theorem.*}
+text{*A lengthy proof of a significant theorem: @{text singleton_example_1}*}
 
 lemmas subsetI_0 = subsetI[skolem, clausify 0]
 lemmas subsetI_1 = subsetI[skolem, clausify 1]
 
+text{*Full single-step proof*}
+lemma "\<And>S::'a set set. \<forall>x \<in> S. \<forall>y \<in> S. x \<subseteq> y \<Longrightarrow> \<exists>z. S \<subseteq> {z}"
+proof (rule ccontr, skolemize, make_clauses)
+  fix S :: "'a set set"
+  assume CL1: "\<And>Z. S \<subseteq> {Z} \<Longrightarrow> False"
+     and CL2: "\<And>X Y. \<lbrakk>X \<in> S; Y \<in> S; \<not> X \<subseteq> Y\<rbrakk> \<Longrightarrow> False"
+  have CL10: "!!U V. \<lbrakk>U \<in> S; V \<in> S; V \<subseteq> U; V \<noteq> U\<rbrakk> \<Longrightarrow> False"
+    by (meson equalityI CL2) 
+  have CL11: "!!U V. \<lbrakk>U \<in> S; V \<in> S; V \<noteq> U\<rbrakk> \<Longrightarrow> False"
+    by (meson CL10 CL2) 
+  have CL13: "!!U V. \<lbrakk>U \<in> S; ~ (S \<subseteq> V); U \<noteq> Set_XsubsetI_sko1_ S V\<rbrakk> \<Longrightarrow> False"
+    by (meson subsetI_0 CL11)
+  have CL14: "!!U V. \<lbrakk>~ (S \<subseteq> U); ~(S \<subseteq> V); Set_XsubsetI_sko1_ S U \<noteq> Set_XsubsetI_sko1_ S V\<rbrakk> \<Longrightarrow> False"
+    by (meson subsetI_0 CL13)
+  have CL29: "!!U V. \<lbrakk>~ (S \<subseteq> U);  Set_XsubsetI_sko1_ S U \<noteq> Set_XsubsetI_sko1_ S {V}\<rbrakk> \<Longrightarrow> False"
+    by (meson CL1 CL14)
+  have CL58: "!!U V. \<lbrakk>Set_XsubsetI_sko1_ S {U} \<noteq> Set_XsubsetI_sko1_ S {V}\<rbrakk> \<Longrightarrow> False"
+    by (meson CL1 CL29)
+  have CL82: "!!U V. \<lbrakk>Set_XsubsetI_sko1_ S {U} \<in> {V}; ~ (S \<subseteq> {V})\<rbrakk> \<Longrightarrow> False"
+    by (iprover intro: subsetI_1 CL58 elim: ssubst)
+  have CL85: "!!U V. \<lbrakk>Set_XsubsetI_sko1_ S {U} \<in> {V}\<rbrakk> \<Longrightarrow> False"
+    by (meson CL1 CL82)
+  show False
+    by (meson insertI1 CL85)
+qed
+
+text{*Partially condensed proof*}
 lemma singleton_example_1:
      "\<And>S::'a set set. \<forall>x \<in> S. \<forall>y \<in> S. x \<subseteq> y \<Longrightarrow> \<exists>z. S \<subseteq> {z}"
 proof (rule ccontr, skolemize, make_clauses)
   fix S :: "'a set set"
   assume CL1: "\<And>Z. S \<subseteq> {Z} \<Longrightarrow> False"
      and CL2: "\<And>X Y. \<lbrakk>X \<in> S; Y \<in> S; \<not> X \<subseteq> Y\<rbrakk> \<Longrightarrow> False"
-  have CL10: "!!U V. [|U \<in> S; V \<in> S; V \<subseteq> U; V \<noteq> U|] ==> False"
-    by (iprover intro: equalityI CL2) 
-  have CL11: "!!U V. [|U \<in> S; V \<in> S; V \<noteq> U|] ==> False"
-    by (iprover intro: CL10 CL2) 
-  have CL13: "!!U V. [|U \<in> S; ~ (S \<subseteq> V); U \<noteq> Set_XsubsetI_sko1_ S V|] ==> False"
-    by (iprover intro: subsetI_0 CL11)
-  have CL14: "!!U V. [|~ (S \<subseteq> U); ~(S \<subseteq> V); Set_XsubsetI_sko1_ S U \<noteq> Set_XsubsetI_sko1_ S V|] ==> False"
-    by (iprover intro: subsetI_0 CL13)
-  have CL29: "!!U V. [|~ (S \<subseteq> U);  Set_XsubsetI_sko1_ S U \<noteq> Set_XsubsetI_sko1_ S {V}|] ==> False"
-    by (iprover intro: CL1 CL14)
-  have CL58: "!!U V. [| Set_XsubsetI_sko1_ S {U} \<noteq> Set_XsubsetI_sko1_ S {V}|] ==> False"
-    by (iprover intro: CL1 CL29)
-  have CL82: "!!U V. [| Set_XsubsetI_sko1_ S {U} \<in> {V}; ~ (S \<subseteq> {V})|] ==> False"
+  have CL13: "!!U V. \<lbrakk>U \<in> S; ~ (S \<subseteq> V); U \<noteq> Set_XsubsetI_sko1_ S V\<rbrakk> \<Longrightarrow> False"
+    by (meson subsetI_0 equalityI CL2)
+  have CL58: "!!U V. \<lbrakk>Set_XsubsetI_sko1_ S {U} \<noteq> Set_XsubsetI_sko1_ S {V}\<rbrakk> \<Longrightarrow> False"
+    by (meson CL1 subsetI_0 CL13)
+  have CL82: "!!U V. \<lbrakk>Set_XsubsetI_sko1_ S {U} \<in> {V}; ~ (S \<subseteq> {V})\<rbrakk> \<Longrightarrow> False"
     by (iprover intro: subsetI_1 CL58 elim: ssubst)
-  have CL85: "!!U V. [| Set_XsubsetI_sko1_ S {U} \<in> {V}|] ==> False"
-    by (blast intro: CL1 CL82)
   show False
-    by (iprover intro: insertI1 CL85)
+    by (meson insertI1 CL1 CL82)
+qed
+
+text{*More condensed proof*}
+lemma "\<And>S::'a set set. \<forall>x \<in> S. \<forall>y \<in> S. x \<subseteq> y \<Longrightarrow> \<exists>z. S \<subseteq> {z}"
+proof (rule ccontr, skolemize, make_clauses)
+  fix S :: "'a set set"
+  assume CL1: "\<And>Z. S \<subseteq> {Z} \<Longrightarrow> False"
+     and CL2: "\<And>X Y. \<lbrakk>X \<in> S; Y \<in> S; \<not> X \<subseteq> Y\<rbrakk> \<Longrightarrow> False"
+  have CL58: "!!U V. \<lbrakk>Set_XsubsetI_sko1_ S {U} \<noteq> Set_XsubsetI_sko1_ S {V}\<rbrakk> \<Longrightarrow> False"
+    by (meson CL1 subsetI_0 equalityI CL2)
+  show False
+    by (iprover intro: subsetI_1 insertI1 CL1 CL58 elim: ssubst)
 qed
 
 
-(*Based on this SPASS proof:
+(*These are based on the following SPASS proof:
 
 Here is a proof with depth 6, length 15 :
 1[0:Inp] ||  -> c_in(U,c_insert(U,V,W),W)*.