伊莎贝尔的一组元组

Question

I试图用一个以术语和一组元组作为参数的定义来编写，但我不知道如何显示这组元组

theory fullbb
imports 
Main

begin 
typedecl NAME
typedecl ADDRESS

locale addresbook
begin

definition address :: "NAME set ⇒ (NAME * ADDRESS) set ⇒ bool"
where 
"address name addresses  = (name = dom (addresses))"
end

我得到的错误信息是

Type unification failed: Clash of types "_set" and "_=>_"    
Type error in application: incompatible operand type
Operator: dom :: (??'a => ??'b option) => ??'a set
Operand: addresses :: (NAME x ADDRESS) set

Answer 1

函数dom返回映射的域，映射在HOL中建模为函数'a => 'b option。对于一个关系(即一组元组)，适当的函数称为Domain。因此，只需在定义中使用Domain而不是dom，它应该按预期键入check。

Answer 2

第一步是CNTL-点击相关函数来查看它们所做的事情，并查看它们的类型签名是什么。

对于dom，它带我去Map.thy第40行

definition
  dom :: "('a ~=> 'b) => 'a set" where
  "dom m = {a. m a ~= None}"

看上去你不是在处理元组。在第13行中有这种类型的同义词

type_synonym ('a,'b) "map" = "'a => 'b option" (infixr "~=>" 0)

locale在这里并不重要。我将元组语法更改为：

definition address :: "NAME set => (NAME ~=> ADDRESS) set => bool"
where 
  "address name addresses = (name = dom (addresses))"

我仍然有一个类型错误。这是因为dom需要(NAME ~=> ADDRESS)类型。

definition address :: "NAME set => (NAME ~=> ADDRESS) => bool" 
where 
  "address name addresses = (name = dom (addresses))"

所以，dom不是你想象的那样。