Add new definition: word_exp

[xrchz]

Includes a more-efficient-to-eval tail-recursive version as well as a straightforward recursive version.

[acjf3]

To be consistent with the existing theory, I'd expect word_exp to be declared around line 262 in wordsScript.sml, in the "Word arithmetic: definitions" section, preferably using the same style. That is, the definition would be word_exp (v:'a word) (w:'a word) = (n2w:num->'a word) (w2n v ** w2n w), and the overloading would be added to the list at line 313. The old definition would then be derived within a theorem. Is the efficient-to-eval version actually faster than casting to and from :num? Could EXP evaluation be sped up with a tail recursive version instead?

[acjf3]

It now occurs to me that the ability to do a MOD upon every iteration should help the efficiency quite a bit. I still think it's a good idea to make the n2w version the definition, and then derive an efficient-to-compute version from that. Also, can you look into updating the wordsSyntax files as well. My other concern is that the new overloading on ** might break some developments, but at least fixes should be fairly straightforward.

[xrchz]

@acjf3 I think I've addressed all your concerns but please take a look and let me know. Thanks for the good suggestions.

[acjf3]

Yes, those changes have have addressed my concerns and the pull request looks v. good to me.