src/Tools/isac/Knowledge/Biegelinie.thy
author wneuper <Walther.Neuper@jku.at>
Tue, 31 May 2022 09:36:02 +0200
changeset 60437 023f3a30596a
parent 60436 1c8263e775d4
child 60449 2406d378cede
permissions -rw-r--r--
Calculation 1''': remove test-code from previous changeset 1c8263e775d4
neuper@37906
     1
(* chapter 'Biegelinie' from the textbook: 
neuper@37906
     2
   Timischl, Kaiser. Ingenieur-Mathematik 3. Wien 1999. p.268-271.
neuper@37999
     3
   author: Walther Neuper 050826,
neuper@37906
     4
   (c) due to copyright terms
neuper@37906
     5
*)
neuper@37906
     6
wneuper@59424
     7
theory Biegelinie imports Integrate Equation EqSystem Base_Tools begin
neuper@37906
     8
walther@60023
     9
section \<open>Constants specific for Biegelinie\<close>
walther@60023
    10
neuper@37906
    11
consts
neuper@42385
    12
  qq    :: "real => real"             (* Streckenlast               *)
neuper@37999
    13
  Q     :: "real => real"             (* Querkraft                  *)
neuper@37999
    14
  Q'    :: "real => real"             (* Ableitung der Querkraft    *)
walther@60278
    15
  M_b  :: "real => real" ("M'_b")    (* Biegemoment                *)
walther@60278
    16
(*M_b' :: "real => real" ("M_b' ")  ( * Ableitung des Biegemoments
walther@60278
    17
  Isabelle2020: new handling of quotes in mixfix in, so the parser cannot distinguish M_b  M_b'
walther@60086
    18
walther@60086
    19
Outcommenting causes error at Neigung_Moment:   "y'' x = -M_b x/ EI" below:
walther@60086
    20
Ambiguous input\<^here> produces 2 parse trees:
walther@60086
    21
  ("\<^const>HOL.Trueprop"
walther@60086
    22
    ("\<^const>HOL.eq" ("_applC" ("_position" y'') ("_position" x))
walther@60278
    23
      ("\<^const>Fields.inverse_class.inverse_divide" ("\<^const>Groups.uminus_class.uminus" ("_applC" ("\<^const>Biegelinie_Test.M_b") ("_position" x)))
walther@60086
    24
        ("_position" EI))))
walther@60086
    25
  ("\<^const>HOL.Trueprop"
walther@60086
    26
    ("\<^const>HOL.eq" ("_applC" ("_position" y'') ("_position" x))
walther@60278
    27
      ("\<^const>Fields.inverse_class.inverse_divide" ("\<^const>Groups.uminus_class.uminus" ("_applC" ("\<^const>Biegelinie_Test.M_b'") ("_position" x)))
walther@60086
    28
        ("_position" EI))))
walther@60086
    29
Ambiguous input -------------------------------------------------------------------------------------------------------^^^^^^
walther@60086
    30
2 terms are type correct:
walther@60086
    31
  ((y'' x) = ((- (M_b x)) / EI))
walther@60086
    32
  ((y'' x) = ((- (M_b x)) / EI))
walther@60086
    33
Failed to parse prop
walther@60086
    34
*)
neuper@37999
    35
  y''   :: "real => real"             (* 2.Ableitung der Biegeline  *)
neuper@37999
    36
  y'    :: "real => real"             (* Neigung der Biegeline      *)
neuper@37999
    37
(*y     :: "real => real"             (* Biegeline                  *)*)
neuper@37999
    38
  EI    :: "real"                     (* Biegesteifigkeit           *)
neuper@37906
    39
walther@60023
    40
walther@60023
    41
section \<open>Descriptions extending Input_Descript.thy\<close>
walther@60023
    42
walther@60023
    43
consts
neuper@37999
    44
  Traegerlaenge            :: "real => una"
neuper@37999
    45
  Streckenlast             :: "real => una"
neuper@37999
    46
  BiegemomentVerlauf       :: "bool => una"
neuper@37999
    47
  Biegelinie               :: "(real => real) => una"
wneuper@59540
    48
  AbleitungBiegelinie      :: "(real => real) => una"
neuper@37999
    49
  Randbedingungen          :: "bool list => una"
neuper@37999
    50
  RandbedingungenBiegung   :: "bool list => una"
neuper@37999
    51
  RandbedingungenNeigung   :: "bool list => una"
neuper@37999
    52
  RandbedingungenMoment    :: "bool list => una"
neuper@37999
    53
  RandbedingungenQuerkraft :: "bool list => una"
neuper@37999
    54
  FunktionsVariable        :: "real => una"
neuper@37999
    55
  Funktionen               :: "bool list => una"
neuper@37999
    56
  Gleichungen              :: "bool list => una"
wneuper@59539
    57
  GleichungsVariablen      :: "real list => una"
neuper@37906
    58
walther@60023
    59
walther@60023
    60
section \<open>Theorems from statics, still as axioms\<close>
walther@60023
    61
neuper@52148
    62
axiomatization where
neuper@37906
    63
neuper@52148
    64
  Querkraft_Belastung:   "Q' x = -qq x" and
neuper@52148
    65
  Belastung_Querkraft:   "-qq x = Q' x" and
neuper@37906
    66
neuper@52148
    67
  Moment_Querkraft:      "M_b' x = Q x" and
neuper@52148
    68
  Querkraft_Moment:      "Q x = M_b' x" and
neuper@37906
    69
walther@60079
    70
  Neigung_Moment:        "y'' x = -M_b (x / EI)" and
walther@60079
    71
  Moment_Neigung:        "(M_b x) = -EI * y'' x" and
neuper@37906
    72
neuper@37906
    73
  (*according to rls 'simplify_Integral': .. = 1/a * .. instead .. = ../ a*)
walther@60278
    74
  make_fun_explicit:     "~ (a =!= 0) ==> (a * (f x) = bb) = (f x = 1/a * bb)"
neuper@37906
    75
walther@60023
    76
walther@60023
    77
section \<open>Acknowledgements shown in browsers of Isac_Knowledge\<close>
walther@60023
    78
walther@60255
    79
(* there will be other ways in Isabelle/PIDE * )
wneuper@59472
    80
setup \<open>
neuper@55425
    81
KEStore_Elems.add_thes
walther@60253
    82
  [Thy_Hierarchy.make_thy @{theory}
neuper@55425
    83
    ["Walther Neuper 2005 supported by a grant from NMI Austria"],
walther@60253
    84
  Thy_Hierarchy.make_isa @{theory} ("IsacKnowledge", "Theorems")
neuper@55425
    85
    ["Walther Neuper 2005 supported by a grant from NMI Austria"],
walther@60253
    86
  Thy_Hierarchy.make_thm @{theory}  "IsacKnowledge" ("Belastung_Querkraft", @{thm Belastung_Querkraft})
neuper@55425
    87
	  ["Walther Neuper 2005 supported by a grant from NMI Austria"],
walther@60253
    88
  Thy_Hierarchy.make_thm @{theory}  "IsacKnowledge" ("Moment_Neigung", @{thm Moment_Neigung})
neuper@55425
    89
	  ["Walther Neuper 2005 supported by a grant from NMI Austria"],
walther@60253
    90
  Thy_Hierarchy.make_thm @{theory}  "IsacKnowledge" ("Moment_Querkraft", @{thm Moment_Querkraft})
neuper@55425
    91
	  ["Walther Neuper 2005 supported by a grant from NMI Austria"],
walther@60253
    92
  Thy_Hierarchy.make_thm @{theory}  "IsacKnowledge" ("Neigung_Moment", @{thm Neigung_Moment})
neuper@55425
    93
	  ["Walther Neuper 2005 supported by a grant from NMI Austria"],
walther@60253
    94
  Thy_Hierarchy.make_thm @{theory}  "IsacKnowledge" ("Querkraft_Belastung", @{thm Querkraft_Belastung})
neuper@55425
    95
	  ["Walther Neuper 2005 supported by a grant from NMI Austria"],
walther@60253
    96
  Thy_Hierarchy.make_thm @{theory}  "IsacKnowledge" ("Querkraft_Moment", @{thm Querkraft_Moment})
neuper@55425
    97
	  ["Walther Neuper 2005 supported by a grant from NMI Austria"],
walther@60253
    98
  Thy_Hierarchy.make_thm @{theory}  "IsacKnowledge" ("make_fun_explicit", @{thm make_fun_explicit})
neuper@55425
    99
	  ["Walther Neuper 2005 supported by a grant from NMI Austria"]]
wneuper@59472
   100
\<close>
walther@60255
   101
( **)
neuper@37954
   102
walther@60023
   103
section \<open>Problems\<close>
walther@60023
   104
wenzelm@60306
   105
problem pbl_bieg : "Biegelinien" =
wenzelm@60306
   106
  \<open>Rule_Set.append_rules "empty" Rule_Set.empty []\<close>
wenzelm@60306
   107
  Method: "IntegrierenUndKonstanteBestimmen2"
wenzelm@60306
   108
  Given: "Traegerlaenge l_l" "Streckenlast q_q"
wenzelm@60306
   109
  (* Where: "0 < l_l" ...wait for &lt; and handling Arbfix*)
wenzelm@60306
   110
  Find: "Biegelinie b_b"
wenzelm@60306
   111
  Relate: "Randbedingungen r_b"
wenzelm@60306
   112
wenzelm@60306
   113
problem pbl_bieg_mom : "MomentBestimmte/Biegelinien" =
wenzelm@60306
   114
  \<open>Rule_Set.append_rules "empty" Rule_Set.empty []\<close>
wenzelm@60306
   115
  Method: "IntegrierenUndKonstanteBestimmen"
wenzelm@60306
   116
  Given: "Traegerlaenge l_l" "Streckenlast q_q"
wenzelm@60306
   117
  (* Where: "0 < l_l" ...wait for &lt; and handling Arbfix*)
wenzelm@60306
   118
  Find: "Biegelinie b_b"
wenzelm@60306
   119
  Relate: "RandbedingungenBiegung r_b" "RandbedingungenMoment r_m"
wenzelm@60306
   120
wenzelm@60306
   121
problem pbl_bieg_momg : "MomentGegebene/Biegelinien" =
wenzelm@60306
   122
  \<open>Rule_Set.append_rules "empty" Rule_Set.empty []\<close>
wenzelm@60306
   123
  Method: "IntegrierenUndKonstanteBestimmen/2xIntegrieren"
wenzelm@60306
   124
wenzelm@60306
   125
problem pbl_bieg_einf : "einfache/Biegelinien" =
wenzelm@60306
   126
  \<open>Rule_Set.append_rules "empty" Rule_Set.empty []\<close>
wenzelm@60306
   127
  Method: "IntegrierenUndKonstanteBestimmen/4x4System"
wenzelm@60306
   128
wenzelm@60306
   129
problem pbl_bieg_momquer : "QuerkraftUndMomentBestimmte/Biegelinien" =
wenzelm@60306
   130
  \<open>Rule_Set.append_rules "empty" Rule_Set.empty []\<close>
wenzelm@60306
   131
  Method: "IntegrierenUndKonstanteBestimmen/1xIntegrieren"
wenzelm@60306
   132
wenzelm@60306
   133
problem pbl_bieg_vonq : "vonBelastungZu/Biegelinien" =
wenzelm@60306
   134
  \<open>Rule_Set.append_rules "empty" Rule_Set.empty []\<close>
wenzelm@60306
   135
  Method: "Biegelinien/ausBelastung"
wenzelm@60306
   136
  Given: "Streckenlast q_q" "FunktionsVariable v_v"
wenzelm@60306
   137
  Find: "Funktionen funs'''"
wenzelm@60306
   138
wenzelm@60306
   139
problem pbl_bieg_randbed : "setzeRandbedingungen/Biegelinien" =
wenzelm@60306
   140
  \<open>Rule_Set.append_rules "empty" Rule_Set.empty []\<close>
wenzelm@60306
   141
  Method: "Biegelinien/setzeRandbedingungenEin"
wenzelm@60306
   142
  Given: "Funktionen fun_s" "Randbedingungen r_b"
wenzelm@60306
   143
  Find: "Gleichungen equs'''"
wenzelm@60306
   144
wenzelm@60306
   145
problem pbl_equ_fromfun : "makeFunctionTo/equation" =
wenzelm@60306
   146
  \<open>Rule_Set.append_rules "empty" Rule_Set.empty []\<close>
wenzelm@60306
   147
  Method: "Equation/fromFunction"
wenzelm@60306
   148
  Given: "functionEq fu_n" "substitution su_b"
wenzelm@60306
   149
  Find: "equality equ'''"
wenzelm@60306
   150
wneuper@59472
   151
ML \<open>
neuper@37954
   152
(** methods **)
neuper@37954
   153
walther@60358
   154
val srls = Rule_Def.Repeat {
walther@60358
   155
  id="srls_IntegrierenUnd..", preconds = [], rew_ord = ("termlessI",termlessI), 
walther@60358
   156
	erls = Rule_Set.append_rules "erls_in_srls_IntegrierenUnd.." Rule_Set.empty [
walther@60358
   157
    (*for asm in NTH_CONS ...*)
walther@60358
   158
	  \<^rule_eval>\<open>less\<close> (Prog_Expr.eval_equ "#less_"),
walther@60358
   159
	  (*2nd NTH_CONS pushes n+-1 into asms*)
walther@60358
   160
	  \<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_")], 
walther@60358
   161
	srls = Rule_Set.Empty, calc = [], errpatts = [],
walther@60358
   162
	rules = [
walther@60358
   163
     \<^rule_thm>\<open>NTH_CONS\<close>,
walther@60358
   164
		 \<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_"),
walther@60358
   165
		 \<^rule_thm>\<open>NTH_NIL\<close>,
walther@60358
   166
		 \<^rule_eval>\<open>Prog_Expr.lhs\<close> (Prog_Expr.eval_lhs"eval_lhs_"),
walther@60358
   167
		 \<^rule_eval>\<open>Prog_Expr.rhs\<close> (Prog_Expr.eval_rhs"eval_rhs_"),
walther@60358
   168
		 \<^rule_eval>\<open>Prog_Expr.argument_in\<close> (Prog_Expr.eval_argument_in "Prog_Expr.argument_in")],
walther@60358
   169
	scr = Rule.Empty_Prog};
neuper@37954
   170
    
walther@60358
   171
val srls2 = Rule_Def.Repeat {
walther@60358
   172
  id="srls_IntegrierenUnd..", preconds = [], rew_ord = ("termlessI",termlessI), 
walther@60358
   173
	erls = Rule_Set.append_rules "erls_in_srls_IntegrierenUnd.." Rule_Set.empty [
walther@60358
   174
    (*for asm in NTH_CONS ...*)
walther@60358
   175
		\<^rule_eval>\<open>less\<close> (Prog_Expr.eval_equ "#less_"),
walther@60358
   176
		(*2nd NTH_CONS pushes n+-1 into asms*)
walther@60358
   177
		\<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_")], 
walther@60358
   178
	srls = Rule_Set.Empty, calc = [], errpatts = [],
walther@60358
   179
	rules = [
walther@60358
   180
    \<^rule_thm>\<open>NTH_CONS\<close>,
walther@60358
   181
	  \<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_"),
walther@60358
   182
	  \<^rule_thm>\<open>NTH_NIL\<close>,
walther@60358
   183
	  \<^rule_eval>\<open>Prog_Expr.lhs\<close> (Prog_Expr.eval_lhs "eval_lhs_"),
walther@60358
   184
	  \<^rule_eval>\<open>Prog_Expr.filter_sameFunId\<close> (Prog_Expr.eval_filter_sameFunId "Prog_Expr.filter_sameFunId"),
walther@60358
   185
	  (*WN070514 just for smltest/../biegelinie.sml ...*)
walther@60358
   186
	  \<^rule_eval>\<open>Prog_Expr.sameFunId\<close> (Prog_Expr.eval_sameFunId "Prog_Expr.sameFunId"),
walther@60358
   187
	  \<^rule_thm>\<open>filter_Cons\<close>,
walther@60358
   188
	  \<^rule_thm>\<open>filter_Nil\<close>,
walther@60358
   189
	  \<^rule_thm>\<open>if_True\<close>,
walther@60358
   190
	  \<^rule_thm>\<open>if_False\<close>,
walther@60358
   191
	  \<^rule_thm>\<open>hd_thm\<close>],
walther@60358
   192
	scr = Rule.Empty_Prog};
wneuper@59472
   193
\<close>
neuper@37999
   194
wneuper@59429
   195
section \<open>Methods\<close>
wneuper@59506
   196
(* setup parent directory *)
wenzelm@60303
   197
method met_biege : "IntegrierenUndKonstanteBestimmen" =
wenzelm@60303
   198
  \<open>{rew_ord'="tless_true", rls'= Rule_Set.Empty, calc = [], srls = Rule_Set.Empty, prls = Rule_Set.Empty, crls =Rule_Set.Empty,
wenzelm@60303
   199
    errpats = [], nrls = Rule_Set.Empty}\<close>
wneuper@59545
   200
walther@60023
   201
subsection \<open>Survey on Methods\<close>
walther@60023
   202
text \<open>
walther@60023
   203
  Theory "Biegelinie" used by all Subproblems
walther@60023
   204
  v-- the root Problem calling SubProblems according to indentation
walther@60023
   205
walther@60023
   206
  Problem ["Biegelinien"]
walther@60154
   207
  MethodC ["IntegrierenUndKonstanteBestimmen2"]  biegelinie
walther@60023
   208
walther@60023
   209
    Problem ["vonBelastungZu", "Biegelinien"]
walther@60154
   210
    MethodC ["Biegelinien", "ausBelastung"]  belastung_zu_biegelinie
walther@60023
   211
walther@60023
   212
      Problem ["named", "integrate", "function"]
walther@60154
   213
      MethodC ["diff", "integration", "named"]
walther@60023
   214
walther@60023
   215
      -"- 4 times
walther@60023
   216
walther@60023
   217
    Problem ["setzeRandbedingungen", "Biegelinien"]
walther@60154
   218
    MethodC ["Biegelinien", "setzeRandbedingungenEin"]  setzte_randbedingungen
walther@60023
   219
walther@60023
   220
      Problem ["makeFunctionTo", "equation"]
walther@60154
   221
      MethodC ["Equation", "fromFunction"]
walther@60023
   222
walther@60023
   223
      -"- 4 times
walther@60023
   224
walther@60023
   225
    Problem ["LINEAR", "system"]
walther@60154
   226
    MethodC ["no_met"]
walther@60023
   227
             ^^^^^^--- thus automatied refinement to appropriate Problem
walther@60023
   228
\<close>
walther@60023
   229
walther@60023
   230
subsection \<open>Compute the general bending line\<close>
walther@60023
   231
(* Traegerlaenge beam      Biegelinie!TYPE! id_fun                    AbleitungBiegelinie id_der
walther@60023
   232
           Streckenlast load                Randbedingungen side_conds                 Biegelinie \<noteq>!TYPE!
walther@60023
   233
                   FunktionsVariable fun_var             GleichungsVariablen vs                *)
wneuper@59549
   234
partial_function (tailrec) biegelinie ::
wneuper@59549
   235
  "real \<Rightarrow> real \<Rightarrow> real \<Rightarrow> (real \<Rightarrow> real) \<Rightarrow> bool list \<Rightarrow> real list \<Rightarrow> (real \<Rightarrow> real) \<Rightarrow> bool"
wneuper@59504
   236
  where
walther@60023
   237
"biegelinie beam load fun_var id_fun side_conds vs id_der = (
walther@59635
   238
  let
wneuper@59504
   239
    funs = SubProblem (''Biegelinie'', [''vonBelastungZu'', ''Biegelinien''],
walther@60023
   240
      [''Biegelinien'', ''ausBelastung''])
walther@60023
   241
        [REAL load, REAL fun_var, REAL_REAL id_fun, REAL_REAL id_der];
wneuper@59504
   242
    equs = SubProblem (''Biegelinie'', [''setzeRandbedingungen'', ''Biegelinien''],
walther@60023
   243
      [''Biegelinien'', ''setzeRandbedingungenEin'']) [BOOL_LIST funs, BOOL_LIST side_conds];
walther@59635
   244
    cons = SubProblem (''Biegelinie'', [''LINEAR'', ''system''],
walther@59635
   245
      [''no_met'']) [BOOL_LIST equs, REAL_LIST vs];
wneuper@59504
   246
    B = Take (lastI funs);
walther@60023
   247
    B = ((Substitute cons) #> (Rewrite_Set_Inst [(''bdv'', fun_var)] ''make_ratpoly_in'')) B
wneuper@59504
   248
  in B)"
wenzelm@60303
   249
wenzelm@60303
   250
method met_biege_2 : "IntegrierenUndKonstanteBestimmen2" =
wenzelm@60303
   251
  \<open>{rew_ord'="tless_true",
walther@60358
   252
    rls' = Rule_Set.append_rules "erls_IntegrierenUndK.." Rule_Set.empty [
walther@60358
   253
      \<^rule_eval>\<open>Prog_Expr.ident\<close> (Prog_Expr.eval_ident "#ident_"),
walther@60358
   254
      \<^rule_thm>\<open>not_true\<close>,
walther@60358
   255
      \<^rule_thm>\<open>not_false\<close>], 
wenzelm@60303
   256
    calc = [], 
walther@60358
   257
    srls = Rule_Set.append_rules "erls_IntegrierenUndK.." Rule_Set.empty [
walther@60358
   258
      \<^rule_eval>\<open>Prog_Expr.rhs\<close> (Prog_Expr.eval_rhs"eval_rhs_"),
walther@60358
   259
      \<^rule_eval>\<open>Prog_Expr.ident\<close> (Prog_Expr.eval_ident "#ident_"),
walther@60358
   260
      \<^rule_thm>\<open>last_thmI\<close>,
walther@60358
   261
      \<^rule_thm>\<open>if_True\<close>,
walther@60358
   262
      \<^rule_thm>\<open>if_False\<close>],
wenzelm@60303
   263
    prls = Rule_Set.Empty, crls = Atools_erls, errpats = [], nrls = Rule_Set.Empty}\<close>
wenzelm@60303
   264
  Program: biegelinie.simps
wenzelm@60303
   265
  Given: "Traegerlaenge beam" "Streckenlast load"
wenzelm@60303
   266
    "FunktionsVariable fun_var" "GleichungsVariablen vs" "AbleitungBiegelinie id_der"
wenzelm@60303
   267
  (* Where: "0 < beam" ...wait for &lt; and handling Arbfix*)
wenzelm@60303
   268
  Find: "Biegelinie id_fun"
wenzelm@60303
   269
  Relate: "Randbedingungen side_conds"
wenzelm@60303
   270
wenzelm@60303
   271
method met_biege_intconst_2 : "IntegrierenUndKonstanteBestimmen/2xIntegrieren" =
wenzelm@60303
   272
  \<open>{rew_ord'="tless_true", rls'=Rule_Set.Empty, calc = [], srls = Rule_Set.empty, prls=Rule_Set.empty, crls = Atools_erls,
wenzelm@60303
   273
    errpats = [], nrls = Rule_Set.empty}\<close>
wenzelm@60303
   274
wenzelm@60303
   275
method met_biege_intconst_4 : "IntegrierenUndKonstanteBestimmen/4x4System" =
wenzelm@60303
   276
  \<open>{rew_ord'="tless_true", rls'=Rule_Set.Empty, calc = [], srls = Rule_Set.empty, prls=Rule_Set.empty, crls = Atools_erls,
wenzelm@60303
   277
    errpats = [], nrls = Rule_Set.empty}\<close>
wenzelm@60303
   278
wenzelm@60303
   279
method met_biege_intconst_1 : "IntegrierenUndKonstanteBestimmen/1xIntegrieren" =
wenzelm@60303
   280
  \<open>{rew_ord'="tless_true", rls'=Rule_Set.Empty, calc = [], srls = Rule_Set.empty, prls=Rule_Set.empty, crls = Atools_erls,
wenzelm@60303
   281
    errpats = [], nrls = Rule_Set.empty}\<close>
wenzelm@60303
   282
wenzelm@60303
   283
method met_biege2 : "Biegelinien" =
wenzelm@60303
   284
  \<open>{rew_ord'="tless_true", rls'=Rule_Set.Empty, calc = [], srls = Rule_Set.empty, prls=Rule_Set.empty, crls = Atools_erls,
wenzelm@60303
   285
    errpats = [], nrls = Rule_Set.empty}\<close>
wenzelm@60303
   286
wenzelm@60303
   287
walther@60023
   288
subsection \<open>Sub-problem "integrate and determine constants", nicely modularised\<close>
wneuper@59429
   289
walther@59998
   290
partial_function (tailrec) belastung_zu_biegelinie ::
walther@59998
   291
(* Streckenlast     Biegelinie                       Funktionen
walther@59998
   292
           FunktionsVariable         AbleitungBiegelinie       *)
walther@59998
   293
  "real \<Rightarrow> real \<Rightarrow> (real \<Rightarrow> real) \<Rightarrow> (real \<Rightarrow> real) \<Rightarrow> bool list"
wneuper@59504
   294
  where
walther@60023
   295
"belastung_zu_biegelinie q__q v_v id_fun id_der = (
walther@59635
   296
  let
walther@59635
   297
    q___q = Take (qq v_v = q__q);
walther@59635
   298
    q___q = (
walther@59637
   299
      (Rewrite ''sym_neg_equal_iff_equal'') #>
walther@59635
   300
      (Rewrite ''Belastung_Querkraft'')) q___q;
walther@59635
   301
    Q__Q = SubProblem (''Biegelinie'', [''named'', ''integrate'', ''function''],
walther@59635
   302
      [''diff'', ''integration'', ''named'']) [REAL (rhs q___q), REAL v_v, REAL_REAL Q];
walther@59635
   303
    M__M = Rewrite ''Querkraft_Moment'' Q__Q;
walther@59635
   304
    M__M = SubProblem (''Biegelinie'', [''named'', ''integrate'', ''function''],
walther@59635
   305
      [''diff'', ''integration'', ''named'']) [REAL (rhs M__M), REAL v_v, REAL_REAL M_b];
walther@59635
   306
    N__N = (
walther@59637
   307
      (Rewrite ''Moment_Neigung'' ) #> (Rewrite ''make_fun_explicit'' )) M__M;
walther@59635
   308
    N__N = SubProblem (''Biegelinie'', [''named'', ''integrate'', ''function''],
walther@60023
   309
      [''diff'', ''integration'', ''named'']) [REAL (rhs N__N), REAL v_v, REAL_REAL id_der];
walther@59635
   310
    B__B = SubProblem (''Biegelinie'', [''named'', ''integrate'', ''function''],
walther@59635
   311
      [''diff'', ''integration'', ''named'']) [REAL (rhs N__N), REAL v_v, REAL_REAL id_fun]
walther@59635
   312
  in
walther@59998
   313
    [Q__Q, M__M, N__N, B__B])"  (*..Q is Const Querkraft    -------------------------^ *)
wenzelm@60303
   314
wenzelm@60303
   315
method met_biege_ausbelast : "Biegelinien/ausBelastung" =
wenzelm@60303
   316
  \<open>{rew_ord'="tless_true", 
walther@60358
   317
    rls' = Rule_Set.append_rules "erls_ausBelastung" Rule_Set.empty [
walther@60358
   318
      \<^rule_eval>\<open>Prog_Expr.ident\<close> (Prog_Expr.eval_ident "#ident_"),
walther@60358
   319
      \<^rule_thm>\<open>not_true\<close>,
walther@60358
   320
      \<^rule_thm>\<open>not_false\<close>],
wenzelm@60303
   321
    calc = [], 
walther@60358
   322
    srls = Rule_Set.append_rules "srls_ausBelastung" Rule_Set.empty [
walther@60358
   323
      \<^rule_eval>\<open>Prog_Expr.rhs\<close> (Prog_Expr.eval_rhs "eval_rhs_")],
wenzelm@60303
   324
    prls = Rule_Set.empty, crls = Atools_erls, errpats = [], nrls = Rule_Set.empty}\<close>
wenzelm@60303
   325
  Program: belastung_zu_biegelinie.simps
wenzelm@60303
   326
  Given: "Streckenlast q__q" "FunktionsVariable v_v" "Biegelinie id_fun" "AbleitungBiegelinie id_der"
wenzelm@60303
   327
  Find: "Funktionen fun_s"
wenzelm@60303
   328
wneuper@59429
   329
subsection \<open>Substitute the constraints into the equations\<close>
wneuper@59429
   330
wneuper@59504
   331
partial_function (tailrec) setzte_randbedingungen :: "bool list \<Rightarrow> bool list \<Rightarrow> bool list"
wneuper@59504
   332
  where 
walther@59635
   333
"setzte_randbedingungen fun_s r_b = (
walther@59635
   334
  let
walther@59635
   335
    b_1 = NTH 1 r_b;
walther@59635
   336
    f_s = filter_sameFunId (lhs b_1) fun_s;
walther@59635
   337
    e_1 = SubProblem (''Biegelinie'', [''makeFunctionTo'', ''equation''],
walther@59635
   338
            [''Equation'', ''fromFunction'']) [BOOL (hd f_s), BOOL b_1];
walther@59635
   339
    b_2 = NTH 2 r_b;
walther@59635
   340
    f_s = filter_sameFunId (lhs b_2) fun_s;
walther@59635
   341
    e_2 = SubProblem (''Biegelinie'', [''makeFunctionTo'', ''equation''],
walther@59635
   342
             [''Equation'', ''fromFunction'']) [BOOL (hd f_s), BOOL b_2];
walther@59635
   343
    b_3 = NTH 3 r_b;
walther@59635
   344
    f_s = filter_sameFunId (lhs b_3) fun_s;
walther@59635
   345
    e_3 = SubProblem (''Biegelinie'', [''makeFunctionTo'', ''equation''],
walther@59635
   346
             [''Equation'', ''fromFunction'']) [BOOL (hd f_s), BOOL b_3];
walther@59635
   347
    b_4 = NTH 4 r_b;
walther@59635
   348
    f_s = filter_sameFunId (lhs b_4) fun_s;
walther@59635
   349
    e_4 = SubProblem (''Biegelinie'', [''makeFunctionTo'', ''equation''],
walther@59635
   350
             [''Equation'', ''fromFunction'']) [BOOL (hd f_s), BOOL b_4]
walther@59635
   351
  in
walther@59635
   352
    [e_1, e_2, e_3, e_4])"
wenzelm@60303
   353
wenzelm@60303
   354
method met_biege_setzrand : "Biegelinien/setzeRandbedingungenEin" =
wenzelm@60303
   355
  \<open>{rew_ord'="tless_true", rls'=Rule_Set.Empty, calc = [], srls = srls2, prls=Rule_Set.empty, crls = Atools_erls,
wenzelm@60303
   356
    errpats = [], nrls = Rule_Set.empty}\<close>
wenzelm@60303
   357
  Program: setzte_randbedingungen.simps
wenzelm@60303
   358
  Given: "Funktionen fun_s" "Randbedingungen r_b"
wenzelm@60303
   359
  Find: "Gleichungen equs'''"
wenzelm@60303
   360
wenzelm@60303
   361
wneuper@59429
   362
subsection \<open>Transform an equality into a function\<close>
wneuper@59429
   363
walther@60242
   364
        (*(M_b x = c_2 + c * x + -1 * q_0 / 2 * x \<up> 2) (M_b L = 0) -->
walther@60242
   365
               0 = c_2 + c * L + -1 * q_0 / 2 * L \<up> 2*)
wneuper@59504
   366
partial_function (tailrec) function_to_equality :: "bool \<Rightarrow> bool \<Rightarrow> bool"
wneuper@59504
   367
  where
walther@59635
   368
"function_to_equality fu_n su_b = (
walther@59635
   369
  let
walther@59635
   370
    fu_n = Take fu_n;
walther@59635
   371
    bd_v = argument_in (lhs fu_n);
walther@59635
   372
    va_l = argument_in (lhs su_b);
walther@60242
   373
    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>
walther@59635
   374
    eq_u = Substitute [su_b] eq_u
walther@59635
   375
  in
walther@59635
   376
    (Rewrite_Set ''norm_Rational'') eq_u)"
wenzelm@60303
   377
wenzelm@60303
   378
method met_equ_fromfun : "Equation/fromFunction" =
wenzelm@60303
   379
  \<open>{rew_ord'="tless_true", rls'=Rule_Set.Empty, calc = [],
walther@60358
   380
    srls = Rule_Set.append_rules "srls_in_EquationfromFunc" Rule_Set.empty [
walther@60358
   381
      \<^rule_eval>\<open>Prog_Expr.lhs\<close> (Prog_Expr.eval_lhs "eval_lhs_"),
walther@60358
   382
      \<^rule_eval>\<open>Prog_Expr.argument_in\<close> (Prog_Expr.eval_argument_in "Prog_Expr.argument_in")],
wenzelm@60303
   383
    prls=Rule_Set.empty, crls = Atools_erls, errpats = [], nrls = Rule_Set.empty}\<close>
wenzelm@60303
   384
  Program: function_to_equality.simps
wenzelm@60303
   385
  (*(M_b x = c_2 + c * x + -1 * q_0 / 2 * x \<up> 2) (M_b L = 0) -->
wenzelm@60303
   386
         0 = c_2 + c * L + -1 * q_0 / 2 * L \<up> 2*)
wenzelm@60303
   387
  Given: "functionEq fu_n" "substitution su_b"
wenzelm@60303
   388
  Find: "equality equ'''"
wenzelm@60303
   389
wneuper@59549
   390
ML \<open>
wneuper@59549
   391
\<close> ML \<open>
walther@60278
   392
\<close> ML \<open>
wneuper@59549
   393
\<close>
neuper@37906
   394
end
neuper@37906
   395