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

 (* collecting all knowledge for Root Equations

    created by: rlang 

          date: 02.08

    changed by: rlang

    last change by: rlang

              date: 02.11.14

 *)

 (*  use"../knowledge/RootEq.ML";

    use"knowledge/RootEq.ML";

    use"RootEq.ML";

    remove_thy"RootEq";

    use_thy"Isac";

    use"ROOT.ML";

    cd"knowledge";

  *)

 RootEq = Root + 

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

 consts

   (*-------------------------root-----------------------*)

   is'_rootTerm'_in :: [real, real] => bool ("_ is'_rootTerm'_in _") 

   is'_sqrtTerm'_in :: [real, real] => bool ("_ is'_sqrtTerm'_in _") 

   is'_normSqrtTerm'_in :: [real, real] => bool ("_ is'_normSqrtTerm'_in _") 

   (*----------------------scripts-----------------------*)

   Norm'_sq'_root'_equation

              :: "[bool,real, \

 		  \ bool list] => bool list"

                ("((Script Norm'_sq'_root'_equation (_ _ =))// \

                  \ (_))" 9)

   Solve'_sq'_root'_equation

              :: "[bool,real, \

 		  \ bool list] => bool list"

                ("((Script Solve'_sq'_root'_equation (_ _ =))// \

                  \ (_))" 9)

   Solve'_left'_sq'_root'_equation

              :: "[bool,real, \

 		  \ bool list] => bool list"

                ("((Script Solve'_left'_sq'_root'_equation (_ _ =))// \

                  \ (_))" 9)

   Solve'_right'_sq'_root'_equation

              :: "[bool,real, \

 		  \ bool list] => bool list"

                ("((Script Solve'_right'_sq'_root'_equation (_ _ =))// \

                  \ (_))" 9)

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

 rules 

 (* normalize *)

   makex1_x

     "a^^^1  = a"  

   real_assoc_1

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

   real_assoc_2

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

   (* simplification of root*)

   sqrt_square_1

   "[|0 <= a|] ==>  (sqrt a)^^^2 = a"

   sqrt_square_2

    "sqrt (a ^^^ 2) = a"

   sqrt_times_root_1

    "sqrt a * sqrt b = sqrt(a*b)"

   sqrt_times_root_2

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

   (* isolate one root on the LEFT or RIGHT hand side of the equation *)

   sqrt_isolate_l_add1

   "[|bdv occurs_in c|] ==> (a + b*sqrt(c) = d) = (b * sqrt(c) = d+ (-1) * a)"

   sqrt_isolate_l_add2

   "[|bdv occurs_in c|] ==>(a + sqrt(c) = d) = ((sqrt(c) = d+ (-1) * a))"

   sqrt_isolate_l_add3

   "[|bdv occurs_in c|] ==> (a + b*(e/sqrt(c)) = d) = (b * (e/sqrt(c)) = d+ (-1) * a)"

   sqrt_isolate_l_add4

   "[|bdv occurs_in c|] ==>(a + b/(f*sqrt(c)) = d) = (b / (f*sqrt(c)) = d+ (-1) * a)"

   sqrt_isolate_l_add5

   "[|bdv occurs_in c|] ==> (a + b*(e/(f*sqrt(c))) = d) = (b * (e/(f*sqrt(c))) = d+ (-1) * a)"

   sqrt_isolate_l_add6

   "[|bdv occurs_in c|] ==>(a + b/sqrt(c) = d) = (b / sqrt(c) = d+ (-1) * a)"

   sqrt_isolate_r_add1

   "[|bdv occurs_in f|] ==>(a = d + e*sqrt(f)) = (a + (-1) * d = e*sqrt(f))"

   sqrt_isolate_r_add2

   "[|bdv occurs_in f|] ==>(a = d + sqrt(f)) = (a + (-1) * d = sqrt(f))"

  (* small hack: thm 3,5,6 are not needed if rootnormalize is well done*)

   sqrt_isolate_r_add3

   "[|bdv occurs_in f|] ==>(a = d + e*(g/sqrt(f))) = (a + (-1) * d = e*(g/sqrt(f)))"

   sqrt_isolate_r_add4

   "[|bdv occurs_in f|] ==>(a = d + g/sqrt(f)) = (a + (-1) * d = g/sqrt(f))"

   sqrt_isolate_r_add5

   "[|bdv occurs_in f|] ==>(a = d + e*(g/(h*sqrt(f)))) = (a + (-1) * d = e*(g/(h*sqrt(f))))"

   sqrt_isolate_r_add6

   "[|bdv occurs_in f|] ==>(a = d + g/(h*sqrt(f))) = (a + (-1) * d = g/(h*sqrt(f)))"

   (* eliminate isolates sqrt *)

   sqrt_square_equation_both_1

   "[|bdv occurs_in b; bdv occurs_in d|] ==> 

                ( (sqrt a + sqrt b         = sqrt c + sqrt d) = 

                  (a+2*sqrt(a)*sqrt(b)+b  = c+2*sqrt(c)*sqrt(d)+d))"

   sqrt_square_equation_both_2

   "[|bdv occurs_in b; bdv occurs_in d|] ==> 

                ( (sqrt a - sqrt b           = sqrt c + sqrt d) = 

                  (a - 2*sqrt(a)*sqrt(b)+b  = c+2*sqrt(c)*sqrt(d)+d))"

   sqrt_square_equation_both_3

   "[|bdv occurs_in b; bdv occurs_in d|] ==> 

                ( (sqrt a + sqrt b           = sqrt c - sqrt d) = 

                  (a + 2*sqrt(a)*sqrt(b)+b  = c - 2*sqrt(c)*sqrt(d)+d))"

   sqrt_square_equation_both_4

   "[|bdv occurs_in b; bdv occurs_in d|] ==> 

                ( (sqrt a - sqrt b           = sqrt c - sqrt d) = 

                  (a - 2*sqrt(a)*sqrt(b)+b  = c - 2*sqrt(c)*sqrt(d)+d))"

   sqrt_square_equation_left_1

   "[|bdv occurs_in a; 0 <= a; 0 <= b|] ==> ( (sqrt (a) = b) = (a = (b^^^2)))"

   sqrt_square_equation_left_2

   "[|bdv occurs_in a; 0 <= a; 0 <= b*c|] ==> ( (c*sqrt(a) = b) = (c^^^2*a = b^^^2))"

   sqrt_square_equation_left_3

   "[|bdv occurs_in a; 0 <= a; 0 <= b*c|] ==> ( c/sqrt(a) = b) = (c^^^2 / a = b^^^2)"

   (* small hack: thm 4-6 are not needed if rootnormalize is well done*)

   sqrt_square_equation_left_4

   "[|bdv occurs_in a; 0 <= a; 0 <= b*c*d|] ==> ( (c*(d/sqrt (a)) = b) = (c^^^2*(d^^^2/a) = b^^^2))"

   sqrt_square_equation_left_5

   "[|bdv occurs_in a; 0 <= a; 0 <= b*c*d|] ==> ( c/(d*sqrt(a)) = b) = (c^^^2 / (d^^^2*a) = b^^^2)"

   sqrt_square_equation_left_6

   "[|bdv occurs_in a; 0 <= a; 0 <= b*c*d*e|] ==> ( (c*(d/(e*sqrt (a))) = b) = (c^^^2*(d^^^2/(e^^^2*a)) = b^^^2))"

   sqrt_square_equation_right_1

   "[|bdv occurs_in b; 0 <= a; 0 <= b|] ==> ( (a = sqrt (b)) = (a^^^2 = b))"

   sqrt_square_equation_right_2

   "[|bdv occurs_in b; 0 <= a*c; 0 <= b|] ==> ( (a = c*sqrt (b)) = ((a^^^2) = c^^^2*b))"

   sqrt_square_equation_right_3

   "[|bdv occurs_in b; 0 <= a*c; 0 <= b|] ==> ( (a = c/sqrt (b)) = (a^^^2 = c^^^2/b))"

  (* small hack: thm 4-6 are not needed if rootnormalize is well done*)

   sqrt_square_equation_right_4

   "[|bdv occurs_in b; 0 <= a*c*d; 0 <= b|] ==> ( (a = c*(d/sqrt (b))) = ((a^^^2) = c^^^2*(d^^^2/b)))"

   sqrt_square_equation_right_5

   "[|bdv occurs_in b; 0 <= a*c*d; 0 <= b|] ==> ( (a = c/(d*sqrt (b))) = (a^^^2 = c^^^2/(d^^^2*b)))"

   sqrt_square_equation_right_6

   "[|bdv occurs_in b; 0 <= a*c*d*e; 0 <= b|] ==> ( (a = c*(d/(e*sqrt (b)))) = ((a^^^2) = c^^^2*(d^^^2/(e^^^2*b))))"

 end