1.1 --- a/src/Tools/isac/Knowledge/Test.thy Thu Sep 09 13:39:30 2010 +0200
1.2 +++ b/src/Tools/isac/Knowledge/Test.thy Fri Sep 10 10:36:41 2010 +0200
1.3 @@ -3,7 +3,7 @@
1.4 (c) due to copyright terms
1.5 *)
1.6
1.7 -theory Test imports Atools + Rational + Root + Poly +
1.8 +theory Test imports Atools Rational Root Poly begin
1.9
1.10 consts
1.11
1.12 @@ -29,8 +29,8 @@
1.13
1.14 (*17.9.02 aus SqRoot.thy------------------------------vvv---*)
1.15
1.16 - "is'_root'_free" :: 'a => bool ("is'_root'_free _" 10)
1.17 - "contains'_root" :: 'a => bool ("contains'_root _" 10)
1.18 + "is'_root'_free" :: "'a => bool" ("is'_root'_free _" 10)
1.19 + "contains'_root" :: "'a => bool" ("contains'_root _" 10)
1.20
1.21 Solve'_root'_equation
1.22 :: "[bool,real,
1.23 @@ -203,9 +203,10 @@
1.24 ]);
1.25
1.26 (** term order **)
1.27 -fun Term_Ord.term_order (_:subst) tu = (term_ordI [] tu = LESS);
1.28 -
1.29 -(** rule sets GOON **)
1.30 +fun term_order (_:subst) tu = (term_ordI [] tu = LESS);
1.31 +*}
1.32 +ML {*
1.33 +(** rule sets **)
1.34
1.35 val testerls =
1.36 Rls {id = "testerls", preconds = [], rew_ord = ("termlessI",termlessI),
1.37 @@ -237,7 +238,8 @@
1.38 scr = Script ((term_of o the o (parse thy))
1.39 "empty_script")
1.40 }:rls;
1.41 -
1.42 +*}
1.43 +ML {*
1.44 (*.for evaluation of conditions in rewrite rules.*)
1.45 (*FIXXXXXXME 10.8.02: handle like _simplify*)
1.46 val tval_rls =
1.47 @@ -255,7 +257,7 @@
1.48 Thm ("or_true",num_str @{thm or_true}),
1.49 Thm ("or_false",num_str @{thm or_false}),
1.50 Thm ("and_commute",num_str @{thm and_commute}),
1.51 - Thm ("or_commute",num_str @{or_commute}),
1.52 + Thm ("or_commute",num_str @{thm or_commute}),
1.53
1.54 Thm ("real_diff_minus",num_str @{thm real_diff_minus}),
1.55
1.56 @@ -282,7 +284,8 @@
1.57 scr = Script ((term_of o the o (parse thy))
1.58 "empty_script")
1.59 }:rls;
1.60 -
1.61 +*}
1.62 +ML {*
1.63
1.64 ruleset' := overwritelthy @{theory} (!ruleset',
1.65 [("testerls", prep_rls testerls)
1.66 @@ -319,16 +322,17 @@
1.67 val norm_equation =
1.68 Rls{id = "norm_equation", preconds = [], rew_ord = ("e_rew_ord",e_rew_ord),
1.69 erls = tval_rls, srls = e_rls, calc = [], (*asm_thm=[],*)
1.70 - rules = [Thm ("rnorm_equation_add",num_str @{thm rnorm_equation_add)
1.71 + rules = [Thm ("rnorm_equation_add",num_str @{thm rnorm_equation_add})
1.72 ],
1.73 scr = Script ((term_of o the o (parse thy))
1.74 "empty_script")
1.75 }:rls;
1.76 -
1.77 +*}
1.78 +ML {*
1.79 (** rule sets **)
1.80
1.81 val STest_simplify = (* vv--- not changed to real by parse*)
1.82 - "Script STest_simplify (t_::'z) = " ^
1.83 + "Script STest_simplify (t_t::'z) = " ^
1.84 "(Repeat" ^
1.85 " ((Try (Repeat (Rewrite real_diff_minus False))) @@ " ^
1.86 " (Try (Repeat (Rewrite radd_mult_distrib2 False))) @@ " ^
1.87 @@ -372,9 +376,10 @@
1.88 " (Try (Repeat (Rewrite rmult_0_right False))) @@ " ^
1.89 " (Try (Repeat (Rewrite radd_0 False))) @@ " ^
1.90 " (Try (Repeat (Rewrite radd_0_right False)))) " ^
1.91 - " t_)";
1.92 + " t_t)";
1.93
1.94 -
1.95 +*}
1.96 +ML {*
1.97 (* expects * distributed over + *)
1.98 val Test_simplify =
1.99 Rls{id = "Test_simplify", preconds = [],
1.100 @@ -417,7 +422,7 @@
1.101 Thm ("rroot_times_root",num_str @{thm rroot_times_root}),
1.102 Thm ("rroot_times_root_assoc_p",num_str @{thm rroot_times_root_assoc_p}),
1.103 Thm ("rsqare",num_str @{thm rsqare}),
1.104 - Thm ("power_1",num_str @{power_1}),
1.105 + Thm ("power_1",num_str @{thm power_1}),
1.106 Thm ("rtwo_of_the_same",num_str @{thm rtwo_of_the_same}),
1.107 Thm ("rtwo_of_the_same_assoc_p",num_str @{thm rtwo_of_the_same_assoc_p}),
1.108
1.109 @@ -431,10 +436,8 @@
1.110 scr = Script ((term_of o the o (parse thy)) "empty_script")
1.111 (*since 040209 filled by prep_rls: STest_simplify*)
1.112 }:rls;
1.113 -
1.114 -
1.115 -
1.116 -
1.117 +*}
1.118 +ML {*
1.119
1.120 (** rule sets **)
1.121
1.122 @@ -462,16 +465,15 @@
1.123 [Thm ("risolate_bdv_add",num_str @{thm risolate_bdv_add}),
1.124 Thm ("risolate_bdv_mult_add",num_str @{thm risolate_bdv_mult_add}),
1.125 Thm ("risolate_bdv_mult",num_str @{thm risolate_bdv_mult}),
1.126 - Thm ("mult_square",num_str @{mult_square}),
1.127 - Thm ("constant_square",num_str @{constant_square}),
1.128 - Thm ("constant_mult_square",num_str @{constant_mult_square})
1.129 + Thm ("mult_square",num_str @{thm mult_square}),
1.130 + Thm ("constant_square",num_str @{thm constant_square}),
1.131 + Thm ("constant_mult_square",num_str @{thm constant_mult_square})
1.132 ],
1.133 scr = Script ((term_of o the o (parse thy))
1.134 "empty_script")
1.135 }:rls;
1.136 -
1.137 -
1.138 -
1.139 +*}
1.140 +ML {*
1.141
1.142 (* association list for calculate_, calculate
1.143 "op +" etc. not usable in scripts *)
1.144 @@ -507,6 +509,8 @@
1.145 [Calc ("Tools.matches",eval_matches "#matches_")]))
1.146 ]);
1.147
1.148 +*}
1.149 +ML {*
1.150 (** problem types **)
1.151 store_pbt
1.152 (prep_pbt thy "pbl_test" [] e_pblID
1.153 @@ -537,8 +541,8 @@
1.154 (prep_pbt thy "pbl_test_uni_lin" [] e_pblID
1.155 (["linear","univariate","equation","test"],
1.156 [("#Given" ,["equality e_e","solveFor v_v"]),
1.157 - ("#Where" ,["(matches ( v_v = 0) e_e) | (matches ( ?b*v_ = 0) e_e) |" ^
1.158 - "(matches (?a+v_ = 0) e_e) | (matches (?a+?b*v_ = 0) e_e) "]),
1.159 + ("#Where" ,["(matches ( v_v = 0) e_e) | (matches ( ?b*v_v = 0) e_e) |" ^
1.160 + "(matches (?a+v_v = 0) e_e) | (matches (?a+?b*v_v = 0) e_e) "]),
1.161 ("#Find" ,["solutions v_i"])
1.162 ],
1.163 assoc_rls "matches",
1.164 @@ -548,7 +552,7 @@
1.165 store_pbt
1.166 (prep_pbt thy
1.167 (["thy"],
1.168 - [("#Given" ,"boolTestGiven g_"),
1.169 + [("#Given" ,"boolTestGiven g_g"),
1.170 ("#Find" ,"boolTestFind f_f")
1.171 ],
1.172 []));
1.173 @@ -556,7 +560,7 @@
1.174 store_pbt
1.175 (prep_pbt thy
1.176 (["testeq","thy"],
1.177 - [("#Given" ,"boolTestGiven g_"),
1.178 + [("#Given" ,"boolTestGiven g_g"),
1.179 ("#Find" ,"boolTestFind f_f")
1.180 ],
1.181 []));
1.182 @@ -566,7 +570,8 @@
1.183
1.184 ------ 25.8.01*)
1.185
1.186 -
1.187 +*}
1.188 +ML {*
1.189 (** methods **)
1.190 store_met
1.191 (prep_met (theory "Diff") "met_test" [] e_metID
1.192 @@ -583,6 +588,8 @@
1.193 {rew_ord'="e_rew_ord",rls'=tval_rls,srls=e_rls,prls=e_rls,calc=[],
1.194 asm_rls=[],asm_thm=[]},
1.195 "Undef"));*)
1.196 +*}
1.197 +ML {*
1.198 store_met
1.199 (prep_met thy "met_test_solvelin" [] e_metID
1.200 (["Test","solve_linear"]:metID,
1.201 @@ -590,27 +597,26 @@
1.202 ("#Where" ,["matches (?a = ?b) e_e"]),
1.203 ("#Find" ,["solutions v_i"])
1.204 ],
1.205 - {rew_ord'="e_rew_ord",rls'=tval_rls,srls=e_rls,
1.206 - prls=assoc_rls "matches",
1.207 - calc=[],
1.208 - crls=tval_rls, nrls=Test_simplify},
1.209 - "Script Solve_linear (e_e::bool) (v_v::real)= " ^
1.210 - "(let e_e =" ^
1.211 - " Repeat" ^
1.212 - " (((Rewrite_Set_Inst [(bdv,v_v::real)] isolate_bdv False) @@" ^
1.213 + {rew_ord' = "e_rew_ord", rls' = tval_rls, srls = e_rls,
1.214 + prls = assoc_rls "matches", calc = [], crls = tval_rls,
1.215 + nrls = Test_simplify},
1.216 + "Script Solve_linear (e_e::bool) (v_v::real)= " ^
1.217 + "(let e_e = " ^
1.218 + " Repeat " ^
1.219 + " (((Rewrite_Set_Inst [(bdv,v_v::real)] isolate_bdv False) @@ " ^
1.220 " (Rewrite_Set Test_simplify False))) e_e" ^
1.221 - " in [e_::bool])"
1.222 + " in [e_e::bool])"
1.223 )
1.224 (*, prep_met thy (*test for equations*)
1.225 (["Test","testeq"]:metID,
1.226 - [("#Given" ,["boolTestGiven g_"]),
1.227 + [("#Given" ,["boolTestGiven g_g"]),
1.228 ("#Find" ,["boolTestFind f_f"])
1.229 ],
1.230 {rew_ord'="e_rew_ord",rls'="tval_rls",asm_rls=[],
1.231 asm_thm=[("square_equation_left","")]},
1.232 - "Script Testeq (eq_::bool) = " ^
1.233 + "Script Testeq (e_q::bool) = " ^
1.234 "Repeat " ^
1.235 - " (let e_e = Try (Repeat (Rewrite rroot_square_inv False eq_)); " ^
1.236 + " (let e_e = Try (Repeat (Rewrite rroot_square_inv False e_q)); " ^
1.237 " e_e = Try (Repeat (Rewrite square_equation_left True e_e)); " ^
1.238 " e_e = Try (Repeat (Rewrite rmult_0 False e_e)) " ^
1.239 " in e_e) Until (is_root_free e_e)" (*deleted*)
1.240 @@ -618,8 +624,8 @@
1.241 , ---------27.4.02*)
1.242 );
1.243
1.244 -
1.245 -
1.246 +*}
1.247 +ML {*
1.248
1.249 ruleset' := overwritelthy @{theory} (!ruleset',
1.250 [("norm_equation", prep_rls norm_equation),
1.251 @@ -764,7 +770,8 @@
1.252 fun rational t div_op bdVar =
1.253 is_denom bdVar div_op t andalso bin_ops_only t;
1.254
1.255 -
1.256 +*}
1.257 +ML {*
1.258
1.259 (** problem types **)
1.260
1.261 @@ -772,8 +779,8 @@
1.262 (prep_pbt thy "pbl_test_uni_plain2" [] e_pblID
1.263 (["plain_square","univariate","equation","test"],
1.264 [("#Given" ,["equality e_e","solveFor v_v"]),
1.265 - ("#Where" ,["(matches (?a + ?b*v_ ^^^2 = 0) e_e) |" ^
1.266 - "(matches ( ?b*v_ ^^^2 = 0) e_e) |" ^
1.267 + ("#Where" ,["(matches (?a + ?b*v_v ^^^2 = 0) e_e) |" ^
1.268 + "(matches ( ?b*v_v ^^^2 = 0) e_e) |" ^
1.269 "(matches (?a + v_v ^^^2 = 0) e_e) |" ^
1.270 "(matches ( v_v ^^^2 = 0) e_e)"]),
1.271 ("#Find" ,["solutions v_i"])
1.272 @@ -781,13 +788,13 @@
1.273 assoc_rls "matches",
1.274 SOME "solve (e_e::bool, v_v)", [["Test","solve_plain_square"]]));
1.275 (*
1.276 - val e_e = (term_of o the o (parse thy)) "e_::bool";
1.277 + val e_e = (term_of o the o (parse thy)) "e_e::bool";
1.278 val ve = (term_of o the o (parse thy)) "4 + 3*x^^^2 = 0";
1.279 val env = [(e_,ve)];
1.280
1.281 val pre = (term_of o the o (parse thy))
1.282 - "(matches (a + b*v_ ^^^2 = 0, e_e::bool)) |" ^
1.283 - "(matches ( b*v_ ^^^2 = 0, e_e::bool)) |" ^
1.284 + "(matches (a + b*v_v ^^^2 = 0, e_e::bool)) |" ^
1.285 + "(matches ( b*v_v ^^^2 = 0, e_e::bool)) |" ^
1.286 "(matches (a + v_v ^^^2 = 0, e_e::bool)) |" ^
1.287 "(matches ( v_v ^^^2 = 0, e_e::bool))";
1.288 val prei = subst_atomic env pre;
1.289 @@ -803,10 +810,12 @@
1.290
1.291 *)
1.292
1.293 +*}
1.294 +ML {*
1.295 store_pbt
1.296 (prep_pbt thy "pbl_test_uni_poly" [] e_pblID
1.297 (["polynomial","univariate","equation","test"],
1.298 - [("#Given" ,["equality (v_ ^^^2 + p_ * v_v + q__ = 0)","solveFor v_v"]),
1.299 + [("#Given" ,["equality (v_v ^^^2 + p_p * v_v + q__q = 0)","solveFor v_v"]),
1.300 ("#Where" ,["False"]),
1.301 ("#Find" ,["solutions v_i"])
1.302 ],
1.303 @@ -815,27 +824,29 @@
1.304 store_pbt
1.305 (prep_pbt thy "pbl_test_uni_poly_deg2" [] e_pblID
1.306 (["degree_two","polynomial","univariate","equation","test"],
1.307 - [("#Given" ,["equality (v_ ^^^2 + p_ * v_v + q__ = 0)","solveFor v_v"]),
1.308 + [("#Given" ,["equality (v_v ^^^2 + p_p * v_v + q__q = 0)","solveFor v_v"]),
1.309 ("#Find" ,["solutions v_i"])
1.310 ],
1.311 - e_rls, SOME "solve (v_ ^^^2 + p_ * v_v + q__ = 0, v_v)", []));
1.312 + e_rls, SOME "solve (v_v ^^^2 + p_p * v_v + q__q = 0, v_v)", []));
1.313
1.314 store_pbt
1.315 (prep_pbt thy "pbl_test_uni_poly_deg2_pq" [] e_pblID
1.316 (["pq_formula","degree_two","polynomial","univariate","equation","test"],
1.317 - [("#Given" ,["equality (v_ ^^^2 + p_ * v_v + q__ = 0)","solveFor v_v"]),
1.318 + [("#Given" ,["equality (v_v ^^^2 + p_p * v_v + q__q = 0)","solveFor v_v"]),
1.319 ("#Find" ,["solutions v_i"])
1.320 ],
1.321 - e_rls, SOME "solve (v_ ^^^2 + p_ * v_v + q__ = 0, v_v)", []));
1.322 + e_rls, SOME "solve (v_v ^^^2 + p_p * v_v + q__q = 0, v_v)", []));
1.323
1.324 store_pbt
1.325 (prep_pbt thy "pbl_test_uni_poly_deg2_abc" [] e_pblID
1.326 (["abc_formula","degree_two","polynomial","univariate","equation","test"],
1.327 - [("#Given" ,["equality (a_ * x ^^^2 + b_ * x + c_ = 0)","solveFor v_v"]),
1.328 + [("#Given" ,["equality (a_a * x ^^^2 + b_b * x + c_c = 0)","solveFor v_v"]),
1.329 ("#Find" ,["solutions v_i"])
1.330 ],
1.331 - e_rls, SOME "solve (a_ * x ^^^2 + b_ * x + c_ = 0, v_v)", []));
1.332 + e_rls, SOME "solve (a_a * x ^^^2 + b_b * x + c_c = 0, v_v)", []));
1.333
1.334 +*}
1.335 +ML {*
1.336 store_pbt
1.337 (prep_pbt thy "pbl_test_uni_root" [] e_pblID
1.338 (["squareroot","univariate","equation","test"],
1.339 @@ -868,6 +879,8 @@
1.340 (*
1.341 (#ppc o get_pbt) ["sqroot-test","univariate","equation"];
1.342 *)
1.343 +*}
1.344 +ML {*
1.345
1.346
1.347 store_met
1.348 @@ -900,9 +913,11 @@
1.349 " (Rewrite_Set_Inst [(bdv,v_v::real)] isolate_bdv False) @@" ^
1.350 " (Try (Rewrite_Set Test_simplify False)))" ^
1.351 " e_e" ^
1.352 - " in [e_::bool])"
1.353 + " in [e_e::bool])"
1.354 ));
1.355
1.356 +*}
1.357 +ML {*
1.358 store_met
1.359 (prep_met thy "met_test_sqrt2" [] e_metID
1.360 (*root-equation ... for test-*.sml until 8.01*)
1.361 @@ -930,11 +945,13 @@
1.362 " (Rewrite_Set_Inst [(bdv,v_v::real)] isolate_bdv False) @@" ^
1.363 " (Try (Rewrite_Set Test_simplify False)))" ^
1.364 " e_e;" ^
1.365 - " (L_::bool list) = Tac subproblem_equation_dummy; " ^
1.366 + " (L_L::bool list) = Tac subproblem_equation_dummy; " ^
1.367 " L_L = Tac solve_equation_dummy " ^
1.368 " in Check_elementwise L_L {(v_v::real). Assumptions})"
1.369 ));
1.370
1.371 +*}
1.372 +ML {*
1.373 store_met
1.374 (prep_met thy "met_test_squ_sub" [] e_metID
1.375 (*tests subproblem fixed linear*)
1.376 @@ -944,14 +961,18 @@
1.377 ],
1.378 {rew_ord'="e_rew_ord",rls'=tval_rls,srls=e_rls,prls=e_rls,calc=[],
1.379 crls=tval_rls, nrls=Test_simplify},
1.380 - "Script Solve_root_equation (e_e::bool) (v_v::real) = " ^
1.381 - " (let e_e = ((Try (Rewrite_Set norm_equation False)) @@ " ^
1.382 - " (Try (Rewrite_Set Test_simplify False))) e_e; " ^
1.383 - "(L_::bool list) = (SubProblem (Test_,[linear,univariate,equation,test]," ^
1.384 - " [Test,solve_linear]) [BOOL e_e, REAL v_])" ^
1.385 + "Script Solve_root_equation (e_e::bool) (v_v::real) = " ^
1.386 + " (let e_e = ((Try (Rewrite_Set norm_equation False)) @@ " ^
1.387 + " (Try (Rewrite_Set Test_simplify False))) e_e; " ^
1.388 + "(L_L::bool list) = (SubProblem (Test', " ^
1.389 + " [linear,univariate,equation,test], " ^
1.390 + " [Test,solve_linear])" ^
1.391 + " [BOOL e_e, REAL v_v])" ^
1.392 "in Check_elementwise L_L {(v_v::real). Assumptions})"
1.393 ));
1.394
1.395 +*}
1.396 +ML {*
1.397 store_met
1.398 (prep_met thy "met_test_squ_sub2" [] e_metID
1.399 (*tests subproblem fixed degree 2*)
1.400 @@ -965,11 +986,13 @@
1.401 ("square_equation_right","")]*)},
1.402 "Script Solve_root_equation (e_e::bool) (v_v::real) = " ^
1.403 " (let e_e = Try (Rewrite_Set norm_equation False) e_e; " ^
1.404 - "(L_::bool list) = (SubProblem (Test_,[linear,univariate,equation,test]," ^
1.405 - " [Test,solve_by_pq_formula]) [BOOL e_e, REAL v_])" ^
1.406 + "(L_L::bool list) = (SubProblem (Test',[linear,univariate,equation,test]," ^
1.407 + " [Test,solve_by_pq_formula]) [BOOL e_e, REAL v_v])" ^
1.408 "in Check_elementwise L_L {(v_v::real). Assumptions})"
1.409 ));
1.410
1.411 +*}
1.412 +ML {*
1.413 store_met
1.414 (prep_met thy "met_test_squ_nonterm" [] e_metID
1.415 (*root-equation: see foils..., but notTerminating*)
1.416 @@ -995,12 +1018,14 @@
1.417 " (Try (Rewrite_Set norm_equation False)) @@" ^
1.418 " (Try (Rewrite_Set Test_simplify False)))" ^
1.419 " e_e;" ^
1.420 - " (L_::bool list) = " ^
1.421 - " (SubProblem (Test_,[linear,univariate,equation,test]," ^
1.422 - " [Test,solve_linear]) [BOOL e_e, REAL v_])" ^
1.423 + " (L_L::bool list) = " ^
1.424 + " (SubProblem (Test',[linear,univariate,equation,test]," ^
1.425 + " [Test,solve_linear]) [BOOL e_e, REAL v_v])" ^
1.426 "in Check_elementwise L_L {(v_v::real). Assumptions})"
1.427 ));
1.428
1.429 +*}
1.430 +ML {*
1.431 store_met
1.432 (prep_met thy "met_test_eq1" [] e_metID
1.433 (*root-equation1:*)
1.434 @@ -1026,11 +1051,13 @@
1.435 " (Try (Rewrite_Set norm_equation False)) @@" ^
1.436 " (Try (Rewrite_Set Test_simplify False)))" ^
1.437 " e_e;" ^
1.438 - " (L_::bool list) = (SubProblem (Test_,[linear,univariate,equation,test]," ^
1.439 - " [Test,solve_linear]) [BOOL e_e, REAL v_])" ^
1.440 + " (L_L::bool list) = (SubProblem (Test',[linear,univariate,equation,test]," ^
1.441 + " [Test,solve_linear]) [BOOL e_e, REAL v_v])" ^
1.442 " in Check_elementwise L_L {(v_v::real). Assumptions})"
1.443 ));
1.444
1.445 +*}
1.446 +ML {*
1.447 store_met
1.448 (prep_met thy "met_test_squ2" [] e_metID
1.449 (*root-equation2*)
1.450 @@ -1057,11 +1084,13 @@
1.451 " (Try (Rewrite_Set norm_equation False)) @@" ^
1.452 " (Try (Rewrite_Set Test_simplify False)))" ^
1.453 " e_e;" ^
1.454 - " (L_::bool list) = (SubProblem (Test_,[plain_square,univariate,equation,test]," ^
1.455 - " [Test,solve_plain_square]) [BOOL e_e, REAL v_])" ^
1.456 + " (L_L::bool list) = (SubProblem (Test',[plain_square,univariate,equation,test]," ^
1.457 + " [Test,solve_plain_square]) [BOOL e_e, REAL v_v])" ^
1.458 " in Check_elementwise L_L {(v_v::real). Assumptions})"
1.459 ));
1.460
1.461 +*}
1.462 +ML {*
1.463 store_met
1.464 (prep_met thy "met_test_squeq" [] e_metID
1.465 (*root-equation*)
1.466 @@ -1088,18 +1117,20 @@
1.467 " (Try (Rewrite_Set norm_equation False)) @@" ^
1.468 " (Try (Rewrite_Set Test_simplify False)))" ^
1.469 " e_e;" ^
1.470 - " (L_::bool list) = (SubProblem (Test_,[univariate,equation,test]," ^
1.471 - " [no_met]) [BOOL e_e, REAL v_])" ^
1.472 + " (L_L::bool list) = (SubProblem (Test',[univariate,equation,test]," ^
1.473 + " [no_met]) [BOOL e_e, REAL v_v])" ^
1.474 " in Check_elementwise L_L {(v_v::real). Assumptions})"
1.475 ) ); (*#######*)
1.476
1.477 +*}
1.478 +ML {*
1.479 store_met
1.480 (prep_met thy "met_test_eq_plain" [] e_metID
1.481 (*solve_plain_square*)
1.482 (["Test","solve_plain_square"]:metID,
1.483 [("#Given",["equality e_e","solveFor v_v"]),
1.484 - ("#Where" ,["(matches (?a + ?b*v_ ^^^2 = 0) e_e) |" ^
1.485 - "(matches ( ?b*v_ ^^^2 = 0) e_e) |" ^
1.486 + ("#Where" ,["(matches (?a + ?b*v_v ^^^2 = 0) e_e) |" ^
1.487 + "(matches ( ?b*v_v ^^^2 = 0) e_e) |" ^
1.488 "(matches (?a + v_v ^^^2 = 0) e_e) |" ^
1.489 "(matches ( v_v ^^^2 = 0) e_e)"]),
1.490 ("#Find" ,["solutions v_i"])
1.491 @@ -1117,6 +1148,8 @@
1.492 " in ((Or_to_List e_e)::bool list))"
1.493 ));
1.494
1.495 +*}
1.496 +ML {*
1.497 store_met
1.498 (prep_met thy "met_test_norm_univ" [] e_metID
1.499 (["Test","norm_univar_equation"]:metID,
1.500 @@ -1130,13 +1163,15 @@
1.501 "Script Norm_univar_equation (e_e::bool) (v_v::real) = " ^
1.502 " (let e_e = ((Try (Rewrite rnorm_equation_add False)) @@ " ^
1.503 " (Try (Rewrite_Set Test_simplify False))) e_e " ^
1.504 - " in (SubProblem (Test_,[univariate,equation,test], " ^
1.505 - " [no_met]) [BOOL e_e, REAL v_]))"
1.506 + " in (SubProblem (Test',[univariate,equation,test], " ^
1.507 + " [no_met]) [BOOL e_e, REAL v_v]))"
1.508 ));
1.509
1.510
1.511
1.512 (*17.9.02 aus SqRoot.ML------------------------------^^^---*)
1.513 +*}
1.514 +ML {*
1.515
1.516 (*8.4.03 aus Poly.ML--------------------------------vvv---
1.517 make_polynomial ---> make_poly
1.518 @@ -1171,18 +1206,18 @@
1.519 | size_of_term' (f$t) = size_of_term' f + size_of_term' t
1.520 | size_of_term' _ = 1;
1.521
1.522 -fun Term_Ord.term_ord' pr thy (Abs (_, T, t), Abs(_, U, u)) = (* ~ term.ML *)
1.523 - (case Term_Ord.term_ord' pr thy (t, u) of EQUAL => Term_Ord.typ_ord (T, U) | ord => ord)
1.524 - | Term_Ord.term_ord' pr thy (t, u) =
1.525 +fun term_ord' pr thy (Abs (_, T, t), Abs(_, U, u)) = (* ~ term.ML *)
1.526 + (case term_ord' pr thy (t, u) of EQUAL => Term_Ord.typ_ord (T, U) | ord => ord)
1.527 + | term_ord' pr thy (t, u) =
1.528 (if pr then
1.529 let
1.530 val (f, ts) = strip_comb t and (g, us) = strip_comb u;
1.531 val _=writeln("t= f@ts= " ^ "" ^
1.532 ((Syntax.string_of_term (thy2ctxt thy)) f)^ "\" @ " ^ "[" ^
1.533 - (commas(map(Syntax.string_of_term (thy2ctxt thy)) ts)) ^ "]""");
1.534 + (commas(map(Syntax.string_of_term (thy2ctxt thy)) ts)) ^ "]\"");
1.535 val _=writeln("u= g@us= " ^ "" ^
1.536 ((Syntax.string_of_term (thy2ctxt thy)) g) ^ "\" @ " ^ "[" ^
1.537 - (commas(map(Syntax.string_of_term (thy2ctxt thy)) us))^"]""");
1.538 + (commas(map(Syntax.string_of_term (thy2ctxt thy)) us))^"]\"");
1.539 val _=writeln("size_of_term(t,u)= ("^
1.540 (string_of_int(size_of_term' t)) ^ ", " ^
1.541 (string_of_int(size_of_term' u)) ^ ")");
1.542 @@ -1209,6 +1244,8 @@
1.543 (term_ord' pr thy(***) tu = LESS );
1.544
1.545 end;(*local*)
1.546 +*}
1.547 +ML {*
1.548
1.549 rew_ord' := overwritel (!rew_ord',
1.550 [("termlessI", termlessI),
1.551 @@ -1217,7 +1254,7 @@
1.552
1.553 (*WN060510 this was a preparation for prep_rls ...
1.554 val scr_make_polytest =
1.555 -"Script Expand_binomtest t_ =" ^
1.556 +"Script Expand_binomtest t_t =" ^
1.557 "(Repeat " ^
1.558 "((Try (Repeat (Rewrite real_diff_minus False))) @@ " ^
1.559
1.560 @@ -1251,7 +1288,7 @@
1.561 " (Try (Repeat (Calculate PLUS ))) @@ " ^
1.562 " (Try (Repeat (Calculate TIMES ))) @@ " ^
1.563 " (Try (Repeat (Calculate POWER)))) " ^
1.564 -" t_)";
1.565 +" t_t)";
1.566 -----------------------------------------------------*)
1.567
1.568 val make_polytest =
1.569 @@ -1321,10 +1358,12 @@
1.570 ],
1.571 scr = EmptyScr(*Script ((term_of o the o (parse thy))
1.572 scr_make_polytest)*)
1.573 - }:rls;
1.574 -(*WN060510 this was done before 'fun prep_rls' ...
1.575 + }:rls;
1.576 +*}
1.577 +ML {*
1.578 +(*WN060510 this was done before 'fun prep_rls' ...------------------------
1.579 val scr_expand_binomtest =
1.580 -"Script Expand_binomtest t_ =" ^
1.581 +"Script Expand_binomtest t_t =" ^
1.582 "(Repeat " ^
1.583 "((Try (Repeat (Rewrite real_plus_binom_pow2 False))) @@ " ^
1.584 " (Try (Repeat (Rewrite real_plus_binom_times False))) @@ " ^
1.585 @@ -1355,8 +1394,8 @@
1.586 " (Try (Repeat (Calculate PLUS ))) @@ " ^
1.587 " (Try (Repeat (Calculate TIMES ))) @@ " ^
1.588 " (Try (Repeat (Calculate POWER)))) " ^
1.589 -" t_)";
1.590 -------------------------------------------------------*)
1.591 +" t_t)";
1.592 +--------------------------------------------------------------------------*)
1.593
1.594 val expand_binomtest =
1.595 Rls{id = "expand_binomtest", preconds = [],
1.596 @@ -1366,85 +1405,90 @@
1.597 ("TIMES" , ("op *", eval_binop "#mult_")),
1.598 ("POWER", ("Atools.pow", eval_binop "#power_"))
1.599 ],
1.600 - rules = [Thm ("real_plus_binom_pow2" ,num_str @{thm real_plus_binom_pow2}),
1.601 + rules =
1.602 + [Thm ("real_plus_binom_pow2" ,num_str @{thm real_plus_binom_pow2}),
1.603 (*"(a + b) ^^^ 2 = a ^^^ 2 + 2 * a * b + b ^^^ 2"*)
1.604 - Thm ("real_plus_binom_times" ,num_str @{thm real_plus_binom_times}),
1.605 + Thm ("real_plus_binom_times" ,num_str @{thm real_plus_binom_times}),
1.606 (*"(a + b)*(a + b) = ...*)
1.607 - Thm ("real_minus_binom_pow2" ,num_str @{thm real_minus_binom_pow2}),
1.608 - (*"(a - b) ^^^ 2 = a ^^^ 2 - 2 * a * b + b ^^^ 2"*)
1.609 - Thm ("real_minus_binom_times",num_str @{thm real_minus_binom_times}),
1.610 - (*"(a - b)*(a - b) = ...*)
1.611 - Thm ("real_plus_minus_binom1",num_str @{thm real_plus_minus_binom1}),
1.612 - (*"(a + b) * (a - b) = a ^^^ 2 - b ^^^ 2"*)
1.613 - Thm ("real_plus_minus_binom2",num_str @{thm real_plus_minus_binom2}),
1.614 - (*"(a - b) * (a + b) = a ^^^ 2 - b ^^^ 2"*)
1.615 - (*RL 020915*)
1.616 - Thm ("real_pp_binom_times",num_str @{thm real_pp_binom_times}),
1.617 - (*(a + b)*(c + d) = a*c + a*d + b*c + b*d*)
1.618 - Thm ("real_pm_binom_times",num_str @{thm real_pm_binom_times}),
1.619 - (*(a + b)*(c - d) = a*c - a*d + b*c - b*d*)
1.620 - Thm ("real_mp_binom_times",num_str @{thm real_mp_binom_times}),
1.621 - (*(a - b)*(c p d) = a*c + a*d - b*c - b*d*)
1.622 - Thm ("real_mm_binom_times",num_str @{thm real_mm_binom_times}),
1.623 - (*(a - b)*(c p d) = a*c - a*d - b*c + b*d*)
1.624 - Thm ("realpow_multI",num_str @{thm realpow_multI}),
1.625 - (*(a*b)^^^n = a^^^n * b^^^n*)
1.626 - Thm ("real_plus_binom_pow3",num_str @{thm real_plus_binom_pow3}),
1.627 - (* (a + b)^^^3 = a^^^3 + 3*a^^^2*b + 3*a*b^^^2 + b^^^3 *)
1.628 - Thm ("real_minus_binom_pow3",num_str @{thm real_minus_binom_pow3}),
1.629 - (* (a - b)^^^3 = a^^^3 - 3*a^^^2*b + 3*a*b^^^2 - b^^^3 *)
1.630 + Thm ("real_minus_binom_pow2" ,num_str @{thm real_minus_binom_pow2}),
1.631 + (*"(a - b) ^^^ 2 = a ^^^ 2 - 2 * a * b + b ^^^ 2"*)
1.632 + Thm ("real_minus_binom_times",num_str @{thm real_minus_binom_times}),
1.633 + (*"(a - b)*(a - b) = ...*)
1.634 + Thm ("real_plus_minus_binom1",num_str @{thm real_plus_minus_binom1}),
1.635 + (*"(a + b) * (a - b) = a ^^^ 2 - b ^^^ 2"*)
1.636 + Thm ("real_plus_minus_binom2",num_str @{thm real_plus_minus_binom2}),
1.637 + (*"(a - b) * (a + b) = a ^^^ 2 - b ^^^ 2"*)
1.638 + (*RL 020915*)
1.639 + Thm ("real_pp_binom_times",num_str @{thm real_pp_binom_times}),
1.640 + (*(a + b)*(c + d) = a*c + a*d + b*c + b*d*)
1.641 + Thm ("real_pm_binom_times",num_str @{thm real_pm_binom_times}),
1.642 + (*(a + b)*(c - d) = a*c - a*d + b*c - b*d*)
1.643 + Thm ("real_mp_binom_times",num_str @{thm real_mp_binom_times}),
1.644 + (*(a - b)*(c p d) = a*c + a*d - b*c - b*d*)
1.645 + Thm ("real_mm_binom_times",num_str @{thm real_mm_binom_times}),
1.646 + (*(a - b)*(c p d) = a*c - a*d - b*c + b*d*)
1.647 + Thm ("realpow_multI",num_str @{thm realpow_multI}),
1.648 + (*(a*b)^^^n = a^^^n * b^^^n*)
1.649 + Thm ("real_plus_binom_pow3",num_str @{thm real_plus_binom_pow3}),
1.650 + (* (a + b)^^^3 = a^^^3 + 3*a^^^2*b + 3*a*b^^^2 + b^^^3 *)
1.651 + Thm ("real_minus_binom_pow3",num_str @{thm real_minus_binom_pow3}),
1.652 + (* (a - b)^^^3 = a^^^3 - 3*a^^^2*b + 3*a*b^^^2 - b^^^3 *)
1.653
1.654
1.655 - (* Thm ("left_distrib" ,num_str @{thm left_distrib}}),
1.656 - (*"(z1.0 + z2.0) * w = z1.0 * w + z2.0 * w"*)
1.657 - Thm ("right_distrib",num_str @{thm right_distrib}),
1.658 - (*"w * (z1.0 + z2.0) = w * z1.0 + w * z2.0"*)
1.659 - Thm ("left_diff_distrib" ,num_str @{thm left_diff_distrib}}),
1.660 - (*"(z1.0 - z2.0) * w = z1.0 * w - z2.0 * w"*)
1.661 - Thm ("right_diff_distrib",num_str @{thm right_diff_distrib}),
1.662 - (*"w * (z1.0 - z2.0) = w * z1.0 - w * z2.0"*)
1.663 - *)
1.664 -
1.665 - Thm ("mult_1_left",num_str @{thm mult_1_left}}), (*"1 * z = z"*)
1.666 - Thm ("mult_zero_left",num_str @{thm mult_zero_left}}), (*"0 * z = 0"*)
1.667 - Thm ("add_0_left",num_str @{thm add_0_left}}),(*"0 + z = z"*)
1.668 + (* Thm ("left_distrib" ,num_str @{thm left_distrib}),
1.669 + (*"(z1.0 + z2.0) * w = z1.0 * w + z2.0 * w"*)
1.670 + Thm ("right_distrib",num_str @{thm right_distrib}),
1.671 + (*"w * (z1.0 + z2.0) = w * z1.0 + w * z2.0"*)
1.672 + Thm ("left_diff_distrib" ,num_str @{thm left_diff_distrib}),
1.673 + (*"(z1.0 - z2.0) * w = z1.0 * w - z2.0 * w"*)
1.674 + Thm ("right_diff_distrib",num_str @{thm right_diff_distrib}),
1.675 + (*"w * (z1.0 - z2.0) = w * z1.0 - w * z2.0"*)
1.676 + *)
1.677 +
1.678 + Thm ("mult_1_left",num_str @{thm mult_1_left}),
1.679 + (*"1 * z = z"*)
1.680 + Thm ("mult_zero_left",num_str @{thm mult_zero_left}),
1.681 + (*"0 * z = 0"*)
1.682 + Thm ("add_0_left",num_str @{thm add_0_left}),
1.683 + (*"0 + z = z"*)
1.684
1.685 - Calc ("op +", eval_binop "#add_"),
1.686 - Calc ("op *", eval_binop "#mult_"),
1.687 - Calc ("Atools.pow", eval_binop "#power_"),
1.688 - (*
1.689 - Thm ("real_mult_commute",num_str @{thm real_mult_commute}), (*AC-rewriting*)
1.690 - Thm ("real_mult_left_commute",num_str @{thm real_mult_left_commute}), (**)
1.691 - Thm ("real_mult_assoc",num_str @{thm real_mult_assoc}), (**)
1.692 - Thm ("add_commute",num_str @{thm add_commute}), (**)
1.693 - Thm ("add_left_commute",num_str @{thm add_left_commute}), (**)
1.694 - Thm ("add_assoc",num_str @{thm add_assoc}), (**)
1.695 - *)
1.696 -
1.697 - Thm ("sym_realpow_twoI",
1.698 - num_str (@{thm realpow_twoI} RS @{thm sym})),
1.699 - (*"r1 * r1 = r1 ^^^ 2"*)
1.700 - Thm ("realpow_plus_1",num_str @{thm realpow_plus_1}),
1.701 - (*"r * r ^^^ n = r ^^^ (n + 1)"*)
1.702 - (*Thm ("sym_real_mult_2",
1.703 - num_str (@{thm real_mult_2} RS @{thm sym})),
1.704 - (*"z1 + z1 = 2 * z1"*)*)
1.705 - Thm ("real_mult_2_assoc",num_str @{thm real_mult_2_assoc}),
1.706 - (*"z1 + (z1 + k) = 2 * z1 + k"*)
1.707 + Calc ("op +", eval_binop "#add_"),
1.708 + Calc ("op *", eval_binop "#mult_"),
1.709 + Calc ("Atools.pow", eval_binop "#power_"),
1.710 + (*
1.711 + Thm ("real_mult_commute",num_str @{thm real_mult_commute}),
1.712 + (*AC-rewriting*)
1.713 + Thm ("real_mult_left_commute",num_str @{thm real_mult_left_commute}),
1.714 + Thm ("real_mult_assoc",num_str @{thm real_mult_assoc}),
1.715 + Thm ("add_commute",num_str @{thm add_commute}),
1.716 + Thm ("add_left_commute",num_str @{thm add_left_commute}),
1.717 + Thm ("add_assoc",num_str @{thm add_assoc}),
1.718 + *)
1.719 +
1.720 + Thm ("sym_realpow_twoI",
1.721 + num_str (@{thm realpow_twoI} RS @{thm sym})),
1.722 + (*"r1 * r1 = r1 ^^^ 2"*)
1.723 + Thm ("realpow_plus_1",num_str @{thm realpow_plus_1}),
1.724 + (*"r * r ^^^ n = r ^^^ (n + 1)"*)
1.725 + (*Thm ("sym_real_mult_2",
1.726 + num_str (@{thm real_mult_2} RS @{thm sym})),
1.727 + (*"z1 + z1 = 2 * z1"*)*)
1.728 + Thm ("real_mult_2_assoc",num_str @{thm real_mult_2_assoc}),
1.729 + (*"z1 + (z1 + k) = 2 * z1 + k"*)
1.730
1.731 - Thm ("real_num_collect",num_str @{thm real_num_collect}),
1.732 - (*"[| l is_const; m is_const |] ==> l * n + m * n = (l + m) * n"*)
1.733 - Thm ("real_num_collect_assoc",num_str @{thm real_num_collect_assoc}),
1.734 - (*"[| l is_const; m is_const |] ==> l * n + (m * n + k) = (l + m) * n + k"*)
1.735 - Thm ("real_one_collect",num_str @{thm real_one_collect}),
1.736 - (*"m is_const ==> n + m * n = (1 + m) * n"*)
1.737 - Thm ("real_one_collect_assoc",num_str @{thm real_one_collect_assoc}),
1.738 - (*"m is_const ==> k + (n + m * n) = k + (1 + m) * n"*)
1.739 + Thm ("real_num_collect",num_str @{thm real_num_collect}),
1.740 + (*"[| l is_const; m is_const |] ==> l * n + m * n = (l + m) * n"*)
1.741 + Thm ("real_num_collect_assoc",num_str @{thm real_num_collect_assoc}),
1.742 + (*"[| l is_const; m is_const |] ==> l * n + (m * n + k) = (l + m) * n + k"*)
1.743 + Thm ("real_one_collect",num_str @{thm real_one_collect}),
1.744 + (*"m is_const ==> n + m * n = (1 + m) * n"*)
1.745 + Thm ("real_one_collect_assoc",num_str @{thm real_one_collect_assoc}),
1.746 + (*"m is_const ==> k + (n + m * n) = k + (1 + m) * n"*)
1.747
1.748 - Calc ("op +", eval_binop "#add_"),
1.749 - Calc ("op *", eval_binop "#mult_"),
1.750 - Calc ("Atools.pow", eval_binop "#power_")
1.751 - ],
1.752 + Calc ("op +", eval_binop "#add_"),
1.753 + Calc ("op *", eval_binop "#mult_"),
1.754 + Calc ("Atools.pow", eval_binop "#power_")
1.755 + ],
1.756 scr = EmptyScr
1.757 (*Script ((term_of o the o (parse thy)) scr_expand_binomtest)*)
1.758 }:rls;