Fix bug in PAT_ASSUM when use of variables from goal is not respected

In particular, the old code gave itself licence to instantiate type
variables in patterns when those were associated with variables from
the goal, thereby allowing it to pick completely different
assumptions that didn't even include the quoted variable. The test
case illustrates.

Where a proof breaks (as in io_onestepTheory), the fix is to remove
the use of goal-variables of the wrong type, perhaps replacing them
with underscores.

Improve propagation of error messages out of goal_assum

Implement machinery to check that tactic results change acceptably

Used to implement checks that h.o. redexes don't remain, or have
decreased in count.

This is progress towards implementation of github issue #680.

Provide more information in exceptions raised by Tactical.VALID

Correct typo in comment

Another go at strengthening the (default) behaviour of Tactical.prove.

By default Tactical.prove now checks for the validity of the supplied tactic using VALID. This breaks a few proofs in which assumptions were surreptitiously being introduced.

It is expected that this commit will break some external proofs that relied on the old behaviour (e.g. under CakeML). A workaround is to selectively restore the old behaviour with

val () = set_prover (fn (t, tac) => TAC_PROOF (([], t), tac))

in places that contain non-valid tactic proofs.

Print a message when "prove" introduces hypotheses.

Revert "Add hypotheses count check to TAC_PROOF."

This reverts commit 01930d56ce7a31c10ff7f422a0cf535a8c502a59.

I don't believe that changing this primitive is a good idea. I'd like
TAC_PROOF to stay as the base primitive that applies a tactic to a
goal state without checking for validity or similar.

This change is also causing breakages in CakeML and
examples/machine-code/lisp. If there is a need for this sort of
validity-style check (apart from what is done by expand), it could be
added to prove quite reasonably, possibly there under the control of
another trace variable, or just permanently on (as it is easy enough
to change the behaviour of prove by adjusting the reference it
consults).

Add hypotheses count check to TAC_PROOF.

This helps guard against the following:

val lem = Q.prove(
`F`,
ACCEPT_TAC (ASSUME ``F``)
)

Before this returned the theorem [F] |-> F without complaint, despite an "Invalid tactic" exception being raised when using proofManagerLib.e. This proof will now fail. The new check falls short of requiring alpha equivalence of assumption lists, which would be safer.

This change has identified a few areas of imprecision within automation, namely within "dep_rewrite" and "Satisfy". There it may be the case that a subset of the stated assumptions appear in the final theorem.

Fixes for mp_then/drule bug found in previous commit

Provide more test-cases as well. Extend normalisation done by
goal_assum after a theorem is returned to it after "resolution".

Remove TABs in some source code, replacing them with spaces

Use Emacs's conception of how many spaces the TAB was
representing (and the M-x untabify command).

This may not line up with the author's original conception, but then,
using TABs makes it impossible to tell just what the original
conception was in the first place anyway.

Should probably script this over all of repository (excluding
makefiles of course), and use standard expand or col utilities rather
than emacs.

Remove eqtype declaration for term type

Implement line-number reporting for failing THEN1/>-

This relies on a somewhat disgusting quotation filter hack which
replaces occurrences of >-/THEN1 in line with the following pattern:

tac1 >- tac2 - - - > tac1 >>- linenumber ?? tac2

This relies on >>- and ?? being left-associative, which is how they
are defined. The definition of ?? is

fun f ?? x = f x

The linenumber is inserted by the quotation filter, which tracks this
naturally.

Provide access to more switches when parsing in context

In particular, allow setting of Feedback traces which will be used
when parsing of quotations occurs.

This allows Q.PAT_ASSUM to be made quiet about inventing type
variables. This is deemed desirable in github issue #425. (I'm not
100% sure now of this, but hey.)

Closes #425

Use cache Absyn to speed up QTY_TAC

Addressing github issue #383

Modify Q_TAC to try all possible parses

This makes a difference in the presence of overloads. Modify
implementations of Q.SPEC_THEN and Q.SPECL_THEN to use QTY_TAC (making
them simpler), and check that they seem to behave as desired with some
test-cases.

Fix pat_assum problem caused by use of H.O. match

As per the comment in Tactical.sml, ho_match_term is too clever at
times.

Provide "typed" parsing-in-context entry-points

This allows

QTY_TAC ty tac q

to parse q in the context of the goal and also require the resulting
term to have the provided type. The resulting term is then passed to
tac, as per Q_TAC>

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.

Fix build errors prompted by goal_assum

Implement goal_assum

Like first_assum, but uses the negation of the goal.

Fix HDTM_{X_,}ASSUM implementation

can (same_const t) is the same as fn _ => true, and so not at all
helpful.

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.

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.

Move some tactics from lcsymtacs to Tactic{,al}

As per Github issue #274

Move lcsymtacs functions to natural homes

For example, we do not need to have >> in lcsymtacs; it might as be in
Tactical. The ultimate aim is to do away with lcsymtacs entirely.

This is work towards github issue #274

Delete trailing whitespace

new irule, order of new subgoals is consistent,

regardless of how the substitution may change the internal
order of hypothesis in the argument theorem

also new tactical ADD_SGS_TAC - like VALIDATE
but new terms to be proved need to be specified

fix construction of error value in NTH_GOAL

trivial change to comment in source file

purpose is to trigger another attempt at buiding on github

fix garbled comment in source code

only the comment is changed

Move useful apnth function to Lib

Also make it raise a HOL_ERR rather than a Bind error if the index is
negative or greater than the length of the list.

Remove trailing whitespace in Tactical.sml

Remove non-exhaustive match warning by slight code rewrite

new list-tactic USE_SG_THEN

makes one subgoal available in the proof of another

relaxing type constraint for THEN and THENL

to permit
val THEN : list_tactic * tactic -> list_tactic
val THENL : list_tactic * tactic list -> list_tactic
as well as the usual types

GEN_VALIDATE(_LT) - flag for adding new subgoals in any event

GEN_VALIDATE false is like VALIDATE, but adds subgoals for the assumptions
of the theorem produced by the justification, regardless of whether they
are among the assumptions of the goal. Advantage of this is that
GEN_VALIDATE false (ACCEPT_TAC th) produces predictable subgoals,
which may help in coding compound tactics

VALIDATE and VALIDATE_LT

If tac (ltac) is invalid due to proving theorems with extra assumptions,
VALIDATE tac and VALIDATE_LT ltac make the tactic valid by returning extra
subgoals to prove the extra assumptions

expand_list to interactively work on a list of subgoals

also Tactical.VALID_LT, to check that a list-tactical is valid
(expand_list checks validity, expand_listf doesn't)

also abbreviations elt, eall, eta, enth to apply (list-)tactic to subgoal(s)

Delete trailing whitespace in src/

This needs doing periodically, and is best done to a whole bunch of files
at once.

replacing code for THEN and THENL using ALLGOALS and TACS_TO_LT

also defines NULL_OK_LT to implement change to THENL
(see https://github.com/HOL-Theorem-Prover/HOL/issues/214 )

some new doc files to do with list_tactics

list_tactic concept

introduce list_tactic - works on a list of goals, not a single goal
THEN_LT (tac1, ltac2 : list_tactic),
A tactical that applies ltac2 to the list of subgoals resulting from tac1
TACS_TO_LT (tac2l: tactic list) : list_tactic
ALLGOALS - A list_tactic which applies a given tactic to all goals
ALL_LT - always succeeds
NTH_GOAL - applies tactic to nth goal of list
REVERSE_LT - A list_tactic that reverses a list of subgoals
SPLIT_LT - apply two list-tactics, one to first n subgoals,
the other to the rest
ROTATE_LT - rotate the list of subgoals by n positions

Add LAST_ASSUM and LAST_X_ASSUM tactics

like first_assum and first_x_assum, but work from the other end of the
assumption list

Provide more feedback when proofs fail.

Tidy up some code under src/1. See commit ad9b041.

Change src/bool to src/1 as a prelude to experimentation!