(* 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)

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

  (*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); Not (a is_f_x) |] ==> \

		    \a = a + new_c a"

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

end