时间戳

首页 > 解决方案 > Isabelle 不评估引理

isabelle - Isabelle 不评估引理

问题描述

我正在阅读介绍“ Isabelle/HOL 中的编程和 Provin ”并尝试做练习 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都是蓝色而不是标准红色。

伊莎贝尔编辑

我没有收到任何错误消息。当我将它悬停在输出控制台中时都不会。

我究竟做错了什么？

标签： isabelle

解决方案

红色背景表示当前正在处理该行。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，并且证明将成功。

推荐阅读