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

i'm working through isabelle "programming , proving" tutorial, , coming ex2.10, have arrive @ equation discribing number of nodes in "exploded" tree.

the approach i've taken create separate expressions internal , leaf nodes in tree, , working on proof number of internal nodes in tree, such:

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

and leaves proof state following:

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

now, created (and proved) lemma should replace ptser 2 + 2 * 2 ^ * nodes_noleaf b (suc (2 * ((ptser (a - suc 0) 2) + 2 ^ * nodes_noleaf b)))), such:

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

however, adding list of simplifications dddq nothing, , don't see reason why.

---

additional definitions..

fun nodes_noleaf:: "tree0 ⇒ nat" "nodes_noleaf tip = 0"| "nodes_noleaf (node b) = (add 1 (add (nodes_noleaf a) (nodes_noleaf b)))"  fun explode:: "nat ⇒ tree0 ⇒ tree0" "explode 0 t = t" | "explode (suc n) t = explode n (node t t)"  fun ptser:: "nat ⇒ nat ⇒ nat" "ptser 0 b = b^0" | "ptser b = b^a + (ptser (a - 1) b)" 

your lemma eeek conditional rewrite rule, because can applied when simplifier can prove a > 0 holds. in goal state, however, not have assumption a > 0. 0 < a precondition induction hypothesis (--> binds stronger ==>), why simp not apply induction hypothesis either.

since question not contain definitions of goal, hard pinpoint exact reason. nevertheless, suggest drop assumption a > 0 dddq , prove stronger statement.

a comment on style: try use connectives !! , ==> of natural deduction framework rather explicit universal quantifiers , -->. simplifier knows how convert them !! , ==>, other proof methods not automatically. thus, using !! , ==> save boilerplate proof steps later on.