Idiomatic proof of contradiction in Isabel?

Question

So far, I have written evidence of controversy in the following style in Isabelle (using the template of Jeremy Siek ):

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

Is there a way that works without a block of nested raw evidence { ... } ?

Answer 1

For classic evidence, the ccontr rule ccontr :

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

This can sometimes help to use by contradiction to confirm the last step.

There is also a classical rule (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

Answer 2

For a better understanding of the classical rule, you can print it in a structured Isar style as follows:

 print_statement classical 

Output:

 theorem classical: obtains "¬ thesis" 

Thus, pure evil to intuitionists seems a little more intuitive: in order to prove some arbitrary thesis, we can assume that its denial takes place.

The corresponding canonical proof template is as follows:

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

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