1.1 --- a/src/Tools/isac/Knowledge/Diff.thy Fri Feb 15 16:52:05 2019 +0100
1.2 +++ b/src/Tools/isac/Knowledge/Diff.thy Tue Feb 19 19:35:12 2019 +0100
1.3 @@ -287,6 +287,30 @@
1.4 crls = Atools_erls, errpats = [], nrls = norm_diff},
1.5 "empty_script")]
1.6 \<close>
1.7 +partial_function (tailrec) differentiate_on_R :: "real \<Rightarrow> real \<Rightarrow> real"
1.8 + where
1.9 +"differentiate_on_R f_f v_v =
1.10 + (let f_f' = Take (d_d v_v f_f)
1.11 + in (((Try (Rewrite_Set_Inst [(''bdv'',v_v)] ''diff_conv'' False)) @@
1.12 + (Repeat
1.13 + ((Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_sum'' False)) Or
1.14 + (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_prod_const'' False)) Or
1.15 + (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_prod'' False)) Or
1.16 + (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_quot'' True )) Or
1.17 + (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_sin'' False)) Or
1.18 + (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_sin_chain'' False)) Or
1.19 + (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_cos'' False)) Or
1.20 + (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_cos_chain'' False)) Or
1.21 + (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_pow'' False)) Or
1.22 + (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_pow_chain'' False)) Or
1.23 + (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_ln'' False)) Or
1.24 + (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_ln_chain'' False)) Or
1.25 + (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_exp'' False)) Or
1.26 + (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_exp_chain'' False)) Or
1.27 + (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_const'' False)) Or
1.28 + (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_var'' False)) Or
1.29 + (Repeat (Rewrite_Set ''make_polynomial'' False)))) @@
1.30 + (Try (Rewrite_Set_Inst [(''bdv'',v_v)] ''diff_sym_conv'' False)))) f_f')"
1.31 setup \<open>KEStore_Elems.add_mets
1.32 [Specify.prep_met thy "met_diff_onR" [] Celem.e_metID
1.33 (["diff","differentiate_on_R"],
1.34 @@ -317,6 +341,30 @@
1.35 " (Repeat (Rewrite_Set ''make_polynomial'' False)))) @@ " ^
1.36 " (Try (Rewrite_Set_Inst [(''bdv'',v_v)] ''diff_sym_conv'' False)))) f_f')")]
1.37 \<close>
1.38 +partial_function (tailrec) differentiateX :: "real \<Rightarrow> real \<Rightarrow> real"
1.39 + where
1.40 +"differentiateX f_f v_v =
1.41 + (let f_f' = Take (d_d v_v f_f)
1.42 + in ((
1.43 + (Repeat
1.44 + ((Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_sum'' False)) Or
1.45 + (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_prod_const'' False)) Or
1.46 + (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_prod'' False)) Or
1.47 + (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_quot'' False)) Or
1.48 + (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_sin'' False)) Or
1.49 + (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_sin_chain'' False)) Or
1.50 + (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_cos'' False)) Or
1.51 + (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_cos_chain'' False)) Or
1.52 + (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_pow'' False)) Or
1.53 + (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_pow_chain'' False)) Or
1.54 + (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_ln'' False)) Or
1.55 + (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_ln_chain'' False)) Or
1.56 + (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_exp'' False)) Or
1.57 + (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_exp_chain'' False)) Or
1.58 + (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_const'' False)) Or
1.59 + (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_var'' False)) Or
1.60 + (Repeat (Rewrite_Set ''make_polynomial'' False))))
1.61 + )) f_f')"
1.62 setup \<open>KEStore_Elems.add_mets
1.63 [Specify.prep_met thy "met_diff_simpl" [] Celem.e_metID
1.64 (["diff","diff_simpl"],
1.65 @@ -347,6 +395,33 @@
1.66 " (Repeat (Rewrite_Set ''make_polynomial'' False)))) " ^
1.67 " )) f_f')")]
1.68 \<close>
1.69 +partial_function (tailrec) differentiate_equality :: "bool \<Rightarrow> real \<Rightarrow> bool"
1.70 + where
1.71 +"differentiate_equality f_f v_v =
1.72 + (let
1.73 + f_f' = Take ((primed (lhs f_f)) = d_d v_v (rhs f_f))
1.74 + in
1.75 + (((Try (Rewrite_Set_Inst [(''bdv'',v_v)] ''diff_conv'' False)) @@
1.76 + (Repeat
1.77 + ((Repeat (Rewrite_Inst [(''bdv'', v_v)] ''diff_sum'' False)) Or
1.78 + (Repeat (Rewrite_Inst [(''bdv'', v_v)] ''diff_dif'' False)) Or
1.79 + (Repeat (Rewrite_Inst [(''bdv'', v_v)] ''diff_prod_const'' False)) Or
1.80 + (Repeat (Rewrite_Inst [(''bdv'', v_v)] ''diff_prod'' False)) Or
1.81 + (Repeat (Rewrite_Inst [(''bdv'', v_v)] ''diff_quot'' True )) Or
1.82 + (Repeat (Rewrite_Inst [(''bdv'', v_v)] ''diff_sin'' False)) Or
1.83 + (Repeat (Rewrite_Inst [(''bdv'', v_v)] ''diff_sin_chain'' False)) Or
1.84 + (Repeat (Rewrite_Inst [(''bdv'', v_v)] ''diff_cos'' False)) Or
1.85 + (Repeat (Rewrite_Inst [(''bdv'', v_v)] ''diff_cos_chain'' False)) Or
1.86 + (Repeat (Rewrite_Inst [(''bdv'', v_v)] ''diff_pow'' False)) Or
1.87 + (Repeat (Rewrite_Inst [(''bdv'', v_v)] ''diff_pow_chain'' False)) Or
1.88 + (Repeat (Rewrite_Inst [(''bdv'', v_v)] ''diff_ln'' False)) Or
1.89 + (Repeat (Rewrite_Inst [(''bdv'', v_v)] ''diff_ln_chain'' False)) Or
1.90 + (Repeat (Rewrite_Inst [(''bdv'', v_v)] ''diff_exp'' False)) Or
1.91 + (Repeat (Rewrite_Inst [(''bdv'', v_v)] ''diff_exp_chain'' False)) Or
1.92 + (Repeat (Rewrite_Inst [(''bdv'', v_v)] ''diff_const'' False)) Or
1.93 + (Repeat (Rewrite_Inst [(''bdv'', v_v)] ''diff_var'' False)) Or
1.94 + (Repeat (Rewrite_Set ''make_polynomial'' False)))) @@
1.95 + (Try (Rewrite_Set_Inst [(''bdv'', v_v)] ''diff_sym_conv'' False)))) f_f')"
1.96 setup \<open>KEStore_Elems.add_mets
1.97 [Specify.prep_met thy "met_diff_equ" [] Celem.e_metID
1.98 (["diff","differentiate_equality"],
1.99 @@ -378,6 +453,16 @@
1.100 " (Repeat (Rewrite_Set ''make_polynomial'' False)))) @@ " ^
1.101 " (Try (Rewrite_Set_Inst [(''bdv'',v_v)] ''diff_sym_conv'' False)))) f_f') ")]
1.102 \<close>
1.103 +partial_function (tailrec) simplify_derivative :: "real \<Rightarrow> real \<Rightarrow> real"
1.104 + where
1.105 +"simplify_derivative f_f v_v =
1.106 + (let
1.107 + f_f' = Take (d_d v_v f_f)
1.108 + in ((Try (Rewrite_Set ''norm_Rational'' False)) @@
1.109 + (Try (Rewrite_Set_Inst [(''bdv'',v_v)] ''diff_conv'' False)) @@
1.110 + (Try (Rewrite_Set_Inst [(''bdv'',v_v)] ''norm_diff'' False)) @@
1.111 + (Try (Rewrite_Set_Inst [(''bdv'',v_v)] ''diff_sym_conv'' False)) @@
1.112 + (Try (Rewrite_Set ''norm_Rational'' False))) f_f')"
1.113 setup \<open>KEStore_Elems.add_mets
1.114 [Specify.prep_met thy "met_diff_after_simp" [] Celem.e_metID
1.115 (["diff","after_simplification"],