Consolidate functional descriptions of various NEON multiplication instructions

[hanno-becker]

Various NEON multiplication instructions {S,X}MULL{2} could be consolidated, making the signed-ness and low/top bit parameters to a common functional description. It is unclear (to me) if this would require patching up some proofs dealing with UMULL{2}/UMLAL, so it was not attempted in the PR #204 which introduces the signed variants. Still, the descriptions should be consolidated at some point.