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.
Tobias Amine Chaieb wrote: > Hi, > 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? > > Cheers, > Amine. > _______________________________________________ > Isabelle-dev mailing list > Isabelle-dev at mailbroy.informatik.tu-muenchen.de > https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
