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