15 "----------- build predicate for +- ordering ---------------------"; |
15 "----------- build predicate for +- ordering ---------------------"; |
16 "----------- build fasse_zusammen --------------------------------"; |
16 "----------- build fasse_zusammen --------------------------------"; |
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 ------------------------------"; |
|
21 "----------- pbl polynom probe -----------------------------------"; |
20 "-----------------------------------------------------------------"; |
22 "-----------------------------------------------------------------"; |
21 "-----------------------------------------------------------------"; |
23 "-----------------------------------------------------------------"; |
22 "-----------------------------------------------------------------"; |
24 "-----------------------------------------------------------------"; |
23 |
25 |
24 |
26 |
193 moveActiveRoot 1; |
195 moveActiveRoot 1; |
194 autoCalculate 1 CompleteCalc; |
196 autoCalculate 1 CompleteCalc; |
195 val ((pt,p),_) = get_calc 1; |
197 val ((pt,p),_) = get_calc 1; |
196 if p = ([], Res) andalso |
198 if p = ([], Res) andalso |
197 term2str (get_obj g_res pt (fst p)) = "3 - 2 * e + 2 * f + 2 * g" |
199 term2str (get_obj g_res pt (fst p)) = "3 - 2 * e + 2 * f + 2 * g" |
198 then () else raise error "biegelinie.sml: 1st biegelin.7.27 changed"; |
200 then () else raise error "polyminus.sml: Vereinfache (3 - 2 * e + 2 * f..."; |
199 show_pt pt; |
201 show_pt pt; |
200 |
202 |
201 |
203 |
202 |
204 "----------- met probe fuer_polynom ------------------------------"; |
203 |
205 "----------- met probe fuer_polynom ------------------------------"; |
|
206 "----------- met probe fuer_polynom ------------------------------"; |
|
207 val str = |
|
208 "Script ProbeScript (e_::bool) (ws_::bool list) =\ |
|
209 \ (let e_ = Take e_; \ |
|
210 \ e_ = Substitute ws_ e_ \ |
|
211 \ in (Repeat((Try (Repeat (Calculate times))) @@ \ |
|
212 \ (Try (Repeat (Calculate plus ))) @@ \ |
|
213 \ (Try (Repeat (Calculate minus))))) e_)" |
|
214 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str; |
|
215 atomty sc; |
|
216 |
|
217 |
|
218 "----------- pbl polynom probe -----------------------------------"; |
|
219 "----------- pbl polynom probe -----------------------------------"; |
|
220 "----------- pbl polynom probe -----------------------------------"; |
|
221 states:=[]; |
|
222 CalcTree [(["Pruefe (5*e + 6*f - 8*g - 9 - 7*e - 4*f + 10*g + 12 =\ |
|
223 \3 - 2 * e + 2 * f + 2 * g)", |
|
224 "mitWert [e = 1, f = 2, g = 3]", |
|
225 "Geprueft b"], |
|
226 ("PolyMinus.thy",["polynom","probe"], |
|
227 ["probe","fuer_polynom"]))]; |
|
228 moveActiveRoot 1; |
|
229 autoCalculate 1 CompleteCalc; |
|
230 val ((pt,p),_) = get_calc 1; |
|
231 (*if p = ([], Res) andalso |
|
232 term2str (get_obj g_res pt (fst p)) = "11 = 11" |
|
233 then () else raise error "polyminus.sml: Probe 11 = 11";*) |
|
234 show_pt pt; |
204 |
235 |
205 |
236 |
206 |
237 |
207 |
238 |
208 |
239 |