如何用偏函数证明引理？

Question

你能建议如何证明这个简单的引理吗？

datatype val = BVal bool | IVal int

lemma the_unif:
"the (x :: val option) = the (y :: val option) ⟹ x = y"
  apply (induct x; induct y)
  apply simp

我试图通过归纳来证明它，但我坚持案例 ⋀option. the None = the (Some option) ⟹ None = Some option。

option 可能等于 BVal x 或 IVal x。它永远不会等于 the None。所以在这种情况下假设总是有错误的价值。

更新：

我可以证明以下引理：

lemma the_none_ne_the_some:
  "x ≠ the None ⟹ the None ≠ the (Some x)"
  by simp

所以我想，第一个引理也可以被证明。

无法证明一般引理，因为它确实不成立：

lemma the_unif:
  "the x = the y ⟹ x = y"

一个反例：

x = None
y = Some (the None)

但在第一个引理中，x 和 y 都不能等于 Some (the None)。所以我找不到第一个引理的反例。

哦，我知道了，我可以证明下面的引理：

lemma the_unif:
  "x ≠ Some (the None) ⟹ y ≠ Some (the None) ⟹ the x = the y ⟹ x = y"
  by (induct x; induct y; simp)

但是如何证明x :: val option蕴含x ≠ Some (the None)呢？

更新 2：

看来无法证明：

lemma val_not_the_none:
  "x = BVal b ∨ x = IVal i ⟹ x ≠ the None"

但是如果引理不成立那么它们一定有反例？你能提供一个吗？

Answer 1

你想证明的根本不成立。 the None 未指定 - 本质上，您无法证明任何不平凡的事情。因此，说 "it will never be equal to the None" 是空洞的，因为你不知道 the None 是什么。

如何用偏函数证明引理？

How to prove lemmas with partial functions?

isabelle