neuper@37906
|
1 |
(* integration over the reals
|
neuper@37906
|
2 |
author: Walther Neuper
|
neuper@37906
|
3 |
050814, 08:51
|
neuper@37906
|
4 |
(c) due to copyright terms
|
neuper@37906
|
5 |
*)
|
neuper@37906
|
6 |
|
neuper@37954
|
7 |
theory Integrate imports Diff begin
|
neuper@37906
|
8 |
|
neuper@37906
|
9 |
consts
|
neuper@37906
|
10 |
|
neuper@37906
|
11 |
Integral :: "[real, real]=> real" ("Integral _ D _" 91)
|
walther@60368
|
12 |
add_new_c :: "real => real" ("add'_new'_c _" 66)
|
walther@60278
|
13 |
is_f_x :: "real => bool" ("_ is'_f'_x" 10)
|
neuper@37906
|
14 |
|
neuper@37906
|
15 |
(*descriptions in the related problems*)
|
neuper@37996
|
16 |
integrateBy :: "real => una"
|
neuper@37996
|
17 |
antiDerivative :: "real => una"
|
neuper@37996
|
18 |
antiDerivativeName :: "(real => real) => una"
|
neuper@37906
|
19 |
|
walther@60260
|
20 |
(*the CAS-command, eg. "Integrate (2*x \<up> 3, x)"*)
|
neuper@37906
|
21 |
Integrate :: "[real * real] => real"
|
neuper@37906
|
22 |
|
neuper@52148
|
23 |
axiomatization where
|
neuper@37906
|
24 |
(*stated as axioms, todo: prove as theorems
|
neuper@37906
|
25 |
'bdv' is a constant handled on the meta-level
|
neuper@37906
|
26 |
specifically as a 'bound variable' *)
|
neuper@37906
|
27 |
|
walther@60269
|
28 |
(*Ambiguous input\<^here> produces 3 parse trees -----------------------------\\*)
|
neuper@52148
|
29 |
integral_const: "Not (bdv occurs_in u) ==> Integral u D bdv = u * bdv" and
|
walther@60242
|
30 |
integral_var: "Integral bdv D bdv = bdv \<up> 2 / 2" and
|
neuper@37906
|
31 |
|
neuper@37983
|
32 |
integral_add: "Integral (u + v) D bdv =
|
neuper@52148
|
33 |
(Integral u D bdv) + (Integral v D bdv)" and
|
neuper@37983
|
34 |
integral_mult: "[| Not (bdv occurs_in u); bdv occurs_in v |] ==>
|
neuper@52148
|
35 |
Integral (u * v) D bdv = u * (Integral v D bdv)" and
|
neuper@37906
|
36 |
(*WN080222: this goes into sub-terms, too ...
|
neuper@37983
|
37 |
call_for_new_c: "[| Not (matches (u + new_c v) a); Not (a is_f_x) |] ==>
|
neuper@37954
|
38 |
a = a + new_c a"
|
neuper@37906
|
39 |
*)
|
walther@60242
|
40 |
integral_pow: "Integral bdv \<up> n D bdv = bdv \<up> (n+1) / (n + 1)"
|
walther@60269
|
41 |
(*Ambiguous input\<^here> produces 3 parse trees -----------------------------//*)
|
neuper@37906
|
42 |
|
wneuper@59472
|
43 |
ML \<open>
|
neuper@37954
|
44 |
(** eval functions **)
|
neuper@37954
|
45 |
|
neuper@37954
|
46 |
val c = Free ("c", HOLogic.realT);
|
walther@60358
|
47 |
(*.create a new unique variable 'c..' in a term; for use by \<^rule_eval> in a rls;
|
neuper@37954
|
48 |
an alternative to do this would be '(Try (Calculate new_c_) (new_c es__))'
|
neuper@37954
|
49 |
in the script; this will be possible if currying doesnt take the value
|
neuper@37954
|
50 |
from a variable, but the value '(new_c es__)' itself.*)
|
neuper@37954
|
51 |
fun new_c term =
|
neuper@37954
|
52 |
let fun selc var =
|
neuper@40836
|
53 |
case (Symbol.explode o id_of) var of
|
neuper@37954
|
54 |
"c"::[] => true
|
walther@59875
|
55 |
| "c"::"_"::is => (case (TermC.int_opt_of_string o implode) is of
|
neuper@37954
|
56 |
SOME _ => true
|
neuper@37954
|
57 |
| NONE => false)
|
neuper@37954
|
58 |
| _ => false;
|
neuper@40836
|
59 |
fun get_coeff c = case (Symbol.explode o id_of) c of
|
walther@59875
|
60 |
"c"::"_"::is => (the o TermC.int_opt_of_string o implode) is
|
neuper@37954
|
61 |
| _ => 0;
|
wneuper@59389
|
62 |
val cs = filter selc (TermC.vars term);
|
neuper@37954
|
63 |
in
|
neuper@37954
|
64 |
case cs of
|
neuper@37954
|
65 |
[] => c
|
walther@60269
|
66 |
| [_] => Free ("c_2", HOLogic.realT)
|
neuper@37954
|
67 |
| cs =>
|
neuper@37954
|
68 |
let val max_coeff = maxl (map get_coeff cs)
|
neuper@37954
|
69 |
in Free ("c_"^string_of_int (max_coeff + 1), HOLogic.realT) end
|
neuper@37954
|
70 |
end;
|
neuper@37954
|
71 |
|
neuper@37954
|
72 |
(*WN080222
|
walther@60278
|
73 |
(*("new_c", ("Integrate.new_c", eval_new_c "#new_c_"))*)
|
walther@60335
|
74 |
fun eval_new_c _ _ (p as (Const (\<^const_name>\<open>Integrate.new_c\<close>,_) $ t)) _ =
|
walther@59868
|
75 |
SOME ((UnparseC.term p) ^ " = " ^ UnparseC.term (new_c p),
|
neuper@37954
|
76 |
Trueprop $ (mk_equality (p, new_c p)))
|
neuper@37954
|
77 |
| eval_new_c _ _ _ _ = NONE;
|
neuper@37954
|
78 |
*)
|
neuper@37954
|
79 |
|
neuper@37954
|
80 |
(*WN080222:*)
|
walther@60278
|
81 |
(*("add_new_c", ("Integrate.add_new_c", eval_add_new_c "#add_new_c_"))
|
neuper@37954
|
82 |
add a new c to a term or a fun-equation;
|
neuper@37954
|
83 |
this is _not in_ the term, because only applied to _whole_ term*)
|
Walther@60504
|
84 |
fun eval_add_new_c (_:string) "Integrate.add_new_c" p (_:Proof.context) =
|
neuper@37954
|
85 |
let val p' = case p of
|
wenzelm@60309
|
86 |
Const (\<^const_name>\<open>HOL.eq\<close>, T) $ lh $ rh =>
|
wenzelm@60309
|
87 |
Const (\<^const_name>\<open>HOL.eq\<close>, T) $ lh $ TermC.mk_add rh (new_c rh)
|
wneuper@59389
|
88 |
| p => TermC.mk_add p (new_c p)
|
walther@59868
|
89 |
in SOME ((UnparseC.term p) ^ " = " ^ UnparseC.term p',
|
wneuper@59390
|
90 |
HOLogic.Trueprop $ (TermC.mk_equality (p, p')))
|
neuper@37954
|
91 |
end
|
neuper@37954
|
92 |
| eval_add_new_c _ _ _ _ = NONE;
|
neuper@37954
|
93 |
|
neuper@37954
|
94 |
|
walther@60278
|
95 |
(*("is_f_x", ("Integrate.is_f_x", eval_is_f_x "is_f_x_"))*)
|
walther@60335
|
96 |
fun eval_is_f_x _ _(p as (Const (\<^const_name>\<open>Integrate.is_f_x\<close>, _)
|
neuper@37954
|
97 |
$ arg)) _ =
|
wneuper@59389
|
98 |
if TermC.is_f_x arg
|
walther@59868
|
99 |
then SOME ((UnparseC.term p) ^ " = True",
|
wneuper@59390
|
100 |
HOLogic.Trueprop $ (TermC.mk_equality (p, @{term True})))
|
walther@59868
|
101 |
else SOME ((UnparseC.term p) ^ " = False",
|
wneuper@59390
|
102 |
HOLogic.Trueprop $ (TermC.mk_equality (p, @{term False})))
|
neuper@37954
|
103 |
| eval_is_f_x _ _ _ _ = NONE;
|
wneuper@59472
|
104 |
\<close>
|
walther@60368
|
105 |
|
walther@60368
|
106 |
calculation add_new_c = \<open>eval_add_new_c "add_new_c_"\<close>
|
wenzelm@60313
|
107 |
calculation is_f_x = \<open>eval_is_f_x "is_f_idextifier_"\<close>
|
wenzelm@60313
|
108 |
|
wneuper@59472
|
109 |
ML \<open>
|
neuper@37954
|
110 |
(** rulesets **)
|
neuper@37954
|
111 |
|
neuper@37954
|
112 |
(*.rulesets for integration.*)
|
neuper@37954
|
113 |
val integration_rules =
|
walther@60358
|
114 |
Rule_Def.Repeat {id="integration_rules", preconds = [],
|
walther@60358
|
115 |
rew_ord = ("termlessI",termlessI),
|
walther@60358
|
116 |
erls = Rule_Def.Repeat {id="conditions_in_integration_rules",
|
walther@60358
|
117 |
preconds = [],
|
walther@60358
|
118 |
rew_ord = ("termlessI",termlessI),
|
walther@60358
|
119 |
erls = Rule_Set.Empty,
|
walther@60358
|
120 |
srls = Rule_Set.Empty, calc = [], errpatts = [],
|
walther@60358
|
121 |
rules = [(*for rewriting conditions in Thm's*)
|
walther@60358
|
122 |
\<^rule_eval>\<open>Prog_Expr.occurs_in\<close> (Prog_Expr.eval_occurs_in "#occurs_in_"),
|
walther@60358
|
123 |
\<^rule_thm>\<open>not_true\<close>,
|
walther@60358
|
124 |
\<^rule_thm>\<open>not_false\<close>],
|
walther@60358
|
125 |
scr = Rule.Empty_Prog},
|
walther@60358
|
126 |
srls = Rule_Set.Empty, calc = [], errpatts = [],
|
walther@60358
|
127 |
rules = [
|
walther@60358
|
128 |
\<^rule_thm>\<open>integral_const\<close>,
|
walther@60358
|
129 |
\<^rule_thm>\<open>integral_var\<close>,
|
walther@60358
|
130 |
\<^rule_thm>\<open>integral_add\<close>,
|
walther@60358
|
131 |
\<^rule_thm>\<open>integral_mult\<close>,
|
walther@60358
|
132 |
\<^rule_thm>\<open>integral_pow\<close>,
|
walther@60358
|
133 |
\<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_")(*for n+1*)],
|
walther@60358
|
134 |
scr = Rule.Empty_Prog};
|
wneuper@59472
|
135 |
\<close>
|
wneuper@59472
|
136 |
ML \<open>
|
neuper@37954
|
137 |
val add_new_c =
|
walther@60358
|
138 |
Rule_Set.Sequence {id="add_new_c", preconds = [],
|
walther@60358
|
139 |
rew_ord = ("termlessI",termlessI),
|
walther@60358
|
140 |
erls = Rule_Def.Repeat {id="conditions_in_add_new_c",
|
walther@60358
|
141 |
preconds = [], rew_ord = ("termlessI",termlessI), erls = Rule_Set.Empty,
|
walther@60358
|
142 |
srls = Rule_Set.Empty, calc = [], errpatts = [],
|
walther@60358
|
143 |
rules = [
|
walther@60358
|
144 |
\<^rule_eval>\<open>Prog_Expr.matches\<close> (Prog_Expr.eval_matches""),
|
walther@60358
|
145 |
\<^rule_eval>\<open>Integrate.is_f_x\<close> (eval_is_f_x "is_f_x_"),
|
walther@60358
|
146 |
\<^rule_thm>\<open>not_true\<close>,
|
walther@60358
|
147 |
\<^rule_thm>\<open>not_false\<close>],
|
walther@60358
|
148 |
scr = Rule.Empty_Prog},
|
walther@60358
|
149 |
srls = Rule_Set.Empty, calc = [], errpatts = [],
|
walther@60358
|
150 |
rules = [ (*\<^rule_thm>\<open>call_for_new_c\<close>,*)
|
walther@60358
|
151 |
Rule.Cal1 ("Integrate.add_new_c", eval_add_new_c "new_c_")],
|
walther@60358
|
152 |
scr = Rule.Empty_Prog};
|
wneuper@59472
|
153 |
\<close>
|
wneuper@59472
|
154 |
ML \<open>
|
neuper@37954
|
155 |
|
neuper@37954
|
156 |
(*.rulesets for simplifying Integrals.*)
|
neuper@37954
|
157 |
|
neuper@37954
|
158 |
(*.for simplify_Integral adapted from 'norm_Rational_rls'.*)
|
neuper@37954
|
159 |
val norm_Rational_rls_noadd_fractions =
|
walther@60358
|
160 |
Rule_Def.Repeat {id = "norm_Rational_rls_noadd_fractions", preconds = [],
|
walther@60358
|
161 |
rew_ord = ("dummy_ord",Rewrite_Ord.dummy_ord),
|
walther@60358
|
162 |
erls = norm_rat_erls, srls = Rule_Set.Empty, calc = [], errpatts = [],
|
walther@60358
|
163 |
rules = [(*Rule.Rls_ add_fractions_p_rls,!!!*)
|
walther@60358
|
164 |
Rule.Rls_ (*rat_mult_div_pow original corrected WN051028*)
|
walther@60358
|
165 |
(Rule_Def.Repeat {id = "rat_mult_div_pow", preconds = [],
|
walther@60358
|
166 |
rew_ord = ("dummy_ord",Rewrite_Ord.dummy_ord),
|
walther@60358
|
167 |
erls = Rule_Set.append_rules "Rule_Set.empty-is_polyexp" Rule_Set.empty
|
walther@60358
|
168 |
[\<^rule_eval>\<open>is_polyexp\<close> (eval_is_polyexp "")],
|
walther@60358
|
169 |
srls = Rule_Set.Empty, calc = [], errpatts = [],
|
walther@60358
|
170 |
rules = [
|
walther@60358
|
171 |
\<^rule_thm>\<open>rat_mult\<close>, (*"?a / ?b * (?c / ?d) = ?a * ?c / (?b * ?d)"*)
|
walther@60358
|
172 |
\<^rule_thm>\<open>rat_mult_poly_l\<close>, (*"?c is_polyexp ==> ?c * (?a / ?b) = ?c * ?a / ?b"*)
|
walther@60358
|
173 |
\<^rule_thm>\<open>rat_mult_poly_r\<close>, (*"?c is_polyexp ==> ?a / ?b * ?c = ?a * ?c / ?b"*)
|
walther@60358
|
174 |
|
walther@60358
|
175 |
\<^rule_thm>\<open>real_divide_divide1_mg\<close>, (*"y ~= 0 ==> (u / v) / (y / z) = (u * z) / (y * v)"*)
|
walther@60358
|
176 |
\<^rule_thm>\<open>divide_divide_eq_right\<close>, (*"?x / (?y / ?z) = ?x * ?z / ?y"*)
|
walther@60358
|
177 |
\<^rule_thm>\<open>divide_divide_eq_left\<close>, (*"?x / ?y / ?z = ?x / (?y * ?z)"*)
|
walther@60358
|
178 |
\<^rule_eval>\<open>divide\<close> (Prog_Expr.eval_cancel "#divide_e"),
|
walther@60358
|
179 |
|
walther@60358
|
180 |
\<^rule_thm>\<open>rat_power\<close>], (*"(?a / ?b) \<up> ?n = ?a \<up> ?n / ?b \<up> ?n"*)
|
walther@60358
|
181 |
scr = Rule.Empty_Prog}),
|
walther@60358
|
182 |
Rule.Rls_ make_rat_poly_with_parentheses,
|
walther@60358
|
183 |
Rule.Rls_ cancel_p_rls,(*FIXME:cancel_p does NOT order sometimes*)
|
walther@60358
|
184 |
Rule.Rls_ rat_reduce_1],
|
walther@60358
|
185 |
scr = Rule.Empty_Prog};
|
neuper@37954
|
186 |
|
neuper@37954
|
187 |
(*.for simplify_Integral adapted from 'norm_Rational'.*)
|
neuper@37954
|
188 |
val norm_Rational_noadd_fractions =
|
walther@60358
|
189 |
Rule_Set.Sequence {id = "norm_Rational_noadd_fractions", preconds = [],
|
walther@60358
|
190 |
rew_ord = ("dummy_ord",Rewrite_Ord.dummy_ord),
|
walther@60358
|
191 |
erls = norm_rat_erls, srls = Rule_Set.Empty, calc = [], errpatts = [],
|
walther@60358
|
192 |
rules = [Rule.Rls_ discard_minus,
|
walther@60358
|
193 |
Rule.Rls_ rat_mult_poly,(* removes double fractions like a/b/c *)
|
walther@60358
|
194 |
Rule.Rls_ make_rat_poly_with_parentheses, (*WN0510 also in(#)below*)
|
walther@60358
|
195 |
Rule.Rls_ cancel_p_rls, (*FIXME.MG:cancel_p does NOT order sometim*)
|
walther@60358
|
196 |
Rule.Rls_ norm_Rational_rls_noadd_fractions,(* the main rls (#) *)
|
walther@60358
|
197 |
Rule.Rls_ discard_parentheses1], (* mult only *)
|
walther@60358
|
198 |
scr = Rule.Empty_Prog};
|
neuper@37954
|
199 |
|
neuper@37954
|
200 |
(*.simplify terms before and after Integration such that
|
neuper@37954
|
201 |
..a.x^2/2 + b.x^3/3.. is made to ..a/2.x^2 + b/3.x^3.. (and NO
|
neuper@37954
|
202 |
common denominator as done by norm_Rational or make_ratpoly_in.
|
neuper@37954
|
203 |
This is a copy from 'make_ratpoly_in' with respective reduction of rules and
|
neuper@37954
|
204 |
*1* expand the term, ie. distribute * and / over +
|
neuper@37954
|
205 |
.*)
|
neuper@37954
|
206 |
val separate_bdv2 =
|
walther@60358
|
207 |
Rule_Set.append_rules "separate_bdv2" collect_bdv [
|
walther@60358
|
208 |
\<^rule_thm>\<open>separate_bdv\<close>, (*"?a * ?bdv / ?b = ?a / ?b * ?bdv"*)
|
wenzelm@60297
|
209 |
\<^rule_thm>\<open>separate_bdv_n\<close>,
|
walther@60358
|
210 |
\<^rule_thm>\<open>separate_1_bdv\<close>, (*"?bdv / ?b = (1 / ?b) * ?bdv"*)
|
walther@60358
|
211 |
\<^rule_thm>\<open>separate_1_bdv_n\<close> (*"?bdv \<up> ?n / ?b = 1 / ?b * ?bdv \<up> ?n"*)
|
walther@60358
|
212 |
(*
|
walther@60358
|
213 |
rule_thm>\<open>add_divide_distrib\<close> (*"(?x + ?y) / ?z = ?x / ?z + ?y / ?z"*)*)
|
neuper@37954
|
214 |
];
|
neuper@37954
|
215 |
val simplify_Integral =
|
walther@59878
|
216 |
Rule_Set.Sequence {id = "simplify_Integral", preconds = []:term list,
|
walther@60358
|
217 |
rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord),
|
walther@60358
|
218 |
erls = Atools_erls, srls = Rule_Set.Empty,
|
walther@60358
|
219 |
calc = [], errpatts = [],
|
walther@60358
|
220 |
rules = [
|
walther@60358
|
221 |
\<^rule_thm>\<open>distrib_right\<close>, (*"(?z1.0 + ?z2.0) * ?w = ?z1.0 * ?w + ?z2.0 * ?w"*)
|
walther@60358
|
222 |
\<^rule_thm>\<open>add_divide_distrib\<close>, (*"(?x + ?y) / ?z = ?x / ?z + ?y / ?z"*)
|
walther@60358
|
223 |
(*^^^^^ *1* ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^*)
|
walther@60358
|
224 |
Rule.Rls_ norm_Rational_noadd_fractions,
|
walther@60358
|
225 |
Rule.Rls_ order_add_mult_in,
|
walther@60358
|
226 |
Rule.Rls_ discard_parentheses,
|
walther@60358
|
227 |
(*Rule.Rls_ collect_bdv, from make_polynomial_in*)
|
walther@60358
|
228 |
Rule.Rls_ separate_bdv2,
|
walther@60358
|
229 |
\<^rule_eval>\<open>divide\<close> (Prog_Expr.eval_cancel "#divide_e")],
|
walther@60358
|
230 |
scr = Rule.Empty_Prog};
|
neuper@37954
|
231 |
|
walther@60358
|
232 |
val integration =
|
walther@60358
|
233 |
Rule_Set.Sequence {
|
walther@60358
|
234 |
id="integration", preconds = [], rew_ord = ("termlessI",termlessI),
|
walther@60358
|
235 |
erls = Rule_Def.Repeat {
|
walther@60358
|
236 |
id="conditions_in_integration", preconds = [], rew_ord = ("termlessI",termlessI),
|
walther@60358
|
237 |
erls = Rule_Set.Empty, srls = Rule_Set.Empty, calc = [], errpatts = [],
|
walther@60358
|
238 |
rules = [], scr = Rule.Empty_Prog},
|
walther@60358
|
239 |
srls = Rule_Set.Empty, calc = [], errpatts = [],
|
walther@60358
|
240 |
rules = [
|
walther@60358
|
241 |
Rule.Rls_ integration_rules,
|
walther@60358
|
242 |
Rule.Rls_ add_new_c,
|
walther@60358
|
243 |
Rule.Rls_ simplify_Integral],
|
walther@60358
|
244 |
scr = Rule.Empty_Prog};
|
s1210629013@55444
|
245 |
|
walther@59618
|
246 |
val prep_rls' = Auto_Prog.prep_rls @{theory};
|
wneuper@59472
|
247 |
\<close>
|
wenzelm@60289
|
248 |
rule_set_knowledge
|
wenzelm@60286
|
249 |
integration_rules = \<open>prep_rls' integration_rules\<close> and
|
wenzelm@60286
|
250 |
add_new_c = \<open>prep_rls' add_new_c\<close> and
|
wenzelm@60286
|
251 |
simplify_Integral = \<open>prep_rls' simplify_Integral\<close> and
|
wenzelm@60286
|
252 |
integration = \<open>prep_rls' integration\<close> and
|
wenzelm@60286
|
253 |
separate_bdv2 = \<open>prep_rls' separate_bdv2\<close> and
|
wenzelm@60286
|
254 |
norm_Rational_noadd_fractions = \<open>prep_rls' norm_Rational_noadd_fractions\<close> and
|
wenzelm@60286
|
255 |
norm_Rational_rls_noadd_fractions = \<open>prep_rls' norm_Rational_rls_noadd_fractions\<close>
|
neuper@37954
|
256 |
|
neuper@37954
|
257 |
(** problems **)
|
wenzelm@60306
|
258 |
|
wenzelm@60306
|
259 |
problem pbl_fun_integ : "integrate/function" =
|
wenzelm@60306
|
260 |
\<open>Rule_Set.append_rules "empty" Rule_Set.empty [(*for preds in where_*)]\<close>
|
Walther@60449
|
261 |
Method_Ref: "diff/integration"
|
wenzelm@60306
|
262 |
CAS: "Integrate (f_f, v_v)"
|
wenzelm@60306
|
263 |
Given: "functionTerm f_f" "integrateBy v_v"
|
wenzelm@60306
|
264 |
Find: "antiDerivative F_F"
|
wenzelm@60306
|
265 |
|
wenzelm@60306
|
266 |
problem pbl_fun_integ_nam : "named/integrate/function" =
|
wenzelm@60306
|
267 |
(*here "named" is used differently from Differentiation"*)
|
wenzelm@60306
|
268 |
\<open>Rule_Set.append_rules "empty" Rule_Set.empty [(*for preds in where_*)]\<close>
|
Walther@60449
|
269 |
Method_Ref: "diff/integration/named"
|
wenzelm@60306
|
270 |
CAS: "Integrate (f_f, v_v)"
|
wenzelm@60306
|
271 |
Given: "functionTerm f_f" "integrateBy v_v"
|
wenzelm@60306
|
272 |
Find: "antiDerivativeName F_F"
|
s1210629013@55380
|
273 |
|
neuper@37954
|
274 |
(** methods **)
|
wneuper@59545
|
275 |
|
wneuper@59504
|
276 |
partial_function (tailrec) integrate :: "real \<Rightarrow> real \<Rightarrow> real"
|
wneuper@59504
|
277 |
where
|
walther@59635
|
278 |
"integrate f_f v_v = (
|
walther@59635
|
279 |
let
|
walther@59635
|
280 |
t_t = Take (Integral f_f D v_v)
|
walther@59635
|
281 |
in
|
walther@59635
|
282 |
(Rewrite_Set_Inst [(''bdv'', v_v)] ''integration'') t_t)"
|
wenzelm@60303
|
283 |
|
wenzelm@60303
|
284 |
method met_diffint : "diff/integration" =
|
wenzelm@60303
|
285 |
\<open>{rew_ord'="tless_true", rls'=Atools_erls, calc = [], srls = Rule_Set.empty, prls=Rule_Set.empty,
|
wenzelm@60303
|
286 |
crls = Atools_erls, errpats = [], nrls = Rule_Set.empty}\<close>
|
wenzelm@60303
|
287 |
Program: integrate.simps
|
wenzelm@60303
|
288 |
Given: "functionTerm f_f" "integrateBy v_v"
|
wenzelm@60303
|
289 |
Find: "antiDerivative F_F"
|
wneuper@59545
|
290 |
|
wneuper@59504
|
291 |
partial_function (tailrec) intergrate_named :: "real \<Rightarrow> real \<Rightarrow> (real \<Rightarrow> real) \<Rightarrow> bool"
|
walther@59635
|
292 |
where
|
walther@59635
|
293 |
"intergrate_named f_f v_v F_F =(
|
walther@59635
|
294 |
let
|
walther@59635
|
295 |
t_t = Take (F_F v_v = Integral f_f D v_v)
|
walther@59635
|
296 |
in (
|
walther@59637
|
297 |
(Try (Rewrite_Set_Inst [(''bdv'', v_v)] ''simplify_Integral'')) #>
|
walther@59635
|
298 |
(Rewrite_Set_Inst [(''bdv'', v_v)] ''integration'')
|
walther@59635
|
299 |
) t_t)"
|
wenzelm@60303
|
300 |
|
wenzelm@60303
|
301 |
method met_diffint_named : "diff/integration/named" =
|
wenzelm@60303
|
302 |
\<open>{rew_ord'="tless_true", rls'=Atools_erls, calc = [], srls = Rule_Set.empty, prls=Rule_Set.empty,
|
wenzelm@60303
|
303 |
crls = Atools_erls, errpats = [], nrls = Rule_Set.empty}\<close>
|
wenzelm@60303
|
304 |
Program: intergrate_named.simps
|
wenzelm@60303
|
305 |
Given: "functionTerm f_f" "integrateBy v_v"
|
wenzelm@60303
|
306 |
Find: "antiDerivativeName F_F"
|
wenzelm@60303
|
307 |
|
wenzelm@60303
|
308 |
ML \<open>
|
walther@60278
|
309 |
\<close> ML \<open>
|
wneuper@59472
|
310 |
\<close>
|
neuper@37954
|
311 |
|
neuper@37906
|
312 |
end |