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

 (*("is_f_x", ("Integrate.is'_f'_x", eval_is_f_x "is_f_x_"))*)

 fun eval_is_f_x _ _(p as (Const ("Integrate.is'_f'_x", _)

 					   $ arg)) _ =

     if is_f_x arg

     then Some ((term2str p) ^ " = True",

 	       Trueprop $ (mk_equality (p, HOLogic.true_const)))

     else Some ((term2str p) ^ " = False",

 	       Trueprop $ (mk_equality (p, HOLogic.false_const)))

   | eval_is_f_x _ _ _ _ = None;

 calclist':= overwritel (!calclist', 

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

     ("is_f_x", ("Integrate.is'_f'_x", eval_is_f_x "is_f_idextifier_"))

     ]);

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

 					Calc ("Integrate.is'_f'_x", 

 					 eval_is_f_x "is_f_x_"),

 					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"  ,["antiDerivativeName 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_ = Take (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"  ,["antiDerivativeName 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=>real) = \

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

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

  ));