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