typeclass - 类型类实例化中的现有常量(例如构造函数)

Question

考虑这个伊莎贝尔代码

theory Scratch imports Main begin

datatype Expr = Const nat | Plus Expr Expr

实例化 plus 是很合理的键入 class 以获得 Plus 的良好语法构造函数:

instantiation Expr :: plus
begin
  definition "plus_Exp = Plus"
instance..
end

但是现在，+和 Plus仍然是单独的常量。特别是，我不能(轻松)使用 +在函数定义中，例如

fun swap where
   "swap (Const n) = Const n"
 | "swap (e1 + e2) = e2 + e1"

将打印

Malformed definition:
Non-constructor pattern not allowed in sequential mode.
⋀e1 e2. swap (e1 + e2) = e2 + e1

如何使用现有常量而不是定义新常量来实例化类型类？

Answer 1

Isabelle 中的类型类实例化总是为类型类的参数引入新的常量。因此，你不能说 plus (写作中缀为 + )应与 Plus 相同.但是，您可以反过来，即先实例化类型类，然后再将类型类上的操作声明为数据类型的构造函数。

一个这样的案例可以在理论Extended_Nat中找到。哪里类型enat通过 typedef 手动构建，然后实例化无穷大类型类，最后enat使用 old_rep_datatype 声明为具有两个构造函数的数据类型.然而，这是没有类型变量的非递归数据类型的一个非常简单的情况。对于您的表达式示例，我建议您执行以下操作:

定义类型 expr_aux与 datatype expr_aux = Const_aux nat | Plus_aux expr_aux expr_aux .

定义一个 expr作为 expr_aux 的类型副本与 typedef expr = "UNIV :: expr_aux set"和 setup_lifting type_definition_expr .

升降构造器Const_aux至 expr带吊装包:lift_definition Const :: "nat => expr" is Const_aux .

实例化类型类 plus :

instantiation expr :: plus begin
lift_definition plus_expr :: "expr => expr => expr" is Plus_aux .
instance ..
end

注册 expr作为 old_rep_datatype expr Const "plus :: expr => _" 的数据类型和适当的证明(使用 transfer )。

定义一个 abbreviation Plus :: "expr => expr => expr" where "Plus == plus"

显然，这是非常乏味的。如果只想在函数中使用模式匹配，可以使用 free_constructor命令注册构造函数 Const和 plus :: expr => expr => expr作为 expr 的新构造函数实例化之后。如果然后添加“Plus = plus”作为简单规则，这应该几乎与乏味的方式一样好。然而，我不知道各种包(特别是 case 语法)如何处理构造函数的这种重新注册。