1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/Tools/isac/Knowledge/Rational.thy	Wed Aug 25 16:20:07 2010 +0200
     1.3 @@ -0,0 +1,76 @@
     1.4 +(* rationals, i.e. fractions of multivariate polynomials over the real field
     1.5 +   author: isac team
     1.6 +   Copyright (c) isac team 2002
     1.7 +   Use is subject to license terms.
     1.8 +
     1.9 +   depends on Poly (and not on Atools), because 
    1.10 +   fractions with _normalized_ polynomials are canceled, added, etc.
    1.11 +
    1.12 +   use_thy_only"Knowledge/Rational";
    1.13 +   use_thy"../Knowledge/Rational";
    1.14 +   use_thy"Knowledge/Rational";
    1.15 +
    1.16 +   remove_thy"Rational";
    1.17 +   use_thy"Knowledge/Isac";
    1.18 +   use_thy_only"Knowledge/Rational";
    1.19 +
    1.20 +*)
    1.21 +
    1.22 +Rational = Poly +
    1.23 +
    1.24 +consts
    1.25 +
    1.26 +  is'_expanded   :: "real => bool" ("_ is'_expanded")     (*RL->Poly.thy*)
    1.27 +  is'_ratpolyexp :: "real => bool" ("_ is'_ratpolyexp") 
    1.28 +
    1.29 +rules (*.not contained in Isabelle2002,
    1.30 +         stated as axioms, TODO: prove as theorems*)
    1.31 +
    1.32 +  mult_cross   "[| b ~= 0; d ~= 0 |] ==> (a / b = c / d) = (a * d = b * c)"
    1.33 +  mult_cross1  "   b ~= 0            ==> (a / b = c    ) = (a     = b * c)"
    1.34 +  mult_cross2  "           d ~= 0    ==> (a     = c / d) = (a * d =     c)"
    1.35 +
    1.36 +  add_minus  "a + b - b = a"(*RL->Poly.thy*)
    1.37 +  add_minus1 "a - b + b = a"(*RL->Poly.thy*)
    1.38 +
    1.39 +  rat_mult                "a / b * (c / d) = a * c / (b * d)"(*?Isa02*) 
    1.40 +  rat_mult2               "a / b *  c      = a * c /  b     "(*?Isa02*)
    1.41 +
    1.42 +  rat_mult_poly_l         "c is_polyexp ==> c * (a / b) = c * a /  b"
    1.43 +  rat_mult_poly_r         "c is_polyexp ==> (a / b) * c = a * c /  b"
    1.44 +
    1.45 +(*real_times_divide1_eq .. Isa02*) 
    1.46 +  real_times_divide_1_eq  "-1    * (c / d) =-1 * c /      d "
    1.47 +  real_times_divide_num   "a is_const ==> \
    1.48 +	          	  \a     * (c / d) = a * c /      d "
    1.49 +
    1.50 +  real_mult_div_cancel2   "k ~= 0 ==> m * k / (n * k) = m / n"
    1.51 +(*real_mult_div_cancel1   "k ~= 0 ==> k * m / (k * n) = m / n"..Isa02*)
    1.52 +			  
    1.53 +  real_divide_divide1     "y ~= 0 ==> (u / v) / (y / z) = (u / v) * (z / y)"
    1.54 +  real_divide_divide1_mg  "y ~= 0 ==> (u / v) / (y / z) = (u * z) / (y * v)"
    1.55 +(*real_divide_divide2_eq  "x / y / z = x / (y * z)"..Isa02*)
    1.56 +			  
    1.57 +  rat_power               "(a / b)^^^n = (a^^^n) / (b^^^n)"
    1.58 +
    1.59 +
    1.60 +  rat_add         "[| a is_const; b is_const; c is_const; d is_const |] ==> \
    1.61 +	          \a / c + b / d = (a * d + b * c) / (c * d)"
    1.62 +  rat_add_assoc   "[| a is_const; b is_const; c is_const; d is_const |] ==> \
    1.63 +	          \a / c +(b / d + e) = (a * d + b * c)/(d * c) + e"
    1.64 +  rat_add1        "[| a is_const; b is_const; c is_const |] ==> \
    1.65 +	          \a / c + b / c = (a + b) / c"
    1.66 +  rat_add1_assoc   "[| a is_const; b is_const; c is_const |] ==> \
    1.67 +	          \a / c + (b / c + e) = (a + b) / c + e"
    1.68 +  rat_add2        "[| a is_const; b is_const; c is_const |] ==> \
    1.69 +	          \a / c + b = (a + b * c) / c"
    1.70 +  rat_add2_assoc  "[| a is_const; b is_const; c is_const |] ==> \
    1.71 +	          \a / c + (b + e) = (a + b * c) / c + e"
    1.72 +  rat_add3        "[| a is_const; b is_const; c is_const |] ==> \
    1.73 +	          \a + b / c = (a * c + b) / c"
    1.74 +  rat_add3_assoc   "[| a is_const; b is_const; c is_const |] ==> \
    1.75 +	          \a + (b / c + e) = (a * c + b) / c + e"
    1.76 +
    1.77 +
    1.78 +
    1.79 +end