Defining overloaded constants in Isabelle

问题:

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

回答1:

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

回答2:

Isabelle supports overloaded definitions by defining a constant name and then later providing the constant with new definitions for different types. This can be done with the consts command to define the constant name, and then the defs (overloaded) command to provide a partial definition.

For example:

consts is_default :: "'a ⇒ bool"

defs (overloaded) is_default_nat:
  "is_default a ≡ ((a::nat) = 0)"

defs (overloaded) is_default_option:
  "is_default a ≡ (a = None)"

The above will also work without the (overloaded) parameter, but will cause Isabelle to issue a warning.

The defs command is also given a name, which is the name of the theorem generated by Isabelle which contains the definition. This name can then be used in later proofs:

lemma "¬ is_default (Some 3)"
  by (clarsimp simp: is_default_option)

More information is available in section "Constants and definitions" in the Isablle/Isar reference manual. Additionally, there is a paper "Conservative Overloading in Higher-Order Logic" by Obua that discusses some of the implementation details and gotchas in having such a framework without sacrificing soundness.