nipkow at in.tum.de
Wed Oct 10 13:03:14 CEST 2007
I have had problems with the conversion from ~ x = (0::nat) to x > 0 as
well. Can anyone recall why we installed that? I suspect it may have
helped a little before we had linear arithmetic but I now feel it is
more of a problem than a solution. Maybe I'm missing something.
Amine Chaieb wrote:
> I remarked the following (odd?) behaviour of blast and auto : Although
> they prove the general form:
> ~ P y ==> P x ==> ~ x = y
> they can't for the special instance:
> ~ P (0::nat) ==> P x ==> ~ x = 0
> I suspect this is due to an implicit classet rule such as
> ~ x = (0::nat) = x > 0.
> Is there a simple way to "correct" this behavious, if it might be
> considered erronous?
> Isabelle-dev mailing list
> Isabelle-dev at mailbroy.informatik.tu-muenchen.de
More information about the isabelle-dev