Quoting Tobias Nipkow <nipkow at in.tum.de>: > This is exactly the point: recursive functions defined by pattern > matching expect Suc. They tend to dominate the scene in CS-oriented > applications. Hence Suc 0 is made the default. However, for math > applications this tends to be inconvenient, esp in connection with > abstract algebra involving 1.
But this is exactly my point: CS-oriented users, who define a lot of recursive functions by pattern matching on Suc, can use Suc 0. Math-oriented users can use 1. Users can choose which style they want to use. To support this separation of Suc 0 and 1, Nat.thy would probably need to have two versions of some lemmas, one in each style; but this should not be difficult. The real problem that I can see is that a lot of CS-oriented users have gotten used to writing "1" as shorthand for "Suc 0". Currently they can get away with it, because it is expanded by the simplifier. > The original posting by Chris Capel merely aimed at readability: "Suc > 0" is less pleasant than "1". An alternative we discussed but never > agreed on is to abbreviate "Suc 0" to "#1". This would merely be new > surface syntax and not help with the algebraic 1, but it may already > satisfy some people. I think abbreviations like this could really help. Being able to write "#1" for "Suc 0" means that users won't have to write "1" for "Suc 0" solely for the sake of brevity. - Brian
