neuper@37906
|
1 |
(* all outcommented in order to demonstrate authoring:
|
neuper@37906
|
2 |
WN071203
|
neuper@37906
|
3 |
*)
|
neuper@37954
|
4 |
|
neuper@37954
|
5 |
theory LogExp imports PolyEq begin
|
neuper@37906
|
6 |
|
neuper@37906
|
7 |
consts
|
neuper@37906
|
8 |
|
neuper@37906
|
9 |
ln :: "real => real"
|
neuper@37906
|
10 |
exp :: "real => real" ("E'_ ^^^ _" 80)
|
neuper@37906
|
11 |
|
neuper@37906
|
12 |
(*--------------------------------------------------*)
|
neuper@37906
|
13 |
alog :: "[real, real] => real" ("_ log _" 90)
|
neuper@37906
|
14 |
|
neuper@37906
|
15 |
(*Script-names*)
|
neuper@37954
|
16 |
Solve'_log :: "[bool,real, bool list]
|
neuper@37954
|
17 |
=> bool list"
|
neuper@37906
|
18 |
("((Script Solve'_log (_ _=))//(_))" 9)
|
neuper@37906
|
19 |
|
neuper@37983
|
20 |
axioms
|
neuper@37906
|
21 |
|
neuper@37983
|
22 |
equality_pow: "0 < a ==> (l = r) = (a^^^l = a^^^r)"
|
neuper@37906
|
23 |
(* this is what students ^^^^^^^... are told to do *)
|
neuper@37983
|
24 |
equality_power: "((a log b) = c) = (a^^^(a log b) = a^^^c)"
|
neuper@37983
|
25 |
exp_invers_log: "a^^^(a log b) = b"
|
neuper@37954
|
26 |
|
neuper@37954
|
27 |
ML {*
|
neuper@37972
|
28 |
val thy = @{theory};
|
neuper@37972
|
29 |
|
neuper@37954
|
30 |
(** problems **)
|
neuper@37954
|
31 |
store_pbt
|
neuper@37972
|
32 |
(prep_pbt thy "pbl_test_equ_univ_log" [] e_pblID
|
neuper@37954
|
33 |
(["logarithmic","univariate","equation"],
|
neuper@37981
|
34 |
[("#Given",["equality e_e","solveFor v_v"]),
|
neuper@37981
|
35 |
("#Where",["matches ((?a log ?v_) = ?b) e_e"]),
|
neuper@37981
|
36 |
("#Find" ,["solutions v_i"]),
|
neuper@37981
|
37 |
("#With" ,["||(lhs (Subst (v_i_,v_) e_e) - " ^
|
neuper@37981
|
38 |
" (rhs (Subst (v_i_,v_) e_e) || < eps)"])
|
neuper@37954
|
39 |
],
|
neuper@37981
|
40 |
PolyEq_prls, SOME "solve (e_e::bool, v_v)",
|
neuper@37954
|
41 |
[["Equation","solve_log"]]));
|
neuper@37954
|
42 |
|
neuper@37954
|
43 |
(** methods **)
|
neuper@37954
|
44 |
store_met
|
neuper@37972
|
45 |
(prep_met thy "met_equ_log" [] e_metID
|
neuper@37954
|
46 |
(["Equation","solve_log"],
|
neuper@37981
|
47 |
[("#Given" ,["equality e_e","solveFor v_v"]),
|
neuper@37981
|
48 |
("#Where" ,["matches ((?a log ?v_) = ?b) e_e"]),
|
neuper@37981
|
49 |
("#Find" ,["solutions v_i"])
|
neuper@37954
|
50 |
],
|
neuper@37954
|
51 |
{rew_ord'="termlessI",rls'=PolyEq_erls,srls=e_rls,prls=PolyEq_prls,
|
neuper@37954
|
52 |
calc=[],crls=PolyEq_crls, nrls=norm_Rational},
|
neuper@37982
|
53 |
"Script Solve_log (e_e::bool) (v_v::real) = " ^
|
neuper@37981
|
54 |
"(let e_e = ((Rewrite equality_power False) @@ " ^
|
neuper@37954
|
55 |
" (Rewrite exp_invers_log False) @@ " ^
|
neuper@37981
|
56 |
" (Rewrite_Set norm_Poly False)) e_e " ^
|
neuper@37954
|
57 |
" in [e_])"
|
neuper@37954
|
58 |
));
|
neuper@37954
|
59 |
*}
|
neuper@37906
|
60 |
|
neuper@37906
|
61 |
end |