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

(* theory collecting all knowledge for LinearEquations

   created by: rlang 

         date: 02.10

   changed by: rlang

   last change by: rlang

             date: 02.10.20

*)

(*

 use"knowledge/LinEq.ML";

 use"LinEq.ML";

 use"ROOT.ML";

 cd"knowledge";

*)

LinEq = Poly + Equation +

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

consts

   Solve'_lineq'_equation

             :: "[bool,real, \

		  \ bool list] => bool list"

               ("((Script Solve'_lineq'_equation (_ _ =))// \

                 \ (_))" 9)

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

rules

(*-- normalize --*)

  (*WN0509 compare PolyEq.all_left "[|Not(b=!=0)|] ==> (a = b) = (a - b = 0)"*)

  all_left

    "[|Not(b=!=0)|] ==> (a=b) = (a+(-1)*b=0)"

  makex1_x

    "a^^^1  = a"  

  real_assoc_1

   "a+(b+c) = a+b+c"

  real_assoc_2

   "a*(b*c) = a*b*c"

(*-- solve --*)

  lin_isolate_add1

   "(a + b*bdv = 0) = (b*bdv = (-1)*a)"

  lin_isolate_add2

   "(a +   bdv = 0) = (  bdv = (-1)*a)"

  lin_isolate_div

   "[|Not(b=0)|] ==> (b*bdv = c) = (bdv = c / b)"

end