Make selftest output line up with parallel Holmake's

Also make tests use testutils.OK to report OK

Detect and abort on vacuous inductive relation clauses

A vacuous clause is something like

!x y. R x y

where R is the relation being defined. Such a thing makes the relation
the universal relation. If you really want such a thing, you can always
write

!x y. T ==> R x y

Closes #269

Prevent bad constant names at Definition level

Enforces a constraint I'd long assumed to be true.

Closes #268

add MONO_COND to bool_monoset (and hence the_monoset)

This enables inductive definitions that make recursive calls in the
branches of conditionals expressed with COND (if_then_else).
Also added a selftest.

Move IndDef earlier in the build sequence (just before BasicProof).

This will let me reinstate my new Induct_on functionality.

Make IndDefLib lose its unnecessary dependency on arithmeticTheory.

Its selftest then needs to fake an arithmetic theory in order to get some of
its test-cases to look similar to what they used to be.

Delete a misplaced comment.

Bug fix, with test-case and release notes write-up.

Remove some unnecessary fluff from the selftest script, and also make
it executable in an interactive session without it causing the session to
exit on hitting an error.

A new bug - strong induction derivation doesn't work for definitions with
only a single rule.

IndDefLib fails this example because a term arises of the form
UNCURRY f x y, which does not match the conclusion of the UNCURRY
monotonicity rule. As the range of UNCURRY is polymorphic (rather than
bool), it's impossible to tell how many arguments UNCURRY will be
applied to before the resulting term is boolean. This suggests that the
implementation of monotonicity proving needs to change to special-case
UNCURRY, just as lambda is special-cased.

Check behaviour more consistently and more thoroughly.

A new bug, reported by Peter, where the Inductive definitions package
fails to do its stuff.

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

Fix output of selftest slightly; adjust its dependencies in Holmakefile.

This example causes grief to a new way of implementing back-chaining that
I am investigating.

----------------------------------------------------------------------

Committing in fix so that a fresh build of HOL4 works.
A recent addition caused a build to break since lists, etc. were not
built before this library.

Modified Files:
selftest.sml
----------------------------------------------------------------------

----------------------------------------------------------------------

Committing in slight tuneups to rule inductive definitions.

Modified Files:
IndDefRules.sml selftest.sml
----------------------------------------------------------------------

----------------------------------------------------------------------

Committing in revisions to rule induction library, supporting the
proof of strong induction theorems for rules that involve new
monotonic operators. There is now a new function,
prim_derive_strong_induction, available in IndDefLib.

Modified Files:
IndDefLib.sig IndDefLib.sml IndDefRules.sig IndDefRules.sml
selftest.sml
----------------------------------------------------------------------

Add a test case that one might argue we should support. Currently, the
Hol_reln call is fine, but the call to derive_strong_induction fails.

Regression testing for inductive definitions.