neuper@37906: (* all outcommented in order to demonstrate authoring:
neuper@37906:    WN071203
neuper@37906: *)
neuper@37954: 
neuper@37954: theory LogExp imports PolyEq begin
neuper@37906: 
neuper@37906: consts
neuper@37906: 
neuper@37906:   ln     :: "real => real"
neuper@37906:   exp    :: "real => real"         ("E'_ ^^^ _" 80)
neuper@37906: 
neuper@37906: (*--------------------------------------------------*) 
neuper@37906:   alog   :: "[real, real] => real" ("_ log _" 90)
neuper@37906: 
neuper@37906:   (*Script-names*)
neuper@37954:   Solve'_log    :: "[bool,real,        bool list]  
neuper@37954: 				    => bool list"
neuper@37906:                   ("((Script Solve'_log (_ _=))//(_))" 9)
neuper@37906: 
neuper@37983: axioms
neuper@37906: 
neuper@37983:   equality_pow:    "0 < a ==> (l = r) = (a^^^l = a^^^r)"
neuper@37906:   (* this is what students   ^^^^^^^... are told to do *)
neuper@37983:   equality_power:  "((a log b) = c) = (a^^^(a log b) = a^^^c)"
neuper@37983:   exp_invers_log:  "a^^^(a log b) = b"
neuper@37954: 
neuper@37954: ML {*
neuper@37972: val thy = @{theory};
neuper@37972: 
neuper@37954: (** problems **)
neuper@37954: store_pbt
neuper@37972:  (prep_pbt thy "pbl_test_equ_univ_log" [] e_pblID
neuper@37954:  (["logarithmic","univariate","equation"],
neuper@37981:   [("#Given",["equality e_e","solveFor v_v"]),
neuper@37991:    ("#Where",["matches ((?a log ?v_v) = ?b) e_e"]),
neuper@38010:    ("#Find" ,["solutions v'i'"]),
neuper@38010:    ("#With" ,["||(lhs (Subst (v'i', v_v) e_e) - " ^
neuper@38010: 	      "  (rhs (Subst (v'i', v_v) e_e) || < eps)"])
neuper@37954:    ],
neuper@37981:   PolyEq_prls, SOME "solve (e_e::bool, v_v)",
neuper@37954:   [["Equation","solve_log"]]));
neuper@37992: *}
neuper@37992: ML {*
neuper@37954: (** methods **)
neuper@37954: store_met
neuper@37972:  (prep_met thy "met_equ_log" [] e_metID
neuper@37954:  (["Equation","solve_log"],
neuper@37981:   [("#Given" ,["equality e_e","solveFor v_v"]),
neuper@37991:    ("#Where" ,["matches ((?a log ?v_v) = ?b) e_e"]),
neuper@38010:    ("#Find"  ,["solutions v'i'"])
neuper@37954:   ],
neuper@37954:    {rew_ord'="termlessI",rls'=PolyEq_erls,srls=e_rls,prls=PolyEq_prls,
neuper@37954:     calc=[],crls=PolyEq_crls, nrls=norm_Rational},
neuper@37982:     "Script Solve_log (e_e::bool) (v_v::real) =     " ^
neuper@37981:     "(let e_e = ((Rewrite equality_power False) @@ " ^
neuper@37954:     "           (Rewrite exp_invers_log False) @@ " ^
neuper@37981:     "           (Rewrite_Set norm_Poly False)) e_e " ^
neuper@37992:     " in [e_e])"
neuper@37954:    ));
neuper@37954: *}
neuper@37906: 
neuper@37906: end