neuper@37906: (* chapter 'Biegelinie' from the textbook: neuper@37906: Timischl, Kaiser. Ingenieur-Mathematik 3. Wien 1999. p.268-271. neuper@37906: author: Walther Neuper neuper@37906: 050826, neuper@37906: (c) due to copyright terms neuper@37906: *) neuper@37906: neuper@37954: theory Biegelinie imports Integrate Equation EqSystem begin neuper@37906: neuper@37906: consts neuper@37906: neuper@37906: q_ :: real => real ("q'_") (* Streckenlast *) neuper@37906: Q :: real => real (* Querkraft *) neuper@37906: Q' :: real => real (* Ableitung der Querkraft *) neuper@37906: M'_b :: real => real ("M'_b") (* Biegemoment *) neuper@37906: M'_b' :: real => real ("M'_b'") (* Ableitung des Biegemoments *) neuper@37906: y'' :: real => real (* 2.Ableitung der Biegeline *) neuper@37906: y' :: real => real (* Neigung der Biegeline *) neuper@37906: (*y :: real => real (* Biegeline *)*) neuper@37906: EI :: real (* Biegesteifigkeit *) neuper@37906: neuper@37906: (*new Descriptions in the related problems*) neuper@37906: Traegerlaenge :: real => una neuper@37906: Streckenlast :: real => una neuper@37906: BiegemomentVerlauf :: bool => una neuper@37906: Biegelinie :: (real => real) => una neuper@37906: Randbedingungen :: bool list => una neuper@37906: RandbedingungenBiegung :: bool list => una neuper@37906: RandbedingungenNeigung :: bool list => una neuper@37906: RandbedingungenMoment :: bool list => una neuper@37906: RandbedingungenQuerkraft :: bool list => una neuper@37906: FunktionsVariable :: real => una neuper@37906: Funktionen :: bool list => una neuper@37906: Gleichungen :: bool list => una neuper@37906: neuper@37906: (*Script-names*) neuper@37906: Biegelinie2Script :: "[real,real,real,real=>real,bool list, neuper@37906: bool] => bool" neuper@37906: ("((Script Biegelinie2Script (_ _ _ _ _ =))// (_))" 9) neuper@37906: BiegelinieScript :: "[real,real,real,real=>real,bool list,bool list, neuper@37906: bool] => bool" neuper@37906: ("((Script BiegelinieScript (_ _ _ _ _ _ =))// (_))" 9) neuper@37906: Biege2xIntegrierenScript :: "[real,real,real,bool,real=>real,bool list, neuper@37906: bool] => bool" neuper@37906: ("((Script Biege2xIntegrierenScript (_ _ _ _ _ _ =))// (_))" 9) neuper@37906: Biege4x4SystemScript :: "[real,real,real,real=>real,bool list, neuper@37906: bool] => bool" neuper@37906: ("((Script Biege4x4SystemScript (_ _ _ _ _ =))// (_))" 9) neuper@37906: Biege1xIntegrierenScript :: neuper@37906: "[real,real,real,real=>real,bool list,bool list,bool list, neuper@37906: bool] => bool" neuper@37906: ("((Script Biege1xIntegrierenScript (_ _ _ _ _ _ _ =))// (_))" 9) neuper@37906: Belastung2BiegelScript :: "[real,real, neuper@37906: bool list] => bool list" neuper@37906: ("((Script Belastung2BiegelScript (_ _ =))// (_))" 9) neuper@37906: SetzeRandbedScript :: "[bool list,bool list, neuper@37906: bool list] => bool list" neuper@37906: ("((Script SetzeRandbedScript (_ _ =))// (_))" 9) neuper@37906: neuper@37983: axioms neuper@37906: neuper@37983: Querkraft_Belastung: "Q' x = -q_ x" neuper@37983: Belastung_Querkraft: "-q_ x = Q' x" neuper@37906: neuper@37983: Moment_Querkraft: "M_b' x = Q x" neuper@37983: Querkraft_Moment: "Q x = M_b' x" neuper@37906: neuper@37983: Neigung_Moment: "y'' x = -M_b x/ EI" neuper@37983: Moment_Neigung: "M_b x = -EI * y'' x" neuper@37906: neuper@37906: (*according to rls 'simplify_Integral': .. = 1/a * .. instead .. = ../ a*) neuper@37983: make_fun_explicit: "Not (a =!= 0) ==> (a * (f x) = b) = (f x = 1/a * b)" neuper@37906: neuper@37954: ML {* neuper@37972: val thy = @{theory}; neuper@37972: neuper@37954: (** theory elements for transfer into html **) neuper@37954: neuper@37954: store_isa ["IsacKnowledge"] []; neuper@37972: store_thy thy neuper@37954: ["Walther Neuper 2005 supported by a grant from NMI Austria"]; neuper@37972: store_isa ["IsacKnowledge", theory2thyID thy, "Theorems"] neuper@37954: ["Walther Neuper 2005 supported by a grant from NMI Austria"]; neuper@37972: store_thm thy ("Belastung_Querkraft", Belastung_Querkraft) neuper@37954: ["Walther Neuper 2005 supported by a grant from NMI Austria"]; neuper@37972: store_thm thy ("Moment_Neigung", Moment_Neigung) neuper@37954: ["Walther Neuper 2005 supported by a grant from NMI Austria"]; neuper@37972: store_thm thy ("Moment_Querkraft", Moment_Querkraft) neuper@37954: ["Walther Neuper 2005 supported by a grant from NMI Austria"]; neuper@37972: store_thm thy ("Neigung_Moment", Neigung_Moment) neuper@37954: ["Walther Neuper 2005 supported by a grant from NMI Austria"]; neuper@37972: store_thm thy ("Querkraft_Belastung", Querkraft_Belastung) neuper@37954: ["Walther Neuper 2005 supported by a grant from NMI Austria"]; neuper@37972: store_thm thy ("Querkraft_Moment", Querkraft_Moment) neuper@37954: ["Walther Neuper 2005 supported by a grant from NMI Austria"]; neuper@37972: store_thm thy ("make_fun_explicit", make_fun_explicit) neuper@37954: ["Walther Neuper 2005 supported by a grant from NMI Austria"]; neuper@37954: neuper@37954: neuper@37954: (** problems **) neuper@37954: neuper@37954: store_pbt neuper@37972: (prep_pbt thy "pbl_bieg" [] e_pblID neuper@37954: (["Biegelinien"], neuper@37954: [("#Given" ,["Traegerlaenge l_", "Streckenlast q__"]), neuper@37954: (*("#Where",["0 < l_"]), ...wait for < and handling Arbfix*) neuper@37954: ("#Find" ,["Biegelinie b_"]), neuper@37954: ("#Relate",["Randbedingungen rb_"]) neuper@37954: ], neuper@37954: append_rls "e_rls" e_rls [], neuper@37954: NONE, neuper@37954: [["IntegrierenUndKonstanteBestimmen2"]])); neuper@37954: neuper@37954: store_pbt neuper@37972: (prep_pbt thy "pbl_bieg_mom" [] e_pblID neuper@37954: (["MomentBestimmte","Biegelinien"], neuper@37954: [("#Given" ,["Traegerlaenge l_", "Streckenlast q__"]), neuper@37954: (*("#Where",["0 < l_"]), ...wait for < and handling Arbfix*) neuper@37954: ("#Find" ,["Biegelinie b_"]), neuper@37954: ("#Relate",["RandbedingungenBiegung rb_","RandbedingungenMoment rm_"]) neuper@37954: ], neuper@37954: append_rls "e_rls" e_rls [], neuper@37954: NONE, neuper@37954: [["IntegrierenUndKonstanteBestimmen"]])); neuper@37954: neuper@37954: store_pbt neuper@37972: (prep_pbt thy "pbl_bieg_momg" [] e_pblID neuper@37954: (["MomentGegebene","Biegelinien"], neuper@37954: [], neuper@37954: append_rls "e_rls" e_rls [], neuper@37954: NONE, neuper@37954: [["IntegrierenUndKonstanteBestimmen","2xIntegrieren"]])); neuper@37954: neuper@37954: store_pbt neuper@37972: (prep_pbt thy "pbl_bieg_einf" [] e_pblID neuper@37954: (["einfache","Biegelinien"], neuper@37954: [], neuper@37954: append_rls "e_rls" e_rls [], neuper@37954: NONE, neuper@37954: [["IntegrierenUndKonstanteBestimmen","4x4System"]])); neuper@37954: neuper@37954: store_pbt neuper@37972: (prep_pbt thy "pbl_bieg_momquer" [] e_pblID neuper@37954: (["QuerkraftUndMomentBestimmte","Biegelinien"], neuper@37954: [], neuper@37954: append_rls "e_rls" e_rls [], neuper@37954: NONE, neuper@37954: [["IntegrierenUndKonstanteBestimmen","1xIntegrieren"]])); neuper@37954: neuper@37954: store_pbt neuper@37972: (prep_pbt thy "pbl_bieg_vonq" [] e_pblID neuper@37954: (["vonBelastungZu","Biegelinien"], neuper@37981: [("#Given" ,["Streckenlast q__","FunktionsVariable v_v"]), neuper@37954: ("#Find" ,["Funktionen funs___"])], neuper@37954: append_rls "e_rls" e_rls [], neuper@37954: NONE, neuper@37954: [["Biegelinien","ausBelastung"]])); neuper@37954: neuper@37954: store_pbt neuper@37972: (prep_pbt thy "pbl_bieg_randbed" [] e_pblID neuper@37954: (["setzeRandbedingungen","Biegelinien"], neuper@37954: [("#Given" ,["Funktionen funs_","Randbedingungen rb_"]), neuper@37954: ("#Find" ,["Gleichungen equs___"])], neuper@37954: append_rls "e_rls" e_rls [], neuper@37954: NONE, neuper@37954: [["Biegelinien","setzeRandbedingungenEin"]])); neuper@37954: neuper@37954: store_pbt neuper@37972: (prep_pbt thy "pbl_equ_fromfun" [] e_pblID neuper@37954: (["makeFunctionTo","equation"], neuper@37954: [("#Given" ,["functionEq fun_","substitution sub_"]), neuper@37954: ("#Find" ,["equality equ___"])], neuper@37954: append_rls "e_rls" e_rls [], neuper@37954: NONE, neuper@37954: [["Equation","fromFunction"]])); neuper@37954: neuper@37954: neuper@37954: (** methods **) neuper@37954: neuper@37954: val srls = Rls {id="srls_IntegrierenUnd..", neuper@37954: preconds = [], neuper@37954: rew_ord = ("termlessI",termlessI), neuper@37954: erls = append_rls "erls_in_srls_IntegrierenUnd.." e_rls neuper@37954: [(*for asm in nth_Cons_ ...*) neuper@37954: Calc ("op <",eval_equ "#less_"), neuper@37954: (*2nd nth_Cons_ pushes n+-1 into asms*) neuper@37954: Calc("op +", eval_binop "#add_") neuper@37954: ], neuper@37954: srls = Erls, calc = [], neuper@37969: rules = [Thm ("nth_Cons_",num_str @{thm nth_Cons_}), neuper@37954: Calc("op +", eval_binop "#add_"), neuper@37969: Thm ("nth_Nil_",num_str @{thm nth_Nil_}), neuper@37954: Calc("Tools.lhs", eval_lhs"eval_lhs_"), neuper@37954: Calc("Tools.rhs", eval_rhs"eval_rhs_"), neuper@37954: Calc("Atools.argument'_in", neuper@37954: eval_argument_in "Atools.argument'_in") neuper@37954: ], neuper@37954: scr = EmptyScr}; neuper@37954: neuper@37954: val srls2 = neuper@37954: Rls {id="srls_IntegrierenUnd..", neuper@37954: preconds = [], neuper@37954: rew_ord = ("termlessI",termlessI), neuper@37954: erls = append_rls "erls_in_srls_IntegrierenUnd.." e_rls neuper@37954: [(*for asm in nth_Cons_ ...*) neuper@37954: Calc ("op <",eval_equ "#less_"), neuper@37954: (*2nd nth_Cons_ pushes n+-1 into asms*) neuper@37954: Calc("op +", eval_binop "#add_") neuper@37954: ], neuper@37954: srls = Erls, calc = [], neuper@37969: rules = [Thm ("nth_Cons_",num_str @{thm nth_Cons_}), neuper@37954: Calc("op +", eval_binop "#add_"), neuper@37969: Thm ("nth_Nil_", num_str @{thm nth_Nil_}), neuper@37954: Calc("Tools.lhs", eval_lhs "eval_lhs_"), neuper@37954: Calc("Atools.filter'_sameFunId", neuper@37954: eval_filter_sameFunId "Atools.filter'_sameFunId"), neuper@37954: (*WN070514 just for smltest/../biegelinie.sml ...*) neuper@37954: Calc("Atools.sameFunId", eval_sameFunId "Atools.sameFunId"), neuper@37969: Thm ("filter_Cons", num_str @{thm filter_Cons}), neuper@37969: Thm ("filter_Nil", num_str @{thm filter_Nil}), neuper@37969: Thm ("if_True", num_str @{thm if_True}), neuper@37969: Thm ("if_False", num_str @{thm if_False}), neuper@37969: Thm ("hd_thm", num_str @{thm hd_thm}) neuper@37954: ], neuper@37954: scr = EmptyScr}; neuper@37954: neuper@37954: store_met neuper@37972: (prep_met thy "met_biege" [] e_metID neuper@37954: (["IntegrierenUndKonstanteBestimmen"], neuper@37954: [("#Given" ,["Traegerlaenge l_", "Streckenlast q__", neuper@37981: "FunktionsVariable v_v"]), neuper@37954: (*("#Where",["0 < l_"]), ...wait for < and handling Arbfix*) neuper@37954: ("#Find" ,["Biegelinie b_"]), neuper@37954: ("#Relate",["RandbedingungenBiegung rb_", neuper@37954: "RandbedingungenMoment rm_"]) neuper@37954: ], neuper@37954: {rew_ord'="tless_true", neuper@37954: rls' = append_rls "erls_IntegrierenUndK.." e_rls neuper@37954: [Calc ("Atools.ident",eval_ident "#ident_"), neuper@37969: Thm ("not_true",num_str @{thm not_true}), neuper@37969: Thm ("not_false",num_str @{thm not_false})], neuper@37954: calc = [], srls = srls, prls = Erls, neuper@37954: crls = Atools_erls, nrls = Erls}, neuper@37954: "Script BiegelinieScript " ^ neuper@37982: "(l_::real) (q__::real) (v_v::real) (b_::real=>real) " ^ neuper@37954: "(rb_::bool list) (rm_::bool list) = " ^ neuper@37981: " (let q___ = Take (q_ v_v = q__); " ^ neuper@37954: " q___ = ((Rewrite sym_real_minus_eq_cancel True) @@ " ^ neuper@37954: " (Rewrite Belastung_Querkraft True)) q___; " ^ neuper@37954: " (Q__:: bool) = " ^ neuper@37954: " (SubProblem (Biegelinie_,[named,integrate,function], " ^ neuper@37954: " [diff,integration,named]) " ^ neuper@37981: " [real_ (rhs q___), real_ v_v, real_real_ Q]); " ^ neuper@37954: " Q__ = Rewrite Querkraft_Moment True Q__; " ^ neuper@37954: " (M__::bool) = " ^ neuper@37954: " (SubProblem (Biegelinie_,[named,integrate,function], " ^ neuper@37954: " [diff,integration,named]) " ^ neuper@37981: " [real_ (rhs Q__), real_ v_v, real_real_ M_b]); " ^ neuper@37954: " e1__ = nth_ 1 rm_; " ^ neuper@37954: " (x1__::real) = argument_in (lhs e1__); " ^ neuper@37954: " (M1__::bool) = (Substitute [v_ = x1__]) M__; " ^ neuper@37954: " M1__ = (Substitute [e1__]) M1__ ; " ^ neuper@37954: " M2__ = Take M__; " ^ neuper@37954: (*without this Take 'Substitute [v_ = x2__]' takes _last formula from ctree_*) neuper@37954: " e2__ = nth_ 2 rm_; " ^ neuper@37954: " (x2__::real) = argument_in (lhs e2__); " ^ neuper@37954: " (M2__::bool) = ((Substitute [v_ = x2__]) @@ " ^ neuper@37954: " (Substitute [e2__])) M2__; " ^ neuper@37954: " (c_1_2__::bool list) = " ^ neuper@37954: " (SubProblem (Biegelinie_,[linear,system],[no_met]) " ^ neuper@37954: " [booll_ [M1__, M2__], reall [c,c_2]]); " ^ neuper@37954: " M__ = Take M__; " ^ neuper@37954: " M__ = ((Substitute c_1_2__) @@ " ^ neuper@37954: " (Try (Rewrite_Set_Inst [(bdv_1, c),(bdv_2, c_2)]" ^ neuper@37954: " simplify_System False)) @@ " ^ neuper@37954: " (Rewrite Moment_Neigung False) @@ " ^ neuper@37954: " (Rewrite make_fun_explicit False)) M__; " ^ neuper@37954: (*----------------------- and the same once more ------------------------*) neuper@37954: " (N__:: bool) = " ^ neuper@37954: " (SubProblem (Biegelinie_,[named,integrate,function], " ^ neuper@37954: " [diff,integration,named]) " ^ neuper@37981: " [real_ (rhs M__), real_ v_v, real_real_ y']); " ^ neuper@37954: " (B__:: bool) = " ^ neuper@37954: " (SubProblem (Biegelinie_,[named,integrate,function], " ^ neuper@37954: " [diff,integration,named]) " ^ neuper@37981: " [real_ (rhs N__), real_ v_v, real_real_ y]); " ^ neuper@37954: " e1__ = nth_ 1 rb_; " ^ neuper@37954: " (x1__::real) = argument_in (lhs e1__); " ^ neuper@37954: " (B1__::bool) = (Substitute [v_ = x1__]) B__; " ^ neuper@37954: " B1__ = (Substitute [e1__]) B1__ ; " ^ neuper@37954: " B2__ = Take B__; " ^ neuper@37954: " e2__ = nth_ 2 rb_; " ^ neuper@37954: " (x2__::real) = argument_in (lhs e2__); " ^ neuper@37954: " (B2__::bool) = ((Substitute [v_ = x2__]) @@ " ^ neuper@37954: " (Substitute [e2__])) B2__; " ^ neuper@37954: " (c_1_2__::bool list) = " ^ neuper@37954: " (SubProblem (Biegelinie_,[linear,system],[no_met]) " ^ neuper@37954: " [booll_ [B1__, B2__], reall [c,c_2]]); " ^ neuper@37954: " B__ = Take B__; " ^ neuper@37954: " B__ = ((Substitute c_1_2__) @@ " ^ neuper@37954: " (Rewrite_Set_Inst [(bdv, x)] make_ratpoly_in False)) B__ " ^ neuper@37954: " in B__)" neuper@37954: )); neuper@37954: neuper@37954: store_met neuper@37972: (prep_met thy "met_biege_2" [] e_metID neuper@37954: (["IntegrierenUndKonstanteBestimmen2"], neuper@37954: [("#Given" ,["Traegerlaenge l_", "Streckenlast q__", neuper@37981: "FunktionsVariable v_v"]), neuper@37954: (*("#Where",["0 < l_"]), ...wait for < and handling Arbfix*) neuper@37954: ("#Find" ,["Biegelinie b_"]), neuper@37954: ("#Relate",["Randbedingungen rb_"]) neuper@37954: ], neuper@37954: {rew_ord'="tless_true", neuper@37954: rls' = append_rls "erls_IntegrierenUndK.." e_rls neuper@37954: [Calc ("Atools.ident",eval_ident "#ident_"), neuper@37969: Thm ("not_true",num_str @{thm not_true}), neuper@37969: Thm ("not_false",num_str @{thm not_false})], neuper@37954: calc = [], neuper@37954: srls = append_rls "erls_IntegrierenUndK.." e_rls neuper@37954: [Calc("Tools.rhs", eval_rhs"eval_rhs_"), neuper@37954: Calc ("Atools.ident",eval_ident "#ident_"), neuper@37969: Thm ("last_thmI",num_str @{thm last_thmI}), neuper@37969: Thm ("if_True",num_str @{thm if_True}), neuper@37969: Thm ("if_False",num_str @{thm if_False}) neuper@37954: ], neuper@37954: prls = Erls, crls = Atools_erls, nrls = Erls}, neuper@37954: "Script Biegelinie2Script " ^ neuper@37982: "(l_::real) (q__::real) (v_v::real) (b_::real=>real) (rb_::bool list) = " ^ neuper@37954: " (let " ^ neuper@37954: " (funs_:: bool list) = " ^ neuper@37954: " (SubProblem (Biegelinie_,[vonBelastungZu,Biegelinien], " ^ neuper@37954: " [Biegelinien,ausBelastung]) " ^ neuper@37954: " [real_ q__, real_ v_]); " ^ neuper@37954: " (equs_::bool list) = " ^ neuper@37954: " (SubProblem (Biegelinie_,[setzeRandbedingungen,Biegelinien]," ^ neuper@37954: " [Biegelinien,setzeRandbedingungenEin]) " ^ neuper@37954: " [booll_ funs_, booll_ rb_]); " ^ neuper@37954: " (cons_::bool list) = " ^ neuper@37954: " (SubProblem (Biegelinie_,[linear,system],[no_met]) " ^ neuper@37954: " [booll_ equs_, reall [c,c_2,c_3,c_4]]); " ^ neuper@37954: " B_ = Take (lastI funs_); " ^ neuper@37954: " B_ = ((Substitute cons_) @@ " ^ neuper@37981: " (Rewrite_Set_Inst [(bdv, v_v)] make_ratpoly_in False)) B_ " ^ neuper@37954: " in B_)" neuper@37954: )); neuper@37954: neuper@37954: store_met neuper@37972: (prep_met thy "met_biege_intconst_2" [] e_metID neuper@37954: (["IntegrierenUndKonstanteBestimmen","2xIntegrieren"], neuper@37954: [], neuper@37954: {rew_ord'="tless_true", rls'=Erls, calc = [], neuper@37954: srls = e_rls, neuper@37954: prls=e_rls, neuper@37954: crls = Atools_erls, nrls = e_rls}, neuper@37954: "empty_script" neuper@37954: )); neuper@37954: neuper@37954: store_met neuper@37972: (prep_met thy "met_biege_intconst_4" [] e_metID neuper@37954: (["IntegrierenUndKonstanteBestimmen","4x4System"], neuper@37954: [], neuper@37954: {rew_ord'="tless_true", rls'=Erls, calc = [], neuper@37954: srls = e_rls, neuper@37954: prls=e_rls, neuper@37954: crls = Atools_erls, nrls = e_rls}, neuper@37954: "empty_script" neuper@37954: )); neuper@37954: neuper@37954: store_met neuper@37972: (prep_met thy "met_biege_intconst_1" [] e_metID neuper@37954: (["IntegrierenUndKonstanteBestimmen","1xIntegrieren"], neuper@37954: [], neuper@37954: {rew_ord'="tless_true", rls'=Erls, calc = [], neuper@37954: srls = e_rls, neuper@37954: prls=e_rls, neuper@37954: crls = Atools_erls, nrls = e_rls}, neuper@37954: "empty_script" neuper@37954: )); neuper@37954: neuper@37954: store_met neuper@37972: (prep_met thy "met_biege2" [] e_metID neuper@37954: (["Biegelinien"], neuper@37954: [], neuper@37954: {rew_ord'="tless_true", rls'=Erls, calc = [], neuper@37954: srls = e_rls, neuper@37954: prls=e_rls, neuper@37954: crls = Atools_erls, nrls = e_rls}, neuper@37954: "empty_script" neuper@37954: )); neuper@37954: neuper@37954: store_met neuper@37972: (prep_met thy "met_biege_ausbelast" [] e_metID neuper@37954: (["Biegelinien","ausBelastung"], neuper@37981: [("#Given" ,["Streckenlast q__","FunktionsVariable v_v"]), neuper@37954: ("#Find" ,["Funktionen funs_"])], neuper@37954: {rew_ord'="tless_true", neuper@37954: rls' = append_rls "erls_ausBelastung" e_rls neuper@37954: [Calc ("Atools.ident",eval_ident "#ident_"), neuper@37969: Thm ("not_true",num_str @{thm not_true}), neuper@37969: Thm ("not_false",num_str @{thm not_false})], neuper@37954: calc = [], neuper@37954: srls = append_rls "srls_ausBelastung" e_rls neuper@37954: [Calc("Tools.rhs", eval_rhs"eval_rhs_")], neuper@37954: prls = e_rls, crls = Atools_erls, nrls = e_rls}, neuper@37982: "Script Belastung2BiegelScript (q__::real) (v_v::real) = " ^ neuper@37981: " (let q___ = Take (q_ v_v = q__); " ^ neuper@37954: " q___ = ((Rewrite sym_real_minus_eq_cancel True) @@ " ^ neuper@37954: " (Rewrite Belastung_Querkraft True)) q___; " ^ neuper@37954: " (Q__:: bool) = " ^ neuper@37954: " (SubProblem (Biegelinie_,[named,integrate,function], " ^ neuper@37954: " [diff,integration,named]) " ^ neuper@37981: " [real_ (rhs q___), real_ v_v, real_real_ Q]); " ^ neuper@37954: " M__ = Rewrite Querkraft_Moment True Q__; " ^ neuper@37954: " (M__::bool) = " ^ neuper@37954: " (SubProblem (Biegelinie_,[named,integrate,function], " ^ neuper@37954: " [diff,integration,named]) " ^ neuper@37981: " [real_ (rhs M__), real_ v_v, real_real_ M_b]); " ^ neuper@37954: " N__ = ((Rewrite Moment_Neigung False) @@ " ^ neuper@37954: " (Rewrite make_fun_explicit False)) M__; " ^ neuper@37954: " (N__:: bool) = " ^ neuper@37954: " (SubProblem (Biegelinie_,[named,integrate,function], " ^ neuper@37954: " [diff,integration,named]) " ^ neuper@37981: " [real_ (rhs N__), real_ v_v, real_real_ y']); " ^ neuper@37954: " (B__:: bool) = " ^ neuper@37954: " (SubProblem (Biegelinie_,[named,integrate,function], " ^ neuper@37954: " [diff,integration,named]) " ^ neuper@37981: " [real_ (rhs N__), real_ v_v, real_real_ y]) " ^ neuper@37954: " in [Q__, M__, N__, B__])" neuper@37954: )); neuper@37954: neuper@37954: store_met neuper@37972: (prep_met thy "met_biege_setzrand" [] e_metID neuper@37954: (["Biegelinien","setzeRandbedingungenEin"], neuper@37954: [("#Given" ,["Funktionen funs_","Randbedingungen rb_"]), neuper@37954: ("#Find" ,["Gleichungen equs___"])], neuper@37954: {rew_ord'="tless_true", rls'=Erls, calc = [], neuper@37954: srls = srls2, neuper@37954: prls=e_rls, neuper@37954: crls = Atools_erls, nrls = e_rls}, neuper@37954: "Script SetzeRandbedScript (funs_::bool list) (rb_::bool list) = " ^ neuper@37954: " (let b1_ = nth_ 1 rb_; " ^ neuper@37954: " fs_ = filter_sameFunId (lhs b1_) funs_; " ^ neuper@37954: " (e1_::bool) = " ^ neuper@37954: " (SubProblem (Biegelinie_,[makeFunctionTo,equation]," ^ neuper@37954: " [Equation,fromFunction]) " ^ neuper@37954: " [bool_ (hd fs_), bool_ b1_]); " ^ neuper@37954: " b2_ = nth_ 2 rb_; " ^ neuper@37954: " fs_ = filter_sameFunId (lhs b2_) funs_; " ^ neuper@37954: " (e2_::bool) = " ^ neuper@37954: " (SubProblem (Biegelinie_,[makeFunctionTo,equation]," ^ neuper@37954: " [Equation,fromFunction]) " ^ neuper@37954: " [bool_ (hd fs_), bool_ b2_]); " ^ neuper@37954: " b3_ = nth_ 3 rb_; " ^ neuper@37954: " fs_ = filter_sameFunId (lhs b3_) funs_; " ^ neuper@37954: " (e3_::bool) = " ^ neuper@37954: " (SubProblem (Biegelinie_,[makeFunctionTo,equation]," ^ neuper@37954: " [Equation,fromFunction]) " ^ neuper@37954: " [bool_ (hd fs_), bool_ b3_]); " ^ neuper@37954: " b4_ = nth_ 4 rb_; " ^ neuper@37954: " fs_ = filter_sameFunId (lhs b4_) funs_; " ^ neuper@37954: " (e4_::bool) = " ^ neuper@37954: " (SubProblem (Biegelinie_,[makeFunctionTo,equation]," ^ neuper@37954: " [Equation,fromFunction]) " ^ neuper@37954: " [bool_ (hd fs_), bool_ b4_]) " ^ neuper@37954: " in [e1_,e2_,e3_,e4_])" neuper@37954: (* filter requires more than 1 sec !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!! neuper@37954: "Script SetzeRandbedScript (funs_::bool list) (rb_::bool list) = " ^ neuper@37954: " (let b1_ = nth_ 1 rb_; " ^ neuper@37954: " fs_ = filter (sameFunId (lhs b1_)) funs_; " ^ neuper@37954: " (e1_::bool) = " ^ neuper@37954: " (SubProblem (Biegelinie_,[makeFunctionTo,equation]," ^ neuper@37954: " [Equation,fromFunction]) " ^ neuper@37954: " [bool_ (hd fs_), bool_ b1_]); " ^ neuper@37954: " b2_ = nth_ 2 rb_; " ^ neuper@37954: " fs_ = filter (sameFunId (lhs b2_)) funs_; " ^ neuper@37954: " (e2_::bool) = " ^ neuper@37954: " (SubProblem (Biegelinie_,[makeFunctionTo,equation]," ^ neuper@37954: " [Equation,fromFunction]) " ^ neuper@37954: " [bool_ (hd fs_), bool_ b2_]); " ^ neuper@37954: " b3_ = nth_ 3 rb_; " ^ neuper@37954: " fs_ = filter (sameFunId (lhs b3_)) funs_; " ^ neuper@37954: " (e3_::bool) = " ^ neuper@37954: " (SubProblem (Biegelinie_,[makeFunctionTo,equation]," ^ neuper@37954: " [Equation,fromFunction]) " ^ neuper@37954: " [bool_ (hd fs_), bool_ b3_]); " ^ neuper@37954: " b4_ = nth_ 4 rb_; " ^ neuper@37954: " fs_ = filter (sameFunId (lhs b4_)) funs_; " ^ neuper@37954: " (e4_::bool) = " ^ neuper@37954: " (SubProblem (Biegelinie_,[makeFunctionTo,equation]," ^ neuper@37954: " [Equation,fromFunction]) " ^ neuper@37954: " [bool_ (hd fs_), bool_ b4_]) " ^ neuper@37954: " in [e1_,e2_,e3_,e4_])"*) neuper@37954: )); neuper@37954: neuper@37954: store_met neuper@37972: (prep_met thy "met_equ_fromfun" [] e_metID neuper@37954: (["Equation","fromFunction"], neuper@37954: [("#Given" ,["functionEq fun_","substitution sub_"]), neuper@37954: ("#Find" ,["equality equ___"])], neuper@37954: {rew_ord'="tless_true", rls'=Erls, calc = [], neuper@37954: srls = append_rls "srls_in_EquationfromFunc" e_rls neuper@37954: [Calc("Tools.lhs", eval_lhs"eval_lhs_"), neuper@37954: Calc("Atools.argument'_in", neuper@37954: eval_argument_in neuper@37954: "Atools.argument'_in")], neuper@37954: prls=e_rls, neuper@37954: crls = Atools_erls, nrls = e_rls}, neuper@37954: (*(M_b x = c_2 + c * x + -1 * q_0 / 2 * x ^^^ 2) (M_b L = 0) --> neuper@37954: 0 = c_2 + c * L + -1 * q_0 / 2 * L ^^^ 2*) neuper@37954: "Script Function2Equality (fun_::bool) (sub_::bool) =" ^ neuper@37954: " (let fun_ = Take fun_; " ^ neuper@37954: " bdv_ = argument_in (lhs fun_); " ^ neuper@37954: " val_ = argument_in (lhs sub_); " ^ neuper@37954: " equ_ = (Substitute [bdv_ = val_]) fun_; " ^ neuper@37954: " equ_ = (Substitute [sub_]) fun_ " ^ neuper@37954: " in (Rewrite_Set norm_Rational False) equ_) " neuper@37954: )); neuper@37954: *} neuper@37954: neuper@37906: end neuper@37906: