equal
deleted
inserted
replaced
173 (fn Const(@{const_name bottom}, _) => true | _ => false) |
173 (fn Const(@{const_name bottom}, _) => true | _ => false) |
174 *} |
174 *} |
175 |
175 |
176 simproc_setup reorient_bottom ("\<bottom> = x") = Reorient_Proc.proc |
176 simproc_setup reorient_bottom ("\<bottom> = x") = Reorient_Proc.proc |
177 |
177 |
178 context pcpo |
|
179 begin |
|
180 |
|
181 text {* useful lemmas about @{term \<bottom>} *} |
178 text {* useful lemmas about @{term \<bottom>} *} |
182 |
179 |
183 lemma below_bottom_iff [simp]: "(x \<sqsubseteq> \<bottom>) = (x = \<bottom>)" |
180 lemma below_bottom_iff [simp]: "(x \<sqsubseteq> \<bottom>) = (x = \<bottom>)" |
184 by (simp add: po_eq_conv) |
181 by (simp add: po_eq_conv) |
185 |
182 |
189 lemma bottomI: "x \<sqsubseteq> \<bottom> \<Longrightarrow> x = \<bottom>" |
186 lemma bottomI: "x \<sqsubseteq> \<bottom> \<Longrightarrow> x = \<bottom>" |
190 by (subst eq_bottom_iff) |
187 by (subst eq_bottom_iff) |
191 |
188 |
192 lemma lub_eq_bottom_iff: "chain Y \<Longrightarrow> (\<Squnion>i. Y i) = \<bottom> \<longleftrightarrow> (\<forall>i. Y i = \<bottom>)" |
189 lemma lub_eq_bottom_iff: "chain Y \<Longrightarrow> (\<Squnion>i. Y i) = \<bottom> \<longleftrightarrow> (\<forall>i. Y i = \<bottom>)" |
193 by (simp only: eq_bottom_iff lub_below_iff) |
190 by (simp only: eq_bottom_iff lub_below_iff) |
194 |
|
195 lemma chain_UU_I: "\<lbrakk>chain Y; (\<Squnion>i. Y i) = \<bottom>\<rbrakk> \<Longrightarrow> \<forall>i. Y i = \<bottom>" |
|
196 by (simp add: lub_eq_bottom_iff) |
|
197 |
|
198 lemma chain_UU_I_inverse: "\<forall>i::nat. Y i = \<bottom> \<Longrightarrow> (\<Squnion>i. Y i) = \<bottom>" |
|
199 by simp |
|
200 |
|
201 lemma chain_UU_I_inverse2: "(\<Squnion>i. Y i) \<noteq> \<bottom> \<Longrightarrow> \<exists>i::nat. Y i \<noteq> \<bottom>" |
|
202 by (blast intro: chain_UU_I_inverse) |
|
203 |
|
204 lemma notUU_I: "\<lbrakk>x \<sqsubseteq> y; x \<noteq> \<bottom>\<rbrakk> \<Longrightarrow> y \<noteq> \<bottom>" |
|
205 by (blast intro: bottomI) |
|
206 |
|
207 end |
|
208 |
191 |
209 subsection {* Chain-finite and flat cpos *} |
192 subsection {* Chain-finite and flat cpos *} |
210 |
193 |
211 text {* further useful classes for HOLCF domains *} |
194 text {* further useful classes for HOLCF domains *} |
212 |
195 |