1.1 --- a/src/Tools/isac/Knowledge/Integrate.thy Sun Mar 25 13:59:57 2018 +0200
1.2 +++ b/src/Tools/isac/Knowledge/Integrate.thy Mon Mar 26 07:28:39 2018 +0200
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 Celem.Calc in a rls;
1.8 +(*.create a new unique variable 'c..' in a term; for use by Rule.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 ((Celem.term2str p) ^ " = " ^ Celem.term2str (new_c p),
1.17 + SOME ((Rule.term2str p) ^ " = " ^ Rule.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 ((Celem.term2str p) ^ " = " ^ Celem.term2str p',
1.26 + in SOME ((Rule.term2str p) ^ " = " ^ Rule.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 ((Celem.term2str p) ^ " = True",
1.35 + then SOME ((Rule.term2str p) ^ " = True",
1.36 HOLogic.Trueprop $ (TermC.mk_equality (p, @{term True})))
1.37 - else SOME ((Celem.term2str p) ^ " = False",
1.38 + else SOME ((Rule.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 - Celem.Rls {id="integration_rules", preconds = [],
1.47 + Rule.Rls {id="integration_rules", preconds = [],
1.48 rew_ord = ("termlessI",termlessI),
1.49 - erls = Celem.Rls {id="conditions_in_integration_rules",
1.50 + erls = Rule.Rls {id="conditions_in_integration_rules",
1.51 preconds = [],
1.52 rew_ord = ("termlessI",termlessI),
1.53 - erls = Celem.Erls,
1.54 - srls = Celem.Erls, calc = [], errpatts = [],
1.55 + erls = Rule.Erls,
1.56 + srls = Rule.Erls, calc = [], errpatts = [],
1.57 rules = [(*for rewriting conditions in Thm's*)
1.58 - Celem.Calc ("Atools.occurs'_in",
1.59 + Rule.Calc ("Atools.occurs'_in",
1.60 eval_occurs_in "#occurs_in_"),
1.61 - Celem.Thm ("not_true", TermC.num_str @{thm not_true}),
1.62 - Celem.Thm ("not_false",@{thm not_false})
1.63 + Rule.Thm ("not_true", TermC.num_str @{thm not_true}),
1.64 + Rule.Thm ("not_false",@{thm not_false})
1.65 ],
1.66 - scr = Celem.EmptyScr},
1.67 - srls = Celem.Erls, calc = [], errpatts = [],
1.68 + scr = Rule.EmptyScr},
1.69 + srls = Rule.Erls, calc = [], errpatts = [],
1.70 rules = [
1.71 - Celem.Thm ("integral_const", TermC.num_str @{thm integral_const}),
1.72 - Celem.Thm ("integral_var", TermC.num_str @{thm integral_var}),
1.73 - Celem.Thm ("integral_add", TermC.num_str @{thm integral_add}),
1.74 - Celem.Thm ("integral_mult", TermC.num_str @{thm integral_mult}),
1.75 - Celem.Thm ("integral_pow", TermC.num_str @{thm integral_pow}),
1.76 - Celem.Calc ("Groups.plus_class.plus", eval_binop "#add_")(*for n+1*)
1.77 + Rule.Thm ("integral_const", TermC.num_str @{thm integral_const}),
1.78 + Rule.Thm ("integral_var", TermC.num_str @{thm integral_var}),
1.79 + Rule.Thm ("integral_add", TermC.num_str @{thm integral_add}),
1.80 + Rule.Thm ("integral_mult", TermC.num_str @{thm integral_mult}),
1.81 + Rule.Thm ("integral_pow", TermC.num_str @{thm integral_pow}),
1.82 + Rule.Calc ("Groups.plus_class.plus", eval_binop "#add_")(*for n+1*)
1.83 ],
1.84 - scr = Celem.EmptyScr};
1.85 + scr = Rule.EmptyScr};
1.86 *}
1.87 ML {*
1.88 val add_new_c =
1.89 - Celem.Seq {id="add_new_c", preconds = [],
1.90 + Rule.Seq {id="add_new_c", preconds = [],
1.91 rew_ord = ("termlessI",termlessI),
1.92 - erls = Celem.Rls {id="conditions_in_add_new_c",
1.93 + erls = Rule.Rls {id="conditions_in_add_new_c",
1.94 preconds = [],
1.95 rew_ord = ("termlessI",termlessI),
1.96 - erls = Celem.Erls,
1.97 - srls = Celem.Erls, calc = [], errpatts = [],
1.98 - rules = [Celem.Calc ("Tools.matches", eval_matches""),
1.99 - Celem.Calc ("Integrate.is'_f'_x",
1.100 + erls = Rule.Erls,
1.101 + srls = Rule.Erls, calc = [], errpatts = [],
1.102 + rules = [Rule.Calc ("Tools.matches", eval_matches""),
1.103 + Rule.Calc ("Integrate.is'_f'_x",
1.104 eval_is_f_x "is_f_x_"),
1.105 - Celem.Thm ("not_true", TermC.num_str @{thm not_true}),
1.106 - Celem.Thm ("not_false", TermC.num_str @{thm not_false})
1.107 + Rule.Thm ("not_true", TermC.num_str @{thm not_true}),
1.108 + Rule.Thm ("not_false", TermC.num_str @{thm not_false})
1.109 ],
1.110 - scr = Celem.EmptyScr},
1.111 - srls = Celem.Erls, calc = [], errpatts = [],
1.112 - rules = [ (*Celem.Thm ("call_for_new_c", TermC.num_str @{thm call_for_new_c}),*)
1.113 - Celem.Cal1 ("Integrate.add'_new'_c", eval_add_new_c "new_c_")
1.114 + scr = Rule.EmptyScr},
1.115 + srls = Rule.Erls, calc = [], errpatts = [],
1.116 + rules = [ (*Rule.Thm ("call_for_new_c", TermC.num_str @{thm call_for_new_c}),*)
1.117 + Rule.Cal1 ("Integrate.add'_new'_c", eval_add_new_c "new_c_")
1.118 ],
1.119 - scr = Celem.EmptyScr};
1.120 + scr = Rule.EmptyScr};
1.121 *}
1.122 ML {*
1.123
1.124 @@ -169,61 +169,61 @@
1.125
1.126 (*.for simplify_Integral adapted from 'norm_Rational_rls'.*)
1.127 val norm_Rational_rls_noadd_fractions =
1.128 -Celem.Rls {id = "norm_Rational_rls_noadd_fractions", preconds = [],
1.129 - rew_ord = ("dummy_ord",Celem.dummy_ord),
1.130 - erls = norm_rat_erls, srls = Celem.Erls, calc = [], errpatts = [],
1.131 - rules = [(*Celem.Rls_ add_fractions_p_rls,!!!*)
1.132 - Celem.Rls_ (*rat_mult_div_pow original corrected WN051028*)
1.133 - (Celem.Rls {id = "rat_mult_div_pow", preconds = [],
1.134 - rew_ord = ("dummy_ord",Celem.dummy_ord),
1.135 - erls = (*FIXME.WN051028 Celem.e_rls,*)
1.136 - Celem.append_rls "Celem.e_rls-is_polyexp" Celem.e_rls
1.137 - [Celem.Calc ("Poly.is'_polyexp",
1.138 +Rule.Rls {id = "norm_Rational_rls_noadd_fractions", preconds = [],
1.139 + rew_ord = ("dummy_ord",Rule.dummy_ord),
1.140 + erls = norm_rat_erls, srls = Rule.Erls, calc = [], errpatts = [],
1.141 + rules = [(*Rule.Rls_ add_fractions_p_rls,!!!*)
1.142 + Rule.Rls_ (*rat_mult_div_pow original corrected WN051028*)
1.143 + (Rule.Rls {id = "rat_mult_div_pow", preconds = [],
1.144 + rew_ord = ("dummy_ord",Rule.dummy_ord),
1.145 + erls = (*FIXME.WN051028 Rule.e_rls,*)
1.146 + Rule.append_rls "Rule.e_rls-is_polyexp" Rule.e_rls
1.147 + [Rule.Calc ("Poly.is'_polyexp",
1.148 eval_is_polyexp "")],
1.149 - srls = Celem.Erls, calc = [], errpatts = [],
1.150 - rules = [Celem.Thm ("rat_mult", TermC.num_str @{thm rat_mult}),
1.151 + srls = Rule.Erls, calc = [], errpatts = [],
1.152 + rules = [Rule.Thm ("rat_mult", TermC.num_str @{thm rat_mult}),
1.153 (*"?a / ?b * (?c / ?d) = ?a * ?c / (?b * ?d)"*)
1.154 - Celem.Thm ("rat_mult_poly_l", TermC.num_str @{thm rat_mult_poly_l}),
1.155 + Rule.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 - Celem.Thm ("rat_mult_poly_r", TermC.num_str @{thm rat_mult_poly_r}),
1.158 + Rule.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 - Celem.Thm ("real_divide_divide1_mg",
1.162 + Rule.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 - Celem.Thm ("divide_divide_eq_right",
1.166 + Rule.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 - Celem.Thm ("divide_divide_eq_left",
1.170 + Rule.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 - Celem.Calc ("Rings.divide_class.divide" ,eval_cancel "#divide_e"),
1.174 + Rule.Calc ("Rings.divide_class.divide" ,eval_cancel "#divide_e"),
1.175
1.176 - Celem.Thm ("rat_power", TermC.num_str @{thm rat_power})
1.177 + Rule.Thm ("rat_power", TermC.num_str @{thm rat_power})
1.178 (*"(?a / ?b) ^^^ ?n = ?a ^^^ ?n / ?b ^^^ ?n"*)
1.179 ],
1.180 - scr = Celem.Prog ((Thm.term_of o the o (TermC.parse thy)) "empty_script")
1.181 + scr = Rule.Prog ((Thm.term_of o the o (TermC.parse thy)) "empty_script")
1.182 }),
1.183 - Celem.Rls_ make_rat_poly_with_parentheses,
1.184 - Celem.Rls_ cancel_p_rls,(*FIXME:cancel_p does NOT order sometimes*)
1.185 - Celem.Rls_ rat_reduce_1
1.186 + Rule.Rls_ make_rat_poly_with_parentheses,
1.187 + Rule.Rls_ cancel_p_rls,(*FIXME:cancel_p does NOT order sometimes*)
1.188 + Rule.Rls_ rat_reduce_1
1.189 ],
1.190 - scr = Celem.Prog ((Thm.term_of o the o (TermC.parse thy)) "empty_script")
1.191 + scr = Rule.Prog ((Thm.term_of o the o (TermC.parse thy)) "empty_script")
1.192 };
1.193
1.194 (*.for simplify_Integral adapted from 'norm_Rational'.*)
1.195 val norm_Rational_noadd_fractions =
1.196 - Celem.Seq {id = "norm_Rational_noadd_fractions", preconds = [],
1.197 - rew_ord = ("dummy_ord",Celem.dummy_ord),
1.198 - erls = norm_rat_erls, srls = Celem.Erls, calc = [], errpatts = [],
1.199 - rules = [Celem.Rls_ discard_minus,
1.200 - Celem.Rls_ rat_mult_poly,(* removes double fractions like a/b/c *)
1.201 - Celem.Rls_ make_rat_poly_with_parentheses, (*WN0510 also in(#)below*)
1.202 - Celem.Rls_ cancel_p_rls, (*FIXME.MG:cancel_p does NOT order sometim*)
1.203 - Celem.Rls_ norm_Rational_rls_noadd_fractions,(* the main rls (#) *)
1.204 - Celem.Rls_ discard_parentheses1 (* mult only *)
1.205 + Rule.Seq {id = "norm_Rational_noadd_fractions", preconds = [],
1.206 + rew_ord = ("dummy_ord",Rule.dummy_ord),
1.207 + erls = norm_rat_erls, srls = Rule.Erls, calc = [], errpatts = [],
1.208 + rules = [Rule.Rls_ discard_minus,
1.209 + Rule.Rls_ rat_mult_poly,(* removes double fractions like a/b/c *)
1.210 + Rule.Rls_ make_rat_poly_with_parentheses, (*WN0510 also in(#)below*)
1.211 + Rule.Rls_ cancel_p_rls, (*FIXME.MG:cancel_p does NOT order sometim*)
1.212 + Rule.Rls_ norm_Rational_rls_noadd_fractions,(* the main rls (#) *)
1.213 + Rule.Rls_ discard_parentheses1 (* mult only *)
1.214 ],
1.215 - scr = Celem.Prog ((Thm.term_of o the o (TermC.parse thy)) "empty_script")
1.216 + scr = Rule.Prog ((Thm.term_of o the o (TermC.parse thy)) "empty_script")
1.217 };
1.218
1.219 (*.simplify terms before and after Integration such that
1.220 @@ -233,37 +233,37 @@
1.221 *1* expand the term, ie. distribute * and / over +
1.222 .*)
1.223 val separate_bdv2 =
1.224 - Celem.append_rls "separate_bdv2"
1.225 + Rule.append_rls "separate_bdv2"
1.226 collect_bdv
1.227 - [Celem.Thm ("separate_bdv", TermC.num_str @{thm separate_bdv}),
1.228 + [Rule.Thm ("separate_bdv", TermC.num_str @{thm separate_bdv}),
1.229 (*"?a * ?bdv / ?b = ?a / ?b * ?bdv"*)
1.230 - Celem.Thm ("separate_bdv_n", TermC.num_str @{thm separate_bdv_n}),
1.231 - Celem.Thm ("separate_1_bdv", TermC.num_str @{thm separate_1_bdv}),
1.232 + Rule.Thm ("separate_bdv_n", TermC.num_str @{thm separate_bdv_n}),
1.233 + Rule.Thm ("separate_1_bdv", TermC.num_str @{thm separate_1_bdv}),
1.234 (*"?bdv / ?b = (1 / ?b) * ?bdv"*)
1.235 - Celem.Thm ("separate_1_bdv_n", TermC.num_str @{thm separate_1_bdv_n})(*,
1.236 + Rule.Thm ("separate_1_bdv_n", TermC.num_str @{thm separate_1_bdv_n})(*,
1.237 (*"?bdv ^^^ ?n / ?b = 1 / ?b * ?bdv ^^^ ?n"*)
1.238 - *****Celem.Thm ("add_divide_distrib",
1.239 + *****Rule.Thm ("add_divide_distrib",
1.240 ***** TermC.num_str @{thm add_divide_distrib})
1.241 (*"(?x + ?y) / ?z = ?x / ?z + ?y / ?z"*)----------*)
1.242 ];
1.243 val simplify_Integral =
1.244 - Celem.Seq {id = "simplify_Integral", preconds = []:term list,
1.245 - rew_ord = ("dummy_ord", Celem.dummy_ord),
1.246 - erls = Atools_erls, srls = Celem.Erls,
1.247 + Rule.Seq {id = "simplify_Integral", preconds = []:term list,
1.248 + rew_ord = ("dummy_ord", Rule.dummy_ord),
1.249 + erls = Atools_erls, srls = Rule.Erls,
1.250 calc = [], errpatts = [],
1.251 - rules = [Celem.Thm ("distrib_right", TermC.num_str @{thm distrib_right}),
1.252 + rules = [Rule.Thm ("distrib_right", TermC.num_str @{thm distrib_right}),
1.253 (*"(?z1.0 + ?z2.0) * ?w = ?z1.0 * ?w + ?z2.0 * ?w"*)
1.254 - Celem.Thm ("add_divide_distrib", TermC.num_str @{thm add_divide_distrib}),
1.255 + Rule.Thm ("add_divide_distrib", TermC.num_str @{thm add_divide_distrib}),
1.256 (*"(?x + ?y) / ?z = ?x / ?z + ?y / ?z"*)
1.257 (*^^^^^ *1* ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^*)
1.258 - Celem.Rls_ norm_Rational_noadd_fractions,
1.259 - Celem.Rls_ order_add_mult_in,
1.260 - Celem.Rls_ discard_parentheses,
1.261 - (*Celem.Rls_ collect_bdv, from make_polynomial_in*)
1.262 - Celem.Rls_ separate_bdv2,
1.263 - Celem.Calc ("Rings.divide_class.divide" ,eval_cancel "#divide_e")
1.264 + Rule.Rls_ norm_Rational_noadd_fractions,
1.265 + Rule.Rls_ order_add_mult_in,
1.266 + Rule.Rls_ discard_parentheses,
1.267 + (*Rule.Rls_ collect_bdv, from make_polynomial_in*)
1.268 + Rule.Rls_ separate_bdv2,
1.269 + Rule.Calc ("Rings.divide_class.divide" ,eval_cancel "#divide_e")
1.270 ],
1.271 - scr = Celem.EmptyScr};
1.272 + scr = Rule.EmptyScr};
1.273
1.274
1.275 (*simplify terms before and after Integration such that
1.276 @@ -273,54 +273,54 @@
1.277 'make_ratpoly_in'
1.278 THIS IS KEPT FOR COMPARISON ............................................
1.279 * val simplify_Integral = prep_rls'(
1.280 -* Celem.Seq {id = "", preconds = []:term list,
1.281 -* rew_ord = ("dummy_ord", Celem.dummy_ord),
1.282 -* erls = Atools_erls, srls = Celem.Erls,
1.283 +* Rule.Seq {id = "", preconds = []:term list,
1.284 +* rew_ord = ("dummy_ord", Rule.dummy_ord),
1.285 +* erls = Atools_erls, srls = Rule.Erls,
1.286 * calc = [], (*asm_thm = [],*)
1.287 -* rules = [Celem.Rls_ expand_poly,
1.288 -* Celem.Rls_ order_add_mult_in,
1.289 -* Celem.Rls_ simplify_power,
1.290 -* Celem.Rls_ collect_numerals,
1.291 -* Celem.Rls_ reduce_012,
1.292 -* Celem.Thm ("realpow_oneI", TermC.num_str @{thm realpow_oneI}),
1.293 -* Celem.Rls_ discard_parentheses,
1.294 -* Celem.Rls_ collect_bdv,
1.295 +* rules = [Rule.Rls_ expand_poly,
1.296 +* Rule.Rls_ order_add_mult_in,
1.297 +* Rule.Rls_ simplify_power,
1.298 +* Rule.Rls_ collect_numerals,
1.299 +* Rule.Rls_ reduce_012,
1.300 +* Rule.Thm ("realpow_oneI", TermC.num_str @{thm realpow_oneI}),
1.301 +* Rule.Rls_ discard_parentheses,
1.302 +* Rule.Rls_ collect_bdv,
1.303 * (*below inserted from 'make_ratpoly_in'*)
1.304 -* Celem.Rls_ (Celem.append_rls "separate_bdv"
1.305 +* Rule.Rls_ (Rule.append_rls "separate_bdv"
1.306 * collect_bdv
1.307 -* [Celem.Thm ("separate_bdv", TermC.num_str @{thm separate_bdv}),
1.308 +* [Rule.Thm ("separate_bdv", TermC.num_str @{thm separate_bdv}),
1.309 * (*"?a * ?bdv / ?b = ?a / ?b * ?bdv"*)
1.310 -* Celem.Thm ("separate_bdv_n", TermC.num_str @{thm separate_bdv_n}),
1.311 -* Celem.Thm ("separate_1_bdv", TermC.num_str @{thm separate_1_bdv}),
1.312 +* Rule.Thm ("separate_bdv_n", TermC.num_str @{thm separate_bdv_n}),
1.313 +* Rule.Thm ("separate_1_bdv", TermC.num_str @{thm separate_1_bdv}),
1.314 * (*"?bdv / ?b = (1 / ?b) * ?bdv"*)
1.315 -* Celem.Thm ("separate_1_bdv_n", TermC.num_str @{thm separate_1_bdv_n})(*,
1.316 +* Rule.Thm ("separate_1_bdv_n", TermC.num_str @{thm separate_1_bdv_n})(*,
1.317 * (*"?bdv ^^^ ?n / ?b = 1 / ?b * ?bdv ^^^ ?n"*)
1.318 -* Celem.Thm ("add_divide_distrib",
1.319 +* Rule.Thm ("add_divide_distrib",
1.320 * TermC.num_str @{thm add_divide_distrib})
1.321 * (*"(?x + ?y) / ?z = ?x / ?z + ?y / ?z"*)*)
1.322 * ]),
1.323 -* Celem.Calc ("Rings.divide_class.divide" ,eval_cancel "#divide_e")
1.324 +* Rule.Calc ("Rings.divide_class.divide" ,eval_cancel "#divide_e")
1.325 * ],
1.326 -* scr = Celem.EmptyScr
1.327 +* scr = Rule.EmptyScr
1.328 * });
1.329 .......................................................................*)
1.330
1.331 val integration =
1.332 - Celem.Seq {id="integration", preconds = [],
1.333 + Rule.Seq {id="integration", preconds = [],
1.334 rew_ord = ("termlessI",termlessI),
1.335 - erls = Celem.Rls {id="conditions_in_integration",
1.336 + erls = Rule.Rls {id="conditions_in_integration",
1.337 preconds = [],
1.338 rew_ord = ("termlessI",termlessI),
1.339 - erls = Celem.Erls,
1.340 - srls = Celem.Erls, calc = [], errpatts = [],
1.341 + erls = Rule.Erls,
1.342 + srls = Rule.Erls, calc = [], errpatts = [],
1.343 rules = [],
1.344 - scr = Celem.EmptyScr},
1.345 - srls = Celem.Erls, calc = [], errpatts = [],
1.346 - rules = [ Celem.Rls_ integration_rules,
1.347 - Celem.Rls_ add_new_c,
1.348 - Celem.Rls_ simplify_Integral
1.349 + scr = Rule.EmptyScr},
1.350 + srls = Rule.Erls, calc = [], errpatts = [],
1.351 + rules = [ Rule.Rls_ integration_rules,
1.352 + Rule.Rls_ add_new_c,
1.353 + Rule.Rls_ simplify_Integral
1.354 ],
1.355 - scr = Celem.EmptyScr};
1.356 + scr = Rule.EmptyScr};
1.357
1.358 val prep_rls' = LTool.prep_rls @{theory};
1.359 *}
1.360 @@ -342,7 +342,7 @@
1.361 (["integrate","function"],
1.362 [("#Given" ,["functionTerm f_f", "integrateBy v_v"]),
1.363 ("#Find" ,["antiDerivative F_F"])],
1.364 - Celem.append_rls "e_rls" Celem.e_rls [(*for preds in where_*)],
1.365 + Rule.append_rls "e_rls" Rule.e_rls [(*for preds in where_*)],
1.366 SOME "Integrate (f_f, v_v)",
1.367 [["diff","integration"]])),
1.368 (*here "named" is used differently from Differentiation"*)
1.369 @@ -350,7 +350,7 @@
1.370 (["named","integrate","function"],
1.371 [("#Given" ,["functionTerm f_f", "integrateBy v_v"]),
1.372 ("#Find" ,["antiDerivativeName F_F"])],
1.373 - Celem.append_rls "e_rls" Celem.e_rls [(*for preds in where_*)],
1.374 + Rule.append_rls "e_rls" Rule.e_rls [(*for preds in where_*)],
1.375 SOME "Integrate (f_f, v_v)",
1.376 [["diff","integration","named"]]))] *}
1.377
1.378 @@ -359,8 +359,8 @@
1.379 [Specify.prep_met thy "met_diffint" [] Celem.e_metID
1.380 (["diff","integration"],
1.381 [("#Given" ,["functionTerm f_f", "integrateBy v_v"]), ("#Find" ,["antiDerivative F_F"])],
1.382 - {rew_ord'="tless_true", rls'=Atools_erls, calc = [], srls = Celem.e_rls, prls=Celem.e_rls,
1.383 - crls = Atools_erls, errpats = [], nrls = Celem.e_rls},
1.384 + {rew_ord'="tless_true", rls'=Atools_erls, calc = [], srls = Rule.e_rls, prls=Rule.e_rls,
1.385 + crls = Atools_erls, errpats = [], nrls = Rule.e_rls},
1.386 "Script IntegrationScript (f_f::real) (v_v::real) = " ^
1.387 " (let t_t = Take (Integral f_f D v_v) " ^
1.388 " in (Rewrite_Set_Inst [(bdv,v_v)] integration False) (t_t::real))"),
1.389 @@ -368,8 +368,8 @@
1.390 (["diff","integration","named"],
1.391 [("#Given" ,["functionTerm f_f", "integrateBy v_v"]),
1.392 ("#Find" ,["antiDerivativeName F_F"])],
1.393 - {rew_ord'="tless_true", rls'=Atools_erls, calc = [], srls = Celem.e_rls, prls=Celem.e_rls,
1.394 - crls = Atools_erls, errpats = [], nrls = Celem.e_rls},
1.395 + {rew_ord'="tless_true", rls'=Atools_erls, calc = [], srls = Rule.e_rls, prls=Rule.e_rls,
1.396 + crls = Atools_erls, errpats = [], nrls = Rule.e_rls},
1.397 "Script NamedIntegrationScript (f_f::real) (v_v::real) (F_F::real=>real) = " ^
1.398 " (let t_t = Take (F_F v_v = Integral f_f D v_v) " ^
1.399 " in ((Try (Rewrite_Set_Inst [(bdv,v_v)] simplify_Integral False)) @@ " ^