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