定义伊莎贝尔和更多不同类型的不相交的结合
定义伊莎贝尔和更多不同类型的不相交的结合
提问于 2014-11-14 09:22:55
我问了一系列的问题，我可以在Isabelle中定义以下简单的模型，但我仍然坚持要得到我想要的。我试着用一个例子来简单地描述这个问题：
示例：
假设我有两类人和车，人拥有汽车，也有驾驶汽车。因此，我需要下列类型/集合：
人物
小汽车
拥有(*拥有人与汽车相关的要素*)
驱动器(*驱动器也与人与汽车相关*)
问题：
在Isabelle中，我想用上面的例子来说明提供以下灵活性的方法：
- 请允许我定义一些约束；例如:如果一个人拥有一辆汽车，他/她肯定会驾驶这辆车。我可以通过使用来自here的善意的回答来做到这一点。
- 请允许我定义一种新的集合/类型，即C，它的元素是不相交的汽车元素和所有者元素的结合。这个是我第一个碰到的地方:汽车和车主都是不同类型的，所以我如何将它们结合起来呢？
- 能够在数字(2)中多次继续这个过程；例如，定义一个新的类型/集，即D，它是C和驱动器的不相交的结合。
在数字(2)和(3)中，我希望保留新定义的集合/类型的元素的属性/特征；例如，如果我为一个人定义了一个属性年龄(请参见here)，我希望C元素保留该属性，因为我可以访问属于Person类型的C中的元素。因此，如果o1是一个类型为o1的C元素，我希望访问o1相关的源(即Person)和目标( Car)。
如有任何意见和建议，我将不胜感激。
回答 1
Stack Overflow用户
回答已采纳
发布于 2014-11-14 17:10:42
在Isabelle/HOL中有一个求和类型(写为'a + 'b )，它允许您将两种不同类型的元素组合成一个新类型。和类型的两个构造函数是
Inl :: 'a => 'a + 'b注射左和
Inr :: 'b => 'a + 'b打右针。例如，使用和类型，您可以将数字列表nat list与普通数字nat组合起来，以获得(nat list) + nat。由于lists提供了一个函数length :: 'a list => nat，所以您仍然可以在不相交和的元素上使用该函数，因为您知道它们是列表。为了获得此信息(即，您所查看的元素是列表还是普通数字)，我们通常使用模式匹配。
如果当前元素是一个列表，下面的函数将计算列表的长度，然后返回它所代表的数字，否则。
fun maybe_length :: "(nat list) + nat => nat"
where
"maybe_length (Inl xs) = length xs" |
"maybe_length (Inr n) = n"页面原文内容由Stack Overflow提供。腾讯云小微IT领域专用引擎提供翻译支持
原文链接：
https://stackoverflow.com/questions/26926632
复制相关文章
相似问题
腾讯云开发者
