33 "----------- fun eval_ist_monom ----------------------------------"; |
33 "----------- fun eval_ist_monom ----------------------------------"; |
34 "----------- fun eval_ist_monom ----------------------------------"; |
34 "----------- fun eval_ist_monom ----------------------------------"; |
35 "----------- fun eval_ist_monom ----------------------------------"; |
35 "----------- fun eval_ist_monom ----------------------------------"; |
36 ist_monom (str2term "12"); |
36 ist_monom (str2term "12"); |
37 case eval_ist_monom 0 0 (str2term "12 ist_monom") 0 of |
37 case eval_ist_monom 0 0 (str2term "12 ist_monom") 0 of |
38 Some ("12 ist_monom = True", _) => () |
38 SOME ("12 ist_monom = True", _) => () |
39 | _ => raise error "polyminus.sml: 12 ist_monom = True"; |
39 | _ => raise error "polyminus.sml: 12 ist_monom = True"; |
40 |
40 |
41 case eval_ist_monom 0 0 (str2term "a ist_monom") 0 of |
41 case eval_ist_monom 0 0 (str2term "a ist_monom") 0 of |
42 Some ("a ist_monom = True", _) => () |
42 SOME ("a ist_monom = True", _) => () |
43 | _ => raise error "polyminus.sml: a ist_monom = True"; |
43 | _ => raise error "polyminus.sml: a ist_monom = True"; |
44 |
44 |
45 case eval_ist_monom 0 0 (str2term "(3*a) ist_monom") 0 of |
45 case eval_ist_monom 0 0 (str2term "(3*a) ist_monom") 0 of |
46 Some ("3 * a ist_monom = True", _) => () |
46 SOME ("3 * a ist_monom = True", _) => () |
47 | _ => raise error "polyminus.sml: 3 * a ist_monom = True"; |
47 | _ => raise error "polyminus.sml: 3 * a ist_monom = True"; |
48 |
48 |
49 case eval_ist_monom 0 0 (str2term "(a^^^2) ist_monom") 0 of |
49 case eval_ist_monom 0 0 (str2term "(a^^^2) ist_monom") 0 of |
50 Some ("a ^^^ 2 ist_monom = True", _) => () |
50 SOME ("a ^^^ 2 ist_monom = True", _) => () |
51 | _ => raise error "polyminus.sml: a^^^2 ist_monom = True"; |
51 | _ => raise error "polyminus.sml: a^^^2 ist_monom = True"; |
52 |
52 |
53 case eval_ist_monom 0 0 (str2term "(3*a^^^2) ist_monom") 0 of |
53 case eval_ist_monom 0 0 (str2term "(3*a^^^2) ist_monom") 0 of |
54 Some ("3 * a ^^^ 2 ist_monom = True", _) => () |
54 SOME ("3 * a ^^^ 2 ist_monom = True", _) => () |
55 | _ => raise error "polyminus.sml: 3*a^^^2 ist_monom = True"; |
55 | _ => raise error "polyminus.sml: 3*a^^^2 ist_monom = True"; |
56 |
56 |
57 case eval_ist_monom 0 0 (str2term "(a*b) ist_monom") 0 of |
57 case eval_ist_monom 0 0 (str2term "(a*b) ist_monom") 0 of |
58 Some ("a * b ist_monom = True", _) => () |
58 SOME ("a * b ist_monom = True", _) => () |
59 | _ => raise error "polyminus.sml: a*b ist_monom = True"; |
59 | _ => raise error "polyminus.sml: a*b ist_monom = True"; |
60 |
60 |
61 case eval_ist_monom 0 0 (str2term "(3*a*b) ist_monom") 0 of |
61 case eval_ist_monom 0 0 (str2term "(3*a*b) ist_monom") 0 of |
62 Some ("3 * a * b ist_monom = True", _) => () |
62 SOME ("3 * a * b ist_monom = True", _) => () |
63 | _ => raise error "polyminus.sml: 3*a*b ist_monom = True"; |
63 | _ => raise error "polyminus.sml: 3*a*b ist_monom = True"; |
64 |
64 |
65 |
65 |
66 "----------- watch order_add_mult -------------------------------"; |
66 "----------- watch order_add_mult -------------------------------"; |
67 "----------- watch order_add_mult -------------------------------"; |
67 "----------- watch order_add_mult -------------------------------"; |
68 "----------- watch order_add_mult -------------------------------"; |
68 "----------- watch order_add_mult -------------------------------"; |
69 "----- with these simple variables it works..."; |
69 "----- with these simple variables it works..."; |
70 trace_rewrite:=true; |
70 trace_rewrite:=true; |
71 trace_rewrite:=false; |
71 trace_rewrite:=false; |
72 val t = str2term "((a + d) + c) + b"; |
72 val t = str2term "((a + d) + c) + b"; |
73 val Some (t,_) = rewrite_set_ thy false order_add_mult t; term2str t; |
73 val SOME (t,_) = rewrite_set_ thy false order_add_mult t; term2str t; |
74 if term2str t = "a + (b + (c + d))" then () |
74 if term2str t = "a + (b + (c + d))" then () |
75 else raise error "polyminus.sml 1 watch order_add_mult"; |
75 else raise error "polyminus.sml 1 watch order_add_mult"; |
76 trace_rewrite:=false; |
76 trace_rewrite:=false; |
77 |
77 |
78 "----- the same stepwise..."; |
78 "----- the same stepwise..."; |
79 val od = ord_make_polynomial true Poly.thy; |
79 val od = ord_make_polynomial true Poly.thy; |
80 val t = str2term "((a + d) + c) + b"; |
80 val t = str2term "((a + d) + c) + b"; |
81 "((a + d) + c) + b"; |
81 "((a + d) + c) + b"; |
82 val Some (t,_) = rewrite_ thy od e_rls true real_add_commute t; term2str t; |
82 val SOME (t,_) = rewrite_ thy od e_rls true real_add_commute t; term2str t; |
83 "b + ((a + d) + c)"; |
83 "b + ((a + d) + c)"; |
84 val Some (t,_) = rewrite_ thy od e_rls true real_add_commute t; term2str t; |
84 val SOME (t,_) = rewrite_ thy od e_rls true real_add_commute t; term2str t; |
85 "b + (c + (a + d))"; |
85 "b + (c + (a + d))"; |
86 val Some (t,_) = rewrite_ thy od e_rls true real_add_left_commute t;term2str t; |
86 val SOME (t,_) = rewrite_ thy od e_rls true real_add_left_commute t;term2str t; |
87 "b + (a + (c + d))"; |
87 "b + (a + (c + d))"; |
88 val Some (t,_) = rewrite_ thy od e_rls true real_add_left_commute t;term2str t; |
88 val SOME (t,_) = rewrite_ thy od e_rls true real_add_left_commute t;term2str t; |
89 "a + (b + (c + d))"; |
89 "a + (b + (c + d))"; |
90 if term2str t = "a + (b + (c + d))" then () |
90 if term2str t = "a + (b + (c + d))" then () |
91 else raise error "polyminus.sml 2 watch order_add_mult"; |
91 else raise error "polyminus.sml 2 watch order_add_mult"; |
92 |
92 |
93 "----- if parentheses are right, left_commute is (almost) sufficient..."; |
93 "----- if parentheses are right, left_commute is (almost) sufficient..."; |
94 val t = str2term "a + (d + (c + b))"; |
94 val t = str2term "a + (d + (c + b))"; |
95 "a + (d + (c + b))"; |
95 "a + (d + (c + b))"; |
96 val Some (t,_) = rewrite_ thy od e_rls true real_add_left_commute t;term2str t; |
96 val SOME (t,_) = rewrite_ thy od e_rls true real_add_left_commute t;term2str t; |
97 "a + (c + (d + b))"; |
97 "a + (c + (d + b))"; |
98 val Some (t,_) = rewrite_ thy od e_rls true real_add_commute t;term2str t; |
98 val SOME (t,_) = rewrite_ thy od e_rls true real_add_commute t;term2str t; |
99 "a + (c + (b + d))"; |
99 "a + (c + (b + d))"; |
100 val Some (t,_) = rewrite_ thy od e_rls true real_add_left_commute t;term2str t; |
100 val SOME (t,_) = rewrite_ thy od e_rls true real_add_left_commute t;term2str t; |
101 "a + (b + (c + d))"; |
101 "a + (b + (c + d))"; |
102 |
102 |
103 "----- but we do not want the parentheses at right; thus: cond.rew."; |
103 "----- but we do not want the parentheses at right; thus: cond.rew."; |
104 "WN0712707 complicated monomials do not yet work ..."; |
104 "WN0712707 complicated monomials do not yet work ..."; |
105 val t = str2term "((5*a + 4*d) + 3*c) + 2*b"; |
105 val t = str2term "((5*a + 4*d) + 3*c) + 2*b"; |
106 val Some (t,_) = rewrite_set_ thy false order_add_mult t; term2str t; |
106 val SOME (t,_) = rewrite_set_ thy false order_add_mult t; term2str t; |
107 if term2str t = "2 * b + (3 * c + (4 * d + 5 * a))" then () |
107 if term2str t = "2 * b + (3 * c + (4 * d + 5 * a))" then () |
108 else raise error "polyminus.sml: order_add_mult changed"; |
108 else raise error "polyminus.sml: order_add_mult changed"; |
109 |
109 |
110 "----- here we see rew_sub going into subterm with ord.rew...."; |
110 "----- here we see rew_sub going into subterm with ord.rew...."; |
111 val od = ord_make_polynomial false Poly.thy; |
111 val od = ord_make_polynomial false Poly.thy; |
112 val t = str2term "b + a + c + d"; |
112 val t = str2term "b + a + c + d"; |
113 val Some (t,_) = rewrite_ thy od e_rls false real_add_commute t; term2str t; |
113 val SOME (t,_) = rewrite_ thy od e_rls false real_add_commute t; term2str t; |
114 val Some (t,_) = rewrite_ thy od e_rls false real_add_commute t; term2str t; |
114 val SOME (t,_) = rewrite_ thy od e_rls false real_add_commute t; term2str t; |
115 (*@@@ rew_sub gosub: t = d + (b + a + c) |
115 (*@@@ rew_sub gosub: t = d + (b + a + c) |
116 @@@ rew_sub begin: t = b + a + c*) |
116 @@@ rew_sub begin: t = b + a + c*) |
117 |
117 |
118 |
118 |
119 "----------- build predicate for +- ordering ---------------------"; |
119 "----------- build predicate for +- ordering ---------------------"; |
127 " a kleiner b ==> (b + a) = (a + b)"; |
127 " a kleiner b ==> (b + a) = (a + b)"; |
128 str2term "aaa"; |
128 str2term "aaa"; |
129 str2term "222 * aaa"; |
129 str2term "222 * aaa"; |
130 (* |
130 (* |
131 case eval_kleiner 0 0 (str2term "123 kleiner 32") 0 of |
131 case eval_kleiner 0 0 (str2term "123 kleiner 32") 0 of |
132 Some ("12 kleiner 9 = False", _) => () |
132 SOME ("12 kleiner 9 = False", _) => () |
133 | _ => raise error "polyminus.sml: 12 kleiner 9 = False"; |
133 | _ => raise error "polyminus.sml: 12 kleiner 9 = False"; |
134 *) |
134 *) |
135 case eval_kleiner 0 0 (str2term "a kleiner b") 0 of |
135 case eval_kleiner 0 0 (str2term "a kleiner b") 0 of |
136 Some ("a kleiner b = True", _) => () |
136 SOME ("a kleiner b = True", _) => () |
137 | _ => raise error "polyminus.sml: a kleiner b = True"; |
137 | _ => raise error "polyminus.sml: a kleiner b = True"; |
138 |
138 |
139 case eval_kleiner 0 0 (str2term "(10*g) kleiner f") 0 of |
139 case eval_kleiner 0 0 (str2term "(10*g) kleiner f") 0 of |
140 Some ("10 * g kleiner f = False", _) => () |
140 SOME ("10 * g kleiner f = False", _) => () |
141 | _ => raise error "polyminus.sml: 10 * g kleiner f = False"; |
141 | _ => raise error "polyminus.sml: 10 * g kleiner f = False"; |
142 |
142 |
143 case eval_kleiner 0 0 (str2term "(a^^^2) kleiner b") 0 of |
143 case eval_kleiner 0 0 (str2term "(a^^^2) kleiner b") 0 of |
144 Some ("a ^^^ 2 kleiner b = True", _) => () |
144 SOME ("a ^^^ 2 kleiner b = True", _) => () |
145 | _ => raise error "polyminus.sml: a ^^^ 2 kleiner b = True"; |
145 | _ => raise error "polyminus.sml: a ^^^ 2 kleiner b = True"; |
146 |
146 |
147 case eval_kleiner 0 0 (str2term "(3*a^^^2) kleiner b") 0 of |
147 case eval_kleiner 0 0 (str2term "(3*a^^^2) kleiner b") 0 of |
148 Some ("3 * a ^^^ 2 kleiner b = True", _) => () |
148 SOME ("3 * a ^^^ 2 kleiner b = True", _) => () |
149 | _ => raise error "polyminus.sml: 3 * a ^^^ 2 kleiner b = True"; |
149 | _ => raise error "polyminus.sml: 3 * a ^^^ 2 kleiner b = True"; |
150 |
150 |
151 case eval_kleiner 0 0 (str2term "(a*b) kleiner c") 0 of |
151 case eval_kleiner 0 0 (str2term "(a*b) kleiner c") 0 of |
152 Some ("a * b kleiner c = True", _) => () |
152 SOME ("a * b kleiner c = True", _) => () |
153 | _ => raise error "polyminus.sml: a * b kleiner b = True"; |
153 | _ => raise error "polyminus.sml: a * b kleiner b = True"; |
154 |
154 |
155 case eval_kleiner 0 0 (str2term "(3*a*b) kleiner c") 0 of |
155 case eval_kleiner 0 0 (str2term "(3*a*b) kleiner c") 0 of |
156 Some ("3 * a * b kleiner c = True", _) => () |
156 SOME ("3 * a * b kleiner c = True", _) => () |
157 | _ => raise error "polyminus.sml: 3 * a * b kleiner b = True"; |
157 | _ => raise error "polyminus.sml: 3 * a * b kleiner b = True"; |
158 |
158 |
159 |
159 |
160 |
160 |
161 "----- compare tausche_plus with real_num_collect"; |
161 "----- compare tausche_plus with real_num_collect"; |
162 val od = dummy_ord; |
162 val od = dummy_ord; |
163 |
163 |
164 val erls = erls_ordne_alphabetisch; |
164 val erls = erls_ordne_alphabetisch; |
165 val t = str2term "b + a"; |
165 val t = str2term "b + a"; |
166 val Some (t,_) = rewrite_ thy od erls false tausche_plus t; term2str t; |
166 val SOME (t,_) = rewrite_ thy od erls false tausche_plus t; term2str t; |
167 if term2str t = "a + b" then () |
167 if term2str t = "a + b" then () |
168 else raise error "polyminus.sml: ordne_alphabetisch1 b + a"; |
168 else raise error "polyminus.sml: ordne_alphabetisch1 b + a"; |
169 |
169 |
170 val erls = Atools_erls; |
170 val erls = Atools_erls; |
171 val t = str2term "2*a + 3*a"; |
171 val t = str2term "2*a + 3*a"; |
172 val Some (t,_) = rewrite_ thy od erls false real_num_collect t; term2str t; |
172 val SOME (t,_) = rewrite_ thy od erls false real_num_collect t; term2str t; |
173 |
173 |
174 "----- test rewrite_, rewrite_set_"; |
174 "----- test rewrite_, rewrite_set_"; |
175 trace_rewrite:=true; |
175 trace_rewrite:=true; |
176 val erls = erls_ordne_alphabetisch; |
176 val erls = erls_ordne_alphabetisch; |
177 val t = str2term "b + a"; |
177 val t = str2term "b + a"; |
178 val Some (t,_) = rewrite_set_ thy false ordne_alphabetisch t; term2str t; |
178 val SOME (t,_) = rewrite_set_ thy false ordne_alphabetisch t; term2str t; |
179 if term2str t = "a + b" then () |
179 if term2str t = "a + b" then () |
180 else raise error "polyminus.sml: ordne_alphabetisch a + b"; |
180 else raise error "polyminus.sml: ordne_alphabetisch a + b"; |
181 |
181 |
182 val t = str2term "2*b + a"; |
182 val t = str2term "2*b + a"; |
183 val Some (t,_) = rewrite_set_ thy false ordne_alphabetisch t; term2str t; |
183 val SOME (t,_) = rewrite_set_ thy false ordne_alphabetisch t; term2str t; |
184 if term2str t = "a + 2 * b" then () |
184 if term2str t = "a + 2 * b" then () |
185 else raise error "polyminus.sml: ordne_alphabetisch a + 2 * b"; |
185 else raise error "polyminus.sml: ordne_alphabetisch a + 2 * b"; |
186 |
186 |
187 val t = str2term "a + c + b"; |
187 val t = str2term "a + c + b"; |
188 val Some (t,_) = rewrite_set_ thy false ordne_alphabetisch t; term2str t; |
188 val SOME (t,_) = rewrite_set_ thy false ordne_alphabetisch t; term2str t; |
189 if term2str t = "a + b + c" then () |
189 if term2str t = "a + b + c" then () |
190 else raise error "polyminus.sml: ordne_alphabetisch a + b + c"; |
190 else raise error "polyminus.sml: ordne_alphabetisch a + b + c"; |
191 |
191 |
192 "----- rewrite goes into subterms"; |
192 "----- rewrite goes into subterms"; |
193 val t = str2term "a + c + b + d"; |
193 val t = str2term "a + c + b + d"; |
194 val Some (t,_) = rewrite_ thy od erls false tausche_plus_plus t; term2str t; |
194 val SOME (t,_) = rewrite_ thy od erls false tausche_plus_plus t; term2str t; |
195 if term2str t = "a + b + c + d" then () |
195 if term2str t = "a + b + c + d" then () |
196 else raise error "polyminus.sml: ordne_alphabetisch1 a + b + c + d"; |
196 else raise error "polyminus.sml: ordne_alphabetisch1 a + b + c + d"; |
197 |
197 |
198 val t = str2term "a + c + d + b"; |
198 val t = str2term "a + c + d + b"; |
199 val Some (t,_) = rewrite_set_ thy false ordne_alphabetisch t; term2str t; |
199 val SOME (t,_) = rewrite_set_ thy false ordne_alphabetisch t; term2str t; |
200 if term2str t = "a + b + c + d" then () |
200 if term2str t = "a + b + c + d" then () |
201 else raise error "polyminus.sml: ordne_alphabetisch2 a + b + c + d"; |
201 else raise error "polyminus.sml: ordne_alphabetisch2 a + b + c + d"; |
202 |
202 |
203 "----- here we see rew_sub going into subterm with cond.rew...."; |
203 "----- here we see rew_sub going into subterm with cond.rew...."; |
204 val t = str2term "b + a + c + d"; |
204 val t = str2term "b + a + c + d"; |
205 val Some (t,_) = rewrite_ thy od erls false tausche_plus t; term2str t; |
205 val SOME (t,_) = rewrite_ thy od erls false tausche_plus t; term2str t; |
206 if term2str t = "a + b + c + d" then () |
206 if term2str t = "a + b + c + d" then () |
207 else raise error "polyminus.sml: ordne_alphabetisch3 a + b + c + d"; |
207 else raise error "polyminus.sml: ordne_alphabetisch3 a + b + c + d"; |
208 |
208 |
209 "----- compile rls for the most complicated terms"; |
209 "----- compile rls for the most complicated terms"; |
210 val t = str2term "5*e + 6*f - 8*g - 9 - 7*e - 4*f + 10*g + 12"; |
210 val t = str2term "5*e + 6*f - 8*g - 9 - 7*e - 4*f + 10*g + 12"; |
211 "5 * e + 6 * f - 8 * g - 9 - 7 * e - 4 * f + 10 * g + 12"; |
211 "5 * e + 6 * f - 8 * g - 9 - 7 * e - 4 * f + 10 * g + 12"; |
212 val Some (t,_) = rewrite_set_ thy false ordne_alphabetisch t; |
212 val SOME (t,_) = rewrite_set_ thy false ordne_alphabetisch t; |
213 if term2str t = "- 9 + 12 + 5 * e - 7 * e + 6 * f - 4 * f - 8 * g + 10 * g" |
213 if term2str t = "- 9 + 12 + 5 * e - 7 * e + 6 * f - 4 * f - 8 * g + 10 * g" |
214 then () else raise error "polyminus.sml: ordne_alphabetisch finished"; |
214 then () else raise error "polyminus.sml: ordne_alphabetisch finished"; |
215 |
215 |
216 |
216 |
217 "----------- build fasse_zusammen --------------------------------"; |
217 "----------- build fasse_zusammen --------------------------------"; |
218 "----------- build fasse_zusammen --------------------------------"; |
218 "----------- build fasse_zusammen --------------------------------"; |
219 "----------- build fasse_zusammen --------------------------------"; |
219 "----------- build fasse_zusammen --------------------------------"; |
220 val t = str2term "- 9 + 12 + 5 * e - 7 * e + 6 * f - 4 * f - 8 * g + 10 * g"; |
220 val t = str2term "- 9 + 12 + 5 * e - 7 * e + 6 * f - 4 * f - 8 * g + 10 * g"; |
221 val Some (t,_) = rewrite_set_ thy false fasse_zusammen t; |
221 val SOME (t,_) = rewrite_set_ thy false fasse_zusammen t; |
222 if term2str t = "3 + -2 * e + 2 * f + 2 * g" then () |
222 if term2str t = "3 + -2 * e + 2 * f + 2 * g" then () |
223 else raise error "polyminus.sml: fasse_zusammen finished"; |
223 else raise error "polyminus.sml: fasse_zusammen finished"; |
224 |
224 |
225 "----------- build verschoenere ----------------------------------"; |
225 "----------- build verschoenere ----------------------------------"; |
226 "----------- build verschoenere ----------------------------------"; |
226 "----------- build verschoenere ----------------------------------"; |
227 "----------- build verschoenere ----------------------------------"; |
227 "----------- build verschoenere ----------------------------------"; |
228 val t = str2term "3 + -2 * e + 2 * f + 2 * g"; |
228 val t = str2term "3 + -2 * e + 2 * f + 2 * g"; |
229 val Some (t,_) = rewrite_set_ thy false verschoenere t; |
229 val SOME (t,_) = rewrite_set_ thy false verschoenere t; |
230 if term2str t = "3 - 2 * e + 2 * f + 2 * g" then () |
230 if term2str t = "3 - 2 * e + 2 * f + 2 * g" then () |
231 else raise error "polyminus.sml: verschoenere 3 + -2 * e ..."; |
231 else raise error "polyminus.sml: verschoenere 3 + -2 * e ..."; |
232 |
232 |
233 trace_rewrite:=true; |
233 trace_rewrite:=true; |
234 trace_rewrite:=false; |
234 trace_rewrite:=false; |
474 "----------- pbl binom polynom vereinfachen p.39 -----------------"; |
474 "----------- pbl binom polynom vereinfachen p.39 -----------------"; |
475 "----------- pbl binom polynom vereinfachen p.39 -----------------"; |
475 "----------- pbl binom polynom vereinfachen p.39 -----------------"; |
476 "----------- pbl binom polynom vereinfachen p.39 -----------------"; |
476 "----------- pbl binom polynom vereinfachen p.39 -----------------"; |
477 val rls = klammern_ausmultiplizieren; |
477 val rls = klammern_ausmultiplizieren; |
478 val t = str2term "(3 * a + 2) * (4 * a - 1)"; |
478 val t = str2term "(3 * a + 2) * (4 * a - 1)"; |
479 val Some (t,_) = rewrite_set_ thy false rls t; term2str t; |
479 val SOME (t,_) = rewrite_set_ thy false rls t; term2str t; |
480 "3 * a * (4 * a) - 3 * a * 1 + (2 * (4 * a) - 2 * 1)"; |
480 "3 * a * (4 * a) - 3 * a * 1 + (2 * (4 * a) - 2 * 1)"; |
481 val rls = discard_parentheses; |
481 val rls = discard_parentheses; |
482 val Some (t,_) = rewrite_set_ thy false rls t; term2str t; |
482 val SOME (t,_) = rewrite_set_ thy false rls t; term2str t; |
483 "3 * a * 4 * a - 3 * a * 1 + (2 * 4 * a - 2 * 1)"; |
483 "3 * a * 4 * a - 3 * a * 1 + (2 * 4 * a - 2 * 1)"; |
484 val rls = ordne_monome; |
484 val rls = ordne_monome; |
485 val Some (t,_) = rewrite_set_ thy false rls t; term2str t; |
485 val SOME (t,_) = rewrite_set_ thy false rls t; term2str t; |
486 "3 * 4 * a * a - 1 * 3 * a + (2 * 4 * a - 1 * 2)"; |
486 "3 * 4 * a * a - 1 * 3 * a + (2 * 4 * a - 1 * 2)"; |
487 (* |
487 (* |
488 val t = str2term "3 * a * 4 * a"; |
488 val t = str2term "3 * a * 4 * a"; |
489 val rls = ordne_monome; |
489 val rls = ordne_monome; |
490 val Some (t,_) = rewrite_set_ thy false rls t; term2str t; |
490 val SOME (t,_) = rewrite_set_ thy false rls t; term2str t; |
491 *) |
491 *) |
492 val rls = klammern_aufloesen; |
492 val rls = klammern_aufloesen; |
493 val Some (t,_) = rewrite_set_ thy false rls t; term2str t; |
493 val SOME (t,_) = rewrite_set_ thy false rls t; term2str t; |
494 "3 * 4 * a * a - 1 * 3 * a + 2 * 4 * a - 1 * 2"; |
494 "3 * 4 * a * a - 1 * 3 * a + 2 * 4 * a - 1 * 2"; |
495 val rls = ordne_alphabetisch; |
495 val rls = ordne_alphabetisch; |
496 (*TODO: make is_monom more general, a*a=a^2, ...*) |
496 (*TODO: make is_monom more general, a*a=a^2, ...*) |
497 val Some (t,_) = rewrite_set_ thy false rls t; term2str t; |
497 val SOME (t,_) = rewrite_set_ thy false rls t; term2str t; |
498 "3 * 4 * a * a - 1 * 2 - 1 * 3 * a + 2 * 4 * a"; |
498 "3 * 4 * a * a - 1 * 2 - 1 * 3 * a + 2 * 4 * a"; |
499 (*GOON.WN080104 |
499 (*GOON.WN080104 |
500 val rls = fasse_zusammen; |
500 val rls = fasse_zusammen; |
501 val Some (t,_) = rewrite_set_ thy false rls t; term2str t; |
501 val SOME (t,_) = rewrite_set_ thy false rls t; term2str t; |
502 val rls = verschoenere; |
502 val rls = verschoenere; |
503 val Some (t,_) = rewrite_set_ thy false rls t; term2str t; |
503 val SOME (t,_) = rewrite_set_ thy false rls t; term2str t; |
504 *) |
504 *) |
505 |
505 |
506 |
506 |
507 trace_rewrite := true; |
507 trace_rewrite := true; |
508 trace_rewrite := false; |
508 trace_rewrite := false; |
568 Thm ("not_true",num_str not_true), |
568 Thm ("not_true",num_str not_true), |
569 (*"(~ True) = False"*) |
569 (*"(~ True) = False"*) |
570 Thm ("not_false",num_str not_false) |
570 Thm ("not_false",num_str not_false) |
571 (*"(~ False) = True"*)]; |
571 (*"(~ False) = True"*)]; |
572 trace_rewrite := true; |
572 trace_rewrite := true; |
573 val Some (t', _) = rewrite_set_ thy false prls t; |
573 val SOME (t', _) = rewrite_set_ thy false prls t; |
574 trace_rewrite := false; |
574 trace_rewrite := false; |
575 |
575 |
576 "--- does the respective prls rewrite the whole predicate ?"; |
576 "--- does the respective prls rewrite the whole predicate ?"; |
577 val t = str2term |
577 val t = str2term |
578 "Not (matchsub (?a * (?b + ?c)) (8 * (a - q) + a - 2 * q) | \ |
578 "Not (matchsub (?a * (?b + ?c)) (8 * (a - q) + a - 2 * q) | \ |
579 \ matchsub (?a * (?b - ?c)) (8 * (a - q) + a - 2 * q) | \ |
579 \ matchsub (?a * (?b - ?c)) (8 * (a - q) + a - 2 * q) | \ |
580 \ matchsub ((?b + ?c) * ?a) (8 * (a - q) + a - 2 * q) | \ |
580 \ matchsub ((?b + ?c) * ?a) (8 * (a - q) + a - 2 * q) | \ |
581 \ matchsub ((?b - ?c) * ?a) (8 * (a - q) + a - 2 * q) )"; |
581 \ matchsub ((?b - ?c) * ?a) (8 * (a - q) + a - 2 * q) )"; |
582 trace_rewrite := true; |
582 trace_rewrite := true; |
583 val Some (t', _) = rewrite_set_ thy false prls t; |
583 val SOME (t', _) = rewrite_set_ thy false prls t; |
584 trace_rewrite := false; |
584 trace_rewrite := false; |
585 if term2str t' = "False" then () |
585 if term2str t' = "False" then () |
586 else raise error "polyminus.sml Not (matchsub (?a * (?b + ?c)) (8 ..."; |
586 else raise error "polyminus.sml Not (matchsub (?a * (?b + ?c)) (8 ..."; |
587 |
587 |
588 |
588 |