1.1 --- a/src/Tools/isac/IsacKnowledge/Rational.thy	Wed Aug 25 15:15:01 2010 +0200
     1.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.3 @@ -1,76 +0,0 @@
     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"IsacKnowledge/Rational";
    1.13 -   use_thy"../IsacKnowledge/Rational";
    1.14 -   use_thy"IsacKnowledge/Rational";
    1.15 -
    1.16 -   remove_thy"Rational";
    1.17 -   use_thy"IsacKnowledge/Isac";
    1.18 -   use_thy_only"IsacKnowledge/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