[isabelle] Printing natural numbers



I think this was discussed on the mailing list a few years ago, but I don't recall the exact details and I cannot seem to find the emails.

When using the âvalueâ command, natural numbers are printed in âSucâ notation. I for one find that very inconvenient. One way to get the system to print natural numbers as numerals is to include Code_Target_Numeral (this works for the [code], [nbe], and [simp] evaluators). It also makes evaluation much more efficient.

However, one does not always want to include Code_Target_Numeral whenever one experiments with âvalueâ. I just realised that the following [code_post] rules allow nice printing of natural numbers (although computation is still done Peano-style behind the curtain):


lemma eval_Suc_nat [code_post]:
  "Suc 0 = 1"
  "Suc 1 = 2"
  "Suc (numeral n) = numeral (Num.inc n)"
  unfolding One_nat_def numeral_inc by simp_all

declare Num.inc.simps [code_post]


However, for some reason, this does not seem to work for the [simp] and [nbe] evaluators.


Does anyone apart from me think that something like this should be done? Is there a way that also works for [simp] and [nbe]?


Cheers,

Manuel




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.