src/HOL/Set.thy
changeset 18447 da548623916a
parent 18423 d7859164447f
child 18674 98d380757893
     1.1 --- a/src/HOL/Set.thy	Tue Dec 20 22:06:00 2005 +0100
     1.2 +++ b/src/HOL/Set.thy	Wed Dec 21 12:02:57 2005 +0100
     1.3 @@ -1452,10 +1452,10 @@
     1.4  lemma Union_Int_subset: "\<Union>(A \<inter> B) \<subseteq> \<Union>A \<inter> \<Union>B"
     1.5    by blast
     1.6  
     1.7 -lemma Union_empty_conv [iff]: "(\<Union>A = {}) = (\<forall>x\<in>A. x = {})"
     1.8 +lemma Union_empty_conv [simp]: "(\<Union>A = {}) = (\<forall>x\<in>A. x = {})"
     1.9    by blast
    1.10  
    1.11 -lemma empty_Union_conv [iff]: "({} = \<Union>A) = (\<forall>x\<in>A. x = {})"
    1.12 +lemma empty_Union_conv [simp]: "({} = \<Union>A) = (\<forall>x\<in>A. x = {})"
    1.13    by blast
    1.14  
    1.15  lemma Union_disjoint: "(\<Union>C \<inter> A = {}) = (\<forall>B\<in>C. B \<inter> A = {})"
    1.16 @@ -1479,7 +1479,7 @@
    1.17  lemma Inter_Un_distrib: "\<Inter>(A \<union> B) = \<Inter>A \<inter> \<Inter>B"
    1.18    by blast
    1.19  
    1.20 -lemma Inter_UNIV_conv [iff]:
    1.21 +lemma Inter_UNIV_conv [simp]:
    1.22    "(\<Inter>A = UNIV) = (\<forall>x\<in>A. x = UNIV)"
    1.23    "(UNIV = \<Inter>A) = (\<forall>x\<in>A. x = UNIV)"
    1.24    by blast+
    1.25 @@ -1555,12 +1555,12 @@
    1.26    -- {* Look: it has an \emph{existential} quantifier *}
    1.27    by blast
    1.28  
    1.29 -lemma UNION_empty_conv[iff]:
    1.30 +lemma UNION_empty_conv[simp]:
    1.31    "({} = (UN x:A. B x)) = (\<forall>x\<in>A. B x = {})"
    1.32    "((UN x:A. B x) = {}) = (\<forall>x\<in>A. B x = {})"
    1.33  by blast+
    1.34  
    1.35 -lemma INTER_UNIV_conv[iff]:
    1.36 +lemma INTER_UNIV_conv[simp]:
    1.37   "(UNIV = (INT x:A. B x)) = (\<forall>x\<in>A. B x = UNIV)"
    1.38   "((INT x:A. B x) = UNIV) = (\<forall>x\<in>A. B x = UNIV)"
    1.39  by blast+
    1.40 @@ -1790,7 +1790,7 @@
    1.41  lemma subset_iff_psubset_eq: "(A \<subseteq> B) = ((A \<subset> B) | (A = B))"
    1.42    by (unfold psubset_def) blast
    1.43  
    1.44 -lemma all_not_in_conv [iff]: "(\<forall>x. x \<notin> A) = (A = {})"
    1.45 +lemma all_not_in_conv [simp]: "(\<forall>x. x \<notin> A) = (A = {})"
    1.46    by blast
    1.47  
    1.48  lemma ex_in_conv: "(\<exists>x. x \<in> A) = (A \<noteq> {})"