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.

Solution

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