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

Add Option constructor to ThyDataSexp.t

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)

Force users of ThyDataSexp to provide their own merge function

Provide a couple of likely candidates for this purpose.

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.

Fix bug in repeated Datatype calls with mutual recursion

Closes #435

Fixes with polymorphic record literals

1. When you write <| fld1 := foo ; fld2 := bar |> there is secretly an
ARB term hiding in the result. You don't want that ARB term to be
unnecessarily polymorphic.

2. TypeBase.mk_record has to adjust for the possibility that fupds can
have types of the form

fupd : (α fldty -> β fldty) -> (α,γ) rcd -> (β, γ) rcd

Continuing work on github issue #173

Remove duplication of code between Pmatch and TypeBasePure.

The case-syntax code in the latter has moved entirely to Pmatch.

Fix for bug in dest_case caused by use of hd rather than last.

It turns out that last will raise a HOL_ERR on the empty list, but hd
raises Empty, of course. (This is because we have our own version of
last in Lib, and I’m far from sure this is a good idea.)

Fix TypeBase’s dest_case entry-points.

This makes pretty-printing work.

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.

Start of project to flip argument order in case constants.

One scary (but probably optional) change is to do away with bool_case
constant because it is now identical to COND. This could be reversed,
but having two constants with exactly the same type and semantics does
seem silly. I think the parsing/pretty-printing behaviour can be made
sensible even in the face of this unification.

Prim_rec’s functions for defining case constants and proving case
congruence theorems have been adjusted appropriately.

This is relevant to Github issue #97.

Remove some trailing whitespace.

Added size functions for finite sets, maps, and bags.

These are helpful for measures supporting recursive definitions and
induction schemes. The size functions have been added to the TypeBase,
with the intent that Induct, Induct_on, Cases, and Cases_on should be
applicable. (However, this has not been checked yet, so these might
not work.)

The size of a finite set is the number of elements in it, plus the
sizes of all the elements. (The size of a set with 0 as an element is
larger than that set with the zero deleted.)

The size of a finite map is the number of mapped elements, plus the
sizes of the mapped elements. Key size is ignored.

The size of a finite multiset is the number of elements in the
multiset plus the sizes of the elements. There are more extensive
orderings (e.g. the multiset order) but they aren't measures, which is
important for the way termination proofs are automated.

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.

Remove trailing whitespace in source files.

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!