src/HOL/Set.thy
changeset 33044 fd0a9c794ec1
parent 33022 c95102496490
child 33045 2b3694001c48
     1.1 --- a/src/HOL/Set.thy	Tue Oct 20 15:02:48 2009 +0100
     1.2 +++ b/src/HOL/Set.thy	Tue Oct 20 16:32:51 2009 +0100
     1.3 @@ -458,7 +458,7 @@
     1.4    unfolding mem_def by (erule le_funE, erule le_boolE)
     1.5    -- {* Rule in Modus Ponens style. *}
     1.6  
     1.7 -lemma rev_subsetD [intro?]: "c \<in> A ==> A \<subseteq> B ==> c \<in> B"
     1.8 +lemma rev_subsetD [noatp,intro?]: "c \<in> A ==> A \<subseteq> B ==> c \<in> B"
     1.9    -- {* The same, with reversed premises for use with @{text erule} --
    1.10        cf @{text rev_mp}. *}
    1.11    by (rule subsetD)
    1.12 @@ -467,13 +467,13 @@
    1.13    \medskip Converts @{prop "A \<subseteq> B"} to @{prop "x \<in> A ==> x \<in> B"}.
    1.14  *}
    1.15  
    1.16 -lemma subsetCE [elim]: "A \<subseteq> B ==> (c \<notin> A ==> P) ==> (c \<in> B ==> P) ==> P"
    1.17 +lemma subsetCE [noatp,elim]: "A \<subseteq> B ==> (c \<notin> A ==> P) ==> (c \<in> B ==> P) ==> P"
    1.18    -- {* Classical elimination rule. *}
    1.19    unfolding mem_def by (blast dest: le_funE le_boolE)
    1.20  
    1.21 -lemma subset_eq: "A \<le> B = (\<forall>x\<in>A. x \<in> B)" by blast
    1.22 +lemma subset_eq [noatp]: "A \<le> B = (\<forall>x\<in>A. x \<in> B)" by blast
    1.23  
    1.24 -lemma contra_subsetD: "A \<subseteq> B ==> c \<notin> B ==> c \<notin> A"
    1.25 +lemma contra_subsetD [noatp]: "A \<subseteq> B ==> c \<notin> B ==> c \<notin> A"
    1.26    by blast
    1.27  
    1.28  lemma subset_refl [simp]: "A \<subseteq> A"
    1.29 @@ -488,8 +488,11 @@
    1.30  lemma set_mp: "A \<subseteq> B ==> x:A ==> x:B"
    1.31    by (rule subsetD)
    1.32  
    1.33 +lemma eq_mem_trans: "a=b ==> b \<in> A ==> a \<in> A"
    1.34 +  by simp
    1.35 +
    1.36  lemmas basic_trans_rules [trans] =
    1.37 -  order_trans_rules set_rev_mp set_mp
    1.38 +  order_trans_rules set_rev_mp set_mp eq_mem_trans
    1.39  
    1.40  
    1.41  subsubsection {* Equality *}