theory Keyword_ISAC

imports Main

keywords "ISAC" :: diag

begin

ML \<open> (* original from Makarius 2018 *)

val _ =

  Outer_Syntax.command @{command_keyword ISAC} "embedded ISAC language"

    (Parse.input Parse.cartouche >> (fn input =>

      Toplevel.keep (fn _ => ignore (ML_Lex.read_source (*true*) input))))

\<close>

ISAC \<open>any content "for" cartouche, 1 + 2 = 3\<close>

ISAC \<open>

Problem ("Biegelinie", ["Biegelinien"])

  Specification:

    Model:

      Given: "Traegerlaenge L", "Streckenlast q_0"

      Where: "q_0 ist_integrierbar_auf {| 0, L |}", "0 < L"

      Find: "Biegelinie y"

      Relate: "Randbedingungen [ Q_0 = q_0 * L, M_b L = 0, y_0 = 0, d_d x y_0 = 0 ]"

    References:

      Theory: "Biegelinie"

      Problem: ["Biegelinien"]

      Method: ["Integrieren", "KonstanteBestimmen2"]

  Solution:

    Problem ("Biegelinie", ["vonBelastungZu", "Biegelinien"])

    "[Q x = c + -1 * q_0 * x, M_b x = c_2 + c * x + -1 * q_0 / 2 * x ^ 2,  y' x =  c_3 + 1 / (-1 * EI) * (c_2 * x + c / 2 * x ^ 2 + -1 * q_0 / 6 * x ^ 3),  y x =  c_4 + c_3 * x +  1 / (-1 * EI) *  (c_2 / 2 * x ^ 2 + c / 6 * x ^ 3 + -1 * q_0 / 24 * x ^ 4)]"

    Problem ("Biegelinie", ["setzeRandbedingungen", "Biegelinien"])

    "[L * q_0 = c, 0 = (2 * c_2 + 2 * L * c + -1 * L ^ 2 * q_0) / 2, 0 = c_4,  0 = c_3]"

    "solveSystem [L * q_0 = c, 0 = (2 * c_2 + 2 * L * c + -1 * L ^ 2 * q_0) / 2, 0 = c_4,  0 = c_3] [c, c_1, c_2, c_4]"

    "[c = -1 * L * q_0 / -1, c_2 = -1 * L ^ 2 * q_0 / 2, c_3 = 0, c_4 = 0]"

    "y x = c_4 + c_3 * x + 1 / (-1 * EI) * (c_2 / 2 * x ^ 2 + c / 6 * x ^ 3 + -1 * q_0 / 24 * x ^ 4)"

      Tactic Substitute "c_4 + c_3 * x +  1 / (-1 * EI) *  (c_2 / 2 * x ^ 2 + c / 6 * x ^ 3 + -1 * q_0 / 24 * x ^ 4)" "[c, c_1, c_2, c_4]"

    "y x = 0 + 0 * x + 1 / (-1 * EI) * (-1 * L ^ 2 * q_0 / 2 / 2 * x ^ 2 + -1 * L * q_0 / -1 / 6 * x ^ 3 +  -1 * q_0 / 24 * x ^ 4)"

      Tactic Rewrite_Set_Inst "[(bdv, x)]" "make_ratpoly_in" "y x"

    "y x = -6 * q_0 * L ^ 2 / (-24 * EI) * x ^ 2 + 4 * L * q_0 / (-24 * EI) * x ^ 3 + -1 * q_0 / (-24 * EI) * x ^ 4"

      Tactic Check_Postcond ["Biegelinien"]

"y x = -6 * q_0 * L ^ 2 / (-24 * EI) * x ^ 2 + 4 * L * q_0 / (-24 * EI) * x ^ 3 + -1 * q_0 / (-24 * EI) * x ^ 4"

\<close>

ML \<open>

\<close> ML \<open>

\<close> ML \<open>

\<close>

end