Up to core types

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.

Update simpLib.remove_theorems to work over terms (lhs patterns) instead of theorems.

Congruence rules aren't removed but it now works for removing AC rewrites, e.g.

> SIMP_CONV (simpLib.remove_theorems [``a * b``] (pure_ss++numSimps.ARITH_AC_ss)) [] ``c * b + a``;
val it =
|- c * b + a = a + c * b:
thm

Add simpLib.remove_theorems.

This is essentially untested - it may or may not help with issue #313. For example:

> SIMP_CONV (simpLib.remove_theorems [DECIDE ``T /\ a = a``] bool_ss) [] ``T /\ x /\ T``;
val it = |- T ∧ x ∧ T ⇔ T ∧ x: thm

Add two more variants of FULL_SIMP_TAC.

The tactics NO_STRIP_FULL_SIMP_TAC and NO_STRIP_REV_FULL_SIMP_TAC don't use STRIP_THM_THEN. This means that simplifying with an assumption ``a \/ b`` will not split the current goal into two sub-goals.

Add REV_FULL_SIMP_TAC. This is the same as FULL_SIMP_TAC but it simplifies assumptions in the reverse order.

Allow simpset fragments to contain pre-order simplification data.

Addition of destructors and recognizers for datatypes.
So far, I've just got basic support put in.

Some other trivial mods as well.

Add ssfrag_names_of, which lists the fragment names within in a simpset.

Handle compilation error for stringSimps; change ssfrag internals.

Clearly, nothing used that file because it was only Moscow ML
compilation that complained about it. Anyway, I've added a
destructor function to the simpLib API for getting the rewrites out
of a simpset fragment. I also changed the internal representation
so that SSFRAG is no longer the constructor. Instead SSFRAG_CON is,
and I will now be able to add additional fields to the record that
it takes as an argument.

Make ssfrag an abstract type, and SSFRAG a function, not a constructor.

This will help me add extra components to ssfrag values while retaining
much of the old API.

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

Rework the handling of bounded rewrites to fix bug in previous check-in.

Unfortunately, the type of the filter field of a ssfrag has to change;
I'll adjust our documentation shortly.

Removed trailing whitespace from all .sml and .sig files.

This affects over 900 files and was done using emacs's delete-trailing-whitespace
function in batch mode. Building the system with Poly/ML and Moscow ML seems to
work, so I'm hoping these changes don't break anything. Please complain if
they do!

Add an "easy-to-use" interface to the rewrite-with-preorders
functionality. I will document this in the DESCRIPTION before we
release.

Add an entry-point to the simpLib API that I hope will be sufficient
to allow congLib-like functionality in the base simplifier.

Implement a scheme whereby a simpset can be limited to apply no more
than a limited number of rewrites/conversions/d.p. invocations. The
limit is stored in a simpset. By default all simpsets are unlimited.
To limit a simpset, use
limit n simpset
and it will then stop simplifying after n actions.

There is a border case: if a conditional rewrite requires exactly as
many rewrites to solve its side-conditions as it is limited to, it
will still go through with the rewrite, thereby exceeding the limit by
one (n side conditions, plus the final simplification)

The design is there to give a (better) guarantee of termination than
simpLib currently provides. For this reason, I didn't go with the
otherwise appealing idea of just letting side-condition discharge
ignore the limit entirely.

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.

Tracking facility: only those rewrites that
actually apply are remembered. Can be useful
for teaching students about what the rewriter
has done, but does not keep full information
(such as what subterm is rewritten).

Added entrypoint for making an "ss" thingy from a conversion.

Addition of the parameter relation to the reducers apply function and extraction of traversedata_for_ss out of SIMP_QCONV. Both changes were made to implement congLib

Changed the TypeBase to be indexed by types. Originally it was
indexed by a single string (representing the type operator), then
Michael changed it to a pair of strings (precise representation
of the type operator). The latest change allows non-datatypes to
be added to the TypeBase. This will allow case analysis and
termination proofs to be supported for non-datatypes.

I reckon there are still a few bugs left after the massive
revision, so you might want to wait a while before upgrading.

Wide-ranging change to make the TypeBase export an interface forcing users
to be concerned about which theory their types are from. Interactive users
of the "induction_of", "axiom_of" and similar functions are thrown the only
bone: they can effectively omit the theory parameter by using "" instead
of a theory name.
Prompted by a bug found by Tom Ridge where it was impossible to define
a pattern matching function on a type with the same name as another type
because the pattern-matching code was using dest_type and TypeBase.read
on just the type-operator name.

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.

New entrypoint in simpLib to make it easier to construct custom simpsets.

First cut at adding in useful rewriting annotations, so that people
don't have to remember arcane entrypoints to do things like
incorporating AC reasoning. The provided annotations are

AC : thm -> thm -> thm
Cong : thm -> thm

An invocation like

SIMP_TAC ss [AC th1 th2, ...]

says to use permutative rewriting with th1 and th2 (which are a statement
of associativity and commutativity, respectively). An invocation like

SIMP_TAC ss [Cong th, ...]

says to use th as a congruence rule when rewriting.

Fixes to the induction theorems that TFL produces. Changes to recInduct
to reflect this. Other minor changes.

Robustification of permutative rewriting. Added an entrypoint aimed
at easing construction of simpset of permutative rewrites.

Fixing recInduct in SingleStep.sml, adding RESTR_EVAL thingies to bossLib,
adding distinction between "strip_pair" and "spine_pair" in pairSyntax,
and other minor things.

Initial revision