Q:

Why must Isabelle functions have at least one argument?

When I try to write
fun foo :: "nat ⇒ nat"  
where "foo = Suc"

Isabelle complains that "Function has no arguments". Why is this? What's wrong with a fun having no arguments? I know that I can change fun to abbreviation or definition and all is fine. But it seems a shame to spoil the uniformity of my .thy file, in which every other definition is declared with fun.

A:

Alex Krauss, the author of the present generation of fun and function in Isabelle/HOL had particular opinions about that, and probably also good formal reasons to say that a "function" really needs to have arguments.  In SML you actually have a similar situation: "constants" without arguments are defined via val not fun.
In the rare situations, where zero-argument functions are needed in Isabelle/HOL, it is sufficiently easy to use definition [simp] "c = t to get mostly the same result, apart from the name of the key theorems produced internally: c_def versus c.simps.
I think the main inconvenience and occasional pitfal of function in this respect is its exposure of the auxiliary c_def that is not meant to be used in applications: it unfolds the internal construction behind the function specification, not its main characterizing equation.

