(* all outcommented in order to demonstrate authoring:

   WN071203

*)

theory LogExp imports PolyEq begin

consts

  ln     :: "real => real"

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

axiomatization where

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

  (* this is what students   \<up> \<up> ^... are told to do *)

  equality_power:  "((a log b) = c) = (a \<up> (a log b) = a \<up> c)" and

  exp_invers_log:  "a \<up> (a log b) = b"

(** problems **)

problem pbl_test_equ_univ_log : "logarithmic/univariate/equation" =

  \<open>PolyEq_prls\<close>

  Method_Ref: "Equation/solve_log"

  CAS: "solve (e_e::bool, v_v)"

  Given: "equality e_e" "solveFor v_v"

  Where: "matches ((?a log ?v_v) = ?b) e_e"

  Find: "solutions v_v'i'"

  (*With: FIXME !? "||(lhs (Subst (v'i', v_v) e_e) - (rhs (Subst (v'i', v_v) e_e) || < eps)" *)

(** methods **)

partial_function (tailrec) solve_log :: "bool \<Rightarrow> real \<Rightarrow> bool list"

  where

"solve_log e_e v_v = (

  let

    e_e = (

      (Rewrite ''equality_power'') #>

      (Rewrite ''exp_invers_log'') #>

      (Rewrite_Set ''norm_Poly'') ) e_e

  in

    [e_e])"

method met_equ_log : "Equation/solve_log" =

  \<open>{rew_ord = "termlessI", rls' = PolyEq_erls, prog_rls = Rule_Set.empty, where_rls = PolyEq_prls, calc = [],

    errpats = [], rew_rls = norm_Rational}\<close>

  Program: solve_log.simps

  Given: "equality e_e" "solveFor v_v"

  Where: "matches ((?a log ?v_v) = ?b) e_e"

  Find: "solutions v_v'i'"

ML \<open>

\<close> ML \<open>

\<close>

end