Email Gateway (Aug 22 2022 at 11:36): Email Gateway (Aug 22 2022 at 11:36):From: "Roger H." <s57076@hotmail.com>
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
Email Gateway (Aug 22 2022 at 11:37):From: "Roger H." <s57076@hotmail.com>
Hello, thank you for your help, it was sucessfully proven and this issue is closed.Excuse me for duplicat post.
Best regards!
Last updated: Apr 25 2024 at 04:18 UTC