ad 967c8a1eb6b1 (2): add functions accessing Theory_Data in parallel to those accessing 'mets = Unsynchronized.ref'
1 (* chapter 'Biegelinie' from the textbook:
2 Timischl, Kaiser. Ingenieur-Mathematik 3. Wien 1999. p.268-271.
3 author: Walther Neuper 050826,
4 (c) due to copyright terms
7 theory Biegelinie imports Integrate Equation EqSystem Atools begin
11 qq :: "real => real" (* Streckenlast *)
12 Q :: "real => real" (* Querkraft *)
13 Q' :: "real => real" (* Ableitung der Querkraft *)
14 M'_b :: "real => real" ("M'_b") (* Biegemoment *)
15 M'_b' :: "real => real" ("M'_b'") (* Ableitung des Biegemoments *)
16 y'' :: "real => real" (* 2.Ableitung der Biegeline *)
17 y' :: "real => real" (* Neigung der Biegeline *)
18 (*y :: "real => real" (* Biegeline *)*)
19 EI :: "real" (* Biegesteifigkeit *)
21 (*new Descriptions in the related problems*)
22 Traegerlaenge :: "real => una"
23 Streckenlast :: "real => una"
24 BiegemomentVerlauf :: "bool => una"
25 Biegelinie :: "(real => real) => una"
26 Randbedingungen :: "bool list => una"
27 RandbedingungenBiegung :: "bool list => una"
28 RandbedingungenNeigung :: "bool list => una"
29 RandbedingungenMoment :: "bool list => una"
30 RandbedingungenQuerkraft :: "bool list => una"
31 FunktionsVariable :: "real => una"
32 Funktionen :: "bool list => una"
33 Gleichungen :: "bool list => una"
36 Biegelinie2Script :: "[real,real,real,real=>real,bool list,
38 ("((Script Biegelinie2Script (_ _ _ _ _ =))// (_))" 9)
39 BiegelinieScript :: "[real,real,real,real=>real,bool list,bool list,
41 ("((Script BiegelinieScript (_ _ _ _ _ _ =))// (_))" 9)
42 Biege2xIntegrierenScript :: "[real,real,real,bool,real=>real,bool list,
44 ("((Script Biege2xIntegrierenScript (_ _ _ _ _ _ =))// (_))" 9)
45 Biege4x4SystemScript :: "[real,real,real,real=>real,bool list,
47 ("((Script Biege4x4SystemScript (_ _ _ _ _ =))// (_))" 9)
48 Biege1xIntegrierenScript ::
49 "[real,real,real,real=>real,bool list,bool list,bool list,
51 ("((Script Biege1xIntegrierenScript (_ _ _ _ _ _ _ =))// (_))" 9)
52 Belastung2BiegelScript :: "[real,real,
53 bool list] => bool list"
54 ("((Script Belastung2BiegelScript (_ _ =))// (_))" 9)
55 SetzeRandbedScript :: "[bool list,bool list,
56 bool list] => bool list"
57 ("((Script SetzeRandbedScript (_ _ =))// (_))" 9)
61 Querkraft_Belastung: "Q' x = -qq x" and
62 Belastung_Querkraft: "-qq x = Q' x" and
64 Moment_Querkraft: "M_b' x = Q x" and
65 Querkraft_Moment: "Q x = M_b' x" and
67 Neigung_Moment: "y'' x = -M_b x/ EI" and
68 Moment_Neigung: "M_b x = -EI * y'' x" and
70 (*according to rls 'simplify_Integral': .. = 1/a * .. instead .. = ../ a*)
71 make_fun_explicit: "Not (a =!= 0) ==> (a * (f x) = b) = (f x = 1/a * b)"
76 (** theory elements for transfer into html **)
78 store_isa ["IsacKnowledge"] [];
80 ["Walther Neuper 2005 supported by a grant from NMI Austria"];
81 store_isa ["IsacKnowledge", theory2thyID thy, "Theorems"]
82 ["Walther Neuper 2005 supported by a grant from NMI Austria"];
83 store_thm thy "IsacKnowledge" ("Belastung_Querkraft", prop_of @{thm Belastung_Querkraft})
84 ["Walther Neuper 2005 supported by a grant from NMI Austria"];
85 store_thm thy "IsacKnowledge" ("Moment_Neigung", prop_of @{thm Moment_Neigung})
86 ["Walther Neuper 2005 supported by a grant from NMI Austria"];
87 store_thm thy "IsacKnowledge" ("Moment_Querkraft", prop_of @{thm Moment_Querkraft})
88 ["Walther Neuper 2005 supported by a grant from NMI Austria"];
89 store_thm thy "IsacKnowledge" ("Neigung_Moment", prop_of @{thm Neigung_Moment})
90 ["Walther Neuper 2005 supported by a grant from NMI Austria"];
91 store_thm thy "IsacKnowledge" ("Querkraft_Belastung", prop_of @{thm Querkraft_Belastung})
92 ["Walther Neuper 2005 supported by a grant from NMI Austria"];
93 store_thm thy "IsacKnowledge" ("Querkraft_Moment", prop_of @{thm Querkraft_Moment})
94 ["Walther Neuper 2005 supported by a grant from NMI Austria"];
95 store_thm thy "IsacKnowledge" ("make_fun_explicit", prop_of @{thm make_fun_explicit})
96 ["Walther Neuper 2005 supported by a grant from NMI Austria"];
100 setup {* KEStore_Elems.add_pbts
101 [(prep_pbt thy "pbl_bieg" [] e_pblID
103 [("#Given" ,["Traegerlaenge l_l", "Streckenlast q_q"]),
104 (*("#Where",["0 < l_l"]), ...wait for < and handling Arbfix*)
105 ("#Find" ,["Biegelinie b_b"]),
106 ("#Relate",["Randbedingungen r_b"])],
107 append_rls "e_rls" e_rls [], NONE, [["IntegrierenUndKonstanteBestimmen2"]])),
108 (prep_pbt thy "pbl_bieg_mom" [] e_pblID
109 (["MomentBestimmte","Biegelinien"],
110 [("#Given" ,["Traegerlaenge l_l", "Streckenlast q_q"]),
111 (*("#Where",["0 < l_l"]), ...wait for < and handling Arbfix*)
112 ("#Find" ,["Biegelinie b_b"]),
113 ("#Relate",["RandbedingungenBiegung r_b","RandbedingungenMoment r_m"])
115 append_rls "e_rls" e_rls [], NONE, [["IntegrierenUndKonstanteBestimmen"]])),
116 (prep_pbt thy "pbl_bieg_momg" [] e_pblID
117 (["MomentGegebene","Biegelinien"], [], append_rls "e_rls" e_rls [], NONE,
118 [["IntegrierenUndKonstanteBestimmen","2xIntegrieren"]])),
119 (prep_pbt thy "pbl_bieg_einf" [] e_pblID
120 (["einfache","Biegelinien"], [], append_rls "e_rls" e_rls [], NONE,
121 [["IntegrierenUndKonstanteBestimmen","4x4System"]])),
122 (prep_pbt thy "pbl_bieg_momquer" [] e_pblID
123 (["QuerkraftUndMomentBestimmte","Biegelinien"], [], append_rls "e_rls" e_rls [], NONE,
124 [["IntegrierenUndKonstanteBestimmen","1xIntegrieren"]])),
125 (prep_pbt thy "pbl_bieg_vonq" [] e_pblID
126 (["vonBelastungZu","Biegelinien"],
127 [("#Given" ,["Streckenlast q_q","FunktionsVariable v_v"]),
128 ("#Find" ,["Funktionen funs'''"])],
129 append_rls "e_rls" e_rls [], NONE, [["Biegelinien","ausBelastung"]])),
130 (prep_pbt thy "pbl_bieg_randbed" [] e_pblID
131 (["setzeRandbedingungen","Biegelinien"],
132 [("#Given" ,["Funktionen fun_s","Randbedingungen r_b"]),
133 ("#Find" ,["Gleichungen equs'''"])],
134 append_rls "e_rls" e_rls [], NONE, [["Biegelinien","setzeRandbedingungenEin"]])),
135 (prep_pbt thy "pbl_equ_fromfun" [] e_pblID
136 (["makeFunctionTo","equation"],
137 [("#Given" ,["functionEq fu_n","substitution su_b"]),
138 ("#Find" ,["equality equ'''"])],
139 append_rls "e_rls" e_rls [], NONE, [["Equation","fromFunction"]]))] *}
143 val srls = Rls {id="srls_IntegrierenUnd..",
145 rew_ord = ("termlessI",termlessI),
146 erls = append_rls "erls_in_srls_IntegrierenUnd.." e_rls
147 [(*for asm in NTH_CONS ...*)
148 Calc ("Orderings.ord_class.less",eval_equ "#less_"),
149 (*2nd NTH_CONS pushes n+-1 into asms*)
150 Calc("Groups.plus_class.plus", eval_binop "#add_")
152 srls = Erls, calc = [], errpatts = [],
153 rules = [Thm ("NTH_CONS",num_str @{thm NTH_CONS}),
154 Calc("Groups.plus_class.plus", eval_binop "#add_"),
155 Thm ("NTH_NIL",num_str @{thm NTH_NIL}),
156 Calc("Tools.lhs", eval_lhs"eval_lhs_"),
157 Calc("Tools.rhs", eval_rhs"eval_rhs_"),
158 Calc("Atools.argument'_in",
159 eval_argument_in "Atools.argument'_in")
164 Rls {id="srls_IntegrierenUnd..",
166 rew_ord = ("termlessI",termlessI),
167 erls = append_rls "erls_in_srls_IntegrierenUnd.." e_rls
168 [(*for asm in NTH_CONS ...*)
169 Calc ("Orderings.ord_class.less",eval_equ "#less_"),
170 (*2nd NTH_CONS pushes n+-1 into asms*)
171 Calc("Groups.plus_class.plus", eval_binop "#add_")
173 srls = Erls, calc = [], errpatts = [],
174 rules = [Thm ("NTH_CONS",num_str @{thm NTH_CONS}),
175 Calc("Groups.plus_class.plus", eval_binop "#add_"),
176 Thm ("NTH_NIL", num_str @{thm NTH_NIL}),
177 Calc("Tools.lhs", eval_lhs "eval_lhs_"),
178 Calc("Atools.filter'_sameFunId",
179 eval_filter_sameFunId "Atools.filter'_sameFunId"),
180 (*WN070514 just for smltest/../biegelinie.sml ...*)
181 Calc("Atools.sameFunId", eval_sameFunId "Atools.sameFunId"),
182 Thm ("filter_Cons", num_str @{thm filter_Cons}),
183 Thm ("filter_Nil", num_str @{thm filter_Nil}),
184 Thm ("if_True", num_str @{thm if_True}),
185 Thm ("if_False", num_str @{thm if_False}),
186 Thm ("hd_thm", num_str @{thm hd_thm})
193 (prep_met thy "met_biege" [] e_metID
194 (["IntegrierenUndKonstanteBestimmen"],
195 [("#Given" ,["Traegerlaenge l_l", "Streckenlast q__q", "FunktionsVariable v_v"]),
196 (*("#Where",["0 < l_l"]), ...wait for < and handling Arbfix*)
197 ("#Find" ,["Biegelinie b_b"]),
198 ("#Relate",["RandbedingungenBiegung r_b", "RandbedingungenMoment r_m"])],
199 {rew_ord'="tless_true",
200 rls' = append_rls "erls_IntegrierenUndK.." e_rls
201 [Calc ("Atools.ident",eval_ident "#ident_"),
202 Thm ("not_true",num_str @{thm not_true}),
203 Thm ("not_false",num_str @{thm not_false})],
204 calc = [], srls = srls, prls = Erls, crls = Atools_erls, errpats = [], nrls = Erls},
205 "Script BiegelinieScript " ^
206 "(l_l::real) (q__q::real) (v_v::real) (b_b::real=>real) " ^
207 "(r_b::bool list) (r_m::bool list) = " ^
208 " (let q___q = Take (qq v_v = q__q); " ^
209 " q___q = ((Rewrite sym_neg_equal_iff_equal True) @@ " ^
210 " (Rewrite Belastung_Querkraft True)) q___q; " ^
211 " (Q__Q:: bool) = " ^
212 " (SubProblem (Biegelinie',[named,integrate,function], " ^
213 " [diff,integration,named]) " ^
214 " [REAL (rhs q___q), REAL v_v, REAL_REAL Q]); " ^
215 " Q__Q = Rewrite Querkraft_Moment True Q__Q; " ^
217 " (SubProblem (Biegelinie',[named,integrate,function], " ^
218 " [diff,integration,named]) " ^
219 " [REAL (rhs Q__Q), REAL v_v, REAL_REAL M_b]); " ^
220 (*([5], Res), M_b x = c_2 + c * x + -1 * q_0 / 2 * x ^^^ 2*)
221 " e__1 = NTH 1 r_m; " ^
222 " (x__1::real) = argument_in (lhs e__1); " ^
223 " (M__1::bool) = (Substitute [v_v = x__1]) M__M; " ^
224 (*([6], Res), M_b 0 = c_2 + c * 0 + -1 * q_0 / 2 * 0 ^^^ 2*)
225 " M__1 = (Substitute [e__1]) M__1; " ^
226 (*([7], Res), 0 = c_2 + c * 0 + -1 * q_0 / 2 * 0 ^^^ 2*)
227 " M__2 = Take M__M; " ^
228 (*([8], Frm), M_b x = c_2 + c * x + -1 * q_0 / 2 * x ^^^ 2*)
229 (*without above Take 'Substitute [v_v = x__2]' takes _last formula from ctree_*)
230 " e__2 = NTH 2 r_m; " ^
231 " (x__2::real) = argument_in (lhs e__2); " ^
232 " (M__2::bool) = (Substitute [v_v = x__2]) M__M; " ^
233 (*([8], Res), M_b L = c_2 + c * L + -1 * q_0 / 2 * L ^^^ 2*)
234 " M__2 = (Substitute [e__2]) M__2; " ^
236 " (c_1_2::bool list) = " ^
237 " (SubProblem (Biegelinie',[LINEAR,system],[no_met]) " ^
238 " [BOOL_LIST [M__1, M__2], REAL_LIST [c,c_2]]); " ^
239 " M__M = Take M__M; " ^
240 " M__M = ((Substitute c_1_2) @@ " ^
241 " (Try (Rewrite_Set_Inst [(bdv_1, c),(bdv_2, c_2)] " ^
242 " simplify_System False)) @@ " ^
243 " (Rewrite Moment_Neigung False) @@ " ^
244 " (Rewrite make_fun_explicit False)) M__M; " ^
245 (*----------------------- and the same once more ------------------------*)
246 " (N__N:: bool) = " ^
247 " (SubProblem (Biegelinie',[named,integrate,function], " ^
248 " [diff,integration,named]) " ^
249 " [REAL (rhs M__M), REAL v_v, REAL_REAL y']); " ^
250 " (B__B:: bool) = " ^
251 " (SubProblem (Biegelinie',[named,integrate,function], " ^
252 " [diff,integration,named]) " ^
253 " [REAL (rhs N__N), REAL v_v, REAL_REAL y]); " ^
254 " e__1 = NTH 1 r_b; " ^
255 " (x__1::real) = argument_in (lhs e__1); " ^
256 " (B__1::bool) = (Substitute [v_v = x__1]) B__B; " ^
257 " B__1 = (Substitute [e__1]) B__1 ; " ^
258 " B__2 = Take B__B; " ^
259 " e__2 = NTH 2 r_b; " ^
260 " (x__2::real) = argument_in (lhs e__2); " ^
261 " (B__2::bool) = (Substitute [v_v = x__2]) B__B; " ^
262 " B__2 = (Substitute [e__2]) B__2 ; " ^
263 " (c_1_2::bool list) = " ^
264 " (SubProblem (Biegelinie',[LINEAR,system],[no_met]) " ^
265 " [BOOL_LIST [B__1, B__2], REAL_LIST [c,c_2]]); " ^
266 " B__B = Take B__B; " ^
267 " B__B = ((Substitute c_1_2) @@ " ^
268 " (Rewrite_Set_Inst [(bdv, x)] make_ratpoly_in False)) B__B " ^
274 (prep_met thy "met_biege_2" [] e_metID
275 (["IntegrierenUndKonstanteBestimmen2"],
276 [("#Given" ,["Traegerlaenge l_l", "Streckenlast q__q", "FunktionsVariable v_v"]),
277 (*("#Where",["0 < l_l"]), ...wait for < and handling Arbfix*)
278 ("#Find" ,["Biegelinie b_b"]),
279 ("#Relate",["Randbedingungen r_b"])],
280 {rew_ord'="tless_true",
281 rls' = append_rls "erls_IntegrierenUndK.." e_rls
282 [Calc ("Atools.ident",eval_ident "#ident_"),
283 Thm ("not_true",num_str @{thm not_true}),
284 Thm ("not_false",num_str @{thm not_false})],
286 srls = append_rls "erls_IntegrierenUndK.." e_rls
287 [Calc("Tools.rhs", eval_rhs"eval_rhs_"),
288 Calc ("Atools.ident",eval_ident "#ident_"),
289 Thm ("last_thmI",num_str @{thm last_thmI}),
290 Thm ("if_True",num_str @{thm if_True}),
291 Thm ("if_False",num_str @{thm if_False})],
292 prls = Erls, crls = Atools_erls, errpats = [], nrls = Erls},
293 "Script Biegelinie2Script " ^
294 "(l_l::real) (q__q::real) (v_v::real) (b_b::real=>real) (r_b::bool list) = " ^
296 " (fun_s:: bool list) = " ^
297 " (SubProblem (Biegelinie',[vonBelastungZu,Biegelinien], " ^
298 " [Biegelinien,ausBelastung]) " ^
299 " [REAL q__q, REAL v_v]); " ^
300 " (equ_s::bool list) = " ^
301 " (SubProblem (Biegelinie',[setzeRandbedingungen,Biegelinien], " ^
302 " [Biegelinien,setzeRandbedingungenEin]) " ^
303 " [BOOL_LIST fun_s, BOOL_LIST r_b]); " ^
304 " (con_s::bool list) = " ^
305 " (SubProblem (Biegelinie',[LINEAR,system],[no_met]) " ^
306 " [BOOL_LIST equ_s, REAL_LIST [c,c_2,c_3,c_4]]); " ^
307 " B_B = Take (lastI fun_s); " ^
308 " B_B = ((Substitute con_s) @@ " ^
309 " (Rewrite_Set_Inst [(bdv, v_v)] make_ratpoly_in False)) B_B " ^
316 (prep_met thy "met_biege_intconst_2" [] e_metID
317 (["IntegrierenUndKonstanteBestimmen","2xIntegrieren"],
319 {rew_ord'="tless_true", rls'=Erls, calc = [],
322 crls = Atools_erls, errpats = [], nrls = e_rls},
327 (prep_met thy "met_biege_intconst_4" [] e_metID
328 (["IntegrierenUndKonstanteBestimmen","4x4System"],
330 {rew_ord'="tless_true", rls'=Erls, calc = [],
333 crls = Atools_erls, errpats = [], nrls = e_rls},
338 (prep_met thy "met_biege_intconst_1" [] e_metID
339 (["IntegrierenUndKonstanteBestimmen","1xIntegrieren"],
341 {rew_ord'="tless_true", rls'=Erls, calc = [],
344 crls = Atools_erls, errpats = [], nrls = e_rls},
349 (prep_met thy "met_biege2" [] e_metID
352 {rew_ord'="tless_true", rls'=Erls, calc = [],
355 crls = Atools_erls, errpats = [], nrls = e_rls},
362 (prep_met thy "met_biege_ausbelast" [] e_metID
363 (["Biegelinien", "ausBelastung"],
364 [("#Given" ,["Streckenlast q__q", "FunktionsVariable v_v"]),
365 ("#Find" ,["Funktionen fun_s"])],
366 {rew_ord'="tless_true",
367 rls' = append_rls "erls_ausBelastung" e_rls
368 [Calc ("Atools.ident", eval_ident "#ident_"),
369 Thm ("not_true", num_str @{thm not_true}),
370 Thm ("not_false", num_str @{thm not_false})],
372 srls = append_rls "srls_ausBelastung" e_rls
373 [Calc ("Tools.rhs", eval_rhs "eval_rhs_")],
374 prls = e_rls, crls = Atools_erls, errpats = [], nrls = e_rls},
375 "Script Belastung2BiegelScript (q__q::real) (v_v::real) = " ^
376 " (let q___q = Take (qq v_v = q__q); " ^
377 " q___q = ((Rewrite sym_neg_equal_iff_equal True) @@ " ^
378 " (Rewrite Belastung_Querkraft True)) q___q; " ^
379 " (Q__Q:: bool) = " ^
380 " (SubProblem (Biegelinie',[named,integrate,function], " ^
381 " [diff,integration,named]) " ^
382 " [REAL (rhs q___q), REAL v_v, REAL_REAL Q]); " ^
383 " M__M = Rewrite Querkraft_Moment True Q__Q; " ^
385 " (SubProblem (Biegelinie',[named,integrate,function], " ^
386 " [diff,integration,named]) " ^
387 " [REAL (rhs M__M), REAL v_v, REAL_REAL M_b]); " ^
388 " N__N = ((Rewrite Moment_Neigung False) @@ " ^
389 " (Rewrite make_fun_explicit False)) M__M; " ^
390 " (N__N:: bool) = " ^
391 " (SubProblem (Biegelinie',[named,integrate,function], " ^
392 " [diff,integration,named]) " ^
393 " [REAL (rhs N__N), REAL v_v, REAL_REAL y']); " ^
394 " (B__B:: bool) = " ^
395 " (SubProblem (Biegelinie',[named,integrate,function], " ^
396 " [diff,integration,named]) " ^
397 " [REAL (rhs N__N), REAL v_v, REAL_REAL y]) " ^
398 " in [Q__Q, M__M, N__N, B__B])"
404 (prep_met thy "met_biege_setzrand" [] e_metID
405 (["Biegelinien", "setzeRandbedingungenEin"],
406 [("#Given" , ["Funktionen fun_s", "Randbedingungen r_b"]),
407 ("#Find" , ["Gleichungen equs'''"])],
408 {rew_ord'="tless_true", rls'=Erls, calc = [],
411 crls = Atools_erls, errpats = [], nrls = e_rls},
412 "Script SetzeRandbedScript (fun_s::bool list) (r_b::bool list) = " ^
413 " (let b_1 = NTH 1 r_b; " ^
414 " f_s = filter_sameFunId (lhs b_1) fun_s; " ^
416 " (SubProblem (Biegelinie',[makeFunctionTo,equation]," ^
417 " [Equation,fromFunction]) " ^
418 " [BOOL (hd f_s), BOOL b_1]); " ^
419 " b_2 = NTH 2 r_b; " ^
420 " f_s = filter_sameFunId (lhs b_2) fun_s; " ^
422 " (SubProblem (Biegelinie',[makeFunctionTo,equation]," ^
423 " [Equation,fromFunction]) " ^
424 " [BOOL (hd f_s), BOOL b_2]); " ^
425 " b_3 = NTH 3 r_b; " ^
426 " f_s = filter_sameFunId (lhs b_3) fun_s; " ^
428 " (SubProblem (Biegelinie',[makeFunctionTo,equation]," ^
429 " [Equation,fromFunction]) " ^
430 " [BOOL (hd f_s), BOOL b_3]); " ^
431 " b_4 = NTH 4 r_b; " ^
432 " f_s = filter_sameFunId (lhs b_4) fun_s; " ^
434 " (SubProblem (Biegelinie',[makeFunctionTo,equation]," ^
435 " [Equation,fromFunction]) " ^
436 " [BOOL (hd f_s), BOOL b_4]) " ^
437 " in [e_1, e_2, e_3, e_4])"
438 (* filter requires more than 1 sec !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!
439 "Script SetzeRandbedScript (fun_s::bool list) (r_b::bool list) = " ^
440 " (let b_1 = NTH 1 r_b; " ^
441 " f_s = filter (sameFunId (lhs b_1)) fun_s; " ^
443 " (SubProblem (Biegelinie',[makeFunctionTo,equation]," ^
444 " [Equation,fromFunction]) " ^
445 " [BOOL (hd f_s), BOOL b_1]); " ^
446 " b_2 = NTH 2 r_b; " ^
447 " f_s = filter (sameFunId (lhs b_2)) fun_s; " ^
449 " (SubProblem (Biegelinie',[makeFunctionTo,equation]," ^
450 " [Equation,fromFunction]) " ^
451 " [BOOL (hd f_s), BOOL b_2]); " ^
452 " b_3 = NTH 3 r_b; " ^
453 " f_s = filter (sameFunId (lhs b_3)) fun_s; " ^
455 " (SubProblem (Biegelinie',[makeFunctionTo,equation]," ^
456 " [Equation,fromFunction]) " ^
457 " [BOOL (hd f_s), BOOL b_3]); " ^
458 " b_4 = NTH 4 r_b; " ^
459 " f_s = filter (sameFunId (lhs b_4)) fun_s; " ^
461 " (SubProblem (Biegelinie',[makeFunctionTo,equation]," ^
462 " [Equation,fromFunction]) " ^
463 " [BOOL (hd f_s), BOOL b_4]) " ^
464 " in [e_1,e_2,e_3,e_4])"*)
470 (prep_met thy "met_equ_fromfun" [] e_metID
471 (["Equation","fromFunction"],
472 [("#Given" ,["functionEq fu_n","substitution su_b"]),
473 ("#Find" ,["equality equ'''"])],
474 {rew_ord'="tless_true", rls'=Erls, calc = [],
475 srls = append_rls "srls_in_EquationfromFunc" e_rls
476 [Calc("Tools.lhs", eval_lhs"eval_lhs_"),
477 Calc("Atools.argument'_in", eval_argument_in "Atools.argument'_in")],
478 prls=e_rls, crls = Atools_erls, errpats = [], nrls = e_rls},
479 (*(M_b x = c_2 + c * x + -1 * q_0 / 2 * x ^^^ 2) (M_b L = 0) -->
480 0 = c_2 + c * L + -1 * q_0 / 2 * L ^^^ 2*)
481 "Script Function2Equality (fu_n::bool) (su_b::bool) =" ^
482 " (let fu_n = Take fu_n; " ^
483 " bd_v = argument_in (lhs fu_n); " ^
484 " va_l = argument_in (lhs su_b); " ^
485 " eq_u = (Substitute [bd_v = va_l]) fu_n; " ^
486 (*([1], Res), M_b L = c_2 + c * L + -1 * q_0 / 2 * L ^^^ 2*)
487 " eq_u = (Substitute [su_b]) eq_u " ^
488 " in (Rewrite_Set norm_Rational False) eq_u) "
492 setup {* KEStore_Elems.add_mets
493 [prep_met thy "met_biege" [] e_metID
494 (["IntegrierenUndKonstanteBestimmen"],
495 [("#Given" ,["Traegerlaenge l_l", "Streckenlast q__q", "FunktionsVariable v_v"]),
496 (*("#Where",["0 < l_l"]), ...wait for < and handling Arbfix*)
497 ("#Find" ,["Biegelinie b_b"]),
498 ("#Relate",["RandbedingungenBiegung r_b", "RandbedingungenMoment r_m"])],
499 {rew_ord'="tless_true",
500 rls' = append_rls "erls_IntegrierenUndK.." e_rls
501 [Calc ("Atools.ident",eval_ident "#ident_"),
502 Thm ("not_true",num_str @{thm not_true}),
503 Thm ("not_false",num_str @{thm not_false})],
504 calc = [], srls = srls, prls = Erls, crls = Atools_erls, errpats = [], nrls = Erls},
505 "Script BiegelinieScript " ^
506 "(l_l::real) (q__q::real) (v_v::real) (b_b::real=>real) " ^
507 "(r_b::bool list) (r_m::bool list) = " ^
508 " (let q___q = Take (qq v_v = q__q); " ^
509 " q___q = ((Rewrite sym_neg_equal_iff_equal True) @@ " ^
510 " (Rewrite Belastung_Querkraft True)) q___q; " ^
511 " (Q__Q:: bool) = " ^
512 " (SubProblem (Biegelinie',[named,integrate,function], " ^
513 " [diff,integration,named]) " ^
514 " [REAL (rhs q___q), REAL v_v, REAL_REAL Q]); " ^
515 " Q__Q = Rewrite Querkraft_Moment True Q__Q; " ^
517 " (SubProblem (Biegelinie',[named,integrate,function], " ^
518 " [diff,integration,named]) " ^
519 " [REAL (rhs Q__Q), REAL v_v, REAL_REAL M_b]); " ^
520 (*([5], Res), M_b x = c_2 + c * x + -1 * q_0 / 2 * x ^^^ 2*)
521 " e__1 = NTH 1 r_m; " ^
522 " (x__1::real) = argument_in (lhs e__1); " ^
523 " (M__1::bool) = (Substitute [v_v = x__1]) M__M; " ^
524 (*([6], Res), M_b 0 = c_2 + c * 0 + -1 * q_0 / 2 * 0 ^^^ 2*)
525 " M__1 = (Substitute [e__1]) M__1; " ^
526 (*([7], Res), 0 = c_2 + c * 0 + -1 * q_0 / 2 * 0 ^^^ 2*)
527 " M__2 = Take M__M; " ^
528 (*([8], Frm), M_b x = c_2 + c * x + -1 * q_0 / 2 * x ^^^ 2*)
529 (*without above Take 'Substitute [v_v = x__2]' takes _last formula from ctree_*)
530 " e__2 = NTH 2 r_m; " ^
531 " (x__2::real) = argument_in (lhs e__2); " ^
532 " (M__2::bool) = (Substitute [v_v = x__2]) M__M; " ^
533 (*([8], Res), M_b L = c_2 + c * L + -1 * q_0 / 2 * L ^^^ 2*)
534 " M__2 = (Substitute [e__2]) M__2; " ^
535 " (c_1_2::bool list) = " ^
536 " (SubProblem (Biegelinie',[LINEAR,system],[no_met]) " ^
537 " [BOOL_LIST [M__1, M__2], REAL_LIST [c,c_2]]); " ^
538 " M__M = Take M__M; " ^
539 " M__M = ((Substitute c_1_2) @@ " ^
540 " (Try (Rewrite_Set_Inst [(bdv_1, c),(bdv_2, c_2)] " ^
541 " simplify_System False)) @@ " ^
542 " (Rewrite Moment_Neigung False) @@ " ^
543 " (Rewrite make_fun_explicit False)) M__M; " ^
544 (*----------------------- and the same once more ------------------------*)
545 " (N__N:: bool) = " ^
546 " (SubProblem (Biegelinie',[named,integrate,function], " ^
547 " [diff,integration,named]) " ^
548 " [REAL (rhs M__M), REAL v_v, REAL_REAL y']); " ^
549 " (B__B:: bool) = " ^
550 " (SubProblem (Biegelinie',[named,integrate,function], " ^
551 " [diff,integration,named]) " ^
552 " [REAL (rhs N__N), REAL v_v, REAL_REAL y]); " ^
553 " e__1 = NTH 1 r_b; " ^
554 " (x__1::real) = argument_in (lhs e__1); " ^
555 " (B__1::bool) = (Substitute [v_v = x__1]) B__B; " ^
556 " B__1 = (Substitute [e__1]) B__1 ; " ^
557 " B__2 = Take B__B; " ^
558 " e__2 = NTH 2 r_b; " ^
559 " (x__2::real) = argument_in (lhs e__2); " ^
560 " (B__2::bool) = (Substitute [v_v = x__2]) B__B; " ^
561 " B__2 = (Substitute [e__2]) B__2 ; " ^
562 " (c_1_2::bool list) = " ^
563 " (SubProblem (Biegelinie',[LINEAR,system],[no_met]) " ^
564 " [BOOL_LIST [B__1, B__2], REAL_LIST [c,c_2]]); " ^
565 " B__B = Take B__B; " ^
566 " B__B = ((Substitute c_1_2) @@ " ^
567 " (Rewrite_Set_Inst [(bdv, x)] make_ratpoly_in False)) B__B " ^
569 prep_met thy "met_biege_2" [] e_metID
570 (["IntegrierenUndKonstanteBestimmen2"],
571 [("#Given" ,["Traegerlaenge l_l", "Streckenlast q__q", "FunktionsVariable v_v"]),
572 (*("#Where",["0 < l_l"]), ...wait for < and handling Arbfix*)
573 ("#Find" ,["Biegelinie b_b"]),
574 ("#Relate",["Randbedingungen r_b"])],
575 {rew_ord'="tless_true",
576 rls' = append_rls "erls_IntegrierenUndK.." e_rls
577 [Calc ("Atools.ident",eval_ident "#ident_"),
578 Thm ("not_true",num_str @{thm not_true}),
579 Thm ("not_false",num_str @{thm not_false})],
581 srls = append_rls "erls_IntegrierenUndK.." e_rls
582 [Calc("Tools.rhs", eval_rhs"eval_rhs_"),
583 Calc ("Atools.ident",eval_ident "#ident_"),
584 Thm ("last_thmI",num_str @{thm last_thmI}),
585 Thm ("if_True",num_str @{thm if_True}),
586 Thm ("if_False",num_str @{thm if_False})],
587 prls = Erls, crls = Atools_erls, errpats = [], nrls = Erls},
588 "Script Biegelinie2Script " ^
589 "(l_l::real) (q__q::real) (v_v::real) (b_b::real=>real) (r_b::bool list) = " ^
591 " (fun_s:: bool list) = " ^
592 " (SubProblem (Biegelinie',[vonBelastungZu,Biegelinien], " ^
593 " [Biegelinien,ausBelastung]) " ^
594 " [REAL q__q, REAL v_v]); " ^
595 " (equ_s::bool list) = " ^
596 " (SubProblem (Biegelinie',[setzeRandbedingungen,Biegelinien], " ^
597 " [Biegelinien,setzeRandbedingungenEin]) " ^
598 " [BOOL_LIST fun_s, BOOL_LIST r_b]); " ^
599 " (con_s::bool list) = " ^
600 " (SubProblem (Biegelinie',[LINEAR,system],[no_met]) " ^
601 " [BOOL_LIST equ_s, REAL_LIST [c,c_2,c_3,c_4]]); " ^
602 " B_B = Take (lastI fun_s); " ^
603 " B_B = ((Substitute con_s) @@ " ^
604 " (Rewrite_Set_Inst [(bdv, v_v)] make_ratpoly_in False)) B_B " ^
606 prep_met thy "met_biege_intconst_2" [] e_metID
607 (["IntegrierenUndKonstanteBestimmen","2xIntegrieren"], [],
608 {rew_ord'="tless_true", rls'=Erls, calc = [], srls = e_rls, prls=e_rls, crls = Atools_erls,
609 errpats = [], nrls = e_rls},
611 prep_met thy "met_biege_intconst_4" [] e_metID
612 (["IntegrierenUndKonstanteBestimmen","4x4System"], [],
613 {rew_ord'="tless_true", rls'=Erls, calc = [], srls = e_rls, prls=e_rls, crls = Atools_erls,
614 errpats = [], nrls = e_rls},
616 prep_met thy "met_biege_intconst_1" [] e_metID
617 (["IntegrierenUndKonstanteBestimmen","1xIntegrieren"], [],
618 {rew_ord'="tless_true", rls'=Erls, calc = [], srls = e_rls, prls=e_rls, crls = Atools_erls,
619 errpats = [], nrls = e_rls},
621 prep_met thy "met_biege2" [] e_metID
622 (["Biegelinien"], [],
623 {rew_ord'="tless_true", rls'=Erls, calc = [], srls = e_rls, prls=e_rls, crls = Atools_erls,
624 errpats = [], nrls = e_rls},
626 prep_met thy "met_biege_ausbelast" [] e_metID
627 (["Biegelinien", "ausBelastung"],
628 [("#Given" ,["Streckenlast q__q", "FunktionsVariable v_v"]),
629 ("#Find" ,["Funktionen fun_s"])],
630 {rew_ord'="tless_true",
631 rls' = append_rls "erls_ausBelastung" e_rls
632 [Calc ("Atools.ident", eval_ident "#ident_"),
633 Thm ("not_true", num_str @{thm not_true}),
634 Thm ("not_false", num_str @{thm not_false})],
636 srls = append_rls "srls_ausBelastung" e_rls
637 [Calc ("Tools.rhs", eval_rhs "eval_rhs_")],
638 prls = e_rls, crls = Atools_erls, errpats = [], nrls = e_rls},
639 "Script Belastung2BiegelScript (q__q::real) (v_v::real) = " ^
640 " (let q___q = Take (qq v_v = q__q); " ^
641 " q___q = ((Rewrite sym_neg_equal_iff_equal True) @@ " ^
642 " (Rewrite Belastung_Querkraft True)) q___q; " ^
643 " (Q__Q:: bool) = " ^
644 " (SubProblem (Biegelinie',[named,integrate,function], " ^
645 " [diff,integration,named]) " ^
646 " [REAL (rhs q___q), REAL v_v, REAL_REAL Q]); " ^
647 " M__M = Rewrite Querkraft_Moment True Q__Q; " ^
649 " (SubProblem (Biegelinie',[named,integrate,function], " ^
650 " [diff,integration,named]) " ^
651 " [REAL (rhs M__M), REAL v_v, REAL_REAL M_b]); " ^
652 " N__N = ((Rewrite Moment_Neigung False) @@ " ^
653 " (Rewrite make_fun_explicit False)) M__M; " ^
654 " (N__N:: bool) = " ^
655 " (SubProblem (Biegelinie',[named,integrate,function], " ^
656 " [diff,integration,named]) " ^
657 " [REAL (rhs N__N), REAL v_v, REAL_REAL y']); " ^
658 " (B__B:: bool) = " ^
659 " (SubProblem (Biegelinie',[named,integrate,function], " ^
660 " [diff,integration,named]) " ^
661 " [REAL (rhs N__N), REAL v_v, REAL_REAL y]) " ^
662 " in [Q__Q, M__M, N__N, B__B])"),
663 prep_met thy "met_biege_setzrand" [] e_metID
664 (["Biegelinien", "setzeRandbedingungenEin"],
665 [("#Given" , ["Funktionen fun_s", "Randbedingungen r_b"]),
666 ("#Find" , ["Gleichungen equs'''"])],
667 {rew_ord'="tless_true", rls'=Erls, calc = [], srls = srls2, prls=e_rls, crls = Atools_erls,
668 errpats = [], nrls = e_rls},
669 "Script SetzeRandbedScript (fun_s::bool list) (r_b::bool list) = " ^
670 " (let b_1 = NTH 1 r_b; " ^
671 " f_s = filter_sameFunId (lhs b_1) fun_s; " ^
673 " (SubProblem (Biegelinie',[makeFunctionTo,equation]," ^
674 " [Equation,fromFunction]) " ^
675 " [BOOL (hd f_s), BOOL b_1]); " ^
676 " b_2 = NTH 2 r_b; " ^
677 " f_s = filter_sameFunId (lhs b_2) fun_s; " ^
679 " (SubProblem (Biegelinie',[makeFunctionTo,equation]," ^
680 " [Equation,fromFunction]) " ^
681 " [BOOL (hd f_s), BOOL b_2]); " ^
682 " b_3 = NTH 3 r_b; " ^
683 " f_s = filter_sameFunId (lhs b_3) fun_s; " ^
685 " (SubProblem (Biegelinie',[makeFunctionTo,equation]," ^
686 " [Equation,fromFunction]) " ^
687 " [BOOL (hd f_s), BOOL b_3]); " ^
688 " b_4 = NTH 4 r_b; " ^
689 " f_s = filter_sameFunId (lhs b_4) fun_s; " ^
691 " (SubProblem (Biegelinie',[makeFunctionTo,equation]," ^
692 " [Equation,fromFunction]) " ^
693 " [BOOL (hd f_s), BOOL b_4]) " ^
694 " in [e_1, e_2, e_3, e_4])"
695 (* filter requires more than 1 sec !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!
696 "Script SetzeRandbedScript (fun_s::bool list) (r_b::bool list) = " ^
697 " (let b_1 = NTH 1 r_b; " ^
698 " f_s = filter (sameFunId (lhs b_1)) fun_s; " ^
700 " (SubProblem (Biegelinie',[makeFunctionTo,equation]," ^
701 " [Equation,fromFunction]) " ^
702 " [BOOL (hd f_s), BOOL b_1]); " ^
703 " b_2 = NTH 2 r_b; " ^
704 " f_s = filter (sameFunId (lhs b_2)) fun_s; " ^
706 " (SubProblem (Biegelinie',[makeFunctionTo,equation]," ^
707 " [Equation,fromFunction]) " ^
708 " [BOOL (hd f_s), BOOL b_2]); " ^
709 " b_3 = NTH 3 r_b; " ^
710 " f_s = filter (sameFunId (lhs b_3)) fun_s; " ^
712 " (SubProblem (Biegelinie',[makeFunctionTo,equation]," ^
713 " [Equation,fromFunction]) " ^
714 " [BOOL (hd f_s), BOOL b_3]); " ^
715 " b_4 = NTH 4 r_b; " ^
716 " f_s = filter (sameFunId (lhs b_4)) fun_s; " ^
718 " (SubProblem (Biegelinie',[makeFunctionTo,equation]," ^
719 " [Equation,fromFunction]) " ^
720 " [BOOL (hd f_s), BOOL b_4]) " ^
721 " in [e_1,e_2,e_3,e_4])"*)),
722 prep_met thy "met_equ_fromfun" [] e_metID
723 (["Equation","fromFunction"],
724 [("#Given" ,["functionEq fu_n","substitution su_b"]),
725 ("#Find" ,["equality equ'''"])],
726 {rew_ord'="tless_true", rls'=Erls, calc = [],
727 srls = append_rls "srls_in_EquationfromFunc" e_rls
728 [Calc("Tools.lhs", eval_lhs"eval_lhs_"),
729 Calc("Atools.argument'_in", eval_argument_in "Atools.argument'_in")],
730 prls=e_rls, crls = Atools_erls, errpats = [], nrls = e_rls},
731 (*(M_b x = c_2 + c * x + -1 * q_0 / 2 * x ^^^ 2) (M_b L = 0) -->
732 0 = c_2 + c * L + -1 * q_0 / 2 * L ^^^ 2*)
733 "Script Function2Equality (fu_n::bool) (su_b::bool) =" ^
734 " (let fu_n = Take fu_n; " ^
735 " bd_v = argument_in (lhs fu_n); " ^
736 " va_l = argument_in (lhs su_b); " ^
737 " eq_u = (Substitute [bd_v = va_l]) fu_n; " ^
738 (*([1], Res), M_b L = c_2 + c * L + -1 * q_0 / 2 * L ^^^ 2*)
739 " eq_u = (Substitute [su_b]) eq_u " ^
740 " in (Rewrite_Set norm_Rational False) eq_u) ")]