1.1 --- a/src/Tools/isac/Knowledge/PolyEq.thy Wed Sep 08 12:41:04 2010 +0200
1.2 +++ b/src/Tools/isac/Knowledge/PolyEq.thy Wed Sep 08 16:28:24 2010 +0200
1.3 @@ -318,7 +318,7 @@
1.4
1.5 (* ---- degree 4 ----*)
1.6 (* RL03.FIXME es wir nicht getestet ob u>0 *)
1.7 - d4_sub_u1
1.8 + d4_sub_u1:
1.9 "(c+b*bdv^^^2+a*bdv^^^4=0) =
1.10 ((a*u^^^2+b*u+c=0) & (bdv^^^2=u))"
1.11
1.12 @@ -414,24 +414,23 @@
1.13 Rls {id = "cancel_leading_coeff", preconds = [],
1.14 rew_ord = ("e_rew_ord",e_rew_ord),
1.15 erls = PolyEq_erls, srls = Erls, calc = [], (*asm_thm = [],*)
1.16 - rules = [Thm ("cancel_leading_coeff1",num_str @{thm cancel_leading_coeff1}),
1.17 - Thm ("cancel_leading_coeff2",num_str @{thm cancel_leading_coeff2}),
1.18 - Thm ("cancel_leading_coeff3",num_str @{thm cancel_leading_coeff3}),
1.19 - Thm ("cancel_leading_coeff4",num_str @{thm cancel_leading_coeff4}),
1.20 - Thm ("cancel_leading_coeff5",num_str @{thm cancel_leading_coeff5}),
1.21 - Thm ("cancel_leading_coeff6",num_str @{thm cancel_leading_coeff6}),
1.22 - Thm ("cancel_leading_coeff7",num_str @{thm cancel_leading_coeff7}),
1.23 - Thm ("cancel_leading_coeff8",num_str @{thm cancel_leading_coeff8}),
1.24 - Thm ("cancel_leading_coeff9",num_str @{thm cancel_leading_coeff9}),
1.25 - Thm ("cancel_leading_coeff10",num_str @{thm cancel_leading_coeff10}),
1.26 - Thm ("cancel_leading_coeff11",num_str @{thm cancel_leading_coeff11}),
1.27 - Thm ("cancel_leading_coeff12",num_str @{thm cancel_leading_coeff12}),
1.28 - Thm ("cancel_leading_coeff13",num_str @{thm cancel_leading_coeff13})
1.29 - ],
1.30 - scr = Script ((term_of o the o (parse thy))
1.31 - "empty_script")
1.32 - }:rls);
1.33 -
1.34 + rules =
1.35 + [Thm ("cancel_leading_coeff1",num_str @{thm cancel_leading_coeff1}),
1.36 + Thm ("cancel_leading_coeff2",num_str @{thm cancel_leading_coeff2}),
1.37 + Thm ("cancel_leading_coeff3",num_str @{thm cancel_leading_coeff3}),
1.38 + Thm ("cancel_leading_coeff4",num_str @{thm cancel_leading_coeff4}),
1.39 + Thm ("cancel_leading_coeff5",num_str @{thm cancel_leading_coeff5}),
1.40 + Thm ("cancel_leading_coeff6",num_str @{thm cancel_leading_coeff6}),
1.41 + Thm ("cancel_leading_coeff7",num_str @{thm cancel_leading_coeff7}),
1.42 + Thm ("cancel_leading_coeff8",num_str @{thm cancel_leading_coeff8}),
1.43 + Thm ("cancel_leading_coeff9",num_str @{thm cancel_leading_coeff9}),
1.44 + Thm ("cancel_leading_coeff10",num_str @{thm cancel_leading_coeff10}),
1.45 + Thm ("cancel_leading_coeff11",num_str @{thm cancel_leading_coeff11}),
1.46 + Thm ("cancel_leading_coeff12",num_str @{thm cancel_leading_coeff12}),
1.47 + Thm ("cancel_leading_coeff13",num_str @{thm cancel_leading_coeff13})
1.48 + ],scr = Script ((term_of o the o (parse thy)) "empty_script")}:rls);
1.49 +*}
1.50 +ML{*
1.51 val complete_square = prep_rls(
1.52 Rls {id = "complete_square", preconds = [],
1.53 rew_ord = ("e_rew_ord",e_rew_ord),
1.54 @@ -475,6 +474,8 @@
1.55 ("PolyEq_erls",PolyEq_erls),(*FIXXXME:del with rls.rls'*)
1.56 ("polyeq_simplify",polyeq_simplify)]);
1.57
1.58 +*}
1.59 +ML{*
1.60
1.61 (* ------------- polySolve ------------------ *)
1.62 (* -- d0 -- *)
1.63 @@ -512,6 +513,8 @@
1.64 scr = Script ((term_of o the o (parse thy)) "empty_script")
1.65 }:rls);
1.66
1.67 +*}
1.68 +ML{*
1.69 (* -- d2 -- *)
1.70 (* isolate the bound variable in an d2 equation with bdv only;
1.71 'bdv' is a meta-constant*)
1.72 @@ -546,7 +549,8 @@
1.73 ],
1.74 scr = Script ((term_of o the o (parse thy)) "empty_script")
1.75 }:rls);
1.76 -
1.77 +*}
1.78 +ML{*
1.79 (* isolate the bound variable in an d2 equation with sqrt only;
1.80 'bdv' is a meta-constant*)
1.81 val d2_polyeq_sq_only_simplify = prep_rls(
1.82 @@ -572,7 +576,8 @@
1.83 ],
1.84 scr = Script ((term_of o the o (parse thy)) "empty_script")
1.85 }:rls);
1.86 -
1.87 +*}
1.88 +ML{*
1.89 (* isolate the bound variable in an d2 equation with pqFormula;
1.90 'bdv' is a meta-constant*)
1.91 val d2_polyeq_pqFormula_simplify = prep_rls(
1.92 @@ -615,10 +620,10 @@
1.93 (* x^2=0 *)
1.94 Thm("d2_sqrt_equation3",num_str @{thm d2_sqrt_equation3})
1.95 (* 1x^2=0 *)
1.96 - ],
1.97 - scr = Script ((term_of o the o (parse thy)) "empty_script")
1.98 + ],scr = Script ((term_of o the o (parse thy)) "empty_script")
1.99 }:rls);
1.100 -
1.101 +*}
1.102 +ML{*
1.103 (* isolate the bound variable in an d2 equation with abcFormula;
1.104 'bdv' is a meta-constant*)
1.105 val d2_polyeq_abcFormula_simplify = prep_rls(
1.106 @@ -664,6 +669,8 @@
1.107 ],
1.108 scr = Script ((term_of o the o (parse thy)) "empty_script")
1.109 }:rls);
1.110 +*}
1.111 +ML{*
1.112
1.113 (* isolate the bound variable in an d2 equation;
1.114 'bdv' is a meta-constant*)
1.115 @@ -722,6 +729,8 @@
1.116 ],
1.117 scr = Script ((term_of o the o (parse thy)) "empty_script")
1.118 }:rls);
1.119 +*}
1.120 +ML{*
1.121
1.122 (* -- d3 -- *)
1.123 (* isolate the bound variable in an d3 equation; 'bdv' is a meta-constant *)
1.124 @@ -793,6 +802,8 @@
1.125 ],
1.126 scr = Script ((term_of o the o (parse thy)) "empty_script")
1.127 }:rls);
1.128 +*}
1.129 +ML{*
1.130
1.131 (* -- d4 -- *)
1.132 (*isolate the bound variable in an d4 equation; 'bdv' is a meta-constant*)
1.133 @@ -801,7 +812,7 @@
1.134 rew_ord = ("e_rew_ord",e_rew_ord), erls = PolyEq_erls,
1.135 srls = Erls, calc = [],
1.136 rules =
1.137 - [Thm("d4_sub_u1",num_str @{thm d4_sub_u1)
1.138 + [Thm("d4_sub_u1",num_str @{thm d4_sub_u1})
1.139 (* ax^4+bx^2+c=0 -> x=+-sqrt(ax^2+bx^+c) *)
1.140 ],
1.141 scr = Script ((term_of o the o (parse thy)) "empty_script")
1.142 @@ -821,6 +832,8 @@
1.143 ("d3_polyeq_simplify", d3_polyeq_simplify),
1.144 ("d4_polyeq_simplify", d4_polyeq_simplify)
1.145 ]);
1.146 +*}
1.147 +ML{*
1.148
1.149 (*------------------------problems------------------------*)
1.150 (*
1.151 @@ -867,7 +880,8 @@
1.152 ],
1.153 PolyEq_prls, SOME "solve (e_e::bool, v_v)",
1.154 [["PolyEq","solve_d1_polyeq_equation"]]));
1.155 -
1.156 +*}
1.157 +ML{*
1.158 (*--- d2 ---*)
1.159 store_pbt
1.160 (prep_pbt thy "pbl_equ_univ_poly_deg2" [] e_pblID
1.161 @@ -938,7 +952,8 @@
1.162 ],
1.163 PolyEq_prls, SOME "solve (e_e::bool, v_v)",
1.164 [["PolyEq","solve_d2_polyeq_abc_equation"]]));
1.165 -
1.166 +*}
1.167 +ML{*
1.168 (*--- d3 ---*)
1.169 store_pbt
1.170 (prep_pbt thy "pbl_equ_univ_poly_deg3" [] e_pblID
1.171 @@ -999,7 +1014,21 @@
1.172 PolyEq_prls, SOME "solve (e_e::bool, v_v)",
1.173 [["PolyEq","complete_square"]]));
1.174
1.175 -
1.176 +*}
1.177 +ML{*
1.178 +val scr =
1.179 + "Script Normalize_poly (e_e::bool) (v_v::real) = " ^
1.180 + "(let e_e =((Try (Rewrite all_left False)) @@ " ^
1.181 + " (Try (Repeat (Rewrite makex1_x False))) @@ " ^
1.182 + " (Try (Repeat (Rewrite_Set expand_binoms False))) @@ " ^
1.183 + " (Try (Repeat (Rewrite_Set_Inst [(bdv,v_v::real)] " ^
1.184 + " make_ratpoly_in False))) @@ " ^
1.185 + " (Try (Repeat (Rewrite_Set polyeq_simplify False)))) e_e " ^
1.186 + " in (SubProblem (PolyEq',[polynomial,univariate,equation], [no_met]) " ^
1.187 + " [BOOL e_e, REAL v_v]))";
1.188 +parse thy scr;
1.189 +*}
1.190 +ML{*
1.191 "-------------------------methods-----------------------";
1.192 store_met
1.193 (prep_met thy "met_polyeq" [] e_metID
1.194 @@ -1021,18 +1050,20 @@
1.195 srls=e_rls,
1.196 prls=PolyEq_prls,
1.197 calc=[],
1.198 - crls=PolyEq_crls, nrls=norm_Rational
1.199 + crls=PolyEq_crls, nrls=norm_Rational},
1.200 "Script Normalize_poly (e_e::bool) (v_v::real) = " ^
1.201 "(let e_e =((Try (Rewrite all_left False)) @@ " ^
1.202 " (Try (Repeat (Rewrite makex1_x False))) @@ " ^
1.203 " (Try (Repeat (Rewrite_Set expand_binoms False))) @@ " ^
1.204 - " (Try (Repeat (Rewrite_Set_Inst [(bdv,v_::real)] " ^
1.205 + " (Try (Repeat (Rewrite_Set_Inst [(bdv,v_v::real)] " ^
1.206 " make_ratpoly_in False))) @@ " ^
1.207 " (Try (Repeat (Rewrite_Set polyeq_simplify False)))) e_e " ^
1.208 - " in (SubProblem (PolyEq_,[polynomial,univariate,equation], " ^
1.209 - " [no_met]) [BOOL e_e, REAL v_]))"
1.210 + " in (SubProblem (PolyEq',[polynomial,univariate,equation], [no_met]) " ^
1.211 + " [BOOL e_e, REAL v_v]))"
1.212 ));
1.213
1.214 +*}
1.215 +ML{*
1.216 store_met
1.217 (prep_met thy "met_polyeq_d0" [] e_metID
1.218 (["PolyEq","solve_d0_polyeq_equation"],
1.219 @@ -1048,11 +1079,12 @@
1.220 calc=[("sqrt", ("NthRoot.sqrt", eval_sqrt "#sqrt_"))],
1.221 crls=PolyEq_crls, nrls=norm_Rational},
1.222 "Script Solve_d0_polyeq_equation (e_e::bool) (v_v::real) = " ^
1.223 - "(let e_e = ((Try (Rewrite_Set_Inst [(bdv,v_::real)] " ^
1.224 + "(let e_e = ((Try (Rewrite_Set_Inst [(bdv,v_v::real)] " ^
1.225 " d0_polyeq_simplify False))) e_e " ^
1.226 " in ((Or_to_List e_e)::bool list))"
1.227 ));
1.228 -
1.229 +*}
1.230 +ML{*
1.231 store_met
1.232 (prep_met thy "met_polyeq_d1" [] e_metID
1.233 (["PolyEq","solve_d1_polyeq_equation"],
1.234 @@ -1061,24 +1093,19 @@
1.235 "((lhs e_e) has_degree_in v_v) = 1"]),
1.236 ("#Find" ,["solutions v_i"])
1.237 ],
1.238 - {rew_ord'="termlessI",
1.239 - rls'=PolyEq_erls,
1.240 - srls=e_rls,
1.241 - prls=PolyEq_prls,
1.242 + {rew_ord'="termlessI", rls'=PolyEq_erls, srls=e_rls, prls=PolyEq_prls,
1.243 calc=[("sqrt", ("NthRoot.sqrt", eval_sqrt "#sqrt_"))],
1.244 - crls=PolyEq_crls, nrls=norm_Rational(*,
1.245 - (* asm_rls=["d1_polyeq_simplify"],*)
1.246 - asm_rls=[],
1.247 - asm_thm=[("d1_isolate_div","")]*)},
1.248 + crls=PolyEq_crls, nrls=norm_Rational},
1.249 "Script Solve_d1_polyeq_equation (e_e::bool) (v_v::real) = " ^
1.250 - "(let e_e = ((Try (Rewrite_Set_Inst [(bdv,v_::real)] " ^
1.251 + "(let e_e = ((Try (Rewrite_Set_Inst [(bdv,v_v::real)] " ^
1.252 " d1_polyeq_simplify True)) @@ " ^
1.253 " (Try (Rewrite_Set polyeq_simplify False)) @@ " ^
1.254 - " (Try (Rewrite_Set norm_Rational_parenthesized False))) e_;" ^
1.255 - " (L_::bool list) = ((Or_to_List e_e)::bool list) " ^
1.256 - " in Check_elementwise L_ {(v_v::real). Assumptions} )"
1.257 + " (Try (Rewrite_Set norm_Rational_parenthesized False))) e_e;" ^
1.258 + " (L_L::bool list) = ((Or_to_List e_e)::bool list) " ^
1.259 + " in Check_elementwise L_L {(v_v::real). Assumptions} )"
1.260 ));
1.261 -
1.262 +*}
1.263 +ML{*
1.264 store_met
1.265 (prep_met thy "met_polyeq_d22" [] e_metID
1.266 (["PolyEq","solve_d2_polyeq_equation"],
1.267 @@ -1094,17 +1121,18 @@
1.268 calc=[("sqrt", ("NthRoot.sqrt", eval_sqrt "#sqrt_"))],
1.269 crls=PolyEq_crls, nrls=norm_Rational},
1.270 "Script Solve_d2_polyeq_equation (e_e::bool) (v_v::real) = " ^
1.271 - " (let e_e = ((Try (Rewrite_Set_Inst [(bdv,v_::real)] " ^
1.272 + " (let e_e = ((Try (Rewrite_Set_Inst [(bdv,v_v::real)] " ^
1.273 " d2_polyeq_simplify True)) @@ " ^
1.274 " (Try (Rewrite_Set polyeq_simplify False)) @@ " ^
1.275 - " (Try (Rewrite_Set_Inst [(bdv,v_::real)] " ^
1.276 + " (Try (Rewrite_Set_Inst [(bdv,v_v::real)] " ^
1.277 " d1_polyeq_simplify True)) @@ " ^
1.278 " (Try (Rewrite_Set polyeq_simplify False)) @@ " ^
1.279 - " (Try (Rewrite_Set norm_Rational_parenthesized False))) e_;" ^
1.280 - " (L_::bool list) = ((Or_to_List e_e)::bool list) " ^
1.281 - " in Check_elementwise L_ {(v_v::real). Assumptions} )"
1.282 + " (Try (Rewrite_Set norm_Rational_parenthesized False))) e_e;" ^
1.283 + " (L_L::bool list) = ((Or_to_List e_e)::bool list) " ^
1.284 + " in Check_elementwise L_L {(v_v::real). Assumptions} )"
1.285 ));
1.286 -
1.287 +*}
1.288 +ML{*
1.289 store_met
1.290 (prep_met thy "met_polyeq_d2_bdvonly" [] e_metID
1.291 (["PolyEq","solve_d2_polyeq_bdvonly_equation"],
1.292 @@ -1120,17 +1148,18 @@
1.293 calc=[("sqrt", ("NthRoot.sqrt", eval_sqrt "#sqrt_"))],
1.294 crls=PolyEq_crls, nrls=norm_Rational},
1.295 "Script Solve_d2_polyeq_bdvonly_equation (e_e::bool) (v_v::real) =" ^
1.296 - " (let e_e = ((Try (Rewrite_Set_Inst [(bdv,v_::real)] " ^
1.297 + " (let e_e = ((Try (Rewrite_Set_Inst [(bdv,v_v::real)] " ^
1.298 " d2_polyeq_bdv_only_simplify True)) @@ " ^
1.299 " (Try (Rewrite_Set polyeq_simplify False)) @@ " ^
1.300 - " (Try (Rewrite_Set_Inst [(bdv,v_::real)] " ^
1.301 + " (Try (Rewrite_Set_Inst [(bdv,v_v::real)] " ^
1.302 " d1_polyeq_simplify True)) @@ " ^
1.303 " (Try (Rewrite_Set polyeq_simplify False)) @@ " ^
1.304 - " (Try (Rewrite_Set norm_Rational_parenthesized False))) e_;" ^
1.305 - " (L_::bool list) = ((Or_to_List e_e)::bool list) " ^
1.306 - " in Check_elementwise L_ {(v_v::real). Assumptions} )"
1.307 + " (Try (Rewrite_Set norm_Rational_parenthesized False))) e_e;" ^
1.308 + " (L_L::bool list) = ((Or_to_List e_e)::bool list) " ^
1.309 + " in Check_elementwise L_L {(v_v::real). Assumptions} )"
1.310 ));
1.311 -
1.312 +*}
1.313 +ML{*
1.314 store_met
1.315 (prep_met thy "met_polyeq_d2_sqonly" [] e_metID
1.316 (["PolyEq","solve_d2_polyeq_sqonly_equation"],
1.317 @@ -1146,14 +1175,15 @@
1.318 calc=[("sqrt", ("NthRoot.sqrt", eval_sqrt "#sqrt_"))],
1.319 crls=PolyEq_crls, nrls=norm_Rational},
1.320 "Script Solve_d2_polyeq_sqonly_equation (e_e::bool) (v_v::real) =" ^
1.321 - " (let e_e = ((Try (Rewrite_Set_Inst [(bdv,v_::real)] " ^
1.322 + " (let e_e = ((Try (Rewrite_Set_Inst [(bdv,v_v::real)] " ^
1.323 " d2_polyeq_sq_only_simplify True)) @@ " ^
1.324 " (Try (Rewrite_Set polyeq_simplify False)) @@ " ^
1.325 - " (Try (Rewrite_Set norm_Rational_parenthesized False))) e_; " ^
1.326 - " (L_::bool list) = ((Or_to_List e_e)::bool list) " ^
1.327 - " in Check_elementwise L_ {(v_v::real). Assumptions} )"
1.328 + " (Try (Rewrite_Set norm_Rational_parenthesized False))) e_e; " ^
1.329 + " (L_L::bool list) = ((Or_to_List e_e)::bool list) " ^
1.330 + " in Check_elementwise L_L {(v_v::real). Assumptions} )"
1.331 ));
1.332 -
1.333 +*}
1.334 +ML{*
1.335 store_met
1.336 (prep_met thy "met_polyeq_d2_pq" [] e_metID
1.337 (["PolyEq","solve_d2_polyeq_pq_equation"],
1.338 @@ -1169,14 +1199,15 @@
1.339 calc=[("sqrt", ("NthRoot.sqrt", eval_sqrt "#sqrt_"))],
1.340 crls=PolyEq_crls, nrls=norm_Rational},
1.341 "Script Solve_d2_polyeq_pq_equation (e_e::bool) (v_v::real) = " ^
1.342 - " (let e_e = ((Try (Rewrite_Set_Inst [(bdv,v_::real)] " ^
1.343 + " (let e_e = ((Try (Rewrite_Set_Inst [(bdv,v_v::real)] " ^
1.344 " d2_polyeq_pqFormula_simplify True)) @@ " ^
1.345 " (Try (Rewrite_Set polyeq_simplify False)) @@ " ^
1.346 - " (Try (Rewrite_Set norm_Rational_parenthesized False))) e_;" ^
1.347 - " (L_::bool list) = ((Or_to_List e_e)::bool list) " ^
1.348 - " in Check_elementwise L_ {(v_v::real). Assumptions} )"
1.349 + " (Try (Rewrite_Set norm_Rational_parenthesized False))) e_e;" ^
1.350 + " (L_L::bool list) = ((Or_to_List e_e)::bool list) " ^
1.351 + " in Check_elementwise L_L {(v_v::real). Assumptions} )"
1.352 ));
1.353 -
1.354 +*}
1.355 +ML{*
1.356 store_met
1.357 (prep_met thy "met_polyeq_d2_abc" [] e_metID
1.358 (["PolyEq","solve_d2_polyeq_abc_equation"],
1.359 @@ -1192,14 +1223,15 @@
1.360 calc=[("sqrt", ("NthRoot.sqrt", eval_sqrt "#sqrt_"))],
1.361 crls=PolyEq_crls, nrls=norm_Rational},
1.362 "Script Solve_d2_polyeq_abc_equation (e_e::bool) (v_v::real) = " ^
1.363 - " (let e_e = ((Try (Rewrite_Set_Inst [(bdv,v_::real)] " ^
1.364 + " (let e_e = ((Try (Rewrite_Set_Inst [(bdv,v_v::real)] " ^
1.365 " d2_polyeq_abcFormula_simplify True)) @@ " ^
1.366 " (Try (Rewrite_Set polyeq_simplify False)) @@ " ^
1.367 - " (Try (Rewrite_Set norm_Rational_parenthesized False))) e_;" ^
1.368 - " (L_::bool list) = ((Or_to_List e_e)::bool list) " ^
1.369 - " in Check_elementwise L_ {(v_v::real). Assumptions} )"
1.370 + " (Try (Rewrite_Set norm_Rational_parenthesized False))) e_e;" ^
1.371 + " (L_L::bool list) = ((Or_to_List e_e)::bool list) " ^
1.372 + " in Check_elementwise L_L {(v_v::real). Assumptions} )"
1.373 ));
1.374 -
1.375 +*}
1.376 +ML{*
1.377 store_met
1.378 (prep_met thy "met_polyeq_d3" [] e_metID
1.379 (["PolyEq","solve_d3_polyeq_equation"],
1.380 @@ -1215,20 +1247,21 @@
1.381 calc=[("sqrt", ("NthRoot.sqrt", eval_sqrt "#sqrt_"))],
1.382 crls=PolyEq_crls, nrls=norm_Rational},
1.383 "Script Solve_d3_polyeq_equation (e_e::bool) (v_v::real) = " ^
1.384 - " (let e_e = ((Try (Rewrite_Set_Inst [(bdv,v_::real)] " ^
1.385 + " (let e_e = ((Try (Rewrite_Set_Inst [(bdv,v_v::real)] " ^
1.386 " d3_polyeq_simplify True)) @@ " ^
1.387 " (Try (Rewrite_Set polyeq_simplify False)) @@ " ^
1.388 - " (Try (Rewrite_Set_Inst [(bdv,v_::real)] " ^
1.389 + " (Try (Rewrite_Set_Inst [(bdv,v_v::real)] " ^
1.390 " d2_polyeq_simplify True)) @@ " ^
1.391 " (Try (Rewrite_Set polyeq_simplify False)) @@ " ^
1.392 - " (Try (Rewrite_Set_Inst [(bdv,v_::real)] " ^
1.393 + " (Try (Rewrite_Set_Inst [(bdv,v_v::real)] " ^
1.394 " d1_polyeq_simplify True)) @@ " ^
1.395 " (Try (Rewrite_Set polyeq_simplify False)) @@ " ^
1.396 - " (Try (Rewrite_Set norm_Rational_parenthesized False))) e_;" ^
1.397 - " (L_::bool list) = ((Or_to_List e_e)::bool list) " ^
1.398 - " in Check_elementwise L_ {(v_v::real). Assumptions} )"
1.399 + " (Try (Rewrite_Set norm_Rational_parenthesized False))) e_e;" ^
1.400 + " (L_L::bool list) = ((Or_to_List e_e)::bool list) " ^
1.401 + " in Check_elementwise L_L {(v_v::real). Assumptions} )"
1.402 ));
1.403 -
1.404 +*}
1.405 +ML{*
1.406 (*.solves all expanded (ie. normalized) terms of degree 2.*)
1.407 (*Oct.02 restriction: 'eval_true 0 =< discriminant' ony for integer values
1.408 by 'PolyEq_erls'; restricted until Float.thy is implemented*)
1.409 @@ -1243,21 +1276,23 @@
1.410 {rew_ord'="termlessI",rls'=PolyEq_erls,srls=e_rls,prls=PolyEq_prls,
1.411 calc=[("sqrt", ("NthRoot.sqrt", eval_sqrt "#sqrt_"))],
1.412 crls=PolyEq_crls, nrls=norm_Rational},
1.413 - "Script Complete_square (e_e::bool) (v_v::real) = " ^
1.414 - "(let e_e = ((Try (Rewrite_Set_Inst [(bdv,v_)] cancel_leading_coeff True))" ^
1.415 - " @@ (Try (Rewrite_Set_Inst [(bdv,v_)] complete_square True)) " ^
1.416 + "Script Complete_square (e_e::bool) (v_v::real) = " ^
1.417 + "(let e_e = " ^
1.418 + " ((Try (Rewrite_Set_Inst [(bdv,v_v)] cancel_leading_coeff True)) " ^
1.419 + " @@ (Try (Rewrite_Set_Inst [(bdv,v_v)] complete_square True)) " ^
1.420 " @@ (Try (Rewrite square_explicit1 False)) " ^
1.421 " @@ (Try (Rewrite square_explicit2 False)) " ^
1.422 " @@ (Rewrite root_plus_minus True) " ^
1.423 - " @@ (Try (Repeat (Rewrite_Inst [(bdv,v_)] bdv_explicit1 False))) " ^
1.424 - " @@ (Try (Repeat (Rewrite_Inst [(bdv,v_)] bdv_explicit2 False))) " ^
1.425 + " @@ (Try (Repeat (Rewrite_Inst [(bdv,v_v)] bdv_explicit1 False))) " ^
1.426 + " @@ (Try (Repeat (Rewrite_Inst [(bdv,v_v)] bdv_explicit2 False))) " ^
1.427 " @@ (Try (Repeat " ^
1.428 - " (Rewrite_Inst [(bdv,v_)] bdv_explicit3 False))) " ^
1.429 + " (Rewrite_Inst [(bdv,v_v)] bdv_explicit3 False))) " ^
1.430 " @@ (Try (Rewrite_Set calculate_RootRat False)) " ^
1.431 " @@ (Try (Repeat (Calculate SQRT)))) e_e " ^
1.432 " in ((Or_to_List e_e)::bool list))"
1.433 ));
1.434 -
1.435 +*}
1.436 +ML{*
1.437
1.438 (* termorder hacked by MG *)
1.439 local (*. for make_polynomial_in .*)
1.440 @@ -1292,24 +1327,24 @@
1.441 | size_of_term' x _ = 1;
1.442
1.443
1.444 -fun Term_Ord.term_ord' x pr thy (Abs (_, T, t), Abs(_, U, u)) = (* ~ term.ML *)
1.445 - (case Term_Ord.term_ord' x pr thy (t, u) of EQUAL => Term_Ord.typ_ord (T, U) | ord => ord)
1.446 - | Term_Ord.term_ord' x pr thy (t, u) =
1.447 +fun term_ord' x pr thy (Abs (_, T, t), Abs(_, U, u)) = (* ~ term.ML *)
1.448 + (case term_ord' x pr thy (t, u) of EQUAL => Term_Ord.typ_ord (T, U) | ord => ord)
1.449 + | term_ord' x pr thy (t, u) =
1.450 (if pr then
1.451 let
1.452 val (f, ts) = strip_comb t and (g, us) = strip_comb u;
1.453 val _=writeln("t= f@ts= \""^
1.454 ((Syntax.string_of_term (thy2ctxt thy)) f)^"\" @ \"["^
1.455 - (commas(map(string_of_cterm o cterm_of(sign_of thy)) ts))^"]\"");
1.456 + (commas(map (Syntax.string_of_term (thy2ctxt thy)) ts))^"]\"");
1.457 val _=writeln("u= g@us= \""^
1.458 ((Syntax.string_of_term (thy2ctxt thy)) g)^"\" @ \"["^
1.459 - (commas(map(string_of_cterm o cterm_of(sign_of thy)) us))^"]\"");
1.460 + (commas(map (Syntax.string_of_term (thy2ctxt thy)) us))^"]\"");
1.461 val _=writeln("size_of_term(t,u)= ("^
1.462 (string_of_int(size_of_term' x t))^", "^
1.463 (string_of_int(size_of_term' x u))^")");
1.464 val _=writeln("hd_ord(f,g) = "^((pr_ord o (hd_ord x))(f,g)));
1.465 val _=writeln("terms_ord(ts,us) = "^
1.466 - ((pr_ord o (terms_ord x) str false)(ts,us)));
1.467 + ((pr_ord o (terms_ord x) str false)(ts, us)));
1.468 val _=writeln("-------");
1.469 in () end
1.470 else ();
1.471 @@ -1321,10 +1356,10 @@
1.472 end
1.473 | ord => ord)
1.474 and hd_ord x (f, g) = (* ~ term.ML *)
1.475 - prod_ord (prod_ord indexname_ord Term_Ord.typ_ord) int_ord (dest_hd' x f,
1.476 - dest_hd' x g)
1.477 + prod_ord (prod_ord Term_Ord.indexname_ord Term_Ord.typ_ord)
1.478 + int_ord (dest_hd' x f, dest_hd' x g)
1.479 and terms_ord x str pr (ts, us) =
1.480 - list_ord (term_ord' x pr (assoc_thy "Isac.thy"))(ts, us);
1.481 + list_ord (term_ord' x pr (assoc_thy "Isac"))(ts, us);
1.482 in
1.483
1.484 fun ord_make_polynomial_in (pr:bool) thy subst tu =
1.485 @@ -1336,12 +1371,14 @@
1.486 | _ => raise error ("ord_make_polynomial_in called with subst = "^
1.487 (subst2str subst))
1.488 end;
1.489 -end;
1.490 +end;(*local*)
1.491
1.492 +*}
1.493 +ML{*
1.494 val order_add_mult_in = prep_rls(
1.495 Rls{id = "order_add_mult_in", preconds = [],
1.496 rew_ord = ("ord_make_polynomial_in",
1.497 - ord_make_polynomial_in false Poly.thy),
1.498 + ord_make_polynomial_in false (theory "Poly")),
1.499 erls = e_rls,srls = Erls,
1.500 calc = [],
1.501 (*asm_thm = [],*)
1.502 @@ -1359,6 +1396,8 @@
1.503 (*z1.0 + z2.0 + z3.0 = z1.0 + (z2.0 + z3.0)*)
1.504 ], scr = EmptyScr}:rls);
1.505
1.506 +*}
1.507 +ML{*
1.508 val collect_bdv = prep_rls(
1.509 Rls{id = "collect_bdv", preconds = [],
1.510 rew_ord = ("dummy_ord", dummy_ord),
1.511 @@ -1388,9 +1427,11 @@
1.512
1.513 Thm ("bdv_n_collect_assoc2_1",num_str @{thm bdv_n_collect_assoc2_1}),
1.514 Thm ("bdv_n_collect_assoc2_2",num_str @{thm bdv_n_collect_assoc2_2}),
1.515 - Thm ("bdv_n_collect_assoc2_3",num_str @{thm bdv_n_collect_assoc2_3)
1.516 + Thm ("bdv_n_collect_assoc2_3",num_str @{thm bdv_n_collect_assoc2_3})
1.517 ], scr = EmptyScr}:rls);
1.518
1.519 +*}
1.520 +ML{*
1.521 (*.transforms an arbitrary term without roots to a polynomial [4]
1.522 according to knowledge/Poly.sml.*)
1.523 val make_polynomial_in = prep_rls(
1.524 @@ -1410,21 +1451,25 @@
1.525 scr = EmptyScr
1.526 }:rls);
1.527
1.528 +*}
1.529 +ML{*
1.530 val separate_bdvs =
1.531 append_rls "separate_bdvs"
1.532 collect_bdv
1.533 - [Thm ("separate_bdv", num_str @{separate_bdv}),
1.534 + [Thm ("separate_bdv", num_str @{thm separate_bdv}),
1.535 (*"?a * ?bdv / ?b = ?a / ?b * ?bdv"*)
1.536 - Thm ("separate_bdv_n", num_str @{separate_bdv_n}),
1.537 - Thm ("separate_1_bdv", num_str @{separate_1_bdv}),
1.538 + Thm ("separate_bdv_n", num_str @{thm separate_bdv_n}),
1.539 + Thm ("separate_1_bdv", num_str @{thm separate_1_bdv}),
1.540 (*"?bdv / ?b = (1 / ?b) * ?bdv"*)
1.541 - Thm ("separate_1_bdv_n", num_str @{separate_1_bdv_n}),
1.542 + Thm ("separate_1_bdv_n", num_str @{thm separate_1_bdv_n}),
1.543 (*"?bdv ^^^ ?n / ?b = 1 / ?b * ?bdv ^^^ ?n"*)
1.544 Thm ("nadd_divide_distrib",
1.545 - num_str @{thm nadd_divide_distrib})
1.546 + num_str @{thm add_divide_distrib})
1.547 (*"(?x + ?y) / ?z = ?x / ?z + ?y / ?z"
1.548 WN051031 DOES NOT BELONG TO HERE*)
1.549 ];
1.550 +*}
1.551 +ML{*
1.552 val make_ratpoly_in = prep_rls(
1.553 Seq {id = "make_ratpoly_in", preconds = []:term list,
1.554 rew_ord = ("dummy_ord", dummy_ord),