Re: [isabelle] Default implementations for instances



> 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
Description: OpenPGP digital signature



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