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

rules

  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 {*

(** problems **)

store_pbt

 (prep_pbt (theory "LogExp") "pbl_test_equ_univ_log" [] e_pblID

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

  [("#Given",["equality e_","solveFor v_"]),

   ("#Where",["matches ((?a log ?v_) = ?b) e_"]),

   ("#Find" ,["solutions v_i_"]),

   ("#With" ,["||(lhs (Subst (v_i_,v_) e_) - " ^

	      "  (rhs (Subst (v_i_,v_) e_) || < eps)"])

   ],

  PolyEq_prls, SOME "solve (e_::bool, v_)",

  [["Equation","solve_log"]]));

(** methods **)

store_met

 (prep_met (theory "LogExp") "met_equ_log" [] e_metID

 (["Equation","solve_log"],

  [("#Given" ,["equality e_","solveFor v_"]),

   ("#Where" ,["matches ((?a log ?v_) = ?b) e_"]),

   ("#Find"  ,["solutions 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_::bool) (v_::real) =     " ^

    "(let e_ = ((Rewrite equality_power False) @@ " ^

    "           (Rewrite exp_invers_log False) @@ " ^

    "           (Rewrite_Set norm_Poly False)) e_ " ^

    " in [e_])"

   ));

*}

end