consolidate equations between ASpec/Haskell constants into one theory

[lsf37]

See discussion on #846 (comment) -- it would be nice to collect lemmas like

lemma virqType_eq[simp]:
  "virqType = virq_type"

into one theory in Refine that is included relatively early.

This would help to consolidate, make sure we're using a consistent simp direction for these and potentially mark them for sharing between the specs directly.

Main problem is how to find them all.