(* chapter 'Biegelinie' from the textbook: 

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

   author: Walther Neuper 050826,

   (c) due to copyright terms

*)

theory Biegelinie imports Integrate Equation EqSystem Atools begin

consts

  qq    :: "real => real"             (* Streckenlast               *)

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

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

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

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

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

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

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

  EI    :: "real"                     (* Biegesteifigkeit           *)

  (*new Descriptions in the related problems*)

  Traegerlaenge            :: "real => una"

  Streckenlast             :: "real => una"

  BiegemomentVerlauf       :: "bool => una"

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

  Randbedingungen          :: "bool list => una"

  RandbedingungenBiegung   :: "bool list => una"

  RandbedingungenNeigung   :: "bool list => una"

  RandbedingungenMoment    :: "bool list => una"

  RandbedingungenQuerkraft :: "bool list => una"

  FunktionsVariable        :: "real => una"

  Funktionen               :: "bool list => una"

  Gleichungen              :: "bool list => una"

  (*Script-names*)

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

				bool] => bool"	

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

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

				bool] => bool"	

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

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

				bool] => bool"		

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

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

				bool] => bool"	

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

  Biege1xIntegrierenScript :: 

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

		      bool] => bool"	

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

  Belastung2BiegelScript   :: "[real,real,

	                        bool list] => bool list"	

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

  SetzeRandbedScript       :: "[bool list,bool list,

	                        bool list] => bool list"	

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

axiomatization where

  Querkraft_Belastung:   "Q' x = -qq x" and

  Belastung_Querkraft:   "-qq x = Q' x" and

  Moment_Querkraft:      "M_b' x = Q x" and

  Querkraft_Moment:      "Q x = M_b' x" and

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

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

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

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

ML {*

val thy = @{theory};

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

store_isa ["IsacKnowledge"] [];

store_thy thy 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

*}

ML {*

(** problems **)

store_pbt

 (prep_pbt thy "pbl_bieg" [] e_pblID

 (["Biegelinien"],

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

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

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

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

  ],

  append_rls "e_rls" e_rls [], 

  NONE, 

  [["IntegrierenUndKonstanteBestimmen2"]]));

store_pbt 

 (prep_pbt thy "pbl_bieg_mom" [] e_pblID

 (["MomentBestimmte","Biegelinien"],

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

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

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

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

  ],

  append_rls "e_rls" e_rls [], 

  NONE, 

  [["IntegrierenUndKonstanteBestimmen"]]));

store_pbt

 (prep_pbt thy "pbl_bieg_momg" [] e_pblID

 (["MomentGegebene","Biegelinien"],

  [],

  append_rls "e_rls" e_rls [], 

  NONE, 

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

store_pbt

 (prep_pbt thy "pbl_bieg_einf" [] e_pblID

 (["einfache","Biegelinien"],

  [],

  append_rls "e_rls" e_rls [], 

  NONE, 

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

store_pbt

 (prep_pbt thy "pbl_bieg_momquer" [] e_pblID

 (["QuerkraftUndMomentBestimmte","Biegelinien"],

  [],

  append_rls "e_rls" e_rls [], 

  NONE, 

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

store_pbt

 (prep_pbt thy "pbl_bieg_vonq" [] e_pblID

 (["vonBelastungZu","Biegelinien"],

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

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

  append_rls "e_rls" e_rls [], 

  NONE, 

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

store_pbt

 (prep_pbt thy "pbl_bieg_randbed" [] e_pblID

 (["setzeRandbedingungen","Biegelinien"],

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

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

  append_rls "e_rls" e_rls [], 

  NONE, 

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

store_pbt

 (prep_pbt thy "pbl_equ_fromfun" [] e_pblID

 (["makeFunctionTo","equation"],

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

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

  append_rls "e_rls" e_rls [], 

  NONE, 

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

KEStore_Elems.get_ptyps @{theory};

*}

setup {* KEStore_Elems.store_pbts

  [(prep_pbt thy "pbl_bieg" [] e_pblID

      (["Biegelinien"],

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

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

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

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

        append_rls "e_rls" e_rls [], NONE, [["IntegrierenUndKonstanteBestimmen2"]])),

    (prep_pbt thy "pbl_bieg_mom" [] e_pblID

      (["MomentBestimmte","Biegelinien"],

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

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

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

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

        ],

        append_rls "e_rls" e_rls [], NONE, [["IntegrierenUndKonstanteBestimmen"]])),

    (prep_pbt thy "pbl_bieg_momg" [] e_pblID

      (["MomentGegebene","Biegelinien"], [], append_rls "e_rls" e_rls [], NONE,

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

    (prep_pbt thy "pbl_bieg_einf" [] e_pblID

      (["einfache","Biegelinien"], [], append_rls "e_rls" e_rls [], NONE,

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

    (prep_pbt thy "pbl_bieg_momquer" [] e_pblID

      (["QuerkraftUndMomentBestimmte","Biegelinien"], [], append_rls "e_rls" e_rls [], NONE,

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

    (prep_pbt thy "pbl_bieg_vonq" [] e_pblID

      (["vonBelastungZu","Biegelinien"],

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

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

        append_rls "e_rls" e_rls [], NONE, [["Biegelinien","ausBelastung"]])),

    (prep_pbt thy "pbl_bieg_randbed" [] e_pblID

      (["setzeRandbedingungen","Biegelinien"],

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

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

        append_rls "e_rls" e_rls [], NONE, [["Biegelinien","setzeRandbedingungenEin"]])),

    (prep_pbt thy "pbl_equ_fromfun" [] e_pblID

      (["makeFunctionTo","equation"],

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

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

        append_rls "e_rls" e_rls [], NONE, [["Equation","fromFunction"]]))] *}

ML {*

(** methods **)

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

		preconds = [], 

		rew_ord = ("termlessI",termlessI), 

		erls = append_rls "erls_in_srls_IntegrierenUnd.." e_rls

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

				   Calc ("Orderings.ord_class.less",eval_equ "#less_"),

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

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

				   ], 

		srls = Erls, calc = [], errpatts = [],

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

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

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

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

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

			 Calc("Atools.argument'_in",

			      eval_argument_in "Atools.argument'_in")

			 ],

		scr = EmptyScr};

val srls2 = 

    Rls {id="srls_IntegrierenUnd..", 

	 preconds = [], 

	 rew_ord = ("termlessI",termlessI), 

	 erls = append_rls "erls_in_srls_IntegrierenUnd.." e_rls

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

			    Calc ("Orderings.ord_class.less",eval_equ "#less_"),

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

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

			    ], 

	 srls = Erls, calc = [], errpatts = [],

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

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

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

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

		  Calc("Atools.filter'_sameFunId",

		       eval_filter_sameFunId "Atools.filter'_sameFunId"),

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

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

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

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

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

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

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

		  ],

	 scr = EmptyScr};

*}

ML {*

store_met

  (prep_met thy "met_biege" [] e_metID 

	    (["IntegrierenUndKonstanteBestimmen"],

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

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

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

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

	     {rew_ord'="tless_true", 

	      rls' = append_rls "erls_IntegrierenUndK.." e_rls 

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

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

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

				       calc = [], srls = srls, prls = Erls, crls = Atools_erls, errpats = [], nrls = Erls},

"Script BiegelinieScript                                                 " ^

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

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

"  (let q___q = Take (qq v_v = q__q);                                    " ^

"       q___q = ((Rewrite sym_neg_equal_iff_equal True) @@               " ^

"              (Rewrite Belastung_Querkraft True)) q___q;                " ^

"      (Q__Q:: bool) =                                                   " ^

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

"                          [diff,integration,named])                     " ^

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

"       Q__Q = Rewrite Querkraft_Moment True Q__Q;                       " ^

"      (M__M::bool) =                                                    " ^

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

"                          [diff,integration,named])                     " ^

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

                                        (*([5], Res), M_b x = c_2 + c * x + -1 * q_0 / 2 * x ^^^ 2*)

"       e__1 = NTH 1 r_m;                                                " ^

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

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

                                        (*([6], Res), M_b 0 = c_2 + c * 0 + -1 * q_0 / 2 * 0 ^^^ 2*)

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

                                        (*([7], Res), 0 = c_2 + c * 0 + -1 * q_0 / 2 * 0 ^^^ 2*)

"       M__2 = Take M__M;                                                " ^

                                        (*([8], Frm), M_b x = c_2 + c * x + -1 * q_0 / 2 * x ^^^ 2*)

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

"       e__2 = NTH 2 r_m;                                                " ^

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

"      (M__2::bool) = (Substitute [v_v = x__2]) M__M;                    " ^

                                        (*([8], Res), M_b L = c_2 + c * L + -1 * q_0 / 2 * L ^^^ 2*)

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

                                        (**)

"      (c_1_2::bool list) =                                              " ^

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

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

"       M__M = Take  M__M;                                               " ^

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

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

"                                   simplify_System False)) @@           " ^

"              (Rewrite Moment_Neigung False) @@                         " ^

"              (Rewrite make_fun_explicit False)) M__M;                  " ^

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

"      (N__N:: bool) =                                                   " ^

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

"                          [diff,integration,named])                     " ^

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

"      (B__B:: bool) =                                                   " ^

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

"                          [diff,integration,named])                     " ^

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

"       e__1 = NTH 1 r_b;                                                " ^

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

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

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

"       B__2 = Take B__B;                                                " ^

"       e__2 = NTH 2 r_b;                                                " ^

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

"      (B__2::bool) = (Substitute [v_v = x__2]) B__B;                    " ^

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

"      (c_1_2::bool list) =                                              " ^

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

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

"       B__B = Take  B__B;                                               " ^

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

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

" in B__B)"

));

*}

ML {*

store_met

  (prep_met thy "met_biege_2" [] e_metID

	    (["IntegrierenUndKonstanteBestimmen2"],

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

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

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

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

	    {rew_ord'="tless_true", 

	     rls' = append_rls "erls_IntegrierenUndK.." e_rls 

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

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

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

				     calc = [], 

				     srls = append_rls "erls_IntegrierenUndK.." e_rls 

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

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

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

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

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

				     prls = Erls, crls = Atools_erls, errpats = [], nrls = Erls},

"Script Biegelinie2Script                                                  " ^

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

"  (let                                                                    " ^

"      (fun_s:: bool list) =                                               " ^

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

"                          [Biegelinien,ausBelastung])                     " ^

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

"      (equ_s::bool list) =                                                " ^

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

"                          [Biegelinien,setzeRandbedingungenEin])          " ^

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

"      (con_s::bool list) =                                                " ^

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

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

"       B_B = Take (lastI fun_s);                                          " ^

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

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

" in B_B)"

));

*}

ML {*

store_met

    (prep_met thy "met_biege_intconst_2" [] e_metID

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

	       [],

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

		srls = e_rls, 

		prls=e_rls,

	     crls = Atools_erls, errpats = [], nrls = e_rls},

"empty_script"

));

store_met

    (prep_met thy "met_biege_intconst_4" [] e_metID

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

	       [],

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

		srls = e_rls, 

		prls=e_rls,

	     crls = Atools_erls, errpats = [], nrls = e_rls},

"empty_script"

));

store_met

    (prep_met thy "met_biege_intconst_1" [] e_metID

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

	       [],

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

		srls = e_rls, 

		prls=e_rls,

	     crls = Atools_erls, errpats = [], nrls = e_rls},

"empty_script"

));

store_met

    (prep_met thy "met_biege2" [] e_metID

	      (["Biegelinien"],

	       [],

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

		srls = e_rls, 

		prls=e_rls,

	     crls = Atools_erls, errpats = [], nrls = e_rls},

"empty_script"

));

*}

ML {*

store_met

  (prep_met thy "met_biege_ausbelast" [] e_metID

	    (["Biegelinien", "ausBelastung"],

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

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

	     {rew_ord'="tless_true", 

	      rls' = append_rls "erls_ausBelastung" e_rls 

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

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

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

				      calc = [], 

				      srls = append_rls "srls_ausBelastung" e_rls 

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

				      prls = e_rls, crls = Atools_erls, errpats = [], nrls = e_rls},

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

"  (let q___q = Take (qq v_v = q__q);                                  " ^

"       q___q = ((Rewrite sym_neg_equal_iff_equal True) @@              " ^

"              (Rewrite Belastung_Querkraft True)) q___q;               " ^

"      (Q__Q:: bool) =                                                  " ^

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

"                          [diff,integration,named])                    " ^

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

"       M__M = Rewrite Querkraft_Moment True Q__Q;                      " ^

"      (M__M::bool) =                                                   " ^

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

"                          [diff,integration,named])                    " ^

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

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

"              (Rewrite make_fun_explicit False)) M__M;                 " ^

"      (N__N:: bool) =                                                  " ^

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

"                          [diff,integration,named])                    " ^

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

"      (B__B:: bool) =                                                  " ^

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

"                          [diff,integration,named])                    " ^

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

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

));

*}

ML {*

store_met

    (prep_met thy "met_biege_setzrand" [] e_metID

	      (["Biegelinien", "setzeRandbedingungenEin"],

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

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

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

		srls = srls2, 

		prls=e_rls,

	     crls = Atools_erls, errpats = [], nrls = e_rls},

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

" (let b_1 = NTH 1 r_b;                                         " ^

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

"      (e_1::bool) =                                             " ^

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

"                          [Equation,fromFunction])              " ^

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

"      b_2 = NTH 2 r_b;                                         " ^

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

"      (e_2::bool) =                                             " ^

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

"                          [Equation,fromFunction])              " ^

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

"      b_3 = NTH 3 r_b;                                         " ^

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

"      (e_3::bool) =                                             " ^

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

"                          [Equation,fromFunction])              " ^

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

"      b_4 = NTH 4 r_b;                                         " ^

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

"      (e_4::bool) =                                             " ^

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

"                          [Equation,fromFunction])              " ^

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

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

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

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

" (let b_1 = NTH 1 r_b;                                         " ^

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

"      (e_1::bool) =                                             " ^

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

"                          [Equation,fromFunction])              " ^

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

"      b_2 = NTH 2 r_b;                                         " ^

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

"      (e_2::bool) =                                             " ^

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

"                          [Equation,fromFunction])              " ^

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

"      b_3 = NTH 3 r_b;                                         " ^

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

"      (e_3::bool) =                                             " ^

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

"                          [Equation,fromFunction])              " ^

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

"      b_4 = NTH 4 r_b;                                         " ^

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

"      (e_4::bool) =                                             " ^

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

"                          [Equation,fromFunction])              " ^

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

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

));

*}

ML {*

store_met

  (prep_met thy "met_equ_fromfun" [] e_metID

	    (["Equation","fromFunction"],

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

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

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

	      srls = append_rls "srls_in_EquationfromFunc" e_rls

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

				         Calc("Atools.argument'_in", eval_argument_in "Atools.argument'_in")], 

				       prls=e_rls, crls = Atools_erls, errpats = [], nrls = e_rls},

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

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

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

" (let fu_n = Take fu_n;                             " ^

"      bd_v = argument_in (lhs fu_n);                " ^

"      va_l = argument_in (lhs su_b);                " ^

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

                                        (*([1], Res), M_b L = c_2 + c * L + -1 * q_0 / 2 * L ^^^ 2*)

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

" in (Rewrite_Set norm_Rational False) eq_u)         "

));

*}

end