Использование кортежей в определениях

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" 

Каков наилучший способ использовать кортежи в качестве аргументов в definition?

Answer 1

Использование fun, вероятно, является наименее болезненным способом для этого, пакет определения не распознает шаблоны с левой стороны.

Другой вариант заключается в использовании шаблонов кортежей для лямбда-выражений: my_def ≡ %(a,b). a = b