(* 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 Base_Tools 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"

   AbleitungBiegelinie      :: "(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"

   GleichungsVariablen      :: "real list => una"

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

 setup \<open>

 KEStore_Elems.add_thes

   [make_thy @{theory}

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

   make_isa @{theory} ("IsacKnowledge", "Theorems")

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

   make_thm @{theory}  "IsacKnowledge" ("Belastung_Querkraft", @{thm Belastung_Querkraft})

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

   make_thm @{theory}  "IsacKnowledge" ("Moment_Neigung", @{thm Moment_Neigung})

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

   make_thm @{theory}  "IsacKnowledge" ("Moment_Querkraft", @{thm Moment_Querkraft})

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

   make_thm @{theory}  "IsacKnowledge" ("Neigung_Moment", @{thm Neigung_Moment})

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

   make_thm @{theory}  "IsacKnowledge" ("Querkraft_Belastung", @{thm Querkraft_Belastung})

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

   make_thm @{theory}  "IsacKnowledge" ("Querkraft_Moment", @{thm Querkraft_Moment})

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

   make_thm @{theory}  "IsacKnowledge" ("make_fun_explicit", @{thm make_fun_explicit})

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

 \<close>

 (** problems **)

 setup \<open>KEStore_Elems.add_pbts

   [(Specify.prep_pbt @{theory} "pbl_bieg" [] Celem.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"])],

         Rule_Set.append_rules "empty" Rule_Set.empty [], NONE, [["IntegrierenUndKonstanteBestimmen2"]])),

     (Specify.prep_pbt @{theory} "pbl_bieg_mom" [] Celem.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"])

         ],

         Rule_Set.append_rules "empty" Rule_Set.empty [], NONE, [["IntegrierenUndKonstanteBestimmen"]])),

     (Specify.prep_pbt @{theory} "pbl_bieg_momg" [] Celem.e_pblID

       (["MomentGegebene","Biegelinien"], [], Rule_Set.append_rules "empty" Rule_Set.empty [], NONE,

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

     (Specify.prep_pbt @{theory} "pbl_bieg_einf" [] Celem.e_pblID

       (["einfache","Biegelinien"], [], Rule_Set.append_rules "empty" Rule_Set.empty [], NONE,

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

     (Specify.prep_pbt @{theory} "pbl_bieg_momquer" [] Celem.e_pblID

       (["QuerkraftUndMomentBestimmte","Biegelinien"], [], Rule_Set.append_rules "empty" Rule_Set.empty [], NONE,

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

     (Specify.prep_pbt @{theory} "pbl_bieg_vonq" [] Celem.e_pblID

       (["vonBelastungZu","Biegelinien"],

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

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

         Rule_Set.append_rules "empty" Rule_Set.empty [], NONE, [["Biegelinien","ausBelastung"]])),

     (Specify.prep_pbt @{theory} "pbl_bieg_randbed" [] Celem.e_pblID

       (["setzeRandbedingungen","Biegelinien"],

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

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

         Rule_Set.append_rules "empty" Rule_Set.empty [], NONE, [["Biegelinien","setzeRandbedingungenEin"]])),

     (Specify.prep_pbt @{theory} "pbl_equ_fromfun" [] Celem.e_pblID

       (["makeFunctionTo","equation"],

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

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

         Rule_Set.append_rules "empty" Rule_Set.empty [], NONE, [["Equation","fromFunction"]]))]\<close>

 ML \<open>

 (** methods **)

 val srls = Rule_Def.Repeat {id="srls_IntegrierenUnd..", 

 		preconds = [], 

 		rew_ord = ("termlessI",termlessI), 

 		erls = Rule_Set.append_rules "erls_in_srls_IntegrierenUnd.." Rule_Set.empty

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

 				   Rule.Eval ("Orderings.ord_class.less", Prog_Expr.eval_equ "#less_"),

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

 				   Rule.Eval("Groups.plus_class.plus", (**)eval_binop "#add_")

 				   ], 

 		srls = Rule_Set.Empty, calc = [], errpatts = [],

 		rules = [Rule.Thm ("NTH_CONS",ThmC.numerals_to_Free @{thm NTH_CONS}),

 			 Rule.Eval("Groups.plus_class.plus", (**)eval_binop "#add_"),

 			 Rule.Thm ("NTH_NIL",ThmC.numerals_to_Free @{thm NTH_NIL}),

 			 Rule.Eval("Prog_Expr.lhs", Prog_Expr.eval_lhs"eval_lhs_"),

 			 Rule.Eval("Prog_Expr.rhs", Prog_Expr.eval_rhs"eval_rhs_"),

 			 Rule.Eval("Prog_Expr.argument'_in", Prog_Expr.eval_argument_in "Prog_Expr.argument'_in")

 			 ],

 		scr = Rule.Empty_Prog};

 val srls2 = 

     Rule_Def.Repeat {id="srls_IntegrierenUnd..", 

 	 preconds = [], 

 	 rew_ord = ("termlessI",termlessI), 

 	 erls = Rule_Set.append_rules "erls_in_srls_IntegrierenUnd.." Rule_Set.empty

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

 			    Rule.Eval ("Orderings.ord_class.less", Prog_Expr.eval_equ "#less_"),

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

 			    Rule.Eval("Groups.plus_class.plus", (**)eval_binop "#add_")

 			    ], 

 	 srls = Rule_Set.Empty, calc = [], errpatts = [],

 	 rules = [Rule.Thm ("NTH_CONS",ThmC.numerals_to_Free @{thm NTH_CONS}),

 		  Rule.Eval("Groups.plus_class.plus", (**)eval_binop "#add_"),

 		  Rule.Thm ("NTH_NIL", ThmC.numerals_to_Free @{thm NTH_NIL}),

 		  Rule.Eval("Prog_Expr.lhs", Prog_Expr.eval_lhs "eval_lhs_"),

 		  Rule.Eval("Prog_Expr.filter'_sameFunId", Prog_Expr.eval_filter_sameFunId "Prog_Expr.filter'_sameFunId"),

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

 		  Rule.Eval("Prog_Expr.sameFunId", Prog_Expr.eval_sameFunId "Prog_Expr.sameFunId"),

 		  Rule.Thm ("filter_Cons", ThmC.numerals_to_Free @{thm filter_Cons}),

 		  Rule.Thm ("filter_Nil", ThmC.numerals_to_Free @{thm filter_Nil}),

 		  Rule.Thm ("if_True", ThmC.numerals_to_Free @{thm if_True}),

 		  Rule.Thm ("if_False", ThmC.numerals_to_Free @{thm if_False}),

 		  Rule.Thm ("hd_thm", ThmC.numerals_to_Free @{thm hd_thm})

 		  ],

 	 scr = Rule.Empty_Prog};

 \<close>

 section \<open>Methods\<close>

 (* setup parent directory *)

 setup \<open>KEStore_Elems.add_mets

     [Specify.prep_met @{theory} "met_biege" [] Celem.e_metID 

 	    (["IntegrierenUndKonstanteBestimmen"], [],

 	    {rew_ord'="tless_true", rls'= Rule_Set.Empty, calc = [], srls = Rule_Set.Empty, prls = Rule_Set.Empty, crls =Rule_Set.Empty,

           errpats = [], nrls = Rule_Set.Empty},

       @{thm refl})]

 \<close>

 subsection \<open>Sub-problem "integrate and determine constants", nicely modularised\<close>

 partial_function (tailrec) biegelinie ::

   "real \<Rightarrow> real \<Rightarrow> real \<Rightarrow> (real \<Rightarrow> real) \<Rightarrow> bool list \<Rightarrow> real list \<Rightarrow> (real \<Rightarrow> real) \<Rightarrow> bool"

   where

 "biegelinie l q v b s vs id_abl = (

   let

     funs = SubProblem (''Biegelinie'', [''vonBelastungZu'', ''Biegelinien''],

       [''Biegelinien'', ''ausBelastung'']) [REAL q, REAL v, REAL_REAL b, REAL_REAL id_abl];

     equs = SubProblem (''Biegelinie'', [''setzeRandbedingungen'', ''Biegelinien''],

       [''Biegelinien'', ''setzeRandbedingungenEin'']) [BOOL_LIST funs, BOOL_LIST s];

     cons = SubProblem (''Biegelinie'', [''LINEAR'', ''system''],

       [''no_met'']) [BOOL_LIST equs, REAL_LIST vs];

     B = Take (lastI funs);

     B = ((Substitute cons) #> (Rewrite_Set_Inst [(''bdv'', v)] ''make_ratpoly_in'')) B

   in B)"

 setup \<open>KEStore_Elems.add_mets

     [Specify.prep_met @{theory} "met_biege_2" [] Celem.e_metID

 	    (["IntegrierenUndKonstanteBestimmen2"],

 	      [("#Given" ,["Traegerlaenge l", "Streckenlast q",

               "FunktionsVariable v", "GleichungsVariablen vs", "AbleitungBiegelinie id_abl"]),

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

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

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

 	      {rew_ord'="tless_true", 

 	        rls' = Rule_Set.append_rules "erls_IntegrierenUndK.." Rule_Set.empty 

 				      [Rule.Eval ("Prog_Expr.ident", Prog_Expr.eval_ident "#ident_"),

 				        Rule.Thm ("not_true",ThmC.numerals_to_Free @{thm not_true}),

 				        Rule.Thm ("not_false",ThmC.numerals_to_Free @{thm not_false})], 

 				  calc = [], 

 				  srls = Rule_Set.append_rules "erls_IntegrierenUndK.." Rule_Set.empty 

 				      [Rule.Eval("Prog_Expr.rhs", Prog_Expr.eval_rhs"eval_rhs_"),

 				        Rule.Eval ("Prog_Expr.ident", Prog_Expr.eval_ident "#ident_"),

 				        Rule.Thm ("last_thmI",ThmC.numerals_to_Free @{thm last_thmI}),

 				        Rule.Thm ("if_True",ThmC.numerals_to_Free @{thm if_True}),

 				        Rule.Thm ("if_False",ThmC.numerals_to_Free @{thm if_False})],

 				  prls = Rule_Set.Empty, crls = Atools_erls, errpats = [], nrls = Rule_Set.Empty},

         @{thm biegelinie.simps})]

 \<close>

 setup \<open>KEStore_Elems.add_mets

     [Specify.prep_met @{theory} "met_biege_intconst_2" [] Celem.e_metID

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

 	      {rew_ord'="tless_true", rls'=Rule_Set.Empty, calc = [], srls = Rule_Set.empty, prls=Rule_Set.empty, crls = Atools_erls,

           errpats = [], nrls = Rule_Set.empty},

         @{thm refl}),

     Specify.prep_met @{theory} "met_biege_intconst_4" [] Celem.e_metID

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

 	      {rew_ord'="tless_true", rls'=Rule_Set.Empty, calc = [], srls = Rule_Set.empty, prls=Rule_Set.empty, crls = Atools_erls,

           errpats = [], nrls = Rule_Set.empty},

         @{thm refl}),

     Specify.prep_met @{theory} "met_biege_intconst_1" [] Celem.e_metID

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

         {rew_ord'="tless_true", rls'=Rule_Set.Empty, calc = [], srls = Rule_Set.empty, prls=Rule_Set.empty, crls = Atools_erls,

           errpats = [], nrls = Rule_Set.empty},

         @{thm refl}),

     Specify.prep_met @{theory} "met_biege2" [] Celem.e_metID

 	    (["Biegelinien"], [],

 	      {rew_ord'="tless_true", rls'=Rule_Set.Empty, calc = [], srls = Rule_Set.empty, prls=Rule_Set.empty, crls = Atools_erls,

           errpats = [], nrls = Rule_Set.empty},

         @{thm refl})]

 \<close>

 subsection \<open>Compute the general bending line\<close>

 partial_function (tailrec) belastung_zu_biegelinie :: "real \<Rightarrow> real \<Rightarrow> (real \<Rightarrow> real) \<Rightarrow> (real \<Rightarrow> real) \<Rightarrow> bool list"

   where

 "belastung_zu_biegelinie q__q v_v id_fun id_abl = (

   let

     q___q = Take (qq v_v = q__q);

     q___q = (

       (Rewrite ''sym_neg_equal_iff_equal'') #>

       (Rewrite ''Belastung_Querkraft'')) q___q;

     Q__Q = SubProblem (''Biegelinie'', [''named'', ''integrate'', ''function''],

       [''diff'', ''integration'', ''named'']) [REAL (rhs q___q), REAL v_v, REAL_REAL Q];

     M__M = Rewrite ''Querkraft_Moment'' Q__Q;

     M__M = SubProblem (''Biegelinie'', [''named'', ''integrate'', ''function''],

       [''diff'', ''integration'', ''named'']) [REAL (rhs M__M), REAL v_v, REAL_REAL M_b];

     N__N = (

       (Rewrite ''Moment_Neigung'' ) #> (Rewrite ''make_fun_explicit'' )) M__M;

     N__N = SubProblem (''Biegelinie'', [''named'', ''integrate'', ''function''],

       [''diff'', ''integration'', ''named'']) [REAL (rhs N__N), REAL v_v, REAL_REAL id_abl];

     B__B = SubProblem (''Biegelinie'', [''named'', ''integrate'', ''function''],

       [''diff'', ''integration'', ''named'']) [REAL (rhs N__N), REAL v_v, REAL_REAL id_fun]

   in

     [Q__Q, M__M, N__N, B__B])"

 setup \<open>KEStore_Elems.add_mets

     [Specify.prep_met @{theory} "met_biege_ausbelast" [] Celem.e_metID

 	    (["Biegelinien", "ausBelastung"],

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

             "Biegelinie id_fun", "AbleitungBiegelinie id_abl"]),

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

 	      {rew_ord'="tless_true", 

 	        rls' = Rule_Set.append_rules "erls_ausBelastung" Rule_Set.empty 

 				      [Rule.Eval ("Prog_Expr.ident", Prog_Expr.eval_ident "#ident_"),

 				        Rule.Thm ("not_true", ThmC.numerals_to_Free @{thm not_true}),

 				        Rule.Thm ("not_false", ThmC.numerals_to_Free @{thm not_false})], 

 				  calc = [], 

 				  srls = Rule_Set.append_rules "srls_ausBelastung" Rule_Set.empty 

 				      [Rule.Eval ("Prog_Expr.rhs", Prog_Expr.eval_rhs "eval_rhs_")], 

 				  prls = Rule_Set.empty, crls = Atools_erls, errpats = [], nrls = Rule_Set.empty},

         @{thm belastung_zu_biegelinie.simps})]

 \<close>

 subsection \<open>Substitute the constraints into the equations\<close>

 partial_function (tailrec) setzte_randbedingungen :: "bool list \<Rightarrow> bool list \<Rightarrow> bool list"

   where 

 "setzte_randbedingungen fun_s r_b = (

   let

     b_1 = NTH 1 r_b;

     f_s = filter_sameFunId (lhs b_1) fun_s;

     e_1 = 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 = 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 = 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 = SubProblem (''Biegelinie'', [''makeFunctionTo'', ''equation''],

              [''Equation'', ''fromFunction'']) [BOOL (hd f_s), BOOL b_4]

   in

     [e_1, e_2, e_3, e_4])"

 setup \<open>KEStore_Elems.add_mets

     [Specify.prep_met @{theory} "met_biege_setzrand" [] Celem.e_metID

 	    (["Biegelinien", "setzeRandbedingungenEin"],

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

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

 	      {rew_ord'="tless_true", rls'=Rule_Set.Empty, calc = [], srls = srls2, prls=Rule_Set.empty, crls = Atools_erls,

           errpats = [], nrls = Rule_Set.empty},

         @{thm setzte_randbedingungen.simps})]

 \<close>

 subsection \<open>Transform an equality into a function\<close>

         (*(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*)

 partial_function (tailrec) function_to_equality :: "bool \<Rightarrow> bool \<Rightarrow> bool"

   where

 "function_to_equality fu_n su_b = (

   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; \<comment> \<open>([1], Res), M_b L = c_2 + c * L + -1 * q_0 / 2 * L ^^^ 2\<close>

     eq_u = Substitute [su_b] eq_u

   in

     (Rewrite_Set ''norm_Rational'') eq_u)"

 setup \<open>KEStore_Elems.add_mets

     [Specify.prep_met @{theory} "met_equ_fromfun" [] Celem.e_metID

 	    (["Equation","fromFunction"],

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

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

 	      {rew_ord'="tless_true", rls'=Rule_Set.Empty, calc = [],

           srls = Rule_Set.append_rules "srls_in_EquationfromFunc" Rule_Set.empty

 				      [Rule.Eval("Prog_Expr.lhs", Prog_Expr.eval_lhs "eval_lhs_"),

 				        Rule.Eval("Prog_Expr.argument'_in", Prog_Expr.eval_argument_in "Prog_Expr.argument'_in")], 

 				  prls=Rule_Set.empty, crls = Atools_erls, errpats = [], nrls = Rule_Set.empty},

         (*(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*)

         @{thm function_to_equality.simps})]

 \<close>

 ML \<open>

 \<close> ML \<open>

 \<close>

 end