4 (c) due to copyright terms |
4 (c) due to copyright terms |
5 |
5 |
6 use"../smltest/IsacKnowledge/polyminus.sml"; |
6 use"../smltest/IsacKnowledge/polyminus.sml"; |
7 use"polyminus.sml"; |
7 use"polyminus.sml"; |
8 *) |
8 *) |
9 (*========== inhibit exn ?====================================================== |
|
10 "--------------------------------------------------------"; |
9 "--------------------------------------------------------"; |
11 "--------------------------------------------------------"; |
10 "--------------------------------------------------------"; |
12 "table of contents --------------------------------------"; |
11 "table of contents --------------------------------------"; |
13 "--------------------------------------------------------"; |
12 "--------------------------------------------------------"; |
14 "----------- fun eval_ist_monom -------------------------"; |
13 "----------- fun eval_ist_monom -------------------------"; |
15 "----------- watch order_add_mult ----------------------"; |
14 "----------- watch order_add_mult ----------------------"; |
16 "----------- build predicate for +- ordering ------------"; |
15 "----------- build predicate for +- ordering ------------"; |
17 "----------- build fasse_zusammen -----------------------"; |
16 "----------- build fasse_zusammen -----------------------"; |
18 "----------- build verschoenere -------------------------"; |
17 "----------- build verschoenere -------------------------"; |
19 "----------- met simplification for_polynomials with_minu"; |
18 "----------- met simplification for_polynomials with_minu"; |
|
19 "----------- me simplification.for_polynomials.with_minus"; |
20 "----------- pbl polynom vereinfachen p.33 --------------"; |
20 "----------- pbl polynom vereinfachen p.33 --------------"; |
21 "----------- met probe fuer_polynom ---------------------"; |
21 "----------- met probe fuer_polynom ---------------------"; |
22 "----------- pbl polynom probe --------------------------"; |
22 "----------- pbl polynom probe --------------------------"; |
23 "----------- pbl klammer polynom vereinfachen p.34 ------"; |
23 "----------- pbl klammer polynom vereinfachen p.34 ------"; |
24 "----------- try fun applyTactics -----------------------"; |
24 "----------- try fun applyTactics -----------------------"; |
28 "----------- *** prep_pbt: syntax error in '#Where' of [v"; |
28 "----------- *** prep_pbt: syntax error in '#Where' of [v"; |
29 "--------------------------------------------------------"; |
29 "--------------------------------------------------------"; |
30 "--------------------------------------------------------"; |
30 "--------------------------------------------------------"; |
31 "--------------------------------------------------------"; |
31 "--------------------------------------------------------"; |
32 |
32 |
33 val thy = PolyMinus.thy; |
33 val thy = theory "PolyMinus"; |
34 |
34 |
35 "----------- fun eval_ist_monom ----------------------------------"; |
35 "----------- fun eval_ist_monom ----------------------------------"; |
36 "----------- fun eval_ist_monom ----------------------------------"; |
36 "----------- fun eval_ist_monom ----------------------------------"; |
37 "----------- fun eval_ist_monom ----------------------------------"; |
37 "----------- fun eval_ist_monom ----------------------------------"; |
38 ist_monom (str2term "12"); |
38 ist_monom (str2term "12"); |
|
39 (*========== inhibit exn ======================================================= |
39 case eval_ist_monom 0 0 (str2term "12 ist_monom") 0 of |
40 case eval_ist_monom 0 0 (str2term "12 ist_monom") 0 of |
40 SOME ("12 ist_monom = True", _) => () |
41 SOME ("12 ist_monom = True", _) => () |
41 | _ => error "polyminus.sml: 12 ist_monom = True"; |
42 | _ => error "polyminus.sml: 12 ist_monom = True"; |
42 |
43 |
43 case eval_ist_monom 0 0 (str2term "a ist_monom") 0 of |
44 case eval_ist_monom 0 0 (str2term "a ist_monom") 0 of |
62 |
63 |
63 case eval_ist_monom 0 0 (str2term "(3*a*b) ist_monom") 0 of |
64 case eval_ist_monom 0 0 (str2term "(3*a*b) ist_monom") 0 of |
64 SOME ("3 * a * b ist_monom = True", _) => () |
65 SOME ("3 * a * b ist_monom = True", _) => () |
65 | _ => error "polyminus.sml: 3*a*b ist_monom = True"; |
66 | _ => error "polyminus.sml: 3*a*b ist_monom = True"; |
66 |
67 |
|
68 ============ inhibit exn =====================================================*) |
67 |
69 |
68 "----------- watch order_add_mult -------------------------------"; |
70 "----------- watch order_add_mult -------------------------------"; |
69 "----------- watch order_add_mult -------------------------------"; |
71 "----------- watch order_add_mult -------------------------------"; |
70 "----------- watch order_add_mult -------------------------------"; |
72 "----------- watch order_add_mult -------------------------------"; |
71 "----- with these simple variables it works..."; |
73 "----- with these simple variables it works..."; |
76 if term2str t = "a + (b + (c + d))" then () |
78 if term2str t = "a + (b + (c + d))" then () |
77 else error "polyminus.sml 1 watch order_add_mult"; |
79 else error "polyminus.sml 1 watch order_add_mult"; |
78 trace_rewrite:=false; |
80 trace_rewrite:=false; |
79 |
81 |
80 "----- the same stepwise..."; |
82 "----- the same stepwise..."; |
81 val od = ord_make_polynomial true Poly.thy; |
83 val od = ord_make_polynomial true (theory "Poly"); |
82 val t = str2term "((a + d) + c) + b"; |
84 val t = str2term "((a + d) + c) + b"; |
83 "((a + d) + c) + b"; |
85 "((a + d) + c) + b"; |
84 val SOME (t,_) = rewrite_ thy od e_rls true add_commute t; term2str t; |
86 val SOME (t,_) = rewrite_ thy od e_rls true @{thm add_commute} t; term2str t; |
85 "b + ((a + d) + c)"; |
87 "b + ((a + d) + c)"; |
86 val SOME (t,_) = rewrite_ thy od e_rls true add_commute t; term2str t; |
88 val SOME (t,_) = rewrite_ thy od e_rls true @{thm add_commute} t; term2str t; |
87 "b + (c + (a + d))"; |
89 "b + (c + (a + d))"; |
88 val SOME (t,_) = rewrite_ thy od e_rls true add_left_commute t;term2str t; |
90 val SOME (t,_) = rewrite_ thy od e_rls true @{thm add_left_commute} t;term2str t; |
89 "b + (a + (c + d))"; |
91 "b + (a + (c + d))"; |
90 val SOME (t,_) = rewrite_ thy od e_rls true add_left_commute t;term2str t; |
92 val SOME (t,_) = rewrite_ thy od e_rls true @{thm add_left_commute} t;term2str t; |
91 "a + (b + (c + d))"; |
93 "a + (b + (c + d))"; |
92 if term2str t = "a + (b + (c + d))" then () |
94 if term2str t = "a + (b + (c + d))" then () |
93 else error "polyminus.sml 2 watch order_add_mult"; |
95 else error "polyminus.sml 2 watch order_add_mult"; |
94 |
96 |
95 "----- if parentheses are right, left_commute is (almost) sufficient..."; |
97 "----- if parentheses are right, left_commute is (almost) sufficient..."; |
96 val t = str2term "a + (d + (c + b))"; |
98 val t = str2term "a + (d + (c + b))"; |
97 "a + (d + (c + b))"; |
99 "a + (d + (c + b))"; |
98 val SOME (t,_) = rewrite_ thy od e_rls true add_left_commute t;term2str t; |
100 val SOME (t,_) = rewrite_ thy od e_rls true @{thm add_left_commute} t;term2str t; |
99 "a + (c + (d + b))"; |
101 "a + (c + (d + b))"; |
100 val SOME (t,_) = rewrite_ thy od e_rls true add_commute t;term2str t; |
102 val SOME (t,_) = rewrite_ thy od e_rls true @{thm add_commute} t;term2str t; |
101 "a + (c + (b + d))"; |
103 "a + (c + (b + d))"; |
102 val SOME (t,_) = rewrite_ thy od e_rls true add_left_commute t;term2str t; |
104 val SOME (t,_) = rewrite_ thy od e_rls true @{thm add_left_commute} t;term2str t; |
103 "a + (b + (c + d))"; |
105 "a + (b + (c + d))"; |
104 |
106 |
105 "----- but we do not want the parentheses at right; thus: cond.rew."; |
107 "----- but we do not want the parentheses at right; thus: cond.rew."; |
106 "WN0712707 complicated monomials do not yet work ..."; |
108 "WN0712707 complicated monomials do not yet work ..."; |
107 val t = str2term "((5*a + 4*d) + 3*c) + 2*b"; |
109 val t = str2term "((5*a + 4*d) + 3*c) + 2*b"; |
108 val SOME (t,_) = rewrite_set_ thy false order_add_mult t; term2str t; |
110 val SOME (t,_) = rewrite_set_ thy false order_add_mult t; term2str t; |
109 if term2str t = "2 * b + (3 * c + (4 * d + 5 * a))" then () |
111 if term2str t = "2 * b + (3 * c + (4 * d + 5 * a))" then () |
110 else error "polyminus.sml: order_add_mult changed"; |
112 else error "polyminus.sml: order_add_mult changed"; |
111 |
113 |
112 "----- here we see rew_sub going into subterm with ord.rew...."; |
114 "----- here we see rew_sub going into subterm with ord.rew...."; |
113 val od = ord_make_polynomial false Poly.thy; |
115 val od = ord_make_polynomial false (theory "Poly"); |
114 val t = str2term "b + a + c + d"; |
116 val t = str2term "b + a + c + d"; |
115 val SOME (t,_) = rewrite_ thy od e_rls false add_commute t; term2str t; |
117 val SOME (t,_) = rewrite_ thy od e_rls false @{thm add_commute} t; term2str t; |
116 val SOME (t,_) = rewrite_ thy od e_rls false add_commute t; term2str t; |
118 val SOME (t,_) = rewrite_ thy od e_rls false @{thm add_commute} t; term2str t; |
117 (*@@@ rew_sub gosub: t = d + (b + a + c) |
119 (*@@@ rew_sub gosub: t = d + (b + a + c) |
118 @@@ rew_sub begin: t = b + a + c*) |
120 @@@ rew_sub begin: t = b + a + c*) |
119 |
121 |
120 |
122 |
121 "----------- build predicate for +- ordering ---------------------"; |
123 "----------- build predicate for +- ordering ---------------------"; |
132 (* |
134 (* |
133 case eval_kleiner 0 0 (str2term "123 kleiner 32") 0 of |
135 case eval_kleiner 0 0 (str2term "123 kleiner 32") 0 of |
134 SOME ("12 kleiner 9 = False", _) => () |
136 SOME ("12 kleiner 9 = False", _) => () |
135 | _ => error "polyminus.sml: 12 kleiner 9 = False"; |
137 | _ => error "polyminus.sml: 12 kleiner 9 = False"; |
136 *) |
138 *) |
|
139 (*========== inhibit exn ======================================================= |
137 case eval_kleiner 0 0 (str2term "a kleiner b") 0 of |
140 case eval_kleiner 0 0 (str2term "a kleiner b") 0 of |
138 SOME ("a kleiner b = True", _) => () |
141 SOME ("a kleiner b = True", _) => () |
139 | _ => error "polyminus.sml: a kleiner b = True"; |
142 | _ => error "polyminus.sml: a kleiner b = True"; |
140 |
143 |
141 case eval_kleiner 0 0 (str2term "(10*g) kleiner f") 0 of |
144 case eval_kleiner 0 0 (str2term "(10*g) kleiner f") 0 of |
156 |
159 |
157 case eval_kleiner 0 0 (str2term "(3*a*b) kleiner c") 0 of |
160 case eval_kleiner 0 0 (str2term "(3*a*b) kleiner c") 0 of |
158 SOME ("3 * a * b kleiner c = True", _) => () |
161 SOME ("3 * a * b kleiner c = True", _) => () |
159 | _ => error "polyminus.sml: 3 * a * b kleiner b = True"; |
162 | _ => error "polyminus.sml: 3 * a * b kleiner b = True"; |
160 |
163 |
|
164 ============ inhibit exn =====================================================*) |
161 |
165 |
162 |
166 |
163 "----- compare tausche_plus with real_num_collect"; |
167 "----- compare tausche_plus with real_num_collect"; |
164 val od = dummy_ord; |
168 val od = dummy_ord; |
165 |
169 |
166 val erls = erls_ordne_alphabetisch; |
170 val erls = erls_ordne_alphabetisch; |
167 val t = str2term "b + a"; |
171 val t = str2term "b + a"; |
168 val SOME (t,_) = rewrite_ thy od erls false tausche_plus t; term2str t; |
172 val SOME (t,_) = rewrite_ thy od erls false @{thm tausche_plus} t; term2str t; |
169 if term2str t = "a + b" then () |
173 if term2str t = "a + b" then () |
170 else error "polyminus.sml: ordne_alphabetisch1 b + a"; |
174 else error "polyminus.sml: ordne_alphabetisch1 b + a"; |
171 |
175 |
172 val erls = Atools_erls; |
176 val erls = Atools_erls; |
173 val t = str2term "2*a + 3*a"; |
177 val t = str2term "2*a + 3*a"; |
174 val SOME (t,_) = rewrite_ thy od erls false real_num_collect t; term2str t; |
178 val SOME (t,_) = rewrite_ thy od erls false @{thm real_num_collect} t; term2str t; |
175 |
179 |
176 "----- test rewrite_, rewrite_set_"; |
180 "----- test rewrite_, rewrite_set_"; |
177 trace_rewrite:=true; |
181 trace_rewrite:=true; |
178 val erls = erls_ordne_alphabetisch; |
182 val erls = erls_ordne_alphabetisch; |
179 val t = str2term "b + a"; |
183 val t = str2term "b + a"; |
191 if term2str t = "a + b + c" then () |
195 if term2str t = "a + b + c" then () |
192 else error "polyminus.sml: ordne_alphabetisch a + b + c"; |
196 else error "polyminus.sml: ordne_alphabetisch a + b + c"; |
193 |
197 |
194 "----- rewrite goes into subterms"; |
198 "----- rewrite goes into subterms"; |
195 val t = str2term "a + c + b + d"; |
199 val t = str2term "a + c + b + d"; |
196 val SOME (t,_) = rewrite_ thy od erls false tausche_plus_plus t; term2str t; |
200 val SOME (t,_) = rewrite_ thy od erls false @{thm tausche_plus_plus} t; term2str t; |
197 if term2str t = "a + b + c + d" then () |
201 if term2str t = "a + b + c + d" then () |
198 else error "polyminus.sml: ordne_alphabetisch1 a + b + c + d"; |
202 else error "polyminus.sml: ordne_alphabetisch1 a + b + c + d"; |
199 |
203 |
200 val t = str2term "a + c + d + b"; |
204 val t = str2term "a + c + d + b"; |
201 val SOME (t,_) = rewrite_set_ thy false ordne_alphabetisch t; term2str t; |
205 val SOME (t,_) = rewrite_set_ thy false ordne_alphabetisch t; term2str t; |
202 if term2str t = "a + b + c + d" then () |
206 if term2str t = "a + b + c + d" then () |
203 else error "polyminus.sml: ordne_alphabetisch2 a + b + c + d"; |
207 else error "polyminus.sml: ordne_alphabetisch2 a + b + c + d"; |
204 |
208 |
205 "----- here we see rew_sub going into subterm with cond.rew...."; |
209 "----- here we see rew_sub going into subterm with cond.rew...."; |
206 val t = str2term "b + a + c + d"; |
210 val t = str2term "b + a + c + d"; |
207 val SOME (t,_) = rewrite_ thy od erls false tausche_plus t; term2str t; |
211 val SOME (t,_) = rewrite_ thy od erls false @{thm tausche_plus} t; term2str t; |
208 if term2str t = "a + b + c + d" then () |
212 if term2str t = "a + b + c + d" then () |
209 else error "polyminus.sml: ordne_alphabetisch3 a + b + c + d"; |
213 else error "polyminus.sml: ordne_alphabetisch3 a + b + c + d"; |
210 |
214 |
211 "----- compile rls for the most complicated terms"; |
215 "----- compile rls for the most complicated terms"; |
212 val t = str2term "5*e + 6*f - 8*g - 9 - 7*e - 4*f + 10*g + 12"; |
216 val t = str2term "5*e + 6*f - 8*g - 9 - 7*e - 4*f + 10*g + 12"; |
237 |
241 |
238 "----------- met simplification for_polynomials with_minus -------"; |
242 "----------- met simplification for_polynomials with_minus -------"; |
239 "----------- met simplification for_polynomials with_minus -------"; |
243 "----------- met simplification for_polynomials with_minus -------"; |
240 "----------- met simplification for_polynomials with_minus -------"; |
244 "----------- met simplification for_polynomials with_minus -------"; |
241 val str = |
245 val str = |
242 "Script SimplifyScript (t_::real) = \ |
246 "Script SimplifyScript (t_t::real) = \ |
243 \ (((Try (Rewrite_Set ordne_alphabetisch False)) @@ \ |
247 \ (((Try (Rewrite_Set ordne_alphabetisch False)) @@ \ |
244 \ (Try (Rewrite_Set fasse_zusammen False)) @@ \ |
248 \ (Try (Rewrite_Set fasse_zusammen False)) @@ \ |
245 \ (Try (Rewrite_Set verschoenere False))) t_)" |
249 \ (Try (Rewrite_Set verschoenere False))) t_t)" |
246 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str; |
250 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str; |
247 atomty sc; |
251 atomty sc; |
248 |
252 |
249 |
253 "----------- me simplification.for_polynomials.with_minus"; |
|
254 "----------- me simplification.for_polynomials.with_minus"; |
|
255 "----------- me simplification.for_polynomials.with_minus"; |
|
256 val c = []; |
|
257 val (p,_,f,nxt,_,pt) = |
|
258 CalcTreeTEST |
|
259 [(["TERM (5*e + 6*f - 8*g - 9 - 7*e - 4*f + 10*g + 12)", |
|
260 "normalform N"], |
|
261 ("PolyMinus",["plus_minus","polynom","vereinfachen"], |
|
262 ["simplification","for_polynomials","with_minus"]))]; |
|
263 (*========== inhibit exn ======================================================= |
|
264 val (p,_,f,nxt,_,pt) = me nxt p c pt; |
|
265 ============ inhibit exn =====================================================*) |
|
266 |
|
267 (*========== inhibit exn ?====================================================== |
250 "----------- pbl polynom vereinfachen p.33 -----------------------"; |
268 "----------- pbl polynom vereinfachen p.33 -----------------------"; |
251 "----------- pbl polynom vereinfachen p.33 -----------------------"; |
269 "----------- pbl polynom vereinfachen p.33 -----------------------"; |
252 "----------- pbl polynom vereinfachen p.33 -----------------------"; |
270 "----------- pbl polynom vereinfachen p.33 -----------------------"; |
253 "----------- 140 c ---"; |
271 "----------- 140 c ---"; |
254 states:=[]; |
272 states:=[]; |
528 |
546 |
529 "----------- pbl binom polynom vereinfachen: cube ----------------"; |
547 "----------- pbl binom polynom vereinfachen: cube ----------------"; |
530 "----------- pbl binom polynom vereinfachen: cube ----------------"; |
548 "----------- pbl binom polynom vereinfachen: cube ----------------"; |
531 "----------- pbl binom polynom vereinfachen: cube ----------------"; |
549 "----------- pbl binom polynom vereinfachen: cube ----------------"; |
532 states:=[]; |
550 states:=[]; |
533 CalcTree [(["TERM (8*(a - q) + a - 2*q + 3*(a - 2*q))", |
551 CalcTree [(["TERM (8*(a - q) + a - 2*q + 3*(a - 2*q))", "normalform N"], |
534 "normalform N"], |
|
535 ("PolyMinus",["binom_klammer","polynom","vereinfachen"], |
552 ("PolyMinus",["binom_klammer","polynom","vereinfachen"], |
536 ["simplification","for_polynomials","with_parentheses_mult"]))]; |
553 ["simplification","for_polynomials","with_parentheses_mult"]))]; |
537 moveActiveRoot 1; |
554 moveActiveRoot 1; |
538 autoCalculate 1 CompleteCalc; |
555 autoCalculate 1 CompleteCalc; |
539 val ((pt,p),_) = get_calc 1; show_pt pt; |
556 val ((pt,p),_) = get_calc 1; show_pt pt; |