1.1 --- a/src/Tools/isac/Knowledge/Diff.thy Fri Aug 27 10:39:12 2010 +0200
1.2 +++ b/src/Tools/isac/Knowledge/Diff.thy Fri Aug 27 14:56:54 2010 +0200
1.3 @@ -1,13 +1,9 @@
1.4 (* differentiation over the reals
1.5 author: Walther Neuper
1.6 000516
1.7 -
1.8 -remove_thy"Diff";
1.9 -use_thy_only"Knowledge/Diff";
1.10 -use_thy"Knowledge/Isac";
1.11 *)
1.12
1.13 -Diff = Calculus + Trig + LogExp + Rational + Root + Poly + Atools +
1.14 +theory Diff imports Calculus Trig LogExp Rational Root Poly Atools begin
1.15
1.16 consts
1.17
1.18 @@ -37,19 +33,31 @@
1.19 DiffEqScr :: "[bool,real, bool] => bool"
1.20 ("((Script DiffEqScr (_ _ =))// (_))" 9)
1.21
1.22 +text {*a variant of the derivatives defintion:
1.23
1.24 -rules (*stated as axioms, todo: prove as theorems
1.25 + d_d :: "(real => real) => (real => real)"
1.26 +
1.27 + advantages:
1.28 +(1) no variable 'bdv' on the meta-level required
1.29 +(2) chain_rule "d_d (%x. (u (v x))) = (%x. (d_d u)) (v x) * d_d v"
1.30 +(3) and no specialized chain-rules required like
1.31 + diff_sin_chain "d_d bdv (sin u) = cos u * d_d bdv u"
1.32 +
1.33 + disadvantage: d_d (%x. 1 + x^2) = ... differs from high-school notation
1.34 +*}
1.35 +
1.36 +axioms (*stated as axioms, todo: prove as theorems
1.37 'bdv' is a constant on the meta-level *)
1.38 diff_const "[| Not (bdv occurs_in a) |] ==> d_d bdv a = 0"
1.39 diff_var "d_d bdv bdv = 1"
1.40 - diff_prod_const"[| Not (bdv occurs_in u) |] ==> \
1.41 - \d_d bdv (u * v) = u * d_d bdv v"
1.42 + diff_prod_const"[| Not (bdv occurs_in u) |] ==>
1.43 + d_d bdv (u * v) = u * d_d bdv v"
1.44
1.45 diff_sum "d_d bdv (u + v) = d_d bdv u + d_d bdv v"
1.46 diff_dif "d_d bdv (u - v) = d_d bdv u - d_d bdv v"
1.47 diff_prod "d_d bdv (u * v) = d_d bdv u * v + u * d_d bdv v"
1.48 - diff_quot "Not (v = 0) ==> (d_d bdv (u / v) = \
1.49 - \(d_d bdv u * v - u * d_d bdv v) / v ^^^ 2)"
1.50 + diff_quot "Not (v = 0) ==> (d_d bdv (u / v) =
1.51 + (d_d bdv u * v - u * d_d bdv v) / v ^^^ 2)"
1.52
1.53 diff_sin "d_d bdv (sin bdv) = cos bdv"
1.54 diff_sin_chain "d_d bdv (sin u) = cos u * d_d bdv u"
1.55 @@ -67,8 +75,8 @@
1.56 *)
1.57 (*...*)
1.58
1.59 - frac_conv "[| bdv occurs_in b; 0 < n |] ==> \
1.60 - \ a / (b ^^^ n) = a * b ^^^ (-n)"
1.61 + frac_conv "[| bdv occurs_in b; 0 < n |] ==>
1.62 + a / (b ^^^ n) = a * b ^^^ (-n)"
1.63 frac_sym_conv "n < 0 ==> a * b ^^^ n = a / b ^^^ (-n)"
1.64
1.65 sqrt_conv_bdv "sqrt bdv = bdv ^^^ (1 / 2)"
1.66 @@ -81,17 +89,340 @@
1.67
1.68 realpow_pow_bdv "(bdv ^^^ b) ^^^ c = bdv ^^^ (b * c)"
1.69
1.70 +ML {*
1.71 +(** eval functions **)
1.72 +
1.73 +fun primed (Const (id, T)) = Const (id ^ "'", T)
1.74 + | primed (Free (id, T)) = Free (id ^ "'", T)
1.75 + | primed t = raise error ("primed called with arg = '"^ term2str t ^"'");
1.76 +
1.77 +(*("primed", ("Diff.primed", eval_primed "#primed"))*)
1.78 +fun eval_primed _ _ (p as (Const ("Diff.primed",_) $ t)) _ =
1.79 + SOME ((term2str p) ^ " = " ^ term2str (primed t),
1.80 + Trueprop $ (mk_equality (p, primed t)))
1.81 + | eval_primed _ _ _ _ = NONE;
1.82 +
1.83 +calclist':= overwritel (!calclist',
1.84 + [("primed", ("Diff.primed", eval_primed "#primed"))
1.85 + ]);
1.86 +
1.87 +
1.88 +(** rulesets **)
1.89 +
1.90 +(*.converts a term such that differentiation works optimally.*)
1.91 +val diff_conv =
1.92 + Rls {id="diff_conv",
1.93 + preconds = [],
1.94 + rew_ord = ("termlessI",termlessI),
1.95 + erls = append_rls "erls_diff_conv" e_rls
1.96 + [Calc ("Atools.occurs'_in", eval_occurs_in ""),
1.97 + Thm ("not_true",num_str not_true),
1.98 + Thm ("not_false",num_str not_false),
1.99 + Calc ("op <",eval_equ "#less_"),
1.100 + Thm ("and_true",num_str and_true),
1.101 + Thm ("and_false",num_str and_false)
1.102 + ],
1.103 + srls = Erls, calc = [],
1.104 + rules = [Thm ("frac_conv", num_str frac_conv),
1.105 + Thm ("sqrt_conv_bdv", num_str sqrt_conv_bdv),
1.106 + Thm ("sqrt_conv_bdv_n", num_str sqrt_conv_bdv_n),
1.107 + Thm ("sqrt_conv", num_str sqrt_conv),
1.108 + Thm ("root_conv", num_str root_conv),
1.109 + Thm ("realpow_pow_bdv", num_str realpow_pow_bdv),
1.110 + Calc ("op *", eval_binop "#mult_"),
1.111 + Thm ("rat_mult",num_str rat_mult),
1.112 + (*a / b * (c / d) = a * c / (b * d)*)
1.113 + Thm ("real_times_divide1_eq",num_str real_times_divide1_eq),
1.114 + (*?x * (?y / ?z) = ?x * ?y / ?z*)
1.115 + Thm ("real_times_divide2_eq",num_str real_times_divide2_eq)
1.116 + (*?y / ?z * ?x = ?y * ?x / ?z*)
1.117 + (*
1.118 + Thm ("", num_str ),*)
1.119 + ],
1.120 + scr = EmptyScr};
1.121 +
1.122 +(*.beautifies a term after differentiation.*)
1.123 +val diff_sym_conv =
1.124 + Rls {id="diff_sym_conv",
1.125 + preconds = [],
1.126 + rew_ord = ("termlessI",termlessI),
1.127 + erls = append_rls "erls_diff_sym_conv" e_rls
1.128 + [Calc ("op <",eval_equ "#less_")
1.129 + ],
1.130 + srls = Erls, calc = [],
1.131 + rules = [Thm ("frac_sym_conv", num_str frac_sym_conv),
1.132 + Thm ("sqrt_sym_conv", num_str sqrt_sym_conv),
1.133 + Thm ("root_sym_conv", num_str root_sym_conv),
1.134 + Thm ("sym_real_mult_minus1",
1.135 + num_str (real_mult_minus1 RS sym)),
1.136 + (*- ?z = "-1 * ?z"*)
1.137 + Thm ("rat_mult",num_str rat_mult),
1.138 + (*a / b * (c / d) = a * c / (b * d)*)
1.139 + Thm ("real_times_divide1_eq",num_str real_times_divide1_eq),
1.140 + (*?x * (?y / ?z) = ?x * ?y / ?z*)
1.141 + Thm ("real_times_divide2_eq",num_str real_times_divide2_eq),
1.142 + (*?y / ?z * ?x = ?y * ?x / ?z*)
1.143 + Calc ("op *", eval_binop "#mult_")
1.144 + ],
1.145 + scr = EmptyScr};
1.146 +
1.147 +(*..*)
1.148 +val srls_diff =
1.149 + Rls {id="srls_differentiate..",
1.150 + preconds = [],
1.151 + rew_ord = ("termlessI",termlessI),
1.152 + erls = e_rls,
1.153 + srls = Erls, calc = [],
1.154 + rules = [Calc("Tools.lhs", eval_lhs "eval_lhs_"),
1.155 + Calc("Tools.rhs", eval_rhs "eval_rhs_"),
1.156 + Calc("Diff.primed", eval_primed "Diff.primed")
1.157 + ],
1.158 + scr = EmptyScr};
1.159 +
1.160 +(*..*)
1.161 +val erls_diff =
1.162 + append_rls "erls_differentiate.." e_rls
1.163 + [Thm ("not_true",num_str not_true),
1.164 + Thm ("not_false",num_str not_false),
1.165 +
1.166 + Calc ("Atools.ident",eval_ident "#ident_"),
1.167 + Calc ("Atools.is'_atom",eval_is_atom "#is_atom_"),
1.168 + Calc ("Atools.occurs'_in",eval_occurs_in ""),
1.169 + Calc ("Atools.is'_const",eval_const "#is_const_")
1.170 + ];
1.171 +
1.172 +(*.rules for differentiation, _no_ simplification.*)
1.173 +val diff_rules =
1.174 + Rls {id="diff_rules", preconds = [], rew_ord = ("termlessI",termlessI),
1.175 + erls = erls_diff, srls = Erls, calc = [],
1.176 + rules = [Thm ("diff_sum",num_str diff_sum),
1.177 + Thm ("diff_dif",num_str diff_dif),
1.178 + Thm ("diff_prod_const",num_str diff_prod_const),
1.179 + Thm ("diff_prod",num_str diff_prod),
1.180 + Thm ("diff_quot",num_str diff_quot),
1.181 + Thm ("diff_sin",num_str diff_sin),
1.182 + Thm ("diff_sin_chain",num_str diff_sin_chain),
1.183 + Thm ("diff_cos",num_str diff_cos),
1.184 + Thm ("diff_cos_chain",num_str diff_cos_chain),
1.185 + Thm ("diff_pow",num_str diff_pow),
1.186 + Thm ("diff_pow_chain",num_str diff_pow_chain),
1.187 + Thm ("diff_ln",num_str diff_ln),
1.188 + Thm ("diff_ln_chain",num_str diff_ln_chain),
1.189 + Thm ("diff_exp",num_str diff_exp),
1.190 + Thm ("diff_exp_chain",num_str diff_exp_chain),
1.191 +(*
1.192 + Thm ("diff_sqrt",num_str diff_sqrt),
1.193 + Thm ("diff_sqrt_chain",num_str diff_sqrt_chain),
1.194 +*)
1.195 + Thm ("diff_const",num_str diff_const),
1.196 + Thm ("diff_var",num_str diff_var)
1.197 + ],
1.198 + scr = EmptyScr};
1.199 +
1.200 +(*.normalisation for checking user-input.*)
1.201 +val norm_diff =
1.202 + Rls {id="diff_rls", preconds = [], rew_ord = ("termlessI",termlessI),
1.203 + erls = Erls, srls = Erls, calc = [],
1.204 + rules = [Rls_ diff_rules,
1.205 + Rls_ norm_Poly
1.206 + ],
1.207 + scr = EmptyScr};
1.208 +ruleset' :=
1.209 +overwritelthy thy (!ruleset',
1.210 + [("diff_rules", prep_rls norm_diff),
1.211 + ("norm_diff", prep_rls norm_diff),
1.212 + ("diff_conv", prep_rls diff_conv),
1.213 + ("diff_sym_conv", prep_rls diff_sym_conv)
1.214 + ]);
1.215 +
1.216 +
1.217 +(** problem types **)
1.218 +
1.219 +store_pbt
1.220 + (prep_pbt (theory "Diff") "pbl_fun" [] e_pblID
1.221 + (["function"], [], e_rls, NONE, []));
1.222 +
1.223 +store_pbt
1.224 + (prep_pbt (theory "Diff") "pbl_fun_deriv" [] e_pblID
1.225 + (["derivative_of","function"],
1.226 + [("#Given" ,["functionTerm f_","differentiateFor v_"]),
1.227 + ("#Find" ,["derivative f_'_"])
1.228 + ],
1.229 + append_rls "e_rls" e_rls [],
1.230 + SOME "Diff (f_, v_)", [["diff","differentiate_on_R"],
1.231 + ["diff","after_simplification"]]));
1.232 +
1.233 +(*here "named" is used differently from Integration"*)
1.234 +store_pbt
1.235 + (prep_pbt (theory "Diff") "pbl_fun_deriv_nam" [] e_pblID
1.236 + (["named","derivative_of","function"],
1.237 + [("#Given" ,["functionEq f_","differentiateFor v_"]),
1.238 + ("#Find" ,["derivativeEq f_'_"])
1.239 + ],
1.240 + append_rls "e_rls" e_rls [],
1.241 + SOME "Differentiate (f_, v_)", [["diff","differentiate_equality"]]));
1.242 +
1.243 +
1.244 +(** methods **)
1.245 +
1.246 +store_met
1.247 + (prep_met (theory "Diff") "met_diff" [] e_metID
1.248 + (["diff"], [],
1.249 + {rew_ord'="tless_true",rls'=Atools_erls,calc = [], srls = e_rls, prls=e_rls,
1.250 + crls = Atools_erls, nrls = norm_diff}, "empty_script"));
1.251 +
1.252 +store_met
1.253 + (prep_met (theory "Diff") "met_diff_onR" [] e_metID
1.254 + (["diff","differentiate_on_R"],
1.255 + [("#Given" ,["functionTerm f_","differentiateFor v_"]),
1.256 + ("#Find" ,["derivative f_'_"])
1.257 + ],
1.258 + {rew_ord'="tless_true", rls' = erls_diff, calc = [], srls = e_rls,
1.259 + prls=e_rls, crls = Atools_erls, nrls = norm_diff},
1.260 +"Script DiffScr (f_::real) (v_::real) = " ^
1.261 +" (let f'_ = Take (d_d v_ f_) " ^
1.262 +" in (((Try (Rewrite_Set_Inst [(bdv,v_)] diff_conv False)) @@ " ^
1.263 +" (Repeat " ^
1.264 +" ((Repeat (Rewrite_Inst [(bdv,v_)] diff_sum False)) Or " ^
1.265 +" (Repeat (Rewrite_Inst [(bdv,v_)] diff_prod_const False)) Or " ^
1.266 +" (Repeat (Rewrite_Inst [(bdv,v_)] diff_prod False)) Or " ^
1.267 +" (Repeat (Rewrite_Inst [(bdv,v_)] diff_quot True )) Or " ^
1.268 +" (Repeat (Rewrite_Inst [(bdv,v_)] diff_sin False)) Or " ^
1.269 +" (Repeat (Rewrite_Inst [(bdv,v_)] diff_sin_chain False)) Or " ^
1.270 +" (Repeat (Rewrite_Inst [(bdv,v_)] diff_cos False)) Or " ^
1.271 +" (Repeat (Rewrite_Inst [(bdv,v_)] diff_cos_chain False)) Or " ^
1.272 +" (Repeat (Rewrite_Inst [(bdv,v_)] diff_pow False)) Or " ^
1.273 +" (Repeat (Rewrite_Inst [(bdv,v_)] diff_pow_chain False)) Or " ^
1.274 +" (Repeat (Rewrite_Inst [(bdv,v_)] diff_ln False)) Or " ^
1.275 +" (Repeat (Rewrite_Inst [(bdv,v_)] diff_ln_chain False)) Or " ^
1.276 +" (Repeat (Rewrite_Inst [(bdv,v_)] diff_exp False)) Or " ^
1.277 +" (Repeat (Rewrite_Inst [(bdv,v_)] diff_exp_chain False)) Or " ^
1.278 +" (Repeat (Rewrite_Inst [(bdv,v_)] diff_const False)) Or " ^
1.279 +" (Repeat (Rewrite_Inst [(bdv,v_)] diff_var False)) Or " ^
1.280 +" (Repeat (Rewrite_Set make_polynomial False)))) @@ " ^
1.281 +" (Try (Rewrite_Set_Inst [(bdv,v_)] diff_sym_conv False)))) f'_)"
1.282 +));
1.283 +
1.284 +store_met
1.285 + (prep_met (theory "Diff") "met_diff_simpl" [] e_metID
1.286 + (["diff","diff_simpl"],
1.287 + [("#Given" ,["functionTerm f_","differentiateFor v_"]),
1.288 + ("#Find" ,["derivative f_'_"])
1.289 + ],
1.290 + {rew_ord'="tless_true", rls' = erls_diff, calc = [], srls = e_rls,
1.291 + prls=e_rls, crls = Atools_erls, nrls = norm_diff},
1.292 +"Script DiffScr (f_::real) (v_::real) = " ^
1.293 +" (let f'_ = Take (d_d v_ f_) " ^
1.294 +" in (( " ^
1.295 +" (Repeat " ^
1.296 +" ((Repeat (Rewrite_Inst [(bdv,v_)] diff_sum False)) Or " ^
1.297 +" (Repeat (Rewrite_Inst [(bdv,v_)] diff_prod_const False)) Or " ^
1.298 +" (Repeat (Rewrite_Inst [(bdv,v_)] diff_prod False)) Or " ^
1.299 +" (Repeat (Rewrite_Inst [(bdv,v_)] diff_quot True )) Or " ^
1.300 +" (Repeat (Rewrite_Inst [(bdv,v_)] diff_sin False)) Or " ^
1.301 +" (Repeat (Rewrite_Inst [(bdv,v_)] diff_sin_chain False)) Or " ^
1.302 +" (Repeat (Rewrite_Inst [(bdv,v_)] diff_cos False)) Or " ^
1.303 +" (Repeat (Rewrite_Inst [(bdv,v_)] diff_cos_chain False)) Or " ^
1.304 +" (Repeat (Rewrite_Inst [(bdv,v_)] diff_pow False)) Or " ^
1.305 +" (Repeat (Rewrite_Inst [(bdv,v_)] diff_pow_chain False)) Or " ^
1.306 +" (Repeat (Rewrite_Inst [(bdv,v_)] diff_ln False)) Or " ^
1.307 +" (Repeat (Rewrite_Inst [(bdv,v_)] diff_ln_chain False)) Or " ^
1.308 +" (Repeat (Rewrite_Inst [(bdv,v_)] diff_exp False)) Or " ^
1.309 +" (Repeat (Rewrite_Inst [(bdv,v_)] diff_exp_chain False)) Or " ^
1.310 +" (Repeat (Rewrite_Inst [(bdv,v_)] diff_const False)) Or " ^
1.311 +" (Repeat (Rewrite_Inst [(bdv,v_)] diff_var False)) Or " ^
1.312 +" (Repeat (Rewrite_Set make_polynomial False)))) " ^
1.313 +" )) f'_)"
1.314 + ));
1.315 +
1.316 +store_met
1.317 + (prep_met (theory "Diff") "met_diff_equ" [] e_metID
1.318 + (["diff","differentiate_equality"],
1.319 + [("#Given" ,["functionEq f_","differentiateFor v_"]),
1.320 + ("#Find" ,["derivativeEq f_'_"])
1.321 + ],
1.322 + {rew_ord'="tless_true", rls' = erls_diff, calc = [],
1.323 + srls = srls_diff, prls=e_rls, crls=Atools_erls, nrls = norm_diff},
1.324 +"Script DiffEqScr (f_::bool) (v_::real) = " ^
1.325 +" (let f'_ = Take ((primed (lhs f_)) = d_d v_ (rhs f_)) " ^
1.326 +" in (((Try (Rewrite_Set_Inst [(bdv,v_)] diff_conv False)) @@ " ^
1.327 +" (Repeat " ^
1.328 +" ((Repeat (Rewrite_Inst [(bdv,v_)] diff_sum False)) Or " ^
1.329 +" (Repeat (Rewrite_Inst [(bdv,v_)] diff_dif False)) Or " ^
1.330 +" (Repeat (Rewrite_Inst [(bdv,v_)] diff_prod_const False)) Or " ^
1.331 +" (Repeat (Rewrite_Inst [(bdv,v_)] diff_prod False)) Or " ^
1.332 +" (Repeat (Rewrite_Inst [(bdv,v_)] diff_quot True )) Or " ^
1.333 +" (Repeat (Rewrite_Inst [(bdv,v_)] diff_sin False)) Or " ^
1.334 +" (Repeat (Rewrite_Inst [(bdv,v_)] diff_sin_chain False)) Or " ^
1.335 +" (Repeat (Rewrite_Inst [(bdv,v_)] diff_cos False)) Or " ^
1.336 +" (Repeat (Rewrite_Inst [(bdv,v_)] diff_cos_chain False)) Or " ^
1.337 +" (Repeat (Rewrite_Inst [(bdv,v_)] diff_pow False)) Or " ^
1.338 +" (Repeat (Rewrite_Inst [(bdv,v_)] diff_pow_chain False)) Or " ^
1.339 +" (Repeat (Rewrite_Inst [(bdv,v_)] diff_ln False)) Or " ^
1.340 +" (Repeat (Rewrite_Inst [(bdv,v_)] diff_ln_chain False)) Or " ^
1.341 +" (Repeat (Rewrite_Inst [(bdv,v_)] diff_exp False)) Or " ^
1.342 +" (Repeat (Rewrite_Inst [(bdv,v_)] diff_exp_chain False)) Or " ^
1.343 +" (Repeat (Rewrite_Inst [(bdv,v_)] diff_const False)) Or " ^
1.344 +" (Repeat (Rewrite_Inst [(bdv,v_)] diff_var False)) Or " ^
1.345 +" (Repeat (Rewrite_Set make_polynomial False)))) @@ " ^
1.346 +" (Try (Rewrite_Set_Inst [(bdv,v_)] diff_sym_conv False)))) f'_)"
1.347 +));
1.348 +
1.349 +store_met
1.350 + (prep_met (theory "Diff") "met_diff_after_simp" [] e_metID
1.351 + (["diff","after_simplification"],
1.352 + [("#Given" ,["functionTerm f_","differentiateFor v_"]),
1.353 + ("#Find" ,["derivative f_'_"])
1.354 + ],
1.355 + {rew_ord'="tless_true", rls' = e_rls, calc = [], srls = e_rls, prls=e_rls,
1.356 + crls=Atools_erls, nrls = norm_Rational},
1.357 +"Script DiffScr (f_::real) (v_::real) = " ^
1.358 +" (let f'_ = Take (d_d v_ f_) " ^
1.359 +" in ((Try (Rewrite_Set norm_Rational False)) @@ " ^
1.360 +" (Try (Rewrite_Set_Inst [(bdv,v_)] diff_conv False)) @@ " ^
1.361 +" (Try (Rewrite_Set_Inst [(bdv,v_)] norm_diff False)) @@ " ^
1.362 +" (Try (Rewrite_Set_Inst [(bdv,v_)] diff_sym_conv False)) @@ " ^
1.363 +" (Try (Rewrite_Set norm_Rational False))) f'_)"
1.364 +));
1.365 +
1.366 +
1.367 +(** CAS-commands **)
1.368 +
1.369 +(*.handle cas-input like "Diff (a * x^3 + b, x)".*)
1.370 +(* val (t, pairl) = strip_comb (str2term "Diff (a * x^3 + b, x)");
1.371 + val [Const ("Pair", _) $ t $ bdv] = pairl;
1.372 + *)
1.373 +fun argl2dtss [Const ("Pair", _) $ t $ bdv] =
1.374 + [((term_of o the o (parse thy)) "functionTerm", [t]),
1.375 + ((term_of o the o (parse thy)) "differentiateFor", [bdv]),
1.376 + ((term_of o the o (parse thy)) "derivative",
1.377 + [(term_of o the o (parse thy)) "f_'_"])
1.378 + ]
1.379 + | argl2dtss _ = raise error "Diff.ML: wrong argument for argl2dtss";
1.380 +castab :=
1.381 +overwritel (!castab,
1.382 + [((term_of o the o (parse thy)) "Diff",
1.383 + (("Isac.thy", ["derivative_of","function"], ["no_met"]),
1.384 + argl2dtss))
1.385 + ]);
1.386 +
1.387 +(*.handle cas-input like "Differentiate (A = s * (a - s), s)".*)
1.388 +(* val (t, pairl) = strip_comb (str2term "Differentiate (A = s * (a - s), s)");
1.389 + val [Const ("Pair", _) $ t $ bdv] = pairl;
1.390 + *)
1.391 +fun argl2dtss [Const ("Pair", _) $ t $ bdv] =
1.392 + [((term_of o the o (parse thy)) "functionEq", [t]),
1.393 + ((term_of o the o (parse thy)) "differentiateFor", [bdv]),
1.394 + ((term_of o the o (parse thy)) "derivativeEq",
1.395 + [(term_of o the o (parse thy)) "f_'_::bool"])
1.396 + ]
1.397 + | argl2dtss _ = raise error "Diff.ML: wrong argument for argl2dtss";
1.398 +castab :=
1.399 +overwritel (!castab,
1.400 + [((term_of o the o (parse thy)) "Differentiate",
1.401 + (("Isac.thy", ["named","derivative_of","function"], ["no_met"]),
1.402 + argl2dtss))
1.403 + ]);
1.404 +*}
1.405 +
1.406 end
1.407 -
1.408 -(* a variant of the derivatives defintion:
1.409 -
1.410 - d_d :: "(real => real) => (real => real)"
1.411 -
1.412 - advantages:
1.413 -(1) no variable 'bdv' on the meta-level required
1.414 -(2) chain_rule "d_d (%x. (u (v x))) = (%x. (d_d u)) (v x) * d_d v"
1.415 -(3) and no specialized chain-rules required like
1.416 - diff_sin_chain "d_d bdv (sin u) = cos u * d_d bdv u"
1.417 -
1.418 - disadvantage: d_d (%x. 1 + x^2) = ... differs from high-school notation
1.419 -*)