伊莎贝尔函数定义的案例分析
伊莎贝尔函数定义的案例分析
提问于 2020-03-14 13:07:46
假设我有一个函数定义，有三种情况：
function f where
eq1 if cond1
| eq2 if cond2
| eq3 if cond3我如何证明一些等式：
f x y = f y x用左手边的案例分析？
只是写应用程序(案例f.cases)对我不起作用。我犯了个错误
未定义常数："f"⌂
回答 2
Stack Overflow用户
发布于 2020-03-17 22:37:04
我决定把我的评论作为回答，试图结束这个问题。
对于您的用例，应该可以使用apply(cases ‹(x, y)› rule: f.cases) (或类似的)。然而，在确认这一点之前，最好能看到一个最低限度的工作示例。
有关方法cases的更多信息，请参见Isar-ref中的6.5.2节“验证方法”。
Stack Overflow用户
发布于 2020-03-19 03:53:35
为了补充order 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页面原文内容由Stack Overflow提供。腾讯云小微IT领域专用引擎提供翻译支持
原文链接：
https://stackoverflow.com/questions/60683091
复制相关文章
相似问题
腾讯云开发者
