A place for folded machine_word_len lemmas

[Xaphiosis]

When doing generic proofs involving machine_word_len words, we are not supposed to know what machine_word_len is. Unfortunately, a number of lemmas provided by Word_Lib and our WordSetup will be lemmas that are generic in the word size, but use LENGTH('a) which immediately leaks the word length as a number. These lemmas can't be used in arch-generic context without the [where 'a=machine_word_len, folded word_bits_def] pattern.
Furthermore, some lemmas only provide 32/64 versions explicitly.

This means two things:

1. to not write [where 'a=machine_word_len, folded word_bits_def] every single time, it would be useful to have lemmas which use machine_word_len internally, but with the same name on all arches, e.g.

lemmas unat_of_nat_eq_mw = unat_of_nat_eq[where 'a=machine_word_len, folded word_bits_def]

2. it would be really good to have a bundle which takes all of the LENGTH('a) lemmas that are in the simpset and:
   • removes them from the simpset (we can find these with the new inside: functionality of find_theorems)
   • adds [where 'a=machine_word_len, folded word_bits_def] versions of them to the simpset instead

For 1, @lsf37 noted the following:

I think we're missing a quasi-generic Machine_Word.thy, i.e. one that already sees a fixed machine_word declaration, but one that does not make use of what that is. It does not quite fit into the rest of Word_Lib, because standard Word_Lib does not yet have the concept of loading only one of Machine_Word_64 or Machine_Word_32. We introduce that in WordSetup.thy, which is our current entry point into Word_Lib. Machine_Word.thy would have to import WordSetup.thy. I have the feeling that a lot the lemmas that currently are in Machine_Word_32 and Machine_Word_64 could be deduplicated into such a new Machine_Word theory, because many of them have exactly the pattern you have above.

Concrete proposal: Add Machine_Word.thy to Word_Lib (not included in AFP). It imports WordSetup. Change all imports of WordSetup to Machine_Word instead. Put the lemmas above in Machine_Word, consider moving more lemmas of the same form there.

With the clarification:

I meant: change all existing mentions of WordSetup imports in l4v to Machine_Word instead, making it our new entry point to Word_Lib.

This would also be a good place for the bundle.