tuned some theorem and attribute bindings
authorhaftmann
Thu Mar 19 14:08:41 2009 +0100 (2009-03-19)
changeset 30596140b22f22071
parent 30570 8fac7efcce0a
child 30597 88c29b3b1fa2
tuned some theorem and attribute bindings
src/HOL/Set.thy
     1.1 --- a/src/HOL/Set.thy	Wed Mar 18 15:23:52 2009 +0100
     1.2 +++ b/src/HOL/Set.thy	Thu Mar 19 14:08:41 2009 +0100
     1.3 @@ -561,19 +561,15 @@
     1.4    "'a set"}.
     1.5  *}
     1.6  
     1.7 -lemma subsetD [elim]: "A \<subseteq> B ==> c \<in> A ==> c \<in> B"
     1.8 +lemma subsetD [elim, intro?]: "A \<subseteq> B ==> c \<in> A ==> c \<in> B"
     1.9    -- {* Rule in Modus Ponens style. *}
    1.10    by (unfold mem_def) blast
    1.11  
    1.12 -declare subsetD [intro?] -- FIXME
    1.13 -
    1.14 -lemma rev_subsetD: "c \<in> A ==> A \<subseteq> B ==> c \<in> B"
    1.15 +lemma rev_subsetD [intro?]: "c \<in> A ==> A \<subseteq> B ==> c \<in> B"
    1.16    -- {* The same, with reversed premises for use with @{text erule} --
    1.17        cf @{text rev_mp}. *}
    1.18    by (rule subsetD)
    1.19  
    1.20 -declare rev_subsetD [intro?] -- FIXME
    1.21 -
    1.22  text {*
    1.23    \medskip Converts @{prop "A \<subseteq> B"} to @{prop "x \<in> A ==> x \<in> B"}.
    1.24  *}
    1.25 @@ -623,8 +619,6 @@
    1.26    -- {* Anti-symmetry of the subset relation. *}
    1.27    by (iprover intro: set_ext subsetD)
    1.28  
    1.29 -lemmas equalityI [intro!] = subset_antisym
    1.30 -
    1.31  text {*
    1.32    \medskip Equality rules from ZF set theory -- are they appropriate
    1.33    here?
    1.34 @@ -1064,11 +1058,6 @@
    1.35  
    1.36  lemmas split_ifs = if_bool_eq_conj split_if_eq1 split_if_eq2 split_if_mem1 split_if_mem2
    1.37  
    1.38 -lemmas mem_simps =
    1.39 -  insert_iff empty_iff Un_iff Int_iff Compl_iff Diff_iff
    1.40 -  mem_Collect_eq UN_iff Union_iff INT_iff Inter_iff
    1.41 -  -- {* Each of these has ALREADY been added @{text "[simp]"} above. *}
    1.42 -
    1.43  (*Would like to add these, but the existing code only searches for the
    1.44    outer-level constant, which in this case is just "op :"; we instead need
    1.45    to use term-nets to associate patterns with rules.  Also, if a rule fails to
    1.46 @@ -2489,7 +2478,13 @@
    1.47    Sup  ("\<Squnion>_" [900] 900)
    1.48  
    1.49  
    1.50 -subsection {* Basic ML bindings *}
    1.51 +subsection {* Misc theorem and ML bindings *}
    1.52 +
    1.53 +lemmas equalityI = subset_antisym
    1.54 +lemmas mem_simps =
    1.55 +  insert_iff empty_iff Un_iff Int_iff Compl_iff Diff_iff
    1.56 +  mem_Collect_eq UN_iff Union_iff INT_iff Inter_iff
    1.57 +  -- {* Each of these has ALREADY been added @{text "[simp]"} above. *}
    1.58  
    1.59  ML {*
    1.60  val Ball_def = @{thm Ball_def}