1.1 --- a/src/sml/IsacKnowledge/Integrate.ML Sat Aug 20 18:25:14 2005 +0200
1.2 +++ b/src/sml/IsacKnowledge/Integrate.ML Sat Aug 20 19:10:30 2005 +0200
1.3 @@ -89,7 +89,9 @@
1.4 rew_ord = ("termlessI",termlessI),
1.5 erls = Erls,
1.6 srls = Erls, calc = [],
1.7 - rules = [Calc ("Tools.matches", eval_matches "")
1.8 + rules = [Calc ("Tools.matches", eval_matches""),
1.9 + Thm ("not_true",num_str not_true),
1.10 + Thm ("not_false",num_str not_false)
1.11 ],
1.12 scr = EmptyScr},
1.13 srls = Erls, calc = [],
2.1 --- a/src/smltest/IsacKnowledge/integrate.sml Sat Aug 20 18:25:14 2005 +0200
2.2 +++ b/src/smltest/IsacKnowledge/integrate.sml Sat Aug 20 19:10:30 2005 +0200
2.3 @@ -32,6 +32,7 @@
2.4 val t = str2t "Integral x^^^2 D x";
2.5 atomty thy t;
2.6
2.7 +
2.8 "----------- integrate by rewriting ------------------------------";
2.9 "----------- integrate by rewriting ------------------------------";
2.10 "----------- integrate by rewriting ------------------------------";
2.11 @@ -70,6 +71,7 @@
2.12
2.13 val str = rewrit integral_pow (str2t "Integral x^^^3 D x"); term2s str;
2.14
2.15 +
2.16 "----------- test new_c ------------------------------------------";
2.17 "----------- test new_c ------------------------------------------";
2.18 "----------- test new_c ------------------------------------------";
2.19 @@ -106,18 +108,10 @@
2.20 fun rewrit thm str =
2.21 fst (the (rewrite_inst_ Integrate.thy tless_true
2.22 conditions_in_integration true subs thm str));
2.23 -(*
2.24 -trace_rewrite := true;
2.25 -*)
2.26 val str = rewrit call_for_new_c (str2t "x ^^^ 2 / 2"); term2s str;
2.27 val str = (rewrit call_for_new_c str)
2.28 handle OPTION => str2t "no_rewrite";;
2.29
2.30 -(*
2.31 -use"~/proto2/isac/src/smltest/IsacKnowledge/integrate.sml";
2.32 -*)
2.33 -(*################################################################;
2.34 -
2.35
2.36 "----------- integrate by ruleset --------------------------------";
2.37 "----------- integrate by ruleset --------------------------------";
2.38 @@ -125,18 +119,21 @@
2.39 fun rewrite_se subs rls str =
2.40 fst (the (rewrite_set_inst "Integrate.thy" true subs rls str));
2.41 val subs = [("bdv","x::real")];
2.42 +val rls = "integration_rules";
2.43 +val str = rewrite_se subs rls "Integral x D x";
2.44 +val str = rewrite_se subs rls "Integral c * x ^^^ 2 + c_2 D x";
2.45 +if str = "c * (x ^^^ 3 / 3) + c_2 * x"
2.46 +then () else raise error "integrate.sml: diff.behav. in integration_rules";
2.47 +
2.48 +val rls = "add_new_c";
2.49 +val str = rewrite_se subs rls "c * (x ^^^ 3 / 3) + c_2 * x";
2.50 +if str = "c * (x ^^^ 3 / 3) + c_2 * x + c_3" then ()
2.51 +else raise error "integrate.sml: diff.behav. in add_new_c";
2.52 +
2.53 val rls = "integration";
2.54 val str = rewrite_se subs rls "Integral c * x ^^^ 2 + c_2 D x";
2.55 -
2.56 -val str = rewrite_se subs rls "Integral x D x";
2.57 -
2.58 if str = "c * (x ^^^ 3 / 3) + c_2 * x + c_3"
2.59 -then () else raise error "integrate.sml: diff.behav. in rew.by ruleset";
2.60 -
2.61 -(*
2.62 -use"~/proto2/isac/src/smltest/IsacKnowledge/integrate.sml";
2.63 -*)
2.64 -################################################################;*)
2.65 +then () else raise error "integrate.sml: diff.behav. in integration";
2.66
2.67
2.68 "----------- check probem type -----------------------------------";
2.69 @@ -162,12 +159,25 @@
2.70 "----------- check method [Diff,integration] ---------------------";
2.71 "----------- check method [Diff,integration] ---------------------";
2.72 show_mets();
2.73 +(*
2.74 val str =
2.75 -"Script IntegrationScript (f_::real) (v_::real) = \
2.76 -\ ((Rewrite_Set_Inst [(bdv,v_)] integration_rules False)\
2.77 -\ (Integral f_ D v_))";
2.78 +"Script IntegrationScript (f_::real) (v_::real) = \
2.79 +\ (let t_ = (Integral f_ D v_)::real \
2.80 +\ in (Rewrite_Set_Inst [(bdv,v_)] integration False t_::real))";
2.81 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
2.82 +
2.83 +val str =
2.84 +"Script IntegrationScript (f_::real) (v_::real) = \
2.85 +\ (let t_ = (Integral f_ D v_)::real \
2.86 +\ in t_)";
2.87 +val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
2.88 +val str =
2.89 +"Rewrite_Set_Inst [(bdv,v_)] integration False (t_::real)";
2.90 +val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
2.91 +
2.92 +
2.93 atomty thy sc;
2.94 +###############################################################*)
2.95
2.96 "----------- me method [Diff,integration] ---------------------";
2.97 "----------- me method [Diff,integration] ---------------------";