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

 (* collecting all knowledge for Root and Rational Equations

    created by: rlang 

          date: 02.10

    changed by: rlang

    last change by: rlang

              date: 02.11.04

 *)

 (* use"knowledge/RootRatEq.ML";

    use"RootRatEq.ML";

    use"ROOT.ML";

    cd"knowledge";

    remove_thy"RootRatEq";

    use_thy"Isac";

    *)

 RootRatEq = RootEq + RatEq + RootRat + 

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

 consts

   is'_rootRatAddTerm'_in :: [real, real] => bool ("_ is'_rootRatAddTerm'_in _") (*RL DA*)

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

   Elim'_rootrat'_equation

              :: "[bool,real, \

 		  \ bool list] => bool list"

                ("((Script Elim'_rootrat'_equation (_ _ =))// \

                  \ (_))" 9)

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

 rules

   (* eliminate ratRootTerm *)

   rootrat_equation_left_1

    "[|c is_rootTerm_in bdv|] ==> ( (a + b/c = d) = ( b = (d - a) * c ))"

   rootrat_equation_left_2

    "[|c is_rootTerm_in bdv|] ==> ( (b/c = d) = ( b = d * c ))"

   rootrat_equation_right_2

    "[|f is_rootTerm_in bdv|] ==> ( (a = d + e/f) = ( (a - d) * f = e ))"

   rootrat_equation_right_1

    "[|f is_rootTerm_in bdv|] ==> ( (a = e/f) = ( a * f = e ))"

 end