use datatype package selectors, discriminators etc in ASpec and ExecSpec

[lsf37]

ASpec and ExecSpec were written before the "new" datatype package existed, which introduced selectors (named fields) and discriminators (is_Cons) for data types. In a number of places, we still have old definitions that duplicate these. We should get rid of them.

This is not entirely non-trivial, because the datatype package adds default dest, simp, etc rules which will break some proofs.

PR https://github.com/seL4/l4v/pull/340 did an experiment on this on the rt branch for thread_state. This was successful but shows there is some proof work associated with it. In particular it sounds like the generated distinct_disc rule set sometimes leads to non-termination.

See also VER-957 for potential follow-on issues.