3 use"../smltest/IsacKnowledge/diff.sml";
7 "--------------------------------------------------------";
8 "--------------------------------------------------------";
9 "table of contents --------------------------------------";
10 "--------------------------------------------------------";
11 "----------- problemtype --------------------------------";
12 "----------- for correction of diff_const ---------------";
13 "----------- for correction of diff_quot ----------------";
14 "----------- differentiate by rewrite -------------------";
15 "----------- differentiate: me (*+ tacs input*) ---------";
16 "----------- 1.5.02 me from script ----------------------";
17 "----------- primed id ----------------------------------";
18 "----------- diff_conv, sym_diff_conv -------------------";
19 "----------- autoCalculate differentiate_on_R 2/x^2 -----";
20 "----------- autoCalculate diff after_simplification ----";
21 "----------- autoCalculate differentiate_equality -------";
22 "----------- tests for examples -------------------------";
23 "------------inform for x^2+x+1 -------------------------";
24 "--------------------------------------------------------";
25 "--------------------------------------------------------";
26 "--------------------------------------------------------";
29 val thy = @{theory "Diff"};
31 "----------- problemtype --------------------------------";
32 "----------- problemtype --------------------------------";
33 "----------- problemtype --------------------------------";
34 val pbt = {Given =["functionTerm f_f", "differentiateFor v_v"],
36 Find =["derivative f_f'"],
38 Relate=[]}:string ppc;
39 val chkpbt = ((map (the o (parse thy))) o ppc2list) pbt;
41 val org = ["functionTerm (d_d x (x ^^^ 2 + 3 * x + 4))",
42 "differentiateFor x","derivative f_f'"];
43 val chkorg = map (the o (parse thy)) org;
45 get_pbt ["derivative_of","function"];
46 get_met ["diff","differentiate_on_R"];
48 "----------- for correction of diff_const ---------------";
49 "----------- for correction of diff_const ---------------";
50 "----------- for correction of diff_const ---------------";
51 (*re-evaluate this file, otherwise > *** ME_Isa: 'erls' not known*)
52 val t = (Thm.term_of o the o (parse thy)) "Not (x =!= a)";
53 case rewrite_set_ thy false erls_diff t of
54 SOME (Const ("HOL.True", _), []) => ()
55 | _ => error "rewrite_set_ Not (x =!= a) changed";
57 val t =(Thm.term_of o the o (parse thy)) "2 is_const";
58 case rewrite_set_ thy false erls_diff t of
59 SOME (Const ("HOL.True", _), []) => ()
60 | _ => error "rewrite_set_ 2 is_const changed";
63 val ct = (Thm.term_of o the o (parse thy)) "d_d x x";
64 val NONE = (rewrite_inst_ thy tless_true erls_diff false subst thm ct);
66 "----------- for correction of diff_quot ----------------";
67 "----------- for correction of diff_quot ----------------";
68 "----------- for correction of diff_quot ----------------";
69 val thy = @{theory "Diff"};
70 val ct = (Thm.term_of o the o (parse thy)) "Not (x = 0)";
71 rewrite_set_ thy false erls_diff ct;
73 val ct = (Thm.term_of o the o (parse thy)) "d_d x ((x+1) / (x - 1))";
74 val thm = @{thm diff_quot};
76 (rewrite_inst_ thy tless_true erls_diff true subst thm ct);
78 "----------- differentiate by rewrite -------------------";
79 "----------- differentiate by rewrite -------------------";
80 "----------- differentiate by rewrite -------------------";
81 val thy = @{theory "Diff"};
82 val ct = (Thm.term_of o the o (parse thy)) "d_d x (x ^^^ 2 + 3 * x + 4)";
84 val thm = @{thm "diff_sum"};
85 val (ct, _) = the (rewrite_inst_ thy tless_true erls_diff true subst thm ct);
87 val (ct, _) = the (rewrite_inst_ thy tless_true erls_diff true subst thm ct);
89 val thm = @{thm "diff_prod_const"};
90 val (ct, _) = the (rewrite_inst_ thy tless_true erls_diff true subst thm ct);
92 val thm = @{thm "diff_pow"};
93 val (ct, _) = the (rewrite_inst_ thy tless_true erls_diff true subst thm ct);
95 val thm = @{thm "diff_const"};
96 val (ct, _) = the (rewrite_inst_ thy tless_true erls_diff true subst thm ct);
98 val thm = @{thm "diff_var"};
99 val (ct, _) = the (rewrite_inst_ thy tless_true erls_diff true subst thm ct);
100 if term2str ct = "2 * x ^^^ (2 - 1) + 3 * 1 + 0" then ()
101 else error "diff.sml diff.behav. in rewrite 1";
104 val rls = Test_simplify;
105 val ct = (Thm.term_of o the o (parse thy)) "2 * x ^^^ (2 - 1) + 3 * 1 + 0";
106 val (ct, _) = the (rewrite_set_ thy true rls ct);
107 if term2str ct = "3 + 2 * x" then () else error "rewrite_set_ Test_simplify 2 changed";
109 "----------- differentiate: me (*+ tacs input*) ---------";
110 "----------- differentiate: me (*+ tacs input*) ---------";
111 "----------- differentiate: me (*+ tacs input*) ---------";
112 val fmz = ["functionTerm (x ^^^ 2 + 3 * x + 4)",
113 "differentiateFor x","derivative f_f'"];
115 ("Diff",["derivative_of","function"],
116 ["diff","diff_simpl"]);
117 val p = e_pos'; val c = [];
119 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
120 val (p,_,f,nxt,_,pt) = me nxt p c pt;
122 (*val nxt = ("Add_Given",
123 Add_Given "functionTerm (d_d x (x ^^^ #2 + #3 * x + #4))");*)
124 val (p,_,f,nxt,_,pt) = me nxt p c pt;
126 (*val nxt = ("Add_Given",Add_Given "differentiateFor x");*)
127 val (p,_,f,nxt,_,pt) = me nxt p c pt;
129 (*val nxt = ("Add_Find",Add_Find "derivative f_f'");*)
130 val (p,_,f,nxt,_,pt) = me nxt p c pt;
132 (*val nxt = ("Specify_Theory",Specify_Theory dI');*)
133 val (p,_,f,nxt,_,pt) = me nxt p c pt;
135 (*val nxt = ("Specify_Problem",Specify_Problem pI');*)
136 val (p,_,f,nxt,_,pt) = me nxt p c pt;
138 (*val nxt = ("Specify_Method",Specify_Method mI');*)
139 val (p,_,f,nxt,_,pt) = me nxt p c pt;
141 (*val nxt = ("Apply_Method",Apply_Method mI');*)
142 val (p,_,f,nxt,_,pt) = me nxt p c pt;
144 (*val nxt = ("Rewrite_Inst",Rewrite_Inst (["(''bdv'',x)"],("diff_sum","")));*)
145 val (p,_,f,nxt,_,pt) = me nxt p c pt;
147 (*val nxt = ("Rewrite_Inst",Rewrite_Inst (["(''bdv'',x)"],("diff_sum","")));*)
148 val (p,_,f,nxt,_,pt) = me nxt p c pt;
149 (*val (p,_,f,nxt,_,pt) = me nxt p c pt;
150 val (p,_,f,nxt,_,pt) = me nxt p c pt;*)
152 (*val nxt = ("Rewrite_Inst",Rewrite_Inst (["(''bdv'',x)"],("diff_prod_const",...;*)
153 val (p,_,f,nxt,_,pt) = me nxt p c pt;
154 (*val (p,_,f,nxt,_,pt) = me nxt p c pt;*)
156 (*val nxt = ("Rewrite_Inst",Rewrite_Inst (["(''bdv'',x)"],("diff_pow","")));*)
157 val (p,_,f,nxt,_,pt) = me nxt p c pt;
158 (*val (p,_,f,nxt,_,pt) = me nxt p c pt;*)
160 (*val nxt = ("Rewrite_Inst",Rewrite_Inst (["(''bdv'',x)"],("diff_prod_const",...;*)
161 val (p,_,f,nxt,_,pt) = me nxt p c pt;
162 (*val (p,_,f,nxt,_,pt) = me nxt p c pt;*)
164 (*val nxt = ("Rewrite_Inst",Rewrite_Inst (["(''bdv'',x)"],("diff_var","")));*)
165 val (p,_,f,nxt,_,pt) = me nxt p c pt;
166 if f2str f = "2 * x ^^^ (2 - 1) + 3 * 1 + 0" then ()
167 else error "diff.sml: diff.behav. in d_d x ^^^ 2 + 3 * x + 4";
169 (*val nxt = ("Rewrite_Set",Rewrite_Set "make_polynomial");*)
170 val (p,_,f,nxt,_,pt) = me nxt p c pt;
172 (*val nxt = ("Check_Postcond",Check_Postcond ("Diff","differentiate_on_R"));*)
173 val (p,_,f,nxt,_,pt) = me nxt p c pt;
175 (*val nxt = ("End_Proof'",End_Proof');*)
176 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
177 if f2str f = "3 + 2 * x"
178 then case nxt of ("End_Proof'", End_Proof') => ()
179 | _ => error "diff.sml: new.behav. in me (*+ tacs input*) 1"
180 else error "diff.sml: new.behav. in me (*+ tacs input*) 2";
181 (*if f = EmptyMout then () else error "new behaviour in + tacs input";
182 meNEW extracts Form once more*)
184 "----------- 1.5.02 me from script ----------------------";
185 "----------- 1.5.02 me from script ----------------------";
186 "----------- 1.5.02 me from script ----------------------";
187 (*exp_Diff_No-1.xml*)
188 val fmz = ["functionTerm (x ^^^ 2 + 3 * x + 4)",
189 "differentiateFor x","derivative f_f'"];
191 ("Diff",["derivative_of","function"],
192 ["diff","diff_simpl"]);
193 (*val p = e_pos'; val c = [];
194 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
195 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
196 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
197 val (p,_,f,nxt,_,pt) = me nxt p c pt;
198 val (p,_,f,nxt,_,pt) = me nxt p c pt;
199 val (p,_,f,nxt,_,pt) = me nxt p c pt;
200 val (p,_,f,nxt,_,pt) = me nxt p c pt;
201 val (p,_,f,nxt,_,pt) = me nxt p c pt;
202 val (p,_,f,nxt,_,pt) = me nxt p c pt;
203 val (p,_,f,nxt,_,pt) = me nxt p c pt;
204 (*nxt = ("Apply_Method",Apply_Method ("Diff","differentiate_on_R*)
205 val (p,_,f,nxt,_,pt) = me nxt p c pt;
207 val (p,_,f,nxt,_,pt) = me nxt p c pt;
208 val (p,_,f,nxt,_,pt) = me nxt p c pt;
209 val (p,_,f,nxt,_,pt) = me nxt p c pt;
210 val (p,_,f,nxt,_,pt) = me nxt p c pt;
211 val (p,_,f,nxt,_,pt) = me nxt p c pt;
212 val (p,_,f,nxt,_,pt) = me nxt p c pt;
213 val (p,_,f,nxt,_,pt) = me nxt p c pt;
214 val (p,_,f,nxt,_,pt) = me nxt p c pt;
215 case nxt of ("End_Proof'",End_Proof') => ()
216 | _ => error "new behaviour in tests/differentiate, 1.5.02 me from script";
218 "----------- primed id ----------------------------------";
219 "----------- primed id ----------------------------------";
220 "----------- primed id ----------------------------------";
221 val f_ = str2term "f_f::bool";
222 val f = str2term "A = s * (a - s)";
223 val v_ = str2term "v_v";
224 val v = str2term "s";
225 val screxp0 = str2term "Take ((primed (lhs f_f)) = d_d v_v (rhs f_f))";
228 val screxp1 = subst_atomic [(f_, f), (v_, v)] screxp0;
232 val SOME (f'_,_) = rewrite_set_ (@{theory "Isac_Knowledge"}) false srls_diff screxp1;
233 if term2str f'_= "Take (A' = d_d s (s * (a - s)))" then ()
234 else error "diff.sml: diff.behav. in 'primed'";
237 val str = "Program DiffEqScr (f_f::bool) (v_v::real) = \
238 \ (let f_f' = Take ((primed (lhs f_f)) = d_d v_v (rhs f_f)) \
239 \ in (((Try (Repeat (Rewrite frac_conv))) @@ \
240 \ (Try (Repeat (Rewrite root_conv))) @@ \
241 \ (Try (Repeat (Rewrite realpow_pow))) @@ \
243 \ ((Repeat (Rewrite_Inst [(''bdv'',v_v)] diff_sum )) Or \
244 \ (Repeat (Rewrite_Inst [(''bdv'',v_v)] diff_prod_const )) Or \
245 \ (Repeat (Rewrite_Inst [(''bdv'',v_v)] diff_prod )) Or \
246 \ (Repeat (Rewrite_Inst [(''bdv'',v_v)] diff_quot )) Or \
247 \ (Repeat (Rewrite_Inst [(''bdv'',v_v)] diff_sin )) Or \
248 \ (Repeat (Rewrite_Inst [(''bdv'',v_v)] diff_sin_chain )) Or \
249 \ (Repeat (Rewrite_Inst [(''bdv'',v_v)] diff_cos )) Or \
250 \ (Repeat (Rewrite_Inst [(''bdv'',v_v)] diff_cos_chain )) Or \
251 \ (Repeat (Rewrite_Inst [(''bdv'',v_v)] diff_pow )) Or \
252 \ (Repeat (Rewrite_Inst [(''bdv'',v_v)] diff_pow_chain )) Or \
253 \ (Repeat (Rewrite_Inst [(''bdv'',v_v)] diff_ln )) Or \
254 \ (Repeat (Rewrite_Inst [(''bdv'',v_v)] diff_ln_chain )) Or \
255 \ (Repeat (Rewrite_Inst [(''bdv'',v_v)] diff_exp )) Or \
256 \ (Repeat (Rewrite_Inst [(''bdv'',v_v)] diff_exp_chain )) Or \
257 \ (Repeat (Rewrite_Inst [(''bdv'',v_v)] diff_sqrt )) Or \
258 \ (Repeat (Rewrite_Inst [(''bdv'',v_v)] diff_sqrt_chain )) Or \
259 \ (Repeat (Rewrite_Inst [(''bdv'',v_v)] diff_const )) Or \
260 \ (Repeat (Rewrite_Inst [(''bdv'',v_v)] diff_var )) Or \
261 \ (Repeat (Rewrite_Set make_polynomial)))) @@ \
262 \ (Try (Repeat (Rewrite sym_frac_conv))) @@ \
263 \ (Try (Repeat (Rewrite sym_root_conv))))) f_f')"
265 val sc = (inst_abs o Thm.term_of o the o (parse thy)) str;
268 "----------- diff_conv, sym_diff_conv -------------------";
269 "----------- diff_conv, sym_diff_conv -------------------";
270 "----------- diff_conv, sym_diff_conv -------------------";
271 val subs = [(str2term "bdv", str2term "x")];
274 val t = str2term "2/x^^^2";
275 val SOME (t,_) = rewrite_set_inst_ thy false subs rls t; term2str t;
276 if term2str t = "2 * x ^^^ -2" then () else error "diff.sml 1/x";
278 val t = str2term "sqrt (x^^^3)";
279 val SOME (t,_) = rewrite_set_inst_ thy false subs rls t; term2str t;
280 if term2str t = "x ^^^ (3 / 2)" then () else error "diff.sml x^1/2";
282 val t = str2term "2 / sqrt x^^^3";
283 val SOME (t,_) = rewrite_set_inst_ thy false subs rls t; term2str t;
284 if term2str t = "2 * x ^^^ (-3 / 2)" then () else error"diff.sml x^-1/2";
285 val rls = diff_sym_conv;
287 val t = str2term "2 * x ^^^ -2";
288 val SOME (t,_) = rewrite_set_inst_ thy false subs rls t; term2str t;
289 if term2str t = "2 / x ^^^ 2" then () else error "diff.sml sym 1/x";
292 val t = str2term "x ^^^ (3 / 2)";
293 val SOME (t,_) = rewrite_set_inst_ thy false subs rls t; term2str t;
294 if term2str t = "sqrt (x ^^^ 3)" then () else error"diff.sml sym x^1/x";
296 val t = str2term "2 * x ^^^ (-3 / 2)";
297 val SOME (t,_) = rewrite_set_inst_ thy false subs rls t; term2str t;
298 if term2str t ="2 / sqrt (x ^^^ 3)"then()else error"diff.sml sym x^-1/x";
301 "----------- autoCalculate differentiate_on_R 2/x^2 -----";
302 "----------- autoCalculate differentiate_on_R 2/x^2 -----";
303 "----------- autoCalculate differentiate_on_R 2/x^2 -----";
306 [(["functionTerm (x^2 + x+ 1/x + 2/x^2)",
307 (*"functionTerm ((x^3)^5)",*)
308 "differentiateFor x", "derivative f_f'"],
309 ("Isac_Knowledge", ["derivative_of","function"],
310 ["diff","differentiate_on_R"]))];
313 autoCalculate 1 CompleteCalc;
314 val ((pt,p),_) = get_calc 1; show_pt pt;
315 if p = ([], Res) andalso term2str (get_obj g_res pt (fst p)) =
316 "1 + 2 * x + -1 / x ^^^ 2 + -4 / x ^^^ 3" then ()
317 else error "diff.sml: differentiate_on_R 2/x^2 changed";
319 "---------------------------------------------------------";
322 [(["functionTerm (x^3 * x^5)",
323 "differentiateFor x", "derivative f_f'"],
324 ("Isac_Knowledge", ["derivative_of","function"],
325 ["diff","differentiate_on_R"]))];
328 autoCalculate 1 CompleteCalc;
329 (* trace_rewrite := true;
330 trace_script := false;
332 val ((pt,p),_) = get_calc 1; show_pt pt;
334 if p = ([], Res) andalso term2str (get_obj g_res pt (fst p)) =
335 "8 * x ^^^ 7" then ()
336 else error "diff.sml: differentiate_on_R (x^3 * x^5) changed";
338 "----------- autoCalculate diff after_simplification ----";
339 "----------- autoCalculate diff after_simplification ----";
340 "----------- autoCalculate diff after_simplification ----";
343 [(["functionTerm (x^3 * x^5)",
344 "differentiateFor x", "derivative f_f'"],
345 ("Isac_Knowledge", ["derivative_of","function"],
346 ["diff","after_simplification"]))];
349 (* trace_rewrite := true;
350 trace_script := true;
352 autoCalculate 1 CompleteCalc;
353 (* trace_rewrite := false;
354 trace_script := false;
356 val ((pt,p),_) = get_calc 1; show_pt pt;
357 if p = ([], Res) andalso term2str (get_obj g_res pt (fst p)) = "8 * x ^^^ 7"
358 then () else error "biegelinie.sml: 1st biegelin.7.27 changed";
360 "--------------------------------------------------------";
363 [(["functionTerm ((x^3)^5)",
364 "differentiateFor x", "derivative f_f'"],
365 ("Isac_Knowledge", ["derivative_of","function"],
366 ["diff","after_simplification"]))];
369 autoCalculate 1 CompleteCalc;
370 val ((pt,p),_) = get_calc 1; show_pt pt;
371 if p = ([], Res) andalso term2str (get_obj g_res pt (fst p)) = "15 * x ^^^ 14"
372 then () else error "biegelinie.sml: 1st biegelin.7.27 changed";
374 "----------- autoCalculate differentiate_equality -------";
375 "----------- autoCalculate differentiate_equality -------";
376 "----------- autoCalculate differentiate_equality -------";
379 [(["functionEq (A = s * (a - (s::real)))", "differentiateFor s", "derivativeEq f_f'"],
380 ("Isac_Knowledge", ["named","derivative_of","function"],
381 ["diff","differentiate_equality"]))];
384 autoCalculate 1 CompleteCalc;
385 val ((pt,p),_) = get_calc 1; show_pt pt;
387 "----------- tests for examples -------------------------";
388 "----------- tests for examples -------------------------";
389 "----------- tests for examples -------------------------";
390 "----- parse errors";
391 (*str2term "F = sqrt( y^^^2 - O) * (z + O^^^2)";
393 str2term "OO"; ---errors*)
396 "----- thm 'diff_prod_const'";
397 val subs = [(str2term "bdv", str2term "l")];
398 val f = str2term "G' = d_d l (l * sqrt (7 * s ^^^ 2 - l ^^^ 2))";
400 "------------inform for x^2+x+1 -------------------------";
401 "------------inform for x^2+x+1 -------------------------";
402 "------------inform for x^2+x+1 -------------------------";
405 [(["functionTerm (x^2 + x + 1)",
406 "differentiateFor x", "derivative f_f'"],
407 ("Isac_Knowledge", ["derivative_of","function"],
408 ["diff","differentiate_on_R"]))];
411 autoCalculate 1 CompleteCalcHead;
412 autoCalculate 1 (Step 1);
413 autoCalculate 1 (Step 1);
414 autoCalculate 1 (Step 1);
415 val ((pt,p),_) = get_calc 1; show_pt pt;
416 appendFormula 1 "2*x + d_d x x + d_d x 1" (*|> Future.join*);
417 val ((pt,p),_) = get_calc 1; show_pt pt;
418 if existpt' ([3], Res) pt then ()
419 else error "diff.sml: inform d_d x (x^2 + x + 1) doesnt work";