(* integration over the reals

    author: Walther Neuper

    050814, 08:51

    (c) due to copyright terms

 remove_thy"Integrate";

 use_thy"Knowledge/Integrate";

 use_thy_only"Knowledge/Integrate";

 remove_thy"Typefix";

 use_thy"Knowledge/Isac";

 *)

 Integrate = Diff +

 consts

   Integral            :: "[real, real]=> real" ("Integral _ D _" 91)

 (*new'_c	      :: "real => real"        ("new'_c _" 66)*)

   is'_f'_x            :: "real => bool"        ("_ is'_f'_x" 10)

   (*descriptions in the related problems*)

   integrateBy         :: real => una

   antiDerivative      :: real => una

   antiDerivativeName  :: (real => real) => una

   (*the CAS-command, eg. "Integrate (2*x^^^3, x)"*)

   Integrate           :: "[real * real] => real"

   (*Script-names*)

   IntegrationScript      :: "[real,real,  real] => real"

                   ("((Script IntegrationScript (_ _ =))// (_))" 9)

   NamedIntegrationScript :: "[real,real, real=>real,  bool] => bool"

                   ("((Script NamedIntegrationScript (_ _ _=))// (_))" 9)

 rules 

 (*stated as axioms, todo: prove as theorems

   'bdv' is a constant handled on the meta-level 

    specifically as a 'bound variable'            *)

   integral_const    "Not (bdv occurs_in u) ==> Integral u D bdv = u * bdv"

   integral_var      "Integral bdv D bdv = bdv ^^^ 2 / 2"

   integral_add      "Integral (u + v) D bdv = \

 		    \(Integral u D bdv) + (Integral v D bdv)"

   integral_mult     "[| Not (bdv occurs_in u); bdv occurs_in v |] ==> \

 		    \Integral (u * v) D bdv = u * (Integral v D bdv)"

 (*WN080222: this goes into sub-terms, too ...

   call_for_new_c    "[| Not (matches (u + new_c v) a); Not (a is_f_x) |] ==> \

 		    \a = a + new_c a"

 *)

   integral_pow      "Integral bdv ^^^ n D bdv = bdv ^^^ (n+1) / (n + 1)"

 end