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 Base_Tools begin
9 section \<open>Constants specific for Biegelinie\<close>
12 qq :: "real => real" (* 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 Isabelle2020: new handling of quotes in mixfix, so the parser cannot distinguish M_b M_b'
19 Outcommenting causes error at Neigung_Moment: "y'' x = -M_b x/ EI" below:
20 Ambiguous input\<^here> produces 2 parse trees:
21 ("\<^const>HOL.Trueprop"
22 ("\<^const>HOL.eq" ("_applC" ("_position" y'') ("_position" x))
23 ("\<^const>Fields.inverse_class.inverse_divide" ("\<^const>Groups.uminus_class.uminus" ("_applC" ("\<^const>Biegelinie_Test.M_b") ("_position" x)))
25 ("\<^const>HOL.Trueprop"
26 ("\<^const>HOL.eq" ("_applC" ("_position" y'') ("_position" x))
27 ("\<^const>Fields.inverse_class.inverse_divide" ("\<^const>Groups.uminus_class.uminus" ("_applC" ("\<^const>Biegelinie_Test.M_b'") ("_position" x)))
29 Ambiguous input -------------------------------------------------------------------------------------------------------^^^^^^
30 2 terms are type correct:
31 ((y'' x) = ((- (M_b x)) / EI))
32 ((y'' x) = ((- (M_b x)) / EI))
35 y'' :: "real => real" (* 2.Ableitung der Biegeline *)
36 y' :: "real => real" (* Neigung der Biegeline *)
37 (*y :: "real => real" (* Biegeline *)*)
38 EI :: "real" (* Biegesteifigkeit *)
41 section \<open>Descriptions extending Input_Descript.thy\<close>
44 Traegerlaenge :: "real => una"
45 Streckenlast :: "real => una"
46 BiegemomentVerlauf :: "bool => una"
47 Biegelinie :: "(real => real) => una"
48 AbleitungBiegelinie :: "(real => real) => una"
49 Randbedingungen :: "bool list => una"
50 RandbedingungenBiegung :: "bool list => una"
51 RandbedingungenNeigung :: "bool list => una"
52 RandbedingungenMoment :: "bool list => una"
53 RandbedingungenQuerkraft :: "bool list => una"
54 FunktionsVariable :: "real => una"
55 Funktionen :: "bool list => una"
56 Gleichungen :: "bool list => una"
57 GleichungsVariablen :: "real list => una"
60 section \<open>Theorems from statics, still as axioms\<close>
64 Querkraft_Belastung: "Q' x = -qq x" and
65 Belastung_Querkraft: "-qq x = Q' x" and
67 Moment_Querkraft: "M_b' x = Q x" and
68 Querkraft_Moment: "Q x = M_b' x" and
70 Neigung_Moment: "y'' x = -M_b (x / EI)" and
71 Moment_Neigung: "(M_b x) = -EI * y'' x" and
73 (*according to rls 'simplify_Integral': .. = 1/a * .. instead .. = ../ a*)
74 make_fun_explicit: "~ (a =!= 0) ==> (a * (f x) = bb) = (f x = 1/a * bb)"
77 section \<open>Acknowledgements shown in browsers of Isac_Knowledge\<close>
79 setup \<open>ThyC.set_metadata {
80 coursedesign = ["(c) Christian Dürnsteiner 2006 supported by a grant from NMI Austria"],
81 mathauthors = ["Walther Neuper 2005 supported by a grant from NMI Austria"]}
83 (* ? more finegrained as above in Isabelle/PIDE ?* )
86 [Thy_Hierarchy.make_thy @{theory}
87 ["Walther Neuper 2005 supported by a grant from NMI Austria"],
88 Thy_Hierarchy.make_isa @{theory} ("IsacKnowledge", "Theorems")
89 ["Walther Neuper 2005 supported by a grant from NMI Austria"],
90 Thy_Hierarchy.make_thm @{theory} "IsacKnowledge" ("Belastung_Querkraft", @{thm Belastung_Querkraft})
91 ["Walther Neuper 2005 supported by a grant from NMI Austria"],
92 Thy_Hierarchy.make_thm @{theory} "IsacKnowledge" ("Moment_Neigung", @{thm Moment_Neigung})
93 ["Walther Neuper 2005 supported by a grant from NMI Austria"],
94 Thy_Hierarchy.make_thm @{theory} "IsacKnowledge" ("Moment_Querkraft", @{thm Moment_Querkraft})
95 ["Walther Neuper 2005 supported by a grant from NMI Austria"],
96 Thy_Hierarchy.make_thm @{theory} "IsacKnowledge" ("Neigung_Moment", @{thm Neigung_Moment})
97 ["Walther Neuper 2005 supported by a grant from NMI Austria"],
98 Thy_Hierarchy.make_thm @{theory} "IsacKnowledge" ("Querkraft_Belastung", @{thm Querkraft_Belastung})
99 ["Walther Neuper 2005 supported by a grant from NMI Austria"],
100 Thy_Hierarchy.make_thm @{theory} "IsacKnowledge" ("Querkraft_Moment", @{thm Querkraft_Moment})
101 ["Walther Neuper 2005 supported by a grant from NMI Austria"],
102 Thy_Hierarchy.make_thm @{theory} "IsacKnowledge" ("make_fun_explicit", @{thm make_fun_explicit})
103 ["Walther Neuper 2005 supported by a grant from NMI Austria"]]
107 section \<open>Problem.T\<close>
109 (Only) here was a trial to decouple the model of the problem from the model of the method.
110 E.g. for "Traegerlaenge" in the problem we had "l_l", while in the method we had "beam".
111 This had been working with the old "fun arguments_from_model, relate_args" in LItool.
112 But the Pre_Conds of Biegelinie were empty at that time --
113 -- how should this work with Pre_Conds <>[] involved with both, problem and method?
114 A kind of "model-translation" (see the old "fun LItool.arguments_from_model";
115 there is already an implicit kind of relation exploitet by refinement)?
116 In this changeset there is the decision to make the two models equal, of model and of method.
118 problem pbl_bieg : "Biegelinien" =
119 \<open>Rule_Set.append_rules "empty" Rule_Set.empty []\<close>
120 Method_Ref: "IntegrierenUndKonstanteBestimmen2"
121 Given: "Traegerlaenge l_l" "Streckenlast q_q"
122 (* Where: "0 < l_l" ...wait for < and handling Arbfix*)
123 Find: "Biegelinie b_b"
124 Relate: "Randbedingungen r_b"
126 (* Traegerlaenge beam Biegelinie!TYPE! id_fun AbleitungBiegelinie id_der
127 Streckenlast load Randbedingungen side_conds Biegelinie \<noteq>!TYPE!
128 FunktionsVariable fun_var GleichungsVariablen vs *)
129 partial_function (tailrec) biegelinie ::
130 "real \<Rightarrow> real \<Rightarrow> real \<Rightarrow> (real \<Rightarrow> real) \<Rightarrow> bool list \<Rightarrow> real list \<Rightarrow> (real \<Rightarrow> real) \<Rightarrow> bool"
132 "biegelinie beam load fun_var id_fun side_conds vs id_der = (
134 funs = SubProblem (''Biegelinie'', [''vonBelastungZu'', ''Biegelinien''],
135 [''Biegelinien'', ''ausBelastung''])
136 [REAL load, REAL fun_var, REAL_REAL id_fun, REAL_REAL id_der];
137 equs = SubProblem (''Biegelinie'', [''setzeRandbedingungen'', ''Biegelinien''],
138 [''Biegelinien'', ''setzeRandbedingungenEin'']) [BOOL_LIST funs, BOOL_LIST side_conds];
139 cons = SubProblem (''Biegelinie'', [''LINEAR'', ''system''],
140 [''no_met'']) [BOOL_LIST equs, REAL_LIST vs];
141 B = Take (lastI funs);
142 B = ((Substitute cons) #> (Rewrite_Set_Inst [(''bdv'', fun_var)] ''make_ratpoly_in'')) B
145 method met_biege_2 : "IntegrierenUndKonstanteBestimmen2" =
146 \<open>{rew_ord="tless_true",
147 rls' = Rule_Set.append_rules "erls_IntegrierenUndK.." Rule_Set.empty [
148 \<^rule_eval>\<open>Prog_Expr.ident\<close> (Prog_Expr.eval_ident "#ident_"),
149 \<^rule_thm>\<open>not_true\<close>,
150 \<^rule_thm>\<open>not_false\<close>],
152 prog_rls = Rule_Set.append_rules "erls_IntegrierenUndK.." Rule_Set.empty [
153 \<^rule_eval>\<open>Prog_Expr.rhs\<close> (Prog_Expr.eval_rhs"eval_rhs_"),
154 \<^rule_eval>\<open>Prog_Expr.ident\<close> (Prog_Expr.eval_ident "#ident_"),
155 \<^rule_thm>\<open>last_thmI\<close>,
156 \<^rule_thm>\<open>if_True\<close>,
157 \<^rule_thm>\<open>if_False\<close>],
158 where_rls = Rule_Set.Empty, errpats = [], rew_rls = Rule_Set.Empty}\<close>
159 Program: biegelinie.simps
160 Given: "Traegerlaenge beam" "Streckenlast load"
161 "FunktionsVariable fun_var" "GleichungsVariablen vs" "AbleitungBiegelinie id_der"
162 (* Where: "0 < beam" ...wait for < and handling Arbfix*)
163 Find: "Biegelinie id_fun"
164 Relate: "Randbedingungen side_conds"
166 problem pbl_bieg : "Biegelinien" =
167 \<open>Rule_Set.append_rules "empty" Rule_Set.empty []\<close>
168 Method_Ref: "IntegrierenUndKonstanteBestimmen2"
169 Given: "Traegerlaenge l_l" "Streckenlast q_q"
170 (* Where: "0 < l_l" ...wait for < and handling Arbfix*)
171 Find: "Biegelinie b_b"
172 Relate: "Randbedingungen r_b"
174 problem pbl_bieg_mom : "MomentBestimmte/Biegelinien" =
175 \<open>Rule_Set.append_rules "empty" Rule_Set.empty []\<close>
176 Method_Ref: "IntegrierenUndKonstanteBestimmen"
177 Given: "Traegerlaenge l_l" "Streckenlast q_q"
178 (* Where: "0 < l_l" ...wait for < and handling Arbfix*)
179 Find: "Biegelinie b_b"
180 Relate: "RandbedingungenBiegung r_b" "RandbedingungenMoment r_m"
182 problem pbl_bieg_momg : "MomentGegebene/Biegelinien" =
183 \<open>Rule_Set.append_rules "empty" Rule_Set.empty []\<close>
184 Method_Ref: "IntegrierenUndKonstanteBestimmen/2xIntegrieren"
186 problem pbl_bieg_einf : "einfache/Biegelinien" =
187 \<open>Rule_Set.append_rules "empty" Rule_Set.empty []\<close>
188 Method_Ref: "IntegrierenUndKonstanteBestimmen/4x4System"
190 problem pbl_bieg_momquer : "QuerkraftUndMomentBestimmte/Biegelinien" =
191 \<open>Rule_Set.append_rules "empty" Rule_Set.empty []\<close>
192 Method_Ref: "IntegrierenUndKonstanteBestimmen/1xIntegrieren"
194 problem pbl_bieg_vonq : "vonBelastungZu/Biegelinien" =
195 \<open>Rule_Set.append_rules "empty" Rule_Set.empty []\<close>
196 Method_Ref: "Biegelinien/ausBelastung"
197 Given: "Streckenlast q_q" "FunktionsVariable v_v"
198 Find: "Funktionen funs'''"
200 problem pbl_bieg_randbed : "setzeRandbedingungen/Biegelinien" =
201 \<open>Rule_Set.append_rules "empty" Rule_Set.empty []\<close>
202 Method_Ref: "Biegelinien/setzeRandbedingungenEin"
203 Given: "Funktionen fun_s" "Randbedingungen r_b"
204 Find: "Gleichungen equs'''"
206 problem pbl_equ_fromfun : "makeFunctionTo/equation" =
207 \<open>Rule_Set.append_rules "empty" Rule_Set.empty []\<close>
208 Method_Ref: "Equation/fromFunction"
209 Given: "functionEq fu_n" "substitution su_b"
210 Find: "equality equ'''"
215 val prog_rls = Rule_Def.Repeat {
216 id="srls_IntegrierenUnd..", preconds = [], rew_ord = ("termlessI",termlessI),
217 asm_rls = Rule_Set.append_rules "erls_in_srls_IntegrierenUnd.." Rule_Set.empty [
218 (*for asm in NTH_CONS ...*)
219 \<^rule_eval>\<open>less\<close> (Prog_Expr.eval_equ "#less_"),
220 (*2nd NTH_CONS pushes n+-1 into asms*)
221 \<^rule_eval>\<open>plus\<close> (**)(Calc_Binop.numeric "#add_")],
222 prog_rls = Rule_Set.Empty, calc = [], errpatts = [],
224 \<^rule_thm>\<open>NTH_CONS\<close>,
225 \<^rule_eval>\<open>plus\<close> (**)(Calc_Binop.numeric "#add_"),
226 \<^rule_thm>\<open>NTH_NIL\<close>,
227 \<^rule_eval>\<open>Prog_Expr.lhs\<close> (Prog_Expr.eval_lhs"eval_lhs_"),
228 \<^rule_eval>\<open>Prog_Expr.rhs\<close> (Prog_Expr.eval_rhs"eval_rhs_"),
229 \<^rule_eval>\<open>Prog_Expr.argument_in\<close> (Prog_Expr.eval_argument_in "Prog_Expr.argument_in")],
230 program = Rule.Empty_Prog};
232 val srls2 = Rule_Def.Repeat {
233 id="srls_IntegrierenUnd..", preconds = [], rew_ord = ("termlessI",termlessI),
234 asm_rls = Rule_Set.append_rules "erls_in_srls_IntegrierenUnd.." Rule_Set.empty [
235 (*for asm in NTH_CONS ...*)
236 \<^rule_eval>\<open>less\<close> (Prog_Expr.eval_equ "#less_"),
237 (*2nd NTH_CONS pushes n+-1 into asms*)
238 \<^rule_eval>\<open>plus\<close> (**)(Calc_Binop.numeric "#add_")],
239 prog_rls = Rule_Set.Empty, calc = [], errpatts = [],
241 \<^rule_thm>\<open>NTH_CONS\<close>,
242 \<^rule_eval>\<open>plus\<close> (**)(Calc_Binop.numeric "#add_"),
243 \<^rule_thm>\<open>NTH_NIL\<close>,
244 \<^rule_eval>\<open>Prog_Expr.lhs\<close> (Prog_Expr.eval_lhs "eval_lhs_"),
245 \<^rule_eval>\<open>Prog_Expr.filter_sameFunId\<close> (Prog_Expr.eval_filter_sameFunId "Prog_Expr.filter_sameFunId"),
246 (*WN070514 just for smltest/../biegelinie.sml ...*)
247 \<^rule_eval>\<open>Prog_Expr.sameFunId\<close> (Prog_Expr.eval_sameFunId "Prog_Expr.sameFunId"),
248 \<^rule_thm>\<open>filter_Cons\<close>,
249 \<^rule_thm>\<open>filter_Nil\<close>,
250 \<^rule_thm>\<open>if_True\<close>,
251 \<^rule_thm>\<open>if_False\<close>,
252 \<^rule_thm>\<open>hd_thm\<close>],
253 program = Rule.Empty_Prog};
256 section \<open>Methods\<close>
257 (* setup parent directory *)
258 method met_biege : "IntegrierenUndKonstanteBestimmen" =
259 \<open>{rew_ord="tless_true", rls'= Rule_Set.Empty, calc = [], prog_rls = Rule_Set.Empty, where_rls = Rule_Set.Empty,
260 errpats = [], rew_rls = Rule_Set.Empty}\<close>
262 subsection \<open>Survey on Methods\<close>
264 Theory "Biegelinie" used by all Subproblems
265 v-- the root Problem calling SubProblems according to indentation
267 Problem ["Biegelinien"]
268 MethodC ["IntegrierenUndKonstanteBestimmen2"] biegelinie
270 Problem ["vonBelastungZu", "Biegelinien"]
271 MethodC ["Biegelinien", "ausBelastung"] belastung_zu_biegelinie
273 Problem ["named", "integrate", "function"]
274 MethodC ["diff", "integration", "named"]
278 Problem ["setzeRandbedingungen", "Biegelinien"]
279 MethodC ["Biegelinien", "setzeRandbedingungenEin"] setzte_randbedingungen
281 Problem ["makeFunctionTo", "equation"]
282 MethodC ["Equation", "fromFunction"]
286 Problem ["LINEAR", "system"]
288 ^^^^^^--- thus automatied refinement to appropriate Problem
291 subsection \<open>Compute the general bending line\<close>
292 (* Traegerlaenge l_l Biegelinie!TYPE! b_b AbleitungBiegelinie id_der
293 Streckenlast q_q Randbedingungen r_b Biegelinie \<noteq>!TYPE!
294 FunktionsVariable fun_var GleichungsVariablen vs *)
295 partial_function (tailrec) biegelinie ::
296 "real \<Rightarrow> real \<Rightarrow> real \<Rightarrow> (real \<Rightarrow> real) \<Rightarrow> bool list \<Rightarrow> real list \<Rightarrow> (real \<Rightarrow> real) \<Rightarrow> bool"
298 "biegelinie l_l q_q fun_var b_b r_b vs id_der = (
300 funs = SubProblem (''Biegelinie'', [''vonBelastungZu'', ''Biegelinien''],
301 [''Biegelinien'', ''ausBelastung''])
302 [REAL q_q, REAL fun_var, REAL_REAL b_b, REAL_REAL id_der];
303 equs = SubProblem (''Biegelinie'', [''setzeRandbedingungen'', ''Biegelinien''],
304 [''Biegelinien'', ''setzeRandbedingungenEin'']) [BOOL_LIST funs, BOOL_LIST r_b];
305 cons = SubProblem (''Biegelinie'', [''LINEAR'', ''system''],
306 [''no_met'']) [BOOL_LIST equs, REAL_LIST vs];
307 B = Take (lastI funs);
308 B = ((Substitute cons) #> (Rewrite_Set_Inst [(''bdv'', fun_var)] ''make_ratpoly_in'')) B
311 method met_biege_2 : "IntegrierenUndKonstanteBestimmen2" =
312 \<open>{rew_ord="tless_true",
313 rls' = Rule_Set.append_rules "erls_IntegrierenUndK.." Rule_Set.empty [
314 \<^rule_eval>\<open>Prog_Expr.ident\<close> (Prog_Expr.eval_ident "#ident_"),
315 \<^rule_thm>\<open>not_true\<close>,
316 \<^rule_thm>\<open>not_false\<close>],
318 prog_rls = Rule_Set.append_rules "erls_IntegrierenUndK.." Rule_Set.empty [
319 \<^rule_eval>\<open>Prog_Expr.rhs\<close> (Prog_Expr.eval_rhs"eval_rhs_"),
320 \<^rule_eval>\<open>Prog_Expr.ident\<close> (Prog_Expr.eval_ident "#ident_"),
321 \<^rule_thm>\<open>last_thmI\<close>,
322 \<^rule_thm>\<open>if_True\<close>,
323 \<^rule_thm>\<open>if_False\<close>],
324 where_rls = Rule_Set.Empty, errpats = [], rew_rls = Rule_Set.Empty}\<close>
325 Program: biegelinie.simps
326 Given: "Traegerlaenge l_l" "Streckenlast q_q"
327 "FunktionsVariable fun_var" "GleichungsVariablen vs" "AbleitungBiegelinie id_der"
328 (* Where: "0 < l_l" ...wait for < and handling Arbfix*)
329 Find: "Biegelinie b_b"
330 Relate: "Randbedingungen r_b"
332 method met_biege_intconst_2 : "IntegrierenUndKonstanteBestimmen/2xIntegrieren" =
333 \<open>{rew_ord="tless_true", rls'=Rule_Set.Empty, calc = [], prog_rls = Rule_Set.empty, where_rls=Rule_Set.empty,
334 errpats = [], rew_rls = Rule_Set.empty}\<close>
336 method met_biege_intconst_4 : "IntegrierenUndKonstanteBestimmen/4x4System" =
337 \<open>{rew_ord="tless_true", rls'=Rule_Set.Empty, calc = [], prog_rls = Rule_Set.empty, where_rls=Rule_Set.empty,
338 errpats = [], rew_rls = Rule_Set.empty}\<close>
340 method met_biege_intconst_1 : "IntegrierenUndKonstanteBestimmen/1xIntegrieren" =
341 \<open>{rew_ord="tless_true", rls'=Rule_Set.Empty, calc = [], prog_rls = Rule_Set.empty, where_rls=Rule_Set.empty,
342 errpats = [], rew_rls = Rule_Set.empty}\<close>
344 method met_biege2 : "Biegelinien" =
345 \<open>{rew_ord="tless_true", rls'=Rule_Set.Empty, calc = [], prog_rls = Rule_Set.empty, where_rls=Rule_Set.empty,
346 errpats = [], rew_rls = Rule_Set.empty}\<close>
349 subsection \<open>Sub-problem "integrate and determine constants", nicely modularised\<close>
351 partial_function (tailrec) belastung_zu_biegelinie ::
352 (* Streckenlast Biegelinie Funktionen
353 FunktionsVariable AbleitungBiegelinie *)
354 "real \<Rightarrow> real \<Rightarrow> (real \<Rightarrow> real) \<Rightarrow> (real \<Rightarrow> real) \<Rightarrow> bool list"
355 (* q__q----v_v------b_b--------------id_der------*)
359 "belastung_zu_biegelinie q__q v_v b_b id_der = (
361 q___q = Take (qq v_v = q__q);
363 (Rewrite ''sym_neg_equal_iff_equal'') #>
364 (Rewrite ''Belastung_Querkraft'')) q___q;
365 Q__Q = SubProblem (''Biegelinie'', [''named'', ''integrate'', ''function''],
366 [''diff'', ''integration'', ''named'']) [REAL (rhs q___q), REAL v_v, REAL_REAL Q];
367 M__M = Rewrite ''Querkraft_Moment'' Q__Q;
368 M__M = SubProblem (''Biegelinie'', [''named'', ''integrate'', ''function''],
369 [''diff'', ''integration'', ''named'']) [REAL (rhs M__M), REAL v_v, REAL_REAL M_b];
371 (Rewrite ''Moment_Neigung'' ) #> (Rewrite ''make_fun_explicit'' )) M__M;
372 N__N = SubProblem (''Biegelinie'', [''named'', ''integrate'', ''function''],
373 [''diff'', ''integration'', ''named'']) [REAL (rhs N__N), REAL v_v, REAL_REAL id_der];
374 B__B = SubProblem (''Biegelinie'', [''named'', ''integrate'', ''function''],
375 [''diff'', ''integration'', ''named'']) [REAL (rhs N__N), REAL v_v, REAL_REAL b_b]
377 [Q__Q, M__M, N__N, B__B])" (*..Q is Const Querkraft -------------------------^ *)
379 method met_biege_ausbelast : "Biegelinien/ausBelastung" =
380 \<open>{rew_ord="tless_true",
381 rls' = Rule_Set.append_rules "erls_ausBelastung" Rule_Set.empty [
382 \<^rule_eval>\<open>Prog_Expr.ident\<close> (Prog_Expr.eval_ident "#ident_"),
383 \<^rule_thm>\<open>not_true\<close>,
384 \<^rule_thm>\<open>not_false\<close>],
386 prog_rls = Rule_Set.append_rules "srls_ausBelastung" Rule_Set.empty [
387 \<^rule_eval>\<open>Prog_Expr.rhs\<close> (Prog_Expr.eval_rhs "eval_rhs_")],
388 where_rls = Rule_Set.empty, errpats = [], rew_rls = Rule_Set.empty}\<close>
389 Program: belastung_zu_biegelinie.simps
390 Given: "Streckenlast q__q" "FunktionsVariable v_v" "Biegelinie b_b" "AbleitungBiegelinie id_der"
391 Find: "Funktionen fun_s"
393 subsection \<open>Substitute the constraints into the equations\<close>
395 partial_function (tailrec) setzte_randbedingungen :: "bool list \<Rightarrow> bool list \<Rightarrow> bool list"
397 "setzte_randbedingungen fun_s r_b = (
400 f_s = filter_sameFunId (lhs b_1) fun_s;
401 e_1 = SubProblem (''Biegelinie'', [''makeFunctionTo'', ''equation''],
402 [''Equation'', ''fromFunction'']) [BOOL (hd f_s), BOOL b_1];
404 f_s = filter_sameFunId (lhs b_2) fun_s;
405 e_2 = SubProblem (''Biegelinie'', [''makeFunctionTo'', ''equation''],
406 [''Equation'', ''fromFunction'']) [BOOL (hd f_s), BOOL b_2];
408 f_s = filter_sameFunId (lhs b_3) fun_s;
409 e_3 = SubProblem (''Biegelinie'', [''makeFunctionTo'', ''equation''],
410 [''Equation'', ''fromFunction'']) [BOOL (hd f_s), BOOL b_3];
412 f_s = filter_sameFunId (lhs b_4) fun_s;
413 e_4 = SubProblem (''Biegelinie'', [''makeFunctionTo'', ''equation''],
414 [''Equation'', ''fromFunction'']) [BOOL (hd f_s), BOOL b_4]
416 [e_1, e_2, e_3, e_4])"
418 method met_biege_setzrand : "Biegelinien/setzeRandbedingungenEin" =
419 \<open>{rew_ord="tless_true", rls'=Rule_Set.Empty, calc = [], prog_rls = srls2, where_rls=Rule_Set.empty,
420 errpats = [], rew_rls = Rule_Set.empty}\<close>
421 Program: setzte_randbedingungen.simps
422 Given: "Funktionen fun_s" "Randbedingungen r_b"
423 Find: "Gleichungen equs'''"
426 subsection \<open>Transform an equality into a function\<close>
428 (*(M_b x = c_2 + c * x + -1 * q_0 / 2 * x \<up> 2) (M_b L = 0) -->
429 0 = c_2 + c * L + -1 * q_0 / 2 * L \<up> 2*)
430 partial_function (tailrec) function_to_equality :: "bool \<Rightarrow> bool \<Rightarrow> bool"
432 "function_to_equality fu_n su_b = (
435 bd_v = argument_in (lhs fu_n);
436 va_l = argument_in (lhs su_b);
437 eq_u = Substitute [bd_v = va_l] fu_n; \<comment> \<open>([1], Res), M_b L = c_2 + c * L + -1 * q_0 / 2 * L \<up> 2\<close>
438 eq_u = Substitute [su_b] eq_u
440 (Rewrite_Set ''norm_Rational'') eq_u)"
442 method met_equ_fromfun : "Equation/fromFunction" =
443 \<open>{rew_ord="tless_true", rls'=Rule_Set.Empty, calc = [],
444 prog_rls = Rule_Set.append_rules "srls_in_EquationfromFunc" Rule_Set.empty [
445 \<^rule_eval>\<open>Prog_Expr.lhs\<close> (Prog_Expr.eval_lhs "eval_lhs_"),
446 \<^rule_eval>\<open>Prog_Expr.argument_in\<close> (Prog_Expr.eval_argument_in "Prog_Expr.argument_in")],
447 where_rls=Rule_Set.empty, errpats = [], rew_rls = Rule_Set.empty}\<close>
448 Program: function_to_equality.simps
449 (*(M_b x = c_2 + c * x + -1 * q_0 / 2 * x \<up> 2) (M_b L = 0) -->
450 0 = c_2 + c * L + -1 * q_0 / 2 * L \<up> 2*)
451 Given: "functionEq fu_n" "substitution su_b"
452 Find: "equality equ'''"