1.1 --- a/TODO.md Thu Aug 04 15:38:42 2022 +0200
1.2 +++ b/TODO.md Thu Aug 04 16:48:37 2022 +0200
1.3 @@ -67,7 +67,7 @@
1.4
1.5 ***** priority of WN items is top down, most urgent/simple on top
1.6
1.7 -* WN: Calculate.thy: add structure Calculate, also signature EXAMPLE
1.8 +* WN: add signature EXAMPLE
1.9 * WN: MethodC.from_store throws exn 'get_pbt not found: ' ... confusing !! take 'ketype' as an argument
1.10
1.11 * WN: rewriting with ctxt not complete (cause errors hard to indentify later)
2.1 --- a/src/Tools/isac/Knowledge/Base_Tools.thy Thu Aug 04 15:38:42 2022 +0200
2.2 +++ b/src/Tools/isac/Knowledge/Base_Tools.thy Thu Aug 04 16:48:37 2022 +0200
2.3 @@ -24,7 +24,7 @@
2.4
2.5
2.6 subsection \<open>setup for ML-functions\<close>
2.7 -text \<open>required by "eval_binop" below\<close>
2.8 +text \<open>required by "Calc_Binop.numeric" below\<close>
2.9 calculation occurs_in = \<open>Prog_Expr.eval_occurs_in "#occurs_in_"\<close>
2.10 calculation some_occur_in = \<open>Prog_Expr.eval_some_occur_in "#some_occur_in_"\<close>
2.11 calculation is_atom = \<open>Prog_Expr.eval_is_atom "#is_atom_"\<close>
2.12 @@ -33,11 +33,11 @@
2.13 calculation leq (less_eq) = \<open>Prog_Expr.eval_equ "#less_equal_"\<close>
2.14 calculation ident = \<open>Prog_Expr.eval_ident "#ident_"\<close>
2.15 calculation equal (HOL.eq) = \<open>Prog_Expr.eval_equal "#equal_"\<close>
2.16 -calculation PLUS (plus) = \<open>(**)eval_binop "#add_"\<close>
2.17 -calculation MINUS (minus) = \<open>(**)eval_binop "#sub_"\<close>
2.18 -calculation TIMES (times) = \<open>(**)eval_binop "#mult_"\<close>
2.19 +calculation PLUS (plus) = \<open>(**)Calc_Binop.numeric "#add_"\<close>
2.20 +calculation MINUS (minus) = \<open>(**)Calc_Binop.numeric "#sub_"\<close>
2.21 +calculation TIMES (times) = \<open>(**)Calc_Binop.numeric "#mult_"\<close>
2.22 calculation DIVIDE (divide) = \<open>Prog_Expr.eval_cancel "#divide_e"\<close>
2.23 -calculation POWER (realpow) = \<open>(**)eval_binop "#power_"\<close>
2.24 +calculation POWER (realpow) = \<open>(**)Calc_Binop.numeric "#power_"\<close>
2.25 calculation boollist2sum = \<open>Prog_Expr.eval_boollist2sum ""\<close>
2.26
2.27 subsection \<open>rewrite-order for rule-sets\<close>
2.28 @@ -115,11 +115,11 @@
2.29 \<close>
2.30
2.31 subsection \<open>ONCE AGAIN extend rule-set for evaluating pre-conditions and program-expressions\<close>
2.32 -text \<open>requires "eval_binop" from above\<close>
2.33 +text \<open>requires "Calc_Binop.numeric" from above\<close>
2.34 ML \<open>
2.35 val prog_expr = Rule_Set.append_rules "prog_expr" prog_expr [
2.36 - \<^rule_eval>\<open>times\<close> (**)(eval_binop "#mult_"),
2.37 - \<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_"),
2.38 + \<^rule_eval>\<open>times\<close> (**)(Calc_Binop.numeric "#mult_"),
2.39 + \<^rule_eval>\<open>plus\<close> (**)(Calc_Binop.numeric "#add_"),
2.40 \<^rule_eval>\<open>less\<close> (Prog_Expr.eval_equ "#less_"),
2.41 \<^rule_eval>\<open>less_eq\<close> (Prog_Expr.eval_equ "#less_equal_"),
2.42 \<^rule_eval>\<open>Prog_Expr.ident\<close> (Prog_Expr.eval_ident "#ident_"),
2.43 @@ -135,7 +135,7 @@
2.44 erls = Rule_Def.Repeat {id = "list_elrs", preconds = [], rew_ord = ("termlessI", termlessI),
2.45 erls = Rule_Set.empty, srls = Rule_Set.Empty, calc = [], errpatts = [],
2.46 rules = [
2.47 - \<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_"),
2.48 + \<^rule_eval>\<open>plus\<close> (**)(Calc_Binop.numeric "#add_"),
2.49 \<^rule_eval>\<open>less\<close> (Prog_Expr.eval_equ "#less_") (*..for nth_Cons_*)],
2.50 scr = Rule.Empty_Prog},
2.51 srls = Rule_Set.Empty, calc = [], errpatts = [],
3.1 --- a/src/Tools/isac/Knowledge/Biegelinie.thy Thu Aug 04 15:38:42 2022 +0200
3.2 +++ b/src/Tools/isac/Knowledge/Biegelinie.thy Thu Aug 04 16:48:37 2022 +0200
3.3 @@ -157,11 +157,11 @@
3.4 (*for asm in NTH_CONS ...*)
3.5 \<^rule_eval>\<open>less\<close> (Prog_Expr.eval_equ "#less_"),
3.6 (*2nd NTH_CONS pushes n+-1 into asms*)
3.7 - \<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_")],
3.8 + \<^rule_eval>\<open>plus\<close> (**)(Calc_Binop.numeric "#add_")],
3.9 srls = Rule_Set.Empty, calc = [], errpatts = [],
3.10 rules = [
3.11 \<^rule_thm>\<open>NTH_CONS\<close>,
3.12 - \<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_"),
3.13 + \<^rule_eval>\<open>plus\<close> (**)(Calc_Binop.numeric "#add_"),
3.14 \<^rule_thm>\<open>NTH_NIL\<close>,
3.15 \<^rule_eval>\<open>Prog_Expr.lhs\<close> (Prog_Expr.eval_lhs"eval_lhs_"),
3.16 \<^rule_eval>\<open>Prog_Expr.rhs\<close> (Prog_Expr.eval_rhs"eval_rhs_"),
3.17 @@ -174,11 +174,11 @@
3.18 (*for asm in NTH_CONS ...*)
3.19 \<^rule_eval>\<open>less\<close> (Prog_Expr.eval_equ "#less_"),
3.20 (*2nd NTH_CONS pushes n+-1 into asms*)
3.21 - \<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_")],
3.22 + \<^rule_eval>\<open>plus\<close> (**)(Calc_Binop.numeric "#add_")],
3.23 srls = Rule_Set.Empty, calc = [], errpatts = [],
3.24 rules = [
3.25 \<^rule_thm>\<open>NTH_CONS\<close>,
3.26 - \<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_"),
3.27 + \<^rule_eval>\<open>plus\<close> (**)(Calc_Binop.numeric "#add_"),
3.28 \<^rule_thm>\<open>NTH_NIL\<close>,
3.29 \<^rule_eval>\<open>Prog_Expr.lhs\<close> (Prog_Expr.eval_lhs "eval_lhs_"),
3.30 \<^rule_eval>\<open>Prog_Expr.filter_sameFunId\<close> (Prog_Expr.eval_filter_sameFunId "Prog_Expr.filter_sameFunId"),
4.1 --- a/src/Tools/isac/Knowledge/Diff.thy Thu Aug 04 15:38:42 2022 +0200
4.2 +++ b/src/Tools/isac/Knowledge/Diff.thy Thu Aug 04 16:48:37 2022 +0200
4.3 @@ -123,7 +123,7 @@
4.4 \<^rule_thm>\<open>sqrt_conv\<close>, (*"?bdv occurs_in ?u \<Longrightarrow> sqrt ?u = ?u \<up> (1 / 2)"*)
4.5 \<^rule_thm>\<open>root_conv\<close>, (*"?bdv occurs_in ?u \<Longrightarrow> nroot ?n ?u = ?u \<up> (1 / ?n)"*)
4.6 \<^rule_thm>\<open>realpow_pow_bdv\<close>, (* "(?bdv \<up> ?b) \<up> ?c = ?bdv \<up> (?b * ?c)"*)
4.7 - \<^rule_eval>\<open>times\<close> (**)(eval_binop "#mult_"),
4.8 + \<^rule_eval>\<open>times\<close> (**)(Calc_Binop.numeric "#mult_"),
4.9 \<^rule_thm>\<open>rat_mult\<close>, (*a / b * (c / d) = a * c / (b * d)*)
4.10 \<^rule_thm>\<open>times_divide_eq_right\<close>, (*?x * (?y / ?z) = ?x * ?y / ?z*)
4.11 \<^rule_thm>\<open>times_divide_eq_left\<close>], (*?y / ?z * ?x = ?y * ?x / ?z*)
4.12 @@ -151,7 +151,7 @@
4.13 \<^rule_thm>\<open>rat_mult\<close> (*a / b * (c / d) = a * c / (b * d)*),
4.14 \<^rule_thm>\<open>times_divide_eq_right\<close> (*?x * (?y / ?z) = ?x * ?y / ?z*),
4.15 \<^rule_thm>\<open>times_divide_eq_left\<close> (*?y / ?z * ?x = ?y * ?x / ?z*),
4.16 - \<^rule_eval>\<open>times\<close> (**)(eval_binop "#mult_")],
4.17 + \<^rule_eval>\<open>times\<close> (**)(Calc_Binop.numeric "#mult_")],
4.18 scr = Rule.Empty_Prog};
4.19
4.20 (*..*)
5.1 --- a/src/Tools/isac/Knowledge/EqSystem.thy Thu Aug 04 15:38:42 2022 +0200
5.2 +++ b/src/Tools/isac/Knowledge/EqSystem.thy Thu Aug 04 16:48:37 2022 +0200
5.3 @@ -324,14 +324,14 @@
5.4 erls = Rule_Set.Empty, srls = Rule_Set.Empty, calc = [], errpatts = [],
5.5 rules = [(*for precond NTH_CONS ...*)
5.6 \<^rule_eval>\<open>less\<close> (Prog_Expr.eval_equ "#less_"),
5.7 - \<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_"),
5.8 + \<^rule_eval>\<open>plus\<close> (**)(Calc_Binop.numeric "#add_"),
5.9 \<^rule_eval>\<open>occur_exactly_in\<close> (eval_occur_exactly_in "#eval_occur_exactly_in_")],
5.10 (*immediately repeated rewrite pushes '+' into precondition !*)
5.11 scr = Rule.Empty_Prog},
5.12 srls = Rule_Set.Empty, calc = [], errpatts = [],
5.13 rules = [
5.14 \<^rule_thm>\<open>NTH_CONS\<close>,
5.15 - \<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_"),
5.16 + \<^rule_eval>\<open>plus\<close> (**)(Calc_Binop.numeric "#add_"),
5.17 \<^rule_thm>\<open>NTH_NIL\<close>,
5.18 \<^rule_thm>\<open>tl_Cons\<close>,
5.19 \<^rule_thm>\<open>tl_Nil\<close>,
5.20 @@ -350,13 +350,13 @@
5.21 erls = Rule_Set.Empty, srls = Rule_Set.Empty, calc = [], errpatts = [],
5.22 rules = [(*for precond NTH_CONS ...*)
5.23 \<^rule_eval>\<open>less\<close> (Prog_Expr.eval_equ "#less_"),
5.24 - \<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_")],
5.25 + \<^rule_eval>\<open>plus\<close> (**)(Calc_Binop.numeric "#add_")],
5.26 (*immediately repeated rewrite pushes '+' into precondition !*)
5.27 scr = Rule.Empty_Prog},
5.28 srls = Rule_Set.Empty, calc = [], errpatts = [],
5.29 rules = [
5.30 \<^rule_thm>\<open>NTH_CONS\<close>,
5.31 - \<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_"),
5.32 + \<^rule_eval>\<open>plus\<close> (**)(Calc_Binop.numeric "#add_"),
5.33 \<^rule_thm>\<open>NTH_NIL\<close>,
5.34 \<^rule_thm>\<open>tl_Cons\<close>,
5.35 \<^rule_thm>\<open>tl_Nil\<close>,
5.36 @@ -394,7 +394,7 @@
5.37 \<open>Rule_Set.append_rules "prls_2x2_linear_system" Rule_Set.empty
5.38 [\<^rule_thm>\<open>LENGTH_CONS\<close>,
5.39 \<^rule_thm>\<open>LENGTH_NIL\<close>,
5.40 - \<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_"),
5.41 + \<^rule_eval>\<open>plus\<close> (**)(Calc_Binop.numeric "#add_"),
5.42 \<^rule_eval>\<open>HOL.eq\<close> (Prog_Expr.eval_equal "#equal_")]\<close>
5.43 CAS: "solveSystem e_s v_s"
5.44 Given: "equalities e_s" "solveForVars v_s"
5.45 @@ -422,7 +422,7 @@
5.46 \<open>Rule_Set.append_rules "prls_3x3_linear_system" Rule_Set.empty
5.47 [\<^rule_thm>\<open>LENGTH_CONS\<close>,
5.48 \<^rule_thm>\<open>LENGTH_NIL\<close>,
5.49 - \<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_"),
5.50 + \<^rule_eval>\<open>plus\<close> (**)(Calc_Binop.numeric "#add_"),
5.51 \<^rule_eval>\<open>HOL.eq\<close> (Prog_Expr.eval_equal "#equal_")]\<close>
5.52 CAS: "solveSystem e_s v_s"
5.53 Given: "equalities e_s" "solveForVars v_s"
5.54 @@ -433,7 +433,7 @@
5.55 \<open>Rule_Set.append_rules "prls_4x4_linear_system" Rule_Set.empty
5.56 [\<^rule_thm>\<open>LENGTH_CONS\<close>,
5.57 \<^rule_thm>\<open>LENGTH_NIL\<close>,
5.58 - \<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_"),
5.59 + \<^rule_eval>\<open>plus\<close> (**)(Calc_Binop.numeric "#add_"),
5.60 \<^rule_eval>\<open>HOL.eq\<close> (Prog_Expr.eval_equal "#equal_")]\<close>
5.61 CAS: "solveSystem e_s v_s"
5.62 Given: "equalities e_s" "solveForVars v_s"
5.63 @@ -470,11 +470,11 @@
5.64 [(*for asm in NTH_CONS ...*)
5.65 \<^rule_eval>\<open>less\<close> (Prog_Expr.eval_equ "#less_"),
5.66 (*2nd NTH_CONS pushes n+-1 into asms*)
5.67 - \<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_")
5.68 + \<^rule_eval>\<open>plus\<close> (**)(Calc_Binop.numeric "#add_")
5.69 ],
5.70 srls = Rule_Set.Empty, calc = [], errpatts = [],
5.71 rules = [\<^rule_thm>\<open>NTH_CONS\<close>,
5.72 - \<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_"),
5.73 + \<^rule_eval>\<open>plus\<close> (**)(Calc_Binop.numeric "#add_"),
5.74 \<^rule_thm>\<open>NTH_NIL\<close>],
5.75 scr = Rule.Empty_Prog};
5.76 \<close>
6.1 --- a/src/Tools/isac/Knowledge/Integrate.thy Thu Aug 04 15:38:42 2022 +0200
6.2 +++ b/src/Tools/isac/Knowledge/Integrate.thy Thu Aug 04 16:48:37 2022 +0200
6.3 @@ -130,7 +130,7 @@
6.4 \<^rule_thm>\<open>integral_add\<close>,
6.5 \<^rule_thm>\<open>integral_mult\<close>,
6.6 \<^rule_thm>\<open>integral_pow\<close>,
6.7 - \<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_")(*for n+1*)],
6.8 + \<^rule_eval>\<open>plus\<close> (**)(Calc_Binop.numeric "#add_")(*for n+1*)],
6.9 scr = Rule.Empty_Prog};
6.10 \<close>
6.11 ML \<open>
7.1 --- a/src/Tools/isac/Knowledge/Inverse_Z_Transform.thy Thu Aug 04 15:38:42 2022 +0200
7.2 +++ b/src/Tools/isac/Knowledge/Inverse_Z_Transform.thy Thu Aug 04 16:48:37 2022 +0200
7.3 @@ -115,10 +115,10 @@
7.4 erls = Rule_Set.append_rules "erls_in_srls_partial_fraction" Rule_Set.empty [
7.5 \<^rule_eval>\<open>less\<close> (Prog_Expr.eval_equ "#less_"), (* ...for asm in NTH_CONS*)
7.6 (*2nd NTH_CONS pushes n+-1 into asms*)
7.7 - \<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_")],
7.8 + \<^rule_eval>\<open>plus\<close> (**)(Calc_Binop.numeric "#add_")],
7.9 srls = Rule_Set.Empty, calc = [], errpatts = [],
7.10 rules = [\<^rule_thm>\<open>NTH_CONS\<close>,
7.11 - \<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_"),
7.12 + \<^rule_eval>\<open>plus\<close> (**)(Calc_Binop.numeric "#add_"),
7.13 \<^rule_thm>\<open>NTH_NIL\<close>,
7.14 \<^rule_eval>\<open>Prog_Expr.lhs\<close> (Prog_Expr.eval_lhs "eval_lhs_"),
7.15 \<^rule_eval>\<open>Prog_Expr.rhs\<close> (Prog_Expr.eval_rhs"eval_rhs_"),
8.1 --- a/src/Tools/isac/Knowledge/LinEq.thy Thu Aug 04 15:38:42 2022 +0200
8.2 +++ b/src/Tools/isac/Knowledge/LinEq.thy Thu Aug 04 16:48:37 2022 +0200
8.3 @@ -46,7 +46,7 @@
8.4 (*
8.5 Don't use
8.6 \<^rule_eval>\<open>divide\<close> (Prog_Expr.eval_cancel "#divide_e"),
8.7 - \<^rule_eval>\<open>realpow\<close> (**)(eval_binop "#power_"),
8.8 + \<^rule_eval>\<open>realpow\<close> (**)(Calc_Binop.numeric "#power_"),
8.9 *)
8.10 ];
8.11
8.12 @@ -57,7 +57,7 @@
8.13 (*
8.14 Don't use
8.15 \<^rule_eval>\<open>divide\<close> (Prog_Expr.eval_cancel "#divide_e"),
8.16 - \<^rule_eval>\<open>realpow\<close> (**)(eval_binop "#power_"),
8.17 + \<^rule_eval>\<open>realpow\<close> (**)(Calc_Binop.numeric "#power_"),
8.18 *)
8.19 ];
8.20 \<close>
8.21 @@ -72,14 +72,14 @@
8.22 calc = [], errpatts = [],
8.23 rules = [
8.24 \<^rule_thm>\<open>real_assoc_1\<close>,
8.25 - \<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_"),
8.26 - \<^rule_eval>\<open>minus\<close> (**)(eval_binop "#sub_"),
8.27 - \<^rule_eval>\<open>times\<close> (**)(eval_binop "#mult_"),
8.28 + \<^rule_eval>\<open>plus\<close> (**)(Calc_Binop.numeric "#add_"),
8.29 + \<^rule_eval>\<open>minus\<close> (**)(Calc_Binop.numeric "#sub_"),
8.30 + \<^rule_eval>\<open>times\<close> (**)(Calc_Binop.numeric "#mult_"),
8.31 (* Don't use
8.32 \<^rule_eval>\<open>divide\<close> (Prog_Expr.eval_cancel "#divide_e"),
8.33 \<^rule_eval>\<open>sqrt\<close> (eval_sqrt "#sqrt_"),
8.34 *)
8.35 - \<^rule_eval>\<open>realpow\<close> (**)(eval_binop "#power_")],
8.36 + \<^rule_eval>\<open>realpow\<close> (**)(Calc_Binop.numeric "#power_")],
8.37 scr = Rule.Empty_Prog});
8.38 \<close>
8.39 rule_set_knowledge LinPoly_simplify = LinPoly_simplify
9.1 --- a/src/Tools/isac/Knowledge/Partial_Fractions.thy Thu Aug 04 15:38:42 2022 +0200
9.2 +++ b/src/Tools/isac/Knowledge/Partial_Fractions.thy Thu Aug 04 16:48:37 2022 +0200
9.3 @@ -163,11 +163,11 @@
9.4 [(*for asm in NTH_CONS ...*)
9.5 \<^rule_eval>\<open>less\<close> (Prog_Expr.eval_equ "#less_"),
9.6 (*2nd NTH_CONS pushes n+-1 into asms*)
9.7 - \<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_")],
9.8 + \<^rule_eval>\<open>plus\<close> (**)(Calc_Binop.numeric "#add_")],
9.9 srls = Rule_Set.Empty, calc = [], errpatts = [],
9.10 rules = [
9.11 \<^rule_thm>\<open>NTH_CONS\<close>,
9.12 - \<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_"),
9.13 + \<^rule_eval>\<open>plus\<close> (**)(Calc_Binop.numeric "#add_"),
9.14 \<^rule_thm>\<open>NTH_NIL\<close>,
9.15 \<^rule_eval>\<open>Prog_Expr.lhs\<close> (Prog_Expr.eval_lhs "eval_lhs_"),
9.16 \<^rule_eval>\<open>Prog_Expr.rhs\<close> (Prog_Expr.eval_rhs"eval_rhs_"),
10.1 --- a/src/Tools/isac/Knowledge/Poly.thy Thu Aug 04 15:38:42 2022 +0200
10.2 +++ b/src/Tools/isac/Knowledge/Poly.thy Thu Aug 04 16:48:37 2022 +0200
10.3 @@ -708,18 +708,18 @@
10.4 val Poly_erls = Rule_Set.append_rules "Poly_erls" Atools_erls [
10.5 \<^rule_eval>\<open>HOL.eq\<close> (Prog_Expr.eval_equal "#equal_"),
10.6 \<^rule_thm>\<open>real_unari_minus\<close>,
10.7 - \<^rule_eval>\<open>plus\<close> (eval_binop "#add_"),
10.8 - \<^rule_eval>\<open>minus\<close> (eval_binop "#sub_"),
10.9 - \<^rule_eval>\<open>times\<close> (eval_binop "#mult_"),
10.10 - \<^rule_eval>\<open>realpow\<close> (eval_binop "#power_")];
10.11 + \<^rule_eval>\<open>plus\<close> (Calc_Binop.numeric "#add_"),
10.12 + \<^rule_eval>\<open>minus\<close> (Calc_Binop.numeric "#sub_"),
10.13 + \<^rule_eval>\<open>times\<close> (Calc_Binop.numeric "#mult_"),
10.14 + \<^rule_eval>\<open>realpow\<close> (Calc_Binop.numeric "#power_")];
10.15
10.16 val poly_crls = Rule_Set.append_rules "poly_crls" Atools_crls [
10.17 \<^rule_eval>\<open>HOL.eq\<close> (Prog_Expr.eval_equal "#equal_"),
10.18 \<^rule_thm>\<open>real_unari_minus\<close>,
10.19 - \<^rule_eval>\<open>plus\<close> (eval_binop "#add_"),
10.20 - \<^rule_eval>\<open>minus\<close> (eval_binop "#sub_"),
10.21 - \<^rule_eval>\<open>times\<close> (eval_binop "#mult_"),
10.22 - \<^rule_eval>\<open>realpow\<close> (eval_binop "#power_")];
10.23 + \<^rule_eval>\<open>plus\<close> (Calc_Binop.numeric "#add_"),
10.24 + \<^rule_eval>\<open>minus\<close> (Calc_Binop.numeric "#sub_"),
10.25 + \<^rule_eval>\<open>times\<close> (Calc_Binop.numeric "#mult_"),
10.26 + \<^rule_eval>\<open>realpow\<close> (Calc_Binop.numeric "#power_")];
10.27 \<close>
10.28 ML \<open>
10.29 val expand =
10.30 @@ -745,7 +745,7 @@
10.31 \<^rule_eval>\<open>ord_class.less\<close> (Prog_Expr.eval_equ "#less_"),
10.32 \<^rule_thm>\<open>not_false\<close>,
10.33 \<^rule_thm>\<open>not_true\<close>,
10.34 - \<^rule_eval>\<open>plus_class.plus\<close> (eval_binop "#add_")],
10.35 + \<^rule_eval>\<open>plus_class.plus\<close> (Calc_Binop.numeric "#add_")],
10.36 scr = Rule.Empty_Prog};
10.37
10.38 \<close> ML \<open>
10.39 @@ -838,15 +838,15 @@
10.40 Rule_Def.Repeat{id = "calc_add_mult_pow_", preconds = [],
10.41 rew_ord = ("dummy_ord", Rewrite_Ord.function_empty),
10.42 erls = Atools_erls(*erls3.4.03*),srls = Rule_Set.Empty,
10.43 - calc = [("PLUS" , (\<^const_name>\<open>plus\<close>, eval_binop "#add_")),
10.44 - ("TIMES" , (\<^const_name>\<open>times\<close>, eval_binop "#mult_")),
10.45 - ("POWER", (\<^const_name>\<open>realpow\<close>, eval_binop "#power_"))
10.46 + calc = [("PLUS" , (\<^const_name>\<open>plus\<close>, Calc_Binop.numeric "#add_")),
10.47 + ("TIMES" , (\<^const_name>\<open>times\<close>, Calc_Binop.numeric "#mult_")),
10.48 + ("POWER", (\<^const_name>\<open>realpow\<close>, Calc_Binop.numeric "#power_"))
10.49 ],
10.50 errpatts = [],
10.51 rules = [
10.52 - \<^rule_eval>\<open>plus\<close> (eval_binop "#add_"),
10.53 - \<^rule_eval>\<open>times\<close> (eval_binop "#mult_"),
10.54 - \<^rule_eval>\<open>realpow\<close> (eval_binop "#power_")],
10.55 + \<^rule_eval>\<open>plus\<close> (Calc_Binop.numeric "#add_"),
10.56 + \<^rule_eval>\<open>times\<close> (Calc_Binop.numeric "#mult_"),
10.57 + \<^rule_eval>\<open>realpow\<close> (Calc_Binop.numeric "#power_")],
10.58 scr = Rule.Empty_Prog};
10.59
10.60 val reduce_012_mult_ =
10.61 @@ -865,7 +865,7 @@
10.62 Rule_Def.Repeat{id = "collect_numerals_", preconds = [],
10.63 rew_ord = ("dummy_ord", Rewrite_Ord.function_empty),
10.64 erls = Atools_erls, srls = Rule_Set.Empty,
10.65 - calc = [("PLUS" , (\<^const_name>\<open>plus\<close>, eval_binop "#add_"))
10.66 + calc = [("PLUS" , (\<^const_name>\<open>plus\<close>, Calc_Binop.numeric "#add_"))
10.67 ], errpatts = [],
10.68 rules = [
10.69 \<^rule_thm>\<open>real_num_collect\<close>, (*"[| l is_num; m is_num |]==>l * n + m * n = (l + m) * n"*)
10.70 @@ -874,7 +874,7 @@
10.71 \<^rule_thm>\<open>real_one_collect\<close>, (*"m is_num ==> n + m * n = (1 + m) * n"*)
10.72 \<^rule_thm>\<open>real_one_collect_assoc_r\<close>, (*"m is_num ==> (k + n) + m * n = k + (m + 1) * n"*)
10.73
10.74 - \<^rule_eval>\<open>plus\<close> (eval_binop "#add_"),
10.75 + \<^rule_eval>\<open>plus\<close> (Calc_Binop.numeric "#add_"),
10.76
10.77 (*MG: Reihenfolge der folgenden 2 Rule.Thm muss so bleiben, wegen
10.78 (a+a)+a --> a + 2*a --> 3*a and not (a+a)+a --> 2*a + a *)
10.79 @@ -943,9 +943,9 @@
10.80 Rule_Def.Repeat{id = "collect_numerals", preconds = [],
10.81 rew_ord = ("dummy_ord", Rewrite_Ord.function_empty),
10.82 erls = Atools_erls(*erls3.4.03*),srls = Rule_Set.Empty,
10.83 - calc = [("PLUS" , (\<^const_name>\<open>plus\<close>, eval_binop "#add_")),
10.84 - ("TIMES" , (\<^const_name>\<open>times\<close>, eval_binop "#mult_")),
10.85 - ("POWER", (\<^const_name>\<open>realpow\<close>, eval_binop "#power_"))
10.86 + calc = [("PLUS" , (\<^const_name>\<open>plus\<close>, Calc_Binop.numeric "#add_")),
10.87 + ("TIMES" , (\<^const_name>\<open>times\<close>, Calc_Binop.numeric "#mult_")),
10.88 + ("POWER", (\<^const_name>\<open>realpow\<close>, Calc_Binop.numeric "#power_"))
10.89 ], errpatts = [],
10.90 rules =[
10.91 \<^rule_thm>\<open>real_num_collect\<close>, (*"[| l is_num; m is_num |]==>l * n + m * n = (l + m) * n"*)
10.92 @@ -953,9 +953,9 @@
10.93 (*"[| l is_num; m is_num |] ==> l * n + (m * n + k) = (l + m) * n + k"*)
10.94 \<^rule_thm>\<open>real_one_collect\<close>, (*"m is_num ==> n + m * n = (1 + m) * n"*)
10.95 \<^rule_thm>\<open>real_one_collect_assoc\<close>, (*"m is_num ==> k + (n + m * n) = k + (1 + m) * n"*)
10.96 - \<^rule_eval>\<open>plus\<close> (eval_binop "#add_"),
10.97 - \<^rule_eval>\<open>times\<close> (eval_binop "#mult_"),
10.98 - \<^rule_eval>\<open>realpow\<close> (eval_binop "#power_")],
10.99 + \<^rule_eval>\<open>plus\<close> (Calc_Binop.numeric "#add_"),
10.100 + \<^rule_eval>\<open>times\<close> (Calc_Binop.numeric "#mult_"),
10.101 + \<^rule_eval>\<open>realpow\<close> (Calc_Binop.numeric "#power_")],
10.102 scr = Rule.Empty_Prog};
10.103 val reduce_012 =
10.104 Rule_Def.Repeat{id = "reduce_012", preconds = [],
10.105 @@ -1032,10 +1032,10 @@
10.106 rew_ord = ("dummy_ord", Rewrite_Ord.function_empty),
10.107 erls = Rule_Set.append_rules "Rule_Set.empty-is_multUnordered" Rule_Set.empty
10.108 [\<^rule_eval>\<open>is_multUnordered\<close> (eval_is_multUnordered "")],
10.109 - calc = [("PLUS" , (\<^const_name>\<open>plus\<close>, eval_binop "#add_")),
10.110 - ("TIMES" , (\<^const_name>\<open>times\<close>, eval_binop "#mult_")),
10.111 + calc = [("PLUS" , (\<^const_name>\<open>plus\<close>, Calc_Binop.numeric "#add_")),
10.112 + ("TIMES" , (\<^const_name>\<open>times\<close>, Calc_Binop.numeric "#mult_")),
10.113 ("DIVIDE", (\<^const_name>\<open>divide\<close>, Prog_Expr.eval_cancel "#divide_e")),
10.114 - ("POWER" , (\<^const_name>\<open>realpow\<close>, eval_binop "#power_"))],
10.115 + ("POWER" , (\<^const_name>\<open>realpow\<close>, Calc_Binop.numeric "#power_"))],
10.116 errpatts = [],
10.117 scr = Rule.Rfuns {init_state = init_state,
10.118 normal_form = normal_form,
10.119 @@ -1073,10 +1073,10 @@
10.120 erls = Rule_Set.append_rules "Rule_Set.empty-is_addUnordered" Rule_Set.empty(*MG: poly_erls*)
10.121 [\<^rule_eval>\<open>is_addUnordered\<close> (eval_is_addUnordered "")],
10.122 calc = [
10.123 - ("PLUS" ,(\<^const_name>\<open>plus\<close>, eval_binop "#add_")),
10.124 - ("TIMES" ,(\<^const_name>\<open>times\<close>, eval_binop "#mult_")),
10.125 + ("PLUS" ,(\<^const_name>\<open>plus\<close>, Calc_Binop.numeric "#add_")),
10.126 + ("TIMES" ,(\<^const_name>\<open>times\<close>, Calc_Binop.numeric "#mult_")),
10.127 ("DIVIDE",(\<^const_name>\<open>divide\<close>, Prog_Expr.eval_cancel "#divide_e")),
10.128 - ("POWER" ,(\<^const_name>\<open>realpow\<close> , eval_binop "#power_"))],
10.129 + ("POWER" ,(\<^const_name>\<open>realpow\<close> , Calc_Binop.numeric "#power_"))],
10.130 errpatts = [],
10.131 scr = Rule.Rfuns {
10.132 init_state = init_state,
10.133 @@ -1113,7 +1113,7 @@
10.134 rules = [
10.135 Rule.Rls_ discard_minus,
10.136 Rule.Rls_ expand_poly_,
10.137 - \<^rule_eval>\<open>times\<close> (eval_binop "#mult_"),
10.138 + \<^rule_eval>\<open>times\<close> (Calc_Binop.numeric "#mult_"),
10.139 Rule.Rls_ order_mult_rls_,
10.140 Rule.Rls_ simplify_power_,
10.141 Rule.Rls_ calc_add_mult_pow_,
10.142 @@ -1132,7 +1132,7 @@
10.143 rules = [
10.144 Rule.Rls_ discard_minus,
10.145 Rule.Rls_ expand_poly_,
10.146 - \<^rule_eval>\<open>times\<close> (eval_binop "#mult_"),
10.147 + \<^rule_eval>\<open>times\<close> (Calc_Binop.numeric "#mult_"),
10.148 Rule.Rls_ order_mult_rls_,
10.149 Rule.Rls_ simplify_power_,
10.150 Rule.Rls_ calc_add_mult_pow_,
10.151 @@ -1154,7 +1154,7 @@
10.152 rules = [
10.153 Rule.Rls_ discard_minus,
10.154 Rule.Rls_ expand_poly_rat_,(*ignors rationals*)
10.155 - \<^rule_eval>\<open>times\<close> (eval_binop "#mult_"),
10.156 + \<^rule_eval>\<open>times\<close> (Calc_Binop.numeric "#mult_"),
10.157 Rule.Rls_ order_mult_rls_,
10.158 Rule.Rls_ simplify_power_,
10.159 Rule.Rls_ calc_add_mult_pow_,
10.160 @@ -1171,9 +1171,9 @@
10.161 val rev_rew_p =
10.162 Rule_Set.Sequence{id = "rev_rew_p", preconds = [], rew_ord = ("termlessI",termlessI),
10.163 erls = Atools_erls, srls = Rule_Set.Empty,
10.164 - calc = [(*("PLUS" , (\<^const_name>\<open>plus\<close>, eval_binop "#add_")),
10.165 - ("TIMES" , (\<^const_name>\<open>times\<close>, eval_binop "#mult_")),
10.166 - ("POWER", (\<^const_name>\<open>realpow\<close>, eval_binop "#power_"))*)
10.167 + calc = [(*("PLUS" , (\<^const_name>\<open>plus\<close>, Calc_Binop.numeric "#add_")),
10.168 + ("TIMES" , (\<^const_name>\<open>times\<close>, Calc_Binop.numeric "#mult_")),
10.169 + ("POWER", (\<^const_name>\<open>realpow\<close>, Calc_Binop.numeric "#power_"))*)
10.170 ], errpatts = [],
10.171 rules = [
10.172 \<^rule_thm>\<open>real_plus_binom_times\<close>, (*"(a + b)*(a + b) = a ^ 2 + 2 * a * b + b ^ 2*)
10.173 @@ -1189,9 +1189,9 @@
10.174 Rule.Rls_ order_mult_rls_,
10.175 (*Rule.Rls_ order_add_rls_,*)
10.176
10.177 - \<^rule_eval>\<open>plus\<close> (eval_binop "#add_"),
10.178 - \<^rule_eval>\<open>times\<close> (eval_binop "#mult_"),
10.179 - \<^rule_eval>\<open>realpow\<close> (eval_binop "#power_"),
10.180 + \<^rule_eval>\<open>plus\<close> (Calc_Binop.numeric "#add_"),
10.181 + \<^rule_eval>\<open>times\<close> (Calc_Binop.numeric "#mult_"),
10.182 + \<^rule_eval>\<open>realpow\<close> (Calc_Binop.numeric "#power_"),
10.183
10.184 \<^rule_thm_sym>\<open>realpow_twoI\<close>, (*"r1 * r1 = r1 \<up> 2"*)
10.185 \<^rule_thm_sym>\<open>real_mult_2\<close>, (*"z1 + z1 = 2 * z1"*)
10.186 @@ -1204,9 +1204,9 @@
10.187
10.188 \<^rule_thm>\<open>realpow_multI\<close>, (*"(r * s) \<up> n = r \<up> n * s \<up> n"*)
10.189
10.190 - \<^rule_eval>\<open>plus\<close> (eval_binop "#add_"),
10.191 - \<^rule_eval>\<open>times\<close> (eval_binop "#mult_"),
10.192 - \<^rule_eval>\<open>realpow\<close> (eval_binop "#power_"),
10.193 + \<^rule_eval>\<open>plus\<close> (Calc_Binop.numeric "#add_"),
10.194 + \<^rule_eval>\<open>times\<close> (Calc_Binop.numeric "#mult_"),
10.195 + \<^rule_eval>\<open>realpow\<close> (Calc_Binop.numeric "#power_"),
10.196
10.197 \<^rule_thm>\<open>mult_1_left\<close>, (*"1 * z = z"*)
10.198 \<^rule_thm>\<open>mult_zero_left\<close>, (*"0 * z = 0"*)
10.199 @@ -1256,9 +1256,9 @@
10.200 val expand_binoms =
10.201 Rule_Def.Repeat{id = "expand_binoms", preconds = [], rew_ord = ("termlessI",termlessI),
10.202 erls = Atools_erls, srls = Rule_Set.Empty,
10.203 - calc = [("PLUS" , (\<^const_name>\<open>plus\<close>, eval_binop "#add_")),
10.204 - ("TIMES" , (\<^const_name>\<open>times\<close>, eval_binop "#mult_")),
10.205 - ("POWER", (\<^const_name>\<open>realpow\<close>, eval_binop "#power_"))
10.206 + calc = [("PLUS" , (\<^const_name>\<open>plus\<close>, Calc_Binop.numeric "#add_")),
10.207 + ("TIMES" , (\<^const_name>\<open>times\<close>, Calc_Binop.numeric "#mult_")),
10.208 + ("POWER", (\<^const_name>\<open>realpow\<close>, Calc_Binop.numeric "#power_"))
10.209 ], errpatts = [],
10.210 rules = [
10.211 \<^rule_thm>\<open>real_plus_binom_pow2\<close>, (*"(a + b) \<up> 2 = a \<up> 2 + 2 * a * b + b \<up> 2"*)
10.212 @@ -1285,9 +1285,9 @@
10.213 \<^rule_thm>\<open>mult_zero_left\<close>, (*"0 * z = 0"*)
10.214 \<^rule_thm>\<open>add_0_left\<close>, (*"0 + z = z"*)
10.215
10.216 - \<^rule_eval>\<open>plus\<close> (eval_binop "#add_"),
10.217 - \<^rule_eval>\<open>times\<close> (eval_binop "#mult_"),
10.218 - \<^rule_eval>\<open>realpow\<close> (eval_binop "#power_"),
10.219 + \<^rule_eval>\<open>plus\<close> (Calc_Binop.numeric "#add_"),
10.220 + \<^rule_eval>\<open>times\<close> (Calc_Binop.numeric "#mult_"),
10.221 + \<^rule_eval>\<open>realpow\<close> (Calc_Binop.numeric "#power_"),
10.222 (*\<^rule_thm>\<open>mult.commute\<close>,
10.223 (*AC-rewriting*)
10.224 \<^rule_thm>\<open>real_mult_left_commute\<close>,
10.225 @@ -1307,9 +1307,9 @@
10.226 \<^rule_thm>\<open>real_one_collect\<close>, (*"m is_num ==> n + m * n = (1 + m) * n"*)
10.227 \<^rule_thm>\<open>real_one_collect_assoc\<close>, (*"m is_num ==> k + (n + m * n) = k + (1 + m) * n"*)
10.228
10.229 - \<^rule_eval>\<open>plus\<close> (eval_binop "#add_"),
10.230 - \<^rule_eval>\<open>times\<close> (eval_binop "#mult_"),
10.231 - \<^rule_eval>\<open>realpow\<close> (eval_binop "#power_")],
10.232 + \<^rule_eval>\<open>plus\<close> (Calc_Binop.numeric "#add_"),
10.233 + \<^rule_eval>\<open>times\<close> (Calc_Binop.numeric "#mult_"),
10.234 + \<^rule_eval>\<open>realpow\<close> (Calc_Binop.numeric "#power_")],
10.235 scr = Rule.Prog (Program.prep_program @{thm expand_binoms_2.simps})};
10.236 \<close>
10.237
11.1 --- a/src/Tools/isac/Knowledge/PolyEq.thy Thu Aug 04 15:38:42 2022 +0200
11.2 +++ b/src/Tools/isac/Knowledge/PolyEq.thy Thu Aug 04 16:48:37 2022 +0200
11.3 @@ -406,12 +406,12 @@
11.4 \<^rule_thm>\<open>real_diff_minus\<close>,
11.5 \<^rule_thm>\<open>real_unari_minus\<close>,
11.6 \<^rule_thm>\<open>realpow_multI\<close>,
11.7 - \<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_"),
11.8 - \<^rule_eval>\<open>minus\<close> (**)(eval_binop "#sub_"),
11.9 - \<^rule_eval>\<open>times\<close> (**)(eval_binop "#mult_"),
11.10 + \<^rule_eval>\<open>plus\<close> (**)(Calc_Binop.numeric "#add_"),
11.11 + \<^rule_eval>\<open>minus\<close> (**)(Calc_Binop.numeric "#sub_"),
11.12 + \<^rule_eval>\<open>times\<close> (**)(Calc_Binop.numeric "#mult_"),
11.13 \<^rule_eval>\<open>divide\<close> (Prog_Expr.eval_cancel "#divide_e"),
11.14 \<^rule_eval>\<open>sqrt\<close> (eval_sqrt "#sqrt_"),
11.15 - \<^rule_eval>\<open>realpow\<close> (**)(eval_binop "#power_"),
11.16 + \<^rule_eval>\<open>realpow\<close> (**)(Calc_Binop.numeric "#power_"),
11.17 Rule.Rls_ reduce_012],
11.18 scr = Rule.Empty_Prog});
11.19 \<close>
12.1 --- a/src/Tools/isac/Knowledge/PolyMinus.thy Thu Aug 04 15:38:42 2022 +0200
12.2 +++ b/src/Tools/isac/Knowledge/PolyMinus.thy Thu Aug 04 16:48:37 2022 +0200
12.3 @@ -232,8 +232,8 @@
12.4 \<^rule_thm>\<open>subtrahiere_x_minus1_minus\<close>, (*"[| l is_num |] ==> (x - v) - l * v = x + (-1 - l) * v"*)
12.5 \<^rule_thm>\<open>subtrahiere_x_minus_minus1\<close>, (*"[| m is_num |] ==> (x - m * v) - v = x + (-m - 1) * v"*)
12.6
12.7 - \<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_"),
12.8 - \<^rule_eval>\<open>minus\<close> (**)(eval_binop "#subtr_"),
12.9 + \<^rule_eval>\<open>plus\<close> (**)(Calc_Binop.numeric "#add_"),
12.10 + \<^rule_eval>\<open>minus\<close> (**)(Calc_Binop.numeric "#subtr_"),
12.11
12.12 (*MG: Reihenfolge der folgenden 2 Rule.Thm muss so bleiben, wegen
12.13 (a+a)+a --> a + 2*a --> 3*a and not (a+a)+a --> 2*a + a *)
12.14 @@ -257,7 +257,7 @@
12.15 \<^rule_thm>\<open>vorzeichen_minus_weg3\<close>, (*"l kleiner 0 ==> k + a - l * b = k + a + -l * b"*)
12.16 \<^rule_thm>\<open>vorzeichen_minus_weg4\<close>, (*"l kleiner 0 ==> k - a - l * b = k - a + -l * b"*)
12.17
12.18 - \<^rule_eval>\<open>times\<close> (**)(eval_binop "#mult_"),
12.19 + \<^rule_eval>\<open>times\<close> (**)(Calc_Binop.numeric "#mult_"),
12.20
12.21 \<^rule_thm>\<open>mult_zero_left\<close>, (*"0 * z = 0"*)
12.22 \<^rule_thm>\<open>mult_1_left\<close>, (*"1 * z = z"*)
12.23 @@ -316,9 +316,9 @@
12.24 Rule.Rls_ verschoenere];
12.25 val rechnen =
12.26 Rule_Set.append_rules "rechnen" Rule_Set.empty [
12.27 - \<^rule_eval>\<open>times\<close> (**)(eval_binop "#mult_"),
12.28 - \<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_"),
12.29 - \<^rule_eval>\<open>minus\<close> (**)(eval_binop "#subtr_")];
12.30 + \<^rule_eval>\<open>times\<close> (**)(Calc_Binop.numeric "#mult_"),
12.31 + \<^rule_eval>\<open>plus\<close> (**)(Calc_Binop.numeric "#add_"),
12.32 + \<^rule_eval>\<open>minus\<close> (**)(Calc_Binop.numeric "#subtr_")];
12.33 \<close>
12.34 rule_set_knowledge
12.35 ordne_alphabetisch = \<open>prep_rls' ordne_alphabetisch\<close> and
13.1 --- a/src/Tools/isac/Knowledge/Rational.thy Thu Aug 04 15:38:42 2022 +0200
13.2 +++ b/src/Tools/isac/Knowledge/Rational.thy Thu Aug 04 16:48:37 2022 +0200
13.3 @@ -516,10 +516,10 @@
13.4 rew_ord = ("ord_make_polynomial", ord_make_polynomial false \<^theory>),
13.5 erls = rational_erls,
13.6 calc =
13.7 - [("PLUS", (\<^const_name>\<open>plus\<close>, (**)eval_binop "#add_")),
13.8 - ("TIMES" , (\<^const_name>\<open>times\<close>, (**)eval_binop "#mult_")),
13.9 + [("PLUS", (\<^const_name>\<open>plus\<close>, (**)Calc_Binop.numeric "#add_")),
13.10 + ("TIMES" , (\<^const_name>\<open>times\<close>, (**)Calc_Binop.numeric "#mult_")),
13.11 ("DIVIDE", (\<^const_name>\<open>divide\<close>, Prog_Expr.eval_cancel "#divide_e")),
13.12 - ("POWER", (\<^const_name>\<open>realpow\<close>, (**)eval_binop "#power_"))],
13.13 + ("POWER", (\<^const_name>\<open>realpow\<close>, (**)Calc_Binop.numeric "#power_"))],
13.14 errpatts = [],
13.15 scr =
13.16 Rule.Rfuns {init_state = init_state \<^theory> Atools_erls ro,
13.17 @@ -583,10 +583,10 @@
13.18 Rule_Set.Rrls {id = "add_fractions_p", prepat=prepat,
13.19 rew_ord = ("ord_make_polynomial", ord_make_polynomial false \<^theory>),
13.20 erls = rational_erls,
13.21 - calc = [("PLUS", (\<^const_name>\<open>plus\<close>, (**)eval_binop "#add_")),
13.22 - ("TIMES", (\<^const_name>\<open>times\<close>, (**)eval_binop "#mult_")),
13.23 + calc = [("PLUS", (\<^const_name>\<open>plus\<close>, (**)Calc_Binop.numeric "#add_")),
13.24 + ("TIMES", (\<^const_name>\<open>times\<close>, (**)Calc_Binop.numeric "#mult_")),
13.25 ("DIVIDE", (\<^const_name>\<open>divide\<close>, Prog_Expr.eval_cancel "#divide_e")),
13.26 - ("POWER", (\<^const_name>\<open>realpow\<close>, (**)eval_binop "#power_"))],
13.27 + ("POWER", (\<^const_name>\<open>realpow\<close>, (**)Calc_Binop.numeric "#power_"))],
13.28 errpatts = [],
13.29 scr = Rule.Rfuns {init_state = init_state \<^theory> Atools_erls ro,
13.30 normal_form = add_fraction_p_ \<^theory>,
13.31 @@ -623,7 +623,7 @@
13.32 (*----- distribute none-atoms -----*)
13.33 \<^rule_thm>\<open>realpow_def_atom\<close>, (*"[| 1 < n; ~ (r is_atom) |]==>r \<up> n = r * r \<up> (n + -1)"*)
13.34 \<^rule_thm>\<open>realpow_eq_oneI\<close>, (*"1 \<up> n = 1"*)
13.35 - \<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_")],
13.36 + \<^rule_eval>\<open>plus\<close> (**)(Calc_Binop.numeric "#add_")],
13.37 scr = Rule.Empty_Prog});
13.38
13.39 \<close> ML \<open>
14.1 --- a/src/Tools/isac/Knowledge/Root.thy Thu Aug 04 15:38:42 2022 +0200
14.2 +++ b/src/Tools/isac/Knowledge/Root.thy Thu Aug 04 16:48:37 2022 +0200
14.3 @@ -162,10 +162,10 @@
14.4 \<^rule_thm>\<open>real_unari_minus\<close>,
14.5 \<^rule_eval>\<open>sqrt\<close> (eval_sqrt "#sqrt_"),
14.6 \<^rule_eval>\<open>divide\<close> (Prog_Expr.eval_cancel "#divide_e"),
14.7 - \<^rule_eval>\<open>realpow\<close> (**)(eval_binop "#power_"),
14.8 - \<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_"),
14.9 - \<^rule_eval>\<open>minus\<close> (**)(eval_binop "#sub_"),
14.10 - \<^rule_eval>\<open>times\<close> (**)(eval_binop "#mult_"),
14.11 + \<^rule_eval>\<open>realpow\<close> (**)(Calc_Binop.numeric "#power_"),
14.12 + \<^rule_eval>\<open>plus\<close> (**)(Calc_Binop.numeric "#add_"),
14.13 + \<^rule_eval>\<open>minus\<close> (**)(Calc_Binop.numeric "#sub_"),
14.14 + \<^rule_eval>\<open>times\<close> (**)(Calc_Binop.numeric "#mult_"),
14.15 \<^rule_eval>\<open>HOL.eq\<close> (Prog_Expr.eval_equal "#equal_")];
14.16
14.17 val Root_erls =
14.18 @@ -173,10 +173,10 @@
14.19 \<^rule_thm>\<open>real_unari_minus\<close>,
14.20 \<^rule_eval>\<open>sqrt\<close> (eval_sqrt "#sqrt_"),
14.21 \<^rule_eval>\<open>Rings.divide_class.divide\<close> (Prog_Expr.eval_cancel "#divide_e"),
14.22 - \<^rule_eval>\<open>realpow\<close> (**)(eval_binop "#power_"),
14.23 - \<^rule_eval>\<open>Groups.plus_class.plus\<close> (**)(eval_binop "#add_"),
14.24 - \<^rule_eval>\<open>Groups.minus_class.minus\<close> (**)(eval_binop "#sub_"),
14.25 - \<^rule_eval>\<open>Groups.times_class.times\<close> (**)(eval_binop "#mult_"),
14.26 + \<^rule_eval>\<open>realpow\<close> (**)(Calc_Binop.numeric "#power_"),
14.27 + \<^rule_eval>\<open>Groups.plus_class.plus\<close> (**)(Calc_Binop.numeric "#add_"),
14.28 + \<^rule_eval>\<open>Groups.minus_class.minus\<close> (**)(Calc_Binop.numeric "#sub_"),
14.29 + \<^rule_eval>\<open>Groups.times_class.times\<close> (**)(Calc_Binop.numeric "#mult_"),
14.30 \<^rule_eval>\<open>HOL.eq\<close> (Prog_Expr.eval_equal "#equal_")];
14.31 val Root_erls =
14.32 Rule_Set.append_erls_rules "Root_erls_erls" Root_erls [
14.33 @@ -222,9 +222,9 @@
14.34 \<^rule_thm>\<open>real_one_collect\<close>, (*"m is_num ==> n + m * n = (1 + m) * n"*)
14.35 \<^rule_thm>\<open>real_one_collect_assoc\<close>, (*"m is_num ==> k + (n + m * n) = k + (1 + m) * n"*)
14.36
14.37 - \<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_"),
14.38 - \<^rule_eval>\<open>times\<close> (**)(eval_binop "#mult_"),
14.39 - \<^rule_eval>\<open>realpow\<close> (**)(eval_binop "#power_")],
14.40 + \<^rule_eval>\<open>plus\<close> (**)(Calc_Binop.numeric "#add_"),
14.41 + \<^rule_eval>\<open>times\<close> (**)(Calc_Binop.numeric "#mult_"),
14.42 + \<^rule_eval>\<open>realpow\<close> (**)(Calc_Binop.numeric "#power_")],
14.43 scr = Rule.Empty_Prog});
14.44 \<close>
14.45 rule_set_knowledge make_rooteq = make_rooteq
14.46 @@ -254,12 +254,12 @@
14.47 \<^rule_thm>\<open>mult_zero_left\<close>, (*"0 * z = 0"*)
14.48 \<^rule_thm>\<open>add_0_left\<close>, (*"0 + z = z"*)
14.49
14.50 - \<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_"),
14.51 - \<^rule_eval>\<open>minus\<close> (**)(eval_binop "#sub_"),
14.52 - \<^rule_eval>\<open>times\<close> (**)(eval_binop "#mult_"),
14.53 + \<^rule_eval>\<open>plus\<close> (**)(Calc_Binop.numeric "#add_"),
14.54 + \<^rule_eval>\<open>minus\<close> (**)(Calc_Binop.numeric "#sub_"),
14.55 + \<^rule_eval>\<open>times\<close> (**)(Calc_Binop.numeric "#mult_"),
14.56 \<^rule_eval>\<open>divide\<close> (Prog_Expr.eval_cancel "#divide_e"),
14.57 \<^rule_eval>\<open>sqrt\<close> (eval_sqrt "#sqrt_"),
14.58 - \<^rule_eval>\<open>realpow\<close> (**)(eval_binop "#power_"),
14.59 + \<^rule_eval>\<open>realpow\<close> (**)(Calc_Binop.numeric "#power_"),
14.60
14.61 \<^rule_thm_sym>\<open>realpow_twoI\<close>, (*"r1 * r1 = r1 \<up> 2"*)
14.62 \<^rule_thm>\<open>realpow_plus_1\<close>, (*"r * r \<up> n = r \<up> (n + 1)"*)
14.63 @@ -270,12 +270,12 @@
14.64 \<^rule_thm>\<open>real_one_collect\<close>, (*"m is_num ==> n + m * n = (1 + m) * n"*)
14.65 \<^rule_thm>\<open>real_one_collect_assoc\<close>, (*"m is_num ==> k + (n + m * n) = k + (1 + m) * n"*)
14.66
14.67 - \<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_"),
14.68 - \<^rule_eval>\<open>minus\<close> (**)(eval_binop "#sub_"),
14.69 - \<^rule_eval>\<open>times\<close> (**)(eval_binop "#mult_"),
14.70 + \<^rule_eval>\<open>plus\<close> (**)(Calc_Binop.numeric "#add_"),
14.71 + \<^rule_eval>\<open>minus\<close> (**)(Calc_Binop.numeric "#sub_"),
14.72 + \<^rule_eval>\<open>times\<close> (**)(Calc_Binop.numeric "#mult_"),
14.73 \<^rule_eval>\<open>divide\<close> (Prog_Expr.eval_cancel "#divide_e"),
14.74 \<^rule_eval>\<open>sqrt\<close> (eval_sqrt "#sqrt_"),
14.75 - \<^rule_eval>\<open>realpow\<close> (**)(eval_binop "#power_")],
14.76 + \<^rule_eval>\<open>realpow\<close> (**)(Calc_Binop.numeric "#power_")],
14.77 scr = Rule.Empty_Prog});
14.78 \<close>
14.79 rule_set_knowledge expand_rootbinoms = expand_rootbinoms
15.1 --- a/src/Tools/isac/Knowledge/RootEq.thy Thu Aug 04 15:38:42 2022 +0200
15.2 +++ b/src/Tools/isac/Knowledge/RootEq.thy Thu Aug 04 16:48:37 2022 +0200
15.3 @@ -318,12 +318,12 @@
15.4 rules = [
15.5 \<^rule_thm>\<open>real_assoc_1\<close>, (* a+(b+c) = a+b+c *)
15.6 \<^rule_thm>\<open>real_assoc_2\<close>, (* a*(b*c) = a*b*c *)
15.7 - \<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_"),
15.8 - \<^rule_eval>\<open>minus\<close> (**)(eval_binop "#sub_"),
15.9 - \<^rule_eval>\<open>times\<close> (**)(eval_binop "#mult_"),
15.10 + \<^rule_eval>\<open>plus\<close> (**)(Calc_Binop.numeric "#add_"),
15.11 + \<^rule_eval>\<open>minus\<close> (**)(Calc_Binop.numeric "#sub_"),
15.12 + \<^rule_eval>\<open>times\<close> (**)(Calc_Binop.numeric "#mult_"),
15.13 \<^rule_eval>\<open>divide\<close> (Prog_Expr.eval_cancel "#divide_e"),
15.14 \<^rule_eval>\<open>sqrt\<close> (eval_sqrt "#sqrt_"),
15.15 - \<^rule_eval>\<open>realpow\<close> (**)(eval_binop "#power_"),
15.16 + \<^rule_eval>\<open>realpow\<close> (**)(Calc_Binop.numeric "#power_"),
15.17 \<^rule_thm>\<open>real_plus_binom_pow2\<close>,
15.18 \<^rule_thm>\<open>real_minus_binom_pow2\<close>,
15.19 \<^rule_thm>\<open>realpow_mul\<close>, (* (a * b)^n = a^n * b^n*)
16.1 --- a/src/Tools/isac/Knowledge/Test.thy Thu Aug 04 15:38:42 2022 +0200
16.2 +++ b/src/Tools/isac/Knowledge/Test.thy Thu Aug 04 16:48:37 2022 +0200
16.3 @@ -378,9 +378,9 @@
16.4 \<^rule_eval>\<open>Prog_Expr.is_num\<close> (Prog_Expr.eval_is_num "#is_num_"),
16.5 \<^rule_eval>\<open>Prog_Expr.matches\<close> (Prog_Expr.eval_matches ""),
16.6
16.7 - \<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_"),
16.8 - \<^rule_eval>\<open>times\<close> (**)(eval_binop "#mult_"),
16.9 - \<^rule_eval>\<open>realpow\<close> (**)(eval_binop "#power_"),
16.10 + \<^rule_eval>\<open>plus\<close> (**)(Calc_Binop.numeric "#add_"),
16.11 + \<^rule_eval>\<open>times\<close> (**)(Calc_Binop.numeric "#mult_"),
16.12 + \<^rule_eval>\<open>realpow\<close> (**)(Calc_Binop.numeric "#power_"),
16.13
16.14 \<^rule_eval>\<open>less\<close> (Prog_Expr.eval_equ "#less_"),
16.15 \<^rule_eval>\<open>less_eq\<close> (Prog_Expr.eval_equ "#less_equal_"),
16.16 @@ -421,10 +421,10 @@
16.17 \<^rule_eval>\<open>Prog_Expr.matches\<close> (Prog_Expr.eval_matches ""),
16.18 \<^rule_eval>\<open>contains_root\<close> (eval_contains_root"#contains_root_"),
16.19
16.20 - \<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_"),
16.21 - \<^rule_eval>\<open>times\<close> (**)(eval_binop "#mult_"),
16.22 + \<^rule_eval>\<open>plus\<close> (**)(Calc_Binop.numeric "#add_"),
16.23 + \<^rule_eval>\<open>times\<close> (**)(Calc_Binop.numeric "#mult_"),
16.24 \<^rule_eval>\<open>sqrt\<close> (eval_sqrt "#sqrt_"),
16.25 - \<^rule_eval>\<open>realpow\<close> (**)(eval_binop "#power_"),
16.26 + \<^rule_eval>\<open>realpow\<close> (**)(Calc_Binop.numeric "#power_"),
16.27
16.28 \<^rule_eval>\<open>less\<close> (Prog_Expr.eval_equ "#less_"),
16.29 \<^rule_eval>\<open>less_eq\<close> (Prog_Expr.eval_equ "#less_equal_"),
16.30 @@ -494,10 +494,10 @@
16.31 \<^rule_thm>\<open>radd_real_const\<close>,
16.32 (* these 2 rules are invers to distr_div_right wrt. termination.
16.33 thus they MUST be done IMMEDIATELY before calc *)
16.34 - \<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_"),
16.35 - \<^rule_eval>\<open>times\<close> (**)(eval_binop "#mult_"),
16.36 + \<^rule_eval>\<open>plus\<close> (**)(Calc_Binop.numeric "#add_"),
16.37 + \<^rule_eval>\<open>times\<close> (**)(Calc_Binop.numeric "#mult_"),
16.38 \<^rule_eval>\<open>divide\<close> (Prog_Expr.eval_cancel "#divide_e"),
16.39 - \<^rule_eval>\<open>realpow\<close> (**)(eval_binop "#power_"),
16.40 + \<^rule_eval>\<open>realpow\<close> (**)(Calc_Binop.numeric "#power_"),
16.41
16.42 \<^rule_thm>\<open>rcollect_right\<close>,
16.43 \<^rule_thm>\<open>rcollect_one_left\<close>,
16.44 @@ -599,9 +599,9 @@
16.45 rew_ord = ("ord_make_polytest", ord_make_polytest false @{theory "Poly"}),
16.46 erls = testerls, srls = Rule_Set.Empty,
16.47 calc = [
16.48 - ("PLUS" , (\<^const_name>\<open>plus\<close>, (**)eval_binop "#add_")),
16.49 - ("TIMES" , (\<^const_name>\<open>times\<close>, (**)eval_binop "#mult_")),
16.50 - ("POWER", (\<^const_name>\<open>realpow\<close>, (**)eval_binop "#power_"))],
16.51 + ("PLUS" , (\<^const_name>\<open>plus\<close>, (**)Calc_Binop.numeric "#add_")),
16.52 + ("TIMES" , (\<^const_name>\<open>times\<close>, (**)Calc_Binop.numeric "#mult_")),
16.53 + ("POWER", (\<^const_name>\<open>realpow\<close>, (**)Calc_Binop.numeric "#power_"))],
16.54 errpatts = [],
16.55 rules = [
16.56 \<^rule_thm>\<open>real_diff_minus\<close>, (*"a - b = a + (-1) * b"*)
16.57 @@ -630,18 +630,18 @@
16.58 \<^rule_thm>\<open>real_one_collect\<close>, (*"m is_num ==> n + m * n = (1 + m) * n"*)
16.59 \<^rule_thm>\<open>real_one_collect_assoc\<close>, (*"m is_num ==> k + (n + m * n) = k + (1 + m) * n"*)
16.60
16.61 - \<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_"),
16.62 - \<^rule_eval>\<open>times\<close> (**)(eval_binop "#mult_"),
16.63 - \<^rule_eval>\<open>realpow\<close> (**)(eval_binop "#power_")],
16.64 + \<^rule_eval>\<open>plus\<close> (**)(Calc_Binop.numeric "#add_"),
16.65 + \<^rule_eval>\<open>times\<close> (**)(Calc_Binop.numeric "#mult_"),
16.66 + \<^rule_eval>\<open>realpow\<close> (**)(Calc_Binop.numeric "#power_")],
16.67 scr = Rule.Empty_Prog};
16.68
16.69 val expand_binomtest =
16.70 Rule_Def.Repeat{id = "expand_binomtest", preconds = [],
16.71 rew_ord = ("termlessI",termlessI), erls = testerls, srls = Rule_Set.Empty,
16.72 calc = [
16.73 - ("PLUS" , (\<^const_name>\<open>plus\<close>, (**)eval_binop "#add_")),
16.74 - ("TIMES" , (\<^const_name>\<open>times\<close>, (**)eval_binop "#mult_")),
16.75 - ("POWER", (\<^const_name>\<open>realpow\<close>, (**)eval_binop "#power_"))
16.76 + ("PLUS" , (\<^const_name>\<open>plus\<close>, (**)Calc_Binop.numeric "#add_")),
16.77 + ("TIMES" , (\<^const_name>\<open>times\<close>, (**)Calc_Binop.numeric "#mult_")),
16.78 + ("POWER", (\<^const_name>\<open>realpow\<close>, (**)Calc_Binop.numeric "#power_"))
16.79 ],
16.80 errpatts = [],
16.81 rules = [
16.82 @@ -664,9 +664,9 @@
16.83 \<^rule_thm>\<open>mult_zero_left\<close>, (*"0 * z = 0"*)
16.84 \<^rule_thm>\<open>add_0_left\<close>, (*"0 + z = z"*)
16.85
16.86 - \<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_"),
16.87 - \<^rule_eval>\<open>times\<close> (**)(eval_binop "#mult_"),
16.88 - \<^rule_eval>\<open>realpow\<close> (**)(eval_binop "#power_"),
16.89 + \<^rule_eval>\<open>plus\<close> (**)(Calc_Binop.numeric "#add_"),
16.90 + \<^rule_eval>\<open>times\<close> (**)(Calc_Binop.numeric "#mult_"),
16.91 + \<^rule_eval>\<open>realpow\<close> (**)(Calc_Binop.numeric "#power_"),
16.92
16.93 \<^rule_thm_sym>\<open>realpow_twoI\<close>, (*"r1 * r1 = r1 \<up> 2"*)
16.94 \<^rule_thm>\<open>realpow_plus_1\<close>, (*"r * r \<up> n = r \<up> (n + 1)"*)
16.95 @@ -678,9 +678,9 @@
16.96 \<^rule_thm>\<open>real_one_collect\<close>, (*"m is_num ==> n + m * n = (1 + m) * n"*)
16.97 \<^rule_thm>\<open>real_one_collect_assoc\<close>, (*"m is_num ==> k + (n + m * n) = k + (1 + m) * n"*)
16.98
16.99 - \<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_"),
16.100 - \<^rule_eval>\<open>times\<close> (**)(eval_binop "#mult_"),
16.101 - \<^rule_eval>\<open>realpow\<close> (**)(eval_binop "#power_")],
16.102 + \<^rule_eval>\<open>plus\<close> (**)(Calc_Binop.numeric "#add_"),
16.103 + \<^rule_eval>\<open>times\<close> (**)(Calc_Binop.numeric "#mult_"),
16.104 + \<^rule_eval>\<open>realpow\<close> (**)(Calc_Binop.numeric "#power_")],
16.105 scr = Rule.Empty_Prog};
16.106 \<close>
16.107 rule_set_knowledge
17.1 --- a/src/Tools/isac/ProgLang/Calculate.thy Thu Aug 04 15:38:42 2022 +0200
17.2 +++ b/src/Tools/isac/ProgLang/Calculate.thy Thu Aug 04 16:48:37 2022 +0200
17.3 @@ -21,29 +21,37 @@
17.4 ML_file evaluate.sml
17.5
17.6 ML \<open>
17.7 -\<close> ML \<open>
17.8 +signature CALCULATE_BINARY_OPERATION =
17.9 +sig
17.10 + val numeric: string -> string -> term -> Proof.context -> (string * term) option
17.11 +\<^isac_test>\<open>
17.12 + val is_calcul_op: string -> bool
17.13 + val calcul: Proof.context -> term -> term
17.14 +\<close>
17.15 +end
17.16 +
17.17 +(**)
17.18 +structure Calc_Binop(**): CALCULATE_BINARY_OPERATION(**) =
17.19 +struct
17.20 +(**)
17.21 +
17.22 (*** evaluate binary associative operations ***)
17.23
17.24 -val is_num = can HOLogic.dest_number;
17.25 -
17.26 val is_calcul_op =
17.27 member (op =) [\<^const_name>\<open>plus\<close>, \<^const_name>\<open>minus\<close>, \<^const_name>\<open>times\<close>, \<^const_name>\<open>realpow\<close>];
17.28
17.29 fun calcul ctxt lhs =
17.30 let
17.31 val simp_ctxt =
17.32 -(*
17.33 - Proof_Context.init_global thy
17.34 -*)
17.35 ctxt |> put_simpset (Simplifier.simpset_of @{theory_context BaseDefinitions});
17.36 val eq = Simplifier.rewrite simp_ctxt (Thm.cterm_of ctxt lhs);
17.37 val rhs = Thm.term_of (Thm.rhs_of eq);
17.38 in rhs end;
17.39
17.40 -fun eval_binop (_: string) (_: string) t ctxt =
17.41 +fun numeric (_: string) (_: string) t ctxt =
17.42 (case t of
17.43 (opp as Const (c1, T)) $ (Const (c2, _) $ v $ t1) $ t2 => (* binary \<circ> (v \<circ> n1) \<circ> n2 *)
17.44 - if c1 = c2 andalso is_calcul_op c1 andalso is_num t1 andalso is_num t2 then
17.45 + if c1 = c2 andalso is_calcul_op c1 andalso Eval.is_num t1 andalso Eval.is_num t2 then
17.46 let
17.47 val opp' = Const (if c1 = \<^const_name>\<open>minus\<close> then \<^const_name>\<open>plus\<close> else c1, T);
17.48 val res = calcul ctxt (opp' $ t1 $ t2);
17.49 @@ -52,7 +60,7 @@
17.50 else NONE
17.51 | (opp as Const (c1, _)) $ t1 $ (Const (c2, _) $ t2 $ v) => (* binary \<circ> n1 \<circ> (n2 \<circ> v) *)
17.52 if c1 = c2 andalso is_calcul_op c1 andalso c1 <> \<^const_name>\<open>minus\<close>
17.53 - andalso is_num t1 andalso is_num t2
17.54 + andalso Eval.is_num t1 andalso Eval.is_num t2
17.55 then
17.56 let
17.57 val res = calcul ctxt (opp $ t1 $ t2);
17.58 @@ -62,7 +70,7 @@
17.59 end
17.60 else NONE
17.61 | Const (c, _) $ t1 $ t2 => (* binary \<circ> n1 \<circ> n2 *)
17.62 - if is_calcul_op c andalso is_num t1 andalso is_num t2 then
17.63 + if is_calcul_op c andalso Eval.is_num t1 andalso Eval.is_num t2 then
17.64 let
17.65 val res = calcul ctxt t;
17.66 val prop = HOLogic.Trueprop $ (HOLogic.mk_eq (t, res));
17.67 @@ -71,7 +79,7 @@
17.68 end
17.69 else NONE
17.70 | _ => NONE);
17.71 -
17.72 +(**)end(**)
17.73 \<close> ML \<open>
17.74 \<close> ML \<open>
17.75 \<close>
18.1 --- a/src/Tools/isac/ProgLang/evaluate.sml Thu Aug 04 15:38:42 2022 +0200
18.2 +++ b/src/Tools/isac/ProgLang/evaluate.sml Thu Aug 04 16:48:37 2022 +0200
18.3 @@ -7,6 +7,7 @@
18.4
18.5 signature EVALUATE =
18.6 sig
18.7 + val is_num: term -> bool
18.8 val calc_equ: string -> int * int -> bool
18.9 val power: int -> int -> int
18.10 val sign_mult: int -> int -> int
18.11 @@ -32,6 +33,8 @@
18.12 struct
18.13 (**)
18.14
18.15 +val is_num = can HOLogic.dest_number;
18.16 +
18.17 (* trace internal steps of isac's numeral calculations *)
18.18 val eval_trace = Attrib.setup_config_bool \<^binding>\<open>eval_trace\<close> (K false);
18.19