Re: [isabelle] About contradiction method

Dear Lawrence.

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.


On Wed, Jun 18, 2008 at 7:54 AM, Lawrence Paulson <lp15 at> wrote:

> You will find it much easier if you read the examples in the Tutorial
> rather than just trying out all the different methods. The contradiction
> method is not used very often.
> Larry Paulson
> On 17 Jun 2008, at 21:30, Glauber Cabral wrote:
>  I've been writing proofs only with apply (method) because Isabelle is not
>> the main focus right now and I thought it should be enough at this moment
>> to
>> write proofs this way.
>> The problem is that I could not find any example or explanation about how
>> to
>> use contradiction method. When I use it, I got 2 goals: P x y and not P x
>> y,
>> and I couldn't find how to make Isabelle relates P with a function I've
>> already created. Can anyone tell me where do I found any explanation or
>> example to understand how it works?

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