(* Introduce Isabelle/jEdit as Isac front-end.

   Trials due to suggestions by Makarius Wenzel

   Walther Neuper 2018

   (c) due to copyright terms

 *)

theory ISAC_Test

imports Main

keywords

  "ISAC" :: (* ? correct...*)thy_decl

begin

ML \<open>

val _ =

  Outer_Syntax.command @{command_keyword ISAC} (* dummy parser *) ""

    (Parse.cartouche >> (fn s =>

      Toplevel.keep (fn _ => writeln s)))

\<close>

ISAC \<open>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>

text \<open>

A "Specification" consists exactly of the keywords given in the example

(while the "terms" vary from example to example).

A "Solution" consists of steps of calculation; each step occupies 1 or 2 lines,

depending whether the respective "tactic" is displayed or not.

This simple structure gives cause for hope, that specific keywords can be omitted

by some trickery in the front-end.

\<close>

end