|
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@52148
|
20 |
axiomatization where
|
|
neuper@37906
|
21 |
|
|
neuper@52148
|
22 |
equality_pow: "0 < a ==> (l = r) = (a^^^l = a^^^r)" and
|
|
neuper@37906
|
23 |
(* this is what students ^^^^^^^... are told to do *)
|
|
neuper@52148
|
24 |
equality_power: "((a log b) = c) = (a^^^(a log b) = a^^^c)" and
|
|
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@37991
|
35 |
("#Where",["matches ((?a log ?v_v) = ?b) e_e"]),
|
|
neuper@38012
|
36 |
("#Find" ,["solutions v_v'i'"]),
|
|
neuper@38010
|
37 |
("#With" ,["||(lhs (Subst (v'i', v_v) e_e) - " ^
|
|
neuper@38010
|
38 |
" (rhs (Subst (v'i', v_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@37992
|
42 |
*}
|
|
s1210629013@55359
|
43 |
setup {* KEStore_Elems.add_pbts
|
|
s1210629013@55339
|
44 |
[(prep_pbt thy "pbl_test_equ_univ_log" [] e_pblID
|
|
s1210629013@55339
|
45 |
(["logarithmic","univariate","equation"],
|
|
s1210629013@55339
|
46 |
[("#Given",["equality e_e","solveFor v_v"]),
|
|
s1210629013@55339
|
47 |
("#Where",["matches ((?a log ?v_v) = ?b) e_e"]),
|
|
s1210629013@55339
|
48 |
("#Find" ,["solutions v_v'i'"]),
|
|
s1210629013@55339
|
49 |
("#With" ,["||(lhs (Subst (v'i', v_v) e_e) - " ^
|
|
s1210629013@55339
|
50 |
" (rhs (Subst (v'i', v_v) e_e) || < eps)"])],
|
|
s1210629013@55339
|
51 |
PolyEq_prls, SOME "solve (e_e::bool, v_v)", [["Equation","solve_log"]]))] *}
|
|
neuper@37992
|
52 |
ML {*
|
|
neuper@37954
|
53 |
(** methods **)
|
|
neuper@37954
|
54 |
store_met
|
|
neuper@37972
|
55 |
(prep_met thy "met_equ_log" [] e_metID
|
|
neuper@37954
|
56 |
(["Equation","solve_log"],
|
|
neuper@37981
|
57 |
[("#Given" ,["equality e_e","solveFor v_v"]),
|
|
neuper@37991
|
58 |
("#Where" ,["matches ((?a log ?v_v) = ?b) e_e"]),
|
|
neuper@38012
|
59 |
("#Find" ,["solutions v_v'i'"])
|
|
neuper@37954
|
60 |
],
|
|
neuper@37954
|
61 |
{rew_ord'="termlessI",rls'=PolyEq_erls,srls=e_rls,prls=PolyEq_prls,
|
|
neuper@42425
|
62 |
calc=[],crls=PolyEq_crls, errpats = [], nrls = norm_Rational},
|
|
neuper@37982
|
63 |
"Script Solve_log (e_e::bool) (v_v::real) = " ^
|
|
neuper@37981
|
64 |
"(let e_e = ((Rewrite equality_power False) @@ " ^
|
|
neuper@37954
|
65 |
" (Rewrite exp_invers_log False) @@ " ^
|
|
neuper@37981
|
66 |
" (Rewrite_Set norm_Poly False)) e_e " ^
|
|
neuper@37992
|
67 |
" in [e_e])"
|
|
neuper@37954
|
68 |
));
|
|
neuper@37954
|
69 |
*}
|
|
neuper@37906
|
70 |
|
|
neuper@37906
|
71 |
end |