1.1 --- a/src/Tools/isac/Knowledge/EqSystem.thy Sat Apr 04 12:11:32 2020 +0200
1.2 +++ b/src/Tools/isac/Knowledge/EqSystem.thy Mon Apr 06 11:44:36 2020 +0200
1.3 @@ -170,10 +170,10 @@
1.4
1.5 (*.adapted from 'order_add_mult_in' by just replacing the rew_ord.*)
1.6 val order_add_mult_System =
1.7 - Rule_Set.Rls{id = "order_add_mult_System", preconds = [],
1.8 + Rule_Def.Repeat{id = "order_add_mult_System", preconds = [],
1.9 rew_ord = ("ord_simplify_System",
1.10 ord_simplify_System false @{theory "Integrate"}),
1.11 - erls = Rule_Set.e_rls,srls = Rule_Set.Erls, calc = [], errpatts = [],
1.12 + erls = Rule_Set.e_rls,srls = Rule_Set.Empty, calc = [], errpatts = [],
1.13 rules = [Rule.Thm ("mult_commute",TermC.num_str @{thm mult.commute}),
1.14 (* z * w = w * z *)
1.15 Rule.Thm ("real_mult_left_commute",TermC.num_str @{thm real_mult_left_commute}),
1.16 @@ -194,9 +194,9 @@
1.17 #1 using 'ord_simplify_System' in 'order_add_mult_System'
1.18 #2 NOT using common_nominator_p .*)
1.19 val norm_System_noadd_fractions =
1.20 - Rule_Set.Rls {id = "norm_System_noadd_fractions", preconds = [],
1.21 + Rule_Def.Repeat {id = "norm_System_noadd_fractions", preconds = [],
1.22 rew_ord = ("dummy_ord",Rule.dummy_ord),
1.23 - erls = norm_rat_erls, srls = Rule_Set.Erls, calc = [], errpatts = [],
1.24 + erls = norm_rat_erls, srls = Rule_Set.Empty, calc = [], errpatts = [],
1.25 rules = [(*sequence given by operator precedence*)
1.26 Rule.Rls_ discard_minus,
1.27 Rule.Rls_ powers,
1.28 @@ -215,9 +215,9 @@
1.29 (*.adapted from 'norm_Rational' by
1.30 *1* using 'ord_simplify_System' in 'order_add_mult_System'.*)
1.31 val norm_System =
1.32 - Rule_Set.Rls {id = "norm_System", preconds = [],
1.33 + Rule_Def.Repeat {id = "norm_System", preconds = [],
1.34 rew_ord = ("dummy_ord",Rule.dummy_ord),
1.35 - erls = norm_rat_erls, srls = Rule_Set.Erls, calc = [], errpatts = [],
1.36 + erls = norm_rat_erls, srls = Rule_Set.Empty, calc = [], errpatts = [],
1.37 rules = [(*sequence given by operator precedence*)
1.38 Rule.Rls_ discard_minus,
1.39 Rule.Rls_ powers,
1.40 @@ -243,9 +243,9 @@
1.41 *3* discard_parentheses only for (.*(.*.))
1.42 analoguous to simplify_Integral .*)
1.43 val simplify_System_parenthesized =
1.44 - Rule_Set.Seq {id = "simplify_System_parenthesized", preconds = []:term list,
1.45 + Rule_Set.Seqence {id = "simplify_System_parenthesized", preconds = []:term list,
1.46 rew_ord = ("dummy_ord", Rule.dummy_ord),
1.47 - erls = Atools_erls, srls = Rule_Set.Erls, calc = [], errpatts = [],
1.48 + erls = Atools_erls, srls = Rule_Set.Empty, calc = [], errpatts = [],
1.49 rules = [Rule.Thm ("distrib_right",TermC.num_str @{thm distrib_right}),
1.50 (*"(?z1.0 + ?z2.0) * ?w = ?z1.0 * ?w + ?z2.0 * ?w"*)
1.51 Rule.Thm ("add_divide_distrib",TermC.num_str @{thm add_divide_distrib}),
1.52 @@ -268,9 +268,9 @@
1.53 *1* ord_simplify_System instead of termlessI .*)
1.54 (*TODO.WN051031 ^^^^^^^^^^ should be in EACH rls contained *)
1.55 val simplify_System =
1.56 - Rule_Set.Seq {id = "simplify_System", preconds = []:term list,
1.57 + Rule_Set.Seqence {id = "simplify_System", preconds = []:term list,
1.58 rew_ord = ("dummy_ord", Rule.dummy_ord),
1.59 - erls = Atools_erls, srls = Rule_Set.Erls, calc = [], errpatts = [],
1.60 + erls = Atools_erls, srls = Rule_Set.Empty, calc = [], errpatts = [],
1.61 rules = [Rule.Rls_ norm_Rational,
1.62 Rule.Rls_ (*order_add_mult_in*) norm_System (**1**),
1.63 Rule.Rls_ discard_parentheses,
1.64 @@ -288,14 +288,14 @@
1.65 \<close>
1.66 ML \<open>
1.67 val isolate_bdvs =
1.68 - Rule_Set.Rls {id="isolate_bdvs", preconds = [],
1.69 + Rule_Def.Repeat {id="isolate_bdvs", preconds = [],
1.70 rew_ord = ("e_rew_ord", Rule.e_rew_ord),
1.71 erls = Rule_Set.append_rls "erls_isolate_bdvs" Rule_Set.e_rls
1.72 [(Rule.Num_Calc ("EqSystem.occur'_exactly'_in",
1.73 eval_occur_exactly_in
1.74 "#eval_occur_exactly_in_"))
1.75 ],
1.76 - srls = Rule_Set.Erls, calc = [], errpatts = [],
1.77 + srls = Rule_Set.Empty, calc = [], errpatts = [],
1.78 rules =
1.79 [Rule.Thm ("commute_0_equality", TermC.num_str @{thm commute_0_equality}),
1.80 Rule.Thm ("separate_bdvs_add", TermC.num_str @{thm separate_bdvs_add}),
1.81 @@ -304,7 +304,7 @@
1.82 \<close>
1.83 ML \<open>
1.84 val isolate_bdvs_4x4 =
1.85 - Rule_Set.Rls {id="isolate_bdvs_4x4", preconds = [],
1.86 + Rule_Def.Repeat {id="isolate_bdvs_4x4", preconds = [],
1.87 rew_ord = ("e_rew_ord", Rule.e_rew_ord),
1.88 erls = Rule_Set.append_rls
1.89 "erls_isolate_bdvs_4x4" Rule_Set.e_rls
1.90 @@ -315,7 +315,7 @@
1.91 Rule.Thm ("not_true",TermC.num_str @{thm not_true}),
1.92 Rule.Thm ("not_false",TermC.num_str @{thm not_false})
1.93 ],
1.94 - srls = Rule_Set.Erls, calc = [], errpatts = [],
1.95 + srls = Rule_Set.Empty, calc = [], errpatts = [],
1.96 rules = [Rule.Thm ("commute_0_equality", TermC.num_str @{thm commute_0_equality}),
1.97 Rule.Thm ("separate_bdvs0", TermC.num_str @{thm separate_bdvs0}),
1.98 Rule.Thm ("separate_bdvs_add1", TermC.num_str @{thm separate_bdvs_add1}),
1.99 @@ -329,20 +329,20 @@
1.100 (*.order the equations in a system such, that a triangular system (if any)
1.101 appears as [..c_4 = .., ..., ..., ..c_1 + ..c_2 + ..c_3 ..c_4 = ..].*)
1.102 val order_system =
1.103 - Rule_Set.Rls {id="order_system", preconds = [],
1.104 + Rule_Def.Repeat {id="order_system", preconds = [],
1.105 rew_ord = ("ord_simplify_System",
1.106 ord_simplify_System false thy),
1.107 - erls = Rule_Set.Erls, srls = Rule_Set.Erls, calc = [], errpatts = [],
1.108 + erls = Rule_Set.Empty, srls = Rule_Set.Empty, calc = [], errpatts = [],
1.109 rules = [Rule.Thm ("order_system_NxN", TermC.num_str @{thm order_system_NxN})
1.110 ],
1.111 scr = Rule.EmptyScr};
1.112
1.113 val prls_triangular =
1.114 - Rule_Set.Rls {id="prls_triangular", preconds = [],
1.115 + Rule_Def.Repeat {id="prls_triangular", preconds = [],
1.116 rew_ord = ("e_rew_ord", Rule.e_rew_ord),
1.117 - erls = Rule_Set.Rls {id="erls_prls_triangular", preconds = [],
1.118 + erls = Rule_Def.Repeat {id="erls_prls_triangular", preconds = [],
1.119 rew_ord = ("e_rew_ord", Rule.e_rew_ord),
1.120 - erls = Rule_Set.Erls, srls = Rule_Set.Erls, calc = [], errpatts = [],
1.121 + erls = Rule_Set.Empty, srls = Rule_Set.Empty, calc = [], errpatts = [],
1.122 rules = [(*for precond NTH_CONS ...*)
1.123 Rule.Num_Calc ("Orderings.ord_class.less", Prog_Expr.eval_equ "#less_"),
1.124 Rule.Num_Calc ("Groups.plus_class.plus", (**)eval_binop "#add_")
1.125 @@ -350,7 +350,7 @@
1.126 '+' into precondition !*)
1.127 ],
1.128 scr = Rule.EmptyScr},
1.129 - srls = Rule_Set.Erls, calc = [], errpatts = [],
1.130 + srls = Rule_Set.Empty, calc = [], errpatts = [],
1.131 rules = [Rule.Thm ("NTH_CONS",TermC.num_str @{thm NTH_CONS}),
1.132 Rule.Num_Calc ("Groups.plus_class.plus", (**)eval_binop "#add_"),
1.133 Rule.Thm ("NTH_NIL",TermC.num_str @{thm NTH_NIL}),
1.134 @@ -367,11 +367,11 @@
1.135 (*WN060914 quickly created for 4x4;
1.136 more similarity to prls_triangular desirable*)
1.137 val prls_triangular4 =
1.138 - Rule_Set.Rls {id="prls_triangular4", preconds = [],
1.139 + Rule_Def.Repeat {id="prls_triangular4", preconds = [],
1.140 rew_ord = ("e_rew_ord", Rule.e_rew_ord),
1.141 - erls = Rule_Set.Rls {id="erls_prls_triangular4", preconds = [],
1.142 + erls = Rule_Def.Repeat {id="erls_prls_triangular4", preconds = [],
1.143 rew_ord = ("e_rew_ord", Rule.e_rew_ord),
1.144 - erls = Rule_Set.Erls, srls = Rule_Set.Erls, calc = [], errpatts = [],
1.145 + erls = Rule_Set.Empty, srls = Rule_Set.Empty, calc = [], errpatts = [],
1.146 rules = [(*for precond NTH_CONS ...*)
1.147 Rule.Num_Calc ("Orderings.ord_class.less", Prog_Expr.eval_equ "#less_"),
1.148 Rule.Num_Calc ("Groups.plus_class.plus", (**)eval_binop "#add_")
1.149 @@ -379,7 +379,7 @@
1.150 '+' into precondition !*)
1.151 ],
1.152 scr = Rule.EmptyScr},
1.153 - srls = Rule_Set.Erls, calc = [], errpatts = [],
1.154 + srls = Rule_Set.Empty, calc = [], errpatts = [],
1.155 rules = [Rule.Thm ("NTH_CONS",TermC.num_str @{thm NTH_CONS}),
1.156 Rule.Num_Calc ("Groups.plus_class.plus", (**)eval_binop "#add_"),
1.157 Rule.Thm ("NTH_NIL",TermC.num_str @{thm NTH_NIL}),
1.158 @@ -492,7 +492,7 @@
1.159
1.160 ML \<open>
1.161 (*this is for NTH only*)
1.162 -val srls = Rule_Set.Rls {id="srls_normalise_4x4",
1.163 +val srls = Rule_Def.Repeat {id="srls_normalise_4x4",
1.164 preconds = [],
1.165 rew_ord = ("termlessI",termlessI),
1.166 erls = Rule_Set.append_rls "erls_in_srls_IntegrierenUnd.." Rule_Set.e_rls
1.167 @@ -501,7 +501,7 @@
1.168 (*2nd NTH_CONS pushes n+-1 into asms*)
1.169 Rule.Num_Calc("Groups.plus_class.plus", (**)eval_binop "#add_")
1.170 ],
1.171 - srls = Rule_Set.Erls, calc = [], errpatts = [],
1.172 + srls = Rule_Set.Empty, calc = [], errpatts = [],
1.173 rules = [Rule.Thm ("NTH_CONS",TermC.num_str @{thm NTH_CONS}),
1.174 Rule.Num_Calc("Groups.plus_class.plus", (**)eval_binop "#add_"),
1.175 Rule.Thm ("NTH_NIL",TermC.num_str @{thm NTH_NIL})],
1.176 @@ -512,13 +512,13 @@
1.177 setup \<open>KEStore_Elems.add_mets
1.178 [Specify.prep_met thy "met_eqsys" [] Celem.e_metID
1.179 (["EqSystem"], [],
1.180 - {rew_ord'="tless_true", rls' = Rule_Set.Erls, calc = [], srls = Rule_Set.Erls, prls = Rule_Set.Erls, crls = Rule_Set.Erls,
1.181 - errpats = [], nrls = Rule_Set.Erls},
1.182 + {rew_ord'="tless_true", rls' = Rule_Set.Empty, calc = [], srls = Rule_Set.Empty, prls = Rule_Set.Empty, crls = Rule_Set.Empty,
1.183 + errpats = [], nrls = Rule_Set.Empty},
1.184 @{thm refl}),
1.185 Specify.prep_met thy "met_eqsys_topdown" [] Celem.e_metID
1.186 (["EqSystem","top_down_substitution"], [],
1.187 - {rew_ord'="tless_true", rls' = Rule_Set.Erls, calc = [], srls = Rule_Set.Erls, prls = Rule_Set.Erls, crls = Rule_Set.Erls,
1.188 - errpats = [], nrls = Rule_Set.Erls},
1.189 + {rew_ord'="tless_true", rls' = Rule_Set.Empty, calc = [], srls = Rule_Set.Empty, prls = Rule_Set.Empty, crls = Rule_Set.Empty,
1.190 + errpats = [], nrls = Rule_Set.Empty},
1.191 @{thm refl})]
1.192 \<close>
1.193
1.194 @@ -549,19 +549,19 @@
1.195 ["(tl v_s) from v_s occur_exactly_in (NTH 1 (e_s::bool list))",
1.196 " v_s from v_s occur_exactly_in (NTH 2 (e_s::bool list))"]),
1.197 ("#Find" ,["solution ss'''"])],
1.198 - {rew_ord'="ord_simplify_System", rls' = Rule_Set.Erls, calc = [],
1.199 + {rew_ord'="ord_simplify_System", rls' = Rule_Set.Empty, calc = [],
1.200 srls = Rule_Set.append_rls "srls_top_down_2x2" Rule_Set.e_rls
1.201 [Rule.Thm ("hd_thm",TermC.num_str @{thm hd_thm}),
1.202 Rule.Thm ("tl_Cons",TermC.num_str @{thm tl_Cons}),
1.203 Rule.Thm ("tl_Nil",TermC.num_str @{thm tl_Nil})],
1.204 - prls = prls_triangular, crls = Rule_Set.Erls, errpats = [], nrls = Rule_Set.Erls},
1.205 + prls = prls_triangular, crls = Rule_Set.Empty, errpats = [], nrls = Rule_Set.Empty},
1.206 @{thm solve_system.simps})]
1.207 \<close>
1.208 setup \<open>KEStore_Elems.add_mets
1.209 [Specify.prep_met thy "met_eqsys_norm" [] Celem.e_metID
1.210 (["EqSystem", "normalise"], [],
1.211 - {rew_ord'="tless_true", rls' = Rule_Set.Erls, calc = [], srls = Rule_Set.Erls, prls = Rule_Set.Erls, crls = Rule_Set.Erls,
1.212 - errpats = [], nrls = Rule_Set.Erls},
1.213 + {rew_ord'="tless_true", rls' = Rule_Set.Empty, calc = [], srls = Rule_Set.Empty, prls = Rule_Set.Empty, crls = Rule_Set.Empty,
1.214 + errpats = [], nrls = Rule_Set.Empty},
1.215 @{thm refl})]
1.216 \<close>
1.217
1.218 @@ -584,12 +584,12 @@
1.219 (["EqSystem","normalise","2x2"],
1.220 [("#Given" ,["equalities e_s", "solveForVars v_s"]),
1.221 ("#Find" ,["solution ss'''"])],
1.222 - {rew_ord'="tless_true", rls' = Rule_Set.Erls, calc = [],
1.223 + {rew_ord'="tless_true", rls' = Rule_Set.Empty, calc = [],
1.224 srls = Rule_Set.append_rls "srls_normalise_2x2" Rule_Set.e_rls
1.225 [Rule.Thm ("hd_thm",TermC.num_str @{thm hd_thm}),
1.226 Rule.Thm ("tl_Cons",TermC.num_str @{thm tl_Cons}),
1.227 Rule.Thm ("tl_Nil",TermC.num_str @{thm tl_Nil})],
1.228 - prls = Rule_Set.Erls, crls = Rule_Set.Erls, errpats = [], nrls = Rule_Set.Erls},
1.229 + prls = Rule_Set.Empty, crls = Rule_Set.Empty, errpats = [], nrls = Rule_Set.Empty},
1.230 @{thm solve_system2.simps})]
1.231 \<close>
1.232
1.233 @@ -616,12 +616,12 @@
1.234 (["EqSystem","normalise","4x4"],
1.235 [("#Given" ,["equalities e_s", "solveForVars v_s"]),
1.236 ("#Find" ,["solution ss'''"])],
1.237 - {rew_ord'="tless_true", rls' = Rule_Set.Erls, calc = [],
1.238 + {rew_ord'="tless_true", rls' = Rule_Set.Empty, calc = [],
1.239 srls = Rule_Set.append_rls "srls_normalise_4x4" srls
1.240 [Rule.Thm ("hd_thm",TermC.num_str @{thm hd_thm}),
1.241 Rule.Thm ("tl_Cons",TermC.num_str @{thm tl_Cons}),
1.242 Rule.Thm ("tl_Nil",TermC.num_str @{thm tl_Nil})],
1.243 - prls = Rule_Set.Erls, crls = Rule_Set.Erls, errpats = [], nrls = Rule_Set.Erls},
1.244 + prls = Rule_Set.Empty, crls = Rule_Set.Empty, errpats = [], nrls = Rule_Set.Empty},
1.245 (*STOPPED.WN06? met ["EqSystem","normalise","4x4"] #>#>#>#>#>#>#>#>#>#>#>#>#>@*)
1.246 @{thm solve_system3.simps})]
1.247 \<close>
1.248 @@ -653,11 +653,11 @@
1.249 "(NTH 3 (v_s::real list)) occurs_in (NTH 3 (e_s::bool list))",
1.250 "(NTH 4 (v_s::real list)) occurs_in (NTH 4 (e_s::bool list))"]),
1.251 ("#Find", ["solution ss'''"])],
1.252 - {rew_ord'="ord_simplify_System", rls' = Rule_Set.Erls, calc = [],
1.253 + {rew_ord'="ord_simplify_System", rls' = Rule_Set.Empty, calc = [],
1.254 srls = Rule_Set.append_rls "srls_top_down_4x4" srls [],
1.255 prls = Rule_Set.append_rls "prls_tri_4x4_lin_sys" prls_triangular
1.256 [Rule.Num_Calc ("Prog_Expr.occurs'_in", Prog_Expr.eval_occurs_in "")],
1.257 - crls = Rule_Set.Erls, errpats = [], nrls = Rule_Set.Erls},
1.258 + crls = Rule_Set.Empty, errpats = [], nrls = Rule_Set.Empty},
1.259 (*FIXXXXME.WN060916: this script works ONLY for exp 7.79 #>#>#>#>#>#>#>#>#>#>*)
1.260 @{thm solve_system4.simps})]
1.261 \<close>