1.1 --- a/src/Tools/isac/Knowledge/Integrate.thy Mon Aug 09 14:20:20 2021 +0200
1.2 +++ b/src/Tools/isac/Knowledge/Integrate.thy Tue Aug 10 09:43:07 2021 +0200
1.3 @@ -44,7 +44,7 @@
1.4 (** eval functions **)
1.5
1.6 val c = Free ("c", HOLogic.realT);
1.7 -(*.create a new unique variable 'c..' in a term; for use by Rule.Eval in a rls;
1.8 +(*.create a new unique variable 'c..' in a term; for use by \<^rule_eval> in a rls;
1.9 an alternative to do this would be '(Try (Calculate new_c_) (new_c es__))'
1.10 in the script; this will be possible if currying doesnt take the value
1.11 from a variable, but the value '(new_c es__)' itself.*)
1.12 @@ -111,50 +111,45 @@
1.13
1.14 (*.rulesets for integration.*)
1.15 val integration_rules =
1.16 - Rule_Def.Repeat {id="integration_rules", preconds = [],
1.17 - rew_ord = ("termlessI",termlessI),
1.18 - erls = Rule_Def.Repeat {id="conditions_in_integration_rules",
1.19 - preconds = [],
1.20 - rew_ord = ("termlessI",termlessI),
1.21 - erls = Rule_Set.Empty,
1.22 - srls = Rule_Set.Empty, calc = [], errpatts = [],
1.23 - rules = [(*for rewriting conditions in Thm's*)
1.24 - \<^rule_eval>\<open>Prog_Expr.occurs_in\<close> (Prog_Expr.eval_occurs_in "#occurs_in_"),
1.25 - \<^rule_thm>\<open>not_true\<close>,
1.26 - \<^rule_thm>\<open>not_false\<close>
1.27 - ],
1.28 - scr = Rule.Empty_Prog},
1.29 - srls = Rule_Set.Empty, calc = [], errpatts = [],
1.30 - rules = [
1.31 - \<^rule_thm>\<open>integral_const\<close>,
1.32 - \<^rule_thm>\<open>integral_var\<close>,
1.33 - \<^rule_thm>\<open>integral_add\<close>,
1.34 - \<^rule_thm>\<open>integral_mult\<close>,
1.35 - \<^rule_thm>\<open>integral_pow\<close>,
1.36 - \<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_")(*for n+1*)
1.37 - ],
1.38 - scr = Rule.Empty_Prog};
1.39 + Rule_Def.Repeat {id="integration_rules", preconds = [],
1.40 + rew_ord = ("termlessI",termlessI),
1.41 + erls = Rule_Def.Repeat {id="conditions_in_integration_rules",
1.42 + preconds = [],
1.43 + rew_ord = ("termlessI",termlessI),
1.44 + erls = Rule_Set.Empty,
1.45 + srls = Rule_Set.Empty, calc = [], errpatts = [],
1.46 + rules = [(*for rewriting conditions in Thm's*)
1.47 + \<^rule_eval>\<open>Prog_Expr.occurs_in\<close> (Prog_Expr.eval_occurs_in "#occurs_in_"),
1.48 + \<^rule_thm>\<open>not_true\<close>,
1.49 + \<^rule_thm>\<open>not_false\<close>],
1.50 + scr = Rule.Empty_Prog},
1.51 + srls = Rule_Set.Empty, calc = [], errpatts = [],
1.52 + rules = [
1.53 + \<^rule_thm>\<open>integral_const\<close>,
1.54 + \<^rule_thm>\<open>integral_var\<close>,
1.55 + \<^rule_thm>\<open>integral_add\<close>,
1.56 + \<^rule_thm>\<open>integral_mult\<close>,
1.57 + \<^rule_thm>\<open>integral_pow\<close>,
1.58 + \<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_")(*for n+1*)],
1.59 + scr = Rule.Empty_Prog};
1.60 \<close>
1.61 ML \<open>
1.62 val add_new_c =
1.63 - Rule_Set.Sequence {id="add_new_c", preconds = [],
1.64 - rew_ord = ("termlessI",termlessI),
1.65 - erls = Rule_Def.Repeat {id="conditions_in_add_new_c",
1.66 - preconds = [],
1.67 - rew_ord = ("termlessI",termlessI),
1.68 - erls = Rule_Set.Empty,
1.69 - srls = Rule_Set.Empty, calc = [], errpatts = [],
1.70 - rules = [\<^rule_eval>\<open>Prog_Expr.matches\<close> (Prog_Expr.eval_matches""),
1.71 - \<^rule_eval>\<open>Integrate.is_f_x\<close> (eval_is_f_x "is_f_x_"),
1.72 - \<^rule_thm>\<open>not_true\<close>,
1.73 - \<^rule_thm>\<open>not_false\<close>
1.74 - ],
1.75 - scr = Rule.Empty_Prog},
1.76 - srls = Rule_Set.Empty, calc = [], errpatts = [],
1.77 - rules = [ (*\<^rule_thm>\<open>call_for_new_c\<close>,*)
1.78 - Rule.Cal1 ("Integrate.add_new_c", eval_add_new_c "new_c_")
1.79 - ],
1.80 - scr = Rule.Empty_Prog};
1.81 + Rule_Set.Sequence {id="add_new_c", preconds = [],
1.82 + rew_ord = ("termlessI",termlessI),
1.83 + erls = Rule_Def.Repeat {id="conditions_in_add_new_c",
1.84 + preconds = [], rew_ord = ("termlessI",termlessI), erls = Rule_Set.Empty,
1.85 + srls = Rule_Set.Empty, calc = [], errpatts = [],
1.86 + rules = [
1.87 + \<^rule_eval>\<open>Prog_Expr.matches\<close> (Prog_Expr.eval_matches""),
1.88 + \<^rule_eval>\<open>Integrate.is_f_x\<close> (eval_is_f_x "is_f_x_"),
1.89 + \<^rule_thm>\<open>not_true\<close>,
1.90 + \<^rule_thm>\<open>not_false\<close>],
1.91 + scr = Rule.Empty_Prog},
1.92 + srls = Rule_Set.Empty, calc = [], errpatts = [],
1.93 + rules = [ (*\<^rule_thm>\<open>call_for_new_c\<close>,*)
1.94 + Rule.Cal1 ("Integrate.add_new_c", eval_add_new_c "new_c_")],
1.95 + scr = Rule.Empty_Prog};
1.96 \<close>
1.97 ML \<open>
1.98
1.99 @@ -162,58 +157,45 @@
1.100
1.101 (*.for simplify_Integral adapted from 'norm_Rational_rls'.*)
1.102 val norm_Rational_rls_noadd_fractions =
1.103 -Rule_Def.Repeat {id = "norm_Rational_rls_noadd_fractions", preconds = [],
1.104 - rew_ord = ("dummy_ord",Rewrite_Ord.dummy_ord),
1.105 - erls = norm_rat_erls, srls = Rule_Set.Empty, calc = [], errpatts = [],
1.106 - rules = [(*Rule.Rls_ add_fractions_p_rls,!!!*)
1.107 - Rule.Rls_ (*rat_mult_div_pow original corrected WN051028*)
1.108 - (Rule_Def.Repeat {id = "rat_mult_div_pow", preconds = [],
1.109 - rew_ord = ("dummy_ord",Rewrite_Ord.dummy_ord),
1.110 - erls = (*FIXME.WN051028 Rule_Set.empty,*)
1.111 - Rule_Set.append_rules "Rule_Set.empty-is_polyexp" Rule_Set.empty
1.112 - [\<^rule_eval>\<open>is_polyexp\<close> (eval_is_polyexp "")],
1.113 - srls = Rule_Set.Empty, calc = [], errpatts = [],
1.114 - rules = [\<^rule_thm>\<open>rat_mult\<close>,
1.115 - (*"?a / ?b * (?c / ?d) = ?a * ?c / (?b * ?d)"*)
1.116 - \<^rule_thm>\<open>rat_mult_poly_l\<close>,
1.117 - (*"?c is_polyexp ==> ?c * (?a / ?b) = ?c * ?a / ?b"*)
1.118 - \<^rule_thm>\<open>rat_mult_poly_r\<close>,
1.119 - (*"?c is_polyexp ==> ?a / ?b * ?c = ?a * ?c / ?b"*)
1.120 -
1.121 - \<^rule_thm>\<open>real_divide_divide1_mg\<close>,
1.122 - (*"y ~= 0 ==> (u / v) / (y / z) = (u * z) / (y * v)"*)
1.123 - \<^rule_thm>\<open>divide_divide_eq_right\<close>,
1.124 - (*"?x / (?y / ?z) = ?x * ?z / ?y"*)
1.125 - \<^rule_thm>\<open>divide_divide_eq_left\<close>,
1.126 - (*"?x / ?y / ?z = ?x / (?y * ?z)"*)
1.127 - \<^rule_eval>\<open>divide\<close> (Prog_Expr.eval_cancel "#divide_e"),
1.128 -
1.129 - \<^rule_thm>\<open>rat_power\<close>
1.130 - (*"(?a / ?b) \<up> ?n = ?a \<up> ?n / ?b \<up> ?n"*)
1.131 - ],
1.132 - scr = Rule.Empty_Prog
1.133 - }),
1.134 - Rule.Rls_ make_rat_poly_with_parentheses,
1.135 - Rule.Rls_ cancel_p_rls,(*FIXME:cancel_p does NOT order sometimes*)
1.136 - Rule.Rls_ rat_reduce_1
1.137 - ],
1.138 - scr = Rule.Empty_Prog
1.139 - };
1.140 + Rule_Def.Repeat {id = "norm_Rational_rls_noadd_fractions", preconds = [],
1.141 + rew_ord = ("dummy_ord",Rewrite_Ord.dummy_ord),
1.142 + erls = norm_rat_erls, srls = Rule_Set.Empty, calc = [], errpatts = [],
1.143 + rules = [(*Rule.Rls_ add_fractions_p_rls,!!!*)
1.144 + Rule.Rls_ (*rat_mult_div_pow original corrected WN051028*)
1.145 + (Rule_Def.Repeat {id = "rat_mult_div_pow", preconds = [],
1.146 + rew_ord = ("dummy_ord",Rewrite_Ord.dummy_ord),
1.147 + erls = Rule_Set.append_rules "Rule_Set.empty-is_polyexp" Rule_Set.empty
1.148 + [\<^rule_eval>\<open>is_polyexp\<close> (eval_is_polyexp "")],
1.149 + srls = Rule_Set.Empty, calc = [], errpatts = [],
1.150 + rules = [
1.151 + \<^rule_thm>\<open>rat_mult\<close>, (*"?a / ?b * (?c / ?d) = ?a * ?c / (?b * ?d)"*)
1.152 + \<^rule_thm>\<open>rat_mult_poly_l\<close>, (*"?c is_polyexp ==> ?c * (?a / ?b) = ?c * ?a / ?b"*)
1.153 + \<^rule_thm>\<open>rat_mult_poly_r\<close>, (*"?c is_polyexp ==> ?a / ?b * ?c = ?a * ?c / ?b"*)
1.154 +
1.155 + \<^rule_thm>\<open>real_divide_divide1_mg\<close>, (*"y ~= 0 ==> (u / v) / (y / z) = (u * z) / (y * v)"*)
1.156 + \<^rule_thm>\<open>divide_divide_eq_right\<close>, (*"?x / (?y / ?z) = ?x * ?z / ?y"*)
1.157 + \<^rule_thm>\<open>divide_divide_eq_left\<close>, (*"?x / ?y / ?z = ?x / (?y * ?z)"*)
1.158 + \<^rule_eval>\<open>divide\<close> (Prog_Expr.eval_cancel "#divide_e"),
1.159 +
1.160 + \<^rule_thm>\<open>rat_power\<close>], (*"(?a / ?b) \<up> ?n = ?a \<up> ?n / ?b \<up> ?n"*)
1.161 + scr = Rule.Empty_Prog}),
1.162 + Rule.Rls_ make_rat_poly_with_parentheses,
1.163 + Rule.Rls_ cancel_p_rls,(*FIXME:cancel_p does NOT order sometimes*)
1.164 + Rule.Rls_ rat_reduce_1],
1.165 + scr = Rule.Empty_Prog};
1.166
1.167 (*.for simplify_Integral adapted from 'norm_Rational'.*)
1.168 val norm_Rational_noadd_fractions =
1.169 - Rule_Set.Sequence {id = "norm_Rational_noadd_fractions", preconds = [],
1.170 - rew_ord = ("dummy_ord",Rewrite_Ord.dummy_ord),
1.171 - erls = norm_rat_erls, srls = Rule_Set.Empty, calc = [], errpatts = [],
1.172 - rules = [Rule.Rls_ discard_minus,
1.173 - Rule.Rls_ rat_mult_poly,(* removes double fractions like a/b/c *)
1.174 - Rule.Rls_ make_rat_poly_with_parentheses, (*WN0510 also in(#)below*)
1.175 - Rule.Rls_ cancel_p_rls, (*FIXME.MG:cancel_p does NOT order sometim*)
1.176 - Rule.Rls_ norm_Rational_rls_noadd_fractions,(* the main rls (#) *)
1.177 - Rule.Rls_ discard_parentheses1 (* mult only *)
1.178 - ],
1.179 - scr = Rule.Empty_Prog
1.180 - };
1.181 + Rule_Set.Sequence {id = "norm_Rational_noadd_fractions", preconds = [],
1.182 + rew_ord = ("dummy_ord",Rewrite_Ord.dummy_ord),
1.183 + erls = norm_rat_erls, srls = Rule_Set.Empty, calc = [], errpatts = [],
1.184 + rules = [Rule.Rls_ discard_minus,
1.185 + Rule.Rls_ rat_mult_poly,(* removes double fractions like a/b/c *)
1.186 + Rule.Rls_ make_rat_poly_with_parentheses, (*WN0510 also in(#)below*)
1.187 + Rule.Rls_ cancel_p_rls, (*FIXME.MG:cancel_p does NOT order sometim*)
1.188 + Rule.Rls_ norm_Rational_rls_noadd_fractions,(* the main rls (#) *)
1.189 + Rule.Rls_ discard_parentheses1], (* mult only *)
1.190 + scr = Rule.Empty_Prog};
1.191
1.192 (*.simplify terms before and after Integration such that
1.193 ..a.x^2/2 + b.x^3/3.. is made to ..a/2.x^2 + b/3.x^3.. (and NO
1.194 @@ -222,92 +204,44 @@
1.195 *1* expand the term, ie. distribute * and / over +
1.196 .*)
1.197 val separate_bdv2 =
1.198 - Rule_Set.append_rules "separate_bdv2"
1.199 - collect_bdv
1.200 - [\<^rule_thm>\<open>separate_bdv\<close>,
1.201 - (*"?a * ?bdv / ?b = ?a / ?b * ?bdv"*)
1.202 + Rule_Set.append_rules "separate_bdv2" collect_bdv [
1.203 + \<^rule_thm>\<open>separate_bdv\<close>, (*"?a * ?bdv / ?b = ?a / ?b * ?bdv"*)
1.204 \<^rule_thm>\<open>separate_bdv_n\<close>,
1.205 - \<^rule_thm>\<open>separate_1_bdv\<close>,
1.206 - (*"?bdv / ?b = (1 / ?b) * ?bdv"*)
1.207 - \<^rule_thm>\<open>separate_1_bdv_n\<close>(*,
1.208 - (*"?bdv \<up> ?n / ?b = 1 / ?b * ?bdv \<up> ?n"*)
1.209 - *****\<^rule_thm>\<open>add_divide_distrib\<close>
1.210 - (*"(?x + ?y) / ?z = ?x / ?z + ?y / ?z"*)----------*)
1.211 + \<^rule_thm>\<open>separate_1_bdv\<close>, (*"?bdv / ?b = (1 / ?b) * ?bdv"*)
1.212 + \<^rule_thm>\<open>separate_1_bdv_n\<close> (*"?bdv \<up> ?n / ?b = 1 / ?b * ?bdv \<up> ?n"*)
1.213 + (*
1.214 + rule_thm>\<open>add_divide_distrib\<close> (*"(?x + ?y) / ?z = ?x / ?z + ?y / ?z"*)*)
1.215 ];
1.216 val simplify_Integral =
1.217 Rule_Set.Sequence {id = "simplify_Integral", preconds = []:term list,
1.218 - rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord),
1.219 - erls = Atools_erls, srls = Rule_Set.Empty,
1.220 - calc = [], errpatts = [],
1.221 - rules = [\<^rule_thm>\<open>distrib_right\<close>,
1.222 - (*"(?z1.0 + ?z2.0) * ?w = ?z1.0 * ?w + ?z2.0 * ?w"*)
1.223 - \<^rule_thm>\<open>add_divide_distrib\<close>,
1.224 - (*"(?x + ?y) / ?z = ?x / ?z + ?y / ?z"*)
1.225 - (*^^^^^ *1* ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^*)
1.226 - Rule.Rls_ norm_Rational_noadd_fractions,
1.227 - Rule.Rls_ order_add_mult_in,
1.228 - Rule.Rls_ discard_parentheses,
1.229 - (*Rule.Rls_ collect_bdv, from make_polynomial_in*)
1.230 - Rule.Rls_ separate_bdv2,
1.231 - \<^rule_eval>\<open>divide\<close> (Prog_Expr.eval_cancel "#divide_e")
1.232 - ],
1.233 - scr = Rule.Empty_Prog};
1.234 + rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord),
1.235 + erls = Atools_erls, srls = Rule_Set.Empty,
1.236 + calc = [], errpatts = [],
1.237 + rules = [
1.238 + \<^rule_thm>\<open>distrib_right\<close>, (*"(?z1.0 + ?z2.0) * ?w = ?z1.0 * ?w + ?z2.0 * ?w"*)
1.239 + \<^rule_thm>\<open>add_divide_distrib\<close>, (*"(?x + ?y) / ?z = ?x / ?z + ?y / ?z"*)
1.240 + (*^^^^^ *1* ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^*)
1.241 + Rule.Rls_ norm_Rational_noadd_fractions,
1.242 + Rule.Rls_ order_add_mult_in,
1.243 + Rule.Rls_ discard_parentheses,
1.244 + (*Rule.Rls_ collect_bdv, from make_polynomial_in*)
1.245 + Rule.Rls_ separate_bdv2,
1.246 + \<^rule_eval>\<open>divide\<close> (Prog_Expr.eval_cancel "#divide_e")],
1.247 + scr = Rule.Empty_Prog};
1.248
1.249 -
1.250 -(*simplify terms before and after Integration such that
1.251 - ..a.x^2/2 + b.x^3/3.. is made to ..a/2.x^2 + b/3.x^3.. (and NO
1.252 - common denominator as done by norm_Rational or make_ratpoly_in.
1.253 - This is a copy from 'make_polynomial_in' with insertions from
1.254 - 'make_ratpoly_in'
1.255 -THIS IS KEPT FOR COMPARISON ............................................
1.256 -* val simplify_Integral = prep_rls'(
1.257 -* Rule_Set.Sequence {id = "", preconds = []:term list,
1.258 -* rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord),
1.259 -* erls = Atools_erls, srls = Rule_Set.Empty,
1.260 -* calc = [], (*asm_thm = [],*)
1.261 -* rules = [Rule.Rls_ expand_poly,
1.262 -* Rule.Rls_ order_add_mult_in,
1.263 -* Rule.Rls_ simplify_power,
1.264 -* Rule.Rls_ collect_numerals,
1.265 -* Rule.Rls_ reduce_012,
1.266 -* \<^rule_thm>\<open>realpow_oneI\<close>,
1.267 -* Rule.Rls_ discard_parentheses,
1.268 -* Rule.Rls_ collect_bdv,
1.269 -* (*below inserted from 'make_ratpoly_in'*)
1.270 -* Rule.Rls_ (Rule_Set.append_rules "separate_bdv"
1.271 -* collect_bdv
1.272 -* [\<^rule_thm>\<open>separate_bdv\<close>,
1.273 -* (*"?a * ?bdv / ?b = ?a / ?b * ?bdv"*)
1.274 -* \<^rule_thm>\<open>separate_bdv_n\<close>,
1.275 -* \<^rule_thm>\<open>separate_1_bdv\<close>,
1.276 -* (*"?bdv / ?b = (1 / ?b) * ?bdv"*)
1.277 -* \<^rule_thm>\<open>separate_1_bdv_n\<close>(*,
1.278 -* (*"?bdv \<up> ?n / ?b = 1 / ?b * ?bdv \<up> ?n"*)
1.279 -* \<^rule_thm>\<open>add_divide_distrib\<close>
1.280 -* (*"(?x + ?y) / ?z = ?x / ?z + ?y / ?z"*)*)
1.281 -* ]),
1.282 -* \<^rule_eval>\<open>divide\<close> (eval_cancel "#divide_e")
1.283 -* ],
1.284 -* scr = Rule.Empty_Prog
1.285 -* });
1.286 -.......................................................................*)
1.287 -
1.288 -val integration =
1.289 - Rule_Set.Sequence {id="integration", preconds = [],
1.290 - rew_ord = ("termlessI",termlessI),
1.291 - erls = Rule_Def.Repeat {id="conditions_in_integration",
1.292 - preconds = [],
1.293 - rew_ord = ("termlessI",termlessI),
1.294 - erls = Rule_Set.Empty,
1.295 - srls = Rule_Set.Empty, calc = [], errpatts = [],
1.296 - rules = [],
1.297 - scr = Rule.Empty_Prog},
1.298 - srls = Rule_Set.Empty, calc = [], errpatts = [],
1.299 - rules = [ Rule.Rls_ integration_rules,
1.300 - Rule.Rls_ add_new_c,
1.301 - Rule.Rls_ simplify_Integral
1.302 - ],
1.303 - scr = Rule.Empty_Prog};
1.304 +val integration =
1.305 + Rule_Set.Sequence {
1.306 + id="integration", preconds = [], rew_ord = ("termlessI",termlessI),
1.307 + erls = Rule_Def.Repeat {
1.308 + id="conditions_in_integration", preconds = [], rew_ord = ("termlessI",termlessI),
1.309 + erls = Rule_Set.Empty, srls = Rule_Set.Empty, calc = [], errpatts = [],
1.310 + rules = [], scr = Rule.Empty_Prog},
1.311 + srls = Rule_Set.Empty, calc = [], errpatts = [],
1.312 + rules = [
1.313 + Rule.Rls_ integration_rules,
1.314 + Rule.Rls_ add_new_c,
1.315 + Rule.Rls_ simplify_Integral],
1.316 + scr = Rule.Empty_Prog};
1.317
1.318 val prep_rls' = Auto_Prog.prep_rls @{theory};
1.319 \<close>