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.

Answers


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

Search




Leave an answer