《伊莎贝尔》中函数定义的案例分析

Question

想象一下，我有一个有三种情况的函数定义：

function f where 
eq1 if cond1 
| eq2 if cond2
| eq3 if cond3

我如何证明一些等式：

f x y = f y x

在左手边使用案例分析？

仅仅写申请(cases.f.cases(对我不起作用。我收到了一个错误

未定义的常数："f"⌂

Answer 1

我决定发布我的评论作为答案，试图解决这个问题。

对于您的用例，应该可以使用apply(cases ‹(x, y)› rule: f.cases)(或类似的(。然而，在确认这一点之前，看到一个最小的工作示例会有所帮助。

有关方法cases的更多信息，请参见Isar-ref中的第6.5.2节"证明方法"。

Answer 2

为了补充用户9716869的答案，这里有一个最小的工作示例：

function f where
"f x y = 0" if "x = y" | 
"f x y = Suc 0" if "x ≠ y"
by auto
termination by lexicographic_order
lemma "f x y = f y x"
proof (cases ‹(x, y)› rule: f.cases)
case (1 x y)
then show ?thesis
by simp
next
case (2 x y)
then show ?thesis
by simp
qed