1 (* chapter 'Biegelinie' from the textbook: |
|
2 Timischl, Kaiser. Ingenieur-Mathematik 3. Wien 1999. p.268-271. |
|
3 authors: Walther Neuper 2005 |
|
4 (c) due to copyright terms |
|
5 |
|
6 use"IsacKnowledge/Biegelinie.ML"; |
|
7 use"Biegelinie.ML"; |
|
8 |
|
9 remove_thy"Typefix"; |
|
10 remove_thy"Biegelinie"; |
|
11 use_thy"IsacKnowledge/Isac"; |
|
12 *) |
|
13 |
|
14 (** interface isabelle -- isac **) |
|
15 |
|
16 theory' := overwritel (!theory', [("Biegelinie.thy",Biegelinie.thy)]); |
|
17 |
|
18 (** theory elements **) |
|
19 |
|
20 store_isa ["IsacKnowledge"] []; |
|
21 store_thy Biegelinie.thy |
|
22 ["Walther Neuper 2005 supported by a grant from NMI Austria"]; |
|
23 store_isa ["IsacKnowledge", theory2thyID Biegelinie.thy, "Theorems"] |
|
24 ["Walther Neuper 2005 supported by a grant from NMI Austria"]; |
|
25 store_thm Biegelinie.thy ("Belastung_Querkraft", Belastung_Querkraft) |
|
26 ["Walther Neuper 2005 supported by a grant from NMI Austria"]; |
|
27 store_thm Biegelinie.thy ("Moment_Neigung", Moment_Neigung) |
|
28 ["Walther Neuper 2005 supported by a grant from NMI Austria"]; |
|
29 store_thm Biegelinie.thy ("Moment_Querkraft", Moment_Querkraft) |
|
30 ["Walther Neuper 2005 supported by a grant from NMI Austria"]; |
|
31 store_thm Biegelinie.thy ("Neigung_Moment", Neigung_Moment) |
|
32 ["Walther Neuper 2005 supported by a grant from NMI Austria"]; |
|
33 store_thm Biegelinie.thy ("Querkraft_Belastung", Querkraft_Belastung) |
|
34 ["Walther Neuper 2005 supported by a grant from NMI Austria"]; |
|
35 store_thm Biegelinie.thy ("Querkraft_Moment", Querkraft_Moment) |
|
36 ["Walther Neuper 2005 supported by a grant from NMI Austria"]; |
|
37 store_thm Biegelinie.thy ("make_fun_explicit", make_fun_explicit) |
|
38 ["Walther Neuper 2005 supported by a grant from NMI Austria"]; |
|
39 |
|
40 |
|
41 (** problems **) |
|
42 |
|
43 store_pbt |
|
44 (prep_pbt Biegelinie.thy "pbl_bieg" [] e_pblID |
|
45 (["Biegelinien"], |
|
46 [("#Given" ,["Traegerlaenge l_", "Streckenlast q__"]), |
|
47 (*("#Where",["0 < l_"]), ...wait for < and handling Arbfix*) |
|
48 ("#Find" ,["Biegelinie b_"]), |
|
49 ("#Relate",["Randbedingungen rb_"]) |
|
50 ], |
|
51 append_rls "e_rls" e_rls [], |
|
52 NONE, |
|
53 [["IntegrierenUndKonstanteBestimmen2"]])); |
|
54 |
|
55 store_pbt |
|
56 (prep_pbt Biegelinie.thy "pbl_bieg_mom" [] e_pblID |
|
57 (["MomentBestimmte","Biegelinien"], |
|
58 [("#Given" ,["Traegerlaenge l_", "Streckenlast q__"]), |
|
59 (*("#Where",["0 < l_"]), ...wait for < and handling Arbfix*) |
|
60 ("#Find" ,["Biegelinie b_"]), |
|
61 ("#Relate",["RandbedingungenBiegung rb_","RandbedingungenMoment rm_"]) |
|
62 ], |
|
63 append_rls "e_rls" e_rls [], |
|
64 NONE, |
|
65 [["IntegrierenUndKonstanteBestimmen"]])); |
|
66 |
|
67 store_pbt |
|
68 (prep_pbt Biegelinie.thy "pbl_bieg_momg" [] e_pblID |
|
69 (["MomentGegebene","Biegelinien"], |
|
70 [], |
|
71 append_rls "e_rls" e_rls [], |
|
72 NONE, |
|
73 [["IntegrierenUndKonstanteBestimmen","2xIntegrieren"]])); |
|
74 |
|
75 store_pbt |
|
76 (prep_pbt Biegelinie.thy "pbl_bieg_einf" [] e_pblID |
|
77 (["einfache","Biegelinien"], |
|
78 [], |
|
79 append_rls "e_rls" e_rls [], |
|
80 NONE, |
|
81 [["IntegrierenUndKonstanteBestimmen","4x4System"]])); |
|
82 |
|
83 store_pbt |
|
84 (prep_pbt Biegelinie.thy "pbl_bieg_momquer" [] e_pblID |
|
85 (["QuerkraftUndMomentBestimmte","Biegelinien"], |
|
86 [], |
|
87 append_rls "e_rls" e_rls [], |
|
88 NONE, |
|
89 [["IntegrierenUndKonstanteBestimmen","1xIntegrieren"]])); |
|
90 |
|
91 store_pbt |
|
92 (prep_pbt Biegelinie.thy "pbl_bieg_vonq" [] e_pblID |
|
93 (["vonBelastungZu","Biegelinien"], |
|
94 [("#Given" ,["Streckenlast q__","FunktionsVariable v_"]), |
|
95 ("#Find" ,["Funktionen funs___"])], |
|
96 append_rls "e_rls" e_rls [], |
|
97 NONE, |
|
98 [["Biegelinien","ausBelastung"]])); |
|
99 |
|
100 store_pbt |
|
101 (prep_pbt Biegelinie.thy "pbl_bieg_randbed" [] e_pblID |
|
102 (["setzeRandbedingungen","Biegelinien"], |
|
103 [("#Given" ,["Funktionen funs_","Randbedingungen rb_"]), |
|
104 ("#Find" ,["Gleichungen equs___"])], |
|
105 append_rls "e_rls" e_rls [], |
|
106 NONE, |
|
107 [["Biegelinien","setzeRandbedingungenEin"]])); |
|
108 |
|
109 store_pbt |
|
110 (prep_pbt Biegelinie.thy "pbl_equ_fromfun" [] e_pblID |
|
111 (["makeFunctionTo","equation"], |
|
112 [("#Given" ,["functionEq fun_","substitution sub_"]), |
|
113 ("#Find" ,["equality equ___"])], |
|
114 append_rls "e_rls" e_rls [], |
|
115 NONE, |
|
116 [["Equation","fromFunction"]])); |
|
117 |
|
118 |
|
119 |
|
120 (** methods **) |
|
121 |
|
122 val srls = Rls {id="srls_IntegrierenUnd..", |
|
123 preconds = [], |
|
124 rew_ord = ("termlessI",termlessI), |
|
125 erls = append_rls "erls_in_srls_IntegrierenUnd.." e_rls |
|
126 [(*for asm in nth_Cons_ ...*) |
|
127 Calc ("op <",eval_equ "#less_"), |
|
128 (*2nd nth_Cons_ pushes n+-1 into asms*) |
|
129 Calc("op +", eval_binop "#add_") |
|
130 ], |
|
131 srls = Erls, calc = [], |
|
132 rules = [Thm ("nth_Cons_",num_str nth_Cons_), |
|
133 Calc("op +", eval_binop "#add_"), |
|
134 Thm ("nth_Nil_",num_str nth_Nil_), |
|
135 Calc("Tools.lhs", eval_lhs"eval_lhs_"), |
|
136 Calc("Tools.rhs", eval_rhs"eval_rhs_"), |
|
137 Calc("Atools.argument'_in", |
|
138 eval_argument_in "Atools.argument'_in") |
|
139 ], |
|
140 scr = EmptyScr}; |
|
141 |
|
142 val srls2 = |
|
143 Rls {id="srls_IntegrierenUnd..", |
|
144 preconds = [], |
|
145 rew_ord = ("termlessI",termlessI), |
|
146 erls = append_rls "erls_in_srls_IntegrierenUnd.." e_rls |
|
147 [(*for asm in nth_Cons_ ...*) |
|
148 Calc ("op <",eval_equ "#less_"), |
|
149 (*2nd nth_Cons_ pushes n+-1 into asms*) |
|
150 Calc("op +", eval_binop "#add_") |
|
151 ], |
|
152 srls = Erls, calc = [], |
|
153 rules = [Thm ("nth_Cons_",num_str nth_Cons_), |
|
154 Calc("op +", eval_binop "#add_"), |
|
155 Thm ("nth_Nil_", num_str nth_Nil_), |
|
156 Calc("Tools.lhs", eval_lhs "eval_lhs_"), |
|
157 Calc("Atools.filter'_sameFunId", |
|
158 eval_filter_sameFunId "Atools.filter'_sameFunId"), |
|
159 (*WN070514 just for smltest/../biegelinie.sml ...*) |
|
160 Calc("Atools.sameFunId", eval_sameFunId "Atools.sameFunId"), |
|
161 Thm ("filter_Cons", num_str filter_Cons), |
|
162 Thm ("filter_Nil", num_str filter_Nil), |
|
163 Thm ("if_True", num_str if_True), |
|
164 Thm ("if_False", num_str if_False), |
|
165 Thm ("hd_thm", num_str hd_thm) |
|
166 ], |
|
167 scr = EmptyScr}; |
|
168 (*@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@*) |
|
169 (* use"IsacKnowledge/Biegelinie.ML"; |
|
170 *) |
|
171 |
|
172 store_met |
|
173 (prep_met Biegelinie.thy "met_biege" [] e_metID |
|
174 (["IntegrierenUndKonstanteBestimmen"], |
|
175 [("#Given" ,["Traegerlaenge l_", "Streckenlast q__", |
|
176 "FunktionsVariable v_"]), |
|
177 (*("#Where",["0 < l_"]), ...wait for < and handling Arbfix*) |
|
178 ("#Find" ,["Biegelinie b_"]), |
|
179 ("#Relate",["RandbedingungenBiegung rb_", |
|
180 "RandbedingungenMoment rm_"]) |
|
181 ], |
|
182 {rew_ord'="tless_true", |
|
183 rls' = append_rls "erls_IntegrierenUndK.." e_rls |
|
184 [Calc ("Atools.ident",eval_ident "#ident_"), |
|
185 Thm ("not_true",num_str not_true), |
|
186 Thm ("not_false",num_str not_false)], |
|
187 calc = [], srls = srls, prls = Erls, |
|
188 crls = Atools_erls, nrls = Erls}, |
|
189 "Script BiegelinieScript \ |
|
190 \(l_::real) (q__::real) (v_::real) (b_::real=>real) \ |
|
191 \(rb_::bool list) (rm_::bool list) = \ |
|
192 \ (let q___ = Take (q_ v_ = q__); \ |
|
193 \ q___ = ((Rewrite sym_real_minus_eq_cancel True) @@ \ |
|
194 \ (Rewrite Belastung_Querkraft True)) q___; \ |
|
195 \ (Q__:: bool) = \ |
|
196 \ (SubProblem (Biegelinie_,[named,integrate,function], \ |
|
197 \ [diff,integration,named]) \ |
|
198 \ [real_ (rhs q___), real_ v_, real_real_ Q]); \ |
|
199 \ Q__ = Rewrite Querkraft_Moment True Q__; \ |
|
200 \ (M__::bool) = \ |
|
201 \ (SubProblem (Biegelinie_,[named,integrate,function], \ |
|
202 \ [diff,integration,named]) \ |
|
203 \ [real_ (rhs Q__), real_ v_, real_real_ M_b]); \ |
|
204 \ e1__ = nth_ 1 rm_; \ |
|
205 \ (x1__::real) = argument_in (lhs e1__); \ |
|
206 \ (M1__::bool) = (Substitute [v_ = x1__]) M__; \ |
|
207 \ M1__ = (Substitute [e1__]) M1__ ; \ |
|
208 \ M2__ = Take M__; "^ |
|
209 (*without this Take 'Substitute [v_ = x2__]' takes _last formula from ctree_*) |
|
210 " e2__ = nth_ 2 rm_; \ |
|
211 \ (x2__::real) = argument_in (lhs e2__); \ |
|
212 \ (M2__::bool) = ((Substitute [v_ = x2__]) @@ \ |
|
213 \ (Substitute [e2__])) M2__; \ |
|
214 \ (c_1_2__::bool list) = \ |
|
215 \ (SubProblem (Biegelinie_,[linear,system],[no_met]) \ |
|
216 \ [booll_ [M1__, M2__], reall [c,c_2]]); \ |
|
217 \ M__ = Take M__; \ |
|
218 \ M__ = ((Substitute c_1_2__) @@ \ |
|
219 \ (Try (Rewrite_Set_Inst [(bdv_1, c),(bdv_2, c_2)]\ |
|
220 \ simplify_System False)) @@ \ |
|
221 \ (Rewrite Moment_Neigung False) @@ \ |
|
222 \ (Rewrite make_fun_explicit False)) M__; "^ |
|
223 (*----------------------- and the same once more ------------------------*) |
|
224 " (N__:: bool) = \ |
|
225 \ (SubProblem (Biegelinie_,[named,integrate,function], \ |
|
226 \ [diff,integration,named]) \ |
|
227 \ [real_ (rhs M__), real_ v_, real_real_ y']); \ |
|
228 \ (B__:: bool) = \ |
|
229 \ (SubProblem (Biegelinie_,[named,integrate,function], \ |
|
230 \ [diff,integration,named]) \ |
|
231 \ [real_ (rhs N__), real_ v_, real_real_ y]); \ |
|
232 \ e1__ = nth_ 1 rb_; \ |
|
233 \ (x1__::real) = argument_in (lhs e1__); \ |
|
234 \ (B1__::bool) = (Substitute [v_ = x1__]) B__; \ |
|
235 \ B1__ = (Substitute [e1__]) B1__ ; \ |
|
236 \ B2__ = Take B__; \ |
|
237 \ e2__ = nth_ 2 rb_; \ |
|
238 \ (x2__::real) = argument_in (lhs e2__); \ |
|
239 \ (B2__::bool) = ((Substitute [v_ = x2__]) @@ \ |
|
240 \ (Substitute [e2__])) B2__; \ |
|
241 \ (c_1_2__::bool list) = \ |
|
242 \ (SubProblem (Biegelinie_,[linear,system],[no_met]) \ |
|
243 \ [booll_ [B1__, B2__], reall [c,c_2]]); \ |
|
244 \ B__ = Take B__; \ |
|
245 \ B__ = ((Substitute c_1_2__) @@ \ |
|
246 \ (Rewrite_Set_Inst [(bdv, x)] make_ratpoly_in False)) B__ \ |
|
247 \ in B__)" |
|
248 )); |
|
249 |
|
250 store_met |
|
251 (prep_met Biegelinie.thy "met_biege_2" [] e_metID |
|
252 (["IntegrierenUndKonstanteBestimmen2"], |
|
253 [("#Given" ,["Traegerlaenge l_", "Streckenlast q__", |
|
254 "FunktionsVariable v_"]), |
|
255 (*("#Where",["0 < l_"]), ...wait for < and handling Arbfix*) |
|
256 ("#Find" ,["Biegelinie b_"]), |
|
257 ("#Relate",["Randbedingungen rb_"]) |
|
258 ], |
|
259 {rew_ord'="tless_true", |
|
260 rls' = append_rls "erls_IntegrierenUndK.." e_rls |
|
261 [Calc ("Atools.ident",eval_ident "#ident_"), |
|
262 Thm ("not_true",num_str not_true), |
|
263 Thm ("not_false",num_str not_false)], |
|
264 calc = [], |
|
265 srls = append_rls "erls_IntegrierenUndK.." e_rls |
|
266 [Calc("Tools.rhs", eval_rhs"eval_rhs_"), |
|
267 Calc ("Atools.ident",eval_ident "#ident_"), |
|
268 Thm ("last_thmI",num_str last_thmI), |
|
269 Thm ("if_True",num_str if_True), |
|
270 Thm ("if_False",num_str if_False) |
|
271 ], |
|
272 prls = Erls, crls = Atools_erls, nrls = Erls}, |
|
273 "Script Biegelinie2Script \ |
|
274 \(l_::real) (q__::real) (v_::real) (b_::real=>real) (rb_::bool list) = \ |
|
275 \ (let \ |
|
276 \ (funs_:: bool list) = \ |
|
277 \ (SubProblem (Biegelinie_,[vonBelastungZu,Biegelinien], \ |
|
278 \ [Biegelinien,ausBelastung]) \ |
|
279 \ [real_ q__, real_ v_]); \ |
|
280 \ (equs_::bool list) = \ |
|
281 \ (SubProblem (Biegelinie_,[setzeRandbedingungen,Biegelinien],\ |
|
282 \ [Biegelinien,setzeRandbedingungenEin]) \ |
|
283 \ [booll_ funs_, booll_ rb_]); \ |
|
284 \ (cons_::bool list) = \ |
|
285 \ (SubProblem (Biegelinie_,[linear,system],[no_met]) \ |
|
286 \ [booll_ equs_, reall [c,c_2,c_3,c_4]]); \ |
|
287 \ B_ = Take (lastI funs_); \ |
|
288 \ B_ = ((Substitute cons_) @@ \ |
|
289 \ (Rewrite_Set_Inst [(bdv, v_)] make_ratpoly_in False)) B_ \ |
|
290 \ in B_)" |
|
291 )); |
|
292 |
|
293 store_met |
|
294 (prep_met Biegelinie.thy "met_biege_intconst_2" [] e_metID |
|
295 (["IntegrierenUndKonstanteBestimmen","2xIntegrieren"], |
|
296 [], |
|
297 {rew_ord'="tless_true", rls'=Erls, calc = [], |
|
298 srls = e_rls, |
|
299 prls=e_rls, |
|
300 crls = Atools_erls, nrls = e_rls}, |
|
301 "empty_script" |
|
302 )); |
|
303 |
|
304 store_met |
|
305 (prep_met Biegelinie.thy "met_biege_intconst_4" [] e_metID |
|
306 (["IntegrierenUndKonstanteBestimmen","4x4System"], |
|
307 [], |
|
308 {rew_ord'="tless_true", rls'=Erls, calc = [], |
|
309 srls = e_rls, |
|
310 prls=e_rls, |
|
311 crls = Atools_erls, nrls = e_rls}, |
|
312 "empty_script" |
|
313 )); |
|
314 |
|
315 store_met |
|
316 (prep_met Biegelinie.thy "met_biege_intconst_1" [] e_metID |
|
317 (["IntegrierenUndKonstanteBestimmen","1xIntegrieren"], |
|
318 [], |
|
319 {rew_ord'="tless_true", rls'=Erls, calc = [], |
|
320 srls = e_rls, |
|
321 prls=e_rls, |
|
322 crls = Atools_erls, nrls = e_rls}, |
|
323 "empty_script" |
|
324 )); |
|
325 |
|
326 store_met |
|
327 (prep_met Biegelinie.thy "met_biege2" [] e_metID |
|
328 (["Biegelinien"], |
|
329 [], |
|
330 {rew_ord'="tless_true", rls'=Erls, calc = [], |
|
331 srls = e_rls, |
|
332 prls=e_rls, |
|
333 crls = Atools_erls, nrls = e_rls}, |
|
334 "empty_script" |
|
335 )); |
|
336 |
|
337 store_met |
|
338 (prep_met Biegelinie.thy "met_biege_ausbelast" [] e_metID |
|
339 (["Biegelinien","ausBelastung"], |
|
340 [("#Given" ,["Streckenlast q__","FunktionsVariable v_"]), |
|
341 ("#Find" ,["Funktionen funs_"])], |
|
342 {rew_ord'="tless_true", |
|
343 rls' = append_rls "erls_ausBelastung" e_rls |
|
344 [Calc ("Atools.ident",eval_ident "#ident_"), |
|
345 Thm ("not_true",num_str not_true), |
|
346 Thm ("not_false",num_str not_false)], |
|
347 calc = [], |
|
348 srls = append_rls "srls_ausBelastung" e_rls |
|
349 [Calc("Tools.rhs", eval_rhs"eval_rhs_")], |
|
350 prls = e_rls, crls = Atools_erls, nrls = e_rls}, |
|
351 "Script Belastung2BiegelScript (q__::real) (v_::real) = \ |
|
352 \ (let q___ = Take (q_ v_ = q__); \ |
|
353 \ q___ = ((Rewrite sym_real_minus_eq_cancel True) @@ \ |
|
354 \ (Rewrite Belastung_Querkraft True)) q___; \ |
|
355 \ (Q__:: bool) = \ |
|
356 \ (SubProblem (Biegelinie_,[named,integrate,function], \ |
|
357 \ [diff,integration,named]) \ |
|
358 \ [real_ (rhs q___), real_ v_, real_real_ Q]); \ |
|
359 \ M__ = Rewrite Querkraft_Moment True Q__; \ |
|
360 \ (M__::bool) = \ |
|
361 \ (SubProblem (Biegelinie_,[named,integrate,function], \ |
|
362 \ [diff,integration,named]) \ |
|
363 \ [real_ (rhs M__), real_ v_, real_real_ M_b]); \ |
|
364 \ N__ = ((Rewrite Moment_Neigung False) @@ \ |
|
365 \ (Rewrite make_fun_explicit False)) M__; \ |
|
366 \ (N__:: bool) = \ |
|
367 \ (SubProblem (Biegelinie_,[named,integrate,function], \ |
|
368 \ [diff,integration,named]) \ |
|
369 \ [real_ (rhs N__), real_ v_, real_real_ y']); \ |
|
370 \ (B__:: bool) = \ |
|
371 \ (SubProblem (Biegelinie_,[named,integrate,function], \ |
|
372 \ [diff,integration,named]) \ |
|
373 \ [real_ (rhs N__), real_ v_, real_real_ y]) \ |
|
374 \ in [Q__, M__, N__, B__])" |
|
375 )); |
|
376 |
|
377 store_met |
|
378 (prep_met Biegelinie.thy "met_biege_setzrand" [] e_metID |
|
379 (["Biegelinien","setzeRandbedingungenEin"], |
|
380 [("#Given" ,["Funktionen funs_","Randbedingungen rb_"]), |
|
381 ("#Find" ,["Gleichungen equs___"])], |
|
382 {rew_ord'="tless_true", rls'=Erls, calc = [], |
|
383 srls = srls2, |
|
384 prls=e_rls, |
|
385 crls = Atools_erls, nrls = e_rls}, |
|
386 "Script SetzeRandbedScript (funs_::bool list) (rb_::bool list) = \ |
|
387 \ (let b1_ = nth_ 1 rb_; \ |
|
388 \ fs_ = filter_sameFunId (lhs b1_) funs_; \ |
|
389 \ (e1_::bool) = \ |
|
390 \ (SubProblem (Biegelinie_,[makeFunctionTo,equation],\ |
|
391 \ [Equation,fromFunction]) \ |
|
392 \ [bool_ (hd fs_), bool_ b1_]); \ |
|
393 \ b2_ = nth_ 2 rb_; \ |
|
394 \ fs_ = filter_sameFunId (lhs b2_) funs_; \ |
|
395 \ (e2_::bool) = \ |
|
396 \ (SubProblem (Biegelinie_,[makeFunctionTo,equation],\ |
|
397 \ [Equation,fromFunction]) \ |
|
398 \ [bool_ (hd fs_), bool_ b2_]); \ |
|
399 \ b3_ = nth_ 3 rb_; \ |
|
400 \ fs_ = filter_sameFunId (lhs b3_) funs_; \ |
|
401 \ (e3_::bool) = \ |
|
402 \ (SubProblem (Biegelinie_,[makeFunctionTo,equation],\ |
|
403 \ [Equation,fromFunction]) \ |
|
404 \ [bool_ (hd fs_), bool_ b3_]); \ |
|
405 \ b4_ = nth_ 4 rb_; \ |
|
406 \ fs_ = filter_sameFunId (lhs b4_) funs_; \ |
|
407 \ (e4_::bool) = \ |
|
408 \ (SubProblem (Biegelinie_,[makeFunctionTo,equation],\ |
|
409 \ [Equation,fromFunction]) \ |
|
410 \ [bool_ (hd fs_), bool_ b4_]) \ |
|
411 \ in [e1_,e2_,e3_,e4_])" |
|
412 (* filter requires more than 1 sec !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!! |
|
413 "Script SetzeRandbedScript (funs_::bool list) (rb_::bool list) = \ |
|
414 \ (let b1_ = nth_ 1 rb_; \ |
|
415 \ fs_ = filter (sameFunId (lhs b1_)) funs_; \ |
|
416 \ (e1_::bool) = \ |
|
417 \ (SubProblem (Biegelinie_,[makeFunctionTo,equation],\ |
|
418 \ [Equation,fromFunction]) \ |
|
419 \ [bool_ (hd fs_), bool_ b1_]); \ |
|
420 \ b2_ = nth_ 2 rb_; \ |
|
421 \ fs_ = filter (sameFunId (lhs b2_)) funs_; \ |
|
422 \ (e2_::bool) = \ |
|
423 \ (SubProblem (Biegelinie_,[makeFunctionTo,equation],\ |
|
424 \ [Equation,fromFunction]) \ |
|
425 \ [bool_ (hd fs_), bool_ b2_]); \ |
|
426 \ b3_ = nth_ 3 rb_; \ |
|
427 \ fs_ = filter (sameFunId (lhs b3_)) funs_; \ |
|
428 \ (e3_::bool) = \ |
|
429 \ (SubProblem (Biegelinie_,[makeFunctionTo,equation],\ |
|
430 \ [Equation,fromFunction]) \ |
|
431 \ [bool_ (hd fs_), bool_ b3_]); \ |
|
432 \ b4_ = nth_ 4 rb_; \ |
|
433 \ fs_ = filter (sameFunId (lhs b4_)) funs_; \ |
|
434 \ (e4_::bool) = \ |
|
435 \ (SubProblem (Biegelinie_,[makeFunctionTo,equation],\ |
|
436 \ [Equation,fromFunction]) \ |
|
437 \ [bool_ (hd fs_), bool_ b4_]) \ |
|
438 \ in [e1_,e2_,e3_,e4_])"*) |
|
439 )); |
|
440 |
|
441 store_met |
|
442 (prep_met Biegelinie.thy "met_equ_fromfun" [] e_metID |
|
443 (["Equation","fromFunction"], |
|
444 [("#Given" ,["functionEq fun_","substitution sub_"]), |
|
445 ("#Find" ,["equality equ___"])], |
|
446 {rew_ord'="tless_true", rls'=Erls, calc = [], |
|
447 srls = append_rls "srls_in_EquationfromFunc" e_rls |
|
448 [Calc("Tools.lhs", eval_lhs"eval_lhs_"), |
|
449 Calc("Atools.argument'_in", |
|
450 eval_argument_in |
|
451 "Atools.argument'_in")], |
|
452 prls=e_rls, |
|
453 crls = Atools_erls, nrls = e_rls}, |
|
454 (*(M_b x = c_2 + c * x + -1 * q_0 / 2 * x ^^^ 2) (M_b L = 0) --> |
|
455 0 = c_2 + c * L + -1 * q_0 / 2 * L ^^^ 2*) |
|
456 "Script Function2Equality (fun_::bool) (sub_::bool) =\ |
|
457 \ (let fun_ = Take fun_; \ |
|
458 \ bdv_ = argument_in (lhs fun_); \ |
|
459 \ val_ = argument_in (lhs sub_); \ |
|
460 \ equ_ = (Substitute [bdv_ = val_]) fun_; \ |
|
461 \ equ_ = (Substitute [sub_]) fun_ \ |
|
462 \ in (Rewrite_Set norm_Rational False) equ_) " |
|
463 )); |
|
464 |
|
465 |
|
466 |
|
467 (* use"IsacKnowledge/Biegelinie.ML"; |
|
468 *) |
|