Fixes of bag, container, finite_map and in n-bit/

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.

Reformat finite_mapTheory ; add some theorems from CakeML.

Reformatting includes
- indentation changes
- removal of TABs

Improve statement of o_f_FUPDATE

This theorem does not need to use the \\ operator (i.e., there is an
instance of fm \\ k on the theorem's RHS that can be replaced by fm).

Adjust fixities of finite map composition operators

Add associativity result for f_o (f/map-function composition)

Assume injectivity of the two functions involved as this seems a
reasonable common case.

Fix one of the bugs in previous commit's test-case

This was done by simply removing the entry-points (uoverload_on, and
uset_fixity) that were causing problems. They have long been redundant
in terms of their desired effect, and introduced buggy behaviour with
the switch to explicit grammar deltas.

The uoverload_on function is still used internally.

Remove Unicode under src/

This problem is now being spotted by self-testing again, thanks to
c529f76

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 finite-map theories in light of pat_assum rename

Add various theorems from CakeML

Opening lcsymtacs is no longer necessary.

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.

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 sorting/perm theorems to finite_maps and alists

This makes the finite_map directory depend on the sorting directory.

move theorems out of finite_mapTheory into (rich)_listTheory

they have nothing to do with finite maps

New theorems about finite maps and alists

Importing theorems that were useful in CakeML (https://cakeml.org).
Mostly by Ramana Kumar, some by Scott Owens.

Also removed the unnecessary ALL_DISTINCE assumption from
ALOOKUP_TABULATE.

Add domain restriction and deletion to relations (reusing \\ syntax).

a couple of small theorems about FUPDATE_LIST

The first is essentially combines the definition of FUPDATE_LIST as a
fold with rich_list's theorem about folding a mapped list.

The second simplifies fm |++ SNOC x xs.

Some more theorems about fmap_rel.

move thm that FUNION is idempotent to finite_mapTheory

Move fmap_rel (analogous to LIST_REL) to finite_mapTheory

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.

Remove some trailing whitespace.

Added size functions for finite sets, maps, and bags.

These are helpful for measures supporting recursive definitions and
induction schemes. The size functions have been added to the TypeBase,
with the intent that Induct, Induct_on, Cases, and Cases_on should be
applicable. (However, this has not been checked yet, so these might
not work.)

The size of a finite set is the number of elements in it, plus the
sizes of all the elements. (The size of a set with 0 as an element is
larger than that set with the zero deleted.)

The size of a finite map is the number of mapped elements, plus the
sizes of the mapped elements. Key size is ignored.

The size of a finite multiset is the number of elements in the
multiset plus the sizes of the elements. There are more extensive
orderings (e.g. the multiset order) but they aren't measures, which is
important for the way termination proofs are automated.

Allow "non-datatypes" in TypeBase to have optional induction thm.

Provide appropriate values for this field for finite sets, strings,
integers, finite maps and words.

Remove some non-ASCII under src/

various new finite map theorems

characterising these situations:
- {} = FDOM fm
- (DRESTRICT f1 s2 = DRESTRICT f2 s2)
- FMERGE m m1 m2 \\ k
- FUNION f g = g
and giving sufficient conditions for:
- (f |++ kvl) ' k = v

new constant for mapping over the keys of a finite map

The operation only makes sense for an injective function, because
otherwise you have two values for the same key and the map provides
nothing by which to prefer one of them.

MAP_KEYS is definable using existing constants (see the theorem
MAP_KEYS_using_LINV) but it's pretty complicated and I think warrants
its own constant.

new finite map theorems and rewrites

Some rewrites seem obviously good. I was too afraid to include
FAPPLY_FUPDATE_THM.

The statement of f_o_FUPDATE is a bit unwieldy. I don't know if there's
a nice way to characterise that situation.

Remove some Unicode from sources.

Add automatic rewrite for FDOM (FUNION fm1 fm2).

Add rewrite about FRANGE (FUNION fm1 fm2).

Require that the domains be disjoint.

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

Extensionality of finite maps in terms of FLOOKUP

Three theorems about DOMSUB and FLOOKUP.

Add new theorem about FLOOKUPing in a FUN_FMAP.

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.

TeX macros in TeX_notation calls need to be terminated with {}.

Move more TeX notations into appropriate theory files.

Word-related notation still to do.

Added DOMSUB_COMMUTES to finite_mapTheory.

Added a number of theorems, mainly to finite_mapTheory.

finite_map:
FLOOKUP_FUNION
FEVERY_FLOOKUP
FLOOKUP_o_f
FUPDATE_LIST_APPEND
FUPDATE_FUPDATE_LIST_COMMUTES
FUPDATE_FUPDATE_LIST_MEM
pred_set:
COMPL_UNION

Make SUBMAP_REFL an exported rewrite.

SUBMAP_FUPDATE_EQN now includes more information in one of its disjuncts.

In particular, move from
f SUBMAP (f |+ (x,y)) <=> x NOTIN FDOM f \/ (f ' x = y)
to
f SUBMAP (f |+ (x,y)) <=> x NOTIN FDOM f \/ (f ' x = y) /\ x IN FDOM f

Also prove a version that uses FLOOKUP on the RHS.

(Suggested by Ramana Kumar.)

New, powerful, automatic rewrite in optionScript.

Rewrite is

|- ((if P then SOME x else NONE) = SOME z) = P /\ (x = z)

and all variants there-on.

A number of changes were necessary in other theories. This change
affects not just srw_ss() but also std_ss.

In finite_map, I created a couple of new Unicode variants for SUBMAP
and FUNION. I also tidied up some proofs, and the statement of some
goals (indentation, column limits).

added fupdate_NORMALISE_CONV

fupdate_NORMALISE_CONV simplifies fupdate - sequences by removing the ones that are masked by
later appearances.

``f |+ (x1, y1) |+ (x2, y2) |+ (x1, y3) |+ (x4, y4)``
gets for example simplied to to

|- (f |+ (x1, y1) |+ (x2, y2) |+ (x1, y3) |+ (x4, y4)) =
(f |+ (x2, y2) |+ (x1, y3) |+ (x4, y4))

The slightly tricky part in writing this conversion was to avoid checking, whether two keys are equal.
They are treaded as equal by this conversion, iff they are alpha-equivalent. Otherwise, it is not
somehow cleverly checked, whether they are equal.

For implementing this conversion the concept of two finite maps beeing equal upto a given
set of keys (fmap_EQ_UPTO) was introduced in finite_mapTheory.

New finite_mapTheory thm: |- v IN FRANGE f <=> ?k. FLOOKUP f k = SOME v
(suggested by Ramana Kumar)

Another finite map theorem from Ramana Kumar: |- DRESTRICT f P SUBMAP f

A couple of more theorems about finite maps and submaps in
particular from Ramana Kumar. One is automatic.

Add some theorems suggested by Ramana Kumar, clean up some proofs, and
make some more theorems automatic rewrites.

Additions to multiset and primeFactor
theories. Fixed definition of PRIMES
sequence in dividesTheory. Also added misc.
theorems to arithmetic. Some amount of
meaningless shuffling about.

Removed function FMAP_MAP because it was equivalent to o_f.

A collection of minor extensions. Most noticably, a operation for merging two maps has been added. Moreover, there are is a mapping operator for finite maps now. Theorems about these new operations as well as some old ones have been added as well. The new library finite_mapLib contains a conversion fevery_EXPAND_CONV that is able to expand FEVERY into a conjunction. For example

``FEVERY P (FEMPTY |+ (x1, y1) |+ (x2, y2) |+ (x3, y3) |+ (x4, y4))``

is exanded to

|- FEVERY P (X |+ (x1,y1) |+ (x2,y2) |+ (x3,y3) |+ (x4,y4)) <=>

P (x4,y4) /\
(~(x3 = x4) ==> P (x3,y3)) /\
(~((x2 = x3) \/ (x2 = x4)) ==> P (x2,y2)) /\
(~((x1 = x2) \/ (x1 = x3) \/ (x1 = x4)) ==> P (x1,y1))

Added some finite_map support to EVAL. Also
a new theorem and more syntactic support for
lists of updates.

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

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.

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.

A couple of new theorems about the FLOOKUP constant, and prettier proof
for one of the theory's lemmas.

Fixing up treatment of "ABSDATATYPE" thingies, where ordinary
constants are treated as datatype constructors in the generatd
ML.

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.

Upgrading EmitML to support records. Lots of associated changes
as well.

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.

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.

Spotted a strange-looking theorem name.

Mostly minor changes. Mainly, have changed FUPDATE_LIST in
finite_mapTheory to be a prefix, and have replaced it with
the infix notation |++.

Michael said it was OK.

Should have done this a long time ago; you can see from examination
of the sources how many times GSYM fmap_EQ_THM gets called. This theorem
now mentioned in the DESCRIPTION manual too.

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

Added a couple of extra automatic rewrites.

Some new theorems (from my specification of the Hare-Clark voting system)
and a bit of tidying, now that LIST_TO_SET has moved.

Prove a couple of useful rewrites for the o_f function (which maps a
function over a finite map), and correct an ancient typo.

A better rewrite for calculating FRANGE over finite maps that are
given in terms of FUPDATE.

More theorems; some exported.

Forgot this as an automatic rewrite candidate.

A new constant for removing a single entry from a finite map. Has nice
rewrites that don't require manipulating sets and their intersections,
which is what you get into if you use DRESTRICT straight.

YAFMT (Yet Another Finite Map Theorem). This can be used to eliminate
simple equalities between finite maps where one side is know to have
just one element. Sadly it introduces a disjunction.

A couple of new lemmas to help with simple cases of finite map elimination.

More "obvious theorems" exported.

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

Changes to parsing technology to allow left-associated infixes to
co-exist with function application in the same slot in the grammar.
Application of this new facility to the example of FAPPLY in finite_map
theory. Might also be useful if and when we get round to modelling sets
as functions in pred_set theory.

Fiddling with precedence levels for '. Comment illustrates the issue I
hope.

An "unwinding" theorem for FUPDATE_LIST that will let me match and eliminate
existentially-bound variables in expressions such as
?v1 v2 fm. (fm FUPDATE_LIST [(k1,v1); (k2, v2)] =
FEMPTY FUPDATE_LIST [... ; (k1, v11); (k2, v21)]) /\
P v1 v2 fm

Some new theorems. The pseudo injectivity results will allow me to write
code to match expressions involving FUPDATE against concrete maps.

Fairly radical revision. The original didn't depend on either of hol98's
set theories, so re-invented the notion of a predicate being finite, and
even defined the notion of deleting elements from predicates (= sets).
I have done away with this and linked whole-heartedly to pred_sets. This
means that I have changed every occurrence of FDOM f x to x IN FDOM f
(meaning, x is an element of the domain of finite map f). The power
of the modern rewriter and PROVE_TAC also means that the script file is
now 30K shorter than it used to be.
I've defined a couple of bits of new syntax:
f ' x = FAPPLY f x
and
f |+ (x, y) = FUPDATE f (x, y)
The underlying constants are still called the same thing, so the old syntax
is still supported. (Thanks to Keith for the FUPDATE syntax.)
Finally, I've added an iterated version of FUPDATE, called FUPDATE_LIST,
which is taken from the Netsem work (again, thanks Keith).

Deleted dependence on PairedDefinition.

Vacuous fix.

Minor changes to track changes in IndDefLib.

Changes to track changes in interface to
IndDefLib.new_inductive_definition.

Updates to accomodate changes to IndDefLib.

Theory of finite maps now builds in Kan.0.

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

Initial revision