Re: [isabelle] About contradiction method
You will find that the following "scheme" also works for Isar proofs:
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.
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