|
1 (* integration over the reals |
|
2 author: Walther Neuper |
|
3 050814, 08:51 |
|
4 (c) due to copyright terms |
|
5 |
|
6 remove_thy"Integrate"; |
|
7 use_thy"Knowledge/Integrate"; |
|
8 use_thy_only"Knowledge/Integrate"; |
|
9 |
|
10 remove_thy"Typefix"; |
|
11 use_thy"Knowledge/Isac"; |
|
12 *) |
|
13 |
|
14 Integrate = Diff + |
|
15 |
|
16 consts |
|
17 |
|
18 Integral :: "[real, real]=> real" ("Integral _ D _" 91) |
|
19 (*new'_c :: "real => real" ("new'_c _" 66)*) |
|
20 is'_f'_x :: "real => bool" ("_ is'_f'_x" 10) |
|
21 |
|
22 (*descriptions in the related problems*) |
|
23 integrateBy :: real => una |
|
24 antiDerivative :: real => una |
|
25 antiDerivativeName :: (real => real) => una |
|
26 |
|
27 (*the CAS-command, eg. "Integrate (2*x^^^3, x)"*) |
|
28 Integrate :: "[real * real] => real" |
|
29 |
|
30 (*Script-names*) |
|
31 IntegrationScript :: "[real,real, real] => real" |
|
32 ("((Script IntegrationScript (_ _ =))// (_))" 9) |
|
33 NamedIntegrationScript :: "[real,real, real=>real, bool] => bool" |
|
34 ("((Script NamedIntegrationScript (_ _ _=))// (_))" 9) |
|
35 |
|
36 rules |
|
37 (*stated as axioms, todo: prove as theorems |
|
38 'bdv' is a constant handled on the meta-level |
|
39 specifically as a 'bound variable' *) |
|
40 |
|
41 integral_const "Not (bdv occurs_in u) ==> Integral u D bdv = u * bdv" |
|
42 integral_var "Integral bdv D bdv = bdv ^^^ 2 / 2" |
|
43 |
|
44 integral_add "Integral (u + v) D bdv = \ |
|
45 \(Integral u D bdv) + (Integral v D bdv)" |
|
46 integral_mult "[| Not (bdv occurs_in u); bdv occurs_in v |] ==> \ |
|
47 \Integral (u * v) D bdv = u * (Integral v D bdv)" |
|
48 (*WN080222: this goes into sub-terms, too ... |
|
49 call_for_new_c "[| Not (matches (u + new_c v) a); Not (a is_f_x) |] ==> \ |
|
50 \a = a + new_c a" |
|
51 *) |
|
52 integral_pow "Integral bdv ^^^ n D bdv = bdv ^^^ (n+1) / (n + 1)" |
|
53 |
|
54 end |