1.1 --- a/src/Tools/isac/Knowledge/Poly.thy Thu Aug 29 13:52:47 2019 +0200
1.2 +++ b/src/Tools/isac/Knowledge/Poly.thy Tue Sep 03 12:40:27 2019 +0200
1.3 @@ -180,7 +180,7 @@
1.4 val poly_consts =
1.5 ["Groups.plus_class.plus", "Groups.minus_class.minus",
1.6 "Rings.divide_class.divide", "Groups.times_class.times",
1.7 - "Atools.pow"];
1.8 + "Prog_Expr.pow"];
1.9 \<close>
1.10 subsubsection \<open>for predicates in specifications (ML)\<close>
1.11 ML \<open>
1.12 @@ -190,16 +190,16 @@
1.13 if (1) then degree 0
1.14 if (2) then v is a factor on the very right, ev. with exponent.*)
1.15 fun factor_right_deg (*case 2*)
1.16 - (Const ("Groups.times_class.times", _) $ t1 $ (Const ("Atools.pow",_) $ vv $ Free (d, _))) v =
1.17 - if vv = v andalso not (occurs_in v t1) then SOME (TermC.int_of_str d) else NONE
1.18 - | factor_right_deg (Const ("Atools.pow",_) $ vv $ Free (d,_)) v =
1.19 + (Const ("Groups.times_class.times", _) $ t1 $ (Const ("Prog_Expr.pow",_) $ vv $ Free (d, _))) v =
1.20 + if vv = v andalso not (Prog_Expr.occurs_in v t1) then SOME (TermC.int_of_str d) else NONE
1.21 + | factor_right_deg (Const ("Prog_Expr.pow",_) $ vv $ Free (d,_)) v =
1.22 if (vv = v) then SOME (TermC.int_of_str d) else NONE
1.23 | factor_right_deg (Const ("Groups.times_class.times",_) $ t1 $ vv) v =
1.24 - if vv = v andalso not (occurs_in v t1) then SOME 1 else NONE
1.25 + if vv = v andalso not (Prog_Expr.occurs_in v t1) then SOME 1 else NONE
1.26 | factor_right_deg vv v =
1.27 if (vv = v) then SOME 1 else NONE;
1.28 fun mono_deg_in m v = (*case 1*)
1.29 - if not (occurs_in v m) then (*case 1*) SOME 0 else factor_right_deg m v;
1.30 + if not (Prog_Expr.occurs_in v m) then (*case 1*) SOME 0 else factor_right_deg m v;
1.31
1.32 fun expand_deg_in t v =
1.33 let
1.34 @@ -266,15 +266,15 @@
1.35 | monom2list t = [t];
1.36
1.37 (* liefert Variablenname (String) einer Variablen und Basis bei Potenz *)
1.38 -fun get_basStr (Const ("Atools.pow",_) $ Free (str, _) $ _) = str
1.39 +fun get_basStr (Const ("Prog_Expr.pow",_) $ Free (str, _) $ _) = str
1.40 | get_basStr (Free (str, _)) = str
1.41 | get_basStr _ = "|||"; (* gross gewichtet; für Brüch ect. *)
1.42 (*| get_basStr t =
1.43 error("get_basStr: called with t= "^(Rule.term2str t));*)
1.44
1.45 (* liefert Hochzahl (String) einer Variablen bzw Gewichtstring (zum Sortieren) *)
1.46 -fun get_potStr (Const ("Atools.pow",_) $ Free _ $ Free (str, _)) = str
1.47 - | get_potStr (Const ("Atools.pow",_) $ Free _ $ _ ) = "|||" (* gross gewichtet *)
1.48 +fun get_potStr (Const ("Prog_Expr.pow",_) $ Free _ $ Free (str, _)) = str
1.49 + | get_potStr (Const ("Prog_Expr.pow",_) $ Free _ $ _ ) = "|||" (* gross gewichtet *)
1.50 | get_potStr (Free (_, _)) = "---" (* keine Hochzahl --> kleinst gewichtet *)
1.51 | get_potStr _ = "||||||"; (* gross gewichtet; für Brüch ect. *)
1.52 (*| get_potStr t =
1.53 @@ -330,11 +330,11 @@
1.54 counter (n, xs)
1.55 else
1.56 (case x of
1.57 - (Const ("Atools.pow", _) $ Free _ $ Free (str_h, T)) =>
1.58 + (Const ("Prog_Expr.pow", _) $ Free _ $ Free (str_h, T)) =>
1.59 if (is_nums (Free (str_h, T))) then
1.60 counter (n + (the (TermC.int_of_str_opt str_h)), xs)
1.61 else counter (n + 1000, xs) (*FIXME.MG?!*)
1.62 - | (Const ("Atools.pow", _) $ Free _ $ _ ) =>
1.63 + | (Const ("Prog_Expr.pow", _) $ Free _ $ _ ) =>
1.64 counter (n + 1000, xs) (*FIXME.MG?!*)
1.65 | (Free _) => counter (n + 1, xs)
1.66 (*| _ => error("monom_degree: called with factor: "^(Rule.term2str x)))*)
1.67 @@ -460,7 +460,7 @@
1.68
1.69 fun dest_hd' (Const (a, T)) = (* ~ term.ML *)
1.70 (case a of
1.71 - "Atools.pow" => ((("|||||||||||||", 0), T), 0) (*WN greatest string*)
1.72 + "Prog_Expr.pow" => ((("|||||||||||||", 0), T), 0) (*WN greatest string*)
1.73 | _ => (((a, 0), T), 0))
1.74 | dest_hd' (Free (a, T)) = (((a, 0), T), 1)
1.75 | dest_hd' (Var v) = (v, 2)
1.76 @@ -469,7 +469,7 @@
1.77 | dest_hd' t = raise TERM ("dest_hd'", [t]);
1.78
1.79 fun size_of_term' (Const(str,_) $ t) =
1.80 - if "Atools.pow"= str then 1000 + size_of_term' t else 1+size_of_term' t(*WN*)
1.81 + if "Prog_Expr.pow"= str then 1000 + size_of_term' t else 1+size_of_term' t(*WN*)
1.82 | size_of_term' (Abs (_,_,body)) = 1 + size_of_term' body
1.83 | size_of_term' (f$t) = size_of_term' f + size_of_term' t
1.84 | size_of_term' _ = 1;
1.85 @@ -522,7 +522,7 @@
1.86 let
1.87 fun finddivide (_ $ _ $ _ $ _) _ = error("is_polyrat_in:")
1.88 (* at the moment there is no term like this, but ....*)
1.89 - | finddivide (Const ("Rings.divide_class.divide",_) $ _ $ b) v = not (occurs_in v b)
1.90 + | finddivide (Const ("Rings.divide_class.divide",_) $ _ $ b) v = not (Prog_Expr.occurs_in v b)
1.91 | finddivide (_ $ t1 $ t2) v = finddivide t1 v orelse finddivide t2 v
1.92 | finddivide (_ $ t1) v = finddivide t1 v
1.93 | finddivide _ _ = false;
1.94 @@ -539,14 +539,14 @@
1.95 | is_polyexp (Const ("Groups.plus_class.plus",_) $ Free _ $ Free _) = true
1.96 | is_polyexp (Const ("Groups.minus_class.minus",_) $ Free _ $ Free _) = true
1.97 | is_polyexp (Const ("Groups.times_class.times",_) $ Free _ $ Free _) = true
1.98 - | is_polyexp (Const ("Atools.pow",_) $ Free _ $ Free _) = true
1.99 + | is_polyexp (Const ("Prog_Expr.pow",_) $ Free _ $ Free _) = true
1.100 | is_polyexp (Const ("Groups.plus_class.plus",_) $ t1 $ t2) =
1.101 ((is_polyexp t1) andalso (is_polyexp t2))
1.102 | is_polyexp (Const ("Groups.minus_class.minus",_) $ t1 $ t2) =
1.103 ((is_polyexp t1) andalso (is_polyexp t2))
1.104 | is_polyexp (Const ("Groups.times_class.times",_) $ t1 $ t2) =
1.105 ((is_polyexp t1) andalso (is_polyexp t2))
1.106 - | is_polyexp (Const ("Atools.pow",_) $ t1 $ t2) =
1.107 + | is_polyexp (Const ("Prog_Expr.pow",_) $ t1 $ t2) =
1.108 ((is_polyexp t1) andalso (is_polyexp t2))
1.109 | is_polyexp _ = false;
1.110 \<close>
1.111 @@ -652,20 +652,20 @@
1.112
1.113 (*.for evaluation of conditions in rewrite rules.*)
1.114 val Poly_erls = Rule.append_rls "Poly_erls" Atools_erls
1.115 - [Rule.Calc ("HOL.eq", eval_equal "#equal_"),
1.116 + [Rule.Calc ("HOL.eq", Prog_Expr.eval_equal "#equal_"),
1.117 Rule.Thm ("real_unari_minus", TermC.num_str @{thm real_unari_minus}),
1.118 - Rule.Calc ("Groups.plus_class.plus", eval_binop "#add_"),
1.119 - Rule.Calc ("Groups.minus_class.minus", eval_binop "#sub_"),
1.120 - Rule.Calc ("Groups.times_class.times", eval_binop "#mult_"),
1.121 - Rule.Calc ("Atools.pow", eval_binop "#power_")];
1.122 + Rule.Calc ("Groups.plus_class.plus", (**)eval_binop "#add_"),
1.123 + Rule.Calc ("Groups.minus_class.minus", (**)eval_binop "#sub_"),
1.124 + Rule.Calc ("Groups.times_class.times", (**)eval_binop "#mult_"),
1.125 + Rule.Calc ("Prog_Expr.pow", (**)eval_binop "#power_")];
1.126
1.127 val poly_crls = Rule.append_rls "poly_crls" Atools_crls
1.128 - [Rule.Calc ("HOL.eq", eval_equal "#equal_"),
1.129 + [Rule.Calc ("HOL.eq", Prog_Expr.eval_equal "#equal_"),
1.130 Rule.Thm ("real_unari_minus", TermC.num_str @{thm real_unari_minus}),
1.131 - Rule.Calc ("Groups.plus_class.plus", eval_binop "#add_"),
1.132 - Rule.Calc ("Groups.minus_class.minus", eval_binop "#sub_"),
1.133 - Rule.Calc ("Groups.times_class.times", eval_binop "#mult_"),
1.134 - Rule.Calc ("Atools.pow" ,eval_binop "#power_")];
1.135 + Rule.Calc ("Groups.plus_class.plus", (**)eval_binop "#add_"),
1.136 + Rule.Calc ("Groups.minus_class.minus", (**)eval_binop "#sub_"),
1.137 + Rule.Calc ("Groups.times_class.times", (**)eval_binop "#mult_"),
1.138 + Rule.Calc ("Prog_Expr.pow" , (**)eval_binop "#power_")];
1.139 \<close>
1.140 ML \<open>
1.141 val expand =
1.142 @@ -798,14 +798,14 @@
1.143 Rule.Rls{id = "calc_add_mult_pow_", preconds = [],
1.144 rew_ord = ("dummy_ord", Rule.dummy_ord),
1.145 erls = Atools_erls(*erls3.4.03*),srls = Rule.Erls,
1.146 - calc = [("PLUS" , ("Groups.plus_class.plus", eval_binop "#add_")),
1.147 - ("TIMES" , ("Groups.times_class.times", eval_binop "#mult_")),
1.148 - ("POWER", ("Atools.pow", eval_binop "#power_"))
1.149 + calc = [("PLUS" , ("Groups.plus_class.plus", (**)eval_binop "#add_")),
1.150 + ("TIMES" , ("Groups.times_class.times", (**)eval_binop "#mult_")),
1.151 + ("POWER", ("Prog_Expr.pow", (**)eval_binop "#power_"))
1.152 ],
1.153 errpatts = [],
1.154 - rules = [Rule.Calc ("Groups.plus_class.plus", eval_binop "#add_"),
1.155 - Rule.Calc ("Groups.times_class.times", eval_binop "#mult_"),
1.156 - Rule.Calc ("Atools.pow", eval_binop "#power_")
1.157 + rules = [Rule.Calc ("Groups.plus_class.plus", (**)eval_binop "#add_"),
1.158 + Rule.Calc ("Groups.times_class.times", (**)eval_binop "#mult_"),
1.159 + Rule.Calc ("Prog_Expr.pow", (**)eval_binop "#power_")
1.160 ], scr = Rule.EmptyScr};
1.161
1.162 val reduce_012_mult_ =
1.163 @@ -828,7 +828,7 @@
1.164 Rule.Rls{id = "collect_numerals_", preconds = [],
1.165 rew_ord = ("dummy_ord", Rule.dummy_ord),
1.166 erls = Atools_erls, srls = Rule.Erls,
1.167 - calc = [("PLUS" , ("Groups.plus_class.plus", eval_binop "#add_"))
1.168 + calc = [("PLUS" , ("Groups.plus_class.plus", (**)eval_binop "#add_"))
1.169 ], errpatts = [],
1.170 rules =
1.171 [Rule.Thm ("real_num_collect",TermC.num_str @{thm real_num_collect}),
1.172 @@ -841,7 +841,7 @@
1.173 Rule.Thm ("real_one_collect_assoc_r",TermC.num_str @{thm real_one_collect_assoc_r}),
1.174 (*"m is_const ==> (k + n) + m * n = k + (m + 1) * n"*)
1.175
1.176 - Rule.Calc ("Groups.plus_class.plus", eval_binop "#add_"),
1.177 + Rule.Calc ("Groups.plus_class.plus", (**)eval_binop "#add_"),
1.178
1.179 (*MG: Reihenfolge der folgenden 2 Rule.Thm muss so bleiben, wegen
1.180 (a+a)+a --> a + 2*a --> 3*a and not (a+a)+a --> 2*a + a *)
1.181 @@ -949,9 +949,9 @@
1.182 Rule.Rls{id = "collect_numerals", preconds = [],
1.183 rew_ord = ("dummy_ord", Rule.dummy_ord),
1.184 erls = Atools_erls(*erls3.4.03*),srls = Rule.Erls,
1.185 - calc = [("PLUS" , ("Groups.plus_class.plus", eval_binop "#add_")),
1.186 - ("TIMES" , ("Groups.times_class.times", eval_binop "#mult_")),
1.187 - ("POWER", ("Atools.pow", eval_binop "#power_"))
1.188 + calc = [("PLUS" , ("Groups.plus_class.plus", (**)eval_binop "#add_")),
1.189 + ("TIMES" , ("Groups.times_class.times", (**)eval_binop "#mult_")),
1.190 + ("POWER", ("Prog_Expr.pow", (**)eval_binop "#power_"))
1.191 ], errpatts = [],
1.192 rules = [Rule.Thm ("real_num_collect",TermC.num_str @{thm real_num_collect}),
1.193 (*"[| l is_const; m is_const |]==>l * n + m * n = (l + m) * n"*)
1.194 @@ -962,9 +962,9 @@
1.195 (*"m is_const ==> n + m * n = (1 + m) * n"*)
1.196 Rule.Thm ("real_one_collect_assoc",TermC.num_str @{thm real_one_collect_assoc}),
1.197 (*"m is_const ==> k + (n + m * n) = k + (1 + m) * n"*)
1.198 - Rule.Calc ("Groups.plus_class.plus", eval_binop "#add_"),
1.199 - Rule.Calc ("Groups.times_class.times", eval_binop "#mult_"),
1.200 - Rule.Calc ("Atools.pow", eval_binop "#power_")
1.201 + Rule.Calc ("Groups.plus_class.plus", (**)eval_binop "#add_"),
1.202 + Rule.Calc ("Groups.times_class.times", (**)eval_binop "#mult_"),
1.203 + Rule.Calc ("Prog_Expr.pow", (**)eval_binop "#power_")
1.204 ], scr = Rule.EmptyScr};
1.205 val reduce_012 =
1.206 Rule.Rls{id = "reduce_012", preconds = [],
1.207 @@ -1059,11 +1059,10 @@
1.208 erls = Rule.append_rls "Rule.e_rls-is_multUnordered" Rule.e_rls
1.209 [Rule.Calc ("Poly.is'_multUnordered",
1.210 eval_is_multUnordered "")],
1.211 - calc = [("PLUS" , ("Groups.plus_class.plus", eval_binop "#add_")),
1.212 - ("TIMES" , ("Groups.times_class.times", eval_binop "#mult_")),
1.213 - ("DIVIDE", ("Rings.divide_class.divide",
1.214 - eval_cancel "#divide_e")),
1.215 - ("POWER" , ("Atools.pow", eval_binop "#power_"))],
1.216 + calc = [("PLUS" , ("Groups.plus_class.plus", (**)eval_binop "#add_")),
1.217 + ("TIMES" , ("Groups.times_class.times", (**)eval_binop "#mult_")),
1.218 + ("DIVIDE", ("Rings.divide_class.divide", Prog_Expr.eval_cancel "#divide_e")),
1.219 + ("POWER" , ("Prog_Expr.pow", (**)eval_binop "#power_"))],
1.220 errpatts = [],
1.221 scr = Rule.Rfuns {init_state = init_state,
1.222 normal_form = normal_form,
1.223 @@ -1098,13 +1097,11 @@
1.224 fuer die Evaluation der Precondition "p is_addUnordered"*))],
1.225 rew_ord = ("dummy_ord", Rule.dummy_ord),
1.226 erls = Rule.append_rls "Rule.e_rls-is_addUnordered" Rule.e_rls(*MG: poly_erls*)
1.227 - [Rule.Calc ("Poly.is'_addUnordered",
1.228 - eval_is_addUnordered "")],
1.229 - calc = [("PLUS" ,("Groups.plus_class.plus", eval_binop "#add_")),
1.230 - ("TIMES" ,("Groups.times_class.times", eval_binop "#mult_")),
1.231 - ("DIVIDE",("Rings.divide_class.divide",
1.232 - eval_cancel "#divide_e")),
1.233 - ("POWER" ,("Atools.pow" ,eval_binop "#power_"))],
1.234 + [Rule.Calc ("Poly.is'_addUnordered", eval_is_addUnordered "")],
1.235 + calc = [("PLUS" ,("Groups.plus_class.plus", (**)eval_binop "#add_")),
1.236 + ("TIMES" ,("Groups.times_class.times", (**)eval_binop "#mult_")),
1.237 + ("DIVIDE",("Rings.divide_class.divide", Prog_Expr.eval_cancel "#divide_e")),
1.238 + ("POWER" ,("Prog_Expr.pow" , (**)eval_binop "#power_"))],
1.239 errpatts = [],
1.240 scr = Rule.Rfuns {init_state = init_state,
1.241 normal_form = normal_form,
1.242 @@ -1138,7 +1135,7 @@
1.243 erls = Atools_erls, srls = Rule.Erls,calc = [], errpatts = [],
1.244 rules = [Rule.Rls_ discard_minus,
1.245 Rule.Rls_ expand_poly_,
1.246 - Rule.Calc ("Groups.times_class.times", eval_binop "#mult_"),
1.247 + Rule.Calc ("Groups.times_class.times", (**)eval_binop "#mult_"),
1.248 Rule.Rls_ order_mult_rls_,
1.249 Rule.Rls_ simplify_power_,
1.250 Rule.Rls_ calc_add_mult_pow_,
1.251 @@ -1158,7 +1155,7 @@
1.252 erls = Atools_erls, srls = Rule.Erls, calc = [], errpatts = [],
1.253 rules = [Rule.Rls_ discard_minus,
1.254 Rule.Rls_ expand_poly_,
1.255 - Rule.Calc ("Groups.times_class.times", eval_binop "#mult_"),
1.256 + Rule.Calc ("Groups.times_class.times", (**)eval_binop "#mult_"),
1.257 Rule.Rls_ order_mult_rls_,
1.258 Rule.Rls_ simplify_power_,
1.259 Rule.Rls_ calc_add_mult_pow_,
1.260 @@ -1181,7 +1178,7 @@
1.261 erls = Atools_erls, srls = Rule.Erls, calc = [], errpatts = [],
1.262 rules = [Rule.Rls_ discard_minus,
1.263 Rule.Rls_ expand_poly_rat_,(*ignors rationals*)
1.264 - Rule.Calc ("Groups.times_class.times", eval_binop "#mult_"),
1.265 + Rule.Calc ("Groups.times_class.times", (**)eval_binop "#mult_"),
1.266 Rule.Rls_ order_mult_rls_,
1.267 Rule.Rls_ simplify_power_,
1.268 Rule.Rls_ calc_add_mult_pow_,
1.269 @@ -1200,9 +1197,9 @@
1.270 val rev_rew_p =
1.271 Rule.Seq{id = "rev_rew_p", preconds = [], rew_ord = ("termlessI",termlessI),
1.272 erls = Atools_erls, srls = Rule.Erls,
1.273 - calc = [(*("PLUS" , ("Groups.plus_class.plus", eval_binop "#add_")),
1.274 - ("TIMES" , ("Groups.times_class.times", eval_binop "#mult_")),
1.275 - ("POWER", ("Atools.pow", eval_binop "#power_"))*)
1.276 + calc = [(*("PLUS" , ("Groups.plus_class.plus", (**)eval_binop "#add_")),
1.277 + ("TIMES" , ("Groups.times_class.times", (**)eval_binop "#mult_")),
1.278 + ("POWER", ("Prog_Expr.pow", (**)eval_binop "#power_"))*)
1.279 ], errpatts = [],
1.280 rules = [Rule.Thm ("real_plus_binom_times" ,TermC.num_str @{thm real_plus_binom_times}),
1.281 (*"(a + b)*(a + b) = a ^ 2 + 2 * a * b + b ^ 2*)
1.282 @@ -1223,9 +1220,9 @@
1.283 Rule.Rls_ order_mult_rls_,
1.284 (*Rule.Rls_ order_add_rls_,*)
1.285
1.286 - Rule.Calc ("Groups.plus_class.plus", eval_binop "#add_"),
1.287 - Rule.Calc ("Groups.times_class.times", eval_binop "#mult_"),
1.288 - Rule.Calc ("Atools.pow", eval_binop "#power_"),
1.289 + Rule.Calc ("Groups.plus_class.plus", (**)eval_binop "#add_"),
1.290 + Rule.Calc ("Groups.times_class.times", (**)eval_binop "#mult_"),
1.291 + Rule.Calc ("Prog_Expr.pow", (**)eval_binop "#power_"),
1.292
1.293 Rule.Thm ("sym_realpow_twoI",
1.294 TermC.num_str (@{thm realpow_twoI} RS @{thm sym})),
1.295 @@ -1249,9 +1246,9 @@
1.296 Rule.Thm ("realpow_multI", TermC.num_str @{thm realpow_multI}),
1.297 (*"(r * s) ^^^ n = r ^^^ n * s ^^^ n"*)
1.298
1.299 - Rule.Calc ("Groups.plus_class.plus", eval_binop "#add_"),
1.300 - Rule.Calc ("Groups.times_class.times", eval_binop "#mult_"),
1.301 - Rule.Calc ("Atools.pow", eval_binop "#power_"),
1.302 + Rule.Calc ("Groups.plus_class.plus", (**)eval_binop "#add_"),
1.303 + Rule.Calc ("Groups.times_class.times", (**)eval_binop "#mult_"),
1.304 + Rule.Calc ("Prog_Expr.pow", (**)eval_binop "#power_"),
1.305
1.306 Rule.Thm ("mult_1_left",TermC.num_str @{thm mult_1_left}),(*"1 * z = z"*)
1.307 Rule.Thm ("mult_zero_left",TermC.num_str @{thm mult_zero_left}),(*"0 * z = 0"*)
1.308 @@ -1302,9 +1299,9 @@
1.309 val expand_binoms =
1.310 Rule.Rls{id = "expand_binoms", preconds = [], rew_ord = ("termlessI",termlessI),
1.311 erls = Atools_erls, srls = Rule.Erls,
1.312 - calc = [("PLUS" , ("Groups.plus_class.plus", eval_binop "#add_")),
1.313 - ("TIMES" , ("Groups.times_class.times", eval_binop "#mult_")),
1.314 - ("POWER", ("Atools.pow", eval_binop "#power_"))
1.315 + calc = [("PLUS" , ("Groups.plus_class.plus", (**)eval_binop "#add_")),
1.316 + ("TIMES" , ("Groups.times_class.times", (**)eval_binop "#mult_")),
1.317 + ("POWER", ("Prog_Expr.pow", (**)eval_binop "#power_"))
1.318 ], errpatts = [],
1.319 rules = [Rule.Thm ("real_plus_binom_pow2",
1.320 TermC.num_str @{thm real_plus_binom_pow2}),
1.321 @@ -1357,9 +1354,9 @@
1.322 (*"0 * z = 0"*)
1.323 Rule.Thm ("add_0_left",TermC.num_str @{thm add_0_left}),(*"0 + z = z"*)
1.324
1.325 - Rule.Calc ("Groups.plus_class.plus", eval_binop "#add_"),
1.326 - Rule.Calc ("Groups.times_class.times", eval_binop "#mult_"),
1.327 - Rule.Calc ("Atools.pow", eval_binop "#power_"),
1.328 + Rule.Calc ("Groups.plus_class.plus", (**)eval_binop "#add_"),
1.329 + Rule.Calc ("Groups.times_class.times", (**)eval_binop "#mult_"),
1.330 + Rule.Calc ("Prog_Expr.pow", (**)eval_binop "#power_"),
1.331 (*Rule.Thm ("mult_commute",TermC.num_str @{thm mult_commute}),
1.332 (*AC-rewriting*)
1.333 Rule.Thm ("real_mult_left_commute",
1.334 @@ -1392,9 +1389,9 @@
1.335 TermC.num_str @{thm real_one_collect_assoc}),
1.336 (*"m is_const ==> k + (n + m * n) = k + (1 + m) * n"*)
1.337
1.338 - Rule.Calc ("Groups.plus_class.plus", eval_binop "#add_"),
1.339 - Rule.Calc ("Groups.times_class.times", eval_binop "#mult_"),
1.340 - Rule.Calc ("Atools.pow", eval_binop "#power_")
1.341 + Rule.Calc ("Groups.plus_class.plus", (**)eval_binop "#add_"),
1.342 + Rule.Calc ("Groups.times_class.times", (**)eval_binop "#mult_"),
1.343 + Rule.Calc ("Prog_Expr.pow", (**)eval_binop "#power_")
1.344 ],
1.345 scr = Rule.Prog (LTool.prep_program @{thm expand_binoms_2.simps})
1.346 };
1.347 @@ -1461,7 +1458,7 @@
1.348 {rew_ord'="tless_true", rls' = Rule.e_rls, calc = [], srls = Rule.e_rls,
1.349 prls = Rule.append_rls "simplification_for_polynomials_prls" Rule.e_rls
1.350 [(*for preds in where_*)
1.351 - Rule.Calc ("Poly.is'_polyexp",eval_is_polyexp"")],
1.352 + Rule.Calc ("Poly.is'_polyexp", eval_is_polyexp"")],
1.353 crls = Rule.e_rls, errpats = [], nrls = norm_Poly},
1.354 @{thm simplify.simps})]
1.355 \<close>