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