src/HOL/HOLCF/Pcpo.thy
changeset 41431 138f414f14cb
parent 41430 1aa23e9f2c87
child 42151 4da4fc77664b
equal deleted inserted replaced
41430:1aa23e9f2c87 41431:138f414f14cb
   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