//reduce the number of TermC.parse*; "//"means: tests broken .
broken tests are outcommented with "reduce the number of TermC.parse*"
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'' thy "((r + u) + t) + s";
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 (*broken with "reduce the number of TermC.parse*-------exception MATCH---------------------\\
56 TOODOO ERROR exception MATCH raised (line 284 of "pattern.ML)
58 (Pattern.match thy (LHS, t) (Vartab.empty, Vartab.empty));
59 val (rew, RHS) = (Envir.subst_term
60 (Pattern.match thy (LHS, t) (Vartab.empty, Vartab.empty)) rtm, rtm);
61 (*lookup in isabelle?trace?response...*)
62 writeln(Syntax.string_of_term ctxt rew);
63 writeln(Syntax.string_of_term ctxt RHS);
64 "===== rewriting: prep insertion into rew_sub";
65 val thy = @{theory Complex_Main};
66 val ctxt = @{context};
67 val thm = @{thm nonzero_divide_mult_cancel_right};
68 val r = Thm.prop_of thm;
69 val tm = @{term "x / (2 * x)::real"};
71 val (LHS, RHS) = (HOLogic.dest_eq o HOLogic.dest_Trueprop
72 o Logic.strip_imp_concl) r;
73 val r' = Envir.subst_term (Pattern.match thy (LHS, tm)
74 (Vartab.empty, Vartab.empty)) r;
75 val p' = (fst o Logic.strip_prems) (Logic.count_prems r', [], r');
76 val t' = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop
77 o Logic.strip_imp_concl) r';
79 (*is displayed on top of <response> buffer...*)
80 Pretty.writeln (Proof_Context.pretty_term_abbrev @{context} r');
81 Pretty.writeln (Proof_Context.pretty_term_abbrev @{context} t');
82 --broken with "reduce the number of TermC.parse*------------------------------------------//( **)
84 "----------- test rewriting without Isac's thys ------------------------------------------------";
85 "----------- test rewriting without Isac's thys ------------------------------------------------";
86 "----------- test rewriting without Isac's thys ------------------------------------------------";
88 "===== rewriting with Isabelle2009-1 only, i.e without isac-hacks";
89 val thy = @{theory Complex_Main};
90 val ctxt = @{context};
91 val thm = @{thm add.commute};
92 val tm = @{term "x + y*z::real"};
94 val SOME (r,_) = (rewrite_ thy dummy_ord Rule_Set.empty false thm tm);
95 (*is displayed on _TOP_ of <response> buffer...*)
96 Pretty.writeln (Proof_Context.pretty_term_abbrev @{context} r);
97 if r = @{term "y*z + x::real"}
98 then () else error "rewrite.sml diff.result in rewriting";
100 "----- rewriting a subterm";
101 val tm = @{term "w*(x + y*z)::real"};
103 val SOME (r, _) = (rewrite_ thy dummy_ord Rule_Set.empty false thm tm);
105 "----- ordered rewriting";
106 fun tord (_:subst) pp = LibraryC.termless pp;
107 if tord [] (@{term "x + y*z::real"}, @{term "y*z + x::real"}) then ()
108 else error "rewrite.sml diff.behav. in ord.rewr.";
110 val NONE = (rewrite_ thy tord Rule_Set.empty false thm tm);
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);
118 "----------- conditional rewriting without Isac's thys -----------------------------------------";
119 "----------- conditional rewriting without Isac's thys -----------------------------------------";
120 "----------- 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}; (* = "?b \<noteq> 0 \<Longrightarrow> ?b / (?a * ?b) = 1 / ?a":*)
125 val rule = Thm.prop_of thm;
126 val tm = @{term "x / (2 * x)::real"};
127 val prem = Logic.strip_imp_prems rule;
128 val nps = Logic.count_prems rule;
129 val prems = Logic.strip_prems (nps, [], rule);
131 val eq = Logic.strip_imp_concl rule;
132 val (LHS, RHS) = (HOLogic.dest_eq o HOLogic.dest_Trueprop) eq;
134 val mtcs = Pattern.match thy (LHS, tm) (Vartab.empty, Vartab.empty);
135 val rule' = Envir.subst_term mtcs rule;
137 val prems' = (fst o Logic.strip_prems) (Logic.count_prems rule', [], rule');
138 val RHS' = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop o Logic.strip_imp_concl) rule';
140 (rule' |> UnparseC.term) = "x \<noteq> 0 \<Longrightarrow> x / (2 * x) = 1 / 2";
143 (rule' |> Logic.strip_imp_concl |> UnparseC.term) = "x / (2 * x) = 1 / 2";
144 rule' |> Logic.strip_imp_concl;
146 (rule' |> Logic.strip_imp_concl |> UnparseC.term) = "x / (2 * x) = 1 / 2";
147 rule' |> Logic.strip_imp_concl;
150 "----------- conditional rewriting creating an assumption---------------------------------------";
151 "----------- conditional rewriting creating an assumption---------------------------------------";
152 "----------- conditional rewriting creating an assumption---------------------------------------";
153 val thm = @{thm nonzero_divide_mult_cancel_right};
154 val tm = @{term "x / (2 * x)::real"};
156 val SOME (rew, asm) = (rewrite_ thy dummy_ord Rule_Set.empty false thm tm);
158 if rew = @{term "1 / 2::real"} then () (* the rewrite is _NO_ Trueprop *)
159 else error "rewrite.sml diff.result in cond.rew.";
161 if hd asm = @{term "x \<noteq> (0::real)"} (* dropped Trueprop $ ...*)
162 then () else error "rewrite.sml diff.asm in cond.rew.";
163 "----- conditional rewriting immediately: can only be done with ";
164 "------Isabelle numerals, because erls cannot handle them yet.";
167 "----------- conditional rewriting creating an assumption, ~~~~~ fun rewrite_ ------------------";
168 "----------- conditional rewriting creating an assumption, ~~~~~ fun rewrite_ ------------------";
169 "----------- conditional rewriting creating an assumption, ~~~~~ fun rewrite_ ------------------";
170 val thm = @{thm nonzero_divide_mult_cancel_right};(* = "?b \<noteq> 0 \<Longrightarrow> ?b / (?a * ?b) = 1 / ?a"*)
171 val tm = @{term "x / (2 * x)::real"};
174 (**)val SOME (rew, asm) = (rewrite_ thy dummy_ord Rule_Set.empty false thm tm);
175 (** )exception TERM raised (line 196 of "~~/src/HOL/Tools/hologic.ML"):
177 ?b \<noteq> 0 \<Longrightarrow> ?b / (?a * ?b) = 1 / ?a( **)
178 "~~~~~ fun rewrite_ , args:"; val (thy, rew_ord, erls, bool, thm, term) =
179 (thy, dummy_ord, erls, false, thm, tm);
180 "~~~~~ fun rewrite__ , args:"; val (thy, i, bdv, tless, rls, put_asm, thm, ct) =
181 (thy, 1, []: (term * term) list, rew_ord, erls, bool, thm, term);
183 (**) val (t', asms, _(*lrd*), rew) = rew_sub thy i bdv tless rls put_asm ([(*root of the term*)]: TermC.path)
184 (TermC.inst_bdv bdv (Eval.norm (Thm.prop_of thm))) ct;
185 (** )exception TERM raised (line 196 of "~~/src/HOL/Tools/hologic.ML"):
187 ?b \<noteq> 0 \<Longrightarrow> ?b / (?a * ?b) = 1 / ?a( **)
188 "~~~~~ fun rew_sub , args:"; val (thy, i, bdv, tless, rls, put_asm, lrd, r, t) =
189 (thy, i, bdv, tless, rls, put_asm, ([(*root of the term*)]: TermC.path),
190 (TermC.inst_bdv bdv (Eval.norm (Thm.prop_of thm))), ct);
191 (*+*)UnparseC.term r = "?b \<noteq> (0::?'a) \<Longrightarrow> ?b / (?a * ?b) = (1::?'a) / ?a";
193 val (lhs, rhs) = (HOLogic.dest_eq o HOLogic.dest_Trueprop o Logic.strip_imp_concl) r;
194 (*+*)(UnparseC.term lhs, UnparseC.term rhs) = ("?b / (?a * ?b)", "(1::?'a) / ?a");
195 val r' = (Envir.subst_term (Pattern.match thy (lhs, t) (Vartab.empty, Vartab.empty)) r)
196 handle Pattern.MATCH => raise NO_REWRITE;
197 val p' = map HOLogic.dest_Trueprop ((fst o Logic.strip_prems) (Logic.count_prems r', [], r'));
198 (*+*)UnparseC.term r' = "x \<noteq> 0 \<Longrightarrow> x / (2 * x) = 1 / 2";
200 val t' = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop o Logic.strip_imp_concl) r'
201 val _ = trace_in2 i "eval asms" thy r';
202 val (simpl_p', nofalse) = eval__true thy (i + 1) p' bdv rls;
203 (*if*) nofalse (*then*);
204 val (t'', p'') = (trace_in4 i "asms accepted" thy p' simpl_p'; (t',simpl_p'));
205 (*## asms accepted: [x \<noteq> 0] stored: [x \<noteq> 0] *)
207 (*+*)if (UnparseC.term t'', map UnparseC.term p'') = ("1 / 2", ["x \<noteq> 0"]) then ()
208 (*+*)else error "conditional rewriting x \<noteq> 0 \<Longrightarrow> x / (2 * x) = 1 / 2 CHANGED";
211 "----------- step through 'and rew_sub': ----------------";
212 "----------- step through 'and rew_sub': ----------------";
213 "----------- step through 'and rew_sub': ----------------";
214 (*and make asms without Trueprop, beginning with the result:*)
215 val tm = @{term "x / (2 * x)::real"};
216 val (t', asm, _, _) = rew_sub thy 0 [] dummy_ord Rule_Set.empty true [] (Thm.prop_of thm) tm;
217 (*show_types := false;*)
218 "----- evaluate arguments";
219 val (thy, i, bdv, tless, rls, put_asm, lrd, r, t) =
220 (thy, 0, [], dummy_ord, Rule_Set.empty, true, [], (Thm.prop_of thm), tm);
221 "----- step 1: LHS, RHS of rule";
222 val (LHS, RHS) = (HOLogic.dest_eq o HOLogic.dest_Trueprop
223 o Logic.strip_imp_concl) r;
224 UnparseC.term r = "?b \<noteq> (0::?'a) \<Longrightarrow> ?b / (?a * ?b) = (1::?'a) / ?a";
225 UnparseC.term LHS = "?b / (?a * ?b)"; UnparseC.term RHS = "(1::?'a) / ?a";
226 "----- step 2: the rule instantiated";
227 val r' = Envir.subst_term
228 (Pattern.match thy (LHS, t) (Vartab.empty, Vartab.empty)) r;
229 UnparseC.term r' = "x \<noteq> 0 \<Longrightarrow> x / (2 * x) = 1 / 2";
230 "----- step 3: get the (instantiated) assumption(s)";
231 val p' = (fst o Logic.strip_prems) (Logic.count_prems r', [], r');
232 UnparseC.term (hd p') = "x \<noteq> 0";
233 "=====vvv make asms without Trueprop ---vvv";
234 val p' = map HOLogic.dest_Trueprop ((fst o Logic.strip_prems)
235 (Logic.count_prems r', [], r'));
237 [Const (\<^const_name>\<open>Not\<close>, _) $ (Const (\<^const_name>\<open>HOL.eq\<close>, _)
238 $ Free ("x", _) $ Const (\<^const_name>\<open>zero_class.zero\<close>, _))] => ()
239 | _ => error "rewrite.sml assumption changed";
240 "===== \<up> make asms without Trueprop --- \<up> ";
241 "----- step 4: get the (instantiated) RHS";
242 val t' = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop
243 o Logic.strip_imp_concl) r';
244 UnparseC.term t' = "1 / 2";
246 "----------- step through 'fun rewrite_terms_' ------------------------------------------------";
247 "----------- step through 'fun rewrite_terms_' ------------------------------------------------";
248 "----------- step through 'fun rewrite_terms_' ------------------------------------------------";
249 "----- step 0: args for rewrite_terms_, local fun";
250 val (thy, ord, erls, equs, t) =
251 (@{theory "Biegelinie"}, dummy_ord, Rule_Set.Empty, [TermC.str2term "x = 0"],
252 TermC.str2term "M_b x = -1 * q_0 * x \<up> 2 / 2 + x * c + c_2");
253 "----- step 1: args for rew_";
254 val ((t', asm'), (rules as r::rs), t) = ((TermC.empty, []), equs, t);
255 "----- step 2: rew_sub";
256 rew_sub thy 1 [] ord erls false [] (HOLogic.Trueprop $ r) t;
257 "----- step 3: step through rew_sub -- inefficient: goes into subterms";
260 val SOME (t', _) = rewrite_terms_ thy dummy_ord Rule_Set.Empty equs t;
261 writeln "---------- rewrite_terms_ 1---------------------------";
262 if UnparseC.term t' = "M_b 0 = - 1 * q_0 * 0 \<up> 2 / 2 + 0 * c + c_2" then ()
263 else error "rewrite.sml rewrite_terms_ [x = 0]";
265 val equs = [TermC.str2term "M_b 0 = 0"];
266 val t = TermC.str2term "M_b 0 = - 1 * q_0 * 0 \<up> 2 / 2 + 0 * c + c_2";
267 val SOME (t', _) = rewrite_terms_ thy dummy_ord Rule_Set.Empty equs t;
268 writeln "---------- rewrite_terms_ 2---------------------------";
269 if UnparseC.term t' = "0 = - 1 * q_0 * 0 \<up> 2 / 2 + 0 * c + c_2" then ()
270 else error "rewrite.sml rewrite_terms_ [M_b 0 = 0]";
272 val equs = [TermC.str2term "x = 0", TermC.str2term"M_b 0 = 0"];
273 val t = TermC.str2term "M_b x = - 1 * q_0 * x \<up> 2 / 2 + x * c + c_2";
274 val SOME (t', _) = rewrite_terms_ thy dummy_ord Rule_Set.Empty equs t;
275 writeln "---------- rewrite_terms_ 3---------------------------";
276 if UnparseC.term t' = "0 = - 1 * q_0 * 0 \<up> 2 / 2 + 0 * c + c_2" then ()
277 else error "rewrite.sml rewrite_terms_ [x = 0, M_b 0 = 0]";
280 "----------- rewrite_inst_ bdvs ----------------------------------------------------------------";
281 "----------- rewrite_inst_ bdvs ----------------------------------------------------------------";
282 "----------- rewrite_inst_ bdvs ----------------------------------------------------------------";
283 (*see smltest/Scripts/term_G.sml: inst_bdv 2*)
284 val t = TermC.str2term"-1 * (q_0 * L \<up> 2) / 2 + (L * c_3 + c_4) = 0";
285 val bdvs = [(TermC.str2term"bdv_1",TermC.str2term"c"),
286 (TermC.str2term"bdv_2",TermC.str2term"c_2"),
287 (TermC.str2term"bdv_3",TermC.str2term"c_3"),
288 (TermC.str2term"bdv_4",TermC.str2term"c_4")];
289 (*------------ outcommented WN071210, after inclusion into ROOT.ML
291 rewrite_inst_ thy e_rew_ord
292 (Rule_Set.append_rules "erls_isolate_bdvs" Rule_Set.empty
293 [(Eval ("EqSystem.occur_exactly_in",
294 eval_occur_exactly_in
295 "#eval_occur_exactly_in_"))
297 false bdvs (ThmC.numerals_to_Free @{separate_bdvs_add) t;
298 (writeln o UnparseC.term) t;
299 if UnparseC.term t = "L * c_3 + c_4 = 0 + -1 * (-1 * (q_0 * L \<up> 2) / 2)"
300 then () else error "rewrite.sml rewrite_inst_ bdvs";
301 > Rewrite.trace_on:=true;false
302 Rewrite.trace_on:=false;--------------------------------------------*)
305 "----------- compare all prepat's existing 2010 ------------------------------------------------";
306 "----------- compare all prepat's existing 2010 ------------------------------------------------";
307 "----------- compare all prepat's existing 2010 ------------------------------------------------";
308 val thy = @{theory "Isac_Knowledge"};
309 val t = @{term "a + b * x = (0 ::real)"};
310 val pat = TermC.parse_patt thy "?l = (?r ::real)";
311 val precond = TermC.parse_patt thy "is_polynomial (?l::real)";(*no infix def*)
312 val precond = TermC.parse_patt thy "(?l::real) is_expanded";
314 val inst = Pattern.match thy (pat, t) (Vartab.empty, Vartab.empty);
315 val preinst = Envir.subst_term inst precond;
316 UnparseC.term preinst;
318 "===== Rational.thy: cancel ===";
319 (* pat matched with the current term gives an environment
320 (or not: hen the Rrls not applied);
321 if pre1 and pre2 evaluate to @{term True} in this environment,
322 then the Rrls is applied. *)
323 val t = TermC.str2term "(a + b) / c ::real";
324 val pat = TermC.parse_patt thy "?r / ?s ::real";
325 val pres = [TermC.parse_patt thy "?r is_expanded", TermC.parse_patt thy "?s is_expanded"];
326 val prepat = [(pres, pat)];
327 val erls = rational_erls;
328 (* erls got from Rrls {erls, prepat, scr = Rfuns {normal_form, ...}, ...} *)
330 val subst = Pattern.match thy (pat, t) (Vartab.empty, Vartab.empty);
331 val asms = map (Envir.subst_term subst) pres;
332 if UnparseC.terms asms = "[\"a + b is_expanded\", \"c is_expanded\"]"
333 then () else error "rewrite.sml: prepat cancel subst";
335 if ([], true) = eval__true thy 0 asms [] erls
336 then () else error "rewrite.sml: prepat cancel eval__true";
338 "===== Rational.thy: add_fractions_p ===";
339 (* if each pat* TermC.matches with the current term, the Rrls is applied
340 (there are no preconditions to be checked, they are @{term True}) *)
341 val t = TermC.str2term "a / b + 1 / 2";
342 val pat = TermC.parse_patt thy "?r / ?s + ?u / ?v";
343 val pres = [@{term True}];
344 val prepat = [(pres, pat)];
345 val erls = rational_erls;
346 (* erls got from Rrls {erls, prepat, scr = Rfuns {normal_form, ...}, ...} *)
348 val subst = Pattern.match thy (pat, t) (Vartab.empty, Vartab.empty);
349 if ([], true) = eval__true thy 0 (map (Envir.subst_term subst) pres) [] erls
350 then () else error "rewrite.sml: prepat add_fractions_p";
352 "===== Poly.thy: order_mult_ ===";
353 (* ?p matched with the current term gives an environment,
354 which evaluates (the instantiated) "p is_multUnordered" to true*)
355 val t = TermC.str2term "x \<up> 2 * x";
356 val pat = TermC.parse_patt thy "?p :: real"
357 val pres = [TermC.parse_patt thy "?p is_multUnordered"];
358 val prepat = [(pres, pat)];
359 val erls = Rule_Set.append_rules "Rule_Set.empty-is_multUnordered" Rule_Set.empty
360 [Eval ("Poly.is_multUnordered",
361 eval_is_multUnordered "")];
363 val subst = Pattern.match thy (pat, t) (Vartab.empty, Vartab.empty);
364 val asms = map (Envir.subst_term subst) pres;
365 if UnparseC.terms asms = "[\"x \<up> 2 * x is_multUnordered\"]"
366 then () else error "rewrite.sml: prepat order_mult_ subst";
368 if ([], true) = eval__true thy 0 asms [] erls
369 then () else error "rewrite.sml: prepat order_mult_ eval__true";
372 "----------- fun app_rev, Rrls, ----------------------------------------------------------------";
373 "----------- fun app_rev, Rrls, ----------------------------------------------------------------";
374 "----------- fun app_rev, Rrls, ----------------------------------------------------------------";
375 val t = TermC.str2term "x \<up> 2 * x";
377 if is_multUnordered t then () else error "rewrite.sml diff. is_multUnordered 2";
378 val tm = TermC.str2term "(x \<up> 2 * x) is_multUnordered";
380 (*+*)case eval_is_multUnordered "testid" "" tm thy of
382 (*+*) ("testidx \<up> 2 * x_",
383 (*+*) Const (\<^const_name>\<open>Trueprop\<close>, _) $
384 (*+*) (Const (\<^const_name>\<open>HOL.eq\<close>, _) $
385 (*+*) (Const (\<^const_name>\<open>is_multUnordered\<close>, _) $
386 (*+*) (Const (\<^const_name>\<open>times\<close>, _) $
387 (*+*) (Const (\<^const_name>\<open>powr\<close>, _) $ Free ("x", _) $ _ ) $ Free ("x", _))) $
388 (*+*) Const (\<^const_name>\<open>True\<close>, _))) => ()
389 (*+*)(* ^^^^^^ compare ---vvv *)
390 (*+*)| _ => error "rewrite.sml diff. eval_is_multUnordered 2b CHANGED";
393 eval_is_multUnordered "testid" "" tm thy;
395 case eval_is_multUnordered "testid" "" tm thy of
396 SOME (_, Const (\<^const_name>\<open>Trueprop\<close>, _) $
397 (Const (\<^const_name>\<open>HOL.eq\<close>, _) $
398 (Const (\<^const_name>\<open>is_multUnordered\<close>, _) $ _) $
399 Const (\<^const_name>\<open>True\<close>, _))) => ()
400 | _ => error "rewrite.sml diff. eval_is_multUnordered 2b";
402 tracing "----- begin rewrite x \<up> 2 * x ---"; Rewrite.trace_on := false; (*true false*)
403 val SOME (t', _) = rewrite_set_ thy true order_mult_ t;
404 tracing "----- end rewrite x \<up> 2 * x ---"; Rewrite.trace_on := false; (*true false*)
405 if UnparseC.term t' = "x * x \<up> 2" then ()
406 else error "rewrite.sml Poly.is_multUnordered doesn't work";
408 (* for achieving the previous result, the following code was taken apart *)
409 "----- rewrite__set_ ---";
410 val (thy, i, _, _, (rrls as Rrls _), t) = (thy, 0, true, [], order_mult_, tm);
411 val (t', asm, rew) = app_rev thy (i+1) rrls t;
413 val (thy, i, rrls, t) = (thy, (i+1), rrls, t);
414 fun chk_prepat thy erls [] t = true
415 | chk_prepat thy erls prepat t =
416 let fun chk (pres, pat) =
417 (let val subst: Type.tyenv * Envir.tenv =
418 Pattern.match thy (pat, t)
419 (Vartab.empty, Vartab.empty)
420 in snd (eval__true thy (i+1)
421 (map (Envir.subst_term subst) pres)
424 handle Pattern.MATCH => false
425 fun scan_ f [] = false (*scan_ NEVER called by []*)
426 | scan_ f (pp::pps) = if f pp then true
428 in scan_ chk prepat end;
430 (*.apply the normal_form of a rev-set.*)
431 fun app_rev' thy (Rrls{erls,prepat,scr=Rfuns{normal_form,...},...}) t =
432 if chk_prepat thy erls prepat t
433 then ((*tracing("### app_rev': t = "^(UnparseC.term t));*)
436 (*fixme val NONE = app_rev' thy rrls t;*)
437 "----- app_rev' ---";
438 val (thy, Rrls{erls,prepat,scr=Rfuns{normal_form,...},...}, t) = (thy, rrls, t);
439 (*fixme false*) chk_prepat thy erls prepat t;
440 "----- chk_prepat ---";
441 val (thy, erls, prepat, t) = (thy, erls, prepat, t);
442 fun chk (pres, pat) =
443 (let val subst: Type.tyenv * Envir.tenv =
444 Pattern.match thy (pat, t)
445 (Vartab.empty, Vartab.empty)
446 in snd (eval__true thy (i+1)
447 (map (Envir.subst_term subst) pres)
450 handle Pattern.MATCH => false;
451 fun scan_ _ [] = false (*scan_ NEVER called by []*)
452 | scan_ f (pp::pps) = if f pp then true
454 tracing "=== poly.sml: scan_ chk prepat begin";
456 tracing "=== poly.sml: scan_ chk prepat end";
459 (*reestablish...*) val t = TermC.str2term "x \<up> 2 * x";
460 val [(pres, pat)] = prepat;
461 val subst: Type.tyenv * Envir.tenv =
462 Pattern.match thy (pat, t)
463 (Vartab.empty, Vartab.empty);
465 (*fixme: asms = ["p is_multUnordered"]...instantiate*)
466 "----- eval__true ---";
467 val asms = (map (Envir.subst_term subst) pres);
468 if UnparseC.terms asms = "[\"x \<up> 2 * x is_multUnordered\"]" then ()
469 else error "rewrite.sml: diff. is_multUnordered, asms";
470 val (thy, i, asms, bdv, rls) =
471 (thy, (i+1), [TermC.str2term "(x \<up> 2 * x) is_multUnordered"],
472 [] : (term * term) list, erls);
473 case eval__true thy i asms bdv rls of
475 | _ => error "rewrite.sml: diff. is_multUnordered, eval__true";
477 "----------- 2011 thms with axclasses ----------------------------------------------------------";
478 "----------- 2011 thms with axclasses ----------------------------------------------------------";
479 "----------- 2011 thms with axclasses ----------------------------------------------------------";
480 val thm = @{thm div_by_1};
481 val prop = Thm.prop_of thm;
482 TermC.atomty prop; (*Type 'a*)
483 val t = TermC.str2term "(2*x)/1"; (*Type real*)
485 val (thy, ro, er, inst) =
486 (@{theory "Isac_Knowledge"}, tless_true, eval_rls, [(@{term "bdv::real"}, @{term "x::real"})]);
487 val SOME (t, _) = rewrite_ thy ro er true thm t; (*real TermC.matches 'a ?via ring? etc*)
489 "----------- fun rewrite_set_ .. RatEq_eliminate step into to fun chk --------------------------";
490 "----------- fun rewrite_set_ .. RatEq_eliminate step into to fun chk --------------------------";
491 "----------- fun rewrite_set_ .. RatEq_eliminate step into to fun chk --------------------------";
492 val thy = @{theory RatEq};
493 val ctxt = Proof_Context.init_global thy;
494 val SOME t = parseNEW ctxt "(3 + -1 * x + x \<up> 2) / (9 * x + -6 * x \<up> 2 + x \<up> 3) = 1 / x";
495 val rls = assoc_rls "RatEq_eliminate"
497 val SOME (t''''', asm''''') =
498 rewrite_set_ thy true rls t;
499 "~~~~~ fun rewrite_set_ , args:"; val (thy, bool, rls, term) = (thy, true, rls, t);
500 rewrite__set_ thy 1 bool [] rls term;
501 "~~~~~ and rewrite__set_ , args:"; val (thy, i, put_asm, bdv, rls, ct)
502 = (thy, 1, bool, []:(term * term) list, rls, term);
504 (*/------- outcomment this code: otherwise the re-definition could infect tests lateron ------\ * )
505 datatype switch = Applicable.Yes | Noap;
506 fun rew_once _ asm ct Noap [] = (ct, asm) (* ?TODO unify with Prog_Expr.rew_once? *)
507 | rew_once ruls asm ct Applicable.Yes [] =
508 (case rls of Rule_Set.Repeat _ => rew_once ruls asm ct Noap ruls
509 | Rule_Set.Sequence _ => (ct, asm)
510 | rls => raise ERROR ("rew_once not appl. to \"" ^ Rule_Set.id rls ^ "\""))
511 | rew_once ruls asm ct apno (rul :: thms) =
513 Rule.Thm (thmid, thm) =>
514 (trace1 i (" try thm: " ^ thmid);
515 case rewrite__ thy (i + 1) bdv ((snd o #rew_ord o Rule.Rule_Set.rep) rls)
516 ((#erls o Rule.Rule_Set.rep) rls) put_asm thm ct of
517 NONE => rew_once ruls asm ct apno thms
518 | SOME (ct', asm') =>
519 (trace1 i (" rewrites to: " ^ UnparseC.term_in_thy thy ct');
520 rew_once ruls (union (op =) asm asm') ct' Applicable.Yes (rul :: thms)))
521 (* once again try the same rule, e.g. associativity against "()"*)
522 | Rule.Eval (cc as (op_, _)) =>
523 let val _= trace1 i (" try calc: " ^ op_ ^ "'")
524 val ct = TermC.uminus_to_string ct (*WN190312: superfluous?*)
525 in case Eval.adhoc_thm thy cc ct of
526 NONE => rew_once ruls asm ct apno thms
529 val pairopt = rewrite__ thy (i + 1) bdv ((snd o #rew_ord o Rule.Rule_Set.rep) rls)
530 ((#erls o Rule.Rule_Set.rep) rls) put_asm thm' ct;
531 val _ = if pairopt <> NONE then () else error ("rewrite_set_, rewrite_ \"" ^
532 ThmC.string_of_thm thm' ^ "\" " ^ UnparseC.term_in_thy thy ct ^ " = NONE")
533 val _ = trace1 i (" calc. to: " ^ UnparseC.term_in_thy thy ((fst o the) pairopt))
534 in rew_once ruls asm ((fst o the) pairopt) Applicable.Yes (rul :: thms) end
536 | Rule.Cal1 (cc as (op_, _)) =>
537 let val _= trace1 i (" try cal1: " ^ op_ ^ "'");
538 val ct = TermC.uminus_to_string ct
539 in case Eval.adhoc_thm1_ thy cc ct of
543 val pairopt = rewrite__ thy (i + 1) bdv ((snd o #rew_ord o Rule.Rule_Set.rep) rls)
544 ((#erls o Rule.Rule_Set.rep) rls) put_asm thm' ct;
545 val _ = if pairopt <> NONE then () else error ("rewrite_set_, rewrite_ \"" ^
546 ThmC.string_of_thm thm' ^ "\" " ^ UnparseC.term_in_thy thy ct ^ " = NONE")
547 val _ = trace1 i (" cal1. to: " ^ UnparseC.term_in_thy thy ((fst o the) pairopt))
551 (case rewrite__set_ thy (i + 1) put_asm bdv rls' ct of
552 SOME (t', asm') => rew_once ruls (union (op =) asm asm') t' Applicable.Yes thms
553 | NONE => rew_once ruls asm ct apno thms)
554 | r => raise ERROR ("rew_once not appl. to \"" ^ Rule.Rule.to_string r ^ "\"");
555 val ruls = (#rules o Rule.Rule_Set.rep) rls;
556 (* val _ = trace i (" rls: " ^ Rule_Set.id rls ^ " on: " ^ UnparseC.term_in_thy thy ct)*)
557 val (ct', asm') = rew_once ruls [] ct Noap ruls;
558 "~~~~~ fun rew_once , args:"; val (ruls, asm, ct, apno, (rul :: thms))
559 = (ruls, []:term list, ct, Noap, ruls);
560 val Rule.Thm (thmid, thm) = (*case*) rul (*of*);
562 val SOME (ct', asm') = (*case*)
563 rewrite__ 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 (*of*);
565 "~~~~~ fun rewrite__ , args:"; val (thy, i, bdv, tless, rls, put_asm, thm, ct)
566 = (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);
569 val (t', asms, _ (*lrd*), rew) =
570 rew_sub 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 "~~~~~ and rew_sub , args:"; val (thy, i, bdv, tless, rls, put_asm, lrd, r, t)
573 = (thy, i, bdv, tless, rls, put_asm, ([(*root of the term*)]: TermC.path),
574 (((TermC.inst_bdv bdv) o Eval.norm o Thm.prop_of) thm), ct);
575 val (lhs, rhs) = (HOLogic.dest_eq o HOLogic.dest_Trueprop o Logic.strip_imp_concl) r
576 val r' = Envir.subst_term (Pattern.match thy (lhs, t) (Vartab.empty, Vartab.empty)) r
578 (*+*)if UnparseC.term r' =
579 (*+*) "\<lbrakk>9 * x + -6 * x \<up> 2 + x \<up> 3 \<noteq> 0; x \<noteq> 0\<rbrakk>\n" ^
580 (*+*) "\<Longrightarrow> ((3 + -1 * x + x \<up> 2) /\n" ^
581 (*+*) " (9 * x + -6 * x \<up> 2 + x \<up> 3) =\n" ^
582 (*+*) " 1 / x) =\n" ^
583 (*+*) " ((3 + -1 * x + x \<up> 2) * x =\n" ^
584 (*+*) " 1 * (9 * x + -6 * x \<up> 2 + x \<up> 3))"
585 (*+*)then () else error "instantiated rule CHANGED";
587 val p' = map HOLogic.dest_Trueprop ((fst o Logic.strip_prems) (Logic.count_prems r', [], r'))
589 (*+*)if map UnparseC.term p' = ["x \<noteq> 0", "9 * x + -6 * x \<up> 2 + x \<up> 3 \<noteq> 0"]
590 (*+*)then () else error "stored assumptions CHANGED";
592 val t' = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop o Logic.strip_imp_concl) r'
594 (*+*)if UnparseC.term t' = "(3 + -1 * x + x \<up> 2) * x = 1 * (9 * x + -6 * x \<up> 2 + x \<up> 3)"
595 (*+*)then () else error "rewritten term (an equality) CHANGED";
597 val (simpl_p', nofalse) =
598 eval__true thy (i + 1) p' bdv rls;
599 "~~~~~ and eval__true , args:"; val (thy, i, asms, bdv, rls) = (thy, (i + 1), p', bdv, rls);
600 (*if*) asms = [@{term True}] orelse asms = [] (*else*);
602 (*+*)if map UnparseC.term asms = ["x \<noteq> 0", "9 * x + -6 * x \<up> 2 + x \<up> 3 \<noteq> 0"]
603 (*+*)then () else error "asms before chk CHANGED";
605 fun chk indets [] = (indets, true) (*return asms<>True until false*)
606 | chk indets (a :: asms) =
607 (case rewrite__set_ thy (i + 1) false bdv rls a of
608 NONE => (chk (indets @ [a]) asms)
610 if t = @{term True} then (chk (indets @ a') asms)
611 else if t = @{term False} then ([], false)
612 (*asm false .. thm not applied \<up> ; continue until False vvv*)
613 else chk (indets @ [t] @ a') asms);
616 chk [] asms; (*return from eval__true*);
617 "~~~~~ fun chk , args:"; val (indets, (a :: asms)) = ([], asms);
619 (*+*)val Rule_Set.Repeat {id = "rateq_erls", rules, ...} = rls;
621 (*+*) [Eval (\<^const_name>\<open>divide\<close>, fn),
622 (*+*) Thm ("minus_divide_left", "- ?a1 / ?b1 = - (?a1 / ?b1)"),
624 (*+*) Eval (\<^const_name>\<open>HOL.eq\<close>, fn),
625 (*+*) Thm ("not_true", "(\<not> True) = False"),
626 (*+*) Thm ("not_false", "(\<not> False) = True"),
628 (*+*) Eval (\<^const_name>\<open>powr\<close>, fn),
629 (*+*) Eval ("RatEq.is_ratequation_in", fn)]:
631 (*+*)chk: term list -> term list -> term list * bool
633 rewrite__set_ thy (i + 1) false bdv rls a (*of*);
635 (*+*)Rewrite.trace_on := false; (*true false*)
637 (*this was False; vvvv--- means: indeterminate*)
638 val (* SOME (t, a') *)NONE = (*case*)
639 rewrite__set_ thy (i + 1) false bdv rls a (*of*);
641 (*+*)UnparseC.term a = "x \<noteq> 0"; (* rewrite__set_ \<rightarrow> @{term True} ----------------- SHOULD BE indet !*)
644 #### rls: rateq_erls on: x \<noteq> 0
646 ##### try calc: HOL.eq' <<<------------------------------- here the error comes from
647 ===== calc. to: ~ False <<<------------------------------- \<not> x = 0 is NOT False
648 ##### try calc: HOL.eq'
649 ##### try thm: not_true
650 ##### try thm: not_false
651 ===== rewrites to: True <<<------------------------------- so x \<noteq> 0 is NOT True
652 and True, False are NOT stored ...
654 ### asms accepted: [x \<noteq> 0] stored: []
656 Rewrite.trace_on := false; (*true false*)
657 ( *\------- outcomment this code: otherwise the re-definition could infect tests lateron ------/*)
660 "----------- fun rewrite_ down to Pattern.match ------------------------------------------------";
661 "----------- fun rewrite_ down to Pattern.match ------------------------------------------------";
662 "----------- fun rewrite_ down to Pattern.match ------------------------------------------------";
663 "~~~~~ fun rewrite_ , args:"; val (thy, rew_ord, erls, bool, thm, term) =
664 (@{theory}, dummy_ord, Rule_Set.empty, false, @{thm distrib_left}, @{term "x * (y + z) :: int"});
665 "~~~~~ fun rewrite__ , args:"; val (thy, i, bdv, tless, rls, put_asm, thm, ct) =
666 (thy, 1, [], rew_ord, erls, bool, thm, term);
667 "~~~~~ and rew_sub , args:"; val (thy, i, bdv, tless, rls, put_asm, lrd, r, t) =
668 (thy, i, bdv, tless, rls, put_asm, [], TermC.inst_bdv bdv (Eval.norm (Thm.prop_of thm)), ct)
669 val (lhss, rhss) = (HOLogic.dest_eq o Logic.strip_imp_concl o HOLogic.dest_Trueprop) r
670 val r' = Envir.subst_term (Pattern.match thy (lhss, t) (Vartab.empty, Vartab.empty)) r
671 val p' = map HOLogic.dest_Trueprop ((fst o Logic.strip_prems) (Logic.count_prems r', [], r'))
672 val t' = (snd o HOLogic.dest_eq o Logic.strip_imp_concl o HOLogic.dest_Trueprop) r'
674 if UnparseC.term lhss = "?a * (?b + ?c)" andalso UnparseC.term t = "x * (y + z)" then ()
675 else error "ARGS FOR Pattern.match CHANGED";
676 val match = Pattern.match thy (lhss, t) (Vartab.empty, Vartab.empty);
677 if (Envir.subst_term match r |> UnparseC.term) = "x * (y + z) = x * y + x * z" then ()
678 else error "Pattern.match CHANGED";
680 "----------- fun rewrite_set_ .. norm_equation, ~~~~~ fun rewrite_set_ -------------------------";
681 "----------- fun rewrite_set_ .. norm_equation, ~~~~~ fun rewrite_set_ -------------------------";
682 "----------- fun rewrite_set_ .. norm_equation, ~~~~~ fun rewrite_set_ -------------------------";
683 (* norm_equation is defined in Test.thy, other rls see Knowledg/**)
685 val rls = norm_equation;
686 val term = TermC.str2term "x + 1 = 2";
688 (**)val SOME (t, asm) = rewrite_set_ thy false rls term;
689 (** )##### try thm: "root_ge0"
690 exception TERM raised (line 271 of "~~/src/HOL/Tools/hologic.ML"):
692 0 \<le> ?a \<Longrightarrow> (0 \<le> sqrt ?a) = True( **)
693 if UnparseC.term t = "x + 1 + - 1 * 2 = 0" then () else error "rewrite_set_ norm_equation CHANGED";
695 "~~~~~ fun rewrite_set_ , args:"; val (thy, bool, rls, term) = (thy, false, rls, term);
696 "~~~~~ and rewrite__set_ , args:"; val (thy, i, put_asm, bdv, rls, ct) =
697 (thy, 1, bool, []: (term * term) list, rls, term);
698 (*deleted after error detection*)