diff -r a28b5fc129b7 -r 22235e4dbe5f src/Tools/isac/Knowledge/PolyEq.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Tools/isac/Knowledge/PolyEq.ML Wed Aug 25 16:20:07 2010 +0200 @@ -0,0 +1,1162 @@ +(*. (c) by Richard Lang, 2003 .*) +(* collecting all knowledge for PolynomialEquations + created by: rlang + date: 02.07 + changed by: rlang + last change by: rlang + date: 02.11.26 +*) + +(* use"Knowledge/PolyEq.ML"; + use"PolyEq.ML"; + + use"ROOT.ML"; + cd"IsacKnowledge"; + + remove_thy"PolyEq"; + use_thy"Knowledge/Isac"; + *) +"******* PolyEq.ML begin *******"; + +theory' := overwritel (!theory', [("PolyEq.thy",PolyEq.thy)]); +(*-------------------------functions---------------------*) +(* just for try +local + fun add0 l d d_ = if (d_+1) < d then add0 (str2term"0"::l) d (d_+1) else l; + fun poly2list_ (t as (Const ("op +",_) $ t1 $ (Const ("Atools.pow",_) $ v_ $ Free (d_,_)))) v l d = + if (v=v_) + then poly2list_ t1 v (((str2term("1")))::(add0 l d (int_of_str' d_))) (int_of_str' d_) + else t::(add0 l d 0) + | poly2list_ (t as (Const ("op +",_) $ t1 $ (Const ("op *",_) $ t11 $ + (Const ("Atools.pow",_) $ v_ $ Free (d_,_))))) v l d = + if (v=v_) + then poly2list_ t1 v (((t11))::(add0 l d (int_of_str' d_))) (int_of_str' d_) + else t::(add0 l d 0) + | poly2list_ (t as (Const ("op +",_) $ t1 $ (Free (v_ , _)) )) v l d = + if (v = (str2term v_)) + then poly2list_ t1 v (((str2term("1")))::(add0 l d 1 )) 1 + else t::(add0 l d 0) + | poly2list_ (t as (Const ("op +",_) $ t1 $ (Const ("op *",_) $ t11 $ (Free (v_,_)) ))) v l d = + if (v= (str2term v_)) + then poly2list_ t1 v ( (t11)::(add0 l d 1 )) 1 + else t::(add0 l d 0) + | poly2list_ (t as (Const ("op +",_) $ _ $ _))_ l d = t::(add0 l d 0) + | poly2list_ (t as (Free (_,_))) _ l d = t::(add0 l d 0) + | poly2list_ t _ l d = t::(add0 l d 0); + + fun poly2list t v = poly2list_ t v [] 0; + fun diffpolylist_ [] _ = [] + | diffpolylist_ (x::xs) d = (str2term (if term2str(x)="0" + then "0" + else term2str(x)^"*"^str_of_int(d)))::diffpolylist_ xs (d+1); + fun diffpolylist [] = [] + | diffpolylist (x::xs) = diffpolylist_ xs 1; + (* diffpolylist(poly2list (str2term "1+ x +3*x^^^3") (str2term "x"));*) +in + +end; +*) +(*-------------------------rulse-------------------------*) +val PolyEq_prls = (*3.10.02:just the following order due to subterm evaluation*) + append_rls "PolyEq_prls" e_rls + [Calc ("Atools.ident",eval_ident "#ident_"), + Calc ("Tools.matches",eval_matches ""), + Calc ("Tools.lhs" ,eval_lhs ""), + Calc ("Tools.rhs" ,eval_rhs ""), + Calc ("Poly.is'_expanded'_in",eval_is_expanded_in ""), + Calc ("Poly.is'_poly'_in",eval_is_poly_in ""), + Calc ("Poly.has'_degree'_in",eval_has_degree_in ""), + Calc ("Poly.is'_polyrat'_in",eval_is_polyrat_in ""), + (*Calc ("Atools.occurs'_in",eval_occurs_in ""), *) + (*Calc ("Atools.is'_const",eval_const "#is_const_"),*) + Calc ("op =",eval_equal "#equal_"), + Calc ("RootEq.is'_rootTerm'_in",eval_is_rootTerm_in ""), + Calc ("RatEq.is'_ratequation'_in",eval_is_ratequation_in ""), + Thm ("not_true",num_str not_true), + Thm ("not_false",num_str not_false), + Thm ("and_true",num_str and_true), + Thm ("and_false",num_str and_false), + Thm ("or_true",num_str or_true), + Thm ("or_false",num_str or_false) + ]; + +val PolyEq_erls = + merge_rls "PolyEq_erls" LinEq_erls + (append_rls "ops_preds" calculate_Rational + [Calc ("op =",eval_equal "#equal_"), + Thm ("plus_leq", num_str plus_leq), + Thm ("minus_leq", num_str minus_leq), + Thm ("rat_leq1", num_str rat_leq1), + Thm ("rat_leq2", num_str rat_leq2), + Thm ("rat_leq3", num_str rat_leq3) + ]); + +val PolyEq_crls = + merge_rls "PolyEq_crls" LinEq_crls + (append_rls "ops_preds" calculate_Rational + [Calc ("op =",eval_equal "#equal_"), + Thm ("plus_leq", num_str plus_leq), + Thm ("minus_leq", num_str minus_leq), + Thm ("rat_leq1", num_str rat_leq1), + Thm ("rat_leq2", num_str rat_leq2), + Thm ("rat_leq3", num_str rat_leq3) + ]); +(*------ +val PolyEq_erls = + merge_rls "PolyEq_erls" + (append_rls "" (Rls {(*asm_thm=[],*)calc=[], + erls= Rls {(*asm_thm=[],*)calc=[], + erls= Erls, + id="e_rls",preconds=[], + rew_ord=("dummy_ord",dummy_ord), + rules=[Thm ("", + num_str ), + Thm ("", + num_str ), + Thm ("", + num_str ) + ], + scr=EmptyScr,srls=Erls}, + id="e_rls",preconds=[],rew_ord=("dummy_ord", + dummy_ord), + rules=[],scr=EmptyScr,srls=Erls} + ) + ((#rules o rep_rls) LinEq_erls)) + (append_rls "ops_preds" calculate_Rational + [Calc ("op =",eval_equal "#equal_"), + Thm ("plus_leq", num_str plus_leq), + Thm ("minus_leq", num_str minus_leq), + Thm ("rat_leq1", num_str rat_leq1), + Thm ("rat_leq2", num_str rat_leq2), + Thm ("rat_leq3", num_str rat_leq3) + ]); +-----*) + + +val cancel_leading_coeff = prep_rls( + Rls {id = "cancel_leading_coeff", preconds = [], + rew_ord = ("e_rew_ord",e_rew_ord), + erls = PolyEq_erls, srls = Erls, calc = [], (*asm_thm = [],*) + rules = [Thm ("cancel_leading_coeff1",num_str cancel_leading_coeff1), + Thm ("cancel_leading_coeff2",num_str cancel_leading_coeff2), + Thm ("cancel_leading_coeff3",num_str cancel_leading_coeff3), + Thm ("cancel_leading_coeff4",num_str cancel_leading_coeff4), + Thm ("cancel_leading_coeff5",num_str cancel_leading_coeff5), + Thm ("cancel_leading_coeff6",num_str cancel_leading_coeff6), + Thm ("cancel_leading_coeff7",num_str cancel_leading_coeff7), + Thm ("cancel_leading_coeff8",num_str cancel_leading_coeff8), + Thm ("cancel_leading_coeff9",num_str cancel_leading_coeff9), + Thm ("cancel_leading_coeff10",num_str cancel_leading_coeff10), + Thm ("cancel_leading_coeff11",num_str cancel_leading_coeff11), + Thm ("cancel_leading_coeff12",num_str cancel_leading_coeff12), + Thm ("cancel_leading_coeff13",num_str cancel_leading_coeff13) + ], + scr = Script ((term_of o the o (parse thy)) + "empty_script") + }:rls); +val complete_square = prep_rls( + Rls {id = "complete_square", preconds = [], + rew_ord = ("e_rew_ord",e_rew_ord), + erls = PolyEq_erls, srls = Erls, calc = [], (*asm_thm = [],*) + rules = [Thm ("complete_square1",num_str complete_square1), + Thm ("complete_square2",num_str complete_square2), + Thm ("complete_square3",num_str complete_square3), + Thm ("complete_square4",num_str complete_square4), + Thm ("complete_square5",num_str complete_square5) + ], + scr = Script ((term_of o the o (parse thy)) + "empty_script") + }:rls); +ruleset' := overwritelthy thy (!ruleset', + [("cancel_leading_coeff",cancel_leading_coeff), + ("complete_square",complete_square), + ("PolyEq_erls",PolyEq_erls)(*FIXXXME:del with rls.rls'*) + ]); +val polyeq_simplify = prep_rls( + Rls {id = "polyeq_simplify", preconds = [], + rew_ord = ("termlessI",termlessI), + erls = PolyEq_erls, + srls = Erls, + calc = [], + (*asm_thm = [],*) + rules = [Thm ("real_assoc_1",num_str real_assoc_1), + Thm ("real_assoc_2",num_str real_assoc_2), + Thm ("real_diff_minus",num_str real_diff_minus), + Thm ("real_unari_minus",num_str real_unari_minus), + Thm ("realpow_multI",num_str realpow_multI), + Calc ("op +",eval_binop "#add_"), + Calc ("op -",eval_binop "#sub_"), + Calc ("op *",eval_binop "#mult_"), + Calc ("HOL.divide", eval_cancel "#divide_"), + Calc ("Root.sqrt",eval_sqrt "#sqrt_"), + Calc ("Atools.pow" ,eval_binop "#power_"), + Rls_ reduce_012 + ], + scr = Script ((term_of o the o (parse thy)) "empty_script") + }:rls); +ruleset' := overwritelthy thy (!ruleset', + [("polyeq_simplify",polyeq_simplify)]); + + +(* ------------- polySolve ------------------ *) +(* -- d0 -- *) +(*isolate the bound variable in an d0 equation; 'bdv' is a meta-constant*) +val d0_polyeq_simplify = prep_rls( + Rls {id = "d0_polyeq_simplify", preconds = [], + rew_ord = ("e_rew_ord",e_rew_ord), + erls = PolyEq_erls, + srls = Erls, + calc = [], + (*asm_thm = [],*) + rules = [Thm("d0_true",num_str d0_true), + Thm("d0_false",num_str d0_false) + ], + scr = Script ((term_of o the o (parse thy)) "empty_script") + }:rls); +(* -- d1 -- *) +(*isolate the bound variable in an d1 equation; 'bdv' is a meta-constant*) +val d1_polyeq_simplify = prep_rls( + Rls {id = "d1_polyeq_simplify", preconds = [], + rew_ord = ("e_rew_ord",e_rew_ord), + erls = PolyEq_erls, + srls = Erls, + calc = [], + (*asm_thm = [("d1_isolate_div","")],*) + rules = [ + Thm("d1_isolate_add1",num_str d1_isolate_add1), + (* a+bx=0 -> bx=-a *) + Thm("d1_isolate_add2",num_str d1_isolate_add2), + (* a+ x=0 -> x=-a *) + Thm("d1_isolate_div",num_str d1_isolate_div) + (* bx=c -> x=c/b *) + ], + scr = Script ((term_of o the o (parse thy)) "empty_script") + }:rls); +(* -- d2 -- *) +(*isolate the bound variable in an d2 equation with bdv only; 'bdv' is a meta-constant*) +val d2_polyeq_bdv_only_simplify = prep_rls( + Rls {id = "d2_polyeq_bdv_only_simplify", preconds = [], + rew_ord = ("e_rew_ord",e_rew_ord), + erls = PolyEq_erls, + srls = Erls, + calc = [], + (*asm_thm = [("d2_sqrt_equation1",""),("d2_sqrt_equation1_neg",""), + ("d2_isolate_div","")],*) + rules = [ + Thm("d2_prescind1",num_str d2_prescind1), (* ax+bx^2=0 -> x(a+bx)=0 *) + Thm("d2_prescind2",num_str d2_prescind2), (* ax+ x^2=0 -> x(a+ x)=0 *) + Thm("d2_prescind3",num_str d2_prescind3), (* x+bx^2=0 -> x(1+bx)=0 *) + Thm("d2_prescind4",num_str d2_prescind4), (* x+ x^2=0 -> x(1+ x)=0 *) + Thm("d2_sqrt_equation1",num_str d2_sqrt_equation1), (* x^2=c -> x=+-sqrt(c)*) + Thm("d2_sqrt_equation1_neg",num_str d2_sqrt_equation1_neg), (* [0 [] *) + Thm("d2_sqrt_equation2",num_str d2_sqrt_equation2), (* x^2=0 -> x=0 *) + Thm("d2_reduce_equation1",num_str d2_reduce_equation1),(* x(a+bx)=0 -> x=0 | a+bx=0*) + Thm("d2_reduce_equation2",num_str d2_reduce_equation2),(* x(a+ x)=0 -> x=0 | a+ x=0*) + Thm("d2_isolate_div",num_str d2_isolate_div) (* bx^2=c -> x^2=c/b*) + ], + scr = Script ((term_of o the o (parse thy)) "empty_script") + }:rls); +(*isolate the bound variable in an d2 equation with sqrt only; 'bdv' is a meta-constant*) +val d2_polyeq_sq_only_simplify = prep_rls( + Rls {id = "d2_polyeq_sq_only_simplify", preconds = [], + rew_ord = ("e_rew_ord",e_rew_ord), + erls = PolyEq_erls, + srls = Erls, + calc = [], + (*asm_thm = [("d2_sqrt_equation1",""),("d2_sqrt_equation1_neg",""), + ("d2_isolate_div","")],*) + rules = [ + Thm("d2_isolate_add1",num_str d2_isolate_add1), (* a+ bx^2=0 -> bx^2=(-1)a*) + Thm("d2_isolate_add2",num_str d2_isolate_add2), (* a+ x^2=0 -> x^2=(-1)a*) + Thm("d2_sqrt_equation2",num_str d2_sqrt_equation2), (* x^2=0 -> x=0 *) + Thm("d2_sqrt_equation1",num_str d2_sqrt_equation1), (* x^2=c -> x=+-sqrt(c)*) + Thm("d2_sqrt_equation1_neg",num_str d2_sqrt_equation1_neg),(* [c<0] x^2=c -> x=[] *) + Thm("d2_isolate_div",num_str d2_isolate_div) (* bx^2=c -> x^2=c/b*) + ], + scr = Script ((term_of o the o (parse thy)) "empty_script") + }:rls); +(*isolate the bound variable in an d2 equation with pqFormula; 'bdv' is a meta-constant*) +val d2_polyeq_pqFormula_simplify = prep_rls( + Rls {id = "d2_polyeq_pqFormula_simplify", preconds = [], + rew_ord = ("e_rew_ord",e_rew_ord), + erls = PolyEq_erls, + srls = Erls, + calc = [], + (*asm_thm = [("d2_pqformula1",""),("d2_pqformula2",""),("d2_pqformula3",""),("d2_pqformula4",""), + ("d2_pqformula5",""),("d2_pqformula6",""),("d2_pqformula7",""),("d2_pqformula8",""), + ("d2_pqformula9",""),("d2_pqformula10",""), + ("d2_pqformula1_neg",""),("d2_pqformula2_neg",""),("d2_pqformula3_neg",""), + ("d2_pqformula4_neg",""),("d2_pqformula9_neg",""),("d2_pqformula10_neg","")],*) + rules = [ + Thm("d2_pqformula1",num_str d2_pqformula1), (* q+px+ x^2=0 *) + Thm("d2_pqformula1_neg",num_str d2_pqformula1_neg), (* q+px+ x^2=0 *) + Thm("d2_pqformula2",num_str d2_pqformula2), (* q+px+1x^2=0 *) + Thm("d2_pqformula2_neg",num_str d2_pqformula2_neg), (* q+px+1x^2=0 *) + Thm("d2_pqformula3",num_str d2_pqformula3), (* q+ x+ x^2=0 *) + Thm("d2_pqformula3_neg",num_str d2_pqformula3_neg), (* q+ x+ x^2=0 *) + Thm("d2_pqformula4",num_str d2_pqformula4), (* q+ x+1x^2=0 *) + Thm("d2_pqformula4_neg",num_str d2_pqformula4_neg), (* q+ x+1x^2=0 *) + Thm("d2_pqformula5",num_str d2_pqformula5), (* qx+ x^2=0 *) + Thm("d2_pqformula6",num_str d2_pqformula6), (* qx+1x^2=0 *) + Thm("d2_pqformula7",num_str d2_pqformula7), (* x+ x^2=0 *) + Thm("d2_pqformula8",num_str d2_pqformula8), (* x+1x^2=0 *) + Thm("d2_pqformula9",num_str d2_pqformula9), (* q +1x^2=0 *) + Thm("d2_pqformula9_neg",num_str d2_pqformula9_neg), (* q +1x^2=0 *) + Thm("d2_pqformula10",num_str d2_pqformula10), (* q + x^2=0 *) + Thm("d2_pqformula10_neg",num_str d2_pqformula10_neg), (* q + x^2=0 *) + Thm("d2_sqrt_equation2",num_str d2_sqrt_equation2), (* x^2=0 *) + Thm("d2_sqrt_equation3",num_str d2_sqrt_equation3) (* 1x^2=0 *) + ], + scr = Script ((term_of o the o (parse thy)) "empty_script") + }:rls); +(*isolate the bound variable in an d2 equation with abcFormula; 'bdv' is a meta-constant*) +val d2_polyeq_abcFormula_simplify = prep_rls( + Rls {id = "d2_polyeq_abcFormula_simplify", preconds = [], + rew_ord = ("e_rew_ord",e_rew_ord), + erls = PolyEq_erls, + srls = Erls, + calc = [], + (*asm_thm = [("d2_abcformula1",""),("d2_abcformula2",""),("d2_abcformula3",""), + ("d2_abcformula4",""),("d2_abcformula5",""),("d2_abcformula6",""), + ("d2_abcformula7",""),("d2_abcformula8",""),("d2_abcformula9",""), + ("d2_abcformula10",""),("d2_abcformula1_neg",""),("d2_abcformula2_neg",""), + ("d2_abcformula3_neg",""),("d2_abcformula4_neg",""),("d2_abcformula5_neg",""), + ("d2_abcformula6_neg","")],*) + rules = [ + Thm("d2_abcformula1",num_str d2_abcformula1), (*c+bx+cx^2=0 *) + Thm("d2_abcformula1_neg",num_str d2_abcformula1_neg), (*c+bx+cx^2=0 *) + Thm("d2_abcformula2",num_str d2_abcformula2), (*c+ x+cx^2=0 *) + Thm("d2_abcformula2_neg",num_str d2_abcformula2_neg), (*c+ x+cx^2=0 *) + Thm("d2_abcformula3",num_str d2_abcformula3), (*c+bx+ x^2=0 *) + Thm("d2_abcformula3_neg",num_str d2_abcformula3_neg), (*c+bx+ x^2=0 *) + Thm("d2_abcformula4",num_str d2_abcformula4), (*c+ x+ x^2=0 *) + Thm("d2_abcformula4_neg",num_str d2_abcformula4_neg), (*c+ x+ x^2=0 *) + Thm("d2_abcformula5",num_str d2_abcformula5), (*c+ cx^2=0 *) + Thm("d2_abcformula5_neg",num_str d2_abcformula5_neg), (*c+ cx^2=0 *) + Thm("d2_abcformula6",num_str d2_abcformula6), (*c+ x^2=0 *) + Thm("d2_abcformula6_neg",num_str d2_abcformula6_neg), (*c+ x^2=0 *) + Thm("d2_abcformula7",num_str d2_abcformula7), (* bx+ax^2=0 *) + Thm("d2_abcformula8",num_str d2_abcformula8), (* bx+ x^2=0 *) + Thm("d2_abcformula9",num_str d2_abcformula9), (* x+ax^2=0 *) + Thm("d2_abcformula10",num_str d2_abcformula10), (* x+ x^2=0 *) + Thm("d2_sqrt_equation2",num_str d2_sqrt_equation2), (* x^2=0 *) + Thm("d2_sqrt_equation3",num_str d2_sqrt_equation3) (* bx^2=0 *) + ], + scr = Script ((term_of o the o (parse thy)) "empty_script") + }:rls); +(*isolate the bound variable in an d2 equation; 'bdv' is a meta-constant*) +val d2_polyeq_simplify = prep_rls( + Rls {id = "d2_polyeq_simplify", preconds = [], + rew_ord = ("e_rew_ord",e_rew_ord), + erls = PolyEq_erls, + srls = Erls, + calc = [], + (*asm_thm = [("d2_pqformula1",""),("d2_pqformula2",""),("d2_pqformula3",""),("d2_pqformula4",""), + ("d2_pqformula1_neg",""),("d2_pqformula2_neg",""),("d2_pqformula3_neg",""), + ("d2_pqformula4_neg",""), + ("d2_abcformula1",""),("d2_abcformula2",""),("d2_abcformula1_neg",""), + ("d2_abcformula2_neg",""), ("d2_sqrt_equation1",""), + ("d2_sqrt_equation1_neg",""),("d2_isolate_div","")],*) + rules = [ + Thm("d2_pqformula1",num_str d2_pqformula1), (* p+qx+ x^2=0 *) + Thm("d2_pqformula1_neg",num_str d2_pqformula1_neg), (* p+qx+ x^2=0 *) + Thm("d2_pqformula2",num_str d2_pqformula2), (* p+qx+1x^2=0 *) + Thm("d2_pqformula2_neg",num_str d2_pqformula2_neg), (* p+qx+1x^2=0 *) + Thm("d2_pqformula3",num_str d2_pqformula3), (* p+ x+ x^2=0 *) + Thm("d2_pqformula3_neg",num_str d2_pqformula3_neg), (* p+ x+ x^2=0 *) + Thm("d2_pqformula4",num_str d2_pqformula4), (* p+ x+1x^2=0 *) + Thm("d2_pqformula4_neg",num_str d2_pqformula4_neg), (* p+ x+1x^2=0 *) + Thm("d2_abcformula1",num_str d2_abcformula1), (* c+bx+cx^2=0 *) + Thm("d2_abcformula1_neg",num_str d2_abcformula1_neg), (* c+bx+cx^2=0 *) + Thm("d2_abcformula2",num_str d2_abcformula2), (* c+ x+cx^2=0 *) + Thm("d2_abcformula2_neg",num_str d2_abcformula2_neg), (* c+ x+cx^2=0 *) + Thm("d2_prescind1",num_str d2_prescind1), (* ax+bx^2=0 -> x(a+bx)=0 *) + Thm("d2_prescind2",num_str d2_prescind2), (* ax+ x^2=0 -> x(a+ x)=0 *) + Thm("d2_prescind3",num_str d2_prescind3), (* x+bx^2=0 -> x(1+bx)=0 *) + Thm("d2_prescind4",num_str d2_prescind4), (* x+ x^2=0 -> x(1+ x)=0 *) + Thm("d2_isolate_add1",num_str d2_isolate_add1), (* a+ bx^2=0 -> bx^2=(-1)a*) + Thm("d2_isolate_add2",num_str d2_isolate_add2), (* a+ x^2=0 -> x^2=(-1)a*) + Thm("d2_sqrt_equation1",num_str d2_sqrt_equation1), (* x^2=c -> x=+-sqrt(c)*) + Thm("d2_sqrt_equation1_neg",num_str d2_sqrt_equation1_neg),(* [c<0] x^2=c -> x=[]*) + Thm("d2_sqrt_equation2",num_str d2_sqrt_equation2), (* x^2=0 -> x=0 *) + Thm("d2_reduce_equation1",num_str d2_reduce_equation1),(* x(a+bx)=0 -> x=0 | a+bx=0*) + Thm("d2_reduce_equation2",num_str d2_reduce_equation2),(* x(a+ x)=0 -> x=0 | a+ x=0*) + Thm("d2_isolate_div",num_str d2_isolate_div) (* bx^2=c -> x^2=c/b*) + ], + scr = Script ((term_of o the o (parse thy)) "empty_script") + }:rls); +(* -- d3 -- *) +(*isolate the bound variable in an d3 equation; 'bdv' is a meta-constant*) +val d3_polyeq_simplify = prep_rls( + Rls {id = "d3_polyeq_simplify", preconds = [], + rew_ord = ("e_rew_ord",e_rew_ord), + erls = PolyEq_erls, + srls = Erls, + calc = [], + (*asm_thm = [("d3_isolate_div","")],*) + rules = [ + Thm("d3_reduce_equation1",num_str d3_reduce_equation1), + (*a*bdv + b*bdv^^^2 + c*bdv^^^3=0) = (bdv=0 | (a + b*bdv + c*bdv^^^2=0)*) + Thm("d3_reduce_equation2",num_str d3_reduce_equation2), + (* bdv + b*bdv^^^2 + c*bdv^^^3=0) = (bdv=0 | (1 + b*bdv + c*bdv^^^2=0)*) + Thm("d3_reduce_equation3",num_str d3_reduce_equation3), + (*a*bdv + bdv^^^2 + c*bdv^^^3=0) = (bdv=0 | (a + bdv + c*bdv^^^2=0)*) + Thm("d3_reduce_equation4",num_str d3_reduce_equation4), + (* bdv + bdv^^^2 + c*bdv^^^3=0) = (bdv=0 | (1 + bdv + c*bdv^^^2=0)*) + Thm("d3_reduce_equation5",num_str d3_reduce_equation5), + (*a*bdv + b*bdv^^^2 + bdv^^^3=0) = (bdv=0 | (a + b*bdv + bdv^^^2=0)*) + Thm("d3_reduce_equation6",num_str d3_reduce_equation6), + (* bdv + b*bdv^^^2 + bdv^^^3=0) = (bdv=0 | (1 + b*bdv + bdv^^^2=0)*) + Thm("d3_reduce_equation7",num_str d3_reduce_equation7), + (*a*bdv + bdv^^^2 + bdv^^^3=0) = (bdv=0 | (1 + bdv + bdv^^^2=0)*) + Thm("d3_reduce_equation8",num_str d3_reduce_equation8), + (* bdv + bdv^^^2 + bdv^^^3=0) = (bdv=0 | (1 + bdv + bdv^^^2=0)*) + Thm("d3_reduce_equation9",num_str d3_reduce_equation9), + (*a*bdv + c*bdv^^^3=0) = (bdv=0 | (a + c*bdv^^^2=0)*) + Thm("d3_reduce_equation10",num_str d3_reduce_equation10), + (* bdv + c*bdv^^^3=0) = (bdv=0 | (1 + c*bdv^^^2=0)*) + Thm("d3_reduce_equation11",num_str d3_reduce_equation11), + (*a*bdv + bdv^^^3=0) = (bdv=0 | (a + bdv^^^2=0)*) + Thm("d3_reduce_equation12",num_str d3_reduce_equation12), + (* bdv + bdv^^^3=0) = (bdv=0 | (1 + bdv^^^2=0)*) + Thm("d3_reduce_equation13",num_str d3_reduce_equation13), + (* b*bdv^^^2 + c*bdv^^^3=0) = (bdv=0 | ( b*bdv + c*bdv^^^2=0)*) + Thm("d3_reduce_equation14",num_str d3_reduce_equation14), + (* bdv^^^2 + c*bdv^^^3=0) = (bdv=0 | ( bdv + c*bdv^^^2=0)*) + Thm("d3_reduce_equation15",num_str d3_reduce_equation15), + (* b*bdv^^^2 + bdv^^^3=0) = (bdv=0 | ( b*bdv + bdv^^^2=0)*) + Thm("d3_reduce_equation16",num_str d3_reduce_equation16), + (* bdv^^^2 + bdv^^^3=0) = (bdv=0 | ( bdv + bdv^^^2=0)*) + Thm("d3_isolate_add1",num_str d3_isolate_add1), + (*[|Not(bdv occurs_in a)|] ==> (a + b*bdv^^^3=0) = (bdv=0 | (b*bdv^^^3=a)*) + Thm("d3_isolate_add2",num_str d3_isolate_add2), + (*[|Not(bdv occurs_in a)|] ==> (a + bdv^^^3=0) = (bdv=0 | ( bdv^^^3=a)*) + Thm("d3_isolate_div",num_str d3_isolate_div), + (*[|Not(b=0)|] ==> (b*bdv^^^3=c) = (bdv^^^3=c/b*) + Thm("d3_root_equation2",num_str d3_root_equation2), + (*(bdv^^^3=0) = (bdv=0) *) + Thm("d3_root_equation1",num_str d3_root_equation1) + (*bdv^^^3=c) = (bdv = nroot 3 c*) + ], + scr = Script ((term_of o the o (parse thy)) "empty_script") + }:rls); +(* -- d4 -- *) +(*isolate the bound variable in an d4 equation; 'bdv' is a meta-constant*) +val d4_polyeq_simplify = prep_rls( + Rls {id = "d4_polyeq_simplify", preconds = [], + rew_ord = ("e_rew_ord",e_rew_ord), + erls = PolyEq_erls, + srls = Erls, + calc = [], + (*asm_thm = [],*) + rules = [Thm("d4_sub_u1",num_str d4_sub_u1) + (* ax^4+bx^2+c=0 -> x=+-sqrt(ax^2+bx^+c) *) + ], + scr = Script ((term_of o the o (parse thy)) "empty_script") + }:rls); + +ruleset' := overwritelthy thy (!ruleset', + [("d0_polyeq_simplify", d0_polyeq_simplify), + ("d1_polyeq_simplify", d1_polyeq_simplify), + ("d2_polyeq_simplify", d2_polyeq_simplify), + ("d2_polyeq_bdv_only_simplify", d2_polyeq_bdv_only_simplify), + ("d2_polyeq_sq_only_simplify", d2_polyeq_sq_only_simplify), + ("d2_polyeq_pqFormula_simplify", d2_polyeq_pqFormula_simplify), + ("d2_polyeq_abcFormula_simplify", d2_polyeq_abcFormula_simplify), + ("d3_polyeq_simplify", d3_polyeq_simplify), + ("d4_polyeq_simplify", d4_polyeq_simplify) + ]); + +(*------------------------problems------------------------*) +(* +(get_pbt ["degree_2","polynomial","univariate","equation"]); +show_ptyps(); +*) + +(*-------------------------poly-----------------------*) +store_pbt + (prep_pbt PolyEq.thy "pbl_equ_univ_poly" [] e_pblID + (["polynomial","univariate","equation"], + [("#Given" ,["equality e_","solveFor v_"]), + ("#Where" ,["~((e_::bool) is_ratequation_in (v_::real))", + "~((lhs e_) is_rootTerm_in (v_::real))", + "~((rhs e_) is_rootTerm_in (v_::real))"]), + ("#Find" ,["solutions v_i_"]) + ], + PolyEq_prls, SOME "solve (e_::bool, v_)", + [])); +(*--- d0 ---*) +store_pbt + (prep_pbt PolyEq.thy "pbl_equ_univ_poly_deg0" [] e_pblID + (["degree_0","polynomial","univariate","equation"], + [("#Given" ,["equality e_","solveFor v_"]), + ("#Where" ,["matches (?a = 0) e_", + "(lhs e_) is_poly_in v_", + "((lhs e_) has_degree_in v_ ) = 0" + ]), + ("#Find" ,["solutions v_i_"]) + ], + PolyEq_prls, SOME "solve (e_::bool, v_)", + [["PolyEq","solve_d0_polyeq_equation"]])); + +(*--- d1 ---*) +store_pbt + (prep_pbt PolyEq.thy "pbl_equ_univ_poly_deg1" [] e_pblID + (["degree_1","polynomial","univariate","equation"], + [("#Given" ,["equality e_","solveFor v_"]), + ("#Where" ,["matches (?a = 0) e_", + "(lhs e_) is_poly_in v_", + "((lhs e_) has_degree_in v_ ) = 1" + ]), + ("#Find" ,["solutions v_i_"]) + ], + PolyEq_prls, SOME "solve (e_::bool, v_)", + [["PolyEq","solve_d1_polyeq_equation"]])); + +(*--- d2 ---*) +store_pbt + (prep_pbt PolyEq.thy "pbl_equ_univ_poly_deg2" [] e_pblID + (["degree_2","polynomial","univariate","equation"], + [("#Given" ,["equality e_","solveFor v_"]), + ("#Where" ,["matches (?a = 0) e_", + "(lhs e_) is_poly_in v_ ", + "((lhs e_) has_degree_in v_ ) = 2"]), + ("#Find" ,["solutions v_i_"]) + ], + PolyEq_prls, SOME "solve (e_::bool, v_)", + [["PolyEq","solve_d2_polyeq_equation"]])); + + store_pbt + (prep_pbt PolyEq.thy "pbl_equ_univ_poly_deg2_sqonly" [] e_pblID + (["sq_only","degree_2","polynomial","univariate","equation"], + [("#Given" ,["equality e_","solveFor v_"]), + ("#Where" ,["matches ( ?a + ?v_^^^2 = 0) e_ | \ + \matches ( ?a + ?b*?v_^^^2 = 0) e_ | \ + \matches ( ?v_^^^2 = 0) e_ | \ + \matches ( ?b*?v_^^^2 = 0) e_" , + "Not (matches (?a + ?v_ + ?v_^^^2 = 0) e_) &\ + \Not (matches (?a + ?b*?v_ + ?v_^^^2 = 0) e_) &\ + \Not (matches (?a + ?v_ + ?c*?v_^^^2 = 0) e_) &\ + \Not (matches (?a + ?b*?v_ + ?c*?v_^^^2 = 0) e_) &\ + \Not (matches ( ?v_ + ?v_^^^2 = 0) e_) &\ + \Not (matches ( ?b*?v_ + ?v_^^^2 = 0) e_) &\ + \Not (matches ( ?v_ + ?c*?v_^^^2 = 0) e_) &\ + \Not (matches ( ?b*?v_ + ?c*?v_^^^2 = 0) e_)"]), + ("#Find" ,["solutions v_i_"]) + ], + PolyEq_prls, SOME "solve (e_::bool, v_)", + [["PolyEq","solve_d2_polyeq_sqonly_equation"]])); + +store_pbt + (prep_pbt PolyEq.thy "pbl_equ_univ_poly_deg2_bdvonly" [] e_pblID + (["bdv_only","degree_2","polynomial","univariate","equation"], + [("#Given" ,["equality e_","solveFor v_"]), + ("#Where" ,["matches (?a*?v_ + ?v_^^^2 = 0) e_ | \ + \matches ( ?v_ + ?v_^^^2 = 0) e_ | \ + \matches ( ?v_ + ?b*?v_^^^2 = 0) e_ | \ + \matches (?a*?v_ + ?b*?v_^^^2 = 0) e_ | \ + \matches ( ?v_^^^2 = 0) e_ | \ + \matches ( ?b*?v_^^^2 = 0) e_ "]), + ("#Find" ,["solutions v_i_"]) + ], + PolyEq_prls, SOME "solve (e_::bool, v_)", + [["PolyEq","solve_d2_polyeq_bdvonly_equation"]])); + +store_pbt + (prep_pbt PolyEq.thy "pbl_equ_univ_poly_deg2_pq" [] e_pblID + (["pqFormula","degree_2","polynomial","univariate","equation"], + [("#Given" ,["equality e_","solveFor v_"]), + ("#Where" ,["matches (?a + 1*?v_^^^2 = 0) e_ | \ + \matches (?a + ?v_^^^2 = 0) e_"]), + ("#Find" ,["solutions v_i_"]) + ], + PolyEq_prls, SOME "solve (e_::bool, v_)", + [["PolyEq","solve_d2_polyeq_pq_equation"]])); + +store_pbt + (prep_pbt PolyEq.thy "pbl_equ_univ_poly_deg2_abc" [] e_pblID + (["abcFormula","degree_2","polynomial","univariate","equation"], + [("#Given" ,["equality e_","solveFor v_"]), + ("#Where" ,["matches (?a + ?v_^^^2 = 0) e_ | \ + \matches (?a + ?b*?v_^^^2 = 0) e_"]), + ("#Find" ,["solutions v_i_"]) + ], + PolyEq_prls, SOME "solve (e_::bool, v_)", + [["PolyEq","solve_d2_polyeq_abc_equation"]])); + +(*--- d3 ---*) +store_pbt + (prep_pbt PolyEq.thy "pbl_equ_univ_poly_deg3" [] e_pblID + (["degree_3","polynomial","univariate","equation"], + [("#Given" ,["equality e_","solveFor v_"]), + ("#Where" ,["matches (?a = 0) e_", + "(lhs e_) is_poly_in v_ ", + "((lhs e_) has_degree_in v_) = 3"]), + ("#Find" ,["solutions v_i_"]) + ], + PolyEq_prls, SOME "solve (e_::bool, v_)", + [["PolyEq","solve_d3_polyeq_equation"]])); + +(*--- d4 ---*) +store_pbt + (prep_pbt PolyEq.thy "pbl_equ_univ_poly_deg4" [] e_pblID + (["degree_4","polynomial","univariate","equation"], + [("#Given" ,["equality e_","solveFor v_"]), + ("#Where" ,["matches (?a = 0) e_", + "(lhs e_) is_poly_in v_ ", + "((lhs e_) has_degree_in v_) = 4"]), + ("#Find" ,["solutions v_i_"]) + ], + PolyEq_prls, SOME "solve (e_::bool, v_)", + [(*["PolyEq","solve_d4_polyeq_equation"]*)])); + +(*--- normalize ---*) +store_pbt + (prep_pbt PolyEq.thy "pbl_equ_univ_poly_norm" [] e_pblID + (["normalize","polynomial","univariate","equation"], + [("#Given" ,["equality e_","solveFor v_"]), + ("#Where" ,["(Not((matches (?a = 0 ) e_ ))) |\ + \(Not(((lhs e_) is_poly_in v_)))"]), + ("#Find" ,["solutions v_i_"]) + ], + PolyEq_prls, SOME "solve (e_::bool, v_)", + [["PolyEq","normalize_poly"]])); +(*-------------------------expanded-----------------------*) +store_pbt + (prep_pbt PolyEq.thy "pbl_equ_univ_expand" [] e_pblID + (["expanded","univariate","equation"], + [("#Given" ,["equality e_","solveFor v_"]), + ("#Where" ,["matches (?a = 0) e_", + "(lhs e_) is_expanded_in v_ "]), + ("#Find" ,["solutions v_i_"]) + ], + PolyEq_prls, SOME "solve (e_::bool, v_)", + [])); + +(*--- d2 ---*) +store_pbt + (prep_pbt PolyEq.thy "pbl_equ_univ_expand_deg2" [] e_pblID + (["degree_2","expanded","univariate","equation"], + [("#Given" ,["equality e_","solveFor v_"]), + ("#Where" ,["((lhs e_) has_degree_in v_) = 2"]), + ("#Find" ,["solutions v_i_"]) + ], + PolyEq_prls, SOME "solve (e_::bool, v_)", + [["PolyEq","complete_square"]])); + + +"-------------------------methods-----------------------"; +store_met + (prep_met PolyEq.thy "met_polyeq" [] e_metID + (["PolyEq"], + [], + {rew_ord'="tless_true",rls'=Atools_erls,calc = [], srls = e_rls, prls=e_rls, + crls=PolyEq_crls, nrls=norm_Rational + (*, asm_rls=[],asm_thm=[]*)}, "empty_script")); + +store_met + (prep_met PolyEq.thy "met_polyeq_norm" [] e_metID + (["PolyEq","normalize_poly"], + [("#Given" ,["equality e_","solveFor v_"]), + ("#Where" ,["(Not((matches (?a = 0 ) e_ ))) |\ + \(Not(((lhs e_) is_poly_in v_)))"]), + ("#Find" ,["solutions v_i_"]) + ], + {rew_ord'="termlessI", + rls'=PolyEq_erls, + srls=e_rls, + prls=PolyEq_prls, + calc=[], + crls=PolyEq_crls, nrls=norm_Rational(*, + asm_rls=[], + asm_thm=[]*)}, + (*RL: Ratpoly loest Brueche ohne bdv*) + "Script Normalize_poly (e_::bool) (v_::real) = \ + \(let e_ =((Try (Rewrite all_left False)) @@ \ + \ (Try (Repeat (Rewrite makex1_x False))) @@ \ + \ (Try (Repeat (Rewrite_Set expand_binoms False))) @@ \ + \ (Try (Repeat (Rewrite_Set_Inst [(bdv,v_::real)] \ + \ make_ratpoly_in False))) @@ \ + \ (Try (Repeat (Rewrite_Set polyeq_simplify False)))) e_ \ + \ in (SubProblem (PolyEq_,[polynomial,univariate,equation], \ + \ [no_met]) [bool_ e_, real_ v_]))" + )); + +store_met + (prep_met PolyEq.thy "met_polyeq_d0" [] e_metID + (["PolyEq","solve_d0_polyeq_equation"], + [("#Given" ,["equality e_","solveFor v_"]), + ("#Where" ,["(lhs e_) is_poly_in v_ ", + "((lhs e_) has_degree_in v_) = 0"]), + ("#Find" ,["solutions v_i_"]) + ], + {rew_ord'="termlessI", + rls'=PolyEq_erls, + srls=e_rls, + prls=PolyEq_prls, + calc=[("sqrt", ("Root.sqrt", eval_sqrt "#sqrt_"))], + crls=PolyEq_crls, nrls=norm_Rational(*, + asm_rls=[], + asm_thm=[]*)}, + "Script Solve_d0_polyeq_equation (e_::bool) (v_::real) = \ + \(let e_ = ((Try (Rewrite_Set_Inst [(bdv,v_::real)] \ + \ d0_polyeq_simplify False))) e_ \ + \ in ((Or_to_List e_)::bool list))" + )); + +store_met + (prep_met PolyEq.thy "met_polyeq_d1" [] e_metID + (["PolyEq","solve_d1_polyeq_equation"], + [("#Given" ,["equality e_","solveFor v_"]), + ("#Where" ,["(lhs e_) is_poly_in v_ ", + "((lhs e_) has_degree_in v_) = 1"]), + ("#Find" ,["solutions v_i_"]) + ], + {rew_ord'="termlessI", + rls'=PolyEq_erls, + srls=e_rls, + prls=PolyEq_prls, + calc=[("sqrt", ("Root.sqrt", eval_sqrt "#sqrt_"))], + crls=PolyEq_crls, nrls=norm_Rational(*, + (* asm_rls=["d1_polyeq_simplify"],*) + asm_rls=[], + asm_thm=[("d1_isolate_div","")]*)}, + "Script Solve_d1_polyeq_equation (e_::bool) (v_::real) = \ + \(let e_ = ((Try (Rewrite_Set_Inst [(bdv,v_::real)] \ + \ d1_polyeq_simplify True)) @@ \ + \ (Try (Rewrite_Set polyeq_simplify False)) @@ \ + \ (Try (Rewrite_Set norm_Rational_parenthesized False))) e_;\ + \ (L_::bool list) = ((Or_to_List e_)::bool list) \ + \ in Check_elementwise L_ {(v_::real). Assumptions} )" + )); + +store_met + (prep_met PolyEq.thy "met_polyeq_d22" [] e_metID + (["PolyEq","solve_d2_polyeq_equation"], + [("#Given" ,["equality e_","solveFor v_"]), + ("#Where" ,["(lhs e_) is_poly_in v_ ", + "((lhs e_) has_degree_in v_) = 2"]), + ("#Find" ,["solutions v_i_"]) + ], + {rew_ord'="termlessI", + rls'=PolyEq_erls, + srls=e_rls, + prls=PolyEq_prls, + calc=[("sqrt", ("Root.sqrt", eval_sqrt "#sqrt_"))], + crls=PolyEq_crls, nrls=norm_Rational(*, + (*asm_rls=["d2_polyeq_simplify","d1_polyeq_simplify"],*) + asm_rls=[], + asm_thm = [("d1_isolate_div",""),("d2_pqformula1",""),("d2_pqformula2",""), + ("d2_pqformula3",""),("d2_pqformula4",""),("d2_pqformula1_neg",""), + ("d2_pqformula2_neg",""),("d2_pqformula3_neg",""),("d2_pqformula4_neg",""), + ("d2_abcformula1",""),("d2_abcformula2",""),("d2_abcformula1_neg",""), + ("d2_abcformula2_neg",""), ("d2_sqrt_equation1",""), + ("d2_sqrt_equation1_neg",""), ("d2_isolate_div","")]*)}, + "Script Solve_d2_polyeq_equation (e_::bool) (v_::real) = \ + \ (let e_ = ((Try (Rewrite_Set_Inst [(bdv,v_::real)] \ + \ d2_polyeq_simplify True)) @@ \ + \ (Try (Rewrite_Set polyeq_simplify False)) @@ \ + \ (Try (Rewrite_Set_Inst [(bdv,v_::real)] \ + \ d1_polyeq_simplify True)) @@ \ + \ (Try (Rewrite_Set polyeq_simplify False)) @@ \ + \ (Try (Rewrite_Set norm_Rational_parenthesized False))) e_;\ + \ (L_::bool list) = ((Or_to_List e_)::bool list) \ + \ in Check_elementwise L_ {(v_::real). Assumptions} )" + )); + +store_met + (prep_met PolyEq.thy "met_polyeq_d2_bdvonly" [] e_metID + (["PolyEq","solve_d2_polyeq_bdvonly_equation"], + [("#Given" ,["equality e_","solveFor v_"]), + ("#Where" ,["(lhs e_) is_poly_in v_ ", + "((lhs e_) has_degree_in v_) = 2"]), + ("#Find" ,["solutions v_i_"]) + ], + {rew_ord'="termlessI", + rls'=PolyEq_erls, + srls=e_rls, + prls=PolyEq_prls, + calc=[("sqrt", ("Root.sqrt", eval_sqrt "#sqrt_"))], + crls=PolyEq_crls, nrls=norm_Rational(*, + (*asm_rls=["d2_polyeq_bdv_only_simplify","d1_polyeq_simplify "],*) + asm_rls=[], + asm_thm=[("d1_isolate_div",""),("d2_isolate_div",""), + ("d2_sqrt_equation1",""),("d2_sqrt_equation1_neg","")]*)}, + "Script Solve_d2_polyeq_bdvonly_equation (e_::bool) (v_::real) =\ + \ (let e_ = ((Try (Rewrite_Set_Inst [(bdv,v_::real)] \ + \ d2_polyeq_bdv_only_simplify True)) @@ \ + \ (Try (Rewrite_Set polyeq_simplify False)) @@ \ + \ (Try (Rewrite_Set_Inst [(bdv,v_::real)] \ + \ d1_polyeq_simplify True)) @@ \ + \ (Try (Rewrite_Set polyeq_simplify False)) @@ \ + \ (Try (Rewrite_Set norm_Rational_parenthesized False))) e_;\ + \ (L_::bool list) = ((Or_to_List e_)::bool list) \ + \ in Check_elementwise L_ {(v_::real). Assumptions} )" + )); + +store_met + (prep_met PolyEq.thy "met_polyeq_d2_sqonly" [] e_metID + (["PolyEq","solve_d2_polyeq_sqonly_equation"], + [("#Given" ,["equality e_","solveFor v_"]), + ("#Where" ,["(lhs e_) is_poly_in v_ ", + "((lhs e_) has_degree_in v_) = 2"]), + ("#Find" ,["solutions v_i_"]) + ], + {rew_ord'="termlessI", + rls'=PolyEq_erls, + srls=e_rls, + prls=PolyEq_prls, + calc=[("sqrt", ("Root.sqrt", eval_sqrt "#sqrt_"))], + crls=PolyEq_crls, nrls=norm_Rational(*, + (*asm_rls=["d2_polyeq_sq_only_simplify"],*) + asm_rls=[], + asm_thm=[("d2_sqrt_equation1",""),("d2_sqrt_equation1_neg",""), + ("d2_isolate_div","")]*)}, + "Script Solve_d2_polyeq_sqonly_equation (e_::bool) (v_::real) =\ + \ (let e_ = ((Try (Rewrite_Set_Inst [(bdv,v_::real)] \ + \ d2_polyeq_sq_only_simplify True)) @@ \ + \ (Try (Rewrite_Set polyeq_simplify False)) @@ \ + \ (Try (Rewrite_Set norm_Rational_parenthesized False))) e_; \ + \ (L_::bool list) = ((Or_to_List e_)::bool list) \ + \ in Check_elementwise L_ {(v_::real). Assumptions} )" + )); + +store_met + (prep_met PolyEq.thy "met_polyeq_d2_pq" [] e_metID + (["PolyEq","solve_d2_polyeq_pq_equation"], + [("#Given" ,["equality e_","solveFor v_"]), + ("#Where" ,["(lhs e_) is_poly_in v_ ", + "((lhs e_) has_degree_in v_) = 2"]), + ("#Find" ,["solutions v_i_"]) + ], + {rew_ord'="termlessI", + rls'=PolyEq_erls, + srls=e_rls, + prls=PolyEq_prls, + calc=[("sqrt", ("Root.sqrt", eval_sqrt "#sqrt_"))], + crls=PolyEq_crls, nrls=norm_Rational(*, + (*asm_rls=["d2_polyeq_pqFormula_simplify"],*) + asm_rls=[], + asm_thm=[("d2_pqformula1",""),("d2_pqformula2",""),("d2_pqformula3",""), + ("d2_pqformula4",""),("d2_pqformula5",""),("d2_pqformula6",""), + ("d2_pqformula7",""),("d2_pqformula8",""),("d2_pqformula9",""), + ("d2_pqformula10",""),("d2_pqformula1_neg",""),("d2_pqformula2_neg",""), + ("d2_pqformula3_neg",""), ("d2_pqformula4_neg",""),("d2_pqformula9_neg",""), + ("d2_pqformula10_neg","")]*)}, + "Script Solve_d2_polyeq_pq_equation (e_::bool) (v_::real) = \ + \ (let e_ = ((Try (Rewrite_Set_Inst [(bdv,v_::real)] \ + \ d2_polyeq_pqFormula_simplify True)) @@ \ + \ (Try (Rewrite_Set polyeq_simplify False)) @@ \ + \ (Try (Rewrite_Set norm_Rational_parenthesized False))) e_;\ + \ (L_::bool list) = ((Or_to_List e_)::bool list) \ + \ in Check_elementwise L_ {(v_::real). Assumptions} )" + )); + +store_met + (prep_met PolyEq.thy "met_polyeq_d2_abc" [] e_metID + (["PolyEq","solve_d2_polyeq_abc_equation"], + [("#Given" ,["equality e_","solveFor v_"]), + ("#Where" ,["(lhs e_) is_poly_in v_ ", + "((lhs e_) has_degree_in v_) = 2"]), + ("#Find" ,["solutions v_i_"]) + ], + {rew_ord'="termlessI", + rls'=PolyEq_erls, + srls=e_rls, + prls=PolyEq_prls, + calc=[("sqrt", ("Root.sqrt", eval_sqrt "#sqrt_"))], + crls=PolyEq_crls, nrls=norm_Rational(*, + (*asm_rls=["d2_polyeq_abcFormula_simplify"],*) + asm_rls=[], + asm_thm=[("d2_abcformula1",""),("d2_abcformula2",""),("d2_abcformula3",""), + ("d2_abcformula4",""),("d2_abcformula5",""),("d2_abcformula6",""), + ("d2_abcformula7",""),("d2_abcformula8",""),("d2_abcformula9",""), + ("d2_abcformula10",""),("d2_abcformula1_neg",""),("d2_abcformula2_neg",""), + ("d2_abcformula3_neg",""), ("d2_abcformula4_neg",""),("d2_abcformula5_neg",""), + ("d2_abcformula6_neg","")]*)}, + "Script Solve_d2_polyeq_abc_equation (e_::bool) (v_::real) = \ + \ (let e_ = ((Try (Rewrite_Set_Inst [(bdv,v_::real)] \ + \ d2_polyeq_abcFormula_simplify True)) @@ \ + \ (Try (Rewrite_Set polyeq_simplify False)) @@ \ + \ (Try (Rewrite_Set norm_Rational_parenthesized False))) e_;\ + \ (L_::bool list) = ((Or_to_List e_)::bool list) \ + \ in Check_elementwise L_ {(v_::real). Assumptions} )" + )); + +store_met + (prep_met PolyEq.thy "met_polyeq_d3" [] e_metID + (["PolyEq","solve_d3_polyeq_equation"], + [("#Given" ,["equality e_","solveFor v_"]), + ("#Where" ,["(lhs e_) is_poly_in v_ ", + "((lhs e_) has_degree_in v_) = 3"]), + ("#Find" ,["solutions v_i_"]) + ], + {rew_ord'="termlessI", + rls'=PolyEq_erls, + srls=e_rls, + prls=PolyEq_prls, + calc=[("sqrt", ("Root.sqrt", eval_sqrt "#sqrt_"))], + crls=PolyEq_crls, nrls=norm_Rational(*, + (* asm_rls=["d1_polyeq_simplify","d2_polyeq_simplify","d1_polyeq_simplify"],*) + asm_rls=[], + asm_thm=[("d3_isolate_div",""),("d1_isolate_div",""),("d2_pqformula1",""), + ("d2_pqformula2",""),("d2_pqformula3",""),("d2_pqformula4",""), + ("d2_pqformula1_neg",""), ("d2_pqformula2_neg",""),("d2_pqformula3_neg",""), + ("d2_pqformula4_neg",""), ("d2_abcformula1",""),("d2_abcformula2",""), + ("d2_abcformula1_neg",""),("d2_abcformula2_neg",""), + ("d2_sqrt_equation1",""),("d2_sqrt_equation1_neg",""), ("d2_isolate_div","")]*)}, + "Script Solve_d3_polyeq_equation (e_::bool) (v_::real) = \ + \ (let e_ = ((Try (Rewrite_Set_Inst [(bdv,v_::real)] \ + \ d3_polyeq_simplify True)) @@ \ + \ (Try (Rewrite_Set polyeq_simplify False)) @@ \ + \ (Try (Rewrite_Set_Inst [(bdv,v_::real)] \ + \ d2_polyeq_simplify True)) @@ \ + \ (Try (Rewrite_Set polyeq_simplify False)) @@ \ + \ (Try (Rewrite_Set_Inst [(bdv,v_::real)] \ + \ d1_polyeq_simplify True)) @@ \ + \ (Try (Rewrite_Set polyeq_simplify False)) @@ \ + \ (Try (Rewrite_Set norm_Rational_parenthesized False))) e_;\ + \ (L_::bool list) = ((Or_to_List e_)::bool list) \ + \ in Check_elementwise L_ {(v_::real). Assumptions} )" + )); + + (*.solves all expanded (ie. normalized) terms of degree 2.*) + (*Oct.02 restriction: 'eval_true 0 =< discriminant' ony for integer values + by 'PolyEq_erls'; restricted until Float.thy is implemented*) +store_met + (prep_met PolyEq.thy "met_polyeq_complsq" [] e_metID + (["PolyEq","complete_square"], + [("#Given" ,["equality e_","solveFor v_"]), + ("#Where" ,["matches (?a = 0) e_", + "((lhs e_) has_degree_in v_) = 2"]), + ("#Find" ,["solutions v_i_"]) + ], + {rew_ord'="termlessI",rls'=PolyEq_erls,srls=e_rls,prls=PolyEq_prls, + calc=[("sqrt", ("Root.sqrt", eval_sqrt "#sqrt_"))], + crls=PolyEq_crls, nrls=norm_Rational(*, + asm_rls=[], + asm_thm=[("root_plus_minus","")]*)}, + "Script Complete_square (e_::bool) (v_::real) = \ + \(let e_ = ((Try (Rewrite_Set_Inst [(bdv,v_)] cancel_leading_coeff True))\ + \ @@ (Try (Rewrite_Set_Inst [(bdv,v_)] complete_square True)) \ + \ @@ (Try (Rewrite square_explicit1 False)) \ + \ @@ (Try (Rewrite square_explicit2 False)) \ + \ @@ (Rewrite root_plus_minus True) \ + \ @@ (Try (Repeat (Rewrite_Inst [(bdv,v_)] bdv_explicit1 False))) \ + \ @@ (Try (Repeat (Rewrite_Inst [(bdv,v_)] bdv_explicit2 False))) \ + \ @@ (Try (Repeat \ + \ (Rewrite_Inst [(bdv,v_)] bdv_explicit3 False))) \ + \ @@ (Try (Rewrite_Set calculate_RootRat False)) \ + \ @@ (Try (Repeat (Calculate sqrt_)))) e_ \ + \ in ((Or_to_List e_)::bool list))" + )); +(*6.10.02: x^2=64: root_plus_minus -/-/-> + "Script Complete_square (e_::bool) (v_::real) = \ + \(let e_ = ((Try (Rewrite_Set_Inst [(bdv,v_)] cancel_leading_coeff True))\ + \ @@ (Try (Rewrite_Set_Inst [(bdv,v_)] complete_square True)) \ + \ @@ (Try ((Rewrite square_explicit1 False) \ + \ Or (Rewrite square_explicit2 False))) \ + \ @@ (Rewrite root_plus_minus True) \ + \ @@ ((Repeat (Rewrite_Inst [(bdv,v_)] bdv_explicit1 False)) \ + \ Or (Repeat (Rewrite_Inst [(bdv,v_)] bdv_explicit2 False))) \ + \ @@ (Try (Repeat \ + \ (Rewrite_Inst [(bdv,v_)] bdv_explicit3 False))) \ + \ @@ (Try (Rewrite_Set calculate_RootRat False)) \ + \ @@ (Try (Repeat (Calculate sqrt_)))) e_ \ + \ in ((Or_to_List e_)::bool list))"*) + +"******* PolyEq.ML end *******"; + +(*eine gehackte termorder*) +local (*. for make_polynomial_in .*) + +open Term; (* for type order = EQUAL | LESS | GREATER *) + +fun pr_ord EQUAL = "EQUAL" + | pr_ord LESS = "LESS" + | pr_ord GREATER = "GREATER"; + +fun dest_hd' x (Const (a, T)) = (((a, 0), T), 0) + | dest_hd' x (t as Free (a, T)) = + if x = t then ((("|||||||||||||", 0), T), 0) (*WN*) + else (((a, 0), T), 1) + | dest_hd' x (Var v) = (v, 2) + | dest_hd' x (Bound i) = ((("", i), dummyT), 3) + | dest_hd' x (Abs (_, T, _)) = ((("", 0), T), 4); + +fun size_of_term' x (Const ("Atools.pow",_) $ Free (var,_) $ Free (pot,_)) = + (case x of (*WN*) + (Free (xstr,_)) => + (if xstr = var then 1000*(the (int_of_str pot)) else 3) + | _ => raise error ("size_of_term' called with subst = "^ + (term2str x))) + | size_of_term' x (Free (subst,_)) = + (case x of + (Free (xstr,_)) => (if xstr = subst then 1000 else 1) + | _ => raise error ("size_of_term' called with subst = "^ + (term2str x))) + | size_of_term' x (Abs (_,_,body)) = 1 + size_of_term' x body + | size_of_term' x (f$t) = size_of_term' x f + size_of_term' x t + | size_of_term' x _ = 1; + + +fun term_ord' x pr thy (Abs (_, T, t), Abs(_, U, u)) = (* ~ term.ML *) + (case term_ord' x pr thy (t, u) of EQUAL => typ_ord (T, U) | ord => ord) + | term_ord' x pr thy (t, u) = + (if pr then + let + val (f, ts) = strip_comb t and (g, us) = strip_comb u; + val _=writeln("t= f@ts= \""^ + ((Syntax.string_of_term (thy2ctxt thy)) f)^"\" @ \"["^ + (commas(map(string_of_cterm o cterm_of(sign_of thy)) ts))^"]\""); + val _=writeln("u= g@us= \""^ + ((Syntax.string_of_term (thy2ctxt thy)) g)^"\" @ \"["^ + (commas(map(string_of_cterm o cterm_of(sign_of thy)) us))^"]\""); + val _=writeln("size_of_term(t,u)= ("^ + (string_of_int(size_of_term' x t))^", "^ + (string_of_int(size_of_term' x u))^")"); + val _=writeln("hd_ord(f,g) = "^((pr_ord o (hd_ord x))(f,g))); + val _=writeln("terms_ord(ts,us) = "^ + ((pr_ord o (terms_ord x) str false)(ts,us))); + val _=writeln("-------"); + in () end + else (); + case int_ord (size_of_term' x t, size_of_term' x u) of + EQUAL => + let val (f, ts) = strip_comb t and (g, us) = strip_comb u in + (case hd_ord x (f, g) of EQUAL => (terms_ord x str pr) (ts, us) + | ord => ord) + end + | ord => ord) +and hd_ord x (f, g) = (* ~ term.ML *) + prod_ord (prod_ord indexname_ord typ_ord) int_ord (dest_hd' x f, + dest_hd' x g) +and terms_ord x str pr (ts, us) = + list_ord (term_ord' x pr (assoc_thy "Isac.thy"))(ts, us); +(*val x = (term_of o the o (parse thy)) "x"; (*FIXXXXXXME*) +*) + +in + +fun ord_make_polynomial_in (pr:bool) thy subst tu = + let + (* val _=writeln("*** subs variable is: "^(subst2str subst)); *) + in + case subst of + (_,x)::_ => (term_ord' x pr thy tu = LESS) + | _ => raise error ("ord_make_polynomial_in called with subst = "^ + (subst2str subst)) + end; +end; + +val order_add_mult_in = prep_rls( + Rls{id = "order_add_mult_in", preconds = [], + rew_ord = ("ord_make_polynomial_in", + ord_make_polynomial_in false Poly.thy), + erls = e_rls,srls = Erls, + calc = [], + (*asm_thm = [],*) + rules = [Thm ("real_mult_commute",num_str real_mult_commute), + (* z * w = w * z *) + Thm ("real_mult_left_commute",num_str real_mult_left_commute), + (*z1.0 * (z2.0 * z3.0) = z2.0 * (z1.0 * z3.0)*) + Thm ("real_mult_assoc",num_str real_mult_assoc), + (*z1.0 * z2.0 * z3.0 = z1.0 * (z2.0 * z3.0)*) + Thm ("real_add_commute",num_str real_add_commute), + (*z + w = w + z*) + Thm ("real_add_left_commute",num_str real_add_left_commute), + (*x + (y + z) = y + (x + z)*) + Thm ("real_add_assoc",num_str real_add_assoc) + (*z1.0 + z2.0 + z3.0 = z1.0 + (z2.0 + z3.0)*) + ], scr = EmptyScr}:rls); + +val collect_bdv = prep_rls( + Rls{id = "collect_bdv", preconds = [], + rew_ord = ("dummy_ord", dummy_ord), + erls = e_rls,srls = Erls, + calc = [], + (*asm_thm = [],*) + rules = [Thm ("bdv_collect_1",num_str bdv_collect_1), + Thm ("bdv_collect_2",num_str bdv_collect_2), + Thm ("bdv_collect_3",num_str bdv_collect_3), + + Thm ("bdv_collect_assoc1_1",num_str bdv_collect_assoc1_1), + Thm ("bdv_collect_assoc1_2",num_str bdv_collect_assoc1_2), + Thm ("bdv_collect_assoc1_3",num_str bdv_collect_assoc1_3), + + Thm ("bdv_collect_assoc2_1",num_str bdv_collect_assoc2_1), + Thm ("bdv_collect_assoc2_2",num_str bdv_collect_assoc2_2), + Thm ("bdv_collect_assoc2_3",num_str bdv_collect_assoc2_3), + + + Thm ("bdv_n_collect_1",num_str bdv_n_collect_1), + Thm ("bdv_n_collect_2",num_str bdv_n_collect_2), + Thm ("bdv_n_collect_3",num_str bdv_n_collect_3), + + Thm ("bdv_n_collect_assoc1_1",num_str bdv_n_collect_assoc1_1), + Thm ("bdv_n_collect_assoc1_2",num_str bdv_n_collect_assoc1_2), + Thm ("bdv_n_collect_assoc1_3",num_str bdv_n_collect_assoc1_3), + + Thm ("bdv_n_collect_assoc2_1",num_str bdv_n_collect_assoc2_1), + Thm ("bdv_n_collect_assoc2_2",num_str bdv_n_collect_assoc2_2), + Thm ("bdv_n_collect_assoc2_3",num_str bdv_n_collect_assoc2_3) + ], scr = EmptyScr}:rls); + +(*.transforms an arbitrary term without roots to a polynomial [4] + according to knowledge/Poly.sml.*) +val make_polynomial_in = prep_rls( + Seq {id = "make_polynomial_in", preconds = []:term list, + rew_ord = ("dummy_ord", dummy_ord), + erls = Atools_erls, srls = Erls, + calc = [], (*asm_thm = [],*) + rules = [Rls_ expand_poly, + Rls_ order_add_mult_in, + Rls_ simplify_power, + Rls_ collect_numerals, + Rls_ reduce_012, + Thm ("realpow_oneI",num_str realpow_oneI), + Rls_ discard_parentheses, + Rls_ collect_bdv + ], + scr = EmptyScr + }:rls); + +val separate_bdvs = + append_rls "separate_bdvs" + collect_bdv + [Thm ("separate_bdv", num_str separate_bdv), + (*"?a * ?bdv / ?b = ?a / ?b * ?bdv"*) + Thm ("separate_bdv_n", num_str separate_bdv_n), + Thm ("separate_1_bdv", num_str separate_1_bdv), + (*"?bdv / ?b = (1 / ?b) * ?bdv"*) + Thm ("separate_1_bdv_n", num_str separate_1_bdv_n), + (*"?bdv ^^^ ?n / ?b = 1 / ?b * ?bdv ^^^ ?n"*) + Thm ("real_add_divide_distrib", + num_str real_add_divide_distrib) + (*"(?x + ?y) / ?z = ?x / ?z + ?y / ?z" + WN051031 DOES NOT BELONG TO HERE*) + ]; +val make_ratpoly_in = prep_rls( + Seq {id = "make_ratpoly_in", preconds = []:term list, + rew_ord = ("dummy_ord", dummy_ord), + erls = Atools_erls, srls = Erls, + calc = [], (*asm_thm = [],*) + rules = [Rls_ norm_Rational, + Rls_ order_add_mult_in, + Rls_ discard_parentheses, + Rls_ separate_bdvs, + (* Rls_ rearrange_assoc, WN060916 why does cancel_p not work?*) + Rls_ cancel_p + (*Calc ("HOL.divide" ,eval_cancel "#divide_") too weak!*) + ], + scr = EmptyScr}:rls); + + +ruleset' := overwritelthy thy (!ruleset', + [("order_add_mult_in", order_add_mult_in), + ("collect_bdv", collect_bdv), + ("make_polynomial_in", make_polynomial_in), + ("make_ratpoly_in", make_ratpoly_in), + ("separate_bdvs", separate_bdvs) + ]); +