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 session --------";
15 "----------- conditional rewriting without Isac session -";
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 "----------- fun assoc_thm' -----------------------------";
25 "----------- fun rewrite_ down to Pattern.match ------------------------------------------------";
26 "----------- fun mk_thm ------------------------------------------------------------------------";
27 "----------- fun rewrite_set_ .. norm_equation -------------------------------------------------";
28 "--------------------------------------------------------";
29 "--------------------------------------------------------";
30 "--------------------------------------------------------";
33 "----------- assemble rewrite ---------------------------";
34 "----------- assemble rewrite ---------------------------";
35 "----------- assemble rewrite ---------------------------";
36 "===== rewriting by thm with 'a";
37 (*show_types := true;*)
39 val thy = @{theory Complex_Main};
40 val ctxt = @{context};
41 val thm = @{thm add.commute};
42 val t = (Thm.term_of o the) (parse thy "((r + u) + t) + s");
43 "----- from old: fun rewrite__";
45 val r = (((inst_bdv bdv) o norm o #prop o Thm.rep_thm) thm);
46 "----- from old: and rew_sub";
47 val (LHS,RHS) = (dest_equals o strip_trueprop
48 o Logic.strip_imp_concl) r;
50 val insts = Pattern.match thy (LHS,t) (Vartab.empty, Vartab.empty);*)
51 "----- fun match_rew in Pure/pattern.ML";
52 val rtm = the_default RHS (Term.rename_abs LHS t RHS);
54 writeln(Syntax.string_of_term ctxt rtm);
55 writeln(Syntax.string_of_term ctxt LHS);
56 writeln(Syntax.string_of_term ctxt t);
58 (Pattern.match thy (LHS, t) (Vartab.empty, Vartab.empty));
59 val (rew, RHS) = (Envir.subst_term
60 (Pattern.match thy (LHS, t) (Vartab.empty, Vartab.empty)) rtm, rtm);
61 (*lookup in isabelle?trace?response...*)
62 writeln(Syntax.string_of_term ctxt rew);
63 writeln(Syntax.string_of_term ctxt RHS);
64 "===== rewriting: prep insertion into rew_sub";
65 val thy = @{theory Complex_Main};
66 val ctxt = @{context};
67 val thm = @{thm nonzero_divide_mult_cancel_right};
68 val r = Thm.prop_of thm;
69 val tm = @{term "x / (2 * x)::real"};
71 val (LHS, RHS) = (HOLogic.dest_eq o HOLogic.dest_Trueprop
72 o Logic.strip_imp_concl) r;
73 val r' = Envir.subst_term (Pattern.match thy (LHS, tm)
74 (Vartab.empty, Vartab.empty)) r;
75 val p' = (fst o Logic.strip_prems) (Logic.count_prems r', [], r');
76 val t' = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop
77 o Logic.strip_imp_concl) r';
79 (*is displayed on top of <response> buffer...*)
80 Pretty.writeln (Proof_Context.pretty_term_abbrev @{context} r');
81 Pretty.writeln (Proof_Context.pretty_term_abbrev @{context} t');
84 "----------- test rewriting without Isac's thys ---------";
85 "----------- test rewriting without Isac's thys ---------";
86 "----------- test rewriting without Isac's thys ---------";
88 "===== rewriting with Isabelle2009-1 only, i.e without isac-hacks";
89 val thy = @{theory Complex_Main};
90 val ctxt = @{context};
91 val thm = @{thm add.commute};
92 val tm = @{term "x + y*z::real"};
94 val SOME (r,_) = (rewrite_ thy dummy_ord e_rls false thm tm)
95 handle _ => error "rewrite.sml diff.behav. in rewriting";
96 (*is displayed on _TOP_ of <response> buffer...*)
97 Pretty.writeln (Proof_Context.pretty_term_abbrev @{context} r);
98 if r = @{term "y*z + x::real"}
99 then () else error "rewrite.sml diff.result in rewriting";
101 "----- rewriting a subterm";
102 val tm = @{term "w*(x + y*z)::real"};
104 val SOME (r,_) = (rewrite_ thy dummy_ord e_rls false thm tm)
105 handle _ => error "rewrite.sml diff.behav. in rew_sub";
107 "----- ordered rewriting";
108 fun tord (_:subst) pp = Term_Ord.termless pp;
109 if tord [] (@{term "x + y*z::real"}, @{term "y*z + x::real"}) then ()
110 else error "rewrite.sml diff.behav. in ord.rewr.";
112 val NONE = (rewrite_ thy tord e_rls false thm tm)
113 handle _ => error "rewrite.sml diff.behav. in rewriting";
114 (*is displayed on _TOP_ of <response> buffer...*)
115 Pretty.writeln (Proof_Context.pretty_term_abbrev @{context} r);
117 val tm = @{term "x*y + z::real"};
118 val SOME (r,_) = (rewrite_ thy tord e_rls false thm tm)
119 handle _ => error "rewrite.sml diff.behav. in rewriting";
122 "----------- conditional rewriting without Isac's thys --";
123 "----------- conditional rewriting without Isac's thys --";
124 "----------- conditional rewriting without Isac's thys --";
126 "===== prepr cond.rew. with Pattern.match";
127 val thy = @{theory Complex_Main};
128 val ctxt = @{context};
129 val thm = @{thm nonzero_divide_mult_cancel_right};
130 val rule = Thm.prop_of thm;
131 val tm = @{term "x / (2 * x)::real"};
133 val prem = Logic.strip_imp_prems rule;
134 val nps = Logic.count_prems rule;
135 val prems = Logic.strip_prems (nps, [], rule);
137 val eq = Logic.strip_imp_concl rule;
138 val (LHS, RHS) = (HOLogic.dest_eq o HOLogic.dest_Trueprop) eq;
140 val mtcs = Pattern.match thy (LHS, tm) (Vartab.empty, Vartab.empty);
141 val rule' = Envir.subst_term mtcs rule;
143 val prems' = (fst o Logic.strip_prems)
144 (Logic.count_prems rule', [], rule');
145 val RHS' = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop
146 o Logic.strip_imp_concl) rule';
148 "----- conditional rewriting creating an assumption";
149 "----- conditional rewriting creating an assumption";
150 val thm = @{thm nonzero_divide_mult_cancel_right};
151 val tm = @{term "x / (2 * x)::real"};
152 val SOME (rew, asm) = (rewrite_ thy dummy_ord e_rls false thm tm)
153 handle _ => error "rewrite.sml diff.behav. in cond.rew.";
155 if rew = @{term "1 / 2::real"} then () (* the rewrite is _NO_ Trueprop *)
156 else error "rewrite.sml diff.result in cond.rew.";
158 if hd asm = @{term "x \<noteq> (0::real)"} (* dropped Trueprop $ ...*)
159 then () else error "rewrite.sml diff.asm in cond.rew.";
160 "----- conditional rewriting immediately: can only be done with ";
161 "------Isabelle numerals, because erls cannot handle them yet.";
164 "----------- step through 'and rew_sub': ----------------";
165 "----------- step through 'and rew_sub': ----------------";
166 "----------- step through 'and rew_sub': ----------------";
167 (*and make asms without Trueprop, beginning with the result:*)
168 val tm = @{term "x / (2 * x)::real"};
169 val (t', asm, _, _) = rew_sub thy 0 [] dummy_ord e_rls true [] (Thm.prop_of thm) tm;
170 (*show_types := false;*)
171 "----- evaluate arguments";
172 val (thy, i, bdv, tless, rls, put_asm, lrd, r, t) =
173 (thy, 0, [], dummy_ord, e_rls, true, [], (Thm.prop_of thm), tm);
174 "----- step 1: LHS, RHS of rule";
175 val (LHS, RHS) = (HOLogic.dest_eq o HOLogic.dest_Trueprop
176 o Logic.strip_imp_concl) r;
177 term2str r = "?b \<noteq> (0::?'a) \<Longrightarrow> ?b / (?a * ?b) = (1::?'a) / ?a";
178 term2str LHS = "?b / (?a * ?b)"; term2str RHS = "(1::?'a) / ?a";
179 "----- step 2: the rule instantiated";
180 val r' = Envir.subst_term
181 (Pattern.match thy (LHS, t) (Vartab.empty, Vartab.empty)) r;
182 term2str r' = "x \<noteq> 0 \<Longrightarrow> x / (2 * x) = 1 / 2";
183 "----- step 3: get the (instantiated) assumption(s)";
184 val p' = (fst o Logic.strip_prems) (Logic.count_prems r', [], r');
185 term2str (hd p') = "x \<noteq> 0";
186 "=====vvv make asms without Trueprop ---vvv";
187 val p' = map HOLogic.dest_Trueprop ((fst o Logic.strip_prems)
188 (Logic.count_prems r', [], r'));
190 [Const ("HOL.Not", _) $ (Const ("HOL.eq", _)
191 $ Free ("x", _) $ Const ("Groups.zero_class.zero", _))] => ()
192 | _ => error "rewrite.sml assumption changed";
193 "=====^^^ make asms without Trueprop ---^^^";
194 "----- step 4: get the (instantiated) RHS";
195 val t' = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop
196 o Logic.strip_imp_concl) r';
197 term2str t' = "1 / 2";
199 "----------- step through 'fun rewrite_terms_' ---------";
200 "----------- step through 'fun rewrite_terms_' ---------";
201 "----------- step through 'fun rewrite_terms_' ---------";
202 "----- step 0: args for rewrite_terms_, local fun";
203 val (thy, ord, erls, equs, t) =
204 (@{theory "Biegelinie"}, dummy_ord, Erls, [str2term "x = 0"],
205 str2term "M_b x = -1 * q_0 * x ^^^ 2 / 2 + x * c + c_2");
206 "----- step 1: args for rew_";
207 val ((t', asm'), (rules as r::rs), t) = ((e_term, []), equs, t);
208 "----- step 2: rew_sub";
209 rew_sub thy 1 [] ord erls false [] (HOLogic.Trueprop $ r) t;
210 "----- step 3: step through rew_sub -- inefficient: goes into subterms";
213 val SOME (t', _) = rewrite_terms_ thy dummy_ord Erls equs t;
214 writeln "----------- rewrite_terms_ 1---------------------------";
215 if term2str t' = "M_b 0 = -1 * q_0 * 0 ^^^ 2 / 2 + 0 * c + c_2" then ()
216 else error "rewrite.sml rewrite_terms_ [x = 0]";
218 val equs = [str2term "M_b 0 = 0"];
219 val t = str2term "M_b 0 = -1 * q_0 * 0 ^^^ 2 / 2 + 0 * c + c_2";
220 val SOME (t', _) = rewrite_terms_ thy dummy_ord Erls equs t;
221 writeln "----------- rewrite_terms_ 2---------------------------";
222 if term2str t' = "0 = -1 * q_0 * 0 ^^^ 2 / 2 + 0 * c + c_2" then ()
223 else error "rewrite.sml rewrite_terms_ [M_b 0 = 0]";
225 val equs = [str2term "x = 0", str2term"M_b 0 = 0"];
226 val t = str2term "M_b x = -1 * q_0 * x ^^^ 2 / 2 + x * c + c_2";
227 val SOME (t', _) = rewrite_terms_ thy dummy_ord Erls equs t;
228 writeln "----------- rewrite_terms_ 3---------------------------";
229 if term2str t' = "0 = -1 * q_0 * 0 ^^^ 2 / 2 + 0 * c + c_2" then ()
230 else error "rewrite.sml rewrite_terms_ [x = 0, M_b 0 = 0]";
233 "----------- rewrite_inst_ bdvs -------------------------";
234 "----------- rewrite_inst_ bdvs -------------------------";
235 "----------- rewrite_inst_ bdvs -------------------------";
236 (*see smltest/Scripts/term_G.sml: inst_bdv 2*)
237 val t = str2term"-1 * (q_0 * L ^^^ 2) / 2 + (L * c_3 + c_4) = 0";
238 val bdvs = [(str2term"bdv_1",str2term"c"),
239 (str2term"bdv_2",str2term"c_2"),
240 (str2term"bdv_3",str2term"c_3"),
241 (str2term"bdv_4",str2term"c_4")];
242 (*------------ outcommented WN071210, after inclusion into ROOT.ML
244 rewrite_inst_ thy e_rew_ord
245 (append_rls "erls_isolate_bdvs" e_rls
246 [(Calc ("EqSystem.occur'_exactly'_in",
247 eval_occur_exactly_in
248 "#eval_occur_exactly_in_"))
250 false bdvs (num_str @{separate_bdvs_add) t;
251 (writeln o term2str) t;
252 if term2str t = "L * c_3 + c_4 = 0 + -1 * (-1 * (q_0 * L ^^^ 2) / 2)"
253 then () else error "rewrite.sml rewrite_inst_ bdvs";
255 trace_rewrite:=false;--------------------------------------------*)
258 "----------- check diff 2002--2009-3 --------------------";
259 "----------- check diff 2002--2009-3 --------------------";
260 "----------- check diff 2002--2009-3 --------------------";
261 (*----- 2002 -------------------------------------------------------------------
262 # rls: norm_Rational_noadd_fractions on: 1 / EI * (L * q_0 * x / 2 + -1 *
264 ## rls: discard_minus_ on: 1 / EI * (L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2
266 ### try thm: real_diff_minus
267 ### try thm: sym_real_mult_minus1
268 ## rls: rat_mult_poly on: 1 / EI * (L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2
270 ### try thm: rat_mult_poly_l
271 ### try thm: rat_mult_poly_r
272 #### eval asms: L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2 is_polyexp
273 ==> 1 / EI * (L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2) =
274 1 * (L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2) / EI
275 ##### rls: e_rls-is_polyexp on: L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2
277 ###### try calc: Poly.is'_polyexp'
278 ====== calc. to: False
279 ###### try calc: Poly.is'_polyexp'
280 ###### try calc: Poly.is'_polyexp'
281 #### asms false: ["L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2 is_polyexp"]
282 ----- 2002 NONE rewrite --------------------------------------------------------
283 ----- 2009 should maintain this behaviour, but: --------------------------------
284 # rls: norm_Rational_noadd_fractions on: 1 / EI * (L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2)
285 ## rls: discard_minus on: 1 / EI * (L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2)
286 ### try thm: real_diff_minus
287 ### try thm: sym_real_mult_minus1
288 ## rls: rat_mult_poly on: 1 / EI * (L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2)
289 ### try thm: rat_mult_poly_l
290 ### try thm: rat_mult_poly_r
291 #### eval asms: L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2 is_polyexp
292 ==> 1 / EI * (L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2) =
293 1 * (L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2) / EI
294 ##### rls: e_rls-is_polyexp on: L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2 is_polyexp
295 ###### try calc: Poly.is'_polyexp'
296 ====== calc. to: False
297 ###### try calc: Poly.is'_polyexp'
298 ###### try calc: Poly.is'_polyexp'
299 #### asms accepted: ["L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2 is_polyexp"] stored: ["False"]
300 === rewrites to: 1 * (L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2) / EI
301 ----- 2009 -------------------------------------------------------------------*)
303 (*the situation as was before repair (asm without Trueprop) is outcommented*)
304 val thy = @{theory "Isac"};
305 "===== example which raised the problem =================";
306 val t = @{term "1 / EI * (L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2)"};
307 "----- rewrite_set_inst_ norm_Rational_noadd_fractions--";
308 val subs = [(@{term "bdv"}, @{term "x"})];
309 val rls = norm_Rational_noadd_fractions;
310 val SOME (t', asms) = rewrite_set_inst_ thy true subs rls t;
311 if term2str t' = "1 / EI * (L * q_0 * x / 2 + -1 * 1 * q_0 * x ^^^ 2 / 2)" andalso
312 terms2str asms = "[]" then {}
313 else error "this was NONE with Isabelle2013-2 ?!?"
314 "----- rewrite_ rat_mult_poly_r--------------------------";
315 val thm = @{thm rat_mult_poly_r};
316 "?c::real is_polyexp ==> (?a::real) / (?b::real) * ?c = ?a * ?c / ?b";
317 val erls = append_rls "e_rls-is_polyexp" e_rls
318 [Calc ("Poly.is'_polyexp", eval_is_polyexp "")];
319 val NONE (*SOME (t'', _)*) = rewrite_ thy dummy_ord erls true thm t;
320 (*t' = t''; (*false because of further rewrites in t'*)*)
321 "----- rew_sub --------------------------------";
322 val (t''', _, _, _) = rew_sub thy 0 [] dummy_ord erls true [] (Thm.prop_of thm) t;
323 (*t'' = t'''; (*true*)*)
324 "----- rewrite_set_ erls --------------------------------";
325 val cond = @{term "(L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2)"};
326 val NONE = rewrite_set_ thy true erls cond;
327 (* ^^^^^ goes with '====== calc. to: False' above from beginning*)
329 writeln "===== maximally simplified example =====================";
330 val t = @{term "a / b * (x / x ^^^ 2)"};
331 "?c::real is_polyexp ==> (?a::real) / (?b::real) * ?c = ?a * ?c / ?b";
332 writeln "----- rewrite_set_inst_ norm_Rational_noadd_fractions--";
333 val (*NONE*) SOME (t', asm) = rewrite_set_inst_ thy true subs rls t;
334 term2str t' = "a * x / (b * x ^^^ 2)"; (*rew. by thm outside test case*)
335 (*checked visually: trace_rewrite looks like above for 2009*)
337 writeln "----- rewrite_ rat_mult_poly_r--------------------------";
338 val NONE (*SOME (t'', _)*) = rewrite_ thy dummy_ord erls true thm t;
339 (*t' = t''; (*false because of further rewrites in t'*)*)
340 writeln "----- rew_sub --------------------------------";
341 val (t''', _, _, _) = rew_sub thy 0 [] dummy_ord erls true [] (Thm.prop_of thm) t;
342 (*t'' = t'''; (*true*)*)
343 writeln "----- rewrite_set_ erls --------------------------------";
344 val cond = @{term "(x / x ^^^ 2)"};
345 val NONE = rewrite_set_ thy true erls cond;
346 (* ^^^^^ goes with '====== calc. to: False' above from beginning*)
349 "----------- compare all prepat's existing 2010 ---------";
350 "----------- compare all prepat's existing 2010 ---------";
351 "----------- compare all prepat's existing 2010 ---------";
352 val thy = @{theory "Isac"};
353 val t = @{term "a + b * x = (0 ::real)"};
354 val pat = parse_patt thy "?l = (?r ::real)";
355 val precond = parse_patt thy "is_polynomial (?l::real)";(*no infix def*)
356 val precond = parse_patt thy "(?l::real) is_expanded";
358 val inst = Pattern.match thy (pat, t) (Vartab.empty, Vartab.empty);
359 val preinst = Envir.subst_term inst precond;
362 "===== Rational.thy: cancel ===";
363 (* pat matched with the current term gives an environment
364 (or not: hen the Rrls not applied);
365 if pre1 and pre2 evaluate to @{term True} in this environment,
366 then the Rrls is applied. *)
367 val t = str2term "(a + b) / c ::real";
368 val pat = parse_patt thy "?r / ?s ::real";
369 val pres = [parse_patt thy "?r is_expanded", parse_patt thy "?s is_expanded"];
370 val prepat = [(pres, pat)];
371 val erls = rational_erls;
372 (* erls got from Rrls {erls, prepat, scr = Rfuns {normal_form, ...}, ...} *)
374 val subst = Pattern.match thy (pat, t) (Vartab.empty, Vartab.empty);
375 val asms = map (Envir.subst_term subst) pres;
376 if terms2str asms = "[\"a + b is_expanded\",\"c is_expanded\"]"
377 then () else error "rewrite.sml: prepat cancel subst";
378 if ([], true) = eval__true thy 0 asms [] erls
379 then () else error "rewrite.sml: prepat cancel eval__true";
381 "===== Rational.thy: add_fractions_p ===";
382 (* if each pat* matches with the current term, the Rrls is applied
383 (there are no preconditions to be checked, they are @{term True}) *)
384 val t = str2term "a / b + 1 / 2";
385 val pat = parse_patt thy "?r / ?s + ?u / ?v";
386 val pres = [@{term True}];
387 val prepat = [(pres, pat)];
388 val erls = rational_erls;
389 (* erls got from Rrls {erls, prepat, scr = Rfuns {normal_form, ...}, ...} *)
391 val subst = Pattern.match thy (pat, t) (Vartab.empty, Vartab.empty);
392 if ([], true) = eval__true thy 0 (map (Envir.subst_term subst) pres) [] erls
393 then () else error "rewrite.sml: prepat add_fractions_p";
395 "===== Poly.thy: order_mult_ ===";
396 (* ?p matched with the current term gives an environment,
397 which evaluates (the instantiated) "p is_multUnordered" to true*)
398 val t = str2term "x^^^2 * x";
399 val pat = parse_patt thy "?p :: real"
400 val pres = [parse_patt thy "?p is_multUnordered"];
401 val prepat = [(pres, pat)];
402 val erls = append_rls "e_rls-is_multUnordered" e_rls
403 [Calc ("Poly.is'_multUnordered",
404 eval_is_multUnordered "")];
406 val subst = Pattern.match thy (pat, t) (Vartab.empty, Vartab.empty);
407 val asms = map (Envir.subst_term subst) pres;
408 if terms2str asms = "[\"x ^^^ 2 * x is_multUnordered\"]"
409 then () else error "rewrite.sml: prepat order_mult_ subst";
410 if ([], true) = eval__true thy 0 asms [] erls
411 then () else error "rewrite.sml: prepat order_mult_ eval__true";
414 "----------- fun app_rev, Rrls, -------------------------";
415 "----------- fun app_rev, Rrls, -------------------------";
416 "----------- fun app_rev, Rrls, -------------------------";
417 val t = str2term "x^^^2 * x";
419 if is_multUnordered t then () else error "rewrite.sml diff. is_multUnordered 2";
420 val tm = str2term "(x^^^2 * x) is_multUnordered";
421 eval_is_multUnordered "testid" "" tm thy;
423 case eval_is_multUnordered "testid" "" tm thy of
424 SOME (_, Const ("HOL.Trueprop", _) $
425 (Const ("HOL.eq", _) $
426 (Const ("Poly.is'_multUnordered", _) $ _) $
427 Const ("HOL.True", _))) => ()
428 | _ => error "rewrite.sml diff. eval_is_multUnordered 2b";
430 tracing "----- begin rewrite x^^^2 * x ---"; trace_rewrite := true;
431 val SOME (t', _) = rewrite_set_ thy true order_mult_ t;
432 tracing "----- end rewrite x^^^2 * x ---"; trace_rewrite := false;
433 if term2str t' = "x * x ^^^ 2" then ()
434 else error "rewrite.sml Poly.is'_multUnordered doesn't work";
436 (* for achieving the previous result, the following code was taken apart *)
437 "----- rewrite__set_ ---";
438 val (thy, i, _, _, (rrls as Rrls _), t) = (thy, 0, true, [], order_mult_, tm);
439 val (t', asm, rew) = app_rev thy (i+1) rrls t;
441 val (thy, i, rrls, t) = (thy, (i+1), rrls, t);
442 fun chk_prepat thy erls [] t = true
443 | chk_prepat thy erls prepat t =
444 let fun chk (pres, pat) =
445 (let val subst: Type.tyenv * Envir.tenv =
446 Pattern.match thy (pat, t)
447 (Vartab.empty, Vartab.empty)
448 in snd (eval__true thy (i+1)
449 (map (Envir.subst_term subst) pres)
453 fun scan_ f [] = false (*scan_ NEVER called by []*)
454 | scan_ f (pp::pps) = if f pp then true
456 in scan_ chk prepat end;
458 (*.apply the normal_form of a rev-set.*)
459 fun app_rev' thy (Rrls{erls,prepat,scr=Rfuns{normal_form,...},...}) t =
460 if chk_prepat thy erls prepat t
461 then ((*tracing("### app_rev': t = "^(term2str t));*)
464 (*fixme val NONE = app_rev' thy rrls t;*)
465 "----- app_rev' ---";
466 val (thy, Rrls{erls,prepat,scr=Rfuns{normal_form,...},...}, t) = (thy, rrls, t);
467 (*fixme false*) chk_prepat thy erls prepat t;
468 "----- chk_prepat ---";
469 val (thy, erls, prepat, t) = (thy, erls, prepat, t);
470 fun chk (pres, pat) =
471 (let val subst: Type.tyenv * Envir.tenv =
472 Pattern.match thy (pat, t)
473 (Vartab.empty, Vartab.empty)
474 in snd (eval__true thy (i+1)
475 (map (Envir.subst_term subst) pres)
479 fun scan_ f [] = false (*scan_ NEVER called by []*)
480 | scan_ f (pp::pps) = if f pp then true
482 tracing "=== poly.sml: scan_ chk prepat begin";
484 tracing "=== poly.sml: scan_ chk prepat end";
487 (*reestablish...*) val t = str2term "x ^^^ 2 * x";
488 val [(pres, pat)] = prepat;
489 val subst: Type.tyenv * Envir.tenv =
490 Pattern.match thy (pat, t)
491 (Vartab.empty, Vartab.empty);
493 (*fixme: asms = ["p is_multUnordered"]...instantiate*)
494 "----- eval__true ---";
495 val asms = (map (Envir.subst_term subst) pres);
496 if terms2str asms = "[\"x ^^^ 2 * x is_multUnordered\"]" then ()
497 else error "rewrite.sml: diff. is_multUnordered, asms";
498 val (thy, i, asms, bdv, rls) =
499 (thy, (i+1), [str2term "(x^^^2 * x) is_multUnordered"],
500 [] : (term * term) list, erls);
501 case eval__true thy i asms bdv rls of
503 | _ => error "rewrite.sml: diff. is_multUnordered, eval__true";
505 "----------- 2011 thms with axclasses -------------------";
506 "----------- 2011 thms with axclasses -------------------";
507 "----------- 2011 thms with axclasses -------------------";
508 val thm = num_str @{thm div_by_1};
509 val prop = Thm.prop_of thm;
510 atomty prop; (*Type 'a*)
511 val t = str2term "(2*x)/1"; (*Type real*)
513 val (thy, ro, er, inst) =
514 (@{theory "Isac"}, tless_true, eval_rls, [(@{term "bdv::real"}, @{term "x::real"})]);
515 val SOME (t, _) = rewrite_ thy ro er true thm t; (*real matches 'a ?via ring? etc*)
517 "----------- repair NO asms from rls RatEq_eliminate ----";
518 "----------- repair NO asms from rls RatEq_eliminate ----";
519 "----------- repair NO asms from rls RatEq_eliminate ----";
520 val t = str2term "1 / x = 5";
521 trace_rewrite := true;
522 val SOME (t', asm) = rewrite_ thy e_rew_ord e_rls true @{thm rat_mult_denominator_right} t;
523 term2str t' = "1 = 5 * x";
524 terms2str asm = "[\"x ~= 0\"]";
526 ## eval asms: x ~= 0 ==> (1 / x = 5) = (1 = 5 * x)
527 ### rls: e_rls on: x ~= 0
528 ## asms accepted: ["x ~= 0"] stored: ["x ~= 0"]
530 trace_rewrite := false;
532 trace_rewrite := false;
533 val SOME (t', []) = rewrite_set_ thy true RatEq_eliminate t; (*= [] must be = "x ~= 0"*)
534 term2str t' = "1 = 5 * x";
537 #### rls: rateq_erls on: x ~= 0
539 ##### try calc: HOL.eq' <<<------------------------------- here the error comes from
540 ===== calc. to: ~ False
541 ##### try calc: HOL.eq'
542 ##### try thm: not_true
543 ##### try thm: not_false
544 ===== rewrites to: True
546 ### asms accepted: ["x ~= 0"] stored: []
549 trace_rewrite := false;
550 (* WN120317.TODO dropped rateq: the above error is the same in 2002 *)
552 "----------- fun assoc_thm' -----------------------------";
553 "----------- fun assoc_thm' -----------------------------";
554 "----------- fun assoc_thm' -----------------------------";
555 val thy = @{theory ProgLang}
557 val tth = assoc_thm' thy ("sym_#mult_2_3","6 = 2 * 3");
558 if string_of_thm' thy tth = "6 = 2 * 3" then ()
559 else error "assoc_thm' (sym_#mult_2_3, 6 = 2 * 3) changed";
561 val tth = assoc_thm' thy ("add_0_left","");
562 if string_of_thm' thy tth = "0 + ?a = ?a" then ()
563 else error "assoc_thm' (add_0_left,\"\") changed";
565 val tth = assoc_thm' thy ("sym_add_0_left","");
566 if string_of_thm' thy tth = "?t = 0 + ?t" then ()
567 else error "assoc_thm' (sym_add_0_left,\"\") changed";
569 val tth = assoc_thm' thy ("add_commute","");
570 if string_of_thm' thy tth = "?a + ?b = ?b + ?a" then ()
571 else error "assoc_thm' (add_commute,\"\") changed"
573 "----------- fun rewrite_ down to Pattern.match ------------------------------------------------";
574 "----------- fun rewrite_ down to Pattern.match ------------------------------------------------";
575 "----------- fun rewrite_ down to Pattern.match ------------------------------------------------";
576 "~~~~~ fun rewrite_ , args:"; val (thy, rew_ord, erls, bool, thm, term) =
577 (@{theory}, dummy_ord, e_rls, false, @{thm distrib_left}, @{term "x * (y + z) :: int"});
578 "~~~~~ fun rewrite__ , args:"; val (thy, i, bdv, tless, rls, put_asm, thm, ct) =
579 (thy, 1, [], rew_ord, erls, bool, thm, term);
580 "~~~~~ and rew_sub , args:"; val (thy, i, bdv, tless, rls, put_asm, lrd, r, t) =
581 (thy, i, bdv, tless, rls, put_asm, [], (((inst_bdv bdv) o norm o #prop o Thm.rep_thm) thm), ct)
582 val (lhss, rhss) = (HOLogic.dest_eq o HOLogic.dest_Trueprop o Logic.strip_imp_concl) r
583 val r' = Envir.subst_term (Pattern.match thy (lhss, t) (Vartab.empty, Vartab.empty)) r
584 val p' = map HOLogic.dest_Trueprop ((fst o Logic.strip_prems) (Logic.count_prems r', [], r'))
585 val t' = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop o Logic.strip_imp_concl) r'
587 if term2str lhss = "?a * (?b + ?c)" andalso term2str t = "x * (y + z)" then ()
588 else error "ARGS FOR Pattern.match CHANGED";
589 val match = Pattern.match thy (lhss, t) (Vartab.empty, Vartab.empty);
590 if (Envir.subst_term match r |> term2str) = "x * (y + z) = x * y + x * z" then ()
591 else error "Pattern.match CHANGED";
593 "----------- fun mk_thm ------------------------------------------------------------------------";
594 "----------- fun mk_thm ------------------------------------------------------------------------";
595 "----------- fun mk_thm ------------------------------------------------------------------------";
596 val thy = @{theory Isac}
598 (*~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~*)
599 val thm = @{thm realpow_twoI};
600 val patt_str = "?r ^^^ 2 = ?r * ?r";
601 val term_str = "r ^^^ 2 = r * r";
602 (*~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~*)
603 case parse_patt thy patt_str of
604 Const ("HOL.eq", _) $ (Const ("Atools.pow", _) $ Var (("r", 0), _) $ Free ("2", _)) $
605 (Const ("Groups.times_class.times", _) $ Var (("r", 0), _) $ Var (("r", 0), _)) => ()
606 | _ => error "parse_patt ?r ^^^ 2 = ?r * ?r changed";
607 case parse thy term_str of
609 | _ => writeln "parse does NOT take patterns with '?'";
611 val t1 = (#prop o Thm.rep_thm) (num_str thm);
612 if term2str t1 = patt_str then () else error "realpow_twoI (\<rightarrow> string) NOT equal to given string";
614 val t2 = HOLogic.Trueprop $ (((parse_patt thy)) patt_str) : term;
615 if t1 = t2 then () else error "prop of realpow_twoI NOT equal to parsed string";
617 (mk_thm thy patt_str) handle _ => mk_thm thy "mk_thm = does NOT handle patterns";
618 (*and this*) mk_thm thy term_str (* = "r ^^^ 2 = r * r" [.]: thm
619 gives a strange thm*);
621 val thm_made = Thm.make_thm (Thm.global_cterm_of thy t2) (* = "?r ^^^ 2 = ?r * ?r" [.]: thm
622 ..gives another strange thm; but it is used and works with rewriting: *);
624 val t1' = (#prop o Thm.rep_thm) (num_str thm_made);
625 if t1 = t1' then () else error "prop of realpow_twoI NOT equal to thm_made from string";
627 (*~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~*)
628 val thm = @{thm real_mult_div_cancel2};
629 val patt_str = "?k \<noteq> 0 \<Longrightarrow> ?m * ?k / (?n * ?k) = ?m / ?n";
630 val term_str = "k \<noteq> 0 \<Longrightarrow> m * k / (n * k) = m / n";
631 (*~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~*)
632 case parse_patt thy patt_str of
633 Const ("Pure.imp", _) $
634 (Const ("HOL.Trueprop", _) $ (Const ("HOL.Not", _) $
635 (Const ("HOL.eq", _) $ Var (("k", 0), _) $ Free ("0", _)))) $
636 (Const ("HOL.Trueprop", _) $
637 (Const ("HOL.eq", _) $ _ $ _ )) => ()
638 | _ => error "parse_patt ?k \<noteq> 0 ==> ?m * ?k / (?n * ?k) = ?m / ?n changed";
639 case parse thy term_str of
641 | _ => writeln "parse does NOT take patterns with '?'";
643 val t1 = (#prop o Thm.rep_thm) (num_str thm);
644 if term2str t1 = patt_str then () else error "realpow_twoI (\<rightarrow> string) NOT equal to given string";
646 val t2 = (*Trueprop $*) (((parse_patt thy)) patt_str) : term;
647 if t1 = t2 then () else error "prop of realpow_twoI NOT equal to parsed string";
649 (mk_thm thy patt_str) handle _ => mk_thm thy "mk_thm = does NOT handle patterns";
650 (*and this*) mk_thm thy term_str (* = "r ^^^ 2 = r * r" [.]: thm
651 gives a strange thm*);
653 val thm_made = Thm.make_thm (Thm.global_cterm_of thy t2) (* = "?r ^^^ 2 = ?r * ?r" [.]: thm
654 gives another strange thm; but it is used and words with rewriting: *);
656 val t1' = (#prop o Thm.rep_thm) (num_str thm_made);
657 if t1 = t1' then () else error "prop of realpow_twoI NOT equal to thm_made from string";
659 "----------- fun rewrite_set_ .. norm_equation -------------------------------------------------";
660 "----------- fun rewrite_set_ .. norm_equation -------------------------------------------------";
661 "----------- fun rewrite_set_ .. norm_equation -------------------------------------------------";
662 (* norm_equation is defined in Test.thy, other rls see Knowledg/**)
664 val rls = norm_equation;
665 val term = str2term "x + 1 = 2";
667 val SOME (t, asm) = rewrite_set_ thy false rls term;
668 if term2str t = "x + 1 + -1 * 2 = 0" then () else error "rewrite_set_ norm_equation CHANGED";
670 "~~~~~ fun rewrite_set_, args:"; val (thy, bool, rls, term) = (thy, false, rls, term);
671 "~~~~~ fun rewrite__set_, args:"; val (thy, i, put_asm, bdv, rls, ct) = (thy, 1, bool, [], rls, term);