neuper@37906: (*.c) by Richard Lang, 2003 .*)
neuper@37906: (* collecting all knowledge for Root and Rational Equations
neuper@37906:    created by: rlang 
neuper@37906:          date: 02.10
neuper@37906:    changed by: rlang
neuper@37906:    last change by: rlang
neuper@37906:              date: 02.11.04
neuper@37906: *)
neuper@37906: 
neuper@37906: (* use"knowledge/RootRatEq.ML";
neuper@37906:    use"RootRatEq.ML";
neuper@37906: 
neuper@37906:    use"ROOT.ML";
neuper@37906:    cd"knowledge";
neuper@37906: 
neuper@37906:    remove_thy"RootRatEq";
neuper@37906:    use_thy"Isac";
neuper@37906:    *)
neuper@37906: 
neuper@37906: RootRatEq = RootEq + RatEq + RootRat + 
neuper@37906: 
neuper@37906: (*-------------------- consts-----------------------------------------------*)
neuper@37906: consts
neuper@37906: 
neuper@37906:   is'_rootRatAddTerm'_in :: [real, real] => bool ("_ is'_rootRatAddTerm'_in _") (*RL DA*)
neuper@37906: 
neuper@37906: (*---------scripts--------------------------*)
neuper@37906:   Elim'_rootrat'_equation
neuper@37906:              :: "[bool,real, \
neuper@37906: 		  \ bool list] => bool list"
neuper@37906:                ("((Script Elim'_rootrat'_equation (_ _ =))// \
neuper@37906:                  \ (_))" 9)
neuper@37906:  (*-------------------- rules------------------------------------------------*)
neuper@37906: rules
neuper@37906: 
neuper@37906:   (* eliminate ratRootTerm *)
neuper@37906:   rootrat_equation_left_1
neuper@37906:    "[|c is_rootTerm_in bdv|] ==> ( (a + b/c = d) = ( b = (d - a) * c ))"
neuper@37906:   rootrat_equation_left_2
neuper@37906:    "[|c is_rootTerm_in bdv|] ==> ( (b/c = d) = ( b = d * c ))"
neuper@37906:   rootrat_equation_right_2
neuper@37906:    "[|f is_rootTerm_in bdv|] ==> ( (a = d + e/f) = ( (a - d) * f = e ))"
neuper@37906:   rootrat_equation_right_1
neuper@37906:    "[|f is_rootTerm_in bdv|] ==> ( (a = e/f) = ( a * f = e ))"
neuper@37906: 
neuper@37906: 
neuper@37906: 
neuper@37906: end