Fix CaseEq to handle type abbreviations as the specified name

Again allow ancestral data to consume deltas all at once on theory-load

This allows named simpset-fragments to be added to srw_ss. This then
allows those fragments to be easily removed with calls to
diminish_srw_ss. In the 'fix-ancestry' rework this ability was
removed but this did break proofs when diminish_srw_ss calls had no
effect.

Selftest in coretypes demonstrates this with removal of the "one"
fragment.

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.

Make grammar-deltas s-expressions when stored in theory .dat files

This makes them more legible, and is also a prelude to being more
uniform in the treatment of theory data that merges deltas across
ancestors.

Simplify grammar handling by using abstract ancestral data framework

This is not fully worked out yet, and the abstract framework has only
been instantiated on the one test-case. It's definitely worth it
there though as there can be less awful code smashed into
fooTheory.sml files as a result. Aim is to instantiate theorem-sets
in the same way though so that it will be possible to access srw_ss()
as it was at different points in the theory hierarchy.

Not yet clear if AncestryData should be responsible for holding onto
the underlying references that hold the global "values" (grammars,
simpsets, etc).

Changes in examples fix various adjoin calls that either shouldn't be
there at all (TypeBase now has export; or need to be made "after
completion" so that parses work correctly (these should be using
exportable data themselves)).

Update TypeBase to allow updating of induction & axiom theorems

These changes persist (are exported to theory files).

Be more careful over handling of ThmSetData and rebinding of thm names

In particular, it was previously possible to do

val thm = store_thm("thm[some_attribute]", tm1, tac2);
val thm = store_thm("thm", tm2, tac2);

and have the second thm be exported but to pick up the attribute from
the first call. This is clearly outrageous, so now the attribute is
lost when the second theorem is slotted into the theory.

Working through all this found three places where this
double-definition pattern was happening (there may yet be more). In
src/finite_map and src/list the second theorem was clearly just
redundant and could be deleted.

The example in fun-op-sem is slightly more interesting: there it
defines a function (which definition gives that function a "compute"
attribute), and then restates the definition, saving it under the same
name ("foo_def"). Though arguably bad style, it's important that the
second theorem replace the first, and that it should have the
"compute" attribute. Here the change is to explicitly add that
attribute to the second theorem.

Finally, all this work revealed that Theory.sml's handling of the
NewBinding theory-delta hook was wrong and caused changes to be
dropped after the hook function was called. Debugging *that* led me to
add a pp field to the LoadableThyData registration process so that
theory-data values could be inspected more easily. There is also a
trace variable to turn on some debugging output in Theory.

Fix bug: TypeBase.simpls_of not being filled in on load

Code previously looked for possible 1-1 theorem in simpls_of; if it
wasn't there, it would add the "standard simplifications". Now, it
looks for rewrites about the case-constant as :one doesn't have a 1-1
theorem, but should have a case-const theorem rewrite added.

Control generation (and storage) of TypeBase simpls fields better

Core types were picking up extra copies of their simplification fields
and more was being written to disk than necessary.

With test cases

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.

Fix bug in handling of distinctness for large enumerated types

Previous attempt at regression test for this didn't capture scenario
where srw_ss() had already been initialised and correctness relied on
TypeBase hook telling BasicProvers about newly arriving tyinfo.

Performance is still bad when theories dump large tyinfos to disk.

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 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.

Properly enable case-expr p/printing overloads

This had been made the responsibility of the process that stored
TypeBase information, but that didn't interact properly with the
user-delta approach to storing grammar changes. Now the persistent
overloads are emitted separately.

Avoid using pp_strip_case.

This code needs to be fixed before it's used.

Avoid using pp_strip_case.

This code needs to be fixed before it's used.

tweak case pretty-printing: allow free variables

actual free variables on the collapsed right-hand-sides are harmless,
the thing to avoid is including any of the pattern-variables.

fix some problems in the case pretty-printer

1. It needs to not collapse rows that depend on their pattern variables.
2. Only collapse when there are >2 rows to begin with.
3. Use tryfind instead of first twice.

passes selftest, will rebase on master (see #165)

replace broken attempt by a partial solution to #165

Revert "Implement smarter case pretty-printer. Resolves #165."

This reverts commit 86e201abf6b7591de14e79cfbed0e58bc2d34cd7.

Too many bugs. Will continue development on a separate branch.

Implement smarter case pretty-printer. Resolves #165.

Improvements welcome.

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

implemented qba heurtic for pattern matching; don't do splits for which
lead to same result for all cases

started with writing more complex pattern match heuristics

Fix for bug identified in dc26673.

Problem was that TypeBase’s congruence rule for the case constant over
booleans was not the same as COND_CONG, and the former got applied
rather than the latter when a function’s r.h.s. was being rewritten.

Previously, this was not an issue because the case constant over
booleans wasn’t the same term as COND. But when these two got
identified, TFL started to use

> Prim_rec.case_cong_thm BOOL_CASES_AX bool_case_thm;
val it =
|- ∀M M' t1 t2.
(M ⇔ M') ∧ ((M' ⇔ T) ⇒ (t1 = t1')) ∧ ((M' ⇔ F) ⇒ (t2 = t2')) ⇒
((if M then t1 else t2) = if M' then t1' else t2')

as the congruence rule, putting unnecessary = T, and = F stuff into
induction principles for functions.

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!