# [isabelle] Default implementations for instances

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

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