neuper@37906: (*.(c) by Richard Lang, 2003 .*) neuper@37906: (* collecting all knowledge for Root Equations neuper@37906: created by: rlang neuper@37906: date: 02.08 neuper@37906: changed by: rlang neuper@37906: last change by: rlang neuper@37906: date: 02.11.14 neuper@37906: *) neuper@37906: neuper@37985: theory RootEq imports Root begin neuper@37906: neuper@37906: consts neuper@37985: neuper@37985: is'_rootTerm'_in :: "[real, real] => bool" ("_ is'_rootTerm'_in _") neuper@37950: is'_sqrtTerm'_in :: "[real, real] => bool" ("_ is'_sqrtTerm'_in _") neuper@37950: is'_normSqrtTerm'_in :: "[real, real] => bool" ("_ is'_normSqrtTerm'_in _") neuper@37950: neuper@37906: (*----------------------scripts-----------------------*) neuper@37906: Norm'_sq'_root'_equation neuper@37950: :: "[bool,real, neuper@37950: bool list] => bool list" neuper@37950: ("((Script Norm'_sq'_root'_equation (_ _ =))// neuper@37950: (_))" 9) neuper@37906: Solve'_sq'_root'_equation neuper@37950: :: "[bool,real, neuper@37950: bool list] => bool list" neuper@37950: ("((Script Solve'_sq'_root'_equation (_ _ =))// neuper@37950: (_))" 9) neuper@37906: Solve'_left'_sq'_root'_equation neuper@37950: :: "[bool,real, neuper@37950: bool list] => bool list" neuper@37950: ("((Script Solve'_left'_sq'_root'_equation (_ _ =))// neuper@37950: (_))" 9) neuper@37906: Solve'_right'_sq'_root'_equation neuper@37950: :: "[bool,real, neuper@37950: bool list] => bool list" neuper@37950: ("((Script Solve'_right'_sq'_root'_equation (_ _ =))// neuper@37950: (_))" 9) neuper@37906: neuper@37950: axioms neuper@37906: neuper@37906: (* normalize *) neuper@37983: makex1_x: "a^^^1 = a" neuper@37983: real_assoc_1: "a+(b+c) = a+b+c" neuper@37983: real_assoc_2: "a*(b*c) = a*b*c" neuper@37906: neuper@37906: (* simplification of root*) neuper@37983: sqrt_square_1: "[|0 <= a|] ==> (sqrt a)^^^2 = a" neuper@37983: sqrt_square_2: "sqrt (a ^^^ 2) = a" neuper@37983: sqrt_times_root_1: "sqrt a * sqrt b = sqrt(a*b)" neuper@37983: sqrt_times_root_2: "a * sqrt b * sqrt c = a * sqrt(b*c)" neuper@37906: neuper@37906: (* isolate one root on the LEFT or RIGHT hand side of the equation *) neuper@37983: sqrt_isolate_l_add1: "[|bdv occurs_in c|] ==> neuper@37950: (a + b*sqrt(c) = d) = (b * sqrt(c) = d+ (-1) * a)" neuper@37983: sqrt_isolate_l_add2: "[|bdv occurs_in c|] ==> neuper@37950: (a + sqrt(c) = d) = ((sqrt(c) = d+ (-1) * a))" neuper@37983: sqrt_isolate_l_add3: "[|bdv occurs_in c|] ==> neuper@37950: (a + b*(e/sqrt(c)) = d) = (b * (e/sqrt(c)) = d + (-1) * a)" neuper@37983: sqrt_isolate_l_add4: "[|bdv occurs_in c|] ==> neuper@37950: (a + b/(f*sqrt(c)) = d) = (b / (f*sqrt(c)) = d + (-1) * a)" neuper@37983: sqrt_isolate_l_add5: "[|bdv occurs_in c|] ==> neuper@37950: (a + b*(e/(f*sqrt(c))) = d) = (b * (e/(f*sqrt(c))) = d+ (-1) * a)" neuper@37983: sqrt_isolate_l_add6: "[|bdv occurs_in c|] ==> neuper@37950: (a + b/sqrt(c) = d) = (b / sqrt(c) = d+ (-1) * a)" neuper@37983: sqrt_isolate_r_add1: "[|bdv occurs_in f|] ==> neuper@37950: (a = d + e*sqrt(f)) = (a + (-1) * d = e*sqrt(f))" neuper@37983: sqrt_isolate_r_add2: "[|bdv occurs_in f|] ==> neuper@37950: (a = d + sqrt(f)) = (a + (-1) * d = sqrt(f))" neuper@37906: (* small hack: thm 3,5,6 are not needed if rootnormalize is well done*) neuper@37983: sqrt_isolate_r_add3: "[|bdv occurs_in f|] ==> neuper@37950: (a = d + e*(g/sqrt(f))) = (a + (-1) * d = e*(g/sqrt(f)))" neuper@37983: sqrt_isolate_r_add4: "[|bdv occurs_in f|] ==> neuper@37950: (a = d + g/sqrt(f)) = (a + (-1) * d = g/sqrt(f))" neuper@37983: sqrt_isolate_r_add5: "[|bdv occurs_in f|] ==> neuper@37950: (a = d + e*(g/(h*sqrt(f)))) = (a + (-1) * d = e*(g/(h*sqrt(f))))" neuper@37983: sqrt_isolate_r_add6: "[|bdv occurs_in f|] ==> neuper@37950: (a = d + g/(h*sqrt(f))) = (a + (-1) * d = g/(h*sqrt(f)))" neuper@37906: neuper@37906: (* eliminate isolates sqrt *) neuper@37983: sqrt_square_equation_both_1: "[|bdv occurs_in b; bdv occurs_in d|] ==> neuper@37950: ( (sqrt a + sqrt b = sqrt c + sqrt d) = neuper@37950: (a+2*sqrt(a)*sqrt(b)+b = c+2*sqrt(c)*sqrt(d)+d))" neuper@37983: sqrt_square_equation_both_2: "[|bdv occurs_in b; bdv occurs_in d|] ==> neuper@37950: ( (sqrt a - sqrt b = sqrt c + sqrt d) = neuper@37950: (a - 2*sqrt(a)*sqrt(b)+b = c+2*sqrt(c)*sqrt(d)+d))" neuper@37983: sqrt_square_equation_both_3: "[|bdv occurs_in b; bdv occurs_in d|] ==> neuper@37950: ( (sqrt a + sqrt b = sqrt c - sqrt d) = neuper@37950: (a + 2*sqrt(a)*sqrt(b)+b = c - 2*sqrt(c)*sqrt(d)+d))" neuper@37983: sqrt_square_equation_both_4: "[|bdv occurs_in b; bdv occurs_in d|] ==> neuper@37950: ( (sqrt a - sqrt b = sqrt c - sqrt d) = neuper@37950: (a - 2*sqrt(a)*sqrt(b)+b = c - 2*sqrt(c)*sqrt(d)+d))" neuper@37983: sqrt_square_equation_left_1: "[|bdv occurs_in a; 0 <= a; 0 <= b|] ==> neuper@37950: ( (sqrt (a) = b) = (a = (b^^^2)))" neuper@37983: sqrt_square_equation_left_2: "[|bdv occurs_in a; 0 <= a; 0 <= b*c|] ==> neuper@37950: ( (c*sqrt(a) = b) = (c^^^2*a = b^^^2))" neuper@37983: sqrt_square_equation_left_3: "[|bdv occurs_in a; 0 <= a; 0 <= b*c|] ==> neuper@37950: ( c/sqrt(a) = b) = (c^^^2 / a = b^^^2)" neuper@37906: (* small hack: thm 4-6 are not needed if rootnormalize is well done*) neuper@37983: sqrt_square_equation_left_4: "[|bdv occurs_in a; 0 <= a; 0 <= b*c*d|] ==> neuper@37950: ( (c*(d/sqrt (a)) = b) = (c^^^2*(d^^^2/a) = b^^^2))" neuper@37983: sqrt_square_equation_left_5: "[|bdv occurs_in a; 0 <= a; 0 <= b*c*d|] ==> neuper@37950: ( c/(d*sqrt(a)) = b) = (c^^^2 / (d^^^2*a) = b^^^2)" neuper@37983: sqrt_square_equation_left_6: "[|bdv occurs_in a; 0 <= a; 0 <= b*c*d*e|] ==> neuper@37950: ( (c*(d/(e*sqrt (a))) = b) = (c^^^2*(d^^^2/(e^^^2*a)) = b^^^2))" neuper@37983: sqrt_square_equation_right_1: "[|bdv occurs_in b; 0 <= a; 0 <= b|] ==> neuper@37950: ( (a = sqrt (b)) = (a^^^2 = b))" neuper@37983: sqrt_square_equation_right_2: "[|bdv occurs_in b; 0 <= a*c; 0 <= b|] ==> neuper@37950: ( (a = c*sqrt (b)) = ((a^^^2) = c^^^2*b))" neuper@37983: sqrt_square_equation_right_3: "[|bdv occurs_in b; 0 <= a*c; 0 <= b|] ==> neuper@37950: ( (a = c/sqrt (b)) = (a^^^2 = c^^^2/b))" neuper@37906: (* small hack: thm 4-6 are not needed if rootnormalize is well done*) neuper@37983: sqrt_square_equation_right_4: "[|bdv occurs_in b; 0 <= a*c*d; 0 <= b|] ==> neuper@37950: ( (a = c*(d/sqrt (b))) = ((a^^^2) = c^^^2*(d^^^2/b)))" neuper@37983: sqrt_square_equation_right_5: "[|bdv occurs_in b; 0 <= a*c*d; 0 <= b|] ==> neuper@37950: ( (a = c/(d*sqrt (b))) = (a^^^2 = c^^^2/(d^^^2*b)))" neuper@37983: sqrt_square_equation_right_6: "[|bdv occurs_in b; 0 <= a*c*d*e; 0 <= b|] ==> neuper@37950: ( (a = c*(d/(e*sqrt (b)))) = ((a^^^2) = c^^^2*(d^^^2/(e^^^2*b))))" neuper@37950: neuper@37950: ML {* neuper@37972: val thy = @{theory}; neuper@37972: neuper@37950: (*-------------------------functions---------------------*) neuper@37950: (* true if bdv is under sqrt of a Equation*) neuper@37950: fun is_rootTerm_in t v = neuper@37950: let neuper@37950: fun coeff_in c v = member op = (vars c) v; neuper@38031: fun findroot (_ $ _ $ _ $ _) v = error("is_rootTerm_in:") neuper@37950: (* at the moment there is no term like this, but ....*) neuper@37950: | findroot (t as (Const ("Root.nroot",_) $ _ $ t3)) v = coeff_in t3 v neuper@37950: | findroot (_ $ t2 $ t3) v = (findroot t2 v) orelse (findroot t3 v) neuper@37982: | findroot (t as (Const ("NthRoot.sqrt",_) $ t2)) v = coeff_in t2 v neuper@37950: | findroot (_ $ t2) v = (findroot t2 v) neuper@37950: | findroot _ _ = false; neuper@37950: in neuper@37950: findroot t v neuper@37950: end; neuper@37950: neuper@37950: fun is_sqrtTerm_in t v = neuper@37950: let neuper@37950: fun coeff_in c v = member op = (vars c) v; neuper@38031: fun findsqrt (_ $ _ $ _ $ _) v = error("is_sqrteqation_in:") neuper@37950: (* at the moment there is no term like this, but ....*) neuper@37950: | findsqrt (_ $ t1 $ t2) v = (findsqrt t1 v) orelse (findsqrt t2 v) neuper@37982: | findsqrt (t as (Const ("NthRoot.sqrt",_) $ a)) v = coeff_in a v neuper@37950: | findsqrt (_ $ t1) v = (findsqrt t1 v) neuper@37950: | findsqrt _ _ = false; neuper@37950: in neuper@37950: findsqrt t v neuper@37950: end; neuper@37950: neuper@37950: (* RL: 030518: Is in the rightest subterm of a term a sqrt with bdv, neuper@37950: and the subterm ist connected with + or * --> is normalized*) neuper@37950: fun is_normSqrtTerm_in t v = neuper@37950: let neuper@37950: fun coeff_in c v = member op = (vars c) v; neuper@38031: fun isnorm (_ $ _ $ _ $ _) v = error("is_normSqrtTerm_in:") neuper@37950: (* at the moment there is no term like this, but ....*) neuper@38014: | isnorm (Const ("Groups.plus_class.plus",_) $ _ $ t2) v = is_sqrtTerm_in t2 v neuper@37950: | isnorm (Const ("op *",_) $ _ $ t2) v = is_sqrtTerm_in t2 v neuper@38014: | isnorm (Const ("Groups.minus_class.minus",_) $ _ $ _) v = false neuper@38014: | isnorm (Const ("Rings.inverse_class.divide",_) $ t1 $ t2) v = (is_sqrtTerm_in t1 v) orelse neuper@37950: (is_sqrtTerm_in t2 v) neuper@37982: | isnorm (Const ("NthRoot.sqrt",_) $ t1) v = coeff_in t1 v neuper@37950: | isnorm (_ $ t1) v = is_sqrtTerm_in t1 v neuper@37950: | isnorm _ _ = false; neuper@37950: in neuper@37950: isnorm t v neuper@37950: end; neuper@37950: neuper@37950: fun eval_is_rootTerm_in _ _ neuper@37950: (p as (Const ("RootEq.is'_rootTerm'_in",_) $ t $ v)) _ = neuper@37950: if is_rootTerm_in t v then neuper@37950: SOME ((term2str p) ^ " = True", neuper@37950: Trueprop $ (mk_equality (p, HOLogic.true_const))) neuper@37950: else SOME ((term2str p) ^ " = True", neuper@37950: Trueprop $ (mk_equality (p, HOLogic.false_const))) neuper@38015: | eval_is_rootTerm_in _ _ _ _ = ((*tracing"### nichts matcht";*) NONE); neuper@37950: neuper@37950: fun eval_is_sqrtTerm_in _ _ neuper@37950: (p as (Const ("RootEq.is'_sqrtTerm'_in",_) $ t $ v)) _ = neuper@37950: if is_sqrtTerm_in t v then neuper@37950: SOME ((term2str p) ^ " = True", neuper@37950: Trueprop $ (mk_equality (p, HOLogic.true_const))) neuper@37950: else SOME ((term2str p) ^ " = True", neuper@37950: Trueprop $ (mk_equality (p, HOLogic.false_const))) neuper@38015: | eval_is_sqrtTerm_in _ _ _ _ = ((*tracing"### nichts matcht";*) NONE); neuper@37950: neuper@37950: fun eval_is_normSqrtTerm_in _ _ neuper@37950: (p as (Const ("RootEq.is'_normSqrtTerm'_in",_) $ t $ v)) _ = neuper@37950: if is_normSqrtTerm_in t v then neuper@37950: SOME ((term2str p) ^ " = True", neuper@37950: Trueprop $ (mk_equality (p, HOLogic.true_const))) neuper@37950: else SOME ((term2str p) ^ " = True", neuper@37950: Trueprop $ (mk_equality (p, HOLogic.false_const))) neuper@38015: | eval_is_normSqrtTerm_in _ _ _ _ = ((*tracing"### nichts matcht";*) NONE); neuper@37950: neuper@37950: (*-------------------------rulse-------------------------*) neuper@37950: val RootEq_prls =(*15.10.02:just the following order due to subterm evaluation*) neuper@37950: append_rls "RootEq_prls" e_rls neuper@37950: [Calc ("Atools.ident",eval_ident "#ident_"), neuper@37950: Calc ("Tools.matches",eval_matches ""), neuper@37950: Calc ("Tools.lhs" ,eval_lhs ""), neuper@37950: Calc ("Tools.rhs" ,eval_rhs ""), neuper@37950: Calc ("RootEq.is'_sqrtTerm'_in",eval_is_sqrtTerm_in ""), neuper@37950: Calc ("RootEq.is'_rootTerm'_in",eval_is_rootTerm_in ""), neuper@37950: Calc ("RootEq.is'_normSqrtTerm'_in",eval_is_normSqrtTerm_in ""), neuper@37950: Calc ("op =",eval_equal "#equal_"), neuper@37969: Thm ("not_true",num_str @{thm not_true}), neuper@37969: Thm ("not_false",num_str @{thm not_false}), neuper@37969: Thm ("and_true",num_str @{thm and_true}), neuper@37969: Thm ("and_false",num_str @{thm and_false}), neuper@37969: Thm ("or_true",num_str @{thm or_true}), neuper@37969: Thm ("or_false",num_str @{thm or_false}) neuper@37950: ]; neuper@37950: neuper@37950: val RootEq_erls = neuper@37950: append_rls "RootEq_erls" Root_erls neuper@37965: [Thm ("divide_divide_eq_left",num_str @{thm divide_divide_eq_left}) neuper@37950: ]; neuper@37950: neuper@37950: val RootEq_crls = neuper@37950: append_rls "RootEq_crls" Root_crls neuper@37965: [Thm ("divide_divide_eq_left",num_str @{thm divide_divide_eq_left}) neuper@37950: ]; neuper@37950: neuper@37950: val rooteq_srls = neuper@37950: append_rls "rooteq_srls" e_rls neuper@37950: [Calc ("RootEq.is'_sqrtTerm'_in",eval_is_sqrtTerm_in ""), neuper@37950: Calc ("RootEq.is'_normSqrtTerm'_in",eval_is_normSqrtTerm_in""), neuper@37950: Calc ("RootEq.is'_rootTerm'_in",eval_is_rootTerm_in "") neuper@37950: ]; neuper@37950: neuper@37967: ruleset' := overwritelthy @{theory} (!ruleset', neuper@37950: [("RootEq_erls",RootEq_erls), neuper@37950: (*FIXXXME:del with rls.rls'*) neuper@37950: ("rooteq_srls",rooteq_srls) neuper@37950: ]); neuper@37950: neuper@37950: (*isolate the bound variable in an sqrt equation; 'bdv' is a meta-constant*) neuper@37950: val sqrt_isolate = prep_rls( neuper@37950: Rls {id = "sqrt_isolate", preconds = [], rew_ord = ("termlessI",termlessI), neuper@37950: erls = RootEq_erls, srls = Erls, calc = [], neuper@37950: rules = [ neuper@37969: Thm("sqrt_square_1",num_str @{thm sqrt_square_1}), neuper@37950: (* (sqrt a)^^^2 -> a *) neuper@37969: Thm("sqrt_square_2",num_str @{thm sqrt_square_2}), neuper@37950: (* sqrt (a^^^2) -> a *) neuper@37969: Thm("sqrt_times_root_1",num_str @{thm sqrt_times_root_1}), neuper@37950: (* sqrt a sqrt b -> sqrt(ab) *) neuper@37969: Thm("sqrt_times_root_2",num_str @{thm sqrt_times_root_2}), neuper@37950: (* a sqrt b sqrt c -> a sqrt(bc) *) neuper@37950: Thm("sqrt_square_equation_both_1", neuper@37969: num_str @{thm sqrt_square_equation_both_1}), neuper@37950: (* (sqrt a + sqrt b = sqrt c + sqrt d) -> neuper@37950: (a+2*sqrt(a)*sqrt(b)+b) = c+2*sqrt(c)*sqrt(d)+d) *) neuper@37950: Thm("sqrt_square_equation_both_2", neuper@37969: num_str @{thm sqrt_square_equation_both_2}), neuper@37950: (* (sqrt a - sqrt b = sqrt c + sqrt d) -> neuper@37950: (a-2*sqrt(a)*sqrt(b)+b) = c+2*sqrt(c)*sqrt(d)+d) *) neuper@37950: Thm("sqrt_square_equation_both_3", neuper@37969: num_str @{thm sqrt_square_equation_both_3}), neuper@37950: (* (sqrt a + sqrt b = sqrt c - sqrt d) -> neuper@37950: (a+2*sqrt(a)*sqrt(b)+b) = c-2*sqrt(c)*sqrt(d)+d) *) neuper@37950: Thm("sqrt_square_equation_both_4", neuper@37969: num_str @{thm sqrt_square_equation_both_4}), neuper@37950: (* (sqrt a - sqrt b = sqrt c - sqrt d) -> neuper@37950: (a-2*sqrt(a)*sqrt(b)+b) = c-2*sqrt(c)*sqrt(d)+d) *) neuper@37950: Thm("sqrt_isolate_l_add1", neuper@37969: num_str @{thm sqrt_isolate_l_add1}), neuper@37950: (* a+b*sqrt(x)=d -> b*sqrt(x) = d-a *) neuper@37950: Thm("sqrt_isolate_l_add2", neuper@37969: num_str @{thm sqrt_isolate_l_add2}), neuper@37950: (* a+ sqrt(x)=d -> sqrt(x) = d-a *) neuper@37950: Thm("sqrt_isolate_l_add3", neuper@37969: num_str @{thm sqrt_isolate_l_add3}), neuper@37950: (* a+b*c/sqrt(x)=d->b*c/sqrt(x)=d-a *) neuper@37950: Thm("sqrt_isolate_l_add4", neuper@37969: num_str @{thm sqrt_isolate_l_add4}), neuper@37950: (* a+c/sqrt(x)=d -> c/sqrt(x) = d-a *) neuper@37950: Thm("sqrt_isolate_l_add5", neuper@37969: num_str @{thm sqrt_isolate_l_add5}), neuper@37950: (* a+b*c/f*sqrt(x)=d->b*c/f*sqrt(x)=d-a *) neuper@37950: Thm("sqrt_isolate_l_add6", neuper@37969: num_str @{thm sqrt_isolate_l_add6}), neuper@37950: (* a+c/f*sqrt(x)=d -> c/f*sqrt(x) = d-a *) neuper@37969: (*Thm("sqrt_isolate_l_div",num_str @{thm sqrt_isolate_l_div}),*) neuper@37950: (* b*sqrt(x) = d sqrt(x) d/b *) neuper@37950: Thm("sqrt_isolate_r_add1", neuper@37969: num_str @{thm sqrt_isolate_r_add1}), neuper@37950: (* a= d+e*sqrt(x) -> a-d=e*sqrt(x) *) neuper@37950: Thm("sqrt_isolate_r_add2", neuper@37969: num_str @{thm sqrt_isolate_r_add2}), neuper@37950: (* a= d+ sqrt(x) -> a-d= sqrt(x) *) neuper@37950: Thm("sqrt_isolate_r_add3", neuper@37969: num_str @{thm sqrt_isolate_r_add3}), neuper@37950: (* a=d+e*g/sqrt(x)->a-d=e*g/sqrt(x)*) neuper@37950: Thm("sqrt_isolate_r_add4", neuper@37969: num_str @{thm sqrt_isolate_r_add4}), neuper@37950: (* a= d+g/sqrt(x) -> a-d=g/sqrt(x) *) neuper@37950: Thm("sqrt_isolate_r_add5", neuper@37969: num_str @{thm sqrt_isolate_r_add5}), neuper@37950: (* a=d+e*g/h*sqrt(x)->a-d=e*g/h*sqrt(x)*) neuper@37950: Thm("sqrt_isolate_r_add6", neuper@37969: num_str @{thm sqrt_isolate_r_add6}), neuper@37950: (* a= d+g/h*sqrt(x) -> a-d=g/h*sqrt(x) *) neuper@37969: (*Thm("sqrt_isolate_r_div",num_str @{thm sqrt_isolate_r_div}),*) neuper@37950: (* a=e*sqrt(x) -> a/e = sqrt(x) *) neuper@37950: Thm("sqrt_square_equation_left_1", neuper@37969: num_str @{thm sqrt_square_equation_left_1}), neuper@37950: (* sqrt(x)=b -> x=b^2 *) neuper@37950: Thm("sqrt_square_equation_left_2", neuper@37969: num_str @{thm sqrt_square_equation_left_2}), neuper@37950: (* c*sqrt(x)=b -> c^2*x=b^2 *) neuper@37969: Thm("sqrt_square_equation_left_3",num_str @{thm sqrt_square_equation_left_3}), neuper@37950: (* c/sqrt(x)=b -> c^2/x=b^2 *) neuper@37969: Thm("sqrt_square_equation_left_4",num_str @{thm sqrt_square_equation_left_4}), neuper@37950: (* c*d/sqrt(x)=b -> c^2*d^2/x=b^2 *) neuper@37969: Thm("sqrt_square_equation_left_5",num_str @{thm sqrt_square_equation_left_5}), neuper@37950: (* c/d*sqrt(x)=b -> c^2/d^2x=b^2 *) neuper@37969: Thm("sqrt_square_equation_left_6",num_str @{thm sqrt_square_equation_left_6}), neuper@37950: (* c*d/g*sqrt(x)=b -> c^2*d^2/g^2x=b^2 *) neuper@37969: Thm("sqrt_square_equation_right_1",num_str @{thm sqrt_square_equation_right_1}), neuper@37950: (* a=sqrt(x) ->a^2=x *) neuper@37969: Thm("sqrt_square_equation_right_2",num_str @{thm sqrt_square_equation_right_2}), neuper@37950: (* a=c*sqrt(x) ->a^2=c^2*x *) neuper@37969: Thm("sqrt_square_equation_right_3",num_str @{thm sqrt_square_equation_right_3}), neuper@37950: (* a=c/sqrt(x) ->a^2=c^2/x *) neuper@37969: Thm("sqrt_square_equation_right_4",num_str @{thm sqrt_square_equation_right_4}), neuper@37950: (* a=c*d/sqrt(x) ->a^2=c^2*d^2/x *) neuper@37969: Thm("sqrt_square_equation_right_5",num_str @{thm sqrt_square_equation_right_5}), neuper@37950: (* a=c/e*sqrt(x) ->a^2=c^2/e^2x *) neuper@37969: Thm("sqrt_square_equation_right_6",num_str @{thm sqrt_square_equation_right_6}) neuper@37950: (* a=c*d/g*sqrt(x) ->a^2=c^2*d^2/g^2*x *) neuper@37950: ],scr = Script ((term_of o the o (parse thy)) "empty_script") neuper@37950: }:rls); neuper@37950: neuper@37967: ruleset' := overwritelthy @{theory} (!ruleset', neuper@37950: [("sqrt_isolate",sqrt_isolate) neuper@37950: ]); neuper@37950: (* -- left 28.08.02--*) neuper@37950: (*isolate the bound variable in an sqrt left equation; 'bdv' is a meta-constant*) neuper@37950: val l_sqrt_isolate = prep_rls( neuper@37950: Rls {id = "l_sqrt_isolate", preconds = [], neuper@37950: rew_ord = ("termlessI",termlessI), neuper@37950: erls = RootEq_erls, srls = Erls, calc = [], neuper@37950: rules = [ neuper@37969: Thm("sqrt_square_1",num_str @{thm sqrt_square_1}), neuper@37950: (* (sqrt a)^^^2 -> a *) neuper@37969: Thm("sqrt_square_2",num_str @{thm sqrt_square_2}), neuper@37950: (* sqrt (a^^^2) -> a *) neuper@37969: Thm("sqrt_times_root_1",num_str @{thm sqrt_times_root_1}), neuper@37950: (* sqrt a sqrt b -> sqrt(ab) *) neuper@37969: Thm("sqrt_times_root_2",num_str @{thm sqrt_times_root_2}), neuper@37950: (* a sqrt b sqrt c -> a sqrt(bc) *) neuper@37969: Thm("sqrt_isolate_l_add1",num_str @{thm sqrt_isolate_l_add1}), neuper@37950: (* a+b*sqrt(x)=d -> b*sqrt(x) = d-a *) neuper@37969: Thm("sqrt_isolate_l_add2",num_str @{thm sqrt_isolate_l_add2}), neuper@37950: (* a+ sqrt(x)=d -> sqrt(x) = d-a *) neuper@37969: Thm("sqrt_isolate_l_add3",num_str @{thm sqrt_isolate_l_add3}), neuper@37950: (* a+b*c/sqrt(x)=d->b*c/sqrt(x)=d-a *) neuper@37969: Thm("sqrt_isolate_l_add4",num_str @{thm sqrt_isolate_l_add4}), neuper@37950: (* a+c/sqrt(x)=d -> c/sqrt(x) = d-a *) neuper@37969: Thm("sqrt_isolate_l_add5",num_str @{thm sqrt_isolate_l_add5}), neuper@37950: (* a+b*c/f*sqrt(x)=d->b*c/f*sqrt(x)=d-a *) neuper@37969: Thm("sqrt_isolate_l_add6",num_str @{thm sqrt_isolate_l_add6}), neuper@37950: (* a+c/f*sqrt(x)=d -> c/f*sqrt(x) = d-a *) neuper@37969: (*Thm("sqrt_isolate_l_div",num_str @{thm sqrt_isolate_l_div}),*) neuper@37950: (* b*sqrt(x) = d sqrt(x) d/b *) neuper@37969: Thm("sqrt_square_equation_left_1",num_str @{thm sqrt_square_equation_left_1}), neuper@37950: (* sqrt(x)=b -> x=b^2 *) neuper@37969: Thm("sqrt_square_equation_left_2",num_str @{thm sqrt_square_equation_left_2}), neuper@37950: (* a*sqrt(x)=b -> a^2*x=b^2*) neuper@37969: Thm("sqrt_square_equation_left_3",num_str @{thm sqrt_square_equation_left_3}), neuper@37950: (* c/sqrt(x)=b -> c^2/x=b^2 *) neuper@37969: Thm("sqrt_square_equation_left_4",num_str @{thm sqrt_square_equation_left_4}), neuper@37950: (* c*d/sqrt(x)=b -> c^2*d^2/x=b^2 *) neuper@37969: Thm("sqrt_square_equation_left_5",num_str @{thm sqrt_square_equation_left_5}), neuper@37950: (* c/d*sqrt(x)=b -> c^2/d^2x=b^2 *) neuper@37969: Thm("sqrt_square_equation_left_6",num_str @{thm sqrt_square_equation_left_6}) neuper@37950: (* c*d/g*sqrt(x)=b -> c^2*d^2/g^2x=b^2 *) neuper@37950: ], neuper@37950: scr = Script ((term_of o the o (parse thy)) "empty_script") neuper@37950: }:rls); neuper@37950: neuper@37967: ruleset' := overwritelthy @{theory} (!ruleset', neuper@37950: [("l_sqrt_isolate",l_sqrt_isolate) neuper@37950: ]); neuper@37950: neuper@37950: (* -- right 28.8.02--*) neuper@37950: (*isolate the bound variable in an sqrt right equation; 'bdv' is a meta-constant*) neuper@37950: val r_sqrt_isolate = prep_rls( neuper@37950: Rls {id = "r_sqrt_isolate", preconds = [], neuper@37950: rew_ord = ("termlessI",termlessI), neuper@37950: erls = RootEq_erls, srls = Erls, calc = [], neuper@37950: rules = [ neuper@37969: Thm("sqrt_square_1",num_str @{thm sqrt_square_1}), neuper@37950: (* (sqrt a)^^^2 -> a *) neuper@37969: Thm("sqrt_square_2",num_str @{thm sqrt_square_2}), neuper@37950: (* sqrt (a^^^2) -> a *) neuper@37969: Thm("sqrt_times_root_1",num_str @{thm sqrt_times_root_1}), neuper@37950: (* sqrt a sqrt b -> sqrt(ab) *) neuper@37969: Thm("sqrt_times_root_2",num_str @{thm sqrt_times_root_2}), neuper@37950: (* a sqrt b sqrt c -> a sqrt(bc) *) neuper@37969: Thm("sqrt_isolate_r_add1",num_str @{thm sqrt_isolate_r_add1}), neuper@37950: (* a= d+e*sqrt(x) -> a-d=e*sqrt(x) *) neuper@37969: Thm("sqrt_isolate_r_add2",num_str @{thm sqrt_isolate_r_add2}), neuper@37950: (* a= d+ sqrt(x) -> a-d= sqrt(x) *) neuper@37969: Thm("sqrt_isolate_r_add3",num_str @{thm sqrt_isolate_r_add3}), neuper@37950: (* a=d+e*g/sqrt(x)->a-d=e*g/sqrt(x)*) neuper@37969: Thm("sqrt_isolate_r_add4",num_str @{thm sqrt_isolate_r_add4}), neuper@37950: (* a= d+g/sqrt(x) -> a-d=g/sqrt(x) *) neuper@37969: Thm("sqrt_isolate_r_add5",num_str @{thm sqrt_isolate_r_add5}), neuper@37950: (* a=d+e*g/h*sqrt(x)->a-d=e*g/h*sqrt(x)*) neuper@37969: Thm("sqrt_isolate_r_add6",num_str @{thm sqrt_isolate_r_add6}), neuper@37950: (* a= d+g/h*sqrt(x) -> a-d=g/h*sqrt(x) *) neuper@37969: (*Thm("sqrt_isolate_r_div",num_str @{thm sqrt_isolate_r_div}),*) neuper@37950: (* a=e*sqrt(x) -> a/e = sqrt(x) *) neuper@37969: Thm("sqrt_square_equation_right_1",num_str @{thm sqrt_square_equation_right_1}), neuper@37950: (* a=sqrt(x) ->a^2=x *) neuper@37969: Thm("sqrt_square_equation_right_2",num_str @{thm sqrt_square_equation_right_2}), neuper@37950: (* a=c*sqrt(x) ->a^2=c^2*x *) neuper@37969: Thm("sqrt_square_equation_right_3",num_str @{thm sqrt_square_equation_right_3}), neuper@37950: (* a=c/sqrt(x) ->a^2=c^2/x *) neuper@37969: Thm("sqrt_square_equation_right_4",num_str @{thm sqrt_square_equation_right_4}), neuper@37950: (* a=c*d/sqrt(x) ->a^2=c^2*d^2/x *) neuper@37969: Thm("sqrt_square_equation_right_5",num_str @{thm sqrt_square_equation_right_5}), neuper@37950: (* a=c/e*sqrt(x) ->a^2=c^2/e^2x *) neuper@37969: Thm("sqrt_square_equation_right_6",num_str @{thm sqrt_square_equation_right_6}) neuper@37950: (* a=c*d/g*sqrt(x) ->a^2=c^2*d^2/g^2*x *) neuper@37950: ], neuper@37950: scr = Script ((term_of o the o (parse thy)) "empty_script") neuper@37950: }:rls); neuper@37950: neuper@37967: ruleset' := overwritelthy @{theory} (!ruleset', neuper@37950: [("r_sqrt_isolate",r_sqrt_isolate) neuper@37950: ]); neuper@37950: neuper@37950: val rooteq_simplify = prep_rls( neuper@37950: Rls {id = "rooteq_simplify", neuper@37950: preconds = [], rew_ord = ("termlessI",termlessI), neuper@37950: erls = RootEq_erls, srls = Erls, calc = [], neuper@37950: (*asm_thm = [("sqrt_square_1","")],*) neuper@37969: rules = [Thm ("real_assoc_1",num_str @{thm real_assoc_1}), neuper@37950: (* a+(b+c) = a+b+c *) neuper@37969: Thm ("real_assoc_2",num_str @{thm real_assoc_2}), neuper@37950: (* a*(b*c) = a*b*c *) neuper@38014: Calc ("Groups.plus_class.plus",eval_binop "#add_"), neuper@38014: Calc ("Groups.minus_class.minus",eval_binop "#sub_"), neuper@37950: Calc ("op *",eval_binop "#mult_"), neuper@38014: Calc ("Rings.inverse_class.divide", eval_cancel "#divide_e"), neuper@37982: Calc ("NthRoot.sqrt",eval_sqrt "#sqrt_"), neuper@37950: Calc ("Atools.pow" ,eval_binop "#power_"), neuper@37969: Thm("real_plus_binom_pow2",num_str @{thm real_plus_binom_pow2}), neuper@37969: Thm("real_minus_binom_pow2",num_str @{thm real_minus_binom_pow2}), neuper@37969: Thm("realpow_mul",num_str @{thm realpow_mul}), neuper@37950: (* (a * b)^n = a^n * b^n*) neuper@37969: Thm("sqrt_times_root_1",num_str @{thm sqrt_times_root_1}), neuper@37950: (* sqrt b * sqrt c = sqrt(b*c) *) neuper@37969: Thm("sqrt_times_root_2",num_str @{thm sqrt_times_root_2}), neuper@37950: (* a * sqrt a * sqrt b = a * sqrt(a*b) *) neuper@37969: Thm("sqrt_square_2",num_str @{thm sqrt_square_2}), neuper@37950: (* sqrt (a^^^2) = a *) neuper@37969: Thm("sqrt_square_1",num_str @{thm sqrt_square_1}) neuper@37950: (* sqrt a ^^^ 2 = a *) neuper@37950: ], neuper@37950: scr = Script ((term_of o the o (parse thy)) "empty_script") neuper@37950: }:rls); neuper@37967: ruleset' := overwritelthy @{theory} (!ruleset', neuper@37950: [("rooteq_simplify",rooteq_simplify) neuper@37950: ]); neuper@37950: neuper@37950: (*-------------------------Problem-----------------------*) neuper@37950: (* neuper@37986: (get_pbt ["root'","univariate","equation"]); neuper@37950: show_ptyps(); neuper@37950: *) neuper@37950: (* ---------root----------- *) neuper@37950: store_pbt neuper@37972: (prep_pbt thy "pbl_equ_univ_root" [] e_pblID neuper@37986: (["root'","univariate","equation"], neuper@37981: [("#Given" ,["equality e_e","solveFor v_v"]), neuper@37982: ("#Where" ,["(lhs e_e) is_rootTerm_in (v_v::real) | " ^ neuper@37982: "(rhs e_e) is_rootTerm_in (v_v::real)"]), neuper@38012: ("#Find" ,["solutions v_v'i'"]) neuper@37950: ], neuper@37981: RootEq_prls, SOME "solve (e_e::bool, v_v)", neuper@37950: [])); neuper@37950: (* ---------sqrt----------- *) neuper@37950: store_pbt neuper@37972: (prep_pbt thy "pbl_equ_univ_root_sq" [] e_pblID neuper@37986: (["sq","root'","univariate","equation"], neuper@37981: [("#Given" ,["equality e_e","solveFor v_v"]), neuper@37982: ("#Where" ,["( ((lhs e_e) is_sqrtTerm_in (v_v::real)) &" ^ neuper@37982: " ((lhs e_e) is_normSqrtTerm_in (v_v::real)) ) |" ^ neuper@37982: "( ((rhs e_e) is_sqrtTerm_in (v_v::real)) &" ^ neuper@37982: " ((rhs e_e) is_normSqrtTerm_in (v_v::real)) )"]), neuper@38012: ("#Find" ,["solutions v_v'i'"]) neuper@37950: ], neuper@37981: RootEq_prls, SOME "solve (e_e::bool, v_v)", neuper@37950: [["RootEq","solve_sq_root_equation"]])); neuper@37950: (* ---------normalize----------- *) neuper@37950: store_pbt neuper@37972: (prep_pbt thy "pbl_equ_univ_root_norm" [] e_pblID neuper@37986: (["normalize","root'","univariate","equation"], neuper@37981: [("#Given" ,["equality e_e","solveFor v_v"]), neuper@37982: ("#Where" ,["( ((lhs e_e) is_sqrtTerm_in (v_v::real)) &" ^ neuper@37982: " Not((lhs e_e) is_normSqrtTerm_in (v_v::real))) | " ^ neuper@37982: "( ((rhs e_e) is_sqrtTerm_in (v_v::real)) &" ^ neuper@37982: " Not((rhs e_e) is_normSqrtTerm_in (v_v::real)))"]), neuper@38012: ("#Find" ,["solutions v_v'i'"]) neuper@37950: ], neuper@37981: RootEq_prls, SOME "solve (e_e::bool, v_v)", neuper@37950: [["RootEq","norm_sq_root_equation"]])); neuper@37950: neuper@37950: (*-------------------------methods-----------------------*) neuper@37950: (* ---- root 20.8.02 ---*) neuper@37950: store_met neuper@37972: (prep_met thy "met_rooteq" [] e_metID neuper@37950: (["RootEq"], neuper@37950: [], neuper@37950: {rew_ord'="tless_true",rls'=Atools_erls,calc = [], srls = e_rls, prls=e_rls, neuper@37950: crls=RootEq_crls, nrls=norm_Poly(*, neuper@37950: asm_rls=[],asm_thm=[]*)}, "empty_script")); neuper@37985: neuper@37950: (*-- normalize 20.10.02 --*) neuper@37950: store_met neuper@37972: (prep_met thy "met_rooteq_norm" [] e_metID neuper@37950: (["RootEq","norm_sq_root_equation"], neuper@37981: [("#Given" ,["equality e_e","solveFor v_v"]), neuper@37982: ("#Where" ,["( ((lhs e_e) is_sqrtTerm_in (v_v::real)) &" ^ neuper@37982: " Not((lhs e_e) is_normSqrtTerm_in (v_v::real))) | " ^ neuper@37982: "( ((rhs e_e) is_sqrtTerm_in (v_v::real)) &" ^ neuper@37982: " Not((rhs e_e) is_normSqrtTerm_in (v_v::real)))"]), neuper@38012: ("#Find" ,["solutions v_v'i'"]) neuper@37950: ], neuper@37985: {rew_ord'="termlessI", rls'=RootEq_erls, srls=e_rls, prls=RootEq_prls, neuper@37985: calc=[], crls=RootEq_crls, nrls=norm_Poly}, neuper@37982: "Script Norm_sq_root_equation (e_e::bool) (v_v::real) = " ^ neuper@37981: "(let e_e = ((Repeat(Try (Rewrite makex1_x False))) @@ " ^ neuper@37950: " (Try (Repeat (Rewrite_Set expand_rootbinoms False))) @@ " ^ neuper@37950: " (Try (Rewrite_Set rooteq_simplify True)) @@ " ^ neuper@37950: " (Try (Repeat (Rewrite_Set make_rooteq False))) @@ " ^ neuper@37981: " (Try (Rewrite_Set rooteq_simplify True))) e_e " ^ neuper@37987: " in ((SubProblem (RootEq',[univariate,equation], " ^ neuper@37985: " [no_met]) [BOOL e_e, REAL v_v])))" neuper@37950: )); neuper@37950: neuper@37985: *} neuper@37985: neuper@37985: ML {* neuper@37985: val -------------------------------------------------- = "00000"; neuper@37950: store_met neuper@37972: (prep_met thy "met_rooteq_sq" [] e_metID neuper@37950: (["RootEq","solve_sq_root_equation"], neuper@37985: [("#Given" ,["equality e_e", "solveFor v_v"]), neuper@37985: ("#Where" ,["(((lhs e_e) is_sqrtTerm_in (v_v::real)) & " ^ neuper@37985: " ((lhs e_e) is_normSqrtTerm_in (v_v::real))) |" ^ neuper@37985: "(((rhs e_e) is_sqrtTerm_in (v_v::real)) & " ^ neuper@37985: " ((rhs e_e) is_normSqrtTerm_in (v_v::real)))"]), neuper@38012: ("#Find" ,["solutions v_v'i'"]) neuper@37950: ], neuper@37985: {rew_ord'="termlessI", rls'=RootEq_erls, srls = rooteq_srls, neuper@37985: prls = RootEq_prls, calc = [], crls=RootEq_crls, nrls=norm_Poly}, neuper@37985: "Script Solve_sq_root_equation (e_e::bool) (v_v::real) = " ^ neuper@37985: "(let e_e = " ^ neuper@37985: " ((Try (Rewrite_Set_Inst [(bdv,v_v::real)] sqrt_isolate True)) @@ " ^ neuper@37985: " (Try (Rewrite_Set rooteq_simplify True)) @@ " ^ neuper@37985: " (Try (Repeat (Rewrite_Set expand_rootbinoms False))) @@ " ^ neuper@37985: " (Try (Repeat (Rewrite_Set make_rooteq False))) @@ " ^ neuper@37985: " (Try (Rewrite_Set rooteq_simplify True)) ) e_e; " ^ neuper@37985: " (L_L::bool list) = " ^ neuper@37985: " (if (((lhs e_e) is_sqrtTerm_in v_v) | ((rhs e_e) is_sqrtTerm_in v_v))" ^ neuper@37987: " then (SubProblem (RootEq',[normalize,root',univariate,equation], " ^ neuper@37985: " [no_met]) [BOOL e_e, REAL v_v]) " ^ neuper@37987: " else (SubProblem (RootEq',[univariate,equation], [no_met]) " ^ neuper@37985: " [BOOL e_e, REAL v_v])) " ^ neuper@37991: "in Check_elementwise L_LL {(v_v::real). Assumptions})" neuper@37950: )); neuper@37985: *} neuper@37950: neuper@37985: ML {* neuper@37950: (*-- right 28.08.02 --*) neuper@37950: store_met neuper@37972: (prep_met thy "met_rooteq_sq_right" [] e_metID neuper@37950: (["RootEq","solve_right_sq_root_equation"], neuper@37981: [("#Given" ,["equality e_e","solveFor v_v"]), neuper@37981: ("#Where" ,["(rhs e_e) is_sqrtTerm_in v_v"]), neuper@38012: ("#Find" ,["solutions v_v'i'"]) neuper@37950: ], neuper@37985: {rew_ord' = "termlessI", rls' = RootEq_erls, srls = e_rls, neuper@37985: prls = RootEq_prls, calc = [], crls = RootEq_crls, nrls = norm_Poly}, neuper@37985: "Script Solve_right_sq_root_equation (e_e::bool) (v_v::real) = " ^ neuper@37985: "(let e_e = " ^ neuper@37985: " ((Try (Rewrite_Set_Inst [(bdv,v_v::real)] r_sqrt_isolate False)) @@ " ^ neuper@37985: " (Try (Rewrite_Set rooteq_simplify False)) @@ " ^ neuper@37985: " (Try (Repeat (Rewrite_Set expand_rootbinoms False))) @@ " ^ neuper@37985: " (Try (Repeat (Rewrite_Set make_rooteq False))) @@ " ^ neuper@37981: " (Try (Rewrite_Set rooteq_simplify False))) e_e " ^ neuper@37985: " in if ((rhs e_e) is_sqrtTerm_in v_v) " ^ neuper@37987: " then (SubProblem (RootEq',[normalize,root',univariate,equation], " ^ neuper@37985: " [no_met]) [BOOL e_e, REAL v_v]) " ^ neuper@37987: " else ((SubProblem (RootEq',[univariate,equation], " ^ neuper@37985: " [no_met]) [BOOL e_e, REAL v_v])))" neuper@37950: )); neuper@37985: val --------------------------------------------------+++ = "33333"; neuper@37950: neuper@37950: (*-- left 28.08.02 --*) neuper@37950: store_met neuper@37972: (prep_met thy "met_rooteq_sq_left" [] e_metID neuper@37950: (["RootEq","solve_left_sq_root_equation"], neuper@37981: [("#Given" ,["equality e_e","solveFor v_v"]), neuper@37981: ("#Where" ,["(lhs e_e) is_sqrtTerm_in v_v"]), neuper@38012: ("#Find" ,["solutions v_v'i'"]) neuper@37950: ], neuper@37950: {rew_ord'="termlessI", neuper@37950: rls'=RootEq_erls, neuper@37950: srls=e_rls, neuper@37950: prls=RootEq_prls, neuper@37950: calc=[], neuper@37950: crls=RootEq_crls, nrls=norm_Poly}, neuper@37982: "Script Solve_left_sq_root_equation (e_e::bool) (v_v::real) = " ^ neuper@37981: "(let e_e = " ^ neuper@37985: " ((Try (Rewrite_Set_Inst [(bdv,v_v::real)] l_sqrt_isolate False)) @@ " ^ neuper@37950: " (Try (Rewrite_Set rooteq_simplify False)) @@ " ^ neuper@37950: " (Try (Repeat (Rewrite_Set expand_rootbinoms False))) @@ " ^ neuper@37950: " (Try (Repeat (Rewrite_Set make_rooteq False))) @@ " ^ neuper@37981: " (Try (Rewrite_Set rooteq_simplify False))) e_e " ^ neuper@37981: " in if ((lhs e_e) is_sqrtTerm_in v_v) " ^ neuper@37987: " then (SubProblem (RootEq',[normalize,root',univariate,equation], " ^ neuper@37985: " [no_met]) [BOOL e_e, REAL v_v]) " ^ neuper@37987: " else ((SubProblem (RootEq',[univariate,equation], " ^ neuper@37985: " [no_met]) [BOOL e_e, REAL v_v])))" neuper@37950: )); neuper@37985: val --------------------------------------------------++++ = "44444"; neuper@37950: neuper@37950: calclist':= overwritel (!calclist', neuper@37950: [("is_rootTerm_in", ("RootEq.is'_rootTerm'_in", neuper@37950: eval_is_rootTerm_in"")), neuper@37950: ("is_sqrtTerm_in", ("RootEq.is'_sqrtTerm'_in", neuper@37950: eval_is_sqrtTerm_in"")), neuper@37950: ("is_normSqrtTerm_in", ("RootEq.is_normSqrtTerm_in", neuper@37950: eval_is_normSqrtTerm_in"")) neuper@37950: ]);(*("", ("", "")),*) neuper@37950: *} neuper@37950: neuper@37906: end