1

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

4

1 回答 1

2

有一种语法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)`
于 2021-01-06T19:15:45.287 回答