Simp 不使用 Isabelle 中提供的引理

Question

我正在做 Concrete Semantics 书中的练习 2.6：

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).

我已经开始证明定理，不是使用自动而是指导伊莎贝尔使用必要的定理：

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)

这里它到达了证明状态

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)

我想知道为什么 simp 没有使用提供的 sum_list_contents 引理。我知道简单的 simp 可以求解方程。

通用 simp 包含哪些 simp only 在这种情况下不会使用的内容？

Answer 1

正如评论中所指出的，缺少的部分是自然数加法的结合性。添加 add.assoc 到简化规则求解方程。

或者，可以更改定义树和时操作数的顺序：

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))"

那么不需要结合律：

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 不使用 Isabelle 中提供的引理

Simp does not use the provided lemma in Isabelle

isabelle

theorem-proving

simplification