在Isabelle中定义不同类型的不相交联合 [英] Defining disjoint union of different types in Isabelle and more

问题描述

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

I asked a series of question to get to the point I can define the following simple model in Isabelle, But I still stuck in getting what I wanted. I try to very briefly describe the problem with an example:

假设我有两个班级 Person 和 Car ， Person 拥有汽车，还有驱动器汽车.因此，我需要以下类型/集:

Suppose I have two classes Person and Car, Person owns cars and also drives cars. So I need the following types/sets:

人员

汽车

拥有(*具有将人与汽车"相关的元素*)

owns (* owns relates elements of Person to Car *)

驱动器(*驱动器也将Person的元素与汽车相关*)

drives (* drives relate elements of Person to car as well *)

问题:

我想在伊莎贝尔(Isabelle)中举例说明上面的例子，它提供了以下灵活性:

I would like to formulate above example in Isabelle is a way that provides the following flexibilities:

1. 使我能够定义一些约束；例如:如果某人拥有汽车，那么他/她一定会开车.我可以使用使我能够定义一个新集合/类型，即 C ，其元素是 Car 和 owns 的元素的不交集并集. 这是我第一个卡住的地方: Car 和 owns 是不同的类型，那么如何合并它们呢?

   Enable me to define a new set/type namely C whose elements are disjoint union of elements of Car and owns. This is the first place I stuck: Car and owns are different types, so how I can union them?

   能够以数字(2)多次继续该过程；例如，定义一个新的类型/集，即 D ，它是 C 和 drives 的不相交的并集.

   Be able to continue the process numerous time in number (2); for example, define a new type/set namely D which is disjoint union of C and drives.

   在数字(2)和(3)中，我想保留新定义的集合/类型的元素的属性/特性；例如，如果我要为一个人定义一个属性 age (请参阅

   In number (2) and (3), I would like to keep the properties/characteristics of the elements of newly defined sets/types; for example, if I would have defined a property age for a Person (see here), I would like the elements of C retain this property in the sense that I can access this property for the elements in C whose type are Person. Consequently, if o1 is an element in C whose type is owns, I would like to access the source (i.e., the Person) and the target (the Car) that are related by o1.

   如果有任何意见和建议，我将不胜感激.

   I would appreciate any comments and suggestions.

   推荐答案

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

   There is the sum-type, written 'a + 'b, in Isabelle/HOL that allows you to combine elements of two different types into a new one. The two constructors of the sum type are

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

   用于向左注入和

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

   右插入.使用sum-type，您可以例如将数字nat list与纯数字nat的列表组合以获得(nat list) + nat.由于列表提供功能length :: 'a list => nat，因此您仍然可以在您知道它们是列表的不相加和元素上使用此功能.为了获取此信息(即，您查看的元素是列表还是纯数字)，我们通常使用 pattern-matching .

   for inject right. Using the sum-type you could for example combine lists of numbers nat list with plain numbers nat to obtain (nat list) + nat. Since lists provide a function length :: 'a list => nat, you can still use this function on elements of the disjoint sum for which you know that they are lists. In order to obtain this information (i.e., whether the element you look at is a list or a plain number) we typically use pattern-matching.

   如果当前元素是列表，则以下函数将计算列表的长度，否则仅返回其表示的数字.

   The following function would compute the length of the list if the current element is a list and just return the number it represents, otherwise.

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

   这篇关于在Isabelle中定义不同类型的不相交联合的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！