This translation is not in there by default because it is bound to confuse novices and sometimes even experts: they see 1 in their proof state and 1 in their theorem and wonder why Isabelle refuses to apply the theorem. And eventually they realise that one of the two 1s is a Suc 0, whereas the other one is a genuine 1.
Of course, we avoid the above frustration at the cost of Suc 0. This issue comes up again and again, and we are not happy with the current state either. Thanks for your input. Tobias Chris Capel schrieb: > translations > "1" <= "Suc 0" > "2" <= "Suc (Suc 0)" > > Is there a reason why the above isn't defined by default? Is it a > matter of preference? Context? As a translation, the above doesn't > interfere with simplification machinery, so I don't think including it > by default would do any harm. Of course, not including it would be > fine too. But in the latter case perhaps the statement could be > mentioned in documentation instead of the current apology for the > strangeness of seeing "Suc 0" where one would expect "1". > > The 2 translation isn't as important. It seems like I occasionally see > "Suc (Suc 0)", but I don't think the simplifier will ever leave it. > > Chris Capel