1.1 --- a/src/Tools/isac/Knowledge/Test.thy Thu Aug 04 15:38:42 2022 +0200
1.2 +++ b/src/Tools/isac/Knowledge/Test.thy Thu Aug 04 16:48:37 2022 +0200
1.3 @@ -378,9 +378,9 @@
1.4 \<^rule_eval>\<open>Prog_Expr.is_num\<close> (Prog_Expr.eval_is_num "#is_num_"),
1.5 \<^rule_eval>\<open>Prog_Expr.matches\<close> (Prog_Expr.eval_matches ""),
1.6
1.7 - \<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_"),
1.8 - \<^rule_eval>\<open>times\<close> (**)(eval_binop "#mult_"),
1.9 - \<^rule_eval>\<open>realpow\<close> (**)(eval_binop "#power_"),
1.10 + \<^rule_eval>\<open>plus\<close> (**)(Calc_Binop.numeric "#add_"),
1.11 + \<^rule_eval>\<open>times\<close> (**)(Calc_Binop.numeric "#mult_"),
1.12 + \<^rule_eval>\<open>realpow\<close> (**)(Calc_Binop.numeric "#power_"),
1.13
1.14 \<^rule_eval>\<open>less\<close> (Prog_Expr.eval_equ "#less_"),
1.15 \<^rule_eval>\<open>less_eq\<close> (Prog_Expr.eval_equ "#less_equal_"),
1.16 @@ -421,10 +421,10 @@
1.17 \<^rule_eval>\<open>Prog_Expr.matches\<close> (Prog_Expr.eval_matches ""),
1.18 \<^rule_eval>\<open>contains_root\<close> (eval_contains_root"#contains_root_"),
1.19
1.20 - \<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_"),
1.21 - \<^rule_eval>\<open>times\<close> (**)(eval_binop "#mult_"),
1.22 + \<^rule_eval>\<open>plus\<close> (**)(Calc_Binop.numeric "#add_"),
1.23 + \<^rule_eval>\<open>times\<close> (**)(Calc_Binop.numeric "#mult_"),
1.24 \<^rule_eval>\<open>sqrt\<close> (eval_sqrt "#sqrt_"),
1.25 - \<^rule_eval>\<open>realpow\<close> (**)(eval_binop "#power_"),
1.26 + \<^rule_eval>\<open>realpow\<close> (**)(Calc_Binop.numeric "#power_"),
1.27
1.28 \<^rule_eval>\<open>less\<close> (Prog_Expr.eval_equ "#less_"),
1.29 \<^rule_eval>\<open>less_eq\<close> (Prog_Expr.eval_equ "#less_equal_"),
1.30 @@ -494,10 +494,10 @@
1.31 \<^rule_thm>\<open>radd_real_const\<close>,
1.32 (* these 2 rules are invers to distr_div_right wrt. termination.
1.33 thus they MUST be done IMMEDIATELY before calc *)
1.34 - \<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_"),
1.35 - \<^rule_eval>\<open>times\<close> (**)(eval_binop "#mult_"),
1.36 + \<^rule_eval>\<open>plus\<close> (**)(Calc_Binop.numeric "#add_"),
1.37 + \<^rule_eval>\<open>times\<close> (**)(Calc_Binop.numeric "#mult_"),
1.38 \<^rule_eval>\<open>divide\<close> (Prog_Expr.eval_cancel "#divide_e"),
1.39 - \<^rule_eval>\<open>realpow\<close> (**)(eval_binop "#power_"),
1.40 + \<^rule_eval>\<open>realpow\<close> (**)(Calc_Binop.numeric "#power_"),
1.41
1.42 \<^rule_thm>\<open>rcollect_right\<close>,
1.43 \<^rule_thm>\<open>rcollect_one_left\<close>,
1.44 @@ -599,9 +599,9 @@
1.45 rew_ord = ("ord_make_polytest", ord_make_polytest false @{theory "Poly"}),
1.46 erls = testerls, srls = Rule_Set.Empty,
1.47 calc = [
1.48 - ("PLUS" , (\<^const_name>\<open>plus\<close>, (**)eval_binop "#add_")),
1.49 - ("TIMES" , (\<^const_name>\<open>times\<close>, (**)eval_binop "#mult_")),
1.50 - ("POWER", (\<^const_name>\<open>realpow\<close>, (**)eval_binop "#power_"))],
1.51 + ("PLUS" , (\<^const_name>\<open>plus\<close>, (**)Calc_Binop.numeric "#add_")),
1.52 + ("TIMES" , (\<^const_name>\<open>times\<close>, (**)Calc_Binop.numeric "#mult_")),
1.53 + ("POWER", (\<^const_name>\<open>realpow\<close>, (**)Calc_Binop.numeric "#power_"))],
1.54 errpatts = [],
1.55 rules = [
1.56 \<^rule_thm>\<open>real_diff_minus\<close>, (*"a - b = a + (-1) * b"*)
1.57 @@ -630,18 +630,18 @@
1.58 \<^rule_thm>\<open>real_one_collect\<close>, (*"m is_num ==> n + m * n = (1 + m) * n"*)
1.59 \<^rule_thm>\<open>real_one_collect_assoc\<close>, (*"m is_num ==> k + (n + m * n) = k + (1 + m) * n"*)
1.60
1.61 - \<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_"),
1.62 - \<^rule_eval>\<open>times\<close> (**)(eval_binop "#mult_"),
1.63 - \<^rule_eval>\<open>realpow\<close> (**)(eval_binop "#power_")],
1.64 + \<^rule_eval>\<open>plus\<close> (**)(Calc_Binop.numeric "#add_"),
1.65 + \<^rule_eval>\<open>times\<close> (**)(Calc_Binop.numeric "#mult_"),
1.66 + \<^rule_eval>\<open>realpow\<close> (**)(Calc_Binop.numeric "#power_")],
1.67 scr = Rule.Empty_Prog};
1.68
1.69 val expand_binomtest =
1.70 Rule_Def.Repeat{id = "expand_binomtest", preconds = [],
1.71 rew_ord = ("termlessI",termlessI), erls = testerls, srls = Rule_Set.Empty,
1.72 calc = [
1.73 - ("PLUS" , (\<^const_name>\<open>plus\<close>, (**)eval_binop "#add_")),
1.74 - ("TIMES" , (\<^const_name>\<open>times\<close>, (**)eval_binop "#mult_")),
1.75 - ("POWER", (\<^const_name>\<open>realpow\<close>, (**)eval_binop "#power_"))
1.76 + ("PLUS" , (\<^const_name>\<open>plus\<close>, (**)Calc_Binop.numeric "#add_")),
1.77 + ("TIMES" , (\<^const_name>\<open>times\<close>, (**)Calc_Binop.numeric "#mult_")),
1.78 + ("POWER", (\<^const_name>\<open>realpow\<close>, (**)Calc_Binop.numeric "#power_"))
1.79 ],
1.80 errpatts = [],
1.81 rules = [
1.82 @@ -664,9 +664,9 @@
1.83 \<^rule_thm>\<open>mult_zero_left\<close>, (*"0 * z = 0"*)
1.84 \<^rule_thm>\<open>add_0_left\<close>, (*"0 + z = z"*)
1.85
1.86 - \<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_"),
1.87 - \<^rule_eval>\<open>times\<close> (**)(eval_binop "#mult_"),
1.88 - \<^rule_eval>\<open>realpow\<close> (**)(eval_binop "#power_"),
1.89 + \<^rule_eval>\<open>plus\<close> (**)(Calc_Binop.numeric "#add_"),
1.90 + \<^rule_eval>\<open>times\<close> (**)(Calc_Binop.numeric "#mult_"),
1.91 + \<^rule_eval>\<open>realpow\<close> (**)(Calc_Binop.numeric "#power_"),
1.92
1.93 \<^rule_thm_sym>\<open>realpow_twoI\<close>, (*"r1 * r1 = r1 \<up> 2"*)
1.94 \<^rule_thm>\<open>realpow_plus_1\<close>, (*"r * r \<up> n = r \<up> (n + 1)"*)
1.95 @@ -678,9 +678,9 @@
1.96 \<^rule_thm>\<open>real_one_collect\<close>, (*"m is_num ==> n + m * n = (1 + m) * n"*)
1.97 \<^rule_thm>\<open>real_one_collect_assoc\<close>, (*"m is_num ==> k + (n + m * n) = k + (1 + m) * n"*)
1.98
1.99 - \<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_"),
1.100 - \<^rule_eval>\<open>times\<close> (**)(eval_binop "#mult_"),
1.101 - \<^rule_eval>\<open>realpow\<close> (**)(eval_binop "#power_")],
1.102 + \<^rule_eval>\<open>plus\<close> (**)(Calc_Binop.numeric "#add_"),
1.103 + \<^rule_eval>\<open>times\<close> (**)(Calc_Binop.numeric "#mult_"),
1.104 + \<^rule_eval>\<open>realpow\<close> (**)(Calc_Binop.numeric "#power_")],
1.105 scr = Rule.Empty_Prog};
1.106 \<close>
1.107 rule_set_knowledge