1.1 --- a/src/Tools/isac/Knowledge/EqSystem.thy Sun Mar 25 13:59:57 2018 +0200
1.2 +++ b/src/Tools/isac/Knowledge/EqSystem.thy Mon Mar 26 07:28:39 2018 +0200
1.3 @@ -77,9 +77,9 @@
1.4 (p as (Const ("EqSystem.occur'_exactly'_in",_)
1.5 $ vs $ all $ t)) _ =
1.6 if occur_exactly_in (TermC.isalist2list vs) (TermC.isalist2list all) t
1.7 - then SOME ((Celem.term2str p) ^ " = True",
1.8 + then SOME ((Rule.term2str p) ^ " = True",
1.9 HOLogic.Trueprop $ (TermC.mk_equality (p, @{term True})))
1.10 - else SOME ((Celem.term2str p) ^ " = False",
1.11 + else SOME ((Rule.term2str p) ^ " = False",
1.12 HOLogic.Trueprop $ (TermC.mk_equality (p, @{term False})))
1.13 | eval_occur_exactly_in _ _ _ _ = NONE;
1.14 *}
1.15 @@ -131,10 +131,10 @@
1.16 then
1.17 let
1.18 val (f, ts) = strip_comb t and (g, us) = strip_comb u;
1.19 - val _ = tracing ("t= f@ts= \"" ^ Celem.term_to_string''' thy f ^ "\" @ \"[" ^
1.20 - commas (map (Celem.term_to_string''' thy) ts) ^ "]\"");
1.21 - val _ = tracing ("u= g@us= \"" ^ Celem.term_to_string''' thy g ^ "\" @ \"[" ^
1.22 - commas (map (Celem.term_to_string''' thy) us) ^ "]\"");
1.23 + val _ = tracing ("t= f@ts= \"" ^ Rule.term_to_string''' thy f ^ "\" @ \"[" ^
1.24 + commas (map (Rule.term_to_string''' thy) ts) ^ "]\"");
1.25 + val _ = tracing ("u= g@us= \"" ^ Rule.term_to_string''' thy g ^ "\" @ \"[" ^
1.26 + commas (map (Rule.term_to_string''' thy) us) ^ "]\"");
1.27 val _ = tracing ("size_of_term(t,u)= (" ^ string_of_int (size_of_term' t) ^ ", " ^
1.28 string_of_int (size_of_term' u) ^ ")");
1.29 val _ = tracing ("hd_ord(f,g) = " ^ ((pr_ord o hd_ord) (f,g)));
1.30 @@ -166,7 +166,7 @@
1.31 (**)
1.32 end;
1.33 (**)
1.34 -Celem.rew_ord' := overwritel (! Celem.rew_ord',
1.35 +Rule.rew_ord' := overwritel (! Rule.rew_ord',
1.36 [("ord_simplify_System", ord_simplify_System false thy)
1.37 ]);
1.38 *}
1.39 @@ -175,66 +175,66 @@
1.40
1.41 (*.adapted from 'order_add_mult_in' by just replacing the rew_ord.*)
1.42 val order_add_mult_System =
1.43 - Celem.Rls{id = "order_add_mult_System", preconds = [],
1.44 + Rule.Rls{id = "order_add_mult_System", preconds = [],
1.45 rew_ord = ("ord_simplify_System",
1.46 ord_simplify_System false @{theory "Integrate"}),
1.47 - erls = Celem.e_rls,srls = Celem.Erls, calc = [], errpatts = [],
1.48 - rules = [Celem.Thm ("mult_commute",TermC.num_str @{thm mult.commute}),
1.49 + erls = Rule.e_rls,srls = Rule.Erls, calc = [], errpatts = [],
1.50 + rules = [Rule.Thm ("mult_commute",TermC.num_str @{thm mult.commute}),
1.51 (* z * w = w * z *)
1.52 - Celem.Thm ("real_mult_left_commute",TermC.num_str @{thm real_mult_left_commute}),
1.53 + Rule.Thm ("real_mult_left_commute",TermC.num_str @{thm real_mult_left_commute}),
1.54 (*z1.0 * (z2.0 * z3.0) = z2.0 * (z1.0 * z3.0)*)
1.55 - Celem.Thm ("mult_assoc",TermC.num_str @{thm mult.assoc}),
1.56 + Rule.Thm ("mult_assoc",TermC.num_str @{thm mult.assoc}),
1.57 (*z1.0 * z2.0 * z3.0 = z1.0 * (z2.0 * z3.0)*)
1.58 - Celem.Thm ("add_commute",TermC.num_str @{thm add.commute}),
1.59 + Rule.Thm ("add_commute",TermC.num_str @{thm add.commute}),
1.60 (*z + w = w + z*)
1.61 - Celem.Thm ("add_left_commute",TermC.num_str @{thm add.left_commute}),
1.62 + Rule.Thm ("add_left_commute",TermC.num_str @{thm add.left_commute}),
1.63 (*x + (y + z) = y + (x + z)*)
1.64 - Celem.Thm ("add_assoc",TermC.num_str @{thm add.assoc})
1.65 + Rule.Thm ("add_assoc",TermC.num_str @{thm add.assoc})
1.66 (*z1.0 + z2.0 + z3.0 = z1.0 + (z2.0 + z3.0)*)
1.67 ],
1.68 - scr = Celem.EmptyScr};
1.69 + scr = Rule.EmptyScr};
1.70 *}
1.71 ML {*
1.72 (*.adapted from 'norm_Rational' by
1.73 #1 using 'ord_simplify_System' in 'order_add_mult_System'
1.74 #2 NOT using common_nominator_p .*)
1.75 val norm_System_noadd_fractions =
1.76 - Celem.Rls {id = "norm_System_noadd_fractions", preconds = [],
1.77 - rew_ord = ("dummy_ord",Celem.dummy_ord),
1.78 - erls = norm_rat_erls, srls = Celem.Erls, calc = [], errpatts = [],
1.79 + Rule.Rls {id = "norm_System_noadd_fractions", preconds = [],
1.80 + rew_ord = ("dummy_ord",Rule.dummy_ord),
1.81 + erls = norm_rat_erls, srls = Rule.Erls, calc = [], errpatts = [],
1.82 rules = [(*sequence given by operator precedence*)
1.83 - Celem.Rls_ discard_minus,
1.84 - Celem.Rls_ powers,
1.85 - Celem.Rls_ rat_mult_divide,
1.86 - Celem.Rls_ expand,
1.87 - Celem.Rls_ reduce_0_1_2,
1.88 - Celem.Rls_ (*order_add_mult #1*) order_add_mult_System,
1.89 - Celem.Rls_ collect_numerals,
1.90 - (*Celem.Rls_ add_fractions_p, #2*)
1.91 - Celem.Rls_ cancel_p
1.92 + Rule.Rls_ discard_minus,
1.93 + Rule.Rls_ powers,
1.94 + Rule.Rls_ rat_mult_divide,
1.95 + Rule.Rls_ expand,
1.96 + Rule.Rls_ reduce_0_1_2,
1.97 + Rule.Rls_ (*order_add_mult #1*) order_add_mult_System,
1.98 + Rule.Rls_ collect_numerals,
1.99 + (*Rule.Rls_ add_fractions_p, #2*)
1.100 + Rule.Rls_ cancel_p
1.101 ],
1.102 - scr = Celem.Prog ((Thm.term_of o the o (TermC.parse thy)) "empty_script")
1.103 + scr = Rule.Prog ((Thm.term_of o the o (TermC.parse thy)) "empty_script")
1.104 };
1.105 *}
1.106 ML {*
1.107 (*.adapted from 'norm_Rational' by
1.108 *1* using 'ord_simplify_System' in 'order_add_mult_System'.*)
1.109 val norm_System =
1.110 - Celem.Rls {id = "norm_System", preconds = [],
1.111 - rew_ord = ("dummy_ord",Celem.dummy_ord),
1.112 - erls = norm_rat_erls, srls = Celem.Erls, calc = [], errpatts = [],
1.113 + Rule.Rls {id = "norm_System", preconds = [],
1.114 + rew_ord = ("dummy_ord",Rule.dummy_ord),
1.115 + erls = norm_rat_erls, srls = Rule.Erls, calc = [], errpatts = [],
1.116 rules = [(*sequence given by operator precedence*)
1.117 - Celem.Rls_ discard_minus,
1.118 - Celem.Rls_ powers,
1.119 - Celem.Rls_ rat_mult_divide,
1.120 - Celem.Rls_ expand,
1.121 - Celem.Rls_ reduce_0_1_2,
1.122 - Celem.Rls_ (*order_add_mult *1*) order_add_mult_System,
1.123 - Celem.Rls_ collect_numerals,
1.124 - Celem.Rls_ add_fractions_p,
1.125 - Celem.Rls_ cancel_p
1.126 + Rule.Rls_ discard_minus,
1.127 + Rule.Rls_ powers,
1.128 + Rule.Rls_ rat_mult_divide,
1.129 + Rule.Rls_ expand,
1.130 + Rule.Rls_ reduce_0_1_2,
1.131 + Rule.Rls_ (*order_add_mult *1*) order_add_mult_System,
1.132 + Rule.Rls_ collect_numerals,
1.133 + Rule.Rls_ add_fractions_p,
1.134 + Rule.Rls_ cancel_p
1.135 ],
1.136 - scr = Celem.Prog ((Thm.term_of o the o (TermC.parse thy)) "empty_script")
1.137 + scr = Rule.Prog ((Thm.term_of o the o (TermC.parse thy)) "empty_script")
1.138 };
1.139 *}
1.140 ML {*
1.141 @@ -248,24 +248,24 @@
1.142 *3* discard_parentheses only for (.*(.*.))
1.143 analoguous to simplify_Integral .*)
1.144 val simplify_System_parenthesized =
1.145 - Celem.Seq {id = "simplify_System_parenthesized", preconds = []:term list,
1.146 - rew_ord = ("dummy_ord", Celem.dummy_ord),
1.147 - erls = Atools_erls, srls = Celem.Erls, calc = [], errpatts = [],
1.148 - rules = [Celem.Thm ("distrib_right",TermC.num_str @{thm distrib_right}),
1.149 + Rule.Seq {id = "simplify_System_parenthesized", preconds = []:term list,
1.150 + rew_ord = ("dummy_ord", Rule.dummy_ord),
1.151 + erls = Atools_erls, srls = Rule.Erls, calc = [], errpatts = [],
1.152 + rules = [Rule.Thm ("distrib_right",TermC.num_str @{thm distrib_right}),
1.153 (*"(?z1.0 + ?z2.0) * ?w = ?z1.0 * ?w + ?z2.0 * ?w"*)
1.154 - Celem.Thm ("add_divide_distrib",TermC.num_str @{thm add_divide_distrib}),
1.155 + Rule.Thm ("add_divide_distrib",TermC.num_str @{thm add_divide_distrib}),
1.156 (*"(?x + ?y) / ?z = ?x / ?z + ?y / ?z"*)
1.157 (*^^^^^ *0* ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^*)
1.158 - Celem.Rls_ norm_Rational_noadd_fractions(**2**),
1.159 - Celem.Rls_ (*order_add_mult_in*) norm_System_noadd_fractions (**1**),
1.160 - Celem.Thm ("sym_mult_assoc",
1.161 + Rule.Rls_ norm_Rational_noadd_fractions(**2**),
1.162 + Rule.Rls_ (*order_add_mult_in*) norm_System_noadd_fractions (**1**),
1.163 + Rule.Thm ("sym_mult_assoc",
1.164 TermC.num_str (@{thm mult.assoc} RS @{thm sym}))
1.165 - (*Celem.Rls_ discard_parentheses *3**),
1.166 - Celem.Rls_ collect_bdv, (*from make_polynomial_in WN051031 welldone?*)
1.167 - Celem.Rls_ separate_bdv2,
1.168 - Celem.Calc ("Rings.divide_class.divide" ,eval_cancel "#divide_e")
1.169 + (*Rule.Rls_ discard_parentheses *3**),
1.170 + Rule.Rls_ collect_bdv, (*from make_polynomial_in WN051031 welldone?*)
1.171 + Rule.Rls_ separate_bdv2,
1.172 + Rule.Calc ("Rings.divide_class.divide" ,eval_cancel "#divide_e")
1.173 ],
1.174 - scr = Celem.EmptyScr};
1.175 + scr = Rule.EmptyScr};
1.176 *}
1.177 ML {*
1.178 (*.simplify an equational system AFTER solving it;
1.179 @@ -273,61 +273,61 @@
1.180 *1* ord_simplify_System instead of termlessI .*)
1.181 (*TODO.WN051031 ^^^^^^^^^^ should be in EACH rls contained *)
1.182 val simplify_System =
1.183 - Celem.Seq {id = "simplify_System", preconds = []:term list,
1.184 - rew_ord = ("dummy_ord", Celem.dummy_ord),
1.185 - erls = Atools_erls, srls = Celem.Erls, calc = [], errpatts = [],
1.186 - rules = [Celem.Rls_ norm_Rational,
1.187 - Celem.Rls_ (*order_add_mult_in*) norm_System (**1**),
1.188 - Celem.Rls_ discard_parentheses,
1.189 - Celem.Rls_ collect_bdv, (*from make_polynomial_in WN051031 welldone?*)
1.190 - Celem.Rls_ separate_bdv2,
1.191 - Celem.Calc ("Rings.divide_class.divide" ,eval_cancel "#divide_e")
1.192 + Rule.Seq {id = "simplify_System", preconds = []:term list,
1.193 + rew_ord = ("dummy_ord", Rule.dummy_ord),
1.194 + erls = Atools_erls, srls = Rule.Erls, calc = [], errpatts = [],
1.195 + rules = [Rule.Rls_ norm_Rational,
1.196 + Rule.Rls_ (*order_add_mult_in*) norm_System (**1**),
1.197 + Rule.Rls_ discard_parentheses,
1.198 + Rule.Rls_ collect_bdv, (*from make_polynomial_in WN051031 welldone?*)
1.199 + Rule.Rls_ separate_bdv2,
1.200 + Rule.Calc ("Rings.divide_class.divide" ,eval_cancel "#divide_e")
1.201 ],
1.202 - scr = Celem.EmptyScr};
1.203 + scr = Rule.EmptyScr};
1.204 (*
1.205 val simplify_System =
1.206 - Celem.append_rls "simplify_System" simplify_System_parenthesized
1.207 - [Celem.Thm ("sym_add_assoc",
1.208 + Rule.append_rls "simplify_System" simplify_System_parenthesized
1.209 + [Rule.Thm ("sym_add_assoc",
1.210 TermC.num_str (@{thm add.assoc} RS @{thm sym}))];
1.211 *)
1.212 *}
1.213 ML {*
1.214 val isolate_bdvs =
1.215 - Celem.Rls {id="isolate_bdvs", preconds = [],
1.216 - rew_ord = ("e_rew_ord", Celem.e_rew_ord),
1.217 - erls = Celem.append_rls "erls_isolate_bdvs" Celem.e_rls
1.218 - [(Celem.Calc ("EqSystem.occur'_exactly'_in",
1.219 + Rule.Rls {id="isolate_bdvs", preconds = [],
1.220 + rew_ord = ("e_rew_ord", Rule.e_rew_ord),
1.221 + erls = Rule.append_rls "erls_isolate_bdvs" Rule.e_rls
1.222 + [(Rule.Calc ("EqSystem.occur'_exactly'_in",
1.223 eval_occur_exactly_in
1.224 "#eval_occur_exactly_in_"))
1.225 ],
1.226 - srls = Celem.Erls, calc = [], errpatts = [],
1.227 + srls = Rule.Erls, calc = [], errpatts = [],
1.228 rules =
1.229 - [Celem.Thm ("commute_0_equality", TermC.num_str @{thm commute_0_equality}),
1.230 - Celem.Thm ("separate_bdvs_add", TermC.num_str @{thm separate_bdvs_add}),
1.231 - Celem.Thm ("separate_bdvs_mult", TermC.num_str @{thm separate_bdvs_mult})],
1.232 - scr = Celem.EmptyScr};
1.233 + [Rule.Thm ("commute_0_equality", TermC.num_str @{thm commute_0_equality}),
1.234 + Rule.Thm ("separate_bdvs_add", TermC.num_str @{thm separate_bdvs_add}),
1.235 + Rule.Thm ("separate_bdvs_mult", TermC.num_str @{thm separate_bdvs_mult})],
1.236 + scr = Rule.EmptyScr};
1.237 *}
1.238 ML {*
1.239 val isolate_bdvs_4x4 =
1.240 - Celem.Rls {id="isolate_bdvs_4x4", preconds = [],
1.241 - rew_ord = ("e_rew_ord", Celem.e_rew_ord),
1.242 - erls = Celem.append_rls
1.243 - "erls_isolate_bdvs_4x4" Celem.e_rls
1.244 - [Celem.Calc ("EqSystem.occur'_exactly'_in",
1.245 + Rule.Rls {id="isolate_bdvs_4x4", preconds = [],
1.246 + rew_ord = ("e_rew_ord", Rule.e_rew_ord),
1.247 + erls = Rule.append_rls
1.248 + "erls_isolate_bdvs_4x4" Rule.e_rls
1.249 + [Rule.Calc ("EqSystem.occur'_exactly'_in",
1.250 eval_occur_exactly_in "#eval_occur_exactly_in_"),
1.251 - Celem.Calc ("Atools.ident",eval_ident "#ident_"),
1.252 - Celem.Calc ("Atools.some'_occur'_in",
1.253 + Rule.Calc ("Atools.ident",eval_ident "#ident_"),
1.254 + Rule.Calc ("Atools.some'_occur'_in",
1.255 eval_some_occur_in "#some_occur_in_"),
1.256 - Celem.Thm ("not_true",TermC.num_str @{thm not_true}),
1.257 - Celem.Thm ("not_false",TermC.num_str @{thm not_false})
1.258 + Rule.Thm ("not_true",TermC.num_str @{thm not_true}),
1.259 + Rule.Thm ("not_false",TermC.num_str @{thm not_false})
1.260 ],
1.261 - srls = Celem.Erls, calc = [], errpatts = [],
1.262 - rules = [Celem.Thm ("commute_0_equality", TermC.num_str @{thm commute_0_equality}),
1.263 - Celem.Thm ("separate_bdvs0", TermC.num_str @{thm separate_bdvs0}),
1.264 - Celem.Thm ("separate_bdvs_add1", TermC.num_str @{thm separate_bdvs_add1}),
1.265 - Celem.Thm ("separate_bdvs_add1", TermC.num_str @{thm separate_bdvs_add2}),
1.266 - Celem.Thm ("separate_bdvs_mult", TermC.num_str @{thm separate_bdvs_mult})
1.267 - ], scr = Celem.EmptyScr};
1.268 + srls = Rule.Erls, calc = [], errpatts = [],
1.269 + rules = [Rule.Thm ("commute_0_equality", TermC.num_str @{thm commute_0_equality}),
1.270 + Rule.Thm ("separate_bdvs0", TermC.num_str @{thm separate_bdvs0}),
1.271 + Rule.Thm ("separate_bdvs_add1", TermC.num_str @{thm separate_bdvs_add1}),
1.272 + Rule.Thm ("separate_bdvs_add1", TermC.num_str @{thm separate_bdvs_add2}),
1.273 + Rule.Thm ("separate_bdvs_mult", TermC.num_str @{thm separate_bdvs_mult})
1.274 + ], scr = Rule.EmptyScr};
1.275
1.276 *}
1.277 ML {*
1.278 @@ -335,67 +335,67 @@
1.279 (*.order the equations in a system such, that a triangular system (if any)
1.280 appears as [..c_4 = .., ..., ..., ..c_1 + ..c_2 + ..c_3 ..c_4 = ..].*)
1.281 val order_system =
1.282 - Celem.Rls {id="order_system", preconds = [],
1.283 + Rule.Rls {id="order_system", preconds = [],
1.284 rew_ord = ("ord_simplify_System",
1.285 ord_simplify_System false thy),
1.286 - erls = Celem.Erls, srls = Celem.Erls, calc = [], errpatts = [],
1.287 - rules = [Celem.Thm ("order_system_NxN", TermC.num_str @{thm order_system_NxN})
1.288 + erls = Rule.Erls, srls = Rule.Erls, calc = [], errpatts = [],
1.289 + rules = [Rule.Thm ("order_system_NxN", TermC.num_str @{thm order_system_NxN})
1.290 ],
1.291 - scr = Celem.EmptyScr};
1.292 + scr = Rule.EmptyScr};
1.293
1.294 val prls_triangular =
1.295 - Celem.Rls {id="prls_triangular", preconds = [],
1.296 - rew_ord = ("e_rew_ord", Celem.e_rew_ord),
1.297 - erls = Celem.Rls {id="erls_prls_triangular", preconds = [],
1.298 - rew_ord = ("e_rew_ord", Celem.e_rew_ord),
1.299 - erls = Celem.Erls, srls = Celem.Erls, calc = [], errpatts = [],
1.300 + Rule.Rls {id="prls_triangular", preconds = [],
1.301 + rew_ord = ("e_rew_ord", Rule.e_rew_ord),
1.302 + erls = Rule.Rls {id="erls_prls_triangular", preconds = [],
1.303 + rew_ord = ("e_rew_ord", Rule.e_rew_ord),
1.304 + erls = Rule.Erls, srls = Rule.Erls, calc = [], errpatts = [],
1.305 rules = [(*for precond NTH_CONS ...*)
1.306 - Celem.Calc ("Orderings.ord_class.less",eval_equ "#less_"),
1.307 - Celem.Calc ("Groups.plus_class.plus", eval_binop "#add_")
1.308 + Rule.Calc ("Orderings.ord_class.less",eval_equ "#less_"),
1.309 + Rule.Calc ("Groups.plus_class.plus", eval_binop "#add_")
1.310 (*immediately repeated rewrite pushes
1.311 '+' into precondition !*)
1.312 ],
1.313 - scr = Celem.EmptyScr},
1.314 - srls = Celem.Erls, calc = [], errpatts = [],
1.315 - rules = [Celem.Thm ("NTH_CONS",TermC.num_str @{thm NTH_CONS}),
1.316 - Celem.Calc ("Groups.plus_class.plus", eval_binop "#add_"),
1.317 - Celem.Thm ("NTH_NIL",TermC.num_str @{thm NTH_NIL}),
1.318 - Celem.Thm ("tl_Cons",TermC.num_str @{thm tl_Cons}),
1.319 - Celem.Thm ("tl_Nil",TermC.num_str @{thm tl_Nil}),
1.320 - Celem.Calc ("EqSystem.occur'_exactly'_in",
1.321 + scr = Rule.EmptyScr},
1.322 + srls = Rule.Erls, calc = [], errpatts = [],
1.323 + rules = [Rule.Thm ("NTH_CONS",TermC.num_str @{thm NTH_CONS}),
1.324 + Rule.Calc ("Groups.plus_class.plus", eval_binop "#add_"),
1.325 + Rule.Thm ("NTH_NIL",TermC.num_str @{thm NTH_NIL}),
1.326 + Rule.Thm ("tl_Cons",TermC.num_str @{thm tl_Cons}),
1.327 + Rule.Thm ("tl_Nil",TermC.num_str @{thm tl_Nil}),
1.328 + Rule.Calc ("EqSystem.occur'_exactly'_in",
1.329 eval_occur_exactly_in
1.330 "#eval_occur_exactly_in_")
1.331 ],
1.332 - scr = Celem.EmptyScr};
1.333 + scr = Rule.EmptyScr};
1.334 *}
1.335 ML {*
1.336
1.337 (*WN060914 quickly created for 4x4;
1.338 more similarity to prls_triangular desirable*)
1.339 val prls_triangular4 =
1.340 - Celem.Rls {id="prls_triangular4", preconds = [],
1.341 - rew_ord = ("e_rew_ord", Celem.e_rew_ord),
1.342 - erls = Celem.Rls {id="erls_prls_triangular4", preconds = [],
1.343 - rew_ord = ("e_rew_ord", Celem.e_rew_ord),
1.344 - erls = Celem.Erls, srls = Celem.Erls, calc = [], errpatts = [],
1.345 + Rule.Rls {id="prls_triangular4", preconds = [],
1.346 + rew_ord = ("e_rew_ord", Rule.e_rew_ord),
1.347 + erls = Rule.Rls {id="erls_prls_triangular4", preconds = [],
1.348 + rew_ord = ("e_rew_ord", Rule.e_rew_ord),
1.349 + erls = Rule.Erls, srls = Rule.Erls, calc = [], errpatts = [],
1.350 rules = [(*for precond NTH_CONS ...*)
1.351 - Celem.Calc ("Orderings.ord_class.less",eval_equ "#less_"),
1.352 - Celem.Calc ("Groups.plus_class.plus", eval_binop "#add_")
1.353 + Rule.Calc ("Orderings.ord_class.less",eval_equ "#less_"),
1.354 + Rule.Calc ("Groups.plus_class.plus", eval_binop "#add_")
1.355 (*immediately repeated rewrite pushes
1.356 '+' into precondition !*)
1.357 ],
1.358 - scr = Celem.EmptyScr},
1.359 - srls = Celem.Erls, calc = [], errpatts = [],
1.360 - rules = [Celem.Thm ("NTH_CONS",TermC.num_str @{thm NTH_CONS}),
1.361 - Celem.Calc ("Groups.plus_class.plus", eval_binop "#add_"),
1.362 - Celem.Thm ("NTH_NIL",TermC.num_str @{thm NTH_NIL}),
1.363 - Celem.Thm ("tl_Cons",TermC.num_str @{thm tl_Cons}),
1.364 - Celem.Thm ("tl_Nil",TermC.num_str @{thm tl_Nil}),
1.365 - Celem.Calc ("EqSystem.occur'_exactly'_in",
1.366 + scr = Rule.EmptyScr},
1.367 + srls = Rule.Erls, calc = [], errpatts = [],
1.368 + rules = [Rule.Thm ("NTH_CONS",TermC.num_str @{thm NTH_CONS}),
1.369 + Rule.Calc ("Groups.plus_class.plus", eval_binop "#add_"),
1.370 + Rule.Thm ("NTH_NIL",TermC.num_str @{thm NTH_NIL}),
1.371 + Rule.Thm ("tl_Cons",TermC.num_str @{thm tl_Cons}),
1.372 + Rule.Thm ("tl_Nil",TermC.num_str @{thm tl_Nil}),
1.373 + Rule.Calc ("EqSystem.occur'_exactly'_in",
1.374 eval_occur_exactly_in
1.375 "#eval_occur_exactly_in_")
1.376 ],
1.377 - scr = Celem.EmptyScr};
1.378 + scr = Rule.EmptyScr};
1.379 *}
1.380
1.381 setup {* KEStore_Elems.add_rlss
1.382 @@ -416,24 +416,24 @@
1.383 (["system"],
1.384 [("#Given" ,["equalities e_s", "solveForVars v_s"]),
1.385 ("#Find" ,["solution ss'''"](*''' is copy-named*))],
1.386 - Celem.append_rls "e_rls" Celem.e_rls [(*for preds in where_*)], SOME "solveSystem e_s v_s", [])),
1.387 + Rule.append_rls "e_rls" Rule.e_rls [(*for preds in where_*)], SOME "solveSystem e_s v_s", [])),
1.388 (Specify.prep_pbt thy "pbl_equsys_lin" [] Celem.e_pblID
1.389 (["LINEAR", "system"],
1.390 [("#Given" ,["equalities e_s", "solveForVars v_s"]),
1.391 (*TODO.WN050929 check linearity*)
1.392 ("#Find" ,["solution ss'''"])],
1.393 - Celem.append_rls "e_rls" Celem.e_rls [(*for preds in where_*)], SOME "solveSystem e_s v_s", [])),
1.394 + Rule.append_rls "e_rls" Rule.e_rls [(*for preds in where_*)], SOME "solveSystem e_s v_s", [])),
1.395 (Specify.prep_pbt thy "pbl_equsys_lin_2x2" [] Celem.e_pblID
1.396 (["2x2", "LINEAR", "system"],
1.397 (*~~~~~~~~~~~~~~~~~~~~~~~~~*)
1.398 [("#Given" ,["equalities e_s", "solveForVars v_s"]),
1.399 ("#Where" ,["LENGTH (e_s:: bool list) = 2", "LENGTH v_s = 2"]),
1.400 ("#Find" ,["solution ss'''"])],
1.401 - Celem.append_rls "prls_2x2_linear_system" Celem.e_rls
1.402 - [Celem.Thm ("LENGTH_CONS",TermC.num_str @{thm LENGTH_CONS}),
1.403 - Celem.Thm ("LENGTH_NIL",TermC.num_str @{thm LENGTH_NIL}),
1.404 - Celem.Calc ("Groups.plus_class.plus", eval_binop "#add_"),
1.405 - Celem.Calc ("HOL.eq",eval_equal "#equal_")],
1.406 + Rule.append_rls "prls_2x2_linear_system" Rule.e_rls
1.407 + [Rule.Thm ("LENGTH_CONS",TermC.num_str @{thm LENGTH_CONS}),
1.408 + Rule.Thm ("LENGTH_NIL",TermC.num_str @{thm LENGTH_NIL}),
1.409 + Rule.Calc ("Groups.plus_class.plus", eval_binop "#add_"),
1.410 + Rule.Calc ("HOL.eq",eval_equal "#equal_")],
1.411 SOME "solveSystem e_s v_s", [])),
1.412 (Specify.prep_pbt thy "pbl_equsys_lin_2x2_tri" [] Celem.e_pblID
1.413 (["triangular", "2x2", "LINEAR", "system"],
1.414 @@ -447,7 +447,7 @@
1.415 (["normalise", "2x2", "LINEAR", "system"],
1.416 [("#Given" ,["equalities e_s", "solveForVars v_s"]),
1.417 ("#Find" ,["solution ss'''"])],
1.418 - Celem.append_rls "e_rls" Celem.e_rls [(*for preds in where_*)],
1.419 + Rule.append_rls "e_rls" Rule.e_rls [(*for preds in where_*)],
1.420 SOME "solveSystem e_s v_s",
1.421 [["EqSystem","normalise","2x2"]])),
1.422 (Specify.prep_pbt thy "pbl_equsys_lin_3x3" [] Celem.e_pblID
1.423 @@ -456,11 +456,11 @@
1.424 [("#Given" ,["equalities e_s", "solveForVars v_s"]),
1.425 ("#Where" ,["LENGTH (e_s:: bool list) = 3", "LENGTH v_s = 3"]),
1.426 ("#Find" ,["solution ss'''"])],
1.427 - Celem.append_rls "prls_3x3_linear_system" Celem.e_rls
1.428 - [Celem.Thm ("LENGTH_CONS",TermC.num_str @{thm LENGTH_CONS}),
1.429 - Celem.Thm ("LENGTH_NIL",TermC.num_str @{thm LENGTH_NIL}),
1.430 - Celem.Calc ("Groups.plus_class.plus", eval_binop "#add_"),
1.431 - Celem.Calc ("HOL.eq",eval_equal "#equal_")],
1.432 + Rule.append_rls "prls_3x3_linear_system" Rule.e_rls
1.433 + [Rule.Thm ("LENGTH_CONS",TermC.num_str @{thm LENGTH_CONS}),
1.434 + Rule.Thm ("LENGTH_NIL",TermC.num_str @{thm LENGTH_NIL}),
1.435 + Rule.Calc ("Groups.plus_class.plus", eval_binop "#add_"),
1.436 + Rule.Calc ("HOL.eq",eval_equal "#equal_")],
1.437 SOME "solveSystem e_s v_s", [])),
1.438 (Specify.prep_pbt thy "pbl_equsys_lin_4x4" [] Celem.e_pblID
1.439 (["4x4", "LINEAR", "system"],
1.440 @@ -468,11 +468,11 @@
1.441 [("#Given" ,["equalities e_s", "solveForVars v_s"]),
1.442 ("#Where" ,["LENGTH (e_s:: bool list) = 4", "LENGTH v_s = 4"]),
1.443 ("#Find" ,["solution ss'''"])],
1.444 - Celem.append_rls "prls_4x4_linear_system" Celem.e_rls
1.445 - [Celem.Thm ("LENGTH_CONS",TermC.num_str @{thm LENGTH_CONS}),
1.446 - Celem.Thm ("LENGTH_NIL",TermC.num_str @{thm LENGTH_NIL}),
1.447 - Celem.Calc ("Groups.plus_class.plus", eval_binop "#add_"),
1.448 - Celem.Calc ("HOL.eq",eval_equal "#equal_")],
1.449 + Rule.append_rls "prls_4x4_linear_system" Rule.e_rls
1.450 + [Rule.Thm ("LENGTH_CONS",TermC.num_str @{thm LENGTH_CONS}),
1.451 + Rule.Thm ("LENGTH_NIL",TermC.num_str @{thm LENGTH_NIL}),
1.452 + Rule.Calc ("Groups.plus_class.plus", eval_binop "#add_"),
1.453 + Rule.Calc ("HOL.eq",eval_equal "#equal_")],
1.454 SOME "solveSystem e_s v_s", [])),
1.455 (Specify.prep_pbt thy "pbl_equsys_lin_4x4_tri" [] Celem.e_pblID
1.456 (["triangular", "4x4", "LINEAR", "system"],
1.457 @@ -483,8 +483,8 @@
1.458 "(NTH 3 (v_s::real list)) occurs_in (NTH 3 (e_s::bool list))",
1.459 "(NTH 4 (v_s::real list)) occurs_in (NTH 4 (e_s::bool list))"]),
1.460 ("#Find" ,["solution ss'''"])],
1.461 - Celem.append_rls "prls_tri_4x4_lin_sys" prls_triangular
1.462 - [Celem.Calc ("Atools.occurs'_in",eval_occurs_in "")],
1.463 + Rule.append_rls "prls_tri_4x4_lin_sys" prls_triangular
1.464 + [Rule.Calc ("Atools.occurs'_in",eval_occurs_in "")],
1.465 SOME "solveSystem e_s v_s",
1.466 [["EqSystem","top_down_substitution","4x4"]])),
1.467 (Specify.prep_pbt thy "pbl_equsys_lin_4x4_norm" [] Celem.e_pblID
1.468 @@ -492,39 +492,39 @@
1.469 [("#Given" ,["equalities e_s", "solveForVars v_s"]),
1.470 (*LENGTH is checked 1 level above*)
1.471 ("#Find" ,["solution ss'''"])],
1.472 - Celem.append_rls "e_rls" Celem.e_rls [(*for preds in where_*)],
1.473 + Rule.append_rls "e_rls" Rule.e_rls [(*for preds in where_*)],
1.474 SOME "solveSystem e_s v_s",
1.475 [["EqSystem","normalise","4x4"]]))] *}
1.476
1.477 ML {*
1.478 (*this is for NTH only*)
1.479 -val srls = Celem.Rls {id="srls_normalise_4x4",
1.480 +val srls = Rule.Rls {id="srls_normalise_4x4",
1.481 preconds = [],
1.482 rew_ord = ("termlessI",termlessI),
1.483 - erls = Celem.append_rls "erls_in_srls_IntegrierenUnd.." Celem.e_rls
1.484 + erls = Rule.append_rls "erls_in_srls_IntegrierenUnd.." Rule.e_rls
1.485 [(*for asm in NTH_CONS ...*)
1.486 - Celem.Calc ("Orderings.ord_class.less",eval_equ "#less_"),
1.487 + Rule.Calc ("Orderings.ord_class.less",eval_equ "#less_"),
1.488 (*2nd NTH_CONS pushes n+-1 into asms*)
1.489 - Celem.Calc("Groups.plus_class.plus", eval_binop "#add_")
1.490 + Rule.Calc("Groups.plus_class.plus", eval_binop "#add_")
1.491 ],
1.492 - srls = Celem.Erls, calc = [], errpatts = [],
1.493 - rules = [Celem.Thm ("NTH_CONS",TermC.num_str @{thm NTH_CONS}),
1.494 - Celem.Calc("Groups.plus_class.plus", eval_binop "#add_"),
1.495 - Celem.Thm ("NTH_NIL",TermC.num_str @{thm NTH_NIL})],
1.496 - scr = Celem.EmptyScr};
1.497 + srls = Rule.Erls, calc = [], errpatts = [],
1.498 + rules = [Rule.Thm ("NTH_CONS",TermC.num_str @{thm NTH_CONS}),
1.499 + Rule.Calc("Groups.plus_class.plus", eval_binop "#add_"),
1.500 + Rule.Thm ("NTH_NIL",TermC.num_str @{thm NTH_NIL})],
1.501 + scr = Rule.EmptyScr};
1.502 *}
1.503
1.504 (**methods**)
1.505 setup {* KEStore_Elems.add_mets
1.506 [Specify.prep_met thy "met_eqsys" [] Celem.e_metID
1.507 (["EqSystem"], [],
1.508 - {rew_ord'="tless_true", rls' = Celem.Erls, calc = [], srls = Celem.Erls, prls = Celem.Erls, crls = Celem.Erls,
1.509 - errpats = [], nrls = Celem.Erls},
1.510 + {rew_ord'="tless_true", rls' = Rule.Erls, calc = [], srls = Rule.Erls, prls = Rule.Erls, crls = Rule.Erls,
1.511 + errpats = [], nrls = Rule.Erls},
1.512 "empty_script"),
1.513 Specify.prep_met thy "met_eqsys_topdown" [] Celem.e_metID
1.514 (["EqSystem","top_down_substitution"], [],
1.515 - {rew_ord'="tless_true", rls' = Celem.Erls, calc = [], srls = Celem.Erls, prls = Celem.Erls, crls = Celem.Erls,
1.516 - errpats = [], nrls = Celem.Erls},
1.517 + {rew_ord'="tless_true", rls' = Rule.Erls, calc = [], srls = Rule.Erls, prls = Rule.Erls, crls = Rule.Erls,
1.518 + errpats = [], nrls = Rule.Erls},
1.519 "empty_script"),
1.520 Specify.prep_met thy "met_eqsys_topdown_2x2" [] Celem.e_metID
1.521 (["EqSystem", "top_down_substitution", "2x2"],
1.522 @@ -533,12 +533,12 @@
1.523 ["(tl v_s) from v_s occur_exactly_in (NTH 1 (e_s::bool list))",
1.524 " v_s from v_s occur_exactly_in (NTH 2 (e_s::bool list))"]),
1.525 ("#Find" ,["solution ss'''"])],
1.526 - {rew_ord'="ord_simplify_System", rls' = Celem.Erls, calc = [],
1.527 - srls = Celem.append_rls "srls_top_down_2x2" Celem.e_rls
1.528 - [Celem.Thm ("hd_thm",TermC.num_str @{thm hd_thm}),
1.529 - Celem.Thm ("tl_Cons",TermC.num_str @{thm tl_Cons}),
1.530 - Celem.Thm ("tl_Nil",TermC.num_str @{thm tl_Nil})],
1.531 - prls = prls_triangular, crls = Celem.Erls, errpats = [], nrls = Celem.Erls},
1.532 + {rew_ord'="ord_simplify_System", rls' = Rule.Erls, calc = [],
1.533 + srls = Rule.append_rls "srls_top_down_2x2" Rule.e_rls
1.534 + [Rule.Thm ("hd_thm",TermC.num_str @{thm hd_thm}),
1.535 + Rule.Thm ("tl_Cons",TermC.num_str @{thm tl_Cons}),
1.536 + Rule.Thm ("tl_Nil",TermC.num_str @{thm tl_Nil})],
1.537 + prls = prls_triangular, crls = Rule.Erls, errpats = [], nrls = Rule.Erls},
1.538 "Script SolveSystemScript (e_s::bool list) (v_s::real list) = " ^
1.539 " (let e_1 = Take (hd e_s); " ^
1.540 " e_1 = ((Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]" ^
1.541 @@ -574,19 +574,19 @@
1.542 ---------------------------------------------------------------------------*)),
1.543 Specify.prep_met thy "met_eqsys_norm" [] Celem.e_metID
1.544 (["EqSystem", "normalise"], [],
1.545 - {rew_ord'="tless_true", rls' = Celem.Erls, calc = [], srls = Celem.Erls, prls = Celem.Erls, crls = Celem.Erls,
1.546 - errpats = [], nrls = Celem.Erls},
1.547 + {rew_ord'="tless_true", rls' = Rule.Erls, calc = [], srls = Rule.Erls, prls = Rule.Erls, crls = Rule.Erls,
1.548 + errpats = [], nrls = Rule.Erls},
1.549 "empty_script"),
1.550 Specify.prep_met thy "met_eqsys_norm_2x2" [] Celem.e_metID
1.551 (["EqSystem","normalise","2x2"],
1.552 [("#Given" ,["equalities e_s", "solveForVars v_s"]),
1.553 ("#Find" ,["solution ss'''"])],
1.554 - {rew_ord'="tless_true", rls' = Celem.Erls, calc = [],
1.555 - srls = Celem.append_rls "srls_normalise_2x2" Celem.e_rls
1.556 - [Celem.Thm ("hd_thm",TermC.num_str @{thm hd_thm}),
1.557 - Celem.Thm ("tl_Cons",TermC.num_str @{thm tl_Cons}),
1.558 - Celem.Thm ("tl_Nil",TermC.num_str @{thm tl_Nil})],
1.559 - prls = Celem.Erls, crls = Celem.Erls, errpats = [], nrls = Celem.Erls},
1.560 + {rew_ord'="tless_true", rls' = Rule.Erls, calc = [],
1.561 + srls = Rule.append_rls "srls_normalise_2x2" Rule.e_rls
1.562 + [Rule.Thm ("hd_thm",TermC.num_str @{thm hd_thm}),
1.563 + Rule.Thm ("tl_Cons",TermC.num_str @{thm tl_Cons}),
1.564 + Rule.Thm ("tl_Nil",TermC.num_str @{thm tl_Nil})],
1.565 + prls = Rule.Erls, crls = Rule.Erls, errpats = [], nrls = Rule.Erls},
1.566 "Script SolveSystemScript (e_s::bool list) (v_s::real list) = " ^
1.567 " (let e__s = ((Try (Rewrite_Set norm_Rational False)) @@ " ^
1.568 " (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]" ^
1.569 @@ -602,12 +602,12 @@
1.570 (["EqSystem","normalise","4x4"],
1.571 [("#Given" ,["equalities e_s", "solveForVars v_s"]),
1.572 ("#Find" ,["solution ss'''"])],
1.573 - {rew_ord'="tless_true", rls' = Celem.Erls, calc = [],
1.574 - srls = Celem.append_rls "srls_normalise_4x4" srls
1.575 - [Celem.Thm ("hd_thm",TermC.num_str @{thm hd_thm}),
1.576 - Celem.Thm ("tl_Cons",TermC.num_str @{thm tl_Cons}),
1.577 - Celem.Thm ("tl_Nil",TermC.num_str @{thm tl_Nil})],
1.578 - prls = Celem.Erls, crls = Celem.Erls, errpats = [], nrls = Celem.Erls},
1.579 + {rew_ord'="tless_true", rls' = Rule.Erls, calc = [],
1.580 + srls = Rule.append_rls "srls_normalise_4x4" srls
1.581 + [Rule.Thm ("hd_thm",TermC.num_str @{thm hd_thm}),
1.582 + Rule.Thm ("tl_Cons",TermC.num_str @{thm tl_Cons}),
1.583 + Rule.Thm ("tl_Nil",TermC.num_str @{thm tl_Nil})],
1.584 + prls = Rule.Erls, crls = Rule.Erls, errpats = [], nrls = Rule.Erls},
1.585 (*STOPPED.WN06? met ["EqSystem","normalise","4x4"] @@@@@@@@@@@@@@@@@@@@@@@@@@@*)
1.586 "Script SolveSystemScript (e_s::bool list) (v_s::real list) = " ^
1.587 " (let e__s = " ^
1.588 @@ -634,11 +634,11 @@
1.589 "(NTH 3 (v_s::real list)) occurs_in (NTH 3 (e_s::bool list))",
1.590 "(NTH 4 (v_s::real list)) occurs_in (NTH 4 (e_s::bool list))"]),
1.591 ("#Find", ["solution ss'''"])],
1.592 - {rew_ord'="ord_simplify_System", rls' = Celem.Erls, calc = [],
1.593 - srls = Celem.append_rls "srls_top_down_4x4" srls [],
1.594 - prls = Celem.append_rls "prls_tri_4x4_lin_sys" prls_triangular
1.595 - [Celem.Calc ("Atools.occurs'_in",eval_occurs_in "")],
1.596 - crls = Celem.Erls, errpats = [], nrls = Celem.Erls},
1.597 + {rew_ord'="ord_simplify_System", rls' = Rule.Erls, calc = [],
1.598 + srls = Rule.append_rls "srls_top_down_4x4" srls [],
1.599 + prls = Rule.append_rls "prls_tri_4x4_lin_sys" prls_triangular
1.600 + [Rule.Calc ("Atools.occurs'_in",eval_occurs_in "")],
1.601 + crls = Rule.Erls, errpats = [], nrls = Rule.Erls},
1.602 (*FIXXXXME.WN060916: this script works ONLY for exp 7.79 @@@@@@@@@@@@@@@@@@@@*)
1.603 "Script SolveSystemScript (e_s::bool list) (v_s::real list) = " ^
1.604 " (let e_1 = NTH 1 e_s; " ^