Isabelle：前身函数

Question

我不确定，但我认为有时如果我有一个前置函数，我的证明会更容易，例如，如果已知变量不为零。

我不知道一个很好的例子，但也许在这里：{ fix n have "(n::nat) > 0 ⟹ (∑i<n. f i) = Predecessor n" sorry }

可能因为不是个好主意，所以库中没有前置函数。

有没有办法模拟前驱功能或类似功能？

我想到了这个例子：

theorem dummy:
shows "1=1" (* dummy *)
proof-

  (* Predecessor function *)
  def pred == "λnum::nat. (∑i∈{ i . Suc i = num}. i)"

  {fix n :: nat
  from pred_def have "n>0 ⟹ Suc (pred n) = n" 
  apply(induct n)
  by simp_all
  }
  show ?thesis sorry
qed

Answer 1

您的定义过于复杂。为什么不直接写

def pred ≡ "λn::nat. n - 1"

那么你可以拥有

have [simp]: "⋀n. n > 0 ⟹ Suc (pred n) = n" by (simp add: pred_def)

在0 的情况下，pred 函数然后简单地返回0 和Suc (pred 0) = 0 显然不成立。你也可以定义pred ≡ "λn. THE n'. Suc n' = n"。如果存在这样的数字（即如果存在n > 0）和undefined（即您一无所知的某个自然数），那将返回其后继为n 的唯一自然数。但是，我认为在这种情况下，只做pred ≡ λn::nat. n - 1 会更容易和更明智。

我怀疑在大多数情况下，您可以简单地放弃pred 函数并编写n - 1；但是，我确实知道有时将- 1 定义为“受保护”是件好事。在这些情况下，我通常将def 一个变量n' 作为n - 1 并证明Suc n' = n——基本上是一样的。在我看来，既然证明这一点只需要一行，它并不真正值得自己定义，比如这个 pred 函数，但我想可以为它提出一个合理的理由。

另一件事：我注意到您使用 lemma "1 = 1" 作为某种虚拟环境来进行 Isar 证明。我想指出 notepad 的存在，它恰好针对该用例而存在，并且可以用法如下：

notepad
begin
  have "some fact" by something
end