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
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 AbleitungBiegelinie :: "(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"
35 GleichungsVariablen :: "real list => una"
38 Biegelinie2Script :: "[real, real, real, real => real, real => real, bool list, real list,
40 ("((Script Biegelinie2Script (_ _ _ _ _ _ _=))// (_))" 9)
41 Biege1xIntegrierenScript ::
42 "[real,real,real,real=>real,bool list,bool list,bool list,
44 ("((Script Biege1xIntegrierenScript (_ _ _ _ _ _ _ =))// (_))" 9)
45 Belastung2BiegelScript :: "[real,real,real=>real,real=>real,
46 bool list] => bool list"
47 ("((Script Belastung2BiegelScript (_ _ _ _ =))// (_))" 9)
48 SetzeRandbedScript :: "[bool list,bool list,
49 bool list] => bool list"
50 ("((Script SetzeRandbedScript (_ _ =))// (_))" 9)
54 Querkraft_Belastung: "Q' x = -qq x" and
55 Belastung_Querkraft: "-qq x = Q' x" and
57 Moment_Querkraft: "M_b' x = Q x" and
58 Querkraft_Moment: "Q x = M_b' x" and
60 Neigung_Moment: "y'' x = -M_b x/ EI" and
61 Moment_Neigung: "M_b x = -EI * y'' x" and
63 (*according to rls 'simplify_Integral': .. = 1/a * .. instead .. = ../ a*)
64 make_fun_explicit: "Not (a =!= 0) ==> (a * (f x) = b) = (f x = 1/a * b)"
67 KEStore_Elems.add_thes
69 ["Walther Neuper 2005 supported by a grant from NMI Austria"],
70 make_isa @{theory} ("IsacKnowledge", "Theorems")
71 ["Walther Neuper 2005 supported by a grant from NMI Austria"],
72 make_thm @{theory} "IsacKnowledge" ("Belastung_Querkraft", @{thm Belastung_Querkraft})
73 ["Walther Neuper 2005 supported by a grant from NMI Austria"],
74 make_thm @{theory} "IsacKnowledge" ("Moment_Neigung", @{thm Moment_Neigung})
75 ["Walther Neuper 2005 supported by a grant from NMI Austria"],
76 make_thm @{theory} "IsacKnowledge" ("Moment_Querkraft", @{thm Moment_Querkraft})
77 ["Walther Neuper 2005 supported by a grant from NMI Austria"],
78 make_thm @{theory} "IsacKnowledge" ("Neigung_Moment", @{thm Neigung_Moment})
79 ["Walther Neuper 2005 supported by a grant from NMI Austria"],
80 make_thm @{theory} "IsacKnowledge" ("Querkraft_Belastung", @{thm Querkraft_Belastung})
81 ["Walther Neuper 2005 supported by a grant from NMI Austria"],
82 make_thm @{theory} "IsacKnowledge" ("Querkraft_Moment", @{thm Querkraft_Moment})
83 ["Walther Neuper 2005 supported by a grant from NMI Austria"],
84 make_thm @{theory} "IsacKnowledge" ("make_fun_explicit", @{thm make_fun_explicit})
85 ["Walther Neuper 2005 supported by a grant from NMI Austria"]]
89 setup \<open>KEStore_Elems.add_pbts
90 [(Specify.prep_pbt @{theory} "pbl_bieg" [] Celem.e_pblID
92 [("#Given" ,["Traegerlaenge l_l", "Streckenlast q_q"]),
93 (*("#Where",["0 < l_l"]), ...wait for < and handling Arbfix*)
94 ("#Find" ,["Biegelinie b_b"]),
95 ("#Relate",["Randbedingungen r_b"])],
96 Rule.append_rls "e_rls" Rule.e_rls [], NONE, [["IntegrierenUndKonstanteBestimmen2"]])),
97 (Specify.prep_pbt @{theory} "pbl_bieg_mom" [] Celem.e_pblID
98 (["MomentBestimmte","Biegelinien"],
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",["RandbedingungenBiegung r_b","RandbedingungenMoment r_m"])
104 Rule.append_rls "e_rls" Rule.e_rls [], NONE, [["IntegrierenUndKonstanteBestimmen"]])),
105 (Specify.prep_pbt @{theory} "pbl_bieg_momg" [] Celem.e_pblID
106 (["MomentGegebene","Biegelinien"], [], Rule.append_rls "e_rls" Rule.e_rls [], NONE,
107 [["IntegrierenUndKonstanteBestimmen","2xIntegrieren"]])),
108 (Specify.prep_pbt @{theory} "pbl_bieg_einf" [] Celem.e_pblID
109 (["einfache","Biegelinien"], [], Rule.append_rls "e_rls" Rule.e_rls [], NONE,
110 [["IntegrierenUndKonstanteBestimmen","4x4System"]])),
111 (Specify.prep_pbt @{theory} "pbl_bieg_momquer" [] Celem.e_pblID
112 (["QuerkraftUndMomentBestimmte","Biegelinien"], [], Rule.append_rls "e_rls" Rule.e_rls [], NONE,
113 [["IntegrierenUndKonstanteBestimmen","1xIntegrieren"]])),
114 (Specify.prep_pbt @{theory} "pbl_bieg_vonq" [] Celem.e_pblID
115 (["vonBelastungZu","Biegelinien"],
116 [("#Given" ,["Streckenlast q_q","FunktionsVariable v_v"]),
117 ("#Find" ,["Funktionen funs'''"])],
118 Rule.append_rls "e_rls" Rule.e_rls [], NONE, [["Biegelinien","ausBelastung"]])),
119 (Specify.prep_pbt @{theory} "pbl_bieg_randbed" [] Celem.e_pblID
120 (["setzeRandbedingungen","Biegelinien"],
121 [("#Given" ,["Funktionen fun_s","Randbedingungen r_b"]),
122 ("#Find" ,["Gleichungen equs'''"])],
123 Rule.append_rls "e_rls" Rule.e_rls [], NONE, [["Biegelinien","setzeRandbedingungenEin"]])),
124 (Specify.prep_pbt @{theory} "pbl_equ_fromfun" [] Celem.e_pblID
125 (["makeFunctionTo","equation"],
126 [("#Given" ,["functionEq fu_n","substitution su_b"]),
127 ("#Find" ,["equality equ'''"])],
128 Rule.append_rls "e_rls" Rule.e_rls [], NONE, [["Equation","fromFunction"]]))]\<close>
132 val srls = Rule.Rls {id="srls_IntegrierenUnd..",
134 rew_ord = ("termlessI",termlessI),
135 erls = Rule.append_rls "erls_in_srls_IntegrierenUnd.." Rule.e_rls
136 [(*for asm in NTH_CONS ...*)
137 Rule.Calc ("Orderings.ord_class.less",eval_equ "#less_"),
138 (*2nd NTH_CONS pushes n+-1 into asms*)
139 Rule.Calc("Groups.plus_class.plus", eval_binop "#add_")
141 srls = Rule.Erls, calc = [], errpatts = [],
142 rules = [Rule.Thm ("NTH_CONS",TermC.num_str @{thm NTH_CONS}),
143 Rule.Calc("Groups.plus_class.plus", eval_binop "#add_"),
144 Rule.Thm ("NTH_NIL",TermC.num_str @{thm NTH_NIL}),
145 Rule.Calc("Tools.lhs", Tools.eval_lhs"eval_lhs_"),
146 Rule.Calc("Tools.rhs", Tools.eval_rhs"eval_rhs_"),
147 Rule.Calc("Atools.argument'_in",
148 eval_argument_in "Atools.argument'_in")
150 scr = Rule.EmptyScr};
153 Rule.Rls {id="srls_IntegrierenUnd..",
155 rew_ord = ("termlessI",termlessI),
156 erls = Rule.append_rls "erls_in_srls_IntegrierenUnd.." Rule.e_rls
157 [(*for asm in NTH_CONS ...*)
158 Rule.Calc ("Orderings.ord_class.less",eval_equ "#less_"),
159 (*2nd NTH_CONS pushes n+-1 into asms*)
160 Rule.Calc("Groups.plus_class.plus", eval_binop "#add_")
162 srls = Rule.Erls, calc = [], errpatts = [],
163 rules = [Rule.Thm ("NTH_CONS",TermC.num_str @{thm NTH_CONS}),
164 Rule.Calc("Groups.plus_class.plus", eval_binop "#add_"),
165 Rule.Thm ("NTH_NIL", TermC.num_str @{thm NTH_NIL}),
166 Rule.Calc("Tools.lhs", Tools.eval_lhs "eval_lhs_"),
167 Rule.Calc("Atools.filter'_sameFunId",
168 eval_filter_sameFunId "Atools.filter'_sameFunId"),
169 (*WN070514 just for smltest/../biegelinie.sml ...*)
170 Rule.Calc("Atools.sameFunId", eval_sameFunId "Atools.sameFunId"),
171 Rule.Thm ("filter_Cons", TermC.num_str @{thm filter_Cons}),
172 Rule.Thm ("filter_Nil", TermC.num_str @{thm filter_Nil}),
173 Rule.Thm ("if_True", TermC.num_str @{thm if_True}),
174 Rule.Thm ("if_False", TermC.num_str @{thm if_False}),
175 Rule.Thm ("hd_thm", TermC.num_str @{thm hd_thm})
177 scr = Rule.EmptyScr};
180 section \<open>Methods\<close>
181 (* setup parent directory *)
182 setup \<open>KEStore_Elems.add_mets
183 [Specify.prep_met @{theory} "met_biege" [] Celem.e_metID
184 (["IntegrierenUndKonstanteBestimmen"], [],
185 {rew_ord'="tless_true", rls'= Rule.Erls, calc = [], srls = Rule.Erls, prls = Rule.Erls, crls =Rule.Erls,
186 errpats = [], nrls = Rule.Erls},
189 subsection \<open>Sub-problem "integrate and determine constants", nicely modularised\<close>
191 partial_function (tailrec) biegelinie ::
192 "real \<Rightarrow> real \<Rightarrow> real \<Rightarrow> (real \<Rightarrow> real) \<Rightarrow> bool list \<Rightarrow> real list \<Rightarrow> (real \<Rightarrow> real) \<Rightarrow> bool"
194 "biegelinie l q v b s vs id_abl =
196 funs = SubProblem (''Biegelinie'', [''vonBelastungZu'', ''Biegelinien''],
197 [''Biegelinien'', ''ausBelastung'']) [REAL q, REAL v, REAL_REAL b, REAL_REAL id_abl];
198 equs = SubProblem (''Biegelinie'', [''setzeRandbedingungen'', ''Biegelinien''],
199 [''Biegelinien'', ''setzeRandbedingungenEin'']) [BOOL_LIST funs, BOOL_LIST s];
200 cons = SubProblem (''Biegelinie'', [''LINEAR'', ''system''], [''no_met''])
201 [BOOL_LIST equs, REAL_LIST vs]; \<comment> \<open>PROG consts\<close>
202 B = Take (lastI funs);
203 B = ((Substitute cons) @@ (Rewrite_Set_Inst [(''bdv'', v)] ''make_ratpoly_in'' False)) B
205 setup \<open>KEStore_Elems.add_mets
206 [Specify.prep_met @{theory} "met_biege_2" [] Celem.e_metID
207 (["IntegrierenUndKonstanteBestimmen2"],
208 [("#Given" ,["Traegerlaenge l", "Streckenlast q",
209 "FunktionsVariable v", "GleichungsVariablen vs", "AbleitungBiegelinie id_abl"]),
210 (*("#Where",["0 < l"]), ...wait for < and handling Arbfix*)
211 ("#Find" ,["Biegelinie b"]),
212 ("#Relate",["Randbedingungen s"])],
213 {rew_ord'="tless_true",
214 rls' = Rule.append_rls "erls_IntegrierenUndK.." Rule.e_rls
215 [Rule.Calc ("Atools.ident",eval_ident "#ident_"),
216 Rule.Thm ("not_true",TermC.num_str @{thm not_true}),
217 Rule.Thm ("not_false",TermC.num_str @{thm not_false})],
219 srls = Rule.append_rls "erls_IntegrierenUndK.." Rule.e_rls
220 [Rule.Calc("Tools.rhs", Tools.eval_rhs"eval_rhs_"),
221 Rule.Calc ("Atools.ident",eval_ident "#ident_"),
222 Rule.Thm ("last_thmI",TermC.num_str @{thm last_thmI}),
223 Rule.Thm ("if_True",TermC.num_str @{thm if_True}),
224 Rule.Thm ("if_False",TermC.num_str @{thm if_False})],
225 prls = Rule.Erls, crls = Atools_erls, errpats = [], nrls = Rule.Erls},
226 @{thm biegelinie.simps}
227 (*""Script Biegelinie2Script " ^
228 "(l::real) (q :: real) (v :: real) (id_abl::real\<Rightarrow>real) (b :: real => real) (s :: bool list) (vs :: real list) = " ^
230 " (funs :: bool list) = (SubProblem (''Biegelinie'', " ^
231 " [''vonBelastungZu'', ''Biegelinien''], [''Biegelinien'', ''ausBelastung'']) " ^
232 " [REAL q, REAL v, REAL_REAL b, REAL_REAL id_abl]); " ^
233 " (equs :: bool list) = (SubProblem (''Biegelinie'', " ^
234 " [''setzeRandbedingungen'', ''Biegelinien''], [''Biegelinien'', ''setzeRandbedingungenEin'']) " ^
235 " [BOOL_LIST funs, BOOL_LIST s]); " ^
236 " (cons :: bool list) = (SubProblem (''Biegelinie'', " ^
237 " [''LINEAR'', ''system''], [''no_met'']) " ^
238 " [BOOL_LIST equs, REAL_LIST vs]); " ^
239 " B = Take (lastI funs); " ^
240 " B = ((Substitute cons) @@ " ^
241 " (Rewrite_Set_Inst [(''bdv'', v)] ''make_ratpoly_in'' False)) B " ^
244 setup \<open>KEStore_Elems.add_mets
245 [Specify.prep_met @{theory} "met_biege_intconst_2" [] Celem.e_metID
246 (["IntegrierenUndKonstanteBestimmen","2xIntegrieren"], [],
247 {rew_ord'="tless_true", rls'=Rule.Erls, calc = [], srls = Rule.e_rls, prls=Rule.e_rls, crls = Atools_erls,
248 errpats = [], nrls = Rule.e_rls},
250 Specify.prep_met @{theory} "met_biege_intconst_4" [] Celem.e_metID
251 (["IntegrierenUndKonstanteBestimmen","4x4System"], [],
252 {rew_ord'="tless_true", rls'=Rule.Erls, calc = [], srls = Rule.e_rls, prls=Rule.e_rls, crls = Atools_erls,
253 errpats = [], nrls = Rule.e_rls},
255 Specify.prep_met @{theory} "met_biege_intconst_1" [] Celem.e_metID
256 (["IntegrierenUndKonstanteBestimmen","1xIntegrieren"], [],
257 {rew_ord'="tless_true", rls'=Rule.Erls, calc = [], srls = Rule.e_rls, prls=Rule.e_rls, crls = Atools_erls,
258 errpats = [], nrls = Rule.e_rls},
260 Specify.prep_met @{theory} "met_biege2" [] Celem.e_metID
261 (["Biegelinien"], [],
262 {rew_ord'="tless_true", rls'=Rule.Erls, calc = [], srls = Rule.e_rls, prls=Rule.e_rls, crls = Atools_erls,
263 errpats = [], nrls = Rule.e_rls},
266 subsection \<open>Compute the general bending line\<close>
268 partial_function (tailrec) belastung_zu_biegelinie :: "real \<Rightarrow> real \<Rightarrow> (real \<Rightarrow> real) \<Rightarrow> (real \<Rightarrow> real) \<Rightarrow> bool list"
270 "belastung_zu_biegelinie q__q v_v id_fun id_abl =
271 (let q___q = Take (qq v_v = q__q);
272 q___q = ((Rewrite ''sym_neg_equal_iff_equal'' True) @@
273 (Rewrite ''Belastung_Querkraft'' True)) q___q;
274 Q__Q = SubProblem (''Biegelinie'', [''named'', ''integrate'', ''function''],
275 [''diff'', ''integration'', ''named'']) [REAL (rhs q___q), REAL v_v, REAL_REAL Q];
276 M__M = Rewrite ''Querkraft_Moment'' True Q__Q;
277 M__M = SubProblem (''Biegelinie'', [''named'', ''integrate'', ''function''],
278 [''diff'', ''integration'', ''named'']) [REAL (rhs M__M), REAL v_v, REAL_REAL M_b];
279 N__N = ((Rewrite ''Moment_Neigung'' False) @@
280 (Rewrite ''make_fun_explicit'' False)) M__M;
281 N__N = SubProblem (''Biegelinie'', [''named'', ''integrate'', ''function''],
282 [''diff'', ''integration'', ''named''])
283 [REAL (rhs N__N), REAL v_v, REAL_REAL id_abl];
284 B__B = SubProblem (''Biegelinie'', [''named'', ''integrate'', ''function''],
285 [''diff'', ''integration'', ''named''])
286 [REAL (rhs N__N), REAL v_v, REAL_REAL id_fun]
287 in [Q__Q, M__M, N__N, B__B])"
288 setup \<open>KEStore_Elems.add_mets
289 [Specify.prep_met @{theory} "met_biege_ausbelast" [] Celem.e_metID
290 (["Biegelinien", "ausBelastung"],
291 [("#Given" ,["Streckenlast q__q", "FunktionsVariable v_v",
292 "Biegelinie id_fun", "AbleitungBiegelinie id_abl"]),
293 ("#Find" ,["Funktionen fun_s"])],
294 {rew_ord'="tless_true",
295 rls' = Rule.append_rls "erls_ausBelastung" Rule.e_rls
296 [Rule.Calc ("Atools.ident", eval_ident "#ident_"),
297 Rule.Thm ("not_true", TermC.num_str @{thm not_true}),
298 Rule.Thm ("not_false", TermC.num_str @{thm not_false})],
300 srls = Rule.append_rls "srls_ausBelastung" Rule.e_rls
301 [Rule.Calc ("Tools.rhs", Tools.eval_rhs "eval_rhs_")],
302 prls = Rule.e_rls, crls = Atools_erls, errpats = [], nrls = Rule.e_rls},
303 @{thm belastung_zu_biegelinie.simps}
304 (*"Script Belastung2BiegelScript (q__q::real) (v_v::real) (id_fun::real\<Rightarrow>real) (id_abl::real\<Rightarrow>real) = " ^
305 " (let q___q = Take (qq v_v = q__q); " ^
306 " q___q = ((Rewrite ''sym_neg_equal_iff_equal'' True) @@ " ^
307 " (Rewrite ''Belastung_Querkraft'' True)) q___q; " ^
308 " (Q__Q:: bool) = " ^
309 " (SubProblem (''Biegelinie'',[''named'',''integrate'',''function''], " ^
310 " [''diff'',''integration'',''named'']) " ^
311 " [REAL (rhs q___q), REAL v_v, REAL_REAL Q]); " ^
312 " M__M = Rewrite ''Querkraft_Moment'' True Q__Q; " ^
314 " (SubProblem (''Biegelinie'',[''named'',''integrate'',''function''], " ^
315 " [''diff'',''integration'',''named'']) " ^
316 " [REAL (rhs M__M), REAL v_v, REAL_REAL M_b]); " ^
317 " N__N = ((Rewrite ''Moment_Neigung'' False) @@ " ^
318 " (Rewrite ''make_fun_explicit'' False)) M__M; " ^
319 " (N__N:: bool) = " ^
320 " (SubProblem (''Biegelinie'',[''named'',''integrate'',''function''], " ^
321 " [''diff'',''integration'', ''named'']) " ^
322 " [REAL (rhs N__N), REAL v_v, REAL_REAL id_abl]); " ^
323 " (B__B:: bool) = " ^
324 " (SubProblem (''Biegelinie'',[''named'',''integrate'',''function''], " ^
325 " [''diff'',''integration'',''named'']) " ^
326 " [REAL (rhs N__N), REAL v_v, REAL_REAL id_fun]) " ^
327 " in [Q__Q, M__M, N__N, B__B]) "*))]
329 subsection \<open>Substitute the constraints into the equations\<close>
331 partial_function (tailrec) setzte_randbedingungen :: "bool list \<Rightarrow> bool list \<Rightarrow> bool list"
333 "setzte_randbedingungen fun_s r_b =
334 (let b_1 = NTH 1 r_b;
335 f_s = filter_sameFunId (lhs b_1) fun_s;
336 e_1 = SubProblem (''Biegelinie'', [''makeFunctionTo'', ''equation''],
337 [''Equation'', ''fromFunction'']) [BOOL (hd f_s), BOOL b_1];
339 f_s = filter_sameFunId (lhs b_2) fun_s;
340 e_2 = SubProblem (''Biegelinie'', [''makeFunctionTo'', ''equation''],
341 [''Equation'', ''fromFunction'']) [BOOL (hd f_s), BOOL b_2];
343 f_s = filter_sameFunId (lhs b_3) fun_s;
344 e_3 = SubProblem (''Biegelinie'', [''makeFunctionTo'', ''equation''],
345 [''Equation'', ''fromFunction'']) [BOOL (hd f_s), BOOL b_3];
347 f_s = filter_sameFunId (lhs b_4) fun_s;
348 e_4 = SubProblem (''Biegelinie'', [''makeFunctionTo'', ''equation''],
349 [''Equation'', ''fromFunction'']) [BOOL (hd f_s), BOOL b_4]
350 in [e_1, e_2, e_3, e_4])"
351 setup \<open>KEStore_Elems.add_mets
352 [Specify.prep_met @{theory} "met_biege_setzrand" [] Celem.e_metID
353 (["Biegelinien", "setzeRandbedingungenEin"],
354 [("#Given" , ["Funktionen fun_s", "Randbedingungen r_b"]),
355 ("#Find" , ["Gleichungen equs'''"])],
356 {rew_ord'="tless_true", rls'=Rule.Erls, calc = [], srls = srls2, prls=Rule.e_rls, crls = Atools_erls,
357 errpats = [], nrls = Rule.e_rls},
358 @{thm setzte_randbedingungen.simps}
359 (*"Script SetzeRandbedScript (fun_s::bool list) (r_b::bool list) = " ^
360 " (let b_1 = NTH 1 r_b; " ^
361 " f_s = filter_sameFunId (lhs b_1) fun_s; " ^
363 " (SubProblem (''Biegelinie'',[''makeFunctionTo'',''equation'']," ^
364 " [''Equation'',''fromFunction'']) " ^
365 " [BOOL (hd f_s), BOOL b_1]); " ^
366 " b_2 = NTH 2 r_b; " ^
367 " f_s = filter_sameFunId (lhs b_2) fun_s; " ^
369 " (SubProblem (''Biegelinie'',[''makeFunctionTo'',''equation'']," ^
370 " [''Equation'',''fromFunction'']) " ^
371 " [BOOL (hd f_s), BOOL b_2]); " ^
372 " b_3 = NTH 3 r_b; " ^
373 " f_s = filter_sameFunId (lhs b_3) fun_s; " ^
375 " (SubProblem (''Biegelinie'',[''makeFunctionTo'',''equation'']," ^
376 " [''Equation'',''fromFunction'']) " ^
377 " [BOOL (hd f_s), BOOL b_3]); " ^
378 " b_4 = NTH 4 r_b; " ^
379 " f_s = filter_sameFunId (lhs b_4) fun_s; " ^
381 " (SubProblem (''Biegelinie'',[''makeFunctionTo'',''equation'']," ^
382 " [''Equation'',''fromFunction'']) " ^
383 " [BOOL (hd f_s), BOOL b_4]) " ^
384 " in [e_1, e_2, e_3, e_4])"*)
385 (* filter requires more than 1 sec !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!
386 "Script SetzeRandbedScript (fun_s::bool list) (r_b::bool list) = " ^
387 " (let b_1 = NTH 1 r_b; " ^
388 " f_s = filter (sameFunId (lhs b_1)) fun_s; " ^
390 " (SubProblem (''Biegelinie'',[''makeFunctionTo'',''equation'']," ^
391 " [''Equation'',''fromFunction'']) " ^
392 " [BOOL (hd f_s), BOOL b_1]); " ^
393 " b_2 = NTH 2 r_b; " ^
394 " f_s = filter (sameFunId (lhs b_2)) fun_s; " ^
396 " (SubProblem (''Biegelinie'',[''makeFunctionTo'',''equation'']," ^
397 " [''Equation'',''fromFunction'']) " ^
398 " [BOOL (hd f_s), BOOL b_2]); " ^
399 " b_3 = NTH 3 r_b; " ^
400 " f_s = filter (sameFunId (lhs b_3)) fun_s; " ^
402 " (SubProblem (''Biegelinie'',[''makeFunctionTo'',''equation'']," ^
403 " [''Equation'',''fromFunction'']) " ^
404 " [BOOL (hd f_s), BOOL b_3]); " ^
405 " b_4 = NTH 4 r_b; " ^
406 " f_s = filter (sameFunId (lhs b_4)) fun_s; " ^
408 " (SubProblem (''Biegelinie'',[''makeFunctionTo'',''equation'']," ^
409 " [''Equation'',''fromFunction'']) " ^
410 " [BOOL (hd f_s), BOOL b_4]) " ^
411 " in [e_1,e_2,e_3,e_4])"*))]
413 subsection \<open>Transform an equality into a function\<close>
415 (*(M_b x = c_2 + c * x + -1 * q_0 / 2 * x ^^^ 2) (M_b L = 0) -->
416 0 = c_2 + c * L + -1 * q_0 / 2 * L ^^^ 2*)
417 partial_function (tailrec) function_to_equality :: "bool \<Rightarrow> bool \<Rightarrow> bool"
419 "function_to_equality fu_n su_b =
420 (let fu_n = Take fu_n;
421 bd_v = argument_in (lhs fu_n);
422 va_l = argument_in (lhs su_b);
423 eq_u = Substitute [bd_v = va_l] fu_n;
424 \<comment> \<open>([1], Res), M_b L = c_2 + c * L + -1 * q_0 / 2 * L ^^^ 2\<close>
425 eq_u = Substitute [su_b] eq_u
426 in (Rewrite_Set ''norm_Rational'' False) eq_u)"
427 setup \<open>KEStore_Elems.add_mets
428 [Specify.prep_met @{theory} "met_equ_fromfun" [] Celem.e_metID
429 (["Equation","fromFunction"],
430 [("#Given" ,["functionEq fu_n","substitution su_b"]),
431 ("#Find" ,["equality equ'''"])],
432 {rew_ord'="tless_true", rls'=Rule.Erls, calc = [],
433 srls = Rule.append_rls "srls_in_EquationfromFunc" Rule.e_rls
434 [Rule.Calc("Tools.lhs", Tools.eval_lhs "eval_lhs_"),
435 Rule.Calc("Atools.argument'_in", eval_argument_in "Atools.argument'_in")],
436 prls=Rule.e_rls, crls = Atools_erls, errpats = [], nrls = Rule.e_rls},
437 (*(M_b x = c_2 + c * x + -1 * q_0 / 2 * x ^^^ 2) (M_b L = 0) -->
438 0 = c_2 + c * L + -1 * q_0 / 2 * L ^^^ 2*)
439 @{thm function_to_equality.simps}
440 (*"Script Function2Equality (fu_n::bool) (su_b::bool) =" ^
441 " (let fu_n = Take fu_n; " ^
442 " bd_v = argument_in (lhs fu_n); " ^
443 " va_l = argument_in (lhs su_b); " ^
444 " eq_u = (Substitute [bd_v = va_l]) fu_n; " ^
445 (*([1], Res), M_b L = c_2 + c * L + -1 * q_0 / 2 * L ^^^ 2*)
446 " eq_u = (Substitute [su_b]) eq_u " ^
447 " in (Rewrite_Set ''norm_Rational'' False) eq_u) "*))]