1.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
1.2 +++ b/src/sml/systest/testdaten.sml Thu Apr 17 18:01:03 2003 +0200
1.3 @@ -0,0 +1,400 @@
1.4 +(* testdaten f"ur isac demo0
1.5 + WN 31.10.00, .., 18.1.01
1.6 + use"tests/testdaten.sml";
1.7 + use"testdaten.sml";
1.8 +
1.9 + proofs:= []; dials:=([],[],[]);
1.10 + *)
1.11 +" _________________ exampel [x=4]: Rules 4.2.01a________________ ";
1.12 +" _________________ exampel [x=4]: Rules 4.2.01b________________ ";
1.13 +" _________________ exampel [x=4]: tutor active ________________ ";
1.14 +" _________________ exampel [x=4] ________________ ";
1.15 +" _________________ exampel [x =(-12)/5] ________________ ";
1.16 +" _________________ exampel [x =(-12)/5] Auto ________________ ";
1.17 +" ----------------- d_d x (x ^^^ 2 + 3 * x + 4) ----------------- ";
1.18 +" ----------------- d_d x (x ^^^ 2 + x + 1 / x ^^^ 2) ----------------- ";
1.19 +" ----------------- Schalk III S.62 Nr. 51a) --------- ";
1.20 +" ----------------- Schalk III S.144 Nr. 408b) --------- ";
1.21 +" ----------------- Schalk III S.137 Nr. 359g) --------- ";
1.22 +
1.23 +
1.24 +
1.25 +
1.26 +
1.27 +" _________________ exampel [x=4]: Rules 4.2.01a________________ ";
1.28 +" _________________ exampel [x=4]: Rules 4.2.01a________________ ";
1.29 +val (_,uI,0,0,[],[New_User],_) = StdinSML 0 0 0 0 New_User;
1.30 +val (_,_,pI,0,[],[New_Proof],_) = StdinSML uI 0 0 0 New_Proof;
1.31 +val fmz = ["equality (sqrt(9+4*x)=sqrt x + sqrt(5+x))",
1.32 + "solveFor x","errorBound (eps=0)",
1.33 + "solutions L"];
1.34 +val (dI',pI',mI') =
1.35 + ("Test.thy",["squareroot","univariate","equation","test"],
1.36 + ("Test.thy","sqrt-equ-test"));
1.37 +"--- 0 ---";
1.38 +StdinSML uI pI 1 1 (RuleFK (Init_Proof (fmz,(dI',pI',mI'))));
1.39 +"--- 1 ---";
1.40 +StdinSML uI pI ~1 ~1 (Command Accept);
1.41 +(* square_equation_left
1.42 +"#9 + #4 * x = (sqrt x + sqrt (#5 + x)) ^^^ #2"*)
1.43 +"--- 2 ---";
1.44 +StdinSML uI pI ~2 ~2 (Command Rules);
1.45 +"--- 3 ---";
1.46 +StdinSML uI pI ~2 ~2 (RuleFK (Rewrite_Set "Test_simplify"));
1.47 +"--- 4 ---";
1.48 +val (_,_,_,_,_,[Error_ _ (*"Error_ Test_simplify not applicable to ..*),
1.49 + Request "apply a rule !"],_) =
1.50 +StdinSML uI pI ~3 ~3 (RuleFK (Rewrite_Set "Test_simplify"));
1.51 +
1.52 +
1.53 +" _________________ exampel [x=4]: Rules 4.2.01b________________ ";
1.54 +" _________________ exampel [x=4]: Rules 4.2.01b________________ ";
1.55 +val (_,uI,0,0,[],[New_User],_) = StdinSML 0 0 0 0 New_User;
1.56 +val (_,_,pI,0,[],[New_Proof],_) = StdinSML uI 0 0 0 New_Proof;
1.57 +val fmz = ["equality (sqrt(9+4*x)=sqrt x + sqrt(5+x))",
1.58 + "solveFor x","errorBound (eps=0)",
1.59 + "solutions L"];
1.60 +val (dI',pI',mI') =
1.61 + ("Test.thy",["squareroot","univariate","equation","test"],
1.62 + ("Test.thy","sqrt-equ-test"));
1.63 +"--- 0 ---";
1.64 +StdinSML uI pI 1 1 (RuleFK (Init_Proof (fmz,(dI',pI',mI'))));
1.65 +"--- 1 ---";
1.66 +StdinSML uI pI ~1 ~1 (Command Accept);
1.67 +(* square_equation_left
1.68 +"#9 + #4 * x = (sqrt x + sqrt (#5 + x)) ^^^ #2"*)
1.69 +"--- 2 ---";
1.70 +StdinSML uI pI ~2 ~2 (Command Rules);
1.71 +"--- 3 ---";
1.72 +val (_,_,_,_,_,
1.73 + [Error_ _ (*"Error_ 'square_equation_left' not applicable to: #9 *),
1.74 + Select _, Request "select a rule !"],_) =
1.75 +StdinSML uI pI ~2 ~2 (RuleFK (Rewrite ("square_equation_left","")));
1.76 +
1.77 +
1.78 +" _________________ exampel [x=4]: tutor active ________________ ";
1.79 +" _________________ exampel [x=4]: tutor active ________________ ";
1.80 +val (_,uI,0,0,[],[New_User],_) = StdinSML 0 0 0 0 New_User;
1.81 +val (_,_,pI,0,[],[New_Proof],_) = StdinSML uI 0 0 0 New_Proof;
1.82 +val fmz = ["equality (sqrt(9+4*x)=sqrt x + sqrt(5+x))",
1.83 + "solveFor x","errorBound (eps=0)",
1.84 + "solutions L"];
1.85 +val (dI',pI',mI') =
1.86 + ("Test.thy",["squareroot","univariate","equation","test"],
1.87 + ("Test.thy","sqrt-equ-test"));
1.88 +"--- s1 ---";
1.89 +StdinSML uI pI 1 1 (RuleFK (Init_Proof (fmz,(dI',pI',mI'))));
1.90 +"--- 1 ---";
1.91 +StdinSML uI pI ~1 ~1 (Command Accept);
1.92 +(* square_equation_left
1.93 +"#9 + #4 * x = (sqrt x + sqrt (#5 + x)) ^^^ #2"*)
1.94 +"--- 2 ---";
1.95 +StdinSML uI pI ~2 ~2 (Command Accept);
1.96 +(* Test_simplify
1.97 +"#9 + #4 * x = #5 + (#2 * x + #2 * sqrt (x ^^^ #2 + #5 * x))"*)
1.98 +"--- 3 ---";
1.99 +StdinSML uI pI ~3 ~3 (Command Accept);
1.100 +(* rearrange_assoc
1.101 +"#9 + #4 * x = #5 + #2 * x + #2 * sqrt (x ^^^ #2 + #5 * x)"*)
1.102 +"--- 4 ---";
1.103 +StdinSML uI pI ~4 ~4 (Command Accept);
1.104 +(* isolate_root
1.105 +"sqrt (x ^^^ #2 + #5 * x) = (#5 + #2 * x + #-1 * (#9 + #4 * x)) // (#-1 *#2)"*)
1.106 +"--- 5 ---";
1.107 +StdinSML uI pI ~5 ~5 (Command Accept);
1.108 +(* Test_simplify
1.109 +"sqrt (x ^^^ #2 + #5 * x) = #2 + x"*)
1.110 +"--- 6 ---";
1.111 +StdinSML uI pI ~6 ~6 (Command Accept);
1.112 +(* square_equation_left
1.113 +"x ^^^ #2 + #5 * x = (#2 + x) ^^^ #2"*)
1.114 +"--- 7 ---";
1.115 +StdinSML uI pI ~7 ~7 (Command Accept);
1.116 +(* Test_simplify
1.117 +"x ^^^ #2 + #5 * x = #4 + (x ^^^ #2 + #4 * x)"*)
1.118 +"--- 8 ---";
1.119 +StdinSML uI pI ~8 ~8 (Command Accept);
1.120 +(* rearrange_assoc
1.121 +"x ^^^ #2 + #5 * x = #4 + x ^^^ #2 + #4 * x"*)
1.122 +"--- 9 ---";
1.123 +StdinSML uI pI ~9 ~9 (Command Accept);
1.124 +(* Test_simplify
1.125 +"x ^^^ #2 + #5 * x = #4 + (x ^^^ #2 + #4 * x)"*)
1.126 +"--- 10 ---";
1.127 +StdinSML uI pI ~10 ~10 (Command Accept);
1.128 +(* norm_equation
1.129 +"x ^^^ #2 + #5 * x + #-1 * (#4 + (x ^^^ #2 + #4 * x)) = #0"*)
1.130 +"--- 11 ---";
1.131 +StdinSML uI pI ~11 ~11 (Command Accept);
1.132 +(* Test_simplify
1.133 + "#-4 + x = #0"*)
1.134 +"--- 12 ---";
1.135 +StdinSML uI pI ~12 ~12 (Command Accept);
1.136 +(* isolate_bdv
1.137 +"x = #0 + #-1 * #-4" *)
1.138 +"--- 13 ---";
1.139 +StdinSML uI pI ~13 ~13 (Command Accept);
1.140 +(* Test_simplify
1.141 +"x = #4" *)
1.142 +"--- 14 ---";
1.143 +StdinSML uI pI ~14 ~14 (Command Accept);
1.144 +val (_,_,1,~14,[],[RuleKF (_,m),FormKF (_,_,_,_,f),Request "Accept ?"],_) = it;
1.145 +if m = Check_Postcond ["squareroot","univariate","equation","test"]
1.146 + andalso f = "[x = 4]" then ()
1.147 +else raise error "new behaviour in: exampel [x=4]: tutor active";
1.148 +"--- 15 ---";
1.149 +StdinSML uI pI ~15 ~15 (Command Accept);
1.150 +(* Request "start another example"*)
1.151 +
1.152 +(*---- after restruct. kb 18.9.02 ---- (same is in test-FE...)
1.153 +" _________________ exampel [x=4] ________________ ";
1.154 +" _________________ exampel [x=4] ________________ ";
1.155 +proofs:= []; dials:=([],[],[]);
1.156 +StdinSML 0 0 0 0 New_User;
1.157 +StdinSML 1 0 0 0 New_Proof;
1.158 +val fmz = ["equality (sqrt(9+4*x)=sqrt x + sqrt(5+x))",
1.159 + "solveFor x","errorBound (eps=0)",
1.160 + "solutions L"];
1.161 +val (dI',pI',mI') =
1.162 + ("Test.thy",["squareroot","univariate","equation","test"],
1.163 + ("Test.thy","sqrt-equ-test"));
1.164 +"--- s1 ---";
1.165 +val (_,1,1,1,[],[_,_,FormKF (_,_,_,_,f),req],_) =
1.166 +StdinSML 1 1 1 1 (RuleFK (Init_Proof (fmz,(dI',pI',mI'))));
1.167 +
1.168 +StdinSML 1 1 ~1 ~1 (Command ActivePlus);
1.169 +StdinSML 1 1 ~1 ~1 (Command ActivePlus);
1.170 +StdinSML 1 1 ~1 ~1 (Command ActivePlus);
1.171 +StdinSML 1 1 ~1 ~1 (Command ActivePlus);(*acti=4..SelRule*)
1.172 +
1.173 +"--- !!! x1 --- strange choice"; (* hier nochmals spec !*)
1.174 +StdinSML 1 1 ~1 ~1 (RuleFK (Rewrite_Set "norm_equation"));
1.175 +"--- !!! x2 --- ME knows nxt_step";
1.176 +StdinSML 1 1 ~2 ~2 (RuleFK (Rewrite_Set "Test_simplify"));
1.177 +"--- !!! x3 --- helpless !!!";
1.178 +val (_,_,_,_,_,[FormKF (_,_,_,_,res),_,requ],_) =
1.179 +StdinSML 1 1 ~3 ~3 (RuleFK (Rewrite_Set "rearrange_assoc"));
1.180 +"--- !!! x4 ---";
1.181 +val (_,_,_,_,_,[FormKF (_,_,_,_,res),_,requ],_) =
1.182 +StdinSML 1 1 ~4 ~4 (RuleFK (Rewrite_Set "isolate_root"));
1.183 +"--- !!! x5 --- back at original equation !!!";
1.184 +val (_,_,_,_,_,[FormKF (_,_,_,_,res),_,requ],_) =
1.185 +StdinSML 1 1 ~5 ~5 (RuleFK (Rewrite_Set "Test_simplify"));
1.186 +if res="sqrt (9 + 4 * x) = sqrt x + sqrt (5 + x)"
1.187 +then () else raise error "new behaviour in test-example";
1.188 +"--- !!! x6 --- not applicable";
1.189 +val (_,_,_,_,_,[Error_ err,_,requ],_) =
1.190 +StdinSML 1 1 ~6 ~6 (RuleFK (Rewrite_Set "Test_simplify"));
1.191 +(*val (_,_,_,_,_,[RuleKF r,requ],_) =*)
1.192 +val (_,_,_,_,_,ios,_) =
1.193 +StdinSML 1 1 ~6 ~6 (Command YourTurn);
1.194 +StdinSML 1 1 ~7 ~7 (Command Accept);
1.195 +StdinSML 1 1 ~8 ~8 (Command Accept);
1.196 +StdinSML 1 1 ~9 ~9 (Command Accept);
1.197 +StdinSML 1 1 ~10 ~10 (Command Accept);
1.198 +StdinSML 1 1 ~11 ~11 (Command Accept);
1.199 +StdinSML 1 1 ~12 ~12 (Command Accept);
1.200 +StdinSML 1 1 ~13 ~13 (Command Accept);
1.201 +StdinSML 1 1 ~14 ~14 (Command Accept);
1.202 +StdinSML 1 1 ~15 ~15 (Command Accept);
1.203 +StdinSML 1 1 ~16 ~16 (Command Accept);
1.204 +StdinSML 1 1 ~17 ~17 (Command Accept);
1.205 +StdinSML 1 1 ~18 ~18 (Command Accept);
1.206 +StdinSML 1 1 ~19 ~19 (Command Accept);
1.207 +val (_,1,1,_,[],[FormKF (_,_,_,_,f),Request "Accept ?"],_) = it;
1.208 +if f="[x = 4]" then () else raise error "new behaviour in test-example[x=4]";
1.209 +
1.210 +val (_,1,1,~20,[],[Request "start another example",End_Proof],_) =
1.211 +StdinSML 1 1 ~20 ~20 (Command Accept);
1.212 +-------------------------------------------------------------------*)
1.213 +
1.214 +
1.215 +
1.216 +" _________________ exampel [x =(-12)/5] ________________ ";
1.217 +" _________________ exampel [x =(-12)/5] ________________ ";
1.218 +proofs:= []; dials:=([],[],[]);
1.219 +StdinSML 0 0 0 0 New_User;
1.220 +StdinSML 1 0 0 0 New_Proof;
1.221 +val fmz = ["equality (sqrt(9+4*x)=sqrt x + sqrt(-3+x))",
1.222 + "solveFor x","errorBound (eps=0)",
1.223 + "solutions L"];
1.224 +val (dI',pI',mI') =
1.225 + ("Test.thy",["squareroot","univariate","equation","test"],
1.226 + ("Test.thy","sqrt-equ-test"));
1.227 +"--- s1 ---";
1.228 +val (_,1,1,1,[],[_,_,FormKF (_,_,_,_,f),req],_) =
1.229 +StdinSML 1 1 1 1 (RuleFK (Init_Proof (fmz,(dI',pI',mI'))));
1.230 +
1.231 +StdinSML 1 1 ~1 ~1 (Command SpeedMinus);
1.232 +StdinSML 1 1 ~1 ~1 (Command SpeedMinus);
1.233 +StdinSML 1 1 ~1 ~1 (Command Accept);(*->rule*)
1.234 +StdinSML 1 1 ~1 ~1 (Command Accept);(*->form*)
1.235 +val (_,_,_,_,_,dats,_) =
1.236 +StdinSML 1 1 ~2 ~2 (Command Accept);(*->rule*)
1.237 +StdinSML 1 1 ~2 ~2 (Command Accept);(*->form*)
1.238 +
1.239 +
1.240 +StdinSML 1 1 ~3 ~3 (Command ActivePlus);
1.241 +StdinSML 1 1 ~3 ~3 (Command ActivePlus);(*act=2: SelRule..PutRuleRes,Tt*)
1.242 +StdinSML 1 1 ~3 ~3 (RuleFK (Rewrite_Set "rearrange_assoc"));
1.243 +StdinSML 1 1 ~4 ~4 (Command Accept);
1.244 +StdinSML 1 1 ~4 ~4 (RuleFK (Rewrite_Set "isolate_root"));
1.245 +StdinSML 1 1 ~5 ~5 (Command Accept);
1.246 +StdinSML 1 1 ~5 ~5 (RuleFK (Rewrite_Set "Test_simplify"));
1.247 +StdinSML 1 1 ~6 ~6 (Command Accept);
1.248 +
1.249 +
1.250 +StdinSML 1 1 ~6 ~6 (Command SpeedPlus);
1.251 +StdinSML 1 1 ~6 ~6 (Command SpeedPlus);(*act=2: SelRule..SelRule*)
1.252 +StdinSML 1 1 ~6 ~6 (RuleFK (Rewrite ("square_equation_left","")));
1.253 +StdinSML 1 1 ~7 ~7 (RuleFK (Rewrite_Set "Test_simplify"));
1.254 +StdinSML 1 1 ~8 ~8 (RuleFK (Rewrite_Set "rearrange_assoc"));
1.255 +
1.256 +
1.257 +StdinSML 1 1 ~9 ~9 (Command YourTurn);
1.258 +StdinSML 1 1 ~10 ~10 (Command Accept);
1.259 +StdinSML 1 1 ~11 ~11 (Command Accept);
1.260 +StdinSML 1 1 ~12 ~12 (Command Accept);
1.261 +StdinSML 1 1 ~13 ~13 (Command Accept);
1.262 +StdinSML 1 1 ~14 ~14 (Command Accept);
1.263 +val (_,_,_,_,_,dats,_) =
1.264 +StdinSML 1 1 ~15 ~15 (Command Accept);
1.265 +if dats=[Request "start another example",End_Proof] then ()
1.266 +else raise error "new behaviour in test-example 1: [x =(-12)/5]";
1.267 +
1.268 +
1.269 +" _________________ exampel [x =(-12)/5] Auto ________________ ";
1.270 +" _________________ exampel [x =(-12)/5] Auto ________________ ";
1.271 +proofs:= []; dials:=([],[],[]);
1.272 +StdinSML 0 0 0 0 New_User;
1.273 +StdinSML 1 0 0 0 New_Proof;
1.274 +val fmz = ["equality (sqrt(9+4*x)=sqrt x + sqrt(-3+x))",
1.275 + "solveFor x","errorBound (eps=0)",
1.276 + "solutions L"];
1.277 +val (dI',pI',mI') =
1.278 + ("Test.thy",["squareroot","univariate","equation","test"],
1.279 + ("Test.thy","sqrt-equ-test"));
1.280 +val Script sc = (#scr o get_met) ("Test.thy","sqrt-equ-test");
1.281 +writeln(term2str sc);
1.282 +"--- s1 ---";
1.283 +val (_,1,1,1,[],[_,_,FormKF (_,_,_,_,f),req],_) =
1.284 +StdinSML 1 1 1 1 (RuleFK (Init_Proof (fmz,(dI',pI',mI'))));
1.285 +
1.286 +val (_,_,_,_,_,dats,_) = StdinSML 1 1 ~1 ~1 (Command Auto);
1.287 +val FormKF (~16,Protect,0,Nundef,res) =
1.288 + (last_elem o drop_last o drop_last) dats;
1.289 +if res=(*"[]"*)"[x = -12 / 5]" then ()
1.290 +else raise error "new behaviour in test-example 2: [x =(-12)/5]";
1.291 +
1.292 +
1.293 +
1.294 +" ----------------- differentiate ----------------- ";
1.295 +" ----------------- d_d x (x ^^^ 2 + 3 * x + 4) ----------------- ";
1.296 +proofs:= []; dials:=([],[],[]);
1.297 +StdinSML 0 0 0 0 New_User;
1.298 +StdinSML 1 0 0 0 New_Proof;
1.299 +val fmz = ["functionTerm (d_d x (x ^^^ 2 + 3 * x + 4))",
1.300 + "differentiateFor x","derivative f_'_"];
1.301 +val (dI',pI',mI') =
1.302 + ("Diff.thy",["derivative_of","function"],
1.303 + ("Diff.thy","differentiate_on_R"));
1.304 +StdinSML 1 1 1 1 (RuleFK (Init_Proof (fmz,(dI',pI',mI'))));
1.305 +(*FormKF (~10,Protect,0,Nundef,"#3 + #2 * x")*)
1.306 +(* 25.4.01: remove Error with NotAppl
1.307 + StdinSML 1 1 ~1 ~1 (RuleFK (Rewrite_Set "Test_simplify"));
1.308 + StdinSML 1 1 ~2 ~2 (RuleFK (Rewrite_Inst (["(bdv,x)"],("diff_sum",""))));
1.309 + StdinSML 1 1 ~3 ~3 (RuleFK (Rewrite_Inst (["(bdv,x)"],("diff_const",""))));
1.310 +uncaught exception TYPE ...
1.311 +
1.312 +val uI=1;val pI=1;val acI= ~3;val cI= ~3;
1.313 +val dat=(RuleFK (Rewrite_Inst (["(bdv,x)"],("diff_const",""))));;
1.314 +*)
1.315 +
1.316 +
1.317 +(*18.4.01 tests mit speed*)
1.318 +
1.319 +StdinSML 1 1 ~1 ~1 (Command Accept);
1.320 +
1.321 +StdinSML 1 1 ~2 ~2 (Command SpeedPlus);
1.322 +StdinSML 1 1 ~2 ~2 (Command Accept);
1.323 +
1.324 +StdinSML 1 1 ~4 ~4 (Command SpeedMinus);
1.325 +StdinSML 1 1 ~4 ~4 (Command Accept);
1.326 +
1.327 +StdinSML 1 1 ~5 ~5 (Command Accept);
1.328 +(**)
1.329 +val xxx = StdinSML 1 1 ~6 ~6 (Command Auto);
1.330 +if xxx = ("@@@@@begin@@@@@",1,1,~6,[],
1.331 + [FormKF (~7,Protect,1,Nundef,"2 * x ^^^ (2 - 1) + 3 * d_d x x + 0"),
1.332 + FormKF (~8,Protect,1,Nundef,"2 * x ^^^ (2 - 1) + 3 * 1 + 0"),
1.333 + FormKF (~9,Protect,1,Nundef,"3 + 2 * x"),
1.334 + FormKF (~10,Protect,0,Nundef,"3 + 2 * x"),
1.335 + Request "start another example",End_Proof],"@@@@@end@@@@@")
1.336 +then () else writeln "new behaviour in example d_d x (x ^^^ 2 + 3 * x + 4), SpeedPlus/Minus";
1.337 +
1.338 +
1.339 +" ----------------- d_d x (x ^^^ 2 + x + 1 / x ^^^ 2) ----------------- ";
1.340 +proofs:= []; dials:=([],[],[]);
1.341 +StdinSML 0 0 0 0 New_User;
1.342 +StdinSML 1 0 0 0 New_Proof;
1.343 +val fmz = ["functionTerm (d_d x (x ^^^ 2 + x + 1 / x ^^^ 2))",
1.344 + "differentiateFor x","derivative f_'_"];
1.345 +val (dI',pI',mI') =
1.346 + ("Diff.thy",["derivative_of","function"],
1.347 + ("Diff.thy","differentiate_on_R"));
1.348 +StdinSML 1 1 1 1 (RuleFK (Init_Proof (fmz,(dI',pI',mI'))));
1.349 +StdinSML 1 1 ~1 ~1 (Command Auto);
1.350 +(*FormKF (~12,Protect,0,Nundef,"#1 + (#2 * x + #-2 * x ^^^ #-3)")*)
1.351 +
1.352 +" ----------------- Schalk III S.62 Nr. 34a) --------- ";
1.353 +proofs:= []; dials:=([],[],[]);
1.354 +StdinSML 0 0 0 0 New_User;
1.355 +StdinSML 1 0 0 0 New_Proof;
1.356 +val fmz = ["functionTerm (d_d x ((5 * x ^^^ 2 - 2) * (7 * x + 1)))",
1.357 + "differentiateFor x","derivative f_'_"];
1.358 +val (dI',pI',mI') =
1.359 + ("Diff.thy",["derivative_of","function"],
1.360 + ("Diff.thy","differentiate_on_R"));
1.361 +StdinSML 1 1 1 1 (RuleFK (Init_Proof (fmz,(dI',pI',mI'))));
1.362 +StdinSML 1 1 ~1 ~1 (Command Auto);
1.363 +
1.364 +
1.365 +" ----------------- Schalk III S.62 Nr. 51a) --------- ";
1.366 +proofs:= []; dials:=([],[],[]);
1.367 +StdinSML 0 0 0 0 New_User;
1.368 +StdinSML 1 0 0 0 New_Proof;
1.369 +val fmz = ["functionTerm (d_d x ((x+1)/(x- 1)))",
1.370 + "differentiateFor x","derivative f_'_"];
1.371 +val (dI',pI',mI') =
1.372 + ("Diff.thy",["derivative_of","function"],
1.373 + ("Diff.thy","differentiate_on_R"));
1.374 +StdinSML 1 1 1 1 (RuleFK (Init_Proof (fmz,(dI',pI',mI'))));
1.375 +StdinSML 1 1 ~1 ~1 (Command Auto);
1.376 +(*"#-1 // (#1 + (x ^^^ #2 + #-2 * x)) +\n(x // (#1 + (x ^^^ #2 + #-2 * x)) +\n (#1 + x) * (#-1 // (#1 + (x ^^^ #2 + #-2 * x))))" ----- simplification !?!*)
1.377 +
1.378 +
1.379 +" ----------------- Schalk III S.144 Nr. 408b) --------- ";
1.380 +proofs:= []; dials:=([],[],[]);
1.381 +StdinSML 0 0 0 0 New_User;
1.382 +StdinSML 1 0 0 0 New_Proof;
1.383 +val fmz = ["functionTerm (d_d x (x ^^^ 2 * (ln ((sin x) ^^^ 2))))",
1.384 + "differentiateFor x","derivative f_'_"];
1.385 +val (dI',pI',mI') =
1.386 + ("Diff.thy",["derivative_of","function"],
1.387 + ("Diff.thy","differentiate_on_R"));
1.388 +StdinSML 1 1 1 1 (RuleFK (Init_Proof (fmz,(dI',pI',mI'))));
1.389 +StdinSML 1 1 ~1 ~1 (Command Auto);
1.390 +(*"#2 * (x * ln (sin x ^^^ #2)) +\ncos x * (sin x * (x ^^^ #2 * (#2 // sin x ^^^ #2)))"---- cancel sin x !!!*)
1.391 +
1.392 +
1.393 +" ----------------- Schalk III S.137 Nr. 359g) --------- ";
1.394 +proofs:= []; dials:=([],[],[]);
1.395 +StdinSML 0 0 0 0 New_User;
1.396 +StdinSML 1 0 0 0 New_Proof;
1.397 +val fmz = ["functionTerm (d_d x (sqrt (cos (3*x))))",
1.398 + "differentiateFor x","derivative f_'_"];
1.399 +val (dI',pI',mI') =
1.400 + ("Diff.thy",["derivative_of","function"],
1.401 + ("Diff.thy","differentiate_on_R"));
1.402 +StdinSML 1 1 1 1 (RuleFK (Init_Proof (fmz,(dI',pI',mI'))));
1.403 +StdinSML 1 1 ~1 ~1 (Command Auto);