1.1 --- a/NEWS	Fri Mar 16 22:26:55 2012 +0100
     1.2 +++ b/NEWS	Sat Mar 17 08:00:18 2012 +0100
     1.3 @@ -114,6 +114,8 @@
     1.4    Domain_def ~> Domain_unfold
     1.5    Range_def ~> Domain_converse [symmetric]
     1.6  
     1.7 +Generalized theorems INF_INT_eq, INF_INT_eq2, SUP_UN_eq, SUP_UN_eq2.
     1.8 +
     1.9  INCOMPATIBILITY.
    1.10  
    1.11  * Consolidated various theorem names relating to Finite_Set.fold

     2.1 --- a/src/HOL/Relation.thy	Fri Mar 16 22:26:55 2012 +0100
     2.2 +++ b/src/HOL/Relation.thy	Sat Mar 17 08:00:18 2012 +0100
     2.3 @@ -95,6 +95,18 @@
     2.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)"
     2.5    by (simp add: sup_fun_def)
     2.6  
     2.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))"
     2.8 +  by (simp add: fun_eq_iff)
     2.9 +
    2.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))"
    2.11 +  by (simp add: fun_eq_iff)
    2.12 +
    2.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))"
    2.14 +  by (simp add: fun_eq_iff)
    2.15 +
    2.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))"
    2.17 +  by (simp add: fun_eq_iff)
    2.18 +
    2.19  lemma Inf_INT_eq [pred_set_conv]: "\<Sqinter>S = (\<lambda>x. x \<in> INTER S Collect)"
    2.20    by (simp add: fun_eq_iff)
    2.21  
    2.22 @@ -119,19 +131,6 @@
    2.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)"
    2.24    by (simp add: fun_eq_iff)
    2.25  
    2.26 -lemma INF_INT_eq [pred_set_conv]: "(\<Sqinter>i. (\<lambda>x. x \<in> r i)) = (\<lambda>x. x \<in> (\<Inter>i. r i))"
    2.27 -  by (simp add: fun_eq_iff)
    2.28 -
    2.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))"
    2.30 -  by (simp add: fun_eq_iff)
    2.31 -
    2.32 -lemma SUP_UN_eq [pred_set_conv]: "(\<Squnion>i. (\<lambda>x. x \<in> r i)) = (\<lambda>x. x \<in> (\<Union>i. r i))"
    2.33 -  by (simp add: fun_eq_iff)
    2.34 -
    2.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))"
    2.36 -  by (simp add: fun_eq_iff)
    2.37 -
    2.38 -
    2.39  
    2.40  subsection {* Properties of relations *}
    2.41