*To*: Lars Hupel <hupel at in.tum.de>, <isabelle-users at cl.cam.ac.uk>*Subject*: Re: [isabelle] Default implementations for instances*From*: Andreas Lochbihler <andreas.lochbihler at inf.ethz.ch>*Date*: Thu, 10 Apr 2014 17:04:22 +0200*In-reply-to*: <c318b460c1f157ccc49027532bc01ecb-EhVcX1hCQQpcRwURGhY3AF9BdAJSS1xcXF9EBlw1WENZS1kNVkFyBktcXjBeQkwFXllQQ19W-webmailer2@server02.webmailer.hosteurope.de>*References*: <c318b460c1f157ccc49027532bc01ecb-EhVcX1hCQQpcRwURGhY3AF9BdAJSS1xcXF9EBlw1WENZS1kNVkFyBktcXjBeQkwFXllQQ19W-webmailer2@server02.webmailer.hosteurope.de>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:24.0) Gecko/20100101 Thunderbird/24.4.0

Hi Lars, I have longed for a similar mechanism for default implementations in two situations:

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

**Follow-Ups**:**Re: [isabelle] Default implementations for instances***From:*Florian Haftmann

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

- Previous by Date: [isabelle] Default implementations for instances
- Next by Date: [isabelle] system of representatives of an equivalence relation
- Previous by Thread: [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