Mercurial Mercurial > wneuper > isa / file revision
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
src/Tools/isac/Knowledge/PolyEq.thy
author Walther Neuper <neuper@ist.tugraz.at>
Wed, 25 Aug 2010 16:20:07 +0200
branchisac-update-Isa09-2
changeset 37947 22235e4dbe5f
parent 37906 src/Tools/isac/IsacKnowledge/PolyEq.thy@e2b23ba9df13
child 37954 4022d670753c
permissions -rw-r--r--
renamed isac's directories and Build_Isac.thy

Scripts --> ProgLang
ME --> Interpret
IsacKnowledge --> Knowledge 
     1 (*.(c) by Richard Lang, 2003 .*)

     2 (* theory collecting all knowledge 

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

     4    for PolynomialEquations.

     5    alternative dependencies see Isac.thy

     6    created by: rlang 

     7          date: 02.07

     8    changed by: rlang

     9    last change by: rlang

    10              date: 03.06.03

    11 *)

    12 

    13 (* remove_thy"PolyEq";

    14    use_thy"Knowledge/Isac";

    15    use_thy"Knowledge/PolyEq";

    16    

    17    remove_thy"PolyEq";

    18    use_thy"Isac";

    19 

    20    use"ROOT.ML";

    21    cd"knowledge";

    22    *)

    23 

    24 PolyEq = LinEq + RootRatEq + 

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

    26 consts

    27 

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

    29   Complete'_square

    30              :: "[bool,real, \

    31 		  \ bool list] => bool list"

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

    33                  \ (_))" 9)

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

    35   Normalize'_poly

    36              :: "[bool,real, \

    37 		  \ bool list] => bool list"

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

    39                  \ (_))" 9)

    40   Solve'_d0'_polyeq'_equation

    41              :: "[bool,real, \

    42 		  \ bool list] => bool list"

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

    44                  \ (_))" 9)

    45   Solve'_d1'_polyeq'_equation

    46              :: "[bool,real, \

    47 		  \ bool list] => bool list"

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

    49                  \ (_))" 9)

    50   Solve'_d2'_polyeq'_equation

    51              :: "[bool,real, \

    52 		  \ bool list] => bool list"

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

    54                  \ (_))" 9)

    55   Solve'_d2'_polyeq'_sqonly'_equation

    56              :: "[bool,real, \

    57 		  \ bool list] => bool list"

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

    59                  \ (_))" 9)

    60   Solve'_d2'_polyeq'_bdvonly'_equation

    61              :: "[bool,real, \

    62 		  \ bool list] => bool list"

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

    64                  \ (_))" 9)

    65   Solve'_d2'_polyeq'_pq'_equation

    66              :: "[bool,real, \

    67 		  \ bool list] => bool list"

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

    69                  \ (_))" 9)

    70   Solve'_d2'_polyeq'_abc'_equation

    71              :: "[bool,real, \

    72 		  \ bool list] => bool list"

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

    74                  \ (_))" 9)

    75   Solve'_d3'_polyeq'_equation

    76              :: "[bool,real, \

    77 		  \ bool list] => bool list"

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

    79                  \ (_))" 9)

    80   Solve'_d4'_polyeq'_equation

    81              :: "[bool,real, \

    82 		  \ bool list] => bool list"

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

    84                  \ (_))" 9)

    85   Biquadrat'_poly

    86              :: "[bool,real, \

    87 		  \ bool list] => bool list"

    88                ("((Script Biquadrat'_poly (_ _=))// \

    89                  \ (_))" 9)

    90 

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

    92 rules 

    93 

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

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

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

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

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

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

   100 

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

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

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

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

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

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

   107 

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

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

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

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

   112 

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

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

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

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

   117 

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

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

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

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

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

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

   124 

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

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

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

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

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

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

   131 		        

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

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

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

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

   136 

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

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

   139 

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

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

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

   143 

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

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

   146 

   147 (*-- normalize --*)

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

   149   all_left

   150     "[|Not(b=!=0)|] ==> (a = b) = (a - b = 0)"

   151   makex1_x

   152     "a^^^1  = a"  

   153   real_assoc_1

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

   155   real_assoc_2

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

   157 

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

   159   d0_true

   160   "(0=0) = True"

   161   d0_false

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

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

   164   d1_isolate_add1

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

   166   d1_isolate_add2

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

   168   d1_isolate_div

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

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

   171   d2_isolate_add1

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

   173   d2_isolate_add2

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

   175   d2_isolate_div

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

   177   d2_prescind1

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

   179   d2_prescind2

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

   181   d2_prescind3

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

   183   d2_prescind4

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

   185   (* eliminate degree 2 *)

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

   187   d2_sqrt_equation1

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

   189   d2_sqrt_equation1_neg

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

   191   d2_sqrt_equation2

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

   193   d2_sqrt_equation3

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

   195   d2_reduce_equation1

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

   197   d2_reduce_equation2

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

   199   d2_pqformula1

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

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

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

   203   d2_pqformula1_neg

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

   205   d2_pqformula2

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

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

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

   209   d2_pqformula2_neg

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

   211   d2_pqformula3

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

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

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

   215   d2_pqformula3_neg

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

   217   d2_pqformula4

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

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

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

   221   d2_pqformula4_neg

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

   223   d2_pqformula5

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

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

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

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

   228   d2_pqformula6

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

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

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

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

   233   d2_pqformula7

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

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

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

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

   238   d2_pqformula8

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

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

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

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

   243   d2_pqformula9

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

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

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

   247   d2_pqformula9_neg

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

   249   d2_pqformula10

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

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

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

   253   d2_pqformula10_neg

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

   255   d2_abcformula1

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

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

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

   259   d2_abcformula1_neg

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

   261   d2_abcformula2

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

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

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

   265   d2_abcformula2_neg

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

   267   d2_abcformula3

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

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

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

   271   d2_abcformula3_neg

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

   273   d2_abcformula4

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

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

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

   277   d2_abcformula4_neg

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

   279   d2_abcformula5

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

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

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

   283   d2_abcformula5_neg

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

   285   d2_abcformula6

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

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

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

   289   d2_abcformula6_neg

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

   291   d2_abcformula7

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

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

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

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

   296   d2_abcformula8

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

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

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

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

   301   d2_abcformula9

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

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

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

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

   306   d2_abcformula10

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

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

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

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

   311 

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

   313   d3_reduce_equation1

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

   315   d3_reduce_equation2

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

   317   d3_reduce_equation3

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

   319   d3_reduce_equation4

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

   321   d3_reduce_equation5

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

   323   d3_reduce_equation6

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

   325   d3_reduce_equation7

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

   327   d3_reduce_equation8

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

   329   d3_reduce_equation9

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

   331   d3_reduce_equation10

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

   333   d3_reduce_equation11

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

   335   d3_reduce_equation12

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

   337   d3_reduce_equation13

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

   339   d3_reduce_equation14

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

   341   d3_reduce_equation15

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

   343   d3_reduce_equation16

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

   345   d3_isolate_add1

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

   347   d3_isolate_add2

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

   349   d3_isolate_div

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

   351   d3_root_equation2

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

   353   d3_root_equation1

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

   355 

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

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

   358  d4_sub_u1

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

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

   361 

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

   363 

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

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

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

   367 

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

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

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

   371 *)

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

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

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

   375 

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

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

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

   379 

   380 

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

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

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

   384 

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

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

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

   388 

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

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

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

   392 

   393 (*WN.14.3.03*)

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

   395 

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

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

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

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

   400 

   401 end

   402 

   403 

   404 

   405 

   406 

   407
wneuper/isa