|
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 |
|
|
wneuper@59472
|
27 |
ML \<open>
|
|
neuper@37972
|
28 |
val thy = @{theory};
|
|
wneuper@59472
|
29 |
\<close>
|
|
neuper@37954
|
30 |
(** problems **)
|
|
wneuper@59472
|
31 |
setup \<open>KEStore_Elems.add_pbts
|
|
wneuper@59406
|
32 |
[(Specify.prep_pbt thy "pbl_test_equ_univ_log" [] Celem.e_pblID
|
|
s1210629013@55339
|
33 |
(["logarithmic","univariate","equation"],
|
|
s1210629013@55339
|
34 |
[("#Given",["equality e_e","solveFor v_v"]),
|
|
s1210629013@55339
|
35 |
("#Where",["matches ((?a log ?v_v) = ?b) e_e"]),
|
|
s1210629013@55339
|
36 |
("#Find" ,["solutions v_v'i'"]),
|
|
s1210629013@55339
|
37 |
("#With" ,["||(lhs (Subst (v'i', v_v) e_e) - " ^
|
|
s1210629013@55339
|
38 |
" (rhs (Subst (v'i', v_v) e_e) || < eps)"])],
|
|
wneuper@59472
|
39 |
PolyEq_prls, SOME "solve (e_e::bool, v_v)", [["Equation","solve_log"]]))]\<close>
|
|
s1210629013@55380
|
40 |
|
|
s1210629013@55373
|
41 |
(** methods **)
|
|
wneuper@59504
|
42 |
partial_function (tailrec) solve_log :: "bool \<Rightarrow> real \<Rightarrow> bool list"
|
|
wneuper@59504
|
43 |
where
|
|
wneuper@59504
|
44 |
"solve_log e_e v_v =
|
|
wneuper@59504
|
45 |
(let e_e = ((Rewrite ''equality_power'' False) @@
|
|
wneuper@59504
|
46 |
(Rewrite ''exp_invers_log'' False) @@
|
|
wneuper@59504
|
47 |
(Rewrite_Set ''norm_Poly'' False)) e_e
|
|
wneuper@59504
|
48 |
in [e_e])"
|
|
wneuper@59472
|
49 |
setup \<open>KEStore_Elems.add_mets
|
|
wneuper@59473
|
50 |
[Specify.prep_met thy "met_equ_log" [] Celem.e_metID
|
|
s1210629013@55373
|
51 |
(["Equation","solve_log"],
|
|
s1210629013@55373
|
52 |
[("#Given" ,["equality e_e","solveFor v_v"]),
|
|
s1210629013@55373
|
53 |
("#Where" ,["matches ((?a log ?v_v) = ?b) e_e"]),
|
|
s1210629013@55373
|
54 |
("#Find" ,["solutions v_v'i'"])],
|
|
wneuper@59416
|
55 |
{rew_ord' = "termlessI", rls' = PolyEq_erls, srls = Rule.e_rls, prls = PolyEq_prls, calc = [],
|
|
s1210629013@55373
|
56 |
crls = PolyEq_crls, errpats = [], nrls = norm_Rational},
|
|
s1210629013@55373
|
57 |
"Script Solve_log (e_e::bool) (v_v::real) = " ^
|
|
wneuper@59489
|
58 |
"(let e_e = ((Rewrite ''equality_power'' False) @@ " ^
|
|
wneuper@59489
|
59 |
" (Rewrite ''exp_invers_log'' False) @@ " ^
|
|
wneuper@59489
|
60 |
" (Rewrite_Set ''norm_Poly'' False)) e_e " ^
|
|
s1210629013@55373
|
61 |
" in [e_e])")]
|
|
wneuper@59472
|
62 |
\<close>
|
|
neuper@37906
|
63 |
|
|
neuper@37906
|
64 |
end |