author | Walther Neuper <neuper@ist.tugraz.at> |
Thu, 12 Aug 2010 11:02:32 +0200 | |
branch | isac-update-Isa09-2 |
changeset 37906 | e2b23ba9df13 |
permissions | -rw-r--r-- |
neuper@37906 | 1 |
(* rationals, i.e. fractions of multivariate polynomials over the real field |
neuper@37906 | 2 |
author: isac team |
neuper@37906 | 3 |
Copyright (c) isac team 2002 |
neuper@37906 | 4 |
Use is subject to license terms. |
neuper@37906 | 5 |
|
neuper@37906 | 6 |
depends on Poly (and not on Atools), because |
neuper@37906 | 7 |
fractions with _normalized_ polynomials are canceled, added, etc. |
neuper@37906 | 8 |
|
neuper@37906 | 9 |
use_thy_only"IsacKnowledge/Rational"; |
neuper@37906 | 10 |
use_thy"../IsacKnowledge/Rational"; |
neuper@37906 | 11 |
use_thy"IsacKnowledge/Rational"; |
neuper@37906 | 12 |
|
neuper@37906 | 13 |
remove_thy"Rational"; |
neuper@37906 | 14 |
use_thy"IsacKnowledge/Isac"; |
neuper@37906 | 15 |
use_thy_only"IsacKnowledge/Rational"; |
neuper@37906 | 16 |
|
neuper@37906 | 17 |
*) |
neuper@37906 | 18 |
|
neuper@37906 | 19 |
Rational = Poly + |
neuper@37906 | 20 |
|
neuper@37906 | 21 |
consts |
neuper@37906 | 22 |
|
neuper@37906 | 23 |
is'_expanded :: "real => bool" ("_ is'_expanded") (*RL->Poly.thy*) |
neuper@37906 | 24 |
is'_ratpolyexp :: "real => bool" ("_ is'_ratpolyexp") |
neuper@37906 | 25 |
|
neuper@37906 | 26 |
rules (*.not contained in Isabelle2002, |
neuper@37906 | 27 |
stated as axioms, TODO: prove as theorems*) |
neuper@37906 | 28 |
|
neuper@37906 | 29 |
mult_cross "[| b ~= 0; d ~= 0 |] ==> (a / b = c / d) = (a * d = b * c)" |
neuper@37906 | 30 |
mult_cross1 " b ~= 0 ==> (a / b = c ) = (a = b * c)" |
neuper@37906 | 31 |
mult_cross2 " d ~= 0 ==> (a = c / d) = (a * d = c)" |
neuper@37906 | 32 |
|
neuper@37906 | 33 |
add_minus "a + b - b = a"(*RL->Poly.thy*) |
neuper@37906 | 34 |
add_minus1 "a - b + b = a"(*RL->Poly.thy*) |
neuper@37906 | 35 |
|
neuper@37906 | 36 |
rat_mult "a / b * (c / d) = a * c / (b * d)"(*?Isa02*) |
neuper@37906 | 37 |
rat_mult2 "a / b * c = a * c / b "(*?Isa02*) |
neuper@37906 | 38 |
|
neuper@37906 | 39 |
rat_mult_poly_l "c is_polyexp ==> c * (a / b) = c * a / b" |
neuper@37906 | 40 |
rat_mult_poly_r "c is_polyexp ==> (a / b) * c = a * c / b" |
neuper@37906 | 41 |
|
neuper@37906 | 42 |
(*real_times_divide1_eq .. Isa02*) |
neuper@37906 | 43 |
real_times_divide_1_eq "-1 * (c / d) =-1 * c / d " |
neuper@37906 | 44 |
real_times_divide_num "a is_const ==> \ |
neuper@37906 | 45 |
\a * (c / d) = a * c / d " |
neuper@37906 | 46 |
|
neuper@37906 | 47 |
real_mult_div_cancel2 "k ~= 0 ==> m * k / (n * k) = m / n" |
neuper@37906 | 48 |
(*real_mult_div_cancel1 "k ~= 0 ==> k * m / (k * n) = m / n"..Isa02*) |
neuper@37906 | 49 |
|
neuper@37906 | 50 |
real_divide_divide1 "y ~= 0 ==> (u / v) / (y / z) = (u / v) * (z / y)" |
neuper@37906 | 51 |
real_divide_divide1_mg "y ~= 0 ==> (u / v) / (y / z) = (u * z) / (y * v)" |
neuper@37906 | 52 |
(*real_divide_divide2_eq "x / y / z = x / (y * z)"..Isa02*) |
neuper@37906 | 53 |
|
neuper@37906 | 54 |
rat_power "(a / b)^^^n = (a^^^n) / (b^^^n)" |
neuper@37906 | 55 |
|
neuper@37906 | 56 |
|
neuper@37906 | 57 |
rat_add "[| a is_const; b is_const; c is_const; d is_const |] ==> \ |
neuper@37906 | 58 |
\a / c + b / d = (a * d + b * c) / (c * d)" |
neuper@37906 | 59 |
rat_add_assoc "[| a is_const; b is_const; c is_const; d is_const |] ==> \ |
neuper@37906 | 60 |
\a / c +(b / d + e) = (a * d + b * c)/(d * c) + e" |
neuper@37906 | 61 |
rat_add1 "[| a is_const; b is_const; c is_const |] ==> \ |
neuper@37906 | 62 |
\a / c + b / c = (a + b) / c" |
neuper@37906 | 63 |
rat_add1_assoc "[| a is_const; b is_const; c is_const |] ==> \ |
neuper@37906 | 64 |
\a / c + (b / c + e) = (a + b) / c + e" |
neuper@37906 | 65 |
rat_add2 "[| a is_const; b is_const; c is_const |] ==> \ |
neuper@37906 | 66 |
\a / c + b = (a + b * c) / c" |
neuper@37906 | 67 |
rat_add2_assoc "[| a is_const; b is_const; c is_const |] ==> \ |
neuper@37906 | 68 |
\a / c + (b + e) = (a + b * c) / c + e" |
neuper@37906 | 69 |
rat_add3 "[| a is_const; b is_const; c is_const |] ==> \ |
neuper@37906 | 70 |
\a + b / c = (a * c + b) / c" |
neuper@37906 | 71 |
rat_add3_assoc "[| a is_const; b is_const; c is_const |] ==> \ |
neuper@37906 | 72 |
\a + (b / c + e) = (a * c + b) / c + e" |
neuper@37906 | 73 |
|
neuper@37906 | 74 |
|
neuper@37906 | 75 |
|
neuper@37906 | 76 |
end |