1.1 --- a/src/Tools/isac/Knowledge/Integrate.thy Sat Apr 04 12:11:32 2020 +0200
1.2 +++ b/src/Tools/isac/Knowledge/Integrate.thy Mon Apr 06 11:44:36 2020 +0200
1.3 @@ -110,20 +110,20 @@
1.4
1.5 (*.rulesets for integration.*)
1.6 val integration_rules =
1.7 - Rule_Set.Rls {id="integration_rules", preconds = [],
1.8 + Rule_Def.Repeat {id="integration_rules", preconds = [],
1.9 rew_ord = ("termlessI",termlessI),
1.10 - erls = Rule_Set.Rls {id="conditions_in_integration_rules",
1.11 + erls = Rule_Def.Repeat {id="conditions_in_integration_rules",
1.12 preconds = [],
1.13 rew_ord = ("termlessI",termlessI),
1.14 - erls = Rule_Set.Erls,
1.15 - srls = Rule_Set.Erls, calc = [], errpatts = [],
1.16 + erls = Rule_Set.Empty,
1.17 + srls = Rule_Set.Empty, calc = [], errpatts = [],
1.18 rules = [(*for rewriting conditions in Thm's*)
1.19 Rule.Num_Calc ("Prog_Expr.occurs'_in", Prog_Expr.eval_occurs_in "#occurs_in_"),
1.20 Rule.Thm ("not_true", TermC.num_str @{thm not_true}),
1.21 Rule.Thm ("not_false",@{thm not_false})
1.22 ],
1.23 scr = Rule.EmptyScr},
1.24 - srls = Rule_Set.Erls, calc = [], errpatts = [],
1.25 + srls = Rule_Set.Empty, calc = [], errpatts = [],
1.26 rules = [
1.27 Rule.Thm ("integral_const", TermC.num_str @{thm integral_const}),
1.28 Rule.Thm ("integral_var", TermC.num_str @{thm integral_var}),
1.29 @@ -136,13 +136,13 @@
1.30 \<close>
1.31 ML \<open>
1.32 val add_new_c =
1.33 - Rule_Set.Seq {id="add_new_c", preconds = [],
1.34 + Rule_Set.Seqence {id="add_new_c", preconds = [],
1.35 rew_ord = ("termlessI",termlessI),
1.36 - erls = Rule_Set.Rls {id="conditions_in_add_new_c",
1.37 + erls = Rule_Def.Repeat {id="conditions_in_add_new_c",
1.38 preconds = [],
1.39 rew_ord = ("termlessI",termlessI),
1.40 - erls = Rule_Set.Erls,
1.41 - srls = Rule_Set.Erls, calc = [], errpatts = [],
1.42 + erls = Rule_Set.Empty,
1.43 + srls = Rule_Set.Empty, calc = [], errpatts = [],
1.44 rules = [Rule.Num_Calc ("Prog_Expr.matches", Prog_Expr.eval_matches""),
1.45 Rule.Num_Calc ("Integrate.is'_f'_x",
1.46 eval_is_f_x "is_f_x_"),
1.47 @@ -150,7 +150,7 @@
1.48 Rule.Thm ("not_false", TermC.num_str @{thm not_false})
1.49 ],
1.50 scr = Rule.EmptyScr},
1.51 - srls = Rule_Set.Erls, calc = [], errpatts = [],
1.52 + srls = Rule_Set.Empty, calc = [], errpatts = [],
1.53 rules = [ (*Rule.Thm ("call_for_new_c", TermC.num_str @{thm call_for_new_c}),*)
1.54 Rule.Cal1 ("Integrate.add'_new'_c", eval_add_new_c "new_c_")
1.55 ],
1.56 @@ -162,18 +162,18 @@
1.57
1.58 (*.for simplify_Integral adapted from 'norm_Rational_rls'.*)
1.59 val norm_Rational_rls_noadd_fractions =
1.60 -Rule_Set.Rls {id = "norm_Rational_rls_noadd_fractions", preconds = [],
1.61 +Rule_Def.Repeat {id = "norm_Rational_rls_noadd_fractions", preconds = [],
1.62 rew_ord = ("dummy_ord",Rule.dummy_ord),
1.63 - erls = norm_rat_erls, srls = Rule_Set.Erls, calc = [], errpatts = [],
1.64 + erls = norm_rat_erls, srls = Rule_Set.Empty, calc = [], errpatts = [],
1.65 rules = [(*Rule.Rls_ add_fractions_p_rls,!!!*)
1.66 Rule.Rls_ (*rat_mult_div_pow original corrected WN051028*)
1.67 - (Rule_Set.Rls {id = "rat_mult_div_pow", preconds = [],
1.68 + (Rule_Def.Repeat {id = "rat_mult_div_pow", preconds = [],
1.69 rew_ord = ("dummy_ord",Rule.dummy_ord),
1.70 erls = (*FIXME.WN051028 Rule_Set.e_rls,*)
1.71 Rule_Set.append_rls "Rule_Set.e_rls-is_polyexp" Rule_Set.e_rls
1.72 [Rule.Num_Calc ("Poly.is'_polyexp",
1.73 eval_is_polyexp "")],
1.74 - srls = Rule_Set.Erls, calc = [], errpatts = [],
1.75 + srls = Rule_Set.Empty, calc = [], errpatts = [],
1.76 rules = [Rule.Thm ("rat_mult", TermC.num_str @{thm rat_mult}),
1.77 (*"?a / ?b * (?c / ?d) = ?a * ?c / (?b * ?d)"*)
1.78 Rule.Thm ("rat_mult_poly_l", TermC.num_str @{thm rat_mult_poly_l}),
1.79 @@ -206,9 +206,9 @@
1.80
1.81 (*.for simplify_Integral adapted from 'norm_Rational'.*)
1.82 val norm_Rational_noadd_fractions =
1.83 - Rule_Set.Seq {id = "norm_Rational_noadd_fractions", preconds = [],
1.84 + Rule_Set.Seqence {id = "norm_Rational_noadd_fractions", preconds = [],
1.85 rew_ord = ("dummy_ord",Rule.dummy_ord),
1.86 - erls = norm_rat_erls, srls = Rule_Set.Erls, calc = [], errpatts = [],
1.87 + erls = norm_rat_erls, srls = Rule_Set.Empty, calc = [], errpatts = [],
1.88 rules = [Rule.Rls_ discard_minus,
1.89 Rule.Rls_ rat_mult_poly,(* removes double fractions like a/b/c *)
1.90 Rule.Rls_ make_rat_poly_with_parentheses, (*WN0510 also in(#)below*)
1.91 @@ -240,9 +240,9 @@
1.92 (*"(?x + ?y) / ?z = ?x / ?z + ?y / ?z"*)----------*)
1.93 ];
1.94 val simplify_Integral =
1.95 - Rule_Set.Seq {id = "simplify_Integral", preconds = []:term list,
1.96 + Rule_Set.Seqence {id = "simplify_Integral", preconds = []:term list,
1.97 rew_ord = ("dummy_ord", Rule.dummy_ord),
1.98 - erls = Atools_erls, srls = Rule_Set.Erls,
1.99 + erls = Atools_erls, srls = Rule_Set.Empty,
1.100 calc = [], errpatts = [],
1.101 rules = [Rule.Thm ("distrib_right", TermC.num_str @{thm distrib_right}),
1.102 (*"(?z1.0 + ?z2.0) * ?w = ?z1.0 * ?w + ?z2.0 * ?w"*)
1.103 @@ -266,9 +266,9 @@
1.104 'make_ratpoly_in'
1.105 THIS IS KEPT FOR COMPARISON ............................................
1.106 * val simplify_Integral = prep_rls'(
1.107 -* Rule_Set.Seq {id = "", preconds = []:term list,
1.108 +* Rule_Set.Seqence {id = "", preconds = []:term list,
1.109 * rew_ord = ("dummy_ord", Rule.dummy_ord),
1.110 -* erls = Atools_erls, srls = Rule_Set.Erls,
1.111 +* erls = Atools_erls, srls = Rule_Set.Empty,
1.112 * calc = [], (*asm_thm = [],*)
1.113 * rules = [Rule.Rls_ expand_poly,
1.114 * Rule.Rls_ order_add_mult_in,
1.115 @@ -299,16 +299,16 @@
1.116 .......................................................................*)
1.117
1.118 val integration =
1.119 - Rule_Set.Seq {id="integration", preconds = [],
1.120 + Rule_Set.Seqence {id="integration", preconds = [],
1.121 rew_ord = ("termlessI",termlessI),
1.122 - erls = Rule_Set.Rls {id="conditions_in_integration",
1.123 + erls = Rule_Def.Repeat {id="conditions_in_integration",
1.124 preconds = [],
1.125 rew_ord = ("termlessI",termlessI),
1.126 - erls = Rule_Set.Erls,
1.127 - srls = Rule_Set.Erls, calc = [], errpatts = [],
1.128 + erls = Rule_Set.Empty,
1.129 + srls = Rule_Set.Empty, calc = [], errpatts = [],
1.130 rules = [],
1.131 scr = Rule.EmptyScr},
1.132 - srls = Rule_Set.Erls, calc = [], errpatts = [],
1.133 + srls = Rule_Set.Empty, calc = [], errpatts = [],
1.134 rules = [ Rule.Rls_ integration_rules,
1.135 Rule.Rls_ add_new_c,
1.136 Rule.Rls_ simplify_Integral