Idiomatic Proof by Contradiction in Isabelle?

Question

So far I wrote proofs by contradiction in the following style in Isabelle (using a pattern by Jeremy Siek):

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

Is there a way that works without the nested raw proof block { ... }?

Answer 1

There is the rule ccontr for classical proofs by contradiction:

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

It may sometimes help to use by contradiction to prove the last step.

There is also the rule classical (which looks less intuitive):

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

For further examples using classical, see $ISABELLE_HOME/src/HOL/Isar_Examples/Drinker.thy