CODEWITHSUNDEEP
settuplesdefinitionisabelle
lburski
lburski

Reputation: 109

Set of tuples in Isabelle

Im trying to write in a definition which takes a term and a set of tuples as argument but I don't know how to display the set of tuples 

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

The error message I get with this is

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

Upvotes: 1

Views: 549

Answers (2)

Andreas Lochbihler
Andreas Lochbihler

Reputation: 5058

The function dom returns the domain of a map, which is modeled in HOL as a function 'a => 'b option. For a relation (i.e., a set of tuples), the appropriate function is called Domain. So just use Domain instead of dom in your definition and it should type-check as expected.

Upvotes: 3

user4655408
user4655408

Reputation:

The first step is to CNTL-click on pertinent functions to see what they do, and see what their type signature is.

For dom, it takes me to line 40 of Map.thy:

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

It's looking like you're not dealing with tuples. There is this type synonym at line 13:

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

The locale is not important here. I change the tuple syntax to this:

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

I still get a type error. It's because dom needs type (NAME ~=> ADDRESS).

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

So, dom is not what you thought it was.

Upvotes: 2

Related Questions