wneuper/isa: src/Tools/isac/Knowledge/Biegelinie.thy@3e11e3c2dc42

     1 (* chapter 'Biegelinie' from the textbook:

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

     3    author: Walther Neuper 050826,

     4    (c) due to copyright terms

     5 *)

     7 theory Biegelinie imports Integrate Equation EqSystem begin

     9 consts

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

    12   Q     :: "real => real"             (* Querkraft                  *)

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

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

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

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

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

    18 (*y     :: "real => real"             (* Biegeline                  *)*)

    19   EI    :: "real"                     (* Biegesteifigkeit           *)

    21   (*new Descriptions in the related problems*)

    22   Traegerlaenge            :: "real => una"

    23   Streckenlast             :: "real => una"

    24   BiegemomentVerlauf       :: "bool => una"

    25   Biegelinie               :: "(real => real) => una"

    26   Randbedingungen          :: "bool list => una"

    27   RandbedingungenBiegung   :: "bool list => una"

    28   RandbedingungenNeigung   :: "bool list => una"

    29   RandbedingungenMoment    :: "bool list => una"

    30   RandbedingungenQuerkraft :: "bool list => una"

    31   FunktionsVariable        :: "real => una"

    32   Funktionen               :: "bool list => una"

    33   Gleichungen              :: "bool list => una"

    35   (*Script-names*)

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

    37 				bool] => bool"

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

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

    40 				bool] => bool"

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

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

    43 				bool] => bool"

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

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

    46 				bool] => bool"

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

    48   Biege1xIntegrierenScript ::

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

    50 		      bool] => bool"

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

    52   Belastung2BiegelScript   :: "[real,real,

    53 	                        bool list] => bool list"

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

    55   SetzeRandbedScript       :: "[bool list,bool list,

    56 	                        bool list] => bool list"

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

    59 axioms

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

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

    64   Moment_Querkraft:      "M_b' x = Q x"

    65   Querkraft_Moment:      "Q x = M_b' x"

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

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

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

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

    73 ML {*

    74 val thy = @{theory};

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

    78 store_isa ["IsacKnowledge"] [];

    79 store_thy thy

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

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

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

    83 store_thm thy ("Belastung_Querkraft", prop_of @{thm Belastung_Querkraft})

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

    85 store_thm thy ("Moment_Neigung", prop_of @{thm Moment_Neigung})

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

    87 store_thm thy ("Moment_Querkraft", prop_of @{thm Moment_Querkraft})

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

    89 store_thm thy ("Neigung_Moment", prop_of @{thm Neigung_Moment})

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

    91 store_thm thy ("Querkraft_Belastung", prop_of @{thm Querkraft_Belastung})

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

    93 store_thm thy ("Querkraft_Moment", prop_of @{thm Querkraft_Moment})

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

    95 store_thm thy ("make_fun_explicit", prop_of @{thm make_fun_explicit})

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

    98 *}

    99 ML {*

   100 (** problems **)

   102 store_pbt

   103  (prep_pbt thy "pbl_bieg" [] e_pblID

   104  (["Biegelinien"],

   105   [("#Given" ,["Traegerlaenge l_l", "Streckenlast q_q"]),

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

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

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

   109   ],

   110   append_rls "e_rls" e_rls [],

   111   NONE,

   112   [["IntegrierenUndKonstanteBestimmen2"]]));

   114 store_pbt

   115  (prep_pbt thy "pbl_bieg_mom" [] e_pblID

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

   117   [("#Given" ,["Traegerlaenge l_l", "Streckenlast q_q"]),

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

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

   120    ("#Relate",["RandbedingungenBiegung r_b","RandbedingungenMoment r_m"])

   121   ],

   122   append_rls "e_rls" e_rls [],

   123   NONE,

   124   [["IntegrierenUndKonstanteBestimmen"]]));

   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"]]));

   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"]]));

   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"]]));

   150 store_pbt

   151  (prep_pbt thy "pbl_bieg_vonq" [] e_pblID

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

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

   154    ("#Find"  ,["Funktionen funs'''"])],

   155   append_rls "e_rls" e_rls [],

   156   NONE,

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

   159 store_pbt

   160  (prep_pbt thy "pbl_bieg_randbed" [] e_pblID

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

   162   [("#Given" ,["Funktionen fun_s","Randbedingungen r_b"]),

   163    ("#Find"  ,["Gleichungen equs'''"])],

   164   append_rls "e_rls" e_rls [],

   165   NONE,

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

   168 store_pbt

   169  (prep_pbt thy "pbl_equ_fromfun" [] e_pblID

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

   171   [("#Given" ,["functionEq fu_n","substitution su_b"]),

   172    ("#Find"  ,["equality equ'''"])],

   173   append_rls "e_rls" e_rls [],

   174   NONE,

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

   177 *}

   178 ML {*

   179 (** methods **)

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

   182 		preconds = [],

   183 		rew_ord = ("termlessI",termlessI),

   184 		erls = append_rls "erls_in_srls_IntegrierenUnd.." e_rls

   185 				  [(*for asm in NTH_CONS ...*)

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

   187 				   (*2nd NTH_CONS pushes n+-1 into asms*)

   188 				   Calc("Groups.plus_class.plus", eval_binop "#add_")

   189 				   ],

   190 		srls = Erls, calc = [],

   191 		rules = [Thm ("NTH_CONS",num_str @{thm NTH_CONS}),

   192 			 Calc("Groups.plus_class.plus", eval_binop "#add_"),

   193 			 Thm ("NTH_NIL",num_str @{thm NTH_NIL}),

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

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

   196 			 Calc("Atools.argument'_in",

   197 			      eval_argument_in "Atools.argument'_in")

   198 			 ],

   199 		scr = EmptyScr};

   201 val srls2 =

   202     Rls {id="srls_IntegrierenUnd..",

   203 	 preconds = [],

   204 	 rew_ord = ("termlessI",termlessI),

   205 	 erls = append_rls "erls_in_srls_IntegrierenUnd.." e_rls

   206 			   [(*for asm in NTH_CONS ...*)

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

   208 			    (*2nd NTH_CONS pushes n+-1 into asms*)

   209 			    Calc("Groups.plus_class.plus", eval_binop "#add_")

   210 			    ],

   211 	 srls = Erls, calc = [],

   212 	 rules = [Thm ("NTH_CONS",num_str @{thm NTH_CONS}),

   213 		  Calc("Groups.plus_class.plus", eval_binop "#add_"),

   214 		  Thm ("NTH_NIL", num_str @{thm NTH_NIL}),

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

   216 		  Calc("Atools.filter'_sameFunId",

   217 		       eval_filter_sameFunId "Atools.filter'_sameFunId"),

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

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

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

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

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

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

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

   225 		  ],

   226 	 scr = EmptyScr};

   227 *}

   229 ML {*

   230 store_met

   231     (prep_met thy "met_biege" [] e_metID

   232 	      (["IntegrierenUndKonstanteBestimmen"],

   233 	       [("#Given" ,["Traegerlaenge l_l", "Streckenlast q_q",

   234 			    "FunktionsVariable v_v"]),

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

   236 		("#Find"  ,["Biegelinie b_b"]),

   237 		("#Relate",["RandbedingungenBiegung r_b",

   238 			    "RandbedingungenMoment r_m"])

   239 		],

   240 	       {rew_ord'="tless_true",

   241 		rls' = append_rls "erls_IntegrierenUndK.." e_rls

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

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

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

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

   246 		crls = Atools_erls, nrls = Erls},

   247 "Script BiegelinieScript                                                  " ^

   248 "(l_l::real) (q__q::real) (v_v::real) (b_b::real=>real)                   " ^

   249 "(r_b::bool list) (r_m::bool list) =                                      " ^

   250 "  (let q___q = Take (q_q v_v = q__q);                                       " ^

   251 "       q___q = ((Rewrite sym_real_minus_eq_cancel True) @@                " ^

   252 "              (Rewrite Belastung_Querkraft True)) q___q;                  " ^

   253 "      (Q__Q:: bool) =                                                     " ^

   254 "             (SubProblem (Biegelinie',[named,integrate,function],        " ^

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

   256 "                          [REAL (rhs q___q), REAL v_v, REAL_REAL Q]);   " ^

   257 "       Q__Q = Rewrite Querkraft_Moment True Q__Q;                          " ^

   258 "      (M__M::bool) =                                                      " ^

   259 "             (SubProblem (Biegelinie',[named,integrate,function],        " ^

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

   261 "                          [REAL (rhs Q__Q), REAL v_v, REAL_REAL M_b]);  " ^

   262 "       e__1 = NTH 1 r_m;                                                " ^

   263 "      (x__1::real) = argument_in (lhs e__1);                             " ^

   264 "      (M__1::bool) = (Substitute [v_v = x__1]) M__M;                       " ^

   265 "       M__1        = (Substitute [e__1]) M__1 ;                          " ^

   266 "       M__2 = Take M__M;                                                  " ^

   267 (*without this Take 'Substitute [v_v = x__2]' takes _last formula from ctree_*)

   268 "       e__2 = NTH 2 r_m;                                                " ^

   269 "      (x__2::real) = argument_in (lhs e__2);                             " ^

   270 "      (M__2::bool) = ((Substitute [v_v = x__2]) @@                        " ^

   271 "                      (Substitute [e__2])) M__2;                         " ^

   272 "      (c_1_2::bool list) =                                             " ^

   273 "             (SubProblem (Biegelinie',[linear,system],[no_met])          " ^

   274 "                          [BOOL_LIST [M__1, M__2], REAL_LIST [c,c_2]]);         " ^

   275 "       M__M = Take  M__M;                                                  " ^

   276 "       M__M = ((Substitute c_1_2) @@                                    " ^

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

   278 "                                   simplify_System False)) @@ " ^

   279 "              (Rewrite Moment_Neigung False) @@ " ^

   280 "              (Rewrite make_fun_explicit False)) M__M;                    " ^

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

   282 "      (N__N:: bool) =                                                     " ^

   283 "             (SubProblem (Biegelinie',[named,integrate,function],        " ^

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

   285 "                          [REAL (rhs M__M), REAL v_v, REAL_REAL y']);   " ^

   286 "      (B__B:: bool) =                                                     " ^

   287 "             (SubProblem (Biegelinie',[named,integrate,function],        " ^

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

   289 "                          [REAL (rhs N__N), REAL v_v, REAL_REAL y]);    " ^

   290 "       e__1 = NTH 1 r_b;                                                " ^

   291 "      (x__1::real) = argument_in (lhs e__1);                             " ^

   292 "      (B__1::bool) = (Substitute [v_v = x__1]) B__B;                       " ^

   293 "       B__1        = (Substitute [e__1]) B__1 ;                          " ^

   294 "       B__2 = Take B__B;                                                  " ^

   295 "       e__2 = NTH 2 r_b;                                                " ^

   296 "      (x__2::real) = argument_in (lhs e__2);                             " ^

   297 "      (B__2::bool) = ((Substitute [v_v = x__2]) @@                        " ^

   298 "                      (Substitute [e__2])) B__2;                         " ^

   299 "      (c_1_2::bool list) =                                             " ^

   300 "             (SubProblem (Biegelinie',[linear,system],[no_met])          " ^

   301 "                          [BOOL_LIST [B__1, B__2], REAL_LIST [c,c_2]]);         " ^

   302 "       B__B = Take  B__B;                                                  " ^

   303 "       B__B = ((Substitute c_1_2) @@                                    " ^

   304 "              (Rewrite_Set_Inst [(bdv, x)] make_ratpoly_in False)) B__B   " ^

   305 " in B__B)"

   306 ));

   307 *}

   308 ML {*

   310 store_met

   311     (prep_met thy "met_biege_2" [] e_metID

   312 	      (["IntegrierenUndKonstanteBestimmen2"],

   313 	       [("#Given" ,["Traegerlaenge l_l", "Streckenlast q__q",

   314 			    "FunktionsVariable v_v"]),

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

   316 		("#Find"  ,["Biegelinie b_b"]),

   317 		("#Relate",["Randbedingungen r_b"])

   318 		],

   319 	       {rew_ord'="tless_true",

   320 		rls' = append_rls "erls_IntegrierenUndK.." e_rls

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

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

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

   324 		calc = [],

   325 		srls = append_rls "erls_IntegrierenUndK.." e_rls

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

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

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

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

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

   331 				   ],

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

   333 "Script Biegelinie2Script                                                 " ^

   334 "(l_l::real) (q__q::real) (v_v::real) (b_b::real=>real) (r_b::bool list) = " ^

   335 "  (let                                                                   " ^

   336 "      (fun_s:: bool list) =                                              " ^

   337 "             (SubProblem (Biegelinie',[vonBelastungZu,Biegelinien],      " ^

   338 "                          [Biegelinien,ausBelastung])                    " ^

   339 "                          [REAL q__q, REAL v_v]);                        " ^

   340 "      (equ_s::bool list) =                                               " ^

   341 "             (SubProblem (Biegelinie',[setzeRandbedingungen,Biegelinien]," ^

   342 "                          [Biegelinien,setzeRandbedingungenEin])         " ^

   343 "                          [BOOL_LIST fun_s, BOOL_LIST r_b]);              " ^

   344 "      (con_s::bool list) =                                               " ^

   345 "             (SubProblem (Biegelinie',[linear,system],[no_met])          " ^

   346 "                          [BOOL_LIST equ_s, REAL_LIST [c,c_2,c_3,c_4]]);   " ^

   347 "       B_B = Take (lastI fun_s);                                          " ^

   348 "       B_B = ((Substitute con_s) @@                                       " ^

   349 "              (Rewrite_Set_Inst [(bdv, v_v)] make_ratpoly_in False)) B_B   " ^

   350 " in B_B)"

   351 ));

   353 *}

   354 ML {*

   355 store_met

   356     (prep_met thy "met_biege_intconst_2" [] e_metID

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

   358 	       [],

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

   360 		srls = e_rls,

   361 		prls=e_rls,

   362 	     crls = Atools_erls, nrls = e_rls},

   363 "empty_script"

   364 ));

   366 store_met

   367     (prep_met thy "met_biege_intconst_4" [] e_metID

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

   369 	       [],

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

   371 		srls = e_rls,

   372 		prls=e_rls,

   373 	     crls = Atools_erls, nrls = e_rls},

   374 "empty_script"

   375 ));

   377 store_met

   378     (prep_met thy "met_biege_intconst_1" [] e_metID

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

   380 	       [],

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

   382 		srls = e_rls,

   383 		prls=e_rls,

   384 	     crls = Atools_erls, nrls = e_rls},

   385 "empty_script"

   386 ));

   388 store_met

   389     (prep_met thy "met_biege2" [] e_metID

   390 	      (["Biegelinien"],

   391 	       [],

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

   393 		srls = e_rls,

   394 		prls=e_rls,

   395 	     crls = Atools_erls, nrls = e_rls},

   396 "empty_script"

   397 ));

   399 *}

   400 ML {*

   401 store_met

   402     (prep_met thy "met_biege_ausbelast" [] e_metID

   403 	      (["Biegelinien","ausBelastung"],

   404 	       [("#Given" ,["Streckenlast q__q","FunktionsVariable v_v"]),

   405 		("#Find"  ,["Funktionen fun_s"])],

   406 	       {rew_ord'="tless_true",

   407 		rls' = append_rls "erls_ausBelastung" e_rls

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

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

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

   411 		calc = [],

   412 		srls = append_rls "srls_ausBelastung" e_rls

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

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

   415 "Script Belastung2BiegelScript (q__q::real) (v_v::real) =                   " ^

   416 "  (let q___q = Take (q_q v_v = q__q);                                        " ^

   417 "       q___q = ((Rewrite sym_real_minus_eq_cancel True) @@                " ^

   418 "              (Rewrite Belastung_Querkraft True)) q___q;                  " ^

   419 "      (Q__Q:: bool) =                                                     " ^

   420 "             (SubProblem (Biegelinie',[named,integrate,function],        " ^

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

   422 "                          [REAL (rhs q___q), REAL v_v, REAL_REAL Q]);   " ^

   423 "       M__M = Rewrite Querkraft_Moment True Q__Q;                          " ^

   424 "      (M__M::bool) =                                                      " ^

   425 "             (SubProblem (Biegelinie',[named,integrate,function],        " ^

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

   427 "                          [REAL (rhs M__M), REAL v_v, REAL_REAL M_b]);  " ^

   428 "       N__N = ((Rewrite Moment_Neigung False) @@                          " ^

   429 "              (Rewrite make_fun_explicit False)) M__M;                    " ^

   430 "      (N__N:: bool) =                                                     " ^

   431 "             (SubProblem (Biegelinie',[named,integrate,function],        " ^

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

   433 "                          [REAL (rhs N__N), REAL v_v, REAL_REAL y']);   " ^

   434 "      (B__B:: bool) =                                                     " ^

   435 "             (SubProblem (Biegelinie',[named,integrate,function],        " ^

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

   437 "                          [REAL (rhs N__N), REAL v_v, REAL_REAL y])     " ^

   438 " in [Q__Q, M__M, N__N, B__B])"

   439 ));

   441 *}

   442 ML {*

   443 store_met

   444     (prep_met thy "met_biege_setzrand" [] e_metID

   445 	      (["Biegelinien","setzeRandbedingungenEin"],

   446 	       [("#Given" ,["Funktionen fun_s","Randbedingungen r_b"]),

   447 		("#Find"  ,["Gleichungen equs'''"])],

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

   449 		srls = srls2,

   450 		prls=e_rls,

   451 	     crls = Atools_erls, nrls = e_rls},

   452 "Script SetzeRandbedScript (fun_s::bool list) (r_b::bool list) = " ^

   453 " (let b_1 = NTH 1 r_b;                                         " ^

   454 "      f_s = filter_sameFunId (lhs b_1) fun_s;                   " ^

   455 "      (e_1::bool) =                                             " ^

   456 "             (SubProblem (Biegelinie',[makeFunctionTo,equation]," ^

   457 "                          [Equation,fromFunction])              " ^

   458 "                          [BOOL (hd f_s), BOOL b_1]);         " ^

   459 "      b_2 = NTH 2 r_b;                                         " ^

   460 "      f_s = filter_sameFunId (lhs b_2) fun_s;                   " ^

   461 "      (e_2::bool) =                                             " ^

   462 "             (SubProblem (Biegelinie',[makeFunctionTo,equation]," ^

   463 "                          [Equation,fromFunction])              " ^

   464 "                          [BOOL (hd f_s), BOOL b_2]);         " ^

   465 "      b_3 = NTH 3 r_b;                                         " ^

   466 "      f_s = filter_sameFunId (lhs b_3) fun_s;                   " ^

   467 "      (e_3::bool) =                                             " ^

   468 "             (SubProblem (Biegelinie',[makeFunctionTo,equation]," ^

   469 "                          [Equation,fromFunction])              " ^

   470 "                          [BOOL (hd f_s), BOOL b_3]);         " ^

   471 "      b_4 = NTH 4 r_b;                                         " ^

   472 "      f_s = filter_sameFunId (lhs b_4) fun_s;                   " ^

   473 "      (e_4::bool) =                                             " ^

   474 "             (SubProblem (Biegelinie',[makeFunctionTo,equation]," ^

   475 "                          [Equation,fromFunction])              " ^

   476 "                          [BOOL (hd f_s), BOOL b_4])          " ^

   477 " in [e_1,e_2,e_3,e_4])"

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

   479 "Script SetzeRandbedScript (fun_s::bool list) (r_b::bool list) = " ^

   480 " (let b_1 = NTH 1 r_b;                                         " ^

   481 "      f_s = filter (sameFunId (lhs b_1)) fun_s;                 " ^

   482 "      (e_1::bool) =                                             " ^

   483 "             (SubProblem (Biegelinie',[makeFunctionTo,equation]," ^

   484 "                          [Equation,fromFunction])              " ^

   485 "                          [BOOL (hd f_s), BOOL b_1]);         " ^

   486 "      b_2 = NTH 2 r_b;                                         " ^

   487 "      f_s = filter (sameFunId (lhs b_2)) fun_s;                 " ^

   488 "      (e_2::bool) =                                             " ^

   489 "             (SubProblem (Biegelinie',[makeFunctionTo,equation]," ^

   490 "                          [Equation,fromFunction])              " ^

   491 "                          [BOOL (hd f_s), BOOL b_2]);         " ^

   492 "      b_3 = NTH 3 r_b;                                         " ^

   493 "      f_s = filter (sameFunId (lhs b_3)) fun_s;                 " ^

   494 "      (e_3::bool) =                                             " ^

   495 "             (SubProblem (Biegelinie',[makeFunctionTo,equation]," ^

   496 "                          [Equation,fromFunction])              " ^

   497 "                          [BOOL (hd f_s), BOOL b_3]);         " ^

   498 "      b_4 = NTH 4 r_b;                                         " ^

   499 "      f_s = filter (sameFunId (lhs b_4)) fun_s;                 " ^

   500 "      (e_4::bool) =                                             " ^

   501 "             (SubProblem (Biegelinie',[makeFunctionTo,equation]," ^

   502 "                          [Equation,fromFunction])              " ^

   503 "                          [BOOL (hd f_s), BOOL b_4])          " ^

   504 " in [e_1,e_2,e_3,e_4])"*)

   505 ));

   507 *}

   508 ML {*

   509 store_met

   510     (prep_met thy "met_equ_fromfun" [] e_metID

   511 	      (["Equation","fromFunction"],

   512 	       [("#Given" ,["functionEq fu_n","substitution su_b"]),

   513 		("#Find"  ,["equality equ'''"])],

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

   515 		srls = append_rls "srls_in_EquationfromFunc" e_rls

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

   517 				   Calc("Atools.argument'_in",

   518 					eval_argument_in

   519 					    "Atools.argument'_in")],

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

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

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

   523 "Script Function2Equality (fu_n::bool) (su_b::bool) =" ^

   524 " (let fu_n = Take fu_n;                             " ^

   525 "      bd_v = argument_in (lhs fu_n);                " ^

   526 "      va_l = argument_in (lhs su_b);                " ^

   527 "      eq_u = (Substitute [bd_v = va_l]) fu_n;       " ^

   528 "      eq_u = (Substitute [su_b]) fu_n               " ^

   529 " in (Rewrite_Set norm_Rational False) eq_u)             "

   530 ));

   531 *}

   533 end

author	Walther Neuper <neuper@ist.tugraz.at>
	Thu, 23 Sep 2010 14:49:23 +0200
branch	isac-update-Isa09-2
changeset 38014	3e11e3c2dc42
parent 38002	10a171ce75d5
child 38045	ac0f6fd8d129
permissions	-rw-r--r--