prove compile_decs_divergence

This required some extra lemmas about the bytecode clock, which
surprises me. Maybe I did the proof some long wrong way. However, the
lemmas added are in the clockScript.sml sketch and weren't previously
proved (as far as I remember).

In particular, I needed to prove that if you timeout with a given clock,
then you also timeout when any lower clock.

This had not been necessary previously even when divergence for single
declarations had been proved. I guess maybe there is an issue with
multiple declarations, because you need to start with enough ticks to
process them all, whereas results in the semantics are phrased in terms
of just enough ticks to process one.

I also had to copy a lot of the proof from compile_decs_thm, to prove
the assumptions of the inductive hypothesis, which is essentially the
same when we want to go past a terminating declaration to find the
divergence (in the other theorem we want to go past a terminating
declaration to find the final value). It would be nice if this could be
modularised out as a separate lemma somehow, but copy+paste+edit works
for now.