equal
deleted
inserted
replaced
47 "-----------------------------------------------------------------"; |
47 "-----------------------------------------------------------------"; |
48 |
48 |
49 "----------- tests on predicates in problems ---------------------"; |
49 "----------- tests on predicates in problems ---------------------"; |
50 "----------- tests on predicates in problems ---------------------"; |
50 "----------- tests on predicates in problems ---------------------"; |
51 "----------- tests on predicates in problems ---------------------"; |
51 "----------- tests on predicates in problems ---------------------"; |
52 (* trace_rewrite:=true; |
52 (* Trace.trace_rewrite:=true; |
53 trace_rewrite:=false; |
53 Trace.trace_rewrite:=false; |
54 *) |
54 *) |
55 val t1 = (Thm.term_of o the o (parse thy)) "lhs (-8 - 2*x + x^^^2 = 0)"; |
55 val t1 = (Thm.term_of o the o (parse thy)) "lhs (-8 - 2*x + x^^^2 = 0)"; |
56 val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t1; |
56 val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t1; |
57 if ((UnparseC.term t) = "-8 - 2 * x + x ^^^ 2") then () |
57 if ((UnparseC.term t) = "-8 - 2 * x + x ^^^ 2") then () |
58 else error "polyeq.sml: diff.behav. in lhs"; |
58 else error "polyeq.sml: diff.behav. in lhs"; |
158 "x ^^^ 2 + (-1 * (b * x) + a * (b + -1 * x)) = 0"; |
158 "x ^^^ 2 + (-1 * (b * x) + a * (b + -1 * x)) = 0"; |
159 (*da sind wir fast am Ziel: make_polynomial_in 'a' sollte ergeben |
159 (*da sind wir fast am Ziel: make_polynomial_in 'a' sollte ergeben |
160 "x ^^^ 2 + (-1 * (b * x)) + (b + -1 * x) * a = 0"*) |
160 "x ^^^ 2 + (-1 * (b * x)) + (b + -1 * x) * a = 0"*) |
161 |
161 |
162 (*das rewriting l"asst sich beobachten mit |
162 (*das rewriting l"asst sich beobachten mit |
163 trace_rewrite := false; |
163 Trace.trace_rewrite := false; |
164 *) |
164 *) |
165 |
165 |
166 "------15.11.02 --------------------------"; |
166 "------15.11.02 --------------------------"; |
167 val t = (Thm.term_of o the o (parse thy)) "1 + a * x + b * x"; |
167 val t = (Thm.term_of o the o (parse thy)) "1 + a * x + b * x"; |
168 val bdv = (Thm.term_of o the o (parse thy)) "bdv"; |
168 val bdv = (Thm.term_of o the o (parse thy)) "bdv"; |
169 val a = (Thm.term_of o the o (parse thy)) "a"; |
169 val a = (Thm.term_of o the o (parse thy)) "a"; |
170 |
170 |
171 trace_rewrite := false; |
171 Trace.trace_rewrite := false; |
172 (* Anwenden einer Regelmenge aus Termorder.ML: *) |
172 (* Anwenden einer Regelmenge aus Termorder.ML: *) |
173 val SOME (t,_) = |
173 val SOME (t,_) = |
174 rewrite_set_inst_ thy false [(bdv,a)] make_polynomial_in t; |
174 rewrite_set_inst_ thy false [(bdv,a)] make_polynomial_in t; |
175 UnparseC.term t; |
175 UnparseC.term t; |
176 val SOME (t,_) = |
176 val SOME (t,_) = |