1.1 --- a/src/Tools/isac/Knowledge/Base_Tools.thy	Mon Jun 21 15:50:58 2021 +0200
     1.2 +++ b/src/Tools/isac/Knowledge/Base_Tools.thy	Mon Jun 21 16:18:27 2021 +0200
     1.3 @@ -25,21 +25,21 @@
     1.4  subsection \<open>setup for ML-functions\<close>
     1.5  text \<open>required by "eval_binop" below\<close>
     1.6  setup \<open>KEStore_Elems.add_calcs
     1.7 -  [ ("occurs_in", ("Prog_Expr.occurs_in", Prog_Expr.eval_occurs_in "#occurs_in_")),
     1.8 -    ("some_occur_in", ("Prog_Expr.some_occur_in", Prog_Expr.eval_some_occur_in "#some_occur_in_")),
     1.9 -    ("is_atom", ("Prog_Expr.is_atom", Prog_Expr.eval_is_atom "#is_atom_")),
    1.10 -    ("is_even", ("Prog_Expr.is_even", Prog_Expr.eval_is_even "#is_even_")),
    1.11 -    ("is_const", ("Prog_Expr.is_const", Prog_Expr.eval_const "#is_const_")),
    1.12 +  [ ("occurs_in", (\<^const_name>\<open>occurs_in\<close>, Prog_Expr.eval_occurs_in "#occurs_in_")),
    1.13 +    ("some_occur_in", (\<^const_name>\<open>some_occur_in\<close>, Prog_Expr.eval_some_occur_in "#some_occur_in_")),
    1.14 +    ("is_atom", (\<^const_name>\<open>is_atom\<close>, Prog_Expr.eval_is_atom "#is_atom_")),
    1.15 +    ("is_even", (\<^const_name>\<open>is_even\<close>, Prog_Expr.eval_is_even "#is_even_")),
    1.16 +    ("is_const", (\<^const_name>\<open>is_const\<close>, Prog_Expr.eval_const "#is_const_")),
    1.17      ("le", (\<^const_name>\<open>less\<close>, Prog_Expr.eval_equ "#less_")),
    1.18      ("leq", (\<^const_name>\<open>less_eq\<close>, Prog_Expr.eval_equ "#less_equal_")),
    1.19 -    ("ident", ("Prog_Expr.ident", Prog_Expr.eval_ident "#ident_")),
    1.20 +    ("ident", (\<^const_name>\<open>ident\<close>, Prog_Expr.eval_ident "#ident_")),
    1.21      ("equal", (\<^const_name>\<open>HOL.eq\<close>, Prog_Expr.eval_equal "#equal_")),
    1.22      ("PLUS", (\<^const_name>\<open>plus\<close>, (**)eval_binop "#add_")),
    1.23      ("MINUS", (\<^const_name>\<open>minus\<close>, (**)eval_binop "#sub_")),
    1.24      ("TIMES", (\<^const_name>\<open>times\<close>, (**)eval_binop "#mult_")),
    1.25      ("DIVIDE", (\<^const_name>\<open>divide\<close>, Prog_Expr.eval_cancel "#divide_e")),
    1.26      ("POWER",(\<^const_name>\<open>powr\<close>, (**)eval_binop "#power_")),
    1.27 -    ("boollist2sum", ("Prog_Expr.boollist2sum", Prog_Expr.eval_boollist2sum ""))]\<close>
    1.28 +    ("boollist2sum", (\<^const_name>\<open>boollist2sum\<close>, Prog_Expr.eval_boollist2sum ""))]\<close>
    1.29  
    1.30  subsection \<open>rewrite-order for rule-sets\<close>
    1.31  ML \<open>

     2.1 --- a/src/Tools/isac/Knowledge/Diff.thy	Mon Jun 21 15:50:58 2021 +0200
     2.2 +++ b/src/Tools/isac/Knowledge/Diff.thy	Mon Jun 21 16:18:27 2021 +0200
     2.3 @@ -100,7 +100,7 @@
     2.4    | eval_primed _ _ _ _ = NONE;
     2.5  \<close>
     2.6  setup \<open>KEStore_Elems.add_calcs
     2.7 -  [("primed", ("Diff.primed", eval_primed "#primed"))]\<close>
     2.8 +  [("primed", (\<^const_name>\<open>primed\<close>, eval_primed "#primed"))]\<close>
     2.9  ML \<open>
    2.10  (** rulesets **)
    2.11  

     3.1 --- a/src/Tools/isac/Knowledge/EqSystem.thy	Mon Jun 21 15:50:58 2021 +0200
     3.2 +++ b/src/Tools/isac/Knowledge/EqSystem.thy	Mon Jun 21 16:18:27 2021 +0200
     3.3 @@ -77,9 +77,7 @@
     3.4    | eval_occur_exactly_in _ _ _ _ = NONE;
     3.5  \<close>
     3.6  setup \<open>KEStore_Elems.add_calcs
     3.7 -  [("occur_exactly_in",
     3.8 -	    ("EqSystem.occur_exactly_in",
     3.9 -	      eval_occur_exactly_in "#eval_occur_exactly_in_"))]\<close>
    3.10 +  [("occur_exactly_in", (\<^const_name>\<open>occur_exactly_in\<close>, eval_occur_exactly_in "#eval_occur_exactly_in_"))]\<close>
    3.11  ML \<open>
    3.12  (** rewrite order 'ord_simplify_System' **)
    3.13  

     4.1 --- a/src/Tools/isac/Knowledge/Integrate.thy	Mon Jun 21 15:50:58 2021 +0200
     4.2 +++ b/src/Tools/isac/Knowledge/Integrate.thy	Mon Jun 21 16:18:27 2021 +0200
     4.3 @@ -103,8 +103,8 @@
     4.4    | eval_is_f_x _ _ _ _ = NONE;
     4.5  \<close>
     4.6  setup \<open>KEStore_Elems.add_calcs
     4.7 -  [("add_new_c", ("Integrate.add_new_c", eval_add_new_c "add_new_c_")),
     4.8 -    ("is_f_x", ("Integrate.is_f_x", eval_is_f_x "is_f_idextifier_"))]\<close>
     4.9 +  [("add_new_c", ("Integrate.add_new_c" (* FIXME proper const!? *), eval_add_new_c "add_new_c_")),
    4.10 +    ("is_f_x", (\<^const_name>\<open>is_f_x\<close>, eval_is_f_x "is_f_idextifier_"))]\<close>
    4.11  ML \<open>
    4.12  (** rulesets **)
    4.13  

     5.1 --- a/src/Tools/isac/Knowledge/Poly.thy	Mon Jun 21 15:50:58 2021 +0200
     5.2 +++ b/src/Tools/isac/Knowledge/Poly.thy	Mon Jun 21 16:18:27 2021 +0200
     5.3 @@ -635,14 +635,13 @@
     5.4    | eval_is_multUnordered _ _ _ _ = NONE; 
     5.5  \<close>
     5.6  setup \<open>KEStore_Elems.add_calcs
     5.7 -  [("is_polyrat_in", ("Poly.is_polyrat_in",
     5.8 -		    eval_is_polyrat_in "#eval_is_polyrat_in")),
     5.9 -    ("is_expanded_in", ("Poly.is_expanded_in", eval_is_expanded_in "")),
    5.10 -    ("is_poly_in", ("Poly.is_poly_in", eval_is_poly_in "")),
    5.11 -    ("has_degree_in", ("Poly.has_degree_in", eval_has_degree_in "")),
    5.12 -    ("is_polyexp", ("Poly.is_polyexp", eval_is_polyexp "")),
    5.13 -    ("is_multUnordered", ("Poly.is_multUnordered", eval_is_multUnordered"")),
    5.14 -    ("is_addUnordered", ("Poly.is_addUnordered", eval_is_addUnordered ""))]\<close>
    5.15 +  [("is_polyrat_in", (\<^const_name>\<open>is_polyrat_in\<close>, eval_is_polyrat_in "#eval_is_polyrat_in")),
    5.16 +    ("is_expanded_in", (\<^const_name>\<open>is_expanded_in\<close>, eval_is_expanded_in "")),
    5.17 +    ("is_poly_in", (\<^const_name>\<open>is_poly_in\<close>, eval_is_poly_in "")),
    5.18 +    ("has_degree_in", (\<^const_name>\<open>has_degree_in\<close>, eval_has_degree_in "")),
    5.19 +    ("is_polyexp", (\<^const_name>\<open>is_polyexp\<close>, eval_is_polyexp "")),
    5.20 +    ("is_multUnordered", (\<^const_name>\<open>is_multUnordered\<close>, eval_is_multUnordered"")),
    5.21 +    ("is_addUnordered", (\<^const_name>\<open>is_addUnordered\<close>, eval_is_addUnordered ""))]\<close>
    5.22  
    5.23  subsection \<open>rule-sets\<close>
    5.24  subsubsection \<open>without specific order\<close>

     6.1 --- a/src/Tools/isac/Knowledge/RatEq.thy	Mon Jun 21 15:50:58 2021 +0200
     6.2 +++ b/src/Tools/isac/Knowledge/RatEq.thy	Mon Jun 21 16:18:27 2021 +0200
     6.3 @@ -74,7 +74,7 @@
     6.4    | eval_is_ratequation_in _ _ _ _ = ((*tracing"### nichts matcht";*) NONE);
     6.5  \<close>
     6.6  setup \<open>KEStore_Elems.add_calcs
     6.7 -  [("is_ratequation_in", ("RatEq.is_ratequation_in", eval_is_ratequation_in ""))]\<close>
     6.8 +  [("is_ratequation_in", (\<^const_name>\<open>is_ratequation_in\<close>, eval_is_ratequation_in ""))]\<close>
     6.9  
    6.10  subsection \<open>rule-sets\<close>
    6.11  ML \<open>

     7.1 --- a/src/Tools/isac/Knowledge/Rational.thy	Mon Jun 21 15:50:58 2021 +0200
     7.2 +++ b/src/Tools/isac/Knowledge/Rational.thy	Mon Jun 21 16:18:27 2021 +0200
     7.3 @@ -459,7 +459,7 @@
     7.4    | eval_is_expanded _ _ _ _ = NONE;
     7.5  \<close>
     7.6  setup \<open>KEStore_Elems.add_calcs
     7.7 -  [("is_expanded", ("Rational.is_expanded", eval_is_expanded ""))]\<close>
     7.8 +  [("is_expanded", (\<^const_name>\<open>is_expanded\<close>, eval_is_expanded ""))]\<close>
     7.9  ML \<open>
    7.10  val rational_erls = 
    7.11    Rule_Set.merge "rational_erls" calculate_Rational 

     8.1 --- a/src/Tools/isac/Knowledge/RootEq.thy	Mon Jun 21 15:50:58 2021 +0200
     8.2 +++ b/src/Tools/isac/Knowledge/RootEq.thy	Mon Jun 21 16:18:27 2021 +0200
     8.3 @@ -170,9 +170,9 @@
     8.4    | eval_is_normSqrtTerm_in _ _ _ _ = ((*tracing"### nichts matcht";*) NONE);
     8.5  \<close>
     8.6  setup \<open>KEStore_Elems.add_calcs
     8.7 -  [("is_rootTerm_in", ("RootEq.is_rootTerm_in", eval_is_rootTerm_in"")),
     8.8 -    ("is_sqrtTerm_in", ("RootEq.is_sqrtTerm_in", eval_is_sqrtTerm_in"")),
     8.9 -    ("is_normSqrtTerm_in", ("RootEq.is_normSqrtTerm_in", eval_is_normSqrtTerm_in""))]\<close>
    8.10 +  [("is_rootTerm_in", (\<^const_name>\<open>is_rootTerm_in\<close>, eval_is_rootTerm_in"")),
    8.11 +    ("is_sqrtTerm_in", (\<^const_name>\<open>is_sqrtTerm_in\<close>, eval_is_sqrtTerm_in"")),
    8.12 +    ("is_normSqrtTerm_in", (\<^const_name>\<open>is_normSqrtTerm_in\<close>, eval_is_normSqrtTerm_in""))]\<close>
    8.13  
    8.14  subsection \<open>rule-sets\<close>
    8.15  ML \<open>

     9.1 --- a/src/Tools/isac/Knowledge/RootRatEq.thy	Mon Jun 21 15:50:58 2021 +0200
     9.2 +++ b/src/Tools/isac/Knowledge/RootRatEq.thy	Mon Jun 21 16:18:27 2021 +0200
     9.3 @@ -62,7 +62,7 @@
     9.4    | eval_is_rootRatAddTerm_in _ _ _ _ = ((*tracing"### nichts matcht";*) NONE);
     9.5  \<close>
     9.6  setup \<open>KEStore_Elems.add_calcs
     9.7 -  [("is_rootRatAddTerm_in", ("RootRatEq.is_rootRatAddTerm_in", eval_is_rootRatAddTerm_in""))]\<close>
     9.8 +  [("is_rootRatAddTerm_in", (\<^const_name>\<open>is_rootRatAddTerm_in\<close>, eval_is_rootRatAddTerm_in""))]\<close>
     9.9  
    9.10  subsection \<open>rule-sets\<close>
    9.11  ML \<open>

    10.1 --- a/src/Tools/isac/Knowledge/Test.thy	Mon Jun 21 15:50:58 2021 +0200
    10.2 +++ b/src/Tools/isac/Knowledge/Test.thy	Mon Jun 21 16:18:27 2021 +0200
    10.3 @@ -273,9 +273,9 @@
    10.4  	| eval_precond_rootpbl _ _ _ _ = NONE;
    10.5  \<close>
    10.6  setup \<open>KEStore_Elems.add_calcs
    10.7 -  [("contains_root", ("Test.contains_root", eval_contains_root"#contains_root_")),
    10.8 -    ("Test.precond_rootmet", ("Test.precond_rootmet", eval_precond_rootmet"#Test.precond_rootmet_")),
    10.9 -    ("Test.precond_rootpbl", ("Test.precond_rootpbl",
   10.10 +  [("contains_root", (\<^const_name>\<open>contains_root\<close>, eval_contains_root"#contains_root_")),
   10.11 +    ("Test.precond_rootmet", (\<^const_name>\<open>Test.precond_rootmet\<close>, eval_precond_rootmet"#Test.precond_rootmet_")),
   10.12 +    ("Test.precond_rootpbl", (\<^const_name>\<open>Test.precond_rootpbl\<close>,
   10.13          eval_precond_rootpbl"#Test.precond_rootpbl_"))]
   10.14  \<close>
   10.15  ML \<open>

    11.1 --- a/src/Tools/isac/ProgLang/Prog_Expr.thy	Mon Jun 21 15:50:58 2021 +0200
    11.2 +++ b/src/Tools/isac/ProgLang/Prog_Expr.thy	Mon Jun 21 16:18:27 2021 +0200
    11.3 @@ -536,11 +536,11 @@
    11.4  
    11.5  rule_set_knowledge prog_expr = prog_expr
    11.6  setup \<open>KEStore_Elems.add_calcs
    11.7 -  [("matches", ("Prog_Expr.matches", Prog_Expr.eval_matches "#matches_")),
    11.8 -    ("matchsub", ("Prog_Expr.matchsub", Prog_Expr.eval_matchsub "#matchsub_")),
    11.9 -    ("Vars", ("Prog_Expr.Vars", Prog_Expr.eval_var "#Vars_")),
   11.10 -    ("lhs", ("Prog_Expr.lhs", Prog_Expr.eval_lhs "")),
   11.11 -    ("rhs", ("Prog_Expr.rhs", Prog_Expr.eval_rhs ""))]\<close>
   11.12 +  [("matches", (\<^const_name>\<open>matches\<close>, Prog_Expr.eval_matches "#matches_")),
   11.13 +    ("matchsub", (\<^const_name>\<open>matchsub\<close>, Prog_Expr.eval_matchsub "#matchsub_")),
   11.14 +    ("Vars", (\<^const_name>\<open>Vars\<close>, Prog_Expr.eval_var "#Vars_")),
   11.15 +    ("lhs", (\<^const_name>\<open>lhs\<close>, Prog_Expr.eval_lhs "")),
   11.16 +    ("rhs", (\<^const_name>\<open>rhs\<close>, Prog_Expr.eval_rhs ""))]\<close>
   11.17  (*\\------------------------- from Tools .thy-------------------------------------------------//*)
   11.18  ML \<open>
   11.19  \<close> ML \<open>