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.