Isabelle中矛盾的惯用语证明？

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