Fix register machine theory for pat_assum rename

Invent a listpresent b v = 'list of values v is present starting at reg b'

Complete projection and SUC cases in RMs implement RecFns proof.

Prove a bunch of usedregs rewrites.

Add 'usedregs' constant to calculate registers touched by an RM.

Prove various properties, including the important one that unused
registers really don't change.

Complete register machine 'implements' proofs for SUC and projection.

Progress with implements relation for connection between RM and RecFun.

Thoughts about a new implements relation.

Complete proof of correctness of 'copy' program for reg. machines.

Start on properties of register machine 'copy program'.

Updates for register theory.

* new notation for HOARE triples
* proof of Norbert Schirmer's nice "intro of auxiliary variable" rule
* lots of rewrites for substitutions over state-predicates
* proof of move's correctness using the while rule as well as the NS
auxiliary consequence rule

Prove WHILE-rule for register machine Hoare logic; use on 1 example.

The 1 example is the simplest possible loop: one where the body of
the loop is skip. This is a terminating program that zeroes a
register.

Scribblings towards a Hoare-ish logic for register machines.

Update case-syntax in register machines script.

Turn reg interactive script into regScript. Also use records.