*To*: Andreas Lochbihler <andreas.lochbihler at inf.ethz.ch>, Lars Hupel <hupel at in.tum.de>, isabelle-users at cl.cam.ac.uk*Subject*: Re: [isabelle] Default implementations for instances*From*: Florian Haftmann <florian.haftmann at informatik.tu-muenchen.de>*Date*: Fri, 11 Apr 2014 15:46:44 +0200*In-reply-to*: <5346B2F6.9040703@inf.ethz.ch>*Organization*: TU Munich*References*: <c318b460c1f157ccc49027532bc01ecb-EhVcX1hCQQpcRwURGhY3AF9BdAJSS1xcXF9EBlw1WENZS1kNVkFyBktcXjBeQkwFXllQQ19W-webmailer2@server02.webmailer.hosteurope.de> <5346B2F6.9040703@inf.ethz.ch>*User-agent*: Mozilla/5.0 (X11; Linux i686; rv:24.0) Gecko/20100101 Thunderbird/24.4.0

> The most prominent example of this probably is "op <" in the preorder > type class, which is completely determined by the assumption > strict_iff_order. All instantiations have to specify both "op <=" and > "op <" and prove that they are compatible. The theory Partial_Function > even defines a general mk_less operator to that end. This strict coupling of Orderings.less_eq and Orderings.less is mainly historic and could be split into two class hierarchies (e.g. strict_* and reflexive_*, where the existing class »foo« joins the classes strict_foo and reflexive_foo). If the situation is pressing enough, this should be seriously considered. Cheers, Florian > > 2. In my AFP entry Containers, I introduce a new typeclass clinorder > which has a default implementation if the type is in linorder, and the > same for ceq and HOL.equal. René Thiemann extended his > Datatype_Order_Generator such that it can automatically produce these > instantiations and discharge the proof obligations. > > However, in this setting, I would not want to the instance to be > automatic. Rather do I want to decide when I pick the default > implementation and when I choose some other implementation. This would > mean that I still issue a command that triggers the default > implementation, but I no longer have to specify the instantiation nor > prove the assumptions. > > Note that in this case, the assumptions are not of the form "f = foo g". > > Andreas > > On 10/04/14 16:16, Lars Hupel wrote: >> Assume the following classes: >> >> class a = >> fixes f :: "'a => nat" >> assumes ... >> >> class b = >> fixes g :: "'a => 'a => nat" >> assumes ... >> >> (the precise types of the class parameters don't matter) >> >> Furthermore assume that 'f' can be implemented in terms of 'g', but >> not all types can be >> made instances of class 'b'. In such a case, I would like to define a >> subclass >> relationship between 'b' and 'a', but this doesn't work (because 'f' >> is not a class >> parameter of 'g'). >> >> Johannes showed me the following "pattern" which is used e.g. in >> Real_Vector_Space: >> >> class a0 = >> fixes f :: "'a => nat" >> >> class a = >> assumes ... >> >> class b = a0 + >> assumes "f = foo g" (* the implementation of 'f' in terms of 'g' *) >> and ... >> begin >> >> subclass a >> proof ... >> >> end >> >> This works well, but comes at the cost of having to duplicate the 'f = >> foo g' line in >> every instantiation of some type for 'b'. Additionally, when using >> 'f', type inference >> will give me a class constraint 'a0' which does not carry the >> necessary assumptions. >> >> My question now is whether this is common enough that it warrants a >> "default >> implementation" mechanism, in the sense that one could specify the >> implementation of 'f' >> in terms of 'g' "once and for all", and not having to define and prove >> it everywhere. This >> could potentially also make sense if just one class is involved: >> >> class eq = >> fixes eq :: "'a => 'a => bool" >> and neq :: "'a => 'a => bool" >> assumes "neq x y <--> ~(eq x y)" >> >> >> Lars >> -- PGP available: http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

**Attachment:
signature.asc**

**Follow-Ups**:**Re: [isabelle] Default implementations for instances***From:*Andreas Lochbihler

**References**:**[isabelle] Default implementations for instances***From:*Lars Hupel

**Re: [isabelle] Default implementations for instances***From:*Andreas Lochbihler

- Previous by Date: Re: [isabelle] Default implementations for instances
- Next by Date: [isabelle] Working with SML's Word8Array and al
- Previous by Thread: Re: [isabelle] Default implementations for instances
- Next by Thread: Re: [isabelle] Default implementations for instances
- 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