在 Isabelle 等中定义不同类型的不相交联合答案

【问题标题】：Defining disjoint union of different types in Isabelle and more在 Isabelle 等中定义不同类型的不相交联合
【发布时间】：2015-01-11 15:30:31
【问题描述】：

我问了一系列问题以达到我可以在 Isabelle 中定义以下简单模型的目的，但我仍然坚持得到我想要的。我试着用一个例子非常简要地描述这个问题：

示例：

假设我有两个类 Person 和 Car，Person 拥有汽车和 drives 汽车。所以我需要以下类型/集合：

人

汽车

拥有（*拥有将 Person 与 Car 相关联的元素 *）

驱动器（*驱动器也将人的元素与汽车相关*）

问题：

我想在 Isabelle 中制定上述示例是一种提供以下灵活性的方式：

让我能够定义一些约束；例如：如果一个人拥有一辆车，他/她肯定会开车。我可以通过使用来自here 的友好回答来做到这一点。
让我能够定义一个新的集合/类型，即 C，其元素是 Car 和 owns 元素的不相交并集。这是我第一个卡住的地方：Car 和 owns 是不同的类型，那么我该如何合并它们呢？
能够多次继续该过程（2）；例如，定义一个新类型/集合，即 D，它是 C 和 drives 的不相交联合。

在数字（2）和（3）中，我想保留新定义的集合/类型的元素的属性/特征；例如，如果我要为 Person 定义一个属性 age（参见 here），我希望 C 的元素保留这个属性，因为我可以为 C 中类型为 Person 的元素访问此属性。因此，如果 o1 是 C 中类型为 owns 的元素，我想访问源（即人）和目标（汽车）由o1相关。

我将不胜感激任何 cmets 和建议。

【问题讨论】：

标签： isabelle isar

【解决方案1】：

在 Isabelle/HOL 中有 sum-type，写为 'a + 'b，它允许您将两种不同类型的元素组合成一个新类型。 sum 类型的两个构造函数是

Inl :: 'a => 'a + 'b

对于向左注入和

Inr :: 'b => 'a + 'b

为注入权。例如，使用 sum 类型，您可以将数字列表 nat list 与普通数字 nat 组合以获得 (nat list) + nat。由于列表提供了函数length :: 'a list => nat，因此您仍然可以在不相交和的元素上使用此函数，您知道它们是列表。为了获取此信息（即，您查看的元素是列表还是普通数字），我们通常使用 pattern-matching。

如果当前元素是一个列表，则以下函数将计算列表的长度，否则只返回它所代表的数字。

fun maybe_length :: "(nat list) + nat => nat"
where
  "maybe_length (Inl xs) = length xs" |
  "maybe_length (Inr n) = n"

【讨论】：