在 Isabelle 中定义重载常量 [英] Defining overloaded constants in Isabelle

问题描述

如何在 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?

例如，我可能想定义一个类型为 'a ⇒ bool 的函数 is_default，其中每个不同的类型 'a 都有一个可能不同的默认值".(为了论证起见，我还假设诸如 zero 之类的现有概念不适合.)

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

推荐答案

这种重载看起来非常适合类型类.首先你为你想要的函数定义一个类型类 is_default:

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

和列表

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

这篇关于在 Isabelle 中定义重载常量的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！