1.1 --- a/src/Tools/isac/Knowledge/PolyEq.thy Thu Mar 15 10:17:44 2018 +0100
1.2 +++ b/src/Tools/isac/Knowledge/PolyEq.thy Thu Mar 15 12:42:04 2018 +0100
1.3 @@ -376,107 +376,107 @@
1.4
1.5 (*-------------------------rulse-------------------------*)
1.6 val PolyEq_prls = (*3.10.02:just the following order due to subterm evaluation*)
1.7 - append_rls "PolyEq_prls" e_rls
1.8 - [Calc ("Atools.ident",eval_ident "#ident_"),
1.9 - Calc ("Tools.matches",eval_matches ""),
1.10 - Calc ("Tools.lhs" ,eval_lhs ""),
1.11 - Calc ("Tools.rhs" ,eval_rhs ""),
1.12 - Calc ("Poly.is'_expanded'_in",eval_is_expanded_in ""),
1.13 - Calc ("Poly.is'_poly'_in",eval_is_poly_in ""),
1.14 - Calc ("Poly.has'_degree'_in",eval_has_degree_in ""),
1.15 - Calc ("Poly.is'_polyrat'_in",eval_is_polyrat_in ""),
1.16 - (*Calc ("Atools.occurs'_in",eval_occurs_in ""), *)
1.17 - (*Calc ("Atools.is'_const",eval_const "#is_const_"),*)
1.18 - Calc ("HOL.eq",eval_equal "#equal_"),
1.19 - Calc ("RootEq.is'_rootTerm'_in",eval_is_rootTerm_in ""),
1.20 - Calc ("RatEq.is'_ratequation'_in",eval_is_ratequation_in ""),
1.21 - Thm ("not_true",TermC.num_str @{thm not_true}),
1.22 - Thm ("not_false",TermC.num_str @{thm not_false}),
1.23 - Thm ("and_true",TermC.num_str @{thm and_true}),
1.24 - Thm ("and_false",TermC.num_str @{thm and_false}),
1.25 - Thm ("or_true",TermC.num_str @{thm or_true}),
1.26 - Thm ("or_false",TermC.num_str @{thm or_false})
1.27 + Celem.append_rls "PolyEq_prls" Celem.e_rls
1.28 + [Celem.Calc ("Atools.ident",eval_ident "#ident_"),
1.29 + Celem.Calc ("Tools.matches",eval_matches ""),
1.30 + Celem.Calc ("Tools.lhs" ,eval_lhs ""),
1.31 + Celem.Calc ("Tools.rhs" ,eval_rhs ""),
1.32 + Celem.Calc ("Poly.is'_expanded'_in",eval_is_expanded_in ""),
1.33 + Celem.Calc ("Poly.is'_poly'_in",eval_is_poly_in ""),
1.34 + Celem.Calc ("Poly.has'_degree'_in",eval_has_degree_in ""),
1.35 + Celem.Calc ("Poly.is'_polyrat'_in",eval_is_polyrat_in ""),
1.36 + (*Celem.Calc ("Atools.occurs'_in",eval_occurs_in ""), *)
1.37 + (*Celem.Calc ("Atools.is'_const",eval_const "#is_const_"),*)
1.38 + Celem.Calc ("HOL.eq",eval_equal "#equal_"),
1.39 + Celem.Calc ("RootEq.is'_rootTerm'_in",eval_is_rootTerm_in ""),
1.40 + Celem.Calc ("RatEq.is'_ratequation'_in",eval_is_ratequation_in ""),
1.41 + Celem.Thm ("not_true",TermC.num_str @{thm not_true}),
1.42 + Celem.Thm ("not_false",TermC.num_str @{thm not_false}),
1.43 + Celem.Thm ("and_true",TermC.num_str @{thm and_true}),
1.44 + Celem.Thm ("and_false",TermC.num_str @{thm and_false}),
1.45 + Celem.Thm ("or_true",TermC.num_str @{thm or_true}),
1.46 + Celem.Thm ("or_false",TermC.num_str @{thm or_false})
1.47 ];
1.48
1.49 val PolyEq_erls =
1.50 - merge_rls "PolyEq_erls" LinEq_erls
1.51 - (append_rls "ops_preds" calculate_Rational
1.52 - [Calc ("HOL.eq",eval_equal "#equal_"),
1.53 - Thm ("plus_leq", TermC.num_str @{thm plus_leq}),
1.54 - Thm ("minus_leq", TermC.num_str @{thm minus_leq}),
1.55 - Thm ("rat_leq1", TermC.num_str @{thm rat_leq1}),
1.56 - Thm ("rat_leq2", TermC.num_str @{thm rat_leq2}),
1.57 - Thm ("rat_leq3", TermC.num_str @{thm rat_leq3})
1.58 + Celem.merge_rls "PolyEq_erls" LinEq_erls
1.59 + (Celem.append_rls "ops_preds" calculate_Rational
1.60 + [Celem.Calc ("HOL.eq",eval_equal "#equal_"),
1.61 + Celem.Thm ("plus_leq", TermC.num_str @{thm plus_leq}),
1.62 + Celem.Thm ("minus_leq", TermC.num_str @{thm minus_leq}),
1.63 + Celem.Thm ("rat_leq1", TermC.num_str @{thm rat_leq1}),
1.64 + Celem.Thm ("rat_leq2", TermC.num_str @{thm rat_leq2}),
1.65 + Celem.Thm ("rat_leq3", TermC.num_str @{thm rat_leq3})
1.66 ]);
1.67
1.68 val PolyEq_crls =
1.69 - merge_rls "PolyEq_crls" LinEq_crls
1.70 - (append_rls "ops_preds" calculate_Rational
1.71 - [Calc ("HOL.eq",eval_equal "#equal_"),
1.72 - Thm ("plus_leq", TermC.num_str @{thm plus_leq}),
1.73 - Thm ("minus_leq", TermC.num_str @{thm minus_leq}),
1.74 - Thm ("rat_leq1", TermC.num_str @{thm rat_leq1}),
1.75 - Thm ("rat_leq2", TermC.num_str @{thm rat_leq2}),
1.76 - Thm ("rat_leq3", TermC.num_str @{thm rat_leq3})
1.77 + Celem.merge_rls "PolyEq_crls" LinEq_crls
1.78 + (Celem.append_rls "ops_preds" calculate_Rational
1.79 + [Celem.Calc ("HOL.eq",eval_equal "#equal_"),
1.80 + Celem.Thm ("plus_leq", TermC.num_str @{thm plus_leq}),
1.81 + Celem.Thm ("minus_leq", TermC.num_str @{thm minus_leq}),
1.82 + Celem.Thm ("rat_leq1", TermC.num_str @{thm rat_leq1}),
1.83 + Celem.Thm ("rat_leq2", TermC.num_str @{thm rat_leq2}),
1.84 + Celem.Thm ("rat_leq3", TermC.num_str @{thm rat_leq3})
1.85 ]);
1.86
1.87 val cancel_leading_coeff = prep_rls'(
1.88 - Rls {id = "cancel_leading_coeff", preconds = [],
1.89 - rew_ord = ("e_rew_ord",e_rew_ord),
1.90 - erls = PolyEq_erls, srls = Erls, calc = [], errpatts = [],
1.91 + Celem.Rls {id = "cancel_leading_coeff", preconds = [],
1.92 + rew_ord = ("xxxe_rew_ordxxx",Celem.e_rew_ord),
1.93 + erls = PolyEq_erls, srls = Celem.Erls, calc = [], errpatts = [],
1.94 rules =
1.95 - [Thm ("cancel_leading_coeff1",TermC.num_str @{thm cancel_leading_coeff1}),
1.96 - Thm ("cancel_leading_coeff2",TermC.num_str @{thm cancel_leading_coeff2}),
1.97 - Thm ("cancel_leading_coeff3",TermC.num_str @{thm cancel_leading_coeff3}),
1.98 - Thm ("cancel_leading_coeff4",TermC.num_str @{thm cancel_leading_coeff4}),
1.99 - Thm ("cancel_leading_coeff5",TermC.num_str @{thm cancel_leading_coeff5}),
1.100 - Thm ("cancel_leading_coeff6",TermC.num_str @{thm cancel_leading_coeff6}),
1.101 - Thm ("cancel_leading_coeff7",TermC.num_str @{thm cancel_leading_coeff7}),
1.102 - Thm ("cancel_leading_coeff8",TermC.num_str @{thm cancel_leading_coeff8}),
1.103 - Thm ("cancel_leading_coeff9",TermC.num_str @{thm cancel_leading_coeff9}),
1.104 - Thm ("cancel_leading_coeff10",TermC.num_str @{thm cancel_leading_coeff10}),
1.105 - Thm ("cancel_leading_coeff11",TermC.num_str @{thm cancel_leading_coeff11}),
1.106 - Thm ("cancel_leading_coeff12",TermC.num_str @{thm cancel_leading_coeff12}),
1.107 - Thm ("cancel_leading_coeff13",TermC.num_str @{thm cancel_leading_coeff13})
1.108 - ],scr = Prog ((Thm.term_of o the o (TermC.parse thy)) "empty_script")}:rls);
1.109 + [Celem.Thm ("cancel_leading_coeff1",TermC.num_str @{thm cancel_leading_coeff1}),
1.110 + Celem.Thm ("cancel_leading_coeff2",TermC.num_str @{thm cancel_leading_coeff2}),
1.111 + Celem.Thm ("cancel_leading_coeff3",TermC.num_str @{thm cancel_leading_coeff3}),
1.112 + Celem.Thm ("cancel_leading_coeff4",TermC.num_str @{thm cancel_leading_coeff4}),
1.113 + Celem.Thm ("cancel_leading_coeff5",TermC.num_str @{thm cancel_leading_coeff5}),
1.114 + Celem.Thm ("cancel_leading_coeff6",TermC.num_str @{thm cancel_leading_coeff6}),
1.115 + Celem.Thm ("cancel_leading_coeff7",TermC.num_str @{thm cancel_leading_coeff7}),
1.116 + Celem.Thm ("cancel_leading_coeff8",TermC.num_str @{thm cancel_leading_coeff8}),
1.117 + Celem.Thm ("cancel_leading_coeff9",TermC.num_str @{thm cancel_leading_coeff9}),
1.118 + Celem.Thm ("cancel_leading_coeff10",TermC.num_str @{thm cancel_leading_coeff10}),
1.119 + Celem.Thm ("cancel_leading_coeff11",TermC.num_str @{thm cancel_leading_coeff11}),
1.120 + Celem.Thm ("cancel_leading_coeff12",TermC.num_str @{thm cancel_leading_coeff12}),
1.121 + Celem.Thm ("cancel_leading_coeff13",TermC.num_str @{thm cancel_leading_coeff13})
1.122 + ],scr = Celem.Prog ((Thm.term_of o the o (TermC.parse thy)) "empty_script")});
1.123
1.124 val prep_rls' = LTool.prep_rls @{theory};
1.125 *}
1.126 ML{*
1.127 val complete_square = prep_rls'(
1.128 - Rls {id = "complete_square", preconds = [],
1.129 - rew_ord = ("e_rew_ord",e_rew_ord),
1.130 - erls = PolyEq_erls, srls = Erls, calc = [], errpatts = [],
1.131 - rules = [Thm ("complete_square1",TermC.num_str @{thm complete_square1}),
1.132 - Thm ("complete_square2",TermC.num_str @{thm complete_square2}),
1.133 - Thm ("complete_square3",TermC.num_str @{thm complete_square3}),
1.134 - Thm ("complete_square4",TermC.num_str @{thm complete_square4}),
1.135 - Thm ("complete_square5",TermC.num_str @{thm complete_square5})
1.136 + Celem.Rls {id = "complete_square", preconds = [],
1.137 + rew_ord = ("xxxe_rew_ordxxx",Celem.e_rew_ord),
1.138 + erls = PolyEq_erls, srls = Celem.Erls, calc = [], errpatts = [],
1.139 + rules = [Celem.Thm ("complete_square1",TermC.num_str @{thm complete_square1}),
1.140 + Celem.Thm ("complete_square2",TermC.num_str @{thm complete_square2}),
1.141 + Celem.Thm ("complete_square3",TermC.num_str @{thm complete_square3}),
1.142 + Celem.Thm ("complete_square4",TermC.num_str @{thm complete_square4}),
1.143 + Celem.Thm ("complete_square5",TermC.num_str @{thm complete_square5})
1.144 ],
1.145 - scr = Prog ((Thm.term_of o the o (TermC.parse thy)) "empty_script")
1.146 - }:rls);
1.147 + scr = Celem.Prog ((Thm.term_of o the o (TermC.parse thy)) "empty_script")
1.148 + });
1.149
1.150 val polyeq_simplify = prep_rls'(
1.151 - Rls {id = "polyeq_simplify", preconds = [],
1.152 + Celem.Rls {id = "polyeq_simplify", preconds = [],
1.153 rew_ord = ("termlessI",termlessI),
1.154 erls = PolyEq_erls,
1.155 - srls = Erls,
1.156 + srls = Celem.Erls,
1.157 calc = [], errpatts = [],
1.158 - rules = [Thm ("real_assoc_1",TermC.num_str @{thm real_assoc_1}),
1.159 - Thm ("real_assoc_2",TermC.num_str @{thm real_assoc_2}),
1.160 - Thm ("real_diff_minus",TermC.num_str @{thm real_diff_minus}),
1.161 - Thm ("real_unari_minus",TermC.num_str @{thm real_unari_minus}),
1.162 - Thm ("realpow_multI",TermC.num_str @{thm realpow_multI}),
1.163 - Calc ("Groups.plus_class.plus",eval_binop "#add_"),
1.164 - Calc ("Groups.minus_class.minus",eval_binop "#sub_"),
1.165 - Calc ("Groups.times_class.times",eval_binop "#mult_"),
1.166 - Calc ("Rings.divide_class.divide", eval_cancel "#divide_e"),
1.167 - Calc ("NthRoot.sqrt",eval_sqrt "#sqrt_"),
1.168 - Calc ("Atools.pow" ,eval_binop "#power_"),
1.169 - Rls_ reduce_012
1.170 + rules = [Celem.Thm ("real_assoc_1",TermC.num_str @{thm real_assoc_1}),
1.171 + Celem.Thm ("real_assoc_2",TermC.num_str @{thm real_assoc_2}),
1.172 + Celem.Thm ("real_diff_minus",TermC.num_str @{thm real_diff_minus}),
1.173 + Celem.Thm ("real_unari_minus",TermC.num_str @{thm real_unari_minus}),
1.174 + Celem.Thm ("realpow_multI",TermC.num_str @{thm realpow_multI}),
1.175 + Celem.Calc ("Groups.plus_class.plus",eval_binop "#add_"),
1.176 + Celem.Calc ("Groups.minus_class.minus",eval_binop "#sub_"),
1.177 + Celem.Calc ("Groups.times_class.times",eval_binop "#mult_"),
1.178 + Celem.Calc ("Rings.divide_class.divide", eval_cancel "#divide_e"),
1.179 + Celem.Calc ("NthRoot.sqrt",eval_sqrt "#sqrt_"),
1.180 + Celem.Calc ("Atools.pow" ,eval_binop "#power_"),
1.181 + Celem.Rls_ reduce_012
1.182 ],
1.183 - scr = Prog ((Thm.term_of o the o (TermC.parse thy)) "empty_script")
1.184 - }:rls);
1.185 + scr = Celem.Prog ((Thm.term_of o the o (TermC.parse thy)) "empty_script")
1.186 + });
1.187 *}
1.188 setup {* KEStore_Elems.add_rlss
1.189 [("cancel_leading_coeff", (Context.theory_name @{theory}, cancel_leading_coeff)),
1.190 @@ -489,35 +489,35 @@
1.191 (* -- d0 -- *)
1.192 (*isolate the bound variable in an d0 equation; 'bdv' is a meta-constant*)
1.193 val d0_polyeq_simplify = prep_rls'(
1.194 - Rls {id = "d0_polyeq_simplify", preconds = [],
1.195 - rew_ord = ("e_rew_ord",e_rew_ord),
1.196 + Celem.Rls {id = "d0_polyeq_simplify", preconds = [],
1.197 + rew_ord = ("xxxe_rew_ordxxx",Celem.e_rew_ord),
1.198 erls = PolyEq_erls,
1.199 - srls = Erls,
1.200 + srls = Celem.Erls,
1.201 calc = [], errpatts = [],
1.202 - rules = [Thm("d0_true",TermC.num_str @{thm d0_true}),
1.203 - Thm("d0_false",TermC.num_str @{thm d0_false})
1.204 + rules = [Celem.Thm("d0_true",TermC.num_str @{thm d0_true}),
1.205 + Celem.Thm("d0_false",TermC.num_str @{thm d0_false})
1.206 ],
1.207 - scr = Prog ((Thm.term_of o the o (TermC.parse thy)) "empty_script")
1.208 - }:rls);
1.209 + scr = Celem.Prog ((Thm.term_of o the o (TermC.parse thy)) "empty_script")
1.210 + });
1.211
1.212 (* -- d1 -- *)
1.213 (*isolate the bound variable in an d1 equation; 'bdv' is a meta-constant*)
1.214 val d1_polyeq_simplify = prep_rls'(
1.215 - Rls {id = "d1_polyeq_simplify", preconds = [],
1.216 - rew_ord = ("e_rew_ord",e_rew_ord),
1.217 + Celem.Rls {id = "d1_polyeq_simplify", preconds = [],
1.218 + rew_ord = ("xxxe_rew_ordxxx",Celem.e_rew_ord),
1.219 erls = PolyEq_erls,
1.220 - srls = Erls,
1.221 + srls = Celem.Erls,
1.222 calc = [], errpatts = [],
1.223 rules = [
1.224 - Thm("d1_isolate_add1",TermC.num_str @{thm d1_isolate_add1}),
1.225 + Celem.Thm("d1_isolate_add1",TermC.num_str @{thm d1_isolate_add1}),
1.226 (* a+bx=0 -> bx=-a *)
1.227 - Thm("d1_isolate_add2",TermC.num_str @{thm d1_isolate_add2}),
1.228 + Celem.Thm("d1_isolate_add2",TermC.num_str @{thm d1_isolate_add2}),
1.229 (* a+ x=0 -> x=-a *)
1.230 - Thm("d1_isolate_div",TermC.num_str @{thm d1_isolate_div})
1.231 + Celem.Thm("d1_isolate_div",TermC.num_str @{thm d1_isolate_div})
1.232 (* bx=c -> x=c/b *)
1.233 ],
1.234 - scr = Prog ((Thm.term_of o the o (TermC.parse thy)) "empty_script")
1.235 - }:rls);
1.236 + scr = Celem.Prog ((Thm.term_of o the o (TermC.parse thy)) "empty_script")
1.237 + });
1.238
1.239 *}
1.240 subsection {* degree 2 *}
1.241 @@ -525,290 +525,290 @@
1.242 (* isolate the bound variable in an d2 equation with bdv only;
1.243 "bdv" is a meta-constant substituted for the "x" below by isac's rewriter. *)
1.244 val d2_polyeq_bdv_only_simplify = prep_rls'(
1.245 - Rls {id = "d2_polyeq_bdv_only_simplify", preconds = [], rew_ord = ("e_rew_ord",e_rew_ord),
1.246 - erls = PolyEq_erls, srls = Erls, calc = [], errpatts = [],
1.247 + Celem.Rls {id = "d2_polyeq_bdv_only_simplify", preconds = [], rew_ord = ("xxxe_rew_ordxxx",Celem.e_rew_ord),
1.248 + erls = PolyEq_erls, srls = Celem.Erls, calc = [], errpatts = [],
1.249 rules =
1.250 - [Thm ("d2_prescind1", TermC.num_str @{thm d2_prescind1}), (* ax+bx^2=0 -> x(a+bx)=0 *)
1.251 - Thm ("d2_prescind2", TermC.num_str @{thm d2_prescind2}), (* ax+ x^2=0 -> x(a+ x)=0 *)
1.252 - Thm ("d2_prescind3", TermC.num_str @{thm d2_prescind3}), (* x+bx^2=0 -> x(1+bx)=0 *)
1.253 - Thm ("d2_prescind4", TermC.num_str @{thm d2_prescind4}), (* x+ x^2=0 -> x(1+ x)=0 *)
1.254 - Thm ("d2_sqrt_equation1", TermC.num_str @{thm d2_sqrt_equation1}), (* x^2=c -> x=+-sqrt(c) *)
1.255 - Thm ("d2_sqrt_equation1_neg", TermC.num_str @{thm d2_sqrt_equation1_neg}), (* [0<c] x^2=c -> []*)
1.256 - Thm ("d2_sqrt_equation2", TermC.num_str @{thm d2_sqrt_equation2}), (* x^2=0 -> x=0 *)
1.257 - Thm ("d2_reduce_equation1", TermC.num_str @{thm d2_reduce_equation1}),(* x(a+bx)=0 -> x=0 |a+bx=0*)
1.258 - Thm ("d2_reduce_equation2", TermC.num_str @{thm d2_reduce_equation2}),(* x(a+ x)=0 -> x=0 |a+ x=0*)
1.259 - Thm ("d2_isolate_div", TermC.num_str @{thm d2_isolate_div}) (* bx^2=c -> x^2=c/b *)
1.260 + [Celem.Thm ("d2_prescind1", TermC.num_str @{thm d2_prescind1}), (* ax+bx^2=0 -> x(a+bx)=0 *)
1.261 + Celem.Thm ("d2_prescind2", TermC.num_str @{thm d2_prescind2}), (* ax+ x^2=0 -> x(a+ x)=0 *)
1.262 + Celem.Thm ("d2_prescind3", TermC.num_str @{thm d2_prescind3}), (* x+bx^2=0 -> x(1+bx)=0 *)
1.263 + Celem.Thm ("d2_prescind4", TermC.num_str @{thm d2_prescind4}), (* x+ x^2=0 -> x(1+ x)=0 *)
1.264 + Celem.Thm ("d2_sqrt_equation1", TermC.num_str @{thm d2_sqrt_equation1}), (* x^2=c -> x=+-sqrt(c) *)
1.265 + Celem.Thm ("d2_sqrt_equation1_neg", TermC.num_str @{thm d2_sqrt_equation1_neg}), (* [0<c] x^2=c -> []*)
1.266 + Celem.Thm ("d2_sqrt_equation2", TermC.num_str @{thm d2_sqrt_equation2}), (* x^2=0 -> x=0 *)
1.267 + Celem.Thm ("d2_reduce_equation1", TermC.num_str @{thm d2_reduce_equation1}),(* x(a+bx)=0 -> x=0 |a+bx=0*)
1.268 + Celem.Thm ("d2_reduce_equation2", TermC.num_str @{thm d2_reduce_equation2}),(* x(a+ x)=0 -> x=0 |a+ x=0*)
1.269 + Celem.Thm ("d2_isolate_div", TermC.num_str @{thm d2_isolate_div}) (* bx^2=c -> x^2=c/b *)
1.270 ],
1.271 - scr = Prog ((Thm.term_of o the o (TermC.parse thy)) "empty_script")
1.272 - }:rls);
1.273 + scr = Celem.Prog ((Thm.term_of o the o (TermC.parse thy)) "empty_script")
1.274 + });
1.275 *}
1.276 ML{*
1.277 (* isolate the bound variable in an d2 equation with sqrt only;
1.278 'bdv' is a meta-constant*)
1.279 val d2_polyeq_sq_only_simplify = prep_rls'(
1.280 - Rls {id = "d2_polyeq_sq_only_simplify", preconds = [],
1.281 - rew_ord = ("e_rew_ord",e_rew_ord),
1.282 + Celem.Rls {id = "d2_polyeq_sq_only_simplify", preconds = [],
1.283 + rew_ord = ("xxxe_rew_ordxxx",Celem.e_rew_ord),
1.284 erls = PolyEq_erls,
1.285 - srls = Erls,
1.286 + srls = Celem.Erls,
1.287 calc = [], errpatts = [],
1.288 (*asm_thm = [("d2_sqrt_equation1",""),("d2_sqrt_equation1_neg",""),
1.289 ("d2_isolate_div","")],*)
1.290 - rules = [Thm("d2_isolate_add1",TermC.num_str @{thm d2_isolate_add1}),
1.291 + rules = [Celem.Thm("d2_isolate_add1",TermC.num_str @{thm d2_isolate_add1}),
1.292 (* a+ bx^2=0 -> bx^2=(-1)a*)
1.293 - Thm("d2_isolate_add2",TermC.num_str @{thm d2_isolate_add2}),
1.294 + Celem.Thm("d2_isolate_add2",TermC.num_str @{thm d2_isolate_add2}),
1.295 (* a+ x^2=0 -> x^2=(-1)a*)
1.296 - Thm("d2_sqrt_equation2",TermC.num_str @{thm d2_sqrt_equation2}),
1.297 + Celem.Thm("d2_sqrt_equation2",TermC.num_str @{thm d2_sqrt_equation2}),
1.298 (* x^2=0 -> x=0 *)
1.299 - Thm("d2_sqrt_equation1",TermC.num_str @{thm d2_sqrt_equation1}),
1.300 + Celem.Thm("d2_sqrt_equation1",TermC.num_str @{thm d2_sqrt_equation1}),
1.301 (* x^2=c -> x=+-sqrt(c)*)
1.302 - Thm("d2_sqrt_equation1_neg",TermC.num_str @{thm d2_sqrt_equation1_neg}),
1.303 + Celem.Thm("d2_sqrt_equation1_neg",TermC.num_str @{thm d2_sqrt_equation1_neg}),
1.304 (* [c<0] x^2=c -> x=[] *)
1.305 - Thm("d2_isolate_div",TermC.num_str @{thm d2_isolate_div})
1.306 + Celem.Thm("d2_isolate_div",TermC.num_str @{thm d2_isolate_div})
1.307 (* bx^2=c -> x^2=c/b*)
1.308 ],
1.309 - scr = Prog ((Thm.term_of o the o (TermC.parse thy)) "empty_script")
1.310 - }:rls);
1.311 + scr = Celem.Prog ((Thm.term_of o the o (TermC.parse thy)) "empty_script")
1.312 + });
1.313 *}
1.314 ML{*
1.315 (* isolate the bound variable in an d2 equation with pqFormula;
1.316 'bdv' is a meta-constant*)
1.317 val d2_polyeq_pqFormula_simplify = prep_rls'(
1.318 - Rls {id = "d2_polyeq_pqFormula_simplify", preconds = [],
1.319 - rew_ord = ("e_rew_ord",e_rew_ord), erls = PolyEq_erls,
1.320 - srls = Erls, calc = [], errpatts = [],
1.321 - rules = [Thm("d2_pqformula1",TermC.num_str @{thm d2_pqformula1}),
1.322 + Celem.Rls {id = "d2_polyeq_pqFormula_simplify", preconds = [],
1.323 + rew_ord = ("xxxe_rew_ordxxx",Celem.e_rew_ord), erls = PolyEq_erls,
1.324 + srls = Celem.Erls, calc = [], errpatts = [],
1.325 + rules = [Celem.Thm("d2_pqformula1",TermC.num_str @{thm d2_pqformula1}),
1.326 (* q+px+ x^2=0 *)
1.327 - Thm("d2_pqformula1_neg",TermC.num_str @{thm d2_pqformula1_neg}),
1.328 + Celem.Thm("d2_pqformula1_neg",TermC.num_str @{thm d2_pqformula1_neg}),
1.329 (* q+px+ x^2=0 *)
1.330 - Thm("d2_pqformula2",TermC.num_str @{thm d2_pqformula2}),
1.331 + Celem.Thm("d2_pqformula2",TermC.num_str @{thm d2_pqformula2}),
1.332 (* q+px+1x^2=0 *)
1.333 - Thm("d2_pqformula2_neg",TermC.num_str @{thm d2_pqformula2_neg}),
1.334 + Celem.Thm("d2_pqformula2_neg",TermC.num_str @{thm d2_pqformula2_neg}),
1.335 (* q+px+1x^2=0 *)
1.336 - Thm("d2_pqformula3",TermC.num_str @{thm d2_pqformula3}),
1.337 + Celem.Thm("d2_pqformula3",TermC.num_str @{thm d2_pqformula3}),
1.338 (* q+ x+ x^2=0 *)
1.339 - Thm("d2_pqformula3_neg",TermC.num_str @{thm d2_pqformula3_neg}),
1.340 + Celem.Thm("d2_pqformula3_neg",TermC.num_str @{thm d2_pqformula3_neg}),
1.341 (* q+ x+ x^2=0 *)
1.342 - Thm("d2_pqformula4",TermC.num_str @{thm d2_pqformula4}),
1.343 + Celem.Thm("d2_pqformula4",TermC.num_str @{thm d2_pqformula4}),
1.344 (* q+ x+1x^2=0 *)
1.345 - Thm("d2_pqformula4_neg",TermC.num_str @{thm d2_pqformula4_neg}),
1.346 + Celem.Thm("d2_pqformula4_neg",TermC.num_str @{thm d2_pqformula4_neg}),
1.347 (* q+ x+1x^2=0 *)
1.348 - Thm("d2_pqformula5",TermC.num_str @{thm d2_pqformula5}),
1.349 + Celem.Thm("d2_pqformula5",TermC.num_str @{thm d2_pqformula5}),
1.350 (* qx+ x^2=0 *)
1.351 - Thm("d2_pqformula6",TermC.num_str @{thm d2_pqformula6}),
1.352 + Celem.Thm("d2_pqformula6",TermC.num_str @{thm d2_pqformula6}),
1.353 (* qx+1x^2=0 *)
1.354 - Thm("d2_pqformula7",TermC.num_str @{thm d2_pqformula7}),
1.355 + Celem.Thm("d2_pqformula7",TermC.num_str @{thm d2_pqformula7}),
1.356 (* x+ x^2=0 *)
1.357 - Thm("d2_pqformula8",TermC.num_str @{thm d2_pqformula8}),
1.358 + Celem.Thm("d2_pqformula8",TermC.num_str @{thm d2_pqformula8}),
1.359 (* x+1x^2=0 *)
1.360 - Thm("d2_pqformula9",TermC.num_str @{thm d2_pqformula9}),
1.361 + Celem.Thm("d2_pqformula9",TermC.num_str @{thm d2_pqformula9}),
1.362 (* q +1x^2=0 *)
1.363 - Thm("d2_pqformula9_neg",TermC.num_str @{thm d2_pqformula9_neg}),
1.364 + Celem.Thm("d2_pqformula9_neg",TermC.num_str @{thm d2_pqformula9_neg}),
1.365 (* q +1x^2=0 *)
1.366 - Thm("d2_pqformula10",TermC.num_str @{thm d2_pqformula10}),
1.367 + Celem.Thm("d2_pqformula10",TermC.num_str @{thm d2_pqformula10}),
1.368 (* q + x^2=0 *)
1.369 - Thm("d2_pqformula10_neg",TermC.num_str @{thm d2_pqformula10_neg}),
1.370 + Celem.Thm("d2_pqformula10_neg",TermC.num_str @{thm d2_pqformula10_neg}),
1.371 (* q + x^2=0 *)
1.372 - Thm("d2_sqrt_equation2",TermC.num_str @{thm d2_sqrt_equation2}),
1.373 + Celem.Thm("d2_sqrt_equation2",TermC.num_str @{thm d2_sqrt_equation2}),
1.374 (* x^2=0 *)
1.375 - Thm("d2_sqrt_equation3",TermC.num_str @{thm d2_sqrt_equation3})
1.376 + Celem.Thm("d2_sqrt_equation3",TermC.num_str @{thm d2_sqrt_equation3})
1.377 (* 1x^2=0 *)
1.378 - ],scr = Prog ((Thm.term_of o the o (TermC.parse thy)) "empty_script")
1.379 - }:rls);
1.380 + ],scr = Celem.Prog ((Thm.term_of o the o (TermC.parse thy)) "empty_script")
1.381 + });
1.382 *}
1.383 ML{*
1.384 (* isolate the bound variable in an d2 equation with abcFormula;
1.385 'bdv' is a meta-constant*)
1.386 val d2_polyeq_abcFormula_simplify = prep_rls'(
1.387 - Rls {id = "d2_polyeq_abcFormula_simplify", preconds = [],
1.388 - rew_ord = ("e_rew_ord",e_rew_ord), erls = PolyEq_erls,
1.389 - srls = Erls, calc = [], errpatts = [],
1.390 - rules = [Thm("d2_abcformula1",TermC.num_str @{thm d2_abcformula1}),
1.391 + Celem.Rls {id = "d2_polyeq_abcFormula_simplify", preconds = [],
1.392 + rew_ord = ("xxxe_rew_ordxxx",Celem.e_rew_ord), erls = PolyEq_erls,
1.393 + srls = Celem.Erls, calc = [], errpatts = [],
1.394 + rules = [Celem.Thm("d2_abcformula1",TermC.num_str @{thm d2_abcformula1}),
1.395 (*c+bx+cx^2=0 *)
1.396 - Thm("d2_abcformula1_neg",TermC.num_str @{thm d2_abcformula1_neg}),
1.397 + Celem.Thm("d2_abcformula1_neg",TermC.num_str @{thm d2_abcformula1_neg}),
1.398 (*c+bx+cx^2=0 *)
1.399 - Thm("d2_abcformula2",TermC.num_str @{thm d2_abcformula2}),
1.400 + Celem.Thm("d2_abcformula2",TermC.num_str @{thm d2_abcformula2}),
1.401 (*c+ x+cx^2=0 *)
1.402 - Thm("d2_abcformula2_neg",TermC.num_str @{thm d2_abcformula2_neg}),
1.403 + Celem.Thm("d2_abcformula2_neg",TermC.num_str @{thm d2_abcformula2_neg}),
1.404 (*c+ x+cx^2=0 *)
1.405 - Thm("d2_abcformula3",TermC.num_str @{thm d2_abcformula3}),
1.406 + Celem.Thm("d2_abcformula3",TermC.num_str @{thm d2_abcformula3}),
1.407 (*c+bx+ x^2=0 *)
1.408 - Thm("d2_abcformula3_neg",TermC.num_str @{thm d2_abcformula3_neg}),
1.409 + Celem.Thm("d2_abcformula3_neg",TermC.num_str @{thm d2_abcformula3_neg}),
1.410 (*c+bx+ x^2=0 *)
1.411 - Thm("d2_abcformula4",TermC.num_str @{thm d2_abcformula4}),
1.412 + Celem.Thm("d2_abcformula4",TermC.num_str @{thm d2_abcformula4}),
1.413 (*c+ x+ x^2=0 *)
1.414 - Thm("d2_abcformula4_neg",TermC.num_str @{thm d2_abcformula4_neg}),
1.415 + Celem.Thm("d2_abcformula4_neg",TermC.num_str @{thm d2_abcformula4_neg}),
1.416 (*c+ x+ x^2=0 *)
1.417 - Thm("d2_abcformula5",TermC.num_str @{thm d2_abcformula5}),
1.418 + Celem.Thm("d2_abcformula5",TermC.num_str @{thm d2_abcformula5}),
1.419 (*c+ cx^2=0 *)
1.420 - Thm("d2_abcformula5_neg",TermC.num_str @{thm d2_abcformula5_neg}),
1.421 + Celem.Thm("d2_abcformula5_neg",TermC.num_str @{thm d2_abcformula5_neg}),
1.422 (*c+ cx^2=0 *)
1.423 - Thm("d2_abcformula6",TermC.num_str @{thm d2_abcformula6}),
1.424 + Celem.Thm("d2_abcformula6",TermC.num_str @{thm d2_abcformula6}),
1.425 (*c+ x^2=0 *)
1.426 - Thm("d2_abcformula6_neg",TermC.num_str @{thm d2_abcformula6_neg}),
1.427 + Celem.Thm("d2_abcformula6_neg",TermC.num_str @{thm d2_abcformula6_neg}),
1.428 (*c+ x^2=0 *)
1.429 - Thm("d2_abcformula7",TermC.num_str @{thm d2_abcformula7}),
1.430 + Celem.Thm("d2_abcformula7",TermC.num_str @{thm d2_abcformula7}),
1.431 (* bx+ax^2=0 *)
1.432 - Thm("d2_abcformula8",TermC.num_str @{thm d2_abcformula8}),
1.433 + Celem.Thm("d2_abcformula8",TermC.num_str @{thm d2_abcformula8}),
1.434 (* bx+ x^2=0 *)
1.435 - Thm("d2_abcformula9",TermC.num_str @{thm d2_abcformula9}),
1.436 + Celem.Thm("d2_abcformula9",TermC.num_str @{thm d2_abcformula9}),
1.437 (* x+ax^2=0 *)
1.438 - Thm("d2_abcformula10",TermC.num_str @{thm d2_abcformula10}),
1.439 + Celem.Thm("d2_abcformula10",TermC.num_str @{thm d2_abcformula10}),
1.440 (* x+ x^2=0 *)
1.441 - Thm("d2_sqrt_equation2",TermC.num_str @{thm d2_sqrt_equation2}),
1.442 + Celem.Thm("d2_sqrt_equation2",TermC.num_str @{thm d2_sqrt_equation2}),
1.443 (* x^2=0 *)
1.444 - Thm("d2_sqrt_equation3",TermC.num_str @{thm d2_sqrt_equation3})
1.445 + Celem.Thm("d2_sqrt_equation3",TermC.num_str @{thm d2_sqrt_equation3})
1.446 (* bx^2=0 *)
1.447 ],
1.448 - scr = Prog ((Thm.term_of o the o (TermC.parse thy)) "empty_script")
1.449 - }:rls);
1.450 + scr = Celem.Prog ((Thm.term_of o the o (TermC.parse thy)) "empty_script")
1.451 + });
1.452 *}
1.453 ML{*
1.454
1.455 (* isolate the bound variable in an d2 equation;
1.456 'bdv' is a meta-constant*)
1.457 val d2_polyeq_simplify = prep_rls'(
1.458 - Rls {id = "d2_polyeq_simplify", preconds = [],
1.459 - rew_ord = ("e_rew_ord",e_rew_ord), erls = PolyEq_erls,
1.460 - srls = Erls, calc = [], errpatts = [],
1.461 - rules = [Thm("d2_pqformula1",TermC.num_str @{thm d2_pqformula1}),
1.462 + Celem.Rls {id = "d2_polyeq_simplify", preconds = [],
1.463 + rew_ord = ("xxxe_rew_ordxxx",Celem.e_rew_ord), erls = PolyEq_erls,
1.464 + srls = Celem.Erls, calc = [], errpatts = [],
1.465 + rules = [Celem.Thm("d2_pqformula1",TermC.num_str @{thm d2_pqformula1}),
1.466 (* p+qx+ x^2=0 *)
1.467 - Thm("d2_pqformula1_neg",TermC.num_str @{thm d2_pqformula1_neg}),
1.468 + Celem.Thm("d2_pqformula1_neg",TermC.num_str @{thm d2_pqformula1_neg}),
1.469 (* p+qx+ x^2=0 *)
1.470 - Thm("d2_pqformula2",TermC.num_str @{thm d2_pqformula2}),
1.471 + Celem.Thm("d2_pqformula2",TermC.num_str @{thm d2_pqformula2}),
1.472 (* p+qx+1x^2=0 *)
1.473 - Thm("d2_pqformula2_neg",TermC.num_str @{thm d2_pqformula2_neg}),
1.474 + Celem.Thm("d2_pqformula2_neg",TermC.num_str @{thm d2_pqformula2_neg}),
1.475 (* p+qx+1x^2=0 *)
1.476 - Thm("d2_pqformula3",TermC.num_str @{thm d2_pqformula3}),
1.477 + Celem.Thm("d2_pqformula3",TermC.num_str @{thm d2_pqformula3}),
1.478 (* p+ x+ x^2=0 *)
1.479 - Thm("d2_pqformula3_neg",TermC.num_str @{thm d2_pqformula3_neg}),
1.480 + Celem.Thm("d2_pqformula3_neg",TermC.num_str @{thm d2_pqformula3_neg}),
1.481 (* p+ x+ x^2=0 *)
1.482 - Thm("d2_pqformula4",TermC.num_str @{thm d2_pqformula4}),
1.483 + Celem.Thm("d2_pqformula4",TermC.num_str @{thm d2_pqformula4}),
1.484 (* p+ x+1x^2=0 *)
1.485 - Thm("d2_pqformula4_neg",TermC.num_str @{thm d2_pqformula4_neg}),
1.486 + Celem.Thm("d2_pqformula4_neg",TermC.num_str @{thm d2_pqformula4_neg}),
1.487 (* p+ x+1x^2=0 *)
1.488 - Thm("d2_abcformula1",TermC.num_str @{thm d2_abcformula1}),
1.489 + Celem.Thm("d2_abcformula1",TermC.num_str @{thm d2_abcformula1}),
1.490 (* c+bx+cx^2=0 *)
1.491 - Thm("d2_abcformula1_neg",TermC.num_str @{thm d2_abcformula1_neg}),
1.492 + Celem.Thm("d2_abcformula1_neg",TermC.num_str @{thm d2_abcformula1_neg}),
1.493 (* c+bx+cx^2=0 *)
1.494 - Thm("d2_abcformula2",TermC.num_str @{thm d2_abcformula2}),
1.495 + Celem.Thm("d2_abcformula2",TermC.num_str @{thm d2_abcformula2}),
1.496 (* c+ x+cx^2=0 *)
1.497 - Thm("d2_abcformula2_neg",TermC.num_str @{thm d2_abcformula2_neg}),
1.498 + Celem.Thm("d2_abcformula2_neg",TermC.num_str @{thm d2_abcformula2_neg}),
1.499 (* c+ x+cx^2=0 *)
1.500 - Thm("d2_prescind1",TermC.num_str @{thm d2_prescind1}),
1.501 + Celem.Thm("d2_prescind1",TermC.num_str @{thm d2_prescind1}),
1.502 (* ax+bx^2=0 -> x(a+bx)=0 *)
1.503 - Thm("d2_prescind2",TermC.num_str @{thm d2_prescind2}),
1.504 + Celem.Thm("d2_prescind2",TermC.num_str @{thm d2_prescind2}),
1.505 (* ax+ x^2=0 -> x(a+ x)=0 *)
1.506 - Thm("d2_prescind3",TermC.num_str @{thm d2_prescind3}),
1.507 + Celem.Thm("d2_prescind3",TermC.num_str @{thm d2_prescind3}),
1.508 (* x+bx^2=0 -> x(1+bx)=0 *)
1.509 - Thm("d2_prescind4",TermC.num_str @{thm d2_prescind4}),
1.510 + Celem.Thm("d2_prescind4",TermC.num_str @{thm d2_prescind4}),
1.511 (* x+ x^2=0 -> x(1+ x)=0 *)
1.512 - Thm("d2_isolate_add1",TermC.num_str @{thm d2_isolate_add1}),
1.513 + Celem.Thm("d2_isolate_add1",TermC.num_str @{thm d2_isolate_add1}),
1.514 (* a+ bx^2=0 -> bx^2=(-1)a*)
1.515 - Thm("d2_isolate_add2",TermC.num_str @{thm d2_isolate_add2}),
1.516 + Celem.Thm("d2_isolate_add2",TermC.num_str @{thm d2_isolate_add2}),
1.517 (* a+ x^2=0 -> x^2=(-1)a*)
1.518 - Thm("d2_sqrt_equation1",TermC.num_str @{thm d2_sqrt_equation1}),
1.519 + Celem.Thm("d2_sqrt_equation1",TermC.num_str @{thm d2_sqrt_equation1}),
1.520 (* x^2=c -> x=+-sqrt(c)*)
1.521 - Thm("d2_sqrt_equation1_neg",TermC.num_str @{thm d2_sqrt_equation1_neg}),
1.522 + Celem.Thm("d2_sqrt_equation1_neg",TermC.num_str @{thm d2_sqrt_equation1_neg}),
1.523 (* [c<0] x^2=c -> x=[]*)
1.524 - Thm("d2_sqrt_equation2",TermC.num_str @{thm d2_sqrt_equation2}),
1.525 + Celem.Thm("d2_sqrt_equation2",TermC.num_str @{thm d2_sqrt_equation2}),
1.526 (* x^2=0 -> x=0 *)
1.527 - Thm("d2_reduce_equation1",TermC.num_str @{thm d2_reduce_equation1}),
1.528 + Celem.Thm("d2_reduce_equation1",TermC.num_str @{thm d2_reduce_equation1}),
1.529 (* x(a+bx)=0 -> x=0 | a+bx=0*)
1.530 - Thm("d2_reduce_equation2",TermC.num_str @{thm d2_reduce_equation2}),
1.531 + Celem.Thm("d2_reduce_equation2",TermC.num_str @{thm d2_reduce_equation2}),
1.532 (* x(a+ x)=0 -> x=0 | a+ x=0*)
1.533 - Thm("d2_isolate_div",TermC.num_str @{thm d2_isolate_div})
1.534 + Celem.Thm("d2_isolate_div",TermC.num_str @{thm d2_isolate_div})
1.535 (* bx^2=c -> x^2=c/b*)
1.536 ],
1.537 - scr = Prog ((Thm.term_of o the o (TermC.parse thy)) "empty_script")
1.538 - }:rls);
1.539 + scr = Celem.Prog ((Thm.term_of o the o (TermC.parse thy)) "empty_script")
1.540 + });
1.541 *}
1.542 ML{*
1.543
1.544 (* -- d3 -- *)
1.545 (* isolate the bound variable in an d3 equation; 'bdv' is a meta-constant *)
1.546 val d3_polyeq_simplify = prep_rls'(
1.547 - Rls {id = "d3_polyeq_simplify", preconds = [],
1.548 - rew_ord = ("e_rew_ord",e_rew_ord), erls = PolyEq_erls,
1.549 - srls = Erls, calc = [], errpatts = [],
1.550 + Celem.Rls {id = "d3_polyeq_simplify", preconds = [],
1.551 + rew_ord = ("xxxe_rew_ordxxx",Celem.e_rew_ord), erls = PolyEq_erls,
1.552 + srls = Celem.Erls, calc = [], errpatts = [],
1.553 rules =
1.554 - [Thm("d3_reduce_equation1",TermC.num_str @{thm d3_reduce_equation1}),
1.555 + [Celem.Thm("d3_reduce_equation1",TermC.num_str @{thm d3_reduce_equation1}),
1.556 (*a*bdv + b*bdv^^^2 + c*bdv^^^3=0) =
1.557 (bdv=0 | (a + b*bdv + c*bdv^^^2=0)*)
1.558 - Thm("d3_reduce_equation2",TermC.num_str @{thm d3_reduce_equation2}),
1.559 + Celem.Thm("d3_reduce_equation2",TermC.num_str @{thm d3_reduce_equation2}),
1.560 (* bdv + b*bdv^^^2 + c*bdv^^^3=0) =
1.561 (bdv=0 | (1 + b*bdv + c*bdv^^^2=0)*)
1.562 - Thm("d3_reduce_equation3",TermC.num_str @{thm d3_reduce_equation3}),
1.563 + Celem.Thm("d3_reduce_equation3",TermC.num_str @{thm d3_reduce_equation3}),
1.564 (*a*bdv + bdv^^^2 + c*bdv^^^3=0) =
1.565 (bdv=0 | (a + bdv + c*bdv^^^2=0)*)
1.566 - Thm("d3_reduce_equation4",TermC.num_str @{thm d3_reduce_equation4}),
1.567 + Celem.Thm("d3_reduce_equation4",TermC.num_str @{thm d3_reduce_equation4}),
1.568 (* bdv + bdv^^^2 + c*bdv^^^3=0) =
1.569 (bdv=0 | (1 + bdv + c*bdv^^^2=0)*)
1.570 - Thm("d3_reduce_equation5",TermC.num_str @{thm d3_reduce_equation5}),
1.571 + Celem.Thm("d3_reduce_equation5",TermC.num_str @{thm d3_reduce_equation5}),
1.572 (*a*bdv + b*bdv^^^2 + bdv^^^3=0) =
1.573 (bdv=0 | (a + b*bdv + bdv^^^2=0)*)
1.574 - Thm("d3_reduce_equation6",TermC.num_str @{thm d3_reduce_equation6}),
1.575 + Celem.Thm("d3_reduce_equation6",TermC.num_str @{thm d3_reduce_equation6}),
1.576 (* bdv + b*bdv^^^2 + bdv^^^3=0) =
1.577 (bdv=0 | (1 + b*bdv + bdv^^^2=0)*)
1.578 - Thm("d3_reduce_equation7",TermC.num_str @{thm d3_reduce_equation7}),
1.579 + Celem.Thm("d3_reduce_equation7",TermC.num_str @{thm d3_reduce_equation7}),
1.580 (*a*bdv + bdv^^^2 + bdv^^^3=0) =
1.581 (bdv=0 | (1 + bdv + bdv^^^2=0)*)
1.582 - Thm("d3_reduce_equation8",TermC.num_str @{thm d3_reduce_equation8}),
1.583 + Celem.Thm("d3_reduce_equation8",TermC.num_str @{thm d3_reduce_equation8}),
1.584 (* bdv + bdv^^^2 + bdv^^^3=0) =
1.585 (bdv=0 | (1 + bdv + bdv^^^2=0)*)
1.586 - Thm("d3_reduce_equation9",TermC.num_str @{thm d3_reduce_equation9}),
1.587 + Celem.Thm("d3_reduce_equation9",TermC.num_str @{thm d3_reduce_equation9}),
1.588 (*a*bdv + c*bdv^^^3=0) =
1.589 (bdv=0 | (a + c*bdv^^^2=0)*)
1.590 - Thm("d3_reduce_equation10",TermC.num_str @{thm d3_reduce_equation10}),
1.591 + Celem.Thm("d3_reduce_equation10",TermC.num_str @{thm d3_reduce_equation10}),
1.592 (* bdv + c*bdv^^^3=0) =
1.593 (bdv=0 | (1 + c*bdv^^^2=0)*)
1.594 - Thm("d3_reduce_equation11",TermC.num_str @{thm d3_reduce_equation11}),
1.595 + Celem.Thm("d3_reduce_equation11",TermC.num_str @{thm d3_reduce_equation11}),
1.596 (*a*bdv + bdv^^^3=0) =
1.597 (bdv=0 | (a + bdv^^^2=0)*)
1.598 - Thm("d3_reduce_equation12",TermC.num_str @{thm d3_reduce_equation12}),
1.599 + Celem.Thm("d3_reduce_equation12",TermC.num_str @{thm d3_reduce_equation12}),
1.600 (* bdv + bdv^^^3=0) =
1.601 (bdv=0 | (1 + bdv^^^2=0)*)
1.602 - Thm("d3_reduce_equation13",TermC.num_str @{thm d3_reduce_equation13}),
1.603 + Celem.Thm("d3_reduce_equation13",TermC.num_str @{thm d3_reduce_equation13}),
1.604 (* b*bdv^^^2 + c*bdv^^^3=0) =
1.605 (bdv=0 | ( b*bdv + c*bdv^^^2=0)*)
1.606 - Thm("d3_reduce_equation14",TermC.num_str @{thm d3_reduce_equation14}),
1.607 + Celem.Thm("d3_reduce_equation14",TermC.num_str @{thm d3_reduce_equation14}),
1.608 (* bdv^^^2 + c*bdv^^^3=0) =
1.609 (bdv=0 | ( bdv + c*bdv^^^2=0)*)
1.610 - Thm("d3_reduce_equation15",TermC.num_str @{thm d3_reduce_equation15}),
1.611 + Celem.Thm("d3_reduce_equation15",TermC.num_str @{thm d3_reduce_equation15}),
1.612 (* b*bdv^^^2 + bdv^^^3=0) =
1.613 (bdv=0 | ( b*bdv + bdv^^^2=0)*)
1.614 - Thm("d3_reduce_equation16",TermC.num_str @{thm d3_reduce_equation16}),
1.615 + Celem.Thm("d3_reduce_equation16",TermC.num_str @{thm d3_reduce_equation16}),
1.616 (* bdv^^^2 + bdv^^^3=0) =
1.617 (bdv=0 | ( bdv + bdv^^^2=0)*)
1.618 - Thm("d3_isolate_add1",TermC.num_str @{thm d3_isolate_add1}),
1.619 + Celem.Thm("d3_isolate_add1",TermC.num_str @{thm d3_isolate_add1}),
1.620 (*[|Not(bdv occurs_in a)|] ==> (a + b*bdv^^^3=0) =
1.621 (bdv=0 | (b*bdv^^^3=a)*)
1.622 - Thm("d3_isolate_add2",TermC.num_str @{thm d3_isolate_add2}),
1.623 + Celem.Thm("d3_isolate_add2",TermC.num_str @{thm d3_isolate_add2}),
1.624 (*[|Not(bdv occurs_in a)|] ==> (a + bdv^^^3=0) =
1.625 (bdv=0 | ( bdv^^^3=a)*)
1.626 - Thm("d3_isolate_div",TermC.num_str @{thm d3_isolate_div}),
1.627 + Celem.Thm("d3_isolate_div",TermC.num_str @{thm d3_isolate_div}),
1.628 (*[|Not(b=0)|] ==> (b*bdv^^^3=c) = (bdv^^^3=c/b*)
1.629 - Thm("d3_root_equation2",TermC.num_str @{thm d3_root_equation2}),
1.630 + Celem.Thm("d3_root_equation2",TermC.num_str @{thm d3_root_equation2}),
1.631 (*(bdv^^^3=0) = (bdv=0) *)
1.632 - Thm("d3_root_equation1",TermC.num_str @{thm d3_root_equation1})
1.633 + Celem.Thm("d3_root_equation1",TermC.num_str @{thm d3_root_equation1})
1.634 (*bdv^^^3=c) = (bdv = nroot 3 c*)
1.635 ],
1.636 - scr = Prog ((Thm.term_of o the o (TermC.parse thy)) "empty_script")
1.637 - }:rls);
1.638 + scr = Celem.Prog ((Thm.term_of o the o (TermC.parse thy)) "empty_script")
1.639 + });
1.640 *}
1.641 ML{*
1.642
1.643 (* -- d4 -- *)
1.644 (*isolate the bound variable in an d4 equation; 'bdv' is a meta-constant*)
1.645 val d4_polyeq_simplify = prep_rls'(
1.646 - Rls {id = "d4_polyeq_simplify", preconds = [],
1.647 - rew_ord = ("e_rew_ord",e_rew_ord), erls = PolyEq_erls,
1.648 - srls = Erls, calc = [], errpatts = [],
1.649 + Celem.Rls {id = "d4_polyeq_simplify", preconds = [],
1.650 + rew_ord = ("xxxe_rew_ordxxx",Celem.e_rew_ord), erls = PolyEq_erls,
1.651 + srls = Celem.Erls, calc = [], errpatts = [],
1.652 rules =
1.653 - [Thm("d4_sub_u1",TermC.num_str @{thm d4_sub_u1})
1.654 + [Celem.Thm("d4_sub_u1",TermC.num_str @{thm d4_sub_u1})
1.655 (* ax^4+bx^2+c=0 -> x=+-sqrt(ax^2+bx^+c) *)
1.656 ],
1.657 - scr = Prog ((Thm.term_of o the o (TermC.parse thy)) "empty_script")
1.658 - }:rls);
1.659 + scr = Celem.Prog ((Thm.term_of o the o (TermC.parse thy)) "empty_script")
1.660 + });
1.661 *}
1.662 setup {* KEStore_Elems.add_rlss
1.663 [("d0_polyeq_simplify", (Context.theory_name @{theory}, d0_polyeq_simplify)),
1.664 @@ -831,7 +831,7 @@
1.665 *)
1.666 *}
1.667 setup {* KEStore_Elems.add_pbts
1.668 - [(Specify.prep_pbt thy "pbl_equ_univ_poly" [] e_pblID
1.669 + [(Specify.prep_pbt thy "pbl_equ_univ_poly" [] Celem.e_pblID
1.670 (["polynomial","univariate","equation"],
1.671 [("#Given" ,["equality e_e","solveFor v_v"]),
1.672 ("#Where" ,["~((e_e::bool) is_ratequation_in (v_v::real))",
1.673 @@ -840,7 +840,7 @@
1.674 ("#Find" ,["solutions v_v'i'"])],
1.675 PolyEq_prls, SOME "solve (e_e::bool, v_v)", [])),
1.676 (*--- d0 ---*)
1.677 - (Specify.prep_pbt thy "pbl_equ_univ_poly_deg0" [] e_pblID
1.678 + (Specify.prep_pbt thy "pbl_equ_univ_poly_deg0" [] Celem.e_pblID
1.679 (["degree_0","polynomial","univariate","equation"],
1.680 [("#Given" ,["equality e_e","solveFor v_v"]),
1.681 ("#Where" ,["matches (?a = 0) e_e",
1.682 @@ -849,7 +849,7 @@
1.683 ("#Find" ,["solutions v_v'i'"])],
1.684 PolyEq_prls, SOME "solve (e_e::bool, v_v)", [["PolyEq","solve_d0_polyeq_equation"]])),
1.685 (*--- d1 ---*)
1.686 - (Specify.prep_pbt thy "pbl_equ_univ_poly_deg1" [] e_pblID
1.687 + (Specify.prep_pbt thy "pbl_equ_univ_poly_deg1" [] Celem.e_pblID
1.688 (["degree_1","polynomial","univariate","equation"],
1.689 [("#Given" ,["equality e_e","solveFor v_v"]),
1.690 ("#Where" ,["matches (?a = 0) e_e",
1.691 @@ -858,7 +858,7 @@
1.692 ("#Find" ,["solutions v_v'i'"])],
1.693 PolyEq_prls, SOME "solve (e_e::bool, v_v)", [["PolyEq","solve_d1_polyeq_equation"]])),
1.694 (*--- d2 ---*)
1.695 - (Specify.prep_pbt thy "pbl_equ_univ_poly_deg2" [] e_pblID
1.696 + (Specify.prep_pbt thy "pbl_equ_univ_poly_deg2" [] Celem.e_pblID
1.697 (["degree_2","polynomial","univariate","equation"],
1.698 [("#Given" ,["equality e_e","solveFor v_v"]),
1.699 ("#Where" ,["matches (?a = 0) e_e",
1.700 @@ -866,7 +866,7 @@
1.701 "((lhs e_e) has_degree_in v_v ) = 2"]),
1.702 ("#Find" ,["solutions v_v'i'"])],
1.703 PolyEq_prls, SOME "solve (e_e::bool, v_v)", [["PolyEq","solve_d2_polyeq_equation"]])),
1.704 - (Specify.prep_pbt thy "pbl_equ_univ_poly_deg2_sqonly" [] e_pblID
1.705 + (Specify.prep_pbt thy "pbl_equ_univ_poly_deg2_sqonly" [] Celem.e_pblID
1.706 (["sq_only","degree_2","polynomial","univariate","equation"],
1.707 [("#Given" ,["equality e_e","solveFor v_v"]),
1.708 ("#Where" ,["matches ( ?a + ?v_^^^2 = 0) e_e | " ^
1.709 @@ -884,7 +884,7 @@
1.710 ("#Find" ,["solutions v_v'i'"])],
1.711 PolyEq_prls, SOME "solve (e_e::bool, v_v)",
1.712 [["PolyEq","solve_d2_polyeq_sqonly_equation"]])),
1.713 - (Specify.prep_pbt thy "pbl_equ_univ_poly_deg2_bdvonly" [] e_pblID
1.714 + (Specify.prep_pbt thy "pbl_equ_univ_poly_deg2_bdvonly" [] Celem.e_pblID
1.715 (["bdv_only","degree_2","polynomial","univariate","equation"],
1.716 [("#Given", ["equality e_e","solveFor v_v"]),
1.717 ("#Where", ["matches (?a*?v_ + ?v_^^^2 = 0) e_e | " ^
1.718 @@ -896,14 +896,14 @@
1.719 ("#Find", ["solutions v_v'i'"])],
1.720 PolyEq_prls, SOME "solve (e_e::bool, v_v)",
1.721 [["PolyEq","solve_d2_polyeq_bdvonly_equation"]])),
1.722 - (Specify.prep_pbt thy "pbl_equ_univ_poly_deg2_pq" [] e_pblID
1.723 + (Specify.prep_pbt thy "pbl_equ_univ_poly_deg2_pq" [] Celem.e_pblID
1.724 (["pqFormula","degree_2","polynomial","univariate","equation"],
1.725 [("#Given", ["equality e_e","solveFor v_v"]),
1.726 ("#Where", ["matches (?a + 1*?v_^^^2 = 0) e_e | " ^
1.727 "matches (?a + ?v_^^^2 = 0) e_e"]),
1.728 ("#Find", ["solutions v_v'i'"])],
1.729 PolyEq_prls, SOME "solve (e_e::bool, v_v)", [["PolyEq","solve_d2_polyeq_pq_equation"]])),
1.730 - (Specify.prep_pbt thy "pbl_equ_univ_poly_deg2_abc" [] e_pblID
1.731 + (Specify.prep_pbt thy "pbl_equ_univ_poly_deg2_abc" [] Celem.e_pblID
1.732 (["abcFormula","degree_2","polynomial","univariate","equation"],
1.733 [("#Given", ["equality e_e","solveFor v_v"]),
1.734 ("#Where", ["matches (?a + ?v_^^^2 = 0) e_e | " ^
1.735 @@ -911,7 +911,7 @@
1.736 ("#Find", ["solutions v_v'i'"])],
1.737 PolyEq_prls, SOME "solve (e_e::bool, v_v)", [["PolyEq","solve_d2_polyeq_abc_equation"]])),
1.738 (*--- d3 ---*)
1.739 - (Specify.prep_pbt thy "pbl_equ_univ_poly_deg3" [] e_pblID
1.740 + (Specify.prep_pbt thy "pbl_equ_univ_poly_deg3" [] Celem.e_pblID
1.741 (["degree_3","polynomial","univariate","equation"],
1.742 [("#Given", ["equality e_e","solveFor v_v"]),
1.743 ("#Where", ["matches (?a = 0) e_e",
1.744 @@ -920,7 +920,7 @@
1.745 ("#Find", ["solutions v_v'i'"])],
1.746 PolyEq_prls, SOME "solve (e_e::bool, v_v)", [["PolyEq","solve_d3_polyeq_equation"]])),
1.747 (*--- d4 ---*)
1.748 - (Specify.prep_pbt thy "pbl_equ_univ_poly_deg4" [] e_pblID
1.749 + (Specify.prep_pbt thy "pbl_equ_univ_poly_deg4" [] Celem.e_pblID
1.750 (["degree_4","polynomial","univariate","equation"],
1.751 [("#Given", ["equality e_e","solveFor v_v"]),
1.752 ("#Where", ["matches (?a = 0) e_e",
1.753 @@ -929,7 +929,7 @@
1.754 ("#Find", ["solutions v_v'i'"])],
1.755 PolyEq_prls, SOME "solve (e_e::bool, v_v)", [(*["PolyEq","solve_d4_polyeq_equation"]*)])),
1.756 (*--- normalise ---*)
1.757 - (Specify.prep_pbt thy "pbl_equ_univ_poly_norm" [] e_pblID
1.758 + (Specify.prep_pbt thy "pbl_equ_univ_poly_norm" [] Celem.e_pblID
1.759 (["normalise","polynomial","univariate","equation"],
1.760 [("#Given", ["equality e_e","solveFor v_v"]),
1.761 ("#Where", ["(Not((matches (?a = 0 ) e_e ))) |" ^
1.762 @@ -937,7 +937,7 @@
1.763 ("#Find", ["solutions v_v'i'"])],
1.764 PolyEq_prls, SOME "solve (e_e::bool, v_v)", [["PolyEq","normalise_poly"]])),
1.765 (*-------------------------expanded-----------------------*)
1.766 - (Specify.prep_pbt thy "pbl_equ_univ_expand" [] e_pblID
1.767 + (Specify.prep_pbt thy "pbl_equ_univ_expand" [] Celem.e_pblID
1.768 (["expanded","univariate","equation"],
1.769 [("#Given", ["equality e_e","solveFor v_v"]),
1.770 ("#Where", ["matches (?a = 0) e_e",
1.771 @@ -945,7 +945,7 @@
1.772 ("#Find", ["solutions v_v'i'"])],
1.773 PolyEq_prls, SOME "solve (e_e::bool, v_v)", [])),
1.774 (*--- d2 ---*)
1.775 - (Specify.prep_pbt thy "pbl_equ_univ_expand_deg2" [] e_pblID
1.776 + (Specify.prep_pbt thy "pbl_equ_univ_expand_deg2" [] Celem.e_pblID
1.777 (["degree_2","expanded","univariate","equation"],
1.778 [("#Given", ["equality e_e","solveFor v_v"]),
1.779 ("#Where", ["((lhs e_e) has_degree_in v_v) = 2"]),
1.780 @@ -968,17 +968,17 @@
1.781
1.782 text {* "-------------------------methods-----------------------" *}
1.783 setup {* KEStore_Elems.add_mets
1.784 - [Specify.prep_met thy "met_polyeq" [] e_metID
1.785 + [Specify.prep_met thy "met_polyeq" [] Celem.e_metID
1.786 (["PolyEq"], [],
1.787 - {rew_ord'="tless_true",rls'=Atools_erls,calc = [], srls = e_rls, prls=e_rls,
1.788 + {rew_ord'="tless_true",rls'=Atools_erls,calc = [], srls = Celem.e_rls, prls=Celem.e_rls,
1.789 crls=PolyEq_crls, errpats = [], nrls = norm_Rational},
1.790 "empty_script"),
1.791 - Specify.prep_met thy "met_polyeq_norm" [] e_metID
1.792 + Specify.prep_met thy "met_polyeq_norm" [] Celem.e_metID
1.793 (["PolyEq","normalise_poly"],
1.794 [("#Given" ,["equality e_e","solveFor v_v"]),
1.795 ("#Where" ,["(Not((matches (?a = 0 ) e_e ))) |(Not(((lhs e_e) is_poly_in v_v)))"]),
1.796 ("#Find" ,["solutions v_v'i'"])],
1.797 - {rew_ord'="termlessI", rls'=PolyEq_erls, srls=e_rls, prls=PolyEq_prls, calc=[],
1.798 + {rew_ord'="termlessI", rls'=PolyEq_erls, srls=Celem.e_rls, prls=PolyEq_prls, calc=[],
1.799 crls=PolyEq_crls, errpats = [], nrls = norm_Rational},
1.800 "Script Normalize_poly (e_e::bool) (v_v::real) = " ^
1.801 "(let e_e =((Try (Rewrite all_left False)) @@ " ^
1.802 @@ -989,24 +989,24 @@
1.803 " (Try (Repeat (Rewrite_Set polyeq_simplify False)))) e_e " ^
1.804 " in (SubProblem (PolyEq',[polynomial,univariate,equation], [no_met]) " ^
1.805 " [BOOL e_e, REAL v_v]))"),
1.806 - Specify.prep_met thy "met_polyeq_d0" [] e_metID
1.807 + Specify.prep_met thy "met_polyeq_d0" [] Celem.e_metID
1.808 (["PolyEq","solve_d0_polyeq_equation"],
1.809 [("#Given" ,["equality e_e","solveFor v_v"]),
1.810 ("#Where" ,["(lhs e_e) is_poly_in v_v ", "((lhs e_e) has_degree_in v_v) = 0"]),
1.811 ("#Find" ,["solutions v_v'i'"])],
1.812 - {rew_ord'="termlessI", rls'=PolyEq_erls, srls=e_rls, prls=PolyEq_prls,
1.813 + {rew_ord'="termlessI", rls'=PolyEq_erls, srls=Celem.e_rls, prls=PolyEq_prls,
1.814 calc=[("sqrt", ("NthRoot.sqrt", eval_sqrt "#sqrt_"))], crls=PolyEq_crls, errpats = [],
1.815 nrls = norm_Rational},
1.816 "Script Solve_d0_polyeq_equation (e_e::bool) (v_v::real) = " ^
1.817 "(let e_e = ((Try (Rewrite_Set_Inst [(bdv,v_v::real)] " ^
1.818 " d0_polyeq_simplify False))) e_e " ^
1.819 " in ((Or_to_List e_e)::bool list))"),
1.820 - Specify.prep_met thy "met_polyeq_d1" [] e_metID
1.821 + Specify.prep_met thy "met_polyeq_d1" [] Celem.e_metID
1.822 (["PolyEq","solve_d1_polyeq_equation"],
1.823 [("#Given" ,["equality e_e","solveFor v_v"]),
1.824 ("#Where" ,["(lhs e_e) is_poly_in v_v ", "((lhs e_e) has_degree_in v_v) = 1"]),
1.825 ("#Find" ,["solutions v_v'i'"])],
1.826 - {rew_ord'="termlessI", rls'=PolyEq_erls, srls=e_rls, prls=PolyEq_prls,
1.827 + {rew_ord'="termlessI", rls'=PolyEq_erls, srls=Celem.e_rls, prls=PolyEq_prls,
1.828 calc=[("sqrt", ("NthRoot.sqrt", eval_sqrt "#sqrt_"))], crls=PolyEq_crls, errpats = [],
1.829 nrls = norm_Rational},
1.830 "Script Solve_d1_polyeq_equation (e_e::bool) (v_v::real) = " ^
1.831 @@ -1016,12 +1016,12 @@
1.832 " (Try (Rewrite_Set norm_Rational_parenthesized False))) e_e;" ^
1.833 " (L_L::bool list) = ((Or_to_List e_e)::bool list) " ^
1.834 " in Check_elementwise L_L {(v_v::real). Assumptions} )"),
1.835 - Specify.prep_met thy "met_polyeq_d22" [] e_metID
1.836 + Specify.prep_met thy "met_polyeq_d22" [] Celem.e_metID
1.837 (["PolyEq","solve_d2_polyeq_equation"],
1.838 [("#Given" ,["equality e_e","solveFor v_v"]),
1.839 ("#Where" ,["(lhs e_e) is_poly_in v_v ", "((lhs e_e) has_degree_in v_v) = 2"]),
1.840 ("#Find" ,["solutions v_v'i'"])],
1.841 - {rew_ord'="termlessI", rls'=PolyEq_erls, srls=e_rls, prls=PolyEq_prls,
1.842 + {rew_ord'="termlessI", rls'=PolyEq_erls, srls=Celem.e_rls, prls=PolyEq_prls,
1.843 calc=[("sqrt", ("NthRoot.sqrt", eval_sqrt "#sqrt_"))], crls=PolyEq_crls, errpats = [],
1.844 nrls = norm_Rational},
1.845 "Script Solve_d2_polyeq_equation (e_e::bool) (v_v::real) = " ^
1.846 @@ -1034,12 +1034,12 @@
1.847 " (Try (Rewrite_Set norm_Rational_parenthesized False))) e_e;" ^
1.848 " (L_L::bool list) = ((Or_to_List e_e)::bool list) " ^
1.849 " in Check_elementwise L_L {(v_v::real). Assumptions} )"),
1.850 - Specify.prep_met thy "met_polyeq_d2_bdvonly" [] e_metID
1.851 + Specify.prep_met thy "met_polyeq_d2_bdvonly" [] Celem.e_metID
1.852 (["PolyEq","solve_d2_polyeq_bdvonly_equation"],
1.853 [("#Given" ,["equality e_e","solveFor v_v"]),
1.854 ("#Where" ,["(lhs e_e) is_poly_in v_v ", "((lhs e_e) has_degree_in v_v) = 2"]),
1.855 ("#Find" ,["solutions v_v'i'"])],
1.856 - {rew_ord'="termlessI", rls'=PolyEq_erls, srls=e_rls, prls=PolyEq_prls,
1.857 + {rew_ord'="termlessI", rls'=PolyEq_erls, srls=Celem.e_rls, prls=PolyEq_prls,
1.858 calc=[("sqrt", ("NthRoot.sqrt", eval_sqrt "#sqrt_"))], crls=PolyEq_crls, errpats = [],
1.859 nrls = norm_Rational},
1.860 "Script Solve_d2_polyeq_bdvonly_equation (e_e::bool) (v_v::real) =" ^
1.861 @@ -1052,12 +1052,12 @@
1.862 " (Try (Rewrite_Set norm_Rational_parenthesized False))) e_e;" ^
1.863 " (L_L::bool list) = ((Or_to_List e_e)::bool list) " ^
1.864 " in Check_elementwise L_L {(v_v::real). Assumptions} )"),
1.865 - Specify.prep_met thy "met_polyeq_d2_sqonly" [] e_metID
1.866 + Specify.prep_met thy "met_polyeq_d2_sqonly" [] Celem.e_metID
1.867 (["PolyEq","solve_d2_polyeq_sqonly_equation"],
1.868 [("#Given" ,["equality e_e","solveFor v_v"]),
1.869 ("#Where" ,["(lhs e_e) is_poly_in v_v ", "((lhs e_e) has_degree_in v_v) = 2"]),
1.870 ("#Find" ,["solutions v_v'i'"])],
1.871 - {rew_ord'="termlessI", rls'=PolyEq_erls, srls=e_rls, prls=PolyEq_prls,
1.872 + {rew_ord'="termlessI", rls'=PolyEq_erls, srls=Celem.e_rls, prls=PolyEq_prls,
1.873 calc=[("sqrt", ("NthRoot.sqrt", eval_sqrt "#sqrt_"))], crls=PolyEq_crls, errpats = [],
1.874 nrls = norm_Rational},
1.875 "Script Solve_d2_polyeq_sqonly_equation (e_e::bool) (v_v::real) =" ^
1.876 @@ -1067,12 +1067,12 @@
1.877 " (Try (Rewrite_Set norm_Rational_parenthesized False))) e_e; " ^
1.878 " (L_L::bool list) = ((Or_to_List e_e)::bool list) " ^
1.879 " in Check_elementwise L_L {(v_v::real). Assumptions} )"),
1.880 - Specify.prep_met thy "met_polyeq_d2_pq" [] e_metID
1.881 + Specify.prep_met thy "met_polyeq_d2_pq" [] Celem.e_metID
1.882 (["PolyEq","solve_d2_polyeq_pq_equation"],
1.883 [("#Given" ,["equality e_e","solveFor v_v"]),
1.884 ("#Where" ,["(lhs e_e) is_poly_in v_v ", "((lhs e_e) has_degree_in v_v) = 2"]),
1.885 ("#Find" ,["solutions v_v'i'"])],
1.886 - {rew_ord'="termlessI", rls'=PolyEq_erls, srls=e_rls, prls=PolyEq_prls,
1.887 + {rew_ord'="termlessI", rls'=PolyEq_erls, srls=Celem.e_rls, prls=PolyEq_prls,
1.888 calc=[("sqrt", ("NthRoot.sqrt", eval_sqrt "#sqrt_"))], crls=PolyEq_crls, errpats = [],
1.889 nrls = norm_Rational},
1.890 "Script Solve_d2_polyeq_pq_equation (e_e::bool) (v_v::real) = " ^
1.891 @@ -1082,12 +1082,12 @@
1.892 " (Try (Rewrite_Set norm_Rational_parenthesized False))) e_e;" ^
1.893 " (L_L::bool list) = ((Or_to_List e_e)::bool list) " ^
1.894 " in Check_elementwise L_L {(v_v::real). Assumptions} )"),
1.895 - Specify.prep_met thy "met_polyeq_d2_abc" [] e_metID
1.896 + Specify.prep_met thy "met_polyeq_d2_abc" [] Celem.e_metID
1.897 (["PolyEq","solve_d2_polyeq_abc_equation"],
1.898 [("#Given" ,["equality e_e","solveFor v_v"]),
1.899 ("#Where" ,["(lhs e_e) is_poly_in v_v ", "((lhs e_e) has_degree_in v_v) = 2"]),
1.900 ("#Find" ,["solutions v_v'i'"])],
1.901 - {rew_ord'="termlessI", rls'=PolyEq_erls,srls=e_rls, prls=PolyEq_prls,
1.902 + {rew_ord'="termlessI", rls'=PolyEq_erls,srls=Celem.e_rls, prls=PolyEq_prls,
1.903 calc=[("sqrt", ("NthRoot.sqrt", eval_sqrt "#sqrt_"))], crls=PolyEq_crls, errpats = [],
1.904 nrls = norm_Rational},
1.905 "Script Solve_d2_polyeq_abc_equation (e_e::bool) (v_v::real) = " ^
1.906 @@ -1097,12 +1097,12 @@
1.907 " (Try (Rewrite_Set norm_Rational_parenthesized False))) e_e;" ^
1.908 " (L_L::bool list) = ((Or_to_List e_e)::bool list) " ^
1.909 " in Check_elementwise L_L {(v_v::real). Assumptions} )"),
1.910 - Specify.prep_met thy "met_polyeq_d3" [] e_metID
1.911 + Specify.prep_met thy "met_polyeq_d3" [] Celem.e_metID
1.912 (["PolyEq","solve_d3_polyeq_equation"],
1.913 [("#Given" ,["equality e_e","solveFor v_v"]),
1.914 ("#Where" ,["(lhs e_e) is_poly_in v_v ", "((lhs e_e) has_degree_in v_v) = 3"]),
1.915 ("#Find" ,["solutions v_v'i'"])],
1.916 - {rew_ord'="termlessI", rls'=PolyEq_erls, srls=e_rls, prls=PolyEq_prls,
1.917 + {rew_ord'="termlessI", rls'=PolyEq_erls, srls=Celem.e_rls, prls=PolyEq_prls,
1.918 calc=[("sqrt", ("NthRoot.sqrt", eval_sqrt "#sqrt_"))], crls=PolyEq_crls, errpats = [],
1.919 nrls = norm_Rational},
1.920 "Script Solve_d3_polyeq_equation (e_e::bool) (v_v::real) = " ^
1.921 @@ -1121,12 +1121,12 @@
1.922 (*.solves all expanded (ie. normalised) terms of degree 2.*)
1.923 (*Oct.02 restriction: 'eval_true 0 =< discriminant' ony for integer values
1.924 by 'PolyEq_erls'; restricted until Float.thy is implemented*)
1.925 - Specify.prep_met thy "met_polyeq_complsq" [] e_metID
1.926 + Specify.prep_met thy "met_polyeq_complsq" [] Celem.e_metID
1.927 (["PolyEq","complete_square"],
1.928 [("#Given" ,["equality e_e","solveFor v_v"]),
1.929 ("#Where" ,["matches (?a = 0) e_e", "((lhs e_e) has_degree_in v_v) = 2"]),
1.930 ("#Find" ,["solutions v_v'i'"])],
1.931 - {rew_ord'="termlessI",rls'=PolyEq_erls,srls=e_rls,prls=PolyEq_prls,
1.932 + {rew_ord'="termlessI",rls'=PolyEq_erls,srls=Celem.e_rls,prls=PolyEq_prls,
1.933 calc=[("sqrt", ("NthRoot.sqrt", eval_sqrt "#sqrt_"))], crls=PolyEq_crls, errpats = [],
1.934 nrls = norm_Rational},
1.935 "Script Complete_square (e_e::bool) (v_v::real) = " ^
1.936 @@ -1169,12 +1169,12 @@
1.937 (Free (xstr,_)) =>
1.938 (if xstr = var then 1000*(the (TermC.int_of_str_opt pot)) else 3)
1.939 | _ => error ("size_of_term' called with subst = "^
1.940 - (term2str x)))
1.941 + (Celem.term2str x)))
1.942 | size_of_term' x (Free (subst,_)) =
1.943 (case x of
1.944 (Free (xstr,_)) => (if xstr = subst then 1000 else 1)
1.945 | _ => error ("size_of_term' called with subst = "^
1.946 - (term2str x)))
1.947 + (Celem.term2str x)))
1.948 | size_of_term' x (Abs (_,_,body)) = 1 + size_of_term' x body
1.949 | size_of_term' x (f$t) = size_of_term' x f + size_of_term' x t
1.950 | size_of_term' x _ = 1;
1.951 @@ -1186,10 +1186,10 @@
1.952 then
1.953 let
1.954 val (f, ts) = strip_comb t and (g, us) = strip_comb u;
1.955 - val _ = tracing ("t= f@ts= \"" ^ term_to_string''' thy f ^ "\" @ \"[" ^
1.956 - commas (map (term_to_string''' thy) ts) ^ "]\"");
1.957 - val _ = tracing ("u= g@us= \"" ^ term_to_string''' thy g ^ "\" @ \"[" ^
1.958 - commas(map (term_to_string''' thy) us) ^ "]\"");
1.959 + val _ = tracing ("t= f@ts= \"" ^ Celem.term_to_string''' thy f ^ "\" @ \"[" ^
1.960 + commas (map (Celem.term_to_string''' thy) ts) ^ "]\"");
1.961 + val _ = tracing ("u= g@us= \"" ^ Celem.term_to_string''' thy g ^ "\" @ \"[" ^
1.962 + commas(map (Celem.term_to_string''' thy) us) ^ "]\"");
1.963 val _ = tracing ("size_of_term(t,u)= (" ^ string_of_int (size_of_term' x t) ^ ", " ^
1.964 string_of_int (size_of_term' x u) ^ ")");
1.965 val _ = tracing ("hd_ord(f,g) = " ^ (pr_ord o (hd_ord x)) (f,g));
1.966 @@ -1210,110 +1210,110 @@
1.967 prod_ord (prod_ord Term_Ord.indexname_ord Term_Ord.typ_ord)
1.968 int_ord (dest_hd' x f, dest_hd' x g)
1.969 and terms_ord x str pr (ts, us) =
1.970 - list_ord (term_ord' x pr (assoc_thy "Isac"))(ts, us);
1.971 + list_ord (term_ord' x pr (Celem.assoc_thy "Isac"))(ts, us);
1.972
1.973 in
1.974
1.975 fun ord_make_polynomial_in (pr:bool) thy subst tu =
1.976 let
1.977 - (* val _=tracing("*** subs variable is: "^(subst2str subst)); *)
1.978 + (* val _=tracing("*** subs variable is: "^(Celem.subst2str subst)); *)
1.979 in
1.980 case subst of
1.981 (_,x)::_ => (term_ord' x pr thy tu = LESS)
1.982 | _ => error ("ord_make_polynomial_in called with subst = "^
1.983 - (subst2str subst))
1.984 + (Celem.subst2str subst))
1.985 end;
1.986 end;(*local*)
1.987
1.988 *}
1.989 ML{*
1.990 val order_add_mult_in = prep_rls'(
1.991 - Rls{id = "order_add_mult_in", preconds = [],
1.992 + Celem.Rls{id = "order_add_mult_in", preconds = [],
1.993 rew_ord = ("ord_make_polynomial_in",
1.994 ord_make_polynomial_in false @{theory "Poly"}),
1.995 - erls = e_rls,srls = Erls,
1.996 + erls = Celem.e_rls,srls = Celem.Erls,
1.997 calc = [], errpatts = [],
1.998 - rules = [Thm ("mult_commute",TermC.num_str @{thm mult.commute}),
1.999 + rules = [Celem.Thm ("mult_commute",TermC.num_str @{thm mult.commute}),
1.1000 (* z * w = w * z *)
1.1001 - Thm ("real_mult_left_commute",TermC.num_str @{thm real_mult_left_commute}),
1.1002 + Celem.Thm ("real_mult_left_commute",TermC.num_str @{thm real_mult_left_commute}),
1.1003 (*z1.0 * (z2.0 * z3.0) = z2.0 * (z1.0 * z3.0)*)
1.1004 - Thm ("mult_assoc",TermC.num_str @{thm mult.assoc}),
1.1005 + Celem.Thm ("mult_assoc",TermC.num_str @{thm mult.assoc}),
1.1006 (*z1.0 * z2.0 * z3.0 = z1.0 * (z2.0 * z3.0)*)
1.1007 - Thm ("add_commute",TermC.num_str @{thm add.commute}),
1.1008 + Celem.Thm ("add_commute",TermC.num_str @{thm add.commute}),
1.1009 (*z + w = w + z*)
1.1010 - Thm ("add_left_commute",TermC.num_str @{thm add.left_commute}),
1.1011 + Celem.Thm ("add_left_commute",TermC.num_str @{thm add.left_commute}),
1.1012 (*x + (y + z) = y + (x + z)*)
1.1013 - Thm ("add_assoc",TermC.num_str @{thm add.assoc})
1.1014 + Celem.Thm ("add_assoc",TermC.num_str @{thm add.assoc})
1.1015 (*z1.0 + z2.0 + z3.0 = z1.0 + (z2.0 + z3.0)*)
1.1016 - ], scr = EmptyScr}:rls);
1.1017 + ], scr = Celem.EmptyScr});
1.1018
1.1019 *}
1.1020 ML{*
1.1021 val collect_bdv = prep_rls'(
1.1022 - Rls{id = "collect_bdv", preconds = [],
1.1023 - rew_ord = ("dummy_ord", dummy_ord),
1.1024 - erls = e_rls,srls = Erls,
1.1025 + Celem.Rls{id = "collect_bdv", preconds = [],
1.1026 + rew_ord = ("dummy_ord", Celem.dummy_ord),
1.1027 + erls = Celem.e_rls,srls = Celem.Erls,
1.1028 calc = [], errpatts = [],
1.1029 - rules = [Thm ("bdv_collect_1",TermC.num_str @{thm bdv_collect_1}),
1.1030 - Thm ("bdv_collect_2",TermC.num_str @{thm bdv_collect_2}),
1.1031 - Thm ("bdv_collect_3",TermC.num_str @{thm bdv_collect_3}),
1.1032 + rules = [Celem.Thm ("bdv_collect_1",TermC.num_str @{thm bdv_collect_1}),
1.1033 + Celem.Thm ("bdv_collect_2",TermC.num_str @{thm bdv_collect_2}),
1.1034 + Celem.Thm ("bdv_collect_3",TermC.num_str @{thm bdv_collect_3}),
1.1035
1.1036 - Thm ("bdv_collect_assoc1_1",TermC.num_str @{thm bdv_collect_assoc1_1}),
1.1037 - Thm ("bdv_collect_assoc1_2",TermC.num_str @{thm bdv_collect_assoc1_2}),
1.1038 - Thm ("bdv_collect_assoc1_3",TermC.num_str @{thm bdv_collect_assoc1_3}),
1.1039 + Celem.Thm ("bdv_collect_assoc1_1",TermC.num_str @{thm bdv_collect_assoc1_1}),
1.1040 + Celem.Thm ("bdv_collect_assoc1_2",TermC.num_str @{thm bdv_collect_assoc1_2}),
1.1041 + Celem.Thm ("bdv_collect_assoc1_3",TermC.num_str @{thm bdv_collect_assoc1_3}),
1.1042
1.1043 - Thm ("bdv_collect_assoc2_1",TermC.num_str @{thm bdv_collect_assoc2_1}),
1.1044 - Thm ("bdv_collect_assoc2_2",TermC.num_str @{thm bdv_collect_assoc2_2}),
1.1045 - Thm ("bdv_collect_assoc2_3",TermC.num_str @{thm bdv_collect_assoc2_3}),
1.1046 + Celem.Thm ("bdv_collect_assoc2_1",TermC.num_str @{thm bdv_collect_assoc2_1}),
1.1047 + Celem.Thm ("bdv_collect_assoc2_2",TermC.num_str @{thm bdv_collect_assoc2_2}),
1.1048 + Celem.Thm ("bdv_collect_assoc2_3",TermC.num_str @{thm bdv_collect_assoc2_3}),
1.1049
1.1050
1.1051 - Thm ("bdv_n_collect_1",TermC.num_str @{thm bdv_n_collect_1}),
1.1052 - Thm ("bdv_n_collect_2",TermC.num_str @{thm bdv_n_collect_2}),
1.1053 - Thm ("bdv_n_collect_3",TermC.num_str @{thm bdv_n_collect_3}),
1.1054 + Celem.Thm ("bdv_n_collect_1",TermC.num_str @{thm bdv_n_collect_1}),
1.1055 + Celem.Thm ("bdv_n_collect_2",TermC.num_str @{thm bdv_n_collect_2}),
1.1056 + Celem.Thm ("bdv_n_collect_3",TermC.num_str @{thm bdv_n_collect_3}),
1.1057
1.1058 - Thm ("bdv_n_collect_assoc1_1",TermC.num_str @{thm bdv_n_collect_assoc1_1}),
1.1059 - Thm ("bdv_n_collect_assoc1_2",TermC.num_str @{thm bdv_n_collect_assoc1_2}),
1.1060 - Thm ("bdv_n_collect_assoc1_3",TermC.num_str @{thm bdv_n_collect_assoc1_3}),
1.1061 + Celem.Thm ("bdv_n_collect_assoc1_1",TermC.num_str @{thm bdv_n_collect_assoc1_1}),
1.1062 + Celem.Thm ("bdv_n_collect_assoc1_2",TermC.num_str @{thm bdv_n_collect_assoc1_2}),
1.1063 + Celem.Thm ("bdv_n_collect_assoc1_3",TermC.num_str @{thm bdv_n_collect_assoc1_3}),
1.1064
1.1065 - Thm ("bdv_n_collect_assoc2_1",TermC.num_str @{thm bdv_n_collect_assoc2_1}),
1.1066 - Thm ("bdv_n_collect_assoc2_2",TermC.num_str @{thm bdv_n_collect_assoc2_2}),
1.1067 - Thm ("bdv_n_collect_assoc2_3",TermC.num_str @{thm bdv_n_collect_assoc2_3})
1.1068 - ], scr = EmptyScr}:rls);
1.1069 + Celem.Thm ("bdv_n_collect_assoc2_1",TermC.num_str @{thm bdv_n_collect_assoc2_1}),
1.1070 + Celem.Thm ("bdv_n_collect_assoc2_2",TermC.num_str @{thm bdv_n_collect_assoc2_2}),
1.1071 + Celem.Thm ("bdv_n_collect_assoc2_3",TermC.num_str @{thm bdv_n_collect_assoc2_3})
1.1072 + ], scr = Celem.EmptyScr});
1.1073
1.1074 *}
1.1075 ML{*
1.1076 (*.transforms an arbitrary term without roots to a polynomial [4]
1.1077 according to knowledge/Poly.sml.*)
1.1078 val make_polynomial_in = prep_rls'(
1.1079 - Seq {id = "make_polynomial_in", preconds = []:term list,
1.1080 - rew_ord = ("dummy_ord", dummy_ord),
1.1081 - erls = Atools_erls, srls = Erls,
1.1082 + Celem.Seq {id = "make_polynomial_in", preconds = []:term list,
1.1083 + rew_ord = ("dummy_ord", Celem.dummy_ord),
1.1084 + erls = Atools_erls, srls = Celem.Erls,
1.1085 calc = [], errpatts = [],
1.1086 - rules = [Rls_ expand_poly,
1.1087 - Rls_ order_add_mult_in,
1.1088 - Rls_ simplify_power,
1.1089 - Rls_ collect_numerals,
1.1090 - Rls_ reduce_012,
1.1091 - Thm ("realpow_oneI",TermC.num_str @{thm realpow_oneI}),
1.1092 - Rls_ discard_parentheses,
1.1093 - Rls_ collect_bdv
1.1094 + rules = [Celem.Rls_ expand_poly,
1.1095 + Celem.Rls_ order_add_mult_in,
1.1096 + Celem.Rls_ simplify_power,
1.1097 + Celem.Rls_ collect_numerals,
1.1098 + Celem.Rls_ reduce_012,
1.1099 + Celem.Thm ("realpow_oneI",TermC.num_str @{thm realpow_oneI}),
1.1100 + Celem.Rls_ discard_parentheses,
1.1101 + Celem.Rls_ collect_bdv
1.1102 ],
1.1103 - scr = EmptyScr
1.1104 - }:rls);
1.1105 + scr = Celem.EmptyScr
1.1106 + });
1.1107
1.1108 *}
1.1109 ML{*
1.1110 val separate_bdvs =
1.1111 - append_rls "separate_bdvs"
1.1112 + Celem.append_rls "separate_bdvs"
1.1113 collect_bdv
1.1114 - [Thm ("separate_bdv", TermC.num_str @{thm separate_bdv}),
1.1115 + [Celem.Thm ("separate_bdv", TermC.num_str @{thm separate_bdv}),
1.1116 (*"?a * ?bdv / ?b = ?a / ?b * ?bdv"*)
1.1117 - Thm ("separate_bdv_n", TermC.num_str @{thm separate_bdv_n}),
1.1118 - Thm ("separate_1_bdv", TermC.num_str @{thm separate_1_bdv}),
1.1119 + Celem.Thm ("separate_bdv_n", TermC.num_str @{thm separate_bdv_n}),
1.1120 + Celem.Thm ("separate_1_bdv", TermC.num_str @{thm separate_1_bdv}),
1.1121 (*"?bdv / ?b = (1 / ?b) * ?bdv"*)
1.1122 - Thm ("separate_1_bdv_n", TermC.num_str @{thm separate_1_bdv_n}),
1.1123 + Celem.Thm ("separate_1_bdv_n", TermC.num_str @{thm separate_1_bdv_n}),
1.1124 (*"?bdv ^^^ ?n / ?b = 1 / ?b * ?bdv ^^^ ?n"*)
1.1125 - Thm ("add_divide_distrib",
1.1126 + Celem.Thm ("add_divide_distrib",
1.1127 TermC.num_str @{thm add_divide_distrib})
1.1128 (*"(?x + ?y) / ?z = ?x / ?z + ?y / ?z"
1.1129 WN051031 DOES NOT BELONG TO HERE*)
1.1130 @@ -1321,19 +1321,19 @@
1.1131 *}
1.1132 ML{*
1.1133 val make_ratpoly_in = prep_rls'(
1.1134 - Seq {id = "make_ratpoly_in", preconds = []:term list,
1.1135 - rew_ord = ("dummy_ord", dummy_ord),
1.1136 - erls = Atools_erls, srls = Erls,
1.1137 + Celem.Seq {id = "make_ratpoly_in", preconds = []:term list,
1.1138 + rew_ord = ("dummy_ord", Celem.dummy_ord),
1.1139 + erls = Atools_erls, srls = Celem.Erls,
1.1140 calc = [], errpatts = [],
1.1141 - rules = [Rls_ norm_Rational,
1.1142 - Rls_ order_add_mult_in,
1.1143 - Rls_ discard_parentheses,
1.1144 - Rls_ separate_bdvs,
1.1145 - (* Rls_ rearrange_assoc, WN060916 why does cancel_p not work?*)
1.1146 - Rls_ cancel_p
1.1147 - (*Calc ("Rings.divide_class.divide" ,eval_cancel "#divide_e") too weak!*)
1.1148 + rules = [Celem.Rls_ norm_Rational,
1.1149 + Celem.Rls_ order_add_mult_in,
1.1150 + Celem.Rls_ discard_parentheses,
1.1151 + Celem.Rls_ separate_bdvs,
1.1152 + (* Celem.Rls_ rearrange_assoc, WN060916 why does cancel_p not work?*)
1.1153 + Celem.Rls_ cancel_p
1.1154 + (*Celem.Calc ("Rings.divide_class.divide" ,eval_cancel "#divide_e") too weak!*)
1.1155 ],
1.1156 - scr = EmptyScr}:rls);
1.1157 + scr = Celem.EmptyScr});
1.1158 *}
1.1159 setup {* KEStore_Elems.add_rlss
1.1160 [("order_add_mult_in", (Context.theory_name @{theory}, order_add_mult_in)),