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