isabelle - 将产品/元组/对类型的变量拆分为应用样式的成员

Question

假设我们正在使用一对类型 ('a × 'a) 并为其定义一个具有模式匹配的 fun。

fun test :: "('a × 'a) ⇒ 'a ⇒ bool" where "test (a,b) c = True"

如果我现在有一个 ('a × 'a) 类型的变量 a_b，我怎样才能将它替换为它的对表示 (a,b ) 在应用样式证明中。例如，显示以下引理的最佳方式是什么？如何将 test a_b c 替换为 test (a,b) c？

lemma "test a_b c = True"

这是否也适用于假设中的对？

lemma "¬ test a_b c ⟹ flying_pigs"

Answer 1

在 a_b 上使用 cases/case_tac 怎么样？