# HG changeset patch
# User paulson
# Date 1182875573 -7200
# Node ID 702e27cabe82b2bb68b755e2eb8d7856bf36cc29
# Parent  13a9f54175ad0e7812553019ef65b4ca95a6eaa1
updated for metis method

diff -r 13a9f54175ad -r 702e27cabe82 src/HOL/ex/Classical.thy
--- a/src/HOL/ex/Classical.thy	Tue Jun 26 18:32:24 2007 +0200
+++ b/src/HOL/ex/Classical.thy	Tue Jun 26 18:32:53 2007 +0200
@@ -329,10 +329,7 @@
   the type constraint ensures that x,y,z have the same type as a,b,u. *}
 lemma "(\<exists>x y::'a. \<forall>z. z=x | z=y) & P(a) & P(b) & (~a=b)
                 --> (\<forall>u::'a. P(u))"
-apply safe
-apply (rule_tac x = a in allE, assumption)
-apply (rule_tac x = b in allE, assumption, fast)  --{*blast's treatment of equality can't do it*}
-done
+by metis
 
 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)"
@@ -807,8 +804,7 @@
 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 *}
+    by metis
   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 *}
@@ -820,125 +816,4 @@
 lemma "p1 = (p2 = (p3 = (p4 = (p5 = (p1 = (p2 = (p3 = (p4 = p5))))))))"
 by blast
 
-
-subsection{*Examples of proof reconstruction*}
-
-text{*A manual resolution proof of problem 19.*}
-lemma "\<exists>x. \<forall>y z. (P(y)-->Q(z)) --> (P(x)-->Q(x))"
-proof (neg_clausify)
-  fix x
-  assume P: "\<And>U. P U" 
-     and Q: "\<And>U. ~ Q U"
-     and PQ: "~ P x | Q x"
-  have 1: "\<And>U. Q x"
-    by (meson P PQ)
-  show "False"
-    by (meson Q 1)
-qed
-
-
-text{*A lengthy proof of a significant theorem: @{text singleton_example_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 (neg_clausify)
-  fix S :: "'a set set"
-  assume 1: "\<And>Z. ~ (S \<subseteq> {Z})"
-     and 2: "\<And>X Y. X \<notin> S | Y \<notin> S | X \<subseteq> Y"
-  have 10: "!!U V. U \<notin> S | V \<notin> S | ~ V \<subseteq> U | V = U"
-    by (meson equalityI 2) 
-  have 11: "!!U V. U \<notin> S | V \<notin> S | V = U"
-    by (meson 10 2) 
-  have 13: "!!U V. U \<notin> S | S \<subseteq> V | U = sko_Set_XsubsetI_1_ S V"
-    by (meson subsetI 11)
-  have 14: "!!U V. S \<subseteq> U | S \<subseteq> V | sko_Set_XsubsetI_1_ S U = sko_Set_XsubsetI_1_ S V"
-    by (meson subsetI 13)
-  have 29: "!!U V. S \<subseteq> U |  sko_Set_XsubsetI_1_ S U = sko_Set_XsubsetI_1_ S {V}"
-    by (meson 1 14)
-  have 58: "!!U V. sko_Set_XsubsetI_1_ S {U} = sko_Set_XsubsetI_1_ S {V}"
-    by (meson 1 29)
-    (*hacked here while we wait for Metis: !!U V complicates proofs.*)
-  have 82: "sko_Set_XsubsetI_1_ S {U} \<notin> {V} | S \<subseteq> {V}"
-    apply (insert 58 [of U V], erule ssubst)
-    by (meson 58 subsetI)
-  have 85: "sko_Set_XsubsetI_1_ S {U} \<notin> {V}"
-    by (meson 1 82)
-  show False
-    by (meson insertI1 85)
-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 (neg_clausify)
-  fix S :: "'a set set"
-  assume 1: "\<And>Z. ~ (S \<subseteq> {Z})"
-     and 2: "\<And>X Y. X \<notin> S | Y \<notin> S | X \<subseteq> Y"
-  have 13: "!!U V. U \<notin> S | S \<subseteq> V | U = sko_Set_XsubsetI_1_ S V"
-    by (meson subsetI equalityI 2)
-  have 58: "!!U V. sko_Set_XsubsetI_1_ S {U} = sko_Set_XsubsetI_1_ S {V}"
-    by (meson 1 subsetI 13)
-    (*hacked here while we wait for Metis: !!U V complicates proofs.*)
-  have 82: "sko_Set_XsubsetI_1_ S {U} \<notin> {V} | S \<subseteq> {V}"
-    apply (insert 58 [of U V], erule ssubst)
-    by (meson 58 subsetI)
-  show False
-    by (meson insertI1 1 82)
-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 (neg_clausify)
-  fix S :: "'a set set"
-  assume 1: "\<And>Z. ~ (S \<subseteq> {Z})"
-     and 2: "\<And>X Y. X \<notin> S | Y \<notin> S | X \<subseteq> Y"
-  have 58: "!!U V. sko_Set_XsubsetI_1_ S {U} = sko_Set_XsubsetI_1_ S {V}"
-    by (meson 1 subsetI_0 equalityI 2)
-  show False
-    by (iprover intro: subsetI_1 insertI1 1 58 elim: ssubst)  
-qed
-***)
-
-(*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)*.
-2[0:Inp] ||  -> c_lessequals(U,V,tc_set(W)) c_in(c_Main_OsubsetI__1(U,V,W),U,W)*
-.
-3[0:Inp] || c_in(c_Main_OsubsetI__1(U,V,W),V,W)* -> c_lessequals(U,V,tc_set(W)).
-
-4[0:Inp] || c_lessequals(U,V,tc_set(W))* c_lessequals(V,U,tc_set(W))* -> equal(U
-,V).
-
-5[0:Inp] || c_lessequals(v_S,c_insert(U,c_emptyset,tc_set(t_a)),tc_set(tc_set(t_
-a)))* -> .
-
-6[0:Inp] || c_in(U,v_S,tc_set(t_a)) c_in(V,v_S,tc_set(t_a)) -> c_lessequals(U,V,
-tc_set(t_a))*.
-10[0:Res:6.2,4.1] || c_in(U,v_S,tc_set(t_a)) c_in(V,v_S,tc_set(t_a)) c_lessequal
-s(V,U,tc_set(t_a))* -> equal(V,U).
-11[0:MRR:10.2,6.2] || c_in(U,v_S,tc_set(t_a))*+ c_in(V,v_S,tc_set(t_a))* -> equa
-l(V,U)*.
-13[0:Res:2.1,11.0] || c_in(U,v_S,tc_set(t_a))*+ -> c_lessequals(v_S,V,tc_set(tc_set(t_a)))* equal(U,c_Main_OsubsetI__1(v_S,V,tc_set(t_a)))*.
-
-14[0:Res:2.1,13.0] ||  -> c_lessequals(v_S,U,tc_set(tc_set(t_a)))* c_lessequals(
-v_S,V,tc_set(tc_set(t_a)))* equal(c_Main_OsubsetI__1(v_S,U,tc_set(t_a)),c_Main_OsubsetI__1(v_S,V,tc_set(t_a)))*.
-
-29[0:Res:14.1,5.0] ||  -> c_lessequals(v_S,U,tc_set(tc_set(t_a)))* equal(c_Main_
-OsubsetI__1(v_S,U,tc_set(t_a)),c_Main_OsubsetI__1(v_S,c_insert(V,c_emptyset,tc_s
-et(t_a)),tc_set(t_a)))*.
-58[0:Res:29.0,5.0] ||  -> equal(c_Main_OsubsetI__1(v_S,c_insert(U,c_emptyset,tc_
-set(t_a)),tc_set(t_a)),c_Main_OsubsetI__1(v_S,c_insert(V,c_emptyset,tc_set(t_a))
-,tc_set(t_a)))*.
-
-82[0:SpL:58.0,3.0] || c_in(c_Main_OsubsetI__1(v_S,c_insert(U,c_emptyset,tc_set(t_a)),tc_set(t_a)),c_insert(V,c_emptyset,tc_set(t_a)),tc_set(t_a))* -> c_lessequals(v_S,c_insert(V,c_emptyset,tc_set(t_a)),tc_set(tc_set(t_a))).
-
-85[0:MRR:82.1,5.0] || c_in(c_Main_OsubsetI__1(v_S,c_insert(U,c_emptyset,tc_set(t
-_a)),tc_set(t_a)),c_insert(V,c_emptyset,tc_set(t_a)),tc_set(t_a))* -> .
-
-86[0:UnC:85.0,1.0] ||  -> .
-Formulae used in the proof :
-*)
-
 end