src/HOL/Relation.thy
changeset 61424 c3658c18b7bc
parent 61169 4de9ff3ea29a
child 61630 608520e0e8e2
     1.1 --- a/src/HOL/Relation.thy	Tue Oct 13 09:21:14 2015 +0200
     1.2 +++ b/src/HOL/Relation.thy	Tue Oct 13 09:21:15 2015 +0200
     1.3 @@ -951,10 +951,10 @@
     1.4  lemma Field_converse [simp]: "Field (r\<inverse>) = Field r"
     1.5    by (auto simp: Field_def)
     1.6  
     1.7 -lemma Domain_Collect_split [simp]: "Domain {(x, y). P x y} = {x. EX y. P x y}"
     1.8 +lemma Domain_Collect_case_prod [simp]: "Domain {(x, y). P x y} = {x. EX y. P x y}"
     1.9    by auto
    1.10  
    1.11 -lemma Range_Collect_split [simp]: "Range {(x, y). P x y} = {y. EX x. P x y}"
    1.12 +lemma Range_Collect_case_prod [simp]: "Range {(x, y). P x y} = {y. EX x. P x y}"
    1.13    by auto
    1.14  
    1.15  lemma finite_Domain: "finite r \<Longrightarrow> finite (Domain r)"
    1.16 @@ -1058,7 +1058,7 @@
    1.17  lemma Image_subset_eq: "(r``A \<subseteq> B) = (A \<subseteq> - ((r^-1) `` (-B)))"
    1.18    by blast
    1.19  
    1.20 -lemma Image_Collect_split [simp]: "{(x, y). P x y} `` A = {y. EX x:A. P x y}"
    1.21 +lemma Image_Collect_case_prod [simp]: "{(x, y). P x y} `` A = {y. EX x:A. P x y}"
    1.22    by auto
    1.23  
    1.24  lemma Sigma_Image: "(SIGMA x:A. B x) `` X = (\<Union>x\<in>X \<inter> A. B x)"