CODEWITHSUNDEEP
isabelle
thor
thor

Reputation: 22460

How to state a lemma about equiv in Isabelle

I am trying to learn Isabelle notation and syntax from its documentation. In particular, I am trying to state a lemma using the equivalence notation (equiv in main.pdf of Isabelle 2020).

equiv  :: 'a set ⇒ ('a × 'a) set ⇒ bool

The lemma does not have to be useful, but I was hoping to get the grammar right. I tried to fill the blanks with something as follows, hoping to state that equality is an equivalence relation:

lemma "equiv nat (=)"

The attempt wasn't successful and generates this error:

Type unification failed: Clash of types "_ ⇒ _" and "_ set"

Type error in application: incompatible operand type

Operator:  equiv :: ??'a set ⇒ (??'a × ??'a) set ⇒ bool
Operand:   nat :: int ⇒ nat

My questions are:

How to state the equivalence about equality correctly?

More generally, how does one go about discovering the right way to use the basic notation or syntax such as those in Main?

(I am interested in notation only here, not necessarily proving anything)

Upvotes: 0

Views: 122

Answers (1)

Mathias Fleury
Mathias Fleury

Reputation: 2261

The first critical thing when trying notations is to look at types or type error messages:

Operator:  equiv :: ??'a set ⇒ (??'a × ??'a) set ⇒ bool
Operand:   nat :: int ⇒ nat

shows that nat has type int ⇒ nat, while equiv expects the first argument to have type ?'a set. So you somehow want a set of natural numbers, instead of the function that converts an integer to a natural number.

How to fix that problem? Either you already know that UNIV exists for such purpose or you search for example on Find facts, based on some intuition on the name.

Once you have changed that, you will see a similar typing problem for equality that you can easily fix.

Upvotes: 1

Related Questions