Geek asks and answers

Definition of Overloaded Constants in Isabel

How to define a function in Isabelle that has a different definition depending on the type of argument or the type of context in which it is used?

For example, I might need to define functions is_defaultwith a type 'a ⇒ boolwhere each other type 'ahas a potentially different "default value". (I also assume, for the sake of argument, that existing concepts, such as zero, are not appropriate.)

+5
source share
2 answers

Such overloading looks perfect for type classes. First, you define a type class for the desired function is_default:

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

Then you enter arbitrary instances. For example, 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 , , . consts , defs (overloaded) .

:

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

(overloaded), , Isabelle .

defs , , , . :

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

" " Isablle/Isar. , Obua " " , gotchas .

+3

More articles:


All Articles