# HG changeset patch # User Walther Neuper # Date 1283784982 -7200 # Node ID 03bfbc48010741ac28fb94d53f75b566e080c00e # Parent 66f3570ba808657727be3138bd5a1fcc604a42d7 corrected format for axioms in remaining theories diff -r 66f3570ba808 -r 03bfbc480107 src/Tools/isac/Knowledge/Biegelinie.thy --- a/src/Tools/isac/Knowledge/Biegelinie.thy Mon Sep 06 15:53:18 2010 +0200 +++ b/src/Tools/isac/Knowledge/Biegelinie.thy Mon Sep 06 16:56:22 2010 +0200 @@ -57,19 +57,19 @@ bool list] => bool list" ("((Script SetzeRandbedScript (_ _ =))// (_))" 9) -rules +axioms - Querkraft_Belastung "Q' x = -q_ x" - Belastung_Querkraft "-q_ x = Q' x" + Querkraft_Belastung: "Q' x = -q_ x" + Belastung_Querkraft: "-q_ x = Q' x" - Moment_Querkraft "M_b' x = Q x" - Querkraft_Moment "Q x = M_b' x" + Moment_Querkraft: "M_b' x = Q x" + Querkraft_Moment: "Q x = M_b' x" - Neigung_Moment "y'' x = -M_b x/ EI" - Moment_Neigung "M_b x = -EI * y'' x" + Neigung_Moment: "y'' x = -M_b x/ EI" + Moment_Neigung: "M_b x = -EI * y'' x" (*according to rls 'simplify_Integral': .. = 1/a * .. instead .. = ../ a*) - make_fun_explicit "Not (a =!= 0) ==> (a * (f x) = b) = (f x = 1/a * b)" + make_fun_explicit: "Not (a =!= 0) ==> (a * (f x) = b) = (f x = 1/a * b)" ML {* val thy = @{theory}; diff -r 66f3570ba808 -r 03bfbc480107 src/Tools/isac/Knowledge/Diff.thy --- a/src/Tools/isac/Knowledge/Diff.thy Mon Sep 06 15:53:18 2010 +0200 +++ b/src/Tools/isac/Knowledge/Diff.thy Mon Sep 06 16:56:22 2010 +0200 @@ -48,46 +48,46 @@ axioms (*stated as axioms, todo: prove as theorems 'bdv' is a constant on the meta-level *) - diff_const "[| Not (bdv occurs_in a) |] ==> d_d bdv a = 0" - diff_var "d_d bdv bdv = 1" - diff_prod_const"[| Not (bdv occurs_in u) |] ==> + diff_const: "[| Not (bdv occurs_in a) |] ==> d_d bdv a = 0" + diff_var: "d_d bdv bdv = 1" + diff_prod_const:"[| Not (bdv occurs_in u) |] ==> d_d bdv (u * v) = u * d_d bdv v" - diff_sum "d_d bdv (u + v) = d_d bdv u + d_d bdv v" - diff_dif "d_d bdv (u - v) = d_d bdv u - d_d bdv v" - diff_prod "d_d bdv (u * v) = d_d bdv u * v + u * d_d bdv v" - diff_quot "Not (v = 0) ==> (d_d bdv (u / v) = + diff_sum: "d_d bdv (u + v) = d_d bdv u + d_d bdv v" + diff_dif: "d_d bdv (u - v) = d_d bdv u - d_d bdv v" + diff_prod: "d_d bdv (u * v) = d_d bdv u * v + u * d_d bdv v" + diff_quot: "Not (v = 0) ==> (d_d bdv (u / v) = (d_d bdv u * v - u * d_d bdv v) / v ^^^ 2)" - diff_sin "d_d bdv (sin bdv) = cos bdv" - diff_sin_chain "d_d bdv (sin u) = cos u * d_d bdv u" - diff_cos "d_d bdv (cos bdv) = - sin bdv" - diff_cos_chain "d_d bdv (cos u) = - sin u * d_d bdv u" - diff_pow "d_d bdv (bdv ^^^ n) = n * (bdv ^^^ (n - 1))" - diff_pow_chain "d_d bdv (u ^^^ n) = n * (u ^^^ (n - 1)) * d_d bdv u" - diff_ln "d_d bdv (ln bdv) = 1 / bdv" - diff_ln_chain "d_d bdv (ln u) = d_d bdv u / u" - diff_exp "d_d bdv (exp bdv) = exp bdv" - diff_exp_chain "d_d bdv (exp u) = exp u * d_d x u" + diff_sin: "d_d bdv (sin bdv) = cos bdv" + diff_sin_chain: "d_d bdv (sin u) = cos u * d_d bdv u" + diff_cos: "d_d bdv (cos bdv) = - sin bdv" + diff_cos_chain: "d_d bdv (cos u) = - sin u * d_d bdv u" + diff_pow: "d_d bdv (bdv ^^^ n) = n * (bdv ^^^ (n - 1))" + diff_pow_chain: "d_d bdv (u ^^^ n) = n * (u ^^^ (n - 1)) * d_d bdv u" + diff_ln: "d_d bdv (ln bdv) = 1 / bdv" + diff_ln_chain: "d_d bdv (ln u) = d_d bdv u / u" + diff_exp: "d_d bdv (exp bdv) = exp bdv" + diff_exp_chain: "d_d bdv (exp u) = exp u * d_d x u" (* diff_sqrt "d_d bdv (sqrt bdv) = 1 / (2 * sqrt bdv)" diff_sqrt_chain"d_d bdv (sqrt u) = d_d bdv u / (2 * sqrt u)" *) (*...*) - frac_conv "[| bdv occurs_in b; 0 < n |] ==> + frac_conv: "[| bdv occurs_in b; 0 < n |] ==> a / (b ^^^ n) = a * b ^^^ (-n)" - frac_sym_conv "n < 0 ==> a * b ^^^ n = a / b ^^^ (-n)" + frac_sym_conv: "n < 0 ==> a * b ^^^ n = a / b ^^^ (-n)" - sqrt_conv_bdv "sqrt bdv = bdv ^^^ (1 / 2)" - sqrt_conv_bdv_n "sqrt (bdv ^^^ n) = bdv ^^^ (n / 2)" - sqrt_conv "bdv occurs_in u ==> sqrt u = u ^^^ (1 / 2)" - sqrt_sym_conv "u ^^^ (a / 2) = sqrt (u ^^^ a)" + sqrt_conv_bdv: "sqrt bdv = bdv ^^^ (1 / 2)" + sqrt_conv_bdv_n: "sqrt (bdv ^^^ n) = bdv ^^^ (n / 2)" + sqrt_conv: "bdv occurs_in u ==> sqrt u = u ^^^ (1 / 2)" + sqrt_sym_conv: "u ^^^ (a / 2) = sqrt (u ^^^ a)" - root_conv "bdv occurs_in u ==> nroot n u = u ^^^ (1 / n)" - root_sym_conv "u ^^^ (a / b) = nroot b (u ^^^ a)" + root_conv: "bdv occurs_in u ==> nroot n u = u ^^^ (1 / n)" + root_sym_conv: "u ^^^ (a / b) = nroot b (u ^^^ a)" - realpow_pow_bdv "(bdv ^^^ b) ^^^ c = bdv ^^^ (b * c)" + realpow_pow_bdv: "(bdv ^^^ b) ^^^ c = bdv ^^^ (b * c)" ML {* val thy = @{theory}; diff -r 66f3570ba808 -r 03bfbc480107 src/Tools/isac/Knowledge/DiffApp.thy --- a/src/Tools/isac/Knowledge/DiffApp.thy Mon Sep 06 15:53:18 2010 +0200 +++ b/src/Tools/isac/Knowledge/DiffApp.thy Mon Sep 06 16:56:22 2010 +0200 @@ -28,7 +28,7 @@ (*for script Maximum_value*) filterVar :: "[real, 'a list] => 'a list" -(*primrec*)rules +(*primrec*)axioms filterVar_Nil "filterVar v [] = []" filterVar_Const "filterVar v (x#xs) = (if (v mem (Vars x)) then x#(filterVar v xs) diff -r 66f3570ba808 -r 03bfbc480107 src/Tools/isac/Knowledge/EqSystem.thy --- a/src/Tools/isac/Knowledge/EqSystem.thy Mon Sep 06 15:53:18 2010 +0200 +++ b/src/Tools/isac/Knowledge/EqSystem.thy Mon Sep 06 16:56:22 2010 +0200 @@ -28,32 +28,32 @@ 'bdv' is a constant handled on the meta-level specifically as a 'bound variable' *) - commute_0_equality "(0 = a) = (a = 0)" + commute_0_equality: "(0 = a) = (a = 0)" (*WN0510 see simliar rules 'isolate_' 'separate_' (by RL) [bdv_1,bdv_2,bdv_3,bdv_4] work also for 2 and 3 bdvs, ugly !*) - separate_bdvs_add + separate_bdvs_add: "[| [] from_ [bdv_1,bdv_2,bdv_3,bdv_4] occur_exactly_in a |] ==> (a + b = c) = (b = c + -1*a)" - separate_bdvs0 + separate_bdvs0: "[| some_of [bdv_1,bdv_2,bdv_3,bdv_4] occur_in b; Not (b=!=0) |] ==> (a = b) = (a + -1*b = 0)" - separate_bdvs_add1 + separate_bdvs_add1: "[| some_of [bdv_1,bdv_2,bdv_3,bdv_4] occur_in c |] ==> (a = b + c) = (a + -1*c = b)" - separate_bdvs_add2 + separate_bdvs_add2: "[| Not (some_of [bdv_1,bdv_2,bdv_3,bdv_4] occur_in a) |] ==> (a + b = c) = (b = -1*a + c)" - separate_bdvs_mult + separate_bdvs_mult: "[| [] from_ [bdv_1,bdv_2,bdv_3,bdv_4] occur_exactly_in a; Not (a=!=0) |] ==>(a * b = c) = (b = c / a)" (*requires rew_ord for termination, eg. ord_simplify_Integral; works for lists of any length, interestingly !?!*) - order_system_NxN "[a,b] = [b,a]" + order_system_NxN: "[a,b] = [b,a]" ML {* val thy = @{theory}; diff -r 66f3570ba808 -r 03bfbc480107 src/Tools/isac/Knowledge/Integrate.thy --- a/src/Tools/isac/Knowledge/Integrate.thy Mon Sep 06 15:53:18 2010 +0200 +++ b/src/Tools/isac/Knowledge/Integrate.thy Mon Sep 06 16:56:22 2010 +0200 @@ -31,18 +31,18 @@ 'bdv' is a constant handled on the meta-level specifically as a 'bound variable' *) - integral_const "Not (bdv occurs_in u) ==> Integral u D bdv = u * bdv" - integral_var "Integral bdv D bdv = bdv ^^^ 2 / 2" + integral_const: "Not (bdv occurs_in u) ==> Integral u D bdv = u * bdv" + integral_var: "Integral bdv D bdv = bdv ^^^ 2 / 2" - integral_add "Integral (u + v) D bdv = + integral_add: "Integral (u + v) D bdv = (Integral u D bdv) + (Integral v D bdv)" - integral_mult "[| Not (bdv occurs_in u); bdv occurs_in v |] ==> + integral_mult: "[| Not (bdv occurs_in u); bdv occurs_in v |] ==> Integral (u * v) D bdv = u * (Integral v D bdv)" (*WN080222: this goes into sub-terms, too ... - call_for_new_c "[| Not (matches (u + new_c v) a); Not (a is_f_x) |] ==> + call_for_new_c: "[| Not (matches (u + new_c v) a); Not (a is_f_x) |] ==> a = a + new_c a" *) - integral_pow "Integral bdv ^^^ n D bdv = bdv ^^^ (n+1) / (n + 1)" + integral_pow: "Integral bdv ^^^ n D bdv = bdv ^^^ (n+1) / (n + 1)" ML {* val thy = @{theory}; diff -r 66f3570ba808 -r 03bfbc480107 src/Tools/isac/Knowledge/LogExp.thy --- a/src/Tools/isac/Knowledge/LogExp.thy Mon Sep 06 15:53:18 2010 +0200 +++ b/src/Tools/isac/Knowledge/LogExp.thy Mon Sep 06 16:56:22 2010 +0200 @@ -17,12 +17,12 @@ => bool list" ("((Script Solve'_log (_ _=))//(_))" 9) -rules +axioms - equality_pow "0 < a ==> (l = r) = (a^^^l = a^^^r)" + equality_pow: "0 < a ==> (l = r) = (a^^^l = a^^^r)" (* this is what students ^^^^^^^... are told to do *) - equality_power "((a log b) = c) = (a^^^(a log b) = a^^^c)" - exp_invers_log "a^^^(a log b) = b" + equality_power: "((a log b) = c) = (a^^^(a log b) = a^^^c)" + exp_invers_log: "a^^^(a log b) = b" ML {* val thy = @{theory}; diff -r 66f3570ba808 -r 03bfbc480107 src/Tools/isac/Knowledge/PolyEq.thy --- a/src/Tools/isac/Knowledge/PolyEq.thy Mon Sep 06 15:53:18 2010 +0200 +++ b/src/Tools/isac/Knowledge/PolyEq.thy Mon Sep 06 16:56:22 2010 +0200 @@ -80,240 +80,240 @@ (*-------------------- rules -------------------------------------------------*) axioms - cancel_leading_coeff1 "Not (c =!= 0) ==> (a + b*bdv + c*bdv^^^2 = 0) = + 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) = + 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) = + 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) = + 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) = + 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) = + 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) = + 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) = + 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) = + 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) = + 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) = + 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) = + 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) = + cancel_leading_coeff13:"Not (c =!= 0) ==> ( b*bdv^^^2 = 0) = ( bdv^^^2 = 0/b)" - complete_square1 "(q + p*bdv + bdv^^^2 = 0) = + complete_square1: "(q + p*bdv + bdv^^^2 = 0) = (q + (p/2 + bdv)^^^2 = (p/2)^^^2)" - complete_square2 "( p*bdv + bdv^^^2 = 0) = + complete_square2: "( p*bdv + bdv^^^2 = 0) = ( (p/2 + bdv)^^^2 = (p/2)^^^2)" - complete_square3 "( bdv + bdv^^^2 = 0) = + complete_square3: "( bdv + bdv^^^2 = 0) = ( (1/2 + bdv)^^^2 = (1/2)^^^2)" - complete_square4 "(q - p*bdv + bdv^^^2 = 0) = + complete_square4: "(q - p*bdv + bdv^^^2 = 0) = (q + (p/2 - bdv)^^^2 = (p/2)^^^2)" - complete_square5 "(q + p*bdv - bdv^^^2 = 0) = + 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)" + 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)" + 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?*) + 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" + 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" + d0_true: "(0=0) = True" + d0_false: "[|Not(bdv occurs_in a);Not(a=0)|] ==> (a=0) = False" (* ---- degree 1 ----*) - d1_isolate_add1 + d1_isolate_add1: "[|Not(bdv occurs_in a)|] ==> (a + b*bdv = 0) = (b*bdv = (-1)*a)" - d1_isolate_add2 + d1_isolate_add2: "[|Not(bdv occurs_in a)|] ==> (a + bdv = 0) = ( bdv = (-1)*a)" - d1_isolate_div + d1_isolate_div: "[|Not(b=0);Not(bdv occurs_in c)|] ==> (b*bdv = c) = (bdv = c/b)" (* ---- degree 2 ----*) - d2_isolate_add1 + d2_isolate_add1: "[|Not(bdv occurs_in a)|] ==> (a + b*bdv^^^2=0) = (b*bdv^^^2= (-1)*a)" - d2_isolate_add2 + d2_isolate_add2: "[|Not(bdv occurs_in a)|] ==> (a + bdv^^^2=0) = ( bdv^^^2= (-1)*a)" - d2_isolate_div + 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)" + 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)|] ==> + d2_sqrt_equation1: "[|(0<=c);Not(bdv occurs_in c)|] ==> (bdv^^^2=c) = ((bdv=sqrt c) | (bdv=(-1)*sqrt c ))" - d2_sqrt_equation1_neg + 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) = + 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) = + 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) = + 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) = + 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) = + 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) = + 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) = + 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) = + 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|] ==> + 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 + d2_pqformula9_neg: "[|Not(bdv occurs_in q); (-1)*4*q<0|] ==> (q+ 1*bdv^^^2=0) = False" - d2_pqformula10 + 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 + d2_pqformula10_neg: "[|Not(bdv occurs_in q); (-1)*4*q<0|] ==> (q+ bdv^^^2=0) = False" - d2_abcformula1 + 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 + d2_abcformula1_neg: "[|b^^^2 - 4*a*c<0|] ==> (c + b*bdv+a*bdv^^^2=0) = False" - d2_abcformula2 + 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 + d2_abcformula2_neg: "[|1 - 4*a*c<0|] ==> (c+ bdv+a*bdv^^^2=0) = False" - d2_abcformula3 + 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 + d2_abcformula3_neg: "[|b^^^2 - 4*1*c<0|] ==> (c + b*bdv+ bdv^^^2=0) = False" - d2_abcformula4 + 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 + d2_abcformula4_neg: "[|1 - 4*1*c<0|] ==> (c + bdv+ bdv^^^2=0) = False" - d2_abcformula5 + 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 + d2_abcformula5_neg: "[|Not(bdv occurs_in c); 0 - 4*a*c<0|] ==> (c + a*bdv^^^2=0) = False" - d2_abcformula6 + 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 + d2_abcformula6_neg: "[|Not(bdv occurs_in c); 0 - 4*1*c<0|] ==> (c+ bdv^^^2=0) = False" - d2_abcformula7 + 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 + 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 + 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 + 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 + d3_reduce_equation1: "(a*bdv + b*bdv^^^2 + c*bdv^^^3=0) = (bdv=0 | (a + b*bdv + c*bdv^^^2=0))" - d3_reduce_equation2 + d3_reduce_equation2: "( bdv + b*bdv^^^2 + c*bdv^^^3=0) = (bdv=0 | (1 + b*bdv + c*bdv^^^2=0))" - d3_reduce_equation3 + d3_reduce_equation3: "(a*bdv + bdv^^^2 + c*bdv^^^3=0) = (bdv=0 | (a + bdv + c*bdv^^^2=0))" - d3_reduce_equation4 + d3_reduce_equation4: "( bdv + bdv^^^2 + c*bdv^^^3=0) = (bdv=0 | (1 + bdv + c*bdv^^^2=0))" - d3_reduce_equation5 + d3_reduce_equation5: "(a*bdv + b*bdv^^^2 + bdv^^^3=0) = (bdv=0 | (a + b*bdv + bdv^^^2=0))" - d3_reduce_equation6 + d3_reduce_equation6: "( bdv + b*bdv^^^2 + bdv^^^3=0) = (bdv=0 | (1 + b*bdv + bdv^^^2=0))" - d3_reduce_equation7 + d3_reduce_equation7: "(a*bdv + bdv^^^2 + bdv^^^3=0) = (bdv=0 | (1 + bdv + bdv^^^2=0))" - d3_reduce_equation8 + d3_reduce_equation8: "( bdv + bdv^^^2 + bdv^^^3=0) = (bdv=0 | (1 + bdv + bdv^^^2=0))" - d3_reduce_equation9 + d3_reduce_equation9: "(a*bdv + c*bdv^^^3=0) = (bdv=0 | (a + c*bdv^^^2=0))" - d3_reduce_equation10 + d3_reduce_equation10: "( bdv + c*bdv^^^3=0) = (bdv=0 | (1 + c*bdv^^^2=0))" - d3_reduce_equation11 + d3_reduce_equation11: "(a*bdv + bdv^^^3=0) = (bdv=0 | (a + bdv^^^2=0))" - d3_reduce_equation12 + d3_reduce_equation12: "( bdv + bdv^^^3=0) = (bdv=0 | (1 + bdv^^^2=0))" - d3_reduce_equation13 + d3_reduce_equation13: "( b*bdv^^^2 + c*bdv^^^3=0) = (bdv=0 | ( b*bdv + c*bdv^^^2=0))" - d3_reduce_equation14 + d3_reduce_equation14: "( bdv^^^2 + c*bdv^^^3=0) = (bdv=0 | ( bdv + c*bdv^^^2=0))" - d3_reduce_equation15 + d3_reduce_equation15: "( b*bdv^^^2 + bdv^^^3=0) = (bdv=0 | ( b*bdv + bdv^^^2=0))" - d3_reduce_equation16 + d3_reduce_equation16: "( bdv^^^2 + bdv^^^3=0) = (bdv=0 | ( bdv + bdv^^^2=0))" - d3_isolate_add1 + d3_isolate_add1: "[|Not(bdv occurs_in a)|] ==> (a + b*bdv^^^3=0) = (b*bdv^^^3= (-1)*a)" - d3_isolate_add2 + d3_isolate_add2: "[|Not(bdv occurs_in a)|] ==> (a + bdv^^^3=0) = ( bdv^^^3= (-1)*a)" - d3_isolate_div + d3_isolate_div: "[|Not(b=0);Not(bdv occurs_in a)|] ==> (b*bdv^^^3=c) = (bdv^^^3=c/b)" - d3_root_equation2 + d3_root_equation2: "(bdv^^^3=0) = (bdv=0)" - d3_root_equation1 + d3_root_equation1: "(bdv^^^3=c) = (bdv = nroot 3 c)" (* ---- degree 4 ----*) @@ -324,42 +324,42 @@ (* ---- 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_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_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_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_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_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" + 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" + 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" + 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" ML {* val thy = @{theory}; diff -r 66f3570ba808 -r 03bfbc480107 src/Tools/isac/Knowledge/RatEq.thy --- a/src/Tools/isac/Knowledge/RatEq.thy Mon Sep 06 15:53:18 2010 +0200 +++ b/src/Tools/isac/Knowledge/RatEq.thy Mon Sep 06 16:56:22 2010 +0200 @@ -24,28 +24,22 @@ (* FIXME also in Poly.thy def. --> FIXED*) (*real_diff_minus "a - b = a + (-1) * b"*) - real_rat_mult_1 - "a*(b/c) = (a*b)/c" - real_rat_mult_2 - "(a/b)*(c/d) = (a*c)/(b*d)" - real_rat_mult_3 - "(a/b)*c = (a*c)/b" - real_rat_pow - "(a/b)^^^2 = a^^^2/b^^^2" + real_rat_mult_1: "a*(b/c) = (a*b)/c" + real_rat_mult_2: "(a/b)*(c/d) = (a*c)/(b*d)" + real_rat_mult_3: "(a/b)*c = (a*c)/b" + real_rat_pow: "(a/b)^^^2 = a^^^2/b^^^2" - rat_double_rat_1 - "[|Not(c=0); Not(d=0)|] ==> (a / (c/d) = (a*d) / c)" - rat_double_rat_2 - "[|Not(b=0);Not(c=0); Not(d=0)|] ==> ((a/b) / (c/d) = (a*d) / (b*c))" - rat_double_rat_3 - "[|Not(b=0);Not(c=0)|] ==> ((a/b) / c = a / (b*c))" + rat_double_rat_1: "[|Not(c=0); Not(d=0)|] ==> (a / (c/d) = (a*d) / c)" + rat_double_rat_2: "[|Not(b=0);Not(c=0); Not(d=0)|] ==> + ((a/b) / (c/d) = (a*d) / (b*c))" + rat_double_rat_3: "[|Not(b=0);Not(c=0)|] ==> ((a/b) / c = a / (b*c))" (* equation to same denominator *) - rat_mult_denominator_both + rat_mult_denominator_both: "[|Not(b=0); Not(d=0)|] ==> ((a::real) / b = c / d) = (a*d = c*b)" - rat_mult_denominator_left + rat_mult_denominator_left: "[|Not(d=0)|] ==> ((a::real) = c / d) = (a*d = c)" - rat_mult_denominator_right + rat_mult_denominator_right: "[|Not(b=0)|] ==> ((a::real) / b = c) = (a = c*b)" ML {* diff -r 66f3570ba808 -r 03bfbc480107 src/Tools/isac/Knowledge/RootEq.thy --- a/src/Tools/isac/Knowledge/RootEq.thy Mon Sep 06 15:53:18 2010 +0200 +++ b/src/Tools/isac/Knowledge/RootEq.thy Mon Sep 06 16:56:22 2010 +0200 @@ -40,81 +40,81 @@ axioms (* normalize *) - makex1_x "a^^^1 = a" - real_assoc_1 "a+(b+c) = a+b+c" - real_assoc_2 "a*(b*c) = a*b*c" + makex1_x: "a^^^1 = a" + real_assoc_1: "a+(b+c) = a+b+c" + real_assoc_2: "a*(b*c) = a*b*c" (* simplification of root*) - sqrt_square_1 "[|0 <= a|] ==> (sqrt a)^^^2 = a" - sqrt_square_2 "sqrt (a ^^^ 2) = a" - sqrt_times_root_1 "sqrt a * sqrt b = sqrt(a*b)" - sqrt_times_root_2 "a * sqrt b * sqrt c = a * sqrt(b*c)" + sqrt_square_1: "[|0 <= a|] ==> (sqrt a)^^^2 = a" + sqrt_square_2: "sqrt (a ^^^ 2) = a" + sqrt_times_root_1: "sqrt a * sqrt b = sqrt(a*b)" + sqrt_times_root_2: "a * sqrt b * sqrt c = a * sqrt(b*c)" (* isolate one root on the LEFT or RIGHT hand side of the equation *) - sqrt_isolate_l_add1 "[|bdv occurs_in c|] ==> + sqrt_isolate_l_add1: "[|bdv occurs_in c|] ==> (a + b*sqrt(c) = d) = (b * sqrt(c) = d+ (-1) * a)" - sqrt_isolate_l_add2 "[|bdv occurs_in c|] ==> + sqrt_isolate_l_add2: "[|bdv occurs_in c|] ==> (a + sqrt(c) = d) = ((sqrt(c) = d+ (-1) * a))" - sqrt_isolate_l_add3 "[|bdv occurs_in c|] ==> + sqrt_isolate_l_add3: "[|bdv occurs_in c|] ==> (a + b*(e/sqrt(c)) = d) = (b * (e/sqrt(c)) = d + (-1) * a)" - sqrt_isolate_l_add4 "[|bdv occurs_in c|] ==> + sqrt_isolate_l_add4: "[|bdv occurs_in c|] ==> (a + b/(f*sqrt(c)) = d) = (b / (f*sqrt(c)) = d + (-1) * a)" - sqrt_isolate_l_add5 "[|bdv occurs_in c|] ==> + sqrt_isolate_l_add5: "[|bdv occurs_in c|] ==> (a + b*(e/(f*sqrt(c))) = d) = (b * (e/(f*sqrt(c))) = d+ (-1) * a)" - sqrt_isolate_l_add6 "[|bdv occurs_in c|] ==> + sqrt_isolate_l_add6: "[|bdv occurs_in c|] ==> (a + b/sqrt(c) = d) = (b / sqrt(c) = d+ (-1) * a)" - sqrt_isolate_r_add1 "[|bdv occurs_in f|] ==> + sqrt_isolate_r_add1: "[|bdv occurs_in f|] ==> (a = d + e*sqrt(f)) = (a + (-1) * d = e*sqrt(f))" - sqrt_isolate_r_add2 "[|bdv occurs_in f|] ==> + sqrt_isolate_r_add2: "[|bdv occurs_in f|] ==> (a = d + sqrt(f)) = (a + (-1) * d = sqrt(f))" (* small hack: thm 3,5,6 are not needed if rootnormalize is well done*) - sqrt_isolate_r_add3 "[|bdv occurs_in f|] ==> + sqrt_isolate_r_add3: "[|bdv occurs_in f|] ==> (a = d + e*(g/sqrt(f))) = (a + (-1) * d = e*(g/sqrt(f)))" - sqrt_isolate_r_add4 "[|bdv occurs_in f|] ==> + sqrt_isolate_r_add4: "[|bdv occurs_in f|] ==> (a = d + g/sqrt(f)) = (a + (-1) * d = g/sqrt(f))" - sqrt_isolate_r_add5 "[|bdv occurs_in f|] ==> + sqrt_isolate_r_add5: "[|bdv occurs_in f|] ==> (a = d + e*(g/(h*sqrt(f)))) = (a + (-1) * d = e*(g/(h*sqrt(f))))" - sqrt_isolate_r_add6 "[|bdv occurs_in f|] ==> + sqrt_isolate_r_add6: "[|bdv occurs_in f|] ==> (a = d + g/(h*sqrt(f))) = (a + (-1) * d = g/(h*sqrt(f)))" (* eliminate isolates sqrt *) - sqrt_square_equation_both_1 "[|bdv occurs_in b; bdv occurs_in d|] ==> + sqrt_square_equation_both_1: "[|bdv occurs_in b; bdv occurs_in d|] ==> ( (sqrt a + sqrt b = sqrt c + sqrt d) = (a+2*sqrt(a)*sqrt(b)+b = c+2*sqrt(c)*sqrt(d)+d))" - sqrt_square_equation_both_2 "[|bdv occurs_in b; bdv occurs_in d|] ==> + sqrt_square_equation_both_2: "[|bdv occurs_in b; bdv occurs_in d|] ==> ( (sqrt a - sqrt b = sqrt c + sqrt d) = (a - 2*sqrt(a)*sqrt(b)+b = c+2*sqrt(c)*sqrt(d)+d))" - sqrt_square_equation_both_3 "[|bdv occurs_in b; bdv occurs_in d|] ==> + sqrt_square_equation_both_3: "[|bdv occurs_in b; bdv occurs_in d|] ==> ( (sqrt a + sqrt b = sqrt c - sqrt d) = (a + 2*sqrt(a)*sqrt(b)+b = c - 2*sqrt(c)*sqrt(d)+d))" - sqrt_square_equation_both_4 "[|bdv occurs_in b; bdv occurs_in d|] ==> + sqrt_square_equation_both_4: "[|bdv occurs_in b; bdv occurs_in d|] ==> ( (sqrt a - sqrt b = sqrt c - sqrt d) = (a - 2*sqrt(a)*sqrt(b)+b = c - 2*sqrt(c)*sqrt(d)+d))" - sqrt_square_equation_left_1 "[|bdv occurs_in a; 0 <= a; 0 <= b|] ==> + sqrt_square_equation_left_1: "[|bdv occurs_in a; 0 <= a; 0 <= b|] ==> ( (sqrt (a) = b) = (a = (b^^^2)))" - sqrt_square_equation_left_2 "[|bdv occurs_in a; 0 <= a; 0 <= b*c|] ==> + sqrt_square_equation_left_2: "[|bdv occurs_in a; 0 <= a; 0 <= b*c|] ==> ( (c*sqrt(a) = b) = (c^^^2*a = b^^^2))" - sqrt_square_equation_left_3 "[|bdv occurs_in a; 0 <= a; 0 <= b*c|] ==> + sqrt_square_equation_left_3: "[|bdv occurs_in a; 0 <= a; 0 <= b*c|] ==> ( c/sqrt(a) = b) = (c^^^2 / a = b^^^2)" (* small hack: thm 4-6 are not needed if rootnormalize is well done*) - sqrt_square_equation_left_4 "[|bdv occurs_in a; 0 <= a; 0 <= b*c*d|] ==> + sqrt_square_equation_left_4: "[|bdv occurs_in a; 0 <= a; 0 <= b*c*d|] ==> ( (c*(d/sqrt (a)) = b) = (c^^^2*(d^^^2/a) = b^^^2))" - sqrt_square_equation_left_5 "[|bdv occurs_in a; 0 <= a; 0 <= b*c*d|] ==> + sqrt_square_equation_left_5: "[|bdv occurs_in a; 0 <= a; 0 <= b*c*d|] ==> ( c/(d*sqrt(a)) = b) = (c^^^2 / (d^^^2*a) = b^^^2)" - sqrt_square_equation_left_6 "[|bdv occurs_in a; 0 <= a; 0 <= b*c*d*e|] ==> + sqrt_square_equation_left_6: "[|bdv occurs_in a; 0 <= a; 0 <= b*c*d*e|] ==> ( (c*(d/(e*sqrt (a))) = b) = (c^^^2*(d^^^2/(e^^^2*a)) = b^^^2))" - sqrt_square_equation_right_1 "[|bdv occurs_in b; 0 <= a; 0 <= b|] ==> + sqrt_square_equation_right_1: "[|bdv occurs_in b; 0 <= a; 0 <= b|] ==> ( (a = sqrt (b)) = (a^^^2 = b))" - sqrt_square_equation_right_2 "[|bdv occurs_in b; 0 <= a*c; 0 <= b|] ==> + sqrt_square_equation_right_2: "[|bdv occurs_in b; 0 <= a*c; 0 <= b|] ==> ( (a = c*sqrt (b)) = ((a^^^2) = c^^^2*b))" - sqrt_square_equation_right_3 "[|bdv occurs_in b; 0 <= a*c; 0 <= b|] ==> + sqrt_square_equation_right_3: "[|bdv occurs_in b; 0 <= a*c; 0 <= b|] ==> ( (a = c/sqrt (b)) = (a^^^2 = c^^^2/b))" (* small hack: thm 4-6 are not needed if rootnormalize is well done*) - sqrt_square_equation_right_4 "[|bdv occurs_in b; 0 <= a*c*d; 0 <= b|] ==> + sqrt_square_equation_right_4: "[|bdv occurs_in b; 0 <= a*c*d; 0 <= b|] ==> ( (a = c*(d/sqrt (b))) = ((a^^^2) = c^^^2*(d^^^2/b)))" - sqrt_square_equation_right_5 "[|bdv occurs_in b; 0 <= a*c*d; 0 <= b|] ==> + sqrt_square_equation_right_5: "[|bdv occurs_in b; 0 <= a*c*d; 0 <= b|] ==> ( (a = c/(d*sqrt (b))) = (a^^^2 = c^^^2/(d^^^2*b)))" - sqrt_square_equation_right_6 "[|bdv occurs_in b; 0 <= a*c*d*e; 0 <= b|] ==> + sqrt_square_equation_right_6: "[|bdv occurs_in b; 0 <= a*c*d*e; 0 <= b|] ==> ( (a = c*(d/(e*sqrt (b)))) = ((a^^^2) = c^^^2*(d^^^2/(e^^^2*b))))" ML {* diff -r 66f3570ba808 -r 03bfbc480107 src/Tools/isac/Knowledge/RootRatEq.thy --- a/src/Tools/isac/Knowledge/RootRatEq.thy Mon Sep 06 15:53:18 2010 +0200 +++ b/src/Tools/isac/Knowledge/RootRatEq.thy Mon Sep 06 16:56:22 2010 +0200 @@ -24,13 +24,13 @@ axioms (* eliminate ratRootTerm *) - rootrat_equation_left_1 + rootrat_equation_left_1: "[|c is_rootTerm_in bdv|] ==> ( (a + b/c = d) = ( b = (d - a) * c ))" - rootrat_equation_left_2 + rootrat_equation_left_2: "[|c is_rootTerm_in bdv|] ==> ( (b/c = d) = ( b = d * c ))" - rootrat_equation_right_2 + rootrat_equation_right_2: "[|f is_rootTerm_in bdv|] ==> ( (a = d + e/f) = ( (a - d) * f = e ))" - rootrat_equation_right_1 + rootrat_equation_right_1: "[|f is_rootTerm_in bdv|] ==> ( (a = e/f) = ( a * f = e ))" ML {* diff -r 66f3570ba808 -r 03bfbc480107 src/Tools/isac/Knowledge/Test.thy --- a/src/Tools/isac/Knowledge/Test.thy Mon Sep 06 15:53:18 2010 +0200 +++ b/src/Tools/isac/Knowledge/Test.thy Mon Sep 06 16:56:22 2010 +0200 @@ -60,108 +60,108 @@ axioms (*TODO: prove as theorems*) - radd_mult_distrib2 "(k::real) * (m + n) = k * m + k * n" - rdistr_right_assoc "(k::real) + l * n + m * n = k + (l + m) * n" - rdistr_right_assoc_p "l * n + (m * n + (k::real)) = (l + m) * n + k" - rdistr_div_right "((k::real) + l) / n = k / n + l / n" - rcollect_right + radd_mult_distrib2: "(k::real) * (m + n) = k * m + k * n" + rdistr_right_assoc: "(k::real) + l * n + m * n = k + (l + m) * n" + rdistr_right_assoc_p: "l * n + (m * n + (k::real)) = (l + m) * n + k" + rdistr_div_right: "((k::real) + l) / n = k / n + l / n" + rcollect_right: "[| l is_const; m is_const |] ==> (l::real)*n + m*n = (l + m) * n" - rcollect_one_left + rcollect_one_left: "m is_const ==> (n::real) + m * n = (1 + m) * n" - rcollect_one_left_assoc + rcollect_one_left_assoc: "m is_const ==> (k::real) + n + m * n = k + (1 + m) * n" - rcollect_one_left_assoc_p + rcollect_one_left_assoc_p: "m is_const ==> n + (m * n + (k::real)) = (1 + m) * n + k" - rtwo_of_the_same "a + a = 2 * a" - rtwo_of_the_same_assoc "(x + a) + a = x + 2 * a" - rtwo_of_the_same_assoc_p"a + (a + x) = 2 * a + x" + rtwo_of_the_same: "a + a = 2 * a" + rtwo_of_the_same_assoc: "(x + a) + a = x + 2 * a" + rtwo_of_the_same_assoc_p:"a + (a + x) = 2 * a + x" - rcancel_den "not(a=0) ==> a * (b / a) = b" - rcancel_const "[| a is_const; b is_const |] ==> a*(x/b) = a/b*x" - rshift_nominator "(a::real) * b / c = a / c * b" + rcancel_den: "not(a=0) ==> a * (b / a) = b" + rcancel_const: "[| a is_const; b is_const |] ==> a*(x/b) = a/b*x" + rshift_nominator: "(a::real) * b / c = a / c * b" - exp_pow "(a ^^^ b) ^^^ c = a ^^^ (b * c)" - rsqare "(a::real) * a = a ^^^ 2" - power_1 "(a::real) ^^^ 1 = a" - rbinom_power_2 "((a::real) + b)^^^ 2 = a^^^ 2 + 2*a*b + b^^^ 2" + exp_pow: "(a ^^^ b) ^^^ c = a ^^^ (b * c)" + rsqare: "(a::real) * a = a ^^^ 2" + power_1: "(a::real) ^^^ 1 = a" + rbinom_power_2: "((a::real) + b)^^^ 2 = a^^^ 2 + 2*a*b + b^^^ 2" - rmult_1 "1 * k = (k::real)" - rmult_1_right "k * 1 = (k::real)" - rmult_0 "0 * k = (0::real)" - rmult_0_right "k * 0 = (0::real)" - radd_0 "0 + k = (k::real)" - radd_0_right "k + 0 = (k::real)" + rmult_1: "1 * k = (k::real)" + rmult_1_right: "k * 1 = (k::real)" + rmult_0: "0 * k = (0::real)" + rmult_0_right: "k * 0 = (0::real)" + radd_0: "0 + k = (k::real)" + radd_0_right: "k + 0 = (k::real)" - radd_real_const_eq + radd_real_const_eq: "[| a is_const; c is_const; d is_const |] ==> a/d + c/d = (a+c)/(d::real)" - radd_real_const + radd_real_const: "[| a is_const; b is_const; c is_const; d is_const |] ==> a/b + c/d = (a*d + b*c)/(b*(d::real))" (*for AC-operators*) - radd_commute "(m::real) + (n::real) = n + m" - radd_left_commute "(x::real) + (y + z) = y + (x + z)" - radd_assoc "(m::real) + n + k = m + (n + k)" - rmult_commute "(m::real) * n = n * m" - rmult_left_commute "(x::real) * (y * z) = y * (x * z)" - rmult_assoc "(m::real) * n * k = m * (n * k)" + radd_commute: "(m::real) + (n::real) = n + m" + radd_left_commute: "(x::real) + (y + z) = y + (x + z)" + radd_assoc: "(m::real) + n + k = m + (n + k)" + rmult_commute: "(m::real) * n = n * m" + rmult_left_commute: "(x::real) * (y * z) = y * (x * z)" + rmult_assoc: "(m::real) * n * k = m * (n * k)" (*for equations: 'bdv' is a meta-constant*) - risolate_bdv_add "((k::real) + bdv = m) = (bdv = m + (-1)*k)" - risolate_bdv_mult_add "((k::real) + n*bdv = m) = (n*bdv = m + (-1)*k)" - risolate_bdv_mult "((n::real) * bdv = m) = (bdv = m / n)" + risolate_bdv_add: "((k::real) + bdv = m) = (bdv = m + (-1)*k)" + risolate_bdv_mult_add: "((k::real) + n*bdv = m) = (n*bdv = m + (-1)*k)" + risolate_bdv_mult: "((n::real) * bdv = m) = (bdv = m / n)" - rnorm_equation_add + rnorm_equation_add: "~(b =!= 0) ==> (a = b) = (a + (-1)*b = 0)" (*17.9.02 aus SqRoot.thy------------------------------vvv---*) - root_ge0 "0 <= a ==> 0 <= sqrt a" + root_ge0: "0 <= a ==> 0 <= sqrt a" (*should be dropped with better simplification in eval_rls ...*) - root_add_ge0 + root_add_ge0: "[| 0 <= a; 0 <= b |] ==> (0 <= sqrt a + sqrt b) = True" - root_ge0_1 + root_ge0_1: "[| 0<=a; 0<=b; 0<=c |] ==> (0 <= a * sqrt b + sqrt c) = True" - root_ge0_2 + root_ge0_2: "[| 0<=a; 0<=b; 0<=c |] ==> (0 <= sqrt a + b * sqrt c) = True" - rroot_square_inv "(sqrt a)^^^ 2 = a" - rroot_times_root "sqrt a * sqrt b = sqrt(a*b)" - rroot_times_root_assoc "(a * sqrt b) * sqrt c = a * sqrt(b*c)" - rroot_times_root_assoc_p "sqrt b * (sqrt c * a)= sqrt(b*c) * a" + rroot_square_inv: "(sqrt a)^^^ 2 = a" + rroot_times_root: "sqrt a * sqrt b = sqrt(a*b)" + rroot_times_root_assoc: "(a * sqrt b) * sqrt c = a * sqrt(b*c)" + rroot_times_root_assoc_p: "sqrt b * (sqrt c * a)= sqrt(b*c) * a" (*for root-equations*) - square_equation_left + square_equation_left: "[| 0 <= a; 0 <= b |] ==> (((sqrt a)=b)=(a=(b^^^ 2)))" - square_equation_right + square_equation_right: "[| 0 <= a; 0 <= b |] ==> ((a=(sqrt b))=((a^^^ 2)=b))" (*causes frequently non-termination:*) - square_equation + square_equation: "[| 0 <= a; 0 <= b |] ==> ((a=b)=((a^^^ 2)=b^^^ 2))" - risolate_root_add "(a+ sqrt c = d) = ( sqrt c = d + (-1)*a)" - risolate_root_mult "(a+b*sqrt c = d) = (b*sqrt c = d + (-1)*a)" - risolate_root_div "(a * sqrt c = d) = ( sqrt c = d / a)" + risolate_root_add: "(a+ sqrt c = d) = ( sqrt c = d + (-1)*a)" + risolate_root_mult: "(a+b*sqrt c = d) = (b*sqrt c = d + (-1)*a)" + risolate_root_div: "(a * sqrt c = d) = ( sqrt c = d / a)" (*for polynomial equations of degree 2; linear case in RatArith*) - mult_square "(a*bdv^^^2 = b) = (bdv^^^2 = b / a)" - constant_square "(a + bdv^^^2 = b) = (bdv^^^2 = b + -1*a)" - constant_mult_square "(a + b*bdv^^^2 = c) = (b*bdv^^^2 = c + -1*a)" + mult_square: "(a*bdv^^^2 = b) = (bdv^^^2 = b / a)" + constant_square: "(a + bdv^^^2 = b) = (bdv^^^2 = b + -1*a)" + constant_mult_square: "(a + b*bdv^^^2 = c) = (b*bdv^^^2 = c + -1*a)" - square_equality + square_equality: "0 <= a ==> (x^^^2 = a) = ((x=sqrt a) | (x=-1*sqrt a))" - square_equality_0 + square_equality_0: "(x^^^2 = 0) = (x = 0)" (*isolate root on the LEFT hand side of the equation otherwise shuffling from left to right would not terminate*) - rroot_to_lhs + rroot_to_lhs: "is_root_free a ==> (a = sqrt b) = (a + (-1)*sqrt b = 0)" - rroot_to_lhs_mult + rroot_to_lhs_mult: "is_root_free a ==> (a = c*sqrt b) = (a + (-1)*c*sqrt b = 0)" - rroot_to_lhs_add_mult + rroot_to_lhs_add_mult: "is_root_free a ==> (a = d+c*sqrt b) = (a + (-1)*c*sqrt b = d)" (*17.9.02 aus SqRoot.thy------------------------------^^^---*)