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