"state" 模式下的局部假设

Question

经常，在“证明”模式下证明一个陈述时，我发现自己需要一些尚未陈述或证明的中间陈述。为了说明它们，我通常使用 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 来陈述这些假设。然而，当涉及多个假设时，这很快就会变得相当乏味。有没有更简单的方法来简单地引用所有假设？或者，有没有一种好的方法可以直接在“证明”模式下实现带有简短证明的语句？

Answer 1

语法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)`

"state" 模式下的局部假设

Local assumptions in "state" mode

isabelle

isar