43 "interval {x::real. 0 <= x & x <= pi}", |
43 "interval {x::real. 0 <= x & x <= pi}", |
44 "errorBound (eps=(0::real))"]; |
44 "errorBound (eps=(0::real))"]; |
45 map (the o (parseold thy)) fmz; |
45 map (the o (parseold thy)) fmz; |
46 " -------------- [make,function] -------------- "; |
46 " -------------- [make,function] -------------- "; |
47 val pbt = |
47 val pbt = |
48 ["functionOf f_","boundVariable v_v","equalities eqs_", |
48 ["functionOf f_f","boundVariable v_v","equalities eqs", |
49 "functionTerm f_0_"]; |
49 "functionTerm f_0_"]; |
50 map (the o (parseold thy)) pbt; |
50 map (the o (parseold thy)) pbt; |
51 val fmz12 = |
51 val fmz12 = |
52 ["functionOf A","boundVariable a","boundVariable b", |
52 ["functionOf A","boundVariable a","boundVariable b", |
53 "equalities [A=a*b, (a/2)^^^2 + (b/2)^^^2 = r^^^2]", |
53 "equalities [A=a*b, (a/2)^^^2 + (b/2)^^^2 = r^^^2]", |
87 "interval {x::real. 0 <= x & x <= pi}", |
87 "interval {x::real. 0 <= x & x <= pi}", |
88 "errorBound (eps=0)","maxArgument (a_0=Undef)"]; |
88 "errorBound (eps=0)","maxArgument (a_0=Undef)"]; |
89 map (the o (parseold thy)) fmz3; |
89 map (the o (parseold thy)) fmz3; |
90 " --------- [derivative_of,function] --------- "; |
90 " --------- [derivative_of,function] --------- "; |
91 val pbt = |
91 val pbt = |
92 ["functionTerm f_","boundVariable v_v","derivative f_'_"]; |
92 ["functionTerm f_f","boundVariable v_v","derivative f_f'"]; |
93 map (the o (parseold thy)) pbt; |
93 map (the o (parseold thy)) pbt; |
94 val fmz = |
94 val fmz = |
95 [(*28.11.00: "functionTerm (A_0=a*#2*sqrt r^^^#2 - (a//#2)^^^#2)",*) |
95 [(*28.11.00: "functionTerm (A_0=a*#2*sqrt r^^^#2 - (a//#2)^^^#2)",*) |
96 "functionTerm (a*2*sqrt r^^^2 - (a/2)^^^2)", |
96 "functionTerm (a*2*sqrt r^^^2 - (a/2)^^^2)", |
97 "boundVariable a", |
97 "boundVariable a", |
98 (*28.11.00: "derivative (A_0'=Undef)"*)"derivative (Undef)"]; |
98 (*28.11.00: "derivative (A_0'=Undef)"*)"derivative (Undef)"]; |
99 map (the o (parseold thy)) fmz; |
99 map (the o (parseold thy)) fmz; |
100 " --------- [find_values,tool] --------- "; |
100 " --------- [find_values,tool] --------- "; |
101 val pbt = |
101 val pbt = |
102 ["maxArgument ma_","functionTerm f_","boundVariable v_v", |
102 ["maxArgument ma_","functionTerm f_f","boundVariable v_v", |
103 "valuesFor vls_","additionalRels rs_"]; |
103 "valuesFor vls_","additionalRels rs_"]; |
104 map (the o (parseold thy)) pbt; |
104 map (the o (parseold thy)) pbt; |
105 val fmz1 = |
105 val fmz1 = |
106 ["maxArgument (a_0=(srqt 2)*r)", |
106 ["maxArgument (a_0=(srqt 2)*r)", |
107 (*28.11.00: "functionTerm (A_0=a*#2*sqrt r^^^#2 - (a//#2)^^^#2)",*) |
107 (*28.11.00: "functionTerm (A_0=a*#2*sqrt r^^^#2 - (a//#2)^^^#2)",*) |
517 |
517 |
518 "---------------------- 1.5.03: Make_fun_by_explicit ---------------------"; |
518 "---------------------- 1.5.03: Make_fun_by_explicit ---------------------"; |
519 "---------------------- 1.5.03: Make_fun_by_explicit ---------------------"; |
519 "---------------------- 1.5.03: Make_fun_by_explicit ---------------------"; |
520 "---------------------- 1.5.03: Make_fun_by_explicit ---------------------"; |
520 "---------------------- 1.5.03: Make_fun_by_explicit ---------------------"; |
521 str2term |
521 str2term |
522 "Script Make_fun_by_explicit (f_::real) (v_v::real) \ |
522 "Script Make_fun_by_explicit (f_f::real) (v_v::real) \ |
523 \ (eqs_::bool list) = \ |
523 \ (eqs::bool list) = \ |
524 \ (let h_ = (hd o (filterVar f_)) eqs_; \ |
524 \ (let h_ = (hd o (filterVar f_)) eqs; \ |
525 \ e_1 = hd (dropWhile (ident h_) eqs_); \ |
525 \ e_1 = hd (dropWhile (ident h_) eqs); \ |
526 \ vs_ = dropWhile (ident f_) (Vars h_); \ |
526 \ vs_ = dropWhile (ident f_) (Vars h_); \ |
527 \ v_1 = hd (dropWhile (ident v_v) vs_); \ |
527 \ v_1 = hd (dropWhile (ident v_v) vs_); \ |
528 \ (s_1::bool list)=(SubProblem(Reals_,[univar,equation],[no_met])\ |
528 \ (s_1::bool list)=(SubProblem(Reals_,[univar,equation],[no_met])\ |
529 \ [BOOL e_1, REAL v_1])\ |
529 \ [BOOL e_1, REAL v_1])\ |
530 \ in Substitute [(v_1 = (rhs o hd) s_1)] h_)"; |
530 \ in Substitute [(v_1 = (rhs o hd) s_1)] h_)"; |
531 val f_ = (str2term "f_::real", |
531 val f_ = (str2term "f_f::real", |
532 str2term "A"); |
532 str2term "A"); |
533 val v_v = (str2term "v_v::real", |
533 val v_v = (str2term "v_v::real", |
534 str2term "b"); |
534 str2term "b"); |
535 val eqs_=(str2term "eqs_::bool list", |
535 val eqs=(str2term "eqs::bool list", |
536 str2term "[A = a * b, (a / 2) ^^^ 2 + (b / 2) ^^^ 2 = r ^^^ 2]"); |
536 str2term "[A = a * b, (a / 2) ^^^ 2 + (b / 2) ^^^ 2 = r ^^^ 2]"); |
537 val env = [f_, v_v, eqs_]; |
537 val env = [f_f, v_v, eqs]; |
538 |
538 |
539 (*--- 1.line in script ---*) |
539 (*--- 1.line in script ---*) |
540 val t = str2term "(hd o (filterVar v_v)) (eqs_::bool list)"; |
540 val t = str2term "(hd o (filterVar v_v)) (eqs::bool list)"; |
541 val s = subst_atomic env t; |
541 val s = subst_atomic env t; |
542 term2str s; |
542 term2str s; |
543 val t = str2term |
543 val t = str2term |
544 "(hd o filterVar b) [A = a * b, (a / 2) ^^^ 2 + (b / 2) ^^^ 2 = r ^^^ 2]"; |
544 "(hd o filterVar b) [A = a * b, (a / 2) ^^^ 2 + (b / 2) ^^^ 2 = r ^^^ 2]"; |
545 val SOME (t',_) = rewrite_set_ thy false list_rls t; |
545 val SOME (t',_) = rewrite_set_ thy false list_rls t; |
546 val s' = term2str t'; |
546 val s' = term2str t'; |
547 if s' = "A = a * b" then () else raise error "new behaviour with list_rls 2.1"; |
547 if s' = "A = a * b" then () else raise error "new behaviour with list_rls 2.1"; |
548 val env = env @ [(str2term "h_::bool", str2term s')]; |
548 val env = env @ [(str2term "h_::bool", str2term s')]; |
549 |
549 |
550 (*--- 2.line in script ---*) |
550 (*--- 2.line in script ---*) |
551 val t = str2term "hd (dropWhile (ident h_) (eqs_::bool list))"; |
551 val t = str2term "hd (dropWhile (ident h_) (eqs::bool list))"; |
552 val s = subst_atomic env t; |
552 val s = subst_atomic env t; |
553 term2str s; |
553 term2str s; |
554 val t = str2term |
554 val t = str2term |
555 "hd (dropWhile (ident (A = a * b))\ |
555 "hd (dropWhile (ident (A = a * b))\ |
556 \ [A = a * b, (a / 2) ^^^ 2 + (b / 2) ^^^ 2 = r ^^^ 2])"; |
556 \ [A = a * b, (a / 2) ^^^ 2 + (b / 2) ^^^ 2 = r ^^^ 2])"; |
608 |
608 |
609 "---------------------- 2.5.03: Make_fun_by_new_variable -----------------"; |
609 "---------------------- 2.5.03: Make_fun_by_new_variable -----------------"; |
610 "---------------------- 2.5.03: Make_fun_by_new_variable -----------------"; |
610 "---------------------- 2.5.03: Make_fun_by_new_variable -----------------"; |
611 "---------------------- 2.5.03: Make_fun_by_new_variable -----------------"; |
611 "---------------------- 2.5.03: Make_fun_by_new_variable -----------------"; |
612 str2term |
612 str2term |
613 "Script Make_fun_by_new_variable (f_::real) (v_v::real) \ |
613 "Script Make_fun_by_new_variable (f_f::real) (v_v::real) \ |
614 \ (eqs_::bool list) = \ |
614 \ (eqs::bool list) = \ |
615 \(let h_ = (hd o (filterVar f_)) eqs_; \ |
615 \(let h_ = (hd o (filterVar f_)) eqs; \ |
616 \ es_ = dropWhile (ident h_) eqs_; \ |
616 \ es_ = dropWhile (ident h_) eqs; \ |
617 \ vs_ = dropWhile (ident f_) (Vars h_); \ |
617 \ vs_ = dropWhile (ident f_) (Vars h_); \ |
618 \ v_1 = nth_ 1 vs_; \ |
618 \ v_1 = nth_ 1 vs_; \ |
619 \ v_2 = nth_ 2 vs_; \ |
619 \ v_2 = nth_ 2 vs_; \ |
620 \ e_1 = (hd o (filterVar v_1)) es_; \ |
620 \ e_1 = (hd o (filterVar v_1)) es_; \ |
621 \ e_2 = (hd o (filterVar v_2)) es_; \ |
621 \ e_2 = (hd o (filterVar v_2)) es_; \ |
622 \ (s_1::bool list) = (SubProblem (Reals_,[univar,equation],[no_met])\ |
622 \ (s_1::bool list) = (SubProblem (Reals_,[univar,equation],[no_met])\ |
623 \ [BOOL e_1, REAL v_1]);\ |
623 \ [BOOL e_1, REAL v_1]);\ |
624 \ (s_2::bool list) = (SubProblem (Reals_,[univar,equation],[no_met])\ |
624 \ (s_2::bool list) = (SubProblem (Reals_,[univar,equation],[no_met])\ |
625 \ [BOOL e_2, REAL v_2])\ |
625 \ [BOOL e_2, REAL v_2])\ |
626 \in Substitute [(v_1 = (rhs o hd) s_1),(v_2 = (rhs o hd) s_2)] h_)"; |
626 \in Substitute [(v_1 = (rhs o hd) s_1),(v_2 = (rhs o hd) s_2)] h_)"; |
627 val f_ = (str2term "f_::real", |
627 val f_ = (str2term "f_f::real", |
628 str2term "A"); |
628 str2term "A"); |
629 val v_v = (str2term "v_v::real", |
629 val v_v = (str2term "v_v::real", |
630 str2term "alpha"); |
630 str2term "alpha"); |
631 val eqs_=(str2term "eqs_::bool list", |
631 val eqs=(str2term "eqs::bool list", |
632 str2term "[A=a*b, a/2=r*sin alpha, b/2=r*cos alpha]"); |
632 str2term "[A=a*b, a/2=r*sin alpha, b/2=r*cos alpha]"); |
633 val env = [f_, v_v, eqs_]; |
633 val env = [f_f, v_v, eqs]; |
634 |
634 |
635 (*--- 1.line in script ---*) |
635 (*--- 1.line in script ---*) |
636 val t = str2term "(hd o (filterVar (f_::real))) (eqs_::bool list)"; |
636 val t = str2term "(hd o (filterVar (f_f::real))) (eqs::bool list)"; |
637 val s = subst_atomic env t; |
637 val s = subst_atomic env t; |
638 term2str s; |
638 term2str s; |
639 val t = str2term |
639 val t = str2term |
640 "(hd o filterVar A) [A = a * b, a / 2 = r * sin alpha, b / 2 = r * cos alpha]"; |
640 "(hd o filterVar A) [A = a * b, a / 2 = r * sin alpha, b / 2 = r * cos alpha]"; |
641 trace_rewrite:=true; |
641 trace_rewrite:=true; |
644 val s' = term2str t'; |
644 val s' = term2str t'; |
645 if s' = "A = a * b" then() else raise error "new behaviour with list_rls 3.1."; |
645 if s' = "A = a * b" then() else raise error "new behaviour with list_rls 3.1."; |
646 val env = env @ [(str2term "h_::bool", str2term s')]; |
646 val env = env @ [(str2term "h_::bool", str2term s')]; |
647 |
647 |
648 (*--- 2.line in script ---*) |
648 (*--- 2.line in script ---*) |
649 val t = str2term "dropWhile (ident (h_::bool)) (eqs_::bool list)"; |
649 val t = str2term "dropWhile (ident (h_::bool)) (eqs::bool list)"; |
650 val s = subst_atomic env t; |
650 val s = subst_atomic env t; |
651 term2str s; |
651 term2str s; |
652 val t = str2term |
652 val t = str2term |
653 "dropWhile (ident (A = a * b))\ |
653 "dropWhile (ident (A = a * b))\ |
654 \ [A = a * b, a / 2 = r * sin alpha, b / 2 = r * cos alpha]"; |
654 \ [A = a * b, a / 2 = r * sin alpha, b / 2 = r * cos alpha]"; |
657 if s' = "[a / 2 = r * sin alpha, b / 2 = r * cos alpha]" |
657 if s' = "[a / 2 = r * sin alpha, b / 2 = r * cos alpha]" |
658 then () else raise error "new behaviour with list_rls 3.2."; |
658 then () else raise error "new behaviour with list_rls 3.2."; |
659 val env = env @ [(str2term "es_::bool list", str2term s')]; |
659 val env = env @ [(str2term "es_::bool list", str2term s')]; |
660 |
660 |
661 (*--- 3.line in script ---*) |
661 (*--- 3.line in script ---*) |
662 val t = str2term "dropWhile (ident (f_::real)) (Vars (h_::bool))"; |
662 val t = str2term "dropWhile (ident (f_f::real)) (Vars (h_::bool))"; |
663 val s = subst_atomic env t; |
663 val s = subst_atomic env t; |
664 term2str s; |
664 term2str s; |
665 val t = str2term "dropWhile (ident A) (Vars (A = a * b))"; |
665 val t = str2term "dropWhile (ident A) (Vars (A = a * b))"; |
666 val SOME (t',_) = rewrite_set_ thy false list_rls t; |
666 val SOME (t',_) = rewrite_set_ thy false list_rls t; |
667 val s' = term2str t'; |
667 val s' = term2str t'; |