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

を使用したその他の例については、 $ISABELLE_HOME/src/HOL/Isar_Examples/Drinker.thyclassicalを参照してください。

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 の典型です。