Provide more ancestry-based entrypoints for stateful simpsets

In particular, allow for recreation of the simpset as it existed on
theory entry. E.g., a call to

recreate_sset_at_parentage (parents "list")

will make the simpset take on its value as it existed when execution
of the listScript began.

Make TypeBase ancestry-aware

The fix to Boolify/src/Encode.sml attempts to be semantics-preserving,
but there are no test-cases for this code.

Improve TypeBase API for reporting on record fields

Datatype code now bypasses treatment of "big records". This stuff can
all be deleted and I will be happy to see it go as it is horrifically
complicated, and usually only serves to confuse users.

Thanks to a CakeML Slack discussion for the push to make the API
change.

Update TypeBase to allow updating of induction & axiom theorems

These changes persist (are exported to theory files).

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!