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 \<up> 3, x)"*)
21 Integrate :: "[real * real] => real"
24 (*stated as axioms, todo: prove as theorems
25 'bdv' is a constant handled on the meta-level
26 specifically as a 'bound variable' *)
28 (*Ambiguous input\<^here> produces 3 parse trees -----------------------------\\*)
29 integral_const: "Not (bdv occurs_in u) ==> Integral u D bdv = u * bdv" and
30 integral_var: "Integral bdv D bdv = bdv \<up> 2 / 2" and
32 integral_add: "Integral (u + v) D bdv =
33 (Integral u D bdv) + (Integral v D bdv)" and
34 integral_mult: "[| Not (bdv occurs_in u); bdv occurs_in v |] ==>
35 Integral (u * v) D bdv = u * (Integral v D bdv)" and
36 (*WN080222: this goes into sub-terms, too ...
37 call_for_new_c: "[| Not (matches (u + new_c v) a); Not (a is_f_x) |] ==>
40 integral_pow: "Integral bdv \<up> n D bdv = bdv \<up> (n+1) / (n + 1)"
41 (*Ambiguous input\<^here> produces 3 parse trees -----------------------------//*)
46 (** eval functions **)
48 val c = Free ("c", HOLogic.realT);
49 (*.create a new unique variable 'c..' in a term; for use by Rule.Eval in a rls;
50 an alternative to do this would be '(Try (Calculate new_c_) (new_c es__))'
51 in the script; this will be possible if currying doesnt take the value
52 from a variable, but the value '(new_c es__)' itself.*)
55 case (Symbol.explode o id_of) var of
57 | "c"::"_"::is => (case (TermC.int_opt_of_string o implode) is of
61 fun get_coeff c = case (Symbol.explode o id_of) c of
62 "c"::"_"::is => (the o TermC.int_opt_of_string o implode) is
64 val cs = filter selc (TermC.vars term);
68 | [_] => Free ("c_2", HOLogic.realT)
70 let val max_coeff = maxl (map get_coeff cs)
71 in Free ("c_"^string_of_int (max_coeff + 1), HOLogic.realT) end
75 (*("new_c", ("Integrate.new_c", eval_new_c "#new_c_"))*)
76 fun eval_new_c _ _ (p as (Const ("Integrate.new_c",_) $ t)) _ =
77 SOME ((UnparseC.term p) ^ " = " ^ UnparseC.term (new_c p),
78 Trueprop $ (mk_equality (p, new_c p)))
79 | eval_new_c _ _ _ _ = NONE;
83 (*("add_new_c", ("Integrate.add_new_c", eval_add_new_c "#add_new_c_"))
84 add a new c to a term or a fun-equation;
85 this is _not in_ the term, because only applied to _whole_ term*)
86 fun eval_add_new_c (_:string) "Integrate.add_new_c" p (_:theory) =
87 let val p' = case p of
88 Const ("HOL.eq", T) $ lh $ rh =>
89 Const ("HOL.eq", T) $ lh $ TermC.mk_add rh (new_c rh)
90 | p => TermC.mk_add p (new_c p)
91 in SOME ((UnparseC.term p) ^ " = " ^ UnparseC.term p',
92 HOLogic.Trueprop $ (TermC.mk_equality (p, p')))
94 | eval_add_new_c _ _ _ _ = NONE;
97 (*("is_f_x", ("Integrate.is_f_x", eval_is_f_x "is_f_x_"))*)
98 fun eval_is_f_x _ _(p as (Const ("Integrate.is_f_x", _)
101 then SOME ((UnparseC.term p) ^ " = True",
102 HOLogic.Trueprop $ (TermC.mk_equality (p, @{term True})))
103 else SOME ((UnparseC.term p) ^ " = False",
104 HOLogic.Trueprop $ (TermC.mk_equality (p, @{term False})))
105 | eval_is_f_x _ _ _ _ = NONE;
107 setup \<open>KEStore_Elems.add_calcs
108 [("add_new_c", ("Integrate.add_new_c", eval_add_new_c "add_new_c_")),
109 ("is_f_x", ("Integrate.is_f_x", eval_is_f_x "is_f_idextifier_"))]\<close>
113 (*.rulesets for integration.*)
114 val integration_rules =
115 Rule_Def.Repeat {id="integration_rules", preconds = [],
116 rew_ord = ("termlessI",termlessI),
117 erls = Rule_Def.Repeat {id="conditions_in_integration_rules",
119 rew_ord = ("termlessI",termlessI),
120 erls = Rule_Set.Empty,
121 srls = Rule_Set.Empty, calc = [], errpatts = [],
122 rules = [(*for rewriting conditions in Thm's*)
123 Rule.Eval ("Prog_Expr.occurs_in", Prog_Expr.eval_occurs_in "#occurs_in_"),
124 Rule.Thm ("not_true", ThmC.numerals_to_Free @{thm not_true}),
125 Rule.Thm ("not_false",@{thm not_false})
127 scr = Rule.Empty_Prog},
128 srls = Rule_Set.Empty, calc = [], errpatts = [],
130 Rule.Thm ("integral_const", ThmC.numerals_to_Free @{thm integral_const}),
131 Rule.Thm ("integral_var", ThmC.numerals_to_Free @{thm integral_var}),
132 Rule.Thm ("integral_add", ThmC.numerals_to_Free @{thm integral_add}),
133 Rule.Thm ("integral_mult", ThmC.numerals_to_Free @{thm integral_mult}),
134 Rule.Thm ("integral_pow", ThmC.numerals_to_Free @{thm integral_pow}),
135 Rule.Eval ("Groups.plus_class.plus", (**)eval_binop "#add_")(*for n+1*)
137 scr = Rule.Empty_Prog};
141 Rule_Set.Sequence {id="add_new_c", preconds = [],
142 rew_ord = ("termlessI",termlessI),
143 erls = Rule_Def.Repeat {id="conditions_in_add_new_c",
145 rew_ord = ("termlessI",termlessI),
146 erls = Rule_Set.Empty,
147 srls = Rule_Set.Empty, calc = [], errpatts = [],
148 rules = [Rule.Eval ("Prog_Expr.matches", Prog_Expr.eval_matches""),
149 Rule.Eval ("Integrate.is_f_x",
150 eval_is_f_x "is_f_x_"),
151 Rule.Thm ("not_true", ThmC.numerals_to_Free @{thm not_true}),
152 Rule.Thm ("not_false", ThmC.numerals_to_Free @{thm not_false})
154 scr = Rule.Empty_Prog},
155 srls = Rule_Set.Empty, calc = [], errpatts = [],
156 rules = [ (*Rule.Thm ("call_for_new_c", ThmC.numerals_to_Free @{thm call_for_new_c}),*)
157 Rule.Cal1 ("Integrate.add_new_c", eval_add_new_c "new_c_")
159 scr = Rule.Empty_Prog};
163 (*.rulesets for simplifying Integrals.*)
165 (*.for simplify_Integral adapted from 'norm_Rational_rls'.*)
166 val norm_Rational_rls_noadd_fractions =
167 Rule_Def.Repeat {id = "norm_Rational_rls_noadd_fractions", preconds = [],
168 rew_ord = ("dummy_ord",Rewrite_Ord.dummy_ord),
169 erls = norm_rat_erls, srls = Rule_Set.Empty, calc = [], errpatts = [],
170 rules = [(*Rule.Rls_ add_fractions_p_rls,!!!*)
171 Rule.Rls_ (*rat_mult_div_pow original corrected WN051028*)
172 (Rule_Def.Repeat {id = "rat_mult_div_pow", preconds = [],
173 rew_ord = ("dummy_ord",Rewrite_Ord.dummy_ord),
174 erls = (*FIXME.WN051028 Rule_Set.empty,*)
175 Rule_Set.append_rules "Rule_Set.empty-is_polyexp" Rule_Set.empty
176 [Rule.Eval ("Poly.is_polyexp",
177 eval_is_polyexp "")],
178 srls = Rule_Set.Empty, calc = [], errpatts = [],
179 rules = [Rule.Thm ("rat_mult", ThmC.numerals_to_Free @{thm rat_mult}),
180 (*"?a / ?b * (?c / ?d) = ?a * ?c / (?b * ?d)"*)
181 Rule.Thm ("rat_mult_poly_l", ThmC.numerals_to_Free @{thm rat_mult_poly_l}),
182 (*"?c is_polyexp ==> ?c * (?a / ?b) = ?c * ?a / ?b"*)
183 Rule.Thm ("rat_mult_poly_r", ThmC.numerals_to_Free @{thm rat_mult_poly_r}),
184 (*"?c is_polyexp ==> ?a / ?b * ?c = ?a * ?c / ?b"*)
186 Rule.Thm ("real_divide_divide1_mg",
187 ThmC.numerals_to_Free @{thm real_divide_divide1_mg}),
188 (*"y ~= 0 ==> (u / v) / (y / z) = (u * z) / (y * v)"*)
189 Rule.Thm ("divide_divide_eq_right",
190 ThmC.numerals_to_Free @{thm divide_divide_eq_right}),
191 (*"?x / (?y / ?z) = ?x * ?z / ?y"*)
192 Rule.Thm ("divide_divide_eq_left",
193 ThmC.numerals_to_Free @{thm divide_divide_eq_left}),
194 (*"?x / ?y / ?z = ?x / (?y * ?z)"*)
195 Rule.Eval ("Rings.divide_class.divide", Prog_Expr.eval_cancel "#divide_e"),
197 Rule.Thm ("rat_power", ThmC.numerals_to_Free @{thm rat_power})
198 (*"(?a / ?b) \<up> ?n = ?a \<up> ?n / ?b \<up> ?n"*)
200 scr = Rule.Empty_Prog
202 Rule.Rls_ make_rat_poly_with_parentheses,
203 Rule.Rls_ cancel_p_rls,(*FIXME:cancel_p does NOT order sometimes*)
204 Rule.Rls_ rat_reduce_1
206 scr = Rule.Empty_Prog
209 (*.for simplify_Integral adapted from 'norm_Rational'.*)
210 val norm_Rational_noadd_fractions =
211 Rule_Set.Sequence {id = "norm_Rational_noadd_fractions", preconds = [],
212 rew_ord = ("dummy_ord",Rewrite_Ord.dummy_ord),
213 erls = norm_rat_erls, srls = Rule_Set.Empty, calc = [], errpatts = [],
214 rules = [Rule.Rls_ discard_minus,
215 Rule.Rls_ rat_mult_poly,(* removes double fractions like a/b/c *)
216 Rule.Rls_ make_rat_poly_with_parentheses, (*WN0510 also in(#)below*)
217 Rule.Rls_ cancel_p_rls, (*FIXME.MG:cancel_p does NOT order sometim*)
218 Rule.Rls_ norm_Rational_rls_noadd_fractions,(* the main rls (#) *)
219 Rule.Rls_ discard_parentheses1 (* mult only *)
221 scr = Rule.Empty_Prog
224 (*.simplify terms before and after Integration such that
225 ..a.x^2/2 + b.x^3/3.. is made to ..a/2.x^2 + b/3.x^3.. (and NO
226 common denominator as done by norm_Rational or make_ratpoly_in.
227 This is a copy from 'make_ratpoly_in' with respective reduction of rules and
228 *1* expand the term, ie. distribute * and / over +
231 Rule_Set.append_rules "separate_bdv2"
233 [Rule.Thm ("separate_bdv", ThmC.numerals_to_Free @{thm separate_bdv}),
234 (*"?a * ?bdv / ?b = ?a / ?b * ?bdv"*)
235 Rule.Thm ("separate_bdv_n", ThmC.numerals_to_Free @{thm separate_bdv_n}),
236 Rule.Thm ("separate_1_bdv", ThmC.numerals_to_Free @{thm separate_1_bdv}),
237 (*"?bdv / ?b = (1 / ?b) * ?bdv"*)
238 Rule.Thm ("separate_1_bdv_n", ThmC.numerals_to_Free @{thm separate_1_bdv_n})(*,
239 (*"?bdv \<up> ?n / ?b = 1 / ?b * ?bdv \<up> ?n"*)
240 *****Rule.Thm ("add_divide_distrib",
241 ***** ThmC.numerals_to_Free @{thm add_divide_distrib})
242 (*"(?x + ?y) / ?z = ?x / ?z + ?y / ?z"*)----------*)
244 val simplify_Integral =
245 Rule_Set.Sequence {id = "simplify_Integral", preconds = []:term list,
246 rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord),
247 erls = Atools_erls, srls = Rule_Set.Empty,
248 calc = [], errpatts = [],
249 rules = [Rule.Thm ("distrib_right", ThmC.numerals_to_Free @{thm distrib_right}),
250 (*"(?z1.0 + ?z2.0) * ?w = ?z1.0 * ?w + ?z2.0 * ?w"*)
251 Rule.Thm ("add_divide_distrib", ThmC.numerals_to_Free @{thm add_divide_distrib}),
252 (*"(?x + ?y) / ?z = ?x / ?z + ?y / ?z"*)
253 (*^^^^^ *1* ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^*)
254 Rule.Rls_ norm_Rational_noadd_fractions,
255 Rule.Rls_ order_add_mult_in,
256 Rule.Rls_ discard_parentheses,
257 (*Rule.Rls_ collect_bdv, from make_polynomial_in*)
258 Rule.Rls_ separate_bdv2,
259 Rule.Eval ("Rings.divide_class.divide", Prog_Expr.eval_cancel "#divide_e")
261 scr = Rule.Empty_Prog};
264 (*simplify terms before and after Integration such that
265 ..a.x^2/2 + b.x^3/3.. is made to ..a/2.x^2 + b/3.x^3.. (and NO
266 common denominator as done by norm_Rational or make_ratpoly_in.
267 This is a copy from 'make_polynomial_in' with insertions from
269 THIS IS KEPT FOR COMPARISON ............................................
270 * val simplify_Integral = prep_rls'(
271 * Rule_Set.Sequence {id = "", preconds = []:term list,
272 * rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord),
273 * erls = Atools_erls, srls = Rule_Set.Empty,
274 * calc = [], (*asm_thm = [],*)
275 * rules = [Rule.Rls_ expand_poly,
276 * Rule.Rls_ order_add_mult_in,
277 * Rule.Rls_ simplify_power,
278 * Rule.Rls_ collect_numerals,
279 * Rule.Rls_ reduce_012,
280 * Rule.Thm ("realpow_oneI", ThmC.numerals_to_Free @{thm realpow_oneI}),
281 * Rule.Rls_ discard_parentheses,
282 * Rule.Rls_ collect_bdv,
283 * (*below inserted from 'make_ratpoly_in'*)
284 * Rule.Rls_ (Rule_Set.append_rules "separate_bdv"
286 * [Rule.Thm ("separate_bdv", ThmC.numerals_to_Free @{thm separate_bdv}),
287 * (*"?a * ?bdv / ?b = ?a / ?b * ?bdv"*)
288 * Rule.Thm ("separate_bdv_n", ThmC.numerals_to_Free @{thm separate_bdv_n}),
289 * Rule.Thm ("separate_1_bdv", ThmC.numerals_to_Free @{thm separate_1_bdv}),
290 * (*"?bdv / ?b = (1 / ?b) * ?bdv"*)
291 * Rule.Thm ("separate_1_bdv_n", ThmC.numerals_to_Free @{thm separate_1_bdv_n})(*,
292 * (*"?bdv \<up> ?n / ?b = 1 / ?b * ?bdv \<up> ?n"*)
293 * Rule.Thm ("add_divide_distrib",
294 * ThmC.numerals_to_Free @{thm add_divide_distrib})
295 * (*"(?x + ?y) / ?z = ?x / ?z + ?y / ?z"*)*)
297 * Rule.Eval ("Rings.divide_class.divide" , eval_cancel "#divide_e")
299 * scr = Rule.Empty_Prog
301 .......................................................................*)
304 Rule_Set.Sequence {id="integration", preconds = [],
305 rew_ord = ("termlessI",termlessI),
306 erls = Rule_Def.Repeat {id="conditions_in_integration",
308 rew_ord = ("termlessI",termlessI),
309 erls = Rule_Set.Empty,
310 srls = Rule_Set.Empty, calc = [], errpatts = [],
312 scr = Rule.Empty_Prog},
313 srls = Rule_Set.Empty, calc = [], errpatts = [],
314 rules = [ Rule.Rls_ integration_rules,
316 Rule.Rls_ simplify_Integral
318 scr = Rule.Empty_Prog};
320 val prep_rls' = Auto_Prog.prep_rls @{theory};
322 setup \<open>KEStore_Elems.add_rlss
323 [("integration_rules", (Context.theory_name @{theory}, prep_rls' integration_rules)),
324 ("add_new_c", (Context.theory_name @{theory}, prep_rls' add_new_c)),
325 ("simplify_Integral", (Context.theory_name @{theory}, prep_rls' simplify_Integral)),
326 ("integration", (Context.theory_name @{theory}, prep_rls' integration)),
327 ("separate_bdv2", (Context.theory_name @{theory}, prep_rls' separate_bdv2)),
329 ("norm_Rational_noadd_fractions", (Context.theory_name @{theory},
330 prep_rls' norm_Rational_noadd_fractions)),
331 ("norm_Rational_rls_noadd_fractions", (Context.theory_name @{theory},
332 prep_rls' norm_Rational_rls_noadd_fractions))]\<close>
335 setup \<open>KEStore_Elems.add_pbts
336 [(Problem.prep_input thy "pbl_fun_integ" [] Problem.id_empty
337 (["integrate", "function"],
338 [("#Given" ,["functionTerm f_f", "integrateBy v_v"]),
339 ("#Find" ,["antiDerivative F_F"])],
340 Rule_Set.append_rules "empty" Rule_Set.empty [(*for preds in where_*)],
341 SOME "Integrate (f_f, v_v)",
342 [["diff", "integration"]])),
343 (*here "named" is used differently from Differentiation"*)
344 (Problem.prep_input thy "pbl_fun_integ_nam" [] Problem.id_empty
345 (["named", "integrate", "function"],
346 [("#Given" ,["functionTerm f_f", "integrateBy v_v"]),
347 ("#Find" ,["antiDerivativeName F_F"])],
348 Rule_Set.append_rules "empty" Rule_Set.empty [(*for preds in where_*)],
349 SOME "Integrate (f_f, v_v)",
350 [["diff", "integration", "named"]]))]\<close>
354 partial_function (tailrec) integrate :: "real \<Rightarrow> real \<Rightarrow> real"
356 "integrate f_f v_v = (
358 t_t = Take (Integral f_f D v_v)
360 (Rewrite_Set_Inst [(''bdv'', v_v)] ''integration'') t_t)"
361 setup \<open>KEStore_Elems.add_mets
362 [MethodC.prep_input thy "met_diffint" [] MethodC.id_empty
363 (["diff", "integration"],
364 [("#Given" ,["functionTerm f_f", "integrateBy v_v"]), ("#Find" ,["antiDerivative F_F"])],
365 {rew_ord'="tless_true", rls'=Atools_erls, calc = [], srls = Rule_Set.empty, prls=Rule_Set.empty,
366 crls = Atools_erls, errpats = [], nrls = Rule_Set.empty},
367 @{thm integrate.simps})]
370 partial_function (tailrec) intergrate_named :: "real \<Rightarrow> real \<Rightarrow> (real \<Rightarrow> real) \<Rightarrow> bool"
372 "intergrate_named f_f v_v F_F =(
374 t_t = Take (F_F v_v = Integral f_f D v_v)
376 (Try (Rewrite_Set_Inst [(''bdv'', v_v)] ''simplify_Integral'')) #>
377 (Rewrite_Set_Inst [(''bdv'', v_v)] ''integration'')
379 setup \<open>KEStore_Elems.add_mets
380 [MethodC.prep_input thy "met_diffint_named" [] MethodC.id_empty
381 (["diff", "integration", "named"],
382 [("#Given" ,["functionTerm f_f", "integrateBy v_v"]),
383 ("#Find" ,["antiDerivativeName F_F"])],
384 {rew_ord'="tless_true", rls'=Atools_erls, calc = [], srls = Rule_Set.empty, prls=Rule_Set.empty,
385 crls = Atools_erls, errpats = [], nrls = Rule_Set.empty},
386 @{thm intergrate_named.simps})]