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