# HG changeset patch
# User haftmann
# Date 1331967618 -3600
# Node ID d54cea5b64e4e26eb339dfdf48d382206db9b39d
# Parent  6bc213e904015a6b767a3519033ea1eabe34a329
generalized INF_INT_eq, SUP_UN_eq

diff -r 6bc213e90401 -r d54cea5b64e4 NEWS
--- a/NEWS	Fri Mar 16 22:26:55 2012 +0100
+++ b/NEWS	Sat Mar 17 08:00:18 2012 +0100
@@ -114,6 +114,8 @@
   Domain_def ~> Domain_unfold
   Range_def ~> Domain_converse [symmetric]
 
+Generalized theorems INF_INT_eq, INF_INT_eq2, SUP_UN_eq, SUP_UN_eq2.
+
 INCOMPATIBILITY.
 
 * Consolidated various theorem names relating to Finite_Set.fold
diff -r 6bc213e90401 -r d54cea5b64e4 src/HOL/Relation.thy
--- a/src/HOL/Relation.thy	Fri Mar 16 22:26:55 2012 +0100
+++ b/src/HOL/Relation.thy	Sat Mar 17 08:00:18 2012 +0100
@@ -95,6 +95,18 @@
 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)"
   by (simp add: sup_fun_def)
 
+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))"
+  by (simp add: fun_eq_iff)
+
+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))"
+  by (simp add: fun_eq_iff)
+
+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))"
+  by (simp add: fun_eq_iff)
+
+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))"
+  by (simp add: fun_eq_iff)
+
 lemma Inf_INT_eq [pred_set_conv]: "\<Sqinter>S = (\<lambda>x. x \<in> INTER S Collect)"
   by (simp add: fun_eq_iff)
 
@@ -119,19 +131,6 @@
 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)"
   by (simp add: fun_eq_iff)
 
-lemma INF_INT_eq [pred_set_conv]: "(\<Sqinter>i. (\<lambda>x. x \<in> r i)) = (\<lambda>x. x \<in> (\<Inter>i. r i))"
-  by (simp add: fun_eq_iff)
-
-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))"
-  by (simp add: fun_eq_iff)
-
-lemma SUP_UN_eq [pred_set_conv]: "(\<Squnion>i. (\<lambda>x. x \<in> r i)) = (\<lambda>x. x \<in> (\<Union>i. r i))"
-  by (simp add: fun_eq_iff)
-
-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))"
-  by (simp add: fun_eq_iff)
-
-
 
 subsection {* Properties of relations *}