(* chapter 'Biegelinie' from the textbook: 

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

   authors: Walther Neuper 2005

   (c) due to copyright terms

use"IsacKnowledge/Biegelinie.ML";

use"Biegelinie.ML";

remove_thy"Typefix";

remove_thy"Biegelinie";

use_thy"IsacKnowledge/Isac";

*)

(** interface isabelle -- isac **)

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

(** theory elements **)

store_isa ["IsacKnowledge"] [];

store_thy Biegelinie.thy 

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

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

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

store_thm Biegelinie.thy ("Belastung_Querkraft", Belastung_Querkraft)

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

store_thm Biegelinie.thy ("Moment_Neigung", Moment_Neigung)

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

store_thm Biegelinie.thy ("Moment_Querkraft", Moment_Querkraft)

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

store_thm Biegelinie.thy ("Neigung_Moment", Neigung_Moment)

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

store_thm Biegelinie.thy ("Querkraft_Belastung", Querkraft_Belastung)

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

store_thm Biegelinie.thy ("Querkraft_Moment", Querkraft_Moment)

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

store_thm Biegelinie.thy ("make_fun_explicit", make_fun_explicit)

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

(** problems **)

store_pbt

 (prep_pbt Biegelinie.thy "pbl_bieg" [] e_pblID

 (["Biegelinien"],

  [("#Given" ,["Traegerlaenge l_", "Streckenlast q_"]),

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

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

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

  ],

  append_rls "e_rls" e_rls [], 

  None, 

  [["IntegrierenUndKonstanteBestimmen2"]]));

store_pbt 

 (prep_pbt Biegelinie.thy "pbl_bieg_mom" [] e_pblID

 (["MomentBestimmte","Biegelinien"],

  [("#Given" ,["Traegerlaenge l_", "Streckenlast q_"]),

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

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

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

  ],

  append_rls "e_rls" e_rls [], 

  None, 

  [["IntegrierenUndKonstanteBestimmen"]]));

store_pbt

 (prep_pbt Biegelinie.thy "pbl_bieg_momg" [] e_pblID

 (["MomentGegebene","Biegelinien"],

  [],

  append_rls "e_rls" e_rls [], 

  None, 

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

store_pbt

 (prep_pbt Biegelinie.thy "pbl_bieg_einf" [] e_pblID

 (["einfache","Biegelinien"],

  [],

  append_rls "e_rls" e_rls [], 

  None, 

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

store_pbt

 (prep_pbt Biegelinie.thy "pbl_bieg_momquer" [] e_pblID

 (["QuerkraftUndMomentBestimmte","Biegelinien"],

  [],

  append_rls "e_rls" e_rls [], 

  None, 

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

store_pbt

 (prep_pbt Biegelinie.thy "pbl_bieg_vonq" [] e_pblID

 (["vonBelastungZu","Biegelinien"],

  [("#Given" ,["Streckenlast q_","FunktionsVariable v_"]),

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

  append_rls "e_rls" e_rls [], 

  None, 

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

store_pbt

 (prep_pbt Biegelinie.thy "pbl_bieg_randbed" [] e_pblID

 (["setzeRandbedingungen","Biegelinien"],

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

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

  append_rls "e_rls" e_rls [], 

  None, 

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

store_pbt

 (prep_pbt Biegelinie.thy "pbl_equ_fromfun" [] e_pblID

 (["makeFunctionTo","equation"],

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

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

  append_rls "e_rls" e_rls [], 

  None, 

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

(** 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 ("op <",eval_equ "#less_"),

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

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

				   ], 

		srls = Erls, calc = [],

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

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

			 Thm ("nth_Nil_",num_str 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 ("op <",eval_equ "#less_"),

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

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

			    ], 

	 srls = Erls, calc = [],

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

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

		  Thm ("nth_Nil_", num_str nth_Nil_),

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

		  Calc("Atools.sameFunId",

		       eval_sameFunId "Atools.sameFunId"),

		  Thm ("filter_Cons", num_str filter_Cons),

		  Thm ("filter_Nil", num_str filter_Nil),

		  Thm ("if_True", num_str if_True),

		  Thm ("if_False", num_str if_False),

		  Thm ("hd_thm", num_str hd_thm)

		  ],

	 scr = EmptyScr};

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

(* use"IsacKnowledge/Biegelinie.ML";

   *)

store_met

    (prep_met Biegelinie.thy "met_biege" [] e_metID

	      (["IntegrierenUndKonstanteBestimmen"],

	       [("#Given" ,["Traegerlaenge l_", "Streckenlast q_",

			    "FunktionsVariable v_"]),

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

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

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

			    "RandbedingungenMoment rm_"])

		],

	       {rew_ord'="tless_true", 

		rls' = append_rls "erls_IntegrierenUndK.." e_rls 

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

				   Thm ("not_true",num_str not_true),

				   Thm ("not_false",num_str not_false)], 

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

		crls = Atools_erls, nrls = Erls},

"Script BiegelinieScript                                                  \

\(l_::real) (q_::real) (v_::real) (b_::real=>real)                        \

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

\  (let q__ = Take (q v_ = q_);                                           \

\       q__ = ((Rewrite sym_real_minus_eq_cancel True) @@                 \

\              (Rewrite Belastung_Querkraft True)) q__;                   \

\      (Q__:: bool) =                                                     \

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

\                          [Diff,integration,named])                      \

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

\       Q__ = Rewrite Querkraft_Moment True Q__;                          \

\      (M__::bool) =                                                      \

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

\                          [Diff,integration,named])                      \

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

\       e1__ = nth_ 1 rm_;                                                \

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

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

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

\       M2__ = Take M__;                                                  "^

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

"       e2__ = nth_ 2 rm_;                                                \

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

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

\                      (Substitute [e2__])) M2__;                         \

\      (c_1_2__::bool list) =                                             \

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

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

\       M__ = Take  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__;                    "^

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

"      (N__:: bool) =                                                     \

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

\                          [Diff,integration,named])                      \

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

\      (B__:: bool) =                                                     \

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

\                          [Diff,integration,named])                      \

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

\       e1__ = nth_ 1 rb_;                                                \

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

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

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

\       B2__ = Take B__;                                                  \

\       e2__ = nth_ 2 rb_;                                                \

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

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

\                      (Substitute [e2__])) B2__;                         \

\      (c_1_2__::bool list) =                                             \

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

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

\       B__ = Take  B__;                                                  \

\       B__ = ((Substitute c_1_2__) @@                                    \

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

\ in B__)"

));

store_met

    (prep_met Biegelinie.thy "met_biege_2" [] e_metID

	      (["IntegrierenUndKonstanteBestimmen2"],

	       [("#Given" ,["Traegerlaenge l_", "Streckenlast q_",

			    "FunktionsVariable v_"]),

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

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

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

		],

	       {rew_ord'="tless_true", 

		rls' = append_rls "erls_IntegrierenUndK.." e_rls 

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

				   Thm ("not_true",num_str not_true),

				   Thm ("not_false",num_str not_false)], 

		calc = [], 

		srls = append_rls "erls_IntegrierenUndK.." e_rls 

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

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

"Script Biegelinie2Script                                                 \

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

\  (let                                                                   \

\      (funs_:: bool list) =                                              \

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

\                          [Biegelinien,ausBelastung])                    \

\                          [real_ q_, real_ v_]);                         \

\      (equs_::bool list) =                                               \

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

\                          [Biegelinien,setzeRandbedingungenEin])         \

\                          [booll_ funs_, booll_ rb_]);                     \

\      (cons_::bool list) =                                               \

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

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

\       B_ = Take (last_elem funs_);                                      \

\       B_ = ((Substitute cons_) @@                                       \

\              (Rewrite_Set_Inst [(bdv, x)] make_ratpoly_in False)) B_    \

\ in B_)"

));

store_met

    (prep_met Biegelinie.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, nrls = e_rls},

"empty_script"

));

store_met

    (prep_met Biegelinie.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, nrls = e_rls},

"empty_script"

));

store_met

    (prep_met Biegelinie.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, nrls = e_rls},

"empty_script"

));

store_met

    (prep_met Biegelinie.thy "met_biege2" [] e_metID

	      (["Biegelinien"],

	       [],

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

		srls = e_rls, 

		prls=e_rls,

	     crls = Atools_erls, nrls = e_rls},

"empty_script"

));

store_met

    (prep_met Biegelinie.thy "met_biege_ausbelast" [] e_metID

	      (["Biegelinien","ausBelastung"],

	       [("#Given" ,["Streckenlast q_","FunktionsVariable v_"]),

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

	       {rew_ord'="tless_true", 

		rls' = append_rls "erls_ausBelastung" e_rls 

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

				   Thm ("not_true",num_str not_true),

				   Thm ("not_false",num_str not_false)], 

		calc = [], 

		srls = append_rls "srls_ausBelastung" e_rls 

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

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

"Script Belastung2BiegelScript (q_::real) (v_::real) =                    \

\  (let q__ = Take (q v_ = q_);                                           \

\       q__ = ((Rewrite sym_real_minus_eq_cancel True) @@                 \

\              (Rewrite Belastung_Querkraft True)) q__;                   \

\      (Q__:: bool) =                                                     \

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

\                          [Diff,integration,named])                      \

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

\       M__ = Rewrite Querkraft_Moment True Q__;                          \

\      (M__::bool) =                                                      \

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

\                          [Diff,integration,named])                      \

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

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

\              (Rewrite make_fun_explicit False)) M__;                    \

\      (N__:: bool) =                                                     \

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

\                          [Diff,integration,named])                      \

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

\      (B__:: bool) =                                                     \

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

\                          [Diff,integration,named])                      \

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

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

));

store_met

    (prep_met Biegelinie.thy "met_biege_setzrand" [] e_metID

	      (["Biegelinien","setzeRandbedingungenEin"],

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

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

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

		srls = srls2, 

		prls=e_rls,

	     crls = Atools_erls, nrls = e_rls},

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

\ (let b1_ = nth_ 1 rb_;                                         \

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

\      (e1_::bool) =                                             \

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

\                          [Equation,fromFunction])              \

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

\      b2_ = nth_ 2 rb_;                                         \

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

\      (e2_::bool) =                                             \

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

\                          [Equation,fromFunction])              \

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

\      b3_ = nth_ 3 rb_;                                         \

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

\      (e3_::bool) =                                             \

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

\                          [Equation,fromFunction])              \

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

\      b4_ = nth_ 4 rb_;                                         \

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

\      (e4_::bool) =                                             \

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

\                          [Equation,fromFunction])              \

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

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

));

store_met

    (prep_met Biegelinie.thy "met_equ" [] e_metID

	      (["Equation"],

	       [],

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

		srls = e_rls, 

		prls=e_rls,

	     crls = Atools_erls, nrls = e_rls},

"empty_script"

));

store_met

    (prep_met Biegelinie.thy "met_equ_fromfun" [] e_metID

	      (["Equation","fromFunction"],

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

		("#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, 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 (fun_::bool) (sub_::bool) =\

\ (let fun_ = Take fun_;                             \

\      bdv_ = argument_in (lhs fun_);                \

\      val_ = argument_in (lhs sub_);                \

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

\      equ_ = (Substitute [sub_]) fun_               \

\ in (Rewrite_Set norm_Rational False) equ_)             "

(*FIXME.WN060901. scr-interpreter ERROR in nxt_tac without Take above !*)

));

(* use"IsacKnowledge/Biegelinie.ML";

   *)