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

Generate "standard" datatype simpl rewrites as tyinfos are loaded

This saves us from having to write them out to disk, which can make
for unnecessarily large theory.dat files.

Re-implement Datatype package with TypeBase sexps (not adjoin)

Implement code to convert tyinfo's to and from ThyDataSexp.t

Format is rather "wordier" than necessary, but the extra (redundant)
field names should be helpful for debugging.

Up to hol.state0

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.

Provide toPmatchThry entry-point in TypeBasePure.

This converts from a full-blown TypeBase value into a “thry” as
required by the Pmatch module. The “thry” type is simply a lookup
function that returns case-constant and constructor information for a
given type.

Allow "non-datatypes" in TypeBase to have optional induction thm.

Provide appropriate values for this field for finite sets, strings,
integers, finite maps and words.

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!