1 (* all outcommented in order to demonstrate authoring: |
|
2 WN071203 |
|
3 *) |
|
4 |
|
5 (** interface isabelle -- isac **) |
|
6 theory' := overwritel (!theory', [("LogExp.thy",LogExp.thy)]); |
|
7 |
|
8 (*--------------------------------------------------*) |
|
9 |
|
10 (** problems **) |
|
11 store_pbt |
|
12 (prep_pbt LogExp.thy "pbl_test_equ_univ_log" [] e_pblID |
|
13 (["logarithmic","univariate","equation"], |
|
14 [("#Given",["equality e_","solveFor v_"]), |
|
15 ("#Where",["matches ((?a log ?v_) = ?b) e_"]), |
|
16 ("#Find" ,["solutions v_i_"]), |
|
17 ("#With" ,["||(lhs (Subst (v_i_,v_) e_) - \ |
|
18 \ (rhs (Subst (v_i_,v_) e_) || < eps)"]) |
|
19 ], |
|
20 PolyEq_prls, SOME "solve (e_::bool, v_)", |
|
21 [["Equation","solve_log"]])); |
|
22 |
|
23 (** methods **) |
|
24 store_met |
|
25 (prep_met LogExp.thy "met_equ_log" [] e_metID |
|
26 (["Equation","solve_log"], |
|
27 [("#Given" ,["equality e_","solveFor v_"]), |
|
28 ("#Where" ,["matches ((?a log ?v_) = ?b) e_"]), |
|
29 ("#Find" ,["solutions v_i_"]) |
|
30 ], |
|
31 {rew_ord'="termlessI",rls'=PolyEq_erls,srls=e_rls,prls=PolyEq_prls, |
|
32 calc=[],crls=PolyEq_crls, nrls=norm_Rational}, |
|
33 "Script Solve_log (e_::bool) (v_::real) = \ |
|
34 \(let e_ = ((Rewrite equality_power False) @@ \ |
|
35 \ (Rewrite exp_invers_log False) @@ \ |
|
36 \ (Rewrite_Set norm_Poly False)) e_ \ |
|
37 \ in [e_])" |
|
38 )); |
|
39 (*--------------------------------------------------*) |
|