伊莎贝尔证明加法的交换律

我试图证明 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)

应用 auto 后，我只剩下子目标 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)

让我们分别来看一下。

1. 使用的定义add我们只能简化左侧， IE。，add 0 m = m。那么问题就是如何证明add m 0 = m。 你这样做是作为主要证明的一部分。我认为它会增加 证明以下单独引理的可读性

   lemma add_0 [simp]:
     "add m 0 = m"
     by (induct m) simp_all
   

   并将其添加到自动化工具中（例如simp and auto) using [simp]。在此刻 第一个子目标可以通过以下方式解决simp只剩下第二个子目标了。

2. 应用定义后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)以便继续。