1.1 --- a/src/Tools/isac/Knowledge/Integrate.thy Mon Apr 13 13:27:55 2020 +0200
1.2 +++ b/src/Tools/isac/Knowledge/Integrate.thy Mon Apr 13 15:31:23 2020 +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.Num_Calc ("Prog_Expr.occurs'_in", Prog_Expr.eval_occurs_in "#occurs_in_"),
1.7 - Rule.Thm ("not_true", TermC.num_str @{thm not_true}),
1.8 + Rule.Thm ("not_true", ThmC.numerals_to_Free @{thm not_true}),
1.9 Rule.Thm ("not_false",@{thm not_false})
1.10 ],
1.11 scr = Rule.EmptyScr},
1.12 srls = Rule_Set.Empty, calc = [], errpatts = [],
1.13 rules = [
1.14 - Rule.Thm ("integral_const", TermC.num_str @{thm integral_const}),
1.15 - Rule.Thm ("integral_var", TermC.num_str @{thm integral_var}),
1.16 - Rule.Thm ("integral_add", TermC.num_str @{thm integral_add}),
1.17 - Rule.Thm ("integral_mult", TermC.num_str @{thm integral_mult}),
1.18 - Rule.Thm ("integral_pow", TermC.num_str @{thm integral_pow}),
1.19 + Rule.Thm ("integral_const", ThmC.numerals_to_Free @{thm integral_const}),
1.20 + Rule.Thm ("integral_var", ThmC.numerals_to_Free @{thm integral_var}),
1.21 + Rule.Thm ("integral_add", ThmC.numerals_to_Free @{thm integral_add}),
1.22 + Rule.Thm ("integral_mult", ThmC.numerals_to_Free @{thm integral_mult}),
1.23 + Rule.Thm ("integral_pow", ThmC.numerals_to_Free @{thm integral_pow}),
1.24 Rule.Num_Calc ("Groups.plus_class.plus", (**)eval_binop "#add_")(*for n+1*)
1.25 ],
1.26 scr = Rule.EmptyScr};
1.27 @@ -146,12 +146,12 @@
1.28 rules = [Rule.Num_Calc ("Prog_Expr.matches", Prog_Expr.eval_matches""),
1.29 Rule.Num_Calc ("Integrate.is'_f'_x",
1.30 eval_is_f_x "is_f_x_"),
1.31 - Rule.Thm ("not_true", TermC.num_str @{thm not_true}),
1.32 - Rule.Thm ("not_false", TermC.num_str @{thm not_false})
1.33 + Rule.Thm ("not_true", ThmC.numerals_to_Free @{thm not_true}),
1.34 + Rule.Thm ("not_false", ThmC.numerals_to_Free @{thm not_false})
1.35 ],
1.36 scr = Rule.EmptyScr},
1.37 srls = Rule_Set.Empty, calc = [], errpatts = [],
1.38 - rules = [ (*Rule.Thm ("call_for_new_c", TermC.num_str @{thm call_for_new_c}),*)
1.39 + rules = [ (*Rule.Thm ("call_for_new_c", ThmC.numerals_to_Free @{thm call_for_new_c}),*)
1.40 Rule.Cal1 ("Integrate.add'_new'_c", eval_add_new_c "new_c_")
1.41 ],
1.42 scr = Rule.EmptyScr};
1.43 @@ -174,25 +174,25 @@
1.44 [Rule.Num_Calc ("Poly.is'_polyexp",
1.45 eval_is_polyexp "")],
1.46 srls = Rule_Set.Empty, calc = [], errpatts = [],
1.47 - rules = [Rule.Thm ("rat_mult", TermC.num_str @{thm rat_mult}),
1.48 + rules = [Rule.Thm ("rat_mult", ThmC.numerals_to_Free @{thm rat_mult}),
1.49 (*"?a / ?b * (?c / ?d) = ?a * ?c / (?b * ?d)"*)
1.50 - Rule.Thm ("rat_mult_poly_l", TermC.num_str @{thm rat_mult_poly_l}),
1.51 + Rule.Thm ("rat_mult_poly_l", ThmC.numerals_to_Free @{thm rat_mult_poly_l}),
1.52 (*"?c is_polyexp ==> ?c * (?a / ?b) = ?c * ?a / ?b"*)
1.53 - Rule.Thm ("rat_mult_poly_r", TermC.num_str @{thm rat_mult_poly_r}),
1.54 + Rule.Thm ("rat_mult_poly_r", ThmC.numerals_to_Free @{thm rat_mult_poly_r}),
1.55 (*"?c is_polyexp ==> ?a / ?b * ?c = ?a * ?c / ?b"*)
1.56
1.57 Rule.Thm ("real_divide_divide1_mg",
1.58 - TermC.num_str @{thm real_divide_divide1_mg}),
1.59 + ThmC.numerals_to_Free @{thm real_divide_divide1_mg}),
1.60 (*"y ~= 0 ==> (u / v) / (y / z) = (u * z) / (y * v)"*)
1.61 Rule.Thm ("divide_divide_eq_right",
1.62 - TermC.num_str @{thm divide_divide_eq_right}),
1.63 + ThmC.numerals_to_Free @{thm divide_divide_eq_right}),
1.64 (*"?x / (?y / ?z) = ?x * ?z / ?y"*)
1.65 Rule.Thm ("divide_divide_eq_left",
1.66 - TermC.num_str @{thm divide_divide_eq_left}),
1.67 + ThmC.numerals_to_Free @{thm divide_divide_eq_left}),
1.68 (*"?x / ?y / ?z = ?x / (?y * ?z)"*)
1.69 Rule.Num_Calc ("Rings.divide_class.divide", Prog_Expr.eval_cancel "#divide_e"),
1.70
1.71 - Rule.Thm ("rat_power", TermC.num_str @{thm rat_power})
1.72 + Rule.Thm ("rat_power", ThmC.numerals_to_Free @{thm rat_power})
1.73 (*"(?a / ?b) ^^^ ?n = ?a ^^^ ?n / ?b ^^^ ?n"*)
1.74 ],
1.75 scr = Rule.EmptyScr
1.76 @@ -228,15 +228,15 @@
1.77 val separate_bdv2 =
1.78 Rule_Set.append_rules "separate_bdv2"
1.79 collect_bdv
1.80 - [Rule.Thm ("separate_bdv", TermC.num_str @{thm separate_bdv}),
1.81 + [Rule.Thm ("separate_bdv", ThmC.numerals_to_Free @{thm separate_bdv}),
1.82 (*"?a * ?bdv / ?b = ?a / ?b * ?bdv"*)
1.83 - Rule.Thm ("separate_bdv_n", TermC.num_str @{thm separate_bdv_n}),
1.84 - Rule.Thm ("separate_1_bdv", TermC.num_str @{thm separate_1_bdv}),
1.85 + Rule.Thm ("separate_bdv_n", ThmC.numerals_to_Free @{thm separate_bdv_n}),
1.86 + Rule.Thm ("separate_1_bdv", ThmC.numerals_to_Free @{thm separate_1_bdv}),
1.87 (*"?bdv / ?b = (1 / ?b) * ?bdv"*)
1.88 - Rule.Thm ("separate_1_bdv_n", TermC.num_str @{thm separate_1_bdv_n})(*,
1.89 + Rule.Thm ("separate_1_bdv_n", ThmC.numerals_to_Free @{thm separate_1_bdv_n})(*,
1.90 (*"?bdv ^^^ ?n / ?b = 1 / ?b * ?bdv ^^^ ?n"*)
1.91 *****Rule.Thm ("add_divide_distrib",
1.92 - ***** TermC.num_str @{thm add_divide_distrib})
1.93 + ***** ThmC.numerals_to_Free @{thm add_divide_distrib})
1.94 (*"(?x + ?y) / ?z = ?x / ?z + ?y / ?z"*)----------*)
1.95 ];
1.96 val simplify_Integral =
1.97 @@ -244,9 +244,9 @@
1.98 rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord),
1.99 erls = Atools_erls, srls = Rule_Set.Empty,
1.100 calc = [], errpatts = [],
1.101 - rules = [Rule.Thm ("distrib_right", TermC.num_str @{thm distrib_right}),
1.102 + rules = [Rule.Thm ("distrib_right", ThmC.numerals_to_Free @{thm distrib_right}),
1.103 (*"(?z1.0 + ?z2.0) * ?w = ?z1.0 * ?w + ?z2.0 * ?w"*)
1.104 - Rule.Thm ("add_divide_distrib", TermC.num_str @{thm add_divide_distrib}),
1.105 + Rule.Thm ("add_divide_distrib", ThmC.numerals_to_Free @{thm add_divide_distrib}),
1.106 (*"(?x + ?y) / ?z = ?x / ?z + ?y / ?z"*)
1.107 (*^^^^^ *1* ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^*)
1.108 Rule.Rls_ norm_Rational_noadd_fractions,
1.109 @@ -275,21 +275,21 @@
1.110 * Rule.Rls_ simplify_power,
1.111 * Rule.Rls_ collect_numerals,
1.112 * Rule.Rls_ reduce_012,
1.113 -* Rule.Thm ("realpow_oneI", TermC.num_str @{thm realpow_oneI}),
1.114 +* Rule.Thm ("realpow_oneI", ThmC.numerals_to_Free @{thm realpow_oneI}),
1.115 * Rule.Rls_ discard_parentheses,
1.116 * Rule.Rls_ collect_bdv,
1.117 * (*below inserted from 'make_ratpoly_in'*)
1.118 * Rule.Rls_ (Rule_Set.append_rules "separate_bdv"
1.119 * collect_bdv
1.120 -* [Rule.Thm ("separate_bdv", TermC.num_str @{thm separate_bdv}),
1.121 +* [Rule.Thm ("separate_bdv", ThmC.numerals_to_Free @{thm separate_bdv}),
1.122 * (*"?a * ?bdv / ?b = ?a / ?b * ?bdv"*)
1.123 -* Rule.Thm ("separate_bdv_n", TermC.num_str @{thm separate_bdv_n}),
1.124 -* Rule.Thm ("separate_1_bdv", TermC.num_str @{thm separate_1_bdv}),
1.125 +* Rule.Thm ("separate_bdv_n", ThmC.numerals_to_Free @{thm separate_bdv_n}),
1.126 +* Rule.Thm ("separate_1_bdv", ThmC.numerals_to_Free @{thm separate_1_bdv}),
1.127 * (*"?bdv / ?b = (1 / ?b) * ?bdv"*)
1.128 -* Rule.Thm ("separate_1_bdv_n", TermC.num_str @{thm separate_1_bdv_n})(*,
1.129 +* Rule.Thm ("separate_1_bdv_n", ThmC.numerals_to_Free @{thm separate_1_bdv_n})(*,
1.130 * (*"?bdv ^^^ ?n / ?b = 1 / ?b * ?bdv ^^^ ?n"*)
1.131 * Rule.Thm ("add_divide_distrib",
1.132 -* TermC.num_str @{thm add_divide_distrib})
1.133 +* ThmC.numerals_to_Free @{thm add_divide_distrib})
1.134 * (*"(?x + ?y) / ?z = ?x / ?z + ?y / ?z"*)*)
1.135 * ]),
1.136 * Rule.Num_Calc ("Rings.divide_class.divide" , eval_cancel "#divide_e")