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 { ... }?

Zito

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

Zito

If <expression> is huge, it is convenient to start with assume "~ ?thesis". – Secession

An aside: ccontr (which AFAIK abbreviates "classical contradiction") is also classical reasoning. Thus it sounds a bit strange to call the second pattern classical reasoning. – Secession

@chris, you are right, I should change this reference to "classical reasoning". But then what would we the best word to describe the rule "classical"? – Zito

The rule "classical" expresses classical reasoning in its full brutality, without any auxiliary connectives. In the form "ccontr" it looks a bit more civilized, but it is equivalent. The names for these rules in Isabelle/FOL and HOL go back to Larry Paulson, as far as I can tell. – Hodges

Answer 2

For better understanding of rule classical it can be printed in structured Isar style like this:

print_statement classical

Output:

theorem classical:
  obtains "¬ thesis"

Thus the pure evil to intuitionists appears a bit more intuitive: in order to prove some arbitrary thesis, we may assume that its negation holds.

The corresponding canonical proof pattern is this:

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

Here ?thesis is the concrete thesis of the above claim of A, which may be an arbitrarily complex statement. This quasi abstraction via the abbreviation ?thesis is typical for idiomatic Isar, to emphasize the structure of reasoning.

Hodges