188 (*.adapted from 'norm_Rational' by |
188 (*.adapted from 'norm_Rational' by |
189 #1 using 'ord_simplify_System' in 'order_add_mult_System' |
189 #1 using 'ord_simplify_System' in 'order_add_mult_System' |
190 #2 NOT using common_nominator_p .*) |
190 #2 NOT using common_nominator_p .*) |
191 val norm_System_noadd_fractions = |
191 val norm_System_noadd_fractions = |
192 Rule_Def.Repeat {id = "norm_System_noadd_fractions", preconds = [], |
192 Rule_Def.Repeat {id = "norm_System_noadd_fractions", preconds = [], |
193 rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord), |
193 rew_ord = ("dummy_ord", Rewrite_Ord.function_empty), |
194 erls = norm_rat_erls, srls = Rule_Set.Empty, calc = [], errpatts = [], |
194 erls = norm_rat_erls, srls = Rule_Set.Empty, calc = [], errpatts = [], |
195 rules = [(*sequence given by operator precedence*) |
195 rules = [(*sequence given by operator precedence*) |
196 Rule.Rls_ discard_minus, |
196 Rule.Rls_ discard_minus, |
197 Rule.Rls_ powers, |
197 Rule.Rls_ powers, |
198 Rule.Rls_ rat_mult_divide, |
198 Rule.Rls_ rat_mult_divide, |
207 ML \<open> |
207 ML \<open> |
208 (*.adapted from 'norm_Rational' by |
208 (*.adapted from 'norm_Rational' by |
209 *1* using 'ord_simplify_System' in 'order_add_mult_System'.*) |
209 *1* using 'ord_simplify_System' in 'order_add_mult_System'.*) |
210 val norm_System = |
210 val norm_System = |
211 Rule_Def.Repeat {id = "norm_System", preconds = [], |
211 Rule_Def.Repeat {id = "norm_System", preconds = [], |
212 rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord), |
212 rew_ord = ("dummy_ord", Rewrite_Ord.function_empty), |
213 erls = norm_rat_erls, srls = Rule_Set.Empty, calc = [], errpatts = [], |
213 erls = norm_rat_erls, srls = Rule_Set.Empty, calc = [], errpatts = [], |
214 rules = [(*sequence given by operator precedence*) |
214 rules = [(*sequence given by operator precedence*) |
215 Rule.Rls_ discard_minus, |
215 Rule.Rls_ discard_minus, |
216 Rule.Rls_ powers, |
216 Rule.Rls_ powers, |
217 Rule.Rls_ rat_mult_divide, |
217 Rule.Rls_ rat_mult_divide, |
233 *2* no add_fractions_p (= common_nominator_p_rls !) |
233 *2* no add_fractions_p (= common_nominator_p_rls !) |
234 *3* discard_parentheses only for (.*(.*.)) |
234 *3* discard_parentheses only for (.*(.*.)) |
235 analoguous to simplify_Integral .*) |
235 analoguous to simplify_Integral .*) |
236 val simplify_System_parenthesized = |
236 val simplify_System_parenthesized = |
237 Rule_Set.Sequence {id = "simplify_System_parenthesized", preconds = []:term list, |
237 Rule_Set.Sequence {id = "simplify_System_parenthesized", preconds = []:term list, |
238 rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord), |
238 rew_ord = ("dummy_ord", Rewrite_Ord.function_empty), |
239 erls = Atools_erls, srls = Rule_Set.Empty, calc = [], errpatts = [], |
239 erls = Atools_erls, srls = Rule_Set.Empty, calc = [], errpatts = [], |
240 rules = [ |
240 rules = [ |
241 \<^rule_thm>\<open>distrib_right\<close>, (*"(?z1.0 + ?z2.0) * ?w = ?z1.0 * ?w + ?z2.0 * ?w"*) |
241 \<^rule_thm>\<open>distrib_right\<close>, (*"(?z1.0 + ?z2.0) * ?w = ?z1.0 * ?w + ?z2.0 * ?w"*) |
242 \<^rule_thm>\<open>add_divide_distrib\<close>, (*"(?x + ?y) / ?z = ?x / ?z + ?y / ?z"*) |
242 \<^rule_thm>\<open>add_divide_distrib\<close>, (*"(?x + ?y) / ?z = ?x / ?z + ?y / ?z"*) |
243 Rule.Rls_ norm_Rational_noadd_fractions, |
243 Rule.Rls_ norm_Rational_noadd_fractions, |
253 This is a copy of 'make_ratpoly_in' with the differences |
253 This is a copy of 'make_ratpoly_in' with the differences |
254 *1* ord_simplify_System instead of termlessI .*) |
254 *1* ord_simplify_System instead of termlessI .*) |
255 (*TODO.WN051031 ^^^^^^^^^^ should be in EACH rls contained *) |
255 (*TODO.WN051031 ^^^^^^^^^^ should be in EACH rls contained *) |
256 val simplify_System = |
256 val simplify_System = |
257 Rule_Set.Sequence {id = "simplify_System", preconds = []:term list, |
257 Rule_Set.Sequence {id = "simplify_System", preconds = []:term list, |
258 rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord), |
258 rew_ord = ("dummy_ord", Rewrite_Ord.function_empty), |
259 erls = Atools_erls, srls = Rule_Set.Empty, calc = [], errpatts = [], |
259 erls = Atools_erls, srls = Rule_Set.Empty, calc = [], errpatts = [], |
260 rules = [ |
260 rules = [ |
261 Rule.Rls_ norm_Rational, |
261 Rule.Rls_ norm_Rational, |
262 Rule.Rls_ (*order_add_mult_in*) norm_System (**1**), |
262 Rule.Rls_ (*order_add_mult_in*) norm_System (**1**), |
263 Rule.Rls_ discard_parentheses, |
263 Rule.Rls_ discard_parentheses, |
272 *) |
272 *) |
273 \<close> |
273 \<close> |
274 ML \<open> |
274 ML \<open> |
275 val isolate_bdvs = |
275 val isolate_bdvs = |
276 Rule_Def.Repeat { |
276 Rule_Def.Repeat { |
277 id="isolate_bdvs", preconds = [], rew_ord = ("e_rew_ord", Rewrite_Ord.e_rew_ord), |
277 id="isolate_bdvs", preconds = [], rew_ord = ("Rewrite_Ord.id_empty", Rewrite_Ord.function_empty), |
278 erls = Rule_Set.append_rules "erls_isolate_bdvs" Rule_Set.empty [ |
278 erls = Rule_Set.append_rules "erls_isolate_bdvs" Rule_Set.empty [ |
279 (\<^rule_eval>\<open>occur_exactly_in\<close> (eval_occur_exactly_in "#eval_occur_exactly_in_"))], |
279 (\<^rule_eval>\<open>occur_exactly_in\<close> (eval_occur_exactly_in "#eval_occur_exactly_in_"))], |
280 srls = Rule_Set.Empty, calc = [], errpatts = [], |
280 srls = Rule_Set.Empty, calc = [], errpatts = [], |
281 rules = [ |
281 rules = [ |
282 \<^rule_thm>\<open>commute_0_equality\<close>, |
282 \<^rule_thm>\<open>commute_0_equality\<close>, |
285 scr = Rule.Empty_Prog}; |
285 scr = Rule.Empty_Prog}; |
286 \<close> |
286 \<close> |
287 ML \<open> |
287 ML \<open> |
288 val isolate_bdvs_4x4 = |
288 val isolate_bdvs_4x4 = |
289 Rule_Def.Repeat {id="isolate_bdvs_4x4", preconds = [], |
289 Rule_Def.Repeat {id="isolate_bdvs_4x4", preconds = [], |
290 rew_ord = ("e_rew_ord", Rewrite_Ord.e_rew_ord), |
290 rew_ord = ("Rewrite_Ord.id_empty", Rewrite_Ord.function_empty), |
291 erls = Rule_Set.append_rules "erls_isolate_bdvs_4x4" Rule_Set.empty [ |
291 erls = Rule_Set.append_rules "erls_isolate_bdvs_4x4" Rule_Set.empty [ |
292 \<^rule_eval>\<open>occur_exactly_in\<close> (eval_occur_exactly_in "#eval_occur_exactly_in_"), |
292 \<^rule_eval>\<open>occur_exactly_in\<close> (eval_occur_exactly_in "#eval_occur_exactly_in_"), |
293 \<^rule_eval>\<open>Prog_Expr.ident\<close> (Prog_Expr.eval_ident "#ident_"), |
293 \<^rule_eval>\<open>Prog_Expr.ident\<close> (Prog_Expr.eval_ident "#ident_"), |
294 \<^rule_eval>\<open>Prog_Expr.some_occur_in\<close> (Prog_Expr.eval_some_occur_in "#some_occur_in_"), |
294 \<^rule_eval>\<open>Prog_Expr.some_occur_in\<close> (Prog_Expr.eval_some_occur_in "#some_occur_in_"), |
295 \<^rule_thm>\<open>not_true\<close>, |
295 \<^rule_thm>\<open>not_true\<close>, |
316 \<^rule_thm>\<open>order_system_NxN\<close>], |
316 \<^rule_thm>\<open>order_system_NxN\<close>], |
317 scr = Rule.Empty_Prog}; |
317 scr = Rule.Empty_Prog}; |
318 |
318 |
319 val prls_triangular = |
319 val prls_triangular = |
320 Rule_Def.Repeat { |
320 Rule_Def.Repeat { |
321 id="prls_triangular", preconds = [], rew_ord = ("e_rew_ord", Rewrite_Ord.e_rew_ord), |
321 id="prls_triangular", preconds = [], rew_ord = ("Rewrite_Ord.id_empty", Rewrite_Ord.function_empty), |
322 erls = Rule_Def.Repeat { |
322 erls = Rule_Def.Repeat { |
323 id="erls_prls_triangular", preconds = [], rew_ord = ("e_rew_ord", Rewrite_Ord.e_rew_ord), |
323 id="erls_prls_triangular", preconds = [], rew_ord = ("Rewrite_Ord.id_empty", Rewrite_Ord.function_empty), |
324 erls = Rule_Set.Empty, srls = Rule_Set.Empty, calc = [], errpatts = [], |
324 erls = Rule_Set.Empty, srls = Rule_Set.Empty, calc = [], errpatts = [], |
325 rules = [(*for precond NTH_CONS ...*) |
325 rules = [(*for precond NTH_CONS ...*) |
326 \<^rule_eval>\<open>less\<close> (Prog_Expr.eval_equ "#less_"), |
326 \<^rule_eval>\<open>less\<close> (Prog_Expr.eval_equ "#less_"), |
327 \<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_"), |
327 \<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_"), |
328 \<^rule_eval>\<open>occur_exactly_in\<close> (eval_occur_exactly_in "#eval_occur_exactly_in_")], |
328 \<^rule_eval>\<open>occur_exactly_in\<close> (eval_occur_exactly_in "#eval_occur_exactly_in_")], |
342 |
342 |
343 (*WN060914 quickly created for 4x4; |
343 (*WN060914 quickly created for 4x4; |
344 more similarity to prls_triangular desirable*) |
344 more similarity to prls_triangular desirable*) |
345 val prls_triangular4 = |
345 val prls_triangular4 = |
346 Rule_Def.Repeat { |
346 Rule_Def.Repeat { |
347 id="prls_triangular4", preconds = [], rew_ord = ("e_rew_ord", Rewrite_Ord.e_rew_ord), |
347 id="prls_triangular4", preconds = [], rew_ord = ("Rewrite_Ord.id_empty", Rewrite_Ord.function_empty), |
348 erls = Rule_Def.Repeat { |
348 erls = Rule_Def.Repeat { |
349 id="erls_prls_triangular4", preconds = [], rew_ord = ("e_rew_ord", Rewrite_Ord.e_rew_ord), |
349 id="erls_prls_triangular4", preconds = [], rew_ord = ("Rewrite_Ord.id_empty", Rewrite_Ord.function_empty), |
350 erls = Rule_Set.Empty, srls = Rule_Set.Empty, calc = [], errpatts = [], |
350 erls = Rule_Set.Empty, srls = Rule_Set.Empty, calc = [], errpatts = [], |
351 rules = [(*for precond NTH_CONS ...*) |
351 rules = [(*for precond NTH_CONS ...*) |
352 \<^rule_eval>\<open>less\<close> (Prog_Expr.eval_equ "#less_"), |
352 \<^rule_eval>\<open>less\<close> (Prog_Expr.eval_equ "#less_"), |
353 \<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_")], |
353 \<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_")], |
354 (*immediately repeated rewrite pushes '+' into precondition !*) |
354 (*immediately repeated rewrite pushes '+' into precondition !*) |