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 add_new_c :: "real => real" ("add'_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 -----------------------------//*)
44 (** eval functions **)
46 val c = Free ("c", HOLogic.realT);
47 (*.create a new unique variable 'c..' in a term; for use by \<^rule_eval> in a rls;
48 an alternative to do this would be '(Try (Calculate new_c_) (new_c es__))'
49 in the script; this will be possible if currying doesnt take the value
50 from a variable, but the value '(new_c es__)' itself.*)
53 case (Symbol.explode o id_of) var of
55 | "c"::"_"::is => (case (TermC.int_opt_of_string o implode) is of
59 fun get_coeff c = case (Symbol.explode o id_of) c of
60 "c"::"_"::is => (the o TermC.int_opt_of_string o implode) is
62 val cs = filter selc (TermC.vars term);
66 | [_] => Free ("c_2", HOLogic.realT)
68 let val max_coeff = maxl (map get_coeff cs)
69 in Free ("c_"^string_of_int (max_coeff + 1), HOLogic.realT) end
73 (*("add_new_c", ("Integrate.add_new_c", eval_add_new_c "#add_new_c_"))
74 add a new c to a term or a fun-equation;
75 this is _not in_ the term, because only applied to _whole_ term*)
76 fun eval_add_new_c (_:string) "Integrate.add_new_c" p (_:Proof.context) =
77 let val p' = case p of
78 Const (\<^const_name>\<open>HOL.eq\<close>, T) $ lh $ rh =>
79 Const (\<^const_name>\<open>HOL.eq\<close>, T) $ lh $ TermC.mk_add rh (new_c rh)
80 | p => TermC.mk_add p (new_c p)
81 in SOME ((UnparseC.term p) ^ " = " ^ UnparseC.term p',
82 HOLogic.Trueprop $ (TermC.mk_equality (p, p')))
84 | eval_add_new_c _ _ _ _ = NONE;
87 (*("is_f_x", ("Integrate.is_f_x", eval_is_f_x "is_f_x_"))*)
88 fun eval_is_f_x _ _(p as (Const (\<^const_name>\<open>Integrate.is_f_x\<close>, _)
91 then SOME ((UnparseC.term_in_ctxt @{context} p) ^ " = True",
92 HOLogic.Trueprop $ (TermC.mk_equality (p, @{term True})))
93 else SOME ((UnparseC.term_in_ctxt @{context} p) ^ " = False",
94 HOLogic.Trueprop $ (TermC.mk_equality (p, @{term False})))
95 | eval_is_f_x _ _ _ _ = NONE;
98 calculation add_new_c = \<open>eval_add_new_c "add_new_c_"\<close>
99 calculation is_f_x = \<open>eval_is_f_x "is_f_idextifier_"\<close>
104 (*.rulesets for integration.*)
105 val integration_rules =
106 Rule_Def.Repeat {id="integration_rules", preconds = [],
107 rew_ord = ("termlessI",termlessI),
108 asm_rls = Rule_Def.Repeat {id="conditions_in_integration_rules",
110 rew_ord = ("termlessI",termlessI),
111 asm_rls = Rule_Set.Empty,
112 prog_rls = Rule_Set.Empty, calc = [], errpatts = [],
113 rules = [(*for rewriting conditions in Thm's*)
114 \<^rule_eval>\<open>Prog_Expr.occurs_in\<close> (Prog_Expr.eval_occurs_in "#occurs_in_"),
115 \<^rule_thm>\<open>not_true\<close>,
116 \<^rule_thm>\<open>not_false\<close>],
117 program = Rule.Empty_Prog},
118 prog_rls = Rule_Set.Empty, calc = [], errpatts = [],
120 \<^rule_thm>\<open>integral_const\<close>,
121 \<^rule_thm>\<open>integral_var\<close>,
122 \<^rule_thm>\<open>integral_add\<close>,
123 \<^rule_thm>\<open>integral_mult\<close>,
124 \<^rule_thm>\<open>integral_pow\<close>,
125 \<^rule_eval>\<open>plus\<close> (**)(Calc_Binop.numeric "#add_")(*for n+1*)],
126 program = Rule.Empty_Prog};
130 Rule_Set.Sequence {id="add_new_c", preconds = [],
131 rew_ord = ("termlessI",termlessI),
132 asm_rls = Rule_Def.Repeat {id="conditions_in_add_new_c",
133 preconds = [], rew_ord = ("termlessI",termlessI), asm_rls = Rule_Set.Empty,
134 prog_rls = Rule_Set.Empty, calc = [], errpatts = [],
136 \<^rule_eval>\<open>Prog_Expr.matches\<close> (Prog_Expr.eval_matches""),
137 \<^rule_eval>\<open>Integrate.is_f_x\<close> (eval_is_f_x "is_f_x_"),
138 \<^rule_thm>\<open>not_true\<close>,
139 \<^rule_thm>\<open>not_false\<close>],
140 program = Rule.Empty_Prog},
141 prog_rls = Rule_Set.Empty, calc = [], errpatts = [],
142 rules = [ (*\<^rule_thm>\<open>call_for_new_c\<close>,*)
143 Rule.Cal1 ("Integrate.add_new_c", eval_add_new_c "new_c_")],
144 program = Rule.Empty_Prog};
148 (*.rulesets for simplifying Integrals.*)
150 (*.for simplify_Integral adapted from 'norm_Rational_rls'.*)
151 val norm_Rational_rls_noadd_fractions =
152 Rule_Def.Repeat {id = "norm_Rational_rls_noadd_fractions", preconds = [],
153 rew_ord = ("dummy_ord",Rewrite_Ord.function_empty),
154 asm_rls = norm_rat_erls, prog_rls = Rule_Set.Empty, calc = [], errpatts = [],
155 rules = [(*Rule.Rls_ add_fractions_p_rls,!!!*)
156 Rule.Rls_ (*rat_mult_div_pow original corrected WN051028*)
157 (Rule_Def.Repeat {id = "rat_mult_div_pow", preconds = [],
158 rew_ord = ("dummy_ord",Rewrite_Ord.function_empty),
159 asm_rls = Rule_Set.append_rules "Rule_Set.empty-is_polyexp" Rule_Set.empty
160 [\<^rule_eval>\<open>is_polyexp\<close> (eval_is_polyexp "")],
161 prog_rls = Rule_Set.Empty, calc = [], errpatts = [],
163 \<^rule_thm>\<open>rat_mult\<close>, (*"?a / ?b * (?c / ?d) = ?a * ?c / (?b * ?d)"*)
164 \<^rule_thm>\<open>rat_mult_poly_l\<close>, (*"?c is_polyexp ==> ?c * (?a / ?b) = ?c * ?a / ?b"*)
165 \<^rule_thm>\<open>rat_mult_poly_r\<close>, (*"?c is_polyexp ==> ?a / ?b * ?c = ?a * ?c / ?b"*)
167 \<^rule_thm>\<open>real_divide_divide1_mg\<close>, (*"y ~= 0 ==> (u / v) / (y / z) = (u * z) / (y * v)"*)
168 \<^rule_thm>\<open>divide_divide_eq_right\<close>, (*"?x / (?y / ?z) = ?x * ?z / ?y"*)
169 \<^rule_thm>\<open>divide_divide_eq_left\<close>, (*"?x / ?y / ?z = ?x / (?y * ?z)"*)
170 \<^rule_eval>\<open>divide\<close> (Prog_Expr.eval_cancel "#divide_e"),
172 \<^rule_thm>\<open>rat_power\<close>], (*"(?a / ?b) \<up> ?n = ?a \<up> ?n / ?b \<up> ?n"*)
173 program = Rule.Empty_Prog}),
174 Rule.Rls_ make_rat_poly_with_parentheses,
175 Rule.Rls_ cancel_p_rls,(*FIXME:cancel_p does NOT order sometimes*)
176 Rule.Rls_ rat_reduce_1],
177 program = Rule.Empty_Prog};
179 (*.for simplify_Integral adapted from 'norm_Rational'.*)
180 val norm_Rational_noadd_fractions =
181 Rule_Set.Sequence {id = "norm_Rational_noadd_fractions", preconds = [],
182 rew_ord = ("dummy_ord",Rewrite_Ord.function_empty),
183 asm_rls = norm_rat_erls, prog_rls = Rule_Set.Empty, calc = [], errpatts = [],
184 rules = [Rule.Rls_ discard_minus,
185 Rule.Rls_ rat_mult_poly,(* removes double fractions like a/b/c *)
186 Rule.Rls_ make_rat_poly_with_parentheses, (*WN0510 also in(#)below*)
187 Rule.Rls_ cancel_p_rls, (*FIXME.MG:cancel_p does NOT order sometim*)
188 Rule.Rls_ norm_Rational_rls_noadd_fractions,(* the main rls (#) *)
189 Rule.Rls_ discard_parentheses1], (* mult only *)
190 program = Rule.Empty_Prog};
192 (*.simplify terms before and after Integration such that
193 ..a.x^2/2 + b.x^3/3.. is made to ..a/2.x^2 + b/3.x^3.. (and NO
194 common denominator as done by norm_Rational or make_ratpoly_in.
195 This is a copy from 'make_ratpoly_in' with respective reduction of rules and
196 *1* expand the term, ie. distribute * and / over +
199 Rule_Set.append_rules "separate_bdv2" collect_bdv [
200 \<^rule_thm>\<open>separate_bdv\<close>, (*"?a * ?bdv / ?b = ?a / ?b * ?bdv"*)
201 \<^rule_thm>\<open>separate_bdv_n\<close>,
202 \<^rule_thm>\<open>separate_1_bdv\<close>, (*"?bdv / ?b = (1 / ?b) * ?bdv"*)
203 \<^rule_thm>\<open>separate_1_bdv_n\<close> (*"?bdv \<up> ?n / ?b = 1 / ?b * ?bdv \<up> ?n"*)
205 rule_thm>\<open>add_divide_distrib\<close> (*"(?x + ?y) / ?z = ?x / ?z + ?y / ?z"*)*)
207 val simplify_Integral =
208 Rule_Set.Sequence {id = "simplify_Integral", preconds = []:term list,
209 rew_ord = ("dummy_ord", Rewrite_Ord.function_empty),
210 asm_rls = Atools_erls, prog_rls = Rule_Set.Empty,
211 calc = [], errpatts = [],
213 \<^rule_thm>\<open>distrib_right\<close>, (*"(?z1.0 + ?z2.0) * ?w = ?z1.0 * ?w + ?z2.0 * ?w"*)
214 \<^rule_thm>\<open>add_divide_distrib\<close>, (*"(?x + ?y) / ?z = ?x / ?z + ?y / ?z"*)
215 (*^^^^^ *1* ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^*)
216 Rule.Rls_ norm_Rational_noadd_fractions,
217 Rule.Rls_ order_add_mult_in,
218 Rule.Rls_ discard_parentheses,
219 (*Rule.Rls_ collect_bdv, from make_polynomial_in*)
220 Rule.Rls_ separate_bdv2,
221 \<^rule_eval>\<open>divide\<close> (Prog_Expr.eval_cancel "#divide_e")],
222 program = Rule.Empty_Prog};
226 id="integration", preconds = [], rew_ord = ("termlessI",termlessI),
227 asm_rls = Rule_Def.Repeat {
228 id="conditions_in_integration", preconds = [], rew_ord = ("termlessI",termlessI),
229 asm_rls = Rule_Set.Empty, prog_rls = Rule_Set.Empty, calc = [], errpatts = [],
230 rules = [], program = Rule.Empty_Prog},
231 prog_rls = Rule_Set.Empty, calc = [], errpatts = [],
233 Rule.Rls_ integration_rules,
235 Rule.Rls_ simplify_Integral],
236 program = Rule.Empty_Prog};
238 val prep_rls' = Auto_Prog.prep_rls @{theory};
241 integration_rules = \<open>prep_rls' integration_rules\<close> and
242 add_new_c = \<open>prep_rls' add_new_c\<close> and
243 simplify_Integral = \<open>prep_rls' simplify_Integral\<close> and
244 integration = \<open>prep_rls' integration\<close> and
245 separate_bdv2 = \<open>prep_rls' separate_bdv2\<close> and
246 norm_Rational_noadd_fractions = \<open>prep_rls' norm_Rational_noadd_fractions\<close> and
247 norm_Rational_rls_noadd_fractions = \<open>prep_rls' norm_Rational_rls_noadd_fractions\<close>
251 problem pbl_fun_integ : "integrate/function" =
252 \<open>Rule_Set.append_rules "empty" Rule_Set.empty [(*for preds in where_*)]\<close>
253 Method_Ref: "diff/integration"
254 CAS: "Integrate (f_f, v_v)"
255 Given: "functionTerm f_f" "integrateBy v_v"
256 Find: "antiDerivative F_F"
258 problem pbl_fun_integ_nam : "named/integrate/function" =
259 (*here "named" is used differently from Differentiation"*)
260 \<open>Rule_Set.append_rules "empty" Rule_Set.empty [(*for preds in where_*)]\<close>
261 Method_Ref: "diff/integration/named"
262 CAS: "Integrate (f_f, v_v)"
263 Given: "functionTerm f_f" "integrateBy v_v"
264 Find: "antiDerivativeName F_F"
268 partial_function (tailrec) integrate :: "real \<Rightarrow> real \<Rightarrow> real"
270 "integrate f_f v_v = (
272 t_t = Take (Integral f_f D v_v)
274 (Rewrite_Set_Inst [(''bdv'', v_v)] ''integration'') t_t)"
276 method met_diffint : "diff/integration" =
277 \<open>{rew_ord="tless_true", rls'=Atools_erls, calc = [], prog_rls = Rule_Set.empty, where_rls=Rule_Set.empty,
278 errpats = [], rew_rls = Rule_Set.empty}\<close>
279 Program: integrate.simps
280 Given: "functionTerm f_f" "integrateBy v_v"
281 Find: "antiDerivative F_F"
283 partial_function (tailrec) intergrate_named :: "real \<Rightarrow> real \<Rightarrow> (real \<Rightarrow> real) \<Rightarrow> bool"
285 "intergrate_named f_f v_v F_F =(
287 t_t = Take (F_F v_v = Integral f_f D v_v)
289 (Try (Rewrite_Set_Inst [(''bdv'', v_v)] ''simplify_Integral'')) #>
290 (Rewrite_Set_Inst [(''bdv'', v_v)] ''integration'')
293 method met_diffint_named : "diff/integration/named" =
294 \<open>{rew_ord="tless_true", rls'=Atools_erls, calc = [], prog_rls = Rule_Set.empty, where_rls=Rule_Set.empty,
295 errpats = [], rew_rls = Rule_Set.empty}\<close>
296 Program: intergrate_named.simps
297 Given: "functionTerm f_f" "integrateBy v_v"
298 Find: "antiDerivativeName F_F"