(* tests on integration over the reals

   author: Walther Neuper

   050814, 08:51

   (c) due to copyright terms

use"~/proto2/isac/src/smltest/IsacKnowledge/integrate.sml";

*)

"-----------------------------------------------------------------";

"table of contents -----------------------------------------------";

"-----------------------------------------------------------------";

"----------- parsing ---------------------------------------------";

"----------- set up rewriting ------------------------------------";

"----------- integrate by rewriting ------------------------------";

"----------- set up ruleset --------------------------------------";

"----------- integrate by ruleset --------------------------------";

"-----------------------------------------------------------------";

"-----------------------------------------------------------------";

"-----------------------------------------------------------------";

"----------- parsing ---------------------------------------------";

"----------- parsing ---------------------------------------------";

"----------- parsing ---------------------------------------------";

fun str2t thy str = (term_of o the o (parse thy )) str;

fun term2s thy t = Sign.string_of_term (sign_of thy) t;

val t = str2t Integrate.thy "Integral x D x";

val t = str2t Integrate.thy "Integral x^^^2 D x";

atomty thy t;

"----------- set up rewriting ------------------------------------";

"----------- set up rewriting ------------------------------------";

"----------- set up rewriting ------------------------------------";

val conditions_in_integration_rules = 

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

		   rew_ord = ("termlessI",termlessI), 

		   erls = Erls, 

		   srls = Erls, calc = [],

		   rules = [Calc ("Atools.occurs'_in", 

				  eval_occurs_in "#occurs_in_"),

			    Thm ("not_true",num_str not_true),

			    Thm ("not_false",not_false)

			    ],

		   scr = EmptyScr});

ruleset' := overwritel (!ruleset', [("conditions_in_integration_rules", 

				     conditions_in_integration_rules)]);

"----------- integrate by rewriting ------------------------------";

"----------- integrate by rewriting ------------------------------";

"----------- integrate by rewriting ------------------------------";

fun rewrit subs thm str = 

    fst (the (rewrite_inst "Integrate.thy" "tless_true" 

			   "conditions_in_integration_rules" 

			   true subs thm str));

val thm = ("integral_const","");

val str = rewrit [("bdv","x::real")] thm "Integral 1 D x";

val str = rewrit [("bdv","x::real")] thm "Integral M'/EJ D x";

val str = (rewrit [("bdv","x::real")] thm "Integral x D x") 

    handle OPTION => "no rewrite -- OK";

val thm = ("integral_var","");

val str = rewrit [("bdv","x::real")] thm "Integral x D x";

val str = (rewrit [("bdv","x::real")] thm "Integral a D x")

    handle OPTION => "no rewrite -- OK";

val thm = ("integral_add","");

val str = rewrit [("bdv","x::real")] thm "Integral x + 1 D x";

val thm = ("integral_mult","");

val str = rewrit [("bdv","x::real")] thm "Integral M'/EJ * x^^^3 D x";

val str = (rewrit [("bdv","x::real")] thm "Integral x * x D x")

    handle OPTION => "no rewrite -- OK";

val thm = ("integral_pow","");

val str = rewrit [("bdv","x::real")] thm "Integral x^^^3 D x";

"----------- set up ruleset --------------------------------------";

"----------- set up ruleset --------------------------------------";

"----------- set up ruleset --------------------------------------";

val integration_rules = 

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

		   rew_ord = ("termlessI",termlessI), 

		   erls = conditions_in_integration_rules, 

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

			    Rls_ make_polynomial

			    ],

		   scr = EmptyScr});

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

"----------- integrate by ruleset --------------------------------";

"----------- integrate by ruleset --------------------------------";

"----------- integrate by ruleset --------------------------------";

fun rewrite_se subs rls str = 

    fst (the (rewrite_set_inst "Integrate.thy" true subs rls str));

val subs = [("bdv","x::real")];

val rls = "integration_rules";

val str = rewrite_se subs rls "Integral 1 D x";