|
1 (* tools for integration over the reals |
|
2 author: Walther Neuper 050905, 08:51 |
|
3 (c) due to copyright terms |
|
4 |
|
5 use"Knowledge/Integrate.ML"; |
|
6 use"Integrate.ML"; |
|
7 |
|
8 remove_thy"Integrate"; |
|
9 use_thy"Knowledge/Isac"; |
|
10 *) |
|
11 |
|
12 (** interface isabelle -- isac **) |
|
13 |
|
14 theory' := overwritel (!theory', [("Integrate.thy",Integrate.thy)]); |
|
15 |
|
16 (** eval functions **) |
|
17 |
|
18 val c = Free ("c", HOLogic.realT); |
|
19 (*.create a new unique variable 'c..' in a term; for use by Calc in a rls; |
|
20 an alternative to do this would be '(Try (Calculate new_c_) (new_c es__))' |
|
21 in the script; this will be possible if currying doesnt take the value |
|
22 from a variable, but the value '(new_c es__)' itself.*) |
|
23 fun new_c term = |
|
24 let fun selc var = |
|
25 case (explode o id_of) var of |
|
26 "c"::[] => true |
|
27 | "c"::"_"::is => (case (int_of_str o implode) is of |
|
28 SOME _ => true |
|
29 | NONE => false) |
|
30 | _ => false; |
|
31 fun get_coeff c = case (explode o id_of) c of |
|
32 "c"::"_"::is => (the o int_of_str o implode) is |
|
33 | _ => 0; |
|
34 val cs = filter selc (vars term); |
|
35 in |
|
36 case cs of |
|
37 [] => c |
|
38 | [c] => Free ("c_2", HOLogic.realT) |
|
39 | cs => |
|
40 let val max_coeff = maxl (map get_coeff cs) |
|
41 in Free ("c_"^string_of_int (max_coeff + 1), HOLogic.realT) end |
|
42 end; |
|
43 |
|
44 (*WN080222 |
|
45 (*("new_c", ("Integrate.new'_c", eval_new_c "#new_c_"))*) |
|
46 fun eval_new_c _ _ (p as (Const ("Integrate.new'_c",_) $ t)) _ = |
|
47 SOME ((term2str p) ^ " = " ^ term2str (new_c p), |
|
48 Trueprop $ (mk_equality (p, new_c p))) |
|
49 | eval_new_c _ _ _ _ = NONE; |
|
50 *) |
|
51 |
|
52 (*WN080222:*) |
|
53 (*("add_new_c", ("Integrate.add'_new'_c", eval_add_new_c "#add_new_c_")) |
|
54 add a new c to a term or a fun-equation; |
|
55 this is _not in_ the term, because only applied to _whole_ term*) |
|
56 fun eval_add_new_c (_:string) "Integrate.add'_new'_c" p (_:theory) = |
|
57 let val p' = case p of |
|
58 Const ("op =", T) $ lh $ rh => |
|
59 Const ("op =", T) $ lh $ mk_add rh (new_c rh) |
|
60 | p => mk_add p (new_c p) |
|
61 in SOME ((term2str p) ^ " = " ^ term2str p', |
|
62 Trueprop $ (mk_equality (p, p'))) |
|
63 end |
|
64 | eval_add_new_c _ _ _ _ = NONE; |
|
65 |
|
66 |
|
67 (*("is_f_x", ("Integrate.is'_f'_x", eval_is_f_x "is_f_x_"))*) |
|
68 fun eval_is_f_x _ _(p as (Const ("Integrate.is'_f'_x", _) |
|
69 $ arg)) _ = |
|
70 if is_f_x arg |
|
71 then SOME ((term2str p) ^ " = True", |
|
72 Trueprop $ (mk_equality (p, HOLogic.true_const))) |
|
73 else SOME ((term2str p) ^ " = False", |
|
74 Trueprop $ (mk_equality (p, HOLogic.false_const))) |
|
75 | eval_is_f_x _ _ _ _ = NONE; |
|
76 |
|
77 calclist':= overwritel (!calclist', |
|
78 [(*("new_c", ("Integrate.new'_c", eval_new_c "new_c_")),*) |
|
79 ("add_new_c", ("Integrate.add'_new'_c", eval_add_new_c "add_new_c_")), |
|
80 ("is_f_x", ("Integrate.is'_f'_x", eval_is_f_x "is_f_idextifier_")) |
|
81 ]); |
|
82 |
|
83 |
|
84 (** rulesets **) |
|
85 |
|
86 (*.rulesets for integration.*) |
|
87 val integration_rules = |
|
88 Rls {id="integration_rules", preconds = [], |
|
89 rew_ord = ("termlessI",termlessI), |
|
90 erls = Rls {id="conditions_in_integration_rules", |
|
91 preconds = [], |
|
92 rew_ord = ("termlessI",termlessI), |
|
93 erls = Erls, |
|
94 srls = Erls, calc = [], |
|
95 rules = [(*for rewriting conditions in Thm's*) |
|
96 Calc ("Atools.occurs'_in", |
|
97 eval_occurs_in "#occurs_in_"), |
|
98 Thm ("not_true",num_str not_true), |
|
99 Thm ("not_false",not_false) |
|
100 ], |
|
101 scr = EmptyScr}, |
|
102 srls = Erls, calc = [], |
|
103 rules = [ |
|
104 Thm ("integral_const",num_str integral_const), |
|
105 Thm ("integral_var",num_str integral_var), |
|
106 Thm ("integral_add",num_str integral_add), |
|
107 Thm ("integral_mult",num_str integral_mult), |
|
108 Thm ("integral_pow",num_str integral_pow), |
|
109 Calc ("op +", eval_binop "#add_")(*for n+1*) |
|
110 ], |
|
111 scr = EmptyScr}; |
|
112 val add_new_c = |
|
113 Seq {id="add_new_c", preconds = [], |
|
114 rew_ord = ("termlessI",termlessI), |
|
115 erls = Rls {id="conditions_in_add_new_c", |
|
116 preconds = [], |
|
117 rew_ord = ("termlessI",termlessI), |
|
118 erls = Erls, |
|
119 srls = Erls, calc = [], |
|
120 rules = [Calc ("Tools.matches", eval_matches""), |
|
121 Calc ("Integrate.is'_f'_x", |
|
122 eval_is_f_x "is_f_x_"), |
|
123 Thm ("not_true",num_str not_true), |
|
124 Thm ("not_false",num_str not_false) |
|
125 ], |
|
126 scr = EmptyScr}, |
|
127 srls = Erls, calc = [], |
|
128 rules = [ (*Thm ("call_for_new_c", num_str call_for_new_c),*) |
|
129 Cal1 ("Integrate.add'_new'_c", eval_add_new_c "new_c_") |
|
130 ], |
|
131 scr = EmptyScr}; |
|
132 |
|
133 (*.rulesets for simplifying Integrals.*) |
|
134 |
|
135 (*.for simplify_Integral adapted from 'norm_Rational_rls'.*) |
|
136 val norm_Rational_rls_noadd_fractions = |
|
137 Rls {id = "norm_Rational_rls_noadd_fractions", preconds = [], |
|
138 rew_ord = ("dummy_ord",dummy_ord), |
|
139 erls = norm_rat_erls, srls = Erls, calc = [], |
|
140 rules = [(*Rls_ common_nominator_p_rls,!!!*) |
|
141 Rls_ (*rat_mult_div_pow original corrected WN051028*) |
|
142 (Rls {id = "rat_mult_div_pow", preconds = [], |
|
143 rew_ord = ("dummy_ord",dummy_ord), |
|
144 erls = (*FIXME.WN051028 e_rls,*) |
|
145 append_rls "e_rls-is_polyexp" e_rls |
|
146 [Calc ("Poly.is'_polyexp", |
|
147 eval_is_polyexp "")], |
|
148 srls = Erls, calc = [], |
|
149 rules = [Thm ("rat_mult",num_str rat_mult), |
|
150 (*"?a / ?b * (?c / ?d) = ?a * ?c / (?b * ?d)"*) |
|
151 Thm ("rat_mult_poly_l",num_str rat_mult_poly_l), |
|
152 (*"?c is_polyexp ==> ?c * (?a / ?b) = ?c * ?a / ?b"*) |
|
153 Thm ("rat_mult_poly_r",num_str rat_mult_poly_r), |
|
154 (*"?c is_polyexp ==> ?a / ?b * ?c = ?a * ?c / ?b"*) |
|
155 |
|
156 Thm ("real_divide_divide1_mg", real_divide_divide1_mg), |
|
157 (*"y ~= 0 ==> (u / v) / (y / z) = (u * z) / (y * v)"*) |
|
158 Thm ("real_divide_divide1_eq", real_divide_divide1_eq), |
|
159 (*"?x / (?y / ?z) = ?x * ?z / ?y"*) |
|
160 Thm ("real_divide_divide2_eq", real_divide_divide2_eq), |
|
161 (*"?x / ?y / ?z = ?x / (?y * ?z)"*) |
|
162 Calc ("HOL.divide" ,eval_cancel "#divide_"), |
|
163 |
|
164 Thm ("rat_power", num_str rat_power) |
|
165 (*"(?a / ?b) ^^^ ?n = ?a ^^^ ?n / ?b ^^^ ?n"*) |
|
166 ], |
|
167 scr = Script ((term_of o the o (parse thy)) "empty_script") |
|
168 }), |
|
169 Rls_ make_rat_poly_with_parentheses, |
|
170 Rls_ cancel_p_rls,(*FIXME:cancel_p does NOT order sometimes*) |
|
171 Rls_ rat_reduce_1 |
|
172 ], |
|
173 scr = Script ((term_of o the o (parse thy)) "empty_script") |
|
174 }:rls; |
|
175 |
|
176 (*.for simplify_Integral adapted from 'norm_Rational'.*) |
|
177 val norm_Rational_noadd_fractions = |
|
178 Seq {id = "norm_Rational_noadd_fractions", preconds = [], |
|
179 rew_ord = ("dummy_ord",dummy_ord), |
|
180 erls = norm_rat_erls, srls = Erls, calc = [], |
|
181 rules = [Rls_ discard_minus_, |
|
182 Rls_ rat_mult_poly,(* removes double fractions like a/b/c *) |
|
183 Rls_ make_rat_poly_with_parentheses, (*WN0510 also in(#)below*) |
|
184 Rls_ cancel_p_rls, (*FIXME.MG:cancel_p does NOT order sometim*) |
|
185 Rls_ norm_Rational_rls_noadd_fractions,(* the main rls (#) *) |
|
186 Rls_ discard_parentheses_ (* mult only *) |
|
187 ], |
|
188 scr = Script ((term_of o the o (parse thy)) "empty_script") |
|
189 }:rls; |
|
190 |
|
191 (*.simplify terms before and after Integration such that |
|
192 ..a.x^2/2 + b.x^3/3.. is made to ..a/2.x^2 + b/3.x^3.. (and NO |
|
193 common denominator as done by norm_Rational or make_ratpoly_in. |
|
194 This is a copy from 'make_ratpoly_in' with respective reduction of rules and |
|
195 *1* expand the term, ie. distribute * and / over + |
|
196 .*) |
|
197 val separate_bdv2 = |
|
198 append_rls "separate_bdv2" |
|
199 collect_bdv |
|
200 [Thm ("separate_bdv", num_str separate_bdv), |
|
201 (*"?a * ?bdv / ?b = ?a / ?b * ?bdv"*) |
|
202 Thm ("separate_bdv_n", num_str separate_bdv_n), |
|
203 Thm ("separate_1_bdv", num_str separate_1_bdv), |
|
204 (*"?bdv / ?b = (1 / ?b) * ?bdv"*) |
|
205 Thm ("separate_1_bdv_n", num_str separate_1_bdv_n)(*, |
|
206 (*"?bdv ^^^ ?n / ?b = 1 / ?b * ?bdv ^^^ ?n"*) |
|
207 *****Thm ("real_add_divide_distrib", |
|
208 *****num_str real_add_divide_distrib) |
|
209 (*"(?x + ?y) / ?z = ?x / ?z + ?y / ?z"*)----------*) |
|
210 ]; |
|
211 val simplify_Integral = |
|
212 Seq {id = "simplify_Integral", preconds = []:term list, |
|
213 rew_ord = ("dummy_ord", dummy_ord), |
|
214 erls = Atools_erls, srls = Erls, |
|
215 calc = [], (*asm_thm = [],*) |
|
216 rules = [Thm ("real_add_mult_distrib",num_str real_add_mult_distrib), |
|
217 (*"(?z1.0 + ?z2.0) * ?w = ?z1.0 * ?w + ?z2.0 * ?w"*) |
|
218 Thm ("real_add_divide_distrib",num_str real_add_divide_distrib), |
|
219 (*"(?x + ?y) / ?z = ?x / ?z + ?y / ?z"*) |
|
220 (*^^^^^ *1* ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^*) |
|
221 Rls_ norm_Rational_noadd_fractions, |
|
222 Rls_ order_add_mult_in, |
|
223 Rls_ discard_parentheses, |
|
224 (*Rls_ collect_bdv, from make_polynomial_in*) |
|
225 Rls_ separate_bdv2, |
|
226 Calc ("HOL.divide" ,eval_cancel "#divide_") |
|
227 ], |
|
228 scr = EmptyScr}:rls; |
|
229 |
|
230 |
|
231 (*simplify terms before and after Integration such that |
|
232 ..a.x^2/2 + b.x^3/3.. is made to ..a/2.x^2 + b/3.x^3.. (and NO |
|
233 common denominator as done by norm_Rational or make_ratpoly_in. |
|
234 This is a copy from 'make_polynomial_in' with insertions from |
|
235 'make_ratpoly_in' |
|
236 THIS IS KEPT FOR COMPARISON ............................................ |
|
237 * val simplify_Integral = prep_rls( |
|
238 * Seq {id = "", preconds = []:term list, |
|
239 * rew_ord = ("dummy_ord", dummy_ord), |
|
240 * erls = Atools_erls, srls = Erls, |
|
241 * calc = [], (*asm_thm = [],*) |
|
242 * rules = [Rls_ expand_poly, |
|
243 * Rls_ order_add_mult_in, |
|
244 * Rls_ simplify_power, |
|
245 * Rls_ collect_numerals, |
|
246 * Rls_ reduce_012, |
|
247 * Thm ("realpow_oneI",num_str realpow_oneI), |
|
248 * Rls_ discard_parentheses, |
|
249 * Rls_ collect_bdv, |
|
250 * (*below inserted from 'make_ratpoly_in'*) |
|
251 * Rls_ (append_rls "separate_bdv" |
|
252 * collect_bdv |
|
253 * [Thm ("separate_bdv", num_str separate_bdv), |
|
254 * (*"?a * ?bdv / ?b = ?a / ?b * ?bdv"*) |
|
255 * Thm ("separate_bdv_n", num_str separate_bdv_n), |
|
256 * Thm ("separate_1_bdv", num_str separate_1_bdv), |
|
257 * (*"?bdv / ?b = (1 / ?b) * ?bdv"*) |
|
258 * Thm ("separate_1_bdv_n", num_str separate_1_bdv_n)(*, |
|
259 * (*"?bdv ^^^ ?n / ?b = 1 / ?b * ?bdv ^^^ ?n"*) |
|
260 * Thm ("real_add_divide_distrib", |
|
261 * num_str real_add_divide_distrib) |
|
262 * (*"(?x + ?y) / ?z = ?x / ?z + ?y / ?z"*)*) |
|
263 * ]), |
|
264 * Calc ("HOL.divide" ,eval_cancel "#divide_") |
|
265 * ], |
|
266 * scr = EmptyScr |
|
267 * }:rls); |
|
268 .......................................................................*) |
|
269 |
|
270 val integration = |
|
271 Seq {id="integration", preconds = [], |
|
272 rew_ord = ("termlessI",termlessI), |
|
273 erls = Rls {id="conditions_in_integration", |
|
274 preconds = [], |
|
275 rew_ord = ("termlessI",termlessI), |
|
276 erls = Erls, |
|
277 srls = Erls, calc = [], |
|
278 rules = [], |
|
279 scr = EmptyScr}, |
|
280 srls = Erls, calc = [], |
|
281 rules = [ Rls_ integration_rules, |
|
282 Rls_ add_new_c, |
|
283 Rls_ simplify_Integral |
|
284 ], |
|
285 scr = EmptyScr}; |
|
286 ruleset' := |
|
287 overwritelthy thy (!ruleset', |
|
288 [("integration_rules", prep_rls integration_rules), |
|
289 ("add_new_c", prep_rls add_new_c), |
|
290 ("simplify_Integral", prep_rls simplify_Integral), |
|
291 ("integration", prep_rls integration), |
|
292 ("separate_bdv2", separate_bdv2), |
|
293 ("norm_Rational_noadd_fractions", norm_Rational_noadd_fractions), |
|
294 ("norm_Rational_rls_noadd_fractions", |
|
295 norm_Rational_rls_noadd_fractions) |
|
296 ]); |
|
297 |
|
298 (** problems **) |
|
299 |
|
300 store_pbt |
|
301 (prep_pbt Integrate.thy "pbl_fun_integ" [] e_pblID |
|
302 (["integrate","function"], |
|
303 [("#Given" ,["functionTerm f_", "integrateBy v_"]), |
|
304 ("#Find" ,["antiDerivative F_"]) |
|
305 ], |
|
306 append_rls "e_rls" e_rls [(*for preds in where_*)], |
|
307 SOME "Integrate (f_, v_)", |
|
308 [["diff","integration"]])); |
|
309 |
|
310 (*here "named" is used differently from Differentiation"*) |
|
311 store_pbt |
|
312 (prep_pbt Integrate.thy "pbl_fun_integ_nam" [] e_pblID |
|
313 (["named","integrate","function"], |
|
314 [("#Given" ,["functionTerm f_", "integrateBy v_"]), |
|
315 ("#Find" ,["antiDerivativeName F_"]) |
|
316 ], |
|
317 append_rls "e_rls" e_rls [(*for preds in where_*)], |
|
318 SOME "Integrate (f_, v_)", |
|
319 [["diff","integration","named"]])); |
|
320 |
|
321 (** methods **) |
|
322 |
|
323 store_met |
|
324 (prep_met Integrate.thy "met_diffint" [] e_metID |
|
325 (["diff","integration"], |
|
326 [("#Given" ,["functionTerm f_", "integrateBy v_"]), |
|
327 ("#Find" ,["antiDerivative F_"]) |
|
328 ], |
|
329 {rew_ord'="tless_true", rls'=Atools_erls, calc = [], |
|
330 srls = e_rls, |
|
331 prls=e_rls, |
|
332 crls = Atools_erls, nrls = e_rls}, |
|
333 "Script IntegrationScript (f_::real) (v_::real) = \ |
|
334 \ (let t_ = Take (Integral f_ D v_) \ |
|
335 \ in (Rewrite_Set_Inst [(bdv,v_)] integration False) (t_::real))" |
|
336 )); |
|
337 |
|
338 store_met |
|
339 (prep_met Integrate.thy "met_diffint_named" [] e_metID |
|
340 (["diff","integration","named"], |
|
341 [("#Given" ,["functionTerm f_", "integrateBy v_"]), |
|
342 ("#Find" ,["antiDerivativeName F_"]) |
|
343 ], |
|
344 {rew_ord'="tless_true", rls'=Atools_erls, calc = [], |
|
345 srls = e_rls, |
|
346 prls=e_rls, |
|
347 crls = Atools_erls, nrls = e_rls}, |
|
348 "Script NamedIntegrationScript (f_::real) (v_::real) (F_::real=>real) = \ |
|
349 \ (let t_ = Take (F_ v_ = Integral f_ D v_) \ |
|
350 \ in ((Try (Rewrite_Set_Inst [(bdv,v_)] simplify_Integral False)) @@\ |
|
351 \ (Rewrite_Set_Inst [(bdv,v_)] integration False)) t_)" |
|
352 (* |
|
353 "Script NamedIntegrationScript (f_::real) (v_::real) (F_::real=>real) = \ |
|
354 \ (let t_ = Take (F_ v_ = Integral f_ D v_) \ |
|
355 \ in (Rewrite_Set_Inst [(bdv,v_)] integration False) t_)" |
|
356 *) |
|
357 )); |