[isabelle-dev] Suc 0 necessary?

[Brian Huffman]

Quoting Tobias Nipkow <nipkow at in.tum.de>:

> IIRC, 1 used to abbreviate Suc 0. Making "1 = Suc 0" a simp rule
> mimiced that.

Aha! The real reason comes out. Now things are starting to make sense...

> 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...

Yes, this is a real problem. There are even simp rules in the  
distribution that will never fire because they have "1::nat" 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.

This remains to be seen; I think the library theorems could probably  
remain agnostic about 1 vs. Suc 0. Theorems could come in both styles,  
and each theorem would ensure that the representation is preserved. I  
might have to try this out, and see how well it works. Actually, I  
suppose it wouldn't hurt to make sure the library theorems follow this  
policy, even with "1 = Suc 0" [simp] in place.

- Brian