1.1 --- a/src/Tools/isac/BaseDefinitions/Know_Store.thy	Wed May 26 16:19:41 2021 +0200
     1.2 +++ b/src/Tools/isac/BaseDefinitions/Know_Store.thy	Wed May 26 16:24:05 2021 +0200
     1.3 @@ -15,7 +15,9 @@
     1.4  appropriate use of polymorphic high order functions.
     1.5  *)
     1.6  
     1.7 -theory Know_Store imports Complex_Main
     1.8 +theory Know_Store
     1.9 +  imports Complex_Main
    1.10 +  keywords "setup_rule" :: thy_decl
    1.11  begin
    1.12  
    1.13  setup \<open>
    1.14 @@ -166,6 +168,35 @@
    1.15  end;
    1.16  \<close>
    1.17  
    1.18 +
    1.19 +subsection \<open>Isar command syntax\<close>
    1.20 +
    1.21 +ML \<open>
    1.22 +local
    1.23 +
    1.24 +val parse_rule = Parse.name -- Parse.!!! (\<^keyword>\<open>=\<close> |-- Parse.ML_source);
    1.25 +
    1.26 +val ml = ML_Lex.read;
    1.27 +
    1.28 +fun ml_rule thy (name, source) =
    1.29 +  ml "(" @ ml (ML_Syntax.print_string name) @ ml ", " @
    1.30 +  ml "(" @ ml (ML_Syntax.print_string (Context.theory_name thy)) @ ml ", " @
    1.31 +  ML_Lex.read_source source @ ml "))";
    1.32 +
    1.33 +fun ml_rules thy args =
    1.34 +  ml "Theory.setup (KEStore_Elems.add_rlss [" @
    1.35 +    flat (separate (ml ",") (map (ml_rule thy) args)) @ ml "])";
    1.36 +
    1.37 +val _ =
    1.38 +  Outer_Syntax.command \<^command_keyword>\<open>setup_rule\<close> "setup ISAC rules"
    1.39 +    (Parse.and_list1 parse_rule >> (fn args => Toplevel.theory (fn thy =>
    1.40 +      thy |> Context.theory_map
    1.41 +        (ML_Context.expression (Position.thread_data ()) (ml_rules thy args)))));
    1.42 +
    1.43 +in end;
    1.44 +\<close>
    1.45 +
    1.46 +
    1.47  section \<open>Re-use existing access functions for knowledge elements\<close>
    1.48  text \<open>
    1.49    The independence of problems' and methods' structure enforces the accesse
    1.50 @@ -206,9 +237,10 @@
    1.51  fun get_mets () = get_ref_thy () |> KEStore_Elems.get_mets;
    1.52  fun get_thes () = get_ref_thy () |> KEStore_Elems.get_thes;
    1.53  \<close>
    1.54 -setup \<open>KEStore_Elems.add_rlss 
    1.55 -  [("empty", (Context.theory_name @{theory}, Rule_Set.empty)), 
    1.56 -  ("e_rrls", (Context.theory_name @{theory}, Rule_Set.e_rrls))]\<close>
    1.57 +
    1.58 +setup_rule
    1.59 +  empty = \<open>Rule_Set.empty\<close> and
    1.60 +  e_rrls = \<open>Rule_Set.e_rrls\<close>
    1.61  
    1.62  section \<open>determine sequence of main parts in thehier\<close>
    1.63  setup \<open>

     2.1 --- a/src/Tools/isac/Knowledge/Base_Tools.thy	Wed May 26 16:19:41 2021 +0200
     2.2 +++ b/src/Tools/isac/Knowledge/Base_Tools.thy	Wed May 26 16:24:05 2021 +0200
     2.3 @@ -147,9 +147,10 @@
     2.4      rules = [], scr = Rule.Empty_Prog})
     2.5    prog_expr);
     2.6  \<close>
     2.7 +
     2.8  subsection \<open>setup for extended rule-set\<close>
     2.9 -setup \<open>KEStore_Elems.add_rlss
    2.10 -  [("prog_expr", (Context.theory_name @{theory}, Auto_Prog.prep_rls @{theory} prog_expr))]\<close>
    2.11 +
    2.12 +setup_rule prog_expr = \<open>Auto_Prog.prep_rls @{theory} prog_expr\<close>
    2.13  
    2.14  ML \<open>
    2.15  \<close> ML \<open>

     3.1 --- a/src/Tools/isac/Knowledge/Diff.thy	Wed May 26 16:19:41 2021 +0200
     3.2 +++ b/src/Tools/isac/Knowledge/Diff.thy	Wed May 26 16:24:05 2021 +0200
     3.3 @@ -232,12 +232,12 @@
     3.4       rules = [Rule.Rls_ diff_rules, Rule.Rls_ norm_Poly ],
     3.5       scr = Rule.Empty_Prog};
     3.6  \<close>
     3.7 -setup \<open>KEStore_Elems.add_rlss 
     3.8 -  [("erls_diff", (Context.theory_name @{theory}, prep_rls' erls_diff)), 
     3.9 -  ("diff_rules", (Context.theory_name @{theory}, prep_rls' diff_rules)), 
    3.10 -  ("norm_diff", (Context.theory_name @{theory}, prep_rls' norm_diff)), 
    3.11 -  ("diff_conv", (Context.theory_name @{theory}, prep_rls' diff_conv)), 
    3.12 -  ("diff_sym_conv", (Context.theory_name @{theory}, prep_rls' diff_sym_conv))]\<close>
    3.13 +setup_rule
    3.14 +  erls_diff = \<open>prep_rls' erls_diff\<close> and
    3.15 +  diff_rules = \<open>prep_rls' diff_rules\<close> and
    3.16 +  norm_diff = \<open>prep_rls' norm_diff\<close> and
    3.17 +  diff_conv = \<open>prep_rls' diff_conv\<close> and
    3.18 +  diff_sym_conv = \<open>prep_rls' diff_sym_conv\<close>
    3.19  
    3.20  (** problem types **)
    3.21  setup \<open>KEStore_Elems.add_pbts

     4.1 --- a/src/Tools/isac/Knowledge/DiffApp.thy	Wed May 26 16:19:41 2021 +0200
     4.2 +++ b/src/Tools/isac/Knowledge/DiffApp.thy	Wed May 26 16:24:05 2021 +0200
     4.3 @@ -59,7 +59,7 @@
     4.4      scr = Rule.Empty_Prog
     4.5      });
     4.6  \<close>
     4.7 -setup \<open>KEStore_Elems.add_rlss [("eval_rls", (Context.theory_name @{theory}, eval_rls))]\<close>
     4.8 +setup_rule eval_rls = \<open>eval_rls\<close>
     4.9  
    4.10  (** problem types **)
    4.11  setup \<open>KEStore_Elems.add_pbts
    4.12 @@ -199,8 +199,8 @@
    4.13    [Rule.Thm ("filterVar_Const", ThmC.numerals_to_Free @{thm filterVar_Const}),
    4.14     Rule.Thm ("filterVar_Nil", ThmC.numerals_to_Free @{thm filterVar_Nil})];
    4.15  \<close>
    4.16 -setup \<open>KEStore_Elems.add_rlss [("prog_expr", (Context.theory_name @{theory}, prog_expr))]
    4.17 -\<close> ML \<open>
    4.18 +setup_rule prog_expr = \<open>prog_expr\<close>
    4.19 +ML \<open>
    4.20  \<close> ML \<open>
    4.21  \<close> ML \<open>
    4.22  \<close>

     5.1 --- a/src/Tools/isac/Knowledge/EqSystem.thy	Wed May 26 16:19:41 2021 +0200
     5.2 +++ b/src/Tools/isac/Knowledge/EqSystem.thy	Wed May 26 16:24:05 2021 +0200
     5.3 @@ -393,17 +393,15 @@
     5.4  	 scr = Rule.Empty_Prog};
     5.5  \<close>
     5.6  
     5.7 -setup \<open>KEStore_Elems.add_rlss 
     5.8 -  [("simplify_System_parenthesized",
     5.9 -    (Context.theory_name @{theory}, prep_rls' simplify_System_parenthesized)), 
    5.10 -  ("simplify_System", (Context.theory_name @{theory}, prep_rls' simplify_System)), 
    5.11 -  ("isolate_bdvs", (Context.theory_name @{theory}, prep_rls' isolate_bdvs)), 
    5.12 -  ("isolate_bdvs_4x4", (Context.theory_name @{theory}, prep_rls' isolate_bdvs_4x4)), 
    5.13 -  ("order_system", (Context.theory_name @{theory}, prep_rls' order_system)), 
    5.14 -  ("order_add_mult_System", (Context.theory_name @{theory}, prep_rls' order_add_mult_System)), 
    5.15 -  ("norm_System_noadd_fractions", 
    5.16 -    (Context.theory_name @{theory}, prep_rls' norm_System_noadd_fractions)), 
    5.17 -  ("norm_System", (Context.theory_name @{theory}, prep_rls' norm_System))]\<close>
    5.18 +setup_rule
    5.19 +  simplify_System_parenthesized = \<open>prep_rls' simplify_System_parenthesized\<close> and
    5.20 +  simplify_System = \<open>prep_rls' simplify_System\<close> and
    5.21 +  isolate_bdvs = \<open>prep_rls' isolate_bdvs\<close> and
    5.22 +  isolate_bdvs_4x4 = \<open>prep_rls' isolate_bdvs_4x4\<close> and 
    5.23 +  order_system = \<open>prep_rls' order_system\<close> and 
    5.24 +  order_add_mult_System = \<open>prep_rls' order_add_mult_System\<close> and
    5.25 +  norm_System_noadd_fractions = \<open>prep_rls' norm_System_noadd_fractions\<close> and
    5.26 +  norm_System = \<open>prep_rls' norm_System\<close>
    5.27  
    5.28  
    5.29  section \<open>Problems\<close>

     6.1 --- a/src/Tools/isac/Knowledge/Equation.thy	Wed May 26 16:19:41 2021 +0200
     6.2 +++ b/src/Tools/isac/Knowledge/Equation.thy	Wed May 26 16:24:05 2021 +0200
     6.3 @@ -40,8 +40,7 @@
     6.4      Rule_Set.append_rules "univariate_equation_prls" Rule_Set.empty 
     6.5  	       [Rule.Eval ("Prog_Expr.matches", Prog_Expr.eval_matches "")];
     6.6  \<close>
     6.7 -setup \<open>KEStore_Elems.add_rlss [("univariate_equation_prls",
     6.8 -  (Context.theory_name @{theory}, Auto_Prog.prep_rls @{theory} univariate_equation_prls))]\<close>
     6.9 +setup_rule univariate_equation_prls = \<open>Auto_Prog.prep_rls @{theory} univariate_equation_prls\<close>
    6.10  setup \<open>KEStore_Elems.add_pbts
    6.11    [(Problem.prep_input thy "pbl_equ" [] Problem.id_empty
    6.12        (["equation"],

     7.1 --- a/src/Tools/isac/Knowledge/InsSort.thy	Wed May 26 16:19:41 2021 +0200
     7.2 +++ b/src/Tools/isac/Knowledge/InsSort.thy	Wed May 26 16:24:05 2021 +0200
     7.3 @@ -68,7 +68,7 @@
     7.4  	    Rule.Thm ("if_False", @{thm if_False} (* "(if False then x else y) = y" *))],
     7.5  	  errpatts = [], scr = Rule.Empty_Prog};      
     7.6  \<close>
     7.7 -setup \<open>KEStore_Elems.add_rlss [("ins_sort", (Context.theory_name @{theory}, ins_sort))]\<close>
     7.8 +setup_rule ins_sort = ins_sort
     7.9  
    7.10  section \<open>problems\<close>
    7.11  setup \<open>KEStore_Elems.add_pbts

     8.1 --- a/src/Tools/isac/Knowledge/Integrate.thy	Wed May 26 16:19:41 2021 +0200
     8.2 +++ b/src/Tools/isac/Knowledge/Integrate.thy	Wed May 26 16:24:05 2021 +0200
     8.3 @@ -319,17 +319,14 @@
     8.4  
     8.5  val prep_rls' = Auto_Prog.prep_rls @{theory};
     8.6  \<close>
     8.7 -setup \<open>KEStore_Elems.add_rlss 
     8.8 -  [("integration_rules", (Context.theory_name @{theory}, prep_rls' integration_rules)), 
     8.9 -  ("add_new_c", (Context.theory_name @{theory}, prep_rls' add_new_c)), 
    8.10 -  ("simplify_Integral", (Context.theory_name @{theory}, prep_rls' simplify_Integral)), 
    8.11 -  ("integration", (Context.theory_name @{theory}, prep_rls' integration)), 
    8.12 -  ("separate_bdv2", (Context.theory_name @{theory}, prep_rls' separate_bdv2)),
    8.13 -
    8.14 -  ("norm_Rational_noadd_fractions", (Context.theory_name @{theory},
    8.15 -    prep_rls' norm_Rational_noadd_fractions)), 
    8.16 -  ("norm_Rational_rls_noadd_fractions", (Context.theory_name @{theory},
    8.17 -    prep_rls' norm_Rational_rls_noadd_fractions))]\<close>
    8.18 +setup_rule
    8.19 +  integration_rules = \<open>prep_rls' integration_rules\<close> and
    8.20 +  add_new_c = \<open>prep_rls' add_new_c\<close> and
    8.21 +  simplify_Integral = \<open>prep_rls' simplify_Integral\<close> and
    8.22 +  integration = \<open>prep_rls' integration\<close> and
    8.23 +  separate_bdv2 = \<open>prep_rls' separate_bdv2\<close> and
    8.24 +  norm_Rational_noadd_fractions = \<open>prep_rls' norm_Rational_noadd_fractions\<close> and
    8.25 +  norm_Rational_rls_noadd_fractions = \<open>prep_rls' norm_Rational_rls_noadd_fractions\<close>
    8.26  
    8.27  (** problems **)
    8.28  setup \<open>KEStore_Elems.add_pbts

     9.1 --- a/src/Tools/isac/Knowledge/Inverse_Z_Transform.thy	Wed May 26 16:19:41 2021 +0200
     9.2 +++ b/src/Tools/isac/Knowledge/Inverse_Z_Transform.thy	Wed May 26 16:24:05 2021 +0200
     9.3 @@ -39,7 +39,7 @@
     9.4  
     9.5  text \<open>store the rule set for math engine\<close>
     9.6  
     9.7 -setup \<open>KEStore_Elems.add_rlss [("inverse_z", (Context.theory_name @{theory}, inverse_z))]\<close>
     9.8 +setup_rule inverse_z = inverse_z
     9.9  
    9.10  subsection\<open>Define the Specification\<close>
    9.11  ML \<open>

    10.1 --- a/src/Tools/isac/Knowledge/LinEq.thy	Wed May 26 16:19:41 2021 +0200
    10.2 +++ b/src/Tools/isac/Knowledge/LinEq.thy	Wed May 26 16:24:05 2021 +0200
    10.3 @@ -64,8 +64,7 @@
    10.4       *)
    10.5      ];
    10.6  \<close>
    10.7 -setup \<open>KEStore_Elems.add_rlss 
    10.8 -  [("LinEq_erls", (Context.theory_name @{theory}, LinEq_erls))]\<close>
    10.9 +setup_rule LinEq_erls = LinEq_erls
   10.10  ML \<open>
   10.11      
   10.12  val LinPoly_simplify = prep_rls'(
   10.13 @@ -87,8 +86,7 @@
   10.14  		],
   10.15         scr = Rule.Empty_Prog});
   10.16  \<close>
   10.17 -setup \<open>KEStore_Elems.add_rlss 
   10.18 -  [("LinPoly_simplify", (Context.theory_name @{theory}, LinPoly_simplify))]\<close>
   10.19 +setup_rule LinPoly_simplify = LinPoly_simplify
   10.20  ML \<open>
   10.21  
   10.22  (*isolate the bound variable in an linear equation; 'bdv' is a meta-constant*)
   10.23 @@ -108,8 +106,7 @@
   10.24  	      ],
   10.25       scr = Rule.Empty_Prog});
   10.26  \<close>
   10.27 -setup \<open>KEStore_Elems.add_rlss 
   10.28 -  [("LinEq_simplify", (Context.theory_name @{theory}, LinEq_simplify))]\<close>
   10.29 +setup_rule LinEq_simplify = LinEq_simplify
   10.30  
   10.31  (*----------------------------- problem types --------------------------------*)
   10.32  (* ---------linear----------- *)

    11.1 --- a/src/Tools/isac/Knowledge/Partial_Fractions.thy	Wed May 26 16:19:41 2021 +0200
    11.2 +++ b/src/Tools/isac/Knowledge/Partial_Fractions.thy	Wed May 26 16:24:05 2021 +0200
    11.3 @@ -134,10 +134,10 @@
    11.4  \<close>
    11.5  
    11.6  text \<open>store the rule set for math engine\<close>
    11.7 -setup \<open>KEStore_Elems.add_rlss 
    11.8 -  [("ansatz_rls", (Context.theory_name @{theory}, ansatz_rls)), 
    11.9 -  ("multiply_ansatz", (Context.theory_name @{theory}, multiply_ansatz)), 
   11.10 -  ("equival_trans", (Context.theory_name @{theory}, equival_trans))]\<close>
   11.11 +setup_rule
   11.12 +  ansatz_rls = ansatz_rls and
   11.13 +  multiply_ansatz = multiply_ansatz and
   11.14 +  equival_trans = equival_trans
   11.15  
   11.16  subsection \<open>Specification\<close>
   11.17  

    12.1 --- a/src/Tools/isac/Knowledge/Poly.thy	Wed May 26 16:19:41 2021 +0200
    12.2 +++ b/src/Tools/isac/Knowledge/Poly.thy	Wed May 26 16:24:05 2021 +0200
    12.3 @@ -1402,36 +1402,35 @@
    12.4  subsubsection \<open>rule-sets\<close>
    12.5  ML \<open>val prep_rls' = Auto_Prog.prep_rls @{theory}\<close>
    12.6  
    12.7 -setup \<open>KEStore_Elems.add_rlss 
    12.8 -  [("norm_Poly", (Context.theory_name @{theory}, prep_rls' norm_Poly)), 
    12.9 -  ("Poly_erls", (Context.theory_name @{theory}, prep_rls' Poly_erls)),(*FIXXXME:del with rls.rls'*) 
   12.10 -  ("expand", (Context.theory_name @{theory}, prep_rls' expand)), 
   12.11 -  ("expand_poly", (Context.theory_name @{theory}, prep_rls' expand_poly)), 
   12.12 -  ("simplify_power", (Context.theory_name @{theory}, prep_rls' simplify_power)),
   12.13 +setup_rule
   12.14 +  norm_Poly = \<open>prep_rls' norm_Poly\<close> and
   12.15 +  Poly_erls = \<open>prep_rls' Poly_erls\<close> (*FIXXXME:del with rls.rls'*) and
   12.16 +  expand = \<open>prep_rls' expand\<close> and
   12.17 +  expand_poly = \<open>prep_rls' expand_poly\<close> and
   12.18 +  simplify_power = \<open>prep_rls' simplify_power\<close> and
   12.19  
   12.20 -  ("order_add_mult", (Context.theory_name @{theory}, prep_rls' order_add_mult)), 
   12.21 -  ("collect_numerals", (Context.theory_name @{theory}, prep_rls' collect_numerals)), 
   12.22 -  ("collect_numerals_", (Context.theory_name @{theory}, prep_rls' collect_numerals_)), 
   12.23 -  ("reduce_012", (Context.theory_name @{theory}, prep_rls' reduce_012)), 
   12.24 -  ("discard_parentheses", (Context.theory_name @{theory}, prep_rls' discard_parentheses)),
   12.25 +  order_add_mult = \<open>prep_rls' order_add_mult\<close> and
   12.26 +  collect_numerals = \<open>prep_rls' collect_numerals\<close> and
   12.27 +  collect_numerals_= \<open>prep_rls' collect_numerals_\<close> and
   12.28 +  reduce_012 = \<open>prep_rls' reduce_012\<close> and
   12.29 +  discard_parentheses = \<open>prep_rls' discard_parentheses\<close> and
   12.30   
   12.31 -  ("make_polynomial", (Context.theory_name @{theory}, prep_rls' make_polynomial)), 
   12.32 -  ("expand_binoms", (Context.theory_name @{theory}, prep_rls' expand_binoms)), 
   12.33 -  ("rev_rew_p", (Context.theory_name @{theory}, prep_rls' rev_rew_p)), 
   12.34 -  ("discard_minus", (Context.theory_name @{theory}, prep_rls' discard_minus)), 
   12.35 -  ("expand_poly_", (Context.theory_name @{theory}, prep_rls' expand_poly_)),
   12.36 +  make_polynomial = \<open>prep_rls' make_polynomial\<close> and
   12.37 +  expand_binoms = \<open>prep_rls' expand_binoms\<close> and
   12.38 +  rev_rew_p = \<open>prep_rls' rev_rew_p\<close> and
   12.39 +  discard_minus = \<open>prep_rls' discard_minus\<close> and
   12.40 +  expand_poly_ = \<open>prep_rls' expand_poly_\<close> and
   12.41   
   12.42 -  ("expand_poly_rat_", (Context.theory_name @{theory}, prep_rls' expand_poly_rat_)), 
   12.43 -  ("simplify_power_", (Context.theory_name @{theory}, prep_rls' simplify_power_)), 
   12.44 -  ("calc_add_mult_pow_", (Context.theory_name @{theory}, prep_rls' calc_add_mult_pow_)), 
   12.45 -  ("reduce_012_mult_", (Context.theory_name @{theory}, prep_rls' reduce_012_mult_)), 
   12.46 -  ("reduce_012_", (Context.theory_name @{theory}, prep_rls' reduce_012_)),
   12.47 +  expand_poly_rat_ = \<open>prep_rls' expand_poly_rat_\<close> and
   12.48 +  simplify_power_ = \<open>prep_rls' simplify_power_\<close> and
   12.49 +  calc_add_mult_pow_ = \<open>prep_rls' calc_add_mult_pow_\<close> and
   12.50 +  reduce_012_mult_ = \<open>prep_rls' reduce_012_mult_\<close> and
   12.51 +  reduce_012_ = \<open>prep_rls' reduce_012_\<close> and
   12.52   
   12.53 -  ("discard_parentheses1", (Context.theory_name @{theory}, prep_rls' discard_parentheses1)), 
   12.54 -  ("order_mult_rls_", (Context.theory_name @{theory}, prep_rls' order_mult_rls_)), 
   12.55 -  ("order_add_rls_", (Context.theory_name @{theory}, prep_rls' order_add_rls_)), 
   12.56 -  ("make_rat_poly_with_parentheses",
   12.57 -    (Context.theory_name @{theory}, prep_rls' make_rat_poly_with_parentheses))]\<close>
   12.58 +  discard_parentheses1 = \<open>prep_rls' discard_parentheses1\<close> and
   12.59 +  order_mult_rls_ = \<open>prep_rls' order_mult_rls_\<close> and
   12.60 +  order_add_rls_ = \<open>prep_rls' order_add_rls_\<close> and
   12.61 +  make_rat_poly_with_parentheses = \<open>prep_rls' make_rat_poly_with_parentheses\<close>
   12.62  
   12.63  subsection \<open>problems\<close>
   12.64  setup \<open>KEStore_Elems.add_pbts

    13.1 --- a/src/Tools/isac/Knowledge/PolyEq.thy	Wed May 26 16:19:41 2021 +0200
    13.2 +++ b/src/Tools/isac/Knowledge/PolyEq.thy	Wed May 26 16:24:05 2021 +0200
    13.3 @@ -425,11 +425,11 @@
    13.4         scr = Rule.Empty_Prog
    13.5         });
    13.6  \<close>
    13.7 -setup \<open>KEStore_Elems.add_rlss 
    13.8 -  [("cancel_leading_coeff", (Context.theory_name @{theory}, cancel_leading_coeff)), 
    13.9 -  ("complete_square", (Context.theory_name @{theory}, complete_square)), 
   13.10 -  ("PolyEq_erls", (Context.theory_name @{theory}, PolyEq_erls)), 
   13.11 -  ("polyeq_simplify", (Context.theory_name @{theory}, polyeq_simplify))]\<close>
   13.12 +setup_rule
   13.13 +  cancel_leading_coeff = cancel_leading_coeff and
   13.14 +  complete_square = complete_square and
   13.15 +  PolyEq_erls = PolyEq_erls and
   13.16 +  polyeq_simplify = polyeq_simplify
   13.17  ML\<open>
   13.18  
   13.19  (* ------------- polySolve ------------------ *)
   13.20 @@ -757,19 +757,17 @@
   13.21         scr = Rule.Empty_Prog
   13.22        });
   13.23  \<close>
   13.24 -setup \<open>KEStore_Elems.add_rlss 
   13.25 -  [("d0_polyeq_simplify", (Context.theory_name @{theory}, d0_polyeq_simplify)), 
   13.26 -  ("d1_polyeq_simplify", (Context.theory_name @{theory}, d1_polyeq_simplify)), 
   13.27 -  ("d2_polyeq_simplify", (Context.theory_name @{theory}, d2_polyeq_simplify)), 
   13.28 -  ("d2_polyeq_bdv_only_simplify", (Context.theory_name @{theory}, d2_polyeq_bdv_only_simplify)), 
   13.29 -  ("d2_polyeq_sq_only_simplify", (Context.theory_name @{theory}, d2_polyeq_sq_only_simplify)),
   13.30 +setup_rule
   13.31 +  d0_polyeq_simplify = d0_polyeq_simplify and
   13.32 +  d1_polyeq_simplify = d1_polyeq_simplify and
   13.33 +  d2_polyeq_simplify = d2_polyeq_simplify and
   13.34 +  d2_polyeq_bdv_only_simplify = d2_polyeq_bdv_only_simplify and
   13.35 +  d2_polyeq_sq_only_simplify = d2_polyeq_sq_only_simplify and
   13.36  
   13.37 -  ("d2_polyeq_pqFormula_simplify",
   13.38 -    (Context.theory_name @{theory}, d2_polyeq_pqFormula_simplify)), 
   13.39 -  ("d2_polyeq_abcFormula_simplify",
   13.40 -    (Context.theory_name @{theory}, d2_polyeq_abcFormula_simplify)), 
   13.41 -  ("d3_polyeq_simplify", (Context.theory_name @{theory}, d3_polyeq_simplify)), 
   13.42 -  ("d4_polyeq_simplify", (Context.theory_name @{theory}, d4_polyeq_simplify))]\<close>
   13.43 +  d2_polyeq_pqFormula_simplify = d2_polyeq_pqFormula_simplify and
   13.44 +  d2_polyeq_abcFormula_simplify = d2_polyeq_abcFormula_simplify and
   13.45 +  d3_polyeq_simplify = d3_polyeq_simplify and
   13.46 +  d4_polyeq_simplify = d4_polyeq_simplify
   13.47  
   13.48  setup \<open>KEStore_Elems.add_pbts
   13.49    [(Problem.prep_input thy "pbl_equ_univ_poly" [] Problem.id_empty
   13.50 @@ -1331,13 +1329,13 @@
   13.51  	       ],
   13.52        scr = Rule.Empty_Prog});      
   13.53  \<close>
   13.54 -setup \<open>KEStore_Elems.add_rlss 
   13.55 -  [("order_add_mult_in", (Context.theory_name @{theory}, order_add_mult_in)), 
   13.56 -  ("collect_bdv", (Context.theory_name @{theory}, collect_bdv)), 
   13.57 -  ("make_polynomial_in", (Context.theory_name @{theory}, make_polynomial_in)), 
   13.58 -  ("make_ratpoly_in", (Context.theory_name @{theory}, make_ratpoly_in)), 
   13.59 -  ("separate_bdvs", (Context.theory_name @{theory}, separate_bdvs))]
   13.60 -\<close> ML \<open>
   13.61 +setup_rule
   13.62 +  order_add_mult_in = order_add_mult_in and
   13.63 +  collect_bdv = collect_bdv and
   13.64 +  make_polynomial_in = make_polynomial_in and
   13.65 +  make_ratpoly_in = make_ratpoly_in and
   13.66 +  separate_bdvs = separate_bdvs
   13.67 +ML \<open>
   13.68  \<close> ML \<open>
   13.69  \<close> ML \<open>
   13.70  \<close>

    14.1 --- a/src/Tools/isac/Knowledge/PolyMinus.thy	Wed May 26 16:19:41 2021 +0200
    14.2 +++ b/src/Tools/isac/Knowledge/PolyMinus.thy	Wed May 26 16:24:05 2021 +0200
    14.3 @@ -389,14 +389,13 @@
    14.4  		Rule.Eval ("Groups.minus_class.minus", (**)eval_binop "#subtr_")
    14.5  		];
    14.6  \<close>
    14.7 -setup \<open>KEStore_Elems.add_rlss 
    14.8 -  [("ordne_alphabetisch", (Context.theory_name @{theory}, prep_rls' ordne_alphabetisch)), 
    14.9 -  ("fasse_zusammen", (Context.theory_name @{theory}, prep_rls' fasse_zusammen)), 
   14.10 -  ("verschoenere", (Context.theory_name @{theory}, prep_rls' verschoenere)), 
   14.11 -  ("ordne_monome", (Context.theory_name @{theory}, prep_rls' ordne_monome)), 
   14.12 -  ("klammern_aufloesen", (Context.theory_name @{theory}, prep_rls' klammern_aufloesen)), 
   14.13 -  ("klammern_ausmultiplizieren",
   14.14 -    (Context.theory_name @{theory}, prep_rls' klammern_ausmultiplizieren))]\<close>
   14.15 +setup_rule
   14.16 +  ordne_alphabetisch = \<open>prep_rls' ordne_alphabetisch\<close> and
   14.17 +  fasse_zusammen = \<open>prep_rls' fasse_zusammen\<close> and
   14.18 +  verschoenere = \<open>prep_rls' verschoenere\<close> and
   14.19 +  ordne_monome = \<open>prep_rls' ordne_monome\<close> and
   14.20 +  klammern_aufloesen = \<open>prep_rls' klammern_aufloesen\<close> and
   14.21 +  klammern_ausmultiplizieren = \<open>prep_rls' klammern_ausmultiplizieren\<close>
   14.22  
   14.23  (** problems **)
   14.24  setup \<open>KEStore_Elems.add_pbts

    15.1 --- a/src/Tools/isac/Knowledge/RatEq.thy	Wed May 26 16:19:41 2021 +0200
    15.2 +++ b/src/Tools/isac/Knowledge/RatEq.thy	Wed May 26 16:24:05 2021 +0200
    15.3 @@ -155,9 +155,9 @@
    15.4         (* ((a/b) / c = a / (b*c) ) *)],
    15.5       scr = Rule.Empty_Prog});
    15.6  \<close>
    15.7 -setup \<open>KEStore_Elems.add_rlss [("rateq_erls", (Context.theory_name @{theory}, rateq_erls))]\<close>
    15.8 -setup \<open>KEStore_Elems.add_rlss [("RatEq_eliminate", (Context.theory_name @{theory}, RatEq_eliminate))]\<close>
    15.9 -setup \<open>KEStore_Elems.add_rlss [("RatEq_simplify", (Context.theory_name @{theory}, RatEq_simplify))]\<close>
   15.10 +setup_rule rateq_erls = rateq_erls
   15.11 +setup_rule RatEq_eliminate = RatEq_eliminate
   15.12 +setup_rule RatEq_simplify = RatEq_simplify
   15.13  
   15.14  subsection \<open>problems\<close>
   15.15  setup \<open>KEStore_Elems.add_pbts

    16.1 --- a/src/Tools/isac/Knowledge/Rational.thy	Wed May 26 16:19:41 2021 +0200
    16.2 +++ b/src/Tools/isac/Knowledge/Rational.thy	Wed May 26 16:24:05 2021 +0200
    16.3 @@ -852,29 +852,29 @@
    16.4      scr = Rule.Empty_Prog});
    16.5  \<close>
    16.6  
    16.7 -setup \<open>KEStore_Elems.add_rlss 
    16.8 -  [("calculate_Rational", (Context.theory_name @{theory}, calculate_Rational)), 
    16.9 -  ("calc_rat_erls", (Context.theory_name @{theory}, calc_rat_erls)), 
   16.10 -  ("rational_erls", (Context.theory_name @{theory}, rational_erls)), 
   16.11 -  ("cancel_p", (Context.theory_name @{theory}, cancel_p)), 
   16.12 -  ("add_fractions_p", (Context.theory_name @{theory}, add_fractions_p)),
   16.13 - 
   16.14 -  ("add_fractions_p_rls", (Context.theory_name @{theory}, add_fractions_p_rls)), 
   16.15 -  ("powers_erls", (Context.theory_name @{theory}, powers_erls)), 
   16.16 -  ("powers", (Context.theory_name @{theory}, powers)), 
   16.17 -  ("rat_mult_divide", (Context.theory_name @{theory}, rat_mult_divide)), 
   16.18 -  ("reduce_0_1_2", (Context.theory_name @{theory}, reduce_0_1_2)),
   16.19 - 
   16.20 -  ("rat_reduce_1", (Context.theory_name @{theory}, rat_reduce_1)), 
   16.21 -  ("norm_rat_erls", (Context.theory_name @{theory}, norm_rat_erls)), 
   16.22 -  ("norm_Rational", (Context.theory_name @{theory}, norm_Rational)), 
   16.23 -  ("norm_Rational_rls", (Context.theory_name @{theory}, norm_Rational_rls)), 
   16.24 -  ("norm_Rational_min", (Context.theory_name @{theory}, norm_Rational_min)),
   16.25 -  ("norm_Rational_parenthesized", (Context.theory_name @{theory}, norm_Rational_parenthesized)),
   16.26 - 
   16.27 -  ("rat_mult_poly", (Context.theory_name @{theory}, rat_mult_poly)), 
   16.28 -  ("rat_mult_div_pow", (Context.theory_name @{theory}, rat_mult_div_pow)), 
   16.29 -  ("cancel_p_rls", (Context.theory_name @{theory}, cancel_p_rls))]\<close>
   16.30 +setup_rule
   16.31 +  calculate_Rational = calculate_Rational and
   16.32 +  calc_rat_erls = calc_rat_erls and
   16.33 +  rational_erls = rational_erls and
   16.34 +  cancel_p = cancel_p and
   16.35 +  add_fractions_p = add_fractions_p and
   16.36 +
   16.37 +  add_fractions_p_rls = add_fractions_p_rls and
   16.38 +  powers_erls = powers_erls and
   16.39 +  powers = powers and
   16.40 +  rat_mult_divide = rat_mult_divide and
   16.41 +  reduce_0_1_2 = reduce_0_1_2 and
   16.42 +
   16.43 +  rat_reduce_1 = rat_reduce_1 and
   16.44 +  norm_rat_erls = norm_rat_erls and
   16.45 +  norm_Rational = norm_Rational and
   16.46 +  norm_Rational_rls = norm_Rational_rls and
   16.47 +  norm_Rational_min = norm_Rational_min and
   16.48 +  norm_Rational_parenthesized = norm_Rational_parenthesized and
   16.49 +
   16.50 +  rat_mult_poly = rat_mult_poly and
   16.51 +  rat_mult_div_pow = rat_mult_div_pow and
   16.52 +  cancel_p_rls = cancel_p_rls
   16.53  
   16.54  section \<open>A problem for simplification of rationals\<close>
   16.55  setup \<open>KEStore_Elems.add_pbts

    17.1 --- a/src/Tools/isac/Knowledge/Root.thy	Wed May 26 16:19:41 2021 +0200
    17.2 +++ b/src/Tools/isac/Knowledge/Root.thy	Wed May 26 16:24:05 2021 +0200
    17.3 @@ -186,7 +186,7 @@
    17.4          Rule.Eval ("HOL.eq", Prog_Expr.eval_equal "#equal_") 
    17.5          ];
    17.6  \<close>
    17.7 -setup \<open>KEStore_Elems.add_rlss [("Root_erls", (Context.theory_name @{theory}, Root_erls))]\<close>
    17.8 +setup_rule Root_erls = Root_erls
    17.9  ML \<open>
   17.10  
   17.11  val make_rooteq = prep_rls'(
   17.12 @@ -254,7 +254,7 @@
   17.13        scr = Rule.Empty_Prog
   17.14        });      
   17.15  \<close>
   17.16 -setup \<open>KEStore_Elems.add_rlss [("make_rooteq", (Context.theory_name @{theory}, make_rooteq))]\<close>
   17.17 +setup_rule make_rooteq = make_rooteq
   17.18  ML \<open>
   17.19  
   17.20  val prep_rls' = Auto_Prog.prep_rls @{theory};
   17.21 @@ -328,8 +328,7 @@
   17.22        scr = Rule.Empty_Prog
   17.23         });      
   17.24  \<close>
   17.25 -setup \<open>KEStore_Elems.add_rlss
   17.26 -  [("expand_rootbinoms", (Context.theory_name @{theory}, expand_rootbinoms))]\<close>
   17.27 +setup_rule expand_rootbinoms = expand_rootbinoms
   17.28  ML \<open>
   17.29  \<close> ML \<open>
   17.30  \<close> ML \<open>

    18.1 --- a/src/Tools/isac/Knowledge/RootEq.thy	Wed May 26 16:19:41 2021 +0200
    18.2 +++ b/src/Tools/isac/Knowledge/RootEq.thy	Wed May 26 16:24:05 2021 +0200
    18.3 @@ -433,13 +433,13 @@
    18.4         scr = Rule.Empty_Prog
    18.5      });
    18.6  \<close>
    18.7 -setup \<open>KEStore_Elems.add_rlss 
    18.8 -  [("RootEq_erls", (Context.theory_name @{theory}, RootEq_erls)), 
    18.9 -  ("rooteq_srls", (Context.theory_name @{theory}, rooteq_srls)),
   18.10 -  ("sqrt_isolate", (Context.theory_name @{theory}, sqrt_isolate)),
   18.11 -  ("l_sqrt_isolate", (Context.theory_name @{theory}, l_sqrt_isolate)),
   18.12 -  ("r_sqrt_isolate", (Context.theory_name @{theory}, r_sqrt_isolate)),
   18.13 -  ("rooteq_simplify", (Context.theory_name @{theory}, rooteq_simplify))]\<close>
   18.14 +setup_rule
   18.15 +  RootEq_erls = RootEq_erls and
   18.16 +  rooteq_srls = rooteq_srls and
   18.17 +  sqrt_isolate = sqrt_isolate and
   18.18 +  l_sqrt_isolate = l_sqrt_isolate and
   18.19 +  r_sqrt_isolate = r_sqrt_isolate and
   18.20 +  rooteq_simplify = rooteq_simplify
   18.21  
   18.22  subsection \<open>problems\<close>
   18.23  (*Ambiguous input produces 5 parse trees -----------------------------------------------------\\*)

    19.1 --- a/src/Tools/isac/Knowledge/RootRat.thy	Wed May 26 16:19:41 2021 +0200
    19.2 +++ b/src/Tools/isac/Knowledge/RootRat.thy	Wed May 26 16:24:05 2021 +0200
    19.3 @@ -27,9 +27,9 @@
    19.4  
    19.5  val prep_rls' = Auto_Prog.prep_rls @{theory};
    19.6  \<close>
    19.7 -setup \<open>KEStore_Elems.add_rlss 
    19.8 -  [("rootrat_erls", (Context.theory_name @{theory}, prep_rls' rootrat_erls)), 
    19.9 -  ("calculate_RootRat", (Context.theory_name @{theory}, prep_rls' calculate_RootRat))]\<close>
   19.10 +setup_rule
   19.11 +  rootrat_erls = \<open>prep_rls' rootrat_erls\<close> and
   19.12 +  calculate_RootRat = \<open>prep_rls' calculate_RootRat\<close>
   19.13  ML \<open>
   19.14  \<close> ML \<open>
   19.15  \<close> ML \<open>

    20.1 --- a/src/Tools/isac/Knowledge/RootRatEq.thy	Wed May 26 16:19:41 2021 +0200
    20.2 +++ b/src/Tools/isac/Knowledge/RootRatEq.thy	Wed May 26 16:24:05 2021 +0200
    20.3 @@ -116,9 +116,9 @@
    20.4  	(* [|f is_rootTerm_in bdv|] ==> ( (a =  e/f) = ( a  * f = e ))*)
    20.5       ], scr = Rule.Empty_Prog});
    20.6  \<close>
    20.7 -setup \<open>KEStore_Elems.add_rlss
    20.8 -  [("RooRatEq_erls", (Context.theory_name @{theory}, RooRatEq_erls)),
    20.9 -   ("rootrat_solve", (Context.theory_name @{theory}, rootrat_solve))]\<close>
   20.10 +setup_rule
   20.11 +  RooRatEq_erls = RooRatEq_erls and
   20.12 +  rootrat_solve = rootrat_solve
   20.13  
   20.14  subsection \<open>problems\<close>
   20.15  

    21.1 --- a/src/Tools/isac/Knowledge/Test.thy	Wed May 26 16:19:41 2021 +0200
    21.2 +++ b/src/Tools/isac/Knowledge/Test.thy	Wed May 26 16:24:05 2021 +0200
    21.3 @@ -436,7 +436,7 @@
    21.4        scr = Rule.Empty_Prog
    21.5        };      
    21.6  \<close>
    21.7 -setup \<open>KEStore_Elems.add_rlss [("testerls", (Context.theory_name @{theory}, prep_rls' testerls))]\<close>
    21.8 +setup_rule testerls = \<open>prep_rls' testerls\<close>
    21.9  
   21.10  ML \<open>
   21.11  (*make () dissappear*)   
   21.12 @@ -561,14 +561,15 @@
   21.13  	};      
   21.14  \<close>
   21.15  ML \<open>val prep_rls' = Auto_Prog.prep_rls @{theory};\<close>
   21.16 -setup \<open>KEStore_Elems.add_rlss 
   21.17 -  [("Test_simplify", (Context.theory_name @{theory}, prep_rls' Test_simplify)), 
   21.18 -  ("tval_rls", (Context.theory_name @{theory}, prep_rls' tval_rls)), 
   21.19 -  ("isolate_root", (Context.theory_name @{theory}, prep_rls' isolate_root)), 
   21.20 -  ("isolate_bdv", (Context.theory_name @{theory}, prep_rls' isolate_bdv)), 
   21.21 -  ("matches", (Context.theory_name @{theory}, prep_rls'
   21.22 -    (Rule_Set.append_rules "matches" testerls [Rule.Eval ("Prog_Expr.matches", Prog_Expr.eval_matches "#matches_")])))]
   21.23 -\<close>
   21.24 +setup_rule
   21.25 +  Test_simplify = \<open>prep_rls' Test_simplify\<close> and
   21.26 +  tval_rls = \<open>prep_rls' tval_rls\<close> and
   21.27 +  isolate_root = \<open>prep_rls' isolate_root\<close> and
   21.28 +  isolate_bdv = \<open>prep_rls' isolate_bdv\<close> and
   21.29 +  matches = \<open>prep_rls'
   21.30 +    (Rule_Set.append_rules "matches" testerls
   21.31 +      [Rule.Eval ("Prog_Expr.matches", Prog_Expr.eval_matches "#matches_")])\<close>
   21.32 +
   21.33  
   21.34  subsection \<open>problems\<close>
   21.35  (** problem types **)
   21.36 @@ -765,13 +766,13 @@
   21.37  (*Program ((Thm.term_of o the o (parse thy)) scr_expand_binomtest)*)
   21.38        };      
   21.39  \<close>
   21.40 -setup \<open>KEStore_Elems.add_rlss 
   21.41 -  [("make_polytest", (Context.theory_name @{theory}, prep_rls' make_polytest)), 
   21.42 -  ("expand_binomtest", (Context.theory_name @{theory}, prep_rls' expand_binomtest))]\<close>
   21.43 -setup \<open>KEStore_Elems.add_rlss 
   21.44 -  [("norm_equation", (Context.theory_name @{theory}, prep_rls' norm_equation)), 
   21.45 -  ("ac_plus_times", (Context.theory_name @{theory}, prep_rls' ac_plus_times)), 
   21.46 -  ("rearrange_assoc", (Context.theory_name @{theory}, prep_rls' rearrange_assoc))]\<close>
   21.47 +setup_rule
   21.48 +  make_polytest = \<open>prep_rls' make_polytest\<close> and
   21.49 +  expand_binomtest = \<open>prep_rls' expand_binomtest\<close>
   21.50 +setup_rule
   21.51 +  norm_equation = \<open>prep_rls' norm_equation\<close> and
   21.52 +  ac_plus_times = \<open>prep_rls' ac_plus_times\<close> and
   21.53 +  rearrange_assoc = \<open>prep_rls' rearrange_assoc\<close>
   21.54  
   21.55  section \<open>problems\<close>
   21.56  setup \<open>KEStore_Elems.add_pbts

    22.1 --- a/src/Tools/isac/Knowledge/Test_Build_Thydata.thy	Wed May 26 16:19:41 2021 +0200
    22.2 +++ b/src/Tools/isac/Knowledge/Test_Build_Thydata.thy	Wed May 26 16:24:05 2021 +0200
    22.3 @@ -28,9 +28,9 @@
    22.4  val prep_rls' = Auto_Prog.prep_rls @{theory};
    22.5  \<close>
    22.6  
    22.7 -setup \<open>KEStore_Elems.add_rlss 
    22.8 -  [("rls111", (Context.theory_name @{theory}, prep_rls' rls111)),
    22.9 -   ("rls222", (Context.theory_name @{theory}, prep_rls' rls222))]\<close>
   22.10 +setup_rule
   22.11 +  rls111 = \<open>prep_rls' rls111\<close> and
   22.12 +  rls222 = \<open>prep_rls' rls222\<close>
   22.13  
   22.14  ML \<open>
   22.15    @{thm refl};

    23.1 --- a/src/Tools/isac/ProgLang/ListC.thy	Wed May 26 16:19:41 2021 +0200
    23.2 +++ b/src/Tools/isac/ProgLang/ListC.thy	Wed May 26 16:24:05 2021 +0200
    23.3 @@ -178,7 +178,7 @@
    23.4         Rule_Def.Thm ("zip_Nil",ThmC_Def.numerals_to_Free @{thm zip_Nil})],
    23.5      scr = Rule_Def.Empty_Prog}: Rule_Set.T;
    23.6  \<close>
    23.7 -setup \<open>KEStore_Elems.add_rlss [("prog_expr", (Context.theory_name @{theory}, prog_expr))]\<close>
    23.8 +setup_rule prog_expr = prog_expr
    23.9  
   23.10  ML \<open>
   23.11  \<close> ML \<open>

    24.1 --- a/src/Tools/isac/ProgLang/Prog_Expr.thy	Wed May 26 16:19:41 2021 +0200
    24.2 +++ b/src/Tools/isac/ProgLang/Prog_Expr.thy	Wed May 26 16:24:05 2021 +0200
    24.3 @@ -533,7 +533,8 @@
    24.4  \<close>
    24.5  
    24.6  subsection \<open>setup for rule-sets and ML-functions\<close>
    24.7 -setup \<open>KEStore_Elems.add_rlss [("prog_expr", (Context.theory_name @{theory}, prog_expr))]\<close>
    24.8 +
    24.9 +setup_rule prog_expr = prog_expr
   24.10  setup \<open>KEStore_Elems.add_calcs
   24.11    [("matches", ("Prog_Expr.matches", Prog_Expr.eval_matches "#matches_")),
   24.12      ("matchsub", ("Prog_Expr.matchsub", Prog_Expr.eval_matchsub "#matchsub_")),