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