1

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

我不知道一个很好的例子，但也许在这里：{ 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
4

1 回答 1

2

你的定义是不必要的复杂。为什么你不只是写

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如果这样的数字存在（即 if n > 0）和undefined（即一些你一无所知的自然数）否则。但是，我认为在这种情况下，只做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
于 2013-12-01T23:43:33.717 回答