1 (* Title: "MathEngBasic/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's thys ------------------------------------------------";
11 "----------- test rewriting without Isac's thys, ~~~~~ fun rewrite_ ----------------------------";
12 "----------- conditional rewriting without Isac's thys -----------------------------------------";
13 "----------- conditional rewriting without Isac's thys, ~~~~~ fun ------------------------------";
14 "----------- conditional rewriting creating an assumption---------------------------------------";
15 "----------- step through 'and rew_sub': -------------------------------------------------------";
16 "----------- step through 'fun rewrite_terms_' ------------------------------------------------";
17 "----------- rewrite_inst_ bdvs ----------------------------------------------------------------";
18 "----------- check diff 2002--2009-3 -----------------------------------------------------------";
19 "----------- compare all prepat's existing 2010 ------------------------------------------------";
20 "----------- fun app_rev, Rrls, ----------------------------------------------------------------";
21 "----------- 2011 thms with axclasses ----------------------------------------------------------";
22 "----------- fun rewrite_set_ .. RatEq_eliminate step into to fun chk --------------------------";
23 "----------- fun rewrite_ down to Pattern.match ------------------------------------------------";
24 "----------- fun rewrite_set_ .. norm_equation -------------------------------------------------";
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 = TermC.parseNEW' ctxt "((r + u) + t) + (s::real)";
40 "----- from old: fun rewrite__";
42 val r = TermC.inst_bdv bdv (Eval.norm (Thm.prop_of 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_ ctxt Rewrite_Ord.function_empty Rule_Set.empty false thm tm);
92 (*is displayed on _TOP_ of <response> buffer...*)
93 Pretty.writeln (Proof_Context.pretty_term_abbrev @{context} r);
94 if r = @{term "y*z + x::real"}
95 then () else error "rewrite.sml diff.result in rewriting";
97 "----- rewriting a subterm";
98 val tm = @{term "w*(x + y*z)::real"};
100 val SOME (r, _) = (rewrite_ ctxt Rewrite_Ord.function_empty Rule_Set.empty false thm tm);
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_ ctxt tord Rule_Set.empty false thm tm);
108 (*is displayed on _TOP_ of <response> buffer...*)
109 Pretty.writeln (Proof_Context.pretty_term_abbrev @{context} r);
111 val tm = @{term "x*y + z::real"};
112 val SOME (r, _) = (rewrite_ ctxt tord Rule_Set.empty false thm tm);
115 "----------- conditional rewriting without Isac's thys -----------------------------------------";
116 "----------- conditional rewriting without Isac's thys -----------------------------------------";
117 "----------- conditional rewriting without Isac's thys -----------------------------------------";
118 "===== prepr cond.rew. with Pattern.match";
119 val thy = @{theory Complex_Main};
120 val ctxt = @{context};
121 val thm = @{thm nonzero_divide_mult_cancel_right}; (* = "?b \<noteq> 0 \<Longrightarrow> ?b / (?a * ?b) = 1 / ?a":*)
122 val rule = Thm.prop_of thm;
123 val tm = @{term "x / (2 * x)::real"};
124 val prem = Logic.strip_imp_prems rule;
125 val nps = Logic.count_prems rule;
126 val prems = Logic.strip_prems (nps, [], rule);
128 val eq = Logic.strip_imp_concl rule;
129 val (LHS, RHS) = (HOLogic.dest_eq o HOLogic.dest_Trueprop) eq;
131 val mtcs = Pattern.match thy (LHS, tm) (Vartab.empty, Vartab.empty);
132 val rule' = Envir.subst_term mtcs rule;
134 val prems' = (fst o Logic.strip_prems) (Logic.count_prems rule', [], rule');
135 val RHS' = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop o Logic.strip_imp_concl) rule';
137 (rule' |> UnparseC.term) = "x \<noteq> 0 \<Longrightarrow> x / (2 * x) = 1 / 2";
140 (rule' |> Logic.strip_imp_concl |> UnparseC.term) = "x / (2 * x) = 1 / 2";
141 rule' |> Logic.strip_imp_concl;
143 (rule' |> Logic.strip_imp_concl |> UnparseC.term) = "x / (2 * x) = 1 / 2";
144 rule' |> Logic.strip_imp_concl;
147 "----------- conditional rewriting creating an assumption---------------------------------------";
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"};
153 val SOME (rew, asm) = rewrite_ ctxt Rewrite_Ord.function_empty Rule_Set.empty false thm tm;
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 "----------- conditional rewriting creating an assumption, ~~~~~ fun rewrite_ ------------------";
165 "----------- conditional rewriting creating an assumption, ~~~~~ fun rewrite_ ------------------";
166 "----------- conditional rewriting creating an assumption, ~~~~~ fun rewrite_ ------------------";
167 val thm = @{thm nonzero_divide_mult_cancel_right};(* = "?b \<noteq> 0 \<Longrightarrow> ?b / (?a * ?b) = 1 / ?a"*)
168 val tm = @{term "x / (2 * x)::real"};
171 (**)val SOME (rew, asm) = rewrite_ ctxt Rewrite_Ord.function_empty Rule_Set.empty false thm tm;
172 (** )exception TERM raised (line 196 of "~~/src/HOL/Tools/hologic.ML"):
174 ?b \<noteq> 0 \<Longrightarrow> ?b / (?a * ?b) = 1 / ?a( **)
175 "~~~~~ fun rewrite_ , args:"; val (thy, rew_ord, erls, bool, thm, term) =
176 (thy, Rewrite_Ord.function_empty, erls, false, thm, tm);
177 "~~~~~ fun rewrite__ , args:"; val (thy, i, bdv, tless, rls, put_asm, thm, ct) =
178 (thy, 1, []: Subst.T, rew_ord, erls, bool, thm, term);
180 (**) val (t', asms, _(*lrd*), rew) = rew_sub ctxt i bdv tless rls put_asm ([(*root of the term*)]: TermC.path)
181 (TermC.inst_bdv bdv (Eval.norm (Thm.prop_of thm))) ct;
182 (** )exception TERM raised (line 196 of "~~/src/HOL/Tools/hologic.ML"):
184 ?b \<noteq> 0 \<Longrightarrow> ?b / (?a * ?b) = 1 / ?a( **)
185 "~~~~~ fun rew_sub , args:"; val (thy, i, bdv, tless, rls, put_asm, lrd, r, t) =
186 (thy, i, bdv, tless, rls, put_asm, ([(*root of the term*)]: TermC.path),
187 (TermC.inst_bdv bdv (Eval.norm (Thm.prop_of thm))), ct);
188 (*+*)UnparseC.term r = "?b \<noteq> (0::?'a) \<Longrightarrow> ?b / (?a * ?b) = (1::?'a) / ?a";
190 val (lhs, rhs) = (HOLogic.dest_eq o HOLogic.dest_Trueprop o Logic.strip_imp_concl) r;
191 (*+*)(UnparseC.term lhs, UnparseC.term rhs) = ("?b / (?a * ?b)", "(1::?'a) / ?a");
192 val r' = (Envir.subst_term (Pattern.match thy (lhs, t) (Vartab.empty, Vartab.empty)) r)
193 handle Pattern.MATCH => raise NO_REWRITE;
194 val p' = map HOLogic.dest_Trueprop ((fst o Logic.strip_prems) (Logic.count_prems r', [], r'));
195 (*+*)UnparseC.term r' = "x \<noteq> 0 \<Longrightarrow> x / (2 * x) = 1 / 2";
197 val t' = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop o Logic.strip_imp_concl) r'
198 val _ = trace_in2 ctxt i "eval asms" r';
199 val (simpl_p', nofalse) = eval__true ctxt (i + 1) p' bdv rls;
200 (*if*) nofalse (*then*);
201 val (t'', p'') = (trace_in4 ctxt i "asms accepted" p' simpl_p'; (t',simpl_p'));
202 (*## asms accepted: [x \<noteq> 0] stored: [x \<noteq> 0] *)
204 (*+*)if (UnparseC.term t'', map UnparseC.term p'') = ("1 / 2", ["x \<noteq> 0"]) then ()
205 (*+*)else error "conditional rewriting x \<noteq> 0 \<Longrightarrow> x / (2 * x) = 1 / 2 CHANGED";
208 "----------- step through 'and rew_sub': ----------------";
209 "----------- step through 'and rew_sub': ----------------";
210 "----------- step through 'and rew_sub': ----------------";
211 (*and make asms without Trueprop, beginning with the result:*)
212 val tm = @{term "x / (2 * x)::real"};
213 val (t', asm, _, _) = rew_sub ctxt 0 [] Rewrite_Ord.function_empty Rule_Set.empty true [] (Thm.prop_of thm) tm;
214 (*show_types := false;*)
215 "----- evaluate arguments";
216 val (thy, i, bdv, tless, rls, put_asm, lrd, r, t) =
217 (thy, 0, [], Rewrite_Ord.function_empty, Rule_Set.empty, true, [], (Thm.prop_of thm), tm);
218 "----- step 1: LHS, RHS of rule";
219 val (LHS, RHS) = (HOLogic.dest_eq o HOLogic.dest_Trueprop
220 o Logic.strip_imp_concl) r;
221 UnparseC.term r = "?b \<noteq> (0::?'a) \<Longrightarrow> ?b / (?a * ?b) = (1::?'a) / ?a";
222 UnparseC.term LHS = "?b / (?a * ?b)"; UnparseC.term RHS = "(1::?'a) / ?a";
223 "----- step 2: the rule instantiated";
224 val r' = Envir.subst_term
225 (Pattern.match thy (LHS, t) (Vartab.empty, Vartab.empty)) r;
226 UnparseC.term r' = "x \<noteq> 0 \<Longrightarrow> x / (2 * x) = 1 / 2";
227 "----- step 3: get the (instantiated) assumption(s)";
228 val p' = (fst o Logic.strip_prems) (Logic.count_prems r', [], r');
229 UnparseC.term (hd p') = "x \<noteq> 0";
230 "=====vvv make asms without Trueprop ---vvv";
231 val p' = map HOLogic.dest_Trueprop ((fst o Logic.strip_prems)
232 (Logic.count_prems r', [], r'));
234 [Const (\<^const_name>\<open>Not\<close>, _) $ (Const (\<^const_name>\<open>HOL.eq\<close>, _)
235 $ Free ("x", _) $ Const (\<^const_name>\<open>zero_class.zero\<close>, _))] => ()
236 | _ => error "rewrite.sml assumption changed";
237 "===== \<up> make asms without Trueprop --- \<up> ";
238 "----- step 4: get the (instantiated) RHS";
239 val t' = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop
240 o Logic.strip_imp_concl) r';
241 UnparseC.term t' = "1 / 2";
243 "----------- step through 'fun rewrite_terms_' ------------------------------------------------";
244 "----------- step through 'fun rewrite_terms_' ------------------------------------------------";
245 "----------- step through 'fun rewrite_terms_' ------------------------------------------------";
246 "----- step 0: args for rewrite_terms_, local fun";
247 val (thy, ord, erls, equs, t) =
248 (@{theory "Biegelinie"}, Rewrite_Ord.function_empty, Rule_Set.Empty, [TermC.str2term "x = 0"],
249 TermC.str2term "M_b x = -1 * q_0 * x \<up> 2 / 2 + x * c + c_2");
250 "----- step 1: args for rew_";
251 val ((t', asm'), (rules as r::rs), t) = ((TermC.empty, []), equs, t);
252 "----- step 2: rew_sub";
253 rew_sub ctxt 1 [] ord erls false [] (HOLogic.Trueprop $ r) t;
254 "----- step 3: step through rew_sub -- inefficient: goes into subterms";
257 val SOME (t', _) = rewrite_terms_ ctxt Rewrite_Ord.function_empty Rule_Set.Empty equs t;
258 writeln "---------- rewrite_terms_ 1---------------------------";
259 if UnparseC.term t' = "M_b 0 = - 1 * q_0 * 0 \<up> 2 / 2 + 0 * c + c_2" then ()
260 else error "rewrite.sml rewrite_terms_ [x = 0]";
262 val equs = [TermC.str2term "M_b 0 = 0"];
263 val t = TermC.str2term "M_b 0 = - 1 * q_0 * 0 \<up> 2 / 2 + 0 * c + c_2";
264 val SOME (t', _) = rewrite_terms_ ctxt Rewrite_Ord.function_empty Rule_Set.Empty equs t;
265 writeln "---------- rewrite_terms_ 2---------------------------";
266 if UnparseC.term t' = "0 = - 1 * q_0 * 0 \<up> 2 / 2 + 0 * c + c_2" then ()
267 else error "rewrite.sml rewrite_terms_ [M_b 0 = 0]";
269 val equs = [TermC.str2term "x = 0", TermC.str2term"M_b 0 = 0"];
270 val t = TermC.str2term "M_b x = - 1 * q_0 * x \<up> 2 / 2 + x * c + c_2";
271 val SOME (t', _) = rewrite_terms_ ctxt Rewrite_Ord.function_empty Rule_Set.Empty equs t;
272 writeln "---------- rewrite_terms_ 3---------------------------";
273 if UnparseC.term t' = "0 = - 1 * q_0 * 0 \<up> 2 / 2 + 0 * c + c_2" then ()
274 else error "rewrite.sml rewrite_terms_ [x = 0, M_b 0 = 0]";
277 "----------- rewrite_inst_ bdvs ----------------------------------------------------------------";
278 "----------- rewrite_inst_ bdvs ----------------------------------------------------------------";
279 "----------- rewrite_inst_ bdvs ----------------------------------------------------------------";
280 (*see smltest/Scripts/term_G.sml: inst_bdv 2*)
281 val t = TermC.str2term"-1 * (q_0 * L \<up> 2) / 2 + (L * c_3 + c_4) = 0";
282 val bdvs = [(TermC.str2term"bdv_1",TermC.str2term"c"),
283 (TermC.str2term"bdv_2",TermC.str2term"c_2"),
284 (TermC.str2term"bdv_3",TermC.str2term"c_3"),
285 (TermC.str2term"bdv_4",TermC.str2term"c_4")];
286 (*------------ outcommented WN071210, after inclusion into ROOT.ML
288 rewrite_inst_ thy e_rew_ord
289 (Rule_Set.append_rules "erls_isolate_bdvs" Rule_Set.empty
290 [(Eval ("EqSystem.occur_exactly_in",
291 eval_occur_exactly_in
292 "#eval_occur_exactly_in_"))
294 false bdvs (ThmC.numerals_to_Free @{separate_bdvs_add) t;
295 (writeln o UnparseC.term) t;
296 if UnparseC.term t = "L * c_3 + c_4 = 0 + -1 * (-1 * (q_0 * L \<up> 2) / 2)"
297 then () else error "rewrite.sml rewrite_inst_ bdvs";
298 > Rewrite.trace_on:=true;false
299 Rewrite.trace_on:=false;--------------------------------------------*)
302 "----------- compare all prepat's existing 2010 ------------------------------------------------";
303 "----------- compare all prepat's existing 2010 ------------------------------------------------";
304 "----------- compare all prepat's existing 2010 ------------------------------------------------";
305 val thy = @{theory "Isac_Knowledge"};
306 val t = @{term "a + b * x = (0 ::real)"};
307 val pat = TermC.parse_patt thy "?l = (?r ::real)";
308 val precond = TermC.parse_patt thy "is_polynomial (?l::real)";(*no infix def*)
309 val precond = TermC.parse_patt thy "(?l::real) is_expanded";
311 val inst = Pattern.match thy (pat, t) (Vartab.empty, Vartab.empty);
312 val preinst = Envir.subst_term inst precond;
313 UnparseC.term preinst;
315 "===== Rational.thy: cancel ===";
316 (* pat matched with the current term gives an environment
317 (or not: hen the Rrls not applied);
318 if pre1 and pre2 evaluate to @{term True} in this environment,
319 then the Rrls is applied. *)
320 val t = TermC.str2term "(a + b) / c ::real";
321 val pat = TermC.parse_patt thy "?r / ?s ::real";
322 val pres = [TermC.parse_patt thy "?r is_expanded", TermC.parse_patt thy "?s is_expanded"];
323 val prepat = [(pres, pat)];
324 val erls = rational_erls;
325 (* erls got from Rrls {erls, prepat, scr = Rfuns {normal_form, ...}, ...} *)
327 val subst = Pattern.match thy (pat, t) (Vartab.empty, Vartab.empty);
328 val asms = map (Envir.subst_term subst) pres;
329 if UnparseC.terms asms = "[\"a + b is_expanded\", \"c is_expanded\"]"
330 then () else error "rewrite.sml: prepat cancel subst";
332 if ([], true) = eval__true ctxt 0 asms [] erls
333 then () else error "rewrite.sml: prepat cancel eval__true";
335 "===== Rational.thy: add_fractions_p ===";
336 (* if each pat* TermC.matches with the current term, the Rrls is applied
337 (there are no preconditions to be checked, they are @{term True}) *)
338 val t = TermC.str2term "a / b + 1 / 2";
339 val pat = TermC.parse_patt thy "?r / ?s + ?u / ?v";
340 val pres = [@{term True}];
341 val prepat = [(pres, pat)];
342 val erls = rational_erls;
343 (* erls got from Rrls {erls, prepat, scr = Rfuns {normal_form, ...}, ...} *)
345 val subst = Pattern.match thy (pat, t) (Vartab.empty, Vartab.empty);
346 if ([], true) = eval__true ctxt 0 (map (Envir.subst_term subst) pres) [] erls
347 then () else error "rewrite.sml: prepat add_fractions_p";
349 "===== Poly.thy: order_mult_ ===";
350 (* ?p matched with the current term gives an environment,
351 which evaluates (the instantiated) "p is_multUnordered" to true*)
352 val t = TermC.str2term "x \<up> 2 * x";
353 val pat = TermC.parse_patt thy "?p :: real"
354 val pres = [TermC.parse_patt thy "?p is_multUnordered"];
355 val prepat = [(pres, pat)];
356 val erls = Rule_Set.append_rules "Rule_Set.empty-is_multUnordered" Rule_Set.empty
357 [Eval ("Poly.is_multUnordered",
358 eval_is_multUnordered "")];
360 val subst = Pattern.match thy (pat, t) (Vartab.empty, Vartab.empty);
361 val asms = map (Envir.subst_term subst) pres;
362 if UnparseC.terms asms = "[\"x \<up> 2 * x is_multUnordered\"]"
363 then () else error "rewrite.sml: prepat order_mult_ subst";
365 if ([], true) = eval__true ctxt 0 asms [] erls
366 then () else error "rewrite.sml: prepat order_mult_ eval__true";
369 "----------- fun app_rev, Rrls, ----------------------------------------------------------------";
370 "----------- fun app_rev, Rrls, ----------------------------------------------------------------";
371 "----------- fun app_rev, Rrls, ----------------------------------------------------------------";
372 val t = TermC.str2term "x \<up> 2 * x";
374 if is_multUnordered t then () else error "rewrite.sml diff. is_multUnordered 2";
375 val tm = TermC.str2term "(x \<up> 2 * x) is_multUnordered";
377 (*+*)case eval_is_multUnordered "testid" "" tm ctxt of
379 (*+*) ("testidx \<up> 2 * x_",
380 (*+*) Const (\<^const_name>\<open>Trueprop\<close>, _) $
381 (*+*) (Const (\<^const_name>\<open>HOL.eq\<close>, _) $
382 (*+*) (Const (\<^const_name>\<open>is_multUnordered\<close>, _) $
383 (*+*) (Const (\<^const_name>\<open>times\<close>, _) $
384 (*+*) (Const (\<^const_name>\<open>realpow\<close>, _) $ Free ("x", _) $ _ ) $ Free ("x", _))) $
385 (*+*) Const (\<^const_name>\<open>True\<close>, _))) => ()
386 (*+*)(* ^^^^^^ compare ---vvv *)
387 (*+*)| _ => error "rewrite.sml diff. eval_is_multUnordered 2b CHANGED";
390 eval_is_multUnordered "testid" "" tm ctxt;
392 case eval_is_multUnordered "testid" "" tm ctxt of
393 SOME (_, Const (\<^const_name>\<open>Trueprop\<close>, _) $
394 (Const (\<^const_name>\<open>HOL.eq\<close>, _) $
395 (Const (\<^const_name>\<open>is_multUnordered\<close>, _) $ _) $
396 Const (\<^const_name>\<open>True\<close>, _))) => ()
397 | _ => error "rewrite.sml diff. eval_is_multUnordered 2b";
399 tracing "----- begin rewrite x \<up> 2 * x ---";
400 val SOME (t', _) = rewrite_set_ ctxt true order_mult_ t;
401 tracing "----- end rewrite x \<up> 2 * x ---";
402 if UnparseC.term t' = "x * x \<up> 2" then ()
403 else error "rewrite.sml Poly.is_multUnordered doesn't work";
405 (* for achieving the previous result, the following code was taken apart *)
406 "----- rewrite__set_ ---";
407 val (thy, i, _, _, (rrls as Rrls _), t) = (thy, 0, true, [], order_mult_, tm);
408 val (t', asm, rew) = app_rev ctxt (i+1) rrls t;
410 val (thy, i, rrls, t) = (thy, (i+1), rrls, t);
411 fun chk_prepat thy erls [] t = true
412 | chk_prepat thy erls prepat t =
413 let fun chk (pres, pat) =
414 (let val subst: Type.tyenv * Envir.tenv =
415 Pattern.match thy (pat, t)
416 (Vartab.empty, Vartab.empty)
417 in snd (eval__true ctxt (i+1)
418 (map (Envir.subst_term subst) pres)
421 handle Pattern.MATCH => false
422 fun scan_ f [] = false (*scan_ NEVER called by []*)
423 | scan_ f (pp::pps) = if f pp then true
425 in scan_ chk prepat end;
427 (*.apply the normal_form of a rev-set.*)
428 fun app_rev' thy (Rrls{erls,prepat,scr=Rfuns{normal_form,...},...}) t =
429 if chk_prepat thy erls prepat t
430 then ((*tracing("### app_rev': t = "^(UnparseC.term t));*)
433 (*fixme val NONE = app_rev' thy rrls t;*)
434 "----- app_rev' ---";
435 val (thy, Rrls{erls,prepat,scr=Rfuns{normal_form,...},...}, t) = (thy, rrls, t);
436 (*fixme false*) chk_prepat thy erls prepat t;
437 "----- chk_prepat ---";
438 val (thy, erls, prepat, t) = (thy, erls, prepat, t);
439 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 ctxt (i+1)
444 (map (Envir.subst_term subst) pres)
447 handle Pattern.MATCH => false;
448 fun scan_ _ [] = false (*scan_ NEVER called by []*)
449 | scan_ f (pp::pps) = if f pp then true
451 tracing "=== poly.sml: scan_ chk prepat begin";
453 tracing "=== poly.sml: scan_ chk prepat end";
456 (*reestablish...*) val t = TermC.str2term "x \<up> 2 * x";
457 val [(pres, pat)] = prepat;
458 val subst: Type.tyenv * Envir.tenv =
459 Pattern.match thy (pat, t)
460 (Vartab.empty, Vartab.empty);
462 (*fixme: asms = ["p is_multUnordered"]...instantiate*)
463 "----- eval__true ---";
464 val asms = (map (Envir.subst_term subst) pres);
465 if UnparseC.terms asms = "[\"x \<up> 2 * x is_multUnordered\"]" then ()
466 else error "rewrite.sml: diff. is_multUnordered, asms";
467 val (thy, i, asms, bdv, rls) =
468 (thy, (i+1), [TermC.str2term "(x \<up> 2 * x) is_multUnordered"],
470 case eval__true ctxt i asms bdv rls of
472 | _ => error "rewrite.sml: diff. is_multUnordered, eval__true";
474 "----------- 2011 thms with axclasses ----------------------------------------------------------";
475 "----------- 2011 thms with axclasses ----------------------------------------------------------";
476 "----------- 2011 thms with axclasses ----------------------------------------------------------";
477 val thm = @{thm div_by_1};
478 val prop = Thm.prop_of thm;
479 TermC.atomty prop; (*Type 'a*)
480 val t = TermC.str2term "(2*x)/1"; (*Type real*)
482 val (thy, ro, er, inst) =
483 (@{theory "Isac_Knowledge"}, tless_true, eval_rls, [(@{term "bdv::real"}, @{term "x::real"})]);
484 val SOME (t, _) = rewrite_ ctxt ro er true thm t; (*real TermC.matches 'a ?via ring? etc*)
486 "----------- fun rewrite_set_ .. RatEq_eliminate step into to fun chk --------------------------";
487 "----------- fun rewrite_set_ .. RatEq_eliminate step into to fun chk --------------------------";
488 "----------- fun rewrite_set_ .. RatEq_eliminate step into to fun chk --------------------------";
489 val thy = @{theory RatEq};
490 val ctxt = Proof_Context.init_global thy;
491 val SOME t = TermC.parseNEW ctxt "(3 + -1 * x + x \<up> 2) / (9 * x + -6 * x \<up> 2 + x \<up> 3) = 1 / x";
492 val rls = assoc_rls "RatEq_eliminate"
494 val SOME (t''''', asm''''') =
495 rewrite_set_ ctxt true rls t;
496 "~~~~~ fun rewrite_set_ , args:"; val (thy, bool, rls, term) = (thy, true, rls, t);
497 rewrite__set_ ctxt 1 bool [] rls term;
498 "~~~~~ and rewrite__set_ , args:"; val (thy, i, put_asm, bdv, rls, ct)
499 = (thy, 1, bool, []:Subst.T, rls, term);
501 (*/------- outcomment this code: otherwise the re-definition could infect tests lateron ------\ * )
502 datatype switch = Applicable.Yes | Noap;
503 fun rew_once _ asm ct Noap [] = (ct, asm) (* ?TODO unify with Prog_Expr.rew_once? *)
504 | rew_once ruls asm ct Applicable.Yes [] =
505 (case rls of Rule_Set.Repeat _ => rew_once ruls asm ct Noap ruls
506 | Rule_Set.Sequence _ => (ct, asm)
507 | rls => raise ERROR ("rew_once not appl. to \"" ^ Rule_Set.id rls ^ "\""))
508 | rew_once ruls asm ct apno (rul :: thms) =
510 Rule.Thm (thmid, thm) =>
511 (trace1 i (" try thm: " ^ thmid);
512 case rewrite__ thy (i + 1) bdv ((snd o #rew_ord o Rule.Rule_Set.rep) rls)
513 ((#erls o Rule.Rule_Set.rep) rls) put_asm thm ct of
514 NONE => rew_once ruls asm ct apno thms
515 | SOME (ct', asm') =>
516 (trace1 i (" rewrites to: " ^ UnparseC.term_in_thy thy ct');
517 rew_once ruls (union (op =) asm asm') ct' Applicable.Yes (rul :: thms)))
518 (* once again try the same rule, e.g. associativity against "()"*)
519 | Rule.Eval (cc as (op_, _)) =>
520 let val _= trace1 i (" try calc: " ^ op_ ^ "'")
521 val ct = TermC.uminus_to_string ct (*WN190312: superfluous?*)
522 in case Eval.adhoc_thm thy cc ct of
523 NONE => rew_once ruls asm ct apno thms
526 val pairopt = rewrite__ thy (i + 1) bdv ((snd o #rew_ord o Rule.Rule_Set.rep) rls)
527 ((#erls o Rule.Rule_Set.rep) rls) put_asm thm' ct;
528 val _ = if pairopt <> NONE then () else error ("rewrite_set_, rewrite_ \"" ^
529 ThmC.string_of_thm thm' ^ "\" " ^ UnparseC.term_in_thy thy ct ^ " = NONE")
530 val _ = trace1 i (" calc. to: " ^ UnparseC.term_in_thy thy ((fst o the) pairopt))
531 in rew_once ruls asm ((fst o the) pairopt) Applicable.Yes (rul :: thms) end
533 | Rule.Cal1 (cc as (op_, _)) =>
534 let val _= trace1 i (" try cal1: " ^ op_ ^ "'");
535 val ct = TermC.uminus_to_string ct
536 in case Eval.adhoc_thm1_ thy cc ct of
540 val pairopt = 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;
542 val _ = if pairopt <> NONE then () else error ("rewrite_set_, rewrite_ \"" ^
543 ThmC.string_of_thm thm' ^ "\" " ^ UnparseC.term_in_thy thy ct ^ " = NONE")
544 val _ = trace1 i (" cal1. to: " ^ UnparseC.term_in_thy thy ((fst o the) pairopt))
548 (case rewrite__set_ thy (i + 1) put_asm bdv rls' ct of
549 SOME (t', asm') => rew_once ruls (union (op =) asm asm') t' Applicable.Yes thms
550 | NONE => rew_once ruls asm ct apno thms)
551 | r => raise ERROR ("rew_once not appl. to \"" ^ Rule.Rule.to_string r ^ "\"");
552 val ruls = (#rules o Rule.Rule_Set.rep) rls;
553 (* val _ = trace i (" rls: " ^ Rule_Set.id rls ^ " on: " ^ UnparseC.term_in_thy thy ct)*)
554 val (ct', asm') = rew_once ruls [] ct Noap ruls;
555 "~~~~~ fun rew_once , args:"; val (ruls, asm, ct, apno, (rul :: thms))
556 = (ruls, []:term list, ct, Noap, ruls);
557 val Rule.Thm (thmid, thm) = (*case*) rul (*of*);
559 val SOME (ct', asm') = (*case*)
560 rewrite__ thy (i + 1) bdv ((snd o #rew_ord o Rule.Rule_Set.rep) rls)
561 ((#erls o Rule.Rule_Set.rep) rls) put_asm thm ct (*of*);
562 "~~~~~ fun rewrite__ , args:"; val (thy, i, bdv, tless, rls, put_asm, thm, ct)
563 = (thy, (i + 1), bdv, ((snd o #rew_ord o Rule.Rule_Set.rep) rls),
564 ((#erls o Rule.Rule_Set.rep) rls), put_asm, thm, ct);
566 val (t', asms, _ (*lrd*), rew) =
567 rew_sub thy i bdv tless rls put_asm ([(*root of the term*)]: TermC.path)
568 (((TermC.inst_bdv bdv) o Eval.norm o Thm.prop_of) thm) ct;
569 "~~~~~ and rew_sub , args:"; val (thy, i, bdv, tless, rls, put_asm, lrd, r, t)
570 = (thy, i, bdv, tless, rls, put_asm, ([(*root of the term*)]: TermC.path),
571 (((TermC.inst_bdv bdv) o Eval.norm o Thm.prop_of) thm), ct);
572 val (lhs, rhs) = (HOLogic.dest_eq o HOLogic.dest_Trueprop o Logic.strip_imp_concl) r
573 val r' = Envir.subst_term (Pattern.match thy (lhs, t) (Vartab.empty, Vartab.empty)) r
575 (*+*)if UnparseC.term r' =
576 (*+*) "\<lbrakk>9 * x + -6 * x \<up> 2 + x \<up> 3 \<noteq> 0; x \<noteq> 0\<rbrakk>\n" ^
577 (*+*) "\<Longrightarrow> ((3 + -1 * x + x \<up> 2) /\n" ^
578 (*+*) " (9 * x + -6 * x \<up> 2 + x \<up> 3) =\n" ^
579 (*+*) " 1 / x) =\n" ^
580 (*+*) " ((3 + -1 * x + x \<up> 2) * x =\n" ^
581 (*+*) " 1 * (9 * x + -6 * x \<up> 2 + x \<up> 3))"
582 (*+*)then () else error "instantiated rule CHANGED";
584 val p' = map HOLogic.dest_Trueprop ((fst o Logic.strip_prems) (Logic.count_prems r', [], r'))
586 (*+*)if map UnparseC.term p' = ["x \<noteq> 0", "9 * x + -6 * x \<up> 2 + x \<up> 3 \<noteq> 0"]
587 (*+*)then () else error "stored assumptions CHANGED";
589 val t' = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop o Logic.strip_imp_concl) r'
591 (*+*)if UnparseC.term t' = "(3 + -1 * x + x \<up> 2) * x = 1 * (9 * x + -6 * x \<up> 2 + x \<up> 3)"
592 (*+*)then () else error "rewritten term (an equality) CHANGED";
594 val (simpl_p', nofalse) =
595 eval__true thy (i + 1) p' bdv rls;
596 "~~~~~ and eval__true , args:"; val (thy, i, asms, bdv, rls) = (thy, (i + 1), p', bdv, rls);
597 (*if*) asms = [@{term True}] orelse asms = [] (*else*);
599 (*+*)if map UnparseC.term asms = ["x \<noteq> 0", "9 * x + -6 * x \<up> 2 + x \<up> 3 \<noteq> 0"]
600 (*+*)then () else error "asms before chk CHANGED";
602 fun chk indets [] = (indets, true) (*return asms<>True until false*)
603 | chk indets (a :: asms) =
604 (case rewrite__set_ thy (i + 1) false bdv rls a of
605 NONE => (chk (indets @ [a]) asms)
607 if t = @{term True} then (chk (indets @ a') asms)
608 else if t = @{term False} then ([], false)
609 (*asm false .. thm not applied \<up> ; continue until False vvv*)
610 else chk (indets @ [t] @ a') asms);
613 chk [] asms; (*return from eval__true*);
614 "~~~~~ fun chk , args:"; val (indets, (a :: asms)) = ([], asms);
616 (*+*)val Rule_Set.Repeat {id = "rateq_erls", rules, ...} = rls;
618 (*+*) [Eval (\<^const_name>\<open>divide\<close>, fn),
619 (*+*) Thm ("minus_divide_left", "- ?a1 / ?b1 = - (?a1 / ?b1)"),
621 (*+*) Eval (\<^const_name>\<open>HOL.eq\<close>, fn),
622 (*+*) Thm ("not_true", "(\<not> True) = False"),
623 (*+*) Thm ("not_false", "(\<not> False) = True"),
625 (*+*) Eval (\<^const_name>\<open>realpow\<close>, fn),
626 (*+*) Eval ("RatEq.is_ratequation_in", fn)]:
628 (*+*)chk: term list -> term list -> term list * bool
630 rewrite__set_ thy (i + 1) false bdv rls a (*of*);
632 (*+*)Rewrite.trace_on := false; (*true false*)
634 (*this was False; vvvv--- means: indeterminate*)
635 val (* SOME (t, a') *)NONE = (*case*)
636 rewrite__set_ thy (i + 1) false bdv rls a (*of*);
638 (*+*)UnparseC.term a = "x \<noteq> 0"; (* rewrite__set_ \<rightarrow> @{term True} ----------------- SHOULD BE indet !*)
641 #### rls: rateq_erls on: x \<noteq> 0
643 ##### try calc: HOL.eq' <<<------------------------------- here the error comes from
644 ===== calc. to: ~ False <<<------------------------------- \<not> x = 0 is NOT False
645 ##### try calc: HOL.eq'
646 ##### try thm: not_true
647 ##### try thm: not_false
648 ===== rewrites to: True <<<------------------------------- so x \<noteq> 0 is NOT True
649 and True, False are NOT stored ...
651 ### asms accepted: [x \<noteq> 0] stored: []
653 Rewrite.trace_on := false; (*true false*)
654 ( *\------- outcomment this code: otherwise the re-definition could infect tests lateron ------/*)
657 "----------- fun rewrite_ down to Pattern.match ------------------------------------------------";
658 "----------- fun rewrite_ down to Pattern.match ------------------------------------------------";
659 "----------- fun rewrite_ down to Pattern.match ------------------------------------------------";
660 "~~~~~ fun rewrite_ , args:"; val (thy, rew_ord, erls, bool, thm, term) =
661 (@{theory}, Rewrite_Ord.function_empty, Rule_Set.empty, false, @{thm distrib_left}, @{term "x * (y + z) :: int"});
662 "~~~~~ fun rewrite__ , args:"; val (thy, i, bdv, tless, rls, put_asm, thm, ct) =
663 (thy, 1, [], rew_ord, erls, bool, thm, term);
664 "~~~~~ and rew_sub , args:"; val (thy, i, bdv, tless, rls, put_asm, lrd, r, t) =
665 (thy, i, bdv, tless, rls, put_asm, [], TermC.inst_bdv bdv (Eval.norm (Thm.prop_of thm)), ct)
666 val (lhss, rhss) = (HOLogic.dest_eq o Logic.strip_imp_concl o HOLogic.dest_Trueprop) r
667 val r' = Envir.subst_term (Pattern.match thy (lhss, t) (Vartab.empty, Vartab.empty)) r
668 val p' = map HOLogic.dest_Trueprop ((fst o Logic.strip_prems) (Logic.count_prems r', [], r'))
669 val t' = (snd o HOLogic.dest_eq o Logic.strip_imp_concl o HOLogic.dest_Trueprop) r'
671 if UnparseC.term lhss = "?a * (?b + ?c)" andalso UnparseC.term t = "x * (y + z)" then ()
672 else error "ARGS FOR Pattern.match CHANGED";
673 val match = Pattern.match thy (lhss, t) (Vartab.empty, Vartab.empty);
674 if (Envir.subst_term match r |> UnparseC.term) = "x * (y + z) = x * y + x * z" then ()
675 else error "Pattern.match CHANGED";
677 "----------- fun rewrite_set_ .. norm_equation, ~~~~~ fun rewrite_set_ -------------------------";
678 "----------- fun rewrite_set_ .. norm_equation, ~~~~~ fun rewrite_set_ -------------------------";
679 "----------- fun rewrite_set_ .. norm_equation, ~~~~~ fun rewrite_set_ -------------------------";
680 (* norm_equation is defined in Test.thy, other rls see Knowledg/**)
682 val rls = norm_equation;
683 val term = TermC.str2term "x + 1 = 2";
685 (**)val SOME (t, asm) = rewrite_set_ ctxt false rls term;
686 (** )##### try thm: "root_ge0"
687 exception TERM raised (line 271 of "~~/src/HOL/Tools/hologic.ML"):
689 0 \<le> ?a \<Longrightarrow> (0 \<le> sqrt ?a) = True( **)
690 if UnparseC.term t = "x + 1 + - 1 * 2 = 0" then () else error "rewrite_set_ norm_equation CHANGED";
692 "~~~~~ fun rewrite_set_ , args:"; val (thy, bool, rls, term) = (thy, false, rls, term);
693 "~~~~~ and rewrite__set_ , args:"; val (thy, i, put_asm, bdv, rls, ct) =
694 (thy, 1, bool, []: Subst.T, rls, term);
695 (*deleted after error detection*)