1.1 --- a/src/Tools/isac/BaseDefinitions/rule.sml Thu Jun 10 17:06:32 2021 +0200
1.2 +++ b/src/Tools/isac/BaseDefinitions/rule.sml Fri Jun 11 11:49:34 2021 +0200
1.3 @@ -21,6 +21,8 @@
1.4 val distinct' : rule list -> rule list
1.5
1.6 val thm_id: rule -> string
1.7 +
1.8 + val make_eval: string -> Rule_Def.eval_fn -> rule
1.9 end
1.10
1.11 (**)
1.12 @@ -68,4 +70,14 @@
1.13 fun thm (Rule_Def.Thm (_, thm)) = thm
1.14 | thm r = raise ERROR ("Rule.thm: uncovered case " ^ to_string r)
1.15
1.16 +
1.17 +(* ML antiquotations *)
1.18 +
1.19 +val make_eval = curry Eval;
1.20 +
1.21 +val _ = Theory.setup
1.22 + (ML_Antiquotation.value_embedded \<^binding>\<open>rule_eval\<close>
1.23 + (Args.const {proper = true, strict = true} >>
1.24 + (fn name => "Rule.make_eval " ^ ML_Syntax.print_string name)));
1.25 +
1.26 (**)end(**)
2.1 --- a/src/Tools/isac/Knowledge/AlgEin.thy Thu Jun 10 17:06:32 2021 +0200
2.2 +++ b/src/Tools/isac/Knowledge/AlgEin.thy Fri Jun 11 11:49:34 2021 +0200
2.3 @@ -73,7 +73,7 @@
2.4 ("#Find" ,["GesamtLaenge l_l"])],
2.5 {rew_ord'="tless_true", rls'= Rule_Set.empty, calc = [],
2.6 srls = Rule_Set.append_rules "srls_..Berechnung-erstSymbolisch" Rule_Set.empty
2.7 - [Rule.Eval ("Prog_Expr.boollist2sum", Prog_Expr.eval_boollist2sum "")],
2.8 + [\<^rule_eval>\<open>Prog_Expr.boollist2sum\<close> (Prog_Expr.eval_boollist2sum "")],
2.9 prls = Rule_Set.empty, crls =Rule_Set.empty , errpats = [], nrls = norm_Rational},
2.10 @{thm symbolisch_rechnen.simps})]
2.11 \<close>
2.12 @@ -106,7 +106,7 @@
2.13 ("#Find" ,["GesamtLaenge l_l"])],
2.14 {rew_ord'="tless_true", rls'= Rule_Set.empty, calc = [],
2.15 srls = Rule_Set.append_rules "srls_..Berechnung-erstSymbolisch" Rule_Set.empty
2.16 - [Rule.Eval ("Prog_Expr.boollist2sum", Prog_Expr.eval_boollist2sum "")],
2.17 + [\<^rule_eval>\<open>Prog_Expr.boollist2sum\<close> (Prog_Expr.eval_boollist2sum "")],
2.18 prls = Rule_Set.empty, crls =Rule_Set.empty , errpats = [], nrls = norm_Rational},
2.19 @{thm symbolisch_rechnen.simps})]
2.20 \<close> ML \<open>
3.1 --- a/src/Tools/isac/Knowledge/Base_Tools.thy Thu Jun 10 17:06:32 2021 +0200
3.2 +++ b/src/Tools/isac/Knowledge/Base_Tools.thy Fri Jun 11 11:49:34 2021 +0200
3.3 @@ -63,7 +63,7 @@
3.4 ML \<open>
3.5 \<close> ML \<open>
3.6 val Atools_erls = Rule_Set.append_rules "Atools_erls" Rule_Set.empty
3.7 - [ Rule.Eval ("HOL.eq", Prog_Expr.eval_equal "#equal_"),
3.8 + [ \<^rule_eval>\<open>HOL.eq\<close> (Prog_Expr.eval_equal "#equal_"),
3.9 Rule.Thm ("not_true", ThmC.numerals_to_Free @{thm not_true}),
3.10 (*"(~ True) = False"*)
3.11 Rule.Thm ("not_false", ThmC.numerals_to_Free @{thm not_false}),
3.12 @@ -84,18 +84,18 @@
3.13 Rule.Thm ("order_refl", ThmC.numerals_to_Free @{thm order_refl}),
3.14 Rule.Thm ("radd_left_cancel_le", ThmC.numerals_to_Free @{thm radd_left_cancel_le}),
3.15
3.16 - Rule.Eval ("Orderings.ord_class.less", Prog_Expr.eval_equ "#less_"),
3.17 - Rule.Eval ("Orderings.ord_class.less_eq", Prog_Expr.eval_equ "#less_equal_"),
3.18 + \<^rule_eval>\<open>less\<close> (Prog_Expr.eval_equ "#less_"),
3.19 + \<^rule_eval>\<open>less_eq\<close> (Prog_Expr.eval_equ "#less_equal_"),
3.20
3.21 - Rule.Eval ("Prog_Expr.ident", Prog_Expr.eval_ident "#ident_"),
3.22 - Rule.Eval ("Prog_Expr.is_const", Prog_Expr.eval_const "#is_const_"),
3.23 - Rule.Eval ("Prog_Expr.occurs_in", Prog_Expr.eval_occurs_in ""),
3.24 - Rule.Eval ("Prog_Expr.matches", Prog_Expr.eval_matches "")];
3.25 + \<^rule_eval>\<open>Prog_Expr.ident\<close> (Prog_Expr.eval_ident "#ident_"),
3.26 + \<^rule_eval>\<open>Prog_Expr.is_const\<close> (Prog_Expr.eval_const "#is_const_"),
3.27 + \<^rule_eval>\<open>Prog_Expr.occurs_in\<close> (Prog_Expr.eval_occurs_in ""),
3.28 + \<^rule_eval>\<open>Prog_Expr.matches\<close> (Prog_Expr.eval_matches "")];
3.29 \<close>
3.30
3.31 ML \<open>
3.32 val Atools_crls = Rule_Set.append_rules "Atools_crls" Rule_Set.empty
3.33 - [ Rule.Eval ("HOL.eq", Prog_Expr.eval_equal "#equal_"),
3.34 + [ \<^rule_eval>\<open>HOL.eq\<close> (Prog_Expr.eval_equal "#equal_"),
3.35 Rule.Thm ("not_true", ThmC.numerals_to_Free @{thm not_true}),
3.36 Rule.Thm ("not_false", ThmC.numerals_to_Free @{thm not_false}),
3.37 Rule.Thm ("and_true", ThmC.numerals_to_Free @{thm and_true}),
3.38 @@ -110,27 +110,27 @@
3.39 Rule.Thm ("order_refl", ThmC.numerals_to_Free @{thm order_refl}),
3.40 Rule.Thm ("radd_left_cancel_le", ThmC.numerals_to_Free @{thm radd_left_cancel_le}),
3.41
3.42 - Rule.Eval ("Orderings.ord_class.less", Prog_Expr.eval_equ "#less_"),
3.43 - Rule.Eval ("Orderings.ord_class.less_eq", Prog_Expr.eval_equ "#less_equal_"),
3.44 + \<^rule_eval>\<open>less\<close> (Prog_Expr.eval_equ "#less_"),
3.45 + \<^rule_eval>\<open>less_eq\<close> (Prog_Expr.eval_equ "#less_equal_"),
3.46
3.47 - Rule.Eval ("Prog_Expr.ident", Prog_Expr.eval_ident "#ident_"),
3.48 - Rule.Eval ("Prog_Expr.is_const", Prog_Expr.eval_const "#is_const_"),
3.49 - Rule.Eval ("Prog_Expr.occurs_in", Prog_Expr.eval_occurs_in ""),
3.50 - Rule.Eval ("Prog_Expr.matches", Prog_Expr.eval_matches "")];
3.51 + \<^rule_eval>\<open>Prog_Expr.ident\<close> (Prog_Expr.eval_ident "#ident_"),
3.52 + \<^rule_eval>\<open>Prog_Expr.is_const\<close> (Prog_Expr.eval_const "#is_const_"),
3.53 + \<^rule_eval>\<open>Prog_Expr.occurs_in\<close> (Prog_Expr.eval_occurs_in ""),
3.54 + \<^rule_eval>\<open>Prog_Expr.matches\<close> (Prog_Expr.eval_matches "")];
3.55 \<close>
3.56
3.57 subsection \<open>ONCE AGAIN extend rule-set for evaluating pre-conditions and program-expressions\<close>
3.58 text \<open>requires "eval_binop" from above\<close>
3.59 ML \<open>
3.60 val prog_expr = Rule_Set.append_rules "prog_expr" prog_expr
3.61 - [ Rule.Eval ("Groups.times_class.times", (**)eval_binop "#mult_"),
3.62 - Rule.Eval ("Groups.plus_class.plus", (**)eval_binop "#add_"),
3.63 - Rule.Eval ("Orderings.ord_class.less", Prog_Expr.eval_equ "#less_"),
3.64 - Rule.Eval ("Orderings.ord_class.less_eq", Prog_Expr.eval_equ "#less_equal_"),
3.65 - Rule.Eval ("Prog_Expr.ident", Prog_Expr.eval_ident "#ident_"),
3.66 - Rule.Eval ("HOL.eq", Prog_Expr.eval_equal "#equal_"),(*atom <> atom -> False*)
3.67 + [ \<^rule_eval>\<open>times\<close> (**)(eval_binop "#mult_"),
3.68 + \<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_"),
3.69 + \<^rule_eval>\<open>less\<close> (Prog_Expr.eval_equ "#less_"),
3.70 + \<^rule_eval>\<open>less_eq\<close> (Prog_Expr.eval_equ "#less_equal_"),
3.71 + \<^rule_eval>\<open>Prog_Expr.ident\<close> (Prog_Expr.eval_ident "#ident_"),
3.72 + \<^rule_eval>\<open>HOL.eq\<close> (Prog_Expr.eval_equal "#equal_"),(*atom <> atom -> False*)
3.73
3.74 - Rule.Eval ("Prog_Expr.Vars",Prog_Expr.eval_var "#Vars_"),
3.75 + \<^rule_eval>\<open>Prog_Expr.Vars\<close> (Prog_Expr.eval_var "#Vars_"),
3.76
3.77 Rule.Thm ("if_True",ThmC.numerals_to_Free @{thm if_True}),
3.78 Rule.Thm ("if_False",ThmC.numerals_to_Free @{thm if_False})];
3.79 @@ -139,8 +139,8 @@
3.80 (Rule_Def.Repeat {id = "replaced", preconds = [], rew_ord = ("termlessI", termlessI),
3.81 erls = Rule_Def.Repeat {id = "list_elrs", preconds = [], rew_ord = ("termlessI", termlessI),
3.82 erls = Rule_Set.empty, srls = Rule_Set.Empty, calc = [], errpatts = [],
3.83 - rules = [Rule.Eval ("Groups.plus_class.plus", (**)eval_binop "#add_"),
3.84 - Rule.Eval ("Orderings.ord_class.less", Prog_Expr.eval_equ "#less_")
3.85 + rules = [\<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_"),
3.86 + \<^rule_eval>\<open>less\<close> (Prog_Expr.eval_equ "#less_")
3.87 (* ~~~~~~ for nth_Cons_*)],
3.88 scr = Rule.Empty_Prog},
3.89 srls = Rule_Set.Empty, calc = [], errpatts = [],
4.1 --- a/src/Tools/isac/Knowledge/Biegelinie.thy Thu Jun 10 17:06:32 2021 +0200
4.2 +++ b/src/Tools/isac/Knowledge/Biegelinie.thy Fri Jun 11 11:49:34 2021 +0200
4.3 @@ -150,17 +150,17 @@
4.4 rew_ord = ("termlessI",termlessI),
4.5 erls = Rule_Set.append_rules "erls_in_srls_IntegrierenUnd.." Rule_Set.empty
4.6 [(*for asm in NTH_CONS ...*)
4.7 - Rule.Eval ("Orderings.ord_class.less", Prog_Expr.eval_equ "#less_"),
4.8 + \<^rule_eval>\<open>less\<close> (Prog_Expr.eval_equ "#less_"),
4.9 (*2nd NTH_CONS pushes n+-1 into asms*)
4.10 - Rule.Eval("Groups.plus_class.plus", (**)eval_binop "#add_")
4.11 + \<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_")
4.12 ],
4.13 srls = Rule_Set.Empty, calc = [], errpatts = [],
4.14 rules = [Rule.Thm ("NTH_CONS",ThmC.numerals_to_Free @{thm NTH_CONS}),
4.15 - Rule.Eval("Groups.plus_class.plus", (**)eval_binop "#add_"),
4.16 + \<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_"),
4.17 Rule.Thm ("NTH_NIL",ThmC.numerals_to_Free @{thm NTH_NIL}),
4.18 - Rule.Eval("Prog_Expr.lhs", Prog_Expr.eval_lhs"eval_lhs_"),
4.19 - Rule.Eval("Prog_Expr.rhs", Prog_Expr.eval_rhs"eval_rhs_"),
4.20 - Rule.Eval("Prog_Expr.argument_in", Prog_Expr.eval_argument_in "Prog_Expr.argument_in")
4.21 + \<^rule_eval>\<open>Prog_Expr.lhs\<close> (Prog_Expr.eval_lhs"eval_lhs_"),
4.22 + \<^rule_eval>\<open>Prog_Expr.rhs\<close> (Prog_Expr.eval_rhs"eval_rhs_"),
4.23 + \<^rule_eval>\<open>Prog_Expr.argument_in\<close> (Prog_Expr.eval_argument_in "Prog_Expr.argument_in")
4.24 ],
4.25 scr = Rule.Empty_Prog};
4.26
4.27 @@ -170,18 +170,18 @@
4.28 rew_ord = ("termlessI",termlessI),
4.29 erls = Rule_Set.append_rules "erls_in_srls_IntegrierenUnd.." Rule_Set.empty
4.30 [(*for asm in NTH_CONS ...*)
4.31 - Rule.Eval ("Orderings.ord_class.less", Prog_Expr.eval_equ "#less_"),
4.32 + \<^rule_eval>\<open>less\<close> (Prog_Expr.eval_equ "#less_"),
4.33 (*2nd NTH_CONS pushes n+-1 into asms*)
4.34 - Rule.Eval("Groups.plus_class.plus", (**)eval_binop "#add_")
4.35 + \<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_")
4.36 ],
4.37 srls = Rule_Set.Empty, calc = [], errpatts = [],
4.38 rules = [Rule.Thm ("NTH_CONS",ThmC.numerals_to_Free @{thm NTH_CONS}),
4.39 - Rule.Eval("Groups.plus_class.plus", (**)eval_binop "#add_"),
4.40 + \<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_"),
4.41 Rule.Thm ("NTH_NIL", ThmC.numerals_to_Free @{thm NTH_NIL}),
4.42 - Rule.Eval("Prog_Expr.lhs", Prog_Expr.eval_lhs "eval_lhs_"),
4.43 - Rule.Eval("Prog_Expr.filter_sameFunId", Prog_Expr.eval_filter_sameFunId "Prog_Expr.filter_sameFunId"),
4.44 + \<^rule_eval>\<open>Prog_Expr.lhs\<close> (Prog_Expr.eval_lhs "eval_lhs_"),
4.45 + \<^rule_eval>\<open>Prog_Expr.filter_sameFunId\<close> (Prog_Expr.eval_filter_sameFunId "Prog_Expr.filter_sameFunId"),
4.46 (*WN070514 just for smltest/../biegelinie.sml ...*)
4.47 - Rule.Eval("Prog_Expr.sameFunId", Prog_Expr.eval_sameFunId "Prog_Expr.sameFunId"),
4.48 + \<^rule_eval>\<open>Prog_Expr.sameFunId\<close> (Prog_Expr.eval_sameFunId "Prog_Expr.sameFunId"),
4.49 Rule.Thm ("filter_Cons", ThmC.numerals_to_Free @{thm filter_Cons}),
4.50 Rule.Thm ("filter_Nil", ThmC.numerals_to_Free @{thm filter_Nil}),
4.51 Rule.Thm ("if_True", ThmC.numerals_to_Free @{thm if_True}),
4.52 @@ -259,13 +259,13 @@
4.53 ("#Relate",["Randbedingungen side_conds"])],
4.54 {rew_ord'="tless_true",
4.55 rls' = Rule_Set.append_rules "erls_IntegrierenUndK.." Rule_Set.empty
4.56 - [Rule.Eval ("Prog_Expr.ident", Prog_Expr.eval_ident "#ident_"),
4.57 + [\<^rule_eval>\<open>Prog_Expr.ident\<close> (Prog_Expr.eval_ident "#ident_"),
4.58 Rule.Thm ("not_true",ThmC.numerals_to_Free @{thm not_true}),
4.59 Rule.Thm ("not_false",ThmC.numerals_to_Free @{thm not_false})],
4.60 calc = [],
4.61 srls = Rule_Set.append_rules "erls_IntegrierenUndK.." Rule_Set.empty
4.62 - [Rule.Eval("Prog_Expr.rhs", Prog_Expr.eval_rhs"eval_rhs_"),
4.63 - Rule.Eval ("Prog_Expr.ident", Prog_Expr.eval_ident "#ident_"),
4.64 + [\<^rule_eval>\<open>Prog_Expr.rhs\<close> (Prog_Expr.eval_rhs"eval_rhs_"),
4.65 + \<^rule_eval>\<open>Prog_Expr.ident\<close> (Prog_Expr.eval_ident "#ident_"),
4.66 Rule.Thm ("last_thmI",ThmC.numerals_to_Free @{thm last_thmI}),
4.67 Rule.Thm ("if_True",ThmC.numerals_to_Free @{thm if_True}),
4.68 Rule.Thm ("if_False",ThmC.numerals_to_Free @{thm if_False})],
4.69 @@ -327,13 +327,13 @@
4.70 "Biegelinie id_fun", "AbleitungBiegelinie id_der"]),
4.71 ("#Find" ,["Funktionen fun_s"])],
4.72 {rew_ord'="tless_true",
4.73 - rls' = Rule_Set.append_rules "erls_ausBelastung" Rule_Set.empty
4.74 - [Rule.Eval ("Prog_Expr.ident", Prog_Expr.eval_ident "#ident_"),
4.75 + rls' = Rule_Set.append_rules "erls_ausBelastung" Rule_Set.empty
4.76 + [\<^rule_eval>\<open>Prog_Expr.ident\<close> (Prog_Expr.eval_ident "#ident_"),
4.77 Rule.Thm ("not_true", ThmC.numerals_to_Free @{thm not_true}),
4.78 - Rule.Thm ("not_false", ThmC.numerals_to_Free @{thm not_false})],
4.79 + Rule.Thm ("not_false", ThmC.numerals_to_Free @{thm not_false})],
4.80 calc = [],
4.81 - srls = Rule_Set.append_rules "srls_ausBelastung" Rule_Set.empty
4.82 - [Rule.Eval ("Prog_Expr.rhs", Prog_Expr.eval_rhs "eval_rhs_")],
4.83 + srls = Rule_Set.append_rules "srls_ausBelastung" Rule_Set.empty
4.84 + [\<^rule_eval>\<open>Prog_Expr.rhs\<close> (Prog_Expr.eval_rhs "eval_rhs_")],
4.85 prls = Rule_Set.empty, crls = Atools_erls, errpats = [], nrls = Rule_Set.empty},
4.86 @{thm belastung_zu_biegelinie.simps})]
4.87 \<close>
4.88 @@ -392,8 +392,8 @@
4.89 ("#Find" ,["equality equ'''"])],
4.90 {rew_ord'="tless_true", rls'=Rule_Set.Empty, calc = [],
4.91 srls = Rule_Set.append_rules "srls_in_EquationfromFunc" Rule_Set.empty
4.92 - [Rule.Eval("Prog_Expr.lhs", Prog_Expr.eval_lhs "eval_lhs_"),
4.93 - Rule.Eval("Prog_Expr.argument_in", Prog_Expr.eval_argument_in "Prog_Expr.argument_in")],
4.94 + [\<^rule_eval>\<open>Prog_Expr.lhs\<close> (Prog_Expr.eval_lhs "eval_lhs_"),
4.95 + \<^rule_eval>\<open>Prog_Expr.argument_in\<close> (Prog_Expr.eval_argument_in "Prog_Expr.argument_in")],
4.96 prls=Rule_Set.empty, crls = Atools_erls, errpats = [], nrls = Rule_Set.empty},
4.97 (*(M_b x = c_2 + c * x + -1 * q_0 / 2 * x \<up> 2) (M_b L = 0) -->
4.98 0 = c_2 + c * L + -1 * q_0 / 2 * L \<up> 2*)
5.1 --- a/src/Tools/isac/Knowledge/Diff.thy Thu Jun 10 17:06:32 2021 +0200
5.2 +++ b/src/Tools/isac/Knowledge/Diff.thy Fri Jun 11 11:49:34 2021 +0200
5.3 @@ -110,10 +110,10 @@
5.4 preconds = [],
5.5 rew_ord = ("termlessI",termlessI),
5.6 erls = Rule_Set.append_rules "erls_diff_conv" Rule_Set.empty
5.7 - [Rule.Eval ("Prog_Expr.occurs_in", Prog_Expr.eval_occurs_in ""),
5.8 + [\<^rule_eval>\<open>Prog_Expr.occurs_in\<close> (Prog_Expr.eval_occurs_in ""),
5.9 Rule.Thm ("not_true",ThmC.numerals_to_Free @{thm not_true}),
5.10 Rule.Thm ("not_false",ThmC.numerals_to_Free @{thm not_false}),
5.11 - Rule.Eval ("Orderings.ord_class.less", Prog_Expr.eval_equ "#less_"),
5.12 + \<^rule_eval>\<open>less\<close> (Prog_Expr.eval_equ "#less_"),
5.13 Rule.Thm ("and_true",ThmC.numerals_to_Free @{thm and_true}),
5.14 Rule.Thm ("and_false",ThmC.numerals_to_Free @{thm and_false})
5.15 ],
5.16 @@ -131,7 +131,7 @@
5.17 (*"?bdv occurs_in ?u \<Longrightarrow> nroot ?n ?u = ?u \<up> (1 / ?n)"*)
5.18 Rule.Thm ("realpow_pow_bdv", ThmC.numerals_to_Free @{thm realpow_pow_bdv}),
5.19 (* "(?bdv \<up> ?b) \<up> ?c = ?bdv \<up> (?b * ?c)"*)
5.20 - Rule.Eval ("Groups.times_class.times", (**)eval_binop "#mult_"),
5.21 + \<^rule_eval>\<open>times\<close> (**)(eval_binop "#mult_"),
5.22 Rule.Thm ("rat_mult",ThmC.numerals_to_Free @{thm rat_mult}),
5.23 (*a / b * (c / d) = a * c / (b * d)*)
5.24 Rule.Thm ("times_divide_eq_right",ThmC.numerals_to_Free @{thm times_divide_eq_right}),
5.25 @@ -148,8 +148,7 @@
5.26 preconds = [],
5.27 rew_ord = ("termlessI",termlessI),
5.28 erls = Rule_Set.append_rules "erls_diff_sym_conv" Rule_Set.empty
5.29 - [Rule.Eval ("Orderings.ord_class.less", Prog_Expr.eval_equ "#less_")
5.30 - ],
5.31 + [\<^rule_eval>\<open>less\<close> (Prog_Expr.eval_equ "#less_")],
5.32 srls = Rule_Set.Empty, calc = [], errpatts = [],
5.33 rules = [Rule.Thm ("frac_sym_conv", ThmC.numerals_to_Free @{thm frac_sym_conv}),
5.34 Rule.Thm ("sqrt_sym_conv", ThmC.numerals_to_Free @{thm sqrt_sym_conv}),
5.35 @@ -163,7 +162,7 @@
5.36 (*?x * (?y / ?z) = ?x * ?y / ?z*)
5.37 Rule.Thm ("times_divide_eq_left",ThmC.numerals_to_Free @{thm times_divide_eq_left}),
5.38 (*?y / ?z * ?x = ?y * ?x / ?z*)
5.39 - Rule.Eval ("Groups.times_class.times", (**)eval_binop "#mult_")
5.40 + \<^rule_eval>\<open>times\<close> (**)(eval_binop "#mult_")
5.41 ],
5.42 scr = Rule.Empty_Prog};
5.43
5.44 @@ -174,9 +173,9 @@
5.45 rew_ord = ("termlessI",termlessI),
5.46 erls = Rule_Set.empty,
5.47 srls = Rule_Set.Empty, calc = [], errpatts = [],
5.48 - rules = [Rule.Eval("Prog_Expr.lhs", Prog_Expr.eval_lhs "eval_lhs_"),
5.49 - Rule.Eval("Prog_Expr.rhs", Prog_Expr.eval_rhs "eval_rhs_"),
5.50 - Rule.Eval("Diff.primed", eval_primed "Diff.primed")
5.51 + rules = [\<^rule_eval>\<open>Prog_Expr.lhs\<close> (Prog_Expr.eval_lhs "eval_lhs_"),
5.52 + \<^rule_eval>\<open>Prog_Expr.rhs\<close> (Prog_Expr.eval_rhs "eval_rhs_"),
5.53 + \<^rule_eval>\<open>Diff.primed\<close> (eval_primed "Diff.primed")
5.54 ],
5.55 scr = Rule.Empty_Prog};
5.56 \<close>
5.57 @@ -187,10 +186,10 @@
5.58 [Rule.Thm ("not_true",ThmC.numerals_to_Free @{thm not_true}),
5.59 Rule.Thm ("not_false",ThmC.numerals_to_Free @{thm not_false}),
5.60
5.61 - Rule.Eval ("Prog_Expr.ident", Prog_Expr.eval_ident "#ident_"),
5.62 - Rule.Eval ("Prog_Expr.is_atom", Prog_Expr.eval_is_atom "#is_atom_"),
5.63 - Rule.Eval ("Prog_Expr.occurs_in", Prog_Expr.eval_occurs_in ""),
5.64 - Rule.Eval ("Prog_Expr.is_const", Prog_Expr.eval_const "#is_const_")
5.65 + \<^rule_eval>\<open>Prog_Expr.ident\<close> (Prog_Expr.eval_ident "#ident_"),
5.66 + \<^rule_eval>\<open>Prog_Expr.is_atom\<close> (Prog_Expr.eval_is_atom "#is_atom_"),
5.67 + \<^rule_eval>\<open>Prog_Expr.occurs_in\<close> (Prog_Expr.eval_occurs_in ""),
5.68 + \<^rule_eval>\<open>Prog_Expr.is_const\<close> (Prog_Expr.eval_const "#is_const_")
5.69 ];
5.70
5.71 (*.rules for differentiation, _no_ simplification.*)
6.1 --- a/src/Tools/isac/Knowledge/DiffApp.thy Thu Jun 10 17:06:32 2021 +0200
6.2 +++ b/src/Tools/isac/Knowledge/DiffApp.thy Fri Jun 11 11:49:34 2021 +0200
6.3 @@ -47,13 +47,13 @@
6.4 Rule.Thm ("and_commute", ThmC.numerals_to_Free @{thm and_commute}),
6.5 Rule.Thm ("or_commute", ThmC.numerals_to_Free @{thm or_commute}),
6.6
6.7 - Rule.Eval ("Orderings.ord_class.less", Prog_Expr.eval_equ "#less_"),
6.8 - Rule.Eval ("Orderings.ord_class.less_eq", Prog_Expr.eval_equ "#less_equal_"),
6.9 + \<^rule_eval>\<open>less\<close> (Prog_Expr.eval_equ "#less_"),
6.10 + \<^rule_eval>\<open>less_eq\<close> (Prog_Expr.eval_equ "#less_equal_"),
6.11
6.12 - Rule.Eval ("Prog_Expr.ident", Prog_Expr.eval_ident "#ident_"),
6.13 - Rule.Eval ("Prog_Expr.is_const", Prog_Expr.eval_const "#is_const_"),
6.14 - Rule.Eval ("Prog_Expr.occurs_in", Prog_Expr.eval_occurs_in ""),
6.15 - Rule.Eval ("Prog_Expr.matches", Prog_Expr.eval_matches "")],
6.16 + \<^rule_eval>\<open>Prog_Expr.ident\<close> (Prog_Expr.eval_ident "#ident_"),
6.17 + \<^rule_eval>\<open>Prog_Expr.is_const\<close> (Prog_Expr.eval_const "#is_const_"),
6.18 + \<^rule_eval>\<open>Prog_Expr.occurs_in\<close> (Prog_Expr.eval_occurs_in ""),
6.19 + \<^rule_eval>\<open>Prog_Expr.matches\<close> (Prog_Expr.eval_matches "")],
6.20 scr = Rule.Empty_Prog
6.21 });
6.22 \<close>
7.1 --- a/src/Tools/isac/Knowledge/EqSystem.thy Thu Jun 10 17:06:32 2021 +0200
7.2 +++ b/src/Tools/isac/Knowledge/EqSystem.thy Fri Jun 11 11:49:34 2021 +0200
7.3 @@ -257,7 +257,7 @@
7.4 (*Rule.Rls_ discard_parentheses *3**),
7.5 Rule.Rls_ collect_bdv, (*from make_polynomial_in WN051031 welldone?*)
7.6 Rule.Rls_ separate_bdv2,
7.7 - Rule.Eval ("Rings.divide_class.divide", Prog_Expr.eval_cancel "#divide_e")
7.8 + \<^rule_eval>\<open>divide\<close> (Prog_Expr.eval_cancel "#divide_e")
7.9 ],
7.10 scr = Rule.Empty_Prog};
7.11 \<close>
7.12 @@ -275,7 +275,7 @@
7.13 Rule.Rls_ discard_parentheses,
7.14 Rule.Rls_ collect_bdv, (*from make_polynomial_in WN051031 welldone?*)
7.15 Rule.Rls_ separate_bdv2,
7.16 - Rule.Eval ("Rings.divide_class.divide", Prog_Expr.eval_cancel "#divide_e")
7.17 + \<^rule_eval>\<open>divide\<close> (Prog_Expr.eval_cancel "#divide_e")
7.18 ],
7.19 scr = Rule.Empty_Prog};
7.20 (*
7.21 @@ -290,10 +290,7 @@
7.22 Rule_Def.Repeat {id="isolate_bdvs", preconds = [],
7.23 rew_ord = ("e_rew_ord", Rewrite_Ord.e_rew_ord),
7.24 erls = Rule_Set.append_rules "erls_isolate_bdvs" Rule_Set.empty
7.25 - [(Rule.Eval ("EqSystem.occur_exactly_in",
7.26 - eval_occur_exactly_in
7.27 - "#eval_occur_exactly_in_"))
7.28 - ],
7.29 + [(\<^rule_eval>\<open>occur_exactly_in\<close> (eval_occur_exactly_in "#eval_occur_exactly_in_"))],
7.30 srls = Rule_Set.Empty, calc = [], errpatts = [],
7.31 rules =
7.32 [Rule.Thm ("commute_0_equality", ThmC.numerals_to_Free @{thm commute_0_equality}),
7.33 @@ -307,10 +304,9 @@
7.34 rew_ord = ("e_rew_ord", Rewrite_Ord.e_rew_ord),
7.35 erls = Rule_Set.append_rules
7.36 "erls_isolate_bdvs_4x4" Rule_Set.empty
7.37 - [Rule.Eval ("EqSystem.occur_exactly_in",
7.38 - eval_occur_exactly_in "#eval_occur_exactly_in_"),
7.39 - Rule.Eval ("Prog_Expr.ident", Prog_Expr.eval_ident "#ident_"),
7.40 - Rule.Eval ("Prog_Expr.some_occur_in", Prog_Expr.eval_some_occur_in "#some_occur_in_"),
7.41 + [\<^rule_eval>\<open>occur_exactly_in\<close> (eval_occur_exactly_in "#eval_occur_exactly_in_"),
7.42 + \<^rule_eval>\<open>Prog_Expr.ident\<close> (Prog_Expr.eval_ident "#ident_"),
7.43 + \<^rule_eval>\<open>Prog_Expr.some_occur_in\<close> (Prog_Expr.eval_some_occur_in "#some_occur_in_"),
7.44 Rule.Thm ("not_true",ThmC.numerals_to_Free @{thm not_true}),
7.45 Rule.Thm ("not_false",ThmC.numerals_to_Free @{thm not_false})
7.46 ],
7.47 @@ -343,21 +339,19 @@
7.48 rew_ord = ("e_rew_ord", Rewrite_Ord.e_rew_ord),
7.49 erls = Rule_Set.Empty, srls = Rule_Set.Empty, calc = [], errpatts = [],
7.50 rules = [(*for precond NTH_CONS ...*)
7.51 - Rule.Eval ("Orderings.ord_class.less", Prog_Expr.eval_equ "#less_"),
7.52 - Rule.Eval ("Groups.plus_class.plus", (**)eval_binop "#add_")
7.53 + \<^rule_eval>\<open>less\<close> (Prog_Expr.eval_equ "#less_"),
7.54 + \<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_")
7.55 (*immediately repeated rewrite pushes
7.56 '+' into precondition !*)
7.57 ],
7.58 scr = Rule.Empty_Prog},
7.59 srls = Rule_Set.Empty, calc = [], errpatts = [],
7.60 rules = [Rule.Thm ("NTH_CONS",ThmC.numerals_to_Free @{thm NTH_CONS}),
7.61 - Rule.Eval ("Groups.plus_class.plus", (**)eval_binop "#add_"),
7.62 + \<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_"),
7.63 Rule.Thm ("NTH_NIL",ThmC.numerals_to_Free @{thm NTH_NIL}),
7.64 Rule.Thm ("tl_Cons",ThmC.numerals_to_Free @{thm tl_Cons}),
7.65 Rule.Thm ("tl_Nil",ThmC.numerals_to_Free @{thm tl_Nil}),
7.66 - Rule.Eval ("EqSystem.occur_exactly_in",
7.67 - eval_occur_exactly_in
7.68 - "#eval_occur_exactly_in_")
7.69 + \<^rule_eval>\<open>occur_exactly_in\<close> (eval_occur_exactly_in "#eval_occur_exactly_in_")
7.70 ],
7.71 scr = Rule.Empty_Prog};
7.72 \<close>
7.73 @@ -372,21 +366,19 @@
7.74 rew_ord = ("e_rew_ord", Rewrite_Ord.e_rew_ord),
7.75 erls = Rule_Set.Empty, srls = Rule_Set.Empty, calc = [], errpatts = [],
7.76 rules = [(*for precond NTH_CONS ...*)
7.77 - Rule.Eval ("Orderings.ord_class.less", Prog_Expr.eval_equ "#less_"),
7.78 - Rule.Eval ("Groups.plus_class.plus", (**)eval_binop "#add_")
7.79 + \<^rule_eval>\<open>less\<close> (Prog_Expr.eval_equ "#less_"),
7.80 + \<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_")
7.81 (*immediately repeated rewrite pushes
7.82 '+' into precondition !*)
7.83 ],
7.84 scr = Rule.Empty_Prog},
7.85 srls = Rule_Set.Empty, calc = [], errpatts = [],
7.86 rules = [Rule.Thm ("NTH_CONS",ThmC.numerals_to_Free @{thm NTH_CONS}),
7.87 - Rule.Eval ("Groups.plus_class.plus", (**)eval_binop "#add_"),
7.88 + \<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_"),
7.89 Rule.Thm ("NTH_NIL",ThmC.numerals_to_Free @{thm NTH_NIL}),
7.90 Rule.Thm ("tl_Cons",ThmC.numerals_to_Free @{thm tl_Cons}),
7.91 Rule.Thm ("tl_Nil",ThmC.numerals_to_Free @{thm tl_Nil}),
7.92 - Rule.Eval ("EqSystem.occur_exactly_in",
7.93 - eval_occur_exactly_in
7.94 - "#eval_occur_exactly_in_")
7.95 + \<^rule_eval>\<open>occur_exactly_in\<close> (eval_occur_exactly_in "#eval_occur_exactly_in_")
7.96 ],
7.97 scr = Rule.Empty_Prog};
7.98 \<close>
7.99 @@ -425,8 +417,8 @@
7.100 Rule_Set.append_rules "prls_2x2_linear_system" Rule_Set.empty
7.101 [Rule.Thm ("LENGTH_CONS",ThmC.numerals_to_Free @{thm LENGTH_CONS}),
7.102 Rule.Thm ("LENGTH_NIL",ThmC.numerals_to_Free @{thm LENGTH_NIL}),
7.103 - Rule.Eval ("Groups.plus_class.plus", (**)eval_binop "#add_"),
7.104 - Rule.Eval ("HOL.eq", Prog_Expr.eval_equal "#equal_")],
7.105 + \<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_"),
7.106 + \<^rule_eval>\<open>HOL.eq\<close> (Prog_Expr.eval_equal "#equal_")],
7.107 SOME "solveSystem e_s v_s", [])),
7.108 (Problem.prep_input @{theory} "pbl_equsys_lin_2x2_tri" [] Problem.id_empty
7.109 (["triangular", "2x2", "LINEAR", "system"],
7.110 @@ -452,8 +444,8 @@
7.111 Rule_Set.append_rules "prls_3x3_linear_system" Rule_Set.empty
7.112 [Rule.Thm ("LENGTH_CONS",ThmC.numerals_to_Free @{thm LENGTH_CONS}),
7.113 Rule.Thm ("LENGTH_NIL",ThmC.numerals_to_Free @{thm LENGTH_NIL}),
7.114 - Rule.Eval ("Groups.plus_class.plus", (**)eval_binop "#add_"),
7.115 - Rule.Eval ("HOL.eq", Prog_Expr.eval_equal "#equal_")],
7.116 + \<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_"),
7.117 + \<^rule_eval>\<open>HOL.eq\<close> (Prog_Expr.eval_equal "#equal_")],
7.118 SOME "solveSystem e_s v_s", [])),
7.119 (Problem.prep_input @{theory} "pbl_equsys_lin_4x4" [] Problem.id_empty
7.120 (["4x4", "LINEAR", "system"],
7.121 @@ -464,8 +456,8 @@
7.122 Rule_Set.append_rules "prls_4x4_linear_system" Rule_Set.empty
7.123 [Rule.Thm ("LENGTH_CONS",ThmC.numerals_to_Free @{thm LENGTH_CONS}),
7.124 Rule.Thm ("LENGTH_NIL",ThmC.numerals_to_Free @{thm LENGTH_NIL}),
7.125 - Rule.Eval ("Groups.plus_class.plus", (**)eval_binop "#add_"),
7.126 - Rule.Eval ("HOL.eq", Prog_Expr.eval_equal "#equal_")],
7.127 + \<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_"),
7.128 + \<^rule_eval>\<open>HOL.eq\<close> (Prog_Expr.eval_equal "#equal_")],
7.129 SOME "solveSystem e_s v_s", [])),
7.130 (Problem.prep_input @{theory} "pbl_equsys_lin_4x4_tri" [] Problem.id_empty
7.131 (["triangular", "4x4", "LINEAR", "system"],
7.132 @@ -477,7 +469,7 @@
7.133 "(NTH 4 (v_s::real list)) occurs_in (NTH 4 (e_s::bool list))"]),
7.134 ("#Find" ,["solution ss'''"])],
7.135 Rule_Set.append_rules "prls_tri_4x4_lin_sys" prls_triangular
7.136 - [Rule.Eval ("Prog_Expr.occurs_in", Prog_Expr.eval_occurs_in "")],
7.137 + [\<^rule_eval>\<open>Prog_Expr.occurs_in\<close> (Prog_Expr.eval_occurs_in "")],
7.138 SOME "solveSystem e_s v_s",
7.139 [["EqSystem", "top_down_substitution", "4x4"]])),
7.140 (Problem.prep_input @{theory} "pbl_equsys_lin_4x4_norm" [] Problem.id_empty
7.141 @@ -496,13 +488,13 @@
7.142 rew_ord = ("termlessI",termlessI),
7.143 erls = Rule_Set.append_rules "erls_in_srls_IntegrierenUnd.." Rule_Set.empty
7.144 [(*for asm in NTH_CONS ...*)
7.145 - Rule.Eval ("Orderings.ord_class.less", Prog_Expr.eval_equ "#less_"),
7.146 + \<^rule_eval>\<open>less\<close> (Prog_Expr.eval_equ "#less_"),
7.147 (*2nd NTH_CONS pushes n+-1 into asms*)
7.148 - Rule.Eval("Groups.plus_class.plus", (**)eval_binop "#add_")
7.149 + \<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_")
7.150 ],
7.151 srls = Rule_Set.Empty, calc = [], errpatts = [],
7.152 rules = [Rule.Thm ("NTH_CONS",ThmC.numerals_to_Free @{thm NTH_CONS}),
7.153 - Rule.Eval("Groups.plus_class.plus", (**)eval_binop "#add_"),
7.154 + \<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_"),
7.155 Rule.Thm ("NTH_NIL",ThmC.numerals_to_Free @{thm NTH_NIL})],
7.156 scr = Rule.Empty_Prog};
7.157 \<close>
7.158 @@ -656,7 +648,7 @@
7.159 {rew_ord'="ord_simplify_System", rls' = Rule_Set.Empty, calc = [],
7.160 srls = Rule_Set.append_rules "srls_top_down_4x4" srls [],
7.161 prls = Rule_Set.append_rules "prls_tri_4x4_lin_sys" prls_triangular
7.162 - [Rule.Eval ("Prog_Expr.occurs_in", Prog_Expr.eval_occurs_in "")],
7.163 + [\<^rule_eval>\<open>Prog_Expr.occurs_in\<close> (Prog_Expr.eval_occurs_in "")],
7.164 crls = Rule_Set.Empty, errpats = [], nrls = Rule_Set.Empty},
7.165 (*FIXXXXME.WN060916: this script works ONLY for exp 7.79 #>#>#>#>#>#>#>#>#>#>*)
7.166 @{thm solve_system4.simps})]
8.1 --- a/src/Tools/isac/Knowledge/Equation.thy Thu Jun 10 17:06:32 2021 +0200
8.2 +++ b/src/Tools/isac/Knowledge/Equation.thy Fri Jun 11 11:49:34 2021 +0200
8.3 @@ -35,7 +35,7 @@
8.4 ML \<open>
8.5 val univariate_equation_prls =
8.6 Rule_Set.append_rules "univariate_equation_prls" Rule_Set.empty
8.7 - [Rule.Eval ("Prog_Expr.matches", Prog_Expr.eval_matches "")];
8.8 + [\<^rule_eval>\<open>Prog_Expr.matches\<close> (Prog_Expr.eval_matches "")];
8.9 \<close>
8.10 rule_set_knowledge univariate_equation_prls = \<open>Auto_Prog.prep_rls @{theory} univariate_equation_prls\<close>
8.11 setup \<open>KEStore_Elems.add_pbts
8.12 @@ -44,7 +44,8 @@
8.13 [("#Given" ,["equality e_e", "solveFor v_v"]),
8.14 ("#Where" ,["matches (?a = ?b) e_e"]),
8.15 ("#Find" ,["solutions v_v'i'"])],
8.16 - Rule_Set.append_rules "equation_prls" Rule_Set.empty [Rule.Eval ("Prog_Expr.matches", Prog_Expr.eval_matches "")],
8.17 + Rule_Set.append_rules "equation_prls" Rule_Set.empty
8.18 + [\<^rule_eval>\<open>Prog_Expr.matches\<close> (Prog_Expr.eval_matches "")],
8.19 SOME "solve (e_e::bool, v_v)", [])),
8.20 (Problem.prep_input @{theory} "pbl_equ_univ" [] Problem.id_empty
8.21 (["univariate", "equation"],
9.1 --- a/src/Tools/isac/Knowledge/InsSort.thy Thu Jun 10 17:06:32 2021 +0200
9.2 +++ b/src/Tools/isac/Knowledge/InsSort.thy Fri Jun 11 11:49:34 2021 +0200
9.3 @@ -62,7 +62,7 @@
9.4 Rule.Thm ("o_apply", @{thm o_apply} (* (?f \<circ> ?g) ?x = ?f (?g ?x) *)),
9.5 Rule.Thm ("id_apply", @{thm id_apply} (* id ?x = ?x *)),
9.6
9.7 - Rule.Eval ("Orderings.ord_class.less", Prog_Expr.eval_equ "#less_"),
9.8 + \<^rule_eval>\<open>less\<close> (Prog_Expr.eval_equ "#less_"),
9.9 Rule.Thm ("If_def", @{thm If_def} (* if ?P then ?x else ?y \<equiv> THE z. (?P = True \<longrightarrow> z = ?x) \<and> (?P = False \<longrightarrow> z = ?y) *)),
9.10 Rule.Thm ("if_True", @{thm if_True} (* "(if True then x else y) = x" *)),
9.11 Rule.Thm ("if_False", @{thm if_False} (* "(if False then x else y) = y" *))],
10.1 --- a/src/Tools/isac/Knowledge/Integrate.thy Thu Jun 10 17:06:32 2021 +0200
10.2 +++ b/src/Tools/isac/Knowledge/Integrate.thy Fri Jun 11 11:49:34 2021 +0200
10.3 @@ -118,7 +118,7 @@
10.4 erls = Rule_Set.Empty,
10.5 srls = Rule_Set.Empty, calc = [], errpatts = [],
10.6 rules = [(*for rewriting conditions in Thm's*)
10.7 - Rule.Eval ("Prog_Expr.occurs_in", Prog_Expr.eval_occurs_in "#occurs_in_"),
10.8 + \<^rule_eval>\<open>Prog_Expr.occurs_in\<close> (Prog_Expr.eval_occurs_in "#occurs_in_"),
10.9 Rule.Thm ("not_true", ThmC.numerals_to_Free @{thm not_true}),
10.10 Rule.Thm ("not_false",@{thm not_false})
10.11 ],
10.12 @@ -130,7 +130,7 @@
10.13 Rule.Thm ("integral_add", ThmC.numerals_to_Free @{thm integral_add}),
10.14 Rule.Thm ("integral_mult", ThmC.numerals_to_Free @{thm integral_mult}),
10.15 Rule.Thm ("integral_pow", ThmC.numerals_to_Free @{thm integral_pow}),
10.16 - Rule.Eval ("Groups.plus_class.plus", (**)eval_binop "#add_")(*for n+1*)
10.17 + \<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_")(*for n+1*)
10.18 ],
10.19 scr = Rule.Empty_Prog};
10.20 \<close>
10.21 @@ -143,9 +143,8 @@
10.22 rew_ord = ("termlessI",termlessI),
10.23 erls = Rule_Set.Empty,
10.24 srls = Rule_Set.Empty, calc = [], errpatts = [],
10.25 - rules = [Rule.Eval ("Prog_Expr.matches", Prog_Expr.eval_matches""),
10.26 - Rule.Eval ("Integrate.is_f_x",
10.27 - eval_is_f_x "is_f_x_"),
10.28 + rules = [\<^rule_eval>\<open>Prog_Expr.matches\<close> (Prog_Expr.eval_matches""),
10.29 + \<^rule_eval>\<open>Integrate.is_f_x\<close> (eval_is_f_x "is_f_x_"),
10.30 Rule.Thm ("not_true", ThmC.numerals_to_Free @{thm not_true}),
10.31 Rule.Thm ("not_false", ThmC.numerals_to_Free @{thm not_false})
10.32 ],
10.33 @@ -171,8 +170,7 @@
10.34 rew_ord = ("dummy_ord",Rewrite_Ord.dummy_ord),
10.35 erls = (*FIXME.WN051028 Rule_Set.empty,*)
10.36 Rule_Set.append_rules "Rule_Set.empty-is_polyexp" Rule_Set.empty
10.37 - [Rule.Eval ("Poly.is_polyexp",
10.38 - eval_is_polyexp "")],
10.39 + [\<^rule_eval>\<open>is_polyexp\<close> (eval_is_polyexp "")],
10.40 srls = Rule_Set.Empty, calc = [], errpatts = [],
10.41 rules = [Rule.Thm ("rat_mult", ThmC.numerals_to_Free @{thm rat_mult}),
10.42 (*"?a / ?b * (?c / ?d) = ?a * ?c / (?b * ?d)"*)
10.43 @@ -190,7 +188,7 @@
10.44 Rule.Thm ("divide_divide_eq_left",
10.45 ThmC.numerals_to_Free @{thm divide_divide_eq_left}),
10.46 (*"?x / ?y / ?z = ?x / (?y * ?z)"*)
10.47 - Rule.Eval ("Rings.divide_class.divide", Prog_Expr.eval_cancel "#divide_e"),
10.48 + \<^rule_eval>\<open>divide\<close> (Prog_Expr.eval_cancel "#divide_e"),
10.49
10.50 Rule.Thm ("rat_power", ThmC.numerals_to_Free @{thm rat_power})
10.51 (*"(?a / ?b) \<up> ?n = ?a \<up> ?n / ?b \<up> ?n"*)
10.52 @@ -254,7 +252,7 @@
10.53 Rule.Rls_ discard_parentheses,
10.54 (*Rule.Rls_ collect_bdv, from make_polynomial_in*)
10.55 Rule.Rls_ separate_bdv2,
10.56 - Rule.Eval ("Rings.divide_class.divide", Prog_Expr.eval_cancel "#divide_e")
10.57 + \<^rule_eval>\<open>divide\<close> (Prog_Expr.eval_cancel "#divide_e")
10.58 ],
10.59 scr = Rule.Empty_Prog};
10.60
10.61 @@ -292,7 +290,7 @@
10.62 * ThmC.numerals_to_Free @{thm add_divide_distrib})
10.63 * (*"(?x + ?y) / ?z = ?x / ?z + ?y / ?z"*)*)
10.64 * ]),
10.65 -* Rule.Eval ("Rings.divide_class.divide" , eval_cancel "#divide_e")
10.66 +* \<^rule_eval>\<open>divide\<close> (eval_cancel "#divide_e")
10.67 * ],
10.68 * scr = Rule.Empty_Prog
10.69 * });
11.1 --- a/src/Tools/isac/Knowledge/Inverse_Z_Transform.thy Thu Jun 10 17:06:32 2021 +0200
11.2 +++ b/src/Tools/isac/Knowledge/Inverse_Z_Transform.thy Fri Jun 11 11:49:34 2021 +0200
11.3 @@ -122,20 +122,19 @@
11.4 preconds = [], rew_ord = ("termlessI",termlessI),
11.5 erls = Rule_Set.append_rules "erls_in_srls_partial_fraction" Rule_Set.empty
11.6 [(*for asm in NTH_CONS ...*)
11.7 - Rule.Eval ("Orderings.ord_class.less", Prog_Expr.eval_equ "#less_"),
11.8 + \<^rule_eval>\<open>less\<close> (Prog_Expr.eval_equ "#less_"),
11.9 (*2nd NTH_CONS pushes n+-1 into asms*)
11.10 - Rule.Eval("Groups.plus_class.plus", (**)eval_binop "#add_")],
11.11 + \<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_")],
11.12 srls = Rule_Set.Empty, calc = [], errpatts = [],
11.13 rules = [Rule.Thm ("NTH_CONS", @{thm NTH_CONS}),
11.14 - Rule.Eval ("Groups.plus_class.plus", (**)eval_binop "#add_"),
11.15 + \<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_"),
11.16 Rule.Thm ("NTH_NIL", @{thm NTH_NIL}),
11.17 - Rule.Eval ("Prog_Expr.lhs", Prog_Expr.eval_lhs "eval_lhs_"),
11.18 - Rule.Eval ("Prog_Expr.rhs", Prog_Expr.eval_rhs"eval_rhs_"),
11.19 - Rule.Eval ("Prog_Expr.argument_in", Prog_Expr.eval_argument_in "Prog_Expr.argument_in"),
11.20 - Rule.Eval ("Rational.get_denominator", eval_get_denominator "#get_denominator"),
11.21 - Rule.Eval ("Rational.get_numerator", eval_get_numerator "#get_numerator"),
11.22 - Rule.Eval ("Partial_Fractions.factors_from_solution",
11.23 - eval_factors_from_solution "#factors_from_solution")
11.24 + \<^rule_eval>\<open>Prog_Expr.lhs\<close> (Prog_Expr.eval_lhs "eval_lhs_"),
11.25 + \<^rule_eval>\<open>Prog_Expr.rhs\<close> (Prog_Expr.eval_rhs"eval_rhs_"),
11.26 + \<^rule_eval>\<open>Prog_Expr.argument_in\<close> (Prog_Expr.eval_argument_in "Prog_Expr.argument_in"),
11.27 + \<^rule_eval>\<open>get_denominator\<close> (eval_get_denominator "#get_denominator"),
11.28 + \<^rule_eval>\<open>get_numerator\<close> (eval_get_numerator "#get_numerator"),
11.29 + \<^rule_eval>\<open>factors_from_solution\<close> (eval_factors_from_solution "#factors_from_solution")
11.30 ], scr = Rule.Empty_Prog},
11.31 prls = Rule_Set.empty, crls = Rule_Set.empty, errpats = [], nrls = norm_Rational},
11.32 @{thm inverse_ztransform2.simps})]
12.1 --- a/src/Tools/isac/Knowledge/LinEq.thy Thu Jun 10 17:06:32 2021 +0200
12.2 +++ b/src/Tools/isac/Knowledge/LinEq.thy Fri Jun 11 11:49:34 2021 +0200
12.3 @@ -25,14 +25,14 @@
12.4 ML \<open>
12.5 val LinEq_prls = (*3.10.02:just the following order due to subterm evaluation*)
12.6 Rule_Set.append_rules "LinEq_prls" Rule_Set.empty
12.7 - [Rule.Eval ("HOL.eq", Prog_Expr.eval_equal "#equal_"),
12.8 - Rule.Eval ("Prog_Expr.matches", Prog_Expr.eval_matches ""),
12.9 - Rule.Eval ("Prog_Expr.lhs" , Prog_Expr.eval_lhs ""),
12.10 - Rule.Eval ("Prog_Expr.rhs" , Prog_Expr.eval_rhs ""),
12.11 - Rule.Eval ("Poly.has_degree_in", eval_has_degree_in ""),
12.12 - Rule.Eval ("Poly.is_polyrat_in", eval_is_polyrat_in ""),
12.13 - Rule.Eval ("Prog_Expr.occurs_in", Prog_Expr.eval_occurs_in ""),
12.14 - Rule.Eval ("Prog_Expr.ident", Prog_Expr.eval_ident "#ident_"),
12.15 + [\<^rule_eval>\<open>HOL.eq\<close> (Prog_Expr.eval_equal "#equal_"),
12.16 + \<^rule_eval>\<open>Prog_Expr.matches\<close> (Prog_Expr.eval_matches ""),
12.17 + \<^rule_eval>\<open>Prog_Expr.lhs\<close> (Prog_Expr.eval_lhs ""),
12.18 + \<^rule_eval>\<open>Prog_Expr.rhs\<close> (Prog_Expr.eval_rhs ""),
12.19 + \<^rule_eval>\<open>has_degree_in\<close> (eval_has_degree_in ""),
12.20 + \<^rule_eval>\<open>is_polyrat_in\<close> (eval_is_polyrat_in ""),
12.21 + \<^rule_eval>\<open>Prog_Expr.occurs_in\<close> (Prog_Expr.eval_occurs_in ""),
12.22 + \<^rule_eval>\<open>Prog_Expr.ident\<close> (Prog_Expr.eval_ident "#ident_"),
12.23 Rule.Thm ("not_true",ThmC.numerals_to_Free @{thm not_true}),
12.24 Rule.Thm ("not_false",ThmC.numerals_to_Free @{thm not_false}),
12.25 Rule.Thm ("and_true",ThmC.numerals_to_Free @{thm and_true}),
12.26 @@ -46,8 +46,8 @@
12.27 [Rule.Thm ("real_assoc_1",ThmC.numerals_to_Free @{thm real_assoc_1})
12.28 (*
12.29 Don't use
12.30 - Rule.Eval ("Rings.divide_class.divide", Prog_Expr.eval_cancel "#divide_e"),
12.31 - Rule.Eval ("Transcendental.powr" , (**)eval_binop "#power_"),
12.32 + \<^rule_eval>\<open>divide\<close> (Prog_Expr.eval_cancel "#divide_e"),
12.33 + \<^rule_eval>\<open>powr\<close> (**)(eval_binop "#power_"),
12.34 *)
12.35 ];
12.36
12.37 @@ -57,8 +57,8 @@
12.38 [Rule.Thm ("real_assoc_1",ThmC.numerals_to_Free @{thm real_assoc_1})
12.39 (*
12.40 Don't use
12.41 - Rule.Eval ("Rings.divide_class.divide", Prog_Expr.eval_cancel "#divide_e"),
12.42 - Rule.Eval ("Transcendental.powr" , (**)eval_binop "#power_"),
12.43 + \<^rule_eval>\<open>divide\<close> (Prog_Expr.eval_cancel "#divide_e"),
12.44 + \<^rule_eval>\<open>powr\<close> (**)(eval_binop "#power_"),
12.45 *)
12.46 ];
12.47 \<close>
12.48 @@ -73,14 +73,14 @@
12.49 calc = [], errpatts = [],
12.50 rules = [
12.51 Rule.Thm ("real_assoc_1",ThmC.numerals_to_Free @{thm real_assoc_1}),
12.52 - Rule.Eval ("Groups.plus_class.plus", (**)eval_binop "#add_"),
12.53 - Rule.Eval ("Groups.minus_class.minus", (**)eval_binop "#sub_"),
12.54 - Rule.Eval ("Groups.times_class.times", (**)eval_binop "#mult_"),
12.55 - (* Dont use
12.56 - Rule.Eval ("Rings.divide_class.divide", Prog_Expr.eval_cancel "#divide_e"),
12.57 - Rule.Eval ("NthRoot.sqrt", eval_sqrt "#sqrt_"),
12.58 + \<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_"),
12.59 + \<^rule_eval>\<open>minus\<close> (**)(eval_binop "#sub_"),
12.60 + \<^rule_eval>\<open>times\<close> (**)(eval_binop "#mult_"),
12.61 + (* Don't use
12.62 + \<^rule_eval>\<open>divide\<close> (Prog_Expr.eval_cancel "#divide_e"),
12.63 + \<^rule_eval>\<open>sqrt\<close> (eval_sqrt "#sqrt_"),
12.64 *)
12.65 - Rule.Eval ("Transcendental.powr" , (**)eval_binop "#power_")
12.66 + \<^rule_eval>\<open>powr\<close> (**)(eval_binop "#power_")
12.67 ],
12.68 scr = Rule.Empty_Prog});
12.69 \<close>
13.1 --- a/src/Tools/isac/Knowledge/Partial_Fractions.thy Thu Jun 10 17:06:32 2021 +0200
13.2 +++ b/src/Tools/isac/Knowledge/Partial_Fractions.thy Fri Jun 11 11:49:34 2021 +0200
13.3 @@ -168,21 +168,21 @@
13.4 rew_ord = ("termlessI",termlessI),
13.5 erls = Rule_Set.append_rules "erls_in_srls_partial_fraction" Rule_Set.empty
13.6 [(*for asm in NTH_CONS ...*)
13.7 - Rule.Eval ("Orderings.ord_class.less", Prog_Expr.eval_equ "#less_"),
13.8 + \<^rule_eval>\<open>less\<close> (Prog_Expr.eval_equ "#less_"),
13.9 (*2nd NTH_CONS pushes n+-1 into asms*)
13.10 - Rule.Eval("Groups.plus_class.plus", (**)eval_binop "#add_")],
13.11 + \<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_")],
13.12 srls = Rule_Set.Empty, calc = [], errpatts = [],
13.13 rules = [
13.14 Rule.Thm ("NTH_CONS",ThmC.numerals_to_Free @{thm NTH_CONS}),
13.15 - Rule.Eval("Groups.plus_class.plus", (**)eval_binop "#add_"),
13.16 + \<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_"),
13.17 Rule.Thm ("NTH_NIL",ThmC.numerals_to_Free @{thm NTH_NIL}),
13.18 - Rule.Eval("Prog_Expr.lhs", Prog_Expr.eval_lhs "eval_lhs_"),
13.19 - Rule.Eval("Prog_Expr.rhs", Prog_Expr.eval_rhs"eval_rhs_"),
13.20 - Rule.Eval("Prog_Expr.argument_in", Prog_Expr.eval_argument_in "Prog_Expr.argument_in"),
13.21 - Rule.Eval("Rational.get_denominator", eval_get_denominator "#get_denominator"),
13.22 - Rule.Eval("Rational.get_numerator", eval_get_numerator "#get_numerator"),
13.23 - Rule.Eval("Partial_Fractions.factors_from_solution",
13.24 - eval_factors_from_solution "#factors_from_solution")
13.25 + \<^rule_eval>\<open>Prog_Expr.lhs\<close> (Prog_Expr.eval_lhs "eval_lhs_"),
13.26 + \<^rule_eval>\<open>Prog_Expr.rhs\<close> (Prog_Expr.eval_rhs"eval_rhs_"),
13.27 + \<^rule_eval>\<open>Prog_Expr.argument_in\<close> (Prog_Expr.eval_argument_in "Prog_Expr.argument_in"),
13.28 + \<^rule_eval>\<open>get_denominator\<close> (eval_get_denominator "#get_denominator"),
13.29 + \<^rule_eval>\<open>get_numerator\<close> (eval_get_numerator "#get_numerator"),
13.30 + \<^rule_eval>\<open>factors_from_solution\<close>
13.31 + (eval_factors_from_solution "#factors_from_solution")
13.32 ],
13.33 scr = Rule.Empty_Prog};
13.34 \<close>
14.1 --- a/src/Tools/isac/Knowledge/Poly.thy Thu Jun 10 17:06:32 2021 +0200
14.2 +++ b/src/Tools/isac/Knowledge/Poly.thy Fri Jun 11 11:49:34 2021 +0200
14.3 @@ -652,20 +652,20 @@
14.4
14.5 (*.for evaluation of conditions in rewrite rules.*)
14.6 val Poly_erls = Rule_Set.append_rules "Poly_erls" Atools_erls
14.7 - [Rule.Eval ("HOL.eq", Prog_Expr.eval_equal "#equal_"),
14.8 + [\<^rule_eval>\<open>HOL.eq\<close> (Prog_Expr.eval_equal "#equal_"),
14.9 Rule.Thm ("real_unari_minus", ThmC.numerals_to_Free @{thm real_unari_minus}),
14.10 - Rule.Eval ("Groups.plus_class.plus", eval_binop "#add_"),
14.11 - Rule.Eval ("Groups.minus_class.minus", eval_binop "#sub_"),
14.12 - Rule.Eval ("Groups.times_class.times", eval_binop "#mult_"),
14.13 - Rule.Eval ("Transcendental.powr", eval_binop "#power_")];
14.14 + \<^rule_eval>\<open>plus\<close> (eval_binop "#add_"),
14.15 + \<^rule_eval>\<open>minus\<close> (eval_binop "#sub_"),
14.16 + \<^rule_eval>\<open>times\<close> (eval_binop "#mult_"),
14.17 + \<^rule_eval>\<open>powr\<close> (eval_binop "#power_")];
14.18
14.19 val poly_crls = Rule_Set.append_rules "poly_crls" Atools_crls
14.20 - [Rule.Eval ("HOL.eq", Prog_Expr.eval_equal "#equal_"),
14.21 + [\<^rule_eval>\<open>HOL.eq\<close> (Prog_Expr.eval_equal "#equal_"),
14.22 Rule.Thm ("real_unari_minus", ThmC.numerals_to_Free @{thm real_unari_minus}),
14.23 - Rule.Eval ("Groups.plus_class.plus", eval_binop "#add_"),
14.24 - Rule.Eval ("Groups.minus_class.minus", eval_binop "#sub_"),
14.25 - Rule.Eval ("Groups.times_class.times", eval_binop "#mult_"),
14.26 - Rule.Eval ("Transcendental.powr" , eval_binop "#power_")];
14.27 + \<^rule_eval>\<open>plus\<close> (eval_binop "#add_"),
14.28 + \<^rule_eval>\<open>minus\<close> (eval_binop "#sub_"),
14.29 + \<^rule_eval>\<open>times\<close> (eval_binop "#mult_"),
14.30 + \<^rule_eval>\<open>powr\<close> (eval_binop "#power_")];
14.31 \<close>
14.32 ML \<open>
14.33 val expand =
14.34 @@ -725,7 +725,7 @@
14.35 Rule_Def.Repeat{id = "expand_poly_rat_", preconds = [],
14.36 rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord),
14.37 erls = Rule_Set.append_rules "Rule_Set.empty-is_polyexp" Rule_Set.empty
14.38 - [Rule.Eval ("Poly.is_polyexp", eval_is_polyexp "")
14.39 + [\<^rule_eval>\<open>is_polyexp\<close> (eval_is_polyexp "")
14.40 ],
14.41 srls = Rule_Set.Empty,
14.42 calc = [], errpatts = [],
14.43 @@ -803,9 +803,9 @@
14.44 ("POWER", ("Transcendental.powr", eval_binop "#power_"))
14.45 ],
14.46 errpatts = [],
14.47 - rules = [Rule.Eval ("Groups.plus_class.plus", eval_binop "#add_"),
14.48 - Rule.Eval ("Groups.times_class.times", eval_binop "#mult_"),
14.49 - Rule.Eval ("Transcendental.powr", eval_binop "#power_")
14.50 + rules = [\<^rule_eval>\<open>plus\<close> (eval_binop "#add_"),
14.51 + \<^rule_eval>\<open>times\<close> (eval_binop "#mult_"),
14.52 + \<^rule_eval>\<open>powr\<close> (eval_binop "#power_")
14.53 ], scr = Rule.Empty_Prog};
14.54
14.55 val reduce_012_mult_ =
14.56 @@ -841,7 +841,7 @@
14.57 Rule.Thm ("real_one_collect_assoc_r",ThmC.numerals_to_Free @{thm real_one_collect_assoc_r}),
14.58 (*"m is_const ==> (k + n) + m * n = k + (m + 1) * n"*)
14.59
14.60 - Rule.Eval ("Groups.plus_class.plus", eval_binop "#add_"),
14.61 + \<^rule_eval>\<open>plus\<close> (eval_binop "#add_"),
14.62
14.63 (*MG: Reihenfolge der folgenden 2 Rule.Thm muss so bleiben, wegen
14.64 (a+a)+a --> a + 2*a --> 3*a and not (a+a)+a --> 2*a + a *)
14.65 @@ -962,9 +962,9 @@
14.66 (*"m is_const ==> n + m * n = (1 + m) * n"*)
14.67 Rule.Thm ("real_one_collect_assoc",ThmC.numerals_to_Free @{thm real_one_collect_assoc}),
14.68 (*"m is_const ==> k + (n + m * n) = k + (1 + m) * n"*)
14.69 - Rule.Eval ("Groups.plus_class.plus", eval_binop "#add_"),
14.70 - Rule.Eval ("Groups.times_class.times", eval_binop "#mult_"),
14.71 - Rule.Eval ("Transcendental.powr", eval_binop "#power_")
14.72 + \<^rule_eval>\<open>plus\<close> (eval_binop "#add_"),
14.73 + \<^rule_eval>\<open>times\<close> (eval_binop "#mult_"),
14.74 + \<^rule_eval>\<open>powr\<close> (eval_binop "#power_")
14.75 ], scr = Rule.Empty_Prog};
14.76 val reduce_012 =
14.77 Rule_Def.Repeat{id = "reduce_012", preconds = [],
14.78 @@ -1057,8 +1057,7 @@
14.79 TermC.parse_patt \<^theory> "?p :: real")],
14.80 rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord),
14.81 erls = Rule_Set.append_rules "Rule_Set.empty-is_multUnordered" Rule_Set.empty
14.82 - [Rule.Eval ("Poly.is_multUnordered",
14.83 - eval_is_multUnordered "")],
14.84 + [\<^rule_eval>\<open>is_multUnordered\<close> (eval_is_multUnordered "")],
14.85 calc = [("PLUS" , ("Groups.plus_class.plus", eval_binop "#add_")),
14.86 ("TIMES" , ("Groups.times_class.times", eval_binop "#mult_")),
14.87 ("DIVIDE", ("Rings.divide_class.divide", Prog_Expr.eval_cancel "#divide_e")),
14.88 @@ -1097,7 +1096,7 @@
14.89 fuer die Evaluation der Precondition "p is_addUnordered"*))],
14.90 rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord),
14.91 erls = Rule_Set.append_rules "Rule_Set.empty-is_addUnordered" Rule_Set.empty(*MG: poly_erls*)
14.92 - [Rule.Eval ("Poly.is_addUnordered", eval_is_addUnordered "")],
14.93 + [\<^rule_eval>\<open>is_addUnordered\<close> (eval_is_addUnordered "")],
14.94 calc = [("PLUS" ,("Groups.plus_class.plus", eval_binop "#add_")),
14.95 ("TIMES" ,("Groups.times_class.times", eval_binop "#mult_")),
14.96 ("DIVIDE",("Rings.divide_class.divide", Prog_Expr.eval_cancel "#divide_e")),
14.97 @@ -1135,7 +1134,7 @@
14.98 erls = Atools_erls, srls = Rule_Set.Empty,calc = [], errpatts = [],
14.99 rules = [Rule.Rls_ discard_minus,
14.100 Rule.Rls_ expand_poly_,
14.101 - Rule.Eval ("Groups.times_class.times", eval_binop "#mult_"),
14.102 + \<^rule_eval>\<open>times\<close> (eval_binop "#mult_"),
14.103 Rule.Rls_ order_mult_rls_,
14.104 Rule.Rls_ simplify_power_,
14.105 Rule.Rls_ calc_add_mult_pow_,
14.106 @@ -1155,7 +1154,7 @@
14.107 erls = Atools_erls, srls = Rule_Set.Empty, calc = [], errpatts = [],
14.108 rules = [Rule.Rls_ discard_minus,
14.109 Rule.Rls_ expand_poly_,
14.110 - Rule.Eval ("Groups.times_class.times", eval_binop "#mult_"),
14.111 + \<^rule_eval>\<open>times\<close> (eval_binop "#mult_"),
14.112 Rule.Rls_ order_mult_rls_,
14.113 Rule.Rls_ simplify_power_,
14.114 Rule.Rls_ calc_add_mult_pow_,
14.115 @@ -1178,7 +1177,7 @@
14.116 erls = Atools_erls, srls = Rule_Set.Empty, calc = [], errpatts = [],
14.117 rules = [Rule.Rls_ discard_minus,
14.118 Rule.Rls_ expand_poly_rat_,(*ignors rationals*)
14.119 - Rule.Eval ("Groups.times_class.times", eval_binop "#mult_"),
14.120 + \<^rule_eval>\<open>times\<close> (eval_binop "#mult_"),
14.121 Rule.Rls_ order_mult_rls_,
14.122 Rule.Rls_ simplify_power_,
14.123 Rule.Rls_ calc_add_mult_pow_,
14.124 @@ -1220,9 +1219,9 @@
14.125 Rule.Rls_ order_mult_rls_,
14.126 (*Rule.Rls_ order_add_rls_,*)
14.127
14.128 - Rule.Eval ("Groups.plus_class.plus", eval_binop "#add_"),
14.129 - Rule.Eval ("Groups.times_class.times", eval_binop "#mult_"),
14.130 - Rule.Eval ("Transcendental.powr", eval_binop "#power_"),
14.131 + \<^rule_eval>\<open>plus\<close> (eval_binop "#add_"),
14.132 + \<^rule_eval>\<open>times\<close> (eval_binop "#mult_"),
14.133 + \<^rule_eval>\<open>powr\<close> (eval_binop "#power_"),
14.134
14.135 Rule.Thm ("sym_realpow_twoI",
14.136 ThmC.numerals_to_Free (@{thm realpow_twoI} RS @{thm sym})),
14.137 @@ -1246,9 +1245,9 @@
14.138 Rule.Thm ("realpow_multI", ThmC.numerals_to_Free @{thm realpow_multI}),
14.139 (*"(r * s) \<up> n = r \<up> n * s \<up> n"*)
14.140
14.141 - Rule.Eval ("Groups.plus_class.plus", eval_binop "#add_"),
14.142 - Rule.Eval ("Groups.times_class.times", eval_binop "#mult_"),
14.143 - Rule.Eval ("Transcendental.powr", eval_binop "#power_"),
14.144 + \<^rule_eval>\<open>plus\<close> (eval_binop "#add_"),
14.145 + \<^rule_eval>\<open>times\<close> (eval_binop "#mult_"),
14.146 + \<^rule_eval>\<open>powr\<close> (eval_binop "#power_"),
14.147
14.148 Rule.Thm ("mult_1_left",ThmC.numerals_to_Free @{thm mult_1_left}),(*"1 * z = z"*)
14.149 Rule.Thm ("mult_zero_left",ThmC.numerals_to_Free @{thm mult_zero_left}),(*"0 * z = 0"*)
14.150 @@ -1354,9 +1353,9 @@
14.151 (*"0 * z = 0"*)
14.152 Rule.Thm ("add_0_left",ThmC.numerals_to_Free @{thm add_0_left}),(*"0 + z = z"*)
14.153
14.154 - Rule.Eval ("Groups.plus_class.plus", eval_binop "#add_"),
14.155 - Rule.Eval ("Groups.times_class.times", eval_binop "#mult_"),
14.156 - Rule.Eval ("Transcendental.powr", eval_binop "#power_"),
14.157 + \<^rule_eval>\<open>plus\<close> (eval_binop "#add_"),
14.158 + \<^rule_eval>\<open>times\<close> (eval_binop "#mult_"),
14.159 + \<^rule_eval>\<open>powr\<close> (eval_binop "#power_"),
14.160 (*Rule.Thm ("mult.commute",ThmC.numerals_to_Free @{thm mult.commute}),
14.161 (*AC-rewriting*)
14.162 Rule.Thm ("real_mult_left_commute",
14.163 @@ -1389,9 +1388,9 @@
14.164 ThmC.numerals_to_Free @{thm real_one_collect_assoc}),
14.165 (*"m is_const ==> k + (n + m * n) = k + (1 + m) * n"*)
14.166
14.167 - Rule.Eval ("Groups.plus_class.plus", eval_binop "#add_"),
14.168 - Rule.Eval ("Groups.times_class.times", eval_binop "#mult_"),
14.169 - Rule.Eval ("Transcendental.powr", eval_binop "#power_")
14.170 + \<^rule_eval>\<open>plus\<close> (eval_binop "#add_"),
14.171 + \<^rule_eval>\<open>times\<close> (eval_binop "#mult_"),
14.172 + \<^rule_eval>\<open>powr\<close> (eval_binop "#power_")
14.173 ],
14.174 scr = Rule.Prog (Program.prep_program @{thm expand_binoms_2.simps})
14.175 };
14.176 @@ -1439,7 +1438,7 @@
14.177 ("#Where" ,["t_t is_polyexp"]),
14.178 ("#Find" ,["normalform n_n"])],
14.179 Rule_Set.append_rules "empty" Rule_Set.empty [(*for preds in where_*)
14.180 - Rule.Eval ("Poly.is_polyexp", eval_is_polyexp "")],
14.181 + \<^rule_eval>\<open>is_polyexp\<close> (eval_is_polyexp "")],
14.182 SOME "Simplify t_t",
14.183 [["simplification", "for_polynomials"]]))]\<close>
14.184
14.185 @@ -1457,7 +1456,7 @@
14.186 {rew_ord'="tless_true", rls' = Rule_Set.empty, calc = [], srls = Rule_Set.empty,
14.187 prls = Rule_Set.append_rules "simplification_for_polynomials_prls" Rule_Set.empty
14.188 [(*for preds in where_*)
14.189 - Rule.Eval ("Poly.is_polyexp", eval_is_polyexp"")],
14.190 + \<^rule_eval>\<open>is_polyexp\<close> (eval_is_polyexp"")],
14.191 crls = Rule_Set.empty, errpats = [], nrls = norm_Poly},
14.192 @{thm simplify.simps})]
14.193 \<close>
15.1 --- a/src/Tools/isac/Knowledge/PolyEq.thy Thu Jun 10 17:06:32 2021 +0200
15.2 +++ b/src/Tools/isac/Knowledge/PolyEq.thy Fri Jun 11 11:49:34 2021 +0200
15.3 @@ -322,19 +322,19 @@
15.4 (*-------------------------rulse-------------------------*)
15.5 val PolyEq_prls = (*3.10.02:just the following order due to subterm evaluation*)
15.6 Rule_Set.append_rules "PolyEq_prls" Rule_Set.empty
15.7 - [Rule.Eval ("Prog_Expr.ident", Prog_Expr.eval_ident "#ident_"),
15.8 - Rule.Eval ("Prog_Expr.matches", Prog_Expr.eval_matches ""),
15.9 - Rule.Eval ("Prog_Expr.lhs", Prog_Expr.eval_lhs ""),
15.10 - Rule.Eval ("Prog_Expr.rhs", Prog_Expr.eval_rhs ""),
15.11 - Rule.Eval ("Poly.is_expanded_in", eval_is_expanded_in ""),
15.12 - Rule.Eval ("Poly.is_poly_in", eval_is_poly_in ""),
15.13 - Rule.Eval ("Poly.has_degree_in", eval_has_degree_in ""),
15.14 - Rule.Eval ("Poly.is_polyrat_in", eval_is_polyrat_in ""),
15.15 - (*Rule.Eval ("Prog_Expr.occurs_in", Prog_Expr.eval_occurs_in ""), *)
15.16 - (*Rule.Eval ("Prog_Expr.is_const", Prog_Expr.eval_const "#is_const_"),*)
15.17 - Rule.Eval ("HOL.eq", Prog_Expr.eval_equal "#equal_"),
15.18 - Rule.Eval ("RootEq.is_rootTerm_in", eval_is_rootTerm_in ""),
15.19 - Rule.Eval ("RatEq.is_ratequation_in", eval_is_ratequation_in ""),
15.20 + [\<^rule_eval>\<open>Prog_Expr.ident\<close> (Prog_Expr.eval_ident "#ident_"),
15.21 + \<^rule_eval>\<open>Prog_Expr.matches\<close> (Prog_Expr.eval_matches ""),
15.22 + \<^rule_eval>\<open>Prog_Expr.lhs\<close> (Prog_Expr.eval_lhs ""),
15.23 + \<^rule_eval>\<open>Prog_Expr.rhs\<close> (Prog_Expr.eval_rhs ""),
15.24 + \<^rule_eval>\<open>is_expanded_in\<close> (eval_is_expanded_in ""),
15.25 + \<^rule_eval>\<open>is_poly_in\<close> (eval_is_poly_in ""),
15.26 + \<^rule_eval>\<open>has_degree_in\<close> (eval_has_degree_in ""),
15.27 + \<^rule_eval>\<open>is_polyrat_in\<close> (eval_is_polyrat_in ""),
15.28 + (*\<^rule_eval>\<open>Prog_Expr.occurs_in\<close> (Prog_Expr.eval_occurs_in ""), *)
15.29 + (*\<^rule_eval>\<open>Prog_Expr.is_const\<close> (Prog_Expr.eval_const "#is_const_"),*)
15.30 + \<^rule_eval>\<open>HOL.eq\<close> (Prog_Expr.eval_equal "#equal_"),
15.31 + \<^rule_eval>\<open>is_rootTerm_in\<close> (eval_is_rootTerm_in ""),
15.32 + \<^rule_eval>\<open>is_ratequation_in\<close> (eval_is_ratequation_in ""),
15.33 Rule.Thm ("not_true",ThmC.numerals_to_Free @{thm not_true}),
15.34 Rule.Thm ("not_false",ThmC.numerals_to_Free @{thm not_false}),
15.35 Rule.Thm ("and_true",ThmC.numerals_to_Free @{thm and_true}),
15.36 @@ -346,7 +346,7 @@
15.37 val PolyEq_erls =
15.38 Rule_Set.merge "PolyEq_erls" LinEq_erls
15.39 (Rule_Set.append_rules "ops_preds" calculate_Rational
15.40 - [Rule.Eval ("HOL.eq", Prog_Expr.eval_equal "#equal_"),
15.41 + [\<^rule_eval>\<open>HOL.eq\<close> (Prog_Expr.eval_equal "#equal_"),
15.42 Rule.Thm ("plus_leq", ThmC.numerals_to_Free @{thm plus_leq}),
15.43 Rule.Thm ("minus_leq", ThmC.numerals_to_Free @{thm minus_leq}),
15.44 Rule.Thm ("rat_leq1", ThmC.numerals_to_Free @{thm rat_leq1}),
15.45 @@ -357,7 +357,7 @@
15.46 val PolyEq_crls =
15.47 Rule_Set.merge "PolyEq_crls" LinEq_crls
15.48 (Rule_Set.append_rules "ops_preds" calculate_Rational
15.49 - [Rule.Eval ("HOL.eq", Prog_Expr.eval_equal "#equal_"),
15.50 + [\<^rule_eval>\<open>HOL.eq\<close> (Prog_Expr.eval_equal "#equal_"),
15.51 Rule.Thm ("plus_leq", ThmC.numerals_to_Free @{thm plus_leq}),
15.52 Rule.Thm ("minus_leq", ThmC.numerals_to_Free @{thm minus_leq}),
15.53 Rule.Thm ("rat_leq1", ThmC.numerals_to_Free @{thm rat_leq1}),
15.54 @@ -412,12 +412,12 @@
15.55 Rule.Thm ("real_diff_minus",ThmC.numerals_to_Free @{thm real_diff_minus}),
15.56 Rule.Thm ("real_unari_minus",ThmC.numerals_to_Free @{thm real_unari_minus}),
15.57 Rule.Thm ("realpow_multI",ThmC.numerals_to_Free @{thm realpow_multI}),
15.58 - Rule.Eval ("Groups.plus_class.plus", (**)eval_binop "#add_"),
15.59 - Rule.Eval ("Groups.minus_class.minus", (**)eval_binop "#sub_"),
15.60 - Rule.Eval ("Groups.times_class.times", (**)eval_binop "#mult_"),
15.61 - Rule.Eval ("Rings.divide_class.divide", Prog_Expr.eval_cancel "#divide_e"),
15.62 - Rule.Eval ("NthRoot.sqrt", eval_sqrt "#sqrt_"),
15.63 - Rule.Eval ("Transcendental.powr" , (**)eval_binop "#power_"),
15.64 + \<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_"),
15.65 + \<^rule_eval>\<open>minus\<close> (**)(eval_binop "#sub_"),
15.66 + \<^rule_eval>\<open>times\<close> (**)(eval_binop "#mult_"),
15.67 + \<^rule_eval>\<open>divide\<close> (Prog_Expr.eval_cancel "#divide_e"),
15.68 + \<^rule_eval>\<open>sqrt\<close> (eval_sqrt "#sqrt_"),
15.69 + \<^rule_eval>\<open>powr\<close> (**)(eval_binop "#power_"),
15.70 Rule.Rls_ reduce_012
15.71 ],
15.72 scr = Rule.Empty_Prog
15.73 @@ -1323,7 +1323,7 @@
15.74 Rule.Rls_ separate_bdvs,
15.75 (* Rule.Rls_ rearrange_assoc, WN060916 why does cancel_p not work?*)
15.76 Rule.Rls_ cancel_p
15.77 - (*Rule.Eval ("Rings.divide_class.divide" , eval_cancel "#divide_e") too weak!*)
15.78 + (*\<^rule_eval>\<open>divide\<close> (eval_cancel "#divide_e") too weak!*)
15.79 ],
15.80 scr = Rule.Empty_Prog});
15.81 \<close>
16.1 --- a/src/Tools/isac/Knowledge/PolyMinus.thy Thu Jun 10 17:06:32 2021 +0200
16.2 +++ b/src/Tools/isac/Knowledge/PolyMinus.thy Fri Jun 11 11:49:34 2021 +0200
16.3 @@ -192,8 +192,8 @@
16.4
16.5 val erls_ordne_alphabetisch =
16.6 Rule_Set.append_rules "erls_ordne_alphabetisch" Rule_Set.empty
16.7 - [Rule.Eval ("PolyMinus.kleiner", eval_kleiner ""),
16.8 - Rule.Eval ("PolyMinus.ist_monom", eval_ist_monom "")
16.9 + [\<^rule_eval>\<open>PolyMinus.kleiner\<close> (eval_kleiner ""),
16.10 + \<^rule_eval>\<open>PolyMinus.ist_monom\<close> (eval_ist_monom "")
16.11 ];
16.12
16.13 val ordne_alphabetisch =
16.14 @@ -222,7 +222,7 @@
16.15 Rule_Def.Repeat{id = "fasse_zusammen", preconds = [],
16.16 rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord),
16.17 erls = Rule_Set.append_rules "erls_fasse_zusammen" Rule_Set.empty
16.18 - [Rule.Eval ("Prog_Expr.is_const", Prog_Expr.eval_const "#is_const_")],
16.19 + [\<^rule_eval>\<open>Prog_Expr.is_const\<close> (Prog_Expr.eval_const "#is_const_")],
16.20 srls = Rule_Set.Empty, calc = [], errpatts = [],
16.21 rules =
16.22 [Rule.Thm ("real_num_collect",ThmC.numerals_to_Free @{thm real_num_collect}),
16.23 @@ -263,8 +263,8 @@
16.24 Rule.Thm ("subtrahiere_x_minus_minus1",ThmC.numerals_to_Free @{thm subtrahiere_x_minus_minus1}),
16.25 (*"[| m is_const |] ==> (x - m * v) - v = x + (-m - 1) * v"*)
16.26
16.27 - Rule.Eval ("Groups.plus_class.plus", (**)eval_binop "#add_"),
16.28 - Rule.Eval ("Groups.minus_class.minus", (**)eval_binop "#subtr_"),
16.29 + \<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_"),
16.30 + \<^rule_eval>\<open>minus\<close> (**)(eval_binop "#subtr_"),
16.31
16.32 (*MG: Reihenfolge der folgenden 2 Rule.Thm muss so bleiben, wegen
16.33 (a+a)+a --> a + 2*a --> 3*a and not (a+a)+a --> 2*a + a *)
16.34 @@ -288,7 +288,7 @@
16.35 Rule_Def.Repeat{id = "verschoenere", preconds = [],
16.36 rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord), srls = Rule_Set.Empty, calc = [], errpatts = [],
16.37 erls = Rule_Set.append_rules "erls_verschoenere" Rule_Set.empty
16.38 - [Rule.Eval ("PolyMinus.kleiner", eval_kleiner "")],
16.39 + [\<^rule_eval>\<open>PolyMinus.kleiner\<close> (eval_kleiner "")],
16.40 rules = [Rule.Thm ("vorzeichen_minus_weg1",ThmC.numerals_to_Free @{thm vorzeichen_minus_weg1}),
16.41 (*"l kleiner 0 ==> a + l * b = a - -l * b"*)
16.42 Rule.Thm ("vorzeichen_minus_weg2",ThmC.numerals_to_Free @{thm vorzeichen_minus_weg2}),
16.43 @@ -298,7 +298,7 @@
16.44 Rule.Thm ("vorzeichen_minus_weg4",ThmC.numerals_to_Free @{thm vorzeichen_minus_weg4}),
16.45 (*"l kleiner 0 ==> k - a - l * b = k - a + -l * b"*)
16.46
16.47 - Rule.Eval ("Groups.times_class.times", (**)eval_binop "#mult_"),
16.48 + \<^rule_eval>\<open>times\<close> (**)(eval_binop "#mult_"),
16.49
16.50 Rule.Thm ("mult_zero_left",ThmC.numerals_to_Free @{thm mult_zero_left}),
16.51 (*"0 * z = 0"*)
16.52 @@ -350,8 +350,8 @@
16.53 Rule_Def.Repeat{id = "ordne_monome", preconds = [],
16.54 rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord), srls = Rule_Set.Empty, calc = [], errpatts = [],
16.55 erls = Rule_Set.append_rules "erls_ordne_monome" Rule_Set.empty
16.56 - [Rule.Eval ("PolyMinus.kleiner", eval_kleiner ""),
16.57 - Rule.Eval ("Prog_Expr.is_atom", Prog_Expr.eval_is_atom "")
16.58 + [\<^rule_eval>\<open>PolyMinus.kleiner\<close> (eval_kleiner ""),
16.59 + \<^rule_eval>\<open>Prog_Expr.is_atom\<close> (Prog_Expr.eval_is_atom "")
16.60 ],
16.61 rules = [Rule.Thm ("tausche_mal",ThmC.numerals_to_Free @{thm tausche_mal}),
16.62 (*"[| b is_atom; a kleiner b |] ==> (b * a) = (a * b)"*)
16.63 @@ -382,9 +382,9 @@
16.64 ];
16.65 val rechnen =
16.66 Rule_Set.append_rules "rechnen" Rule_Set.empty
16.67 - [Rule.Eval ("Groups.times_class.times", (**)eval_binop "#mult_"),
16.68 - Rule.Eval ("Groups.plus_class.plus", (**)eval_binop "#add_"),
16.69 - Rule.Eval ("Groups.minus_class.minus", (**)eval_binop "#subtr_")
16.70 + [\<^rule_eval>\<open>times\<close> (**)(eval_binop "#mult_"),
16.71 + \<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_"),
16.72 + \<^rule_eval>\<open>minus\<close> (**)(eval_binop "#subtr_")
16.73 ];
16.74 \<close>
16.75 rule_set_knowledge
16.76 @@ -413,8 +413,8 @@
16.77 " matchsub ((?b - ?c) * ?a) t_t )"]),
16.78 ("#Find", ["normalform n_n"])],
16.79 Rule_Set.append_rules "prls_pbl_vereinf_poly" Rule_Set.empty
16.80 - [Rule.Eval ("Poly.is_polyexp", eval_is_polyexp ""),
16.81 - Rule.Eval ("Prog_Expr.matchsub", Prog_Expr.eval_matchsub ""),
16.82 + [\<^rule_eval>\<open>is_polyexp\<close> (eval_is_polyexp ""),
16.83 + \<^rule_eval>\<open>Prog_Expr.matchsub\<close> (Prog_Expr.eval_matchsub ""),
16.84 Rule.Thm ("or_true", ThmC.numerals_to_Free @{thm or_true}),
16.85 (*"(?a | True) = True"*)
16.86 Rule.Thm ("or_false", ThmC.numerals_to_Free @{thm or_false}),
16.87 @@ -434,8 +434,8 @@
16.88 " matchsub ((?b - ?c) * ?a) t_t )"]),
16.89 ("#Find" ,["normalform n_n"])],
16.90 Rule_Set.append_rules "prls_pbl_vereinf_poly_klammer" Rule_Set.empty
16.91 - [Rule.Eval ("Poly.is_polyexp", eval_is_polyexp ""),
16.92 - Rule.Eval ("Prog_Expr.matchsub", Prog_Expr.eval_matchsub ""),
16.93 + [\<^rule_eval>\<open>is_polyexp\<close> (eval_is_polyexp ""),
16.94 + \<^rule_eval>\<open>Prog_Expr.matchsub\<close> (Prog_Expr.eval_matchsub ""),
16.95 Rule.Thm ("or_true", ThmC.numerals_to_Free @{thm or_true}),
16.96 (*"(?a | True) = True"*)
16.97 Rule.Thm ("or_false", ThmC.numerals_to_Free @{thm or_false}),
16.98 @@ -452,7 +452,7 @@
16.99 ("#Where", ["t_t is_polyexp"]),
16.100 ("#Find", ["normalform n_n"])],
16.101 Rule_Set.append_rules "empty" Rule_Set.empty [(*for preds in where_*)
16.102 - Rule.Eval ("Poly.is_polyexp", eval_is_polyexp "")],
16.103 + \<^rule_eval>\<open>is_polyexp\<close> (eval_is_polyexp "")],
16.104 SOME "Vereinfache t_t",
16.105 [["simplification", "for_polynomials", "with_parentheses_mult"]])),
16.106 (Problem.prep_input @{theory} "pbl_probe" [] Problem.id_empty (["probe"], [], Rule_Set.Empty, NONE, [])),
16.107 @@ -462,7 +462,7 @@
16.108 ("#Where", ["e_e is_polyexp"]),
16.109 ("#Find", ["Geprueft p_p"])],
16.110 Rule_Set.append_rules "prls_pbl_probe_poly" Rule_Set.empty [(*for preds in where_*)
16.111 - Rule.Eval ("Poly.is_polyexp", eval_is_polyexp "")],
16.112 + \<^rule_eval>\<open>is_polyexp\<close> (eval_is_polyexp "")],
16.113 SOME "Probe e_e w_w",
16.114 [["probe", "fuer_polynom"]])),
16.115 (Problem.prep_input @{theory} "pbl_probe_bruch" [] Problem.id_empty
16.116 @@ -471,7 +471,7 @@
16.117 ("#Where" ,["e_e is_ratpolyexp"]),
16.118 ("#Find" ,["Geprueft p_p"])],
16.119 Rule_Set.append_rules "prls_pbl_probe_bruch" Rule_Set.empty [(*for preds in where_*)
16.120 - Rule.Eval ("Rational.is_ratpolyexp", eval_is_ratpolyexp "")],
16.121 + \<^rule_eval>\<open>is_ratpolyexp\<close> (eval_is_ratpolyexp "")],
16.122 SOME "Probe e_e w_w", [["probe", "fuer_bruch"]]))]\<close>
16.123
16.124 (** methods **)
16.125 @@ -496,8 +496,8 @@
16.126 ("#Find" ,["normalform n_n"])],
16.127 {rew_ord'="tless_true", rls' = Rule_Set.empty, calc = [], srls = Rule_Set.empty,
16.128 prls = Rule_Set.append_rules "prls_met_simp_poly_minus" Rule_Set.empty
16.129 - [Rule.Eval ("Poly.is_polyexp", eval_is_polyexp ""),
16.130 - Rule.Eval ("Prog_Expr.matchsub", Prog_Expr.eval_matchsub ""),
16.131 + [\<^rule_eval>\<open>is_polyexp\<close> (eval_is_polyexp ""),
16.132 + \<^rule_eval>\<open>Prog_Expr.matchsub\<close> (Prog_Expr.eval_matchsub ""),
16.133 Rule.Thm ("and_true",ThmC.numerals_to_Free @{thm and_true}),
16.134 (*"(?a & True) = ?a"*)
16.135 Rule.Thm ("and_false",ThmC.numerals_to_Free @{thm and_false}),
16.136 @@ -527,7 +527,7 @@
16.137 ("#Find" ,["normalform n_n"])],
16.138 {rew_ord'="tless_true", rls' = Rule_Set.empty, calc = [], srls = Rule_Set.empty,
16.139 prls = Rule_Set.append_rules "simplification_for_polynomials_prls" Rule_Set.empty
16.140 - [(*for preds in where_*) Rule.Eval("Poly.is_polyexp", eval_is_polyexp"")],
16.141 + [(*for preds in where_*) \<^rule_eval>\<open>is_polyexp\<close> (eval_is_polyexp"")],
16.142 crls = Rule_Set.empty, errpats = [], nrls = rls_p_34},
16.143 @{thm simplify2.simps})]
16.144 \<close>
16.145 @@ -550,7 +550,7 @@
16.146 [("#Given" ,["Term t_t"]), ("#Where" ,["t_t is_polyexp"]), ("#Find" ,["normalform n_n"])],
16.147 {rew_ord'="tless_true", rls' = Rule_Set.empty, calc = [], srls = Rule_Set.empty,
16.148 prls = Rule_Set.append_rules "simplification_for_polynomials_prls" Rule_Set.empty
16.149 - [(*for preds in where_*) Rule.Eval("Poly.is_polyexp", eval_is_polyexp"")],
16.150 + [(*for preds in where_*) \<^rule_eval>\<open>is_polyexp\<close> (eval_is_polyexp"")],
16.151 crls = Rule_Set.empty, errpats = [], nrls = rls_p_34},
16.152 @{thm simplify3.simps})]
16.153 \<close>
16.154 @@ -582,7 +582,7 @@
16.155 ("#Find" ,["Geprueft p_p"])],
16.156 {rew_ord'="tless_true", rls' = Rule_Set.empty, calc = [], srls = Rule_Set.empty,
16.157 prls = Rule_Set.append_rules "prls_met_probe_bruch" Rule_Set.empty
16.158 - [(*for preds in where_*) Rule.Eval ("Rational.is_ratpolyexp", eval_is_ratpolyexp "")],
16.159 + [(*for preds in where_*) \<^rule_eval>\<open>is_ratpolyexp\<close> (eval_is_ratpolyexp "")],
16.160 crls = Rule_Set.empty, errpats = [], nrls = rechnen},
16.161 @{thm mache_probe.simps})]
16.162 \<close>
16.163 @@ -594,7 +594,7 @@
16.164 ("#Find" ,["Geprueft p_p"])],
16.165 {rew_ord'="tless_true", rls' = Rule_Set.empty, calc = [], srls = Rule_Set.empty,
16.166 prls = Rule_Set.append_rules "prls_met_probe_bruch" Rule_Set.empty
16.167 - [(*for preds in where_*) Rule.Eval ("Rational.is_ratpolyexp", eval_is_ratpolyexp "")],
16.168 + [(*for preds in where_*) \<^rule_eval>\<open>is_ratpolyexp\<close> (eval_is_ratpolyexp "")],
16.169 crls = Rule_Set.empty, errpats = [], nrls = Rule_Set.Empty},
16.170 @{thm refl})]
16.171 \<close> ML \<open>
17.1 --- a/src/Tools/isac/Knowledge/RatEq.thy Thu Jun 10 17:06:32 2021 +0200
17.2 +++ b/src/Tools/isac/Knowledge/RatEq.thy Fri Jun 11 11:49:34 2021 +0200
17.3 @@ -80,12 +80,12 @@
17.4 ML \<open>
17.5 val RatEq_prls = (*15.10.02:just the following order due to subterm evaluation*)
17.6 Rule_Set.append_rules "RatEq_prls" Rule_Set.empty
17.7 - [Rule.Eval ("Prog_Expr.ident", Prog_Expr.eval_ident "#ident_"),
17.8 - Rule.Eval ("Prog_Expr.matches", Prog_Expr.eval_matches ""),
17.9 - Rule.Eval ("Prog_Expr.lhs", Prog_Expr.eval_lhs ""),
17.10 - Rule.Eval ("Prog_Expr.rhs", Prog_Expr.eval_rhs ""),
17.11 - Rule.Eval ("RatEq.is_ratequation_in", eval_is_ratequation_in ""),
17.12 - Rule.Eval ("HOL.eq", Prog_Expr.eval_equal "#equal_"),
17.13 + [\<^rule_eval>\<open>Prog_Expr.ident\<close> (Prog_Expr.eval_ident "#ident_"),
17.14 + \<^rule_eval>\<open>Prog_Expr.matches\<close> (Prog_Expr.eval_matches ""),
17.15 + \<^rule_eval>\<open>Prog_Expr.lhs\<close> (Prog_Expr.eval_lhs ""),
17.16 + \<^rule_eval>\<open>Prog_Expr.rhs\<close> (Prog_Expr.eval_rhs ""),
17.17 + \<^rule_eval>\<open>is_ratequation_in\<close> (eval_is_ratequation_in ""),
17.18 + \<^rule_eval>\<open>HOL.eq\<close> (Prog_Expr.eval_equal "#equal_"),
17.19 Rule.Thm ("not_true",ThmC.numerals_to_Free @{thm not_true}),
17.20 Rule.Thm ("not_false",ThmC.numerals_to_Free @{thm not_false}),
17.21 Rule.Thm ("and_true",ThmC.numerals_to_Free @{thm and_true}),
17.22 @@ -100,8 +100,8 @@
17.23 Rule_Set.keep_unique_rules "rateq_erls" (*WN: ein Hack*)
17.24 (Rule_Set.merge "is_ratequation_in" calculate_Rational
17.25 (Rule_Set.append_rules "is_ratequation_in"
17.26 - Poly_erls [(*Rule.Eval ("Rings.divide_class.divide", Prog_Expr.eval_cancel "#divide_e"),*)
17.27 - Rule.Eval ("RatEq.is_ratequation_in", eval_is_ratequation_in "")]))
17.28 + Poly_erls [(*\<^rule_eval>\<open>divide\<close> (Prog_Expr.eval_cancel "#divide_e"),*)
17.29 + \<^rule_eval>\<open>is_ratequation_in\<close> (eval_is_ratequation_in "")]))
17.30 [Rule.Thm ("and_commute",ThmC.numerals_to_Free @{thm and_commute}), (*WN: ein Hack*)
17.31 Rule.Thm ("or_commute",ThmC.numerals_to_Free @{thm or_commute})]; (*WN: ein Hack*)
17.32
17.33 @@ -110,8 +110,8 @@
17.34 Rule_Set.keep_unique_rules "RatEq_crls" (*WN: ein Hack*)
17.35 (Rule_Set.merge "is_ratequation_in" calculate_Rational
17.36 (Rule_Set.append_rules "is_ratequation_in"
17.37 - Poly_erls [(*Rule.Eval ("Rings.divide_class.divide", Prog_Expr.eval_cancel "#divide_e"),*)
17.38 - Rule.Eval ("RatEq.is_ratequation_in", eval_is_ratequation_in "")]))
17.39 + Poly_erls [(*\<^rule_eval>\<open>divide\<close> (Prog_Expr.eval_cancel "#divide_e"),*)
17.40 + \<^rule_eval>\<open>is_ratequation_in\<close> (eval_is_ratequation_in "")]))
17.41 [Rule.Thm ("and_commute",ThmC.numerals_to_Free @{thm and_commute}), (*WN: ein Hack*)
17.42 Rule.Thm ("or_commute",ThmC.numerals_to_Free @{thm or_commute})]; (*WN: ein Hack*)
17.43
18.1 --- a/src/Tools/isac/Knowledge/Rational.thy Thu Jun 10 17:06:32 2021 +0200
18.2 +++ b/src/Tools/isac/Knowledge/Rational.thy Fri Jun 11 11:49:34 2021 +0200
18.3 @@ -394,8 +394,8 @@
18.4 (Rule_Def.Repeat {id = "calc_rat_erls", preconds = [], rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord),
18.5 erls = Rule_Set.empty, srls = Rule_Set.Empty, calc = [], errpatts = [],
18.6 rules =
18.7 - [Rule.Eval ("HOL.eq", Prog_Expr.eval_equal "#equal_"),
18.8 - Rule.Eval ("Prog_Expr.is_const", Prog_Expr.eval_const "#is_const_"),
18.9 + [\<^rule_eval>\<open>HOL.eq\<close> (Prog_Expr.eval_equal "#equal_"),
18.10 + \<^rule_eval>\<open>Prog_Expr.is_const\<close> (Prog_Expr.eval_const "#is_const_"),
18.11 Rule.Thm ("not_true", ThmC.numerals_to_Free @{thm not_true}),
18.12 Rule.Thm ("not_false", ThmC.numerals_to_Free @{thm not_false})],
18.13 scr = Rule.Empty_Prog});
18.14 @@ -409,7 +409,7 @@
18.15 erls = calc_rat_erls, srls = Rule_Set.Empty,
18.16 calc = [], errpatts = [],
18.17 rules =
18.18 - [Rule.Eval ("Rings.divide_class.divide", Prog_Expr.eval_cancel "#divide_e"),
18.19 + [\<^rule_eval>\<open>divide\<close> (Prog_Expr.eval_cancel "#divide_e"),
18.20
18.21 Rule.Thm ("minus_divide_left", ThmC.numerals_to_Free (@{thm minus_divide_left} RS @{thm sym})),
18.22 (*SYM - ?x / ?y = - (?x / ?y) may come from subst*)
18.23 @@ -464,7 +464,7 @@
18.24 val rational_erls =
18.25 Rule_Set.merge "rational_erls" calculate_Rational
18.26 (Rule_Set.append_rules "is_expanded" Atools_erls
18.27 - [Rule.Eval ("Rational.is_expanded", eval_is_expanded "")]);
18.28 + [\<^rule_eval>\<open>is_expanded\<close> (eval_is_expanded "")]);
18.29 \<close>
18.30
18.31 subsection \<open>Embed cancellation into rewriting\<close>
18.32 @@ -604,12 +604,12 @@
18.33 val powers_erls = prep_rls'(
18.34 Rule_Def.Repeat {id = "powers_erls", preconds = [], rew_ord = ("dummy_ord",Rewrite_Ord.dummy_ord),
18.35 erls = Rule_Set.empty, srls = Rule_Set.Empty, calc = [], errpatts = [],
18.36 - rules = [Rule.Eval ("Prog_Expr.is_atom", Prog_Expr.eval_is_atom "#is_atom_"),
18.37 - Rule.Eval ("Prog_Expr.is_even", Prog_Expr.eval_is_even "#is_even_"),
18.38 - Rule.Eval ("Orderings.ord_class.less", Prog_Expr.eval_equ "#less_"),
18.39 + rules = [\<^rule_eval>\<open>Prog_Expr.is_atom\<close> (Prog_Expr.eval_is_atom "#is_atom_"),
18.40 + \<^rule_eval>\<open>Prog_Expr.is_even\<close> (Prog_Expr.eval_is_even "#is_even_"),
18.41 + \<^rule_eval>\<open>less\<close> (Prog_Expr.eval_equ "#less_"),
18.42 Rule.Thm ("not_false", ThmC.numerals_to_Free @{thm not_false}),
18.43 Rule.Thm ("not_true", ThmC.numerals_to_Free @{thm not_true}),
18.44 - Rule.Eval ("Groups.plus_class.plus", (**)eval_binop "#add_")
18.45 + \<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_")
18.46 ],
18.47 scr = Rule.Empty_Prog
18.48 });
18.49 @@ -642,7 +642,7 @@
18.50 (*"[| 1 < n; ~ (r is_atom) |]==>r \<up> n = r * r \<up> (n + -1)"*)
18.51 Rule.Thm ("realpow_eq_oneI",ThmC.numerals_to_Free @{thm realpow_eq_oneI}),
18.52 (*"1 \<up> n = 1"*)
18.53 - Rule.Eval ("Groups.plus_class.plus", (**)eval_binop "#add_")
18.54 + \<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_")
18.55 ],
18.56 scr = Rule.Empty_Prog
18.57 });
18.58 @@ -666,7 +666,7 @@
18.59 Rule.Thm ("divide_divide_eq_left",
18.60 ThmC.numerals_to_Free @{thm divide_divide_eq_left}),
18.61 (*"?x / ?y / ?z = ?x / (?y * ?z)"*)
18.62 - Rule.Eval ("Rings.divide_class.divide", Prog_Expr.eval_cancel "#divide_e")
18.63 + \<^rule_eval>\<open>divide\<close> (Prog_Expr.eval_cancel "#divide_e")
18.64 ],
18.65 scr = Rule.Empty_Prog
18.66 });
18.67 @@ -706,7 +706,7 @@
18.68 val norm_rat_erls = prep_rls'(
18.69 Rule_Def.Repeat {id = "norm_rat_erls", preconds = [], rew_ord = ("dummy_ord",Rewrite_Ord.dummy_ord),
18.70 erls = Rule_Set.empty, srls = Rule_Set.Empty, calc = [], errpatts = [],
18.71 - rules = [Rule.Eval ("Prog_Expr.is_const", Prog_Expr.eval_const "#is_const_")
18.72 + rules = [\<^rule_eval>\<open>Prog_Expr.is_const\<close> (Prog_Expr.eval_const "#is_const_")
18.73 ], scr = Rule.Empty_Prog});
18.74
18.75 (* consists of rls containing the absolute minimum of thms *)
18.76 @@ -778,7 +778,8 @@
18.77 used in initial part norm_Rational_mg, see example DA-M02-main.p.60.*)
18.78 val rat_mult_poly = prep_rls'(
18.79 Rule_Def.Repeat {id = "rat_mult_poly", preconds = [], rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord),
18.80 - erls = Rule_Set.append_rules "Rule_Set.empty-is_polyexp" Rule_Set.empty [Rule.Eval ("Poly.is_polyexp", eval_is_polyexp "")],
18.81 + erls = Rule_Set.append_rules "Rule_Set.empty-is_polyexp" Rule_Set.empty
18.82 + [\<^rule_eval>\<open>is_polyexp\<close> (eval_is_polyexp "")],
18.83 srls = Rule_Set.Empty, calc = [], errpatts = [],
18.84 rules =
18.85 [Rule.Thm ("rat_mult_poly_l",ThmC.numerals_to_Free @{thm rat_mult_poly_l}),
18.86 @@ -808,7 +809,7 @@
18.87 (*"?x / (?y / ?z) = ?x * ?z / ?y"*)
18.88 Rule.Thm ("divide_divide_eq_left", ThmC.numerals_to_Free @{thm divide_divide_eq_left}),
18.89 (*"?x / ?y / ?z = ?x / (?y * ?z)"*)
18.90 - Rule.Eval ("Rings.divide_class.divide", Prog_Expr.eval_cancel "#divide_e"),
18.91 + \<^rule_eval>\<open>divide\<close> (Prog_Expr.eval_cancel "#divide_e"),
18.92
18.93 Rule.Thm ("rat_power", ThmC.numerals_to_Free @{thm rat_power})
18.94 (*"(?a / ?b) \<up> ?n = ?a \<up> ?n / ?b \<up> ?n"*)
18.95 @@ -913,7 +914,7 @@
18.96 ("#Find" ,["normalform n_n"])],
18.97 {rew_ord'="tless_true", rls' = Rule_Set.empty, calc = [], srls = Rule_Set.empty,
18.98 prls = Rule_Set.append_rules "simplification_of_rationals_prls" Rule_Set.empty
18.99 - [(*for preds in where_*) Rule.Eval ("Rational.is_ratpolyexp", eval_is_ratpolyexp "")],
18.100 + [(*for preds in where_*) \<^rule_eval>\<open>is_ratpolyexp\<close> (eval_is_ratpolyexp "")],
18.101 crls = Rule_Set.empty, errpats = [], nrls = norm_Rational_rls},
18.102 @{thm simplify.simps})]
18.103 \<close> ML \<open>
19.1 --- a/src/Tools/isac/Knowledge/Root.thy Thu Jun 10 17:06:32 2021 +0200
19.2 +++ b/src/Tools/isac/Knowledge/Root.thy Fri Jun 11 11:49:34 2021 +0200
19.3 @@ -163,25 +163,25 @@
19.4 val Root_crls =
19.5 Rule_Set.append_rules "Root_crls" Atools_erls
19.6 [Rule.Thm ("real_unari_minus",ThmC.numerals_to_Free @{thm real_unari_minus}),
19.7 - Rule.Eval ("NthRoot.sqrt" , eval_sqrt "#sqrt_"),
19.8 - Rule.Eval ("Rings.divide_class.divide", Prog_Expr.eval_cancel "#divide_e"),
19.9 - Rule.Eval ("Transcendental.powr" , (**)eval_binop "#power_"),
19.10 - Rule.Eval ("Groups.plus_class.plus", (**)eval_binop "#add_"),
19.11 - Rule.Eval ("Groups.minus_class.minus", (**)eval_binop "#sub_"),
19.12 - Rule.Eval ("Groups.times_class.times", (**)eval_binop "#mult_"),
19.13 - Rule.Eval ("HOL.eq", Prog_Expr.eval_equal "#equal_")
19.14 + \<^rule_eval>\<open>sqrt\<close> (eval_sqrt "#sqrt_"),
19.15 + \<^rule_eval>\<open>divide\<close> (Prog_Expr.eval_cancel "#divide_e"),
19.16 + \<^rule_eval>\<open>powr\<close> (**)(eval_binop "#power_"),
19.17 + \<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_"),
19.18 + \<^rule_eval>\<open>minus\<close> (**)(eval_binop "#sub_"),
19.19 + \<^rule_eval>\<open>times\<close> (**)(eval_binop "#mult_"),
19.20 + \<^rule_eval>\<open>HOL.eq\<close> (Prog_Expr.eval_equal "#equal_")
19.21 ];
19.22
19.23 val Root_erls =
19.24 Rule_Set.append_rules "Root_erls" Atools_erls
19.25 [Rule.Thm ("real_unari_minus",ThmC.numerals_to_Free @{thm real_unari_minus}),
19.26 - Rule.Eval ("NthRoot.sqrt" , eval_sqrt "#sqrt_"),
19.27 - Rule.Eval ("Rings.divide_class.divide", Prog_Expr.eval_cancel "#divide_e"),
19.28 - Rule.Eval ("Transcendental.powr" , (**)eval_binop "#power_"),
19.29 - Rule.Eval ("Groups.plus_class.plus", (**)eval_binop "#add_"),
19.30 - Rule.Eval ("Groups.minus_class.minus", (**)eval_binop "#sub_"),
19.31 - Rule.Eval ("Groups.times_class.times", (**)eval_binop "#mult_"),
19.32 - Rule.Eval ("HOL.eq", Prog_Expr.eval_equal "#equal_")
19.33 + \<^rule_eval>\<open>sqrt\<close> (eval_sqrt "#sqrt_"),
19.34 + \<^rule_eval>\<open>Rings.divide_class.divide\<close> (Prog_Expr.eval_cancel "#divide_e"),
19.35 + \<^rule_eval>\<open>Transcendental.powr\<close> (**)(eval_binop "#power_"),
19.36 + \<^rule_eval>\<open>Groups.plus_class.plus\<close> (**)(eval_binop "#add_"),
19.37 + \<^rule_eval>\<open>Groups.minus_class.minus\<close> (**)(eval_binop "#sub_"),
19.38 + \<^rule_eval>\<open>Groups.times_class.times\<close> (**)(eval_binop "#mult_"),
19.39 + \<^rule_eval>\<open>HOL.eq\<close> (Prog_Expr.eval_equal "#equal_")
19.40 ];
19.41 \<close>
19.42 rule_set_knowledge Root_erls = Root_erls
19.43 @@ -245,9 +245,9 @@
19.44 Rule.Thm ("real_one_collect_assoc",ThmC.numerals_to_Free @{thm real_one_collect_assoc}),
19.45 (*"m is_const ==> k + (n + m * n) = k + (1 + m) * n"*)
19.46
19.47 - Rule.Eval ("Groups.plus_class.plus", (**)eval_binop "#add_"),
19.48 - Rule.Eval ("Groups.times_class.times", (**)eval_binop "#mult_"),
19.49 - Rule.Eval ("Transcendental.powr", (**)eval_binop "#power_")
19.50 + \<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_"),
19.51 + \<^rule_eval>\<open>times\<close> (**)(eval_binop "#mult_"),
19.52 + \<^rule_eval>\<open>powr\<close> (**)(eval_binop "#power_")
19.53 ],
19.54 scr = Rule.Empty_Prog
19.55 });
19.56 @@ -291,12 +291,12 @@
19.57 Rule.Thm ("add_0_left",ThmC.numerals_to_Free @{thm add_0_left}),
19.58 (*"0 + z = z"*)
19.59
19.60 - Rule.Eval ("Groups.plus_class.plus", (**)eval_binop "#add_"),
19.61 - Rule.Eval ("Groups.minus_class.minus", (**)eval_binop "#sub_"),
19.62 - Rule.Eval ("Groups.times_class.times", (**)eval_binop "#mult_"),
19.63 - Rule.Eval ("Rings.divide_class.divide" , Prog_Expr.eval_cancel "#divide_e"),
19.64 - Rule.Eval ("NthRoot.sqrt", eval_sqrt "#sqrt_"),
19.65 - Rule.Eval ("Transcendental.powr", (**)eval_binop "#power_"),
19.66 + \<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_"),
19.67 + \<^rule_eval>\<open>minus\<close> (**)(eval_binop "#sub_"),
19.68 + \<^rule_eval>\<open>times\<close> (**)(eval_binop "#mult_"),
19.69 + \<^rule_eval>\<open>divide\<close> (Prog_Expr.eval_cancel "#divide_e"),
19.70 + \<^rule_eval>\<open>sqrt\<close> (eval_sqrt "#sqrt_"),
19.71 + \<^rule_eval>\<open>powr\<close> (**)(eval_binop "#power_"),
19.72
19.73 Rule.Thm ("sym_realpow_twoI",
19.74 ThmC.numerals_to_Free (@{thm realpow_twoI} RS @{thm sym})),
19.75 @@ -316,12 +316,12 @@
19.76 Rule.Thm ("real_one_collect_assoc",ThmC.numerals_to_Free @{thm real_one_collect_assoc}),
19.77 (*"m is_const ==> k + (n + m * n) = k + (1 + m) * n"*)
19.78
19.79 - Rule.Eval ("Groups.plus_class.plus", (**)eval_binop "#add_"),
19.80 - Rule.Eval ("Groups.minus_class.minus", (**)eval_binop "#sub_"),
19.81 - Rule.Eval ("Groups.times_class.times", (**)eval_binop "#mult_"),
19.82 - Rule.Eval ("Rings.divide_class.divide", Prog_Expr.eval_cancel "#divide_e"),
19.83 - Rule.Eval ("NthRoot.sqrt", eval_sqrt "#sqrt_"),
19.84 - Rule.Eval ("Transcendental.powr", (**)eval_binop "#power_")
19.85 + \<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_"),
19.86 + \<^rule_eval>\<open>minus\<close> (**)(eval_binop "#sub_"),
19.87 + \<^rule_eval>\<open>times\<close> (**)(eval_binop "#mult_"),
19.88 + \<^rule_eval>\<open>divide\<close> (Prog_Expr.eval_cancel "#divide_e"),
19.89 + \<^rule_eval>\<open>sqrt\<close> (eval_sqrt "#sqrt_"),
19.90 + \<^rule_eval>\<open>powr\<close> (**)(eval_binop "#power_")
19.91 ],
19.92 scr = Rule.Empty_Prog
19.93 });
20.1 --- a/src/Tools/isac/Knowledge/RootEq.thy Thu Jun 10 17:06:32 2021 +0200
20.2 +++ b/src/Tools/isac/Knowledge/RootEq.thy Fri Jun 11 11:49:34 2021 +0200
20.3 @@ -178,14 +178,14 @@
20.4 ML \<open>
20.5 val RootEq_prls =(*15.10.02:just the following order due to subterm evaluation*)
20.6 Rule_Set.append_rules "RootEq_prls" Rule_Set.empty
20.7 - [Rule.Eval ("Prog_Expr.ident", Prog_Expr.eval_ident "#ident_"),
20.8 - Rule.Eval ("Prog_Expr.matches", Prog_Expr.eval_matches ""),
20.9 - Rule.Eval ("Prog_Expr.lhs" , Prog_Expr.eval_lhs ""),
20.10 - Rule.Eval ("Prog_Expr.rhs" , Prog_Expr.eval_rhs ""),
20.11 - Rule.Eval ("RootEq.is_sqrtTerm_in", eval_is_sqrtTerm_in ""),
20.12 - Rule.Eval ("RootEq.is_rootTerm_in", eval_is_rootTerm_in ""),
20.13 - Rule.Eval ("RootEq.is_normSqrtTerm_in", eval_is_normSqrtTerm_in ""),
20.14 - Rule.Eval ("HOL.eq", Prog_Expr.eval_equal "#equal_"),
20.15 + [\<^rule_eval>\<open>Prog_Expr.ident\<close> (Prog_Expr.eval_ident "#ident_"),
20.16 + \<^rule_eval>\<open>Prog_Expr.matches\<close> (Prog_Expr.eval_matches ""),
20.17 + \<^rule_eval>\<open>Prog_Expr.lhs\<close> (Prog_Expr.eval_lhs ""),
20.18 + \<^rule_eval>\<open>Prog_Expr.rhs\<close> (Prog_Expr.eval_rhs ""),
20.19 + \<^rule_eval>\<open>is_sqrtTerm_in\<close> (eval_is_sqrtTerm_in ""),
20.20 + \<^rule_eval>\<open>is_rootTerm_in\<close> (eval_is_rootTerm_in ""),
20.21 + \<^rule_eval>\<open>is_normSqrtTerm_in\<close> (eval_is_normSqrtTerm_in ""),
20.22 + \<^rule_eval>\<open>HOL.eq\<close> (Prog_Expr.eval_equal "#equal_"),
20.23 Rule.Thm ("not_true", ThmC.numerals_to_Free @{thm not_true}),
20.24 Rule.Thm ("not_false", ThmC.numerals_to_Free @{thm not_false}),
20.25 Rule.Thm ("and_true", ThmC.numerals_to_Free @{thm and_true}),
20.26 @@ -204,9 +204,9 @@
20.27
20.28 val rooteq_srls =
20.29 Rule_Set.append_rules "rooteq_srls" Rule_Set.empty
20.30 - [Rule.Eval ("RootEq.is_sqrtTerm_in", eval_is_sqrtTerm_in ""),
20.31 - Rule.Eval ("RootEq.is_normSqrtTerm_in", eval_is_normSqrtTerm_in""),
20.32 - Rule.Eval ("RootEq.is_rootTerm_in", eval_is_rootTerm_in "")];
20.33 + [\<^rule_eval>\<open>is_sqrtTerm_in\<close> (eval_is_sqrtTerm_in ""),
20.34 + \<^rule_eval>\<open>is_normSqrtTerm_in\<close> (eval_is_normSqrtTerm_in""),
20.35 + \<^rule_eval>\<open>is_rootTerm_in\<close> (eval_is_rootTerm_in "")];
20.36 \<close>
20.37 ML \<open>
20.38
20.39 @@ -409,12 +409,12 @@
20.40 (* a+(b+c) = a+b+c *)
20.41 Rule.Thm ("real_assoc_2",ThmC.numerals_to_Free @{thm real_assoc_2}),
20.42 (* a*(b*c) = a*b*c *)
20.43 - Rule.Eval ("Groups.plus_class.plus", (**)eval_binop "#add_"),
20.44 - Rule.Eval ("Groups.minus_class.minus", (**)eval_binop "#sub_"),
20.45 - Rule.Eval ("Groups.times_class.times", (**)eval_binop "#mult_"),
20.46 - Rule.Eval ("Rings.divide_class.divide", Prog_Expr.eval_cancel "#divide_e"),
20.47 - Rule.Eval ("NthRoot.sqrt", eval_sqrt "#sqrt_"),
20.48 - Rule.Eval ("Transcendental.powr" , (**)eval_binop "#power_"),
20.49 + \<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_"),
20.50 + \<^rule_eval>\<open>minus\<close> (**)(eval_binop "#sub_"),
20.51 + \<^rule_eval>\<open>times\<close> (**)(eval_binop "#mult_"),
20.52 + \<^rule_eval>\<open>divide\<close> (Prog_Expr.eval_cancel "#divide_e"),
20.53 + \<^rule_eval>\<open>sqrt\<close> (eval_sqrt "#sqrt_"),
20.54 + \<^rule_eval>\<open>powr\<close> (**)(eval_binop "#power_"),
20.55 Rule.Thm("real_plus_binom_pow2",ThmC.numerals_to_Free @{thm real_plus_binom_pow2}),
20.56 Rule.Thm("real_minus_binom_pow2",ThmC.numerals_to_Free @{thm real_minus_binom_pow2}),
20.57 Rule.Thm("realpow_mul",ThmC.numerals_to_Free @{thm realpow_mul}),
21.1 --- a/src/Tools/isac/Knowledge/RootRat.thy Thu Jun 10 17:06:32 2021 +0200
21.2 +++ b/src/Tools/isac/Knowledge/RootRat.thy Fri Jun 11 11:49:34 2021 +0200
21.3 @@ -20,7 +20,7 @@
21.4 (* 1 * z = z *)
21.5 Rule.Thm ("sym_real_mult_minus1",ThmC.numerals_to_Free (@{thm real_mult_minus1} RS @{thm sym})),
21.6 (* "- z1 = -1 * z1" *)
21.7 - Rule.Eval ("NthRoot.sqrt", eval_sqrt "#sqrt_")
21.8 + \<^rule_eval>\<open>sqrt\<close> (eval_sqrt "#sqrt_")
21.9 ];
21.10
21.11 val prep_rls' = Auto_Prog.prep_rls @{theory};
22.1 --- a/src/Tools/isac/Knowledge/RootRatEq.thy Thu Jun 10 17:06:32 2021 +0200
22.2 +++ b/src/Tools/isac/Knowledge/RootRatEq.thy Fri Jun 11 11:49:34 2021 +0200
22.3 @@ -68,13 +68,13 @@
22.4 ML \<open>
22.5 val RootRatEq_prls =
22.6 Rule_Set.append_rules "RootRatEq_prls" Rule_Set.empty
22.7 - [Rule.Eval ("Prog_Expr.ident", Prog_Expr.eval_ident "#ident_"),
22.8 - Rule.Eval ("Prog_Expr.matches", Prog_Expr.eval_matches ""),
22.9 - Rule.Eval ("Prog_Expr.lhs", Prog_Expr.eval_lhs ""),
22.10 - Rule.Eval ("Prog_Expr.rhs", Prog_Expr.eval_rhs ""),
22.11 - Rule.Eval ("RootEq.is_rootTerm_in", eval_is_rootTerm_in ""),
22.12 - Rule.Eval ("RootRatEq.is_rootRatAddTerm_in", eval_is_rootRatAddTerm_in ""),
22.13 - Rule.Eval ("HOL.eq", Prog_Expr.eval_equal "#equal_"),
22.14 + [\<^rule_eval>\<open>Prog_Expr.ident\<close> (Prog_Expr.eval_ident "#ident_"),
22.15 + \<^rule_eval>\<open>Prog_Expr.matches\<close> (Prog_Expr.eval_matches ""),
22.16 + \<^rule_eval>\<open>Prog_Expr.lhs\<close> (Prog_Expr.eval_lhs ""),
22.17 + \<^rule_eval>\<open>Prog_Expr.rhs\<close> (Prog_Expr.eval_rhs ""),
22.18 + \<^rule_eval>\<open>is_rootTerm_in\<close> (eval_is_rootTerm_in ""),
22.19 + \<^rule_eval>\<open>is_rootRatAddTerm_in\<close> (eval_is_rootRatAddTerm_in ""),
22.20 + \<^rule_eval>\<open>HOL.eq\<close> (Prog_Expr.eval_equal "#equal_"),
22.21 Rule.Thm ("not_true",ThmC.numerals_to_Free @{thm not_true}),
22.22 Rule.Thm ("not_false",ThmC.numerals_to_Free @{thm not_false}),
22.23 Rule.Thm ("and_true",ThmC.numerals_to_Free @{thm and_true}),
23.1 --- a/src/Tools/isac/Knowledge/Test.thy Thu Jun 10 17:06:32 2021 +0200
23.2 +++ b/src/Tools/isac/Knowledge/Test.thy Fri Jun 11 11:49:34 2021 +0200
23.3 @@ -375,17 +375,17 @@
23.4 Rule.Thm ("and_commute",ThmC.numerals_to_Free @{thm and_commute}),
23.5 Rule.Thm ("or_commute",ThmC.numerals_to_Free @{thm or_commute}),
23.6
23.7 - Rule.Eval ("Prog_Expr.is_const", Prog_Expr.eval_const "#is_const_"),
23.8 - Rule.Eval ("Prog_Expr.matches", Prog_Expr.eval_matches ""),
23.9 -
23.10 - Rule.Eval ("Groups.plus_class.plus", (**)eval_binop "#add_"),
23.11 - Rule.Eval ("Groups.times_class.times", (**)eval_binop "#mult_"),
23.12 - Rule.Eval ("Transcendental.powr" , (**)eval_binop "#power_"),
23.13 -
23.14 - Rule.Eval ("Orderings.ord_class.less", Prog_Expr.eval_equ "#less_"),
23.15 - Rule.Eval ("Orderings.ord_class.less_eq", Prog_Expr.eval_equ "#less_equal_"),
23.16 -
23.17 - Rule.Eval ("Prog_Expr.ident", Prog_Expr.eval_ident "#ident_")],
23.18 + \<^rule_eval>\<open>Prog_Expr.is_const\<close> (Prog_Expr.eval_const "#is_const_"),
23.19 + \<^rule_eval>\<open>Prog_Expr.matches\<close> (Prog_Expr.eval_matches ""),
23.20 +
23.21 + \<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_"),
23.22 + \<^rule_eval>\<open>times\<close> (**)(eval_binop "#mult_"),
23.23 + \<^rule_eval>\<open>powr\<close> (**)(eval_binop "#power_"),
23.24 +
23.25 + \<^rule_eval>\<open>less\<close> (Prog_Expr.eval_equ "#less_"),
23.26 + \<^rule_eval>\<open>less_eq\<close> (Prog_Expr.eval_equ "#less_equal_"),
23.27 +
23.28 + \<^rule_eval>\<open>Prog_Expr.ident\<close> (Prog_Expr.eval_ident "#ident_")],
23.29 scr = Rule.Empty_Prog
23.30 };
23.31 \<close>
23.32 @@ -416,21 +416,20 @@
23.33 Rule.Thm ("root_ge0_1",ThmC.numerals_to_Free @{thm root_ge0_1}),
23.34 Rule.Thm ("root_ge0_2",ThmC.numerals_to_Free @{thm root_ge0_2}),
23.35
23.36 - Rule.Eval ("Prog_Expr.is_const", Prog_Expr.eval_const "#is_const_"),
23.37 - Rule.Eval ("Test.contains_root", eval_contains_root "#eval_contains_root"),
23.38 - Rule.Eval ("Prog_Expr.matches", Prog_Expr.eval_matches ""),
23.39 - Rule.Eval ("Test.contains_root",
23.40 - eval_contains_root"#contains_root_"),
23.41 -
23.42 - Rule.Eval ("Groups.plus_class.plus", (**)eval_binop "#add_"),
23.43 - Rule.Eval ("Groups.times_class.times", (**)eval_binop "#mult_"),
23.44 - Rule.Eval ("NthRoot.sqrt", eval_sqrt "#sqrt_"),
23.45 - Rule.Eval ("Transcendental.powr", (**)eval_binop "#power_"),
23.46 -
23.47 - Rule.Eval ("Orderings.ord_class.less", Prog_Expr.eval_equ "#less_"),
23.48 - Rule.Eval ("Orderings.ord_class.less_eq", Prog_Expr.eval_equ "#less_equal_"),
23.49 -
23.50 - Rule.Eval ("Prog_Expr.ident", Prog_Expr.eval_ident "#ident_")],
23.51 + \<^rule_eval>\<open>Prog_Expr.is_const\<close> (Prog_Expr.eval_const "#is_const_"),
23.52 + \<^rule_eval>\<open>contains_root\<close> (eval_contains_root "#eval_contains_root"),
23.53 + \<^rule_eval>\<open>Prog_Expr.matches\<close> (Prog_Expr.eval_matches ""),
23.54 + \<^rule_eval>\<open>contains_root\<close> (eval_contains_root"#contains_root_"),
23.55 +
23.56 + \<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_"),
23.57 + \<^rule_eval>\<open>times\<close> (**)(eval_binop "#mult_"),
23.58 + \<^rule_eval>\<open>sqrt\<close> (eval_sqrt "#sqrt_"),
23.59 + \<^rule_eval>\<open>powr\<close> (**)(eval_binop "#power_"),
23.60 +
23.61 + \<^rule_eval>\<open>less\<close> (Prog_Expr.eval_equ "#less_"),
23.62 + \<^rule_eval>\<open>less_eq\<close> (Prog_Expr.eval_equ "#less_equal_"),
23.63 +
23.64 + \<^rule_eval>\<open>Prog_Expr.ident\<close> (Prog_Expr.eval_ident "#ident_")],
23.65 scr = Rule.Empty_Prog
23.66 };
23.67 \<close>
23.68 @@ -496,10 +495,10 @@
23.69 Rule.Thm ("radd_real_const",ThmC.numerals_to_Free @{thm radd_real_const}),
23.70 (* these 2 rules are invers to distr_div_right wrt. termination.
23.71 thus they MUST be done IMMEDIATELY before calc *)
23.72 - Rule.Eval ("Groups.plus_class.plus", (**)eval_binop "#add_"),
23.73 - Rule.Eval ("Groups.times_class.times", (**)eval_binop "#mult_"),
23.74 - Rule.Eval ("Rings.divide_class.divide", Prog_Expr.eval_cancel "#divide_e"),
23.75 - Rule.Eval ("Transcendental.powr", (**)eval_binop "#power_"),
23.76 + \<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_"),
23.77 + \<^rule_eval>\<open>times\<close> (**)(eval_binop "#mult_"),
23.78 + \<^rule_eval>\<open>divide\<close> (Prog_Expr.eval_cancel "#divide_e"),
23.79 + \<^rule_eval>\<open>powr\<close> (**)(eval_binop "#power_"),
23.80
23.81 Rule.Thm ("rcollect_right",ThmC.numerals_to_Free @{thm rcollect_right}),
23.82 Rule.Thm ("rcollect_one_left",ThmC.numerals_to_Free @{thm rcollect_one_left}),
23.83 @@ -566,7 +565,7 @@
23.84 isolate_bdv = \<open>prep_rls' isolate_bdv\<close> and
23.85 matches = \<open>prep_rls'
23.86 (Rule_Set.append_rules "matches" testerls
23.87 - [Rule.Eval ("Prog_Expr.matches", Prog_Expr.eval_matches "#matches_")])\<close>
23.88 + [\<^rule_eval>\<open>Prog_Expr.matches\<close> (Prog_Expr.eval_matches "#matches_")])\<close>
23.89
23.90
23.91 subsection \<open>problems\<close>
23.92 @@ -660,9 +659,9 @@
23.93 Rule.Thm ("real_one_collect_assoc",ThmC.numerals_to_Free @{thm real_one_collect_assoc}),
23.94 (*"m is_const ==> k + (n + m * n) = k + (1 + m) * n"*)
23.95
23.96 - Rule.Eval ("Groups.plus_class.plus", (**)eval_binop "#add_"),
23.97 - Rule.Eval ("Groups.times_class.times", (**)eval_binop "#mult_"),
23.98 - Rule.Eval ("Transcendental.powr", (**)eval_binop "#power_")
23.99 + \<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_"),
23.100 + \<^rule_eval>\<open>times\<close> (**)(eval_binop "#mult_"),
23.101 + \<^rule_eval>\<open>powr\<close> (**)(eval_binop "#power_")
23.102 ],
23.103 scr = Rule.Empty_Prog(*Rule.Prog ((Thm.term_of o the o (parse thy))
23.104 scr_make_polytest)*)
23.105 @@ -723,9 +722,9 @@
23.106 Rule.Thm ("add_0_left",ThmC.numerals_to_Free @{thm add_0_left}),
23.107 (*"0 + z = z"*)
23.108
23.109 - Rule.Eval ("Groups.plus_class.plus", (**)eval_binop "#add_"),
23.110 - Rule.Eval ("Groups.times_class.times", (**)eval_binop "#mult_"),
23.111 - Rule.Eval ("Transcendental.powr", (**)eval_binop "#power_"),
23.112 + \<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_"),
23.113 + \<^rule_eval>\<open>times\<close> (**)(eval_binop "#mult_"),
23.114 + \<^rule_eval>\<open>powr\<close> (**)(eval_binop "#power_"),
23.115 (*
23.116 Rule.Thm ("mult.commute",ThmC.numerals_to_Free @{thm mult.commute}),
23.117 (*AC-rewriting*)
23.118 @@ -756,9 +755,9 @@
23.119 Rule.Thm ("real_one_collect_assoc",ThmC.numerals_to_Free @{thm real_one_collect_assoc}),
23.120 (*"m is_const ==> k + (n + m * n) = k + (1 + m) * n"*)
23.121
23.122 - Rule.Eval ("Groups.plus_class.plus", (**)eval_binop "#add_"),
23.123 - Rule.Eval ("Groups.times_class.times", (**)eval_binop "#mult_"),
23.124 - Rule.Eval ("Transcendental.powr", (**)eval_binop "#power_")
23.125 + \<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_"),
23.126 + \<^rule_eval>\<open>times\<close> (**)(eval_binop "#mult_"),
23.127 + \<^rule_eval>\<open>powr\<close> (**)(eval_binop "#power_")
23.128 ],
23.129 scr = Rule.Empty_Prog
23.130 (*Program ((Thm.term_of o the o (parse thy)) scr_expand_binomtest)*)
23.131 @@ -810,8 +809,8 @@
23.132 [("#Given" ,["equality e_e", "solveFor v_v"]),
23.133 ("#Where" ,["precond_rootpbl v_v"]),
23.134 ("#Find" ,["solutions v_v'i'"])],
23.135 - Rule_Set.append_rules "contains_root" Rule_Set.empty [Rule.Eval ("Test.contains_root",
23.136 - eval_contains_root "#contains_root_")],
23.137 + Rule_Set.append_rules "contains_root" Rule_Set.empty [\<^rule_eval>\<open>contains_root\<close>
23.138 + (eval_contains_root "#contains_root_")],
23.139 SOME "solve (e_e::bool, v_v)", [["Test", "square_equation"]])),
23.140 (Problem.prep_input @{theory} "pbl_test_uni_norm" [] Problem.id_empty
23.141 (["normalise", "univariate", "equation", "test"],
23.142 @@ -890,9 +889,9 @@
23.143 ("#Find" ,["solutions v_v'i'"])],
23.144 {rew_ord'="e_rew_ord",rls'=tval_rls,
23.145 srls = Rule_Set.append_rules "srls_contains_root" Rule_Set.empty
23.146 - [Rule.Eval ("Test.contains_root", eval_contains_root "")],
23.147 + [\<^rule_eval>\<open>contains_root\<close> (eval_contains_root "")],
23.148 prls = Rule_Set.append_rules "prls_contains_root" Rule_Set.empty
23.149 - [Rule.Eval ("Test.contains_root", eval_contains_root "")],
23.150 + [\<^rule_eval>\<open>contains_root\<close> (eval_contains_root "")],
23.151 calc=[], crls=tval_rls, errpats = [], nrls = Rule_Set.empty (*,asm_rls=[],
23.152 asm_thm=[("square_equation_left", ""), ("square_equation_right", "")]*)},
23.153 @{thm solve_root_equ.simps})]
23.154 @@ -918,7 +917,7 @@
23.155 ("#Find" ,["solutions v_v'i'"])],
23.156 {rew_ord' = "e_rew_ord", rls' = tval_rls, srls = Rule_Set.empty,
23.157 prls = Rule_Set.append_rules "prls_met_test_squ_sub" Rule_Set.empty
23.158 - [Rule.Eval ("Test.precond_rootmet", eval_precond_rootmet "")],
23.159 + [\<^rule_eval>\<open>precond_rootmet\<close> (eval_precond_rootmet "")],
23.160 calc=[], crls=tval_rls, errpats = [], nrls = Test_simplify},
23.161 @{thm minisubpbl.simps})]
23.162 \<close>
23.163 @@ -949,7 +948,7 @@
23.164 ("#Find" ,["solutions v_v'i'"])],
23.165 {rew_ord'="e_rew_ord",rls'=tval_rls,
23.166 srls = Rule_Set.append_rules "srls_contains_root" Rule_Set.empty
23.167 - [Rule.Eval ("Test.contains_root", eval_contains_root"")], prls=Rule_Set.empty, calc=[], crls=tval_rls,
23.168 + [\<^rule_eval>\<open>contains_root\<close> (eval_contains_root"")], prls=Rule_Set.empty, calc=[], crls=tval_rls,
23.169 errpats = [], nrls = Rule_Set.empty(*,asm_rls=[], asm_thm=[("square_equation_left", ""),
23.170 ("square_equation_right", "")]*)},
23.171 @{thm solve_root_equ2.simps})]
23.172 @@ -982,7 +981,7 @@
23.173 ("#Find" ,["solutions v_v'i'"])],
23.174 {rew_ord'="e_rew_ord",rls'=tval_rls,
23.175 srls = Rule_Set.append_rules "srls_contains_root" Rule_Set.empty
23.176 - [Rule.Eval ("Test.contains_root", eval_contains_root"")],
23.177 + [\<^rule_eval>\<open>contains_root\<close> (eval_contains_root"")],
23.178 prls=Rule_Set.empty,calc=[], crls=tval_rls, errpats = [], nrls = Rule_Set.empty(*,asm_rls=[],
23.179 asm_thm=[("square_equation_left", ""), ("square_equation_right", "")]*)},
23.180 @{thm solve_root_equ3.simps})]
23.181 @@ -1015,7 +1014,7 @@
23.182 ("#Find" ,["solutions v_v'i'"])],
23.183 {rew_ord'="e_rew_ord",rls'=tval_rls,
23.184 srls = Rule_Set.append_rules "srls_contains_root" Rule_Set.empty
23.185 - [Rule.Eval ("Test.contains_root", eval_contains_root"")],
23.186 + [\<^rule_eval>\<open>contains_root\<close> (eval_contains_root"")],
23.187 prls=Rule_Set.empty,calc=[], crls=tval_rls, errpats = [], nrls = Rule_Set.empty (*,asm_rls=[],
23.188 asm_thm=[("square_equation_left", ""), ("square_equation_right", "")]*)},
23.189 @{thm solve_root_equ4.simps})]
24.1 --- a/src/Tools/isac/ProgLang/Prog_Expr.thy Thu Jun 10 17:06:32 2021 +0200
24.2 +++ b/src/Tools/isac/ProgLang/Prog_Expr.thy Fri Jun 11 11:49:34 2021 +0200
24.3 @@ -527,7 +527,7 @@
24.4
24.5 subsection \<open>extend rule-set for evaluating pre-conditions and program-expressions\<close>
24.6 ML \<open>
24.7 -val prog_expr = Rule_Set.append_rules "prog_expr" prog_expr [Rule.Eval ("Prog_Expr.rhs", Prog_Expr.eval_rhs "")];
24.8 +val prog_expr = Rule_Set.append_rules "prog_expr" prog_expr [\<^rule_eval>\<open>Prog_Expr.rhs\<close> (Prog_Expr.eval_rhs "")];
24.9 \<close> ML \<open>
24.10 \<close> ML \<open>
24.11 \<close>