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 global simpset state easier to recreate with "logged_update"

This entry-point records that a change to the global simpset has
happened within a piece of code (rather than a script). The change is
made (as before), but the change is also recorded so that it can be
recreated/applied to different base simpsets.

Extend BasicProvers interface with temp_setsimpset

Reimplement global simpset to be "ancestry-aware"

Allows API to be enriched with {temp_,}set_simpset_ancestry and
thy_simpset functions.

Both of these don't fold in appropriate additions from the TypeBase
after these calculations yet.

Tweak ThmSetData API: take callbacks with more honest types

In particular, the callbacks are always only ever called on singleton
lists, so it seems silly to ask the user for functions with types that
have lists.

Fix diminish_srw_ss invalidating earlier call to temp_delsimps

With test cases. Also change type of simpLib.remove_ssfrags to have
the acted on type and return type be adjacent. I.e., prefer

foo : B -> A -> A

over

foo : A -> B -> A

as the former curries to create a nice update function.

Alter VAR_EQ_TAC to call TIDY_ABBREVS after invocation

TIDY_ABBREVS "purges" abbreviations that have become malformed, where

- "malformed" means no longer of form Abbrev (var = exp), with exp not
itself a variable
- "purge" means Abbrev(e1 = e2) becomes e2 = e1, and Abbrev(other_exp)
becomes other_exp.

The action of TIDY_ABBREVS is included in the ABBREV_ss simpset
fragment, which is in turn included in the stateful simpset.

The calling of TIDY_ABBREVS is the only change in the behaviour of
VAR_EQ_TAC, and this can be turned off with the
BasicProvers.var_eq_old trace.

Provide new term-based version of Cases_on

This version takes an extra string list parameter for specifying names
to be used in the split.

revised namedCases{_on} to support auto-name generation for underscored names

adding ability to specify names introduced by Cases and Cases_on

Provide entry-point to temporarily remove rewrites from srw_ss

So, delsimps ["foo", "bar", "baz"] removes those rewrites and exports
the change to future theories; temp_delsimps ["foo", "bar", "baz"]
removes the rewrites temporarily (i.e., only in the current theory).

Rework persistent ThmSetData API to allow for "removal" of elements

The removals are strings encoding removal "instructions", which are up
to the underlying consumer to interpret. Still to test any of this
new machinery, but the old behaviours have been preserved.

Move without loss of generality tacticals to new library.

Add “SPLICE_CONJ_CONV”; add tacticals “wlog_tac” and “wlog_then”.

Get core HOL to build with new definition of "by"

Progress with github issue #407

More moving lcsymtacs implementations elsewhere

Eventually lcsymtacs will just be a bunch of 'open' declarations, and
then people won't bother to include it at all.

extra semicolons removed from (some) .sig files

Implement new suffices_by tactic in BasicProvers and bossLib.

Closes #116.

Improvements to Induct and Induct_on for non-datatypes.

Bug in TypeBase.is_case. It would return true
on

option_case NONE

Fixes to CASE_TAC to make proofs in Boolify go through.

Fix to CASE_TAC, which could loop on nested cases over the option type
(and thus, presumably other types as well). Also, added a few more
entrypoints for case-splitting, e.g. FULL_CASE_TAC (do a case split
anywhere in goal, including assumptions) and EVERY_CASE_TAC (do all
possible case splits).

Also beefed up NORM_TAC so that it splits case expressions. Possibly
this could be migrated to RW_TAC and kin, but that might break a lot
of proofs.

src/num/theories/SingleStep.{sig,sml} is gone. The
defininitions of Cases, Cases_on, Induct, Induct_on,
CASE_TAC (and co.) are now in basicProof/BasicProvers.
completeInduct_on and measureInduct_on are now in
numLib. recInduct is now in src/tfl/Induction.sml.
All these are collected in bossLib, so the changes
should be invisible to ordinary users.

SingleStep.*.doc has been changed accordingly.

BasicProvers.NORM_TAC should now automatically perform
all case splits (from if-then-else expressions as
well as case expression) arising anywhere in the goal.

Added a few more operations for working with simpsets and simpset fragments.
In particular, added the facility to remove named fragments from a simpset.
This is done fairly crudely -- the new simpset is simply rebuilt using all of
the remaining fragments.

This enables you do do things like:

- SIMP_CONV (simpLib.remove_ssfrags (srw_ss()) ["word arith"]) [] ``...``

and

- val ss = diminish_srw_ss ["word arith","word logic"];
- e (SRW_TAC [] []);
- val _ = augment_srw_ss ss;

Doing this will re-order the fragments, which I believe can affect behaviour?
diminish_srw_ss isn't persistent -- not sure if that is good or not.

The new operations are:

> val name_ss : string -> ssfrag -> ssfrag

(* Give a name to a fragment. *)

> val named_merge_ss : string -> ssfrag list -> ssfrag

(* A version of merge_ss that allows users to name the merged fragment. *)

> val std_conv_ss : stdconvdata -> ssfrag

where

type stdconvdata = { name: string, pats: term list, conv: conv }

(* A simplified interface to conv_ss. For conversions with: no
side-conditions, trace level 2 and for a list of "variable only" keys. *)

> partition_ssfrags : string list -> ssfrag list ->
(ssfrag list * ssfrag list)

(* Partition a simpset fragment list: lhs for fragments in a list of
names and rhs for those not in the list. *)

> remove_ssfrags : simpset -> string list -> simpset

(* Remove named fragments from a simpset. *)

> diminish_srw_ss : string list -> simpLib.ssfrag list

(* Remove named fragments from srw_ss. Returns removed fragments. *)

Complete implementation of generic theory data feature, and use it to
implement the exportable rewrites used in srw_ss(). The code still
needs some more polishing. Hopefully that will come as I convert
other "stored data features" to use the same underlying code.

Change export_rewrites back to its old API (without requiring an extra
string). When exported, the resulting simpset fragment always picked
up the name of the theory to be the base of its name, so there didn't
seem much point in giving users a false impression of naming power.

A whole mess of small changes intended
at making simpsets prettyprint informatively
in the interactive loop. Very possibly
I haven't updated all the files in the examples
directories.

Changed a couple of misleading/annoying names. The type ssdata is now
called ssfrag (to bring it into line with documentation that talks about
simpset fragments), and the constructor SIMPSET is now called SSFRAG.
It never created a simpset, so the latter was a stupid name.

Make LET_ELIM_TAC part of STP_TAC, and thus SRW_TAC and RW_TAC.
The LEAVE_LET theorem can be used to tell this not to happen if included
in the list of theorems passed to the rewrite tactics.

New entry point in BasicProvers called LET_ELIM_TAC to do lovely things
with lets, whether uncurried or not. They're lifted out of the goal
and turned into abbreviations into the assumptions. Plan is to tack
LET_ELIM_TAC into the basic action of RW_TAC and SRW_TAC as well.

New treatment of abbreviations. Documentation still to be updated.
Backwards compatibility illustrated in examples/lambda/standardisationScript
and examples/arm6. New techniques and entry-points illustrated in
core distribution and some of the lambda example scripts.

Minor fixes to support rewriting annotations.

Added VAR_EQ_TAC to BasicProvers. It eliminates assumptions of the
form v = M or M = v (provided v doesn't occur as a proper subterm of M).

The other changes are just messing about.

Simplified some proofs in MachineTransitionScript.

Reverted to Taupo-6 RW_TAC. This should make RW_TAC faster, and a little
less eager to case-split conditionals. Some proofs may break as a result.
In that case, use the drop-in replacement BasicProvers.NORM_TAC.

Term destructors now operate using same_const to check the operator
of the term being destructed. This may increase efficiency somewhat.
There were consequent changes to the xSyntax modules of the system.

More machinery to make the "stateful" rewriter even snappier.
Script files for theories can now do a
val _ = export_rewrites ["th1", "th2"]
where the argument is a list of strings corresponding to theorem names.
If the theorem names are from the current theory, they can be quoted
as is. If theorems are to be included from elsewhere, dotted IDs
have to be used.

When the corresponding theory loads, it automatically extends the
stateful rewriter's underlying simpset with the given simpset. The
theory's interface is also extended with a value thyname_rwts of
type simpLib.ssdata corresponding to the rewrites specified.

New SRW_TAC tactic (stateful RW_TAC) implemented.

Kananaskis compatibility.

Split-off from bossLib, so that these things are available earlier
in the development of the system.