114 ML {* |
114 ML {* |
115 (** rulesets **) |
115 (** rulesets **) |
116 |
116 |
117 (*.rulesets for integration.*) |
117 (*.rulesets for integration.*) |
118 val integration_rules = |
118 val integration_rules = |
119 Rls {id="integration_rules", preconds = [], |
119 Celem.Rls {id="integration_rules", preconds = [], |
120 rew_ord = ("termlessI",termlessI), |
120 rew_ord = ("termlessI",termlessI), |
121 erls = Rls {id="conditions_in_integration_rules", |
121 erls = Celem.Rls {id="conditions_in_integration_rules", |
122 preconds = [], |
122 preconds = [], |
123 rew_ord = ("termlessI",termlessI), |
123 rew_ord = ("termlessI",termlessI), |
124 erls = Erls, |
124 erls = Celem.Erls, |
125 srls = Erls, calc = [], errpatts = [], |
125 srls = Celem.Erls, calc = [], errpatts = [], |
126 rules = [(*for rewriting conditions in Thm's*) |
126 rules = [(*for rewriting conditions in Thm's*) |
127 Calc ("Atools.occurs'_in", |
127 Celem.Calc ("Atools.occurs'_in", |
128 eval_occurs_in "#occurs_in_"), |
128 eval_occurs_in "#occurs_in_"), |
129 Thm ("not_true", TermC.num_str @{thm not_true}), |
129 Celem.Thm ("not_true", TermC.num_str @{thm not_true}), |
130 Thm ("not_false",@{thm not_false}) |
130 Celem.Thm ("not_false",@{thm not_false}) |
131 ], |
131 ], |
132 scr = EmptyScr}, |
132 scr = Celem.EmptyScr}, |
133 srls = Erls, calc = [], errpatts = [], |
133 srls = Celem.Erls, calc = [], errpatts = [], |
134 rules = [ |
134 rules = [ |
135 Thm ("integral_const", TermC.num_str @{thm integral_const}), |
135 Celem.Thm ("integral_const", TermC.num_str @{thm integral_const}), |
136 Thm ("integral_var", TermC.num_str @{thm integral_var}), |
136 Celem.Thm ("integral_var", TermC.num_str @{thm integral_var}), |
137 Thm ("integral_add", TermC.num_str @{thm integral_add}), |
137 Celem.Thm ("integral_add", TermC.num_str @{thm integral_add}), |
138 Thm ("integral_mult", TermC.num_str @{thm integral_mult}), |
138 Celem.Thm ("integral_mult", TermC.num_str @{thm integral_mult}), |
139 Thm ("integral_pow", TermC.num_str @{thm integral_pow}), |
139 Celem.Thm ("integral_pow", TermC.num_str @{thm integral_pow}), |
140 Calc ("Groups.plus_class.plus", eval_binop "#add_")(*for n+1*) |
140 Celem.Calc ("Groups.plus_class.plus", eval_binop "#add_")(*for n+1*) |
141 ], |
141 ], |
142 scr = EmptyScr}; |
142 scr = Celem.EmptyScr}; |
143 *} |
143 *} |
144 ML {* |
144 ML {* |
145 val add_new_c = |
145 val add_new_c = |
146 Seq {id="add_new_c", preconds = [], |
146 Celem.Seq {id="add_new_c", preconds = [], |
147 rew_ord = ("termlessI",termlessI), |
147 rew_ord = ("termlessI",termlessI), |
148 erls = Rls {id="conditions_in_add_new_c", |
148 erls = Celem.Rls {id="conditions_in_add_new_c", |
149 preconds = [], |
149 preconds = [], |
150 rew_ord = ("termlessI",termlessI), |
150 rew_ord = ("termlessI",termlessI), |
151 erls = Erls, |
151 erls = Celem.Erls, |
152 srls = Erls, calc = [], errpatts = [], |
152 srls = Celem.Erls, calc = [], errpatts = [], |
153 rules = [Calc ("Tools.matches", eval_matches""), |
153 rules = [Celem.Calc ("Tools.matches", eval_matches""), |
154 Calc ("Integrate.is'_f'_x", |
154 Celem.Calc ("Integrate.is'_f'_x", |
155 eval_is_f_x "is_f_x_"), |
155 eval_is_f_x "is_f_x_"), |
156 Thm ("not_true", TermC.num_str @{thm not_true}), |
156 Celem.Thm ("not_true", TermC.num_str @{thm not_true}), |
157 Thm ("not_false", TermC.num_str @{thm not_false}) |
157 Celem.Thm ("not_false", TermC.num_str @{thm not_false}) |
158 ], |
158 ], |
159 scr = EmptyScr}, |
159 scr = Celem.EmptyScr}, |
160 srls = Erls, calc = [], errpatts = [], |
160 srls = Celem.Erls, calc = [], errpatts = [], |
161 rules = [ (*Thm ("call_for_new_c", TermC.num_str @{thm call_for_new_c}),*) |
161 rules = [ (*Celem.Thm ("call_for_new_c", TermC.num_str @{thm call_for_new_c}),*) |
162 Cal1 ("Integrate.add'_new'_c", eval_add_new_c "new_c_") |
162 Celem.Cal1 ("Integrate.add'_new'_c", eval_add_new_c "new_c_") |
163 ], |
163 ], |
164 scr = EmptyScr}; |
164 scr = Celem.EmptyScr}; |
165 *} |
165 *} |
166 ML {* |
166 ML {* |
167 |
167 |
168 (*.rulesets for simplifying Integrals.*) |
168 (*.rulesets for simplifying Integrals.*) |
169 |
169 |
170 (*.for simplify_Integral adapted from 'norm_Rational_rls'.*) |
170 (*.for simplify_Integral adapted from 'norm_Rational_rls'.*) |
171 val norm_Rational_rls_noadd_fractions = |
171 val norm_Rational_rls_noadd_fractions = |
172 Rls {id = "norm_Rational_rls_noadd_fractions", preconds = [], |
172 Celem.Rls {id = "norm_Rational_rls_noadd_fractions", preconds = [], |
173 rew_ord = ("dummy_ord",dummy_ord), |
173 rew_ord = ("dummy_ord",Celem.dummy_ord), |
174 erls = norm_rat_erls, srls = Erls, calc = [], errpatts = [], |
174 erls = norm_rat_erls, srls = Celem.Erls, calc = [], errpatts = [], |
175 rules = [(*Rls_ add_fractions_p_rls,!!!*) |
175 rules = [(*Celem.Rls_ add_fractions_p_rls,!!!*) |
176 Rls_ (*rat_mult_div_pow original corrected WN051028*) |
176 Celem.Rls_ (*rat_mult_div_pow original corrected WN051028*) |
177 (Rls {id = "rat_mult_div_pow", preconds = [], |
177 (Celem.Rls {id = "rat_mult_div_pow", preconds = [], |
178 rew_ord = ("dummy_ord",dummy_ord), |
178 rew_ord = ("dummy_ord",Celem.dummy_ord), |
179 erls = (*FIXME.WN051028 e_rls,*) |
179 erls = (*FIXME.WN051028 Celem.e_rls,*) |
180 append_rls "e_rls-is_polyexp" e_rls |
180 Celem.append_rls "Celem.e_rls-is_polyexp" Celem.e_rls |
181 [Calc ("Poly.is'_polyexp", |
181 [Celem.Calc ("Poly.is'_polyexp", |
182 eval_is_polyexp "")], |
182 eval_is_polyexp "")], |
183 srls = Erls, calc = [], errpatts = [], |
183 srls = Celem.Erls, calc = [], errpatts = [], |
184 rules = [Thm ("rat_mult", TermC.num_str @{thm rat_mult}), |
184 rules = [Celem.Thm ("rat_mult", TermC.num_str @{thm rat_mult}), |
185 (*"?a / ?b * (?c / ?d) = ?a * ?c / (?b * ?d)"*) |
185 (*"?a / ?b * (?c / ?d) = ?a * ?c / (?b * ?d)"*) |
186 Thm ("rat_mult_poly_l", TermC.num_str @{thm rat_mult_poly_l}), |
186 Celem.Thm ("rat_mult_poly_l", TermC.num_str @{thm rat_mult_poly_l}), |
187 (*"?c is_polyexp ==> ?c * (?a / ?b) = ?c * ?a / ?b"*) |
187 (*"?c is_polyexp ==> ?c * (?a / ?b) = ?c * ?a / ?b"*) |
188 Thm ("rat_mult_poly_r", TermC.num_str @{thm rat_mult_poly_r}), |
188 Celem.Thm ("rat_mult_poly_r", TermC.num_str @{thm rat_mult_poly_r}), |
189 (*"?c is_polyexp ==> ?a / ?b * ?c = ?a * ?c / ?b"*) |
189 (*"?c is_polyexp ==> ?a / ?b * ?c = ?a * ?c / ?b"*) |
190 |
190 |
191 Thm ("real_divide_divide1_mg", |
191 Celem.Thm ("real_divide_divide1_mg", |
192 TermC.num_str @{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)"*) |
193 (*"y ~= 0 ==> (u / v) / (y / z) = (u * z) / (y * v)"*) |
194 Thm ("divide_divide_eq_right", |
194 Celem.Thm ("divide_divide_eq_right", |
195 TermC.num_str @{thm divide_divide_eq_right}), |
195 TermC.num_str @{thm divide_divide_eq_right}), |
196 (*"?x / (?y / ?z) = ?x * ?z / ?y"*) |
196 (*"?x / (?y / ?z) = ?x * ?z / ?y"*) |
197 Thm ("divide_divide_eq_left", |
197 Celem.Thm ("divide_divide_eq_left", |
198 TermC.num_str @{thm divide_divide_eq_left}), |
198 TermC.num_str @{thm divide_divide_eq_left}), |
199 (*"?x / ?y / ?z = ?x / (?y * ?z)"*) |
199 (*"?x / ?y / ?z = ?x / (?y * ?z)"*) |
200 Calc ("Rings.divide_class.divide" ,eval_cancel "#divide_e"), |
200 Celem.Calc ("Rings.divide_class.divide" ,eval_cancel "#divide_e"), |
201 |
201 |
202 Thm ("rat_power", TermC.num_str @{thm rat_power}) |
202 Celem.Thm ("rat_power", TermC.num_str @{thm rat_power}) |
203 (*"(?a / ?b) ^^^ ?n = ?a ^^^ ?n / ?b ^^^ ?n"*) |
203 (*"(?a / ?b) ^^^ ?n = ?a ^^^ ?n / ?b ^^^ ?n"*) |
204 ], |
204 ], |
205 scr = Prog ((Thm.term_of o the o (TermC.parse thy)) "empty_script") |
205 scr = Celem.Prog ((Thm.term_of o the o (TermC.parse thy)) "empty_script") |
206 }), |
206 }), |
207 Rls_ make_rat_poly_with_parentheses, |
207 Celem.Rls_ make_rat_poly_with_parentheses, |
208 Rls_ cancel_p_rls,(*FIXME:cancel_p does NOT order sometimes*) |
208 Celem.Rls_ cancel_p_rls,(*FIXME:cancel_p does NOT order sometimes*) |
209 Rls_ rat_reduce_1 |
209 Celem.Rls_ rat_reduce_1 |
210 ], |
210 ], |
211 scr = Prog ((Thm.term_of o the o (TermC.parse thy)) "empty_script") |
211 scr = Celem.Prog ((Thm.term_of o the o (TermC.parse thy)) "empty_script") |
212 }:rls; |
212 }; |
213 |
213 |
214 (*.for simplify_Integral adapted from 'norm_Rational'.*) |
214 (*.for simplify_Integral adapted from 'norm_Rational'.*) |
215 val norm_Rational_noadd_fractions = |
215 val norm_Rational_noadd_fractions = |
216 Seq {id = "norm_Rational_noadd_fractions", preconds = [], |
216 Celem.Seq {id = "norm_Rational_noadd_fractions", preconds = [], |
217 rew_ord = ("dummy_ord",dummy_ord), |
217 rew_ord = ("dummy_ord",Celem.dummy_ord), |
218 erls = norm_rat_erls, srls = Erls, calc = [], errpatts = [], |
218 erls = norm_rat_erls, srls = Celem.Erls, calc = [], errpatts = [], |
219 rules = [Rls_ discard_minus, |
219 rules = [Celem.Rls_ discard_minus, |
220 Rls_ rat_mult_poly,(* removes double fractions like a/b/c *) |
220 Celem.Rls_ rat_mult_poly,(* removes double fractions like a/b/c *) |
221 Rls_ make_rat_poly_with_parentheses, (*WN0510 also in(#)below*) |
221 Celem.Rls_ make_rat_poly_with_parentheses, (*WN0510 also in(#)below*) |
222 Rls_ cancel_p_rls, (*FIXME.MG:cancel_p does NOT order sometim*) |
222 Celem.Rls_ cancel_p_rls, (*FIXME.MG:cancel_p does NOT order sometim*) |
223 Rls_ norm_Rational_rls_noadd_fractions,(* the main rls (#) *) |
223 Celem.Rls_ norm_Rational_rls_noadd_fractions,(* the main rls (#) *) |
224 Rls_ discard_parentheses1 (* mult only *) |
224 Celem.Rls_ discard_parentheses1 (* mult only *) |
225 ], |
225 ], |
226 scr = Prog ((Thm.term_of o the o (TermC.parse thy)) "empty_script") |
226 scr = Celem.Prog ((Thm.term_of o the o (TermC.parse thy)) "empty_script") |
227 }:rls; |
227 }; |
228 |
228 |
229 (*.simplify terms before and after Integration such that |
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 |
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. |
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 |
232 This is a copy from 'make_ratpoly_in' with respective reduction of rules and |
233 *1* expand the term, ie. distribute * and / over + |
233 *1* expand the term, ie. distribute * and / over + |
234 .*) |
234 .*) |
235 val separate_bdv2 = |
235 val separate_bdv2 = |
236 append_rls "separate_bdv2" |
236 Celem.append_rls "separate_bdv2" |
237 collect_bdv |
237 collect_bdv |
238 [Thm ("separate_bdv", TermC.num_str @{thm separate_bdv}), |
238 [Celem.Thm ("separate_bdv", TermC.num_str @{thm separate_bdv}), |
239 (*"?a * ?bdv / ?b = ?a / ?b * ?bdv"*) |
239 (*"?a * ?bdv / ?b = ?a / ?b * ?bdv"*) |
240 Thm ("separate_bdv_n", TermC.num_str @{thm separate_bdv_n}), |
240 Celem.Thm ("separate_bdv_n", TermC.num_str @{thm separate_bdv_n}), |
241 Thm ("separate_1_bdv", TermC.num_str @{thm separate_1_bdv}), |
241 Celem.Thm ("separate_1_bdv", TermC.num_str @{thm separate_1_bdv}), |
242 (*"?bdv / ?b = (1 / ?b) * ?bdv"*) |
242 (*"?bdv / ?b = (1 / ?b) * ?bdv"*) |
243 Thm ("separate_1_bdv_n", TermC.num_str @{thm separate_1_bdv_n})(*, |
243 Celem.Thm ("separate_1_bdv_n", TermC.num_str @{thm separate_1_bdv_n})(*, |
244 (*"?bdv ^^^ ?n / ?b = 1 / ?b * ?bdv ^^^ ?n"*) |
244 (*"?bdv ^^^ ?n / ?b = 1 / ?b * ?bdv ^^^ ?n"*) |
245 *****Thm ("add_divide_distrib", |
245 *****Celem.Thm ("add_divide_distrib", |
246 ***** TermC.num_str @{thm add_divide_distrib}) |
246 ***** TermC.num_str @{thm add_divide_distrib}) |
247 (*"(?x + ?y) / ?z = ?x / ?z + ?y / ?z"*)----------*) |
247 (*"(?x + ?y) / ?z = ?x / ?z + ?y / ?z"*)----------*) |
248 ]; |
248 ]; |
249 val simplify_Integral = |
249 val simplify_Integral = |
250 Seq {id = "simplify_Integral", preconds = []:term list, |
250 Celem.Seq {id = "simplify_Integral", preconds = []:term list, |
251 rew_ord = ("dummy_ord", dummy_ord), |
251 rew_ord = ("dummy_ord", Celem.dummy_ord), |
252 erls = Atools_erls, srls = Erls, |
252 erls = Atools_erls, srls = Celem.Erls, |
253 calc = [], errpatts = [], |
253 calc = [], errpatts = [], |
254 rules = [Thm ("distrib_right", TermC.num_str @{thm distrib_right}), |
254 rules = [Celem.Thm ("distrib_right", TermC.num_str @{thm distrib_right}), |
255 (*"(?z1.0 + ?z2.0) * ?w = ?z1.0 * ?w + ?z2.0 * ?w"*) |
255 (*"(?z1.0 + ?z2.0) * ?w = ?z1.0 * ?w + ?z2.0 * ?w"*) |
256 Thm ("add_divide_distrib", TermC.num_str @{thm add_divide_distrib}), |
256 Celem.Thm ("add_divide_distrib", TermC.num_str @{thm add_divide_distrib}), |
257 (*"(?x + ?y) / ?z = ?x / ?z + ?y / ?z"*) |
257 (*"(?x + ?y) / ?z = ?x / ?z + ?y / ?z"*) |
258 (*^^^^^ *1* ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^*) |
258 (*^^^^^ *1* ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^*) |
259 Rls_ norm_Rational_noadd_fractions, |
259 Celem.Rls_ norm_Rational_noadd_fractions, |
260 Rls_ order_add_mult_in, |
260 Celem.Rls_ order_add_mult_in, |
261 Rls_ discard_parentheses, |
261 Celem.Rls_ discard_parentheses, |
262 (*Rls_ collect_bdv, from make_polynomial_in*) |
262 (*Celem.Rls_ collect_bdv, from make_polynomial_in*) |
263 Rls_ separate_bdv2, |
263 Celem.Rls_ separate_bdv2, |
264 Calc ("Rings.divide_class.divide" ,eval_cancel "#divide_e") |
264 Celem.Calc ("Rings.divide_class.divide" ,eval_cancel "#divide_e") |
265 ], |
265 ], |
266 scr = EmptyScr}:rls; |
266 scr = Celem.EmptyScr}; |
267 |
267 |
268 |
268 |
269 (*simplify terms before and after Integration such that |
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 |
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. |
271 common denominator as done by norm_Rational or make_ratpoly_in. |
272 This is a copy from 'make_polynomial_in' with insertions from |
272 This is a copy from 'make_polynomial_in' with insertions from |
273 'make_ratpoly_in' |
273 'make_ratpoly_in' |
274 THIS IS KEPT FOR COMPARISON ............................................ |
274 THIS IS KEPT FOR COMPARISON ............................................ |
275 * val simplify_Integral = prep_rls'( |
275 * val simplify_Integral = prep_rls'( |
276 * Seq {id = "", preconds = []:term list, |
276 * Celem.Seq {id = "", preconds = []:term list, |
277 * rew_ord = ("dummy_ord", dummy_ord), |
277 * rew_ord = ("dummy_ord", Celem.dummy_ord), |
278 * erls = Atools_erls, srls = Erls, |
278 * erls = Atools_erls, srls = Celem.Erls, |
279 * calc = [], (*asm_thm = [],*) |
279 * calc = [], (*asm_thm = [],*) |
280 * rules = [Rls_ expand_poly, |
280 * rules = [Celem.Rls_ expand_poly, |
281 * Rls_ order_add_mult_in, |
281 * Celem.Rls_ order_add_mult_in, |
282 * Rls_ simplify_power, |
282 * Celem.Rls_ simplify_power, |
283 * Rls_ collect_numerals, |
283 * Celem.Rls_ collect_numerals, |
284 * Rls_ reduce_012, |
284 * Celem.Rls_ reduce_012, |
285 * Thm ("realpow_oneI", TermC.num_str @{thm realpow_oneI}), |
285 * Celem.Thm ("realpow_oneI", TermC.num_str @{thm realpow_oneI}), |
286 * Rls_ discard_parentheses, |
286 * Celem.Rls_ discard_parentheses, |
287 * Rls_ collect_bdv, |
287 * Celem.Rls_ collect_bdv, |
288 * (*below inserted from 'make_ratpoly_in'*) |
288 * (*below inserted from 'make_ratpoly_in'*) |
289 * Rls_ (append_rls "separate_bdv" |
289 * Celem.Rls_ (Celem.append_rls "separate_bdv" |
290 * collect_bdv |
290 * collect_bdv |
291 * [Thm ("separate_bdv", TermC.num_str @{thm separate_bdv}), |
291 * [Celem.Thm ("separate_bdv", TermC.num_str @{thm separate_bdv}), |
292 * (*"?a * ?bdv / ?b = ?a / ?b * ?bdv"*) |
292 * (*"?a * ?bdv / ?b = ?a / ?b * ?bdv"*) |
293 * Thm ("separate_bdv_n", TermC.num_str @{thm separate_bdv_n}), |
293 * Celem.Thm ("separate_bdv_n", TermC.num_str @{thm separate_bdv_n}), |
294 * Thm ("separate_1_bdv", TermC.num_str @{thm separate_1_bdv}), |
294 * Celem.Thm ("separate_1_bdv", TermC.num_str @{thm separate_1_bdv}), |
295 * (*"?bdv / ?b = (1 / ?b) * ?bdv"*) |
295 * (*"?bdv / ?b = (1 / ?b) * ?bdv"*) |
296 * Thm ("separate_1_bdv_n", TermC.num_str @{thm separate_1_bdv_n})(*, |
296 * Celem.Thm ("separate_1_bdv_n", TermC.num_str @{thm separate_1_bdv_n})(*, |
297 * (*"?bdv ^^^ ?n / ?b = 1 / ?b * ?bdv ^^^ ?n"*) |
297 * (*"?bdv ^^^ ?n / ?b = 1 / ?b * ?bdv ^^^ ?n"*) |
298 * Thm ("add_divide_distrib", |
298 * Celem.Thm ("add_divide_distrib", |
299 * TermC.num_str @{thm add_divide_distrib}) |
299 * TermC.num_str @{thm add_divide_distrib}) |
300 * (*"(?x + ?y) / ?z = ?x / ?z + ?y / ?z"*)*) |
300 * (*"(?x + ?y) / ?z = ?x / ?z + ?y / ?z"*)*) |
301 * ]), |
301 * ]), |
302 * Calc ("Rings.divide_class.divide" ,eval_cancel "#divide_e") |
302 * Celem.Calc ("Rings.divide_class.divide" ,eval_cancel "#divide_e") |
303 * ], |
303 * ], |
304 * scr = EmptyScr |
304 * scr = Celem.EmptyScr |
305 * }:rls); |
305 * }); |
306 .......................................................................*) |
306 .......................................................................*) |
307 |
307 |
308 val integration = |
308 val integration = |
309 Seq {id="integration", preconds = [], |
309 Celem.Seq {id="integration", preconds = [], |
310 rew_ord = ("termlessI",termlessI), |
310 rew_ord = ("termlessI",termlessI), |
311 erls = Rls {id="conditions_in_integration", |
311 erls = Celem.Rls {id="conditions_in_integration", |
312 preconds = [], |
312 preconds = [], |
313 rew_ord = ("termlessI",termlessI), |
313 rew_ord = ("termlessI",termlessI), |
314 erls = Erls, |
314 erls = Celem.Erls, |
315 srls = Erls, calc = [], errpatts = [], |
315 srls = Celem.Erls, calc = [], errpatts = [], |
316 rules = [], |
316 rules = [], |
317 scr = EmptyScr}, |
317 scr = Celem.EmptyScr}, |
318 srls = Erls, calc = [], errpatts = [], |
318 srls = Celem.Erls, calc = [], errpatts = [], |
319 rules = [ Rls_ integration_rules, |
319 rules = [ Celem.Rls_ integration_rules, |
320 Rls_ add_new_c, |
320 Celem.Rls_ add_new_c, |
321 Rls_ simplify_Integral |
321 Celem.Rls_ simplify_Integral |
322 ], |
322 ], |
323 scr = EmptyScr}; |
323 scr = Celem.EmptyScr}; |
324 |
324 |
325 val prep_rls' = LTool.prep_rls @{theory}; |
325 val prep_rls' = LTool.prep_rls @{theory}; |
326 *} |
326 *} |
327 setup {* KEStore_Elems.add_rlss |
327 setup {* KEStore_Elems.add_rlss |
328 [("integration_rules", (Context.theory_name @{theory}, prep_rls' integration_rules)), |
328 [("integration_rules", (Context.theory_name @{theory}, prep_rls' integration_rules)), |
336 ("norm_Rational_rls_noadd_fractions", (Context.theory_name @{theory}, |
336 ("norm_Rational_rls_noadd_fractions", (Context.theory_name @{theory}, |
337 prep_rls' norm_Rational_rls_noadd_fractions))] *} |
337 prep_rls' norm_Rational_rls_noadd_fractions))] *} |
338 |
338 |
339 (** problems **) |
339 (** problems **) |
340 setup {* KEStore_Elems.add_pbts |
340 setup {* KEStore_Elems.add_pbts |
341 [(Specify.prep_pbt thy "pbl_fun_integ" [] e_pblID |
341 [(Specify.prep_pbt thy "pbl_fun_integ" [] Celem.e_pblID |
342 (["integrate","function"], |
342 (["integrate","function"], |
343 [("#Given" ,["functionTerm f_f", "integrateBy v_v"]), |
343 [("#Given" ,["functionTerm f_f", "integrateBy v_v"]), |
344 ("#Find" ,["antiDerivative F_F"])], |
344 ("#Find" ,["antiDerivative F_F"])], |
345 append_rls "e_rls" e_rls [(*for preds in where_*)], |
345 Celem.append_rls "xxxe_rlsxxx" Celem.e_rls [(*for preds in where_*)], |
346 SOME "Integrate (f_f, v_v)", |
346 SOME "Integrate (f_f, v_v)", |
347 [["diff","integration"]])), |
347 [["diff","integration"]])), |
348 (*here "named" is used differently from Differentiation"*) |
348 (*here "named" is used differently from Differentiation"*) |
349 (Specify.prep_pbt thy "pbl_fun_integ_nam" [] e_pblID |
349 (Specify.prep_pbt thy "pbl_fun_integ_nam" [] Celem.e_pblID |
350 (["named","integrate","function"], |
350 (["named","integrate","function"], |
351 [("#Given" ,["functionTerm f_f", "integrateBy v_v"]), |
351 [("#Given" ,["functionTerm f_f", "integrateBy v_v"]), |
352 ("#Find" ,["antiDerivativeName F_F"])], |
352 ("#Find" ,["antiDerivativeName F_F"])], |
353 append_rls "e_rls" e_rls [(*for preds in where_*)], |
353 Celem.append_rls "xxxe_rlsxxx" Celem.e_rls [(*for preds in where_*)], |
354 SOME "Integrate (f_f, v_v)", |
354 SOME "Integrate (f_f, v_v)", |
355 [["diff","integration","named"]]))] *} |
355 [["diff","integration","named"]]))] *} |
356 |
356 |
357 (** methods **) |
357 (** methods **) |
358 setup {* KEStore_Elems.add_mets |
358 setup {* KEStore_Elems.add_mets |
359 [Specify.prep_met thy "met_diffint" [] e_metID |
359 [Specify.prep_met thy "met_diffint" [] Celem.e_metID |
360 (["diff","integration"], |
360 (["diff","integration"], |
361 [("#Given" ,["functionTerm f_f", "integrateBy v_v"]), ("#Find" ,["antiDerivative F_F"])], |
361 [("#Given" ,["functionTerm f_f", "integrateBy v_v"]), ("#Find" ,["antiDerivative F_F"])], |
362 {rew_ord'="tless_true", rls'=Atools_erls, calc = [], srls = e_rls, prls=e_rls, |
362 {rew_ord'="tless_true", rls'=Atools_erls, calc = [], srls = Celem.e_rls, prls=Celem.e_rls, |
363 crls = Atools_erls, errpats = [], nrls = e_rls}, |
363 crls = Atools_erls, errpats = [], nrls = Celem.e_rls}, |
364 "Script IntegrationScript (f_f::real) (v_v::real) = " ^ |
364 "Script IntegrationScript (f_f::real) (v_v::real) = " ^ |
365 " (let t_t = Take (Integral f_f D v_v) " ^ |
365 " (let t_t = Take (Integral f_f D v_v) " ^ |
366 " in (Rewrite_Set_Inst [(bdv,v_v)] integration False) (t_t::real))"), |
366 " in (Rewrite_Set_Inst [(bdv,v_v)] integration False) (t_t::real))"), |
367 Specify.prep_met thy "met_diffint_named" [] e_metID |
367 Specify.prep_met thy "met_diffint_named" [] Celem.e_metID |
368 (["diff","integration","named"], |
368 (["diff","integration","named"], |
369 [("#Given" ,["functionTerm f_f", "integrateBy v_v"]), |
369 [("#Given" ,["functionTerm f_f", "integrateBy v_v"]), |
370 ("#Find" ,["antiDerivativeName F_F"])], |
370 ("#Find" ,["antiDerivativeName F_F"])], |
371 {rew_ord'="tless_true", rls'=Atools_erls, calc = [], srls = e_rls, prls=e_rls, |
371 {rew_ord'="tless_true", rls'=Atools_erls, calc = [], srls = Celem.e_rls, prls=Celem.e_rls, |
372 crls = Atools_erls, errpats = [], nrls = e_rls}, |
372 crls = Atools_erls, errpats = [], nrls = Celem.e_rls}, |
373 "Script NamedIntegrationScript (f_f::real) (v_v::real) (F_F::real=>real) = " ^ |
373 "Script NamedIntegrationScript (f_f::real) (v_v::real) (F_F::real=>real) = " ^ |
374 " (let t_t = Take (F_F v_v = Integral f_f D v_v) " ^ |
374 " (let t_t = Take (F_F v_v = Integral f_f D v_v) " ^ |
375 " in ((Try (Rewrite_Set_Inst [(bdv,v_v)] simplify_Integral False)) @@ " ^ |
375 " in ((Try (Rewrite_Set_Inst [(bdv,v_v)] simplify_Integral False)) @@ " ^ |
376 " (Rewrite_Set_Inst [(bdv,v_v)] integration False)) t_t) ")] |
376 " (Rewrite_Set_Inst [(bdv,v_v)] integration False)) t_t) ")] |
377 *} |
377 *} |