|
1 (* rationals, i.e. fractions of multivariate polynomials over the real field |
|
2 author: isac team |
|
3 Copyright (c) isac team 2002 |
|
4 Use is subject to license terms. |
|
5 |
|
6 depends on Poly (and not on Atools), because |
|
7 fractions with _normalized_ polynomials are canceled, added, etc. |
|
8 |
|
9 use_thy_only"Knowledge/Rational"; |
|
10 use_thy"../Knowledge/Rational"; |
|
11 use_thy"Knowledge/Rational"; |
|
12 |
|
13 remove_thy"Rational"; |
|
14 use_thy"Knowledge/Isac"; |
|
15 use_thy_only"Knowledge/Rational"; |
|
16 |
|
17 *) |
|
18 |
|
19 Rational = Poly + |
|
20 |
|
21 consts |
|
22 |
|
23 is'_expanded :: "real => bool" ("_ is'_expanded") (*RL->Poly.thy*) |
|
24 is'_ratpolyexp :: "real => bool" ("_ is'_ratpolyexp") |
|
25 |
|
26 rules (*.not contained in Isabelle2002, |
|
27 stated as axioms, TODO: prove as theorems*) |
|
28 |
|
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)" |
|
32 |
|
33 add_minus "a + b - b = a"(*RL->Poly.thy*) |
|
34 add_minus1 "a - b + b = a"(*RL->Poly.thy*) |
|
35 |
|
36 rat_mult "a / b * (c / d) = a * c / (b * d)"(*?Isa02*) |
|
37 rat_mult2 "a / b * c = a * c / b "(*?Isa02*) |
|
38 |
|
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" |
|
41 |
|
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 " |
|
46 |
|
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*) |
|
49 |
|
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*) |
|
53 |
|
54 rat_power "(a / b)^^^n = (a^^^n) / (b^^^n)" |
|
55 |
|
56 |
|
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" |
|
73 |
|
74 |
|
75 |
|
76 end |