Re: [isabelle] About contradiction method
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.
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
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