1.1 --- a/src/Tools/isac/BaseDefinitions/Know_Store.thy	Wed Jun 09 20:28:42 2021 +0200
     1.2 +++ b/src/Tools/isac/BaseDefinitions/Know_Store.thy	Thu Jun 10 11:54:20 2021 +0200
     1.3 @@ -17,7 +17,7 @@
     1.4  
     1.5  theory Know_Store
     1.6    imports Complex_Main
     1.7 -  keywords "setup_rule" :: thy_decl
     1.8 +  keywords "rule_set_knowledge" :: thy_decl
     1.9  begin
    1.10  
    1.11  setup \<open>
    1.12 @@ -188,7 +188,7 @@
    1.13      flat (separate (ml ",") (map (ml_rule thy) args)) @ ml "])";
    1.14  
    1.15  val _ =
    1.16 -  Outer_Syntax.command \<^command_keyword>\<open>setup_rule\<close> "setup ISAC rules"
    1.17 +  Outer_Syntax.command \<^command_keyword>\<open>rule_set_knowledge\<close> "register ISAC rule set to Knowledge Store"
    1.18      (Parse.and_list1 parse_rule >> (fn args => Toplevel.theory (fn thy =>
    1.19        thy |> Context.theory_map
    1.20          (ML_Context.expression (Position.thread_data ()) (ml_rules thy args)))));
    1.21 @@ -238,7 +238,7 @@
    1.22  fun get_thes () = get_ref_thy () |> KEStore_Elems.get_thes;
    1.23  \<close>
    1.24  
    1.25 -setup_rule
    1.26 +rule_set_knowledge
    1.27    empty = \<open>Rule_Set.empty\<close> and
    1.28    e_rrls = \<open>Rule_Set.e_rrls\<close>
    1.29  

     2.1 --- a/src/Tools/isac/Knowledge/Base_Tools.thy	Wed Jun 09 20:28:42 2021 +0200
     2.2 +++ b/src/Tools/isac/Knowledge/Base_Tools.thy	Thu Jun 10 11:54:20 2021 +0200
     2.3 @@ -150,7 +150,7 @@
     2.4  
     2.5  subsection \<open>setup for extended rule-set\<close>
     2.6  
     2.7 -setup_rule prog_expr = \<open>Auto_Prog.prep_rls @{theory} prog_expr\<close>
     2.8 +rule_set_knowledge prog_expr = \<open>Auto_Prog.prep_rls @{theory} prog_expr\<close>
     2.9  
    2.10  ML \<open>
    2.11  \<close> ML \<open>

     3.1 --- a/src/Tools/isac/Knowledge/Diff.thy	Wed Jun 09 20:28:42 2021 +0200
     3.2 +++ b/src/Tools/isac/Knowledge/Diff.thy	Thu Jun 10 11:54:20 2021 +0200
     3.3 @@ -232,7 +232,7 @@
     3.4       rules = [Rule.Rls_ diff_rules, Rule.Rls_ norm_Poly ],
     3.5       scr = Rule.Empty_Prog};
     3.6  \<close>
     3.7 -setup_rule
     3.8 +rule_set_knowledge
     3.9    erls_diff = \<open>prep_rls' erls_diff\<close> and
    3.10    diff_rules = \<open>prep_rls' diff_rules\<close> and
    3.11    norm_diff = \<open>prep_rls' norm_diff\<close> and

     4.1 --- a/src/Tools/isac/Knowledge/DiffApp.thy	Wed Jun 09 20:28:42 2021 +0200
     4.2 +++ b/src/Tools/isac/Knowledge/DiffApp.thy	Thu Jun 10 11:54:20 2021 +0200
     4.3 @@ -59,7 +59,7 @@
     4.4      scr = Rule.Empty_Prog
     4.5      });
     4.6  \<close>
     4.7 -setup_rule eval_rls = \<open>eval_rls\<close>
     4.8 +rule_set_knowledge eval_rls = \<open>eval_rls\<close>
     4.9  
    4.10  (** problem types **)
    4.11  setup \<open>KEStore_Elems.add_pbts
    4.12 @@ -199,7 +199,7 @@
    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_rule prog_expr = \<open>prog_expr\<close>
    4.17 +rule_set_knowledge prog_expr = \<open>prog_expr\<close>
    4.18  ML \<open>
    4.19  \<close> ML \<open>
    4.20  \<close> ML \<open>

     5.1 --- a/src/Tools/isac/Knowledge/EqSystem.thy	Wed Jun 09 20:28:42 2021 +0200
     5.2 +++ b/src/Tools/isac/Knowledge/EqSystem.thy	Thu Jun 10 11:54:20 2021 +0200
     5.3 @@ -393,7 +393,7 @@
     5.4  	 scr = Rule.Empty_Prog};
     5.5  \<close>
     5.6  
     5.7 -setup_rule
     5.8 +rule_set_knowledge
     5.9    simplify_System_parenthesized = \<open>prep_rls' simplify_System_parenthesized\<close> and
    5.10    simplify_System = \<open>prep_rls' simplify_System\<close> and
    5.11    isolate_bdvs = \<open>prep_rls' isolate_bdvs\<close> and

     6.1 --- a/src/Tools/isac/Knowledge/Equation.thy	Wed Jun 09 20:28:42 2021 +0200
     6.2 +++ b/src/Tools/isac/Knowledge/Equation.thy	Thu Jun 10 11:54:20 2021 +0200
     6.3 @@ -40,7 +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_rule univariate_equation_prls = \<open>Auto_Prog.prep_rls @{theory} univariate_equation_prls\<close>
     6.8 +rule_set_knowledge univariate_equation_prls = \<open>Auto_Prog.prep_rls @{theory} univariate_equation_prls\<close>
     6.9  setup \<open>KEStore_Elems.add_pbts
    6.10    [(Problem.prep_input thy "pbl_equ" [] Problem.id_empty
    6.11        (["equation"],

     7.1 --- a/src/Tools/isac/Knowledge/InsSort.thy	Wed Jun 09 20:28:42 2021 +0200
     7.2 +++ b/src/Tools/isac/Knowledge/InsSort.thy	Thu Jun 10 11:54:20 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_rule ins_sort = ins_sort
     7.8 +rule_set_knowledge 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 Jun 09 20:28:42 2021 +0200
     8.2 +++ b/src/Tools/isac/Knowledge/Integrate.thy	Thu Jun 10 11:54:20 2021 +0200
     8.3 @@ -319,7 +319,7 @@
     8.4  
     8.5  val prep_rls' = Auto_Prog.prep_rls @{theory};
     8.6  \<close>
     8.7 -setup_rule
     8.8 +rule_set_knowledge
     8.9    integration_rules = \<open>prep_rls' integration_rules\<close> and
    8.10    add_new_c = \<open>prep_rls' add_new_c\<close> and
    8.11    simplify_Integral = \<open>prep_rls' simplify_Integral\<close> and

     9.1 --- a/src/Tools/isac/Knowledge/Inverse_Z_Transform.thy	Wed Jun 09 20:28:42 2021 +0200
     9.2 +++ b/src/Tools/isac/Knowledge/Inverse_Z_Transform.thy	Thu Jun 10 11:54:20 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_rule inverse_z = inverse_z
     9.8 +rule_set_knowledge 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 Jun 09 20:28:42 2021 +0200
    10.2 +++ b/src/Tools/isac/Knowledge/LinEq.thy	Thu Jun 10 11:54:20 2021 +0200
    10.3 @@ -64,7 +64,7 @@
    10.4       *)
    10.5      ];
    10.6  \<close>
    10.7 -setup_rule LinEq_erls = LinEq_erls
    10.8 +rule_set_knowledge LinEq_erls = LinEq_erls
    10.9  ML \<open>
   10.10      
   10.11  val LinPoly_simplify = prep_rls'(
   10.12 @@ -86,7 +86,7 @@
   10.13  		],
   10.14         scr = Rule.Empty_Prog});
   10.15  \<close>
   10.16 -setup_rule LinPoly_simplify = LinPoly_simplify
   10.17 +rule_set_knowledge LinPoly_simplify = LinPoly_simplify
   10.18  ML \<open>
   10.19  
   10.20  (*isolate the bound variable in an linear equation; 'bdv' is a meta-constant*)
   10.21 @@ -106,7 +106,7 @@
   10.22  	      ],
   10.23       scr = Rule.Empty_Prog});
   10.24  \<close>
   10.25 -setup_rule LinEq_simplify = LinEq_simplify
   10.26 +rule_set_knowledge LinEq_simplify = LinEq_simplify
   10.27  
   10.28  (*----------------------------- problem types --------------------------------*)
   10.29  (* ---------linear----------- *)

    11.1 --- a/src/Tools/isac/Knowledge/Partial_Fractions.thy	Wed Jun 09 20:28:42 2021 +0200
    11.2 +++ b/src/Tools/isac/Knowledge/Partial_Fractions.thy	Thu Jun 10 11:54:20 2021 +0200
    11.3 @@ -134,7 +134,7 @@
    11.4  \<close>
    11.5  
    11.6  text \<open>store the rule set for math engine\<close>
    11.7 -setup_rule
    11.8 +rule_set_knowledge
    11.9    ansatz_rls = ansatz_rls and
   11.10    multiply_ansatz = multiply_ansatz and
   11.11    equival_trans = equival_trans

    12.1 --- a/src/Tools/isac/Knowledge/Poly.thy	Wed Jun 09 20:28:42 2021 +0200
    12.2 +++ b/src/Tools/isac/Knowledge/Poly.thy	Thu Jun 10 11:54:20 2021 +0200
    12.3 @@ -1402,7 +1402,7 @@
    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_rule
    12.8 +rule_set_knowledge
    12.9    norm_Poly = \<open>prep_rls' norm_Poly\<close> and
   12.10    Poly_erls = \<open>prep_rls' Poly_erls\<close> (*FIXXXME:del with rls.rls'*) and
   12.11    expand = \<open>prep_rls' expand\<close> and

    13.1 --- a/src/Tools/isac/Knowledge/PolyEq.thy	Wed Jun 09 20:28:42 2021 +0200
    13.2 +++ b/src/Tools/isac/Knowledge/PolyEq.thy	Thu Jun 10 11:54:20 2021 +0200
    13.3 @@ -425,7 +425,7 @@
    13.4         scr = Rule.Empty_Prog
    13.5         });
    13.6  \<close>
    13.7 -setup_rule
    13.8 +rule_set_knowledge
    13.9    cancel_leading_coeff = cancel_leading_coeff and
   13.10    complete_square = complete_square and
   13.11    PolyEq_erls = PolyEq_erls and
   13.12 @@ -757,7 +757,7 @@
   13.13         scr = Rule.Empty_Prog
   13.14        });
   13.15  \<close>
   13.16 -setup_rule
   13.17 +rule_set_knowledge
   13.18    d0_polyeq_simplify = d0_polyeq_simplify and
   13.19    d1_polyeq_simplify = d1_polyeq_simplify and
   13.20    d2_polyeq_simplify = d2_polyeq_simplify and
   13.21 @@ -1329,7 +1329,7 @@
   13.22  	       ],
   13.23        scr = Rule.Empty_Prog});      
   13.24  \<close>
   13.25 -setup_rule
   13.26 +rule_set_knowledge
   13.27    order_add_mult_in = order_add_mult_in and
   13.28    collect_bdv = collect_bdv and
   13.29    make_polynomial_in = make_polynomial_in and

    14.1 --- a/src/Tools/isac/Knowledge/PolyMinus.thy	Wed Jun 09 20:28:42 2021 +0200
    14.2 +++ b/src/Tools/isac/Knowledge/PolyMinus.thy	Thu Jun 10 11:54:20 2021 +0200
    14.3 @@ -389,7 +389,7 @@
    14.4  		Rule.Eval ("Groups.minus_class.minus", (**)eval_binop "#subtr_")
    14.5  		];
    14.6  \<close>
    14.7 -setup_rule
    14.8 +rule_set_knowledge
    14.9    ordne_alphabetisch = \<open>prep_rls' ordne_alphabetisch\<close> and
   14.10    fasse_zusammen = \<open>prep_rls' fasse_zusammen\<close> and
   14.11    verschoenere = \<open>prep_rls' verschoenere\<close> and

    15.1 --- a/src/Tools/isac/Knowledge/RatEq.thy	Wed Jun 09 20:28:42 2021 +0200
    15.2 +++ b/src/Tools/isac/Knowledge/RatEq.thy	Thu Jun 10 11:54:20 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_rule rateq_erls = rateq_erls
    15.8 -setup_rule RatEq_eliminate = RatEq_eliminate
    15.9 -setup_rule RatEq_simplify = RatEq_simplify
   15.10 +rule_set_knowledge rateq_erls = rateq_erls
   15.11 +rule_set_knowledge RatEq_eliminate = RatEq_eliminate
   15.12 +rule_set_knowledge 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 Jun 09 20:28:42 2021 +0200
    16.2 +++ b/src/Tools/isac/Knowledge/Rational.thy	Thu Jun 10 11:54:20 2021 +0200
    16.3 @@ -852,7 +852,7 @@
    16.4      scr = Rule.Empty_Prog});
    16.5  \<close>
    16.6  
    16.7 -setup_rule
    16.8 +rule_set_knowledge
    16.9    calculate_Rational = calculate_Rational and
   16.10    calc_rat_erls = calc_rat_erls and
   16.11    rational_erls = rational_erls and

    17.1 --- a/src/Tools/isac/Knowledge/Root.thy	Wed Jun 09 20:28:42 2021 +0200
    17.2 +++ b/src/Tools/isac/Knowledge/Root.thy	Thu Jun 10 11:54:20 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_rule Root_erls = Root_erls
    17.8 +rule_set_knowledge 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_rule make_rooteq = make_rooteq
   17.17 +rule_set_knowledge make_rooteq = make_rooteq
   17.18  ML \<open>
   17.19  
   17.20  val prep_rls' = Auto_Prog.prep_rls @{theory};
   17.21 @@ -328,7 +328,7 @@
   17.22        scr = Rule.Empty_Prog
   17.23         });      
   17.24  \<close>
   17.25 -setup_rule expand_rootbinoms = expand_rootbinoms
   17.26 +rule_set_knowledge expand_rootbinoms = expand_rootbinoms
   17.27  ML \<open>
   17.28  \<close> ML \<open>
   17.29  \<close> ML \<open>

    18.1 --- a/src/Tools/isac/Knowledge/RootEq.thy	Wed Jun 09 20:28:42 2021 +0200
    18.2 +++ b/src/Tools/isac/Knowledge/RootEq.thy	Thu Jun 10 11:54:20 2021 +0200
    18.3 @@ -433,7 +433,7 @@
    18.4         scr = Rule.Empty_Prog
    18.5      });
    18.6  \<close>
    18.7 -setup_rule
    18.8 +rule_set_knowledge
    18.9    RootEq_erls = RootEq_erls and
   18.10    rooteq_srls = rooteq_srls and
   18.11    sqrt_isolate = sqrt_isolate and

    19.1 --- a/src/Tools/isac/Knowledge/RootRat.thy	Wed Jun 09 20:28:42 2021 +0200
    19.2 +++ b/src/Tools/isac/Knowledge/RootRat.thy	Thu Jun 10 11:54:20 2021 +0200
    19.3 @@ -27,7 +27,7 @@
    19.4  
    19.5  val prep_rls' = Auto_Prog.prep_rls @{theory};
    19.6  \<close>
    19.7 -setup_rule
    19.8 +rule_set_knowledge
    19.9    rootrat_erls = \<open>prep_rls' rootrat_erls\<close> and
   19.10    calculate_RootRat = \<open>prep_rls' calculate_RootRat\<close>
   19.11  ML \<open>

    20.1 --- a/src/Tools/isac/Knowledge/RootRatEq.thy	Wed Jun 09 20:28:42 2021 +0200
    20.2 +++ b/src/Tools/isac/Knowledge/RootRatEq.thy	Thu Jun 10 11:54:20 2021 +0200
    20.3 @@ -116,7 +116,7 @@
    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_rule
    20.8 +rule_set_knowledge
    20.9    RooRatEq_erls = RooRatEq_erls and
   20.10    rootrat_solve = rootrat_solve
   20.11  

    21.1 --- a/src/Tools/isac/Knowledge/Test.thy	Wed Jun 09 20:28:42 2021 +0200
    21.2 +++ b/src/Tools/isac/Knowledge/Test.thy	Thu Jun 10 11:54:20 2021 +0200
    21.3 @@ -436,7 +436,7 @@
    21.4        scr = Rule.Empty_Prog
    21.5        };      
    21.6  \<close>
    21.7 -setup_rule testerls = \<open>prep_rls' testerls\<close>
    21.8 +rule_set_knowledge testerls = \<open>prep_rls' testerls\<close>
    21.9  
   21.10  ML \<open>
   21.11  (*make () dissappear*)   
   21.12 @@ -561,7 +561,7 @@
   21.13  	};      
   21.14  \<close>
   21.15  ML \<open>val prep_rls' = Auto_Prog.prep_rls @{theory};\<close>
   21.16 -setup_rule
   21.17 +rule_set_knowledge
   21.18    Test_simplify = \<open>prep_rls' Test_simplify\<close> and
   21.19    tval_rls = \<open>prep_rls' tval_rls\<close> and
   21.20    isolate_root = \<open>prep_rls' isolate_root\<close> and
   21.21 @@ -766,10 +766,10 @@
   21.22  (*Program ((Thm.term_of o the o (parse thy)) scr_expand_binomtest)*)
   21.23        };      
   21.24  \<close>
   21.25 -setup_rule
   21.26 +rule_set_knowledge
   21.27    make_polytest = \<open>prep_rls' make_polytest\<close> and
   21.28    expand_binomtest = \<open>prep_rls' expand_binomtest\<close>
   21.29 -setup_rule
   21.30 +rule_set_knowledge
   21.31    norm_equation = \<open>prep_rls' norm_equation\<close> and
   21.32    ac_plus_times = \<open>prep_rls' ac_plus_times\<close> and
   21.33    rearrange_assoc = \<open>prep_rls' rearrange_assoc\<close>

    22.1 --- a/src/Tools/isac/Knowledge/Test_Build_Thydata.thy	Wed Jun 09 20:28:42 2021 +0200
    22.2 +++ b/src/Tools/isac/Knowledge/Test_Build_Thydata.thy	Thu Jun 10 11:54:20 2021 +0200
    22.3 @@ -28,7 +28,7 @@
    22.4  val prep_rls' = Auto_Prog.prep_rls @{theory};
    22.5  \<close>
    22.6  
    22.7 -setup_rule
    22.8 +rule_set_knowledge
    22.9    rls111 = \<open>prep_rls' rls111\<close> and
   22.10    rls222 = \<open>prep_rls' rls222\<close>
   22.11  

    23.1 --- a/src/Tools/isac/ProgLang/ListC.thy	Wed Jun 09 20:28:42 2021 +0200
    23.2 +++ b/src/Tools/isac/ProgLang/ListC.thy	Thu Jun 10 11:54:20 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_rule prog_expr = prog_expr
    23.8 +rule_set_knowledge 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 Jun 09 20:28:42 2021 +0200
    24.2 +++ b/src/Tools/isac/ProgLang/Prog_Expr.thy	Thu Jun 10 11:54:20 2021 +0200
    24.3 @@ -534,7 +534,7 @@
    24.4  
    24.5  subsection \<open>setup for rule-sets and ML-functions\<close>
    24.6  
    24.7 -setup_rule prog_expr = prog_expr
    24.8 +rule_set_knowledge prog_expr = prog_expr
    24.9  setup \<open>KEStore_Elems.add_calcs
   24.10    [("matches", ("Prog_Expr.matches", Prog_Expr.eval_matches "#matches_")),
   24.11      ("matchsub", ("Prog_Expr.matchsub", Prog_Expr.eval_matchsub "#matchsub_")),