1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/Tools/isac/Knowledge/Diff.thy	Wed Aug 25 16:20:07 2010 +0200
     1.3 @@ -0,0 +1,97 @@
     1.4 +(* differentiation over the reals
     1.5 +   author: Walther Neuper
     1.6 +   000516   
     1.7 +
     1.8 +remove_thy"Diff";
     1.9 +use_thy_only"Knowledge/Diff";
    1.10 +use_thy"Knowledge/Isac";
    1.11 + *)
    1.12 +
    1.13 +Diff = Calculus + Trig + LogExp + Rational + Root + Poly + Atools +
    1.14 +
    1.15 +consts
    1.16 +
    1.17 +  d_d           :: "[real, real]=> real"
    1.18 +  sin, cos      :: "real => real"
    1.19 +(*
    1.20 +  log, ln       :: "real => real"
    1.21 +  nlog          :: "[real, real] => real"
    1.22 +  exp           :: "real => real"         ("E'_ ^^^ _" 80)
    1.23 +*)
    1.24 +  (*descriptions in the related problems*)
    1.25 +  derivativeEq  :: bool => una
    1.26 +
    1.27 +  (*predicates*)
    1.28 +  primed        :: "'a => 'a" (*"primed A" -> "A'"*)
    1.29 +
    1.30 +  (*the CAS-commands, eg. "Diff (2*x^^^3, x)", 
    1.31 +			  "Differentiate (A = s * (a - s), s)"*)
    1.32 +  Diff           :: "[real * real] => real"
    1.33 +  Differentiate  :: "[bool * real] => bool"
    1.34 +
    1.35 +  (*subproblem and script-name*)
    1.36 +  differentiate  :: "[ID * (ID list) * ID, real,real] => real"
    1.37 +               	   ("(differentiate (_)/ (_ _ ))" 9)
    1.38 +  DiffScr        :: "[real,real,  real] => real"
    1.39 +                   ("((Script DiffScr (_ _ =))// (_))" 9)
    1.40 +  DiffEqScr   :: "[bool,real,  bool] => bool"
    1.41 +                   ("((Script DiffEqScr (_ _ =))// (_))" 9)
    1.42 +
    1.43 +
    1.44 +rules (*stated as axioms, todo: prove as theorems
    1.45 +        'bdv' is a constant on the meta-level  *)
    1.46 +  diff_const     "[| Not (bdv occurs_in a) |] ==> d_d bdv a = 0"
    1.47 +  diff_var       "d_d bdv bdv = 1"
    1.48 +  diff_prod_const"[| Not (bdv occurs_in u) |] ==> \
    1.49 +					\d_d bdv (u * v) = u * d_d bdv v"
    1.50 +
    1.51 +  diff_sum       "d_d bdv (u + v)     = d_d bdv u + d_d bdv v"
    1.52 +  diff_dif       "d_d bdv (u - v)     = d_d bdv u - d_d bdv v"
    1.53 +  diff_prod      "d_d bdv (u * v)     = d_d bdv u * v + u * d_d bdv v"
    1.54 +  diff_quot      "Not (v = 0) ==> (d_d bdv (u / v) = \
    1.55 +	          \(d_d bdv u * v - u * d_d bdv v) / v ^^^ 2)"
    1.56 +
    1.57 +  diff_sin       "d_d bdv (sin bdv)   = cos bdv"
    1.58 +  diff_sin_chain "d_d bdv (sin u)     = cos u * d_d bdv u"
    1.59 +  diff_cos       "d_d bdv (cos bdv)   = - sin bdv"
    1.60 +  diff_cos_chain "d_d bdv (cos u)     = - sin u * d_d bdv u"
    1.61 +  diff_pow       "d_d bdv (bdv ^^^ n) = n * (bdv ^^^ (n - 1))"
    1.62 +  diff_pow_chain "d_d bdv (u ^^^ n)   = n * (u ^^^ (n - 1)) * d_d bdv u"
    1.63 +  diff_ln        "d_d bdv (ln bdv)    = 1 / bdv"
    1.64 +  diff_ln_chain  "d_d bdv (ln u)      = d_d bdv u / u"
    1.65 +  diff_exp       "d_d bdv (exp bdv)   = exp bdv"
    1.66 +  diff_exp_chain "d_d bdv (exp u)     = exp u * d_d x u"
    1.67 +(*
    1.68 +  diff_sqrt      "d_d bdv (sqrt bdv)  = 1 / (2 * sqrt bdv)"
    1.69 +  diff_sqrt_chain"d_d bdv (sqrt u)    = d_d bdv u / (2 * sqrt u)"
    1.70 +*)
    1.71 +  (*...*)
    1.72 +
    1.73 +  frac_conv       "[| bdv occurs_in b; 0 < n |] ==> \
    1.74 +		  \ a / (b ^^^ n) = a * b ^^^ (-n)"
    1.75 +  frac_sym_conv   "n < 0 ==> a * b ^^^ n = a / b ^^^ (-n)"
    1.76 +
    1.77 +  sqrt_conv_bdv   "sqrt bdv = bdv ^^^ (1 / 2)"
    1.78 +  sqrt_conv_bdv_n "sqrt (bdv ^^^ n) = bdv ^^^ (n / 2)"
    1.79 +  sqrt_conv       "bdv occurs_in u ==> sqrt u = u ^^^ (1 / 2)"
    1.80 +  sqrt_sym_conv   "u ^^^ (a / 2) = sqrt (u ^^^ a)"
    1.81 +
    1.82 +  root_conv       "bdv occurs_in u ==> nroot n u = u ^^^ (1 / n)"
    1.83 +  root_sym_conv   "u ^^^ (a / b) = nroot b (u ^^^ a)"
    1.84 +
    1.85 +  realpow_pow_bdv "(bdv ^^^ b) ^^^ c = bdv ^^^ (b * c)"
    1.86 +
    1.87 +end
    1.88 +
    1.89 +(* a variant of the derivatives defintion:
    1.90 +
    1.91 +  d_d            :: "(real => real) => (real => real)"
    1.92 +
    1.93 +  advantages:
    1.94 +(1) no variable 'bdv' on the meta-level required
    1.95 +(2) chain_rule "d_d (%x. (u (v x))) = (%x. (d_d u)) (v x) * d_d v"
    1.96 +(3) and no specialized chain-rules required like
    1.97 +    diff_sin_chain "d_d bdv (sin u)    = cos u * d_d bdv u"
    1.98 +
    1.99 +  disadvantage: d_d (%x. 1 + x^2) = ... differs from high-school notation
   1.100 +*)