removing one source of unbreakable looping behaviour in dep_rewrite

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.

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.

Include Abbrev in dep_rewrite

Before this fix this happened:

> rw [];
val it = fn: tactic

> open dep_rewrite;
[...]

> rw [];
val it = fn: bossLib.tactic

Remove eqtype declaration for term type

trailing newlines in *.{sml,sig} files from src/ removed

Trailing newlines from SML files in src/ were rendered in HTML documentation.

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