243 "........... 2nd integral ........................................"; |
243 "........... 2nd integral ........................................"; |
244 val t = str2term |
244 val t = str2term |
245 "Integral 1 / EI * (L * q_0 / 2 * (x ^^^ 2 / 2) + -1 * q_0 / 2 * (x ^^^ 3 / 3)) D x"; |
245 "Integral 1 / EI * (L * q_0 / 2 * (x ^^^ 2 / 2) + -1 * q_0 / 2 * (x ^^^ 3 / 3)) D x"; |
246 val rls = simplify_Integral; |
246 val rls = simplify_Integral; |
247 val SOME (t,[]) = rewrite_set_inst_ thy true subs rls t; |
247 val SOME (t,[]) = rewrite_set_inst_ thy true subs rls t; |
248 if term2str t = |
248 if term2str t = |
249 "Integral 1 / EI * (L * q_0 / 4 * x ^^^ 2 + -1 * q_0 / 6 * x ^^^ 3) D x" |
249 "Integral 1 / EI *\n (L * q_0 / 4 * x ^^^ 2 +\n -1 * q_0 / 6 * x ^^^ 3) D x" |
|
250 (*"Integral 1 / EI * (L * q_0 / 4 * x ^^^ 2 + -1 * q_0 / 6 * x ^^^ 3) D x"*) |
250 then () else raise error "integrate.sml, simplify_Integral #198"; |
251 then () else raise error "integrate.sml, simplify_Integral #198"; |
251 |
252 |
252 val rls = integration_rules; |
253 val rls = integration_rules; |
253 val SOME (t,[]) = rewrite_set_ thy true rls t; |
254 val SOME (t,[]) = rewrite_set_ thy true rls t; |
|
255 term2str t; |
254 if term2str t = |
256 if term2str t = |
255 "1 / EI * (L * q_0 / 4 * (x ^^^ 3 / 3) + -1 * q_0 / 6 * (x ^^^ 4 / 4))" |
257 "1 / EI *\n(L * q_0 / 4 * (x ^^^ 3 / 3) +\n -1 * q_0 / 6 * (x ^^^ 4 / 4))" |
|
258 (*"1 / EI * (L * q_0 / 4 * (x ^^^ 3 / 3) + -1 * q_0 / 6 * (x ^^^ 4 / 4))"*) |
256 then () else error "integrate.sml, simplify_Integral #199"; |
259 then () else error "integrate.sml, simplify_Integral #199"; |
257 |
260 |
258 |
261 |
259 "----------- integrate by ruleset -----------------------"; |
262 "----------- integrate by ruleset -----------------------"; |
260 "----------- integrate by ruleset -----------------------"; |
263 "----------- integrate by ruleset -----------------------"; |
296 else error "integrate.sml: diff.behav. in integration #2"; |
299 else error "integrate.sml: diff.behav. in integration #2"; |
297 |
300 |
298 val str = rewrit_sinst subs rls |
301 val str = rewrit_sinst subs rls |
299 "Integral 1 / EI * (L * q_0 / 2 * x + -1 * q_0 / 2 * x ^^^ 2) D x"; |
302 "Integral 1 / EI * (L * q_0 / 2 * x + -1 * q_0 / 2 * x ^^^ 2) D x"; |
300 if str = |
303 if str = |
301 "c + 1 / EI * (L * q_0 / 4 * x ^^^ 2 + -1 * q_0 / 6 * x ^^^ 3)" |
304 "c +\n1 / EI * (L * q_0 / 4 * x ^^^ 2 + -1 * q_0 / 6 * x ^^^ 3)" |
|
305 (*"c + 1 / EI * (L * q_0 / 4 * x ^^^ 2 + -1 * q_0 / 6 * x ^^^ 3)"*) |
302 then () else error "integrate.sml: diff.behav. in integration #3"; |
306 then () else error "integrate.sml: diff.behav. in integration #3"; |
303 |
307 |
304 val str = "Integral "^str^" D x"; |
308 val str = "Integral "^str^" D x"; |
305 val str = rewrit_sinst subs rls str; |
309 val str = rewrit_sinst subs rls str; |
306 if str = |
310 if str = |
307 "c_2 + c * x + 1 / EI * (L * q_0 / 12 * x ^^^ 3 + -1 * q_0 / 24 * x ^^^ 4)" |
311 "c_2 + c * x +\n1 / EI *\n(L * q_0 / 12 * x ^^^ 3 + -1 * q_0 / 24 * x ^^^ 4)" |
|
312 (*"c_2 + c * x + 1 / EI * (L * q_0 / 12 * x ^^^ 3 + -1 * q_0 / 24 * x ^^^ 4)"*) |
308 then () else error "integrate.sml: diff.behav. in integration #4"; |
313 then () else error "integrate.sml: diff.behav. in integration #4"; |
309 |
314 |
310 |
315 |
311 |
316 |
312 "----------- rewrite 3rd integration in 7.27 ------------"; |
317 "----------- rewrite 3rd integration in 7.27 ------------"; |
315 val thy = @{theory "Isac"} (*because of Undeclared constant "Biegelinie.EI*); |
320 val thy = @{theory "Isac"} (*because of Undeclared constant "Biegelinie.EI*); |
316 val bdv = [(str2term"bdv", str2term"x")]; |
321 val bdv = [(str2term"bdv", str2term"x")]; |
317 val t = str2term |
322 val t = str2term |
318 "Integral 1 / EI * ((L * q_0 * x + -1 * q_0 * x ^^^ 2) / 2) D x"; |
323 "Integral 1 / EI * ((L * q_0 * x + -1 * q_0 * x ^^^ 2) / 2) D x"; |
319 val SOME(t,_)= rewrite_set_inst_ thy true bdv simplify_Integral t; |
324 val SOME(t,_)= rewrite_set_inst_ thy true bdv simplify_Integral t; |
|
325 term2str t; |
320 if term2str t = |
326 if term2str t = |
321 "Integral 1 / EI * (L * q_0 / 2 * x + -1 * q_0 / 2 * x ^^^ 2) D x" then () |
327 "Integral 1 / EI *\n (L * q_0 / 2 * x + -1 * q_0 / 2 * x ^^^ 2) D x" |
322 else error "integrate.sml 3rd integration in 7.27, simplify_Integral"; |
328 (*"Integral 1 / EI * (L * q_0 / 2 * x + -1 * q_0 / 2 * x ^^^ 2) D x" *) |
|
329 then () else error "integrate.sml 3rd integration in 7.27, simplify_Integral"; |
323 |
330 |
324 val SOME(t,_)= rewrite_set_inst_ thy true bdv integration t; |
331 val SOME(t,_)= rewrite_set_inst_ thy true bdv integration t; |
325 if term2str t = "c + 1 / EI * (L * q_0 / 4 * x ^^^ 2 + -1 * q_0 / 6 * x ^^^ 3)" |
332 term2str t; |
|
333 if term2str t = |
|
334 "c +\n1 / EI * (L * q_0 / 4 * x ^^^ 2 + -1 * q_0 / 6 * x ^^^ 3)" |
|
335 (*"c + 1 / EI * (L * q_0 / 4 * x ^^^ 2 + -1 * q_0 / 6 * x ^^^ 3)"*) |
326 then () else error "integrate.sml 3rd integration in 7.27, integration"; |
336 then () else error "integrate.sml 3rd integration in 7.27, integration"; |
327 |
337 |
328 |
338 |
329 "----------- check probem type --------------------------"; |
339 "----------- check probem type --------------------------"; |
330 "----------- check probem type --------------------------"; |
340 "----------- check probem type --------------------------"; |