A TLA+ specification is a mathematical formula. "Evaluation' is not a
meaningful concept in mathematics. TLC is a program, one of its tasks
being to compute the set of possible next states of an action for a
given state. Since this involves trying to solve an unsolvable
problem, TLC uses certain heuristics. For example, it will do this
for the action formula (x' = 1) /\ (y' = x') but not for the
equivalent action formula (y' = x') /\ (x' = 1).
TLC's heuristics are insensitive to the use of definitions. In your
example, it handles Foo(x)' exactly the way it handles (x \cup y)',
which is exactly the way it handles (x' \cup y').
In almost all cases that arise in practice, it is easy to rewrite a
sensible action formula in a form that TLC can handle--for example by
rewriting (y' = x') /\ (x' = 1) as (x' = 1) /\ (y' = x'). Thus, if
you can't find such a rewriting, the odds are that your formula is not
sensible because it doesn't mean what you think it should. It may
therefore be instructive if you would post an action formula (that is
as simple as possible) that you would like TLC to evaluate but that
it doesn't.
Leslie