1 (* tests for ME/rewrite.sml
2 TODO.WN0509 collect typical tests from systest here !!!!!
3 author: Walther Neuper 050908
4 (c) copyright due to lincense terms.
6 12345678901234567890123456789012345678901234567890123456789012345678901234567890
7 10 20 30 40 50 60 70 80
10 "--------------------------------------------------------";
11 "table of contents --------------------------------------";
12 "--------------------------------------------------------";
13 "----------- assemble rewrite ---------------------------";
14 "----------- test rewriting without Isac's thys ---------";
15 "----------- conditional rewriting without Isac's thys --";
16 "----------- step through 'and rew_sub': ----------------";
17 "----------- step through 'fun rewrite_terms_' ---------";
18 "----------- rewrite_inst_ bdvs -------------------------";
19 "----------- check diff 2002--2009-3 --------------------";
20 "--------------------------------------------------------";
21 "--------------------------------------------------------";
22 "--------------------------------------------------------";
24 "----------- assemble rewrite ---------------------------";
25 "----------- assemble rewrite ---------------------------";
26 "----------- assemble rewrite ---------------------------";
27 "===== rewriting by thm with 'a";
29 val thy = @{theory Complex_Main};
30 val ctxt = @{context};
31 val thm = @{thm add_commute};
32 val t = (term_of o the) (parse thy "((r + u) + t) + s");
33 "----- from old: fun rewrite__";
35 val r = (((inst_bdv bdv) o norm o #prop o rep_thm) thm);
36 "----- from old: and rew_sub";
37 val (lhs,rhs) = (dest_equals' o strip_trueprop
38 o Logic.strip_imp_concl) r;
40 val insts = Pattern.match thy (lhs,t) (Vartab.empty, Vartab.empty);*)
41 "----- fun match_rew in Pure/pattern.ML";
42 val rtm = the_default rhs (Term.rename_abs lhs t rhs);
44 writeln(Syntax.string_of_term ctxt rtm);
45 writeln(Syntax.string_of_term ctxt lhs);
46 writeln(Syntax.string_of_term ctxt t);
48 (Pattern.match thy (lhs, t) (Vartab.empty, Vartab.empty));
49 val (rew, rhs) = (Envir.subst_term
50 (Pattern.match thy (lhs, t) (Vartab.empty, Vartab.empty)) rtm, rtm);
51 (*lookup in isabelle?trace?response...*)
52 writeln(Syntax.string_of_term ctxt rew);
53 writeln(Syntax.string_of_term ctxt rhs);
55 "===== rewriting: prep insertion into rew_sub";
56 val thy = @{theory Complex_Main};
57 val ctxt = @{context};
58 val thm = @{thm nonzero_mult_divide_cancel_right};
59 val r = Thm.prop_of thm;
60 val tm = @{term "x*2 / 2::real"};
62 val (lhs, rhs) = (HOLogic.dest_eq o HOLogic.dest_Trueprop
63 o Logic.strip_imp_concl) r;
64 val r' = Envir.subst_term (Pattern.match thy (lhs, tm)
65 (Vartab.empty, Vartab.empty)) r;
66 val p' = (fst o Logic.strip_prems) (Logic.count_prems r', [], r');
67 val t' = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop
68 o Logic.strip_imp_concl) r';
70 (*is displayed on top of <response> buffer...*)
71 Pretty.writeln (ProofContext.pretty_term_abbrev @{context} r');
72 Pretty.writeln (ProofContext.pretty_term_abbrev @{context} t');
75 "----------- test rewriting without Isac's thys ---------";
76 "----------- test rewriting without Isac's thys ---------";
77 "----------- test rewriting without Isac's thys ---------";
79 "===== rewriting with Isabelle2009-1 only, i.e without isac-hacks";
80 val thy = @{theory Complex_Main};
81 val ctxt = @{context};
82 val thm = @{thm add_commute};
83 val tm = @{term "x + y*z::real"};
85 val SOME (r,_) = (rewrite_ thy dummy_ord e_rls false thm tm)
86 handle _ => error "rewrite.sml diff.behav. in rewriting";
87 (*is displayed on _TOP_ of <response> buffer...*)
88 Pretty.writeln (ProofContext.pretty_term_abbrev @{context} r);
89 if r = @{term "y*z + x::real"}
90 then () else error "rewrite.sml diff.result in rewriting";
92 "----- rewriting a subterm";
93 val tm = @{term "w*(x + y*z)::real"};
95 val SOME (r,_) = (rewrite_ thy dummy_ord e_rls false thm tm)
96 handle _ => error "rewrite.sml diff.behav. in rew_sub";
98 "----- ordered rewriting";
99 fun tord (_:subst) pp = Term_Ord.termless pp;
100 if tord [] (@{term "x + y*z::real"}, @{term "y*z + x::real"}) then ()
101 else error "rewrite.sml diff.behav. in ord.rewr.";
103 val NONE = (rewrite_ thy tord e_rls false thm tm)
104 handle _ => error "rewrite.sml diff.behav. in rewriting";
105 (*is displayed on _TOP_ of <response> buffer...*)
106 Pretty.writeln (ProofContext.pretty_term_abbrev @{context} r);
108 val tm = @{term "x*y + z::real"};
109 val SOME (r,_) = (rewrite_ thy tord e_rls false thm tm)
110 handle _ => error "rewrite.sml diff.behav. in rewriting";
113 "----------- conditional rewriting without Isac's thys --";
114 "----------- conditional rewriting without Isac's thys --";
115 "----------- conditional rewriting without Isac's thys --";
117 "===== prepr cond.rew. with Pattern.match";
118 val thy = @{theory Complex_Main};
119 val ctxt = @{context};
120 val thm = @{thm nonzero_mult_divide_cancel_right};
121 val rule = Thm.prop_of thm;
122 val tm = @{term "x*2 / 2::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)
135 (Logic.count_prems rule', [], rule');
136 val rhs' = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop
137 o Logic.strip_imp_concl) rule';
139 "----- conditional rewriting creating an assumption";
140 "----- conditional rewriting creating an assumption";
141 val tm = @{term "x*y / y::real"};
142 val SOME (rew, asm) = (rewrite_ thy dummy_ord e_rls false thm tm)
143 handle _ => error "rewrite.sml diff.behav. in cond.rew.";
145 if rew = @{term "x::real"} then () (* the rewrite is _NO_ Trueprop *)
146 else error "rewrite.sml diff.result in cond.rew.";
148 if hd asm = @{term "~ y = (0::real)"} (* dropped Trueprop $ ...*)
149 then () else error "rewrite.sml diff.asm in cond.rew.";
150 "----- conditional rewriting immediately: can only be done with ";
151 "------Isabelle numerals, because erls cannot handle them yet.";
154 "----------- step through 'and rew_sub': ----------------";
155 "----------- step through 'and rew_sub': ----------------";
156 "----------- step through 'and rew_sub': ----------------";
157 (*and make asms without Trueprop, beginning with the result:*)
158 val tm = @{term "x*y / y::real"};
159 val (t', asm, _, _) = rew_sub thy 0 [] dummy_ord e_rls true [] (prop_of thm) tm;
161 "----- evaluate arguments";
162 val (thy, i, bdv, tless, rls, put_asm, lrd, r, t) =
163 (thy, 0, [], dummy_ord, e_rls, true, [], (prop_of thm), tm);
164 "----- step 1: lhs, rhs of rule";
165 val (lhs, rhs) = (HOLogic.dest_eq o HOLogic.dest_Trueprop
166 o Logic.strip_imp_concl) r;
167 term2str r = "?b ~= (0::?'a) ==> ?a * ?b / ?b = ?a";
168 term2str lhs = "?a * ?b / ?b"; term2str rhs = "?a";
169 "----- step 2: the rule instantiated";
170 val r' = Envir.subst_term
171 (Pattern.match thy (lhs, t) (Vartab.empty, Vartab.empty)) r;
172 term2str r' = "y ~= 0 ==> x * y / y = x";
173 "----- step 3: get the (instantiated) assumption(s)";
174 val p' = (fst o Logic.strip_prems) (Logic.count_prems r', [], r');
175 term2str (hd p') = "y ~= 0";
176 "=====vvv make asms without Trueprop ---vvv";
177 val p' = map HOLogic.dest_Trueprop ((fst o Logic.strip_prems)
178 (Logic.count_prems r', [], r'));
180 [Const ("Not", _) $ (Const ("op =", _) $ Free ("y", _) $
181 Const ("Groups.zero_class.zero", _))] => ()
182 | _ => error "rewrite.sml assumption changed";
183 "=====^^^ make asms without Trueprop ---^^^";
184 "----- step 4: get the (instantiated) rhs";
185 val t' = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop
186 o Logic.strip_imp_concl) r';
189 "----------- step through 'fun rewrite_terms_' ---------";
190 "----------- step through 'fun rewrite_terms_' ---------";
191 "----------- step through 'fun rewrite_terms_' ---------";
192 "----- step 0: args for rewrite_terms_, local fun";
193 val (thy, ord, erls, equs, t) =
194 (theory "Biegelinie", dummy_ord, Erls, [str2term "x = 0"],
195 str2term "M_b x = -1 * q_0 * x ^^^ 2 / 2 + x * c + c_2");
196 "----- step 1: args for rew_";
197 val ((t', asm'), (rules as r::rs), t) = ((e_term, []), equs, t);
198 "----- step 2: rew_sub";
199 rew_sub thy 1 [] ord erls false [] (Trueprop $ r) t;
200 "----- step 3: step through rew_sub -- inefficient: goes into subterms";
203 val SOME (t', _) = rewrite_terms_ thy dummy_ord Erls equs t;
204 writeln "----------- rewrite_terms_ 1---------------------------";
205 if term2str t' = "M_b 0 = -1 * q_0 * 0 ^^^ 2 / 2 + 0 * c + c_2" then ()
206 else error "rewrite.sml rewrite_terms_ [x = 0]";
208 val equs = [str2term "M_b 0 = 0"];
209 val t = str2term "M_b 0 = -1 * q_0 * 0 ^^^ 2 / 2 + 0 * c + c_2";
210 val SOME (t', _) = rewrite_terms_ thy dummy_ord Erls equs t;
211 writeln "----------- rewrite_terms_ 2---------------------------";
212 if term2str t' = "0 = -1 * q_0 * 0 ^^^ 2 / 2 + 0 * c + c_2" then ()
213 else error "rewrite.sml rewrite_terms_ [M_b 0 = 0]";
215 val equs = [str2term "x = 0", str2term"M_b 0 = 0"];
216 val t = str2term "M_b x = -1 * q_0 * x ^^^ 2 / 2 + x * c + c_2";
217 val SOME (t', _) = rewrite_terms_ thy dummy_ord Erls equs t;
218 writeln "----------- rewrite_terms_ 3---------------------------";
219 if term2str t' = "0 = -1 * q_0 * 0 ^^^ 2 / 2 + 0 * c + c_2" then ()
220 else error "rewrite.sml rewrite_terms_ [x = 0, M_b 0 = 0]";
223 "----------- rewrite_inst_ bdvs -------------------------";
224 "----------- rewrite_inst_ bdvs -------------------------";
225 "----------- rewrite_inst_ bdvs -------------------------";
226 (*see smltest/Scripts/term_G.sml: inst_bdv 2*)
227 val t = str2term"-1 * (q_0 * L ^^^ 2) / 2 + (L * c_3 + c_4) = 0";
228 val bdvs = [(str2term"bdv_1",str2term"c"),
229 (str2term"bdv_2",str2term"c_2"),
230 (str2term"bdv_3",str2term"c_3"),
231 (str2term"bdv_4",str2term"c_4")];
232 (*------------ outcommented WN071210, after inclusion into ROOT.ML
234 rewrite_inst_ thy e_rew_ord
235 (append_rls "erls_isolate_bdvs" e_rls
236 [(Calc ("EqSystem.occur'_exactly'_in",
237 eval_occur_exactly_in
238 "#eval_occur_exactly_in_"))
240 false bdvs (num_str @{separate_bdvs_add) t;
241 (writeln o term2str) t;
242 if term2str t = "L * c_3 + c_4 = 0 + -1 * (-1 * (q_0 * L ^^^ 2) / 2)"
243 then () else error "rewrite.sml rewrite_inst_ bdvs";
245 trace_rewrite:=false;--------------------------------------------*)
248 "----------- check diff 2002--2009-3 --------------------";
249 "----------- check diff 2002--2009-3 --------------------";
250 "----------- check diff 2002--2009-3 --------------------";
251 (*----- 2002 -------------------------------------------------------------------
252 # rls: norm_Rational_noadd_fractions on: 1 / EI * (L * q_0 * x / 2 + -1 *
254 ## rls: discard_minus_ on: 1 / EI * (L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2
256 ### try thm: real_diff_minus
257 ### try thm: sym_real_mult_minus1
258 ## rls: rat_mult_poly on: 1 / EI * (L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2
260 ### try thm: rat_mult_poly_l
261 ### try thm: rat_mult_poly_r
262 #### eval asms: L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2 is_polyexp
263 ==> 1 / EI * (L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2) =
264 1 * (L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2) / EI
265 ##### rls: e_rls-is_polyexp on: L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2
267 ###### try calc: Poly.is'_polyexp'
268 ====== calc. to: False
269 ###### try calc: Poly.is'_polyexp'
270 ###### try calc: Poly.is'_polyexp'
271 #### asms false: ["L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2 is_polyexp"]
272 ----- 2002 NONE rewrite --------------------------------------------------------
273 ----- 2009 should maintain this behaviour, but: --------------------------------
274 # rls: norm_Rational_noadd_fractions on: 1 / EI * (L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2)
275 ## rls: discard_minus on: 1 / EI * (L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2)
276 ### try thm: real_diff_minus
277 ### try thm: sym_real_mult_minus1
278 ## rls: rat_mult_poly on: 1 / EI * (L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2)
279 ### try thm: rat_mult_poly_l
280 ### try thm: rat_mult_poly_r
281 #### eval asms: L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2 is_polyexp
282 ==> 1 / EI * (L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2) =
283 1 * (L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2) / EI
284 ##### rls: e_rls-is_polyexp on: L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2 is_polyexp
285 ###### try calc: Poly.is'_polyexp'
286 ====== calc. to: False
287 ###### try calc: Poly.is'_polyexp'
288 ###### try calc: Poly.is'_polyexp'
289 #### asms accepted: ["L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2 is_polyexp"] stored: ["False"]
290 === rewrites to: 1 * (L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2) / EI
291 ----- 2009 -------------------------------------------------------------------*)
293 (*the situation as was before repair (asm without Trueprop) is outcommented*)
294 val thy = theory "Isac";
295 "===== example which raised the problem =================";
296 val t = @{term "1 / EI * (L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2)"};
297 "----- rewrite_set_inst_ norm_Rational_noadd_fractions--";
298 val subs = [(str2term "bdv", str2term "x")];
299 val rls = norm_Rational_noadd_fractions;
300 val NONE (*SOME (t', _)*) = rewrite_set_inst_ thy true subs rls t;
301 "----- rewrite_ rat_mult_poly_r--------------------------";
302 val thm = @{thm rat_mult_poly_r};
303 "?c::real is_polyexp ==> (?a::real) / (?b::real) * ?c = ?a * ?c / ?b";
304 val erls = append_rls "e_rls-is_polyexp" e_rls
305 [Calc ("Poly.is'_polyexp", eval_is_polyexp "")];
306 val NONE (*SOME (t'', _)*) = rewrite_ thy dummy_ord erls true thm t;
307 (*t' = t''; (*false because of further rewrites in t'*)*)
308 "----- rew_sub --------------------------------";
309 val (t''', _, _, _) = rew_sub thy 0 [] dummy_ord erls true [] (prop_of thm) t;
310 (*t'' = t'''; (*true*)*)
311 "----- rewrite_set_ erls --------------------------------";
312 val cond = @{term "(L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2)"};
313 val NONE = rewrite_set_ thy true erls cond;
314 (* ^^^^^ goes with '====== calc. to: False' above from beginning*)
316 writeln "===== maximally simplified example =====================";
317 val t = @{term "a / b * (x / x ^^^ 2)"};
318 "?c::real is_polyexp ==> (?a::real) / (?b::real) * ?c = ?a * ?c / ?b";
319 writeln "----- rewrite_set_inst_ norm_Rational_noadd_fractions--";
320 val (*NONE*) SOME (t', asm) = rewrite_set_inst_ thy true subs rls t;
321 term2str t' = "a * x / (b * x ^^^ 2)"; (*rew. by thm outside test case*)
322 (*checked visually: trace_rewrite looks like above for 2009*)
324 trace_rewrite := false; (*<<<<<<<<<<<<<<<<<<<<<###############################*)
326 writeln "----- rewrite_ rat_mult_poly_r--------------------------";
327 val NONE (*SOME (t'', _)*) = rewrite_ thy dummy_ord erls true thm t;
328 (*t' = t''; (*false because of further rewrites in t'*)*)
329 writeln "----- rew_sub --------------------------------";
330 val (t''', _, _, _) = rew_sub thy 0 [] dummy_ord erls true [] (prop_of thm) t;
331 (*t'' = t'''; (*true*)*)
332 writeln "----- rewrite_set_ erls --------------------------------";
333 val cond = @{term "(x / x ^^^ 2)"};
334 val NONE = rewrite_set_ thy true erls cond;
335 (* ^^^^^ goes with '====== calc. to: False' above from beginning*)
336 trace_rewrite := false; (*<<<<<<<<<<<<<<<<<<<<<###############################*)
337 "--------------------------------------------------------";
340 (*===== inhibit exn ============================================================
341 ===== inhibit exn ============================================================*)
343 (*-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.
344 -.-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.*)