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