Merged hol-light's cardTheory (rich_cardinalTheory) with HOL4's cardinalTheory

Don't export ERR from HolKernel

Prove two simple results about isPREFIX (x <<= y)

More complicated results about this constant are ending up in
rich_list.

Define SHORTLEX lexicographic ordering over lists

Unlike the traditional dictionary order, this one is a wellorder if
the order over the elements is wellfounded.

Remove TABs from src

Will also make selftest to check that they aren't introduced

Provide machinery for declaring/exporting monad information

Declare options, lists, state-transformers (bad name!) and
errorStateMonads as monads. For the moment, this infrastructure is not
used, but next step will be to link it into the parsing and printing
machinery.

Re-implement Datatype package with TypeBase sexps (not adjoin)

Fix multi-line list forms (incl. records)

Prove two simple theorems about OLEAST (one becomes automatic)

The automatic rewrite is

|- ((OLEAST) P = NONE) <=> !n. ~P n

This breaks a proof in listScript, that does become simpler thanks to
these theorems now being available.

Add some theorems from CakeML

pred_set: to do with bijections and surjections
list: MAP2 and LIST_REL results
pair: rewrites with (FST x = y) and (SND x = y) as LHSs

other changes are fixes for broken proofs.

Add oHD and oEL (option-valued) functions from CakeML

oEL was called LLOOKUP in CakeML but I don't much like that name.

Add congruence rule for OPT_MMAP

From Thomas Tuerk, see #491

Added TeX_notation for "++" in listTheory

Define ZIP with all cases specified

The new definition is called ZIP_def. The old definition has the same
old name, i.e. ZIP.

Closes #463

Moved UNIQUE_FILTER and UNIQUE_LENGTH_FILTER to listTheory

Uniqueness of list elements (UNIQUE) and 3 alternative definitions

Remove -- as an alias for Term parser.

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

Provide a Unicode ++ symbol for APPEND

Happy to revert this if people hate the look of it - this is mostly an
experiment.

Switch order of listform/::-as-infix declarations in listScript

This ensures that list-forms are preferred when possible.

Previously the preference for list-forms was hard-coded into the
pretty-printing code; now the most recent rule is preferred. Of
course, if you write “h::t” that's how it will be printed, as the
listform rule doesn't apply.

Move list thms from multiword to list

Get core HOL to build with new definition of "by"

Progress with github issue #407

Add INJ_MAP_EQ_IFF to listTheory from CakeML's miscTheory

Fix inaccurate comment about dependencies at head of list script

Add monadic map for the option monad (OPT_MMAP) to listScript

With type

(α → β option) → α list → α list option

it maps the function over the list, and if any element maps to NONE,
the overall result is NONE. Otherwise, it's SOME of the list of all
the "successful" results that appeared under the SOMEs.

Fix proofs in listTheory for LENGTH_NIL rewrites

Make LENGTH_NIL rewrites automatic

As requested in issue #346.

Tweak automatic rewrites for TAKE and DROP

The previous rewrites introduce COND (if), which is often undesirable.
The new rewrites are more constrained but desirable in more contexts.

See https://sourceforge.net/p/hol/mailman/message/35184168/

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.

Fix listLib.FLAT_CONV

Include some tests.

Closes #358

listTheory.CARD_LIST_TO_SET_ALL_DISTINCT

Fix pre-boss theories in light of pat_assum renaming

Strengthen statement of TAKE_SUM

Also tidy up listScript, removing a big local-in-end that made bit
cut-and-pastes painful. (If you put your point down in the middle of a
local-in-end, and do a cut-and-paste, you will get an syntax error.) For
this many theorems at once, better just to export the local declarations
to the top-level and deal with the consequent changes.

One theorem needed to have its proof adjusted.

Closes #330.

Add new useful rewrite theorems (in list theory)

In particular:

EL_APPEND_EQN :
EL n (l1 ++ l2) = if n < LENGTH l1 then EL n l1
else EL (n - LENGTH l1) l2
LAST_MAP
l <> [] ==> (LAST (MAP f l) = f (LAST l))

Make the latter an automatic rewrite. EL_APPEND_EQN is then used to
simplify proofs of EL_APPEND1 and EL_APPEND2 in rich_listTheory.

From Joseph Chan.

Add various theorems from CakeML

Add Theory.quote_adjoin_to_theory. Use this in llistTheory.

This should close #304.

This has been implemented using a new function Portable.quote_to_string_list. Other uses of adjoin_to_theory under src/ have been updated.

Delete *_tuple constants after they have been used.

This one line change seems to address issue #99.

Improve logging of listTheory, axiomatise construction

Preivously, the construction via ind_type was leaking out via an
induction theorem in TypeBase that was never saved. The fix is to save
it (list_INDUCT0) and then use the otd file to delete its proof.

It would probably be possible to delete the binding at some point in
export_theory, to prevent it actually occurring in the final exported
theory, but that may not be worth the trouble.

Remove some duplicates of the theorem TRUTH.

These are:
• INFINITE_DEF and IN_LIST_TO_SET (replaced with overloadings)
• IN_APP_applied and IN_ABS_applied (inadvertently generated)

Also, made changes to try to avoid new definitions in listTheory accidentally having a "_DEF" suffix instead of "_def". Old naming inconsistencies still remain in listTheory (e.g. EXISTS_DEF, FIND_def and FLAT).

These changes will break a few proofs but patches should be trivial (i.e. removing references to these TRUTH theorems and/ or renaming "_DEF" to "_def").

Remove Unicode under src/

add some more OpenTheory names to listTheory

also alphabetise the list.

list$EL cannot be mapped to Data.List.nth directly because it takes its
arguments in the other order.

Clean src/ to remove Unicode (or to mark it as OK)

Marking Unicode as OK is done by putting the UOK tag on the same line of
the relevant file.

move some theorems from lprefix_lub into src

miscellaneous fixes

LLEX_CONG not LEX_CONG, also delete some trailing whitespace

cong for llex (closes #219)

add LLEX_MONO (this and 191963d related to #219)

Rewrites about terms of form ``MAP f t1 = t2``

When t2 is involves a standard list function (CONS, APPEND etc), there
are useful possible rhses. When t2 = [x], the rewrite seems
sufficiently useful to warrant making the rewrite automatic.

Moved from grammarTheory in examples/parsing

Move 2 open declarations to head of listScript.sml

more list theorems

from CakeML

mark some theorems as automatic rewrites

selection taken from CakeML

Change API of Q's MATCH...RENAME_TACs.

Now rather than a string list hanging off the end specifying which
variable bindings aren't supposed to induce a renaming, just put
underscores into the pattern in those positions.

Documentation and release notes updated.

Remove some Unicode in src/

Attempt to tidy-up some proof scripts. Much of this has come from CakeML.

Removed Unicode and tried to eliminate lines longer than 80 characters.

Also added a few new constants to listTheory: INDEX_FIND, FIND and INDEX_OF.

Added "nub" to listSyntax.

add new dropWhile constant to listTheory, and various lemmas

Improve nub_set lemma

As suggested by Michael Norrish

move theorems out of finite_mapTheory into (rich)_listTheory

they have nothing to do with finite maps

Added CakeML list theorems to listScript.sml

Added a new function, nub, which removes all duplicates.

I'm not sure how to decide what goes in list and in rich_list, so I put
everything in list that I could. That is, everything but theorems about
rich_list only constants and theorems whose proofs depend on rich_list
theorems.

Fix order of the existentially quantified vars in list_nchotomy thm.

This makes the theorem conform to the pattern used by types in the
TypeBase. This theorem is stated explicitly here to override the
datatype package's choice of variable names, which make a difference
when you use Cases_on or Cases.

Define the "dictionary order" for lists.

Some properties also, including the fact that it isn't usually
wellfounded.

Get LIST_APPLY to use <*> syntax via APPLICATIVE_FAPPLY name.

Make listTheory's (short-lived) SINGL constant an overload to ``\x. [x]``

It's nice to have SINGL to hand as an abbreviation for the above
abstraction (particularly as writing the abstraction will usually
require enclosing parentheses, lifting the character count to 9,
compared to SINGL's 5). But one doesn't want to see SINGL 3, when [3]
is so much nicer.

Use the new feature "ignore-for-printing" feature of overload_on (see
ac4806d), so this happens. Somewhat sadly, this does mean that
although one can write MAP SINGL l, one will get back MAP (\x. [x]) l.

Implement "ignore overloads for printing" feature.

Demonstrate with change to list, so that ``~MEM a l`` prints that way
rather than as ``a NOTIN set l``. Selftest checks this, and also that
``x NOTIN {2;3;4}`` continues to print the right way.

Closes #95.

List monad related definitions (mimicking what's in option)

Also adding the "apply" operator, which is the analogue of what on
options would be

APPLY (SOME f) (SOME x) = SOME (f x)
APPLY _ _ = NONE

Prove some relevant theorems.

Move export_rewrites of MAP and FLAT earlier in listScript.

Syntax support for PAD_LEFT and PAD_RIGHT.

Revert to using LENGTH instead of LEN

Based on some performance experiments done by Anthony.
This partially reverts aeb5670.

add tail-recursive SUM for EVAL, and use the tail-rec LENGTH

this modifies list_compset, and what is added to the_compset by
listTheory. LEN appeared to have been defined but not used.

Minor lemmas about TAKE, DROP and splitAtPki.

Some new useful theorems from CakeML work.

Define a general “split at first element satisfying P” function on lists.

Perhaps unnecessarily generic in its use of predicates that also get
the indexes of the element and taking a continuation, but the index
argument to the predicate can be ignored with K, and to return a pair
you just need to pass $, so that

splitAtPki (K P) $,

is a function that returns the pair of lists where the first element
of the second list satisfies P unless there is no such in all of the
list, in which case the second list will be empty.

add various more constants to OpenTheoryMap

Make EVERY2 an alias for the LIST_REL constant.

Preserve the EVERY2 theorems, at least for the moment.

This issue was first identified in discussion around github issue #98

Fix lists in world of flipped arguments for case constants.

Things like using lazyfy of list_case_compute in EVAL are probably now wrong.

Define and case-parsing are generating the right code for the new form
of case constant. Pretty-printing is not working correctly yet.

Progress with github issue #97.

add some more OpenTheory names to the map

Move rich_listTheory.FLAT_APPEND to listTheory; make it an automatic rewrite.

Keep a SML-level alias in rich_listTheory.

FLAT_APPEND says |- FLAT (l1 ++ l2) = FLAT l1 ++ FLAT l2

Adjust way LIST_TO_SET is defined so it can go into emitted listML

Manually delete {EVERY2,MAP2,FOLDL2}_tupled constants from listTheory.

See #98 (clean up listTheory) and #99 (automatically delete unneeded
_tupled constants).

Delete unused listRel constant from listTheory.

It’s identical to LIST_REL, which *is* used in a variety of places.
Retain listRel as an overloading for LIST_REL just in case someone
ever used that name. LIST_REL stays as the preferred printing form.

Make listTheory.IN_LIST_TO_SET a trivial rwt for backwards compatibility.

Its old statement was

x IN set l <=> MEM x l

but that is now an instance of reflexivity given MEM's overloading.

Build all of src/list/src and up to integer_word. See #52.

listSyntax loses mem_tm, but retains a mk_mem and a dest_mem that do
the obvious thing.

Get listTheory to build in features/mem-abbrev branch. See #52.

Start of work to replace MEM with λx l. x ∈ set l. See #52.

Theorem characterising NULL (FILTER P ls)

Theorem characterising (SUM ls = 0)

REPLACE_ELEMENT --> LUPDATE

Thomas showed me that REPLACE_ELEMENT is the same as LUPDATE. In this
commit, I moved REPLACE_ELEMENT from rich_listTheory to listTheory and
rename it LUPDATE -- deleting the old definition of LUPDATE. I also
updated examples/machine-code which uses LUPDATE.

Minor tweaks to list compset.

LUPDATE added to listTheory

move some theorems about DROP and LIST_REL into listTheory

Change EVAL behaviour for TAKE and DROP.

Following check-in 994d485, rich_listTheory no longer adds compute theorems for TAKE and DROP to the_compset (they were added by the Define in listTheory). Before that check-in

EVAL ``DROP 0 x``;
EVAL ``TAKE 0 x``;

would give

|- DROP 0 x = x
|- TAKE 0 x = []

when rich_listTheory was loaded. However, after that check-in these terms would remain unchanged. This check-in ensures that the former behaviour is restored.

Overhaul to rich_listTheory (it had become a bit of a disaster area).

Some points:

1. rich_listTheory now uses the same constant names that are used in listTheory, e.g. TAKE instead of FIRSTN.

2. listTheory theorems are no longer replicated (saved again) in rich_listTheory. This avoids DB.match returning multiple instances of the same theorem. It also avoids saving around 100 theorems twice — in some cases after re-proving them.

3. Compatibility is now maintained though a bunch of SML "val" assignments added using adjoin_to_theory, e.g.

val ZIP_FIRSTN_LEQ = ZIP_TAKE_LEQ
val ALL_DISTINCT_SNOC = listTheory.ALL_DISTINCT_SNOC

4. Some incompatibilities are introduced:

* FRONT___LENGTH is deleted, since it is the same as rich_listTheory.LENGTH_FRONT.
* COUNT_LIST___ADD -> COUNT_LIST_ADD
* COUNT_LIST___COUNT -> COUNT_LIST_COUNT
* The compute theorems for COUNT_LIST and SPLITP have been renamed.
* Some other theorems are no longer saved, e.g. rich_listTheory.list_INDUCT

5. Some theorems in listTheory have gained quantifiers.

Revert "make patricia play nice..."

This reverts commit da47401d5163b28a320790e7acca897d8374880c.
Reason: qualified names in the list of add_persistent_funs exports are
supposed to work.
See comments on #73.
The reason why they probably weren't working before is that you need to
use a name like:
"pred_set.FINITE_EMPTY"
not
"pred_setTheory.FINITE_EMPTY"

Conflicts:
src/list/src/listScript.sml
src/patricia/patriciaScript.sml
src/patricia/patricia_castsScript.sml
src/pred_set/src/pred_setScript.sml

(Conflicts all due to change in add_persistent_funs interface.)

change interface to add_persistent_funs (#73) and fix more calls

The new interface takes a list of strings naming theorems.
(The old interface took a list of (string * thm) pairs.)
The new way better ensures consistency of theory development and theory
load behaviour: you can no longer pass a name with a theorem that isn't
actually saved under it.

Theorems are looked up with DB.theorem, or failing that, DB.definition
or DB.axiom.

Alas, I found more examples using add_persistent_funs to add theorems in
ancestor theories. Rather than modify the ancestor theories, I have
opted to make the offending theories save the theorems they want to add
to computeLib themselves so they have a name in the current theory to
pass to add_persistent_funs.

If this behavior was appropriate for patricia too (da47401) change it.
Alternatively, if the ancestor theories should have exported those
things for computeLib anyway, search this commit for new instances of
"save_thm" to see what needs fixing.

make patricia play nice with new add_persistent_funs (#73)

Some theories in src/patricia were calling add_persistent_funs for
definitions from other theories (list and pred_set) and using the
arbitrary code string to refer to those theorems with fully qualified
names.

The fix adopted here is to call add_persistent_funs for those constants
in the theories where they are defined.

add more automatic rewrites to listTheory

in particular LENGTH_ZIP, and other stuff involving ZIP and UNZIP

theorem about FOLDR of a function that does CONS

(this generalises rich_listTheory.FOLDR_CONS_NIL)

theorem: MAP preserves injectivity

Maybe the statement/name should match my commit summary better?

Also, proved a simple lemma about replacing the set arguments to INJ
with super/subsets.

theorem: ALL_DISTINCT (MAP f ls) ==> ALL_DISTINCT ls

rewrites for MAP/FOLDLing a list ZIPped with itself

theorems relating FOLDL2/EVERY2 back to FOLDL/EVERY

also, export FOLDL2_def as a rewrite, and provide an alias ("MAP2_MAP")
for the analogous theorem (also called "MAP2_ZIP") for MAP2.

theorems validating computation of BIGUNION by FOLDL of UNION

new theorems about SORTED

The most interesting concludes that two lists are equal if they are both
sorted and are permutations of each other. Another characterises SORTED
R ls as !m n. m < n ==> R (EL m ls) (EL n ls).

Some "ListPair" functions: FOLDL2 and EVERY2

totalize MAP2 and export a congruence theorem for it

and use it in the miniml compiler

theorem about SUM of MAP

Support list_compset evaluation of TAKE, DROP, PAD_LEFT, PAD_RIGHT and isPREFIX. Also make evaluation of REVERSE more efficient.

New results about "splitting" lists up with append.

Also prove SNOC's injectivity, and make more of SNOC's rewrites
automatic.

Remove unnecessary reference to prim_recTheory.PRIM_REC_THM.

I'm tempted to simplify prim_recTheory; its internal PRIM_REC and SIMP_REC constants
aren't really necessary for the proof of num_Axiom, and they're not used externally.

Some more theorems about LIST_REL.

LIST_REL_MAP1 uses composition and allows for anything in the R
position.
LIST_REL_MAP2 requires an abstraction in the R position and so can
directly apply the f to an abstracted variable. There is a version of
this that looks like

LIST_REL R l1 (MAP f l2) = LIST_REL (combin$C ($o $o R) f) l1 l2

and this can be made to do the right thing when R is an abstraction
with subsequent rewrites from combinTheory, but it looks so confusing
that I thought we might as well restrict it to the case when R is
already an abstraction.

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

Adopt ML-style syntax for case expressions and use freed up "||" for bitwise-or. See issue #24.

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

Minor tweaks to evaluation.

Terms and labelled terms now derived from generic terms.

This is a big change that points to the implementation of a complete
nominal datatype package. The use of generic terms means that we only
need to do one hairy quotient, and one hairy derivation of a recursion
principle.

The recursion principle in question features a new "FCB" (one of the
side-conditions that need to be proved in order to get a recursive
function admitted). Though I think it's better, it can be a little
fiddlier to prove. It's also stronger, so in theory, there may be
reasonable functions that the new FCB rejects. It should certainly be
possible to automate the bulk of the new fiddly proofs.

Rename TruePrefix to Prefix; use fixity options with NONE for what was Prefix.

90+% of this work was done by Ramana Kumar. The following list are
the commits for a series of individual commits that have been squished
into one big change:
* remove mention of TruePrefix from the add_rule docfile
* first batch of changes removing TruePrefix from src/parse
* replace TruePrefix by Prefix in boolScript.sml
* remove TruePrefix from Rsyntax
is a fixity ever required for new_specification?
* some more Prefix -> NONE and TruePrefix -> Prefix in theories
* TruePrefix changes for datatype
* TruePrefix changes for res_quan
* TruePrefix->Prefix in a TeX selftest
* TruePrefix changes for quotient
* TruePrefix changes for integer and real
* fix quotient examples for TruePrefix removal
* more fixes for quotient examples
* fixes for lambda example for TruePrefix removal
* Reword description manual in light of removal of TruePrefix.
* Fix msgTheory quotient example; Poly 5.3 had problems with monotypes.
* Fixes for files in examples/lambda given removal of TruePrefix.
* Fix in examples/unification given removal of TruePrefix.
* Fix in examples/HolCheck given removal of TruePrefix.
* Fixes in examples/acl2 given removal of TruePrefix.

Some extra list theorems.

Remove some Unicode that has crept into scripts.

Move PAD_LEFT and PAD_RIGHT from stringTheory to listTheory.

Also, patch up emit scripts following GENLIST moving from rich_list to
listTheory.

Prove and export thm that SET_TO_LIST {} = [].

Add an OpenTheoryMap analogous to TexTokenMap

Also, add names for various type operators and constants in boolTheory,
listTheory, and numTheory so that the Opentheory selftests now pass without
having to set up those name mappings themselves.

Theorem about adding items in chunks of equal size

That is, SIGMA f (count (k * n)) = SIGMA g (count n), where g adds
k-sized chunks of f.

Also moved SUM_APPEND to listTheory.

New theorem REVERSE_GENLIST, and moved EL_REVERSE to listTheory

Used DECIDE_TAC at the end of EL_REVERSE's proof instead of also
moving another lemma from rich_listTheory.

Restore support for evaluation of GENLIST, which was broken by recent changes.

Couple of equivalences about GENLIST

In particular MEM and ALL_DISTINCT on GENLISTs.
Proof of the latter is messy - probably can be done better.

Moved another SNOC theorem to listTheory.

Couple of theorems about SUM (MAP f l)

Also moved 2 requirements from rich_list to list

Move SNOC_INDUCT and SNOC_CASES into listTheory

Prove ITSET is indeed a fold-like operation

New theorem relating LIST_TO_SET and FILTER.

Move LIST_REL from quotient_list to list, and make it more polymorphic.

The extra polymorphism makes LIST_REL usable in inductive definitions, as
I have done in the generic_terms example. It doesn't interfere with the
use made of it in the quotient library.

Two theorems about SUM of lists.

Put GENLIST computation with numerals back into automatic simpset.

This broke one proof of Anthony's that didn't want
GENLIST f 16
expanded (for good reason). Fixed it by abbreviating the 16 into a
variable.

Fixes and tweaks following check-in 8434 (GENLIST moving to listTheory).

Moved GENLIST from rich_list to list.
Also moved some theorems about SNOC and about MAP.

Give isPREFIX symbols TeX equivalents.

src/num/theories/SingleStep.{sig,sml} is gone. The
defininitions of Cases, Cases_on, Induct, Induct_on,
CASE_TAC (and co.) are now in basicProof/BasicProvers.
completeInduct_on and measureInduct_on are now in
numLib. recInduct is now in src/tfl/Induction.sml.
All these are collected in bossLib, so the changes
should be invisible to ordinary users.

SingleStep.*.doc has been changed accordingly.

BasicProvers.NORM_TAC should now automatically perform
all case splits (from if-then-else expressions as
well as case expression) arising anywhere in the goal.

INFINITE is now an abbreviation for ``\s. ~FINITE s``.

Prove some results about the finite-ness or otherwise of some universal sets.

Modications to simpsets and compsets for lists with respect to the evaluation of EL.
This requiered some minor additions to listTheory. I used the change to add some more simple rewrites and definition that I use in my separationLogic example.

As discussed on the HOL-developers mailing list (18 March 2010, 3:33 pm, "Simpsets and compsets for lists / evaluation of EL"), I had
trouble with the standard compsets and EL. If applied to a term "EL n l" where "n" was not a ground term these compsets diverged.
That is changed now. For ground terms the evaluation should behave the same, for non-ground ones it will now terminate.

The simpsets terminated, but evaluated EL as long as possible. For example
``EL 5 (x1::x2::xs)`` got converted to "|- EL 5 (x1::x2::xs) = HD (TL (TL (TL xs)))".
That has been changed and now the result is "|- EL 5 (x1::x2::xs) = EL 3 xs".

The main additional definition I added is "LIST_COUNT" to rich_listTheory.
``LIST_COUNT n`` evaluates to the list [0;1;...;(n-1)].

Added a couple of theorems about ALL_DISTINCT of a ZIP to listTheory.

Added LIST_TO_SET_SNOC to listTheory.

Move Thomas' list_eq_simp_ss to listSimps and make it automatic.

This requires the movement of SNOC and some theorems from rich_list to list.
Making the simpset fragment automatic may break proofs by solving more than
expected.

Add evaluation support for FCP index and update. This has required fixing
a problem with the evaluation of EL, namely EVAL ``EL i x`` didn't terminate.

Add automatic, obvious rewrites about REVERSE to listTheory.

* Make duplicates in rich_list just point to listTheory
* Minor change to a proof in patricia_casts also required.

New constant LRC which is like NRC but records the list of nodes in the path between two nodes linked by the transitive closure of a binary relation, rather than just the number of steps

removed utf-8 from my last commit

some theorems about LIST_TO_BAG and LIST_TO_SET

Add a new theorem |- (LIST_TO_SET l = {}) <=> (l = [])

Actually add a version of this to cover the lhs's equality the other
way 'round. Make this an automatic rewrite. Clean-up some proofs
about ALL_DISTINCT, and reorder things to put LIST_TO_SET and
SET_TO_LIST stuff together.

Two theorems about lists suggested by Ramana Kumar.

Add a couple of theorems about LAST, inspired by a suggestion from Ramana Kumar.

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!

Theorem MEMBER_NOT_NIL is renamed to NOT_NULL_MEM and it's syntax is slightly changed, because it did not fit into the naming schema.

Remove some theorems that Thomas added to listTheory.

Also added TRAVERSE_AUX which is now used to evaluate TRAVERSE and KEYS.

theorems by Anthony Fox and Thomas Tuerk added

Attempt to tidy up (fix) EmitML and finish off the transition that Scott
started. EmitML has been moved to the end of the build sequence. "Hooks"
have been eliminated and all EmitML related stuff has been removed from the
various theory directories. All code for generating ML/Caml is now
self-contained within src/emit. I've not tested the generated Caml code but
the SML seems to build fine.

The directories:

src/theoryML
src/theoryOcaml
src/emitScript

have been replaced by

src/emit/theories/ML
src/emit/theories/Caml
src/emit/theories

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.

Create an isPREFIX constant in listTheory, and subsequently:
* use <<= as an infix version of isPREFIX, with Unicode version the
LaTeX symbol \preceq (U+227C)
* map rich_listTheory's IS_PREFIX to be the same, but with the
arguments reversed (i.e., IS_PREFIX -> \x y. isPREFIX y x). Take
care to make rich_listTheory.IS_PREFIX look exactly the same as
before in terms of variable names, universal quantification etc
* map stringTheory's isPREFIX to just be listTheory's.

Next steps:
* move across some of rich_listTheory's theorems about isPREFIX to be
in listTheory
* maybe move across IS_SUFFIX, perhaps once I've figured out what the
order of the arguments should be, and what the infix operator should
look like

Fairly dramatic change, supporting the use of "syntactic patterns".
It is now possible to overload a name to term (typically a
lambda-abstraction) in order to create syntax-only definitions. For
example, there is a definition of not-equals now in the system:
val _ = overload_on ("<>", ``\x y. ~(x = y)``)
val _ = set_fixity "<>" (Infix(NONASSOC, 450))
This definition is parsed and pretty-printed.

Two other annoying changes. The interface for adding unicode variants
has changed, and I have made precedence level 450 of the parser
non-associative. This latter change has caused most of the (minor)
adjustments to the files below. The regression test doesn't go
through yet. (Currently there is a failure in
quotient/examples/sigma that I don't understand.)

Change export_rewrites back to its old API (without requiring an extra
string). When exported, the resulting simpset fragment always picked
up the name of the theory to be the base of its name, so there didn't
seem much point in giving users a false impression of naming power.

A whole mess of small changes intended
at making simpsets prettyprint informatively
in the interactive loop. Very possibly
I haven't updated all the files in the examples
directories.

Add a proof of (REVERSE l = []) = (l = []) (also already proved in
rich_listTheory), and make it an automatic rewrite with srw_ss().

Move pred_set to be earlier in the build sequence, making it an
ancestor of listTheory, and available in bossLib. The various
LIST_TO_SET and SET_TO_LIST theorems are now available in listTheory.
Also introduce the set abbreviation for LIST_TO_SET that I've found
very useful. Documented in release notes as an incompatibility.
Incidentally reckon containerTheory might be something we could do
away with entirely.

* Add TAKE and DROP constants to listTheory, along with a few simple theorems
about them
* Make FIRSTN and BUTFIRSTN in rich_listTheory aliases for the above,
though the constants are now more defined than they were
* Preserve theorem forms in rich_listTheory
* Preserve FIRSTN_CONV and BUTFIRSTN_CONV behaviours (adding selftest too)

Prove a tfl-congruence theorem for OPTION_MAP so that recursion can
happen underneath it OK and give plausible termination requirements.
Also provide an additional "export" interface for adding to the
DefnBase. This saves having to write adjoin_to_sml code in Script
files. Use this new style for OPTION_MAP and the congruence rules in
listTheory.

(We now have three databases of this form (monotonicity results for
inductive relations, simplification rewrites, congruences for tfl);
there may be an elegant generalisation possible...)

These extra monotonicity results should help get more inductive definitions
made.

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 change to the interface of derive_strong_induction hits these scripts -
the fix makes the call easier to make.

Changes having to do with generating ML. System should build again.

Want to make this part of the InductiveDefinitions package (which will
need to be told that listRel is monotone). Currently the default interface
there uses a fixed monotonicity set, rather than one that can be updated
with new monotonic constants like this one.

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.

Extend the add_listform interface so that the user can specify a printing
"consistency" for the block of list elements. Previously, it was just
assumed that the user always wanted (INCONSISTENT,0). This is the value
now specified in the various places where add_listform is used.

Changed the TypeBase to be indexed by types. Originally it was
indexed by a single string (representing the type operator), then
Michael changed it to a pair of strings (precise representation
of the type operator). The latest change allows non-datatypes to
be added to the TypeBase. This will allow case analysis and
termination proofs to be supported for non-datatypes.

I reckon there are still a few bugs left after the massive
revision, so you might want to wait a while before upgrading.

Wide-ranging change to make the TypeBase export an interface forcing users
to be concerned about which theory their types are from. Interactive users
of the "induction_of", "axiom_of" and similar functions are thrown the only
bone: they can effectively omit the theory parameter by using "" instead
of a theory name.
Prompted by a bug found by Tom Ridge where it was impossible to define
a pattern matching function on a type with the same name as another type
because the pattern-matching code was using dest_type and TypeBase.read
on just the type-operator name.

Add simplifier-safe treatment of EL (and use this in lbtreeScript).

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.

Had the wrong name.

Added equality versions of induction theorems. Sometimes this can
let you do induction proofs by rewriting. For example,

!L1 L2. LENGTH (L1 ++ L2) = LENGTH L1 + LENGTH L2

can be proved by RW_TAC list_ss [FORALL_LIST]. But just as
often it doesn't do the right thing ...

Alter the fixity information for ++ so that it is looser than ::
Thus, the theorem for APPEND becomes h::t ++ l = h::(t ++ l)
rather than (h::t) ++ l = h::t ++ l
where the RHS of the latter is quite misleading.
Also fix fixedPointTheory to be compatible with all this.

Small changes.

Per Michael's suggestion, "++" is now infix for APPEND. Let me know
if that causes problems.

VS: Committing in .

Added tail-recursive versions of REVERSE and LENGTH. Neglected, however,
to add them into various simplification sets ...

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

*** empty log message ***

Ignore this ... I'm just using CVS to transfer files from home to
work.

Added a bit of FAIL-related theorem proving. More still to be
added here for things like FRONT, LAST, MAP2, and ZIP.

Minor changes.

Some useful lemmas.

Misc. tweakery.

Upgrades to ML code generation. It now works for numerals, although
the results of a computation will be incomprehensible usually. Writing
a prettyprinter needs to be done.

Export ML from list theory.

Add EXISTS_DEF to the set of things automatically expanded by srw_ss().
(EVERY_DEF is already there.)

Move LIST_TO_SET into listTheory from containerTheory as part of my general
campaign to move set "things" as early as possible into the build sequence.
Also add various theorems about lists and bags.

Added LAST to the functions known to EVAL.

This theorem had been missed out as a useful rewriting export.

Sorry! I've realised that there's a better way of doing what I want
within the netsem code-base, and that I don't need to make any changes
to the way HOL currently does things. More, that letting HOL stay
just the way it was is probably better. So, this change is to put the
code I meddled with over the last couple of days back the way it was
originally. (Minor exceptions include changes to comments, elimination
of unnecessary infix declarations, and revealing a PAIR0_ss that is
equal to PAIR_ss minus LET_ss.)

A new approach to handling LETs for the stateful rewriter. Introduces an
incompatibility in that bool_ss no longer rewrites LET f x to f x (std_ss
still does though). The new strategy is:

Don't put LET_THM into any of the simpsets, but rather
put in specialised versions of this that allow "values" to be
substituted into the body. Thus ``let v = e1 in e2`` will only reduce
to e2[e1/v] when e1 has been reduced to a proper value. Better,
allow partial substitution to happen when e1 has become partially
value-like. For example, if we get to

let v = SUC e in v + v

and e isn't necessarily evaluated, we can still move this to

let v = e in SUC v + SUC v

The rewrite for this is |- LET f (SUC e) = LET (\v. f (SUC v)) e
Comparable rewrites for constructors of any type are easy to state
and prove. Arguably, these theorems should be generated when new
types are defined, and stored in the TypeBase. Because I know Konrad
will be (is already?) messing with the TypeBase to support ML lifting,
I haven't done this for Hol_datatype (it's not quite so easy to see
how to capture the notion of "record value").

I have written the appropriate theorems for the obivous built-in
types. This strategy gives the simplifier a notion of "value" that
is different from "can't reduce any more by the given rewrites"
(which is what CBV_CONV uses). The problem with CBV_CONV, or a
congruence rule that always performs the reduction from LET f e to
f e is that you can get big explosions in term size, which is
particularly bad if you are doing symbolic evaluation.

Have fixed problems arising in probability (which was using its own
version of std_ss, and those places where srw_ss() is being used. The
examples/lambda directory uses SRW_TAC pretty extensively, so there are
fixes required there. The easiest way is to just put LET_THM back into
the stateful simpset and to forget about it. The general problem with
the stateful system as it stands is that it is very easy to put things
into it, but impossible to pull them out. Isabelle has some way of
doing this that might be worth looking into.

Modify the add_listform function in line with a suggestion of Lockwood
Morris's to provide slightly more flexibility in the way that list forms
are pretty-printed. Previously, the format was fixed as
<left-delimiter> el1 <sep> <a space> el2 <sep> <a space> ...
Now, the spacing is more directly under user-control.

Support for ML evaluation of HOL terms. Preliminary.

Many small changes, most associated with boolification or lifting.

Change to type of new_specification, and made it tell that parser about
the introduced constants. Lots of knock-on (trivial) mods.

Add ALL_DISTINCT to those functions that automatically added to the global
evaluator (EVAL).

Forgot to include ALL_DISTINCT in the exported automatic updates.

For a long time I believed that any wish to have a predicate ALL_DISTINCT
for lists was a sure indication that the user was foolishly using lists
rather than sets. But no, my work on finite maps has found me a situation
where I really do need to use this notion (with FUPDATE_LIST, it's
important, for one result I want, to know that the list of key-value pairs
doesn't contain any duplicated keys: i.e., ALL_DISTINCT (MAP FST kvl)).
Note use of two new features: (=) x rather than $=, and the call
to METIS_TAC. Joe will be pleased to know that MESON_TAC can't do it, but
METIS can. All hail METIS.

A couple of additions to the stateful rewriter: I got thoroughly sick of
having to write combinTheory.o_THM, and was also surprised to see that
FILTER P (h::t) wasn't being dealt with automatically (though it does
introduce a case-split).

Added some trivial theorems about EXISTS and EVERY and exported some of
them too.

Added definitions of FOLDL and FOLDR to list_ss (and related simpsets).

I'd missed a couple of theorems in transcribing the list from listSimps.sml

Exported some SRW rewrites, using the theorems that go into
listSimps.LIST_ss. In fact, made listSimps.LIST_ss just refer back
to listTheory.list_rwts.

Added a trivial theorem about MEM and APPEND.

Change stemming from split of TypeBase into TypeBasePure and TypeBase.

Changing arithLib to numLib.

Added FRONT and LAST to listTheory. These constants are also available
in rich_list; but there FRONT becomes aliased with BUTLAST.

Made the :: operator a little tighter binding, taking it out of the domain
of "logical operators" and into the weak arithmetic area (<=, etc).

Changes to add REVERSE to the automatic tools.

Moved REVERSE from rich_list to list.

Modifications caused by change of TypeBase signature.

Not sure what this was.

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

Upgraded to build in Kan. 0.

Made directory Kananaskis compatible; added listSyntax library.

Improved pretty-printing for :: (cons) by allowing a break to come
after it.

Added APPEND_11 theorem.

A couple more theorems for listTheory (EVERY_APPEND and EXISTS_APPEND).
Also put these into the standard simpset. Put entries for ZIP and UNZIP
into rich_list to preserve some modicum of backwards compatibility. Of
course, these will be theorems now rather than definitions, but who's
going to notice?

Moved ZIP and UNZIP into listTheory. Proved a bunch of theorems about
them and also EVERY and EXISTS.

Minor change.

Added standard congruences for higher order recursion
on lists to things that Tfl knows about.

Now that the datatype axioms produced by the datatype package are more
reasonable in their choice of type variable names, the proof of
list_Axiom_old is slightly simplified.

Changes due to the incorporation of John Harrison's datatype definition
package.

New additions to listSimps, to track all the relevant definitions
made in listScript.

added list_rws to work with computeLib

Movement of some of the more useful list functions (FOLDL,FOLDR, EXISTS,MEM)
from rich_list to list. Also, proved congruence theorems for higher-order
functions (supports bossLib.Define).

ConstrProofs has been moved to Prim_rec given my development of alternatives
for prove_constructors_distinct and prove_constructors_one_one that don't
need numbers or pairs.

ConstrProofs.sml : changed ZERO to 0

listScript.sml : added a proof that the predecessor relation
on lists is wellfounded.

Updates for new pretty-printing support.

Changes necessary to make :: an infix operator representing CONS as well
as the restricted quantification operator. This change has required some
changes to the basic design of the parser; it's now not possible to have
more than one res. quan. operator.

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

Initial revision