src/HOL/Relation.thy
changeset 22172 e7d6cb237b5e
parent 21404 eb85850d3eb7
child 23185 1fa87978cf27
     1.1 --- a/src/HOL/Relation.thy	Wed Jan 24 13:15:16 2007 +0100
     1.2 +++ b/src/HOL/Relation.thy	Wed Jan 24 17:10:50 2007 +0100
     1.3 @@ -356,6 +356,11 @@
     1.4  lemma Domain_mono: "r \<subseteq> s ==> Domain r \<subseteq> Domain s"
     1.5    by blast
     1.6  
     1.7 +lemma fst_eq_Domain: "fst ` R = Domain R";
     1.8 +  apply auto
     1.9 +  apply (rule image_eqI, auto) 
    1.10 +  done
    1.11 +
    1.12  
    1.13  subsection {* Range *}
    1.14  
    1.15 @@ -392,6 +397,11 @@
    1.16  lemma Range_Union: "Range (Union S) = (\<Union>A\<in>S. Range A)"
    1.17    by blast
    1.18  
    1.19 +lemma snd_eq_Range: "snd ` R = Range R";
    1.20 +  apply auto
    1.21 +  apply (rule image_eqI, auto) 
    1.22 +  done
    1.23 +
    1.24  
    1.25  subsection {* Image of a set under a relation *}
    1.26