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

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

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

Answer 2