1.1 --- a/src/Tools/isac/Knowledge/Biegelinie.ML Fri Aug 27 10:39:12 2010 +0200
1.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
1.3 @@ -1,459 +0,0 @@
1.4 -(* chapter 'Biegelinie' from the textbook:
1.5 - Timischl, Kaiser. Ingenieur-Mathematik 3. Wien 1999. p.268-271.
1.6 - authors: Walther Neuper 2005
1.7 - (c) due to copyright terms
1.8 -
1.9 -use"Knowledge/Biegelinie.ML";
1.10 -use"Biegelinie.ML";
1.11 -
1.12 -remove_thy"Typefix";
1.13 -remove_thy"Biegelinie";
1.14 -use_thy"Knowledge/Isac";
1.15 -*)
1.16 -
1.17 -(** interface isabelle -- isac **)
1.18 -
1.19 -theory' := overwritel (!theory', [("Biegelinie.thy",Biegelinie.thy)]);
1.20 -
1.21 -(** theory elements **)
1.22 -
1.23 -store_isa ["IsacKnowledge"] [];
1.24 -store_thy (theory "Biegelinie")
1.25 - ["Walther Neuper 2005 supported by a grant from NMI Austria"];
1.26 -store_isa ["IsacKnowledge", theory2thyID (theory "Biegelinie"), "Theorems"]
1.27 - ["Walther Neuper 2005 supported by a grant from NMI Austria"];
1.28 -store_thm (theory "Biegelinie") ("Belastung_Querkraft", Belastung_Querkraft)
1.29 - ["Walther Neuper 2005 supported by a grant from NMI Austria"];
1.30 -store_thm (theory "Biegelinie") ("Moment_Neigung", Moment_Neigung)
1.31 - ["Walther Neuper 2005 supported by a grant from NMI Austria"];
1.32 -store_thm (theory "Biegelinie") ("Moment_Querkraft", Moment_Querkraft)
1.33 - ["Walther Neuper 2005 supported by a grant from NMI Austria"];
1.34 -store_thm (theory "Biegelinie") ("Neigung_Moment", Neigung_Moment)
1.35 - ["Walther Neuper 2005 supported by a grant from NMI Austria"];
1.36 -store_thm (theory "Biegelinie") ("Querkraft_Belastung", Querkraft_Belastung)
1.37 - ["Walther Neuper 2005 supported by a grant from NMI Austria"];
1.38 -store_thm (theory "Biegelinie") ("Querkraft_Moment", Querkraft_Moment)
1.39 - ["Walther Neuper 2005 supported by a grant from NMI Austria"];
1.40 -store_thm (theory "Biegelinie") ("make_fun_explicit", make_fun_explicit)
1.41 - ["Walther Neuper 2005 supported by a grant from NMI Austria"];
1.42 -
1.43 -
1.44 -(** problems **)
1.45 -
1.46 -store_pbt
1.47 - (prep_pbt (theory "Biegelinie") "pbl_bieg" [] e_pblID
1.48 - (["Biegelinien"],
1.49 - [("#Given" ,["Traegerlaenge l_", "Streckenlast q__"]),
1.50 - (*("#Where",["0 < l_"]), ...wait for < and handling Arbfix*)
1.51 - ("#Find" ,["Biegelinie b_"]),
1.52 - ("#Relate",["Randbedingungen rb_"])
1.53 - ],
1.54 - append_rls "e_rls" e_rls [],
1.55 - NONE,
1.56 - [["IntegrierenUndKonstanteBestimmen2"]]));
1.57 -
1.58 -store_pbt
1.59 - (prep_pbt (theory "Biegelinie") "pbl_bieg_mom" [] e_pblID
1.60 - (["MomentBestimmte","Biegelinien"],
1.61 - [("#Given" ,["Traegerlaenge l_", "Streckenlast q__"]),
1.62 - (*("#Where",["0 < l_"]), ...wait for < and handling Arbfix*)
1.63 - ("#Find" ,["Biegelinie b_"]),
1.64 - ("#Relate",["RandbedingungenBiegung rb_","RandbedingungenMoment rm_"])
1.65 - ],
1.66 - append_rls "e_rls" e_rls [],
1.67 - NONE,
1.68 - [["IntegrierenUndKonstanteBestimmen"]]));
1.69 -
1.70 -store_pbt
1.71 - (prep_pbt (theory "Biegelinie") "pbl_bieg_momg" [] e_pblID
1.72 - (["MomentGegebene","Biegelinien"],
1.73 - [],
1.74 - append_rls "e_rls" e_rls [],
1.75 - NONE,
1.76 - [["IntegrierenUndKonstanteBestimmen","2xIntegrieren"]]));
1.77 -
1.78 -store_pbt
1.79 - (prep_pbt (theory "Biegelinie") "pbl_bieg_einf" [] e_pblID
1.80 - (["einfache","Biegelinien"],
1.81 - [],
1.82 - append_rls "e_rls" e_rls [],
1.83 - NONE,
1.84 - [["IntegrierenUndKonstanteBestimmen","4x4System"]]));
1.85 -
1.86 -store_pbt
1.87 - (prep_pbt (theory "Biegelinie") "pbl_bieg_momquer" [] e_pblID
1.88 - (["QuerkraftUndMomentBestimmte","Biegelinien"],
1.89 - [],
1.90 - append_rls "e_rls" e_rls [],
1.91 - NONE,
1.92 - [["IntegrierenUndKonstanteBestimmen","1xIntegrieren"]]));
1.93 -
1.94 -store_pbt
1.95 - (prep_pbt (theory "Biegelinie") "pbl_bieg_vonq" [] e_pblID
1.96 - (["vonBelastungZu","Biegelinien"],
1.97 - [("#Given" ,["Streckenlast q__","FunktionsVariable v_"]),
1.98 - ("#Find" ,["Funktionen funs___"])],
1.99 - append_rls "e_rls" e_rls [],
1.100 - NONE,
1.101 - [["Biegelinien","ausBelastung"]]));
1.102 -
1.103 -store_pbt
1.104 - (prep_pbt (theory "Biegelinie") "pbl_bieg_randbed" [] e_pblID
1.105 - (["setzeRandbedingungen","Biegelinien"],
1.106 - [("#Given" ,["Funktionen funs_","Randbedingungen rb_"]),
1.107 - ("#Find" ,["Gleichungen equs___"])],
1.108 - append_rls "e_rls" e_rls [],
1.109 - NONE,
1.110 - [["Biegelinien","setzeRandbedingungenEin"]]));
1.111 -
1.112 -store_pbt
1.113 - (prep_pbt (theory "Biegelinie") "pbl_equ_fromfun" [] e_pblID
1.114 - (["makeFunctionTo","equation"],
1.115 - [("#Given" ,["functionEq fun_","substitution sub_"]),
1.116 - ("#Find" ,["equality equ___"])],
1.117 - append_rls "e_rls" e_rls [],
1.118 - NONE,
1.119 - [["Equation","fromFunction"]]));
1.120 -
1.121 -
1.122 -(** methods **)
1.123 -
1.124 -val srls = Rls {id="srls_IntegrierenUnd..",
1.125 - preconds = [],
1.126 - rew_ord = ("termlessI",termlessI),
1.127 - erls = append_rls "erls_in_srls_IntegrierenUnd.." e_rls
1.128 - [(*for asm in nth_Cons_ ...*)
1.129 - Calc ("op <",eval_equ "#less_"),
1.130 - (*2nd nth_Cons_ pushes n+-1 into asms*)
1.131 - Calc("op +", eval_binop "#add_")
1.132 - ],
1.133 - srls = Erls, calc = [],
1.134 - rules = [Thm ("nth_Cons_",num_str nth_Cons_),
1.135 - Calc("op +", eval_binop "#add_"),
1.136 - Thm ("nth_Nil_",num_str nth_Nil_),
1.137 - Calc("Tools.lhs", eval_lhs"eval_lhs_"),
1.138 - Calc("Tools.rhs", eval_rhs"eval_rhs_"),
1.139 - Calc("Atools.argument'_in",
1.140 - eval_argument_in "Atools.argument'_in")
1.141 - ],
1.142 - scr = EmptyScr};
1.143 -
1.144 -val srls2 =
1.145 - Rls {id="srls_IntegrierenUnd..",
1.146 - preconds = [],
1.147 - rew_ord = ("termlessI",termlessI),
1.148 - erls = append_rls "erls_in_srls_IntegrierenUnd.." e_rls
1.149 - [(*for asm in nth_Cons_ ...*)
1.150 - Calc ("op <",eval_equ "#less_"),
1.151 - (*2nd nth_Cons_ pushes n+-1 into asms*)
1.152 - Calc("op +", eval_binop "#add_")
1.153 - ],
1.154 - srls = Erls, calc = [],
1.155 - rules = [Thm ("nth_Cons_",num_str nth_Cons_),
1.156 - Calc("op +", eval_binop "#add_"),
1.157 - Thm ("nth_Nil_", num_str nth_Nil_),
1.158 - Calc("Tools.lhs", eval_lhs "eval_lhs_"),
1.159 - Calc("Atools.filter'_sameFunId",
1.160 - eval_filter_sameFunId "Atools.filter'_sameFunId"),
1.161 - (*WN070514 just for smltest/../biegelinie.sml ...*)
1.162 - Calc("Atools.sameFunId", eval_sameFunId "Atools.sameFunId"),
1.163 - Thm ("filter_Cons", num_str filter_Cons),
1.164 - Thm ("filter_Nil", num_str filter_Nil),
1.165 - Thm ("if_True", num_str if_True),
1.166 - Thm ("if_False", num_str if_False),
1.167 - Thm ("hd_thm", num_str hd_thm)
1.168 - ],
1.169 - scr = EmptyScr};
1.170 -
1.171 -store_met
1.172 - (prep_met (theory "Biegelinie") "met_biege" [] e_metID
1.173 - (["IntegrierenUndKonstanteBestimmen"],
1.174 - [("#Given" ,["Traegerlaenge l_", "Streckenlast q__",
1.175 - "FunktionsVariable v_"]),
1.176 - (*("#Where",["0 < l_"]), ...wait for < and handling Arbfix*)
1.177 - ("#Find" ,["Biegelinie b_"]),
1.178 - ("#Relate",["RandbedingungenBiegung rb_",
1.179 - "RandbedingungenMoment rm_"])
1.180 - ],
1.181 - {rew_ord'="tless_true",
1.182 - rls' = append_rls "erls_IntegrierenUndK.." e_rls
1.183 - [Calc ("Atools.ident",eval_ident "#ident_"),
1.184 - Thm ("not_true",num_str not_true),
1.185 - Thm ("not_false",num_str not_false)],
1.186 - calc = [], srls = srls, prls = Erls,
1.187 - crls = Atools_erls, nrls = Erls},
1.188 -"Script BiegelinieScript " ^
1.189 -"(l_::real) (q__::real) (v_::real) (b_::real=>real) " ^
1.190 -"(rb_::bool list) (rm_::bool list) = " ^
1.191 -" (let q___ = Take (q_ v_ = q__); " ^
1.192 -" q___ = ((Rewrite sym_real_minus_eq_cancel True) @@ " ^
1.193 -" (Rewrite Belastung_Querkraft True)) q___; " ^
1.194 -" (Q__:: bool) = " ^
1.195 -" (SubProblem (Biegelinie_,[named,integrate,function], " ^
1.196 -" [diff,integration,named]) " ^
1.197 -" [real_ (rhs q___), real_ v_, real_real_ Q]); " ^
1.198 -" Q__ = Rewrite Querkraft_Moment True Q__; " ^
1.199 -" (M__::bool) = " ^
1.200 -" (SubProblem (Biegelinie_,[named,integrate,function], " ^
1.201 -" [diff,integration,named]) " ^
1.202 -" [real_ (rhs Q__), real_ v_, real_real_ M_b]); " ^
1.203 -" e1__ = nth_ 1 rm_; " ^
1.204 -" (x1__::real) = argument_in (lhs e1__); " ^
1.205 -" (M1__::bool) = (Substitute [v_ = x1__]) M__; " ^
1.206 -" M1__ = (Substitute [e1__]) M1__ ; " ^
1.207 -" M2__ = Take M__; " ^
1.208 -(*without this Take 'Substitute [v_ = x2__]' takes _last formula from ctree_*)
1.209 -" e2__ = nth_ 2 rm_; " ^
1.210 -" (x2__::real) = argument_in (lhs e2__); " ^
1.211 -" (M2__::bool) = ((Substitute [v_ = x2__]) @@ " ^
1.212 -" (Substitute [e2__])) M2__; " ^
1.213 -" (c_1_2__::bool list) = " ^
1.214 -" (SubProblem (Biegelinie_,[linear,system],[no_met]) " ^
1.215 -" [booll_ [M1__, M2__], reall [c,c_2]]); " ^
1.216 -" M__ = Take M__; " ^
1.217 -" M__ = ((Substitute c_1_2__) @@ " ^
1.218 -" (Try (Rewrite_Set_Inst [(bdv_1, c),(bdv_2, c_2)]" ^
1.219 -" simplify_System False)) @@ " ^
1.220 -" (Rewrite Moment_Neigung False) @@ " ^
1.221 -" (Rewrite make_fun_explicit False)) M__; " ^
1.222 -(*----------------------- and the same once more ------------------------*)
1.223 -" (N__:: bool) = " ^
1.224 -" (SubProblem (Biegelinie_,[named,integrate,function], " ^
1.225 -" [diff,integration,named]) " ^
1.226 -" [real_ (rhs M__), real_ v_, real_real_ y']); " ^
1.227 -" (B__:: bool) = " ^
1.228 -" (SubProblem (Biegelinie_,[named,integrate,function], " ^
1.229 -" [diff,integration,named]) " ^
1.230 -" [real_ (rhs N__), real_ v_, real_real_ y]); " ^
1.231 -" e1__ = nth_ 1 rb_; " ^
1.232 -" (x1__::real) = argument_in (lhs e1__); " ^
1.233 -" (B1__::bool) = (Substitute [v_ = x1__]) B__; " ^
1.234 -" B1__ = (Substitute [e1__]) B1__ ; " ^
1.235 -" B2__ = Take B__; " ^
1.236 -" e2__ = nth_ 2 rb_; " ^
1.237 -" (x2__::real) = argument_in (lhs e2__); " ^
1.238 -" (B2__::bool) = ((Substitute [v_ = x2__]) @@ " ^
1.239 -" (Substitute [e2__])) B2__; " ^
1.240 -" (c_1_2__::bool list) = " ^
1.241 -" (SubProblem (Biegelinie_,[linear,system],[no_met]) " ^
1.242 -" [booll_ [B1__, B2__], reall [c,c_2]]); " ^
1.243 -" B__ = Take B__; " ^
1.244 -" B__ = ((Substitute c_1_2__) @@ " ^
1.245 -" (Rewrite_Set_Inst [(bdv, x)] make_ratpoly_in False)) B__ " ^
1.246 -" in B__)"
1.247 -));
1.248 -
1.249 -store_met
1.250 - (prep_met (theory "Biegelinie") "met_biege_2" [] e_metID
1.251 - (["IntegrierenUndKonstanteBestimmen2"],
1.252 - [("#Given" ,["Traegerlaenge l_", "Streckenlast q__",
1.253 - "FunktionsVariable v_"]),
1.254 - (*("#Where",["0 < l_"]), ...wait for < and handling Arbfix*)
1.255 - ("#Find" ,["Biegelinie b_"]),
1.256 - ("#Relate",["Randbedingungen rb_"])
1.257 - ],
1.258 - {rew_ord'="tless_true",
1.259 - rls' = append_rls "erls_IntegrierenUndK.." e_rls
1.260 - [Calc ("Atools.ident",eval_ident "#ident_"),
1.261 - Thm ("not_true",num_str not_true),
1.262 - Thm ("not_false",num_str not_false)],
1.263 - calc = [],
1.264 - srls = append_rls "erls_IntegrierenUndK.." e_rls
1.265 - [Calc("Tools.rhs", eval_rhs"eval_rhs_"),
1.266 - Calc ("Atools.ident",eval_ident "#ident_"),
1.267 - Thm ("last_thmI",num_str last_thmI),
1.268 - Thm ("if_True",num_str if_True),
1.269 - Thm ("if_False",num_str if_False)
1.270 - ],
1.271 - prls = Erls, crls = Atools_erls, nrls = Erls},
1.272 -"Script Biegelinie2Script " ^
1.273 -"(l_::real) (q__::real) (v_::real) (b_::real=>real) (rb_::bool list) = " ^
1.274 -" (let " ^
1.275 -" (funs_:: bool list) = " ^
1.276 -" (SubProblem (Biegelinie_,[vonBelastungZu,Biegelinien], " ^
1.277 -" [Biegelinien,ausBelastung]) " ^
1.278 -" [real_ q__, real_ v_]); " ^
1.279 -" (equs_::bool list) = " ^
1.280 -" (SubProblem (Biegelinie_,[setzeRandbedingungen,Biegelinien]," ^
1.281 -" [Biegelinien,setzeRandbedingungenEin]) " ^
1.282 -" [booll_ funs_, booll_ rb_]); " ^
1.283 -" (cons_::bool list) = " ^
1.284 -" (SubProblem (Biegelinie_,[linear,system],[no_met]) " ^
1.285 -" [booll_ equs_, reall [c,c_2,c_3,c_4]]); " ^
1.286 -" B_ = Take (lastI funs_); " ^
1.287 -" B_ = ((Substitute cons_) @@ " ^
1.288 -" (Rewrite_Set_Inst [(bdv, v_)] make_ratpoly_in False)) B_ " ^
1.289 -" in B_)"
1.290 -));
1.291 -
1.292 -store_met
1.293 - (prep_met (theory "Biegelinie") "met_biege_intconst_2" [] e_metID
1.294 - (["IntegrierenUndKonstanteBestimmen","2xIntegrieren"],
1.295 - [],
1.296 - {rew_ord'="tless_true", rls'=Erls, calc = [],
1.297 - srls = e_rls,
1.298 - prls=e_rls,
1.299 - crls = Atools_erls, nrls = e_rls},
1.300 -"empty_script"
1.301 -));
1.302 -
1.303 -store_met
1.304 - (prep_met (theory "Biegelinie") "met_biege_intconst_4" [] e_metID
1.305 - (["IntegrierenUndKonstanteBestimmen","4x4System"],
1.306 - [],
1.307 - {rew_ord'="tless_true", rls'=Erls, calc = [],
1.308 - srls = e_rls,
1.309 - prls=e_rls,
1.310 - crls = Atools_erls, nrls = e_rls},
1.311 -"empty_script"
1.312 -));
1.313 -
1.314 -store_met
1.315 - (prep_met (theory "Biegelinie") "met_biege_intconst_1" [] e_metID
1.316 - (["IntegrierenUndKonstanteBestimmen","1xIntegrieren"],
1.317 - [],
1.318 - {rew_ord'="tless_true", rls'=Erls, calc = [],
1.319 - srls = e_rls,
1.320 - prls=e_rls,
1.321 - crls = Atools_erls, nrls = e_rls},
1.322 -"empty_script"
1.323 -));
1.324 -
1.325 -store_met
1.326 - (prep_met (theory "Biegelinie") "met_biege2" [] e_metID
1.327 - (["Biegelinien"],
1.328 - [],
1.329 - {rew_ord'="tless_true", rls'=Erls, calc = [],
1.330 - srls = e_rls,
1.331 - prls=e_rls,
1.332 - crls = Atools_erls, nrls = e_rls},
1.333 -"empty_script"
1.334 -));
1.335 -
1.336 -store_met
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 - {rew_ord'="tless_true",
1.342 - rls' = append_rls "erls_ausBelastung" e_rls
1.343 - [Calc ("Atools.ident",eval_ident "#ident_"),
1.344 - Thm ("not_true",num_str not_true),
1.345 - Thm ("not_false",num_str not_false)],
1.346 - calc = [],
1.347 - srls = append_rls "srls_ausBelastung" e_rls
1.348 - [Calc("Tools.rhs", eval_rhs"eval_rhs_")],
1.349 - prls = e_rls, crls = Atools_erls, nrls = e_rls},
1.350 -"Script Belastung2BiegelScript (q__::real) (v_::real) = " ^
1.351 -" (let q___ = Take (q_ v_ = q__); " ^
1.352 -" q___ = ((Rewrite sym_real_minus_eq_cancel True) @@ " ^
1.353 -" (Rewrite Belastung_Querkraft True)) q___; " ^
1.354 -" (Q__:: bool) = " ^
1.355 -" (SubProblem (Biegelinie_,[named,integrate,function], " ^
1.356 -" [diff,integration,named]) " ^
1.357 -" [real_ (rhs q___), real_ v_, real_real_ Q]); " ^
1.358 -" M__ = Rewrite Querkraft_Moment True Q__; " ^
1.359 -" (M__::bool) = " ^
1.360 -" (SubProblem (Biegelinie_,[named,integrate,function], " ^
1.361 -" [diff,integration,named]) " ^
1.362 -" [real_ (rhs M__), real_ v_, real_real_ M_b]); " ^
1.363 -" N__ = ((Rewrite Moment_Neigung False) @@ " ^
1.364 -" (Rewrite make_fun_explicit False)) M__; " ^
1.365 -" (N__:: bool) = " ^
1.366 -" (SubProblem (Biegelinie_,[named,integrate,function], " ^
1.367 -" [diff,integration,named]) " ^
1.368 -" [real_ (rhs N__), real_ v_, real_real_ y']); " ^
1.369 -" (B__:: bool) = " ^
1.370 -" (SubProblem (Biegelinie_,[named,integrate,function], " ^
1.371 -" [diff,integration,named]) " ^
1.372 -" [real_ (rhs N__), real_ v_, real_real_ y]) " ^
1.373 -" in [Q__, M__, N__, B__])"
1.374 -));
1.375 -
1.376 -store_met
1.377 - (prep_met (theory "Biegelinie") "met_biege_setzrand" [] e_metID
1.378 - (["Biegelinien","setzeRandbedingungenEin"],
1.379 - [("#Given" ,["Funktionen funs_","Randbedingungen rb_"]),
1.380 - ("#Find" ,["Gleichungen equs___"])],
1.381 - {rew_ord'="tless_true", rls'=Erls, calc = [],
1.382 - srls = srls2,
1.383 - prls=e_rls,
1.384 - crls = Atools_erls, nrls = e_rls},
1.385 -"Script SetzeRandbedScript (funs_::bool list) (rb_::bool list) = " ^
1.386 -" (let b1_ = nth_ 1 rb_; " ^
1.387 -" fs_ = filter_sameFunId (lhs b1_) funs_; " ^
1.388 -" (e1_::bool) = " ^
1.389 -" (SubProblem (Biegelinie_,[makeFunctionTo,equation]," ^
1.390 -" [Equation,fromFunction]) " ^
1.391 -" [bool_ (hd fs_), bool_ b1_]); " ^
1.392 -" b2_ = nth_ 2 rb_; " ^
1.393 -" fs_ = filter_sameFunId (lhs b2_) funs_; " ^
1.394 -" (e2_::bool) = " ^
1.395 -" (SubProblem (Biegelinie_,[makeFunctionTo,equation]," ^
1.396 -" [Equation,fromFunction]) " ^
1.397 -" [bool_ (hd fs_), bool_ b2_]); " ^
1.398 -" b3_ = nth_ 3 rb_; " ^
1.399 -" fs_ = filter_sameFunId (lhs b3_) funs_; " ^
1.400 -" (e3_::bool) = " ^
1.401 -" (SubProblem (Biegelinie_,[makeFunctionTo,equation]," ^
1.402 -" [Equation,fromFunction]) " ^
1.403 -" [bool_ (hd fs_), bool_ b3_]); " ^
1.404 -" b4_ = nth_ 4 rb_; " ^
1.405 -" fs_ = filter_sameFunId (lhs b4_) funs_; " ^
1.406 -" (e4_::bool) = " ^
1.407 -" (SubProblem (Biegelinie_,[makeFunctionTo,equation]," ^
1.408 -" [Equation,fromFunction]) " ^
1.409 -" [bool_ (hd fs_), bool_ b4_]) " ^
1.410 -" in [e1_,e2_,e3_,e4_])"
1.411 -(* filter requires more than 1 sec !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!
1.412 -"Script SetzeRandbedScript (funs_::bool list) (rb_::bool list) = " ^
1.413 -" (let b1_ = nth_ 1 rb_; " ^
1.414 -" fs_ = filter (sameFunId (lhs b1_)) funs_; " ^
1.415 -" (e1_::bool) = " ^
1.416 -" (SubProblem (Biegelinie_,[makeFunctionTo,equation]," ^
1.417 -" [Equation,fromFunction]) " ^
1.418 -" [bool_ (hd fs_), bool_ b1_]); " ^
1.419 -" b2_ = nth_ 2 rb_; " ^
1.420 -" fs_ = filter (sameFunId (lhs b2_)) funs_; " ^
1.421 -" (e2_::bool) = " ^
1.422 -" (SubProblem (Biegelinie_,[makeFunctionTo,equation]," ^
1.423 -" [Equation,fromFunction]) " ^
1.424 -" [bool_ (hd fs_), bool_ b2_]); " ^
1.425 -" b3_ = nth_ 3 rb_; " ^
1.426 -" fs_ = filter (sameFunId (lhs b3_)) funs_; " ^
1.427 -" (e3_::bool) = " ^
1.428 -" (SubProblem (Biegelinie_,[makeFunctionTo,equation]," ^
1.429 -" [Equation,fromFunction]) " ^
1.430 -" [bool_ (hd fs_), bool_ b3_]); " ^
1.431 -" b4_ = nth_ 4 rb_; " ^
1.432 -" fs_ = filter (sameFunId (lhs b4_)) funs_; " ^
1.433 -" (e4_::bool) = " ^
1.434 -" (SubProblem (Biegelinie_,[makeFunctionTo,equation]," ^
1.435 -" [Equation,fromFunction]) " ^
1.436 -" [bool_ (hd fs_), bool_ b4_]) " ^
1.437 -" in [e1_,e2_,e3_,e4_])"*)
1.438 -));
1.439 -
1.440 -store_met
1.441 - (prep_met (theory "Biegelinie") "met_equ_fromfun" [] e_metID
1.442 - (["Equation","fromFunction"],
1.443 - [("#Given" ,["functionEq fun_","substitution sub_"]),
1.444 - ("#Find" ,["equality equ___"])],
1.445 - {rew_ord'="tless_true", rls'=Erls, calc = [],
1.446 - srls = append_rls "srls_in_EquationfromFunc" e_rls
1.447 - [Calc("Tools.lhs", eval_lhs"eval_lhs_"),
1.448 - Calc("Atools.argument'_in",
1.449 - eval_argument_in
1.450 - "Atools.argument'_in")],
1.451 - prls=e_rls,
1.452 - crls = Atools_erls, nrls = e_rls},
1.453 -(*(M_b x = c_2 + c * x + -1 * q_0 / 2 * x ^^^ 2) (M_b L = 0) -->
1.454 - 0 = c_2 + c * L + -1 * q_0 / 2 * L ^^^ 2*)
1.455 -"Script Function2Equality (fun_::bool) (sub_::bool) =" ^
1.456 -" (let fun_ = Take fun_; " ^
1.457 -" bdv_ = argument_in (lhs fun_); " ^
1.458 -" val_ = argument_in (lhs sub_); " ^
1.459 -" equ_ = (Substitute [bdv_ = val_]) fun_; " ^
1.460 -" equ_ = (Substitute [sub_]) fun_ " ^
1.461 -" in (Rewrite_Set norm_Rational False) equ_) "
1.462 -));