Home Ask Login Register

Developers Planet

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:

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

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))"

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.

Post Status

Asked in February 2016
Viewed 1,457 times
Voted 9
Answered 1 times


Leave an answer

Quote of the day: live life