Isabelle不对引理求值
Isabelle不对引理求值
提问于 2020-07-06 20:05:12
我正在阅读"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都是蓝色，而不是标准的红色。
我没有收到任何错误消息。无论是在我悬停它的时候，还是在输出控制台中。
我做错了什么？
回答 1
Stack Overflow用户
回答已采纳
发布于 2020-07-06 23:09:20
红色背景表示该行当前正在处理中。由于add1引理，看起来简化程序陷入了一个无尽的循环。如果您使用apply (subst add1)手动重复应用引理，则可以看到这一点
步骤1. 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，证明将会成功。
页面原文内容由Stack Overflow提供。腾讯云小微IT领域专用引擎提供翻译支持
原文链接：
https://stackoverflow.com/questions/62755713
复制相关文章
相似问题
腾讯云开发者
