107 \end{description} |
107 \end{description} |
108 |
108 |
109 The above rulesets are all visible to the user, and also may be input; |
109 The above rulesets are all visible to the user, and also may be input; |
110 thus they must be contained in {\tt Theory_Data} (KEStore_Elems.add_rlss, |
110 thus they must be contained in {\tt Theory_Data} (KEStore_Elems.add_rlss, |
111 KEStore_Elems.get_rlss). All these rulesets must undergo a preparation |
111 KEStore_Elems.get_rlss). All these rulesets must undergo a preparation |
112 using the function {\tt prep_rls}, which generates a script for stepwise rewriting etc. |
112 using the function {\tt prep_rls'}, which generates a script for stepwise rewriting etc. |
113 The following rulesets are used for internal purposes and usually invisible to the (naive) user: |
113 The following rulesets are used for internal purposes and usually invisible to the (naive) user: |
114 \begin{description} |
114 \begin{description} |
115 |
115 |
116 \item [*\_erls] TODO |
116 \item [*\_erls] TODO |
117 \item [*\_prls] |
117 \item [*\_prls] |
641 Calc ("Atools.occurs'_in", |
641 Calc ("Atools.occurs'_in", |
642 eval_occurs_in "#occurs_in"), |
642 eval_occurs_in "#occurs_in"), |
643 Calc ("Tools.matches",eval_matches "#matches") |
643 Calc ("Tools.matches",eval_matches "#matches") |
644 ] (*i.A. zu viele rules*) |
644 ] (*i.A. zu viele rules*) |
645 );*) |
645 );*) |
646 (* val atools_erls = prep_rls( (*outcommented*) |
646 (* val atools_erls = prep_rls'( (*outcommented*) |
647 Rls {id="atools_erls",preconds = [], rew_ord = ("termlessI",termlessI), |
647 Rls {id="atools_erls",preconds = [], rew_ord = ("termlessI",termlessI), |
648 erls = e_rls, srls = Erls, calc = [], errpatts = [], |
648 erls = e_rls, srls = Erls, calc = [], errpatts = [], |
649 rules = [Thm ("refl",num_str @{thm refl}), |
649 rules = [Thm ("refl",num_str @{thm refl}), |
650 Thm ("order_refl",num_str @{thm order_refl}), |
650 Thm ("order_refl",num_str @{thm order_refl}), |
651 Thm ("radd_left_cancel_le",num_str @{thm radd_left_cancel_le}), |
651 Thm ("radd_left_cancel_le",num_str @{thm radd_left_cancel_le}), |
687 ("TIMES" ,("Groups.times_class.times", eval_binop "#mult_")), |
687 ("TIMES" ,("Groups.times_class.times", eval_binop "#mult_")), |
688 ("DIVIDE" ,("Fields.inverse_class.divide", eval_cancel "#divide_e")), |
688 ("DIVIDE" ,("Fields.inverse_class.divide", eval_cancel "#divide_e")), |
689 ("POWER" ,("Atools.pow", eval_binop "#power_")), |
689 ("POWER" ,("Atools.pow", eval_binop "#power_")), |
690 ("boollist2sum",("Atools.boollist2sum", eval_boollist2sum ""))] *} |
690 ("boollist2sum",("Atools.boollist2sum", eval_boollist2sum ""))] *} |
691 ML {* |
691 ML {* |
692 val list_rls = prep_rls' @{theory} (merge_rls "list_erls" |
692 val list_rls = prep_rls @{theory} (merge_rls "list_erls" |
693 (Rls {id = "replaced", preconds = [], rew_ord = ("termlessI", termlessI), |
693 (Rls {id = "replaced", preconds = [], rew_ord = ("termlessI", termlessI), |
694 erls = Rls {id = "list_elrs", preconds = [], rew_ord = ("termlessI", termlessI), |
694 erls = Rls {id = "list_elrs", preconds = [], rew_ord = ("termlessI", termlessI), |
695 erls = e_rls, srls = Erls, calc = [], errpatts = [], |
695 erls = e_rls, srls = Erls, calc = [], errpatts = [], |
696 rules = [Calc ("Groups.plus_class.plus", eval_binop "#add_"), |
696 rules = [Calc ("Groups.plus_class.plus", eval_binop "#add_"), |
697 Calc ("Orderings.ord_class.less", eval_equ "#less_") |
697 Calc ("Orderings.ord_class.less", eval_equ "#less_") |
700 srls = Erls, calc = [], errpatts = [], |
700 srls = Erls, calc = [], errpatts = [], |
701 rules = [], scr = EmptyScr}) |
701 rules = [], scr = EmptyScr}) |
702 list_rls); |
702 list_rls); |
703 *} |
703 *} |
704 setup {* KEStore_Elems.add_rlss |
704 setup {* KEStore_Elems.add_rlss |
705 [("list_rls", (Context.theory_name @{theory}, prep_rls' @{theory} list_rls))] *} |
705 [("list_rls", (Context.theory_name @{theory}, prep_rls @{theory} list_rls))] *} |
706 |
706 |
707 end |
707 end |