src/HOL/Relation.thy
changeset 62087 44841d07ef1d
parent 61955 e96292f32c3c
child 62343 24106dc44def
     1.1 --- a/src/HOL/Relation.thy	Wed Jan 06 16:17:50 2016 +0100
     1.2 +++ b/src/HOL/Relation.thy	Thu Jan 07 17:40:55 2016 +0000
     1.3 @@ -515,6 +515,8 @@
     1.4  lemma total_on_diff_Id [simp]: "total_on A (r - Id) = total_on A r"
     1.5    by (simp add: total_on_def)
     1.6  
     1.7 +lemma Id_fstsnd_eq: "Id = {x. fst x = snd x}"
     1.8 +  by force
     1.9  
    1.10  subsubsection \<open>Diagonal: identity over a set\<close>
    1.11  
    1.12 @@ -873,6 +875,12 @@
    1.13  lemma snd_eq_Range: "snd ` R = Range R"
    1.14    by force
    1.15  
    1.16 +lemma range_fst [simp]: "range fst = UNIV"
    1.17 +  by (auto simp: fst_eq_Domain)
    1.18 +
    1.19 +lemma range_snd [simp]: "range snd = UNIV"
    1.20 +  by (auto simp: snd_eq_Range)
    1.21 +
    1.22  lemma Domain_empty [simp]: "Domain {} = {}"
    1.23    by auto
    1.24