[isabelle-dev] Suc 0 necessary?

[Brian Huffman]

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