automatic-simplification-2010-02-24.pure

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

using math ;

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

sump x = case x of (a+b) = 1 ; a = 0 ; end ;

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

flatten_product (a*b*c) = cat [(flatten_product (a*b)),[c]] ;

flatten_product (a*b) = [a,b] ;

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

flatten_sum (a+b+c) = cat [(flatten_sum (a+b)),[c]] ;

flatten_sum (a+b) = [a,b] ;

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

O_3 [] x = 1 ;

O_3 x [] = 0 ;

O_3 (u:us) (v:vs) = if u === v then O_3 us vs else order_relation u v ;

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

order_relation a b = a < b if numberp a && numberp b ;

order_relation a b = 1 if numberp a && ~ numberp b ;

order_relation a b = 0 if ~ numberp a && numberp b ;


order_relation (a*b) (c*d) = 
  O_3 (reverse (flatten_product (a*b))) (reverse (flatten_product (c*d))) ;

order_relation (a+b) (c+d) = 
  O_3 (reverse (flatten_sum (a+b))) (reverse (flatten_sum (c+d))) ;

// power ...

// functions ...

// order_relation (a+b) (c*d) = 0 ; // experimental
// order_relation (a*b) (c+d) = 0 ; // experimental

order_relation a b = (str a) < (str b) ;

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

base (x^y) = x ;

base x = x ;

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

exponent (x^y) = y ;

exponent x = 1 ;

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

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

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

term x = x ;

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

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

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

constant x = 1 ;

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

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

// x^(1.0) = x ;

// (r^s)^w = r^(s*w) if intp w ;

// (x*y)^w = (x^w)*(y^w) if intp w ;

(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 order_relation y x ;

x*y*z = x*z*y if order_relation 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 (order_relation b a) && ~(sump a) ;

a+b+c = a+c+b if order_relation c b ;

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

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

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

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

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

// base (x^y) ;

// base x ;

// exponent (x^y) ;

// exponent x ;

// 4+x+6+x ;

// x+y+z+x

// x*x ;

// x*x^3

// x*y*x*z ;

// -((x*y)/3)

// ((x^(1%2))^(1%2))^8 ;

// ((x^(1/2))^(1/2))^8 ;

// (((x*y)^(1/2))*(z^2))^2

// x/x ;

// x/y * y/x ;

// x^2 * x^3 ;

// x+y+x+z+5+z ;

// 5+5*x+5*y ;

// (x+y) * (4+y+x-4) ;

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