[isabelle-dev] Suc 0 necessary?

[Tobias Nipkow]

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