15 (*descriptions in the related problems*) |
15 (*descriptions in the related problems*) |
16 integrateBy :: "real => una" |
16 integrateBy :: "real => una" |
17 antiDerivative :: "real => una" |
17 antiDerivative :: "real => una" |
18 antiDerivativeName :: "(real => real) => una" |
18 antiDerivativeName :: "(real => real) => una" |
19 |
19 |
20 (*the CAS-command, eg. "Integrate (2*x^^^3, x)"*) |
20 (*the CAS-command, eg. "Integrate (2*x \<up> 3, x)"*) |
21 Integrate :: "[real * real] => real" |
21 Integrate :: "[real * real] => real" |
22 |
22 |
23 axiomatization where |
23 axiomatization where |
24 (*stated as axioms, todo: prove as theorems |
24 (*stated as axioms, todo: prove as theorems |
25 'bdv' is a constant handled on the meta-level |
25 'bdv' is a constant handled on the meta-level |
191 ThmC.numerals_to_Free @{thm divide_divide_eq_left}), |
191 ThmC.numerals_to_Free @{thm divide_divide_eq_left}), |
192 (*"?x / ?y / ?z = ?x / (?y * ?z)"*) |
192 (*"?x / ?y / ?z = ?x / (?y * ?z)"*) |
193 Rule.Eval ("Rings.divide_class.divide", Prog_Expr.eval_cancel "#divide_e"), |
193 Rule.Eval ("Rings.divide_class.divide", Prog_Expr.eval_cancel "#divide_e"), |
194 |
194 |
195 Rule.Thm ("rat_power", ThmC.numerals_to_Free @{thm rat_power}) |
195 Rule.Thm ("rat_power", ThmC.numerals_to_Free @{thm rat_power}) |
196 (*"(?a / ?b) ^^^ ?n = ?a ^^^ ?n / ?b ^^^ ?n"*) |
196 (*"(?a / ?b) \<up> ?n = ?a \<up> ?n / ?b \<up> ?n"*) |
197 ], |
197 ], |
198 scr = Rule.Empty_Prog |
198 scr = Rule.Empty_Prog |
199 }), |
199 }), |
200 Rule.Rls_ make_rat_poly_with_parentheses, |
200 Rule.Rls_ make_rat_poly_with_parentheses, |
201 Rule.Rls_ cancel_p_rls,(*FIXME:cancel_p does NOT order sometimes*) |
201 Rule.Rls_ cancel_p_rls,(*FIXME:cancel_p does NOT order sometimes*) |
232 (*"?a * ?bdv / ?b = ?a / ?b * ?bdv"*) |
232 (*"?a * ?bdv / ?b = ?a / ?b * ?bdv"*) |
233 Rule.Thm ("separate_bdv_n", ThmC.numerals_to_Free @{thm separate_bdv_n}), |
233 Rule.Thm ("separate_bdv_n", ThmC.numerals_to_Free @{thm separate_bdv_n}), |
234 Rule.Thm ("separate_1_bdv", ThmC.numerals_to_Free @{thm separate_1_bdv}), |
234 Rule.Thm ("separate_1_bdv", ThmC.numerals_to_Free @{thm separate_1_bdv}), |
235 (*"?bdv / ?b = (1 / ?b) * ?bdv"*) |
235 (*"?bdv / ?b = (1 / ?b) * ?bdv"*) |
236 Rule.Thm ("separate_1_bdv_n", ThmC.numerals_to_Free @{thm separate_1_bdv_n})(*, |
236 Rule.Thm ("separate_1_bdv_n", ThmC.numerals_to_Free @{thm separate_1_bdv_n})(*, |
237 (*"?bdv ^^^ ?n / ?b = 1 / ?b * ?bdv ^^^ ?n"*) |
237 (*"?bdv \<up> ?n / ?b = 1 / ?b * ?bdv \<up> ?n"*) |
238 *****Rule.Thm ("add_divide_distrib", |
238 *****Rule.Thm ("add_divide_distrib", |
239 ***** ThmC.numerals_to_Free @{thm add_divide_distrib}) |
239 ***** ThmC.numerals_to_Free @{thm add_divide_distrib}) |
240 (*"(?x + ?y) / ?z = ?x / ?z + ?y / ?z"*)----------*) |
240 (*"(?x + ?y) / ?z = ?x / ?z + ?y / ?z"*)----------*) |
241 ]; |
241 ]; |
242 val simplify_Integral = |
242 val simplify_Integral = |
285 * (*"?a * ?bdv / ?b = ?a / ?b * ?bdv"*) |
285 * (*"?a * ?bdv / ?b = ?a / ?b * ?bdv"*) |
286 * Rule.Thm ("separate_bdv_n", ThmC.numerals_to_Free @{thm separate_bdv_n}), |
286 * Rule.Thm ("separate_bdv_n", ThmC.numerals_to_Free @{thm separate_bdv_n}), |
287 * Rule.Thm ("separate_1_bdv", ThmC.numerals_to_Free @{thm separate_1_bdv}), |
287 * Rule.Thm ("separate_1_bdv", ThmC.numerals_to_Free @{thm separate_1_bdv}), |
288 * (*"?bdv / ?b = (1 / ?b) * ?bdv"*) |
288 * (*"?bdv / ?b = (1 / ?b) * ?bdv"*) |
289 * Rule.Thm ("separate_1_bdv_n", ThmC.numerals_to_Free @{thm separate_1_bdv_n})(*, |
289 * Rule.Thm ("separate_1_bdv_n", ThmC.numerals_to_Free @{thm separate_1_bdv_n})(*, |
290 * (*"?bdv ^^^ ?n / ?b = 1 / ?b * ?bdv ^^^ ?n"*) |
290 * (*"?bdv \<up> ?n / ?b = 1 / ?b * ?bdv \<up> ?n"*) |
291 * Rule.Thm ("add_divide_distrib", |
291 * Rule.Thm ("add_divide_distrib", |
292 * ThmC.numerals_to_Free @{thm add_divide_distrib}) |
292 * ThmC.numerals_to_Free @{thm add_divide_distrib}) |
293 * (*"(?x + ?y) / ?z = ?x / ?z + ?y / ?z"*)*) |
293 * (*"(?x + ?y) / ?z = ?x / ?z + ?y / ?z"*)*) |
294 * ]), |
294 * ]), |
295 * Rule.Eval ("Rings.divide_class.divide" , eval_cancel "#divide_e") |
295 * Rule.Eval ("Rings.divide_class.divide" , eval_cancel "#divide_e") |