equal
deleted
inserted
replaced
71 by (rule predicate2D) |
71 by (rule predicate2D) |
72 |
72 |
73 |
73 |
74 subsubsection {* Equality *} |
74 subsubsection {* Equality *} |
75 |
75 |
76 lemma pred_equals_eq: "((\<lambda>x. x \<in> R) = (\<lambda>x. x \<in> S)) \<longleftrightarrow> (R = S)" |
76 lemma pred_equals_eq [pred_set_conv]: "((\<lambda>x. x \<in> R) = (\<lambda>x. x \<in> S)) \<longleftrightarrow> (R = S)" |
77 by (simp add: set_eq_iff fun_eq_iff) |
77 by (simp add: set_eq_iff fun_eq_iff) |
78 |
78 |
79 lemma pred_equals_eq2 [pred_set_conv]: "((\<lambda>x y. (x, y) \<in> R) = (\<lambda>x y. (x, y) \<in> S)) \<longleftrightarrow> (R = S)" |
79 lemma pred_equals_eq2 [pred_set_conv]: "((\<lambda>x y. (x, y) \<in> R) = (\<lambda>x y. (x, y) \<in> S)) \<longleftrightarrow> (R = S)" |
80 by (simp add: set_eq_iff fun_eq_iff) |
80 by (simp add: set_eq_iff fun_eq_iff) |
81 |
81 |
82 |
82 |
83 subsubsection {* Order relation *} |
83 subsubsection {* Order relation *} |
84 |
84 |
85 lemma pred_subset_eq: "((\<lambda>x. x \<in> R) \<le> (\<lambda>x. x \<in> S)) \<longleftrightarrow> (R \<subseteq> S)" |
85 lemma pred_subset_eq [pred_set_conv]: "((\<lambda>x. x \<in> R) \<le> (\<lambda>x. x \<in> S)) \<longleftrightarrow> (R \<subseteq> S)" |
86 by (simp add: subset_iff le_fun_def) |
86 by (simp add: subset_iff le_fun_def) |
87 |
87 |
88 lemma pred_subset_eq2 [pred_set_conv]: "((\<lambda>x y. (x, y) \<in> R) \<le> (\<lambda>x y. (x, y) \<in> S)) \<longleftrightarrow> (R \<subseteq> S)" |
88 lemma pred_subset_eq2 [pred_set_conv]: "((\<lambda>x y. (x, y) \<in> R) \<le> (\<lambda>x y. (x, y) \<in> S)) \<longleftrightarrow> (R \<subseteq> S)" |
89 by (simp add: subset_iff le_fun_def) |
89 by (simp add: subset_iff le_fun_def) |
90 |
90 |
172 by (auto simp add: sup_fun_def) |
172 by (auto simp add: sup_fun_def) |
173 |
173 |
174 lemma sup2CI [intro!]: "(\<not> B x y \<Longrightarrow> A x y) \<Longrightarrow> (A \<squnion> B) x y" |
174 lemma sup2CI [intro!]: "(\<not> B x y \<Longrightarrow> A x y) \<Longrightarrow> (A \<squnion> B) x y" |
175 by (auto simp add: sup_fun_def) |
175 by (auto simp add: sup_fun_def) |
176 |
176 |
177 lemma sup_Un_eq: "(\<lambda>x. x \<in> R) \<squnion> (\<lambda>x. x \<in> S) = (\<lambda>x. x \<in> R \<union> S)" |
177 lemma sup_Un_eq [pred_set_conv]: "(\<lambda>x. x \<in> R) \<squnion> (\<lambda>x. x \<in> S) = (\<lambda>x. x \<in> R \<union> S)" |
178 by (simp add: sup_fun_def) |
178 by (simp add: sup_fun_def) |
179 |
179 |
180 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)" |
180 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)" |
181 by (simp add: sup_fun_def) |
181 by (simp add: sup_fun_def) |
182 |
182 |
232 by (auto simp add: SUP_apply) |
232 by (auto simp add: SUP_apply) |
233 |
233 |
234 lemma SUP2_E [elim!]: "(\<Squnion>x\<in>A. B x) b c \<Longrightarrow> (\<And>x. x \<in> A \<Longrightarrow> B x b c \<Longrightarrow> R) \<Longrightarrow> R" |
234 lemma SUP2_E [elim!]: "(\<Squnion>x\<in>A. B x) b c \<Longrightarrow> (\<And>x. x \<in> A \<Longrightarrow> B x b c \<Longrightarrow> R) \<Longrightarrow> R" |
235 by (auto simp add: SUP_apply) |
235 by (auto simp add: SUP_apply) |
236 |
236 |
237 lemma SUP_UN_eq: "(\<Squnion>i. (\<lambda>x. x \<in> r i)) = (\<lambda>x. x \<in> (\<Union>i. r i))" |
237 lemma SUP_UN_eq [pred_set_conv]: "(\<Squnion>i. (\<lambda>x. x \<in> r i)) = (\<lambda>x. x \<in> (\<Union>i. r i))" |
238 by (simp add: SUP_apply fun_eq_iff) |
238 by (simp add: SUP_apply fun_eq_iff) |
239 |
239 |
240 lemma SUP_UN_eq2: "(\<Squnion>i. (\<lambda>x y. (x, y) \<in> r i)) = (\<lambda>x y. (x, y) \<in> (\<Union>i. r i))" |
240 lemma SUP_UN_eq2 [pred_set_conv]: "(\<Squnion>i. (\<lambda>x y. (x, y) \<in> r i)) = (\<lambda>x y. (x, y) \<in> (\<Union>i. r i))" |
241 by (simp add: SUP_apply fun_eq_iff) |
241 by (simp add: SUP_apply fun_eq_iff) |
242 |
242 |
243 |
243 |
244 subsection {* Predicates as relations *} |
244 subsection {* Predicates as relations *} |
245 |
245 |
339 "Powp A = (\<lambda>B. \<forall>x \<in> B. A x)" |
339 "Powp A = (\<lambda>B. \<forall>x \<in> B. A x)" |
340 |
340 |
341 lemma Powp_Pow_eq [pred_set_conv]: "Powp (\<lambda>x. x \<in> A) = (\<lambda>x. x \<in> Pow A)" |
341 lemma Powp_Pow_eq [pred_set_conv]: "Powp (\<lambda>x. x \<in> A) = (\<lambda>x. x \<in> Pow A)" |
342 by (auto simp add: Powp_def fun_eq_iff) |
342 by (auto simp add: Powp_def fun_eq_iff) |
343 |
343 |
344 lemmas Powp_mono [mono] = Pow_mono [to_pred pred_subset_eq] |
344 lemmas Powp_mono [mono] = Pow_mono [to_pred] |
345 |
345 |
346 |
346 |
347 subsubsection {* Properties of relations *} |
347 subsubsection {* Properties of relations *} |
348 |
348 |
349 abbreviation antisymP :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool" where |
349 abbreviation antisymP :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool" where |