1 (* chapter 'Biegelinie' from the textbook:
2 Timischl, Kaiser. Ingenieur-Mathematik 3. Wien 1999. p.268-271.
5 (c) due to copyright terms
8 theory Biegelinie imports Integrate Equation EqSystem begin
12 q_ :: real => real ("q'_") (* Streckenlast *)
13 Q :: real => real (* Querkraft *)
14 Q' :: real => real (* Ableitung der Querkraft *)
15 M'_b :: real => real ("M'_b") (* Biegemoment *)
16 M'_b' :: real => real ("M'_b'") (* Ableitung des Biegemoments *)
17 y'' :: real => real (* 2.Ableitung der Biegeline *)
18 y' :: real => real (* Neigung der Biegeline *)
19 (*y :: real => real (* Biegeline *)*)
20 EI :: real (* Biegesteifigkeit *)
22 (*new Descriptions in the related problems*)
23 Traegerlaenge :: real => una
24 Streckenlast :: real => una
25 BiegemomentVerlauf :: bool => una
26 Biegelinie :: (real => real) => una
27 Randbedingungen :: bool list => una
28 RandbedingungenBiegung :: bool list => una
29 RandbedingungenNeigung :: bool list => una
30 RandbedingungenMoment :: bool list => una
31 RandbedingungenQuerkraft :: bool list => una
32 FunktionsVariable :: real => una
33 Funktionen :: bool list => una
34 Gleichungen :: bool list => una
37 Biegelinie2Script :: "[real,real,real,real=>real,bool list,
39 ("((Script Biegelinie2Script (_ _ _ _ _ =))// (_))" 9)
40 BiegelinieScript :: "[real,real,real,real=>real,bool list,bool list,
42 ("((Script BiegelinieScript (_ _ _ _ _ _ =))// (_))" 9)
43 Biege2xIntegrierenScript :: "[real,real,real,bool,real=>real,bool list,
45 ("((Script Biege2xIntegrierenScript (_ _ _ _ _ _ =))// (_))" 9)
46 Biege4x4SystemScript :: "[real,real,real,real=>real,bool list,
48 ("((Script Biege4x4SystemScript (_ _ _ _ _ =))// (_))" 9)
49 Biege1xIntegrierenScript ::
50 "[real,real,real,real=>real,bool list,bool list,bool list,
52 ("((Script Biege1xIntegrierenScript (_ _ _ _ _ _ _ =))// (_))" 9)
53 Belastung2BiegelScript :: "[real,real,
54 bool list] => bool list"
55 ("((Script Belastung2BiegelScript (_ _ =))// (_))" 9)
56 SetzeRandbedScript :: "[bool list,bool list,
57 bool list] => bool list"
58 ("((Script SetzeRandbedScript (_ _ =))// (_))" 9)
62 Querkraft_Belastung "Q' x = -q_ x"
63 Belastung_Querkraft "-q_ x = Q' x"
65 Moment_Querkraft "M_b' x = Q x"
66 Querkraft_Moment "Q x = M_b' x"
68 Neigung_Moment "y'' x = -M_b x/ EI"
69 Moment_Neigung "M_b x = -EI * y'' x"
71 (*according to rls 'simplify_Integral': .. = 1/a * .. instead .. = ../ a*)
72 make_fun_explicit "Not (a =!= 0) ==> (a * (f x) = b) = (f x = 1/a * b)"
75 (** theory elements for transfer into html **)
77 store_isa ["IsacKnowledge"] [];
78 store_thy (theory "Biegelinie")
79 ["Walther Neuper 2005 supported by a grant from NMI Austria"];
80 store_isa ["IsacKnowledge", theory2thyID (theory "Biegelinie"), "Theorems"]
81 ["Walther Neuper 2005 supported by a grant from NMI Austria"];
82 store_thm (theory "Biegelinie") ("Belastung_Querkraft", Belastung_Querkraft)
83 ["Walther Neuper 2005 supported by a grant from NMI Austria"];
84 store_thm (theory "Biegelinie") ("Moment_Neigung", Moment_Neigung)
85 ["Walther Neuper 2005 supported by a grant from NMI Austria"];
86 store_thm (theory "Biegelinie") ("Moment_Querkraft", Moment_Querkraft)
87 ["Walther Neuper 2005 supported by a grant from NMI Austria"];
88 store_thm (theory "Biegelinie") ("Neigung_Moment", Neigung_Moment)
89 ["Walther Neuper 2005 supported by a grant from NMI Austria"];
90 store_thm (theory "Biegelinie") ("Querkraft_Belastung", Querkraft_Belastung)
91 ["Walther Neuper 2005 supported by a grant from NMI Austria"];
92 store_thm (theory "Biegelinie") ("Querkraft_Moment", Querkraft_Moment)
93 ["Walther Neuper 2005 supported by a grant from NMI Austria"];
94 store_thm (theory "Biegelinie") ("make_fun_explicit", make_fun_explicit)
95 ["Walther Neuper 2005 supported by a grant from NMI Austria"];
101 (prep_pbt (theory "Biegelinie") "pbl_bieg" [] e_pblID
103 [("#Given" ,["Traegerlaenge l_", "Streckenlast q__"]),
104 (*("#Where",["0 < l_"]), ...wait for < and handling Arbfix*)
105 ("#Find" ,["Biegelinie b_"]),
106 ("#Relate",["Randbedingungen rb_"])
108 append_rls "e_rls" e_rls [],
110 [["IntegrierenUndKonstanteBestimmen2"]]));
113 (prep_pbt (theory "Biegelinie") "pbl_bieg_mom" [] e_pblID
114 (["MomentBestimmte","Biegelinien"],
115 [("#Given" ,["Traegerlaenge l_", "Streckenlast q__"]),
116 (*("#Where",["0 < l_"]), ...wait for < and handling Arbfix*)
117 ("#Find" ,["Biegelinie b_"]),
118 ("#Relate",["RandbedingungenBiegung rb_","RandbedingungenMoment rm_"])
120 append_rls "e_rls" e_rls [],
122 [["IntegrierenUndKonstanteBestimmen"]]));
125 (prep_pbt (theory "Biegelinie") "pbl_bieg_momg" [] e_pblID
126 (["MomentGegebene","Biegelinien"],
128 append_rls "e_rls" e_rls [],
130 [["IntegrierenUndKonstanteBestimmen","2xIntegrieren"]]));
133 (prep_pbt (theory "Biegelinie") "pbl_bieg_einf" [] e_pblID
134 (["einfache","Biegelinien"],
136 append_rls "e_rls" e_rls [],
138 [["IntegrierenUndKonstanteBestimmen","4x4System"]]));
141 (prep_pbt (theory "Biegelinie") "pbl_bieg_momquer" [] e_pblID
142 (["QuerkraftUndMomentBestimmte","Biegelinien"],
144 append_rls "e_rls" e_rls [],
146 [["IntegrierenUndKonstanteBestimmen","1xIntegrieren"]]));
149 (prep_pbt (theory "Biegelinie") "pbl_bieg_vonq" [] e_pblID
150 (["vonBelastungZu","Biegelinien"],
151 [("#Given" ,["Streckenlast q__","FunktionsVariable v_"]),
152 ("#Find" ,["Funktionen funs___"])],
153 append_rls "e_rls" e_rls [],
155 [["Biegelinien","ausBelastung"]]));
158 (prep_pbt (theory "Biegelinie") "pbl_bieg_randbed" [] e_pblID
159 (["setzeRandbedingungen","Biegelinien"],
160 [("#Given" ,["Funktionen funs_","Randbedingungen rb_"]),
161 ("#Find" ,["Gleichungen equs___"])],
162 append_rls "e_rls" e_rls [],
164 [["Biegelinien","setzeRandbedingungenEin"]]));
167 (prep_pbt (theory "Biegelinie") "pbl_equ_fromfun" [] e_pblID
168 (["makeFunctionTo","equation"],
169 [("#Given" ,["functionEq fun_","substitution sub_"]),
170 ("#Find" ,["equality equ___"])],
171 append_rls "e_rls" e_rls [],
173 [["Equation","fromFunction"]]));
178 val srls = Rls {id="srls_IntegrierenUnd..",
180 rew_ord = ("termlessI",termlessI),
181 erls = append_rls "erls_in_srls_IntegrierenUnd.." e_rls
182 [(*for asm in nth_Cons_ ...*)
183 Calc ("op <",eval_equ "#less_"),
184 (*2nd nth_Cons_ pushes n+-1 into asms*)
185 Calc("op +", eval_binop "#add_")
187 srls = Erls, calc = [],
188 rules = [Thm ("nth_Cons_",num_str nth_Cons_),
189 Calc("op +", eval_binop "#add_"),
190 Thm ("nth_Nil_",num_str nth_Nil_),
191 Calc("Tools.lhs", eval_lhs"eval_lhs_"),
192 Calc("Tools.rhs", eval_rhs"eval_rhs_"),
193 Calc("Atools.argument'_in",
194 eval_argument_in "Atools.argument'_in")
199 Rls {id="srls_IntegrierenUnd..",
201 rew_ord = ("termlessI",termlessI),
202 erls = append_rls "erls_in_srls_IntegrierenUnd.." e_rls
203 [(*for asm in nth_Cons_ ...*)
204 Calc ("op <",eval_equ "#less_"),
205 (*2nd nth_Cons_ pushes n+-1 into asms*)
206 Calc("op +", eval_binop "#add_")
208 srls = Erls, calc = [],
209 rules = [Thm ("nth_Cons_",num_str nth_Cons_),
210 Calc("op +", eval_binop "#add_"),
211 Thm ("nth_Nil_", num_str nth_Nil_),
212 Calc("Tools.lhs", eval_lhs "eval_lhs_"),
213 Calc("Atools.filter'_sameFunId",
214 eval_filter_sameFunId "Atools.filter'_sameFunId"),
215 (*WN070514 just for smltest/../biegelinie.sml ...*)
216 Calc("Atools.sameFunId", eval_sameFunId "Atools.sameFunId"),
217 Thm ("filter_Cons", num_str filter_Cons),
218 Thm ("filter_Nil", num_str filter_Nil),
219 Thm ("if_True", num_str if_True),
220 Thm ("if_False", num_str if_False),
221 Thm ("hd_thm", num_str hd_thm)
226 (prep_met (theory "Biegelinie") "met_biege" [] e_metID
227 (["IntegrierenUndKonstanteBestimmen"],
228 [("#Given" ,["Traegerlaenge l_", "Streckenlast q__",
229 "FunktionsVariable v_"]),
230 (*("#Where",["0 < l_"]), ...wait for < and handling Arbfix*)
231 ("#Find" ,["Biegelinie b_"]),
232 ("#Relate",["RandbedingungenBiegung rb_",
233 "RandbedingungenMoment rm_"])
235 {rew_ord'="tless_true",
236 rls' = append_rls "erls_IntegrierenUndK.." e_rls
237 [Calc ("Atools.ident",eval_ident "#ident_"),
238 Thm ("not_true",num_str not_true),
239 Thm ("not_false",num_str not_false)],
240 calc = [], srls = srls, prls = Erls,
241 crls = Atools_erls, nrls = Erls},
242 "Script BiegelinieScript " ^
243 "(l_::real) (q__::real) (v_::real) (b_::real=>real) " ^
244 "(rb_::bool list) (rm_::bool list) = " ^
245 " (let q___ = Take (q_ v_ = q__); " ^
246 " q___ = ((Rewrite sym_real_minus_eq_cancel True) @@ " ^
247 " (Rewrite Belastung_Querkraft True)) q___; " ^
249 " (SubProblem (Biegelinie_,[named,integrate,function], " ^
250 " [diff,integration,named]) " ^
251 " [real_ (rhs q___), real_ v_, real_real_ Q]); " ^
252 " Q__ = Rewrite Querkraft_Moment True Q__; " ^
254 " (SubProblem (Biegelinie_,[named,integrate,function], " ^
255 " [diff,integration,named]) " ^
256 " [real_ (rhs Q__), real_ v_, real_real_ M_b]); " ^
257 " e1__ = nth_ 1 rm_; " ^
258 " (x1__::real) = argument_in (lhs e1__); " ^
259 " (M1__::bool) = (Substitute [v_ = x1__]) M__; " ^
260 " M1__ = (Substitute [e1__]) M1__ ; " ^
261 " M2__ = Take M__; " ^
262 (*without this Take 'Substitute [v_ = x2__]' takes _last formula from ctree_*)
263 " e2__ = nth_ 2 rm_; " ^
264 " (x2__::real) = argument_in (lhs e2__); " ^
265 " (M2__::bool) = ((Substitute [v_ = x2__]) @@ " ^
266 " (Substitute [e2__])) M2__; " ^
267 " (c_1_2__::bool list) = " ^
268 " (SubProblem (Biegelinie_,[linear,system],[no_met]) " ^
269 " [booll_ [M1__, M2__], reall [c,c_2]]); " ^
270 " M__ = Take M__; " ^
271 " M__ = ((Substitute c_1_2__) @@ " ^
272 " (Try (Rewrite_Set_Inst [(bdv_1, c),(bdv_2, c_2)]" ^
273 " simplify_System False)) @@ " ^
274 " (Rewrite Moment_Neigung False) @@ " ^
275 " (Rewrite make_fun_explicit False)) M__; " ^
276 (*----------------------- and the same once more ------------------------*)
278 " (SubProblem (Biegelinie_,[named,integrate,function], " ^
279 " [diff,integration,named]) " ^
280 " [real_ (rhs M__), real_ v_, real_real_ y']); " ^
282 " (SubProblem (Biegelinie_,[named,integrate,function], " ^
283 " [diff,integration,named]) " ^
284 " [real_ (rhs N__), real_ v_, real_real_ y]); " ^
285 " e1__ = nth_ 1 rb_; " ^
286 " (x1__::real) = argument_in (lhs e1__); " ^
287 " (B1__::bool) = (Substitute [v_ = x1__]) B__; " ^
288 " B1__ = (Substitute [e1__]) B1__ ; " ^
289 " B2__ = Take B__; " ^
290 " e2__ = nth_ 2 rb_; " ^
291 " (x2__::real) = argument_in (lhs e2__); " ^
292 " (B2__::bool) = ((Substitute [v_ = x2__]) @@ " ^
293 " (Substitute [e2__])) B2__; " ^
294 " (c_1_2__::bool list) = " ^
295 " (SubProblem (Biegelinie_,[linear,system],[no_met]) " ^
296 " [booll_ [B1__, B2__], reall [c,c_2]]); " ^
297 " B__ = Take B__; " ^
298 " B__ = ((Substitute c_1_2__) @@ " ^
299 " (Rewrite_Set_Inst [(bdv, x)] make_ratpoly_in False)) B__ " ^
304 (prep_met (theory "Biegelinie") "met_biege_2" [] e_metID
305 (["IntegrierenUndKonstanteBestimmen2"],
306 [("#Given" ,["Traegerlaenge l_", "Streckenlast q__",
307 "FunktionsVariable v_"]),
308 (*("#Where",["0 < l_"]), ...wait for < and handling Arbfix*)
309 ("#Find" ,["Biegelinie b_"]),
310 ("#Relate",["Randbedingungen rb_"])
312 {rew_ord'="tless_true",
313 rls' = append_rls "erls_IntegrierenUndK.." e_rls
314 [Calc ("Atools.ident",eval_ident "#ident_"),
315 Thm ("not_true",num_str not_true),
316 Thm ("not_false",num_str not_false)],
318 srls = append_rls "erls_IntegrierenUndK.." e_rls
319 [Calc("Tools.rhs", eval_rhs"eval_rhs_"),
320 Calc ("Atools.ident",eval_ident "#ident_"),
321 Thm ("last_thmI",num_str last_thmI),
322 Thm ("if_True",num_str if_True),
323 Thm ("if_False",num_str if_False)
325 prls = Erls, crls = Atools_erls, nrls = Erls},
326 "Script Biegelinie2Script " ^
327 "(l_::real) (q__::real) (v_::real) (b_::real=>real) (rb_::bool list) = " ^
329 " (funs_:: bool list) = " ^
330 " (SubProblem (Biegelinie_,[vonBelastungZu,Biegelinien], " ^
331 " [Biegelinien,ausBelastung]) " ^
332 " [real_ q__, real_ v_]); " ^
333 " (equs_::bool list) = " ^
334 " (SubProblem (Biegelinie_,[setzeRandbedingungen,Biegelinien]," ^
335 " [Biegelinien,setzeRandbedingungenEin]) " ^
336 " [booll_ funs_, booll_ rb_]); " ^
337 " (cons_::bool list) = " ^
338 " (SubProblem (Biegelinie_,[linear,system],[no_met]) " ^
339 " [booll_ equs_, reall [c,c_2,c_3,c_4]]); " ^
340 " B_ = Take (lastI funs_); " ^
341 " B_ = ((Substitute cons_) @@ " ^
342 " (Rewrite_Set_Inst [(bdv, v_)] make_ratpoly_in False)) B_ " ^
347 (prep_met (theory "Biegelinie") "met_biege_intconst_2" [] e_metID
348 (["IntegrierenUndKonstanteBestimmen","2xIntegrieren"],
350 {rew_ord'="tless_true", rls'=Erls, calc = [],
353 crls = Atools_erls, nrls = e_rls},
358 (prep_met (theory "Biegelinie") "met_biege_intconst_4" [] e_metID
359 (["IntegrierenUndKonstanteBestimmen","4x4System"],
361 {rew_ord'="tless_true", rls'=Erls, calc = [],
364 crls = Atools_erls, nrls = e_rls},
369 (prep_met (theory "Biegelinie") "met_biege_intconst_1" [] e_metID
370 (["IntegrierenUndKonstanteBestimmen","1xIntegrieren"],
372 {rew_ord'="tless_true", rls'=Erls, calc = [],
375 crls = Atools_erls, nrls = e_rls},
380 (prep_met (theory "Biegelinie") "met_biege2" [] e_metID
383 {rew_ord'="tless_true", rls'=Erls, calc = [],
386 crls = Atools_erls, nrls = e_rls},
391 (prep_met (theory "Biegelinie") "met_biege_ausbelast" [] e_metID
392 (["Biegelinien","ausBelastung"],
393 [("#Given" ,["Streckenlast q__","FunktionsVariable v_"]),
394 ("#Find" ,["Funktionen funs_"])],
395 {rew_ord'="tless_true",
396 rls' = append_rls "erls_ausBelastung" e_rls
397 [Calc ("Atools.ident",eval_ident "#ident_"),
398 Thm ("not_true",num_str not_true),
399 Thm ("not_false",num_str not_false)],
401 srls = append_rls "srls_ausBelastung" e_rls
402 [Calc("Tools.rhs", eval_rhs"eval_rhs_")],
403 prls = e_rls, crls = Atools_erls, nrls = e_rls},
404 "Script Belastung2BiegelScript (q__::real) (v_::real) = " ^
405 " (let q___ = Take (q_ v_ = q__); " ^
406 " q___ = ((Rewrite sym_real_minus_eq_cancel True) @@ " ^
407 " (Rewrite Belastung_Querkraft True)) q___; " ^
409 " (SubProblem (Biegelinie_,[named,integrate,function], " ^
410 " [diff,integration,named]) " ^
411 " [real_ (rhs q___), real_ v_, real_real_ Q]); " ^
412 " M__ = Rewrite Querkraft_Moment True Q__; " ^
414 " (SubProblem (Biegelinie_,[named,integrate,function], " ^
415 " [diff,integration,named]) " ^
416 " [real_ (rhs M__), real_ v_, real_real_ M_b]); " ^
417 " N__ = ((Rewrite Moment_Neigung False) @@ " ^
418 " (Rewrite make_fun_explicit False)) M__; " ^
420 " (SubProblem (Biegelinie_,[named,integrate,function], " ^
421 " [diff,integration,named]) " ^
422 " [real_ (rhs N__), real_ v_, real_real_ y']); " ^
424 " (SubProblem (Biegelinie_,[named,integrate,function], " ^
425 " [diff,integration,named]) " ^
426 " [real_ (rhs N__), real_ v_, real_real_ y]) " ^
427 " in [Q__, M__, N__, B__])"
431 (prep_met (theory "Biegelinie") "met_biege_setzrand" [] e_metID
432 (["Biegelinien","setzeRandbedingungenEin"],
433 [("#Given" ,["Funktionen funs_","Randbedingungen rb_"]),
434 ("#Find" ,["Gleichungen equs___"])],
435 {rew_ord'="tless_true", rls'=Erls, calc = [],
438 crls = Atools_erls, nrls = e_rls},
439 "Script SetzeRandbedScript (funs_::bool list) (rb_::bool list) = " ^
440 " (let b1_ = nth_ 1 rb_; " ^
441 " fs_ = filter_sameFunId (lhs b1_) funs_; " ^
443 " (SubProblem (Biegelinie_,[makeFunctionTo,equation]," ^
444 " [Equation,fromFunction]) " ^
445 " [bool_ (hd fs_), bool_ b1_]); " ^
446 " b2_ = nth_ 2 rb_; " ^
447 " fs_ = filter_sameFunId (lhs b2_) funs_; " ^
449 " (SubProblem (Biegelinie_,[makeFunctionTo,equation]," ^
450 " [Equation,fromFunction]) " ^
451 " [bool_ (hd fs_), bool_ b2_]); " ^
452 " b3_ = nth_ 3 rb_; " ^
453 " fs_ = filter_sameFunId (lhs b3_) funs_; " ^
455 " (SubProblem (Biegelinie_,[makeFunctionTo,equation]," ^
456 " [Equation,fromFunction]) " ^
457 " [bool_ (hd fs_), bool_ b3_]); " ^
458 " b4_ = nth_ 4 rb_; " ^
459 " fs_ = filter_sameFunId (lhs b4_) funs_; " ^
461 " (SubProblem (Biegelinie_,[makeFunctionTo,equation]," ^
462 " [Equation,fromFunction]) " ^
463 " [bool_ (hd fs_), bool_ b4_]) " ^
464 " in [e1_,e2_,e3_,e4_])"
465 (* filter requires more than 1 sec !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!
466 "Script SetzeRandbedScript (funs_::bool list) (rb_::bool list) = " ^
467 " (let b1_ = nth_ 1 rb_; " ^
468 " fs_ = filter (sameFunId (lhs b1_)) funs_; " ^
470 " (SubProblem (Biegelinie_,[makeFunctionTo,equation]," ^
471 " [Equation,fromFunction]) " ^
472 " [bool_ (hd fs_), bool_ b1_]); " ^
473 " b2_ = nth_ 2 rb_; " ^
474 " fs_ = filter (sameFunId (lhs b2_)) funs_; " ^
476 " (SubProblem (Biegelinie_,[makeFunctionTo,equation]," ^
477 " [Equation,fromFunction]) " ^
478 " [bool_ (hd fs_), bool_ b2_]); " ^
479 " b3_ = nth_ 3 rb_; " ^
480 " fs_ = filter (sameFunId (lhs b3_)) funs_; " ^
482 " (SubProblem (Biegelinie_,[makeFunctionTo,equation]," ^
483 " [Equation,fromFunction]) " ^
484 " [bool_ (hd fs_), bool_ b3_]); " ^
485 " b4_ = nth_ 4 rb_; " ^
486 " fs_ = filter (sameFunId (lhs b4_)) funs_; " ^
488 " (SubProblem (Biegelinie_,[makeFunctionTo,equation]," ^
489 " [Equation,fromFunction]) " ^
490 " [bool_ (hd fs_), bool_ b4_]) " ^
491 " in [e1_,e2_,e3_,e4_])"*)
495 (prep_met (theory "Biegelinie") "met_equ_fromfun" [] e_metID
496 (["Equation","fromFunction"],
497 [("#Given" ,["functionEq fun_","substitution sub_"]),
498 ("#Find" ,["equality equ___"])],
499 {rew_ord'="tless_true", rls'=Erls, calc = [],
500 srls = append_rls "srls_in_EquationfromFunc" e_rls
501 [Calc("Tools.lhs", eval_lhs"eval_lhs_"),
502 Calc("Atools.argument'_in",
504 "Atools.argument'_in")],
506 crls = Atools_erls, nrls = e_rls},
507 (*(M_b x = c_2 + c * x + -1 * q_0 / 2 * x ^^^ 2) (M_b L = 0) -->
508 0 = c_2 + c * L + -1 * q_0 / 2 * L ^^^ 2*)
509 "Script Function2Equality (fun_::bool) (sub_::bool) =" ^
510 " (let fun_ = Take fun_; " ^
511 " bdv_ = argument_in (lhs fun_); " ^
512 " val_ = argument_in (lhs sub_); " ^
513 " equ_ = (Substitute [bdv_ = val_]) fun_; " ^
514 " equ_ = (Substitute [sub_]) fun_ " ^
515 " in (Rewrite_Set norm_Rational False) equ_) "