automatic-simplification-2010-02-25.pure

using math ;

//////////////////////////////////////////////////////////////////////

sump (x+y) = 1 ; sump x = 0 ;

//////////////////////////////////////////////////////////////////////

base (x^y) = x ;

base x = x ;

//////////////////////////////////////////////////////////////////////

exponent (x^y) = y ;

exponent x = 1 ;

//////////////////////////////////////////////////////////////////////

term (n*x) = x if numberp n ;

term ((x*y)*z) = (term (x*y)) * z ;

term x = x ;

//////////////////////////////////////////////////////////////////////

constant (n*x) = n if numberp n ;

constant ((x*y)*z) = (constant (x*y)) ;

constant x = 1 ;

//////////////////////////////////////////////////////////////////////

cmp x y = x < y if numberp x && numberp y ;

cmp x y = 1 if numberp x && ~(numberp y) ;

cmp (a^b) (c^d) = if a === c then cmp b d else cmp a c ;

cmp a (b^c) = if a === b then cmp 1 c else cmp a b ;

cmp (a^b) c = if a === b then cmp b 1 else cmp a c ;

cmp (x1@_ y1) (x2@_ y2) = if x1===x2 then cmp y1 y2 else cmp x1 x2;

cmp (x1@_ y1) x2 = if x1===x2 then 0 else cmp x1 x2;

cmp x1 (x2@_ y2) = if x1===x2 then 1 else cmp x1 x2;

cmp x y = str x < str y if atomp x && atomp y ;

cmp x y = ~(cmp y x) otherwise ;

//////////////////////////////////////////////////////////////////////
// ^
//////////////////////////////////////////////////////////////////////

0^x = 0 ;
1^x = 1 ;
x^0 = 1 ;
x^1 = x ;

(r^s)^w = r^(s*w) if numberp w ;

(x*y)^w = (x^w)*(y^w) if numberp w ;

//////////////////////////////////////////////////////////////////////
// *
//////////////////////////////////////////////////////////////////////

0*x = 0 ;

x*y = (base x) ^ ((exponent x) + (exponent y)) if (base x) === (base y) ;

a*x*y = a * ( (base x) ^ ((exponent x) + (exponent y)) ) if (base x) === (base y) ;

x*y = y*x if cmp y x ;

x*y*z = x*z*y if cmp z y ;

x*(y*z) = x*y*z ;

//////////////////////////////////////////////////////////////////////
// +
//////////////////////////////////////////////////////////////////////

0+x = x ;

a+b = ((constant a) + (constant b)) * (term a) if ((term a) === (term b)) ;

a+b+c = a + (((constant b) + (constant c)) * (term b)) if (term b) === (term c) ;

a+b = b+a if (cmp b a) && ~(sump a) ;

a+b+c = a+c+b if cmp c b ;

a+(b+c) = a+b+c ;

//////////////////////////////////////////////////////////////////////

x - y = x + (-1 * y) ;

x / y = x * (y^(-1)) ;

//////////////////////////////////////////////////////////////////////
// cmp examples
//////////////////////////////////////////////////////////////////////

cmp (z^2) y == 0 || throw 1000

cmp y (z^2) == 1 || throw 1001




//////////////////////////////////////////////////////////////////////
// examples
//////////////////////////////////////////////////////////////////////

4+x+6+x === 10+2*x || throw 0 ;

x+y+z+x === 2*x+y+z || throw 1 ;

x*x === x^2 || throw 2 ;

x*x^3 === x^4 || throw 3 ;

x*y*x*z === x^2*y*z || throw 4 ;

((x^(1/2))^(1/2))^8 === x^2.0 || throw 5 ;

x/x === 1 || throw 6 ;

x/y * y/x === 1 || throw 7 ;

x^2 * x^3 === x^5 || throw 8 ;

x+y+x+z+5+z === 5+2*x+2*z+y || throw 9 ;

(x+y) * (4+y+x-4) === (x+y)^2 || throw 10 ;

x*x*z*z*x === x^3*z^2 || throw 11 ;