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)"
50 (** eval functions **)
52 val c = Free ("c", HOLogic.realT);
53 (*.create a new unique variable 'c..' in a term; for use by Calc in a rls;
54 an alternative to do this would be '(Try (Calculate new_c_) (new_c es__))'
55 in the script; this will be possible if currying doesnt take the value
56 from a variable, but the value '(new_c es__)' itself.*)
59 case (explode o id_of) var of
61 | "c"::"_"::is => (case (int_of_str o implode) is of
65 fun get_coeff c = case (explode o id_of) c of
66 "c"::"_"::is => (the o int_of_str o implode) is
68 val cs = filter selc (vars term);
72 | [c] => Free ("c_2", HOLogic.realT)
74 let val max_coeff = maxl (map get_coeff cs)
75 in Free ("c_"^string_of_int (max_coeff + 1), HOLogic.realT) end
79 (*("new_c", ("Integrate.new'_c", eval_new_c "#new_c_"))*)
80 fun eval_new_c _ _ (p as (Const ("Integrate.new'_c",_) $ t)) _ =
81 SOME ((term2str p) ^ " = " ^ term2str (new_c p),
82 Trueprop $ (mk_equality (p, new_c p)))
83 | eval_new_c _ _ _ _ = NONE;
87 (*("add_new_c", ("Integrate.add'_new'_c", eval_add_new_c "#add_new_c_"))
88 add a new c to a term or a fun-equation;
89 this is _not in_ the term, because only applied to _whole_ term*)
90 fun eval_add_new_c (_:string) "Integrate.add'_new'_c" p (_:theory) =
91 let val p' = case p of
92 Const ("op =", T) $ lh $ rh =>
93 Const ("op =", T) $ lh $ mk_add rh (new_c rh)
94 | p => mk_add p (new_c p)
95 in SOME ((term2str p) ^ " = " ^ term2str p',
96 Trueprop $ (mk_equality (p, p')))
98 | eval_add_new_c _ _ _ _ = NONE;
101 (*("is_f_x", ("Integrate.is'_f'_x", eval_is_f_x "is_f_x_"))*)
102 fun eval_is_f_x _ _(p as (Const ("Integrate.is'_f'_x", _)
105 then SOME ((term2str p) ^ " = True",
106 Trueprop $ (mk_equality (p, HOLogic.true_const)))
107 else SOME ((term2str p) ^ " = False",
108 Trueprop $ (mk_equality (p, HOLogic.false_const)))
109 | eval_is_f_x _ _ _ _ = NONE;
111 calclist':= overwritel (!calclist',
112 [(*("new_c", ("Integrate.new'_c", eval_new_c "new_c_")),*)
113 ("add_new_c", ("Integrate.add'_new'_c", eval_add_new_c "add_new_c_")),
114 ("is_f_x", ("Integrate.is'_f'_x", eval_is_f_x "is_f_idextifier_"))
120 (*.rulesets for integration.*)
121 val integration_rules =
122 Rls {id="integration_rules", preconds = [],
123 rew_ord = ("termlessI",termlessI),
124 erls = Rls {id="conditions_in_integration_rules",
126 rew_ord = ("termlessI",termlessI),
128 srls = Erls, calc = [],
129 rules = [(*for rewriting conditions in Thm's*)
130 Calc ("Atools.occurs'_in",
131 eval_occurs_in "#occurs_in_"),
132 Thm ("not_true",num_str @{thm not_true}),
133 Thm ("not_false",@{thm not_false})
136 srls = Erls, calc = [],
138 Thm ("integral_const",num_str @{thm integral_const}),
139 Thm ("integral_var",num_str @{thm integral_var}),
140 Thm ("integral_add",num_str @{thm integral_add}),
141 Thm ("integral_mult",num_str @{thm integral_mult}),
142 Thm ("integral_pow",num_str @{thm integral_pow}),
143 Calc ("op +", eval_binop "#add_")(*for n+1*)
147 Seq {id="add_new_c", preconds = [],
148 rew_ord = ("termlessI",termlessI),
149 erls = Rls {id="conditions_in_add_new_c",
151 rew_ord = ("termlessI",termlessI),
153 srls = Erls, calc = [],
154 rules = [Calc ("Tools.matches", eval_matches""),
155 Calc ("Integrate.is'_f'_x",
156 eval_is_f_x "is_f_x_"),
157 Thm ("not_true",num_str @{thm not_true}),
158 Thm ("not_false",num_str @{thm not_false)
161 srls = Erls, calc = [],
162 rules = [ (*Thm ("call_for_new_c", num_str @{thm call_for_new_c}),*)
163 Cal1 ("Integrate.add'_new'_c", eval_add_new_c "new_c_")
167 (*.rulesets for simplifying Integrals.*)
169 (*.for simplify_Integral adapted from 'norm_Rational_rls'.*)
170 val norm_Rational_rls_noadd_fractions =
171 Rls {id = "norm_Rational_rls_noadd_fractions", preconds = [],
172 rew_ord = ("dummy_ord",dummy_ord),
173 erls = norm_rat_erls, srls = Erls, calc = [],
174 rules = [(*Rls_ common_nominator_p_rls,!!!*)
175 Rls_ (*rat_mult_div_pow original corrected WN051028*)
176 (Rls {id = "rat_mult_div_pow", preconds = [],
177 rew_ord = ("dummy_ord",dummy_ord),
178 erls = (*FIXME.WN051028 e_rls,*)
179 append_rls "e_rls-is_polyexp" e_rls
180 [Calc ("Poly.is'_polyexp",
181 eval_is_polyexp "")],
182 srls = Erls, calc = [],
183 rules = [Thm ("rat_mult",num_str @{thm rat_mult}),
184 (*"?a / ?b * (?c / ?d) = ?a * ?c / (?b * ?d)"*)
185 Thm ("rat_mult_poly_l",num_str @{thm rat_mult_poly_l}),
186 (*"?c is_polyexp ==> ?c * (?a / ?b) = ?c * ?a / ?b"*)
187 Thm ("rat_mult_poly_r",num_str @{thm rat_mult_poly_r}),
188 (*"?c is_polyexp ==> ?a / ?b * ?c = ?a * ?c / ?b"*)
190 Thm ("real_divide_divide1_mg",
191 num_str @{thm real_divide_divide1_mg}),
192 (*"y ~= 0 ==> (u / v) / (y / z) = (u * z) / (y * v)"*)
193 Thm ("divide_divide_eq_right",
194 num_str @{thm divide_divide_eq_right}),
195 (*"?x / (?y / ?z) = ?x * ?z / ?y"*)
196 Thm ("divide_divide_eq_left",
197 num_str @{thm divide_divide_eq_left}),
198 (*"?x / ?y / ?z = ?x / (?y * ?z)"*)
199 Calc ("HOL.divide" ,eval_cancel "#divide_"),
201 Thm ("rat_power", num_str @{thm rat_power})
202 (*"(?a / ?b) ^^^ ?n = ?a ^^^ ?n / ?b ^^^ ?n"*)
204 scr = Script ((term_of o the o (parse thy)) "empty_script")
206 Rls_ make_rat_poly_with_parentheses,
207 Rls_ cancel_p_rls,(*FIXME:cancel_p does NOT order sometimes*)
210 scr = Script ((term_of o the o (parse thy)) "empty_script")
213 (*.for simplify_Integral adapted from 'norm_Rational'.*)
214 val norm_Rational_noadd_fractions =
215 Seq {id = "norm_Rational_noadd_fractions", preconds = [],
216 rew_ord = ("dummy_ord",dummy_ord),
217 erls = norm_rat_erls, srls = Erls, calc = [],
218 rules = [Rls_ discard_minus1,
219 Rls_ rat_mult_poly,(* removes double fractions like a/b/c *)
220 Rls_ make_rat_poly_with_parentheses, (*WN0510 also in(#)below*)
221 Rls_ cancel_p_rls, (*FIXME.MG:cancel_p does NOT order sometim*)
222 Rls_ norm_Rational_rls_noadd_fractions,(* the main rls (#) *)
223 Rls_ discard_parentheses1 (* mult only *)
225 scr = Script ((term_of o the o (parse thy)) "empty_script")
228 (*.simplify terms before and after Integration such that
229 ..a.x^2/2 + b.x^3/3.. is made to ..a/2.x^2 + b/3.x^3.. (and NO
230 common denominator as done by norm_Rational or make_ratpoly_in.
231 This is a copy from 'make_ratpoly_in' with respective reduction of rules and
232 *1* expand the term, ie. distribute * and / over +
235 append_rls "separate_bdv2"
237 [Thm ("separate_bdv", num_str @{thm separate_bdv}),
238 (*"?a * ?bdv / ?b = ?a / ?b * ?bdv"*)
239 Thm ("separate_bdv_n", num_str @{thm separate_bdv_n}),
240 Thm ("separate_1_bdv", num_str @{thm separate_1_bdv}),
241 (*"?bdv / ?b = (1 / ?b) * ?bdv"*)
242 Thm ("separate_1_bdv_n", num_str @{thm separate_1_bdv_n})(*,
243 (*"?bdv ^^^ ?n / ?b = 1 / ?b * ?bdv ^^^ ?n"*)
244 *****Thm ("nadd_divide_distrib",
245 *****num_str @{thm nadd_divide_distrib})
246 (*"(?x + ?y) / ?z = ?x / ?z + ?y / ?z"*)----------*)
248 val simplify_Integral =
249 Seq {id = "simplify_Integral", preconds = []:term list,
250 rew_ord = ("dummy_ord", dummy_ord),
251 erls = Atools_erls, srls = Erls,
252 calc = [], (*asm_thm = [],*)
253 rules = [Thm ("left_distrib",num_str @{thm left_distrib}),
254 (*"(?z1.0 + ?z2.0) * ?w = ?z1.0 * ?w + ?z2.0 * ?w"*)
255 Thm ("nadd_divide_distrib",num_str @{thm nadd_divide_distrib}),
256 (*"(?x + ?y) / ?z = ?x / ?z + ?y / ?z"*)
257 (*^^^^^ *1* ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^*)
258 Rls_ norm_Rational_noadd_fractions,
259 Rls_ order_add_mult_in,
260 Rls_ discard_parentheses,
261 (*Rls_ collect_bdv, from make_polynomial_in*)
263 Calc ("HOL.divide" ,eval_cancel "#divide_")
268 (*simplify terms before and after Integration such that
269 ..a.x^2/2 + b.x^3/3.. is made to ..a/2.x^2 + b/3.x^3.. (and NO
270 common denominator as done by norm_Rational or make_ratpoly_in.
271 This is a copy from 'make_polynomial_in' with insertions from
273 THIS IS KEPT FOR COMPARISON ............................................
274 * val simplify_Integral = prep_rls(
275 * Seq {id = "", preconds = []:term list,
276 * rew_ord = ("dummy_ord", dummy_ord),
277 * erls = Atools_erls, srls = Erls,
278 * calc = [], (*asm_thm = [],*)
279 * rules = [Rls_ expand_poly,
280 * Rls_ order_add_mult_in,
281 * Rls_ simplify_power,
282 * Rls_ collect_numerals,
284 * Thm ("realpow_oneI",num_str @{thm realpow_oneI}),
285 * Rls_ discard_parentheses,
287 * (*below inserted from 'make_ratpoly_in'*)
288 * Rls_ (append_rls "separate_bdv"
290 * [Thm ("separate_bdv", num_str @{thm separate_bdv}),
291 * (*"?a * ?bdv / ?b = ?a / ?b * ?bdv"*)
292 * Thm ("separate_bdv_n", num_str @{thm separate_bdv_n}),
293 * Thm ("separate_1_bdv", num_str @{thm separate_1_bdv}),
294 * (*"?bdv / ?b = (1 / ?b) * ?bdv"*)
295 * Thm ("separate_1_bdv_n", num_str @{thm separate_1_bdv_n})(*,
296 * (*"?bdv ^^^ ?n / ?b = 1 / ?b * ?bdv ^^^ ?n"*)
297 * Thm ("nadd_divide_distrib",
298 * num_str @{thm nadd_divide_distrib})
299 * (*"(?x + ?y) / ?z = ?x / ?z + ?y / ?z"*)*)
301 * Calc ("HOL.divide" ,eval_cancel "#divide_")
305 .......................................................................*)
308 Seq {id="integration", preconds = [],
309 rew_ord = ("termlessI",termlessI),
310 erls = Rls {id="conditions_in_integration",
312 rew_ord = ("termlessI",termlessI),
314 srls = Erls, calc = [],
317 srls = Erls, calc = [],
318 rules = [ Rls_ integration_rules,
320 Rls_ simplify_Integral
324 overwritelthy @{theory} (!ruleset',
325 [("integration_rules", prep_rls integration_rules),
326 ("add_new_c", prep_rls add_new_c),
327 ("simplify_Integral", prep_rls simplify_Integral),
328 ("integration", prep_rls integration),
329 ("separate_bdv2", separate_bdv2),
330 ("norm_Rational_noadd_fractions", norm_Rational_noadd_fractions),
331 ("norm_Rational_rls_noadd_fractions",
332 norm_Rational_rls_noadd_fractions)
338 (prep_pbt thy "pbl_fun_integ" [] e_pblID
339 (["integrate","function"],
340 [("#Given" ,["functionTerm f_", "integrateBy v_"]),
341 ("#Find" ,["antiDerivative F_"])
343 append_rls "e_rls" e_rls [(*for preds in where_*)],
344 SOME "Integrate (f_, v_)",
345 [["diff","integration"]]));
347 (*here "named" is used differently from Differentiation"*)
349 (prep_pbt thy "pbl_fun_integ_nam" [] e_pblID
350 (["named","integrate","function"],
351 [("#Given" ,["functionTerm f_", "integrateBy v_"]),
352 ("#Find" ,["antiDerivativeName F_"])
354 append_rls "e_rls" e_rls [(*for preds in where_*)],
355 SOME "Integrate (f_, v_)",
356 [["diff","integration","named"]]));
361 (prep_met thy "met_diffint" [] e_metID
362 (["diff","integration"],
363 [("#Given" ,["functionTerm f_", "integrateBy v_"]),
364 ("#Find" ,["antiDerivative F_"])
366 {rew_ord'="tless_true", rls'=Atools_erls, calc = [],
369 crls = Atools_erls, nrls = e_rls},
370 "Script IntegrationScript (f_::real) (v_::real) = " ^
371 " (let t_ = Take (Integral f_ D v_) " ^
372 " in (Rewrite_Set_Inst [(bdv,v_)] integration False) (t_::real))"
376 (prep_met thy "met_diffint_named" [] e_metID
377 (["diff","integration","named"],
378 [("#Given" ,["functionTerm f_", "integrateBy v_"]),
379 ("#Find" ,["antiDerivativeName F_"])
381 {rew_ord'="tless_true", rls'=Atools_erls, calc = [],
384 crls = Atools_erls, nrls = e_rls},
385 "Script NamedIntegrationScript (f_::real) (v_::real) (F_::real=>real) = " ^
386 " (let t_ = Take (F_ v_ = Integral f_ D v_) " ^
387 " in ((Try (Rewrite_Set_Inst [(bdv,v_)] simplify_Integral False)) @@ " ^
388 " (Rewrite_Set_Inst [(bdv,v_)] integration False)) t_) "