Re: [isabelle] Bool cpo

Hi Roger,

bool and set are already ccpos:

instance bool :: ccpo .. -- "this proof is actually empty"
instance set :: (type) ccpo .. -- "this proof is actually empty"

Also, your example is strange:

  definition less_bool_def: "(op â) = (op â)"

can not work, as â is specific for set, you need to use <=.
Also where do you get â from?

  - Johannes

Am Montag, den 26.10.2015, 21:27 +0200 schrieb Roger H.:
> Hello,
> to make set a cpo, its sufficient to make bool a cpo.
> If one defines the "â" operator as the "â" 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
> This induces an order on sets, which corresponds to the  "â" operator. 
> lemma less_set_eq: "(op â) = (op â)"
> But this lemma is not accepted by giving this error message:
> ---Type unification failed: No type arity set :: below---
> Can you help me?
> Many thanks! 		 	   		  

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