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

Annotate a theorem with explicit type variables

The tactic depends on a particular type assignment, so this removes the
possibility that some change in the way that guessed type variables are
assigned will break the proof.

Remove a local-in-end block

These make cutting and pasting from the beginning of a script file up to
a particular theorem error-prone because you may cut-and-paste the local
without also getting the in-end.

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.

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.

move alist_to_fmap_PERM to alistTheory, and simplify proof a lot

move a couple of thms about ALOOKUP into alistTheory

move thm about FUNION (alist_to_fmap ls) fm to alistTheory

Remove Unicode in src/

some alist theorems about APPEND

in particular for ALOOKUP (l1 ++ l2) and alist_to_fmap (l1 ++ l2).
making the latter an automatic rewrite means some other proofs changed.

Also made ALL_DISTINCT_fmap_to_alist_keys an automatic rewrite.

make ALOOKUP_MAP more applicable as a rewrite

by removing the argument

Remove some non-ASCII under src/

various new theorems for alistTheory, mainly about fmap_to_alist

simple ones:
- a rewrite for LENGTH (fmap_to_alist fm)
- MEM p (fmap_to_alist fm) in terms of FLOOKUP

more substantially:

- Characterise ALOOKUP "non-recursively" in terms of MEM/EL and LEAST.

- fmap_to_alist produces alists with ALL_DISTINCT keys.

- fmap_to_alist is injective.

- fmap_to_alist produces elements in a fixed order: if finite maps have
equal domains, their alist counterparts will have equal keys in the
same order.

- If alists produced by fmap_to_alist are permutations, then the finite
maps they came from are equal. (Hence actually the permutations were
equal.)

possibly these proofs can be shortened, or there are missed
opportunities to recover something as a corollary.

characterise fmap_to_alist (alist_to_fmap al)

The unconditional equation is ugly. But if we know the keys are distinct
we get that the result is a permutation of the original list.

a rewrite for FAPPLYing an alist_to_fmap when ALOOKUP succeeds

theorem about alist_to_fmap (MAP ... al)

export FDOM_alist_to_fmap as a rewrite

Remove some Unicode from sources.

add theorem ALOOKUP_MAP to alistTheory

A small theory about association lists (a concrete finite map).

Thanks to Ramana Kumar for doing most of the work on this.