diff -r a28b5fc129b7 -r 22235e4dbe5f src/Tools/isac/IsacKnowledge/PolyEq.thy --- a/src/Tools/isac/IsacKnowledge/PolyEq.thy Wed Aug 25 15:15:01 2010 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,407 +0,0 @@ -(*.(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"IsacKnowledge/Isac"; - use_thy"IsacKnowledge/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 - - - - - -