(* tools for integration over the reals

   author: Walther Neuper 050905, 08:51

   (c) due to copyright terms

use"IsacKnowledge/Integrate.ML";

use"Integrate.ML";

remove_thy"Integrate";

use_thy"IsacKnowledge/Isac";

*)

(** 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; for use by Calc in a rls;

   an alternative to do this would be '(Try (Calculate new_c_) (new_c es__))'

   in the script; this will be possible if currying doesnt take the value

   from a variable, but the value '(new_c es__)' itself.*)

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

(*.rulesets for integration.*)

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

(*.rulesets for simplifying Integrals.*)

(*.for simplify_Integral adapted from 'norm_Rational_rls'.*)

val norm_Rational_rls_noadd_fractions = prep_rls(

Rls {id = "norm_Rational_rls_noadd_fractions", preconds = [], 

     rew_ord = ("dummy_ord",dummy_ord), 

     erls = norm_rat_erls, srls = Erls, calc = [],

     rules = [(*Rls_ common_nominator_p_rls,!!!*)

	      Rls_ (*rat_mult_div_pow original corrected WN051028*)

		  (Rls {id = "rat_mult_div_pow", preconds = [], 

		       rew_ord = ("dummy_ord",dummy_ord), 

		       erls = (*FIXME.WN051028 e_rls,*)

		       append_rls "e_rls-is_polyexp" e_rls

				  [Calc ("Poly.is'_polyexp", 

					 eval_is_polyexp "")],

				  srls = Erls, calc = [],

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

	       (*"?a / ?b * (?c / ?d) = ?a * ?c / (?b * ?d)"*)

	       Thm ("rat_mult_poly_l",num_str rat_mult_poly_l),

	       (*"?c is_polyexp ==> ?c * (?a / ?b) = ?c * ?a / ?b"*)

	       Thm ("rat_mult_poly_r",num_str rat_mult_poly_r),

	       (*"?c is_polyexp ==> ?a / ?b * ?c = ?a * ?c / ?b"*)

	       Thm ("real_divide_divide1_mg", real_divide_divide1_mg),

	       (*"y ~= 0 ==> (u / v) / (y / z) = (u * z) / (y * v)"*)

	       Thm ("real_divide_divide1_eq", real_divide_divide1_eq),

	       (*"?x / (?y / ?z) = ?x * ?z / ?y"*)

	       Thm ("real_divide_divide2_eq", real_divide_divide2_eq),

	       (*"?x / ?y / ?z = ?x / (?y * ?z)"*)

	       Calc ("HOL.divide"  ,eval_cancel "#divide_"),

	       Thm ("rat_power", num_str rat_power)

		(*"(?a / ?b) ^^^ ?n = ?a ^^^ ?n / ?b ^^^ ?n"*)

	       ],

      scr = Script ((term_of o the o (parse thy)) "empty_script")

      }),

		Rls_ make_rat_poly_with_parentheses,

		Rls_ cancel_p_rls,(*FIXME:cancel_p does NOT order sometimes*)

		Rls_ rat_reduce_1

		],

       scr = Script ((term_of o the o (parse thy)) "empty_script")

       }:rls);

(*.for simplify_Integral adapted from 'norm_Rational'.*)

val norm_Rational_noadd_fractions = prep_rls(

   Seq {id = "norm_Rational_noadd_fractions", preconds = [], 

       rew_ord = ("dummy_ord",dummy_ord), 

       erls = norm_rat_erls, srls = Erls, calc = [],

       rules = [Rls_ discard_minus_,

		Rls_ rat_mult_poly,(* removes double fractions like a/b/c    *)

		Rls_ make_rat_poly_with_parentheses, (*WN0510 also in(#)below*)

		Rls_ cancel_p_rls, (*FIXME.MG:cancel_p does NOT order sometim*)

		Rls_ norm_Rational_rls_noadd_fractions,(* the main rls (#)   *)

		Rls_ discard_parentheses_ (* mult only                       *)

		],

       scr = Script ((term_of o the o (parse thy)) "empty_script")

       }:rls);

(*.simplify terms before and after Integration such that  

   ..a.x^2/2 + b.x^3/3.. is made to ..a/2.x^2 + b/3.x^3.. (and NO

   common denominator as done by norm_Rational or make_ratpoly_in.

   This is a copy from 'make_ratpoly_in' with respective reduction of rules.*)

val simplify_Integral = prep_rls(

  Seq {id = "simplify_Integral", preconds = []:term list, 

       rew_ord = ("dummy_ord", dummy_ord),

      erls = Atools_erls, srls = Erls,

      calc = [], (*asm_thm = [],*)

      rules = [Rls_ norm_Rational_noadd_fractions,

	       Rls_ order_add_mult_in,

	       Rls_ discard_parentheses,

	       (*Rls_ collect_bdv, from make_polynomial_in*)

	       Rls_ (append_rls "separate_bdv"

			 collect_bdv

			 [Thm ("separate_bdv", num_str separate_bdv),

			  (*"?a * ?bdv / ?b = ?a / ?b * ?bdv"*)

			  Thm ("separate_bdv_n", num_str separate_bdv_n),

			  Thm ("separate_1_bdv", num_str separate_1_bdv),

			  (*"?bdv / ?b = (1 / ?b) * ?bdv"*)

			  Thm ("separate_1_bdv_n", num_str separate_1_bdv_n)(*,

			  (*"?bdv ^^^ ?n / ?b = 1 / ?b * ?bdv ^^^ ?n"*)

			  Thm ("real_add_divide_distrib", 

			       num_str real_add_divide_distrib)

			  (*"(?x + ?y) / ?z = ?x / ?z + ?y / ?z"*)----------*)

			  ]),

	       Calc ("HOL.divide"  ,eval_cancel "#divide_")

	       ],

      scr = EmptyScr}:rls);      

(*simplify terms before and after Integration such that  

   ..a.x^2/2 + b.x^3/3.. is made to ..a/2.x^2 + b/3.x^3.. (and NO

   common denominator as done by norm_Rational or make_ratpoly_in.

   This is a copy from 'make_polynomial_in' with insertions from 

   'make_ratpoly_in' 

THIS IS KEPT FOR COMPARISON ............................................   

val simplify_Integral = prep_rls(

  Seq {id = "", preconds = []:term list, 

       rew_ord = ("dummy_ord", dummy_ord),

      erls = Atools_erls, srls = Erls,

      calc = [], (*asm_thm = [],*)

      rules = [Rls_ expand_poly,

	       Rls_ order_add_mult_in,

	       Rls_ simplify_power,

	       Rls_ collect_numerals,

	       Rls_ reduce_012,

	       Thm ("realpow_oneI",num_str realpow_oneI),

	       Rls_ discard_parentheses,

	       Rls_ collect_bdv,

	       (*below inserted from 'make_ratpoly_in'*)

	       Rls_ (append_rls "separate_bdv"

			 collect_bdv

			 [Thm ("separate_bdv", num_str separate_bdv),

			  (*"?a * ?bdv / ?b = ?a / ?b * ?bdv"*)

			  Thm ("separate_bdv_n", num_str separate_bdv_n),

			  Thm ("separate_1_bdv", num_str separate_1_bdv),

			  (*"?bdv / ?b = (1 / ?b) * ?bdv"*)

			  Thm ("separate_1_bdv_n", num_str separate_1_bdv_n)(*,

			  (*"?bdv ^^^ ?n / ?b = 1 / ?b * ?bdv ^^^ ?n"*)

			  Thm ("real_add_divide_distrib", 

				 num_str real_add_divide_distrib)

			   (*"(?x + ?y) / ?z = ?x / ?z + ?y / ?z"*)*)

			  ]),

	       Calc ("HOL.divide"  ,eval_cancel "#divide_")

	       ],

      scr = EmptyScr

      }:rls); 

.......................................................................*)     

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_ simplify_Integral

			    ],

		   scr = EmptyScr});

ruleset' := 

overwritel (!ruleset', 

	    [("integration_rules", integration_rules),

	     ("add_new_c", add_new_c),

	     ("simplify_Integral", simplify_Integral),

	     ("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_)"

 ));