1.1 --- a/test/Tools/isac/Knowledge/diff.sml Wed Sep 08 16:45:27 2010 +0200
1.2 +++ b/test/Tools/isac/Knowledge/diff.sml Wed Sep 08 16:47:22 2010 +0200
1.3 @@ -86,7 +86,7 @@
1.4 "----------- for correction of diff_const ------------------------";
1.5 "----------- for correction of diff_const ------------------------";
1.6 (*re-evaluate this file, otherwise > *** ME_Isa: 'erls' not known*)
1.7 -val thy' = "Diff.thy";
1.8 +val thy' = "Diff";
1.9 val ct = "Not (x =!= a)";
1.10 rewrite_set thy' false "erls" ct;
1.11 val ct = "2 is_const";
1.12 @@ -127,7 +127,7 @@
1.13 " _________________ for correction of diff_quot _________________ ";
1.14 " _________________ for correction of diff_quot _________________ ";
1.15 " _________________ for correction of diff_quot _________________ ";
1.16 -val thy' = "Diff.thy";
1.17 +val thy' = "Diff";
1.18 val ct = "Not (x = 0)";
1.19 rewrite_set thy' false "erls" ct;
1.20
1.21 @@ -145,7 +145,7 @@
1.22 " _________________ differentiate by rewrite _________________ ";
1.23 " _________________ differentiate by rewrite _________________ ";
1.24 " _________________ differentiate by rewrite _________________ ";
1.25 -val thy' = "Diff.thy";
1.26 +val thy' = "Diff";
1.27 val ct = "d_d x (x ^^^ 2 + 3 * x + 4)";
1.28 "--- 1 ---";
1.29 val thm = ("diff_sum","");
1.30 @@ -197,7 +197,7 @@
1.31 val fmz = ["functionTerm (x ^^^ 2 + 3 * x + 4)",
1.32 "differentiateFor x","derivative f_'_"];
1.33 val (dI',pI',mI') =
1.34 - ("Diff.thy",["derivative_of","function"],
1.35 + ("Diff",["derivative_of","function"],
1.36 ["diff","diff_simpl"]);
1.37 val p = e_pos'; val c = [];
1.38 "--- s1 ---";
1.39 @@ -258,7 +258,7 @@
1.40 trace_rewrite:=false;
1.41
1.42 val ct = "2 * x ^^^ (2 - 1) + 3 * 1 + 0";
1.43 - val SOME (ct',_) = rewrite_set "Isac.thy" false "make_polynomial" ct;
1.44 + val SOME (ct',_) = rewrite_set "Isac" false "make_polynomial" ct;
1.45
1.46 trace_rewrite:=true;
1.47 val t = str2term ct;
1.48 @@ -274,7 +274,7 @@
1.49 case string_of_thm thm of
1.50
1.51
1.52 - val Rewrite_Set' ("Diff.thy",false,"make_polynomial",ff,(ff',[])) = m;
1.53 + val Rewrite_Set' ("Diff",false,"make_polynomial",ff,(ff',[])) = m;
1.54 term2str ff; term2str ff';
1.55
1.56
1.57 @@ -285,7 +285,7 @@
1.58 val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.59 "--- 8 ---";
1.60 (*val nxt =
1.61 -("Check_Postcond",Check_Postcond ("Diff.thy","differentiate_on_R"));*)
1.62 +("Check_Postcond",Check_Postcond ("Diff","differentiate_on_R"));*)
1.63 val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.64 "--- 9 ---";
1.65 (*val nxt = ("End_Proof'",End_Proof');*)
1.66 @@ -303,35 +303,35 @@
1.67 " _________________ script-eval corrected _________________ ";
1.68 " _________________ script-eval corrected _________________ ";
1.69 " _________________ script-eval corrected _________________ ";
1.70 -val scr = Script (((inst_abs (assoc_thy "Test.thy")) o
1.71 +val scr = Script (((inst_abs (assoc_thy "Test")) o
1.72 term_of o the o (parse Diff.thy))
1.73 - "Script Differentiate (f_::real) (v_::real) = \
1.74 + "Script Differentiate (f_::real) (v_v::real) = \
1.75 \(let f_ = Try (Repeat (Rewrite frac_conv False f_)); \
1.76 \ f_ = Try (Repeat (Rewrite root_conv False f_)); \
1.77 \ f_ = Repeat \
1.78 - \ ((Repeat (Rewrite_Inst [(bdv,v_)] diff_sum False f_)) Or \
1.79 - \ (Repeat (Rewrite_Inst [(bdv,v_)] diff_prod_const False f_)) Or \
1.80 - \ (Repeat (Rewrite_Inst [(bdv,v_)] diff_prod False f_)) Or \
1.81 - \ (Repeat (Rewrite_Inst [(bdv,v_)] diff_quot False f_)) Or \
1.82 - \ (Repeat (Rewrite_Inst [(bdv,v_)] diff_sin False f_)) Or \
1.83 - \ (Repeat (Rewrite_Inst [(bdv,v_)] diff_sin_chain False f_)) Or \
1.84 - \ (Repeat (Rewrite_Inst [(bdv,v_)] diff_cos False f_)) Or \
1.85 - \ (Repeat (Rewrite_Inst [(bdv,v_)] diff_cos_chain False f_)) Or \
1.86 - \ (Repeat (Rewrite_Inst [(bdv,v_)] diff_pow False f_)) Or \
1.87 - \ (Repeat (Rewrite_Inst [(bdv,v_)] diff_pow_chain False f_)) Or \
1.88 - \ (Repeat (Rewrite_Inst [(bdv,v_)] diff_ln False f_)) Or \
1.89 - \ (Repeat (Rewrite_Inst [(bdv,v_)] diff_ln_chain False f_)) Or \
1.90 - \ (Repeat (Rewrite_Inst [(bdv,v_)] diff_exp False f_)) Or \
1.91 - \ (Repeat (Rewrite_Inst [(bdv,v_)] diff_exp_chain False f_)) Or \
1.92 - \ (Repeat (Rewrite_Inst [(bdv,v_)] diff_const False f_)) Or \
1.93 - \ (Repeat (Rewrite_Inst [(bdv,v_)] diff_var False f_)) Or \
1.94 + \ ((Repeat (Rewrite_Inst [(bdv,v_v)] diff_sum False f_)) Or \
1.95 + \ (Repeat (Rewrite_Inst [(bdv,v_v)] diff_prod_const False f_)) Or \
1.96 + \ (Repeat (Rewrite_Inst [(bdv,v_v)] diff_prod False f_)) Or \
1.97 + \ (Repeat (Rewrite_Inst [(bdv,v_v)] diff_quot False f_)) Or \
1.98 + \ (Repeat (Rewrite_Inst [(bdv,v_v)] diff_sin False f_)) Or \
1.99 + \ (Repeat (Rewrite_Inst [(bdv,v_v)] diff_sin_chain False f_)) Or \
1.100 + \ (Repeat (Rewrite_Inst [(bdv,v_v)] diff_cos False f_)) Or \
1.101 + \ (Repeat (Rewrite_Inst [(bdv,v_v)] diff_cos_chain False f_)) Or \
1.102 + \ (Repeat (Rewrite_Inst [(bdv,v_v)] diff_pow False f_)) Or \
1.103 + \ (Repeat (Rewrite_Inst [(bdv,v_v)] diff_pow_chain False f_)) Or \
1.104 + \ (Repeat (Rewrite_Inst [(bdv,v_v)] diff_ln False f_)) Or \
1.105 + \ (Repeat (Rewrite_Inst [(bdv,v_v)] diff_ln_chain False f_)) Or \
1.106 + \ (Repeat (Rewrite_Inst [(bdv,v_v)] diff_exp False f_)) Or \
1.107 + \ (Repeat (Rewrite_Inst [(bdv,v_v)] diff_exp_chain False f_)) Or \
1.108 + \ (Repeat (Rewrite_Inst [(bdv,v_v)] diff_const False f_)) Or \
1.109 + \ (Repeat (Rewrite_Inst [(bdv,v_v)] diff_var False f_)) Or \
1.110 \ (Repeat (Rewrite_Set Test_simplify False f_))); \
1.111 \ f_ = Try (Repeat (Rewrite sym_frac_conv False f_)) \
1.112 \ in Try (Repeat (Rewrite sym_root_conv False f_)))");
1.113 val d = e_rls;
1.114 val (dI',pI',mI') =
1.115 - ("Diff.thy",e_pblID,
1.116 - ("Diff.thy","differentiate_on_R"));
1.117 + ("Diff",e_pblID,
1.118 + ("Diff","differentiate_on_R"));
1.119 val p = e_pos'; val c = [];
1.120 val (mI,m) = ("Init_Proof",Init_Proof ([], (dI',pI',mI')));
1.121 val (p,_,_,_,_,pt) = me (mI,m) p c EmptyPtree;
1.122 @@ -352,45 +352,45 @@
1.123 val (pt,_) = cappend_atomic pt[1]e_loc ct (Rewrite("test","")) ct Complete;
1.124 val Appl m'=applicable_in p pt (Rewrite_Inst (["(bdv,x)"],("diff_sum","")));
1.125
1.126 -val NextStep(l1,m') = nxt_tac "Diff.thy" (pt,p) scr ets0 l0;
1.127 +val NextStep(l1,m') = nxt_tac "Diff" (pt,p) scr ets0 l0;
1.128 (*("diff_sum","")*)
1.129 val Steps[(Form' (FormKF (_,_,_,_,res)),pt,p,_,s,ets1)] =
1.130 - locate_gen "Diff.thy" m' (pt,p) (scr,d) ets0 l0;
1.131 + locate_gen "Diff" m' (pt,p) (scr,d) ets0 l0;
1.132 val ets1 = (drop_last ets0) @ ets1;val pt = update_ets pt [] [(1,ets1)];
1.133 " --------------- 2. ---------------------------------------------";
1.134 val Appl m'=applicable_in p pt (Rewrite_Inst (["(bdv,x)"],("diff_sum","")));
1.135 -val NextStep(l2,m') = nxt_tac "Diff.thy" (pt,p) scr ets1 l1;
1.136 +val NextStep(l2,m') = nxt_tac "Diff" (pt,p) scr ets1 l1;
1.137 (*("diff_sum","")*)
1.138 val Steps[(Form' (FormKF (_,_,_,_,res)),pt,p,_,s,ets2)] =
1.139 - locate_gen "Diff.thy" m' (pt,p) (scr,d) ets1 l1;
1.140 + locate_gen "Diff" m' (pt,p) (scr,d) ets1 l1;
1.141 val ets2 = (drop_last ets1) @ ets2;val pt = update_ets pt [] [(1,ets2)];
1.142 " --------------- 3. ---------------------------------------------";
1.143 val Appl m'=applicable_in p pt (Rewrite_Inst (["(bdv,x)"],("diff_prod_const","")));
1.144 -val NextStep(l3,m') = nxt_tac "Diff.thy" (pt,p) scr ets2 l2;
1.145 +val NextStep(l3,m') = nxt_tac "Diff" (pt,p) scr ets2 l2;
1.146 (*("diff_prod_const","")*)
1.147 val Steps[(Form' (FormKF (_,_,_,_,res)),pt,p,_,s,ets3)] =
1.148 - locate_gen "Diff.thy" m' (pt,p) (scr,d) ets2 l2;
1.149 + locate_gen "Diff" m' (pt,p) (scr,d) ets2 l2;
1.150 val ets3 = (drop_last ets2) @ ets3; val pt = update_ets pt [] [(1,ets3)];
1.151 " --------------- 4. ---------------------------------------------";
1.152 val Appl m'=applicable_in p pt (Rewrite_Inst (["(bdv,x)"],("diff_pow","")));
1.153 -val NextStep(l4,m') = nxt_tac "Diff.thy" (pt,p) scr ets3 l3;
1.154 +val NextStep(l4,m') = nxt_tac "Diff" (pt,p) scr ets3 l3;
1.155 (*("diff_pow","")*)
1.156 val Steps[(Form' (FormKF (_,_,_,_,res)),pt,p,_,s,ets4)] =
1.157 - locate_gen "Diff.thy" m' (pt,p) (scr,d) ets3 l3;
1.158 + locate_gen "Diff" m' (pt,p) (scr,d) ets3 l3;
1.159 val ets4 = (drop_last ets3) @ ets4; val pt = update_ets pt [] [(1,ets4)];
1.160 " --------------- 5. ---------------------------------------------";
1.161 val Appl m'=applicable_in p pt (Rewrite_Inst (["(bdv,x)"],("diff_const","")));
1.162 -val NextStep(l5,m') = nxt_tac "Diff.thy" (pt,p) scr ets4 l4;
1.163 +val NextStep(l5,m') = nxt_tac "Diff" (pt,p) scr ets4 l4;
1.164 (*("diff_const","")*)
1.165 val Steps[ (Form' (FormKF (_,_,_,_,res)),pt,p,_,s,ets5)] =
1.166 - locate_gen "Diff.thy" m' (pt,p) (scr,d) ets4 l4;
1.167 + locate_gen "Diff" m' (pt,p) (scr,d) ets4 l4;
1.168 val ets5 = (drop_last ets4) @ ets5; val pt = update_ets pt [] [(1,ets5)];
1.169 " --------------- 6. ---------------------------------------------";
1.170 val Appl m'=applicable_in p pt (Rewrite_Inst (["(bdv,x)"],("diff_var","")));
1.171 -val NextStep(l6,m') = nxt_tac "Diff.thy" (pt,p) scr ets5 l5;
1.172 +val NextStep(l6,m') = nxt_tac "Diff" (pt,p) scr ets5 l5;
1.173 (*("diff_var","")ok; here was("diff_const","")because of wrong rule in *.thy*)
1.174 val Steps[(Form' (FormKF (_,_,_,_,res)),pt,p,_,s,ets6)] =
1.175 - locate_gen "Diff.thy" m' (pt,p) (scr,d) ets5 l5;
1.176 + locate_gen "Diff" m' (pt,p) (scr,d) ets5 l5;
1.177 val ets6 = (drop_last ets5) @ ets6; val pt = update_ets pt [] [(1,ets6)];
1.178 " --------------- 7. ---------------------------------------------";
1.179 val Appl m'=applicable_in p pt (Rewrite_Set "Test_simplify");
1.180 @@ -412,7 +412,7 @@
1.181 val fmz = ["functionTerm (d_d x (x ^^^ 2 + 3 * x + 4))",
1.182 "differentiateFor x","derivative f_'_"];
1.183 val (dI',pI',mI') =
1.184 - ("Diff.thy",["derivative_of","function"],
1.185 + ("Diff",["derivative_of","function"],
1.186 ["diff","differentiate_on_R"]);
1.187 *)
1.188
1.189 @@ -427,7 +427,7 @@
1.190 val fmz = ["functionTerm (d_d x (x ^^^ 2 + 3 * x + 4))",
1.191 "differentiateFor x","derivative f_'_"];
1.192 val (dI',pI',mI') =
1.193 - ("Diff.thy",["derivative_of","function"],
1.194 + ("Diff",["derivative_of","function"],
1.195 ["diff","differentiate_on_R"]);
1.196 *)
1.197
1.198 @@ -439,7 +439,7 @@
1.199 val fmz = ["functionTerm (x ^^^ 2 + 3 * x + 4)",
1.200 "differentiateFor x","derivative f_'_"];
1.201 val (dI',pI',mI') =
1.202 - ("Diff.thy",["derivative_of","function"],
1.203 + ("Diff",["derivative_of","function"],
1.204 ["diff","diff_simpl"]);
1.205 (*val p = e_pos'; val c = [];
1.206 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
1.207 @@ -452,7 +452,7 @@
1.208 val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.209 val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.210 val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.211 -(*nxt = ("Apply_Method",Apply_Method ("Diff.thy","differentiate_on_R*)
1.212 +(*nxt = ("Apply_Method",Apply_Method ("Diff","differentiate_on_R*)
1.213 val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.214
1.215 val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.216 @@ -486,30 +486,30 @@
1.217 else raise error "diff.sml: diff.behav. in 'primed'";
1.218 atomty f'_;
1.219
1.220 -val str = "Script DiffEqScr (f_::bool) (v_::real) = \
1.221 +val str = "Script DiffEqScr (f_::bool) (v_v::real) = \
1.222 \ (let f'_ = Take ((primed (lhs f_)) = d_d v_v (rhs f_)) \
1.223 \ in (((Try (Repeat (Rewrite frac_conv False))) @@ \
1.224 \ (Try (Repeat (Rewrite root_conv False))) @@ \
1.225 \ (Try (Repeat (Rewrite realpow_pow False))) @@ \
1.226 \ (Repeat \
1.227 - \ ((Repeat (Rewrite_Inst [(bdv,v_)] diff_sum False)) Or \
1.228 - \ (Repeat (Rewrite_Inst [(bdv,v_)] diff_prod_const False)) Or \
1.229 - \ (Repeat (Rewrite_Inst [(bdv,v_)] diff_prod False)) Or \
1.230 - \ (Repeat (Rewrite_Inst [(bdv,v_)] diff_quot True )) Or \
1.231 - \ (Repeat (Rewrite_Inst [(bdv,v_)] diff_sin False)) Or \
1.232 - \ (Repeat (Rewrite_Inst [(bdv,v_)] diff_sin_chain False)) Or \
1.233 - \ (Repeat (Rewrite_Inst [(bdv,v_)] diff_cos False)) Or \
1.234 - \ (Repeat (Rewrite_Inst [(bdv,v_)] diff_cos_chain False)) Or \
1.235 - \ (Repeat (Rewrite_Inst [(bdv,v_)] diff_pow False)) Or \
1.236 - \ (Repeat (Rewrite_Inst [(bdv,v_)] diff_pow_chain False)) Or \
1.237 - \ (Repeat (Rewrite_Inst [(bdv,v_)] diff_ln False)) Or \
1.238 - \ (Repeat (Rewrite_Inst [(bdv,v_)] diff_ln_chain False)) Or \
1.239 - \ (Repeat (Rewrite_Inst [(bdv,v_)] diff_exp False)) Or \
1.240 - \ (Repeat (Rewrite_Inst [(bdv,v_)] diff_exp_chain False)) Or \
1.241 - \ (Repeat (Rewrite_Inst [(bdv,v_)] diff_sqrt False)) Or \
1.242 - \ (Repeat (Rewrite_Inst [(bdv,v_)] diff_sqrt_chain False)) Or \
1.243 - \ (Repeat (Rewrite_Inst [(bdv,v_)] diff_const False)) Or \
1.244 - \ (Repeat (Rewrite_Inst [(bdv,v_)] diff_var False)) Or \
1.245 + \ ((Repeat (Rewrite_Inst [(bdv,v_v)] diff_sum False)) Or \
1.246 + \ (Repeat (Rewrite_Inst [(bdv,v_v)] diff_prod_const False)) Or \
1.247 + \ (Repeat (Rewrite_Inst [(bdv,v_v)] diff_prod False)) Or \
1.248 + \ (Repeat (Rewrite_Inst [(bdv,v_v)] diff_quot True )) Or \
1.249 + \ (Repeat (Rewrite_Inst [(bdv,v_v)] diff_sin False)) Or \
1.250 + \ (Repeat (Rewrite_Inst [(bdv,v_v)] diff_sin_chain False)) Or \
1.251 + \ (Repeat (Rewrite_Inst [(bdv,v_v)] diff_cos False)) Or \
1.252 + \ (Repeat (Rewrite_Inst [(bdv,v_v)] diff_cos_chain False)) Or \
1.253 + \ (Repeat (Rewrite_Inst [(bdv,v_v)] diff_pow False)) Or \
1.254 + \ (Repeat (Rewrite_Inst [(bdv,v_v)] diff_pow_chain False)) Or \
1.255 + \ (Repeat (Rewrite_Inst [(bdv,v_v)] diff_ln False)) Or \
1.256 + \ (Repeat (Rewrite_Inst [(bdv,v_v)] diff_ln_chain False)) Or \
1.257 + \ (Repeat (Rewrite_Inst [(bdv,v_v)] diff_exp False)) Or \
1.258 + \ (Repeat (Rewrite_Inst [(bdv,v_v)] diff_exp_chain False)) Or \
1.259 + \ (Repeat (Rewrite_Inst [(bdv,v_v)] diff_sqrt False)) Or \
1.260 + \ (Repeat (Rewrite_Inst [(bdv,v_v)] diff_sqrt_chain False)) Or \
1.261 + \ (Repeat (Rewrite_Inst [(bdv,v_v)] diff_const False)) Or \
1.262 + \ (Repeat (Rewrite_Inst [(bdv,v_v)] diff_var False)) Or \
1.263 \ (Repeat (Rewrite_Set make_polynomial False)))) @@ \
1.264 \ (Try (Repeat (Rewrite sym_frac_conv False))) @@ \
1.265 \ (Try (Repeat (Rewrite sym_root_conv False))))) f'_)"
1.266 @@ -568,7 +568,7 @@
1.267 [(["functionTerm (x^2 + x+ 1/x + 2/x^2)",
1.268 (*"functionTerm ((x^3)^5)",*)
1.269 "differentiateFor x", "derivative f_'_"],
1.270 - ("Isac.thy", ["derivative_of","function"],
1.271 + ("Isac", ["derivative_of","function"],
1.272 ["diff","differentiate_on_R"]))];
1.273 Iterator 1;
1.274 moveActiveRoot 1;
1.275 @@ -583,7 +583,7 @@
1.276 CalcTree
1.277 [(["functionTerm (x^3 * x^5)",
1.278 "differentiateFor x", "derivative f_'_"],
1.279 - ("Isac.thy", ["derivative_of","function"],
1.280 + ("Isac", ["derivative_of","function"],
1.281 ["diff","differentiate_on_R"]))];
1.282 Iterator 1;
1.283 moveActiveRoot 1;
1.284 @@ -608,7 +608,7 @@
1.285 CalcTree
1.286 [(["functionTerm (x^3 * x^5)",
1.287 "differentiateFor x", "derivative f_'_"],
1.288 - ("Isac.thy", ["derivative_of","function"],
1.289 + ("Isac", ["derivative_of","function"],
1.290 ["diff","after_simplification"]))];
1.291 Iterator 1;
1.292 moveActiveRoot 1;
1.293 @@ -628,7 +628,7 @@
1.294 CalcTree
1.295 [(["functionTerm ((x^3)^5)",
1.296 "differentiateFor x", "derivative f_'_"],
1.297 - ("Isac.thy", ["derivative_of","function"],
1.298 + ("Isac", ["derivative_of","function"],
1.299 ["diff","after_simplification"]))];
1.300 Iterator 1;
1.301 moveActiveRoot 1;
1.302 @@ -645,7 +645,7 @@
1.303 states:=[];
1.304 CalcTree
1.305 [(["functionEq (A = s * (a - s))", "differentiateFor s", "derivativeEq f_'_"],
1.306 - ("Isac.thy", ["named","derivative_of","function"],
1.307 + ("Isac", ["named","derivative_of","function"],
1.308 ["diff","differentiate_equality"]))];
1.309 Iterator 1;
1.310 moveActiveRoot 1;
1.311 @@ -677,7 +677,7 @@
1.312 CalcTree
1.313 [(["functionTerm (x^2 + x + 1)",
1.314 "differentiateFor x", "derivative f_'_"],
1.315 - ("Isac.thy", ["derivative_of","function"],
1.316 + ("Isac", ["derivative_of","function"],
1.317 ["diff","differentiate_on_R"]))];
1.318 Iterator 1;
1.319 moveActiveRoot 1;