Fix examples/lambda/barendregt for tight equality

Fix some bare case constant applications in examples/lambda.

This is progress with github issue #97.

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

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.

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

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

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

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

Prove that K is not recursive.

Demonstrate the easy closure properties for recursive sets (empty,
UNIV, and finite sets are recursive; they are closed under union,
complement and intersection).

Make much use of the fact that it is legitimate to rewrite with
beta-reduction under the bnf_of function:

M == N ==> (bnf_of M = bnf_of N)

Adding this to my weakening congruences did break the proof of one of
my Halting Problem theorems, but a little abbreviation hackery solved
that.

Prove another easy consequence of the general result about the degree to which
weak-head evaluation mimicks normal order evaluation: that if M -n->* v, with
v a variable, then M -w->* v too.

Some additional rewrites of "general utility".

Prove some theorems about normal order reduction to weak-head normal
forms (abstractions, or variables in the head position of a series of
applications). Basically, if something can normal reduce to such a
thing, then it can weak-head reduce to something that shares the key
aspects of the shape. Either, it can weak-head reduce to an
abstraction, or it can weak-head reduce to a series of applications,
where the head is the variable that is in that position at the end of
the normal order reduction.

Along the way, invent a notation for
FOLDL (@@) t ts
where t is a term, and ts a list of terms. The notation is (t @* ts)
in ASCII. This is a "series of applications" with t in the head
position. Prove a bunch of theorems about these forms. All this
stuff goes into basics/appFOLDLTheory.

More support for weak head reduction, including a simpset for
rewriting with it.

Introduce weak-head reduction very sketchily in order to show that
there's a sort-of congruence rule with it and normal order reduction.
Unfortunately, you don't have
M1 -n->* M2 ==> M1 @@ N -n->* M2 @@ N
because the reductions undergone by M1 might produce an abstraction,
in which case the M1 reductions have to stop for the higher level
redex to be reduced. But weak head reduction will never happen at all
once an abstraction is produced so all is well.

Add a more complete characterisation of what it means when the bnf_of
while loop terminates.

Add a constant bnf_of that "calculates" the beta-normal form of a
term, returning SOME t, if t is that form, NONE if there is no such
bnf. The calculation is done with a while loop that doesn't terminate
if there isn't a beta-normal-form.

Two minor results showing that permutations and substitution of
variables for variables commute with the noreduct function.

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.

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.

Symbolic evaluation for beta and normal order reduction is coming
along well. The proofs in bool are much nicer. The
churchnumScript.sml is broken until I get implement conditional
rewriting in my rewriter for beta-reduction (should be easy). The
proofs there should become considerably nicer.

Fully support weaker relations than equality that aren't also
constants. Start to implement a reduction engine for beta-reduction
in the lambda-calculus. Still some wrinkles to work out.

Some useful theorems about normal order reduction, and conversion of
the development of Church numerals to use normal order reduction as
the basic notion. FRESH_TAC proves useful. Doing symbolic evaluation
of lambda-terms is still not all it might be.

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.

Prove the key fact about normal order reduction: if M can beta-reduce
to a normal form N in any way, then normal order reduction can get to
the same place.

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.

Make a start on a theory of normal order reduction (= "topmost
leftmost reduction"). I've decided that this is the best notion of
reduction to be the basis for the computability development.