# Re: [isabelle] Bool cpo: status update

Hello, thank you for your help, it was sucessfully proven and this issue is closed.Excuse me for duplicat post.
Best regards!
> From: s57076 at hotmail.com
> To: isabelle-users at cl.cam.ac.uk
> Date: Tue, 27 Oct 2015 16:57:00 +0200
> Subject: 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.*