Your answer is one click away!

lburski February 2016
### range restriction/domain restriction in Isabelle

I am trying to input a schema into Isabelle however when I add range restriction or domain restriction into the theorem prover it doesn't want to parse. I have the following schema in LaTeX:

```
\begin{schema}{VideoShop}
members: \power PERSON \\
rented: PERSON \rel TITLE \\
stockLevel: TITLE \pfun \nat
\where
\dom rented \subseteq members \\
\ran rented \subseteq \dom stockLevel \\
\forall t: \ran rented @ \# (rented \rres \{t\}) \leq stockLevel~t
\end{schema}
```

When inputting this into Isabelle I get the following:

```
locale videoshop =
fixes members :: "PERSON set"
and rented :: "(PERSON * TITLE) set"
and stockLevel :: "(TITLE * nat) set"
assumes "Domain rented \<subseteq> members"
and "Range rented \<subseteq> Domain stockLevel"
and "(\<forall> t. (t \<in> Range rented) \<and> (card (rented \<rhd> {t}) \<le> stockLevel t))"
begin
.....
```

It all parses except for the last expression `\<forall> t.....`

I just don't understand how to add range restriction into Isabelle.

There are multiple problems with your input.

The

`⊳`

symbol you are using in the expression`(rented ⊳ {t})`

is not associated with any operator, so it can't be parsed. I'm not quite sure what it's supposed to mean. From the high-level idea of the specification I'm guessing something along the lines of "all persons who rented a specific title". This can be expressed most easily with a set comprehension:

`{p. (p, t) ∈ rented}`

You translated the bounded universal quantifier into a quantifier containing a conjunction. This is likely not what you want, because it says "for all

`t`

,`t`

is in the range of`rented`

*and*something else". Isabelle has notation for bounded quantifiers.`∀t ∈ Range rented. ...`

You are trying to use

`stockLevel`

as a function, which it isn't. From your LaTeX input I gather that it's supposed to be a partial function. Isabelle calls these`map`

s. The appropriate type is:`TITLE ⇀ nat`

Note the "harpoon" symbol instead of a function arrow. The domain function for maps is called

`dom`

. The second locale assumption can be expressed as:`Range rented ⊆ dom stockLevel`

Given that, you can use

`stockLevel`

as a function from`TITLE`

to`nat option`

.

Asked in February 2016

Viewed 1,457 times

Voted 9

Answered 1 times

Viewed 1,457 times

Voted 9

Answered 1 times