It is used for nondeterministic choice, so Undefined might be
misleading.

The suffix _lemmas is more descriptive than _extras.

Architecture-specific lemmas about concrete registers and types are generated
and written to a file <prefix>_lemmas.thy, generic lemmas are in the
theories *_extras.thy in lib/isabelle.  In particular, State_extras contains
simplification lemmas about the lifting from prompt to state monad.

Generate only one Lem model based on the prompt monad (instead of two models
with different monads), and add a lifting from prompt to state monad.  Add some
Isabelle lemmas about the monad lifting.

Also drop the "_embed" and "_sequential" suffixes from names of generated
files.

Makes bitvector typeclass instance dictionaries disappear from generated
Isabelle output.

- Remove vector start indices
- Library refactoring:  Definitions in sail_operators.lem now use Bitvector
  type class and work for both bit list and machine word representations
- Add Lem bindings to AArch64 and RISC-V preludes

TODO: Merge specialised machine word operations from sail_operators_mwords into
sail_operators.