(* 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)

 axioms

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

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

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

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

 ML {*

 val thy = @{theory};

 (** problems **)

 store_pbt

  (prep_pbt thy "pbl_test_equ_univ_log" [] 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"]]));

 *}

 ML {*

 (** methods **)

 store_met

  (prep_met thy "met_equ_log" [] 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=e_rls,prls=PolyEq_prls,

     calc=[],crls=PolyEq_crls, 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])"

    ));

 *}

 end