Re: [isabelle] Default implementations for instances
On 11/04/14 15:46, Florian Haftmann wrote:
No, please do not triple the number of type classes. It is already now somewhat cumbersome
to instantiate the order type classes for some type 'a foo to get the right sort
constraints on the type parameter (things are already worse for the algebraic type classes).
The most prominent example of this probably is "op <" in the preorder
type class, which is completely determined by the assumption
strict_iff_order. All instantiations have to specify both "op <=" and
"op <" and prove that they are compatible. The theory Partial_Function
even defines a general mk_less operator to that end.
This strict coupling of Orderings.less_eq and Orderings.less is mainly
historic and could be split into two class hierarchies (e.g. strict_*
and reflexive_*, where the existing class »foo« joins the classes
strict_foo and reflexive_foo).
If the situation is pressing enough, this should be seriously considered.
instantiation foo :: (ord) ord ...
instance foo :: (preorder) preorder ...
instance foo :: (order) order ...
instance foo :: (linorder) linorder ...
If you split each of these type classes into three, one would have to write twelve
instance declarations and proofs.
My point was that such default implementations might be convenient for the order
hierarchy. By the way, another example of making constants to type class parameters for
the sake of code generation can be found in the card_UNIV hierarchy in
This archive was generated by a fusion of
Pipermail (Mailman edition) and