Isabelle 中的一组元组

Question

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

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

第一步是 CNTL - 单击相关函数以查看它们的作用，并查看它们的类型签名是什么。

对于dom，我需要line 40 of Map.thy:

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

看起来你不是在处理元组。在 line 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 不是你想象的那样。

Answer 2

函数 dom returns 地图的域，在 HOL 中建模为函数 'a => 'b option。对于关系（即一组元组），适当的函数称为 Domain。因此，只需在您的定义中使用 Domain 而不是 dom，它应该按预期进行类型检查。

Isabelle 中的一组元组

Set of tuples in Isabelle

set

tuples

definition

isabelle