1.1 --- a/src/Tools/isac/IsacKnowledge/Integrate.ML Wed Aug 25 15:15:01 2010 +0200
1.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
1.3 @@ -1,357 +0,0 @@
1.4 -(* tools for integration over the reals
1.5 - author: Walther Neuper 050905, 08:51
1.6 - (c) due to copyright terms
1.7 -
1.8 -use"IsacKnowledge/Integrate.ML";
1.9 -use"Integrate.ML";
1.10 -
1.11 -remove_thy"Integrate";
1.12 -use_thy"IsacKnowledge/Isac";
1.13 -*)
1.14 -
1.15 -(** interface isabelle -- isac **)
1.16 -
1.17 -theory' := overwritel (!theory', [("Integrate.thy",Integrate.thy)]);
1.18 -
1.19 -(** eval functions **)
1.20 -
1.21 -val c = Free ("c", HOLogic.realT);
1.22 -(*.create a new unique variable 'c..' in a term; for use by Calc in a rls;
1.23 - an alternative to do this would be '(Try (Calculate new_c_) (new_c es__))'
1.24 - in the script; this will be possible if currying doesnt take the value
1.25 - from a variable, but the value '(new_c es__)' itself.*)
1.26 -fun new_c term =
1.27 - let fun selc var =
1.28 - case (explode o id_of) var of
1.29 - "c"::[] => true
1.30 - | "c"::"_"::is => (case (int_of_str o implode) is of
1.31 - SOME _ => true
1.32 - | NONE => false)
1.33 - | _ => false;
1.34 - fun get_coeff c = case (explode o id_of) c of
1.35 - "c"::"_"::is => (the o int_of_str o implode) is
1.36 - | _ => 0;
1.37 - val cs = filter selc (vars term);
1.38 - in
1.39 - case cs of
1.40 - [] => c
1.41 - | [c] => Free ("c_2", HOLogic.realT)
1.42 - | cs =>
1.43 - let val max_coeff = maxl (map get_coeff cs)
1.44 - in Free ("c_"^string_of_int (max_coeff + 1), HOLogic.realT) end
1.45 - end;
1.46 -
1.47 -(*WN080222
1.48 -(*("new_c", ("Integrate.new'_c", eval_new_c "#new_c_"))*)
1.49 -fun eval_new_c _ _ (p as (Const ("Integrate.new'_c",_) $ t)) _ =
1.50 - SOME ((term2str p) ^ " = " ^ term2str (new_c p),
1.51 - Trueprop $ (mk_equality (p, new_c p)))
1.52 - | eval_new_c _ _ _ _ = NONE;
1.53 -*)
1.54 -
1.55 -(*WN080222:*)
1.56 -(*("add_new_c", ("Integrate.add'_new'_c", eval_add_new_c "#add_new_c_"))
1.57 - add a new c to a term or a fun-equation;
1.58 - this is _not in_ the term, because only applied to _whole_ term*)
1.59 -fun eval_add_new_c (_:string) "Integrate.add'_new'_c" p (_:theory) =
1.60 - let val p' = case p of
1.61 - Const ("op =", T) $ lh $ rh =>
1.62 - Const ("op =", T) $ lh $ mk_add rh (new_c rh)
1.63 - | p => mk_add p (new_c p)
1.64 - in SOME ((term2str p) ^ " = " ^ term2str p',
1.65 - Trueprop $ (mk_equality (p, p')))
1.66 - end
1.67 - | eval_add_new_c _ _ _ _ = NONE;
1.68 -
1.69 -
1.70 -(*("is_f_x", ("Integrate.is'_f'_x", eval_is_f_x "is_f_x_"))*)
1.71 -fun eval_is_f_x _ _(p as (Const ("Integrate.is'_f'_x", _)
1.72 - $ arg)) _ =
1.73 - if is_f_x arg
1.74 - then SOME ((term2str p) ^ " = True",
1.75 - Trueprop $ (mk_equality (p, HOLogic.true_const)))
1.76 - else SOME ((term2str p) ^ " = False",
1.77 - Trueprop $ (mk_equality (p, HOLogic.false_const)))
1.78 - | eval_is_f_x _ _ _ _ = NONE;
1.79 -
1.80 -calclist':= overwritel (!calclist',
1.81 - [(*("new_c", ("Integrate.new'_c", eval_new_c "new_c_")),*)
1.82 - ("add_new_c", ("Integrate.add'_new'_c", eval_add_new_c "add_new_c_")),
1.83 - ("is_f_x", ("Integrate.is'_f'_x", eval_is_f_x "is_f_idextifier_"))
1.84 - ]);
1.85 -
1.86 -
1.87 -(** rulesets **)
1.88 -
1.89 -(*.rulesets for integration.*)
1.90 -val integration_rules =
1.91 - Rls {id="integration_rules", preconds = [],
1.92 - rew_ord = ("termlessI",termlessI),
1.93 - erls = Rls {id="conditions_in_integration_rules",
1.94 - preconds = [],
1.95 - rew_ord = ("termlessI",termlessI),
1.96 - erls = Erls,
1.97 - srls = Erls, calc = [],
1.98 - rules = [(*for rewriting conditions in Thm's*)
1.99 - Calc ("Atools.occurs'_in",
1.100 - eval_occurs_in "#occurs_in_"),
1.101 - Thm ("not_true",num_str not_true),
1.102 - Thm ("not_false",not_false)
1.103 - ],
1.104 - scr = EmptyScr},
1.105 - srls = Erls, calc = [],
1.106 - rules = [
1.107 - Thm ("integral_const",num_str integral_const),
1.108 - Thm ("integral_var",num_str integral_var),
1.109 - Thm ("integral_add",num_str integral_add),
1.110 - Thm ("integral_mult",num_str integral_mult),
1.111 - Thm ("integral_pow",num_str integral_pow),
1.112 - Calc ("op +", eval_binop "#add_")(*for n+1*)
1.113 - ],
1.114 - scr = EmptyScr};
1.115 -val add_new_c =
1.116 - Seq {id="add_new_c", preconds = [],
1.117 - rew_ord = ("termlessI",termlessI),
1.118 - erls = Rls {id="conditions_in_add_new_c",
1.119 - preconds = [],
1.120 - rew_ord = ("termlessI",termlessI),
1.121 - erls = Erls,
1.122 - srls = Erls, calc = [],
1.123 - rules = [Calc ("Tools.matches", eval_matches""),
1.124 - Calc ("Integrate.is'_f'_x",
1.125 - eval_is_f_x "is_f_x_"),
1.126 - Thm ("not_true",num_str not_true),
1.127 - Thm ("not_false",num_str not_false)
1.128 - ],
1.129 - scr = EmptyScr},
1.130 - srls = Erls, calc = [],
1.131 - rules = [ (*Thm ("call_for_new_c", num_str call_for_new_c),*)
1.132 - Cal1 ("Integrate.add'_new'_c", eval_add_new_c "new_c_")
1.133 - ],
1.134 - scr = EmptyScr};
1.135 -
1.136 -(*.rulesets for simplifying Integrals.*)
1.137 -
1.138 -(*.for simplify_Integral adapted from 'norm_Rational_rls'.*)
1.139 -val norm_Rational_rls_noadd_fractions =
1.140 -Rls {id = "norm_Rational_rls_noadd_fractions", preconds = [],
1.141 - rew_ord = ("dummy_ord",dummy_ord),
1.142 - erls = norm_rat_erls, srls = Erls, calc = [],
1.143 - rules = [(*Rls_ common_nominator_p_rls,!!!*)
1.144 - Rls_ (*rat_mult_div_pow original corrected WN051028*)
1.145 - (Rls {id = "rat_mult_div_pow", preconds = [],
1.146 - rew_ord = ("dummy_ord",dummy_ord),
1.147 - erls = (*FIXME.WN051028 e_rls,*)
1.148 - append_rls "e_rls-is_polyexp" e_rls
1.149 - [Calc ("Poly.is'_polyexp",
1.150 - eval_is_polyexp "")],
1.151 - srls = Erls, calc = [],
1.152 - rules = [Thm ("rat_mult",num_str rat_mult),
1.153 - (*"?a / ?b * (?c / ?d) = ?a * ?c / (?b * ?d)"*)
1.154 - Thm ("rat_mult_poly_l",num_str rat_mult_poly_l),
1.155 - (*"?c is_polyexp ==> ?c * (?a / ?b) = ?c * ?a / ?b"*)
1.156 - Thm ("rat_mult_poly_r",num_str rat_mult_poly_r),
1.157 - (*"?c is_polyexp ==> ?a / ?b * ?c = ?a * ?c / ?b"*)
1.158 -
1.159 - Thm ("real_divide_divide1_mg", real_divide_divide1_mg),
1.160 - (*"y ~= 0 ==> (u / v) / (y / z) = (u * z) / (y * v)"*)
1.161 - Thm ("real_divide_divide1_eq", real_divide_divide1_eq),
1.162 - (*"?x / (?y / ?z) = ?x * ?z / ?y"*)
1.163 - Thm ("real_divide_divide2_eq", real_divide_divide2_eq),
1.164 - (*"?x / ?y / ?z = ?x / (?y * ?z)"*)
1.165 - Calc ("HOL.divide" ,eval_cancel "#divide_"),
1.166 -
1.167 - Thm ("rat_power", num_str rat_power)
1.168 - (*"(?a / ?b) ^^^ ?n = ?a ^^^ ?n / ?b ^^^ ?n"*)
1.169 - ],
1.170 - scr = Script ((term_of o the o (parse thy)) "empty_script")
1.171 - }),
1.172 - Rls_ make_rat_poly_with_parentheses,
1.173 - Rls_ cancel_p_rls,(*FIXME:cancel_p does NOT order sometimes*)
1.174 - Rls_ rat_reduce_1
1.175 - ],
1.176 - scr = Script ((term_of o the o (parse thy)) "empty_script")
1.177 - }:rls;
1.178 -
1.179 -(*.for simplify_Integral adapted from 'norm_Rational'.*)
1.180 -val norm_Rational_noadd_fractions =
1.181 - Seq {id = "norm_Rational_noadd_fractions", preconds = [],
1.182 - rew_ord = ("dummy_ord",dummy_ord),
1.183 - erls = norm_rat_erls, srls = Erls, calc = [],
1.184 - rules = [Rls_ discard_minus_,
1.185 - Rls_ rat_mult_poly,(* removes double fractions like a/b/c *)
1.186 - Rls_ make_rat_poly_with_parentheses, (*WN0510 also in(#)below*)
1.187 - Rls_ cancel_p_rls, (*FIXME.MG:cancel_p does NOT order sometim*)
1.188 - Rls_ norm_Rational_rls_noadd_fractions,(* the main rls (#) *)
1.189 - Rls_ discard_parentheses_ (* mult only *)
1.190 - ],
1.191 - scr = Script ((term_of o the o (parse thy)) "empty_script")
1.192 - }:rls;
1.193 -
1.194 -(*.simplify terms before and after Integration such that
1.195 - ..a.x^2/2 + b.x^3/3.. is made to ..a/2.x^2 + b/3.x^3.. (and NO
1.196 - common denominator as done by norm_Rational or make_ratpoly_in.
1.197 - This is a copy from 'make_ratpoly_in' with respective reduction of rules and
1.198 - *1* expand the term, ie. distribute * and / over +
1.199 -.*)
1.200 -val separate_bdv2 =
1.201 - append_rls "separate_bdv2"
1.202 - collect_bdv
1.203 - [Thm ("separate_bdv", num_str separate_bdv),
1.204 - (*"?a * ?bdv / ?b = ?a / ?b * ?bdv"*)
1.205 - Thm ("separate_bdv_n", num_str separate_bdv_n),
1.206 - Thm ("separate_1_bdv", num_str separate_1_bdv),
1.207 - (*"?bdv / ?b = (1 / ?b) * ?bdv"*)
1.208 - Thm ("separate_1_bdv_n", num_str separate_1_bdv_n)(*,
1.209 - (*"?bdv ^^^ ?n / ?b = 1 / ?b * ?bdv ^^^ ?n"*)
1.210 - *****Thm ("real_add_divide_distrib",
1.211 - *****num_str real_add_divide_distrib)
1.212 - (*"(?x + ?y) / ?z = ?x / ?z + ?y / ?z"*)----------*)
1.213 - ];
1.214 -val simplify_Integral =
1.215 - Seq {id = "simplify_Integral", preconds = []:term list,
1.216 - rew_ord = ("dummy_ord", dummy_ord),
1.217 - erls = Atools_erls, srls = Erls,
1.218 - calc = [], (*asm_thm = [],*)
1.219 - rules = [Thm ("real_add_mult_distrib",num_str real_add_mult_distrib),
1.220 - (*"(?z1.0 + ?z2.0) * ?w = ?z1.0 * ?w + ?z2.0 * ?w"*)
1.221 - Thm ("real_add_divide_distrib",num_str real_add_divide_distrib),
1.222 - (*"(?x + ?y) / ?z = ?x / ?z + ?y / ?z"*)
1.223 - (*^^^^^ *1* ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^*)
1.224 - Rls_ norm_Rational_noadd_fractions,
1.225 - Rls_ order_add_mult_in,
1.226 - Rls_ discard_parentheses,
1.227 - (*Rls_ collect_bdv, from make_polynomial_in*)
1.228 - Rls_ separate_bdv2,
1.229 - Calc ("HOL.divide" ,eval_cancel "#divide_")
1.230 - ],
1.231 - scr = EmptyScr}:rls;
1.232 -
1.233 -
1.234 -(*simplify terms before and after Integration such that
1.235 - ..a.x^2/2 + b.x^3/3.. is made to ..a/2.x^2 + b/3.x^3.. (and NO
1.236 - common denominator as done by norm_Rational or make_ratpoly_in.
1.237 - This is a copy from 'make_polynomial_in' with insertions from
1.238 - 'make_ratpoly_in'
1.239 -THIS IS KEPT FOR COMPARISON ............................................
1.240 -* val simplify_Integral = prep_rls(
1.241 -* Seq {id = "", preconds = []:term list,
1.242 -* rew_ord = ("dummy_ord", dummy_ord),
1.243 -* erls = Atools_erls, srls = Erls,
1.244 -* calc = [], (*asm_thm = [],*)
1.245 -* rules = [Rls_ expand_poly,
1.246 -* Rls_ order_add_mult_in,
1.247 -* Rls_ simplify_power,
1.248 -* Rls_ collect_numerals,
1.249 -* Rls_ reduce_012,
1.250 -* Thm ("realpow_oneI",num_str realpow_oneI),
1.251 -* Rls_ discard_parentheses,
1.252 -* Rls_ collect_bdv,
1.253 -* (*below inserted from 'make_ratpoly_in'*)
1.254 -* Rls_ (append_rls "separate_bdv"
1.255 -* collect_bdv
1.256 -* [Thm ("separate_bdv", num_str separate_bdv),
1.257 -* (*"?a * ?bdv / ?b = ?a / ?b * ?bdv"*)
1.258 -* Thm ("separate_bdv_n", num_str separate_bdv_n),
1.259 -* Thm ("separate_1_bdv", num_str separate_1_bdv),
1.260 -* (*"?bdv / ?b = (1 / ?b) * ?bdv"*)
1.261 -* Thm ("separate_1_bdv_n", num_str separate_1_bdv_n)(*,
1.262 -* (*"?bdv ^^^ ?n / ?b = 1 / ?b * ?bdv ^^^ ?n"*)
1.263 -* Thm ("real_add_divide_distrib",
1.264 -* num_str real_add_divide_distrib)
1.265 -* (*"(?x + ?y) / ?z = ?x / ?z + ?y / ?z"*)*)
1.266 -* ]),
1.267 -* Calc ("HOL.divide" ,eval_cancel "#divide_")
1.268 -* ],
1.269 -* scr = EmptyScr
1.270 -* }:rls);
1.271 -.......................................................................*)
1.272 -
1.273 -val integration =
1.274 - Seq {id="integration", preconds = [],
1.275 - rew_ord = ("termlessI",termlessI),
1.276 - erls = Rls {id="conditions_in_integration",
1.277 - preconds = [],
1.278 - rew_ord = ("termlessI",termlessI),
1.279 - erls = Erls,
1.280 - srls = Erls, calc = [],
1.281 - rules = [],
1.282 - scr = EmptyScr},
1.283 - srls = Erls, calc = [],
1.284 - rules = [ Rls_ integration_rules,
1.285 - Rls_ add_new_c,
1.286 - Rls_ simplify_Integral
1.287 - ],
1.288 - scr = EmptyScr};
1.289 -ruleset' :=
1.290 -overwritelthy thy (!ruleset',
1.291 - [("integration_rules", prep_rls integration_rules),
1.292 - ("add_new_c", prep_rls add_new_c),
1.293 - ("simplify_Integral", prep_rls simplify_Integral),
1.294 - ("integration", prep_rls integration),
1.295 - ("separate_bdv2", separate_bdv2),
1.296 - ("norm_Rational_noadd_fractions", norm_Rational_noadd_fractions),
1.297 - ("norm_Rational_rls_noadd_fractions",
1.298 - norm_Rational_rls_noadd_fractions)
1.299 - ]);
1.300 -
1.301 -(** problems **)
1.302 -
1.303 -store_pbt
1.304 - (prep_pbt Integrate.thy "pbl_fun_integ" [] e_pblID
1.305 - (["integrate","function"],
1.306 - [("#Given" ,["functionTerm f_", "integrateBy v_"]),
1.307 - ("#Find" ,["antiDerivative F_"])
1.308 - ],
1.309 - append_rls "e_rls" e_rls [(*for preds in where_*)],
1.310 - SOME "Integrate (f_, v_)",
1.311 - [["diff","integration"]]));
1.312 -
1.313 -(*here "named" is used differently from Differentiation"*)
1.314 -store_pbt
1.315 - (prep_pbt Integrate.thy "pbl_fun_integ_nam" [] e_pblID
1.316 - (["named","integrate","function"],
1.317 - [("#Given" ,["functionTerm f_", "integrateBy v_"]),
1.318 - ("#Find" ,["antiDerivativeName F_"])
1.319 - ],
1.320 - append_rls "e_rls" e_rls [(*for preds in where_*)],
1.321 - SOME "Integrate (f_, v_)",
1.322 - [["diff","integration","named"]]));
1.323 -
1.324 -(** methods **)
1.325 -
1.326 -store_met
1.327 - (prep_met Integrate.thy "met_diffint" [] e_metID
1.328 - (["diff","integration"],
1.329 - [("#Given" ,["functionTerm f_", "integrateBy v_"]),
1.330 - ("#Find" ,["antiDerivative F_"])
1.331 - ],
1.332 - {rew_ord'="tless_true", rls'=Atools_erls, calc = [],
1.333 - srls = e_rls,
1.334 - prls=e_rls,
1.335 - crls = Atools_erls, nrls = e_rls},
1.336 -"Script IntegrationScript (f_::real) (v_::real) = \
1.337 -\ (let t_ = Take (Integral f_ D v_) \
1.338 -\ in (Rewrite_Set_Inst [(bdv,v_)] integration False) (t_::real))"
1.339 -));
1.340 -
1.341 -store_met
1.342 - (prep_met Integrate.thy "met_diffint_named" [] e_metID
1.343 - (["diff","integration","named"],
1.344 - [("#Given" ,["functionTerm f_", "integrateBy v_"]),
1.345 - ("#Find" ,["antiDerivativeName F_"])
1.346 - ],
1.347 - {rew_ord'="tless_true", rls'=Atools_erls, calc = [],
1.348 - srls = e_rls,
1.349 - prls=e_rls,
1.350 - crls = Atools_erls, nrls = e_rls},
1.351 -"Script NamedIntegrationScript (f_::real) (v_::real) (F_::real=>real) = \
1.352 -\ (let t_ = Take (F_ v_ = Integral f_ D v_) \
1.353 -\ in ((Try (Rewrite_Set_Inst [(bdv,v_)] simplify_Integral False)) @@\
1.354 -\ (Rewrite_Set_Inst [(bdv,v_)] integration False)) t_)"
1.355 -(*
1.356 -"Script NamedIntegrationScript (f_::real) (v_::real) (F_::real=>real) = \
1.357 -\ (let t_ = Take (F_ v_ = Integral f_ D v_) \
1.358 -\ in (Rewrite_Set_Inst [(bdv,v_)] integration False) t_)"
1.359 -*)
1.360 - ));