diff -r 0042fe0bc764 -r 82428ca0d23e src/Tools/isac/Knowledge/Integrate.thy --- a/src/Tools/isac/Knowledge/Integrate.thy Mon Apr 13 13:27:55 2020 +0200 +++ b/src/Tools/isac/Knowledge/Integrate.thy Mon Apr 13 15:31:23 2020 +0200 @@ -119,17 +119,17 @@ srls = Rule_Set.Empty, calc = [], errpatts = [], rules = [(*for rewriting conditions in Thm's*) Rule.Num_Calc ("Prog_Expr.occurs'_in", Prog_Expr.eval_occurs_in "#occurs_in_"), - Rule.Thm ("not_true", TermC.num_str @{thm not_true}), + Rule.Thm ("not_true", ThmC.numerals_to_Free @{thm not_true}), Rule.Thm ("not_false",@{thm not_false}) ], scr = Rule.EmptyScr}, srls = Rule_Set.Empty, calc = [], errpatts = [], rules = [ - Rule.Thm ("integral_const", TermC.num_str @{thm integral_const}), - Rule.Thm ("integral_var", TermC.num_str @{thm integral_var}), - Rule.Thm ("integral_add", TermC.num_str @{thm integral_add}), - Rule.Thm ("integral_mult", TermC.num_str @{thm integral_mult}), - Rule.Thm ("integral_pow", TermC.num_str @{thm integral_pow}), + Rule.Thm ("integral_const", ThmC.numerals_to_Free @{thm integral_const}), + Rule.Thm ("integral_var", ThmC.numerals_to_Free @{thm integral_var}), + Rule.Thm ("integral_add", ThmC.numerals_to_Free @{thm integral_add}), + Rule.Thm ("integral_mult", ThmC.numerals_to_Free @{thm integral_mult}), + Rule.Thm ("integral_pow", ThmC.numerals_to_Free @{thm integral_pow}), Rule.Num_Calc ("Groups.plus_class.plus", (**)eval_binop "#add_")(*for n+1*) ], scr = Rule.EmptyScr}; @@ -146,12 +146,12 @@ rules = [Rule.Num_Calc ("Prog_Expr.matches", Prog_Expr.eval_matches""), Rule.Num_Calc ("Integrate.is'_f'_x", eval_is_f_x "is_f_x_"), - Rule.Thm ("not_true", TermC.num_str @{thm not_true}), - Rule.Thm ("not_false", TermC.num_str @{thm not_false}) + Rule.Thm ("not_true", ThmC.numerals_to_Free @{thm not_true}), + Rule.Thm ("not_false", ThmC.numerals_to_Free @{thm not_false}) ], scr = Rule.EmptyScr}, srls = Rule_Set.Empty, calc = [], errpatts = [], - rules = [ (*Rule.Thm ("call_for_new_c", TermC.num_str @{thm call_for_new_c}),*) + rules = [ (*Rule.Thm ("call_for_new_c", ThmC.numerals_to_Free @{thm call_for_new_c}),*) Rule.Cal1 ("Integrate.add'_new'_c", eval_add_new_c "new_c_") ], scr = Rule.EmptyScr}; @@ -174,25 +174,25 @@ [Rule.Num_Calc ("Poly.is'_polyexp", eval_is_polyexp "")], srls = Rule_Set.Empty, calc = [], errpatts = [], - rules = [Rule.Thm ("rat_mult", TermC.num_str @{thm rat_mult}), + rules = [Rule.Thm ("rat_mult", ThmC.numerals_to_Free @{thm rat_mult}), (*"?a / ?b * (?c / ?d) = ?a * ?c / (?b * ?d)"*) - Rule.Thm ("rat_mult_poly_l", TermC.num_str @{thm rat_mult_poly_l}), + Rule.Thm ("rat_mult_poly_l", ThmC.numerals_to_Free @{thm rat_mult_poly_l}), (*"?c is_polyexp ==> ?c * (?a / ?b) = ?c * ?a / ?b"*) - Rule.Thm ("rat_mult_poly_r", TermC.num_str @{thm rat_mult_poly_r}), + Rule.Thm ("rat_mult_poly_r", ThmC.numerals_to_Free @{thm rat_mult_poly_r}), (*"?c is_polyexp ==> ?a / ?b * ?c = ?a * ?c / ?b"*) Rule.Thm ("real_divide_divide1_mg", - TermC.num_str @{thm real_divide_divide1_mg}), + ThmC.numerals_to_Free @{thm real_divide_divide1_mg}), (*"y ~= 0 ==> (u / v) / (y / z) = (u * z) / (y * v)"*) Rule.Thm ("divide_divide_eq_right", - TermC.num_str @{thm divide_divide_eq_right}), + ThmC.numerals_to_Free @{thm divide_divide_eq_right}), (*"?x / (?y / ?z) = ?x * ?z / ?y"*) Rule.Thm ("divide_divide_eq_left", - TermC.num_str @{thm divide_divide_eq_left}), + ThmC.numerals_to_Free @{thm divide_divide_eq_left}), (*"?x / ?y / ?z = ?x / (?y * ?z)"*) Rule.Num_Calc ("Rings.divide_class.divide", Prog_Expr.eval_cancel "#divide_e"), - Rule.Thm ("rat_power", TermC.num_str @{thm rat_power}) + Rule.Thm ("rat_power", ThmC.numerals_to_Free @{thm rat_power}) (*"(?a / ?b) ^^^ ?n = ?a ^^^ ?n / ?b ^^^ ?n"*) ], scr = Rule.EmptyScr @@ -228,15 +228,15 @@ val separate_bdv2 = Rule_Set.append_rules "separate_bdv2" collect_bdv - [Rule.Thm ("separate_bdv", TermC.num_str @{thm separate_bdv}), + [Rule.Thm ("separate_bdv", ThmC.numerals_to_Free @{thm separate_bdv}), (*"?a * ?bdv / ?b = ?a / ?b * ?bdv"*) - Rule.Thm ("separate_bdv_n", TermC.num_str @{thm separate_bdv_n}), - Rule.Thm ("separate_1_bdv", TermC.num_str @{thm separate_1_bdv}), + Rule.Thm ("separate_bdv_n", ThmC.numerals_to_Free @{thm separate_bdv_n}), + Rule.Thm ("separate_1_bdv", ThmC.numerals_to_Free @{thm separate_1_bdv}), (*"?bdv / ?b = (1 / ?b) * ?bdv"*) - Rule.Thm ("separate_1_bdv_n", TermC.num_str @{thm separate_1_bdv_n})(*, + Rule.Thm ("separate_1_bdv_n", ThmC.numerals_to_Free @{thm separate_1_bdv_n})(*, (*"?bdv ^^^ ?n / ?b = 1 / ?b * ?bdv ^^^ ?n"*) *****Rule.Thm ("add_divide_distrib", - ***** TermC.num_str @{thm add_divide_distrib}) + ***** ThmC.numerals_to_Free @{thm add_divide_distrib}) (*"(?x + ?y) / ?z = ?x / ?z + ?y / ?z"*)----------*) ]; val simplify_Integral = @@ -244,9 +244,9 @@ rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord), erls = Atools_erls, srls = Rule_Set.Empty, calc = [], errpatts = [], - rules = [Rule.Thm ("distrib_right", TermC.num_str @{thm distrib_right}), + rules = [Rule.Thm ("distrib_right", ThmC.numerals_to_Free @{thm distrib_right}), (*"(?z1.0 + ?z2.0) * ?w = ?z1.0 * ?w + ?z2.0 * ?w"*) - Rule.Thm ("add_divide_distrib", TermC.num_str @{thm add_divide_distrib}), + Rule.Thm ("add_divide_distrib", ThmC.numerals_to_Free @{thm add_divide_distrib}), (*"(?x + ?y) / ?z = ?x / ?z + ?y / ?z"*) (*^^^^^ *1* ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^*) Rule.Rls_ norm_Rational_noadd_fractions, @@ -275,21 +275,21 @@ * Rule.Rls_ simplify_power, * Rule.Rls_ collect_numerals, * Rule.Rls_ reduce_012, -* Rule.Thm ("realpow_oneI", TermC.num_str @{thm realpow_oneI}), +* Rule.Thm ("realpow_oneI", ThmC.numerals_to_Free @{thm realpow_oneI}), * Rule.Rls_ discard_parentheses, * Rule.Rls_ collect_bdv, * (*below inserted from 'make_ratpoly_in'*) * Rule.Rls_ (Rule_Set.append_rules "separate_bdv" * collect_bdv -* [Rule.Thm ("separate_bdv", TermC.num_str @{thm separate_bdv}), +* [Rule.Thm ("separate_bdv", ThmC.numerals_to_Free @{thm separate_bdv}), * (*"?a * ?bdv / ?b = ?a / ?b * ?bdv"*) -* Rule.Thm ("separate_bdv_n", TermC.num_str @{thm separate_bdv_n}), -* Rule.Thm ("separate_1_bdv", TermC.num_str @{thm separate_1_bdv}), +* Rule.Thm ("separate_bdv_n", ThmC.numerals_to_Free @{thm separate_bdv_n}), +* Rule.Thm ("separate_1_bdv", ThmC.numerals_to_Free @{thm separate_1_bdv}), * (*"?bdv / ?b = (1 / ?b) * ?bdv"*) -* Rule.Thm ("separate_1_bdv_n", TermC.num_str @{thm separate_1_bdv_n})(*, +* Rule.Thm ("separate_1_bdv_n", ThmC.numerals_to_Free @{thm separate_1_bdv_n})(*, * (*"?bdv ^^^ ?n / ?b = 1 / ?b * ?bdv ^^^ ?n"*) * Rule.Thm ("add_divide_distrib", -* TermC.num_str @{thm add_divide_distrib}) +* ThmC.numerals_to_Free @{thm add_divide_distrib}) * (*"(?x + ?y) / ?z = ?x / ?z + ?y / ?z"*)*) * ]), * Rule.Num_Calc ("Rings.divide_class.divide" , eval_cancel "#divide_e")