1.1 --- a/src/Tools/isac/Knowledge/Diff.thy Thu Mar 15 10:17:44 2018 +0100
1.2 +++ b/src/Tools/isac/Knowledge/Diff.thy Thu Mar 15 12:42:04 2018 +0100
1.3 @@ -100,11 +100,11 @@
1.4
1.5 fun primed (Const (id, T)) = Const (id ^ "'", T)
1.6 | primed (Free (id, T)) = Free (id ^ "'", T)
1.7 - | primed t = error ("primed called with arg = '"^ term2str t ^"'");
1.8 + | primed t = error ("primed called with arg = '"^ Celem.term2str t ^"'");
1.9
1.10 (*("primed", ("Diff.primed", eval_primed "#primed"))*)
1.11 fun eval_primed _ _ (p as (Const ("Diff.primed",_) $ t)) _ =
1.12 - SOME ((term2str p) ^ " = " ^ term2str (primed t),
1.13 + SOME ((Celem.term2str p) ^ " = " ^ Celem.term2str (primed t),
1.14 HOLogic.Trueprop $ (TermC.mk_equality (p, primed t)))
1.15 | eval_primed _ _ _ _ = NONE;
1.16 *}
1.17 @@ -115,129 +115,129 @@
1.18
1.19 (*.converts a term such that differentiation works optimally.*)
1.20 val diff_conv =
1.21 - Rls {id="diff_conv",
1.22 + Celem.Rls {id="diff_conv",
1.23 preconds = [],
1.24 rew_ord = ("termlessI",termlessI),
1.25 - erls = append_rls "erls_diff_conv" e_rls
1.26 - [Calc ("Atools.occurs'_in", eval_occurs_in ""),
1.27 - Thm ("not_true",TermC.num_str @{thm not_true}),
1.28 - Thm ("not_false",TermC.num_str @{thm not_false}),
1.29 - Calc ("Orderings.ord_class.less",eval_equ "#less_"),
1.30 - Thm ("and_true",TermC.num_str @{thm and_true}),
1.31 - Thm ("and_false",TermC.num_str @{thm and_false})
1.32 + erls = Celem.append_rls "erls_diff_conv" Celem.e_rls
1.33 + [Celem.Calc ("Atools.occurs'_in", eval_occurs_in ""),
1.34 + Celem.Thm ("not_true",TermC.num_str @{thm not_true}),
1.35 + Celem.Thm ("not_false",TermC.num_str @{thm not_false}),
1.36 + Celem.Calc ("Orderings.ord_class.less",eval_equ "#less_"),
1.37 + Celem.Thm ("and_true",TermC.num_str @{thm and_true}),
1.38 + Celem.Thm ("and_false",TermC.num_str @{thm and_false})
1.39 ],
1.40 - srls = Erls, calc = [], errpatts = [],
1.41 + srls = Celem.Erls, calc = [], errpatts = [],
1.42 rules =
1.43 - [Thm ("frac_conv", TermC.num_str @{thm frac_conv}),
1.44 + [Celem.Thm ("frac_conv", TermC.num_str @{thm frac_conv}),
1.45 (*"?bdv occurs_in ?b \<Longrightarrow> 0 < ?n \<Longrightarrow> ?a / ?b ^^^ ?n = ?a * ?b ^^^ - ?n"*)
1.46 - Thm ("sqrt_conv_bdv", TermC.num_str @{thm sqrt_conv_bdv}),
1.47 + Celem.Thm ("sqrt_conv_bdv", TermC.num_str @{thm sqrt_conv_bdv}),
1.48 (*"sqrt ?bdv = ?bdv ^^^ (1 / 2)"*)
1.49 - Thm ("sqrt_conv_bdv_n", TermC.num_str @{thm sqrt_conv_bdv_n}),
1.50 + Celem.Thm ("sqrt_conv_bdv_n", TermC.num_str @{thm sqrt_conv_bdv_n}),
1.51 (*"sqrt (?bdv ^^^ ?n) = ?bdv ^^^ (?n / 2)"*)
1.52 - Thm ("sqrt_conv", TermC.num_str @{thm sqrt_conv}),
1.53 + Celem.Thm ("sqrt_conv", TermC.num_str @{thm sqrt_conv}),
1.54 (*"?bdv occurs_in ?u \<Longrightarrow> sqrt ?u = ?u ^^^ (1 / 2)"*)
1.55 - Thm ("root_conv", TermC.num_str @{thm root_conv}),
1.56 + Celem.Thm ("root_conv", TermC.num_str @{thm root_conv}),
1.57 (*"?bdv occurs_in ?u \<Longrightarrow> nroot ?n ?u = ?u ^^^ (1 / ?n)"*)
1.58 - Thm ("realpow_pow_bdv", TermC.num_str @{thm realpow_pow_bdv}),
1.59 + Celem.Thm ("realpow_pow_bdv", TermC.num_str @{thm realpow_pow_bdv}),
1.60 (* "(?bdv ^^^ ?b) ^^^ ?c = ?bdv ^^^ (?b * ?c)"*)
1.61 - Calc ("Groups.times_class.times", eval_binop "#mult_"),
1.62 - Thm ("rat_mult",TermC.num_str @{thm rat_mult}),
1.63 + Celem.Calc ("Groups.times_class.times", eval_binop "#mult_"),
1.64 + Celem.Thm ("rat_mult",TermC.num_str @{thm rat_mult}),
1.65 (*a / b * (c / d) = a * c / (b * d)*)
1.66 - Thm ("times_divide_eq_right",TermC.num_str @{thm times_divide_eq_right}),
1.67 + Celem.Thm ("times_divide_eq_right",TermC.num_str @{thm times_divide_eq_right}),
1.68 (*?x * (?y / ?z) = ?x * ?y / ?z*)
1.69 - Thm ("times_divide_eq_left",TermC.num_str @{thm times_divide_eq_left})
1.70 + Celem.Thm ("times_divide_eq_left",TermC.num_str @{thm times_divide_eq_left})
1.71 (*?y / ?z * ?x = ?y * ?x / ?z*)
1.72 ],
1.73 - scr = EmptyScr};
1.74 + scr = Celem.EmptyScr};
1.75 *}
1.76 ML {*
1.77 (*.beautifies a term after differentiation.*)
1.78 val diff_sym_conv =
1.79 - Rls {id="diff_sym_conv",
1.80 + Celem.Rls {id="diff_sym_conv",
1.81 preconds = [],
1.82 rew_ord = ("termlessI",termlessI),
1.83 - erls = append_rls "erls_diff_sym_conv" e_rls
1.84 - [Calc ("Orderings.ord_class.less",eval_equ "#less_")
1.85 + erls = Celem.append_rls "erls_diff_sym_conv" Celem.e_rls
1.86 + [Celem.Calc ("Orderings.ord_class.less",eval_equ "#less_")
1.87 ],
1.88 - srls = Erls, calc = [], errpatts = [],
1.89 - rules = [Thm ("frac_sym_conv", TermC.num_str @{thm frac_sym_conv}),
1.90 - Thm ("sqrt_sym_conv", TermC.num_str @{thm sqrt_sym_conv}),
1.91 - Thm ("root_sym_conv", TermC.num_str @{thm root_sym_conv}),
1.92 - Thm ("sym_real_mult_minus1",
1.93 + srls = Celem.Erls, calc = [], errpatts = [],
1.94 + rules = [Celem.Thm ("frac_sym_conv", TermC.num_str @{thm frac_sym_conv}),
1.95 + Celem.Thm ("sqrt_sym_conv", TermC.num_str @{thm sqrt_sym_conv}),
1.96 + Celem.Thm ("root_sym_conv", TermC.num_str @{thm root_sym_conv}),
1.97 + Celem.Thm ("sym_real_mult_minus1",
1.98 TermC.num_str (@{thm real_mult_minus1} RS @{thm sym})),
1.99 (*- ?z = "-1 * ?z"*)
1.100 - Thm ("rat_mult",TermC.num_str @{thm rat_mult}),
1.101 + Celem.Thm ("rat_mult",TermC.num_str @{thm rat_mult}),
1.102 (*a / b * (c / d) = a * c / (b * d)*)
1.103 - Thm ("times_divide_eq_right",TermC.num_str @{thm times_divide_eq_right}),
1.104 + Celem.Thm ("times_divide_eq_right",TermC.num_str @{thm times_divide_eq_right}),
1.105 (*?x * (?y / ?z) = ?x * ?y / ?z*)
1.106 - Thm ("times_divide_eq_left",TermC.num_str @{thm times_divide_eq_left}),
1.107 + Celem.Thm ("times_divide_eq_left",TermC.num_str @{thm times_divide_eq_left}),
1.108 (*?y / ?z * ?x = ?y * ?x / ?z*)
1.109 - Calc ("Groups.times_class.times", eval_binop "#mult_")
1.110 + Celem.Calc ("Groups.times_class.times", eval_binop "#mult_")
1.111 ],
1.112 - scr = EmptyScr};
1.113 + scr = Celem.EmptyScr};
1.114
1.115 (*..*)
1.116 val srls_diff =
1.117 - Rls {id="srls_differentiate..",
1.118 + Celem.Rls {id="srls_differentiate..",
1.119 preconds = [],
1.120 rew_ord = ("termlessI",termlessI),
1.121 - erls = e_rls,
1.122 - srls = Erls, calc = [], errpatts = [],
1.123 - rules = [Calc("Tools.lhs", eval_lhs "eval_lhs_"),
1.124 - Calc("Tools.rhs", eval_rhs "eval_rhs_"),
1.125 - Calc("Diff.primed", eval_primed "Diff.primed")
1.126 + erls = Celem.e_rls,
1.127 + srls = Celem.Erls, calc = [], errpatts = [],
1.128 + rules = [Celem.Calc("Tools.lhs", eval_lhs "eval_lhs_"),
1.129 + Celem.Calc("Tools.rhs", eval_rhs "eval_rhs_"),
1.130 + Celem.Calc("Diff.primed", eval_primed "Diff.primed")
1.131 ],
1.132 - scr = EmptyScr};
1.133 + scr = Celem.EmptyScr};
1.134 *}
1.135 ML {*
1.136 (*..*)
1.137 val erls_diff =
1.138 - append_rls "erls_differentiate.." e_rls
1.139 - [Thm ("not_true",TermC.num_str @{thm not_true}),
1.140 - Thm ("not_false",TermC.num_str @{thm not_false}),
1.141 + Celem.append_rls "erls_differentiate.." Celem.e_rls
1.142 + [Celem.Thm ("not_true",TermC.num_str @{thm not_true}),
1.143 + Celem.Thm ("not_false",TermC.num_str @{thm not_false}),
1.144
1.145 - Calc ("Atools.ident",eval_ident "#ident_"),
1.146 - Calc ("Atools.is'_atom",eval_is_atom "#is_atom_"),
1.147 - Calc ("Atools.occurs'_in",eval_occurs_in ""),
1.148 - Calc ("Atools.is'_const",eval_const "#is_const_")
1.149 + Celem.Calc ("Atools.ident",eval_ident "#ident_"),
1.150 + Celem.Calc ("Atools.is'_atom",eval_is_atom "#is_atom_"),
1.151 + Celem.Calc ("Atools.occurs'_in",eval_occurs_in ""),
1.152 + Celem.Calc ("Atools.is'_const",eval_const "#is_const_")
1.153 ];
1.154
1.155 (*.rules for differentiation, _no_ simplification.*)
1.156 val diff_rules =
1.157 - Rls {id="diff_rules", preconds = [], rew_ord = ("termlessI",termlessI),
1.158 - erls = erls_diff, srls = Erls, calc = [], errpatts = [],
1.159 - rules = [Thm ("diff_sum",TermC.num_str @{thm diff_sum}),
1.160 - Thm ("diff_dif",TermC.num_str @{thm diff_dif}),
1.161 - Thm ("diff_prod_const",TermC.num_str @{thm diff_prod_const}),
1.162 - Thm ("diff_prod",TermC.num_str @{thm diff_prod}),
1.163 - Thm ("diff_quot",TermC.num_str @{thm diff_quot}),
1.164 - Thm ("diff_sin",TermC.num_str @{thm diff_sin}),
1.165 - Thm ("diff_sin_chain",TermC.num_str @{thm diff_sin_chain}),
1.166 - Thm ("diff_cos",TermC.num_str @{thm diff_cos}),
1.167 - Thm ("diff_cos_chain",TermC.num_str @{thm diff_cos_chain}),
1.168 - Thm ("diff_pow",TermC.num_str @{thm diff_pow}),
1.169 - Thm ("diff_pow_chain",TermC.num_str @{thm diff_pow_chain}),
1.170 - Thm ("diff_ln",TermC.num_str @{thm diff_ln}),
1.171 - Thm ("diff_ln_chain",TermC.num_str @{thm diff_ln_chain}),
1.172 - Thm ("diff_exp",TermC.num_str @{thm diff_exp}),
1.173 - Thm ("diff_exp_chain",TermC.num_str @{thm diff_exp_chain}),
1.174 + Celem.Rls {id="diff_rules", preconds = [], rew_ord = ("termlessI",termlessI),
1.175 + erls = erls_diff, srls = Celem.Erls, calc = [], errpatts = [],
1.176 + rules = [Celem.Thm ("diff_sum",TermC.num_str @{thm diff_sum}),
1.177 + Celem.Thm ("diff_dif",TermC.num_str @{thm diff_dif}),
1.178 + Celem.Thm ("diff_prod_const",TermC.num_str @{thm diff_prod_const}),
1.179 + Celem.Thm ("diff_prod",TermC.num_str @{thm diff_prod}),
1.180 + Celem.Thm ("diff_quot",TermC.num_str @{thm diff_quot}),
1.181 + Celem.Thm ("diff_sin",TermC.num_str @{thm diff_sin}),
1.182 + Celem.Thm ("diff_sin_chain",TermC.num_str @{thm diff_sin_chain}),
1.183 + Celem.Thm ("diff_cos",TermC.num_str @{thm diff_cos}),
1.184 + Celem.Thm ("diff_cos_chain",TermC.num_str @{thm diff_cos_chain}),
1.185 + Celem.Thm ("diff_pow",TermC.num_str @{thm diff_pow}),
1.186 + Celem.Thm ("diff_pow_chain",TermC.num_str @{thm diff_pow_chain}),
1.187 + Celem.Thm ("diff_ln",TermC.num_str @{thm diff_ln}),
1.188 + Celem.Thm ("diff_ln_chain",TermC.num_str @{thm diff_ln_chain}),
1.189 + Celem.Thm ("diff_exp",TermC.num_str @{thm diff_exp}),
1.190 + Celem.Thm ("diff_exp_chain",TermC.num_str @{thm diff_exp_chain}),
1.191 (*
1.192 - Thm ("diff_sqrt",TermC.num_str @{thm diff_sqrt}),
1.193 - Thm ("diff_sqrt_chain",TermC.num_str @{thm diff_sqrt_chain}),
1.194 + Celem.Thm ("diff_sqrt",TermC.num_str @{thm diff_sqrt}),
1.195 + Celem.Thm ("diff_sqrt_chain",TermC.num_str @{thm diff_sqrt_chain}),
1.196 *)
1.197 - Thm ("diff_const",TermC.num_str @{thm diff_const}),
1.198 - Thm ("diff_var",TermC.num_str @{thm diff_var})
1.199 + Celem.Thm ("diff_const",TermC.num_str @{thm diff_const}),
1.200 + Celem.Thm ("diff_var",TermC.num_str @{thm diff_var})
1.201 ],
1.202 - scr = EmptyScr};
1.203 + scr = Celem.EmptyScr};
1.204 *}
1.205 ML {*
1.206 (*.normalisation for checking user-input.*)
1.207 val norm_diff =
1.208 - Rls
1.209 + Celem.Rls
1.210 {id="norm_diff", preconds = [], rew_ord = ("termlessI",termlessI),
1.211 - erls = Erls, srls = Erls, calc = [], errpatts = [],
1.212 - rules = [Rls_ diff_rules, Rls_ norm_Poly ],
1.213 - scr = EmptyScr};
1.214 + erls = Celem.Erls, srls = Celem.Erls, calc = [], errpatts = [],
1.215 + rules = [Celem.Rls_ diff_rules, Celem.Rls_ norm_Poly ],
1.216 + scr = Celem.EmptyScr};
1.217 *}
1.218 setup {* KEStore_Elems.add_rlss
1.219 [("erls_diff", (Context.theory_name @{theory}, prep_rls' erls_diff)),
1.220 @@ -248,20 +248,20 @@
1.221
1.222 (** problem types **)
1.223 setup {* KEStore_Elems.add_pbts
1.224 - [(Specify.prep_pbt thy "pbl_fun" [] e_pblID (["function"], [], e_rls, NONE, [])),
1.225 - (Specify.prep_pbt thy "pbl_fun_deriv" [] e_pblID
1.226 + [(Specify.prep_pbt thy "pbl_fun" [] Celem.e_pblID (["function"], [], Celem.e_rls, NONE, [])),
1.227 + (Specify.prep_pbt thy "pbl_fun_deriv" [] Celem.e_pblID
1.228 (["derivative_of","function"],
1.229 [("#Given" ,["functionTerm f_f","differentiateFor v_v"]),
1.230 ("#Find" ,["derivative f_f'"])],
1.231 - append_rls "e_rls" e_rls [],
1.232 + Celem.append_rls "xxxe_rlsxxx" Celem.e_rls [],
1.233 SOME "Diff (f_f, v_v)", [["diff","differentiate_on_R"],
1.234 ["diff","after_simplification"]])),
1.235 (*here "named" is used differently from Integration"*)
1.236 - (Specify.prep_pbt thy "pbl_fun_deriv_nam" [] e_pblID
1.237 + (Specify.prep_pbt thy "pbl_fun_deriv_nam" [] Celem.e_pblID
1.238 (["named","derivative_of","function"],
1.239 [("#Given" ,["functionEq f_f","differentiateFor v_v"]),
1.240 ("#Find" ,["derivativeEq f_f'"])],
1.241 - append_rls "e_rls" e_rls [],
1.242 + Celem.append_rls "xxxe_rlsxxx" Celem.e_rls [],
1.243 SOME "Differentiate (f_f, v_v)",
1.244 [["diff","differentiate_equality"]]))] *}
1.245
1.246 @@ -281,16 +281,16 @@
1.247 | argl2dtss _ = error "Diff.ML: wrong argument for argl2dtss";
1.248 *}
1.249 setup {* KEStore_Elems.add_mets
1.250 - [Specify.prep_met thy "met_diff" [] e_metID
1.251 + [Specify.prep_met thy "met_diff" [] Celem.e_metID
1.252 (["diff"], [],
1.253 - {rew_ord'="tless_true",rls'=Atools_erls,calc = [], srls = e_rls, prls=e_rls,
1.254 + {rew_ord'="tless_true",rls'=Atools_erls,calc = [], srls = Celem.e_rls, prls=Celem.e_rls,
1.255 crls = Atools_erls, errpats = [], nrls = norm_diff},
1.256 "empty_script"),
1.257 - Specify.prep_met thy "met_diff_onR" [] e_metID
1.258 + Specify.prep_met thy "met_diff_onR" [] Celem.e_metID
1.259 (["diff","differentiate_on_R"],
1.260 [("#Given" ,["functionTerm f_f","differentiateFor v_v"]),
1.261 ("#Find" ,["derivative f_f'"])],
1.262 - {rew_ord'="tless_true", rls' = erls_diff, calc = [], srls = e_rls, prls=e_rls,
1.263 + {rew_ord'="tless_true", rls' = erls_diff, calc = [], srls = Celem.e_rls, prls=Celem.e_rls,
1.264 crls = Atools_erls, errpats = [], nrls = norm_diff},
1.265 "Script DiffScr (f_f::real) (v_v::real) = " ^
1.266 " (let f_f' = Take (d_d v_v f_f) " ^
1.267 @@ -314,11 +314,11 @@
1.268 " (Repeat (Rewrite_Inst [(bdv,v_v)] diff_var False)) Or " ^
1.269 " (Repeat (Rewrite_Set make_polynomial False)))) @@ " ^
1.270 " (Try (Rewrite_Set_Inst [(bdv,v_v)] diff_sym_conv False)))) f_f')"),
1.271 - Specify.prep_met thy "met_diff_simpl" [] e_metID
1.272 + Specify.prep_met thy "met_diff_simpl" [] Celem.e_metID
1.273 (["diff","diff_simpl"],
1.274 [("#Given", ["functionTerm f_f","differentiateFor v_v"]),
1.275 ("#Find" , ["derivative f_f'"])],
1.276 - {rew_ord'="tless_true", rls' = erls_diff, calc = [], srls = e_rls, prls=e_rls,
1.277 + {rew_ord'="tless_true", rls' = erls_diff, calc = [], srls = Celem.e_rls, prls=Celem.e_rls,
1.278 crls = Atools_erls, errpats = [], nrls = norm_diff},
1.279 "Script DiffScr (f_f::real) (v_v::real) = " ^
1.280 " (let f_f' = Take (d_d v_v f_f) " ^
1.281 @@ -342,11 +342,11 @@
1.282 " (Repeat (Rewrite_Inst [(bdv,v_v)] diff_var False)) Or " ^
1.283 " (Repeat (Rewrite_Set make_polynomial False)))) " ^
1.284 " )) f_f')"),
1.285 - Specify.prep_met thy "met_diff_equ" [] e_metID
1.286 + Specify.prep_met thy "met_diff_equ" [] Celem.e_metID
1.287 (["diff","differentiate_equality"],
1.288 [("#Given" ,["functionEq f_f","differentiateFor v_v"]),
1.289 ("#Find" ,["derivativeEq f_f'"])],
1.290 - {rew_ord'="tless_true", rls' = erls_diff, calc = [], srls = srls_diff, prls=e_rls,
1.291 + {rew_ord'="tless_true", rls' = erls_diff, calc = [], srls = srls_diff, prls=Celem.e_rls,
1.292 crls=Atools_erls, errpats = [], nrls = norm_diff},
1.293 "Script DiffEqScr (f_f::bool) (v_v::real) = " ^
1.294 " (let f_f' = Take ((primed (lhs f_f)) = d_d v_v (rhs f_f)) " ^
1.295 @@ -371,11 +371,11 @@
1.296 " (Repeat (Rewrite_Inst [(bdv,v_v)] diff_var False)) Or " ^
1.297 " (Repeat (Rewrite_Set make_polynomial False)))) @@ " ^
1.298 " (Try (Rewrite_Set_Inst [(bdv,v_v)] diff_sym_conv False)))) f_f')"),
1.299 - Specify.prep_met thy "met_diff_after_simp" [] e_metID
1.300 + Specify.prep_met thy "met_diff_after_simp" [] Celem.e_metID
1.301 (["diff","after_simplification"],
1.302 [("#Given" ,["functionTerm f_f","differentiateFor v_v"]),
1.303 ("#Find" ,["derivative f_f'"])],
1.304 - {rew_ord'="tless_true", rls' = e_rls, calc = [], srls = e_rls, prls=e_rls,
1.305 + {rew_ord'="tless_true", rls' = Celem.e_rls, calc = [], srls = Celem.e_rls, prls=Celem.e_rls,
1.306 crls=Atools_erls, errpats = [], nrls = norm_Rational},
1.307 "Script DiffScr (f_f::real) (v_v::real) = " ^
1.308 " (let f_f' = Take (d_d v_v f_f) " ^