summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | haftmann |

Thu, 19 Mar 2009 14:08:55 +0100 | |

changeset 30597 | 88c29b3b1fa2 |

parent 30583 | b51811144ed4 (current diff) |

parent 30596 | 140b22f22071 (diff) |

child 30598 | eb827cd69fd3 |

merged

--- a/src/HOL/Set.thy Thu Mar 19 11:51:49 2009 +0100 +++ b/src/HOL/Set.thy Thu Mar 19 14:08:55 2009 +0100 @@ -561,19 +561,15 @@ "'a set"}. *} -lemma subsetD [elim]: "A \<subseteq> B ==> c \<in> A ==> c \<in> B" +lemma subsetD [elim, intro?]: "A \<subseteq> B ==> c \<in> A ==> c \<in> B" -- {* Rule in Modus Ponens style. *} by (unfold mem_def) blast -declare subsetD [intro?] -- FIXME - -lemma rev_subsetD: "c \<in> A ==> A \<subseteq> B ==> c \<in> B" +lemma rev_subsetD [intro?]: "c \<in> A ==> A \<subseteq> B ==> c \<in> B" -- {* The same, with reversed premises for use with @{text erule} -- cf @{text rev_mp}. *} by (rule subsetD) -declare rev_subsetD [intro?] -- FIXME - text {* \medskip Converts @{prop "A \<subseteq> B"} to @{prop "x \<in> A ==> x \<in> B"}. *} @@ -623,8 +619,6 @@ -- {* Anti-symmetry of the subset relation. *} by (iprover intro: set_ext subsetD) -lemmas equalityI [intro!] = subset_antisym - text {* \medskip Equality rules from ZF set theory -- are they appropriate here? @@ -1064,11 +1058,6 @@ lemmas split_ifs = if_bool_eq_conj split_if_eq1 split_if_eq2 split_if_mem1 split_if_mem2 -lemmas mem_simps = - insert_iff empty_iff Un_iff Int_iff Compl_iff Diff_iff - mem_Collect_eq UN_iff Union_iff INT_iff Inter_iff - -- {* Each of these has ALREADY been added @{text "[simp]"} above. *} - (*Would like to add these, but the existing code only searches for the outer-level constant, which in this case is just "op :"; we instead need to use term-nets to associate patterns with rules. Also, if a rule fails to @@ -2489,7 +2478,13 @@ Sup ("\<Squnion>_" [900] 900) -subsection {* Basic ML bindings *} +subsection {* Misc theorem and ML bindings *} + +lemmas equalityI = subset_antisym +lemmas mem_simps = + insert_iff empty_iff Un_iff Int_iff Compl_iff Diff_iff + mem_Collect_eq UN_iff Union_iff INT_iff Inter_iff + -- {* Each of these has ALREADY been added @{text "[simp]"} above. *} ML {* val Ball_def = @{thm Ball_def}