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" and
35 integral_var: "Integral bdv D bdv = bdv ^^^ 2 / 2" and
37 integral_add: "Integral (u + v) D bdv =
38 (Integral u D bdv) + (Integral v D bdv)" and
39 integral_mult: "[| Not (bdv occurs_in u); bdv occurs_in v |] ==>
40 Integral (u * v) D bdv = u * (Integral v D bdv)" and
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 Rule.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 (Symbol.explode o id_of) var of
61 | "c"::"_"::is => (case (TermC.int_of_str_opt o implode) is of
65 fun get_coeff c = case (Symbol.explode o id_of) c of
66 "c"::"_"::is => (the o TermC.int_of_str_opt o implode) is
68 val cs = filter selc (TermC.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 ((Rule.term2str p) ^ " = " ^ Rule.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 ("HOL.eq", T) $ lh $ rh =>
93 Const ("HOL.eq", T) $ lh $ TermC.mk_add rh (new_c rh)
94 | p => TermC.mk_add p (new_c p)
95 in SOME ((Rule.term2str p) ^ " = " ^ Rule.term2str p',
96 HOLogic.Trueprop $ (TermC.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 ((Rule.term2str p) ^ " = True",
106 HOLogic.Trueprop $ (TermC.mk_equality (p, @{term True})))
107 else SOME ((Rule.term2str p) ^ " = False",
108 HOLogic.Trueprop $ (TermC.mk_equality (p, @{term False})))
109 | eval_is_f_x _ _ _ _ = NONE;
111 setup \<open>KEStore_Elems.add_calcs
112 [("add_new_c", ("Integrate.add'_new'_c", eval_add_new_c "add_new_c_")),
113 ("is_f_x", ("Integrate.is'_f'_x", eval_is_f_x "is_f_idextifier_"))]\<close>
117 (*.rulesets for integration.*)
118 val integration_rules =
119 Rule.Rls {id="integration_rules", preconds = [],
120 rew_ord = ("termlessI",termlessI),
121 erls = Rule.Rls {id="conditions_in_integration_rules",
123 rew_ord = ("termlessI",termlessI),
125 srls = Rule.Erls, calc = [], errpatts = [],
126 rules = [(*for rewriting conditions in Thm's*)
127 Rule.Calc ("Atools.occurs'_in",
128 eval_occurs_in "#occurs_in_"),
129 Rule.Thm ("not_true", TermC.num_str @{thm not_true}),
130 Rule.Thm ("not_false",@{thm not_false})
132 scr = Rule.EmptyScr},
133 srls = Rule.Erls, calc = [], errpatts = [],
135 Rule.Thm ("integral_const", TermC.num_str @{thm integral_const}),
136 Rule.Thm ("integral_var", TermC.num_str @{thm integral_var}),
137 Rule.Thm ("integral_add", TermC.num_str @{thm integral_add}),
138 Rule.Thm ("integral_mult", TermC.num_str @{thm integral_mult}),
139 Rule.Thm ("integral_pow", TermC.num_str @{thm integral_pow}),
140 Rule.Calc ("Groups.plus_class.plus", eval_binop "#add_")(*for n+1*)
142 scr = Rule.EmptyScr};
146 Rule.Seq {id="add_new_c", preconds = [],
147 rew_ord = ("termlessI",termlessI),
148 erls = Rule.Rls {id="conditions_in_add_new_c",
150 rew_ord = ("termlessI",termlessI),
152 srls = Rule.Erls, calc = [], errpatts = [],
153 rules = [Rule.Calc ("Tools.matches", Tools.eval_matches""),
154 Rule.Calc ("Integrate.is'_f'_x",
155 eval_is_f_x "is_f_x_"),
156 Rule.Thm ("not_true", TermC.num_str @{thm not_true}),
157 Rule.Thm ("not_false", TermC.num_str @{thm not_false})
159 scr = Rule.EmptyScr},
160 srls = Rule.Erls, calc = [], errpatts = [],
161 rules = [ (*Rule.Thm ("call_for_new_c", TermC.num_str @{thm call_for_new_c}),*)
162 Rule.Cal1 ("Integrate.add'_new'_c", eval_add_new_c "new_c_")
164 scr = Rule.EmptyScr};
168 (*.rulesets for simplifying Integrals.*)
170 (*.for simplify_Integral adapted from 'norm_Rational_rls'.*)
171 val norm_Rational_rls_noadd_fractions =
172 Rule.Rls {id = "norm_Rational_rls_noadd_fractions", preconds = [],
173 rew_ord = ("dummy_ord",Rule.dummy_ord),
174 erls = norm_rat_erls, srls = Rule.Erls, calc = [], errpatts = [],
175 rules = [(*Rule.Rls_ add_fractions_p_rls,!!!*)
176 Rule.Rls_ (*rat_mult_div_pow original corrected WN051028*)
177 (Rule.Rls {id = "rat_mult_div_pow", preconds = [],
178 rew_ord = ("dummy_ord",Rule.dummy_ord),
179 erls = (*FIXME.WN051028 Rule.e_rls,*)
180 Rule.append_rls "Rule.e_rls-is_polyexp" Rule.e_rls
181 [Rule.Calc ("Poly.is'_polyexp",
182 eval_is_polyexp "")],
183 srls = Rule.Erls, calc = [], errpatts = [],
184 rules = [Rule.Thm ("rat_mult", TermC.num_str @{thm rat_mult}),
185 (*"?a / ?b * (?c / ?d) = ?a * ?c / (?b * ?d)"*)
186 Rule.Thm ("rat_mult_poly_l", TermC.num_str @{thm rat_mult_poly_l}),
187 (*"?c is_polyexp ==> ?c * (?a / ?b) = ?c * ?a / ?b"*)
188 Rule.Thm ("rat_mult_poly_r", TermC.num_str @{thm rat_mult_poly_r}),
189 (*"?c is_polyexp ==> ?a / ?b * ?c = ?a * ?c / ?b"*)
191 Rule.Thm ("real_divide_divide1_mg",
192 TermC.num_str @{thm real_divide_divide1_mg}),
193 (*"y ~= 0 ==> (u / v) / (y / z) = (u * z) / (y * v)"*)
194 Rule.Thm ("divide_divide_eq_right",
195 TermC.num_str @{thm divide_divide_eq_right}),
196 (*"?x / (?y / ?z) = ?x * ?z / ?y"*)
197 Rule.Thm ("divide_divide_eq_left",
198 TermC.num_str @{thm divide_divide_eq_left}),
199 (*"?x / ?y / ?z = ?x / (?y * ?z)"*)
200 Rule.Calc ("Rings.divide_class.divide" ,eval_cancel "#divide_e"),
202 Rule.Thm ("rat_power", TermC.num_str @{thm rat_power})
203 (*"(?a / ?b) ^^^ ?n = ?a ^^^ ?n / ?b ^^^ ?n"*)
205 scr = Rule.Prog ((Thm.term_of o the o (TermC.parse thy)) "empty_script")
207 Rule.Rls_ make_rat_poly_with_parentheses,
208 Rule.Rls_ cancel_p_rls,(*FIXME:cancel_p does NOT order sometimes*)
209 Rule.Rls_ rat_reduce_1
211 scr = Rule.Prog ((Thm.term_of o the o (TermC.parse thy)) "empty_script")
214 (*.for simplify_Integral adapted from 'norm_Rational'.*)
215 val norm_Rational_noadd_fractions =
216 Rule.Seq {id = "norm_Rational_noadd_fractions", preconds = [],
217 rew_ord = ("dummy_ord",Rule.dummy_ord),
218 erls = norm_rat_erls, srls = Rule.Erls, calc = [], errpatts = [],
219 rules = [Rule.Rls_ discard_minus,
220 Rule.Rls_ rat_mult_poly,(* removes double fractions like a/b/c *)
221 Rule.Rls_ make_rat_poly_with_parentheses, (*WN0510 also in(#)below*)
222 Rule.Rls_ cancel_p_rls, (*FIXME.MG:cancel_p does NOT order sometim*)
223 Rule.Rls_ norm_Rational_rls_noadd_fractions,(* the main rls (#) *)
224 Rule.Rls_ discard_parentheses1 (* mult only *)
226 scr = Rule.Prog ((Thm.term_of o the o (TermC.parse thy)) "empty_script")
229 (*.simplify terms before and after Integration such that
230 ..a.x^2/2 + b.x^3/3.. is made to ..a/2.x^2 + b/3.x^3.. (and NO
231 common denominator as done by norm_Rational or make_ratpoly_in.
232 This is a copy from 'make_ratpoly_in' with respective reduction of rules and
233 *1* expand the term, ie. distribute * and / over +
236 Rule.append_rls "separate_bdv2"
238 [Rule.Thm ("separate_bdv", TermC.num_str @{thm separate_bdv}),
239 (*"?a * ?bdv / ?b = ?a / ?b * ?bdv"*)
240 Rule.Thm ("separate_bdv_n", TermC.num_str @{thm separate_bdv_n}),
241 Rule.Thm ("separate_1_bdv", TermC.num_str @{thm separate_1_bdv}),
242 (*"?bdv / ?b = (1 / ?b) * ?bdv"*)
243 Rule.Thm ("separate_1_bdv_n", TermC.num_str @{thm separate_1_bdv_n})(*,
244 (*"?bdv ^^^ ?n / ?b = 1 / ?b * ?bdv ^^^ ?n"*)
245 *****Rule.Thm ("add_divide_distrib",
246 ***** TermC.num_str @{thm add_divide_distrib})
247 (*"(?x + ?y) / ?z = ?x / ?z + ?y / ?z"*)----------*)
249 val simplify_Integral =
250 Rule.Seq {id = "simplify_Integral", preconds = []:term list,
251 rew_ord = ("dummy_ord", Rule.dummy_ord),
252 erls = Atools_erls, srls = Rule.Erls,
253 calc = [], errpatts = [],
254 rules = [Rule.Thm ("distrib_right", TermC.num_str @{thm distrib_right}),
255 (*"(?z1.0 + ?z2.0) * ?w = ?z1.0 * ?w + ?z2.0 * ?w"*)
256 Rule.Thm ("add_divide_distrib", TermC.num_str @{thm add_divide_distrib}),
257 (*"(?x + ?y) / ?z = ?x / ?z + ?y / ?z"*)
258 (*^^^^^ *1* ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^*)
259 Rule.Rls_ norm_Rational_noadd_fractions,
260 Rule.Rls_ order_add_mult_in,
261 Rule.Rls_ discard_parentheses,
262 (*Rule.Rls_ collect_bdv, from make_polynomial_in*)
263 Rule.Rls_ separate_bdv2,
264 Rule.Calc ("Rings.divide_class.divide" ,eval_cancel "#divide_e")
266 scr = Rule.EmptyScr};
269 (*simplify terms before and after Integration such that
270 ..a.x^2/2 + b.x^3/3.. is made to ..a/2.x^2 + b/3.x^3.. (and NO
271 common denominator as done by norm_Rational or make_ratpoly_in.
272 This is a copy from 'make_polynomial_in' with insertions from
274 THIS IS KEPT FOR COMPARISON ............................................
275 * val simplify_Integral = prep_rls'(
276 * Rule.Seq {id = "", preconds = []:term list,
277 * rew_ord = ("dummy_ord", Rule.dummy_ord),
278 * erls = Atools_erls, srls = Rule.Erls,
279 * calc = [], (*asm_thm = [],*)
280 * rules = [Rule.Rls_ expand_poly,
281 * Rule.Rls_ order_add_mult_in,
282 * Rule.Rls_ simplify_power,
283 * Rule.Rls_ collect_numerals,
284 * Rule.Rls_ reduce_012,
285 * Rule.Thm ("realpow_oneI", TermC.num_str @{thm realpow_oneI}),
286 * Rule.Rls_ discard_parentheses,
287 * Rule.Rls_ collect_bdv,
288 * (*below inserted from 'make_ratpoly_in'*)
289 * Rule.Rls_ (Rule.append_rls "separate_bdv"
291 * [Rule.Thm ("separate_bdv", TermC.num_str @{thm separate_bdv}),
292 * (*"?a * ?bdv / ?b = ?a / ?b * ?bdv"*)
293 * Rule.Thm ("separate_bdv_n", TermC.num_str @{thm separate_bdv_n}),
294 * Rule.Thm ("separate_1_bdv", TermC.num_str @{thm separate_1_bdv}),
295 * (*"?bdv / ?b = (1 / ?b) * ?bdv"*)
296 * Rule.Thm ("separate_1_bdv_n", TermC.num_str @{thm separate_1_bdv_n})(*,
297 * (*"?bdv ^^^ ?n / ?b = 1 / ?b * ?bdv ^^^ ?n"*)
298 * Rule.Thm ("add_divide_distrib",
299 * TermC.num_str @{thm add_divide_distrib})
300 * (*"(?x + ?y) / ?z = ?x / ?z + ?y / ?z"*)*)
302 * Rule.Calc ("Rings.divide_class.divide" ,eval_cancel "#divide_e")
304 * scr = Rule.EmptyScr
306 .......................................................................*)
309 Rule.Seq {id="integration", preconds = [],
310 rew_ord = ("termlessI",termlessI),
311 erls = Rule.Rls {id="conditions_in_integration",
313 rew_ord = ("termlessI",termlessI),
315 srls = Rule.Erls, calc = [], errpatts = [],
317 scr = Rule.EmptyScr},
318 srls = Rule.Erls, calc = [], errpatts = [],
319 rules = [ Rule.Rls_ integration_rules,
321 Rule.Rls_ simplify_Integral
323 scr = Rule.EmptyScr};
325 val prep_rls' = LTool.prep_rls @{theory};
327 setup \<open>KEStore_Elems.add_rlss
328 [("integration_rules", (Context.theory_name @{theory}, prep_rls' integration_rules)),
329 ("add_new_c", (Context.theory_name @{theory}, prep_rls' add_new_c)),
330 ("simplify_Integral", (Context.theory_name @{theory}, prep_rls' simplify_Integral)),
331 ("integration", (Context.theory_name @{theory}, prep_rls' integration)),
332 ("separate_bdv2", (Context.theory_name @{theory}, prep_rls' separate_bdv2)),
334 ("norm_Rational_noadd_fractions", (Context.theory_name @{theory},
335 prep_rls' norm_Rational_noadd_fractions)),
336 ("norm_Rational_rls_noadd_fractions", (Context.theory_name @{theory},
337 prep_rls' norm_Rational_rls_noadd_fractions))]\<close>
340 setup \<open>KEStore_Elems.add_pbts
341 [(Specify.prep_pbt thy "pbl_fun_integ" [] Celem.e_pblID
342 (["integrate","function"],
343 [("#Given" ,["functionTerm f_f", "integrateBy v_v"]),
344 ("#Find" ,["antiDerivative F_F"])],
345 Rule.append_rls "e_rls" Rule.e_rls [(*for preds in where_*)],
346 SOME "Integrate (f_f, v_v)",
347 [["diff","integration"]])),
348 (*here "named" is used differently from Differentiation"*)
349 (Specify.prep_pbt thy "pbl_fun_integ_nam" [] Celem.e_pblID
350 (["named","integrate","function"],
351 [("#Given" ,["functionTerm f_f", "integrateBy v_v"]),
352 ("#Find" ,["antiDerivativeName F_F"])],
353 Rule.append_rls "e_rls" Rule.e_rls [(*for preds in where_*)],
354 SOME "Integrate (f_f, v_v)",
355 [["diff","integration","named"]]))]\<close>
359 partial_function (tailrec) integrate :: "real \<Rightarrow> real \<Rightarrow> real"
362 (let t_t = Take (Integral f_f D v_v)
363 in (Rewrite_Set_Inst [(''bdv'', v_v)] ''integration'' False) t_t)"
364 setup \<open>KEStore_Elems.add_mets
365 [Specify.prep_met thy "met_diffint" [] Celem.e_metID
366 (["diff","integration"],
367 [("#Given" ,["functionTerm f_f", "integrateBy v_v"]), ("#Find" ,["antiDerivative F_F"])],
368 {rew_ord'="tless_true", rls'=Atools_erls, calc = [], srls = Rule.e_rls, prls=Rule.e_rls,
369 crls = Atools_erls, errpats = [], nrls = Rule.e_rls},
370 @{thm integrate.simps}
371 (*"Script IntegrationScript (f_f::real) (v_v::real) = " ^
372 " (let t_t = Take (Integral f_f D v_v) " ^
373 " in (Rewrite_Set_Inst [(''bdv'',v_v)] ''integration'' False) (t_t::real))"*))]
376 partial_function (tailrec) intergrate_named :: "real \<Rightarrow> real \<Rightarrow> (real \<Rightarrow> real) \<Rightarrow> bool"
377 where "intergrate_named f_f v_v F_F =
378 (let t_t = Take (F_F v_v = Integral f_f D v_v)
379 in ((Try (Rewrite_Set_Inst [(''bdv'', v_v)] ''simplify_Integral'' False)) @@
380 (Rewrite_Set_Inst [(''bdv'', v_v)] ''integration'' False)) t_t)"
381 setup \<open>KEStore_Elems.add_mets
382 [Specify.prep_met thy "met_diffint_named" [] Celem.e_metID
383 (["diff","integration","named"],
384 [("#Given" ,["functionTerm f_f", "integrateBy v_v"]),
385 ("#Find" ,["antiDerivativeName F_F"])],
386 {rew_ord'="tless_true", rls'=Atools_erls, calc = [], srls = Rule.e_rls, prls=Rule.e_rls,
387 crls = Atools_erls, errpats = [], nrls = Rule.e_rls},
388 @{thm intergrate_named.simps}
389 (*"Script NamedIntegrationScript (f_f::real) (v_v::real) (F_F::real=>real) = " ^
390 " (let t_t = Take (F_F v_v = Integral f_f D v_v) " ^
391 " in ((Try (Rewrite_Set_Inst [(''bdv'',v_v)] ''simplify_Integral'' False)) @@ " ^
392 " (Rewrite_Set_Inst [(''bdv'',v_v)] ''integration'' False)) t_t) "*))]