我问了一系列问题，直到我可以在 Isabelle 中定义以下简单模型，但我仍然坚持得到我想要的东西。我尝试用一个例子来非常简短地描述这个问题：
Example:
假设我有两节课Person and Car, Person owns汽车还有drives汽车。所以我需要以下类型/集：
Person
Car
owns(* 拥有 Person 与 Car 的相关元素 *)
drives（* 驱动器也将人的元素与汽车相关联 *）
Problem:
我想用 Isabelle 来表述上面的例子是一种提供以下灵活性的方式：
使我能够定义一些约束；例如：如果一个人拥有一辆车，他/她肯定会驾驶这辆车。我可以通过使用来自的友善回答来做到这一点here.
让我能够定义一个新的集合/类型C其元素是元素的不相交并Car and owns. This 是我第一个卡住的地方: Car and owns是不同的类型，那么我如何将它们结合起来？
能够多次继续该过程（2）；例如，定义一个新类型/集合，即D这是 的不相交并集C and drives.
在第（2）和（3）中，我想保留新定义的集合/类型的元素的属性/特征；例如，如果我定义了一个属性age对于一个人（参见here），我想要以下元素C保留此属性是因为我可以访问其中元素的此属性C其类型为 Person。因此，如果 o1 是C其类型是owns，我想访问与 o1 相关的源（即人）和目标（汽车）。
我将不胜感激任何意见和建议。
有 sum-类型，写成'a + 'b，在 Isabelle/HOL 中，允许您将两种不同类型的元素组合成一个新的元素。 sum 类型的两个构造函数是
Inl :: 'a => 'a + 'b
for 向左注射 and
Inr :: 'b => 'a + 'b
for 注射正确。例如，使用 sum-type 您可以组合数字列表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"
本文内容由网友自发贡献，版权归原作者所有，本站不承担相应法律责任。如您发现有涉嫌抄袭侵权的内容，请联系:hwhale#tublm.com(使用前将#替换为@)
