Re: [isabelle] About contradiction method

You will find that the following "scheme" also works for Isar proofs:

{assume "~P"
  have False <proof>}
 then show ?thesis by metis/blast/simp

Lawrence Paulson wrote:
If you wish to prove a theorem by contradiction, the usual approach is to begin with the following line:

apply (rule ccontr)

Its effect should be self explanatory.

Larry Paulson

On 18 Jun 2008, at 14:05, Glauber Cabral wrote:

I've already read the Isabelle tutorial. This method is not explained there (as, you've told, it's not used often). And I've found only how to instantiate variables in a theorem, usin *rule_tac methods.

I wanted to use contradiction method because proof by contradiction was the only way I found to prove Assymetry of Strict total order using only Irreflexivity and Transitivity axioms.

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.