eliminated some ref-matches

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.

extend interface of reducers in simplifier

reducers, i.e. dprocs, are the most flexible way to use the
simplifier. Reducers can use a callback to resolve
side-conditions. However the old interface only allowed
proving these side-conditions. This commits adds an additional
callback interface, that allows to only simplify
side-conditions. This allows using additional tools to
prove a sidecondition after it has already been processed by
the callback.

rename Ho_Net.empty_net to Ho_Net.empty

All similar structures (e.g. Net and Raw) use "empty" not "empty_net";
it seems right to follow a single naming convention.

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

Remove unnecessary abstype constructions in {simp,cong}Lib.

These just make debugging more painful than it needs to be.

Allow simpset fragments to contain pre-order simplification data.

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.

Remove an unnecessary infix declaration.

Fix a bug in the handling of weakened 'subset' theorems.

A subset theorem is one of the form |- R' x y ==> R x y where R' is a
relation that might appear in an input theorem, and R is the relation
that one wishes to rewrite with respect to. When the weakened rewriter
sees a bit of context of the form R' x y, it applies modus ponens to
derive useful information for its R-rewriting.

Get congLib to compile again by changing Traverse API again.

Rewriters get access both to the term of the current relation and a
function that will give them an instance of reflexivity for that
relation. Thomas's code was using this possibility.

Generalise and correct "weak congruence" handling.

Some notes:
- Add extra tracing, including to congruence rule application in
simplifier.

In particular, spit out a message when a hypothesis is recognised as
a side condition rather than something that will prompt a recursive
invocation of the 'depther'.

- If rewriting with a relation that includes a variable that gets
instantiated, the specific relation being used needs to be included
in the argument that gets passed to the reducer. How else is the
atomic rewriting step to know which theorem is to be produced?
Think of rewriting MOD 5, say. When it happens upon argument 7, the
atomic step should produce MODEQ 5 7 (7 MOD 5), where MODEQ 5 is the
rewriting relation.

- Congruence opener needs to avoid treating user vars as genvars.

Hitherto, it was looking at the RHS of the congruence's conclusion
and treating all the vars there as things that were due to get
instantiated through the recursive invocation of the simplifier.
But if the relation can take a variable, that variable may come from
the conclusion.

In particular, imagine

0 < n ==> MODEQ n genv1 genv2 ==> (genv1 MOD n = genv2 MOD n)

The n has been instantiated from the term to be rewritten, and
shouldn't be viewed as a genvar.

Generalise congruence API to handle terms with free vars as equivs.

Correct a minor problem in remembering the ssfrags making up a simpset.

In particular, the old code wouldn't remember that a fragment had been
added (it wouldn't add it at all) if it had the same name as one
already in the set. This was done with the op_insert same_frag.

Now the code just conses the fragment onto the list. It might be
better to merge the incoming fragment with one in the set of the same
name, but I don't know that there's really a problem with having
multiples of the same name.

The problem particularly arises when successive calls to
export_rewrites in a theory cause multiple fragments to be added to
the srw_ss() all with the same name (the name of the current theory).

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

Delete redundant copy of dest_tagged_rewrite from simpLib.sml.

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.

Adding an ssfrag to a simpset now adds frag rwts to set's dprocs as context.

This has a few knock-on effects, mainly on use of ARITH_ss, which had
hitherto only been getting context from goal assumptions and theorems
passed to the simp-tactics at the top-level. The ARITH_ss addctxt
function needs to be a bit fussier in order to avoid picking up
unusable junk.

The intention with the change is to get exported rewrites for
relations other than equality to work, as per the change to
churchboolScript (this should be the first of many). One change this
then required in add_relsimps was to have it check for looping
rewrites (particularly: if reflexivity of the relation is added as a
normal equality rewrite, which is reasonable, this can't be allowed to
put the relation-rewriter into a loop).

Added trace information to signal when rewrites with
existential variables are encountered.

Fix for bug identified in r6991.

As has so often been the case, eta-expanding wins the day!

Simplification with pre-orders can now use bounded rewrites.

Modify the standard conditional rewrite behaviour so that if a rewrite
theorem has been bounded (with Once, or Ntimes), then it is allowed to
be applied in circumstances where the simplifier's looping detection
would otherwise reject it. This allows (Once EQ_SYM_EQ) to do
something, as the new self-test demonstrates.

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

Fix for a bug whereby the wrong reflexivity function might get called
when a weakening congruence was applied.

Allow congruence rules for relations other than equality to be added
via the congs field of a ss-fragment. This means that using the
special 'Cong' marker also works.

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

Realise that eta-expanding the definitions of SIMP_CONV and SIMP_PROVE
will solve the bug which causes Once and Ntimes not to work correctly
in situations like
map (SIMP_CONV bool_ss [Once combinTheory.o_THM])
[``(f o g o h) x``, ``(f o g) x``];
or more realistically, when a single tactic is applied to multiple
goals, when that tactic is after a THEN.

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

Definitions like

(f 0w = T) /\ (f 23w = F) /\ (f 12w = F)

now work. Also improved the performance of basic
equality conversions between literals (char_EQ_CONV,
string_EQ_CONV, NEQ_CONV, and word_EQ_CONV) in
the case where the involved literals are actually
equal. Now trying to figure out how to teach
REDUCE_CONV and EVAL about this.

Additional functionality for abbreviations.

1. The labels library has been merged into
markerLib and the src/labels directory eliminated.
2. Have added markerSyntax structure.
3. Operations on abbrevs used to all be in
structure Q, even those that didn't deal
with quotations (like UNABBREV_ALL_TAC). Now
markerLib provides all abbrev. operations and
these take terms. Operations that benefit from
quotes, e.g., ABBREV_TAC, MATCH_ABBREV_TAC, etc.
are still to be found in Q.
4. Abbrevs are kept reduced by the simplifiers and
there is a REABBREV_TAC which can be separately called.
This sorts abbrevs topologically, so that they get
restored in a sensible order.
5. For situations where one wants to get rid of all
abbrevs, apply a tactic, and then restore the abbrevs,
there is WITHOUT_ABBREVS: tactic->tactic.
6. Have added a simple topological sort to Lib.
7. Updated proofs in the src directories, and also
in examples/lambda.

Changed behaviour of simplifier to
propagate the abbreviation coming from
a let binding in the goal being moved to
the assumptions. This helps keep the goal
in "fully abbreviated form". Also added

Q.REABBREV_TAC

which re-abbreviates the goal and

Q.WITHOUT_ABBREVS tac

which temporarily removes all abbreviations,
runs tac, then reabbreviates.

Probably, Q is not the right place for these
functions, but the rest of the abbreviation
stuff is there.

Also added some internal documentation on what
Q.ABBRS_THEN does, and the like.

This check-in mainly fixes a problem with
literals occurring in patterns of TFL-style
definitions. There are a host of other minor
changes as well.

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.

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.

Add a comment about how theorems get added to simpset contexts (in the
"reverse" order). Visible in
- SIMP_CONV bool_ss [ASSUME ``!x. f x = x + 1``,
ASSUME ``!x. f x = x + 2``] ``f (x:num) > 4``;
> val it = [.] |- f x > 4 = x + 1 > 4 : thm
(Later rewrites take precedence over earlier ones.)

A little code reorganisation and a fix for a bug in the implementation
of ASM_SIMP_TAC and FULL_SIMP_TAC: abbreviation references in the
argument list weren't being dealt with early enough. In the case of
ASM_SIMP_TAC this caused the effect of an abbreviation being eliminated
in the assumptions but not in the goal.

Slight robustification of the conversion from lists of theorems to
rewrites. Now, if the simpset's conversion function doesn't do enough
to create an equality out of a theorem, that theorem is just dropped.
Previous behaviour raised an untrapped exception. This fixes S/F
bug #963358.

Alter the way BOUNDED/UNBOUNDED rewriting works, so that the BOUNDED
tag is now a theorem hypothesis of a special form, and so there is no
UNBOUNDED tag at all (i.e., the default is to be unbounded). This is
simpler, and means that if you come to write a simplifier filter (as
in the case of SUC_FILTER_ss) you don't need to worry about whether
or not the rewrite is bounded. (Will add this check-in message to
changed files in src/simp/src that got mistakenly tagged with my change
to selftest there.)

Add a test to check on bounded simplification.

Trace the production of the rewrites that will actually get used
by the conditional rewriter, and remove the assumption that all
rewrite theorems will be tagged with either BOUNDED or UNBOUNDED.
(The assumption doesn't hold in the empty_ss simpset, and this was
causing exceptions when people did (silly) things like
mk_simpset [pred_setSimps.PRED_SET_ss]
)

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.

Added another option to the sinplifier. You can specify how many times
a rewrite rule is applied by the "Ntimes" tag

SIMP_TAC std_ss [Ntimes <thm> 2]

will allow thm to be used as a rewrite rule at most 2 times. As a shorthand,
you can apply a rewrite only once wiht

SIMP_TAC std_ss [Once <thm>, ...]

Of course, other theorems can be chucked in too, using the other annotations
too, if you want.

Testing has been a bit disappointing, since the obvious uses: restricting
application of looping rewrites, is already mostly taken care of with
permutative rewriting. However, rewriting with "destructor"-style
recursion equations can be controlled with Ntimes and Once.

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.

It turns out that I don't need to do anything really to make new
conversions and the simplifier play together properly. This is
because of two things:
* SIMP_CONV is really just call to TRY_CONV (internal_conv ..), and
this use of TRY_CONV ensures that the internal uses of HOL_ERRs to
indicate changelessness get turned into UNCHANGEDs appropriately.
* The use of Lib.tryfind in the code that attempts to do things
(including the application of user-supplied conversions),
automatically traps and drops all but Interrupt exceptions. This
means that conversions that raise UNCHANGED won't throw a spanner
in the simplifier's works.

This change merely allows user-conversions to be better traced. The
fact that they might be throwing who-knows-what should be visible
now.

The call to thm_to_string that I've deleted here could cause the addition
of theorems to a simpset to fail because of a problem in the pretty-printer.
Additionally, the information this printed out at level 3 just repeated
information that COND_REWR_CONV printed out at level 2.

Again, being explicit here can help Holmake later on, though it's still
not a guarantee.

Initial ideas towards labelled assumption implementation.

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.

Fixed AC rewriting so that it works now.

Made tracing of rewrites slightly more informative, by having them
print out the theorem that is the rewrite rule.

Paired syntax.

Elimination of dependence on Ho_theorems.

Fixes in order to remove library file dependencies on global grammars.

Initial revision