(*.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