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