isabelle - 驯服 Isar 证明中的元含义

Question

在证明一个简单的定理时，我在证明中遇到了元级含义。拥有它们可以吗？或者可以避免它们吗？如果我应该处理它们，这是正确的方法吗？

theory Sandbox
imports Main
begin

lemma "(x::nat) > 0 ∨ x = 0"
proof (cases x)
  assume "x = 0"
  show "0 < x ∨ x = 0" by (auto)
next
  have "x = Suc n ⟹ 0 < x" by (simp only: Nat.zero_less_Suc)
  then have "x = Suc n ⟹ 0 < x ∨ x = 0" by (auto)
  then show "⋀nat. x = Suc nat ⟹ 0 < x ∨ x = 0" by (auto)
qed

end

我想这可以更容易地证明，但我想要一个结构化的证明。

Answer 1

原则上，元蕴涵 ==> 是无可避免的(事实上，它是 Isabelle 中表达推理规则的“原生”方式)。有一种规范的方法通常可以让我们在编写 Isar 证明时避免元含义。例如，为了总体目标

"!!x. A ==> B"

我们可以用 Isar 写

fix x
assume "A"
...
show "B"

对于您的具体示例，在 Isabelle/jEdit 中查看时您可能会注意到第二种情况的 n 被突出显示。原因是它是一个自由变量。虽然这本身不是问题，但在本地修复此类变量更为规范(就像教科书中的典型语句“对于任意但固定的......”)。例如，

next
  fix n
  assume "x = Suc n"
  then have "0 < x" by (simp only: Nat.zero_less_Suc)
  then show "0 < x ∨ x = 0" ..
qed

这里再次可以看出Isar中的fix/assume/show是如何对应实际目标的，即

1. ⋀nat. x = Suc nat ⟹ 0 < x ∨ x = 0