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