1.1 --- a/src/Tools/isac/Knowledge/Rational.thy Thu Jun 10 17:06:32 2021 +0200
1.2 +++ b/src/Tools/isac/Knowledge/Rational.thy Fri Jun 11 11:49:34 2021 +0200
1.3 @@ -394,8 +394,8 @@
1.4 (Rule_Def.Repeat {id = "calc_rat_erls", preconds = [], rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord),
1.5 erls = Rule_Set.empty, srls = Rule_Set.Empty, calc = [], errpatts = [],
1.6 rules =
1.7 - [Rule.Eval ("HOL.eq", Prog_Expr.eval_equal "#equal_"),
1.8 - Rule.Eval ("Prog_Expr.is_const", Prog_Expr.eval_const "#is_const_"),
1.9 + [\<^rule_eval>\<open>HOL.eq\<close> (Prog_Expr.eval_equal "#equal_"),
1.10 + \<^rule_eval>\<open>Prog_Expr.is_const\<close> (Prog_Expr.eval_const "#is_const_"),
1.11 Rule.Thm ("not_true", ThmC.numerals_to_Free @{thm not_true}),
1.12 Rule.Thm ("not_false", ThmC.numerals_to_Free @{thm not_false})],
1.13 scr = Rule.Empty_Prog});
1.14 @@ -409,7 +409,7 @@
1.15 erls = calc_rat_erls, srls = Rule_Set.Empty,
1.16 calc = [], errpatts = [],
1.17 rules =
1.18 - [Rule.Eval ("Rings.divide_class.divide", Prog_Expr.eval_cancel "#divide_e"),
1.19 + [\<^rule_eval>\<open>divide\<close> (Prog_Expr.eval_cancel "#divide_e"),
1.20
1.21 Rule.Thm ("minus_divide_left", ThmC.numerals_to_Free (@{thm minus_divide_left} RS @{thm sym})),
1.22 (*SYM - ?x / ?y = - (?x / ?y) may come from subst*)
1.23 @@ -464,7 +464,7 @@
1.24 val rational_erls =
1.25 Rule_Set.merge "rational_erls" calculate_Rational
1.26 (Rule_Set.append_rules "is_expanded" Atools_erls
1.27 - [Rule.Eval ("Rational.is_expanded", eval_is_expanded "")]);
1.28 + [\<^rule_eval>\<open>is_expanded\<close> (eval_is_expanded "")]);
1.29 \<close>
1.30
1.31 subsection \<open>Embed cancellation into rewriting\<close>
1.32 @@ -604,12 +604,12 @@
1.33 val powers_erls = prep_rls'(
1.34 Rule_Def.Repeat {id = "powers_erls", preconds = [], rew_ord = ("dummy_ord",Rewrite_Ord.dummy_ord),
1.35 erls = Rule_Set.empty, srls = Rule_Set.Empty, calc = [], errpatts = [],
1.36 - rules = [Rule.Eval ("Prog_Expr.is_atom", Prog_Expr.eval_is_atom "#is_atom_"),
1.37 - Rule.Eval ("Prog_Expr.is_even", Prog_Expr.eval_is_even "#is_even_"),
1.38 - Rule.Eval ("Orderings.ord_class.less", Prog_Expr.eval_equ "#less_"),
1.39 + rules = [\<^rule_eval>\<open>Prog_Expr.is_atom\<close> (Prog_Expr.eval_is_atom "#is_atom_"),
1.40 + \<^rule_eval>\<open>Prog_Expr.is_even\<close> (Prog_Expr.eval_is_even "#is_even_"),
1.41 + \<^rule_eval>\<open>less\<close> (Prog_Expr.eval_equ "#less_"),
1.42 Rule.Thm ("not_false", ThmC.numerals_to_Free @{thm not_false}),
1.43 Rule.Thm ("not_true", ThmC.numerals_to_Free @{thm not_true}),
1.44 - Rule.Eval ("Groups.plus_class.plus", (**)eval_binop "#add_")
1.45 + \<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_")
1.46 ],
1.47 scr = Rule.Empty_Prog
1.48 });
1.49 @@ -642,7 +642,7 @@
1.50 (*"[| 1 < n; ~ (r is_atom) |]==>r \<up> n = r * r \<up> (n + -1)"*)
1.51 Rule.Thm ("realpow_eq_oneI",ThmC.numerals_to_Free @{thm realpow_eq_oneI}),
1.52 (*"1 \<up> n = 1"*)
1.53 - Rule.Eval ("Groups.plus_class.plus", (**)eval_binop "#add_")
1.54 + \<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_")
1.55 ],
1.56 scr = Rule.Empty_Prog
1.57 });
1.58 @@ -666,7 +666,7 @@
1.59 Rule.Thm ("divide_divide_eq_left",
1.60 ThmC.numerals_to_Free @{thm divide_divide_eq_left}),
1.61 (*"?x / ?y / ?z = ?x / (?y * ?z)"*)
1.62 - Rule.Eval ("Rings.divide_class.divide", Prog_Expr.eval_cancel "#divide_e")
1.63 + \<^rule_eval>\<open>divide\<close> (Prog_Expr.eval_cancel "#divide_e")
1.64 ],
1.65 scr = Rule.Empty_Prog
1.66 });
1.67 @@ -706,7 +706,7 @@
1.68 val norm_rat_erls = prep_rls'(
1.69 Rule_Def.Repeat {id = "norm_rat_erls", preconds = [], rew_ord = ("dummy_ord",Rewrite_Ord.dummy_ord),
1.70 erls = Rule_Set.empty, srls = Rule_Set.Empty, calc = [], errpatts = [],
1.71 - rules = [Rule.Eval ("Prog_Expr.is_const", Prog_Expr.eval_const "#is_const_")
1.72 + rules = [\<^rule_eval>\<open>Prog_Expr.is_const\<close> (Prog_Expr.eval_const "#is_const_")
1.73 ], scr = Rule.Empty_Prog});
1.74
1.75 (* consists of rls containing the absolute minimum of thms *)
1.76 @@ -778,7 +778,8 @@
1.77 used in initial part norm_Rational_mg, see example DA-M02-main.p.60.*)
1.78 val rat_mult_poly = prep_rls'(
1.79 Rule_Def.Repeat {id = "rat_mult_poly", preconds = [], rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord),
1.80 - erls = Rule_Set.append_rules "Rule_Set.empty-is_polyexp" Rule_Set.empty [Rule.Eval ("Poly.is_polyexp", eval_is_polyexp "")],
1.81 + erls = Rule_Set.append_rules "Rule_Set.empty-is_polyexp" Rule_Set.empty
1.82 + [\<^rule_eval>\<open>is_polyexp\<close> (eval_is_polyexp "")],
1.83 srls = Rule_Set.Empty, calc = [], errpatts = [],
1.84 rules =
1.85 [Rule.Thm ("rat_mult_poly_l",ThmC.numerals_to_Free @{thm rat_mult_poly_l}),
1.86 @@ -808,7 +809,7 @@
1.87 (*"?x / (?y / ?z) = ?x * ?z / ?y"*)
1.88 Rule.Thm ("divide_divide_eq_left", ThmC.numerals_to_Free @{thm divide_divide_eq_left}),
1.89 (*"?x / ?y / ?z = ?x / (?y * ?z)"*)
1.90 - Rule.Eval ("Rings.divide_class.divide", Prog_Expr.eval_cancel "#divide_e"),
1.91 + \<^rule_eval>\<open>divide\<close> (Prog_Expr.eval_cancel "#divide_e"),
1.92
1.93 Rule.Thm ("rat_power", ThmC.numerals_to_Free @{thm rat_power})
1.94 (*"(?a / ?b) \<up> ?n = ?a \<up> ?n / ?b \<up> ?n"*)
1.95 @@ -913,7 +914,7 @@
1.96 ("#Find" ,["normalform n_n"])],
1.97 {rew_ord'="tless_true", rls' = Rule_Set.empty, calc = [], srls = Rule_Set.empty,
1.98 prls = Rule_Set.append_rules "simplification_of_rationals_prls" Rule_Set.empty
1.99 - [(*for preds in where_*) Rule.Eval ("Rational.is_ratpolyexp", eval_is_ratpolyexp "")],
1.100 + [(*for preds in where_*) \<^rule_eval>\<open>is_ratpolyexp\<close> (eval_is_ratpolyexp "")],
1.101 crls = Rule_Set.empty, errpats = [], nrls = norm_Rational_rls},
1.102 @{thm simplify.simps})]
1.103 \<close> ML \<open>