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.

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.