equal
deleted
inserted
replaced
122 |
122 |
123 val SOME (str, pred) = eval_boollist2sum "" "Atools.boollist2sum" t ""; |
123 val SOME (str, pred) = eval_boollist2sum "" "Atools.boollist2sum" t ""; |
124 if term2str pred = "boollist2sum\n [b1 = k - 2 * q, b2 = k - 2 * q, b3 = k - 2 * q, b4 = k - 2 * q] =\nb1 + b2 + b3 + b4" then () |
124 if term2str pred = "boollist2sum\n [b1 = k - 2 * q, b2 = k - 2 * q, b3 = k - 2 * q, b4 = k - 2 * q] =\nb1 + b2 + b3 + b4" then () |
125 else error "atools.sml diff.behav. in eval_boollist2sum"; |
125 else error "atools.sml diff.behav. in eval_boollist2sum"; |
126 |
126 |
127 trace_rewrite:=true; |
127 trace_rewrite := false; |
128 val srls_ = append_rls "srls_..Berechnung-erstSymbolisch" e_rls |
128 val srls_ = append_rls "srls_..Berechnung-erstSymbolisch" e_rls |
129 [Calc ("Atools.boollist2sum", eval_boollist2sum "")]; |
129 [Calc ("Atools.boollist2sum", eval_boollist2sum "")]; |
130 val t = str2t |
130 val t = str2t |
131 "boollist2sum [b1 = k - 2*q, b2 = k - 2*q, b3 = k - 2*q, b4 = k - 2*q]"; |
131 "boollist2sum [b1 = k - 2*q, b2 = k - 2*q, b3 = k - 2*q, b4 = k - 2*q]"; |
132 case rewrite_set_ thy false srls_ t of SOME _ => () |
132 case rewrite_set_ thy false srls_ t of SOME _ => () |
236 "x ^^^ 2 + (-1 * (b * x) + a * (b + -1 * x)) = 0"; |
236 "x ^^^ 2 + (-1 * (b * x) + a * (b + -1 * x)) = 0"; |
237 (*da sind wir fast am Ziel: make_polynomial_in 'a' sollte ergeben |
237 (*da sind wir fast am Ziel: make_polynomial_in 'a' sollte ergeben |
238 "x ^^^ 2 + (-1 * (b * x)) + (b + -1 * x) * a = 0"*) |
238 "x ^^^ 2 + (-1 * (b * x)) + (b + -1 * x) * a = 0"*) |
239 |
239 |
240 (*das rewriting l"asst sich beobachten mit |
240 (*das rewriting l"asst sich beobachten mit |
241 trace_rewrite:=true; |
241 trace_rewrite := false; |
242 *) |
242 *) |
243 |
243 |
244 "------15.11.02 --------------------------"; |
244 "------15.11.02 --------------------------"; |
245 val t = (term_of o the o (parse thy)) "1 + a * x + b * x"; |
245 val t = (term_of o the o (parse thy)) "1 + a * x + b * x"; |
246 val bdv = (term_of o the o (parse thy)) "bdv"; |
246 val bdv = (term_of o the o (parse thy)) "bdv"; |
247 val a = (term_of o the o (parse thy)) "a"; |
247 val a = (term_of o the o (parse thy)) "a"; |
248 |
248 |
249 trace_rewrite:=true; |
249 trace_rewrite := false; |
250 (* Anwenden einer Regelmenge aus Termorder.ML: *) |
250 (* Anwenden einer Regelmenge aus Termorder.ML: *) |
251 val SOME (t,_) = |
251 val SOME (t,_) = |
252 rewrite_set_inst_ thy false [(bdv,a)] make_polynomial_in t; |
252 rewrite_set_inst_ thy false [(bdv,a)] make_polynomial_in t; |
253 term2str t; |
253 term2str t; |
254 val SOME (t,_) = |
254 val SOME (t,_) = |