Added an interpreter

Given that I had already proved the clocked big-step semantics total and
deterministic, it was pretty easy to add a verified interpreter.
Hopefully it will be of use later on in creating a more sensible scheme
for initialisation.

Also tweaked a few existing proofs because I improved HOL to make
EVERY_CASE_TAC go much faster.
REPEAT FULL_CASE_TAC -> EVERY_CASE_TAC

They do the same thing, but EVERY_CASE_TAC should be faster.  But it
doesn't seem to have made a difference overall.