3 use"../smltest/IsacKnowledge/diff.sml";
7 "-----------------------------------------------------------------";
8 "table of contents -----------------------------------------------";
9 "-----------------------------------------------------------------";
10 " _________________ problemtype _________________ ";
11 "----------- for correction of diff_const ------------------------";
12 " _________________ for correction of diff_quot _________________ ";
13 " _________________ differentiate by rewrite _________________ ";
14 " ______________ differentiate: me (*+ tacs input*) ______________ ";
15 " ________________ differentiate stdin: student active________________ ";
16 " _________________ differentiate stdin: tutor active_________________ ";
17 "---------------------1.5.02 me from script ---------------------";
18 "----------- primed id -------------------------------------------";
19 "----------- diff_conv, sym_diff_conv ----------------------------";
20 "----------- autoCalculate differentiate_on_R 2/x^2 --------------";
21 "----------- autoCalculate diff after_simplification -------------";
22 "----------- autoCalculate differentiate_equality ----------------";
23 "----------- tests for examples ----------------------------------";
24 "------------inform for x^2+x+1 ----------------------------------";
25 "-----------------------------------------------------------------";
26 "-----------------------------------------------------------------";
27 "-----------------------------------------------------------------";
32 " _________________ problemtype _________________ ";
33 " _________________ problemtype _________________ ";
34 " _________________ problemtype _________________ ";
35 val pbt = {Given =["functionTerm f_f", "differentiateFor v_v"],
37 Find =["derivative f_f'"],
39 Relate=[]}:string ppc;
40 val chkpbt = ((map (the o (parse Diff.thy))) o ppc2list) pbt;
42 val org = ["functionTerm (d_d x (x ^^^ 2 + 3 * x + 4))",
43 "differentiateFor x","derivative f_f'"];
44 val chkorg = map (the o (parse Diff.thy)) org;
46 get_pbt ["derivative_of","function"];
47 get_met ["diff","differentiate_on_R"];
49 (*erls should not be in ruleset'! Here only for tests*)
54 Rls {id = "erls",preconds = [], rew_ord = ("termlessI",termlessI),
55 erls = e_rls, srls = Erls, calc = [], (*asm_thm = [],*)
56 rules = [Thm ("refl",num_str @{thm refl}),
57 Thm ("real_le_refl",num_str @{thm real_le_refl}}),
58 Thm ("radd_left_cancel_le",num_str @{thm radd_left_cancel_le}),
59 Thm ("not_true",num_str @{thm not_true}),
60 Thm ("not_false",num_str @{thm not_false}),
61 Thm ("and_true",num_str @{thm and_true}),
62 Thm ("and_false",num_str @{thm and_false}),
63 Thm ("or_true",num_str @{thm or_true}),
64 Thm ("or_false",num_str @{thm or_false}),
65 Thm ("and_commute",num_str @{and_commute}),
66 Thm ("or_commute",num_str @{or_commute}),
68 Calc ("Atools.is'_const",eval_const "#is_const_"),
69 Calc ("Atools.occurs'_in", eval_occurs_in ""),
70 Calc ("Tools.matches",eval_matches ""),
72 Calc ("Groups.plus_class.plus",eval_binop "#add_"),
73 Calc ("op *",eval_binop "#mult_"),
74 Calc ("Atools.pow" ,eval_binop "#power_"),
76 Calc ("op <",eval_equ "#less_"),
77 Calc ("op <=",eval_equ "#less_equal_"),
79 Calc ("Atools.ident",eval_ident "#ident_")],
80 scr = Script ((term_of o the o (parse thy))
85 "----------- for correction of diff_const ------------------------";
86 "----------- for correction of diff_const ------------------------";
87 "----------- for correction of diff_const ------------------------";
88 (*re-evaluate this file, otherwise > *** ME_Isa: 'erls' not known*)
90 val ct = "Not (x =!= a)";
91 rewrite_set thy' false "erls" ct;
92 val ct = "2 is_const";
93 rewrite_set thy' false "erls" ct;
95 val thm = ("diff_const","");
98 (rewrite_inst thy' "tless_true" "erls" false [("bdv","x")] thm ct);
101 (rewrite_inst thy' "tless_true" "erls" false [("bdv","x")] thm ct);
102 "----- for 'd_d s a' we got 'a is_const' --> False --------vvv-----";
103 trace_rewrite := true;
105 (rewrite_inst thy' "tless_true" "erls" false [("bdv","s")] thm ct);
106 (*got: NONE instead SOME*)
107 eval_true Isac.thy [str2term "a is_const"] (assoc_rls"erls");
108 (*got: false instead true; ~~~~~~~~~~~ replaced by 'is_atom'*)
110 (rewrite_inst thy' "tless_true" "erls" false [("bdv","s")] thm ct);
111 if ctt = "0" then () else error "diff.sml: thm 'diff_const' diff.behav.";
112 trace_rewrite := false;
113 "----- for 'd_d s a' we had 'a is_const' --> False --------^^^-----";
115 val thm = ("diff_var","");
118 (rewrite_inst thy' "tless_true" "erls" false [("bdv","x")] thm ct);
121 (rewrite_inst thy' "tless_true" "erls" false [("bdv","x")] thm ct);
122 val ct = "d_d x (x+x)";
124 (rewrite_inst thy' "tless_true" "erls" false [("bdv","x")] thm ct);
127 " _________________ for correction of diff_quot _________________ ";
128 " _________________ for correction of diff_quot _________________ ";
129 " _________________ for correction of diff_quot _________________ ";
131 val ct = "Not (x = 0)";
132 rewrite_set thy' false "erls" ct;
134 val ct = "d_d x ((x+1) / (x - 1))";
135 val thm = ("diff_quot","");
137 (rewrite_inst thy' "tless_true" "erls" true [("bdv","x")] thm ct);
145 " _________________ differentiate by rewrite _________________ ";
146 " _________________ differentiate by rewrite _________________ ";
147 " _________________ differentiate by rewrite _________________ ";
149 val ct = "d_d x (x ^^^ 2 + 3 * x + 4)";
151 val thm = ("diff_sum","");
152 val (ct,_) = the (rewrite_inst thy' "tless_true" "erls" true
153 [("bdv","x::real")] thm ct);
155 val (ct,_) = the (rewrite_inst thy' "tless_true" "erls" true
156 [("bdv","x::real")] thm ct);
158 val thm = ("diff_prod_const","");
159 val (ct,_) = the (rewrite_inst thy' "tless_true" "erls" true
160 [("bdv","x::real")] thm ct);
162 val thm = ("diff_pow","");
163 val (ct,_) = the (rewrite_inst thy' "tless_true" "erls" true
164 [("bdv","x::real")] thm ct);
166 val thm = ("diff_const","");
167 val (ct,_) = the (rewrite_inst thy' "tless_true" "erls" true
168 [("bdv","x::real")] thm ct);
170 val thm = ("diff_var","");
171 val (ct,_) = the (rewrite_inst thy' "tless_true" "erls" true
172 [("bdv","x::real")] thm ct);
173 if ct = "2 * x ^^^ (2 - 1) + 3 * 1 + 0" then ()
174 else error "diff.sml diff.behav. in rewrite 1";
176 val rls = ("Test_simplify");
177 val (ct,_) = the (rewrite_set thy' false rls ct);
178 if ct="3 + 2 * x" then () else error "new behaviour in test-example";
180 val ct = "2 * x ^^^ (2 - 1) + 3 * 1 + 0";
181 val (ct,_) = the (rewrite_set thy' true rls ct);
185 val t = str2term "x ^^^ (2 - 1)";
186 val SOME (t',_) = rewrite_set_ thy false Test_simplify t;
189 val t = str2term "-1 * 1";
190 val SOME (thmID,thm) = get_calculation_ thy (the(assoc(calclist,"times"))) t;
194 " ______________ differentiate: me (*+ tacs input*) ______________ ";
195 " ______________ differentiate: me (*+ tacs input*) ______________ ";
196 " ______________ differentiate: me (*+ tacs input*) ______________ ";
197 val fmz = ["functionTerm (x ^^^ 2 + 3 * x + 4)",
198 "differentiateFor x","derivative f_f'"];
200 ("Diff",["derivative_of","function"],
201 ["diff","diff_simpl"]);
202 val p = e_pos'; val c = [];
204 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
205 val (p,_,f,nxt,_,pt) = me nxt p c pt;
207 (*val nxt = ("Add_Given",
208 Add_Given "functionTerm (d_d x (x ^^^ #2 + #3 * x + #4))");*)
209 val (p,_,f,nxt,_,pt) = me nxt p c pt;
211 (*val nxt = ("Add_Given",Add_Given "differentiateFor x");*)
212 val (p,_,f,nxt,_,pt) = me nxt p c pt;
214 (*val nxt = ("Add_Find",Add_Find "derivative f_f'");*)
215 val (p,_,f,nxt,_,pt) = me nxt p c pt;
217 (*val nxt = ("Specify_Theory",Specify_Theory dI');*)
218 val (p,_,f,nxt,_,pt) = me nxt p c pt;
220 (*val nxt = ("Specify_Problem",Specify_Problem pI');*)
221 val (p,_,f,nxt,_,pt) = me nxt p c pt;
223 (*val nxt = ("Specify_Method",Specify_Method mI');*)
224 val (p,_,f,nxt,_,pt) = me nxt p c pt;
226 (*val nxt = ("Apply_Method",Apply_Method mI');*)
227 val (p,_,f,nxt,_,pt) = me nxt p c pt;
229 (*val nxt = ("Rewrite_Inst",Rewrite_Inst (["(bdv,x)"],("diff_sum","")));*)
230 val (p,_,f,nxt,_,pt) = me nxt p c pt;
232 (*val nxt = ("Rewrite_Inst",Rewrite_Inst (["(bdv,x)"],("diff_sum","")));*)
233 val (p,_,f,nxt,_,pt) = me nxt p c pt;
234 (*val (p,_,f,nxt,_,pt) = me nxt p c pt;
235 val (p,_,f,nxt,_,pt) = me nxt p c pt;*)
237 (*val nxt = ("Rewrite_Inst",Rewrite_Inst (["(bdv,x)"],("diff_prod_const",...;*)
238 val (p,_,f,nxt,_,pt) = me nxt p c pt;
239 (*val (p,_,f,nxt,_,pt) = me nxt p c pt;*)
241 (*val nxt = ("Rewrite_Inst",Rewrite_Inst (["(bdv,x)"],("diff_pow","")));*)
242 val (p,_,f,nxt,_,pt) = me nxt p c pt;
243 (*val (p,_,f,nxt,_,pt) = me nxt p c pt;*)
245 (*val nxt = ("Rewrite_Inst",Rewrite_Inst (["(bdv,x)"],("diff_prod_const",...;*)
246 val (p,_,f,nxt,_,pt) = me nxt p c pt;
247 (*val (p,_,f,nxt,_,pt) = me nxt p c pt;*)
249 (*val nxt = ("Rewrite_Inst",Rewrite_Inst (["(bdv,x)"],("diff_var","")));*)
250 val (p,_,f,nxt,_,pt) = me nxt p c pt;
251 if f2str f = "2 * x ^^^ (2 - 1) + 3 * 1 + 0" then ()
252 else error "diff.sml: diff.behav. in d_d x ^^^ 2 + 3 * x + 4";
254 (*------------------------------11.3.03--------------------
256 val (_,_,f,_,_,_) = me nxt p c pt;
257 val Form' (FormKF (_,_,_,_,res)) = f;
258 trace_rewrite:=false;
260 val ct = "2 * x ^^^ (2 - 1) + 3 * 1 + 0";
261 val SOME (ct',_) = rewrite_set "Isac" false "make_polynomial" ct;
266 val SOME (t',_) = rewrite_set_ Isac.thy false make_polynomial t;
268 trace_rewrite:=false;
270 val SOME (t'',_) = rewrite_set_ Isac.thy false make_polynomial t';
273 val thm = num_str @{thm realpow_eq_oneI;
274 case string_of_thm thm of
277 val Rewrite_Set' ("Diff",false,"make_polynomial",ff,(ff',[])) = m;
278 term2str ff; term2str ff';
282 --------------------------------11.3.03--------------------*)
284 (*val nxt = ("Rewrite_Set",Rewrite_Set "make_polynomial");*)
285 val (p,_,f,nxt,_,pt) = me nxt p c pt;
288 ("Check_Postcond",Check_Postcond ("Diff","differentiate_on_R"));*)
289 val (p,_,f,nxt,_,pt) = me nxt p c pt;
291 (*val nxt = ("End_Proof'",End_Proof');*)
292 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
293 if nxt = ("End_Proof'",End_Proof') andalso f2str f = "3 + 2 * x" then ()
294 else error "diff.sml: new.behav. in me (*+ tacs input*)";
295 (*if f = EmptyMout then () else error "new behaviour in + tacs input";
296 meNEW extracts Form once more*)
301 (*---------------- 1.5.02 -----------------------------------------
303 " _________________ script-eval corrected _________________ ";
304 " _________________ script-eval corrected _________________ ";
305 " _________________ script-eval corrected _________________ ";
306 val scr = Script (((inst_abs (assoc_thy "Test")) o
307 term_of o the o (parse Diff.thy))
308 "Script Differentiate (f_f::real) (v_v::real) = \
309 \(let f_ = Try (Repeat (Rewrite frac_conv False f_)); \
310 \ f_ = Try (Repeat (Rewrite root_conv False f_)); \
312 \ ((Repeat (Rewrite_Inst [(bdv,v_v)] diff_sum False f_)) Or \
313 \ (Repeat (Rewrite_Inst [(bdv,v_v)] diff_prod_const False f_)) Or \
314 \ (Repeat (Rewrite_Inst [(bdv,v_v)] diff_prod False f_)) Or \
315 \ (Repeat (Rewrite_Inst [(bdv,v_v)] diff_quot False f_)) Or \
316 \ (Repeat (Rewrite_Inst [(bdv,v_v)] diff_sin False f_)) Or \
317 \ (Repeat (Rewrite_Inst [(bdv,v_v)] diff_sin_chain False f_)) Or \
318 \ (Repeat (Rewrite_Inst [(bdv,v_v)] diff_cos False f_)) Or \
319 \ (Repeat (Rewrite_Inst [(bdv,v_v)] diff_cos_chain False f_)) Or \
320 \ (Repeat (Rewrite_Inst [(bdv,v_v)] diff_pow False f_)) Or \
321 \ (Repeat (Rewrite_Inst [(bdv,v_v)] diff_pow_chain False f_)) Or \
322 \ (Repeat (Rewrite_Inst [(bdv,v_v)] diff_ln False f_)) Or \
323 \ (Repeat (Rewrite_Inst [(bdv,v_v)] diff_ln_chain False f_)) Or \
324 \ (Repeat (Rewrite_Inst [(bdv,v_v)] diff_exp False f_)) Or \
325 \ (Repeat (Rewrite_Inst [(bdv,v_v)] diff_exp_chain False f_)) Or \
326 \ (Repeat (Rewrite_Inst [(bdv,v_v)] diff_const False f_)) Or \
327 \ (Repeat (Rewrite_Inst [(bdv,v_v)] diff_var False f_)) Or \
328 \ (Repeat (Rewrite_Set Test_simplify False f_))); \
329 \ f_ = Try (Repeat (Rewrite sym_frac_conv False f_)) \
330 \ in Try (Repeat (Rewrite sym_root_conv False f_)))");
334 ("Diff","differentiate_on_R"));
335 val p = e_pos'; val c = [];
336 val (mI,m) = ("Init_Proof",Init_Proof ([], (dI',pI',mI')));
337 val (p,_,_,_,_,pt) = me (mI,m) p c EmptyPtree;
338 val nxt = ("Specify_Theory",Specify_Theory dI');
339 val (p,_,_,_,_,pt) = me nxt p c pt;
340 val nxt = ("Specify_Method",Specify_Method mI');
341 val (p,_,_,_,_,pt) = me nxt p c pt;
342 val p = ([1],Frm):pos';
345 val parseee = (term_of o the o (parse Diff.thy));
346 val ct = "d_d x (x ^^^ #2 + #3 * x + #4)";
347 val envvv = [(parseee"f_f",parseee ct),(parseee"v_",parseee"x")];
348 val ets0=[([],(Tac'(Script.thy,"BS","",""),envvv,envvv,empty,empty,Safe)),
349 ([],(User', [], [], empty, empty,Sundef))]:ets;
351 " --------------- 1. ---------------------------------------------";
352 val (pt,_) = cappend_atomic pt[1]e_loc ct (Rewrite("test","")) ct Complete;
353 val Appl m'=applicable_in p pt (Rewrite_Inst (["(bdv,x)"],("diff_sum","")));
355 val NextStep(l1,m') = nxt_tac "Diff" (pt,p) scr ets0 l0;
357 val Steps[(Form' (FormKF (_,_,_,_,res)),pt,p,_,s,ets1)] =
358 locate_gen "Diff" m' (pt,p) (scr,d) ets0 l0;
359 val ets1 = (drop_last ets0) @ ets1;val pt = update_ets pt [] [(1,ets1)];
360 " --------------- 2. ---------------------------------------------";
361 val Appl m'=applicable_in p pt (Rewrite_Inst (["(bdv,x)"],("diff_sum","")));
362 val NextStep(l2,m') = nxt_tac "Diff" (pt,p) scr ets1 l1;
364 val Steps[(Form' (FormKF (_,_,_,_,res)),pt,p,_,s,ets2)] =
365 locate_gen "Diff" m' (pt,p) (scr,d) ets1 l1;
366 val ets2 = (drop_last ets1) @ ets2;val pt = update_ets pt [] [(1,ets2)];
367 " --------------- 3. ---------------------------------------------";
368 val Appl m'=applicable_in p pt (Rewrite_Inst (["(bdv,x)"],("diff_prod_const","")));
369 val NextStep(l3,m') = nxt_tac "Diff" (pt,p) scr ets2 l2;
370 (*("diff_prod_const","")*)
371 val Steps[(Form' (FormKF (_,_,_,_,res)),pt,p,_,s,ets3)] =
372 locate_gen "Diff" m' (pt,p) (scr,d) ets2 l2;
373 val ets3 = (drop_last ets2) @ ets3; val pt = update_ets pt [] [(1,ets3)];
374 " --------------- 4. ---------------------------------------------";
375 val Appl m'=applicable_in p pt (Rewrite_Inst (["(bdv,x)"],("diff_pow","")));
376 val NextStep(l4,m') = nxt_tac "Diff" (pt,p) scr ets3 l3;
378 val Steps[(Form' (FormKF (_,_,_,_,res)),pt,p,_,s,ets4)] =
379 locate_gen "Diff" m' (pt,p) (scr,d) ets3 l3;
380 val ets4 = (drop_last ets3) @ ets4; val pt = update_ets pt [] [(1,ets4)];
381 " --------------- 5. ---------------------------------------------";
382 val Appl m'=applicable_in p pt (Rewrite_Inst (["(bdv,x)"],("diff_const","")));
383 val NextStep(l5,m') = nxt_tac "Diff" (pt,p) scr ets4 l4;
384 (*("diff_const","")*)
385 val Steps[ (Form' (FormKF (_,_,_,_,res)),pt,p,_,s,ets5)] =
386 locate_gen "Diff" m' (pt,p) (scr,d) ets4 l4;
387 val ets5 = (drop_last ets4) @ ets5; val pt = update_ets pt [] [(1,ets5)];
388 " --------------- 6. ---------------------------------------------";
389 val Appl m'=applicable_in p pt (Rewrite_Inst (["(bdv,x)"],("diff_var","")));
390 val NextStep(l6,m') = nxt_tac "Diff" (pt,p) scr ets5 l5;
391 (*("diff_var","")ok; here was("diff_const","")because of wrong rule in *.thy*)
392 val Steps[(Form' (FormKF (_,_,_,_,res)),pt,p,_,s,ets6)] =
393 locate_gen "Diff" m' (pt,p) (scr,d) ets5 l5;
394 val ets6 = (drop_last ets5) @ ets6; val pt = update_ets pt [] [(1,ets6)];
395 " --------------- 7. ---------------------------------------------";
396 val Appl m'=applicable_in p pt (Rewrite_Set "Test_simplify");
399 ---------------- 1.5.02 -----------------------------------------*)
404 " ________________ differentiate stdin: student active________________ ";
405 " ________________ differentiate stdin: student active________________ ";
406 " ________________ differentiate stdin: student active________________ ";
408 proofs:= []; dials:=([],[],[]);
409 StdinSML 0 0 0 0 New_User;
410 set_dstate 1 test_hide 4 1;(*SelRule,St..PutRuleRes,TskipS..*)
411 StdinSML 1 0 0 0 New_Proof;
412 val fmz = ["functionTerm (d_d x (x ^^^ 2 + 3 * x + 4))",
413 "differentiateFor x","derivative f_f'"];
415 ("Diff",["derivative_of","function"],
416 ["diff","differentiate_on_R"]);
420 " _________________ differentiate stdin: tutor active_________________ ";
421 " _________________ differentiate stdin: tutor active_________________ ";
422 " _________________ differentiate stdin: tutor active_________________ ";
423 (*proofs:= []; dials:=([],[],[]);
424 StdinSML 0 0 0 0 New_User;
425 set_dstate 1 test_hide 0 2;(*PutRule,TskipS..PutRuleRes,Tt..*)
426 StdinSML 1 0 0 0 New_Proof;
427 val fmz = ["functionTerm (d_d x (x ^^^ 2 + 3 * x + 4))",
428 "differentiateFor x","derivative f_f'"];
430 ("Diff",["derivative_of","function"],
431 ["diff","differentiate_on_R"]);
435 "---------------------1.5.02 me from script ---------------------";
436 "---------------------1.5.02 me from script ---------------------";
437 "---------------------1.5.02 me from script ---------------------";
438 (*exp_Diff_No-1.xml*)
439 val fmz = ["functionTerm (x ^^^ 2 + 3 * x + 4)",
440 "differentiateFor x","derivative f_f'"];
442 ("Diff",["derivative_of","function"],
443 ["diff","diff_simpl"]);
444 (*val p = e_pos'; val c = [];
445 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
446 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
447 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
448 val (p,_,f,nxt,_,pt) = me nxt p c pt;
449 val (p,_,f,nxt,_,pt) = me nxt p c pt;
450 val (p,_,f,nxt,_,pt) = me nxt p c pt;
451 val (p,_,f,nxt,_,pt) = me nxt p c pt;
452 val (p,_,f,nxt,_,pt) = me nxt p c pt;
453 val (p,_,f,nxt,_,pt) = me nxt p c pt;
454 val (p,_,f,nxt,_,pt) = me nxt p c pt;
455 (*nxt = ("Apply_Method",Apply_Method ("Diff","differentiate_on_R*)
456 val (p,_,f,nxt,_,pt) = me nxt p c pt;
458 val (p,_,f,nxt,_,pt) = me nxt p c pt;
459 val (p,_,f,nxt,_,pt) = me nxt p c pt;
460 val (p,_,f,nxt,_,pt) = me nxt p c pt;
461 val (p,_,f,nxt,_,pt) = me nxt p c pt;
462 val (p,_,f,nxt,_,pt) = me nxt p c pt;
463 val (p,_,f,nxt,_,pt) = me nxt p c pt;
464 val (p,_,f,nxt,_,pt) = me nxt p c pt;
465 val (p,_,f,nxt,_,pt) = me nxt p c pt;
466 if nxt = ("End_Proof'",End_Proof') then ()
467 else error "new behaviour in tests/differentiate, 1.5.02 me from script";
469 "----------- primed id -------------------------------------------";
470 "----------- primed id -------------------------------------------";
471 "----------- primed id -------------------------------------------";
473 val f_ = str2term "f_f::bool";
474 val f = str2term "A = s * (a - s)";
475 val v_v = str2term "v_";
476 val v = str2term "s";
477 val screxp0 = str2term "Take ((primed (lhs f_)) = d_d v_v (rhs f_))";
480 val screxp1 = subst_atomic [(f_f, f), (v_, v)] screxp0;
484 val SOME (f'_,_) = rewrite_set_ Isac.thy false srls_diff screxp1;
485 if term2str f'_= "Take (A' = d_d s (s * (a - s)))" then ()
486 else error "diff.sml: diff.behav. in 'primed'";
489 val str = "Script DiffEqScr (f_f::bool) (v_v::real) = \
490 \ (let f_f' = Take ((primed (lhs f_)) = d_d v_v (rhs f_)) \
491 \ in (((Try (Repeat (Rewrite frac_conv False))) @@ \
492 \ (Try (Repeat (Rewrite root_conv False))) @@ \
493 \ (Try (Repeat (Rewrite realpow_pow False))) @@ \
495 \ ((Repeat (Rewrite_Inst [(bdv,v_v)] diff_sum False)) Or \
496 \ (Repeat (Rewrite_Inst [(bdv,v_v)] diff_prod_const False)) Or \
497 \ (Repeat (Rewrite_Inst [(bdv,v_v)] diff_prod False)) Or \
498 \ (Repeat (Rewrite_Inst [(bdv,v_v)] diff_quot True )) Or \
499 \ (Repeat (Rewrite_Inst [(bdv,v_v)] diff_sin False)) Or \
500 \ (Repeat (Rewrite_Inst [(bdv,v_v)] diff_sin_chain False)) Or \
501 \ (Repeat (Rewrite_Inst [(bdv,v_v)] diff_cos False)) Or \
502 \ (Repeat (Rewrite_Inst [(bdv,v_v)] diff_cos_chain False)) Or \
503 \ (Repeat (Rewrite_Inst [(bdv,v_v)] diff_pow False)) Or \
504 \ (Repeat (Rewrite_Inst [(bdv,v_v)] diff_pow_chain False)) Or \
505 \ (Repeat (Rewrite_Inst [(bdv,v_v)] diff_ln False)) Or \
506 \ (Repeat (Rewrite_Inst [(bdv,v_v)] diff_ln_chain False)) Or \
507 \ (Repeat (Rewrite_Inst [(bdv,v_v)] diff_exp False)) Or \
508 \ (Repeat (Rewrite_Inst [(bdv,v_v)] diff_exp_chain False)) Or \
509 \ (Repeat (Rewrite_Inst [(bdv,v_v)] diff_sqrt False)) Or \
510 \ (Repeat (Rewrite_Inst [(bdv,v_v)] diff_sqrt_chain False)) Or \
511 \ (Repeat (Rewrite_Inst [(bdv,v_v)] diff_const False)) Or \
512 \ (Repeat (Rewrite_Inst [(bdv,v_v)] diff_var False)) Or \
513 \ (Repeat (Rewrite_Set make_polynomial False)))) @@ \
514 \ (Try (Repeat (Rewrite sym_frac_conv False))) @@ \
515 \ (Try (Repeat (Rewrite sym_root_conv False))))) f_f')"
517 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
520 "----------- diff_conv, sym_diff_conv ----------------------------";
521 "----------- diff_conv, sym_diff_conv ----------------------------";
522 "----------- diff_conv, sym_diff_conv ----------------------------";
523 val subs = [(str2term "bdv", str2term "x")];
526 val t = str2term "2/x^^^2";
527 val SOME (t,_) = rewrite_set_inst_ thy false subs rls t; term2str t;
528 if term2str t = "2 * x ^^^ -2" then () else error "diff.sml 1/x";
530 val t = str2term "sqrt (x^^^3)";
531 val SOME (t,_) = rewrite_set_inst_ thy false subs rls t; term2str t;
532 if term2str t = "x ^^^ (3 / 2)" then () else error "diff.sml x^1/2";
534 val t = str2term "2 / sqrt x^^^3";
535 val SOME (t,_) = rewrite_set_inst_ thy false subs rls t; term2str t;
536 if term2str t = "2 * x ^^^ (-3 / 2)" then () else error"diff.sml x^-1/2";
537 (* trace_rewrite := true;
538 trace_rewrite := false;
540 val rls = diff_sym_conv;
542 val t = str2term "2 * x ^^^ -2";
543 val SOME (t,_) = rewrite_set_inst_ thy false subs rls t; term2str t;
544 if term2str t = "2 / x ^^^ 2" then () else error "diff.sml sym 1/x";
547 val t = str2term "x ^^^ (3 / 2)";
548 val SOME (t,_) = rewrite_set_inst_ thy false subs rls t; term2str t;
549 if term2str t = "sqrt (x ^^^ 3)" then () else error"diff.sml sym x^1/x";
551 val t = str2term "2 * x ^^^ (-3 / 2)";
552 val SOME (t,_) = rewrite_set_inst_ thy false subs rls t; term2str t;
553 if term2str t ="2 / sqrt (x ^^^ 3)"then()else error"diff.sml sym x^-1/x";
556 (* trace_rewrite:=true;
558 (* trace_rewrite:=false;
563 "----------- autoCalculate differentiate_on_R 2/x^2 --------------";
564 "----------- autoCalculate differentiate_on_R 2/x^2 --------------";
565 "----------- autoCalculate differentiate_on_R 2/x^2 --------------";
568 [(["functionTerm (x^2 + x+ 1/x + 2/x^2)",
569 (*"functionTerm ((x^3)^5)",*)
570 "differentiateFor x", "derivative f_f'"],
571 ("Isac", ["derivative_of","function"],
572 ["diff","differentiate_on_R"]))];
575 autoCalculate 1 CompleteCalc;
576 val ((pt,p),_) = get_calc 1; show_pt pt;
577 if p = ([], Res) andalso term2str (get_obj g_res pt (fst p)) =
578 "1 + 2 * x + -1 / x ^^^ 2 + -4 / x ^^^ 3" then ()
579 else error "diff.sml: differentiate_on_R 2/x^2 changed";
581 "-----------------------------------------------------------------";
584 [(["functionTerm (x^3 * x^5)",
585 "differentiateFor x", "derivative f_f'"],
586 ("Isac", ["derivative_of","function"],
587 ["diff","differentiate_on_R"]))];
590 (* trace_rewrite := true;
591 trace_script := true;
593 autoCalculate 1 CompleteCalc;
594 (* trace_rewrite := false;
595 trace_script := false;
597 val ((pt,p),_) = get_calc 1; show_pt pt;
599 if p = ([], Res) andalso term2str (get_obj g_res pt (fst p)) =
600 "8 * x ^^^ 7" then ()
601 else error "diff.sml: differentiate_on_R (x^3 * x^5) changed";
604 "----------- autoCalculate diff after_simplification -------------";
605 "----------- autoCalculate diff after_simplification -------------";
606 "----------- autoCalculate diff after_simplification -------------";
609 [(["functionTerm (x^3 * x^5)",
610 "differentiateFor x", "derivative f_f'"],
611 ("Isac", ["derivative_of","function"],
612 ["diff","after_simplification"]))];
615 (* trace_rewrite := true;
616 trace_script := true;
618 autoCalculate 1 CompleteCalc;
619 (* trace_rewrite := false;
620 trace_script := false;
622 val ((pt,p),_) = get_calc 1; show_pt pt;
623 if p = ([], Res) andalso term2str (get_obj g_res pt (fst p)) = "8 * x ^^^ 7"
624 then () else error "biegelinie.sml: 1st biegelin.7.27 changed";
626 "-----------------------------------------------------------------";
629 [(["functionTerm ((x^3)^5)",
630 "differentiateFor x", "derivative f_f'"],
631 ("Isac", ["derivative_of","function"],
632 ["diff","after_simplification"]))];
635 autoCalculate 1 CompleteCalc;
636 val ((pt,p),_) = get_calc 1; show_pt pt;
637 if p = ([], Res) andalso term2str (get_obj g_res pt (fst p)) = "15 * x ^^^ 14"
638 then () else error "biegelinie.sml: 1st biegelin.7.27 changed";
642 "----------- autoCalculate differentiate_equality ----------------";
643 "----------- autoCalculate differentiate_equality ----------------";
644 "----------- autoCalculate differentiate_equality ----------------";
647 [(["functionEq (A = s * (a - s))", "differentiateFor s", "derivativeEq f_f'"],
648 ("Isac", ["named","derivative_of","function"],
649 ["diff","differentiate_equality"]))];
652 autoCalculate 1 CompleteCalc;
653 val ((pt,p),_) = get_calc 1; show_pt pt;
656 "----------- tests for examples ----------------------------------";
657 "----------- tests for examples ----------------------------------";
658 "----------- tests for examples ----------------------------------";
659 "----- parse errors";
660 (*str2term "F = sqrt( y^2 - O) * (z + O^2)";
664 "----- thm 'diff_prod_const'";
665 val subs = [(str2term "bdv", str2term "l")];
666 val f = str2term "G' = d_d l (l * sqrt (7 * s ^ 2 - l ^ 2))";
668 trace_rewrite := true;
669 rewrite_inst_ Isac.thy tless_true erls_diff true subs diff_prod_const f;
670 trace_rewrite := false;
673 "------------inform for x^2+x+1 ----------------------------------";
674 "------------inform for x^2+x+1 ----------------------------------";
675 "------------inform for x^2+x+1 ----------------------------------";
678 [(["functionTerm (x^2 + x + 1)",
679 "differentiateFor x", "derivative f_f'"],
680 ("Isac", ["derivative_of","function"],
681 ["diff","differentiate_on_R"]))];
684 autoCalculate 1 CompleteCalcHead;
685 autoCalculate 1 (Step 1);
686 autoCalculate 1 (Step 1);
687 autoCalculate 1 (Step 1);
688 val ((pt,p),_) = get_calc 1; show_pt pt;
689 appendFormula 1 "2*x + d_d x x + d_d x 1";
690 val ((pt,p),_) = get_calc 1; show_pt pt;
691 if existpt' ([3], Res) pt then ()
692 else error "diff.sml: inform d_d x (x^2 + x + 1) doesnt work";