1 (* integration over the reals
4 (c) due to copyright terms
7 theory Integrate imports Diff begin
11 Integral :: "[real, real]=> real" ("Integral _ D _" 91)
12 (*new'_c :: "real => real" ("new'_c _" 66)*)
13 is'_f'_x :: "real => bool" ("_ is'_f'_x" 10)
15 (*descriptions in the related problems*)
16 integrateBy :: real => una
17 antiDerivative :: real => una
18 antiDerivativeName :: (real => real) => una
20 (*the CAS-command, eg. "Integrate (2*x^^^3, x)"*)
21 Integrate :: "[real * real] => real"
24 IntegrationScript :: "[real,real, real] => real"
25 ("((Script IntegrationScript (_ _ =))// (_))" 9)
26 NamedIntegrationScript :: "[real,real, real=>real, bool] => bool"
27 ("((Script NamedIntegrationScript (_ _ _=))// (_))" 9)
30 (*stated as axioms, todo: prove as theorems
31 'bdv' is a constant handled on the meta-level
32 specifically as a 'bound variable' *)
34 integral_const "Not (bdv occurs_in u) ==> Integral u D bdv = u * bdv"
35 integral_var "Integral bdv D bdv = bdv ^^^ 2 / 2"
37 integral_add "Integral (u + v) D bdv =
38 (Integral u D bdv) + (Integral v D bdv)"
39 integral_mult "[| Not (bdv occurs_in u); bdv occurs_in v |] ==>
40 Integral (u * v) D bdv = u * (Integral v D bdv)"
41 (*WN080222: this goes into sub-terms, too ...
42 call_for_new_c "[| Not (matches (u + new_c v) a); Not (a is_f_x) |] ==>
45 integral_pow "Integral bdv ^^^ n D bdv = bdv ^^^ (n+1) / (n + 1)"
48 (** eval functions **)
50 val c = Free ("c", HOLogic.realT);
51 (*.create a new unique variable 'c..' in a term; for use by Calc in a rls;
52 an alternative to do this would be '(Try (Calculate new_c_) (new_c es__))'
53 in the script; this will be possible if currying doesnt take the value
54 from a variable, but the value '(new_c es__)' itself.*)
57 case (explode o id_of) var of
59 | "c"::"_"::is => (case (int_of_str o implode) is of
63 fun get_coeff c = case (explode o id_of) c of
64 "c"::"_"::is => (the o int_of_str o implode) is
66 val cs = filter selc (vars term);
70 | [c] => Free ("c_2", HOLogic.realT)
72 let val max_coeff = maxl (map get_coeff cs)
73 in Free ("c_"^string_of_int (max_coeff + 1), HOLogic.realT) end
77 (*("new_c", ("Integrate.new'_c", eval_new_c "#new_c_"))*)
78 fun eval_new_c _ _ (p as (Const ("Integrate.new'_c",_) $ t)) _ =
79 SOME ((term2str p) ^ " = " ^ term2str (new_c p),
80 Trueprop $ (mk_equality (p, new_c p)))
81 | eval_new_c _ _ _ _ = NONE;
85 (*("add_new_c", ("Integrate.add'_new'_c", eval_add_new_c "#add_new_c_"))
86 add a new c to a term or a fun-equation;
87 this is _not in_ the term, because only applied to _whole_ term*)
88 fun eval_add_new_c (_:string) "Integrate.add'_new'_c" p (_:theory) =
89 let val p' = case p of
90 Const ("op =", T) $ lh $ rh =>
91 Const ("op =", T) $ lh $ mk_add rh (new_c rh)
92 | p => mk_add p (new_c p)
93 in SOME ((term2str p) ^ " = " ^ term2str p',
94 Trueprop $ (mk_equality (p, p')))
96 | eval_add_new_c _ _ _ _ = NONE;
99 (*("is_f_x", ("Integrate.is'_f'_x", eval_is_f_x "is_f_x_"))*)
100 fun eval_is_f_x _ _(p as (Const ("Integrate.is'_f'_x", _)
103 then SOME ((term2str p) ^ " = True",
104 Trueprop $ (mk_equality (p, HOLogic.true_const)))
105 else SOME ((term2str p) ^ " = False",
106 Trueprop $ (mk_equality (p, HOLogic.false_const)))
107 | eval_is_f_x _ _ _ _ = NONE;
109 calclist':= overwritel (!calclist',
110 [(*("new_c", ("Integrate.new'_c", eval_new_c "new_c_")),*)
111 ("add_new_c", ("Integrate.add'_new'_c", eval_add_new_c "add_new_c_")),
112 ("is_f_x", ("Integrate.is'_f'_x", eval_is_f_x "is_f_idextifier_"))
118 (*.rulesets for integration.*)
119 val integration_rules =
120 Rls {id="integration_rules", preconds = [],
121 rew_ord = ("termlessI",termlessI),
122 erls = Rls {id="conditions_in_integration_rules",
124 rew_ord = ("termlessI",termlessI),
126 srls = Erls, calc = [],
127 rules = [(*for rewriting conditions in Thm's*)
128 Calc ("Atools.occurs'_in",
129 eval_occurs_in "#occurs_in_"),
130 Thm ("not_true",num_str not_true),
131 Thm ("not_false",not_false)
134 srls = Erls, calc = [],
136 Thm ("integral_const",num_str integral_const),
137 Thm ("integral_var",num_str integral_var),
138 Thm ("integral_add",num_str integral_add),
139 Thm ("integral_mult",num_str integral_mult),
140 Thm ("integral_pow",num_str integral_pow),
141 Calc ("op +", eval_binop "#add_")(*for n+1*)
145 Seq {id="add_new_c", preconds = [],
146 rew_ord = ("termlessI",termlessI),
147 erls = Rls {id="conditions_in_add_new_c",
149 rew_ord = ("termlessI",termlessI),
151 srls = Erls, calc = [],
152 rules = [Calc ("Tools.matches", eval_matches""),
153 Calc ("Integrate.is'_f'_x",
154 eval_is_f_x "is_f_x_"),
155 Thm ("not_true",num_str not_true),
156 Thm ("not_false",num_str not_false)
159 srls = Erls, calc = [],
160 rules = [ (*Thm ("call_for_new_c", num_str call_for_new_c),*)
161 Cal1 ("Integrate.add'_new'_c", eval_add_new_c "new_c_")
165 (*.rulesets for simplifying Integrals.*)
167 (*.for simplify_Integral adapted from 'norm_Rational_rls'.*)
168 val norm_Rational_rls_noadd_fractions =
169 Rls {id = "norm_Rational_rls_noadd_fractions", preconds = [],
170 rew_ord = ("dummy_ord",dummy_ord),
171 erls = norm_rat_erls, srls = Erls, calc = [],
172 rules = [(*Rls_ common_nominator_p_rls,!!!*)
173 Rls_ (*rat_mult_div_pow original corrected WN051028*)
174 (Rls {id = "rat_mult_div_pow", preconds = [],
175 rew_ord = ("dummy_ord",dummy_ord),
176 erls = (*FIXME.WN051028 e_rls,*)
177 append_rls "e_rls-is_polyexp" e_rls
178 [Calc ("Poly.is'_polyexp",
179 eval_is_polyexp "")],
180 srls = Erls, calc = [],
181 rules = [Thm ("rat_mult",num_str rat_mult),
182 (*"?a / ?b * (?c / ?d) = ?a * ?c / (?b * ?d)"*)
183 Thm ("rat_mult_poly_l",num_str rat_mult_poly_l),
184 (*"?c is_polyexp ==> ?c * (?a / ?b) = ?c * ?a / ?b"*)
185 Thm ("rat_mult_poly_r",num_str rat_mult_poly_r),
186 (*"?c is_polyexp ==> ?a / ?b * ?c = ?a * ?c / ?b"*)
188 Thm ("real_divide_divide1_mg", real_divide_divide1_mg),
189 (*"y ~= 0 ==> (u / v) / (y / z) = (u * z) / (y * v)"*)
190 Thm ("real_divide_divide1_eq", real_divide_divide1_eq),
191 (*"?x / (?y / ?z) = ?x * ?z / ?y"*)
192 Thm ("real_divide_divide2_eq", real_divide_divide2_eq),
193 (*"?x / ?y / ?z = ?x / (?y * ?z)"*)
194 Calc ("HOL.divide" ,eval_cancel "#divide_"),
196 Thm ("rat_power", num_str rat_power)
197 (*"(?a / ?b) ^^^ ?n = ?a ^^^ ?n / ?b ^^^ ?n"*)
199 scr = Script ((term_of o the o (parse thy)) "empty_script")
201 Rls_ make_rat_poly_with_parentheses,
202 Rls_ cancel_p_rls,(*FIXME:cancel_p does NOT order sometimes*)
205 scr = Script ((term_of o the o (parse thy)) "empty_script")
208 (*.for simplify_Integral adapted from 'norm_Rational'.*)
209 val norm_Rational_noadd_fractions =
210 Seq {id = "norm_Rational_noadd_fractions", preconds = [],
211 rew_ord = ("dummy_ord",dummy_ord),
212 erls = norm_rat_erls, srls = Erls, calc = [],
213 rules = [Rls_ discard_minus_,
214 Rls_ rat_mult_poly,(* removes double fractions like a/b/c *)
215 Rls_ make_rat_poly_with_parentheses, (*WN0510 also in(#)below*)
216 Rls_ cancel_p_rls, (*FIXME.MG:cancel_p does NOT order sometim*)
217 Rls_ norm_Rational_rls_noadd_fractions,(* the main rls (#) *)
218 Rls_ discard_parentheses_ (* mult only *)
220 scr = Script ((term_of o the o (parse thy)) "empty_script")
223 (*.simplify terms before and after Integration such that
224 ..a.x^2/2 + b.x^3/3.. is made to ..a/2.x^2 + b/3.x^3.. (and NO
225 common denominator as done by norm_Rational or make_ratpoly_in.
226 This is a copy from 'make_ratpoly_in' with respective reduction of rules and
227 *1* expand the term, ie. distribute * and / over +
230 append_rls "separate_bdv2"
232 [Thm ("separate_bdv", num_str separate_bdv),
233 (*"?a * ?bdv / ?b = ?a / ?b * ?bdv"*)
234 Thm ("separate_bdv_n", num_str separate_bdv_n),
235 Thm ("separate_1_bdv", num_str separate_1_bdv),
236 (*"?bdv / ?b = (1 / ?b) * ?bdv"*)
237 Thm ("separate_1_bdv_n", num_str separate_1_bdv_n)(*,
238 (*"?bdv ^^^ ?n / ?b = 1 / ?b * ?bdv ^^^ ?n"*)
239 *****Thm ("real_add_divide_distrib",
240 *****num_str real_add_divide_distrib)
241 (*"(?x + ?y) / ?z = ?x / ?z + ?y / ?z"*)----------*)
243 val simplify_Integral =
244 Seq {id = "simplify_Integral", preconds = []:term list,
245 rew_ord = ("dummy_ord", dummy_ord),
246 erls = Atools_erls, srls = Erls,
247 calc = [], (*asm_thm = [],*)
248 rules = [Thm ("real_add_mult_distrib",num_str real_add_mult_distrib),
249 (*"(?z1.0 + ?z2.0) * ?w = ?z1.0 * ?w + ?z2.0 * ?w"*)
250 Thm ("real_add_divide_distrib",num_str real_add_divide_distrib),
251 (*"(?x + ?y) / ?z = ?x / ?z + ?y / ?z"*)
252 (*^^^^^ *1* ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^*)
253 Rls_ norm_Rational_noadd_fractions,
254 Rls_ order_add_mult_in,
255 Rls_ discard_parentheses,
256 (*Rls_ collect_bdv, from make_polynomial_in*)
258 Calc ("HOL.divide" ,eval_cancel "#divide_")
263 (*simplify terms before and after Integration such that
264 ..a.x^2/2 + b.x^3/3.. is made to ..a/2.x^2 + b/3.x^3.. (and NO
265 common denominator as done by norm_Rational or make_ratpoly_in.
266 This is a copy from 'make_polynomial_in' with insertions from
268 THIS IS KEPT FOR COMPARISON ............................................
269 * val simplify_Integral = prep_rls(
270 * Seq {id = "", preconds = []:term list,
271 * rew_ord = ("dummy_ord", dummy_ord),
272 * erls = Atools_erls, srls = Erls,
273 * calc = [], (*asm_thm = [],*)
274 * rules = [Rls_ expand_poly,
275 * Rls_ order_add_mult_in,
276 * Rls_ simplify_power,
277 * Rls_ collect_numerals,
279 * Thm ("realpow_oneI",num_str realpow_oneI),
280 * Rls_ discard_parentheses,
282 * (*below inserted from 'make_ratpoly_in'*)
283 * Rls_ (append_rls "separate_bdv"
285 * [Thm ("separate_bdv", num_str separate_bdv),
286 * (*"?a * ?bdv / ?b = ?a / ?b * ?bdv"*)
287 * Thm ("separate_bdv_n", num_str separate_bdv_n),
288 * Thm ("separate_1_bdv", num_str separate_1_bdv),
289 * (*"?bdv / ?b = (1 / ?b) * ?bdv"*)
290 * Thm ("separate_1_bdv_n", num_str separate_1_bdv_n)(*,
291 * (*"?bdv ^^^ ?n / ?b = 1 / ?b * ?bdv ^^^ ?n"*)
292 * Thm ("real_add_divide_distrib",
293 * num_str real_add_divide_distrib)
294 * (*"(?x + ?y) / ?z = ?x / ?z + ?y / ?z"*)*)
296 * Calc ("HOL.divide" ,eval_cancel "#divide_")
300 .......................................................................*)
303 Seq {id="integration", preconds = [],
304 rew_ord = ("termlessI",termlessI),
305 erls = Rls {id="conditions_in_integration",
307 rew_ord = ("termlessI",termlessI),
309 srls = Erls, calc = [],
312 srls = Erls, calc = [],
313 rules = [ Rls_ integration_rules,
315 Rls_ simplify_Integral
319 overwritelthy thy (!ruleset',
320 [("integration_rules", prep_rls integration_rules),
321 ("add_new_c", prep_rls add_new_c),
322 ("simplify_Integral", prep_rls simplify_Integral),
323 ("integration", prep_rls integration),
324 ("separate_bdv2", separate_bdv2),
325 ("norm_Rational_noadd_fractions", norm_Rational_noadd_fractions),
326 ("norm_Rational_rls_noadd_fractions",
327 norm_Rational_rls_noadd_fractions)
333 (prep_pbt (theory "Integrate") "pbl_fun_integ" [] e_pblID
334 (["integrate","function"],
335 [("#Given" ,["functionTerm f_", "integrateBy v_"]),
336 ("#Find" ,["antiDerivative F_"])
338 append_rls "e_rls" e_rls [(*for preds in where_*)],
339 SOME "Integrate (f_, v_)",
340 [["diff","integration"]]));
342 (*here "named" is used differently from Differentiation"*)
344 (prep_pbt (theory "Integrate") "pbl_fun_integ_nam" [] e_pblID
345 (["named","integrate","function"],
346 [("#Given" ,["functionTerm f_", "integrateBy v_"]),
347 ("#Find" ,["antiDerivativeName F_"])
349 append_rls "e_rls" e_rls [(*for preds in where_*)],
350 SOME "Integrate (f_, v_)",
351 [["diff","integration","named"]]));
356 (prep_met (theory "Integrate") "met_diffint" [] e_metID
357 (["diff","integration"],
358 [("#Given" ,["functionTerm f_", "integrateBy v_"]),
359 ("#Find" ,["antiDerivative F_"])
361 {rew_ord'="tless_true", rls'=Atools_erls, calc = [],
364 crls = Atools_erls, nrls = e_rls},
365 "Script IntegrationScript (f_::real) (v_::real) = " ^
366 " (let t_ = Take (Integral f_ D v_) " ^
367 " in (Rewrite_Set_Inst [(bdv,v_)] integration False) (t_::real))"
371 (prep_met (theory "Integrate") "met_diffint_named" [] e_metID
372 (["diff","integration","named"],
373 [("#Given" ,["functionTerm f_", "integrateBy v_"]),
374 ("#Find" ,["antiDerivativeName F_"])
376 {rew_ord'="tless_true", rls'=Atools_erls, calc = [],
379 crls = Atools_erls, nrls = e_rls},
380 "Script NamedIntegrationScript (f_::real) (v_::real) (F_::real=>real) = " ^
381 " (let t_ = Take (F_ v_ = Integral f_ D v_) " ^
382 " in ((Try (Rewrite_Set_Inst [(bdv,v_)] simplify_Integral False)) @@ " ^
383 " (Rewrite_Set_Inst [(bdv,v_)] integration False)) t_) "