# HG changeset patch
# User paulson
# Date 1124284200 -7200
# Node ID 7e3828a6ebccf05409872dc75dd025bd6c255f47
# Parent  16971afe75f6bf94e8c40bf3b1bb3d0bb3ede4e1
new examples

diff -r 16971afe75f6 -r 7e3828a6ebcc src/ZF/ex/misc.thy
--- a/src/ZF/ex/misc.thy	Wed Aug 17 14:19:17 2005 +0200
+++ b/src/ZF/ex/misc.thy	Wed Aug 17 15:10:00 2005 +0200
@@ -10,8 +10,27 @@
 
 theory misc imports Main begin
 
+
 subsection{*Various Small Problems*}
 
+text{*The singleton problems are much harder in HOL.*}
+lemma singleton_example_1:
+     "\<forall>x \<in> S. \<forall>y \<in> S. x \<subseteq> y \<Longrightarrow> \<exists>z. S \<subseteq> {z}"
+  by blast
+
+lemma singleton_example_2:
+     "\<forall>x \<in> S. \<Union>S \<subseteq> x \<Longrightarrow> \<exists>z. S \<subseteq> {z}"
+  -- {*Variant of the problem above. *}
+  by blast
+
+lemma "\<exists>!x. f (g(x)) = x \<Longrightarrow> \<exists>!y. g (f(y)) = y"
+  -- {* A unique fixpoint theorem --- @{text fast}/@{text best}/@{text auto} all fail. *} 
+  apply (erule ex1E, rule ex1I, erule subst_context)
+  apply (rule subst, assumption, erule allE, rule subst_context, erule mp)
+  apply (erule subst_context)
+  done
+
+
 text{*A weird property of ordered pairs.*}
 lemma "b\<noteq>c ==> <a,b> Int <a,c> = <a,a>"
 by (simp add: Pair_def Int_cons_left Int_cons_right doubleton_eq_iff, blast)