*To*: Andreas Lochbihler <andreas.lochbihler at inf.ethz.ch>, Johannes Hölzl <hoelzl at in.tum.de>, <cl-isabelle-users at lists.cam.ac.uk>*Subject*: Re: [isabelle] operator on predicates and relations*From*: Viorel Preoteasa <viorel.preoteasa at aalto.fi>*Date*: Thu, 3 Apr 2014 10:31:03 +0300*In-reply-to*: <532FF25A.9060408@inf.ethz.ch>*References*: <CDD9A9D3-F081-422C-9364-DB0E3252A0C8@cam.ac.uk> <53299484.2030100@aalto.fi> <1395237305.2841.192.camel@lapnipkow5> <5329C4DD.1030706@aalto.fi> <532FF25A.9060408@inf.ethz.ch>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:24.0) Gecko/20100101 Thunderbird/24.4.0

Hi Andreas, Thank you for your message. On 03/24/2014 10:52 AM, Andreas Lochbihler wrote: > Hi Viorel, > > If you do not care about the type system checks for type classes that > Isabelle provides, you can just use overloaded definitions, because > your types A, B, and C do not overlap. The most primitive form would > be the following (where myop on A and C is the identity and on B the > negation). > > consts myop :: "'a => 'a" > > defs (overloaded) myop_A_def: "myop == %P :: 'a A. P" > defs (overloaded) myop_B_def: "myop == %P :: ('a, 'b) B. %s t. ~ P s t" > defs (overloaded) myop_C_def: "myop == %P :: ('a, 'b, 'c) C. P" > > Note however that Isabelle does not enforce that myop is used only on > defined types. For example, "myop (3 :: int)" also type-checks. This is close to what I wanted, but I did not realize that this will have a price. It is no longer possible to have the type inferred from myop. If the class mechanism would work, then I could axiomatize the properties of myop in the class. > > If you want to use more advanced definition facilities > (definition/function/...), you should have a look at "context > overloading ... begin" context blocks. Where can I find more information and examples about this mechanism? Best regards, Viorel > > Best, > Andreas > > On 19/03/14 17:25, Viorel Preoteasa wrote: >> >> On 3/19/2014 3:55 PM, Johannes Hölzl wrote: >>> Am Mittwoch, den 19.03.2014, 14:58 +0200 schrieb Viorel Preoteasa: >>>> I am interested in a construction of the following structure: >>>> >>>> type_synonym 'a trace = "nat => 'a" >>>> type_synonym 'a A= "'a trace => bool" >>>> type_synonym 'a 'b B= "'a trace => 'b trace => bool" >>>> type_synonym 'a 'b 'c C= "'a trace => 'b trace => 'c trace => bool" >>>> >>>> class myoperator = >>>> fixes myop:: "'a => 'a" >>>> >>>> I would like to get an instantiation for myoperator class >>>> for the types ('a A), ('a 'b B), and ('a 'b 'c C), and to define >>>> myop in all these cases. >>>> >>>> More abstractly, I could also manage with using >>>> 'a::order instead of 'a trace. >>>> >>>> So I would like to be able to define myop for >>>> >>>> 'a::order => bool >>>> 'a::order => 'b::order => bool >>>> 'a::order => 'b::order => 'c::order => bool >>> If you use typedef instead of type_synonym you can instantiate the >>> myoperator type class. Then lift_definition + transfer could help you >>> translate the theorems on myop to theorems on functions. >> I guess that you suggest to define >> >> typedef 'a A= "{x :: 'a trace => bool . True}" >> instantiation "A":: (type) myoperator >> >> and then define myop on predicates via the bijection given by typedef. >> With this approach I end up with 3 different names for functions >> on 'a A, 'a 'b B, and 'a 'b 'c C. >> >> I could define these functions right from the beginning because I do >> not have theorems in myoperator. I just need a mechanism to have the >> same symbol for all these functions. >> >> Viorel >> >>

**Follow-Ups**:**Re: [isabelle] operator on predicates and relations***From:*Andreas Lochbihler

- Previous by Date: Re: [isabelle] I need an ML function to get the THY path and filename
- Next by Date: Re: [isabelle] operator on predicates and relations
- Previous by Thread: [isabelle] VSTTE CfP
- Next by Thread: Re: [isabelle] operator on predicates and relations
- Cl-isabelle-users April 2014 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list