434 |
434 |
435 Rule.Eval ("Prog_Expr.ident", Prog_Expr.eval_ident "#ident_")], |
435 Rule.Eval ("Prog_Expr.ident", Prog_Expr.eval_ident "#ident_")], |
436 scr = Rule.Empty_Prog |
436 scr = Rule.Empty_Prog |
437 }; |
437 }; |
438 \<close> |
438 \<close> |
439 setup \<open>KEStore_Elems.add_rlss [("testerls", (Context.theory_name @{theory}, prep_rls' testerls))]\<close> |
439 setup_rule testerls = \<open>prep_rls' testerls\<close> |
440 |
440 |
441 ML \<open> |
441 ML \<open> |
442 (*make () dissappear*) |
442 (*make () dissappear*) |
443 val rearrange_assoc = |
443 val rearrange_assoc = |
444 Rule_Def.Repeat{id = "rearrange_assoc", preconds = [], |
444 Rule_Def.Repeat{id = "rearrange_assoc", preconds = [], |
559 scr = Rule.Prog ((Thm.term_of o the o (TermC.parse thy)) |
559 scr = Rule.Prog ((Thm.term_of o the o (TermC.parse thy)) |
560 "empty_script") |
560 "empty_script") |
561 }; |
561 }; |
562 \<close> |
562 \<close> |
563 ML \<open>val prep_rls' = Auto_Prog.prep_rls @{theory};\<close> |
563 ML \<open>val prep_rls' = Auto_Prog.prep_rls @{theory};\<close> |
564 setup \<open>KEStore_Elems.add_rlss |
564 setup_rule |
565 [("Test_simplify", (Context.theory_name @{theory}, prep_rls' Test_simplify)), |
565 Test_simplify = \<open>prep_rls' Test_simplify\<close> and |
566 ("tval_rls", (Context.theory_name @{theory}, prep_rls' tval_rls)), |
566 tval_rls = \<open>prep_rls' tval_rls\<close> and |
567 ("isolate_root", (Context.theory_name @{theory}, prep_rls' isolate_root)), |
567 isolate_root = \<open>prep_rls' isolate_root\<close> and |
568 ("isolate_bdv", (Context.theory_name @{theory}, prep_rls' isolate_bdv)), |
568 isolate_bdv = \<open>prep_rls' isolate_bdv\<close> and |
569 ("matches", (Context.theory_name @{theory}, prep_rls' |
569 matches = \<open>prep_rls' |
570 (Rule_Set.append_rules "matches" testerls [Rule.Eval ("Prog_Expr.matches", Prog_Expr.eval_matches "#matches_")])))] |
570 (Rule_Set.append_rules "matches" testerls |
571 \<close> |
571 [Rule.Eval ("Prog_Expr.matches", Prog_Expr.eval_matches "#matches_")])\<close> |
|
572 |
572 |
573 |
573 subsection \<open>problems\<close> |
574 subsection \<open>problems\<close> |
574 (** problem types **) |
575 (** problem types **) |
575 setup \<open>KEStore_Elems.add_pbts |
576 setup \<open>KEStore_Elems.add_pbts |
576 [(Problem.prep_input thy "pbl_test" [] Problem.id_empty (["test"], [], Rule_Set.empty, NONE, [])), |
577 [(Problem.prep_input thy "pbl_test" [] Problem.id_empty (["test"], [], Rule_Set.empty, NONE, [])), |
763 ], |
764 ], |
764 scr = Rule.Empty_Prog |
765 scr = Rule.Empty_Prog |
765 (*Program ((Thm.term_of o the o (parse thy)) scr_expand_binomtest)*) |
766 (*Program ((Thm.term_of o the o (parse thy)) scr_expand_binomtest)*) |
766 }; |
767 }; |
767 \<close> |
768 \<close> |
768 setup \<open>KEStore_Elems.add_rlss |
769 setup_rule |
769 [("make_polytest", (Context.theory_name @{theory}, prep_rls' make_polytest)), |
770 make_polytest = \<open>prep_rls' make_polytest\<close> and |
770 ("expand_binomtest", (Context.theory_name @{theory}, prep_rls' expand_binomtest))]\<close> |
771 expand_binomtest = \<open>prep_rls' expand_binomtest\<close> |
771 setup \<open>KEStore_Elems.add_rlss |
772 setup_rule |
772 [("norm_equation", (Context.theory_name @{theory}, prep_rls' norm_equation)), |
773 norm_equation = \<open>prep_rls' norm_equation\<close> and |
773 ("ac_plus_times", (Context.theory_name @{theory}, prep_rls' ac_plus_times)), |
774 ac_plus_times = \<open>prep_rls' ac_plus_times\<close> and |
774 ("rearrange_assoc", (Context.theory_name @{theory}, prep_rls' rearrange_assoc))]\<close> |
775 rearrange_assoc = \<open>prep_rls' rearrange_assoc\<close> |
775 |
776 |
776 section \<open>problems\<close> |
777 section \<open>problems\<close> |
777 setup \<open>KEStore_Elems.add_pbts |
778 setup \<open>KEStore_Elems.add_pbts |
778 [(Problem.prep_input thy "pbl_test_uni_plain2" [] Problem.id_empty |
779 [(Problem.prep_input thy "pbl_test_uni_plain2" [] Problem.id_empty |
779 (["plain_square", "univariate", "equation", "test"], |
780 (["plain_square", "univariate", "equation", "test"], |