
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 &lt; 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 &lt; 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 &lt; 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 &lt; 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: 




