Re: [isabelle] Proving a simple lemma
Am 09.06.2010 um 12:29 schrieb dayzman at gmail.com:
> 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