Implement easier API entrypoints to get at case_eq theorems

Closes #345

Implement code to load/save tyinfos into/out-of TypeBase's database

Rename TypeBase entrypoints for caseeqsplit and friends

Now use case_eq everywhere.

Work on github issue #345

Automatically prove "case-eqsplit" theorems and store in TypeBase

For :num, this theorem looks like

(num_CASE n zc sc = v) <=>
(n = 0) ∧ (zc = v) ∨ ∃x. (n = SUC x) ∧ (sc x = v)

Such theorems can be powerful rewrites when (large) case-expressions
are asserted to be equal to some value or other.

These theorems have to be installed somewhat by hand for early types,
but from list onwards, the Datatype package handles this. This work
leverages earlier work done implementing prove_case_eq_thm (8f16922426).

Take the opportunity to rework TypeBasePure's code to use
FunctionalRecordUpdate.

This is progress with github issue #345.

execute several heuristics for pattern-matching and choose the best result
interface of pattern matching simplified

started with writing more complex pattern match heuristics

Avoid clunky call mechanism for mk_pattern_fn.

Uncovered simple support in TypeBase. Also refined the notion
of "subterm" in the guesser for termination relations in Define.
Now x.fld is a subterm of record term x, which should automate
termination of simple recursions through record fields.

Addition of destructors and recognizers for datatypes.
So far, I've just got basic support put in.

Some other trivial mods as well.

Change src/bool to src/1 as a prelude to experimentation!