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)"
```