从“值”到“引理”

Question

我有一个相当大的术语foo。当我打字时

value "foo"

然后 Isabelle 计算foo出一个值，例如foo_value。我现在想证明以下引理。

lemma "foo = foo_value"

我应该使用什么证明方法？我尝试过try，但超时了。我想我可以通过展开 中出现的各种定义来手动进行foo，但我肯定应该能够利用该value命令正在使用的任何机制，对吧？

Answer 1

对应于 的不同评估机制，共有三种证明方法value：

• eval使用代码生成器；它对应于value [code]. 如果生成的 ML 代码的计算结果为 ，则证明成功True。
• normalization将语句编译为 ML 中的符号规范化引擎。它模仿value [nbe].
• code_simp使用伊莎贝尔简化器作为求值器。它对应于value [simp].

代码生成教程更详细地描述了这些证明方法。eval其normalization行为就像神谕，即它们绕过 Isabelle 的内核，而 的每个评估步骤都code_simp经过内核。通常，eval比 更快normalization并且normalization比 更快code_simp。