156 (*.rulesets for simplifying Integrals.*) |
156 (*.rulesets for simplifying Integrals.*) |
157 |
157 |
158 (*.for simplify_Integral adapted from 'norm_Rational_rls'.*) |
158 (*.for simplify_Integral adapted from 'norm_Rational_rls'.*) |
159 val norm_Rational_rls_noadd_fractions = |
159 val norm_Rational_rls_noadd_fractions = |
160 Rule_Def.Repeat {id = "norm_Rational_rls_noadd_fractions", preconds = [], |
160 Rule_Def.Repeat {id = "norm_Rational_rls_noadd_fractions", preconds = [], |
161 rew_ord = ("dummy_ord",Rewrite_Ord.dummy_ord), |
161 rew_ord = ("dummy_ord",Rewrite_Ord.function_empty), |
162 erls = norm_rat_erls, srls = Rule_Set.Empty, calc = [], errpatts = [], |
162 erls = norm_rat_erls, srls = Rule_Set.Empty, calc = [], errpatts = [], |
163 rules = [(*Rule.Rls_ add_fractions_p_rls,!!!*) |
163 rules = [(*Rule.Rls_ add_fractions_p_rls,!!!*) |
164 Rule.Rls_ (*rat_mult_div_pow original corrected WN051028*) |
164 Rule.Rls_ (*rat_mult_div_pow original corrected WN051028*) |
165 (Rule_Def.Repeat {id = "rat_mult_div_pow", preconds = [], |
165 (Rule_Def.Repeat {id = "rat_mult_div_pow", preconds = [], |
166 rew_ord = ("dummy_ord",Rewrite_Ord.dummy_ord), |
166 rew_ord = ("dummy_ord",Rewrite_Ord.function_empty), |
167 erls = Rule_Set.append_rules "Rule_Set.empty-is_polyexp" Rule_Set.empty |
167 erls = Rule_Set.append_rules "Rule_Set.empty-is_polyexp" Rule_Set.empty |
168 [\<^rule_eval>\<open>is_polyexp\<close> (eval_is_polyexp "")], |
168 [\<^rule_eval>\<open>is_polyexp\<close> (eval_is_polyexp "")], |
169 srls = Rule_Set.Empty, calc = [], errpatts = [], |
169 srls = Rule_Set.Empty, calc = [], errpatts = [], |
170 rules = [ |
170 rules = [ |
171 \<^rule_thm>\<open>rat_mult\<close>, (*"?a / ?b * (?c / ?d) = ?a * ?c / (?b * ?d)"*) |
171 \<^rule_thm>\<open>rat_mult\<close>, (*"?a / ?b * (?c / ?d) = ?a * ?c / (?b * ?d)"*) |
185 scr = Rule.Empty_Prog}; |
185 scr = Rule.Empty_Prog}; |
186 |
186 |
187 (*.for simplify_Integral adapted from 'norm_Rational'.*) |
187 (*.for simplify_Integral adapted from 'norm_Rational'.*) |
188 val norm_Rational_noadd_fractions = |
188 val norm_Rational_noadd_fractions = |
189 Rule_Set.Sequence {id = "norm_Rational_noadd_fractions", preconds = [], |
189 Rule_Set.Sequence {id = "norm_Rational_noadd_fractions", preconds = [], |
190 rew_ord = ("dummy_ord",Rewrite_Ord.dummy_ord), |
190 rew_ord = ("dummy_ord",Rewrite_Ord.function_empty), |
191 erls = norm_rat_erls, srls = Rule_Set.Empty, calc = [], errpatts = [], |
191 erls = norm_rat_erls, srls = Rule_Set.Empty, calc = [], errpatts = [], |
192 rules = [Rule.Rls_ discard_minus, |
192 rules = [Rule.Rls_ discard_minus, |
193 Rule.Rls_ rat_mult_poly,(* removes double fractions like a/b/c *) |
193 Rule.Rls_ rat_mult_poly,(* removes double fractions like a/b/c *) |
194 Rule.Rls_ make_rat_poly_with_parentheses, (*WN0510 also in(#)below*) |
194 Rule.Rls_ make_rat_poly_with_parentheses, (*WN0510 also in(#)below*) |
195 Rule.Rls_ cancel_p_rls, (*FIXME.MG:cancel_p does NOT order sometim*) |
195 Rule.Rls_ cancel_p_rls, (*FIXME.MG:cancel_p does NOT order sometim*) |
212 (* |
212 (* |
213 rule_thm>\<open>add_divide_distrib\<close> (*"(?x + ?y) / ?z = ?x / ?z + ?y / ?z"*)*) |
213 rule_thm>\<open>add_divide_distrib\<close> (*"(?x + ?y) / ?z = ?x / ?z + ?y / ?z"*)*) |
214 ]; |
214 ]; |
215 val simplify_Integral = |
215 val simplify_Integral = |
216 Rule_Set.Sequence {id = "simplify_Integral", preconds = []:term list, |
216 Rule_Set.Sequence {id = "simplify_Integral", preconds = []:term list, |
217 rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord), |
217 rew_ord = ("dummy_ord", Rewrite_Ord.function_empty), |
218 erls = Atools_erls, srls = Rule_Set.Empty, |
218 erls = Atools_erls, srls = Rule_Set.Empty, |
219 calc = [], errpatts = [], |
219 calc = [], errpatts = [], |
220 rules = [ |
220 rules = [ |
221 \<^rule_thm>\<open>distrib_right\<close>, (*"(?z1.0 + ?z2.0) * ?w = ?z1.0 * ?w + ?z2.0 * ?w"*) |
221 \<^rule_thm>\<open>distrib_right\<close>, (*"(?z1.0 + ?z2.0) * ?w = ?z1.0 * ?w + ?z2.0 * ?w"*) |
222 \<^rule_thm>\<open>add_divide_distrib\<close>, (*"(?x + ?y) / ?z = ?x / ?z + ?y / ?z"*) |
222 \<^rule_thm>\<open>add_divide_distrib\<close>, (*"(?x + ?y) / ?z = ?x / ?z + ?y / ?z"*) |