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.