equal
deleted
inserted
replaced
79 by (simp add: sup_fun_eq sup_bool_eq) |
79 by (simp add: sup_fun_eq sup_bool_eq) |
80 |
80 |
81 lemma sup2_iff: "sup A B x y \<longleftrightarrow> A x y | B x y" |
81 lemma sup2_iff: "sup A B x y \<longleftrightarrow> A x y | B x y" |
82 by (simp add: sup_fun_eq sup_bool_eq) |
82 by (simp add: sup_fun_eq sup_bool_eq) |
83 |
83 |
84 lemma sup_Un_eq [pred_set_conv]: "sup (\<lambda>x. x \<in> R) (\<lambda>x. x \<in> S) = (\<lambda>x. x \<in> R \<union> S)" |
84 lemma sup_Un_eq: "sup (\<lambda>x. x \<in> R) (\<lambda>x. x \<in> S) = (\<lambda>x. x \<in> R \<union> S)" |
85 by (simp add: sup1_iff expand_fun_eq) |
85 by (simp add: sup1_iff expand_fun_eq) |
86 |
86 |
87 lemma sup_Un_eq2 [pred_set_conv]: "sup (\<lambda>x y. (x, y) \<in> R) (\<lambda>x y. (x, y) \<in> S) = (\<lambda>x y. (x, y) \<in> R \<union> S)" |
87 lemma sup_Un_eq2 [pred_set_conv]: "sup (\<lambda>x y. (x, y) \<in> R) (\<lambda>x y. (x, y) \<in> S) = (\<lambda>x y. (x, y) \<in> R \<union> S)" |
88 by (simp add: sup2_iff expand_fun_eq) |
88 by (simp add: sup2_iff expand_fun_eq) |
89 |
89 |
123 by (simp add: inf_fun_eq inf_bool_eq) |
123 by (simp add: inf_fun_eq inf_bool_eq) |
124 |
124 |
125 lemma inf2_iff: "inf A B x y \<longleftrightarrow> A x y \<and> B x y" |
125 lemma inf2_iff: "inf A B x y \<longleftrightarrow> A x y \<and> B x y" |
126 by (simp add: inf_fun_eq inf_bool_eq) |
126 by (simp add: inf_fun_eq inf_bool_eq) |
127 |
127 |
128 lemma inf_Int_eq [pred_set_conv]: "inf (\<lambda>x. x \<in> R) (\<lambda>x. x \<in> S) = (\<lambda>x. x \<in> R \<inter> S)" |
128 lemma inf_Int_eq: "inf (\<lambda>x. x \<in> R) (\<lambda>x. x \<in> S) = (\<lambda>x. x \<in> R \<inter> S)" |
129 by (simp add: inf1_iff expand_fun_eq) |
129 by (simp add: inf1_iff expand_fun_eq) |
130 |
130 |
131 lemma inf_Int_eq2 [pred_set_conv]: "inf (\<lambda>x y. (x, y) \<in> R) (\<lambda>x y. (x, y) \<in> S) = (\<lambda>x y. (x, y) \<in> R \<inter> S)" |
131 lemma inf_Int_eq2 [pred_set_conv]: "inf (\<lambda>x y. (x, y) \<in> R) (\<lambda>x y. (x, y) \<in> S) = (\<lambda>x y. (x, y) \<in> R \<inter> S)" |
132 by (simp add: inf2_iff expand_fun_eq) |
132 by (simp add: inf2_iff expand_fun_eq) |
133 |
133 |