在伊莎贝尔，为什么这个简化引理没有被取代？

Question

我正在学习 Isabelle "Programming and Proving" 教程，接下来要学习 Ex2.10，您必须在其中得出描述 "exploded" 树中节点数的方程式。

我对此采取的方法是为树中的内部节点和叶节点创建单独的表达式，并且正在为树中的内部节点数进行证明，例如：

lemma dddq: " a>0 ⟶ (nodes_noleaf (explode a b) = (ptser (a - 1) (2::nat)) + ((2 ^ a) * (nodes_noleaf b)))"
apply(induction a)
apply(simp)
apply(simp add:eeei eeed eeej eeek )

这使得证明状态如下：

goal (1 subgoal):
 1. ⋀a. 0 < a ⟶ nodes_noleaf (explode a b) = ptser (a - Suc 0) 2 + 2 ^ a * nodes_noleaf b ⟹
     Suc (2 * nodes_noleaf (explode a b)) = ptser a 2 + 2 * 2 ^ a * nodes_noleaf b

现在，我还创建（并成功证明）了一个应该用 (Suc (2 * ((ptser (a - Suc 0) 2) + 2 ^ a * nodes_noleaf b)))) 替换 ptser a 2 + 2 * 2 ^ a * nodes_noleaf b 的引理，例如：

lemma eeek: "∀ a b . a>0 ⟶ (((ptser a 2) + 2 * 2 ^ a * nodes_noleaf b) = (Suc (2 * ((ptser (a - Suc 0) 2) + 2 ^ a * nodes_noleaf b))))"
apply(auto)
apply(simp add: ddddd)
done

但是，将其添加到 dddq 的简化列表中没有任何作用，而且我不明白为什么。

附加定义..

fun nodes_noleaf:: "tree0 ⇒ nat" where
"nodes_noleaf Tip = 0"|
"nodes_noleaf (Node a b) = (add 1 (add (nodes_noleaf a) (nodes_noleaf b)))"

fun explode:: "nat ⇒ tree0 ⇒ tree0" where
"explode 0 t = t" |
"explode (Suc n) t = explode n (Node t t)"

fun ptser:: "nat ⇒ nat ⇒ nat" where
"ptser 0 b = b^0" |
"ptser a b = b^a + (ptser (a - 1) b)"

Answer 1

你的引理 eeek 是条件重写规则，因为它只能在简化器可以证明 a > 0 成立时应用。但是，在您的目标状态下，您没有假设 a > 0。 0 < a 是归纳假设的先决条件（--> 结合比 ==> 强），这就是为什么 simp 也不应用归纳假设。

由于问题没有包含你的目标的所有定义，所以很难确定确切的原因。尽管如此，我建议从 dddq 中删除假设 a > 0 并证明一个更强的陈述。

风格评论：尝试使用自然演绎框架的连接词!!和==>，而不是显式全称量词和-->。简化器知道如何将它们转换回 !! 和 ==>，但其他证明方法不会自动执行此操作。因此，使用 !! 和 ==> 将为您节省以后的样板证明步骤。

在伊莎贝尔，为什么这个简化引理没有被取代？

In isabelle, why is this simplification lemma not being substituted?

isabelle