1.1 --- a/src/Tools/isac/Knowledge/EqSystem.thy Mon Oct 31 18:28:36 2022 +0100
1.2 +++ b/src/Tools/isac/Knowledge/EqSystem.thy Mon Nov 07 17:37:20 2022 +0100
1.3 @@ -174,7 +174,7 @@
1.4 Rule_Def.Repeat{
1.5 id = "order_add_mult_System", preconds = [],
1.6 rew_ord = ("ord_simplify_System", ord_simplify_System false @{theory "Integrate"}),
1.7 - erls = Rule_Set.empty,srls = Rule_Set.Empty, calc = [], errpatts = [],
1.8 + asm_rls = Rule_Set.empty,prog_rls = Rule_Set.Empty, calc = [], errpatts = [],
1.9 rules = [
1.10 \<^rule_thm>\<open>mult.commute\<close>, (* z * w = w * z *)
1.11 \<^rule_thm>\<open>real_mult_left_commute\<close>, (*z1.0 * (z2.0 * z3.0) = z2.0 * (z1.0 * z3.0)*)
1.12 @@ -182,7 +182,7 @@
1.13 \<^rule_thm>\<open>add.commute\<close>, (*z + w = w + z*)
1.14 \<^rule_thm>\<open>add.left_commute\<close>, (*x + (y + z) = y + (x + z)*)
1.15 \<^rule_thm>\<open>add.assoc\<close> ], (*z1.0 + z2.0 + z3.0 = z1.0 + (z2.0 + z3.0)*)
1.16 - scr = Rule.Empty_Prog};
1.17 + program = Rule.Empty_Prog};
1.18 \<close>
1.19 ML \<open>
1.20 (*.adapted from 'norm_Rational' by
1.21 @@ -191,7 +191,7 @@
1.22 val norm_System_noadd_fractions =
1.23 Rule_Def.Repeat {id = "norm_System_noadd_fractions", preconds = [],
1.24 rew_ord = ("dummy_ord", Rewrite_Ord.function_empty),
1.25 - erls = norm_rat_erls, srls = Rule_Set.Empty, calc = [], errpatts = [],
1.26 + asm_rls = norm_rat_erls, prog_rls = Rule_Set.Empty, calc = [], errpatts = [],
1.27 rules = [(*sequence given by operator precedence*)
1.28 Rule.Rls_ discard_minus,
1.29 Rule.Rls_ powers,
1.30 @@ -202,7 +202,7 @@
1.31 Rule.Rls_ collect_numerals,
1.32 (*Rule.Rls_ add_fractions_p, #2*)
1.33 Rule.Rls_ cancel_p],
1.34 - scr = Rule.Empty_Prog};
1.35 + program = Rule.Empty_Prog};
1.36 \<close>
1.37 ML \<open>
1.38 (*.adapted from 'norm_Rational' by
1.39 @@ -210,7 +210,7 @@
1.40 val norm_System =
1.41 Rule_Def.Repeat {id = "norm_System", preconds = [],
1.42 rew_ord = ("dummy_ord", Rewrite_Ord.function_empty),
1.43 - erls = norm_rat_erls, srls = Rule_Set.Empty, calc = [], errpatts = [],
1.44 + asm_rls = norm_rat_erls, prog_rls = Rule_Set.Empty, calc = [], errpatts = [],
1.45 rules = [(*sequence given by operator precedence*)
1.46 Rule.Rls_ discard_minus,
1.47 Rule.Rls_ powers,
1.48 @@ -221,7 +221,7 @@
1.49 Rule.Rls_ collect_numerals,
1.50 Rule.Rls_ add_fractions_p,
1.51 Rule.Rls_ cancel_p],
1.52 - scr = Rule.Empty_Prog};
1.53 + program = Rule.Empty_Prog};
1.54 \<close>
1.55 ML \<open>
1.56 (*.simplify an equational system BEFORE solving it such that parentheses are
1.57 @@ -236,7 +236,7 @@
1.58 val simplify_System_parenthesized =
1.59 Rule_Set.Sequence {id = "simplify_System_parenthesized", preconds = []:term list,
1.60 rew_ord = ("dummy_ord", Rewrite_Ord.function_empty),
1.61 - erls = Atools_erls, srls = Rule_Set.Empty, calc = [], errpatts = [],
1.62 + asm_rls = Atools_erls, prog_rls = Rule_Set.Empty, calc = [], errpatts = [],
1.63 rules = [
1.64 \<^rule_thm>\<open>distrib_right\<close>, (*"(?z1.0 + ?z2.0) * ?w = ?z1.0 * ?w + ?z2.0 * ?w"*)
1.65 \<^rule_thm>\<open>add_divide_distrib\<close>, (*"(?x + ?y) / ?z = ?x / ?z + ?y / ?z"*)
1.66 @@ -246,7 +246,7 @@
1.67 Rule.Rls_ collect_bdv, (*from make_polynomial_in WN051031 welldone?*)
1.68 Rule.Rls_ separate_bdv2,
1.69 \<^rule_eval>\<open>divide\<close> (Prog_Expr.eval_cancel "#divide_e")],
1.70 - scr = Rule.Empty_Prog};
1.71 + program = Rule.Empty_Prog};
1.72 \<close>
1.73 ML \<open>
1.74 (*.simplify an equational system AFTER solving it;
1.75 @@ -256,7 +256,7 @@
1.76 val simplify_System =
1.77 Rule_Set.Sequence {id = "simplify_System", preconds = []:term list,
1.78 rew_ord = ("dummy_ord", Rewrite_Ord.function_empty),
1.79 - erls = Atools_erls, srls = Rule_Set.Empty, calc = [], errpatts = [],
1.80 + asm_rls = Atools_erls, prog_rls = Rule_Set.Empty, calc = [], errpatts = [],
1.81 rules = [
1.82 Rule.Rls_ norm_Rational,
1.83 Rule.Rls_ (*order_add_mult_in*) norm_System (**1**),
1.84 @@ -264,7 +264,7 @@
1.85 Rule.Rls_ collect_bdv, (*from make_polynomial_in WN051031 welldone?*)
1.86 Rule.Rls_ separate_bdv2,
1.87 \<^rule_eval>\<open>divide\<close> (Prog_Expr.eval_cancel "#divide_e")],
1.88 - scr = Rule.Empty_Prog};
1.89 + program = Rule.Empty_Prog};
1.90 (*
1.91 val simplify_System =
1.92 Rule_Set.append_rules "simplify_System" simplify_System_parenthesized
1.93 @@ -275,33 +275,33 @@
1.94 val isolate_bdvs =
1.95 Rule_Def.Repeat {
1.96 id="isolate_bdvs", preconds = [], rew_ord = ("Rewrite_Ord.id_empty", Rewrite_Ord.function_empty),
1.97 - erls = Rule_Set.append_rules "erls_isolate_bdvs" Rule_Set.empty [
1.98 + asm_rls = Rule_Set.append_rules "erls_isolate_bdvs" Rule_Set.empty [
1.99 (\<^rule_eval>\<open>occur_exactly_in\<close> (eval_occur_exactly_in "#eval_occur_exactly_in_"))],
1.100 - srls = Rule_Set.Empty, calc = [], errpatts = [],
1.101 + prog_rls = Rule_Set.Empty, calc = [], errpatts = [],
1.102 rules = [
1.103 \<^rule_thm>\<open>commute_0_equality\<close>,
1.104 \<^rule_thm>\<open>separate_bdvs_add\<close>,
1.105 \<^rule_thm>\<open>separate_bdvs_mult\<close>],
1.106 - scr = Rule.Empty_Prog};
1.107 + program = Rule.Empty_Prog};
1.108 \<close>
1.109 ML \<open>
1.110 val isolate_bdvs_4x4 =
1.111 Rule_Def.Repeat {id="isolate_bdvs_4x4", preconds = [],
1.112 rew_ord = ("Rewrite_Ord.id_empty", Rewrite_Ord.function_empty),
1.113 - erls = Rule_Set.append_rules "erls_isolate_bdvs_4x4" Rule_Set.empty [
1.114 + asm_rls = Rule_Set.append_rules "erls_isolate_bdvs_4x4" Rule_Set.empty [
1.115 \<^rule_eval>\<open>occur_exactly_in\<close> (eval_occur_exactly_in "#eval_occur_exactly_in_"),
1.116 \<^rule_eval>\<open>Prog_Expr.ident\<close> (Prog_Expr.eval_ident "#ident_"),
1.117 \<^rule_eval>\<open>Prog_Expr.some_occur_in\<close> (Prog_Expr.eval_some_occur_in "#some_occur_in_"),
1.118 \<^rule_thm>\<open>not_true\<close>,
1.119 \<^rule_thm>\<open>not_false\<close>],
1.120 - srls = Rule_Set.Empty, calc = [], errpatts = [],
1.121 + prog_rls = Rule_Set.Empty, calc = [], errpatts = [],
1.122 rules = [
1.123 \<^rule_thm>\<open>commute_0_equality\<close>,
1.124 \<^rule_thm>\<open>separate_bdvs0\<close>,
1.125 \<^rule_thm>\<open>separate_bdvs_add1\<close>,
1.126 \<^rule_thm>\<open>separate_bdvs_add2\<close>,
1.127 \<^rule_thm>\<open>separate_bdvs_mult\<close>],
1.128 - scr = Rule.Empty_Prog};
1.129 + program = Rule.Empty_Prog};
1.130
1.131 \<close>
1.132 ML \<open>
1.133 @@ -311,24 +311,24 @@
1.134 val order_system =
1.135 Rule_Def.Repeat {id="order_system", preconds = [],
1.136 rew_ord = ("ord_simplify_System", ord_simplify_System false \<^theory>),
1.137 - erls = Rule_Set.Empty, srls = Rule_Set.Empty, calc = [], errpatts = [],
1.138 + asm_rls = Rule_Set.Empty, prog_rls = Rule_Set.Empty, calc = [], errpatts = [],
1.139 rules = [
1.140 \<^rule_thm>\<open>order_system_NxN\<close>],
1.141 - scr = Rule.Empty_Prog};
1.142 + program = Rule.Empty_Prog};
1.143
1.144 val prls_triangular =
1.145 Rule_Def.Repeat {
1.146 id="prls_triangular", preconds = [], rew_ord = ("Rewrite_Ord.id_empty", Rewrite_Ord.function_empty),
1.147 - erls = Rule_Def.Repeat {
1.148 + asm_rls = Rule_Def.Repeat {
1.149 id="erls_prls_triangular", preconds = [], rew_ord = ("Rewrite_Ord.id_empty", Rewrite_Ord.function_empty),
1.150 - erls = Rule_Set.Empty, srls = Rule_Set.Empty, calc = [], errpatts = [],
1.151 + asm_rls = Rule_Set.Empty, prog_rls = Rule_Set.Empty, calc = [], errpatts = [],
1.152 rules = [(*for precond NTH_CONS ...*)
1.153 \<^rule_eval>\<open>less\<close> (Prog_Expr.eval_equ "#less_"),
1.154 \<^rule_eval>\<open>plus\<close> (Calc_Binop.numeric "#add_"),
1.155 \<^rule_eval>\<open>occur_exactly_in\<close> (eval_occur_exactly_in "#eval_occur_exactly_in_")],
1.156 (*immediately repeated rewrite pushes '+' into precondition !*)
1.157 - scr = Rule.Empty_Prog},
1.158 - srls = Rule_Set.Empty, calc = [], errpatts = [],
1.159 + program = Rule.Empty_Prog},
1.160 + prog_rls = Rule_Set.Empty, calc = [], errpatts = [],
1.161 rules = [
1.162 \<^rule_thm>\<open>NTH_CONS\<close>,
1.163 \<^rule_eval>\<open>plus\<close> (Calc_Binop.numeric "#add_"),
1.164 @@ -336,7 +336,7 @@
1.165 \<^rule_thm>\<open>tl_Cons\<close>,
1.166 \<^rule_thm>\<open>tl_Nil\<close>,
1.167 \<^rule_eval>\<open>occur_exactly_in\<close> (eval_occur_exactly_in "#eval_occur_exactly_in_")],
1.168 - scr = Rule.Empty_Prog};
1.169 + program = Rule.Empty_Prog};
1.170 \<close>
1.171 ML \<open>
1.172
1.173 @@ -345,15 +345,15 @@
1.174 val prls_triangular4 =
1.175 Rule_Def.Repeat {
1.176 id="prls_triangular4", preconds = [], rew_ord = ("Rewrite_Ord.id_empty", Rewrite_Ord.function_empty),
1.177 - erls = Rule_Def.Repeat {
1.178 + asm_rls = Rule_Def.Repeat {
1.179 id="erls_prls_triangular4", preconds = [], rew_ord = ("Rewrite_Ord.id_empty", Rewrite_Ord.function_empty),
1.180 - erls = Rule_Set.Empty, srls = Rule_Set.Empty, calc = [], errpatts = [],
1.181 + asm_rls = Rule_Set.Empty, prog_rls = Rule_Set.Empty, calc = [], errpatts = [],
1.182 rules = [(*for precond NTH_CONS ...*)
1.183 \<^rule_eval>\<open>less\<close> (Prog_Expr.eval_equ "#less_"),
1.184 \<^rule_eval>\<open>plus\<close> (**)(Calc_Binop.numeric "#add_")],
1.185 (*immediately repeated rewrite pushes '+' into precondition !*)
1.186 - scr = Rule.Empty_Prog},
1.187 - srls = Rule_Set.Empty, calc = [], errpatts = [],
1.188 + program = Rule.Empty_Prog},
1.189 + prog_rls = Rule_Set.Empty, calc = [], errpatts = [],
1.190 rules = [
1.191 \<^rule_thm>\<open>NTH_CONS\<close>,
1.192 \<^rule_eval>\<open>plus\<close> (**)(Calc_Binop.numeric "#add_"),
1.193 @@ -361,7 +361,7 @@
1.194 \<^rule_thm>\<open>tl_Cons\<close>,
1.195 \<^rule_thm>\<open>tl_Nil\<close>,
1.196 \<^rule_eval>\<open>occur_exactly_in\<close> (eval_occur_exactly_in "#eval_occur_exactly_in_")],
1.197 - scr = Rule.Empty_Prog};
1.198 + program = Rule.Empty_Prog};
1.199 \<close>
1.200
1.201 rule_set_knowledge
1.202 @@ -463,31 +463,31 @@
1.203
1.204 ML \<open>
1.205 (*this is for NTH only*)
1.206 -val srls = Rule_Def.Repeat {id="srls_normalise_4x4",
1.207 +val prog_rls = Rule_Def.Repeat {id="srls_normalise_4x4",
1.208 preconds = [],
1.209 rew_ord = ("termlessI",termlessI),
1.210 - erls = Rule_Set.append_rules "erls_in_srls_IntegrierenUnd.." Rule_Set.empty
1.211 + asm_rls = Rule_Set.append_rules "erls_in_srls_IntegrierenUnd.." Rule_Set.empty
1.212 [(*for asm in NTH_CONS ...*)
1.213 \<^rule_eval>\<open>less\<close> (Prog_Expr.eval_equ "#less_"),
1.214 (*2nd NTH_CONS pushes n+-1 into asms*)
1.215 \<^rule_eval>\<open>plus\<close> (**)(Calc_Binop.numeric "#add_")
1.216 ],
1.217 - srls = Rule_Set.Empty, calc = [], errpatts = [],
1.218 + prog_rls = Rule_Set.Empty, calc = [], errpatts = [],
1.219 rules = [\<^rule_thm>\<open>NTH_CONS\<close>,
1.220 \<^rule_eval>\<open>plus\<close> (**)(Calc_Binop.numeric "#add_"),
1.221 \<^rule_thm>\<open>NTH_NIL\<close>],
1.222 - scr = Rule.Empty_Prog};
1.223 + program = Rule.Empty_Prog};
1.224 \<close>
1.225
1.226 section \<open>Methods\<close>
1.227
1.228 method met_eqsys : "EqSystem" =
1.229 - \<open>{rew_ord'="tless_true", rls' = Rule_Set.Empty, calc = [], srls = Rule_Set.Empty, prls = Rule_Set.Empty, crls = Rule_Set.Empty,
1.230 - errpats = [], nrls = Rule_Set.Empty}\<close>
1.231 + \<open>{rew_ord="tless_true", rls' = Rule_Set.Empty, calc = [], prog_rls = Rule_Set.Empty, where_rls = Rule_Set.Empty, crls = Rule_Set.Empty,
1.232 + errpats = [], rew_rls = Rule_Set.Empty}\<close>
1.233
1.234 method met_eqsys_topdown : "EqSystem/top_down_substitution" =
1.235 - \<open>{rew_ord'="tless_true", rls' = Rule_Set.Empty, calc = [], srls = Rule_Set.Empty, prls = Rule_Set.Empty, crls = Rule_Set.Empty,
1.236 - errpats = [], nrls = Rule_Set.Empty}\<close>
1.237 + \<open>{rew_ord="tless_true", rls' = Rule_Set.Empty, calc = [], prog_rls = Rule_Set.Empty, where_rls = Rule_Set.Empty, crls = Rule_Set.Empty,
1.238 + errpats = [], rew_rls = Rule_Set.Empty}\<close>
1.239
1.240 partial_function (tailrec) solve_system :: "bool list => real list => bool list"
1.241 where
1.242 @@ -510,12 +510,12 @@
1.243 Try (Rewrite_Set ''order_system'' ) e__s) "
1.244
1.245 method met_eqsys_topdown_2x2 : "EqSystem/top_down_substitution/2x2" =
1.246 - \<open>{rew_ord'="ord_simplify_System", rls' = Rule_Set.Empty, calc = [],
1.247 - srls = Rule_Set.append_rules "srls_top_down_2x2" Rule_Set.empty
1.248 + \<open>{rew_ord="ord_simplify_System", rls' = Rule_Set.Empty, calc = [],
1.249 + prog_rls = Rule_Set.append_rules "srls_top_down_2x2" Rule_Set.empty
1.250 [\<^rule_thm>\<open>hd_thm\<close>,
1.251 \<^rule_thm>\<open>tl_Cons\<close>,
1.252 \<^rule_thm>\<open>tl_Nil\<close>],
1.253 - prls = prls_triangular, crls = Rule_Set.Empty, errpats = [], nrls = Rule_Set.Empty}\<close>
1.254 + where_rls = prls_triangular, crls = Rule_Set.Empty, errpats = [], rew_rls = Rule_Set.Empty}\<close>
1.255 Program: solve_system.simps
1.256 Given: "equalities e_s" "solveForVars v_s"
1.257 Where:
1.258 @@ -524,8 +524,8 @@
1.259 Find: "solution ss'''"
1.260
1.261 method met_eqsys_norm : "EqSystem/normalise" =
1.262 - \<open>{rew_ord'="tless_true", rls' = Rule_Set.Empty, calc = [], srls = Rule_Set.Empty, prls = Rule_Set.Empty, crls = Rule_Set.Empty,
1.263 - errpats = [], nrls = Rule_Set.Empty}\<close>
1.264 + \<open>{rew_ord="tless_true", rls' = Rule_Set.Empty, calc = [], prog_rls = Rule_Set.Empty, where_rls = Rule_Set.Empty, crls = Rule_Set.Empty,
1.265 + errpats = [], rew_rls = Rule_Set.Empty}\<close>
1.266
1.267 partial_function (tailrec) solve_system2 :: "bool list => real list => bool list"
1.268 where
1.269 @@ -543,12 +543,12 @@
1.270 [BOOL_LIST e__s, REAL_LIST v_s])"
1.271
1.272 method met_eqsys_norm_2x2 : "EqSystem/normalise/2x2" =
1.273 - \<open>{rew_ord'="tless_true", rls' = Rule_Set.Empty, calc = [],
1.274 - srls = Rule_Set.append_rules "srls_normalise_2x2" Rule_Set.empty
1.275 + \<open>{rew_ord="tless_true", rls' = Rule_Set.Empty, calc = [],
1.276 + prog_rls = Rule_Set.append_rules "srls_normalise_2x2" Rule_Set.empty
1.277 [\<^rule_thm>\<open>hd_thm\<close>,
1.278 \<^rule_thm>\<open>tl_Cons\<close>,
1.279 \<^rule_thm>\<open>tl_Nil\<close>],
1.280 - prls = Rule_Set.Empty, crls = Rule_Set.Empty, errpats = [], nrls = Rule_Set.Empty}\<close>
1.281 + where_rls = Rule_Set.Empty, crls = Rule_Set.Empty, errpats = [], rew_rls = Rule_Set.Empty}\<close>
1.282 Program: solve_system2.simps
1.283 Given: "equalities e_s" "solveForVars v_s"
1.284 Find: "solution ss'''"
1.285 @@ -573,11 +573,11 @@
1.286 [BOOL_LIST e__s, REAL_LIST v_s])"
1.287
1.288 method met_eqsys_norm_4x4 : "EqSystem/normalise/4x4" =
1.289 - \<open>{rew_ord'="tless_true", rls' = Rule_Set.Empty, calc = [],
1.290 - srls =
1.291 - Rule_Set.append_rules "srls_normalise_4x4" srls
1.292 + \<open>{rew_ord="tless_true", rls' = Rule_Set.Empty, calc = [],
1.293 + prog_rls =
1.294 + Rule_Set.append_rules "srls_normalise_4x4" prog_rls
1.295 [\<^rule_thm>\<open>hd_thm\<close>, \<^rule_thm>\<open>tl_Cons\<close>, \<^rule_thm>\<open>tl_Nil\<close>],
1.296 - prls = Rule_Set.Empty, crls = Rule_Set.Empty, errpats = [], nrls = Rule_Set.Empty}\<close>
1.297 + where_rls = Rule_Set.Empty, crls = Rule_Set.Empty, errpats = [], rew_rls = Rule_Set.Empty}\<close>
1.298 Program: solve_system3.simps
1.299 Given: "equalities e_s" "solveForVars v_s"
1.300 Find: "solution ss'''"
1.301 @@ -602,11 +602,11 @@
1.302 [e_1, e_2, NTH 3 e_s, NTH 4 e_s])"
1.303
1.304 method met_eqsys_topdown_4x4 : "EqSystem/top_down_substitution/4x4" =
1.305 - \<open>{rew_ord'="ord_simplify_System", rls' = Rule_Set.Empty, calc = [],
1.306 - srls = Rule_Set.append_rules "srls_top_down_4x4" srls [],
1.307 - prls = Rule_Set.append_rules "prls_tri_4x4_lin_sys" prls_triangular
1.308 + \<open>{rew_ord="ord_simplify_System", rls' = Rule_Set.Empty, calc = [],
1.309 + prog_rls = Rule_Set.append_rules "srls_top_down_4x4" prog_rls [],
1.310 + where_rls = Rule_Set.append_rules "prls_tri_4x4_lin_sys" prls_triangular
1.311 [\<^rule_eval>\<open>Prog_Expr.occurs_in\<close> (Prog_Expr.eval_occurs_in "")],
1.312 - crls = Rule_Set.Empty, errpats = [], nrls = Rule_Set.Empty}\<close>
1.313 + crls = Rule_Set.Empty, errpats = [], rew_rls = Rule_Set.Empty}\<close>
1.314 (*FIXXXXME.WN060916: this script works ONLY for exp 7.79 #>#>#>#>#>#>#>#>#>#>*)
1.315 Program: solve_system4.simps
1.316 Given: "equalities e_s" "solveForVars v_s"