(* 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_only"~/proto2/isac/src/sml/IsacKnowledge/Integrate";

 remove_thy"Typefix";

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

 *)

 Integrate = Diff +

 consts

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

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

   (*new Descriptions in the problem*)

   integrateBy      :: real => una

   antiDerivative   :: real => una

   (*the CAS-command*)

   Integrate        :: "[real * real] => real"  (* "integrate (2*x^^^3, x)" *)

   (*Script-names*)

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

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

   NamedIntegrationScript :: "[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)"

   call_for_new_c    "Not (matches (u + new_c v) a) ==> a = a + new_c a"

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

 end