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)"
74 KEStore_Elems.add_thes
76 ["Walther Neuper 2005 supported by a grant from NMI Austria"],
77 make_isa @{theory} ("IsacKnowledge", "Theorems")
78 ["Walther Neuper 2005 supported by a grant from NMI Austria"],
79 make_thm @{theory} "IsacKnowledge" ("Belastung_Querkraft", @{thm Belastung_Querkraft})
80 ["Walther Neuper 2005 supported by a grant from NMI Austria"],
81 make_thm @{theory} "IsacKnowledge" ("Moment_Neigung", @{thm Moment_Neigung})
82 ["Walther Neuper 2005 supported by a grant from NMI Austria"],
83 make_thm @{theory} "IsacKnowledge" ("Moment_Querkraft", @{thm Moment_Querkraft})
84 ["Walther Neuper 2005 supported by a grant from NMI Austria"],
85 make_thm @{theory} "IsacKnowledge" ("Neigung_Moment", @{thm Neigung_Moment})
86 ["Walther Neuper 2005 supported by a grant from NMI Austria"],
87 make_thm @{theory} "IsacKnowledge" ("Querkraft_Belastung", @{thm Querkraft_Belastung})
88 ["Walther Neuper 2005 supported by a grant from NMI Austria"],
89 make_thm @{theory} "IsacKnowledge" ("Querkraft_Moment", @{thm Querkraft_Moment})
90 ["Walther Neuper 2005 supported by a grant from NMI Austria"],
91 make_thm @{theory} "IsacKnowledge" ("make_fun_explicit", @{thm make_fun_explicit})
92 ["Walther Neuper 2005 supported by a grant from NMI Austria"]]
96 setup {* KEStore_Elems.add_pbts
97 [(prep_pbt @{theory} "pbl_bieg" [] e_pblID
99 [("#Given" ,["Traegerlaenge l_l", "Streckenlast q_q"]),
100 (*("#Where",["0 < l_l"]), ...wait for < and handling Arbfix*)
101 ("#Find" ,["Biegelinie b_b"]),
102 ("#Relate",["Randbedingungen r_b"])],
103 append_rls "e_rls" e_rls [], NONE, [["IntegrierenUndKonstanteBestimmen2"]])),
104 (prep_pbt @{theory} "pbl_bieg_mom" [] e_pblID
105 (["MomentBestimmte","Biegelinien"],
106 [("#Given" ,["Traegerlaenge l_l", "Streckenlast q_q"]),
107 (*("#Where",["0 < l_l"]), ...wait for < and handling Arbfix*)
108 ("#Find" ,["Biegelinie b_b"]),
109 ("#Relate",["RandbedingungenBiegung r_b","RandbedingungenMoment r_m"])
111 append_rls "e_rls" e_rls [], NONE, [["IntegrierenUndKonstanteBestimmen"]])),
112 (prep_pbt @{theory} "pbl_bieg_momg" [] e_pblID
113 (["MomentGegebene","Biegelinien"], [], append_rls "e_rls" e_rls [], NONE,
114 [["IntegrierenUndKonstanteBestimmen","2xIntegrieren"]])),
115 (prep_pbt @{theory} "pbl_bieg_einf" [] e_pblID
116 (["einfache","Biegelinien"], [], append_rls "e_rls" e_rls [], NONE,
117 [["IntegrierenUndKonstanteBestimmen","4x4System"]])),
118 (prep_pbt @{theory} "pbl_bieg_momquer" [] e_pblID
119 (["QuerkraftUndMomentBestimmte","Biegelinien"], [], append_rls "e_rls" e_rls [], NONE,
120 [["IntegrierenUndKonstanteBestimmen","1xIntegrieren"]])),
121 (prep_pbt @{theory} "pbl_bieg_vonq" [] e_pblID
122 (["vonBelastungZu","Biegelinien"],
123 [("#Given" ,["Streckenlast q_q","FunktionsVariable v_v"]),
124 ("#Find" ,["Funktionen funs'''"])],
125 append_rls "e_rls" e_rls [], NONE, [["Biegelinien","ausBelastung"]])),
126 (prep_pbt @{theory} "pbl_bieg_randbed" [] e_pblID
127 (["setzeRandbedingungen","Biegelinien"],
128 [("#Given" ,["Funktionen fun_s","Randbedingungen r_b"]),
129 ("#Find" ,["Gleichungen equs'''"])],
130 append_rls "e_rls" e_rls [], NONE, [["Biegelinien","setzeRandbedingungenEin"]])),
131 (prep_pbt @{theory} "pbl_equ_fromfun" [] e_pblID
132 (["makeFunctionTo","equation"],
133 [("#Given" ,["functionEq fu_n","substitution su_b"]),
134 ("#Find" ,["equality equ'''"])],
135 append_rls "e_rls" e_rls [], NONE, [["Equation","fromFunction"]]))] *}
139 val srls = Rls {id="srls_IntegrierenUnd..",
141 rew_ord = ("termlessI",termlessI),
142 erls = append_rls "erls_in_srls_IntegrierenUnd.." e_rls
143 [(*for asm in NTH_CONS ...*)
144 Calc ("Orderings.ord_class.less",eval_equ "#less_"),
145 (*2nd NTH_CONS pushes n+-1 into asms*)
146 Calc("Groups.plus_class.plus", eval_binop "#add_")
148 srls = Erls, calc = [], errpatts = [],
149 rules = [Thm ("NTH_CONS",num_str @{thm NTH_CONS}),
150 Calc("Groups.plus_class.plus", eval_binop "#add_"),
151 Thm ("NTH_NIL",num_str @{thm NTH_NIL}),
152 Calc("Tools.lhs", eval_lhs"eval_lhs_"),
153 Calc("Tools.rhs", eval_rhs"eval_rhs_"),
154 Calc("Atools.argument'_in",
155 eval_argument_in "Atools.argument'_in")
160 Rls {id="srls_IntegrierenUnd..",
162 rew_ord = ("termlessI",termlessI),
163 erls = append_rls "erls_in_srls_IntegrierenUnd.." e_rls
164 [(*for asm in NTH_CONS ...*)
165 Calc ("Orderings.ord_class.less",eval_equ "#less_"),
166 (*2nd NTH_CONS pushes n+-1 into asms*)
167 Calc("Groups.plus_class.plus", eval_binop "#add_")
169 srls = Erls, calc = [], errpatts = [],
170 rules = [Thm ("NTH_CONS",num_str @{thm NTH_CONS}),
171 Calc("Groups.plus_class.plus", eval_binop "#add_"),
172 Thm ("NTH_NIL", num_str @{thm NTH_NIL}),
173 Calc("Tools.lhs", eval_lhs "eval_lhs_"),
174 Calc("Atools.filter'_sameFunId",
175 eval_filter_sameFunId "Atools.filter'_sameFunId"),
176 (*WN070514 just for smltest/../biegelinie.sml ...*)
177 Calc("Atools.sameFunId", eval_sameFunId "Atools.sameFunId"),
178 Thm ("filter_Cons", num_str @{thm filter_Cons}),
179 Thm ("filter_Nil", num_str @{thm filter_Nil}),
180 Thm ("if_True", num_str @{thm if_True}),
181 Thm ("if_False", num_str @{thm if_False}),
182 Thm ("hd_thm", num_str @{thm hd_thm})
187 setup {* KEStore_Elems.add_mets
188 [prep_met @{theory} "met_biege" [] e_metID
189 (["IntegrierenUndKonstanteBestimmen"],
190 [("#Given" ,["Traegerlaenge l_l", "Streckenlast q__q", "FunktionsVariable v_v"]),
191 (*("#Where",["0 < l_l"]), ...wait for < and handling Arbfix*)
192 ("#Find" ,["Biegelinie b_b"]),
193 ("#Relate",["RandbedingungenBiegung r_b", "RandbedingungenMoment r_m"])],
194 {rew_ord'="tless_true",
195 rls' = append_rls "erls_IntegrierenUndK.." e_rls
196 [Calc ("Atools.ident",eval_ident "#ident_"),
197 Thm ("not_true",num_str @{thm not_true}),
198 Thm ("not_false",num_str @{thm not_false})],
199 calc = [], srls = srls, prls = Erls, crls = Atools_erls, errpats = [], nrls = Erls},
200 "Script BiegelinieScript " ^
201 "(l_l::real) (q__q::real) (v_v::real) (b_b::real=>real) " ^
202 "(r_b::bool list) (r_m::bool list) = " ^
203 " (let q___q = Take (qq v_v = q__q); " ^
204 " q___q = ((Rewrite sym_neg_equal_iff_equal True) @@ " ^
205 " (Rewrite Belastung_Querkraft True)) q___q; " ^
206 " (Q__Q:: bool) = " ^
207 " (SubProblem (Biegelinie',[named,integrate,function], " ^
208 " [diff,integration,named]) " ^
209 " [REAL (rhs q___q), REAL v_v, REAL_REAL Q]); " ^
210 " Q__Q = Rewrite Querkraft_Moment True Q__Q; " ^
212 " (SubProblem (Biegelinie',[named,integrate,function], " ^
213 " [diff,integration,named]) " ^
214 " [REAL (rhs Q__Q), REAL v_v, REAL_REAL M_b]); " ^
215 (*([5], Res), M_b x = c_2 + c * x + -1 * q_0 / 2 * x ^^^ 2*)
216 " e__1 = NTH 1 r_m; " ^
217 " (x__1::real) = argument_in (lhs e__1); " ^
218 " (M__1::bool) = (Substitute [v_v = x__1]) M__M; " ^
219 (*([6], Res), M_b 0 = c_2 + c * 0 + -1 * q_0 / 2 * 0 ^^^ 2*)
220 " M__1 = (Substitute [e__1]) M__1; " ^
221 (*([7], Res), 0 = c_2 + c * 0 + -1 * q_0 / 2 * 0 ^^^ 2*)
222 " M__2 = Take M__M; " ^
223 (*([8], Frm), M_b x = c_2 + c * x + -1 * q_0 / 2 * x ^^^ 2*)
224 (*without above Take 'Substitute [v_v = x__2]' takes _last formula from ctree_*)
225 " e__2 = NTH 2 r_m; " ^
226 " (x__2::real) = argument_in (lhs e__2); " ^
227 " (M__2::bool) = (Substitute [v_v = x__2]) M__M; " ^
228 (*([8], Res), M_b L = c_2 + c * L + -1 * q_0 / 2 * L ^^^ 2*)
229 " M__2 = (Substitute [e__2]) M__2; " ^
230 " (c_1_2::bool list) = " ^
231 " (SubProblem (Biegelinie',[LINEAR,system],[no_met]) " ^
232 " [BOOL_LIST [M__1, M__2], REAL_LIST [c,c_2]]); " ^
233 " M__M = Take M__M; " ^
234 " M__M = ((Substitute c_1_2) @@ " ^
235 " (Try (Rewrite_Set_Inst [(bdv_1, c),(bdv_2, c_2)] " ^
236 " simplify_System False)) @@ " ^
237 " (Rewrite Moment_Neigung False) @@ " ^
238 " (Rewrite make_fun_explicit False)) M__M; " ^
239 (*----------------------- and the same once more ------------------------*)
240 " (N__N:: bool) = " ^
241 " (SubProblem (Biegelinie',[named,integrate,function], " ^
242 " [diff,integration,named]) " ^
243 " [REAL (rhs M__M), REAL v_v, REAL_REAL y']); " ^
244 " (B__B:: bool) = " ^
245 " (SubProblem (Biegelinie',[named,integrate,function], " ^
246 " [diff,integration,named]) " ^
247 " [REAL (rhs N__N), REAL v_v, REAL_REAL y]); " ^
248 " e__1 = NTH 1 r_b; " ^
249 " (x__1::real) = argument_in (lhs e__1); " ^
250 " (B__1::bool) = (Substitute [v_v = x__1]) B__B; " ^
251 " B__1 = (Substitute [e__1]) B__1 ; " ^
252 " B__2 = Take B__B; " ^
253 " e__2 = NTH 2 r_b; " ^
254 " (x__2::real) = argument_in (lhs e__2); " ^
255 " (B__2::bool) = (Substitute [v_v = x__2]) B__B; " ^
256 " B__2 = (Substitute [e__2]) B__2 ; " ^
257 " (c_1_2::bool list) = " ^
258 " (SubProblem (Biegelinie',[LINEAR,system],[no_met]) " ^
259 " [BOOL_LIST [B__1, B__2], REAL_LIST [c,c_2]]); " ^
260 " B__B = Take B__B; " ^
261 " B__B = ((Substitute c_1_2) @@ " ^
262 " (Rewrite_Set_Inst [(bdv, x)] make_ratpoly_in False)) B__B " ^
264 prep_met @{theory} "met_biege_2" [] e_metID
265 (["IntegrierenUndKonstanteBestimmen2"],
266 [("#Given" ,["Traegerlaenge l_l", "Streckenlast q__q", "FunktionsVariable v_v"]),
267 (*("#Where",["0 < l_l"]), ...wait for < and handling Arbfix*)
268 ("#Find" ,["Biegelinie b_b"]),
269 ("#Relate",["Randbedingungen r_b"])],
270 {rew_ord'="tless_true",
271 rls' = append_rls "erls_IntegrierenUndK.." e_rls
272 [Calc ("Atools.ident",eval_ident "#ident_"),
273 Thm ("not_true",num_str @{thm not_true}),
274 Thm ("not_false",num_str @{thm not_false})],
276 srls = append_rls "erls_IntegrierenUndK.." e_rls
277 [Calc("Tools.rhs", eval_rhs"eval_rhs_"),
278 Calc ("Atools.ident",eval_ident "#ident_"),
279 Thm ("last_thmI",num_str @{thm last_thmI}),
280 Thm ("if_True",num_str @{thm if_True}),
281 Thm ("if_False",num_str @{thm if_False})],
282 prls = Erls, crls = Atools_erls, errpats = [], nrls = Erls},
283 "Script Biegelinie2Script " ^
284 "(l_l::real) (q__q::real) (v_v::real) (b_b::real=>real) (r_b::bool list) = " ^
286 " (fun_s:: bool list) = " ^
287 " (SubProblem (Biegelinie',[vonBelastungZu,Biegelinien], " ^
288 " [Biegelinien,ausBelastung]) " ^
289 " [REAL q__q, REAL v_v]); " ^
290 " (equ_s::bool list) = " ^
291 " (SubProblem (Biegelinie',[setzeRandbedingungen,Biegelinien], " ^
292 " [Biegelinien,setzeRandbedingungenEin]) " ^
293 " [BOOL_LIST fun_s, BOOL_LIST r_b]); " ^
294 " (con_s::bool list) = " ^
295 " (SubProblem (Biegelinie',[LINEAR,system],[no_met]) " ^
296 " [BOOL_LIST equ_s, REAL_LIST [c,c_2,c_3,c_4]]); " ^
297 " B_B = Take (lastI fun_s); " ^
298 " B_B = ((Substitute con_s) @@ " ^
299 " (Rewrite_Set_Inst [(bdv, v_v)] make_ratpoly_in False)) B_B " ^
301 prep_met @{theory} "met_biege_intconst_2" [] e_metID
302 (["IntegrierenUndKonstanteBestimmen","2xIntegrieren"], [],
303 {rew_ord'="tless_true", rls'=Erls, calc = [], srls = e_rls, prls=e_rls, crls = Atools_erls,
304 errpats = [], nrls = e_rls},
306 prep_met @{theory} "met_biege_intconst_4" [] e_metID
307 (["IntegrierenUndKonstanteBestimmen","4x4System"], [],
308 {rew_ord'="tless_true", rls'=Erls, calc = [], srls = e_rls, prls=e_rls, crls = Atools_erls,
309 errpats = [], nrls = e_rls},
311 prep_met @{theory} "met_biege_intconst_1" [] e_metID
312 (["IntegrierenUndKonstanteBestimmen","1xIntegrieren"], [],
313 {rew_ord'="tless_true", rls'=Erls, calc = [], srls = e_rls, prls=e_rls, crls = Atools_erls,
314 errpats = [], nrls = e_rls},
316 prep_met @{theory} "met_biege2" [] e_metID
317 (["Biegelinien"], [],
318 {rew_ord'="tless_true", rls'=Erls, calc = [], srls = e_rls, prls=e_rls, crls = Atools_erls,
319 errpats = [], nrls = e_rls},
321 prep_met @{theory} "met_biege_ausbelast" [] e_metID
322 (["Biegelinien", "ausBelastung"],
323 [("#Given" ,["Streckenlast q__q", "FunktionsVariable v_v"]),
324 ("#Find" ,["Funktionen fun_s"])],
325 {rew_ord'="tless_true",
326 rls' = append_rls "erls_ausBelastung" e_rls
327 [Calc ("Atools.ident", eval_ident "#ident_"),
328 Thm ("not_true", num_str @{thm not_true}),
329 Thm ("not_false", num_str @{thm not_false})],
331 srls = append_rls "srls_ausBelastung" e_rls
332 [Calc ("Tools.rhs", eval_rhs "eval_rhs_")],
333 prls = e_rls, crls = Atools_erls, errpats = [], nrls = e_rls},
334 "Script Belastung2BiegelScript (q__q::real) (v_v::real) = " ^
335 " (let q___q = Take (qq v_v = q__q); " ^
336 " q___q = ((Rewrite sym_neg_equal_iff_equal True) @@ " ^
337 " (Rewrite Belastung_Querkraft True)) q___q; " ^
338 " (Q__Q:: bool) = " ^
339 " (SubProblem (Biegelinie',[named,integrate,function], " ^
340 " [diff,integration,named]) " ^
341 " [REAL (rhs q___q), REAL v_v, REAL_REAL Q]); " ^
342 " M__M = Rewrite Querkraft_Moment True Q__Q; " ^
344 " (SubProblem (Biegelinie',[named,integrate,function], " ^
345 " [diff,integration,named]) " ^
346 " [REAL (rhs M__M), REAL v_v, REAL_REAL M_b]); " ^
347 " N__N = ((Rewrite Moment_Neigung False) @@ " ^
348 " (Rewrite make_fun_explicit False)) M__M; " ^
349 " (N__N:: bool) = " ^
350 " (SubProblem (Biegelinie',[named,integrate,function], " ^
351 " [diff,integration,named]) " ^
352 " [REAL (rhs N__N), REAL v_v, REAL_REAL y']); " ^
353 " (B__B:: bool) = " ^
354 " (SubProblem (Biegelinie',[named,integrate,function], " ^
355 " [diff,integration,named]) " ^
356 " [REAL (rhs N__N), REAL v_v, REAL_REAL y]) " ^
357 " in [Q__Q, M__M, N__N, B__B])"),
358 prep_met @{theory} "met_biege_setzrand" [] e_metID
359 (["Biegelinien", "setzeRandbedingungenEin"],
360 [("#Given" , ["Funktionen fun_s", "Randbedingungen r_b"]),
361 ("#Find" , ["Gleichungen equs'''"])],
362 {rew_ord'="tless_true", rls'=Erls, calc = [], srls = srls2, prls=e_rls, crls = Atools_erls,
363 errpats = [], nrls = e_rls},
364 "Script SetzeRandbedScript (fun_s::bool list) (r_b::bool list) = " ^
365 " (let b_1 = NTH 1 r_b; " ^
366 " f_s = filter_sameFunId (lhs b_1) fun_s; " ^
368 " (SubProblem (Biegelinie',[makeFunctionTo,equation]," ^
369 " [Equation,fromFunction]) " ^
370 " [BOOL (hd f_s), BOOL b_1]); " ^
371 " b_2 = NTH 2 r_b; " ^
372 " f_s = filter_sameFunId (lhs b_2) fun_s; " ^
374 " (SubProblem (Biegelinie',[makeFunctionTo,equation]," ^
375 " [Equation,fromFunction]) " ^
376 " [BOOL (hd f_s), BOOL b_2]); " ^
377 " b_3 = NTH 3 r_b; " ^
378 " f_s = filter_sameFunId (lhs b_3) fun_s; " ^
380 " (SubProblem (Biegelinie',[makeFunctionTo,equation]," ^
381 " [Equation,fromFunction]) " ^
382 " [BOOL (hd f_s), BOOL b_3]); " ^
383 " b_4 = NTH 4 r_b; " ^
384 " f_s = filter_sameFunId (lhs b_4) fun_s; " ^
386 " (SubProblem (Biegelinie',[makeFunctionTo,equation]," ^
387 " [Equation,fromFunction]) " ^
388 " [BOOL (hd f_s), BOOL b_4]) " ^
389 " in [e_1, e_2, e_3, e_4])"
390 (* filter requires more than 1 sec !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!
391 "Script SetzeRandbedScript (fun_s::bool list) (r_b::bool list) = " ^
392 " (let b_1 = NTH 1 r_b; " ^
393 " f_s = filter (sameFunId (lhs b_1)) fun_s; " ^
395 " (SubProblem (Biegelinie',[makeFunctionTo,equation]," ^
396 " [Equation,fromFunction]) " ^
397 " [BOOL (hd f_s), BOOL b_1]); " ^
398 " b_2 = NTH 2 r_b; " ^
399 " f_s = filter (sameFunId (lhs b_2)) fun_s; " ^
401 " (SubProblem (Biegelinie',[makeFunctionTo,equation]," ^
402 " [Equation,fromFunction]) " ^
403 " [BOOL (hd f_s), BOOL b_2]); " ^
404 " b_3 = NTH 3 r_b; " ^
405 " f_s = filter (sameFunId (lhs b_3)) fun_s; " ^
407 " (SubProblem (Biegelinie',[makeFunctionTo,equation]," ^
408 " [Equation,fromFunction]) " ^
409 " [BOOL (hd f_s), BOOL b_3]); " ^
410 " b_4 = NTH 4 r_b; " ^
411 " f_s = filter (sameFunId (lhs b_4)) fun_s; " ^
413 " (SubProblem (Biegelinie',[makeFunctionTo,equation]," ^
414 " [Equation,fromFunction]) " ^
415 " [BOOL (hd f_s), BOOL b_4]) " ^
416 " in [e_1,e_2,e_3,e_4])"*)),
417 prep_met @{theory} "met_equ_fromfun" [] e_metID
418 (["Equation","fromFunction"],
419 [("#Given" ,["functionEq fu_n","substitution su_b"]),
420 ("#Find" ,["equality equ'''"])],
421 {rew_ord'="tless_true", rls'=Erls, calc = [],
422 srls = append_rls "srls_in_EquationfromFunc" e_rls
423 [Calc("Tools.lhs", eval_lhs"eval_lhs_"),
424 Calc("Atools.argument'_in", eval_argument_in "Atools.argument'_in")],
425 prls=e_rls, crls = Atools_erls, errpats = [], nrls = e_rls},
426 (*(M_b x = c_2 + c * x + -1 * q_0 / 2 * x ^^^ 2) (M_b L = 0) -->
427 0 = c_2 + c * L + -1 * q_0 / 2 * L ^^^ 2*)
428 "Script Function2Equality (fu_n::bool) (su_b::bool) =" ^
429 " (let fu_n = Take fu_n; " ^
430 " bd_v = argument_in (lhs fu_n); " ^
431 " va_l = argument_in (lhs su_b); " ^
432 " eq_u = (Substitute [bd_v = va_l]) fu_n; " ^
433 (*([1], Res), M_b L = c_2 + c * L + -1 * q_0 / 2 * L ^^^ 2*)
434 " eq_u = (Substitute [su_b]) eq_u " ^
435 " in (Rewrite_Set norm_Rational False) eq_u) ")]