Re: [isabelle] Bool cpo



Hello, thank you for your help, it was sucessfully proven and this issue is closed.

> From: s57076 at hotmail.com
> To: isabelle-users at cl.cam.ac.uk
> Date: Tue, 27 Oct 2015 16:01:46 +0200
> Subject: Re: [isabelle] Bool cpo
> 
> Hello Johannes
> 
> my exact question is:
> While working in HOLCF(not HOL)...if I copy-paste the following class SetPcpo
> http://isabelle.in.tum.de/website-Isabelle2008/dist/library/HOLCF/SetPcpo.html
> in the HOLCF folder,
> and run it, then I get at the following spot
> lemma less_set_eq: "(op â) = (op â)"the following error: --Type unification failed: No type arity set :: below
> 
> Type error in application: incompatible operand type
> 
> Operator:  op = op â :: (??'a â ??'a â bool) â bool
> Operand:   op â :: ??'b set â ??'b set â bool--1. Why is the error?
> 2. How do i prove here "instance bool :: cpo"   //notice that this is the class cpo of holcf, as in [Huf 11],  and not --hol ccpo--  3. How do i then prove "instance set :: (type) cpo"     
> Thank you! 		 	   		  
 		 	   		  


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