fix a couple small proofs in x64_decoderScript.sml

also broken by 5203fc450

change interface to add_persistent_funs (#73) and fix more calls

The new interface takes a list of strings naming theorems.
(The old interface took a list of (string * thm) pairs.)
The new way better ensures consistency of theory development and theory
load behaviour: you can no longer pass a name with a theorem that isn't
actually saved under it.

Theorems are looked up with DB.theorem, or failing that, DB.definition
or DB.axiom.

Alas, I found more examples using add_persistent_funs to add theorems in
ancestor theories. Rather than modify the ancestor theories, I have
opted to make the offending theories save the theorems they want to add
to computeLib themselves so they have a name in the current theory to
pass to add_persistent_funs.

If this behavior was appropriate for patricia too (da47401) change it.
Alternatively, if the ancestor theories should have exported those
things for computeLib anyway, search this commit for new instances of
"save_thm" to see what needs fixing.

Various minor changes.

A few corrections.

Anthony showed me how to speed up the evaluation of x64_decode.
Each decode used to take 2-10 seconds. Now evaluation of
x64_decode takes less than 0.1 seconds, often just 0.05 seconds.

The trick is to pre-evaluate the decoder to the point where you
get equations that expose pattern matching:

x64_decode (T::F::T::F::F::F::F::rest) = ... rest ...
x64_decode (T::F::T::F::F::F::T::rest) = ... rest ...
x64_decode (T::F::T::F::F::T::F::rest) = ... rest ...
...

These equations are then given to EVAL.

The same trick should be applicable to the other decoders.

Bug fix.

A model of 64-bit x86 which supports data operations on 8-bit, 16-bit,
32-bit and 64-bit data. This is a only a first draft: there are
undoubtedly bugs lurking in how 16-bit operations perform
sign extension and how eflags are updated.