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

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

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

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

  Querkraft                :: "(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" (*\<longrightarrow> Input_Descript.thy: known by fun is_NObrack_list*)

  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>

setup \<open>ThyC.set_metadata {

  coursedesign = ["(c) Christian Dürnsteiner 2006 supported by a grant from NMI Austria"],

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

\<close>

(* ? more finegrained as above in Isabelle/PIDE ?* )

setup \<open>

Know_Store.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>Problem.T, trial to decouple the models/formal arguments\<close>

text \<open>

  (Only) here was a trial to decouple the model of the problem from the model of the method.

  E.g. for "Traegerlaenge" in the problem we had "l_l", while in the method we had "beam".

  This had been working with the old "fun arguments_from_model, relate_args" in LItool.

  But the Pre_Conds of Biegelinie were empty at that time --

  -- how should this work with Pre_Conds <>[] involved with both, problem and method?

  A kind of "model-translation" (see the old "fun LItool.arguments_from_model";

  there is already an implicit kind of relation exploitet by refinement)?

  In this changeset there is the decision to make the two models equal, of model and of method.

problem pbl_bieg : "Biegelinien" =

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

  Method_Ref: "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"

(* 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 = [], 

    prog_rls = 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>],

    where_rls = Rule_Set.Empty, errpats = [], rew_rls = 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"

(*here was a trial to decouple the model of the problem from the model of the method.*)

\<close>

problem pbl_bieg : "Biegelinien" =

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

  Method_Ref: "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_Ref: "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_Ref: "IntegrierenUndKonstanteBestimmen/2xIntegrieren"

problem pbl_bieg_einf : "einfache/Biegelinien" =

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

  Method_Ref: "IntegrierenUndKonstanteBestimmen/4x4System"

problem pbl_bieg_momquer : "QuerkraftUndMomentBestimmte/Biegelinien" =

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

  Method_Ref: "IntegrierenUndKonstanteBestimmen/1xIntegrieren"

problem pbl_bieg_vonq : "vonBelastungZu/Biegelinien" =

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

  Method_Ref: "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_Ref: "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_Ref: "Equation/fromFunction"

  Given: "functionEq fu_n" "substitution su_b"

  Find: "equality equ'''"

ML \<open>

(** methods **)

val prog_rls = Rule_Def.Repeat {

  id="srls_IntegrierenUnd..", preconds = [], rew_ord = ("termlessI",termlessI), 

	asm_rls = 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> (**)(Calc_Binop.numeric "#add_")], 

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

	rules = [

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

		 \<^rule_eval>\<open>plus\<close> (**)(Calc_Binop.numeric "#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")],

	program = Rule.Empty_Prog};

val srls2 = Rule_Def.Repeat {

  id="srls_IntegrierenUnd..", preconds = [], rew_ord = ("termlessI",termlessI), 

	asm_rls = 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> (**)(Calc_Binop.numeric "#add_")], 

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

	rules = [

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

	  \<^rule_eval>\<open>plus\<close> (**)(Calc_Binop.numeric "#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>],

	program = 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 = [], prog_rls = Rule_Set.Empty, where_rls = Rule_Set.Empty,

    errpats = [], rew_rls = Rule_Set.Empty}\<close>

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

text \<open>

  Calculations guided by IntegrierenUndKonstanteBestimmen are structured

  by the following Subproblems.

  An example calculation is found in test/../biegelinie-4.sml as

  test --- IntegrierenUndKonstanteBestimmen2: Bsp.7.70. me' with ALL subproblems ---.

  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 l_l                Randbedingungen r_b                    Biegemoment id_momentum

           Streckenlast q_q                      FunktionsVariable fun_var                  Querkraft id_lat_force

                   Biegelinie b_b                         AbleitungBiegelinie id_der                         GleichungsVariablen vs                *)

partial_function (tailrec) biegelinie ::

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

(* l_l-----q__q---r_b----------fun_var--id_der-----------id_momentum------id_lat_force------vs----------b_b--------------value

  Note: while the sequence of formal arguments tries to follow the sequence of items in the models

    (also the models of the SubProblems),

    the fairly liberal <fun relate_args> shifts b_b to the end -----------------------------------------^^^

*)

  where

"biegelinie l_l q_q r_b fun_var id_der id_momentum id_lat_force vs  b_b = (

  let

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

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

        [REAL q_q, REAL fun_var, REAL_REAL b_b, REAL_REAL id_der, REAL_REAL id_momentum, REAL_REAL id_lat_force];

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

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

    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 = [], 

    prog_rls = 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>],

    where_rls = Rule_Set.Empty, errpats = [], rew_rls = Rule_Set.Empty}\<close>

  Program: biegelinie.simps

  Given: "Traegerlaenge l_l" "Streckenlast q_q"

    (*OLD "FunktionsVariable fun_var" "GleichungsVariablen vs" "AbleitungBiegelinie id_der"*)

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

    "Randbedingungen r_b"

  (* Items for MethodC "IntegrierenUndKonstanteBestimmen2" *)

    (*NEW*)"FunktionsVariable fun_var"

      "AbleitungBiegelinie id_der" "Biegemoment id_momentum" "Querkraft id_lat_force"

  (* Item for Problem "LINEAR/system", which by [''no_met''] involves refinement *)

    "GleichungsVariablen vs"(*NEW*)

  Find: "Biegelinie b_b"

method met_biege_intconst_2 : "IntegrierenUndKonstanteBestimmen/2xIntegrieren" =

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

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

method met_biege_intconst_4 : "IntegrierenUndKonstanteBestimmen/4x4System" =

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

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

method met_biege_intconst_1 : "IntegrierenUndKonstanteBestimmen/1xIntegrieren" =

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

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

method met_biege2 : "Biegelinien" =

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

    errpats = [], rew_rls = 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       

                                                      id_lateral_force  id_momentum               *)

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

(* q__q----v_v------b_b--------------id_der-----------id_momentum-------id_lat_force-----value*)

  where

"belastung_zu_biegelinie q__q v_v b_b id_der id_momentum id_lat_force = (

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

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

    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 b_b]

  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 = [], 

    prog_rls = Rule_Set.append_rules "srls_ausBelastung" Rule_Set.empty [

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

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

  Program: belastung_zu_biegelinie.simps

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

         (*NEW*)"Biegemoment id_momentum" "Querkraft id_lat_force"(*NEW*)

  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 = [], prog_rls = srls2, where_rls=Rule_Set.empty,

    errpats = [], rew_rls = 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 = [],

    prog_rls = 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")],

    where_rls=Rule_Set.empty, errpats = [], rew_rls = 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