如何让伊莎贝尔使用基本的数学规则？

Question

我正在努力学习伊莎贝尔：

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

然而，定理未解：

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

如果我没记错的话，Isabelle 只是没有应用 x + x = 2*x 和 a + (b + c) = a + b + c。所以我尝试添加一个引理以将其与 simp 一起使用：

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

但这失败了

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

Type error in application: incompatible operand type

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

我假设不可能在引理中定义变量的类型？

现在我当然可以重新定义加法 - 但我想这并不是真正的最佳实践。解决最初问题的最佳方法是什么？

Answer 1

algebra_simps 是常用数学规则的列表。添加它解决了问题：

apply(auto simp add: numeral_eq_Suc algebra_simps)

Answer 2

找到正确引理的一些通用方法：

通过查询面板或在带有 find_theorems:

的文本中使用定理搜索

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

使用大锤。
试试 waldelb 建议的 algebra_simps 集合（还有 ac_simps、algebra_split_simps、field_simps 和 field_split_simps ).

试着把它分成更小的步骤。这有助于 simp 工具，因为简化可以在等式的两边起作用，并且因为您可以将其引导到正确的中间步骤。下面的例子有点过于极端，每一步只重写一次。一般来说，您可以在自动失败的地方添加中间步骤。

 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

如何让伊莎贝尔使用基本的数学规则？

How to make Isabelle use basic math rules?

isabelle