Re: [isabelle] Proving a simple lemma

Hi Michael,

Am 09.06.2010 um 12:29 schrieb dayzman at

> fixes f :: "real => real"
> shows "(EX x y. fx ~= fy) --> ~(EX x y. fx > fy)"
> apply (rule impI)
> apply (rule notE)
> apply auto

The conjecture is not valid. Indeed, Nitpick (which you can invoke by typing "nitpick" after the statement of the lemma or at any point in the proof) gives a counterexample.

One problem seems to be that you should put a space between "f" and "x" (or "y"). The second problem is that there shouldn't be any negation in the right-hand side of "-->".



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