Test_Isac works again, perfectly ..
# the same tests works as in 8df4b6196660 (the *child* of "Test_Isac works...")
# ..EXCEPT those marked with "exception Div raised"
# for general state of tests see Test_Isac section {* history of tests *}.
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 "----------- repair NO asms from rls RatEq_eliminate ----";
24 "--------------------------------------------------------";
25 "--------------------------------------------------------";
26 "--------------------------------------------------------";
29 "----------- assemble rewrite ---------------------------";
30 "----------- assemble rewrite ---------------------------";
31 "----------- assemble rewrite ---------------------------";
32 "===== rewriting by thm with 'a";
33 (*show_types := true;*)
35 val thy = @{theory Complex_Main};
36 val ctxt = @{context};
37 val thm = @{thm add_commute};
38 val t = (term_of o the) (parse thy "((r + u) + t) + s");
39 "----- from old: fun rewrite__";
41 val r = (((inst_bdv bdv) o norm o #prop o rep_thm) thm);
42 "----- from old: and rew_sub";
43 val (LHS,RHS) = (dest_equals' o strip_trueprop
44 o Logic.strip_imp_concl) r;
46 val insts = Pattern.match thy (LHS,t) (Vartab.empty, Vartab.empty);*)
47 "----- fun match_rew in Pure/pattern.ML";
48 val rtm = the_default RHS (Term.rename_abs LHS t RHS);
50 writeln(Syntax.string_of_term ctxt rtm);
51 writeln(Syntax.string_of_term ctxt LHS);
52 writeln(Syntax.string_of_term ctxt t);
54 (Pattern.match thy (LHS, t) (Vartab.empty, Vartab.empty));
55 val (rew, RHS) = (Envir.subst_term
56 (Pattern.match thy (LHS, t) (Vartab.empty, Vartab.empty)) rtm, rtm);
57 (*lookup in isabelle?trace?response...*)
58 writeln(Syntax.string_of_term ctxt rew);
59 writeln(Syntax.string_of_term ctxt RHS);
60 "===== rewriting: prep insertion into rew_sub";
61 val thy = @{theory Complex_Main};
62 val ctxt = @{context};
63 val thm = @{thm nonzero_mult_divide_cancel_right};
64 val r = Thm.prop_of thm;
65 val tm = @{term "x*2 / 2::real"};
67 val (LHS, RHS) = (HOLogic.dest_eq o HOLogic.dest_Trueprop
68 o Logic.strip_imp_concl) r;
69 val r' = Envir.subst_term (Pattern.match thy (LHS, tm)
70 (Vartab.empty, Vartab.empty)) r;
71 val p' = (fst o Logic.strip_prems) (Logic.count_prems r', [], r');
72 val t' = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop
73 o Logic.strip_imp_concl) r';
75 (*is displayed on top of <response> buffer...*)
76 Pretty.writeln (Proof_Context.pretty_term_abbrev @{context} r');
77 Pretty.writeln (Proof_Context.pretty_term_abbrev @{context} t');
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"};
90 val SOME (r,_) = (rewrite_ thy dummy_ord e_rls false thm tm)
91 handle _ => error "rewrite.sml diff.behav. in rewriting";
92 (*is displayed on _TOP_ of <response> buffer...*)
93 Pretty.writeln (Proof_Context.pretty_term_abbrev @{context} r);
94 if r = @{term "y*z + x::real"}
95 then () else error "rewrite.sml diff.result in rewriting";
97 "----- rewriting a subterm";
98 val tm = @{term "w*(x + y*z)::real"};
100 val SOME (r,_) = (rewrite_ thy dummy_ord e_rls false thm tm)
101 handle _ => error "rewrite.sml diff.behav. in rew_sub";
103 "----- ordered rewriting";
104 fun tord (_:subst) pp = Term_Ord.termless pp;
105 if tord [] (@{term "x + y*z::real"}, @{term "y*z + x::real"}) then ()
106 else error "rewrite.sml diff.behav. in ord.rewr.";
108 val NONE = (rewrite_ thy tord e_rls false thm tm)
109 handle _ => error "rewrite.sml diff.behav. in rewriting";
110 (*is displayed on _TOP_ of <response> buffer...*)
111 Pretty.writeln (Proof_Context.pretty_term_abbrev @{context} r);
113 val tm = @{term "x*y + z::real"};
114 val SOME (r,_) = (rewrite_ thy tord e_rls false thm tm)
115 handle _ => error "rewrite.sml diff.behav. in rewriting";
118 "----------- conditional rewriting without Isac's thys --";
119 "----------- conditional rewriting without Isac's thys --";
120 "----------- conditional rewriting without Isac's thys --";
122 "===== prepr cond.rew. with Pattern.match";
123 val thy = @{theory Complex_Main};
124 val ctxt = @{context};
125 val thm = @{thm nonzero_mult_divide_cancel_right};
126 val rule = Thm.prop_of thm;
127 val tm = @{term "x*2 / 2::real"};
129 val prem = Logic.strip_imp_prems rule;
130 val nps = Logic.count_prems rule;
131 val prems = Logic.strip_prems (nps, [], rule);
133 val eq = Logic.strip_imp_concl rule;
134 val (LHS, RHS) = (HOLogic.dest_eq o HOLogic.dest_Trueprop) eq;
136 val mtcs = Pattern.match thy (LHS, tm) (Vartab.empty, Vartab.empty);
137 val rule' = Envir.subst_term mtcs rule;
139 val prems' = (fst o Logic.strip_prems)
140 (Logic.count_prems rule', [], rule');
141 val RHS' = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop
142 o Logic.strip_imp_concl) rule';
144 "----- conditional rewriting creating an assumption";
145 "----- conditional rewriting creating an assumption";
146 val tm = @{term "x*y / y::real"};
147 val SOME (rew, asm) = (rewrite_ thy dummy_ord e_rls false thm tm)
148 handle _ => error "rewrite.sml diff.behav. in cond.rew.";
150 if rew = @{term "x::real"} then () (* the rewrite is _NO_ Trueprop *)
151 else error "rewrite.sml diff.result in cond.rew.";
153 if hd asm = @{term "~ y = (0::real)"} (* dropped Trueprop $ ...*)
154 then () else error "rewrite.sml diff.asm in cond.rew.";
155 "----- conditional rewriting immediately: can only be done with ";
156 "------Isabelle numerals, because erls cannot handle them yet.";
159 "----------- step through 'and rew_sub': ----------------";
160 "----------- step through 'and rew_sub': ----------------";
161 "----------- step through 'and rew_sub': ----------------";
162 (*and make asms without Trueprop, beginning with the result:*)
163 val tm = @{term "x*y / y::real"};
164 val (t', asm, _, _) = rew_sub thy 0 [] dummy_ord e_rls true [] (prop_of thm) tm;
165 (*show_types := false;*)
166 "----- evaluate arguments";
167 val (thy, i, bdv, tless, rls, put_asm, lrd, r, t) =
168 (thy, 0, [], dummy_ord, e_rls, true, [], (prop_of thm), tm);
169 "----- step 1: LHS, RHS of rule";
170 val (LHS, RHS) = (HOLogic.dest_eq o HOLogic.dest_Trueprop
171 o Logic.strip_imp_concl) r;
172 term2str r = "?b ~= (0::?'a) ==> ?a * ?b / ?b = ?a";
173 term2str LHS = "?a * ?b / ?b"; term2str RHS = "?a";
174 "----- step 2: the rule instantiated";
175 val r' = Envir.subst_term
176 (Pattern.match thy (LHS, t) (Vartab.empty, Vartab.empty)) r;
177 term2str r' = "y ~= 0 ==> x * y / y = x";
178 "----- step 3: get the (instantiated) assumption(s)";
179 val p' = (fst o Logic.strip_prems) (Logic.count_prems r', [], r');
180 term2str (hd p') = "y ~= 0";
181 "=====vvv make asms without Trueprop ---vvv";
182 val p' = map HOLogic.dest_Trueprop ((fst o Logic.strip_prems)
183 (Logic.count_prems r', [], r'));
185 [Const ("HOL.Not", _) $ (Const ("HOL.eq", _) $ Free ("y", _) $
186 Const ("Groups.zero_class.zero", _))] => ()
187 | _ => error "rewrite.sml assumption changed";
188 "=====^^^ make asms without Trueprop ---^^^";
189 "----- step 4: get the (instantiated) RHS";
190 val t' = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop
191 o Logic.strip_imp_concl) r';
194 "----------- step through 'fun rewrite_terms_' ---------";
195 "----------- step through 'fun rewrite_terms_' ---------";
196 "----------- step through 'fun rewrite_terms_' ---------";
197 "----- step 0: args for rewrite_terms_, local fun";
198 val (thy, ord, erls, equs, t) =
199 (@{theory "Biegelinie"}, dummy_ord, Erls, [str2term "x = 0"],
200 str2term "M_b x = -1 * q_0 * x ^^^ 2 / 2 + x * c + c_2");
201 "----- step 1: args for rew_";
202 val ((t', asm'), (rules as r::rs), t) = ((e_term, []), equs, t);
203 "----- step 2: rew_sub";
204 rew_sub thy 1 [] ord erls false [] (Trueprop $ r) t;
205 "----- step 3: step through rew_sub -- inefficient: goes into subterms";
208 val SOME (t', _) = rewrite_terms_ thy dummy_ord Erls equs t;
209 writeln "----------- rewrite_terms_ 1---------------------------";
210 if term2str t' = "M_b 0 = -1 * q_0 * 0 ^^^ 2 / 2 + 0 * c + c_2" then ()
211 else error "rewrite.sml rewrite_terms_ [x = 0]";
213 val equs = [str2term "M_b 0 = 0"];
214 val t = str2term "M_b 0 = -1 * q_0 * 0 ^^^ 2 / 2 + 0 * c + c_2";
215 val SOME (t', _) = rewrite_terms_ thy dummy_ord Erls equs t;
216 writeln "----------- rewrite_terms_ 2---------------------------";
217 if term2str t' = "0 = -1 * q_0 * 0 ^^^ 2 / 2 + 0 * c + c_2" then ()
218 else error "rewrite.sml rewrite_terms_ [M_b 0 = 0]";
220 val equs = [str2term "x = 0", str2term"M_b 0 = 0"];
221 val t = str2term "M_b x = -1 * q_0 * x ^^^ 2 / 2 + x * c + c_2";
222 val SOME (t', _) = rewrite_terms_ thy dummy_ord Erls equs t;
223 writeln "----------- rewrite_terms_ 3---------------------------";
224 if term2str t' = "0 = -1 * q_0 * 0 ^^^ 2 / 2 + 0 * c + c_2" then ()
225 else error "rewrite.sml rewrite_terms_ [x = 0, M_b 0 = 0]";
228 "----------- rewrite_inst_ bdvs -------------------------";
229 "----------- rewrite_inst_ bdvs -------------------------";
230 "----------- rewrite_inst_ bdvs -------------------------";
231 (*see smltest/Scripts/term_G.sml: inst_bdv 2*)
232 val t = str2term"-1 * (q_0 * L ^^^ 2) / 2 + (L * c_3 + c_4) = 0";
233 val bdvs = [(str2term"bdv_1",str2term"c"),
234 (str2term"bdv_2",str2term"c_2"),
235 (str2term"bdv_3",str2term"c_3"),
236 (str2term"bdv_4",str2term"c_4")];
237 (*------------ outcommented WN071210, after inclusion into ROOT.ML
239 rewrite_inst_ thy e_rew_ord
240 (append_rls "erls_isolate_bdvs" e_rls
241 [(Calc ("EqSystem.occur'_exactly'_in",
242 eval_occur_exactly_in
243 "#eval_occur_exactly_in_"))
245 false bdvs (num_str @{separate_bdvs_add) t;
246 (writeln o term2str) t;
247 if term2str t = "L * c_3 + c_4 = 0 + -1 * (-1 * (q_0 * L ^^^ 2) / 2)"
248 then () else error "rewrite.sml rewrite_inst_ bdvs";
250 trace_rewrite:=false;--------------------------------------------*)
253 "----------- check diff 2002--2009-3 --------------------";
254 "----------- check diff 2002--2009-3 --------------------";
255 "----------- check diff 2002--2009-3 --------------------";
256 (*----- 2002 -------------------------------------------------------------------
257 # rls: norm_Rational_noadd_fractions on: 1 / EI * (L * q_0 * x / 2 + -1 *
259 ## rls: discard_minus_ on: 1 / EI * (L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2
261 ### try thm: real_diff_minus
262 ### try thm: sym_real_mult_minus1
263 ## rls: rat_mult_poly on: 1 / EI * (L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2
265 ### try thm: rat_mult_poly_l
266 ### try thm: rat_mult_poly_r
267 #### eval asms: L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2 is_polyexp
268 ==> 1 / EI * (L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2) =
269 1 * (L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2) / EI
270 ##### rls: e_rls-is_polyexp on: L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2
272 ###### try calc: Poly.is'_polyexp'
273 ====== calc. to: False
274 ###### try calc: Poly.is'_polyexp'
275 ###### try calc: Poly.is'_polyexp'
276 #### asms false: ["L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2 is_polyexp"]
277 ----- 2002 NONE rewrite --------------------------------------------------------
278 ----- 2009 should maintain this behaviour, but: --------------------------------
279 # rls: norm_Rational_noadd_fractions on: 1 / EI * (L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2)
280 ## rls: discard_minus on: 1 / EI * (L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2)
281 ### try thm: real_diff_minus
282 ### try thm: sym_real_mult_minus1
283 ## rls: rat_mult_poly on: 1 / EI * (L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2)
284 ### try thm: rat_mult_poly_l
285 ### try thm: rat_mult_poly_r
286 #### eval asms: L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2 is_polyexp
287 ==> 1 / EI * (L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2) =
288 1 * (L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2) / EI
289 ##### rls: e_rls-is_polyexp on: L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2 is_polyexp
290 ###### try calc: Poly.is'_polyexp'
291 ====== calc. to: False
292 ###### try calc: Poly.is'_polyexp'
293 ###### try calc: Poly.is'_polyexp'
294 #### asms accepted: ["L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2 is_polyexp"] stored: ["False"]
295 === rewrites to: 1 * (L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2) / EI
296 ----- 2009 -------------------------------------------------------------------*)
298 (*the situation as was before repair (asm without Trueprop) is outcommented*)
299 val thy = @{theory "Isac"};
300 "===== example which raised the problem =================";
301 val t = @{term "1 / EI * (L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2)"};
302 "----- rewrite_set_inst_ norm_Rational_noadd_fractions--";
303 val subs = [(str2term "bdv", str2term "x")];
304 val rls = norm_Rational_noadd_fractions;
305 val NONE (*SOME (t', _)*) = rewrite_set_inst_ thy true subs rls t;
306 "----- rewrite_ rat_mult_poly_r--------------------------";
307 val thm = @{thm rat_mult_poly_r};
308 "?c::real is_polyexp ==> (?a::real) / (?b::real) * ?c = ?a * ?c / ?b";
309 val erls = append_rls "e_rls-is_polyexp" e_rls
310 [Calc ("Poly.is'_polyexp", eval_is_polyexp "")];
311 val NONE (*SOME (t'', _)*) = rewrite_ thy dummy_ord erls true thm t;
312 (*t' = t''; (*false because of further rewrites in t'*)*)
313 "----- rew_sub --------------------------------";
314 val (t''', _, _, _) = rew_sub thy 0 [] dummy_ord erls true [] (prop_of thm) t;
315 (*t'' = t'''; (*true*)*)
316 "----- rewrite_set_ erls --------------------------------";
317 val cond = @{term "(L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2)"};
318 val NONE = rewrite_set_ thy true erls cond;
319 (* ^^^^^ goes with '====== calc. to: False' above from beginning*)
321 writeln "===== maximally simplified example =====================";
322 val t = @{term "a / b * (x / x ^^^ 2)"};
323 "?c::real is_polyexp ==> (?a::real) / (?b::real) * ?c = ?a * ?c / ?b";
324 writeln "----- rewrite_set_inst_ norm_Rational_noadd_fractions--";
325 val (*NONE*) SOME (t', asm) = rewrite_set_inst_ thy true subs rls t;
326 term2str t' = "a * x / (b * x ^^^ 2)"; (*rew. by thm outside test case*)
327 (*checked visually: trace_rewrite looks like above for 2009*)
329 writeln "----- rewrite_ rat_mult_poly_r--------------------------";
330 val NONE (*SOME (t'', _)*) = rewrite_ thy dummy_ord erls true thm t;
331 (*t' = t''; (*false because of further rewrites in t'*)*)
332 writeln "----- rew_sub --------------------------------";
333 val (t''', _, _, _) = rew_sub thy 0 [] dummy_ord erls true [] (prop_of thm) t;
334 (*t'' = t'''; (*true*)*)
335 writeln "----- rewrite_set_ erls --------------------------------";
336 val cond = @{term "(x / x ^^^ 2)"};
337 val NONE = rewrite_set_ thy true erls cond;
338 (* ^^^^^ goes with '====== calc. to: False' above from beginning*)
341 "----------- compare all prepat's existing 2010 ---------";
342 "----------- compare all prepat's existing 2010 ---------";
343 "----------- compare all prepat's existing 2010 ---------";
344 val thy = @{theory "Isac"};
345 val t = @{term "a + b * x = (0 ::real)"};
346 val pat = parse_patt thy "?l = (?r ::real)";
347 val precond = parse_patt thy "is_polynomial (?l::real)";(*no infix def*)
348 val precond = parse_patt thy "(?l::real) is_expanded";
350 val inst = Pattern.match thy (pat, t) (Vartab.empty, Vartab.empty);
351 val preinst = Envir.subst_term inst precond;
354 "===== Rational.thy: cancel ===";
355 (* pat matched with the current term gives an environment
356 (or not: hen the Rrls not applied);
357 if pre1 and pre2 evaluate to @{term True} in this environment,
358 then the Rrls is applied. *)
359 val t = str2term "(a + b) / c ::real";
360 val pat = parse_patt thy "?r / ?s ::real";
361 val pres = [parse_patt thy "?r is_expanded", parse_patt thy "?s is_expanded"];
362 val prepat = [(pres, pat)];
363 val erls = rational_erls;
364 (* erls got from Rrls {erls, prepat, scr = Rfuns {normal_form, ...}, ...} *)
366 val subst = Pattern.match thy (pat, t) (Vartab.empty, Vartab.empty);
367 val asms = map (Envir.subst_term subst) pres;
368 if terms2str asms = "[\"a + b is_expanded\",\"c is_expanded\"]"
369 then () else error "rewrite.sml: prepat cancel subst";
370 if ([], true) = eval__true thy 0 asms [] erls
371 then () else error "rewrite.sml: prepat cancel eval__true";
373 "===== Rational.thy: add_fractions_p ===";
374 (* if each pat* matches with the current term, the Rrls is applied
375 (there are no preconditions to be checked, they are @{term True}) *)
376 val t = str2term "a / b + 1 / 2";
377 val pat = parse_patt thy "?r / ?s + ?u / ?v";
378 val pres = [@{term True}];
379 val prepat = [(pres, pat)];
380 val erls = rational_erls;
381 (* erls got from Rrls {erls, prepat, scr = Rfuns {normal_form, ...}, ...} *)
383 val subst = Pattern.match thy (pat, t) (Vartab.empty, Vartab.empty);
384 if ([], true) = eval__true thy 0 (map (Envir.subst_term subst) pres) [] erls
385 then () else error "rewrite.sml: prepat add_fractions_p";
387 "===== Poly.thy: order_mult_ ===";
388 (* ?p matched with the current term gives an environment,
389 which evaluates (the instantiated) "p is_multUnordered" to true*)
390 val t = str2term "x^^^2 * x";
391 val pat = parse_patt thy "?p :: real"
392 val pres = [parse_patt thy "?p is_multUnordered"];
393 val prepat = [(pres, pat)];
394 val erls = append_rls "e_rls-is_multUnordered" e_rls
395 [Calc ("Poly.is'_multUnordered",
396 eval_is_multUnordered "")];
398 val subst = Pattern.match thy (pat, t) (Vartab.empty, Vartab.empty);
399 val asms = map (Envir.subst_term subst) pres;
400 if terms2str asms = "[\"x ^^^ 2 * x is_multUnordered\"]"
401 then () else error "rewrite.sml: prepat order_mult_ subst";
402 if ([], true) = eval__true thy 0 asms [] erls
403 then () else error "rewrite.sml: prepat order_mult_ eval__true";
406 "----------- fun app_rev, Rrls, -------------------------";
407 "----------- fun app_rev, Rrls, -------------------------";
408 "----------- fun app_rev, Rrls, -------------------------";
409 val t = str2term "x^^^2 * x";
411 if is_multUnordered t then () else error "rewrite.sml diff. is_multUnordered 2";
412 val tm = str2term "(x^^^2 * x) is_multUnordered";
413 eval_is_multUnordered "testid" "" tm thy;
415 case eval_is_multUnordered "testid" "" tm thy of
416 SOME (_, Const ("HOL.Trueprop", _) $
417 (Const ("HOL.eq", _) $
418 (Const ("Poly.is'_multUnordered", _) $ _) $
419 Const ("HOL.True", _))) => ()
420 | _ => error "rewrite.sml diff. eval_is_multUnordered 2b";
422 tracing "----- begin rewrite x^^^2 * x ---"; trace_rewrite := true;
423 val SOME (t', _) = rewrite_set_ thy true order_mult_ t;
424 tracing "----- end rewrite x^^^2 * x ---"; trace_rewrite := false;
425 if term2str t' = "x * x ^^^ 2" then ()
426 else error "rewrite.sml Poly.is'_multUnordered doesn't work";
428 (* for achieving the previous result, the following code was taken apart *)
429 "----- rewrite__set_ ---";
430 val (thy, i, _, _, (rrls as Rrls _), t) = (thy, 0, true, [], order_mult_, tm);
431 val (t', asm, rew) = app_rev thy (i+1) rrls t;
433 val (thy, i, rrls, t) = (thy, (i+1), rrls, t);
434 fun chk_prepat thy erls [] t = true
435 | chk_prepat thy erls prepat t =
436 let fun chk (pres, pat) =
437 (let val subst: Type.tyenv * Envir.tenv =
438 Pattern.match thy (pat, t)
439 (Vartab.empty, Vartab.empty)
440 in snd (eval__true thy (i+1)
441 (map (Envir.subst_term subst) pres)
445 fun scan_ f [] = false (*scan_ NEVER called by []*)
446 | scan_ f (pp::pps) = if f pp then true
448 in scan_ chk prepat end;
450 (*.apply the normal_form of a rev-set.*)
451 fun app_rev' thy (Rrls{erls,prepat,scr=Rfuns{normal_form,...},...}) t =
452 if chk_prepat thy erls prepat t
453 then ((*tracing("### app_rev': t = "^(term2str t));*)
456 (*fixme val NONE = app_rev' thy rrls t;*)
457 "----- app_rev' ---";
458 val (thy, Rrls{erls,prepat,scr=Rfuns{normal_form,...},...}, t) = (thy, rrls, t);
459 (*fixme false*) chk_prepat thy erls prepat t;
460 "----- chk_prepat ---";
461 val (thy, erls, prepat, t) = (thy, erls, prepat, t);
462 fun chk (pres, pat) =
463 (let val subst: Type.tyenv * Envir.tenv =
464 Pattern.match thy (pat, t)
465 (Vartab.empty, Vartab.empty)
466 in snd (eval__true thy (i+1)
467 (map (Envir.subst_term subst) pres)
471 fun scan_ f [] = false (*scan_ NEVER called by []*)
472 | scan_ f (pp::pps) = if f pp then true
474 tracing "=== poly.sml: scan_ chk prepat begin";
476 tracing "=== poly.sml: scan_ chk prepat end";
479 (*reestablish...*) val t = str2term "x ^^^ 2 * x";
480 val [(pres, pat)] = prepat;
481 val subst: Type.tyenv * Envir.tenv =
482 Pattern.match thy (pat, t)
483 (Vartab.empty, Vartab.empty);
485 (*fixme: asms = ["p is_multUnordered"]...instantiate*)
486 "----- eval__true ---";
487 val asms = (map (Envir.subst_term subst) pres);
488 if terms2str asms = "[\"x ^^^ 2 * x is_multUnordered\"]" then ()
489 else error "rewrite.sml: diff. is_multUnordered, asms";
490 val (thy, i, asms, bdv, rls) =
491 (thy, (i+1), [str2term "(x^^^2 * x) is_multUnordered"],
492 [] : (term * term) list, erls);
493 case eval__true thy i asms bdv rls of
495 | _ => error "rewrite.sml: diff. is_multUnordered, eval__true";
497 "----------- 2011 thms with axclasses -------------------";
498 "----------- 2011 thms with axclasses -------------------";
499 "----------- 2011 thms with axclasses -------------------";
500 val thm = num_str @{thm divide_1};
501 val prop = prop_of thm;
502 atomty prop; (*Type 'a*)
503 val t = str2term "(2*x)/1"; (*Type real*)
505 val (thy, ro, er, inst) =
506 (@{theory "Isac"}, tless_true, eval_rls, [(@{term "bdv::real"}, @{term "x::real"})]);
507 val SOME (t, _) = rewrite_ thy ro er true thm t; (*real matches 'a ?via ring? etc*)
509 "----------- repair NO asms from rls RatEq_eliminate ----";
510 "----------- repair NO asms from rls RatEq_eliminate ----";
511 "----------- repair NO asms from rls RatEq_eliminate ----";
512 val t = str2term "1 / x = 5";
513 trace_rewrite := true;
514 val SOME (t', asm) = rewrite_ thy e_rew_ord e_rls true @{thm rat_mult_denominator_right} t;
515 term2str t' = "1 = 5 * x";
516 terms2str asm = "[\"x ~= 0\"]";
518 ## eval asms: x ~= 0 ==> (1 / x = 5) = (1 = 5 * x)
519 ### rls: e_rls on: x ~= 0
520 ## asms accepted: ["x ~= 0"] stored: ["x ~= 0"]
522 trace_rewrite := false;
524 trace_rewrite := false;
525 val SOME (t', []) = rewrite_set_ thy true RatEq_eliminate t; (*= [] must be = "x ~= 0"*)
526 term2str t' = "1 = 5 * x";
529 #### rls: rateq_erls on: x ~= 0
531 ##### try calc: HOL.eq' <<<------------------------------- here the error comes from
532 ===== calc. to: ~ False
533 ##### try calc: HOL.eq'
534 ##### try thm: not_true
535 ##### try thm: not_false
536 ===== rewrites to: True
538 ### asms accepted: ["x ~= 0"] stored: []
541 trace_rewrite := false;
542 (* WN120317.TODO dropped rateq: the above error is the same in 2002 *)