Definition mechanism for tail-recursive functions

[myreen]

The new automation has two parts: the first part proves that a tail-recursive function exists; the second part uses new_specification to define such a function.

The given equations must have only curried variable arguments left of the equality, e.g.

foo m n = ...

is allowed, but the following is not:

foo (m, n) = ...

This commit also renames:

examples/machine-code/hoare-triple/tailrecLib.{sml,sig}
->
examples/machine-code/hoare-triple/mc_tailrecLib.{sml,sig}

Here's an example use of the new definition mechanism:

val _ = List.map Parse.hide ["foo","bar"];

val foo_def = tailrec_define "foo_def"
  “(foo m n = if m = (n:num) then bar m (SOME 8) else bar 4 NONE) ∧
   (bar k l = case l of
              | NONE => k - 6
              | SOME i =>
                  let (q,r) = ARB i
                  and (t,w,a) = ARB k l in
                    foo (q + r) (t + w + a))”;

[mn200]

Thanks for this!