“状态”模式下的本地假设

问题描述

经常，在“证明”模式下证明一个陈述时，我发现自己需要一些尚未陈述或证明的中间陈述。为了说明它们，我通常使用 subgoal 命令，然后使用 proof- 更改为“状态”模式。然而，在这个过程中，所有的局部假设都被删除了。一个典型的例子可能是这样的

lemma "0 < n ⟷ ((2::nat)^n < 3^n)"
  apply(auto)
  subgoal
  proof-
    have "0<n" sorry (* here I would like to refer to the assumption from the subgoal *)
    then show ?thesis sorry
  qed
  subgoal sorry
  done

我知道我可以明确地使用 assume 陈述这些假设。但是，当涉及多个假设时，这会很快变得乏味。有没有更简单的方法来简单地引用所有假设？或者，有没有一种好方法可以直接在“证明”模式下实现带有简短证明的语句？

解决方法

有语法 subgoal premises prems 将子目标的前提绑定到名称 prems（或任何其他名称 - 但 prems 是合理的默认值）：

lemma "0 < n ⟷ ((2::nat)^n < 3^n)"
  apply(auto)
  subgoal premises prems
  proof -
    thm prems

还有一个名为 goal_cases 的方法可以自动为所有当前子目标命名——我觉得它非常有用。如果 subgoal premises 不存在，您可以改为这样做：

lemma "0 < n ⟷ ((2::nat)^n < 3^n)"
  apply(auto)
  subgoal
  proof goal_cases
    case 1

顺便说一下，看看你的例子，在 auto 之后做任何取决于证明状态的确切形式的事情被认为是一个坏主意，例如 metis 调用或 Isar 证明。 auto 是相当残酷的，在下一个 Isabelle 版本中可能会有不同的表现，因此此类证明会失效。我建议在这里做一个很好的结构化 Isar 证明。

另请注意，您的定理是 power_strict_mono 和 power_less_imp_less_base 的直接结果，可以在一行中证明：

lemma "0 < n ⟷ ((2::nat)^n < 3^n)"
  by (auto intro: Nat.gr0I power_strict_mono)`