(* rationals, i.e. fractions of multivariate polynomials over the real field

   author: isac team

   Copyright (c) isac team 2002

   Use is subject to license terms.

   depends on Poly (and not on Atools), because 

   fractions with _normalized_ polynomials are canceled, added, etc.

   use_thy_only"Knowledge/Rational";

   use_thy"../Knowledge/Rational";

   use_thy"Knowledge/Rational";

   remove_thy"Rational";

   use_thy"Knowledge/Isac";

   use_thy_only"Knowledge/Rational";

*)

Rational = Poly +

consts

  is'_expanded   :: "real => bool" ("_ is'_expanded")     (*RL->Poly.thy*)

  is'_ratpolyexp :: "real => bool" ("_ is'_ratpolyexp") 

rules (*.not contained in Isabelle2002,

         stated as axioms, TODO: prove as theorems*)

  mult_cross   "[| b ~= 0; d ~= 0 |] ==> (a / b = c / d) = (a * d = b * c)"

  mult_cross1  "   b ~= 0            ==> (a / b = c    ) = (a     = b * c)"

  mult_cross2  "           d ~= 0    ==> (a     = c / d) = (a * d =     c)"

  add_minus  "a + b - b = a"(*RL->Poly.thy*)

  add_minus1 "a - b + b = a"(*RL->Poly.thy*)

  rat_mult                "a / b * (c / d) = a * c / (b * d)"(*?Isa02*) 

  rat_mult2               "a / b *  c      = a * c /  b     "(*?Isa02*)

  rat_mult_poly_l         "c is_polyexp ==> c * (a / b) = c * a /  b"

  rat_mult_poly_r         "c is_polyexp ==> (a / b) * c = a * c /  b"

(*real_times_divide1_eq .. Isa02*) 

  real_times_divide_1_eq  "-1    * (c / d) =-1 * c /      d "

  real_times_divide_num   "a is_const ==> \

	          	  \a     * (c / d) = a * c /      d "

  real_mult_div_cancel2   "k ~= 0 ==> m * k / (n * k) = m / n"

(*real_mult_div_cancel1   "k ~= 0 ==> k * m / (k * n) = m / n"..Isa02*)

  real_divide_divide1     "y ~= 0 ==> (u / v) / (y / z) = (u / v) * (z / y)"

  real_divide_divide1_mg  "y ~= 0 ==> (u / v) / (y / z) = (u * z) / (y * v)"

(*real_divide_divide2_eq  "x / y / z = x / (y * z)"..Isa02*)

  rat_power               "(a / b)^^^n = (a^^^n) / (b^^^n)"

  rat_add         "[| a is_const; b is_const; c is_const; d is_const |] ==> \

	          \a / c + b / d = (a * d + b * c) / (c * d)"

  rat_add_assoc   "[| a is_const; b is_const; c is_const; d is_const |] ==> \

	          \a / c +(b / d + e) = (a * d + b * c)/(d * c) + e"

  rat_add1        "[| a is_const; b is_const; c is_const |] ==> \

	          \a / c + b / c = (a + b) / c"

  rat_add1_assoc   "[| a is_const; b is_const; c is_const |] ==> \

	          \a / c + (b / c + e) = (a + b) / c + e"

  rat_add2        "[| a is_const; b is_const; c is_const |] ==> \

	          \a / c + b = (a + b * c) / c"

  rat_add2_assoc  "[| a is_const; b is_const; c is_const |] ==> \

	          \a / c + (b + e) = (a + b * c) / c + e"

  rat_add3        "[| a is_const; b is_const; c is_const |] ==> \

	          \a + b / c = (a * c + b) / c"

  rat_add3_assoc   "[| a is_const; b is_const; c is_const |] ==> \

	          \a + (b / c + e) = (a * c + b) / c + e"

end