1.1 --- a/src/Tools/isac/Knowledge/Biegelinie.ML Thu Aug 26 18:21:14 2010 +0200
1.2 +++ b/src/Tools/isac/Knowledge/Biegelinie.ML Fri Aug 27 10:28:44 2010 +0200
1.3 @@ -18,30 +18,30 @@
1.4 (** theory elements **)
1.5
1.6 store_isa ["IsacKnowledge"] [];
1.7 -store_thy Biegelinie.thy
1.8 +store_thy (theory "Biegelinie")
1.9 ["Walther Neuper 2005 supported by a grant from NMI Austria"];
1.10 -store_isa ["IsacKnowledge", theory2thyID Biegelinie.thy, "Theorems"]
1.11 +store_isa ["IsacKnowledge", theory2thyID (theory "Biegelinie"), "Theorems"]
1.12 ["Walther Neuper 2005 supported by a grant from NMI Austria"];
1.13 -store_thm Biegelinie.thy ("Belastung_Querkraft", Belastung_Querkraft)
1.14 +store_thm (theory "Biegelinie") ("Belastung_Querkraft", Belastung_Querkraft)
1.15 ["Walther Neuper 2005 supported by a grant from NMI Austria"];
1.16 -store_thm Biegelinie.thy ("Moment_Neigung", Moment_Neigung)
1.17 +store_thm (theory "Biegelinie") ("Moment_Neigung", Moment_Neigung)
1.18 ["Walther Neuper 2005 supported by a grant from NMI Austria"];
1.19 -store_thm Biegelinie.thy ("Moment_Querkraft", Moment_Querkraft)
1.20 +store_thm (theory "Biegelinie") ("Moment_Querkraft", Moment_Querkraft)
1.21 ["Walther Neuper 2005 supported by a grant from NMI Austria"];
1.22 -store_thm Biegelinie.thy ("Neigung_Moment", Neigung_Moment)
1.23 +store_thm (theory "Biegelinie") ("Neigung_Moment", Neigung_Moment)
1.24 ["Walther Neuper 2005 supported by a grant from NMI Austria"];
1.25 -store_thm Biegelinie.thy ("Querkraft_Belastung", Querkraft_Belastung)
1.26 +store_thm (theory "Biegelinie") ("Querkraft_Belastung", Querkraft_Belastung)
1.27 ["Walther Neuper 2005 supported by a grant from NMI Austria"];
1.28 -store_thm Biegelinie.thy ("Querkraft_Moment", Querkraft_Moment)
1.29 +store_thm (theory "Biegelinie") ("Querkraft_Moment", Querkraft_Moment)
1.30 ["Walther Neuper 2005 supported by a grant from NMI Austria"];
1.31 -store_thm Biegelinie.thy ("make_fun_explicit", make_fun_explicit)
1.32 +store_thm (theory "Biegelinie") ("make_fun_explicit", make_fun_explicit)
1.33 ["Walther Neuper 2005 supported by a grant from NMI Austria"];
1.34
1.35
1.36 (** problems **)
1.37
1.38 store_pbt
1.39 - (prep_pbt Biegelinie.thy "pbl_bieg" [] e_pblID
1.40 + (prep_pbt (theory "Biegelinie") "pbl_bieg" [] e_pblID
1.41 (["Biegelinien"],
1.42 [("#Given" ,["Traegerlaenge l_", "Streckenlast q__"]),
1.43 (*("#Where",["0 < l_"]), ...wait for < and handling Arbfix*)
1.44 @@ -53,7 +53,7 @@
1.45 [["IntegrierenUndKonstanteBestimmen2"]]));
1.46
1.47 store_pbt
1.48 - (prep_pbt Biegelinie.thy "pbl_bieg_mom" [] e_pblID
1.49 + (prep_pbt (theory "Biegelinie") "pbl_bieg_mom" [] e_pblID
1.50 (["MomentBestimmte","Biegelinien"],
1.51 [("#Given" ,["Traegerlaenge l_", "Streckenlast q__"]),
1.52 (*("#Where",["0 < l_"]), ...wait for < and handling Arbfix*)
1.53 @@ -65,7 +65,7 @@
1.54 [["IntegrierenUndKonstanteBestimmen"]]));
1.55
1.56 store_pbt
1.57 - (prep_pbt Biegelinie.thy "pbl_bieg_momg" [] e_pblID
1.58 + (prep_pbt (theory "Biegelinie") "pbl_bieg_momg" [] e_pblID
1.59 (["MomentGegebene","Biegelinien"],
1.60 [],
1.61 append_rls "e_rls" e_rls [],
1.62 @@ -73,7 +73,7 @@
1.63 [["IntegrierenUndKonstanteBestimmen","2xIntegrieren"]]));
1.64
1.65 store_pbt
1.66 - (prep_pbt Biegelinie.thy "pbl_bieg_einf" [] e_pblID
1.67 + (prep_pbt (theory "Biegelinie") "pbl_bieg_einf" [] e_pblID
1.68 (["einfache","Biegelinien"],
1.69 [],
1.70 append_rls "e_rls" e_rls [],
1.71 @@ -81,7 +81,7 @@
1.72 [["IntegrierenUndKonstanteBestimmen","4x4System"]]));
1.73
1.74 store_pbt
1.75 - (prep_pbt Biegelinie.thy "pbl_bieg_momquer" [] e_pblID
1.76 + (prep_pbt (theory "Biegelinie") "pbl_bieg_momquer" [] e_pblID
1.77 (["QuerkraftUndMomentBestimmte","Biegelinien"],
1.78 [],
1.79 append_rls "e_rls" e_rls [],
1.80 @@ -89,7 +89,7 @@
1.81 [["IntegrierenUndKonstanteBestimmen","1xIntegrieren"]]));
1.82
1.83 store_pbt
1.84 - (prep_pbt Biegelinie.thy "pbl_bieg_vonq" [] e_pblID
1.85 + (prep_pbt (theory "Biegelinie") "pbl_bieg_vonq" [] e_pblID
1.86 (["vonBelastungZu","Biegelinien"],
1.87 [("#Given" ,["Streckenlast q__","FunktionsVariable v_"]),
1.88 ("#Find" ,["Funktionen funs___"])],
1.89 @@ -98,7 +98,7 @@
1.90 [["Biegelinien","ausBelastung"]]));
1.91
1.92 store_pbt
1.93 - (prep_pbt Biegelinie.thy "pbl_bieg_randbed" [] e_pblID
1.94 + (prep_pbt (theory "Biegelinie") "pbl_bieg_randbed" [] e_pblID
1.95 (["setzeRandbedingungen","Biegelinien"],
1.96 [("#Given" ,["Funktionen funs_","Randbedingungen rb_"]),
1.97 ("#Find" ,["Gleichungen equs___"])],
1.98 @@ -107,7 +107,7 @@
1.99 [["Biegelinien","setzeRandbedingungenEin"]]));
1.100
1.101 store_pbt
1.102 - (prep_pbt Biegelinie.thy "pbl_equ_fromfun" [] e_pblID
1.103 + (prep_pbt (theory "Biegelinie") "pbl_equ_fromfun" [] e_pblID
1.104 (["makeFunctionTo","equation"],
1.105 [("#Given" ,["functionEq fun_","substitution sub_"]),
1.106 ("#Find" ,["equality equ___"])],
1.107 @@ -116,7 +116,6 @@
1.108 [["Equation","fromFunction"]]));
1.109
1.110
1.111 -
1.112 (** methods **)
1.113
1.114 val srls = Rls {id="srls_IntegrierenUnd..",
1.115 @@ -165,12 +164,9 @@
1.116 Thm ("hd_thm", num_str hd_thm)
1.117 ],
1.118 scr = EmptyScr};
1.119 -(*@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@*)
1.120 -(* use"Knowledge/Biegelinie.ML";
1.121 - *)
1.122
1.123 store_met
1.124 - (prep_met Biegelinie.thy "met_biege" [] e_metID
1.125 + (prep_met (theory "Biegelinie") "met_biege" [] e_metID
1.126 (["IntegrierenUndKonstanteBestimmen"],
1.127 [("#Given" ,["Traegerlaenge l_", "Streckenlast q__",
1.128 "FunktionsVariable v_"]),
1.129 @@ -186,69 +182,69 @@
1.130 Thm ("not_false",num_str not_false)],
1.131 calc = [], srls = srls, prls = Erls,
1.132 crls = Atools_erls, nrls = Erls},
1.133 -"Script BiegelinieScript \
1.134 -\(l_::real) (q__::real) (v_::real) (b_::real=>real) \
1.135 -\(rb_::bool list) (rm_::bool list) = \
1.136 -\ (let q___ = Take (q_ v_ = q__); \
1.137 -\ q___ = ((Rewrite sym_real_minus_eq_cancel True) @@ \
1.138 -\ (Rewrite Belastung_Querkraft True)) q___; \
1.139 -\ (Q__:: bool) = \
1.140 -\ (SubProblem (Biegelinie_,[named,integrate,function], \
1.141 -\ [diff,integration,named]) \
1.142 -\ [real_ (rhs q___), real_ v_, real_real_ Q]); \
1.143 -\ Q__ = Rewrite Querkraft_Moment True Q__; \
1.144 -\ (M__::bool) = \
1.145 -\ (SubProblem (Biegelinie_,[named,integrate,function], \
1.146 -\ [diff,integration,named]) \
1.147 -\ [real_ (rhs Q__), real_ v_, real_real_ M_b]); \
1.148 -\ e1__ = nth_ 1 rm_; \
1.149 -\ (x1__::real) = argument_in (lhs e1__); \
1.150 -\ (M1__::bool) = (Substitute [v_ = x1__]) M__; \
1.151 -\ M1__ = (Substitute [e1__]) M1__ ; \
1.152 -\ M2__ = Take M__; "^
1.153 +"Script BiegelinieScript " ^
1.154 +"(l_::real) (q__::real) (v_::real) (b_::real=>real) " ^
1.155 +"(rb_::bool list) (rm_::bool list) = " ^
1.156 +" (let q___ = Take (q_ v_ = q__); " ^
1.157 +" q___ = ((Rewrite sym_real_minus_eq_cancel True) @@ " ^
1.158 +" (Rewrite Belastung_Querkraft True)) q___; " ^
1.159 +" (Q__:: bool) = " ^
1.160 +" (SubProblem (Biegelinie_,[named,integrate,function], " ^
1.161 +" [diff,integration,named]) " ^
1.162 +" [real_ (rhs q___), real_ v_, real_real_ Q]); " ^
1.163 +" Q__ = Rewrite Querkraft_Moment True Q__; " ^
1.164 +" (M__::bool) = " ^
1.165 +" (SubProblem (Biegelinie_,[named,integrate,function], " ^
1.166 +" [diff,integration,named]) " ^
1.167 +" [real_ (rhs Q__), real_ v_, real_real_ M_b]); " ^
1.168 +" e1__ = nth_ 1 rm_; " ^
1.169 +" (x1__::real) = argument_in (lhs e1__); " ^
1.170 +" (M1__::bool) = (Substitute [v_ = x1__]) M__; " ^
1.171 +" M1__ = (Substitute [e1__]) M1__ ; " ^
1.172 +" M2__ = Take M__; " ^
1.173 (*without this Take 'Substitute [v_ = x2__]' takes _last formula from ctree_*)
1.174 -" e2__ = nth_ 2 rm_; \
1.175 -\ (x2__::real) = argument_in (lhs e2__); \
1.176 -\ (M2__::bool) = ((Substitute [v_ = x2__]) @@ \
1.177 -\ (Substitute [e2__])) M2__; \
1.178 -\ (c_1_2__::bool list) = \
1.179 -\ (SubProblem (Biegelinie_,[linear,system],[no_met]) \
1.180 -\ [booll_ [M1__, M2__], reall [c,c_2]]); \
1.181 -\ M__ = Take M__; \
1.182 -\ M__ = ((Substitute c_1_2__) @@ \
1.183 -\ (Try (Rewrite_Set_Inst [(bdv_1, c),(bdv_2, c_2)]\
1.184 -\ simplify_System False)) @@ \
1.185 -\ (Rewrite Moment_Neigung False) @@ \
1.186 -\ (Rewrite make_fun_explicit False)) M__; "^
1.187 +" e2__ = nth_ 2 rm_; " ^
1.188 +" (x2__::real) = argument_in (lhs e2__); " ^
1.189 +" (M2__::bool) = ((Substitute [v_ = x2__]) @@ " ^
1.190 +" (Substitute [e2__])) M2__; " ^
1.191 +" (c_1_2__::bool list) = " ^
1.192 +" (SubProblem (Biegelinie_,[linear,system],[no_met]) " ^
1.193 +" [booll_ [M1__, M2__], reall [c,c_2]]); " ^
1.194 +" M__ = Take M__; " ^
1.195 +" M__ = ((Substitute c_1_2__) @@ " ^
1.196 +" (Try (Rewrite_Set_Inst [(bdv_1, c),(bdv_2, c_2)]" ^
1.197 +" simplify_System False)) @@ " ^
1.198 +" (Rewrite Moment_Neigung False) @@ " ^
1.199 +" (Rewrite make_fun_explicit False)) M__; " ^
1.200 (*----------------------- and the same once more ------------------------*)
1.201 -" (N__:: bool) = \
1.202 -\ (SubProblem (Biegelinie_,[named,integrate,function], \
1.203 -\ [diff,integration,named]) \
1.204 -\ [real_ (rhs M__), real_ v_, real_real_ y']); \
1.205 -\ (B__:: bool) = \
1.206 -\ (SubProblem (Biegelinie_,[named,integrate,function], \
1.207 -\ [diff,integration,named]) \
1.208 -\ [real_ (rhs N__), real_ v_, real_real_ y]); \
1.209 -\ e1__ = nth_ 1 rb_; \
1.210 -\ (x1__::real) = argument_in (lhs e1__); \
1.211 -\ (B1__::bool) = (Substitute [v_ = x1__]) B__; \
1.212 -\ B1__ = (Substitute [e1__]) B1__ ; \
1.213 -\ B2__ = Take B__; \
1.214 -\ e2__ = nth_ 2 rb_; \
1.215 -\ (x2__::real) = argument_in (lhs e2__); \
1.216 -\ (B2__::bool) = ((Substitute [v_ = x2__]) @@ \
1.217 -\ (Substitute [e2__])) B2__; \
1.218 -\ (c_1_2__::bool list) = \
1.219 -\ (SubProblem (Biegelinie_,[linear,system],[no_met]) \
1.220 -\ [booll_ [B1__, B2__], reall [c,c_2]]); \
1.221 -\ B__ = Take B__; \
1.222 -\ B__ = ((Substitute c_1_2__) @@ \
1.223 -\ (Rewrite_Set_Inst [(bdv, x)] make_ratpoly_in False)) B__ \
1.224 -\ in B__)"
1.225 +" (N__:: bool) = " ^
1.226 +" (SubProblem (Biegelinie_,[named,integrate,function], " ^
1.227 +" [diff,integration,named]) " ^
1.228 +" [real_ (rhs M__), real_ v_, real_real_ y']); " ^
1.229 +" (B__:: bool) = " ^
1.230 +" (SubProblem (Biegelinie_,[named,integrate,function], " ^
1.231 +" [diff,integration,named]) " ^
1.232 +" [real_ (rhs N__), real_ v_, real_real_ y]); " ^
1.233 +" e1__ = nth_ 1 rb_; " ^
1.234 +" (x1__::real) = argument_in (lhs e1__); " ^
1.235 +" (B1__::bool) = (Substitute [v_ = x1__]) B__; " ^
1.236 +" B1__ = (Substitute [e1__]) B1__ ; " ^
1.237 +" B2__ = Take B__; " ^
1.238 +" e2__ = nth_ 2 rb_; " ^
1.239 +" (x2__::real) = argument_in (lhs e2__); " ^
1.240 +" (B2__::bool) = ((Substitute [v_ = x2__]) @@ " ^
1.241 +" (Substitute [e2__])) B2__; " ^
1.242 +" (c_1_2__::bool list) = " ^
1.243 +" (SubProblem (Biegelinie_,[linear,system],[no_met]) " ^
1.244 +" [booll_ [B1__, B2__], reall [c,c_2]]); " ^
1.245 +" B__ = Take B__; " ^
1.246 +" B__ = ((Substitute c_1_2__) @@ " ^
1.247 +" (Rewrite_Set_Inst [(bdv, x)] make_ratpoly_in False)) B__ " ^
1.248 +" in B__)"
1.249 ));
1.250
1.251 store_met
1.252 - (prep_met Biegelinie.thy "met_biege_2" [] e_metID
1.253 + (prep_met (theory "Biegelinie") "met_biege_2" [] e_metID
1.254 (["IntegrierenUndKonstanteBestimmen2"],
1.255 [("#Given" ,["Traegerlaenge l_", "Streckenlast q__",
1.256 "FunktionsVariable v_"]),
1.257 @@ -270,28 +266,28 @@
1.258 Thm ("if_False",num_str if_False)
1.259 ],
1.260 prls = Erls, crls = Atools_erls, nrls = Erls},
1.261 -"Script Biegelinie2Script \
1.262 -\(l_::real) (q__::real) (v_::real) (b_::real=>real) (rb_::bool list) = \
1.263 -\ (let \
1.264 -\ (funs_:: bool list) = \
1.265 -\ (SubProblem (Biegelinie_,[vonBelastungZu,Biegelinien], \
1.266 -\ [Biegelinien,ausBelastung]) \
1.267 -\ [real_ q__, real_ v_]); \
1.268 -\ (equs_::bool list) = \
1.269 -\ (SubProblem (Biegelinie_,[setzeRandbedingungen,Biegelinien],\
1.270 -\ [Biegelinien,setzeRandbedingungenEin]) \
1.271 -\ [booll_ funs_, booll_ rb_]); \
1.272 -\ (cons_::bool list) = \
1.273 -\ (SubProblem (Biegelinie_,[linear,system],[no_met]) \
1.274 -\ [booll_ equs_, reall [c,c_2,c_3,c_4]]); \
1.275 -\ B_ = Take (lastI funs_); \
1.276 -\ B_ = ((Substitute cons_) @@ \
1.277 -\ (Rewrite_Set_Inst [(bdv, v_)] make_ratpoly_in False)) B_ \
1.278 -\ in B_)"
1.279 +"Script Biegelinie2Script " ^
1.280 +"(l_::real) (q__::real) (v_::real) (b_::real=>real) (rb_::bool list) = " ^
1.281 +" (let " ^
1.282 +" (funs_:: bool list) = " ^
1.283 +" (SubProblem (Biegelinie_,[vonBelastungZu,Biegelinien], " ^
1.284 +" [Biegelinien,ausBelastung]) " ^
1.285 +" [real_ q__, real_ v_]); " ^
1.286 +" (equs_::bool list) = " ^
1.287 +" (SubProblem (Biegelinie_,[setzeRandbedingungen,Biegelinien]," ^
1.288 +" [Biegelinien,setzeRandbedingungenEin]) " ^
1.289 +" [booll_ funs_, booll_ rb_]); " ^
1.290 +" (cons_::bool list) = " ^
1.291 +" (SubProblem (Biegelinie_,[linear,system],[no_met]) " ^
1.292 +" [booll_ equs_, reall [c,c_2,c_3,c_4]]); " ^
1.293 +" B_ = Take (lastI funs_); " ^
1.294 +" B_ = ((Substitute cons_) @@ " ^
1.295 +" (Rewrite_Set_Inst [(bdv, v_)] make_ratpoly_in False)) B_ " ^
1.296 +" in B_)"
1.297 ));
1.298
1.299 store_met
1.300 - (prep_met Biegelinie.thy "met_biege_intconst_2" [] e_metID
1.301 + (prep_met (theory "Biegelinie") "met_biege_intconst_2" [] e_metID
1.302 (["IntegrierenUndKonstanteBestimmen","2xIntegrieren"],
1.303 [],
1.304 {rew_ord'="tless_true", rls'=Erls, calc = [],
1.305 @@ -302,7 +298,7 @@
1.306 ));
1.307
1.308 store_met
1.309 - (prep_met Biegelinie.thy "met_biege_intconst_4" [] e_metID
1.310 + (prep_met (theory "Biegelinie") "met_biege_intconst_4" [] e_metID
1.311 (["IntegrierenUndKonstanteBestimmen","4x4System"],
1.312 [],
1.313 {rew_ord'="tless_true", rls'=Erls, calc = [],
1.314 @@ -313,7 +309,7 @@
1.315 ));
1.316
1.317 store_met
1.318 - (prep_met Biegelinie.thy "met_biege_intconst_1" [] e_metID
1.319 + (prep_met (theory "Biegelinie") "met_biege_intconst_1" [] e_metID
1.320 (["IntegrierenUndKonstanteBestimmen","1xIntegrieren"],
1.321 [],
1.322 {rew_ord'="tless_true", rls'=Erls, calc = [],
1.323 @@ -324,7 +320,7 @@
1.324 ));
1.325
1.326 store_met
1.327 - (prep_met Biegelinie.thy "met_biege2" [] e_metID
1.328 + (prep_met (theory "Biegelinie") "met_biege2" [] e_metID
1.329 (["Biegelinien"],
1.330 [],
1.331 {rew_ord'="tless_true", rls'=Erls, calc = [],
1.332 @@ -335,7 +331,7 @@
1.333 ));
1.334
1.335 store_met
1.336 - (prep_met Biegelinie.thy "met_biege_ausbelast" [] e_metID
1.337 + (prep_met (theory "Biegelinie") "met_biege_ausbelast" [] e_metID
1.338 (["Biegelinien","ausBelastung"],
1.339 [("#Given" ,["Streckenlast q__","FunktionsVariable v_"]),
1.340 ("#Find" ,["Funktionen funs_"])],
1.341 @@ -348,34 +344,34 @@
1.342 srls = append_rls "srls_ausBelastung" e_rls
1.343 [Calc("Tools.rhs", eval_rhs"eval_rhs_")],
1.344 prls = e_rls, crls = Atools_erls, nrls = e_rls},
1.345 -"Script Belastung2BiegelScript (q__::real) (v_::real) = \
1.346 -\ (let q___ = Take (q_ v_ = q__); \
1.347 -\ q___ = ((Rewrite sym_real_minus_eq_cancel True) @@ \
1.348 -\ (Rewrite Belastung_Querkraft True)) q___; \
1.349 -\ (Q__:: bool) = \
1.350 -\ (SubProblem (Biegelinie_,[named,integrate,function], \
1.351 -\ [diff,integration,named]) \
1.352 -\ [real_ (rhs q___), real_ v_, real_real_ Q]); \
1.353 -\ M__ = Rewrite Querkraft_Moment True Q__; \
1.354 -\ (M__::bool) = \
1.355 -\ (SubProblem (Biegelinie_,[named,integrate,function], \
1.356 -\ [diff,integration,named]) \
1.357 -\ [real_ (rhs M__), real_ v_, real_real_ M_b]); \
1.358 -\ N__ = ((Rewrite Moment_Neigung False) @@ \
1.359 -\ (Rewrite make_fun_explicit False)) M__; \
1.360 -\ (N__:: bool) = \
1.361 -\ (SubProblem (Biegelinie_,[named,integrate,function], \
1.362 -\ [diff,integration,named]) \
1.363 -\ [real_ (rhs N__), real_ v_, real_real_ y']); \
1.364 -\ (B__:: bool) = \
1.365 -\ (SubProblem (Biegelinie_,[named,integrate,function], \
1.366 -\ [diff,integration,named]) \
1.367 -\ [real_ (rhs N__), real_ v_, real_real_ y]) \
1.368 -\ in [Q__, M__, N__, B__])"
1.369 +"Script Belastung2BiegelScript (q__::real) (v_::real) = " ^
1.370 +" (let q___ = Take (q_ v_ = q__); " ^
1.371 +" q___ = ((Rewrite sym_real_minus_eq_cancel True) @@ " ^
1.372 +" (Rewrite Belastung_Querkraft True)) q___; " ^
1.373 +" (Q__:: bool) = " ^
1.374 +" (SubProblem (Biegelinie_,[named,integrate,function], " ^
1.375 +" [diff,integration,named]) " ^
1.376 +" [real_ (rhs q___), real_ v_, real_real_ Q]); " ^
1.377 +" M__ = Rewrite Querkraft_Moment True Q__; " ^
1.378 +" (M__::bool) = " ^
1.379 +" (SubProblem (Biegelinie_,[named,integrate,function], " ^
1.380 +" [diff,integration,named]) " ^
1.381 +" [real_ (rhs M__), real_ v_, real_real_ M_b]); " ^
1.382 +" N__ = ((Rewrite Moment_Neigung False) @@ " ^
1.383 +" (Rewrite make_fun_explicit False)) M__; " ^
1.384 +" (N__:: bool) = " ^
1.385 +" (SubProblem (Biegelinie_,[named,integrate,function], " ^
1.386 +" [diff,integration,named]) " ^
1.387 +" [real_ (rhs N__), real_ v_, real_real_ y']); " ^
1.388 +" (B__:: bool) = " ^
1.389 +" (SubProblem (Biegelinie_,[named,integrate,function], " ^
1.390 +" [diff,integration,named]) " ^
1.391 +" [real_ (rhs N__), real_ v_, real_real_ y]) " ^
1.392 +" in [Q__, M__, N__, B__])"
1.393 ));
1.394
1.395 store_met
1.396 - (prep_met Biegelinie.thy "met_biege_setzrand" [] e_metID
1.397 + (prep_met (theory "Biegelinie") "met_biege_setzrand" [] e_metID
1.398 (["Biegelinien","setzeRandbedingungenEin"],
1.399 [("#Given" ,["Funktionen funs_","Randbedingungen rb_"]),
1.400 ("#Find" ,["Gleichungen equs___"])],
1.401 @@ -383,63 +379,63 @@
1.402 srls = srls2,
1.403 prls=e_rls,
1.404 crls = Atools_erls, nrls = e_rls},
1.405 -"Script SetzeRandbedScript (funs_::bool list) (rb_::bool list) = \
1.406 -\ (let b1_ = nth_ 1 rb_; \
1.407 -\ fs_ = filter_sameFunId (lhs b1_) funs_; \
1.408 -\ (e1_::bool) = \
1.409 -\ (SubProblem (Biegelinie_,[makeFunctionTo,equation],\
1.410 -\ [Equation,fromFunction]) \
1.411 -\ [bool_ (hd fs_), bool_ b1_]); \
1.412 -\ b2_ = nth_ 2 rb_; \
1.413 -\ fs_ = filter_sameFunId (lhs b2_) funs_; \
1.414 -\ (e2_::bool) = \
1.415 -\ (SubProblem (Biegelinie_,[makeFunctionTo,equation],\
1.416 -\ [Equation,fromFunction]) \
1.417 -\ [bool_ (hd fs_), bool_ b2_]); \
1.418 -\ b3_ = nth_ 3 rb_; \
1.419 -\ fs_ = filter_sameFunId (lhs b3_) funs_; \
1.420 -\ (e3_::bool) = \
1.421 -\ (SubProblem (Biegelinie_,[makeFunctionTo,equation],\
1.422 -\ [Equation,fromFunction]) \
1.423 -\ [bool_ (hd fs_), bool_ b3_]); \
1.424 -\ b4_ = nth_ 4 rb_; \
1.425 -\ fs_ = filter_sameFunId (lhs b4_) funs_; \
1.426 -\ (e4_::bool) = \
1.427 -\ (SubProblem (Biegelinie_,[makeFunctionTo,equation],\
1.428 -\ [Equation,fromFunction]) \
1.429 -\ [bool_ (hd fs_), bool_ b4_]) \
1.430 -\ in [e1_,e2_,e3_,e4_])"
1.431 +"Script SetzeRandbedScript (funs_::bool list) (rb_::bool list) = " ^
1.432 +" (let b1_ = nth_ 1 rb_; " ^
1.433 +" fs_ = filter_sameFunId (lhs b1_) funs_; " ^
1.434 +" (e1_::bool) = " ^
1.435 +" (SubProblem (Biegelinie_,[makeFunctionTo,equation]," ^
1.436 +" [Equation,fromFunction]) " ^
1.437 +" [bool_ (hd fs_), bool_ b1_]); " ^
1.438 +" b2_ = nth_ 2 rb_; " ^
1.439 +" fs_ = filter_sameFunId (lhs b2_) funs_; " ^
1.440 +" (e2_::bool) = " ^
1.441 +" (SubProblem (Biegelinie_,[makeFunctionTo,equation]," ^
1.442 +" [Equation,fromFunction]) " ^
1.443 +" [bool_ (hd fs_), bool_ b2_]); " ^
1.444 +" b3_ = nth_ 3 rb_; " ^
1.445 +" fs_ = filter_sameFunId (lhs b3_) funs_; " ^
1.446 +" (e3_::bool) = " ^
1.447 +" (SubProblem (Biegelinie_,[makeFunctionTo,equation]," ^
1.448 +" [Equation,fromFunction]) " ^
1.449 +" [bool_ (hd fs_), bool_ b3_]); " ^
1.450 +" b4_ = nth_ 4 rb_; " ^
1.451 +" fs_ = filter_sameFunId (lhs b4_) funs_; " ^
1.452 +" (e4_::bool) = " ^
1.453 +" (SubProblem (Biegelinie_,[makeFunctionTo,equation]," ^
1.454 +" [Equation,fromFunction]) " ^
1.455 +" [bool_ (hd fs_), bool_ b4_]) " ^
1.456 +" in [e1_,e2_,e3_,e4_])"
1.457 (* filter requires more than 1 sec !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!
1.458 -"Script SetzeRandbedScript (funs_::bool list) (rb_::bool list) = \
1.459 -\ (let b1_ = nth_ 1 rb_; \
1.460 -\ fs_ = filter (sameFunId (lhs b1_)) funs_; \
1.461 -\ (e1_::bool) = \
1.462 -\ (SubProblem (Biegelinie_,[makeFunctionTo,equation],\
1.463 -\ [Equation,fromFunction]) \
1.464 -\ [bool_ (hd fs_), bool_ b1_]); \
1.465 -\ b2_ = nth_ 2 rb_; \
1.466 -\ fs_ = filter (sameFunId (lhs b2_)) funs_; \
1.467 -\ (e2_::bool) = \
1.468 -\ (SubProblem (Biegelinie_,[makeFunctionTo,equation],\
1.469 -\ [Equation,fromFunction]) \
1.470 -\ [bool_ (hd fs_), bool_ b2_]); \
1.471 -\ b3_ = nth_ 3 rb_; \
1.472 -\ fs_ = filter (sameFunId (lhs b3_)) funs_; \
1.473 -\ (e3_::bool) = \
1.474 -\ (SubProblem (Biegelinie_,[makeFunctionTo,equation],\
1.475 -\ [Equation,fromFunction]) \
1.476 -\ [bool_ (hd fs_), bool_ b3_]); \
1.477 -\ b4_ = nth_ 4 rb_; \
1.478 -\ fs_ = filter (sameFunId (lhs b4_)) funs_; \
1.479 -\ (e4_::bool) = \
1.480 -\ (SubProblem (Biegelinie_,[makeFunctionTo,equation],\
1.481 -\ [Equation,fromFunction]) \
1.482 -\ [bool_ (hd fs_), bool_ b4_]) \
1.483 -\ in [e1_,e2_,e3_,e4_])"*)
1.484 +"Script SetzeRandbedScript (funs_::bool list) (rb_::bool list) = " ^
1.485 +" (let b1_ = nth_ 1 rb_; " ^
1.486 +" fs_ = filter (sameFunId (lhs b1_)) funs_; " ^
1.487 +" (e1_::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 +" [Equation,fromFunction]) " ^
1.496 +" [bool_ (hd fs_), bool_ b2_]); " ^
1.497 +" b3_ = nth_ 3 rb_; " ^
1.498 +" fs_ = filter (sameFunId (lhs b3_)) funs_; " ^
1.499 +" (e3_::bool) = " ^
1.500 +" (SubProblem (Biegelinie_,[makeFunctionTo,equation]," ^
1.501 +" [Equation,fromFunction]) " ^
1.502 +" [bool_ (hd fs_), bool_ b3_]); " ^
1.503 +" b4_ = nth_ 4 rb_; " ^
1.504 +" fs_ = filter (sameFunId (lhs b4_)) funs_; " ^
1.505 +" (e4_::bool) = " ^
1.506 +" (SubProblem (Biegelinie_,[makeFunctionTo,equation]," ^
1.507 +" [Equation,fromFunction]) " ^
1.508 +" [bool_ (hd fs_), bool_ b4_]) " ^
1.509 +" in [e1_,e2_,e3_,e4_])"*)
1.510 ));
1.511
1.512 store_met
1.513 - (prep_met Biegelinie.thy "met_equ_fromfun" [] e_metID
1.514 + (prep_met (theory "Biegelinie") "met_equ_fromfun" [] e_metID
1.515 (["Equation","fromFunction"],
1.516 [("#Given" ,["functionEq fun_","substitution sub_"]),
1.517 ("#Find" ,["equality equ___"])],
1.518 @@ -453,16 +449,11 @@
1.519 crls = Atools_erls, nrls = e_rls},
1.520 (*(M_b x = c_2 + c * x + -1 * q_0 / 2 * x ^^^ 2) (M_b L = 0) -->
1.521 0 = c_2 + c * L + -1 * q_0 / 2 * L ^^^ 2*)
1.522 -"Script Function2Equality (fun_::bool) (sub_::bool) =\
1.523 -\ (let fun_ = Take fun_; \
1.524 -\ bdv_ = argument_in (lhs fun_); \
1.525 -\ val_ = argument_in (lhs sub_); \
1.526 -\ equ_ = (Substitute [bdv_ = val_]) fun_; \
1.527 -\ equ_ = (Substitute [sub_]) fun_ \
1.528 -\ in (Rewrite_Set norm_Rational False) equ_) "
1.529 +"Script Function2Equality (fun_::bool) (sub_::bool) =" ^
1.530 +" (let fun_ = Take fun_; " ^
1.531 +" bdv_ = argument_in (lhs fun_); " ^
1.532 +" val_ = argument_in (lhs sub_); " ^
1.533 +" equ_ = (Substitute [bdv_ = val_]) fun_; " ^
1.534 +" equ_ = (Substitute [sub_]) fun_ " ^
1.535 +" in (Rewrite_Set norm_Rational False) equ_) "
1.536 ));
1.537 -
1.538 -
1.539 -
1.540 -(* use"Knowledge/Biegelinie.ML";
1.541 - *)
1.542 \ No newline at end of file