Replace a ho_match_mp_tac with an Induct_on

Removes a dependency on how IndDefLib names its generated theorems.

Define a recursivefns$rec1 equivalent of primrec's pr1

This allows for relatively straightforward lifting of standard unary
functions (i.e., of type :num -> num option) into the "space" of
recursive functions, which take lists of arguments and return option
values.

Needs some results about the fact that recursive functions
automatically/implicitly pad (with zeroes) or truncate their argument
lists to make them match the desired arity.

Tweak thms on link between λ-calc and rec. fns

Make the class of recursive functions necessarily of arity > 0.

This eliminates the possibility of being able to define a 0-ary
'function' (i.e., really a constant) as μx. f(x) ("the least x such
that f(x) returns 0").

Adopt ML-style syntax for case expressions and use freed up "||" for bitwise-or. See issue #24.

Super minimalist theory of recursive functions (= primrec + minimisation).