1 (*.(c) by Richard Lang, 2003 .*)
2 (* theory collecting all knowledge for RationalEquations
12 use_thy"knowledge/RatEq";
24 (*-------------------- consts------------------------------------------------*)
27 is'_ratequation'_in :: "[bool, real] => bool" ("_ is'_ratequation'_in _")
29 (*----------------------scripts-----------------------*)
32 \ bool list] => bool list"
33 ("((Script Solve'_rat'_equation (_ _ =))// \
36 (*-------------------- rules------------------------------------------------*)
38 (* FIXME also in Poly.thy def. --> FIXED*)
40 "a - b = a + (-1) * b"*)
44 "(a/b)*(c/d) = (a*c)/(b*d)"
48 "(a/b)^^^2 = a^^^2/b^^^2"
51 "[|Not(c=0); Not(d=0)|] ==> (a / (c/d) = (a*d) / c)"
53 "[|Not(b=0);Not(c=0); Not(d=0)|] ==> ((a/b) / (c/d) = (a*d) / (b*c))"
55 "[|Not(b=0);Not(c=0)|] ==> ((a/b) / c = a / (b*c))"
58 (* equation to same denominator *)
59 rat_mult_denominator_both
60 "[|Not(b=0); Not(d=0)|] ==> ((a::real) / b = c / d) = (a*d = c*b)"
61 rat_mult_denominator_left
62 "[|Not(d=0)|] ==> ((a::real) = c / d) = (a*d = c)"
63 rat_mult_denominator_right
64 "[|Not(b=0)|] ==> ((a::real) / b = c) = (a = c*b)"