12 "--------------------------------------------------------"; |
12 "--------------------------------------------------------"; |
13 "----------- assemble rewrite ---------------------------"; |
13 "----------- assemble rewrite ---------------------------"; |
14 "----------- test rewriting without Isac's thys ---------"; |
14 "----------- test rewriting without Isac's thys ---------"; |
15 "----------- conditional rewriting without Isac's thys --"; |
15 "----------- conditional rewriting without Isac's thys --"; |
16 "----------- step through 'and rew_sub': ----------------"; |
16 "----------- step through 'and rew_sub': ----------------"; |
17 "----------- rewrite_terms_ ----------------------------"; |
17 "----------- step through 'fun rewrite_terms_' ---------"; |
18 "----------- rewrite_inst_ bdvs -------------------------"; |
18 "----------- rewrite_inst_ bdvs -------------------------"; |
19 "----------- check diff 2002--2009-3 --------------------"; |
19 "----------- check diff 2002--2009-3 --------------------"; |
20 "--------------------------------------------------------"; |
20 "--------------------------------------------------------"; |
21 "--------------------------------------------------------"; |
21 "--------------------------------------------------------"; |
22 "--------------------------------------------------------"; |
22 "--------------------------------------------------------"; |
153 |
153 |
154 "----------- step through 'and rew_sub': ----------------"; |
154 "----------- step through 'and rew_sub': ----------------"; |
155 "----------- step through 'and rew_sub': ----------------"; |
155 "----------- step through 'and rew_sub': ----------------"; |
156 "----------- step through 'and rew_sub': ----------------"; |
156 "----------- step through 'and rew_sub': ----------------"; |
157 (*and make asms without Trueprop, beginning with the result:*) |
157 (*and make asms without Trueprop, beginning with the result:*) |
|
158 val tm = @{term "x*y / y::real"}; |
158 val (t', asm, _, _) = rew_sub thy 0 [] dummy_ord e_rls true [] (prop_of thm) tm; |
159 val (t', asm, _, _) = rew_sub thy 0 [] dummy_ord e_rls true [] (prop_of thm) tm; |
159 show_types := false; |
160 show_types := false; |
160 "----- evaluate arguments"; |
161 "----- evaluate arguments"; |
161 val (thy, i, bdv, tless, rls, put_asm, lrd, r, t) = |
162 val (thy, i, bdv, tless, rls, put_asm, lrd, r, t) = |
162 (thy, 0, [], dummy_ord, e_rls, true, [], (prop_of thm), tm); |
163 (thy, 0, [], dummy_ord, e_rls, true, [], (prop_of thm), tm); |
163 "----- step 1: lhs, rhs of rule"; |
164 "----- step 1: lhs, rhs of rule"; |
164 val (lhs, rhs) = (HOLogic.dest_eq o HOLogic.dest_Trueprop |
165 val (lhs, rhs) = (HOLogic.dest_eq o HOLogic.dest_Trueprop |
165 o Logic.strip_imp_concl) r; |
166 o Logic.strip_imp_concl) r; |
166 term2str r = "?b ~= (0::?'a) ==> ?a * ?b / ?b = ?a"; |
167 term2str r = "?b ~= (0::?'a) ==> ?a * ?b / ?b = ?a"; |
167 term2str lhs = "?a * ?b / ?b"; term2str rhs = "?a"; |
168 term2str lhs = "?a * ?b / ?b"; term2str rhs = "?a"; |
168 "----- step 2: the rule instantiated"; |
169 "----- step 2: the rule instantiated"; |
169 val r' = Envir.subst_term (Pattern.match thy (lhs, t) |
170 val r' = Envir.subst_term |
170 (Vartab.empty, Vartab.empty)) r; |
171 (Pattern.match thy (lhs, t) (Vartab.empty, Vartab.empty)) r; |
171 term2str r' = "y ~= 0 ==> x * y / y = x"; |
172 term2str r' = "y ~= 0 ==> x * y / y = x"; |
172 "----- step 3: get the (instantiated) assumption(s)"; |
173 "----- step 3: get the (instantiated) assumption(s)"; |
173 val p' = (fst o Logic.strip_prems) (Logic.count_prems r', [], r'); |
174 val p' = (fst o Logic.strip_prems) (Logic.count_prems r', [], r'); |
174 term2str (hd p') = "y ~= 0"; |
175 term2str (hd p') = "y ~= 0"; |
175 "=====vvv make asms without Trueprop ---vvv"; |
176 "=====vvv make asms without Trueprop ---vvv"; |
183 "----- step 4: get the (instantiated) rhs"; |
184 "----- step 4: get the (instantiated) rhs"; |
184 val t' = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop |
185 val t' = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop |
185 o Logic.strip_imp_concl) r'; |
186 o Logic.strip_imp_concl) r'; |
186 term2str t' = "x"; |
187 term2str t' = "x"; |
187 |
188 |
188 (*===== inhibit exn ============================================================ |
189 "----------- step through 'fun rewrite_terms_' ---------"; |
189 "----------- rewrite_terms_ ----------------------------"; |
190 "----------- step through 'fun rewrite_terms_' ---------"; |
190 "----------- rewrite_terms_ ----------------------------"; |
191 "----------- step through 'fun rewrite_terms_' ---------"; |
191 "----------- rewrite_terms_ ----------------------------"; |
192 "----- step 0: args for rewrite_terms_, local fun"; |
192 val subte = [str2term "x = 0"]; |
193 val (thy, ord, erls, equs, t) = |
193 val t = str2term "M_b x = -1 * q_0 * x ^^^ 2 / 2 + x * c + c_2"; |
194 (theory "Biegelinie", dummy_ord, Erls, [str2term "x = 0"], |
194 val SOME (t',_) = rewrite_terms_ thy dummy_ord Erls subte t; (*NONE..TODO*) |
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"; |
|
201 |
|
202 |
|
203 val SOME (t', _) = rewrite_terms_ thy dummy_ord Erls equs t; |
|
204 writeln "----------- rewrite_terms_ 1---------------------------"; |
195 if term2str t' = "M_b 0 = -1 * q_0 * 0 ^^^ 2 / 2 + 0 * c + c_2" then () |
205 if term2str t' = "M_b 0 = -1 * q_0 * 0 ^^^ 2 / 2 + 0 * c + c_2" then () |
196 else raise error "rewrite.sml rewrite_terms_ [x = 0]"; |
206 else raise error "rewrite.sml rewrite_terms_ [x = 0]"; |
197 |
207 |
198 val subte = [str2term "M_b 0 = 0"]; |
208 val equs = [str2term "M_b 0 = 0"]; |
199 val t = str2term"M_b 0 = -1 * q_0 * 0 ^^^ 2 / 2 + 0 * c + c_2"; |
209 val t = str2term "M_b 0 = -1 * q_0 * 0 ^^^ 2 / 2 + 0 * c + c_2"; |
200 val SOME (t',_) = rewrite_terms_ thy dummy_ord Erls subte t; |
210 val SOME (t', _) = rewrite_terms_ thy dummy_ord Erls equs t; |
|
211 writeln "----------- rewrite_terms_ 2---------------------------"; |
201 if term2str t' = "0 = -1 * q_0 * 0 ^^^ 2 / 2 + 0 * c + c_2" then () |
212 if term2str t' = "0 = -1 * q_0 * 0 ^^^ 2 / 2 + 0 * c + c_2" then () |
202 else raise error "rewrite.sml rewrite_terms_ [M_b 0 = 0]"; |
213 else raise error "rewrite.sml rewrite_terms_ [M_b 0 = 0]"; |
203 |
214 |
204 val subte = [str2term"x = 0", str2term"M_b 0 = 0"]; |
215 val equs = [str2term "x = 0", str2term"M_b 0 = 0"]; |
205 val t = str2term"M_b x = -1 * q_0 * x ^^^ 2 / 2 + x * c + c_2"; |
216 val t = str2term "M_b x = -1 * q_0 * x ^^^ 2 / 2 + x * c + c_2"; |
206 val SOME (t',_) = rewrite_terms_ thy dummy_ord Erls subte t; |
217 val SOME (t', _) = rewrite_terms_ thy dummy_ord Erls equs t; |
|
218 writeln "----------- rewrite_terms_ 3---------------------------"; |
207 if term2str t' = "0 = -1 * q_0 * 0 ^^^ 2 / 2 + 0 * c + c_2" then () |
219 if term2str t' = "0 = -1 * q_0 * 0 ^^^ 2 / 2 + 0 * c + c_2" then () |
208 else raise error "rewrite.sml rewrite_terms_ [x = 0, M_b 0 = 0]"; |
220 else raise error "rewrite.sml rewrite_terms_ [x = 0, M_b 0 = 0]"; |
209 ===== inhibit exn ============================================================*) |
|
210 |
221 |
211 |
222 |
212 "----------- rewrite_inst_ bdvs -------------------------"; |
223 "----------- rewrite_inst_ bdvs -------------------------"; |
213 "----------- rewrite_inst_ bdvs -------------------------"; |
224 "----------- rewrite_inst_ bdvs -------------------------"; |
214 "----------- rewrite_inst_ bdvs -------------------------"; |
225 "----------- rewrite_inst_ bdvs -------------------------"; |
231 if term2str t = "L * c_3 + c_4 = 0 + -1 * (-1 * (q_0 * L ^^^ 2) / 2)" |
242 if term2str t = "L * c_3 + c_4 = 0 + -1 * (-1 * (q_0 * L ^^^ 2) / 2)" |
232 then () else raise error "rewrite.sml rewrite_inst_ bdvs"; |
243 then () else raise error "rewrite.sml rewrite_inst_ bdvs"; |
233 trace_rewrite:=true; |
244 trace_rewrite:=true; |
234 trace_rewrite:=false;--------------------------------------------*) |
245 trace_rewrite:=false;--------------------------------------------*) |
235 |
246 |
|
247 |
236 "----------- check diff 2002--2009-3 --------------------"; |
248 "----------- check diff 2002--2009-3 --------------------"; |
237 "----------- check diff 2002--2009-3 --------------------"; |
249 "----------- check diff 2002--2009-3 --------------------"; |
238 "----------- check diff 2002--2009-3 --------------------"; |
250 "----------- check diff 2002--2009-3 --------------------"; |
239 (*----- 2002 ------------------------------------------------------------------- |
251 (*----- 2002 ------------------------------------------------------------------- |
240 # rls: norm_Rational_noadd_fractions on: 1 / EI * (L * q_0 * x / 2 + -1 * |
252 # rls: norm_Rational_noadd_fractions on: 1 / EI * (L * q_0 * x / 2 + -1 * |
321 val cond = @{term "(x / x ^^^ 2)"}; |
333 val cond = @{term "(x / x ^^^ 2)"}; |
322 val NONE = rewrite_set_ thy true erls cond; |
334 val NONE = rewrite_set_ thy true erls cond; |
323 (* ^^^^^ goes with '====== calc. to: False' above from beginning*) |
335 (* ^^^^^ goes with '====== calc. to: False' above from beginning*) |
324 trace_rewrite := false; (*<<<<<<<<<<<<<<<<<<<<<###############################*) |
336 trace_rewrite := false; (*<<<<<<<<<<<<<<<<<<<<<###############################*) |
325 "--------------------------------------------------------"; |
337 "--------------------------------------------------------"; |
|
338 |
|
339 |
|
340 (*===== inhibit exn ============================================================ |
|
341 ===== inhibit exn ============================================================*) |
|
342 |
|
343 (*-.-.-.-.-.-isolate response.-.-.-.-.-.-. |
|
344 -.-.-.-.-.-.-isolate response.-.-.-.-.-.*) |