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