diff -r a28b5fc129b7 -r 22235e4dbe5f src/Tools/isac/Knowledge/PolyEq.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Tools/isac/Knowledge/PolyEq.thy Wed Aug 25 16:20:07 2010 +0200 @@ -0,0 +1,407 @@ +(*.(c) by Richard Lang, 2003 .*) +(* theory collecting all knowledge + (predicates 'is_rootEq_in', 'is_sqrt_in', 'is_ratEq_in') + for PolynomialEquations. + alternative dependencies see Isac.thy + created by: rlang + date: 02.07 + changed by: rlang + last change by: rlang + date: 03.06.03 +*) + +(* remove_thy"PolyEq"; + use_thy"Knowledge/Isac"; + use_thy"Knowledge/PolyEq"; + + remove_thy"PolyEq"; + use_thy"Isac"; + + use"ROOT.ML"; + cd"knowledge"; + *) + +PolyEq = LinEq + RootRatEq + +(*-------------------- consts ------------------------------------------------*) +consts + +(*---------scripts--------------------------*) + Complete'_square + :: "[bool,real, \ + \ bool list] => bool list" + ("((Script Complete'_square (_ _ =))// \ + \ (_))" 9) + (*----- poly ----- *) + Normalize'_poly + :: "[bool,real, \ + \ bool list] => bool list" + ("((Script Normalize'_poly (_ _=))// \ + \ (_))" 9) + Solve'_d0'_polyeq'_equation + :: "[bool,real, \ + \ bool list] => bool list" + ("((Script Solve'_d0'_polyeq'_equation (_ _ =))// \ + \ (_))" 9) + Solve'_d1'_polyeq'_equation + :: "[bool,real, \ + \ bool list] => bool list" + ("((Script Solve'_d1'_polyeq'_equation (_ _ =))// \ + \ (_))" 9) + Solve'_d2'_polyeq'_equation + :: "[bool,real, \ + \ bool list] => bool list" + ("((Script Solve'_d2'_polyeq'_equation (_ _ =))// \ + \ (_))" 9) + Solve'_d2'_polyeq'_sqonly'_equation + :: "[bool,real, \ + \ bool list] => bool list" + ("((Script Solve'_d2'_polyeq'_sqonly'_equation (_ _ =))// \ + \ (_))" 9) + Solve'_d2'_polyeq'_bdvonly'_equation + :: "[bool,real, \ + \ bool list] => bool list" + ("((Script Solve'_d2'_polyeq'_bdvonly'_equation (_ _ =))// \ + \ (_))" 9) + Solve'_d2'_polyeq'_pq'_equation + :: "[bool,real, \ + \ bool list] => bool list" + ("((Script Solve'_d2'_polyeq'_pq'_equation (_ _ =))// \ + \ (_))" 9) + Solve'_d2'_polyeq'_abc'_equation + :: "[bool,real, \ + \ bool list] => bool list" + ("((Script Solve'_d2'_polyeq'_abc'_equation (_ _ =))// \ + \ (_))" 9) + Solve'_d3'_polyeq'_equation + :: "[bool,real, \ + \ bool list] => bool list" + ("((Script Solve'_d3'_polyeq'_equation (_ _ =))// \ + \ (_))" 9) + Solve'_d4'_polyeq'_equation + :: "[bool,real, \ + \ bool list] => bool list" + ("((Script Solve'_d4'_polyeq'_equation (_ _ =))// \ + \ (_))" 9) + Biquadrat'_poly + :: "[bool,real, \ + \ bool list] => bool list" + ("((Script Biquadrat'_poly (_ _=))// \ + \ (_))" 9) + +(*-------------------- rules -------------------------------------------------*) +rules + + cancel_leading_coeff1 "Not (c =!= 0) ==> (a + b*bdv + c*bdv^^^2 = 0) = \ + \ (a/c + b/c*bdv + bdv^^^2 = 0)" + cancel_leading_coeff2 "Not (c =!= 0) ==> (a - b*bdv + c*bdv^^^2 = 0) = \ + \ (a/c - b/c*bdv + bdv^^^2 = 0)" + cancel_leading_coeff3 "Not (c =!= 0) ==> (a + b*bdv - c*bdv^^^2 = 0) = \ + \ (a/c + b/c*bdv - bdv^^^2 = 0)" + + cancel_leading_coeff4 "Not (c =!= 0) ==> (a + bdv + c*bdv^^^2 = 0) = \ + \ (a/c + 1/c*bdv + bdv^^^2 = 0)" + cancel_leading_coeff5 "Not (c =!= 0) ==> (a - bdv + c*bdv^^^2 = 0) = \ + \ (a/c - 1/c*bdv + bdv^^^2 = 0)" + cancel_leading_coeff6 "Not (c =!= 0) ==> (a + bdv - c*bdv^^^2 = 0) = \ + \ (a/c + 1/c*bdv - bdv^^^2 = 0)" + + cancel_leading_coeff7 "Not (c =!= 0) ==> ( b*bdv + c*bdv^^^2 = 0) = \ + \ ( b/c*bdv + bdv^^^2 = 0)" + cancel_leading_coeff8 "Not (c =!= 0) ==> ( b*bdv - c*bdv^^^2 = 0) = \ + \ ( b/c*bdv - bdv^^^2 = 0)" + + cancel_leading_coeff9 "Not (c =!= 0) ==> ( bdv + c*bdv^^^2 = 0) = \ + \ ( 1/c*bdv + bdv^^^2 = 0)" + cancel_leading_coeff10"Not (c =!= 0) ==> ( bdv - c*bdv^^^2 = 0) = \ + \ ( 1/c*bdv - bdv^^^2 = 0)" + + cancel_leading_coeff11"Not (c =!= 0) ==> (a + b*bdv^^^2 = 0) = \ + \ (a/b + bdv^^^2 = 0)" + cancel_leading_coeff12"Not (c =!= 0) ==> (a - b*bdv^^^2 = 0) = \ + \ (a/b - bdv^^^2 = 0)" + cancel_leading_coeff13"Not (c =!= 0) ==> ( b*bdv^^^2 = 0) = \ + \ ( bdv^^^2 = 0/b)" + + complete_square1 "(q + p*bdv + bdv^^^2 = 0) = \ + \(q + (p/2 + bdv)^^^2 = (p/2)^^^2)" + complete_square2 "( p*bdv + bdv^^^2 = 0) = \ + \( (p/2 + bdv)^^^2 = (p/2)^^^2)" + complete_square3 "( bdv + bdv^^^2 = 0) = \ + \( (1/2 + bdv)^^^2 = (1/2)^^^2)" + + complete_square4 "(q - p*bdv + bdv^^^2 = 0) = \ + \(q + (p/2 - bdv)^^^2 = (p/2)^^^2)" + complete_square5 "(q + p*bdv - bdv^^^2 = 0) = \ + \(q + (p/2 - bdv)^^^2 = (p/2)^^^2)" + + square_explicit1 "(a + b^^^2 = c) = ( b^^^2 = c - a)" + square_explicit2 "(a - b^^^2 = c) = (-(b^^^2) = c - a)" + + bdv_explicit1 "(a + bdv = b) = (bdv = - a + b)" + bdv_explicit2 "(a - bdv = b) = ((-1)*bdv = - a + b)" + bdv_explicit3 "((-1)*bdv = b) = (bdv = (-1)*b)" + + plus_leq "(0 <= a + b) = ((-1)*b <= a)"(*Isa?*) + minus_leq "(0 <= a - b) = ( b <= a)"(*Isa?*) + +(*-- normalize --*) + (*WN0509 compare LinEq.all_left "[|Not(b=!=0)|] ==> (a=b) = (a+(-1)*b=0)"*) + all_left + "[|Not(b=!=0)|] ==> (a = b) = (a - b = 0)" + makex1_x + "a^^^1 = a" + real_assoc_1 + "a+(b+c) = a+b+c" + real_assoc_2 + "a*(b*c) = a*b*c" + +(* ---- degree 0 ----*) + d0_true + "(0=0) = True" + d0_false + "[|Not(bdv occurs_in a);Not(a=0)|] ==> (a=0) = False" +(* ---- degree 1 ----*) + d1_isolate_add1 + "[|Not(bdv occurs_in a)|] ==> (a + b*bdv = 0) = (b*bdv = (-1)*a)" + d1_isolate_add2 + "[|Not(bdv occurs_in a)|] ==> (a + bdv = 0) = ( bdv = (-1)*a)" + d1_isolate_div + "[|Not(b=0);Not(bdv occurs_in c)|] ==> (b*bdv = c) = (bdv = c/b)" +(* ---- degree 2 ----*) + d2_isolate_add1 + "[|Not(bdv occurs_in a)|] ==> (a + b*bdv^^^2=0) = (b*bdv^^^2= (-1)*a)" + d2_isolate_add2 + "[|Not(bdv occurs_in a)|] ==> (a + bdv^^^2=0) = ( bdv^^^2= (-1)*a)" + d2_isolate_div + "[|Not(b=0);Not(bdv occurs_in c)|] ==> (b*bdv^^^2=c) = (bdv^^^2=c/b)" + d2_prescind1 + "(a*bdv + b*bdv^^^2 = 0) = (bdv*(a +b*bdv)=0)" + d2_prescind2 + "(a*bdv + bdv^^^2 = 0) = (bdv*(a + bdv)=0)" + d2_prescind3 + "( bdv + b*bdv^^^2 = 0) = (bdv*(1+b*bdv)=0)" + d2_prescind4 + "( bdv + bdv^^^2 = 0) = (bdv*(1+ bdv)=0)" + (* eliminate degree 2 *) + (* thm for neg arguments in sqroot have postfix _neg *) + d2_sqrt_equation1 + "[|(0<=c);Not(bdv occurs_in c)|] ==> (bdv^^^2=c) = ((bdv=sqrt c) | (bdv=(-1)*sqrt c ))" + d2_sqrt_equation1_neg + "[|(c<0);Not(bdv occurs_in c)|] ==> (bdv^^^2=c) = False" + d2_sqrt_equation2 + "(bdv^^^2=0) = (bdv=0)" + d2_sqrt_equation3 + "(b*bdv^^^2=0) = (bdv=0)" + d2_reduce_equation1 + "(bdv*(a +b*bdv)=0) = ((bdv=0)|(a+b*bdv=0))" + d2_reduce_equation2 + "(bdv*(a + bdv)=0) = ((bdv=0)|(a+ bdv=0))" + d2_pqformula1 + "[|0<=p^^^2 - 4*q|] ==> (q+p*bdv+ bdv^^^2=0) = + ((bdv= (-1)*(p/2) + sqrt(p^^^2 - 4*q)/2) + | (bdv= (-1)*(p/2) - sqrt(p^^^2 - 4*q)/2))" + d2_pqformula1_neg + "[|p^^^2 - 4*q<0|] ==> (q+p*bdv+ bdv^^^2=0) = False" + d2_pqformula2 + "[|0<=p^^^2 - 4*q|] ==> (q+p*bdv+1*bdv^^^2=0) = + ((bdv= (-1)*(p/2) + sqrt(p^^^2 - 4*q)/2) + | (bdv= (-1)*(p/2) - sqrt(p^^^2 - 4*q)/2))" + d2_pqformula2_neg + "[|p^^^2 - 4*q<0|] ==> (q+p*bdv+1*bdv^^^2=0) = False" + d2_pqformula3 + "[|0<=1 - 4*q|] ==> (q+ bdv+ bdv^^^2=0) = + ((bdv= (-1)*(1/2) + sqrt(1 - 4*q)/2) + | (bdv= (-1)*(1/2) - sqrt(1 - 4*q)/2))" + d2_pqformula3_neg + "[|1 - 4*q<0|] ==> (q+ bdv+ bdv^^^2=0) = False" + d2_pqformula4 + "[|0<=1 - 4*q|] ==> (q+ bdv+1*bdv^^^2=0) = + ((bdv= (-1)*(1/2) + sqrt(1 - 4*q)/2) + | (bdv= (-1)*(1/2) - sqrt(1 - 4*q)/2))" + d2_pqformula4_neg + "[|1 - 4*q<0|] ==> (q+ bdv+1*bdv^^^2=0) = False" + d2_pqformula5 + "[|0<=p^^^2 - 0|] ==> ( p*bdv+ bdv^^^2=0) = + ((bdv= (-1)*(p/2) + sqrt(p^^^2 - 0)/2) + | (bdv= (-1)*(p/2) - sqrt(p^^^2 - 0)/2))" + (* d2_pqformula5_neg not need p^2 never less zero in R *) + d2_pqformula6 + "[|0<=p^^^2 - 0|] ==> ( p*bdv+1*bdv^^^2=0) = + ((bdv= (-1)*(p/2) + sqrt(p^^^2 - 0)/2) + | (bdv= (-1)*(p/2) - sqrt(p^^^2 - 0)/2))" + (* d2_pqformula6_neg not need p^2 never less zero in R *) + d2_pqformula7 + "[|0<=1 - 0|] ==> ( bdv+ bdv^^^2=0) = + ((bdv= (-1)*(1/2) + sqrt(1 - 0)/2) + | (bdv= (-1)*(1/2) - sqrt(1 - 0)/2))" + (* d2_pqformula7_neg not need, because 1<0 ==> False*) + d2_pqformula8 + "[|0<=1 - 0|] ==> ( bdv+1*bdv^^^2=0) = + ((bdv= (-1)*(1/2) + sqrt(1 - 0)/2) + | (bdv= (-1)*(1/2) - sqrt(1 - 0)/2))" + (* d2_pqformula8_neg not need, because 1<0 ==> False*) + d2_pqformula9 + "[|Not(bdv occurs_in q); 0<= (-1)*4*q|] ==> (q+ 1*bdv^^^2=0) = + ((bdv= 0 + sqrt(0 - 4*q)/2) + | (bdv= 0 - sqrt(0 - 4*q)/2))" + d2_pqformula9_neg + "[|Not(bdv occurs_in q); (-1)*4*q<0|] ==> (q+ 1*bdv^^^2=0) = False" + d2_pqformula10 + "[|Not(bdv occurs_in q); 0<= (-1)*4*q|] ==> (q+ bdv^^^2=0) = + ((bdv= 0 + sqrt(0 - 4*q)/2) + | (bdv= 0 - sqrt(0 - 4*q)/2))" + d2_pqformula10_neg + "[|Not(bdv occurs_in q); (-1)*4*q<0|] ==> (q+ bdv^^^2=0) = False" + d2_abcformula1 + "[|0<=b^^^2 - 4*a*c|] ==> (c + b*bdv+a*bdv^^^2=0) = + ((bdv=( -b + sqrt(b^^^2 - 4*a*c))/(2*a)) + | (bdv=( -b - sqrt(b^^^2 - 4*a*c))/(2*a)))" + d2_abcformula1_neg + "[|b^^^2 - 4*a*c<0|] ==> (c + b*bdv+a*bdv^^^2=0) = False" + d2_abcformula2 + "[|0<=1 - 4*a*c|] ==> (c+ bdv+a*bdv^^^2=0) = + ((bdv=( -1 + sqrt(1 - 4*a*c))/(2*a)) + | (bdv=( -1 - sqrt(1 - 4*a*c))/(2*a)))" + d2_abcformula2_neg + "[|1 - 4*a*c<0|] ==> (c+ bdv+a*bdv^^^2=0) = False" + d2_abcformula3 + "[|0<=b^^^2 - 4*1*c|] ==> (c + b*bdv+ bdv^^^2=0) = + ((bdv=( -b + sqrt(b^^^2 - 4*1*c))/(2*1)) + | (bdv=( -b - sqrt(b^^^2 - 4*1*c))/(2*1)))" + d2_abcformula3_neg + "[|b^^^2 - 4*1*c<0|] ==> (c + b*bdv+ bdv^^^2=0) = False" + d2_abcformula4 + "[|0<=1 - 4*1*c|] ==> (c + bdv+ bdv^^^2=0) = + ((bdv=( -1 + sqrt(1 - 4*1*c))/(2*1)) + | (bdv=( -1 - sqrt(1 - 4*1*c))/(2*1)))" + d2_abcformula4_neg + "[|1 - 4*1*c<0|] ==> (c + bdv+ bdv^^^2=0) = False" + d2_abcformula5 + "[|Not(bdv occurs_in c); 0<=0 - 4*a*c|] ==> (c + a*bdv^^^2=0) = + ((bdv=( 0 + sqrt(0 - 4*a*c))/(2*a)) + | (bdv=( 0 - sqrt(0 - 4*a*c))/(2*a)))" + d2_abcformula5_neg + "[|Not(bdv occurs_in c); 0 - 4*a*c<0|] ==> (c + a*bdv^^^2=0) = False" + d2_abcformula6 + "[|Not(bdv occurs_in c); 0<=0 - 4*1*c|] ==> (c+ bdv^^^2=0) = + ((bdv=( 0 + sqrt(0 - 4*1*c))/(2*1)) + | (bdv=( 0 - sqrt(0 - 4*1*c))/(2*1)))" + d2_abcformula6_neg + "[|Not(bdv occurs_in c); 0 - 4*1*c<0|] ==> (c+ bdv^^^2=0) = False" + d2_abcformula7 + "[|0<=b^^^2 - 0|] ==> ( b*bdv+a*bdv^^^2=0) = + ((bdv=( -b + sqrt(b^^^2 - 0))/(2*a)) + | (bdv=( -b - sqrt(b^^^2 - 0))/(2*a)))" + (* d2_abcformula7_neg not need b^2 never less zero in R *) + d2_abcformula8 + "[|0<=b^^^2 - 0|] ==> ( b*bdv+ bdv^^^2=0) = + ((bdv=( -b + sqrt(b^^^2 - 0))/(2*1)) + | (bdv=( -b - sqrt(b^^^2 - 0))/(2*1)))" + (* d2_abcformula8_neg not need b^2 never less zero in R *) + d2_abcformula9 + "[|0<=1 - 0|] ==> ( bdv+a*bdv^^^2=0) = + ((bdv=( -1 + sqrt(1 - 0))/(2*a)) + | (bdv=( -1 - sqrt(1 - 0))/(2*a)))" + (* d2_abcformula9_neg not need, because 1<0 ==> False*) + d2_abcformula10 + "[|0<=1 - 0|] ==> ( bdv+ bdv^^^2=0) = + ((bdv=( -1 + sqrt(1 - 0))/(2*1)) + | (bdv=( -1 - sqrt(1 - 0))/(2*1)))" + (* d2_abcformula10_neg not need, because 1<0 ==> False*) + +(* ---- degree 3 ----*) + d3_reduce_equation1 + "(a*bdv + b*bdv^^^2 + c*bdv^^^3=0) = (bdv=0 | (a + b*bdv + c*bdv^^^2=0))" + d3_reduce_equation2 + "( bdv + b*bdv^^^2 + c*bdv^^^3=0) = (bdv=0 | (1 + b*bdv + c*bdv^^^2=0))" + d3_reduce_equation3 + "(a*bdv + bdv^^^2 + c*bdv^^^3=0) = (bdv=0 | (a + bdv + c*bdv^^^2=0))" + d3_reduce_equation4 + "( bdv + bdv^^^2 + c*bdv^^^3=0) = (bdv=0 | (1 + bdv + c*bdv^^^2=0))" + d3_reduce_equation5 + "(a*bdv + b*bdv^^^2 + bdv^^^3=0) = (bdv=0 | (a + b*bdv + bdv^^^2=0))" + d3_reduce_equation6 + "( bdv + b*bdv^^^2 + bdv^^^3=0) = (bdv=0 | (1 + b*bdv + bdv^^^2=0))" + d3_reduce_equation7 + "(a*bdv + bdv^^^2 + bdv^^^3=0) = (bdv=0 | (1 + bdv + bdv^^^2=0))" + d3_reduce_equation8 + "( bdv + bdv^^^2 + bdv^^^3=0) = (bdv=0 | (1 + bdv + bdv^^^2=0))" + d3_reduce_equation9 + "(a*bdv + c*bdv^^^3=0) = (bdv=0 | (a + c*bdv^^^2=0))" + d3_reduce_equation10 + "( bdv + c*bdv^^^3=0) = (bdv=0 | (1 + c*bdv^^^2=0))" + d3_reduce_equation11 + "(a*bdv + bdv^^^3=0) = (bdv=0 | (a + bdv^^^2=0))" + d3_reduce_equation12 + "( bdv + bdv^^^3=0) = (bdv=0 | (1 + bdv^^^2=0))" + d3_reduce_equation13 + "( b*bdv^^^2 + c*bdv^^^3=0) = (bdv=0 | ( b*bdv + c*bdv^^^2=0))" + d3_reduce_equation14 + "( bdv^^^2 + c*bdv^^^3=0) = (bdv=0 | ( bdv + c*bdv^^^2=0))" + d3_reduce_equation15 + "( b*bdv^^^2 + bdv^^^3=0) = (bdv=0 | ( b*bdv + bdv^^^2=0))" + d3_reduce_equation16 + "( bdv^^^2 + bdv^^^3=0) = (bdv=0 | ( bdv + bdv^^^2=0))" + d3_isolate_add1 + "[|Not(bdv occurs_in a)|] ==> (a + b*bdv^^^3=0) = (b*bdv^^^3= (-1)*a)" + d3_isolate_add2 + "[|Not(bdv occurs_in a)|] ==> (a + bdv^^^3=0) = ( bdv^^^3= (-1)*a)" + d3_isolate_div + "[|Not(b=0);Not(bdv occurs_in a)|] ==> (b*bdv^^^3=c) = (bdv^^^3=c/b)" + d3_root_equation2 + "(bdv^^^3=0) = (bdv=0)" + d3_root_equation1 + "(bdv^^^3=c) = (bdv = nroot 3 c)" + +(* ---- degree 4 ----*) + (* RL03.FIXME es wir nicht getestet ob u>0 *) + d4_sub_u1 + "(c+b*bdv^^^2+a*bdv^^^4=0) = + ((a*u^^^2+b*u+c=0) & (bdv^^^2=u))" + +(* ---- 7.3.02 von Termorder ---- *) + + bdv_collect_1 "l * bdv + m * bdv = (l + m) * bdv" + bdv_collect_2 "bdv + m * bdv = (1 + m) * bdv" + bdv_collect_3 "l * bdv + bdv = (l + 1) * bdv" + +(* bdv_collect_assoc0_1 "l * bdv + m * bdv + k = (l + m) * bdv + k" + bdv_collect_assoc0_2 "bdv + m * bdv + k = (1 + m) * bdv + k" + bdv_collect_assoc0_3 "l * bdv + bdv + k = (l + 1) * bdv + k" +*) + bdv_collect_assoc1_1 "l * bdv + (m * bdv + k) = (l + m) * bdv + k" + bdv_collect_assoc1_2 "bdv + (m * bdv + k) = (1 + m) * bdv + k" + bdv_collect_assoc1_3 "l * bdv + (bdv + k) = (l + 1) * bdv + k" + + bdv_collect_assoc2_1 "k + l * bdv + m * bdv = k + (l + m) * bdv" + bdv_collect_assoc2_2 "k + bdv + m * bdv = k + (1 + m) * bdv" + bdv_collect_assoc2_3 "k + l * bdv + bdv = k + (l + 1) * bdv" + + + bdv_n_collect_1 "l * bdv^^^n + m * bdv^^^n = (l + m) * bdv^^^n" + bdv_n_collect_2 " bdv^^^n + m * bdv^^^n = (1 + m) * bdv^^^n" + bdv_n_collect_3 "l * bdv^^^n + bdv^^^n = (l + 1) * bdv^^^n" (*order!*) + + bdv_n_collect_assoc1_1 "l * bdv^^^n + (m * bdv^^^n + k) = (l + m) * bdv^^^n + k" + bdv_n_collect_assoc1_2 "bdv^^^n + (m * bdv^^^n + k) = (1 + m) * bdv^^^n + k" + bdv_n_collect_assoc1_3 "l * bdv^^^n + (bdv^^^n + k) = (l + 1) * bdv^^^n + k" + + bdv_n_collect_assoc2_1 "k + l * bdv^^^n + m * bdv^^^n = k + (l + m) * bdv^^^n" + bdv_n_collect_assoc2_2 "k + bdv^^^n + m * bdv^^^n = k + (1 + m) * bdv^^^n" + bdv_n_collect_assoc2_3 "k + l * bdv^^^n + bdv^^^n = k + (l + 1) * bdv^^^n" + +(*WN.14.3.03*) + real_minus_div "- (a / b) = (-1 * a) / b" + + separate_bdv "(a * bdv) / b = (a / b) * bdv" + separate_bdv_n "(a * bdv ^^^ n) / b = (a / b) * bdv ^^^ n" + separate_1_bdv "bdv / b = (1 / b) * bdv" + separate_1_bdv_n "bdv ^^^ n / b = (1 / b) * bdv ^^^ n" + +end + + + + + +