30 val thy = Diff.thy; |
30 val thy = Diff.thy; |
31 |
31 |
32 " _________________ problemtype _________________ "; |
32 " _________________ problemtype _________________ "; |
33 " _________________ problemtype _________________ "; |
33 " _________________ problemtype _________________ "; |
34 " _________________ problemtype _________________ "; |
34 " _________________ problemtype _________________ "; |
35 val pbt = {Given =["functionTerm f_", "differentiateFor v_v"], |
35 val pbt = {Given =["functionTerm f_f", "differentiateFor v_v"], |
36 Where =[], |
36 Where =[], |
37 Find =["derivative f_'_"], |
37 Find =["derivative f_f'"], |
38 With =[], |
38 With =[], |
39 Relate=[]}:string ppc; |
39 Relate=[]}:string ppc; |
40 val chkpbt = ((map (the o (parse Diff.thy))) o ppc2list) pbt; |
40 val chkpbt = ((map (the o (parse Diff.thy))) o ppc2list) pbt; |
41 |
41 |
42 val org = ["functionTerm (d_d x (x ^^^ 2 + 3 * x + 4))", |
42 val org = ["functionTerm (d_d x (x ^^^ 2 + 3 * x + 4))", |
43 "differentiateFor x","derivative f_'_"]; |
43 "differentiateFor x","derivative f_f'"]; |
44 val chkorg = map (the o (parse Diff.thy)) org; |
44 val chkorg = map (the o (parse Diff.thy)) org; |
45 |
45 |
46 get_pbt ["derivative_of","function"]; |
46 get_pbt ["derivative_of","function"]; |
47 get_met ["diff","differentiate_on_R"]; |
47 get_met ["diff","differentiate_on_R"]; |
48 |
48 |
193 |
193 |
194 " ______________ differentiate: me (*+ tacs input*) ______________ "; |
194 " ______________ differentiate: me (*+ tacs input*) ______________ "; |
195 " ______________ differentiate: me (*+ tacs input*) ______________ "; |
195 " ______________ differentiate: me (*+ tacs input*) ______________ "; |
196 " ______________ differentiate: me (*+ tacs input*) ______________ "; |
196 " ______________ differentiate: me (*+ tacs input*) ______________ "; |
197 val fmz = ["functionTerm (x ^^^ 2 + 3 * x + 4)", |
197 val fmz = ["functionTerm (x ^^^ 2 + 3 * x + 4)", |
198 "differentiateFor x","derivative f_'_"]; |
198 "differentiateFor x","derivative f_f'"]; |
199 val (dI',pI',mI') = |
199 val (dI',pI',mI') = |
200 ("Diff",["derivative_of","function"], |
200 ("Diff",["derivative_of","function"], |
201 ["diff","diff_simpl"]); |
201 ["diff","diff_simpl"]); |
202 val p = e_pos'; val c = []; |
202 val p = e_pos'; val c = []; |
203 "--- s1 ---"; |
203 "--- s1 ---"; |
209 val (p,_,f,nxt,_,pt) = me nxt p c pt; |
209 val (p,_,f,nxt,_,pt) = me nxt p c pt; |
210 "--- s3 ---"; |
210 "--- s3 ---"; |
211 (*val nxt = ("Add_Given",Add_Given "differentiateFor x");*) |
211 (*val nxt = ("Add_Given",Add_Given "differentiateFor x");*) |
212 val (p,_,f,nxt,_,pt) = me nxt p c pt; |
212 val (p,_,f,nxt,_,pt) = me nxt p c pt; |
213 "--- s4 ---"; |
213 "--- s4 ---"; |
214 (*val nxt = ("Add_Find",Add_Find "derivative f_'_");*) |
214 (*val nxt = ("Add_Find",Add_Find "derivative f_f'");*) |
215 val (p,_,f,nxt,_,pt) = me nxt p c pt; |
215 val (p,_,f,nxt,_,pt) = me nxt p c pt; |
216 "--- s5 ---"; |
216 "--- s5 ---"; |
217 (*val nxt = ("Specify_Theory",Specify_Theory dI');*) |
217 (*val nxt = ("Specify_Theory",Specify_Theory dI');*) |
218 val (p,_,f,nxt,_,pt) = me nxt p c pt; |
218 val (p,_,f,nxt,_,pt) = me nxt p c pt; |
219 "--- s6 ---"; |
219 "--- s6 ---"; |
303 " _________________ script-eval corrected _________________ "; |
303 " _________________ script-eval corrected _________________ "; |
304 " _________________ script-eval corrected _________________ "; |
304 " _________________ script-eval corrected _________________ "; |
305 " _________________ script-eval corrected _________________ "; |
305 " _________________ script-eval corrected _________________ "; |
306 val scr = Script (((inst_abs (assoc_thy "Test")) o |
306 val scr = Script (((inst_abs (assoc_thy "Test")) o |
307 term_of o the o (parse Diff.thy)) |
307 term_of o the o (parse Diff.thy)) |
308 "Script Differentiate (f_::real) (v_v::real) = \ |
308 "Script Differentiate (f_f::real) (v_v::real) = \ |
309 \(let f_ = Try (Repeat (Rewrite frac_conv False f_)); \ |
309 \(let f_ = Try (Repeat (Rewrite frac_conv False f_)); \ |
310 \ f_ = Try (Repeat (Rewrite root_conv False f_)); \ |
310 \ f_ = Try (Repeat (Rewrite root_conv False f_)); \ |
311 \ f_ = Repeat \ |
311 \ f_ = Repeat \ |
312 \ ((Repeat (Rewrite_Inst [(bdv,v_v)] diff_sum False f_)) Or \ |
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 \ |
313 \ (Repeat (Rewrite_Inst [(bdv,v_v)] diff_prod_const False f_)) Or \ |
342 val p = ([1],Frm):pos'; |
342 val p = ([1],Frm):pos'; |
343 |
343 |
344 |
344 |
345 val parseee = (term_of o the o (parse Diff.thy)); |
345 val parseee = (term_of o the o (parse Diff.thy)); |
346 val ct = "d_d x (x ^^^ #2 + #3 * x + #4)"; |
346 val ct = "d_d x (x ^^^ #2 + #3 * x + #4)"; |
347 val envvv = [(parseee"f_",parseee ct),(parseee"v_",parseee"x")]; |
347 val envvv = [(parseee"f_f",parseee ct),(parseee"v_",parseee"x")]; |
348 val ets0=[([],(Tac'(Script.thy,"BS","",""),envvv,envvv,empty,empty,Safe)), |
348 val ets0=[([],(Tac'(Script.thy,"BS","",""),envvv,envvv,empty,empty,Safe)), |
349 ([],(User', [], [], empty, empty,Sundef))]:ets; |
349 ([],(User', [], [], empty, empty,Sundef))]:ets; |
350 val l0 = []; |
350 val l0 = []; |
351 " --------------- 1. ---------------------------------------------"; |
351 " --------------- 1. ---------------------------------------------"; |
352 val (pt,_) = cappend_atomic pt[1]e_loc ct (Rewrite("test","")) ct Complete; |
352 val (pt,_) = cappend_atomic pt[1]e_loc ct (Rewrite("test","")) ct Complete; |
408 proofs:= []; dials:=([],[],[]); |
408 proofs:= []; dials:=([],[],[]); |
409 StdinSML 0 0 0 0 New_User; |
409 StdinSML 0 0 0 0 New_User; |
410 set_dstate 1 test_hide 4 1;(*SelRule,St..PutRuleRes,TskipS..*) |
410 set_dstate 1 test_hide 4 1;(*SelRule,St..PutRuleRes,TskipS..*) |
411 StdinSML 1 0 0 0 New_Proof; |
411 StdinSML 1 0 0 0 New_Proof; |
412 val fmz = ["functionTerm (d_d x (x ^^^ 2 + 3 * x + 4))", |
412 val fmz = ["functionTerm (d_d x (x ^^^ 2 + 3 * x + 4))", |
413 "differentiateFor x","derivative f_'_"]; |
413 "differentiateFor x","derivative f_f'"]; |
414 val (dI',pI',mI') = |
414 val (dI',pI',mI') = |
415 ("Diff",["derivative_of","function"], |
415 ("Diff",["derivative_of","function"], |
416 ["diff","differentiate_on_R"]); |
416 ["diff","differentiate_on_R"]); |
417 *) |
417 *) |
418 |
418 |
423 (*proofs:= []; dials:=([],[],[]); |
423 (*proofs:= []; dials:=([],[],[]); |
424 StdinSML 0 0 0 0 New_User; |
424 StdinSML 0 0 0 0 New_User; |
425 set_dstate 1 test_hide 0 2;(*PutRule,TskipS..PutRuleRes,Tt..*) |
425 set_dstate 1 test_hide 0 2;(*PutRule,TskipS..PutRuleRes,Tt..*) |
426 StdinSML 1 0 0 0 New_Proof; |
426 StdinSML 1 0 0 0 New_Proof; |
427 val fmz = ["functionTerm (d_d x (x ^^^ 2 + 3 * x + 4))", |
427 val fmz = ["functionTerm (d_d x (x ^^^ 2 + 3 * x + 4))", |
428 "differentiateFor x","derivative f_'_"]; |
428 "differentiateFor x","derivative f_f'"]; |
429 val (dI',pI',mI') = |
429 val (dI',pI',mI') = |
430 ("Diff",["derivative_of","function"], |
430 ("Diff",["derivative_of","function"], |
431 ["diff","differentiate_on_R"]); |
431 ["diff","differentiate_on_R"]); |
432 *) |
432 *) |
433 |
433 |
435 "---------------------1.5.02 me from script ---------------------"; |
435 "---------------------1.5.02 me from script ---------------------"; |
436 "---------------------1.5.02 me from script ---------------------"; |
436 "---------------------1.5.02 me from script ---------------------"; |
437 "---------------------1.5.02 me from script ---------------------"; |
437 "---------------------1.5.02 me from script ---------------------"; |
438 (*exp_Diff_No-1.xml*) |
438 (*exp_Diff_No-1.xml*) |
439 val fmz = ["functionTerm (x ^^^ 2 + 3 * x + 4)", |
439 val fmz = ["functionTerm (x ^^^ 2 + 3 * x + 4)", |
440 "differentiateFor x","derivative f_'_"]; |
440 "differentiateFor x","derivative f_f'"]; |
441 val (dI',pI',mI') = |
441 val (dI',pI',mI') = |
442 ("Diff",["derivative_of","function"], |
442 ("Diff",["derivative_of","function"], |
443 ["diff","diff_simpl"]); |
443 ["diff","diff_simpl"]); |
444 (*val p = e_pos'; val c = []; |
444 (*val p = e_pos'; val c = []; |
445 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI'))); |
445 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI'))); |
468 |
468 |
469 "----------- primed id -------------------------------------------"; |
469 "----------- primed id -------------------------------------------"; |
470 "----------- primed id -------------------------------------------"; |
470 "----------- primed id -------------------------------------------"; |
471 "----------- primed id -------------------------------------------"; |
471 "----------- primed id -------------------------------------------"; |
472 |
472 |
473 val f_ = str2term "f_::bool"; |
473 val f_ = str2term "f_f::bool"; |
474 val f = str2term "A = s * (a - s)"; |
474 val f = str2term "A = s * (a - s)"; |
475 val v_v = str2term "v_"; |
475 val v_v = str2term "v_"; |
476 val v = str2term "s"; |
476 val v = str2term "s"; |
477 val screxp0 = str2term "Take ((primed (lhs f_)) = d_d v_v (rhs f_))"; |
477 val screxp0 = str2term "Take ((primed (lhs f_)) = d_d v_v (rhs f_))"; |
478 atomty screxp0; |
478 atomty screxp0; |
479 |
479 |
480 val screxp1 = subst_atomic [(f_, f), (v_, v)] screxp0; |
480 val screxp1 = subst_atomic [(f_f, f), (v_, v)] screxp0; |
481 term2str screxp1; |
481 term2str screxp1; |
482 atomty screxp1; |
482 atomty screxp1; |
483 |
483 |
484 val SOME (f'_,_) = rewrite_set_ Isac.thy false srls_diff screxp1; |
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 () |
485 if term2str f'_= "Take (A' = d_d s (s * (a - s)))" then () |
486 else raise error "diff.sml: diff.behav. in 'primed'"; |
486 else raise error "diff.sml: diff.behav. in 'primed'"; |
487 atomty f'_; |
487 atomty f'_; |
488 |
488 |
489 val str = "Script DiffEqScr (f_::bool) (v_v::real) = \ |
489 val str = "Script DiffEqScr (f_f::bool) (v_v::real) = \ |
490 \ (let f'_ = Take ((primed (lhs f_)) = d_d v_v (rhs f_)) \ |
490 \ (let f_f' = Take ((primed (lhs f_)) = d_d v_v (rhs f_)) \ |
491 \ in (((Try (Repeat (Rewrite frac_conv False))) @@ \ |
491 \ in (((Try (Repeat (Rewrite frac_conv False))) @@ \ |
492 \ (Try (Repeat (Rewrite root_conv False))) @@ \ |
492 \ (Try (Repeat (Rewrite root_conv False))) @@ \ |
493 \ (Try (Repeat (Rewrite realpow_pow False))) @@ \ |
493 \ (Try (Repeat (Rewrite realpow_pow False))) @@ \ |
494 \ (Repeat \ |
494 \ (Repeat \ |
495 \ ((Repeat (Rewrite_Inst [(bdv,v_v)] diff_sum False)) Or \ |
495 \ ((Repeat (Rewrite_Inst [(bdv,v_v)] diff_sum False)) Or \ |
510 \ (Repeat (Rewrite_Inst [(bdv,v_v)] diff_sqrt_chain 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 \ |
511 \ (Repeat (Rewrite_Inst [(bdv,v_v)] diff_const False)) Or \ |
512 \ (Repeat (Rewrite_Inst [(bdv,v_v)] diff_var False)) Or \ |
512 \ (Repeat (Rewrite_Inst [(bdv,v_v)] diff_var False)) Or \ |
513 \ (Repeat (Rewrite_Set make_polynomial False)))) @@ \ |
513 \ (Repeat (Rewrite_Set make_polynomial False)))) @@ \ |
514 \ (Try (Repeat (Rewrite sym_frac_conv False))) @@ \ |
514 \ (Try (Repeat (Rewrite sym_frac_conv False))) @@ \ |
515 \ (Try (Repeat (Rewrite sym_root_conv False))))) f'_)" |
515 \ (Try (Repeat (Rewrite sym_root_conv False))))) f_f')" |
516 ; |
516 ; |
517 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str; |
517 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str; |
518 |
518 |
519 |
519 |
520 "----------- diff_conv, sym_diff_conv ----------------------------"; |
520 "----------- diff_conv, sym_diff_conv ----------------------------"; |
565 "----------- autoCalculate differentiate_on_R 2/x^2 --------------"; |
565 "----------- autoCalculate differentiate_on_R 2/x^2 --------------"; |
566 states:=[]; |
566 states:=[]; |
567 CalcTree |
567 CalcTree |
568 [(["functionTerm (x^2 + x+ 1/x + 2/x^2)", |
568 [(["functionTerm (x^2 + x+ 1/x + 2/x^2)", |
569 (*"functionTerm ((x^3)^5)",*) |
569 (*"functionTerm ((x^3)^5)",*) |
570 "differentiateFor x", "derivative f_'_"], |
570 "differentiateFor x", "derivative f_f'"], |
571 ("Isac", ["derivative_of","function"], |
571 ("Isac", ["derivative_of","function"], |
572 ["diff","differentiate_on_R"]))]; |
572 ["diff","differentiate_on_R"]))]; |
573 Iterator 1; |
573 Iterator 1; |
574 moveActiveRoot 1; |
574 moveActiveRoot 1; |
575 autoCalculate 1 CompleteCalc; |
575 autoCalculate 1 CompleteCalc; |
580 |
580 |
581 "-----------------------------------------------------------------"; |
581 "-----------------------------------------------------------------"; |
582 states:=[]; |
582 states:=[]; |
583 CalcTree |
583 CalcTree |
584 [(["functionTerm (x^3 * x^5)", |
584 [(["functionTerm (x^3 * x^5)", |
585 "differentiateFor x", "derivative f_'_"], |
585 "differentiateFor x", "derivative f_f'"], |
586 ("Isac", ["derivative_of","function"], |
586 ("Isac", ["derivative_of","function"], |
587 ["diff","differentiate_on_R"]))]; |
587 ["diff","differentiate_on_R"]))]; |
588 Iterator 1; |
588 Iterator 1; |
589 moveActiveRoot 1; |
589 moveActiveRoot 1; |
590 (* trace_rewrite := true; |
590 (* trace_rewrite := true; |
605 "----------- autoCalculate diff after_simplification -------------"; |
605 "----------- autoCalculate diff after_simplification -------------"; |
606 "----------- autoCalculate diff after_simplification -------------"; |
606 "----------- autoCalculate diff after_simplification -------------"; |
607 states:=[]; |
607 states:=[]; |
608 CalcTree |
608 CalcTree |
609 [(["functionTerm (x^3 * x^5)", |
609 [(["functionTerm (x^3 * x^5)", |
610 "differentiateFor x", "derivative f_'_"], |
610 "differentiateFor x", "derivative f_f'"], |
611 ("Isac", ["derivative_of","function"], |
611 ("Isac", ["derivative_of","function"], |
612 ["diff","after_simplification"]))]; |
612 ["diff","after_simplification"]))]; |
613 Iterator 1; |
613 Iterator 1; |
614 moveActiveRoot 1; |
614 moveActiveRoot 1; |
615 (* trace_rewrite := true; |
615 (* trace_rewrite := true; |
625 |
625 |
626 "-----------------------------------------------------------------"; |
626 "-----------------------------------------------------------------"; |
627 states:=[]; |
627 states:=[]; |
628 CalcTree |
628 CalcTree |
629 [(["functionTerm ((x^3)^5)", |
629 [(["functionTerm ((x^3)^5)", |
630 "differentiateFor x", "derivative f_'_"], |
630 "differentiateFor x", "derivative f_f'"], |
631 ("Isac", ["derivative_of","function"], |
631 ("Isac", ["derivative_of","function"], |
632 ["diff","after_simplification"]))]; |
632 ["diff","after_simplification"]))]; |
633 Iterator 1; |
633 Iterator 1; |
634 moveActiveRoot 1; |
634 moveActiveRoot 1; |
635 autoCalculate 1 CompleteCalc; |
635 autoCalculate 1 CompleteCalc; |
642 "----------- autoCalculate differentiate_equality ----------------"; |
642 "----------- autoCalculate differentiate_equality ----------------"; |
643 "----------- autoCalculate differentiate_equality ----------------"; |
643 "----------- autoCalculate differentiate_equality ----------------"; |
644 "----------- autoCalculate differentiate_equality ----------------"; |
644 "----------- autoCalculate differentiate_equality ----------------"; |
645 states:=[]; |
645 states:=[]; |
646 CalcTree |
646 CalcTree |
647 [(["functionEq (A = s * (a - s))", "differentiateFor s", "derivativeEq f_'_"], |
647 [(["functionEq (A = s * (a - s))", "differentiateFor s", "derivativeEq f_f'"], |
648 ("Isac", ["named","derivative_of","function"], |
648 ("Isac", ["named","derivative_of","function"], |
649 ["diff","differentiate_equality"]))]; |
649 ["diff","differentiate_equality"]))]; |
650 Iterator 1; |
650 Iterator 1; |
651 moveActiveRoot 1; |
651 moveActiveRoot 1; |
652 autoCalculate 1 CompleteCalc; |
652 autoCalculate 1 CompleteCalc; |
674 "------------inform for x^2+x+1 ----------------------------------"; |
674 "------------inform for x^2+x+1 ----------------------------------"; |
675 "------------inform for x^2+x+1 ----------------------------------"; |
675 "------------inform for x^2+x+1 ----------------------------------"; |
676 states:=[]; |
676 states:=[]; |
677 CalcTree |
677 CalcTree |
678 [(["functionTerm (x^2 + x + 1)", |
678 [(["functionTerm (x^2 + x + 1)", |
679 "differentiateFor x", "derivative f_'_"], |
679 "differentiateFor x", "derivative f_f'"], |
680 ("Isac", ["derivative_of","function"], |
680 ("Isac", ["derivative_of","function"], |
681 ["diff","differentiate_on_R"]))]; |
681 ["diff","differentiate_on_R"]))]; |
682 Iterator 1; |
682 Iterator 1; |
683 moveActiveRoot 1; |
683 moveActiveRoot 1; |
684 autoCalculate 1 CompleteCalcHead; |
684 autoCalculate 1 CompleteCalcHead; |