В isabelle, почему эта упрощающая лемма не подставляется?

Question

Я работаю над учебником «Программирование и доказательство» Изабеллы, и я прихожу к Ex2.10, где вы должны прийти к уравнению, определяющему количество узлов в «взорванном» дереве.

Подход, который я взял на это, чтобы создать отдельные выражения для внутренних и листовых узлов в дереве, и я работаю на доказательство числа внутренних узлов в дереве, как таковой:

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 

Теперь, я также создал (и успешно доказано) лемму, которая должна заменить ptser a 2 + 2 * 2^a * nodes_noleaf b с (Suc (2 * ((ptser (a - Suc 0) 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 не применяет гипотезу индукции.

Поскольку вопрос не содержит всех определений вашей цели, трудно точно определить причину. Тем не менее, я предлагаю отказаться от предположения a > 0 от dddq и доказать более сильное утверждение.

Комментарий к стилю: попробуйте использовать связки !! и ==> рамки естественного дедукции, а не явные универсальные кванторы и -->. Упроститель знает, как преобразовать их обратно в !! и ==>, но другие методы доказательства не делают это автоматически. Таким образом, используя !! и ==>, вы сможете сэкономить после этого шаги, описанные ниже.