(* integration over the reals

    author: Walther Neuper

    050814, 08:51

    (c) due to copyright terms

 remove_thy"Integrate";

 use_thy"~/proto2/isac/src/sml/IsacKnowledge/Integrate";

 use_thy"~/proto2/isac/src/sml/IsacKnowledge/Isac";

 *)

 Integrate = Diff +

 consts

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

 rules (*stated as axioms, todo: prove as theorems

         'bdv' is a constant on the meta-level  *)

   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)"

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

 end