Defining overloaded constants in Isabelle

isabelle, overloading

Solution

This kind of overloading looks like a perfect fit for type classes. First you define a type class for your desired function `is_default`:

class is_default =
  fixes is_default :: "'a ⇒ bool"

Then you introduce arbitrary instances. E.g., for Booleans

instantiation bool :: is_default
begin
definition "is_default (b::bool) ⟷ b"
instance ..
end

and lists

instantiation list :: (type) is_default
begin
definition "is_default (xs::'a list) ⟷ xs = []"
instance ..
end

Problem

How can one define a function in Isabelle that has a different definition depending on either the type of its argument, or the type of the context it is used in? For example, I might want to define a functions `is_default` with type `'a ⇒ bool`, where each different type `'a` has a potentially different "default value". (I am also assuming, for the sake of argument, that existing concepts such as `zero` are not suitable.)

Original source