Simp does not use the provided lemma in Isabelle

Question

I am doing Exercise 2.6 from the Concrete Semantics book:

Starting from the type 'a tree defined in the text, define a function contents :: 'a tree ⇒ 'a list that collects all values in a tree in a list, in any order, without removing duplicates. Then define a function sum_tree :: nat tree ⇒ nat that sums up all values in a tree of natural numbers and prove sum_tree t = sum_list (contents t) (where sum_list is predefined).

I have started to prove the theorem not using auto but guiding Isabelle to use the necessary theorems:

theory Minimal

imports Main

begin

datatype 'a tree = Tip | Node "'a tree" 'a "'a tree"

fun contents :: "'a tree ⇒ 'a list" where
  "contents Tip = []"
| "contents (Node l a r) = a # (contents l) @ (contents r)"

fun sum_tree :: "nat tree ⇒ nat" where
  "sum_tree Tip = 0"
| "sum_tree (Node l a r) = a + (sum_tree l) + (sum_tree r)"

lemma sum_list_contents: 
  "sum_list (contents t1) + sum_list (contents t2) = sum_list (contents t1 @ contents t2)"
  apply auto
  done

lemma sum_commutes: "sum_tree(t) = sum_list(contents(t))"
  apply (induction t)
   apply (simp only: sum_tree.simps contents.simps sum_list.Nil)
   apply (simp only: sum_list.Cons contents.simps sum_tree.simps  sum_list_contents)

Here it arrives to a proof state

proof (prove)
goal (1 subgoal):
 1. ⋀t1 x2 t2.
   sum_tree t1 = sum_list (contents t1) ⟹
   sum_tree t2 = sum_list (contents t2) ⟹
   x2 + sum_list (contents t1) + sum_list (contents t2) = x2 + sum_list (contents t1 @ contents t2)

Where I wonder why simp did not use the provided sum_list_contents lemma. I know simple simp would solve the equation.

What does general simp contain that simp only would not use in this case?

It’s probably to do with + being left-associative, so you actually have (x2 + sum_list (contents t1)) + sum_list (contents t2) and now your lemma LHS doesn’t match any more. I’ll wait for the experts to tell you about the “right” way to fix that, though. — Joachim Breitner

Alexander Kogtenkov Alexander Kogtenkov · Accepted Answer · 2020-01-21T12:54:31

As pointed out in the comments, the missing piece is associativity of addition for natural numbers. Adding add.assoc to the simpplification rules solves the equation.

Alternatively, the order of operands when defining the tree sum could be changed:

fun sum_tree_1 :: "nat tree ⇒ nat" where
  "sum_tree_1 Tip = 0"
| "sum_tree_1 (Node l a r) = a + ((sum_tree_1 l) + (sum_tree_1 r))"

Then the associativity is not required:

lemma sum_commutes_1: "sum_tree_1(t) = sum_list(contents(t))"
  apply (induction t)
   apply (simp only: sum_tree_1.simps contents.simps sum_list.Nil)
  apply (simp only: sum_list.Cons contents.simps sum_tree_1.simps sum_list_contents)
  done

Simp does not use the provided lemma in Isabelle

1 Answers