Fix some more examples for #346

Fix λ-calculus examples in light of pat_assum rename

Avoid infix clash at precedence 750.

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.

Fixed standardisation script (all of barendregt directory builds).

Issue here was that new theorems pick slightly different variable
names in some places, and this causes breakage.

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.

Prove some useful theorems about having weak-head normal forms.

Proof fixes given general incorporation of LIST_EQ_SIMP_ss.

New, powerful, automatic rewrite in optionScript.

Rewrite is

|- ((if P then SOME x else NONE) = SOME z) = P /\ (x = z)

and all variants there-on.

A number of changes were necessary in other theories. This change
affects not just srw_ss() but also std_ss.

In finite_map, I created a couple of new Unicode variants for SUBMAP
and FUNION. I also tidied up some proofs, and the statement of some
goals (indentation, column limits).

Tidy up some proofs by using Once and the new Simp* modifiers to the
simplifier (replacing things like CONV_TAC (LAND_CONV (ONCE_REWRITE_CONV ...)))

Fiddle and prettify basic presentation of beta-reduction. Using
syntactic patterns, I can now have ``compat_closure beta M N`` (the
"compatible closure of the beta-relation) appear as ``M -b-> N``.
Also use syntactic patterns to get rid of constants reduction and
conversion. Finally, provide Unicode versions of the various arrow
symbols so that with the Unicode flag on, the above will come out as
M -β-> N
Even in just ASCII, I think the theorems look a deal prettier.

More changes to the lambda-calculus theories about reduction,
including a new theorem giving a coinduction principle for the notion
of being a standard reduction. Also prove that every normal-order
reduction is standard, and that every head reduction is a normal-order
reduction.

Also change the okpath_co_ind theorem in pathTheory so that it doesn't
force the user to consider a useless case. This has some knock-on
effects in the barendregt directory.

Eliminate the head_reduce1 constant from standardisation and replace
it everywhere with head_reduction$hreduce1, written infix -h->. Also,
prove a couple of easy lemmas in head_reduction:
- that hreduce1 is deterministic/unique
- that if M beta-reduces to N, and M is hnf, then so too is N (i.e.,
the reduction happened at an "internal" redex).

Start to move stuff relating to head-reduction into a separate
theory. There's still a pile of stuff, mainly expressed in terms of
reduction paths, in standardisationTheory that could probably be moved
or re-expressed. In particular, there is a head_reduce1 constant
there that is actually the same as -h-> from head_reductionTheory.

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.

As per the comment in the file, I have to begin
standardisationScript.sml with the line
structure standardisationScript = struct
in order to have MoscowML compile it successfully.

Fix for the lambda-calculus examples in light of RTC_REFL being exported
from relationTheory.

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).