# HG changeset patch # User Walther Neuper # Date 1284031896 -7200 # Node ID 7d603b7ead7336b93fc18b8a549e85dac5968098 # Parent 6d9fb5475156289eb8144dcfde197dfc76a46599 updated Knowledge/Biegelinie.thy diff -r 6d9fb5475156 -r 7d603b7ead73 src/Tools/isac/Knowledge/Atools.thy --- a/src/Tools/isac/Knowledge/Atools.thy Thu Sep 09 09:58:28 2010 +0200 +++ b/src/Tools/isac/Knowledge/Atools.thy Thu Sep 09 13:31:36 2010 +0200 @@ -11,7 +11,8 @@ ("Interpret/generate.sml")("Interpret/calchead.sml")("Interpret/appl.sml") ("Interpret/rewtools.sml")("Interpret/script.sml")("Interpret/solve.sml") ("Interpret/inform.sml")("Interpret/mathengine.sml") - +("xmlsrc/mathml.sml")("xmlsrc/datatypes.sml")("xmlsrc/pbl-met-hierarchy.sml") +("xmlsrc/thy-hierarchy.sml")("xmlsrc/interface-xml.sml") begin use "Interpret/mstools.sml" use "Interpret/ctree.sml" @@ -25,6 +26,12 @@ use "Interpret/inform.sml" (*^^^ need files for: fun castab*) use "Interpret/mathengine.sml" +use "xmlsrc/mathml.sml" +use "xmlsrc/datatypes.sml" +use "xmlsrc/pbl-met-hierarchy.sml" +use "xmlsrc/thy-hierarchy.sml" (*^^^ need files for: fun store_isa*) +use "xmlsrc/interface-xml.sml" + consts Arbfix :: "real" diff -r 6d9fb5475156 -r 7d603b7ead73 src/Tools/isac/Knowledge/Biegelinie.thy --- a/src/Tools/isac/Knowledge/Biegelinie.thy Thu Sep 09 09:58:28 2010 +0200 +++ b/src/Tools/isac/Knowledge/Biegelinie.thy Thu Sep 09 13:31:36 2010 +0200 @@ -1,7 +1,6 @@ (* chapter 'Biegelinie' from the textbook: Timischl, Kaiser. Ingenieur-Mathematik 3. Wien 1999. p.268-271. - author: Walther Neuper - 050826, + author: Walther Neuper 050826, (c) due to copyright terms *) @@ -9,29 +8,29 @@ consts - q_ :: real => real ("q'_") (* Streckenlast *) - Q :: real => real (* Querkraft *) - Q' :: real => real (* Ableitung der Querkraft *) - M'_b :: real => real ("M'_b") (* Biegemoment *) - M'_b' :: real => real ("M'_b'") (* Ableitung des Biegemoments *) - y'' :: real => real (* 2.Ableitung der Biegeline *) - y' :: real => real (* Neigung der Biegeline *) -(*y :: real => real (* Biegeline *)*) - EI :: real (* Biegesteifigkeit *) + q_ :: "real => real" ("q'_") (* Streckenlast *) + Q :: "real => real" (* Querkraft *) + Q' :: "real => real" (* Ableitung der Querkraft *) + M'_b :: "real => real" ("M'_b") (* Biegemoment *) + M'_b' :: "real => real" ("M'_b'") (* Ableitung des Biegemoments *) + y'' :: "real => real" (* 2.Ableitung der Biegeline *) + y' :: "real => real" (* Neigung der Biegeline *) +(*y :: "real => real" (* Biegeline *)*) + EI :: "real" (* Biegesteifigkeit *) (*new Descriptions in the related problems*) - Traegerlaenge :: real => una - Streckenlast :: real => una - BiegemomentVerlauf :: bool => una - Biegelinie :: (real => real) => una - Randbedingungen :: bool list => una - RandbedingungenBiegung :: bool list => una - RandbedingungenNeigung :: bool list => una - RandbedingungenMoment :: bool list => una - RandbedingungenQuerkraft :: bool list => una - FunktionsVariable :: real => una - Funktionen :: bool list => una - Gleichungen :: bool list => una + Traegerlaenge :: "real => una" + Streckenlast :: "real => una" + BiegemomentVerlauf :: "bool => una" + Biegelinie :: "(real => real) => una" + Randbedingungen :: "bool list => una" + RandbedingungenBiegung :: "bool list => una" + RandbedingungenNeigung :: "bool list => una" + RandbedingungenMoment :: "bool list => una" + RandbedingungenQuerkraft :: "bool list => una" + FunktionsVariable :: "real => una" + Funktionen :: "bool list => una" + Gleichungen :: "bool list => una" (*Script-names*) Biegelinie2Script :: "[real,real,real,real=>real,bool list, @@ -81,31 +80,32 @@ ["Walther Neuper 2005 supported by a grant from NMI Austria"]; store_isa ["IsacKnowledge", theory2thyID thy, "Theorems"] ["Walther Neuper 2005 supported by a grant from NMI Austria"]; -store_thm thy ("Belastung_Querkraft", Belastung_Querkraft) +store_thm thy ("Belastung_Querkraft", @{thm Belastung_Querkraft}) ["Walther Neuper 2005 supported by a grant from NMI Austria"]; -store_thm thy ("Moment_Neigung", Moment_Neigung) +store_thm thy ("Moment_Neigung", @{thm Moment_Neigung}) ["Walther Neuper 2005 supported by a grant from NMI Austria"]; -store_thm thy ("Moment_Querkraft", Moment_Querkraft) +store_thm thy ("Moment_Querkraft", @{thm Moment_Querkraft}) ["Walther Neuper 2005 supported by a grant from NMI Austria"]; -store_thm thy ("Neigung_Moment", Neigung_Moment) +store_thm thy ("Neigung_Moment", @{thm Neigung_Moment}) ["Walther Neuper 2005 supported by a grant from NMI Austria"]; -store_thm thy ("Querkraft_Belastung", Querkraft_Belastung) +store_thm thy ("Querkraft_Belastung", @{thm Querkraft_Belastung}) ["Walther Neuper 2005 supported by a grant from NMI Austria"]; -store_thm thy ("Querkraft_Moment", Querkraft_Moment) +store_thm thy ("Querkraft_Moment", @{thm Querkraft_Moment}) ["Walther Neuper 2005 supported by a grant from NMI Austria"]; -store_thm thy ("make_fun_explicit", make_fun_explicit) +store_thm thy ("make_fun_explicit", @{thm make_fun_explicit}) ["Walther Neuper 2005 supported by a grant from NMI Austria"]; - +*} +ML {* (** problems **) store_pbt (prep_pbt thy "pbl_bieg" [] e_pblID (["Biegelinien"], - [("#Given" ,["Traegerlaenge l_", "Streckenlast q__"]), - (*("#Where",["0 < l_"]), ...wait for < and handling Arbfix*) - ("#Find" ,["Biegelinie b_"]), - ("#Relate",["Randbedingungen rb_"]) + [("#Given" ,["Traegerlaenge l_l", "Streckenlast q_q"]), + (*("#Where",["0 < l_l"]), ...wait for < and handling Arbfix*) + ("#Find" ,["Biegelinie b_b"]), + ("#Relate",["Randbedingungen r_b"]) ], append_rls "e_rls" e_rls [], NONE, @@ -114,10 +114,10 @@ store_pbt (prep_pbt thy "pbl_bieg_mom" [] e_pblID (["MomentBestimmte","Biegelinien"], - [("#Given" ,["Traegerlaenge l_", "Streckenlast q__"]), - (*("#Where",["0 < l_"]), ...wait for < and handling Arbfix*) - ("#Find" ,["Biegelinie b_"]), - ("#Relate",["RandbedingungenBiegung rb_","RandbedingungenMoment rm_"]) + [("#Given" ,["Traegerlaenge l_l", "Streckenlast q_q"]), + (*("#Where",["0 < l_l"]), ...wait for < and handling Arbfix*) + ("#Find" ,["Biegelinie b_b"]), + ("#Relate",["RandbedingungenBiegung r_b","RandbedingungenMoment r_m"]) ], append_rls "e_rls" e_rls [], NONE, @@ -150,8 +150,8 @@ store_pbt (prep_pbt thy "pbl_bieg_vonq" [] e_pblID (["vonBelastungZu","Biegelinien"], - [("#Given" ,["Streckenlast q__","FunktionsVariable v_v"]), - ("#Find" ,["Funktionen funs___"])], + [("#Given" ,["Streckenlast q_q","FunktionsVariable v_v"]), + ("#Find" ,["Funktionen funs'''"])], append_rls "e_rls" e_rls [], NONE, [["Biegelinien","ausBelastung"]])); @@ -159,8 +159,8 @@ store_pbt (prep_pbt thy "pbl_bieg_randbed" [] e_pblID (["setzeRandbedingungen","Biegelinien"], - [("#Given" ,["Funktionen funs_","Randbedingungen rb_"]), - ("#Find" ,["Gleichungen equs___"])], + [("#Given" ,["Funktionen fun_s","Randbedingungen r_b"]), + ("#Find" ,["Gleichungen equs'''"])], append_rls "e_rls" e_rls [], NONE, [["Biegelinien","setzeRandbedingungenEin"]])); @@ -168,28 +168,29 @@ store_pbt (prep_pbt thy "pbl_equ_fromfun" [] e_pblID (["makeFunctionTo","equation"], - [("#Given" ,["functionEq fun_","substitution sub_"]), - ("#Find" ,["equality equ___"])], + [("#Given" ,["functionEq fu_n","substitution su_b"]), + ("#Find" ,["equality equ'''"])], append_rls "e_rls" e_rls [], NONE, [["Equation","fromFunction"]])); - +*} +ML {* (** methods **) val srls = Rls {id="srls_IntegrierenUnd..", preconds = [], rew_ord = ("termlessI",termlessI), erls = append_rls "erls_in_srls_IntegrierenUnd.." e_rls - [(*for asm in nth_Cons_ ...*) + [(*for asm in NTH_CONS ...*) Calc ("op <",eval_equ "#less_"), - (*2nd nth_Cons_ pushes n+-1 into asms*) + (*2nd NTH_CONS pushes n+-1 into asms*) Calc("op +", eval_binop "#add_") ], srls = Erls, calc = [], - rules = [Thm ("nth_Cons_",num_str @{thm nth_Cons_}), + rules = [Thm ("NTH_CONS",num_str @{thm NTH_CONS}), Calc("op +", eval_binop "#add_"), - Thm ("nth_Nil_",num_str @{thm nth_Nil_}), + Thm ("NTH_NIL",num_str @{thm NTH_NIL}), Calc("Tools.lhs", eval_lhs"eval_lhs_"), Calc("Tools.rhs", eval_rhs"eval_rhs_"), Calc("Atools.argument'_in", @@ -202,15 +203,15 @@ preconds = [], rew_ord = ("termlessI",termlessI), erls = append_rls "erls_in_srls_IntegrierenUnd.." e_rls - [(*for asm in nth_Cons_ ...*) + [(*for asm in NTH_CONS ...*) Calc ("op <",eval_equ "#less_"), - (*2nd nth_Cons_ pushes n+-1 into asms*) + (*2nd NTH_CONS pushes n+-1 into asms*) Calc("op +", eval_binop "#add_") ], srls = Erls, calc = [], - rules = [Thm ("nth_Cons_",num_str @{thm nth_Cons_}), + rules = [Thm ("NTH_CONS",num_str @{thm NTH_CONS}), Calc("op +", eval_binop "#add_"), - Thm ("nth_Nil_", num_str @{thm nth_Nil_}), + Thm ("NTH_NIL", num_str @{thm NTH_NIL}), Calc("Tools.lhs", eval_lhs "eval_lhs_"), Calc("Atools.filter'_sameFunId", eval_filter_sameFunId "Atools.filter'_sameFunId"), @@ -223,16 +224,18 @@ Thm ("hd_thm", num_str @{thm hd_thm}) ], scr = EmptyScr}; - +*} + +ML {* store_met (prep_met thy "met_biege" [] e_metID (["IntegrierenUndKonstanteBestimmen"], - [("#Given" ,["Traegerlaenge l_", "Streckenlast q__", + [("#Given" ,["Traegerlaenge l_l", "Streckenlast q_q", "FunktionsVariable v_v"]), - (*("#Where",["0 < l_"]), ...wait for < and handling Arbfix*) - ("#Find" ,["Biegelinie b_"]), - ("#Relate",["RandbedingungenBiegung rb_", - "RandbedingungenMoment rm_"]) + (*("#Where",["0 < l_l"]), ...wait for < and handling Arbfix*) + ("#Find" ,["Biegelinie b_b"]), + ("#Relate",["RandbedingungenBiegung r_b", + "RandbedingungenMoment r_m"]) ], {rew_ord'="tless_true", rls' = append_rls "erls_IntegrierenUndK.." e_rls @@ -242,74 +245,76 @@ calc = [], srls = srls, prls = Erls, crls = Atools_erls, nrls = Erls}, "Script BiegelinieScript " ^ -"(l_::real) (q__::real) (v_v::real) (b_::real=>real) " ^ -"(rb_::bool list) (rm_::bool list) = " ^ -" (let q___ = Take (q_ v_v = q__); " ^ -" q___ = ((Rewrite sym_real_minus_eq_cancel True) @@ " ^ -" (Rewrite Belastung_Querkraft True)) q___; " ^ -" (Q__:: bool) = " ^ -" (SubProblem (Biegelinie_,[named,integrate,function], " ^ +"(l_l::real) (q__q::real) (v_v::real) (b_b::real=>real) " ^ +"(r_b::bool list) (r_m::bool list) = " ^ +" (let q___q = Take (q_q v_v = q__q); " ^ +" q___q = ((Rewrite sym_real_minus_eq_cancel True) @@ " ^ +" (Rewrite Belastung_Querkraft True)) q___q; " ^ +" (Q__Q:: bool) = " ^ +" (SubProblem (Biegelinie',[named,integrate,function], " ^ " [diff,integration,named]) " ^ -" [REAL (rhs q___), REAL v_v, real_REAL Q]); " ^ -" Q__ = Rewrite Querkraft_Moment True Q__; " ^ -" (M__::bool) = " ^ -" (SubProblem (Biegelinie_,[named,integrate,function], " ^ +" [REAL (rhs q___q), REAL v_v, REAL_REAL Q]); " ^ +" Q__Q = Rewrite Querkraft_Moment True Q__Q; " ^ +" (M__M::bool) = " ^ +" (SubProblem (Biegelinie',[named,integrate,function], " ^ " [diff,integration,named]) " ^ -" [REAL (rhs Q__), REAL v_v, real_REAL M_b]); " ^ -" e1__ = nth_ 1 rm_; " ^ -" (x1__::real) = argument_in (lhs e1__); " ^ -" (M1__::bool) = (Substitute [v_ = x1__]) M__; " ^ -" M1__ = (Substitute [e1__]) M1__ ; " ^ -" M2__ = Take M__; " ^ -(*without this Take 'Substitute [v_ = x2__]' takes _last formula from ctree_*) -" e2__ = nth_ 2 rm_; " ^ -" (x2__::real) = argument_in (lhs e2__); " ^ -" (M2__::bool) = ((Substitute [v_ = x2__]) @@ " ^ -" (Substitute [e2__])) M2__; " ^ -" (c_1_2__::bool list) = " ^ -" (SubProblem (Biegelinie_,[linear,system],[no_met]) " ^ -" [booll_ [M1__, M2__], reall [c,c_2]]); " ^ -" M__ = Take M__; " ^ -" M__ = ((Substitute c_1_2__) @@ " ^ +" [REAL (rhs Q__Q), REAL v_v, REAL_REAL M_b]); " ^ +" e__1 = NTH 1 r_m; " ^ +" (x__1::real) = argument_in (lhs e__1); " ^ +" (M__1::bool) = (Substitute [v_v = x__1]) M__M; " ^ +" M__1 = (Substitute [e__1]) M__1 ; " ^ +" M__2 = Take M__M; " ^ +(*without this Take 'Substitute [v_v = x__2]' takes _last formula from ctree_*) +" e__2 = NTH 2 r_m; " ^ +" (x__2::real) = argument_in (lhs e__2); " ^ +" (M__2::bool) = ((Substitute [v_v = x__2]) @@ " ^ +" (Substitute [e__2])) M__2; " ^ +" (c_1_2::bool list) = " ^ +" (SubProblem (Biegelinie',[linear,system],[no_met]) " ^ +" [BOOL_LIST [M__1, M__2], REAL_LIST [c,c_2]]); " ^ +" M__M = Take M__M; " ^ +" M__M = ((Substitute c_1_2) @@ " ^ " (Try (Rewrite_Set_Inst [(bdv_1, c),(bdv_2, c_2)]" ^ " simplify_System False)) @@ " ^ " (Rewrite Moment_Neigung False) @@ " ^ -" (Rewrite make_fun_explicit False)) M__; " ^ +" (Rewrite make_fun_explicit False)) M__M; " ^ (*----------------------- and the same once more ------------------------*) -" (N__:: bool) = " ^ -" (SubProblem (Biegelinie_,[named,integrate,function], " ^ +" (N__N:: bool) = " ^ +" (SubProblem (Biegelinie',[named,integrate,function], " ^ " [diff,integration,named]) " ^ -" [REAL (rhs M__), REAL v_v, real_REAL y']); " ^ -" (B__:: bool) = " ^ -" (SubProblem (Biegelinie_,[named,integrate,function], " ^ +" [REAL (rhs M__M), REAL v_v, REAL_REAL y']); " ^ +" (B__B:: bool) = " ^ +" (SubProblem (Biegelinie',[named,integrate,function], " ^ " [diff,integration,named]) " ^ -" [REAL (rhs N__), REAL v_v, real_REAL y]); " ^ -" e1__ = nth_ 1 rb_; " ^ -" (x1__::real) = argument_in (lhs e1__); " ^ -" (B1__::bool) = (Substitute [v_ = x1__]) B__; " ^ -" B1__ = (Substitute [e1__]) B1__ ; " ^ -" B2__ = Take B__; " ^ -" e2__ = nth_ 2 rb_; " ^ -" (x2__::real) = argument_in (lhs e2__); " ^ -" (B2__::bool) = ((Substitute [v_ = x2__]) @@ " ^ -" (Substitute [e2__])) B2__; " ^ -" (c_1_2__::bool list) = " ^ -" (SubProblem (Biegelinie_,[linear,system],[no_met]) " ^ -" [booll_ [B1__, B2__], reall [c,c_2]]); " ^ -" B__ = Take B__; " ^ -" B__ = ((Substitute c_1_2__) @@ " ^ -" (Rewrite_Set_Inst [(bdv, x)] make_ratpoly_in False)) B__ " ^ -" in B__)" +" [REAL (rhs N__N), REAL v_v, REAL_REAL y]); " ^ +" e__1 = NTH 1 r_b; " ^ +" (x__1::real) = argument_in (lhs e__1); " ^ +" (B__1::bool) = (Substitute [v_v = x__1]) B__B; " ^ +" B__1 = (Substitute [e__1]) B__1 ; " ^ +" B__2 = Take B__B; " ^ +" e__2 = NTH 2 r_b; " ^ +" (x__2::real) = argument_in (lhs e__2); " ^ +" (B__2::bool) = ((Substitute [v_v = x__2]) @@ " ^ +" (Substitute [e__2])) B__2; " ^ +" (c_1_2::bool list) = " ^ +" (SubProblem (Biegelinie',[linear,system],[no_met]) " ^ +" [BOOL_LIST [B__1, B__2], REAL_LIST [c,c_2]]); " ^ +" B__B = Take B__B; " ^ +" B__B = ((Substitute c_1_2) @@ " ^ +" (Rewrite_Set_Inst [(bdv, x)] make_ratpoly_in False)) B__B " ^ +" in B__B)" )); +*} +ML {* store_met (prep_met thy "met_biege_2" [] e_metID (["IntegrierenUndKonstanteBestimmen2"], - [("#Given" ,["Traegerlaenge l_", "Streckenlast q__", + [("#Given" ,["Traegerlaenge l_l", "Streckenlast q__q", "FunktionsVariable v_v"]), - (*("#Where",["0 < l_"]), ...wait for < and handling Arbfix*) - ("#Find" ,["Biegelinie b_"]), - ("#Relate",["Randbedingungen rb_"]) + (*("#Where",["0 < l_l"]), ...wait for < and handling Arbfix*) + ("#Find" ,["Biegelinie b_b"]), + ("#Relate",["Randbedingungen r_b"]) ], {rew_ord'="tless_true", rls' = append_rls "erls_IntegrierenUndK.." e_rls @@ -326,25 +331,27 @@ ], prls = Erls, crls = Atools_erls, nrls = Erls}, "Script Biegelinie2Script " ^ -"(l_::real) (q__::real) (v_v::real) (b_::real=>real) (rb_::bool list) = " ^ +"(l_l::real) (q__q::real) (v_v::real) (b_b::real=>real) (r_b::bool list) = " ^ " (let " ^ -" (funs_:: bool list) = " ^ -" (SubProblem (Biegelinie_,[vonBelastungZu,Biegelinien], " ^ +" (fun_s:: bool list) = " ^ +" (SubProblem (Biegelinie',[vonBelastungZu,Biegelinien], " ^ " [Biegelinien,ausBelastung]) " ^ -" [REAL q__, REAL v_]); " ^ -" (equs_::bool list) = " ^ -" (SubProblem (Biegelinie_,[setzeRandbedingungen,Biegelinien]," ^ +" [REAL q__q, REAL v_v]); " ^ +" (equ_s::bool list) = " ^ +" (SubProblem (Biegelinie',[setzeRandbedingungen,Biegelinien]," ^ " [Biegelinien,setzeRandbedingungenEin]) " ^ -" [booll_ funs_, booll_ rb_]); " ^ -" (cons_::bool list) = " ^ -" (SubProblem (Biegelinie_,[linear,system],[no_met]) " ^ -" [booll_ equs_, reall [c,c_2,c_3,c_4]]); " ^ -" B_ = Take (lastI funs_); " ^ -" B_ = ((Substitute cons_) @@ " ^ -" (Rewrite_Set_Inst [(bdv, v_v)] make_ratpoly_in False)) B_ " ^ -" in B_)" +" [BOOL_LIST fun_s, BOOL_LIST r_b]); " ^ +" (con_s::bool list) = " ^ +" (SubProblem (Biegelinie',[linear,system],[no_met]) " ^ +" [BOOL_LIST equ_s, REAL_LIST [c,c_2,c_3,c_4]]); " ^ +" B_B = Take (lastI fun_s); " ^ +" B_B = ((Substitute con_s) @@ " ^ +" (Rewrite_Set_Inst [(bdv, v_v)] make_ratpoly_in False)) B_B " ^ +" in B_B)" )); +*} +ML {* store_met (prep_met thy "met_biege_intconst_2" [] e_metID (["IntegrierenUndKonstanteBestimmen","2xIntegrieren"], @@ -389,11 +396,13 @@ "empty_script" )); +*} +ML {* store_met (prep_met thy "met_biege_ausbelast" [] e_metID (["Biegelinien","ausBelastung"], - [("#Given" ,["Streckenlast q__","FunktionsVariable v_v"]), - ("#Find" ,["Funktionen funs_"])], + [("#Given" ,["Streckenlast q__q","FunktionsVariable v_v"]), + ("#Find" ,["Funktionen fun_s"])], {rew_ord'="tless_true", rls' = append_rls "erls_ausBelastung" e_rls [Calc ("Atools.ident",eval_ident "#ident_"), @@ -403,118 +412,121 @@ srls = append_rls "srls_ausBelastung" e_rls [Calc("Tools.rhs", eval_rhs"eval_rhs_")], prls = e_rls, crls = Atools_erls, nrls = e_rls}, -"Script Belastung2BiegelScript (q__::real) (v_v::real) = " ^ -" (let q___ = Take (q_ v_v = q__); " ^ -" q___ = ((Rewrite sym_real_minus_eq_cancel True) @@ " ^ -" (Rewrite Belastung_Querkraft True)) q___; " ^ -" (Q__:: bool) = " ^ -" (SubProblem (Biegelinie_,[named,integrate,function], " ^ +"Script Belastung2BiegelScript (q__q::real) (v_v::real) = " ^ +" (let q___q = Take (q_q v_v = q__q); " ^ +" q___q = ((Rewrite sym_real_minus_eq_cancel True) @@ " ^ +" (Rewrite Belastung_Querkraft True)) q___q; " ^ +" (Q__Q:: bool) = " ^ +" (SubProblem (Biegelinie',[named,integrate,function], " ^ " [diff,integration,named]) " ^ -" [REAL (rhs q___), REAL v_v, real_REAL Q]); " ^ -" M__ = Rewrite Querkraft_Moment True Q__; " ^ -" (M__::bool) = " ^ -" (SubProblem (Biegelinie_,[named,integrate,function], " ^ +" [REAL (rhs q___q), REAL v_v, REAL_REAL Q]); " ^ +" M__M = Rewrite Querkraft_Moment True Q__Q; " ^ +" (M__M::bool) = " ^ +" (SubProblem (Biegelinie',[named,integrate,function], " ^ " [diff,integration,named]) " ^ -" [REAL (rhs M__), REAL v_v, real_REAL M_b]); " ^ -" N__ = ((Rewrite Moment_Neigung False) @@ " ^ -" (Rewrite make_fun_explicit False)) M__; " ^ -" (N__:: bool) = " ^ -" (SubProblem (Biegelinie_,[named,integrate,function], " ^ +" [REAL (rhs M__M), REAL v_v, REAL_REAL M_b]); " ^ +" N__N = ((Rewrite Moment_Neigung False) @@ " ^ +" (Rewrite make_fun_explicit False)) M__M; " ^ +" (N__N:: bool) = " ^ +" (SubProblem (Biegelinie',[named,integrate,function], " ^ " [diff,integration,named]) " ^ -" [REAL (rhs N__), REAL v_v, real_REAL y']); " ^ -" (B__:: bool) = " ^ -" (SubProblem (Biegelinie_,[named,integrate,function], " ^ +" [REAL (rhs N__N), REAL v_v, REAL_REAL y']); " ^ +" (B__B:: bool) = " ^ +" (SubProblem (Biegelinie',[named,integrate,function], " ^ " [diff,integration,named]) " ^ -" [REAL (rhs N__), REAL v_v, real_REAL y]) " ^ -" in [Q__, M__, N__, B__])" +" [REAL (rhs N__N), REAL v_v, REAL_REAL y]) " ^ +" in [Q__Q, M__M, N__N, B__B])" )); +*} +ML {* store_met (prep_met thy "met_biege_setzrand" [] e_metID (["Biegelinien","setzeRandbedingungenEin"], - [("#Given" ,["Funktionen funs_","Randbedingungen rb_"]), - ("#Find" ,["Gleichungen equs___"])], + [("#Given" ,["Funktionen fun_s","Randbedingungen r_b"]), + ("#Find" ,["Gleichungen equs'''"])], {rew_ord'="tless_true", rls'=Erls, calc = [], srls = srls2, prls=e_rls, crls = Atools_erls, nrls = e_rls}, -"Script SetzeRandbedScript (funs_::bool list) (rb_::bool list) = " ^ -" (let b1_ = nth_ 1 rb_; " ^ -" fs_ = filter_sameFunId (lhs b1_) funs_; " ^ -" (e1_::bool) = " ^ -" (SubProblem (Biegelinie_,[makeFunctionTo,equation]," ^ +"Script SetzeRandbedScript (fun_s::bool list) (r_b::bool list) = " ^ +" (let b_1 = NTH 1 r_b; " ^ +" f_s = filter_sameFunId (lhs b_1) fun_s; " ^ +" (e_1::bool) = " ^ +" (SubProblem (Biegelinie',[makeFunctionTo,equation]," ^ " [Equation,fromFunction]) " ^ -" [BOOL (hd fs_), BOOL b1_]); " ^ -" b2_ = nth_ 2 rb_; " ^ -" fs_ = filter_sameFunId (lhs b2_) funs_; " ^ -" (e2_::bool) = " ^ -" (SubProblem (Biegelinie_,[makeFunctionTo,equation]," ^ +" [BOOL (hd f_s), BOOL b_1]); " ^ +" b_2 = NTH 2 r_b; " ^ +" f_s = filter_sameFunId (lhs b_2) fun_s; " ^ +" (e_2::bool) = " ^ +" (SubProblem (Biegelinie',[makeFunctionTo,equation]," ^ " [Equation,fromFunction]) " ^ -" [BOOL (hd fs_), BOOL b2_]); " ^ -" b3_ = nth_ 3 rb_; " ^ -" fs_ = filter_sameFunId (lhs b3_) funs_; " ^ -" (e3_::bool) = " ^ -" (SubProblem (Biegelinie_,[makeFunctionTo,equation]," ^ +" [BOOL (hd f_s), BOOL b_2]); " ^ +" b_3 = NTH 3 r_b; " ^ +" f_s = filter_sameFunId (lhs b_3) fun_s; " ^ +" (e_3::bool) = " ^ +" (SubProblem (Biegelinie',[makeFunctionTo,equation]," ^ " [Equation,fromFunction]) " ^ -" [BOOL (hd fs_), BOOL b3_]); " ^ -" b4_ = nth_ 4 rb_; " ^ -" fs_ = filter_sameFunId (lhs b4_) funs_; " ^ -" (e4_::bool) = " ^ -" (SubProblem (Biegelinie_,[makeFunctionTo,equation]," ^ +" [BOOL (hd f_s), BOOL b_3]); " ^ +" b_4 = NTH 4 r_b; " ^ +" f_s = filter_sameFunId (lhs b_4) fun_s; " ^ +" (e_4::bool) = " ^ +" (SubProblem (Biegelinie',[makeFunctionTo,equation]," ^ " [Equation,fromFunction]) " ^ -" [BOOL (hd fs_), BOOL b4_]) " ^ -" in [e1_,e2_,e3_,e4_])" +" [BOOL (hd f_s), BOOL b_4]) " ^ +" in [e_1,e_2,e_3,e_4])" (* filter requires more than 1 sec !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!! -"Script SetzeRandbedScript (funs_::bool list) (rb_::bool list) = " ^ -" (let b1_ = nth_ 1 rb_; " ^ -" fs_ = filter (sameFunId (lhs b1_)) funs_; " ^ -" (e1_::bool) = " ^ -" (SubProblem (Biegelinie_,[makeFunctionTo,equation]," ^ +"Script SetzeRandbedScript (fun_s::bool list) (r_b::bool list) = " ^ +" (let b_1 = NTH 1 r_b; " ^ +" f_s = filter (sameFunId (lhs b_1)) fun_s; " ^ +" (e_1::bool) = " ^ +" (SubProblem (Biegelinie',[makeFunctionTo,equation]," ^ " [Equation,fromFunction]) " ^ -" [BOOL (hd fs_), BOOL b1_]); " ^ -" b2_ = nth_ 2 rb_; " ^ -" fs_ = filter (sameFunId (lhs b2_)) funs_; " ^ -" (e2_::bool) = " ^ -" (SubProblem (Biegelinie_,[makeFunctionTo,equation]," ^ +" [BOOL (hd f_s), BOOL b_1]); " ^ +" b_2 = NTH 2 r_b; " ^ +" f_s = filter (sameFunId (lhs b_2)) fun_s; " ^ +" (e_2::bool) = " ^ +" (SubProblem (Biegelinie',[makeFunctionTo,equation]," ^ " [Equation,fromFunction]) " ^ -" [BOOL (hd fs_), BOOL b2_]); " ^ -" b3_ = nth_ 3 rb_; " ^ -" fs_ = filter (sameFunId (lhs b3_)) funs_; " ^ -" (e3_::bool) = " ^ -" (SubProblem (Biegelinie_,[makeFunctionTo,equation]," ^ +" [BOOL (hd f_s), BOOL b_2]); " ^ +" b_3 = NTH 3 r_b; " ^ +" f_s = filter (sameFunId (lhs b_3)) fun_s; " ^ +" (e_3::bool) = " ^ +" (SubProblem (Biegelinie',[makeFunctionTo,equation]," ^ " [Equation,fromFunction]) " ^ -" [BOOL (hd fs_), BOOL b3_]); " ^ -" b4_ = nth_ 4 rb_; " ^ -" fs_ = filter (sameFunId (lhs b4_)) funs_; " ^ -" (e4_::bool) = " ^ -" (SubProblem (Biegelinie_,[makeFunctionTo,equation]," ^ +" [BOOL (hd f_s), BOOL b_3]); " ^ +" b_4 = NTH 4 r_b; " ^ +" f_s = filter (sameFunId (lhs b_4)) fun_s; " ^ +" (e_4::bool) = " ^ +" (SubProblem (Biegelinie',[makeFunctionTo,equation]," ^ " [Equation,fromFunction]) " ^ -" [BOOL (hd fs_), BOOL b4_]) " ^ -" in [e1_,e2_,e3_,e4_])"*) +" [BOOL (hd f_s), BOOL b_4]) " ^ +" in [e_1,e_2,e_3,e_4])"*) )); +*} +ML {* store_met (prep_met thy "met_equ_fromfun" [] e_metID (["Equation","fromFunction"], - [("#Given" ,["functionEq fun_","substitution sub_"]), - ("#Find" ,["equality equ___"])], + [("#Given" ,["functionEq fu_n","substitution su_b"]), + ("#Find" ,["equality equ'''"])], {rew_ord'="tless_true", rls'=Erls, calc = [], srls = append_rls "srls_in_EquationfromFunc" e_rls [Calc("Tools.lhs", eval_lhs"eval_lhs_"), Calc("Atools.argument'_in", eval_argument_in "Atools.argument'_in")], - prls=e_rls, - crls = Atools_erls, nrls = e_rls}, + prls=e_rls, crls = Atools_erls, nrls = e_rls}, (*(M_b x = c_2 + c * x + -1 * q_0 / 2 * x ^^^ 2) (M_b L = 0) --> 0 = c_2 + c * L + -1 * q_0 / 2 * L ^^^ 2*) -"Script Function2Equality (fun_::bool) (sub_::bool) =" ^ -" (let fun_ = Take fun_; " ^ -" bdv_ = argument_in (lhs fun_); " ^ -" val_ = argument_in (lhs sub_); " ^ -" equ_ = (Substitute [bdv_ = val_]) fun_; " ^ -" equ_ = (Substitute [sub_]) fun_ " ^ -" in (Rewrite_Set norm_Rational False) equ_) " +"Script Function2Equality (fu_n::bool) (su_b::bool) =" ^ +" (let fu_n = Take fu_n; " ^ +" bd_v = argument_in (lhs fu_n); " ^ +" va_l = argument_in (lhs su_b); " ^ +" eq_u = (Substitute [bd_v = va_l]) fu_n; " ^ +" eq_u = (Substitute [su_b]) fu_n " ^ +" in (Rewrite_Set norm_Rational False) eq_u) " )); *}