(* (c) by Richard Lang

   theory collecting all knowledge 

   (predicates 'is_rootEq_in', 'is_sqrt_in', 'is_ratEq_in')

   for PolynomialEquations.

   alternative dependencies see Isac.thy

   created by: rlang 

         date: 02.07

   changed by: rlang

   last change by: rlang

             date: 02.11.26

   (c) Richard Lang, 2003

*)

(* remove_thy"PolyEq";

   use_thy"knowledge/Isac";

   use_thy"knowledge/PolyEq";

   remove_thy"PolyEq";

   use_thy"Isac";

   use"ROOT.ML";

   cd"knowledge";

   *)

PolyEq = LinEq + RootRatEq + 

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

consts

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

  Complete'_square

             :: "[bool,real, \

		  \ bool list] => bool list"

               ("((Script Complete'_square (_ _ =))// \

                 \ (_))" 9)

 (*----- poly ----- *)	 

  Normalize'_poly

             :: "[bool,real, \

		  \ bool list] => bool list"

               ("((Script Normalize'_poly (_ _=))// \

                 \ (_))" 9)

  Solve'_d0'_poly'_equation

             :: "[bool,real, \

		  \ bool list] => bool list"

               ("((Script Solve'_d0'_poly'_equation (_ _ =))// \

                 \ (_))" 9)

  Solve'_d1'_poly'_equation

             :: "[bool,real, \

		  \ bool list] => bool list"

               ("((Script Solve'_d1'_poly'_equation (_ _ =))// \

                 \ (_))" 9)

  Solve'_d2'_poly'_equation

             :: "[bool,real, \

		  \ bool list] => bool list"

               ("((Script Solve'_d2'_poly'_equation (_ _ =))// \

                 \ (_))" 9)

  Solve'_d2'_poly'_sqonly'_equation

             :: "[bool,real, \

		  \ bool list] => bool list"

               ("((Script Solve'_d2'_poly'_sqonly'_equation (_ _ =))// \

                 \ (_))" 9)

  Solve'_d2'_poly'_bdvonly'_equation

             :: "[bool,real, \

		  \ bool list] => bool list"

               ("((Script Solve'_d2'_poly'_bdvonly'_equation (_ _ =))// \

                 \ (_))" 9)

  Solve'_d2'_poly'_pq'_equation

             :: "[bool,real, \

		  \ bool list] => bool list"

               ("((Script Solve'_d2'_poly'_pq'_equation (_ _ =))// \

                 \ (_))" 9)

  Solve'_d2'_poly'_abc'_equation

             :: "[bool,real, \

		  \ bool list] => bool list"

               ("((Script Solve'_d2'_poly'_abc'_equation (_ _ =))// \

                 \ (_))" 9)

  Solve'_d3'_poly'_equation

             :: "[bool,real, \

		  \ bool list] => bool list"

               ("((Script Solve'_d3'_poly'_equation (_ _ =))// \

                 \ (_))" 9)

  Solve'_d4'_poly'_equation

             :: "[bool,real, \

		  \ bool list] => bool list"

               ("((Script Solve'_d4'_poly'_equation (_ _ =))// \

                 \ (_))" 9)

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

rules 

  cancel_leading_coeff1 "Not (c =!= 0) ==> (a + b*bdv + c*bdv^^^2 = 0) = \

			\                  (a/c + b/c*bdv + bdv^^^2 = 0)"

  cancel_leading_coeff2 "Not (c =!= 0) ==> (a - b*bdv + c*bdv^^^2 = 0) = \

			\                  (a/c - b/c*bdv + bdv^^^2 = 0)"

  cancel_leading_coeff3 "Not (c =!= 0) ==> (a + b*bdv - c*bdv^^^2 = 0) = \

			\                  (a/c + b/c*bdv - bdv^^^2 = 0)"

  cancel_leading_coeff4 "Not (c =!= 0) ==> (a +   bdv + c*bdv^^^2 = 0) = \

			\                  (a/c + 1/c*bdv + bdv^^^2 = 0)"

  cancel_leading_coeff5 "Not (c =!= 0) ==> (a -   bdv + c*bdv^^^2 = 0) = \

			\                  (a/c - 1/c*bdv + bdv^^^2 = 0)"

  cancel_leading_coeff6 "Not (c =!= 0) ==> (a +   bdv - c*bdv^^^2 = 0) = \

			\                  (a/c + 1/c*bdv - bdv^^^2 = 0)"

  cancel_leading_coeff7 "Not (c =!= 0) ==> (    b*bdv + c*bdv^^^2 = 0) = \

			\                  (    b/c*bdv + bdv^^^2 = 0)"

  cancel_leading_coeff8 "Not (c =!= 0) ==> (    b*bdv - c*bdv^^^2 = 0) = \

			\                  (    b/c*bdv - bdv^^^2 = 0)"

  cancel_leading_coeff9 "Not (c =!= 0) ==> (      bdv + c*bdv^^^2 = 0) = \

			\                  (      1/c*bdv + bdv^^^2 = 0)"

  cancel_leading_coeff10"Not (c =!= 0) ==> (      bdv - c*bdv^^^2 = 0) = \

			\                  (      1/c*bdv - bdv^^^2 = 0)"

  cancel_leading_coeff11"Not (c =!= 0) ==> (a +      b*bdv^^^2 = 0) = \

			\                  (a/b +      bdv^^^2 = 0)"

  cancel_leading_coeff12"Not (c =!= 0) ==> (a -      b*bdv^^^2 = 0) = \

			\                  (a/b -      bdv^^^2 = 0)"

  cancel_leading_coeff13"Not (c =!= 0) ==> (         b*bdv^^^2 = 0) = \

			\                  (           bdv^^^2 = 0/b)"

  complete_square1      "(q + p*bdv + bdv^^^2 = 0) = \

		        \(q + (p/2 + bdv)^^^2 = (p/2)^^^2)"

  complete_square2      "(    p*bdv + bdv^^^2 = 0) = \

		        \(    (p/2 + bdv)^^^2 = (p/2)^^^2)"

  complete_square3      "(      bdv + bdv^^^2 = 0) = \

		        \(    (1/2 + bdv)^^^2 = (1/2)^^^2)"

  complete_square4      "(q - p*bdv + bdv^^^2 = 0) = \

		        \(q + (p/2 - bdv)^^^2 = (p/2)^^^2)"

  complete_square5      "(q + p*bdv - bdv^^^2 = 0) = \

		        \(q + (p/2 - bdv)^^^2 = (p/2)^^^2)"

  square_explicit1      "(a + b^^^2 = c) = ( b^^^2 = c - a)"

  square_explicit2      "(a - b^^^2 = c) = (-(b^^^2) = c - a)"

  bdv_explicit1         "(a + bdv = b) = (bdv = - a + b)"

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

  bdv_explicit3         "((-1)*bdv = b) = (bdv = (-1)*b)"

  plus_leq              "(0 <= a + b) = ((-1)*b <= a)"(*Isa?*)

  minus_leq             "(0 <= a - b) = (     b <= a)"(*Isa?*)

(*-- normalize --*)

  all_left

    "[|Not(b=!=0)|] ==> (a = b) = (a - 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"

(* ---- degree 0 ----*)

  d0_true

  "(0=0) = True"

  d0_false

  "[|Not(bdv occurs_in a);Not(a=!=0)|] ==> (a=0) = False"

(* ---- degree 1 ----*)

  d1_isolate_add1

   "[|Not(bdv occurs_in a)|] ==> (a + b*bdv = 0) = (b*bdv = -a)"

  d1_isolate_add2

   "[|Not(bdv occurs_in a)|] ==> (a +   bdv = 0) = (  bdv = -a)"

  d1_isolate_div

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

(* ---- degree 2 ----*)

  d2_isolate_add1

   "[|Not(bdv occurs_in a)|] ==> (a + b*bdv^^^2=0) = (b*bdv^^^2= -a)"

  d2_isolate_add2

   "[|Not(bdv occurs_in a)|] ==> (a +   bdv^^^2=0) = (  bdv^^^2= -a)"

  d2_isolate_div

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

  d2_prescind1

   "(a*bdv + b*bdv^^^2 = 0) = (bdv*(a +b*bdv)=0)"

  d2_prescind2

   "(a*bdv +   bdv^^^2 = 0) = (bdv*(a +  bdv)=0)"

  d2_prescind3

   "(  bdv + b*bdv^^^2 = 0) = (bdv*(1+b*bdv)=0)"

  d2_prescind4

   "(  bdv +   bdv^^^2 = 0) = (bdv*(1+  bdv)=0)"

  (* eliminate degree 2 *)

  d2_sqrt_equation1

  "[|(0<=c)|] ==> (bdv^^^2=c) = ((bdv=sqrt c) | (bdv=-sqrt c ))"

  d2_sqrt_equation2

  "(bdv^^^2=0) = (bdv=0)"

  d2_sqrt_equation3

  "(b*bdv^^^2=0) = (bdv=0)"

  d2_reduce_equation1

  "(bdv*(a +b*bdv)=0) = ((bdv=0)|(a+b*bdv=0))"

  d2_reduce_equation2

  "(bdv*(a +  bdv)=0) = ((bdv=0)|(a+  bdv=0))"

  d2_pqformula1

   "[|0<=p^^^2 - 4*q|] ==> (q+p*bdv+   bdv^^^2=0) =

           ((bdv= -(p/2) + sqrt(p^^^2 - 4*q)/2) 

          | (bdv= -(p/2) - sqrt(p^^^2 - 4*q)/2))"

  d2_pqformula2

   "[|0<=p^^^2 - 4*q|] ==> (q+p*bdv+1*bdv^^^2=0) = 

           ((bdv= -(p/2) + sqrt(p^^^2 - 4*q)/2) 

          | (bdv= -(p/2) - sqrt(p^^^2 - 4*q)/2))"

  d2_pqformula3

   "[|0<=1 - 4*q|] ==> (q+  bdv+   bdv^^^2=0) = 

           ((bdv= -(1/2) + sqrt(1 - 4*q)/2) 

          | (bdv= -(1/2) - sqrt(1 - 4*q)/2))"

  d2_pqformula4

   "[|0<=1 - 4*q|] ==> (q+  bdv+1*bdv^^^2=0) = 

           ((bdv= -(1/2) + sqrt(1 - 4*q)/2) 

          | (bdv= -(1/2) - sqrt(1 - 4*q)/2))"

  d2_pqformula5

   "[|0<=p^^^2 - 0|] ==> (  p*bdv+   bdv^^^2=0) =

           ((bdv= -(p/2) + sqrt(p^^^2 - 0)/2) 

          | (bdv= -(p/2) - sqrt(p^^^2 - 0)/2))"

  d2_pqformula6

   "[|0<=p^^^2 - 0|] ==> (  p*bdv+1*bdv^^^2=0) = 

           ((bdv= -(p/2) + sqrt(p^^^2 - 0)/2) 

          | (bdv= -(p/2) - sqrt(p^^^2 - 0)/2))"

  d2_pqformula7

   "[|0<=1 - 0|] ==> (    bdv+   bdv^^^2=0) = 

           ((bdv= -(1/2) + sqrt(1 - 0)/2) 

          | (bdv= -(1/2) - sqrt(1 - 0)/2))"

  d2_pqformula8

   "[|0<=1 - 4*q|] ==> (    bdv+1*bdv^^^2=0) = 

           ((bdv= -(1/2) + sqrt(1 - 4*q)/2) 

          | (bdv= -(1/2) - sqrt(1 - 4*q)/2))"

  d2_pqformula9

   "[|0<= - 4*q|] ==> (q+      1*bdv^^^2=0) = 

           ((bdv= 0 + sqrt(0 - 4*q)/2) 

          | (bdv= 0 - sqrt(0 - 4*q)/2))"

  d2_pqformula10

   "[|0<= - 4*q|] ==> (q+        bdv^^^2=0) = 

           ((bdv= 0 + sqrt(0 - 4*q)/2) 

          | (bdv= 0 - sqrt(0 - 4*q)/2))"

  d2_abcformula1

   "[|0<=b^^^2 - 4*a*c|] ==> (c + b*bdv+a*bdv^^^2=0) =

           ((bdv=( -b + sqrt(b^^^2 - 4*a*c))/(2*a)) 

          | (bdv=( -b - sqrt(b^^^2 - 4*a*c))/(2*a)))"

  d2_abcformula2

   "[|0<=1 - 4*a*c|]     ==> (c+    bdv+a*bdv^^^2=0) = 

           ((bdv=( -1 + sqrt(1 - 4*a*c))/(2*a)) 

          | (bdv=( -1 - sqrt(1 - 4*a*c))/(2*a)))"

  d2_abcformula3

   "[|0<=b^^^2 - 4*a*c|] ==> (c + b*bdv+  bdv^^^2=0) =

           ((bdv=( -b + sqrt(b^^^2 - 4*1*c))/(2*1)) 

          | (bdv=( -b - sqrt(b^^^2 - 4*1*c))/(2*1)))"

  d2_abcformula4

   "[|0<=b^^^2 - 4*a*c|] ==> (c +   bdv+  bdv^^^2=0) =

           ((bdv=( -b + sqrt(1 - 4*1*c))/(2*1)) 

          | (bdv=( -b - sqrt(1 - 4*1*c))/(2*1)))"

  d2_abcformula5

   "[|0<=b^^^2 - 4*a*c|] ==> (c +        a*bdv^^^2=0) =

           ((bdv=( 0 + sqrt(0 - 4*a*c))/(2*a)) 

          | (bdv=( 0 - sqrt(0 - 4*a*c))/(2*a)))"

  d2_abcformula6

   "[|0<=1 - 4*a*c|]     ==> (c+          bdv^^^2=0) = 

           ((bdv=( 0 + sqrt(0 - 4*1*c))/(2*1)) 

          | (bdv=( 0 - sqrt(0 - 4*1*c))/(2*1)))"

  d2_abcformula7

   "[|0<=1 - 4*a*c|]     ==> (    b*bdv+a*bdv^^^2=0) = 

           ((bdv=( -b + sqrt(b^^^2 - 0))/(2*a)) 

          | (bdv=( -b - sqrt(b^^^2 - 0))/(2*a)))"

  d2_abcformula8

   "[|0<=b^^^2 - 4*a*c|] ==> (    b*bdv+  bdv^^^2=0) =

           ((bdv=( -b + sqrt(b^^^2 - 0))/(2*1)) 

          | (bdv=( -b - sqrt(b^^^2 - 0))/(2*1)))"

  d2_abcformula9

   "[|0<=1 - 4*a*c|]     ==> (      bdv+a*bdv^^^2=0) = 

           ((bdv=( -1 + sqrt(1 - 0))/(2*a)) 

          | (bdv=( -1 - sqrt(1 - 0))/(2*a)))"

  d2_abcformula10

   "[|0<=b^^^2 - 4*a*c|] ==> (      bdv+  bdv^^^2=0) =

           ((bdv=( -1 + sqrt(1 - 0))/(2*1)) 

          | (bdv=( -1 - sqrt(1 - 0))/(2*1)))"

(* ---- degree 3 ----*)

  d3_reduce_equation1

  "(a*bdv + b*bdv^^^2 + c*bdv^^^3=0) = (bdv=0 | (a + b*bdv + c*bdv^^^2=0))"

  d3_reduce_equation2

  "(  bdv + b*bdv^^^2 + c*bdv^^^3=0) = (bdv=0 | (1 + b*bdv + c*bdv^^^2=0))"

  d3_reduce_equation3

  "(a*bdv +   bdv^^^2 + c*bdv^^^3=0) = (bdv=0 | (a +   bdv + c*bdv^^^2=0))"

  d3_reduce_equation4

  "(  bdv +   bdv^^^2 + c*bdv^^^3=0) = (bdv=0 | (1 +   bdv + c*bdv^^^2=0))"

  d3_reduce_equation5

  "(a*bdv + b*bdv^^^2 +   bdv^^^3=0) = (bdv=0 | (a + b*bdv +   bdv^^^2=0))"

  d3_reduce_equation6

  "(  bdv + b*bdv^^^2 +   bdv^^^3=0) = (bdv=0 | (1 + b*bdv +   bdv^^^2=0))"

  d3_reduce_equation7

  "(a*bdv +   bdv^^^2 +   bdv^^^3=0) = (bdv=0 | (1 +   bdv +   bdv^^^2=0))"

  d3_reduce_equation8

  "(  bdv +   bdv^^^2 +   bdv^^^3=0) = (bdv=0 | (1 +   bdv +   bdv^^^2=0))"

  d3_reduce_equation9

  "(a*bdv             + c*bdv^^^3=0) = (bdv=0 | (a         + c*bdv^^^2=0))"

  d3_reduce_equation10

  "(  bdv             + c*bdv^^^3=0) = (bdv=0 | (1         + c*bdv^^^2=0))"

  d3_reduce_equation11

  "(a*bdv             +   bdv^^^3=0) = (bdv=0 | (a         +   bdv^^^2=0))"

  d3_reduce_equation12

  "(  bdv             +   bdv^^^3=0) = (bdv=0 | (1         +   bdv^^^2=0))"

  d3_reduce_equation13

  "(        b*bdv^^^2 + c*bdv^^^3=0) = (bdv=0 | (    b*bdv + c*bdv^^^2=0))"

  d3_reduce_equation14

  "(          bdv^^^2 + c*bdv^^^3=0) = (bdv=0 | (      bdv + c*bdv^^^2=0))"

  d3_reduce_equation15

  "(        b*bdv^^^2 +   bdv^^^3=0) = (bdv=0 | (    b*bdv +   bdv^^^2=0))"

  d3_reduce_equation16

  "(          bdv^^^2 +   bdv^^^3=0) = (bdv=0 | (      bdv +   bdv^^^2=0))"

  d3_isolate_add1

  "[|Not(bdv occurs_in a)|] ==> (a + b*bdv^^^3=0) = (b*bdv^^^3= (-1)*a)"

  d3_isolate_add2

  "[|Not(bdv occurs_in a)|] ==> (a +   bdv^^^3=0) = (  bdv^^^3= (-1)*a)"

  d3_isolate_div

   "[|Not(b=0);Not(bdv occurs_in a)|] ==> (b*bdv^^^3=c) = (bdv^^^3=c/b)"

  d3_root_equation2

  "(bdv^^^3=0) = (bdv=0)"

  d3_root_equation1

  "(bdv^^^3=c) = (bdv = nroot 3 c)"

(* ---- degree 4 ----*)

 (* FIXME es wir nicht getestet ob u>0 *)

 d4_sub_u1

 "(c+b*bdv^^^2+a*bdv^^^4=0) =

   ((a*u^^^2+b*u+c=0) & (bdv^^^2=u))"

(* ---- 7.3.02 von Termorder ---- *)

  bdv_collect_1       "l * bdv + m * bdv = (l + m) * bdv"

  bdv_collect_2       "bdv + m * bdv = (1 + m) * bdv"

  bdv_collect_3       "l * bdv + bdv = (l + 1) * bdv"

(*  bdv_collect_assoc0_1 "l * bdv + m * bdv + k = (l + m) * bdv + k"

    bdv_collect_assoc0_2 "bdv + m * bdv + k = (1 + m) * bdv + k"

    bdv_collect_assoc0_3 "l * bdv + bdv + k = (l + 1) * bdv + k"

*)

  bdv_collect_assoc1_1 "l * bdv + (m * bdv + k) = (l + m) * bdv + k"

  bdv_collect_assoc1_2 "bdv + (m * bdv + k) = (1 + m) * bdv + k"

  bdv_collect_assoc1_3 "l * bdv + (bdv + k) = (l + 1) * bdv + k"

  bdv_collect_assoc2_1 "k + l * bdv + m * bdv = k + (l + m) * bdv"

  bdv_collect_assoc2_2 "k + bdv + m * bdv = k + (1 + m) * bdv"

  bdv_collect_assoc2_3 "k + l * bdv + bdv = k + (l + 1) * bdv"

  bdv_n_collect_1      "l * bdv^^^n + m * bdv^^^n = (l + m) * bdv^^^n"

  bdv_n_collect_2      " bdv^^^n + m * bdv^^^n = (1 + m) * bdv^^^n"

  bdv_n_collect_3      "l * bdv^^^n + bdv^^^n = (l + 1) * bdv^^^n"   (*order!*)

  bdv_n_collect_assoc1_1 "l * bdv^^^n + (m * bdv^^^n + k) = (l + m) * bdv^^^n + k"

  bdv_n_collect_assoc1_2 "bdv^^^n + (m * bdv^^^n + k) = (1 + m) * bdv^^^n + k"

  bdv_n_collect_assoc1_3 "l * bdv^^^n + (bdv^^^n + k) = (l + 1) * bdv^^^n + k"

  bdv_n_collect_assoc2_1 "k + l * bdv^^^n + m * bdv^^^n = k + (l + m) * bdv^^^n"

  bdv_n_collect_assoc2_2 "k + bdv^^^n + m * bdv^^^n = k + (1 + m) * bdv^^^n"

  bdv_n_collect_assoc2_3 "k + l * bdv^^^n + bdv^^^n = k + (l + 1) * bdv^^^n"

(*WN.14.3.03*)

  real_minus_div         "- (a / b) = (-1 * a) / b"

  separate_bdv           "(a * bdv) / b = (a / b) * bdv"

  separate_bdv_n         "(a * bdv ^^^ n) / b = (a / b) * bdv ^^^ n"

  separate_1_bdv         "bdv / b = (1 / b) * bdv"

  separate_1_bdv_n       "bdv ^^^ n / b = (1 / b) * bdv ^^^ n"

end