# HG changeset patch
# User wneuper <Walther.Neuper@jku.at>
# Date 1659624517 -7200
# Node ID 03e19793d81e0285a1c11f5aa0bccae458a86065
# Parent  19bd2f740479c16e7cae473c8e58b02fb3221b65
add structure Calc_Binop

diff -r 19bd2f740479 -r 03e19793d81e TODO.md
--- a/TODO.md	Thu Aug 04 15:38:42 2022 +0200
+++ b/TODO.md	Thu Aug 04 16:48:37 2022 +0200
@@ -67,7 +67,7 @@
 
 ***** priority of WN items is top down, most urgent/simple on top
 
-* WN: Calculate.thy: add structure Calculate, also signature EXAMPLE
+* WN: add signature EXAMPLE
 * WN: MethodC.from_store throws exn 'get_pbt not found: ' ... confusing !! take 'ketype' as an argument
 
 * WN: rewriting with ctxt not complete (cause errors hard to indentify later)
diff -r 19bd2f740479 -r 03e19793d81e src/Tools/isac/Knowledge/Base_Tools.thy
--- a/src/Tools/isac/Knowledge/Base_Tools.thy	Thu Aug 04 15:38:42 2022 +0200
+++ b/src/Tools/isac/Knowledge/Base_Tools.thy	Thu Aug 04 16:48:37 2022 +0200
@@ -24,7 +24,7 @@
 
 
 subsection \<open>setup for ML-functions\<close>
-text \<open>required by "eval_binop" below\<close>
+text \<open>required by "Calc_Binop.numeric" below\<close>
 calculation occurs_in = \<open>Prog_Expr.eval_occurs_in "#occurs_in_"\<close>
 calculation some_occur_in = \<open>Prog_Expr.eval_some_occur_in "#some_occur_in_"\<close>
 calculation is_atom = \<open>Prog_Expr.eval_is_atom "#is_atom_"\<close>
@@ -33,11 +33,11 @@
 calculation leq (less_eq) = \<open>Prog_Expr.eval_equ "#less_equal_"\<close>
 calculation ident = \<open>Prog_Expr.eval_ident "#ident_"\<close>
 calculation equal (HOL.eq) = \<open>Prog_Expr.eval_equal "#equal_"\<close>
-calculation PLUS (plus) = \<open>(**)eval_binop "#add_"\<close>
-calculation MINUS (minus) = \<open>(**)eval_binop "#sub_"\<close>
-calculation TIMES (times) = \<open>(**)eval_binop "#mult_"\<close>
+calculation PLUS (plus) = \<open>(**)Calc_Binop.numeric "#add_"\<close>
+calculation MINUS (minus) = \<open>(**)Calc_Binop.numeric "#sub_"\<close>
+calculation TIMES (times) = \<open>(**)Calc_Binop.numeric "#mult_"\<close>
 calculation DIVIDE (divide) = \<open>Prog_Expr.eval_cancel "#divide_e"\<close>
-calculation POWER (realpow) = \<open>(**)eval_binop "#power_"\<close>
+calculation POWER (realpow) = \<open>(**)Calc_Binop.numeric "#power_"\<close>
 calculation boollist2sum = \<open>Prog_Expr.eval_boollist2sum ""\<close>
 
 subsection \<open>rewrite-order for rule-sets\<close>
@@ -115,11 +115,11 @@
 \<close>
 
 subsection \<open>ONCE AGAIN extend rule-set for evaluating pre-conditions and program-expressions\<close>
-text \<open>requires "eval_binop" from above\<close>
+text \<open>requires "Calc_Binop.numeric" from above\<close>
 ML \<open>
 val prog_expr = Rule_Set.append_rules "prog_expr" prog_expr [
-  \<^rule_eval>\<open>times\<close> (**)(eval_binop "#mult_"),
-	\<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_"), 
+  \<^rule_eval>\<open>times\<close> (**)(Calc_Binop.numeric "#mult_"),
+	\<^rule_eval>\<open>plus\<close> (**)(Calc_Binop.numeric "#add_"), 
 	\<^rule_eval>\<open>less\<close> (Prog_Expr.eval_equ "#less_"),
 	\<^rule_eval>\<open>less_eq\<close> (Prog_Expr.eval_equ "#less_equal_"),
 	\<^rule_eval>\<open>Prog_Expr.ident\<close> (Prog_Expr.eval_ident "#ident_"),
@@ -135,7 +135,7 @@
     erls = Rule_Def.Repeat {id = "list_elrs", preconds = [], rew_ord = ("termlessI", termlessI), 
     erls = Rule_Set.empty, srls = Rule_Set.Empty, calc = [], errpatts = [],
     rules = [
-      \<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_"),
+      \<^rule_eval>\<open>plus\<close> (**)(Calc_Binop.numeric "#add_"),
       \<^rule_eval>\<open>less\<close> (Prog_Expr.eval_equ "#less_") (*..for nth_Cons_*)],
     scr = Rule.Empty_Prog},
     srls = Rule_Set.Empty, calc = [], errpatts = [],
diff -r 19bd2f740479 -r 03e19793d81e src/Tools/isac/Knowledge/Biegelinie.thy
--- a/src/Tools/isac/Knowledge/Biegelinie.thy	Thu Aug 04 15:38:42 2022 +0200
+++ b/src/Tools/isac/Knowledge/Biegelinie.thy	Thu Aug 04 16:48:37 2022 +0200
@@ -157,11 +157,11 @@
     (*for asm in NTH_CONS ...*)
 	  \<^rule_eval>\<open>less\<close> (Prog_Expr.eval_equ "#less_"),
 	  (*2nd NTH_CONS pushes n+-1 into asms*)
-	  \<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_")], 
+	  \<^rule_eval>\<open>plus\<close> (**)(Calc_Binop.numeric "#add_")], 
 	srls = Rule_Set.Empty, calc = [], errpatts = [],
 	rules = [
      \<^rule_thm>\<open>NTH_CONS\<close>,
-		 \<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_"),
+		 \<^rule_eval>\<open>plus\<close> (**)(Calc_Binop.numeric "#add_"),
 		 \<^rule_thm>\<open>NTH_NIL\<close>,
 		 \<^rule_eval>\<open>Prog_Expr.lhs\<close> (Prog_Expr.eval_lhs"eval_lhs_"),
 		 \<^rule_eval>\<open>Prog_Expr.rhs\<close> (Prog_Expr.eval_rhs"eval_rhs_"),
@@ -174,11 +174,11 @@
     (*for asm in NTH_CONS ...*)
 		\<^rule_eval>\<open>less\<close> (Prog_Expr.eval_equ "#less_"),
 		(*2nd NTH_CONS pushes n+-1 into asms*)
-		\<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_")], 
+		\<^rule_eval>\<open>plus\<close> (**)(Calc_Binop.numeric "#add_")], 
 	srls = Rule_Set.Empty, calc = [], errpatts = [],
 	rules = [
     \<^rule_thm>\<open>NTH_CONS\<close>,
-	  \<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_"),
+	  \<^rule_eval>\<open>plus\<close> (**)(Calc_Binop.numeric "#add_"),
 	  \<^rule_thm>\<open>NTH_NIL\<close>,
 	  \<^rule_eval>\<open>Prog_Expr.lhs\<close> (Prog_Expr.eval_lhs "eval_lhs_"),
 	  \<^rule_eval>\<open>Prog_Expr.filter_sameFunId\<close> (Prog_Expr.eval_filter_sameFunId "Prog_Expr.filter_sameFunId"),
diff -r 19bd2f740479 -r 03e19793d81e src/Tools/isac/Knowledge/Diff.thy
--- a/src/Tools/isac/Knowledge/Diff.thy	Thu Aug 04 15:38:42 2022 +0200
+++ b/src/Tools/isac/Knowledge/Diff.thy	Thu Aug 04 16:48:37 2022 +0200
@@ -123,7 +123,7 @@
  	   \<^rule_thm>\<open>sqrt_conv\<close>, (*"?bdv occurs_in ?u \<Longrightarrow> sqrt ?u = ?u \<up> (1 / 2)"*)
  	   \<^rule_thm>\<open>root_conv\<close>, (*"?bdv occurs_in ?u \<Longrightarrow> nroot ?n ?u = ?u \<up> (1 / ?n)"*)
  	   \<^rule_thm>\<open>realpow_pow_bdv\<close>, (* "(?bdv \<up> ?b) \<up> ?c = ?bdv \<up> (?b * ?c)"*)
- 	   \<^rule_eval>\<open>times\<close> (**)(eval_binop "#mult_"),
+ 	   \<^rule_eval>\<open>times\<close> (**)(Calc_Binop.numeric "#mult_"),
  	   \<^rule_thm>\<open>rat_mult\<close>, (*a / b * (c / d) = a * c / (b * d)*)
  	   \<^rule_thm>\<open>times_divide_eq_right\<close>, (*?x * (?y / ?z) = ?x * ?y / ?z*)
  	   \<^rule_thm>\<open>times_divide_eq_left\<close>], (*?y / ?z * ?x = ?y * ?x / ?z*)
@@ -151,7 +151,7 @@
     \<^rule_thm>\<open>rat_mult\<close> (*a / b * (c / d) = a * c / (b * d)*),
     \<^rule_thm>\<open>times_divide_eq_right\<close> (*?x * (?y / ?z) = ?x * ?y / ?z*),
     \<^rule_thm>\<open>times_divide_eq_left\<close> (*?y / ?z * ?x = ?y * ?x / ?z*),
-    \<^rule_eval>\<open>times\<close> (**)(eval_binop "#mult_")],
+    \<^rule_eval>\<open>times\<close> (**)(Calc_Binop.numeric "#mult_")],
   scr = Rule.Empty_Prog};
 
 (*..*)
diff -r 19bd2f740479 -r 03e19793d81e src/Tools/isac/Knowledge/EqSystem.thy
--- a/src/Tools/isac/Knowledge/EqSystem.thy	Thu Aug 04 15:38:42 2022 +0200
+++ b/src/Tools/isac/Knowledge/EqSystem.thy	Thu Aug 04 16:48:37 2022 +0200
@@ -324,14 +324,14 @@
       erls = Rule_Set.Empty, srls = Rule_Set.Empty, calc = [], errpatts = [],
       rules = [(*for precond NTH_CONS ...*)
          \<^rule_eval>\<open>less\<close> (Prog_Expr.eval_equ "#less_"),
-         \<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_"),
+         \<^rule_eval>\<open>plus\<close> (**)(Calc_Binop.numeric "#add_"),
          \<^rule_eval>\<open>occur_exactly_in\<close> (eval_occur_exactly_in "#eval_occur_exactly_in_")],
          (*immediately repeated rewrite pushes '+' into precondition !*)
       scr = Rule.Empty_Prog}, 
     srls = Rule_Set.Empty, calc = [], errpatts = [],
     rules = [
       \<^rule_thm>\<open>NTH_CONS\<close>,
-      \<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_"),
+      \<^rule_eval>\<open>plus\<close> (**)(Calc_Binop.numeric "#add_"),
       \<^rule_thm>\<open>NTH_NIL\<close>,
       \<^rule_thm>\<open>tl_Cons\<close>,
       \<^rule_thm>\<open>tl_Nil\<close>,
@@ -350,13 +350,13 @@
     erls = Rule_Set.Empty, srls = Rule_Set.Empty, calc = [], errpatts = [],
     rules = [(*for precond NTH_CONS ...*)
   	   \<^rule_eval>\<open>less\<close> (Prog_Expr.eval_equ "#less_"),
-  	   \<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_")],
+  	   \<^rule_eval>\<open>plus\<close> (**)(Calc_Binop.numeric "#add_")],
   	   (*immediately repeated rewrite pushes '+' into precondition !*)
     scr = Rule.Empty_Prog}, 
   srls = Rule_Set.Empty, calc = [], errpatts = [],
   rules = [
     \<^rule_thm>\<open>NTH_CONS\<close>,
-    \<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_"),
+    \<^rule_eval>\<open>plus\<close> (**)(Calc_Binop.numeric "#add_"),
     \<^rule_thm>\<open>NTH_NIL\<close>,
     \<^rule_thm>\<open>tl_Cons\<close>,
     \<^rule_thm>\<open>tl_Nil\<close>,
@@ -394,7 +394,7 @@
   \<open>Rule_Set.append_rules "prls_2x2_linear_system" Rule_Set.empty 
     [\<^rule_thm>\<open>LENGTH_CONS\<close>,
       \<^rule_thm>\<open>LENGTH_NIL\<close>,
-      \<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_"),
+      \<^rule_eval>\<open>plus\<close> (**)(Calc_Binop.numeric "#add_"),
       \<^rule_eval>\<open>HOL.eq\<close> (Prog_Expr.eval_equal "#equal_")]\<close>
   CAS: "solveSystem e_s v_s"
   Given: "equalities e_s" "solveForVars v_s"
@@ -422,7 +422,7 @@
   \<open>Rule_Set.append_rules "prls_3x3_linear_system" Rule_Set.empty 
     [\<^rule_thm>\<open>LENGTH_CONS\<close>,
       \<^rule_thm>\<open>LENGTH_NIL\<close>,
-      \<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_"),
+      \<^rule_eval>\<open>plus\<close> (**)(Calc_Binop.numeric "#add_"),
       \<^rule_eval>\<open>HOL.eq\<close> (Prog_Expr.eval_equal "#equal_")]\<close>
   CAS: "solveSystem e_s v_s"
   Given: "equalities e_s" "solveForVars v_s"
@@ -433,7 +433,7 @@
   \<open>Rule_Set.append_rules "prls_4x4_linear_system" Rule_Set.empty 
     [\<^rule_thm>\<open>LENGTH_CONS\<close>,
       \<^rule_thm>\<open>LENGTH_NIL\<close>,
-      \<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_"),
+      \<^rule_eval>\<open>plus\<close> (**)(Calc_Binop.numeric "#add_"),
       \<^rule_eval>\<open>HOL.eq\<close> (Prog_Expr.eval_equal "#equal_")]\<close>
   CAS: "solveSystem e_s v_s"
   Given: "equalities e_s" "solveForVars v_s"
@@ -470,11 +470,11 @@
 				  [(*for asm in NTH_CONS ...*)
 				   \<^rule_eval>\<open>less\<close> (Prog_Expr.eval_equ "#less_"),
 				   (*2nd NTH_CONS pushes n+-1 into asms*)
-				   \<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_")
+				   \<^rule_eval>\<open>plus\<close> (**)(Calc_Binop.numeric "#add_")
 				   ], 
 		srls = Rule_Set.Empty, calc = [], errpatts = [],
 		rules = [\<^rule_thm>\<open>NTH_CONS\<close>,
-			 \<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_"),
+			 \<^rule_eval>\<open>plus\<close> (**)(Calc_Binop.numeric "#add_"),
 			 \<^rule_thm>\<open>NTH_NIL\<close>],
 		scr = Rule.Empty_Prog};
 \<close>
diff -r 19bd2f740479 -r 03e19793d81e src/Tools/isac/Knowledge/Integrate.thy
--- a/src/Tools/isac/Knowledge/Integrate.thy	Thu Aug 04 15:38:42 2022 +0200
+++ b/src/Tools/isac/Knowledge/Integrate.thy	Thu Aug 04 16:48:37 2022 +0200
@@ -130,7 +130,7 @@
    	  \<^rule_thm>\<open>integral_add\<close>,
    	  \<^rule_thm>\<open>integral_mult\<close>,
    	  \<^rule_thm>\<open>integral_pow\<close>,
-   	  \<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_")(*for n+1*)],
+   	  \<^rule_eval>\<open>plus\<close> (**)(Calc_Binop.numeric "#add_")(*for n+1*)],
     scr = Rule.Empty_Prog};
 \<close>
 ML \<open>
diff -r 19bd2f740479 -r 03e19793d81e src/Tools/isac/Knowledge/Inverse_Z_Transform.thy
--- a/src/Tools/isac/Knowledge/Inverse_Z_Transform.thy	Thu Aug 04 15:38:42 2022 +0200
+++ b/src/Tools/isac/Knowledge/Inverse_Z_Transform.thy	Thu Aug 04 16:48:37 2022 +0200
@@ -115,10 +115,10 @@
       erls = Rule_Set.append_rules "erls_in_srls_partial_fraction" Rule_Set.empty [
         \<^rule_eval>\<open>less\<close> (Prog_Expr.eval_equ "#less_"), (* ...for asm in NTH_CONS*)
         (*2nd NTH_CONS pushes n+-1 into asms*)
-        \<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_")], 
+        \<^rule_eval>\<open>plus\<close> (**)(Calc_Binop.numeric "#add_")], 
       srls = Rule_Set.Empty, calc = [], errpatts = [],
       rules = [\<^rule_thm>\<open>NTH_CONS\<close>,
-        \<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_"),
+        \<^rule_eval>\<open>plus\<close> (**)(Calc_Binop.numeric "#add_"),
         \<^rule_thm>\<open>NTH_NIL\<close>,
         \<^rule_eval>\<open>Prog_Expr.lhs\<close> (Prog_Expr.eval_lhs "eval_lhs_"),
         \<^rule_eval>\<open>Prog_Expr.rhs\<close> (Prog_Expr.eval_rhs"eval_rhs_"),
diff -r 19bd2f740479 -r 03e19793d81e src/Tools/isac/Knowledge/LinEq.thy
--- a/src/Tools/isac/Knowledge/LinEq.thy	Thu Aug 04 15:38:42 2022 +0200
+++ b/src/Tools/isac/Knowledge/LinEq.thy	Thu Aug 04 16:48:37 2022 +0200
@@ -46,7 +46,7 @@
     (*		
      Don't use
      \<^rule_eval>\<open>divide\<close> (Prog_Expr.eval_cancel "#divide_e"),
-     \<^rule_eval>\<open>realpow\<close> (**)(eval_binop "#power_"),
+     \<^rule_eval>\<open>realpow\<close> (**)(Calc_Binop.numeric "#power_"),
      *)
     ];
 
@@ -57,7 +57,7 @@
     (*		
      Don't use
      \<^rule_eval>\<open>divide\<close> (Prog_Expr.eval_cancel "#divide_e"),
-     \<^rule_eval>\<open>realpow\<close> (**)(eval_binop "#power_"),
+     \<^rule_eval>\<open>realpow\<close> (**)(Calc_Binop.numeric "#power_"),
      *)
     ];
 \<close>
@@ -72,14 +72,14 @@
     calc = [], errpatts = [],
     rules = [
       \<^rule_thm>\<open>real_assoc_1\<close>,
-      \<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_"),
-      \<^rule_eval>\<open>minus\<close> (**)(eval_binop "#sub_"),
-      \<^rule_eval>\<open>times\<close> (**)(eval_binop "#mult_"),
+      \<^rule_eval>\<open>plus\<close> (**)(Calc_Binop.numeric "#add_"),
+      \<^rule_eval>\<open>minus\<close> (**)(Calc_Binop.numeric "#sub_"),
+      \<^rule_eval>\<open>times\<close> (**)(Calc_Binop.numeric "#mult_"),
       (*  Don't use  
        \<^rule_eval>\<open>divide\<close> (Prog_Expr.eval_cancel "#divide_e"),
        \<^rule_eval>\<open>sqrt\<close> (eval_sqrt "#sqrt_"),
        *)
-      \<^rule_eval>\<open>realpow\<close> (**)(eval_binop "#power_")],
+      \<^rule_eval>\<open>realpow\<close> (**)(Calc_Binop.numeric "#power_")],
     scr = Rule.Empty_Prog});
 \<close>
 rule_set_knowledge LinPoly_simplify = LinPoly_simplify
diff -r 19bd2f740479 -r 03e19793d81e src/Tools/isac/Knowledge/Partial_Fractions.thy
--- a/src/Tools/isac/Knowledge/Partial_Fractions.thy	Thu Aug 04 15:38:42 2022 +0200
+++ b/src/Tools/isac/Knowledge/Partial_Fractions.thy	Thu Aug 04 16:48:37 2022 +0200
@@ -163,11 +163,11 @@
     [(*for asm in NTH_CONS ...*)
      \<^rule_eval>\<open>less\<close> (Prog_Expr.eval_equ "#less_"),
      (*2nd NTH_CONS pushes n+-1 into asms*)
-     \<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_")], 
+     \<^rule_eval>\<open>plus\<close> (**)(Calc_Binop.numeric "#add_")], 
   srls = Rule_Set.Empty, calc = [], errpatts = [],
   rules = [
      \<^rule_thm>\<open>NTH_CONS\<close>,
-     \<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_"),
+     \<^rule_eval>\<open>plus\<close> (**)(Calc_Binop.numeric "#add_"),
      \<^rule_thm>\<open>NTH_NIL\<close>,
      \<^rule_eval>\<open>Prog_Expr.lhs\<close> (Prog_Expr.eval_lhs "eval_lhs_"),
      \<^rule_eval>\<open>Prog_Expr.rhs\<close> (Prog_Expr.eval_rhs"eval_rhs_"),
diff -r 19bd2f740479 -r 03e19793d81e src/Tools/isac/Knowledge/Poly.thy
--- a/src/Tools/isac/Knowledge/Poly.thy	Thu Aug 04 15:38:42 2022 +0200
+++ b/src/Tools/isac/Knowledge/Poly.thy	Thu Aug 04 16:48:37 2022 +0200
@@ -708,18 +708,18 @@
 val Poly_erls = Rule_Set.append_rules "Poly_erls" Atools_erls [
   \<^rule_eval>\<open>HOL.eq\<close> (Prog_Expr.eval_equal "#equal_"),
   \<^rule_thm>\<open>real_unari_minus\<close>,
-  \<^rule_eval>\<open>plus\<close> (eval_binop "#add_"),
-  \<^rule_eval>\<open>minus\<close> (eval_binop "#sub_"),
-  \<^rule_eval>\<open>times\<close> (eval_binop "#mult_"),
-  \<^rule_eval>\<open>realpow\<close> (eval_binop "#power_")];
+  \<^rule_eval>\<open>plus\<close> (Calc_Binop.numeric "#add_"),
+  \<^rule_eval>\<open>minus\<close> (Calc_Binop.numeric "#sub_"),
+  \<^rule_eval>\<open>times\<close> (Calc_Binop.numeric "#mult_"),
+  \<^rule_eval>\<open>realpow\<close> (Calc_Binop.numeric "#power_")];
 
 val poly_crls = Rule_Set.append_rules "poly_crls" Atools_crls [
   \<^rule_eval>\<open>HOL.eq\<close> (Prog_Expr.eval_equal "#equal_"),
   \<^rule_thm>\<open>real_unari_minus\<close>,
-  \<^rule_eval>\<open>plus\<close> (eval_binop "#add_"),
-  \<^rule_eval>\<open>minus\<close> (eval_binop "#sub_"),
-  \<^rule_eval>\<open>times\<close> (eval_binop "#mult_"),
-  \<^rule_eval>\<open>realpow\<close> (eval_binop "#power_")];
+  \<^rule_eval>\<open>plus\<close> (Calc_Binop.numeric "#add_"),
+  \<^rule_eval>\<open>minus\<close> (Calc_Binop.numeric "#sub_"),
+  \<^rule_eval>\<open>times\<close> (Calc_Binop.numeric "#mult_"),
+  \<^rule_eval>\<open>realpow\<close> (Calc_Binop.numeric "#power_")];
 \<close>
 ML \<open>
 val expand =
@@ -745,7 +745,7 @@
         \<^rule_eval>\<open>ord_class.less\<close> (Prog_Expr.eval_equ "#less_"),
         \<^rule_thm>\<open>not_false\<close>,
         \<^rule_thm>\<open>not_true\<close>,
-        \<^rule_eval>\<open>plus_class.plus\<close> (eval_binop "#add_")],
+        \<^rule_eval>\<open>plus_class.plus\<close> (Calc_Binop.numeric "#add_")],
       scr = Rule.Empty_Prog};
 
 \<close> ML \<open>
@@ -838,15 +838,15 @@
   Rule_Def.Repeat{id = "calc_add_mult_pow_", preconds = [], 
       rew_ord = ("dummy_ord", Rewrite_Ord.function_empty),
       erls = Atools_erls(*erls3.4.03*),srls = Rule_Set.Empty,
-      calc = [("PLUS"  , (\<^const_name>\<open>plus\<close>, eval_binop "#add_")), 
-	      ("TIMES" , (\<^const_name>\<open>times\<close>, eval_binop "#mult_")),
-	      ("POWER", (\<^const_name>\<open>realpow\<close>, eval_binop "#power_"))
+      calc = [("PLUS"  , (\<^const_name>\<open>plus\<close>, Calc_Binop.numeric "#add_")), 
+	      ("TIMES" , (\<^const_name>\<open>times\<close>, Calc_Binop.numeric "#mult_")),
+	      ("POWER", (\<^const_name>\<open>realpow\<close>, Calc_Binop.numeric "#power_"))
 	      ],
       errpatts = [],
       rules = [
-        \<^rule_eval>\<open>plus\<close> (eval_binop "#add_"),
-	      \<^rule_eval>\<open>times\<close> (eval_binop "#mult_"),
-	      \<^rule_eval>\<open>realpow\<close> (eval_binop "#power_")],
+        \<^rule_eval>\<open>plus\<close> (Calc_Binop.numeric "#add_"),
+	      \<^rule_eval>\<open>times\<close> (Calc_Binop.numeric "#mult_"),
+	      \<^rule_eval>\<open>realpow\<close> (Calc_Binop.numeric "#power_")],
       scr = Rule.Empty_Prog};
 
 val reduce_012_mult_ = 
@@ -865,7 +865,7 @@
   Rule_Def.Repeat{id = "collect_numerals_", preconds = [], 
       rew_ord = ("dummy_ord", Rewrite_Ord.function_empty),
       erls = Atools_erls, srls = Rule_Set.Empty,
-      calc = [("PLUS"  , (\<^const_name>\<open>plus\<close>, eval_binop "#add_"))
+      calc = [("PLUS"  , (\<^const_name>\<open>plus\<close>, Calc_Binop.numeric "#add_"))
 	      ], errpatts = [],
       rules = [
         \<^rule_thm>\<open>real_num_collect\<close>, (*"[| l is_num; m is_num |]==>l * n + m * n = (l + m) * n"*)
@@ -874,7 +874,7 @@
         \<^rule_thm>\<open>real_one_collect\<close>, (*"m is_num ==> n + m * n = (1 + m) * n"*)
         \<^rule_thm>\<open>real_one_collect_assoc_r\<close>, (*"m is_num ==> (k + n) + m * n = k + (m + 1) * n"*)
 
-        \<^rule_eval>\<open>plus\<close> (eval_binop "#add_"),
+        \<^rule_eval>\<open>plus\<close> (Calc_Binop.numeric "#add_"),
 
       	 (*MG: Reihenfolge der folgenden 2 Rule.Thm muss so bleiben, wegen
 		       (a+a)+a --> a + 2*a --> 3*a and not (a+a)+a --> 2*a + a *)
@@ -943,9 +943,9 @@
   Rule_Def.Repeat{id = "collect_numerals", preconds = [], 
       rew_ord = ("dummy_ord", Rewrite_Ord.function_empty),
       erls = Atools_erls(*erls3.4.03*),srls = Rule_Set.Empty,
-      calc = [("PLUS"  , (\<^const_name>\<open>plus\<close>, eval_binop "#add_")), 
-	      ("TIMES" , (\<^const_name>\<open>times\<close>, eval_binop "#mult_")),
-	      ("POWER", (\<^const_name>\<open>realpow\<close>, eval_binop "#power_"))
+      calc = [("PLUS"  , (\<^const_name>\<open>plus\<close>, Calc_Binop.numeric "#add_")), 
+	      ("TIMES" , (\<^const_name>\<open>times\<close>, Calc_Binop.numeric "#mult_")),
+	      ("POWER", (\<^const_name>\<open>realpow\<close>, Calc_Binop.numeric "#power_"))
 	      ], errpatts = [],
       rules =[
         \<^rule_thm>\<open>real_num_collect\<close>, (*"[| l is_num; m is_num |]==>l * n + m * n = (l + m) * n"*)
@@ -953,9 +953,9 @@
           (*"[| l is_num; m is_num |] ==> l * n + (m * n + k) =  (l + m) * n + k"*)
 	      \<^rule_thm>\<open>real_one_collect\<close>,	 (*"m is_num ==> n + m * n = (1 + m) * n"*)
 	      \<^rule_thm>\<open>real_one_collect_assoc\<close>, (*"m is_num ==> k + (n + m * n) = k + (1 + m) * n"*)
-	      \<^rule_eval>\<open>plus\<close> (eval_binop "#add_"), 
-	      \<^rule_eval>\<open>times\<close> (eval_binop "#mult_"),
-	      \<^rule_eval>\<open>realpow\<close> (eval_binop "#power_")],
+	      \<^rule_eval>\<open>plus\<close> (Calc_Binop.numeric "#add_"), 
+	      \<^rule_eval>\<open>times\<close> (Calc_Binop.numeric "#mult_"),
+	      \<^rule_eval>\<open>realpow\<close> (Calc_Binop.numeric "#power_")],
       scr = Rule.Empty_Prog};
 val reduce_012 = 
   Rule_Def.Repeat{id = "reduce_012", preconds = [], 
@@ -1032,10 +1032,10 @@
 	  rew_ord = ("dummy_ord", Rewrite_Ord.function_empty),
 	  erls = Rule_Set.append_rules "Rule_Set.empty-is_multUnordered" Rule_Set.empty
 			    [\<^rule_eval>\<open>is_multUnordered\<close> (eval_is_multUnordered "")],
-	  calc = [("PLUS"  , (\<^const_name>\<open>plus\<close>, eval_binop "#add_")),
-		  ("TIMES" , (\<^const_name>\<open>times\<close>, eval_binop "#mult_")),
+	  calc = [("PLUS"  , (\<^const_name>\<open>plus\<close>, Calc_Binop.numeric "#add_")),
+		  ("TIMES" , (\<^const_name>\<open>times\<close>, Calc_Binop.numeric "#mult_")),
 		  ("DIVIDE", (\<^const_name>\<open>divide\<close>, Prog_Expr.eval_cancel "#divide_e")),
-		  ("POWER" , (\<^const_name>\<open>realpow\<close>, eval_binop "#power_"))],
+		  ("POWER" , (\<^const_name>\<open>realpow\<close>, Calc_Binop.numeric "#power_"))],
     errpatts = [],
 	  scr = Rule.Rfuns {init_state  = init_state,
 		     normal_form = normal_form,
@@ -1073,10 +1073,10 @@
 	  erls = Rule_Set.append_rules "Rule_Set.empty-is_addUnordered" Rule_Set.empty(*MG: poly_erls*)
 			[\<^rule_eval>\<open>is_addUnordered\<close> (eval_is_addUnordered "")],
 	  calc = [
-      ("PLUS"  ,(\<^const_name>\<open>plus\<close>, eval_binop "#add_")),
-		  ("TIMES" ,(\<^const_name>\<open>times\<close>, eval_binop "#mult_")),
+      ("PLUS"  ,(\<^const_name>\<open>plus\<close>, Calc_Binop.numeric "#add_")),
+		  ("TIMES" ,(\<^const_name>\<open>times\<close>, Calc_Binop.numeric "#mult_")),
 		  ("DIVIDE",(\<^const_name>\<open>divide\<close>, Prog_Expr.eval_cancel "#divide_e")),
-		  ("POWER" ,(\<^const_name>\<open>realpow\<close>  , eval_binop "#power_"))],
+		  ("POWER" ,(\<^const_name>\<open>realpow\<close>  , Calc_Binop.numeric "#power_"))],
 	  errpatts = [],
 	  scr = Rule.Rfuns {
       init_state  = init_state,
@@ -1113,7 +1113,7 @@
     rules = [
        Rule.Rls_ discard_minus,
 	     Rule.Rls_ expand_poly_,
-	     \<^rule_eval>\<open>times\<close> (eval_binop "#mult_"),
+	     \<^rule_eval>\<open>times\<close> (Calc_Binop.numeric "#mult_"),
 	     Rule.Rls_ order_mult_rls_,
 	     Rule.Rls_ simplify_power_, 
 	     Rule.Rls_ calc_add_mult_pow_, 
@@ -1132,7 +1132,7 @@
     rules = [
        Rule.Rls_ discard_minus,
 	     Rule.Rls_ expand_poly_,
-	     \<^rule_eval>\<open>times\<close> (eval_binop "#mult_"),
+	     \<^rule_eval>\<open>times\<close> (Calc_Binop.numeric "#mult_"),
 	     Rule.Rls_ order_mult_rls_,
 	     Rule.Rls_ simplify_power_, 
 	     Rule.Rls_ calc_add_mult_pow_, 
@@ -1154,7 +1154,7 @@
     rules = [
       Rule.Rls_ discard_minus,
 	    Rule.Rls_ expand_poly_rat_,(*ignors rationals*)
-	    \<^rule_eval>\<open>times\<close> (eval_binop "#mult_"),
+	    \<^rule_eval>\<open>times\<close> (Calc_Binop.numeric "#mult_"),
 	    Rule.Rls_ order_mult_rls_,
 	    Rule.Rls_ simplify_power_, 
 	    Rule.Rls_ calc_add_mult_pow_, 
@@ -1171,9 +1171,9 @@
 val rev_rew_p = 
   Rule_Set.Sequence{id = "rev_rew_p", preconds = [], rew_ord = ("termlessI",termlessI),
     erls = Atools_erls, srls = Rule_Set.Empty,
-    calc = [(*("PLUS"  , (\<^const_name>\<open>plus\<close>, eval_binop "#add_")), 
-	    ("TIMES" , (\<^const_name>\<open>times\<close>, eval_binop "#mult_")),
-	    ("POWER", (\<^const_name>\<open>realpow\<close>, eval_binop "#power_"))*)
+    calc = [(*("PLUS"  , (\<^const_name>\<open>plus\<close>, Calc_Binop.numeric "#add_")), 
+	    ("TIMES" , (\<^const_name>\<open>times\<close>, Calc_Binop.numeric "#mult_")),
+	    ("POWER", (\<^const_name>\<open>realpow\<close>, Calc_Binop.numeric "#power_"))*)
 	    ], errpatts = [],
     rules = [
        \<^rule_thm>\<open>real_plus_binom_times\<close>, (*"(a + b)*(a + b) = a ^ 2 + 2 * a * b + b ^ 2*)
@@ -1189,9 +1189,9 @@
 	     Rule.Rls_ order_mult_rls_,
 	     (*Rule.Rls_ order_add_rls_,*)
 
-	     \<^rule_eval>\<open>plus\<close> (eval_binop "#add_"), 
-	     \<^rule_eval>\<open>times\<close> (eval_binop "#mult_"),
-	     \<^rule_eval>\<open>realpow\<close> (eval_binop "#power_"),
+	     \<^rule_eval>\<open>plus\<close> (Calc_Binop.numeric "#add_"), 
+	     \<^rule_eval>\<open>times\<close> (Calc_Binop.numeric "#mult_"),
+	     \<^rule_eval>\<open>realpow\<close> (Calc_Binop.numeric "#power_"),
 	     
 	     \<^rule_thm_sym>\<open>realpow_twoI\<close>, (*"r1 * r1 = r1 \<up> 2"*)
 	     \<^rule_thm_sym>\<open>real_mult_2\<close>, (*"z1 + z1 = 2 * z1"*)
@@ -1204,9 +1204,9 @@
 
 	     \<^rule_thm>\<open>realpow_multI\<close>, (*"(r * s) \<up> n = r \<up> n * s \<up> n"*)
 
-	     \<^rule_eval>\<open>plus\<close> (eval_binop "#add_"),
-	     \<^rule_eval>\<open>times\<close> (eval_binop "#mult_"),
-	     \<^rule_eval>\<open>realpow\<close> (eval_binop "#power_"),
+	     \<^rule_eval>\<open>plus\<close> (Calc_Binop.numeric "#add_"),
+	     \<^rule_eval>\<open>times\<close> (Calc_Binop.numeric "#mult_"),
+	     \<^rule_eval>\<open>realpow\<close> (Calc_Binop.numeric "#power_"),
 
 	     \<^rule_thm>\<open>mult_1_left\<close>, (*"1 * z = z"*)
 	     \<^rule_thm>\<open>mult_zero_left\<close>, (*"0 * z = 0"*)
@@ -1256,9 +1256,9 @@
 val expand_binoms = 
   Rule_Def.Repeat{id = "expand_binoms", preconds = [], rew_ord = ("termlessI",termlessI),
     erls = Atools_erls, srls = Rule_Set.Empty,
-    calc = [("PLUS"  , (\<^const_name>\<open>plus\<close>, eval_binop "#add_")), 
-	    ("TIMES" , (\<^const_name>\<open>times\<close>, eval_binop "#mult_")),
-	    ("POWER", (\<^const_name>\<open>realpow\<close>, eval_binop "#power_"))
+    calc = [("PLUS"  , (\<^const_name>\<open>plus\<close>, Calc_Binop.numeric "#add_")), 
+	    ("TIMES" , (\<^const_name>\<open>times\<close>, Calc_Binop.numeric "#mult_")),
+	    ("POWER", (\<^const_name>\<open>realpow\<close>, Calc_Binop.numeric "#power_"))
 	    ], errpatts = [],
     rules = [
        \<^rule_thm>\<open>real_plus_binom_pow2\<close>, (*"(a + b) \<up> 2 = a \<up> 2 + 2 * a * b + b \<up> 2"*)
@@ -1285,9 +1285,9 @@
 	     \<^rule_thm>\<open>mult_zero_left\<close>, (*"0 * z = 0"*)
 	     \<^rule_thm>\<open>add_0_left\<close>, (*"0 + z = z"*)
     
-	     \<^rule_eval>\<open>plus\<close> (eval_binop "#add_"), 
-	     \<^rule_eval>\<open>times\<close> (eval_binop "#mult_"),
-	     \<^rule_eval>\<open>realpow\<close> (eval_binop "#power_"),
+	     \<^rule_eval>\<open>plus\<close> (Calc_Binop.numeric "#add_"), 
+	     \<^rule_eval>\<open>times\<close> (Calc_Binop.numeric "#mult_"),
+	     \<^rule_eval>\<open>realpow\<close> (Calc_Binop.numeric "#power_"),
             (*\<^rule_thm>\<open>mult.commute\<close>,
 		    (*AC-rewriting*)
 	     \<^rule_thm>\<open>real_mult_left_commute\<close>,
@@ -1307,9 +1307,9 @@
 	     \<^rule_thm>\<open>real_one_collect\<close>, (*"m is_num ==> n + m * n = (1 + m) * n"*)
 	     \<^rule_thm>\<open>real_one_collect_assoc\<close>, (*"m is_num ==> k + (n + m * n) = k + (1 + m) * n"*)
     
-	     \<^rule_eval>\<open>plus\<close> (eval_binop "#add_"), 
-	     \<^rule_eval>\<open>times\<close> (eval_binop "#mult_"),
-	     \<^rule_eval>\<open>realpow\<close> (eval_binop "#power_")],
+	     \<^rule_eval>\<open>plus\<close> (Calc_Binop.numeric "#add_"), 
+	     \<^rule_eval>\<open>times\<close> (Calc_Binop.numeric "#mult_"),
+	     \<^rule_eval>\<open>realpow\<close> (Calc_Binop.numeric "#power_")],
     scr = Rule.Prog (Program.prep_program @{thm expand_binoms_2.simps})};      
 \<close>
 
diff -r 19bd2f740479 -r 03e19793d81e src/Tools/isac/Knowledge/PolyEq.thy
--- a/src/Tools/isac/Knowledge/PolyEq.thy	Thu Aug 04 15:38:42 2022 +0200
+++ b/src/Tools/isac/Knowledge/PolyEq.thy	Thu Aug 04 16:48:37 2022 +0200
@@ -406,12 +406,12 @@
   		\<^rule_thm>\<open>real_diff_minus\<close>,
   		\<^rule_thm>\<open>real_unari_minus\<close>,
   		\<^rule_thm>\<open>realpow_multI\<close>,
-  		\<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_"),
-  		\<^rule_eval>\<open>minus\<close> (**)(eval_binop "#sub_"),
-  		\<^rule_eval>\<open>times\<close> (**)(eval_binop "#mult_"),
+  		\<^rule_eval>\<open>plus\<close> (**)(Calc_Binop.numeric "#add_"),
+  		\<^rule_eval>\<open>minus\<close> (**)(Calc_Binop.numeric "#sub_"),
+  		\<^rule_eval>\<open>times\<close> (**)(Calc_Binop.numeric "#mult_"),
   		\<^rule_eval>\<open>divide\<close> (Prog_Expr.eval_cancel "#divide_e"),
   		\<^rule_eval>\<open>sqrt\<close> (eval_sqrt "#sqrt_"),
-  		\<^rule_eval>\<open>realpow\<close> (**)(eval_binop "#power_"),
+  		\<^rule_eval>\<open>realpow\<close> (**)(Calc_Binop.numeric "#power_"),
        Rule.Rls_ reduce_012],
     scr = Rule.Empty_Prog});
 \<close>
diff -r 19bd2f740479 -r 03e19793d81e src/Tools/isac/Knowledge/PolyMinus.thy
--- a/src/Tools/isac/Knowledge/PolyMinus.thy	Thu Aug 04 15:38:42 2022 +0200
+++ b/src/Tools/isac/Knowledge/PolyMinus.thy	Thu Aug 04 16:48:37 2022 +0200
@@ -232,8 +232,8 @@
   	 \<^rule_thm>\<open>subtrahiere_x_minus1_minus\<close>, (*"[| l is_num |] ==> (x - v) - l * v = x + (-1 - l) * v"*)
   	 \<^rule_thm>\<open>subtrahiere_x_minus_minus1\<close>, (*"[| m is_num |] ==> (x - m * v) - v = x + (-m - 1) * v"*)
 
-  	 \<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_"),
-  	 \<^rule_eval>\<open>minus\<close> (**)(eval_binop "#subtr_"),
+  	 \<^rule_eval>\<open>plus\<close> (**)(Calc_Binop.numeric "#add_"),
+  	 \<^rule_eval>\<open>minus\<close> (**)(Calc_Binop.numeric "#subtr_"),
 
   	 (*MG: Reihenfolge der folgenden 2 Rule.Thm muss so bleiben, wegen
         (a+a)+a --> a + 2*a --> 3*a and not (a+a)+a --> 2*a + a *)
@@ -257,7 +257,7 @@
       \<^rule_thm>\<open>vorzeichen_minus_weg3\<close>, (*"l kleiner 0 ==> k + a - l * b = k + a + -l * b"*)
       \<^rule_thm>\<open>vorzeichen_minus_weg4\<close>, (*"l kleiner 0 ==> k - a - l * b = k - a + -l * b"*)
 
-      \<^rule_eval>\<open>times\<close> (**)(eval_binop "#mult_"),
+      \<^rule_eval>\<open>times\<close> (**)(Calc_Binop.numeric "#mult_"),
 
       \<^rule_thm>\<open>mult_zero_left\<close>, (*"0 * z = 0"*)
       \<^rule_thm>\<open>mult_1_left\<close>, (*"1 * z = z"*)
@@ -316,9 +316,9 @@
   	Rule.Rls_ verschoenere];
 val rechnen = 
   Rule_Set.append_rules "rechnen" Rule_Set.empty [
-    \<^rule_eval>\<open>times\<close> (**)(eval_binop "#mult_"),
-    \<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_"),
-    \<^rule_eval>\<open>minus\<close> (**)(eval_binop "#subtr_")];
+    \<^rule_eval>\<open>times\<close> (**)(Calc_Binop.numeric "#mult_"),
+    \<^rule_eval>\<open>plus\<close> (**)(Calc_Binop.numeric "#add_"),
+    \<^rule_eval>\<open>minus\<close> (**)(Calc_Binop.numeric "#subtr_")];
 \<close>
 rule_set_knowledge
   ordne_alphabetisch = \<open>prep_rls' ordne_alphabetisch\<close> and
diff -r 19bd2f740479 -r 03e19793d81e src/Tools/isac/Knowledge/Rational.thy
--- a/src/Tools/isac/Knowledge/Rational.thy	Thu Aug 04 15:38:42 2022 +0200
+++ b/src/Tools/isac/Knowledge/Rational.thy	Thu Aug 04 16:48:37 2022 +0200
@@ -516,10 +516,10 @@
 	rew_ord = ("ord_make_polynomial", ord_make_polynomial false \<^theory>),
 	erls = rational_erls, 
 	calc = 
-	  [("PLUS", (\<^const_name>\<open>plus\<close>, (**)eval_binop "#add_")),
-	  ("TIMES" , (\<^const_name>\<open>times\<close>, (**)eval_binop "#mult_")),
+	  [("PLUS", (\<^const_name>\<open>plus\<close>, (**)Calc_Binop.numeric "#add_")),
+	  ("TIMES" , (\<^const_name>\<open>times\<close>, (**)Calc_Binop.numeric "#mult_")),
 	  ("DIVIDE", (\<^const_name>\<open>divide\<close>, Prog_Expr.eval_cancel "#divide_e")),
-	  ("POWER", (\<^const_name>\<open>realpow\<close>, (**)eval_binop "#power_"))],
+	  ("POWER", (\<^const_name>\<open>realpow\<close>, (**)Calc_Binop.numeric "#power_"))],
     errpatts = [],
 	scr =
 	  Rule.Rfuns {init_state  = init_state \<^theory> Atools_erls ro,
@@ -583,10 +583,10 @@
   Rule_Set.Rrls {id = "add_fractions_p", prepat=prepat,
     rew_ord = ("ord_make_polynomial", ord_make_polynomial false \<^theory>),
     erls = rational_erls,
-    calc = [("PLUS", (\<^const_name>\<open>plus\<close>, (**)eval_binop "#add_")),
-      ("TIMES", (\<^const_name>\<open>times\<close>, (**)eval_binop "#mult_")),
+    calc = [("PLUS", (\<^const_name>\<open>plus\<close>, (**)Calc_Binop.numeric "#add_")),
+      ("TIMES", (\<^const_name>\<open>times\<close>, (**)Calc_Binop.numeric "#mult_")),
       ("DIVIDE", (\<^const_name>\<open>divide\<close>, Prog_Expr.eval_cancel "#divide_e")),
-      ("POWER", (\<^const_name>\<open>realpow\<close>, (**)eval_binop "#power_"))],
+      ("POWER", (\<^const_name>\<open>realpow\<close>, (**)Calc_Binop.numeric "#power_"))],
     errpatts = [],
     scr = Rule.Rfuns {init_state  = init_state \<^theory> Atools_erls ro,
       normal_form = add_fraction_p_ \<^theory>,
@@ -623,7 +623,7 @@
         (*----- distribute none-atoms -----*)
         \<^rule_thm>\<open>realpow_def_atom\<close>, (*"[| 1 < n; ~ (r is_atom) |]==>r  \<up>  n = r * r  \<up>  (n + -1)"*)
         \<^rule_thm>\<open>realpow_eq_oneI\<close>, (*"1  \<up>  n = 1"*)
-        \<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_")],
+        \<^rule_eval>\<open>plus\<close> (**)(Calc_Binop.numeric "#add_")],
       scr = Rule.Empty_Prog});
 
 \<close> ML \<open>
diff -r 19bd2f740479 -r 03e19793d81e src/Tools/isac/Knowledge/Root.thy
--- a/src/Tools/isac/Knowledge/Root.thy	Thu Aug 04 15:38:42 2022 +0200
+++ b/src/Tools/isac/Knowledge/Root.thy	Thu Aug 04 16:48:37 2022 +0200
@@ -162,10 +162,10 @@
     \<^rule_thm>\<open>real_unari_minus\<close>,
     \<^rule_eval>\<open>sqrt\<close> (eval_sqrt "#sqrt_"),
     \<^rule_eval>\<open>divide\<close> (Prog_Expr.eval_cancel "#divide_e"),
-    \<^rule_eval>\<open>realpow\<close> (**)(eval_binop "#power_"),
-    \<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_"), 
-    \<^rule_eval>\<open>minus\<close> (**)(eval_binop "#sub_"),
-    \<^rule_eval>\<open>times\<close> (**)(eval_binop "#mult_"),
+    \<^rule_eval>\<open>realpow\<close> (**)(Calc_Binop.numeric "#power_"),
+    \<^rule_eval>\<open>plus\<close> (**)(Calc_Binop.numeric "#add_"), 
+    \<^rule_eval>\<open>minus\<close> (**)(Calc_Binop.numeric "#sub_"),
+    \<^rule_eval>\<open>times\<close> (**)(Calc_Binop.numeric "#mult_"),
     \<^rule_eval>\<open>HOL.eq\<close> (Prog_Expr.eval_equal "#equal_")];
 
 val Root_erls = 
@@ -173,10 +173,10 @@
     \<^rule_thm>\<open>real_unari_minus\<close>,
     \<^rule_eval>\<open>sqrt\<close> (eval_sqrt "#sqrt_"),
     \<^rule_eval>\<open>Rings.divide_class.divide\<close> (Prog_Expr.eval_cancel "#divide_e"),
-    \<^rule_eval>\<open>realpow\<close> (**)(eval_binop "#power_"),
-    \<^rule_eval>\<open>Groups.plus_class.plus\<close> (**)(eval_binop "#add_"), 
-    \<^rule_eval>\<open>Groups.minus_class.minus\<close> (**)(eval_binop "#sub_"),
-    \<^rule_eval>\<open>Groups.times_class.times\<close> (**)(eval_binop "#mult_"),
+    \<^rule_eval>\<open>realpow\<close> (**)(Calc_Binop.numeric "#power_"),
+    \<^rule_eval>\<open>Groups.plus_class.plus\<close> (**)(Calc_Binop.numeric "#add_"), 
+    \<^rule_eval>\<open>Groups.minus_class.minus\<close> (**)(Calc_Binop.numeric "#sub_"),
+    \<^rule_eval>\<open>Groups.times_class.times\<close> (**)(Calc_Binop.numeric "#mult_"),
     \<^rule_eval>\<open>HOL.eq\<close> (Prog_Expr.eval_equal "#equal_")];
 val Root_erls = 
   Rule_Set.append_erls_rules "Root_erls_erls" Root_erls [
@@ -222,9 +222,9 @@
       \<^rule_thm>\<open>real_one_collect\<close>, (*"m is_num ==> n + m * n = (1 + m) * n"*)
       \<^rule_thm>\<open>real_one_collect_assoc\<close>, (*"m is_num ==> k + (n + m * n) = k + (1 + m) * n"*)
 
-      \<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_"),
-      \<^rule_eval>\<open>times\<close> (**)(eval_binop "#mult_"),
-      \<^rule_eval>\<open>realpow\<close> (**)(eval_binop "#power_")],
+      \<^rule_eval>\<open>plus\<close> (**)(Calc_Binop.numeric "#add_"),
+      \<^rule_eval>\<open>times\<close> (**)(Calc_Binop.numeric "#mult_"),
+      \<^rule_eval>\<open>realpow\<close> (**)(Calc_Binop.numeric "#power_")],
     scr = Rule.Empty_Prog});      
 \<close>
 rule_set_knowledge make_rooteq = make_rooteq
@@ -254,12 +254,12 @@
        \<^rule_thm>\<open>mult_zero_left\<close>, (*"0 * z = 0"*)
        \<^rule_thm>\<open>add_0_left\<close>, (*"0 + z = z"*)
   
-       \<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_"), 
-       \<^rule_eval>\<open>minus\<close> (**)(eval_binop "#sub_"), 
-       \<^rule_eval>\<open>times\<close> (**)(eval_binop "#mult_"),
+       \<^rule_eval>\<open>plus\<close> (**)(Calc_Binop.numeric "#add_"), 
+       \<^rule_eval>\<open>minus\<close> (**)(Calc_Binop.numeric "#sub_"), 
+       \<^rule_eval>\<open>times\<close> (**)(Calc_Binop.numeric "#mult_"),
        \<^rule_eval>\<open>divide\<close> (Prog_Expr.eval_cancel "#divide_e"),
        \<^rule_eval>\<open>sqrt\<close> (eval_sqrt "#sqrt_"),
-       \<^rule_eval>\<open>realpow\<close> (**)(eval_binop "#power_"),
+       \<^rule_eval>\<open>realpow\<close> (**)(Calc_Binop.numeric "#power_"),
   
        \<^rule_thm_sym>\<open>realpow_twoI\<close>, (*"r1 * r1 = r1  \<up>  2"*)
        \<^rule_thm>\<open>realpow_plus_1\<close>, (*"r * r  \<up>  n = r  \<up>  (n + 1)"*)
@@ -270,12 +270,12 @@
        \<^rule_thm>\<open>real_one_collect\<close>, (*"m is_num ==> n + m * n = (1 + m) * n"*)
        \<^rule_thm>\<open>real_one_collect_assoc\<close>, (*"m is_num ==> k + (n + m * n) = k + (1 + m) * n"*)
   
-       \<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_"), 
-       \<^rule_eval>\<open>minus\<close> (**)(eval_binop "#sub_"), 
-       \<^rule_eval>\<open>times\<close> (**)(eval_binop "#mult_"),
+       \<^rule_eval>\<open>plus\<close> (**)(Calc_Binop.numeric "#add_"), 
+       \<^rule_eval>\<open>minus\<close> (**)(Calc_Binop.numeric "#sub_"), 
+       \<^rule_eval>\<open>times\<close> (**)(Calc_Binop.numeric "#mult_"),
        \<^rule_eval>\<open>divide\<close> (Prog_Expr.eval_cancel "#divide_e"),
        \<^rule_eval>\<open>sqrt\<close> (eval_sqrt "#sqrt_"),
-       \<^rule_eval>\<open>realpow\<close> (**)(eval_binop "#power_")],
+       \<^rule_eval>\<open>realpow\<close> (**)(Calc_Binop.numeric "#power_")],
     scr = Rule.Empty_Prog});      
 \<close>
 rule_set_knowledge expand_rootbinoms = expand_rootbinoms
diff -r 19bd2f740479 -r 03e19793d81e src/Tools/isac/Knowledge/RootEq.thy
--- a/src/Tools/isac/Knowledge/RootEq.thy	Thu Aug 04 15:38:42 2022 +0200
+++ b/src/Tools/isac/Knowledge/RootEq.thy	Thu Aug 04 16:48:37 2022 +0200
@@ -318,12 +318,12 @@
     rules = [
       \<^rule_thm>\<open>real_assoc_1\<close>, (* a+(b+c) = a+b+c *)
       \<^rule_thm>\<open>real_assoc_2\<close>, (* a*(b*c) = a*b*c *)
-      \<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_"),
-      \<^rule_eval>\<open>minus\<close> (**)(eval_binop "#sub_"),
-      \<^rule_eval>\<open>times\<close> (**)(eval_binop "#mult_"),
+      \<^rule_eval>\<open>plus\<close> (**)(Calc_Binop.numeric "#add_"),
+      \<^rule_eval>\<open>minus\<close> (**)(Calc_Binop.numeric "#sub_"),
+      \<^rule_eval>\<open>times\<close> (**)(Calc_Binop.numeric "#mult_"),
       \<^rule_eval>\<open>divide\<close> (Prog_Expr.eval_cancel "#divide_e"),
       \<^rule_eval>\<open>sqrt\<close> (eval_sqrt "#sqrt_"),
-      \<^rule_eval>\<open>realpow\<close> (**)(eval_binop "#power_"),
+      \<^rule_eval>\<open>realpow\<close> (**)(Calc_Binop.numeric "#power_"),
       \<^rule_thm>\<open>real_plus_binom_pow2\<close>,
       \<^rule_thm>\<open>real_minus_binom_pow2\<close>,
       \<^rule_thm>\<open>realpow_mul\<close>, (* (a * b)^n = a^n * b^n*)
diff -r 19bd2f740479 -r 03e19793d81e src/Tools/isac/Knowledge/Test.thy
--- a/src/Tools/isac/Knowledge/Test.thy	Thu Aug 04 15:38:42 2022 +0200
+++ b/src/Tools/isac/Knowledge/Test.thy	Thu Aug 04 16:48:37 2022 +0200
@@ -378,9 +378,9 @@
 	     \<^rule_eval>\<open>Prog_Expr.is_num\<close> (Prog_Expr.eval_is_num "#is_num_"),
 	     \<^rule_eval>\<open>Prog_Expr.matches\<close> (Prog_Expr.eval_matches ""),
     
-	     \<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_"),
-	     \<^rule_eval>\<open>times\<close> (**)(eval_binop "#mult_"),
-	     \<^rule_eval>\<open>realpow\<close> (**)(eval_binop "#power_"),
+	     \<^rule_eval>\<open>plus\<close> (**)(Calc_Binop.numeric "#add_"),
+	     \<^rule_eval>\<open>times\<close> (**)(Calc_Binop.numeric "#mult_"),
+	     \<^rule_eval>\<open>realpow\<close> (**)(Calc_Binop.numeric "#power_"),
     
 	     \<^rule_eval>\<open>less\<close> (Prog_Expr.eval_equ "#less_"),
 	     \<^rule_eval>\<open>less_eq\<close> (Prog_Expr.eval_equ "#less_equal_"),
@@ -421,10 +421,10 @@
 	     \<^rule_eval>\<open>Prog_Expr.matches\<close> (Prog_Expr.eval_matches ""),
 	     \<^rule_eval>\<open>contains_root\<close> (eval_contains_root"#contains_root_"),
     
-	     \<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_"),
-	     \<^rule_eval>\<open>times\<close> (**)(eval_binop "#mult_"),
+	     \<^rule_eval>\<open>plus\<close> (**)(Calc_Binop.numeric "#add_"),
+	     \<^rule_eval>\<open>times\<close> (**)(Calc_Binop.numeric "#mult_"),
 	     \<^rule_eval>\<open>sqrt\<close> (eval_sqrt "#sqrt_"),
-	     \<^rule_eval>\<open>realpow\<close> (**)(eval_binop "#power_"),
+	     \<^rule_eval>\<open>realpow\<close> (**)(Calc_Binop.numeric "#power_"),
     
 	     \<^rule_eval>\<open>less\<close> (Prog_Expr.eval_equ "#less_"),
 	     \<^rule_eval>\<open>less_eq\<close> (Prog_Expr.eval_equ "#less_equal_"),
@@ -494,10 +494,10 @@
 	     \<^rule_thm>\<open>radd_real_const\<close>,
 	     (* these 2 rules are invers to distr_div_right wrt. termination.
 		     thus they MUST be done IMMEDIATELY before calc *)
-	     \<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_"), 
-	     \<^rule_eval>\<open>times\<close> (**)(eval_binop "#mult_"),
+	     \<^rule_eval>\<open>plus\<close> (**)(Calc_Binop.numeric "#add_"), 
+	     \<^rule_eval>\<open>times\<close> (**)(Calc_Binop.numeric "#mult_"),
 	     \<^rule_eval>\<open>divide\<close> (Prog_Expr.eval_cancel "#divide_e"),
-	     \<^rule_eval>\<open>realpow\<close> (**)(eval_binop "#power_"),
+	     \<^rule_eval>\<open>realpow\<close> (**)(Calc_Binop.numeric "#power_"),
 
 	     \<^rule_thm>\<open>rcollect_right\<close>,
 	     \<^rule_thm>\<open>rcollect_one_left\<close>,
@@ -599,9 +599,9 @@
     rew_ord = ("ord_make_polytest", ord_make_polytest false @{theory "Poly"}),
     erls = testerls, srls = Rule_Set.Empty,
     calc = [
-      ("PLUS"  , (\<^const_name>\<open>plus\<close>, (**)eval_binop "#add_")), 
-	    ("TIMES" , (\<^const_name>\<open>times\<close>, (**)eval_binop "#mult_")),
-	    ("POWER", (\<^const_name>\<open>realpow\<close>, (**)eval_binop "#power_"))],
+      ("PLUS"  , (\<^const_name>\<open>plus\<close>, (**)Calc_Binop.numeric "#add_")), 
+	    ("TIMES" , (\<^const_name>\<open>times\<close>, (**)Calc_Binop.numeric "#mult_")),
+	    ("POWER", (\<^const_name>\<open>realpow\<close>, (**)Calc_Binop.numeric "#power_"))],
     errpatts = [],
     rules = [
        \<^rule_thm>\<open>real_diff_minus\<close>, (*"a - b = a + (-1) * b"*)
@@ -630,18 +630,18 @@
 	     \<^rule_thm>\<open>real_one_collect\<close>, (*"m is_num ==> n + m * n = (1 + m) * n"*)
 	     \<^rule_thm>\<open>real_one_collect_assoc\<close>, (*"m is_num ==> k + (n + m * n) = k + (1 + m) * n"*)
     
-	     \<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_"), 
-	     \<^rule_eval>\<open>times\<close> (**)(eval_binop "#mult_"),
-	     \<^rule_eval>\<open>realpow\<close> (**)(eval_binop "#power_")],
+	     \<^rule_eval>\<open>plus\<close> (**)(Calc_Binop.numeric "#add_"), 
+	     \<^rule_eval>\<open>times\<close> (**)(Calc_Binop.numeric "#mult_"),
+	     \<^rule_eval>\<open>realpow\<close> (**)(Calc_Binop.numeric "#power_")],
     scr = Rule.Empty_Prog}; 
 
 val expand_binomtest =
   Rule_Def.Repeat{id = "expand_binomtest", preconds = [], 
     rew_ord = ("termlessI",termlessI), erls = testerls, srls = Rule_Set.Empty,
     calc = [
-      ("PLUS"  , (\<^const_name>\<open>plus\<close>, (**)eval_binop "#add_")), 
-	    ("TIMES" , (\<^const_name>\<open>times\<close>, (**)eval_binop "#mult_")),
-	    ("POWER", (\<^const_name>\<open>realpow\<close>, (**)eval_binop "#power_"))
+      ("PLUS"  , (\<^const_name>\<open>plus\<close>, (**)Calc_Binop.numeric "#add_")), 
+	    ("TIMES" , (\<^const_name>\<open>times\<close>, (**)Calc_Binop.numeric "#mult_")),
+	    ("POWER", (\<^const_name>\<open>realpow\<close>, (**)Calc_Binop.numeric "#power_"))
 	    ],
     errpatts = [],
     rules = [
@@ -664,9 +664,9 @@
     	\<^rule_thm>\<open>mult_zero_left\<close>, (*"0 * z = 0"*)
     	\<^rule_thm>\<open>add_0_left\<close>, (*"0 + z = z"*)
     
-    	\<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_"), 
-    	\<^rule_eval>\<open>times\<close> (**)(eval_binop "#mult_"),
-    	\<^rule_eval>\<open>realpow\<close> (**)(eval_binop "#power_"),
+    	\<^rule_eval>\<open>plus\<close> (**)(Calc_Binop.numeric "#add_"), 
+    	\<^rule_eval>\<open>times\<close> (**)(Calc_Binop.numeric "#mult_"),
+    	\<^rule_eval>\<open>realpow\<close> (**)(Calc_Binop.numeric "#power_"),
     
     	\<^rule_thm_sym>\<open>realpow_twoI\<close>, (*"r1 * r1 = r1 \<up> 2"*)
     	\<^rule_thm>\<open>realpow_plus_1\<close>,	 (*"r * r \<up> n = r \<up> (n + 1)"*)
@@ -678,9 +678,9 @@
     	\<^rule_thm>\<open>real_one_collect\<close>,	 (*"m is_num ==> n + m * n = (1 + m) * n"*)
     	\<^rule_thm>\<open>real_one_collect_assoc\<close>, (*"m is_num ==> k + (n + m * n) = k + (1 + m) * n"*)
     
-    	\<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_"), 
-    	\<^rule_eval>\<open>times\<close> (**)(eval_binop "#mult_"),
-    	\<^rule_eval>\<open>realpow\<close> (**)(eval_binop "#power_")],
+    	\<^rule_eval>\<open>plus\<close> (**)(Calc_Binop.numeric "#add_"), 
+    	\<^rule_eval>\<open>times\<close> (**)(Calc_Binop.numeric "#mult_"),
+    	\<^rule_eval>\<open>realpow\<close> (**)(Calc_Binop.numeric "#power_")],
     scr = Rule.Empty_Prog};      
 \<close>
 rule_set_knowledge
diff -r 19bd2f740479 -r 03e19793d81e src/Tools/isac/ProgLang/Calculate.thy
--- a/src/Tools/isac/ProgLang/Calculate.thy	Thu Aug 04 15:38:42 2022 +0200
+++ b/src/Tools/isac/ProgLang/Calculate.thy	Thu Aug 04 16:48:37 2022 +0200
@@ -21,29 +21,37 @@
 ML_file evaluate.sml
 
 ML \<open>
-\<close> ML \<open>
+signature CALCULATE_BINARY_OPERATION =
+sig
+  val numeric: string -> string -> term -> Proof.context -> (string * term) option
+\<^isac_test>\<open>
+  val is_calcul_op: string -> bool
+  val calcul: Proof.context -> term -> term
+\<close>
+end
+
+(**)
+structure Calc_Binop(**): CALCULATE_BINARY_OPERATION(**) =
+struct
+(**)
+
 (*** evaluate binary associative operations ***)
 
-val is_num = can HOLogic.dest_number;
-
 val is_calcul_op =
   member (op =) [\<^const_name>\<open>plus\<close>, \<^const_name>\<open>minus\<close>, \<^const_name>\<open>times\<close>, \<^const_name>\<open>realpow\<close>];
 
 fun calcul ctxt lhs =
   let
     val simp_ctxt =
-(*
-      Proof_Context.init_global thy
-*)
       ctxt |> put_simpset (Simplifier.simpset_of @{theory_context BaseDefinitions});
     val eq = Simplifier.rewrite simp_ctxt (Thm.cterm_of ctxt lhs);
     val rhs = Thm.term_of (Thm.rhs_of eq);
   in rhs end;
 
-fun eval_binop (_: string) (_: string) t ctxt =
+fun numeric (_: string) (_: string) t ctxt =
   (case t of
     (opp as Const (c1, T)) $ (Const (c2, _) $ v $ t1) $ t2 =>         (* binary \<circ> (v \<circ> n1) \<circ> n2 *)
-      if c1 = c2 andalso is_calcul_op c1 andalso is_num t1 andalso is_num t2 then
+      if c1 = c2 andalso is_calcul_op c1 andalso Eval.is_num t1 andalso Eval.is_num t2 then
         let
           val opp' = Const (if c1 = \<^const_name>\<open>minus\<close> then \<^const_name>\<open>plus\<close> else c1, T);
           val res = calcul ctxt (opp' $ t1 $ t2);
@@ -52,7 +60,7 @@
       else NONE
   | (opp as Const (c1, _)) $ t1 $ (Const (c2, _) $ t2 $ v) =>         (* binary \<circ> n1 \<circ> (n2 \<circ> v) *)
       if c1 = c2 andalso is_calcul_op c1 andalso c1 <> \<^const_name>\<open>minus\<close>
-        andalso is_num t1 andalso is_num t2
+        andalso Eval.is_num t1 andalso Eval.is_num t2
       then
         let
           val res = calcul ctxt (opp $ t1 $ t2);
@@ -62,7 +70,7 @@
         end
       else NONE
   | Const (c, _) $ t1 $ t2 =>                                               (* binary \<circ> n1 \<circ> n2 *)
-      if is_calcul_op c andalso is_num t1 andalso is_num t2 then
+      if is_calcul_op c andalso Eval.is_num t1 andalso Eval.is_num t2 then
         let
           val res = calcul ctxt t;
           val prop = HOLogic.Trueprop $ (HOLogic.mk_eq (t, res));
@@ -71,7 +79,7 @@
         end
       else NONE
   | _ => NONE);
-
+(**)end(**)
 \<close> ML \<open>
 \<close> ML \<open>
 \<close>
diff -r 19bd2f740479 -r 03e19793d81e src/Tools/isac/ProgLang/evaluate.sml
--- a/src/Tools/isac/ProgLang/evaluate.sml	Thu Aug 04 15:38:42 2022 +0200
+++ b/src/Tools/isac/ProgLang/evaluate.sml	Thu Aug 04 16:48:37 2022 +0200
@@ -7,6 +7,7 @@
 
 signature EVALUATE =
 sig
+  val is_num: term -> bool
   val calc_equ: string -> int * int -> bool
   val power: int -> int -> int
   val sign_mult: int -> int -> int
@@ -32,6 +33,8 @@
 struct
 (**)
 
+val is_num = can HOLogic.dest_number;
+
 (* trace internal steps of isac's numeral calculations *)
 val eval_trace = Attrib.setup_config_bool \<^binding>\<open>eval_trace\<close> (K false);