Fix bug in caching behind arith d.p's

It is important to track not only the hypotheses of the theorems in
the context (typically the assumptions in the goal), but also the
statements of the conclusions. If for example, one adds a theorem to
the mix that doesn't have any hypotheses at all, the fact that this is
available should be seen as an extension of the context and the cache
shouldn't reject the new attempt to prove the goal.

Closes github issue #477

Use Sref to store simplifier caches

Remove an unnecessary level of references in simplifier Cache code

eliminated some ref-matches

Remove Polyhash. No performance difference in building HOL.

* Reformat a definition that had become strangely wrapped
* Refine a comment about the nature of the graph that is built
* Fix a bug whereby ground contexts were turned into theorems with incorrect
hypotheses. So, instead of [p /\ (3 = 5)] |- 3 = 5, you might get
[3 = 5] |- 3 = 5
which would cause subsequent attempts to eliminate assumptions in
congruence rules to fail. This in turn led to theorems with extra
assumptions floating 'round.

Fix for a bug in the simplifier's "relevance cache". If a goal had
ground hypotheses, these weren't tested for unsatisfiability.

My last check-in broke the building of the n-bit word theories (should
always try the -selftest option to build to catch this) because the
implementation of relevance analysis didn't believe that SUC a <= 2 ** WL
was relevant to proving 0 < 2 ** WL. The solution is to realise that
even ground terms may end up being treated as variables by decision
procedures. So, there is now an additional parameter to RCACHE : a function
that takes a term and returns a list of terms that should be treated
as free variables in the relevance analysis.

A better cache function, RCACHE that does relevance analysis to speed
up the rejection of formulas that are sure to fail.

By switching to HOLsets from unordered lists, lose a quadratic subset
test when checking hypotheses.

Remove dependency of this code on built-in equality (which is what
Polyhash tables use).

A couple of changes: caches can be examined in a better way than just
printing them, and a new trace "action", lazy text, which will potentially
save time when a trace is not looked at. (The text might print out a term,
say.)

Paired syntax.

Added a couple of extra trace statements to operations on caches, and
implemented a print_cache function.

Initial revision