Add flip as an alias for combin$C

Add some extra automatic rewrites to do with function update

Also make sure that rewrites in COMBIN_ss are named so that they can
be excluded from simplification tactics if necessary.

Make equality of "tight" precedence by default

Start to work through knock-on effects of this.

Pretty-print the new fn-update syntax (e.g., f⦇k ↦ v; x ↦ y⦈)

With a selftest.

This is the function half of github issue #616.

Finite maps still to come.

First steps towards parsing f ⦇ d1 ↦ r1; d2 ↦ r2 ⦈ for fn. UPDATE

The ASCII version of the same is f (| d1 |-> r1; d2 |-> r2 |) and of
course, the old (d1 =+ r1) ((d2 =+ r2) f) can also be used.

The pick of ⦇ ... ⦈ precludes using the same parentheses for
s-expressions in the example of the same name (hence the changes in
that example). The use of (| |) means that (||) no longer parses as
paren-escaping the || operator (hence the change to wordsScript.sml).

Pretty-printing still to be done.

Fix for (new, pretty branch) bug causing computeLib failures with K

Move smpp to Portable - get everything up to arithmeticScript working

Up to core types

Remove -- as an alias for Term parser.

As per comment in release notes this has long been replaced as
appropriate style.

Remove "C" from combinTheory.combin_grammars

Currently, combinTheory is set up to hide C from the global grammar when
it is loaded, but to leave C in combinTheory's own grammar, which you
get via writing things like combinTheory.combin_grammars. This is weird.
To make things more consistent, pull C out of combin's grammar
properly (without having to use adjoin_to_sml), and have it absent in
both descendants, and in combin_grammars.

Of course, the standard trick of typing

reveal "C"

makes it visible again.

The code in src/metis/normalForms.sml used this visibility when stating
and proving a rewrite about C. This was fixed simply by making the
statement use the combin$C notation.

Merge operatorTheory into combinTheory

This was far too small a theory to live an independent existence. It
was included by listTheory so the constant name-space contamination
isn't any different for eventual clients.

Make U+2218 (∘) alternative syntax for combin$o

Also bind C-S-0 0 as Emacs keybinding to generate it.

update OpenTheory names for combinTheory constants

Make 'o' map to existing \HOLTokenCompose in TeX_notation map.

Closes #242

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

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

Add conversion updateLib.UPDATE_APPLY_CONV.

update OpenTheory names for combinators to new standard

Add new rewrite about abstractions and function composition.

This one parallels the existing o_ABS_R. To my surprise, the
simplifier currently preserves bound variable names when this rewrite is
applied, even though the two x's can well be of different types, and
thus different bound variables in a pretty strong sense.

For example,

SIMP_CONV (srw_ss()) [o_ABS_L] ``(\b. b /\ p) o FST``

gives back

|- (λb. b ∧ p) o FST = (λb. FST b ∧ p)

The b on the left is a boolean, the b on the right is a pair. This is
a bit odd, perhaps even a bug. When the types are the same this is
clearly the right thing, but still. The bug, if it is one, will be
in the implementation of HO_PART_MATCH.

Remove structure-struct/end bracketing from combinScript.sml.

add OpenTheory name for combin$K

add various names to the OpenTheory map

This is in preparation for logging llistTheory.

Notes:
- Sent combin$C to Function.Combinator.c (same for combin$S).
Another name might be preferred on the OpenTheory side.
- Not sure what bool$BOUNDED is about; dumped it in the HOL4 namespace.
- Put lots of pred_set constants in the Set namespace, but in the
standard (OpenTheory) library it seems like Set is for constants
operating on an abstract type of sets (rather than predicates). I'm
not sure whether we should use a different namespace when working with
sets-as-predicates or just pretend predicates are the abstract type
and do a bit of magic on article reading/writing as necessary (don't
know what that would be exactly yet).
- Similar for constants in set_relation, which I'm currently putting in
the Relation namespace. Although it looks like currently OpenTheory
doesn't use an abstract type of relations (but probably it will
later).
- Sent marker$Cong and marker$Abbrev to Unwanted.id, but not sure if
Unwanted.id is supposed to be polymorphic (whereas those are identity
functions restricted to bool). Similar for numeral$iZ
- sent GSPEC to Set.specification; maybe not an obvious name...
- Using top-level "While" namespace for whileTheory
- dumped numeral$iiSUC in HOL4 namespace; not sure what to do with it
- BIT2 is going to Number.Numeral.bit2; this is in line with wanting the
base library to be liberal, i.e. a union of all useful basic constants
and theorems (so has bit0, bit1 and bit2)... but I think there may be
competing goals for base

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

add OpenTheory name for combin$I

Add the useful |> combinator to combinTheory. Had to be ":>" because "|>"
is already used for records. If anyone doesn't like the name "APP" then
feel free to change it.

Removed trailing whitespace from all .sml and .sig files.

This affects over 900 files and was done using emacs's delete-trailing-whitespace
function in batch mode. Building the system with Poly/ML and Moscow ML seems to
work, so I'm hoping these changes don't break anything. Please complain if
they do!

Started moving EmitML code out of source scripts and into a single source
script "libraryScript.sml" in src/emitScript, adding calls to emitCAML
alongside the emitML calls in libraryScript.sml.

Replaced o_DEF with o_THM in "the_compset". This fixes a problem when
evaluating record updates (and it also provides consistency with srw_ss()).
For example:

EVAL ``<| f := r |> with f := x``;

produces

``<|f := x|>``

instead of

``<|f updated_by (\x'. x)|>``

At the behest of Konrad and Michael, SUBST is now called UPDATE.

Also, it has been moved into combinTheory (even though it is not
a combinator).

Unfortunately, the symbol ``:-`` has had to be abandoned because
this is used in labelTheory.

The new symbol is ``=+``.

Without the use of METIS, the theorems have been proved the long way.

The theorems are renamed to fall in line with the those of FUPDATE
from finite_mapTheory:

SUBST_EVAL -> APPLY_UPDATE_THM
SUBST_NE_COMMUTES -> UPDATE_COMMUTES
SUBST_EQ -> UPDATE_EQ

Also:

SUBST_IMP_ID -> UPDATE_APPLY_IMP_ID
SUBST_ID -> APPLY_UPDATE_ID

Some more theorems (again similar to those of FUPDATE) have been added:

UPDATE_APPLY_ID
UPD11_SAME_KEY_AND_BASE
UPD11_SAME_BASE
UPD_SAME_KEY_UNWIND
SAME_KEY_UPDATE_DIFFER

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

Committing in additional theorems to aid in SRW_TAC's use of the
new literal patterns. Bug found by Anthony Fox.

Modified Files:
combinScript.sml
----------------------------------------------------------------------

Another of my changes to the filter removed what I thought was unnecessary
code for handling the old-fashioned --`...`-- syntax for terms and types.
But it turns out this code is necessary if Parse isn't around. Easiest
fix: opening Parse.

Minor changes and bugfixes to ML code generation. Have renamed
EmitML.exportML to EmitML.emitML, since exportML is used in
SML/NJ to dump the image. Also renamed Globals.exportMLPath
to Globals.emitMLDir (since it's a directory and not a path).

Also fixed bug in code generated for constructors and tuples.

Revised exportML so that it takes a path parameter, which tells
where the ML corresponding to a theory is to be written.

This has been propagated to all the theories that already export
ML, and the mkword.exe tool has been upgraded to also take a
path where it should write the generated ML. This is useful,
because doing an exportML to the same directory as the theory
files will end up confusing Holmake.

ML code generation for finite_map now added. Also, a whole host
of minor changes and robustifications have been applied.

Added new combinator called FAIL, which is equal to K. FAIL is used
to generate exception-raising code when translated to ML. For
example

HD [] = FAIL HD ^(mk_var("Empty list",bool)) []

which is provable since FAIL x y = x. The translator to ML
will convert FAIL terms so that the above is

HD [] = raise Fail "HD: Empty list"

New entry point in BasicProvers called LET_ELIM_TAC to do lovely things
with lets, whether uncurried or not. They're lifted out of the goal
and turned into abbreviations into the assumptions. Plan is to tack
LET_ELIM_TAC into the basic action of RW_TAC and SRW_TAC as well.

Export ML from combin theory. The exported ML ends up in the
directory src/theoryML.

Many small changes, most associated with boolification or lifting.

Prove a cute little theorem about the K combinator. This is a necessary
prelude to one last change I'm contemplating to make record type
definition roughly twice as fast as it is at the moment. The change to
relationScript makes it explictly depend on combinTheory, something the
automatic dependency analysis can't figure out on its own.

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.

New work aimed at making a single global EVAL function, with
an underlying compset.

Minor changes.

Made sure that the combinator "C" is hidden by default. This will
prevent surprises in developments that already use "C" as a variable.
In principle I should do the same for "W" ...

Kananaskis compatibility; addition of C and W combinators.

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

Initial revision