1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/test/Tools/isac/Bridge/ISAC_Test.thy	Sat May 26 11:26:43 2018 +0200
     1.3 @@ -0,0 +1,60 @@
     1.4 +(* Introduce Isabelle/jEdit as Isac front-end.
     1.5 +   Trials due to suggestions by Makarius Wenzel
     1.6 +   Walther Neuper 2018
     1.7 +   (c) due to copyright terms
     1.8 + *)
     1.9 +
    1.10 +theory ISAC_Test
    1.11 +imports Main
    1.12 +
    1.13 +keywords
    1.14 +  "ISAC" :: (* ? correct...*)thy_decl
    1.15 +
    1.16 +begin
    1.17 +ML \<open>
    1.18 +val _ =
    1.19 +  Outer_Syntax.command @{command_keyword ISAC} (* dummy parser *) ""
    1.20 +    (Parse.cartouche >> (fn s =>
    1.21 +      Toplevel.keep (fn _ => writeln s)))
    1.22 +\<close>
    1.23 +
    1.24 +ISAC \<open>1 + 2 = 3\<close>
    1.25 +ISAC \<open>
    1.26 +Problem ("Biegelinie", ["Biegelinien"])
    1.27 +  Specification:
    1.28 +    Model:
    1.29 +      Given: "Traegerlaenge L", "Streckenlast q_0"
    1.30 +      Where: "q_0 ist_integrierbar_auf {| 0, L |}", "0 < L"
    1.31 +      Find: "Biegelinie y"
    1.32 +      Relate: "Randbedingungen [ Q_0 = q_0 * L, M_b L = 0, y_0 = 0, d_d x y_0 = 0 ]"
    1.33 +    References:
    1.34 +      Theory: "Biegelinie"
    1.35 +      Problem: ["Biegelinien"]
    1.36 +      Method: ["Integrieren", "KonstanteBestimmen2"]
    1.37 +  Solution:
    1.38 +    Problem ("Biegelinie", ["vonBelastungZu", "Biegelinien"])
    1.39 +    "[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)]"
    1.40 +    Problem ("Biegelinie", ["setzeRandbedingungen", "Biegelinien"])
    1.41 +    "[L * q_0 = c, 0 = (2 * c_2 + 2 * L * c + -1 * L ^ 2 * q_0) / 2, 0 = c_4,  0 = c_3]"
    1.42 +    "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]"
    1.43 +    "[c = -1 * L * q_0 / -1, c_2 = -1 * L ^ 2 * q_0 / 2, c_3 = 0, c_4 = 0]"
    1.44 +    "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)"
    1.45 +        (*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]"
    1.46 +    "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)"
    1.47 +        (*tactic...*) Rewrite_Set_Inst "[(bdv, x)]" "make_ratpoly_in" "y x"
    1.48 +    "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"
    1.49 +        (*tactic...*) Check_Postcond ["Biegelinien"]
    1.50 +"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"
    1.51 +\<close>
    1.52 +text \<open>
    1.53 +A "Specification" consists exactly of the keywords given in the example
    1.54 +(while the "terms" vary from example to example).
    1.55 +
    1.56 +A "Solution" consists of steps of calculation; each step occupies 1 or 2 lines,
    1.57 +depending whether the respective "tactic" is displayed or not.
    1.58 +
    1.59 +This simple structure gives cause for hope, that specific keywords can be omitted
    1.60 +by some trickery in the front-end.
    1.61 +\<close>
    1.62 +
    1.63 +end
    1.64 \ No newline at end of file