Move without loss of generality tacticals to new library.

Implement easier API entrypoints to get at case_eq theorems

Closes #345

Document changes to by and new subgoal tactic

Also make sure that the latter (and its alias, sg) are available
through the bossLib signature.

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

Progress with github issue #407

implement simple quantifier heuristics

The quantifier heuristics library is powerful, but often slow. The
unwind conversions are fast, but have serious restrictions. This commits
adds simple quantifier heuristics. They are based on the techniques
developed for quantifier heuristics library, but only search gap guesses
that don't contain free variables. Some very limited experiments suggest
that it is similarly fast as unwind. It can handle all the cases unwind
can handle. However, it supports also a much richer syntax. Moreover, it
can instantiate in addition to universal and existential quantifiers
also unique existential quantifiers, eliminate select and some.
Moreover, it knows about pairs and lists.

Rename pat_assum to pat_x_assum; provide pat_assum

To be consistent with naming conventions elsewhere, change the name of
qpat_assum (and PAT_ASSUM, and Q.PAT_ASSUM) to include an extra _x_ (or
_X_), indicating that the matching assumption is pulled out of the
assumption list.

Use the old names to provide a version that doesn't pull the assumption
out of the list.

Again, seeking consistency with other similar tactics, make variable
names that appear in the pattern and the goal be forced to have the type
that they have in the goal.

Implement Q.RENAME_TAC / bossLib.rename

This tactic is more powerful than rename1 as it allows multiple patterns
to be matched at once, and without regard to the initial goal's free
variables (which might otherwise cause unpredictable clashes).

Rename: qcase_tac/rename1; Q.FIND_CASE_TAC/Q.RENAME1_TAC

This use of the "case" substring was just confusing given things like
Cases_on. The "1" is there because I want to now implement a more
general version that
- deals with the issue (identified in the .doc file), where existing
names in the goal can still get in the way; and
- allows multiple subterms to be matched and renamed as a unit

Though seemingly independent, the second feature is really needed if the
first is to be done: implementing the first will require all the free
variables in a goal to be renamed away (to genvars, I expect), and then
it's impossible to ground particular matches against known free
variables.

Implement and document new split_pair_case_tac

Add new pairarg_tac for splitting pairs

Documented in .doc file.

From CakeML.

Define special backtracking cases of pat_assum

In particular, the "pattern" is a single term or quotation that has to
either be the head constant of the assumption or the head of the lhs of
the assumption. Unlike pat_assum as it stands currently, the behaviour
backtracks (à la first_assum) if the theorem-tactic doesn't succeed with
the first assumption found.

Versions come in "copy assumption" and "cut assumption" versions, just
like first_assum and first_x_assum.

add lowercase subterm-abbrev tactics to bossLib. closes #81

Move kall_tac to bossLib

Closes #274

All l/case short simp tacs use LET_ss + ARITH_ss

This means that fs and rfs pick up LET_ss and ARITH_ss, making them
indistinguishable from the 'l' versions.

More l/case names into bossLib

Work on #274

Corrections for last commit

Move more tactics from lcsymtacs to bossLib

Work on #274

pattern_matches: add to bossLib

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.

add quantHeuristicsLib abbreviations to bossLib

Start porting llists to Hol_coreln

update

towards co-mpletion

fixed Scott's TFL bug on tc-extraction for higher order combinators like pair_cmp.

Make new Datatype definition function available in bossLib

export derived new_specification from bossLib

Implement new suffices_by tactic in BasicProvers and bossLib.

Closes #116.

Add IN_UNION to list_ss; handles set(l1 ++ l2) being rewritten.

This is progress with #52.

Add IN_INSERT and NOT_IN_EMPTY to list_ss.

This allows simplification of MEM terms to work in all circumstances. For example, if the term is

MEM x (FRONT [y])

the simplification works like

x IN set (FRONT [y])
^^^^^^^^^^^^^^^^^^^^

--> x IN set (FRONT [y])
^^^^^^^^^^^^^^^

--> x IN set (FRONT [y])
^^^^^^^^^

--> x IN set []
^^

--> x IN set []
^^^^^^

--> x IN EMPTY

and the simplifier's theorem for MEM x [] (= x IN set []) never gets to fire.

This is progress with #52.

define cheat tactic for unfinished proofs

expose PairCases_on in bossLib

Add zDefine -- this is a version of Define that doesn't add definitions to
computeLib.the_compset. Supports using derived theorems for evaluation.

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.

Add xHol_reln, allowing user to specify 'stem', by analogy with xDefine.

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

Implement congruence-based controls for rewriting with the simplifier,
to make it easier to rewrite only on the left or right of a top-level
relational symbol. (Strictly, this effect persists recursively down
into a term; I don't think this is likely to be an issue, particularly
with equality, which I think is the major use-case.)

Now there is an alternative to

CONV_TAC (LAND_CONV (SIMP_CONV std_ss [...]))

(writing the above has become practically automatic for me, but I
can't help but wince if forced to show it to a new user).

Instead, try

SIMP_TAC std_ss [..., SimpLHS]

assuming the top-level operator is indeed an equality. If it's not an
equality, use

SimpL ``op``

instead. Will write documentation tomorrow.

Demonstrate use, often in conjunction with Once, in arithmeticScript.

Additions to multiset and primeFactor
theories. Fixed definition of PRIMES
sequence in dividesTheory. Also added misc.
theorems to arithmetic. Some amount of
meaningless shuffling about.

Several changes in order to start making emitML a
bit more usable.

1. pred_setLib is now loaded by bossLib.

2. Many applications of emitML will just use
the "standard" background provided by the
ML code generated from the theories available
when bossLib is loaded: bools, funs, pairs,
sums, nums, lists, and sets. To access these,
you don't have to do anything other than just
load and/or open "emitLib". To load other
pre-built emitML support for theories like
words, bags, etc. which are not loaded by
bossLib, you have to explicitly load the relevant
"emit" theories, e.g.

words_emitTheory

3. src/emit/theories has now been lifted into
src/emit. So EmitML, emitLib, and all the
basic x_emitScript.sml stuff lives in the
same directory. This was just because I
didn't bother to figure out how (or if) it
is possible to compile part of emit then
enter and compile all of emit/theories,
then return and compile the rest of emit
which depends on the theories. If that
scenario is possible with the right Holmakefile,
then possibly the previous directory structure
should be restored.

4. The dependency of EmitML on integers has been
eliminated. So examples/ordinalScript.sml
builds again.

5. The reference cell EmitML.reshape_thm_hook can
be used to stick standard pre-processing for
theorems.

Attempt to tidy up (fix) EmitML and finish off the transition that Scott
started. EmitML has been moved to the end of the build sequence. "Hooks"
have been eliminated and all EmitML related stuff has been removed from the
various theory directories. All code for generating ML/Caml is now
self-contained within src/emit. I've not tested the generated Caml code but
the SML seems to build fine.

The directories:

src/theoryML
src/theoryOcaml
src/emitScript

have been replaced by

src/emit/theories/ML
src/emit/theories/Caml
src/emit/theories

Update to EmitTeX. Some functions have been renamed and some help entries
have been added.

EmitTeX is no longer included in bossLib and is instead loaded using
end-init-boss.sml.

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.

Moved EmitML code to a new directory src/emit.

Added a new structure EmitTeX. This allows HOL theories to be printed
as LaTeX source.

Added both of these structures to help/src/Keepers.sml

Added entrypoint for tDefine, version of Define that takes a tactic
to prove termination.

Change to the inductive relations definition code to support a global, and
updated "monoset", which can be updated as theories load, thereby invisibly
increasing the capabilities of Hol_reln. Also simplify the implementation
of derive_strong_induction, and move the entrypoint to IndDefLib. New
test in src/IndDef/selftest.sml wouldn't have passed before (I believe).
It is more onerous than Peter's original monoset example, which didn't
feature recursion under the EVERY operator. Documented in Description and
release notes. Still to update theories with appropriate calls to
export_mono. (export_mono and export_rewrites are now part of bossLib's
interface.)

Upgrading Define so that it proves more termination goals.
Generates lex. combinations and tries them out, so gets
some more ordinary recursions. Gets all iterated primitive
recursions. Also has been taught about some operations
on words (so recursion from w to w-1w will terminate,
for example).

Let me know of any bugs/slowdowns, etc.

Add more aggressive normalisation of multiplicative expressions to ARITH_ss.
Also provide old_arith_ss values for scripts that don't want this new
behaviour. Update proofs to go through again. Some should be a bit more
robust in the face of future changes to arith_ss. Others just punt and refer
to old_arith_ss.

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.

arith_ss can now be built by just adding the decision procedure to
std_ss (as the rewrites are already there).

Moved a whole bunch of "obvious" arithmetic rewrites into std_ss.
This simpset already does arithmetic on ground terms (2 + 3 = 5, sort of
thing), and it seems silly to have it not prove 0 <= x, and other simple
things like this. The change does break some proofs, which I have fixed.

These systems purport to provide multiple logical decision procedures, but
under the hood, they're really all the same.

Finally added METIS_TAC and METIS_PROVE to bossLib. Consequently,
they will be available by default.

More big re-org consequences.

Numerous minor changes associated with various things, most having
to do with exporting ML.

Fixes for a couple of infelicities:

* bool_ss didn't ever treat LETs (why?), so my incompatibility blurb wasn't
accurate. I had messed with the behaviour of PAIR_ss though, and this
was unnecessary. The new arrangement of things changes only the
behaviour of the srw_ss.

* Yesterday's solution for computing with lets would allow a subsitutiion
to occur even before the argument to the let had been simplified.
The new scheme uses a congruence rule to evaluate the sub-expressions,
and after doing so, wraps the value in an I tag. Then the various
LET_{foo,bar,baz} theorems can fire and cause a substitution to occur.
The presence of the I encodes "I have been looked at by the simplifier".

I want this because I want to have tags that indicate likely "value-hood"
such that a whole expression can be substituted at once, but I don't
want to not get a chance to simplify that expression first. Imagine,
for example, that NUMERAL could occasionally occur wrapped around
expressions that weren't already values. Then the theorem
|- LET f (NUMERAL x) = f (NUMERAL x)
would cause the pending computation x to be distributed willy-nilly
around the body of f, potentially causing us to have to simplify it
multiple times.

In the new scheme, the theorem above isn't used. Instead we have
|- LET f (I (NUMERAL x)) = f (NUMERAL x)
and by requiring the presence of the I, the reduction won't happen
until the simplifier has looked at x. Now, this shouldn't happen with
numerals, but it might well happen with other tags I'm planning to use.

So there you go.

A new approach to handling LETs for the stateful rewriter. Introduces an
incompatibility in that bool_ss no longer rewrites LET f x to f x (std_ss
still does though). The new strategy is:

Don't put LET_THM into any of the simpsets, but rather
put in specialised versions of this that allow "values" to be
substituted into the body. Thus ``let v = e1 in e2`` will only reduce
to e2[e1/v] when e1 has been reduced to a proper value. Better,
allow partial substitution to happen when e1 has become partially
value-like. For example, if we get to

let v = SUC e in v + v

and e isn't necessarily evaluated, we can still move this to

let v = e in SUC v + SUC v

The rewrite for this is |- LET f (SUC e) = LET (\v. f (SUC v)) e
Comparable rewrites for constructors of any type are easy to state
and prove. Arguably, these theorems should be generated when new
types are defined, and stored in the TypeBase. Because I know Konrad
will be (is already?) messing with the TypeBase to support ML lifting,
I haven't done this for Hol_datatype (it's not quite so easy to see
how to capture the notion of "record value").

I have written the appropriate theorems for the obivous built-in
types. This strategy gives the simplifier a notion of "value" that
is different from "can't reduce any more by the given rewrites"
(which is what CBV_CONV uses). The problem with CBV_CONV, or a
congruence rule that always performs the reduction from LET f e to
f e is that you can get big explosions in term size, which is
particularly bad if you are doing symbolic evaluation.

Have fixed problems arising in probability (which was using its own
version of std_ss, and those places where srw_ss() is being used. The
examples/lambda directory uses SRW_TAC pretty extensively, so there are
fixes required there. The easiest way is to just put LET_THM back into
the stateful simpset and to forget about it. The general problem with
the stateful system as it stands is that it is very easy to put things
into it, but impossible to pull them out. Isabelle has some way of
doing this that might be worth looking into.

Make sure all the relevant ML structures load with bossLib.

Make sure that various xSyntax structures are loaded by bossLib.

Support for rewriting annotations.

Added COMBIN_ss to std_ss. This will break proofs in prob until Joe
fixes them. (I love this; responsibility free check-ins :-)

The dependency hack in bitsScript.sml is moved to bossLib.sml.
Also extended to cover changes to optionTheory.

Modify TypeBases so that they can store conversions as well as theorems
in a tyinfo's "simpls_of" slot. This is then used to implement a conversion
for enumerated type equalities. Previously, we just used a rewrite
directly, which meant that something of the form (x = C10) might turn
into the rather ugly (foo_to_num x = 11). Now, the rewrite is only
applied to equalities between constants.
Some comments in the .sig files in Datatype, RecordType and EnumType
hopefully also make it clearer what the weird string results are
doing, and how they get added into theory files.

Moved CASE_TAC, an intelligent case-splitting tactic, to SingleStep,
and made it visible in bossLib.

Cause standard simpset fragments to be automatically added to the
stateful rewriter as the relevant theories are loaded, rather than
waiting for bossLib to come and along and do it after the fact.
Strictly speaking, in the case of numSimps and pairSimps it is still
necessary to load these two rather than just the base theories. This
is because the simpset fragments in these cases are more than just
rewrites but include 'real code' (REDUCE_CONV and GEN_BETA_CONV
respectively). Still, rather this than having to load bossLib.

Fix for bug #585828.

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.

Overlay.sml now exports infix declarations for the "standard" infixes,
taken from std.prelude. This means that the infix component of the
standard Script boilerplate is unnecessary. Updated Manual documentation
to reflect this. Changed combinScript and examples/ind_def/clScript.sml
just to show that it worked.

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.

Modified to directly export more of the simplifier's interface.

Made srw_ss and augment_srw_ss visible in bossLib.

Minor changes.

Fix needed given changes to names of list simpset fragements.

Changing arithLib to numLib.

New SRW_TAC tactic (stateful RW_TAC) implemented.

Modified definition of std_ss to include REDUCE_ss. Also made it
explicitly depend on sumSimps.SUM_ss, which didn't exist when the definition
was first made (I guess).

Modifications caused by change of TypeBase signature.

Revised type of EVAL to be a conv.

Added new "on" forward proof thingie to SingleStep. It's more primitive
than "by" because it allows the user to pick the thm_tactic that gets
applied to the goal after it's proved (by forces STRIP_ASSUME_TAC).
Also modified arith_ss to include REDUCE_ss to do arithmetic calculation
as part of the simpset.

Adapting to underlying changes.

New work aimed at making a single global EVAL function, with
an underlying compset.

Added mutual datatypes to those handled by Induct. Also added
Hol_reln to top-level interface. Will probably incoporate that
into Define.

Upgrade to DECIDE and DECIDE_TAC: now tautologies are handled.

Preliminary upgrade to work in Kan. 0.

Deleted ind_suffix and def_suffix.

Deleted inclusion of standard congruences for higher order recursion
on lists. These are now included when listTheory is loaded.

Slight changes to follow removal of Tfl structure.

Eliminated the "Context" structure from tflLib; instead, use
the "Tfl" structure, which now contains the functions from Context.

Uhh.

Modified definition of std_ss to use new OPTION_ss value rather than it
construct it itself.

Removed the ugly boolean of add_thms and from_list.
Use lazyfy_thm or strictify_thm instead.
Modified examples accordingly.

added initial_rws

The standard basic simplification set is now called "std_ss". I also
made "bool_ss" not be part of bossLib (to avoid confusion). Since
bossLib brings in a quite rich theory structure, there doesn't seem to
be any need for bool_ss to be there as well as std_ss.

General re-organization to push down functionality from bossLib into
lower depths of system.

New entrypoint `recInduct' for applying recursion induction. I have to
think about the name for this, since it can just as well be used
for just about any induction theorem.

Many changes, having to do with getting a proper interface for
proving termination.

test.Define is a big list of examples of function definitions.

bossLib has been broken up into simpler components that require less
resources to load induvidually.

BasicProvers provides PROVE_TAC and RW_TAC (loads in bool+combin)
QuotedDef provides a high-level definition interface
SingleStep provides high-level interactive proof steps
(for case analysis, induction, etc.) Another point about
SingleStep is that its operations use quotations and
this enables the use of the context (the current goal, typically)
in order to constrain the types of free variables in the quotation.

Preprocessing of Define improved in case where it deals with an
antiquotation.

Revision to PROVE, PROVE_TAC, and ZAP_TAC: boolean conditionals are
blown away by expanding with boolTheory.COND_EXPAND. This allows more
proofs to go through (MESON doesn't handle conditionals well).

Upgrade to bossLib.Define.

Halts.{sig,sml} : Moved to tflLib

bossLib.{sig,sml} :

primDefine is gone, replaced by Hol_fun, which is more powerful
and more robust. It returns something of type "defn", which is a
type declared in tfl/src/Defn.sml.

Changes to Define. It now handles a wider class of functions,
(mutual and nested recursions and schemas (which may be mutual and/or
nested)) and is more robust.

Define ` ... ` operates as follows:

1. It creates a bindstem for the definition to be made.
2. It makes the definition, using Hol_fun.
3. It attempts to prove termination. If this fails, then
Define fails.
4. Otherwise, if the definition is not recursive or is
primitive recursive, the defining equations alone are returned.
5. Else, the definition is not a trivial recursion, and the
following steps are made:

5a. The induction theorem is stored under bindname_ind
5b. The recursion equations are stored under bindname

Then the recursion equations are returned to the user.

Since Define generates names to store definitions and induction theorems
under, it (currently) exhibits bizarre behaviour with functions
with non-alphanumeric names. This will be fixed. In the meantime, use
Hol_fun.

Define also does the wrong thing with schematic definitions; again,
use Hol_fun.

Modified PROVE_TAC to rewrite out restricted forall and exists, making
it "Do the Right Thing" where theorems and goals using those quantifiers
are about.

Changes to accomodate new look portableML.

Corrected addition of sum size function to TypeBase.

Updated to add a size function to sum type in TypeBase.

Cosmetic changes.

Added error message for when Induct_on is attempted on something with
variable type.

Fixed to bring it up to date with Taupo release 0.
(Changes have come across from parse_branch development.)

Fix so that loading bossLib doesn't result in "inventing new type
variables" message.

Moved size functions for option datatype from option --- option doesn't
know about numbers, so have to do in bossLib.

Initial revision