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.