1.1 --- a/test/Tools/isac/Knowledge/biegelinie-2.sml Sat Sep 14 16:15:05 2019 +0200
1.2 +++ b/test/Tools/isac/Knowledge/biegelinie-2.sml Mon Sep 16 12:43:43 2019 +0200
1.3 @@ -1,19 +1,102 @@
1.4 -(* Isabelle2015->17: divided into 2 files, because if
1.5 - in 1 file: exception Size raised (line 182 of "./basis/LibrarySupport.sml")
1.6 - author: Walther Neuper 180214
1.7 +(* "Knowledge/biegelinie-3.sml"
1.8 + author: Walther Neuper 190515
1.9 (c) due to copyright terms
1.10 *)
1.11 -"table of contents -----------------------------------------------";(* NOT in Test_Isac.thy *)
1.12 +"table of contents -----------------------------------------------";
1.13 "-----------------------------------------------------------------";
1.14 -"----------- see biegelinie-1.sml---------------------------------";
1.15 -"----------- method [Biegelinien,setzeRandbedingungenEin] + exec -";
1.16 -"----------- shift next exp up: exception Size raised ------------";
1.17 -"----------- IntegrierenUndKonstanteBestimmen2: Bsp.7.70. --------";(* --> biegelinie-3.sml *)
1.18 +"----------- SubProblem (_,[vonBelastungZu,Biegelinien] ----------";
1.19 +"da----------- method [Biegelinien,setzeRandbedingungenEin] + exec -";
1.20 +"da-incompl--- IntegrierenUndKonstanteBestimmen2: Bsp.7.70. --------";(* --> biegelinie-3.sml *)
1.21 "----------- investigate normalforms in biegelinien --------------";
1.22 "-----------------------------------------------------------------";
1.23 "-----------------------------------------------------------------";
1.24 "-----------------------------------------------------------------";
1.25
1.26 +"----------- SubProblem (_,[vonBelastungZu,Biegelinien] ----------";
1.27 +"----------- SubProblem (_,[vonBelastungZu,Biegelinien] ----------";
1.28 +"----------- SubProblem (_,[vonBelastungZu,Biegelinien] ----------";
1.29 +val fmz =
1.30 + ["Streckenlast q_0","FunktionsVariable x",
1.31 + "Funktionen [Q x = c + -1 * q_0 * x, \
1.32 + \M_b x = c_2 + c * x + -1 * q_0 / 2 * x ^^^ 2,\
1.33 + \ y' x = c_3 + 1 / (-1 * EI) * (c_2 * x + c / 2 * x ^^^ 2 + -1 * q_0 / 6 * x ^^^ 3),\
1.34 + \ 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.35 + "AbleitungBiegelinie dy"];
1.36 +val (dI',pI',mI') = ("Biegelinie", ["vonBelastungZu","Biegelinien"],
1.37 + ["Biegelinien","ausBelastung"]);
1.38 +val p = e_pos'; val c = [];
1.39 +val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
1.40 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.41 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.42 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.43 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.44 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.45 +case nxt of ("Apply_Method", Apply_Method ["Biegelinien", "ausBelastung"]) => ()
1.46 +| _ => error "biegelinie.sml met2 b";
1.47 +
1.48 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f = "q_ x = q_0";
1.49 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f = "- q_ x = - q_0";
1.50 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f = "Q' x = - q_0";
1.51 +case nxt of (_, Subproblem (_, ["named", "integrate", "function"])) => ()
1.52 +| _ => error "biegelinie.sml met2 c";
1.53 +
1.54 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.55 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.56 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.57 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.58 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.59 +
1.60 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f = "Q x = c + -1 * q_0 * x";
1.61 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f = "Q x = c + -1 * q_0 * x";
1.62 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f = "M_b' x = c + -1 * q_0 * x";
1.63 +case nxt of (_,Subproblem (_, ["named", "integrate", "function"])) => ()
1.64 +| _ => error "biegelinie.sml met2 d";
1.65 +
1.66 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.67 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.68 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.69 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.70 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f =
1.71 + "M_b x = Integral c + -1 * q_0 * x D x";
1.72 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f =
1.73 + "M_b x = c_2 + c * x + -1 * q_0 / 2 * x ^^^ 2";
1.74 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f =
1.75 + "M_b x = c_2 + c * x + -1 * q_0 / 2 * x ^^^ 2";
1.76 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f =
1.77 + "- EI * y'' x = c_2 + c * x + -1 * q_0 / 2 * x ^^^ 2";
1.78 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f =
1.79 + "y'' x = 1 / - EI * (c_2 + c * x + -1 * q_0 / 2 * x ^^^ 2)";
1.80 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.81 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.82 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.83 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.84 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f =
1.85 + "y' x = Integral 1 / - EI * (c_2 + c * x + -1 * q_0 / 2 * x ^^^ 2) D x";
1.86 +(*------vvv---- exception Size raised (line 169 of "./basis/LibrarySupport.sml")-------------*)
1.87 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f =
1.88 +"y' x = Integral 1 / (-1 * EI) * (c_2 + c * x + -1 * q_0 / 2 * x ^^^ 2) D x";
1.89 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f =
1.90 +"y' x =\nc_3 + 1 / (-1 * EI) * (c_2 * x + c / 2 * x ^^^ 2 + -1 * q_0 / 6 * x ^^^ 3)";
1.91 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f =
1.92 +"y' x =\nc_3 + 1 / (-1 * EI) * (c_2 * x + c / 2 * x ^^^ 2 + -1 * q_0 / 6 * x ^^^ 3)";
1.93 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.94 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.95 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.96 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.97 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f =
1.98 +"y x =\nIntegral c_3 +\n 1 / (-1 * EI) *\n (c_2 * x + c / 2 * x ^^^ 2 + -1 * q_0 / 6 * x ^^^ 3) D x";
1.99 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f =
1.100 +"y x =\nc_4 + c_3 * x +\n1 / (-1 * EI) *\n(c_2 / 2 * x ^^^ 2 + c / 6 * x ^^^ 3 + -1 * q_0 / 24 * x ^^^ 4)";
1.101 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f =
1.102 + "y x =\nc_4 + c_3 * x +\n1 / (-1 * EI) *\n(c_2 / 2 * x ^^^ 2 + c / 6 * x ^^^ 3 + -1 * q_0 / 24 * x ^^^ 4)";
1.103 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.104 +if f2str f =
1.105 + "[Q x = c + -1 * q_0 * x, M_b x = c_2 + c * x + -1 * q_0 / 2 * x ^^^ 2,\n dy x =\n c_3 + 1 / (-1 * EI) * (c_2 * x + c / 2 * x ^^^ 2 + -1 * q_0 / 6 * x ^^^ 3),\n y x =\n c_4 + c_3 * x +\n 1 / (-1 * EI) *\n (c_2 / 2 * x ^^^ 2 + c / 6 * x ^^^ 3 + -1 * q_0 / 24 * x ^^^ 4)]"
1.106 +then case nxt of ("End_Proof'", End_Proof') => ()
1.107 + | _ => error "biegelinie.sml met2 e 1"
1.108 +else error "biegelinie.sml met2 e 2";
1.109 +(*-----^^^----- exception Size raised (line 169 of "./basis/LibrarySupport.sml")-------------*)
1.110 +
1.111 "----------- method [Biegelinien,setzeRandbedingungenEin] + exec -";
1.112 "----------- method [Biegelinien,setzeRandbedingungenEin] + exec -";
1.113 "----------- method [Biegelinien,setzeRandbedingungenEin] + exec -";
1.114 @@ -245,21 +328,10 @@
1.115 if p = ([3, 8, 1], Res) then () else error "Bsp.7.70 ok: p = ([3, 8, 1], Res)";
1.116 (*... no progress leads to: exception Size raised (line 182 of "./basis/LibrarySupport.sml")
1.117
1.118 -^^^^^^^^^^^^^^^ no progress already in isabisac15, but not noticed ^^^^^^^^^^^^^^^
1.119 +^^^^^^^^^^^^^^^ no progress already in isabisac15, but not noticed in time ^^^^^^^^^^^^^^^
1.120
1.121 On correction don't forget to reactivate --- test parallel calls to autoCalculate ---,
1.122 which uses this example.*)
1.123
1.124 -"----------- investigate normalforms in biegelinien --------------";
1.125 -"----------- investigate normalforms in biegelinien --------------";
1.126 -"----------- investigate normalforms in biegelinien --------------";
1.127 -"----- coming from integration:";
1.128 -val Q = str2term "Q x = c + -1 * q_0 * x";
1.129 -val M_b = str2term "M_b x = c_2 + c * x + -1 * q_0 / 2 * x ^^^ 2";
1.130 -val y' = str2term "y' x = c_3 + 1 / (-1 * EI) * (c_2 * x + c / 2 * x ^^^ 2 + -1 * q_0 / 6 * x ^^^ 3)";
1.131 -val y = str2term "y x = c_4 + c_3 * x +\n1 / (-1 * EI) * (c_2 / 2 * x ^^^ 2 + c / 6 * x ^^^ 3 + -1 * q_0 / 24 * x ^^^ 4)";
1.132 -(*^^^ 1 / (-1 * EI) NOT distributed - ok! ^^^^^^^^^^^^^^^^^^^^^^^*)
1.133
1.134 -"----- functions comming from:";
1.135
1.136 -