驯服 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/ assume/show在伊萨尔对应于实际的目标，即，

1. ?nat. x = Suc nat ? 0 < x ? x = 0