remove lcsymtacs (github issue #666)

The lcsymtacs structure is regarded superseded as it plainly is
a shorthand for opening the following modules:
Abbrev HolKernel boolLib Tactic Tactical BasicProvers simpLib
Rewrite bossLib Thm_cont

Fix examples/lambda/barendregt for tight equality

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.

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.

Some additional rewrites of "general utility".

Weak-head reduction (like all the others) can't create new free
variables. Also add the substitutivity result for w.h. as a
congruence rule.

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.

Remove a redundant abbreviation tactic in the proof that weak head reduction is substitutive (i.e., if you have a w.h. reduction from M to N, then you will also have one from [P/v]M to [P/v]N).

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.

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.