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