Vector Identities, Redux and more questions

Neilen,

I have been tinkering with some code to process rule definitions like this --

  div (s*V) --> s*(div V) + V.(grad s) (after)
    assuming (scalar_not1p (s), nonscalarp (V));

which expands into appropriate matchdeclare and tellsimp/tellsimpafter
expressions. --> and assuming are implemented as macros which
substitute gensyms for the variables mentioned by predicate
expressions (thus avoiding name collisions) and also encloses
the tellsimp/tellsimpafter within block ([simp : false], ...) .

I am hoping that the --> / assuming stuff is not only easier
for programming (because it avoids the gotchas brought on by
name collisions and unintended application of rules in rule
definitions), but also more comprehensible to read.

I'll post the code somewhere.

HTH
Robert Dodier

PS. Here is a reworking of the vector identities you emailed a few days ago.

scalar_not1p (e) := e # 1 and scalarp (e)$
truep (e) := true;

(curl (s*V) --> s*(curl V) - V~(grad s) (after),
 (s * V) ~ aa --> s * (V ~ aa) (after),
 aa ~ (s * V) --> s * (aa ~ V) (after))
    assuming (scalar_not1p (s), nonscalarp (V), truep (aa));

declare (["grad", "laplacian"], nonscalar);
declare ("curl", additive);

div (s*V) --> s*(div V) + V.(grad s) (after)
    assuming (scalar_not1p (s), nonscalarp (V));

declare ("div", additive);

div(A ~ B) --> B.(curl A) - A.(curl B) (after)
    assuming (nonscalarp (A), nonscalarp (B));

/* grad(f*g) = f*grad(g) + g*grad(f) */

scalarprod2p (e) := not atom(e) and op(e) = "*" and length(e) = 2
    and scalarp (first (e)) and scalarp (second (e));

grad (s2) -->
    first (s2) * (grad second (s2)) + second (s2) * (grad first (s2)) (after)
    assuming (scalarprod2p (s2));

declare ("grad", additive);