[isabelle-dev] blast

Amine Chaieb chaieb at in.tum.de
Wed Oct 10 11:20:24 CEST 2007

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?


More information about the isabelle-dev mailing list