0

假设我在 Isabelle 中有以下代码：

typedecl type1
typedecl type2
typedecl type3

consts 
  A::"type1 set"
  B::"type2 set"

当我想对 A 和 B 使用联合操作时，如下所示：

axiomatization where
 c0: "A ∪ B = {}"

由于 A 和 B 是不同类型的集合，因此我得到了类型冲突的错误，这是有道理的！作为一种解决方法，我想将强制转换 A 和 B 都输入为“type3”类型的集合，这样我就可以对它们应用联合操作。在这个具体的例子中，这种类型转换在 isabelle 中是如何实现的，以及一般情况下是如何实现的。

谢谢

4

1 回答 1

3

类型转换需要类型之间的显式函数，例如，

consts cast_A :: "type1 ⇒ type3"
consts cast_B :: "type2 ⇒ type3"

使用这些函数，您可以如下陈述您的公理：

axiomatization where
 c0: "cast_A ` A ∪ cast_B ` B = {}"

Isabelle 也可以自动插入这样的强制函数，但你必须先启用它：

declare
  [[coercion_enabled]]
  [[coercion cast_A, coercion cast_B]]
  [[coercion_map image]]

这三个声明执行以下操作

  1. 启用强制推理算法。
  2. 将函数声明为强制函数cast_A，cast_B即强制推理可以在需要时插入它们。
  3. 将函数image（写为 ` 中缀）声明为强制转换的映射函数。这些映射函数允许推理系统对类型构造函数的参数应用强制。在这里，声明允许通过对所有元素应用强制函数来强制集。

有了这些准备，公理就可以写成：

axiomatization where
 c0: "A ∪ B = {}"

然而，强制插入只是从输入符号中去除混乱的一种手段。强制在定理中是明确的，您的证明必须处理它们。如果你看定理c0，你会看到强制。

最后对这些嵌入进行评论。预定义的 sum 类型type1 + type2完全由 type 的所有元素以及分别具有强制转换函数和type1的 type组成。因此，如果您的类型除了作为 and 的并集之外没有其他用途，那么 sum 类型可能更便于使用。type2InlInrtype3type1type2

另请注意，您的公理表示集合A和B是空的。

于 2014-11-11T10:17:47.313 回答