Reorganisation of repl_funTheory

Define all the versions of the REPL in the logic, with informative names
and comments. State the desired correctness theorem at the end (but no
proofs updated yet).
work on cleaning up repl_funProofScript.sml

move various things to places where they are more likely to belong.  the
repl correctness lemma builds now, but the main repl correctness
theorems are not yet proved (or stated) and there is some problem with
the setup of the initial bytecode state (different places expect
empty_bc_state to have different code).
rework treatment of initial bytecode state

make empty_bc_state actually empty, and use labelled_repl_step to make
the transition between empty_bc_state and initial_bc_state (which
contains VfromListCode).

also, realise that repl is non-deterministic because of the type error
mask, so we can't get the nice repl theorem in the "proof aim", and will
have to settle for one direction of the bi-implication until
type-inferencer completeness is proved.
make all the repl_funs do the code_asserts
rework repl_fun again, and push the proofs further

The problem was that the initial bytecode should not be run, it should
just be there. So, now we don't start the REPL with empty_bc_state but
rather with (strip_labels initial_bc_state). (This is better than the
alternative of having the main loop check whether it's in the initial
case every time before deciding whether to run the code.)

Also, fixed some mistakes in the definition of main_loop after the
unrolled stage, and prove the unrolled version correct. The statement
mentions the output from running the basis program - somewhere we will
have to prove that that is empty...
more work on repl_funProofTheory

fix error in definition of unlabelled_repl_fun (had an extra REVERSE).
move various bytecode-related theorems into bytecode (though some still
remain to be moved). work towards proving correctness of the
unlabelled_repl_fun (down to 1 fairly big cheat).
prove cheat for unlabelled_repl_fun, tweak definitions

simple_main_loop and unrolled_main_loop need to assert code_labels_ok
earlier than previously defined. It makes a difference now because the
initial bytecode state contains code. This assertion goes away when we
pass to unlabelled_main_loop, so moving it doesn't matter.
prove basis_repl_fun correct

this is the one that should be implemented by the machine-code.
we now have a theorem connecting it to repl (the semantics relation).
delete repl_fun_alt_proofScript.sml
Merge remote-tracking branch 'origin/alpha_vector' into alpha_array