1 (* tests on integration over the reals
4 (c) due to copyright terms
6 use"~/proto2/isac/src/smltest/IsacKnowledge/integrate.sml";
8 val thy = Integrate.thy;
10 "-----------------------------------------------------------------";
11 "table of contents -----------------------------------------------";
12 "-----------------------------------------------------------------";
13 "----------- parsing ---------------------------------------------";
14 "----------- integrate by rewriting ------------------------------";
15 "----------- test new_c ------------------------------------------";
16 "----------- integrate by ruleset --------------------------------";
17 "----------- check probem type -----------------------------------";
18 "----------- check Scripts ---------------------------------------";
19 "----------- me method [Diff,integration] ------------------------";
20 "-----------------------------------------------------------------";
21 "-----------------------------------------------------------------";
22 "-----------------------------------------------------------------";
24 "----------- parsing ---------------------------------------------";
25 "----------- parsing ---------------------------------------------";
26 "----------- parsing ---------------------------------------------";
27 fun str2t str = (term_of o the o (parse Integrate.thy)) str;
28 fun term2s t = Sign.string_of_term (sign_of Integrate.thy) t;
30 val t = str2t "Integral x D x";
31 val t = str2t "Integral x^^^2 D x";
35 "----------- integrate by rewriting ------------------------------";
36 "----------- integrate by rewriting ------------------------------";
37 "----------- integrate by rewriting ------------------------------";
38 val conditions_in_integration_rules =
39 Rls {id="conditions_in_integration_rules",
41 rew_ord = ("termlessI",termlessI),
43 srls = Erls, calc = [],
44 rules = [(*for rewriting conditions in Thm's*)
45 Calc ("Atools.occurs'_in",
46 eval_occurs_in "#occurs_in_"),
47 Thm ("not_true",num_str not_true),
48 Thm ("not_false",not_false)
51 val subs = [(str2t "bdv", str2t "x")];
53 fst (the (rewrite_inst_ Integrate.thy tless_true
54 conditions_in_integration_rules
56 val str = rewrit integral_const (str2t "Integral 1 D x"); term2s str;
57 val str = rewrit integral_const (str2t "Integral M'/EJ D x"); term2s str;
58 val str = (rewrit integral_const (str2t "Integral x D x"))
59 handle OPTION => str2t "no_rewrite";
61 val str = rewrit integral_var (str2t "Integral x D x"); term2s str;
62 val str = (rewrit integral_var (str2t "Integral a D x"))
63 handle OPTION => str2t "no_rewrite";
65 val str = rewrit integral_add (str2t "Integral x + 1 D x"); term2s str;
67 val str = rewrit integral_mult (str2t "Integral M'/EJ * x^^^3 D x");term2s str;
68 val str = (rewrit integral_mult (str2t "Integral x * x D x"))
69 handle OPTION => str2t "no_rewrite";
71 val str = rewrit integral_pow (str2t "Integral x^^^3 D x"); term2s str;
74 "----------- test new_c ------------------------------------------";
75 "----------- test new_c ------------------------------------------";
76 "----------- test new_c ------------------------------------------";
77 val term = str2t "x^^^2*c + c_2";
79 if term2s cc = "c_3" then () else raise error "integrate.sml: new_c ???";
81 val term = str2t "new_c (c * x^^^2 + c_2)";
82 val Some (_,t') = eval_new_c 0 0 term 0;
83 if term2s t' = "new_c c * x ^^^ 2 + c_2 = c_3" then ()
84 else raise error "integrate.sml: eval_new_c ???";
86 val t = str2t "matches (?u + new_c ?v) (x ^^^ 2 / 2)";
87 val Some (_,t') = eval_matches "" "Tools.matches" t thy; term2s t';
88 if term2s t' = "matches (?u + new_c ?v) (x ^^^ 2 / 2) = False" then ()
89 else raise error "integrate.sml: matches new_c = False";
91 val t = str2t "matches (?u + new_c ?v) (x ^^^ 2 / 2 + new_c x ^^^ 2 / 2)";
92 val Some (_,t') = eval_matches "" "Tools.matches" t thy; term2s t';
93 if term2s t'="matches (?u + new_c ?v) (x ^^^ 2 / 2 + new_c x ^^^ 2 / 2) = True"
94 then () else raise error "integrate.sml: matches new_c = True";
96 val conditions_in_integration =
97 Rls {id="conditions_in_integration",
99 rew_ord = ("termlessI",termlessI),
101 srls = Erls, calc = [],
102 rules = [Calc ("Tools.matches",eval_matches ""),
103 Thm ("not_true",num_str not_true),
104 Thm ("not_false",num_str not_false)
108 fst (the (rewrite_inst_ Integrate.thy tless_true
109 conditions_in_integration true subs thm str));
110 val str = rewrit call_for_new_c (str2t "x ^^^ 2 / 2"); term2s str;
111 val str = (rewrit call_for_new_c str)
112 handle OPTION => str2t "no_rewrite";;
115 "----------- integrate by ruleset --------------------------------";
116 "----------- integrate by ruleset --------------------------------";
117 "----------- integrate by ruleset --------------------------------";
118 fun rewrite_se subs rls str =
119 fst (the (rewrite_set_inst "Integrate.thy" true subs rls str));
120 val subs = [("bdv","x::real")];
121 val rls = "integration_rules";
122 val str = rewrite_se subs rls "Integral x D x";
123 val str = rewrite_se subs rls "Integral c * x ^^^ 2 + c_2 D x";
124 if str = "c * (x ^^^ 3 / 3) + c_2 * x"
125 then () else raise error "integrate.sml: diff.behav. in integration_rules";
127 val rls = "add_new_c";
128 val str = rewrite_se subs rls "c * (x ^^^ 3 / 3) + c_2 * x";
129 if str = "c * (x ^^^ 3 / 3) + c_2 * x + c_3" then ()
130 else raise error "integrate.sml: diff.behav. in add_new_c";
132 val rls = "integration";
133 val str = rewrite_se subs rls "Integral c * x ^^^ 2 + c_2 D x";
134 if str = "c * (x ^^^ 3 / 3) + c_2 * x + c_3"
135 then () else raise error "integrate.sml: diff.behav. in integration";
138 "----------- check probem type -----------------------------------";
139 "----------- check probem type -----------------------------------";
140 "----------- check probem type -----------------------------------";
141 val model = {Given =["functionTerm f_", "integrateBy v_"],
143 Find =["antiDerivative F_"],
145 Relate=[]}:string ppc;
146 val chkmodel = ((map (the o (parse Integrate.thy))) o ppc2list) model;
147 val t1 = (term_of o hd) chkmodel;
148 val t2 = (term_of o hd o tl) chkmodel;
149 val t3 = (term_of o hd o tl o tl) chkmodel;
150 case t3 of Const ("Integrate.antiDerivative", _) $ _ => ()
151 | _ => raise error "integrate.sml: Integrate.antiDerivative ???";
153 val pbl = get_pbt ["integrate","function"];
154 case #cas pbl of Some (Const ("Integrate.Integrate",_) $ _) => ()
155 | _ => raise error "integrate.sml: Integrate.Integrate ???";
158 "----------- check Scripts ---------------------------------------";
159 "----------- check Scripts ---------------------------------------";
160 "----------- check Scripts ---------------------------------------";
162 "Script IntegrationScript (f_::real) (v_::real) = \
163 \ (let t_ = Integral f_ D v_ \
164 \ in (Rewrite_Set_Inst [(bdv,v_)] integration False) (t_::real))";
165 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
169 "Script NamedIntegrationScript (f_::real) (v_::real) (F_::real) = \
170 \ (let t_ = (F_ = Integral f_ D v_) \
171 \ in (Rewrite_Set_Inst [(bdv,v_)] integration False) t_)";
172 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
177 "----------- me method [Diff,integration] ---------------------";
178 "----------- me method [Diff,integration] ---------------------";
179 "----------- me method [Diff,integration] ---------------------";
180 val fmz = ["functionTerm (x^^^2 + 1)",
181 "integrateBy x","antiDerivative FF"];
183 ("Integrate.thy",["integrate","function"],
184 ["Diff","integration"]);
185 val p = e_pos'; val c = [];
186 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
187 val (p,_,f,nxt,_,pt) = me nxt p c pt;
188 val (p,_,f,nxt,_,pt) = me nxt p c pt;
189 val (p,_,f,nxt,_,pt) = me nxt p c pt;
190 val (p,_,f,nxt,_,pt) = me nxt p c pt;
191 val (p,_,f,nxt,_,pt) = me nxt p c pt;
192 val (p,_,f,nxt,_,pt) = me nxt p c pt;
193 val (p,_,f,nxt,_,pt) = me nxt p c pt;
194 val (p,_,f,nxt,_,pt) = me nxt p c pt;(*---> Empty_Tac*)