src/HOL/Relation.thy
changeset 13812 91713a1915ee
parent 13639 8ee6ea6627e1
child 13830 7f8c1b533e8b
     1.1 --- a/src/HOL/Relation.thy	Sat Feb 08 14:46:22 2003 +0100
     1.2 +++ b/src/HOL/Relation.thy	Sat Feb 08 16:05:33 2003 +0100
     1.3 @@ -86,6 +86,9 @@
     1.4  
     1.5  subsection {* Diagonal: identity over a set *}
     1.6  
     1.7 +lemma diag_empty [simp]: "diag {} = {}"
     1.8 +  by (simp add: diag_def) 
     1.9 +
    1.10  lemma diag_eqI: "a = b ==> a : A ==> (a, b) : diag A"
    1.11    by (simp add: diag_def)
    1.12  
    1.13 @@ -318,6 +321,9 @@
    1.14  lemma Image_Un: "R `` (A Un B) = R `` A Un R `` B"
    1.15    by blast
    1.16  
    1.17 +lemma Un_Image: "(R \<union> S) `` A = R `` A \<union> S `` A"
    1.18 +  by blast
    1.19 +
    1.20  lemma Image_subset: "r \<subseteq> A \<times> B ==> r``C \<subseteq> B"
    1.21    by (rules intro!: subsetI elim!: ImageE dest!: subsetD SigmaD2)
    1.22