As far as I understand, every TLA+ spec-mapping (INSTANCE/WITH) that is "simple", i.e. does not require auxiliary variables, is indeed a refinement mapping. But once auxiliary variables are needed, things are not so clear. Abadi and Lamport proved
that if specification B implements A, then, provided B satisfies some reasonable conditions, there is a refinement mapping from any B behavior to an A behavior, that possibly requires auxiliary history and/or prophecy variables. What isn't clear to me is the opposite direction: given a mapping from B to A that has auxiliary variables, how do we ensure that it is a valid refinement mapping, namely that every added variable indeed satisfies the requirements of a history/prophecy variable?