isabelle - 在 Isabelle 中使用“induct”证明时如何使用基本情况假设

Question

假设我正在证明一个假设“ n ≥ m”（都是自然数）的定理，并且我对n. 在基本情况下，假设是“ n = 0”。有了这两个，我们可以得出结论，在基本情况下，“ m = 0”。

但是，我在使用语句“ n = 0”时遇到了麻烦：

lemma foo:
  assumes "(n::nat) ≥ (m::nat)"
  shows ...
proof (induct n)
  case 0
  have "m = 0" using <I don't know what to put here> assms by simp
  ...
qed

我试过using "n = 0"了，但它似乎是一个“ Undefined fact”。我也尝试将其添加为假设，但无济于事。尽管如此，很明显，在分析基本情况时，这是一个隐含的假设。

那么，如何在我的证明中直接使用基本情况的假设呢？

Answer 1

当您调用induct. 特别是，这应该是包含您进行归纳的所有假设（即包含n在您的案例中的所有假设）。

因此，您应该using assms在proof. 然后0 ≥ m将在基本情况下以名称提供给您"0.prems"（或仅0适用于所有这些加上归纳假设，在这种情况下不存在）。