1.1 --- a/src/Tools/isac/Build_Isac.thy Thu Sep 09 13:39:30 2010 +0200
1.2 +++ b/src/Tools/isac/Build_Isac.thy Fri Sep 10 10:36:41 2010 +0200
1.3 @@ -83,8 +83,8 @@
1.4 use_thy "Knowledge/Integrate"
1.5 use_thy "Knowledge/EqSystem"
1.6 use_thy "Knowledge/Biegelinie"
1.7 -
1.8 use_thy "Knowledge/AlgEin"
1.9 +use_thy "Knowledge/Test"
1.10
1.11 ML {* 111;
1.12 *}
1.13 @@ -92,7 +92,6 @@
1.14
1.15 text {*------------------------------------------*}
1.16 (*
1.17 -use_thy "Knowledge/Test"
1.18 use_thy "Knowledge/Isac"
1.19 *)
1.20 end
2.1 --- a/src/Tools/isac/Knowledge/Test.thy Thu Sep 09 13:39:30 2010 +0200
2.2 +++ b/src/Tools/isac/Knowledge/Test.thy Fri Sep 10 10:36:41 2010 +0200
2.3 @@ -3,7 +3,7 @@
2.4 (c) due to copyright terms
2.5 *)
2.6
2.7 -theory Test imports Atools + Rational + Root + Poly +
2.8 +theory Test imports Atools Rational Root Poly begin
2.9
2.10 consts
2.11
2.12 @@ -29,8 +29,8 @@
2.13
2.14 (*17.9.02 aus SqRoot.thy------------------------------vvv---*)
2.15
2.16 - "is'_root'_free" :: 'a => bool ("is'_root'_free _" 10)
2.17 - "contains'_root" :: 'a => bool ("contains'_root _" 10)
2.18 + "is'_root'_free" :: "'a => bool" ("is'_root'_free _" 10)
2.19 + "contains'_root" :: "'a => bool" ("contains'_root _" 10)
2.20
2.21 Solve'_root'_equation
2.22 :: "[bool,real,
2.23 @@ -203,9 +203,10 @@
2.24 ]);
2.25
2.26 (** term order **)
2.27 -fun Term_Ord.term_order (_:subst) tu = (term_ordI [] tu = LESS);
2.28 -
2.29 -(** rule sets GOON **)
2.30 +fun term_order (_:subst) tu = (term_ordI [] tu = LESS);
2.31 +*}
2.32 +ML {*
2.33 +(** rule sets **)
2.34
2.35 val testerls =
2.36 Rls {id = "testerls", preconds = [], rew_ord = ("termlessI",termlessI),
2.37 @@ -237,7 +238,8 @@
2.38 scr = Script ((term_of o the o (parse thy))
2.39 "empty_script")
2.40 }:rls;
2.41 -
2.42 +*}
2.43 +ML {*
2.44 (*.for evaluation of conditions in rewrite rules.*)
2.45 (*FIXXXXXXME 10.8.02: handle like _simplify*)
2.46 val tval_rls =
2.47 @@ -255,7 +257,7 @@
2.48 Thm ("or_true",num_str @{thm or_true}),
2.49 Thm ("or_false",num_str @{thm or_false}),
2.50 Thm ("and_commute",num_str @{thm and_commute}),
2.51 - Thm ("or_commute",num_str @{or_commute}),
2.52 + Thm ("or_commute",num_str @{thm or_commute}),
2.53
2.54 Thm ("real_diff_minus",num_str @{thm real_diff_minus}),
2.55
2.56 @@ -282,7 +284,8 @@
2.57 scr = Script ((term_of o the o (parse thy))
2.58 "empty_script")
2.59 }:rls;
2.60 -
2.61 +*}
2.62 +ML {*
2.63
2.64 ruleset' := overwritelthy @{theory} (!ruleset',
2.65 [("testerls", prep_rls testerls)
2.66 @@ -319,16 +322,17 @@
2.67 val norm_equation =
2.68 Rls{id = "norm_equation", preconds = [], rew_ord = ("e_rew_ord",e_rew_ord),
2.69 erls = tval_rls, srls = e_rls, calc = [], (*asm_thm=[],*)
2.70 - rules = [Thm ("rnorm_equation_add",num_str @{thm rnorm_equation_add)
2.71 + rules = [Thm ("rnorm_equation_add",num_str @{thm rnorm_equation_add})
2.72 ],
2.73 scr = Script ((term_of o the o (parse thy))
2.74 "empty_script")
2.75 }:rls;
2.76 -
2.77 +*}
2.78 +ML {*
2.79 (** rule sets **)
2.80
2.81 val STest_simplify = (* vv--- not changed to real by parse*)
2.82 - "Script STest_simplify (t_::'z) = " ^
2.83 + "Script STest_simplify (t_t::'z) = " ^
2.84 "(Repeat" ^
2.85 " ((Try (Repeat (Rewrite real_diff_minus False))) @@ " ^
2.86 " (Try (Repeat (Rewrite radd_mult_distrib2 False))) @@ " ^
2.87 @@ -372,9 +376,10 @@
2.88 " (Try (Repeat (Rewrite rmult_0_right False))) @@ " ^
2.89 " (Try (Repeat (Rewrite radd_0 False))) @@ " ^
2.90 " (Try (Repeat (Rewrite radd_0_right False)))) " ^
2.91 - " t_)";
2.92 + " t_t)";
2.93
2.94 -
2.95 +*}
2.96 +ML {*
2.97 (* expects * distributed over + *)
2.98 val Test_simplify =
2.99 Rls{id = "Test_simplify", preconds = [],
2.100 @@ -417,7 +422,7 @@
2.101 Thm ("rroot_times_root",num_str @{thm rroot_times_root}),
2.102 Thm ("rroot_times_root_assoc_p",num_str @{thm rroot_times_root_assoc_p}),
2.103 Thm ("rsqare",num_str @{thm rsqare}),
2.104 - Thm ("power_1",num_str @{power_1}),
2.105 + Thm ("power_1",num_str @{thm power_1}),
2.106 Thm ("rtwo_of_the_same",num_str @{thm rtwo_of_the_same}),
2.107 Thm ("rtwo_of_the_same_assoc_p",num_str @{thm rtwo_of_the_same_assoc_p}),
2.108
2.109 @@ -431,10 +436,8 @@
2.110 scr = Script ((term_of o the o (parse thy)) "empty_script")
2.111 (*since 040209 filled by prep_rls: STest_simplify*)
2.112 }:rls;
2.113 -
2.114 -
2.115 -
2.116 -
2.117 +*}
2.118 +ML {*
2.119
2.120 (** rule sets **)
2.121
2.122 @@ -462,16 +465,15 @@
2.123 [Thm ("risolate_bdv_add",num_str @{thm risolate_bdv_add}),
2.124 Thm ("risolate_bdv_mult_add",num_str @{thm risolate_bdv_mult_add}),
2.125 Thm ("risolate_bdv_mult",num_str @{thm risolate_bdv_mult}),
2.126 - Thm ("mult_square",num_str @{mult_square}),
2.127 - Thm ("constant_square",num_str @{constant_square}),
2.128 - Thm ("constant_mult_square",num_str @{constant_mult_square})
2.129 + Thm ("mult_square",num_str @{thm mult_square}),
2.130 + Thm ("constant_square",num_str @{thm constant_square}),
2.131 + Thm ("constant_mult_square",num_str @{thm constant_mult_square})
2.132 ],
2.133 scr = Script ((term_of o the o (parse thy))
2.134 "empty_script")
2.135 }:rls;
2.136 -
2.137 -
2.138 -
2.139 +*}
2.140 +ML {*
2.141
2.142 (* association list for calculate_, calculate
2.143 "op +" etc. not usable in scripts *)
2.144 @@ -507,6 +509,8 @@
2.145 [Calc ("Tools.matches",eval_matches "#matches_")]))
2.146 ]);
2.147
2.148 +*}
2.149 +ML {*
2.150 (** problem types **)
2.151 store_pbt
2.152 (prep_pbt thy "pbl_test" [] e_pblID
2.153 @@ -537,8 +541,8 @@
2.154 (prep_pbt thy "pbl_test_uni_lin" [] e_pblID
2.155 (["linear","univariate","equation","test"],
2.156 [("#Given" ,["equality e_e","solveFor v_v"]),
2.157 - ("#Where" ,["(matches ( v_v = 0) e_e) | (matches ( ?b*v_ = 0) e_e) |" ^
2.158 - "(matches (?a+v_ = 0) e_e) | (matches (?a+?b*v_ = 0) e_e) "]),
2.159 + ("#Where" ,["(matches ( v_v = 0) e_e) | (matches ( ?b*v_v = 0) e_e) |" ^
2.160 + "(matches (?a+v_v = 0) e_e) | (matches (?a+?b*v_v = 0) e_e) "]),
2.161 ("#Find" ,["solutions v_i"])
2.162 ],
2.163 assoc_rls "matches",
2.164 @@ -548,7 +552,7 @@
2.165 store_pbt
2.166 (prep_pbt thy
2.167 (["thy"],
2.168 - [("#Given" ,"boolTestGiven g_"),
2.169 + [("#Given" ,"boolTestGiven g_g"),
2.170 ("#Find" ,"boolTestFind f_f")
2.171 ],
2.172 []));
2.173 @@ -556,7 +560,7 @@
2.174 store_pbt
2.175 (prep_pbt thy
2.176 (["testeq","thy"],
2.177 - [("#Given" ,"boolTestGiven g_"),
2.178 + [("#Given" ,"boolTestGiven g_g"),
2.179 ("#Find" ,"boolTestFind f_f")
2.180 ],
2.181 []));
2.182 @@ -566,7 +570,8 @@
2.183
2.184 ------ 25.8.01*)
2.185
2.186 -
2.187 +*}
2.188 +ML {*
2.189 (** methods **)
2.190 store_met
2.191 (prep_met (theory "Diff") "met_test" [] e_metID
2.192 @@ -583,6 +588,8 @@
2.193 {rew_ord'="e_rew_ord",rls'=tval_rls,srls=e_rls,prls=e_rls,calc=[],
2.194 asm_rls=[],asm_thm=[]},
2.195 "Undef"));*)
2.196 +*}
2.197 +ML {*
2.198 store_met
2.199 (prep_met thy "met_test_solvelin" [] e_metID
2.200 (["Test","solve_linear"]:metID,
2.201 @@ -590,27 +597,26 @@
2.202 ("#Where" ,["matches (?a = ?b) e_e"]),
2.203 ("#Find" ,["solutions v_i"])
2.204 ],
2.205 - {rew_ord'="e_rew_ord",rls'=tval_rls,srls=e_rls,
2.206 - prls=assoc_rls "matches",
2.207 - calc=[],
2.208 - crls=tval_rls, nrls=Test_simplify},
2.209 - "Script Solve_linear (e_e::bool) (v_v::real)= " ^
2.210 - "(let e_e =" ^
2.211 - " Repeat" ^
2.212 - " (((Rewrite_Set_Inst [(bdv,v_v::real)] isolate_bdv False) @@" ^
2.213 + {rew_ord' = "e_rew_ord", rls' = tval_rls, srls = e_rls,
2.214 + prls = assoc_rls "matches", calc = [], crls = tval_rls,
2.215 + nrls = Test_simplify},
2.216 + "Script Solve_linear (e_e::bool) (v_v::real)= " ^
2.217 + "(let e_e = " ^
2.218 + " Repeat " ^
2.219 + " (((Rewrite_Set_Inst [(bdv,v_v::real)] isolate_bdv False) @@ " ^
2.220 " (Rewrite_Set Test_simplify False))) e_e" ^
2.221 - " in [e_::bool])"
2.222 + " in [e_e::bool])"
2.223 )
2.224 (*, prep_met thy (*test for equations*)
2.225 (["Test","testeq"]:metID,
2.226 - [("#Given" ,["boolTestGiven g_"]),
2.227 + [("#Given" ,["boolTestGiven g_g"]),
2.228 ("#Find" ,["boolTestFind f_f"])
2.229 ],
2.230 {rew_ord'="e_rew_ord",rls'="tval_rls",asm_rls=[],
2.231 asm_thm=[("square_equation_left","")]},
2.232 - "Script Testeq (eq_::bool) = " ^
2.233 + "Script Testeq (e_q::bool) = " ^
2.234 "Repeat " ^
2.235 - " (let e_e = Try (Repeat (Rewrite rroot_square_inv False eq_)); " ^
2.236 + " (let e_e = Try (Repeat (Rewrite rroot_square_inv False e_q)); " ^
2.237 " e_e = Try (Repeat (Rewrite square_equation_left True e_e)); " ^
2.238 " e_e = Try (Repeat (Rewrite rmult_0 False e_e)) " ^
2.239 " in e_e) Until (is_root_free e_e)" (*deleted*)
2.240 @@ -618,8 +624,8 @@
2.241 , ---------27.4.02*)
2.242 );
2.243
2.244 -
2.245 -
2.246 +*}
2.247 +ML {*
2.248
2.249 ruleset' := overwritelthy @{theory} (!ruleset',
2.250 [("norm_equation", prep_rls norm_equation),
2.251 @@ -764,7 +770,8 @@
2.252 fun rational t div_op bdVar =
2.253 is_denom bdVar div_op t andalso bin_ops_only t;
2.254
2.255 -
2.256 +*}
2.257 +ML {*
2.258
2.259 (** problem types **)
2.260
2.261 @@ -772,8 +779,8 @@
2.262 (prep_pbt thy "pbl_test_uni_plain2" [] e_pblID
2.263 (["plain_square","univariate","equation","test"],
2.264 [("#Given" ,["equality e_e","solveFor v_v"]),
2.265 - ("#Where" ,["(matches (?a + ?b*v_ ^^^2 = 0) e_e) |" ^
2.266 - "(matches ( ?b*v_ ^^^2 = 0) e_e) |" ^
2.267 + ("#Where" ,["(matches (?a + ?b*v_v ^^^2 = 0) e_e) |" ^
2.268 + "(matches ( ?b*v_v ^^^2 = 0) e_e) |" ^
2.269 "(matches (?a + v_v ^^^2 = 0) e_e) |" ^
2.270 "(matches ( v_v ^^^2 = 0) e_e)"]),
2.271 ("#Find" ,["solutions v_i"])
2.272 @@ -781,13 +788,13 @@
2.273 assoc_rls "matches",
2.274 SOME "solve (e_e::bool, v_v)", [["Test","solve_plain_square"]]));
2.275 (*
2.276 - val e_e = (term_of o the o (parse thy)) "e_::bool";
2.277 + val e_e = (term_of o the o (parse thy)) "e_e::bool";
2.278 val ve = (term_of o the o (parse thy)) "4 + 3*x^^^2 = 0";
2.279 val env = [(e_,ve)];
2.280
2.281 val pre = (term_of o the o (parse thy))
2.282 - "(matches (a + b*v_ ^^^2 = 0, e_e::bool)) |" ^
2.283 - "(matches ( b*v_ ^^^2 = 0, e_e::bool)) |" ^
2.284 + "(matches (a + b*v_v ^^^2 = 0, e_e::bool)) |" ^
2.285 + "(matches ( b*v_v ^^^2 = 0, e_e::bool)) |" ^
2.286 "(matches (a + v_v ^^^2 = 0, e_e::bool)) |" ^
2.287 "(matches ( v_v ^^^2 = 0, e_e::bool))";
2.288 val prei = subst_atomic env pre;
2.289 @@ -803,10 +810,12 @@
2.290
2.291 *)
2.292
2.293 +*}
2.294 +ML {*
2.295 store_pbt
2.296 (prep_pbt thy "pbl_test_uni_poly" [] e_pblID
2.297 (["polynomial","univariate","equation","test"],
2.298 - [("#Given" ,["equality (v_ ^^^2 + p_ * v_v + q__ = 0)","solveFor v_v"]),
2.299 + [("#Given" ,["equality (v_v ^^^2 + p_p * v_v + q__q = 0)","solveFor v_v"]),
2.300 ("#Where" ,["False"]),
2.301 ("#Find" ,["solutions v_i"])
2.302 ],
2.303 @@ -815,27 +824,29 @@
2.304 store_pbt
2.305 (prep_pbt thy "pbl_test_uni_poly_deg2" [] e_pblID
2.306 (["degree_two","polynomial","univariate","equation","test"],
2.307 - [("#Given" ,["equality (v_ ^^^2 + p_ * v_v + q__ = 0)","solveFor v_v"]),
2.308 + [("#Given" ,["equality (v_v ^^^2 + p_p * v_v + q__q = 0)","solveFor v_v"]),
2.309 ("#Find" ,["solutions v_i"])
2.310 ],
2.311 - e_rls, SOME "solve (v_ ^^^2 + p_ * v_v + q__ = 0, v_v)", []));
2.312 + e_rls, SOME "solve (v_v ^^^2 + p_p * v_v + q__q = 0, v_v)", []));
2.313
2.314 store_pbt
2.315 (prep_pbt thy "pbl_test_uni_poly_deg2_pq" [] e_pblID
2.316 (["pq_formula","degree_two","polynomial","univariate","equation","test"],
2.317 - [("#Given" ,["equality (v_ ^^^2 + p_ * v_v + q__ = 0)","solveFor v_v"]),
2.318 + [("#Given" ,["equality (v_v ^^^2 + p_p * v_v + q__q = 0)","solveFor v_v"]),
2.319 ("#Find" ,["solutions v_i"])
2.320 ],
2.321 - e_rls, SOME "solve (v_ ^^^2 + p_ * v_v + q__ = 0, v_v)", []));
2.322 + e_rls, SOME "solve (v_v ^^^2 + p_p * v_v + q__q = 0, v_v)", []));
2.323
2.324 store_pbt
2.325 (prep_pbt thy "pbl_test_uni_poly_deg2_abc" [] e_pblID
2.326 (["abc_formula","degree_two","polynomial","univariate","equation","test"],
2.327 - [("#Given" ,["equality (a_ * x ^^^2 + b_ * x + c_ = 0)","solveFor v_v"]),
2.328 + [("#Given" ,["equality (a_a * x ^^^2 + b_b * x + c_c = 0)","solveFor v_v"]),
2.329 ("#Find" ,["solutions v_i"])
2.330 ],
2.331 - e_rls, SOME "solve (a_ * x ^^^2 + b_ * x + c_ = 0, v_v)", []));
2.332 + e_rls, SOME "solve (a_a * x ^^^2 + b_b * x + c_c = 0, v_v)", []));
2.333
2.334 +*}
2.335 +ML {*
2.336 store_pbt
2.337 (prep_pbt thy "pbl_test_uni_root" [] e_pblID
2.338 (["squareroot","univariate","equation","test"],
2.339 @@ -868,6 +879,8 @@
2.340 (*
2.341 (#ppc o get_pbt) ["sqroot-test","univariate","equation"];
2.342 *)
2.343 +*}
2.344 +ML {*
2.345
2.346
2.347 store_met
2.348 @@ -900,9 +913,11 @@
2.349 " (Rewrite_Set_Inst [(bdv,v_v::real)] isolate_bdv False) @@" ^
2.350 " (Try (Rewrite_Set Test_simplify False)))" ^
2.351 " e_e" ^
2.352 - " in [e_::bool])"
2.353 + " in [e_e::bool])"
2.354 ));
2.355
2.356 +*}
2.357 +ML {*
2.358 store_met
2.359 (prep_met thy "met_test_sqrt2" [] e_metID
2.360 (*root-equation ... for test-*.sml until 8.01*)
2.361 @@ -930,11 +945,13 @@
2.362 " (Rewrite_Set_Inst [(bdv,v_v::real)] isolate_bdv False) @@" ^
2.363 " (Try (Rewrite_Set Test_simplify False)))" ^
2.364 " e_e;" ^
2.365 - " (L_::bool list) = Tac subproblem_equation_dummy; " ^
2.366 + " (L_L::bool list) = Tac subproblem_equation_dummy; " ^
2.367 " L_L = Tac solve_equation_dummy " ^
2.368 " in Check_elementwise L_L {(v_v::real). Assumptions})"
2.369 ));
2.370
2.371 +*}
2.372 +ML {*
2.373 store_met
2.374 (prep_met thy "met_test_squ_sub" [] e_metID
2.375 (*tests subproblem fixed linear*)
2.376 @@ -944,14 +961,18 @@
2.377 ],
2.378 {rew_ord'="e_rew_ord",rls'=tval_rls,srls=e_rls,prls=e_rls,calc=[],
2.379 crls=tval_rls, nrls=Test_simplify},
2.380 - "Script Solve_root_equation (e_e::bool) (v_v::real) = " ^
2.381 - " (let e_e = ((Try (Rewrite_Set norm_equation False)) @@ " ^
2.382 - " (Try (Rewrite_Set Test_simplify False))) e_e; " ^
2.383 - "(L_::bool list) = (SubProblem (Test_,[linear,univariate,equation,test]," ^
2.384 - " [Test,solve_linear]) [BOOL e_e, REAL v_])" ^
2.385 + "Script Solve_root_equation (e_e::bool) (v_v::real) = " ^
2.386 + " (let e_e = ((Try (Rewrite_Set norm_equation False)) @@ " ^
2.387 + " (Try (Rewrite_Set Test_simplify False))) e_e; " ^
2.388 + "(L_L::bool list) = (SubProblem (Test', " ^
2.389 + " [linear,univariate,equation,test], " ^
2.390 + " [Test,solve_linear])" ^
2.391 + " [BOOL e_e, REAL v_v])" ^
2.392 "in Check_elementwise L_L {(v_v::real). Assumptions})"
2.393 ));
2.394
2.395 +*}
2.396 +ML {*
2.397 store_met
2.398 (prep_met thy "met_test_squ_sub2" [] e_metID
2.399 (*tests subproblem fixed degree 2*)
2.400 @@ -965,11 +986,13 @@
2.401 ("square_equation_right","")]*)},
2.402 "Script Solve_root_equation (e_e::bool) (v_v::real) = " ^
2.403 " (let e_e = Try (Rewrite_Set norm_equation False) e_e; " ^
2.404 - "(L_::bool list) = (SubProblem (Test_,[linear,univariate,equation,test]," ^
2.405 - " [Test,solve_by_pq_formula]) [BOOL e_e, REAL v_])" ^
2.406 + "(L_L::bool list) = (SubProblem (Test',[linear,univariate,equation,test]," ^
2.407 + " [Test,solve_by_pq_formula]) [BOOL e_e, REAL v_v])" ^
2.408 "in Check_elementwise L_L {(v_v::real). Assumptions})"
2.409 ));
2.410
2.411 +*}
2.412 +ML {*
2.413 store_met
2.414 (prep_met thy "met_test_squ_nonterm" [] e_metID
2.415 (*root-equation: see foils..., but notTerminating*)
2.416 @@ -995,12 +1018,14 @@
2.417 " (Try (Rewrite_Set norm_equation False)) @@" ^
2.418 " (Try (Rewrite_Set Test_simplify False)))" ^
2.419 " e_e;" ^
2.420 - " (L_::bool list) = " ^
2.421 - " (SubProblem (Test_,[linear,univariate,equation,test]," ^
2.422 - " [Test,solve_linear]) [BOOL e_e, REAL v_])" ^
2.423 + " (L_L::bool list) = " ^
2.424 + " (SubProblem (Test',[linear,univariate,equation,test]," ^
2.425 + " [Test,solve_linear]) [BOOL e_e, REAL v_v])" ^
2.426 "in Check_elementwise L_L {(v_v::real). Assumptions})"
2.427 ));
2.428
2.429 +*}
2.430 +ML {*
2.431 store_met
2.432 (prep_met thy "met_test_eq1" [] e_metID
2.433 (*root-equation1:*)
2.434 @@ -1026,11 +1051,13 @@
2.435 " (Try (Rewrite_Set norm_equation False)) @@" ^
2.436 " (Try (Rewrite_Set Test_simplify False)))" ^
2.437 " e_e;" ^
2.438 - " (L_::bool list) = (SubProblem (Test_,[linear,univariate,equation,test]," ^
2.439 - " [Test,solve_linear]) [BOOL e_e, REAL v_])" ^
2.440 + " (L_L::bool list) = (SubProblem (Test',[linear,univariate,equation,test]," ^
2.441 + " [Test,solve_linear]) [BOOL e_e, REAL v_v])" ^
2.442 " in Check_elementwise L_L {(v_v::real). Assumptions})"
2.443 ));
2.444
2.445 +*}
2.446 +ML {*
2.447 store_met
2.448 (prep_met thy "met_test_squ2" [] e_metID
2.449 (*root-equation2*)
2.450 @@ -1057,11 +1084,13 @@
2.451 " (Try (Rewrite_Set norm_equation False)) @@" ^
2.452 " (Try (Rewrite_Set Test_simplify False)))" ^
2.453 " e_e;" ^
2.454 - " (L_::bool list) = (SubProblem (Test_,[plain_square,univariate,equation,test]," ^
2.455 - " [Test,solve_plain_square]) [BOOL e_e, REAL v_])" ^
2.456 + " (L_L::bool list) = (SubProblem (Test',[plain_square,univariate,equation,test]," ^
2.457 + " [Test,solve_plain_square]) [BOOL e_e, REAL v_v])" ^
2.458 " in Check_elementwise L_L {(v_v::real). Assumptions})"
2.459 ));
2.460
2.461 +*}
2.462 +ML {*
2.463 store_met
2.464 (prep_met thy "met_test_squeq" [] e_metID
2.465 (*root-equation*)
2.466 @@ -1088,18 +1117,20 @@
2.467 " (Try (Rewrite_Set norm_equation False)) @@" ^
2.468 " (Try (Rewrite_Set Test_simplify False)))" ^
2.469 " e_e;" ^
2.470 - " (L_::bool list) = (SubProblem (Test_,[univariate,equation,test]," ^
2.471 - " [no_met]) [BOOL e_e, REAL v_])" ^
2.472 + " (L_L::bool list) = (SubProblem (Test',[univariate,equation,test]," ^
2.473 + " [no_met]) [BOOL e_e, REAL v_v])" ^
2.474 " in Check_elementwise L_L {(v_v::real). Assumptions})"
2.475 ) ); (*#######*)
2.476
2.477 +*}
2.478 +ML {*
2.479 store_met
2.480 (prep_met thy "met_test_eq_plain" [] e_metID
2.481 (*solve_plain_square*)
2.482 (["Test","solve_plain_square"]:metID,
2.483 [("#Given",["equality e_e","solveFor v_v"]),
2.484 - ("#Where" ,["(matches (?a + ?b*v_ ^^^2 = 0) e_e) |" ^
2.485 - "(matches ( ?b*v_ ^^^2 = 0) e_e) |" ^
2.486 + ("#Where" ,["(matches (?a + ?b*v_v ^^^2 = 0) e_e) |" ^
2.487 + "(matches ( ?b*v_v ^^^2 = 0) e_e) |" ^
2.488 "(matches (?a + v_v ^^^2 = 0) e_e) |" ^
2.489 "(matches ( v_v ^^^2 = 0) e_e)"]),
2.490 ("#Find" ,["solutions v_i"])
2.491 @@ -1117,6 +1148,8 @@
2.492 " in ((Or_to_List e_e)::bool list))"
2.493 ));
2.494
2.495 +*}
2.496 +ML {*
2.497 store_met
2.498 (prep_met thy "met_test_norm_univ" [] e_metID
2.499 (["Test","norm_univar_equation"]:metID,
2.500 @@ -1130,13 +1163,15 @@
2.501 "Script Norm_univar_equation (e_e::bool) (v_v::real) = " ^
2.502 " (let e_e = ((Try (Rewrite rnorm_equation_add False)) @@ " ^
2.503 " (Try (Rewrite_Set Test_simplify False))) e_e " ^
2.504 - " in (SubProblem (Test_,[univariate,equation,test], " ^
2.505 - " [no_met]) [BOOL e_e, REAL v_]))"
2.506 + " in (SubProblem (Test',[univariate,equation,test], " ^
2.507 + " [no_met]) [BOOL e_e, REAL v_v]))"
2.508 ));
2.509
2.510
2.511
2.512 (*17.9.02 aus SqRoot.ML------------------------------^^^---*)
2.513 +*}
2.514 +ML {*
2.515
2.516 (*8.4.03 aus Poly.ML--------------------------------vvv---
2.517 make_polynomial ---> make_poly
2.518 @@ -1171,18 +1206,18 @@
2.519 | size_of_term' (f$t) = size_of_term' f + size_of_term' t
2.520 | size_of_term' _ = 1;
2.521
2.522 -fun Term_Ord.term_ord' pr thy (Abs (_, T, t), Abs(_, U, u)) = (* ~ term.ML *)
2.523 - (case Term_Ord.term_ord' pr thy (t, u) of EQUAL => Term_Ord.typ_ord (T, U) | ord => ord)
2.524 - | Term_Ord.term_ord' pr thy (t, u) =
2.525 +fun term_ord' pr thy (Abs (_, T, t), Abs(_, U, u)) = (* ~ term.ML *)
2.526 + (case term_ord' pr thy (t, u) of EQUAL => Term_Ord.typ_ord (T, U) | ord => ord)
2.527 + | term_ord' pr thy (t, u) =
2.528 (if pr then
2.529 let
2.530 val (f, ts) = strip_comb t and (g, us) = strip_comb u;
2.531 val _=writeln("t= f@ts= " ^ "" ^
2.532 ((Syntax.string_of_term (thy2ctxt thy)) f)^ "\" @ " ^ "[" ^
2.533 - (commas(map(Syntax.string_of_term (thy2ctxt thy)) ts)) ^ "]""");
2.534 + (commas(map(Syntax.string_of_term (thy2ctxt thy)) ts)) ^ "]\"");
2.535 val _=writeln("u= g@us= " ^ "" ^
2.536 ((Syntax.string_of_term (thy2ctxt thy)) g) ^ "\" @ " ^ "[" ^
2.537 - (commas(map(Syntax.string_of_term (thy2ctxt thy)) us))^"]""");
2.538 + (commas(map(Syntax.string_of_term (thy2ctxt thy)) us))^"]\"");
2.539 val _=writeln("size_of_term(t,u)= ("^
2.540 (string_of_int(size_of_term' t)) ^ ", " ^
2.541 (string_of_int(size_of_term' u)) ^ ")");
2.542 @@ -1209,6 +1244,8 @@
2.543 (term_ord' pr thy(***) tu = LESS );
2.544
2.545 end;(*local*)
2.546 +*}
2.547 +ML {*
2.548
2.549 rew_ord' := overwritel (!rew_ord',
2.550 [("termlessI", termlessI),
2.551 @@ -1217,7 +1254,7 @@
2.552
2.553 (*WN060510 this was a preparation for prep_rls ...
2.554 val scr_make_polytest =
2.555 -"Script Expand_binomtest t_ =" ^
2.556 +"Script Expand_binomtest t_t =" ^
2.557 "(Repeat " ^
2.558 "((Try (Repeat (Rewrite real_diff_minus False))) @@ " ^
2.559
2.560 @@ -1251,7 +1288,7 @@
2.561 " (Try (Repeat (Calculate PLUS ))) @@ " ^
2.562 " (Try (Repeat (Calculate TIMES ))) @@ " ^
2.563 " (Try (Repeat (Calculate POWER)))) " ^
2.564 -" t_)";
2.565 +" t_t)";
2.566 -----------------------------------------------------*)
2.567
2.568 val make_polytest =
2.569 @@ -1321,10 +1358,12 @@
2.570 ],
2.571 scr = EmptyScr(*Script ((term_of o the o (parse thy))
2.572 scr_make_polytest)*)
2.573 - }:rls;
2.574 -(*WN060510 this was done before 'fun prep_rls' ...
2.575 + }:rls;
2.576 +*}
2.577 +ML {*
2.578 +(*WN060510 this was done before 'fun prep_rls' ...------------------------
2.579 val scr_expand_binomtest =
2.580 -"Script Expand_binomtest t_ =" ^
2.581 +"Script Expand_binomtest t_t =" ^
2.582 "(Repeat " ^
2.583 "((Try (Repeat (Rewrite real_plus_binom_pow2 False))) @@ " ^
2.584 " (Try (Repeat (Rewrite real_plus_binom_times False))) @@ " ^
2.585 @@ -1355,8 +1394,8 @@
2.586 " (Try (Repeat (Calculate PLUS ))) @@ " ^
2.587 " (Try (Repeat (Calculate TIMES ))) @@ " ^
2.588 " (Try (Repeat (Calculate POWER)))) " ^
2.589 -" t_)";
2.590 -------------------------------------------------------*)
2.591 +" t_t)";
2.592 +--------------------------------------------------------------------------*)
2.593
2.594 val expand_binomtest =
2.595 Rls{id = "expand_binomtest", preconds = [],
2.596 @@ -1366,85 +1405,90 @@
2.597 ("TIMES" , ("op *", eval_binop "#mult_")),
2.598 ("POWER", ("Atools.pow", eval_binop "#power_"))
2.599 ],
2.600 - rules = [Thm ("real_plus_binom_pow2" ,num_str @{thm real_plus_binom_pow2}),
2.601 + rules =
2.602 + [Thm ("real_plus_binom_pow2" ,num_str @{thm real_plus_binom_pow2}),
2.603 (*"(a + b) ^^^ 2 = a ^^^ 2 + 2 * a * b + b ^^^ 2"*)
2.604 - Thm ("real_plus_binom_times" ,num_str @{thm real_plus_binom_times}),
2.605 + Thm ("real_plus_binom_times" ,num_str @{thm real_plus_binom_times}),
2.606 (*"(a + b)*(a + b) = ...*)
2.607 - Thm ("real_minus_binom_pow2" ,num_str @{thm real_minus_binom_pow2}),
2.608 - (*"(a - b) ^^^ 2 = a ^^^ 2 - 2 * a * b + b ^^^ 2"*)
2.609 - Thm ("real_minus_binom_times",num_str @{thm real_minus_binom_times}),
2.610 - (*"(a - b)*(a - b) = ...*)
2.611 - Thm ("real_plus_minus_binom1",num_str @{thm real_plus_minus_binom1}),
2.612 - (*"(a + b) * (a - b) = a ^^^ 2 - b ^^^ 2"*)
2.613 - Thm ("real_plus_minus_binom2",num_str @{thm real_plus_minus_binom2}),
2.614 - (*"(a - b) * (a + b) = a ^^^ 2 - b ^^^ 2"*)
2.615 - (*RL 020915*)
2.616 - Thm ("real_pp_binom_times",num_str @{thm real_pp_binom_times}),
2.617 - (*(a + b)*(c + d) = a*c + a*d + b*c + b*d*)
2.618 - Thm ("real_pm_binom_times",num_str @{thm real_pm_binom_times}),
2.619 - (*(a + b)*(c - d) = a*c - a*d + b*c - b*d*)
2.620 - Thm ("real_mp_binom_times",num_str @{thm real_mp_binom_times}),
2.621 - (*(a - b)*(c p d) = a*c + a*d - b*c - b*d*)
2.622 - Thm ("real_mm_binom_times",num_str @{thm real_mm_binom_times}),
2.623 - (*(a - b)*(c p d) = a*c - a*d - b*c + b*d*)
2.624 - Thm ("realpow_multI",num_str @{thm realpow_multI}),
2.625 - (*(a*b)^^^n = a^^^n * b^^^n*)
2.626 - Thm ("real_plus_binom_pow3",num_str @{thm real_plus_binom_pow3}),
2.627 - (* (a + b)^^^3 = a^^^3 + 3*a^^^2*b + 3*a*b^^^2 + b^^^3 *)
2.628 - Thm ("real_minus_binom_pow3",num_str @{thm real_minus_binom_pow3}),
2.629 - (* (a - b)^^^3 = a^^^3 - 3*a^^^2*b + 3*a*b^^^2 - b^^^3 *)
2.630 + Thm ("real_minus_binom_pow2" ,num_str @{thm real_minus_binom_pow2}),
2.631 + (*"(a - b) ^^^ 2 = a ^^^ 2 - 2 * a * b + b ^^^ 2"*)
2.632 + Thm ("real_minus_binom_times",num_str @{thm real_minus_binom_times}),
2.633 + (*"(a - b)*(a - b) = ...*)
2.634 + Thm ("real_plus_minus_binom1",num_str @{thm real_plus_minus_binom1}),
2.635 + (*"(a + b) * (a - b) = a ^^^ 2 - b ^^^ 2"*)
2.636 + Thm ("real_plus_minus_binom2",num_str @{thm real_plus_minus_binom2}),
2.637 + (*"(a - b) * (a + b) = a ^^^ 2 - b ^^^ 2"*)
2.638 + (*RL 020915*)
2.639 + Thm ("real_pp_binom_times",num_str @{thm real_pp_binom_times}),
2.640 + (*(a + b)*(c + d) = a*c + a*d + b*c + b*d*)
2.641 + Thm ("real_pm_binom_times",num_str @{thm real_pm_binom_times}),
2.642 + (*(a + b)*(c - d) = a*c - a*d + b*c - b*d*)
2.643 + Thm ("real_mp_binom_times",num_str @{thm real_mp_binom_times}),
2.644 + (*(a - b)*(c p d) = a*c + a*d - b*c - b*d*)
2.645 + Thm ("real_mm_binom_times",num_str @{thm real_mm_binom_times}),
2.646 + (*(a - b)*(c p d) = a*c - a*d - b*c + b*d*)
2.647 + Thm ("realpow_multI",num_str @{thm realpow_multI}),
2.648 + (*(a*b)^^^n = a^^^n * b^^^n*)
2.649 + Thm ("real_plus_binom_pow3",num_str @{thm real_plus_binom_pow3}),
2.650 + (* (a + b)^^^3 = a^^^3 + 3*a^^^2*b + 3*a*b^^^2 + b^^^3 *)
2.651 + Thm ("real_minus_binom_pow3",num_str @{thm real_minus_binom_pow3}),
2.652 + (* (a - b)^^^3 = a^^^3 - 3*a^^^2*b + 3*a*b^^^2 - b^^^3 *)
2.653
2.654
2.655 - (* Thm ("left_distrib" ,num_str @{thm left_distrib}}),
2.656 - (*"(z1.0 + z2.0) * w = z1.0 * w + z2.0 * w"*)
2.657 - Thm ("right_distrib",num_str @{thm right_distrib}),
2.658 - (*"w * (z1.0 + z2.0) = w * z1.0 + w * z2.0"*)
2.659 - Thm ("left_diff_distrib" ,num_str @{thm left_diff_distrib}}),
2.660 - (*"(z1.0 - z2.0) * w = z1.0 * w - z2.0 * w"*)
2.661 - Thm ("right_diff_distrib",num_str @{thm right_diff_distrib}),
2.662 - (*"w * (z1.0 - z2.0) = w * z1.0 - w * z2.0"*)
2.663 - *)
2.664 -
2.665 - Thm ("mult_1_left",num_str @{thm mult_1_left}}), (*"1 * z = z"*)
2.666 - Thm ("mult_zero_left",num_str @{thm mult_zero_left}}), (*"0 * z = 0"*)
2.667 - Thm ("add_0_left",num_str @{thm add_0_left}}),(*"0 + z = z"*)
2.668 + (* Thm ("left_distrib" ,num_str @{thm left_distrib}),
2.669 + (*"(z1.0 + z2.0) * w = z1.0 * w + z2.0 * w"*)
2.670 + Thm ("right_distrib",num_str @{thm right_distrib}),
2.671 + (*"w * (z1.0 + z2.0) = w * z1.0 + w * z2.0"*)
2.672 + Thm ("left_diff_distrib" ,num_str @{thm left_diff_distrib}),
2.673 + (*"(z1.0 - z2.0) * w = z1.0 * w - z2.0 * w"*)
2.674 + Thm ("right_diff_distrib",num_str @{thm right_diff_distrib}),
2.675 + (*"w * (z1.0 - z2.0) = w * z1.0 - w * z2.0"*)
2.676 + *)
2.677 +
2.678 + Thm ("mult_1_left",num_str @{thm mult_1_left}),
2.679 + (*"1 * z = z"*)
2.680 + Thm ("mult_zero_left",num_str @{thm mult_zero_left}),
2.681 + (*"0 * z = 0"*)
2.682 + Thm ("add_0_left",num_str @{thm add_0_left}),
2.683 + (*"0 + z = z"*)
2.684
2.685 - Calc ("op +", eval_binop "#add_"),
2.686 - Calc ("op *", eval_binop "#mult_"),
2.687 - Calc ("Atools.pow", eval_binop "#power_"),
2.688 - (*
2.689 - Thm ("real_mult_commute",num_str @{thm real_mult_commute}), (*AC-rewriting*)
2.690 - Thm ("real_mult_left_commute",num_str @{thm real_mult_left_commute}), (**)
2.691 - Thm ("real_mult_assoc",num_str @{thm real_mult_assoc}), (**)
2.692 - Thm ("add_commute",num_str @{thm add_commute}), (**)
2.693 - Thm ("add_left_commute",num_str @{thm add_left_commute}), (**)
2.694 - Thm ("add_assoc",num_str @{thm add_assoc}), (**)
2.695 - *)
2.696 -
2.697 - Thm ("sym_realpow_twoI",
2.698 - num_str (@{thm realpow_twoI} RS @{thm sym})),
2.699 - (*"r1 * r1 = r1 ^^^ 2"*)
2.700 - Thm ("realpow_plus_1",num_str @{thm realpow_plus_1}),
2.701 - (*"r * r ^^^ n = r ^^^ (n + 1)"*)
2.702 - (*Thm ("sym_real_mult_2",
2.703 - num_str (@{thm real_mult_2} RS @{thm sym})),
2.704 - (*"z1 + z1 = 2 * z1"*)*)
2.705 - Thm ("real_mult_2_assoc",num_str @{thm real_mult_2_assoc}),
2.706 - (*"z1 + (z1 + k) = 2 * z1 + k"*)
2.707 + Calc ("op +", eval_binop "#add_"),
2.708 + Calc ("op *", eval_binop "#mult_"),
2.709 + Calc ("Atools.pow", eval_binop "#power_"),
2.710 + (*
2.711 + Thm ("real_mult_commute",num_str @{thm real_mult_commute}),
2.712 + (*AC-rewriting*)
2.713 + Thm ("real_mult_left_commute",num_str @{thm real_mult_left_commute}),
2.714 + Thm ("real_mult_assoc",num_str @{thm real_mult_assoc}),
2.715 + Thm ("add_commute",num_str @{thm add_commute}),
2.716 + Thm ("add_left_commute",num_str @{thm add_left_commute}),
2.717 + Thm ("add_assoc",num_str @{thm add_assoc}),
2.718 + *)
2.719 +
2.720 + Thm ("sym_realpow_twoI",
2.721 + num_str (@{thm realpow_twoI} RS @{thm sym})),
2.722 + (*"r1 * r1 = r1 ^^^ 2"*)
2.723 + Thm ("realpow_plus_1",num_str @{thm realpow_plus_1}),
2.724 + (*"r * r ^^^ n = r ^^^ (n + 1)"*)
2.725 + (*Thm ("sym_real_mult_2",
2.726 + num_str (@{thm real_mult_2} RS @{thm sym})),
2.727 + (*"z1 + z1 = 2 * z1"*)*)
2.728 + Thm ("real_mult_2_assoc",num_str @{thm real_mult_2_assoc}),
2.729 + (*"z1 + (z1 + k) = 2 * z1 + k"*)
2.730
2.731 - Thm ("real_num_collect",num_str @{thm real_num_collect}),
2.732 - (*"[| l is_const; m is_const |] ==> l * n + m * n = (l + m) * n"*)
2.733 - Thm ("real_num_collect_assoc",num_str @{thm real_num_collect_assoc}),
2.734 - (*"[| l is_const; m is_const |] ==> l * n + (m * n + k) = (l + m) * n + k"*)
2.735 - Thm ("real_one_collect",num_str @{thm real_one_collect}),
2.736 - (*"m is_const ==> n + m * n = (1 + m) * n"*)
2.737 - Thm ("real_one_collect_assoc",num_str @{thm real_one_collect_assoc}),
2.738 - (*"m is_const ==> k + (n + m * n) = k + (1 + m) * n"*)
2.739 + Thm ("real_num_collect",num_str @{thm real_num_collect}),
2.740 + (*"[| l is_const; m is_const |] ==> l * n + m * n = (l + m) * n"*)
2.741 + Thm ("real_num_collect_assoc",num_str @{thm real_num_collect_assoc}),
2.742 + (*"[| l is_const; m is_const |] ==> l * n + (m * n + k) = (l + m) * n + k"*)
2.743 + Thm ("real_one_collect",num_str @{thm real_one_collect}),
2.744 + (*"m is_const ==> n + m * n = (1 + m) * n"*)
2.745 + Thm ("real_one_collect_assoc",num_str @{thm real_one_collect_assoc}),
2.746 + (*"m is_const ==> k + (n + m * n) = k + (1 + m) * n"*)
2.747
2.748 - Calc ("op +", eval_binop "#add_"),
2.749 - Calc ("op *", eval_binop "#mult_"),
2.750 - Calc ("Atools.pow", eval_binop "#power_")
2.751 - ],
2.752 + Calc ("op +", eval_binop "#add_"),
2.753 + Calc ("op *", eval_binop "#mult_"),
2.754 + Calc ("Atools.pow", eval_binop "#power_")
2.755 + ],
2.756 scr = EmptyScr
2.757 (*Script ((term_of o the o (parse thy)) scr_expand_binomtest)*)
2.758 }:rls;