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: "((\<lambda>x. x \<in> R) = (\<lambda>x. x \<in> S)) \<longleftrightarrow> (R = S)" |
77 by (simp add: set_eq_iff fun_eq_iff mem_def) |
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 mem_def) |
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: "((\<lambda>x. x \<in> R) \<le> (\<lambda>x. x \<in> S)) \<longleftrightarrow> (R \<subseteq> S)" |
86 by (simp add: subset_iff le_fun_def mem_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 mem_def) |
89 by (simp add: subset_iff le_fun_def) |
90 |
90 |
91 |
91 |
92 subsubsection {* Top and bottom elements *} |
92 subsubsection {* Top and bottom elements *} |
93 |
93 |
94 lemma bot1E [no_atp, elim!]: "\<bottom> x \<Longrightarrow> P" |
94 lemma bot1E [no_atp, elim!]: "\<bottom> x \<Longrightarrow> P" |
135 |
135 |
136 lemma inf2D2: "(A \<sqinter> B) x y \<Longrightarrow> B x y" |
136 lemma inf2D2: "(A \<sqinter> B) x y \<Longrightarrow> B x y" |
137 by (simp add: inf_fun_def) |
137 by (simp add: inf_fun_def) |
138 |
138 |
139 lemma inf_Int_eq: "(\<lambda>x. x \<in> R) \<sqinter> (\<lambda>x. x \<in> S) = (\<lambda>x. x \<in> R \<inter> S)" |
139 lemma inf_Int_eq: "(\<lambda>x. x \<in> R) \<sqinter> (\<lambda>x. x \<in> S) = (\<lambda>x. x \<in> R \<inter> S)" |
140 by (simp add: inf_fun_def mem_def) |
140 by (simp add: inf_fun_def) |
141 |
141 |
142 lemma inf_Int_eq2 [pred_set_conv]: "(\<lambda>x y. (x, y) \<in> R) \<sqinter> (\<lambda>x y. (x, y) \<in> S) = (\<lambda>x y. (x, y) \<in> R \<inter> S)" |
142 lemma inf_Int_eq2 [pred_set_conv]: "(\<lambda>x y. (x, y) \<in> R) \<sqinter> (\<lambda>x y. (x, y) \<in> S) = (\<lambda>x y. (x, y) \<in> R \<inter> S)" |
143 by (simp add: inf_fun_def mem_def) |
143 by (simp add: inf_fun_def) |
144 |
144 |
145 |
145 |
146 subsubsection {* Binary union *} |
146 subsubsection {* Binary union *} |
147 |
147 |
148 lemma sup1I1 [intro?]: "A x \<Longrightarrow> (A \<squnion> B) x" |
148 lemma sup1I1 [intro?]: "A x \<Longrightarrow> (A \<squnion> B) x" |
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: "(\<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 mem_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 mem_def) |
181 by (simp add: sup_fun_def) |
182 |
182 |
183 |
183 |
184 subsubsection {* Intersections of families *} |
184 subsubsection {* Intersections of families *} |
185 |
185 |
186 lemma INF1_iff: "(\<Sqinter>x\<in>A. B x) b = (\<forall>x\<in>A. B x b)" |
186 lemma INF1_iff: "(\<Sqinter>x\<in>A. B x) b = (\<forall>x\<in>A. B x b)" |
576 by (auto simp add: single_def bot_pred_def fun_eq_iff) |
576 by (auto simp add: single_def bot_pred_def fun_eq_iff) |
577 |
577 |
578 lemma not_bot: |
578 lemma not_bot: |
579 assumes "A \<noteq> \<bottom>" |
579 assumes "A \<noteq> \<bottom>" |
580 obtains x where "eval A x" |
580 obtains x where "eval A x" |
581 using assms by (cases A) (auto simp add: bot_pred_def, simp add: mem_def) |
581 using assms by (cases A) (auto simp add: bot_pred_def) |
582 |
582 |
583 |
583 |
584 subsubsection {* Emptiness check and definite choice *} |
584 subsubsection {* Emptiness check and definite choice *} |
585 |
585 |
586 definition is_empty :: "'a pred \<Rightarrow> bool" where |
586 definition is_empty :: "'a pred \<Rightarrow> bool" where |
587 "is_empty A \<longleftrightarrow> A = \<bottom>" |
587 "is_empty A \<longleftrightarrow> A = \<bottom>" |
1015 fun yieldn P = anamorph yield P; |
1015 fun yieldn P = anamorph yield P; |
1016 |
1016 |
1017 end; |
1017 end; |
1018 *} |
1018 *} |
1019 |
1019 |
1020 lemma eval_mem [simp]: |
|
1021 "x \<in> eval P \<longleftrightarrow> eval P x" |
|
1022 by (simp add: mem_def) |
|
1023 |
|
1024 lemma eq_mem [simp]: |
|
1025 "x \<in> (op =) y \<longleftrightarrow> x = y" |
|
1026 by (auto simp add: mem_def) |
|
1027 |
|
1028 no_notation |
1020 no_notation |
1029 bot ("\<bottom>") and |
1021 bot ("\<bottom>") and |
1030 top ("\<top>") and |
1022 top ("\<top>") and |
1031 inf (infixl "\<sqinter>" 70) and |
1023 inf (infixl "\<sqinter>" 70) and |
1032 sup (infixl "\<squnion>" 65) and |
1024 sup (infixl "\<squnion>" 65) and |