31 store_pbt |
31 store_pbt |
32 (prep_pbt thy "pbl_test_equ_univ_log" [] e_pblID |
32 (prep_pbt thy "pbl_test_equ_univ_log" [] 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_i"]), |
36 ("#Find" ,["solutions 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 ], |
39 ], |
40 PolyEq_prls, SOME "solve (e_e::bool, v_v)", |
40 PolyEq_prls, SOME "solve (e_e::bool, v_v)", |
41 [["Equation","solve_log"]])); |
41 [["Equation","solve_log"]])); |
42 *} |
42 *} |
43 ML {* |
43 ML {* |
45 store_met |
45 store_met |
46 (prep_met thy "met_equ_log" [] e_metID |
46 (prep_met thy "met_equ_log" [] e_metID |
47 (["Equation","solve_log"], |
47 (["Equation","solve_log"], |
48 [("#Given" ,["equality e_e","solveFor v_v"]), |
48 [("#Given" ,["equality e_e","solveFor v_v"]), |
49 ("#Where" ,["matches ((?a log ?v_v) = ?b) e_e"]), |
49 ("#Where" ,["matches ((?a log ?v_v) = ?b) e_e"]), |
50 ("#Find" ,["solutions v_i"]) |
50 ("#Find" ,["solutions v_i'''"]) |
51 ], |
51 ], |
52 {rew_ord'="termlessI",rls'=PolyEq_erls,srls=e_rls,prls=PolyEq_prls, |
52 {rew_ord'="termlessI",rls'=PolyEq_erls,srls=e_rls,prls=PolyEq_prls, |
53 calc=[],crls=PolyEq_crls, nrls=norm_Rational}, |
53 calc=[],crls=PolyEq_crls, nrls=norm_Rational}, |
54 "Script Solve_log (e_e::bool) (v_v::real) = " ^ |
54 "Script Solve_log (e_e::bool) (v_v::real) = " ^ |
55 "(let e_e = ((Rewrite equality_power False) @@ " ^ |
55 "(let e_e = ((Rewrite equality_power False) @@ " ^ |