Re: [isabelle] Proving a simple lemma


Am Mittwoch, den 09.06.2010, 10:29 +0000 schrieb dayzman at
> I'm trying to prove a simple lemma, but am stuck at the last proof step:
> lemma test_wrong:
> fixes f :: "real => real"
> shows "(EX x y. fx ~= fy) --> ~(EX x y. fx > fy)"
> apply (rule impI)
> apply (rule notE)
> apply auto
> goal (1 subgoal):
> 1. !!(x::real) y::real. fx ~= fy --> False
> I think I'm supposed to let x be y, but how do I do that in Isar? Also, is  
> what I've done so far reasonable?

this might be a copy’n’paste problem, but did you really write "fx"
instead of "f x"? Then "fx" becomes a variable, independent of your
function f and the parameters x and y, and the lemma would be unprovable
(e.g. with fx = 0 and fy = 1).


Joachim "nomeata" Breitner
  mail: mail at | ICQ# 74513189 | GPG-Key: 4743206C
  JID: nomeata at |
  Debian Developer: nomeata at

Attachment: signature.asc
Description: This is a digitally signed message part

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