1.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
1.2 +++ b/src/Tools/isac/Knowledge/Integrate.thy Wed Aug 25 16:20:07 2010 +0200
1.3 @@ -0,0 +1,54 @@
1.4 +(* integration over the reals
1.5 + author: Walther Neuper
1.6 + 050814, 08:51
1.7 + (c) due to copyright terms
1.8 +
1.9 +remove_thy"Integrate";
1.10 +use_thy"Knowledge/Integrate";
1.11 +use_thy_only"Knowledge/Integrate";
1.12 +
1.13 +remove_thy"Typefix";
1.14 +use_thy"Knowledge/Isac";
1.15 +*)
1.16 +
1.17 +Integrate = Diff +
1.18 +
1.19 +consts
1.20 +
1.21 + Integral :: "[real, real]=> real" ("Integral _ D _" 91)
1.22 +(*new'_c :: "real => real" ("new'_c _" 66)*)
1.23 + is'_f'_x :: "real => bool" ("_ is'_f'_x" 10)
1.24 +
1.25 + (*descriptions in the related problems*)
1.26 + integrateBy :: real => una
1.27 + antiDerivative :: real => una
1.28 + antiDerivativeName :: (real => real) => una
1.29 +
1.30 + (*the CAS-command, eg. "Integrate (2*x^^^3, x)"*)
1.31 + Integrate :: "[real * real] => real"
1.32 +
1.33 + (*Script-names*)
1.34 + IntegrationScript :: "[real,real, real] => real"
1.35 + ("((Script IntegrationScript (_ _ =))// (_))" 9)
1.36 + NamedIntegrationScript :: "[real,real, real=>real, bool] => bool"
1.37 + ("((Script NamedIntegrationScript (_ _ _=))// (_))" 9)
1.38 +
1.39 +rules
1.40 +(*stated as axioms, todo: prove as theorems
1.41 + 'bdv' is a constant handled on the meta-level
1.42 + specifically as a 'bound variable' *)
1.43 +
1.44 + integral_const "Not (bdv occurs_in u) ==> Integral u D bdv = u * bdv"
1.45 + integral_var "Integral bdv D bdv = bdv ^^^ 2 / 2"
1.46 +
1.47 + integral_add "Integral (u + v) D bdv = \
1.48 + \(Integral u D bdv) + (Integral v D bdv)"
1.49 + integral_mult "[| Not (bdv occurs_in u); bdv occurs_in v |] ==> \
1.50 + \Integral (u * v) D bdv = u * (Integral v D bdv)"
1.51 +(*WN080222: this goes into sub-terms, too ...
1.52 + call_for_new_c "[| Not (matches (u + new_c v) a); Not (a is_f_x) |] ==> \
1.53 + \a = a + new_c a"
1.54 +*)
1.55 + integral_pow "Integral bdv ^^^ n D bdv = bdv ^^^ (n+1) / (n + 1)"
1.56 +
1.57 +end
1.58 \ No newline at end of file