293 |
293 |
294 Calc ("Atools.ident",eval_ident "#ident_")], |
294 Calc ("Atools.ident",eval_ident "#ident_")], |
295 scr = Prog ((term_of o the o (parse thy)) "empty_script") |
295 scr = Prog ((term_of o the o (parse thy)) "empty_script") |
296 }:rls; |
296 }:rls; |
297 *} |
297 *} |
298 setup {* KEStore_Elems.add_rlss [("testerls", (Context.theory_name @{theory}, prep_rls testerls))] *} |
298 setup {* KEStore_Elems.add_rlss [("testerls", (Context.theory_name @{theory}, prep_rls' testerls))] *} |
299 |
299 |
300 ML {* |
300 ML {* |
301 (*make () dissappear*) |
301 (*make () dissappear*) |
302 val rearrange_assoc = |
302 val rearrange_assoc = |
303 Rls{id = "rearrange_assoc", preconds = [], |
303 Rls{id = "rearrange_assoc", preconds = [], |
386 (* expects * distributed over + *) |
386 (* expects * distributed over + *) |
387 val Test_simplify = |
387 val Test_simplify = |
388 Rls{id = "Test_simplify", preconds = [], |
388 Rls{id = "Test_simplify", preconds = [], |
389 rew_ord = ("sqrt_right",sqrt_right false @{theory "Pure"}), |
389 rew_ord = ("sqrt_right",sqrt_right false @{theory "Pure"}), |
390 erls = tval_rls, srls = e_rls, |
390 erls = tval_rls, srls = e_rls, |
391 calc=[(*since 040209 filled by prep_rls*)], errpatts = [], |
391 calc=[(*since 040209 filled by prep_rls'*)], errpatts = [], |
392 rules = [ |
392 rules = [ |
393 Thm ("real_diff_minus",num_str @{thm real_diff_minus}), |
393 Thm ("real_diff_minus",num_str @{thm real_diff_minus}), |
394 Thm ("radd_mult_distrib2",num_str @{thm radd_mult_distrib2}), |
394 Thm ("radd_mult_distrib2",num_str @{thm radd_mult_distrib2}), |
395 Thm ("rdistr_right_assoc",num_str @{thm rdistr_right_assoc}), |
395 Thm ("rdistr_right_assoc",num_str @{thm rdistr_right_assoc}), |
396 Thm ("rdistr_right_assoc_p",num_str @{thm rdistr_right_assoc_p}), |
396 Thm ("rdistr_right_assoc_p",num_str @{thm rdistr_right_assoc_p}), |
434 Thm ("rmult_0_right",num_str @{thm rmult_0_right}), |
434 Thm ("rmult_0_right",num_str @{thm rmult_0_right}), |
435 Thm ("radd_0",num_str @{thm radd_0}), |
435 Thm ("radd_0",num_str @{thm radd_0}), |
436 Thm ("radd_0_right",num_str @{thm radd_0_right}) |
436 Thm ("radd_0_right",num_str @{thm radd_0_right}) |
437 ], |
437 ], |
438 scr = Prog ((term_of o the o (parse thy)) "empty_script") |
438 scr = Prog ((term_of o the o (parse thy)) "empty_script") |
439 (*since 040209 filled by prep_rls: STest_simplify*) |
439 (*since 040209 filled by prep_rls': STest_simplify*) |
440 }:rls; |
440 }:rls; |
441 *} |
441 *} |
442 ML {* |
442 ML {* |
443 |
443 |
444 (** rule sets **) |
444 (** rule sets **) |
499 ("Test.is_root_free",("is'_root'_free", eval_root_free"#is_root_free_e")), |
499 ("Test.is_root_free",("is'_root'_free", eval_root_free"#is_root_free_e")), |
500 ("Test.contains_root",("contains'_root", |
500 ("Test.contains_root",("contains'_root", |
501 eval_contains_root"#contains_root_")) |
501 eval_contains_root"#contains_root_")) |
502 ]; |
502 ]; |
503 *} |
503 *} |
|
504 ML {* val prep_rls' = prep_rls @{theory}; *} |
504 setup {* KEStore_Elems.add_rlss |
505 setup {* KEStore_Elems.add_rlss |
505 [("Test_simplify", (Context.theory_name @{theory}, prep_rls Test_simplify)), |
506 [("Test_simplify", (Context.theory_name @{theory}, prep_rls' Test_simplify)), |
506 ("tval_rls", (Context.theory_name @{theory}, prep_rls tval_rls)), |
507 ("tval_rls", (Context.theory_name @{theory}, prep_rls' tval_rls)), |
507 ("isolate_root", (Context.theory_name @{theory}, prep_rls isolate_root)), |
508 ("isolate_root", (Context.theory_name @{theory}, prep_rls' isolate_root)), |
508 ("isolate_bdv", (Context.theory_name @{theory}, prep_rls isolate_bdv)), |
509 ("isolate_bdv", (Context.theory_name @{theory}, prep_rls' isolate_bdv)), |
509 ("matches", (Context.theory_name @{theory}, prep_rls |
510 ("matches", (Context.theory_name @{theory}, prep_rls' |
510 (append_rls "matches" testerls [Calc ("Tools.matches",eval_matches "#matches_")])))] *} |
511 (append_rls "matches" testerls [Calc ("Tools.matches",eval_matches "#matches_")])))] *} |
511 |
512 |
512 (** problem types **) |
513 (** problem types **) |
513 setup {* KEStore_Elems.add_pbts |
514 setup {* KEStore_Elems.add_pbts |
514 [(prep_pbt thy "pbl_test" [] e_pblID (["test"], [], e_rls, NONE, [])), |
515 [(prep_pbt thy "pbl_test" [] e_pblID (["test"], [], e_rls, NONE, [])), |
578 " e_e = Try (Repeat (Rewrite rmult_0 False e_e)) " ^ |
579 " e_e = Try (Repeat (Rewrite rmult_0 False e_e)) " ^ |
579 " in e_e) Until (is_root_free e_e)" (*deleted*)) ---------27.4.02*)] |
580 " in e_e) Until (is_root_free e_e)" (*deleted*)) ---------27.4.02*)] |
580 *} |
581 *} |
581 |
582 |
582 setup {* KEStore_Elems.add_rlss |
583 setup {* KEStore_Elems.add_rlss |
583 [("norm_equation", (Context.theory_name @{theory}, prep_rls norm_equation)), |
584 [("norm_equation", (Context.theory_name @{theory}, prep_rls' norm_equation)), |
584 ("ac_plus_times", (Context.theory_name @{theory}, prep_rls ac_plus_times)), |
585 ("ac_plus_times", (Context.theory_name @{theory}, prep_rls' ac_plus_times)), |
585 ("rearrange_assoc", (Context.theory_name @{theory}, prep_rls rearrange_assoc))] *} |
586 ("rearrange_assoc", (Context.theory_name @{theory}, prep_rls' rearrange_assoc))] *} |
586 ML {* |
587 ML {* |
587 |
588 |
588 |
589 |
589 fun bin_o (Const (op_,(Type ("fun", |
590 fun bin_o (Const (op_,(Type ("fun", |
590 [Type (s2,[]),Type ("fun", |
591 [Type (s2,[]),Type ("fun", |
1115 rew_ord' := overwritel (!rew_ord', |
1116 rew_ord' := overwritel (!rew_ord', |
1116 [("termlessI", termlessI), |
1117 [("termlessI", termlessI), |
1117 ("ord_make_polytest", ord_make_polytest false thy) |
1118 ("ord_make_polytest", ord_make_polytest false thy) |
1118 ]); |
1119 ]); |
1119 |
1120 |
1120 (*WN060510 this was a preparation for prep_rls ... |
1121 (*WN060510 this was a preparation for prep_rls' ... |
1121 val scr_make_polytest = |
1122 val scr_make_polytest = |
1122 "Script Expand_binomtest t_t =" ^ |
1123 "Script Expand_binomtest t_t =" ^ |
1123 "(Repeat " ^ |
1124 "(Repeat " ^ |
1124 "((Try (Repeat (Rewrite real_diff_minus False))) @@ " ^ |
1125 "((Try (Repeat (Rewrite real_diff_minus False))) @@ " ^ |
1125 |
1126 |
1223 scr = EmptyScr(*Prog ((term_of o the o (parse thy)) |
1224 scr = EmptyScr(*Prog ((term_of o the o (parse thy)) |
1224 scr_make_polytest)*) |
1225 scr_make_polytest)*) |
1225 }:rls; |
1226 }:rls; |
1226 *} |
1227 *} |
1227 ML {* |
1228 ML {* |
1228 (*WN060510 this was done before 'fun prep_rls' ...------------------------ |
1229 (*WN060510 this was done before 'fun prep_rls ...------------------------ |
1229 val scr_expand_binomtest = |
1230 val scr_expand_binomtest = |
1230 "Script Expand_binomtest t_t =" ^ |
1231 "Script Expand_binomtest t_t =" ^ |
1231 "(Repeat " ^ |
1232 "(Repeat " ^ |
1232 "((Try (Repeat (Rewrite real_plus_binom_pow2 False))) @@ " ^ |
1233 "((Try (Repeat (Rewrite real_plus_binom_pow2 False))) @@ " ^ |
1233 " (Try (Repeat (Rewrite real_plus_binom_times False))) @@ " ^ |
1234 " (Try (Repeat (Rewrite real_plus_binom_times False))) @@ " ^ |
1356 scr = EmptyScr |
1357 scr = EmptyScr |
1357 (*Script ((term_of o the o (parse thy)) scr_expand_binomtest)*) |
1358 (*Script ((term_of o the o (parse thy)) scr_expand_binomtest)*) |
1358 }:rls; |
1359 }:rls; |
1359 *} |
1360 *} |
1360 setup {* KEStore_Elems.add_rlss |
1361 setup {* KEStore_Elems.add_rlss |
1361 [("make_polytest", (Context.theory_name @{theory}, prep_rls make_polytest)), |
1362 [("make_polytest", (Context.theory_name @{theory}, prep_rls' make_polytest)), |
1362 ("expand_binomtest", (Context.theory_name @{theory}, prep_rls expand_binomtest))] *} |
1363 ("expand_binomtest", (Context.theory_name @{theory}, prep_rls' expand_binomtest))] *} |
1363 |
1364 |
1364 end |
1365 end |