Re: [isabelle] operator on predicates and relations



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
>>
>>





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