author | wneuper |
Sat, 20 Aug 2005 21:20:16 +0200 | |
changeset 2918 | cac1f942e1a1 |
parent 2916 | 730089aebfcf |
child 3747 | 2fae9b163442 |
permissions | -rw-r--r-- |
wneuper@2854 | 1 |
(* integration over the reals |
wneuper@2854 | 2 |
author: Walther Neuper |
wneuper@2854 | 3 |
050814, 08:51 |
wneuper@2854 | 4 |
(c) due to copyright terms |
wneuper@2854 | 5 |
|
wneuper@2854 | 6 |
remove_thy"Integrate"; |
wneuper@2854 | 7 |
use_thy"~/proto2/isac/src/sml/IsacKnowledge/Integrate"; |
wneuper@2863 | 8 |
use_thy_only"~/proto2/isac/src/sml/IsacKnowledge/Integrate"; |
wneuper@2910 | 9 |
|
wneuper@2910 | 10 |
remove_thy"Typefix"; |
wneuper@2854 | 11 |
use_thy"~/proto2/isac/src/sml/IsacKnowledge/Isac"; |
wneuper@2854 | 12 |
*) |
wneuper@2854 | 13 |
|
wneuper@2854 | 14 |
Integrate = Diff + |
wneuper@2854 | 15 |
|
wneuper@2854 | 16 |
consts |
wneuper@2854 | 17 |
|
wneuper@2899 | 18 |
Integral :: "[real, real]=> real" ("Integral _ D _" 91) |
wneuper@2899 | 19 |
new'_c :: "real => real" ("new'_c _" 66) |
wneuper@2854 | 20 |
|
wneuper@2863 | 21 |
(*new Descriptions in the problem*) |
wneuper@2899 | 22 |
integrateBy :: real => una |
wneuper@2899 | 23 |
antiDerivative :: real => una |
wneuper@2863 | 24 |
|
wneuper@2863 | 25 |
(*the CAS-command*) |
wneuper@2899 | 26 |
Integrate :: "[real * real] => real" (* "integrate (2*x^^^3, x)" *) |
wneuper@2863 | 27 |
|
wneuper@2872 | 28 |
(*Script-names*) |
wneuper@2872 | 29 |
IntegrationScript :: "[real,real, real] => real" |
wneuper@2918 | 30 |
("((Script IntegrationScript (_ _ =))// (_))" 9) |
wneuper@2872 | 31 |
NamedIntegrationScript :: "[real,real,real, bool] => bool" |
wneuper@2872 | 32 |
("((Script NamedIntegrationScript (_ _ _=))// (_))" 9) |
wneuper@2863 | 33 |
|
wneuper@2863 | 34 |
rules |
wneuper@2863 | 35 |
(*stated as axioms, todo: prove as theorems |
wneuper@2863 | 36 |
'bdv' is a constant handled on the meta-level |
wneuper@2863 | 37 |
specifically as a 'bound variable' *) |
wneuper@2863 | 38 |
|
wneuper@2910 | 39 |
integral_const "Not (bdv occurs_in u) ==> Integral u D bdv = u * bdv" |
wneuper@2854 | 40 |
integral_var "Integral bdv D bdv = bdv ^^^ 2 / 2" |
wneuper@2854 | 41 |
|
wneuper@2854 | 42 |
integral_add "Integral (u + v) D bdv = \ |
wneuper@2854 | 43 |
\(Integral u D bdv) + (Integral v D bdv)" |
wneuper@2854 | 44 |
integral_mult "[| Not (bdv occurs_in u); bdv occurs_in v |] ==> \ |
wneuper@2854 | 45 |
\Integral (u * v) D bdv = u * (Integral v D bdv)" |
wneuper@2916 | 46 |
call_for_new_c "Not (matches (u + new_c v) a) ==> a = a + new_c a" |
wneuper@2854 | 47 |
|
wneuper@2854 | 48 |
integral_pow "Integral bdv ^^^ n D bdv = bdv ^^^ (n+1) / (n + 1)" |
wneuper@2854 | 49 |
|
wneuper@2854 | 50 |
end |