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

Question

我刚开始在 Isabelle 中使用 sets 并且我有以下内容：

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.

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

Isabelle syntax: operator not of function type

types

typeerror

isabelle