106 (*got: NONE instead SOME*) |
106 (*got: NONE instead SOME*) |
107 eval_true Isac.thy [str2term "a is_const"] (assoc_rls"erls"); |
107 eval_true Isac.thy [str2term "a is_const"] (assoc_rls"erls"); |
108 (*got: false instead true; ~~~~~~~~~~~ replaced by 'is_atom'*) |
108 (*got: false instead true; ~~~~~~~~~~~ replaced by 'is_atom'*) |
109 val SOME (ctt,_) = |
109 val SOME (ctt,_) = |
110 (rewrite_inst thy' "tless_true" "erls" false [("bdv","s")] thm ct); |
110 (rewrite_inst thy' "tless_true" "erls" false [("bdv","s")] thm ct); |
111 if ctt = "0" then () else raise error "diff.sml: thm 'diff_const' diff.behav."; |
111 if ctt = "0" then () else error "diff.sml: thm 'diff_const' diff.behav."; |
112 trace_rewrite := false; |
112 trace_rewrite := false; |
113 "----- for 'd_d s a' we had 'a is_const' --> False --------^^^-----"; |
113 "----- for 'd_d s a' we had 'a is_const' --> False --------^^^-----"; |
114 |
114 |
115 val thm = ("diff_var",""); |
115 val thm = ("diff_var",""); |
116 val ct = "d_d x x"; |
116 val ct = "d_d x x"; |
169 "--- 6 ---"; |
169 "--- 6 ---"; |
170 val thm = ("diff_var",""); |
170 val thm = ("diff_var",""); |
171 val (ct,_) = the (rewrite_inst thy' "tless_true" "erls" true |
171 val (ct,_) = the (rewrite_inst thy' "tless_true" "erls" true |
172 [("bdv","x::real")] thm ct); |
172 [("bdv","x::real")] thm ct); |
173 if ct = "2 * x ^^^ (2 - 1) + 3 * 1 + 0" then () |
173 if ct = "2 * x ^^^ (2 - 1) + 3 * 1 + 0" then () |
174 else raise error "diff.sml diff.behav. in rewrite 1"; |
174 else error "diff.sml diff.behav. in rewrite 1"; |
175 "--- 7 ---"; |
175 "--- 7 ---"; |
176 val rls = ("Test_simplify"); |
176 val rls = ("Test_simplify"); |
177 val (ct,_) = the (rewrite_set thy' false rls ct); |
177 val (ct,_) = the (rewrite_set thy' false rls ct); |
178 if ct="3 + 2 * x" then () else raise error "new behaviour in test-example"; |
178 if ct="3 + 2 * x" then () else error "new behaviour in test-example"; |
179 |
179 |
180 val ct = "2 * x ^^^ (2 - 1) + 3 * 1 + 0"; |
180 val ct = "2 * x ^^^ (2 - 1) + 3 * 1 + 0"; |
181 val (ct,_) = the (rewrite_set thy' true rls ct); |
181 val (ct,_) = the (rewrite_set thy' true rls ct); |
182 |
182 |
183 |
183 |
247 (*val (p,_,f,nxt,_,pt) = me nxt p c pt;*) |
247 (*val (p,_,f,nxt,_,pt) = me nxt p c pt;*) |
248 "--- 6 ---"; |
248 "--- 6 ---"; |
249 (*val nxt = ("Rewrite_Inst",Rewrite_Inst (["(bdv,x)"],("diff_var","")));*) |
249 (*val nxt = ("Rewrite_Inst",Rewrite_Inst (["(bdv,x)"],("diff_var","")));*) |
250 val (p,_,f,nxt,_,pt) = me nxt p c pt; |
250 val (p,_,f,nxt,_,pt) = me nxt p c pt; |
251 if f2str f = "2 * x ^^^ (2 - 1) + 3 * 1 + 0" then () |
251 if f2str f = "2 * x ^^^ (2 - 1) + 3 * 1 + 0" then () |
252 else raise error "diff.sml: diff.behav. in d_d x ^^^ 2 + 3 * x + 4"; |
252 else error "diff.sml: diff.behav. in d_d x ^^^ 2 + 3 * x + 4"; |
253 "--- 7 ---"; |
253 "--- 7 ---"; |
254 (*------------------------------11.3.03-------------------- |
254 (*------------------------------11.3.03-------------------- |
255 trace_rewrite:=true; |
255 trace_rewrite:=true; |
256 val (_,_,f,_,_,_) = me nxt p c pt; |
256 val (_,_,f,_,_,_) = me nxt p c pt; |
257 val Form' (FormKF (_,_,_,_,res)) = f; |
257 val Form' (FormKF (_,_,_,_,res)) = f; |
289 val (p,_,f,nxt,_,pt) = me nxt p c pt; |
289 val (p,_,f,nxt,_,pt) = me nxt p c pt; |
290 "--- 9 ---"; |
290 "--- 9 ---"; |
291 (*val nxt = ("End_Proof'",End_Proof');*) |
291 (*val nxt = ("End_Proof'",End_Proof');*) |
292 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f; |
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 () |
293 if nxt = ("End_Proof'",End_Proof') andalso f2str f = "3 + 2 * x" then () |
294 else raise error "diff.sml: new.behav. in me (*+ tacs input*)"; |
294 else error "diff.sml: new.behav. in me (*+ tacs input*)"; |
295 (*if f = EmptyMout then () else raise error "new behaviour in + tacs input"; |
295 (*if f = EmptyMout then () else error "new behaviour in + tacs input"; |
296 meNEW extracts Form once more*) |
296 meNEW extracts Form once more*) |
297 |
297 |
298 |
298 |
299 |
299 |
300 |
300 |
462 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; |
463 val (p,_,f,nxt,_,pt) = me nxt p c pt; |
464 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; |
465 val (p,_,f,nxt,_,pt) = me nxt p c pt; |
466 if nxt = ("End_Proof'",End_Proof') then () |
466 if nxt = ("End_Proof'",End_Proof') then () |
467 else raise error "new behaviour in tests/differentiate, 1.5.02 me from script"; |
467 else error "new behaviour in tests/differentiate, 1.5.02 me from script"; |
468 |
468 |
469 "----------- primed id -------------------------------------------"; |
469 "----------- primed id -------------------------------------------"; |
470 "----------- primed id -------------------------------------------"; |
470 "----------- primed id -------------------------------------------"; |
471 "----------- primed id -------------------------------------------"; |
471 "----------- primed id -------------------------------------------"; |
472 |
472 |
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 error "diff.sml: diff.behav. in 'primed'"; |
487 atomty f'_; |
487 atomty f'_; |
488 |
488 |
489 val str = "Script DiffEqScr (f_f::bool) (v_v::real) = \ |
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_)) \ |
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))) @@ \ |
523 val subs = [(str2term "bdv", str2term "x")]; |
523 val subs = [(str2term "bdv", str2term "x")]; |
524 val rls = diff_conv; |
524 val rls = diff_conv; |
525 |
525 |
526 val t = str2term "2/x^^^2"; |
526 val t = str2term "2/x^^^2"; |
527 val SOME (t,_) = rewrite_set_inst_ thy false subs rls t; term2str t; |
527 val SOME (t,_) = rewrite_set_inst_ thy false subs rls t; term2str t; |
528 if term2str t = "2 * x ^^^ -2" then () else raise error "diff.sml 1/x"; |
528 if term2str t = "2 * x ^^^ -2" then () else error "diff.sml 1/x"; |
529 |
529 |
530 val t = str2term "sqrt (x^^^3)"; |
530 val t = str2term "sqrt (x^^^3)"; |
531 val SOME (t,_) = rewrite_set_inst_ thy false subs rls t; term2str t; |
531 val SOME (t,_) = rewrite_set_inst_ thy false subs rls t; term2str t; |
532 if term2str t = "x ^^^ (3 / 2)" then () else raise error "diff.sml x^1/2"; |
532 if term2str t = "x ^^^ (3 / 2)" then () else error "diff.sml x^1/2"; |
533 |
533 |
534 val t = str2term "2 / sqrt x^^^3"; |
534 val t = str2term "2 / sqrt x^^^3"; |
535 val SOME (t,_) = rewrite_set_inst_ thy false subs rls t; term2str t; |
535 val SOME (t,_) = rewrite_set_inst_ thy false subs rls t; term2str t; |
536 if term2str t = "2 * x ^^^ (-3 / 2)" then () else raise error"diff.sml x^-1/2"; |
536 if term2str t = "2 * x ^^^ (-3 / 2)" then () else error"diff.sml x^-1/2"; |
537 (* trace_rewrite := true; |
537 (* trace_rewrite := true; |
538 trace_rewrite := false; |
538 trace_rewrite := false; |
539 *) |
539 *) |
540 val rls = diff_sym_conv; |
540 val rls = diff_sym_conv; |
541 |
541 |
542 val t = str2term "2 * x ^^^ -2"; |
542 val t = str2term "2 * x ^^^ -2"; |
543 val SOME (t,_) = rewrite_set_inst_ thy false subs rls t; term2str t; |
543 val SOME (t,_) = rewrite_set_inst_ thy false subs rls t; term2str t; |
544 if term2str t = "2 / x ^^^ 2" then () else raise error "diff.sml sym 1/x"; |
544 if term2str t = "2 / x ^^^ 2" then () else error "diff.sml sym 1/x"; |
545 |
545 |
546 |
546 |
547 val t = str2term "x ^^^ (3 / 2)"; |
547 val t = str2term "x ^^^ (3 / 2)"; |
548 val SOME (t,_) = rewrite_set_inst_ thy false subs rls t; term2str t; |
548 val SOME (t,_) = rewrite_set_inst_ thy false subs rls t; term2str t; |
549 if term2str t = "sqrt (x ^^^ 3)" then () else raise error"diff.sml sym x^1/x"; |
549 if term2str t = "sqrt (x ^^^ 3)" then () else error"diff.sml sym x^1/x"; |
550 |
550 |
551 val t = str2term "2 * x ^^^ (-3 / 2)"; |
551 val t = str2term "2 * x ^^^ (-3 / 2)"; |
552 val SOME (t,_) = rewrite_set_inst_ thy false subs rls t; term2str t; |
552 val SOME (t,_) = rewrite_set_inst_ thy false subs rls t; term2str t; |
553 if term2str t ="2 / sqrt (x ^^^ 3)"then()else raise error"diff.sml sym x^-1/x"; |
553 if term2str t ="2 / sqrt (x ^^^ 3)"then()else error"diff.sml sym x^-1/x"; |
554 |
554 |
555 |
555 |
556 (* trace_rewrite:=true; |
556 (* trace_rewrite:=true; |
557 *) |
557 *) |
558 (* trace_rewrite:=false; |
558 (* trace_rewrite:=false; |
574 moveActiveRoot 1; |
574 moveActiveRoot 1; |
575 autoCalculate 1 CompleteCalc; |
575 autoCalculate 1 CompleteCalc; |
576 val ((pt,p),_) = get_calc 1; show_pt pt; |
576 val ((pt,p),_) = get_calc 1; show_pt pt; |
577 if p = ([], Res) andalso term2str (get_obj g_res pt (fst p)) = |
577 if p = ([], Res) andalso term2str (get_obj g_res pt (fst p)) = |
578 "1 + 2 * x + -1 / x ^^^ 2 + -4 / x ^^^ 3" then () |
578 "1 + 2 * x + -1 / x ^^^ 2 + -4 / x ^^^ 3" then () |
579 else raise error "diff.sml: differentiate_on_R 2/x^2 changed"; |
579 else error "diff.sml: differentiate_on_R 2/x^2 changed"; |
580 |
580 |
581 "-----------------------------------------------------------------"; |
581 "-----------------------------------------------------------------"; |
582 states:=[]; |
582 states:=[]; |
583 CalcTree |
583 CalcTree |
584 [(["functionTerm (x^3 * x^5)", |
584 [(["functionTerm (x^3 * x^5)", |
596 *) |
596 *) |
597 val ((pt,p),_) = get_calc 1; show_pt pt; |
597 val ((pt,p),_) = get_calc 1; show_pt pt; |
598 |
598 |
599 if p = ([], Res) andalso term2str (get_obj g_res pt (fst p)) = |
599 if p = ([], Res) andalso term2str (get_obj g_res pt (fst p)) = |
600 "8 * x ^^^ 7" then () |
600 "8 * x ^^^ 7" then () |
601 else raise error "diff.sml: differentiate_on_R (x^3 * x^5) changed"; |
601 else error "diff.sml: differentiate_on_R (x^3 * x^5) changed"; |
602 |
602 |
603 |
603 |
604 "----------- autoCalculate diff after_simplification -------------"; |
604 "----------- autoCalculate diff after_simplification -------------"; |
605 "----------- autoCalculate diff after_simplification -------------"; |
605 "----------- autoCalculate diff after_simplification -------------"; |
606 "----------- autoCalculate diff after_simplification -------------"; |
606 "----------- autoCalculate diff after_simplification -------------"; |
619 (* trace_rewrite := false; |
619 (* trace_rewrite := false; |
620 trace_script := false; |
620 trace_script := false; |
621 *) |
621 *) |
622 val ((pt,p),_) = get_calc 1; show_pt pt; |
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" |
623 if p = ([], Res) andalso term2str (get_obj g_res pt (fst p)) = "8 * x ^^^ 7" |
624 then () else raise error "biegelinie.sml: 1st biegelin.7.27 changed"; |
624 then () else error "biegelinie.sml: 1st biegelin.7.27 changed"; |
625 |
625 |
626 "-----------------------------------------------------------------"; |
626 "-----------------------------------------------------------------"; |
627 states:=[]; |
627 states:=[]; |
628 CalcTree |
628 CalcTree |
629 [(["functionTerm ((x^3)^5)", |
629 [(["functionTerm ((x^3)^5)", |
633 Iterator 1; |
633 Iterator 1; |
634 moveActiveRoot 1; |
634 moveActiveRoot 1; |
635 autoCalculate 1 CompleteCalc; |
635 autoCalculate 1 CompleteCalc; |
636 val ((pt,p),_) = get_calc 1; show_pt pt; |
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" |
637 if p = ([], Res) andalso term2str (get_obj g_res pt (fst p)) = "15 * x ^^^ 14" |
638 then () else raise error "biegelinie.sml: 1st biegelin.7.27 changed"; |
638 then () else error "biegelinie.sml: 1st biegelin.7.27 changed"; |
639 |
639 |
640 |
640 |
641 |
641 |
642 "----------- autoCalculate differentiate_equality ----------------"; |
642 "----------- autoCalculate differentiate_equality ----------------"; |
643 "----------- autoCalculate differentiate_equality ----------------"; |
643 "----------- autoCalculate differentiate_equality ----------------"; |
687 autoCalculate 1 (Step 1); |
687 autoCalculate 1 (Step 1); |
688 val ((pt,p),_) = get_calc 1; show_pt pt; |
688 val ((pt,p),_) = get_calc 1; show_pt pt; |
689 appendFormula 1 "2*x + d_d x x + d_d x 1"; |
689 appendFormula 1 "2*x + d_d x x + d_d x 1"; |
690 val ((pt,p),_) = get_calc 1; show_pt pt; |
690 val ((pt,p),_) = get_calc 1; show_pt pt; |
691 if existpt' ([3], Res) pt then () |
691 if existpt' ([3], Res) pt then () |
692 else raise error "diff.sml: inform d_d x (x^2 + x + 1) doesnt work"; |
692 else error "diff.sml: inform d_d x (x^2 + x + 1) doesnt work"; |