1.1 --- a/src/Tools/isac/Knowledge/Biegelinie.thy Thu Sep 09 09:58:28 2010 +0200
1.2 +++ b/src/Tools/isac/Knowledge/Biegelinie.thy Thu Sep 09 13:31:36 2010 +0200
1.3 @@ -1,7 +1,6 @@
1.4 (* chapter 'Biegelinie' from the textbook:
1.5 Timischl, Kaiser. Ingenieur-Mathematik 3. Wien 1999. p.268-271.
1.6 - author: Walther Neuper
1.7 - 050826,
1.8 + author: Walther Neuper 050826,
1.9 (c) due to copyright terms
1.10 *)
1.11
1.12 @@ -9,29 +8,29 @@
1.13
1.14 consts
1.15
1.16 - q_ :: real => real ("q'_") (* Streckenlast *)
1.17 - Q :: real => real (* Querkraft *)
1.18 - Q' :: real => real (* Ableitung der Querkraft *)
1.19 - M'_b :: real => real ("M'_b") (* Biegemoment *)
1.20 - M'_b' :: real => real ("M'_b'") (* Ableitung des Biegemoments *)
1.21 - y'' :: real => real (* 2.Ableitung der Biegeline *)
1.22 - y' :: real => real (* Neigung der Biegeline *)
1.23 -(*y :: real => real (* Biegeline *)*)
1.24 - EI :: real (* Biegesteifigkeit *)
1.25 + q_ :: "real => real" ("q'_") (* Streckenlast *)
1.26 + Q :: "real => real" (* Querkraft *)
1.27 + Q' :: "real => real" (* Ableitung der Querkraft *)
1.28 + M'_b :: "real => real" ("M'_b") (* Biegemoment *)
1.29 + M'_b' :: "real => real" ("M'_b'") (* Ableitung des Biegemoments *)
1.30 + y'' :: "real => real" (* 2.Ableitung der Biegeline *)
1.31 + y' :: "real => real" (* Neigung der Biegeline *)
1.32 +(*y :: "real => real" (* Biegeline *)*)
1.33 + EI :: "real" (* Biegesteifigkeit *)
1.34
1.35 (*new Descriptions in the related problems*)
1.36 - Traegerlaenge :: real => una
1.37 - Streckenlast :: real => una
1.38 - BiegemomentVerlauf :: bool => una
1.39 - Biegelinie :: (real => real) => una
1.40 - Randbedingungen :: bool list => una
1.41 - RandbedingungenBiegung :: bool list => una
1.42 - RandbedingungenNeigung :: bool list => una
1.43 - RandbedingungenMoment :: bool list => una
1.44 - RandbedingungenQuerkraft :: bool list => una
1.45 - FunktionsVariable :: real => una
1.46 - Funktionen :: bool list => una
1.47 - Gleichungen :: bool list => una
1.48 + Traegerlaenge :: "real => una"
1.49 + Streckenlast :: "real => una"
1.50 + BiegemomentVerlauf :: "bool => una"
1.51 + Biegelinie :: "(real => real) => una"
1.52 + Randbedingungen :: "bool list => una"
1.53 + RandbedingungenBiegung :: "bool list => una"
1.54 + RandbedingungenNeigung :: "bool list => una"
1.55 + RandbedingungenMoment :: "bool list => una"
1.56 + RandbedingungenQuerkraft :: "bool list => una"
1.57 + FunktionsVariable :: "real => una"
1.58 + Funktionen :: "bool list => una"
1.59 + Gleichungen :: "bool list => una"
1.60
1.61 (*Script-names*)
1.62 Biegelinie2Script :: "[real,real,real,real=>real,bool list,
1.63 @@ -81,31 +80,32 @@
1.64 ["Walther Neuper 2005 supported by a grant from NMI Austria"];
1.65 store_isa ["IsacKnowledge", theory2thyID thy, "Theorems"]
1.66 ["Walther Neuper 2005 supported by a grant from NMI Austria"];
1.67 -store_thm thy ("Belastung_Querkraft", Belastung_Querkraft)
1.68 +store_thm thy ("Belastung_Querkraft", @{thm Belastung_Querkraft})
1.69 ["Walther Neuper 2005 supported by a grant from NMI Austria"];
1.70 -store_thm thy ("Moment_Neigung", Moment_Neigung)
1.71 +store_thm thy ("Moment_Neigung", @{thm Moment_Neigung})
1.72 ["Walther Neuper 2005 supported by a grant from NMI Austria"];
1.73 -store_thm thy ("Moment_Querkraft", Moment_Querkraft)
1.74 +store_thm thy ("Moment_Querkraft", @{thm Moment_Querkraft})
1.75 ["Walther Neuper 2005 supported by a grant from NMI Austria"];
1.76 -store_thm thy ("Neigung_Moment", Neigung_Moment)
1.77 +store_thm thy ("Neigung_Moment", @{thm Neigung_Moment})
1.78 ["Walther Neuper 2005 supported by a grant from NMI Austria"];
1.79 -store_thm thy ("Querkraft_Belastung", Querkraft_Belastung)
1.80 +store_thm thy ("Querkraft_Belastung", @{thm Querkraft_Belastung})
1.81 ["Walther Neuper 2005 supported by a grant from NMI Austria"];
1.82 -store_thm thy ("Querkraft_Moment", Querkraft_Moment)
1.83 +store_thm thy ("Querkraft_Moment", @{thm Querkraft_Moment})
1.84 ["Walther Neuper 2005 supported by a grant from NMI Austria"];
1.85 -store_thm thy ("make_fun_explicit", make_fun_explicit)
1.86 +store_thm thy ("make_fun_explicit", @{thm make_fun_explicit})
1.87 ["Walther Neuper 2005 supported by a grant from NMI Austria"];
1.88
1.89 -
1.90 +*}
1.91 +ML {*
1.92 (** problems **)
1.93
1.94 store_pbt
1.95 (prep_pbt thy "pbl_bieg" [] e_pblID
1.96 (["Biegelinien"],
1.97 - [("#Given" ,["Traegerlaenge l_", "Streckenlast q__"]),
1.98 - (*("#Where",["0 < l_"]), ...wait for < and handling Arbfix*)
1.99 - ("#Find" ,["Biegelinie b_"]),
1.100 - ("#Relate",["Randbedingungen rb_"])
1.101 + [("#Given" ,["Traegerlaenge l_l", "Streckenlast q_q"]),
1.102 + (*("#Where",["0 < l_l"]), ...wait for < and handling Arbfix*)
1.103 + ("#Find" ,["Biegelinie b_b"]),
1.104 + ("#Relate",["Randbedingungen r_b"])
1.105 ],
1.106 append_rls "e_rls" e_rls [],
1.107 NONE,
1.108 @@ -114,10 +114,10 @@
1.109 store_pbt
1.110 (prep_pbt thy "pbl_bieg_mom" [] e_pblID
1.111 (["MomentBestimmte","Biegelinien"],
1.112 - [("#Given" ,["Traegerlaenge l_", "Streckenlast q__"]),
1.113 - (*("#Where",["0 < l_"]), ...wait for < and handling Arbfix*)
1.114 - ("#Find" ,["Biegelinie b_"]),
1.115 - ("#Relate",["RandbedingungenBiegung rb_","RandbedingungenMoment rm_"])
1.116 + [("#Given" ,["Traegerlaenge l_l", "Streckenlast q_q"]),
1.117 + (*("#Where",["0 < l_l"]), ...wait for < and handling Arbfix*)
1.118 + ("#Find" ,["Biegelinie b_b"]),
1.119 + ("#Relate",["RandbedingungenBiegung r_b","RandbedingungenMoment r_m"])
1.120 ],
1.121 append_rls "e_rls" e_rls [],
1.122 NONE,
1.123 @@ -150,8 +150,8 @@
1.124 store_pbt
1.125 (prep_pbt thy "pbl_bieg_vonq" [] e_pblID
1.126 (["vonBelastungZu","Biegelinien"],
1.127 - [("#Given" ,["Streckenlast q__","FunktionsVariable v_v"]),
1.128 - ("#Find" ,["Funktionen funs___"])],
1.129 + [("#Given" ,["Streckenlast q_q","FunktionsVariable v_v"]),
1.130 + ("#Find" ,["Funktionen funs'''"])],
1.131 append_rls "e_rls" e_rls [],
1.132 NONE,
1.133 [["Biegelinien","ausBelastung"]]));
1.134 @@ -159,8 +159,8 @@
1.135 store_pbt
1.136 (prep_pbt thy "pbl_bieg_randbed" [] e_pblID
1.137 (["setzeRandbedingungen","Biegelinien"],
1.138 - [("#Given" ,["Funktionen funs_","Randbedingungen rb_"]),
1.139 - ("#Find" ,["Gleichungen equs___"])],
1.140 + [("#Given" ,["Funktionen fun_s","Randbedingungen r_b"]),
1.141 + ("#Find" ,["Gleichungen equs'''"])],
1.142 append_rls "e_rls" e_rls [],
1.143 NONE,
1.144 [["Biegelinien","setzeRandbedingungenEin"]]));
1.145 @@ -168,28 +168,29 @@
1.146 store_pbt
1.147 (prep_pbt thy "pbl_equ_fromfun" [] e_pblID
1.148 (["makeFunctionTo","equation"],
1.149 - [("#Given" ,["functionEq fun_","substitution sub_"]),
1.150 - ("#Find" ,["equality equ___"])],
1.151 + [("#Given" ,["functionEq fu_n","substitution su_b"]),
1.152 + ("#Find" ,["equality equ'''"])],
1.153 append_rls "e_rls" e_rls [],
1.154 NONE,
1.155 [["Equation","fromFunction"]]));
1.156
1.157 -
1.158 +*}
1.159 +ML {*
1.160 (** methods **)
1.161
1.162 val srls = Rls {id="srls_IntegrierenUnd..",
1.163 preconds = [],
1.164 rew_ord = ("termlessI",termlessI),
1.165 erls = append_rls "erls_in_srls_IntegrierenUnd.." e_rls
1.166 - [(*for asm in nth_Cons_ ...*)
1.167 + [(*for asm in NTH_CONS ...*)
1.168 Calc ("op <",eval_equ "#less_"),
1.169 - (*2nd nth_Cons_ pushes n+-1 into asms*)
1.170 + (*2nd NTH_CONS pushes n+-1 into asms*)
1.171 Calc("op +", eval_binop "#add_")
1.172 ],
1.173 srls = Erls, calc = [],
1.174 - rules = [Thm ("nth_Cons_",num_str @{thm nth_Cons_}),
1.175 + rules = [Thm ("NTH_CONS",num_str @{thm NTH_CONS}),
1.176 Calc("op +", eval_binop "#add_"),
1.177 - Thm ("nth_Nil_",num_str @{thm nth_Nil_}),
1.178 + Thm ("NTH_NIL",num_str @{thm NTH_NIL}),
1.179 Calc("Tools.lhs", eval_lhs"eval_lhs_"),
1.180 Calc("Tools.rhs", eval_rhs"eval_rhs_"),
1.181 Calc("Atools.argument'_in",
1.182 @@ -202,15 +203,15 @@
1.183 preconds = [],
1.184 rew_ord = ("termlessI",termlessI),
1.185 erls = append_rls "erls_in_srls_IntegrierenUnd.." e_rls
1.186 - [(*for asm in nth_Cons_ ...*)
1.187 + [(*for asm in NTH_CONS ...*)
1.188 Calc ("op <",eval_equ "#less_"),
1.189 - (*2nd nth_Cons_ pushes n+-1 into asms*)
1.190 + (*2nd NTH_CONS pushes n+-1 into asms*)
1.191 Calc("op +", eval_binop "#add_")
1.192 ],
1.193 srls = Erls, calc = [],
1.194 - rules = [Thm ("nth_Cons_",num_str @{thm nth_Cons_}),
1.195 + rules = [Thm ("NTH_CONS",num_str @{thm NTH_CONS}),
1.196 Calc("op +", eval_binop "#add_"),
1.197 - Thm ("nth_Nil_", num_str @{thm nth_Nil_}),
1.198 + Thm ("NTH_NIL", num_str @{thm NTH_NIL}),
1.199 Calc("Tools.lhs", eval_lhs "eval_lhs_"),
1.200 Calc("Atools.filter'_sameFunId",
1.201 eval_filter_sameFunId "Atools.filter'_sameFunId"),
1.202 @@ -223,16 +224,18 @@
1.203 Thm ("hd_thm", num_str @{thm hd_thm})
1.204 ],
1.205 scr = EmptyScr};
1.206 -
1.207 +*}
1.208 +
1.209 +ML {*
1.210 store_met
1.211 (prep_met thy "met_biege" [] e_metID
1.212 (["IntegrierenUndKonstanteBestimmen"],
1.213 - [("#Given" ,["Traegerlaenge l_", "Streckenlast q__",
1.214 + [("#Given" ,["Traegerlaenge l_l", "Streckenlast q_q",
1.215 "FunktionsVariable v_v"]),
1.216 - (*("#Where",["0 < l_"]), ...wait for < and handling Arbfix*)
1.217 - ("#Find" ,["Biegelinie b_"]),
1.218 - ("#Relate",["RandbedingungenBiegung rb_",
1.219 - "RandbedingungenMoment rm_"])
1.220 + (*("#Where",["0 < l_l"]), ...wait for < and handling Arbfix*)
1.221 + ("#Find" ,["Biegelinie b_b"]),
1.222 + ("#Relate",["RandbedingungenBiegung r_b",
1.223 + "RandbedingungenMoment r_m"])
1.224 ],
1.225 {rew_ord'="tless_true",
1.226 rls' = append_rls "erls_IntegrierenUndK.." e_rls
1.227 @@ -242,74 +245,76 @@
1.228 calc = [], srls = srls, prls = Erls,
1.229 crls = Atools_erls, nrls = Erls},
1.230 "Script BiegelinieScript " ^
1.231 -"(l_::real) (q__::real) (v_v::real) (b_::real=>real) " ^
1.232 -"(rb_::bool list) (rm_::bool list) = " ^
1.233 -" (let q___ = Take (q_ v_v = q__); " ^
1.234 -" q___ = ((Rewrite sym_real_minus_eq_cancel True) @@ " ^
1.235 -" (Rewrite Belastung_Querkraft True)) q___; " ^
1.236 -" (Q__:: bool) = " ^
1.237 -" (SubProblem (Biegelinie_,[named,integrate,function], " ^
1.238 +"(l_l::real) (q__q::real) (v_v::real) (b_b::real=>real) " ^
1.239 +"(r_b::bool list) (r_m::bool list) = " ^
1.240 +" (let q___q = Take (q_q v_v = q__q); " ^
1.241 +" q___q = ((Rewrite sym_real_minus_eq_cancel True) @@ " ^
1.242 +" (Rewrite Belastung_Querkraft True)) q___q; " ^
1.243 +" (Q__Q:: bool) = " ^
1.244 +" (SubProblem (Biegelinie',[named,integrate,function], " ^
1.245 " [diff,integration,named]) " ^
1.246 -" [REAL (rhs q___), REAL v_v, real_REAL Q]); " ^
1.247 -" Q__ = Rewrite Querkraft_Moment True Q__; " ^
1.248 -" (M__::bool) = " ^
1.249 -" (SubProblem (Biegelinie_,[named,integrate,function], " ^
1.250 +" [REAL (rhs q___q), REAL v_v, REAL_REAL Q]); " ^
1.251 +" Q__Q = Rewrite Querkraft_Moment True Q__Q; " ^
1.252 +" (M__M::bool) = " ^
1.253 +" (SubProblem (Biegelinie',[named,integrate,function], " ^
1.254 " [diff,integration,named]) " ^
1.255 -" [REAL (rhs Q__), REAL v_v, real_REAL M_b]); " ^
1.256 -" e1__ = nth_ 1 rm_; " ^
1.257 -" (x1__::real) = argument_in (lhs e1__); " ^
1.258 -" (M1__::bool) = (Substitute [v_ = x1__]) M__; " ^
1.259 -" M1__ = (Substitute [e1__]) M1__ ; " ^
1.260 -" M2__ = Take M__; " ^
1.261 -(*without this Take 'Substitute [v_ = x2__]' takes _last formula from ctree_*)
1.262 -" e2__ = nth_ 2 rm_; " ^
1.263 -" (x2__::real) = argument_in (lhs e2__); " ^
1.264 -" (M2__::bool) = ((Substitute [v_ = x2__]) @@ " ^
1.265 -" (Substitute [e2__])) M2__; " ^
1.266 -" (c_1_2__::bool list) = " ^
1.267 -" (SubProblem (Biegelinie_,[linear,system],[no_met]) " ^
1.268 -" [booll_ [M1__, M2__], reall [c,c_2]]); " ^
1.269 -" M__ = Take M__; " ^
1.270 -" M__ = ((Substitute c_1_2__) @@ " ^
1.271 +" [REAL (rhs Q__Q), REAL v_v, REAL_REAL M_b]); " ^
1.272 +" e__1 = NTH 1 r_m; " ^
1.273 +" (x__1::real) = argument_in (lhs e__1); " ^
1.274 +" (M__1::bool) = (Substitute [v_v = x__1]) M__M; " ^
1.275 +" M__1 = (Substitute [e__1]) M__1 ; " ^
1.276 +" M__2 = Take M__M; " ^
1.277 +(*without this Take 'Substitute [v_v = x__2]' takes _last formula from ctree_*)
1.278 +" e__2 = NTH 2 r_m; " ^
1.279 +" (x__2::real) = argument_in (lhs e__2); " ^
1.280 +" (M__2::bool) = ((Substitute [v_v = x__2]) @@ " ^
1.281 +" (Substitute [e__2])) M__2; " ^
1.282 +" (c_1_2::bool list) = " ^
1.283 +" (SubProblem (Biegelinie',[linear,system],[no_met]) " ^
1.284 +" [BOOL_LIST [M__1, M__2], REAL_LIST [c,c_2]]); " ^
1.285 +" M__M = Take M__M; " ^
1.286 +" M__M = ((Substitute c_1_2) @@ " ^
1.287 " (Try (Rewrite_Set_Inst [(bdv_1, c),(bdv_2, c_2)]" ^
1.288 " simplify_System False)) @@ " ^
1.289 " (Rewrite Moment_Neigung False) @@ " ^
1.290 -" (Rewrite make_fun_explicit False)) M__; " ^
1.291 +" (Rewrite make_fun_explicit False)) M__M; " ^
1.292 (*----------------------- and the same once more ------------------------*)
1.293 -" (N__:: bool) = " ^
1.294 -" (SubProblem (Biegelinie_,[named,integrate,function], " ^
1.295 +" (N__N:: bool) = " ^
1.296 +" (SubProblem (Biegelinie',[named,integrate,function], " ^
1.297 " [diff,integration,named]) " ^
1.298 -" [REAL (rhs M__), REAL v_v, real_REAL y']); " ^
1.299 -" (B__:: bool) = " ^
1.300 -" (SubProblem (Biegelinie_,[named,integrate,function], " ^
1.301 +" [REAL (rhs M__M), REAL v_v, REAL_REAL y']); " ^
1.302 +" (B__B:: bool) = " ^
1.303 +" (SubProblem (Biegelinie',[named,integrate,function], " ^
1.304 " [diff,integration,named]) " ^
1.305 -" [REAL (rhs N__), REAL v_v, real_REAL y]); " ^
1.306 -" e1__ = nth_ 1 rb_; " ^
1.307 -" (x1__::real) = argument_in (lhs e1__); " ^
1.308 -" (B1__::bool) = (Substitute [v_ = x1__]) B__; " ^
1.309 -" B1__ = (Substitute [e1__]) B1__ ; " ^
1.310 -" B2__ = Take B__; " ^
1.311 -" e2__ = nth_ 2 rb_; " ^
1.312 -" (x2__::real) = argument_in (lhs e2__); " ^
1.313 -" (B2__::bool) = ((Substitute [v_ = x2__]) @@ " ^
1.314 -" (Substitute [e2__])) B2__; " ^
1.315 -" (c_1_2__::bool list) = " ^
1.316 -" (SubProblem (Biegelinie_,[linear,system],[no_met]) " ^
1.317 -" [booll_ [B1__, B2__], reall [c,c_2]]); " ^
1.318 -" B__ = Take B__; " ^
1.319 -" B__ = ((Substitute c_1_2__) @@ " ^
1.320 -" (Rewrite_Set_Inst [(bdv, x)] make_ratpoly_in False)) B__ " ^
1.321 -" in B__)"
1.322 +" [REAL (rhs N__N), REAL v_v, REAL_REAL y]); " ^
1.323 +" e__1 = NTH 1 r_b; " ^
1.324 +" (x__1::real) = argument_in (lhs e__1); " ^
1.325 +" (B__1::bool) = (Substitute [v_v = x__1]) B__B; " ^
1.326 +" B__1 = (Substitute [e__1]) B__1 ; " ^
1.327 +" B__2 = Take B__B; " ^
1.328 +" e__2 = NTH 2 r_b; " ^
1.329 +" (x__2::real) = argument_in (lhs e__2); " ^
1.330 +" (B__2::bool) = ((Substitute [v_v = x__2]) @@ " ^
1.331 +" (Substitute [e__2])) B__2; " ^
1.332 +" (c_1_2::bool list) = " ^
1.333 +" (SubProblem (Biegelinie',[linear,system],[no_met]) " ^
1.334 +" [BOOL_LIST [B__1, B__2], REAL_LIST [c,c_2]]); " ^
1.335 +" B__B = Take B__B; " ^
1.336 +" B__B = ((Substitute c_1_2) @@ " ^
1.337 +" (Rewrite_Set_Inst [(bdv, x)] make_ratpoly_in False)) B__B " ^
1.338 +" in B__B)"
1.339 ));
1.340 +*}
1.341 +ML {*
1.342
1.343 store_met
1.344 (prep_met thy "met_biege_2" [] e_metID
1.345 (["IntegrierenUndKonstanteBestimmen2"],
1.346 - [("#Given" ,["Traegerlaenge l_", "Streckenlast q__",
1.347 + [("#Given" ,["Traegerlaenge l_l", "Streckenlast q__q",
1.348 "FunktionsVariable v_v"]),
1.349 - (*("#Where",["0 < l_"]), ...wait for < and handling Arbfix*)
1.350 - ("#Find" ,["Biegelinie b_"]),
1.351 - ("#Relate",["Randbedingungen rb_"])
1.352 + (*("#Where",["0 < l_l"]), ...wait for < and handling Arbfix*)
1.353 + ("#Find" ,["Biegelinie b_b"]),
1.354 + ("#Relate",["Randbedingungen r_b"])
1.355 ],
1.356 {rew_ord'="tless_true",
1.357 rls' = append_rls "erls_IntegrierenUndK.." e_rls
1.358 @@ -326,25 +331,27 @@
1.359 ],
1.360 prls = Erls, crls = Atools_erls, nrls = Erls},
1.361 "Script Biegelinie2Script " ^
1.362 -"(l_::real) (q__::real) (v_v::real) (b_::real=>real) (rb_::bool list) = " ^
1.363 +"(l_l::real) (q__q::real) (v_v::real) (b_b::real=>real) (r_b::bool list) = " ^
1.364 " (let " ^
1.365 -" (funs_:: bool list) = " ^
1.366 -" (SubProblem (Biegelinie_,[vonBelastungZu,Biegelinien], " ^
1.367 +" (fun_s:: bool list) = " ^
1.368 +" (SubProblem (Biegelinie',[vonBelastungZu,Biegelinien], " ^
1.369 " [Biegelinien,ausBelastung]) " ^
1.370 -" [REAL q__, REAL v_]); " ^
1.371 -" (equs_::bool list) = " ^
1.372 -" (SubProblem (Biegelinie_,[setzeRandbedingungen,Biegelinien]," ^
1.373 +" [REAL q__q, REAL v_v]); " ^
1.374 +" (equ_s::bool list) = " ^
1.375 +" (SubProblem (Biegelinie',[setzeRandbedingungen,Biegelinien]," ^
1.376 " [Biegelinien,setzeRandbedingungenEin]) " ^
1.377 -" [booll_ funs_, booll_ rb_]); " ^
1.378 -" (cons_::bool list) = " ^
1.379 -" (SubProblem (Biegelinie_,[linear,system],[no_met]) " ^
1.380 -" [booll_ equs_, reall [c,c_2,c_3,c_4]]); " ^
1.381 -" B_ = Take (lastI funs_); " ^
1.382 -" B_ = ((Substitute cons_) @@ " ^
1.383 -" (Rewrite_Set_Inst [(bdv, v_v)] make_ratpoly_in False)) B_ " ^
1.384 -" in B_)"
1.385 +" [BOOL_LIST fun_s, BOOL_LIST r_b]); " ^
1.386 +" (con_s::bool list) = " ^
1.387 +" (SubProblem (Biegelinie',[linear,system],[no_met]) " ^
1.388 +" [BOOL_LIST equ_s, REAL_LIST [c,c_2,c_3,c_4]]); " ^
1.389 +" B_B = Take (lastI fun_s); " ^
1.390 +" B_B = ((Substitute con_s) @@ " ^
1.391 +" (Rewrite_Set_Inst [(bdv, v_v)] make_ratpoly_in False)) B_B " ^
1.392 +" in B_B)"
1.393 ));
1.394
1.395 +*}
1.396 +ML {*
1.397 store_met
1.398 (prep_met thy "met_biege_intconst_2" [] e_metID
1.399 (["IntegrierenUndKonstanteBestimmen","2xIntegrieren"],
1.400 @@ -389,11 +396,13 @@
1.401 "empty_script"
1.402 ));
1.403
1.404 +*}
1.405 +ML {*
1.406 store_met
1.407 (prep_met thy "met_biege_ausbelast" [] e_metID
1.408 (["Biegelinien","ausBelastung"],
1.409 - [("#Given" ,["Streckenlast q__","FunktionsVariable v_v"]),
1.410 - ("#Find" ,["Funktionen funs_"])],
1.411 + [("#Given" ,["Streckenlast q__q","FunktionsVariable v_v"]),
1.412 + ("#Find" ,["Funktionen fun_s"])],
1.413 {rew_ord'="tless_true",
1.414 rls' = append_rls "erls_ausBelastung" e_rls
1.415 [Calc ("Atools.ident",eval_ident "#ident_"),
1.416 @@ -403,118 +412,121 @@
1.417 srls = append_rls "srls_ausBelastung" e_rls
1.418 [Calc("Tools.rhs", eval_rhs"eval_rhs_")],
1.419 prls = e_rls, crls = Atools_erls, nrls = e_rls},
1.420 -"Script Belastung2BiegelScript (q__::real) (v_v::real) = " ^
1.421 -" (let q___ = Take (q_ v_v = q__); " ^
1.422 -" q___ = ((Rewrite sym_real_minus_eq_cancel True) @@ " ^
1.423 -" (Rewrite Belastung_Querkraft True)) q___; " ^
1.424 -" (Q__:: bool) = " ^
1.425 -" (SubProblem (Biegelinie_,[named,integrate,function], " ^
1.426 +"Script Belastung2BiegelScript (q__q::real) (v_v::real) = " ^
1.427 +" (let q___q = Take (q_q v_v = q__q); " ^
1.428 +" q___q = ((Rewrite sym_real_minus_eq_cancel True) @@ " ^
1.429 +" (Rewrite Belastung_Querkraft True)) q___q; " ^
1.430 +" (Q__Q:: bool) = " ^
1.431 +" (SubProblem (Biegelinie',[named,integrate,function], " ^
1.432 " [diff,integration,named]) " ^
1.433 -" [REAL (rhs q___), REAL v_v, real_REAL Q]); " ^
1.434 -" M__ = Rewrite Querkraft_Moment True Q__; " ^
1.435 -" (M__::bool) = " ^
1.436 -" (SubProblem (Biegelinie_,[named,integrate,function], " ^
1.437 +" [REAL (rhs q___q), REAL v_v, REAL_REAL Q]); " ^
1.438 +" M__M = Rewrite Querkraft_Moment True Q__Q; " ^
1.439 +" (M__M::bool) = " ^
1.440 +" (SubProblem (Biegelinie',[named,integrate,function], " ^
1.441 " [diff,integration,named]) " ^
1.442 -" [REAL (rhs M__), REAL v_v, real_REAL M_b]); " ^
1.443 -" N__ = ((Rewrite Moment_Neigung False) @@ " ^
1.444 -" (Rewrite make_fun_explicit False)) M__; " ^
1.445 -" (N__:: bool) = " ^
1.446 -" (SubProblem (Biegelinie_,[named,integrate,function], " ^
1.447 +" [REAL (rhs M__M), REAL v_v, REAL_REAL M_b]); " ^
1.448 +" N__N = ((Rewrite Moment_Neigung False) @@ " ^
1.449 +" (Rewrite make_fun_explicit False)) M__M; " ^
1.450 +" (N__N:: bool) = " ^
1.451 +" (SubProblem (Biegelinie',[named,integrate,function], " ^
1.452 " [diff,integration,named]) " ^
1.453 -" [REAL (rhs N__), REAL v_v, real_REAL y']); " ^
1.454 -" (B__:: bool) = " ^
1.455 -" (SubProblem (Biegelinie_,[named,integrate,function], " ^
1.456 +" [REAL (rhs N__N), REAL v_v, REAL_REAL y']); " ^
1.457 +" (B__B:: bool) = " ^
1.458 +" (SubProblem (Biegelinie',[named,integrate,function], " ^
1.459 " [diff,integration,named]) " ^
1.460 -" [REAL (rhs N__), REAL v_v, real_REAL y]) " ^
1.461 -" in [Q__, M__, N__, B__])"
1.462 +" [REAL (rhs N__N), REAL v_v, REAL_REAL y]) " ^
1.463 +" in [Q__Q, M__M, N__N, B__B])"
1.464 ));
1.465
1.466 +*}
1.467 +ML {*
1.468 store_met
1.469 (prep_met thy "met_biege_setzrand" [] e_metID
1.470 (["Biegelinien","setzeRandbedingungenEin"],
1.471 - [("#Given" ,["Funktionen funs_","Randbedingungen rb_"]),
1.472 - ("#Find" ,["Gleichungen equs___"])],
1.473 + [("#Given" ,["Funktionen fun_s","Randbedingungen r_b"]),
1.474 + ("#Find" ,["Gleichungen equs'''"])],
1.475 {rew_ord'="tless_true", rls'=Erls, calc = [],
1.476 srls = srls2,
1.477 prls=e_rls,
1.478 crls = Atools_erls, nrls = e_rls},
1.479 -"Script SetzeRandbedScript (funs_::bool list) (rb_::bool list) = " ^
1.480 -" (let b1_ = nth_ 1 rb_; " ^
1.481 -" fs_ = filter_sameFunId (lhs b1_) funs_; " ^
1.482 -" (e1_::bool) = " ^
1.483 -" (SubProblem (Biegelinie_,[makeFunctionTo,equation]," ^
1.484 +"Script SetzeRandbedScript (fun_s::bool list) (r_b::bool list) = " ^
1.485 +" (let b_1 = NTH 1 r_b; " ^
1.486 +" f_s = filter_sameFunId (lhs b_1) fun_s; " ^
1.487 +" (e_1::bool) = " ^
1.488 +" (SubProblem (Biegelinie',[makeFunctionTo,equation]," ^
1.489 " [Equation,fromFunction]) " ^
1.490 -" [BOOL (hd fs_), BOOL b1_]); " ^
1.491 -" b2_ = nth_ 2 rb_; " ^
1.492 -" fs_ = filter_sameFunId (lhs b2_) funs_; " ^
1.493 -" (e2_::bool) = " ^
1.494 -" (SubProblem (Biegelinie_,[makeFunctionTo,equation]," ^
1.495 +" [BOOL (hd f_s), BOOL b_1]); " ^
1.496 +" b_2 = NTH 2 r_b; " ^
1.497 +" f_s = filter_sameFunId (lhs b_2) fun_s; " ^
1.498 +" (e_2::bool) = " ^
1.499 +" (SubProblem (Biegelinie',[makeFunctionTo,equation]," ^
1.500 " [Equation,fromFunction]) " ^
1.501 -" [BOOL (hd fs_), BOOL b2_]); " ^
1.502 -" b3_ = nth_ 3 rb_; " ^
1.503 -" fs_ = filter_sameFunId (lhs b3_) funs_; " ^
1.504 -" (e3_::bool) = " ^
1.505 -" (SubProblem (Biegelinie_,[makeFunctionTo,equation]," ^
1.506 +" [BOOL (hd f_s), BOOL b_2]); " ^
1.507 +" b_3 = NTH 3 r_b; " ^
1.508 +" f_s = filter_sameFunId (lhs b_3) fun_s; " ^
1.509 +" (e_3::bool) = " ^
1.510 +" (SubProblem (Biegelinie',[makeFunctionTo,equation]," ^
1.511 " [Equation,fromFunction]) " ^
1.512 -" [BOOL (hd fs_), BOOL b3_]); " ^
1.513 -" b4_ = nth_ 4 rb_; " ^
1.514 -" fs_ = filter_sameFunId (lhs b4_) funs_; " ^
1.515 -" (e4_::bool) = " ^
1.516 -" (SubProblem (Biegelinie_,[makeFunctionTo,equation]," ^
1.517 +" [BOOL (hd f_s), BOOL b_3]); " ^
1.518 +" b_4 = NTH 4 r_b; " ^
1.519 +" f_s = filter_sameFunId (lhs b_4) fun_s; " ^
1.520 +" (e_4::bool) = " ^
1.521 +" (SubProblem (Biegelinie',[makeFunctionTo,equation]," ^
1.522 " [Equation,fromFunction]) " ^
1.523 -" [BOOL (hd fs_), BOOL b4_]) " ^
1.524 -" in [e1_,e2_,e3_,e4_])"
1.525 +" [BOOL (hd f_s), BOOL b_4]) " ^
1.526 +" in [e_1,e_2,e_3,e_4])"
1.527 (* filter requires more than 1 sec !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!
1.528 -"Script SetzeRandbedScript (funs_::bool list) (rb_::bool list) = " ^
1.529 -" (let b1_ = nth_ 1 rb_; " ^
1.530 -" fs_ = filter (sameFunId (lhs b1_)) funs_; " ^
1.531 -" (e1_::bool) = " ^
1.532 -" (SubProblem (Biegelinie_,[makeFunctionTo,equation]," ^
1.533 +"Script SetzeRandbedScript (fun_s::bool list) (r_b::bool list) = " ^
1.534 +" (let b_1 = NTH 1 r_b; " ^
1.535 +" f_s = filter (sameFunId (lhs b_1)) fun_s; " ^
1.536 +" (e_1::bool) = " ^
1.537 +" (SubProblem (Biegelinie',[makeFunctionTo,equation]," ^
1.538 " [Equation,fromFunction]) " ^
1.539 -" [BOOL (hd fs_), BOOL b1_]); " ^
1.540 -" b2_ = nth_ 2 rb_; " ^
1.541 -" fs_ = filter (sameFunId (lhs b2_)) funs_; " ^
1.542 -" (e2_::bool) = " ^
1.543 -" (SubProblem (Biegelinie_,[makeFunctionTo,equation]," ^
1.544 +" [BOOL (hd f_s), BOOL b_1]); " ^
1.545 +" b_2 = NTH 2 r_b; " ^
1.546 +" f_s = filter (sameFunId (lhs b_2)) fun_s; " ^
1.547 +" (e_2::bool) = " ^
1.548 +" (SubProblem (Biegelinie',[makeFunctionTo,equation]," ^
1.549 " [Equation,fromFunction]) " ^
1.550 -" [BOOL (hd fs_), BOOL b2_]); " ^
1.551 -" b3_ = nth_ 3 rb_; " ^
1.552 -" fs_ = filter (sameFunId (lhs b3_)) funs_; " ^
1.553 -" (e3_::bool) = " ^
1.554 -" (SubProblem (Biegelinie_,[makeFunctionTo,equation]," ^
1.555 +" [BOOL (hd f_s), BOOL b_2]); " ^
1.556 +" b_3 = NTH 3 r_b; " ^
1.557 +" f_s = filter (sameFunId (lhs b_3)) fun_s; " ^
1.558 +" (e_3::bool) = " ^
1.559 +" (SubProblem (Biegelinie',[makeFunctionTo,equation]," ^
1.560 " [Equation,fromFunction]) " ^
1.561 -" [BOOL (hd fs_), BOOL b3_]); " ^
1.562 -" b4_ = nth_ 4 rb_; " ^
1.563 -" fs_ = filter (sameFunId (lhs b4_)) funs_; " ^
1.564 -" (e4_::bool) = " ^
1.565 -" (SubProblem (Biegelinie_,[makeFunctionTo,equation]," ^
1.566 +" [BOOL (hd f_s), BOOL b_3]); " ^
1.567 +" b_4 = NTH 4 r_b; " ^
1.568 +" f_s = filter (sameFunId (lhs b_4)) fun_s; " ^
1.569 +" (e_4::bool) = " ^
1.570 +" (SubProblem (Biegelinie',[makeFunctionTo,equation]," ^
1.571 " [Equation,fromFunction]) " ^
1.572 -" [BOOL (hd fs_), BOOL b4_]) " ^
1.573 -" in [e1_,e2_,e3_,e4_])"*)
1.574 +" [BOOL (hd f_s), BOOL b_4]) " ^
1.575 +" in [e_1,e_2,e_3,e_4])"*)
1.576 ));
1.577
1.578 +*}
1.579 +ML {*
1.580 store_met
1.581 (prep_met thy "met_equ_fromfun" [] e_metID
1.582 (["Equation","fromFunction"],
1.583 - [("#Given" ,["functionEq fun_","substitution sub_"]),
1.584 - ("#Find" ,["equality equ___"])],
1.585 + [("#Given" ,["functionEq fu_n","substitution su_b"]),
1.586 + ("#Find" ,["equality equ'''"])],
1.587 {rew_ord'="tless_true", rls'=Erls, calc = [],
1.588 srls = append_rls "srls_in_EquationfromFunc" e_rls
1.589 [Calc("Tools.lhs", eval_lhs"eval_lhs_"),
1.590 Calc("Atools.argument'_in",
1.591 eval_argument_in
1.592 "Atools.argument'_in")],
1.593 - prls=e_rls,
1.594 - crls = Atools_erls, nrls = e_rls},
1.595 + prls=e_rls, crls = Atools_erls, nrls = e_rls},
1.596 (*(M_b x = c_2 + c * x + -1 * q_0 / 2 * x ^^^ 2) (M_b L = 0) -->
1.597 0 = c_2 + c * L + -1 * q_0 / 2 * L ^^^ 2*)
1.598 -"Script Function2Equality (fun_::bool) (sub_::bool) =" ^
1.599 -" (let fun_ = Take fun_; " ^
1.600 -" bdv_ = argument_in (lhs fun_); " ^
1.601 -" val_ = argument_in (lhs sub_); " ^
1.602 -" equ_ = (Substitute [bdv_ = val_]) fun_; " ^
1.603 -" equ_ = (Substitute [sub_]) fun_ " ^
1.604 -" in (Rewrite_Set norm_Rational False) equ_) "
1.605 +"Script Function2Equality (fu_n::bool) (su_b::bool) =" ^
1.606 +" (let fu_n = Take fu_n; " ^
1.607 +" bd_v = argument_in (lhs fu_n); " ^
1.608 +" va_l = argument_in (lhs su_b); " ^
1.609 +" eq_u = (Substitute [bd_v = va_l]) fu_n; " ^
1.610 +" eq_u = (Substitute [su_b]) fu_n " ^
1.611 +" in (Rewrite_Set norm_Rational False) eq_u) "
1.612 ));
1.613 *}
1.614