在 type_synonym 上实例化类型类

Question

在我的理论开发中，我有一个概念“bar”的函数用于一堆类型（比如，bar_atom，bar_clause 等），所以我想我会使用类型类来抽象它以提高可读性（因为我宁愿只需在任何地方输入“bar”，然后让类型系统找出要使用的函数）。

我试过以下方法：

theory Sat
 imports Main
begin

type_synonym atom = nat

class foo =
  fixes bar :: "'a ⇒ nat"

instantiation atom :: foo begin

end

end

Isabelle在“instantiation atom”处报错，如下：

Bad type name: "Sat.atom"⌂

我知道这已经在How to define a class instance of type_synonym?中得到了部分回答。但是，我希望问题是由已经存在的类型类这一事实引起的。在我的例子中，它是一个自定义且完全本地的类型类，所以我希望在这种情况下，类型同义词上的类型类没有问题。但我无法让它工作。我不介意内联类型同义词，但这似乎也不起作用。它似乎只适用于像“nat”和“int”这样的原始类型。

答案说我也可以定义自己的类型，但如果可以的话，我希望我的基类型保持简单。我假设如果我坚持输入像

atom = nat

之类的同义词，证明会更加自动化，但也许这过于谨慎了？也许当这个理论发展完成后，我想对所使用的类型进行抽象（因为大多数类型同义词可以是不透明的，我认为，只要定义了相等性）然后这就更相关了，但是在这一刻只是一个概念证明，没有必要。

Answer 1

不幸的是，这不起作用。您可以选择使用 nat 实例化类，也可以定义包装器类型。如果是你自己的课，我会推荐前者。