如何在伊莎贝尔类型铸造是可能的 [英] How type casting is possible in isabelle

问题描述

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

Supose I have the following code in Isabelle:

typedecl type1
typedecl type2
typedecl type3

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

当我想使用A和B的联合操作如下：

When I want to use union operation with A and B as bellow:

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

不同类型，我得到类型冲突的错误这是有道理的！作为解决方法我想键入cast A和B都成为类型type3的集合，所以我可以对它们应用联合操作。

Since A and B are sets of different types, I get an error of clash of types which makes sense! As a workaround I want to type cast A and B to both become sets of type "type3", so I can apply union operations to them. How this type casting is possible in isabelle in this specific example, and how it is possible in general.

感谢

推荐答案

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

Type casts require explicit functions between the types, say,

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

函数，你可以如下所示来描述你的公理：

Using these functions, you can state your axiom as follows:

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

Isabelle也可以自动插入这种强制函数，

Isabelle can also automatically insert such coercion functions, but you have to enable it first:

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

<

These three declarations do the following

1. 启用强制推理算法。


2. 声明函数 cast_A code> cast_B 作为强制函数，即强制推断可以根据需要插入它们。


3. 声明函数 image （中缀为`）作为强制的映射函数。这些映射函数允许推理系统对类型构造函数的参数应用强制。这里，声明允许通过对其所有元素应用强制函数来强制集合。



1. Enable the coercion inference algorithm.
2. Declare the functions cast_A and cast_B as coercion functions, i.e., coercion inference may insert them if needed.
3. Declare the function image (written infix as ` ) as a map function for coercions. These map functions allow the inference system to apply coercions to the parameters of type constructors. Here, the declaration allows to coerce sets by applying a coercion function to all its elements.

通过这些准备，公理可以被写如前：

With these preparations, the axiom can be written as before:

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

但是，强制插入只是一种消除输入符号混乱的方法。强制在定理中是明确的，你的证明必须处理它们。如果你看定理 c0 ，你会看到强制。

However, coercion insertion is only a means to remove clutter from the input notation. The coercions are explicit in the theorem and your proofs have to deal with them. If you look at the theorem c0, you will see the coercions.

最后，对这些嵌入的评论。预定义和类型 type1 + type2 完全由类型 type1 的所有元素和类型<$ c $分别使用cast函数 Inl 和 Inr 分别创建c> type2 所以，如果你的类型 type3 没有别的目的，而是 type1 和 type2

Finally a comment on these kinds of embedings. The predefined sum type type1 + type2 consists exactly of all the elements of type type1 and those of type type2 with the cast functions Inl and Inr, respectively. So, if your type type3 has no other purpose than being the union of type1 and type2, the sum type might be more convenient to work with.

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

Also note that your axiom expresses that the sets A and B are empty.

这篇关于如何在伊莎贝尔类型铸造是可能的的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！