# Developers Planet

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.

larsrh February 2016

There are multiple problems with your input.

1. 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}

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

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