1.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
1.2 +++ b/src/Tools/isac/Knowledge/Biegelinie.ML Wed Aug 25 16:20:07 2010 +0200
1.3 @@ -0,0 +1,468 @@
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 Biegelinie.thy
1.25 + ["Walther Neuper 2005 supported by a grant from NMI Austria"];
1.26 +store_isa ["IsacKnowledge", theory2thyID Biegelinie.thy, "Theorems"]
1.27 + ["Walther Neuper 2005 supported by a grant from NMI Austria"];
1.28 +store_thm Biegelinie.thy ("Belastung_Querkraft", Belastung_Querkraft)
1.29 + ["Walther Neuper 2005 supported by a grant from NMI Austria"];
1.30 +store_thm Biegelinie.thy ("Moment_Neigung", Moment_Neigung)
1.31 + ["Walther Neuper 2005 supported by a grant from NMI Austria"];
1.32 +store_thm Biegelinie.thy ("Moment_Querkraft", Moment_Querkraft)
1.33 + ["Walther Neuper 2005 supported by a grant from NMI Austria"];
1.34 +store_thm Biegelinie.thy ("Neigung_Moment", Neigung_Moment)
1.35 + ["Walther Neuper 2005 supported by a grant from NMI Austria"];
1.36 +store_thm Biegelinie.thy ("Querkraft_Belastung", Querkraft_Belastung)
1.37 + ["Walther Neuper 2005 supported by a grant from NMI Austria"];
1.38 +store_thm Biegelinie.thy ("Querkraft_Moment", Querkraft_Moment)
1.39 + ["Walther Neuper 2005 supported by a grant from NMI Austria"];
1.40 +store_thm Biegelinie.thy ("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 Biegelinie.thy "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 Biegelinie.thy "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 Biegelinie.thy "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 Biegelinie.thy "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 Biegelinie.thy "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 Biegelinie.thy "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 Biegelinie.thy "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 Biegelinie.thy "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 +
1.123 +(** methods **)
1.124 +
1.125 +val srls = Rls {id="srls_IntegrierenUnd..",
1.126 + preconds = [],
1.127 + rew_ord = ("termlessI",termlessI),
1.128 + erls = append_rls "erls_in_srls_IntegrierenUnd.." e_rls
1.129 + [(*for asm in nth_Cons_ ...*)
1.130 + Calc ("op <",eval_equ "#less_"),
1.131 + (*2nd nth_Cons_ pushes n+-1 into asms*)
1.132 + Calc("op +", eval_binop "#add_")
1.133 + ],
1.134 + srls = Erls, calc = [],
1.135 + rules = [Thm ("nth_Cons_",num_str nth_Cons_),
1.136 + Calc("op +", eval_binop "#add_"),
1.137 + Thm ("nth_Nil_",num_str nth_Nil_),
1.138 + Calc("Tools.lhs", eval_lhs"eval_lhs_"),
1.139 + Calc("Tools.rhs", eval_rhs"eval_rhs_"),
1.140 + Calc("Atools.argument'_in",
1.141 + eval_argument_in "Atools.argument'_in")
1.142 + ],
1.143 + scr = EmptyScr};
1.144 +
1.145 +val srls2 =
1.146 + Rls {id="srls_IntegrierenUnd..",
1.147 + preconds = [],
1.148 + rew_ord = ("termlessI",termlessI),
1.149 + erls = append_rls "erls_in_srls_IntegrierenUnd.." e_rls
1.150 + [(*for asm in nth_Cons_ ...*)
1.151 + Calc ("op <",eval_equ "#less_"),
1.152 + (*2nd nth_Cons_ pushes n+-1 into asms*)
1.153 + Calc("op +", eval_binop "#add_")
1.154 + ],
1.155 + srls = Erls, calc = [],
1.156 + rules = [Thm ("nth_Cons_",num_str nth_Cons_),
1.157 + Calc("op +", eval_binop "#add_"),
1.158 + Thm ("nth_Nil_", num_str nth_Nil_),
1.159 + Calc("Tools.lhs", eval_lhs "eval_lhs_"),
1.160 + Calc("Atools.filter'_sameFunId",
1.161 + eval_filter_sameFunId "Atools.filter'_sameFunId"),
1.162 + (*WN070514 just for smltest/../biegelinie.sml ...*)
1.163 + Calc("Atools.sameFunId", eval_sameFunId "Atools.sameFunId"),
1.164 + Thm ("filter_Cons", num_str filter_Cons),
1.165 + Thm ("filter_Nil", num_str filter_Nil),
1.166 + Thm ("if_True", num_str if_True),
1.167 + Thm ("if_False", num_str if_False),
1.168 + Thm ("hd_thm", num_str hd_thm)
1.169 + ],
1.170 + scr = EmptyScr};
1.171 +(*@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@*)
1.172 +(* use"Knowledge/Biegelinie.ML";
1.173 + *)
1.174 +
1.175 +store_met
1.176 + (prep_met Biegelinie.thy "met_biege" [] e_metID
1.177 + (["IntegrierenUndKonstanteBestimmen"],
1.178 + [("#Given" ,["Traegerlaenge l_", "Streckenlast q__",
1.179 + "FunktionsVariable v_"]),
1.180 + (*("#Where",["0 < l_"]), ...wait for < and handling Arbfix*)
1.181 + ("#Find" ,["Biegelinie b_"]),
1.182 + ("#Relate",["RandbedingungenBiegung rb_",
1.183 + "RandbedingungenMoment rm_"])
1.184 + ],
1.185 + {rew_ord'="tless_true",
1.186 + rls' = append_rls "erls_IntegrierenUndK.." e_rls
1.187 + [Calc ("Atools.ident",eval_ident "#ident_"),
1.188 + Thm ("not_true",num_str not_true),
1.189 + Thm ("not_false",num_str not_false)],
1.190 + calc = [], srls = srls, prls = Erls,
1.191 + crls = Atools_erls, nrls = Erls},
1.192 +"Script BiegelinieScript \
1.193 +\(l_::real) (q__::real) (v_::real) (b_::real=>real) \
1.194 +\(rb_::bool list) (rm_::bool list) = \
1.195 +\ (let q___ = Take (q_ v_ = q__); \
1.196 +\ q___ = ((Rewrite sym_real_minus_eq_cancel True) @@ \
1.197 +\ (Rewrite Belastung_Querkraft True)) q___; \
1.198 +\ (Q__:: bool) = \
1.199 +\ (SubProblem (Biegelinie_,[named,integrate,function], \
1.200 +\ [diff,integration,named]) \
1.201 +\ [real_ (rhs q___), real_ v_, real_real_ Q]); \
1.202 +\ Q__ = Rewrite Querkraft_Moment True Q__; \
1.203 +\ (M__::bool) = \
1.204 +\ (SubProblem (Biegelinie_,[named,integrate,function], \
1.205 +\ [diff,integration,named]) \
1.206 +\ [real_ (rhs Q__), real_ v_, real_real_ M_b]); \
1.207 +\ e1__ = nth_ 1 rm_; \
1.208 +\ (x1__::real) = argument_in (lhs e1__); \
1.209 +\ (M1__::bool) = (Substitute [v_ = x1__]) M__; \
1.210 +\ M1__ = (Substitute [e1__]) M1__ ; \
1.211 +\ M2__ = Take M__; "^
1.212 +(*without this Take 'Substitute [v_ = x2__]' takes _last formula from ctree_*)
1.213 +" e2__ = nth_ 2 rm_; \
1.214 +\ (x2__::real) = argument_in (lhs e2__); \
1.215 +\ (M2__::bool) = ((Substitute [v_ = x2__]) @@ \
1.216 +\ (Substitute [e2__])) M2__; \
1.217 +\ (c_1_2__::bool list) = \
1.218 +\ (SubProblem (Biegelinie_,[linear,system],[no_met]) \
1.219 +\ [booll_ [M1__, M2__], reall [c,c_2]]); \
1.220 +\ M__ = Take M__; \
1.221 +\ M__ = ((Substitute c_1_2__) @@ \
1.222 +\ (Try (Rewrite_Set_Inst [(bdv_1, c),(bdv_2, c_2)]\
1.223 +\ simplify_System False)) @@ \
1.224 +\ (Rewrite Moment_Neigung False) @@ \
1.225 +\ (Rewrite make_fun_explicit False)) M__; "^
1.226 +(*----------------------- and the same once more ------------------------*)
1.227 +" (N__:: bool) = \
1.228 +\ (SubProblem (Biegelinie_,[named,integrate,function], \
1.229 +\ [diff,integration,named]) \
1.230 +\ [real_ (rhs M__), real_ v_, real_real_ y']); \
1.231 +\ (B__:: bool) = \
1.232 +\ (SubProblem (Biegelinie_,[named,integrate,function], \
1.233 +\ [diff,integration,named]) \
1.234 +\ [real_ (rhs N__), real_ v_, real_real_ y]); \
1.235 +\ e1__ = nth_ 1 rb_; \
1.236 +\ (x1__::real) = argument_in (lhs e1__); \
1.237 +\ (B1__::bool) = (Substitute [v_ = x1__]) B__; \
1.238 +\ B1__ = (Substitute [e1__]) B1__ ; \
1.239 +\ B2__ = Take B__; \
1.240 +\ e2__ = nth_ 2 rb_; \
1.241 +\ (x2__::real) = argument_in (lhs e2__); \
1.242 +\ (B2__::bool) = ((Substitute [v_ = x2__]) @@ \
1.243 +\ (Substitute [e2__])) B2__; \
1.244 +\ (c_1_2__::bool list) = \
1.245 +\ (SubProblem (Biegelinie_,[linear,system],[no_met]) \
1.246 +\ [booll_ [B1__, B2__], reall [c,c_2]]); \
1.247 +\ B__ = Take B__; \
1.248 +\ B__ = ((Substitute c_1_2__) @@ \
1.249 +\ (Rewrite_Set_Inst [(bdv, x)] make_ratpoly_in False)) B__ \
1.250 +\ in B__)"
1.251 +));
1.252 +
1.253 +store_met
1.254 + (prep_met Biegelinie.thy "met_biege_2" [] e_metID
1.255 + (["IntegrierenUndKonstanteBestimmen2"],
1.256 + [("#Given" ,["Traegerlaenge l_", "Streckenlast q__",
1.257 + "FunktionsVariable v_"]),
1.258 + (*("#Where",["0 < l_"]), ...wait for < and handling Arbfix*)
1.259 + ("#Find" ,["Biegelinie b_"]),
1.260 + ("#Relate",["Randbedingungen rb_"])
1.261 + ],
1.262 + {rew_ord'="tless_true",
1.263 + rls' = append_rls "erls_IntegrierenUndK.." e_rls
1.264 + [Calc ("Atools.ident",eval_ident "#ident_"),
1.265 + Thm ("not_true",num_str not_true),
1.266 + Thm ("not_false",num_str not_false)],
1.267 + calc = [],
1.268 + srls = append_rls "erls_IntegrierenUndK.." e_rls
1.269 + [Calc("Tools.rhs", eval_rhs"eval_rhs_"),
1.270 + Calc ("Atools.ident",eval_ident "#ident_"),
1.271 + Thm ("last_thmI",num_str last_thmI),
1.272 + Thm ("if_True",num_str if_True),
1.273 + Thm ("if_False",num_str if_False)
1.274 + ],
1.275 + prls = Erls, crls = Atools_erls, nrls = Erls},
1.276 +"Script Biegelinie2Script \
1.277 +\(l_::real) (q__::real) (v_::real) (b_::real=>real) (rb_::bool list) = \
1.278 +\ (let \
1.279 +\ (funs_:: bool list) = \
1.280 +\ (SubProblem (Biegelinie_,[vonBelastungZu,Biegelinien], \
1.281 +\ [Biegelinien,ausBelastung]) \
1.282 +\ [real_ q__, real_ v_]); \
1.283 +\ (equs_::bool list) = \
1.284 +\ (SubProblem (Biegelinie_,[setzeRandbedingungen,Biegelinien],\
1.285 +\ [Biegelinien,setzeRandbedingungenEin]) \
1.286 +\ [booll_ funs_, booll_ rb_]); \
1.287 +\ (cons_::bool list) = \
1.288 +\ (SubProblem (Biegelinie_,[linear,system],[no_met]) \
1.289 +\ [booll_ equs_, reall [c,c_2,c_3,c_4]]); \
1.290 +\ B_ = Take (lastI funs_); \
1.291 +\ B_ = ((Substitute cons_) @@ \
1.292 +\ (Rewrite_Set_Inst [(bdv, v_)] make_ratpoly_in False)) B_ \
1.293 +\ in B_)"
1.294 +));
1.295 +
1.296 +store_met
1.297 + (prep_met Biegelinie.thy "met_biege_intconst_2" [] e_metID
1.298 + (["IntegrierenUndKonstanteBestimmen","2xIntegrieren"],
1.299 + [],
1.300 + {rew_ord'="tless_true", rls'=Erls, calc = [],
1.301 + srls = e_rls,
1.302 + prls=e_rls,
1.303 + crls = Atools_erls, nrls = e_rls},
1.304 +"empty_script"
1.305 +));
1.306 +
1.307 +store_met
1.308 + (prep_met Biegelinie.thy "met_biege_intconst_4" [] e_metID
1.309 + (["IntegrierenUndKonstanteBestimmen","4x4System"],
1.310 + [],
1.311 + {rew_ord'="tless_true", rls'=Erls, calc = [],
1.312 + srls = e_rls,
1.313 + prls=e_rls,
1.314 + crls = Atools_erls, nrls = e_rls},
1.315 +"empty_script"
1.316 +));
1.317 +
1.318 +store_met
1.319 + (prep_met Biegelinie.thy "met_biege_intconst_1" [] e_metID
1.320 + (["IntegrierenUndKonstanteBestimmen","1xIntegrieren"],
1.321 + [],
1.322 + {rew_ord'="tless_true", rls'=Erls, calc = [],
1.323 + srls = e_rls,
1.324 + prls=e_rls,
1.325 + crls = Atools_erls, nrls = e_rls},
1.326 +"empty_script"
1.327 +));
1.328 +
1.329 +store_met
1.330 + (prep_met Biegelinie.thy "met_biege2" [] e_metID
1.331 + (["Biegelinien"],
1.332 + [],
1.333 + {rew_ord'="tless_true", rls'=Erls, calc = [],
1.334 + srls = e_rls,
1.335 + prls=e_rls,
1.336 + crls = Atools_erls, nrls = e_rls},
1.337 +"empty_script"
1.338 +));
1.339 +
1.340 +store_met
1.341 + (prep_met Biegelinie.thy "met_biege_ausbelast" [] e_metID
1.342 + (["Biegelinien","ausBelastung"],
1.343 + [("#Given" ,["Streckenlast q__","FunktionsVariable v_"]),
1.344 + ("#Find" ,["Funktionen funs_"])],
1.345 + {rew_ord'="tless_true",
1.346 + rls' = append_rls "erls_ausBelastung" e_rls
1.347 + [Calc ("Atools.ident",eval_ident "#ident_"),
1.348 + Thm ("not_true",num_str not_true),
1.349 + Thm ("not_false",num_str not_false)],
1.350 + calc = [],
1.351 + srls = append_rls "srls_ausBelastung" e_rls
1.352 + [Calc("Tools.rhs", eval_rhs"eval_rhs_")],
1.353 + prls = e_rls, crls = Atools_erls, nrls = e_rls},
1.354 +"Script Belastung2BiegelScript (q__::real) (v_::real) = \
1.355 +\ (let q___ = Take (q_ v_ = q__); \
1.356 +\ q___ = ((Rewrite sym_real_minus_eq_cancel True) @@ \
1.357 +\ (Rewrite Belastung_Querkraft True)) q___; \
1.358 +\ (Q__:: bool) = \
1.359 +\ (SubProblem (Biegelinie_,[named,integrate,function], \
1.360 +\ [diff,integration,named]) \
1.361 +\ [real_ (rhs q___), real_ v_, real_real_ Q]); \
1.362 +\ M__ = Rewrite Querkraft_Moment True Q__; \
1.363 +\ (M__::bool) = \
1.364 +\ (SubProblem (Biegelinie_,[named,integrate,function], \
1.365 +\ [diff,integration,named]) \
1.366 +\ [real_ (rhs M__), real_ v_, real_real_ M_b]); \
1.367 +\ N__ = ((Rewrite Moment_Neigung False) @@ \
1.368 +\ (Rewrite make_fun_explicit False)) M__; \
1.369 +\ (N__:: 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 +\ (B__:: bool) = \
1.374 +\ (SubProblem (Biegelinie_,[named,integrate,function], \
1.375 +\ [diff,integration,named]) \
1.376 +\ [real_ (rhs N__), real_ v_, real_real_ y]) \
1.377 +\ in [Q__, M__, N__, B__])"
1.378 +));
1.379 +
1.380 +store_met
1.381 + (prep_met Biegelinie.thy "met_biege_setzrand" [] e_metID
1.382 + (["Biegelinien","setzeRandbedingungenEin"],
1.383 + [("#Given" ,["Funktionen funs_","Randbedingungen rb_"]),
1.384 + ("#Find" ,["Gleichungen equs___"])],
1.385 + {rew_ord'="tless_true", rls'=Erls, calc = [],
1.386 + srls = srls2,
1.387 + prls=e_rls,
1.388 + crls = Atools_erls, nrls = e_rls},
1.389 +"Script SetzeRandbedScript (funs_::bool list) (rb_::bool list) = \
1.390 +\ (let b1_ = nth_ 1 rb_; \
1.391 +\ fs_ = filter_sameFunId (lhs b1_) funs_; \
1.392 +\ (e1_::bool) = \
1.393 +\ (SubProblem (Biegelinie_,[makeFunctionTo,equation],\
1.394 +\ [Equation,fromFunction]) \
1.395 +\ [bool_ (hd fs_), bool_ b1_]); \
1.396 +\ b2_ = nth_ 2 rb_; \
1.397 +\ fs_ = filter_sameFunId (lhs b2_) funs_; \
1.398 +\ (e2_::bool) = \
1.399 +\ (SubProblem (Biegelinie_,[makeFunctionTo,equation],\
1.400 +\ [Equation,fromFunction]) \
1.401 +\ [bool_ (hd fs_), bool_ b2_]); \
1.402 +\ b3_ = nth_ 3 rb_; \
1.403 +\ fs_ = filter_sameFunId (lhs b3_) funs_; \
1.404 +\ (e3_::bool) = \
1.405 +\ (SubProblem (Biegelinie_,[makeFunctionTo,equation],\
1.406 +\ [Equation,fromFunction]) \
1.407 +\ [bool_ (hd fs_), bool_ b3_]); \
1.408 +\ b4_ = nth_ 4 rb_; \
1.409 +\ fs_ = filter_sameFunId (lhs b4_) funs_; \
1.410 +\ (e4_::bool) = \
1.411 +\ (SubProblem (Biegelinie_,[makeFunctionTo,equation],\
1.412 +\ [Equation,fromFunction]) \
1.413 +\ [bool_ (hd fs_), bool_ b4_]) \
1.414 +\ in [e1_,e2_,e3_,e4_])"
1.415 +(* filter requires more than 1 sec !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!
1.416 +"Script SetzeRandbedScript (funs_::bool list) (rb_::bool list) = \
1.417 +\ (let b1_ = nth_ 1 rb_; \
1.418 +\ fs_ = filter (sameFunId (lhs b1_)) funs_; \
1.419 +\ (e1_::bool) = \
1.420 +\ (SubProblem (Biegelinie_,[makeFunctionTo,equation],\
1.421 +\ [Equation,fromFunction]) \
1.422 +\ [bool_ (hd fs_), bool_ b1_]); \
1.423 +\ b2_ = nth_ 2 rb_; \
1.424 +\ fs_ = filter (sameFunId (lhs b2_)) funs_; \
1.425 +\ (e2_::bool) = \
1.426 +\ (SubProblem (Biegelinie_,[makeFunctionTo,equation],\
1.427 +\ [Equation,fromFunction]) \
1.428 +\ [bool_ (hd fs_), bool_ b2_]); \
1.429 +\ b3_ = nth_ 3 rb_; \
1.430 +\ fs_ = filter (sameFunId (lhs b3_)) funs_; \
1.431 +\ (e3_::bool) = \
1.432 +\ (SubProblem (Biegelinie_,[makeFunctionTo,equation],\
1.433 +\ [Equation,fromFunction]) \
1.434 +\ [bool_ (hd fs_), bool_ b3_]); \
1.435 +\ b4_ = nth_ 4 rb_; \
1.436 +\ fs_ = filter (sameFunId (lhs b4_)) funs_; \
1.437 +\ (e4_::bool) = \
1.438 +\ (SubProblem (Biegelinie_,[makeFunctionTo,equation],\
1.439 +\ [Equation,fromFunction]) \
1.440 +\ [bool_ (hd fs_), bool_ b4_]) \
1.441 +\ in [e1_,e2_,e3_,e4_])"*)
1.442 +));
1.443 +
1.444 +store_met
1.445 + (prep_met Biegelinie.thy "met_equ_fromfun" [] e_metID
1.446 + (["Equation","fromFunction"],
1.447 + [("#Given" ,["functionEq fun_","substitution sub_"]),
1.448 + ("#Find" ,["equality equ___"])],
1.449 + {rew_ord'="tless_true", rls'=Erls, calc = [],
1.450 + srls = append_rls "srls_in_EquationfromFunc" e_rls
1.451 + [Calc("Tools.lhs", eval_lhs"eval_lhs_"),
1.452 + Calc("Atools.argument'_in",
1.453 + eval_argument_in
1.454 + "Atools.argument'_in")],
1.455 + prls=e_rls,
1.456 + crls = Atools_erls, nrls = e_rls},
1.457 +(*(M_b x = c_2 + c * x + -1 * q_0 / 2 * x ^^^ 2) (M_b L = 0) -->
1.458 + 0 = c_2 + c * L + -1 * q_0 / 2 * L ^^^ 2*)
1.459 +"Script Function2Equality (fun_::bool) (sub_::bool) =\
1.460 +\ (let fun_ = Take fun_; \
1.461 +\ bdv_ = argument_in (lhs fun_); \
1.462 +\ val_ = argument_in (lhs sub_); \
1.463 +\ equ_ = (Substitute [bdv_ = val_]) fun_; \
1.464 +\ equ_ = (Substitute [sub_]) fun_ \
1.465 +\ in (Rewrite_Set norm_Rational False) equ_) "
1.466 +));
1.467 +
1.468 +
1.469 +
1.470 +(* use"Knowledge/Biegelinie.ML";
1.471 + *)
1.472 \ No newline at end of file