diff -r a28b5fc129b7 -r 22235e4dbe5f src/Tools/isac/Knowledge/RootRatEq.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Tools/isac/Knowledge/RootRatEq.ML Wed Aug 25 16:20:07 2010 +0200 @@ -0,0 +1,166 @@ +(*.(c) by Richard Lang, 2003 .*) +(* collecting all knowledge for Root and Rational Equations + created by: rlang + date: 02.10 + changed by: rlang + last change by: rlang + date: 02.11.04 +*) + +(* use"knowledge/RootRatEq.ML"; + use"RootRatEq.ML"; + + use"ROOT.ML"; + cd"knowledge"; + + remove_thy"RootRatEq"; + use_thy"Isac"; + *) + +"******* RootRatEq.ML begin *******"; +theory' := overwritel (!theory', [("RootRatEq.thy",RootRatEq.thy)]); + +(*-------------------------functions---------------------*) +(* true if denominator contains (sq)root in + or - term + 1/(sqrt(x+3)*(x+4)) -> false; 1/(sqrt(x)+2) -> true + if false then (term)^2 contains no (sq)root *) +fun is_rootRatAddTerm_in t v = + let + fun coeff_in c v = member op = (vars c) v; + fun rootadd (t as (Const ("op +",_) $ t2 $ t3)) v = (is_rootTerm_in t2 v) orelse + (is_rootTerm_in t3 v) + | rootadd (t as (Const ("op -",_) $ t2 $ t3)) v = (is_rootTerm_in t2 v) orelse + (is_rootTerm_in t3 v) + | rootadd _ _ = false; + fun findrootrat (_ $ _ $ _ $ _) v = raise error("is_rootRatAddTerm_in:") + (* at the moment there is no term like this, but ....*) + | findrootrat (t as (Const ("HOL.divide",_) $ _ $ t3)) v = + if (is_rootTerm_in t3 v) then rootadd t3 v else false + | findrootrat (_ $ t1 $ t2) v = (findrootrat t1 v) orelse (findrootrat t2 v) + | findrootrat (_ $ t1) v = (findrootrat t1 v) + | findrootrat _ _ = false; + in + findrootrat t v + end; + +fun eval_is_rootRatAddTerm_in _ _ (p as (Const ("RootRatEq.is'_rootRatAddTerm'_in",_) $ t $ v)) _ = + if is_rootRatAddTerm_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_rootRatAddTerm_in _ _ _ _ = ((*writeln"### nichts matcht";*) NONE); + +(*-------------------------rulse-------------------------*) +val RootRatEq_prls = + append_rls "RootRatEq_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 ("RootEq.is'_rootTerm'_in",eval_is_rootTerm_in ""), + Calc ("RootRatEq.is'_rootRatAddTerm'_in", eval_is_rootRatAddTerm_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) + ]; + + +val RooRatEq_erls = + merge_rls "RooRatEq_erls" rootrat_erls + (merge_rls "" RootEq_erls + (merge_rls "" rateq_erls + (append_rls "" e_rls + []))); + +val RootRatEq_crls = + merge_rls "RootRatEq_crls" rootrat_erls + (merge_rls "" RootEq_erls + (merge_rls "" rateq_erls + (append_rls "" e_rls + []))); + +ruleset' := overwritelthy thy (!ruleset', + [("RooRatEq_erls",RooRatEq_erls) (*FIXXXME:del with rls.rls'*) + ]); + +(* Solves a rootrat Equation *) + val rootrat_solve = prep_rls( + Rls {id = "rootrat_solve", preconds = [], + rew_ord = ("termlessI",termlessI), + erls = e_rls, srls = Erls, calc = [], (*asm_thm = [],*) + rules = [ Thm("rootrat_equation_left_1",num_str rootrat_equation_left_1), + (* [|c is_rootTerm_in bdv|] ==> ( (a + b/c = d) = ( b = (d - a) * c )) *) + Thm("rootrat_equation_left_2",num_str rootrat_equation_left_2), + (* [|c is_rootTerm_in bdv|] ==> ( (b/c = d) = ( b = d * c )) *) + Thm("rootrat_equation_right_1",num_str rootrat_equation_right_1), + (* [|f is_rootTerm_in bdv|] ==> ( (a = d + e/f) = ( (a - d) * f = e )) *) + Thm("rootrat_equation_right_2",num_str rootrat_equation_right_2) + (* [|f is_rootTerm_in bdv|] ==> ( (a = e/f) = ( a * f = e )) *) + ], + scr = Script ((term_of o the o (parse thy)) "empty_script") + }:rls); +ruleset' := overwritelthy thy (!ruleset', + [("rootrat_solve",rootrat_solve) + ]); + +(*-----------------------probleme------------------------*) +(* +(get_pbt ["rat","root","univariate","equation"]); +show_ptyps(); +*) +store_pbt + (prep_pbt RootRatEq.thy "pbl_equ_univ_root_sq_rat" [] e_pblID + (["rat","sq","root","univariate","equation"], + [("#Given" ,["equality e_","solveFor v_"]), + ("#Where" ,["( (lhs e_) is_rootRatAddTerm_in (v_::real) )| \ + \( (rhs e_) is_rootRatAddTerm_in (v_::real) )"]), + ("#Find" ,["solutions v_i_"]) + ], + RootRatEq_prls, SOME "solve (e_::bool, v_)", + [["RootRatEq","elim_rootrat_equation"]])); + +(*-------------------------Methode-----------------------*) +store_met + (prep_met LinEq.thy "met_rootrateq" [] e_metID + (["RootRatEq"], + [], + {rew_ord'="tless_true",rls'=Atools_erls,calc = [], srls = e_rls, prls=e_rls, + crls=Atools_erls, nrls=norm_Rational(*, + asm_rls=[],asm_thm=[]*)}, "empty_script")); +(*-- left 20.10.02 --*) +store_met + (prep_met RootRatEq.thy "met_rootrateq_elim" [] e_metID + (["RootRatEq","elim_rootrat_equation"], + [("#Given" ,["equality e_","solveFor v_"]), + ("#Where" ,["( (lhs e_) is_rootRatAddTerm_in (v_::real) ) | \ + \( (rhs e_) is_rootRatAddTerm_in (v_::real) )"]), + ("#Find" ,["solutions v_i_"]) + ], + {rew_ord'="termlessI", + rls'=RooRatEq_erls, + srls=e_rls, + prls=RootRatEq_prls, + calc=[], + crls=RootRatEq_crls, nrls=norm_Rational(*, + asm_rls=[], + asm_thm=[]*)}, + "Script Elim_rootrat_equation (e_::bool) (v_::real) = \ + \(let e_ = ((Try (Rewrite_Set expand_rootbinoms False)) @@ \ + \ (Try (Rewrite_Set rooteq_simplify False)) @@ \ + \ (Try (Rewrite_Set make_rooteq False)) @@ \ + \ (Try (Rewrite_Set rooteq_simplify False)) @@ \ + \ (Try (Rewrite_Set_Inst [(bdv,v_)] \ + \ rootrat_solve False))) e_ \ + \ in (SubProblem (RootEq_,[univariate,equation], \ + \ [no_met]) [bool_ e_, real_ v_]))" + )); +calclist':= overwritel (!calclist', + [("is_rootRatAddTerm_in", ("RootRatEq.is_rootRatAddTerm_in", + eval_is_rootRatAddTerm_in"")) + ]);(*("", ("", "")),*) +"******* RootRatEq.ML end *******";