Provide λ-calculus versions of unfold and fold functions

These functions are currently in unary_recfnsTheory but will probably
soon move to nlistTheory.

Also clean some other things up, including removing an unnecessary
dependency between churchDB and churchlist.

Remove unnecessary structure bracketting

As per 89fc99bc3, but on as many examples as a grep -R can find.

Extract a usable half-way point from nominal_datatype branch.

This replaces the is_perm predicate with a type embodying that predicate.
It doesn't include the subsequent work on allowing multiple 'atom' types.

Terms and labelled terms now derived from generic terms.

This is a big change that points to the implementation of a complete
nominal datatype package. The use of generic terms means that we only
need to do one hairy quotient, and one hairy derivation of a recursion
principle.

The recursion principle in question features a new "FCB" (one of the
side-conditions that need to be proved in order to get a recursive
function admitted). Though I think it's better, it can be a little
fiddlier to prove. It's also stronger, so in theory, there may be
reasonable functions that the new FCB rejects. It should certainly be
possible to automate the bulk of the new fiddly proofs.

Rework lambda-theory scripts to use new varying parameter recursion theorem.

Also make work for myself by having some of the script files use
'tight' equality. Later files get switched back to loose (prec = 100)
equality, because it was all getting to be too much work.

Fix barendregt/chap2Script.sml so that set_MLname is no longer required.

Also fix annoying choice of names while I'm at it.

Move some theorems around; mainly to put cfindleast into churchnumTheory.

Checking in to save my work (progress with findleast).
Unfortunately recsets doesn't quite build - will fix tomorrow.

Progress with findleast combinator.

Forgot to commit simple theorems about Yf in examples/lambda/barendregt.

Recast the definition of the Y combinator to be the "traditional"
\f. (\x. f (x x)) (\x. f (x x))
rather than the combinator version I had before. Reprove the important
characterising theorem. The reason for the switch is to make it
easier to reason about normal order reductions involving Y.

Use new facilities (bounded pre-order rewrites and |>) to simplify a
proof about the Y combinator.

Use the new add_relsimp facilities in simpLib to implement the system
provided by reductionEval, and to simplify the proofs in chap2Script.
While I'm at it, add definitions and characterising theorems about
combinators B, C, and Y in chap2Theory.

Show that the numeric pairing functions are computable by providing
lambda-terms to do them.

Changes so that the weakened rewriting of lambda-terms now happens
with respect to beta-equality (==), rather than beta-reduction
(-b->*). This gives us access to more rewrites. In particular, we
get things like
church (SUC n) @@ z @@ f == f @@ (church n @@ z @@ f)
which is a nice recursive characterisation of what church numerals do,
and saves us from having to do too many ghastly things with FUNPOW.
With the above equation, neither side reduces to the other (they have
a common reduct of course), and so it wasn't a usable rewrite when
using -b->*.

In addition, to the above, I set up a natrec combinator, which would
get typed
: 'a -> (num -> 'a -> 'a) -> num -> 'a
if we were in a typed world. This combinator gets access to the value
of the recursive argument, making predecessor easier to define.

Also, give an equation like the one above for church for the cDB
function.

Many proofs are shorter. Some are slower, but the shortness of
expression won me over.

Add some rewrites about freshness (not being in the free variables of
a term) that work better with the simplifier. This breaks a couple of
proofs later on in chap2 and chap3 theories, that are easily fixed.

More useful facts about Omega, including the fact that if you can
reach it, you have no beta-normal-form.

More facts about normal order reduction paths, including the fact that
the self-looping Omega term has an infinite one, and thus, by another
theorem just proved, has no beta-normal-form.

Change export_rewrites back to its old API (without requiring an extra
string). When exported, the resulting simpset fragment always picked
up the name of the theory to be the base of its name, so there didn't
seem much point in giving users a false impression of naming power.

More laggards.

A whole mess of small changes intended
at making simpsets prettyprint informatively
in the interactive loop. Very possibly
I haven't updated all the files in the examples
directories.

Completely reorganise these files into some sensible directories.
Also, add a file demonstrating that the McKinna-Pollack two-sorted raw
syntax does indeed behave properly (links appropriately to beta over
quotiented terms).