diff -r 47877d6fa35a -r 627d25067f2f src/Tools/isac/Knowledge/Integrate.thy --- a/src/Tools/isac/Knowledge/Integrate.thy Sun Feb 25 16:31:17 2018 +0100 +++ b/src/Tools/isac/Knowledge/Integrate.thy Fri Mar 02 14:19:59 2018 +0100 @@ -58,14 +58,14 @@ let fun selc var = case (Symbol.explode o id_of) var of "c"::[] => true - | "c"::"_"::is => (case (int_of_str o implode) is of + | "c"::"_"::is => (case (TermC.int_of_str o implode) is of SOME _ => true | NONE => false) | _ => false; fun get_coeff c = case (Symbol.explode o id_of) c of - "c"::"_"::is => (the o int_of_str o implode) is + "c"::"_"::is => (the o TermC.int_of_str o implode) is | _ => 0; - val cs = filter selc (vars term); + val cs = filter selc (TermC.vars term); in case cs of [] => c @@ -90,10 +90,10 @@ fun eval_add_new_c (_:string) "Integrate.add'_new'_c" p (_:theory) = let val p' = case p of Const ("HOL.eq", T) $ lh $ rh => - Const ("HOL.eq", T) $ lh $ mk_add rh (new_c rh) - | p => mk_add p (new_c p) + Const ("HOL.eq", T) $ lh $ TermC.mk_add rh (new_c rh) + | p => TermC.mk_add p (new_c p) in SOME ((term2str p) ^ " = " ^ term2str p', - Trueprop $ (mk_equality (p, p'))) + TermC.Trueprop $ (TermC.mk_equality (p, p'))) end | eval_add_new_c _ _ _ _ = NONE; @@ -101,11 +101,11 @@ (*("is_f_x", ("Integrate.is'_f'_x", eval_is_f_x "is_f_x_"))*) fun eval_is_f_x _ _(p as (Const ("Integrate.is'_f'_x", _) $ arg)) _ = - if is_f_x arg + if TermC.is_f_x arg then SOME ((term2str p) ^ " = True", - Trueprop $ (mk_equality (p, @{term True}))) + TermC.Trueprop $ (TermC.mk_equality (p, @{term True}))) else SOME ((term2str p) ^ " = False", - Trueprop $ (mk_equality (p, @{term False}))) + TermC.Trueprop $ (TermC.mk_equality (p, @{term False}))) | eval_is_f_x _ _ _ _ = NONE; *} setup {* KEStore_Elems.add_calcs @@ -126,17 +126,17 @@ rules = [(*for rewriting conditions in Thm's*) Calc ("Atools.occurs'_in", eval_occurs_in "#occurs_in_"), - Thm ("not_true",num_str @{thm not_true}), + Thm ("not_true", @{thm not_true}), Thm ("not_false",@{thm not_false}) ], scr = EmptyScr}, srls = Erls, calc = [], errpatts = [], rules = [ - Thm ("integral_const",num_str @{thm integral_const}), - Thm ("integral_var",num_str @{thm integral_var}), - Thm ("integral_add",num_str @{thm integral_add}), - Thm ("integral_mult",num_str @{thm integral_mult}), - Thm ("integral_pow",num_str @{thm integral_pow}), + Thm ("integral_const", @{thm integral_const}), + Thm ("integral_var", @{thm integral_var}), + Thm ("integral_add", @{thm integral_add}), + Thm ("integral_mult", @{thm integral_mult}), + Thm ("integral_pow", @{thm integral_pow}), Calc ("Groups.plus_class.plus", eval_binop "#add_")(*for n+1*) ], scr = EmptyScr}; @@ -153,12 +153,12 @@ rules = [Calc ("Tools.matches", eval_matches""), Calc ("Integrate.is'_f'_x", eval_is_f_x "is_f_x_"), - Thm ("not_true",num_str @{thm not_true}), - Thm ("not_false",num_str @{thm not_false}) + Thm ("not_true", @{thm not_true}), + Thm ("not_false", @{thm not_false}) ], scr = EmptyScr}, srls = Erls, calc = [], errpatts = [], - rules = [ (*Thm ("call_for_new_c", num_str @{thm call_for_new_c}),*) + rules = [ (*Thm ("call_for_new_c", @{thm call_for_new_c}),*) Cal1 ("Integrate.add'_new'_c", eval_add_new_c "new_c_") ], scr = EmptyScr}; @@ -181,34 +181,34 @@ [Calc ("Poly.is'_polyexp", eval_is_polyexp "")], srls = Erls, calc = [], errpatts = [], - rules = [Thm ("rat_mult",num_str @{thm rat_mult}), + rules = [Thm ("rat_mult", @{thm rat_mult}), (*"?a / ?b * (?c / ?d) = ?a * ?c / (?b * ?d)"*) - Thm ("rat_mult_poly_l",num_str @{thm rat_mult_poly_l}), + Thm ("rat_mult_poly_l", @{thm rat_mult_poly_l}), (*"?c is_polyexp ==> ?c * (?a / ?b) = ?c * ?a / ?b"*) - Thm ("rat_mult_poly_r",num_str @{thm rat_mult_poly_r}), + Thm ("rat_mult_poly_r", @{thm rat_mult_poly_r}), (*"?c is_polyexp ==> ?a / ?b * ?c = ?a * ?c / ?b"*) Thm ("real_divide_divide1_mg", - num_str @{thm real_divide_divide1_mg}), + @{thm real_divide_divide1_mg}), (*"y ~= 0 ==> (u / v) / (y / z) = (u * z) / (y * v)"*) Thm ("divide_divide_eq_right", - num_str @{thm divide_divide_eq_right}), + @{thm divide_divide_eq_right}), (*"?x / (?y / ?z) = ?x * ?z / ?y"*) Thm ("divide_divide_eq_left", - num_str @{thm divide_divide_eq_left}), + @{thm divide_divide_eq_left}), (*"?x / ?y / ?z = ?x / (?y * ?z)"*) Calc ("Rings.divide_class.divide" ,eval_cancel "#divide_e"), - Thm ("rat_power", num_str @{thm rat_power}) + Thm ("rat_power", @{thm rat_power}) (*"(?a / ?b) ^^^ ?n = ?a ^^^ ?n / ?b ^^^ ?n"*) ], - scr = Prog ((Thm.term_of o the o (parse thy)) "empty_script") + scr = Prog ((Thm.term_of o the o (TermC.parse thy)) "empty_script") }), Rls_ make_rat_poly_with_parentheses, Rls_ cancel_p_rls,(*FIXME:cancel_p does NOT order sometimes*) Rls_ rat_reduce_1 ], - scr = Prog ((Thm.term_of o the o (parse thy)) "empty_script") + scr = Prog ((Thm.term_of o the o (TermC.parse thy)) "empty_script") }:rls; (*.for simplify_Integral adapted from 'norm_Rational'.*) @@ -223,7 +223,7 @@ Rls_ norm_Rational_rls_noadd_fractions,(* the main rls (#) *) Rls_ discard_parentheses1 (* mult only *) ], - scr = Prog ((Thm.term_of o the o (parse thy)) "empty_script") + scr = Prog ((Thm.term_of o the o (TermC.parse thy)) "empty_script") }:rls; (*.simplify terms before and after Integration such that @@ -235,15 +235,15 @@ val separate_bdv2 = append_rls "separate_bdv2" collect_bdv - [Thm ("separate_bdv", num_str @{thm separate_bdv}), + [Thm ("separate_bdv", @{thm separate_bdv}), (*"?a * ?bdv / ?b = ?a / ?b * ?bdv"*) - Thm ("separate_bdv_n", num_str @{thm separate_bdv_n}), - Thm ("separate_1_bdv", num_str @{thm separate_1_bdv}), + Thm ("separate_bdv_n", @{thm separate_bdv_n}), + Thm ("separate_1_bdv", @{thm separate_1_bdv}), (*"?bdv / ?b = (1 / ?b) * ?bdv"*) - Thm ("separate_1_bdv_n", num_str @{thm separate_1_bdv_n})(*, + Thm ("separate_1_bdv_n", @{thm separate_1_bdv_n})(*, (*"?bdv ^^^ ?n / ?b = 1 / ?b * ?bdv ^^^ ?n"*) *****Thm ("add_divide_distrib", - *****num_str @{thm add_divide_distrib}) + ***** @{thm add_divide_distrib}) (*"(?x + ?y) / ?z = ?x / ?z + ?y / ?z"*)----------*) ]; val simplify_Integral = @@ -251,9 +251,9 @@ rew_ord = ("dummy_ord", dummy_ord), erls = Atools_erls, srls = Erls, calc = [], errpatts = [], - rules = [Thm ("distrib_right",num_str @{thm distrib_right}), + rules = [Thm ("distrib_right", @{thm distrib_right}), (*"(?z1.0 + ?z2.0) * ?w = ?z1.0 * ?w + ?z2.0 * ?w"*) - Thm ("add_divide_distrib",num_str @{thm add_divide_distrib}), + Thm ("add_divide_distrib", @{thm add_divide_distrib}), (*"(?x + ?y) / ?z = ?x / ?z + ?y / ?z"*) (*^^^^^ *1* ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^*) Rls_ norm_Rational_noadd_fractions, @@ -282,21 +282,21 @@ * Rls_ simplify_power, * Rls_ collect_numerals, * Rls_ reduce_012, -* Thm ("realpow_oneI",num_str @{thm realpow_oneI}), +* Thm ("realpow_oneI", @{thm realpow_oneI}), * Rls_ discard_parentheses, * Rls_ collect_bdv, * (*below inserted from 'make_ratpoly_in'*) * Rls_ (append_rls "separate_bdv" * collect_bdv -* [Thm ("separate_bdv", num_str @{thm separate_bdv}), +* [Thm ("separate_bdv", @{thm separate_bdv}), * (*"?a * ?bdv / ?b = ?a / ?b * ?bdv"*) -* Thm ("separate_bdv_n", num_str @{thm separate_bdv_n}), -* Thm ("separate_1_bdv", num_str @{thm separate_1_bdv}), +* Thm ("separate_bdv_n", @{thm separate_bdv_n}), +* Thm ("separate_1_bdv", @{thm separate_1_bdv}), * (*"?bdv / ?b = (1 / ?b) * ?bdv"*) -* Thm ("separate_1_bdv_n", num_str @{thm separate_1_bdv_n})(*, +* Thm ("separate_1_bdv_n", @{thm separate_1_bdv_n})(*, * (*"?bdv ^^^ ?n / ?b = 1 / ?b * ?bdv ^^^ ?n"*) * Thm ("add_divide_distrib", -* num_str @{thm add_divide_distrib}) +* @{thm add_divide_distrib}) * (*"(?x + ?y) / ?z = ?x / ?z + ?y / ?z"*)*) * ]), * Calc ("Rings.divide_class.divide" ,eval_cancel "#divide_e")