@mmcdara You wrote:
- Thanks for your first reply about the mechanism behind satisfies.
My first Reply is about the distinction between operators and operands. I hope that you read that also. My second Reply is about satisfies.
- Is there a particular reason to write indets(e, typefunc(anything, And(name, Not(mathfunc)))) instead of
indets(e, typefunc(And(anything, name, Not(mathfunc))))?
As you confirmed, anything is the implicit first argument of typefunc when it's used with one argument. Since anything is like the identity type of And, there's never a reason to use anything as an argument to And. So, the whole thing can be simplified to indets(e, typefunc(And(name, Not(mathfunc)))).
- What situation does indets(e, typefunc(anything, And(name, Not(mathfunc)))) avoid that
indets(e, Not(mathfunc)) doesn't?
Given any "reasonable" type foo, I don't think that it'd ever be a good idea to use indets(e, Not(foo)), which would select all subexpressions, no matter how complicated, that aren't of type foo.
- Is it necessary to discard the "case of a constant" in indets(expr, And(name, Not(constant))) ?
For instance it seems that these simplifications of v still give the correct result.
From your new example expr, I guess that you realize that Pi is both a name and a constant. But your example is superficial because the Pi is not inside piecewise. If you put it inside the piecewise for which it's currently a coefficient (this can even be done in a way that doesn't change the mathematical meaning of expr), then you'll see why constants need to be discarded from the freeof set. (Your example is superficial because the expressions that appear outside the piecewises are irrelevant to determining whether a term is selected.)
- Maybe a little less concise than Preben's but I still vote up
Preben's Answer addresses the specific example that you gave. My Answer addresses the verbal description that you gave (modulo my comment about operator vs, operator) using the example as a guide but trying to cover all cases "in the same spirit" as the example that fit your verbal description. There are a vast variety of such cases "in the same spirit" that are covered by my Answer but not his. For example, Preben's Answer will select any term containing any piecewise that contains any inequality or equation whose left side is t, even if that piecewise contains x elsewhere. Surely, such a piecewise shouldn't be considered to be a "function of t alone". And what if 2*t is on the left side of the inequalities? What if t is on the right side but not the left?