1.1 --- a/src/Tools/isac/Knowledge/Integrate.thy Thu Mar 15 10:17:44 2018 +0100
1.2 +++ b/src/Tools/isac/Knowledge/Integrate.thy Thu Mar 15 12:42:04 2018 +0100
1.3 @@ -50,7 +50,7 @@
1.4 (** eval functions **)
1.5
1.6 val c = Free ("c", HOLogic.realT);
1.7 -(*.create a new unique variable 'c..' in a term; for use by Calc in a rls;
1.8 +(*.create a new unique variable 'c..' in a term; for use by Celem.Calc in a rls;
1.9 an alternative to do this would be '(Try (Calculate new_c_) (new_c es__))'
1.10 in the script; this will be possible if currying doesnt take the value
1.11 from a variable, but the value '(new_c es__)' itself.*)
1.12 @@ -78,7 +78,7 @@
1.13 (*WN080222
1.14 (*("new_c", ("Integrate.new'_c", eval_new_c "#new_c_"))*)
1.15 fun eval_new_c _ _ (p as (Const ("Integrate.new'_c",_) $ t)) _ =
1.16 - SOME ((term2str p) ^ " = " ^ term2str (new_c p),
1.17 + SOME ((Celem.term2str p) ^ " = " ^ Celem.term2str (new_c p),
1.18 Trueprop $ (mk_equality (p, new_c p)))
1.19 | eval_new_c _ _ _ _ = NONE;
1.20 *)
1.21 @@ -92,7 +92,7 @@
1.22 Const ("HOL.eq", T) $ lh $ rh =>
1.23 Const ("HOL.eq", T) $ lh $ TermC.mk_add rh (new_c rh)
1.24 | p => TermC.mk_add p (new_c p)
1.25 - in SOME ((term2str p) ^ " = " ^ term2str p',
1.26 + in SOME ((Celem.term2str p) ^ " = " ^ Celem.term2str p',
1.27 HOLogic.Trueprop $ (TermC.mk_equality (p, p')))
1.28 end
1.29 | eval_add_new_c _ _ _ _ = NONE;
1.30 @@ -102,9 +102,9 @@
1.31 fun eval_is_f_x _ _(p as (Const ("Integrate.is'_f'_x", _)
1.32 $ arg)) _ =
1.33 if TermC.is_f_x arg
1.34 - then SOME ((term2str p) ^ " = True",
1.35 + then SOME ((Celem.term2str p) ^ " = True",
1.36 HOLogic.Trueprop $ (TermC.mk_equality (p, @{term True})))
1.37 - else SOME ((term2str p) ^ " = False",
1.38 + else SOME ((Celem.term2str p) ^ " = False",
1.39 HOLogic.Trueprop $ (TermC.mk_equality (p, @{term False})))
1.40 | eval_is_f_x _ _ _ _ = NONE;
1.41 *}
1.42 @@ -116,52 +116,52 @@
1.43
1.44 (*.rulesets for integration.*)
1.45 val integration_rules =
1.46 - Rls {id="integration_rules", preconds = [],
1.47 + Celem.Rls {id="integration_rules", preconds = [],
1.48 rew_ord = ("termlessI",termlessI),
1.49 - erls = Rls {id="conditions_in_integration_rules",
1.50 + erls = Celem.Rls {id="conditions_in_integration_rules",
1.51 preconds = [],
1.52 rew_ord = ("termlessI",termlessI),
1.53 - erls = Erls,
1.54 - srls = Erls, calc = [], errpatts = [],
1.55 + erls = Celem.Erls,
1.56 + srls = Celem.Erls, calc = [], errpatts = [],
1.57 rules = [(*for rewriting conditions in Thm's*)
1.58 - Calc ("Atools.occurs'_in",
1.59 + Celem.Calc ("Atools.occurs'_in",
1.60 eval_occurs_in "#occurs_in_"),
1.61 - Thm ("not_true", TermC.num_str @{thm not_true}),
1.62 - Thm ("not_false",@{thm not_false})
1.63 + Celem.Thm ("not_true", TermC.num_str @{thm not_true}),
1.64 + Celem.Thm ("not_false",@{thm not_false})
1.65 ],
1.66 - scr = EmptyScr},
1.67 - srls = Erls, calc = [], errpatts = [],
1.68 + scr = Celem.EmptyScr},
1.69 + srls = Celem.Erls, calc = [], errpatts = [],
1.70 rules = [
1.71 - Thm ("integral_const", TermC.num_str @{thm integral_const}),
1.72 - Thm ("integral_var", TermC.num_str @{thm integral_var}),
1.73 - Thm ("integral_add", TermC.num_str @{thm integral_add}),
1.74 - Thm ("integral_mult", TermC.num_str @{thm integral_mult}),
1.75 - Thm ("integral_pow", TermC.num_str @{thm integral_pow}),
1.76 - Calc ("Groups.plus_class.plus", eval_binop "#add_")(*for n+1*)
1.77 + Celem.Thm ("integral_const", TermC.num_str @{thm integral_const}),
1.78 + Celem.Thm ("integral_var", TermC.num_str @{thm integral_var}),
1.79 + Celem.Thm ("integral_add", TermC.num_str @{thm integral_add}),
1.80 + Celem.Thm ("integral_mult", TermC.num_str @{thm integral_mult}),
1.81 + Celem.Thm ("integral_pow", TermC.num_str @{thm integral_pow}),
1.82 + Celem.Calc ("Groups.plus_class.plus", eval_binop "#add_")(*for n+1*)
1.83 ],
1.84 - scr = EmptyScr};
1.85 + scr = Celem.EmptyScr};
1.86 *}
1.87 ML {*
1.88 val add_new_c =
1.89 - Seq {id="add_new_c", preconds = [],
1.90 + Celem.Seq {id="add_new_c", preconds = [],
1.91 rew_ord = ("termlessI",termlessI),
1.92 - erls = Rls {id="conditions_in_add_new_c",
1.93 + erls = Celem.Rls {id="conditions_in_add_new_c",
1.94 preconds = [],
1.95 rew_ord = ("termlessI",termlessI),
1.96 - erls = Erls,
1.97 - srls = Erls, calc = [], errpatts = [],
1.98 - rules = [Calc ("Tools.matches", eval_matches""),
1.99 - Calc ("Integrate.is'_f'_x",
1.100 + erls = Celem.Erls,
1.101 + srls = Celem.Erls, calc = [], errpatts = [],
1.102 + rules = [Celem.Calc ("Tools.matches", eval_matches""),
1.103 + Celem.Calc ("Integrate.is'_f'_x",
1.104 eval_is_f_x "is_f_x_"),
1.105 - Thm ("not_true", TermC.num_str @{thm not_true}),
1.106 - Thm ("not_false", TermC.num_str @{thm not_false})
1.107 + Celem.Thm ("not_true", TermC.num_str @{thm not_true}),
1.108 + Celem.Thm ("not_false", TermC.num_str @{thm not_false})
1.109 ],
1.110 - scr = EmptyScr},
1.111 - srls = Erls, calc = [], errpatts = [],
1.112 - rules = [ (*Thm ("call_for_new_c", TermC.num_str @{thm call_for_new_c}),*)
1.113 - Cal1 ("Integrate.add'_new'_c", eval_add_new_c "new_c_")
1.114 + scr = Celem.EmptyScr},
1.115 + srls = Celem.Erls, calc = [], errpatts = [],
1.116 + rules = [ (*Celem.Thm ("call_for_new_c", TermC.num_str @{thm call_for_new_c}),*)
1.117 + Celem.Cal1 ("Integrate.add'_new'_c", eval_add_new_c "new_c_")
1.118 ],
1.119 - scr = EmptyScr};
1.120 + scr = Celem.EmptyScr};
1.121 *}
1.122 ML {*
1.123
1.124 @@ -169,62 +169,62 @@
1.125
1.126 (*.for simplify_Integral adapted from 'norm_Rational_rls'.*)
1.127 val norm_Rational_rls_noadd_fractions =
1.128 -Rls {id = "norm_Rational_rls_noadd_fractions", preconds = [],
1.129 - rew_ord = ("dummy_ord",dummy_ord),
1.130 - erls = norm_rat_erls, srls = Erls, calc = [], errpatts = [],
1.131 - rules = [(*Rls_ add_fractions_p_rls,!!!*)
1.132 - Rls_ (*rat_mult_div_pow original corrected WN051028*)
1.133 - (Rls {id = "rat_mult_div_pow", preconds = [],
1.134 - rew_ord = ("dummy_ord",dummy_ord),
1.135 - erls = (*FIXME.WN051028 e_rls,*)
1.136 - append_rls "e_rls-is_polyexp" e_rls
1.137 - [Calc ("Poly.is'_polyexp",
1.138 +Celem.Rls {id = "norm_Rational_rls_noadd_fractions", preconds = [],
1.139 + rew_ord = ("dummy_ord",Celem.dummy_ord),
1.140 + erls = norm_rat_erls, srls = Celem.Erls, calc = [], errpatts = [],
1.141 + rules = [(*Celem.Rls_ add_fractions_p_rls,!!!*)
1.142 + Celem.Rls_ (*rat_mult_div_pow original corrected WN051028*)
1.143 + (Celem.Rls {id = "rat_mult_div_pow", preconds = [],
1.144 + rew_ord = ("dummy_ord",Celem.dummy_ord),
1.145 + erls = (*FIXME.WN051028 Celem.e_rls,*)
1.146 + Celem.append_rls "Celem.e_rls-is_polyexp" Celem.e_rls
1.147 + [Celem.Calc ("Poly.is'_polyexp",
1.148 eval_is_polyexp "")],
1.149 - srls = Erls, calc = [], errpatts = [],
1.150 - rules = [Thm ("rat_mult", TermC.num_str @{thm rat_mult}),
1.151 + srls = Celem.Erls, calc = [], errpatts = [],
1.152 + rules = [Celem.Thm ("rat_mult", TermC.num_str @{thm rat_mult}),
1.153 (*"?a / ?b * (?c / ?d) = ?a * ?c / (?b * ?d)"*)
1.154 - Thm ("rat_mult_poly_l", TermC.num_str @{thm rat_mult_poly_l}),
1.155 + Celem.Thm ("rat_mult_poly_l", TermC.num_str @{thm rat_mult_poly_l}),
1.156 (*"?c is_polyexp ==> ?c * (?a / ?b) = ?c * ?a / ?b"*)
1.157 - Thm ("rat_mult_poly_r", TermC.num_str @{thm rat_mult_poly_r}),
1.158 + Celem.Thm ("rat_mult_poly_r", TermC.num_str @{thm rat_mult_poly_r}),
1.159 (*"?c is_polyexp ==> ?a / ?b * ?c = ?a * ?c / ?b"*)
1.160
1.161 - Thm ("real_divide_divide1_mg",
1.162 + Celem.Thm ("real_divide_divide1_mg",
1.163 TermC.num_str @{thm real_divide_divide1_mg}),
1.164 (*"y ~= 0 ==> (u / v) / (y / z) = (u * z) / (y * v)"*)
1.165 - Thm ("divide_divide_eq_right",
1.166 + Celem.Thm ("divide_divide_eq_right",
1.167 TermC.num_str @{thm divide_divide_eq_right}),
1.168 (*"?x / (?y / ?z) = ?x * ?z / ?y"*)
1.169 - Thm ("divide_divide_eq_left",
1.170 + Celem.Thm ("divide_divide_eq_left",
1.171 TermC.num_str @{thm divide_divide_eq_left}),
1.172 (*"?x / ?y / ?z = ?x / (?y * ?z)"*)
1.173 - Calc ("Rings.divide_class.divide" ,eval_cancel "#divide_e"),
1.174 + Celem.Calc ("Rings.divide_class.divide" ,eval_cancel "#divide_e"),
1.175
1.176 - Thm ("rat_power", TermC.num_str @{thm rat_power})
1.177 + Celem.Thm ("rat_power", TermC.num_str @{thm rat_power})
1.178 (*"(?a / ?b) ^^^ ?n = ?a ^^^ ?n / ?b ^^^ ?n"*)
1.179 ],
1.180 - scr = Prog ((Thm.term_of o the o (TermC.parse thy)) "empty_script")
1.181 + scr = Celem.Prog ((Thm.term_of o the o (TermC.parse thy)) "empty_script")
1.182 }),
1.183 - Rls_ make_rat_poly_with_parentheses,
1.184 - Rls_ cancel_p_rls,(*FIXME:cancel_p does NOT order sometimes*)
1.185 - Rls_ rat_reduce_1
1.186 + Celem.Rls_ make_rat_poly_with_parentheses,
1.187 + Celem.Rls_ cancel_p_rls,(*FIXME:cancel_p does NOT order sometimes*)
1.188 + Celem.Rls_ rat_reduce_1
1.189 ],
1.190 - scr = Prog ((Thm.term_of o the o (TermC.parse thy)) "empty_script")
1.191 - }:rls;
1.192 + scr = Celem.Prog ((Thm.term_of o the o (TermC.parse thy)) "empty_script")
1.193 + };
1.194
1.195 (*.for simplify_Integral adapted from 'norm_Rational'.*)
1.196 val norm_Rational_noadd_fractions =
1.197 - Seq {id = "norm_Rational_noadd_fractions", preconds = [],
1.198 - rew_ord = ("dummy_ord",dummy_ord),
1.199 - erls = norm_rat_erls, srls = Erls, calc = [], errpatts = [],
1.200 - rules = [Rls_ discard_minus,
1.201 - Rls_ rat_mult_poly,(* removes double fractions like a/b/c *)
1.202 - Rls_ make_rat_poly_with_parentheses, (*WN0510 also in(#)below*)
1.203 - Rls_ cancel_p_rls, (*FIXME.MG:cancel_p does NOT order sometim*)
1.204 - Rls_ norm_Rational_rls_noadd_fractions,(* the main rls (#) *)
1.205 - Rls_ discard_parentheses1 (* mult only *)
1.206 + Celem.Seq {id = "norm_Rational_noadd_fractions", preconds = [],
1.207 + rew_ord = ("dummy_ord",Celem.dummy_ord),
1.208 + erls = norm_rat_erls, srls = Celem.Erls, calc = [], errpatts = [],
1.209 + rules = [Celem.Rls_ discard_minus,
1.210 + Celem.Rls_ rat_mult_poly,(* removes double fractions like a/b/c *)
1.211 + Celem.Rls_ make_rat_poly_with_parentheses, (*WN0510 also in(#)below*)
1.212 + Celem.Rls_ cancel_p_rls, (*FIXME.MG:cancel_p does NOT order sometim*)
1.213 + Celem.Rls_ norm_Rational_rls_noadd_fractions,(* the main rls (#) *)
1.214 + Celem.Rls_ discard_parentheses1 (* mult only *)
1.215 ],
1.216 - scr = Prog ((Thm.term_of o the o (TermC.parse thy)) "empty_script")
1.217 - }:rls;
1.218 + scr = Celem.Prog ((Thm.term_of o the o (TermC.parse thy)) "empty_script")
1.219 + };
1.220
1.221 (*.simplify terms before and after Integration such that
1.222 ..a.x^2/2 + b.x^3/3.. is made to ..a/2.x^2 + b/3.x^3.. (and NO
1.223 @@ -233,37 +233,37 @@
1.224 *1* expand the term, ie. distribute * and / over +
1.225 .*)
1.226 val separate_bdv2 =
1.227 - append_rls "separate_bdv2"
1.228 + Celem.append_rls "separate_bdv2"
1.229 collect_bdv
1.230 - [Thm ("separate_bdv", TermC.num_str @{thm separate_bdv}),
1.231 + [Celem.Thm ("separate_bdv", TermC.num_str @{thm separate_bdv}),
1.232 (*"?a * ?bdv / ?b = ?a / ?b * ?bdv"*)
1.233 - Thm ("separate_bdv_n", TermC.num_str @{thm separate_bdv_n}),
1.234 - Thm ("separate_1_bdv", TermC.num_str @{thm separate_1_bdv}),
1.235 + Celem.Thm ("separate_bdv_n", TermC.num_str @{thm separate_bdv_n}),
1.236 + Celem.Thm ("separate_1_bdv", TermC.num_str @{thm separate_1_bdv}),
1.237 (*"?bdv / ?b = (1 / ?b) * ?bdv"*)
1.238 - Thm ("separate_1_bdv_n", TermC.num_str @{thm separate_1_bdv_n})(*,
1.239 + Celem.Thm ("separate_1_bdv_n", TermC.num_str @{thm separate_1_bdv_n})(*,
1.240 (*"?bdv ^^^ ?n / ?b = 1 / ?b * ?bdv ^^^ ?n"*)
1.241 - *****Thm ("add_divide_distrib",
1.242 + *****Celem.Thm ("add_divide_distrib",
1.243 ***** TermC.num_str @{thm add_divide_distrib})
1.244 (*"(?x + ?y) / ?z = ?x / ?z + ?y / ?z"*)----------*)
1.245 ];
1.246 val simplify_Integral =
1.247 - Seq {id = "simplify_Integral", preconds = []:term list,
1.248 - rew_ord = ("dummy_ord", dummy_ord),
1.249 - erls = Atools_erls, srls = Erls,
1.250 + Celem.Seq {id = "simplify_Integral", preconds = []:term list,
1.251 + rew_ord = ("dummy_ord", Celem.dummy_ord),
1.252 + erls = Atools_erls, srls = Celem.Erls,
1.253 calc = [], errpatts = [],
1.254 - rules = [Thm ("distrib_right", TermC.num_str @{thm distrib_right}),
1.255 + rules = [Celem.Thm ("distrib_right", TermC.num_str @{thm distrib_right}),
1.256 (*"(?z1.0 + ?z2.0) * ?w = ?z1.0 * ?w + ?z2.0 * ?w"*)
1.257 - Thm ("add_divide_distrib", TermC.num_str @{thm add_divide_distrib}),
1.258 + Celem.Thm ("add_divide_distrib", TermC.num_str @{thm add_divide_distrib}),
1.259 (*"(?x + ?y) / ?z = ?x / ?z + ?y / ?z"*)
1.260 (*^^^^^ *1* ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^*)
1.261 - Rls_ norm_Rational_noadd_fractions,
1.262 - Rls_ order_add_mult_in,
1.263 - Rls_ discard_parentheses,
1.264 - (*Rls_ collect_bdv, from make_polynomial_in*)
1.265 - Rls_ separate_bdv2,
1.266 - Calc ("Rings.divide_class.divide" ,eval_cancel "#divide_e")
1.267 + Celem.Rls_ norm_Rational_noadd_fractions,
1.268 + Celem.Rls_ order_add_mult_in,
1.269 + Celem.Rls_ discard_parentheses,
1.270 + (*Celem.Rls_ collect_bdv, from make_polynomial_in*)
1.271 + Celem.Rls_ separate_bdv2,
1.272 + Celem.Calc ("Rings.divide_class.divide" ,eval_cancel "#divide_e")
1.273 ],
1.274 - scr = EmptyScr}:rls;
1.275 + scr = Celem.EmptyScr};
1.276
1.277
1.278 (*simplify terms before and after Integration such that
1.279 @@ -273,54 +273,54 @@
1.280 'make_ratpoly_in'
1.281 THIS IS KEPT FOR COMPARISON ............................................
1.282 * val simplify_Integral = prep_rls'(
1.283 -* Seq {id = "", preconds = []:term list,
1.284 -* rew_ord = ("dummy_ord", dummy_ord),
1.285 -* erls = Atools_erls, srls = Erls,
1.286 +* Celem.Seq {id = "", preconds = []:term list,
1.287 +* rew_ord = ("dummy_ord", Celem.dummy_ord),
1.288 +* erls = Atools_erls, srls = Celem.Erls,
1.289 * calc = [], (*asm_thm = [],*)
1.290 -* rules = [Rls_ expand_poly,
1.291 -* Rls_ order_add_mult_in,
1.292 -* Rls_ simplify_power,
1.293 -* Rls_ collect_numerals,
1.294 -* Rls_ reduce_012,
1.295 -* Thm ("realpow_oneI", TermC.num_str @{thm realpow_oneI}),
1.296 -* Rls_ discard_parentheses,
1.297 -* Rls_ collect_bdv,
1.298 +* rules = [Celem.Rls_ expand_poly,
1.299 +* Celem.Rls_ order_add_mult_in,
1.300 +* Celem.Rls_ simplify_power,
1.301 +* Celem.Rls_ collect_numerals,
1.302 +* Celem.Rls_ reduce_012,
1.303 +* Celem.Thm ("realpow_oneI", TermC.num_str @{thm realpow_oneI}),
1.304 +* Celem.Rls_ discard_parentheses,
1.305 +* Celem.Rls_ collect_bdv,
1.306 * (*below inserted from 'make_ratpoly_in'*)
1.307 -* Rls_ (append_rls "separate_bdv"
1.308 +* Celem.Rls_ (Celem.append_rls "separate_bdv"
1.309 * collect_bdv
1.310 -* [Thm ("separate_bdv", TermC.num_str @{thm separate_bdv}),
1.311 +* [Celem.Thm ("separate_bdv", TermC.num_str @{thm separate_bdv}),
1.312 * (*"?a * ?bdv / ?b = ?a / ?b * ?bdv"*)
1.313 -* Thm ("separate_bdv_n", TermC.num_str @{thm separate_bdv_n}),
1.314 -* Thm ("separate_1_bdv", TermC.num_str @{thm separate_1_bdv}),
1.315 +* Celem.Thm ("separate_bdv_n", TermC.num_str @{thm separate_bdv_n}),
1.316 +* Celem.Thm ("separate_1_bdv", TermC.num_str @{thm separate_1_bdv}),
1.317 * (*"?bdv / ?b = (1 / ?b) * ?bdv"*)
1.318 -* Thm ("separate_1_bdv_n", TermC.num_str @{thm separate_1_bdv_n})(*,
1.319 +* Celem.Thm ("separate_1_bdv_n", TermC.num_str @{thm separate_1_bdv_n})(*,
1.320 * (*"?bdv ^^^ ?n / ?b = 1 / ?b * ?bdv ^^^ ?n"*)
1.321 -* Thm ("add_divide_distrib",
1.322 +* Celem.Thm ("add_divide_distrib",
1.323 * TermC.num_str @{thm add_divide_distrib})
1.324 * (*"(?x + ?y) / ?z = ?x / ?z + ?y / ?z"*)*)
1.325 * ]),
1.326 -* Calc ("Rings.divide_class.divide" ,eval_cancel "#divide_e")
1.327 +* Celem.Calc ("Rings.divide_class.divide" ,eval_cancel "#divide_e")
1.328 * ],
1.329 -* scr = EmptyScr
1.330 -* }:rls);
1.331 +* scr = Celem.EmptyScr
1.332 +* });
1.333 .......................................................................*)
1.334
1.335 val integration =
1.336 - Seq {id="integration", preconds = [],
1.337 + Celem.Seq {id="integration", preconds = [],
1.338 rew_ord = ("termlessI",termlessI),
1.339 - erls = Rls {id="conditions_in_integration",
1.340 + erls = Celem.Rls {id="conditions_in_integration",
1.341 preconds = [],
1.342 rew_ord = ("termlessI",termlessI),
1.343 - erls = Erls,
1.344 - srls = Erls, calc = [], errpatts = [],
1.345 + erls = Celem.Erls,
1.346 + srls = Celem.Erls, calc = [], errpatts = [],
1.347 rules = [],
1.348 - scr = EmptyScr},
1.349 - srls = Erls, calc = [], errpatts = [],
1.350 - rules = [ Rls_ integration_rules,
1.351 - Rls_ add_new_c,
1.352 - Rls_ simplify_Integral
1.353 + scr = Celem.EmptyScr},
1.354 + srls = Celem.Erls, calc = [], errpatts = [],
1.355 + rules = [ Celem.Rls_ integration_rules,
1.356 + Celem.Rls_ add_new_c,
1.357 + Celem.Rls_ simplify_Integral
1.358 ],
1.359 - scr = EmptyScr};
1.360 + scr = Celem.EmptyScr};
1.361
1.362 val prep_rls' = LTool.prep_rls @{theory};
1.363 *}
1.364 @@ -338,38 +338,38 @@
1.365
1.366 (** problems **)
1.367 setup {* KEStore_Elems.add_pbts
1.368 - [(Specify.prep_pbt thy "pbl_fun_integ" [] e_pblID
1.369 + [(Specify.prep_pbt thy "pbl_fun_integ" [] Celem.e_pblID
1.370 (["integrate","function"],
1.371 [("#Given" ,["functionTerm f_f", "integrateBy v_v"]),
1.372 ("#Find" ,["antiDerivative F_F"])],
1.373 - append_rls "e_rls" e_rls [(*for preds in where_*)],
1.374 + Celem.append_rls "xxxe_rlsxxx" Celem.e_rls [(*for preds in where_*)],
1.375 SOME "Integrate (f_f, v_v)",
1.376 [["diff","integration"]])),
1.377 (*here "named" is used differently from Differentiation"*)
1.378 - (Specify.prep_pbt thy "pbl_fun_integ_nam" [] e_pblID
1.379 + (Specify.prep_pbt thy "pbl_fun_integ_nam" [] Celem.e_pblID
1.380 (["named","integrate","function"],
1.381 [("#Given" ,["functionTerm f_f", "integrateBy v_v"]),
1.382 ("#Find" ,["antiDerivativeName F_F"])],
1.383 - append_rls "e_rls" e_rls [(*for preds in where_*)],
1.384 + Celem.append_rls "xxxe_rlsxxx" Celem.e_rls [(*for preds in where_*)],
1.385 SOME "Integrate (f_f, v_v)",
1.386 [["diff","integration","named"]]))] *}
1.387
1.388 (** methods **)
1.389 setup {* KEStore_Elems.add_mets
1.390 - [Specify.prep_met thy "met_diffint" [] e_metID
1.391 + [Specify.prep_met thy "met_diffint" [] Celem.e_metID
1.392 (["diff","integration"],
1.393 [("#Given" ,["functionTerm f_f", "integrateBy v_v"]), ("#Find" ,["antiDerivative F_F"])],
1.394 - {rew_ord'="tless_true", rls'=Atools_erls, calc = [], srls = e_rls, prls=e_rls,
1.395 - crls = Atools_erls, errpats = [], nrls = e_rls},
1.396 + {rew_ord'="tless_true", rls'=Atools_erls, calc = [], srls = Celem.e_rls, prls=Celem.e_rls,
1.397 + crls = Atools_erls, errpats = [], nrls = Celem.e_rls},
1.398 "Script IntegrationScript (f_f::real) (v_v::real) = " ^
1.399 " (let t_t = Take (Integral f_f D v_v) " ^
1.400 " in (Rewrite_Set_Inst [(bdv,v_v)] integration False) (t_t::real))"),
1.401 - Specify.prep_met thy "met_diffint_named" [] e_metID
1.402 + Specify.prep_met thy "met_diffint_named" [] Celem.e_metID
1.403 (["diff","integration","named"],
1.404 [("#Given" ,["functionTerm f_f", "integrateBy v_v"]),
1.405 ("#Find" ,["antiDerivativeName F_F"])],
1.406 - {rew_ord'="tless_true", rls'=Atools_erls, calc = [], srls = e_rls, prls=e_rls,
1.407 - crls = Atools_erls, errpats = [], nrls = e_rls},
1.408 + {rew_ord'="tless_true", rls'=Atools_erls, calc = [], srls = Celem.e_rls, prls=Celem.e_rls,
1.409 + crls = Atools_erls, errpats = [], nrls = Celem.e_rls},
1.410 "Script NamedIntegrationScript (f_f::real) (v_v::real) (F_F::real=>real) = " ^
1.411 " (let t_t = Take (F_F v_v = Integral f_f D v_v) " ^
1.412 " in ((Try (Rewrite_Set_Inst [(bdv,v_v)] simplify_Integral False)) @@ " ^