伊莎贝尔如何进行类型转换

Question

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

typedecl type1
typedecl type2
typedecl type3

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

当我想对 A 和 B 使用联合操作时：

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

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

谢谢

Answer 1

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

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 完全由 type1 类型的所有元素和 type2 类型的所有元素组成，分别具有强制转换函数 Inl 和 Inr。因此，如果您的类型 type3 除了作为 type1 和 type2 的联合之外没有其他用途，那么 sum 类型可能更便于使用。

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