Update for newer version of base, and fix proof

The fix is due to pat_assum-rename. Now open bossLib directly rather than
lcsymtacs, since the latter doesn't include qpat_x_assum.

Bump version on hol-base (and base)

Also, get rid of the hol-base-unsat package: it can be done via articles
only without installing a dummy package.

Add MONO_IMP to hol-base

Export a helper function in Opentheory

The function tweaks the theorems produced by define_new_type_bijections
to match the (closed) format introduced with article version 6.

Remove Unicode from bool_defs and prove_base_assums

Add restricted quantifiers to hol-base

Add bool_case_thm to prove_base_assums

Add BOOL_EQ_DISTINCT to prove_base_assumsTheory

Add more bool theorems to hol-base

Most prominently, add itself and the_value.

The changes to the interpretation in the bool section of
hol4-base-sat.thy are to ensure TYPE_DEFINITION and its definition get
interpreted correctly, since they are now used... I still get confused
about this interpretation stuff...

Use OpenTheory's Data.List.unzip for hol-base

We currently cannot similarly use Data.List.zip to replace list.ZIP
because one is curried and the other is not.

Add more theorems from boolTheory to hol-base

These don't appear as assumptions when building hol-base, but may be
used in later HOL theories. Unfortunately this seems to require the
bool-defs thing to be also done in hol4-base-sat.thy.

Tidy names and authors of OpenTheory packages

The opentheory tool is pretty strict about what it accepts.

Make the ARB definition more innocuous

Use gen_new_specification to avoid introducing an equality, and also
export a theorem mentioning the constant (ARB = ARB) to ensure the
definition gets picked up by OpenTheory.

Add definition of ARB

To avoid an ungrounded external constant. Perhaps it would be better to
define it via prim_new_specification, to avoid exporting an unnecessary
equality.

Prove hol4-base assumptions related to bool constants

The trick (since it is impractical to log boolTheory) is to provide a
fake boolTheory that just makes the definitions of the problematic
constants (and proves some characteristic theorems) and use that where a
logged boolTheory would have been.

Now all assumptions are proved.

Do not target OpenTheory's PRE and $-

We need to define the HOL4 versions of these, because they are more
specified than the OpenTheory versions. (Under appropriate assumptions,
they are equal though.)

Stop pretending ARB and LET are in OpenTheory base

Prove more hol4-base assumptions

There are now 13 left, and they all appear to require changes to the
setup. Some are to do with constants that are more specified in HOL than
OT (such as PRE and arithmetic$-). The rest are mostly to do with
boolTheory, which has not been recorded, and includes things like
TYPE_DEFINITION.

Prove more hol4-base assumtions.

Down to 33. The remainder seem to be problematic
TYPE_DEFINITION/DATATYPE stuff, hopefully ok constant definitions, and
definitely problematic constant definitions.

Prove more hol4-base assumptions

There was a problem with IMP_ANTISYM_AX being a dependency of various
derived rules. The proof of th23 needed to be careful to avoid that. New
implementation of EQF_INTRO does that too. Down to 58 assumptions.

Prove more hol4-base assumptions

Down to 64 unsatisfied assumptions.

Prove more hol4-base assumptions

Prove more hol4-base assumptions

Reimplemented some simple derived rules (EQF_INTRO, etc.) using the new
theorems, to avoid introducing extra unwanted assumptions.

Down to 92 unsatisfied assumptions (started at 120).

Prove more hol4-base assumptions

The expected count of assumptions proved in the resulting package is now
correct.

Start work on proving hol4-base assumptions

Currently, however, it does not seem that the assumptions are actually
getting proven (the number of satisfied assumptions is going up, but the
number of unsatisfied assumptions is not changing). Will need to
investigate further.