0

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

例子：

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

人

车

拥有 （*拥有将人的元素与汽车相关联*）

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

问题：

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

  1. 使我能够定义一些约束；例如：如果一个人拥有一辆车，他/她肯定会开车。我可以通过使用来自这里的友好答案来做到这一点。

  2. 让我能够定义一个新的集合/类型，即C，其元素是Car和owns元素的不相交并集。这是我坚持的第一个地方：Car和owns是不同的类型，那么我该如何合并它们？

  3. 能够在数（2）个中多次继续该过程；例如，定义一个新的类型/集合，即D ，它是C和驱动器的不相交并集。

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

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

4

1 回答 1

1

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

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

用于向左注入和

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

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

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

fun maybe_length :: "(nat list) + nat => nat"
where
  "maybe_length (Inl xs) = length xs" |
  "maybe_length (Inr n) = n"
于 2014-11-14T17:10:42.947 回答