1.1 --- a/src/Tools/isac/Knowledge/Rational.thy Thu Mar 15 10:17:44 2018 +0100
1.2 +++ b/src/Tools/isac/Knowledge/Rational.thy Thu Mar 15 12:42:04 2018 +0100
1.3 @@ -11,7 +11,7 @@
1.4 imports Poly "~~/src/Tools/isac/Knowledge/GCD_Poly_ML"
1.5 begin
1.6
1.7 -section {* Constants for evaluation by "Calc" *}
1.8 +section {* Constants for evaluation by "Celem.Calc" *}
1.9 consts
1.10
1.11 is'_expanded :: "real => bool" ("_ is'_expanded") (*RL->Poly.thy*)
1.12 @@ -43,9 +43,9 @@
1.13 fun eval_is_ratpolyexp (thmid:string) _
1.14 (t as (Const("Rational.is'_ratpolyexp", _) $ arg)) thy =
1.15 if is_ratpolyexp arg
1.16 - then SOME (TermC.mk_thmid thmid (term_to_string''' thy arg) "",
1.17 + then SOME (TermC.mk_thmid thmid (Celem.term_to_string''' thy arg) "",
1.18 HOLogic.Trueprop $ (TermC.mk_equality (t, @{term True})))
1.19 - else SOME (TermC.mk_thmid thmid (term_to_string''' thy arg) "",
1.20 + else SOME (TermC.mk_thmid thmid (Celem.term_to_string''' thy arg) "",
1.21 HOLogic.Trueprop $ (TermC.mk_equality (t, @{term False})))
1.22 | eval_is_ratpolyexp _ _ _ _ = NONE;
1.23
1.24 @@ -54,7 +54,7 @@
1.25 (t as Const ("Rational.get_denominator", _) $
1.26 (Const ("Rings.divide_class.divide", _) $ num $
1.27 denom)) thy =
1.28 - SOME (TermC.mk_thmid thmid (term_to_string''' thy denom) "",
1.29 + SOME (TermC.mk_thmid thmid (Celem.term_to_string''' thy denom) "",
1.30 HOLogic.Trueprop $ (TermC.mk_equality (t, denom)))
1.31 | eval_get_denominator _ _ _ _ = NONE;
1.32
1.33 @@ -63,7 +63,7 @@
1.34 (t as Const ("Rational.get_numerator", _) $
1.35 (Const ("Rings.divide_class.divide", _) $num
1.36 $denom )) thy =
1.37 - SOME (TermC.mk_thmid thmid (term_to_string''' thy num) "",
1.38 + SOME (TermC.mk_thmid thmid (Celem.term_to_string''' thy num) "",
1.39 HOLogic.Trueprop $ (TermC.mk_equality (t, num)))
1.40 | eval_get_numerator _ _ _ _ = NONE;
1.41 *}
1.42 @@ -130,7 +130,7 @@
1.43 | monom_of_term vs (c, es) (Const ("Groups.times_class.times", _) $ m1 $ m2) =
1.44 let val (c', es') = monom_of_term vs (c, es) m1
1.45 in monom_of_term vs (c', es') m2 end
1.46 - | monom_of_term _ _ t = raise ERROR ("poly malformed with " ^ term2str t)
1.47 + | monom_of_term _ _ t = raise ERROR ("poly malformed with " ^ Celem.term2str t)
1.48
1.49 fun monoms_of_term vs (t as Free _) =
1.50 [monom_of_term vs (1, replicate (length vs) 0) t]
1.51 @@ -140,7 +140,7 @@
1.52 [monom_of_term vs (1, replicate (length vs) 0) t]
1.53 | monoms_of_term vs (Const ("Groups.plus_class.plus", _) $ ms1 $ ms2) =
1.54 (monoms_of_term vs ms1) @ (monoms_of_term vs ms2)
1.55 - | monoms_of_term _ t = raise ERROR ("poly malformed with " ^ term2str t)
1.56 + | monoms_of_term _ t = raise ERROR ("poly malformed with " ^ Celem.term2str t)
1.57
1.58 (* convert a term to the internal representation of a multivariate polynomial;
1.59 the conversion is quite liberal, see test --- fun poly_of_term ---:
1.60 @@ -394,70 +394,70 @@
1.61 (* evaluates conditions in calculate_Rational *)
1.62 val calc_rat_erls =
1.63 prep_rls'
1.64 - (Rls {id = "calc_rat_erls", preconds = [], rew_ord = ("dummy_ord", dummy_ord),
1.65 - erls = e_rls, srls = Erls, calc = [], errpatts = [],
1.66 + (Celem.Rls {id = "calc_rat_erls", preconds = [], rew_ord = ("dummy_ord", Celem.dummy_ord),
1.67 + erls = Celem.e_rls, srls = Celem.Erls, calc = [], errpatts = [],
1.68 rules =
1.69 - [Calc ("HOL.eq", eval_equal "#equal_"),
1.70 - Calc ("Atools.is'_const", eval_const "#is_const_"),
1.71 - Thm ("not_true", TermC.num_str @{thm not_true}),
1.72 - Thm ("not_false", TermC.num_str @{thm not_false})],
1.73 - scr = EmptyScr});
1.74 + [Celem.Calc ("HOL.eq", eval_equal "#equal_"),
1.75 + Celem.Calc ("Atools.is'_const", eval_const "#is_const_"),
1.76 + Celem.Thm ("not_true", TermC.num_str @{thm not_true}),
1.77 + Celem.Thm ("not_false", TermC.num_str @{thm not_false})],
1.78 + scr = Celem.EmptyScr});
1.79
1.80 (* simplifies expressions with numerals;
1.81 does NOT rearrange the term by AC-rewriting; thus terms with variables
1.82 need to have constants to be commuted together respectively *)
1.83 val calculate_Rational =
1.84 - prep_rls' (merge_rls "calculate_Rational"
1.85 - (Rls {id = "divide", preconds = [], rew_ord = ("dummy_ord", dummy_ord),
1.86 - erls = calc_rat_erls, srls = Erls,
1.87 + prep_rls' (Celem.merge_rls "calculate_Rational"
1.88 + (Celem.Rls {id = "divide", preconds = [], rew_ord = ("dummy_ord", Celem.dummy_ord),
1.89 + erls = calc_rat_erls, srls = Celem.Erls,
1.90 calc = [], errpatts = [],
1.91 rules =
1.92 - [Calc ("Rings.divide_class.divide", eval_cancel "#divide_e"),
1.93 + [Celem.Calc ("Rings.divide_class.divide", eval_cancel "#divide_e"),
1.94
1.95 - Thm ("minus_divide_left", TermC.num_str (@{thm minus_divide_left} RS @{thm sym})),
1.96 + Celem.Thm ("minus_divide_left", TermC.num_str (@{thm minus_divide_left} RS @{thm sym})),
1.97 (*SYM - ?x / ?y = - (?x / ?y) may come from subst*)
1.98 - Thm ("rat_add", TermC.num_str @{thm rat_add}),
1.99 + Celem.Thm ("rat_add", TermC.num_str @{thm rat_add}),
1.100 (*"[| a is_const; b is_const; c is_const; d is_const |] ==> \
1.101 \a / c + b / d = (a * d) / (c * d) + (b * c ) / (d * c)"*)
1.102 - Thm ("rat_add1", TermC.num_str @{thm rat_add1}),
1.103 + Celem.Thm ("rat_add1", TermC.num_str @{thm rat_add1}),
1.104 (*"[| a is_const; b is_const; c is_const |] ==> a / c + b / c = (a + b) / c"*)
1.105 - Thm ("rat_add2", TermC.num_str @{thm rat_add2}),
1.106 + Celem.Thm ("rat_add2", TermC.num_str @{thm rat_add2}),
1.107 (*"[| ?a is_const; ?b is_const; ?c is_const |] ==> ?a / ?c + ?b = (?a + ?b * ?c) / ?c"*)
1.108 - Thm ("rat_add3", TermC.num_str @{thm rat_add3}),
1.109 + Celem.Thm ("rat_add3", TermC.num_str @{thm rat_add3}),
1.110 (*"[| a is_const; b is_const; c is_const |] ==> a + b / c = (a * c) / c + b / c"\
1.111 .... is_const to be omitted here FIXME*)
1.112
1.113 - Thm ("rat_mult", TermC.num_str @{thm rat_mult}),
1.114 + Celem.Thm ("rat_mult", TermC.num_str @{thm rat_mult}),
1.115 (*a / b * (c / d) = a * c / (b * d)*)
1.116 - Thm ("times_divide_eq_right", TermC.num_str @{thm times_divide_eq_right}),
1.117 + Celem.Thm ("times_divide_eq_right", TermC.num_str @{thm times_divide_eq_right}),
1.118 (*?x * (?y / ?z) = ?x * ?y / ?z*)
1.119 - Thm ("times_divide_eq_left", TermC.num_str @{thm times_divide_eq_left}),
1.120 + Celem.Thm ("times_divide_eq_left", TermC.num_str @{thm times_divide_eq_left}),
1.121 (*?y / ?z * ?x = ?y * ?x / ?z*)
1.122
1.123 - Thm ("real_divide_divide1", TermC.num_str @{thm real_divide_divide1}),
1.124 + Celem.Thm ("real_divide_divide1", TermC.num_str @{thm real_divide_divide1}),
1.125 (*"?y ~= 0 ==> ?u / ?v / (?y / ?z) = ?u / ?v * (?z / ?y)"*)
1.126 - Thm ("divide_divide_eq_left", TermC.num_str @{thm divide_divide_eq_left}),
1.127 + Celem.Thm ("divide_divide_eq_left", TermC.num_str @{thm divide_divide_eq_left}),
1.128 (*"?x / ?y / ?z = ?x / (?y * ?z)"*)
1.129
1.130 - Thm ("rat_power", TermC.num_str @{thm rat_power}),
1.131 + Celem.Thm ("rat_power", TermC.num_str @{thm rat_power}),
1.132 (*"(?a / ?b) ^^^ ?n = ?a ^^^ ?n / ?b ^^^ ?n"*)
1.133
1.134 - Thm ("mult_cross", TermC.num_str @{thm mult_cross}),
1.135 + Celem.Thm ("mult_cross", TermC.num_str @{thm mult_cross}),
1.136 (*"[| b ~= 0; d ~= 0 |] ==> (a / b = c / d) = (a * d = b * c)*)
1.137 - Thm ("mult_cross1", TermC.num_str @{thm mult_cross1}),
1.138 + Celem.Thm ("mult_cross1", TermC.num_str @{thm mult_cross1}),
1.139 (*" b ~= 0 ==> (a / b = c ) = (a = b * c)*)
1.140 - Thm ("mult_cross2", TermC.num_str @{thm mult_cross2})
1.141 + Celem.Thm ("mult_cross2", TermC.num_str @{thm mult_cross2})
1.142 (*" d ~= 0 ==> (a = c / d) = (a * d = c)*)],
1.143 - scr = EmptyScr})
1.144 + scr = Celem.EmptyScr})
1.145 calculate_Poly);
1.146
1.147 (*("is_expanded", ("Rational.is'_expanded", eval_is_expanded ""))*)
1.148 fun eval_is_expanded (thmid:string) _
1.149 (t as (Const("Rational.is'_expanded", _) $ arg)) thy =
1.150 if is_expanded arg
1.151 - then SOME (TermC.mk_thmid thmid (term_to_string''' thy arg) "",
1.152 + then SOME (TermC.mk_thmid thmid (Celem.term_to_string''' thy arg) "",
1.153 HOLogic.Trueprop $ (TermC.mk_equality (t, @{term True})))
1.154 - else SOME (TermC.mk_thmid thmid (term_to_string''' thy arg) "",
1.155 + else SOME (TermC.mk_thmid thmid (Celem.term_to_string''' thy arg) "",
1.156 HOLogic.Trueprop $ (TermC.mk_equality (t, @{term False})))
1.157 | eval_is_expanded _ _ _ _ = NONE;
1.158 *}
1.159 @@ -465,16 +465,16 @@
1.160 [("is_expanded", ("Rational.is'_expanded", eval_is_expanded ""))] *}
1.161 ML {*
1.162 val rational_erls =
1.163 - merge_rls "rational_erls" calculate_Rational
1.164 - (append_rls "is_expanded" Atools_erls
1.165 - [Calc ("Rational.is'_expanded", eval_is_expanded "")]);
1.166 + Celem.merge_rls "rational_erls" calculate_Rational
1.167 + (Celem.append_rls "is_expanded" Atools_erls
1.168 + [Celem.Calc ("Rational.is'_expanded", eval_is_expanded "")]);
1.169 *}
1.170
1.171 subsection {* Embed cancellation into rewriting *}
1.172 ML {*
1.173 local (* cancel_p *)
1.174
1.175 -val {rules = rules, rew_ord = (_, ro), ...} = rep_rls (assoc_rls' @{theory} "rev_rew_p");
1.176 +val {rules = rules, rew_ord = (_, ro), ...} = Celem.rep_rls (assoc_rls' @{theory} "rev_rew_p");
1.177
1.178 fun init_state thy eval_rls ro t =
1.179 let
1.180 @@ -482,22 +482,22 @@
1.181 val SOME (t'', asm) = cancel_p_ thy t;
1.182 val der = Rtools.reverse_deriv thy eval_rls rules ro NONE t';
1.183 val der = der @
1.184 - [(Thm ("real_mult_div_cancel2", TermC.num_str @{thm real_mult_div_cancel2}), (t'', asm))]
1.185 + [(Celem.Thm ("real_mult_div_cancel2", TermC.num_str @{thm real_mult_div_cancel2}), (t'', asm))]
1.186 val rs = (Rtools.distinct_Thm o (map #1)) der
1.187 val rs = filter_out (Rtools.eq_Thms
1.188 ["sym_real_add_zero_left", "sym_real_mult_0", "sym_real_mult_1"]) rs
1.189 in (t, t'', [rs(*one in order to ease locate_rule*)], der) end;
1.190
1.191 fun locate_rule thy eval_rls ro [rs] t r =
1.192 - if member op = ((map (id_of_thm)) rs) (id_of_thm r)
1.193 + if member op = ((map (Celem.id_of_thm)) rs) (Celem.id_of_thm r)
1.194 then
1.195 - let val ropt = Rewrite.rewrite_ thy ro eval_rls true (thm_of_thm r) t;
1.196 + let val ropt = Rewrite.rewrite_ thy ro eval_rls true (Celem.thm_of_thm r) t;
1.197 in
1.198 case ropt of SOME ta => [(r, ta)]
1.199 | NONE => (tracing
1.200 - ("### locate_rule: rewrite " ^ id_of_thm r ^ " " ^ term2str t ^ " = NONE"); [])
1.201 + ("### locate_rule: rewrite " ^ Celem.id_of_thm r ^ " " ^ Celem.term2str t ^ " = NONE"); [])
1.202 end
1.203 - else (tracing ("### locate_rule: " ^ id_of_thm r ^ " not mem rrls"); [])
1.204 + else (tracing ("### locate_rule: " ^ Celem.id_of_thm r ^ " not mem rrls"); [])
1.205 | locate_rule _ _ _ _ _ _ = error "locate_rule: doesnt match rev-sets in istate";
1.206
1.207 fun next_rule thy eval_rls ro [rs] t =
1.208 @@ -506,13 +506,13 @@
1.209 in case der of (_, r, _) :: _ => SOME r | _ => NONE end
1.210 | next_rule _ _ _ _ _ = error ("next_rule: doesnt match rev-sets in istate");
1.211
1.212 -fun attach_form (_:rule list list) (_:term) (_:term) =
1.213 - [(*TODO*)]: (rule * (term * term list)) list;
1.214 +fun attach_form (_: Celem.rule list list) (_: term) (_: term) =
1.215 + [(*TODO*)]: ( Celem.rule * (term * term list)) list;
1.216
1.217 in
1.218
1.219 val cancel_p =
1.220 - Rrls {id = "cancel_p", prepat = [],
1.221 + Celem.Rrls {id = "cancel_p", prepat = [],
1.222 rew_ord=("ord_make_polynomial", ord_make_polynomial false thy),
1.223 erls = rational_erls,
1.224 calc =
1.225 @@ -522,7 +522,7 @@
1.226 ("POWER", ("Atools.pow", eval_binop "#power_"))],
1.227 errpatts = [],
1.228 scr =
1.229 - Rfuns {init_state = init_state thy Atools_erls ro,
1.230 + Celem.Rfuns {init_state = init_state thy Atools_erls ro,
1.231 normal_form = cancel_p_ thy,
1.232 locate_rule = locate_rule thy Atools_erls ro,
1.233 next_rule = next_rule thy Atools_erls ro,
1.234 @@ -534,8 +534,8 @@
1.235 ML {*
1.236 local (* add_fractions_p *)
1.237
1.238 -(*val {rules = rules, rew_ord = (_, ro), ...} = rep_rls (assoc_rls "make_polynomial");*)
1.239 -val {rules, rew_ord=(_,ro),...} = rep_rls (assoc_rls' @{theory} "rev_rew_p");
1.240 +(*val {rules = rules, rew_ord = (_, ro), ...} = Celem.rep_rls (assoc_rls "make_polynomial");*)
1.241 +val {rules, rew_ord=(_,ro),...} = Celem.rep_rls (assoc_rls' @{theory} "rev_rew_p");
1.242
1.243 fun init_state thy eval_rls ro t =
1.244 let
1.245 @@ -543,23 +543,23 @@
1.246 val SOME (t'', asm) = add_fraction_p_ thy t;
1.247 val der = Rtools.reverse_deriv thy eval_rls rules ro NONE t';
1.248 val der = der @
1.249 - [(Thm ("real_mult_div_cancel2", TermC.num_str @{thm real_mult_div_cancel2}), (t'',asm))]
1.250 + [(Celem.Thm ("real_mult_div_cancel2", TermC.num_str @{thm real_mult_div_cancel2}), (t'',asm))]
1.251 val rs = (Rtools.distinct_Thm o (map #1)) der;
1.252 val rs = filter_out (Rtools.eq_Thms
1.253 ["sym_real_add_zero_left", "sym_real_mult_0", "sym_real_mult_1"]) rs;
1.254 in (t, t'', [rs(*here only _ONE_*)], der) end;
1.255
1.256 fun locate_rule thy eval_rls ro [rs] t r =
1.257 - if member op = ((map (id_of_thm)) rs) (id_of_thm r)
1.258 + if member op = ((map (Celem.id_of_thm)) rs) (Celem.id_of_thm r)
1.259 then
1.260 - let val ropt = Rewrite.rewrite_ thy ro eval_rls true (thm_of_thm r) t;
1.261 + let val ropt = Rewrite.rewrite_ thy ro eval_rls true (Celem.thm_of_thm r) t;
1.262 in
1.263 case ropt of
1.264 SOME ta => [(r, ta)]
1.265 | NONE =>
1.266 - (tracing ("### locate_rule: rewrite " ^ id_of_thm r ^ " " ^ term2str t ^ " = NONE");
1.267 + (tracing ("### locate_rule: rewrite " ^ Celem.id_of_thm r ^ " " ^ Celem.term2str t ^ " = NONE");
1.268 []) end
1.269 - else (tracing ("### locate_rule: " ^ id_of_thm r ^ " not mem rrls"); [])
1.270 + else (tracing ("### locate_rule: " ^ Celem.id_of_thm r ^ " not mem rrls"); [])
1.271 | locate_rule _ _ _ _ _ _ = error "locate_rule: doesnt match rev-sets in istate";
1.272
1.273 fun next_rule thy eval_rls ro [rs] t =
1.274 @@ -580,7 +580,7 @@
1.275 in
1.276
1.277 val add_fractions_p =
1.278 - Rrls {id = "add_fractions_p", prepat=prepat,
1.279 + Celem.Rrls {id = "add_fractions_p", prepat=prepat,
1.280 rew_ord = ("ord_make_polynomial", ord_make_polynomial false thy),
1.281 erls = rational_erls,
1.282 calc = [("PLUS", ("Groups.plus_class.plus", eval_binop "#add_")),
1.283 @@ -588,7 +588,7 @@
1.284 ("DIVIDE", ("Rings.divide_class.divide", eval_cancel "#divide_e")),
1.285 ("POWER", ("Atools.pow", eval_binop "#power_"))],
1.286 errpatts = [],
1.287 - scr = Rfuns {init_state = init_state thy Atools_erls ro,
1.288 + scr = Celem.Rfuns {init_state = init_state thy Atools_erls ro,
1.289 normal_form = add_fraction_p_ thy,
1.290 locate_rule = locate_rule thy Atools_erls ro,
1.291 next_rule = next_rule thy Atools_erls ro,
1.292 @@ -610,254 +610,254 @@
1.293
1.294 (*erls for calculate_Rational; make local with FIXX@ME result:term *term list*)
1.295 val powers_erls = prep_rls'(
1.296 - Rls {id = "powers_erls", preconds = [], rew_ord = ("dummy_ord",dummy_ord),
1.297 - erls = e_rls, srls = Erls, calc = [], errpatts = [],
1.298 - rules = [Calc ("Atools.is'_atom",eval_is_atom "#is_atom_"),
1.299 - Calc ("Atools.is'_even",eval_is_even "#is_even_"),
1.300 - Calc ("Orderings.ord_class.less",eval_equ "#less_"),
1.301 - Thm ("not_false", TermC.num_str @{thm not_false}),
1.302 - Thm ("not_true", TermC.num_str @{thm not_true}),
1.303 - Calc ("Groups.plus_class.plus",eval_binop "#add_")
1.304 + Celem.Rls {id = "powers_erls", preconds = [], rew_ord = ("dummy_ord",Celem.dummy_ord),
1.305 + erls = Celem.e_rls, srls = Celem.Erls, calc = [], errpatts = [],
1.306 + rules = [Celem.Calc ("Atools.is'_atom",eval_is_atom "#is_atom_"),
1.307 + Celem.Calc ("Atools.is'_even",eval_is_even "#is_even_"),
1.308 + Celem.Calc ("Orderings.ord_class.less",eval_equ "#less_"),
1.309 + Celem.Thm ("not_false", TermC.num_str @{thm not_false}),
1.310 + Celem.Thm ("not_true", TermC.num_str @{thm not_true}),
1.311 + Celem.Calc ("Groups.plus_class.plus",eval_binop "#add_")
1.312 ],
1.313 - scr = EmptyScr
1.314 - }:rls);
1.315 + scr = Celem.EmptyScr
1.316 + });
1.317 (*.all powers over + distributed; atoms over * collected, other distributed
1.318 contains absolute minimum of thms for context in norm_Rational .*)
1.319 val powers = prep_rls'(
1.320 - Rls {id = "powers", preconds = [], rew_ord = ("dummy_ord",dummy_ord),
1.321 - erls = powers_erls, srls = Erls, calc = [], errpatts = [],
1.322 - rules = [Thm ("realpow_multI", TermC.num_str @{thm realpow_multI}),
1.323 + Celem.Rls {id = "powers", preconds = [], rew_ord = ("dummy_ord",Celem.dummy_ord),
1.324 + erls = powers_erls, srls = Celem.Erls, calc = [], errpatts = [],
1.325 + rules = [Celem.Thm ("realpow_multI", TermC.num_str @{thm realpow_multI}),
1.326 (*"(r * s) ^^^ n = r ^^^ n * s ^^^ n"*)
1.327 - Thm ("realpow_pow",TermC.num_str @{thm realpow_pow}),
1.328 + Celem.Thm ("realpow_pow",TermC.num_str @{thm realpow_pow}),
1.329 (*"(a ^^^ b) ^^^ c = a ^^^ (b * c)"*)
1.330 - Thm ("realpow_oneI",TermC.num_str @{thm realpow_oneI}),
1.331 + Celem.Thm ("realpow_oneI",TermC.num_str @{thm realpow_oneI}),
1.332 (*"r ^^^ 1 = r"*)
1.333 - Thm ("realpow_minus_even",TermC.num_str @{thm realpow_minus_even}),
1.334 + Celem.Thm ("realpow_minus_even",TermC.num_str @{thm realpow_minus_even}),
1.335 (*"n is_even ==> (- r) ^^^ n = r ^^^ n" ?-->discard_minus?*)
1.336 - Thm ("realpow_minus_odd",TermC.num_str @{thm realpow_minus_odd}),
1.337 + Celem.Thm ("realpow_minus_odd",TermC.num_str @{thm realpow_minus_odd}),
1.338 (*"Not (n is_even) ==> (- r) ^^^ n = -1 * r ^^^ n"*)
1.339
1.340 (*----- collect atoms over * -----*)
1.341 - Thm ("realpow_two_atom",TermC.num_str @{thm realpow_two_atom}),
1.342 + Celem.Thm ("realpow_two_atom",TermC.num_str @{thm realpow_two_atom}),
1.343 (*"r is_atom ==> r * r = r ^^^ 2"*)
1.344 - Thm ("realpow_plus_1",TermC.num_str @{thm realpow_plus_1}),
1.345 + Celem.Thm ("realpow_plus_1",TermC.num_str @{thm realpow_plus_1}),
1.346 (*"r is_atom ==> r * r ^^^ n = r ^^^ (n + 1)"*)
1.347 - Thm ("realpow_addI_atom",TermC.num_str @{thm realpow_addI_atom}),
1.348 + Celem.Thm ("realpow_addI_atom",TermC.num_str @{thm realpow_addI_atom}),
1.349 (*"r is_atom ==> r ^^^ n * r ^^^ m = r ^^^ (n + m)"*)
1.350
1.351 (*----- distribute none-atoms -----*)
1.352 - Thm ("realpow_def_atom",TermC.num_str @{thm realpow_def_atom}),
1.353 + Celem.Thm ("realpow_def_atom",TermC.num_str @{thm realpow_def_atom}),
1.354 (*"[| 1 < n; not(r is_atom) |]==>r ^^^ n = r * r ^^^ (n + -1)"*)
1.355 - Thm ("realpow_eq_oneI",TermC.num_str @{thm realpow_eq_oneI}),
1.356 + Celem.Thm ("realpow_eq_oneI",TermC.num_str @{thm realpow_eq_oneI}),
1.357 (*"1 ^^^ n = 1"*)
1.358 - Calc ("Groups.plus_class.plus",eval_binop "#add_")
1.359 + Celem.Calc ("Groups.plus_class.plus",eval_binop "#add_")
1.360 ],
1.361 - scr = EmptyScr
1.362 - }:rls);
1.363 + scr = Celem.EmptyScr
1.364 + });
1.365 (*.contains absolute minimum of thms for context in norm_Rational.*)
1.366 val rat_mult_divide = prep_rls'(
1.367 - Rls {id = "rat_mult_divide", preconds = [],
1.368 - rew_ord = ("dummy_ord", dummy_ord),
1.369 - erls = e_rls, srls = Erls, calc = [], errpatts = [],
1.370 - rules = [Thm ("rat_mult",TermC.num_str @{thm rat_mult}),
1.371 + Celem.Rls {id = "rat_mult_divide", preconds = [],
1.372 + rew_ord = ("dummy_ord", Celem.dummy_ord),
1.373 + erls = Celem.e_rls, srls = Celem.Erls, calc = [], errpatts = [],
1.374 + rules = [Celem.Thm ("rat_mult",TermC.num_str @{thm rat_mult}),
1.375 (*(1)"?a / ?b * (?c / ?d) = ?a * ?c / (?b * ?d)"*)
1.376 - Thm ("times_divide_eq_right",TermC.num_str @{thm times_divide_eq_right}),
1.377 + Celem.Thm ("times_divide_eq_right",TermC.num_str @{thm times_divide_eq_right}),
1.378 (*(2)"?a * (?c / ?d) = ?a * ?c / ?d" must be [2],
1.379 otherwise inv.to a / b / c = ...*)
1.380 - Thm ("times_divide_eq_left",TermC.num_str @{thm times_divide_eq_left}),
1.381 + Celem.Thm ("times_divide_eq_left",TermC.num_str @{thm times_divide_eq_left}),
1.382 (*"?a / ?b * ?c = ?a * ?c / ?b" order weights x^^^n too much
1.383 and does not commute a / b * c ^^^ 2 !*)
1.384
1.385 - Thm ("divide_divide_eq_right",
1.386 + Celem.Thm ("divide_divide_eq_right",
1.387 TermC.num_str @{thm divide_divide_eq_right}),
1.388 (*"?x / (?y / ?z) = ?x * ?z / ?y"*)
1.389 - Thm ("divide_divide_eq_left",
1.390 + Celem.Thm ("divide_divide_eq_left",
1.391 TermC.num_str @{thm divide_divide_eq_left}),
1.392 (*"?x / ?y / ?z = ?x / (?y * ?z)"*)
1.393 - Calc ("Rings.divide_class.divide" ,eval_cancel "#divide_e")
1.394 + Celem.Calc ("Rings.divide_class.divide" ,eval_cancel "#divide_e")
1.395 ],
1.396 - scr = EmptyScr
1.397 - }:rls);
1.398 + scr = Celem.EmptyScr
1.399 + });
1.400
1.401 (*.contains absolute minimum of thms for context in norm_Rational.*)
1.402 val reduce_0_1_2 = prep_rls'(
1.403 - Rls{id = "reduce_0_1_2", preconds = [], rew_ord = ("dummy_ord", dummy_ord),
1.404 - erls = e_rls, srls = Erls, calc = [], errpatts = [],
1.405 - rules = [(*Thm ("divide_1",TermC.num_str @{thm divide_1}),
1.406 + Celem.Rls{id = "reduce_0_1_2", preconds = [], rew_ord = ("dummy_ord", Celem.dummy_ord),
1.407 + erls = Celem.e_rls, srls = Celem.Erls, calc = [], errpatts = [],
1.408 + rules = [(*Celem.Thm ("divide_1",TermC.num_str @{thm divide_1}),
1.409 "?x / 1 = ?x" unnecess.for normalform*)
1.410 - Thm ("mult_1_left",TermC.num_str @{thm mult_1_left}),
1.411 + Celem.Thm ("mult_1_left",TermC.num_str @{thm mult_1_left}),
1.412 (*"1 * z = z"*)
1.413 - (*Thm ("real_mult_minus1",TermC.num_str @{thm real_mult_minus1}),
1.414 + (*Celem.Thm ("real_mult_minus1",TermC.num_str @{thm real_mult_minus1}),
1.415 "-1 * z = - z"*)
1.416 - (*Thm ("real_minus_mult_cancel",TermC.num_str @{thm real_minus_mult_cancel}),
1.417 + (*Celem.Thm ("real_minus_mult_cancel",TermC.num_str @{thm real_minus_mult_cancel}),
1.418 "- ?x * - ?y = ?x * ?y"*)
1.419
1.420 - Thm ("mult_zero_left",TermC.num_str @{thm mult_zero_left}),
1.421 + Celem.Thm ("mult_zero_left",TermC.num_str @{thm mult_zero_left}),
1.422 (*"0 * z = 0"*)
1.423 - Thm ("add_0_left",TermC.num_str @{thm add_0_left}),
1.424 + Celem.Thm ("add_0_left",TermC.num_str @{thm add_0_left}),
1.425 (*"0 + z = z"*)
1.426 - (*Thm ("right_minus",TermC.num_str @{thm right_minus}),
1.427 + (*Celem.Thm ("right_minus",TermC.num_str @{thm right_minus}),
1.428 "?z + - ?z = 0"*)
1.429
1.430 - Thm ("sym_real_mult_2",
1.431 + Celem.Thm ("sym_real_mult_2",
1.432 TermC.num_str (@{thm real_mult_2} RS @{thm sym})),
1.433 (*"z1 + z1 = 2 * z1"*)
1.434 - Thm ("real_mult_2_assoc",TermC.num_str @{thm real_mult_2_assoc}),
1.435 + Celem.Thm ("real_mult_2_assoc",TermC.num_str @{thm real_mult_2_assoc}),
1.436 (*"z1 + (z1 + k) = 2 * z1 + k"*)
1.437
1.438 - Thm ("division_ring_divide_zero",TermC.num_str @{thm division_ring_divide_zero})
1.439 + Celem.Thm ("division_ring_divide_zero",TermC.num_str @{thm division_ring_divide_zero})
1.440 (*"0 / ?x = 0"*)
1.441 - ], scr = EmptyScr}:rls);
1.442 + ], scr = Celem.EmptyScr});
1.443
1.444 (*erls for calculate_Rational;
1.445 make local with FIXX@ME result:term *term list WN0609???SKMG*)
1.446 val norm_rat_erls = prep_rls'(
1.447 - Rls {id = "norm_rat_erls", preconds = [], rew_ord = ("dummy_ord",dummy_ord),
1.448 - erls = e_rls, srls = Erls, calc = [], errpatts = [],
1.449 - rules = [Calc ("Atools.is'_const",eval_const "#is_const_")
1.450 - ], scr = EmptyScr}:rls);
1.451 + Celem.Rls {id = "norm_rat_erls", preconds = [], rew_ord = ("dummy_ord",Celem.dummy_ord),
1.452 + erls = Celem.e_rls, srls = Celem.Erls, calc = [], errpatts = [],
1.453 + rules = [Celem.Calc ("Atools.is'_const",eval_const "#is_const_")
1.454 + ], scr = Celem.EmptyScr});
1.455
1.456 (* consists of rls containing the absolute minimum of thms *)
1.457 (*040209: this version has been used by RL for his equations,
1.458 which is now replaced by MGs version "norm_Rational" below *)
1.459 val norm_Rational_min = prep_rls'(
1.460 - Rls {id = "norm_Rational_min", preconds = [], rew_ord = ("dummy_ord",dummy_ord),
1.461 - erls = norm_rat_erls, srls = Erls, calc = [], errpatts = [],
1.462 + Celem.Rls {id = "norm_Rational_min", preconds = [], rew_ord = ("dummy_ord",Celem.dummy_ord),
1.463 + erls = norm_rat_erls, srls = Celem.Erls, calc = [], errpatts = [],
1.464 rules = [(*sequence given by operator precedence*)
1.465 - Rls_ discard_minus,
1.466 - Rls_ powers,
1.467 - Rls_ rat_mult_divide,
1.468 - Rls_ expand,
1.469 - Rls_ reduce_0_1_2,
1.470 - Rls_ order_add_mult,
1.471 - Rls_ collect_numerals,
1.472 - Rls_ add_fractions_p,
1.473 - Rls_ cancel_p
1.474 + Celem.Rls_ discard_minus,
1.475 + Celem.Rls_ powers,
1.476 + Celem.Rls_ rat_mult_divide,
1.477 + Celem.Rls_ expand,
1.478 + Celem.Rls_ reduce_0_1_2,
1.479 + Celem.Rls_ order_add_mult,
1.480 + Celem.Rls_ collect_numerals,
1.481 + Celem.Rls_ add_fractions_p,
1.482 + Celem.Rls_ cancel_p
1.483 ],
1.484 - scr = EmptyScr}:rls);
1.485 + scr = Celem.EmptyScr});
1.486
1.487 val norm_Rational_parenthesized = prep_rls'(
1.488 - Seq {id = "norm_Rational_parenthesized", preconds = []:term list,
1.489 - rew_ord = ("dummy_ord", dummy_ord),
1.490 - erls = Atools_erls, srls = Erls,
1.491 + Celem.Seq {id = "norm_Rational_parenthesized", preconds = []:term list,
1.492 + rew_ord = ("dummy_ord", Celem.dummy_ord),
1.493 + erls = Atools_erls, srls = Celem.Erls,
1.494 calc = [], errpatts = [],
1.495 - rules = [Rls_ norm_Rational_min,
1.496 - Rls_ discard_parentheses
1.497 + rules = [Celem.Rls_ norm_Rational_min,
1.498 + Celem.Rls_ discard_parentheses
1.499 ],
1.500 - scr = EmptyScr}:rls);
1.501 + scr = Celem.EmptyScr});
1.502
1.503 (*WN030318???SK: simplifies all but cancel and common_nominator*)
1.504 val simplify_rational =
1.505 - merge_rls "simplify_rational" expand_binoms
1.506 - (append_rls "divide" calculate_Rational
1.507 - [Thm ("div_by_1",TermC.num_str @{thm div_by_1}),
1.508 + Celem.merge_rls "simplify_rational" expand_binoms
1.509 + (Celem.append_rls "divide" calculate_Rational
1.510 + [Celem.Thm ("div_by_1",TermC.num_str @{thm div_by_1}),
1.511 (*"?x / 1 = ?x"*)
1.512 - Thm ("rat_mult",TermC.num_str @{thm rat_mult}),
1.513 + Celem.Thm ("rat_mult",TermC.num_str @{thm rat_mult}),
1.514 (*(1)"?a / ?b * (?c / ?d) = ?a * ?c / (?b * ?d)"*)
1.515 - Thm ("times_divide_eq_right",TermC.num_str @{thm times_divide_eq_right}),
1.516 + Celem.Thm ("times_divide_eq_right",TermC.num_str @{thm times_divide_eq_right}),
1.517 (*(2)"?a * (?c / ?d) = ?a * ?c / ?d" must be [2],
1.518 otherwise inv.to a / b / c = ...*)
1.519 - Thm ("times_divide_eq_left",TermC.num_str @{thm times_divide_eq_left}),
1.520 + Celem.Thm ("times_divide_eq_left",TermC.num_str @{thm times_divide_eq_left}),
1.521 (*"?a / ?b * ?c = ?a * ?c / ?b"*)
1.522 - Thm ("add_minus",TermC.num_str @{thm add_minus}),
1.523 + Celem.Thm ("add_minus",TermC.num_str @{thm add_minus}),
1.524 (*"?a + ?b - ?b = ?a"*)
1.525 - Thm ("add_minus1",TermC.num_str @{thm add_minus1}),
1.526 + Celem.Thm ("add_minus1",TermC.num_str @{thm add_minus1}),
1.527 (*"?a - ?b + ?b = ?a"*)
1.528 - Thm ("divide_minus1",TermC.num_str @{thm divide_minus1})
1.529 + Celem.Thm ("divide_minus1",TermC.num_str @{thm divide_minus1})
1.530 (*"?x / -1 = - ?x"*)
1.531 ]);
1.532 *}
1.533 ML {*
1.534 val add_fractions_p_rls = prep_rls'(
1.535 - Rls {id = "add_fractions_p_rls", preconds = [], rew_ord = ("dummy_ord", dummy_ord),
1.536 - erls = e_rls, srls = Erls, calc = [], errpatts = [],
1.537 - rules = [Rls_ add_fractions_p],
1.538 - scr = EmptyScr});
1.539 + Celem.Rls {id = "add_fractions_p_rls", preconds = [], rew_ord = ("dummy_ord", Celem.dummy_ord),
1.540 + erls = Celem.e_rls, srls = Celem.Erls, calc = [], errpatts = [],
1.541 + rules = [Celem.Rls_ add_fractions_p],
1.542 + scr = Celem.EmptyScr});
1.543
1.544 -(* "Rls" causes repeated application of cancel_p to one and the same term *)
1.545 +(* "Celem.Rls" causes repeated application of cancel_p to one and the same term *)
1.546 val cancel_p_rls = prep_rls'(
1.547 - Rls
1.548 - {id = "cancel_p_rls", preconds = [], rew_ord = ("dummy_ord", dummy_ord),
1.549 - erls = e_rls, srls = Erls, calc = [], errpatts = [],
1.550 - rules = [Rls_ cancel_p],
1.551 - scr = EmptyScr});
1.552 + Celem.Rls
1.553 + {id = "cancel_p_rls", preconds = [], rew_ord = ("dummy_ord", Celem.dummy_ord),
1.554 + erls = Celem.e_rls, srls = Celem.Erls, calc = [], errpatts = [],
1.555 + rules = [Celem.Rls_ cancel_p],
1.556 + scr = Celem.EmptyScr});
1.557
1.558 (*. makes 'normal' fractions; 'is_polyexp' inhibits double fractions;
1.559 used in initial part norm_Rational_mg, see example DA-M02-main.p.60.*)
1.560 val rat_mult_poly = prep_rls'(
1.561 - Rls {id = "rat_mult_poly", preconds = [], rew_ord = ("dummy_ord", dummy_ord),
1.562 - erls = append_rls "e_rls-is_polyexp" e_rls [Calc ("Poly.is'_polyexp", eval_is_polyexp "")],
1.563 - srls = Erls, calc = [], errpatts = [],
1.564 + Celem.Rls {id = "rat_mult_poly", preconds = [], rew_ord = ("dummy_ord", Celem.dummy_ord),
1.565 + erls = Celem.append_rls "Celem.e_rls-is_polyexp" Celem.e_rls [Celem.Calc ("Poly.is'_polyexp", eval_is_polyexp "")],
1.566 + srls = Celem.Erls, calc = [], errpatts = [],
1.567 rules =
1.568 - [Thm ("rat_mult_poly_l",TermC.num_str @{thm rat_mult_poly_l}),
1.569 + [Celem.Thm ("rat_mult_poly_l",TermC.num_str @{thm rat_mult_poly_l}),
1.570 (*"?c is_polyexp ==> ?c * (?a / ?b) = ?c * ?a / ?b"*)
1.571 - Thm ("rat_mult_poly_r",TermC.num_str @{thm rat_mult_poly_r})
1.572 + Celem.Thm ("rat_mult_poly_r",TermC.num_str @{thm rat_mult_poly_r})
1.573 (*"?c is_polyexp ==> ?a / ?b * ?c = ?a * ?c / ?b"*) ],
1.574 - scr = EmptyScr});
1.575 + scr = Celem.EmptyScr});
1.576
1.577 (*. makes 'normal' fractions; 'is_polyexp' inhibits double fractions;
1.578 used in looping part norm_Rational_rls, see example DA-M02-main.p.60
1.579 - .. WHERE THE LATTER DOES ALWAYS WORK, BECAUSE erls = e_rls,
1.580 - I.E. THE RESPECTIVE ASSUMPTION IS STORED AND Thm APPLIED; WN051028
1.581 + .. WHERE THE LATTER DOES ALWAYS WORK, BECAUSE erls = Celem.e_rls,
1.582 + I.E. THE RESPECTIVE ASSUMPTION IS STORED AND Celem.Thm APPLIED; WN051028
1.583 ... WN0609???MG.*)
1.584 val rat_mult_div_pow = prep_rls'(
1.585 - Rls {id = "rat_mult_div_pow", preconds = [], rew_ord = ("dummy_ord",dummy_ord),
1.586 - erls = e_rls, srls = Erls, calc = [], errpatts = [],
1.587 - rules = [Thm ("rat_mult", TermC.num_str @{thm rat_mult}),
1.588 + Celem.Rls {id = "rat_mult_div_pow", preconds = [], rew_ord = ("dummy_ord",Celem.dummy_ord),
1.589 + erls = Celem.e_rls, srls = Celem.Erls, calc = [], errpatts = [],
1.590 + rules = [Celem.Thm ("rat_mult", TermC.num_str @{thm rat_mult}),
1.591 (*"?a / ?b * (?c / ?d) = ?a * ?c / (?b * ?d)"*)
1.592 - Thm ("rat_mult_poly_l", TermC.num_str @{thm rat_mult_poly_l}),
1.593 + Celem.Thm ("rat_mult_poly_l", TermC.num_str @{thm rat_mult_poly_l}),
1.594 (*"?c is_polyexp ==> ?c * (?a / ?b) = ?c * ?a / ?b"*)
1.595 - Thm ("rat_mult_poly_r", TermC.num_str @{thm rat_mult_poly_r}),
1.596 + Celem.Thm ("rat_mult_poly_r", TermC.num_str @{thm rat_mult_poly_r}),
1.597 (*"?c is_polyexp ==> ?a / ?b * ?c = ?a * ?c / ?b"*)
1.598
1.599 - Thm ("real_divide_divide1_mg", TermC.num_str @{thm real_divide_divide1_mg}),
1.600 + Celem.Thm ("real_divide_divide1_mg", TermC.num_str @{thm real_divide_divide1_mg}),
1.601 (*"y ~= 0 ==> (u / v) / (y / z) = (u * z) / (y * v)"*)
1.602 - Thm ("divide_divide_eq_right", TermC.num_str @{thm divide_divide_eq_right}),
1.603 + Celem.Thm ("divide_divide_eq_right", TermC.num_str @{thm divide_divide_eq_right}),
1.604 (*"?x / (?y / ?z) = ?x * ?z / ?y"*)
1.605 - Thm ("divide_divide_eq_left", TermC.num_str @{thm divide_divide_eq_left}),
1.606 + Celem.Thm ("divide_divide_eq_left", TermC.num_str @{thm divide_divide_eq_left}),
1.607 (*"?x / ?y / ?z = ?x / (?y * ?z)"*)
1.608 - Calc ("Rings.divide_class.divide", eval_cancel "#divide_e"),
1.609 + Celem.Calc ("Rings.divide_class.divide", eval_cancel "#divide_e"),
1.610
1.611 - Thm ("rat_power", TermC.num_str @{thm rat_power})
1.612 + Celem.Thm ("rat_power", TermC.num_str @{thm rat_power})
1.613 (*"(?a / ?b) ^^^ ?n = ?a ^^^ ?n / ?b ^^^ ?n"*)
1.614 ],
1.615 - scr = EmptyScr}:rls);
1.616 + scr = Celem.EmptyScr});
1.617
1.618 val rat_reduce_1 = prep_rls'(
1.619 - Rls {id = "rat_reduce_1", preconds = [], rew_ord = ("dummy_ord", dummy_ord),
1.620 - erls = e_rls, srls = Erls, calc = [], errpatts = [],
1.621 + Celem.Rls {id = "rat_reduce_1", preconds = [], rew_ord = ("dummy_ord", Celem.dummy_ord),
1.622 + erls = Celem.e_rls, srls = Celem.Erls, calc = [], errpatts = [],
1.623 rules =
1.624 - [Thm ("div_by_1", TermC.num_str @{thm div_by_1}),
1.625 + [Celem.Thm ("div_by_1", TermC.num_str @{thm div_by_1}),
1.626 (*"?x / 1 = ?x"*)
1.627 - Thm ("mult_1_left", TermC.num_str @{thm mult_1_left})
1.628 + Celem.Thm ("mult_1_left", TermC.num_str @{thm mult_1_left})
1.629 (*"1 * z = z"*)
1.630 ],
1.631 - scr = EmptyScr}:rls);
1.632 + scr = Celem.EmptyScr});
1.633
1.634 (* looping part of norm_Rational *)
1.635 val norm_Rational_rls = prep_rls' (
1.636 - Rls {id = "norm_Rational_rls", preconds = [], rew_ord = ("dummy_ord",dummy_ord),
1.637 - erls = norm_rat_erls, srls = Erls, calc = [], errpatts = [],
1.638 - rules = [Rls_ add_fractions_p_rls,
1.639 - Rls_ rat_mult_div_pow,
1.640 - Rls_ make_rat_poly_with_parentheses,
1.641 - Rls_ cancel_p_rls,
1.642 - Rls_ rat_reduce_1
1.643 + Celem.Rls {id = "norm_Rational_rls", preconds = [], rew_ord = ("dummy_ord",Celem.dummy_ord),
1.644 + erls = norm_rat_erls, srls = Celem.Erls, calc = [], errpatts = [],
1.645 + rules = [Celem.Rls_ add_fractions_p_rls,
1.646 + Celem.Rls_ rat_mult_div_pow,
1.647 + Celem.Rls_ make_rat_poly_with_parentheses,
1.648 + Celem.Rls_ cancel_p_rls,
1.649 + Celem.Rls_ rat_reduce_1
1.650 ],
1.651 - scr = EmptyScr}:rls);
1.652 + scr = Celem.EmptyScr});
1.653
1.654 val norm_Rational = prep_rls' (
1.655 - Seq
1.656 - {id = "norm_Rational", preconds = [], rew_ord = ("dummy_ord", dummy_ord),
1.657 - erls = norm_rat_erls, srls = Erls, calc = [], errpatts = [],
1.658 - rules = [Rls_ discard_minus,
1.659 - Rls_ rat_mult_poly, (* removes double fractions like a/b/c *)
1.660 - Rls_ make_rat_poly_with_parentheses,
1.661 - Rls_ cancel_p_rls,
1.662 - Rls_ norm_Rational_rls, (* the main rls, looping (#) *)
1.663 - Rls_ discard_parentheses1 (* mult only *)
1.664 + Celem.Seq
1.665 + {id = "norm_Rational", preconds = [], rew_ord = ("dummy_ord", Celem.dummy_ord),
1.666 + erls = norm_rat_erls, srls = Celem.Erls, calc = [], errpatts = [],
1.667 + rules = [Celem.Rls_ discard_minus,
1.668 + Celem.Rls_ rat_mult_poly, (* removes double fractions like a/b/c *)
1.669 + Celem.Rls_ make_rat_poly_with_parentheses,
1.670 + Celem.Rls_ cancel_p_rls,
1.671 + Celem.Rls_ norm_Rational_rls, (* the main rls, looping (#) *)
1.672 + Celem.Rls_ discard_parentheses1 (* mult only *)
1.673 ],
1.674 - scr = EmptyScr}:rls);
1.675 + scr = Celem.EmptyScr});
1.676 *}
1.677
1.678 setup {* KEStore_Elems.add_rlss
1.679 @@ -886,27 +886,27 @@
1.680
1.681 section {* A problem for simplification of rationals *}
1.682 setup {* KEStore_Elems.add_pbts
1.683 - [(Specify.prep_pbt thy "pbl_simp_rat" [] e_pblID
1.684 + [(Specify.prep_pbt thy "pbl_simp_rat" [] Celem.e_pblID
1.685 (["rational","simplification"],
1.686 [("#Given" ,["Term t_t"]),
1.687 ("#Where" ,["t_t is_ratpolyexp"]),
1.688 ("#Find" ,["normalform n_n"])],
1.689 - append_rls "e_rls" e_rls [(*for preds in where_*)],
1.690 + Celem.append_rls "xxxe_rlsxxx" Celem.e_rls [(*for preds in where_*)],
1.691 SOME "Simplify t_t", [["simplification","of_rationals"]]))] *}
1.692
1.693 section {* A methods for simplification of rationals *}
1.694 (*WN061025 this methods script is copied from (auto-generated) script
1.695 of norm_Rational in order to ease repair on inform*)
1.696 setup {* KEStore_Elems.add_mets
1.697 - [Specify.prep_met thy "met_simp_rat" [] e_metID
1.698 + [Specify.prep_met thy "met_simp_rat" [] Celem.e_metID
1.699 (["simplification","of_rationals"],
1.700 [("#Given" ,["Term t_t"]),
1.701 ("#Where" ,["t_t is_ratpolyexp"]),
1.702 ("#Find" ,["normalform n_n"])],
1.703 - {rew_ord'="tless_true", rls' = e_rls, calc = [], srls = e_rls,
1.704 - prls = append_rls "simplification_of_rationals_prls" e_rls
1.705 - [(*for preds in where_*) Calc ("Rational.is'_ratpolyexp", eval_is_ratpolyexp "")],
1.706 - crls = e_rls, errpats = [], nrls = norm_Rational_rls},
1.707 + {rew_ord'="tless_true", rls' = Celem.e_rls, calc = [], srls = Celem.e_rls,
1.708 + prls = Celem.append_rls "simplification_of_rationals_prls" Celem.e_rls
1.709 + [(*for preds in where_*) Celem.Calc ("Rational.is'_ratpolyexp", eval_is_ratpolyexp "")],
1.710 + crls = Celem.e_rls, errpats = [], nrls = norm_Rational_rls},
1.711 "Script SimplifyScript (t_t::real) = " ^
1.712 " ((Try (Rewrite_Set discard_minus False) @@ " ^
1.713 " Try (Rewrite_Set rat_mult_poly False) @@ " ^