Add LD1R, FMOV and SRI instructions

[pennyannn]

Description of changes:

Adding a couple more Arm instructions used in SHA3 and AES-XTS:

1. LD1R post-immediate offset
2. FMOV (general) double-precision
3. SRI (vector)

By submitting this pull request, I confirm that you can use, modify, copy, and redistribute this contribution, under the terms of your choice.

[jargh]

I think it may be possible to use the relatively new word_duplicate function in the HOL Light libraries to avoid the multiple analogous functions word_replicate2, word_replicate4 etc.

[pennyannn]

I think it may be possible to use the relatively new word_duplicate function in the HOL Light libraries to avoid the multiple analogous functions word_replicate2, word_replicate4 etc.

Thanks for mentioning it! Updated.