Changes

Summary

1. more lemmas
2. build bit operations on word on library theory on bit operations
3. bit operations as distinctive library theory
4. tweak for code generation
5. pragmatically ruled out word types of length zero: a bit string with no bits is not bit string at all
6. more lemmas and less name space pollution
7. canonical bit shifts for word type, leaving duplicates as they are at the moment
8. essential instance about bit structure
9. more transfer rules
10. dropped yet another duplicate
11. fundamental construction of word type following existing transfer rules
12. replaced mere alias by input abbreviation
13. replaced mere alias by abbreviation
14. replaced operation with weak abstraction by input abbreviation
15. avoid compound operation
16. formal relationships between operations
17. eliminated warnings
18. replaced mere alias by input abbreviation