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 rewrite_ down to Pattern.match ------------------------------------------------";
21 "----------- fun rewrite_set_ .. norm_equation -------------------------------------------------";
22 "----------- fun rewrite_set_ .. RatEq_eliminate step into to fun chk --------------------------";
23 "--------------------------------------------------------";
24 "--------------------------------------------------------";
25 "--------------------------------------------------------";
28 "----------- assemble rewrite ---------------------------";
29 "----------- assemble rewrite ---------------------------";
30 "----------- assemble rewrite ---------------------------";
31 "===== rewriting by thm with 'a";
32 (*show_types := true;*)
34 val thy = @{theory Complex_Main};
35 val ctxt = @{context};
36 val thm = @{thm add.commute};
37 val t = (Thm.term_of o the) (TermC.parse thy "((r + u) + t) + s");
38 "----- from old: fun rewrite__";
40 val r = TermC.inst_bdv bdv (Eval.norm (Thm.prop_of thm));
41 "----- from old: and rew_sub";
42 val (LHS,RHS) = (dest_equals o strip_trueprop
43 o Logic.strip_imp_concl) r;
45 val insts = Pattern.match thy (LHS,t) (Vartab.empty, Vartab.empty);*)
46 "----- fun match_rew in Pure/pattern.ML";
47 val rtm = the_default RHS (Term.rename_abs LHS t RHS);
49 writeln(Syntax.string_of_term ctxt rtm);
50 writeln(Syntax.string_of_term ctxt LHS);
51 writeln(Syntax.string_of_term ctxt t);
53 (Pattern.match thy (LHS, t) (Vartab.empty, Vartab.empty));
54 val (rew, RHS) = (Envir.subst_term
55 (Pattern.match thy (LHS, t) (Vartab.empty, Vartab.empty)) rtm, rtm);
56 (*lookup in isabelle?trace?response...*)
57 writeln(Syntax.string_of_term ctxt rew);
58 writeln(Syntax.string_of_term ctxt RHS);
59 "===== rewriting: prep insertion into rew_sub";
60 val thy = @{theory Complex_Main};
61 val ctxt = @{context};
62 val thm = @{thm nonzero_divide_mult_cancel_right};
63 val r = Thm.prop_of thm;
64 val tm = @{term "x / (2 * x)::real"};
66 val (LHS, RHS) = (HOLogic.dest_eq o HOLogic.dest_Trueprop
67 o Logic.strip_imp_concl) r;
68 val r' = Envir.subst_term (Pattern.match thy (LHS, tm)
69 (Vartab.empty, Vartab.empty)) r;
70 val p' = (fst o Logic.strip_prems) (Logic.count_prems r', [], r');
71 val t' = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop
72 o Logic.strip_imp_concl) r';
74 (*is displayed on top of <response> buffer...*)
75 Pretty.writeln (Proof_Context.pretty_term_abbrev @{context} r');
76 Pretty.writeln (Proof_Context.pretty_term_abbrev @{context} t');
79 "----------- test rewriting without Isac's thys ---------";
80 "----------- test rewriting without Isac's thys ---------";
81 "----------- test rewriting without Isac's thys ---------";
83 "===== rewriting with Isabelle2009-1 only, i.e without isac-hacks";
84 val thy = @{theory Complex_Main};
85 val ctxt = @{context};
86 val thm = @{thm add.commute};
87 val tm = @{term "x + y*z::real"};
89 val SOME (r,_) = (rewrite_ thy dummy_ord Rule_Set.empty false thm tm)
90 handle _ => error "rewrite.sml diff.behav. in rewriting";
91 (*is displayed on _TOP_ of <response> buffer...*)
92 Pretty.writeln (Proof_Context.pretty_term_abbrev @{context} r);
93 if r = @{term "y*z + x::real"}
94 then () else error "rewrite.sml diff.result in rewriting";
96 "----- rewriting a subterm";
97 val tm = @{term "w*(x + y*z)::real"};
99 val SOME (r,_) = (rewrite_ thy dummy_ord Rule_Set.empty false thm tm)
100 handle _ => error "rewrite.sml diff.behav. in rew_sub";
102 "----- ordered rewriting";
103 fun tord (_:subst) pp = LibraryC.termless pp;
104 if tord [] (@{term "x + y*z::real"}, @{term "y*z + x::real"}) then ()
105 else error "rewrite.sml diff.behav. in ord.rewr.";
107 val NONE = (rewrite_ thy tord Rule_Set.empty false thm tm)
108 handle _ => error "rewrite.sml diff.behav. in rewriting";
109 (*is displayed on _TOP_ of <response> buffer...*)
110 Pretty.writeln (Proof_Context.pretty_term_abbrev @{context} r);
112 val tm = @{term "x*y + z::real"};
113 val SOME (r,_) = (rewrite_ thy tord Rule_Set.empty false thm tm)
114 handle _ => error "rewrite.sml diff.behav. in rewriting";
117 "----------- conditional rewriting without Isac's thys --";
118 "----------- conditional rewriting without Isac's thys --";
119 "----------- conditional rewriting without Isac's thys --";
121 "===== prepr cond.rew. with Pattern.match";
122 val thy = @{theory Complex_Main};
123 val ctxt = @{context};
124 val thm = @{thm nonzero_divide_mult_cancel_right};
125 val rule = Thm.prop_of thm;
126 val tm = @{term "x / (2 * x)::real"};
128 val prem = Logic.strip_imp_prems rule;
129 val nps = Logic.count_prems rule;
130 val prems = Logic.strip_prems (nps, [], rule);
132 val eq = Logic.strip_imp_concl rule;
133 val (LHS, RHS) = (HOLogic.dest_eq o HOLogic.dest_Trueprop) eq;
135 val mtcs = Pattern.match thy (LHS, tm) (Vartab.empty, Vartab.empty);
136 val rule' = Envir.subst_term mtcs rule;
138 val prems' = (fst o Logic.strip_prems)
139 (Logic.count_prems rule', [], rule');
140 val RHS' = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop
141 o Logic.strip_imp_concl) rule';
143 "----- conditional rewriting creating an assumption";
144 "----- conditional rewriting creating an assumption";
145 val thm = @{thm nonzero_divide_mult_cancel_right};
146 val tm = @{term "x / (2 * x)::real"};
147 val SOME (rew, asm) = (rewrite_ thy dummy_ord Rule_Set.empty false thm tm)
148 handle _ => error "rewrite.sml diff.behav. in cond.rew.";
150 if rew = @{term "1 / 2::real"} then () (* the rewrite is _NO_ Trueprop *)
151 else error "rewrite.sml diff.result in cond.rew.";
153 if hd asm = @{term "x \<noteq> (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 / (2 * x)::real"};
164 val (t', asm, _, _) = rew_sub thy 0 [] dummy_ord Rule_Set.empty true [] (Thm.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, Rule_Set.empty, true, [], (Thm.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 UnparseC.term r = "?b \<noteq> (0::?'a) \<Longrightarrow> ?b / (?a * ?b) = (1::?'a) / ?a";
173 UnparseC.term LHS = "?b / (?a * ?b)"; UnparseC.term RHS = "(1::?'a) / ?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 UnparseC.term r' = "x \<noteq> 0 \<Longrightarrow> x / (2 * x) = 1 / 2";
178 "----- step 3: get the (instantiated) assumption(s)";
179 val p' = (fst o Logic.strip_prems) (Logic.count_prems r', [], r');
180 UnparseC.term (hd p') = "x \<noteq> 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", _)
186 $ Free ("x", _) $ Const ("Groups.zero_class.zero", _))] => ()
187 | _ => error "rewrite.sml assumption changed";
188 "===== \<up> make asms without Trueprop --- \<up> ";
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';
192 UnparseC.term t' = "1 / 2";
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, Rule_Set.Empty, [TermC.str2term "x = 0"],
200 TermC.str2term "M_b x = -1 * q_0 * x \<up> 2 / 2 + x * c + c_2");
201 "----- step 1: args for rew_";
202 val ((t', asm'), (rules as r::rs), t) = ((TermC.empty, []), equs, t);
203 "----- step 2: rew_sub";
204 rew_sub thy 1 [] ord erls false [] (HOLogic.Trueprop $ r) t;
205 "----- step 3: step through rew_sub -- inefficient: goes into subterms";
208 val SOME (t', _) = rewrite_terms_ thy dummy_ord Rule_Set.Empty equs t;
209 writeln "----------- rewrite_terms_ 1---------------------------";
210 if UnparseC.term t' = "M_b 0 = -1 * q_0 * 0 \<up> 2 / 2 + 0 * c + c_2" then ()
211 else error "rewrite.sml rewrite_terms_ [x = 0]";
213 val equs = [TermC.str2term "M_b 0 = 0"];
214 val t = TermC.str2term "M_b 0 = -1 * q_0 * 0 \<up> 2 / 2 + 0 * c + c_2";
215 val SOME (t', _) = rewrite_terms_ thy dummy_ord Rule_Set.Empty equs t;
216 writeln "----------- rewrite_terms_ 2---------------------------";
217 if UnparseC.term t' = "0 = -1 * q_0 * 0 \<up> 2 / 2 + 0 * c + c_2" then ()
218 else error "rewrite.sml rewrite_terms_ [M_b 0 = 0]";
220 val equs = [TermC.str2term "x = 0", TermC.str2term"M_b 0 = 0"];
221 val t = TermC.str2term "M_b x = -1 * q_0 * x \<up> 2 / 2 + x * c + c_2";
222 val SOME (t', _) = rewrite_terms_ thy dummy_ord Rule_Set.Empty equs t;
223 writeln "----------- rewrite_terms_ 3---------------------------";
224 if UnparseC.term t' = "0 = -1 * q_0 * 0 \<up> 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 = TermC.str2term"-1 * (q_0 * L \<up> 2) / 2 + (L * c_3 + c_4) = 0";
233 val bdvs = [(TermC.str2term"bdv_1",TermC.str2term"c"),
234 (TermC.str2term"bdv_2",TermC.str2term"c_2"),
235 (TermC.str2term"bdv_3",TermC.str2term"c_3"),
236 (TermC.str2term"bdv_4",TermC.str2term"c_4")];
237 (*------------ outcommented WN071210, after inclusion into ROOT.ML
239 rewrite_inst_ thy e_rew_ord
240 (Rule_Set.append_rules "erls_isolate_bdvs" Rule_Set.empty
241 [(Eval ("EqSystem.occur'_exactly'_in",
242 eval_occur_exactly_in
243 "#eval_occur_exactly_in_"))
245 false bdvs (ThmC.numerals_to_Free @{separate_bdvs_add) t;
246 (writeln o UnparseC.term) t;
247 if UnparseC.term t = "L * c_3 + c_4 = 0 + -1 * (-1 * (q_0 * L \<up> 2) / 2)"
248 then () else error "rewrite.sml rewrite_inst_ bdvs";
249 > Rewrite.trace_on:=true;
250 Rewrite.trace_on:=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 \<up> 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 \<up> 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 \<up> 2 / 2 is_polyexp
268 ==> 1 / EI * (L * q_0 * x / 2 + -1 * q_0 * x \<up> 2 / 2) =
269 1 * (L * q_0 * x / 2 + -1 * q_0 * x \<up> 2 / 2) / EI
270 ##### rls: Rule_Set.empty-is_polyexp on: L * q_0 * x / 2 + -1 * q_0 * x \<up> 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 \<up> 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 \<up> 2 / 2)
280 ## rls: discard_minus on: 1 / EI * (L * q_0 * x / 2 + -1 * q_0 * x \<up> 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 \<up> 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 \<up> 2 / 2 is_polyexp
287 ==> 1 / EI * (L * q_0 * x / 2 + -1 * q_0 * x \<up> 2 / 2) =
288 1 * (L * q_0 * x / 2 + -1 * q_0 * x \<up> 2 / 2) / EI
289 ##### rls: Rule_Set.empty-is_polyexp on: L * q_0 * x / 2 + -1 * q_0 * x \<up> 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 \<up> 2 / 2 is_polyexp"] stored: ["False"]
295 === rewrites to: 1 * (L * q_0 * x / 2 + -1 * q_0 * x \<up> 2 / 2) / EI
296 ----- 2009 -------------------------------------------------------------------*)
298 (*the situation as was before repair (asm without Trueprop) is outcommented*)
299 val thy = @{theory "Isac_Knowledge"};
300 "===== example which raised the problem =================";
301 val t = @{term "1 / EI * (L * q_0 * x / 2 + -1 * q_0 * x \<up> 2 / 2)"};
302 "----- rewrite_set_inst_ norm_Rational_noadd_fractions--";
303 val subs = [(@{term "bdv"}, @{term "x"})];
304 val rls = norm_Rational_noadd_fractions;
305 val SOME (t', asms) = rewrite_set_inst_ thy true subs rls t;
306 if UnparseC.term t' = "1 / EI * (L * q_0 * x / 2 + -1 * q_0 * 1 * x \<up> 2 / 2)" andalso
307 UnparseC.terms asms = "[]" then {}
308 else error "this was NONE with Isabelle2013-2 ?!?"
309 "----- rewrite_ rat_mult_poly_r--------------------------";
310 val thm = @{thm rat_mult_poly_r};
311 "?c::real is_polyexp ==> (?a::real) / (?b::real) * ?c = ?a * ?c / ?b";
312 val erls = Rule_Set.append_rules "Rule_Set.empty-is_polyexp" Rule_Set.empty
313 [Eval ("Poly.is'_polyexp", eval_is_polyexp "")];
314 val NONE (*SOME (t'', _)*) = rewrite_ thy dummy_ord erls true thm t;
315 (*t' = t''; (*false because of further rewrites in t'*)*)
316 "----- rew_sub --------------------------------";
317 val (t''', _, _, _) = rew_sub thy 0 [] dummy_ord erls true [] (Thm.prop_of thm) t;
318 (*t'' = t'''; (*true*)*)
319 "----- rewrite_set_ erls --------------------------------";
320 val cond = @{term "(L * q_0 * x / 2 + -1 * q_0 * x \<up> 2 / 2)"};
321 val NONE = rewrite_set_ thy true erls cond;
322 (* \<up> ^^ goes with '====== calc. to: False' above from beginning*)
324 writeln "===== maximally simplified example =====================";
325 val t = @{term "a / b * (x / x \<up> 2)"};
326 "?c::real is_polyexp ==> (?a::real) / (?b::real) * ?c = ?a * ?c / ?b";
327 writeln "----- rewrite_set_inst_ norm_Rational_noadd_fractions--";
328 val (*NONE*) SOME (t', asm) = rewrite_set_inst_ thy true subs rls t;
329 UnparseC.term t' = "a * x / (b * x \<up> 2)"; (*rew. by thm outside test case*)
330 (*checked visually: Rewrite.trace_on looks like above for 2009*)
332 writeln "----- rewrite_ rat_mult_poly_r--------------------------";
333 val NONE (*SOME (t'', _)*) = rewrite_ thy dummy_ord erls true thm t;
334 (*t' = t''; (*false because of further rewrites in t'*)*)
335 writeln "----- rew_sub --------------------------------";
336 val (t''', _, _, _) = rew_sub thy 0 [] dummy_ord erls true [] (Thm.prop_of thm) t;
337 (*t'' = t'''; (*true*)*)
338 writeln "----- rewrite_set_ erls --------------------------------";
339 val cond = @{term "(x / x \<up> 2)"};
340 val NONE = rewrite_set_ thy true erls cond;
341 (* \<up> ^^ goes with '====== calc. to: False' above from beginning*)
344 "----------- compare all prepat's existing 2010 ---------";
345 "----------- compare all prepat's existing 2010 ---------";
346 "----------- compare all prepat's existing 2010 ---------";
347 val thy = @{theory "Isac_Knowledge"};
348 val t = @{term "a + b * x = (0 ::real)"};
349 val pat = TermC.parse_patt thy "?l = (?r ::real)";
350 val precond = TermC.parse_patt thy "is_polynomial (?l::real)";(*no infix def*)
351 val precond = TermC.parse_patt thy "(?l::real) is_expanded";
353 val inst = Pattern.match thy (pat, t) (Vartab.empty, Vartab.empty);
354 val preinst = Envir.subst_term inst precond;
355 UnparseC.term preinst;
357 "===== Rational.thy: cancel ===";
358 (* pat matched with the current term gives an environment
359 (or not: hen the Rrls not applied);
360 if pre1 and pre2 evaluate to @{term True} in this environment,
361 then the Rrls is applied. *)
362 val t = TermC.str2term "(a + b) / c ::real";
363 val pat = TermC.parse_patt thy "?r / ?s ::real";
364 val pres = [TermC.parse_patt thy "?r is_expanded", TermC.parse_patt thy "?s is_expanded"];
365 val prepat = [(pres, pat)];
366 val erls = rational_erls;
367 (* erls got from Rrls {erls, prepat, scr = Rfuns {normal_form, ...}, ...} *)
369 val subst = Pattern.match thy (pat, t) (Vartab.empty, Vartab.empty);
370 val asms = map (Envir.subst_term subst) pres;
371 if UnparseC.terms asms = "[\"a + b is_expanded\", \"c is_expanded\"]"
372 then () else error "rewrite.sml: prepat cancel subst";
373 if ([], true) = eval__true thy 0 asms [] erls
374 then () else error "rewrite.sml: prepat cancel eval__true";
376 "===== Rational.thy: add_fractions_p ===";
377 (* if each pat* TermC.matches with the current term, the Rrls is applied
378 (there are no preconditions to be checked, they are @{term True}) *)
379 val t = TermC.str2term "a / b + 1 / 2";
380 val pat = TermC.parse_patt thy "?r / ?s + ?u / ?v";
381 val pres = [@{term True}];
382 val prepat = [(pres, pat)];
383 val erls = rational_erls;
384 (* erls got from Rrls {erls, prepat, scr = Rfuns {normal_form, ...}, ...} *)
386 val subst = Pattern.match thy (pat, t) (Vartab.empty, Vartab.empty);
387 if ([], true) = eval__true thy 0 (map (Envir.subst_term subst) pres) [] erls
388 then () else error "rewrite.sml: prepat add_fractions_p";
390 "===== Poly.thy: order_mult_ ===";
391 (* ?p matched with the current term gives an environment,
392 which evaluates (the instantiated) "p is_multUnordered" to true*)
393 val t = TermC.str2term "x \<up> 2 * x";
394 val pat = TermC.parse_patt thy "?p :: real"
395 val pres = [TermC.parse_patt thy "?p is_multUnordered"];
396 val prepat = [(pres, pat)];
397 val erls = Rule_Set.append_rules "Rule_Set.empty-is_multUnordered" Rule_Set.empty
398 [Eval ("Poly.is'_multUnordered",
399 eval_is_multUnordered "")];
401 val subst = Pattern.match thy (pat, t) (Vartab.empty, Vartab.empty);
402 val asms = map (Envir.subst_term subst) pres;
403 if UnparseC.terms asms = "[\"x \<up> 2 * x is_multUnordered\"]"
404 then () else error "rewrite.sml: prepat order_mult_ subst";
405 if ([], true) = eval__true thy 0 asms [] erls
406 then () else error "rewrite.sml: prepat order_mult_ eval__true";
409 "----------- fun app_rev, Rrls, -------------------------";
410 "----------- fun app_rev, Rrls, -------------------------";
411 "----------- fun app_rev, Rrls, -------------------------";
412 val t = TermC.str2term "x \<up> 2 * x";
414 if is_multUnordered t then () else error "rewrite.sml diff. is_multUnordered 2";
415 val tm = TermC.str2term "(x \<up> 2 * x) is_multUnordered";
416 eval_is_multUnordered "testid" "" tm thy;
418 case eval_is_multUnordered "testid" "" tm thy of
419 SOME (_, Const ("HOL.Trueprop", _) $
420 (Const ("HOL.eq", _) $
421 (Const ("Poly.is'_multUnordered", _) $ _) $
422 Const ("HOL.True", _))) => ()
423 | _ => error "rewrite.sml diff. eval_is_multUnordered 2b";
425 tracing "----- begin rewrite x \<up> 2 * x ---"; Rewrite.trace_on := false;
426 val SOME (t', _) = rewrite_set_ thy true order_mult_ t;
427 tracing "----- end rewrite x \<up> 2 * x ---"; Rewrite.trace_on := false;
428 if UnparseC.term t' = "x * x \<up> 2" then ()
429 else error "rewrite.sml Poly.is'_multUnordered doesn't work";
431 (* for achieving the previous result, the following code was taken apart *)
432 "----- rewrite__set_ ---";
433 val (thy, i, _, _, (rrls as Rrls _), t) = (thy, 0, true, [], order_mult_, tm);
434 val (t', asm, rew) = app_rev thy (i+1) rrls t;
436 val (thy, i, rrls, t) = (thy, (i+1), rrls, t);
437 fun chk_prepat thy erls [] t = true
438 | chk_prepat thy erls prepat t =
439 let fun chk (pres, pat) =
440 (let val subst: Type.tyenv * Envir.tenv =
441 Pattern.match thy (pat, t)
442 (Vartab.empty, Vartab.empty)
443 in snd (eval__true thy (i+1)
444 (map (Envir.subst_term subst) pres)
448 fun scan_ f [] = false (*scan_ NEVER called by []*)
449 | scan_ f (pp::pps) = if f pp then true
451 in scan_ chk prepat end;
453 (*.apply the normal_form of a rev-set.*)
454 fun app_rev' thy (Rrls{erls,prepat,scr=Rfuns{normal_form,...},...}) t =
455 if chk_prepat thy erls prepat t
456 then ((*tracing("### app_rev': t = "^(UnparseC.term t));*)
459 (*fixme val NONE = app_rev' thy rrls t;*)
460 "----- app_rev' ---";
461 val (thy, Rrls{erls,prepat,scr=Rfuns{normal_form,...},...}, t) = (thy, rrls, t);
462 (*fixme false*) chk_prepat thy erls prepat t;
463 "----- chk_prepat ---";
464 val (thy, erls, prepat, t) = (thy, erls, prepat, t);
465 fun chk (pres, pat) =
466 (let val subst: Type.tyenv * Envir.tenv =
467 Pattern.match thy (pat, t)
468 (Vartab.empty, Vartab.empty)
469 in snd (eval__true thy (i+1)
470 (map (Envir.subst_term subst) pres)
474 fun scan_ f [] = false (*scan_ NEVER called by []*)
475 | scan_ f (pp::pps) = if f pp then true
477 tracing "=== poly.sml: scan_ chk prepat begin";
479 tracing "=== poly.sml: scan_ chk prepat end";
482 (*reestablish...*) val t = TermC.str2term "x \<up> 2 * x";
483 val [(pres, pat)] = prepat;
484 val subst: Type.tyenv * Envir.tenv =
485 Pattern.match thy (pat, t)
486 (Vartab.empty, Vartab.empty);
488 (*fixme: asms = ["p is_multUnordered"]...instantiate*)
489 "----- eval__true ---";
490 val asms = (map (Envir.subst_term subst) pres);
491 if UnparseC.terms asms = "[\"x \<up> 2 * x is_multUnordered\"]" then ()
492 else error "rewrite.sml: diff. is_multUnordered, asms";
493 val (thy, i, asms, bdv, rls) =
494 (thy, (i+1), [TermC.str2term "(x \<up> 2 * x) is_multUnordered"],
495 [] : (term * term) list, erls);
496 case eval__true thy i asms bdv rls of
498 | _ => error "rewrite.sml: diff. is_multUnordered, eval__true";
500 "----------- 2011 thms with axclasses -------------------";
501 "----------- 2011 thms with axclasses -------------------";
502 "----------- 2011 thms with axclasses -------------------";
503 val thm = ThmC.numerals_to_Free @{thm div_by_1};
504 val prop = Thm.prop_of thm;
505 TermC.atomty prop; (*Type 'a*)
506 val t = TermC.str2term "(2*x)/1"; (*Type real*)
508 val (thy, ro, er, inst) =
509 (@{theory "Isac_Knowledge"}, tless_true, eval_rls, [(@{term "bdv::real"}, @{term "x::real"})]);
510 val SOME (t, _) = rewrite_ thy ro er true thm t; (*real TermC.matches 'a ?via ring? etc*)
512 "----------- fun rewrite_set_ .. RatEq_eliminate step into to fun chk --------------------------";
513 "----------- fun rewrite_set_ .. RatEq_eliminate step into to fun chk --------------------------";
514 "----------- fun rewrite_set_ .. RatEq_eliminate step into to fun chk --------------------------";
515 val thy = @{theory RatEq};
516 val ctxt = Proof_Context.init_global thy;
517 val SOME t = parseNEW ctxt "(3 + -1 * x + x \<up> 2) / (9 * x + -6 * x \<up> 2 + x \<up> 3) = 1 / x";
518 val rls = assoc_rls "RatEq_eliminate"
520 val SOME (t''''', asm''''') =
521 rewrite_set_ thy true rls t;
522 "~~~~~ fun rewrite_set_ , args:"; val (thy, bool, rls, term) = (thy, true, rls, t);
523 rewrite__set_ thy 1 bool [] rls term;
524 "~~~~~ and rewrite__set_ , args:"; val (thy, i, put_asm, bdv, rls, ct)
525 = (thy, 1, bool, []:(term * term) list, rls, term);
527 (*/------- outcomment this code: otherwise the re-definition could infect tests lateron ------\ * )
528 datatype switch = Applicable.Yes | Noap;
529 fun rew_once _ asm ct Noap [] = (ct, asm) (* ?TODO unify with Prog_Expr.rew_once? *)
530 | rew_once ruls asm ct Applicable.Yes [] =
531 (case rls of Rule_Set.Repeat _ => rew_once ruls asm ct Noap ruls
532 | Rule_Set.Sequence _ => (ct, asm)
533 | rls => raise ERROR ("rew_once not appl. to \"" ^ Rule_Set.id rls ^ "\""))
534 | rew_once ruls asm ct apno (rul :: thms) =
536 Rule.Thm (thmid, thm) =>
537 (trace1 i (" try thm: " ^ thmid);
538 case rewrite__ thy (i + 1) bdv ((snd o #rew_ord o Rule.Rule_Set.rep) rls)
539 ((#erls o Rule.Rule_Set.rep) rls) put_asm thm ct of
540 NONE => rew_once ruls asm ct apno thms
541 | SOME (ct', asm') =>
542 (trace1 i (" rewrites to: " ^ UnparseC.term_in_thy thy ct');
543 rew_once ruls (union (op =) asm asm') ct' Applicable.Yes (rul :: thms)))
544 (* once again try the same rule, e.g. associativity against "()"*)
545 | Rule.Eval (cc as (op_, _)) =>
546 let val _= trace1 i (" try calc: " ^ op_ ^ "'")
547 val ct = TermC.uminus_to_string ct (*WN190312: superfluous?*)
548 in case Eval.adhoc_thm thy cc ct of
549 NONE => rew_once ruls asm ct apno thms
552 val pairopt = rewrite__ thy (i + 1) bdv ((snd o #rew_ord o Rule.Rule_Set.rep) rls)
553 ((#erls o Rule.Rule_Set.rep) rls) put_asm thm' ct;
554 val _ = if pairopt <> NONE then () else error ("rewrite_set_, rewrite_ \"" ^
555 ThmC.string_of_thm thm' ^ "\" " ^ UnparseC.term_in_thy thy ct ^ " = NONE")
556 val _ = trace1 i (" calc. to: " ^ UnparseC.term_in_thy thy ((fst o the) pairopt))
557 in rew_once ruls asm ((fst o the) pairopt) Applicable.Yes (rul :: thms) end
559 | Rule.Cal1 (cc as (op_, _)) =>
560 let val _= trace1 i (" try cal1: " ^ op_ ^ "'");
561 val ct = TermC.uminus_to_string ct
562 in case Eval.adhoc_thm1_ thy cc ct of
566 val pairopt = rewrite__ thy (i + 1) bdv ((snd o #rew_ord o Rule.Rule_Set.rep) rls)
567 ((#erls o Rule.Rule_Set.rep) rls) put_asm thm' ct;
568 val _ = if pairopt <> NONE then () else error ("rewrite_set_, rewrite_ \"" ^
569 ThmC.string_of_thm thm' ^ "\" " ^ UnparseC.term_in_thy thy ct ^ " = NONE")
570 val _ = trace1 i (" cal1. to: " ^ UnparseC.term_in_thy thy ((fst o the) pairopt))
574 (case rewrite__set_ thy (i + 1) put_asm bdv rls' ct of
575 SOME (t', asm') => rew_once ruls (union (op =) asm asm') t' Applicable.Yes thms
576 | NONE => rew_once ruls asm ct apno thms)
577 | r => raise ERROR ("rew_once not appl. to \"" ^ Rule.Rule.to_string r ^ "\"");
578 val ruls = (#rules o Rule.Rule_Set.rep) rls;
579 (* val _ = trace i (" rls: " ^ Rule_Set.id rls ^ " on: " ^ UnparseC.term_in_thy thy ct)*)
580 val (ct', asm') = rew_once ruls [] ct Noap ruls;
581 "~~~~~ fun rew_once , args:"; val (ruls, asm, ct, apno, (rul :: thms))
582 = (ruls, []:term list, ct, Noap, ruls);
583 val Rule.Thm (thmid, thm) = (*case*) rul (*of*);
585 val SOME (ct', asm') = (*case*)
586 rewrite__ thy (i + 1) bdv ((snd o #rew_ord o Rule.Rule_Set.rep) rls)
587 ((#erls o Rule.Rule_Set.rep) rls) put_asm thm ct (*of*);
588 "~~~~~ fun rewrite__ , args:"; val (thy, i, bdv, tless, rls, put_asm, thm, ct)
589 = (thy, (i + 1), bdv, ((snd o #rew_ord o Rule.Rule_Set.rep) rls),
590 ((#erls o Rule.Rule_Set.rep) rls), put_asm, thm, ct);
592 val (t', asms, _ (*lrd*), rew) =
593 rew_sub thy i bdv tless rls put_asm ([(*root of the term*)]: TermC.path)
594 (((TermC.inst_bdv bdv) o Eval.norm o Thm.prop_of) thm) ct;
595 "~~~~~ and rew_sub , args:"; val (thy, i, bdv, tless, rls, put_asm, lrd, r, t)
596 = (thy, i, bdv, tless, rls, put_asm, ([(*root of the term*)]: TermC.path),
597 (((TermC.inst_bdv bdv) o Eval.norm o Thm.prop_of) thm), ct);
598 val (lhs, rhs) = (HOLogic.dest_eq o HOLogic.dest_Trueprop o Logic.strip_imp_concl) r
599 val r' = Envir.subst_term (Pattern.match thy (lhs, t) (Vartab.empty, Vartab.empty)) r
601 (*+*)if UnparseC.term r' =
602 (*+*) "\<lbrakk>9 * x + -6 * x \<up> 2 + x \<up> 3 \<noteq> 0; x \<noteq> 0\<rbrakk>\n" ^
603 (*+*) "\<Longrightarrow> ((3 + -1 * x + x \<up> 2) /\n" ^
604 (*+*) " (9 * x + -6 * x \<up> 2 + x \<up> 3) =\n" ^
605 (*+*) " 1 / x) =\n" ^
606 (*+*) " ((3 + -1 * x + x \<up> 2) * x =\n" ^
607 (*+*) " 1 * (9 * x + -6 * x \<up> 2 + x \<up> 3))"
608 (*+*)then () else error "instantiated rule CHANGED";
610 val p' = map HOLogic.dest_Trueprop ((fst o Logic.strip_prems) (Logic.count_prems r', [], r'))
612 (*+*)if map UnparseC.term p' = ["x \<noteq> 0", "9 * x + -6 * x \<up> 2 + x \<up> 3 \<noteq> 0"]
613 (*+*)then () else error "stored assumptions CHANGED";
615 val t' = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop o Logic.strip_imp_concl) r'
617 (*+*)if UnparseC.term t' = "(3 + -1 * x + x \<up> 2) * x = 1 * (9 * x + -6 * x \<up> 2 + x \<up> 3)"
618 (*+*)then () else error "rewritten term (an equality) CHANGED";
620 val (simpl_p', nofalse) =
621 eval__true thy (i + 1) p' bdv rls;
622 "~~~~~ and eval__true , args:"; val (thy, i, asms, bdv, rls) = (thy, (i + 1), p', bdv, rls);
623 (*if*) asms = [@{term True}] orelse asms = [] (*else*);
625 (*+*)if map UnparseC.term asms = ["x \<noteq> 0", "9 * x + -6 * x \<up> 2 + x \<up> 3 \<noteq> 0"]
626 (*+*)then () else error "asms before chk CHANGED";
628 fun chk indets [] = (indets, true) (*return asms<>True until false*)
629 | chk indets (a :: asms) =
630 (case rewrite__set_ thy (i + 1) false bdv rls a of
631 NONE => (chk (indets @ [a]) asms)
633 if t = @{term True} then (chk (indets @ a') asms)
634 else if t = @{term False} then ([], false)
635 (*asm false .. thm not applied \<up> ; continue until False vvv*)
636 else chk (indets @ [t] @ a') asms);
639 chk [] asms; (*return from eval__true*);
640 "~~~~~ fun chk , args:"; val (indets, (a :: asms)) = ([], asms);
642 (*+*)val Rule_Set.Repeat {id = "rateq_erls", rules, ...} = rls;
644 (*+*) [Eval ("Rings.divide_class.divide", fn),
645 (*+*) Thm ("minus_divide_left", "- ?a1 / ?b1 = - (?a1 / ?b1)"),
647 (*+*) Eval ("HOL.eq", fn),
648 (*+*) Thm ("not_true", "(\<not> True) = False"),
649 (*+*) Thm ("not_false", "(\<not> False) = True"),
651 (*+*) Eval ("Prog_Expr.pow", fn),
652 (*+*) Eval ("RatEq.is'_ratequation'_in", fn)]:
654 (*+*)chk: term list -> term list -> term list * bool
656 rewrite__set_ thy (i + 1) false bdv rls a (*of*);
658 (*+*)Rewrite.trace_on := true;
660 (*this was False; vvvv--- means: indeterminate*)
661 val (* SOME (t, a') *)NONE = (*case*)
662 rewrite__set_ thy (i + 1) false bdv rls a (*of*);
664 (*+*)UnparseC.term a = "x \<noteq> 0"; (* rewrite__set_ \<rightarrow> @{term True} ----------------- SHOULD BE indet !*)
667 #### rls: rateq_erls on: x \<noteq> 0
669 ##### try calc: HOL.eq' <<<------------------------------- here the error comes from
670 ===== calc. to: ~ False <<<------------------------------- \<not> x = 0 is NOT False
671 ##### try calc: HOL.eq'
672 ##### try thm: not_true
673 ##### try thm: not_false
674 ===== rewrites to: True <<<------------------------------- so x \<noteq> 0 is NOT True
675 and True, False are NOT stored ...
677 ### asms accepted: [x \<noteq> 0] stored: []
679 Rewrite.trace_on := false;
680 ( *\------- outcomment this code: otherwise the re-definition could infect tests lateron ------/*)
683 "----------- fun rewrite_ down to Pattern.match ------------------------------------------------";
684 "----------- fun rewrite_ down to Pattern.match ------------------------------------------------";
685 "----------- fun rewrite_ down to Pattern.match ------------------------------------------------";
686 "~~~~~ fun rewrite_ , args:"; val (thy, rew_ord, erls, bool, thm, term) =
687 (@{theory}, dummy_ord, Rule_Set.empty, false, @{thm distrib_left}, @{term "x * (y + z) :: int"});
688 "~~~~~ fun rewrite__ , args:"; val (thy, i, bdv, tless, rls, put_asm, thm, ct) =
689 (thy, 1, [], rew_ord, erls, bool, thm, term);
690 "~~~~~ and rew_sub , args:"; val (thy, i, bdv, tless, rls, put_asm, lrd, r, t) =
691 (thy, i, bdv, tless, rls, put_asm, [], TermC.inst_bdv bdv (Eval.norm (Thm.prop_of thm)), ct)
692 val (lhss, rhss) = (HOLogic.dest_eq o HOLogic.dest_Trueprop o Logic.strip_imp_concl) r
693 val r' = Envir.subst_term (Pattern.match thy (lhss, t) (Vartab.empty, Vartab.empty)) r
694 val p' = map HOLogic.dest_Trueprop ((fst o Logic.strip_prems) (Logic.count_prems r', [], r'))
695 val t' = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop o Logic.strip_imp_concl) r'
697 if UnparseC.term lhss = "?a * (?b + ?c)" andalso UnparseC.term t = "x * (y + z)" then ()
698 else error "ARGS FOR Pattern.match CHANGED";
699 val match = Pattern.match thy (lhss, t) (Vartab.empty, Vartab.empty);
700 if (Envir.subst_term match r |> UnparseC.term) = "x * (y + z) = x * y + x * z" then ()
701 else error "Pattern.match CHANGED";
703 "----------- fun rewrite_set_ .. norm_equation -------------------------------------------------";
704 "----------- fun rewrite_set_ .. norm_equation -------------------------------------------------";
705 "----------- fun rewrite_set_ .. norm_equation -------------------------------------------------";
706 (* norm_equation is defined in Test.thy, other rls see Knowledg/**)
708 val rls = norm_equation;
709 val term = TermC.str2term "x + 1 = 2";
711 val SOME (t, asm) = rewrite_set_ thy false rls term;
712 if UnparseC.term t = "x + 1 + -1 * 2 = 0" then () else error "rewrite_set_ norm_equation CHANGED";
714 "~~~~~ fun rewrite_set_, args:"; val (thy, bool, rls, term) = (thy, false, rls, term);
715 "~~~~~ fun rewrite__set_, args:"; val (thy, i, put_asm, bdv, rls, ct) = (thy, 1, bool, [], rls, term);