(* 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";

*)

val thy = Integrate.thy;

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

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

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

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

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

"----------- test new_c ------------------------------------------";

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

"----------- check probem type -----------------------------------";

"----------- check Scripts ---------------------------------------";

"----------- me method [Diff,integration] ------------------------";

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

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

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

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

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

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

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

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

val t = str2t "Integral x D x";

val t = str2t "Integral x^^^2 D x";

atomty thy t;

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

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

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

val conditions_in_integration_rules =

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};

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

fun rewrit thm str = 

    fst (the (rewrite_inst_ Integrate.thy tless_true 

			   conditions_in_integration_rules 

			   true subs thm str));

val str = rewrit integral_const (str2t "Integral 1 D x"); term2s str;

val str = rewrit integral_const (str2t  "Integral M'/EJ D x"); term2s str;

val str = (rewrit integral_const (str2t "Integral x D x")) 

    handle OPTION => str2t "no_rewrite";

val str = rewrit integral_var (str2t "Integral x D x"); term2s str;

val str = (rewrit integral_var (str2t "Integral a D x"))

    handle OPTION => str2t "no_rewrite";

val str = rewrit integral_add (str2t "Integral x + 1 D x"); term2s str;

val str = rewrit integral_mult (str2t "Integral M'/EJ * x^^^3 D x");term2s str;

val str = (rewrit integral_mult (str2t "Integral x * x D x"))

    handle OPTION => str2t "no_rewrite";

val str = rewrit integral_pow (str2t "Integral x^^^3 D x"); term2s str;

"----------- test new_c ------------------------------------------";

"----------- test new_c ------------------------------------------";

"----------- test new_c ------------------------------------------";

val term = str2t "x^^^2*c + c_2";

val cc = new_c term;

if term2s cc = "c_3" then () else raise error "integrate.sml: new_c ???";

val term = str2t "new_c (c * x^^^2 + c_2)";

val Some (_,t') = eval_new_c 0 0 term 0;

if term2s t' = "new_c c * x ^^^ 2 + c_2 = c_3" then ()

else raise error "integrate.sml: eval_new_c ???";

val t = str2t "matches (?u + new_c ?v) (x ^^^ 2 / 2)";

val Some (_,t') = eval_matches "" "Tools.matches" t thy; term2s t';

if term2s t' = "matches (?u + new_c ?v) (x ^^^ 2 / 2) = False" then ()

else raise error "integrate.sml: matches new_c = False";

val t = str2t "matches (?u + new_c ?v) (x ^^^ 2 / 2 + new_c x ^^^ 2 / 2)";

val Some (_,t') = eval_matches "" "Tools.matches" t thy; term2s t';

if term2s t'="matches (?u + new_c ?v) (x ^^^ 2 / 2 + new_c x ^^^ 2 / 2) = True"

then () else raise error "integrate.sml: matches new_c = True";

val conditions_in_integration =

Rls {id="conditions_in_integration", 

			       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};

fun rewrit thm str = 

    fst (the (rewrite_inst_ Integrate.thy tless_true 

			    conditions_in_integration true subs thm str));

val str = rewrit call_for_new_c (str2t "x ^^^ 2 / 2"); term2s str;

val str = (rewrit call_for_new_c str)

    handle OPTION =>  str2t "no_rewrite";;

"----------- 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 x D x";

val str = rewrite_se subs rls "Integral c * x ^^^ 2 + c_2 D x";

if str = "c * (x ^^^ 3 / 3) + c_2 * x"

then () else raise error "integrate.sml: diff.behav. in integration_rules";

val rls = "add_new_c";

val str = rewrite_se subs rls "c * (x ^^^ 3 / 3) + c_2 * x";

if str = "c * (x ^^^ 3 / 3) + c_2 * x + c_3" then () 

else raise error "integrate.sml: diff.behav. in add_new_c";

val rls = "integration";

val str = rewrite_se subs rls "Integral c * x ^^^ 2 + c_2 D x";

if str = "c * (x ^^^ 3 / 3) + c_2 * x + c_3"

then () else raise error "integrate.sml: diff.behav. in integration";

"----------- check probem type -----------------------------------";

"----------- check probem type -----------------------------------";

"----------- check probem type -----------------------------------";

val model = {Given =["functionTerm f_", "integrateBy v_"],

	   Where =[],

	   Find  =["antiDerivative F_"],

	   With  =[],

	   Relate=[]}:string ppc;

val chkmodel = ((map (the o (parse Integrate.thy))) o ppc2list) model;

val t1 = (term_of o hd) chkmodel;

val t2 = (term_of o hd o tl) chkmodel;

val t3 = (term_of o hd o tl o tl) chkmodel;

case t3 of Const ("Integrate.antiDerivative", _) $ _ => ()

	 | _ => raise error "integrate.sml: Integrate.antiDerivative ???";

show_ptyps();

val pbl = get_pbt ["integrate","function"];

case #cas pbl of Some (Const ("Integrate.Integrate",_) $ _) => ()

	 | _ => raise error "integrate.sml: Integrate.Integrate ???";

"----------- check Scripts ---------------------------------------";

"----------- check Scripts ---------------------------------------";

"----------- check Scripts ---------------------------------------";

val str = 

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

\  (let t_ = Integral f_ D v_                                 \

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

val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;

atomty thy sc;

val str = 

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

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

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

val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;

atomty thy sc;

show_mets();

"----------- me method [Diff,integration] ---------------------";

"----------- me method [Diff,integration] ---------------------";

"----------- me method [Diff,integration] ---------------------";

val fmz = ["functionTerm (x^^^2 + 1)", 

	   "integrateBy x","antiDerivative FF"];

val (dI',pI',mI') =

  ("Integrate.thy",["integrate","function"],

   ["Diff","integration"]);

val p = e_pos'; val c = []; 

val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];

val (p,_,f,nxt,_,pt) = me nxt p c pt;

val (p,_,f,nxt,_,pt) = me nxt p c pt;

val (p,_,f,nxt,_,pt) = me nxt p c pt;

val (p,_,f,nxt,_,pt) = me nxt p c pt;

val (p,_,f,nxt,_,pt) = me nxt p c pt;

val (p,_,f,nxt,_,pt) = me nxt p c pt;

val (p,_,f,nxt,_,pt) = me nxt p c pt;

val (p,_,f,nxt,_,pt) = me nxt p c pt;(*---> Empty_Tac*)