```
theory Regular_Exp
imports Regular_Set
begin
datatype (atoms: 'a) rexp =
is_Zero: Zero |
is_One: One |
Atom 'a |
Plus "('a rexp)" "('a rexp)" |
Times "('a rexp)" "('a rexp)" |
Star "('a rexp)"
instantiation rexp :: (order) "{order}"
begin
...
end
```

For the code above, I have several misunderstanding.

- why atoms in datatype could return a set, in the tutorial the parameter just means the variable.
- What is the role of first and second order in the class instantiation.

any helps would be appreciated

I have no clue what you are talking about. In

```
instantiation rexp :: (order) "order"
```

If you think about applying it to `'a rexp`

: The first `(order)`

is a constraint about `'a`

(in this case, `'a`

must be equipped with an order) and the second `order`

is the constraint you add to `rexp`

. In this case if the case type has an order, then rexp also has an order

Thank you very much. You mean every rexp here is type order now like Zero is an order, One is an order.

And rexp is a name of order class.

What is the function of is_Zero, is_One and atoms play in the datatype.

No, this is not what I mean…

`Zero`

and `One`

are elements of a type called `rexp`

parametrized by another type

and `is_Zero`

and `is_One`

are discriminators (see here)

and atoms returns the set of all atoms in the rexp formula

Last updated: Feb 27 2024 at 08:17 UTC