*To*: 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:43:26 +0200*In-reply-to*: <c318b460c1f157ccc49027532bc01ecb-EhVcX1hCQQpcRwURGhY3AF9BdAJSS1xcXF9EBlw1WENZS1kNVkFyBktcXjBeQkwFXllQQ19W-webmailer2@server02.webmailer.hosteurope.de>*Organization*: TU Munich*References*: <c318b460c1f157ccc49027532bc01ecb-EhVcX1hCQQpcRwURGhY3AF9BdAJSS1xcXF9EBlw1WENZS1kNVkFyBktcXjBeQkwFXllQQ19W-webmailer2@server02.webmailer.hosteurope.de>*User-agent*: Mozilla/5.0 (X11; Linux i686; rv:24.0) Gecko/20100101 Thunderbird/24.4.0

> 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)" The story is more complicated since a »definition« in general is not necessarily equational. As example have a look at class complete_lattice where Inf determines Sup and vice versa, but none is characterized equationally in the class' assumes. I hope someday that »permanent_interpretation« inside instantiation targets yields a pattern for default instantiations, but this is music of the future. Cheers, Florian -- PGP available: http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

**Attachment:
signature.asc**

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

- Previous by Date: Re: [isabelle] Definition in (and of) Isabelle/HOL
- Next by Date: Re: [isabelle] Default implementations for instances
- Previous by Thread: Re: [isabelle] Default implementations for instances
- Next by Thread: [isabelle] system of representatives of an equivalence relation
- 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