diff -r a28b5fc129b7 -r 22235e4dbe5f src/Tools/isac/Knowledge/RatEq.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Tools/isac/Knowledge/RatEq.ML Wed Aug 25 16:20:07 2010 +0200 @@ -0,0 +1,203 @@ +(*.(c) by Richard Lang, 2003 .*) +(* collecting all knowledge for RationalEquations + created by: rlang + date: 02.09 + changed by: rlang + last change by: rlang + date: 02.11.29 +*) + +(* use"Knowledge/RatEq.ML"; + use"RatEq.ML"; + remove_thy"RatEq"; + use_thy"Isac"; + + use"ROOT.ML"; + cd"IsacKnowledge"; + *) +"******* RatEq.ML begin *******"; + +theory' := overwritel (!theory', [("RatEq.thy",RatEq.thy)]); + +(*-------------------------functions-----------------------*) +(* is_rateqation_in becomes true, if a bdv is in the denominator of a fraction*) +fun is_rateqation_in t v = + let + fun coeff_in c v = member op = (vars c) v; + fun finddivide (_ $ _ $ _ $ _) v = raise error("is_rateqation_in:") + (* at the moment there is no term like this, but ....*) + | finddivide (t as (Const ("HOL.divide",_) $ _ $ b)) v = coeff_in b v + | finddivide (_ $ t1 $ t2) v = (finddivide t1 v) + orelse (finddivide t2 v) + | finddivide (_ $ t1) v = (finddivide t1 v) + | finddivide _ _ = false; + in + finddivide t v + end; + +fun eval_is_ratequation_in _ _ (p as (Const ("RatEq.is'_ratequation'_in",_) $ t $ v)) _ = + if is_rateqation_in t v then + SOME ((term2str p) ^ " = True", + Trueprop $ (mk_equality (p, HOLogic.true_const))) + else SOME ((term2str p) ^ " = True", + Trueprop $ (mk_equality (p, HOLogic.false_const))) + | eval_is_ratequation_in _ _ _ _ = ((*writeln"### nichts matcht";*) NONE); + +(*-------------------------rulse-----------------------*) +val RatEq_prls = (*15.10.02:just the following order due to subterm evaluation*) + append_rls "RatEq_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 ("RatEq.is'_ratequation'_in",eval_is_ratequation_in ""), + Calc ("op =",eval_equal "#equal_"), + 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) + ]; + + +(*rls = merge_rls erls Poly_erls *) +val rateq_erls = + remove_rls "rateq_erls" (*WN: ein Hack*) + (merge_rls "is_ratequation_in" calculate_Rational + (append_rls "is_ratequation_in" + Poly_erls + [(*Calc ("HOL.divide", eval_cancel "#divide_"),*) + Calc ("RatEq.is'_ratequation'_in", + eval_is_ratequation_in "") + + ])) + [Thm ("and_commute",num_str and_commute), (*WN: ein Hack*) + Thm ("or_commute",num_str or_commute) (*WN: ein Hack*) + ]; +ruleset' := overwritelthy thy (!ruleset', + [("rateq_erls",rateq_erls)(*FIXXXME:del with rls.rls'*) + ]); + + +val RatEq_crls = + remove_rls "RatEq_crls" (*WN: ein Hack*) + (merge_rls "is_ratequation_in" calculate_Rational + (append_rls "is_ratequation_in" + Poly_erls + [(*Calc ("HOL.divide", eval_cancel "#divide_"),*) + Calc ("RatEq.is'_ratequation'_in", + eval_is_ratequation_in "") + ])) + [Thm ("and_commute",num_str and_commute), (*WN: ein Hack*) + Thm ("or_commute",num_str or_commute) (*WN: ein Hack*) + ]; + +val RatEq_eliminate = prep_rls( + Rls {id = "RatEq_eliminate", preconds = [], rew_ord = ("termlessI",termlessI), + erls = rateq_erls, srls = Erls, calc = [], + (*asm_thm = [("rat_mult_denominator_both",""),("rat_mult_denominator_left",""), + ("rat_mult_denominator_right","")],*) + rules = [ + Thm("rat_mult_denominator_both",num_str rat_mult_denominator_both), + (* a/b=c/d -> ad=cb *) + Thm("rat_mult_denominator_left",num_str rat_mult_denominator_left), + (* a =c/d -> ad=c *) + Thm("rat_mult_denominator_right",num_str rat_mult_denominator_right) + (* a/b=c -> a=cb *) + ], + scr = Script ((term_of o the o (parse thy)) "empty_script") + }:rls); +ruleset' := overwritelthy thy (!ruleset', + [("RatEq_eliminate",RatEq_eliminate) + ]); + + + + +val RatEq_simplify = prep_rls( + Rls {id = "RatEq_simplify", preconds = [], rew_ord = ("termlessI",termlessI), + erls = rateq_erls, srls = Erls, calc = [], + (*asm_thm = [("rat_double_rat_1",""),("rat_double_rat_2",""), + ("rat_double_rat_3","")],*) + rules = [ + Thm("real_rat_mult_1",num_str real_rat_mult_1), + (*a*(b/c) = (a*b)/c*) + Thm("real_rat_mult_2",num_str real_rat_mult_2), + (*(a/b)*(c/d) = (a*c)/(b*d)*) + Thm("real_rat_mult_3",num_str real_rat_mult_3), + (* (a/b)*c = (a*c)/b*) + Thm("real_rat_pow",num_str real_rat_pow), + (*(a/b)^^^2 = a^^^2/b^^^2*) + Thm("real_diff_minus",num_str real_diff_minus), + (* a - b = a + (-1) * b *) + Thm("rat_double_rat_1",num_str rat_double_rat_1), + (* (a / (c/d) = (a*d) / c) *) + Thm("rat_double_rat_2",num_str rat_double_rat_2), + (* ((a/b) / (c/d) = (a*d) / (b*c)) *) + Thm("rat_double_rat_3",num_str rat_double_rat_3) + (* ((a/b) / c = a / (b*c) ) *) + ], + scr = Script ((term_of o the o (parse thy)) "empty_script") + }:rls); +ruleset' := overwritelthy thy (!ruleset', + [("RatEq_simplify",RatEq_simplify) + ]); + +(*-------------------------Problem-----------------------*) +(* +(get_pbt ["rational","univariate","equation"]); +show_ptyps(); +*) +store_pbt + (prep_pbt RatEq.thy "pbl_equ_univ_rat" [] e_pblID + (["rational","univariate","equation"], + [("#Given" ,["equality e_","solveFor v_"]), + ("#Where" ,["(e_::bool) is_ratequation_in (v_::real)"]), + ("#Find" ,["solutions v_i_"]) + ], + + RatEq_prls, SOME "solve (e_::bool, v_)", + [["RatEq","solve_rat_equation"]])); + + +(*-------------------------methods-----------------------*) +store_met + (prep_met RatEq.thy "met_rateq" [] e_metID + (["RatEq"], + [], + {rew_ord'="tless_true",rls'=Atools_erls,calc = [], srls = e_rls, prls=e_rls, + crls=RatEq_crls, nrls=norm_Rational + (*, asm_rls=[],asm_thm=[]*)}, "empty_script")); +store_met + (prep_met RatEq.thy "met_rat_eq" [] e_metID + (["RatEq","solve_rat_equation"], + [("#Given" ,["equality e_","solveFor v_"]), + ("#Where" ,["(e_::bool) is_ratequation_in (v_::real)"]), + ("#Find" ,["solutions v_i_"]) + ], + {rew_ord'="termlessI", + rls'=rateq_erls, + srls=e_rls, + prls=RatEq_prls, + calc=[], + crls=RatEq_crls, nrls=norm_Rational(*, + asm_rls=[], + asm_thm=[("rat_double_rat_1",""),("rat_double_rat_2",""),("rat_double_rat_3",""), + ("rat_mult_denominator_both",""),("rat_mult_denominator_left",""), + ("rat_mult_denominator_right","")]*)}, + "Script Solve_rat_equation (e_::bool) (v_::real) = \ + \(let e_ = ((Repeat(Try (Rewrite_Set RatEq_simplify True))) @@ \ + \ (Repeat(Try (Rewrite_Set norm_Rational False))) @@ \ + \ (Repeat(Try (Rewrite_Set common_nominator_p False))) @@ \ + \ (Repeat(Try (Rewrite_Set RatEq_eliminate True)))) e_;\ + \ (L_::bool list) = (SubProblem (RatEq_,[univariate,equation], \ + \ [no_met]) [bool_ e_, real_ v_]) \ + \ in Check_elementwise L_ {(v_::real). Assumptions})" + )); + +calclist':= overwritel (!calclist', + [("is_ratequation_in", ("RatEq.is_ratequation_in", + eval_is_ratequation_in "")) + ]); +"******* RatEq.ML end *******";