author haftmann Sat, 17 Mar 2012 08:00:18 +0100 changeset 46981 d54cea5b64e4 parent 46980 6bc213e90401 child 46982 144d94446378
generalized INF_INT_eq, SUP_UN_eq
 NEWS file | annotate | diff | comparison | revisions src/HOL/Relation.thy file | annotate | diff | comparison | revisions
```--- 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```
```--- 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)"

+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))"
+
+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))"
+
+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))"
+
+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))"
+
lemma Inf_INT_eq [pred_set_conv]: "\<Sqinter>S = (\<lambda>x. x \<in> INTER S Collect)"

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

-lemma INF_INT_eq [pred_set_conv]: "(\<Sqinter>i. (\<lambda>x. x \<in> r i)) = (\<lambda>x. x \<in> (\<Inter>i. r i))"
-
-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))"