Present IndDefLib's rule-induction-map as a theorem-set with ancestry

Only required change to the underlying API is to acknowledge that a
call to merge may result in no value if none of the desired parents
have a value either.

Complete implementation of smarter Induct_on

This massages a goal to pull out a negative occurrence of a inductive
relation term, replacing compound terms with variables and
generalising appropriately to make the goal suitable for a subsequent
call to ho_match_mp_tac (which is done inside Induct_on).

Not sure yet quite what should be done with mutually recursive
relations and Induct_on.

Closes #244

Start with test-cases for isolation of induction terms

Work on github issue #244

Fix sigs to share co-mmon funs

Inductive definitions now make their core definitions with provided stem name.

Rule-induction theorem map needs to be on Name-Thy pairs, not terms directly.

This is because of polymorphic constants.

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

Automatically store 'strong' induction principles in theories.

The plan is to have Induct_on use these to perform rule inductions as well
as data type inductions.

Make IndDefLib's monotonicity result store use generic theory data.

Improve error reporting for Hol_reln by making common errors (and
messages) be accompanied by location information.

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

Committing in fixes to bugs in literals in pattern matching discovered by
Michael Norrish.

Also committing in changes to the IndDef library, changing the names
of two functions from "prim_..." to "..._mono_...".

Modified Files:
hol98/src/IndDef/IndDefLib.sig hol98/src/IndDef/IndDefLib.sml
hol98/src/IndDef/IndDefRules.sig
hol98/src/IndDef/IndDefRules.sml hol98/src/bool/Pmatch.sml
hol98/src/tfl/src/Functional.sml
----------------------------------------------------------------------

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

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

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

Relatively minor changes in order to enable definitions to be made
from stages later in the parsing process than mere quotations. (In
particular, wanted this to enable definitions from Absyn values.)

Nearly finished with IndDefLib. Added the ability to reload
definitions (bunch of Absyn hacking). Finalized the names
and locations of various entrypoints.

Ongoing changes to merge jrh and tfm ind. def. libs.

Merge of jrh and tfm packages. The stuff from jrh will be used to
define the predicates and derive the rules, induction, and cases
theorems. The stuff from tfm will provide proof support. I hope
that this will be a fairly innocuous change, but I'm still in
the process of getting old examples to build.

Added RULE_INDUCT_TAC to signature.

Added derivation of strong induction.

Upgrade to work in Kananaskis 0.

Type in signature wasn't correct.

Need to add BACKCHAIN_TAC to signature, in order to build monoset
additions.

Generalized new_inductive_definition so that it takes a monoset as
an argument.

Revealed a function from the implementation that needs to be visible for
John's inductive datatype package to work properly.

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

Initial revision