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