1.1 --- a/src/Tools/isac/Knowledge/Integrate.thy Wed Apr 01 19:20:05 2020 +0200
1.2 +++ b/src/Tools/isac/Knowledge/Integrate.thy Sat Apr 04 12:11:32 2020 +0200
1.3 @@ -110,20 +110,20 @@
1.4
1.5 (*.rulesets for integration.*)
1.6 val integration_rules =
1.7 - Rule.Rls {id="integration_rules", preconds = [],
1.8 + Rule_Set.Rls {id="integration_rules", preconds = [],
1.9 rew_ord = ("termlessI",termlessI),
1.10 - erls = Rule.Rls {id="conditions_in_integration_rules",
1.11 + erls = Rule_Set.Rls {id="conditions_in_integration_rules",
1.12 preconds = [],
1.13 rew_ord = ("termlessI",termlessI),
1.14 - erls = Rule.Erls,
1.15 - srls = Rule.Erls, calc = [], errpatts = [],
1.16 + erls = Rule_Set.Erls,
1.17 + srls = Rule_Set.Erls, 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.Erls, calc = [], errpatts = [],
1.25 + srls = Rule_Set.Erls, 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.Seq {id="add_new_c", preconds = [],
1.34 + Rule_Set.Seq {id="add_new_c", preconds = [],
1.35 rew_ord = ("termlessI",termlessI),
1.36 - erls = Rule.Rls {id="conditions_in_add_new_c",
1.37 + erls = Rule_Set.Rls {id="conditions_in_add_new_c",
1.38 preconds = [],
1.39 rew_ord = ("termlessI",termlessI),
1.40 - erls = Rule.Erls,
1.41 - srls = Rule.Erls, calc = [], errpatts = [],
1.42 + erls = Rule_Set.Erls,
1.43 + srls = Rule_Set.Erls, 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.Erls, calc = [], errpatts = [],
1.52 + srls = Rule_Set.Erls, 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.Rls {id = "norm_Rational_rls_noadd_fractions", preconds = [],
1.61 +Rule_Set.Rls {id = "norm_Rational_rls_noadd_fractions", preconds = [],
1.62 rew_ord = ("dummy_ord",Rule.dummy_ord),
1.63 - erls = norm_rat_erls, srls = Rule.Erls, calc = [], errpatts = [],
1.64 + erls = norm_rat_erls, srls = Rule_Set.Erls, 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.Rls {id = "rat_mult_div_pow", preconds = [],
1.68 + (Rule_Set.Rls {id = "rat_mult_div_pow", preconds = [],
1.69 rew_ord = ("dummy_ord",Rule.dummy_ord),
1.70 - erls = (*FIXME.WN051028 Rule.e_rls,*)
1.71 - Rule.append_rls "Rule.e_rls-is_polyexp" Rule.e_rls
1.72 + erls = (*FIXME.WN051028 Rule_Set.e_rls,*)
1.73 + Rule_Set.append_rls "Rule_Set.e_rls-is_polyexp" Rule_Set.e_rls
1.74 [Rule.Num_Calc ("Poly.is'_polyexp",
1.75 eval_is_polyexp "")],
1.76 - srls = Rule.Erls, calc = [], errpatts = [],
1.77 + srls = Rule_Set.Erls, calc = [], errpatts = [],
1.78 rules = [Rule.Thm ("rat_mult", TermC.num_str @{thm rat_mult}),
1.79 (*"?a / ?b * (?c / ?d) = ?a * ?c / (?b * ?d)"*)
1.80 Rule.Thm ("rat_mult_poly_l", TermC.num_str @{thm rat_mult_poly_l}),
1.81 @@ -206,9 +206,9 @@
1.82
1.83 (*.for simplify_Integral adapted from 'norm_Rational'.*)
1.84 val norm_Rational_noadd_fractions =
1.85 - Rule.Seq {id = "norm_Rational_noadd_fractions", preconds = [],
1.86 + Rule_Set.Seq {id = "norm_Rational_noadd_fractions", preconds = [],
1.87 rew_ord = ("dummy_ord",Rule.dummy_ord),
1.88 - erls = norm_rat_erls, srls = Rule.Erls, calc = [], errpatts = [],
1.89 + erls = norm_rat_erls, srls = Rule_Set.Erls, calc = [], errpatts = [],
1.90 rules = [Rule.Rls_ discard_minus,
1.91 Rule.Rls_ rat_mult_poly,(* removes double fractions like a/b/c *)
1.92 Rule.Rls_ make_rat_poly_with_parentheses, (*WN0510 also in(#)below*)
1.93 @@ -226,7 +226,7 @@
1.94 *1* expand the term, ie. distribute * and / over +
1.95 .*)
1.96 val separate_bdv2 =
1.97 - Rule.append_rls "separate_bdv2"
1.98 + Rule_Set.append_rls "separate_bdv2"
1.99 collect_bdv
1.100 [Rule.Thm ("separate_bdv", TermC.num_str @{thm separate_bdv}),
1.101 (*"?a * ?bdv / ?b = ?a / ?b * ?bdv"*)
1.102 @@ -240,9 +240,9 @@
1.103 (*"(?x + ?y) / ?z = ?x / ?z + ?y / ?z"*)----------*)
1.104 ];
1.105 val simplify_Integral =
1.106 - Rule.Seq {id = "simplify_Integral", preconds = []:term list,
1.107 + Rule_Set.Seq {id = "simplify_Integral", preconds = []:term list,
1.108 rew_ord = ("dummy_ord", Rule.dummy_ord),
1.109 - erls = Atools_erls, srls = Rule.Erls,
1.110 + erls = Atools_erls, srls = Rule_Set.Erls,
1.111 calc = [], errpatts = [],
1.112 rules = [Rule.Thm ("distrib_right", TermC.num_str @{thm distrib_right}),
1.113 (*"(?z1.0 + ?z2.0) * ?w = ?z1.0 * ?w + ?z2.0 * ?w"*)
1.114 @@ -266,9 +266,9 @@
1.115 'make_ratpoly_in'
1.116 THIS IS KEPT FOR COMPARISON ............................................
1.117 * val simplify_Integral = prep_rls'(
1.118 -* Rule.Seq {id = "", preconds = []:term list,
1.119 +* Rule_Set.Seq {id = "", preconds = []:term list,
1.120 * rew_ord = ("dummy_ord", Rule.dummy_ord),
1.121 -* erls = Atools_erls, srls = Rule.Erls,
1.122 +* erls = Atools_erls, srls = Rule_Set.Erls,
1.123 * calc = [], (*asm_thm = [],*)
1.124 * rules = [Rule.Rls_ expand_poly,
1.125 * Rule.Rls_ order_add_mult_in,
1.126 @@ -279,7 +279,7 @@
1.127 * Rule.Rls_ discard_parentheses,
1.128 * Rule.Rls_ collect_bdv,
1.129 * (*below inserted from 'make_ratpoly_in'*)
1.130 -* Rule.Rls_ (Rule.append_rls "separate_bdv"
1.131 +* Rule.Rls_ (Rule_Set.append_rls "separate_bdv"
1.132 * collect_bdv
1.133 * [Rule.Thm ("separate_bdv", TermC.num_str @{thm separate_bdv}),
1.134 * (*"?a * ?bdv / ?b = ?a / ?b * ?bdv"*)
1.135 @@ -299,16 +299,16 @@
1.136 .......................................................................*)
1.137
1.138 val integration =
1.139 - Rule.Seq {id="integration", preconds = [],
1.140 + Rule_Set.Seq {id="integration", preconds = [],
1.141 rew_ord = ("termlessI",termlessI),
1.142 - erls = Rule.Rls {id="conditions_in_integration",
1.143 + erls = Rule_Set.Rls {id="conditions_in_integration",
1.144 preconds = [],
1.145 rew_ord = ("termlessI",termlessI),
1.146 - erls = Rule.Erls,
1.147 - srls = Rule.Erls, calc = [], errpatts = [],
1.148 + erls = Rule_Set.Erls,
1.149 + srls = Rule_Set.Erls, calc = [], errpatts = [],
1.150 rules = [],
1.151 scr = Rule.EmptyScr},
1.152 - srls = Rule.Erls, calc = [], errpatts = [],
1.153 + srls = Rule_Set.Erls, calc = [], errpatts = [],
1.154 rules = [ Rule.Rls_ integration_rules,
1.155 Rule.Rls_ add_new_c,
1.156 Rule.Rls_ simplify_Integral
1.157 @@ -335,7 +335,7 @@
1.158 (["integrate","function"],
1.159 [("#Given" ,["functionTerm f_f", "integrateBy v_v"]),
1.160 ("#Find" ,["antiDerivative F_F"])],
1.161 - Rule.append_rls "e_rls" Rule.e_rls [(*for preds in where_*)],
1.162 + Rule_Set.append_rls "e_rls" Rule_Set.e_rls [(*for preds in where_*)],
1.163 SOME "Integrate (f_f, v_v)",
1.164 [["diff","integration"]])),
1.165 (*here "named" is used differently from Differentiation"*)
1.166 @@ -343,7 +343,7 @@
1.167 (["named","integrate","function"],
1.168 [("#Given" ,["functionTerm f_f", "integrateBy v_v"]),
1.169 ("#Find" ,["antiDerivativeName F_F"])],
1.170 - Rule.append_rls "e_rls" Rule.e_rls [(*for preds in where_*)],
1.171 + Rule_Set.append_rls "e_rls" Rule_Set.e_rls [(*for preds in where_*)],
1.172 SOME "Integrate (f_f, v_v)",
1.173 [["diff","integration","named"]]))]\<close>
1.174
1.175 @@ -360,8 +360,8 @@
1.176 [Specify.prep_met thy "met_diffint" [] Celem.e_metID
1.177 (["diff","integration"],
1.178 [("#Given" ,["functionTerm f_f", "integrateBy v_v"]), ("#Find" ,["antiDerivative F_F"])],
1.179 - {rew_ord'="tless_true", rls'=Atools_erls, calc = [], srls = Rule.e_rls, prls=Rule.e_rls,
1.180 - crls = Atools_erls, errpats = [], nrls = Rule.e_rls},
1.181 + {rew_ord'="tless_true", rls'=Atools_erls, calc = [], srls = Rule_Set.e_rls, prls=Rule_Set.e_rls,
1.182 + crls = Atools_erls, errpats = [], nrls = Rule_Set.e_rls},
1.183 @{thm integrate.simps})]
1.184 \<close>
1.185
1.186 @@ -379,8 +379,8 @@
1.187 (["diff","integration","named"],
1.188 [("#Given" ,["functionTerm f_f", "integrateBy v_v"]),
1.189 ("#Find" ,["antiDerivativeName F_F"])],
1.190 - {rew_ord'="tless_true", rls'=Atools_erls, calc = [], srls = Rule.e_rls, prls=Rule.e_rls,
1.191 - crls = Atools_erls, errpats = [], nrls = Rule.e_rls},
1.192 + {rew_ord'="tless_true", rls'=Atools_erls, calc = [], srls = Rule_Set.e_rls, prls=Rule_Set.e_rls,
1.193 + crls = Atools_erls, errpats = [], nrls = Rule_Set.e_rls},
1.194 @{thm intergrate_named.simps})]
1.195 \<close>
1.196