1.1 --- a/src/Tools/isac/Knowledge/Integrate.thy Sun Feb 25 16:31:17 2018 +0100
1.2 +++ b/src/Tools/isac/Knowledge/Integrate.thy Fri Mar 02 14:19:59 2018 +0100
1.3 @@ -58,14 +58,14 @@
1.4 let fun selc var =
1.5 case (Symbol.explode o id_of) var of
1.6 "c"::[] => true
1.7 - | "c"::"_"::is => (case (int_of_str o implode) is of
1.8 + | "c"::"_"::is => (case (TermC.int_of_str o implode) is of
1.9 SOME _ => true
1.10 | NONE => false)
1.11 | _ => false;
1.12 fun get_coeff c = case (Symbol.explode o id_of) c of
1.13 - "c"::"_"::is => (the o int_of_str o implode) is
1.14 + "c"::"_"::is => (the o TermC.int_of_str o implode) is
1.15 | _ => 0;
1.16 - val cs = filter selc (vars term);
1.17 + val cs = filter selc (TermC.vars term);
1.18 in
1.19 case cs of
1.20 [] => c
1.21 @@ -90,10 +90,10 @@
1.22 fun eval_add_new_c (_:string) "Integrate.add'_new'_c" p (_:theory) =
1.23 let val p' = case p of
1.24 Const ("HOL.eq", T) $ lh $ rh =>
1.25 - Const ("HOL.eq", T) $ lh $ mk_add rh (new_c rh)
1.26 - | p => mk_add p (new_c p)
1.27 + Const ("HOL.eq", T) $ lh $ TermC.mk_add rh (new_c rh)
1.28 + | p => TermC.mk_add p (new_c p)
1.29 in SOME ((term2str p) ^ " = " ^ term2str p',
1.30 - Trueprop $ (mk_equality (p, p')))
1.31 + TermC.Trueprop $ (TermC.mk_equality (p, p')))
1.32 end
1.33 | eval_add_new_c _ _ _ _ = NONE;
1.34
1.35 @@ -101,11 +101,11 @@
1.36 (*("is_f_x", ("Integrate.is'_f'_x", eval_is_f_x "is_f_x_"))*)
1.37 fun eval_is_f_x _ _(p as (Const ("Integrate.is'_f'_x", _)
1.38 $ arg)) _ =
1.39 - if is_f_x arg
1.40 + if TermC.is_f_x arg
1.41 then SOME ((term2str p) ^ " = True",
1.42 - Trueprop $ (mk_equality (p, @{term True})))
1.43 + TermC.Trueprop $ (TermC.mk_equality (p, @{term True})))
1.44 else SOME ((term2str p) ^ " = False",
1.45 - Trueprop $ (mk_equality (p, @{term False})))
1.46 + TermC.Trueprop $ (TermC.mk_equality (p, @{term False})))
1.47 | eval_is_f_x _ _ _ _ = NONE;
1.48 *}
1.49 setup {* KEStore_Elems.add_calcs
1.50 @@ -126,17 +126,17 @@
1.51 rules = [(*for rewriting conditions in Thm's*)
1.52 Calc ("Atools.occurs'_in",
1.53 eval_occurs_in "#occurs_in_"),
1.54 - Thm ("not_true",num_str @{thm not_true}),
1.55 + Thm ("not_true", @{thm not_true}),
1.56 Thm ("not_false",@{thm not_false})
1.57 ],
1.58 scr = EmptyScr},
1.59 srls = Erls, calc = [], errpatts = [],
1.60 rules = [
1.61 - Thm ("integral_const",num_str @{thm integral_const}),
1.62 - Thm ("integral_var",num_str @{thm integral_var}),
1.63 - Thm ("integral_add",num_str @{thm integral_add}),
1.64 - Thm ("integral_mult",num_str @{thm integral_mult}),
1.65 - Thm ("integral_pow",num_str @{thm integral_pow}),
1.66 + Thm ("integral_const", @{thm integral_const}),
1.67 + Thm ("integral_var", @{thm integral_var}),
1.68 + Thm ("integral_add", @{thm integral_add}),
1.69 + Thm ("integral_mult", @{thm integral_mult}),
1.70 + Thm ("integral_pow", @{thm integral_pow}),
1.71 Calc ("Groups.plus_class.plus", eval_binop "#add_")(*for n+1*)
1.72 ],
1.73 scr = EmptyScr};
1.74 @@ -153,12 +153,12 @@
1.75 rules = [Calc ("Tools.matches", eval_matches""),
1.76 Calc ("Integrate.is'_f'_x",
1.77 eval_is_f_x "is_f_x_"),
1.78 - Thm ("not_true",num_str @{thm not_true}),
1.79 - Thm ("not_false",num_str @{thm not_false})
1.80 + Thm ("not_true", @{thm not_true}),
1.81 + Thm ("not_false", @{thm not_false})
1.82 ],
1.83 scr = EmptyScr},
1.84 srls = Erls, calc = [], errpatts = [],
1.85 - rules = [ (*Thm ("call_for_new_c", num_str @{thm call_for_new_c}),*)
1.86 + rules = [ (*Thm ("call_for_new_c", @{thm call_for_new_c}),*)
1.87 Cal1 ("Integrate.add'_new'_c", eval_add_new_c "new_c_")
1.88 ],
1.89 scr = EmptyScr};
1.90 @@ -181,34 +181,34 @@
1.91 [Calc ("Poly.is'_polyexp",
1.92 eval_is_polyexp "")],
1.93 srls = Erls, calc = [], errpatts = [],
1.94 - rules = [Thm ("rat_mult",num_str @{thm rat_mult}),
1.95 + rules = [Thm ("rat_mult", @{thm rat_mult}),
1.96 (*"?a / ?b * (?c / ?d) = ?a * ?c / (?b * ?d)"*)
1.97 - Thm ("rat_mult_poly_l",num_str @{thm rat_mult_poly_l}),
1.98 + Thm ("rat_mult_poly_l", @{thm rat_mult_poly_l}),
1.99 (*"?c is_polyexp ==> ?c * (?a / ?b) = ?c * ?a / ?b"*)
1.100 - Thm ("rat_mult_poly_r",num_str @{thm rat_mult_poly_r}),
1.101 + Thm ("rat_mult_poly_r", @{thm rat_mult_poly_r}),
1.102 (*"?c is_polyexp ==> ?a / ?b * ?c = ?a * ?c / ?b"*)
1.103
1.104 Thm ("real_divide_divide1_mg",
1.105 - num_str @{thm real_divide_divide1_mg}),
1.106 + @{thm real_divide_divide1_mg}),
1.107 (*"y ~= 0 ==> (u / v) / (y / z) = (u * z) / (y * v)"*)
1.108 Thm ("divide_divide_eq_right",
1.109 - num_str @{thm divide_divide_eq_right}),
1.110 + @{thm divide_divide_eq_right}),
1.111 (*"?x / (?y / ?z) = ?x * ?z / ?y"*)
1.112 Thm ("divide_divide_eq_left",
1.113 - num_str @{thm divide_divide_eq_left}),
1.114 + @{thm divide_divide_eq_left}),
1.115 (*"?x / ?y / ?z = ?x / (?y * ?z)"*)
1.116 Calc ("Rings.divide_class.divide" ,eval_cancel "#divide_e"),
1.117
1.118 - Thm ("rat_power", num_str @{thm rat_power})
1.119 + Thm ("rat_power", @{thm rat_power})
1.120 (*"(?a / ?b) ^^^ ?n = ?a ^^^ ?n / ?b ^^^ ?n"*)
1.121 ],
1.122 - scr = Prog ((Thm.term_of o the o (parse thy)) "empty_script")
1.123 + scr = Prog ((Thm.term_of o the o (TermC.parse thy)) "empty_script")
1.124 }),
1.125 Rls_ make_rat_poly_with_parentheses,
1.126 Rls_ cancel_p_rls,(*FIXME:cancel_p does NOT order sometimes*)
1.127 Rls_ rat_reduce_1
1.128 ],
1.129 - scr = Prog ((Thm.term_of o the o (parse thy)) "empty_script")
1.130 + scr = Prog ((Thm.term_of o the o (TermC.parse thy)) "empty_script")
1.131 }:rls;
1.132
1.133 (*.for simplify_Integral adapted from 'norm_Rational'.*)
1.134 @@ -223,7 +223,7 @@
1.135 Rls_ norm_Rational_rls_noadd_fractions,(* the main rls (#) *)
1.136 Rls_ discard_parentheses1 (* mult only *)
1.137 ],
1.138 - scr = Prog ((Thm.term_of o the o (parse thy)) "empty_script")
1.139 + scr = Prog ((Thm.term_of o the o (TermC.parse thy)) "empty_script")
1.140 }:rls;
1.141
1.142 (*.simplify terms before and after Integration such that
1.143 @@ -235,15 +235,15 @@
1.144 val separate_bdv2 =
1.145 append_rls "separate_bdv2"
1.146 collect_bdv
1.147 - [Thm ("separate_bdv", num_str @{thm separate_bdv}),
1.148 + [Thm ("separate_bdv", @{thm separate_bdv}),
1.149 (*"?a * ?bdv / ?b = ?a / ?b * ?bdv"*)
1.150 - Thm ("separate_bdv_n", num_str @{thm separate_bdv_n}),
1.151 - Thm ("separate_1_bdv", num_str @{thm separate_1_bdv}),
1.152 + Thm ("separate_bdv_n", @{thm separate_bdv_n}),
1.153 + Thm ("separate_1_bdv", @{thm separate_1_bdv}),
1.154 (*"?bdv / ?b = (1 / ?b) * ?bdv"*)
1.155 - Thm ("separate_1_bdv_n", num_str @{thm separate_1_bdv_n})(*,
1.156 + Thm ("separate_1_bdv_n", @{thm separate_1_bdv_n})(*,
1.157 (*"?bdv ^^^ ?n / ?b = 1 / ?b * ?bdv ^^^ ?n"*)
1.158 *****Thm ("add_divide_distrib",
1.159 - *****num_str @{thm add_divide_distrib})
1.160 + ***** @{thm add_divide_distrib})
1.161 (*"(?x + ?y) / ?z = ?x / ?z + ?y / ?z"*)----------*)
1.162 ];
1.163 val simplify_Integral =
1.164 @@ -251,9 +251,9 @@
1.165 rew_ord = ("dummy_ord", dummy_ord),
1.166 erls = Atools_erls, srls = Erls,
1.167 calc = [], errpatts = [],
1.168 - rules = [Thm ("distrib_right",num_str @{thm distrib_right}),
1.169 + rules = [Thm ("distrib_right", @{thm distrib_right}),
1.170 (*"(?z1.0 + ?z2.0) * ?w = ?z1.0 * ?w + ?z2.0 * ?w"*)
1.171 - Thm ("add_divide_distrib",num_str @{thm add_divide_distrib}),
1.172 + Thm ("add_divide_distrib", @{thm add_divide_distrib}),
1.173 (*"(?x + ?y) / ?z = ?x / ?z + ?y / ?z"*)
1.174 (*^^^^^ *1* ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^*)
1.175 Rls_ norm_Rational_noadd_fractions,
1.176 @@ -282,21 +282,21 @@
1.177 * Rls_ simplify_power,
1.178 * Rls_ collect_numerals,
1.179 * Rls_ reduce_012,
1.180 -* Thm ("realpow_oneI",num_str @{thm realpow_oneI}),
1.181 +* Thm ("realpow_oneI", @{thm realpow_oneI}),
1.182 * Rls_ discard_parentheses,
1.183 * Rls_ collect_bdv,
1.184 * (*below inserted from 'make_ratpoly_in'*)
1.185 * Rls_ (append_rls "separate_bdv"
1.186 * collect_bdv
1.187 -* [Thm ("separate_bdv", num_str @{thm separate_bdv}),
1.188 +* [Thm ("separate_bdv", @{thm separate_bdv}),
1.189 * (*"?a * ?bdv / ?b = ?a / ?b * ?bdv"*)
1.190 -* Thm ("separate_bdv_n", num_str @{thm separate_bdv_n}),
1.191 -* Thm ("separate_1_bdv", num_str @{thm separate_1_bdv}),
1.192 +* Thm ("separate_bdv_n", @{thm separate_bdv_n}),
1.193 +* Thm ("separate_1_bdv", @{thm separate_1_bdv}),
1.194 * (*"?bdv / ?b = (1 / ?b) * ?bdv"*)
1.195 -* Thm ("separate_1_bdv_n", num_str @{thm separate_1_bdv_n})(*,
1.196 +* Thm ("separate_1_bdv_n", @{thm separate_1_bdv_n})(*,
1.197 * (*"?bdv ^^^ ?n / ?b = 1 / ?b * ?bdv ^^^ ?n"*)
1.198 * Thm ("add_divide_distrib",
1.199 -* num_str @{thm add_divide_distrib})
1.200 +* @{thm add_divide_distrib})
1.201 * (*"(?x + ?y) / ?z = ?x / ?z + ?y / ?z"*)*)
1.202 * ]),
1.203 * Calc ("Rings.divide_class.divide" ,eval_cancel "#divide_e")