# HG changeset patch
# User paulson
# Date 1166817655 -3600
# Node ID 07d2a81f69c87c19b81262822eb5a91cc5fcd97b
# Parent  f386d7eb17d15c84e20e7309d604739fc26b76b1
revised for new make_clauses

diff -r f386d7eb17d1 -r 07d2a81f69c8 src/HOL/ex/Classical.thy
--- a/src/HOL/ex/Classical.thy	Fri Dec 22 21:00:42 2006 +0100
+++ b/src/HOL/ex/Classical.thy	Fri Dec 22 21:00:55 2006 +0100
@@ -827,10 +827,10 @@
 lemma "\<exists>x. \<forall>y z. (P(y)-->Q(z)) --> (P(x)-->Q(x))"
 proof (rule ccontr, skolemize, make_clauses)
   fix x
-  assume P: "\<And>U. \<not> P U \<Longrightarrow> False" 
-     and Q: "\<And>U. Q U \<Longrightarrow> False"
-     and PQ: "\<lbrakk>P x; \<not> Q x\<rbrakk> \<Longrightarrow> False"
-  have cl4: "\<And>U. \<not> Q x \<Longrightarrow> False"
+  assume P: "\<And>U. P U" 
+     and Q: "\<And>U. ~ Q U"
+     and PQ: "~ P x | Q x"
+  have cl4: "\<And>U. Q x"
     by (meson P PQ)
   show "False"
     by (meson Q cl4)
@@ -846,23 +846,24 @@
 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"
+  assume CL1: "\<And>Z. ~ (S \<subseteq> {Z})"
+     and CL2: "\<And>X Y. X \<notin> S | Y \<notin> S | X \<subseteq> Y"
+  have CL10: "!!U V. U \<notin> S | V \<notin> S | ~ V \<subseteq> U | V = U"
     by (meson equalityI CL2) 
-  have CL11: "!!U V. \<lbrakk>U \<in> S; V \<in> S; V \<noteq> U\<rbrakk> \<Longrightarrow> False"
+  have CL11: "!!U V. U \<notin> S | V \<notin> S | V = U"
     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"
+  have CL13: "!!U V. U \<notin> S | S \<subseteq> V | U = Set_XsubsetI_sko1_ S V"
     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"
+  have CL14: "!!U V. S \<subseteq> U | S \<subseteq> V | Set_XsubsetI_sko1_ S U = Set_XsubsetI_sko1_ S V"
     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"
+  have CL29: "!!U V. S \<subseteq> U |  Set_XsubsetI_sko1_ S U = Set_XsubsetI_sko1_ S {V}"
     by (meson CL1 CL14)
-  have CL58: "!!U V. \<lbrakk>Set_XsubsetI_sko1_ S {U} \<noteq> Set_XsubsetI_sko1_ S {V}\<rbrakk> \<Longrightarrow> False"
+  have CL58: "!!U V. Set_XsubsetI_sko1_ S {U} = Set_XsubsetI_sko1_ S {V}"
     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"
+    (*hacked here while we wait for Metis: !!U V complicates proofs.*)
+  have CL82: "Set_XsubsetI_sko1_ S {U} \<notin> {V} | S \<subseteq> {V}"
+    by (insert CL58 subsetI_1 [of S "{V}"], force) 
+  have CL85: "Set_XsubsetI_sko1_ S {U} \<notin> {V}"
     by (meson CL1 CL82)
   show False
     by (meson insertI1 CL85)
@@ -873,30 +874,32 @@
      "\<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 CL13: "!!U V. \<lbrakk>U \<in> S; ~ (S \<subseteq> V); U \<noteq> Set_XsubsetI_sko1_ S V\<rbrakk> \<Longrightarrow> False"
+  assume CL1: "\<And>Z. ~ (S \<subseteq> {Z})"
+     and CL2: "\<And>X Y. X \<notin> S | Y \<notin> S | X \<subseteq> Y"
+  have CL13: "!!U V. U \<notin> S | S \<subseteq> V | U = Set_XsubsetI_sko1_ S V"
     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"
+  have CL58: "!!U V. Set_XsubsetI_sko1_ S {U} = Set_XsubsetI_sko1_ S {V}"
     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)
+    (*hacked here while we wait for Metis: !!U V complicates proofs.*)
+  have CL82: "Set_XsubsetI_sko1_ S {U} \<notin> {V} | S \<subseteq> {V}"
+    by (insert CL58 subsetI_1 [of S "{V}"], force)
   show False
     by (meson insertI1 CL1 CL82)
 qed
 
+(**Not working: needs Metis
 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"
+  assume CL1: "\<And>Z. ~ (S \<subseteq> {Z})"
+     and CL2: "\<And>X Y. X \<notin> S | Y \<notin> S | X \<subseteq> Y"
+  have CL58: "!!U V. Set_XsubsetI_sko1_ S {U} = Set_XsubsetI_sko1_ S {V}"
     by (meson CL1 subsetI_0 equalityI CL2)
   show False
-    by (iprover intro: subsetI_1 insertI1 CL1 CL58 elim: ssubst)
+    by (iprover intro: subsetI_1 insertI1 CL1 CL58 elim: ssubst)  
 qed
-
+***)
 
 (*These are based on the following SPASS proof: