[isabelle-dev] blast

[Tobias Nipkow]

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