127 *) |
127 *) |
128 |
128 |
129 (* --vvv-- ausgeliehen von test-root-equ/sml *) |
129 (* --vvv-- ausgeliehen von test-root-equ/sml *) |
130 val loc = e_istate; |
130 val loc = e_istate; |
131 val (dI',pI',mI') = |
131 val (dI',pI',mI') = |
132 ("Script.thy",["sqroot-test","univariate","equation"], |
132 ("Script",["sqroot-test","univariate","equation"], |
133 ["Script","squ-equ-test2"]); |
133 ["Script","squ-equ-test2"]); |
134 val fmz = ["equality (sqrt(9+4*x)=sqrt x + sqrt(5+x))", |
134 val fmz = ["equality (sqrt(9+4*x)=sqrt x + sqrt(5+x))", |
135 "solveFor x","errorBound (eps=0)", |
135 "solveFor x","errorBound (eps=0)", |
136 "solutions L"]; |
136 "solutions L"]; |
137 (* |
137 (* |
264 "interval {x::real. 0 <= x & x <= 2*r}", |
264 "interval {x::real. 0 <= x & x <= 2*r}", |
265 "interval {x::real. 0 <= x & x <= 2*r}", |
265 "interval {x::real. 0 <= x & x <= 2*r}", |
266 "interval {x::real. 0 <= x & x <= pi}", |
266 "interval {x::real. 0 <= x & x <= pi}", |
267 "errorBound (eps=(0::real))"]; |
267 "errorBound (eps=(0::real))"]; |
268 val (dI',pI',mI') = |
268 val (dI',pI',mI') = |
269 ("DiffApp.thy",["maximum_of","function"], |
269 ("DiffApp",["maximum_of","function"], |
270 ["DiffApp","max_by_calculus"]); |
270 ["DiffApp","max_by_calculus"]); |
271 |
271 |
272 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))]; |
272 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))]; |
273 val (p,_,f,nxt,_,pt) = me nxt p c pt; |
273 val (p,_,f,nxt,_,pt) = me nxt p c pt; |
274 val (p,_,f,nxt,_,pt) = me nxt p c pt; |
274 val (p,_,f,nxt,_,pt) = me nxt p c pt; |
293 case nxt of (_,Apply_Method ["DiffApp","max_by_calculus"] ) => () |
293 case nxt of (_,Apply_Method ["DiffApp","max_by_calculus"] ) => () |
294 | _ => raise error "diffapp.sml: max-exp me, nxt = Apply_Method"; |
294 | _ => raise error "diffapp.sml: max-exp me, nxt = Apply_Method"; |
295 val (p,_,f,nxt,_,pt) = me nxt p c pt; |
295 val (p,_,f,nxt,_,pt) = me nxt p c pt; |
296 |
296 |
297 (*since 0508 Apply_Method does the 1st step, if NONE init_form ------------- |
297 (*since 0508 Apply_Method does the 1st step, if NONE init_form ------------- |
298 (*val nxt = ("Subproblem",Subproblem ("DiffApp.thy",["make","function"]))*) |
298 (*val nxt = ("Subproblem",Subproblem ("DiffApp",["make","function"]))*) |
299 val (p,_,f,nxt,_,pt) = (me nxt p c pt) handle e => print_exn_G e; |
299 val (p,_,f,nxt,_,pt) = (me nxt p c pt) handle e => print_exn_G e; |
300 (*val nxt = ("Refine_Tacitly",Refine_Tacitly ["make","function"])*) |
300 (*val nxt = ("Refine_Tacitly",Refine_Tacitly ["make","function"])*) |
301 val (p,_,f,nxt,_,pt) = me nxt p c pt; |
301 val (p,_,f,nxt,_,pt) = me nxt p c pt; |
302 (*val nxt = ("Model_Problem",Model_Problem ["by_explicit","make","function"])*) |
302 (*val nxt = ("Model_Problem",Model_Problem ["by_explicit","make","function"])*) |
303 ----------------------------------------------------------------------------*) |
303 ----------------------------------------------------------------------------*) |
337 |
337 |
338 ############################################################################ |
338 ############################################################################ |
339 # presumerably didnt work before either, but not detected due to Emtpy_Tac # |
339 # presumerably didnt work before either, but not detected due to Emtpy_Tac # |
340 ############################################################################ |
340 ############################################################################ |
341 |
341 |
342 (*val nxt = Subproblem ("DiffApp.thy",["univariate","equation"])) *) |
342 (*val nxt = Subproblem ("DiffApp",["univariate","equation"])) *) |
343 val (p,_,f,nxt,_,pt) = me nxt p c pt; |
343 val (p,_,f,nxt,_,pt) = me nxt p c pt; |
344 (*val nxt = Refine_Tacitly ["univariate","equation"])*) |
344 (*val nxt = Refine_Tacitly ["univariate","equation"])*) |
345 |
345 |
346 val oris = fst3 (get_obj g_origin pt (fst p));writeln(oris2str oris); |
346 val oris = fst3 (get_obj g_origin pt (fst p));writeln(oris2str oris); |
347 val pits = get_obj g_pbl pt (fst p);writeln(itms2str_ ctxt pits); |
347 val pits = get_obj g_pbl pt (fst p);writeln(itms2str_ ctxt pits); |
405 "interval {x::real. 0 <= x & x <= 2*r}", |
405 "interval {x::real. 0 <= x & x <= 2*r}", |
406 "interval {x::real. 0 <= x & x <= 2*r}", |
406 "interval {x::real. 0 <= x & x <= 2*r}", |
407 "interval {x::real. 0 <= x & x <= pi}", |
407 "interval {x::real. 0 <= x & x <= pi}", |
408 "errorBound (eps=(0::real))"]; |
408 "errorBound (eps=(0::real))"]; |
409 val (dI',pI',mI') = |
409 val (dI',pI',mI') = |
410 ("DiffApp.thy",["maximum_of","function"], |
410 ("DiffApp",["maximum_of","function"], |
411 ["DiffApp","max_by_calculus"]); |
411 ["DiffApp","max_by_calculus"]); |
412 |
412 |
413 CalcTree [(fmz, (dI',pI',mI'))]; |
413 CalcTree [(fmz, (dI',pI',mI'))]; |
414 Iterator 1; moveActiveRoot 1; |
414 Iterator 1; moveActiveRoot 1; |
415 autoCalculate 1 CompleteCalcHead; |
415 autoCalculate 1 CompleteCalcHead; |
442 "--------------------- 30.4.03: maximum .. rewrite_set_ list_rls ---------"; |
442 "--------------------- 30.4.03: maximum .. rewrite_set_ list_rls ---------"; |
443 "--------------------- 30.4.03: maximum .. rewrite_set_ list_rls ---------"; |
443 "--------------------- 30.4.03: maximum .. rewrite_set_ list_rls ---------"; |
444 "--------------------- 30.4.03: maximum .. rewrite_set_ list_rls ---------"; |
444 "--------------------- 30.4.03: maximum .. rewrite_set_ list_rls ---------"; |
445 str2term |
445 str2term |
446 "Script Maximum_value(fix_::bool list)(m_::real) (rs_::bool list)\ |
446 "Script Maximum_value(fix_::bool list)(m_::real) (rs_::bool list)\ |
447 \ (v_::real) (itv_::real set) (err_::bool) = \ |
447 \ (v_v::real) (itv_v::real set) (err_::bool) = \ |
448 \ (let e_e = (hd o (filterVar m_)) rs_; \ |
448 \ (let e_e = (hd o (filterVar m_)) rs_; \ |
449 \ t_ = (if 1 < length_ rs_ \ |
449 \ t_ = (if 1 < length_ rs_ \ |
450 \ then (SubProblem (Reals_,[make,function],[no_met])\ |
450 \ then (SubProblem (Reals_,[make,function],[no_met])\ |
451 \ [REAL m_, REAL v_v, BOOL_LIST rs_])\ |
451 \ [REAL m_, REAL v_v, BOOL_LIST rs_])\ |
452 \ else (hd rs_)); \ |
452 \ else (hd rs_)); \ |
461 str2term "[r=Arbfix]"); |
461 str2term "[r=Arbfix]"); |
462 val m_ = (str2term "m_::real", |
462 val m_ = (str2term "m_::real", |
463 str2term "A"); |
463 str2term "A"); |
464 val rs_ = (str2term "rs_::bool list", |
464 val rs_ = (str2term "rs_::bool list", |
465 str2term "[A = a*b, (a/2)^^^2 + (b/2)^^^2 = r^^^2]"); |
465 str2term "[A = a*b, (a/2)^^^2 + (b/2)^^^2 = r^^^2]"); |
466 val v_v = (str2term "v_::real", |
466 val v_v = (str2term "v_v::real", |
467 str2term "b"); |
467 str2term "b"); |
468 val itv_ = (str2term "itv_::real set", |
468 val itv_ = (str2term "itv_v::real set", |
469 str2term "{x::real. 0 <= x & x <= 2*r}"); |
469 str2term "{x::real. 0 <= x & x <= 2*r}"); |
470 val err_ = (str2term "err_::bool", |
470 val err_ = (str2term "err_::bool", |
471 str2term "eps=0"); |
471 str2term "eps=0"); |
472 val env = [fix_, m_, rs_ ,v_, itv_, err_]; |
472 val env = [fix_, m_, rs_ ,v_, itv_, err_]; |
473 |
473 |
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_::real) \ |
522 "Script Make_fun_by_explicit (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_::real", |
532 str2term "A"); |
532 str2term "A"); |
533 val v_v = (str2term "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_, v_v, eqs_]; |
538 |
538 |
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_::real) \ |
613 "Script Make_fun_by_new_variable (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_; \ |
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_::real", |
628 str2term "A"); |
628 str2term "A"); |
629 val v_v = (str2term "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_, v_v, eqs_]; |
634 |
634 |