我是Isabelle/HOL的新手，仍在研究prog-prov练习。与此同时，我正在将这些证明技术应用于组合词的问题。我观察到"价值"和"引理"之间的行为(就效率而言)非常不同。
可以解释一下这两个命令之间的不同评估/搜索策略吗？
有没有办法在"引理"的证明中使用"值"的速度？
当然，我问是因为(到目前为止)我在文档中还没有找到答案。记录和解释这种效率差异的手册是什么？
这是重现问题的最小源代码。
theory SlowLemma
imports Main
begin
(* Alphabet for Motzkin words. *)
datatype alphabet = up | lv | dn
(* Keep the [...] notation for lists. *)
no_notation Cons (infixr "#" 65) and append (infixr "@" 65)
primrec count :: "'a ⇒ 'a list ⇒ nat" where
"count _ Nil = 0" |
"count s (Cons h q) = (if h = s then Suc (count s q) else count s q)"
(* prefix n l simply returns undefined if n > length l. *)
fun prefix :: "'a list ⇒ nat ⇒ 'a list" where
"prefix _ 0 = []" |
"prefix (Cons h q) (Suc n) = Cons h (prefix q n)"
definition M_ex_7 :: "alphabet list" where
"M_ex_7 ≡ [lv, lv, up, up, lv, dn, dn]"
definition M_ex_19 :: "alphabet list" where
"M_ex_19 ≡ [lv, lv, up, up, lv, up, lv, dn, lv, dn, lv, up, dn, dn, lv, up, dn, lv, lv]"
fun height :: "alphabet list ⇒ int" where
"height w = (int (count up w + count up w)) - (int (count dn w + count dn w))"
primrec is_pre_M :: "alphabet list ⇒ nat ⇒ bool" where
"is_pre_M _ (0 :: nat) = True"
| "is_pre_M w (Suc n) = (let w' = prefix w (Suc n) in is_pre_M w' n ∧ height w' ≥ 0)"
fun is_M :: "alphabet list ⇒ bool" where
"is_M w = (is_pre_M w (length w) ∧ height w = 0)"
(* These two calls to value are fast. *)
value "is_M M_ex_7"
value "is_M M_ex_19"
(* This first lemma goes fast. *)
lemma is_M_M_ex_7: "is_M M_ex_7"
by (simp add: M_ex_7_def)
(* This second lemma takes five minutes. *)
lemma is_M_M_ex_19: "is_M M_ex_19"
by (simp add: M_ex_19_def)
end
simp是一种通过证明内核的证明方法，即每一步都必须证明。对于长时间重写链，这可能非常昂贵。
另一方面，value尽可能使用代码生成器。所有使用的常量都转换为 ML 代码，然后执行。你必须相信结果，即它没有通过内核，可能是错误的。
等效于value作为证明方法是eval。因此，加快证明速度的一种简单方法是使用它：
lemma is_M_M_ex_19: "is_M M_ex_19"
by eval
伊莎贝尔社区对是否应该使用它的意见不一。有人说它类似于axiomatization(因为你必须信任它)，其他人认为如果通过内核的速度非常慢，这是一种合理的方法。每个人都同意，尽管您必须非常小心代码生成器的自定义设置(您还没有这样做，所以应该没问题)。
有中间立场：code_simp方法将设置simp仅使用eval将使用的方程。这意味着：simp规则集要小得多，同时仍然通过内核。在您的情况下，它实际上与by eval相同的速度，所以我强烈建议这样做：
lemma is_M_M_ex_19: "is_M M_ex_19"
by code_simp
在您的情况下，code_simp比simp快得多的原因是 simproc 在嵌套let表达式的数量上具有指数级运行时。因此，另一种解决方案是使用simp add: Let_def来展开let表达式。
编辑以反映Andreas Lochbihler的评论