[isabelle-dev] Suc 0 necessary?
nipkow at in.tum.de
Mon Feb 23 16:50:26 CET 2009
> Doesn't it make sense to leave it to users to decide which
> representation they want? Is there really any convincing reason why "1 =
> Suc 0" needs to be a simp rule?
IIRC, 1 used to abbreviate Suc 0. Making "1 = Suc 0" a simp rule mimiced
that. It allows you to write 1 on the rhs of an equation because (if
used as a simp rule) the 1 will be replaced by Suc 0. Of course this
does not work on the lhs...
Even if we did not make "1 = Suc 0" a simp rule, we would still need to
decide how to phrase the library theorems. This would still bias the user.
More information about the isabelle-dev