isabelle - 从 'value' 到 'lemma'

Question

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

value "foo"

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

lemma "foo = foo_value"

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

Answer 1

对应value的不同评估机制，有三种证明方式:

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

tutorial on code generation更详细地描述了这些证明方法。 eval 和 normalization 就像神谕一样，即它们绕过 Isabelle 的内核，而 code_simp 的每个评估步骤都经过内核。通常，eval 比 normalization 快，normalization 比 code_simp 快。