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 "----------- 2011 thms with axclasses -------------------";
23 "--------------------------------------------------------";
24 "--------------------------------------------------------";
25 "--------------------------------------------------------";
28 "----------- assemble rewrite ---------------------------";
29 "----------- assemble rewrite ---------------------------";
30 "----------- assemble rewrite ---------------------------";
31 "===== rewriting by thm with 'a";
32 (*show_types := true;*)
34 val thy = @{theory Complex_Main};
35 val ctxt = @{context};
36 val thm = @{thm add_commute};
37 val t = (term_of o the) (parse thy "((r + u) + t) + s");
38 "----- from old: fun rewrite__";
40 val r = (((inst_bdv bdv) o norm o #prop o rep_thm) thm);
41 "----- from old: and rew_sub";
42 val (LHS,RHS) = (dest_equals' o strip_trueprop
43 o Logic.strip_imp_concl) r;
45 val insts = Pattern.match thy (LHS,t) (Vartab.empty, Vartab.empty);*)
46 "----- fun match_rew in Pure/pattern.ML";
47 val rtm = the_default RHS (Term.rename_abs LHS t RHS);
49 writeln(Syntax.string_of_term ctxt rtm);
50 writeln(Syntax.string_of_term ctxt LHS);
51 writeln(Syntax.string_of_term ctxt t);
53 (Pattern.match thy (LHS, t) (Vartab.empty, Vartab.empty));
54 val (rew, RHS) = (Envir.subst_term
55 (Pattern.match thy (LHS, t) (Vartab.empty, Vartab.empty)) rtm, rtm);
56 (*lookup in isabelle?trace?response...*)
57 writeln(Syntax.string_of_term ctxt rew);
58 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');
79 "----------- test rewriting without Isac's thys ---------";
80 "----------- test rewriting without Isac's thys ---------";
81 "----------- test rewriting without Isac's thys ---------";
83 "===== rewriting with Isabelle2009-1 only, i.e without isac-hacks";
84 val thy = @{theory Complex_Main};
85 val ctxt = @{context};
86 val thm = @{thm add_commute};
87 val tm = @{term "x + y*z::real"};
89 val SOME (r,_) = (rewrite_ thy dummy_ord e_rls false thm tm)
90 handle _ => error "rewrite.sml diff.behav. in rewriting";
91 (*is displayed on _TOP_ of <response> buffer...*)
92 Pretty.writeln (ProofContext.pretty_term_abbrev @{context} r);
93 if r = @{term "y*z + x::real"}
94 then () else error "rewrite.sml diff.result in rewriting";
96 "----- rewriting a subterm";
97 val tm = @{term "w*(x + y*z)::real"};
99 val SOME (r,_) = (rewrite_ thy dummy_ord e_rls false thm tm)
100 handle _ => error "rewrite.sml diff.behav. in rew_sub";
102 "----- ordered rewriting";
103 fun tord (_:subst) pp = Term_Ord.termless pp;
104 if tord [] (@{term "x + y*z::real"}, @{term "y*z + x::real"}) then ()
105 else error "rewrite.sml diff.behav. in ord.rewr.";
107 val NONE = (rewrite_ thy tord e_rls false thm tm)
108 handle _ => error "rewrite.sml diff.behav. in rewriting";
109 (*is displayed on _TOP_ of <response> buffer...*)
110 Pretty.writeln (ProofContext.pretty_term_abbrev @{context} r);
112 val tm = @{term "x*y + z::real"};
113 val SOME (r,_) = (rewrite_ thy tord e_rls false thm tm)
114 handle _ => error "rewrite.sml diff.behav. in rewriting";
117 "----------- conditional rewriting without Isac's thys --";
118 "----------- conditional rewriting without Isac's thys --";
119 "----------- conditional rewriting without Isac's thys --";
121 "===== prepr cond.rew. with Pattern.match";
122 val thy = @{theory Complex_Main};
123 val ctxt = @{context};
124 val thm = @{thm nonzero_mult_divide_cancel_right};
125 val rule = Thm.prop_of thm;
126 val tm = @{term "x*2 / 2::real"};
128 val prem = Logic.strip_imp_prems rule;
129 val nps = Logic.count_prems rule;
130 val prems = Logic.strip_prems (nps, [], rule);
132 val eq = Logic.strip_imp_concl rule;
133 val (LHS, RHS) = (HOLogic.dest_eq o HOLogic.dest_Trueprop) eq;
135 val mtcs = Pattern.match thy (LHS, tm) (Vartab.empty, Vartab.empty);
136 val rule' = Envir.subst_term mtcs rule;
138 val prems' = (fst o Logic.strip_prems)
139 (Logic.count_prems rule', [], rule');
140 val RHS' = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop
141 o Logic.strip_imp_concl) rule';
143 "----- conditional rewriting creating an assumption";
144 "----- conditional rewriting creating an assumption";
145 val tm = @{term "x*y / y::real"};
146 val SOME (rew, asm) = (rewrite_ thy dummy_ord e_rls false thm tm)
147 handle _ => error "rewrite.sml diff.behav. in cond.rew.";
149 if rew = @{term "x::real"} then () (* the rewrite is _NO_ Trueprop *)
150 else error "rewrite.sml diff.result in cond.rew.";
152 if hd asm = @{term "~ y = (0::real)"} (* dropped Trueprop $ ...*)
153 then () else error "rewrite.sml diff.asm in cond.rew.";
154 "----- conditional rewriting immediately: can only be done with ";
155 "------Isabelle numerals, because erls cannot handle them yet.";
158 "----------- step through 'and rew_sub': ----------------";
159 "----------- step through 'and rew_sub': ----------------";
160 "----------- step through 'and rew_sub': ----------------";
161 (*and make asms without Trueprop, beginning with the result:*)
162 val tm = @{term "x*y / y::real"};
163 val (t', asm, _, _) = rew_sub thy 0 [] dummy_ord e_rls true [] (prop_of thm) tm;
164 (*show_types := false;*)
165 "----- evaluate arguments";
166 val (thy, i, bdv, tless, rls, put_asm, lrd, r, t) =
167 (thy, 0, [], dummy_ord, e_rls, true, [], (prop_of thm), tm);
168 "----- step 1: LHS, RHS of rule";
169 val (LHS, RHS) = (HOLogic.dest_eq o HOLogic.dest_Trueprop
170 o Logic.strip_imp_concl) r;
171 term2str r = "?b ~= (0::?'a) ==> ?a * ?b / ?b = ?a";
172 term2str LHS = "?a * ?b / ?b"; term2str RHS = "?a";
173 "----- step 2: the rule instantiated";
174 val r' = Envir.subst_term
175 (Pattern.match thy (LHS, t) (Vartab.empty, Vartab.empty)) r;
176 term2str r' = "y ~= 0 ==> x * y / y = x";
177 "----- step 3: get the (instantiated) assumption(s)";
178 val p' = (fst o Logic.strip_prems) (Logic.count_prems r', [], r');
179 term2str (hd p') = "y ~= 0";
180 "=====vvv make asms without Trueprop ---vvv";
181 val p' = map HOLogic.dest_Trueprop ((fst o Logic.strip_prems)
182 (Logic.count_prems r', [], r'));
184 [Const ("HOL.Not", _) $ (Const ("HOL.eq", _) $ Free ("y", _) $
185 Const ("Groups.zero_class.zero", _))] => ()
186 | _ => error "rewrite.sml assumption changed";
187 "=====^^^ make asms without Trueprop ---^^^";
188 "----- step 4: get the (instantiated) RHS";
189 val t' = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop
190 o Logic.strip_imp_concl) r';
193 "----------- step through 'fun rewrite_terms_' ---------";
194 "----------- step through 'fun rewrite_terms_' ---------";
195 "----------- step through 'fun rewrite_terms_' ---------";
196 "----- step 0: args for rewrite_terms_, local fun";
197 val (thy, ord, erls, equs, t) =
198 (@{theory "Biegelinie"}, dummy_ord, Erls, [str2term "x = 0"],
199 str2term "M_b x = -1 * q_0 * x ^^^ 2 / 2 + x * c + c_2");
200 "----- step 1: args for rew_";
201 val ((t', asm'), (rules as r::rs), t) = ((e_term, []), equs, t);
202 "----- step 2: rew_sub";
203 rew_sub thy 1 [] ord erls false [] (Trueprop $ r) t;
204 "----- step 3: step through rew_sub -- inefficient: goes into subterms";
207 val SOME (t', _) = rewrite_terms_ thy dummy_ord Erls equs t;
208 writeln "----------- rewrite_terms_ 1---------------------------";
209 if term2str t' = "M_b 0 = -1 * q_0 * 0 ^^^ 2 / 2 + 0 * c + c_2" then ()
210 else error "rewrite.sml rewrite_terms_ [x = 0]";
212 val equs = [str2term "M_b 0 = 0"];
213 val t = str2term "M_b 0 = -1 * q_0 * 0 ^^^ 2 / 2 + 0 * c + c_2";
214 val SOME (t', _) = rewrite_terms_ thy dummy_ord Erls equs t;
215 writeln "----------- rewrite_terms_ 2---------------------------";
216 if term2str t' = "0 = -1 * q_0 * 0 ^^^ 2 / 2 + 0 * c + c_2" then ()
217 else error "rewrite.sml rewrite_terms_ [M_b 0 = 0]";
219 val equs = [str2term "x = 0", str2term"M_b 0 = 0"];
220 val t = str2term "M_b x = -1 * q_0 * x ^^^ 2 / 2 + x * c + c_2";
221 val SOME (t', _) = rewrite_terms_ thy dummy_ord Erls equs t;
222 writeln "----------- rewrite_terms_ 3---------------------------";
223 if term2str t' = "0 = -1 * q_0 * 0 ^^^ 2 / 2 + 0 * c + c_2" then ()
224 else error "rewrite.sml rewrite_terms_ [x = 0, M_b 0 = 0]";
227 "----------- rewrite_inst_ bdvs -------------------------";
228 "----------- rewrite_inst_ bdvs -------------------------";
229 "----------- rewrite_inst_ bdvs -------------------------";
230 (*see smltest/Scripts/term_G.sml: inst_bdv 2*)
231 val t = str2term"-1 * (q_0 * L ^^^ 2) / 2 + (L * c_3 + c_4) = 0";
232 val bdvs = [(str2term"bdv_1",str2term"c"),
233 (str2term"bdv_2",str2term"c_2"),
234 (str2term"bdv_3",str2term"c_3"),
235 (str2term"bdv_4",str2term"c_4")];
236 (*------------ outcommented WN071210, after inclusion into ROOT.ML
238 rewrite_inst_ thy e_rew_ord
239 (append_rls "erls_isolate_bdvs" e_rls
240 [(Calc ("EqSystem.occur'_exactly'_in",
241 eval_occur_exactly_in
242 "#eval_occur_exactly_in_"))
244 false bdvs (num_str @{separate_bdvs_add) t;
245 (writeln o term2str) t;
246 if term2str t = "L * c_3 + c_4 = 0 + -1 * (-1 * (q_0 * L ^^^ 2) / 2)"
247 then () else error "rewrite.sml rewrite_inst_ bdvs";
249 trace_rewrite:=false;--------------------------------------------*)
252 "----------- check diff 2002--2009-3 --------------------";
253 "----------- check diff 2002--2009-3 --------------------";
254 "----------- check diff 2002--2009-3 --------------------";
255 (*----- 2002 -------------------------------------------------------------------
256 # rls: norm_Rational_noadd_fractions on: 1 / EI * (L * q_0 * x / 2 + -1 *
258 ## rls: discard_minus_ on: 1 / EI * (L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2
260 ### try thm: real_diff_minus
261 ### try thm: sym_real_mult_minus1
262 ## rls: rat_mult_poly on: 1 / EI * (L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2
264 ### try thm: rat_mult_poly_l
265 ### try thm: rat_mult_poly_r
266 #### eval asms: L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2 is_polyexp
267 ==> 1 / EI * (L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2) =
268 1 * (L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2) / EI
269 ##### rls: e_rls-is_polyexp on: L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2
271 ###### try calc: Poly.is'_polyexp'
272 ====== calc. to: False
273 ###### try calc: Poly.is'_polyexp'
274 ###### try calc: Poly.is'_polyexp'
275 #### asms false: ["L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2 is_polyexp"]
276 ----- 2002 NONE rewrite --------------------------------------------------------
277 ----- 2009 should maintain this behaviour, but: --------------------------------
278 # rls: norm_Rational_noadd_fractions on: 1 / EI * (L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2)
279 ## rls: discard_minus on: 1 / EI * (L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2)
280 ### try thm: real_diff_minus
281 ### try thm: sym_real_mult_minus1
282 ## rls: rat_mult_poly on: 1 / EI * (L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2)
283 ### try thm: rat_mult_poly_l
284 ### try thm: rat_mult_poly_r
285 #### eval asms: L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2 is_polyexp
286 ==> 1 / EI * (L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2) =
287 1 * (L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2) / EI
288 ##### rls: e_rls-is_polyexp on: L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2 is_polyexp
289 ###### try calc: Poly.is'_polyexp'
290 ====== calc. to: False
291 ###### try calc: Poly.is'_polyexp'
292 ###### try calc: Poly.is'_polyexp'
293 #### asms accepted: ["L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2 is_polyexp"] stored: ["False"]
294 === rewrites to: 1 * (L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2) / EI
295 ----- 2009 -------------------------------------------------------------------*)
297 (*the situation as was before repair (asm without Trueprop) is outcommented*)
298 val thy = @{theory "Isac"};
299 "===== example which raised the problem =================";
300 val t = @{term "1 / EI * (L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2)"};
301 "----- rewrite_set_inst_ norm_Rational_noadd_fractions--";
302 val subs = [(str2term "bdv", str2term "x")];
303 val rls = norm_Rational_noadd_fractions;
304 val NONE (*SOME (t', _)*) = rewrite_set_inst_ thy true subs rls t;
305 "----- rewrite_ rat_mult_poly_r--------------------------";
306 val thm = @{thm rat_mult_poly_r};
307 "?c::real is_polyexp ==> (?a::real) / (?b::real) * ?c = ?a * ?c / ?b";
308 val erls = append_rls "e_rls-is_polyexp" e_rls
309 [Calc ("Poly.is'_polyexp", eval_is_polyexp "")];
310 val NONE (*SOME (t'', _)*) = rewrite_ thy dummy_ord erls true thm t;
311 (*t' = t''; (*false because of further rewrites in t'*)*)
312 "----- rew_sub --------------------------------";
313 val (t''', _, _, _) = rew_sub thy 0 [] dummy_ord erls true [] (prop_of thm) t;
314 (*t'' = t'''; (*true*)*)
315 "----- rewrite_set_ erls --------------------------------";
316 val cond = @{term "(L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2)"};
317 val NONE = rewrite_set_ thy true erls cond;
318 (* ^^^^^ goes with '====== calc. to: False' above from beginning*)
320 writeln "===== maximally simplified example =====================";
321 val t = @{term "a / b * (x / x ^^^ 2)"};
322 "?c::real is_polyexp ==> (?a::real) / (?b::real) * ?c = ?a * ?c / ?b";
323 writeln "----- rewrite_set_inst_ norm_Rational_noadd_fractions--";
324 val (*NONE*) SOME (t', asm) = rewrite_set_inst_ thy true subs rls t;
325 term2str t' = "a * x / (b * x ^^^ 2)"; (*rew. by thm outside test case*)
326 (*checked visually: trace_rewrite looks like above for 2009*)
328 writeln "----- rewrite_ rat_mult_poly_r--------------------------";
329 val NONE (*SOME (t'', _)*) = rewrite_ thy dummy_ord erls true thm t;
330 (*t' = t''; (*false because of further rewrites in t'*)*)
331 writeln "----- rew_sub --------------------------------";
332 val (t''', _, _, _) = rew_sub thy 0 [] dummy_ord erls true [] (prop_of thm) t;
333 (*t'' = t'''; (*true*)*)
334 writeln "----- rewrite_set_ erls --------------------------------";
335 val cond = @{term "(x / x ^^^ 2)"};
336 val NONE = rewrite_set_ thy true erls cond;
337 (* ^^^^^ goes with '====== calc. to: False' above from beginning*)
340 "----------- compare all prepat's existing 2010 ---------";
341 "----------- compare all prepat's existing 2010 ---------";
342 "----------- compare all prepat's existing 2010 ---------";
343 val thy = @{theory "Isac"};
344 val t = @{term "a + b * x = (0 ::real)"};
345 val pat = parse_patt thy "?l = (?r ::real)";
346 val precond = parse_patt thy "is_polynomial (?l::real)";(*no infix def*)
347 val precond = parse_patt thy "(?l::real) is_expanded";
349 val inst = Pattern.match thy (pat, t) (Vartab.empty, Vartab.empty);
350 val preinst = Envir.subst_term inst precond;
353 "===== Rational.thy: cancel ===";
354 (* pat matched with the current term gives an environment
355 (or not: hen the Rrls not applied);
356 if pre1 and pre2 evaluate to HOLogic.true_const in this environment,
357 then the Rrls is applied. *)
358 val t = str2term "(a + b) / c ::real";
359 val pat = parse_patt thy "?r / ?s ::real";
360 val pres = [parse_patt thy "?r is_expanded", parse_patt thy "?s is_expanded"];
361 val prepat = [(pres, pat)];
362 val erls = rational_erls;
363 (* erls got from Rrls {erls, prepat, scr = Rfuns {normal_form, ...}, ...} *)
365 val subst = Pattern.match thy (pat, t) (Vartab.empty, Vartab.empty);
366 val asms = map (Envir.subst_term subst) pres;
367 if terms2str asms = "[\"a + b is_expanded\",\"c is_expanded\"]"
368 then () else error "rewrite.sml: prepat cancel subst";
369 if ([], true) = eval__true thy 0 asms [] erls
370 then () else error "rewrite.sml: prepat cancel eval__true";
372 "===== Rational.thy: common_nominator_p ===";
373 (* if each pat* matches with the current term, the Rrls is applied
374 (there are no preconditions to be checked, they are HOLogic.true_const) *)
375 val t = str2term "a / b + 1 / 2";
376 val pat = parse_patt thy "?r / ?s + ?u / ?v";
377 val pres = [HOLogic.true_const];
378 val prepat = [(pres, pat)];
379 val erls = rational_erls;
380 (* erls got from Rrls {erls, prepat, scr = Rfuns {normal_form, ...}, ...} *)
382 val subst = Pattern.match thy (pat, t) (Vartab.empty, Vartab.empty);
383 if ([], true) = eval__true thy 0 (map (Envir.subst_term subst) pres) [] erls
384 then () else error "rewrite.sml: prepat common_nominator_p";
386 "===== Poly.thy: order_mult_ ===";
387 (* ?p matched with the current term gives an environment,
388 which evaluates (the instantiated) "p is_multUnordered" to true*)
389 val t = str2term "x^^^2 * x";
390 val pat = parse_patt thy "?p :: real"
391 val pres = [parse_patt thy "?p is_multUnordered"];
392 val prepat = [(pres, pat)];
393 val erls = append_rls "e_rls-is_multUnordered" e_rls
394 [Calc ("Poly.is'_multUnordered",
395 eval_is_multUnordered "")];
397 val subst = Pattern.match thy (pat, t) (Vartab.empty, Vartab.empty);
398 val asms = map (Envir.subst_term subst) pres;
399 if terms2str asms = "[\"x ^^^ 2 * x is_multUnordered\"]"
400 then () else error "rewrite.sml: prepat order_mult_ subst";
401 if ([], true) = eval__true thy 0 asms [] erls
402 then () else error "rewrite.sml: prepat order_mult_ eval__true";
405 "----------- fun app_rev, Rrls, -------------------------";
406 "----------- fun app_rev, Rrls, -------------------------";
407 "----------- fun app_rev, Rrls, -------------------------";
408 val t = str2term "x^^^2 * x";
410 if is_multUnordered t then () else error "rewrite.sml diff. is_multUnordered 2";
411 val tm = str2term "(x^^^2 * x) is_multUnordered";
412 eval_is_multUnordered "testid" "" tm thy;
414 case eval_is_multUnordered "testid" "" tm thy of
415 SOME (_, Const ("HOL.Trueprop", _) $
416 (Const ("HOL.eq", _) $
417 (Const ("Poly.is'_multUnordered", _) $ _) $
418 Const ("HOL.True", _))) => ()
419 | _ => error "rewrite.sml diff. eval_is_multUnordered 2b";
421 tracing "----- begin rewrite x^^^2 * x ---"; trace_rewrite := true;
422 val SOME (t', _) = rewrite_set_ thy true order_mult_ t;
423 tracing "----- end rewrite x^^^2 * x ---"; trace_rewrite := false;
424 if term2str t' = "x * x ^^^ 2" then ()
425 else error "rewrite.sml Poly.is'_multUnordered doesn't work";
427 (* for achieving the previous result, the following code was taken apart *)
428 "----- rewrite__set_ ---";
429 val (thy, i, _, _, (rrls as Rrls _), t) = (thy, 0, true, [], order_mult_, tm);
430 val (t', asm, rew) = app_rev thy (i+1) rrls t;
432 val (thy, i, rrls, t) = (thy, (i+1), rrls, t);
433 fun chk_prepat thy erls [] t = true
434 | chk_prepat thy erls prepat t =
435 let fun chk (pres, pat) =
436 (let val subst: Type.tyenv * Envir.tenv =
437 Pattern.match thy (pat, t)
438 (Vartab.empty, Vartab.empty)
439 in snd (eval__true thy (i+1)
440 (map (Envir.subst_term subst) pres)
444 fun scan_ f [] = false (*scan_ NEVER called by []*)
445 | scan_ f (pp::pps) = if f pp then true
447 in scan_ chk prepat end;
449 (*.apply the normal_form of a rev-set.*)
450 fun app_rev' thy (Rrls{erls,prepat,scr=Rfuns{normal_form,...},...}) t =
451 if chk_prepat thy erls prepat t
452 then ((*tracing("### app_rev': t = "^(term2str t));*)
455 (*fixme val NONE = app_rev' thy rrls t;*)
456 "----- app_rev' ---";
457 val (thy, Rrls{erls,prepat,scr=Rfuns{normal_form,...},...}, t) = (thy, rrls, t);
458 (*fixme false*) chk_prepat thy erls prepat t;
459 "----- chk_prepat ---";
460 val (thy, erls, prepat, t) = (thy, erls, prepat, t);
461 fun chk (pres, pat) =
462 (let val subst: Type.tyenv * Envir.tenv =
463 Pattern.match thy (pat, t)
464 (Vartab.empty, Vartab.empty)
465 in snd (eval__true thy (i+1)
466 (map (Envir.subst_term subst) pres)
470 fun scan_ f [] = false (*scan_ NEVER called by []*)
471 | scan_ f (pp::pps) = if f pp then true
473 tracing "=== poly.sml: scan_ chk prepat begin";
475 tracing "=== poly.sml: scan_ chk prepat end";
478 (*reestablish...*) val t = str2term "x ^^^ 2 * x";
479 val [(pres, pat)] = prepat;
480 val subst: Type.tyenv * Envir.tenv =
481 Pattern.match thy (pat, t)
482 (Vartab.empty, Vartab.empty);
484 (*fixme: asms = ["p is_multUnordered"]...instantiate*)
485 "----- eval__true ---";
486 val asms = (map (Envir.subst_term subst) pres);
487 if terms2str asms = "[\"x ^^^ 2 * x is_multUnordered\"]" then ()
488 else error "rewrite.sml: diff. is_multUnordered, asms";
489 val (thy, i, asms, bdv, rls) =
490 (thy, (i+1), [str2term "(x^^^2 * x) is_multUnordered"],
491 [] : (term * term) list, erls);
492 case eval__true thy i asms bdv rls of
494 | _ => error "rewrite.sml: diff. is_multUnordered, eval__true";
496 "----------- 2011 thms with axclasses -------------------";
497 "----------- 2011 thms with axclasses -------------------";
498 "----------- 2011 thms with axclasses -------------------";
499 val thm = num_str @{thm divide_1};
500 val prop = prop_of thm;
501 atomty prop; (*Type 'a*)
502 val t = str2term "(2*x)/1"; (*Type real*)
504 val (thy, ro, er, inst) =
505 (@{theory "Isac"}, tless_true, eval_rls, [(@{term "bdv::real"}, @{term "x::real"})]);
506 val SOME (t, _) = rewrite_ thy ro er true thm t; (*real matches 'a ?via ring? etc*)