tuned proofs
authorhaftmann
Wed Oct 07 14:01:26 2009 +0200 (2009-10-07)
changeset 32888ae17e72aac80
parent 32887 85e7ab9020ba
child 32889 c7cd4d3852dd
child 32890 77df12652210
tuned proofs
src/HOL/Set.thy
     1.1 --- a/src/HOL/Set.thy	Wed Oct 07 14:01:26 2009 +0200
     1.2 +++ b/src/HOL/Set.thy	Wed Oct 07 14:01:26 2009 +0200
     1.3 @@ -445,8 +445,8 @@
     1.4  
     1.5  subsubsection {* Subsets *}
     1.6  
     1.7 -lemma subsetI [atp,intro!]: "(!!x. x:A ==> x:B) ==> A \<subseteq> B"
     1.8 -  by (auto simp add: mem_def intro: predicate1I)
     1.9 +lemma subsetI [atp, intro!]: "(\<And>x. x \<in> A \<Longrightarrow> x \<in> B) \<Longrightarrow> A \<subseteq> B"
    1.10 +  unfolding mem_def by (rule le_funI, rule le_boolI)
    1.11  
    1.12  text {*
    1.13    \medskip Map the type @{text "'a set => anything"} to just @{typ
    1.14 @@ -455,8 +455,8 @@
    1.15  *}
    1.16  
    1.17  lemma subsetD [elim, intro?]: "A \<subseteq> B ==> c \<in> A ==> c \<in> B"
    1.18 +  unfolding mem_def by (erule le_funE, erule le_boolE)
    1.19    -- {* Rule in Modus Ponens style. *}
    1.20 -  by (unfold mem_def) blast
    1.21  
    1.22  lemma rev_subsetD [intro?]: "c \<in> A ==> A \<subseteq> B ==> c \<in> B"
    1.23    -- {* The same, with reversed premises for use with @{text erule} --
    1.24 @@ -467,9 +467,9 @@
    1.25    \medskip Converts @{prop "A \<subseteq> B"} to @{prop "x \<in> A ==> x \<in> B"}.
    1.26  *}
    1.27  
    1.28 -lemma subsetCE [elim]: "A \<subseteq>  B ==> (c \<notin> A ==> P) ==> (c \<in> B ==> P) ==> P"
    1.29 +lemma subsetCE [elim]: "A \<subseteq> B ==> (c \<notin> A ==> P) ==> (c \<in> B ==> P) ==> P"
    1.30    -- {* Classical elimination rule. *}
    1.31 -  by (unfold mem_def) blast
    1.32 +  unfolding mem_def by (blast dest: le_funE le_boolE)
    1.33  
    1.34  lemma subset_eq: "A \<le> B = (\<forall>x\<in>A. x \<in> B)" by blast
    1.35