如何陈述《伊莎贝尔》中关于equiv的引理

Question

我正试图从它的文档中学习Isabelle表示法和语法。特别是，我试图使用等价符号来陈述一个引理(Isabelle 2020的main.pdf中的equiv(。

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

引理不一定有用，但我希望语法正确。我试着用以下内容来填补空白，希望说明平等是一种等价关系：

lemma "equiv nat (=)"

尝试未成功，并生成以下错误：

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

我的问题是：

如何正确地陈述关于等式的等价性

更一般地说，如何找到正确的方法来使用基本的表示法或语法，如Main中的那些

(我只对这里的符号感兴趣，不一定能证明什么(

Answer 1

尝试符号时的第一件关键事情是查看类型或类型错误消息：

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

显示nat的类型为int ⇒ nat，而equiv期望第一个参数的类型为?'a set。所以你需要一组自然数，而不是将整数转换为自然数的函数。

如何解决这个问题？要么你已经知道UNIV是为了这个目的而存在的，要么你根据名字的直觉在Find facts上搜索。

一旦你改变了这一点，你就会看到一个类似的平等类型问题，你可以很容易地解决。