1.1 --- a/src/Tools/isac/Knowledge/Diff.thy Wed Sep 08 16:45:27 2010 +0200
1.2 +++ b/src/Tools/isac/Knowledge/Diff.thy Wed Sep 08 16:47:22 2010 +0200
1.3 @@ -283,26 +283,26 @@
1.4 prls=e_rls, crls = Atools_erls, nrls = norm_diff},
1.5 "Script DiffScr (f_::real) (v_v::real) = " ^
1.6 " (let f'_ = Take (d_d v_v f_) " ^
1.7 -" in (((Try (Rewrite_Set_Inst [(bdv,v_)] diff_conv False)) @@ " ^
1.8 +" in (((Try (Rewrite_Set_Inst [(bdv,v_v)] diff_conv False)) @@ " ^
1.9 " (Repeat " ^
1.10 -" ((Repeat (Rewrite_Inst [(bdv,v_)] diff_sum False)) Or " ^
1.11 -" (Repeat (Rewrite_Inst [(bdv,v_)] diff_prod_const False)) Or " ^
1.12 -" (Repeat (Rewrite_Inst [(bdv,v_)] diff_prod False)) Or " ^
1.13 -" (Repeat (Rewrite_Inst [(bdv,v_)] diff_quot True )) Or " ^
1.14 -" (Repeat (Rewrite_Inst [(bdv,v_)] diff_sin False)) Or " ^
1.15 -" (Repeat (Rewrite_Inst [(bdv,v_)] diff_sin_chain False)) Or " ^
1.16 -" (Repeat (Rewrite_Inst [(bdv,v_)] diff_cos False)) Or " ^
1.17 -" (Repeat (Rewrite_Inst [(bdv,v_)] diff_cos_chain False)) Or " ^
1.18 -" (Repeat (Rewrite_Inst [(bdv,v_)] diff_pow False)) Or " ^
1.19 -" (Repeat (Rewrite_Inst [(bdv,v_)] diff_pow_chain False)) Or " ^
1.20 -" (Repeat (Rewrite_Inst [(bdv,v_)] diff_ln False)) Or " ^
1.21 -" (Repeat (Rewrite_Inst [(bdv,v_)] diff_ln_chain False)) Or " ^
1.22 -" (Repeat (Rewrite_Inst [(bdv,v_)] diff_exp False)) Or " ^
1.23 -" (Repeat (Rewrite_Inst [(bdv,v_)] diff_exp_chain False)) Or " ^
1.24 -" (Repeat (Rewrite_Inst [(bdv,v_)] diff_const False)) Or " ^
1.25 -" (Repeat (Rewrite_Inst [(bdv,v_)] diff_var False)) Or " ^
1.26 +" ((Repeat (Rewrite_Inst [(bdv,v_v)] diff_sum False)) Or " ^
1.27 +" (Repeat (Rewrite_Inst [(bdv,v_v)] diff_prod_const False)) Or " ^
1.28 +" (Repeat (Rewrite_Inst [(bdv,v_v)] diff_prod False)) Or " ^
1.29 +" (Repeat (Rewrite_Inst [(bdv,v_v)] diff_quot True )) Or " ^
1.30 +" (Repeat (Rewrite_Inst [(bdv,v_v)] diff_sin False)) Or " ^
1.31 +" (Repeat (Rewrite_Inst [(bdv,v_v)] diff_sin_chain False)) Or " ^
1.32 +" (Repeat (Rewrite_Inst [(bdv,v_v)] diff_cos False)) Or " ^
1.33 +" (Repeat (Rewrite_Inst [(bdv,v_v)] diff_cos_chain False)) Or " ^
1.34 +" (Repeat (Rewrite_Inst [(bdv,v_v)] diff_pow False)) Or " ^
1.35 +" (Repeat (Rewrite_Inst [(bdv,v_v)] diff_pow_chain False)) Or " ^
1.36 +" (Repeat (Rewrite_Inst [(bdv,v_v)] diff_ln False)) Or " ^
1.37 +" (Repeat (Rewrite_Inst [(bdv,v_v)] diff_ln_chain False)) Or " ^
1.38 +" (Repeat (Rewrite_Inst [(bdv,v_v)] diff_exp False)) Or " ^
1.39 +" (Repeat (Rewrite_Inst [(bdv,v_v)] diff_exp_chain False)) Or " ^
1.40 +" (Repeat (Rewrite_Inst [(bdv,v_v)] diff_const False)) Or " ^
1.41 +" (Repeat (Rewrite_Inst [(bdv,v_v)] diff_var False)) Or " ^
1.42 " (Repeat (Rewrite_Set make_polynomial False)))) @@ " ^
1.43 -" (Try (Rewrite_Set_Inst [(bdv,v_)] diff_sym_conv False)))) f'_)"
1.44 +" (Try (Rewrite_Set_Inst [(bdv,v_v)] diff_sym_conv False)))) f'_)"
1.45 ));
1.46
1.47 store_met
1.48 @@ -317,22 +317,22 @@
1.49 " (let f'_ = Take (d_d v_v f_) " ^
1.50 " in (( " ^
1.51 " (Repeat " ^
1.52 -" ((Repeat (Rewrite_Inst [(bdv,v_)] diff_sum False)) Or " ^
1.53 -" (Repeat (Rewrite_Inst [(bdv,v_)] diff_prod_const False)) Or " ^
1.54 -" (Repeat (Rewrite_Inst [(bdv,v_)] diff_prod False)) Or " ^
1.55 -" (Repeat (Rewrite_Inst [(bdv,v_)] diff_quot True )) Or " ^
1.56 -" (Repeat (Rewrite_Inst [(bdv,v_)] diff_sin False)) Or " ^
1.57 -" (Repeat (Rewrite_Inst [(bdv,v_)] diff_sin_chain False)) Or " ^
1.58 -" (Repeat (Rewrite_Inst [(bdv,v_)] diff_cos False)) Or " ^
1.59 -" (Repeat (Rewrite_Inst [(bdv,v_)] diff_cos_chain False)) Or " ^
1.60 -" (Repeat (Rewrite_Inst [(bdv,v_)] diff_pow False)) Or " ^
1.61 -" (Repeat (Rewrite_Inst [(bdv,v_)] diff_pow_chain False)) Or " ^
1.62 -" (Repeat (Rewrite_Inst [(bdv,v_)] diff_ln False)) Or " ^
1.63 -" (Repeat (Rewrite_Inst [(bdv,v_)] diff_ln_chain False)) Or " ^
1.64 -" (Repeat (Rewrite_Inst [(bdv,v_)] diff_exp False)) Or " ^
1.65 -" (Repeat (Rewrite_Inst [(bdv,v_)] diff_exp_chain False)) Or " ^
1.66 -" (Repeat (Rewrite_Inst [(bdv,v_)] diff_const False)) Or " ^
1.67 -" (Repeat (Rewrite_Inst [(bdv,v_)] diff_var False)) Or " ^
1.68 +" ((Repeat (Rewrite_Inst [(bdv,v_v)] diff_sum False)) Or " ^
1.69 +" (Repeat (Rewrite_Inst [(bdv,v_v)] diff_prod_const False)) Or " ^
1.70 +" (Repeat (Rewrite_Inst [(bdv,v_v)] diff_prod False)) Or " ^
1.71 +" (Repeat (Rewrite_Inst [(bdv,v_v)] diff_quot True )) Or " ^
1.72 +" (Repeat (Rewrite_Inst [(bdv,v_v)] diff_sin False)) Or " ^
1.73 +" (Repeat (Rewrite_Inst [(bdv,v_v)] diff_sin_chain False)) Or " ^
1.74 +" (Repeat (Rewrite_Inst [(bdv,v_v)] diff_cos False)) Or " ^
1.75 +" (Repeat (Rewrite_Inst [(bdv,v_v)] diff_cos_chain False)) Or " ^
1.76 +" (Repeat (Rewrite_Inst [(bdv,v_v)] diff_pow False)) Or " ^
1.77 +" (Repeat (Rewrite_Inst [(bdv,v_v)] diff_pow_chain False)) Or " ^
1.78 +" (Repeat (Rewrite_Inst [(bdv,v_v)] diff_ln False)) Or " ^
1.79 +" (Repeat (Rewrite_Inst [(bdv,v_v)] diff_ln_chain False)) Or " ^
1.80 +" (Repeat (Rewrite_Inst [(bdv,v_v)] diff_exp False)) Or " ^
1.81 +" (Repeat (Rewrite_Inst [(bdv,v_v)] diff_exp_chain False)) Or " ^
1.82 +" (Repeat (Rewrite_Inst [(bdv,v_v)] diff_const False)) Or " ^
1.83 +" (Repeat (Rewrite_Inst [(bdv,v_v)] diff_var False)) Or " ^
1.84 " (Repeat (Rewrite_Set make_polynomial False)))) " ^
1.85 " )) f'_)"
1.86 ));
1.87 @@ -347,27 +347,27 @@
1.88 srls = srls_diff, prls=e_rls, crls=Atools_erls, nrls = norm_diff},
1.89 "Script DiffEqScr (f_::bool) (v_v::real) = " ^
1.90 " (let f'_ = Take ((primed (lhs f_)) = d_d v_v (rhs f_)) " ^
1.91 -" in (((Try (Rewrite_Set_Inst [(bdv,v_)] diff_conv False)) @@ " ^
1.92 +" in (((Try (Rewrite_Set_Inst [(bdv,v_v)] diff_conv False)) @@ " ^
1.93 " (Repeat " ^
1.94 -" ((Repeat (Rewrite_Inst [(bdv,v_)] diff_sum False)) Or " ^
1.95 -" (Repeat (Rewrite_Inst [(bdv,v_)] diff_dif False)) Or " ^
1.96 -" (Repeat (Rewrite_Inst [(bdv,v_)] diff_prod_const False)) Or " ^
1.97 -" (Repeat (Rewrite_Inst [(bdv,v_)] diff_prod False)) Or " ^
1.98 -" (Repeat (Rewrite_Inst [(bdv,v_)] diff_quot True )) Or " ^
1.99 -" (Repeat (Rewrite_Inst [(bdv,v_)] diff_sin False)) Or " ^
1.100 -" (Repeat (Rewrite_Inst [(bdv,v_)] diff_sin_chain False)) Or " ^
1.101 -" (Repeat (Rewrite_Inst [(bdv,v_)] diff_cos False)) Or " ^
1.102 -" (Repeat (Rewrite_Inst [(bdv,v_)] diff_cos_chain False)) Or " ^
1.103 -" (Repeat (Rewrite_Inst [(bdv,v_)] diff_pow False)) Or " ^
1.104 -" (Repeat (Rewrite_Inst [(bdv,v_)] diff_pow_chain False)) Or " ^
1.105 -" (Repeat (Rewrite_Inst [(bdv,v_)] diff_ln False)) Or " ^
1.106 -" (Repeat (Rewrite_Inst [(bdv,v_)] diff_ln_chain False)) Or " ^
1.107 -" (Repeat (Rewrite_Inst [(bdv,v_)] diff_exp False)) Or " ^
1.108 -" (Repeat (Rewrite_Inst [(bdv,v_)] diff_exp_chain False)) Or " ^
1.109 -" (Repeat (Rewrite_Inst [(bdv,v_)] diff_const False)) Or " ^
1.110 -" (Repeat (Rewrite_Inst [(bdv,v_)] diff_var False)) Or " ^
1.111 +" ((Repeat (Rewrite_Inst [(bdv,v_v)] diff_sum False)) Or " ^
1.112 +" (Repeat (Rewrite_Inst [(bdv,v_v)] diff_dif False)) Or " ^
1.113 +" (Repeat (Rewrite_Inst [(bdv,v_v)] diff_prod_const False)) Or " ^
1.114 +" (Repeat (Rewrite_Inst [(bdv,v_v)] diff_prod False)) Or " ^
1.115 +" (Repeat (Rewrite_Inst [(bdv,v_v)] diff_quot True )) Or " ^
1.116 +" (Repeat (Rewrite_Inst [(bdv,v_v)] diff_sin False)) Or " ^
1.117 +" (Repeat (Rewrite_Inst [(bdv,v_v)] diff_sin_chain False)) Or " ^
1.118 +" (Repeat (Rewrite_Inst [(bdv,v_v)] diff_cos False)) Or " ^
1.119 +" (Repeat (Rewrite_Inst [(bdv,v_v)] diff_cos_chain False)) Or " ^
1.120 +" (Repeat (Rewrite_Inst [(bdv,v_v)] diff_pow False)) Or " ^
1.121 +" (Repeat (Rewrite_Inst [(bdv,v_v)] diff_pow_chain False)) Or " ^
1.122 +" (Repeat (Rewrite_Inst [(bdv,v_v)] diff_ln False)) Or " ^
1.123 +" (Repeat (Rewrite_Inst [(bdv,v_v)] diff_ln_chain False)) Or " ^
1.124 +" (Repeat (Rewrite_Inst [(bdv,v_v)] diff_exp False)) Or " ^
1.125 +" (Repeat (Rewrite_Inst [(bdv,v_v)] diff_exp_chain False)) Or " ^
1.126 +" (Repeat (Rewrite_Inst [(bdv,v_v)] diff_const False)) Or " ^
1.127 +" (Repeat (Rewrite_Inst [(bdv,v_v)] diff_var False)) Or " ^
1.128 " (Repeat (Rewrite_Set make_polynomial False)))) @@ " ^
1.129 -" (Try (Rewrite_Set_Inst [(bdv,v_)] diff_sym_conv False)))) f'_)"
1.130 +" (Try (Rewrite_Set_Inst [(bdv,v_v)] diff_sym_conv False)))) f'_)"
1.131 ));
1.132
1.133 store_met
1.134 @@ -381,9 +381,9 @@
1.135 "Script DiffScr (f_::real) (v_v::real) = " ^
1.136 " (let f'_ = Take (d_d v_v f_) " ^
1.137 " in ((Try (Rewrite_Set norm_Rational False)) @@ " ^
1.138 -" (Try (Rewrite_Set_Inst [(bdv,v_)] diff_conv False)) @@ " ^
1.139 -" (Try (Rewrite_Set_Inst [(bdv,v_)] norm_diff False)) @@ " ^
1.140 -" (Try (Rewrite_Set_Inst [(bdv,v_)] diff_sym_conv False)) @@ " ^
1.141 +" (Try (Rewrite_Set_Inst [(bdv,v_v)] diff_conv False)) @@ " ^
1.142 +" (Try (Rewrite_Set_Inst [(bdv,v_v)] norm_diff False)) @@ " ^
1.143 +" (Try (Rewrite_Set_Inst [(bdv,v_v)] diff_sym_conv False)) @@ " ^
1.144 " (Try (Rewrite_Set norm_Rational False))) f'_)"
1.145 ));
1.146
1.147 @@ -404,7 +404,7 @@
1.148 castab :=
1.149 overwritel (!castab,
1.150 [((term_of o the o (parse thy)) "Diff",
1.151 - (("Isac.thy", ["derivative_of","function"], ["no_met"]),
1.152 + (("Isac", ["derivative_of","function"], ["no_met"]),
1.153 argl2dtss))
1.154 ]);
1.155
1.156 @@ -422,7 +422,7 @@
1.157 castab :=
1.158 overwritel (!castab,
1.159 [((term_of o the o (parse thy)) "Differentiate",
1.160 - (("Isac.thy", ["named","derivative_of","function"], ["no_met"]),
1.161 + (("Isac", ["named","derivative_of","function"], ["no_met"]),
1.162 argl2dtss))
1.163 ]);
1.164 *}