(* all outcommented in order to demonstrate authoring:

    WN071203

 *)

 theory LogExp imports PolyEq begin

 consts

   ln     :: "real => real"

   exp    :: "real => real"         ("E'_ ^^^ _" 80)

 (*--------------------------------------------------*) 

   alog   :: "[real, real] => real" ("_ log _" 90)

   (*Script-names*)

   Solve'_log    :: "[bool,real,        bool list]  

 				    => bool list"

                   ("((Script Solve'_log (_ _=))//(_))" 9)

 axiomatization where

   equality_pow:    "0 < a ==> (l = r) = (a^^^l = a^^^r)" and

   (* this is what students   ^^^^^^^... are told to do *)

   equality_power:  "((a log b) = c) = (a^^^(a log b) = a^^^c)" and

   exp_invers_log:  "a^^^(a log b) = b"

 ML \<open>

 val thy = @{theory};

 \<close>

 (** problems **)

 setup \<open>KEStore_Elems.add_pbts

   [(Specify.prep_pbt thy "pbl_test_equ_univ_log" [] Celem.e_pblID

       (["logarithmic","univariate","equation"],

         [("#Given",["equality e_e","solveFor v_v"]),

           ("#Where",["matches ((?a log ?v_v) = ?b) e_e"]),

           ("#Find" ,["solutions v_v'i'"]),

           ("#With" ,["||(lhs (Subst (v'i', v_v) e_e) - " ^

 	          "  (rhs (Subst (v'i', v_v) e_e) || < eps)"])],

         PolyEq_prls, SOME "solve (e_e::bool, v_v)", [["Equation","solve_log"]]))]\<close>

 (** methods **)

 setup \<open>KEStore_Elems.add_mets

     [Specify.prep_met thy "met_equ_log" [] Celem.e_metID

       (["Equation","solve_log"],

         [("#Given" ,["equality e_e","solveFor v_v"]),

           ("#Where" ,["matches ((?a log ?v_v) = ?b) e_e"]),

           ("#Find"  ,["solutions v_v'i'"])],

         {rew_ord' = "termlessI", rls' = PolyEq_erls, srls = Rule.e_rls, prls = PolyEq_prls, calc = [],

           crls = PolyEq_crls, errpats = [], nrls = norm_Rational},

         "Script Solve_log (e_e::bool) (v_v::real) =     " ^

         "(let e_e = ((Rewrite ''equality_power'' False) @@ " ^

         "           (Rewrite ''exp_invers_log'' False) @@  " ^

         "           (Rewrite_Set ''norm_Poly'' False)) e_e " ^

         " in [e_e])")]

 \<close>

 end