src/HOL/Relation.thy
 changeset 46981 d54cea5b64e4 parent 46884 154dc6ec0041 child 46982 144d94446378
```     1.1 --- a/src/HOL/Relation.thy	Fri Mar 16 22:26:55 2012 +0100
1.2 +++ b/src/HOL/Relation.thy	Sat Mar 17 08:00:18 2012 +0100
1.3 @@ -95,6 +95,18 @@
1.4  lemma sup_Un_eq2 [pred_set_conv]: "(\<lambda>x y. (x, y) \<in> R) \<squnion> (\<lambda>x y. (x, y) \<in> S) = (\<lambda>x y. (x, y) \<in> R \<union> S)"
1.5    by (simp add: sup_fun_def)
1.6
1.7 +lemma INF_INT_eq [pred_set_conv]: "(\<Sqinter>i\<in>S. (\<lambda>x. x \<in> r i)) = (\<lambda>x. x \<in> (\<Inter>i\<in>S. r i))"
1.8 +  by (simp add: fun_eq_iff)
1.9 +
1.10 +lemma INF_INT_eq2 [pred_set_conv]: "(\<Sqinter>i\<in>S. (\<lambda>x y. (x, y) \<in> r i)) = (\<lambda>x y. (x, y) \<in> (\<Inter>i\<in>S. r i))"
1.11 +  by (simp add: fun_eq_iff)
1.12 +
1.13 +lemma SUP_UN_eq [pred_set_conv]: "(\<Squnion>i\<in>S. (\<lambda>x. x \<in> r i)) = (\<lambda>x. x \<in> (\<Union>i\<in>S. r i))"
1.14 +  by (simp add: fun_eq_iff)
1.15 +
1.16 +lemma SUP_UN_eq2 [pred_set_conv]: "(\<Squnion>i\<in>S. (\<lambda>x y. (x, y) \<in> r i)) = (\<lambda>x y. (x, y) \<in> (\<Union>i\<in>S. r i))"
1.17 +  by (simp add: fun_eq_iff)
1.18 +
1.19  lemma Inf_INT_eq [pred_set_conv]: "\<Sqinter>S = (\<lambda>x. x \<in> INTER S Collect)"
1.20    by (simp add: fun_eq_iff)
1.21
1.22 @@ -119,19 +131,6 @@
1.23  lemma SUP_Sup_eq2 [pred_set_conv]: "(\<Squnion>i\<in>S. (\<lambda>x y. (x, y) \<in> i)) = (\<lambda>x y. (x, y) \<in> \<Union>S)"
1.24    by (simp add: fun_eq_iff)
1.25
1.26 -lemma INF_INT_eq [pred_set_conv]: "(\<Sqinter>i. (\<lambda>x. x \<in> r i)) = (\<lambda>x. x \<in> (\<Inter>i. r i))"
1.27 -  by (simp add: fun_eq_iff)
1.28 -
1.29 -lemma INF_INT_eq2 [pred_set_conv]: "(\<Sqinter>i\<in>S. (\<lambda>x y. (x, y) \<in> r i)) = (\<lambda>x y. (x, y) \<in> (\<Inter>i\<in>S. r i))"
1.30 -  by (simp add: fun_eq_iff)
1.31 -
1.32 -lemma SUP_UN_eq [pred_set_conv]: "(\<Squnion>i. (\<lambda>x. x \<in> r i)) = (\<lambda>x. x \<in> (\<Union>i. r i))"
1.33 -  by (simp add: fun_eq_iff)
1.34 -
1.35 -lemma SUP_UN_eq2 [pred_set_conv]: "(\<Squnion>i\<in>S. (\<lambda>x y. (x, y) \<in> r i)) = (\<lambda>x y. (x, y) \<in> (\<Union>i\<in>S. r i))"
1.36 -  by (simp add: fun_eq_iff)
1.37 -
1.38 -
1.39
1.40  subsection {* Properties of relations *}
1.41
```