The fun command can be used to define functions in Isabelle. Unlike definitions, functions can be defined by multiple pattern-matching equations, they may be recursive, and their equations are automatically added to the simpset.
The print_theorems command allows us to see all of the lemmas generated by this command.
In cases where the recursion and pattern matching follows exactly the structure of the datatype in one argument, primrec can be used instead of fun, which is a bit more efficient: