wneuper/isa: src/Tools/isac/Knowledge/PolyEq.thy@509d70b507e5

     1 (* theory collecting all knowledge

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

     3    for PolynomialEquations.

     4    alternative dependencies see @{theory "Isac"}

     5    created by: rlang

     6          date: 02.07

     7    changed by: rlang

     8    last change by: rlang

     9              date: 03.06.03

    10    (c) by Richard Lang, 2003

    11 *)

    13 theory PolyEq imports LinEq RootRatEq begin

    15 consts

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

    18   Complete'_square

    19              :: "[bool,real,

    20 		   bool list] => bool list"

    21                ("((Script Complete'_square (_ _ =))// (_))" 9)

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

    23   Normalize'_poly

    24              :: "[bool,real,

    25 		   bool list] => bool list"

    26                ("((Script Normalize'_poly (_ _=))// (_))" 9)

    27   Solve'_d0'_polyeq'_equation

    28              :: "[bool,real,

    29 		   bool list] => bool list"

    30                ("((Script Solve'_d0'_polyeq'_equation (_ _ =))// (_))" 9)

    31   Solve'_d1'_polyeq'_equation

    32              :: "[bool,real,

    33 		   bool list] => bool list"

    34                ("((Script Solve'_d1'_polyeq'_equation (_ _ =))// (_))" 9)

    35   Solve'_d2'_polyeq'_equation

    36              :: "[bool,real,

    37 		   bool list] => bool list"

    38                ("((Script Solve'_d2'_polyeq'_equation (_ _ =))// (_))" 9)

    39   Solve'_d2'_polyeq'_sqonly'_equation

    40              :: "[bool,real,

    41 		   bool list] => bool list"

    42                ("((Script Solve'_d2'_polyeq'_sqonly'_equation (_ _ =))// (_))" 9)

    43   Solve'_d2'_polyeq'_bdvonly'_equation

    44              :: "[bool,real,

    45 		   bool list] => bool list"

    46                ("((Script Solve'_d2'_polyeq'_bdvonly'_equation (_ _ =))// (_))" 9)

    47   Solve'_d2'_polyeq'_pq'_equation

    48              :: "[bool,real,

    49 		   bool list] => bool list"

    50                ("((Script Solve'_d2'_polyeq'_pq'_equation (_ _ =))// (_))" 9)

    51   Solve'_d2'_polyeq'_abc'_equation

    52              :: "[bool,real,

    53 		   bool list] => bool list"

    54                ("((Script Solve'_d2'_polyeq'_abc'_equation (_ _ =))// (_))" 9)

    55   Solve'_d3'_polyeq'_equation

    56              :: "[bool,real,

    57 		   bool list] => bool list"

    58                ("((Script Solve'_d3'_polyeq'_equation (_ _ =))// (_))" 9)

    59   Solve'_d4'_polyeq'_equation

    60              :: "[bool,real,

    61 		   bool list] => bool list"

    62                ("((Script Solve'_d4'_polyeq'_equation (_ _ =))// (_))" 9)

    63   Biquadrat'_poly

    64              :: "[bool,real,

    65 		   bool list] => bool list"

    66                ("((Script Biquadrat'_poly (_ _=))// (_))" 9)

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

    69 (* type real enforced by op "^^^" *)

    70 axiomatization where

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

   100 			                   (           bdv^^^2 = 0/b)" and

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

   103 		         (q + (p/2 + bdv)^^^2 = (p/2)^^^2)" and

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

   105 		         (    (p/2 + bdv)^^^2 = (p/2)^^^2)" and

   106   complete_square3:      "(      bdv + bdv^^^2 = 0) =

   107 		         (    (1/2 + bdv)^^^2 = (1/2)^^^2)" and

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

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

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

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

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

   115   square_explicit2:      "(a - b^^^2 = c) = (-(b^^^2) = c - a)" and

   117   (*bdv_explicit* required type constrain to real in --- (-8 - 2*x + x^^^2 = 0),  by rewriting ---*)

   118   bdv_explicit1:         "(a + bdv = b) = (bdv = - a + (b::real))" and

   119   bdv_explicit2:         "(a - bdv = b) = ((-1)*bdv = - a + (b::real))" and

   120   bdv_explicit3:         "((-1)*bdv = b) = (bdv = (-1)*(b::real))" and

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

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

   125 (*-- normalise --*)

   126   (*WN0509 compare LinEq.all_left "[|Not(b=!=0)|] ==> (a=b) = (a+(-1)*b=0)"*)

   127   all_left:              "[|Not(b=!=0)|] ==> (a = b) = (a - b = 0)" and

   128   makex1_x:              "a^^^1  = a"   and

   129   real_assoc_1:          "a+(b+c) = a+b+c" and

   130   real_assoc_2:          "a*(b*c) = a*b*c" and

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

   133   d0_true:               "(0=0) = True" and

   134   d0_false:              "[|Not(bdv occurs_in a);Not(a=0)|] ==> (a=0) = False" and

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

   136   d1_isolate_add1:

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

   138   d1_isolate_add2:

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

   140   d1_isolate_div:

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

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

   143   d2_isolate_add1:

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

   145   d2_isolate_add2:

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

   147   d2_isolate_div:

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

   150   d2_prescind1:          "(a*bdv + b*bdv^^^2 = 0) = (bdv*(a +b*bdv)=0)" and

   151   d2_prescind2:          "(a*bdv +   bdv^^^2 = 0) = (bdv*(a +  bdv)=0)" and

   152   d2_prescind3:          "(  bdv + b*bdv^^^2 = 0) = (bdv*(1+b*bdv)=0)" and

   153   d2_prescind4:          "(  bdv +   bdv^^^2 = 0) = (bdv*(1+  bdv)=0)" and

   154   (* eliminate degree 2 *)

   155   (* thm for neg arguments in sqroot have postfix _neg *)

   156   d2_sqrt_equation1:     "[|(0<=c);Not(bdv occurs_in c)|] ==>

   157                          (bdv^^^2=c) = ((bdv=sqrt c) | (bdv=(-1)*sqrt c ))" and

   158  d2_sqrt_equation1_neg:

   159   "[|(c<0);Not(bdv occurs_in c)|] ==> (bdv^^^2=c) = False" and

   160   d2_sqrt_equation2:     "(bdv^^^2=0) = (bdv=0)" and

   161   d2_sqrt_equation3:     "(b*bdv^^^2=0) = (bdv=0)"

   162 axiomatization where (*AK..if replaced by "and" we get errors:

   163   exception PTREE "nth _ []" raised

   164   (line 783 of "/usr/local/isabisac/src/Tools/isac/Interpret/ctree.sml"):

   165     'fun nth _ []      = raise PTREE "nth _ []"'

   166 and

   167   exception Bind raised

   168   (line 1097 of "/usr/local/isabisac/test/Tools/isac/Frontend/interface.sml"):

   169     'val (Form f, tac, asms) = pt_extract (pt, p);' *)

   170   (* WN120315 these 2 thms need "::real", because no "^^^" constrains type as

   171      required in test --- rls d2_polyeq_bdv_only_simplify --- *)

   172   d2_reduce_equation1:   "(bdv*(a +b*bdv)=0) = ((bdv=0)|(a+b*bdv=(0::real)))" and

   173   d2_reduce_equation2:   "(bdv*(a +  bdv)=0) = ((bdv=0)|(a+  bdv=(0::real)))"

   175 axiomatization where (*..if replaced by "and" we get errors:

   176   exception PTREE "nth _ []" raised

   177   (line 783 of "/usr/local/isabisac/src/Tools/isac/Interpret/ctree.sml"):

   178     'fun nth _ []      = raise PTREE "nth _ []"'

   179 and

   180   exception Bind raised

   181   (line 1097 of "/usr/local/isabisac/test/Tools/isac/Frontend/interface.sml"):

   182     'val (Form f, tac, asms) = pt_extract (pt, p);' *)

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

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

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

   186   d2_pqformula1_neg:     "[|p^^^2 - 4*q<0|] ==> (q+p*bdv+   bdv^^^2=0) = False" and

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

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

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

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

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

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

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

   194   d2_pqformula3_neg:     "[|1 - 4*q<0|] ==> (q+  bdv+   bdv^^^2=0) = False" and

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

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

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

   198   d2_pqformula4_neg:     "[|1 - 4*q<0|] ==> (q+  bdv+1*bdv^^^2=0) = False" and

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

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

   201                           | (bdv= (-1)*(p/2) - sqrt(p^^^2 - 0)/2))" and

   202  (* d2_pqformula5_neg not need p^2 never less zero in R *)

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

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

   205                           | (bdv= (-1)*(p/2) - sqrt(p^^^2 - 0)/2))" and

   206   (* d2_pqformula6_neg not need p^2 never less zero in R *)

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

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

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

   210   (* d2_pqformula7_neg not need, because 1<0 ==> False*)

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

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

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

   214   (* d2_pqformula8_neg not need, because 1<0 ==> False*)

   215   d2_pqformula9:        "[|Not(bdv occurs_in q); 0<= (-1)*4*q|] ==>

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

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

   218   d2_pqformula9_neg:

   219    "[|Not(bdv occurs_in q); (-1)*4*q<0|] ==> (q+    1*bdv^^^2=0) = False" and

   220   d2_pqformula10:

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

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

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

   224   d2_pqformula10_neg:

   225    "[|Not(bdv occurs_in q); (-1)*4*q<0|] ==> (q+     bdv^^^2=0) = False" and

   226   d2_abcformula1:

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

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

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

   230   d2_abcformula1_neg:

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

   232   d2_abcformula2:

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

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

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

   236   d2_abcformula2_neg:

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

   238   d2_abcformula3:

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

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

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

   242   d2_abcformula3_neg:

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

   244   d2_abcformula4:

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

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

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

   248   d2_abcformula4_neg:

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

   250   d2_abcformula5:

   251    "[|Not(bdv occurs_in c); 0<=0 - 4*a*c|] ==> (c +  a*bdv^^^2=0) =

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

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

   254   d2_abcformula5_neg:

   255    "[|Not(bdv occurs_in c); 0 - 4*a*c<0|] ==> (c +  a*bdv^^^2=0) = False" and

   256   d2_abcformula6:

   257    "[|Not(bdv occurs_in c); 0<=0 - 4*1*c|]     ==> (c+    bdv^^^2=0) =

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

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

   260   d2_abcformula6_neg:

   261    "[|Not(bdv occurs_in c); 0 - 4*1*c<0|]     ==> (c+    bdv^^^2=0) = False" and

   262   d2_abcformula7:

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

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

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

   266   (* d2_abcformula7_neg not need b^2 never less zero in R *)

   267   d2_abcformula8:

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

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

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

   271   (* d2_abcformula8_neg not need b^2 never less zero in R *)

   272   d2_abcformula9:

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

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

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

   276   (* d2_abcformula9_neg not need, because 1<0 ==> False*)

   277   d2_abcformula10:

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

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

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

   281   (* d2_abcformula10_neg not need, because 1<0 ==> False*)

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

   285   d3_reduce_equation1:

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

   287   d3_reduce_equation2:

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

   289   d3_reduce_equation3:

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

   291   d3_reduce_equation4:

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

   293   d3_reduce_equation5:

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

   295   d3_reduce_equation6:

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

   297   d3_reduce_equation7:

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

   299   d3_reduce_equation8:

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

   301   d3_reduce_equation9:

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

   303   d3_reduce_equation10:

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

   305   d3_reduce_equation11:

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

   307   d3_reduce_equation12:

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

   309   d3_reduce_equation13:

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

   311   d3_reduce_equation14:

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

   313   d3_reduce_equation15:

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

   315   d3_reduce_equation16:

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

   317   d3_isolate_add1:

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

   319   d3_isolate_add2:

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

   321   d3_isolate_div:

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

   323   d3_root_equation2:

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

   325   d3_root_equation1:

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

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

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

   330  d4_sub_u1:

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

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

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

   336   bdv_collect_1:      "l * bdv + m * bdv = (l + m) * bdv" and

   337   bdv_collect_2:      "bdv + m * bdv = (1 + m) * bdv" and

   338   bdv_collect_3:      "l * bdv + bdv = (l + 1) * bdv" and

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

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

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

   343 *)

   344   bdv_collect_assoc1_1: "l * bdv + (m * bdv + k) = (l + m) * bdv + k" and

   345   bdv_collect_assoc1_2: "bdv + (m * bdv + k) = (1 + m) * bdv + k" and

   346   bdv_collect_assoc1_3: "l * bdv + (bdv + k) = (l + 1) * bdv + k" and

   348   bdv_collect_assoc2_1: "k + l * bdv + m * bdv = k + (l + m) * bdv" and

   349   bdv_collect_assoc2_2: "k + bdv + m * bdv = k + (1 + m) * bdv" and

   350   bdv_collect_assoc2_3: "k + l * bdv + bdv = k + (l + 1) * bdv" and

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

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

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

   357   bdv_n_collect_assoc1_1:

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

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

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

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

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

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

   366 (*WN.14.3.03*)

   367   real_minus_div:         "- (a / b) = (-1 * a) / b" and

   369   separate_bdv:           "(a * bdv) / b = (a / b) * (bdv::real)" and

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

   371   separate_1_bdv:         "bdv / b = (1 / b) * (bdv::real)" and

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

   374 ML {*

   375 val thy = @{theory};

   377 (*-------------------------rulse-------------------------*)

   378 val PolyEq_prls = (*3.10.02:just the following order due to subterm evaluation*)

   379   Celem.append_rls "PolyEq_prls" Celem.e_rls

   380 	     [Celem.Calc ("Atools.ident",eval_ident "#ident_"),

   381 	      Celem.Calc ("Tools.matches",eval_matches ""),

   382 	      Celem.Calc ("Tools.lhs"    ,eval_lhs ""),

   383 	      Celem.Calc ("Tools.rhs"    ,eval_rhs ""),

   384 	      Celem.Calc ("Poly.is'_expanded'_in",eval_is_expanded_in ""),

   385 	      Celem.Calc ("Poly.is'_poly'_in",eval_is_poly_in ""),

   386 	      Celem.Calc ("Poly.has'_degree'_in",eval_has_degree_in ""),

   387               Celem.Calc ("Poly.is'_polyrat'_in",eval_is_polyrat_in ""),

   388 	      (*Celem.Calc ("Atools.occurs'_in",eval_occurs_in ""),   *)

   389 	      (*Celem.Calc ("Atools.is'_const",eval_const "#is_const_"),*)

   390 	      Celem.Calc ("HOL.eq",eval_equal "#equal_"),

   391               Celem.Calc ("RootEq.is'_rootTerm'_in",eval_is_rootTerm_in ""),

   392 	      Celem.Calc ("RatEq.is'_ratequation'_in",eval_is_ratequation_in ""),

   393 	      Celem.Thm ("not_true",TermC.num_str @{thm not_true}),

   394 	      Celem.Thm ("not_false",TermC.num_str @{thm not_false}),

   395 	      Celem.Thm ("and_true",TermC.num_str @{thm and_true}),

   396 	      Celem.Thm ("and_false",TermC.num_str @{thm and_false}),

   397 	      Celem.Thm ("or_true",TermC.num_str @{thm or_true}),

   398 	      Celem.Thm ("or_false",TermC.num_str @{thm or_false})

   399 	       ];

   401 val PolyEq_erls =

   402     Celem.merge_rls "PolyEq_erls" LinEq_erls

   403     (Celem.append_rls "ops_preds" calculate_Rational

   404 		[Celem.Calc ("HOL.eq",eval_equal "#equal_"),

   405 		 Celem.Thm ("plus_leq", TermC.num_str @{thm plus_leq}),

   406 		 Celem.Thm ("minus_leq", TermC.num_str @{thm minus_leq}),

   407 		 Celem.Thm ("rat_leq1", TermC.num_str @{thm rat_leq1}),

   408 		 Celem.Thm ("rat_leq2", TermC.num_str @{thm rat_leq2}),

   409 		 Celem.Thm ("rat_leq3", TermC.num_str @{thm rat_leq3})

   410 		 ]);

   412 val PolyEq_crls =

   413     Celem.merge_rls "PolyEq_crls" LinEq_crls

   414     (Celem.append_rls "ops_preds" calculate_Rational

   415 		[Celem.Calc ("HOL.eq",eval_equal "#equal_"),

   416 		 Celem.Thm ("plus_leq", TermC.num_str @{thm plus_leq}),

   417 		 Celem.Thm ("minus_leq", TermC.num_str @{thm minus_leq}),

   418 		 Celem.Thm ("rat_leq1", TermC.num_str @{thm rat_leq1}),

   419 		 Celem.Thm ("rat_leq2", TermC.num_str @{thm rat_leq2}),

   420 		 Celem.Thm ("rat_leq3", TermC.num_str @{thm rat_leq3})

   421 		 ]);

   423 val cancel_leading_coeff = prep_rls'(

   424   Celem.Rls {id = "cancel_leading_coeff", preconds = [],

   425        rew_ord = ("xxxe_rew_ordxxx",Celem.e_rew_ord),

   426       erls = PolyEq_erls, srls = Celem.Erls, calc = [], errpatts = [],

   427       rules =

   428       [Celem.Thm ("cancel_leading_coeff1",TermC.num_str @{thm cancel_leading_coeff1}),

   429        Celem.Thm ("cancel_leading_coeff2",TermC.num_str @{thm cancel_leading_coeff2}),

   430        Celem.Thm ("cancel_leading_coeff3",TermC.num_str @{thm cancel_leading_coeff3}),

   431        Celem.Thm ("cancel_leading_coeff4",TermC.num_str @{thm cancel_leading_coeff4}),

   432        Celem.Thm ("cancel_leading_coeff5",TermC.num_str @{thm cancel_leading_coeff5}),

   433        Celem.Thm ("cancel_leading_coeff6",TermC.num_str @{thm cancel_leading_coeff6}),

   434        Celem.Thm ("cancel_leading_coeff7",TermC.num_str @{thm cancel_leading_coeff7}),

   435        Celem.Thm ("cancel_leading_coeff8",TermC.num_str @{thm cancel_leading_coeff8}),

   436        Celem.Thm ("cancel_leading_coeff9",TermC.num_str @{thm cancel_leading_coeff9}),

   437        Celem.Thm ("cancel_leading_coeff10",TermC.num_str @{thm cancel_leading_coeff10}),

   438        Celem.Thm ("cancel_leading_coeff11",TermC.num_str @{thm cancel_leading_coeff11}),

   439        Celem.Thm ("cancel_leading_coeff12",TermC.num_str @{thm cancel_leading_coeff12}),

   440        Celem.Thm ("cancel_leading_coeff13",TermC.num_str @{thm cancel_leading_coeff13})

   441        ],scr = Celem.Prog ((Thm.term_of o the o (TermC.parse thy)) "empty_script")});

   443 val prep_rls' = LTool.prep_rls @{theory};

   444 *}

   445 ML{*

   446 val complete_square = prep_rls'(

   447   Celem.Rls {id = "complete_square", preconds = [],

   448        rew_ord = ("xxxe_rew_ordxxx",Celem.e_rew_ord),

   449       erls = PolyEq_erls, srls = Celem.Erls, calc = [],  errpatts = [],

   450       rules = [Celem.Thm ("complete_square1",TermC.num_str @{thm complete_square1}),

   451 	       Celem.Thm ("complete_square2",TermC.num_str @{thm complete_square2}),

   452 	       Celem.Thm ("complete_square3",TermC.num_str @{thm complete_square3}),

   453 	       Celem.Thm ("complete_square4",TermC.num_str @{thm complete_square4}),

   454 	       Celem.Thm ("complete_square5",TermC.num_str @{thm complete_square5})

   455 	       ],

   456       scr = Celem.Prog ((Thm.term_of o the o (TermC.parse thy)) "empty_script")

   457       });

   459 val polyeq_simplify = prep_rls'(

   460   Celem.Rls {id = "polyeq_simplify", preconds = [],

   461        rew_ord = ("termlessI",termlessI),

   462        erls = PolyEq_erls,

   463        srls = Celem.Erls,

   464        calc = [], errpatts = [],

   465        rules = [Celem.Thm  ("real_assoc_1",TermC.num_str @{thm real_assoc_1}),

   466 		Celem.Thm  ("real_assoc_2",TermC.num_str @{thm real_assoc_2}),

   467 		Celem.Thm  ("real_diff_minus",TermC.num_str @{thm real_diff_minus}),

   468 		Celem.Thm  ("real_unari_minus",TermC.num_str @{thm real_unari_minus}),

   469 		Celem.Thm  ("realpow_multI",TermC.num_str @{thm realpow_multI}),

   470 		Celem.Calc ("Groups.plus_class.plus",eval_binop "#add_"),

   471 		Celem.Calc ("Groups.minus_class.minus",eval_binop "#sub_"),

   472 		Celem.Calc ("Groups.times_class.times",eval_binop "#mult_"),

   473 		Celem.Calc ("Rings.divide_class.divide", eval_cancel "#divide_e"),

   474 		Celem.Calc ("NthRoot.sqrt",eval_sqrt "#sqrt_"),

   475 		Celem.Calc ("Atools.pow" ,eval_binop "#power_"),

   476                 Celem.Rls_ reduce_012

   477                 ],

   478        scr = Celem.Prog ((Thm.term_of o the o (TermC.parse thy)) "empty_script")

   479        });

   480 *}

   481 setup {* KEStore_Elems.add_rlss

   482   [("cancel_leading_coeff", (Context.theory_name @{theory}, cancel_leading_coeff)),

   483   ("complete_square", (Context.theory_name @{theory}, complete_square)),

   484   ("PolyEq_erls", (Context.theory_name @{theory}, PolyEq_erls)),

   485   ("polyeq_simplify", (Context.theory_name @{theory}, polyeq_simplify))] *}

   486 ML{*

   488 (* ------------- polySolve ------------------ *)

   489 (* -- d0 -- *)

   490 (*isolate the bound variable in an d0 equation; 'bdv' is a meta-constant*)

   491 val d0_polyeq_simplify = prep_rls'(

   492   Celem.Rls {id = "d0_polyeq_simplify", preconds = [],

   493        rew_ord = ("xxxe_rew_ordxxx",Celem.e_rew_ord),

   494        erls = PolyEq_erls,

   495        srls = Celem.Erls,

   496        calc = [], errpatts = [],

   497        rules = [Celem.Thm("d0_true",TermC.num_str @{thm d0_true}),

   498 		Celem.Thm("d0_false",TermC.num_str @{thm  d0_false})

   499 		],

   500        scr = Celem.Prog ((Thm.term_of o the o (TermC.parse thy)) "empty_script")

   501        });

   503 (* -- d1 -- *)

   504 (*isolate the bound variable in an d1 equation; 'bdv' is a meta-constant*)

   505 val d1_polyeq_simplify = prep_rls'(

   506   Celem.Rls {id = "d1_polyeq_simplify", preconds = [],

   507        rew_ord = ("xxxe_rew_ordxxx",Celem.e_rew_ord),

   508        erls = PolyEq_erls,

   509        srls = Celem.Erls,

   510        calc = [], errpatts = [],

   511        rules = [

   512 		Celem.Thm("d1_isolate_add1",TermC.num_str @{thm d1_isolate_add1}),

   513 		(* a+bx=0 -> bx=-a *)

   514 		Celem.Thm("d1_isolate_add2",TermC.num_str @{thm d1_isolate_add2}),

   515 		(* a+ x=0 ->  x=-a *)

   516 		Celem.Thm("d1_isolate_div",TermC.num_str @{thm d1_isolate_div})

   517 		(*   bx=c -> x=c/b *)

   518 		],

   519        scr = Celem.Prog ((Thm.term_of o the o (TermC.parse thy)) "empty_script")

   520        });

   522 *}

   523 subsection {* degree 2 *}

   524 ML{*

   525 (* isolate the bound variable in an d2 equation with bdv only;

   526   "bdv" is a meta-constant substituted for the "x" below by isac's rewriter. *)

   527 val d2_polyeq_bdv_only_simplify = prep_rls'(

   528   Celem.Rls {id = "d2_polyeq_bdv_only_simplify", preconds = [], rew_ord = ("xxxe_rew_ordxxx",Celem.e_rew_ord),

   529     erls = PolyEq_erls, srls = Celem.Erls, calc = [], errpatts = [],

   530     rules =

   531       [Celem.Thm ("d2_prescind1", TermC.num_str @{thm d2_prescind1}), (*   ax+bx^2=0 -> x(a+bx)=0 *)

   532        Celem.Thm ("d2_prescind2", TermC.num_str @{thm d2_prescind2}), (*   ax+ x^2=0 -> x(a+ x)=0 *)

   533        Celem.Thm ("d2_prescind3", TermC.num_str @{thm d2_prescind3}), (*    x+bx^2=0 -> x(1+bx)=0 *)

   534        Celem.Thm ("d2_prescind4", TermC.num_str @{thm d2_prescind4}), (*    x+ x^2=0 -> x(1+ x)=0 *)

   535        Celem.Thm ("d2_sqrt_equation1", TermC.num_str @{thm d2_sqrt_equation1}),    (* x^2=c   -> x=+-sqrt(c) *)

   536        Celem.Thm ("d2_sqrt_equation1_neg", TermC.num_str @{thm d2_sqrt_equation1_neg}), (* [0<c] x^2=c  -> []*)

   537        Celem.Thm ("d2_sqrt_equation2", TermC.num_str @{thm d2_sqrt_equation2}),    (*  x^2=0 ->    x=0       *)

   538        Celem.Thm ("d2_reduce_equation1", TermC.num_str @{thm d2_reduce_equation1}),(* x(a+bx)=0 -> x=0 |a+bx=0*)

   539        Celem.Thm ("d2_reduce_equation2", TermC.num_str @{thm d2_reduce_equation2}),(* x(a+ x)=0 -> x=0 |a+ x=0*)

   540        Celem.Thm ("d2_isolate_div", TermC.num_str @{thm d2_isolate_div})           (* bx^2=c -> x^2=c/b      *)

   541        ],

   542        scr = Celem.Prog ((Thm.term_of o the o (TermC.parse thy)) "empty_script")

   543        });

   544 *}

   545 ML{*

   546 (* isolate the bound variable in an d2 equation with sqrt only;

   547    'bdv' is a meta-constant*)

   548 val d2_polyeq_sq_only_simplify = prep_rls'(

   549   Celem.Rls {id = "d2_polyeq_sq_only_simplify", preconds = [],

   550        rew_ord = ("xxxe_rew_ordxxx",Celem.e_rew_ord),

   551        erls = PolyEq_erls,

   552        srls = Celem.Erls,

   553        calc = [], errpatts = [],

   554        (*asm_thm = [("d2_sqrt_equation1",""),("d2_sqrt_equation1_neg",""),

   555                   ("d2_isolate_div","")],*)

   556        rules = [Celem.Thm("d2_isolate_add1",TermC.num_str @{thm d2_isolate_add1}),

   557                 (* a+   bx^2=0 -> bx^2=(-1)a*)

   558 		Celem.Thm("d2_isolate_add2",TermC.num_str @{thm d2_isolate_add2}),

   559                 (* a+    x^2=0 ->  x^2=(-1)a*)

   560 		Celem.Thm("d2_sqrt_equation2",TermC.num_str @{thm d2_sqrt_equation2}),

   561                 (*  x^2=0 ->    x=0    *)

   562 		Celem.Thm("d2_sqrt_equation1",TermC.num_str @{thm d2_sqrt_equation1}),

   563                 (* x^2=c   -> x=+-sqrt(c)*)

   564 		Celem.Thm("d2_sqrt_equation1_neg",TermC.num_str @{thm d2_sqrt_equation1_neg}),

   565                 (* [c<0] x^2=c  -> x=[] *)

   566 		Celem.Thm("d2_isolate_div",TermC.num_str @{thm d2_isolate_div})

   567                  (* bx^2=c -> x^2=c/b*)

   568 		],

   569        scr = Celem.Prog ((Thm.term_of o the o (TermC.parse thy)) "empty_script")

   570        });

   571 *}

   572 ML{*

   573 (* isolate the bound variable in an d2 equation with pqFormula;

   574    'bdv' is a meta-constant*)

   575 val d2_polyeq_pqFormula_simplify = prep_rls'(

   576   Celem.Rls {id = "d2_polyeq_pqFormula_simplify", preconds = [],

   577        rew_ord = ("xxxe_rew_ordxxx",Celem.e_rew_ord), erls = PolyEq_erls,

   578        srls = Celem.Erls, calc = [], errpatts = [],

   579        rules = [Celem.Thm("d2_pqformula1",TermC.num_str @{thm d2_pqformula1}),

   580                 (* q+px+ x^2=0 *)

   581 		Celem.Thm("d2_pqformula1_neg",TermC.num_str @{thm d2_pqformula1_neg}),

   582                 (* q+px+ x^2=0 *)

   583 		Celem.Thm("d2_pqformula2",TermC.num_str @{thm d2_pqformula2}),

   584                 (* q+px+1x^2=0 *)

   585 		Celem.Thm("d2_pqformula2_neg",TermC.num_str @{thm d2_pqformula2_neg}),

   586                 (* q+px+1x^2=0 *)

   587 		Celem.Thm("d2_pqformula3",TermC.num_str @{thm d2_pqformula3}),

   588                 (* q+ x+ x^2=0 *)

   589 		Celem.Thm("d2_pqformula3_neg",TermC.num_str @{thm d2_pqformula3_neg}),

   590                 (* q+ x+ x^2=0 *)

   591 		Celem.Thm("d2_pqformula4",TermC.num_str @{thm d2_pqformula4}),

   592                 (* q+ x+1x^2=0 *)

   593 		Celem.Thm("d2_pqformula4_neg",TermC.num_str @{thm d2_pqformula4_neg}),

   594                 (* q+ x+1x^2=0 *)

   595 		Celem.Thm("d2_pqformula5",TermC.num_str @{thm d2_pqformula5}),

   596                 (*   qx+ x^2=0 *)

   597 		Celem.Thm("d2_pqformula6",TermC.num_str @{thm d2_pqformula6}),

   598                 (*   qx+1x^2=0 *)

   599 		Celem.Thm("d2_pqformula7",TermC.num_str @{thm d2_pqformula7}),

   600                 (*    x+ x^2=0 *)

   601 		Celem.Thm("d2_pqformula8",TermC.num_str @{thm d2_pqformula8}),

   602                 (*    x+1x^2=0 *)

   603 		Celem.Thm("d2_pqformula9",TermC.num_str @{thm d2_pqformula9}),

   604                 (* q   +1x^2=0 *)

   605 		Celem.Thm("d2_pqformula9_neg",TermC.num_str @{thm d2_pqformula9_neg}),

   606                 (* q   +1x^2=0 *)

   607 		Celem.Thm("d2_pqformula10",TermC.num_str @{thm d2_pqformula10}),

   608                 (* q   + x^2=0 *)

   609 		Celem.Thm("d2_pqformula10_neg",TermC.num_str @{thm d2_pqformula10_neg}),

   610                 (* q   + x^2=0 *)

   611 		Celem.Thm("d2_sqrt_equation2",TermC.num_str @{thm d2_sqrt_equation2}),

   612                 (*       x^2=0 *)

   613 		Celem.Thm("d2_sqrt_equation3",TermC.num_str @{thm d2_sqrt_equation3})

   614                (*      1x^2=0 *)

   615 	       ],scr = Celem.Prog ((Thm.term_of o the o (TermC.parse thy)) "empty_script")

   616        });

   617 *}

   618 ML{*

   619 (* isolate the bound variable in an d2 equation with abcFormula;

   620    'bdv' is a meta-constant*)

   621 val d2_polyeq_abcFormula_simplify = prep_rls'(

   622   Celem.Rls {id = "d2_polyeq_abcFormula_simplify", preconds = [],

   623        rew_ord = ("xxxe_rew_ordxxx",Celem.e_rew_ord), erls = PolyEq_erls,

   624        srls = Celem.Erls, calc = [], errpatts = [],

   625        rules = [Celem.Thm("d2_abcformula1",TermC.num_str @{thm d2_abcformula1}),

   626                 (*c+bx+cx^2=0 *)

   627 		Celem.Thm("d2_abcformula1_neg",TermC.num_str @{thm d2_abcformula1_neg}),

   628                 (*c+bx+cx^2=0 *)

   629 		Celem.Thm("d2_abcformula2",TermC.num_str @{thm d2_abcformula2}),

   630                 (*c+ x+cx^2=0 *)

   631 		Celem.Thm("d2_abcformula2_neg",TermC.num_str @{thm d2_abcformula2_neg}),

   632                 (*c+ x+cx^2=0 *)

   633 		Celem.Thm("d2_abcformula3",TermC.num_str @{thm d2_abcformula3}),

   634                 (*c+bx+ x^2=0 *)

   635 		Celem.Thm("d2_abcformula3_neg",TermC.num_str @{thm d2_abcformula3_neg}),

   636                 (*c+bx+ x^2=0 *)

   637 		Celem.Thm("d2_abcformula4",TermC.num_str @{thm d2_abcformula4}),

   638                 (*c+ x+ x^2=0 *)

   639 		Celem.Thm("d2_abcformula4_neg",TermC.num_str @{thm d2_abcformula4_neg}),

   640                 (*c+ x+ x^2=0 *)

   641 		Celem.Thm("d2_abcformula5",TermC.num_str @{thm d2_abcformula5}),

   642                 (*c+   cx^2=0 *)

   643 		Celem.Thm("d2_abcformula5_neg",TermC.num_str @{thm d2_abcformula5_neg}),

   644                 (*c+   cx^2=0 *)

   645 		Celem.Thm("d2_abcformula6",TermC.num_str @{thm d2_abcformula6}),

   646                 (*c+    x^2=0 *)

   647 		Celem.Thm("d2_abcformula6_neg",TermC.num_str @{thm d2_abcformula6_neg}),

   648                 (*c+    x^2=0 *)

   649 		Celem.Thm("d2_abcformula7",TermC.num_str @{thm d2_abcformula7}),

   650                 (*  bx+ax^2=0 *)

   651 		Celem.Thm("d2_abcformula8",TermC.num_str @{thm d2_abcformula8}),

   652                 (*  bx+ x^2=0 *)

   653 		Celem.Thm("d2_abcformula9",TermC.num_str @{thm d2_abcformula9}),

   654                 (*   x+ax^2=0 *)

   655 		Celem.Thm("d2_abcformula10",TermC.num_str @{thm d2_abcformula10}),

   656                 (*   x+ x^2=0 *)

   657 		Celem.Thm("d2_sqrt_equation2",TermC.num_str @{thm d2_sqrt_equation2}),

   658                 (*      x^2=0 *)

   659 		Celem.Thm("d2_sqrt_equation3",TermC.num_str @{thm d2_sqrt_equation3})

   660                (*     bx^2=0 *)

   661 	       ],

   662        scr = Celem.Prog ((Thm.term_of o the o (TermC.parse thy)) "empty_script")

   663        });

   664 *}

   665 ML{*

   667 (* isolate the bound variable in an d2 equation;

   668    'bdv' is a meta-constant*)

   669 val d2_polyeq_simplify = prep_rls'(

   670   Celem.Rls {id = "d2_polyeq_simplify", preconds = [],

   671        rew_ord = ("xxxe_rew_ordxxx",Celem.e_rew_ord), erls = PolyEq_erls,

   672        srls = Celem.Erls, calc = [], errpatts = [],

   673        rules = [Celem.Thm("d2_pqformula1",TermC.num_str @{thm d2_pqformula1}),

   674                 (* p+qx+ x^2=0 *)

   675 		Celem.Thm("d2_pqformula1_neg",TermC.num_str @{thm d2_pqformula1_neg}),

   676                 (* p+qx+ x^2=0 *)

   677 		Celem.Thm("d2_pqformula2",TermC.num_str @{thm d2_pqformula2}),

   678                 (* p+qx+1x^2=0 *)

   679 		Celem.Thm("d2_pqformula2_neg",TermC.num_str @{thm d2_pqformula2_neg}),

   680                 (* p+qx+1x^2=0 *)

   681 		Celem.Thm("d2_pqformula3",TermC.num_str @{thm d2_pqformula3}),

   682                 (* p+ x+ x^2=0 *)

   683 		Celem.Thm("d2_pqformula3_neg",TermC.num_str @{thm d2_pqformula3_neg}),

   684                 (* p+ x+ x^2=0 *)

   685 		Celem.Thm("d2_pqformula4",TermC.num_str @{thm d2_pqformula4}),

   686                 (* p+ x+1x^2=0 *)

   687 		Celem.Thm("d2_pqformula4_neg",TermC.num_str @{thm d2_pqformula4_neg}),

   688                 (* p+ x+1x^2=0 *)

   689 		Celem.Thm("d2_abcformula1",TermC.num_str @{thm d2_abcformula1}),

   690                 (* c+bx+cx^2=0 *)

   691 		Celem.Thm("d2_abcformula1_neg",TermC.num_str @{thm d2_abcformula1_neg}),

   692                 (* c+bx+cx^2=0 *)

   693 		Celem.Thm("d2_abcformula2",TermC.num_str @{thm d2_abcformula2}),

   694                 (* c+ x+cx^2=0 *)

   695 		Celem.Thm("d2_abcformula2_neg",TermC.num_str @{thm d2_abcformula2_neg}),

   696                 (* c+ x+cx^2=0 *)

   697 		Celem.Thm("d2_prescind1",TermC.num_str @{thm d2_prescind1}),

   698                 (*   ax+bx^2=0 -> x(a+bx)=0 *)

   699 		Celem.Thm("d2_prescind2",TermC.num_str @{thm d2_prescind2}),

   700                 (*   ax+ x^2=0 -> x(a+ x)=0 *)

   701 		Celem.Thm("d2_prescind3",TermC.num_str @{thm d2_prescind3}),

   702                 (*    x+bx^2=0 -> x(1+bx)=0 *)

   703 		Celem.Thm("d2_prescind4",TermC.num_str @{thm d2_prescind4}),

   704                 (*    x+ x^2=0 -> x(1+ x)=0 *)

   705 		Celem.Thm("d2_isolate_add1",TermC.num_str @{thm d2_isolate_add1}),

   706                 (* a+   bx^2=0 -> bx^2=(-1)a*)

   707 		Celem.Thm("d2_isolate_add2",TermC.num_str @{thm d2_isolate_add2}),

   708                 (* a+    x^2=0 ->  x^2=(-1)a*)

   709 		Celem.Thm("d2_sqrt_equation1",TermC.num_str @{thm d2_sqrt_equation1}),

   710                 (* x^2=c   -> x=+-sqrt(c)*)

   711 		Celem.Thm("d2_sqrt_equation1_neg",TermC.num_str @{thm d2_sqrt_equation1_neg}),

   712                 (* [c<0] x^2=c   -> x=[]*)

   713 		Celem.Thm("d2_sqrt_equation2",TermC.num_str @{thm d2_sqrt_equation2}),

   714                 (*  x^2=0 ->    x=0    *)

   715 		Celem.Thm("d2_reduce_equation1",TermC.num_str @{thm d2_reduce_equation1}),

   716                 (* x(a+bx)=0 -> x=0 | a+bx=0*)

   717 		Celem.Thm("d2_reduce_equation2",TermC.num_str @{thm d2_reduce_equation2}),

   718                 (* x(a+ x)=0 -> x=0 | a+ x=0*)

   719 		Celem.Thm("d2_isolate_div",TermC.num_str @{thm d2_isolate_div})

   720                (* bx^2=c -> x^2=c/b*)

   721 	       ],

   722        scr = Celem.Prog ((Thm.term_of o the o (TermC.parse thy)) "empty_script")

   723       });

   724 *}

   725 ML{*

   727 (* -- d3 -- *)

   728 (* isolate the bound variable in an d3 equation; 'bdv' is a meta-constant *)

   729 val d3_polyeq_simplify = prep_rls'(

   730   Celem.Rls {id = "d3_polyeq_simplify", preconds = [],

   731        rew_ord = ("xxxe_rew_ordxxx",Celem.e_rew_ord), erls = PolyEq_erls,

   732        srls = Celem.Erls, calc = [], errpatts = [],

   733        rules =

   734        [Celem.Thm("d3_reduce_equation1",TermC.num_str @{thm d3_reduce_equation1}),

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

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

   737 	Celem.Thm("d3_reduce_equation2",TermC.num_str @{thm d3_reduce_equation2}),

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

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

   740 	Celem.Thm("d3_reduce_equation3",TermC.num_str @{thm d3_reduce_equation3}),

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

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

   743 	Celem.Thm("d3_reduce_equation4",TermC.num_str @{thm d3_reduce_equation4}),

   744 	(*  bdv +   bdv^^^2 + c*bdv^^^3=0) =

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

   746 	Celem.Thm("d3_reduce_equation5",TermC.num_str @{thm d3_reduce_equation5}),

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

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

   749 	Celem.Thm("d3_reduce_equation6",TermC.num_str @{thm d3_reduce_equation6}),

   750 	(*  bdv + b*bdv^^^2 +   bdv^^^3=0) =

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

   752 	Celem.Thm("d3_reduce_equation7",TermC.num_str @{thm d3_reduce_equation7}),

   753 	     (*a*bdv +   bdv^^^2 +   bdv^^^3=0) =

   754              (bdv=0 | (1 +   bdv +   bdv^^^2=0)*)

   755 	Celem.Thm("d3_reduce_equation8",TermC.num_str @{thm d3_reduce_equation8}),

   756 	     (*  bdv +   bdv^^^2 +   bdv^^^3=0) =

   757              (bdv=0 | (1 +   bdv +   bdv^^^2=0)*)

   758 	Celem.Thm("d3_reduce_equation9",TermC.num_str @{thm d3_reduce_equation9}),

   759 	     (*a*bdv             + c*bdv^^^3=0) =

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

   761 	Celem.Thm("d3_reduce_equation10",TermC.num_str @{thm d3_reduce_equation10}),

   762 	     (*  bdv             + c*bdv^^^3=0) =

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

   764 	Celem.Thm("d3_reduce_equation11",TermC.num_str @{thm d3_reduce_equation11}),

   765 	     (*a*bdv             +   bdv^^^3=0) =

   766              (bdv=0 | (a         +   bdv^^^2=0)*)

   767 	Celem.Thm("d3_reduce_equation12",TermC.num_str @{thm d3_reduce_equation12}),

   768 	     (*  bdv             +   bdv^^^3=0) =

   769              (bdv=0 | (1         +   bdv^^^2=0)*)

   770 	Celem.Thm("d3_reduce_equation13",TermC.num_str @{thm d3_reduce_equation13}),

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

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

   773 	Celem.Thm("d3_reduce_equation14",TermC.num_str @{thm d3_reduce_equation14}),

   774 	     (*          bdv^^^2 + c*bdv^^^3=0) =

   775              (bdv=0 | (      bdv + c*bdv^^^2=0)*)

   776 	Celem.Thm("d3_reduce_equation15",TermC.num_str @{thm d3_reduce_equation15}),

   777 	     (*        b*bdv^^^2 +   bdv^^^3=0) =

   778              (bdv=0 | (    b*bdv +   bdv^^^2=0)*)

   779 	Celem.Thm("d3_reduce_equation16",TermC.num_str @{thm d3_reduce_equation16}),

   780 	     (*          bdv^^^2 +   bdv^^^3=0) =

   781              (bdv=0 | (      bdv +   bdv^^^2=0)*)

   782 	Celem.Thm("d3_isolate_add1",TermC.num_str @{thm d3_isolate_add1}),

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

   784               (bdv=0 | (b*bdv^^^3=a)*)

   785 	Celem.Thm("d3_isolate_add2",TermC.num_str @{thm d3_isolate_add2}),

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

   787               (bdv=0 | (  bdv^^^3=a)*)

   788 	Celem.Thm("d3_isolate_div",TermC.num_str @{thm d3_isolate_div}),

   789         (*[|Not(b=0)|] ==> (b*bdv^^^3=c) = (bdv^^^3=c/b*)

   790         Celem.Thm("d3_root_equation2",TermC.num_str @{thm d3_root_equation2}),

   791         (*(bdv^^^3=0) = (bdv=0) *)

   792 	Celem.Thm("d3_root_equation1",TermC.num_str @{thm d3_root_equation1})

   793        (*bdv^^^3=c) = (bdv = nroot 3 c*)

   794        ],

   795        scr = Celem.Prog ((Thm.term_of o the o (TermC.parse thy)) "empty_script")

   796       });

   797 *}

   798 ML{*

   800 (* -- d4 -- *)

   801 (*isolate the bound variable in an d4 equation; 'bdv' is a meta-constant*)

   802 val d4_polyeq_simplify = prep_rls'(

   803   Celem.Rls {id = "d4_polyeq_simplify", preconds = [],

   804        rew_ord = ("xxxe_rew_ordxxx",Celem.e_rew_ord), erls = PolyEq_erls,

   805        srls = Celem.Erls, calc = [], errpatts = [],

   806        rules =

   807        [Celem.Thm("d4_sub_u1",TermC.num_str @{thm d4_sub_u1})

   808        (* ax^4+bx^2+c=0 -> x=+-sqrt(ax^2+bx^+c) *)

   809        ],

   810        scr = Celem.Prog ((Thm.term_of o the o (TermC.parse thy)) "empty_script")

   811       });

   812 *}

   813 setup {* KEStore_Elems.add_rlss

   814   [("d0_polyeq_simplify", (Context.theory_name @{theory}, d0_polyeq_simplify)),

   815   ("d1_polyeq_simplify", (Context.theory_name @{theory}, d1_polyeq_simplify)),

   816   ("d2_polyeq_simplify", (Context.theory_name @{theory}, d2_polyeq_simplify)),

   817   ("d2_polyeq_bdv_only_simplify", (Context.theory_name @{theory}, d2_polyeq_bdv_only_simplify)),

   818   ("d2_polyeq_sq_only_simplify", (Context.theory_name @{theory}, d2_polyeq_sq_only_simplify)),

   820   ("d2_polyeq_pqFormula_simplify",

   821     (Context.theory_name @{theory}, d2_polyeq_pqFormula_simplify)),

   822   ("d2_polyeq_abcFormula_simplify",

   823     (Context.theory_name @{theory}, d2_polyeq_abcFormula_simplify)),

   824   ("d3_polyeq_simplify", (Context.theory_name @{theory}, d3_polyeq_simplify)),

   825   ("d4_polyeq_simplify", (Context.theory_name @{theory}, d4_polyeq_simplify))] *}

   826 ML{*

   827 (*------------------------problems------------------------*)

   828 (*

   829 (get_pbt ["degree_2","polynomial","univariate","equation"]);

   830 show_ptyps();

   831 *)

   832 *}

   833 setup {* KEStore_Elems.add_pbts

   834   [(Specify.prep_pbt thy "pbl_equ_univ_poly" [] Celem.e_pblID

   835       (["polynomial","univariate","equation"],

   836         [("#Given" ,["equality e_e","solveFor v_v"]),

   837           ("#Where" ,["~((e_e::bool) is_ratequation_in (v_v::real))",

   838 	          "~((lhs e_e) is_rootTerm_in (v_v::real))",

   839 	          "~((rhs e_e) is_rootTerm_in (v_v::real))"]),

   840           ("#Find"  ,["solutions v_v'i'"])],

   841         PolyEq_prls, SOME "solve (e_e::bool, v_v)", [])),

   842     (*--- d0 ---*)

   843     (Specify.prep_pbt thy "pbl_equ_univ_poly_deg0" [] Celem.e_pblID

   844       (["degree_0","polynomial","univariate","equation"],

   845         [("#Given" ,["equality e_e","solveFor v_v"]),

   846           ("#Where" ,["matches (?a = 0) e_e",

   847 	          "(lhs e_e) is_poly_in v_v",

   848 	          "((lhs e_e) has_degree_in v_v ) = 0"]),

   849           ("#Find"  ,["solutions v_v'i'"])],

   850         PolyEq_prls, SOME "solve (e_e::bool, v_v)", [["PolyEq","solve_d0_polyeq_equation"]])),

   851     (*--- d1 ---*)

   852     (Specify.prep_pbt thy "pbl_equ_univ_poly_deg1" [] Celem.e_pblID

   853       (["degree_1","polynomial","univariate","equation"],

   854         [("#Given" ,["equality e_e","solveFor v_v"]),

   855           ("#Where" ,["matches (?a = 0) e_e",

   856 	          "(lhs e_e) is_poly_in v_v",

   857 	          "((lhs e_e) has_degree_in v_v ) = 1"]),

   858           ("#Find"  ,["solutions v_v'i'"])],

   859         PolyEq_prls, SOME "solve (e_e::bool, v_v)", [["PolyEq","solve_d1_polyeq_equation"]])),

   860     (*--- d2 ---*)

   861     (Specify.prep_pbt thy "pbl_equ_univ_poly_deg2" [] Celem.e_pblID

   862       (["degree_2","polynomial","univariate","equation"],

   863         [("#Given" ,["equality e_e","solveFor v_v"]),

   864           ("#Where" ,["matches (?a = 0) e_e",

   865 	          "(lhs e_e) is_poly_in v_v ",

   866 	          "((lhs e_e) has_degree_in v_v ) = 2"]),

   867           ("#Find"  ,["solutions v_v'i'"])],

   868         PolyEq_prls, SOME "solve (e_e::bool, v_v)", [["PolyEq","solve_d2_polyeq_equation"]])),

   869     (Specify.prep_pbt thy "pbl_equ_univ_poly_deg2_sqonly" [] Celem.e_pblID

   870       (["sq_only","degree_2","polynomial","univariate","equation"],

   871         [("#Given" ,["equality e_e","solveFor v_v"]),

   872           ("#Where" ,["matches ( ?a +    ?v_^^^2 = 0) e_e | " ^

   873 	          "matches ( ?a + ?b*?v_^^^2 = 0) e_e | " ^

   874             "matches (         ?v_^^^2 = 0) e_e | " ^

   875             "matches (      ?b*?v_^^^2 = 0) e_e" ,

   876             "Not (matches (?a +    ?v_ +    ?v_^^^2 = 0) e_e) &" ^

   877             "Not (matches (?a + ?b*?v_ +    ?v_^^^2 = 0) e_e) &" ^

   878             "Not (matches (?a +    ?v_ + ?c*?v_^^^2 = 0) e_e) &" ^

   879             "Not (matches (?a + ?b*?v_ + ?c*?v_^^^2 = 0) e_e) &" ^

   880             "Not (matches (        ?v_ +    ?v_^^^2 = 0) e_e) &" ^

   881             "Not (matches (     ?b*?v_ +    ?v_^^^2 = 0) e_e) &" ^

   882             "Not (matches (        ?v_ + ?c*?v_^^^2 = 0) e_e) &" ^

   883             "Not (matches (     ?b*?v_ + ?c*?v_^^^2 = 0) e_e)"]),

   884           ("#Find"  ,["solutions v_v'i'"])],

   885         PolyEq_prls, SOME "solve (e_e::bool, v_v)",

   886         [["PolyEq","solve_d2_polyeq_sqonly_equation"]])),

   887     (Specify.prep_pbt thy "pbl_equ_univ_poly_deg2_bdvonly" [] Celem.e_pblID

   888       (["bdv_only","degree_2","polynomial","univariate","equation"],

   889         [("#Given", ["equality e_e","solveFor v_v"]),

   890           ("#Where", ["matches (?a*?v_ +    ?v_^^^2 = 0) e_e | " ^

   891             "matches (   ?v_ +    ?v_^^^2 = 0) e_e | " ^

   892             "matches (   ?v_ + ?b*?v_^^^2 = 0) e_e | " ^

   893             "matches (?a*?v_ + ?b*?v_^^^2 = 0) e_e | " ^

   894             "matches (            ?v_^^^2 = 0) e_e | " ^

   895             "matches (         ?b*?v_^^^2 = 0) e_e "]),

   896           ("#Find", ["solutions v_v'i'"])],

   897         PolyEq_prls, SOME "solve (e_e::bool, v_v)",

   898         [["PolyEq","solve_d2_polyeq_bdvonly_equation"]])),

   899     (Specify.prep_pbt thy "pbl_equ_univ_poly_deg2_pq" [] Celem.e_pblID

   900       (["pqFormula","degree_2","polynomial","univariate","equation"],

   901         [("#Given", ["equality e_e","solveFor v_v"]),

   902           ("#Where", ["matches (?a + 1*?v_^^^2 = 0) e_e | " ^

   903 	          "matches (?a +   ?v_^^^2 = 0) e_e"]),

   904           ("#Find", ["solutions v_v'i'"])],

   905         PolyEq_prls, SOME "solve (e_e::bool, v_v)", [["PolyEq","solve_d2_polyeq_pq_equation"]])),

   906     (Specify.prep_pbt thy "pbl_equ_univ_poly_deg2_abc" [] Celem.e_pblID

   907       (["abcFormula","degree_2","polynomial","univariate","equation"],

   908         [("#Given", ["equality e_e","solveFor v_v"]),

   909           ("#Where", ["matches (?a +    ?v_^^^2 = 0) e_e | " ^

   910 	          "matches (?a + ?b*?v_^^^2 = 0) e_e"]),

   911           ("#Find", ["solutions v_v'i'"])],

   912         PolyEq_prls, SOME "solve (e_e::bool, v_v)", [["PolyEq","solve_d2_polyeq_abc_equation"]])),

   913     (*--- d3 ---*)

   914     (Specify.prep_pbt thy "pbl_equ_univ_poly_deg3" [] Celem.e_pblID

   915       (["degree_3","polynomial","univariate","equation"],

   916         [("#Given", ["equality e_e","solveFor v_v"]),

   917           ("#Where", ["matches (?a = 0) e_e",

   918 	          "(lhs e_e) is_poly_in v_v ",

   919 	          "((lhs e_e) has_degree_in v_v) = 3"]),

   920           ("#Find", ["solutions v_v'i'"])],

   921         PolyEq_prls, SOME "solve (e_e::bool, v_v)", [["PolyEq","solve_d3_polyeq_equation"]])),

   922     (*--- d4 ---*)

   923     (Specify.prep_pbt thy "pbl_equ_univ_poly_deg4" [] Celem.e_pblID

   924       (["degree_4","polynomial","univariate","equation"],

   925         [("#Given", ["equality e_e","solveFor v_v"]),

   926           ("#Where", ["matches (?a = 0) e_e",

   927 	          "(lhs e_e) is_poly_in v_v ",

   928 	          "((lhs e_e) has_degree_in v_v) = 4"]),

   929           ("#Find", ["solutions v_v'i'"])],

   930         PolyEq_prls, SOME "solve (e_e::bool, v_v)", [(*["PolyEq","solve_d4_polyeq_equation"]*)])),

   931     (*--- normalise ---*)

   932     (Specify.prep_pbt thy "pbl_equ_univ_poly_norm" [] Celem.e_pblID

   933       (["normalise","polynomial","univariate","equation"],

   934         [("#Given", ["equality e_e","solveFor v_v"]),

   935           ("#Where", ["(Not((matches (?a = 0 ) e_e ))) |" ^

   936 	          "(Not(((lhs e_e) is_poly_in v_v)))"]),

   937           ("#Find", ["solutions v_v'i'"])],

   938         PolyEq_prls, SOME "solve (e_e::bool, v_v)", [["PolyEq","normalise_poly"]])),

   939     (*-------------------------expanded-----------------------*)

   940     (Specify.prep_pbt thy "pbl_equ_univ_expand" [] Celem.e_pblID

   941       (["expanded","univariate","equation"],

   942         [("#Given", ["equality e_e","solveFor v_v"]),

   943           ("#Where", ["matches (?a = 0) e_e",

   944 	          "(lhs e_e) is_expanded_in v_v "]),

   945           ("#Find", ["solutions v_v'i'"])],

   946         PolyEq_prls, SOME "solve (e_e::bool, v_v)", [])),

   947     (*--- d2 ---*)

   948     (Specify.prep_pbt thy "pbl_equ_univ_expand_deg2" [] Celem.e_pblID

   949       (["degree_2","expanded","univariate","equation"],

   950         [("#Given", ["equality e_e","solveFor v_v"]),

   951           ("#Where", ["((lhs e_e) has_degree_in v_v) = 2"]),

   952           ("#Find", ["solutions v_v'i'"])],

   953          PolyEq_prls, SOME "solve (e_e::bool, v_v)", [["PolyEq","complete_square"]]))] *}

   955 ML{*

   956 val scr =

   957     "Script Normalize_poly (e_e::bool) (v_v::real) =                     " ^

   958     "(let e_e =((Try         (Rewrite     all_left          False)) @@  " ^

   959     "          (Try (Repeat (Rewrite     makex1_x         False))) @@  " ^

   960     "          (Try (Repeat (Rewrite_Set expand_binoms    False))) @@  " ^

   961     "          (Try (Repeat (Rewrite_Set_Inst [(bdv,v_v::real)]         " ^

   962     "                                 make_ratpoly_in     False))) @@  " ^

   963     "          (Try (Repeat (Rewrite_Set polyeq_simplify  False)))) e_e " ^

   964     " in (SubProblem (PolyEq',[polynomial,univariate,equation], [no_met])   " ^

   965     "                 [BOOL e_e, REAL v_v]))";

   966 TermC.parse thy scr;

   967 *}

   969 text {* "-------------------------methods-----------------------" *}

   970 setup {* KEStore_Elems.add_mets

   971   [Specify.prep_met thy "met_polyeq" [] Celem.e_metID

   972       (["PolyEq"], [],

   973         {rew_ord'="tless_true",rls'=Atools_erls,calc = [], srls = Celem.e_rls, prls=Celem.e_rls,

   974           crls=PolyEq_crls, errpats = [], nrls = norm_Rational},

   975         "empty_script"),

   976     Specify.prep_met thy "met_polyeq_norm" [] Celem.e_metID

   977       (["PolyEq","normalise_poly"],

   978         [("#Given" ,["equality e_e","solveFor v_v"]),

   979           ("#Where" ,["(Not((matches (?a = 0 ) e_e ))) |(Not(((lhs e_e) is_poly_in v_v)))"]),

   980           ("#Find"  ,["solutions v_v'i'"])],

   981         {rew_ord'="termlessI", rls'=PolyEq_erls, srls=Celem.e_rls, prls=PolyEq_prls, calc=[],

   982           crls=PolyEq_crls, errpats = [], nrls = norm_Rational},

   983         "Script Normalize_poly (e_e::bool) (v_v::real) =                     " ^

   984           "(let e_e =((Try         (Rewrite     all_left          False)) @@  " ^

   985           "          (Try (Repeat (Rewrite     makex1_x         False))) @@  " ^

   986           "          (Try (Repeat (Rewrite_Set expand_binoms    False))) @@  " ^

   987           "          (Try (Repeat (Rewrite_Set_Inst [(bdv,v_v::real)]         " ^

   988           "                                 make_ratpoly_in     False))) @@  " ^

   989           "          (Try (Repeat (Rewrite_Set polyeq_simplify  False)))) e_e " ^

   990           " in (SubProblem (PolyEq',[polynomial,univariate,equation], [no_met])   " ^

   991           "                 [BOOL e_e, REAL v_v]))"),

   992     Specify.prep_met thy "met_polyeq_d0" [] Celem.e_metID

   993       (["PolyEq","solve_d0_polyeq_equation"],

   994         [("#Given" ,["equality e_e","solveFor v_v"]),

   995           ("#Where" ,["(lhs e_e) is_poly_in v_v ", "((lhs e_e) has_degree_in v_v) = 0"]),

   996           ("#Find"  ,["solutions v_v'i'"])],

   997         {rew_ord'="termlessI", rls'=PolyEq_erls, srls=Celem.e_rls, prls=PolyEq_prls,

   998           calc=[("sqrt", ("NthRoot.sqrt", eval_sqrt "#sqrt_"))], crls=PolyEq_crls, errpats = [],

   999           nrls = norm_Rational},

  1000         "Script Solve_d0_polyeq_equation  (e_e::bool) (v_v::real)  = " ^

  1001           "(let e_e =  ((Try (Rewrite_Set_Inst [(bdv,v_v::real)]      " ^

  1002           "                  d0_polyeq_simplify  False))) e_e        " ^

  1003           " in ((Or_to_List e_e)::bool list))"),

  1004     Specify.prep_met thy "met_polyeq_d1" [] Celem.e_metID

  1005       (["PolyEq","solve_d1_polyeq_equation"],

  1006         [("#Given" ,["equality e_e","solveFor v_v"]),

  1007           ("#Where" ,["(lhs e_e) is_poly_in v_v ", "((lhs e_e) has_degree_in v_v) = 1"]),

  1008           ("#Find"  ,["solutions v_v'i'"])],

  1009         {rew_ord'="termlessI", rls'=PolyEq_erls, srls=Celem.e_rls, prls=PolyEq_prls,

  1010           calc=[("sqrt", ("NthRoot.sqrt", eval_sqrt "#sqrt_"))], crls=PolyEq_crls, errpats = [],

  1011           nrls = norm_Rational},

  1012         "Script Solve_d1_polyeq_equation  (e_e::bool) (v_v::real)  =   " ^

  1013           "(let e_e =  ((Try (Rewrite_Set_Inst [(bdv,v_v::real)]        " ^

  1014           "                  d1_polyeq_simplify   True))          @@  " ^

  1015           "            (Try (Rewrite_Set polyeq_simplify  False)) @@  " ^

  1016           "            (Try (Rewrite_Set norm_Rational_parenthesized False))) e_e;" ^

  1017           " (L_L::bool list) = ((Or_to_List e_e)::bool list)            " ^

  1018           " in Check_elementwise L_L {(v_v::real). Assumptions} )"),

  1019     Specify.prep_met thy "met_polyeq_d22" [] Celem.e_metID

  1020       (["PolyEq","solve_d2_polyeq_equation"],

  1021         [("#Given" ,["equality e_e","solveFor v_v"]),

  1022           ("#Where" ,["(lhs e_e) is_poly_in v_v ", "((lhs e_e) has_degree_in v_v) = 2"]),

  1023           ("#Find"  ,["solutions v_v'i'"])],

  1024         {rew_ord'="termlessI", rls'=PolyEq_erls, srls=Celem.e_rls, prls=PolyEq_prls,

  1025           calc=[("sqrt", ("NthRoot.sqrt", eval_sqrt "#sqrt_"))], crls=PolyEq_crls, errpats = [],

  1026           nrls = norm_Rational},

  1027           "Script Solve_d2_polyeq_equation  (e_e::bool) (v_v::real) =      " ^

  1028             "  (let e_e = ((Try (Rewrite_Set_Inst [(bdv,v_v::real)]         " ^

  1029             "                    d2_polyeq_simplify           True)) @@   " ^

  1030             "             (Try (Rewrite_Set polyeq_simplify   False)) @@  " ^

  1031             "             (Try (Rewrite_Set_Inst [(bdv,v_v::real)]         " ^

  1032             "                    d1_polyeq_simplify            True)) @@  " ^

  1033             "            (Try (Rewrite_Set polyeq_simplify    False)) @@  " ^

  1034             "            (Try (Rewrite_Set norm_Rational_parenthesized False))) e_e;" ^

  1035             " (L_L::bool list) = ((Or_to_List e_e)::bool list)              " ^

  1036             " in Check_elementwise L_L {(v_v::real). Assumptions} )"),

  1037     Specify.prep_met thy "met_polyeq_d2_bdvonly" [] Celem.e_metID

  1038       (["PolyEq","solve_d2_polyeq_bdvonly_equation"],

  1039         [("#Given" ,["equality e_e","solveFor v_v"]),

  1040           ("#Where" ,["(lhs e_e) is_poly_in v_v ", "((lhs e_e) has_degree_in v_v) = 2"]),

  1041           ("#Find"  ,["solutions v_v'i'"])],

  1042         {rew_ord'="termlessI", rls'=PolyEq_erls, srls=Celem.e_rls, prls=PolyEq_prls,

  1043           calc=[("sqrt", ("NthRoot.sqrt", eval_sqrt "#sqrt_"))], crls=PolyEq_crls, errpats = [],

  1044           nrls = norm_Rational},

  1045           "Script Solve_d2_polyeq_bdvonly_equation  (e_e::bool) (v_v::real) =" ^

  1046             "  (let e_e = ((Try (Rewrite_Set_Inst [(bdv,v_v::real)]         " ^

  1047             "                   d2_polyeq_bdv_only_simplify    True)) @@  " ^

  1048             "             (Try (Rewrite_Set polyeq_simplify   False)) @@  " ^

  1049             "             (Try (Rewrite_Set_Inst [(bdv,v_v::real)]         " ^

  1050             "                   d1_polyeq_simplify             True)) @@  " ^

  1051             "            (Try (Rewrite_Set polyeq_simplify    False)) @@  " ^

  1052             "            (Try (Rewrite_Set norm_Rational_parenthesized False))) e_e;" ^

  1053             " (L_L::bool list) = ((Or_to_List e_e)::bool list)              " ^

  1054             " in Check_elementwise L_L {(v_v::real). Assumptions} )"),

  1055     Specify.prep_met thy "met_polyeq_d2_sqonly" [] Celem.e_metID

  1056       (["PolyEq","solve_d2_polyeq_sqonly_equation"],

  1057         [("#Given" ,["equality e_e","solveFor v_v"]),

  1058           ("#Where" ,["(lhs e_e) is_poly_in v_v ", "((lhs e_e) has_degree_in v_v) = 2"]),

  1059           ("#Find"  ,["solutions v_v'i'"])],

  1060         {rew_ord'="termlessI", rls'=PolyEq_erls, srls=Celem.e_rls, prls=PolyEq_prls,

  1061           calc=[("sqrt", ("NthRoot.sqrt", eval_sqrt "#sqrt_"))], crls=PolyEq_crls, errpats = [],

  1062           nrls = norm_Rational},

  1063           "Script Solve_d2_polyeq_sqonly_equation  (e_e::bool) (v_v::real) =" ^

  1064             "  (let e_e = ((Try (Rewrite_Set_Inst [(bdv,v_v::real)]          " ^

  1065             "                   d2_polyeq_sq_only_simplify     True)) @@   " ^

  1066             "            (Try (Rewrite_Set polyeq_simplify    False)) @@   " ^

  1067             "            (Try (Rewrite_Set norm_Rational_parenthesized False))) e_e; " ^

  1068             " (L_L::bool list) = ((Or_to_List e_e)::bool list)               " ^

  1069             " in Check_elementwise L_L {(v_v::real). Assumptions} )"),

  1070     Specify.prep_met thy "met_polyeq_d2_pq" [] Celem.e_metID

  1071       (["PolyEq","solve_d2_polyeq_pq_equation"],

  1072         [("#Given" ,["equality e_e","solveFor v_v"]),

  1073           ("#Where" ,["(lhs e_e) is_poly_in v_v ", "((lhs e_e) has_degree_in v_v) = 2"]),

  1074           ("#Find"  ,["solutions v_v'i'"])],

  1075         {rew_ord'="termlessI", rls'=PolyEq_erls, srls=Celem.e_rls, prls=PolyEq_prls,

  1076           calc=[("sqrt", ("NthRoot.sqrt", eval_sqrt "#sqrt_"))], crls=PolyEq_crls, errpats = [],

  1077           nrls = norm_Rational},

  1078           "Script Solve_d2_polyeq_pq_equation  (e_e::bool) (v_v::real) =   " ^

  1079             "  (let e_e = ((Try (Rewrite_Set_Inst [(bdv,v_v::real)]         " ^

  1080             "                   d2_polyeq_pqFormula_simplify   True)) @@  " ^

  1081             "            (Try (Rewrite_Set polyeq_simplify    False)) @@  " ^

  1082             "            (Try (Rewrite_Set norm_Rational_parenthesized False))) e_e;" ^

  1083             " (L_L::bool list) = ((Or_to_List e_e)::bool list)              " ^

  1084             " in Check_elementwise L_L {(v_v::real). Assumptions} )"),

  1085     Specify.prep_met thy "met_polyeq_d2_abc" [] Celem.e_metID

  1086       (["PolyEq","solve_d2_polyeq_abc_equation"],

  1087         [("#Given" ,["equality e_e","solveFor v_v"]),

  1088           ("#Where" ,["(lhs e_e) is_poly_in v_v ", "((lhs e_e) has_degree_in v_v) = 2"]),

  1089           ("#Find"  ,["solutions v_v'i'"])],

  1090         {rew_ord'="termlessI", rls'=PolyEq_erls,srls=Celem.e_rls, prls=PolyEq_prls,

  1091           calc=[("sqrt", ("NthRoot.sqrt", eval_sqrt "#sqrt_"))], crls=PolyEq_crls, errpats = [],

  1092           nrls = norm_Rational},

  1093           "Script Solve_d2_polyeq_abc_equation  (e_e::bool) (v_v::real) =   " ^

  1094             "  (let e_e = ((Try (Rewrite_Set_Inst [(bdv,v_v::real)]          " ^

  1095             "                   d2_polyeq_abcFormula_simplify   True)) @@  " ^

  1096             "            (Try (Rewrite_Set polyeq_simplify     False)) @@  " ^

  1097             "            (Try (Rewrite_Set norm_Rational_parenthesized False))) e_e;" ^

  1098             " (L_L::bool list) = ((Or_to_List e_e)::bool list)               " ^

  1099             " in Check_elementwise L_L {(v_v::real). Assumptions} )"),

  1100     Specify.prep_met thy "met_polyeq_d3" [] Celem.e_metID

  1101       (["PolyEq","solve_d3_polyeq_equation"],

  1102         [("#Given" ,["equality e_e","solveFor v_v"]),

  1103           ("#Where" ,["(lhs e_e) is_poly_in v_v ", "((lhs e_e) has_degree_in v_v) = 3"]),

  1104           ("#Find"  ,["solutions v_v'i'"])],

  1105         {rew_ord'="termlessI", rls'=PolyEq_erls, srls=Celem.e_rls, prls=PolyEq_prls,

  1106           calc=[("sqrt", ("NthRoot.sqrt", eval_sqrt "#sqrt_"))], crls=PolyEq_crls, errpats = [],

  1107           nrls = norm_Rational},

  1108         "Script Solve_d3_polyeq_equation  (e_e::bool) (v_v::real) =     " ^

  1109           "  (let e_e = ((Try (Rewrite_Set_Inst [(bdv,v_v::real)]        " ^

  1110           "                    d3_polyeq_simplify           True)) @@  " ^

  1111           "             (Try (Rewrite_Set polyeq_simplify  False)) @@  " ^

  1112           "             (Try (Rewrite_Set_Inst [(bdv,v_v::real)]        " ^

  1113           "                    d2_polyeq_simplify           True)) @@  " ^

  1114           "             (Try (Rewrite_Set polyeq_simplify  False)) @@  " ^

  1115           "             (Try (Rewrite_Set_Inst [(bdv,v_v::real)]        " ^

  1116           "                    d1_polyeq_simplify           True)) @@  " ^

  1117           "             (Try (Rewrite_Set polyeq_simplify  False)) @@  " ^

  1118           "             (Try (Rewrite_Set norm_Rational_parenthesized False))) e_e;" ^

  1119           " (L_L::bool list) = ((Or_to_List e_e)::bool list)             " ^

  1120           " in Check_elementwise L_L {(v_v::real). Assumptions} )"),

  1121     (*.solves all expanded (ie. normalised) terms of degree 2.*)

  1122     (*Oct.02 restriction: 'eval_true 0 =< discriminant' ony for integer values

  1123       by 'PolyEq_erls'; restricted until Float.thy is implemented*)

  1124     Specify.prep_met thy "met_polyeq_complsq" [] Celem.e_metID

  1125       (["PolyEq","complete_square"],

  1126         [("#Given" ,["equality e_e","solveFor v_v"]),

  1127           ("#Where" ,["matches (?a = 0) e_e", "((lhs e_e) has_degree_in v_v) = 2"]),

  1128           ("#Find"  ,["solutions v_v'i'"])],

  1129         {rew_ord'="termlessI",rls'=PolyEq_erls,srls=Celem.e_rls,prls=PolyEq_prls,

  1130           calc=[("sqrt", ("NthRoot.sqrt", eval_sqrt "#sqrt_"))], crls=PolyEq_crls, errpats = [],

  1131           nrls = norm_Rational},

  1132         "Script Complete_square (e_e::bool) (v_v::real) =                         " ^

  1133           "(let e_e = " ^

  1134           "    ((Try (Rewrite_Set_Inst [(bdv,v_v)] cancel_leading_coeff True)) " ^

  1135           "        @@ (Try (Rewrite_Set_Inst [(bdv,v_v)] complete_square True))     " ^

  1136           "        @@ (Try (Rewrite square_explicit1 False))                       " ^

  1137           "        @@ (Try (Rewrite square_explicit2 False))                       " ^

  1138           "        @@ (Rewrite root_plus_minus True)                               " ^

  1139           "        @@ (Try (Repeat (Rewrite_Inst [(bdv,v_v)] bdv_explicit1 False))) " ^

  1140           "        @@ (Try (Repeat (Rewrite_Inst [(bdv,v_v)] bdv_explicit2 False))) " ^

  1141           "        @@ (Try (Repeat                                                 " ^

  1142           "                  (Rewrite_Inst [(bdv,v_v)] bdv_explicit3 False)))       " ^

  1143           "        @@ (Try (Rewrite_Set calculate_RootRat False))                  " ^

  1144           "        @@ (Try (Repeat (Calculate SQRT)))) e_e                         " ^

  1145           " in ((Or_to_List e_e)::bool list))")]

  1146 *}

  1148 ML{*

  1150 (* termorder hacked by MG *)

  1151 local (*. for make_polynomial_in .*)

  1153 open Term;  (* for type order = EQUAL | LESS | GREATER *)

  1155 fun pr_ord EQUAL = "EQUAL"

  1156   | pr_ord LESS  = "LESS"

  1157   | pr_ord GREATER = "GREATER";

  1159 fun dest_hd' x (Const (a, T)) = (((a, 0), T), 0)

  1160   | dest_hd' x (t as Free (a, T)) =

  1161     if x = t then ((("|||||||||||||", 0), T), 0)                        (*WN*)

  1162     else (((a, 0), T), 1)

  1163   | dest_hd' x (Var v) = (v, 2)

  1164   | dest_hd' x (Bound i) = ((("", i), dummyT), 3)

  1165   | dest_hd' x (Abs (_, T, _)) = ((("", 0), T), 4);

  1167 fun size_of_term' x (Const ("Atools.pow",_) $ Free (var,_) $ Free (pot,_)) =

  1168     (case x of                                                          (*WN*)

  1169 	    (Free (xstr,_)) =>

  1170 		(if xstr = var then 1000*(the (TermC.int_of_str_opt pot)) else 3)

  1171 	  | _ => error ("size_of_term' called with subst = "^

  1172 			      (Celem.term2str x)))

  1173   | size_of_term' x (Free (subst,_)) =

  1174     (case x of

  1175 	    (Free (xstr,_)) => (if xstr = subst then 1000 else 1)

  1176 	  | _ => error ("size_of_term' called with subst = "^

  1177 			  (Celem.term2str x)))

  1178   | size_of_term' x (Abs (_,_,body)) = 1 + size_of_term' x body

  1179   | size_of_term' x (f$t) = size_of_term' x f  +  size_of_term' x t

  1180   | size_of_term' x _ = 1;

  1182 fun term_ord' x pr thy (Abs (_, T, t), Abs(_, U, u)) =       (* ~ term.ML *)

  1183     (case term_ord' x pr thy (t, u) of EQUAL => Term_Ord.typ_ord (T, U) | ord => ord)

  1184   | term_ord' x pr thy (t, u) =

  1185     (if pr

  1186      then

  1187        let

  1188          val (f, ts) = strip_comb t and (g, us) = strip_comb u;

  1189          val _ = tracing ("t= f@ts= \"" ^ Celem.term_to_string''' thy f ^ "\" @ \"[" ^

  1190            commas (map (Celem.term_to_string''' thy) ts) ^ "]\"");

  1191          val _ = tracing ("u= g@us= \"" ^ Celem.term_to_string''' thy g ^ "\" @ \"[" ^

  1192            commas(map (Celem.term_to_string''' thy) us) ^ "]\"");

  1193          val _ = tracing ("size_of_term(t,u)= (" ^ string_of_int (size_of_term' x t) ^ ", " ^

  1194            string_of_int (size_of_term' x u) ^ ")");

  1195          val _ = tracing ("hd_ord(f,g)      = " ^ (pr_ord o (hd_ord x)) (f,g));

  1196          val _ = tracing ("terms_ord(ts,us) = " ^ (pr_ord o (terms_ord x) str false) (ts, us));

  1197          val _ = tracing ("-------");

  1198        in () end

  1199      else ();

  1200 	  case int_ord (size_of_term' x t, size_of_term' x u) of

  1201 	    EQUAL =>

  1202 	      let val (f, ts) = strip_comb t and (g, us) = strip_comb u

  1203         in

  1204 	        (case hd_ord x (f, g) of

  1205 	           EQUAL => (terms_ord x str pr) (ts, us)

  1206 	         | ord => ord)

  1207 	      end

  1208 	 | ord => ord)

  1209 and hd_ord x (f, g) =                                        (* ~ term.ML *)

  1210   prod_ord (prod_ord Term_Ord.indexname_ord Term_Ord.typ_ord)

  1211             int_ord (dest_hd' x f, dest_hd' x g)

  1212 and terms_ord x str pr (ts, us) =

  1213     list_ord (term_ord' x pr (Celem.assoc_thy "Isac"))(ts, us);

  1215 in

  1217 fun ord_make_polynomial_in (pr:bool) thy subst tu =

  1218     let

  1219 	(* val _=tracing("*** subs variable is: "^(Celem.subst2str subst)); *)

  1220     in

  1221 	case subst of

  1222 	    (_,x)::_ => (term_ord' x pr thy tu = LESS)

  1223 	  | _ => error ("ord_make_polynomial_in called with subst = "^

  1224 			  (Celem.subst2str subst))

  1225     end;

  1226 end;(*local*)

  1228 *}

  1229 ML{*

  1230 val order_add_mult_in = prep_rls'(

  1231   Celem.Rls{id = "order_add_mult_in", preconds = [],

  1232       rew_ord = ("ord_make_polynomial_in",

  1233 		 ord_make_polynomial_in false @{theory "Poly"}),

  1234       erls = Celem.e_rls,srls = Celem.Erls,

  1235       calc = [], errpatts = [],

  1236       rules = [Celem.Thm ("mult_commute",TermC.num_str @{thm mult.commute}),

  1237 	       (* z * w = w * z *)

  1238 	       Celem.Thm ("real_mult_left_commute",TermC.num_str @{thm real_mult_left_commute}),

  1239 	       (*z1.0 * (z2.0 * z3.0) = z2.0 * (z1.0 * z3.0)*)

  1240 	       Celem.Thm ("mult_assoc",TermC.num_str @{thm mult.assoc}),

  1241 	       (*z1.0 * z2.0 * z3.0 = z1.0 * (z2.0 * z3.0)*)

  1242 	       Celem.Thm ("add_commute",TermC.num_str @{thm add.commute}),

  1243 	       (*z + w = w + z*)

  1244 	       Celem.Thm ("add_left_commute",TermC.num_str @{thm add.left_commute}),

  1245 	       (*x + (y + z) = y + (x + z)*)

  1246 	       Celem.Thm ("add_assoc",TermC.num_str @{thm add.assoc})

  1247 	       (*z1.0 + z2.0 + z3.0 = z1.0 + (z2.0 + z3.0)*)

  1248 	       ], scr = Celem.EmptyScr});

  1250 *}

  1251 ML{*

  1252 val collect_bdv = prep_rls'(

  1253   Celem.Rls{id = "collect_bdv", preconds = [],

  1254       rew_ord = ("dummy_ord", Celem.dummy_ord),

  1255       erls = Celem.e_rls,srls = Celem.Erls,

  1256       calc = [], errpatts = [],

  1257       rules = [Celem.Thm ("bdv_collect_1",TermC.num_str @{thm bdv_collect_1}),

  1258 	       Celem.Thm ("bdv_collect_2",TermC.num_str @{thm bdv_collect_2}),

  1259 	       Celem.Thm ("bdv_collect_3",TermC.num_str @{thm bdv_collect_3}),

  1261 	       Celem.Thm ("bdv_collect_assoc1_1",TermC.num_str @{thm bdv_collect_assoc1_1}),

  1262 	       Celem.Thm ("bdv_collect_assoc1_2",TermC.num_str @{thm bdv_collect_assoc1_2}),

  1263 	       Celem.Thm ("bdv_collect_assoc1_3",TermC.num_str @{thm bdv_collect_assoc1_3}),

  1265 	       Celem.Thm ("bdv_collect_assoc2_1",TermC.num_str @{thm bdv_collect_assoc2_1}),

  1266 	       Celem.Thm ("bdv_collect_assoc2_2",TermC.num_str @{thm bdv_collect_assoc2_2}),

  1267 	       Celem.Thm ("bdv_collect_assoc2_3",TermC.num_str @{thm bdv_collect_assoc2_3}),

  1270 	       Celem.Thm ("bdv_n_collect_1",TermC.num_str @{thm bdv_n_collect_1}),

  1271 	       Celem.Thm ("bdv_n_collect_2",TermC.num_str @{thm bdv_n_collect_2}),

  1272 	       Celem.Thm ("bdv_n_collect_3",TermC.num_str @{thm bdv_n_collect_3}),

  1274 	       Celem.Thm ("bdv_n_collect_assoc1_1",TermC.num_str @{thm bdv_n_collect_assoc1_1}),

  1275 	       Celem.Thm ("bdv_n_collect_assoc1_2",TermC.num_str @{thm bdv_n_collect_assoc1_2}),

  1276 	       Celem.Thm ("bdv_n_collect_assoc1_3",TermC.num_str @{thm bdv_n_collect_assoc1_3}),

  1278 	       Celem.Thm ("bdv_n_collect_assoc2_1",TermC.num_str @{thm bdv_n_collect_assoc2_1}),

  1279 	       Celem.Thm ("bdv_n_collect_assoc2_2",TermC.num_str @{thm bdv_n_collect_assoc2_2}),

  1280 	       Celem.Thm ("bdv_n_collect_assoc2_3",TermC.num_str @{thm bdv_n_collect_assoc2_3})

  1281 	       ], scr = Celem.EmptyScr});

  1283 *}

  1284 ML{*

  1285 (*.transforms an arbitrary term without roots to a polynomial [4]

  1286    according to knowledge/Poly.sml.*)

  1287 val make_polynomial_in = prep_rls'(

  1288   Celem.Seq {id = "make_polynomial_in", preconds = []:term list,

  1289        rew_ord = ("dummy_ord", Celem.dummy_ord),

  1290       erls = Atools_erls, srls = Celem.Erls,

  1291       calc = [], errpatts = [],

  1292       rules = [Celem.Rls_ expand_poly,

  1293 	       Celem.Rls_ order_add_mult_in,

  1294 	       Celem.Rls_ simplify_power,

  1295 	       Celem.Rls_ collect_numerals,

  1296 	       Celem.Rls_ reduce_012,

  1297 	       Celem.Thm ("realpow_oneI",TermC.num_str @{thm realpow_oneI}),

  1298 	       Celem.Rls_ discard_parentheses,

  1299 	       Celem.Rls_ collect_bdv

  1300 	       ],

  1301       scr = Celem.EmptyScr

  1302       });

  1304 *}

  1305 ML{*

  1306 val separate_bdvs =

  1307     Celem.append_rls "separate_bdvs"

  1308 	       collect_bdv

  1309 	       [Celem.Thm ("separate_bdv", TermC.num_str @{thm separate_bdv}),

  1310 		(*"?a * ?bdv / ?b = ?a / ?b * ?bdv"*)

  1311 		Celem.Thm ("separate_bdv_n", TermC.num_str @{thm separate_bdv_n}),

  1312 		Celem.Thm ("separate_1_bdv", TermC.num_str @{thm separate_1_bdv}),

  1313 		(*"?bdv / ?b = (1 / ?b) * ?bdv"*)

  1314 		Celem.Thm ("separate_1_bdv_n", TermC.num_str @{thm separate_1_bdv_n}),

  1315 		(*"?bdv ^^^ ?n / ?b = 1 / ?b * ?bdv ^^^ ?n"*)

  1316 		Celem.Thm ("add_divide_distrib",

  1317 		     TermC.num_str @{thm add_divide_distrib})

  1318 		(*"(?x + ?y) / ?z = ?x / ?z + ?y / ?z"

  1319 		      WN051031 DOES NOT BELONG TO HERE*)

  1320 		];

  1321 *}

  1322 ML{*

  1323 val make_ratpoly_in = prep_rls'(

  1324   Celem.Seq {id = "make_ratpoly_in", preconds = []:term list,

  1325        rew_ord = ("dummy_ord", Celem.dummy_ord),

  1326       erls = Atools_erls, srls = Celem.Erls,

  1327       calc = [], errpatts = [],

  1328       rules = [Celem.Rls_ norm_Rational,

  1329 	       Celem.Rls_ order_add_mult_in,

  1330 	       Celem.Rls_ discard_parentheses,

  1331 	       Celem.Rls_ separate_bdvs,

  1332 	       (* Celem.Rls_ rearrange_assoc, WN060916 why does cancel_p not work?*)

  1333 	       Celem.Rls_ cancel_p

  1334 	       (*Celem.Calc ("Rings.divide_class.divide"  ,eval_cancel "#divide_e") too weak!*)

  1335 	       ],

  1336       scr = Celem.EmptyScr});

  1337 *}

  1338 setup {* KEStore_Elems.add_rlss

  1339   [("order_add_mult_in", (Context.theory_name @{theory}, order_add_mult_in)),

  1340   ("collect_bdv", (Context.theory_name @{theory}, collect_bdv)),

  1341   ("make_polynomial_in", (Context.theory_name @{theory}, make_polynomial_in)),

  1342   ("make_ratpoly_in", (Context.theory_name @{theory}, make_ratpoly_in)),

  1343   ("separate_bdvs", (Context.theory_name @{theory}, separate_bdvs))] *}

  1345 end

author	Walther Neuper <wneuper@ist.tugraz.at>
	Thu, 15 Mar 2018 12:42:04 +0100
changeset 59406	509d70b507e5
parent 59390	f6374c995ac5
child 59411	3e241a6938ce
permissions	-rw-r--r--