Fix combinatory logic and parity examples

Finish tidying up combinator chapter in Tutorial

Documentation reflecting preference for Datatype over Hol_datatype.

Some code changes as well, most importantly in TUTORIAL's
examples/ind_def/clScript.sml.

define arithmetic$ZERO and redefine num$0 opentheory mapping

The main issue is that we want both of these constants to point to
Number.Numeral.zero, but the OpenTheoryMap assumes one-to-one mapping
situations. Another issue is that we want Number.Numeral.zero to point
back to num$0 but arithmetic$ZERO is defined later (and the map retains
the last insertion.)

Solution here is to insert num$0 again after arithmetic$ZERO.
Downside is that a warning is printed saying that a duplicate mapping is
being inserted (probably every time arithmeticTheory is loaded).

Upside is that clScript.sml is now completely unchanged (since before
experimentation with opentheory logging) but is still able to be logged
to an OpenTheory article, with reasonable defaults for all necessary
choices.

The warning could be removed by suppressing the warning when the new
mapping is to the same string, by special-casing zero somewhere
(probably OpenTheoryMap), or by implementing a real many-to-many (or
one-to-many) map situation (hardest).

hooks for logging names without global mappings

By default (i.e., after calling loggingBossLib.new_theory) hooks are set
up to translate a constant or type called thy$name, as long as thy is
the current theory, to the opentheory name ([thy],name).

Thus when logging a new theory, one does not have to set up any mappings
in the OpenTheoryMap explicitly. They can be put there, though, of
course, and the handler could be set to update the map as well as
returning a default name.

Using the new defaults, the names in the combinatory logic example are
all now in the "cl" namespace. To use different namespaces or to rename
certain constants (and to use "combinatoryLogicExample", which is not
the HOL4 theory name) would require a companion file specifying this
information.

better match intended semantics of OpenTheory names

rather than using strings, now have a type abbreviation otname for
string list * string. it might be worth writing more operations on this
type (like for manipulating the namespace).

Fix cl example for changes to Hol_datatype.

Also strip the "old" tags from constants if necessary when defining them
by specification. (The constant might already have been deleted by the
time the virtual machine is going to define it in terms of Hilbert
choice, but we need the constant and not just its name to construct the
alternative definition c = @x. <foo> so it matters whether the constant is
uptodate.)

Minor tweak to cl.thy; will now try uploading it to the gilith repo.

save all defined objects for reuse; pretend old names aren't

By saving the virtual machine's results after running definitional
commands, we avoid the problems with "provenance" when trying to get the
opentheory tool to read our generated articles. Basically, the deal is
you need to use the constant the virtual machine generates after making
a definition; you can't just build it from its name (because then it
would look like an input/assumed constant).

Also, since the "old" constants don't actually ever get defined (i.e.
they are only defined before they are deleted), I now just pretend they
are never deleted as far as logging is concerned. This involves some
hackery to strip the "old->...<-old" tags from the name of the constant
before storing it in the dictionary.

The opentheory tool finally reads our generated cl.art successfully and
can install the theory package. There are lots of warnings though, and
they come in two kinds: 1) the article doesn't leave the stack or
dictionary empty when it's done and 2) lots of article assumptions (i.e.
theorems it doesn't prove) have free variables in them.

Add --ot option to Holmake, create loggingBossLib

At the moment, all the --ot option does is add loggingBossLib.ui to the
environment before trying to build a theory.

A lot more could be done:
- don't assume loggingBossLib exists
- work on mosml too (only touched polyml's Holmake)
- work independently of whether the Theory.sml file already exists; know
you're making an .art file if given --ot and do dependencies correctly
- work with a (format as yet undetermined) companion file for the script
file that gives extra info like constant name mappings and
names/statements of theorems to export (as opposed to just everything
store_thm'd)

Move some OpenTheory_const_name calls into arithmeticScript.sml

My hesitation about arithmetic$ZERO is because the map is one-to-one and
num$0 is already mapped to Number.numeral.zero. Arguably, the article
writer could do some special-purpose renaming of ZERO by 0 before
attempting to log a theorem; or the name map could support multiple
translations.

seems better to ignore the "old" markers on certain ind_type constants

major reworking of treatment of definitions

Since an article needs to define things before it can use them, it is
nice to be able to log definitions in the order they happen in the
kernel. So I have added a generic definition_callback to Thm which is
called when definitions happen, and Logging installs a function that
collects definitional theorems. They can then be logged in order by a
call to log_definitions() right after the definition is made in the
script file being logged.

WIP trying to read logged cl.art back with article reader

allow for logging theorems without exporting them

In particular, this should be used for definitions (and type
definitions), because the machine reading the article will want to
define things before using them. Write a bit of documentation in
Logging.sig. Update clScript.sml accordingly (to log its definitions as
they are made).

two more constants in clScript need opentheory names

complete patch to clScript to record the proofs

continue attempt to log clTheory

WIP: trying to log clTheory, debugging info, rethinking logger

Revise TUTORIAL's CL example to illustrate new Induct_on technology.

Change ind_def example to illustrate use of xHol_reln and new Induct_on.

Add new set_mapped_fixity function to Parse (some documentation included).

Update the script corresponding to the Tutorial's combinatory logic
example so that the two match once more.

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

The interface to derive_strong_induction changed, forcing changes in these
calling sites.

Minor update to the combinatory logic example, removing the need to
extract theorems from the TypeBase.

Put this example back the way it was (symbolic identifiers had not
been invalidated by a proper change to Hol_datatype), if only to avoid
having to update the TUTORIAL chapter which accompanies this file.

Updated examples ... seems that Hol_datatype doesn't allow symbolic
identifiers anymore. Have changed datatype definitions to use
non-symbolic identifiers and re-introduced the symbols with
overload_on.

Changed STRIP_TAC means that some names automatically chosen by the
system are different. Some proofs break as a result. Fixed by more
aggressive use of automatic provers (PROVE_TAC).

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.

Get rid of DB.fetch calls in preference for calls to TypeBase functions.

Added to some README files,and some minor changes.

Making examples work.

Upgrading examples to match new stuff in system. The ind_def examples
are not yet fully integrated!

Hide the RTC constant that now lives in relationTheory from view.
Also set up ML names for the theorems now saved by the inductive
definition package.

Konrad pointed out that -||-> is a better symbol than ===>. The latter
looks too much like implication.

New version of proof of combinatory logic confluence.

Minor changes to deal with new datatype package.

Minor changes.

Changes to accomodate parser upgrade.

Initial revision