1 (* Title: "ProgLang/rewrite.sml"
2 Author: Walther Neuper 050908
3 (c) copyright due to lincense terms.
6 "--------------------------------------------------------";
7 "table of contents --------------------------------------";
8 "--------------------------------------------------------";
9 "----------- assemble rewrite ---------------------------";
10 "----------- test rewriting without Isac session --------";
11 "----------- conditional rewriting without Isac session -";
12 "----------- step through 'and rew_sub': ----------------";
13 "----------- step through 'fun rewrite_terms_' ---------";
14 "----------- rewrite_inst_ bdvs -------------------------";
15 "----------- check diff 2002--2009-3 --------------------";
16 "----------- compare all prepat's existing 2010 ---------";
17 "----------- fun app_rev, Rrls, -------------------------";
18 "----------- 2011 thms with axclasses -------------------";
19 "----------- fun rewrite_set_ .. RatEq_eliminate step into to fun chk --------------------------";
20 "----------- fun assoc_thm' -----------------------------";
21 "----------- fun rewrite_ down to Pattern.match ------------------------------------------------";
22 "----------- fun mk_thm ------------------------------------------------------------------------";
23 "----------- fun rewrite_set_ .. norm_equation -------------------------------------------------";
24 "----------- fun rewrite_set_ .. RatEq_eliminate step into to fun chk --------------------------";
25 "--------------------------------------------------------";
26 "--------------------------------------------------------";
27 "--------------------------------------------------------";
30 "----------- assemble rewrite ---------------------------";
31 "----------- assemble rewrite ---------------------------";
32 "----------- assemble rewrite ---------------------------";
33 "===== rewriting by thm with 'a";
34 (*show_types := true;*)
36 val thy = @{theory Complex_Main};
37 val ctxt = @{context};
38 val thm = @{thm add.commute};
39 val t = (Thm.term_of o the) (parse thy "((r + u) + t) + s");
40 "----- from old: fun rewrite__";
42 val r = (((inst_bdv bdv) o norm o #prop o Thm.rep_thm) thm);
43 "----- from old: and rew_sub";
44 val (LHS,RHS) = (dest_equals o strip_trueprop
45 o Logic.strip_imp_concl) r;
47 val insts = Pattern.match thy (LHS,t) (Vartab.empty, Vartab.empty);*)
48 "----- fun match_rew in Pure/pattern.ML";
49 val rtm = the_default RHS (Term.rename_abs LHS t RHS);
51 writeln(Syntax.string_of_term ctxt rtm);
52 writeln(Syntax.string_of_term ctxt LHS);
53 writeln(Syntax.string_of_term ctxt t);
55 (Pattern.match thy (LHS, t) (Vartab.empty, Vartab.empty));
56 val (rew, RHS) = (Envir.subst_term
57 (Pattern.match thy (LHS, t) (Vartab.empty, Vartab.empty)) rtm, rtm);
58 (*lookup in isabelle?trace?response...*)
59 writeln(Syntax.string_of_term ctxt rew);
60 writeln(Syntax.string_of_term ctxt RHS);
61 "===== rewriting: prep insertion into rew_sub";
62 val thy = @{theory Complex_Main};
63 val ctxt = @{context};
64 val thm = @{thm nonzero_divide_mult_cancel_right};
65 val r = Thm.prop_of thm;
66 val tm = @{term "x / (2 * x)::real"};
68 val (LHS, RHS) = (HOLogic.dest_eq o HOLogic.dest_Trueprop
69 o Logic.strip_imp_concl) r;
70 val r' = Envir.subst_term (Pattern.match thy (LHS, tm)
71 (Vartab.empty, Vartab.empty)) r;
72 val p' = (fst o Logic.strip_prems) (Logic.count_prems r', [], r');
73 val t' = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop
74 o Logic.strip_imp_concl) r';
76 (*is displayed on top of <response> buffer...*)
77 Pretty.writeln (Proof_Context.pretty_term_abbrev @{context} r');
78 Pretty.writeln (Proof_Context.pretty_term_abbrev @{context} t');
81 "----------- test rewriting without Isac's thys ---------";
82 "----------- test rewriting without Isac's thys ---------";
83 "----------- test rewriting without Isac's thys ---------";
85 "===== rewriting with Isabelle2009-1 only, i.e without isac-hacks";
86 val thy = @{theory Complex_Main};
87 val ctxt = @{context};
88 val thm = @{thm add.commute};
89 val tm = @{term "x + y*z::real"};
91 val SOME (r,_) = (rewrite_ thy dummy_ord Rule_Set.empty false thm tm)
92 handle _ => error "rewrite.sml diff.behav. in rewriting";
93 (*is displayed on _TOP_ of <response> buffer...*)
94 Pretty.writeln (Proof_Context.pretty_term_abbrev @{context} r);
95 if r = @{term "y*z + x::real"}
96 then () else error "rewrite.sml diff.result in rewriting";
98 "----- rewriting a subterm";
99 val tm = @{term "w*(x + y*z)::real"};
101 val SOME (r,_) = (rewrite_ thy dummy_ord Rule_Set.empty false thm tm)
102 handle _ => error "rewrite.sml diff.behav. in rew_sub";
104 "----- ordered rewriting";
105 fun tord (_:subst) pp = LibraryC.termless pp;
106 if tord [] (@{term "x + y*z::real"}, @{term "y*z + x::real"}) then ()
107 else error "rewrite.sml diff.behav. in ord.rewr.";
109 val NONE = (rewrite_ thy tord Rule_Set.empty false thm tm)
110 handle _ => error "rewrite.sml diff.behav. in rewriting";
111 (*is displayed on _TOP_ of <response> buffer...*)
112 Pretty.writeln (Proof_Context.pretty_term_abbrev @{context} r);
114 val tm = @{term "x*y + z::real"};
115 val SOME (r,_) = (rewrite_ thy tord Rule_Set.empty false thm tm)
116 handle _ => error "rewrite.sml diff.behav. in rewriting";
119 "----------- conditional rewriting without Isac's thys --";
120 "----------- conditional rewriting without Isac's thys --";
121 "----------- conditional rewriting without Isac's thys --";
123 "===== prepr cond.rew. with Pattern.match";
124 val thy = @{theory Complex_Main};
125 val ctxt = @{context};
126 val thm = @{thm nonzero_divide_mult_cancel_right};
127 val rule = Thm.prop_of thm;
128 val tm = @{term "x / (2 * x)::real"};
130 val prem = Logic.strip_imp_prems rule;
131 val nps = Logic.count_prems rule;
132 val prems = Logic.strip_prems (nps, [], rule);
134 val eq = Logic.strip_imp_concl rule;
135 val (LHS, RHS) = (HOLogic.dest_eq o HOLogic.dest_Trueprop) eq;
137 val mtcs = Pattern.match thy (LHS, tm) (Vartab.empty, Vartab.empty);
138 val rule' = Envir.subst_term mtcs rule;
140 val prems' = (fst o Logic.strip_prems)
141 (Logic.count_prems rule', [], rule');
142 val RHS' = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop
143 o Logic.strip_imp_concl) rule';
145 "----- conditional rewriting creating an assumption";
146 "----- conditional rewriting creating an assumption";
147 val thm = @{thm nonzero_divide_mult_cancel_right};
148 val tm = @{term "x / (2 * x)::real"};
149 val SOME (rew, asm) = (rewrite_ thy dummy_ord Rule_Set.empty false thm tm)
150 handle _ => error "rewrite.sml diff.behav. in cond.rew.";
152 if rew = @{term "1 / 2::real"} then () (* the rewrite is _NO_ Trueprop *)
153 else error "rewrite.sml diff.result in cond.rew.";
155 if hd asm = @{term "x \<noteq> (0::real)"} (* dropped Trueprop $ ...*)
156 then () else error "rewrite.sml diff.asm in cond.rew.";
157 "----- conditional rewriting immediately: can only be done with ";
158 "------Isabelle numerals, because erls cannot handle them yet.";
161 "----------- step through 'and rew_sub': ----------------";
162 "----------- step through 'and rew_sub': ----------------";
163 "----------- step through 'and rew_sub': ----------------";
164 (*and make asms without Trueprop, beginning with the result:*)
165 val tm = @{term "x / (2 * x)::real"};
166 val (t', asm, _, _) = rew_sub thy 0 [] dummy_ord Rule_Set.empty true [] (Thm.prop_of thm) tm;
167 (*show_types := false;*)
168 "----- evaluate arguments";
169 val (thy, i, bdv, tless, rls, put_asm, lrd, r, t) =
170 (thy, 0, [], dummy_ord, Rule_Set.empty, true, [], (Thm.prop_of thm), tm);
171 "----- step 1: LHS, RHS of rule";
172 val (LHS, RHS) = (HOLogic.dest_eq o HOLogic.dest_Trueprop
173 o Logic.strip_imp_concl) r;
174 UnparseC.term2str r = "?b \<noteq> (0::?'a) \<Longrightarrow> ?b / (?a * ?b) = (1::?'a) / ?a";
175 UnparseC.term2str LHS = "?b / (?a * ?b)"; UnparseC.term2str RHS = "(1::?'a) / ?a";
176 "----- step 2: the rule instantiated";
177 val r' = Envir.subst_term
178 (Pattern.match thy (LHS, t) (Vartab.empty, Vartab.empty)) r;
179 UnparseC.term2str r' = "x \<noteq> 0 \<Longrightarrow> x / (2 * x) = 1 / 2";
180 "----- step 3: get the (instantiated) assumption(s)";
181 val p' = (fst o Logic.strip_prems) (Logic.count_prems r', [], r');
182 UnparseC.term2str (hd p') = "x \<noteq> 0";
183 "=====vvv make asms without Trueprop ---vvv";
184 val p' = map HOLogic.dest_Trueprop ((fst o Logic.strip_prems)
185 (Logic.count_prems r', [], r'));
187 [Const ("HOL.Not", _) $ (Const ("HOL.eq", _)
188 $ Free ("x", _) $ Const ("Groups.zero_class.zero", _))] => ()
189 | _ => error "rewrite.sml assumption changed";
190 "=====^^^ make asms without Trueprop ---^^^";
191 "----- step 4: get the (instantiated) RHS";
192 val t' = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop
193 o Logic.strip_imp_concl) r';
194 UnparseC.term2str t' = "1 / 2";
196 "----------- step through 'fun rewrite_terms_' ---------";
197 "----------- step through 'fun rewrite_terms_' ---------";
198 "----------- step through 'fun rewrite_terms_' ---------";
199 "----- step 0: args for rewrite_terms_, local fun";
200 val (thy, ord, erls, equs, t) =
201 (@{theory "Biegelinie"}, dummy_ord, Rule_Set.Empty, [str2term "x = 0"],
202 str2term "M_b x = -1 * q_0 * x ^^^ 2 / 2 + x * c + c_2");
203 "----- step 1: args for rew_";
204 val ((t', asm'), (rules as r::rs), t) = ((TermC.empty, []), equs, t);
205 "----- step 2: rew_sub";
206 rew_sub thy 1 [] ord erls false [] (HOLogic.Trueprop $ r) t;
207 "----- step 3: step through rew_sub -- inefficient: goes into subterms";
210 val SOME (t', _) = rewrite_terms_ thy dummy_ord Rule_Set.Empty equs t;
211 writeln "----------- rewrite_terms_ 1---------------------------";
212 if UnparseC.term2str t' = "M_b 0 = -1 * q_0 * 0 ^^^ 2 / 2 + 0 * c + c_2" then ()
213 else error "rewrite.sml rewrite_terms_ [x = 0]";
215 val equs = [str2term "M_b 0 = 0"];
216 val t = str2term "M_b 0 = -1 * q_0 * 0 ^^^ 2 / 2 + 0 * c + c_2";
217 val SOME (t', _) = rewrite_terms_ thy dummy_ord Rule_Set.Empty equs t;
218 writeln "----------- rewrite_terms_ 2---------------------------";
219 if UnparseC.term2str t' = "0 = -1 * q_0 * 0 ^^^ 2 / 2 + 0 * c + c_2" then ()
220 else error "rewrite.sml rewrite_terms_ [M_b 0 = 0]";
222 val equs = [str2term "x = 0", str2term"M_b 0 = 0"];
223 val t = str2term "M_b x = -1 * q_0 * x ^^^ 2 / 2 + x * c + c_2";
224 val SOME (t', _) = rewrite_terms_ thy dummy_ord Rule_Set.Empty equs t;
225 writeln "----------- rewrite_terms_ 3---------------------------";
226 if UnparseC.term2str t' = "0 = -1 * q_0 * 0 ^^^ 2 / 2 + 0 * c + c_2" then ()
227 else error "rewrite.sml rewrite_terms_ [x = 0, M_b 0 = 0]";
230 "----------- rewrite_inst_ bdvs -------------------------";
231 "----------- rewrite_inst_ bdvs -------------------------";
232 "----------- rewrite_inst_ bdvs -------------------------";
233 (*see smltest/Scripts/term_G.sml: inst_bdv 2*)
234 val t = str2term"-1 * (q_0 * L ^^^ 2) / 2 + (L * c_3 + c_4) = 0";
235 val bdvs = [(str2term"bdv_1",str2term"c"),
236 (str2term"bdv_2",str2term"c_2"),
237 (str2term"bdv_3",str2term"c_3"),
238 (str2term"bdv_4",str2term"c_4")];
239 (*------------ outcommented WN071210, after inclusion into ROOT.ML
241 rewrite_inst_ thy e_rew_ord
242 (Rule_Set.append_rules "erls_isolate_bdvs" Rule_Set.empty
243 [(Num_Calc ("EqSystem.occur'_exactly'_in",
244 eval_occur_exactly_in
245 "#eval_occur_exactly_in_"))
247 false bdvs (num_str @{separate_bdvs_add) t;
248 (writeln o UnparseC.term2str) t;
249 if UnparseC.term2str t = "L * c_3 + c_4 = 0 + -1 * (-1 * (q_0 * L ^^^ 2) / 2)"
250 then () else error "rewrite.sml rewrite_inst_ bdvs";
251 > trace_rewrite:=true;
252 trace_rewrite:=false;--------------------------------------------*)
255 "----------- check diff 2002--2009-3 --------------------";
256 "----------- check diff 2002--2009-3 --------------------";
257 "----------- check diff 2002--2009-3 --------------------";
258 (*----- 2002 -------------------------------------------------------------------
259 # rls: norm_Rational_noadd_fractions on: 1 / EI * (L * q_0 * x / 2 + -1 *
261 ## rls: discard_minus_ on: 1 / EI * (L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2
263 ### try thm: real_diff_minus
264 ### try thm: sym_real_mult_minus1
265 ## rls: rat_mult_poly on: 1 / EI * (L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2
267 ### try thm: rat_mult_poly_l
268 ### try thm: rat_mult_poly_r
269 #### eval asms: L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2 is_polyexp
270 ==> 1 / EI * (L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2) =
271 1 * (L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2) / EI
272 ##### rls: Rule_Set.empty-is_polyexp on: L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2
274 ###### try calc: Poly.is'_polyexp'
275 ====== calc. to: False
276 ###### try calc: Poly.is'_polyexp'
277 ###### try calc: Poly.is'_polyexp'
278 #### asms false: ["L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2 is_polyexp"]
279 ----- 2002 NONE rewrite --------------------------------------------------------
280 ----- 2009 should maintain this behaviour, but: --------------------------------
281 # rls: norm_Rational_noadd_fractions on: 1 / EI * (L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2)
282 ## rls: discard_minus on: 1 / EI * (L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2)
283 ### try thm: real_diff_minus
284 ### try thm: sym_real_mult_minus1
285 ## rls: rat_mult_poly on: 1 / EI * (L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2)
286 ### try thm: rat_mult_poly_l
287 ### try thm: rat_mult_poly_r
288 #### eval asms: L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2 is_polyexp
289 ==> 1 / EI * (L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2) =
290 1 * (L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2) / EI
291 ##### rls: Rule_Set.empty-is_polyexp on: L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2 is_polyexp
292 ###### try calc: Poly.is'_polyexp'
293 ====== calc. to: False
294 ###### try calc: Poly.is'_polyexp'
295 ###### try calc: Poly.is'_polyexp'
296 #### asms accepted: ["L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2 is_polyexp"] stored: ["False"]
297 === rewrites to: 1 * (L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2) / EI
298 ----- 2009 -------------------------------------------------------------------*)
300 (*the situation as was before repair (asm without Trueprop) is outcommented*)
301 val thy = @{theory "Isac_Knowledge"};
302 "===== example which raised the problem =================";
303 val t = @{term "1 / EI * (L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2)"};
304 "----- rewrite_set_inst_ norm_Rational_noadd_fractions--";
305 val subs = [(@{term "bdv"}, @{term "x"})];
306 val rls = norm_Rational_noadd_fractions;
307 val SOME (t', asms) = rewrite_set_inst_ thy true subs rls t;
308 if UnparseC.term2str t' = "1 / EI * (L * q_0 * x / 2 + -1 * q_0 * 1 * x ^^^ 2 / 2)" andalso
309 UnparseC.terms2str asms = "[]" then {}
310 else error "this was NONE with Isabelle2013-2 ?!?"
311 "----- rewrite_ rat_mult_poly_r--------------------------";
312 val thm = @{thm rat_mult_poly_r};
313 "?c::real is_polyexp ==> (?a::real) / (?b::real) * ?c = ?a * ?c / ?b";
314 val erls = Rule_Set.append_rules "Rule_Set.empty-is_polyexp" Rule_Set.empty
315 [Num_Calc ("Poly.is'_polyexp", eval_is_polyexp "")];
316 val NONE (*SOME (t'', _)*) = rewrite_ thy dummy_ord erls true thm t;
317 (*t' = t''; (*false because of further rewrites in t'*)*)
318 "----- rew_sub --------------------------------";
319 val (t''', _, _, _) = rew_sub thy 0 [] dummy_ord erls true [] (Thm.prop_of thm) t;
320 (*t'' = t'''; (*true*)*)
321 "----- rewrite_set_ erls --------------------------------";
322 val cond = @{term "(L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2)"};
323 val NONE = rewrite_set_ thy true erls cond;
324 (* ^^^^^ goes with '====== calc. to: False' above from beginning*)
326 writeln "===== maximally simplified example =====================";
327 val t = @{term "a / b * (x / x ^^^ 2)"};
328 "?c::real is_polyexp ==> (?a::real) / (?b::real) * ?c = ?a * ?c / ?b";
329 writeln "----- rewrite_set_inst_ norm_Rational_noadd_fractions--";
330 val (*NONE*) SOME (t', asm) = rewrite_set_inst_ thy true subs rls t;
331 UnparseC.term2str t' = "a * x / (b * x ^^^ 2)"; (*rew. by thm outside test case*)
332 (*checked visually: trace_rewrite looks like above for 2009*)
334 writeln "----- rewrite_ rat_mult_poly_r--------------------------";
335 val NONE (*SOME (t'', _)*) = rewrite_ thy dummy_ord erls true thm t;
336 (*t' = t''; (*false because of further rewrites in t'*)*)
337 writeln "----- rew_sub --------------------------------";
338 val (t''', _, _, _) = rew_sub thy 0 [] dummy_ord erls true [] (Thm.prop_of thm) t;
339 (*t'' = t'''; (*true*)*)
340 writeln "----- rewrite_set_ erls --------------------------------";
341 val cond = @{term "(x / x ^^^ 2)"};
342 val NONE = rewrite_set_ thy true erls cond;
343 (* ^^^^^ goes with '====== calc. to: False' above from beginning*)
346 "----------- compare all prepat's existing 2010 ---------";
347 "----------- compare all prepat's existing 2010 ---------";
348 "----------- compare all prepat's existing 2010 ---------";
349 val thy = @{theory "Isac_Knowledge"};
350 val t = @{term "a + b * x = (0 ::real)"};
351 val pat = parse_patt thy "?l = (?r ::real)";
352 val precond = parse_patt thy "is_polynomial (?l::real)";(*no infix def*)
353 val precond = parse_patt thy "(?l::real) is_expanded";
355 val inst = Pattern.match thy (pat, t) (Vartab.empty, Vartab.empty);
356 val preinst = Envir.subst_term inst precond;
357 UnparseC.term2str preinst;
359 "===== Rational.thy: cancel ===";
360 (* pat matched with the current term gives an environment
361 (or not: hen the Rrls not applied);
362 if pre1 and pre2 evaluate to @{term True} in this environment,
363 then the Rrls is applied. *)
364 val t = str2term "(a + b) / c ::real";
365 val pat = parse_patt thy "?r / ?s ::real";
366 val pres = [parse_patt thy "?r is_expanded", parse_patt thy "?s is_expanded"];
367 val prepat = [(pres, pat)];
368 val erls = rational_erls;
369 (* erls got from Rrls {erls, prepat, scr = Rfuns {normal_form, ...}, ...} *)
371 val subst = Pattern.match thy (pat, t) (Vartab.empty, Vartab.empty);
372 val asms = map (Envir.subst_term subst) pres;
373 if UnparseC.terms2str asms = "[\"a + b is_expanded\",\"c is_expanded\"]"
374 then () else error "rewrite.sml: prepat cancel subst";
375 if ([], true) = eval__true thy 0 asms [] erls
376 then () else error "rewrite.sml: prepat cancel eval__true";
378 "===== Rational.thy: add_fractions_p ===";
379 (* if each pat* matches with the current term, the Rrls is applied
380 (there are no preconditions to be checked, they are @{term True}) *)
381 val t = str2term "a / b + 1 / 2";
382 val pat = parse_patt thy "?r / ?s + ?u / ?v";
383 val pres = [@{term True}];
384 val prepat = [(pres, pat)];
385 val erls = rational_erls;
386 (* erls got from Rrls {erls, prepat, scr = Rfuns {normal_form, ...}, ...} *)
388 val subst = Pattern.match thy (pat, t) (Vartab.empty, Vartab.empty);
389 if ([], true) = eval__true thy 0 (map (Envir.subst_term subst) pres) [] erls
390 then () else error "rewrite.sml: prepat add_fractions_p";
392 "===== Poly.thy: order_mult_ ===";
393 (* ?p matched with the current term gives an environment,
394 which evaluates (the instantiated) "p is_multUnordered" to true*)
395 val t = str2term "x^^^2 * x";
396 val pat = parse_patt thy "?p :: real"
397 val pres = [parse_patt thy "?p is_multUnordered"];
398 val prepat = [(pres, pat)];
399 val erls = Rule_Set.append_rules "Rule_Set.empty-is_multUnordered" Rule_Set.empty
400 [Num_Calc ("Poly.is'_multUnordered",
401 eval_is_multUnordered "")];
403 val subst = Pattern.match thy (pat, t) (Vartab.empty, Vartab.empty);
404 val asms = map (Envir.subst_term subst) pres;
405 if UnparseC.terms2str asms = "[\"x ^^^ 2 * x is_multUnordered\"]"
406 then () else error "rewrite.sml: prepat order_mult_ subst";
407 if ([], true) = eval__true thy 0 asms [] erls
408 then () else error "rewrite.sml: prepat order_mult_ eval__true";
411 "----------- fun app_rev, Rrls, -------------------------";
412 "----------- fun app_rev, Rrls, -------------------------";
413 "----------- fun app_rev, Rrls, -------------------------";
414 val t = str2term "x^^^2 * x";
416 if is_multUnordered t then () else error "rewrite.sml diff. is_multUnordered 2";
417 val tm = str2term "(x^^^2 * x) is_multUnordered";
418 eval_is_multUnordered "testid" "" tm thy;
420 case eval_is_multUnordered "testid" "" tm thy of
421 SOME (_, Const ("HOL.Trueprop", _) $
422 (Const ("HOL.eq", _) $
423 (Const ("Poly.is'_multUnordered", _) $ _) $
424 Const ("HOL.True", _))) => ()
425 | _ => error "rewrite.sml diff. eval_is_multUnordered 2b";
427 tracing "----- begin rewrite x^^^2 * x ---"; trace_rewrite := false;
428 val SOME (t', _) = rewrite_set_ thy true order_mult_ t;
429 tracing "----- end rewrite x^^^2 * x ---"; trace_rewrite := false;
430 if UnparseC.term2str t' = "x * x ^^^ 2" then ()
431 else error "rewrite.sml Poly.is'_multUnordered doesn't work";
433 (* for achieving the previous result, the following code was taken apart *)
434 "----- rewrite__set_ ---";
435 val (thy, i, _, _, (rrls as Rrls _), t) = (thy, 0, true, [], order_mult_, tm);
436 val (t', asm, rew) = app_rev thy (i+1) rrls t;
438 val (thy, i, rrls, t) = (thy, (i+1), rrls, t);
439 fun chk_prepat thy erls [] t = true
440 | chk_prepat thy erls prepat t =
441 let fun chk (pres, pat) =
442 (let val subst: Type.tyenv * Envir.tenv =
443 Pattern.match thy (pat, t)
444 (Vartab.empty, Vartab.empty)
445 in snd (eval__true thy (i+1)
446 (map (Envir.subst_term subst) pres)
450 fun scan_ f [] = false (*scan_ NEVER called by []*)
451 | scan_ f (pp::pps) = if f pp then true
453 in scan_ chk prepat end;
455 (*.apply the normal_form of a rev-set.*)
456 fun app_rev' thy (Rrls{erls,prepat,scr=Rfuns{normal_form,...},...}) t =
457 if chk_prepat thy erls prepat t
458 then ((*tracing("### app_rev': t = "^(UnparseC.term2str t));*)
461 (*fixme val NONE = app_rev' thy rrls t;*)
462 "----- app_rev' ---";
463 val (thy, Rrls{erls,prepat,scr=Rfuns{normal_form,...},...}, t) = (thy, rrls, t);
464 (*fixme false*) chk_prepat thy erls prepat t;
465 "----- chk_prepat ---";
466 val (thy, erls, prepat, t) = (thy, erls, prepat, t);
467 fun chk (pres, pat) =
468 (let val subst: Type.tyenv * Envir.tenv =
469 Pattern.match thy (pat, t)
470 (Vartab.empty, Vartab.empty)
471 in snd (eval__true thy (i+1)
472 (map (Envir.subst_term subst) pres)
476 fun scan_ f [] = false (*scan_ NEVER called by []*)
477 | scan_ f (pp::pps) = if f pp then true
479 tracing "=== poly.sml: scan_ chk prepat begin";
481 tracing "=== poly.sml: scan_ chk prepat end";
484 (*reestablish...*) val t = str2term "x ^^^ 2 * x";
485 val [(pres, pat)] = prepat;
486 val subst: Type.tyenv * Envir.tenv =
487 Pattern.match thy (pat, t)
488 (Vartab.empty, Vartab.empty);
490 (*fixme: asms = ["p is_multUnordered"]...instantiate*)
491 "----- eval__true ---";
492 val asms = (map (Envir.subst_term subst) pres);
493 if UnparseC.terms2str asms = "[\"x ^^^ 2 * x is_multUnordered\"]" then ()
494 else error "rewrite.sml: diff. is_multUnordered, asms";
495 val (thy, i, asms, bdv, rls) =
496 (thy, (i+1), [str2term "(x^^^2 * x) is_multUnordered"],
497 [] : (term * term) list, erls);
498 case eval__true thy i asms bdv rls of
500 | _ => error "rewrite.sml: diff. is_multUnordered, eval__true";
502 "----------- 2011 thms with axclasses -------------------";
503 "----------- 2011 thms with axclasses -------------------";
504 "----------- 2011 thms with axclasses -------------------";
505 val thm = num_str @{thm div_by_1};
506 val prop = Thm.prop_of thm;
507 atomty prop; (*Type 'a*)
508 val t = str2term "(2*x)/1"; (*Type real*)
510 val (thy, ro, er, inst) =
511 (@{theory "Isac_Knowledge"}, tless_true, eval_rls, [(@{term "bdv::real"}, @{term "x::real"})]);
512 val SOME (t, _) = rewrite_ thy ro er true thm t; (*real matches 'a ?via ring? etc*)
514 "----------- fun rewrite_set_ .. RatEq_eliminate step into to fun chk --------------------------";
515 "----------- fun rewrite_set_ .. RatEq_eliminate step into to fun chk --------------------------";
516 "----------- fun rewrite_set_ .. RatEq_eliminate step into to fun chk --------------------------";
517 val thy = @{theory RatEq};
518 val ctxt = Proof_Context.init_global thy;
519 val SOME t = parseNEW ctxt "(3 + -1 * x + x ^^^ 2) / (9 * x + -6 * x ^^^ 2 + x ^^^ 3) = 1 / x";
520 val rls = assoc_rls "RatEq_eliminate"
522 val SOME (t''''', asm''''') =
523 rewrite_set_ thy true rls t;
524 "~~~~~ fun rewrite_set_ , args:"; val (thy, bool, rls, term) = (thy, true, rls, t);
525 rewrite__set_ thy 1 bool [] rls term;
526 "~~~~~ and rewrite__set_ , args:"; val (thy, i, put_asm, bdv, rls, ct)
527 = (thy, 1, bool, []:(term * term) list, rls, term);
529 (*/------- outcomment this code: otherwise the re-definition could infect tests lateron ------\ * )
530 datatype switch = Appl | Noap;
531 fun rew_once _ asm ct Noap [] = (ct, asm) (* ?TODO unify with Prog_Expr.rew_once? *)
532 | rew_once ruls asm ct Appl [] =
533 (case rls of Rule_Set.Repeat _ => rew_once ruls asm ct Noap ruls
534 | Rule_Set.Seqence _ => (ct, asm)
535 | rls => raise ERROR ("rew_once not appl. to \"" ^ Rule.rls2str rls ^ "\""))
536 | rew_once ruls asm ct apno (rul :: thms) =
538 Rule.Thm (thmid, thm) =>
539 (trace1 i (" try thm: " ^ thmid);
540 case rewrite__ thy (i + 1) bdv ((snd o #rew_ord o Rule.Rule_Set.rep) rls)
541 ((#erls o Rule.Rule_Set.rep) rls) put_asm thm ct of
542 NONE => rew_once ruls asm ct apno thms
543 | SOME (ct', asm') =>
544 (trace1 i (" rewrites to: " ^ UnparseC.t2str thy ct');
545 rew_once ruls (union (op =) asm asm') ct' Appl (rul :: thms)))
546 (* once again try the same rule, e.g. associativity against "()"*)
547 | Rule.Num_Calc (cc as (op_, _)) =>
548 let val _= trace1 i (" try calc: " ^ op_ ^ "'")
549 val ct = TermC.uminus_to_string ct (*WN190312: superfluous?*)
550 in case Num_Calc.adhoc_thm thy cc ct of
551 NONE => rew_once ruls asm ct apno thms
554 val pairopt = rewrite__ thy (i + 1) bdv ((snd o #rew_ord o Rule.Rule_Set.rep) rls)
555 ((#erls o Rule.Rule_Set.rep) rls) put_asm thm' ct;
556 val _ = if pairopt <> NONE then () else error ("rewrite_set_, rewrite_ \"" ^
557 Rule.string_of_thmI thm' ^ "\" " ^ UnparseC.t2str thy ct ^ " = NONE")
558 val _ = trace1 i (" calc. to: " ^ UnparseC.t2str thy ((fst o the) pairopt))
559 in rew_once ruls asm ((fst o the) pairopt) Appl (rul :: thms) end
561 | Rule.Cal1 (cc as (op_, _)) =>
562 let val _= trace1 i (" try cal1: " ^ op_ ^ "'");
563 val ct = TermC.uminus_to_string ct
564 in case Num_Calc.adhoc_thm1_ thy cc ct of
568 val pairopt = rewrite__ thy (i + 1) bdv ((snd o #rew_ord o Rule.Rule_Set.rep) rls)
569 ((#erls o Rule.Rule_Set.rep) rls) put_asm thm' ct;
570 val _ = if pairopt <> NONE then () else error ("rewrite_set_, rewrite_ \"" ^
571 Rule.string_of_thmI thm' ^ "\" " ^ UnparseC.t2str thy ct ^ " = NONE")
572 val _ = trace1 i (" cal1. to: " ^ UnparseC.t2str thy ((fst o the) pairopt))
576 (case rewrite__set_ thy (i + 1) put_asm bdv rls' ct of
577 SOME (t', asm') => rew_once ruls (union (op =) asm asm') t' Appl thms
578 | NONE => rew_once ruls asm ct apno thms)
579 | r => raise ERROR ("rew_once not appl. to \"" ^ Rule.rule2str r ^ "\"");
580 val ruls = (#rules o Rule.Rule_Set.rep) rls;
581 (* val _ = trace i (" rls: " ^ Rule_Set.rls2str rls ^ " on: " ^ UnparseC.t2str thy ct)*)
582 val (ct', asm') = rew_once ruls [] ct Noap ruls;
583 "~~~~~ fun rew_once , args:"; val (ruls, asm, ct, apno, (rul :: thms))
584 = (ruls, []:term list, ct, Noap, ruls);
585 val Rule.Thm (thmid, thm) = (*case*) rul (*of*);
587 val SOME (ct', asm') = (*case*)
588 rewrite__ thy (i + 1) bdv ((snd o #rew_ord o Rule.Rule_Set.rep) rls)
589 ((#erls o Rule.Rule_Set.rep) rls) put_asm thm ct (*of*);
590 "~~~~~ fun rewrite__ , args:"; val (thy, i, bdv, tless, rls, put_asm, thm, ct)
591 = (thy, (i + 1), bdv, ((snd o #rew_ord o Rule.Rule_Set.rep) rls),
592 ((#erls o Rule.Rule_Set.rep) rls), put_asm, thm, ct);
594 val (t', asms, _ (*lrd*), rew) =
595 rew_sub thy i bdv tless rls put_asm ([(*root of the term*)]: TermC.path)
596 (((TermC.inst_bdv bdv) o Num_Calc.norm o #prop o Thm.rep_thm) thm) ct;
597 "~~~~~ and rew_sub , args:"; val (thy, i, bdv, tless, rls, put_asm, lrd, r, t)
598 = (thy, i, bdv, tless, rls, put_asm, ([(*root of the term*)]: TermC.path),
599 (((TermC.inst_bdv bdv) o Num_Calc.norm o #prop o Thm.rep_thm) thm), ct);
600 val (lhs, rhs) = (HOLogic.dest_eq o HOLogic.dest_Trueprop o Logic.strip_imp_concl) r
601 val r' = Envir.subst_term (Pattern.match thy (lhs, t) (Vartab.empty, Vartab.empty)) r
603 (*+*)if UnparseC.term2str r' =
604 (*+*) "\<lbrakk>9 * x + -6 * x ^^^ 2 + x ^^^ 3 \<noteq> 0; x \<noteq> 0\<rbrakk>\n" ^
605 (*+*) "\<Longrightarrow> ((3 + -1 * x + x ^^^ 2) /\n" ^
606 (*+*) " (9 * x + -6 * x ^^^ 2 + x ^^^ 3) =\n" ^
607 (*+*) " 1 / x) =\n" ^
608 (*+*) " ((3 + -1 * x + x ^^^ 2) * x =\n" ^
609 (*+*) " 1 * (9 * x + -6 * x ^^^ 2 + x ^^^ 3))"
610 (*+*)then () else error "instantiated rule CHANGED";
612 val p' = map HOLogic.dest_Trueprop ((fst o Logic.strip_prems) (Logic.count_prems r', [], r'))
614 (*+*)if map UnparseC.term2str p' = ["x \<noteq> 0", "9 * x + -6 * x ^^^ 2 + x ^^^ 3 \<noteq> 0"]
615 (*+*)then () else error "stored assumptions CHANGED";
617 val t' = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop o Logic.strip_imp_concl) r'
619 (*+*)if UnparseC.term2str t' = "(3 + -1 * x + x ^^^ 2) * x = 1 * (9 * x + -6 * x ^^^ 2 + x ^^^ 3)"
620 (*+*)then () else error "rewritten term (an equality) CHANGED";
622 val (simpl_p', nofalse) =
623 eval__true thy (i + 1) p' bdv rls;
624 "~~~~~ and eval__true , args:"; val (thy, i, asms, bdv, rls) = (thy, (i + 1), p', bdv, rls);
625 (*if*) asms = [@{term True}] orelse asms = [] (*else*);
627 (*+*)if map UnparseC.term2str asms = ["x \<noteq> 0", "9 * x + -6 * x ^^^ 2 + x ^^^ 3 \<noteq> 0"]
628 (*+*)then () else error "asms before chk CHANGED";
630 fun chk indets [] = (indets, true) (*return asms<>True until false*)
631 | chk indets (a :: asms) =
632 (case rewrite__set_ thy (i + 1) false bdv rls a of
633 NONE => (chk (indets @ [a]) asms)
635 if t = @{term True} then (chk (indets @ a') asms)
636 else if t = @{term False} then ([], false)
637 (*asm false .. thm not applied ^^^; continue until False vvv*)
638 else chk (indets @ [t] @ a') asms);
641 chk [] asms; (*return from eval__true*);
642 "~~~~~ fun chk , args:"; val (indets, (a :: asms)) = ([], asms);
644 (*+*)val Rule_Set.Repeat {id = "rateq_erls", rules, ...} = rls;
646 (*+*) [Num_Calc ("Rings.divide_class.divide", fn),
647 (*+*) Thm ("minus_divide_left", "- ?a1 / ?b1 = - (?a1 / ?b1)"),
649 (*+*) Num_Calc ("HOL.eq", fn),
650 (*+*) Thm ("not_true", "(\<not> True) = False"),
651 (*+*) Thm ("not_false", "(\<not> False) = True"),
653 (*+*) Num_Calc ("Prog_Expr.pow", fn),
654 (*+*) Num_Calc ("RatEq.is'_ratequation'_in", fn)]:
656 (*+*)chk: term list -> term list -> term list * bool
658 rewrite__set_ thy (i + 1) false bdv rls a (*of*);
660 (*+*)trace_rewrite := true;
662 (*this was False; vvvv--- means: indeterminate*)
663 val (* SOME (t, a') *)NONE = (*case*)
664 rewrite__set_ thy (i + 1) false bdv rls a (*of*);
666 (*+*)UnparseC.term2str a = "x \<noteq> 0"; (* rewrite__set_ \<rightarrow> @{term True} ----------------- SHOULD BE indet !*)
669 #### rls: rateq_erls on: x \<noteq> 0
671 ##### try calc: HOL.eq' <<<------------------------------- here the error comes from
672 ===== calc. to: ~ False <<<------------------------------- \<not> x = 0 is NOT False
673 ##### try calc: HOL.eq'
674 ##### try thm: not_true
675 ##### try thm: not_false
676 ===== rewrites to: True <<<------------------------------- so x \<noteq> 0 is NOT True
677 and True, False are NOT stored ...
679 ### asms accepted: [x \<noteq> 0] stored: []
681 trace_rewrite := false;
682 ( *\------- outcomment this code: otherwise the re-definition could infect tests lateron ------/*)
685 "----------- fun assoc_thm' -----------------------------";
686 "----------- fun assoc_thm' -----------------------------";
687 "----------- fun assoc_thm' -----------------------------";
688 val thy = @{theory ProgLang}
690 val tth = assoc_thm' thy ("sym_#mult_2_3","6 = 2 * 3");
691 if string_of_thm' thy tth = "6 = 2 * 3" then ()
692 else error "assoc_thm' (sym_#mult_2_3, 6 = 2 * 3) changed";
694 val tth = assoc_thm' thy ("add_0_left","");
695 if string_of_thm' thy tth = "0 + ?a = ?a" then ()
696 else error "assoc_thm' (add_0_left,\"\") changed";
698 val tth = assoc_thm' thy ("sym_add_0_left","");
699 if string_of_thm' thy tth = "?t = 0 + ?t" then ()
700 else error "assoc_thm' (sym_add_0_left,\"\") changed";
702 val tth = assoc_thm' thy ("add_commute","");
703 if string_of_thm' thy tth = "?a + ?b = ?b + ?a" then ()
704 else error "assoc_thm' (add_commute,\"\") changed"
706 "----------- fun rewrite_ down to Pattern.match ------------------------------------------------";
707 "----------- fun rewrite_ down to Pattern.match ------------------------------------------------";
708 "----------- fun rewrite_ down to Pattern.match ------------------------------------------------";
709 "~~~~~ fun rewrite_ , args:"; val (thy, rew_ord, erls, bool, thm, term) =
710 (@{theory}, dummy_ord, Rule_Set.empty, false, @{thm distrib_left}, @{term "x * (y + z) :: int"});
711 "~~~~~ fun rewrite__ , args:"; val (thy, i, bdv, tless, rls, put_asm, thm, ct) =
712 (thy, 1, [], rew_ord, erls, bool, thm, term);
713 "~~~~~ and rew_sub , args:"; val (thy, i, bdv, tless, rls, put_asm, lrd, r, t) =
714 (thy, i, bdv, tless, rls, put_asm, [], (((inst_bdv bdv) o norm o #prop o Thm.rep_thm) thm), ct)
715 val (lhss, rhss) = (HOLogic.dest_eq o HOLogic.dest_Trueprop o Logic.strip_imp_concl) r
716 val r' = Envir.subst_term (Pattern.match thy (lhss, t) (Vartab.empty, Vartab.empty)) r
717 val p' = map HOLogic.dest_Trueprop ((fst o Logic.strip_prems) (Logic.count_prems r', [], r'))
718 val t' = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop o Logic.strip_imp_concl) r'
720 if UnparseC.term2str lhss = "?a * (?b + ?c)" andalso UnparseC.term2str t = "x * (y + z)" then ()
721 else error "ARGS FOR Pattern.match CHANGED";
722 val match = Pattern.match thy (lhss, t) (Vartab.empty, Vartab.empty);
723 if (Envir.subst_term match r |> UnparseC.term2str) = "x * (y + z) = x * y + x * z" then ()
724 else error "Pattern.match CHANGED";
726 "----------- fun mk_thm ------------------------------------------------------------------------";
727 "----------- fun mk_thm ------------------------------------------------------------------------";
728 "----------- fun mk_thm ------------------------------------------------------------------------";
729 val thy = @{theory Isac_Knowledge}
731 (*~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~*)
732 val thm = @{thm realpow_twoI};
733 val patt_str = "?r ^^^ 2 = ?r * ?r";
734 val term_str = "r ^^^ 2 = r * r";
735 (*~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~*)
736 case parse_patt thy patt_str of
737 Const ("HOL.eq", _) $ (Const ("Prog_Expr.pow", _) $ Var (("r", 0), _) $ Free ("2", _)) $
738 (Const ("Groups.times_class.times", _) $ Var (("r", 0), _) $ Var (("r", 0), _)) => ()
739 | _ => error "parse_patt ?r ^^^ 2 = ?r * ?r changed";
740 case parse thy term_str of
742 | _ => writeln "parse does NOT take patterns with '?'";
744 val t1 = (#prop o Thm.rep_thm) (num_str thm);
745 if UnparseC.term2str t1 = patt_str then () else error "realpow_twoI (\<rightarrow> string) NOT equal to given string";
747 val t2 = HOLogic.Trueprop $ (((parse_patt thy)) patt_str) : term;
748 if t1 = t2 then () else error "prop of realpow_twoI NOT equal to parsed string";
750 (mk_thm thy patt_str) handle _ => mk_thm thy "mk_thm = does NOT handle patterns";
751 (*and this*) mk_thm thy term_str (* = "r ^^^ 2 = r * r" [.]: thm
752 gives a strange thm*);
754 val thm_made = Thm.make_thm (Thm.global_cterm_of thy t2) (* = "?r ^^^ 2 = ?r * ?r" [.]: thm
755 ..gives another strange thm; but it is used and works with rewriting: *);
757 val t1' = (#prop o Thm.rep_thm) (num_str thm_made);
758 if t1 = t1' then () else error "prop of realpow_twoI NOT equal to thm_made from string";
760 (*~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~*)
761 val thm = @{thm real_mult_div_cancel2};
762 val patt_str = "?k \<noteq> 0 \<Longrightarrow> ?m * ?k / (?n * ?k) = ?m / ?n";
763 val term_str = "k \<noteq> 0 \<Longrightarrow> m * k / (n * k) = m / n";
764 (*~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~*)
765 case parse_patt thy patt_str of
766 Const ("Pure.imp", _) $
767 (Const ("HOL.Trueprop", _) $ (Const ("HOL.Not", _) $
768 (Const ("HOL.eq", _) $ Var (("k", 0), _) $ Free ("0", _)))) $
769 (Const ("HOL.Trueprop", _) $
770 (Const ("HOL.eq", _) $ _ $ _ )) => ()
771 | _ => error "parse_patt ?k \<noteq> 0 ==> ?m * ?k / (?n * ?k) = ?m / ?n changed";
772 case parse thy term_str of
774 | _ => writeln "parse does NOT take patterns with '?'";
776 val t1 = (#prop o Thm.rep_thm) (num_str thm);
777 if UnparseC.term2str t1 = patt_str then () else error "realpow_twoI (\<rightarrow> string) NOT equal to given string";
779 val t2 = (*Trueprop $*) (((parse_patt thy)) patt_str) : term;
780 if t1 = t2 then () else error "prop of realpow_twoI NOT equal to parsed string";
782 (mk_thm thy patt_str) handle _ => mk_thm thy "mk_thm = does NOT handle patterns";
783 (*and this*) mk_thm thy term_str (* = "r ^^^ 2 = r * r" [.]: thm
784 gives a strange thm*);
786 val thm_made = Thm.make_thm (Thm.global_cterm_of thy t2) (* = "?r ^^^ 2 = ?r * ?r" [.]: thm
787 gives another strange thm; but it is used and words with rewriting: *);
789 val t1' = (#prop o Thm.rep_thm) (num_str thm_made);
790 if t1 = t1' then () else error "prop of realpow_twoI NOT equal to thm_made from string";
792 "----------- fun rewrite_set_ .. norm_equation -------------------------------------------------";
793 "----------- fun rewrite_set_ .. norm_equation -------------------------------------------------";
794 "----------- fun rewrite_set_ .. norm_equation -------------------------------------------------";
795 (* norm_equation is defined in Test.thy, other rls see Knowledg/**)
797 val rls = norm_equation;
798 val term = str2term "x + 1 = 2";
800 val SOME (t, asm) = rewrite_set_ thy false rls term;
801 if UnparseC.term2str t = "x + 1 + -1 * 2 = 0" then () else error "rewrite_set_ norm_equation CHANGED";
803 "~~~~~ fun rewrite_set_, args:"; val (thy, bool, rls, term) = (thy, false, rls, term);
804 "~~~~~ fun rewrite__set_, args:"; val (thy, i, put_asm, bdv, rls, ct) = (thy, 1, bool, [], rls, term);