93 by (simp add: sup_fun_def) |
93 by (simp add: sup_fun_def) |
94 |
94 |
95 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)" |
95 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)" |
96 by (simp add: sup_fun_def) |
96 by (simp add: sup_fun_def) |
97 |
97 |
|
98 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))" |
|
99 by (simp add: fun_eq_iff) |
|
100 |
|
101 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))" |
|
102 by (simp add: fun_eq_iff) |
|
103 |
|
104 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))" |
|
105 by (simp add: fun_eq_iff) |
|
106 |
|
107 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))" |
|
108 by (simp add: fun_eq_iff) |
|
109 |
98 lemma Inf_INT_eq [pred_set_conv]: "\<Sqinter>S = (\<lambda>x. x \<in> INTER S Collect)" |
110 lemma Inf_INT_eq [pred_set_conv]: "\<Sqinter>S = (\<lambda>x. x \<in> INTER S Collect)" |
99 by (simp add: fun_eq_iff) |
111 by (simp add: fun_eq_iff) |
100 |
112 |
101 lemma INF_Int_eq [pred_set_conv]: "(\<Sqinter>i\<in>S. (\<lambda>x. x \<in> i)) = (\<lambda>x. x \<in> \<Inter>S)" |
113 lemma INF_Int_eq [pred_set_conv]: "(\<Sqinter>i\<in>S. (\<lambda>x. x \<in> i)) = (\<lambda>x. x \<in> \<Inter>S)" |
102 by (simp add: fun_eq_iff) |
114 by (simp add: fun_eq_iff) |
116 lemma Sup_SUP_eq2 [pred_set_conv]: "\<Squnion>S = (\<lambda>x y. (x, y) \<in> UNION (prod_case ` S) Collect)" |
128 lemma Sup_SUP_eq2 [pred_set_conv]: "\<Squnion>S = (\<lambda>x y. (x, y) \<in> UNION (prod_case ` S) Collect)" |
117 by (simp add: fun_eq_iff) |
129 by (simp add: fun_eq_iff) |
118 |
130 |
119 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)" |
131 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)" |
120 by (simp add: fun_eq_iff) |
132 by (simp add: fun_eq_iff) |
121 |
|
122 lemma INF_INT_eq [pred_set_conv]: "(\<Sqinter>i. (\<lambda>x. x \<in> r i)) = (\<lambda>x. x \<in> (\<Inter>i. r i))" |
|
123 by (simp add: fun_eq_iff) |
|
124 |
|
125 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))" |
|
126 by (simp add: fun_eq_iff) |
|
127 |
|
128 lemma SUP_UN_eq [pred_set_conv]: "(\<Squnion>i. (\<lambda>x. x \<in> r i)) = (\<lambda>x. x \<in> (\<Union>i. r i))" |
|
129 by (simp add: fun_eq_iff) |
|
130 |
|
131 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))" |
|
132 by (simp add: fun_eq_iff) |
|
133 |
|
134 |
133 |
135 |
134 |
136 subsection {* Properties of relations *} |
135 subsection {* Properties of relations *} |
137 |
136 |
138 subsubsection {* Reflexivity *} |
137 subsubsection {* Reflexivity *} |