Isabelle函数定义实例分析

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

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

我怎样才能证明一些方程：

f x y = f y x

使用左侧的案例分析？

仅编写 apply(cases of.cases) 对我来说不起作用。我收到一个错误

未定义常量：“f”⌂

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

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

有关该方法的更多信息cases请参阅 Isar-ref 中第 6.5.2 节“证明方法”。