Simplify grammar handling by using abstract ancestral data framework

This is not fully worked out yet, and the abstract framework has only
been instantiated on the one test-case. It's definitely worth it
there though as there can be less awful code smashed into
fooTheory.sml files as a result. Aim is to instantiate theorem-sets
in the same way though so that it will be possible to access srw_ss()
as it was at different points in the theory hierarchy.

Not yet clear if AncestryData should be responsible for holding onto
the underlying references that hold the global "values" (grammars,
simpsets, etc).

Changes in examples fix various adjoin calls that either shouldn't be
there at all (TypeBase now has export; or need to be made "after
completion" so that parses work correctly (these should be using
exportable data themselves)).

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

Use new syntax for some theorems in examples/lambda/basics/term

Fix some adjoin calls in examples/lambda

Extra parameter for new_type command in nomdatatype allowing for multi-types.

Doesn't work unless each 'type' allows a 'VAR' constructor, which is not the case
in first order formulas and terms, for example.

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.

Rename TruePrefix to Prefix; use fixity options with NONE for what was Prefix.

90+% of this work was done by Ramana Kumar. The following list are
the commits for a series of individual commits that have been squished
into one big change:
* remove mention of TruePrefix from the add_rule docfile
* first batch of changes removing TruePrefix from src/parse
* replace TruePrefix by Prefix in boolScript.sml
* remove TruePrefix from Rsyntax
is a fixity ever required for new_specification?
* some more Prefix -> NONE and TruePrefix -> Prefix in theories
* TruePrefix changes for datatype
* TruePrefix changes for res_quan
* TruePrefix->Prefix in a TeX selftest
* TruePrefix changes for quotient
* TruePrefix changes for integer and real
* fix quotient examples for TruePrefix removal
* more fixes for quotient examples
* fixes for lambda example for TruePrefix removal
* Reword description manual in light of removal of TruePrefix.
* Fix msgTheory quotient example; Poly 5.3 had problems with monotypes.
* Fixes for files in examples/lambda given removal of TruePrefix.
* Fix in examples/unification given removal of TruePrefix.
* Fix in examples/HolCheck given removal of TruePrefix.
* Fixes in examples/acl2 given removal of TruePrefix.

Fix build errors caused by me moving 'some' theorems.

Move a couple of useful theorems about 'some' into optionTheory.

Get lambda/typing directory to build again.

Had to deal with termScript stealing the \rightarrow syntax (I made
that theft local to termScript); and with tight equality.

Prove a varying parameter version of the term recursion principle.

Get termScript to compile with the new principle.
More work will be required to adjust remaining lambda-calculus scripts.

Another minor strengthening of the lambda-term recursion principle.

It still doesn't quite say enough for the 'parameter' version.

Further strengthening of the lambda-term recursion principle.

The assumption that the results of recursive calls are always finitely
supported by the free variables of the argument (plus any vars in the
support of the helper functions) can be used in the FCB as well as in the
assumptions about the support of the helper functions.

Weaken side-conditions needed for recursions on lambda-terms.

Rework lambda-term recursion principle proof once more.

It's simpler and more polished, mostly following the IJCAR'06 paper by
Urban and Berghofer, though slightly simpler even than that. I
believe I have one more useful change in me for this development, and
then I'll attempt to do the whole thing again, generically in
genericTerms.

The change to term_posnScript comes about because it relied slightly
too much on the exact form of the principle. (Previously tm_recursion
was just recursion and not iteration; putting iteration in from the
outset seems harmless.)

Slight simplify the proof of the lambda-terms' recursion theorem.

In particular, change "condition 16" from

?a. "a fresh" /\ !x. something else

into

!a x. "a fresh" ==> something else

This "some-all" transformation (the two are equivalent thanks to
properties of freshness) removes a quantifier alternation.

Simplify the proof of the term recursion principle for lambda-terms.

Revise the base theory of nominal sets to make much greater use of
overloading, thereby reduce the number of Define-d constants. This
reduces the number of theorems as well. With some theorems
disappearing, there were a few knock-on effects in descendent
theories.

Proof that the application constructor isn't cyclic. (We could
probably prove results like these for all inductive data types...)

Fix for a broken proof (caused by change to FV rewrites), that I
didn't spot the first time through (somewhat disturbingly).

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.

Implement a FRESH_TAC that freshens bound variables throughout a term.

Recast binderLib's internal databases about "binder"-information for
types. In the process, give up on the attempt to make this technology
work for the "old" style of recursion theorem as in my TPHOLs paper.
Now the only style supported is the quotient + nominal proof (which is
what is in barendregt).

A start on computability done in the lambda-calculus.
(Change to termScript makes the defining theorem about substitution
an automatic rewrite.)

Missed fixing these in the previous sweep. Again, the problems were
proofs that relied on string variables being given names beginning
with the character #"s".

Proofs and tools broke when I changed the behaviour of
parse_in_context. Thanks for Peter for alerting me to the problem
(should be running build -selftest more often myself).

(Also make barendregt directory QUIT_ON_FAILURE, and removed a
duplicate proof in finite_developments.)

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.

Define permutation over finite maps, and then use finite maps to
define simultaneous substitution over terms. Use fm ' t syntax to
mean application of finite map fm (mapping strings to terms) to term
t. Prove some simple properties of simultaneous substitution.

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