考虑这个伊莎贝尔代码
theory Scratch imports Main begin
datatype Expr = Const nat | Plus Expr Expr
实例化plus类型类以获得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
我如何用一个现有的常量实例化一个类型类，而不是定义一个新的常量？
Isabelle中的类型类实例化总是为类型类的参数引入新的常量。因此，您不能说plus（写为infix +）应与相同Plus。但是，您可以采取另一种方法，即首先实例化类型类，然后才将其声明为数据类型的构造函数。
可以在Extended_Nat理论中找到一种这样的情况，其中类型enat是通过a手动构造的typedef，然后实例化了无限类型类，最后enat使用的两个构造函数将其声明为数据类型old_rep_datatype。但是，这是没有类型变量的非递归数据类型的非常简单的情况。对于您的表达式示例，我建议您执行以下操作：
定义一个类expr_aux有datatype expr_aux = Const_aux nat | Plus_aux expr_aux expr_aux。
用和定义一个expr类型副本。expr_auxtypedef 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实例化后。如果您随后添加“加=加”作为简化规则，则这应几乎与乏味的方法一样好。但是，我不知道各种程序包（特别是语法）在处理构造函数的这种重新注册方面效果如何。
本文收集自互联网，转载请注明来源。
如有侵权，请联系 [email protected] 删除。
我来说两句