1 (* chapter 'Biegelinie' from the textbook: |
1 (* chapter 'Biegelinie' from the textbook: |
2 Timischl, Kaiser. Ingenieur-Mathematik 3. Wien 1999. p.268-271. |
2 Timischl, Kaiser. Ingenieur-Mathematik 3. Wien 1999. p.268-271. |
3 author: Walther Neuper |
3 author: Walther Neuper 050826, |
4 050826, |
|
5 (c) due to copyright terms |
4 (c) due to copyright terms |
6 *) |
5 *) |
7 |
6 |
8 theory Biegelinie imports Integrate Equation EqSystem begin |
7 theory Biegelinie imports Integrate Equation EqSystem begin |
9 |
8 |
10 consts |
9 consts |
11 |
10 |
12 q_ :: real => real ("q'_") (* Streckenlast *) |
11 q_ :: "real => real" ("q'_") (* Streckenlast *) |
13 Q :: real => real (* Querkraft *) |
12 Q :: "real => real" (* Querkraft *) |
14 Q' :: real => real (* Ableitung der Querkraft *) |
13 Q' :: "real => real" (* Ableitung der Querkraft *) |
15 M'_b :: real => real ("M'_b") (* Biegemoment *) |
14 M'_b :: "real => real" ("M'_b") (* Biegemoment *) |
16 M'_b' :: real => real ("M'_b'") (* Ableitung des Biegemoments *) |
15 M'_b' :: "real => real" ("M'_b'") (* Ableitung des Biegemoments *) |
17 y'' :: real => real (* 2.Ableitung der Biegeline *) |
16 y'' :: "real => real" (* 2.Ableitung der Biegeline *) |
18 y' :: real => real (* Neigung der Biegeline *) |
17 y' :: "real => real" (* Neigung der Biegeline *) |
19 (*y :: real => real (* Biegeline *)*) |
18 (*y :: "real => real" (* Biegeline *)*) |
20 EI :: real (* Biegesteifigkeit *) |
19 EI :: "real" (* Biegesteifigkeit *) |
21 |
20 |
22 (*new Descriptions in the related problems*) |
21 (*new Descriptions in the related problems*) |
23 Traegerlaenge :: real => una |
22 Traegerlaenge :: "real => una" |
24 Streckenlast :: real => una |
23 Streckenlast :: "real => una" |
25 BiegemomentVerlauf :: bool => una |
24 BiegemomentVerlauf :: "bool => una" |
26 Biegelinie :: (real => real) => una |
25 Biegelinie :: "(real => real) => una" |
27 Randbedingungen :: bool list => una |
26 Randbedingungen :: "bool list => una" |
28 RandbedingungenBiegung :: bool list => una |
27 RandbedingungenBiegung :: "bool list => una" |
29 RandbedingungenNeigung :: bool list => una |
28 RandbedingungenNeigung :: "bool list => una" |
30 RandbedingungenMoment :: bool list => una |
29 RandbedingungenMoment :: "bool list => una" |
31 RandbedingungenQuerkraft :: bool list => una |
30 RandbedingungenQuerkraft :: "bool list => una" |
32 FunktionsVariable :: real => una |
31 FunktionsVariable :: "real => una" |
33 Funktionen :: bool list => una |
32 Funktionen :: "bool list => una" |
34 Gleichungen :: bool list => una |
33 Gleichungen :: "bool list => una" |
35 |
34 |
36 (*Script-names*) |
35 (*Script-names*) |
37 Biegelinie2Script :: "[real,real,real,real=>real,bool list, |
36 Biegelinie2Script :: "[real,real,real,real=>real,bool list, |
38 bool] => bool" |
37 bool] => bool" |
39 ("((Script Biegelinie2Script (_ _ _ _ _ =))// (_))" 9) |
38 ("((Script Biegelinie2Script (_ _ _ _ _ =))// (_))" 9) |
79 store_isa ["IsacKnowledge"] []; |
78 store_isa ["IsacKnowledge"] []; |
80 store_thy thy |
79 store_thy thy |
81 ["Walther Neuper 2005 supported by a grant from NMI Austria"]; |
80 ["Walther Neuper 2005 supported by a grant from NMI Austria"]; |
82 store_isa ["IsacKnowledge", theory2thyID thy, "Theorems"] |
81 store_isa ["IsacKnowledge", theory2thyID thy, "Theorems"] |
83 ["Walther Neuper 2005 supported by a grant from NMI Austria"]; |
82 ["Walther Neuper 2005 supported by a grant from NMI Austria"]; |
84 store_thm thy ("Belastung_Querkraft", Belastung_Querkraft) |
83 store_thm thy ("Belastung_Querkraft", @{thm Belastung_Querkraft}) |
85 ["Walther Neuper 2005 supported by a grant from NMI Austria"]; |
84 ["Walther Neuper 2005 supported by a grant from NMI Austria"]; |
86 store_thm thy ("Moment_Neigung", Moment_Neigung) |
85 store_thm thy ("Moment_Neigung", @{thm Moment_Neigung}) |
87 ["Walther Neuper 2005 supported by a grant from NMI Austria"]; |
86 ["Walther Neuper 2005 supported by a grant from NMI Austria"]; |
88 store_thm thy ("Moment_Querkraft", Moment_Querkraft) |
87 store_thm thy ("Moment_Querkraft", @{thm Moment_Querkraft}) |
89 ["Walther Neuper 2005 supported by a grant from NMI Austria"]; |
88 ["Walther Neuper 2005 supported by a grant from NMI Austria"]; |
90 store_thm thy ("Neigung_Moment", Neigung_Moment) |
89 store_thm thy ("Neigung_Moment", @{thm Neigung_Moment}) |
91 ["Walther Neuper 2005 supported by a grant from NMI Austria"]; |
90 ["Walther Neuper 2005 supported by a grant from NMI Austria"]; |
92 store_thm thy ("Querkraft_Belastung", Querkraft_Belastung) |
91 store_thm thy ("Querkraft_Belastung", @{thm Querkraft_Belastung}) |
93 ["Walther Neuper 2005 supported by a grant from NMI Austria"]; |
92 ["Walther Neuper 2005 supported by a grant from NMI Austria"]; |
94 store_thm thy ("Querkraft_Moment", Querkraft_Moment) |
93 store_thm thy ("Querkraft_Moment", @{thm Querkraft_Moment}) |
95 ["Walther Neuper 2005 supported by a grant from NMI Austria"]; |
94 ["Walther Neuper 2005 supported by a grant from NMI Austria"]; |
96 store_thm thy ("make_fun_explicit", make_fun_explicit) |
95 store_thm thy ("make_fun_explicit", @{thm make_fun_explicit}) |
97 ["Walther Neuper 2005 supported by a grant from NMI Austria"]; |
96 ["Walther Neuper 2005 supported by a grant from NMI Austria"]; |
98 |
97 |
99 |
98 *} |
|
99 ML {* |
100 (** problems **) |
100 (** problems **) |
101 |
101 |
102 store_pbt |
102 store_pbt |
103 (prep_pbt thy "pbl_bieg" [] e_pblID |
103 (prep_pbt thy "pbl_bieg" [] e_pblID |
104 (["Biegelinien"], |
104 (["Biegelinien"], |
105 [("#Given" ,["Traegerlaenge l_", "Streckenlast q__"]), |
105 [("#Given" ,["Traegerlaenge l_l", "Streckenlast q_q"]), |
106 (*("#Where",["0 < l_"]), ...wait for < and handling Arbfix*) |
106 (*("#Where",["0 < l_l"]), ...wait for < and handling Arbfix*) |
107 ("#Find" ,["Biegelinie b_"]), |
107 ("#Find" ,["Biegelinie b_b"]), |
108 ("#Relate",["Randbedingungen rb_"]) |
108 ("#Relate",["Randbedingungen r_b"]) |
109 ], |
109 ], |
110 append_rls "e_rls" e_rls [], |
110 append_rls "e_rls" e_rls [], |
111 NONE, |
111 NONE, |
112 [["IntegrierenUndKonstanteBestimmen2"]])); |
112 [["IntegrierenUndKonstanteBestimmen2"]])); |
113 |
113 |
114 store_pbt |
114 store_pbt |
115 (prep_pbt thy "pbl_bieg_mom" [] e_pblID |
115 (prep_pbt thy "pbl_bieg_mom" [] e_pblID |
116 (["MomentBestimmte","Biegelinien"], |
116 (["MomentBestimmte","Biegelinien"], |
117 [("#Given" ,["Traegerlaenge l_", "Streckenlast q__"]), |
117 [("#Given" ,["Traegerlaenge l_l", "Streckenlast q_q"]), |
118 (*("#Where",["0 < l_"]), ...wait for < and handling Arbfix*) |
118 (*("#Where",["0 < l_l"]), ...wait for < and handling Arbfix*) |
119 ("#Find" ,["Biegelinie b_"]), |
119 ("#Find" ,["Biegelinie b_b"]), |
120 ("#Relate",["RandbedingungenBiegung rb_","RandbedingungenMoment rm_"]) |
120 ("#Relate",["RandbedingungenBiegung r_b","RandbedingungenMoment r_m"]) |
121 ], |
121 ], |
122 append_rls "e_rls" e_rls [], |
122 append_rls "e_rls" e_rls [], |
123 NONE, |
123 NONE, |
124 [["IntegrierenUndKonstanteBestimmen"]])); |
124 [["IntegrierenUndKonstanteBestimmen"]])); |
125 |
125 |
148 [["IntegrierenUndKonstanteBestimmen","1xIntegrieren"]])); |
148 [["IntegrierenUndKonstanteBestimmen","1xIntegrieren"]])); |
149 |
149 |
150 store_pbt |
150 store_pbt |
151 (prep_pbt thy "pbl_bieg_vonq" [] e_pblID |
151 (prep_pbt thy "pbl_bieg_vonq" [] e_pblID |
152 (["vonBelastungZu","Biegelinien"], |
152 (["vonBelastungZu","Biegelinien"], |
153 [("#Given" ,["Streckenlast q__","FunktionsVariable v_v"]), |
153 [("#Given" ,["Streckenlast q_q","FunktionsVariable v_v"]), |
154 ("#Find" ,["Funktionen funs___"])], |
154 ("#Find" ,["Funktionen funs'''"])], |
155 append_rls "e_rls" e_rls [], |
155 append_rls "e_rls" e_rls [], |
156 NONE, |
156 NONE, |
157 [["Biegelinien","ausBelastung"]])); |
157 [["Biegelinien","ausBelastung"]])); |
158 |
158 |
159 store_pbt |
159 store_pbt |
160 (prep_pbt thy "pbl_bieg_randbed" [] e_pblID |
160 (prep_pbt thy "pbl_bieg_randbed" [] e_pblID |
161 (["setzeRandbedingungen","Biegelinien"], |
161 (["setzeRandbedingungen","Biegelinien"], |
162 [("#Given" ,["Funktionen funs_","Randbedingungen rb_"]), |
162 [("#Given" ,["Funktionen fun_s","Randbedingungen r_b"]), |
163 ("#Find" ,["Gleichungen equs___"])], |
163 ("#Find" ,["Gleichungen equs'''"])], |
164 append_rls "e_rls" e_rls [], |
164 append_rls "e_rls" e_rls [], |
165 NONE, |
165 NONE, |
166 [["Biegelinien","setzeRandbedingungenEin"]])); |
166 [["Biegelinien","setzeRandbedingungenEin"]])); |
167 |
167 |
168 store_pbt |
168 store_pbt |
169 (prep_pbt thy "pbl_equ_fromfun" [] e_pblID |
169 (prep_pbt thy "pbl_equ_fromfun" [] e_pblID |
170 (["makeFunctionTo","equation"], |
170 (["makeFunctionTo","equation"], |
171 [("#Given" ,["functionEq fun_","substitution sub_"]), |
171 [("#Given" ,["functionEq fu_n","substitution su_b"]), |
172 ("#Find" ,["equality equ___"])], |
172 ("#Find" ,["equality equ'''"])], |
173 append_rls "e_rls" e_rls [], |
173 append_rls "e_rls" e_rls [], |
174 NONE, |
174 NONE, |
175 [["Equation","fromFunction"]])); |
175 [["Equation","fromFunction"]])); |
176 |
176 |
177 |
177 *} |
|
178 ML {* |
178 (** methods **) |
179 (** methods **) |
179 |
180 |
180 val srls = Rls {id="srls_IntegrierenUnd..", |
181 val srls = Rls {id="srls_IntegrierenUnd..", |
181 preconds = [], |
182 preconds = [], |
182 rew_ord = ("termlessI",termlessI), |
183 rew_ord = ("termlessI",termlessI), |
183 erls = append_rls "erls_in_srls_IntegrierenUnd.." e_rls |
184 erls = append_rls "erls_in_srls_IntegrierenUnd.." e_rls |
184 [(*for asm in nth_Cons_ ...*) |
185 [(*for asm in NTH_CONS ...*) |
185 Calc ("op <",eval_equ "#less_"), |
186 Calc ("op <",eval_equ "#less_"), |
186 (*2nd nth_Cons_ pushes n+-1 into asms*) |
187 (*2nd NTH_CONS pushes n+-1 into asms*) |
187 Calc("op +", eval_binop "#add_") |
188 Calc("op +", eval_binop "#add_") |
188 ], |
189 ], |
189 srls = Erls, calc = [], |
190 srls = Erls, calc = [], |
190 rules = [Thm ("nth_Cons_",num_str @{thm nth_Cons_}), |
191 rules = [Thm ("NTH_CONS",num_str @{thm NTH_CONS}), |
191 Calc("op +", eval_binop "#add_"), |
192 Calc("op +", eval_binop "#add_"), |
192 Thm ("nth_Nil_",num_str @{thm nth_Nil_}), |
193 Thm ("NTH_NIL",num_str @{thm NTH_NIL}), |
193 Calc("Tools.lhs", eval_lhs"eval_lhs_"), |
194 Calc("Tools.lhs", eval_lhs"eval_lhs_"), |
194 Calc("Tools.rhs", eval_rhs"eval_rhs_"), |
195 Calc("Tools.rhs", eval_rhs"eval_rhs_"), |
195 Calc("Atools.argument'_in", |
196 Calc("Atools.argument'_in", |
196 eval_argument_in "Atools.argument'_in") |
197 eval_argument_in "Atools.argument'_in") |
197 ], |
198 ], |
221 Thm ("if_True", num_str @{thm if_True}), |
222 Thm ("if_True", num_str @{thm if_True}), |
222 Thm ("if_False", num_str @{thm if_False}), |
223 Thm ("if_False", num_str @{thm if_False}), |
223 Thm ("hd_thm", num_str @{thm hd_thm}) |
224 Thm ("hd_thm", num_str @{thm hd_thm}) |
224 ], |
225 ], |
225 scr = EmptyScr}; |
226 scr = EmptyScr}; |
226 |
227 *} |
|
228 |
|
229 ML {* |
227 store_met |
230 store_met |
228 (prep_met thy "met_biege" [] e_metID |
231 (prep_met thy "met_biege" [] e_metID |
229 (["IntegrierenUndKonstanteBestimmen"], |
232 (["IntegrierenUndKonstanteBestimmen"], |
230 [("#Given" ,["Traegerlaenge l_", "Streckenlast q__", |
233 [("#Given" ,["Traegerlaenge l_l", "Streckenlast q_q", |
231 "FunktionsVariable v_v"]), |
234 "FunktionsVariable v_v"]), |
232 (*("#Where",["0 < l_"]), ...wait for < and handling Arbfix*) |
235 (*("#Where",["0 < l_l"]), ...wait for < and handling Arbfix*) |
233 ("#Find" ,["Biegelinie b_"]), |
236 ("#Find" ,["Biegelinie b_b"]), |
234 ("#Relate",["RandbedingungenBiegung rb_", |
237 ("#Relate",["RandbedingungenBiegung r_b", |
235 "RandbedingungenMoment rm_"]) |
238 "RandbedingungenMoment r_m"]) |
236 ], |
239 ], |
237 {rew_ord'="tless_true", |
240 {rew_ord'="tless_true", |
238 rls' = append_rls "erls_IntegrierenUndK.." e_rls |
241 rls' = append_rls "erls_IntegrierenUndK.." e_rls |
239 [Calc ("Atools.ident",eval_ident "#ident_"), |
242 [Calc ("Atools.ident",eval_ident "#ident_"), |
240 Thm ("not_true",num_str @{thm not_true}), |
243 Thm ("not_true",num_str @{thm not_true}), |
241 Thm ("not_false",num_str @{thm not_false})], |
244 Thm ("not_false",num_str @{thm not_false})], |
242 calc = [], srls = srls, prls = Erls, |
245 calc = [], srls = srls, prls = Erls, |
243 crls = Atools_erls, nrls = Erls}, |
246 crls = Atools_erls, nrls = Erls}, |
244 "Script BiegelinieScript " ^ |
247 "Script BiegelinieScript " ^ |
245 "(l_::real) (q__::real) (v_v::real) (b_::real=>real) " ^ |
248 "(l_l::real) (q__q::real) (v_v::real) (b_b::real=>real) " ^ |
246 "(rb_::bool list) (rm_::bool list) = " ^ |
249 "(r_b::bool list) (r_m::bool list) = " ^ |
247 " (let q___ = Take (q_ v_v = q__); " ^ |
250 " (let q___q = Take (q_q v_v = q__q); " ^ |
248 " q___ = ((Rewrite sym_real_minus_eq_cancel True) @@ " ^ |
251 " q___q = ((Rewrite sym_real_minus_eq_cancel True) @@ " ^ |
249 " (Rewrite Belastung_Querkraft True)) q___; " ^ |
252 " (Rewrite Belastung_Querkraft True)) q___q; " ^ |
250 " (Q__:: bool) = " ^ |
253 " (Q__Q:: bool) = " ^ |
251 " (SubProblem (Biegelinie_,[named,integrate,function], " ^ |
254 " (SubProblem (Biegelinie',[named,integrate,function], " ^ |
252 " [diff,integration,named]) " ^ |
255 " [diff,integration,named]) " ^ |
253 " [REAL (rhs q___), REAL v_v, real_REAL Q]); " ^ |
256 " [REAL (rhs q___q), REAL v_v, REAL_REAL Q]); " ^ |
254 " Q__ = Rewrite Querkraft_Moment True Q__; " ^ |
257 " Q__Q = Rewrite Querkraft_Moment True Q__Q; " ^ |
255 " (M__::bool) = " ^ |
258 " (M__M::bool) = " ^ |
256 " (SubProblem (Biegelinie_,[named,integrate,function], " ^ |
259 " (SubProblem (Biegelinie',[named,integrate,function], " ^ |
257 " [diff,integration,named]) " ^ |
260 " [diff,integration,named]) " ^ |
258 " [REAL (rhs Q__), REAL v_v, real_REAL M_b]); " ^ |
261 " [REAL (rhs Q__Q), REAL v_v, REAL_REAL M_b]); " ^ |
259 " e1__ = nth_ 1 rm_; " ^ |
262 " e__1 = NTH 1 r_m; " ^ |
260 " (x1__::real) = argument_in (lhs e1__); " ^ |
263 " (x__1::real) = argument_in (lhs e__1); " ^ |
261 " (M1__::bool) = (Substitute [v_ = x1__]) M__; " ^ |
264 " (M__1::bool) = (Substitute [v_v = x__1]) M__M; " ^ |
262 " M1__ = (Substitute [e1__]) M1__ ; " ^ |
265 " M__1 = (Substitute [e__1]) M__1 ; " ^ |
263 " M2__ = Take M__; " ^ |
266 " M__2 = Take M__M; " ^ |
264 (*without this Take 'Substitute [v_ = x2__]' takes _last formula from ctree_*) |
267 (*without this Take 'Substitute [v_v = x__2]' takes _last formula from ctree_*) |
265 " e2__ = nth_ 2 rm_; " ^ |
268 " e__2 = NTH 2 r_m; " ^ |
266 " (x2__::real) = argument_in (lhs e2__); " ^ |
269 " (x__2::real) = argument_in (lhs e__2); " ^ |
267 " (M2__::bool) = ((Substitute [v_ = x2__]) @@ " ^ |
270 " (M__2::bool) = ((Substitute [v_v = x__2]) @@ " ^ |
268 " (Substitute [e2__])) M2__; " ^ |
271 " (Substitute [e__2])) M__2; " ^ |
269 " (c_1_2__::bool list) = " ^ |
272 " (c_1_2::bool list) = " ^ |
270 " (SubProblem (Biegelinie_,[linear,system],[no_met]) " ^ |
273 " (SubProblem (Biegelinie',[linear,system],[no_met]) " ^ |
271 " [booll_ [M1__, M2__], reall [c,c_2]]); " ^ |
274 " [BOOL_LIST [M__1, M__2], REAL_LIST [c,c_2]]); " ^ |
272 " M__ = Take M__; " ^ |
275 " M__M = Take M__M; " ^ |
273 " M__ = ((Substitute c_1_2__) @@ " ^ |
276 " M__M = ((Substitute c_1_2) @@ " ^ |
274 " (Try (Rewrite_Set_Inst [(bdv_1, c),(bdv_2, c_2)]" ^ |
277 " (Try (Rewrite_Set_Inst [(bdv_1, c),(bdv_2, c_2)]" ^ |
275 " simplify_System False)) @@ " ^ |
278 " simplify_System False)) @@ " ^ |
276 " (Rewrite Moment_Neigung False) @@ " ^ |
279 " (Rewrite Moment_Neigung False) @@ " ^ |
277 " (Rewrite make_fun_explicit False)) M__; " ^ |
280 " (Rewrite make_fun_explicit False)) M__M; " ^ |
278 (*----------------------- and the same once more ------------------------*) |
281 (*----------------------- and the same once more ------------------------*) |
279 " (N__:: bool) = " ^ |
282 " (N__N:: bool) = " ^ |
280 " (SubProblem (Biegelinie_,[named,integrate,function], " ^ |
283 " (SubProblem (Biegelinie',[named,integrate,function], " ^ |
281 " [diff,integration,named]) " ^ |
284 " [diff,integration,named]) " ^ |
282 " [REAL (rhs M__), REAL v_v, real_REAL y']); " ^ |
285 " [REAL (rhs M__M), REAL v_v, REAL_REAL y']); " ^ |
283 " (B__:: bool) = " ^ |
286 " (B__B:: bool) = " ^ |
284 " (SubProblem (Biegelinie_,[named,integrate,function], " ^ |
287 " (SubProblem (Biegelinie',[named,integrate,function], " ^ |
285 " [diff,integration,named]) " ^ |
288 " [diff,integration,named]) " ^ |
286 " [REAL (rhs N__), REAL v_v, real_REAL y]); " ^ |
289 " [REAL (rhs N__N), REAL v_v, REAL_REAL y]); " ^ |
287 " e1__ = nth_ 1 rb_; " ^ |
290 " e__1 = NTH 1 r_b; " ^ |
288 " (x1__::real) = argument_in (lhs e1__); " ^ |
291 " (x__1::real) = argument_in (lhs e__1); " ^ |
289 " (B1__::bool) = (Substitute [v_ = x1__]) B__; " ^ |
292 " (B__1::bool) = (Substitute [v_v = x__1]) B__B; " ^ |
290 " B1__ = (Substitute [e1__]) B1__ ; " ^ |
293 " B__1 = (Substitute [e__1]) B__1 ; " ^ |
291 " B2__ = Take B__; " ^ |
294 " B__2 = Take B__B; " ^ |
292 " e2__ = nth_ 2 rb_; " ^ |
295 " e__2 = NTH 2 r_b; " ^ |
293 " (x2__::real) = argument_in (lhs e2__); " ^ |
296 " (x__2::real) = argument_in (lhs e__2); " ^ |
294 " (B2__::bool) = ((Substitute [v_ = x2__]) @@ " ^ |
297 " (B__2::bool) = ((Substitute [v_v = x__2]) @@ " ^ |
295 " (Substitute [e2__])) B2__; " ^ |
298 " (Substitute [e__2])) B__2; " ^ |
296 " (c_1_2__::bool list) = " ^ |
299 " (c_1_2::bool list) = " ^ |
297 " (SubProblem (Biegelinie_,[linear,system],[no_met]) " ^ |
300 " (SubProblem (Biegelinie',[linear,system],[no_met]) " ^ |
298 " [booll_ [B1__, B2__], reall [c,c_2]]); " ^ |
301 " [BOOL_LIST [B__1, B__2], REAL_LIST [c,c_2]]); " ^ |
299 " B__ = Take B__; " ^ |
302 " B__B = Take B__B; " ^ |
300 " B__ = ((Substitute c_1_2__) @@ " ^ |
303 " B__B = ((Substitute c_1_2) @@ " ^ |
301 " (Rewrite_Set_Inst [(bdv, x)] make_ratpoly_in False)) B__ " ^ |
304 " (Rewrite_Set_Inst [(bdv, x)] make_ratpoly_in False)) B__B " ^ |
302 " in B__)" |
305 " in B__B)" |
303 )); |
306 )); |
|
307 *} |
|
308 ML {* |
304 |
309 |
305 store_met |
310 store_met |
306 (prep_met thy "met_biege_2" [] e_metID |
311 (prep_met thy "met_biege_2" [] e_metID |
307 (["IntegrierenUndKonstanteBestimmen2"], |
312 (["IntegrierenUndKonstanteBestimmen2"], |
308 [("#Given" ,["Traegerlaenge l_", "Streckenlast q__", |
313 [("#Given" ,["Traegerlaenge l_l", "Streckenlast q__q", |
309 "FunktionsVariable v_v"]), |
314 "FunktionsVariable v_v"]), |
310 (*("#Where",["0 < l_"]), ...wait for < and handling Arbfix*) |
315 (*("#Where",["0 < l_l"]), ...wait for < and handling Arbfix*) |
311 ("#Find" ,["Biegelinie b_"]), |
316 ("#Find" ,["Biegelinie b_b"]), |
312 ("#Relate",["Randbedingungen rb_"]) |
317 ("#Relate",["Randbedingungen r_b"]) |
313 ], |
318 ], |
314 {rew_ord'="tless_true", |
319 {rew_ord'="tless_true", |
315 rls' = append_rls "erls_IntegrierenUndK.." e_rls |
320 rls' = append_rls "erls_IntegrierenUndK.." e_rls |
316 [Calc ("Atools.ident",eval_ident "#ident_"), |
321 [Calc ("Atools.ident",eval_ident "#ident_"), |
317 Thm ("not_true",num_str @{thm not_true}), |
322 Thm ("not_true",num_str @{thm not_true}), |
324 Thm ("if_True",num_str @{thm if_True}), |
329 Thm ("if_True",num_str @{thm if_True}), |
325 Thm ("if_False",num_str @{thm if_False}) |
330 Thm ("if_False",num_str @{thm if_False}) |
326 ], |
331 ], |
327 prls = Erls, crls = Atools_erls, nrls = Erls}, |
332 prls = Erls, crls = Atools_erls, nrls = Erls}, |
328 "Script Biegelinie2Script " ^ |
333 "Script Biegelinie2Script " ^ |
329 "(l_::real) (q__::real) (v_v::real) (b_::real=>real) (rb_::bool list) = " ^ |
334 "(l_l::real) (q__q::real) (v_v::real) (b_b::real=>real) (r_b::bool list) = " ^ |
330 " (let " ^ |
335 " (let " ^ |
331 " (funs_:: bool list) = " ^ |
336 " (fun_s:: bool list) = " ^ |
332 " (SubProblem (Biegelinie_,[vonBelastungZu,Biegelinien], " ^ |
337 " (SubProblem (Biegelinie',[vonBelastungZu,Biegelinien], " ^ |
333 " [Biegelinien,ausBelastung]) " ^ |
338 " [Biegelinien,ausBelastung]) " ^ |
334 " [REAL q__, REAL v_]); " ^ |
339 " [REAL q__q, REAL v_v]); " ^ |
335 " (equs_::bool list) = " ^ |
340 " (equ_s::bool list) = " ^ |
336 " (SubProblem (Biegelinie_,[setzeRandbedingungen,Biegelinien]," ^ |
341 " (SubProblem (Biegelinie',[setzeRandbedingungen,Biegelinien]," ^ |
337 " [Biegelinien,setzeRandbedingungenEin]) " ^ |
342 " [Biegelinien,setzeRandbedingungenEin]) " ^ |
338 " [booll_ funs_, booll_ rb_]); " ^ |
343 " [BOOL_LIST fun_s, BOOL_LIST r_b]); " ^ |
339 " (cons_::bool list) = " ^ |
344 " (con_s::bool list) = " ^ |
340 " (SubProblem (Biegelinie_,[linear,system],[no_met]) " ^ |
345 " (SubProblem (Biegelinie',[linear,system],[no_met]) " ^ |
341 " [booll_ equs_, reall [c,c_2,c_3,c_4]]); " ^ |
346 " [BOOL_LIST equ_s, REAL_LIST [c,c_2,c_3,c_4]]); " ^ |
342 " B_ = Take (lastI funs_); " ^ |
347 " B_B = Take (lastI fun_s); " ^ |
343 " B_ = ((Substitute cons_) @@ " ^ |
348 " B_B = ((Substitute con_s) @@ " ^ |
344 " (Rewrite_Set_Inst [(bdv, v_v)] make_ratpoly_in False)) B_ " ^ |
349 " (Rewrite_Set_Inst [(bdv, v_v)] make_ratpoly_in False)) B_B " ^ |
345 " in B_)" |
350 " in B_B)" |
346 )); |
351 )); |
347 |
352 |
|
353 *} |
|
354 ML {* |
348 store_met |
355 store_met |
349 (prep_met thy "met_biege_intconst_2" [] e_metID |
356 (prep_met thy "met_biege_intconst_2" [] e_metID |
350 (["IntegrierenUndKonstanteBestimmen","2xIntegrieren"], |
357 (["IntegrierenUndKonstanteBestimmen","2xIntegrieren"], |
351 [], |
358 [], |
352 {rew_ord'="tless_true", rls'=Erls, calc = [], |
359 {rew_ord'="tless_true", rls'=Erls, calc = [], |
387 prls=e_rls, |
394 prls=e_rls, |
388 crls = Atools_erls, nrls = e_rls}, |
395 crls = Atools_erls, nrls = e_rls}, |
389 "empty_script" |
396 "empty_script" |
390 )); |
397 )); |
391 |
398 |
|
399 *} |
|
400 ML {* |
392 store_met |
401 store_met |
393 (prep_met thy "met_biege_ausbelast" [] e_metID |
402 (prep_met thy "met_biege_ausbelast" [] e_metID |
394 (["Biegelinien","ausBelastung"], |
403 (["Biegelinien","ausBelastung"], |
395 [("#Given" ,["Streckenlast q__","FunktionsVariable v_v"]), |
404 [("#Given" ,["Streckenlast q__q","FunktionsVariable v_v"]), |
396 ("#Find" ,["Funktionen funs_"])], |
405 ("#Find" ,["Funktionen fun_s"])], |
397 {rew_ord'="tless_true", |
406 {rew_ord'="tless_true", |
398 rls' = append_rls "erls_ausBelastung" e_rls |
407 rls' = append_rls "erls_ausBelastung" e_rls |
399 [Calc ("Atools.ident",eval_ident "#ident_"), |
408 [Calc ("Atools.ident",eval_ident "#ident_"), |
400 Thm ("not_true",num_str @{thm not_true}), |
409 Thm ("not_true",num_str @{thm not_true}), |
401 Thm ("not_false",num_str @{thm not_false})], |
410 Thm ("not_false",num_str @{thm not_false})], |
402 calc = [], |
411 calc = [], |
403 srls = append_rls "srls_ausBelastung" e_rls |
412 srls = append_rls "srls_ausBelastung" e_rls |
404 [Calc("Tools.rhs", eval_rhs"eval_rhs_")], |
413 [Calc("Tools.rhs", eval_rhs"eval_rhs_")], |
405 prls = e_rls, crls = Atools_erls, nrls = e_rls}, |
414 prls = e_rls, crls = Atools_erls, nrls = e_rls}, |
406 "Script Belastung2BiegelScript (q__::real) (v_v::real) = " ^ |
415 "Script Belastung2BiegelScript (q__q::real) (v_v::real) = " ^ |
407 " (let q___ = Take (q_ v_v = q__); " ^ |
416 " (let q___q = Take (q_q v_v = q__q); " ^ |
408 " q___ = ((Rewrite sym_real_minus_eq_cancel True) @@ " ^ |
417 " q___q = ((Rewrite sym_real_minus_eq_cancel True) @@ " ^ |
409 " (Rewrite Belastung_Querkraft True)) q___; " ^ |
418 " (Rewrite Belastung_Querkraft True)) q___q; " ^ |
410 " (Q__:: bool) = " ^ |
419 " (Q__Q:: bool) = " ^ |
411 " (SubProblem (Biegelinie_,[named,integrate,function], " ^ |
420 " (SubProblem (Biegelinie',[named,integrate,function], " ^ |
412 " [diff,integration,named]) " ^ |
421 " [diff,integration,named]) " ^ |
413 " [REAL (rhs q___), REAL v_v, real_REAL Q]); " ^ |
422 " [REAL (rhs q___q), REAL v_v, REAL_REAL Q]); " ^ |
414 " M__ = Rewrite Querkraft_Moment True Q__; " ^ |
423 " M__M = Rewrite Querkraft_Moment True Q__Q; " ^ |
415 " (M__::bool) = " ^ |
424 " (M__M::bool) = " ^ |
416 " (SubProblem (Biegelinie_,[named,integrate,function], " ^ |
425 " (SubProblem (Biegelinie',[named,integrate,function], " ^ |
417 " [diff,integration,named]) " ^ |
426 " [diff,integration,named]) " ^ |
418 " [REAL (rhs M__), REAL v_v, real_REAL M_b]); " ^ |
427 " [REAL (rhs M__M), REAL v_v, REAL_REAL M_b]); " ^ |
419 " N__ = ((Rewrite Moment_Neigung False) @@ " ^ |
428 " N__N = ((Rewrite Moment_Neigung False) @@ " ^ |
420 " (Rewrite make_fun_explicit False)) M__; " ^ |
429 " (Rewrite make_fun_explicit False)) M__M; " ^ |
421 " (N__:: bool) = " ^ |
430 " (N__N:: bool) = " ^ |
422 " (SubProblem (Biegelinie_,[named,integrate,function], " ^ |
431 " (SubProblem (Biegelinie',[named,integrate,function], " ^ |
423 " [diff,integration,named]) " ^ |
432 " [diff,integration,named]) " ^ |
424 " [REAL (rhs N__), REAL v_v, real_REAL y']); " ^ |
433 " [REAL (rhs N__N), REAL v_v, REAL_REAL y']); " ^ |
425 " (B__:: bool) = " ^ |
434 " (B__B:: bool) = " ^ |
426 " (SubProblem (Biegelinie_,[named,integrate,function], " ^ |
435 " (SubProblem (Biegelinie',[named,integrate,function], " ^ |
427 " [diff,integration,named]) " ^ |
436 " [diff,integration,named]) " ^ |
428 " [REAL (rhs N__), REAL v_v, real_REAL y]) " ^ |
437 " [REAL (rhs N__N), REAL v_v, REAL_REAL y]) " ^ |
429 " in [Q__, M__, N__, B__])" |
438 " in [Q__Q, M__M, N__N, B__B])" |
430 )); |
439 )); |
431 |
440 |
|
441 *} |
|
442 ML {* |
432 store_met |
443 store_met |
433 (prep_met thy "met_biege_setzrand" [] e_metID |
444 (prep_met thy "met_biege_setzrand" [] e_metID |
434 (["Biegelinien","setzeRandbedingungenEin"], |
445 (["Biegelinien","setzeRandbedingungenEin"], |
435 [("#Given" ,["Funktionen funs_","Randbedingungen rb_"]), |
446 [("#Given" ,["Funktionen fun_s","Randbedingungen r_b"]), |
436 ("#Find" ,["Gleichungen equs___"])], |
447 ("#Find" ,["Gleichungen equs'''"])], |
437 {rew_ord'="tless_true", rls'=Erls, calc = [], |
448 {rew_ord'="tless_true", rls'=Erls, calc = [], |
438 srls = srls2, |
449 srls = srls2, |
439 prls=e_rls, |
450 prls=e_rls, |
440 crls = Atools_erls, nrls = e_rls}, |
451 crls = Atools_erls, nrls = e_rls}, |
441 "Script SetzeRandbedScript (funs_::bool list) (rb_::bool list) = " ^ |
452 "Script SetzeRandbedScript (fun_s::bool list) (r_b::bool list) = " ^ |
442 " (let b1_ = nth_ 1 rb_; " ^ |
453 " (let b_1 = NTH 1 r_b; " ^ |
443 " fs_ = filter_sameFunId (lhs b1_) funs_; " ^ |
454 " f_s = filter_sameFunId (lhs b_1) fun_s; " ^ |
444 " (e1_::bool) = " ^ |
455 " (e_1::bool) = " ^ |
445 " (SubProblem (Biegelinie_,[makeFunctionTo,equation]," ^ |
456 " (SubProblem (Biegelinie',[makeFunctionTo,equation]," ^ |
446 " [Equation,fromFunction]) " ^ |
457 " [Equation,fromFunction]) " ^ |
447 " [BOOL (hd fs_), BOOL b1_]); " ^ |
458 " [BOOL (hd f_s), BOOL b_1]); " ^ |
448 " b2_ = nth_ 2 rb_; " ^ |
459 " b_2 = NTH 2 r_b; " ^ |
449 " fs_ = filter_sameFunId (lhs b2_) funs_; " ^ |
460 " f_s = filter_sameFunId (lhs b_2) fun_s; " ^ |
450 " (e2_::bool) = " ^ |
461 " (e_2::bool) = " ^ |
451 " (SubProblem (Biegelinie_,[makeFunctionTo,equation]," ^ |
462 " (SubProblem (Biegelinie',[makeFunctionTo,equation]," ^ |
452 " [Equation,fromFunction]) " ^ |
463 " [Equation,fromFunction]) " ^ |
453 " [BOOL (hd fs_), BOOL b2_]); " ^ |
464 " [BOOL (hd f_s), BOOL b_2]); " ^ |
454 " b3_ = nth_ 3 rb_; " ^ |
465 " b_3 = NTH 3 r_b; " ^ |
455 " fs_ = filter_sameFunId (lhs b3_) funs_; " ^ |
466 " f_s = filter_sameFunId (lhs b_3) fun_s; " ^ |
456 " (e3_::bool) = " ^ |
467 " (e_3::bool) = " ^ |
457 " (SubProblem (Biegelinie_,[makeFunctionTo,equation]," ^ |
468 " (SubProblem (Biegelinie',[makeFunctionTo,equation]," ^ |
458 " [Equation,fromFunction]) " ^ |
469 " [Equation,fromFunction]) " ^ |
459 " [BOOL (hd fs_), BOOL b3_]); " ^ |
470 " [BOOL (hd f_s), BOOL b_3]); " ^ |
460 " b4_ = nth_ 4 rb_; " ^ |
471 " b_4 = NTH 4 r_b; " ^ |
461 " fs_ = filter_sameFunId (lhs b4_) funs_; " ^ |
472 " f_s = filter_sameFunId (lhs b_4) fun_s; " ^ |
462 " (e4_::bool) = " ^ |
473 " (e_4::bool) = " ^ |
463 " (SubProblem (Biegelinie_,[makeFunctionTo,equation]," ^ |
474 " (SubProblem (Biegelinie',[makeFunctionTo,equation]," ^ |
464 " [Equation,fromFunction]) " ^ |
475 " [Equation,fromFunction]) " ^ |
465 " [BOOL (hd fs_), BOOL b4_]) " ^ |
476 " [BOOL (hd f_s), BOOL b_4]) " ^ |
466 " in [e1_,e2_,e3_,e4_])" |
477 " in [e_1,e_2,e_3,e_4])" |
467 (* filter requires more than 1 sec !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!! |
478 (* filter requires more than 1 sec !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!! |
468 "Script SetzeRandbedScript (funs_::bool list) (rb_::bool list) = " ^ |
479 "Script SetzeRandbedScript (fun_s::bool list) (r_b::bool list) = " ^ |
469 " (let b1_ = nth_ 1 rb_; " ^ |
480 " (let b_1 = NTH 1 r_b; " ^ |
470 " fs_ = filter (sameFunId (lhs b1_)) funs_; " ^ |
481 " f_s = filter (sameFunId (lhs b_1)) fun_s; " ^ |
471 " (e1_::bool) = " ^ |
482 " (e_1::bool) = " ^ |
472 " (SubProblem (Biegelinie_,[makeFunctionTo,equation]," ^ |
483 " (SubProblem (Biegelinie',[makeFunctionTo,equation]," ^ |
473 " [Equation,fromFunction]) " ^ |
484 " [Equation,fromFunction]) " ^ |
474 " [BOOL (hd fs_), BOOL b1_]); " ^ |
485 " [BOOL (hd f_s), BOOL b_1]); " ^ |
475 " b2_ = nth_ 2 rb_; " ^ |
486 " b_2 = NTH 2 r_b; " ^ |
476 " fs_ = filter (sameFunId (lhs b2_)) funs_; " ^ |
487 " f_s = filter (sameFunId (lhs b_2)) fun_s; " ^ |
477 " (e2_::bool) = " ^ |
488 " (e_2::bool) = " ^ |
478 " (SubProblem (Biegelinie_,[makeFunctionTo,equation]," ^ |
489 " (SubProblem (Biegelinie',[makeFunctionTo,equation]," ^ |
479 " [Equation,fromFunction]) " ^ |
490 " [Equation,fromFunction]) " ^ |
480 " [BOOL (hd fs_), BOOL b2_]); " ^ |
491 " [BOOL (hd f_s), BOOL b_2]); " ^ |
481 " b3_ = nth_ 3 rb_; " ^ |
492 " b_3 = NTH 3 r_b; " ^ |
482 " fs_ = filter (sameFunId (lhs b3_)) funs_; " ^ |
493 " f_s = filter (sameFunId (lhs b_3)) fun_s; " ^ |
483 " (e3_::bool) = " ^ |
494 " (e_3::bool) = " ^ |
484 " (SubProblem (Biegelinie_,[makeFunctionTo,equation]," ^ |
495 " (SubProblem (Biegelinie',[makeFunctionTo,equation]," ^ |
485 " [Equation,fromFunction]) " ^ |
496 " [Equation,fromFunction]) " ^ |
486 " [BOOL (hd fs_), BOOL b3_]); " ^ |
497 " [BOOL (hd f_s), BOOL b_3]); " ^ |
487 " b4_ = nth_ 4 rb_; " ^ |
498 " b_4 = NTH 4 r_b; " ^ |
488 " fs_ = filter (sameFunId (lhs b4_)) funs_; " ^ |
499 " f_s = filter (sameFunId (lhs b_4)) fun_s; " ^ |
489 " (e4_::bool) = " ^ |
500 " (e_4::bool) = " ^ |
490 " (SubProblem (Biegelinie_,[makeFunctionTo,equation]," ^ |
501 " (SubProblem (Biegelinie',[makeFunctionTo,equation]," ^ |
491 " [Equation,fromFunction]) " ^ |
502 " [Equation,fromFunction]) " ^ |
492 " [BOOL (hd fs_), BOOL b4_]) " ^ |
503 " [BOOL (hd f_s), BOOL b_4]) " ^ |
493 " in [e1_,e2_,e3_,e4_])"*) |
504 " in [e_1,e_2,e_3,e_4])"*) |
494 )); |
505 )); |
495 |
506 |
|
507 *} |
|
508 ML {* |
496 store_met |
509 store_met |
497 (prep_met thy "met_equ_fromfun" [] e_metID |
510 (prep_met thy "met_equ_fromfun" [] e_metID |
498 (["Equation","fromFunction"], |
511 (["Equation","fromFunction"], |
499 [("#Given" ,["functionEq fun_","substitution sub_"]), |
512 [("#Given" ,["functionEq fu_n","substitution su_b"]), |
500 ("#Find" ,["equality equ___"])], |
513 ("#Find" ,["equality equ'''"])], |
501 {rew_ord'="tless_true", rls'=Erls, calc = [], |
514 {rew_ord'="tless_true", rls'=Erls, calc = [], |
502 srls = append_rls "srls_in_EquationfromFunc" e_rls |
515 srls = append_rls "srls_in_EquationfromFunc" e_rls |
503 [Calc("Tools.lhs", eval_lhs"eval_lhs_"), |
516 [Calc("Tools.lhs", eval_lhs"eval_lhs_"), |
504 Calc("Atools.argument'_in", |
517 Calc("Atools.argument'_in", |
505 eval_argument_in |
518 eval_argument_in |
506 "Atools.argument'_in")], |
519 "Atools.argument'_in")], |
507 prls=e_rls, |
520 prls=e_rls, crls = Atools_erls, nrls = e_rls}, |
508 crls = Atools_erls, nrls = e_rls}, |
|
509 (*(M_b x = c_2 + c * x + -1 * q_0 / 2 * x ^^^ 2) (M_b L = 0) --> |
521 (*(M_b x = c_2 + c * x + -1 * q_0 / 2 * x ^^^ 2) (M_b L = 0) --> |
510 0 = c_2 + c * L + -1 * q_0 / 2 * L ^^^ 2*) |
522 0 = c_2 + c * L + -1 * q_0 / 2 * L ^^^ 2*) |
511 "Script Function2Equality (fun_::bool) (sub_::bool) =" ^ |
523 "Script Function2Equality (fu_n::bool) (su_b::bool) =" ^ |
512 " (let fun_ = Take fun_; " ^ |
524 " (let fu_n = Take fu_n; " ^ |
513 " bdv_ = argument_in (lhs fun_); " ^ |
525 " bd_v = argument_in (lhs fu_n); " ^ |
514 " val_ = argument_in (lhs sub_); " ^ |
526 " va_l = argument_in (lhs su_b); " ^ |
515 " equ_ = (Substitute [bdv_ = val_]) fun_; " ^ |
527 " eq_u = (Substitute [bd_v = va_l]) fu_n; " ^ |
516 " equ_ = (Substitute [sub_]) fun_ " ^ |
528 " eq_u = (Substitute [su_b]) fu_n " ^ |
517 " in (Rewrite_Set norm_Rational False) equ_) " |
529 " in (Rewrite_Set norm_Rational False) eq_u) " |
518 )); |
530 )); |
519 *} |
531 *} |
520 |
532 |
521 end |
533 end |
522 |
534 |