Add fold to sptree and a few lemmas about size

Add a few lemmas to sptreeTheory

Remove Unicode from last commit to sptreeScript.sml

Prove lookup and domain theorems for mapi

Define a mapi constant for sptrees. Prove next to nothing about it

Add theorem about size (insert k v m) to sptreeTheory

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

Progress with github issue #407

Prove that sptree insert commutes

Provide CakeML-translator-friendly version of subspt

The new definition is stored in a theorem called
sptreeTheory.subspt_eq. The old definition, i.e.
sptreeTheory.subspt_def, is proved as a lemma from
the new recursive translator-friendly definition.

Use the new definition when applying the translator:

val res = translate sptreeTheory.subspt_eq;

This is in response to a request from @HeikoBecker.

Add filter_v for sptree

Define submap rel'n on sptrees (and show as p.o.)

Material from CakeML.

Add new automatic rewrites to arithmetic

Also make EQ_MULT_LCANCEL automatic.

The new rewrites are

MAX m n = 0 <=> m = 0 /\ n = 0
MIN m n = 0 <=> m = 0 \/ n = 0

and EQ_MULT_RCANCEL

All seem worth making automatic. Changes elsewhere are fixing
breakages.

Opening lcsymtacs is no longer necessary.

All l/case short simp tacs use LET_ss + ARITH_ss

This means that fs and rfs pick up LET_ss and ARITH_ss, making them
indistinguishable from the 'l' versions.

Add 3 sptree theorems

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.

some sptree theorems

from CakeML

define a map function on sptrees

plus a few simple properties

gave lrnext a better def w.r.t. CakeML translator

prove MEM_toList for sptrees

The tactic used resists the obvious simplifications.
I don't know why sometimes (t1 >> t2) doesn't work whereas (t1 >- t2 >- t2) does.

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.

prove the keys of toAList of an sptree are ALL_DISTINCT

prove relationship between foldi and FOLDR

This means you can prove something about a fold over sptrees by doing a
list proof on the toAList of the tree, rather than messing with the
sptree's structure. (But still do the fold directly on the tree when you
execute it.)

Compute sptree domain via domain_foldi.

Also add a Lib file, which contains some conversions.

Add fromAList to sptreeTheory

Also proved some lemmas about its relation to toAList

added inter_eq, difference and toAList to sptreeTheory

Fixed broken proof

Thanks to Ramana for spotting this.

inter eq same as lookup eq for sptrees

statement of wf_inter improved

mk_wf defined, rewrites for mk_wf

fix typo in previous commit... oops

added inter(section) to sptree, also minor clean up

Some tidying in sptreeTheory.

- prove complete characterisation of lookup k (insert k' v t)
- get quicker proofs of domain_insert
- show domain (fromList l) and lookup k (fromList l) results

theorem characterising equality of wf sptrees

some theorems about isEmpty and toList on sptrees

add domain_insert and domain_sing as automatic rewrites

some theorems about domain and insert on sptrees

New sptree theorem about domain of union.

Additions to simple patricia tree theory.

* should now EVAL in good time
* union proved correct
* fold characterised a bit
* domain defined

Fix insert, delete and naming on functions for sptrees.

Also added fold.

A simple-minded "one bit at a time" patricia-tree-like data structure.