wneuper/isa: src/Tools/isac/Knowledge/Biegelinie.ML@22235e4dbe5f

     1 (* chapter 'Biegelinie' from the textbook:

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

     3    authors: Walther Neuper 2005

     4    (c) due to copyright terms

     6 use"Knowledge/Biegelinie.ML";

     7 use"Biegelinie.ML";

     9 remove_thy"Typefix";

    10 remove_thy"Biegelinie";

    11 use_thy"Knowledge/Isac";

    12 *)

    14 (** interface isabelle -- isac **)

    16 theory' := overwritel (!theory', [("Biegelinie.thy",Biegelinie.thy)]);

    18 (** theory elements **)

    20 store_isa ["IsacKnowledge"] [];

    21 store_thy Biegelinie.thy

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

    23 store_isa ["IsacKnowledge", theory2thyID Biegelinie.thy, "Theorems"]

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

    25 store_thm Biegelinie.thy ("Belastung_Querkraft", Belastung_Querkraft)

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

    27 store_thm Biegelinie.thy ("Moment_Neigung", Moment_Neigung)

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

    29 store_thm Biegelinie.thy ("Moment_Querkraft", Moment_Querkraft)

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

    31 store_thm Biegelinie.thy ("Neigung_Moment", Neigung_Moment)

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

    33 store_thm Biegelinie.thy ("Querkraft_Belastung", Querkraft_Belastung)

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

    35 store_thm Biegelinie.thy ("Querkraft_Moment", Querkraft_Moment)

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

    37 store_thm Biegelinie.thy ("make_fun_explicit", make_fun_explicit)

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

    41 (** problems **)

    43 store_pbt

    44  (prep_pbt Biegelinie.thy "pbl_bieg" [] e_pblID

    45  (["Biegelinien"],

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

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

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

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

    50   ],

    51   append_rls "e_rls" e_rls [],

    52   NONE,

    53   [["IntegrierenUndKonstanteBestimmen2"]]));

    55 store_pbt

    56  (prep_pbt Biegelinie.thy "pbl_bieg_mom" [] e_pblID

    57  (["MomentBestimmte","Biegelinien"],

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

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

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

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

    62   ],

    63   append_rls "e_rls" e_rls [],

    64   NONE,

    65   [["IntegrierenUndKonstanteBestimmen"]]));

    67 store_pbt

    68  (prep_pbt Biegelinie.thy "pbl_bieg_momg" [] e_pblID

    69  (["MomentGegebene","Biegelinien"],

    70   [],

    71   append_rls "e_rls" e_rls [],

    72   NONE,

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

    75 store_pbt

    76  (prep_pbt Biegelinie.thy "pbl_bieg_einf" [] e_pblID

    77  (["einfache","Biegelinien"],

    78   [],

    79   append_rls "e_rls" e_rls [],

    80   NONE,

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

    83 store_pbt

    84  (prep_pbt Biegelinie.thy "pbl_bieg_momquer" [] e_pblID

    85  (["QuerkraftUndMomentBestimmte","Biegelinien"],

    86   [],

    87   append_rls "e_rls" e_rls [],

    88   NONE,

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

    91 store_pbt

    92  (prep_pbt Biegelinie.thy "pbl_bieg_vonq" [] e_pblID

    93  (["vonBelastungZu","Biegelinien"],

    94   [("#Given" ,["Streckenlast q__","FunktionsVariable v_"]),

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

    96   append_rls "e_rls" e_rls [],

    97   NONE,

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

   100 store_pbt

   101  (prep_pbt Biegelinie.thy "pbl_bieg_randbed" [] e_pblID

   102  (["setzeRandbedingungen","Biegelinien"],

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

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

   105   append_rls "e_rls" e_rls [],

   106   NONE,

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

   109 store_pbt

   110  (prep_pbt Biegelinie.thy "pbl_equ_fromfun" [] e_pblID

   111  (["makeFunctionTo","equation"],

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

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

   114   append_rls "e_rls" e_rls [],

   115   NONE,

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

   120 (** methods **)

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

   123 		preconds = [],

   124 		rew_ord = ("termlessI",termlessI),

   125 		erls = append_rls "erls_in_srls_IntegrierenUnd.." e_rls

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

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

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

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

   130 				   ],

   131 		srls = Erls, calc = [],

   132 		rules = [Thm ("nth_Cons_",num_str nth_Cons_),

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

   134 			 Thm ("nth_Nil_",num_str nth_Nil_),

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

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

   137 			 Calc("Atools.argument'_in",

   138 			      eval_argument_in "Atools.argument'_in")

   139 			 ],

   140 		scr = EmptyScr};

   142 val srls2 =

   143     Rls {id="srls_IntegrierenUnd..",

   144 	 preconds = [],

   145 	 rew_ord = ("termlessI",termlessI),

   146 	 erls = append_rls "erls_in_srls_IntegrierenUnd.." e_rls

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

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

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

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

   151 			    ],

   152 	 srls = Erls, calc = [],

   153 	 rules = [Thm ("nth_Cons_",num_str nth_Cons_),

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

   155 		  Thm ("nth_Nil_", num_str nth_Nil_),

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

   157 		  Calc("Atools.filter'_sameFunId",

   158 		       eval_filter_sameFunId "Atools.filter'_sameFunId"),

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

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

   161 		  Thm ("filter_Cons", num_str filter_Cons),

   162 		  Thm ("filter_Nil", num_str filter_Nil),

   163 		  Thm ("if_True", num_str if_True),

   164 		  Thm ("if_False", num_str if_False),

   165 		  Thm ("hd_thm", num_str hd_thm)

   166 		  ],

   167 	 scr = EmptyScr};

   168 (*@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@*)

   169 (* use"Knowledge/Biegelinie.ML";

   170    *)

   172 store_met

   173     (prep_met Biegelinie.thy "met_biege" [] e_metID

   174 	      (["IntegrierenUndKonstanteBestimmen"],

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

   176 			    "FunktionsVariable v_"]),

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

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

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

   180 			    "RandbedingungenMoment rm_"])

   181 		],

   182 	       {rew_ord'="tless_true",

   183 		rls' = append_rls "erls_IntegrierenUndK.." e_rls

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

   185 				   Thm ("not_true",num_str not_true),

   186 				   Thm ("not_false",num_str not_false)],

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

   188 		crls = Atools_erls, nrls = Erls},

   189 "Script BiegelinieScript                                                  \

   190 \(l_::real) (q__::real) (v_::real) (b_::real=>real)                        \

   191 \(rb_::bool list) (rm_::bool list) =                                      \

   192 \  (let q___ = Take (q_ v_ = q__);                                           \

   193 \       q___ = ((Rewrite sym_real_minus_eq_cancel True) @@                 \

   194 \              (Rewrite Belastung_Querkraft True)) q___;                   \

   195 \      (Q__:: bool) =                                                     \

   196 \             (SubProblem (Biegelinie_,[named,integrate,function],        \

   197 \                          [diff,integration,named])                      \

   198 \                          [real_ (rhs q___), real_ v_, real_real_ Q]);    \

   199 \       Q__ = Rewrite Querkraft_Moment True Q__;                          \

   200 \      (M__::bool) =                                                      \

   201 \             (SubProblem (Biegelinie_,[named,integrate,function],        \

   202 \                          [diff,integration,named])                      \

   203 \                          [real_ (rhs Q__), real_ v_, real_real_ M_b]);  \

   204 \       e1__ = nth_ 1 rm_;                                                \

   205 \      (x1__::real) = argument_in (lhs e1__);                             \

   206 \      (M1__::bool) = (Substitute [v_ = x1__]) M__;                       \

   207 \       M1__        = (Substitute [e1__]) M1__ ;                          \

   208 \       M2__ = Take M__;                                                  "^

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

   210 "       e2__ = nth_ 2 rm_;                                                \

   211 \      (x2__::real) = argument_in (lhs e2__);                             \

   212 \      (M2__::bool) = ((Substitute [v_ = x2__]) @@                        \

   213 \                      (Substitute [e2__])) M2__;                         \

   214 \      (c_1_2__::bool list) =                                             \

   215 \             (SubProblem (Biegelinie_,[linear,system],[no_met])          \

   216 \                          [booll_ [M1__, M2__], reall [c,c_2]]);         \

   217 \       M__ = Take  M__;                                                  \

   218 \       M__ = ((Substitute c_1_2__) @@                                    \

   219 \              (Try (Rewrite_Set_Inst [(bdv_1, c),(bdv_2, c_2)]\

   220 \                                   simplify_System False)) @@ \

   221 \              (Rewrite Moment_Neigung False) @@ \

   222 \              (Rewrite make_fun_explicit False)) M__;                    "^

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

   224 "      (N__:: bool) =                                                     \

   225 \             (SubProblem (Biegelinie_,[named,integrate,function],        \

   226 \                          [diff,integration,named])                      \

   227 \                          [real_ (rhs M__), real_ v_, real_real_ y']);   \

   228 \      (B__:: bool) =                                                     \

   229 \             (SubProblem (Biegelinie_,[named,integrate,function],        \

   230 \                          [diff,integration,named])                      \

   231 \                          [real_ (rhs N__), real_ v_, real_real_ y]);    \

   232 \       e1__ = nth_ 1 rb_;                                                \

   233 \      (x1__::real) = argument_in (lhs e1__);                             \

   234 \      (B1__::bool) = (Substitute [v_ = x1__]) B__;                       \

   235 \       B1__        = (Substitute [e1__]) B1__ ;                          \

   236 \       B2__ = Take B__;                                                  \

   237 \       e2__ = nth_ 2 rb_;                                                \

   238 \      (x2__::real) = argument_in (lhs e2__);                             \

   239 \      (B2__::bool) = ((Substitute [v_ = x2__]) @@                        \

   240 \                      (Substitute [e2__])) B2__;                         \

   241 \      (c_1_2__::bool list) =                                             \

   242 \             (SubProblem (Biegelinie_,[linear,system],[no_met])          \

   243 \                          [booll_ [B1__, B2__], reall [c,c_2]]);         \

   244 \       B__ = Take  B__;                                                  \

   245 \       B__ = ((Substitute c_1_2__) @@                                    \

   246 \              (Rewrite_Set_Inst [(bdv, x)] make_ratpoly_in False)) B__   \

   247 \ in B__)"

   248 ));

   250 store_met

   251     (prep_met Biegelinie.thy "met_biege_2" [] e_metID

   252 	      (["IntegrierenUndKonstanteBestimmen2"],

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

   254 			    "FunktionsVariable v_"]),

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

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

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

   258 		],

   259 	       {rew_ord'="tless_true",

   260 		rls' = append_rls "erls_IntegrierenUndK.." e_rls

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

   262 				   Thm ("not_true",num_str not_true),

   263 				   Thm ("not_false",num_str not_false)],

   264 		calc = [],

   265 		srls = append_rls "erls_IntegrierenUndK.." e_rls

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

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

   268 				   Thm ("last_thmI",num_str last_thmI),

   269 				   Thm ("if_True",num_str if_True),

   270 				   Thm ("if_False",num_str if_False)

   271 				   ],

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

   273 "Script Biegelinie2Script                                                 \

   274 \(l_::real) (q__::real) (v_::real) (b_::real=>real) (rb_::bool list) =    \

   275 \  (let                                                                   \

   276 \      (funs_:: bool list) =                                              \

   277 \             (SubProblem (Biegelinie_,[vonBelastungZu,Biegelinien],      \

   278 \                          [Biegelinien,ausBelastung])                    \

   279 \                          [real_ q__, real_ v_]);                        \

   280 \      (equs_::bool list) =                                               \

   281 \             (SubProblem (Biegelinie_,[setzeRandbedingungen,Biegelinien],\

   282 \                          [Biegelinien,setzeRandbedingungenEin])         \

   283 \                          [booll_ funs_, booll_ rb_]);                   \

   284 \      (cons_::bool list) =                                               \

   285 \             (SubProblem (Biegelinie_,[linear,system],[no_met])          \

   286 \                          [booll_ equs_, reall [c,c_2,c_3,c_4]]);        \

   287 \       B_ = Take (lastI funs_);                                          \

   288 \       B_ = ((Substitute cons_) @@                                       \

   289 \              (Rewrite_Set_Inst [(bdv, v_)] make_ratpoly_in False)) B_   \

   290 \ in B_)"

   291 ));

   293 store_met

   294     (prep_met Biegelinie.thy "met_biege_intconst_2" [] e_metID

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

   296 	       [],

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

   298 		srls = e_rls,

   299 		prls=e_rls,

   300 	     crls = Atools_erls, nrls = e_rls},

   301 "empty_script"

   302 ));

   304 store_met

   305     (prep_met Biegelinie.thy "met_biege_intconst_4" [] e_metID

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

   307 	       [],

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

   309 		srls = e_rls,

   310 		prls=e_rls,

   311 	     crls = Atools_erls, nrls = e_rls},

   312 "empty_script"

   313 ));

   315 store_met

   316     (prep_met Biegelinie.thy "met_biege_intconst_1" [] e_metID

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

   318 	       [],

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

   320 		srls = e_rls,

   321 		prls=e_rls,

   322 	     crls = Atools_erls, nrls = e_rls},

   323 "empty_script"

   324 ));

   326 store_met

   327     (prep_met Biegelinie.thy "met_biege2" [] e_metID

   328 	      (["Biegelinien"],

   329 	       [],

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

   331 		srls = e_rls,

   332 		prls=e_rls,

   333 	     crls = Atools_erls, nrls = e_rls},

   334 "empty_script"

   335 ));

   337 store_met

   338     (prep_met Biegelinie.thy "met_biege_ausbelast" [] e_metID

   339 	      (["Biegelinien","ausBelastung"],

   340 	       [("#Given" ,["Streckenlast q__","FunktionsVariable v_"]),

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

   342 	       {rew_ord'="tless_true",

   343 		rls' = append_rls "erls_ausBelastung" e_rls

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

   345 				   Thm ("not_true",num_str not_true),

   346 				   Thm ("not_false",num_str not_false)],

   347 		calc = [],

   348 		srls = append_rls "srls_ausBelastung" e_rls

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

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

   351 "Script Belastung2BiegelScript (q__::real) (v_::real) =                    \

   352 \  (let q___ = Take (q_ v_ = q__);                                           \

   353 \       q___ = ((Rewrite sym_real_minus_eq_cancel True) @@                 \

   354 \              (Rewrite Belastung_Querkraft True)) q___;                   \

   355 \      (Q__:: bool) =                                                     \

   356 \             (SubProblem (Biegelinie_,[named,integrate,function],        \

   357 \                          [diff,integration,named])                      \

   358 \                          [real_ (rhs q___), real_ v_, real_real_ Q]);    \

   359 \       M__ = Rewrite Querkraft_Moment True Q__;                          \

   360 \      (M__::bool) =                                                      \

   361 \             (SubProblem (Biegelinie_,[named,integrate,function],        \

   362 \                          [diff,integration,named])                      \

   363 \                          [real_ (rhs M__), real_ v_, real_real_ M_b]);  \

   364 \       N__ = ((Rewrite Moment_Neigung False) @@                          \

   365 \              (Rewrite make_fun_explicit False)) M__;                    \

   366 \      (N__:: bool) =                                                     \

   367 \             (SubProblem (Biegelinie_,[named,integrate,function],        \

   368 \                          [diff,integration,named])                      \

   369 \                          [real_ (rhs N__), real_ v_, real_real_ y']);   \

   370 \      (B__:: bool) =                                                     \

   371 \             (SubProblem (Biegelinie_,[named,integrate,function],        \

   372 \                          [diff,integration,named])                      \

   373 \                          [real_ (rhs N__), real_ v_, real_real_ y])    \

   374 \ in [Q__, M__, N__, B__])"

   375 ));

   377 store_met

   378     (prep_met Biegelinie.thy "met_biege_setzrand" [] e_metID

   379 	      (["Biegelinien","setzeRandbedingungenEin"],

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

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

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

   383 		srls = srls2,

   384 		prls=e_rls,

   385 	     crls = Atools_erls, nrls = e_rls},

   386 "Script SetzeRandbedScript (funs_::bool list) (rb_::bool list) = \

   387 \ (let b1_ = nth_ 1 rb_;                                         \

   388 \      fs_ = filter_sameFunId (lhs b1_) funs_;                   \

   389 \      (e1_::bool) =                                             \

   390 \             (SubProblem (Biegelinie_,[makeFunctionTo,equation],\

   391 \                          [Equation,fromFunction])              \

   392 \                          [bool_ (hd fs_), bool_ b1_]);         \

   393 \      b2_ = nth_ 2 rb_;                                         \

   394 \      fs_ = filter_sameFunId (lhs b2_) funs_;                   \

   395 \      (e2_::bool) =                                             \

   396 \             (SubProblem (Biegelinie_,[makeFunctionTo,equation],\

   397 \                          [Equation,fromFunction])              \

   398 \                          [bool_ (hd fs_), bool_ b2_]);         \

   399 \      b3_ = nth_ 3 rb_;                                         \

   400 \      fs_ = filter_sameFunId (lhs b3_) funs_;                   \

   401 \      (e3_::bool) =                                             \

   402 \             (SubProblem (Biegelinie_,[makeFunctionTo,equation],\

   403 \                          [Equation,fromFunction])              \

   404 \                          [bool_ (hd fs_), bool_ b3_]);         \

   405 \      b4_ = nth_ 4 rb_;                                         \

   406 \      fs_ = filter_sameFunId (lhs b4_) funs_;                   \

   407 \      (e4_::bool) =                                             \

   408 \             (SubProblem (Biegelinie_,[makeFunctionTo,equation],\

   409 \                          [Equation,fromFunction])              \

   410 \                          [bool_ (hd fs_), bool_ b4_])          \

   411 \ in [e1_,e2_,e3_,e4_])"

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

   413 "Script SetzeRandbedScript (funs_::bool list) (rb_::bool list) = \

   414 \ (let b1_ = nth_ 1 rb_;                                         \

   415 \      fs_ = filter (sameFunId (lhs b1_)) funs_;                 \

   416 \      (e1_::bool) =                                             \

   417 \             (SubProblem (Biegelinie_,[makeFunctionTo,equation],\

   418 \                          [Equation,fromFunction])              \

   419 \                          [bool_ (hd fs_), bool_ b1_]);         \

   420 \      b2_ = nth_ 2 rb_;                                         \

   421 \      fs_ = filter (sameFunId (lhs b2_)) funs_;                 \

   422 \      (e2_::bool) =                                             \

   423 \             (SubProblem (Biegelinie_,[makeFunctionTo,equation],\

   424 \                          [Equation,fromFunction])              \

   425 \                          [bool_ (hd fs_), bool_ b2_]);         \

   426 \      b3_ = nth_ 3 rb_;                                         \

   427 \      fs_ = filter (sameFunId (lhs b3_)) funs_;                 \

   428 \      (e3_::bool) =                                             \

   429 \             (SubProblem (Biegelinie_,[makeFunctionTo,equation],\

   430 \                          [Equation,fromFunction])              \

   431 \                          [bool_ (hd fs_), bool_ b3_]);         \

   432 \      b4_ = nth_ 4 rb_;                                         \

   433 \      fs_ = filter (sameFunId (lhs b4_)) funs_;                 \

   434 \      (e4_::bool) =                                             \

   435 \             (SubProblem (Biegelinie_,[makeFunctionTo,equation],\

   436 \                          [Equation,fromFunction])              \

   437 \                          [bool_ (hd fs_), bool_ b4_])          \

   438 \ in [e1_,e2_,e3_,e4_])"*)

   439 ));

   441 store_met

   442     (prep_met Biegelinie.thy "met_equ_fromfun" [] e_metID

   443 	      (["Equation","fromFunction"],

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

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

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

   447 		srls = append_rls "srls_in_EquationfromFunc" e_rls

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

   449 				   Calc("Atools.argument'_in",

   450 					eval_argument_in

   451 					    "Atools.argument'_in")],

   452 		prls=e_rls,

   453 	     crls = Atools_erls, nrls = e_rls},

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

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

   456 "Script Function2Equality (fun_::bool) (sub_::bool) =\

   457 \ (let fun_ = Take fun_;                             \

   458 \      bdv_ = argument_in (lhs fun_);                \

   459 \      val_ = argument_in (lhs sub_);                \

   460 \      equ_ = (Substitute [bdv_ = val_]) fun_;       \

   461 \      equ_ = (Substitute [sub_]) fun_               \

   462 \ in (Rewrite_Set norm_Rational False) equ_)             "

   463 ));

   467 (* use"Knowledge/Biegelinie.ML";

   468    *)

author	Walther Neuper <neuper@ist.tugraz.at>
	Wed, 25 Aug 2010 16:20:07 +0200
branch	isac-update-Isa09-2
changeset 37947	22235e4dbe5f
parent 37926	src/Tools/isac/IsacKnowledge/Biegelinie.ML@e6fc98fbcb85
child 37952	9ddd1000b900
permissions	-rw-r--r--