[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 ...

  subclass a
  proof ...


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)"


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