(*.(c) by Richard Lang, 2003 .*)

 (* theory collecting all knowledge for RationalEquations

    created by: rlang 

          date: 02.08.12

    changed by: rlang

    last change by: rlang

              date: 02.11.28

 *)

 (*

    RL.020812

    use_thy"knowledge/RatEq";

    use_thy"RatEq";

    use_thy_only"RatEq";

    remove_thy"RatEq";

    use_thy"Isac";

    use"ROOT.ML";

    cd"knowledge";

  *)

 RatEq = Rational +

 (*-------------------- consts------------------------------------------------*)

 consts

   is'_ratequation'_in :: "[bool, real] => bool" ("_ is'_ratequation'_in _")

   (*----------------------scripts-----------------------*)

   Solve'_rat'_equation

              :: "[bool,real, \

 		  \ bool list] => bool list"

                ("((Script Solve'_rat'_equation (_ _ =))// \

                  \ (_))" 9)

 (*-------------------- rules------------------------------------------------*)

 rules 

    (* FIXME also in Poly.thy def. --> FIXED*)

    (*real_diff_minus            

    "a - b = a + (-1) * b"*)

    real_rat_mult_1

    "a*(b/c) = (a*b)/c"

    real_rat_mult_2

    "(a/b)*(c/d) = (a*c)/(b*d)"

    real_rat_mult_3

    "(a/b)*c = (a*c)/b"

    real_rat_pow

    "(a/b)^^^2 = a^^^2/b^^^2"

    rat_double_rat_1

    "[|Not(c=0); Not(d=0)|] ==> (a / (c/d) = (a*d) / c)"

    rat_double_rat_2

    "[|Not(b=0);Not(c=0); Not(d=0)|] ==> ((a/b) / (c/d) = (a*d) / (b*c))"

    rat_double_rat_3

    "[|Not(b=0);Not(c=0)|] ==> ((a/b) / c = a / (b*c))"

   (* equation to same denominator *)

   rat_mult_denominator_both

    "[|Not(b=0); Not(d=0)|] ==> ((a::real) / b = c / d) = (a*d = c*b)"

   rat_mult_denominator_left

    "[|Not(d=0)|] ==> ((a::real) = c / d) = (a*d = c)"

   rat_mult_denominator_right

    "[|Not(b=0)|] ==> ((a::real) / b = c) = (a = c*b)"

 end