wneuper/isa: src/Tools/isac/Knowledge/PolyEq.thy@73dc85c025ab

     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 (_ _ =))//

    22                   (_))" 9)

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

    24   Normalize'_poly

    25              :: "[bool,real,

    26 		   bool list] => bool list"

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

    28                   (_))" 9)

    29   Solve'_d0'_polyeq'_equation

    30              :: "[bool,real,

    31 		   bool list] => bool list"

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

    33                   (_))" 9)

    34   Solve'_d1'_polyeq'_equation

    35              :: "[bool,real,

    36 		   bool list] => bool list"

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

    38                   (_))" 9)

    39   Solve'_d2'_polyeq'_equation

    40              :: "[bool,real,

    41 		   bool list] => bool list"

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

    43                   (_))" 9)

    44   Solve'_d2'_polyeq'_sqonly'_equation

    45              :: "[bool,real,

    46 		   bool list] => bool list"

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

    48                   (_))" 9)

    49   Solve'_d2'_polyeq'_bdvonly'_equation

    50              :: "[bool,real,

    51 		   bool list] => bool list"

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

    53                   (_))" 9)

    54   Solve'_d2'_polyeq'_pq'_equation

    55              :: "[bool,real,

    56 		   bool list] => bool list"

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

    58                   (_))" 9)

    59   Solve'_d2'_polyeq'_abc'_equation

    60              :: "[bool,real,

    61 		   bool list] => bool list"

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

    63                   (_))" 9)

    64   Solve'_d3'_polyeq'_equation

    65              :: "[bool,real,

    66 		   bool list] => bool list"

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

    68                   (_))" 9)

    69   Solve'_d4'_polyeq'_equation

    70              :: "[bool,real,

    71 		   bool list] => bool list"

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

    73                   (_))" 9)

    74   Biquadrat'_poly

    75              :: "[bool,real,

    76 		   bool list] => bool list"

    77                ("((Script Biquadrat'_poly (_ _=))//

    78                   (_))" 9)

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

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

    82 axiomatization where

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

   137 (*-- normalize --*)

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

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

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

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

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

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

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

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

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

   148   d1_isolate_add1:

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

   150   d1_isolate_add2:

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

   152   d1_isolate_div:

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

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

   155   d2_isolate_add1:

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

   157   d2_isolate_add2:

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

   159   d2_isolate_div:

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

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

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

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

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

   166   (* eliminate degree 2 *)

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

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

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

   170  d2_sqrt_equation1_neg:

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

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

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

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

   175   exception PTREE "nth _ []" raised

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

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

   178 and

   179   exception Bind raised

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

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

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

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

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

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

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

   188   exception PTREE "nth _ []" raised

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

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

   191 and

   192   exception Bind raised

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

   230   d2_pqformula9_neg:

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

   232   d2_pqformula10:

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

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

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

   236   d2_pqformula10_neg:

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

   238   d2_abcformula1:

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

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

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

   242   d2_abcformula1_neg:

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

   244   d2_abcformula2:

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

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

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

   248   d2_abcformula2_neg:

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

   250   d2_abcformula3:

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

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

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

   254   d2_abcformula3_neg:

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

   256   d2_abcformula4:

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

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

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

   260   d2_abcformula4_neg:

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

   262   d2_abcformula5:

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

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

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

   266   d2_abcformula5_neg:

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

   268   d2_abcformula6:

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

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

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

   272   d2_abcformula6_neg:

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

   274   d2_abcformula7:

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

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

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

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

   279   d2_abcformula8:

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

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

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

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

   284   d2_abcformula9:

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

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

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

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

   289   d2_abcformula10:

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

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

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

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

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

   297   d3_reduce_equation1:

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

   299   d3_reduce_equation2:

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

   301   d3_reduce_equation3:

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

   303   d3_reduce_equation4:

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

   305   d3_reduce_equation5:

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

   307   d3_reduce_equation6:

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

   309   d3_reduce_equation7:

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

   311   d3_reduce_equation8:

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

   313   d3_reduce_equation9:

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

   315   d3_reduce_equation10:

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

   317   d3_reduce_equation11:

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

   319   d3_reduce_equation12:

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

   321   d3_reduce_equation13:

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

   323   d3_reduce_equation14:

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

   325   d3_reduce_equation15:

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

   327   d3_reduce_equation16:

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

   329   d3_isolate_add1:

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

   331   d3_isolate_add2:

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

   333   d3_isolate_div:

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

   335   d3_root_equation2:

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

   337   d3_root_equation1:

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

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

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

   342  d4_sub_u1:

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

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

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

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

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

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

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

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

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

   355 *)

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

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

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

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

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

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

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

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

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

   369   bdv_n_collect_assoc1_1:

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

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

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

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

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

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

   378 (*WN.14.3.03*)

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

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

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

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

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

   386 ML {*

   387 val thy = @{theory};

   389 (*-------------------------rulse-------------------------*)

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

   391   append_rls "PolyEq_prls" e_rls

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

   393 	      Calc ("Tools.matches",eval_matches ""),

   394 	      Calc ("Tools.lhs"    ,eval_lhs ""),

   395 	      Calc ("Tools.rhs"    ,eval_rhs ""),

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

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

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

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

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

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

   402 	      Calc ("HOL.eq",eval_equal "#equal_"),

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

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

   405 	      Thm ("not_true",num_str @{thm not_true}),

   406 	      Thm ("not_false",num_str @{thm not_false}),

   407 	      Thm ("and_true",num_str @{thm and_true}),

   408 	      Thm ("and_false",num_str @{thm and_false}),

   409 	      Thm ("or_true",num_str @{thm or_true}),

   410 	      Thm ("or_false",num_str @{thm or_false})

   411 	       ];

   413 val PolyEq_erls =

   414     merge_rls "PolyEq_erls" LinEq_erls

   415     (append_rls "ops_preds" calculate_Rational

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

   417 		 Thm ("plus_leq", num_str @{thm plus_leq}),

   418 		 Thm ("minus_leq", num_str @{thm minus_leq}),

   419 		 Thm ("rat_leq1", num_str @{thm rat_leq1}),

   420 		 Thm ("rat_leq2", num_str @{thm rat_leq2}),

   421 		 Thm ("rat_leq3", num_str @{thm rat_leq3})

   422 		 ]);

   424 val PolyEq_crls =

   425     merge_rls "PolyEq_crls" LinEq_crls

   426     (append_rls "ops_preds" calculate_Rational

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

   428 		 Thm ("plus_leq", num_str @{thm plus_leq}),

   429 		 Thm ("minus_leq", num_str @{thm minus_leq}),

   430 		 Thm ("rat_leq1", num_str @{thm rat_leq1}),

   431 		 Thm ("rat_leq2", num_str @{thm rat_leq2}),

   432 		 Thm ("rat_leq3", num_str @{thm rat_leq3})

   433 		 ]);

   435 val cancel_leading_coeff = prep_rls(

   436   Rls {id = "cancel_leading_coeff", preconds = [],

   437        rew_ord = ("e_rew_ord",e_rew_ord),

   438       erls = PolyEq_erls, srls = Erls, calc = [], errpatts = [],

   439       rules =

   440       [Thm ("cancel_leading_coeff1",num_str @{thm cancel_leading_coeff1}),

   441        Thm ("cancel_leading_coeff2",num_str @{thm cancel_leading_coeff2}),

   442        Thm ("cancel_leading_coeff3",num_str @{thm cancel_leading_coeff3}),

   443        Thm ("cancel_leading_coeff4",num_str @{thm cancel_leading_coeff4}),

   444        Thm ("cancel_leading_coeff5",num_str @{thm cancel_leading_coeff5}),

   445        Thm ("cancel_leading_coeff6",num_str @{thm cancel_leading_coeff6}),

   446        Thm ("cancel_leading_coeff7",num_str @{thm cancel_leading_coeff7}),

   447        Thm ("cancel_leading_coeff8",num_str @{thm cancel_leading_coeff8}),

   448        Thm ("cancel_leading_coeff9",num_str @{thm cancel_leading_coeff9}),

   449        Thm ("cancel_leading_coeff10",num_str @{thm cancel_leading_coeff10}),

   450        Thm ("cancel_leading_coeff11",num_str @{thm cancel_leading_coeff11}),

   451        Thm ("cancel_leading_coeff12",num_str @{thm cancel_leading_coeff12}),

   452        Thm ("cancel_leading_coeff13",num_str @{thm cancel_leading_coeff13})

   453        ],scr = Prog ((term_of o the o (parse thy)) "empty_script")}:rls);

   454 *}

   455 ML{*

   456 val complete_square = prep_rls(

   457   Rls {id = "complete_square", preconds = [],

   458        rew_ord = ("e_rew_ord",e_rew_ord),

   459       erls = PolyEq_erls, srls = Erls, calc = [],  errpatts = [],

   460       rules = [Thm ("complete_square1",num_str @{thm complete_square1}),

   461 	       Thm ("complete_square2",num_str @{thm complete_square2}),

   462 	       Thm ("complete_square3",num_str @{thm complete_square3}),

   463 	       Thm ("complete_square4",num_str @{thm complete_square4}),

   464 	       Thm ("complete_square5",num_str @{thm complete_square5})

   465 	       ],

   466       scr = Prog ((term_of o the o (parse thy)) "empty_script")

   467       }:rls);

   469 val polyeq_simplify = prep_rls(

   470   Rls {id = "polyeq_simplify", preconds = [],

   471        rew_ord = ("termlessI",termlessI),

   472        erls = PolyEq_erls,

   473        srls = Erls,

   474        calc = [], errpatts = [],

   475        rules = [Thm  ("real_assoc_1",num_str @{thm real_assoc_1}),

   476 		Thm  ("real_assoc_2",num_str @{thm real_assoc_2}),

   477 		Thm  ("real_diff_minus",num_str @{thm real_diff_minus}),

   478 		Thm  ("real_unari_minus",num_str @{thm real_unari_minus}),

   479 		Thm  ("realpow_multI",num_str @{thm realpow_multI}),

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

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

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

   483 		Calc ("Fields.inverse_class.divide", eval_cancel "#divide_e"),

   484 		Calc ("NthRoot.sqrt",eval_sqrt "#sqrt_"),

   485 		Calc ("Atools.pow" ,eval_binop "#power_"),

   486                 Rls_ reduce_012

   487                 ],

   488        scr = Prog ((term_of o the o (parse thy)) "empty_script")

   489        }:rls);

   490 *}

   491 setup {* KEStore_Elems.add_rlss

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

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

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

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

   496 ML{*

   498 (* ------------- polySolve ------------------ *)

   499 (* -- d0 -- *)

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

   501 val d0_polyeq_simplify = prep_rls(

   502   Rls {id = "d0_polyeq_simplify", preconds = [],

   503        rew_ord = ("e_rew_ord",e_rew_ord),

   504        erls = PolyEq_erls,

   505        srls = Erls,

   506        calc = [], errpatts = [],

   507        rules = [Thm("d0_true",num_str @{thm d0_true}),

   508 		Thm("d0_false",num_str @{thm  d0_false})

   509 		],

   510        scr = Prog ((term_of o the o (parse thy)) "empty_script")

   511        }:rls);

   513 (* -- d1 -- *)

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

   515 val d1_polyeq_simplify = prep_rls(

   516   Rls {id = "d1_polyeq_simplify", preconds = [],

   517        rew_ord = ("e_rew_ord",e_rew_ord),

   518        erls = PolyEq_erls,

   519        srls = Erls,

   520        calc = [], errpatts = [],

   521        rules = [

   522 		Thm("d1_isolate_add1",num_str @{thm d1_isolate_add1}),

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

   524 		Thm("d1_isolate_add2",num_str @{thm d1_isolate_add2}),

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

   526 		Thm("d1_isolate_div",num_str @{thm d1_isolate_div})

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

   528 		],

   529        scr = Prog ((term_of o the o (parse thy)) "empty_script")

   530        }:rls);

   532 *}

   533 subsection {* degree 2 *}

   534 ML{*

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

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

   537 val d2_polyeq_bdv_only_simplify = prep_rls(

   538   Rls {id = "d2_polyeq_bdv_only_simplify", preconds = [], rew_ord = ("e_rew_ord",e_rew_ord),

   539     erls = PolyEq_erls, srls = Erls, calc = [], errpatts = [],

   540     rules =

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

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

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

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

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

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

   547        Thm ("d2_sqrt_equation2", num_str @{thm d2_sqrt_equation2}),    (*  x^2=0 ->    x=0       *)

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

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

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

   551        ],

   552        scr = Prog ((term_of o the o (parse thy)) "empty_script")

   553        }:rls);

   554 *}

   555 ML{*

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

   557    'bdv' is a meta-constant*)

   558 val d2_polyeq_sq_only_simplify = prep_rls(

   559   Rls {id = "d2_polyeq_sq_only_simplify", preconds = [],

   560        rew_ord = ("e_rew_ord",e_rew_ord),

   561        erls = PolyEq_erls,

   562        srls = Erls,

   563        calc = [], errpatts = [],

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

   565                   ("d2_isolate_div","")],*)

   566        rules = [Thm("d2_isolate_add1",num_str @{thm d2_isolate_add1}),

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

   568 		Thm("d2_isolate_add2",num_str @{thm d2_isolate_add2}),

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

   570 		Thm("d2_sqrt_equation2",num_str @{thm d2_sqrt_equation2}),

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

   572 		Thm("d2_sqrt_equation1",num_str @{thm d2_sqrt_equation1}),

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

   574 		Thm("d2_sqrt_equation1_neg",num_str @{thm d2_sqrt_equation1_neg}),

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

   576 		Thm("d2_isolate_div",num_str @{thm d2_isolate_div})

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

   578 		],

   579        scr = Prog ((term_of o the o (parse thy)) "empty_script")

   580        }:rls);

   581 *}

   582 ML{*

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

   584    'bdv' is a meta-constant*)

   585 val d2_polyeq_pqFormula_simplify = prep_rls(

   586   Rls {id = "d2_polyeq_pqFormula_simplify", preconds = [],

   587        rew_ord = ("e_rew_ord",e_rew_ord), erls = PolyEq_erls,

   588        srls = Erls, calc = [], errpatts = [],

   589        rules = [Thm("d2_pqformula1",num_str @{thm d2_pqformula1}),

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

   591 		Thm("d2_pqformula1_neg",num_str @{thm d2_pqformula1_neg}),

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

   593 		Thm("d2_pqformula2",num_str @{thm d2_pqformula2}),

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

   595 		Thm("d2_pqformula2_neg",num_str @{thm d2_pqformula2_neg}),

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

   597 		Thm("d2_pqformula3",num_str @{thm d2_pqformula3}),

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

   599 		Thm("d2_pqformula3_neg",num_str @{thm d2_pqformula3_neg}),

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

   601 		Thm("d2_pqformula4",num_str @{thm d2_pqformula4}),

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

   603 		Thm("d2_pqformula4_neg",num_str @{thm d2_pqformula4_neg}),

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

   605 		Thm("d2_pqformula5",num_str @{thm d2_pqformula5}),

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

   607 		Thm("d2_pqformula6",num_str @{thm d2_pqformula6}),

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

   609 		Thm("d2_pqformula7",num_str @{thm d2_pqformula7}),

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

   611 		Thm("d2_pqformula8",num_str @{thm d2_pqformula8}),

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

   613 		Thm("d2_pqformula9",num_str @{thm d2_pqformula9}),

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

   615 		Thm("d2_pqformula9_neg",num_str @{thm d2_pqformula9_neg}),

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

   617 		Thm("d2_pqformula10",num_str @{thm d2_pqformula10}),

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

   619 		Thm("d2_pqformula10_neg",num_str @{thm d2_pqformula10_neg}),

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

   621 		Thm("d2_sqrt_equation2",num_str @{thm d2_sqrt_equation2}),

   622                 (*       x^2=0 *)

   623 		Thm("d2_sqrt_equation3",num_str @{thm d2_sqrt_equation3})

   624                (*      1x^2=0 *)

   625 	       ],scr = Prog ((term_of o the o (parse thy)) "empty_script")

   626        }:rls);

   627 *}

   628 ML{*

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

   630    'bdv' is a meta-constant*)

   631 val d2_polyeq_abcFormula_simplify = prep_rls(

   632   Rls {id = "d2_polyeq_abcFormula_simplify", preconds = [],

   633        rew_ord = ("e_rew_ord",e_rew_ord), erls = PolyEq_erls,

   634        srls = Erls, calc = [], errpatts = [],

   635        rules = [Thm("d2_abcformula1",num_str @{thm d2_abcformula1}),

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

   637 		Thm("d2_abcformula1_neg",num_str @{thm d2_abcformula1_neg}),

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

   639 		Thm("d2_abcformula2",num_str @{thm d2_abcformula2}),

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

   641 		Thm("d2_abcformula2_neg",num_str @{thm d2_abcformula2_neg}),

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

   643 		Thm("d2_abcformula3",num_str @{thm d2_abcformula3}),

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

   645 		Thm("d2_abcformula3_neg",num_str @{thm d2_abcformula3_neg}),

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

   647 		Thm("d2_abcformula4",num_str @{thm d2_abcformula4}),

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

   649 		Thm("d2_abcformula4_neg",num_str @{thm d2_abcformula4_neg}),

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

   651 		Thm("d2_abcformula5",num_str @{thm d2_abcformula5}),

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

   653 		Thm("d2_abcformula5_neg",num_str @{thm d2_abcformula5_neg}),

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

   655 		Thm("d2_abcformula6",num_str @{thm d2_abcformula6}),

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

   657 		Thm("d2_abcformula6_neg",num_str @{thm d2_abcformula6_neg}),

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

   659 		Thm("d2_abcformula7",num_str @{thm d2_abcformula7}),

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

   661 		Thm("d2_abcformula8",num_str @{thm d2_abcformula8}),

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

   663 		Thm("d2_abcformula9",num_str @{thm d2_abcformula9}),

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

   665 		Thm("d2_abcformula10",num_str @{thm d2_abcformula10}),

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

   667 		Thm("d2_sqrt_equation2",num_str @{thm d2_sqrt_equation2}),

   668                 (*      x^2=0 *)

   669 		Thm("d2_sqrt_equation3",num_str @{thm d2_sqrt_equation3})

   670                (*     bx^2=0 *)

   671 	       ],

   672        scr = Prog ((term_of o the o (parse thy)) "empty_script")

   673        }:rls);

   674 *}

   675 ML{*

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

   678    'bdv' is a meta-constant*)

   679 val d2_polyeq_simplify = prep_rls(

   680   Rls {id = "d2_polyeq_simplify", preconds = [],

   681        rew_ord = ("e_rew_ord",e_rew_ord), erls = PolyEq_erls,

   682        srls = Erls, calc = [], errpatts = [],

   683        rules = [Thm("d2_pqformula1",num_str @{thm d2_pqformula1}),

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

   685 		Thm("d2_pqformula1_neg",num_str @{thm d2_pqformula1_neg}),

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

   687 		Thm("d2_pqformula2",num_str @{thm d2_pqformula2}),

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

   689 		Thm("d2_pqformula2_neg",num_str @{thm d2_pqformula2_neg}),

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

   691 		Thm("d2_pqformula3",num_str @{thm d2_pqformula3}),

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

   693 		Thm("d2_pqformula3_neg",num_str @{thm d2_pqformula3_neg}),

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

   695 		Thm("d2_pqformula4",num_str @{thm d2_pqformula4}),

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

   697 		Thm("d2_pqformula4_neg",num_str @{thm d2_pqformula4_neg}),

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

   699 		Thm("d2_abcformula1",num_str @{thm d2_abcformula1}),

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

   701 		Thm("d2_abcformula1_neg",num_str @{thm d2_abcformula1_neg}),

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

   703 		Thm("d2_abcformula2",num_str @{thm d2_abcformula2}),

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

   705 		Thm("d2_abcformula2_neg",num_str @{thm d2_abcformula2_neg}),

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

   707 		Thm("d2_prescind1",num_str @{thm d2_prescind1}),

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

   709 		Thm("d2_prescind2",num_str @{thm d2_prescind2}),

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

   711 		Thm("d2_prescind3",num_str @{thm d2_prescind3}),

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

   713 		Thm("d2_prescind4",num_str @{thm d2_prescind4}),

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

   715 		Thm("d2_isolate_add1",num_str @{thm d2_isolate_add1}),

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

   717 		Thm("d2_isolate_add2",num_str @{thm d2_isolate_add2}),

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

   719 		Thm("d2_sqrt_equation1",num_str @{thm d2_sqrt_equation1}),

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

   721 		Thm("d2_sqrt_equation1_neg",num_str @{thm d2_sqrt_equation1_neg}),

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

   723 		Thm("d2_sqrt_equation2",num_str @{thm d2_sqrt_equation2}),

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

   725 		Thm("d2_reduce_equation1",num_str @{thm d2_reduce_equation1}),

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

   727 		Thm("d2_reduce_equation2",num_str @{thm d2_reduce_equation2}),

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

   729 		Thm("d2_isolate_div",num_str @{thm d2_isolate_div})

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

   731 	       ],

   732        scr = Prog ((term_of o the o (parse thy)) "empty_script")

   733       }:rls);

   734 *}

   735 ML{*

   737 (* -- d3 -- *)

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

   739 val d3_polyeq_simplify = prep_rls(

   740   Rls {id = "d3_polyeq_simplify", preconds = [],

   741        rew_ord = ("e_rew_ord",e_rew_ord), erls = PolyEq_erls,

   742        srls = Erls, calc = [], errpatts = [],

   743        rules =

   744        [Thm("d3_reduce_equation1",num_str @{thm d3_reduce_equation1}),

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

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

   747 	Thm("d3_reduce_equation2",num_str @{thm d3_reduce_equation2}),

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

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

   750 	Thm("d3_reduce_equation3",num_str @{thm d3_reduce_equation3}),

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

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

   753 	Thm("d3_reduce_equation4",num_str @{thm d3_reduce_equation4}),

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

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

   756 	Thm("d3_reduce_equation5",num_str @{thm d3_reduce_equation5}),

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

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

   759 	Thm("d3_reduce_equation6",num_str @{thm d3_reduce_equation6}),

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

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

   762 	Thm("d3_reduce_equation7",num_str @{thm d3_reduce_equation7}),

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

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

   765 	Thm("d3_reduce_equation8",num_str @{thm d3_reduce_equation8}),

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

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

   768 	Thm("d3_reduce_equation9",num_str @{thm d3_reduce_equation9}),

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

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

   771 	Thm("d3_reduce_equation10",num_str @{thm d3_reduce_equation10}),

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

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

   774 	Thm("d3_reduce_equation11",num_str @{thm d3_reduce_equation11}),

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

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

   777 	Thm("d3_reduce_equation12",num_str @{thm d3_reduce_equation12}),

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

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

   780 	Thm("d3_reduce_equation13",num_str @{thm d3_reduce_equation13}),

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

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

   783 	Thm("d3_reduce_equation14",num_str @{thm d3_reduce_equation14}),

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

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

   786 	Thm("d3_reduce_equation15",num_str @{thm d3_reduce_equation15}),

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

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

   789 	Thm("d3_reduce_equation16",num_str @{thm d3_reduce_equation16}),

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

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

   792 	Thm("d3_isolate_add1",num_str @{thm d3_isolate_add1}),

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

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

   795 	Thm("d3_isolate_add2",num_str @{thm d3_isolate_add2}),

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

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

   798 	Thm("d3_isolate_div",num_str @{thm d3_isolate_div}),

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

   800         Thm("d3_root_equation2",num_str @{thm d3_root_equation2}),

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

   802 	Thm("d3_root_equation1",num_str @{thm d3_root_equation1})

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

   804        ],

   805        scr = Prog ((term_of o the o (parse thy)) "empty_script")

   806       }:rls);

   807 *}

   808 ML{*

   810 (* -- d4 -- *)

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

   812 val d4_polyeq_simplify = prep_rls(

   813   Rls {id = "d4_polyeq_simplify", preconds = [],

   814        rew_ord = ("e_rew_ord",e_rew_ord), erls = PolyEq_erls,

   815        srls = Erls, calc = [], errpatts = [],

   816        rules =

   817        [Thm("d4_sub_u1",num_str @{thm d4_sub_u1})

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

   819        ],

   820        scr = Prog ((term_of o the o (parse thy)) "empty_script")

   821       }:rls);

   822 *}

   823 setup {* KEStore_Elems.add_rlss

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

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

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

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

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

   830   ("d2_polyeq_pqFormula_simplify",

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

   832   ("d2_polyeq_abcFormula_simplify",

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

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

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

   836 ML{*

   838 (*------------------------problems------------------------*)

   839 (*

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

   841 show_ptyps();

   842 *)

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

   845 store_pbt

   846  (prep_pbt thy "pbl_equ_univ_poly" [] e_pblID

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

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

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

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

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

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

   853    ],

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

   855   []));

   856 (*--- d0 ---*)

   857 store_pbt

   858  (prep_pbt thy "pbl_equ_univ_poly_deg0" [] e_pblID

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

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

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

   862 	       "(lhs e_e) is_poly_in v_v",

   863 	       "((lhs e_e) has_degree_in v_v ) = 0"

   864 	      ]),

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

   866   ],

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

   868   [["PolyEq","solve_d0_polyeq_equation"]]));

   870 (*--- d1 ---*)

   871 store_pbt

   872  (prep_pbt thy "pbl_equ_univ_poly_deg1" [] e_pblID

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

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

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

   876 	       "(lhs e_e) is_poly_in v_v",

   877 	       "((lhs e_e) has_degree_in v_v ) = 1"

   878 	      ]),

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

   880   ],

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

   882   [["PolyEq","solve_d1_polyeq_equation"]]));

   883 *}

   884 ML{*

   885 (*--- d2 ---*)

   886 store_pbt

   887  (prep_pbt thy "pbl_equ_univ_poly_deg2" [] e_pblID

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

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

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

   891 	       "(lhs e_e) is_poly_in v_v ",

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

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

   894   ],

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

   896   [["PolyEq","solve_d2_polyeq_equation"]]));

   898  store_pbt

   899  (prep_pbt thy "pbl_equ_univ_poly_deg2_sqonly" [] e_pblID

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

   915   ],

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

   917   [["PolyEq","solve_d2_polyeq_sqonly_equation"]]));

   919 store_pbt

   920  (prep_pbt thy "pbl_equ_univ_poly_deg2_bdvonly" [] e_pblID

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

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

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

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

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

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

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

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

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

   930   ],

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

   932   [["PolyEq","solve_d2_polyeq_bdvonly_equation"]]));

   934 store_pbt

   935  (prep_pbt thy "pbl_equ_univ_poly_deg2_pq" [] e_pblID

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

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

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

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

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

   941   ],

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

   943   [["PolyEq","solve_d2_polyeq_pq_equation"]]));

   945 store_pbt

   946  (prep_pbt thy "pbl_equ_univ_poly_deg2_abc" [] e_pblID

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

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

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

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

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

   952   ],

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

   954   [["PolyEq","solve_d2_polyeq_abc_equation"]]));

   955 *}

   956 ML{*

   957 (*--- d3 ---*)

   958 store_pbt

   959  (prep_pbt thy "pbl_equ_univ_poly_deg3" [] e_pblID

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

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

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

   963 	       "(lhs e_e) is_poly_in v_v ",

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

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

   966   ],

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

   968   [["PolyEq","solve_d3_polyeq_equation"]]));

   970 (*--- d4 ---*)

   971 store_pbt

   972  (prep_pbt thy "pbl_equ_univ_poly_deg4" [] e_pblID

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

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

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

   976 	       "(lhs e_e) is_poly_in v_v ",

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

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

   979   ],

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

   981   [(*["PolyEq","solve_d4_polyeq_equation"]*)]));

   983 (*--- normalize ---*)

   984 store_pbt

   985  (prep_pbt thy "pbl_equ_univ_poly_norm" [] e_pblID

   986  (["normalize","polynomial","univariate","equation"],

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

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

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

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

   991   ],

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

   993   [["PolyEq","normalize_poly"]]));

   994 (*-------------------------expanded-----------------------*)

   995 store_pbt

   996  (prep_pbt thy "pbl_equ_univ_expand" [] e_pblID

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

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

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

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

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

  1002    ],

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

  1004   []));

  1006 (*--- d2 ---*)

  1007 store_pbt

  1008  (prep_pbt thy "pbl_equ_univ_expand_deg2" [] e_pblID

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

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

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

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

  1013   ],

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

  1015   [["PolyEq","complete_square"]]));

  1016 *}

  1017 setup {* KEStore_Elems.add_pbts

  1018   [(prep_pbt thy "pbl_equ_univ_poly" [] e_pblID

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

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

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

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

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

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

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

  1026     (*--- d0 ---*)

  1027     (prep_pbt thy "pbl_equ_univ_poly_deg0" [] e_pblID

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

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

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

  1031 	          "(lhs e_e) is_poly_in v_v",

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

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

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

  1035     (*--- d1 ---*)

  1036     (prep_pbt thy "pbl_equ_univ_poly_deg1" [] e_pblID

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

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

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

  1040 	          "(lhs e_e) is_poly_in v_v",

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

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

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

  1044     (*--- d2 ---*)

  1045     (prep_pbt thy "pbl_equ_univ_poly_deg2" [] e_pblID

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

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

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

  1049 	          "(lhs e_e) is_poly_in v_v ",

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

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

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

  1053     (prep_pbt thy "pbl_equ_univ_poly_deg2_sqonly" [] e_pblID

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

  1070         [["PolyEq","solve_d2_polyeq_sqonly_equation"]])),

  1071     (prep_pbt thy "pbl_equ_univ_poly_deg2_bdvonly" [] e_pblID

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

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

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

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

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

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

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

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

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

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

  1082         [["PolyEq","solve_d2_polyeq_bdvonly_equation"]])),

  1083     (prep_pbt thy "pbl_equ_univ_poly_deg2_pq" [] e_pblID

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

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

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

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

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

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

  1090     (prep_pbt thy "pbl_equ_univ_poly_deg2_abc" [] e_pblID

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

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

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

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

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

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

  1097     (*--- d3 ---*)

  1098     (prep_pbt thy "pbl_equ_univ_poly_deg3" [] e_pblID

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

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

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

  1102 	          "(lhs e_e) is_poly_in v_v ",

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

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

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

  1106     (*--- d4 ---*)

  1107     (prep_pbt thy "pbl_equ_univ_poly_deg4" [] e_pblID

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

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

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

  1111 	          "(lhs e_e) is_poly_in v_v ",

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

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

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

  1115     (*--- normalize ---*)

  1116     (prep_pbt thy "pbl_equ_univ_poly_norm" [] e_pblID

  1117       (["normalize","polynomial","univariate","equation"],

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

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

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

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

  1122         PolyEq_prls, SOME "solve (e_e::bool, v_v)", [["PolyEq","normalize_poly"]])),

  1123     (*-------------------------expanded-----------------------*)

  1124     (prep_pbt thy "pbl_equ_univ_expand" [] e_pblID

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

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

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

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

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

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

  1131     (*--- d2 ---*)

  1132     (prep_pbt thy "pbl_equ_univ_expand_deg2" [] e_pblID

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

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

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

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

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

  1139 ML{*

  1140 val scr =

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

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

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

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

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

  1146     "                                 make_ratpoly_in     False))) @@  " ^

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

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

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

  1150 parse thy scr;

  1151 *}

  1152 ML{*

  1153 "-------------------------methods-----------------------";

  1154 store_met

  1155  (prep_met thy "met_polyeq" [] e_metID

  1156  (["PolyEq"],

  1157    [],

  1158    {rew_ord'="tless_true",rls'=Atools_erls,calc = [], srls = e_rls, prls=e_rls,

  1159     crls=PolyEq_crls, errpats = [], nrls = norm_Rational}, "empty_script"));

  1161 store_met

  1162  (prep_met thy "met_polyeq_norm" [] e_metID

  1163  (["PolyEq","normalize_poly"],

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

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

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

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

  1168   ],

  1169    {rew_ord'="termlessI",

  1170     rls'=PolyEq_erls,

  1171     srls=e_rls,

  1172     prls=PolyEq_prls,

  1173     calc=[],

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

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

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

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

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

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

  1180     "                                 make_ratpoly_in     False))) @@  " ^

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

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

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

  1184    ));

  1186 *}

  1187 ML{*

  1188 store_met

  1189  (prep_met thy "met_polyeq_d0" [] e_metID

  1190  (["PolyEq","solve_d0_polyeq_equation"],

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

  1192    ("#Where" ,["(lhs e_e) is_poly_in v_v ",

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

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

  1195   ],

  1196    {rew_ord'="termlessI",

  1197     rls'=PolyEq_erls,

  1198     srls=e_rls,

  1199     prls=PolyEq_prls,

  1200     calc=[("sqrt", ("NthRoot.sqrt", eval_sqrt "#sqrt_"))],

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

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

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

  1204     "                  d0_polyeq_simplify  False))) e_e        " ^

  1205     " in ((Or_to_List e_e)::bool list))"

  1206  ));

  1207 *}

  1208 ML{*

  1209 store_met

  1210  (prep_met thy "met_polyeq_d1" [] e_metID

  1211  (["PolyEq","solve_d1_polyeq_equation"],

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

  1213    ("#Where" ,["(lhs e_e) is_poly_in v_v ",

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

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

  1216   ],

  1217    {rew_ord'="termlessI", rls'=PolyEq_erls, srls=e_rls, prls=PolyEq_prls,

  1218     calc=[("sqrt", ("NthRoot.sqrt", eval_sqrt "#sqrt_"))],

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

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

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

  1222     "                  d1_polyeq_simplify   True))          @@  " ^

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

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

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

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

  1227  ));

  1228 *}

  1229 ML{*

  1230 store_met

  1231  (prep_met thy "met_polyeq_d22" [] e_metID

  1232  (["PolyEq","solve_d2_polyeq_equation"],

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

  1234    ("#Where" ,["(lhs e_e) is_poly_in v_v ",

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

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

  1237   ],

  1238    {rew_ord'="termlessI",

  1239     rls'=PolyEq_erls,

  1240     srls=e_rls,

  1241     prls=PolyEq_prls,

  1242     calc=[("sqrt", ("NthRoot.sqrt", eval_sqrt "#sqrt_"))],

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

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

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

  1246     "                    d2_polyeq_simplify           True)) @@   " ^

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

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

  1249     "                    d1_polyeq_simplify            True)) @@  " ^

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

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

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

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

  1254  ));

  1255 *}

  1256 ML{*

  1257 store_met

  1258  (prep_met thy "met_polyeq_d2_bdvonly" [] e_metID

  1259  (["PolyEq","solve_d2_polyeq_bdvonly_equation"],

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

  1261    ("#Where" ,["(lhs e_e) is_poly_in v_v ",

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

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

  1264   ],

  1265    {rew_ord'="termlessI",

  1266     rls'=PolyEq_erls,

  1267     srls=e_rls,

  1268     prls=PolyEq_prls,

  1269     calc=[("sqrt", ("NthRoot.sqrt", eval_sqrt "#sqrt_"))],

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

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

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

  1273     "                   d2_polyeq_bdv_only_simplify    True)) @@  " ^

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

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

  1276     "                   d1_polyeq_simplify             True)) @@  " ^

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

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

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

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

  1281  ));

  1282 *}

  1283 ML{*

  1284 store_met

  1285  (prep_met thy "met_polyeq_d2_sqonly" [] e_metID

  1286  (["PolyEq","solve_d2_polyeq_sqonly_equation"],

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

  1288    ("#Where" ,["(lhs e_e) is_poly_in v_v ",

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

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

  1291   ],

  1292    {rew_ord'="termlessI",

  1293     rls'=PolyEq_erls,

  1294     srls=e_rls,

  1295     prls=PolyEq_prls,

  1296     calc=[("sqrt", ("NthRoot.sqrt", eval_sqrt "#sqrt_"))],

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

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

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

  1300     "                   d2_polyeq_sq_only_simplify     True)) @@   " ^

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

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

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

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

  1305  ));

  1306 *}

  1307 ML{*

  1308 store_met

  1309  (prep_met thy "met_polyeq_d2_pq" [] e_metID

  1310  (["PolyEq","solve_d2_polyeq_pq_equation"],

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

  1312    ("#Where" ,["(lhs e_e) is_poly_in v_v ",

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

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

  1315   ],

  1316    {rew_ord'="termlessI",

  1317     rls'=PolyEq_erls,

  1318     srls=e_rls,

  1319     prls=PolyEq_prls,

  1320     calc=[("sqrt", ("NthRoot.sqrt", eval_sqrt "#sqrt_"))],

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

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

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

  1324     "                   d2_polyeq_pqFormula_simplify   True)) @@  " ^

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

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

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

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

  1329  ));

  1330 *}

  1331 ML{*

  1332 store_met

  1333  (prep_met thy "met_polyeq_d2_abc" [] e_metID

  1334  (["PolyEq","solve_d2_polyeq_abc_equation"],

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

  1336    ("#Where" ,["(lhs e_e) is_poly_in v_v ",

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

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

  1339   ],

  1340    {rew_ord'="termlessI",

  1341     rls'=PolyEq_erls,

  1342     srls=e_rls,

  1343     prls=PolyEq_prls,

  1344     calc=[("sqrt", ("NthRoot.sqrt", eval_sqrt "#sqrt_"))],

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

  1346    "Script Solve_d2_polyeq_abc_equation  (e_e::bool) (v_v::real) =   " ^

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

  1348     "                   d2_polyeq_abcFormula_simplify   True)) @@  " ^

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

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

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

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

  1353  ));

  1354 *}

  1355 ML{*

  1356 store_met

  1357  (prep_met thy "met_polyeq_d3" [] e_metID

  1358  (["PolyEq","solve_d3_polyeq_equation"],

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

  1360    ("#Where" ,["(lhs e_e) is_poly_in v_v ",

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

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

  1363   ],

  1364    {rew_ord'="termlessI",

  1365     rls'=PolyEq_erls,

  1366     srls=e_rls,

  1367     prls=PolyEq_prls,

  1368     calc=[("sqrt", ("NthRoot.sqrt", eval_sqrt "#sqrt_"))],

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

  1370    "Script Solve_d3_polyeq_equation  (e_e::bool) (v_v::real) =     " ^

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

  1372     "                    d3_polyeq_simplify           True)) @@  " ^

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

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

  1375     "                    d2_polyeq_simplify           True)) @@  " ^

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

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

  1378     "                    d1_polyeq_simplify           True)) @@  " ^

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

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

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

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

  1383    ));

  1384 *}

  1385 ML{*

  1386  (*.solves all expanded (ie. normalized) terms of degree 2.*)

  1387  (*Oct.02 restriction: 'eval_true 0 =< discriminant' ony for integer values

  1388    by 'PolyEq_erls'; restricted until Float.thy is implemented*)

  1389 store_met

  1390  (prep_met thy "met_polyeq_complsq" [] e_metID

  1391  (["PolyEq","complete_square"],

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

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

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

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

  1396   ],

  1397    {rew_ord'="termlessI",rls'=PolyEq_erls,srls=e_rls,prls=PolyEq_prls,

  1398     calc=[("sqrt", ("NthRoot.sqrt", eval_sqrt "#sqrt_"))],

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

  1400    "Script Complete_square (e_e::bool) (v_v::real) =                         " ^

  1401    "(let e_e = " ^

  1402    "    ((Try (Rewrite_Set_Inst [(bdv,v_v)] cancel_leading_coeff True)) " ^

  1403    "        @@ (Try (Rewrite_Set_Inst [(bdv,v_v)] complete_square True))     " ^

  1404    "        @@ (Try (Rewrite square_explicit1 False))                       " ^

  1405    "        @@ (Try (Rewrite square_explicit2 False))                       " ^

  1406    "        @@ (Rewrite root_plus_minus True)                               " ^

  1407    "        @@ (Try (Repeat (Rewrite_Inst [(bdv,v_v)] bdv_explicit1 False))) " ^

  1408    "        @@ (Try (Repeat (Rewrite_Inst [(bdv,v_v)] bdv_explicit2 False))) " ^

  1409    "        @@ (Try (Repeat                                                 " ^

  1410    "                  (Rewrite_Inst [(bdv,v_v)] bdv_explicit3 False)))       " ^

  1411    "        @@ (Try (Rewrite_Set calculate_RootRat False))                  " ^

  1412    "        @@ (Try (Repeat (Calculate SQRT)))) e_e                         " ^

  1413    " in ((Or_to_List e_e)::bool list))"

  1414    ));

  1415 *}

  1416 ML{*

  1418 (* termorder hacked by MG *)

  1419 local (*. for make_polynomial_in .*)

  1421 open Term;  (* for type order = EQUAL | LESS | GREATER *)

  1423 fun pr_ord EQUAL = "EQUAL"

  1424   | pr_ord LESS  = "LESS"

  1425   | pr_ord GREATER = "GREATER";

  1427 fun dest_hd' x (Const (a, T)) = (((a, 0), T), 0)

  1428   | dest_hd' x (t as Free (a, T)) =

  1429     if x = t then ((("|||||||||||||", 0), T), 0)                        (*WN*)

  1430     else (((a, 0), T), 1)

  1431   | dest_hd' x (Var v) = (v, 2)

  1432   | dest_hd' x (Bound i) = ((("", i), dummyT), 3)

  1433   | dest_hd' x (Abs (_, T, _)) = ((("", 0), T), 4);

  1435 fun size_of_term' x (Const ("Atools.pow",_) $ Free (var,_) $ Free (pot,_)) =

  1436     (case x of                                                          (*WN*)

  1437 	    (Free (xstr,_)) =>

  1438 		(if xstr = var then 1000*(the (int_of_str pot)) else 3)

  1439 	  | _ => error ("size_of_term' called with subst = "^

  1440 			      (term2str x)))

  1441   | size_of_term' x (Free (subst,_)) =

  1442     (case x of

  1443 	    (Free (xstr,_)) => (if xstr = subst then 1000 else 1)

  1444 	  | _ => error ("size_of_term' called with subst = "^

  1445 			  (term2str x)))

  1446   | size_of_term' x (Abs (_,_,body)) = 1 + size_of_term' x body

  1447   | size_of_term' x (f$t) = size_of_term' x f  +  size_of_term' x t

  1448   | size_of_term' x _ = 1;

  1450 fun term_ord' x pr thy (Abs (_, T, t), Abs(_, U, u)) =       (* ~ term.ML *)

  1451     (case term_ord' x pr thy (t, u) of EQUAL => Term_Ord.typ_ord (T, U) | ord => ord)

  1452   | term_ord' x pr thy (t, u) =

  1453     (if pr

  1454      then

  1455        let

  1456          val (f, ts) = strip_comb t and (g, us) = strip_comb u;

  1457          val _ = tracing ("t= f@ts= \"" ^ term_to_string''' thy f ^ "\" @ \"[" ^

  1458            commas (map (term_to_string''' thy) ts) ^ "]\"");

  1459          val _ = tracing ("u= g@us= \"" ^ term_to_string''' thy g ^ "\" @ \"[" ^

  1460            commas(map (term_to_string''' thy) us) ^ "]\"");

  1461          val _ = tracing ("size_of_term(t,u)= (" ^ string_of_int (size_of_term' x t) ^ ", " ^

  1462            string_of_int (size_of_term' x u) ^ ")");

  1463          val _ = tracing ("hd_ord(f,g)      = " ^ (pr_ord o (hd_ord x)) (f,g));

  1464          val _ = tracing ("terms_ord(ts,us) = " ^ (pr_ord o (terms_ord x) str false) (ts, us));

  1465          val _ = tracing ("-------");

  1466        in () end

  1467      else ();

  1468 	  case int_ord (size_of_term' x t, size_of_term' x u) of

  1469 	    EQUAL =>

  1470 	      let val (f, ts) = strip_comb t and (g, us) = strip_comb u

  1471         in

  1472 	        (case hd_ord x (f, g) of

  1473 	           EQUAL => (terms_ord x str pr) (ts, us)

  1474 	         | ord => ord)

  1475 	      end

  1476 	 | ord => ord)

  1477 and hd_ord x (f, g) =                                        (* ~ term.ML *)

  1478   prod_ord (prod_ord Term_Ord.indexname_ord Term_Ord.typ_ord)

  1479             int_ord (dest_hd' x f, dest_hd' x g)

  1480 and terms_ord x str pr (ts, us) =

  1481     list_ord (term_ord' x pr (assoc_thy "Isac"))(ts, us);

  1483 in

  1485 fun ord_make_polynomial_in (pr:bool) thy subst tu =

  1486     let

  1487 	(* val _=tracing("*** subs variable is: "^(subst2str subst)); *)

  1488     in

  1489 	case subst of

  1490 	    (_,x)::_ => (term_ord' x pr thy tu = LESS)

  1491 	  | _ => error ("ord_make_polynomial_in called with subst = "^

  1492 			  (subst2str subst))

  1493     end;

  1494 end;(*local*)

  1496 *}

  1497 ML{*

  1498 val order_add_mult_in = prep_rls(

  1499   Rls{id = "order_add_mult_in", preconds = [],

  1500       rew_ord = ("ord_make_polynomial_in",

  1501 		 ord_make_polynomial_in false @{theory "Poly"}),

  1502       erls = e_rls,srls = Erls,

  1503       calc = [], errpatts = [],

  1504       rules = [Thm ("mult_commute",num_str @{thm mult_commute}),

  1505 	       (* z * w = w * z *)

  1506 	       Thm ("real_mult_left_commute",num_str @{thm real_mult_left_commute}),

  1507 	       (*z1.0 * (z2.0 * z3.0) = z2.0 * (z1.0 * z3.0)*)

  1508 	       Thm ("mult_assoc",num_str @{thm mult_assoc}),

  1509 	       (*z1.0 * z2.0 * z3.0 = z1.0 * (z2.0 * z3.0)*)

  1510 	       Thm ("add_commute",num_str @{thm add_commute}),

  1511 	       (*z + w = w + z*)

  1512 	       Thm ("add_left_commute",num_str @{thm add_left_commute}),

  1513 	       (*x + (y + z) = y + (x + z)*)

  1514 	       Thm ("add_assoc",num_str @{thm add_assoc})

  1515 	       (*z1.0 + z2.0 + z3.0 = z1.0 + (z2.0 + z3.0)*)

  1516 	       ], scr = EmptyScr}:rls);

  1518 *}

  1519 ML{*

  1520 val collect_bdv = prep_rls(

  1521   Rls{id = "collect_bdv", preconds = [],

  1522       rew_ord = ("dummy_ord", dummy_ord),

  1523       erls = e_rls,srls = Erls,

  1524       calc = [], errpatts = [],

  1525       rules = [Thm ("bdv_collect_1",num_str @{thm bdv_collect_1}),

  1526 	       Thm ("bdv_collect_2",num_str @{thm bdv_collect_2}),

  1527 	       Thm ("bdv_collect_3",num_str @{thm bdv_collect_3}),

  1529 	       Thm ("bdv_collect_assoc1_1",num_str @{thm bdv_collect_assoc1_1}),

  1530 	       Thm ("bdv_collect_assoc1_2",num_str @{thm bdv_collect_assoc1_2}),

  1531 	       Thm ("bdv_collect_assoc1_3",num_str @{thm bdv_collect_assoc1_3}),

  1533 	       Thm ("bdv_collect_assoc2_1",num_str @{thm bdv_collect_assoc2_1}),

  1534 	       Thm ("bdv_collect_assoc2_2",num_str @{thm bdv_collect_assoc2_2}),

  1535 	       Thm ("bdv_collect_assoc2_3",num_str @{thm bdv_collect_assoc2_3}),

  1538 	       Thm ("bdv_n_collect_1",num_str @{thm bdv_n_collect_1}),

  1539 	       Thm ("bdv_n_collect_2",num_str @{thm bdv_n_collect_2}),

  1540 	       Thm ("bdv_n_collect_3",num_str @{thm bdv_n_collect_3}),

  1542 	       Thm ("bdv_n_collect_assoc1_1",num_str @{thm bdv_n_collect_assoc1_1}),

  1543 	       Thm ("bdv_n_collect_assoc1_2",num_str @{thm bdv_n_collect_assoc1_2}),

  1544 	       Thm ("bdv_n_collect_assoc1_3",num_str @{thm bdv_n_collect_assoc1_3}),

  1546 	       Thm ("bdv_n_collect_assoc2_1",num_str @{thm bdv_n_collect_assoc2_1}),

  1547 	       Thm ("bdv_n_collect_assoc2_2",num_str @{thm bdv_n_collect_assoc2_2}),

  1548 	       Thm ("bdv_n_collect_assoc2_3",num_str @{thm bdv_n_collect_assoc2_3})

  1549 	       ], scr = EmptyScr}:rls);

  1551 *}

  1552 ML{*

  1553 (*.transforms an arbitrary term without roots to a polynomial [4]

  1554    according to knowledge/Poly.sml.*)

  1555 val make_polynomial_in = prep_rls(

  1556   Seq {id = "make_polynomial_in", preconds = []:term list,

  1557        rew_ord = ("dummy_ord", dummy_ord),

  1558       erls = Atools_erls, srls = Erls,

  1559       calc = [], errpatts = [],

  1560       rules = [Rls_ expand_poly,

  1561 	       Rls_ order_add_mult_in,

  1562 	       Rls_ simplify_power,

  1563 	       Rls_ collect_numerals,

  1564 	       Rls_ reduce_012,

  1565 	       Thm ("realpow_oneI",num_str @{thm realpow_oneI}),

  1566 	       Rls_ discard_parentheses,

  1567 	       Rls_ collect_bdv

  1568 	       ],

  1569       scr = EmptyScr

  1570       }:rls);

  1572 *}

  1573 ML{*

  1574 val separate_bdvs =

  1575     append_rls "separate_bdvs"

  1576 	       collect_bdv

  1577 	       [Thm ("separate_bdv", num_str @{thm separate_bdv}),

  1578 		(*"?a * ?bdv / ?b = ?a / ?b * ?bdv"*)

  1579 		Thm ("separate_bdv_n", num_str @{thm separate_bdv_n}),

  1580 		Thm ("separate_1_bdv", num_str @{thm separate_1_bdv}),

  1581 		(*"?bdv / ?b = (1 / ?b) * ?bdv"*)

  1582 		Thm ("separate_1_bdv_n", num_str @{thm separate_1_bdv_n}),

  1583 		(*"?bdv ^^^ ?n / ?b = 1 / ?b * ?bdv ^^^ ?n"*)

  1584 		Thm ("add_divide_distrib",

  1585 		     num_str @{thm add_divide_distrib})

  1586 		(*"(?x + ?y) / ?z = ?x / ?z + ?y / ?z"

  1587 		      WN051031 DOES NOT BELONG TO HERE*)

  1588 		];

  1589 *}

  1590 ML{*

  1591 val make_ratpoly_in = prep_rls(

  1592   Seq {id = "make_ratpoly_in", preconds = []:term list,

  1593        rew_ord = ("dummy_ord", dummy_ord),

  1594       erls = Atools_erls, srls = Erls,

  1595       calc = [], errpatts = [],

  1596       rules = [Rls_ norm_Rational,

  1597 	       Rls_ order_add_mult_in,

  1598 	       Rls_ discard_parentheses,

  1599 	       Rls_ separate_bdvs,

  1600 	       (* Rls_ rearrange_assoc, WN060916 why does cancel_p not work?*)

  1601 	       Rls_ cancel_p

  1602 	       (*Calc ("Fields.inverse_class.divide"  ,eval_cancel "#divide_e") too weak!*)

  1603 	       ],

  1604       scr = EmptyScr}:rls);

  1605 *}

  1606 setup {* KEStore_Elems.add_rlss

  1607   [("order_add_mult_in", (Context.theory_name @{theory}, order_add_mult_in)),

  1608   ("collect_bdv", (Context.theory_name @{theory}, collect_bdv)),

  1609   ("make_polynomial_in", (Context.theory_name @{theory}, make_polynomial_in)),

  1610   ("make_ratpoly_in", (Context.theory_name @{theory}, make_ratpoly_in)),

  1611   ("separate_bdvs", (Context.theory_name @{theory}, separate_bdvs))] *}

  1613 end

author	Mathias Lehnfeld <s1210629013@students.fh-hagenberg.at>
	Mon, 27 Jan 2014 21:49:27 +0100
changeset 55359	73dc85c025ab
parent 55339	cccd24e959ba
child 55363	d78bc1342183
permissions	-rw-r--r--