quantHeuristicsLibSimple: add some useful rewrites to simpset-fragment

With the simple quantifier instantiation, one was likely to end up with
terms like

``HD l::TL l = l``

or

``l = [HD l]``

or

``X = SOME (THE X)``

Now, some special rewrite rules are added to simplify these to

``~(l = [])``,

``LENGTH l = 0`` and

``IS_SOME X``

respectively.

implement simple quantifier heuristics

The quantifier heuristics library is powerful, but often slow. The
unwind conversions are fast, but have serious restrictions. This commits
adds simple quantifier heuristics. They are based on the techniques
developed for quantifier heuristics library, but only search gap guesses
that don't contain free variables. Some very limited experiments suggest
that it is similarly fast as unwind. It can handle all the cases unwind
can handle. However, it supports also a much richer syntax. Moreover, it
can instantiate in addition to universal and existential quantifiers
also unique existential quantifiers, eliminate select and some.
Moreover, it knows about pairs and lists.

Remove unnecessary structure bracketting

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

quantifierHeuristics tweaks
- some tweaks to make sum_qp behave nicer
- for this some small changes that can be seen as
bug fixes or minor feature improvements

Delete trailing whitespace in src and examples.

A bit more work on list_qp in order to handle LENGTH. For
LENGTH with large numbers, list_len_qp added.
Experimental support for removing redundant function application on
quantified variables added.

Added support for context to quantifier heuristics, add sum_qp

cleanup of quantifier heuristics library

- more sensible names for guesses
- quantHeuristicsLib renamed to quantHeuristicsLibBase
- quantHeuristicsLibArgs renamed to quantHeuristicsLibParameters
- new shorter signature defined in quantHeuristicsLib
- adaptation of usage of quantHeuristicsLib

Delete trailing whitespace in src/

More on quantfier heuristics (I did not add all changes to the first commit)

Remove trailing whitespace in source files.

- reimplementation of quantHeuristicsLib.
- move parts of quantHeuristicsLib to quantHeuristicsTools
- selftest added

Before guesses were justified by hand crafted theorems. There were modified using low level forward proof techniques. This resulted in quantHeuristicsLib being hard to understand and maintain.

This reimplementation exploits recent addition to pairTools about handling paired quantification in order to introduce general predicates for guess theorems. Defining special predicates allows proving general lemmata easily. quantHeuristicsLib can the use the lemmata instead of low level proofs. However, this comes with the additional cost of introducing and eliminating tupled quantifiers.

The new version is easier to understand and maintain. Moreover, it became much simpler to add user specified heuristics. The behavior changed slightly. For example, unnecessary priming of newly introduced variables has been eliminated.

src/num/theories/SingleStep.{sig,sml} is gone. The
defininitions of Cases, Cases_on, Induct, Induct_on,
CASE_TAC (and co.) are now in basicProof/BasicProvers.
completeInduct_on and measureInduct_on are now in
numLib. recInduct is now in src/tfl/Induction.sml.
All these are collected in bossLib, so the changes
should be invisible to ordinary users.

SingleStep.*.doc has been changed accordingly.

BasicProvers.NORM_TAC should now automatically perform
all case splits (from if-then-else expressions as
well as case expression) arising anywhere in the goal.

Removed trailing whitespace from all .sml and .sig files.

This affects over 900 files and was done using emacs's delete-trailing-whitespace
function in batch mode. Building the system with Poly/ML and Moscow ML seems to
work, so I'm hoping these changes don't break anything. Please complain if
they do!

Now occurences of a variable are tried to be removed before a possible instantiation is searched. For example
"?x. P /\ (f 2 = f x) /\ (Q (f x))" is simplied to "?x. P /\ (f 2 = f x) /\ (Q (f 2))" before an instantiation for x is searched. This enables the heuristics to instantiate x with 2.

Moreover, an additional field was added to qhcas. Now one can specifiy a list of theorems used for the final simplification after an instantiation has been picked.

quantHeuristics is a library that instantiates quantifiers with guesses found by heuristics. Please see quantHeuristicsLib-examples.txt for some documentation and examples.