isabelle - 在定义中使用元组

Question

我想创建一个以元组作为参数的定义。

definition my_def :: "('a × 'a) ⇒ bool" where
  "my_def (a, b) ⟷ a = b"

但是，这不被接受。错误信息是

Bad arguments on lhs: "(a, b)"
The error(s) above occurred in definition:
"my_def (a, b) ≡ a = b"

使用fun而不是definition工作，但这不是我想要的。以下表示法也有效，但有点难看：

definition my_def :: "('a × 'a) ⇒ bool" where
  "my_def t ⟷ fst t = snd t"

在 a 中使用元组作为参数的最佳方法是definition什么？

Answer 1

使用fun可能是最不痛苦的方法，定义包无法识别左侧的模式。

另一种选择是对 lambda 表达式使用元组模式： my_def ≡ %(a,b). a = b