[isabelle-dev] real, of_nat and Suc

[Larry Paulson]

As has been discussed previously, our setup of injections among numeric types is chaotic. In particular, we have the function of_nat, which maps 0 and Suc to their equivalents on types that are supersets of the natural numbers. We have another function called real, which is overloaded from a variety of different types and always yields a real; not all of these instances are even injections.

As a first step towards reconciling these, I looked into the problem that of_nat and real were not even simplified in the same way: of_nat (Suc n) was simplified by default whereas real (Suc n) was not. Under the impression that the latter behaviour was canonical, I tried removing the simprule status of of_nat_Suc. This turned out quite badly, and in particular, The function int (which seems to be analogous to real, but in fact is nothing but an abbreviation for of_nat) was then being simplified differently from before, and it’s quite difficult to justify why int (Suc n) should not be simplified in the obvious way.

So instead, real_of_nat_Suc is going to become a simprule. The only proofs where this caused a problem involved goals or even definitions that have been unwisely stated involving real (Suc n), rather than the obvious “real n + 1”.

Over the next week or two, I hope to get the chance to redefine real as an abbreviation for of_nat with the correct type, thereby putting it on exactly the same status as int.

Larry