1.1 --- a/src/Tools/isac/IsacKnowledge/Biegelinie.ML Wed Aug 25 15:15:01 2010 +0200
1.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
1.3 @@ -1,468 +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"IsacKnowledge/Biegelinie.ML";
1.10 -use"Biegelinie.ML";
1.11 -
1.12 -remove_thy"Typefix";
1.13 -remove_thy"Biegelinie";
1.14 -use_thy"IsacKnowledge/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"IsacKnowledge/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"IsacKnowledge/Biegelinie.ML";
1.471 - *)
1.472 \ No newline at end of file