src/HOL/ex/set.thy
changeset 24573 5bbdc9b60648
parent 19982 e4d50f8f3722
child 24853 aab5798e5a33
     1.1 --- a/src/HOL/ex/set.thy	Fri Sep 14 13:32:07 2007 +0200
     1.2 +++ b/src/HOL/ex/set.thy	Fri Sep 14 15:27:12 2007 +0200
     1.3 @@ -43,26 +43,15 @@
     1.4  lemma singleton_example_1:
     1.5       "\<And>S::'a set set. \<forall>x \<in> S. \<forall>y \<in> S. x \<subseteq> y \<Longrightarrow> \<exists>z. S \<subseteq> {z}"
     1.6    by blast
     1.7 -(*With removal of negated equality literals, this no longer works:
     1.8 -  by (meson subsetI subset_antisym insertCI)
     1.9 -*)
    1.10  
    1.11  lemma singleton_example_2:
    1.12       "\<forall>x \<in> S. \<Union>S \<subseteq> x \<Longrightarrow> \<exists>z. S \<subseteq> {z}"
    1.13    -- {*Variant of the problem above. *}
    1.14    by blast
    1.15 -(*With removal of negated equality literals, this no longer works:
    1.16 -by (meson subsetI subset_antisym insertCI UnionI) 
    1.17 -*)
    1.18 -
    1.19  
    1.20  lemma "\<exists>!x. f (g x) = x \<Longrightarrow> \<exists>!y. g (f y) = y"
    1.21    -- {* A unique fixpoint theorem --- @{text fast}/@{text best}/@{text meson} all fail. *}
    1.22 -  apply (erule ex1E, rule ex1I, erule arg_cong)
    1.23 -  apply (rule subst, assumption, erule allE, rule arg_cong, erule mp)
    1.24 -  apply (erule arg_cong)
    1.25 -  done
    1.26 -
    1.27 +  by metis
    1.28  
    1.29  
    1.30  subsection {* Cantor's Theorem: There is no surjection from a set to its powerset *}