Isabelle синтаксис: оператор не типа функции

Question

Я только начинаю с помощью наборов в Изабелле и у меня есть следующие:

theory telephone 
imports 
Main 
begin 

typedecl NAME 
typedecl TELEPHONE 

record TelephoneBook = 
KNOWN :: " NAME set" 
NUMBER :: "(NAME * TELEPHONE) set" 

locale telephone_book = 
fixes known :: " NAME set" 
and number :: "(NAME * TELEPHONE) set" 
assumes "known = Domain number" 
begin 

definition FindBirthday :: 
"TelephoneBook => TelephoneBook => NAME => TELEPHONE => bool" 
where 
"FindTelephone telephonebook telephonebook' name telephone == (
(name \<in> known) 
∧ 
(telephone = number name) 
)" 

Проблема лежит на линии telephone = number name , где у меня есть сообщение об ошибке

Type unification failed: Clash of types " _ => _" and "_ set" 

Type error in application: operator not of function type 

Operator: number :: (NAME × TELEPHONE) set 
Operand: name :: NAME 

Я пробовал добавленную скобку (telephone = number (name)) или tilda (telephone = number~name), но у нее по-прежнему есть та же проблема.

Я знаю, что номер хочет ИМЯ и ТЕЛЕФОН, но я хочу показать, что определение правильное, если вывод telephone должен быть telephone, когда name является его доменом.

Answer 1

Это именно то, что говорит Изабель, то есть вы не можете использовать набор как функцию, поэтому вы не можете применить аргумент к набору, в вашем случае вы не можете применить name к number. То, что вы можете это

(name, telephone) : number

или

(name, telephone) ∈ number.