On 2013-06-18, Wilhelm Haager <wilhelm.haager at htlstp.ac.at> wrote:
> I want to realize the addition theorem for the arctangent using
> defrule:
>
> matchdeclare([aa,bb,cc],true);
> defrule(atanplus,atan(aa)+atan(bb)+cc,atan(xthru((aa+bb)/(1-aa*bb)))+cc);
I don't know for sure whether the problem with the rule as you stated it
is a bug in the pattern matching code, or a predictable consequence.
Anyway, here's a different way to go about it.
(%i20) matchdeclare (aa, all);
(%o20) done
(%i21) defrule (m1, atan (aa), true);
(%o21) m1 : atan(aa) -> true
(%i22) defrule (m2, - atan (aa), true);
(%o22) m2 : - atan(aa) -> true
(%i23) matchdeclare (cc, lambda ([e], not (m1 (e) or m2 (e))));
(%o23) done
(%i24) defrule (r1, aa + bb + cc, FOO (aa, bb, cc));
(%o24) r1 : cc + bb + aa -> FOO(aa, bb, cc)
(%i25) apply1 (atan (x) + atan (y) + 1, r1);
(%o25) atan(y) + atan(x) + 1
(%i26) apply1 (atan (x) + atan (y) + 1 - atan (z), r1);
(%o26) FOO(atan(y) + atan(x), - atan(z), 1)
FOO is presumably the function which implements the addition rule. FOO
still has to extract the arguments of atan.
Note that r1 requires both atan and -atan terms. You would have to
define other rules for only atan and only -atan terms.
Dunno if this is more useful than applying trigsimp and friends. It is
more limited, certainly, which might make it easier to predict what the
result will be -- dunno if that's a real advantage.
Hope this helps,
Robert Dodier