equal
deleted
inserted
replaced
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_"], |
35 val pbt = {Given =["functionTerm f_", "differentiateFor v_v"], |
36 Where =[], |
36 Where =[], |
37 Find =["derivative f_'_"], |
37 Find =["derivative 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; |
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_::bool"; |
474 val f = str2term "A = s * (a - s)"; |
474 val f = str2term "A = s * (a - s)"; |
475 val 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_ (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), (v_, v)] screxp0; |
481 term2str screxp1; |
481 term2str screxp1; |
482 atomty screxp1; |
482 atomty 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_::real) = \ |
489 val str = "Script DiffEqScr (f_::bool) (v_::real) = \ |
490 \ (let f'_ = Take ((primed (lhs f_)) = d_d v_ (rhs f_)) \ |
490 \ (let 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_)] diff_sum False)) Or \ |
495 \ ((Repeat (Rewrite_Inst [(bdv,v_)] diff_sum False)) Or \ |