1 (* differentiation over the reals |
|
2 author: Walther Neuper |
|
3 000516 |
|
4 |
|
5 remove_thy"Diff"; |
|
6 use_thy_only"IsacKnowledge/Diff"; |
|
7 use_thy"IsacKnowledge/Isac"; |
|
8 *) |
|
9 |
|
10 Diff = Calculus + Trig + LogExp + Rational + Root + Poly + Atools + |
|
11 |
|
12 consts |
|
13 |
|
14 d_d :: "[real, real]=> real" |
|
15 sin, cos :: "real => real" |
|
16 (* |
|
17 log, ln :: "real => real" |
|
18 nlog :: "[real, real] => real" |
|
19 exp :: "real => real" ("E'_ ^^^ _" 80) |
|
20 *) |
|
21 (*descriptions in the related problems*) |
|
22 derivativeEq :: bool => una |
|
23 |
|
24 (*predicates*) |
|
25 primed :: "'a => 'a" (*"primed A" -> "A'"*) |
|
26 |
|
27 (*the CAS-commands, eg. "Diff (2*x^^^3, x)", |
|
28 "Differentiate (A = s * (a - s), s)"*) |
|
29 Diff :: "[real * real] => real" |
|
30 Differentiate :: "[bool * real] => bool" |
|
31 |
|
32 (*subproblem and script-name*) |
|
33 differentiate :: "[ID * (ID list) * ID, real,real] => real" |
|
34 ("(differentiate (_)/ (_ _ ))" 9) |
|
35 DiffScr :: "[real,real, real] => real" |
|
36 ("((Script DiffScr (_ _ =))// (_))" 9) |
|
37 DiffEqScr :: "[bool,real, bool] => bool" |
|
38 ("((Script DiffEqScr (_ _ =))// (_))" 9) |
|
39 |
|
40 |
|
41 rules (*stated as axioms, todo: prove as theorems |
|
42 'bdv' is a constant on the meta-level *) |
|
43 diff_const "[| Not (bdv occurs_in a) |] ==> d_d bdv a = 0" |
|
44 diff_var "d_d bdv bdv = 1" |
|
45 diff_prod_const"[| Not (bdv occurs_in u) |] ==> \ |
|
46 \d_d bdv (u * v) = u * d_d bdv v" |
|
47 |
|
48 diff_sum "d_d bdv (u + v) = d_d bdv u + d_d bdv v" |
|
49 diff_dif "d_d bdv (u - v) = d_d bdv u - d_d bdv v" |
|
50 diff_prod "d_d bdv (u * v) = d_d bdv u * v + u * d_d bdv v" |
|
51 diff_quot "Not (v = 0) ==> (d_d bdv (u / v) = \ |
|
52 \(d_d bdv u * v - u * d_d bdv v) / v ^^^ 2)" |
|
53 |
|
54 diff_sin "d_d bdv (sin bdv) = cos bdv" |
|
55 diff_sin_chain "d_d bdv (sin u) = cos u * d_d bdv u" |
|
56 diff_cos "d_d bdv (cos bdv) = - sin bdv" |
|
57 diff_cos_chain "d_d bdv (cos u) = - sin u * d_d bdv u" |
|
58 diff_pow "d_d bdv (bdv ^^^ n) = n * (bdv ^^^ (n - 1))" |
|
59 diff_pow_chain "d_d bdv (u ^^^ n) = n * (u ^^^ (n - 1)) * d_d bdv u" |
|
60 diff_ln "d_d bdv (ln bdv) = 1 / bdv" |
|
61 diff_ln_chain "d_d bdv (ln u) = d_d bdv u / u" |
|
62 diff_exp "d_d bdv (exp bdv) = exp bdv" |
|
63 diff_exp_chain "d_d bdv (exp u) = exp u * d_d x u" |
|
64 (* |
|
65 diff_sqrt "d_d bdv (sqrt bdv) = 1 / (2 * sqrt bdv)" |
|
66 diff_sqrt_chain"d_d bdv (sqrt u) = d_d bdv u / (2 * sqrt u)" |
|
67 *) |
|
68 (*...*) |
|
69 |
|
70 frac_conv "[| bdv occurs_in b; 0 < n |] ==> \ |
|
71 \ a / (b ^^^ n) = a * b ^^^ (-n)" |
|
72 frac_sym_conv "n < 0 ==> a * b ^^^ n = a / b ^^^ (-n)" |
|
73 |
|
74 sqrt_conv_bdv "sqrt bdv = bdv ^^^ (1 / 2)" |
|
75 sqrt_conv_bdv_n "sqrt (bdv ^^^ n) = bdv ^^^ (n / 2)" |
|
76 sqrt_conv "bdv occurs_in u ==> sqrt u = u ^^^ (1 / 2)" |
|
77 sqrt_sym_conv "u ^^^ (a / 2) = sqrt (u ^^^ a)" |
|
78 |
|
79 root_conv "bdv occurs_in u ==> nroot n u = u ^^^ (1 / n)" |
|
80 root_sym_conv "u ^^^ (a / b) = nroot b (u ^^^ a)" |
|
81 |
|
82 realpow_pow_bdv "(bdv ^^^ b) ^^^ c = bdv ^^^ (b * c)" |
|
83 |
|
84 end |
|
85 |
|
86 (* a variant of the derivatives defintion: |
|
87 |
|
88 d_d :: "(real => real) => (real => real)" |
|
89 |
|
90 advantages: |
|
91 (1) no variable 'bdv' on the meta-level required |
|
92 (2) chain_rule "d_d (%x. (u (v x))) = (%x. (d_d u)) (v x) * d_d v" |
|
93 (3) and no specialized chain-rules required like |
|
94 diff_sin_chain "d_d bdv (sin u) = cos u * d_d bdv u" |
|
95 |
|
96 disadvantage: d_d (%x. 1 + x^2) = ... differs from high-school notation |
|
97 *) |
|