[isabelle-dev] Suc 0 necessary?
brianh at cs.pdx.edu
Mon Feb 23 17:33:25 CET 2009
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
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.
More information about the isabelle-dev