1 (* tools for integration over the reals
2 author: Walther Neuper 050905, 08:51
3 (c) due to copyright terms
5 use"Knowledge/Integrate.ML";
9 use_thy"Knowledge/Isac";
12 (** interface isabelle -- isac **)
14 theory' := overwritel (!theory', [("Integrate.thy",Integrate.thy)]);
16 (** eval functions **)
18 val c = Free ("c", HOLogic.realT);
19 (*.create a new unique variable 'c..' in a term; for use by Calc in a rls;
20 an alternative to do this would be '(Try (Calculate new_c_) (new_c es__))'
21 in the script; this will be possible if currying doesnt take the value
22 from a variable, but the value '(new_c es__)' itself.*)
25 case (explode o id_of) var of
27 | "c"::"_"::is => (case (int_of_str o implode) is of
31 fun get_coeff c = case (explode o id_of) c of
32 "c"::"_"::is => (the o int_of_str o implode) is
34 val cs = filter selc (vars term);
38 | [c] => Free ("c_2", HOLogic.realT)
40 let val max_coeff = maxl (map get_coeff cs)
41 in Free ("c_"^string_of_int (max_coeff + 1), HOLogic.realT) end
45 (*("new_c", ("Integrate.new'_c", eval_new_c "#new_c_"))*)
46 fun eval_new_c _ _ (p as (Const ("Integrate.new'_c",_) $ t)) _ =
47 SOME ((term2str p) ^ " = " ^ term2str (new_c p),
48 Trueprop $ (mk_equality (p, new_c p)))
49 | eval_new_c _ _ _ _ = NONE;
53 (*("add_new_c", ("Integrate.add'_new'_c", eval_add_new_c "#add_new_c_"))
54 add a new c to a term or a fun-equation;
55 this is _not in_ the term, because only applied to _whole_ term*)
56 fun eval_add_new_c (_:string) "Integrate.add'_new'_c" p (_:theory) =
57 let val p' = case p of
58 Const ("op =", T) $ lh $ rh =>
59 Const ("op =", T) $ lh $ mk_add rh (new_c rh)
60 | p => mk_add p (new_c p)
61 in SOME ((term2str p) ^ " = " ^ term2str p',
62 Trueprop $ (mk_equality (p, p')))
64 | eval_add_new_c _ _ _ _ = NONE;
67 (*("is_f_x", ("Integrate.is'_f'_x", eval_is_f_x "is_f_x_"))*)
68 fun eval_is_f_x _ _(p as (Const ("Integrate.is'_f'_x", _)
71 then SOME ((term2str p) ^ " = True",
72 Trueprop $ (mk_equality (p, HOLogic.true_const)))
73 else SOME ((term2str p) ^ " = False",
74 Trueprop $ (mk_equality (p, HOLogic.false_const)))
75 | eval_is_f_x _ _ _ _ = NONE;
77 calclist':= overwritel (!calclist',
78 [(*("new_c", ("Integrate.new'_c", eval_new_c "new_c_")),*)
79 ("add_new_c", ("Integrate.add'_new'_c", eval_add_new_c "add_new_c_")),
80 ("is_f_x", ("Integrate.is'_f'_x", eval_is_f_x "is_f_idextifier_"))
86 (*.rulesets for integration.*)
87 val integration_rules =
88 Rls {id="integration_rules", preconds = [],
89 rew_ord = ("termlessI",termlessI),
90 erls = Rls {id="conditions_in_integration_rules",
92 rew_ord = ("termlessI",termlessI),
94 srls = Erls, calc = [],
95 rules = [(*for rewriting conditions in Thm's*)
96 Calc ("Atools.occurs'_in",
97 eval_occurs_in "#occurs_in_"),
98 Thm ("not_true",num_str not_true),
99 Thm ("not_false",not_false)
102 srls = Erls, calc = [],
104 Thm ("integral_const",num_str integral_const),
105 Thm ("integral_var",num_str integral_var),
106 Thm ("integral_add",num_str integral_add),
107 Thm ("integral_mult",num_str integral_mult),
108 Thm ("integral_pow",num_str integral_pow),
109 Calc ("op +", eval_binop "#add_")(*for n+1*)
113 Seq {id="add_new_c", preconds = [],
114 rew_ord = ("termlessI",termlessI),
115 erls = Rls {id="conditions_in_add_new_c",
117 rew_ord = ("termlessI",termlessI),
119 srls = Erls, calc = [],
120 rules = [Calc ("Tools.matches", eval_matches""),
121 Calc ("Integrate.is'_f'_x",
122 eval_is_f_x "is_f_x_"),
123 Thm ("not_true",num_str not_true),
124 Thm ("not_false",num_str not_false)
127 srls = Erls, calc = [],
128 rules = [ (*Thm ("call_for_new_c", num_str call_for_new_c),*)
129 Cal1 ("Integrate.add'_new'_c", eval_add_new_c "new_c_")
133 (*.rulesets for simplifying Integrals.*)
135 (*.for simplify_Integral adapted from 'norm_Rational_rls'.*)
136 val norm_Rational_rls_noadd_fractions =
137 Rls {id = "norm_Rational_rls_noadd_fractions", preconds = [],
138 rew_ord = ("dummy_ord",dummy_ord),
139 erls = norm_rat_erls, srls = Erls, calc = [],
140 rules = [(*Rls_ common_nominator_p_rls,!!!*)
141 Rls_ (*rat_mult_div_pow original corrected WN051028*)
142 (Rls {id = "rat_mult_div_pow", preconds = [],
143 rew_ord = ("dummy_ord",dummy_ord),
144 erls = (*FIXME.WN051028 e_rls,*)
145 append_rls "e_rls-is_polyexp" e_rls
146 [Calc ("Poly.is'_polyexp",
147 eval_is_polyexp "")],
148 srls = Erls, calc = [],
149 rules = [Thm ("rat_mult",num_str rat_mult),
150 (*"?a / ?b * (?c / ?d) = ?a * ?c / (?b * ?d)"*)
151 Thm ("rat_mult_poly_l",num_str rat_mult_poly_l),
152 (*"?c is_polyexp ==> ?c * (?a / ?b) = ?c * ?a / ?b"*)
153 Thm ("rat_mult_poly_r",num_str rat_mult_poly_r),
154 (*"?c is_polyexp ==> ?a / ?b * ?c = ?a * ?c / ?b"*)
156 Thm ("real_divide_divide1_mg", real_divide_divide1_mg),
157 (*"y ~= 0 ==> (u / v) / (y / z) = (u * z) / (y * v)"*)
158 Thm ("real_divide_divide1_eq", real_divide_divide1_eq),
159 (*"?x / (?y / ?z) = ?x * ?z / ?y"*)
160 Thm ("real_divide_divide2_eq", real_divide_divide2_eq),
161 (*"?x / ?y / ?z = ?x / (?y * ?z)"*)
162 Calc ("HOL.divide" ,eval_cancel "#divide_"),
164 Thm ("rat_power", num_str rat_power)
165 (*"(?a / ?b) ^^^ ?n = ?a ^^^ ?n / ?b ^^^ ?n"*)
167 scr = Script ((term_of o the o (parse thy)) "empty_script")
169 Rls_ make_rat_poly_with_parentheses,
170 Rls_ cancel_p_rls,(*FIXME:cancel_p does NOT order sometimes*)
173 scr = Script ((term_of o the o (parse thy)) "empty_script")
176 (*.for simplify_Integral adapted from 'norm_Rational'.*)
177 val norm_Rational_noadd_fractions =
178 Seq {id = "norm_Rational_noadd_fractions", preconds = [],
179 rew_ord = ("dummy_ord",dummy_ord),
180 erls = norm_rat_erls, srls = Erls, calc = [],
181 rules = [Rls_ discard_minus_,
182 Rls_ rat_mult_poly,(* removes double fractions like a/b/c *)
183 Rls_ make_rat_poly_with_parentheses, (*WN0510 also in(#)below*)
184 Rls_ cancel_p_rls, (*FIXME.MG:cancel_p does NOT order sometim*)
185 Rls_ norm_Rational_rls_noadd_fractions,(* the main rls (#) *)
186 Rls_ discard_parentheses_ (* mult only *)
188 scr = Script ((term_of o the o (parse thy)) "empty_script")
191 (*.simplify terms before and after Integration such that
192 ..a.x^2/2 + b.x^3/3.. is made to ..a/2.x^2 + b/3.x^3.. (and NO
193 common denominator as done by norm_Rational or make_ratpoly_in.
194 This is a copy from 'make_ratpoly_in' with respective reduction of rules and
195 *1* expand the term, ie. distribute * and / over +
198 append_rls "separate_bdv2"
200 [Thm ("separate_bdv", num_str separate_bdv),
201 (*"?a * ?bdv / ?b = ?a / ?b * ?bdv"*)
202 Thm ("separate_bdv_n", num_str separate_bdv_n),
203 Thm ("separate_1_bdv", num_str separate_1_bdv),
204 (*"?bdv / ?b = (1 / ?b) * ?bdv"*)
205 Thm ("separate_1_bdv_n", num_str separate_1_bdv_n)(*,
206 (*"?bdv ^^^ ?n / ?b = 1 / ?b * ?bdv ^^^ ?n"*)
207 *****Thm ("real_add_divide_distrib",
208 *****num_str real_add_divide_distrib)
209 (*"(?x + ?y) / ?z = ?x / ?z + ?y / ?z"*)----------*)
211 val simplify_Integral =
212 Seq {id = "simplify_Integral", preconds = []:term list,
213 rew_ord = ("dummy_ord", dummy_ord),
214 erls = Atools_erls, srls = Erls,
215 calc = [], (*asm_thm = [],*)
216 rules = [Thm ("real_add_mult_distrib",num_str real_add_mult_distrib),
217 (*"(?z1.0 + ?z2.0) * ?w = ?z1.0 * ?w + ?z2.0 * ?w"*)
218 Thm ("real_add_divide_distrib",num_str real_add_divide_distrib),
219 (*"(?x + ?y) / ?z = ?x / ?z + ?y / ?z"*)
220 (*^^^^^ *1* ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^*)
221 Rls_ norm_Rational_noadd_fractions,
222 Rls_ order_add_mult_in,
223 Rls_ discard_parentheses,
224 (*Rls_ collect_bdv, from make_polynomial_in*)
226 Calc ("HOL.divide" ,eval_cancel "#divide_")
231 (*simplify terms before and after Integration such that
232 ..a.x^2/2 + b.x^3/3.. is made to ..a/2.x^2 + b/3.x^3.. (and NO
233 common denominator as done by norm_Rational or make_ratpoly_in.
234 This is a copy from 'make_polynomial_in' with insertions from
236 THIS IS KEPT FOR COMPARISON ............................................
237 * val simplify_Integral = prep_rls(
238 * Seq {id = "", preconds = []:term list,
239 * rew_ord = ("dummy_ord", dummy_ord),
240 * erls = Atools_erls, srls = Erls,
241 * calc = [], (*asm_thm = [],*)
242 * rules = [Rls_ expand_poly,
243 * Rls_ order_add_mult_in,
244 * Rls_ simplify_power,
245 * Rls_ collect_numerals,
247 * Thm ("realpow_oneI",num_str realpow_oneI),
248 * Rls_ discard_parentheses,
250 * (*below inserted from 'make_ratpoly_in'*)
251 * Rls_ (append_rls "separate_bdv"
253 * [Thm ("separate_bdv", num_str separate_bdv),
254 * (*"?a * ?bdv / ?b = ?a / ?b * ?bdv"*)
255 * Thm ("separate_bdv_n", num_str separate_bdv_n),
256 * Thm ("separate_1_bdv", num_str separate_1_bdv),
257 * (*"?bdv / ?b = (1 / ?b) * ?bdv"*)
258 * Thm ("separate_1_bdv_n", num_str separate_1_bdv_n)(*,
259 * (*"?bdv ^^^ ?n / ?b = 1 / ?b * ?bdv ^^^ ?n"*)
260 * Thm ("real_add_divide_distrib",
261 * num_str real_add_divide_distrib)
262 * (*"(?x + ?y) / ?z = ?x / ?z + ?y / ?z"*)*)
264 * Calc ("HOL.divide" ,eval_cancel "#divide_")
268 .......................................................................*)
271 Seq {id="integration", preconds = [],
272 rew_ord = ("termlessI",termlessI),
273 erls = Rls {id="conditions_in_integration",
275 rew_ord = ("termlessI",termlessI),
277 srls = Erls, calc = [],
280 srls = Erls, calc = [],
281 rules = [ Rls_ integration_rules,
283 Rls_ simplify_Integral
287 overwritelthy thy (!ruleset',
288 [("integration_rules", prep_rls integration_rules),
289 ("add_new_c", prep_rls add_new_c),
290 ("simplify_Integral", prep_rls simplify_Integral),
291 ("integration", prep_rls integration),
292 ("separate_bdv2", separate_bdv2),
293 ("norm_Rational_noadd_fractions", norm_Rational_noadd_fractions),
294 ("norm_Rational_rls_noadd_fractions",
295 norm_Rational_rls_noadd_fractions)
301 (prep_pbt (theory "Integrate") "pbl_fun_integ" [] e_pblID
302 (["integrate","function"],
303 [("#Given" ,["functionTerm f_", "integrateBy v_"]),
304 ("#Find" ,["antiDerivative F_"])
306 append_rls "e_rls" e_rls [(*for preds in where_*)],
307 SOME "Integrate (f_, v_)",
308 [["diff","integration"]]));
310 (*here "named" is used differently from Differentiation"*)
312 (prep_pbt (theory "Integrate") "pbl_fun_integ_nam" [] e_pblID
313 (["named","integrate","function"],
314 [("#Given" ,["functionTerm f_", "integrateBy v_"]),
315 ("#Find" ,["antiDerivativeName F_"])
317 append_rls "e_rls" e_rls [(*for preds in where_*)],
318 SOME "Integrate (f_, v_)",
319 [["diff","integration","named"]]));
324 (prep_met (theory "Integrate") "met_diffint" [] e_metID
325 (["diff","integration"],
326 [("#Given" ,["functionTerm f_", "integrateBy v_"]),
327 ("#Find" ,["antiDerivative F_"])
329 {rew_ord'="tless_true", rls'=Atools_erls, calc = [],
332 crls = Atools_erls, nrls = e_rls},
333 "Script IntegrationScript (f_::real) (v_::real) = " ^
334 " (let t_ = Take (Integral f_ D v_) " ^
335 " in (Rewrite_Set_Inst [(bdv,v_)] integration False) (t_::real))"
339 (prep_met (theory "Integrate") "met_diffint_named" [] e_metID
340 (["diff","integration","named"],
341 [("#Given" ,["functionTerm f_", "integrateBy v_"]),
342 ("#Find" ,["antiDerivativeName F_"])
344 {rew_ord'="tless_true", rls'=Atools_erls, calc = [],
347 crls = Atools_erls, nrls = e_rls},
348 "Script NamedIntegrationScript (f_::real) (v_::real) (F_::real=>real) = " ^
349 " (let t_ = Take (F_ v_ = Integral f_ D v_) " ^
350 " in ((Try (Rewrite_Set_Inst [(bdv,v_)] simplify_Integral False)) @@ " ^
351 " (Rewrite_Set_Inst [(bdv,v_)] integration False)) t_) "