1.1 --- a/src/Tools/isac/Knowledge/Atools.thy Thu Sep 09 09:58:28 2010 +0200
1.2 +++ b/src/Tools/isac/Knowledge/Atools.thy Thu Sep 09 13:31:36 2010 +0200
1.3 @@ -11,7 +11,8 @@
1.4 ("Interpret/generate.sml")("Interpret/calchead.sml")("Interpret/appl.sml")
1.5 ("Interpret/rewtools.sml")("Interpret/script.sml")("Interpret/solve.sml")
1.6 ("Interpret/inform.sml")("Interpret/mathengine.sml")
1.7 -
1.8 +("xmlsrc/mathml.sml")("xmlsrc/datatypes.sml")("xmlsrc/pbl-met-hierarchy.sml")
1.9 +("xmlsrc/thy-hierarchy.sml")("xmlsrc/interface-xml.sml")
1.10 begin
1.11 use "Interpret/mstools.sml"
1.12 use "Interpret/ctree.sml"
1.13 @@ -25,6 +26,12 @@
1.14 use "Interpret/inform.sml" (*^^^ need files for: fun castab*)
1.15 use "Interpret/mathengine.sml"
1.16
1.17 +use "xmlsrc/mathml.sml"
1.18 +use "xmlsrc/datatypes.sml"
1.19 +use "xmlsrc/pbl-met-hierarchy.sml"
1.20 +use "xmlsrc/thy-hierarchy.sml" (*^^^ need files for: fun store_isa*)
1.21 +use "xmlsrc/interface-xml.sml"
1.22 +
1.23 consts
1.24
1.25 Arbfix :: "real"
2.1 --- a/src/Tools/isac/Knowledge/Biegelinie.thy Thu Sep 09 09:58:28 2010 +0200
2.2 +++ b/src/Tools/isac/Knowledge/Biegelinie.thy Thu Sep 09 13:31:36 2010 +0200
2.3 @@ -1,7 +1,6 @@
2.4 (* chapter 'Biegelinie' from the textbook:
2.5 Timischl, Kaiser. Ingenieur-Mathematik 3. Wien 1999. p.268-271.
2.6 - author: Walther Neuper
2.7 - 050826,
2.8 + author: Walther Neuper 050826,
2.9 (c) due to copyright terms
2.10 *)
2.11
2.12 @@ -9,29 +8,29 @@
2.13
2.14 consts
2.15
2.16 - q_ :: real => real ("q'_") (* Streckenlast *)
2.17 - Q :: real => real (* Querkraft *)
2.18 - Q' :: real => real (* Ableitung der Querkraft *)
2.19 - M'_b :: real => real ("M'_b") (* Biegemoment *)
2.20 - M'_b' :: real => real ("M'_b'") (* Ableitung des Biegemoments *)
2.21 - y'' :: real => real (* 2.Ableitung der Biegeline *)
2.22 - y' :: real => real (* Neigung der Biegeline *)
2.23 -(*y :: real => real (* Biegeline *)*)
2.24 - EI :: real (* Biegesteifigkeit *)
2.25 + q_ :: "real => real" ("q'_") (* Streckenlast *)
2.26 + Q :: "real => real" (* Querkraft *)
2.27 + Q' :: "real => real" (* Ableitung der Querkraft *)
2.28 + M'_b :: "real => real" ("M'_b") (* Biegemoment *)
2.29 + M'_b' :: "real => real" ("M'_b'") (* Ableitung des Biegemoments *)
2.30 + y'' :: "real => real" (* 2.Ableitung der Biegeline *)
2.31 + y' :: "real => real" (* Neigung der Biegeline *)
2.32 +(*y :: "real => real" (* Biegeline *)*)
2.33 + EI :: "real" (* Biegesteifigkeit *)
2.34
2.35 (*new Descriptions in the related problems*)
2.36 - Traegerlaenge :: real => una
2.37 - Streckenlast :: real => una
2.38 - BiegemomentVerlauf :: bool => una
2.39 - Biegelinie :: (real => real) => una
2.40 - Randbedingungen :: bool list => una
2.41 - RandbedingungenBiegung :: bool list => una
2.42 - RandbedingungenNeigung :: bool list => una
2.43 - RandbedingungenMoment :: bool list => una
2.44 - RandbedingungenQuerkraft :: bool list => una
2.45 - FunktionsVariable :: real => una
2.46 - Funktionen :: bool list => una
2.47 - Gleichungen :: bool list => una
2.48 + Traegerlaenge :: "real => una"
2.49 + Streckenlast :: "real => una"
2.50 + BiegemomentVerlauf :: "bool => una"
2.51 + Biegelinie :: "(real => real) => una"
2.52 + Randbedingungen :: "bool list => una"
2.53 + RandbedingungenBiegung :: "bool list => una"
2.54 + RandbedingungenNeigung :: "bool list => una"
2.55 + RandbedingungenMoment :: "bool list => una"
2.56 + RandbedingungenQuerkraft :: "bool list => una"
2.57 + FunktionsVariable :: "real => una"
2.58 + Funktionen :: "bool list => una"
2.59 + Gleichungen :: "bool list => una"
2.60
2.61 (*Script-names*)
2.62 Biegelinie2Script :: "[real,real,real,real=>real,bool list,
2.63 @@ -81,31 +80,32 @@
2.64 ["Walther Neuper 2005 supported by a grant from NMI Austria"];
2.65 store_isa ["IsacKnowledge", theory2thyID thy, "Theorems"]
2.66 ["Walther Neuper 2005 supported by a grant from NMI Austria"];
2.67 -store_thm thy ("Belastung_Querkraft", Belastung_Querkraft)
2.68 +store_thm thy ("Belastung_Querkraft", @{thm Belastung_Querkraft})
2.69 ["Walther Neuper 2005 supported by a grant from NMI Austria"];
2.70 -store_thm thy ("Moment_Neigung", Moment_Neigung)
2.71 +store_thm thy ("Moment_Neigung", @{thm Moment_Neigung})
2.72 ["Walther Neuper 2005 supported by a grant from NMI Austria"];
2.73 -store_thm thy ("Moment_Querkraft", Moment_Querkraft)
2.74 +store_thm thy ("Moment_Querkraft", @{thm Moment_Querkraft})
2.75 ["Walther Neuper 2005 supported by a grant from NMI Austria"];
2.76 -store_thm thy ("Neigung_Moment", Neigung_Moment)
2.77 +store_thm thy ("Neigung_Moment", @{thm Neigung_Moment})
2.78 ["Walther Neuper 2005 supported by a grant from NMI Austria"];
2.79 -store_thm thy ("Querkraft_Belastung", Querkraft_Belastung)
2.80 +store_thm thy ("Querkraft_Belastung", @{thm Querkraft_Belastung})
2.81 ["Walther Neuper 2005 supported by a grant from NMI Austria"];
2.82 -store_thm thy ("Querkraft_Moment", Querkraft_Moment)
2.83 +store_thm thy ("Querkraft_Moment", @{thm Querkraft_Moment})
2.84 ["Walther Neuper 2005 supported by a grant from NMI Austria"];
2.85 -store_thm thy ("make_fun_explicit", make_fun_explicit)
2.86 +store_thm thy ("make_fun_explicit", @{thm make_fun_explicit})
2.87 ["Walther Neuper 2005 supported by a grant from NMI Austria"];
2.88
2.89 -
2.90 +*}
2.91 +ML {*
2.92 (** problems **)
2.93
2.94 store_pbt
2.95 (prep_pbt thy "pbl_bieg" [] e_pblID
2.96 (["Biegelinien"],
2.97 - [("#Given" ,["Traegerlaenge l_", "Streckenlast q__"]),
2.98 - (*("#Where",["0 < l_"]), ...wait for < and handling Arbfix*)
2.99 - ("#Find" ,["Biegelinie b_"]),
2.100 - ("#Relate",["Randbedingungen rb_"])
2.101 + [("#Given" ,["Traegerlaenge l_l", "Streckenlast q_q"]),
2.102 + (*("#Where",["0 < l_l"]), ...wait for < and handling Arbfix*)
2.103 + ("#Find" ,["Biegelinie b_b"]),
2.104 + ("#Relate",["Randbedingungen r_b"])
2.105 ],
2.106 append_rls "e_rls" e_rls [],
2.107 NONE,
2.108 @@ -114,10 +114,10 @@
2.109 store_pbt
2.110 (prep_pbt thy "pbl_bieg_mom" [] e_pblID
2.111 (["MomentBestimmte","Biegelinien"],
2.112 - [("#Given" ,["Traegerlaenge l_", "Streckenlast q__"]),
2.113 - (*("#Where",["0 < l_"]), ...wait for < and handling Arbfix*)
2.114 - ("#Find" ,["Biegelinie b_"]),
2.115 - ("#Relate",["RandbedingungenBiegung rb_","RandbedingungenMoment rm_"])
2.116 + [("#Given" ,["Traegerlaenge l_l", "Streckenlast q_q"]),
2.117 + (*("#Where",["0 < l_l"]), ...wait for < and handling Arbfix*)
2.118 + ("#Find" ,["Biegelinie b_b"]),
2.119 + ("#Relate",["RandbedingungenBiegung r_b","RandbedingungenMoment r_m"])
2.120 ],
2.121 append_rls "e_rls" e_rls [],
2.122 NONE,
2.123 @@ -150,8 +150,8 @@
2.124 store_pbt
2.125 (prep_pbt thy "pbl_bieg_vonq" [] e_pblID
2.126 (["vonBelastungZu","Biegelinien"],
2.127 - [("#Given" ,["Streckenlast q__","FunktionsVariable v_v"]),
2.128 - ("#Find" ,["Funktionen funs___"])],
2.129 + [("#Given" ,["Streckenlast q_q","FunktionsVariable v_v"]),
2.130 + ("#Find" ,["Funktionen funs'''"])],
2.131 append_rls "e_rls" e_rls [],
2.132 NONE,
2.133 [["Biegelinien","ausBelastung"]]));
2.134 @@ -159,8 +159,8 @@
2.135 store_pbt
2.136 (prep_pbt thy "pbl_bieg_randbed" [] e_pblID
2.137 (["setzeRandbedingungen","Biegelinien"],
2.138 - [("#Given" ,["Funktionen funs_","Randbedingungen rb_"]),
2.139 - ("#Find" ,["Gleichungen equs___"])],
2.140 + [("#Given" ,["Funktionen fun_s","Randbedingungen r_b"]),
2.141 + ("#Find" ,["Gleichungen equs'''"])],
2.142 append_rls "e_rls" e_rls [],
2.143 NONE,
2.144 [["Biegelinien","setzeRandbedingungenEin"]]));
2.145 @@ -168,28 +168,29 @@
2.146 store_pbt
2.147 (prep_pbt thy "pbl_equ_fromfun" [] e_pblID
2.148 (["makeFunctionTo","equation"],
2.149 - [("#Given" ,["functionEq fun_","substitution sub_"]),
2.150 - ("#Find" ,["equality equ___"])],
2.151 + [("#Given" ,["functionEq fu_n","substitution su_b"]),
2.152 + ("#Find" ,["equality equ'''"])],
2.153 append_rls "e_rls" e_rls [],
2.154 NONE,
2.155 [["Equation","fromFunction"]]));
2.156
2.157 -
2.158 +*}
2.159 +ML {*
2.160 (** methods **)
2.161
2.162 val srls = Rls {id="srls_IntegrierenUnd..",
2.163 preconds = [],
2.164 rew_ord = ("termlessI",termlessI),
2.165 erls = append_rls "erls_in_srls_IntegrierenUnd.." e_rls
2.166 - [(*for asm in nth_Cons_ ...*)
2.167 + [(*for asm in NTH_CONS ...*)
2.168 Calc ("op <",eval_equ "#less_"),
2.169 - (*2nd nth_Cons_ pushes n+-1 into asms*)
2.170 + (*2nd NTH_CONS pushes n+-1 into asms*)
2.171 Calc("op +", eval_binop "#add_")
2.172 ],
2.173 srls = Erls, calc = [],
2.174 - rules = [Thm ("nth_Cons_",num_str @{thm nth_Cons_}),
2.175 + rules = [Thm ("NTH_CONS",num_str @{thm NTH_CONS}),
2.176 Calc("op +", eval_binop "#add_"),
2.177 - Thm ("nth_Nil_",num_str @{thm nth_Nil_}),
2.178 + Thm ("NTH_NIL",num_str @{thm NTH_NIL}),
2.179 Calc("Tools.lhs", eval_lhs"eval_lhs_"),
2.180 Calc("Tools.rhs", eval_rhs"eval_rhs_"),
2.181 Calc("Atools.argument'_in",
2.182 @@ -202,15 +203,15 @@
2.183 preconds = [],
2.184 rew_ord = ("termlessI",termlessI),
2.185 erls = append_rls "erls_in_srls_IntegrierenUnd.." e_rls
2.186 - [(*for asm in nth_Cons_ ...*)
2.187 + [(*for asm in NTH_CONS ...*)
2.188 Calc ("op <",eval_equ "#less_"),
2.189 - (*2nd nth_Cons_ pushes n+-1 into asms*)
2.190 + (*2nd NTH_CONS pushes n+-1 into asms*)
2.191 Calc("op +", eval_binop "#add_")
2.192 ],
2.193 srls = Erls, calc = [],
2.194 - rules = [Thm ("nth_Cons_",num_str @{thm nth_Cons_}),
2.195 + rules = [Thm ("NTH_CONS",num_str @{thm NTH_CONS}),
2.196 Calc("op +", eval_binop "#add_"),
2.197 - Thm ("nth_Nil_", num_str @{thm nth_Nil_}),
2.198 + Thm ("NTH_NIL", num_str @{thm NTH_NIL}),
2.199 Calc("Tools.lhs", eval_lhs "eval_lhs_"),
2.200 Calc("Atools.filter'_sameFunId",
2.201 eval_filter_sameFunId "Atools.filter'_sameFunId"),
2.202 @@ -223,16 +224,18 @@
2.203 Thm ("hd_thm", num_str @{thm hd_thm})
2.204 ],
2.205 scr = EmptyScr};
2.206 -
2.207 +*}
2.208 +
2.209 +ML {*
2.210 store_met
2.211 (prep_met thy "met_biege" [] e_metID
2.212 (["IntegrierenUndKonstanteBestimmen"],
2.213 - [("#Given" ,["Traegerlaenge l_", "Streckenlast q__",
2.214 + [("#Given" ,["Traegerlaenge l_l", "Streckenlast q_q",
2.215 "FunktionsVariable v_v"]),
2.216 - (*("#Where",["0 < l_"]), ...wait for < and handling Arbfix*)
2.217 - ("#Find" ,["Biegelinie b_"]),
2.218 - ("#Relate",["RandbedingungenBiegung rb_",
2.219 - "RandbedingungenMoment rm_"])
2.220 + (*("#Where",["0 < l_l"]), ...wait for < and handling Arbfix*)
2.221 + ("#Find" ,["Biegelinie b_b"]),
2.222 + ("#Relate",["RandbedingungenBiegung r_b",
2.223 + "RandbedingungenMoment r_m"])
2.224 ],
2.225 {rew_ord'="tless_true",
2.226 rls' = append_rls "erls_IntegrierenUndK.." e_rls
2.227 @@ -242,74 +245,76 @@
2.228 calc = [], srls = srls, prls = Erls,
2.229 crls = Atools_erls, nrls = Erls},
2.230 "Script BiegelinieScript " ^
2.231 -"(l_::real) (q__::real) (v_v::real) (b_::real=>real) " ^
2.232 -"(rb_::bool list) (rm_::bool list) = " ^
2.233 -" (let q___ = Take (q_ v_v = q__); " ^
2.234 -" q___ = ((Rewrite sym_real_minus_eq_cancel True) @@ " ^
2.235 -" (Rewrite Belastung_Querkraft True)) q___; " ^
2.236 -" (Q__:: bool) = " ^
2.237 -" (SubProblem (Biegelinie_,[named,integrate,function], " ^
2.238 +"(l_l::real) (q__q::real) (v_v::real) (b_b::real=>real) " ^
2.239 +"(r_b::bool list) (r_m::bool list) = " ^
2.240 +" (let q___q = Take (q_q v_v = q__q); " ^
2.241 +" q___q = ((Rewrite sym_real_minus_eq_cancel True) @@ " ^
2.242 +" (Rewrite Belastung_Querkraft True)) q___q; " ^
2.243 +" (Q__Q:: bool) = " ^
2.244 +" (SubProblem (Biegelinie',[named,integrate,function], " ^
2.245 " [diff,integration,named]) " ^
2.246 -" [REAL (rhs q___), REAL v_v, real_REAL Q]); " ^
2.247 -" Q__ = Rewrite Querkraft_Moment True Q__; " ^
2.248 -" (M__::bool) = " ^
2.249 -" (SubProblem (Biegelinie_,[named,integrate,function], " ^
2.250 +" [REAL (rhs q___q), REAL v_v, REAL_REAL Q]); " ^
2.251 +" Q__Q = Rewrite Querkraft_Moment True Q__Q; " ^
2.252 +" (M__M::bool) = " ^
2.253 +" (SubProblem (Biegelinie',[named,integrate,function], " ^
2.254 " [diff,integration,named]) " ^
2.255 -" [REAL (rhs Q__), REAL v_v, real_REAL M_b]); " ^
2.256 -" e1__ = nth_ 1 rm_; " ^
2.257 -" (x1__::real) = argument_in (lhs e1__); " ^
2.258 -" (M1__::bool) = (Substitute [v_ = x1__]) M__; " ^
2.259 -" M1__ = (Substitute [e1__]) M1__ ; " ^
2.260 -" M2__ = Take M__; " ^
2.261 -(*without this Take 'Substitute [v_ = x2__]' takes _last formula from ctree_*)
2.262 -" e2__ = nth_ 2 rm_; " ^
2.263 -" (x2__::real) = argument_in (lhs e2__); " ^
2.264 -" (M2__::bool) = ((Substitute [v_ = x2__]) @@ " ^
2.265 -" (Substitute [e2__])) M2__; " ^
2.266 -" (c_1_2__::bool list) = " ^
2.267 -" (SubProblem (Biegelinie_,[linear,system],[no_met]) " ^
2.268 -" [booll_ [M1__, M2__], reall [c,c_2]]); " ^
2.269 -" M__ = Take M__; " ^
2.270 -" M__ = ((Substitute c_1_2__) @@ " ^
2.271 +" [REAL (rhs Q__Q), REAL v_v, REAL_REAL M_b]); " ^
2.272 +" e__1 = NTH 1 r_m; " ^
2.273 +" (x__1::real) = argument_in (lhs e__1); " ^
2.274 +" (M__1::bool) = (Substitute [v_v = x__1]) M__M; " ^
2.275 +" M__1 = (Substitute [e__1]) M__1 ; " ^
2.276 +" M__2 = Take M__M; " ^
2.277 +(*without this Take 'Substitute [v_v = x__2]' takes _last formula from ctree_*)
2.278 +" e__2 = NTH 2 r_m; " ^
2.279 +" (x__2::real) = argument_in (lhs e__2); " ^
2.280 +" (M__2::bool) = ((Substitute [v_v = x__2]) @@ " ^
2.281 +" (Substitute [e__2])) M__2; " ^
2.282 +" (c_1_2::bool list) = " ^
2.283 +" (SubProblem (Biegelinie',[linear,system],[no_met]) " ^
2.284 +" [BOOL_LIST [M__1, M__2], REAL_LIST [c,c_2]]); " ^
2.285 +" M__M = Take M__M; " ^
2.286 +" M__M = ((Substitute c_1_2) @@ " ^
2.287 " (Try (Rewrite_Set_Inst [(bdv_1, c),(bdv_2, c_2)]" ^
2.288 " simplify_System False)) @@ " ^
2.289 " (Rewrite Moment_Neigung False) @@ " ^
2.290 -" (Rewrite make_fun_explicit False)) M__; " ^
2.291 +" (Rewrite make_fun_explicit False)) M__M; " ^
2.292 (*----------------------- and the same once more ------------------------*)
2.293 -" (N__:: bool) = " ^
2.294 -" (SubProblem (Biegelinie_,[named,integrate,function], " ^
2.295 +" (N__N:: bool) = " ^
2.296 +" (SubProblem (Biegelinie',[named,integrate,function], " ^
2.297 " [diff,integration,named]) " ^
2.298 -" [REAL (rhs M__), REAL v_v, real_REAL y']); " ^
2.299 -" (B__:: bool) = " ^
2.300 -" (SubProblem (Biegelinie_,[named,integrate,function], " ^
2.301 +" [REAL (rhs M__M), REAL v_v, REAL_REAL y']); " ^
2.302 +" (B__B:: bool) = " ^
2.303 +" (SubProblem (Biegelinie',[named,integrate,function], " ^
2.304 " [diff,integration,named]) " ^
2.305 -" [REAL (rhs N__), REAL v_v, real_REAL y]); " ^
2.306 -" e1__ = nth_ 1 rb_; " ^
2.307 -" (x1__::real) = argument_in (lhs e1__); " ^
2.308 -" (B1__::bool) = (Substitute [v_ = x1__]) B__; " ^
2.309 -" B1__ = (Substitute [e1__]) B1__ ; " ^
2.310 -" B2__ = Take B__; " ^
2.311 -" e2__ = nth_ 2 rb_; " ^
2.312 -" (x2__::real) = argument_in (lhs e2__); " ^
2.313 -" (B2__::bool) = ((Substitute [v_ = x2__]) @@ " ^
2.314 -" (Substitute [e2__])) B2__; " ^
2.315 -" (c_1_2__::bool list) = " ^
2.316 -" (SubProblem (Biegelinie_,[linear,system],[no_met]) " ^
2.317 -" [booll_ [B1__, B2__], reall [c,c_2]]); " ^
2.318 -" B__ = Take B__; " ^
2.319 -" B__ = ((Substitute c_1_2__) @@ " ^
2.320 -" (Rewrite_Set_Inst [(bdv, x)] make_ratpoly_in False)) B__ " ^
2.321 -" in B__)"
2.322 +" [REAL (rhs N__N), REAL v_v, REAL_REAL y]); " ^
2.323 +" e__1 = NTH 1 r_b; " ^
2.324 +" (x__1::real) = argument_in (lhs e__1); " ^
2.325 +" (B__1::bool) = (Substitute [v_v = x__1]) B__B; " ^
2.326 +" B__1 = (Substitute [e__1]) B__1 ; " ^
2.327 +" B__2 = Take B__B; " ^
2.328 +" e__2 = NTH 2 r_b; " ^
2.329 +" (x__2::real) = argument_in (lhs e__2); " ^
2.330 +" (B__2::bool) = ((Substitute [v_v = x__2]) @@ " ^
2.331 +" (Substitute [e__2])) B__2; " ^
2.332 +" (c_1_2::bool list) = " ^
2.333 +" (SubProblem (Biegelinie',[linear,system],[no_met]) " ^
2.334 +" [BOOL_LIST [B__1, B__2], REAL_LIST [c,c_2]]); " ^
2.335 +" B__B = Take B__B; " ^
2.336 +" B__B = ((Substitute c_1_2) @@ " ^
2.337 +" (Rewrite_Set_Inst [(bdv, x)] make_ratpoly_in False)) B__B " ^
2.338 +" in B__B)"
2.339 ));
2.340 +*}
2.341 +ML {*
2.342
2.343 store_met
2.344 (prep_met thy "met_biege_2" [] e_metID
2.345 (["IntegrierenUndKonstanteBestimmen2"],
2.346 - [("#Given" ,["Traegerlaenge l_", "Streckenlast q__",
2.347 + [("#Given" ,["Traegerlaenge l_l", "Streckenlast q__q",
2.348 "FunktionsVariable v_v"]),
2.349 - (*("#Where",["0 < l_"]), ...wait for < and handling Arbfix*)
2.350 - ("#Find" ,["Biegelinie b_"]),
2.351 - ("#Relate",["Randbedingungen rb_"])
2.352 + (*("#Where",["0 < l_l"]), ...wait for < and handling Arbfix*)
2.353 + ("#Find" ,["Biegelinie b_b"]),
2.354 + ("#Relate",["Randbedingungen r_b"])
2.355 ],
2.356 {rew_ord'="tless_true",
2.357 rls' = append_rls "erls_IntegrierenUndK.." e_rls
2.358 @@ -326,25 +331,27 @@
2.359 ],
2.360 prls = Erls, crls = Atools_erls, nrls = Erls},
2.361 "Script Biegelinie2Script " ^
2.362 -"(l_::real) (q__::real) (v_v::real) (b_::real=>real) (rb_::bool list) = " ^
2.363 +"(l_l::real) (q__q::real) (v_v::real) (b_b::real=>real) (r_b::bool list) = " ^
2.364 " (let " ^
2.365 -" (funs_:: bool list) = " ^
2.366 -" (SubProblem (Biegelinie_,[vonBelastungZu,Biegelinien], " ^
2.367 +" (fun_s:: bool list) = " ^
2.368 +" (SubProblem (Biegelinie',[vonBelastungZu,Biegelinien], " ^
2.369 " [Biegelinien,ausBelastung]) " ^
2.370 -" [REAL q__, REAL v_]); " ^
2.371 -" (equs_::bool list) = " ^
2.372 -" (SubProblem (Biegelinie_,[setzeRandbedingungen,Biegelinien]," ^
2.373 +" [REAL q__q, REAL v_v]); " ^
2.374 +" (equ_s::bool list) = " ^
2.375 +" (SubProblem (Biegelinie',[setzeRandbedingungen,Biegelinien]," ^
2.376 " [Biegelinien,setzeRandbedingungenEin]) " ^
2.377 -" [booll_ funs_, booll_ rb_]); " ^
2.378 -" (cons_::bool list) = " ^
2.379 -" (SubProblem (Biegelinie_,[linear,system],[no_met]) " ^
2.380 -" [booll_ equs_, reall [c,c_2,c_3,c_4]]); " ^
2.381 -" B_ = Take (lastI funs_); " ^
2.382 -" B_ = ((Substitute cons_) @@ " ^
2.383 -" (Rewrite_Set_Inst [(bdv, v_v)] make_ratpoly_in False)) B_ " ^
2.384 -" in B_)"
2.385 +" [BOOL_LIST fun_s, BOOL_LIST r_b]); " ^
2.386 +" (con_s::bool list) = " ^
2.387 +" (SubProblem (Biegelinie',[linear,system],[no_met]) " ^
2.388 +" [BOOL_LIST equ_s, REAL_LIST [c,c_2,c_3,c_4]]); " ^
2.389 +" B_B = Take (lastI fun_s); " ^
2.390 +" B_B = ((Substitute con_s) @@ " ^
2.391 +" (Rewrite_Set_Inst [(bdv, v_v)] make_ratpoly_in False)) B_B " ^
2.392 +" in B_B)"
2.393 ));
2.394
2.395 +*}
2.396 +ML {*
2.397 store_met
2.398 (prep_met thy "met_biege_intconst_2" [] e_metID
2.399 (["IntegrierenUndKonstanteBestimmen","2xIntegrieren"],
2.400 @@ -389,11 +396,13 @@
2.401 "empty_script"
2.402 ));
2.403
2.404 +*}
2.405 +ML {*
2.406 store_met
2.407 (prep_met thy "met_biege_ausbelast" [] e_metID
2.408 (["Biegelinien","ausBelastung"],
2.409 - [("#Given" ,["Streckenlast q__","FunktionsVariable v_v"]),
2.410 - ("#Find" ,["Funktionen funs_"])],
2.411 + [("#Given" ,["Streckenlast q__q","FunktionsVariable v_v"]),
2.412 + ("#Find" ,["Funktionen fun_s"])],
2.413 {rew_ord'="tless_true",
2.414 rls' = append_rls "erls_ausBelastung" e_rls
2.415 [Calc ("Atools.ident",eval_ident "#ident_"),
2.416 @@ -403,118 +412,121 @@
2.417 srls = append_rls "srls_ausBelastung" e_rls
2.418 [Calc("Tools.rhs", eval_rhs"eval_rhs_")],
2.419 prls = e_rls, crls = Atools_erls, nrls = e_rls},
2.420 -"Script Belastung2BiegelScript (q__::real) (v_v::real) = " ^
2.421 -" (let q___ = Take (q_ v_v = q__); " ^
2.422 -" q___ = ((Rewrite sym_real_minus_eq_cancel True) @@ " ^
2.423 -" (Rewrite Belastung_Querkraft True)) q___; " ^
2.424 -" (Q__:: bool) = " ^
2.425 -" (SubProblem (Biegelinie_,[named,integrate,function], " ^
2.426 +"Script Belastung2BiegelScript (q__q::real) (v_v::real) = " ^
2.427 +" (let q___q = Take (q_q v_v = q__q); " ^
2.428 +" q___q = ((Rewrite sym_real_minus_eq_cancel True) @@ " ^
2.429 +" (Rewrite Belastung_Querkraft True)) q___q; " ^
2.430 +" (Q__Q:: bool) = " ^
2.431 +" (SubProblem (Biegelinie',[named,integrate,function], " ^
2.432 " [diff,integration,named]) " ^
2.433 -" [REAL (rhs q___), REAL v_v, real_REAL Q]); " ^
2.434 -" M__ = Rewrite Querkraft_Moment True Q__; " ^
2.435 -" (M__::bool) = " ^
2.436 -" (SubProblem (Biegelinie_,[named,integrate,function], " ^
2.437 +" [REAL (rhs q___q), REAL v_v, REAL_REAL Q]); " ^
2.438 +" M__M = Rewrite Querkraft_Moment True Q__Q; " ^
2.439 +" (M__M::bool) = " ^
2.440 +" (SubProblem (Biegelinie',[named,integrate,function], " ^
2.441 " [diff,integration,named]) " ^
2.442 -" [REAL (rhs M__), REAL v_v, real_REAL M_b]); " ^
2.443 -" N__ = ((Rewrite Moment_Neigung False) @@ " ^
2.444 -" (Rewrite make_fun_explicit False)) M__; " ^
2.445 -" (N__:: bool) = " ^
2.446 -" (SubProblem (Biegelinie_,[named,integrate,function], " ^
2.447 +" [REAL (rhs M__M), REAL v_v, REAL_REAL M_b]); " ^
2.448 +" N__N = ((Rewrite Moment_Neigung False) @@ " ^
2.449 +" (Rewrite make_fun_explicit False)) M__M; " ^
2.450 +" (N__N:: bool) = " ^
2.451 +" (SubProblem (Biegelinie',[named,integrate,function], " ^
2.452 " [diff,integration,named]) " ^
2.453 -" [REAL (rhs N__), REAL v_v, real_REAL y']); " ^
2.454 -" (B__:: bool) = " ^
2.455 -" (SubProblem (Biegelinie_,[named,integrate,function], " ^
2.456 +" [REAL (rhs N__N), REAL v_v, REAL_REAL y']); " ^
2.457 +" (B__B:: bool) = " ^
2.458 +" (SubProblem (Biegelinie',[named,integrate,function], " ^
2.459 " [diff,integration,named]) " ^
2.460 -" [REAL (rhs N__), REAL v_v, real_REAL y]) " ^
2.461 -" in [Q__, M__, N__, B__])"
2.462 +" [REAL (rhs N__N), REAL v_v, REAL_REAL y]) " ^
2.463 +" in [Q__Q, M__M, N__N, B__B])"
2.464 ));
2.465
2.466 +*}
2.467 +ML {*
2.468 store_met
2.469 (prep_met thy "met_biege_setzrand" [] e_metID
2.470 (["Biegelinien","setzeRandbedingungenEin"],
2.471 - [("#Given" ,["Funktionen funs_","Randbedingungen rb_"]),
2.472 - ("#Find" ,["Gleichungen equs___"])],
2.473 + [("#Given" ,["Funktionen fun_s","Randbedingungen r_b"]),
2.474 + ("#Find" ,["Gleichungen equs'''"])],
2.475 {rew_ord'="tless_true", rls'=Erls, calc = [],
2.476 srls = srls2,
2.477 prls=e_rls,
2.478 crls = Atools_erls, nrls = e_rls},
2.479 -"Script SetzeRandbedScript (funs_::bool list) (rb_::bool list) = " ^
2.480 -" (let b1_ = nth_ 1 rb_; " ^
2.481 -" fs_ = filter_sameFunId (lhs b1_) funs_; " ^
2.482 -" (e1_::bool) = " ^
2.483 -" (SubProblem (Biegelinie_,[makeFunctionTo,equation]," ^
2.484 +"Script SetzeRandbedScript (fun_s::bool list) (r_b::bool list) = " ^
2.485 +" (let b_1 = NTH 1 r_b; " ^
2.486 +" f_s = filter_sameFunId (lhs b_1) fun_s; " ^
2.487 +" (e_1::bool) = " ^
2.488 +" (SubProblem (Biegelinie',[makeFunctionTo,equation]," ^
2.489 " [Equation,fromFunction]) " ^
2.490 -" [BOOL (hd fs_), BOOL b1_]); " ^
2.491 -" b2_ = nth_ 2 rb_; " ^
2.492 -" fs_ = filter_sameFunId (lhs b2_) funs_; " ^
2.493 -" (e2_::bool) = " ^
2.494 -" (SubProblem (Biegelinie_,[makeFunctionTo,equation]," ^
2.495 +" [BOOL (hd f_s), BOOL b_1]); " ^
2.496 +" b_2 = NTH 2 r_b; " ^
2.497 +" f_s = filter_sameFunId (lhs b_2) fun_s; " ^
2.498 +" (e_2::bool) = " ^
2.499 +" (SubProblem (Biegelinie',[makeFunctionTo,equation]," ^
2.500 " [Equation,fromFunction]) " ^
2.501 -" [BOOL (hd fs_), BOOL b2_]); " ^
2.502 -" b3_ = nth_ 3 rb_; " ^
2.503 -" fs_ = filter_sameFunId (lhs b3_) funs_; " ^
2.504 -" (e3_::bool) = " ^
2.505 -" (SubProblem (Biegelinie_,[makeFunctionTo,equation]," ^
2.506 +" [BOOL (hd f_s), BOOL b_2]); " ^
2.507 +" b_3 = NTH 3 r_b; " ^
2.508 +" f_s = filter_sameFunId (lhs b_3) fun_s; " ^
2.509 +" (e_3::bool) = " ^
2.510 +" (SubProblem (Biegelinie',[makeFunctionTo,equation]," ^
2.511 " [Equation,fromFunction]) " ^
2.512 -" [BOOL (hd fs_), BOOL b3_]); " ^
2.513 -" b4_ = nth_ 4 rb_; " ^
2.514 -" fs_ = filter_sameFunId (lhs b4_) funs_; " ^
2.515 -" (e4_::bool) = " ^
2.516 -" (SubProblem (Biegelinie_,[makeFunctionTo,equation]," ^
2.517 +" [BOOL (hd f_s), BOOL b_3]); " ^
2.518 +" b_4 = NTH 4 r_b; " ^
2.519 +" f_s = filter_sameFunId (lhs b_4) fun_s; " ^
2.520 +" (e_4::bool) = " ^
2.521 +" (SubProblem (Biegelinie',[makeFunctionTo,equation]," ^
2.522 " [Equation,fromFunction]) " ^
2.523 -" [BOOL (hd fs_), BOOL b4_]) " ^
2.524 -" in [e1_,e2_,e3_,e4_])"
2.525 +" [BOOL (hd f_s), BOOL b_4]) " ^
2.526 +" in [e_1,e_2,e_3,e_4])"
2.527 (* filter requires more than 1 sec !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!
2.528 -"Script SetzeRandbedScript (funs_::bool list) (rb_::bool list) = " ^
2.529 -" (let b1_ = nth_ 1 rb_; " ^
2.530 -" fs_ = filter (sameFunId (lhs b1_)) funs_; " ^
2.531 -" (e1_::bool) = " ^
2.532 -" (SubProblem (Biegelinie_,[makeFunctionTo,equation]," ^
2.533 +"Script SetzeRandbedScript (fun_s::bool list) (r_b::bool list) = " ^
2.534 +" (let b_1 = NTH 1 r_b; " ^
2.535 +" f_s = filter (sameFunId (lhs b_1)) fun_s; " ^
2.536 +" (e_1::bool) = " ^
2.537 +" (SubProblem (Biegelinie',[makeFunctionTo,equation]," ^
2.538 " [Equation,fromFunction]) " ^
2.539 -" [BOOL (hd fs_), BOOL b1_]); " ^
2.540 -" b2_ = nth_ 2 rb_; " ^
2.541 -" fs_ = filter (sameFunId (lhs b2_)) funs_; " ^
2.542 -" (e2_::bool) = " ^
2.543 -" (SubProblem (Biegelinie_,[makeFunctionTo,equation]," ^
2.544 +" [BOOL (hd f_s), BOOL b_1]); " ^
2.545 +" b_2 = NTH 2 r_b; " ^
2.546 +" f_s = filter (sameFunId (lhs b_2)) fun_s; " ^
2.547 +" (e_2::bool) = " ^
2.548 +" (SubProblem (Biegelinie',[makeFunctionTo,equation]," ^
2.549 " [Equation,fromFunction]) " ^
2.550 -" [BOOL (hd fs_), BOOL b2_]); " ^
2.551 -" b3_ = nth_ 3 rb_; " ^
2.552 -" fs_ = filter (sameFunId (lhs b3_)) funs_; " ^
2.553 -" (e3_::bool) = " ^
2.554 -" (SubProblem (Biegelinie_,[makeFunctionTo,equation]," ^
2.555 +" [BOOL (hd f_s), BOOL b_2]); " ^
2.556 +" b_3 = NTH 3 r_b; " ^
2.557 +" f_s = filter (sameFunId (lhs b_3)) fun_s; " ^
2.558 +" (e_3::bool) = " ^
2.559 +" (SubProblem (Biegelinie',[makeFunctionTo,equation]," ^
2.560 " [Equation,fromFunction]) " ^
2.561 -" [BOOL (hd fs_), BOOL b3_]); " ^
2.562 -" b4_ = nth_ 4 rb_; " ^
2.563 -" fs_ = filter (sameFunId (lhs b4_)) funs_; " ^
2.564 -" (e4_::bool) = " ^
2.565 -" (SubProblem (Biegelinie_,[makeFunctionTo,equation]," ^
2.566 +" [BOOL (hd f_s), BOOL b_3]); " ^
2.567 +" b_4 = NTH 4 r_b; " ^
2.568 +" f_s = filter (sameFunId (lhs b_4)) fun_s; " ^
2.569 +" (e_4::bool) = " ^
2.570 +" (SubProblem (Biegelinie',[makeFunctionTo,equation]," ^
2.571 " [Equation,fromFunction]) " ^
2.572 -" [BOOL (hd fs_), BOOL b4_]) " ^
2.573 -" in [e1_,e2_,e3_,e4_])"*)
2.574 +" [BOOL (hd f_s), BOOL b_4]) " ^
2.575 +" in [e_1,e_2,e_3,e_4])"*)
2.576 ));
2.577
2.578 +*}
2.579 +ML {*
2.580 store_met
2.581 (prep_met thy "met_equ_fromfun" [] e_metID
2.582 (["Equation","fromFunction"],
2.583 - [("#Given" ,["functionEq fun_","substitution sub_"]),
2.584 - ("#Find" ,["equality equ___"])],
2.585 + [("#Given" ,["functionEq fu_n","substitution su_b"]),
2.586 + ("#Find" ,["equality equ'''"])],
2.587 {rew_ord'="tless_true", rls'=Erls, calc = [],
2.588 srls = append_rls "srls_in_EquationfromFunc" e_rls
2.589 [Calc("Tools.lhs", eval_lhs"eval_lhs_"),
2.590 Calc("Atools.argument'_in",
2.591 eval_argument_in
2.592 "Atools.argument'_in")],
2.593 - prls=e_rls,
2.594 - crls = Atools_erls, nrls = e_rls},
2.595 + prls=e_rls, crls = Atools_erls, nrls = e_rls},
2.596 (*(M_b x = c_2 + c * x + -1 * q_0 / 2 * x ^^^ 2) (M_b L = 0) -->
2.597 0 = c_2 + c * L + -1 * q_0 / 2 * L ^^^ 2*)
2.598 -"Script Function2Equality (fun_::bool) (sub_::bool) =" ^
2.599 -" (let fun_ = Take fun_; " ^
2.600 -" bdv_ = argument_in (lhs fun_); " ^
2.601 -" val_ = argument_in (lhs sub_); " ^
2.602 -" equ_ = (Substitute [bdv_ = val_]) fun_; " ^
2.603 -" equ_ = (Substitute [sub_]) fun_ " ^
2.604 -" in (Rewrite_Set norm_Rational False) equ_) "
2.605 +"Script Function2Equality (fu_n::bool) (su_b::bool) =" ^
2.606 +" (let fu_n = Take fu_n; " ^
2.607 +" bd_v = argument_in (lhs fu_n); " ^
2.608 +" va_l = argument_in (lhs su_b); " ^
2.609 +" eq_u = (Substitute [bd_v = va_l]) fu_n; " ^
2.610 +" eq_u = (Substitute [su_b]) fu_n " ^
2.611 +" in (Rewrite_Set norm_Rational False) eq_u) "
2.612 ));
2.613 *}
2.614