How to make Isabelle use basic math rules?

I'm trying to learn Isabelle:

theory test
imports Main
begin

datatype tree = Leaf | Node tree tree

fun nodes :: "tree ⇒ nat" where
"nodes Leaf = 1"|
"nodes (Node x y) = 1 + (nodes x) + (nodes y)"

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

theorem tree_count: "nodes (explode h l) = 2^h + 2^h * (nodes l) - 1"
  apply(induction h arbitrary: l)
   apply(auto simp add: numeral_eq_Suc)
  done

end

However, the theorem is not solved:

Failed to finish proof:
goal (1 subgoal):
 1. ⋀h l. (⋀l. nodes (explode h l) = Suc (Suc 0) ^ h + Suc (Suc 0) ^ h * nodes l - Suc 0) ⟹
           Suc (Suc 0) ^ h + (Suc (Suc 0) ^ h + Suc (Suc 0) ^ h * (nodes l + nodes l)) - Suc 0 =
           Suc (Suc 0) ^ h + Suc (Suc 0) ^ h + (Suc (Suc 0) ^ h + Suc (Suc 0) ^ h) * nodes l - Suc 0

If I'm not mistaken, Isabelle is just not applying x + x = 2*x and a + (b + c) = a + b + c. So I tried adding a lemma to use it with simp:

lemma a: "(x:nat) + x = 2*x"

But this fails with

Type unification failed: Clash of types "_ ⇒ _" and "_ set"

Type error in application: incompatible operand type

Operator:  (∈) x :: ??'a set ⇒ bool
Operand:   nat :: int ⇒ nat

I assume that it's just not possible to define the type of a variable in a lemma?

Now I could of course redifine the addition - but I guess that's not really best practice. What would be the best way to solve the initial problem?

Solution

Some general approaches to find the right lemmas:

Use the theorem search, either via the query panel or in the text with find_theorems:

find_theorems ‹_ * (_ + _)›
find_theorems name: assoc "_ + _ + _"
find_theorems ‹2 * ?z = ?z + ?z›

Use sledgehammer.
Try the algebra_simps collection as suggested by waldelb (There are also ac_simps, algebra_split_simps, field_simps, and field_split_simps ).

Try to split it up into smaller steps. This helps the simp tool, because simplification can work on both sides of the equation and because you can guide it to the right intermediate steps. The example below is a bit too extreme, doing only one rewrite per step. In general, you can just add intermediary steps where the automatic ones fail.

 theorem tree_count: ‹nodes (explode h l) = 2^h + 2^h * (nodes l) - 1›
 proof (induction h arbitrary: l)
   case 0
   show ‹nodes (explode 0 l) = 2 ^ 0 + 2 ^ 0 * nodes l - 1›
     by simp
 next
   case (Suc h)

   have ‹nodes (explode (Suc h) l)
      = nodes (explode h (Node l l))›
     by (subst explode.simps, rule refl)
   also have "... = 2 ^ h + 2 ^ h * nodes (Node l l) - 1"
     by (subst Suc, rule refl)
   also have "... = 2 ^ h + 2 ^ h * (1 + nodes l + nodes l) - 1"
     by (subst nodes.simps, rule refl)
   also have "... = 2 ^ h + 2 ^ h * (1 + (nodes l + nodes l)) - 1"
     by (subst add.assoc, rule refl)
   also have "... = 2 ^ h + 2 ^ h * (1 + (2 * nodes l)) - 1"
     by (subst mult_2, rule refl)
   also have "... = 2 ^ h + (2 ^ h * 1 + 2 ^ h * (2 * nodes l)) - 1"
     by (subst distrib_left, rule refl)
   also have "... = 2 ^ h + (2 ^ h * 1 + 2 ^ h * 2 * nodes l) - 1"
     by (subst mult.assoc, rule refl)
   also have "... = 2 ^ h + (2 ^ h * 1 + 2 ^ Suc h * nodes l) - 1"
     by (subst power_Suc2, rule refl)
   also have "... = (2 ^ h + 2 ^ h * 1) + 2 ^ Suc h * nodes l - 1"
     by (subst add.assoc, rule refl)
   also have "... = (2 ^ h + 2 ^ h) + 2 ^ Suc h * nodes l - 1"
     by (subst mult_1_right, rule refl)
   also have "... = 2 ^ h * 2 + 2 ^ Suc h * nodes l - 1"
     by (subst mult_2_right, rule refl)
   also have "... = 2 ^ Suc h + 2 ^ Suc h * nodes l - 1"
     by (subst power_Suc2, rule refl)
   finally show ?case .
 qed