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

section \<open>Constants specific for Biegelinie\<close>

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

  Isabelle2020: new handling of quotes in mixfix in, so the parser cannot distinguish M_b  M_b'

Outcommenting causes error at Neigung_Moment:   "y'' x = -M_b x/ EI" below:

Ambiguous input\<^here> produces 2 parse trees:

  ("\<^const>HOL.Trueprop"

    ("\<^const>HOL.eq" ("_applC" ("_position" y'') ("_position" x))

      ("\<^const>Fields.inverse_class.inverse_divide" ("\<^const>Groups.uminus_class.uminus" ("_applC" ("\<^const>Biegelinie_Test.M_b") ("_position" x)))

        ("_position" EI))))

  ("\<^const>HOL.Trueprop"

    ("\<^const>HOL.eq" ("_applC" ("_position" y'') ("_position" x))

      ("\<^const>Fields.inverse_class.inverse_divide" ("\<^const>Groups.uminus_class.uminus" ("_applC" ("\<^const>Biegelinie_Test.M_b'") ("_position" x)))

        ("_position" EI))))

Ambiguous input -------------------------------------------------------------------------------------------------------^^^^^^

2 terms are type correct:

  ((y'' x) = ((- (M_b x)) / EI))

  ((y'' x) = ((- (M_b x)) / EI))

Failed to parse prop

*)

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

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

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

  EI    :: "real"                     (* Biegesteifigkeit           *)

section \<open>Descriptions extending Input_Descript.thy\<close>

consts

  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"

section \<open>Theorems from statics, still as axioms\<close>

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:     "~ (a =!= 0) ==> (a * (f x) = bb) = (f x = 1/a * bb)"

section \<open>Acknowledgements shown in browsers of Isac_Knowledge\<close>

(* there will be other ways in Isabelle/PIDE * )

setup \<open>

KEStore_Elems.add_thes

  [Thy_Hierarchy.make_thy @{theory}

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

\<close>

( **)

section \<open>Problems\<close>

problem pbl_bieg : "Biegelinien" =

  \<open>Rule_Set.append_rules "empty" Rule_Set.empty []\<close>

  Method: "IntegrierenUndKonstanteBestimmen2"

  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"

problem pbl_bieg_mom : "MomentBestimmte/Biegelinien" =

  \<open>Rule_Set.append_rules "empty" Rule_Set.empty []\<close>

  Method: "IntegrierenUndKonstanteBestimmen"

  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"

problem pbl_bieg_momg : "MomentGegebene/Biegelinien" =

  \<open>Rule_Set.append_rules "empty" Rule_Set.empty []\<close>

  Method: "IntegrierenUndKonstanteBestimmen/2xIntegrieren"

problem pbl_bieg_einf : "einfache/Biegelinien" =

  \<open>Rule_Set.append_rules "empty" Rule_Set.empty []\<close>

  Method: "IntegrierenUndKonstanteBestimmen/4x4System"

problem pbl_bieg_momquer : "QuerkraftUndMomentBestimmte/Biegelinien" =

  \<open>Rule_Set.append_rules "empty" Rule_Set.empty []\<close>

  Method: "IntegrierenUndKonstanteBestimmen/1xIntegrieren"

problem pbl_bieg_vonq : "vonBelastungZu/Biegelinien" =

  \<open>Rule_Set.append_rules "empty" Rule_Set.empty []\<close>

  Method: "Biegelinien/ausBelastung"

  Given: "Streckenlast q_q" "FunktionsVariable v_v"

  Find: "Funktionen funs'''"

problem pbl_bieg_randbed : "setzeRandbedingungen/Biegelinien" =

  \<open>Rule_Set.append_rules "empty" Rule_Set.empty []\<close>

  Method: "Biegelinien/setzeRandbedingungenEin"

  Given: "Funktionen fun_s" "Randbedingungen r_b"

  Find: "Gleichungen equs'''"

problem pbl_equ_fromfun : "makeFunctionTo/equation" =

  \<open>Rule_Set.append_rules "empty" Rule_Set.empty []\<close>

  Method: "Equation/fromFunction"

  Given: "functionEq fu_n" "substitution su_b"

  Find: "equality equ'''"

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>\<open>less\<close> (Prog_Expr.eval_equ "#less_"),

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

				   \<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_")

				   ], 

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

		rules = [\<^rule_thm>\<open>NTH_CONS\<close>,

			 \<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_"),

			 \<^rule_thm>\<open>NTH_NIL\<close>,

			 \<^rule_eval>\<open>Prog_Expr.lhs\<close> (Prog_Expr.eval_lhs"eval_lhs_"),

			 \<^rule_eval>\<open>Prog_Expr.rhs\<close> (Prog_Expr.eval_rhs"eval_rhs_"),

			 \<^rule_eval>\<open>Prog_Expr.argument_in\<close> (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>\<open>less\<close> (Prog_Expr.eval_equ "#less_"),

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

			    \<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_")

			    ], 

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

	 rules = [\<^rule_thm>\<open>NTH_CONS\<close>,

		  \<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_"),

		  \<^rule_thm>\<open>NTH_NIL\<close>,

		  \<^rule_eval>\<open>Prog_Expr.lhs\<close> (Prog_Expr.eval_lhs "eval_lhs_"),

		  \<^rule_eval>\<open>Prog_Expr.filter_sameFunId\<close> (Prog_Expr.eval_filter_sameFunId "Prog_Expr.filter_sameFunId"),

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

		  \<^rule_eval>\<open>Prog_Expr.sameFunId\<close> (Prog_Expr.eval_sameFunId "Prog_Expr.sameFunId"),

		  \<^rule_thm>\<open>filter_Cons\<close>,

		  \<^rule_thm>\<open>filter_Nil\<close>,

		  \<^rule_thm>\<open>if_True\<close>,

		  \<^rule_thm>\<open>if_False\<close>,

		  \<^rule_thm>\<open>hd_thm\<close>

		  ],

	 scr = Rule.Empty_Prog};

\<close>

section \<open>Methods\<close>

(* setup parent directory *)

method met_biege : "IntegrierenUndKonstanteBestimmen" =

  \<open>{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}\<close>

subsection \<open>Survey on Methods\<close>

text \<open>

  Theory "Biegelinie" used by all Subproblems

  v-- the root Problem calling SubProblems according to indentation

  Problem ["Biegelinien"]

  MethodC ["IntegrierenUndKonstanteBestimmen2"]  biegelinie

    Problem ["vonBelastungZu", "Biegelinien"]

    MethodC ["Biegelinien", "ausBelastung"]  belastung_zu_biegelinie

      Problem ["named", "integrate", "function"]

      MethodC ["diff", "integration", "named"]

      -"- 4 times

    Problem ["setzeRandbedingungen", "Biegelinien"]

    MethodC ["Biegelinien", "setzeRandbedingungenEin"]  setzte_randbedingungen

      Problem ["makeFunctionTo", "equation"]

      MethodC ["Equation", "fromFunction"]

      -"- 4 times

    Problem ["LINEAR", "system"]

    MethodC ["no_met"]

             ^^^^^^--- thus automatied refinement to appropriate Problem

\<close>

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

(* Traegerlaenge beam      Biegelinie!TYPE! id_fun                    AbleitungBiegelinie id_der

           Streckenlast load                Randbedingungen side_conds                 Biegelinie \<noteq>!TYPE!

                   FunktionsVariable fun_var             GleichungsVariablen vs                *)

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 beam load fun_var id_fun side_conds vs id_der = (

  let

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

      [''Biegelinien'', ''ausBelastung''])

        [REAL load, REAL fun_var, REAL_REAL id_fun, REAL_REAL id_der];

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

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

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

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

    B = Take (lastI funs);

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

  in B)"

method met_biege_2 : "IntegrierenUndKonstanteBestimmen2" =

  \<open>{rew_ord'="tless_true",

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

        [\<^rule_eval>\<open>Prog_Expr.ident\<close> (Prog_Expr.eval_ident "#ident_"),

          \<^rule_thm>\<open>not_true\<close>,

          \<^rule_thm>\<open>not_false\<close>], 

    calc = [], 

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

        [\<^rule_eval>\<open>Prog_Expr.rhs\<close> (Prog_Expr.eval_rhs"eval_rhs_"),

          \<^rule_eval>\<open>Prog_Expr.ident\<close> (Prog_Expr.eval_ident "#ident_"),

          \<^rule_thm>\<open>last_thmI\<close>,

          \<^rule_thm>\<open>if_True\<close>,

          \<^rule_thm>\<open>if_False\<close>],

    prls = Rule_Set.Empty, crls = Atools_erls, errpats = [], nrls = Rule_Set.Empty}\<close>

  Program: biegelinie.simps

  Given: "Traegerlaenge beam" "Streckenlast load"

    "FunktionsVariable fun_var" "GleichungsVariablen vs" "AbleitungBiegelinie id_der"

  (* Where: "0 < beam" ...wait for &lt; and handling Arbfix*)

  Find: "Biegelinie id_fun"

  Relate: "Randbedingungen side_conds"

method met_biege_intconst_2 : "IntegrierenUndKonstanteBestimmen/2xIntegrieren" =

  \<open>{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}\<close>

method met_biege_intconst_4 : "IntegrierenUndKonstanteBestimmen/4x4System" =

  \<open>{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}\<close>

method met_biege_intconst_1 : "IntegrierenUndKonstanteBestimmen/1xIntegrieren" =

  \<open>{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}\<close>

method met_biege2 : "Biegelinien" =

  \<open>{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}\<close>

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

partial_function (tailrec) belastung_zu_biegelinie ::

(* Streckenlast     Biegelinie                       Funktionen

           FunktionsVariable         AbleitungBiegelinie       *)

  "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_der = (

  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_der];

    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])"  (*..Q is Const Querkraft    -------------------------^ *)

method met_biege_ausbelast : "Biegelinien/ausBelastung" =

  \<open>{rew_ord'="tless_true", 

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

        [\<^rule_eval>\<open>Prog_Expr.ident\<close> (Prog_Expr.eval_ident "#ident_"),

          \<^rule_thm>\<open>not_true\<close>,

          \<^rule_thm>\<open>not_false\<close>],

    calc = [], 

    srls = Rule_Set.append_rules "srls_ausBelastung" Rule_Set.empty

        [\<^rule_eval>\<open>Prog_Expr.rhs\<close> (Prog_Expr.eval_rhs "eval_rhs_")],

    prls = Rule_Set.empty, crls = Atools_erls, errpats = [], nrls = Rule_Set.empty}\<close>

  Program: belastung_zu_biegelinie.simps

  Given: "Streckenlast q__q" "FunktionsVariable v_v" "Biegelinie id_fun" "AbleitungBiegelinie id_der"

  Find: "Funktionen fun_s"

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

method met_biege_setzrand : "Biegelinien/setzeRandbedingungenEin" =

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

    errpats = [], nrls = Rule_Set.empty}\<close>

  Program: setzte_randbedingungen.simps

  Given: "Funktionen fun_s" "Randbedingungen r_b"

  Find: "Gleichungen equs'''"

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

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

               0 = c_2 + c * L + -1 * q_0 / 2 * L \<up> 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 \<up> 2\<close>

    eq_u = Substitute [su_b] eq_u

  in

    (Rewrite_Set ''norm_Rational'') eq_u)"

method met_equ_fromfun : "Equation/fromFunction" =

  \<open>{rew_ord'="tless_true", rls'=Rule_Set.Empty, calc = [],

    srls = Rule_Set.append_rules "srls_in_EquationfromFunc" Rule_Set.empty

        [\<^rule_eval>\<open>Prog_Expr.lhs\<close> (Prog_Expr.eval_lhs "eval_lhs_"),

          \<^rule_eval>\<open>Prog_Expr.argument_in\<close> (Prog_Expr.eval_argument_in "Prog_Expr.argument_in")],

    prls=Rule_Set.empty, crls = Atools_erls, errpats = [], nrls = Rule_Set.empty}\<close>

  Program: function_to_equality.simps

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

         0 = c_2 + c * L + -1 * q_0 / 2 * L \<up> 2*)

  Given: "functionEq fu_n" "substitution su_b"

  Find: "equality equ'''"

ML \<open>

\<close> ML \<open>

\<close> ML \<open>

\<close>

end