(* tools for integration over the reals

   author: Walther Neuper

   050814, 08:51

   (c) due to copyright terms

use"~/proto2/isac/src/sml/IsacKnowledge/Integrate.ML";

*)

(** interface isabelle -- isac **)

theory' := overwritel (!theory', [("Integrate.thy",Integrate.thy)]);

theorem' := overwritel (!theorem',

[("integral_const",num_str integral_const),

 ("integral_var",num_str integral_var),

 ("integral_add",num_str integral_add),

 ("integral_mult",num_str integral_mult),

 ("call_for_new_c",num_str call_for_new_c),

 ("integral_pow",num_str integral_pow)

]);

(** eval functions **)

val c = Free ("c", HOLogic.realT);

(*.create a new unique variable 'c..' in a term.*)

fun new_c term = 

    let fun selc var = 

	    case (explode o id_of) var of

		"c"::[] => true

	      |	"c"::"_"::is => (case (int_of_str o implode) is of

				     Some _ => true

				   | None => false)

              | _ => false;

	fun get_coeff c = case (explode o id_of) c of

	      		      "c"::"_"::is => (the o int_of_str o implode) is

			    | _ => 0;

        val cs = filter selc (vars term);

    in 

	case cs of

	    [] => c

	  | [c] => Free ("c_2", HOLogic.realT)

	  | cs => 

	    let val max_coeff = maxl (map get_coeff cs)

	    in Free ("c_"^string_of_int (max_coeff + 1), HOLogic.realT) end

    end;

(*("new_c", ("Integrate.new'_c", eval_new_c "new_c_"))*)

fun eval_new_c _ _ (p as (Const ("Integrate.new'_c",_) $ t)) _ =

     Some ((term2str p) ^ " = " ^ term2str (new_c p),

	  Trueprop $ (mk_equality (p, new_c p)))

  | eval_new_c _ _ _ _ = None;

calclist':= overwritel (!calclist', 

   [("new_c", ("Integrate.new'_c", eval_new_c "new_c_"))

    ]);

(** rulesets **)

val integration_rules = 

    prep_rls (Rls {id="integration_rules", preconds = [], 

		   rew_ord = ("termlessI",termlessI), 

		   erls = Rls {id="conditions_in_integration_rules", 

			       preconds = [], 

			       rew_ord = ("termlessI",termlessI), 

			       erls = Erls, 

			       srls = Erls, calc = [],

			       rules = [(*for rewriting conditions in Thm's*)

					Calc ("Atools.occurs'_in", 

					      eval_occurs_in "#occurs_in_"),

					Thm ("not_true",num_str not_true),

					Thm ("not_false",not_false)

					],

			       scr = EmptyScr}, 

		   srls = Erls, calc = [],

		   rules = [

			    Thm ("integral_const",num_str integral_const),

			    Thm ("integral_var",num_str integral_var),

			    Thm ("integral_add",num_str integral_add),

			    Thm ("integral_mult",num_str integral_mult),

			    Thm ("integral_pow",num_str integral_pow),

			    Calc ("op +", eval_binop "#add_")(*for n+1*)

			    ],

		   scr = EmptyScr});

val add_new_c = 

    prep_rls (Seq {id="add_new_c", preconds = [], 

		   rew_ord = ("termlessI",termlessI), 

		   erls = Rls {id="conditions_in_add_new_c", 

			       preconds = [], 

			       rew_ord = ("termlessI",termlessI), 

			       erls = Erls, 

			       srls = Erls, calc = [],

			       rules = [Calc ("Tools.matches", eval_matches""),

					Thm ("not_true",num_str not_true),

					Thm ("not_false",num_str not_false)

					],

			       scr = EmptyScr}, 

		   srls = Erls, calc = [],

		   rules = [ Thm ("call_for_new_c", num_str call_for_new_c),

			     Calc("Integrate.new'_c", eval_new_c "new_c_")

			    ],

		   scr = EmptyScr});

val integration = 

    prep_rls (Seq {id="integration", preconds = [], 

		   rew_ord = ("termlessI",termlessI), 

		   erls = Rls {id="conditions_in_integration", 

			       preconds = [], 

			       rew_ord = ("termlessI",termlessI), 

			       erls = Erls, 

			       srls = Erls, calc = [],

			       rules = [],

			       scr = EmptyScr}, 

		   srls = Erls, calc = [],

		   rules = [ Rls_ integration_rules,

			     Rls_ add_new_c,

			     Rls_ norm_Poly

			    ],

		   scr = EmptyScr});

ruleset' := overwritel (!ruleset', [("integration_rules", integration_rules),

				    ("add_new_c", add_new_c),

				    ("integration", integration)]);

(** problems **)

store_pbt

 (prep_pbt Integrate.thy

 (["integrate","function"],

  [("#Given" ,["functionTerm f_", "integrateBy v_"]),

   ("#Find"  ,["antiDerivative F_"])

  ],

  append_rls "e_rls" e_rls [(*for preds in where_*)], 

  Some "Integrate (f_, v_)", 

  [["Diff","integration"]]));

store_pbt

 (prep_pbt Integrate.thy

 (["named","integrate","function"],

  [("#Given" ,["functionTerm f_", "integrateBy v_"]),

   ("#Find"  ,["antiDerivative F_"])

  ],

  append_rls "e_rls" e_rls [(*for preds in where_*)], 

  Some "Integrate (f_, v_)", 

  [["Diff","integration","named"]]));

(** methods **)

store_met

    (prep_met Integrate.thy

	      (["Diff","integration"],

	       [("#Given" ,["functionTerm f_", "integrateBy v_"]),

		("#Find"  ,["antiDerivative F_"])

		],

	       {rew_ord'="tless_true", rls'=Atools_erls, calc = [], 

		srls = e_rls, 

		prls=e_rls,

	     crls = Atools_erls, nrls = e_rls},

"Script IntegrationScript (f_::real) (v_::real) =                \

\  (let t_ = Integral f_ D v_                                    \

\   in (Rewrite_Set_Inst [(bdv,v_)] integration False) (t_::real))"

));

store_met

    (prep_met Integrate.thy

	      (["Diff","integration","named"],

	       [("#Given" ,["functionTerm f_", "integrateBy v_"]),

		("#Find"  ,["antiDerivative F_"])

		],

	       {rew_ord'="tless_true", rls'=Atools_erls, calc = [], 

		srls = e_rls, 

		prls=e_rls,

		crls = Atools_erls, nrls = e_rls},

"Script NamedIntegrationScript (f_::real) (v_::real) (F_::real) = \

\  (let t_ = (F_ = Integral f_ D v_)                                 \

\   in (Rewrite_Set_Inst [(bdv,v_)] integration False) t_)"

 ));