Proof on tree size using Isabelle

I'm trying to learn a little bit about Isabelle and proofs in general, and it's uses in Programming Language Theory. I'm following a book, "Concrete Semantics with Isabelle/HOL". I'm still in the beggining.

I was able to do the first exercises, but I got to a point where I noticed I just don't know what I'm doing. I just solved a question where I spent some time failing to prove something, than tried changing one little thing and it magically worked. Can someone explain what exactly is happening?

Ok, so here is what the question is basically about:

We had to make a simple tree structure with no data, like:

datatype tree0 = Tip | Node "tree0" "tree0"

The question ask us to make a function nodes t that count the number of nodes and leafs on the tree. Then, it provides a function:

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

And ask us to provide an equation for the number of elements (nodes t) of the exploded tree, based on N and T, and prove that this equation is correct.

The equation I found was: nodes(explode n t) = (2^n)*(nodes t + 1) - 1

Which I tried proving using induction on "n" alone.

lemma aft_tree: "nodes(explode n t) = (2^n)*(nodes t + 1) - 1"
apply(induct n)    
apply(auto)
apply(simp add: exp_grow)
apply(simp add: algebra_simps)

done

After "apply(auto)", the goal changed to:

goal (1 subgoal):
 1. ⋀n. nodes (explode n t) = 2 ^ n + 2 ^ n * nodes t - Suc 0 ⟹
         nodes (explode n (Node t t)) = 2 * 2 ^ n + 2 * 2 ^ n * nodes t - Suc 0

So, I thought that proving nodes(explode n (Node t t)) = 2*nodes(explode n t) + 1 would solve it. So I made a lemma for it, proved it and added the next two "simp"s.

But the proof failed, with:

goal (1 subgoal):
 1. ⋀n. nodes (explode n t) = 2 ^ n + nodes t * 2 ^ n - Suc 0 ⟹
         Suc (2 * 2 ^ n + nodes t * (2 * 2 ^ n) - Suc (Suc 0)) =
         2 * 2 ^ n + nodes t * (2 * 2 ^ n) - Suc 0

I don't quit

Your first goal is provable, but is somewhat non-trivial arithmetic. I believe that the issue is essentially Isabelle not knowing that
$$S(x - 2) = x -1$$
is true for arbitrary $x$, and indeed, this property is false in general, if $x<2$! This is because $x-2=0$ in Isabelle for $x=1$.

Here this doesn't occur, because $x=2\cdot 2^n$, so $x\geq 2$ for all $n\in\mathbb{N}$. But the simplifier doesn't know this. Adding a lemma along those lines, or making sure 2nodes(explode n t) + 1 doesn't get simplified to S(2nodes(explode n t)) should solve your issue.

Alternately, you could re-cast your whole proof in $\mathbb{Z}$, where subtraction behaves more sanely.

StackExchange Computer Science Q#43193, answer score: 3