27 ML {* |
27 ML {* |
28 val thy = @{theory}; |
28 val thy = @{theory}; |
29 *} |
29 *} |
30 (** problems **) |
30 (** problems **) |
31 setup {* KEStore_Elems.add_pbts |
31 setup {* KEStore_Elems.add_pbts |
32 [(Specify.prep_pbt thy "pbl_test_equ_univ_log" [] e_pblID |
32 [(Specify.prep_pbt thy "pbl_test_equ_univ_log" [] Celem.e_pblID |
33 (["logarithmic","univariate","equation"], |
33 (["logarithmic","univariate","equation"], |
34 [("#Given",["equality e_e","solveFor v_v"]), |
34 [("#Given",["equality e_e","solveFor v_v"]), |
35 ("#Where",["matches ((?a log ?v_v) = ?b) e_e"]), |
35 ("#Where",["matches ((?a log ?v_v) = ?b) e_e"]), |
36 ("#Find" ,["solutions v_v'i'"]), |
36 ("#Find" ,["solutions v_v'i'"]), |
37 ("#With" ,["||(lhs (Subst (v'i', v_v) e_e) - " ^ |
37 ("#With" ,["||(lhs (Subst (v'i', v_v) e_e) - " ^ |
38 " (rhs (Subst (v'i', v_v) e_e) || < eps)"])], |
38 " (rhs (Subst (v'i', v_v) e_e) || < eps)"])], |
39 PolyEq_prls, SOME "solve (e_e::bool, v_v)", [["Equation","solve_log"]]))] *} |
39 PolyEq_prls, SOME "solve (e_e::bool, v_v)", [["Equation","solve_log"]]))] *} |
40 |
40 |
41 (** methods **) |
41 (** methods **) |
42 setup {* KEStore_Elems.add_mets |
42 setup {* KEStore_Elems.add_mets |
43 [Specify.prep_met thy "met_equ_log" [] e_metID |
43 [Specify.prep_met thy "met_equ_log" [] Celem.e_metID |
44 (["Equation","solve_log"], |
44 (["Equation","solve_log"], |
45 [("#Given" ,["equality e_e","solveFor v_v"]), |
45 [("#Given" ,["equality e_e","solveFor v_v"]), |
46 ("#Where" ,["matches ((?a log ?v_v) = ?b) e_e"]), |
46 ("#Where" ,["matches ((?a log ?v_v) = ?b) e_e"]), |
47 ("#Find" ,["solutions v_v'i'"])], |
47 ("#Find" ,["solutions v_v'i'"])], |
48 {rew_ord' = "termlessI", rls' = PolyEq_erls, srls = e_rls, prls = PolyEq_prls, calc = [], |
48 {rew_ord' = "termlessI", rls' = PolyEq_erls, srls = Celem.e_rls, prls = PolyEq_prls, calc = [], |
49 crls = PolyEq_crls, errpats = [], nrls = norm_Rational}, |
49 crls = PolyEq_crls, errpats = [], nrls = norm_Rational}, |
50 "Script Solve_log (e_e::bool) (v_v::real) = " ^ |
50 "Script Solve_log (e_e::bool) (v_v::real) = " ^ |
51 "(let e_e = ((Rewrite equality_power False) @@ " ^ |
51 "(let e_e = ((Rewrite equality_power False) @@ " ^ |
52 " (Rewrite exp_invers_log False) @@ " ^ |
52 " (Rewrite exp_invers_log False) @@ " ^ |
53 " (Rewrite_Set norm_Poly False)) e_e " ^ |
53 " (Rewrite_Set norm_Poly False)) e_e " ^ |