Defining disjoint union of different types in Isabelle and more

Question

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:

Example:

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

Person

Car

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

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

Problem:

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

1. Enable me to define some constraint; for example: if a Person owns a car, he/she definitely drives the car. I can do this by using a kind answer from here.

2. 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?

3. 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.

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.

Saith

Answer 1

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

for inject left and

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

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"

Nembutal