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