1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/Tools/isac/Knowledge/RootRatEq.thy	Wed Aug 25 16:20:07 2010 +0200
     1.3 @@ -0,0 +1,48 @@
     1.4 +(*.c) by Richard Lang, 2003 .*)
     1.5 +(* collecting all knowledge for Root and Rational Equations
     1.6 +   created by: rlang 
     1.7 +         date: 02.10
     1.8 +   changed by: rlang
     1.9 +   last change by: rlang
    1.10 +             date: 02.11.04
    1.11 +*)
    1.12 +
    1.13 +(* use"knowledge/RootRatEq.ML";
    1.14 +   use"RootRatEq.ML";
    1.15 +
    1.16 +   use"ROOT.ML";
    1.17 +   cd"knowledge";
    1.18 +
    1.19 +   remove_thy"RootRatEq";
    1.20 +   use_thy"Isac";
    1.21 +   *)
    1.22 +
    1.23 +RootRatEq = RootEq + RatEq + RootRat + 
    1.24 +
    1.25 +(*-------------------- consts-----------------------------------------------*)
    1.26 +consts
    1.27 +
    1.28 +  is'_rootRatAddTerm'_in :: [real, real] => bool ("_ is'_rootRatAddTerm'_in _") (*RL DA*)
    1.29 +
    1.30 +(*---------scripts--------------------------*)
    1.31 +  Elim'_rootrat'_equation
    1.32 +             :: "[bool,real, \
    1.33 +		  \ bool list] => bool list"
    1.34 +               ("((Script Elim'_rootrat'_equation (_ _ =))// \
    1.35 +                 \ (_))" 9)
    1.36 + (*-------------------- rules------------------------------------------------*)
    1.37 +rules
    1.38 +
    1.39 +  (* eliminate ratRootTerm *)
    1.40 +  rootrat_equation_left_1
    1.41 +   "[|c is_rootTerm_in bdv|] ==> ( (a + b/c = d) = ( b = (d - a) * c ))"
    1.42 +  rootrat_equation_left_2
    1.43 +   "[|c is_rootTerm_in bdv|] ==> ( (b/c = d) = ( b = d * c ))"
    1.44 +  rootrat_equation_right_2
    1.45 +   "[|f is_rootTerm_in bdv|] ==> ( (a = d + e/f) = ( (a - d) * f = e ))"
    1.46 +  rootrat_equation_right_1
    1.47 +   "[|f is_rootTerm_in bdv|] ==> ( (a = e/f) = ( a * f = e ))"
    1.48 +
    1.49 +
    1.50 +
    1.51 +end