# HG changeset patch # User wenzelm # Date 1273237973 -7200 # Node ID bca8762be737e28a190c067ea5834dbcadfd4a13 # Parent f5b63d2bd8fa056f02f6d9ba77740cdc581b828a# Parent 51e3b38a5e412b7d422bf6327c212e90d6f4a264 merged diff -r 51e3b38a5e41 -r bca8762be737 src/HOL/Relation.thy --- a/src/HOL/Relation.thy Fri May 07 14:47:09 2010 +0200 +++ b/src/HOL/Relation.thy Fri May 07 15:12:53 2010 +0200 @@ -406,7 +406,7 @@ lemma Domain_mono: "r \ s ==> Domain r \ Domain s" by blast -lemma fst_eq_Domain: "fst ` R = Domain R"; +lemma fst_eq_Domain: "fst ` R = Domain R" by (auto intro!:image_eqI) lemma Domain_dprod [simp]: "Domain (dprod r s) = uprod (Domain r) (Domain s)" @@ -457,7 +457,7 @@ lemma Range_converse[simp]: "Range(r^-1) = Domain r" by blast -lemma snd_eq_Range: "snd ` R = Range R"; +lemma snd_eq_Range: "snd ` R = Range R" by (auto intro!:image_eqI) @@ -639,9 +639,16 @@ done -subsection {* Version of @{text lfp_induct} for binary relations *} +subsection {* Miscellaneous *} + +text {* Version of @{thm[source] lfp_induct} for binary relations *} lemmas lfp_induct2 = lfp_induct_set [of "(a, b)", split_format (complete)] +text {* Version of @{thm[source] subsetI} for binary relations *} + +lemma subrelI: "(\x y. (x, y) \ r \ (x, y) \ s) \ r \ s" +by auto + end