CODEWITHSUNDEEP
proofisabelleisar
Christoph Lange
Christoph Lange

Reputation: 615

Idiomatic Proof by Contradiction in Isabelle?

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

Upvotes: 10

Views: 2343

Answers (2)

Christoph Lange
Christoph Lange

Reputation: 615

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

Upvotes: 10

Makarius
Makarius

Reputation: 2204

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.

Upvotes: 5

Related Questions