1.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
1.2 +++ b/src/Tools/isac/Knowledge/PolyEq.thy Wed Aug 25 16:20:07 2010 +0200
1.3 @@ -0,0 +1,407 @@
1.4 +(*.(c) by Richard Lang, 2003 .*)
1.5 +(* theory collecting all knowledge
1.6 + (predicates 'is_rootEq_in', 'is_sqrt_in', 'is_ratEq_in')
1.7 + for PolynomialEquations.
1.8 + alternative dependencies see Isac.thy
1.9 + created by: rlang
1.10 + date: 02.07
1.11 + changed by: rlang
1.12 + last change by: rlang
1.13 + date: 03.06.03
1.14 +*)
1.15 +
1.16 +(* remove_thy"PolyEq";
1.17 + use_thy"Knowledge/Isac";
1.18 + use_thy"Knowledge/PolyEq";
1.19 +
1.20 + remove_thy"PolyEq";
1.21 + use_thy"Isac";
1.22 +
1.23 + use"ROOT.ML";
1.24 + cd"knowledge";
1.25 + *)
1.26 +
1.27 +PolyEq = LinEq + RootRatEq +
1.28 +(*-------------------- consts ------------------------------------------------*)
1.29 +consts
1.30 +
1.31 +(*---------scripts--------------------------*)
1.32 + Complete'_square
1.33 + :: "[bool,real, \
1.34 + \ bool list] => bool list"
1.35 + ("((Script Complete'_square (_ _ =))// \
1.36 + \ (_))" 9)
1.37 + (*----- poly ----- *)
1.38 + Normalize'_poly
1.39 + :: "[bool,real, \
1.40 + \ bool list] => bool list"
1.41 + ("((Script Normalize'_poly (_ _=))// \
1.42 + \ (_))" 9)
1.43 + Solve'_d0'_polyeq'_equation
1.44 + :: "[bool,real, \
1.45 + \ bool list] => bool list"
1.46 + ("((Script Solve'_d0'_polyeq'_equation (_ _ =))// \
1.47 + \ (_))" 9)
1.48 + Solve'_d1'_polyeq'_equation
1.49 + :: "[bool,real, \
1.50 + \ bool list] => bool list"
1.51 + ("((Script Solve'_d1'_polyeq'_equation (_ _ =))// \
1.52 + \ (_))" 9)
1.53 + Solve'_d2'_polyeq'_equation
1.54 + :: "[bool,real, \
1.55 + \ bool list] => bool list"
1.56 + ("((Script Solve'_d2'_polyeq'_equation (_ _ =))// \
1.57 + \ (_))" 9)
1.58 + Solve'_d2'_polyeq'_sqonly'_equation
1.59 + :: "[bool,real, \
1.60 + \ bool list] => bool list"
1.61 + ("((Script Solve'_d2'_polyeq'_sqonly'_equation (_ _ =))// \
1.62 + \ (_))" 9)
1.63 + Solve'_d2'_polyeq'_bdvonly'_equation
1.64 + :: "[bool,real, \
1.65 + \ bool list] => bool list"
1.66 + ("((Script Solve'_d2'_polyeq'_bdvonly'_equation (_ _ =))// \
1.67 + \ (_))" 9)
1.68 + Solve'_d2'_polyeq'_pq'_equation
1.69 + :: "[bool,real, \
1.70 + \ bool list] => bool list"
1.71 + ("((Script Solve'_d2'_polyeq'_pq'_equation (_ _ =))// \
1.72 + \ (_))" 9)
1.73 + Solve'_d2'_polyeq'_abc'_equation
1.74 + :: "[bool,real, \
1.75 + \ bool list] => bool list"
1.76 + ("((Script Solve'_d2'_polyeq'_abc'_equation (_ _ =))// \
1.77 + \ (_))" 9)
1.78 + Solve'_d3'_polyeq'_equation
1.79 + :: "[bool,real, \
1.80 + \ bool list] => bool list"
1.81 + ("((Script Solve'_d3'_polyeq'_equation (_ _ =))// \
1.82 + \ (_))" 9)
1.83 + Solve'_d4'_polyeq'_equation
1.84 + :: "[bool,real, \
1.85 + \ bool list] => bool list"
1.86 + ("((Script Solve'_d4'_polyeq'_equation (_ _ =))// \
1.87 + \ (_))" 9)
1.88 + Biquadrat'_poly
1.89 + :: "[bool,real, \
1.90 + \ bool list] => bool list"
1.91 + ("((Script Biquadrat'_poly (_ _=))// \
1.92 + \ (_))" 9)
1.93 +
1.94 +(*-------------------- rules -------------------------------------------------*)
1.95 +rules
1.96 +
1.97 + cancel_leading_coeff1 "Not (c =!= 0) ==> (a + b*bdv + c*bdv^^^2 = 0) = \
1.98 + \ (a/c + b/c*bdv + bdv^^^2 = 0)"
1.99 + cancel_leading_coeff2 "Not (c =!= 0) ==> (a - b*bdv + c*bdv^^^2 = 0) = \
1.100 + \ (a/c - b/c*bdv + bdv^^^2 = 0)"
1.101 + cancel_leading_coeff3 "Not (c =!= 0) ==> (a + b*bdv - c*bdv^^^2 = 0) = \
1.102 + \ (a/c + b/c*bdv - bdv^^^2 = 0)"
1.103 +
1.104 + cancel_leading_coeff4 "Not (c =!= 0) ==> (a + bdv + c*bdv^^^2 = 0) = \
1.105 + \ (a/c + 1/c*bdv + bdv^^^2 = 0)"
1.106 + cancel_leading_coeff5 "Not (c =!= 0) ==> (a - bdv + c*bdv^^^2 = 0) = \
1.107 + \ (a/c - 1/c*bdv + bdv^^^2 = 0)"
1.108 + cancel_leading_coeff6 "Not (c =!= 0) ==> (a + bdv - c*bdv^^^2 = 0) = \
1.109 + \ (a/c + 1/c*bdv - bdv^^^2 = 0)"
1.110 +
1.111 + cancel_leading_coeff7 "Not (c =!= 0) ==> ( b*bdv + c*bdv^^^2 = 0) = \
1.112 + \ ( b/c*bdv + bdv^^^2 = 0)"
1.113 + cancel_leading_coeff8 "Not (c =!= 0) ==> ( b*bdv - c*bdv^^^2 = 0) = \
1.114 + \ ( b/c*bdv - bdv^^^2 = 0)"
1.115 +
1.116 + cancel_leading_coeff9 "Not (c =!= 0) ==> ( bdv + c*bdv^^^2 = 0) = \
1.117 + \ ( 1/c*bdv + bdv^^^2 = 0)"
1.118 + cancel_leading_coeff10"Not (c =!= 0) ==> ( bdv - c*bdv^^^2 = 0) = \
1.119 + \ ( 1/c*bdv - bdv^^^2 = 0)"
1.120 +
1.121 + cancel_leading_coeff11"Not (c =!= 0) ==> (a + b*bdv^^^2 = 0) = \
1.122 + \ (a/b + bdv^^^2 = 0)"
1.123 + cancel_leading_coeff12"Not (c =!= 0) ==> (a - b*bdv^^^2 = 0) = \
1.124 + \ (a/b - bdv^^^2 = 0)"
1.125 + cancel_leading_coeff13"Not (c =!= 0) ==> ( b*bdv^^^2 = 0) = \
1.126 + \ ( bdv^^^2 = 0/b)"
1.127 +
1.128 + complete_square1 "(q + p*bdv + bdv^^^2 = 0) = \
1.129 + \(q + (p/2 + bdv)^^^2 = (p/2)^^^2)"
1.130 + complete_square2 "( p*bdv + bdv^^^2 = 0) = \
1.131 + \( (p/2 + bdv)^^^2 = (p/2)^^^2)"
1.132 + complete_square3 "( bdv + bdv^^^2 = 0) = \
1.133 + \( (1/2 + bdv)^^^2 = (1/2)^^^2)"
1.134 +
1.135 + complete_square4 "(q - p*bdv + bdv^^^2 = 0) = \
1.136 + \(q + (p/2 - bdv)^^^2 = (p/2)^^^2)"
1.137 + complete_square5 "(q + p*bdv - bdv^^^2 = 0) = \
1.138 + \(q + (p/2 - bdv)^^^2 = (p/2)^^^2)"
1.139 +
1.140 + square_explicit1 "(a + b^^^2 = c) = ( b^^^2 = c - a)"
1.141 + square_explicit2 "(a - b^^^2 = c) = (-(b^^^2) = c - a)"
1.142 +
1.143 + bdv_explicit1 "(a + bdv = b) = (bdv = - a + b)"
1.144 + bdv_explicit2 "(a - bdv = b) = ((-1)*bdv = - a + b)"
1.145 + bdv_explicit3 "((-1)*bdv = b) = (bdv = (-1)*b)"
1.146 +
1.147 + plus_leq "(0 <= a + b) = ((-1)*b <= a)"(*Isa?*)
1.148 + minus_leq "(0 <= a - b) = ( b <= a)"(*Isa?*)
1.149 +
1.150 +(*-- normalize --*)
1.151 + (*WN0509 compare LinEq.all_left "[|Not(b=!=0)|] ==> (a=b) = (a+(-1)*b=0)"*)
1.152 + all_left
1.153 + "[|Not(b=!=0)|] ==> (a = b) = (a - b = 0)"
1.154 + makex1_x
1.155 + "a^^^1 = a"
1.156 + real_assoc_1
1.157 + "a+(b+c) = a+b+c"
1.158 + real_assoc_2
1.159 + "a*(b*c) = a*b*c"
1.160 +
1.161 +(* ---- degree 0 ----*)
1.162 + d0_true
1.163 + "(0=0) = True"
1.164 + d0_false
1.165 + "[|Not(bdv occurs_in a);Not(a=0)|] ==> (a=0) = False"
1.166 +(* ---- degree 1 ----*)
1.167 + d1_isolate_add1
1.168 + "[|Not(bdv occurs_in a)|] ==> (a + b*bdv = 0) = (b*bdv = (-1)*a)"
1.169 + d1_isolate_add2
1.170 + "[|Not(bdv occurs_in a)|] ==> (a + bdv = 0) = ( bdv = (-1)*a)"
1.171 + d1_isolate_div
1.172 + "[|Not(b=0);Not(bdv occurs_in c)|] ==> (b*bdv = c) = (bdv = c/b)"
1.173 +(* ---- degree 2 ----*)
1.174 + d2_isolate_add1
1.175 + "[|Not(bdv occurs_in a)|] ==> (a + b*bdv^^^2=0) = (b*bdv^^^2= (-1)*a)"
1.176 + d2_isolate_add2
1.177 + "[|Not(bdv occurs_in a)|] ==> (a + bdv^^^2=0) = ( bdv^^^2= (-1)*a)"
1.178 + d2_isolate_div
1.179 + "[|Not(b=0);Not(bdv occurs_in c)|] ==> (b*bdv^^^2=c) = (bdv^^^2=c/b)"
1.180 + d2_prescind1
1.181 + "(a*bdv + b*bdv^^^2 = 0) = (bdv*(a +b*bdv)=0)"
1.182 + d2_prescind2
1.183 + "(a*bdv + bdv^^^2 = 0) = (bdv*(a + bdv)=0)"
1.184 + d2_prescind3
1.185 + "( bdv + b*bdv^^^2 = 0) = (bdv*(1+b*bdv)=0)"
1.186 + d2_prescind4
1.187 + "( bdv + bdv^^^2 = 0) = (bdv*(1+ bdv)=0)"
1.188 + (* eliminate degree 2 *)
1.189 + (* thm for neg arguments in sqroot have postfix _neg *)
1.190 + d2_sqrt_equation1
1.191 + "[|(0<=c);Not(bdv occurs_in c)|] ==> (bdv^^^2=c) = ((bdv=sqrt c) | (bdv=(-1)*sqrt c ))"
1.192 + d2_sqrt_equation1_neg
1.193 + "[|(c<0);Not(bdv occurs_in c)|] ==> (bdv^^^2=c) = False"
1.194 + d2_sqrt_equation2
1.195 + "(bdv^^^2=0) = (bdv=0)"
1.196 + d2_sqrt_equation3
1.197 + "(b*bdv^^^2=0) = (bdv=0)"
1.198 + d2_reduce_equation1
1.199 + "(bdv*(a +b*bdv)=0) = ((bdv=0)|(a+b*bdv=0))"
1.200 + d2_reduce_equation2
1.201 + "(bdv*(a + bdv)=0) = ((bdv=0)|(a+ bdv=0))"
1.202 + d2_pqformula1
1.203 + "[|0<=p^^^2 - 4*q|] ==> (q+p*bdv+ bdv^^^2=0) =
1.204 + ((bdv= (-1)*(p/2) + sqrt(p^^^2 - 4*q)/2)
1.205 + | (bdv= (-1)*(p/2) - sqrt(p^^^2 - 4*q)/2))"
1.206 + d2_pqformula1_neg
1.207 + "[|p^^^2 - 4*q<0|] ==> (q+p*bdv+ bdv^^^2=0) = False"
1.208 + d2_pqformula2
1.209 + "[|0<=p^^^2 - 4*q|] ==> (q+p*bdv+1*bdv^^^2=0) =
1.210 + ((bdv= (-1)*(p/2) + sqrt(p^^^2 - 4*q)/2)
1.211 + | (bdv= (-1)*(p/2) - sqrt(p^^^2 - 4*q)/2))"
1.212 + d2_pqformula2_neg
1.213 + "[|p^^^2 - 4*q<0|] ==> (q+p*bdv+1*bdv^^^2=0) = False"
1.214 + d2_pqformula3
1.215 + "[|0<=1 - 4*q|] ==> (q+ bdv+ bdv^^^2=0) =
1.216 + ((bdv= (-1)*(1/2) + sqrt(1 - 4*q)/2)
1.217 + | (bdv= (-1)*(1/2) - sqrt(1 - 4*q)/2))"
1.218 + d2_pqformula3_neg
1.219 + "[|1 - 4*q<0|] ==> (q+ bdv+ bdv^^^2=0) = False"
1.220 + d2_pqformula4
1.221 + "[|0<=1 - 4*q|] ==> (q+ bdv+1*bdv^^^2=0) =
1.222 + ((bdv= (-1)*(1/2) + sqrt(1 - 4*q)/2)
1.223 + | (bdv= (-1)*(1/2) - sqrt(1 - 4*q)/2))"
1.224 + d2_pqformula4_neg
1.225 + "[|1 - 4*q<0|] ==> (q+ bdv+1*bdv^^^2=0) = False"
1.226 + d2_pqformula5
1.227 + "[|0<=p^^^2 - 0|] ==> ( p*bdv+ bdv^^^2=0) =
1.228 + ((bdv= (-1)*(p/2) + sqrt(p^^^2 - 0)/2)
1.229 + | (bdv= (-1)*(p/2) - sqrt(p^^^2 - 0)/2))"
1.230 + (* d2_pqformula5_neg not need p^2 never less zero in R *)
1.231 + d2_pqformula6
1.232 + "[|0<=p^^^2 - 0|] ==> ( p*bdv+1*bdv^^^2=0) =
1.233 + ((bdv= (-1)*(p/2) + sqrt(p^^^2 - 0)/2)
1.234 + | (bdv= (-1)*(p/2) - sqrt(p^^^2 - 0)/2))"
1.235 + (* d2_pqformula6_neg not need p^2 never less zero in R *)
1.236 + d2_pqformula7
1.237 + "[|0<=1 - 0|] ==> ( bdv+ bdv^^^2=0) =
1.238 + ((bdv= (-1)*(1/2) + sqrt(1 - 0)/2)
1.239 + | (bdv= (-1)*(1/2) - sqrt(1 - 0)/2))"
1.240 + (* d2_pqformula7_neg not need, because 1<0 ==> False*)
1.241 + d2_pqformula8
1.242 + "[|0<=1 - 0|] ==> ( bdv+1*bdv^^^2=0) =
1.243 + ((bdv= (-1)*(1/2) + sqrt(1 - 0)/2)
1.244 + | (bdv= (-1)*(1/2) - sqrt(1 - 0)/2))"
1.245 + (* d2_pqformula8_neg not need, because 1<0 ==> False*)
1.246 + d2_pqformula9
1.247 + "[|Not(bdv occurs_in q); 0<= (-1)*4*q|] ==> (q+ 1*bdv^^^2=0) =
1.248 + ((bdv= 0 + sqrt(0 - 4*q)/2)
1.249 + | (bdv= 0 - sqrt(0 - 4*q)/2))"
1.250 + d2_pqformula9_neg
1.251 + "[|Not(bdv occurs_in q); (-1)*4*q<0|] ==> (q+ 1*bdv^^^2=0) = False"
1.252 + d2_pqformula10
1.253 + "[|Not(bdv occurs_in q); 0<= (-1)*4*q|] ==> (q+ bdv^^^2=0) =
1.254 + ((bdv= 0 + sqrt(0 - 4*q)/2)
1.255 + | (bdv= 0 - sqrt(0 - 4*q)/2))"
1.256 + d2_pqformula10_neg
1.257 + "[|Not(bdv occurs_in q); (-1)*4*q<0|] ==> (q+ bdv^^^2=0) = False"
1.258 + d2_abcformula1
1.259 + "[|0<=b^^^2 - 4*a*c|] ==> (c + b*bdv+a*bdv^^^2=0) =
1.260 + ((bdv=( -b + sqrt(b^^^2 - 4*a*c))/(2*a))
1.261 + | (bdv=( -b - sqrt(b^^^2 - 4*a*c))/(2*a)))"
1.262 + d2_abcformula1_neg
1.263 + "[|b^^^2 - 4*a*c<0|] ==> (c + b*bdv+a*bdv^^^2=0) = False"
1.264 + d2_abcformula2
1.265 + "[|0<=1 - 4*a*c|] ==> (c+ bdv+a*bdv^^^2=0) =
1.266 + ((bdv=( -1 + sqrt(1 - 4*a*c))/(2*a))
1.267 + | (bdv=( -1 - sqrt(1 - 4*a*c))/(2*a)))"
1.268 + d2_abcformula2_neg
1.269 + "[|1 - 4*a*c<0|] ==> (c+ bdv+a*bdv^^^2=0) = False"
1.270 + d2_abcformula3
1.271 + "[|0<=b^^^2 - 4*1*c|] ==> (c + b*bdv+ bdv^^^2=0) =
1.272 + ((bdv=( -b + sqrt(b^^^2 - 4*1*c))/(2*1))
1.273 + | (bdv=( -b - sqrt(b^^^2 - 4*1*c))/(2*1)))"
1.274 + d2_abcformula3_neg
1.275 + "[|b^^^2 - 4*1*c<0|] ==> (c + b*bdv+ bdv^^^2=0) = False"
1.276 + d2_abcformula4
1.277 + "[|0<=1 - 4*1*c|] ==> (c + bdv+ bdv^^^2=0) =
1.278 + ((bdv=( -1 + sqrt(1 - 4*1*c))/(2*1))
1.279 + | (bdv=( -1 - sqrt(1 - 4*1*c))/(2*1)))"
1.280 + d2_abcformula4_neg
1.281 + "[|1 - 4*1*c<0|] ==> (c + bdv+ bdv^^^2=0) = False"
1.282 + d2_abcformula5
1.283 + "[|Not(bdv occurs_in c); 0<=0 - 4*a*c|] ==> (c + a*bdv^^^2=0) =
1.284 + ((bdv=( 0 + sqrt(0 - 4*a*c))/(2*a))
1.285 + | (bdv=( 0 - sqrt(0 - 4*a*c))/(2*a)))"
1.286 + d2_abcformula5_neg
1.287 + "[|Not(bdv occurs_in c); 0 - 4*a*c<0|] ==> (c + a*bdv^^^2=0) = False"
1.288 + d2_abcformula6
1.289 + "[|Not(bdv occurs_in c); 0<=0 - 4*1*c|] ==> (c+ bdv^^^2=0) =
1.290 + ((bdv=( 0 + sqrt(0 - 4*1*c))/(2*1))
1.291 + | (bdv=( 0 - sqrt(0 - 4*1*c))/(2*1)))"
1.292 + d2_abcformula6_neg
1.293 + "[|Not(bdv occurs_in c); 0 - 4*1*c<0|] ==> (c+ bdv^^^2=0) = False"
1.294 + d2_abcformula7
1.295 + "[|0<=b^^^2 - 0|] ==> ( b*bdv+a*bdv^^^2=0) =
1.296 + ((bdv=( -b + sqrt(b^^^2 - 0))/(2*a))
1.297 + | (bdv=( -b - sqrt(b^^^2 - 0))/(2*a)))"
1.298 + (* d2_abcformula7_neg not need b^2 never less zero in R *)
1.299 + d2_abcformula8
1.300 + "[|0<=b^^^2 - 0|] ==> ( b*bdv+ bdv^^^2=0) =
1.301 + ((bdv=( -b + sqrt(b^^^2 - 0))/(2*1))
1.302 + | (bdv=( -b - sqrt(b^^^2 - 0))/(2*1)))"
1.303 + (* d2_abcformula8_neg not need b^2 never less zero in R *)
1.304 + d2_abcformula9
1.305 + "[|0<=1 - 0|] ==> ( bdv+a*bdv^^^2=0) =
1.306 + ((bdv=( -1 + sqrt(1 - 0))/(2*a))
1.307 + | (bdv=( -1 - sqrt(1 - 0))/(2*a)))"
1.308 + (* d2_abcformula9_neg not need, because 1<0 ==> False*)
1.309 + d2_abcformula10
1.310 + "[|0<=1 - 0|] ==> ( bdv+ bdv^^^2=0) =
1.311 + ((bdv=( -1 + sqrt(1 - 0))/(2*1))
1.312 + | (bdv=( -1 - sqrt(1 - 0))/(2*1)))"
1.313 + (* d2_abcformula10_neg not need, because 1<0 ==> False*)
1.314 +
1.315 +(* ---- degree 3 ----*)
1.316 + d3_reduce_equation1
1.317 + "(a*bdv + b*bdv^^^2 + c*bdv^^^3=0) = (bdv=0 | (a + b*bdv + c*bdv^^^2=0))"
1.318 + d3_reduce_equation2
1.319 + "( bdv + b*bdv^^^2 + c*bdv^^^3=0) = (bdv=0 | (1 + b*bdv + c*bdv^^^2=0))"
1.320 + d3_reduce_equation3
1.321 + "(a*bdv + bdv^^^2 + c*bdv^^^3=0) = (bdv=0 | (a + bdv + c*bdv^^^2=0))"
1.322 + d3_reduce_equation4
1.323 + "( bdv + bdv^^^2 + c*bdv^^^3=0) = (bdv=0 | (1 + bdv + c*bdv^^^2=0))"
1.324 + d3_reduce_equation5
1.325 + "(a*bdv + b*bdv^^^2 + bdv^^^3=0) = (bdv=0 | (a + b*bdv + bdv^^^2=0))"
1.326 + d3_reduce_equation6
1.327 + "( bdv + b*bdv^^^2 + bdv^^^3=0) = (bdv=0 | (1 + b*bdv + bdv^^^2=0))"
1.328 + d3_reduce_equation7
1.329 + "(a*bdv + bdv^^^2 + bdv^^^3=0) = (bdv=0 | (1 + bdv + bdv^^^2=0))"
1.330 + d3_reduce_equation8
1.331 + "( bdv + bdv^^^2 + bdv^^^3=0) = (bdv=0 | (1 + bdv + bdv^^^2=0))"
1.332 + d3_reduce_equation9
1.333 + "(a*bdv + c*bdv^^^3=0) = (bdv=0 | (a + c*bdv^^^2=0))"
1.334 + d3_reduce_equation10
1.335 + "( bdv + c*bdv^^^3=0) = (bdv=0 | (1 + c*bdv^^^2=0))"
1.336 + d3_reduce_equation11
1.337 + "(a*bdv + bdv^^^3=0) = (bdv=0 | (a + bdv^^^2=0))"
1.338 + d3_reduce_equation12
1.339 + "( bdv + bdv^^^3=0) = (bdv=0 | (1 + bdv^^^2=0))"
1.340 + d3_reduce_equation13
1.341 + "( b*bdv^^^2 + c*bdv^^^3=0) = (bdv=0 | ( b*bdv + c*bdv^^^2=0))"
1.342 + d3_reduce_equation14
1.343 + "( bdv^^^2 + c*bdv^^^3=0) = (bdv=0 | ( bdv + c*bdv^^^2=0))"
1.344 + d3_reduce_equation15
1.345 + "( b*bdv^^^2 + bdv^^^3=0) = (bdv=0 | ( b*bdv + bdv^^^2=0))"
1.346 + d3_reduce_equation16
1.347 + "( bdv^^^2 + bdv^^^3=0) = (bdv=0 | ( bdv + bdv^^^2=0))"
1.348 + d3_isolate_add1
1.349 + "[|Not(bdv occurs_in a)|] ==> (a + b*bdv^^^3=0) = (b*bdv^^^3= (-1)*a)"
1.350 + d3_isolate_add2
1.351 + "[|Not(bdv occurs_in a)|] ==> (a + bdv^^^3=0) = ( bdv^^^3= (-1)*a)"
1.352 + d3_isolate_div
1.353 + "[|Not(b=0);Not(bdv occurs_in a)|] ==> (b*bdv^^^3=c) = (bdv^^^3=c/b)"
1.354 + d3_root_equation2
1.355 + "(bdv^^^3=0) = (bdv=0)"
1.356 + d3_root_equation1
1.357 + "(bdv^^^3=c) = (bdv = nroot 3 c)"
1.358 +
1.359 +(* ---- degree 4 ----*)
1.360 + (* RL03.FIXME es wir nicht getestet ob u>0 *)
1.361 + d4_sub_u1
1.362 + "(c+b*bdv^^^2+a*bdv^^^4=0) =
1.363 + ((a*u^^^2+b*u+c=0) & (bdv^^^2=u))"
1.364 +
1.365 +(* ---- 7.3.02 von Termorder ---- *)
1.366 +
1.367 + bdv_collect_1 "l * bdv + m * bdv = (l + m) * bdv"
1.368 + bdv_collect_2 "bdv + m * bdv = (1 + m) * bdv"
1.369 + bdv_collect_3 "l * bdv + bdv = (l + 1) * bdv"
1.370 +
1.371 +(* bdv_collect_assoc0_1 "l * bdv + m * bdv + k = (l + m) * bdv + k"
1.372 + bdv_collect_assoc0_2 "bdv + m * bdv + k = (1 + m) * bdv + k"
1.373 + bdv_collect_assoc0_3 "l * bdv + bdv + k = (l + 1) * bdv + k"
1.374 +*)
1.375 + bdv_collect_assoc1_1 "l * bdv + (m * bdv + k) = (l + m) * bdv + k"
1.376 + bdv_collect_assoc1_2 "bdv + (m * bdv + k) = (1 + m) * bdv + k"
1.377 + bdv_collect_assoc1_3 "l * bdv + (bdv + k) = (l + 1) * bdv + k"
1.378 +
1.379 + bdv_collect_assoc2_1 "k + l * bdv + m * bdv = k + (l + m) * bdv"
1.380 + bdv_collect_assoc2_2 "k + bdv + m * bdv = k + (1 + m) * bdv"
1.381 + bdv_collect_assoc2_3 "k + l * bdv + bdv = k + (l + 1) * bdv"
1.382 +
1.383 +
1.384 + bdv_n_collect_1 "l * bdv^^^n + m * bdv^^^n = (l + m) * bdv^^^n"
1.385 + bdv_n_collect_2 " bdv^^^n + m * bdv^^^n = (1 + m) * bdv^^^n"
1.386 + bdv_n_collect_3 "l * bdv^^^n + bdv^^^n = (l + 1) * bdv^^^n" (*order!*)
1.387 +
1.388 + bdv_n_collect_assoc1_1 "l * bdv^^^n + (m * bdv^^^n + k) = (l + m) * bdv^^^n + k"
1.389 + bdv_n_collect_assoc1_2 "bdv^^^n + (m * bdv^^^n + k) = (1 + m) * bdv^^^n + k"
1.390 + bdv_n_collect_assoc1_3 "l * bdv^^^n + (bdv^^^n + k) = (l + 1) * bdv^^^n + k"
1.391 +
1.392 + bdv_n_collect_assoc2_1 "k + l * bdv^^^n + m * bdv^^^n = k + (l + m) * bdv^^^n"
1.393 + bdv_n_collect_assoc2_2 "k + bdv^^^n + m * bdv^^^n = k + (1 + m) * bdv^^^n"
1.394 + bdv_n_collect_assoc2_3 "k + l * bdv^^^n + bdv^^^n = k + (l + 1) * bdv^^^n"
1.395 +
1.396 +(*WN.14.3.03*)
1.397 + real_minus_div "- (a / b) = (-1 * a) / b"
1.398 +
1.399 + separate_bdv "(a * bdv) / b = (a / b) * bdv"
1.400 + separate_bdv_n "(a * bdv ^^^ n) / b = (a / b) * bdv ^^^ n"
1.401 + separate_1_bdv "bdv / b = (1 / b) * bdv"
1.402 + separate_1_bdv_n "bdv ^^^ n / b = (1 / b) * bdv ^^^ n"
1.403 +
1.404 +end
1.405 +
1.406 +
1.407 +
1.408 +
1.409 +
1.410 +