--- a/src/HOL/Relation.thy Sat Feb 08 14:46:22 2003 +0100
+++ b/src/HOL/Relation.thy Sat Feb 08 16:05:33 2003 +0100
@@ -86,6 +86,9 @@
subsection {* Diagonal: identity over a set *}
+lemma diag_empty [simp]: "diag {} = {}"
+ by (simp add: diag_def)
+
lemma diag_eqI: "a = b ==> a : A ==> (a, b) : diag A"
by (simp add: diag_def)
@@ -318,6 +321,9 @@
lemma Image_Un: "R `` (A Un B) = R `` A Un R `` B"
by blast
+lemma Un_Image: "(R \<union> S) `` A = R `` A \<union> S `` A"
+ by blast
+
lemma Image_subset: "r \<subseteq> A \<times> B ==> r``C \<subseteq> B"
by (rules intro!: subsetI elim!: ImageE dest!: subsetD SigmaD2)