[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
Does anyone apart from me think that something like this should be done?
Is there a way that also works for [simp] and [nbe]?
This archive was generated by a fusion of
Pipermail (Mailman edition) and