# HG changeset patch
# User paulson
# Date 1121871680 -7200
# Node ID 543ee8fabe1a14a091e11d42a1ae5bc9edfecbb8
# Parent  7e5319d0f41854242fc2c4e3bff44a68b64a74d7
revised examples

diff -r 7e5319d0f418 -r 543ee8fabe1a src/HOL/ex/set.thy
--- a/src/HOL/ex/set.thy	Wed Jul 20 17:00:28 2005 +0200
+++ b/src/HOL/ex/set.thy	Wed Jul 20 17:01:20 2005 +0200
@@ -40,14 +40,19 @@
   -- {* Inter-image, called @{text Int_Inter_image} in Main HOL *}
   by blast
 
-lemma "\<And>S::'a set set. \<forall>x \<in> S. \<forall>y \<in> S. x \<subseteq> y \<Longrightarrow> \<exists>z. S \<subseteq> {z}"
-  -- {* Singleton I.  Nice demonstration of @{text blast}--and its limitations. *}
-  -- {* For some unfathomable reason, @{text UNIV_I} increases the search space greatly. *}
-  by (blast del: UNIV_I)
+text{*Both of the singleton examples can be proved very quickly by @{text
+"blast del: UNIV_I"} but not by @{text blast} alone.  For some reason, @{text
+UNIV_I} greatly increases the search space.*}
 
-lemma "\<forall>x \<in> S. \<Union>S \<subseteq> x \<Longrightarrow> \<exists>z. S \<subseteq> {z}"
-  -- {*Singleton II.  Variant of the benchmark above. *}
-  by (blast del: UNIV_I)
+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}"
+  by (meson subsetI subset_antisym insertCI)
+
+lemma singleton_example_2:
+     "\<forall>x \<in> S. \<Union>S \<subseteq> x \<Longrightarrow> \<exists>z. S \<subseteq> {z}"
+  -- {*Variant of the problem above. *}
+by (meson subsetI subset_antisym insertCI UnionI) 
+
 
 lemma "\<exists>!x. f (g x) = x \<Longrightarrow> \<exists>!y. g (f y) = y"
   -- {* A unique fixpoint theorem --- @{text fast}/@{text best}/@{text meson} all fail. *}