(* differentiation over the reals

    author: Walther Neuper

    000516   

 remove_thy"Diff";

 use_thy_only"Knowledge/Diff";

 use_thy"Knowledge/Isac";

  *)

 Diff = Calculus + Trig + LogExp + Rational + Root + Poly + Atools +

 consts

   d_d           :: "[real, real]=> real"

   sin, cos      :: "real => real"

 (*

   log, ln       :: "real => real"

   nlog          :: "[real, real] => real"

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

 *)

   (*descriptions in the related problems*)

   derivativeEq  :: bool => una

   (*predicates*)

   primed        :: "'a => 'a" (*"primed A" -> "A'"*)

   (*the CAS-commands, eg. "Diff (2*x^^^3, x)", 

 			  "Differentiate (A = s * (a - s), s)"*)

   Diff           :: "[real * real] => real"

   Differentiate  :: "[bool * real] => bool"

   (*subproblem and script-name*)

   differentiate  :: "[ID * (ID list) * ID, real,real] => real"

                	   ("(differentiate (_)/ (_ _ ))" 9)

   DiffScr        :: "[real,real,  real] => real"

                    ("((Script DiffScr (_ _ =))// (_))" 9)

   DiffEqScr   :: "[bool,real,  bool] => bool"

                    ("((Script DiffEqScr (_ _ =))// (_))" 9)

 rules (*stated as axioms, todo: prove as theorems

         'bdv' is a constant on the meta-level  *)

   diff_const     "[| Not (bdv occurs_in a) |] ==> d_d bdv a = 0"

   diff_var       "d_d bdv bdv = 1"

   diff_prod_const"[| Not (bdv occurs_in u) |] ==> \

 					\d_d bdv (u * v) = u * d_d bdv v"

   diff_sum       "d_d bdv (u + v)     = d_d bdv u + d_d bdv v"

   diff_dif       "d_d bdv (u - v)     = d_d bdv u - d_d bdv v"

   diff_prod      "d_d bdv (u * v)     = d_d bdv u * v + u * d_d bdv v"

   diff_quot      "Not (v = 0) ==> (d_d bdv (u / v) = \

 	          \(d_d bdv u * v - u * d_d bdv v) / v ^^^ 2)"

   diff_sin       "d_d bdv (sin bdv)   = cos bdv"

   diff_sin_chain "d_d bdv (sin u)     = cos u * d_d bdv u"

   diff_cos       "d_d bdv (cos bdv)   = - sin bdv"

   diff_cos_chain "d_d bdv (cos u)     = - sin u * d_d bdv u"

   diff_pow       "d_d bdv (bdv ^^^ n) = n * (bdv ^^^ (n - 1))"

   diff_pow_chain "d_d bdv (u ^^^ n)   = n * (u ^^^ (n - 1)) * d_d bdv u"

   diff_ln        "d_d bdv (ln bdv)    = 1 / bdv"

   diff_ln_chain  "d_d bdv (ln u)      = d_d bdv u / u"

   diff_exp       "d_d bdv (exp bdv)   = exp bdv"

   diff_exp_chain "d_d bdv (exp u)     = exp u * d_d x u"

 (*

   diff_sqrt      "d_d bdv (sqrt bdv)  = 1 / (2 * sqrt bdv)"

   diff_sqrt_chain"d_d bdv (sqrt u)    = d_d bdv u / (2 * sqrt u)"

 *)

   (*...*)

   frac_conv       "[| bdv occurs_in b; 0 < n |] ==> \

 		  \ a / (b ^^^ n) = a * b ^^^ (-n)"

   frac_sym_conv   "n < 0 ==> a * b ^^^ n = a / b ^^^ (-n)"

   sqrt_conv_bdv   "sqrt bdv = bdv ^^^ (1 / 2)"

   sqrt_conv_bdv_n "sqrt (bdv ^^^ n) = bdv ^^^ (n / 2)"

   sqrt_conv       "bdv occurs_in u ==> sqrt u = u ^^^ (1 / 2)"

   sqrt_sym_conv   "u ^^^ (a / 2) = sqrt (u ^^^ a)"

   root_conv       "bdv occurs_in u ==> nroot n u = u ^^^ (1 / n)"

   root_sym_conv   "u ^^^ (a / b) = nroot b (u ^^^ a)"

   realpow_pow_bdv "(bdv ^^^ b) ^^^ c = bdv ^^^ (b * c)"

 end

 (* a variant of the derivatives defintion:

   d_d            :: "(real => real) => (real => real)"

   advantages:

 (1) no variable 'bdv' on the meta-level required

 (2) chain_rule "d_d (%x. (u (v x))) = (%x. (d_d u)) (v x) * d_d v"

 (3) and no specialized chain-rules required like

     diff_sin_chain "d_d bdv (sin u)    = cos u * d_d bdv u"

   disadvantage: d_d (%x. 1 + x^2) = ... differs from high-school notation

 *)