17 "----------- build verschoenere ----------------------------------"; |
17 "----------- build verschoenere ----------------------------------"; |
18 "----------- met simplification for_polynomials with_minus -------"; |
18 "----------- met simplification for_polynomials with_minus -------"; |
19 "----------- pbl polynom vereinfachen ----------------------------"; |
19 "----------- pbl polynom vereinfachen ----------------------------"; |
20 "----------- met probe fuer_polynom ------------------------------"; |
20 "----------- met probe fuer_polynom ------------------------------"; |
21 "----------- pbl polynom probe -----------------------------------"; |
21 "----------- pbl polynom probe -----------------------------------"; |
|
22 "----------- pbl klammer polynom vereinfachen p.34 ---------------"; |
22 "-----------------------------------------------------------------"; |
23 "-----------------------------------------------------------------"; |
23 "-----------------------------------------------------------------"; |
24 "-----------------------------------------------------------------"; |
24 "-----------------------------------------------------------------"; |
25 "-----------------------------------------------------------------"; |
25 |
26 |
26 |
27 |
197 val ((pt,p),_) = get_calc 1; |
198 val ((pt,p),_) = get_calc 1; |
198 if p = ([], Res) andalso |
199 if p = ([], Res) andalso |
199 term2str (get_obj g_res pt (fst p)) = "3 - 2 * e + 2 * f + 2 * g" |
200 term2str (get_obj g_res pt (fst p)) = "3 - 2 * e + 2 * f + 2 * g" |
200 then () else raise error "polyminus.sml: Vereinfache (3 - 2 * e + 2 * f..."; |
201 then () else raise error "polyminus.sml: Vereinfache (3 - 2 * e + 2 * f..."; |
201 show_pt pt; |
202 show_pt pt; |
202 |
|
203 |
203 |
204 "----------- met probe fuer_polynom ------------------------------"; |
204 "----------- met probe fuer_polynom ------------------------------"; |
205 "----------- met probe fuer_polynom ------------------------------"; |
205 "----------- met probe fuer_polynom ------------------------------"; |
206 "----------- met probe fuer_polynom ------------------------------"; |
206 "----------- met probe fuer_polynom ------------------------------"; |
207 val str = |
207 val str = |
226 ("PolyMinus.thy",["polynom","probe"], |
226 ("PolyMinus.thy",["polynom","probe"], |
227 ["probe","fuer_polynom"]))]; |
227 ["probe","fuer_polynom"]))]; |
228 moveActiveRoot 1; |
228 moveActiveRoot 1; |
229 autoCalculate 1 CompleteCalc; |
229 autoCalculate 1 CompleteCalc; |
230 val ((pt,p),_) = get_calc 1; |
230 val ((pt,p),_) = get_calc 1; |
231 (*if p = ([], Res) andalso |
231 if p = ([], Res) andalso term2str (get_obj g_res pt (fst p)) = "11 = 11" |
232 term2str (get_obj g_res pt (fst p)) = "11 = 11" |
232 then () else raise error "polyminus.sml: Probe 11 = 11"; |
233 then () else raise error "polyminus.sml: Probe 11 = 11";*) |
233 show_pt pt; |
234 show_pt pt; |
234 |
235 |
235 |
236 |
236 "----------- pbl klammer polynom vereinfachen p.34 ---------------"; |
237 |
237 "----------- pbl klammer polynom vereinfachen p.34 ---------------"; |
238 |
238 "----------- pbl klammer polynom vereinfachen p.34 ---------------"; |
239 |
239 states:=[]; |
240 |
240 CalcTree [(["term (2*u - 5 - (3 - 4*u) + (8*u + 9))", |
241 |
241 "normalform N"], |
242 |
242 ("PolyMinus.thy",["klammer","polynom","vereinfachen"], |
243 |
243 ["simplification","for_polynomials","with_parentheses"]))]; |
|
244 moveActiveRoot 1; |
|
245 autoCalculate 1 CompleteCalc; |
|
246 val ((pt,p),_) = get_calc 1; |
|
247 if p = ([], Res) andalso |
|
248 term2str (get_obj g_res pt (fst p)) = "3 - 2 * e + 2 * f + 2 * g" |
|
249 then () else raise error "polyminus.sml: Vereinfache (3 - 2 * e + 2 * f..."; |
|
250 show_pt pt; |
|
251 |
|
252 "----- probe p.34 -----"; |
|
253 states:=[]; |
|
254 CalcTree [(["Pruefe (2*u - 5 - (3 - 4*u) + (8*u + 9) = 1 + 14 * u)", |
|
255 "mitWert [u = 2]", |
|
256 "Geprueft b"], |
|
257 ("PolyMinus.thy",["polynom","probe"], |
|
258 ["probe","fuer_polynom"]))]; |
|
259 moveActiveRoot 1; |
|
260 autoCalculate 1 CompleteCalc; |
|
261 val ((pt,p),_) = get_calc 1; |
|
262 if p = ([], Res) andalso term2str (get_obj g_res pt (fst p)) = "29 = 29" |
|
263 then () else raise error "polyminus.sml: Probe 29 = 29"; |
|
264 show_pt pt; |
244 |
265 |
245 |
266 |
246 (* |
267 (* |
247 use"../smltest/IsacKnowledge/polyminus.sml"; |
268 use"../smltest/IsacKnowledge/polyminus.sml"; |
248 use"polyminus.sml"; |
269 use"polyminus.sml"; |