Mercurial Mercurial > wneuper > isa / file revision
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
src/Tools/isac/Knowledge/Biegelinie.thy
author Walther Neuper <neuper@ist.tugraz.at>
Mon, 06 Sep 2010 16:56:22 +0200
branchisac-update-Isa09-2
changeset 37983 03bfbc480107
parent 37982 66f3570ba808
child 37984 972a73d7c50b
permissions -rw-r--r--
corrected format for axioms in remaining theories 
     1 (* chapter 'Biegelinie' from the textbook: 

     2    Timischl, Kaiser. Ingenieur-Mathematik 3. Wien 1999. p.268-271.

     3    author: Walther Neuper

     4    050826,

     5    (c) due to copyright terms

     6 *)

     7 

     8 theory Biegelinie imports Integrate Equation EqSystem begin

     9 

    10 consts

    11 

    12   q_    :: real => real ("q'_")     (* Streckenlast               *)

    13   Q     :: real => real             (* Querkraft                  *)

    14   Q'    :: real => real             (* Ableitung der Querkraft    *)

    15   M'_b  :: real => real ("M'_b")    (* Biegemoment                *)

    16   M'_b' :: real => real ("M'_b'")   (* Ableitung des Biegemoments *)

    17   y''   :: real => real             (* 2.Ableitung der Biegeline  *)

    18   y'    :: real => real             (* Neigung der Biegeline      *)

    19 (*y     :: real => real             (* Biegeline                  *)*)

    20   EI    :: real                     (* Biegesteifigkeit           *)

    21 

    22   (*new Descriptions in the related problems*)

    23   Traegerlaenge            :: real => una

    24   Streckenlast             :: real => una

    25   BiegemomentVerlauf       :: bool => una

    26   Biegelinie               :: (real => real) => una

    27   Randbedingungen          :: bool list => una

    28   RandbedingungenBiegung   :: bool list => una

    29   RandbedingungenNeigung   :: bool list => una

    30   RandbedingungenMoment    :: bool list => una

    31   RandbedingungenQuerkraft :: bool list => una

    32   FunktionsVariable        :: real => una

    33   Funktionen               :: bool list => una

    34   Gleichungen              :: bool list => una

    35 

    36   (*Script-names*)

    37   Biegelinie2Script        :: "[real,real,real,real=>real,bool list,

    38 				bool] => bool"	

    39 	("((Script Biegelinie2Script (_ _ _ _ _ =))// (_))" 9)

    40   BiegelinieScript         :: "[real,real,real,real=>real,bool list,bool list,

    41 				bool] => bool"	

    42 	("((Script BiegelinieScript (_ _ _ _ _ _ =))// (_))" 9)

    43   Biege2xIntegrierenScript :: "[real,real,real,bool,real=>real,bool list,

    44 				bool] => bool"		

    45 	("((Script Biege2xIntegrierenScript (_ _ _ _ _ _ =))// (_))" 9)

    46   Biege4x4SystemScript     :: "[real,real,real,real=>real,bool list,  

    47 				bool] => bool"	

    48 	("((Script Biege4x4SystemScript (_ _ _ _ _ =))// (_))" 9)

    49   Biege1xIntegrierenScript :: 

    50 	            "[real,real,real,real=>real,bool list,bool list,bool list,

    51 		      bool] => bool"	

    52 	("((Script Biege1xIntegrierenScript (_ _ _ _ _ _ _ =))// (_))" 9)

    53   Belastung2BiegelScript   :: "[real,real,

    54 	                        bool list] => bool list"	

    55 	("((Script Belastung2BiegelScript (_ _ =))// (_))" 9)

    56   SetzeRandbedScript       :: "[bool list,bool list,

    57 	                        bool list] => bool list"	

    58 	("((Script SetzeRandbedScript (_ _ =))// (_))" 9)

    59 

    60 axioms

    61 

    62   Querkraft_Belastung:   "Q' x = -q_ x"

    63   Belastung_Querkraft:   "-q_ x = Q' x"

    64 

    65   Moment_Querkraft:      "M_b' x = Q x"

    66   Querkraft_Moment:      "Q x = M_b' x"

    67 

    68   Neigung_Moment:        "y'' x = -M_b x/ EI"

    69   Moment_Neigung:        "M_b x = -EI * y'' x"

    70 

    71   (*according to rls 'simplify_Integral': .. = 1/a * .. instead .. = ../ a*)

    72   make_fun_explicit:     "Not (a =!= 0) ==> (a * (f x) = b) = (f x = 1/a * b)"

    73 

    74 ML {*

    75 val thy = @{theory};

    76 

    77 (** theory elements for transfer into html **)

    78 

    79 store_isa ["IsacKnowledge"] [];

    80 store_thy thy 

    81 	  ["Walther Neuper 2005 supported by a grant from NMI Austria"];

    82 store_isa ["IsacKnowledge", theory2thyID thy, "Theorems"] 

    83 	  ["Walther Neuper 2005 supported by a grant from NMI Austria"];

    84 store_thm thy ("Belastung_Querkraft", Belastung_Querkraft)

    85 	  ["Walther Neuper 2005 supported by a grant from NMI Austria"];

    86 store_thm thy ("Moment_Neigung", Moment_Neigung)

    87 	  ["Walther Neuper 2005 supported by a grant from NMI Austria"];

    88 store_thm thy ("Moment_Querkraft", Moment_Querkraft)

    89 	  ["Walther Neuper 2005 supported by a grant from NMI Austria"];

    90 store_thm thy ("Neigung_Moment", Neigung_Moment)

    91 	  ["Walther Neuper 2005 supported by a grant from NMI Austria"];

    92 store_thm thy ("Querkraft_Belastung", Querkraft_Belastung)

    93 	  ["Walther Neuper 2005 supported by a grant from NMI Austria"];

    94 store_thm thy ("Querkraft_Moment", Querkraft_Moment)

    95 	  ["Walther Neuper 2005 supported by a grant from NMI Austria"];

    96 store_thm thy ("make_fun_explicit", make_fun_explicit)

    97 	  ["Walther Neuper 2005 supported by a grant from NMI Austria"];

    98 

    99 

   100 (** problems **)

   101 

   102 store_pbt

   103  (prep_pbt thy "pbl_bieg" [] e_pblID

   104  (["Biegelinien"],

   105   [("#Given" ,["Traegerlaenge l_", "Streckenlast q__"]),

   106    (*("#Where",["0 < l_"]), ...wait for &lt; and handling Arbfix*)

   107    ("#Find"  ,["Biegelinie b_"]),

   108    ("#Relate",["Randbedingungen rb_"])

   109   ],

   110   append_rls "e_rls" e_rls [], 

   111   NONE, 

   112   [["IntegrierenUndKonstanteBestimmen2"]]));

   113 

   114 store_pbt 

   115  (prep_pbt thy "pbl_bieg_mom" [] e_pblID

   116  (["MomentBestimmte","Biegelinien"],

   117   [("#Given" ,["Traegerlaenge l_", "Streckenlast q__"]),

   118    (*("#Where",["0 < l_"]), ...wait for &lt; and handling Arbfix*)

   119    ("#Find"  ,["Biegelinie b_"]),

   120    ("#Relate",["RandbedingungenBiegung rb_","RandbedingungenMoment rm_"])

   121   ],

   122   append_rls "e_rls" e_rls [], 

   123   NONE, 

   124   [["IntegrierenUndKonstanteBestimmen"]]));

   125 

   126 store_pbt

   127  (prep_pbt thy "pbl_bieg_momg" [] e_pblID

   128  (["MomentGegebene","Biegelinien"],

   129   [],

   130   append_rls "e_rls" e_rls [], 

   131   NONE, 

   132   [["IntegrierenUndKonstanteBestimmen","2xIntegrieren"]]));

   133 

   134 store_pbt

   135  (prep_pbt thy "pbl_bieg_einf" [] e_pblID

   136  (["einfache","Biegelinien"],

   137   [],

   138   append_rls "e_rls" e_rls [], 

   139   NONE, 

   140   [["IntegrierenUndKonstanteBestimmen","4x4System"]]));

   141 

   142 store_pbt

   143  (prep_pbt thy "pbl_bieg_momquer" [] e_pblID

   144  (["QuerkraftUndMomentBestimmte","Biegelinien"],

   145   [],

   146   append_rls "e_rls" e_rls [], 

   147   NONE, 

   148   [["IntegrierenUndKonstanteBestimmen","1xIntegrieren"]]));

   149 

   150 store_pbt

   151  (prep_pbt thy "pbl_bieg_vonq" [] e_pblID

   152  (["vonBelastungZu","Biegelinien"],

   153   [("#Given" ,["Streckenlast q__","FunktionsVariable v_v"]),

   154    ("#Find"  ,["Funktionen funs___"])],

   155   append_rls "e_rls" e_rls [], 

   156   NONE, 

   157   [["Biegelinien","ausBelastung"]]));

   158 

   159 store_pbt

   160  (prep_pbt thy "pbl_bieg_randbed" [] e_pblID

   161  (["setzeRandbedingungen","Biegelinien"],

   162   [("#Given" ,["Funktionen funs_","Randbedingungen rb_"]),

   163    ("#Find"  ,["Gleichungen equs___"])],

   164   append_rls "e_rls" e_rls [], 

   165   NONE, 

   166   [["Biegelinien","setzeRandbedingungenEin"]]));

   167 

   168 store_pbt

   169  (prep_pbt thy "pbl_equ_fromfun" [] e_pblID

   170  (["makeFunctionTo","equation"],

   171   [("#Given" ,["functionEq fun_","substitution sub_"]),

   172    ("#Find"  ,["equality equ___"])],

   173   append_rls "e_rls" e_rls [], 

   174   NONE, 

   175   [["Equation","fromFunction"]]));

   176 

   177 

   178 (** methods **)

   179 

   180 val srls = Rls {id="srls_IntegrierenUnd..", 

   181 		preconds = [], 

   182 		rew_ord = ("termlessI",termlessI), 

   183 		erls = append_rls "erls_in_srls_IntegrierenUnd.." e_rls

   184 				  [(*for asm in nth_Cons_ ...*)

   185 				   Calc ("op <",eval_equ "#less_"),

   186 				   (*2nd nth_Cons_ pushes n+-1 into asms*)

   187 				   Calc("op +", eval_binop "#add_")

   188 				   ], 

   189 		srls = Erls, calc = [],

   190 		rules = [Thm ("nth_Cons_",num_str @{thm nth_Cons_}),

   191 			 Calc("op +", eval_binop "#add_"),

   192 			 Thm ("nth_Nil_",num_str @{thm nth_Nil_}),

   193 			 Calc("Tools.lhs", eval_lhs"eval_lhs_"),

   194 			 Calc("Tools.rhs", eval_rhs"eval_rhs_"),

   195 			 Calc("Atools.argument'_in",

   196 			      eval_argument_in "Atools.argument'_in")

   197 			 ],

   198 		scr = EmptyScr};

   199     

   200 val srls2 = 

   201     Rls {id="srls_IntegrierenUnd..", 

   202 	 preconds = [], 

   203 	 rew_ord = ("termlessI",termlessI), 

   204 	 erls = append_rls "erls_in_srls_IntegrierenUnd.." e_rls

   205 			   [(*for asm in nth_Cons_ ...*)

   206 			    Calc ("op <",eval_equ "#less_"),

   207 			    (*2nd nth_Cons_ pushes n+-1 into asms*)

   208 			    Calc("op +", eval_binop "#add_")

   209 			    ], 

   210 	 srls = Erls, calc = [],

   211 	 rules = [Thm ("nth_Cons_",num_str @{thm nth_Cons_}),

   212 		  Calc("op +", eval_binop "#add_"),

   213 		  Thm ("nth_Nil_", num_str @{thm nth_Nil_}),

   214 		  Calc("Tools.lhs", eval_lhs "eval_lhs_"),

   215 		  Calc("Atools.filter'_sameFunId",

   216 		       eval_filter_sameFunId "Atools.filter'_sameFunId"),

   217 		  (*WN070514 just for smltest/../biegelinie.sml ...*)

   218 		  Calc("Atools.sameFunId", eval_sameFunId "Atools.sameFunId"),

   219 		  Thm ("filter_Cons", num_str @{thm filter_Cons}),

   220 		  Thm ("filter_Nil", num_str @{thm filter_Nil}),

   221 		  Thm ("if_True", num_str @{thm if_True}),

   222 		  Thm ("if_False", num_str @{thm if_False}),

   223 		  Thm ("hd_thm", num_str @{thm hd_thm})

   224 		  ],

   225 	 scr = EmptyScr};

   226  

   227 store_met

   228     (prep_met thy "met_biege" [] e_metID

   229 	      (["IntegrierenUndKonstanteBestimmen"],

   230 	       [("#Given" ,["Traegerlaenge l_", "Streckenlast q__",

   231 			    "FunktionsVariable v_v"]),

   232 		(*("#Where",["0 < l_"]), ...wait for &lt; and handling Arbfix*)

   233 		("#Find"  ,["Biegelinie b_"]),

   234 		("#Relate",["RandbedingungenBiegung rb_",

   235 			    "RandbedingungenMoment rm_"])

   236 		],

   237 	       {rew_ord'="tless_true", 

   238 		rls' = append_rls "erls_IntegrierenUndK.." e_rls 

   239 				  [Calc ("Atools.ident",eval_ident "#ident_"),

   240 				   Thm ("not_true",num_str @{thm not_true}),

   241 				   Thm ("not_false",num_str @{thm not_false})], 

   242 		calc = [], srls = srls, prls = Erls,

   243 		crls = Atools_erls, nrls = Erls},

   244 "Script BiegelinieScript                                                  " ^

   245 "(l_::real) (q__::real) (v_v::real) (b_::real=>real)                       " ^

   246 "(rb_::bool list) (rm_::bool list) =                                      " ^

   247 "  (let q___ = Take (q_ v_v = q__);                                        " ^

   248 "       q___ = ((Rewrite sym_real_minus_eq_cancel True) @@                " ^

   249 "              (Rewrite Belastung_Querkraft True)) q___;                  " ^

   250 "      (Q__:: bool) =                                                     " ^

   251 "             (SubProblem (Biegelinie_,[named,integrate,function],        " ^

   252 "                          [diff,integration,named])                      " ^

   253 "                          [real_ (rhs q___), real_ v_v, real_real_ Q]);   " ^

   254 "       Q__ = Rewrite Querkraft_Moment True Q__;                          " ^

   255 "      (M__::bool) =                                                      " ^

   256 "             (SubProblem (Biegelinie_,[named,integrate,function],        " ^

   257 "                          [diff,integration,named])                      " ^

   258 "                          [real_ (rhs Q__), real_ v_v, real_real_ M_b]);  " ^

   259 "       e1__ = nth_ 1 rm_;                                                " ^

   260 "      (x1__::real) = argument_in (lhs e1__);                             " ^

   261 "      (M1__::bool) = (Substitute [v_ = x1__]) M__;                       " ^

   262 "       M1__        = (Substitute [e1__]) M1__ ;                          " ^

   263 "       M2__ = Take M__;                                                  " ^

   264 (*without this Take 'Substitute [v_ = x2__]' takes _last formula from ctree_*)

   265 "       e2__ = nth_ 2 rm_;                                                " ^

   266 "      (x2__::real) = argument_in (lhs e2__);                             " ^

   267 "      (M2__::bool) = ((Substitute [v_ = x2__]) @@                        " ^

   268 "                      (Substitute [e2__])) M2__;                         " ^

   269 "      (c_1_2__::bool list) =                                             " ^

   270 "             (SubProblem (Biegelinie_,[linear,system],[no_met])          " ^

   271 "                          [booll_ [M1__, M2__], reall [c,c_2]]);         " ^

   272 "       M__ = Take  M__;                                                  " ^

   273 "       M__ = ((Substitute c_1_2__) @@                                    " ^

   274 "              (Try (Rewrite_Set_Inst [(bdv_1, c),(bdv_2, c_2)]" ^

   275 "                                   simplify_System False)) @@ " ^

   276 "              (Rewrite Moment_Neigung False) @@ " ^

   277 "              (Rewrite make_fun_explicit False)) M__;                    " ^

   278 (*----------------------- and the same once more ------------------------*)

   279 "      (N__:: bool) =                                                     " ^

   280 "             (SubProblem (Biegelinie_,[named,integrate,function],        " ^

   281 "                          [diff,integration,named])                      " ^

   282 "                          [real_ (rhs M__), real_ v_v, real_real_ y']);   " ^

   283 "      (B__:: bool) =                                                     " ^

   284 "             (SubProblem (Biegelinie_,[named,integrate,function],        " ^

   285 "                          [diff,integration,named])                      " ^

   286 "                          [real_ (rhs N__), real_ v_v, real_real_ y]);    " ^

   287 "       e1__ = nth_ 1 rb_;                                                " ^

   288 "      (x1__::real) = argument_in (lhs e1__);                             " ^

   289 "      (B1__::bool) = (Substitute [v_ = x1__]) B__;                       " ^

   290 "       B1__        = (Substitute [e1__]) B1__ ;                          " ^

   291 "       B2__ = Take B__;                                                  " ^

   292 "       e2__ = nth_ 2 rb_;                                                " ^

   293 "      (x2__::real) = argument_in (lhs e2__);                             " ^

   294 "      (B2__::bool) = ((Substitute [v_ = x2__]) @@                        " ^

   295 "                      (Substitute [e2__])) B2__;                         " ^

   296 "      (c_1_2__::bool list) =                                             " ^

   297 "             (SubProblem (Biegelinie_,[linear,system],[no_met])          " ^

   298 "                          [booll_ [B1__, B2__], reall [c,c_2]]);         " ^

   299 "       B__ = Take  B__;                                                  " ^

   300 "       B__ = ((Substitute c_1_2__) @@                                    " ^

   301 "              (Rewrite_Set_Inst [(bdv, x)] make_ratpoly_in False)) B__   " ^

   302 " in B__)"

   303 ));

   304 

   305 store_met

   306     (prep_met thy "met_biege_2" [] e_metID

   307 	      (["IntegrierenUndKonstanteBestimmen2"],

   308 	       [("#Given" ,["Traegerlaenge l_", "Streckenlast q__",

   309 			    "FunktionsVariable v_v"]),

   310 		(*("#Where",["0 < l_"]), ...wait for &lt; and handling Arbfix*)

   311 		("#Find"  ,["Biegelinie b_"]),

   312 		("#Relate",["Randbedingungen rb_"])

   313 		],

   314 	       {rew_ord'="tless_true", 

   315 		rls' = append_rls "erls_IntegrierenUndK.." e_rls 

   316 				  [Calc ("Atools.ident",eval_ident "#ident_"),

   317 				   Thm ("not_true",num_str @{thm not_true}),

   318 				   Thm ("not_false",num_str @{thm not_false})], 

   319 		calc = [], 

   320 		srls = append_rls "erls_IntegrierenUndK.." e_rls 

   321 				  [Calc("Tools.rhs", eval_rhs"eval_rhs_"),

   322 				   Calc ("Atools.ident",eval_ident "#ident_"),

   323 				   Thm ("last_thmI",num_str @{thm last_thmI}),

   324 				   Thm ("if_True",num_str @{thm if_True}),

   325 				   Thm ("if_False",num_str @{thm if_False})

   326 				   ],

   327 		prls = Erls, crls = Atools_erls, nrls = Erls},

   328 "Script Biegelinie2Script                                                 " ^

   329 "(l_::real) (q__::real) (v_v::real) (b_::real=>real) (rb_::bool list) =    " ^

   330 "  (let                                                                   " ^

   331 "      (funs_:: bool list) =                                              " ^

   332 "             (SubProblem (Biegelinie_,[vonBelastungZu,Biegelinien],      " ^

   333 "                          [Biegelinien,ausBelastung])                    " ^

   334 "                          [real_ q__, real_ v_]);                        " ^

   335 "      (equs_::bool list) =                                               " ^

   336 "             (SubProblem (Biegelinie_,[setzeRandbedingungen,Biegelinien]," ^

   337 "                          [Biegelinien,setzeRandbedingungenEin])         " ^

   338 "                          [booll_ funs_, booll_ rb_]);                   " ^

   339 "      (cons_::bool list) =                                               " ^

   340 "             (SubProblem (Biegelinie_,[linear,system],[no_met])          " ^

   341 "                          [booll_ equs_, reall [c,c_2,c_3,c_4]]);        " ^

   342 "       B_ = Take (lastI funs_);                                          " ^

   343 "       B_ = ((Substitute cons_) @@                                       " ^

   344 "              (Rewrite_Set_Inst [(bdv, v_v)] make_ratpoly_in False)) B_   " ^

   345 " in B_)"

   346 ));

   347 

   348 store_met

   349     (prep_met thy "met_biege_intconst_2" [] e_metID

   350 	      (["IntegrierenUndKonstanteBestimmen","2xIntegrieren"],

   351 	       [],

   352 	       {rew_ord'="tless_true", rls'=Erls, calc = [], 

   353 		srls = e_rls, 

   354 		prls=e_rls,

   355 	     crls = Atools_erls, nrls = e_rls},

   356 "empty_script"

   357 ));

   358 

   359 store_met

   360     (prep_met thy "met_biege_intconst_4" [] e_metID

   361 	      (["IntegrierenUndKonstanteBestimmen","4x4System"],

   362 	       [],

   363 	       {rew_ord'="tless_true", rls'=Erls, calc = [], 

   364 		srls = e_rls, 

   365 		prls=e_rls,

   366 	     crls = Atools_erls, nrls = e_rls},

   367 "empty_script"

   368 ));

   369 

   370 store_met

   371     (prep_met thy "met_biege_intconst_1" [] e_metID

   372 	      (["IntegrierenUndKonstanteBestimmen","1xIntegrieren"],

   373 	       [],

   374 	       {rew_ord'="tless_true", rls'=Erls, calc = [], 

   375 		srls = e_rls, 

   376 		prls=e_rls,

   377 	     crls = Atools_erls, nrls = e_rls},

   378 "empty_script"

   379 ));

   380 

   381 store_met

   382     (prep_met thy "met_biege2" [] e_metID

   383 	      (["Biegelinien"],

   384 	       [],

   385 	       {rew_ord'="tless_true", rls'=Erls, calc = [], 

   386 		srls = e_rls, 

   387 		prls=e_rls,

   388 	     crls = Atools_erls, nrls = e_rls},

   389 "empty_script"

   390 ));

   391 

   392 store_met

   393     (prep_met thy "met_biege_ausbelast" [] e_metID

   394 	      (["Biegelinien","ausBelastung"],

   395 	       [("#Given" ,["Streckenlast q__","FunktionsVariable v_v"]),

   396 		("#Find"  ,["Funktionen funs_"])],

   397 	       {rew_ord'="tless_true", 

   398 		rls' = append_rls "erls_ausBelastung" e_rls 

   399 				  [Calc ("Atools.ident",eval_ident "#ident_"),

   400 				   Thm ("not_true",num_str @{thm not_true}),

   401 				   Thm ("not_false",num_str @{thm not_false})], 

   402 		calc = [], 

   403 		srls = append_rls "srls_ausBelastung" e_rls 

   404 				  [Calc("Tools.rhs", eval_rhs"eval_rhs_")], 

   405 		prls = e_rls, crls = Atools_erls, nrls = e_rls},

   406 "Script Belastung2BiegelScript (q__::real) (v_v::real) =                   " ^

   407 "  (let q___ = Take (q_ v_v = q__);                                        " ^

   408 "       q___ = ((Rewrite sym_real_minus_eq_cancel True) @@                " ^

   409 "              (Rewrite Belastung_Querkraft True)) q___;                  " ^

   410 "      (Q__:: bool) =                                                     " ^

   411 "             (SubProblem (Biegelinie_,[named,integrate,function],        " ^

   412 "                          [diff,integration,named])                      " ^

   413 "                          [real_ (rhs q___), real_ v_v, real_real_ Q]);   " ^

   414 "       M__ = Rewrite Querkraft_Moment True Q__;                          " ^

   415 "      (M__::bool) =                                                      " ^

   416 "             (SubProblem (Biegelinie_,[named,integrate,function],        " ^

   417 "                          [diff,integration,named])                      " ^

   418 "                          [real_ (rhs M__), real_ v_v, real_real_ M_b]);  " ^

   419 "       N__ = ((Rewrite Moment_Neigung False) @@                          " ^

   420 "              (Rewrite make_fun_explicit False)) M__;                    " ^

   421 "      (N__:: bool) =                                                     " ^

   422 "             (SubProblem (Biegelinie_,[named,integrate,function],        " ^

   423 "                          [diff,integration,named])                      " ^

   424 "                          [real_ (rhs N__), real_ v_v, real_real_ y']);   " ^

   425 "      (B__:: bool) =                                                     " ^

   426 "             (SubProblem (Biegelinie_,[named,integrate,function],        " ^

   427 "                          [diff,integration,named])                      " ^

   428 "                          [real_ (rhs N__), real_ v_v, real_real_ y])     " ^

   429 " in [Q__, M__, N__, B__])"

   430 ));

   431 

   432 store_met

   433     (prep_met thy "met_biege_setzrand" [] e_metID

   434 	      (["Biegelinien","setzeRandbedingungenEin"],

   435 	       [("#Given" ,["Funktionen funs_","Randbedingungen rb_"]),

   436 		("#Find"  ,["Gleichungen equs___"])],

   437 	       {rew_ord'="tless_true", rls'=Erls, calc = [], 

   438 		srls = srls2, 

   439 		prls=e_rls,

   440 	     crls = Atools_erls, nrls = e_rls},

   441 "Script SetzeRandbedScript (funs_::bool list) (rb_::bool list) = " ^

   442 " (let b1_ = nth_ 1 rb_;                                         " ^

   443 "      fs_ = filter_sameFunId (lhs b1_) funs_;                   " ^

   444 "      (e1_::bool) =                                             " ^

   445 "             (SubProblem (Biegelinie_,[makeFunctionTo,equation]," ^

   446 "                          [Equation,fromFunction])              " ^

   447 "                          [bool_ (hd fs_), bool_ b1_]);         " ^

   448 "      b2_ = nth_ 2 rb_;                                         " ^

   449 "      fs_ = filter_sameFunId (lhs b2_) funs_;                   " ^

   450 "      (e2_::bool) =                                             " ^

   451 "             (SubProblem (Biegelinie_,[makeFunctionTo,equation]," ^

   452 "                          [Equation,fromFunction])              " ^

   453 "                          [bool_ (hd fs_), bool_ b2_]);         " ^

   454 "      b3_ = nth_ 3 rb_;                                         " ^

   455 "      fs_ = filter_sameFunId (lhs b3_) funs_;                   " ^

   456 "      (e3_::bool) =                                             " ^

   457 "             (SubProblem (Biegelinie_,[makeFunctionTo,equation]," ^

   458 "                          [Equation,fromFunction])              " ^

   459 "                          [bool_ (hd fs_), bool_ b3_]);         " ^

   460 "      b4_ = nth_ 4 rb_;                                         " ^

   461 "      fs_ = filter_sameFunId (lhs b4_) funs_;                   " ^

   462 "      (e4_::bool) =                                             " ^

   463 "             (SubProblem (Biegelinie_,[makeFunctionTo,equation]," ^

   464 "                          [Equation,fromFunction])              " ^

   465 "                          [bool_ (hd fs_), bool_ b4_])          " ^

   466 " in [e1_,e2_,e3_,e4_])"

   467 (* filter requires more than 1 sec !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!

   468 "Script SetzeRandbedScript (funs_::bool list) (rb_::bool list) = " ^

   469 " (let b1_ = nth_ 1 rb_;                                         " ^

   470 "      fs_ = filter (sameFunId (lhs b1_)) funs_;                 " ^

   471 "      (e1_::bool) =                                             " ^

   472 "             (SubProblem (Biegelinie_,[makeFunctionTo,equation]," ^

   473 "                          [Equation,fromFunction])              " ^

   474 "                          [bool_ (hd fs_), bool_ b1_]);         " ^

   475 "      b2_ = nth_ 2 rb_;                                         " ^

   476 "      fs_ = filter (sameFunId (lhs b2_)) funs_;                 " ^

   477 "      (e2_::bool) =                                             " ^

   478 "             (SubProblem (Biegelinie_,[makeFunctionTo,equation]," ^

   479 "                          [Equation,fromFunction])              " ^

   480 "                          [bool_ (hd fs_), bool_ b2_]);         " ^

   481 "      b3_ = nth_ 3 rb_;                                         " ^

   482 "      fs_ = filter (sameFunId (lhs b3_)) funs_;                 " ^

   483 "      (e3_::bool) =                                             " ^

   484 "             (SubProblem (Biegelinie_,[makeFunctionTo,equation]," ^

   485 "                          [Equation,fromFunction])              " ^

   486 "                          [bool_ (hd fs_), bool_ b3_]);         " ^

   487 "      b4_ = nth_ 4 rb_;                                         " ^

   488 "      fs_ = filter (sameFunId (lhs b4_)) funs_;                 " ^

   489 "      (e4_::bool) =                                             " ^

   490 "             (SubProblem (Biegelinie_,[makeFunctionTo,equation]," ^

   491 "                          [Equation,fromFunction])              " ^

   492 "                          [bool_ (hd fs_), bool_ b4_])          " ^

   493 " in [e1_,e2_,e3_,e4_])"*)

   494 ));

   495 

   496 store_met

   497     (prep_met thy "met_equ_fromfun" [] e_metID

   498 	      (["Equation","fromFunction"],

   499 	       [("#Given" ,["functionEq fun_","substitution sub_"]),

   500 		("#Find"  ,["equality equ___"])],

   501 	       {rew_ord'="tless_true", rls'=Erls, calc = [], 

   502 		srls = append_rls "srls_in_EquationfromFunc" e_rls

   503 				  [Calc("Tools.lhs", eval_lhs"eval_lhs_"),

   504 				   Calc("Atools.argument'_in",

   505 					eval_argument_in

   506 					    "Atools.argument'_in")], 

   507 		prls=e_rls,

   508 	     crls = Atools_erls, nrls = e_rls},

   509 (*(M_b x = c_2 + c * x + -1 * q_0 / 2 * x ^^^ 2) (M_b L = 0) -->

   510        0 = c_2 + c * L + -1 * q_0 / 2 * L ^^^ 2*)

   511 "Script Function2Equality (fun_::bool) (sub_::bool) =" ^

   512 " (let fun_ = Take fun_;                             " ^

   513 "      bdv_ = argument_in (lhs fun_);                " ^

   514 "      val_ = argument_in (lhs sub_);                " ^

   515 "      equ_ = (Substitute [bdv_ = val_]) fun_;       " ^

   516 "      equ_ = (Substitute [sub_]) fun_               " ^

   517 " in (Rewrite_Set norm_Rational False) equ_)             "

   518 ));

   519 *}

   520 

   521 end

   522
wneuper/isa