1.1 --- a/src/Tools/isac/IsacKnowledge/PolyEq.ML Wed Aug 25 15:15:01 2010 +0200
1.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
1.3 @@ -1,1162 +0,0 @@
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"IsacKnowledge/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"IsacKnowledge/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 -