Isabelle语法:运算符不是函数类型

Question

我刚刚开始在Isabelle中使用集合，我有以下内容：

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))或波浪号(telephone = number~name)，但它仍然有同样的问题。

我知道这个数字需要一个NAME和TELEPHONE，但我想表明，当输出telephone应该是telephone时，当name是它的域时，定义是正确的。

Answer 1

这正是Isabelle所说的，即不能将集合用作函数，因此不能将参数应用于集合，在这种情况下，不能将name应用于number。你可能想要的是

(name, telephone) : number

或

CCD_ 10。