伊莎贝尔不评估引理

Question

我正在阅读介绍“Programming and Provin in Isabelle/HOL”并尝试做练习 2.2。

目前我有：

theory Scratch
  imports Main
begin

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

lemma add_02 [simp]: "add m 0 = m"
  apply(induction m)
  apply(auto)
  done

lemma succ [simp]: "Suc (add m n) = add m (Suc n)"
  apply(induction m)
  apply(auto)
  done

lemma commutativity [simp]: "add n m = add m n"
  apply(induction n)
  apply(auto)
  done

lemma add1 [simp]: "Suc m = add m (Suc 0)"
  apply(induction m)
  apply(auto)
  done
  
lemma add1_commutativ [simp]: "add n (Suc m) = add m (Suc n) "
  apply(induction n)
  apply(auto)
  done

lemma associativity [simp]: "add n (add m t) = add (add n m) t"
  apply(induction n)
  apply(auto)
  done

end

在引理 add1_commutativ 中，apply(auto) 的背景颜色为红色，随后的关键字 apply 和 done 都是蓝色而不是标准的红色。

我没有收到任何错误消息。无论是在悬停时还是在输出控制台中。

我做错了什么？

Answer 1

红色背景表示该行当前正在处理中。由于 add1 引理，简化器运行看起来像是陷入了无限循环。如果您使用 apply (subst add1):

手动重复应用引理，您会看到这一点

第一步。add 0 (Suc m) = add m (Suc 0)

第 2 步。add 0 (add m (Suc 0)) = add m (Suc 0)

第 3 步。add 0 (add m (add 0 (Suc 0))) = add m (Suc 0)

...

如您所见，每一步都变大，这个过程永远不会终止。

一般来说，您应该尝试编写方程式，使右侧小于左侧，因为简化器将使用方程式从左到右重写项。

因此对于您的示例，您可以将引理 add1 更改为 add m (Suc 0) = Suc m 并且证明将成功。

伊莎贝尔不评估引理

Isabelle does not evaluate lemma

isabelle