ограничение диапазона/ограничение домена в Isabelle

Question

Я пытаюсь ввести схему в Изабель, однако, когда я добавляю ограничение диапазона или ограничение домена в теоретическую проверку, он не хочет анализировать. У меня есть следующие схемы в 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} 

При вводе этого в Изабеллу, я получаю следующее:

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

все эти разборов для последнего выражения, кроме \<forall> t.....

Я просто не понять, как добавить ограничение диапазона в Изабель.

Answer 1

С вашим вводом много проблем.

1. ⊳ символ используется в выражении

   (rented ⊳ {t}) 
   

   не связан с любым оператором, поэтому он не может быть разобран. Я не совсем уверен, что это значит. Из идеи высокого уровня спецификации я угадываю что-то вроде «всех лиц, которые арендовали конкретный титул». Это может быть выражено наиболее легко с набором понимания:

   {p. (p, t) ∈ rented} 
   

2. Вы перевели ограниченный квантор в квантора, содержащей конъюнкцию. Это скорее всего не то, что вы хотите, потому что он говорит «для всех t, t находится в диапазоне rentedи что-то еще». Изабель имеет обозначение для ограниченных кванторов.

   ∀t ∈ Range rented. ... 
   

3. Вы пытаетесь использовать stockLevel как функцию, которой нет. Из вашего ввода LaTeX я понимаю, что он должен быть частичной функцией. Изабель называет эти map с. Соответствующий тип:

   TITLE ⇀ nat 
   

   Обратите внимание на символ «гарпун» вместо стрелки функции. Функция домена для карт называется dom. Вторая локаль предположение может быть выражено как:

   Range rented ⊆ dom stockLevel 
   

   Учитывая, что вы можете использовать stockLevel как функцию от TITLE к nat option.