proof - 伊莎贝尔矛盾的惯用证明？

Question

到目前为止，我在 Isabelle 中以以下风格编写了矛盾证明（使用Jeremy Siek的模式）：

lemma "<expression>"
proof -
  {
    assume "¬ <expression>"
    then have False sorry
  }
  then show ?thesis by blast
qed

有没有嵌套原始证明块的方法{ ... }？

Answer 1

ccontr经典的反证法有以下规则：

have "<expression>"
proof (rule ccontr)
  assume "¬ <expression>"
  then show False sorry
qed

有时它可能有助于by contradiction证明最后一步。

还有一条规则classical（看起来不太直观）：

have "<expression>"
proof (rule classical)
  assume "¬ <expression>"
  then show "<expression>" sorry
qed

有关使用 的更多示例classical，请参阅$ISABELLE_HOME/src/HOL/Isar_Examples/Drinker.thy

Answer 2

为了更好地理解规则classical，它可以以结构化的 Isar 样式打印，如下所示：

print_statement classical

输出：

theorem classical:
  obtains "¬ thesis"

因此，直觉主义者的纯粹邪恶似乎更直观一些：为了证明一些武断的论点，我们可以假设它的否定成立。

相应的规范证明模式是这样的：

notepad
begin
  have A
  proof (rule classical)
    assume "¬ ?thesis"
    then show ?thesis sorry
  qed
end

这?thesis是上述主张的具体论点A，它可能是一个任意复杂的陈述。这种通过缩写的准抽象?thesis对于惯用的 Isar 来说是典型的，以强调推理的结构。