在Isabelle中定义重载常量

Question

如何在Isabelle中定义一个函数,该函数具有不同的定义,具体取决于其参数的类型或它所使用的上下文的类型？

例如,我可能想要定义一个is_default带有类型的函数'a ? bool,其中每个不同的类型'a都有一个可能不同的"默认值".(为了论证,我也假设现有的概念zero不合适.)

Answer 1

这种重载看起来非常适合类型类。首先，为所需的函数定义一个类型类is_default：

\n\n

class is_default =\n  fixes is_default :: "\'a \xe2\x87\x92 bool"\n

\n\n

然后引入任意实例。例如，对于布尔值

\n\n

instantiation bool :: is_default\nbegin\ndefinition "is_default (b::bool) \xe2\x9f\xb7 b"\ninstance ..\nend\n

\n\n

并列出

\n\n

instantiation list :: (type) is_default\nbegin\ndefinition "is_default (xs::\'a list) \xe2\x9f\xb7 xs = []"\ninstance ..\nend\n

\n