伊莎贝尔证明加法的可交换性

埃里达尼斯

我试图证明Isabelle / HOL中的自定义add函数可交换性。我设法证明了关联性，但我坚持这一点。

的定义add：

fun add :: "nat ⇒ nat ⇒ nat" where
"add 0 n = n" |
"add (Suc m) n = Suc(add m n)"

关联性证明：

lemma add_Associative: "add(add k m) z = add k (add m z)"
apply(induction k)
apply(auto)
done

可交换性的证明：

theorem add_commutativity: "add k m = add m k"
apply(induction k)
apply(induction m)
apply(auto)

我实现了以下目标：

goal (3 subgoals):
1. add 0 0 = add 0 0
2. ⋀m. add 0 m = add m 0 ⟹
     add 0 (Suc m) = add (Suc m) 0
3. ⋀k. add k m = add m k ⟹
     add (Suc k) m = add m (Suc k)

应用自动后，我剩下的只是子目标3：

3. ⋀k. add k m = add m k ⟹
     add (Suc k) m = add m (Suc k)

编辑：我不是在寻找答案，而是朝着正确的方向推进。这些是一本名为《混凝土水泥学》的书中的练习。

克里斯

我建议将证明尽可能地模块化（即证明中间引理，以后将有助于解决可交换性证明）。为此induct，在应用全自动（例如apply (auto)）之前，对由引入的子目标进行冥想通常会更有意义。

lemma add_comm:
  "add k m = add m k"
  apply (induct k)

此时，子目标为：

 goal (2 subgoals):
  1. add 0 m = add m 0
  2. ⋀k. add k m = add m k ⟹ add (Suc k) m = add m (Suc k)

让我们分别看看它们。

使用的定义，add我们将只能简化左侧，即add 0 m = m。然后问题仍然是如何证明add m 0 = m。您这样做是作为主要证明的一部分。我认为这可以提高可读性，以证明以下单独的引理
```
lemma add_0 [simp]:
  "add m 0 = m"
  by (induct m) simp_all
```
并使用将其添加到自动化工具（如simp和auto）中[simp]。此时，可以解决第一个子目标，simp而仅保留第二个子目标。
应用的定义和add归纳假设（add k m = add m k）后，我们将必须证明Suc (add m k) = add m (Suc k)。这看起来与的原始定义的第二个方程式非常相似add，仅带有交换参数。（从这个角度来看，我们必须为第一个子目标证明的内容add与带有互换参数的定义中的第一个方程式相对应。）现在，我建议尝试证明一般引理add m (Suc n) = Suc (add m n)以便继续进行。