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 use"../smltest/Scripts/rewrite.sml";
10 "-----------------------------------------------------------------";
11 "table of contents -----------------------------------------------";
12 "-----------------------------------------------------------------";
13 "----------- assemble rewrite ------------------------------------";
14 "----------- test rewriting without Isac's thys ------------------";
15 "----------- conditional rewriting without Isac's thys -----------";
16 "----------- rewrite_terms_ -------------------------------------";
17 "----------- rewrite_inst_ bdvs ----------------------------------";
18 "-----------------------------------------------------------------";
19 "-----------------------------------------------------------------";
20 "-----------------------------------------------------------------";
22 "----------- assemble rewrite ------------------------------------";
23 "----------- assemble rewrite ------------------------------------";
24 "----------- assemble rewrite ------------------------------------";
26 "===== rewriting by thm with 'a";
28 val thy = @{theory Complex_Main};
29 val ctxt = @{context};
30 val thm = @{thm add_commute};
31 val t = (term_of o the) (parse thy "((r + u) + t) + s");
32 "----- from old: fun rewrite__";
34 val r = (((inst_bdv bdv) o norm o #prop o rep_thm) thm);
35 "----- from old: and rew_sub";
36 val (lhs,rhs) = (dest_equals' o strip_trueprop
37 o Logic.strip_imp_concl) r;
39 val insts = Pattern.match thy (lhs,t) (Vartab.empty, Vartab.empty);*)
40 "----- fun match_rew in Pure/pattern.ML";
41 val rtm = the_default rhs (Term.rename_abs lhs t rhs);
43 tracing(Syntax.string_of_term ctxt rtm);
44 tracing(Syntax.string_of_term ctxt lhs);
45 tracing(Syntax.string_of_term ctxt t);
47 (Pattern.match thy (lhs, t) (Vartab.empty, Vartab.empty));
48 val (rew, rhs) = (Envir.subst_term
49 (Pattern.match thy (lhs, t) (Vartab.empty, Vartab.empty)) rtm, rtm);
50 (*lookup in isabelle?trace?response...*)
51 writeln(Syntax.string_of_term ctxt rew);
52 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 with Isabelle2009-1 only";
87 (*is displayed on _TOP_ of <response> buffer...*)
88 Pretty.writeln (ProofContext.pretty_term_abbrev @{context} r);
90 "----- rewriting a subterm";
91 val tm = @{term "w*(x + y*z)::real"};
93 val SOME (r,_) = (rewrite_ thy dummy_ord e_rls false thm tm)
94 handle _ => error "rewrite.sml diff.behav. in rew_sub with Isabelle2009-1 only";
96 "----- ordered rewriting";
97 fun tord (_:subst) pp = TermOrd.termless pp;
98 if tord [] (@{term "x + y*z::real"}, @{term "y*z + x::real"}) then ()
99 else error "rewrite.sml diff.behav. in ord.rewr. with Isabelle2009-1 only";
101 val NONE = (rewrite_ thy tord e_rls false thm tm)
102 handle _ => error "rewrite.sml diff.behav. in rewriting with Isabelle2009-1 only";
103 (*is displayed on _TOP_ of <response> buffer...*)
104 Pretty.writeln (ProofContext.pretty_term_abbrev @{context} r);
106 val tm = @{term "x*y + z::real"};
107 val SOME (r,_) = (rewrite_ thy tord e_rls false thm tm)
108 handle _ => error "rewrite.sml diff.behav. in rewriting with Isabelle2009-1 only";
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. with Isabelle2009-1 only a";
145 if rew = @{term "x::real"} then ()
146 else error "rewrite.sml diff.behav. in cond.rew. with Isabelle2009-1 only b";
148 if HOLogic.dest_Trueprop (hd asm) = @{term "~ y = (0::real)"} then ()
149 else error "rewrite.sml diff.behav. in cond.rew. with Isabelle2009-1 only c";
151 "----- conditional rewriting immediately: can only be done with Isabelle numerals\
152 \because erls cannot handle them yet.";
156 "----------- rewrite_terms_ -------------------------------------";
157 "----------- rewrite_terms_ -------------------------------------";
158 "----------- rewrite_terms_ -------------------------------------";
159 val subte = [str2term"x = 0"];
160 val t = str2term"M_b x = -1 * q_0 * x ^^^ 2 / 2 + x * c + c_2";
161 val Some (t',_) = rewrite_terms_ thy dummy_ord Erls subte t;
162 if term2str t' = "M_b 0 = -1 * q_0 * 0 ^^^ 2 / 2 + 0 * c + c_2" then ()
163 else raise error "rewrite.sml rewrite_terms_ [x = 0]";
165 val subte = [str2term"M_b 0 = 0"];
166 val t = str2term"M_b 0 = -1 * q_0 * 0 ^^^ 2 / 2 + 0 * c + c_2";
167 val Some (t',_) = rewrite_terms_ thy dummy_ord Erls subte t;
168 if term2str t' = "0 = -1 * q_0 * 0 ^^^ 2 / 2 + 0 * c + c_2" then ()
169 else raise error "rewrite.sml rewrite_terms_ [M_b 0 = 0]";
171 val subte = [str2term"x = 0", str2term"M_b 0 = 0"];
172 val t = str2term"M_b x = -1 * q_0 * x ^^^ 2 / 2 + x * c + c_2";
173 val Some (t',_) = rewrite_terms_ thy dummy_ord Erls subte t;
174 if term2str t' = "0 = -1 * q_0 * 0 ^^^ 2 / 2 + 0 * c + c_2" then ()
175 else raise error "rewrite.sml rewrite_terms_ [x = 0, M_b 0 = 0]";
178 "----------- rewrite_inst_ bdvs ----------------------------------";
179 "----------- rewrite_inst_ bdvs ----------------------------------";
180 "----------- rewrite_inst_ bdvs ----------------------------------";
181 (*see smltest/Scripts/term_G.sml: inst_bdv 2*)
182 val t = str2term"-1 * (q_0 * L ^^^ 2) / 2 + (L * c_3 + c_4) = 0";
183 val bdvs = [(str2term"bdv_1",str2term"c"),
184 (str2term"bdv_2",str2term"c_2"),
185 (str2term"bdv_3",str2term"c_3"),
186 (str2term"bdv_4",str2term"c_4")];
187 (*------------ outcommented WN071210, after inclusion into ROOT.ML
189 rewrite_inst_ thy e_rew_ord
190 (append_rls "erls_isolate_bdvs" e_rls
191 [(Calc ("EqSystem.occur'_exactly'_in",
192 eval_occur_exactly_in
193 "#eval_occur_exactly_in_"))
195 false bdvs (num_str separate_bdvs_add) t;
196 (writeln o term2str) t;
197 if term2str t = "L * c_3 + c_4 = 0 + -1 * (-1 * (q_0 * L ^^^ 2) / 2)"
198 then () else raise error "rewrite.sml rewrite_inst_ bdvs";
200 trace_rewrite:=false;--------------------------------------------*)