code-generation - 如何用“未定义”常量证明代码正确性引理

Question

鉴于我对代码生成有一个非常简单的定义。它仅针对某些情况定义，否则会引发运行时异常。

definition "blubb a = (if P a then True else undefined)"

现在我想显示blubb正确。应该忽略抛出异常的情况（从我的角度来看，而不是从数学的角度来看）。但是，我最终得到了一个假设某个任意值X是undefined. 以下引理或多或少等同于子目标。我想显示False，因为我想忽略抛出异常（即undefined返回）的情况。

lemma "X = undefined ⟹ False"

这是无法证明的。

  try

Nitpick found a counterexample for card 'a = 1:
 Free variable:
  X = a1

显示可能引发异常或处理的函数正确性的最佳方法是什么undefined？这与这个问题有关。

score 2 · Accepted Answer

undefined是 Isabelle 中的一个常数，你对此一无所知。特别是，您一般无法证明X ≠ undefined.

如果要编写仅对某些输入有效的函数，可以考虑使用'a option类型，如下所示：

definition "blubb a ≡ (if P a then Some True else None)"

然后在您的证明中假设blubb a定义如下：

lemma "∃x. blubb a = Some x ⟹ Q (blubb a)"
  ...

或者简单地说：

lemma "a ∈ dom blubb ⟹ Q (blubb a)"
  ...

blubb a然后可以使用提取的值the (blubb a)。

1 回答 1