1.1 --- a/src/Tools/isac/Knowledge/Integrate.thy Sat Jun 12 14:29:10 2021 +0200
1.2 +++ b/src/Tools/isac/Knowledge/Integrate.thy Sat Jun 12 18:06:27 2021 +0200
1.3 @@ -119,17 +119,17 @@
1.4 srls = Rule_Set.Empty, calc = [], errpatts = [],
1.5 rules = [(*for rewriting conditions in Thm's*)
1.6 \<^rule_eval>\<open>Prog_Expr.occurs_in\<close> (Prog_Expr.eval_occurs_in "#occurs_in_"),
1.7 - Rule.Thm ("not_true", ThmC.numerals_to_Free @{thm not_true}),
1.8 + \<^rule_thm>\<open>not_true\<close>,
1.9 Rule.Thm ("not_false",@{thm not_false})
1.10 ],
1.11 scr = Rule.Empty_Prog},
1.12 srls = Rule_Set.Empty, calc = [], errpatts = [],
1.13 rules = [
1.14 - Rule.Thm ("integral_const", ThmC.numerals_to_Free @{thm integral_const}),
1.15 - Rule.Thm ("integral_var", ThmC.numerals_to_Free @{thm integral_var}),
1.16 - Rule.Thm ("integral_add", ThmC.numerals_to_Free @{thm integral_add}),
1.17 - Rule.Thm ("integral_mult", ThmC.numerals_to_Free @{thm integral_mult}),
1.18 - Rule.Thm ("integral_pow", ThmC.numerals_to_Free @{thm integral_pow}),
1.19 + \<^rule_thm>\<open>integral_const\<close>,
1.20 + \<^rule_thm>\<open>integral_var\<close>,
1.21 + \<^rule_thm>\<open>integral_add\<close>,
1.22 + \<^rule_thm>\<open>integral_mult\<close>,
1.23 + \<^rule_thm>\<open>integral_pow\<close>,
1.24 \<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_")(*for n+1*)
1.25 ],
1.26 scr = Rule.Empty_Prog};
1.27 @@ -145,12 +145,12 @@
1.28 srls = Rule_Set.Empty, calc = [], errpatts = [],
1.29 rules = [\<^rule_eval>\<open>Prog_Expr.matches\<close> (Prog_Expr.eval_matches""),
1.30 \<^rule_eval>\<open>Integrate.is_f_x\<close> (eval_is_f_x "is_f_x_"),
1.31 - Rule.Thm ("not_true", ThmC.numerals_to_Free @{thm not_true}),
1.32 - Rule.Thm ("not_false", ThmC.numerals_to_Free @{thm not_false})
1.33 + \<^rule_thm>\<open>not_true\<close>,
1.34 + \<^rule_thm>\<open>not_false\<close>
1.35 ],
1.36 scr = Rule.Empty_Prog},
1.37 srls = Rule_Set.Empty, calc = [], errpatts = [],
1.38 - rules = [ (*Rule.Thm ("call_for_new_c", ThmC.numerals_to_Free @{thm call_for_new_c}),*)
1.39 + rules = [ (*\<^rule_thm>\<open>call_for_new_c\<close>,*)
1.40 Rule.Cal1 ("Integrate.add_new_c", eval_add_new_c "new_c_")
1.41 ],
1.42 scr = Rule.Empty_Prog};
1.43 @@ -172,11 +172,11 @@
1.44 Rule_Set.append_rules "Rule_Set.empty-is_polyexp" Rule_Set.empty
1.45 [\<^rule_eval>\<open>is_polyexp\<close> (eval_is_polyexp "")],
1.46 srls = Rule_Set.Empty, calc = [], errpatts = [],
1.47 - rules = [Rule.Thm ("rat_mult", ThmC.numerals_to_Free @{thm rat_mult}),
1.48 + rules = [\<^rule_thm>\<open>rat_mult\<close>,
1.49 (*"?a / ?b * (?c / ?d) = ?a * ?c / (?b * ?d)"*)
1.50 - Rule.Thm ("rat_mult_poly_l", ThmC.numerals_to_Free @{thm rat_mult_poly_l}),
1.51 + \<^rule_thm>\<open>rat_mult_poly_l\<close>,
1.52 (*"?c is_polyexp ==> ?c * (?a / ?b) = ?c * ?a / ?b"*)
1.53 - Rule.Thm ("rat_mult_poly_r", ThmC.numerals_to_Free @{thm rat_mult_poly_r}),
1.54 + \<^rule_thm>\<open>rat_mult_poly_r\<close>,
1.55 (*"?c is_polyexp ==> ?a / ?b * ?c = ?a * ?c / ?b"*)
1.56
1.57 Rule.Thm ("real_divide_divide1_mg",
1.58 @@ -190,7 +190,7 @@
1.59 (*"?x / ?y / ?z = ?x / (?y * ?z)"*)
1.60 \<^rule_eval>\<open>divide\<close> (Prog_Expr.eval_cancel "#divide_e"),
1.61
1.62 - Rule.Thm ("rat_power", ThmC.numerals_to_Free @{thm rat_power})
1.63 + \<^rule_thm>\<open>rat_power\<close>
1.64 (*"(?a / ?b) \<up> ?n = ?a \<up> ?n / ?b \<up> ?n"*)
1.65 ],
1.66 scr = Rule.Empty_Prog
1.67 @@ -226,12 +226,12 @@
1.68 val separate_bdv2 =
1.69 Rule_Set.append_rules "separate_bdv2"
1.70 collect_bdv
1.71 - [Rule.Thm ("separate_bdv", ThmC.numerals_to_Free @{thm separate_bdv}),
1.72 + [\<^rule_thm>\<open>separate_bdv\<close>,
1.73 (*"?a * ?bdv / ?b = ?a / ?b * ?bdv"*)
1.74 - Rule.Thm ("separate_bdv_n", ThmC.numerals_to_Free @{thm separate_bdv_n}),
1.75 - Rule.Thm ("separate_1_bdv", ThmC.numerals_to_Free @{thm separate_1_bdv}),
1.76 + \<^rule_thm>\<open>separate_bdv_n\<close>,
1.77 + \<^rule_thm>\<open>separate_1_bdv\<close>,
1.78 (*"?bdv / ?b = (1 / ?b) * ?bdv"*)
1.79 - Rule.Thm ("separate_1_bdv_n", ThmC.numerals_to_Free @{thm separate_1_bdv_n})(*,
1.80 + \<^rule_thm>\<open>separate_1_bdv_n\<close>(*,
1.81 (*"?bdv \<up> ?n / ?b = 1 / ?b * ?bdv \<up> ?n"*)
1.82 *****Rule.Thm ("add_divide_distrib",
1.83 ***** ThmC.numerals_to_Free @{thm add_divide_distrib})
1.84 @@ -242,9 +242,9 @@
1.85 rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord),
1.86 erls = Atools_erls, srls = Rule_Set.Empty,
1.87 calc = [], errpatts = [],
1.88 - rules = [Rule.Thm ("distrib_right", ThmC.numerals_to_Free @{thm distrib_right}),
1.89 + rules = [\<^rule_thm>\<open>distrib_right\<close>,
1.90 (*"(?z1.0 + ?z2.0) * ?w = ?z1.0 * ?w + ?z2.0 * ?w"*)
1.91 - Rule.Thm ("add_divide_distrib", ThmC.numerals_to_Free @{thm add_divide_distrib}),
1.92 + \<^rule_thm>\<open>add_divide_distrib\<close>,
1.93 (*"(?x + ?y) / ?z = ?x / ?z + ?y / ?z"*)
1.94 (*^^^^^ *1* ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^*)
1.95 Rule.Rls_ norm_Rational_noadd_fractions,
1.96 @@ -273,18 +273,18 @@
1.97 * Rule.Rls_ simplify_power,
1.98 * Rule.Rls_ collect_numerals,
1.99 * Rule.Rls_ reduce_012,
1.100 -* Rule.Thm ("realpow_oneI", ThmC.numerals_to_Free @{thm realpow_oneI}),
1.101 +* \<^rule_thm>\<open>realpow_oneI\<close>,
1.102 * Rule.Rls_ discard_parentheses,
1.103 * Rule.Rls_ collect_bdv,
1.104 * (*below inserted from 'make_ratpoly_in'*)
1.105 * Rule.Rls_ (Rule_Set.append_rules "separate_bdv"
1.106 * collect_bdv
1.107 -* [Rule.Thm ("separate_bdv", ThmC.numerals_to_Free @{thm separate_bdv}),
1.108 +* [\<^rule_thm>\<open>separate_bdv\<close>,
1.109 * (*"?a * ?bdv / ?b = ?a / ?b * ?bdv"*)
1.110 -* Rule.Thm ("separate_bdv_n", ThmC.numerals_to_Free @{thm separate_bdv_n}),
1.111 -* Rule.Thm ("separate_1_bdv", ThmC.numerals_to_Free @{thm separate_1_bdv}),
1.112 +* \<^rule_thm>\<open>separate_bdv_n\<close>,
1.113 +* \<^rule_thm>\<open>separate_1_bdv\<close>,
1.114 * (*"?bdv / ?b = (1 / ?b) * ?bdv"*)
1.115 -* Rule.Thm ("separate_1_bdv_n", ThmC.numerals_to_Free @{thm separate_1_bdv_n})(*,
1.116 +* \<^rule_thm>\<open>separate_1_bdv_n\<close>(*,
1.117 * (*"?bdv \<up> ?n / ?b = 1 / ?b * ?bdv \<up> ?n"*)
1.118 * Rule.Thm ("add_divide_distrib",
1.119 * ThmC.numerals_to_Free @{thm add_divide_distrib})