Improvements to phase shifting + purification lemmas (#8598)

Improvements to phase shifting + purification lemmas (#8598)

Makes 3 improvements to phase shifting + purification lemmas:
(1) we use purification skolems when possible, e.g. for exp(t), or sin(c) where -pi <= c <= pi, since it is unnecessary to assert c is in proper phase. This also adds proofs for purification of exp, which is hence trivial.
(2) we make the phase shift variable a real for which is_int holds. This avoids mixed int/real arithmetic, in preparation for eliminating subtyping
(3) the proof checker and sine solver use a common utility for getting the phase shift lemma.