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