1.1 --- a/src/Tools/isac/IsacKnowledge/Diff.thy Wed Aug 25 15:15:01 2010 +0200
1.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
1.3 @@ -1,97 +0,0 @@
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"IsacKnowledge/Diff";
1.10 -use_thy"IsacKnowledge/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 -*)