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