1.1 --- a/src/Tools/isac/Knowledge/Integrate.thy Mon Oct 31 18:28:36 2022 +0100
1.2 +++ b/src/Tools/isac/Knowledge/Integrate.thy Mon Nov 07 17:37:20 2022 +0100
1.3 @@ -113,17 +113,17 @@
1.4 val integration_rules =
1.5 Rule_Def.Repeat {id="integration_rules", preconds = [],
1.6 rew_ord = ("termlessI",termlessI),
1.7 - erls = Rule_Def.Repeat {id="conditions_in_integration_rules",
1.8 + asm_rls = Rule_Def.Repeat {id="conditions_in_integration_rules",
1.9 preconds = [],
1.10 rew_ord = ("termlessI",termlessI),
1.11 - erls = Rule_Set.Empty,
1.12 - srls = Rule_Set.Empty, calc = [], errpatts = [],
1.13 + asm_rls = Rule_Set.Empty,
1.14 + prog_rls = Rule_Set.Empty, calc = [], errpatts = [],
1.15 rules = [(*for rewriting conditions in Thm's*)
1.16 \<^rule_eval>\<open>Prog_Expr.occurs_in\<close> (Prog_Expr.eval_occurs_in "#occurs_in_"),
1.17 \<^rule_thm>\<open>not_true\<close>,
1.18 \<^rule_thm>\<open>not_false\<close>],
1.19 - scr = Rule.Empty_Prog},
1.20 - srls = Rule_Set.Empty, calc = [], errpatts = [],
1.21 + program = Rule.Empty_Prog},
1.22 + prog_rls = Rule_Set.Empty, calc = [], errpatts = [],
1.23 rules = [
1.24 \<^rule_thm>\<open>integral_const\<close>,
1.25 \<^rule_thm>\<open>integral_var\<close>,
1.26 @@ -131,25 +131,25 @@
1.27 \<^rule_thm>\<open>integral_mult\<close>,
1.28 \<^rule_thm>\<open>integral_pow\<close>,
1.29 \<^rule_eval>\<open>plus\<close> (**)(Calc_Binop.numeric "#add_")(*for n+1*)],
1.30 - scr = Rule.Empty_Prog};
1.31 + program = Rule.Empty_Prog};
1.32 \<close>
1.33 ML \<open>
1.34 val add_new_c =
1.35 Rule_Set.Sequence {id="add_new_c", preconds = [],
1.36 rew_ord = ("termlessI",termlessI),
1.37 - erls = Rule_Def.Repeat {id="conditions_in_add_new_c",
1.38 - preconds = [], rew_ord = ("termlessI",termlessI), erls = Rule_Set.Empty,
1.39 - srls = Rule_Set.Empty, calc = [], errpatts = [],
1.40 + asm_rls = Rule_Def.Repeat {id="conditions_in_add_new_c",
1.41 + preconds = [], rew_ord = ("termlessI",termlessI), asm_rls = Rule_Set.Empty,
1.42 + prog_rls = Rule_Set.Empty, calc = [], errpatts = [],
1.43 rules = [
1.44 \<^rule_eval>\<open>Prog_Expr.matches\<close> (Prog_Expr.eval_matches""),
1.45 \<^rule_eval>\<open>Integrate.is_f_x\<close> (eval_is_f_x "is_f_x_"),
1.46 \<^rule_thm>\<open>not_true\<close>,
1.47 \<^rule_thm>\<open>not_false\<close>],
1.48 - scr = Rule.Empty_Prog},
1.49 - srls = Rule_Set.Empty, calc = [], errpatts = [],
1.50 + program = Rule.Empty_Prog},
1.51 + prog_rls = Rule_Set.Empty, calc = [], errpatts = [],
1.52 rules = [ (*\<^rule_thm>\<open>call_for_new_c\<close>,*)
1.53 Rule.Cal1 ("Integrate.add_new_c", eval_add_new_c "new_c_")],
1.54 - scr = Rule.Empty_Prog};
1.55 + program = Rule.Empty_Prog};
1.56 \<close>
1.57 ML \<open>
1.58
1.59 @@ -159,14 +159,14 @@
1.60 val norm_Rational_rls_noadd_fractions =
1.61 Rule_Def.Repeat {id = "norm_Rational_rls_noadd_fractions", preconds = [],
1.62 rew_ord = ("dummy_ord",Rewrite_Ord.function_empty),
1.63 - erls = norm_rat_erls, srls = Rule_Set.Empty, calc = [], errpatts = [],
1.64 + asm_rls = norm_rat_erls, prog_rls = 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_Def.Repeat {id = "rat_mult_div_pow", preconds = [],
1.68 rew_ord = ("dummy_ord",Rewrite_Ord.function_empty),
1.69 - erls = Rule_Set.append_rules "Rule_Set.empty-is_polyexp" Rule_Set.empty
1.70 + asm_rls = Rule_Set.append_rules "Rule_Set.empty-is_polyexp" Rule_Set.empty
1.71 [\<^rule_eval>\<open>is_polyexp\<close> (eval_is_polyexp "")],
1.72 - srls = Rule_Set.Empty, calc = [], errpatts = [],
1.73 + prog_rls = Rule_Set.Empty, calc = [], errpatts = [],
1.74 rules = [
1.75 \<^rule_thm>\<open>rat_mult\<close>, (*"?a / ?b * (?c / ?d) = ?a * ?c / (?b * ?d)"*)
1.76 \<^rule_thm>\<open>rat_mult_poly_l\<close>, (*"?c is_polyexp ==> ?c * (?a / ?b) = ?c * ?a / ?b"*)
1.77 @@ -178,24 +178,24 @@
1.78 \<^rule_eval>\<open>divide\<close> (Prog_Expr.eval_cancel "#divide_e"),
1.79
1.80 \<^rule_thm>\<open>rat_power\<close>], (*"(?a / ?b) \<up> ?n = ?a \<up> ?n / ?b \<up> ?n"*)
1.81 - scr = Rule.Empty_Prog}),
1.82 + program = Rule.Empty_Prog}),
1.83 Rule.Rls_ make_rat_poly_with_parentheses,
1.84 Rule.Rls_ cancel_p_rls,(*FIXME:cancel_p does NOT order sometimes*)
1.85 Rule.Rls_ rat_reduce_1],
1.86 - scr = Rule.Empty_Prog};
1.87 + program = Rule.Empty_Prog};
1.88
1.89 (*.for simplify_Integral adapted from 'norm_Rational'.*)
1.90 val norm_Rational_noadd_fractions =
1.91 Rule_Set.Sequence {id = "norm_Rational_noadd_fractions", preconds = [],
1.92 rew_ord = ("dummy_ord",Rewrite_Ord.function_empty),
1.93 - erls = norm_rat_erls, srls = Rule_Set.Empty, calc = [], errpatts = [],
1.94 + asm_rls = norm_rat_erls, prog_rls = Rule_Set.Empty, calc = [], errpatts = [],
1.95 rules = [Rule.Rls_ discard_minus,
1.96 Rule.Rls_ rat_mult_poly,(* removes double fractions like a/b/c *)
1.97 Rule.Rls_ make_rat_poly_with_parentheses, (*WN0510 also in(#)below*)
1.98 Rule.Rls_ cancel_p_rls, (*FIXME.MG:cancel_p does NOT order sometim*)
1.99 Rule.Rls_ norm_Rational_rls_noadd_fractions,(* the main rls (#) *)
1.100 Rule.Rls_ discard_parentheses1], (* mult only *)
1.101 - scr = Rule.Empty_Prog};
1.102 + program = Rule.Empty_Prog};
1.103
1.104 (*.simplify terms before and after Integration such that
1.105 ..a.x^2/2 + b.x^3/3.. is made to ..a/2.x^2 + b/3.x^3.. (and NO
1.106 @@ -215,7 +215,7 @@
1.107 val simplify_Integral =
1.108 Rule_Set.Sequence {id = "simplify_Integral", preconds = []:term list,
1.109 rew_ord = ("dummy_ord", Rewrite_Ord.function_empty),
1.110 - erls = Atools_erls, srls = Rule_Set.Empty,
1.111 + asm_rls = Atools_erls, prog_rls = Rule_Set.Empty,
1.112 calc = [], errpatts = [],
1.113 rules = [
1.114 \<^rule_thm>\<open>distrib_right\<close>, (*"(?z1.0 + ?z2.0) * ?w = ?z1.0 * ?w + ?z2.0 * ?w"*)
1.115 @@ -227,21 +227,21 @@
1.116 (*Rule.Rls_ collect_bdv, from make_polynomial_in*)
1.117 Rule.Rls_ separate_bdv2,
1.118 \<^rule_eval>\<open>divide\<close> (Prog_Expr.eval_cancel "#divide_e")],
1.119 - scr = Rule.Empty_Prog};
1.120 + program = Rule.Empty_Prog};
1.121
1.122 val integration =
1.123 Rule_Set.Sequence {
1.124 id="integration", preconds = [], rew_ord = ("termlessI",termlessI),
1.125 - erls = Rule_Def.Repeat {
1.126 + asm_rls = Rule_Def.Repeat {
1.127 id="conditions_in_integration", preconds = [], rew_ord = ("termlessI",termlessI),
1.128 - erls = Rule_Set.Empty, srls = Rule_Set.Empty, calc = [], errpatts = [],
1.129 - rules = [], scr = Rule.Empty_Prog},
1.130 - srls = Rule_Set.Empty, calc = [], errpatts = [],
1.131 + asm_rls = Rule_Set.Empty, prog_rls = Rule_Set.Empty, calc = [], errpatts = [],
1.132 + rules = [], program = Rule.Empty_Prog},
1.133 + prog_rls = Rule_Set.Empty, calc = [], errpatts = [],
1.134 rules = [
1.135 Rule.Rls_ integration_rules,
1.136 Rule.Rls_ add_new_c,
1.137 Rule.Rls_ simplify_Integral],
1.138 - scr = Rule.Empty_Prog};
1.139 + program = Rule.Empty_Prog};
1.140
1.141 val prep_rls' = Auto_Prog.prep_rls @{theory};
1.142 \<close>
1.143 @@ -282,8 +282,8 @@
1.144 (Rewrite_Set_Inst [(''bdv'', v_v)] ''integration'') t_t)"
1.145
1.146 method met_diffint : "diff/integration" =
1.147 - \<open>{rew_ord'="tless_true", rls'=Atools_erls, calc = [], srls = Rule_Set.empty, prls=Rule_Set.empty,
1.148 - crls = Atools_erls, errpats = [], nrls = Rule_Set.empty}\<close>
1.149 + \<open>{rew_ord="tless_true", rls'=Atools_erls, calc = [], prog_rls = Rule_Set.empty, where_rls=Rule_Set.empty,
1.150 + crls = Atools_erls, errpats = [], rew_rls = Rule_Set.empty}\<close>
1.151 Program: integrate.simps
1.152 Given: "functionTerm f_f" "integrateBy v_v"
1.153 Find: "antiDerivative F_F"
1.154 @@ -299,8 +299,8 @@
1.155 ) t_t)"
1.156
1.157 method met_diffint_named : "diff/integration/named" =
1.158 - \<open>{rew_ord'="tless_true", rls'=Atools_erls, calc = [], srls = Rule_Set.empty, prls=Rule_Set.empty,
1.159 - crls = Atools_erls, errpats = [], nrls = Rule_Set.empty}\<close>
1.160 + \<open>{rew_ord="tless_true", rls'=Atools_erls, calc = [], prog_rls = Rule_Set.empty, where_rls=Rule_Set.empty,
1.161 + crls = Atools_erls, errpats = [], rew_rls = Rule_Set.empty}\<close>
1.162 Program: intergrate_named.simps
1.163 Given: "functionTerm f_f" "integrateBy v_v"
1.164 Find: "antiDerivativeName F_F"