1.1 --- a/src/Tools/isac/Build_Isac.thy Wed Sep 08 12:41:04 2010 +0200
1.2 +++ b/src/Tools/isac/Build_Isac.thy Wed Sep 08 16:28:24 2010 +0200
1.3 @@ -70,10 +70,11 @@
1.4 use_thy "Knowledge/LinEq"
1.5 use_thy "Knowledge/Root"
1.6 use_thy "Knowledge/RootEq"
1.7 +use_thy "Knowledge/RatEq"
1.8 +use_thy "Knowledge/RootRat"
1.9 +use_thy "Knowledge/RootRatEq"
1.10
1.11 -
1.12 -use_thy "Knowledge/RatEq"
1.13 -
1.14 +use_thy "Knowledge/PolyEq"
1.15
1.16 ML {*
1.17 *}
1.18 @@ -81,9 +82,6 @@
1.19
1.20 text {*------------------------------------------*}
1.21 (*
1.22 -use_thy "Knowledge/RootRat"
1.23 -use_thy "Knowledge/RootRatEq"
1.24 -use_thy "Knowledge/PolyEq"
1.25 use_thy "Knowledge/Vect"
1.26 use_thy "Knowledge/Calculus"
1.27 use_thy "Knowledge/Trig"
2.1 --- a/src/Tools/isac/Knowledge/PolyEq.thy Wed Sep 08 12:41:04 2010 +0200
2.2 +++ b/src/Tools/isac/Knowledge/PolyEq.thy Wed Sep 08 16:28:24 2010 +0200
2.3 @@ -318,7 +318,7 @@
2.4
2.5 (* ---- degree 4 ----*)
2.6 (* RL03.FIXME es wir nicht getestet ob u>0 *)
2.7 - d4_sub_u1
2.8 + d4_sub_u1:
2.9 "(c+b*bdv^^^2+a*bdv^^^4=0) =
2.10 ((a*u^^^2+b*u+c=0) & (bdv^^^2=u))"
2.11
2.12 @@ -414,24 +414,23 @@
2.13 Rls {id = "cancel_leading_coeff", preconds = [],
2.14 rew_ord = ("e_rew_ord",e_rew_ord),
2.15 erls = PolyEq_erls, srls = Erls, calc = [], (*asm_thm = [],*)
2.16 - rules = [Thm ("cancel_leading_coeff1",num_str @{thm cancel_leading_coeff1}),
2.17 - Thm ("cancel_leading_coeff2",num_str @{thm cancel_leading_coeff2}),
2.18 - Thm ("cancel_leading_coeff3",num_str @{thm cancel_leading_coeff3}),
2.19 - Thm ("cancel_leading_coeff4",num_str @{thm cancel_leading_coeff4}),
2.20 - Thm ("cancel_leading_coeff5",num_str @{thm cancel_leading_coeff5}),
2.21 - Thm ("cancel_leading_coeff6",num_str @{thm cancel_leading_coeff6}),
2.22 - Thm ("cancel_leading_coeff7",num_str @{thm cancel_leading_coeff7}),
2.23 - Thm ("cancel_leading_coeff8",num_str @{thm cancel_leading_coeff8}),
2.24 - Thm ("cancel_leading_coeff9",num_str @{thm cancel_leading_coeff9}),
2.25 - Thm ("cancel_leading_coeff10",num_str @{thm cancel_leading_coeff10}),
2.26 - Thm ("cancel_leading_coeff11",num_str @{thm cancel_leading_coeff11}),
2.27 - Thm ("cancel_leading_coeff12",num_str @{thm cancel_leading_coeff12}),
2.28 - Thm ("cancel_leading_coeff13",num_str @{thm cancel_leading_coeff13})
2.29 - ],
2.30 - scr = Script ((term_of o the o (parse thy))
2.31 - "empty_script")
2.32 - }:rls);
2.33 -
2.34 + rules =
2.35 + [Thm ("cancel_leading_coeff1",num_str @{thm cancel_leading_coeff1}),
2.36 + Thm ("cancel_leading_coeff2",num_str @{thm cancel_leading_coeff2}),
2.37 + Thm ("cancel_leading_coeff3",num_str @{thm cancel_leading_coeff3}),
2.38 + Thm ("cancel_leading_coeff4",num_str @{thm cancel_leading_coeff4}),
2.39 + Thm ("cancel_leading_coeff5",num_str @{thm cancel_leading_coeff5}),
2.40 + Thm ("cancel_leading_coeff6",num_str @{thm cancel_leading_coeff6}),
2.41 + Thm ("cancel_leading_coeff7",num_str @{thm cancel_leading_coeff7}),
2.42 + Thm ("cancel_leading_coeff8",num_str @{thm cancel_leading_coeff8}),
2.43 + Thm ("cancel_leading_coeff9",num_str @{thm cancel_leading_coeff9}),
2.44 + Thm ("cancel_leading_coeff10",num_str @{thm cancel_leading_coeff10}),
2.45 + Thm ("cancel_leading_coeff11",num_str @{thm cancel_leading_coeff11}),
2.46 + Thm ("cancel_leading_coeff12",num_str @{thm cancel_leading_coeff12}),
2.47 + Thm ("cancel_leading_coeff13",num_str @{thm cancel_leading_coeff13})
2.48 + ],scr = Script ((term_of o the o (parse thy)) "empty_script")}:rls);
2.49 +*}
2.50 +ML{*
2.51 val complete_square = prep_rls(
2.52 Rls {id = "complete_square", preconds = [],
2.53 rew_ord = ("e_rew_ord",e_rew_ord),
2.54 @@ -475,6 +474,8 @@
2.55 ("PolyEq_erls",PolyEq_erls),(*FIXXXME:del with rls.rls'*)
2.56 ("polyeq_simplify",polyeq_simplify)]);
2.57
2.58 +*}
2.59 +ML{*
2.60
2.61 (* ------------- polySolve ------------------ *)
2.62 (* -- d0 -- *)
2.63 @@ -512,6 +513,8 @@
2.64 scr = Script ((term_of o the o (parse thy)) "empty_script")
2.65 }:rls);
2.66
2.67 +*}
2.68 +ML{*
2.69 (* -- d2 -- *)
2.70 (* isolate the bound variable in an d2 equation with bdv only;
2.71 'bdv' is a meta-constant*)
2.72 @@ -546,7 +549,8 @@
2.73 ],
2.74 scr = Script ((term_of o the o (parse thy)) "empty_script")
2.75 }:rls);
2.76 -
2.77 +*}
2.78 +ML{*
2.79 (* isolate the bound variable in an d2 equation with sqrt only;
2.80 'bdv' is a meta-constant*)
2.81 val d2_polyeq_sq_only_simplify = prep_rls(
2.82 @@ -572,7 +576,8 @@
2.83 ],
2.84 scr = Script ((term_of o the o (parse thy)) "empty_script")
2.85 }:rls);
2.86 -
2.87 +*}
2.88 +ML{*
2.89 (* isolate the bound variable in an d2 equation with pqFormula;
2.90 'bdv' is a meta-constant*)
2.91 val d2_polyeq_pqFormula_simplify = prep_rls(
2.92 @@ -615,10 +620,10 @@
2.93 (* x^2=0 *)
2.94 Thm("d2_sqrt_equation3",num_str @{thm d2_sqrt_equation3})
2.95 (* 1x^2=0 *)
2.96 - ],
2.97 - scr = Script ((term_of o the o (parse thy)) "empty_script")
2.98 + ],scr = Script ((term_of o the o (parse thy)) "empty_script")
2.99 }:rls);
2.100 -
2.101 +*}
2.102 +ML{*
2.103 (* isolate the bound variable in an d2 equation with abcFormula;
2.104 'bdv' is a meta-constant*)
2.105 val d2_polyeq_abcFormula_simplify = prep_rls(
2.106 @@ -664,6 +669,8 @@
2.107 ],
2.108 scr = Script ((term_of o the o (parse thy)) "empty_script")
2.109 }:rls);
2.110 +*}
2.111 +ML{*
2.112
2.113 (* isolate the bound variable in an d2 equation;
2.114 'bdv' is a meta-constant*)
2.115 @@ -722,6 +729,8 @@
2.116 ],
2.117 scr = Script ((term_of o the o (parse thy)) "empty_script")
2.118 }:rls);
2.119 +*}
2.120 +ML{*
2.121
2.122 (* -- d3 -- *)
2.123 (* isolate the bound variable in an d3 equation; 'bdv' is a meta-constant *)
2.124 @@ -793,6 +802,8 @@
2.125 ],
2.126 scr = Script ((term_of o the o (parse thy)) "empty_script")
2.127 }:rls);
2.128 +*}
2.129 +ML{*
2.130
2.131 (* -- d4 -- *)
2.132 (*isolate the bound variable in an d4 equation; 'bdv' is a meta-constant*)
2.133 @@ -801,7 +812,7 @@
2.134 rew_ord = ("e_rew_ord",e_rew_ord), erls = PolyEq_erls,
2.135 srls = Erls, calc = [],
2.136 rules =
2.137 - [Thm("d4_sub_u1",num_str @{thm d4_sub_u1)
2.138 + [Thm("d4_sub_u1",num_str @{thm d4_sub_u1})
2.139 (* ax^4+bx^2+c=0 -> x=+-sqrt(ax^2+bx^+c) *)
2.140 ],
2.141 scr = Script ((term_of o the o (parse thy)) "empty_script")
2.142 @@ -821,6 +832,8 @@
2.143 ("d3_polyeq_simplify", d3_polyeq_simplify),
2.144 ("d4_polyeq_simplify", d4_polyeq_simplify)
2.145 ]);
2.146 +*}
2.147 +ML{*
2.148
2.149 (*------------------------problems------------------------*)
2.150 (*
2.151 @@ -867,7 +880,8 @@
2.152 ],
2.153 PolyEq_prls, SOME "solve (e_e::bool, v_v)",
2.154 [["PolyEq","solve_d1_polyeq_equation"]]));
2.155 -
2.156 +*}
2.157 +ML{*
2.158 (*--- d2 ---*)
2.159 store_pbt
2.160 (prep_pbt thy "pbl_equ_univ_poly_deg2" [] e_pblID
2.161 @@ -938,7 +952,8 @@
2.162 ],
2.163 PolyEq_prls, SOME "solve (e_e::bool, v_v)",
2.164 [["PolyEq","solve_d2_polyeq_abc_equation"]]));
2.165 -
2.166 +*}
2.167 +ML{*
2.168 (*--- d3 ---*)
2.169 store_pbt
2.170 (prep_pbt thy "pbl_equ_univ_poly_deg3" [] e_pblID
2.171 @@ -999,7 +1014,21 @@
2.172 PolyEq_prls, SOME "solve (e_e::bool, v_v)",
2.173 [["PolyEq","complete_square"]]));
2.174
2.175 -
2.176 +*}
2.177 +ML{*
2.178 +val scr =
2.179 + "Script Normalize_poly (e_e::bool) (v_v::real) = " ^
2.180 + "(let e_e =((Try (Rewrite all_left False)) @@ " ^
2.181 + " (Try (Repeat (Rewrite makex1_x False))) @@ " ^
2.182 + " (Try (Repeat (Rewrite_Set expand_binoms False))) @@ " ^
2.183 + " (Try (Repeat (Rewrite_Set_Inst [(bdv,v_v::real)] " ^
2.184 + " make_ratpoly_in False))) @@ " ^
2.185 + " (Try (Repeat (Rewrite_Set polyeq_simplify False)))) e_e " ^
2.186 + " in (SubProblem (PolyEq',[polynomial,univariate,equation], [no_met]) " ^
2.187 + " [BOOL e_e, REAL v_v]))";
2.188 +parse thy scr;
2.189 +*}
2.190 +ML{*
2.191 "-------------------------methods-----------------------";
2.192 store_met
2.193 (prep_met thy "met_polyeq" [] e_metID
2.194 @@ -1021,18 +1050,20 @@
2.195 srls=e_rls,
2.196 prls=PolyEq_prls,
2.197 calc=[],
2.198 - crls=PolyEq_crls, nrls=norm_Rational
2.199 + crls=PolyEq_crls, nrls=norm_Rational},
2.200 "Script Normalize_poly (e_e::bool) (v_v::real) = " ^
2.201 "(let e_e =((Try (Rewrite all_left False)) @@ " ^
2.202 " (Try (Repeat (Rewrite makex1_x False))) @@ " ^
2.203 " (Try (Repeat (Rewrite_Set expand_binoms False))) @@ " ^
2.204 - " (Try (Repeat (Rewrite_Set_Inst [(bdv,v_::real)] " ^
2.205 + " (Try (Repeat (Rewrite_Set_Inst [(bdv,v_v::real)] " ^
2.206 " make_ratpoly_in False))) @@ " ^
2.207 " (Try (Repeat (Rewrite_Set polyeq_simplify False)))) e_e " ^
2.208 - " in (SubProblem (PolyEq_,[polynomial,univariate,equation], " ^
2.209 - " [no_met]) [BOOL e_e, REAL v_]))"
2.210 + " in (SubProblem (PolyEq',[polynomial,univariate,equation], [no_met]) " ^
2.211 + " [BOOL e_e, REAL v_v]))"
2.212 ));
2.213
2.214 +*}
2.215 +ML{*
2.216 store_met
2.217 (prep_met thy "met_polyeq_d0" [] e_metID
2.218 (["PolyEq","solve_d0_polyeq_equation"],
2.219 @@ -1048,11 +1079,12 @@
2.220 calc=[("sqrt", ("NthRoot.sqrt", eval_sqrt "#sqrt_"))],
2.221 crls=PolyEq_crls, nrls=norm_Rational},
2.222 "Script Solve_d0_polyeq_equation (e_e::bool) (v_v::real) = " ^
2.223 - "(let e_e = ((Try (Rewrite_Set_Inst [(bdv,v_::real)] " ^
2.224 + "(let e_e = ((Try (Rewrite_Set_Inst [(bdv,v_v::real)] " ^
2.225 " d0_polyeq_simplify False))) e_e " ^
2.226 " in ((Or_to_List e_e)::bool list))"
2.227 ));
2.228 -
2.229 +*}
2.230 +ML{*
2.231 store_met
2.232 (prep_met thy "met_polyeq_d1" [] e_metID
2.233 (["PolyEq","solve_d1_polyeq_equation"],
2.234 @@ -1061,24 +1093,19 @@
2.235 "((lhs e_e) has_degree_in v_v) = 1"]),
2.236 ("#Find" ,["solutions v_i"])
2.237 ],
2.238 - {rew_ord'="termlessI",
2.239 - rls'=PolyEq_erls,
2.240 - srls=e_rls,
2.241 - prls=PolyEq_prls,
2.242 + {rew_ord'="termlessI", rls'=PolyEq_erls, srls=e_rls, prls=PolyEq_prls,
2.243 calc=[("sqrt", ("NthRoot.sqrt", eval_sqrt "#sqrt_"))],
2.244 - crls=PolyEq_crls, nrls=norm_Rational(*,
2.245 - (* asm_rls=["d1_polyeq_simplify"],*)
2.246 - asm_rls=[],
2.247 - asm_thm=[("d1_isolate_div","")]*)},
2.248 + crls=PolyEq_crls, nrls=norm_Rational},
2.249 "Script Solve_d1_polyeq_equation (e_e::bool) (v_v::real) = " ^
2.250 - "(let e_e = ((Try (Rewrite_Set_Inst [(bdv,v_::real)] " ^
2.251 + "(let e_e = ((Try (Rewrite_Set_Inst [(bdv,v_v::real)] " ^
2.252 " d1_polyeq_simplify True)) @@ " ^
2.253 " (Try (Rewrite_Set polyeq_simplify False)) @@ " ^
2.254 - " (Try (Rewrite_Set norm_Rational_parenthesized False))) e_;" ^
2.255 - " (L_::bool list) = ((Or_to_List e_e)::bool list) " ^
2.256 - " in Check_elementwise L_ {(v_v::real). Assumptions} )"
2.257 + " (Try (Rewrite_Set norm_Rational_parenthesized False))) e_e;" ^
2.258 + " (L_L::bool list) = ((Or_to_List e_e)::bool list) " ^
2.259 + " in Check_elementwise L_L {(v_v::real). Assumptions} )"
2.260 ));
2.261 -
2.262 +*}
2.263 +ML{*
2.264 store_met
2.265 (prep_met thy "met_polyeq_d22" [] e_metID
2.266 (["PolyEq","solve_d2_polyeq_equation"],
2.267 @@ -1094,17 +1121,18 @@
2.268 calc=[("sqrt", ("NthRoot.sqrt", eval_sqrt "#sqrt_"))],
2.269 crls=PolyEq_crls, nrls=norm_Rational},
2.270 "Script Solve_d2_polyeq_equation (e_e::bool) (v_v::real) = " ^
2.271 - " (let e_e = ((Try (Rewrite_Set_Inst [(bdv,v_::real)] " ^
2.272 + " (let e_e = ((Try (Rewrite_Set_Inst [(bdv,v_v::real)] " ^
2.273 " d2_polyeq_simplify True)) @@ " ^
2.274 " (Try (Rewrite_Set polyeq_simplify False)) @@ " ^
2.275 - " (Try (Rewrite_Set_Inst [(bdv,v_::real)] " ^
2.276 + " (Try (Rewrite_Set_Inst [(bdv,v_v::real)] " ^
2.277 " d1_polyeq_simplify True)) @@ " ^
2.278 " (Try (Rewrite_Set polyeq_simplify False)) @@ " ^
2.279 - " (Try (Rewrite_Set norm_Rational_parenthesized False))) e_;" ^
2.280 - " (L_::bool list) = ((Or_to_List e_e)::bool list) " ^
2.281 - " in Check_elementwise L_ {(v_v::real). Assumptions} )"
2.282 + " (Try (Rewrite_Set norm_Rational_parenthesized False))) e_e;" ^
2.283 + " (L_L::bool list) = ((Or_to_List e_e)::bool list) " ^
2.284 + " in Check_elementwise L_L {(v_v::real). Assumptions} )"
2.285 ));
2.286 -
2.287 +*}
2.288 +ML{*
2.289 store_met
2.290 (prep_met thy "met_polyeq_d2_bdvonly" [] e_metID
2.291 (["PolyEq","solve_d2_polyeq_bdvonly_equation"],
2.292 @@ -1120,17 +1148,18 @@
2.293 calc=[("sqrt", ("NthRoot.sqrt", eval_sqrt "#sqrt_"))],
2.294 crls=PolyEq_crls, nrls=norm_Rational},
2.295 "Script Solve_d2_polyeq_bdvonly_equation (e_e::bool) (v_v::real) =" ^
2.296 - " (let e_e = ((Try (Rewrite_Set_Inst [(bdv,v_::real)] " ^
2.297 + " (let e_e = ((Try (Rewrite_Set_Inst [(bdv,v_v::real)] " ^
2.298 " d2_polyeq_bdv_only_simplify True)) @@ " ^
2.299 " (Try (Rewrite_Set polyeq_simplify False)) @@ " ^
2.300 - " (Try (Rewrite_Set_Inst [(bdv,v_::real)] " ^
2.301 + " (Try (Rewrite_Set_Inst [(bdv,v_v::real)] " ^
2.302 " d1_polyeq_simplify True)) @@ " ^
2.303 " (Try (Rewrite_Set polyeq_simplify False)) @@ " ^
2.304 - " (Try (Rewrite_Set norm_Rational_parenthesized False))) e_;" ^
2.305 - " (L_::bool list) = ((Or_to_List e_e)::bool list) " ^
2.306 - " in Check_elementwise L_ {(v_v::real). Assumptions} )"
2.307 + " (Try (Rewrite_Set norm_Rational_parenthesized False))) e_e;" ^
2.308 + " (L_L::bool list) = ((Or_to_List e_e)::bool list) " ^
2.309 + " in Check_elementwise L_L {(v_v::real). Assumptions} )"
2.310 ));
2.311 -
2.312 +*}
2.313 +ML{*
2.314 store_met
2.315 (prep_met thy "met_polyeq_d2_sqonly" [] e_metID
2.316 (["PolyEq","solve_d2_polyeq_sqonly_equation"],
2.317 @@ -1146,14 +1175,15 @@
2.318 calc=[("sqrt", ("NthRoot.sqrt", eval_sqrt "#sqrt_"))],
2.319 crls=PolyEq_crls, nrls=norm_Rational},
2.320 "Script Solve_d2_polyeq_sqonly_equation (e_e::bool) (v_v::real) =" ^
2.321 - " (let e_e = ((Try (Rewrite_Set_Inst [(bdv,v_::real)] " ^
2.322 + " (let e_e = ((Try (Rewrite_Set_Inst [(bdv,v_v::real)] " ^
2.323 " d2_polyeq_sq_only_simplify True)) @@ " ^
2.324 " (Try (Rewrite_Set polyeq_simplify False)) @@ " ^
2.325 - " (Try (Rewrite_Set norm_Rational_parenthesized False))) e_; " ^
2.326 - " (L_::bool list) = ((Or_to_List e_e)::bool list) " ^
2.327 - " in Check_elementwise L_ {(v_v::real). Assumptions} )"
2.328 + " (Try (Rewrite_Set norm_Rational_parenthesized False))) e_e; " ^
2.329 + " (L_L::bool list) = ((Or_to_List e_e)::bool list) " ^
2.330 + " in Check_elementwise L_L {(v_v::real). Assumptions} )"
2.331 ));
2.332 -
2.333 +*}
2.334 +ML{*
2.335 store_met
2.336 (prep_met thy "met_polyeq_d2_pq" [] e_metID
2.337 (["PolyEq","solve_d2_polyeq_pq_equation"],
2.338 @@ -1169,14 +1199,15 @@
2.339 calc=[("sqrt", ("NthRoot.sqrt", eval_sqrt "#sqrt_"))],
2.340 crls=PolyEq_crls, nrls=norm_Rational},
2.341 "Script Solve_d2_polyeq_pq_equation (e_e::bool) (v_v::real) = " ^
2.342 - " (let e_e = ((Try (Rewrite_Set_Inst [(bdv,v_::real)] " ^
2.343 + " (let e_e = ((Try (Rewrite_Set_Inst [(bdv,v_v::real)] " ^
2.344 " d2_polyeq_pqFormula_simplify True)) @@ " ^
2.345 " (Try (Rewrite_Set polyeq_simplify False)) @@ " ^
2.346 - " (Try (Rewrite_Set norm_Rational_parenthesized False))) e_;" ^
2.347 - " (L_::bool list) = ((Or_to_List e_e)::bool list) " ^
2.348 - " in Check_elementwise L_ {(v_v::real). Assumptions} )"
2.349 + " (Try (Rewrite_Set norm_Rational_parenthesized False))) e_e;" ^
2.350 + " (L_L::bool list) = ((Or_to_List e_e)::bool list) " ^
2.351 + " in Check_elementwise L_L {(v_v::real). Assumptions} )"
2.352 ));
2.353 -
2.354 +*}
2.355 +ML{*
2.356 store_met
2.357 (prep_met thy "met_polyeq_d2_abc" [] e_metID
2.358 (["PolyEq","solve_d2_polyeq_abc_equation"],
2.359 @@ -1192,14 +1223,15 @@
2.360 calc=[("sqrt", ("NthRoot.sqrt", eval_sqrt "#sqrt_"))],
2.361 crls=PolyEq_crls, nrls=norm_Rational},
2.362 "Script Solve_d2_polyeq_abc_equation (e_e::bool) (v_v::real) = " ^
2.363 - " (let e_e = ((Try (Rewrite_Set_Inst [(bdv,v_::real)] " ^
2.364 + " (let e_e = ((Try (Rewrite_Set_Inst [(bdv,v_v::real)] " ^
2.365 " d2_polyeq_abcFormula_simplify True)) @@ " ^
2.366 " (Try (Rewrite_Set polyeq_simplify False)) @@ " ^
2.367 - " (Try (Rewrite_Set norm_Rational_parenthesized False))) e_;" ^
2.368 - " (L_::bool list) = ((Or_to_List e_e)::bool list) " ^
2.369 - " in Check_elementwise L_ {(v_v::real). Assumptions} )"
2.370 + " (Try (Rewrite_Set norm_Rational_parenthesized False))) e_e;" ^
2.371 + " (L_L::bool list) = ((Or_to_List e_e)::bool list) " ^
2.372 + " in Check_elementwise L_L {(v_v::real). Assumptions} )"
2.373 ));
2.374 -
2.375 +*}
2.376 +ML{*
2.377 store_met
2.378 (prep_met thy "met_polyeq_d3" [] e_metID
2.379 (["PolyEq","solve_d3_polyeq_equation"],
2.380 @@ -1215,20 +1247,21 @@
2.381 calc=[("sqrt", ("NthRoot.sqrt", eval_sqrt "#sqrt_"))],
2.382 crls=PolyEq_crls, nrls=norm_Rational},
2.383 "Script Solve_d3_polyeq_equation (e_e::bool) (v_v::real) = " ^
2.384 - " (let e_e = ((Try (Rewrite_Set_Inst [(bdv,v_::real)] " ^
2.385 + " (let e_e = ((Try (Rewrite_Set_Inst [(bdv,v_v::real)] " ^
2.386 " d3_polyeq_simplify True)) @@ " ^
2.387 " (Try (Rewrite_Set polyeq_simplify False)) @@ " ^
2.388 - " (Try (Rewrite_Set_Inst [(bdv,v_::real)] " ^
2.389 + " (Try (Rewrite_Set_Inst [(bdv,v_v::real)] " ^
2.390 " d2_polyeq_simplify True)) @@ " ^
2.391 " (Try (Rewrite_Set polyeq_simplify False)) @@ " ^
2.392 - " (Try (Rewrite_Set_Inst [(bdv,v_::real)] " ^
2.393 + " (Try (Rewrite_Set_Inst [(bdv,v_v::real)] " ^
2.394 " d1_polyeq_simplify True)) @@ " ^
2.395 " (Try (Rewrite_Set polyeq_simplify False)) @@ " ^
2.396 - " (Try (Rewrite_Set norm_Rational_parenthesized False))) e_;" ^
2.397 - " (L_::bool list) = ((Or_to_List e_e)::bool list) " ^
2.398 - " in Check_elementwise L_ {(v_v::real). Assumptions} )"
2.399 + " (Try (Rewrite_Set norm_Rational_parenthesized False))) e_e;" ^
2.400 + " (L_L::bool list) = ((Or_to_List e_e)::bool list) " ^
2.401 + " in Check_elementwise L_L {(v_v::real). Assumptions} )"
2.402 ));
2.403 -
2.404 +*}
2.405 +ML{*
2.406 (*.solves all expanded (ie. normalized) terms of degree 2.*)
2.407 (*Oct.02 restriction: 'eval_true 0 =< discriminant' ony for integer values
2.408 by 'PolyEq_erls'; restricted until Float.thy is implemented*)
2.409 @@ -1243,21 +1276,23 @@
2.410 {rew_ord'="termlessI",rls'=PolyEq_erls,srls=e_rls,prls=PolyEq_prls,
2.411 calc=[("sqrt", ("NthRoot.sqrt", eval_sqrt "#sqrt_"))],
2.412 crls=PolyEq_crls, nrls=norm_Rational},
2.413 - "Script Complete_square (e_e::bool) (v_v::real) = " ^
2.414 - "(let e_e = ((Try (Rewrite_Set_Inst [(bdv,v_)] cancel_leading_coeff True))" ^
2.415 - " @@ (Try (Rewrite_Set_Inst [(bdv,v_)] complete_square True)) " ^
2.416 + "Script Complete_square (e_e::bool) (v_v::real) = " ^
2.417 + "(let e_e = " ^
2.418 + " ((Try (Rewrite_Set_Inst [(bdv,v_v)] cancel_leading_coeff True)) " ^
2.419 + " @@ (Try (Rewrite_Set_Inst [(bdv,v_v)] complete_square True)) " ^
2.420 " @@ (Try (Rewrite square_explicit1 False)) " ^
2.421 " @@ (Try (Rewrite square_explicit2 False)) " ^
2.422 " @@ (Rewrite root_plus_minus True) " ^
2.423 - " @@ (Try (Repeat (Rewrite_Inst [(bdv,v_)] bdv_explicit1 False))) " ^
2.424 - " @@ (Try (Repeat (Rewrite_Inst [(bdv,v_)] bdv_explicit2 False))) " ^
2.425 + " @@ (Try (Repeat (Rewrite_Inst [(bdv,v_v)] bdv_explicit1 False))) " ^
2.426 + " @@ (Try (Repeat (Rewrite_Inst [(bdv,v_v)] bdv_explicit2 False))) " ^
2.427 " @@ (Try (Repeat " ^
2.428 - " (Rewrite_Inst [(bdv,v_)] bdv_explicit3 False))) " ^
2.429 + " (Rewrite_Inst [(bdv,v_v)] bdv_explicit3 False))) " ^
2.430 " @@ (Try (Rewrite_Set calculate_RootRat False)) " ^
2.431 " @@ (Try (Repeat (Calculate SQRT)))) e_e " ^
2.432 " in ((Or_to_List e_e)::bool list))"
2.433 ));
2.434 -
2.435 +*}
2.436 +ML{*
2.437
2.438 (* termorder hacked by MG *)
2.439 local (*. for make_polynomial_in .*)
2.440 @@ -1292,24 +1327,24 @@
2.441 | size_of_term' x _ = 1;
2.442
2.443
2.444 -fun Term_Ord.term_ord' x pr thy (Abs (_, T, t), Abs(_, U, u)) = (* ~ term.ML *)
2.445 - (case Term_Ord.term_ord' x pr thy (t, u) of EQUAL => Term_Ord.typ_ord (T, U) | ord => ord)
2.446 - | Term_Ord.term_ord' x pr thy (t, u) =
2.447 +fun term_ord' x pr thy (Abs (_, T, t), Abs(_, U, u)) = (* ~ term.ML *)
2.448 + (case term_ord' x pr thy (t, u) of EQUAL => Term_Ord.typ_ord (T, U) | ord => ord)
2.449 + | term_ord' x pr thy (t, u) =
2.450 (if pr then
2.451 let
2.452 val (f, ts) = strip_comb t and (g, us) = strip_comb u;
2.453 val _=writeln("t= f@ts= \""^
2.454 ((Syntax.string_of_term (thy2ctxt thy)) f)^"\" @ \"["^
2.455 - (commas(map(string_of_cterm o cterm_of(sign_of thy)) ts))^"]\"");
2.456 + (commas(map (Syntax.string_of_term (thy2ctxt thy)) ts))^"]\"");
2.457 val _=writeln("u= g@us= \""^
2.458 ((Syntax.string_of_term (thy2ctxt thy)) g)^"\" @ \"["^
2.459 - (commas(map(string_of_cterm o cterm_of(sign_of thy)) us))^"]\"");
2.460 + (commas(map (Syntax.string_of_term (thy2ctxt thy)) us))^"]\"");
2.461 val _=writeln("size_of_term(t,u)= ("^
2.462 (string_of_int(size_of_term' x t))^", "^
2.463 (string_of_int(size_of_term' x u))^")");
2.464 val _=writeln("hd_ord(f,g) = "^((pr_ord o (hd_ord x))(f,g)));
2.465 val _=writeln("terms_ord(ts,us) = "^
2.466 - ((pr_ord o (terms_ord x) str false)(ts,us)));
2.467 + ((pr_ord o (terms_ord x) str false)(ts, us)));
2.468 val _=writeln("-------");
2.469 in () end
2.470 else ();
2.471 @@ -1321,10 +1356,10 @@
2.472 end
2.473 | ord => ord)
2.474 and hd_ord x (f, g) = (* ~ term.ML *)
2.475 - prod_ord (prod_ord indexname_ord Term_Ord.typ_ord) int_ord (dest_hd' x f,
2.476 - dest_hd' x g)
2.477 + prod_ord (prod_ord Term_Ord.indexname_ord Term_Ord.typ_ord)
2.478 + int_ord (dest_hd' x f, dest_hd' x g)
2.479 and terms_ord x str pr (ts, us) =
2.480 - list_ord (term_ord' x pr (assoc_thy "Isac.thy"))(ts, us);
2.481 + list_ord (term_ord' x pr (assoc_thy "Isac"))(ts, us);
2.482 in
2.483
2.484 fun ord_make_polynomial_in (pr:bool) thy subst tu =
2.485 @@ -1336,12 +1371,14 @@
2.486 | _ => raise error ("ord_make_polynomial_in called with subst = "^
2.487 (subst2str subst))
2.488 end;
2.489 -end;
2.490 +end;(*local*)
2.491
2.492 +*}
2.493 +ML{*
2.494 val order_add_mult_in = prep_rls(
2.495 Rls{id = "order_add_mult_in", preconds = [],
2.496 rew_ord = ("ord_make_polynomial_in",
2.497 - ord_make_polynomial_in false Poly.thy),
2.498 + ord_make_polynomial_in false (theory "Poly")),
2.499 erls = e_rls,srls = Erls,
2.500 calc = [],
2.501 (*asm_thm = [],*)
2.502 @@ -1359,6 +1396,8 @@
2.503 (*z1.0 + z2.0 + z3.0 = z1.0 + (z2.0 + z3.0)*)
2.504 ], scr = EmptyScr}:rls);
2.505
2.506 +*}
2.507 +ML{*
2.508 val collect_bdv = prep_rls(
2.509 Rls{id = "collect_bdv", preconds = [],
2.510 rew_ord = ("dummy_ord", dummy_ord),
2.511 @@ -1388,9 +1427,11 @@
2.512
2.513 Thm ("bdv_n_collect_assoc2_1",num_str @{thm bdv_n_collect_assoc2_1}),
2.514 Thm ("bdv_n_collect_assoc2_2",num_str @{thm bdv_n_collect_assoc2_2}),
2.515 - Thm ("bdv_n_collect_assoc2_3",num_str @{thm bdv_n_collect_assoc2_3)
2.516 + Thm ("bdv_n_collect_assoc2_3",num_str @{thm bdv_n_collect_assoc2_3})
2.517 ], scr = EmptyScr}:rls);
2.518
2.519 +*}
2.520 +ML{*
2.521 (*.transforms an arbitrary term without roots to a polynomial [4]
2.522 according to knowledge/Poly.sml.*)
2.523 val make_polynomial_in = prep_rls(
2.524 @@ -1410,21 +1451,25 @@
2.525 scr = EmptyScr
2.526 }:rls);
2.527
2.528 +*}
2.529 +ML{*
2.530 val separate_bdvs =
2.531 append_rls "separate_bdvs"
2.532 collect_bdv
2.533 - [Thm ("separate_bdv", num_str @{separate_bdv}),
2.534 + [Thm ("separate_bdv", num_str @{thm separate_bdv}),
2.535 (*"?a * ?bdv / ?b = ?a / ?b * ?bdv"*)
2.536 - Thm ("separate_bdv_n", num_str @{separate_bdv_n}),
2.537 - Thm ("separate_1_bdv", num_str @{separate_1_bdv}),
2.538 + Thm ("separate_bdv_n", num_str @{thm separate_bdv_n}),
2.539 + Thm ("separate_1_bdv", num_str @{thm separate_1_bdv}),
2.540 (*"?bdv / ?b = (1 / ?b) * ?bdv"*)
2.541 - Thm ("separate_1_bdv_n", num_str @{separate_1_bdv_n}),
2.542 + Thm ("separate_1_bdv_n", num_str @{thm separate_1_bdv_n}),
2.543 (*"?bdv ^^^ ?n / ?b = 1 / ?b * ?bdv ^^^ ?n"*)
2.544 Thm ("nadd_divide_distrib",
2.545 - num_str @{thm nadd_divide_distrib})
2.546 + num_str @{thm add_divide_distrib})
2.547 (*"(?x + ?y) / ?z = ?x / ?z + ?y / ?z"
2.548 WN051031 DOES NOT BELONG TO HERE*)
2.549 ];
2.550 +*}
2.551 +ML{*
2.552 val make_ratpoly_in = prep_rls(
2.553 Seq {id = "make_ratpoly_in", preconds = []:term list,
2.554 rew_ord = ("dummy_ord", dummy_ord),
3.1 --- a/src/Tools/isac/Knowledge/RootRatEq.thy Wed Sep 08 12:41:04 2010 +0200
3.2 +++ b/src/Tools/isac/Knowledge/RootRatEq.thy Wed Sep 08 16:28:24 2010 +0200
3.3 @@ -68,7 +68,8 @@
3.4 else SOME ((term2str p) ^ " = True",
3.5 Trueprop $ (mk_equality (p, HOLogic.false_const)))
3.6 | eval_is_rootRatAddTerm_in _ _ _ _ = ((*writeln"### nichts matcht";*) NONE);
3.7 -
3.8 +*}
3.9 +ML {*
3.10 (*-------------------------rulse-------------------------*)
3.11 val RootRatEq_prls =
3.12 append_rls "RootRatEq_prls" e_rls
3.13 @@ -105,27 +106,31 @@
3.14 ruleset' := overwritelthy @{theory} (!ruleset',
3.15 [("RooRatEq_erls",RooRatEq_erls) (*FIXXXME:del with rls.rls'*)]);
3.16
3.17 +*}
3.18 +ML {*
3.19 (* Solves a rootrat Equation *)
3.20 val rootrat_solve = prep_rls(
3.21 Rls {id = "rootrat_solve", preconds = [],
3.22 rew_ord = ("termlessI",termlessI),
3.23 erls = e_rls, srls = Erls, calc = [], (*asm_thm = [],*)
3.24 - rules = [Thm("rootrat_equation_left_1", num_str @{thm }rootrat_equation_left_1),
3.25 + rules =
3.26 + [Thm("rootrat_equation_left_1", num_str @{thm rootrat_equation_left_1}),
3.27 (* [|c is_rootTerm_in bdv|] ==>
3.28 ( (a + b/c = d) = ( b = (d - a) * c )) *)
3.29 - Thm("rootrat_equation_left_2",num_str @{thm rootrat_equation_left_2}),
3.30 + Thm("rootrat_equation_left_2",num_str @{thm rootrat_equation_left_2}),
3.31 (* [|c is_rootTerm_in bdv|] ==> ( (b/c = d) = ( b = d * c )) *)
3.32 - Thm("rootrat_equation_right_1",num_str @{thm rootrat_equation_right_1}),
3.33 + Thm("rootrat_equation_right_1",num_str @{thm rootrat_equation_right_1}),
3.34 (* [|f is_rootTerm_in bdv|] ==>
3.35 ( (a = d + e/f) = ( (a - d) * f = e )) *)
3.36 - Thm("rootrat_equation_right_2",num_str @{thm rootrat_equation_right_2})
3.37 + Thm("rootrat_equation_right_2",num_str @{thm rootrat_equation_right_2})
3.38 (* [|f is_rootTerm_in bdv|] ==> ( (a = e/f) = ( a * f = e ))*)
3.39 - ],
3.40 - scr = Script ((term_of o the o (parse thy)) "empty_script")
3.41 - }:rls);
3.42 + ], scr = Script ((term_of o the o (parse thy)) "empty_script")}:rls);
3.43 +
3.44 ruleset' := overwritelthy @{theory} (!ruleset',
3.45 [("rootrat_solve",rootrat_solve)
3.46 ]);
3.47 +*}
3.48 +ML {*
3.49
3.50 (*-----------------------probleme------------------------*)
3.51 (*
3.52 @@ -143,7 +148,8 @@
3.53 ],
3.54 RootRatEq_prls, SOME "solve (e_e::bool, v_v)",
3.55 [["RootRatEq","elim_rootrat_equation"]]));
3.56 -
3.57 +*}
3.58 +ML {*
3.59 (*-------------------------Methode-----------------------*)
3.60 store_met
3.61 (prep_met (theory "LinEq") "met_rootrateq" [] e_metID
3.62 @@ -173,10 +179,10 @@
3.63 " (Try (Rewrite_Set rooteq_simplify False)) @@ " ^
3.64 " (Try (Rewrite_Set make_rooteq False)) @@ " ^
3.65 " (Try (Rewrite_Set rooteq_simplify False)) @@ " ^
3.66 - " (Try (Rewrite_Set_Inst [(bdv,v_)] " ^
3.67 + " (Try (Rewrite_Set_Inst [(bdv,v_v)] " ^
3.68 " rootrat_solve False))) e_e " ^
3.69 " in (SubProblem (RootEq',[univariate,equation], " ^
3.70 - " [no_met]) [BOOL e_e, REAL v_]))"
3.71 + " [no_met]) [BOOL e_e, REAL v_v]))"
3.72 ));
3.73 calclist':= overwritel (!calclist',
3.74 [("is_rootRatAddTerm_in", ("RootRatEq.is_rootRatAddTerm_in",