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 "----------- fun app_rev, Rrls, prepat ------------------";
21 "--------------------------------------------------------";
22 "--------------------------------------------------------";
23 "--------------------------------------------------------";
25 (*-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.
27 "----------- assemble rewrite ---------------------------";
28 "----------- assemble rewrite ---------------------------";
29 "----------- assemble rewrite ---------------------------";
30 "===== rewriting by thm with 'a";
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 val (lhs,rhs) = (dest_equals' o strip_trueprop
41 o Logic.strip_imp_concl) r;
43 val insts = Pattern.match thy (lhs,t) (Vartab.empty, Vartab.empty);*)
44 "----- fun match_rew in Pure/pattern.ML";
45 val rtm = the_default rhs (Term.rename_abs lhs t rhs);
47 writeln(Syntax.string_of_term ctxt rtm);
48 writeln(Syntax.string_of_term ctxt lhs);
49 writeln(Syntax.string_of_term ctxt t);
51 (Pattern.match thy (lhs, t) (Vartab.empty, Vartab.empty));
52 val (rew, rhs) = (Envir.subst_term
53 (Pattern.match thy (lhs, t) (Vartab.empty, Vartab.empty)) rtm, rtm);
54 (*lookup in isabelle?trace?response...*)
55 writeln(Syntax.string_of_term ctxt rew);
56 writeln(Syntax.string_of_term ctxt rhs);
58 "===== rewriting: prep insertion into rew_sub";
59 val thy = @{theory Complex_Main};
60 val ctxt = @{context};
61 val thm = @{thm nonzero_mult_divide_cancel_right};
62 val r = Thm.prop_of thm;
63 val tm = @{term "x*2 / 2::real"};
65 val (lhs, rhs) = (HOLogic.dest_eq o HOLogic.dest_Trueprop
66 o Logic.strip_imp_concl) r;
67 val r' = Envir.subst_term (Pattern.match thy (lhs, tm)
68 (Vartab.empty, Vartab.empty)) r;
69 val p' = (fst o Logic.strip_prems) (Logic.count_prems r', [], r');
70 val t' = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop
71 o Logic.strip_imp_concl) r';
73 (*is displayed on top of <response> buffer...*)
74 Pretty.writeln (ProofContext.pretty_term_abbrev @{context} r');
75 Pretty.writeln (ProofContext.pretty_term_abbrev @{context} t');
78 "----------- test rewriting without Isac's thys ---------";
79 "----------- test rewriting without Isac's thys ---------";
80 "----------- test rewriting without Isac's thys ---------";
82 "===== rewriting with Isabelle2009-1 only, i.e without isac-hacks";
83 val thy = @{theory Complex_Main};
84 val ctxt = @{context};
85 val thm = @{thm add_commute};
86 val tm = @{term "x + y*z::real"};
88 val SOME (r,_) = (rewrite_ thy dummy_ord e_rls false thm tm)
89 handle _ => error "rewrite.sml diff.behav. in rewriting";
90 (*is displayed on _TOP_ of <response> buffer...*)
91 Pretty.writeln (ProofContext.pretty_term_abbrev @{context} r);
92 if r = @{term "y*z + x::real"}
93 then () else error "rewrite.sml diff.result in rewriting";
95 "----- rewriting a subterm";
96 val tm = @{term "w*(x + y*z)::real"};
98 val SOME (r,_) = (rewrite_ thy dummy_ord e_rls false thm tm)
99 handle _ => error "rewrite.sml diff.behav. in rew_sub";
101 "----- ordered rewriting";
102 fun tord (_:subst) pp = Term_Ord.termless pp;
103 if tord [] (@{term "x + y*z::real"}, @{term "y*z + x::real"}) then ()
104 else error "rewrite.sml diff.behav. in ord.rewr.";
106 val NONE = (rewrite_ thy tord e_rls false thm tm)
107 handle _ => error "rewrite.sml diff.behav. in rewriting";
108 (*is displayed on _TOP_ of <response> buffer...*)
109 Pretty.writeln (ProofContext.pretty_term_abbrev @{context} r);
111 val tm = @{term "x*y + z::real"};
112 val SOME (r,_) = (rewrite_ thy tord e_rls false thm tm)
113 handle _ => error "rewrite.sml diff.behav. in rewriting";
116 "----------- conditional rewriting without Isac's thys --";
117 "----------- conditional rewriting without Isac's thys --";
118 "----------- conditional rewriting without Isac's thys --";
120 "===== prepr cond.rew. with Pattern.match";
121 val thy = @{theory Complex_Main};
122 val ctxt = @{context};
123 val thm = @{thm nonzero_mult_divide_cancel_right};
124 val rule = Thm.prop_of thm;
125 val tm = @{term "x*2 / 2::real"};
127 val prem = Logic.strip_imp_prems rule;
128 val nps = Logic.count_prems rule;
129 val prems = Logic.strip_prems (nps, [], rule);
131 val eq = Logic.strip_imp_concl rule;
132 val (lhs, rhs) = (HOLogic.dest_eq o HOLogic.dest_Trueprop) eq;
134 val mtcs = Pattern.match thy (lhs, tm) (Vartab.empty, Vartab.empty);
135 val rule' = Envir.subst_term mtcs rule;
137 val prems' = (fst o Logic.strip_prems)
138 (Logic.count_prems rule', [], rule');
139 val rhs' = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop
140 o Logic.strip_imp_concl) rule';
142 "----- conditional rewriting creating an assumption";
143 "----- conditional rewriting creating an assumption";
144 val tm = @{term "x*y / y::real"};
145 val SOME (rew, asm) = (rewrite_ thy dummy_ord e_rls false thm tm)
146 handle _ => error "rewrite.sml diff.behav. in cond.rew.";
148 if rew = @{term "x::real"} then () (* the rewrite is _NO_ Trueprop *)
149 else error "rewrite.sml diff.result in cond.rew.";
151 if hd asm = @{term "~ y = (0::real)"} (* dropped Trueprop $ ...*)
152 then () else error "rewrite.sml diff.asm in cond.rew.";
153 "----- conditional rewriting immediately: can only be done with ";
154 "------Isabelle numerals, because erls cannot handle them yet.";
157 "----------- step through 'and rew_sub': ----------------";
158 "----------- step through 'and rew_sub': ----------------";
159 "----------- step through 'and rew_sub': ----------------";
160 (*and make asms without Trueprop, beginning with the result:*)
161 val tm = @{term "x*y / y::real"};
162 val (t', asm, _, _) = rew_sub thy 0 [] dummy_ord e_rls true [] (prop_of thm) tm;
164 "----- evaluate arguments";
165 val (thy, i, bdv, tless, rls, put_asm, lrd, r, t) =
166 (thy, 0, [], dummy_ord, e_rls, true, [], (prop_of thm), tm);
167 "----- step 1: lhs, rhs of rule";
168 val (lhs, rhs) = (HOLogic.dest_eq o HOLogic.dest_Trueprop
169 o Logic.strip_imp_concl) r;
170 term2str r = "?b ~= (0::?'a) ==> ?a * ?b / ?b = ?a";
171 term2str lhs = "?a * ?b / ?b"; term2str rhs = "?a";
172 "----- step 2: the rule instantiated";
173 val r' = Envir.subst_term
174 (Pattern.match thy (lhs, t) (Vartab.empty, Vartab.empty)) r;
175 term2str r' = "y ~= 0 ==> x * y / y = x";
176 "----- step 3: get the (instantiated) assumption(s)";
177 val p' = (fst o Logic.strip_prems) (Logic.count_prems r', [], r');
178 term2str (hd p') = "y ~= 0";
179 "=====vvv make asms without Trueprop ---vvv";
180 val p' = map HOLogic.dest_Trueprop ((fst o Logic.strip_prems)
181 (Logic.count_prems r', [], r'));
183 [Const ("Not", _) $ (Const ("op =", _) $ Free ("y", _) $
184 Const ("Groups.zero_class.zero", _))] => ()
185 | _ => error "rewrite.sml assumption changed";
186 "=====^^^ make asms without Trueprop ---^^^";
187 "----- step 4: get the (instantiated) rhs";
188 val t' = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop
189 o Logic.strip_imp_concl) r';
192 "----------- step through 'fun rewrite_terms_' ---------";
193 "----------- step through 'fun rewrite_terms_' ---------";
194 "----------- step through 'fun rewrite_terms_' ---------";
195 "----- step 0: args for rewrite_terms_, local fun";
196 val (thy, ord, erls, equs, t) =
197 (theory "Biegelinie", dummy_ord, Erls, [str2term "x = 0"],
198 str2term "M_b x = -1 * q_0 * x ^^^ 2 / 2 + x * c + c_2");
199 "----- step 1: args for rew_";
200 val ((t', asm'), (rules as r::rs), t) = ((e_term, []), equs, t);
201 "----- step 2: rew_sub";
202 rew_sub thy 1 [] ord erls false [] (Trueprop $ r) t;
203 "----- step 3: step through rew_sub -- inefficient: goes into subterms";
206 val SOME (t', _) = rewrite_terms_ thy dummy_ord Erls equs t;
207 writeln "----------- rewrite_terms_ 1---------------------------";
208 if term2str t' = "M_b 0 = -1 * q_0 * 0 ^^^ 2 / 2 + 0 * c + c_2" then ()
209 else error "rewrite.sml rewrite_terms_ [x = 0]";
211 val equs = [str2term "M_b 0 = 0"];
212 val t = str2term "M_b 0 = -1 * q_0 * 0 ^^^ 2 / 2 + 0 * c + c_2";
213 val SOME (t', _) = rewrite_terms_ thy dummy_ord Erls equs t;
214 writeln "----------- rewrite_terms_ 2---------------------------";
215 if term2str t' = "0 = -1 * q_0 * 0 ^^^ 2 / 2 + 0 * c + c_2" then ()
216 else error "rewrite.sml rewrite_terms_ [M_b 0 = 0]";
218 val equs = [str2term "x = 0", str2term"M_b 0 = 0"];
219 val t = str2term "M_b x = -1 * q_0 * x ^^^ 2 / 2 + x * c + c_2";
220 val SOME (t', _) = rewrite_terms_ thy dummy_ord Erls equs t;
221 writeln "----------- rewrite_terms_ 3---------------------------";
222 if term2str t' = "0 = -1 * q_0 * 0 ^^^ 2 / 2 + 0 * c + c_2" then ()
223 else error "rewrite.sml rewrite_terms_ [x = 0, M_b 0 = 0]";
226 "----------- rewrite_inst_ bdvs -------------------------";
227 "----------- rewrite_inst_ bdvs -------------------------";
228 "----------- rewrite_inst_ bdvs -------------------------";
229 (*see smltest/Scripts/term_G.sml: inst_bdv 2*)
230 val t = str2term"-1 * (q_0 * L ^^^ 2) / 2 + (L * c_3 + c_4) = 0";
231 val bdvs = [(str2term"bdv_1",str2term"c"),
232 (str2term"bdv_2",str2term"c_2"),
233 (str2term"bdv_3",str2term"c_3"),
234 (str2term"bdv_4",str2term"c_4")];
235 (*------------ outcommented WN071210, after inclusion into ROOT.ML
237 rewrite_inst_ thy e_rew_ord
238 (append_rls "erls_isolate_bdvs" e_rls
239 [(Calc ("EqSystem.occur'_exactly'_in",
240 eval_occur_exactly_in
241 "#eval_occur_exactly_in_"))
243 false bdvs (num_str @{separate_bdvs_add) t;
244 (writeln o term2str) t;
245 if term2str t = "L * c_3 + c_4 = 0 + -1 * (-1 * (q_0 * L ^^^ 2) / 2)"
246 then () else error "rewrite.sml rewrite_inst_ bdvs";
248 trace_rewrite:=false;--------------------------------------------*)
251 "----------- check diff 2002--2009-3 --------------------";
252 "----------- check diff 2002--2009-3 --------------------";
253 "----------- check diff 2002--2009-3 --------------------";
254 (*----- 2002 -------------------------------------------------------------------
255 # rls: norm_Rational_noadd_fractions on: 1 / EI * (L * q_0 * x / 2 + -1 *
257 ## rls: discard_minus_ on: 1 / EI * (L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2
259 ### try thm: real_diff_minus
260 ### try thm: sym_real_mult_minus1
261 ## rls: rat_mult_poly on: 1 / EI * (L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2
263 ### try thm: rat_mult_poly_l
264 ### try thm: rat_mult_poly_r
265 #### eval asms: L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2 is_polyexp
266 ==> 1 / EI * (L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2) =
267 1 * (L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2) / EI
268 ##### rls: e_rls-is_polyexp on: L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2
270 ###### try calc: Poly.is'_polyexp'
271 ====== calc. to: False
272 ###### try calc: Poly.is'_polyexp'
273 ###### try calc: Poly.is'_polyexp'
274 #### asms false: ["L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2 is_polyexp"]
275 ----- 2002 NONE rewrite --------------------------------------------------------
276 ----- 2009 should maintain this behaviour, but: --------------------------------
277 # rls: norm_Rational_noadd_fractions on: 1 / EI * (L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2)
278 ## rls: discard_minus on: 1 / EI * (L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2)
279 ### try thm: real_diff_minus
280 ### try thm: sym_real_mult_minus1
281 ## rls: rat_mult_poly on: 1 / EI * (L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2)
282 ### try thm: rat_mult_poly_l
283 ### try thm: rat_mult_poly_r
284 #### eval asms: L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2 is_polyexp
285 ==> 1 / EI * (L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2) =
286 1 * (L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2) / EI
287 ##### rls: e_rls-is_polyexp on: L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2 is_polyexp
288 ###### try calc: Poly.is'_polyexp'
289 ====== calc. to: False
290 ###### try calc: Poly.is'_polyexp'
291 ###### try calc: Poly.is'_polyexp'
292 #### asms accepted: ["L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2 is_polyexp"] stored: ["False"]
293 === rewrites to: 1 * (L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2) / EI
294 ----- 2009 -------------------------------------------------------------------*)
296 (*the situation as was before repair (asm without Trueprop) is outcommented*)
297 val thy = theory "Isac";
298 "===== example which raised the problem =================";
299 val t = @{term "1 / EI * (L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2)"};
300 "----- rewrite_set_inst_ norm_Rational_noadd_fractions--";
301 val subs = [(str2term "bdv", str2term "x")];
302 val rls = norm_Rational_noadd_fractions;
303 val NONE (*SOME (t', _)*) = rewrite_set_inst_ thy true subs rls t;
304 "----- rewrite_ rat_mult_poly_r--------------------------";
305 val thm = @{thm rat_mult_poly_r};
306 "?c::real is_polyexp ==> (?a::real) / (?b::real) * ?c = ?a * ?c / ?b";
307 val erls = append_rls "e_rls-is_polyexp" e_rls
308 [Calc ("Poly.is'_polyexp", eval_is_polyexp "")];
309 val NONE (*SOME (t'', _)*) = rewrite_ thy dummy_ord erls true thm t;
310 (*t' = t''; (*false because of further rewrites in t'*)*)
311 "----- rew_sub --------------------------------";
312 val (t''', _, _, _) = rew_sub thy 0 [] dummy_ord erls true [] (prop_of thm) t;
313 (*t'' = t'''; (*true*)*)
314 "----- rewrite_set_ erls --------------------------------";
315 val cond = @{term "(L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2)"};
316 val NONE = rewrite_set_ thy true erls cond;
317 (* ^^^^^ goes with '====== calc. to: False' above from beginning*)
319 writeln "===== maximally simplified example =====================";
320 val t = @{term "a / b * (x / x ^^^ 2)"};
321 "?c::real is_polyexp ==> (?a::real) / (?b::real) * ?c = ?a * ?c / ?b";
322 writeln "----- rewrite_set_inst_ norm_Rational_noadd_fractions--";
323 val (*NONE*) SOME (t', asm) = rewrite_set_inst_ thy true subs rls t;
324 term2str t' = "a * x / (b * x ^^^ 2)"; (*rew. by thm outside test case*)
325 (*checked visually: trace_rewrite looks like above for 2009*)
327 trace_rewrite := false; (*<<<<<<<<<<<<<<<<<<<<<###############################*)
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*)
339 trace_rewrite := false; (*<<<<<<<<<<<<<<<<<<<<<###############################*)
340 "--------------------------------------------------------";
342 -.-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.*)
344 "----------- fun app_rev, Rrls, prepat ------------------";
345 "----------- fun app_rev, Rrls, prepat ------------------";
346 "----------- fun app_rev, Rrls, prepat ------------------";
347 (* Christian Urban, 101001
354 val parser = Args.context -- Scan.lift Args.name_source
355 fun term_pat (ctxt, str) = str |> ProofContext.read_term_pattern ctxt
356 |> ML_Syntax.print_term |> ML_Syntax.atomic
358 ML_Antiquote.inline "term_pat" (parser >> term_pat)
363 val t = @{term "a + b * x = (0 ::real)"};
364 val pat = @{term_pat "?l = (?r ::real)"};
365 val precond = @{term_pat "is_polynomial (?l::real)"};
366 val inst = Pattern.match @{theory} (pat, t) (Vartab.empty, Vartab.empty);
370 Envir.subst_term inst precond
371 |> Syntax.string_of_term @{context}
375 val t = @{term "a + b * x = (0 ::real)"};
376 val pat = parse_patt thy "?l = (?r ::real)";
377 val precond = parse_patt thy "is_polynomial (?l::real)";(*no infix def*)
378 val precond = parse_patt thy " (?l::real) is_expanded";
380 val inst = Pattern.match thy (pat, t) (Vartab.empty, Vartab.empty);
381 val preinst = Envir.subst_term inst precond;
384 "===== Rational.thy: cancel ===";
385 (* pat matched with the current term gives an environment
386 (or not: hen the Rrls not applied);
387 if pre1 and pre2 evaluate to HOLogic.true_const in this environment,
388 then the Rrls is applied. *)
389 val t = str2term "(a + b) / c ::real";
390 val pat = parse_patt thy "?r / ?s ::real";
391 val pres = [parse_patt thy "?r is_expanded", parse_patt thy "?s is_expanded"];
392 val prepat = [(pres, pat)];
393 val erls = rational_erls;
394 (* erls got from Rrls {erls, prepat, scr = Rfuns {normal_form, ...}, ...} *)
396 val subst = Pattern.match thy (pat, t) (Vartab.empty, Vartab.empty);
397 val asms = map (Envir.subst_term subst) pres;
398 if terms2str asms = "[\"a + b is_expanded\",\"c is_expanded\"]"
399 then () else error "rewrite.sml: prepat cancel subst";
400 if ([], true) = eval__true thy 0 asms [] erls
401 then () else error "rewrite.sml: prepat cancel eval__true";
403 "===== Rational.thy: common_nominator_p ===";
404 (* if each pat* matches with the current term, the Rrls is applied
405 (there are no preconditions to be checked, they are HOLogic.true_const) *)
406 val t = str2term "a / b + 1 / 2";
407 val pat = parse_patt thy "?r / ?s + ?u / ?v";
408 val pres = [HOLogic.true_const];
409 val prepat = [(pres, pat)];
410 val erls = rational_erls;
411 (* erls got from Rrls {erls, prepat, scr = Rfuns {normal_form, ...}, ...} *)
413 val subst = Pattern.match thy (pat, t) (Vartab.empty, Vartab.empty);
414 if ([], true) = eval__true thy 0 (map (Envir.subst_term subst) pres) [] erls
415 then () else error "rewrite.sml: prepat common_nominator_p";
417 "===== Poly.thy: order_mult_ ===";
418 (* ?p matched with the current term gives an environment,
419 which evaluates (the instantiated) "p is_multUnordered" to true*)
420 val t = str2term "x^^^2 * x";
421 val pat = parse_patt thy "?p :: real"
422 val pres = [parse_patt thy "?p is_multUnordered"];
423 val prepat = [(pres, pat)];
424 val erls = append_rls "e_rls-is_multUnordered" e_rls
425 [Calc ("Poly.is'_multUnordered",
426 eval_is_multUnordered "")];
428 val subst = Pattern.match thy (pat, t) (Vartab.empty, Vartab.empty);
429 val asms = map (Envir.subst_term subst) pres;
430 if terms2str asms = "[\"x ^^^ 2 * x is_multUnordered\"]"
431 then () else error "rewrite.sml: prepat order_mult_ subst";
432 if ([], true) = eval__true thy 0 asms [] erls
433 then () else error "rewrite.sml: prepat order_mult_ eval__true";
436 (*========== inhibit exn =======================================================
437 ============ inhibit exn =====================================================*)
439 (*-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.
440 -.-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.*)