1 (* Title: tests for ProgLang/rewrite.sml
2 TODO.WN0509 collect typical tests from systest here !!!!!
3 Author: Walther Neuper 050908
4 (c) copyright due to lincense terms.
6 12345678901234567890123456789012345678901234567890123456789012345678901234567890
7 10 20 30 40 50 60 70 80
10 "--------------------------------------------------------";
11 "table of contents --------------------------------------";
12 "--------------------------------------------------------";
13 "----------- assemble rewrite ---------------------------";
14 "----------- test rewriting without Isac's thys ---------";
15 "----------- conditional rewriting without Isac's thys --";
16 "----------- step through 'and rew_sub': ----------------";
17 "----------- step through 'fun rewrite_terms_' ---------";
18 "----------- rewrite_inst_ bdvs -------------------------";
19 "----------- check diff 2002--2009-3 --------------------";
20 "----------- compare all prepat's existing 2010 ---------";
21 "----------- fun app_rev, Rrls, -------------------------";
22 "--------------------------------------------------------";
23 "--------------------------------------------------------";
24 "--------------------------------------------------------";
27 "----------- assemble rewrite ---------------------------";
28 "----------- assemble rewrite ---------------------------";
29 "----------- assemble rewrite ---------------------------";
30 "===== rewriting by thm with 'a";
31 (*show_types := true;*)
32 val thy = @{theory Complex_Main};
33 val ctxt = @{context};
34 val thm = @{thm add_commute};
35 val t = (term_of o the) (parse thy "((r + u) + t) + s");
36 "----- from old: fun rewrite__";
38 val r = (((inst_bdv bdv) o norm o #prop o rep_thm) thm);
39 "----- from old: and rew_sub";
40 (*========== inhibit exn =======================================================
41 val (lhs,rhs) = (dest_equals' o strip_trueprop
42 o Logic.strip_imp_concl) r;
44 val insts = Pattern.match thy (lhs,t) (Vartab.empty, Vartab.empty);*)
45 "----- fun match_rew in Pure/pattern.ML";
46 val rtm = the_default rhs (Term.rename_abs lhs t rhs);
48 writeln(Syntax.string_of_term ctxt rtm);
49 writeln(Syntax.string_of_term ctxt lhs);
50 writeln(Syntax.string_of_term ctxt t);
52 (Pattern.match thy (lhs, t) (Vartab.empty, Vartab.empty));
53 val (rew, rhs) = (Envir.subst_term
54 (Pattern.match thy (lhs, t) (Vartab.empty, Vartab.empty)) rtm, rtm);
55 (*lookup in isabelle?trace?response...*)
56 writeln(Syntax.string_of_term ctxt rew);
57 writeln(Syntax.string_of_term ctxt rhs);
59 "===== rewriting: prep insertion into rew_sub";
60 val thy = @{theory Complex_Main};
61 val ctxt = @{context};
62 val thm = @{thm nonzero_mult_divide_cancel_right};
63 val r = Thm.prop_of thm;
64 val tm = @{term "x*2 / 2::real"};
66 val (lhs, rhs) = (HOLogic.dest_eq o HOLogic.dest_Trueprop
67 o Logic.strip_imp_concl) r;
68 val r' = Envir.subst_term (Pattern.match thy (lhs, tm)
69 (Vartab.empty, Vartab.empty)) r;
70 val p' = (fst o Logic.strip_prems) (Logic.count_prems r', [], r');
71 val t' = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop
72 o Logic.strip_imp_concl) r';
74 (*is displayed on top of <response> buffer...*)
75 Pretty.writeln (ProofContext.pretty_term_abbrev @{context} r');
76 Pretty.writeln (ProofContext.pretty_term_abbrev @{context} t');
78 ============ inhibit exn =====================================================*)
80 "----------- test rewriting without Isac's thys ---------";
81 "----------- test rewriting without Isac's thys ---------";
82 "----------- test rewriting without Isac's thys ---------";
84 "===== rewriting with Isabelle2009-1 only, i.e without isac-hacks";
85 val thy = @{theory Complex_Main};
86 val ctxt = @{context};
87 val thm = @{thm add_commute};
88 val tm = @{term "x + y*z::real"};
89 (*-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.
91 val SOME (r,_) = (rewrite_ thy dummy_ord e_rls false thm tm)
92 handle _ => error "rewrite.sml diff.behav. in rewriting";
93 (*is displayed on _TOP_ of <response> buffer...*)
94 Pretty.writeln (ProofContext.pretty_term_abbrev @{context} r);
95 if r = @{term "y*z + x::real"}
96 then () else error "rewrite.sml diff.result in rewriting";
98 "----- rewriting a subterm";
99 val tm = @{term "w*(x + y*z)::real"};
101 val SOME (r,_) = (rewrite_ thy dummy_ord e_rls false thm tm)
102 handle _ => error "rewrite.sml diff.behav. in rew_sub";
104 "----- ordered rewriting";
105 fun tord (_:subst) pp = Term_Ord.termless pp;
106 if tord [] (@{term "x + y*z::real"}, @{term "y*z + x::real"}) then ()
107 else error "rewrite.sml diff.behav. in ord.rewr.";
109 val NONE = (rewrite_ thy tord e_rls false thm tm)
110 handle _ => error "rewrite.sml diff.behav. in rewriting";
111 (*is displayed on _TOP_ of <response> buffer...*)
112 Pretty.writeln (ProofContext.pretty_term_abbrev @{context} r);
114 val tm = @{term "x*y + z::real"};
115 val SOME (r,_) = (rewrite_ thy tord e_rls false thm tm)
116 handle _ => error "rewrite.sml diff.behav. in rewriting";
117 -.-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.*)
120 "----------- conditional rewriting without Isac's thys --";
121 "----------- conditional rewriting without Isac's thys --";
122 "----------- conditional rewriting without Isac's thys --";
124 "===== prepr cond.rew. with Pattern.match";
125 val thy = @{theory Complex_Main};
126 val ctxt = @{context};
127 val thm = @{thm nonzero_mult_divide_cancel_right};
128 val rule = Thm.prop_of thm;
129 val tm = @{term "x*2 / 2::real"};
131 val prem = Logic.strip_imp_prems rule;
132 val nps = Logic.count_prems rule;
133 val prems = Logic.strip_prems (nps, [], rule);
135 val eq = Logic.strip_imp_concl rule;
136 val (lhs, rhs) = (HOLogic.dest_eq o HOLogic.dest_Trueprop) eq;
138 val mtcs = Pattern.match thy (lhs, tm) (Vartab.empty, Vartab.empty);
139 val rule' = Envir.subst_term mtcs rule;
141 val prems' = (fst o Logic.strip_prems)
142 (Logic.count_prems rule', [], rule');
143 val rhs' = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop
144 o Logic.strip_imp_concl) rule';
146 "----- conditional rewriting creating an assumption";
147 "----- conditional rewriting creating an assumption";
148 val tm = @{term "x*y / y::real"};
149 val SOME (rew, asm) = (rewrite_ thy dummy_ord e_rls false thm tm)
150 handle _ => error "rewrite.sml diff.behav. in cond.rew.";
152 if rew = @{term "x::real"} then () (* the rewrite is _NO_ Trueprop *)
153 else error "rewrite.sml diff.result in cond.rew.";
155 if hd asm = @{term "~ y = (0::real)"} (* dropped Trueprop $ ...*)
156 then () else error "rewrite.sml diff.asm in cond.rew.";
157 "----- conditional rewriting immediately: can only be done with ";
158 "------Isabelle numerals, because erls cannot handle them yet.";
161 "----------- step through 'and rew_sub': ----------------";
162 "----------- step through 'and rew_sub': ----------------";
163 "----------- step through 'and rew_sub': ----------------";
164 (*and make asms without Trueprop, beginning with the result:*)
165 val tm = @{term "x*y / y::real"};
166 val (t', asm, _, _) = rew_sub thy 0 [] dummy_ord e_rls true [] (prop_of thm) tm;
167 (*show_types := false;*)
168 "----- evaluate arguments";
169 val (thy, i, bdv, tless, rls, put_asm, lrd, r, t) =
170 (thy, 0, [], dummy_ord, e_rls, true, [], (prop_of thm), tm);
171 "----- step 1: lhs, rhs of rule";
172 val (lhs, rhs) = (HOLogic.dest_eq o HOLogic.dest_Trueprop
173 o Logic.strip_imp_concl) r;
174 term2str r = "?b ~= (0::?'a) ==> ?a * ?b / ?b = ?a";
175 term2str lhs = "?a * ?b / ?b"; term2str rhs = "?a";
176 "----- step 2: the rule instantiated";
177 val r' = Envir.subst_term
178 (Pattern.match thy (lhs, t) (Vartab.empty, Vartab.empty)) r;
179 term2str r' = "y ~= 0 ==> x * y / y = x";
180 "----- step 3: get the (instantiated) assumption(s)";
181 val p' = (fst o Logic.strip_prems) (Logic.count_prems r', [], r');
182 term2str (hd p') = "y ~= 0";
183 "=====vvv make asms without Trueprop ---vvv";
184 val p' = map HOLogic.dest_Trueprop ((fst o Logic.strip_prems)
185 (Logic.count_prems r', [], r'));
187 [Const ("Not", _) $ (Const ("HOL.eq", _) $ Free ("y", _) $
188 Const ("Groups.zero_class.zero", _))] => ()
189 | _ => error "rewrite.sml assumption changed";
190 "=====^^^ make asms without Trueprop ---^^^";
191 "----- step 4: get the (instantiated) rhs";
192 val t' = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop
193 o Logic.strip_imp_concl) r';
196 "----------- step through 'fun rewrite_terms_' ---------";
197 "----------- step through 'fun rewrite_terms_' ---------";
198 "----------- step through 'fun rewrite_terms_' ---------";
199 "----- step 0: args for rewrite_terms_, local fun";
200 val (thy, ord, erls, equs, t) =
201 (theory "Biegelinie", dummy_ord, Erls, [str2term "x = 0"],
202 str2term "M_b x = -1 * q_0 * x ^^^ 2 / 2 + x * c + c_2");
203 "----- step 1: args for rew_";
204 val ((t', asm'), (rules as r::rs), t) = ((e_term, []), equs, t);
205 "----- step 2: rew_sub";
206 rew_sub thy 1 [] ord erls false [] (Trueprop $ r) t;
207 "----- step 3: step through rew_sub -- inefficient: goes into subterms";
210 val SOME (t', _) = rewrite_terms_ thy dummy_ord Erls equs t;
211 writeln "----------- rewrite_terms_ 1---------------------------";
212 if term2str t' = "M_b 0 = -1 * q_0 * 0 ^^^ 2 / 2 + 0 * c + c_2" then ()
213 else error "rewrite.sml rewrite_terms_ [x = 0]";
215 val equs = [str2term "M_b 0 = 0"];
216 val t = str2term "M_b 0 = -1 * q_0 * 0 ^^^ 2 / 2 + 0 * c + c_2";
217 val SOME (t', _) = rewrite_terms_ thy dummy_ord Erls equs t;
218 writeln "----------- rewrite_terms_ 2---------------------------";
219 if term2str t' = "0 = -1 * q_0 * 0 ^^^ 2 / 2 + 0 * c + c_2" then ()
220 else error "rewrite.sml rewrite_terms_ [M_b 0 = 0]";
222 val equs = [str2term "x = 0", str2term"M_b 0 = 0"];
223 val t = str2term "M_b x = -1 * q_0 * x ^^^ 2 / 2 + x * c + c_2";
224 val SOME (t', _) = rewrite_terms_ thy dummy_ord Erls equs t;
225 writeln "----------- rewrite_terms_ 3---------------------------";
226 if term2str t' = "0 = -1 * q_0 * 0 ^^^ 2 / 2 + 0 * c + c_2" then ()
227 else error "rewrite.sml rewrite_terms_ [x = 0, M_b 0 = 0]";
230 "----------- rewrite_inst_ bdvs -------------------------";
231 "----------- rewrite_inst_ bdvs -------------------------";
232 "----------- rewrite_inst_ bdvs -------------------------";
233 (*see smltest/Scripts/term_G.sml: inst_bdv 2*)
234 val t = str2term"-1 * (q_0 * L ^^^ 2) / 2 + (L * c_3 + c_4) = 0";
235 val bdvs = [(str2term"bdv_1",str2term"c"),
236 (str2term"bdv_2",str2term"c_2"),
237 (str2term"bdv_3",str2term"c_3"),
238 (str2term"bdv_4",str2term"c_4")];
239 (*------------ outcommented WN071210, after inclusion into ROOT.ML
241 rewrite_inst_ thy e_rew_ord
242 (append_rls "erls_isolate_bdvs" e_rls
243 [(Calc ("EqSystem.occur'_exactly'_in",
244 eval_occur_exactly_in
245 "#eval_occur_exactly_in_"))
247 false bdvs (num_str @{separate_bdvs_add) t;
248 (writeln o term2str) t;
249 if term2str t = "L * c_3 + c_4 = 0 + -1 * (-1 * (q_0 * L ^^^ 2) / 2)"
250 then () else error "rewrite.sml rewrite_inst_ bdvs";
252 trace_rewrite:=false;--------------------------------------------*)
255 "----------- check diff 2002--2009-3 --------------------";
256 "----------- check diff 2002--2009-3 --------------------";
257 "----------- check diff 2002--2009-3 --------------------";
258 (*----- 2002 -------------------------------------------------------------------
259 # rls: norm_Rational_noadd_fractions on: 1 / EI * (L * q_0 * x / 2 + -1 *
261 ## rls: discard_minus_ on: 1 / EI * (L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2
263 ### try thm: real_diff_minus
264 ### try thm: sym_real_mult_minus1
265 ## rls: rat_mult_poly on: 1 / EI * (L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2
267 ### try thm: rat_mult_poly_l
268 ### try thm: rat_mult_poly_r
269 #### eval asms: L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2 is_polyexp
270 ==> 1 / EI * (L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2) =
271 1 * (L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2) / EI
272 ##### rls: e_rls-is_polyexp on: L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2
274 ###### try calc: Poly.is'_polyexp'
275 ====== calc. to: False
276 ###### try calc: Poly.is'_polyexp'
277 ###### try calc: Poly.is'_polyexp'
278 #### asms false: ["L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2 is_polyexp"]
279 ----- 2002 NONE rewrite --------------------------------------------------------
280 ----- 2009 should maintain this behaviour, but: --------------------------------
281 # rls: norm_Rational_noadd_fractions on: 1 / EI * (L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2)
282 ## rls: discard_minus on: 1 / EI * (L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2)
283 ### try thm: real_diff_minus
284 ### try thm: sym_real_mult_minus1
285 ## rls: rat_mult_poly on: 1 / EI * (L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2)
286 ### try thm: rat_mult_poly_l
287 ### try thm: rat_mult_poly_r
288 #### eval asms: L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2 is_polyexp
289 ==> 1 / EI * (L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2) =
290 1 * (L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2) / EI
291 ##### rls: e_rls-is_polyexp on: L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2 is_polyexp
292 ###### try calc: Poly.is'_polyexp'
293 ====== calc. to: False
294 ###### try calc: Poly.is'_polyexp'
295 ###### try calc: Poly.is'_polyexp'
296 #### asms accepted: ["L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2 is_polyexp"] stored: ["False"]
297 === rewrites to: 1 * (L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2) / EI
298 ----- 2009 -------------------------------------------------------------------*)
300 (*the situation as was before repair (asm without Trueprop) is outcommented*)
301 val thy = theory "Isac";
302 "===== example which raised the problem =================";
303 val t = @{term "1 / EI * (L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2)"};
304 "----- rewrite_set_inst_ norm_Rational_noadd_fractions--";
305 val subs = [(str2term "bdv", str2term "x")];
306 val rls = norm_Rational_noadd_fractions;
307 val NONE (*SOME (t', _)*) = rewrite_set_inst_ thy true subs rls t;
308 "----- rewrite_ rat_mult_poly_r--------------------------";
309 val thm = @{thm rat_mult_poly_r};
310 "?c::real is_polyexp ==> (?a::real) / (?b::real) * ?c = ?a * ?c / ?b";
311 val erls = append_rls "e_rls-is_polyexp" e_rls
312 [Calc ("Poly.is'_polyexp", eval_is_polyexp "")];
313 val NONE (*SOME (t'', _)*) = rewrite_ thy dummy_ord erls true thm t;
314 (*t' = t''; (*false because of further rewrites in t'*)*)
315 "----- rew_sub --------------------------------";
316 val (t''', _, _, _) = rew_sub thy 0 [] dummy_ord erls true [] (prop_of thm) t;
317 (*t'' = t'''; (*true*)*)
318 "----- rewrite_set_ erls --------------------------------";
319 val cond = @{term "(L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2)"};
320 val NONE = rewrite_set_ thy true erls cond;
321 (* ^^^^^ goes with '====== calc. to: False' above from beginning*)
323 writeln "===== maximally simplified example =====================";
324 val t = @{term "a / b * (x / x ^^^ 2)"};
325 "?c::real is_polyexp ==> (?a::real) / (?b::real) * ?c = ?a * ?c / ?b";
326 writeln "----- rewrite_set_inst_ norm_Rational_noadd_fractions--";
327 val (*NONE*) SOME (t', asm) = rewrite_set_inst_ thy true subs rls t;
328 term2str t' = "a * x / (b * x ^^^ 2)"; (*rew. by thm outside test case*)
329 (*checked visually: trace_rewrite looks like above for 2009*)
331 trace_rewrite := false; (*<<<<<<<<<<<<<<<<<<<<<###############################*)
332 (*show_types := false;*)
333 writeln "----- rewrite_ rat_mult_poly_r--------------------------";
334 val NONE (*SOME (t'', _)*) = rewrite_ thy dummy_ord erls true thm t;
335 (*t' = t''; (*false because of further rewrites in t'*)*)
336 writeln "----- rew_sub --------------------------------";
337 val (t''', _, _, _) = rew_sub thy 0 [] dummy_ord erls true [] (prop_of thm) t;
338 (*t'' = t'''; (*true*)*)
339 writeln "----- rewrite_set_ erls --------------------------------";
340 val cond = @{term "(x / x ^^^ 2)"};
341 val NONE = rewrite_set_ thy true erls cond;
342 (* ^^^^^ goes with '====== calc. to: False' above from beginning*)
343 trace_rewrite := false; (*<<<<<<<<<<<<<<<<<<<<<###############################*)
344 "--------------------------------------------------------";
347 "----------- compare all prepat's existing 2010 ---------";
348 "----------- compare all prepat's existing 2010 ---------";
349 "----------- compare all prepat's existing 2010 ---------";
350 (* Christian Urban, 101001
357 val parser = Args.context -- Scan.lift Args.name_source
358 fun term_pat (ctxt, str) = str |> ProofContext.read_term_pattern ctxt
359 |> ML_Syntax.print_term |> ML_Syntax.atomic
361 ML_Antiquote.inline "term_pat" (parser >> term_pat)
366 val t = @{term "a + b * x = (0 ::real)"};
367 val pat = @{term_pat "?l = (?r ::real)"};
368 val precond = @{term_pat "is_polynomial (?l::real)"};
369 val inst = Pattern.match @{theory} (pat, t) (Vartab.empty, Vartab.empty);
373 Envir.subst_term inst precond
374 |> Syntax.string_of_term @{context}
378 val thy = theory "Isac";
379 val t = @{term "a + b * x = (0 ::real)"};
380 val pat = parse_patt thy "?l = (?r ::real)";
381 val precond = parse_patt thy "is_polynomial (?l::real)";(*no infix def*)
382 val precond = parse_patt thy "(?l::real) is_expanded";
384 val inst = Pattern.match thy (pat, t) (Vartab.empty, Vartab.empty);
385 val preinst = Envir.subst_term inst precond;
388 "===== Rational.thy: cancel ===";
389 (* pat matched with the current term gives an environment
390 (or not: hen the Rrls not applied);
391 if pre1 and pre2 evaluate to HOLogic.true_const in this environment,
392 then the Rrls is applied. *)
393 val t = str2term "(a + b) / c ::real";
394 val pat = parse_patt thy "?r / ?s ::real";
395 val pres = [parse_patt thy "?r is_expanded", parse_patt thy "?s is_expanded"];
396 val prepat = [(pres, pat)];
397 val erls = rational_erls;
398 (* erls got from Rrls {erls, prepat, scr = Rfuns {normal_form, ...}, ...} *)
400 val subst = Pattern.match thy (pat, t) (Vartab.empty, Vartab.empty);
401 val asms = map (Envir.subst_term subst) pres;
402 if terms2str asms = "[\"a + b is_expanded\",\"c is_expanded\"]"
403 then () else error "rewrite.sml: prepat cancel subst";
404 if ([], true) = eval__true thy 0 asms [] erls
405 then () else error "rewrite.sml: prepat cancel eval__true";
407 "===== Rational.thy: common_nominator_p ===";
408 (* if each pat* matches with the current term, the Rrls is applied
409 (there are no preconditions to be checked, they are HOLogic.true_const) *)
410 val t = str2term "a / b + 1 / 2";
411 val pat = parse_patt thy "?r / ?s + ?u / ?v";
412 val pres = [HOLogic.true_const];
413 val prepat = [(pres, pat)];
414 val erls = rational_erls;
415 (* erls got from Rrls {erls, prepat, scr = Rfuns {normal_form, ...}, ...} *)
417 val subst = Pattern.match thy (pat, t) (Vartab.empty, Vartab.empty);
418 if ([], true) = eval__true thy 0 (map (Envir.subst_term subst) pres) [] erls
419 then () else error "rewrite.sml: prepat common_nominator_p";
421 "===== Poly.thy: order_mult_ ===";
422 (* ?p matched with the current term gives an environment,
423 which evaluates (the instantiated) "p is_multUnordered" to true*)
424 val t = str2term "x^^^2 * x";
425 val pat = parse_patt thy "?p :: real"
426 val pres = [parse_patt thy "?p is_multUnordered"];
427 val prepat = [(pres, pat)];
428 val erls = append_rls "e_rls-is_multUnordered" e_rls
429 [Calc ("Poly.is'_multUnordered",
430 eval_is_multUnordered "")];
432 val subst = Pattern.match thy (pat, t) (Vartab.empty, Vartab.empty);
433 val asms = map (Envir.subst_term subst) pres;
434 if terms2str asms = "[\"x ^^^ 2 * x is_multUnordered\"]"
435 then () else error "rewrite.sml: prepat order_mult_ subst";
436 if ([], true) = eval__true thy 0 asms [] erls
437 then () else error "rewrite.sml: prepat order_mult_ eval__true";
440 "----------- fun app_rev, Rrls, -------------------------";
441 "----------- fun app_rev, Rrls, -------------------------";
442 "----------- fun app_rev, Rrls, -------------------------";
443 val t = str2term "x^^^2 * x";
444 if is_multUnordered t then () else error "rewrite.sml diff. is_multUnordered 2";
445 val tm = str2term "(x^^^2 * x) is_multUnordered";
446 case eval_is_multUnordered "testid" "" tm thy of
447 SOME (_, Const ("HOL.Trueprop", _) $
448 (Const ("HOL.eq", _) $
449 (Const ("Poly.is'_multUnordered", _) $ _) $
450 Const ("True", _))) => ()
451 | _ => error "rewrite.sml diff. eval_is_multUnordered 2";
453 tracing "----- begin rewrite x^^^2 * x ---"; trace_rewrite := true;
454 val SOME (t', _) = rewrite_set_ thy true order_mult_ t;
455 tracing "----- end rewrite x^^^2 * x ---"; trace_rewrite := false;
456 if term2str t' = "x * x ^^^ 2" then ()
457 else error "rewrite.sml Poly.is'_multUnordered doesn't work";
459 (* for achieving the previous result, the following code was taken apart *)
460 "----- rewrite__set_ ---";
461 val (thy, i, _, _, (rrls as Rrls _), t) = (thy, 0, true, [], order_mult_, tm);
462 val (t', asm, rew) = app_rev thy (i+1) rrls t;
464 val (thy, i, rrls, t) = (thy, (i+1), rrls, t);
465 fun chk_prepat thy erls [] t = true
466 | chk_prepat thy erls prepat t =
467 let fun chk (pres, pat) =
468 (let val subst: Type.tyenv * Envir.tenv =
469 Pattern.match thy (pat, t)
470 (Vartab.empty, Vartab.empty)
471 in snd (eval__true thy (i+1)
472 (map (Envir.subst_term subst) pres)
476 fun scan_ f [] = false (*scan_ NEVER called by []*)
477 | scan_ f (pp::pps) = if f pp then true
479 in scan_ chk prepat end;
481 (*.apply the normal_form of a rev-set.*)
482 fun app_rev' thy (Rrls{erls,prepat,scr=Rfuns{normal_form,...},...}) t =
483 if chk_prepat thy erls prepat t
484 then ((*tracing("### app_rev': t = "^(term2str t));*)
487 (*fixme val NONE = app_rev' thy rrls t;*)
488 "----- app_rev' ---";
489 val (thy, Rrls{erls,prepat,scr=Rfuns{normal_form,...},...}, t) = (thy, rrls, t);
490 (*fixme false*) chk_prepat thy erls prepat t;
491 "----- chk_prepat ---";
492 val (thy, erls, prepat, t) = (thy, erls, prepat, t);
493 fun chk (pres, pat) =
494 (let val subst: Type.tyenv * Envir.tenv =
495 Pattern.match thy (pat, t)
496 (Vartab.empty, Vartab.empty)
497 in snd (eval__true thy (i+1)
498 (map (Envir.subst_term subst) pres)
502 fun scan_ f [] = false (*scan_ NEVER called by []*)
503 | scan_ f (pp::pps) = if f pp then true
505 tracing "=== poly.sml: scan_ chk prepat begin";
507 tracing "=== poly.sml: scan_ chk prepat end";
511 (*reestablish...*) val t = str2term "x ^^^ 2 * x";
512 val [(pres, pat)] = prepat;
513 val subst: Type.tyenv * Envir.tenv =
514 Pattern.match thy (pat, t)
515 (Vartab.empty, Vartab.empty);
517 (*fixme: asms = ["p is_multUnordered"]...instantiate*)
518 "----- eval__true ---";
519 val asms = (map (Envir.subst_term subst) pres);
520 if terms2str asms = "[\"x ^^^ 2 * x is_multUnordered\"]" then ()
521 else error "rewrite.sml: diff. is_multUnordered, asms";
522 val (thy, i, asms, bdv, rls) =
523 (thy, (i+1), [str2term "(x^^^2 * x) is_multUnordered"],
524 [] : (term * term) list, erls);
525 case eval__true thy i asms bdv rls of
527 | _ => error "rewrite.sml: diff. is_multUnordered, eval__true";
529 -.-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.*)