|
1 (* testdaten f"ur isac demo0 |
|
2 WN 31.10.00, .., 18.1.01 |
|
3 use"tests/testdaten.sml"; |
|
4 use"testdaten.sml"; |
|
5 |
|
6 proofs:= []; dials:=([],[],[]); |
|
7 *) |
|
8 " _________________ exampel [x=4]: Rules 4.2.01a________________ "; |
|
9 " _________________ exampel [x=4]: Rules 4.2.01b________________ "; |
|
10 " _________________ exampel [x=4]: tutor active ________________ "; |
|
11 " _________________ exampel [x=4] ________________ "; |
|
12 " _________________ exampel [x =(-12)/5] ________________ "; |
|
13 " _________________ exampel [x =(-12)/5] Auto ________________ "; |
|
14 " ----------------- d_d x (x ^^^ 2 + 3 * x + 4) ----------------- "; |
|
15 " ----------------- d_d x (x ^^^ 2 + x + 1 / x ^^^ 2) ----------------- "; |
|
16 " ----------------- Schalk III S.62 Nr. 51a) --------- "; |
|
17 " ----------------- Schalk III S.144 Nr. 408b) --------- "; |
|
18 " ----------------- Schalk III S.137 Nr. 359g) --------- "; |
|
19 |
|
20 |
|
21 |
|
22 |
|
23 |
|
24 " _________________ exampel [x=4]: Rules 4.2.01a________________ "; |
|
25 " _________________ exampel [x=4]: Rules 4.2.01a________________ "; |
|
26 val (_,uI,0,0,[],[New_User],_) = StdinSML 0 0 0 0 New_User; |
|
27 val (_,_,pI,0,[],[New_Proof],_) = StdinSML uI 0 0 0 New_Proof; |
|
28 val fmz = ["equality (sqrt(9+4*x)=sqrt x + sqrt(5+x))", |
|
29 "solveFor x","errorBound (eps=0)", |
|
30 "solutions L"]; |
|
31 val (dI',pI',mI') = |
|
32 ("Test.thy",["squareroot","univariate","equation","test"], |
|
33 ("Test.thy","sqrt-equ-test")); |
|
34 "--- 0 ---"; |
|
35 StdinSML uI pI 1 1 (RuleFK (Init_Proof (fmz,(dI',pI',mI')))); |
|
36 "--- 1 ---"; |
|
37 StdinSML uI pI ~1 ~1 (Command Accept); |
|
38 (* square_equation_left |
|
39 "#9 + #4 * x = (sqrt x + sqrt (#5 + x)) ^^^ #2"*) |
|
40 "--- 2 ---"; |
|
41 StdinSML uI pI ~2 ~2 (Command Rules); |
|
42 "--- 3 ---"; |
|
43 StdinSML uI pI ~2 ~2 (RuleFK (Rewrite_Set "Test_simplify")); |
|
44 "--- 4 ---"; |
|
45 val (_,_,_,_,_,[Error_ _ (*"Error_ Test_simplify not applicable to ..*), |
|
46 Request "apply a rule !"],_) = |
|
47 StdinSML uI pI ~3 ~3 (RuleFK (Rewrite_Set "Test_simplify")); |
|
48 |
|
49 |
|
50 " _________________ exampel [x=4]: Rules 4.2.01b________________ "; |
|
51 " _________________ exampel [x=4]: Rules 4.2.01b________________ "; |
|
52 val (_,uI,0,0,[],[New_User],_) = StdinSML 0 0 0 0 New_User; |
|
53 val (_,_,pI,0,[],[New_Proof],_) = StdinSML uI 0 0 0 New_Proof; |
|
54 val fmz = ["equality (sqrt(9+4*x)=sqrt x + sqrt(5+x))", |
|
55 "solveFor x","errorBound (eps=0)", |
|
56 "solutions L"]; |
|
57 val (dI',pI',mI') = |
|
58 ("Test.thy",["squareroot","univariate","equation","test"], |
|
59 ("Test.thy","sqrt-equ-test")); |
|
60 "--- 0 ---"; |
|
61 StdinSML uI pI 1 1 (RuleFK (Init_Proof (fmz,(dI',pI',mI')))); |
|
62 "--- 1 ---"; |
|
63 StdinSML uI pI ~1 ~1 (Command Accept); |
|
64 (* square_equation_left |
|
65 "#9 + #4 * x = (sqrt x + sqrt (#5 + x)) ^^^ #2"*) |
|
66 "--- 2 ---"; |
|
67 StdinSML uI pI ~2 ~2 (Command Rules); |
|
68 "--- 3 ---"; |
|
69 val (_,_,_,_,_, |
|
70 [Error_ _ (*"Error_ 'square_equation_left' not applicable to: #9 *), |
|
71 Select _, Request "select a rule !"],_) = |
|
72 StdinSML uI pI ~2 ~2 (RuleFK (Rewrite ("square_equation_left",""))); |
|
73 |
|
74 |
|
75 " _________________ exampel [x=4]: tutor active ________________ "; |
|
76 " _________________ exampel [x=4]: tutor active ________________ "; |
|
77 val (_,uI,0,0,[],[New_User],_) = StdinSML 0 0 0 0 New_User; |
|
78 val (_,_,pI,0,[],[New_Proof],_) = StdinSML uI 0 0 0 New_Proof; |
|
79 val fmz = ["equality (sqrt(9+4*x)=sqrt x + sqrt(5+x))", |
|
80 "solveFor x","errorBound (eps=0)", |
|
81 "solutions L"]; |
|
82 val (dI',pI',mI') = |
|
83 ("Test.thy",["squareroot","univariate","equation","test"], |
|
84 ("Test.thy","sqrt-equ-test")); |
|
85 "--- s1 ---"; |
|
86 StdinSML uI pI 1 1 (RuleFK (Init_Proof (fmz,(dI',pI',mI')))); |
|
87 "--- 1 ---"; |
|
88 StdinSML uI pI ~1 ~1 (Command Accept); |
|
89 (* square_equation_left |
|
90 "#9 + #4 * x = (sqrt x + sqrt (#5 + x)) ^^^ #2"*) |
|
91 "--- 2 ---"; |
|
92 StdinSML uI pI ~2 ~2 (Command Accept); |
|
93 (* Test_simplify |
|
94 "#9 + #4 * x = #5 + (#2 * x + #2 * sqrt (x ^^^ #2 + #5 * x))"*) |
|
95 "--- 3 ---"; |
|
96 StdinSML uI pI ~3 ~3 (Command Accept); |
|
97 (* rearrange_assoc |
|
98 "#9 + #4 * x = #5 + #2 * x + #2 * sqrt (x ^^^ #2 + #5 * x)"*) |
|
99 "--- 4 ---"; |
|
100 StdinSML uI pI ~4 ~4 (Command Accept); |
|
101 (* isolate_root |
|
102 "sqrt (x ^^^ #2 + #5 * x) = (#5 + #2 * x + #-1 * (#9 + #4 * x)) // (#-1 *#2)"*) |
|
103 "--- 5 ---"; |
|
104 StdinSML uI pI ~5 ~5 (Command Accept); |
|
105 (* Test_simplify |
|
106 "sqrt (x ^^^ #2 + #5 * x) = #2 + x"*) |
|
107 "--- 6 ---"; |
|
108 StdinSML uI pI ~6 ~6 (Command Accept); |
|
109 (* square_equation_left |
|
110 "x ^^^ #2 + #5 * x = (#2 + x) ^^^ #2"*) |
|
111 "--- 7 ---"; |
|
112 StdinSML uI pI ~7 ~7 (Command Accept); |
|
113 (* Test_simplify |
|
114 "x ^^^ #2 + #5 * x = #4 + (x ^^^ #2 + #4 * x)"*) |
|
115 "--- 8 ---"; |
|
116 StdinSML uI pI ~8 ~8 (Command Accept); |
|
117 (* rearrange_assoc |
|
118 "x ^^^ #2 + #5 * x = #4 + x ^^^ #2 + #4 * x"*) |
|
119 "--- 9 ---"; |
|
120 StdinSML uI pI ~9 ~9 (Command Accept); |
|
121 (* Test_simplify |
|
122 "x ^^^ #2 + #5 * x = #4 + (x ^^^ #2 + #4 * x)"*) |
|
123 "--- 10 ---"; |
|
124 StdinSML uI pI ~10 ~10 (Command Accept); |
|
125 (* norm_equation |
|
126 "x ^^^ #2 + #5 * x + #-1 * (#4 + (x ^^^ #2 + #4 * x)) = #0"*) |
|
127 "--- 11 ---"; |
|
128 StdinSML uI pI ~11 ~11 (Command Accept); |
|
129 (* Test_simplify |
|
130 "#-4 + x = #0"*) |
|
131 "--- 12 ---"; |
|
132 StdinSML uI pI ~12 ~12 (Command Accept); |
|
133 (* isolate_bdv |
|
134 "x = #0 + #-1 * #-4" *) |
|
135 "--- 13 ---"; |
|
136 StdinSML uI pI ~13 ~13 (Command Accept); |
|
137 (* Test_simplify |
|
138 "x = #4" *) |
|
139 "--- 14 ---"; |
|
140 StdinSML uI pI ~14 ~14 (Command Accept); |
|
141 val (_,_,1,~14,[],[RuleKF (_,m),FormKF (_,_,_,_,f),Request "Accept ?"],_) = it; |
|
142 if m = Check_Postcond ["squareroot","univariate","equation","test"] |
|
143 andalso f = "[x = 4]" then () |
|
144 else raise error "new behaviour in: exampel [x=4]: tutor active"; |
|
145 "--- 15 ---"; |
|
146 StdinSML uI pI ~15 ~15 (Command Accept); |
|
147 (* Request "start another example"*) |
|
148 |
|
149 (*---- after restruct. kb 18.9.02 ---- (same is in test-FE...) |
|
150 " _________________ exampel [x=4] ________________ "; |
|
151 " _________________ exampel [x=4] ________________ "; |
|
152 proofs:= []; dials:=([],[],[]); |
|
153 StdinSML 0 0 0 0 New_User; |
|
154 StdinSML 1 0 0 0 New_Proof; |
|
155 val fmz = ["equality (sqrt(9+4*x)=sqrt x + sqrt(5+x))", |
|
156 "solveFor x","errorBound (eps=0)", |
|
157 "solutions L"]; |
|
158 val (dI',pI',mI') = |
|
159 ("Test.thy",["squareroot","univariate","equation","test"], |
|
160 ("Test.thy","sqrt-equ-test")); |
|
161 "--- s1 ---"; |
|
162 val (_,1,1,1,[],[_,_,FormKF (_,_,_,_,f),req],_) = |
|
163 StdinSML 1 1 1 1 (RuleFK (Init_Proof (fmz,(dI',pI',mI')))); |
|
164 |
|
165 StdinSML 1 1 ~1 ~1 (Command ActivePlus); |
|
166 StdinSML 1 1 ~1 ~1 (Command ActivePlus); |
|
167 StdinSML 1 1 ~1 ~1 (Command ActivePlus); |
|
168 StdinSML 1 1 ~1 ~1 (Command ActivePlus);(*acti=4..SelRule*) |
|
169 |
|
170 "--- !!! x1 --- strange choice"; (* hier nochmals spec !*) |
|
171 StdinSML 1 1 ~1 ~1 (RuleFK (Rewrite_Set "norm_equation")); |
|
172 "--- !!! x2 --- ME knows nxt_step"; |
|
173 StdinSML 1 1 ~2 ~2 (RuleFK (Rewrite_Set "Test_simplify")); |
|
174 "--- !!! x3 --- helpless !!!"; |
|
175 val (_,_,_,_,_,[FormKF (_,_,_,_,res),_,requ],_) = |
|
176 StdinSML 1 1 ~3 ~3 (RuleFK (Rewrite_Set "rearrange_assoc")); |
|
177 "--- !!! x4 ---"; |
|
178 val (_,_,_,_,_,[FormKF (_,_,_,_,res),_,requ],_) = |
|
179 StdinSML 1 1 ~4 ~4 (RuleFK (Rewrite_Set "isolate_root")); |
|
180 "--- !!! x5 --- back at original equation !!!"; |
|
181 val (_,_,_,_,_,[FormKF (_,_,_,_,res),_,requ],_) = |
|
182 StdinSML 1 1 ~5 ~5 (RuleFK (Rewrite_Set "Test_simplify")); |
|
183 if res="sqrt (9 + 4 * x) = sqrt x + sqrt (5 + x)" |
|
184 then () else raise error "new behaviour in test-example"; |
|
185 "--- !!! x6 --- not applicable"; |
|
186 val (_,_,_,_,_,[Error_ err,_,requ],_) = |
|
187 StdinSML 1 1 ~6 ~6 (RuleFK (Rewrite_Set "Test_simplify")); |
|
188 (*val (_,_,_,_,_,[RuleKF r,requ],_) =*) |
|
189 val (_,_,_,_,_,ios,_) = |
|
190 StdinSML 1 1 ~6 ~6 (Command YourTurn); |
|
191 StdinSML 1 1 ~7 ~7 (Command Accept); |
|
192 StdinSML 1 1 ~8 ~8 (Command Accept); |
|
193 StdinSML 1 1 ~9 ~9 (Command Accept); |
|
194 StdinSML 1 1 ~10 ~10 (Command Accept); |
|
195 StdinSML 1 1 ~11 ~11 (Command Accept); |
|
196 StdinSML 1 1 ~12 ~12 (Command Accept); |
|
197 StdinSML 1 1 ~13 ~13 (Command Accept); |
|
198 StdinSML 1 1 ~14 ~14 (Command Accept); |
|
199 StdinSML 1 1 ~15 ~15 (Command Accept); |
|
200 StdinSML 1 1 ~16 ~16 (Command Accept); |
|
201 StdinSML 1 1 ~17 ~17 (Command Accept); |
|
202 StdinSML 1 1 ~18 ~18 (Command Accept); |
|
203 StdinSML 1 1 ~19 ~19 (Command Accept); |
|
204 val (_,1,1,_,[],[FormKF (_,_,_,_,f),Request "Accept ?"],_) = it; |
|
205 if f="[x = 4]" then () else raise error "new behaviour in test-example[x=4]"; |
|
206 |
|
207 val (_,1,1,~20,[],[Request "start another example",End_Proof],_) = |
|
208 StdinSML 1 1 ~20 ~20 (Command Accept); |
|
209 -------------------------------------------------------------------*) |
|
210 |
|
211 |
|
212 |
|
213 " _________________ exampel [x =(-12)/5] ________________ "; |
|
214 " _________________ exampel [x =(-12)/5] ________________ "; |
|
215 proofs:= []; dials:=([],[],[]); |
|
216 StdinSML 0 0 0 0 New_User; |
|
217 StdinSML 1 0 0 0 New_Proof; |
|
218 val fmz = ["equality (sqrt(9+4*x)=sqrt x + sqrt(-3+x))", |
|
219 "solveFor x","errorBound (eps=0)", |
|
220 "solutions L"]; |
|
221 val (dI',pI',mI') = |
|
222 ("Test.thy",["squareroot","univariate","equation","test"], |
|
223 ("Test.thy","sqrt-equ-test")); |
|
224 "--- s1 ---"; |
|
225 val (_,1,1,1,[],[_,_,FormKF (_,_,_,_,f),req],_) = |
|
226 StdinSML 1 1 1 1 (RuleFK (Init_Proof (fmz,(dI',pI',mI')))); |
|
227 |
|
228 StdinSML 1 1 ~1 ~1 (Command SpeedMinus); |
|
229 StdinSML 1 1 ~1 ~1 (Command SpeedMinus); |
|
230 StdinSML 1 1 ~1 ~1 (Command Accept);(*->rule*) |
|
231 StdinSML 1 1 ~1 ~1 (Command Accept);(*->form*) |
|
232 val (_,_,_,_,_,dats,_) = |
|
233 StdinSML 1 1 ~2 ~2 (Command Accept);(*->rule*) |
|
234 StdinSML 1 1 ~2 ~2 (Command Accept);(*->form*) |
|
235 |
|
236 |
|
237 StdinSML 1 1 ~3 ~3 (Command ActivePlus); |
|
238 StdinSML 1 1 ~3 ~3 (Command ActivePlus);(*act=2: SelRule..PutRuleRes,Tt*) |
|
239 StdinSML 1 1 ~3 ~3 (RuleFK (Rewrite_Set "rearrange_assoc")); |
|
240 StdinSML 1 1 ~4 ~4 (Command Accept); |
|
241 StdinSML 1 1 ~4 ~4 (RuleFK (Rewrite_Set "isolate_root")); |
|
242 StdinSML 1 1 ~5 ~5 (Command Accept); |
|
243 StdinSML 1 1 ~5 ~5 (RuleFK (Rewrite_Set "Test_simplify")); |
|
244 StdinSML 1 1 ~6 ~6 (Command Accept); |
|
245 |
|
246 |
|
247 StdinSML 1 1 ~6 ~6 (Command SpeedPlus); |
|
248 StdinSML 1 1 ~6 ~6 (Command SpeedPlus);(*act=2: SelRule..SelRule*) |
|
249 StdinSML 1 1 ~6 ~6 (RuleFK (Rewrite ("square_equation_left",""))); |
|
250 StdinSML 1 1 ~7 ~7 (RuleFK (Rewrite_Set "Test_simplify")); |
|
251 StdinSML 1 1 ~8 ~8 (RuleFK (Rewrite_Set "rearrange_assoc")); |
|
252 |
|
253 |
|
254 StdinSML 1 1 ~9 ~9 (Command YourTurn); |
|
255 StdinSML 1 1 ~10 ~10 (Command Accept); |
|
256 StdinSML 1 1 ~11 ~11 (Command Accept); |
|
257 StdinSML 1 1 ~12 ~12 (Command Accept); |
|
258 StdinSML 1 1 ~13 ~13 (Command Accept); |
|
259 StdinSML 1 1 ~14 ~14 (Command Accept); |
|
260 val (_,_,_,_,_,dats,_) = |
|
261 StdinSML 1 1 ~15 ~15 (Command Accept); |
|
262 if dats=[Request "start another example",End_Proof] then () |
|
263 else raise error "new behaviour in test-example 1: [x =(-12)/5]"; |
|
264 |
|
265 |
|
266 " _________________ exampel [x =(-12)/5] Auto ________________ "; |
|
267 " _________________ exampel [x =(-12)/5] Auto ________________ "; |
|
268 proofs:= []; dials:=([],[],[]); |
|
269 StdinSML 0 0 0 0 New_User; |
|
270 StdinSML 1 0 0 0 New_Proof; |
|
271 val fmz = ["equality (sqrt(9+4*x)=sqrt x + sqrt(-3+x))", |
|
272 "solveFor x","errorBound (eps=0)", |
|
273 "solutions L"]; |
|
274 val (dI',pI',mI') = |
|
275 ("Test.thy",["squareroot","univariate","equation","test"], |
|
276 ("Test.thy","sqrt-equ-test")); |
|
277 val Script sc = (#scr o get_met) ("Test.thy","sqrt-equ-test"); |
|
278 writeln(term2str sc); |
|
279 "--- s1 ---"; |
|
280 val (_,1,1,1,[],[_,_,FormKF (_,_,_,_,f),req],_) = |
|
281 StdinSML 1 1 1 1 (RuleFK (Init_Proof (fmz,(dI',pI',mI')))); |
|
282 |
|
283 val (_,_,_,_,_,dats,_) = StdinSML 1 1 ~1 ~1 (Command Auto); |
|
284 val FormKF (~16,Protect,0,Nundef,res) = |
|
285 (last_elem o drop_last o drop_last) dats; |
|
286 if res=(*"[]"*)"[x = -12 / 5]" then () |
|
287 else raise error "new behaviour in test-example 2: [x =(-12)/5]"; |
|
288 |
|
289 |
|
290 |
|
291 " ----------------- differentiate ----------------- "; |
|
292 " ----------------- d_d x (x ^^^ 2 + 3 * x + 4) ----------------- "; |
|
293 proofs:= []; dials:=([],[],[]); |
|
294 StdinSML 0 0 0 0 New_User; |
|
295 StdinSML 1 0 0 0 New_Proof; |
|
296 val fmz = ["functionTerm (d_d x (x ^^^ 2 + 3 * x + 4))", |
|
297 "differentiateFor x","derivative f_'_"]; |
|
298 val (dI',pI',mI') = |
|
299 ("Diff.thy",["derivative_of","function"], |
|
300 ("Diff.thy","differentiate_on_R")); |
|
301 StdinSML 1 1 1 1 (RuleFK (Init_Proof (fmz,(dI',pI',mI')))); |
|
302 (*FormKF (~10,Protect,0,Nundef,"#3 + #2 * x")*) |
|
303 (* 25.4.01: remove Error with NotAppl |
|
304 StdinSML 1 1 ~1 ~1 (RuleFK (Rewrite_Set "Test_simplify")); |
|
305 StdinSML 1 1 ~2 ~2 (RuleFK (Rewrite_Inst (["(bdv,x)"],("diff_sum","")))); |
|
306 StdinSML 1 1 ~3 ~3 (RuleFK (Rewrite_Inst (["(bdv,x)"],("diff_const","")))); |
|
307 uncaught exception TYPE ... |
|
308 |
|
309 val uI=1;val pI=1;val acI= ~3;val cI= ~3; |
|
310 val dat=(RuleFK (Rewrite_Inst (["(bdv,x)"],("diff_const",""))));; |
|
311 *) |
|
312 |
|
313 |
|
314 (*18.4.01 tests mit speed*) |
|
315 |
|
316 StdinSML 1 1 ~1 ~1 (Command Accept); |
|
317 |
|
318 StdinSML 1 1 ~2 ~2 (Command SpeedPlus); |
|
319 StdinSML 1 1 ~2 ~2 (Command Accept); |
|
320 |
|
321 StdinSML 1 1 ~4 ~4 (Command SpeedMinus); |
|
322 StdinSML 1 1 ~4 ~4 (Command Accept); |
|
323 |
|
324 StdinSML 1 1 ~5 ~5 (Command Accept); |
|
325 (**) |
|
326 val xxx = StdinSML 1 1 ~6 ~6 (Command Auto); |
|
327 if xxx = ("@@@@@begin@@@@@",1,1,~6,[], |
|
328 [FormKF (~7,Protect,1,Nundef,"2 * x ^^^ (2 - 1) + 3 * d_d x x + 0"), |
|
329 FormKF (~8,Protect,1,Nundef,"2 * x ^^^ (2 - 1) + 3 * 1 + 0"), |
|
330 FormKF (~9,Protect,1,Nundef,"3 + 2 * x"), |
|
331 FormKF (~10,Protect,0,Nundef,"3 + 2 * x"), |
|
332 Request "start another example",End_Proof],"@@@@@end@@@@@") |
|
333 then () else writeln "new behaviour in example d_d x (x ^^^ 2 + 3 * x + 4), SpeedPlus/Minus"; |
|
334 |
|
335 |
|
336 " ----------------- d_d x (x ^^^ 2 + x + 1 / x ^^^ 2) ----------------- "; |
|
337 proofs:= []; dials:=([],[],[]); |
|
338 StdinSML 0 0 0 0 New_User; |
|
339 StdinSML 1 0 0 0 New_Proof; |
|
340 val fmz = ["functionTerm (d_d x (x ^^^ 2 + x + 1 / x ^^^ 2))", |
|
341 "differentiateFor x","derivative f_'_"]; |
|
342 val (dI',pI',mI') = |
|
343 ("Diff.thy",["derivative_of","function"], |
|
344 ("Diff.thy","differentiate_on_R")); |
|
345 StdinSML 1 1 1 1 (RuleFK (Init_Proof (fmz,(dI',pI',mI')))); |
|
346 StdinSML 1 1 ~1 ~1 (Command Auto); |
|
347 (*FormKF (~12,Protect,0,Nundef,"#1 + (#2 * x + #-2 * x ^^^ #-3)")*) |
|
348 |
|
349 " ----------------- Schalk III S.62 Nr. 34a) --------- "; |
|
350 proofs:= []; dials:=([],[],[]); |
|
351 StdinSML 0 0 0 0 New_User; |
|
352 StdinSML 1 0 0 0 New_Proof; |
|
353 val fmz = ["functionTerm (d_d x ((5 * x ^^^ 2 - 2) * (7 * x + 1)))", |
|
354 "differentiateFor x","derivative f_'_"]; |
|
355 val (dI',pI',mI') = |
|
356 ("Diff.thy",["derivative_of","function"], |
|
357 ("Diff.thy","differentiate_on_R")); |
|
358 StdinSML 1 1 1 1 (RuleFK (Init_Proof (fmz,(dI',pI',mI')))); |
|
359 StdinSML 1 1 ~1 ~1 (Command Auto); |
|
360 |
|
361 |
|
362 " ----------------- Schalk III S.62 Nr. 51a) --------- "; |
|
363 proofs:= []; dials:=([],[],[]); |
|
364 StdinSML 0 0 0 0 New_User; |
|
365 StdinSML 1 0 0 0 New_Proof; |
|
366 val fmz = ["functionTerm (d_d x ((x+1)/(x- 1)))", |
|
367 "differentiateFor x","derivative f_'_"]; |
|
368 val (dI',pI',mI') = |
|
369 ("Diff.thy",["derivative_of","function"], |
|
370 ("Diff.thy","differentiate_on_R")); |
|
371 StdinSML 1 1 1 1 (RuleFK (Init_Proof (fmz,(dI',pI',mI')))); |
|
372 StdinSML 1 1 ~1 ~1 (Command Auto); |
|
373 (*"#-1 // (#1 + (x ^^^ #2 + #-2 * x)) +\n(x // (#1 + (x ^^^ #2 + #-2 * x)) +\n (#1 + x) * (#-1 // (#1 + (x ^^^ #2 + #-2 * x))))" ----- simplification !?!*) |
|
374 |
|
375 |
|
376 " ----------------- Schalk III S.144 Nr. 408b) --------- "; |
|
377 proofs:= []; dials:=([],[],[]); |
|
378 StdinSML 0 0 0 0 New_User; |
|
379 StdinSML 1 0 0 0 New_Proof; |
|
380 val fmz = ["functionTerm (d_d x (x ^^^ 2 * (ln ((sin x) ^^^ 2))))", |
|
381 "differentiateFor x","derivative f_'_"]; |
|
382 val (dI',pI',mI') = |
|
383 ("Diff.thy",["derivative_of","function"], |
|
384 ("Diff.thy","differentiate_on_R")); |
|
385 StdinSML 1 1 1 1 (RuleFK (Init_Proof (fmz,(dI',pI',mI')))); |
|
386 StdinSML 1 1 ~1 ~1 (Command Auto); |
|
387 (*"#2 * (x * ln (sin x ^^^ #2)) +\ncos x * (sin x * (x ^^^ #2 * (#2 // sin x ^^^ #2)))"---- cancel sin x !!!*) |
|
388 |
|
389 |
|
390 " ----------------- Schalk III S.137 Nr. 359g) --------- "; |
|
391 proofs:= []; dials:=([],[],[]); |
|
392 StdinSML 0 0 0 0 New_User; |
|
393 StdinSML 1 0 0 0 New_Proof; |
|
394 val fmz = ["functionTerm (d_d x (sqrt (cos (3*x))))", |
|
395 "differentiateFor x","derivative f_'_"]; |
|
396 val (dI',pI',mI') = |
|
397 ("Diff.thy",["derivative_of","function"], |
|
398 ("Diff.thy","differentiate_on_R")); |
|
399 StdinSML 1 1 1 1 (RuleFK (Init_Proof (fmz,(dI',pI',mI')))); |
|
400 StdinSML 1 1 ~1 ~1 (Command Auto); |