1.1 --- a/src/Tools/isac/Knowledge/EqSystem.thy Wed Apr 15 11:11:54 2020 +0200
1.2 +++ b/src/Tools/isac/Knowledge/EqSystem.thy Wed Apr 15 11:37:43 2020 +0200
1.3 @@ -187,7 +187,7 @@
1.4 Rule.Thm ("add.assoc",ThmC.numerals_to_Free @{thm add.assoc})
1.5 (*z1.0 + z2.0 + z3.0 = z1.0 + (z2.0 + z3.0)*)
1.6 ],
1.7 - scr = Rule.EmptyScr};
1.8 + scr = Rule.Empty_Prog};
1.9 \<close>
1.10 ML \<open>
1.11 (*.adapted from 'norm_Rational' by
1.12 @@ -208,7 +208,7 @@
1.13 (*Rule.Rls_ add_fractions_p, #2*)
1.14 Rule.Rls_ cancel_p
1.15 ],
1.16 - scr = Rule.EmptyScr
1.17 + scr = Rule.Empty_Prog
1.18 };
1.19 \<close>
1.20 ML \<open>
1.21 @@ -229,7 +229,7 @@
1.22 Rule.Rls_ add_fractions_p,
1.23 Rule.Rls_ cancel_p
1.24 ],
1.25 - scr = Rule.EmptyScr
1.26 + scr = Rule.Empty_Prog
1.27 };
1.28 \<close>
1.29 ML \<open>
1.30 @@ -243,7 +243,7 @@
1.31 *3* discard_parentheses only for (.*(.*.))
1.32 analoguous to simplify_Integral .*)
1.33 val simplify_System_parenthesized =
1.34 - Rule_Set.Seqence {id = "simplify_System_parenthesized", preconds = []:term list,
1.35 + Rule_Set.Sequence {id = "simplify_System_parenthesized", preconds = []:term list,
1.36 rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord),
1.37 erls = Atools_erls, srls = Rule_Set.Empty, calc = [], errpatts = [],
1.38 rules = [Rule.Thm ("distrib_right",ThmC.numerals_to_Free @{thm distrib_right}),
1.39 @@ -258,9 +258,9 @@
1.40 (*Rule.Rls_ discard_parentheses *3**),
1.41 Rule.Rls_ collect_bdv, (*from make_polynomial_in WN051031 welldone?*)
1.42 Rule.Rls_ separate_bdv2,
1.43 - Rule.Num_Calc ("Rings.divide_class.divide", Prog_Expr.eval_cancel "#divide_e")
1.44 + Rule.Eval ("Rings.divide_class.divide", Prog_Expr.eval_cancel "#divide_e")
1.45 ],
1.46 - scr = Rule.EmptyScr};
1.47 + scr = Rule.Empty_Prog};
1.48 \<close>
1.49 ML \<open>
1.50 (*.simplify an equational system AFTER solving it;
1.51 @@ -268,7 +268,7 @@
1.52 *1* ord_simplify_System instead of termlessI .*)
1.53 (*TODO.WN051031 ^^^^^^^^^^ should be in EACH rls contained *)
1.54 val simplify_System =
1.55 - Rule_Set.Seqence {id = "simplify_System", preconds = []:term list,
1.56 + Rule_Set.Sequence {id = "simplify_System", preconds = []:term list,
1.57 rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord),
1.58 erls = Atools_erls, srls = Rule_Set.Empty, calc = [], errpatts = [],
1.59 rules = [Rule.Rls_ norm_Rational,
1.60 @@ -276,9 +276,9 @@
1.61 Rule.Rls_ discard_parentheses,
1.62 Rule.Rls_ collect_bdv, (*from make_polynomial_in WN051031 welldone?*)
1.63 Rule.Rls_ separate_bdv2,
1.64 - Rule.Num_Calc ("Rings.divide_class.divide", Prog_Expr.eval_cancel "#divide_e")
1.65 + Rule.Eval ("Rings.divide_class.divide", Prog_Expr.eval_cancel "#divide_e")
1.66 ],
1.67 - scr = Rule.EmptyScr};
1.68 + scr = Rule.Empty_Prog};
1.69 (*
1.70 val simplify_System =
1.71 Rule_Set.append_rules "simplify_System" simplify_System_parenthesized
1.72 @@ -291,7 +291,7 @@
1.73 Rule_Def.Repeat {id="isolate_bdvs", preconds = [],
1.74 rew_ord = ("e_rew_ord", Rewrite_Ord.e_rew_ord),
1.75 erls = Rule_Set.append_rules "erls_isolate_bdvs" Rule_Set.empty
1.76 - [(Rule.Num_Calc ("EqSystem.occur'_exactly'_in",
1.77 + [(Rule.Eval ("EqSystem.occur'_exactly'_in",
1.78 eval_occur_exactly_in
1.79 "#eval_occur_exactly_in_"))
1.80 ],
1.81 @@ -300,7 +300,7 @@
1.82 [Rule.Thm ("commute_0_equality", ThmC.numerals_to_Free @{thm commute_0_equality}),
1.83 Rule.Thm ("separate_bdvs_add", ThmC.numerals_to_Free @{thm separate_bdvs_add}),
1.84 Rule.Thm ("separate_bdvs_mult", ThmC.numerals_to_Free @{thm separate_bdvs_mult})],
1.85 - scr = Rule.EmptyScr};
1.86 + scr = Rule.Empty_Prog};
1.87 \<close>
1.88 ML \<open>
1.89 val isolate_bdvs_4x4 =
1.90 @@ -308,10 +308,10 @@
1.91 rew_ord = ("e_rew_ord", Rewrite_Ord.e_rew_ord),
1.92 erls = Rule_Set.append_rules
1.93 "erls_isolate_bdvs_4x4" Rule_Set.empty
1.94 - [Rule.Num_Calc ("EqSystem.occur'_exactly'_in",
1.95 + [Rule.Eval ("EqSystem.occur'_exactly'_in",
1.96 eval_occur_exactly_in "#eval_occur_exactly_in_"),
1.97 - Rule.Num_Calc ("Prog_Expr.ident", Prog_Expr.eval_ident "#ident_"),
1.98 - Rule.Num_Calc ("Prog_Expr.some'_occur'_in", Prog_Expr.eval_some_occur_in "#some_occur_in_"),
1.99 + Rule.Eval ("Prog_Expr.ident", Prog_Expr.eval_ident "#ident_"),
1.100 + Rule.Eval ("Prog_Expr.some'_occur'_in", Prog_Expr.eval_some_occur_in "#some_occur_in_"),
1.101 Rule.Thm ("not_true",ThmC.numerals_to_Free @{thm not_true}),
1.102 Rule.Thm ("not_false",ThmC.numerals_to_Free @{thm not_false})
1.103 ],
1.104 @@ -321,7 +321,7 @@
1.105 Rule.Thm ("separate_bdvs_add1", ThmC.numerals_to_Free @{thm separate_bdvs_add1}),
1.106 Rule.Thm ("separate_bdvs_add1", ThmC.numerals_to_Free @{thm separate_bdvs_add2}),
1.107 Rule.Thm ("separate_bdvs_mult", ThmC.numerals_to_Free @{thm separate_bdvs_mult})
1.108 - ], scr = Rule.EmptyScr};
1.109 + ], scr = Rule.Empty_Prog};
1.110
1.111 \<close>
1.112 ML \<open>
1.113 @@ -335,7 +335,7 @@
1.114 erls = Rule_Set.Empty, srls = Rule_Set.Empty, calc = [], errpatts = [],
1.115 rules = [Rule.Thm ("order_system_NxN", ThmC.numerals_to_Free @{thm order_system_NxN})
1.116 ],
1.117 - scr = Rule.EmptyScr};
1.118 + scr = Rule.Empty_Prog};
1.119
1.120 val prls_triangular =
1.121 Rule_Def.Repeat {id="prls_triangular", preconds = [],
1.122 @@ -344,23 +344,23 @@
1.123 rew_ord = ("e_rew_ord", Rewrite_Ord.e_rew_ord),
1.124 erls = Rule_Set.Empty, srls = Rule_Set.Empty, calc = [], errpatts = [],
1.125 rules = [(*for precond NTH_CONS ...*)
1.126 - Rule.Num_Calc ("Orderings.ord_class.less", Prog_Expr.eval_equ "#less_"),
1.127 - Rule.Num_Calc ("Groups.plus_class.plus", (**)eval_binop "#add_")
1.128 + Rule.Eval ("Orderings.ord_class.less", Prog_Expr.eval_equ "#less_"),
1.129 + Rule.Eval ("Groups.plus_class.plus", (**)eval_binop "#add_")
1.130 (*immediately repeated rewrite pushes
1.131 '+' into precondition !*)
1.132 ],
1.133 - scr = Rule.EmptyScr},
1.134 + scr = Rule.Empty_Prog},
1.135 srls = Rule_Set.Empty, calc = [], errpatts = [],
1.136 rules = [Rule.Thm ("NTH_CONS",ThmC.numerals_to_Free @{thm NTH_CONS}),
1.137 - Rule.Num_Calc ("Groups.plus_class.plus", (**)eval_binop "#add_"),
1.138 + Rule.Eval ("Groups.plus_class.plus", (**)eval_binop "#add_"),
1.139 Rule.Thm ("NTH_NIL",ThmC.numerals_to_Free @{thm NTH_NIL}),
1.140 Rule.Thm ("tl_Cons",ThmC.numerals_to_Free @{thm tl_Cons}),
1.141 Rule.Thm ("tl_Nil",ThmC.numerals_to_Free @{thm tl_Nil}),
1.142 - Rule.Num_Calc ("EqSystem.occur'_exactly'_in",
1.143 + Rule.Eval ("EqSystem.occur'_exactly'_in",
1.144 eval_occur_exactly_in
1.145 "#eval_occur_exactly_in_")
1.146 ],
1.147 - scr = Rule.EmptyScr};
1.148 + scr = Rule.Empty_Prog};
1.149 \<close>
1.150 ML \<open>
1.151
1.152 @@ -373,23 +373,23 @@
1.153 rew_ord = ("e_rew_ord", Rewrite_Ord.e_rew_ord),
1.154 erls = Rule_Set.Empty, srls = Rule_Set.Empty, calc = [], errpatts = [],
1.155 rules = [(*for precond NTH_CONS ...*)
1.156 - Rule.Num_Calc ("Orderings.ord_class.less", Prog_Expr.eval_equ "#less_"),
1.157 - Rule.Num_Calc ("Groups.plus_class.plus", (**)eval_binop "#add_")
1.158 + Rule.Eval ("Orderings.ord_class.less", Prog_Expr.eval_equ "#less_"),
1.159 + Rule.Eval ("Groups.plus_class.plus", (**)eval_binop "#add_")
1.160 (*immediately repeated rewrite pushes
1.161 '+' into precondition !*)
1.162 ],
1.163 - scr = Rule.EmptyScr},
1.164 + scr = Rule.Empty_Prog},
1.165 srls = Rule_Set.Empty, calc = [], errpatts = [],
1.166 rules = [Rule.Thm ("NTH_CONS",ThmC.numerals_to_Free @{thm NTH_CONS}),
1.167 - Rule.Num_Calc ("Groups.plus_class.plus", (**)eval_binop "#add_"),
1.168 + Rule.Eval ("Groups.plus_class.plus", (**)eval_binop "#add_"),
1.169 Rule.Thm ("NTH_NIL",ThmC.numerals_to_Free @{thm NTH_NIL}),
1.170 Rule.Thm ("tl_Cons",ThmC.numerals_to_Free @{thm tl_Cons}),
1.171 Rule.Thm ("tl_Nil",ThmC.numerals_to_Free @{thm tl_Nil}),
1.172 - Rule.Num_Calc ("EqSystem.occur'_exactly'_in",
1.173 + Rule.Eval ("EqSystem.occur'_exactly'_in",
1.174 eval_occur_exactly_in
1.175 "#eval_occur_exactly_in_")
1.176 ],
1.177 - scr = Rule.EmptyScr};
1.178 + scr = Rule.Empty_Prog};
1.179 \<close>
1.180
1.181 setup \<open>KEStore_Elems.add_rlss
1.182 @@ -426,8 +426,8 @@
1.183 Rule_Set.append_rules "prls_2x2_linear_system" Rule_Set.empty
1.184 [Rule.Thm ("LENGTH_CONS",ThmC.numerals_to_Free @{thm LENGTH_CONS}),
1.185 Rule.Thm ("LENGTH_NIL",ThmC.numerals_to_Free @{thm LENGTH_NIL}),
1.186 - Rule.Num_Calc ("Groups.plus_class.plus", (**)eval_binop "#add_"),
1.187 - Rule.Num_Calc ("HOL.eq", Prog_Expr.eval_equal "#equal_")],
1.188 + Rule.Eval ("Groups.plus_class.plus", (**)eval_binop "#add_"),
1.189 + Rule.Eval ("HOL.eq", Prog_Expr.eval_equal "#equal_")],
1.190 SOME "solveSystem e_s v_s", [])),
1.191 (Specify.prep_pbt thy "pbl_equsys_lin_2x2_tri" [] Celem.e_pblID
1.192 (["triangular", "2x2", "LINEAR", "system"],
1.193 @@ -453,8 +453,8 @@
1.194 Rule_Set.append_rules "prls_3x3_linear_system" Rule_Set.empty
1.195 [Rule.Thm ("LENGTH_CONS",ThmC.numerals_to_Free @{thm LENGTH_CONS}),
1.196 Rule.Thm ("LENGTH_NIL",ThmC.numerals_to_Free @{thm LENGTH_NIL}),
1.197 - Rule.Num_Calc ("Groups.plus_class.plus", (**)eval_binop "#add_"),
1.198 - Rule.Num_Calc ("HOL.eq", Prog_Expr.eval_equal "#equal_")],
1.199 + Rule.Eval ("Groups.plus_class.plus", (**)eval_binop "#add_"),
1.200 + Rule.Eval ("HOL.eq", Prog_Expr.eval_equal "#equal_")],
1.201 SOME "solveSystem e_s v_s", [])),
1.202 (Specify.prep_pbt thy "pbl_equsys_lin_4x4" [] Celem.e_pblID
1.203 (["4x4", "LINEAR", "system"],
1.204 @@ -465,8 +465,8 @@
1.205 Rule_Set.append_rules "prls_4x4_linear_system" Rule_Set.empty
1.206 [Rule.Thm ("LENGTH_CONS",ThmC.numerals_to_Free @{thm LENGTH_CONS}),
1.207 Rule.Thm ("LENGTH_NIL",ThmC.numerals_to_Free @{thm LENGTH_NIL}),
1.208 - Rule.Num_Calc ("Groups.plus_class.plus", (**)eval_binop "#add_"),
1.209 - Rule.Num_Calc ("HOL.eq", Prog_Expr.eval_equal "#equal_")],
1.210 + Rule.Eval ("Groups.plus_class.plus", (**)eval_binop "#add_"),
1.211 + Rule.Eval ("HOL.eq", Prog_Expr.eval_equal "#equal_")],
1.212 SOME "solveSystem e_s v_s", [])),
1.213 (Specify.prep_pbt thy "pbl_equsys_lin_4x4_tri" [] Celem.e_pblID
1.214 (["triangular", "4x4", "LINEAR", "system"],
1.215 @@ -478,7 +478,7 @@
1.216 "(NTH 4 (v_s::real list)) occurs_in (NTH 4 (e_s::bool list))"]),
1.217 ("#Find" ,["solution ss'''"])],
1.218 Rule_Set.append_rules "prls_tri_4x4_lin_sys" prls_triangular
1.219 - [Rule.Num_Calc ("Prog_Expr.occurs'_in", Prog_Expr.eval_occurs_in "")],
1.220 + [Rule.Eval ("Prog_Expr.occurs'_in", Prog_Expr.eval_occurs_in "")],
1.221 SOME "solveSystem e_s v_s",
1.222 [["EqSystem","top_down_substitution","4x4"]])),
1.223 (Specify.prep_pbt thy "pbl_equsys_lin_4x4_norm" [] Celem.e_pblID
1.224 @@ -497,15 +497,15 @@
1.225 rew_ord = ("termlessI",termlessI),
1.226 erls = Rule_Set.append_rules "erls_in_srls_IntegrierenUnd.." Rule_Set.empty
1.227 [(*for asm in NTH_CONS ...*)
1.228 - Rule.Num_Calc ("Orderings.ord_class.less", Prog_Expr.eval_equ "#less_"),
1.229 + Rule.Eval ("Orderings.ord_class.less", Prog_Expr.eval_equ "#less_"),
1.230 (*2nd NTH_CONS pushes n+-1 into asms*)
1.231 - Rule.Num_Calc("Groups.plus_class.plus", (**)eval_binop "#add_")
1.232 + Rule.Eval("Groups.plus_class.plus", (**)eval_binop "#add_")
1.233 ],
1.234 srls = Rule_Set.Empty, calc = [], errpatts = [],
1.235 rules = [Rule.Thm ("NTH_CONS",ThmC.numerals_to_Free @{thm NTH_CONS}),
1.236 - Rule.Num_Calc("Groups.plus_class.plus", (**)eval_binop "#add_"),
1.237 + Rule.Eval("Groups.plus_class.plus", (**)eval_binop "#add_"),
1.238 Rule.Thm ("NTH_NIL",ThmC.numerals_to_Free @{thm NTH_NIL})],
1.239 - scr = Rule.EmptyScr};
1.240 + scr = Rule.Empty_Prog};
1.241 \<close>
1.242
1.243 (**methods**)
1.244 @@ -656,7 +656,7 @@
1.245 {rew_ord'="ord_simplify_System", rls' = Rule_Set.Empty, calc = [],
1.246 srls = Rule_Set.append_rules "srls_top_down_4x4" srls [],
1.247 prls = Rule_Set.append_rules "prls_tri_4x4_lin_sys" prls_triangular
1.248 - [Rule.Num_Calc ("Prog_Expr.occurs'_in", Prog_Expr.eval_occurs_in "")],
1.249 + [Rule.Eval ("Prog_Expr.occurs'_in", Prog_Expr.eval_occurs_in "")],
1.250 crls = Rule_Set.Empty, errpats = [], nrls = Rule_Set.Empty},
1.251 (*FIXXXXME.WN060916: this script works ONLY for exp 7.79 #>#>#>#>#>#>#>#>#>#>*)
1.252 @{thm solve_system4.simps})]