1 (* rationals, i.e. fractions of multivariate polynomials over the real field
3 Copyright (c) isac team 2002
4 Use is subject to license terms.
6 depends on Poly (and not on Atools), because
7 fractions with _normalized_ polynomials are canceled, added, etc.
9 use_thy_only"Knowledge/Rational";
10 use_thy"../Knowledge/Rational";
11 use_thy"Knowledge/Rational";
14 use_thy"Knowledge/Isac";
15 use_thy_only"Knowledge/Rational";
23 is'_expanded :: "real => bool" ("_ is'_expanded") (*RL->Poly.thy*)
24 is'_ratpolyexp :: "real => bool" ("_ is'_ratpolyexp")
26 rules (*.not contained in Isabelle2002,
27 stated as axioms, TODO: prove as theorems*)
29 mult_cross "[| b ~= 0; d ~= 0 |] ==> (a / b = c / d) = (a * d = b * c)"
30 mult_cross1 " b ~= 0 ==> (a / b = c ) = (a = b * c)"
31 mult_cross2 " d ~= 0 ==> (a = c / d) = (a * d = c)"
33 add_minus "a + b - b = a"(*RL->Poly.thy*)
34 add_minus1 "a - b + b = a"(*RL->Poly.thy*)
36 rat_mult "a / b * (c / d) = a * c / (b * d)"(*?Isa02*)
37 rat_mult2 "a / b * c = a * c / b "(*?Isa02*)
39 rat_mult_poly_l "c is_polyexp ==> c * (a / b) = c * a / b"
40 rat_mult_poly_r "c is_polyexp ==> (a / b) * c = a * c / b"
42 (*real_times_divide1_eq .. Isa02*)
43 real_times_divide_1_eq "-1 * (c / d) =-1 * c / d "
44 real_times_divide_num "a is_const ==> \
45 \a * (c / d) = a * c / d "
47 real_mult_div_cancel2 "k ~= 0 ==> m * k / (n * k) = m / n"
48 (*real_mult_div_cancel1 "k ~= 0 ==> k * m / (k * n) = m / n"..Isa02*)
50 real_divide_divide1 "y ~= 0 ==> (u / v) / (y / z) = (u / v) * (z / y)"
51 real_divide_divide1_mg "y ~= 0 ==> (u / v) / (y / z) = (u * z) / (y * v)"
52 (*real_divide_divide2_eq "x / y / z = x / (y * z)"..Isa02*)
54 rat_power "(a / b)^^^n = (a^^^n) / (b^^^n)"
57 rat_add "[| a is_const; b is_const; c is_const; d is_const |] ==> \
58 \a / c + b / d = (a * d + b * c) / (c * d)"
59 rat_add_assoc "[| a is_const; b is_const; c is_const; d is_const |] ==> \
60 \a / c +(b / d + e) = (a * d + b * c)/(d * c) + e"
61 rat_add1 "[| a is_const; b is_const; c is_const |] ==> \
62 \a / c + b / c = (a + b) / c"
63 rat_add1_assoc "[| a is_const; b is_const; c is_const |] ==> \
64 \a / c + (b / c + e) = (a + b) / c + e"
65 rat_add2 "[| a is_const; b is_const; c is_const |] ==> \
66 \a / c + b = (a + b * c) / c"
67 rat_add2_assoc "[| a is_const; b is_const; c is_const |] ==> \
68 \a / c + (b + e) = (a + b * c) / c + e"
69 rat_add3 "[| a is_const; b is_const; c is_const |] ==> \
70 \a + b / c = (a * c + b) / c"
71 rat_add3_assoc "[| a is_const; b is_const; c is_const |] ==> \
72 \a + (b / c + e) = (a * c + b) / c + e"