1.1 --- a/src/Tools/isac/IsacKnowledge/RootRatEq.ML Wed Aug 25 15:15:01 2010 +0200
1.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
1.3 @@ -1,166 +0,0 @@
1.4 -(*.(c) by Richard Lang, 2003 .*)
1.5 -(* collecting all knowledge for Root and Rational Equations
1.6 - created by: rlang
1.7 - date: 02.10
1.8 - changed by: rlang
1.9 - last change by: rlang
1.10 - date: 02.11.04
1.11 -*)
1.12 -
1.13 -(* use"knowledge/RootRatEq.ML";
1.14 - use"RootRatEq.ML";
1.15 -
1.16 - use"ROOT.ML";
1.17 - cd"knowledge";
1.18 -
1.19 - remove_thy"RootRatEq";
1.20 - use_thy"Isac";
1.21 - *)
1.22 -
1.23 -"******* RootRatEq.ML begin *******";
1.24 -theory' := overwritel (!theory', [("RootRatEq.thy",RootRatEq.thy)]);
1.25 -
1.26 -(*-------------------------functions---------------------*)
1.27 -(* true if denominator contains (sq)root in + or - term
1.28 - 1/(sqrt(x+3)*(x+4)) -> false; 1/(sqrt(x)+2) -> true
1.29 - if false then (term)^2 contains no (sq)root *)
1.30 -fun is_rootRatAddTerm_in t v =
1.31 - let
1.32 - fun coeff_in c v = member op = (vars c) v;
1.33 - fun rootadd (t as (Const ("op +",_) $ t2 $ t3)) v = (is_rootTerm_in t2 v) orelse
1.34 - (is_rootTerm_in t3 v)
1.35 - | rootadd (t as (Const ("op -",_) $ t2 $ t3)) v = (is_rootTerm_in t2 v) orelse
1.36 - (is_rootTerm_in t3 v)
1.37 - | rootadd _ _ = false;
1.38 - fun findrootrat (_ $ _ $ _ $ _) v = raise error("is_rootRatAddTerm_in:")
1.39 - (* at the moment there is no term like this, but ....*)
1.40 - | findrootrat (t as (Const ("HOL.divide",_) $ _ $ t3)) v =
1.41 - if (is_rootTerm_in t3 v) then rootadd t3 v else false
1.42 - | findrootrat (_ $ t1 $ t2) v = (findrootrat t1 v) orelse (findrootrat t2 v)
1.43 - | findrootrat (_ $ t1) v = (findrootrat t1 v)
1.44 - | findrootrat _ _ = false;
1.45 - in
1.46 - findrootrat t v
1.47 - end;
1.48 -
1.49 -fun eval_is_rootRatAddTerm_in _ _ (p as (Const ("RootRatEq.is'_rootRatAddTerm'_in",_) $ t $ v)) _ =
1.50 - if is_rootRatAddTerm_in t v then
1.51 - SOME ((term2str p) ^ " = True",
1.52 - Trueprop $ (mk_equality (p, HOLogic.true_const)))
1.53 - else SOME ((term2str p) ^ " = True",
1.54 - Trueprop $ (mk_equality (p, HOLogic.false_const)))
1.55 - | eval_is_rootRatAddTerm_in _ _ _ _ = ((*writeln"### nichts matcht";*) NONE);
1.56 -
1.57 -(*-------------------------rulse-------------------------*)
1.58 -val RootRatEq_prls =
1.59 - append_rls "RootRatEq_prls" e_rls
1.60 - [Calc ("Atools.ident",eval_ident "#ident_"),
1.61 - Calc ("Tools.matches",eval_matches ""),
1.62 - Calc ("Tools.lhs" ,eval_lhs ""),
1.63 - Calc ("Tools.rhs" ,eval_rhs ""),
1.64 - Calc ("RootEq.is'_rootTerm'_in",eval_is_rootTerm_in ""),
1.65 - Calc ("RootRatEq.is'_rootRatAddTerm'_in", eval_is_rootRatAddTerm_in ""),
1.66 - Calc ("op =",eval_equal "#equal_"),
1.67 - Thm ("not_true",num_str not_true),
1.68 - Thm ("not_false",num_str not_false),
1.69 - Thm ("and_true",num_str and_true),
1.70 - Thm ("and_false",num_str and_false),
1.71 - Thm ("or_true",num_str or_true),
1.72 - Thm ("or_false",num_str or_false)
1.73 - ];
1.74 -
1.75 -
1.76 -val RooRatEq_erls =
1.77 - merge_rls "RooRatEq_erls" rootrat_erls
1.78 - (merge_rls "" RootEq_erls
1.79 - (merge_rls "" rateq_erls
1.80 - (append_rls "" e_rls
1.81 - [])));
1.82 -
1.83 -val RootRatEq_crls =
1.84 - merge_rls "RootRatEq_crls" rootrat_erls
1.85 - (merge_rls "" RootEq_erls
1.86 - (merge_rls "" rateq_erls
1.87 - (append_rls "" e_rls
1.88 - [])));
1.89 -
1.90 -ruleset' := overwritelthy thy (!ruleset',
1.91 - [("RooRatEq_erls",RooRatEq_erls) (*FIXXXME:del with rls.rls'*)
1.92 - ]);
1.93 -
1.94 -(* Solves a rootrat Equation *)
1.95 - val rootrat_solve = prep_rls(
1.96 - Rls {id = "rootrat_solve", preconds = [],
1.97 - rew_ord = ("termlessI",termlessI),
1.98 - erls = e_rls, srls = Erls, calc = [], (*asm_thm = [],*)
1.99 - rules = [ Thm("rootrat_equation_left_1",num_str rootrat_equation_left_1),
1.100 - (* [|c is_rootTerm_in bdv|] ==> ( (a + b/c = d) = ( b = (d - a) * c )) *)
1.101 - Thm("rootrat_equation_left_2",num_str rootrat_equation_left_2),
1.102 - (* [|c is_rootTerm_in bdv|] ==> ( (b/c = d) = ( b = d * c )) *)
1.103 - Thm("rootrat_equation_right_1",num_str rootrat_equation_right_1),
1.104 - (* [|f is_rootTerm_in bdv|] ==> ( (a = d + e/f) = ( (a - d) * f = e )) *)
1.105 - Thm("rootrat_equation_right_2",num_str rootrat_equation_right_2)
1.106 - (* [|f is_rootTerm_in bdv|] ==> ( (a = e/f) = ( a * f = e )) *)
1.107 - ],
1.108 - scr = Script ((term_of o the o (parse thy)) "empty_script")
1.109 - }:rls);
1.110 -ruleset' := overwritelthy thy (!ruleset',
1.111 - [("rootrat_solve",rootrat_solve)
1.112 - ]);
1.113 -
1.114 -(*-----------------------probleme------------------------*)
1.115 -(*
1.116 -(get_pbt ["rat","root","univariate","equation"]);
1.117 -show_ptyps();
1.118 -*)
1.119 -store_pbt
1.120 - (prep_pbt RootRatEq.thy "pbl_equ_univ_root_sq_rat" [] e_pblID
1.121 - (["rat","sq","root","univariate","equation"],
1.122 - [("#Given" ,["equality e_","solveFor v_"]),
1.123 - ("#Where" ,["( (lhs e_) is_rootRatAddTerm_in (v_::real) )| \
1.124 - \( (rhs e_) is_rootRatAddTerm_in (v_::real) )"]),
1.125 - ("#Find" ,["solutions v_i_"])
1.126 - ],
1.127 - RootRatEq_prls, SOME "solve (e_::bool, v_)",
1.128 - [["RootRatEq","elim_rootrat_equation"]]));
1.129 -
1.130 -(*-------------------------Methode-----------------------*)
1.131 -store_met
1.132 - (prep_met LinEq.thy "met_rootrateq" [] e_metID
1.133 - (["RootRatEq"],
1.134 - [],
1.135 - {rew_ord'="tless_true",rls'=Atools_erls,calc = [], srls = e_rls, prls=e_rls,
1.136 - crls=Atools_erls, nrls=norm_Rational(*,
1.137 - asm_rls=[],asm_thm=[]*)}, "empty_script"));
1.138 -(*-- left 20.10.02 --*)
1.139 -store_met
1.140 - (prep_met RootRatEq.thy "met_rootrateq_elim" [] e_metID
1.141 - (["RootRatEq","elim_rootrat_equation"],
1.142 - [("#Given" ,["equality e_","solveFor v_"]),
1.143 - ("#Where" ,["( (lhs e_) is_rootRatAddTerm_in (v_::real) ) | \
1.144 - \( (rhs e_) is_rootRatAddTerm_in (v_::real) )"]),
1.145 - ("#Find" ,["solutions v_i_"])
1.146 - ],
1.147 - {rew_ord'="termlessI",
1.148 - rls'=RooRatEq_erls,
1.149 - srls=e_rls,
1.150 - prls=RootRatEq_prls,
1.151 - calc=[],
1.152 - crls=RootRatEq_crls, nrls=norm_Rational(*,
1.153 - asm_rls=[],
1.154 - asm_thm=[]*)},
1.155 - "Script Elim_rootrat_equation (e_::bool) (v_::real) = \
1.156 - \(let e_ = ((Try (Rewrite_Set expand_rootbinoms False)) @@ \
1.157 - \ (Try (Rewrite_Set rooteq_simplify False)) @@ \
1.158 - \ (Try (Rewrite_Set make_rooteq False)) @@ \
1.159 - \ (Try (Rewrite_Set rooteq_simplify False)) @@ \
1.160 - \ (Try (Rewrite_Set_Inst [(bdv,v_)] \
1.161 - \ rootrat_solve False))) e_ \
1.162 - \ in (SubProblem (RootEq_,[univariate,equation], \
1.163 - \ [no_met]) [bool_ e_, real_ v_]))"
1.164 - ));
1.165 -calclist':= overwritel (!calclist',
1.166 - [("is_rootRatAddTerm_in", ("RootRatEq.is_rootRatAddTerm_in",
1.167 - eval_is_rootRatAddTerm_in""))
1.168 - ]);(*("", ("", "")),*)
1.169 -"******* RootRatEq.ML end *******";