# Re: [isabelle] Bool cpo: status update

Hello Johannes,
an update: In HOLCF, I can prove that bool is a pcpo (see below). Based on this, how can i prove that set is a cpo:
instance set :: (type) cpo
Thank you!
---Proof that bool is a pcpo:
text {* If one defines the @{text "â"} operator as the @{text "-->"} operator on booleans, one obtains a partial order. *}
instantiation bool :: pobegin definition less_bool_def: "(op â) = (op -->)"instanceby (intro_classes, unfold less_bool_def, safe)end
text {* Now we will establish that the partial order on bools is complete. *}
text {* Chains of bools are always finite *}instance bool :: chfinproof fix S:: "nat â bool" assume S: "chain S" then have "finite (range S)" by simp from S and this have "finite_chain S" by (rule finite_range_imp_finch) thus "â n. max_in_chain n S" by (unfold finite_chain_def, simp)qed
instance bool :: cpoproofqed
text {* Bools are also pointed with @{text "False"} as minimal element. *}instance bool :: pcpoproof have "ây::bool. False â y" unfolding less_bool_def by simp thus "âx::bool. ây. x â y" ..qed

*This archive was generated by a fusion of
Pipermail (Mailman edition) and
MHonArc.*