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

问题描述

考虑这个伊莎贝尔代码

theory Scratch imports Main begin

datatype Expr = Const nat | Plus Expr Expr

实例化 plus 类型类以获得 Plus 构造函数的良好语法是非常合理的:

it is quite reasonable to instantiate the plus type class to get nice syntax for the Plus constructor:

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

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

But now, + and Plus are still separate constants. In particular, I cannot (easily) use + in a function definition, e.g.

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

如何使用现有常量实例化类型类而不是定义一个新的常量?

How can I instantiate a type class with an existing constant instead of defining a new one?

推荐答案

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

Type class instantiations in Isabelle always introduce new constants for the parameters of the type class. Thus, you cannot say that plus (written infix as +) shall be the same as Plus. However, you can go the other way around, namely instantiate the type class first and only later declare the operations on the type class as the constructors of the datatype.

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

One such case can be found in the theory Extended_Nat where the type enat is constructed manually via a typedef, then the infinity type class is instantiated, and finally enat is declared as a datatype with two constructors using old_rep_datatype. However, this is a very simple case of a non-recursive datatype without type variables. In case of your expression example, I recommend that you do the following:

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

使用 typedef expr = "UNIV :: expr_aux set" 和 将 expr 定义为 expr_aux 的类型副本>setup_lifting type_definition_expr.

Define a expr as a type copy of expr_aux with typedef expr = "UNIV :: expr_aux set" and setup_lifting type_definition_expr.

使用提升包将构造函数 Const_aux 提升到 expr: lift_definition Const :: "nat => expr" is Const_aux .代码>

Lift the constructor Const_aux to expr with the lifting package: 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

1. 使用 old_rep_datatype expr Const "plus :: expr => _" 和适当的证明(使用 transfer).

1. Register expr as a datatype with old_rep_datatype expr Const "plus :: expr => _" and an appropriate proof (use transfer).

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

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

Obviously, this is very tedious. If you just want to use pattern matching in functions, you can use the free_constructor command to register the constructors Const and plus :: expr => expr => expr as new constructors of expr after the instantiation. If you then add "Plus = plus" as a simp rule, this should be almost as good as the tedious way. Yet, I do not know how well the various packages (in particular case syntax) cope with this re-registration of the constructors.

这篇关于类型类实例化中的现有常量(例如构造函数)的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持！