|
wneuper@3737
|
1 |
(* tests on biegelinie
|
|
wneuper@3737
|
2 |
author: Walther Neuper 050826
|
|
wneuper@3737
|
3 |
(c) due to copyright terms
|
|
wneuper@3737
|
4 |
|
|
wneuper@3737
|
5 |
use"../smltest/IsacKnowledge/biegelinie.sml";
|
|
wneuper@3737
|
6 |
use"biegelinie.sml";
|
|
wneuper@3737
|
7 |
*)
|
|
wneuper@3737
|
8 |
val thy = Biegelinie.thy;
|
|
wneuper@3737
|
9 |
|
|
wneuper@3737
|
10 |
"-----------------------------------------------------------------";
|
|
wneuper@3737
|
11 |
"table of contents -----------------------------------------------";
|
|
wneuper@3737
|
12 |
"-----------------------------------------------------------------";
|
|
wneuper@3737
|
13 |
"----------- the rules -------------------------------------------";
|
|
wneuper@3737
|
14 |
"----------- Script [IntegrierenUndKonstanteBestimmen] -----------";
|
|
wneuper@3737
|
15 |
"----------- IntegrierenUndKonstanteBestimmen by rewriting -------";
|
|
wneuper@3737
|
16 |
"----------- simplify_leaf for this script -----------------------";
|
|
wneuper@3737
|
17 |
"----------- Bsp 7.27 me -----------------------------------------";
|
|
wneuper@3737
|
18 |
"----------- Bsp 7.27 autoCalculate ------------------------------";
|
|
wneuper@3737
|
19 |
"----------- SubProblem (_,[vonBelastungZu,Biegelinien] ----------";
|
|
wneuper@3737
|
20 |
"----------- SubProblem (_,[setzeRandbedingungen,Biegelinien] ----";
|
|
wneuper@3737
|
21 |
"----------- method [Biegelinien,setzeRandbedingungenEin] + exec -";
|
|
wneuper@3879
|
22 |
"----------- method [Biegelinien,setzeRandbedingungenEin]FAST ----";
|
|
wneuper@3879
|
23 |
"----------- IntegrierenUndKonstanteBestimmen2: Bsp.7.70. --------";
|
|
wneuper@3737
|
24 |
"----------- investigate normalforms in biegelinien --------------";
|
|
wneuper@3737
|
25 |
"-----------------------------------------------------------------";
|
|
wneuper@3737
|
26 |
"-----------------------------------------------------------------";
|
|
wneuper@3737
|
27 |
"-----------------------------------------------------------------";
|
|
wneuper@3737
|
28 |
|
|
wneuper@3737
|
29 |
|
|
wneuper@3737
|
30 |
"----------- the rules -------------------------------------------";
|
|
wneuper@3737
|
31 |
"----------- the rules -------------------------------------------";
|
|
wneuper@3737
|
32 |
"----------- the rules -------------------------------------------";
|
|
wneuper@3737
|
33 |
fun str2t str = (term_of o the o (parse Biegelinie.thy)) str;
|
|
wneuper@3737
|
34 |
fun term2s t = Sign.string_of_term (sign_of Biegelinie.thy) t;
|
|
wneuper@3737
|
35 |
fun rewrit thm str =
|
|
wneuper@3737
|
36 |
fst (the (rewrite_ Biegelinie.thy tless_true e_rls true thm str));
|
|
wneuper@3737
|
37 |
|
|
wneuper@3852
|
38 |
val t = rewrit Belastung_Querkraft (str2t "- q_ x = - q_0"); term2s t;
|
|
wneuper@3737
|
39 |
if term2s t = "Q' x = - q_0" then ()
|
|
wneuper@3737
|
40 |
else raise error "/biegelinie.sml: Belastung_Querkraft";
|
|
wneuper@3737
|
41 |
|
|
wneuper@3737
|
42 |
val t = rewrit Querkraft_Moment (str2t "Q x = - q_0 * x + c"); term2s t;
|
|
wneuper@3737
|
43 |
if term2s t = "M_b' x = - q_0 * x + c" then ()
|
|
wneuper@3737
|
44 |
else raise error "/biegelinie.sml: Querkraft_Moment";
|
|
wneuper@3737
|
45 |
|
|
wneuper@3737
|
46 |
val t = rewrit Moment_Neigung (str2t "M_b x = -q_0 * x^^^2/2 + q_0/2 *L*x");
|
|
wneuper@3737
|
47 |
term2s t;
|
|
wneuper@3737
|
48 |
if term2s t = "- EI * y'' x = - q_0 * x ^^^ 2 / 2 + q_0 / 2 * L * x" then ()
|
|
wneuper@3737
|
49 |
else raise error "biegelinie.sml: Moment_Neigung";
|
|
wneuper@3737
|
50 |
|
|
wneuper@3737
|
51 |
|
|
wneuper@3737
|
52 |
"----------- Script [IntegrierenUndKonstanteBestimmen] -----------";
|
|
wneuper@3737
|
53 |
"----------- Script [IntegrierenUndKonstanteBestimmen] -----------";
|
|
wneuper@3737
|
54 |
"----------- Script [IntegrierenUndKonstanteBestimmen] -----------";
|
|
wneuper@3737
|
55 |
val str =
|
|
wneuper@3737
|
56 |
"Script BiegelinieScript \
|
|
wneuper@3849
|
57 |
\(l_::real) (q__::real) (v_::real) (b_::real=>real) \
|
|
wneuper@3737
|
58 |
\(rb_::bool list) (rm_::bool list) = \
|
|
wneuper@3852
|
59 |
\ (let q___ = Take (q_ v_ = q__); \
|
|
wneuper@3849
|
60 |
\ q___ = ((Rewrite sym_real_minus_eq_cancel True) @@ \
|
|
wneuper@3849
|
61 |
\ (Rewrite Belastung_Querkraft True)) q___; \
|
|
wneuper@3737
|
62 |
\ (Q__:: bool) = \
|
|
wneuper@3737
|
63 |
\ (SubProblem (Biegelinie_,[named,integrate,function], \
|
|
wneuper@3789
|
64 |
\ [diff,integration,named]) \
|
|
wneuper@3849
|
65 |
\ [real_ (rhs q___), real_ v_, real_real_ Q]); \
|
|
wneuper@3737
|
66 |
\ Q__ = Rewrite Querkraft_Moment True Q__; \
|
|
wneuper@3737
|
67 |
\ (M__::bool) = \
|
|
wneuper@3737
|
68 |
\ (SubProblem (Biegelinie_,[named,integrate,function], \
|
|
wneuper@3789
|
69 |
\ [diff,integration,named]) \
|
|
wneuper@3737
|
70 |
\ [real_ (rhs Q__), real_ v_, real_real_ M_b]); \
|
|
wneuper@3737
|
71 |
\ e1__ = nth_ 1 rm_; \
|
|
wneuper@3737
|
72 |
\ (x1__::real) = argument_in (lhs e1__); \
|
|
wneuper@3737
|
73 |
\ (M1__::bool) = (Substitute [v_ = x1__]) M__; \
|
|
wneuper@3737
|
74 |
\ M1__ = (Substitute [e1__]) M1__ ; \
|
|
wneuper@3737
|
75 |
\ M2__ = Take M__; "^
|
|
wneuper@3737
|
76 |
(*without this Take 'Substitute [v_ = x2__]' takes _last formula from ctree_*)
|
|
wneuper@3737
|
77 |
" e2__ = nth_ 2 rm_; \
|
|
wneuper@3737
|
78 |
\ (x2__::real) = argument_in (lhs e2__); \
|
|
wneuper@3737
|
79 |
\ (M2__::bool) = ((Substitute [v_ = x2__]) @@ \
|
|
wneuper@3737
|
80 |
\ (Substitute [e2__])) M2__; \
|
|
wneuper@3737
|
81 |
\ (c_1_2__::bool list) = \
|
|
wneuper@3737
|
82 |
\ (SubProblem (Biegelinie_,[linear,system],[no_met]) \
|
|
wneuper@3737
|
83 |
\ [booll_ [M1__, M2__], reall [c,c_2]]); \
|
|
wneuper@3737
|
84 |
\ M__ = Take M__; \
|
|
wneuper@3737
|
85 |
\ M__ = ((Substitute c_1_2__) @@ \
|
|
wneuper@3737
|
86 |
\ (Try (Rewrite_Set_Inst [(bdv_1, c),(bdv_2, c_2)]\
|
|
wneuper@3737
|
87 |
\ simplify_System False)) @@ \
|
|
wneuper@3737
|
88 |
\ (Rewrite Moment_Neigung False) @@ \
|
|
wneuper@3737
|
89 |
\ (Rewrite make_fun_explicit False)) M__; "^
|
|
wneuper@3737
|
90 |
(*----------------------- and the same once more ------------------------*)
|
|
wneuper@3737
|
91 |
" (N__:: bool) = \
|
|
wneuper@3737
|
92 |
\ (SubProblem (Biegelinie_,[named,integrate,function], \
|
|
wneuper@3789
|
93 |
\ [diff,integration,named]) \
|
|
wneuper@3737
|
94 |
\ [real_ (rhs M__), real_ v_, real_real_ y']); \
|
|
wneuper@3737
|
95 |
\ (B__:: bool) = \
|
|
wneuper@3737
|
96 |
\ (SubProblem (Biegelinie_,[named,integrate,function], \
|
|
wneuper@3789
|
97 |
\ [diff,integration,named]) \
|
|
wneuper@3737
|
98 |
\ [real_ (rhs N__), real_ v_, real_real_ y]); \
|
|
wneuper@3737
|
99 |
\ e1__ = nth_ 1 rb_; \
|
|
wneuper@3737
|
100 |
\ (x1__::real) = argument_in (lhs e1__); \
|
|
wneuper@3737
|
101 |
\ (B1__::bool) = (Substitute [v_ = x1__]) B__; \
|
|
wneuper@3737
|
102 |
\ B1__ = (Substitute [e1__]) B1__ ; \
|
|
wneuper@3737
|
103 |
\ B2__ = Take B__; \
|
|
wneuper@3737
|
104 |
\ e2__ = nth_ 2 rb_; \
|
|
wneuper@3737
|
105 |
\ (x2__::real) = argument_in (lhs e2__); \
|
|
wneuper@3737
|
106 |
\ (B2__::bool) = ((Substitute [v_ = x2__]) @@ \
|
|
wneuper@3737
|
107 |
\ (Substitute [e2__])) B2__; \
|
|
wneuper@3737
|
108 |
\ (c_1_2__::bool list) = \
|
|
wneuper@3737
|
109 |
\ (SubProblem (Biegelinie_,[linear,system],[no_met]) \
|
|
wneuper@3737
|
110 |
\ [booll_ [B1__, B2__], reall [c,c_2]]); \
|
|
wneuper@3737
|
111 |
\ B__ = Take B__; \
|
|
wneuper@3737
|
112 |
\ B__ = ((Substitute c_1_2__) @@ \
|
|
wneuper@3737
|
113 |
\ (Rewrite_Set_Inst [(bdv, x)] make_ratpoly_in False)) B__ \
|
|
wneuper@3737
|
114 |
\ in B__)"
|
|
wneuper@3737
|
115 |
;
|
|
wneuper@3737
|
116 |
val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
|
|
wneuper@3737
|
117 |
(*---^^^-OK-----------------------------------------------------------------*)
|
|
wneuper@3737
|
118 |
(*---vvv-NOTok--------------------------------------------------------------*)
|
|
wneuper@3737
|
119 |
atomty sc;
|
|
wneuper@3737
|
120 |
atomt sc;
|
|
wneuper@3737
|
121 |
|
|
wneuper@3737
|
122 |
(* use"../smltest/IsacKnowledge/biegelinie.sml";
|
|
wneuper@3737
|
123 |
*)
|
|
wneuper@3737
|
124 |
|
|
wneuper@3737
|
125 |
"----------- IntegrierenUndKonstanteBestimmen by rewriting -------";
|
|
wneuper@3737
|
126 |
"----------- IntegrierenUndKonstanteBestimmen by rewriting -------";
|
|
wneuper@3737
|
127 |
"----------- IntegrierenUndKonstanteBestimmen by rewriting -------";
|
|
wneuper@3737
|
128 |
val t = str2t "M_b x = L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2";
|
|
wneuper@3737
|
129 |
val t = rewrit Moment_Neigung t; term2s t;
|
|
wneuper@3737
|
130 |
(*was "EI * ?y'' x = L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2"
|
|
wneuper@3737
|
131 |
### before declaring "y''" as a constant *)
|
|
wneuper@3737
|
132 |
val t = rewrit make_fun_explicit t; term2s t;
|
|
wneuper@3737
|
133 |
|
|
wneuper@3737
|
134 |
|
|
wneuper@3737
|
135 |
"----------- simplify_leaf for this script -----------------------";
|
|
wneuper@3737
|
136 |
"----------- simplify_leaf for this script -----------------------";
|
|
wneuper@3737
|
137 |
"----------- simplify_leaf for this script -----------------------";
|
|
wneuper@3737
|
138 |
val rm_ = str2term"[M_b 0 = 0, M_b L = 0]";
|
|
wneuper@3737
|
139 |
val M__ = str2term"M_b x = -1 * x ^^^ 2 / 2 + x * c + c_2";
|
|
wneuper@3737
|
140 |
val Some (e1__,_) =
|
|
wneuper@3737
|
141 |
rewrite_set_ thy false srls
|
|
wneuper@3737
|
142 |
(str2term"(nth_::[real,bool list]=>bool) 1 " $ rm_);
|
|
wneuper@3737
|
143 |
if term2str e1__ = "M_b 0 = 0" then ()
|
|
wneuper@3737
|
144 |
else raise error "biegelinie.sml simplify nth_ 1 rm_";
|
|
wneuper@3737
|
145 |
|
|
wneuper@3737
|
146 |
val Some (x1__,_) =
|
|
wneuper@3737
|
147 |
rewrite_set_ thy false srls
|
|
wneuper@3737
|
148 |
(str2term"argument_in (lhs (M_b 0 = 0))");
|
|
wneuper@3737
|
149 |
if term2str x1__ = "0" then ()
|
|
wneuper@3737
|
150 |
else raise error "biegelinie.sml simplify argument_in (lhs (M_b 0 = 0)";
|
|
wneuper@3737
|
151 |
|
|
wneuper@3737
|
152 |
trace_rewrite:=true;
|
|
wneuper@3737
|
153 |
trace_rewrite:=false;
|
|
wneuper@3737
|
154 |
|
|
wneuper@3737
|
155 |
|
|
wneuper@3737
|
156 |
|
|
wneuper@3737
|
157 |
"----------- Bsp 7.27 me -----------------------------------------";
|
|
wneuper@3737
|
158 |
"----------- Bsp 7.27 me -----------------------------------------";
|
|
wneuper@3737
|
159 |
"----------- Bsp 7.27 me -----------------------------------------";
|
|
wneuper@3737
|
160 |
val fmz = ["Traegerlaenge L","Streckenlast q_0","Biegelinie y",
|
|
wneuper@3737
|
161 |
"RandbedingungenBiegung [y 0 = 0, y L = 0]",
|
|
wneuper@3737
|
162 |
"RandbedingungenMoment [M_b 0 = 0, M_b L = 0]",
|
|
wneuper@3737
|
163 |
"FunktionsVariable x"];
|
|
wneuper@3737
|
164 |
val (dI',pI',mI') =
|
|
wneuper@3737
|
165 |
("Biegelinie.thy",["MomentBestimmte","Biegelinien"],
|
|
wneuper@3737
|
166 |
["IntegrierenUndKonstanteBestimmen"]);
|
|
wneuper@3737
|
167 |
val p = e_pos'; val c = [];
|
|
wneuper@3737
|
168 |
val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
|
|
wneuper@3737
|
169 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
|
wneuper@3737
|
170 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
|
wneuper@3737
|
171 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
|
wneuper@3737
|
172 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
|
wneuper@3737
|
173 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
|
wneuper@3737
|
174 |
|
|
wneuper@3737
|
175 |
val pits = get_obj g_pbl pt (fst p);writeln (itms2str thy pits);
|
|
wneuper@3737
|
176 |
(*if itms2str thy pits = ... all 5 model-items*)
|
|
wneuper@3737
|
177 |
val mits = get_obj g_met pt (fst p); writeln (itms2str thy mits);
|
|
wneuper@3737
|
178 |
if itms2str thy mits = "[]" then ()
|
|
wneuper@3737
|
179 |
else raise error "biegelinie.sml: Bsp 7.27 #2";
|
|
wneuper@3737
|
180 |
|
|
wneuper@3737
|
181 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
|
wneuper@3737
|
182 |
case nxt of (_,Add_Given "FunktionsVariable x") => ()
|
|
wneuper@3737
|
183 |
| _ => raise error "biegelinie.sml: Bsp 7.27 #4a";
|
|
wneuper@3737
|
184 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
|
wneuper@3737
|
185 |
val mits = get_obj g_met pt (fst p);writeln (itms2str thy mits);
|
|
wneuper@3737
|
186 |
(*if itms2str thy mits = ... all 6 guard-items*)
|
|
wneuper@3737
|
187 |
case nxt of (_, Apply_Method ["IntegrierenUndKonstanteBestimmen"]) => ()
|
|
wneuper@3737
|
188 |
| _ => raise error "biegelinie.sml: Bsp 7.27 #4b";
|
|
wneuper@3737
|
189 |
|
|
wneuper@3737
|
190 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
|
|
wneuper@3737
|
191 |
case pt of Nd (PblObj _, [Nd _]) => ((*Apply_Method + Take*))
|
|
wneuper@3737
|
192 |
| _ => raise error "biegelinie.sml: Bsp 7.27 #4c";
|
|
wneuper@3737
|
193 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
|
|
wneuper@3737
|
194 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
|
|
wneuper@3737
|
195 |
|
|
wneuper@3737
|
196 |
case nxt of
|
|
wneuper@3737
|
197 |
(_,Subproblem ("Biegelinie.thy", ["named", "integrate", "function"])) => ()
|
|
wneuper@3737
|
198 |
| _ => raise error "biegelinie.sml: Bsp 7.27 #4c";
|
|
wneuper@3737
|
199 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
|
wneuper@3737
|
200 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
|
wneuper@3737
|
201 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
|
wneuper@3737
|
202 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
|
wneuper@3789
|
203 |
case nxt of (_, Apply_Method ["diff", "integration", "named"]) => ()
|
|
wneuper@3737
|
204 |
| _ => raise error "biegelinie.sml: Bsp 7.27 #5";
|
|
wneuper@3737
|
205 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
|
|
wneuper@3737
|
206 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
|
|
wneuper@3737
|
207 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
|
|
wneuper@3737
|
208 |
case nxt of
|
|
wneuper@3737
|
209 |
("Check_Postcond", Check_Postcond ["named", "integrate", "function"]) => ()
|
|
wneuper@3737
|
210 |
| _ => raise error "biegelinie.sml: Bsp 7.27 #5a";
|
|
wneuper@3737
|
211 |
|
|
wneuper@3737
|
212 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
|
|
wneuper@3737
|
213 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
|
|
wneuper@3737
|
214 |
case nxt of
|
|
wneuper@3737
|
215 |
(_, Subproblem ("Biegelinie.thy", ["named", "integrate", "function"]))=>()
|
|
wneuper@3737
|
216 |
| _ => raise error "biegelinie.sml: Bsp 7.27 #5b";
|
|
wneuper@3737
|
217 |
|
|
wneuper@3737
|
218 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
|
wneuper@3737
|
219 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
|
wneuper@3737
|
220 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
|
wneuper@3737
|
221 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
|
wneuper@3789
|
222 |
case nxt of (_, Apply_Method ["diff", "integration","named"]) => ()
|
|
wneuper@3737
|
223 |
| _ => raise error "biegelinie.sml: Bsp 7.27 #6";
|
|
wneuper@3737
|
224 |
|
|
wneuper@3737
|
225 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
|
|
wneuper@3737
|
226 |
val (p,_,f,nxt,_,pt) = me nxt p c pt(*nxt = Check_Postcond ["named", "int..*);
|
|
wneuper@3737
|
227 |
f2str f;
|
|
wneuper@3737
|
228 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
|
|
wneuper@3737
|
229 |
case nxt of (_, Substitute ["x = 0"]) => ()
|
|
wneuper@3737
|
230 |
| _ => raise error "biegelinie.sml: Bsp 7.27 #7";
|
|
wneuper@3737
|
231 |
|
|
wneuper@3737
|
232 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
|
|
wneuper@3737
|
233 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
|
|
wneuper@3737
|
234 |
if f2str f = "0 = c_2 + c * 0 + -1 * q_0 / 2 * 0 ^^^ 2" then ()
|
|
wneuper@3737
|
235 |
else raise error "biegelinie.sml: Bsp 7.27 #8";
|
|
wneuper@3737
|
236 |
|
|
wneuper@3737
|
237 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
|
|
wneuper@3737
|
238 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
|
|
wneuper@3737
|
239 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
|
|
wneuper@3737
|
240 |
if f2str f = "0 = c_2 + c * L + -1 * q_0 / 2 * L ^^^ 2" then ()
|
|
wneuper@3737
|
241 |
else raise error "biegelinie.sml: Bsp 7.27 #9";
|
|
wneuper@3737
|
242 |
|
|
wneuper@3737
|
243 |
(*val nxt = (+, Subproblem ("Biegelinie.thy", ["normalize", ..lin..sys]))*)
|
|
wneuper@3737
|
244 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
|
wneuper@3737
|
245 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
|
wneuper@3737
|
246 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
|
wneuper@3737
|
247 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
|
wneuper@3737
|
248 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
|
wneuper@3737
|
249 |
case nxt of (_, Apply_Method ["EqSystem", "normalize", "2x2"]) => ()
|
|
wneuper@3737
|
250 |
| _ => raise error "biegelinie.sml: Bsp 7.27 #10";
|
|
wneuper@3737
|
251 |
|
|
wneuper@3737
|
252 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
|
|
wneuper@3737
|
253 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
|
|
wneuper@3737
|
254 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
|
|
wneuper@3737
|
255 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
|
|
wneuper@3737
|
256 |
(*val nxt = Subproblem ["triangular", "2x2", "linear", "system"]*)
|
|
wneuper@3737
|
257 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
|
wneuper@3737
|
258 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
|
wneuper@3737
|
259 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
|
wneuper@3737
|
260 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
|
wneuper@3737
|
261 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
|
wneuper@3737
|
262 |
case nxt of (_, Apply_Method["EqSystem", "top_down_substitution", "2x2"]) => ()
|
|
wneuper@3737
|
263 |
| _ => raise error "biegelinie.sml: Bsp 7.27 #11";
|
|
wneuper@3737
|
264 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
|
|
wneuper@3737
|
265 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
|
|
wneuper@3737
|
266 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
|
|
wneuper@3737
|
267 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
|
|
wneuper@3737
|
268 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
|
|
wneuper@3737
|
269 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
|
|
wneuper@3737
|
270 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
|
|
wneuper@3737
|
271 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
|
|
wneuper@3737
|
272 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
|
|
wneuper@3737
|
273 |
case nxt of (_, Check_Postcond ["normalize", "2x2", "linear", "system"]) => ()
|
|
wneuper@3737
|
274 |
| _ => raise error "biegelinie.sml: Bsp 7.27 #12";
|
|
wneuper@3737
|
275 |
|
|
wneuper@3737
|
276 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
|
|
wneuper@3737
|
277 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
|
|
wneuper@3737
|
278 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
|
|
wneuper@3737
|
279 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
|
|
wneuper@3737
|
280 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
|
|
wneuper@3737
|
281 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
|
|
wneuper@3737
|
282 |
case nxt of
|
|
wneuper@3737
|
283 |
(_, Subproblem ("Biegelinie.thy", ["named", "integrate", "function"]))=>()
|
|
wneuper@3737
|
284 |
| _ => raise error "biegelinie.sml: Bsp 7.27 #13";
|
|
wneuper@3737
|
285 |
|
|
wneuper@3737
|
286 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
|
wneuper@3737
|
287 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
|
wneuper@3737
|
288 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
|
wneuper@3737
|
289 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
|
wneuper@3789
|
290 |
case nxt of (_, Apply_Method ["diff", "integration", "named"]) => ()
|
|
wneuper@3737
|
291 |
| _ => raise error "biegelinie.sml: Bsp 7.27 #14";
|
|
wneuper@3737
|
292 |
|
|
wneuper@3737
|
293 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
|
|
wneuper@3737
|
294 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
|
|
wneuper@3737
|
295 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
|
|
wneuper@3737
|
296 |
case nxt of
|
|
wneuper@3737
|
297 |
(_, Check_Postcond ["named", "integrate", "function"]) => ()
|
|
wneuper@3737
|
298 |
| _ => raise error "biegelinie.sml: Bsp 7.27 #15";
|
|
wneuper@3737
|
299 |
|
|
wneuper@3737
|
300 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
|
|
wneuper@3737
|
301 |
if f2str f =
|
|
wneuper@3737
|
302 |
"y' x = c + 1 / (-1 * EI) * (L * q_0 / 4 * x ^^^ 2 + -1 * q_0 / 6 * x ^^^ 3)"
|
|
wneuper@3737
|
303 |
then () else raise error "biegelinie.sml: Bsp 7.27 #16 f";
|
|
wneuper@3737
|
304 |
case nxt of
|
|
wneuper@3737
|
305 |
(_, Subproblem ("Biegelinie.thy", ["named", "integrate", "function"]))=>()
|
|
wneuper@3737
|
306 |
| _ => raise error "biegelinie.sml: Bsp 7.27 #16";
|
|
wneuper@3737
|
307 |
|
|
wneuper@3737
|
308 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
|
wneuper@3737
|
309 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
|
wneuper@3737
|
310 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
|
wneuper@3737
|
311 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
|
wneuper@3789
|
312 |
case nxt of (_, Apply_Method ["diff", "integration", "named"]) => ()
|
|
wneuper@3737
|
313 |
| _ => raise error "biegelinie.sml: Bsp 7.27 #17";
|
|
wneuper@3737
|
314 |
|
|
wneuper@3737
|
315 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
|
|
wneuper@3737
|
316 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
|
|
wneuper@3737
|
317 |
if f2str f =
|
|
wneuper@3737
|
318 |
"y x =\nc_2 + c * x +\n\
|
|
wneuper@3737
|
319 |
\1 / (-1 * EI) * (L * q_0 / 12 * x ^^^ 3 + -1 * q_0 / 24 * x ^^^ 4)"
|
|
wneuper@3737
|
320 |
then () else raise error "biegelinie.sml: Bsp 7.27 #18 f";
|
|
wneuper@3737
|
321 |
case nxt of
|
|
wneuper@3737
|
322 |
(_, Check_Postcond ["named", "integrate", "function"]) => ()
|
|
wneuper@3737
|
323 |
| _ => raise error "biegelinie.sml: Bsp 7.27 #18";
|
|
wneuper@3737
|
324 |
|
|
wneuper@3737
|
325 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
|
|
wneuper@3737
|
326 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
|
|
wneuper@3737
|
327 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
|
|
wneuper@3737
|
328 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
|
|
wneuper@3737
|
329 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
|
|
wneuper@3737
|
330 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
|
|
wneuper@3737
|
331 |
case nxt of
|
|
wneuper@3737
|
332 |
(_, Subproblem
|
|
wneuper@3737
|
333 |
("Biegelinie.thy", ["normalize", "2x2", "linear", "system"])) => ()
|
|
wneuper@3737
|
334 |
| _ => raise error "biegelinie.sml: Bsp 7.27 #19";
|
|
wneuper@3737
|
335 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
|
wneuper@3737
|
336 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
|
wneuper@3737
|
337 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
|
wneuper@3737
|
338 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
|
wneuper@3737
|
339 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
|
wneuper@3737
|
340 |
case nxt of (_, Apply_Method ["EqSystem", "normalize", "2x2"]) => ()
|
|
wneuper@3737
|
341 |
| _ => raise error "biegelinie.sml: Bsp 7.27 #20";
|
|
wneuper@3737
|
342 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
|
|
wneuper@3737
|
343 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
|
|
wneuper@3737
|
344 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
|
|
wneuper@3737
|
345 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
|
|
wneuper@3737
|
346 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
|
|
wneuper@3737
|
347 |
if f2str f = "[c_2 = 0, L * c + c_2 = -1 * q_0 * L ^^^ 4 / (-24 * EI)]" then ()
|
|
wneuper@3737
|
348 |
else raise error "biegelinie.sml: Bsp 7.27 #21 f";
|
|
wneuper@3737
|
349 |
case nxt of
|
|
wneuper@3737
|
350 |
(_, Subproblem
|
|
wneuper@3737
|
351 |
("Biegelinie.thy", ["triangular", "2x2", "linear", "system"])) =>()
|
|
wneuper@3737
|
352 |
| _ => raise error "biegelinie.sml: Bsp 7.27 #21";
|
|
wneuper@3737
|
353 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
|
wneuper@3737
|
354 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
|
wneuper@3737
|
355 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
|
wneuper@3737
|
356 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
|
wneuper@3737
|
357 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
|
wneuper@3737
|
358 |
case nxt of (_, Apply_Method["EqSystem", "top_down_substitution", "2x2"]) => ()
|
|
wneuper@3737
|
359 |
| _ => raise error "biegelinie.sml: Bsp 7.27 #22";
|
|
wneuper@3737
|
360 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
|
|
wneuper@3737
|
361 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
|
|
wneuper@3737
|
362 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
|
|
wneuper@3737
|
363 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
|
|
wneuper@3737
|
364 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
|
|
wneuper@3737
|
365 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
|
|
wneuper@3737
|
366 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
|
|
wneuper@3737
|
367 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
|
|
wneuper@3737
|
368 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
|
|
wneuper@3737
|
369 |
case nxt of (_, Check_Postcond ["normalize", "2x2", "linear", "system"]) => ()
|
|
wneuper@3737
|
370 |
| _ => raise error "biegelinie.sml: Bsp 7.27 #23";
|
|
wneuper@3737
|
371 |
|
|
wneuper@3737
|
372 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
|
|
wneuper@3737
|
373 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
|
|
wneuper@3737
|
374 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
|
|
wneuper@3737
|
375 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
|
|
wneuper@3737
|
376 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
|
|
wneuper@3737
|
377 |
if f2str f = "y x =\n-1 * q_0 * L ^^^ 4 / (-24 * EI * L) * x +\n\
|
|
wneuper@3737
|
378 |
\(2 * L * q_0 / (-24 * EI) * x ^^^ 3 + \
|
|
wneuper@3737
|
379 |
\-1 * q_0 / (-24 * EI) * x ^^^ 4)" then ()
|
|
wneuper@3737
|
380 |
else raise error "biegelinie.sml: Bsp 7.27 #24 f";
|
|
wneuper@3737
|
381 |
case nxt of ("End_Proof'", End_Proof') => ()
|
|
wneuper@3737
|
382 |
| _ => raise error "biegelinie.sml: Bsp 7.27 #24";
|
|
wneuper@3737
|
383 |
|
|
wneuper@3737
|
384 |
(* use"../smltest/IsacKnowledge/biegelinie.sml";
|
|
wneuper@3737
|
385 |
*)
|
|
wneuper@3737
|
386 |
show_pt pt;
|
|
wneuper@3737
|
387 |
(*(([], Frm), Problem (Biegelinie.thy, [MomentBestimmte, Biegelinien])),
|
|
wneuper@3852
|
388 |
(([1], Frm), q_ x = q_0),
|
|
wneuper@3852
|
389 |
(([1], Res), - q_ x = - q_0),
|
|
wneuper@3737
|
390 |
(([2], Res), Q' x = - q_0),
|
|
wneuper@3737
|
391 |
(([3], Pbl), Integrate (- q_0, x)),
|
|
wneuper@3737
|
392 |
(([3,1], Frm), Q x = Integral - q_0 D x),
|
|
wneuper@3737
|
393 |
(([3,1], Res), Q x = -1 * q_0 * x + c),
|
|
wneuper@3737
|
394 |
(([3], Res), Q x = -1 * q_0 * x + c),
|
|
wneuper@3737
|
395 |
(([4], Res), M_b' x = -1 * q_0 * x + c),
|
|
wneuper@3737
|
396 |
(([5], Pbl), Integrate (-1 * q_0 * x + c, x)),
|
|
wneuper@3737
|
397 |
(([5,1], Frm), M_b x = Integral -1 * q_0 * x + c D x),
|
|
wneuper@3737
|
398 |
(([5,1], Res), M_b x = -1 * q_0 * x ^^^ 2 / 2 + x * c + c_2),
|
|
wneuper@3737
|
399 |
(([5], Res), M_b x = -1 * q_0 * x ^^^ 2 / 2 + x * c + c_2),
|
|
wneuper@3737
|
400 |
(([6], Res), M_b 0 = -1 * q_0 * 0 ^^^ 2 / 2 + 0 * c + c_2),
|
|
wneuper@3737
|
401 |
(([7], Res), 0 = -1 * q_0 * 0 ^^^ 2 / 2 + 0 * c + c_2),
|
|
wneuper@3737
|
402 |
(([8], Res), M_b L = -1 * q_0 * L ^^^ 2 / 2 + L * c + c_2),
|
|
wneuper@3737
|
403 |
(([9], Res), 0 = -1 * q_0 * L ^^^ 2 / 2 + L * c + c_2),
|
|
wneuper@3737
|
404 |
(([10], Pbl), solveSystem [0 = -1 * q_0 * L ^^^ 2 / 2 + L * c + c_2] [c_2]),
|
|
wneuper@3737
|
405 |
(([10,1], Frm), [0 = -1 * q_0 * 0 ^^^ 2 / 2 + 0 * c + c_2,
|
|
wneuper@3737
|
406 |
0 = -1 * q_0 * L ^^^ 2 / 2 + L * c + c_2]),
|
|
wneuper@3737
|
407 |
(([10,1], Res), [0 = c_2, 0 = -1 * (q_0 * L ^^^ 2) / 2 + (L * c + c_2)]),
|
|
wneuper@3737
|
408 |
(([10,2], Res), [c_2 = 0, L * c + c_2 = 0 + -1 * (-1 * (q_0 * L ^^^ 2) / 2)]),
|
|
wneuper@3737
|
409 |
(([10,3], Res), [c_2 = 0, L * c + c_2 = q_0 * L ^^^ 2 / 2]),
|
|
wneuper@3737
|
410 |
(([10,4], Pbl), solveSystem [L * c + c_2 = q_0 * L ^^^ 2 / 2] [c_2]),
|
|
wneuper@3737
|
411 |
(([10,4,1], Frm), L * c + c_2 = q_0 * L ^^^ 2 / 2),
|
|
wneuper@3737
|
412 |
(([10,4,1], Res), L * c + 0 = q_0 * L ^^^ 2 / 2),
|
|
wneuper@3737
|
413 |
(([10,4,2], Res), L * c = q_0 * L ^^^ 2 / 2),
|
|
wneuper@3737
|
414 |
(([10,4,3], Res), c = q_0 * L ^^^ 2 / 2 / L),
|
|
wneuper@3737
|
415 |
(([10,4,4], Res), c = L * q_0 / 2),
|
|
wneuper@3737
|
416 |
(([10,4,5], Res), [c = L * q_0 / 2, c_2 = 0]),
|
|
wneuper@3737
|
417 |
(([10,4], Res), [c = L * q_0 / 2, c_2 = 0]),
|
|
wneuper@3737
|
418 |
(([10], Res), [c = L * q_0 / 2, c_2 = 0]),
|
|
wneuper@3737
|
419 |
(([11], Res), M_b x = -1 * q_0 * x ^^^ 2 / 2 + x * (L * q_0 / 2) + 0),
|
|
wneuper@3737
|
420 |
(([12], Res), M_b x = L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2),
|
|
wneuper@3737
|
421 |
(([13], Res), EI * y'' x = L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2),
|
|
wneuper@3737
|
422 |
(([14], Res), y'' x = 1 / EI * (L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2)),
|
|
wneuper@3737
|
423 |
(([15], Pbl), Integrate (1 / EI * (L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2), x)),
|
|
wneuper@3737
|
424 |
(([15,1], Frm), y' x = Integral 1 / EI * (L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2) D x),
|
|
wneuper@3737
|
425 |
(([15,1], Res), y' x =
|
|
wneuper@3737
|
426 |
(Integral L * q_0 * x / 2 D x + Integral -1 * q_0 * x ^^^ 2 / 2 D x) / EI +
|
|
wneuper@3737
|
427 |
c)]*)
|
|
wneuper@3737
|
428 |
|
|
wneuper@3737
|
429 |
"----------- Bsp 7.27 autoCalculate ------------------------------";
|
|
wneuper@3737
|
430 |
"----------- Bsp 7.27 autoCalculate ------------------------------";
|
|
wneuper@3737
|
431 |
"----------- Bsp 7.27 autoCalculate ------------------------------";
|
|
wneuper@3737
|
432 |
states:=[];
|
|
wneuper@3737
|
433 |
CalcTree [(["Traegerlaenge L","Streckenlast q_0","Biegelinie y",
|
|
wneuper@3737
|
434 |
"RandbedingungenBiegung [y 0 = 0, y L = 0]",
|
|
wneuper@3737
|
435 |
"RandbedingungenMoment [M_b 0 = 0, M_b L = 0]",
|
|
wneuper@3737
|
436 |
"FunktionsVariable x"],
|
|
wneuper@3737
|
437 |
("Biegelinie.thy",
|
|
wneuper@3737
|
438 |
["MomentBestimmte","Biegelinien"],
|
|
wneuper@3737
|
439 |
["IntegrierenUndKonstanteBestimmen"]))];
|
|
wneuper@3737
|
440 |
moveActiveRoot 1;
|
|
wneuper@3737
|
441 |
autoCalculate 1 CompleteCalcHead;
|
|
wneuper@3737
|
442 |
|
|
wneuper@3737
|
443 |
fetchProposedTactic 1 (*->"Apply_Method" IntegrierenUndKonstanteBestimmen*);
|
|
wneuper@3737
|
444 |
(*
|
|
wneuper@3737
|
445 |
> val (_,Apply_Method' (_, None, ScrState is), _)::_ = tacis;
|
|
wneuper@3737
|
446 |
> is = e_scrstate;
|
|
wneuper@3737
|
447 |
val it = true : bool
|
|
wneuper@3737
|
448 |
*)
|
|
wneuper@3737
|
449 |
autoCalculate 1 (Step 1) (*->GENERATED ([1], Frm)*);
|
|
wneuper@3737
|
450 |
val ((pt,_),_) = get_calc 1;
|
|
wneuper@3737
|
451 |
case pt of Nd (PblObj _, [Nd _]) => ((*Apply_Method + Take*))
|
|
wneuper@3737
|
452 |
| _ => raise error "biegelinie.sml: Bsp 7.27 autoCalculate#4c";
|
|
wneuper@3737
|
453 |
|
|
wneuper@3737
|
454 |
autoCalculate 1 CompleteCalc;
|
|
wneuper@3737
|
455 |
val ((pt,p),_) = get_calc 1;
|
|
wneuper@3737
|
456 |
if p = ([], Res) andalso length (children pt) = 23 andalso
|
|
wneuper@3737
|
457 |
term2str (get_obj g_res pt (fst p)) = "y x =\n-1 * q_0 * L ^^^ 4 / (-24 * EI * L) * x +\n(2 * L * q_0 / (-24 * EI) * x ^^^ 3 + -1 * q_0 / (-24 * EI) * x ^^^ 4)"then () else raise error "biegelinie.sml: 1st biegelin.7.27 changed";
|
|
wneuper@3737
|
458 |
|
|
wneuper@3737
|
459 |
val (unc, del, gen) = (([],Pbl), ([],Pbl), ([],Res));
|
|
wneuper@3737
|
460 |
getFormulaeFromTo 1 unc gen 1 (*only level 1*) false;
|
|
wneuper@3737
|
461 |
show_pt pt;
|
|
wneuper@3737
|
462 |
|
|
wneuper@3737
|
463 |
(*check all formulae for getTactic*)
|
|
wneuper@3737
|
464 |
getTactic 1 ([1],Frm) (*see smltest/../reverse-rew.sml*);
|
|
wneuper@3737
|
465 |
getTactic 1 ([5],Res) (*tac2xml: not impl. for Substitute ["x = 0"]*);
|
|
wneuper@3737
|
466 |
getTactic 1 ([6],Res) (* ---"--- ["M_b 0 = 0"]*);
|
|
wneuper@3737
|
467 |
getTactic 1 ([7],Res) (*!!!!!Take!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!*);
|
|
wneuper@3737
|
468 |
getTactic 1 ([8],Frm) (*tac2xml: not impl. for Substitute ["x = L"]*);
|
|
wneuper@3737
|
469 |
getTactic 1 ([8],Res) (* ---"--- ["M_b L = 0"]*);
|
|
wneuper@3737
|
470 |
|
|
wneuper@3737
|
471 |
|
|
wneuper@3737
|
472 |
"----------- SubProblem (_,[vonBelastungZu,Biegelinien] ----------";
|
|
wneuper@3737
|
473 |
"----------- SubProblem (_,[vonBelastungZu,Biegelinien] ----------";
|
|
wneuper@3737
|
474 |
"----------- SubProblem (_,[vonBelastungZu,Biegelinien] ----------";
|
|
wneuper@3737
|
475 |
val fmz =
|
|
wneuper@3737
|
476 |
["Streckenlast q_0","FunktionsVariable x",
|
|
wneuper@3737
|
477 |
"Funktionen [Q x = c + -1 * q_0 * x, \
|
|
wneuper@3737
|
478 |
\M_b x = c_2 + c * x + -1 * q_0 / 2 * x ^^^ 2,\
|
|
wneuper@3737
|
479 |
\ y' x = c_3 + 1 / (-1 * EI) * (c_2 * x + c / 2 * x ^^^ 2 + -1 * q_0 / 6 * x ^^^ 3),\
|
|
wneuper@3737
|
480 |
\ 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)]"];
|
|
wneuper@3737
|
481 |
val (dI',pI',mI') = ("Biegelinie.thy", ["vonBelastungZu","Biegelinien"],
|
|
wneuper@3737
|
482 |
["Biegelinien","ausBelastung"]);
|
|
wneuper@3737
|
483 |
val p = e_pos'; val c = [];
|
|
wneuper@3737
|
484 |
val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
|
|
wneuper@3737
|
485 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
|
wneuper@3737
|
486 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
|
wneuper@3737
|
487 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
|
wneuper@3737
|
488 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
|
wneuper@3737
|
489 |
if nxt = ("Apply_Method", Apply_Method ["Biegelinien", "ausBelastung"])
|
|
wneuper@3737
|
490 |
then () else raise error "biegelinie.sml met2 b";
|
|
wneuper@3737
|
491 |
|
|
wneuper@3852
|
492 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f = "q_ x = q_0";
|
|
wneuper@3852
|
493 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f = "- q_ x = - q_0";
|
|
wneuper@3737
|
494 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f = "Q' x = - q_0";
|
|
wneuper@3737
|
495 |
case nxt of (_, Subproblem (_, ["named", "integrate", "function"])) => ()
|
|
wneuper@3737
|
496 |
| _ => raise error "biegelinie.sml met2 c";
|
|
wneuper@3737
|
497 |
|
|
wneuper@3737
|
498 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
|
wneuper@3737
|
499 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
|
wneuper@3737
|
500 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
|
wneuper@3737
|
501 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
|
wneuper@3737
|
502 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
|
wneuper@3737
|
503 |
|
|
wneuper@3737
|
504 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f = "Q x = c + -1 * q_0 * x";
|
|
wneuper@3737
|
505 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f = "Q x = c + -1 * q_0 * x";
|
|
wneuper@3737
|
506 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f = "M_b' x = c + -1 * q_0 * x";
|
|
wneuper@3737
|
507 |
case nxt of (_,Subproblem (_, ["named", "integrate", "function"])) => ()
|
|
wneuper@3737
|
508 |
| _ => raise error "biegelinie.sml met2 d";
|
|
wneuper@3737
|
509 |
|
|
wneuper@3737
|
510 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
|
wneuper@3737
|
511 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
|
wneuper@3737
|
512 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
|
wneuper@3737
|
513 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
|
wneuper@3737
|
514 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f =
|
|
wneuper@3737
|
515 |
"M_b x = Integral c + -1 * q_0 * x D x";
|
|
wneuper@3737
|
516 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f =
|
|
wneuper@3737
|
517 |
"M_b x = c_2 + c * x + -1 * q_0 / 2 * x ^^^ 2";
|
|
wneuper@3737
|
518 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f =
|
|
wneuper@3737
|
519 |
"M_b x = c_2 + c * x + -1 * q_0 / 2 * x ^^^ 2";
|
|
wneuper@3737
|
520 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f =
|
|
wneuper@3737
|
521 |
"- EI * y'' x = c_2 + c * x + -1 * q_0 / 2 * x ^^^ 2";
|
|
wneuper@3737
|
522 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f =
|
|
wneuper@3737
|
523 |
"y'' x = 1 / - EI * (c_2 + c * x + -1 * q_0 / 2 * x ^^^ 2)";
|
|
wneuper@3737
|
524 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
|
wneuper@3737
|
525 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
|
wneuper@3737
|
526 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
|
wneuper@3737
|
527 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
|
wneuper@3737
|
528 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f =
|
|
wneuper@3737
|
529 |
"y' x = Integral 1 / - EI * (c_2 + c * x + -1 * q_0 / 2 * x ^^^ 2) D x";
|
|
wneuper@3737
|
530 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f =
|
|
wneuper@3737
|
531 |
"y' x = Integral 1 / (-1 * EI) * (c_2 + c * x + -1 * q_0 / 2 * x ^^^ 2) D x";
|
|
wneuper@3737
|
532 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f =
|
|
wneuper@3737
|
533 |
"y' x =\nc_3 + 1 / (-1 * EI) * (c_2 * x + c / 2 * x ^^^ 2 + -1 * q_0 / 6 * x ^^^ 3)";
|
|
wneuper@3737
|
534 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f =
|
|
wneuper@3737
|
535 |
"y' x =\nc_3 + 1 / (-1 * EI) * (c_2 * x + c / 2 * x ^^^ 2 + -1 * q_0 / 6 * x ^^^ 3)";
|
|
wneuper@3737
|
536 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
|
wneuper@3737
|
537 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
|
wneuper@3737
|
538 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
|
wneuper@3737
|
539 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
|
wneuper@3737
|
540 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f =
|
|
wneuper@3737
|
541 |
"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";
|
|
wneuper@3737
|
542 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f =
|
|
wneuper@3737
|
543 |
"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)";
|
|
wneuper@3737
|
544 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f =
|
|
wneuper@3737
|
545 |
"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)";
|
|
wneuper@3737
|
546 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
|
wneuper@3737
|
547 |
if nxt = ("End_Proof'", End_Proof') andalso f2str f =
|
|
wneuper@3737
|
548 |
"[Q x = c + -1 * q_0 * x, M_b x = c_2 + c * x + -1 * q_0 / 2 * x ^^^ 2,\n y' 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)]" then ()
|
|
wneuper@3737
|
549 |
else raise error "biegelinie.sml met2 e";
|
|
wneuper@3737
|
550 |
|
|
wneuper@3737
|
551 |
|
|
wneuper@3737
|
552 |
|
|
wneuper@3737
|
553 |
"----------- SubProblem (_,[setzeRandbedingungen,Biegelinien] ----";
|
|
wneuper@3737
|
554 |
"----------- SubProblem (_,[setzeRandbedingungen,Biegelinien] ----";
|
|
wneuper@3737
|
555 |
"----------- SubProblem (_,[setzeRandbedingungen,Biegelinien] ----";
|
|
wneuper@3737
|
556 |
val str =
|
|
wneuper@3737
|
557 |
"Script Function2Equality (fun_::bool) (sub_::bool) =\
|
|
wneuper@3737
|
558 |
\(equ___::bool)"
|
|
wneuper@3737
|
559 |
;
|
|
wneuper@3737
|
560 |
val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
|
|
wneuper@3737
|
561 |
val str =
|
|
wneuper@3737
|
562 |
"Script Function2Equality (fun_::bool) (sub_::bool) =\
|
|
wneuper@3737
|
563 |
\ (let v_ = argument_in (lhs fun_)\
|
|
wneuper@3737
|
564 |
\ in (equ___::bool))"
|
|
wneuper@3737
|
565 |
;
|
|
wneuper@3737
|
566 |
val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
|
|
wneuper@3737
|
567 |
val str =
|
|
wneuper@3737
|
568 |
"Script Function2Equality (fun_::bool) (sub_::bool) =\
|
|
wneuper@3737
|
569 |
\ (let v_ = argument_in (lhs fun_);\
|
|
wneuper@3737
|
570 |
\ (equ_) = (Substitute [sub_]) fun_\
|
|
wneuper@3737
|
571 |
\ in (equ_::bool))"
|
|
wneuper@3737
|
572 |
;
|
|
wneuper@3737
|
573 |
val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
|
|
wneuper@3737
|
574 |
val str =
|
|
wneuper@3737
|
575 |
"Script Function2Equality (fun_::bool) (sub_::bool) =\
|
|
wneuper@3737
|
576 |
\ (let v_ = argument_in (lhs fun_);\
|
|
wneuper@3737
|
577 |
\ equ_ = (Substitute [sub_]) fun_\
|
|
wneuper@3737
|
578 |
\ in (Rewrite_Set_Inst [(bdv, v_)] make_ratpoly_in False) equ_)"
|
|
wneuper@3737
|
579 |
;
|
|
wneuper@3737
|
580 |
val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
|
|
wneuper@3737
|
581 |
(*---^^^-OK-----------------------------------------------------------------*)
|
|
wneuper@3737
|
582 |
val str =
|
|
wneuper@3737
|
583 |
(*(M_b x = c_2 + c * x + -1 * q_0 / 2 * x ^^^ 2) (M_b L = 0) -->
|
|
wneuper@3737
|
584 |
0 = c_2 + c * L + -1 * q_0 / 2 * L ^^^ 2*)
|
|
wneuper@3737
|
585 |
"Script Function2Equality (fun_::bool) (sub_::bool) =\
|
|
wneuper@3737
|
586 |
\ (let bdv_ = argument_in (lhs fun_);\
|
|
wneuper@3737
|
587 |
\ val_ = argument_in (lhs sub_);\
|
|
wneuper@3737
|
588 |
\ equ_ = (Substitute [bdv_ = val_]) fun_;\
|
|
wneuper@3737
|
589 |
\ equ_ = (Substitute [sub_]) fun_\
|
|
wneuper@3737
|
590 |
\ in (Rewrite_Set_Inst [(bdv_, v_)] make_ratpoly_in False) equ_)"
|
|
wneuper@3737
|
591 |
;
|
|
wneuper@3737
|
592 |
val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
|
|
wneuper@3737
|
593 |
(*---vvv-NOTok--------------------------------------------------------------*)
|
|
wneuper@3737
|
594 |
atomty sc;
|
|
wneuper@3737
|
595 |
|
|
wneuper@3737
|
596 |
val fmz = ["functionEq (M_b x = c_2 + c * x + -1 * q_0 / 2 * x ^^^ 2)",
|
|
wneuper@3737
|
597 |
"substitution (M_b L = 0)",
|
|
wneuper@3737
|
598 |
"equality equ___"];
|
|
wneuper@3737
|
599 |
val (dI',pI',mI') = ("Biegelinie.thy", ["makeFunctionTo","equation"],
|
|
wneuper@3737
|
600 |
["Equation","fromFunction"]);
|
|
wneuper@3737
|
601 |
val p = e_pos'; val c = [];
|
|
wneuper@3737
|
602 |
val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
|
|
wneuper@3737
|
603 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
|
wneuper@3737
|
604 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
|
wneuper@3737
|
605 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
|
wneuper@3737
|
606 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
|
wneuper@3737
|
607 |
|
|
wneuper@3737
|
608 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f =
|
|
wneuper@3737
|
609 |
"M_b x = c_2 + c * x + -1 * q_0 / 2 * x ^^^ 2";
|
|
wneuper@3737
|
610 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f =
|
|
wneuper@3737
|
611 |
"M_b L = c_2 + c * L + -1 * q_0 / 2 * L ^^^ 2";
|
|
wneuper@3737
|
612 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f =
|
|
wneuper@3737
|
613 |
"0 = c_2 + c * L + -1 * q_0 / 2 * L ^^^ 2";
|
|
wneuper@3737
|
614 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
|
|
wneuper@3737
|
615 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
|
|
wneuper@3737
|
616 |
if nxt = ("End_Proof'", End_Proof') andalso
|
|
wneuper@3737
|
617 |
(* f2str f = "0 = c_2 + L * c + -1 * q_0 / 2 * L ^^^ 2"
|
|
wneuper@3737
|
618 |
CHANGE NOT considered, already on leave*)
|
|
wneuper@3737
|
619 |
f2str f = "0 = (2 * c_2 + 2 * L * c + -1 * L ^^^ 2 * q_0) / 2"
|
|
wneuper@3737
|
620 |
then () else raise error "biegelinie.sml: SubProblem (_,[setzeRandbed";
|
|
wneuper@3737
|
621 |
|
|
wneuper@3737
|
622 |
|
|
wneuper@3737
|
623 |
"----------- method [Biegelinien,setzeRandbedingungenEin] + exec -";
|
|
wneuper@3737
|
624 |
"----------- method [Biegelinien,setzeRandbedingungenEin] + exec -";
|
|
wneuper@3737
|
625 |
"----------- method [Biegelinien,setzeRandbedingungenEin] + exec -";
|
|
wneuper@3737
|
626 |
"----- check the scripts syntax";
|
|
wneuper@3737
|
627 |
val str =
|
|
wneuper@3737
|
628 |
"Script SetzeRandbedScript (funs_::bool list) (beds_::bool list) =\
|
|
wneuper@3737
|
629 |
\ (let b1 = Take (nth_ 1 beds_)\
|
|
wneuper@3737
|
630 |
\ in (equs_::bool list))"
|
|
wneuper@3737
|
631 |
;
|
|
wneuper@3737
|
632 |
val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
|
|
wneuper@3737
|
633 |
val str =
|
|
wneuper@3737
|
634 |
"Script SetzeRandbedScript (funs_::bool list) (beds_::bool list) =\
|
|
wneuper@3737
|
635 |
\ (let b1_ = Take (nth_ 1 beds_); \
|
|
wneuper@3737
|
636 |
\ fs_ = filter (sameFunId (lhs b1_)) funs_; \
|
|
wneuper@3737
|
637 |
\ f1_ = hd fs_ \
|
|
wneuper@3737
|
638 |
\ in (equs_::bool list))"
|
|
wneuper@3737
|
639 |
;
|
|
wneuper@3737
|
640 |
val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
|
|
wneuper@3737
|
641 |
|
|
wneuper@3737
|
642 |
val ttt = str2term "sameFunId (lhs b1_) fun___"; atomty ttt;
|
|
wneuper@3737
|
643 |
val ttt = str2term "filter"; atomty ttt;
|
|
wneuper@3737
|
644 |
val ttt = str2term "filter::[real => bool, real list] => real list";atomty ttt;
|
|
wneuper@3737
|
645 |
val ttt = str2term "filter::[bool => bool, bool list] => bool list";
|
|
wneuper@3737
|
646 |
val ttt = str2term "filter (sameFunId (lhs b1_)) funs_"; atomty ttt;
|
|
wneuper@3737
|
647 |
|
|
wneuper@3737
|
648 |
val str =
|
|
wneuper@3737
|
649 |
"Script SetzeRandbedScript (funs_::bool list) (rb_::bool list) =\
|
|
wneuper@3737
|
650 |
\ (let beds_ = rev beds_; \
|
|
wneuper@3737
|
651 |
\ b1_ = Take (nth_ 1 beds_); \
|
|
wneuper@3737
|
652 |
\ fs_ = filter (sameFunId (lhs b1_)) funs_; \
|
|
wneuper@3737
|
653 |
\ f1_ = hd fs_ \
|
|
wneuper@3737
|
654 |
\ in (equs_::bool list))"
|
|
wneuper@3737
|
655 |
;
|
|
wneuper@3737
|
656 |
val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
|
|
wneuper@3737
|
657 |
val str =
|
|
wneuper@3737
|
658 |
"Script SetzeRandbedScript (funs_::bool list) (rb_::bool list) =\
|
|
wneuper@3737
|
659 |
\ (let b1_ = Take (nth_ 1 rb_); \
|
|
wneuper@3737
|
660 |
\ fs_ = filter (sameFunId (lhs b1_)) funs_; \
|
|
wneuper@3737
|
661 |
\ (equ_::bool) = \
|
|
wneuper@3737
|
662 |
\ (SubProblem (Biegelinie_,[makeFunctionTo,equation],\
|
|
wneuper@3737
|
663 |
\ [Equation,fromFunction]) \
|
|
wneuper@3737
|
664 |
\ [bool_ (hd fs_), bool_ b1_]) \
|
|
wneuper@3737
|
665 |
\ in [equ_])"
|
|
wneuper@3737
|
666 |
;
|
|
wneuper@3737
|
667 |
val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
|
|
wneuper@3737
|
668 |
val str =
|
|
wneuper@3737
|
669 |
"Script SetzeRandbedScript (funs_::bool list) (rb_::bool list) =\
|
|
wneuper@3737
|
670 |
\ (let b1_ = Take (nth_ 1 rb_); \
|
|
wneuper@3737
|
671 |
\ fs_ = filter (sameFunId (lhs b1_)) funs_; \
|
|
wneuper@3737
|
672 |
\ (e1_::bool) = \
|
|
wneuper@3737
|
673 |
\ (SubProblem (Biegelinie_,[makeFunctionTo,equation],\
|
|
wneuper@3737
|
674 |
\ [Equation,fromFunction]) \
|
|
wneuper@3737
|
675 |
\ [bool_ (hd fs_), bool_ b1_]); \
|
|
wneuper@3737
|
676 |
\ b2_ = Take (nth_ 2 rb_); \
|
|
wneuper@3737
|
677 |
\ fs_ = filter (sameFunId (lhs b2_)) funs_; \
|
|
wneuper@3737
|
678 |
\ (e2_::bool) = \
|
|
wneuper@3737
|
679 |
\ (SubProblem (Biegelinie_,[makeFunctionTo,equation],\
|
|
wneuper@3737
|
680 |
\ [Equation,fromFunction]) \
|
|
wneuper@3737
|
681 |
\ [bool_ (hd fs_), bool_ b2_]) \
|
|
wneuper@3737
|
682 |
\ in [e1_,e1_])"
|
|
wneuper@3737
|
683 |
;
|
|
wneuper@3737
|
684 |
val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
|
|
wneuper@3737
|
685 |
(*---vvv-NOTok--------------------------------------------------------------*)
|
|
wneuper@3737
|
686 |
(*---^^^-OK-----------------------------------------------------------------*)
|
|
wneuper@3737
|
687 |
atomty sc;
|
|
wneuper@3737
|
688 |
|
|
wneuper@3737
|
689 |
"----- execute script by manual rewriting";
|
|
wneuper@3737
|
690 |
(*show_types := true;*)
|
|
wneuper@3737
|
691 |
val funs_ = str2term "funs_::bool list";
|
|
wneuper@3737
|
692 |
val funs = str2term
|
|
wneuper@3737
|
693 |
"[Q x = c + -1 * q_0 * x,\
|
|
wneuper@3737
|
694 |
\M_b x = c_2 + c * x + -1 * q_0 / 2 * x ^^^ 2,\
|
|
wneuper@3737
|
695 |
\y' x = c_3 + 1 / (-1 * EI) * (c_2 * x + c / 2 * x ^^^ 2 + -1 * q_0 / 6 * x ^^^ 3),\
|
|
wneuper@3737
|
696 |
\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)]";
|
|
wneuper@3737
|
697 |
val rb_ = str2term "rb_::bool list";
|
|
wneuper@3737
|
698 |
val rb = str2term "[y 0 = 0, y L = 0, M_b 0 = 0, M_b L = 0]";
|
|
wneuper@3737
|
699 |
|
|
wneuper@3737
|
700 |
"--- script expression 1";
|
|
wneuper@3737
|
701 |
val screxp1_ = str2term "Take (nth_ 1 (rb_::bool list))";
|
|
wneuper@3737
|
702 |
val screxp1 = subst_atomic [(rb_, rb)] screxp1_; term2str screxp1;
|
|
wneuper@3737
|
703 |
val Some (b1,_) = rewrite_set_ Isac.thy false srls2 screxp1; term2str b1;
|
|
wneuper@3737
|
704 |
if term2str b1 = "Take (y 0 = 0)" then ()
|
|
wneuper@3737
|
705 |
else raise error "biegelinie.sml: rew. Bieglie2 --1";
|
|
wneuper@3737
|
706 |
val b1 = str2term "(y 0 = 0)";
|
|
wneuper@3737
|
707 |
|
|
wneuper@3737
|
708 |
"--- script expression 2";
|
|
wneuper@3737
|
709 |
val screxp2_ = str2term "filter (sameFunId (lhs b1_)) funs_";
|
|
wneuper@3737
|
710 |
val b1_ = str2term "b1_::bool";
|
|
wneuper@3737
|
711 |
val screxp2 = subst_atomic [(b1_,b1),(funs_,funs)] screxp2_; term2str screxp2;
|
|
wneuper@3737
|
712 |
val Some (fs,_) = rewrite_set_ Isac.thy false srls2 screxp2; term2str fs;
|
|
wneuper@3737
|
713 |
if term2str fs = "[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)]" then ()
|
|
wneuper@3737
|
714 |
else raise error "biegelinie.sml: rew. Bieglie2 --2";
|
|
wneuper@3737
|
715 |
|
|
wneuper@3737
|
716 |
"--- script expression 3";
|
|
wneuper@3737
|
717 |
val screxp3_ = str2term "SubProblem (Biegelinie_,[makeFunctionTo,equation],\
|
|
wneuper@3737
|
718 |
\ [Equation,fromFunction]) \
|
|
wneuper@3737
|
719 |
\ [bool_ (hd fs_), bool_ b1_]";
|
|
wneuper@3737
|
720 |
val fs_ = str2term "fs_::bool list";
|
|
wneuper@3737
|
721 |
val screxp3 = subst_atomic [(fs_,fs),(b1_,b1)] screxp3_;
|
|
wneuper@3737
|
722 |
writeln (term2str screxp3);
|
|
wneuper@3737
|
723 |
val Some (equ,_) = rewrite_set_ Isac.thy false srls2 screxp3;
|
|
wneuper@3737
|
724 |
if term2str equ = "SubProblem\n (Biegelinie_, [makeFunctionTo, equation], [Equation, fromFunction])\n [bool_\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)),\n bool_ (y 0 = 0)]" then ()
|
|
wneuper@3737
|
725 |
else raise error "biegelinie.sml: rew. Bieglie2 --3";
|
|
wneuper@3737
|
726 |
writeln (term2str equ);
|
|
wneuper@3737
|
727 |
(*SubProblem
|
|
wneuper@3737
|
728 |
(Biegelinie_, [makeFunctionTo, equation], [Equation, fromFunction])
|
|
wneuper@3737
|
729 |
[bool_
|
|
wneuper@3737
|
730 |
(y x =
|
|
wneuper@3737
|
731 |
c_4 + c_3 * x +
|
|
wneuper@3737
|
732 |
1 / (-1 * EI) *
|
|
wneuper@3737
|
733 |
(c_2 / 2 * x ^^^ 2 + c / 6 * x ^^^ 3 + -1 * q_0 / 24 * x ^^^ 4)),
|
|
wneuper@3737
|
734 |
bool_ (y 0 = 0)]*)
|
|
wneuper@3737
|
735 |
show_types := false;
|
|
wneuper@3737
|
736 |
|
|
wneuper@3737
|
737 |
|
|
wneuper@3737
|
738 |
"----- execute script by interpreter: setzeRandbedingungenEin";
|
|
wneuper@3737
|
739 |
val fmz = ["Funktionen [Q x = c + -1 * q_0 * x,\
|
|
wneuper@3737
|
740 |
\M_b x = c_2 + c * x + -1 * q_0 / 2 * x ^^^ 2,\
|
|
wneuper@3737
|
741 |
\y' x = c_3 + 1 / (-1 * EI) * (c_2 * x + c / 2 * x ^^^ 2 + -1 * q_0 / 6 * x ^^^ 3),\
|
|
wneuper@3737
|
742 |
\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)]",
|
|
wneuper@3737
|
743 |
"Randbedingungen [y 0 = 0, y L = 0, M_b 0 = 0, M_b L = 0]",
|
|
wneuper@3737
|
744 |
"Gleichungen equs___"];
|
|
wneuper@3737
|
745 |
val (dI',pI',mI') = ("Biegelinie.thy", ["setzeRandbedingungen","Biegelinien"],
|
|
wneuper@3737
|
746 |
["Biegelinien","setzeRandbedingungenEin"]);
|
|
wneuper@3737
|
747 |
val p = e_pos'; val c = [];
|
|
wneuper@3737
|
748 |
val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
|
|
wneuper@3737
|
749 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
|
wneuper@3737
|
750 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
|
wneuper@3737
|
751 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
|
wneuper@3737
|
752 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
|
wneuper@3737
|
753 |
|
|
wneuper@3737
|
754 |
"--- before 1.subpbl [Equation, fromFunction]";
|
|
wneuper@3737
|
755 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
|
wneuper@3737
|
756 |
case nxt of (_, Apply_Method ["Biegelinien", "setzeRandbedingungenEin"])=>()
|
|
wneuper@3737
|
757 |
| _ => raise error "biegelinie.sml: met setzeRandbed*Ein aa";
|
|
wneuper@3737
|
758 |
"----- Randbedingung y 0 = 0 in SUBpbl with met [Equation, fromFunction]";
|
|
wneuper@3737
|
759 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
|
wneuper@3737
|
760 |
if (#1 o (get_obj g_fmz pt)) (fst p) =
|
|
wneuper@3737
|
761 |
["functionEq\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))",
|
|
wneuper@3737
|
762 |
"substitution (y 0 = 0)", "equality equ___"] then ()
|
|
wneuper@3737
|
763 |
else raise error "biegelinie.sml met setzeRandbed*Ein bb";
|
|
wneuper@3737
|
764 |
(writeln o istate2str) (get_istate pt p);
|
|
wneuper@3737
|
765 |
"--- after 1.subpbl [Equation, fromFunction]";
|
|
wneuper@3737
|
766 |
|
|
wneuper@3737
|
767 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
|
wneuper@3737
|
768 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
|
wneuper@3737
|
769 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
|
wneuper@3737
|
770 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
|
wneuper@3737
|
771 |
case nxt of (_, Apply_Method["Equation", "fromFunction"]) => ()
|
|
wneuper@3737
|
772 |
| _ => raise error "biegelinie.sml met2 ff";
|
|
wneuper@3737
|
773 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f =
|
|
wneuper@3737
|
774 |
"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)";
|
|
wneuper@3737
|
775 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
|
wneuper@3737
|
776 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
|
wneuper@3737
|
777 |
case nxt of (_, Check_Postcond ["makeFunctionTo", "equation"]) => ()
|
|
wneuper@3737
|
778 |
| _ => raise error "biegelinie.sml met2 gg";
|
|
wneuper@3737
|
779 |
|
|
wneuper@3737
|
780 |
"--- before 2.subpbl [Equation, fromFunction]";
|
|
wneuper@3737
|
781 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f = "0 = c_4 + 0 / (-1 * EI)" ;
|
|
wneuper@3737
|
782 |
case nxt of (_,Subproblem (_, ["makeFunctionTo", "equation"])) => ()
|
|
wneuper@3737
|
783 |
| _ => raise error "biegelinie.sml met2 hh";
|
|
wneuper@3737
|
784 |
"--- after 1st arrival at 2.subpbl [Equation, fromFunction]";
|
|
wneuper@3737
|
785 |
|
|
wneuper@3737
|
786 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
|
wneuper@3737
|
787 |
if (#1 o (get_obj g_fmz pt)) (fst p) =
|
|
wneuper@3737
|
788 |
["functionEq\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))",
|
|
wneuper@3737
|
789 |
"substitution (y L = 0)", "equality equ___"] then ()
|
|
wneuper@3737
|
790 |
else raise error "biegelinie.sml metsetzeRandbed*Ein bb ";
|
|
wneuper@3737
|
791 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
|
wneuper@3737
|
792 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
|
wneuper@3737
|
793 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
|
wneuper@3737
|
794 |
|
|
wneuper@3737
|
795 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
|
wneuper@3737
|
796 |
case nxt of (_, Apply_Method["Equation", "fromFunction"]) => ()
|
|
wneuper@3737
|
797 |
| _ => raise error "biegelinie.sml met2 ii";
|
|
wneuper@3737
|
798 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f = "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)";
|
|
wneuper@3737
|
799 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f = "y L =\nc_4 + c_3 * L +\n1 / (-1 * EI) *\n(c_2 / 2 * L ^^^ 2 + c / 6 * L ^^^ 3 + -1 * q_0 / 24 * L ^^^ 4)";
|
|
wneuper@3737
|
800 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f = "0 =\nc_4 + c_3 * L +\n1 / (-1 * EI) *\n(c_2 / 2 * L ^^^ 2 + c / 6 * L ^^^ 3 + -1 * q_0 / 24 * L ^^^ 4)";
|
|
wneuper@3737
|
801 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f = "0 =\nc_4 + L * c_3 +\n(12 * L ^^^ 2 * c_2 + 4 * L ^^^ 3 * c + -1 * L ^^^ 4 * q_0) / (-24 * EI)" ;
|
|
wneuper@3737
|
802 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f = "0 =\nc_4 + L * c_3 +\n(12 * L ^^^ 2 * c_2 + 4 * L ^^^ 3 * c + -1 * L ^^^ 4 * q_0) / (-24 * EI)";
|
|
wneuper@3737
|
803 |
case nxt of (_,Subproblem (_, ["makeFunctionTo", "equation"])) => ()
|
|
wneuper@3737
|
804 |
| _ => raise error "biegelinie.sml met2 jj";
|
|
wneuper@3737
|
805 |
|
|
wneuper@3737
|
806 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
|
wneuper@3737
|
807 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
|
wneuper@3737
|
808 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
|
wneuper@3737
|
809 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
|
wneuper@3737
|
810 |
case nxt of (_, Apply_Method ["Equation", "fromFunction"])=>()
|
|
wneuper@3737
|
811 |
| _ => raise error "biegelinie.sml met2 kk";
|
|
wneuper@3737
|
812 |
|
|
wneuper@3737
|
813 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f = "M_b x = c_2 + c * x + -1 * q_0 / 2 * x ^^^ 2"(*true*);
|
|
wneuper@3737
|
814 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f = "0 = c_2 + c * 0 + -1 * q_0 / 2 * 0 ^^^ 2";
|
|
wneuper@3737
|
815 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f = "0 = c_2";
|
|
wneuper@3737
|
816 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f = "0 = c_2";
|
|
wneuper@3737
|
817 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
|
wneuper@3737
|
818 |
case nxt of (_,Subproblem (_, ["makeFunctionTo", "equation"])) => ()
|
|
wneuper@3737
|
819 |
| _ => raise error "biegelinie.sml met2 ll";
|
|
wneuper@3737
|
820 |
|
|
wneuper@3737
|
821 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
|
wneuper@3737
|
822 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
|
wneuper@3737
|
823 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
|
wneuper@3737
|
824 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
|
wneuper@3737
|
825 |
case nxt of (_, Apply_Method ["Equation", "fromFunction"])=>()
|
|
wneuper@3737
|
826 |
| _ => raise error "biegelinie.sml met2 mm";
|
|
wneuper@3737
|
827 |
|
|
wneuper@3737
|
828 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f = "M_b x = c_2 + c * x + -1 * q_0 / 2 * x ^^^ 2";
|
|
wneuper@3737
|
829 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f = "M_b L = c_2 + c * L + -1 * q_0 / 2 * L ^^^ 2";
|
|
wneuper@3737
|
830 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f = "0 = c_2 + c * L + -1 * q_0 / 2 * L ^^^ 2";
|
|
wneuper@3737
|
831 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f = "0 = (2 * c_2 + 2 * L * c + -1 * L ^^^ 2 * q_0) / 2";
|
|
wneuper@3737
|
832 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f = "0 = (2 * c_2 + 2 * L * c + -1 * L ^^^ 2 * q_0) / 2";
|
|
wneuper@3737
|
833 |
case nxt of (_, Check_Postcond ["setzeRandbedingungen", "Biegelinien"]) => ()
|
|
wneuper@3737
|
834 |
| _ => raise error "biegelinie.sml met2 nn";
|
|
wneuper@3737
|
835 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
|
wneuper@3737
|
836 |
if nxt = ("End_Proof'", End_Proof') andalso f2str f =
|
|
wneuper@3737
|
837 |
"[0 = c_4,\n 0 =\n c_4 + L * c_3 +\n (12 * L ^^^ 2 * c_2 + 4 * L ^^^ 3 * c + -1 * L ^^^ 4 * q_0) / (-24 * EI),\n 0 = c_2, 0 = (2 * c_2 + 2 * L * c + -1 * L ^^^ 2 * q_0) / 2]" then ()
|
|
wneuper@3737
|
838 |
else raise error "biegelinie.sml met2 oo";
|
|
wneuper@3737
|
839 |
|
|
wneuper@3737
|
840 |
(*
|
|
wneuper@3737
|
841 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
|
|
wneuper@3737
|
842 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
|
wneuper@3737
|
843 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
|
wneuper@3737
|
844 |
*)
|
|
wneuper@3737
|
845 |
|
|
wneuper@3879
|
846 |
"----------- method [Biegelinien,setzeRandbedingungenEin]FAST ----";
|
|
wneuper@3879
|
847 |
"----------- method [Biegelinien,setzeRandbedingungenEin]FAST ----";
|
|
wneuper@3879
|
848 |
"----------- method [Biegelinien,setzeRandbedingungenEin]FAST ----";
|
|
wneuper@3879
|
849 |
(*---^^^-OK-----------------------------------------------------------------*)
|
|
wneuper@3879
|
850 |
(*---vvv-NOTok--------------------------------------------------------------*)
|
|
wneuper@3879
|
851 |
val str =
|
|
wneuper@3879
|
852 |
"Script SetzeRandbedScript (funs_::bool list) (rb_::bool list) = \
|
|
wneuper@3879
|
853 |
\ (let b1_ = nth_ 1 rb_; \
|
|
wneuper@3879
|
854 |
\ (fs_::bool list) = filter_sameFunId (lhs b1_) funs_; \
|
|
wneuper@3879
|
855 |
\ (e1_::bool) = \
|
|
wneuper@3879
|
856 |
\ (SubProblem (Biegelinie_,[makeFunctionTo,equation],\
|
|
wneuper@3879
|
857 |
\ [Equation,fromFunction]) \
|
|
wneuper@3879
|
858 |
\ [bool_ (hd fs_), bool_ b1_]) \
|
|
wneuper@3879
|
859 |
\ in [e1_,e2_,e3_,e4_])"
|
|
wneuper@3879
|
860 |
;
|
|
wneuper@3879
|
861 |
val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
|
|
wneuper@3879
|
862 |
(*---vvv-NOTok--------------------------------------------------------------*)
|
|
wneuper@3879
|
863 |
val str =
|
|
wneuper@3879
|
864 |
"Script SetzeRandbedScript (funs_::bool list) (rb_::bool list) = \
|
|
wneuper@3879
|
865 |
\ (let b1_ = nth_ 1 rb_; \
|
|
wneuper@3879
|
866 |
\ fs_ = filter_sameFunId (lhs b1_) funs_; \
|
|
wneuper@3879
|
867 |
\ (e1_::bool) = \
|
|
wneuper@3879
|
868 |
\ (SubProblem (Biegelinie_,[makeFunctionTo,equation],\
|
|
wneuper@3879
|
869 |
\ [Equation,fromFunction]) \
|
|
wneuper@3879
|
870 |
\ [bool_ (hd fs_), bool_ b1_]); \
|
|
wneuper@3879
|
871 |
\ b2_ = nth_ 2 rb_; \
|
|
wneuper@3879
|
872 |
\ fs_ = filter_sameFunId (lhs b2_) funs_; \
|
|
wneuper@3879
|
873 |
\ (e2_::bool) = \
|
|
wneuper@3879
|
874 |
\ (SubProblem (Biegelinie_,[makeFunctionTo,equation],\
|
|
wneuper@3879
|
875 |
\ [Equation,fromFunction]) \
|
|
wneuper@3879
|
876 |
\ [bool_ (hd fs_), bool_ b2_]); \
|
|
wneuper@3879
|
877 |
\ b3_ = nth_ 3 rb_; \
|
|
wneuper@3879
|
878 |
\ fs_ = filter_sameFunId (lhs b3_) funs_; \
|
|
wneuper@3879
|
879 |
\ (e3_::bool) = \
|
|
wneuper@3879
|
880 |
\ (SubProblem (Biegelinie_,[makeFunctionTo,equation],\
|
|
wneuper@3879
|
881 |
\ [Equation,fromFunction]) \
|
|
wneuper@3879
|
882 |
\ [bool_ (hd fs_), bool_ b3_]); \
|
|
wneuper@3879
|
883 |
\ b4_ = nth_ 4 rb_; \
|
|
wneuper@3879
|
884 |
\ fs_ = filter_sameFunId (lhs b4_) funs_; \
|
|
wneuper@3879
|
885 |
\ (e4_::bool) = \
|
|
wneuper@3879
|
886 |
\ (SubProblem (Biegelinie_,[makeFunctionTo,equation],\
|
|
wneuper@3879
|
887 |
\ [Equation,fromFunction]) \
|
|
wneuper@3879
|
888 |
\ [bool_ (hd fs_), bool_ b4_]) \
|
|
wneuper@3879
|
889 |
\ in [e1_,e2_,e3_,e4_])"
|
|
wneuper@3879
|
890 |
;
|
|
wneuper@3879
|
891 |
val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
|
|
wneuper@3879
|
892 |
|
|
wneuper@3879
|
893 |
|
|
wneuper@3879
|
894 |
|
|
wneuper@3879
|
895 |
"----------- IntegrierenUndKonstanteBestimmen2: Bsp.7.70. --------";
|
|
wneuper@3879
|
896 |
"----------- IntegrierenUndKonstanteBestimmen2: Bsp.7.70. --------";
|
|
wneuper@3879
|
897 |
"----------- IntegrierenUndKonstanteBestimmen2: Bsp.7.70. --------";
|
|
wneuper@3737
|
898 |
"----- script ";
|
|
wneuper@3737
|
899 |
val str =
|
|
wneuper@3849
|
900 |
"Script Belastung2BiegelScript (q__::real) (v_::real) = \
|
|
wneuper@3852
|
901 |
\ (let q___ = Take (q_ v_ = q__); \
|
|
wneuper@3849
|
902 |
\ q___ = ((Rewrite sym_real_minus_eq_cancel True) @@ \
|
|
wneuper@3849
|
903 |
\ (Rewrite Belastung_Querkraft True)) q___; \
|
|
wneuper@3737
|
904 |
\ (Q__:: bool) = \
|
|
wneuper@3737
|
905 |
\ (SubProblem (Biegelinie_,[named,integrate,function], \
|
|
wneuper@3789
|
906 |
\ [diff,integration,named]) \
|
|
wneuper@3849
|
907 |
\ [real_ (rhs q___), real_ v_, real_real_ Q]); \
|
|
wneuper@3737
|
908 |
\ M__ = Rewrite Querkraft_Moment True Q__; \
|
|
wneuper@3737
|
909 |
\ (M__::bool) = \
|
|
wneuper@3737
|
910 |
\ (SubProblem (Biegelinie_,[named,integrate,function], \
|
|
wneuper@3789
|
911 |
\ [diff,integration,named]) \
|
|
wneuper@3737
|
912 |
\ [real_ (rhs M__), real_ v_, real_real_ M_b]); \
|
|
wneuper@3737
|
913 |
\ N__ = ((Rewrite Moment_Neigung False) @@ \
|
|
wneuper@3737
|
914 |
\ (Rewrite make_fun_explicit False)) M__; \
|
|
wneuper@3737
|
915 |
\ (N__:: bool) = \
|
|
wneuper@3737
|
916 |
\ (SubProblem (Biegelinie_,[named,integrate,function], \
|
|
wneuper@3789
|
917 |
\ [diff,integration,named]) \
|
|
wneuper@3737
|
918 |
\ [real_ (rhs N__), real_ v_, real_real_ y']); \
|
|
wneuper@3737
|
919 |
\ (B__:: bool) = \
|
|
wneuper@3737
|
920 |
\ (SubProblem (Biegelinie_,[named,integrate,function], \
|
|
wneuper@3789
|
921 |
\ [diff,integration,named]) \
|
|
wneuper@3737
|
922 |
\ [real_ (rhs N__), real_ v_, real_real_ y]) \
|
|
wneuper@3737
|
923 |
\ in [Q__, M__, N__, B__])"
|
|
wneuper@3737
|
924 |
;
|
|
wneuper@3737
|
925 |
val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
|
|
wneuper@3737
|
926 |
(*---^^^-OK-----------------------------------------------------------------*)
|
|
wneuper@3737
|
927 |
(*---vvv-NOTok--------------------------------------------------------------*)
|
|
wneuper@3737
|
928 |
|
|
wneuper@3737
|
929 |
|
|
wneuper@3737
|
930 |
"----- Bsp 7.70 with me";
|
|
wneuper@3737
|
931 |
val fmz = ["Traegerlaenge L","Streckenlast q_0","Biegelinie y",
|
|
wneuper@3737
|
932 |
"Randbedingungen [y 0 = 0, y L = 0, M_b 0 = 0, M_b L = 0]",
|
|
wneuper@3737
|
933 |
"FunktionsVariable x"];
|
|
wneuper@3737
|
934 |
val (dI',pI',mI') = ("Biegelinie.thy", ["Biegelinien"],
|
|
wneuper@3737
|
935 |
["IntegrierenUndKonstanteBestimmen2"]);
|
|
wneuper@3737
|
936 |
val p = e_pos'; val c = [];
|
|
wneuper@3737
|
937 |
val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
|
|
wneuper@3737
|
938 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
|
wneuper@3737
|
939 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
|
wneuper@3737
|
940 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
|
wneuper@3737
|
941 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
|
wneuper@3737
|
942 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
|
wneuper@3737
|
943 |
if nxt = ("Apply_Method", Apply_Method ["IntegrierenUndKonstanteBestimmen2"])
|
|
wneuper@3737
|
944 |
then () else raise error "biegelinie.sml met2 a";
|
|
wneuper@3737
|
945 |
|
|
wneuper@3737
|
946 |
(*** actual arg(s) missing for '["(#Find, (Funktionen, funs_))"]' i.e. should be 'copy-named' by '*_._'
|
|
wneuper@3737
|
947 |
... THIS MEANS:
|
|
wneuper@3737
|
948 |
#a# "Script Biegelinie2Script ..
|
|
wneuper@3737
|
949 |
\ ... (SubProblem (Biegelinie_,[vonBelastungZu,Biegelinien], \
|
|
wneuper@3737
|
950 |
\ [Biegelinien,ausBelastung]) \
|
|
wneuper@3849
|
951 |
\ [real_ q__, real_ v_]); \
|
|
wneuper@3737
|
952 |
|
|
wneuper@3737
|
953 |
#b# prep_met ... (["Biegelinien","ausBelastung"],
|
|
wneuper@3849
|
954 |
... ("#Given" ,["Streckenlast q__","FunktionsVariable v_"]),
|
|
wneuper@3849
|
955 |
"Script Belastung2BiegelScript (q__::real) (v_::real) = \
|
|
wneuper@3737
|
956 |
|
|
wneuper@3849
|
957 |
#a#b# BOTH HAVE 2 ARGUMENTS q__ and v_ ...OK
|
|
wneuper@3737
|
958 |
##########################################################################
|
|
wneuper@3737
|
959 |
BUT THE (#Find, (Funktionen, funs_)) IS NOT COPYNAMED BY funs___ !!!3*_!!!
|
|
wneuper@3737
|
960 |
##########################################################################*)
|
|
wneuper@3737
|
961 |
"further 'me' see ----- SubProblem (_,[vonBelastungZu,Biegelinien] -------\
|
|
wneuper@3737
|
962 |
\ ----- SubProblem (_,[setzeRandbedingungen,Biegelinien] -";
|
|
wneuper@3737
|
963 |
|
|
wneuper@3737
|
964 |
"----- Bsp 7.70 with autoCalculate";
|
|
wneuper@3737
|
965 |
states:=[];
|
|
wneuper@3737
|
966 |
CalcTree [(["Traegerlaenge L","Streckenlast q_0","Biegelinie y",
|
|
wneuper@3737
|
967 |
"Randbedingungen [Q 0 = q_0 * L, M_b L = 0, y 0 = 0, y' 0 = 0]",
|
|
wneuper@3737
|
968 |
"FunktionsVariable x"],
|
|
wneuper@3737
|
969 |
("Biegelinie.thy", ["Biegelinien"],
|
|
wneuper@3737
|
970 |
["IntegrierenUndKonstanteBestimmen2"]))];
|
|
wneuper@3737
|
971 |
moveActiveRoot 1;
|
|
wneuper@3737
|
972 |
autoCalculate 1 CompleteCalc;
|
|
wneuper@3879
|
973 |
val ((pt,p),_) = get_calc 1; show_pt pt;
|
|
wneuper@3879
|
974 |
if p = ([], Res) andalso term2str (get_obj g_res pt (fst p)) =
|
|
wneuper@3879
|
975 |
"y x =\n-6 * q_0 * L ^^^ 2 / (-24 * EI) * x ^^^ 2 +\n4 * L * q_0 / (-24 * EI) * x ^^^ 3 +\n-1 * q_0 / (-24 * EI) * x ^^^ 4" then ()
|
|
wneuper@3879
|
976 |
else raise error "biegelinie.sml: diff.behav.7.70 with autoCalculate";
|
|
wneuper@3879
|
977 |
|
|
wneuper@3737
|
978 |
val is = get_istate pt ([],Res); writeln (istate2str is);
|
|
wneuper@3737
|
979 |
val t = str2term " last \
|
|
wneuper@3737
|
980 |
\[Q x = L * q_0 + -1 * q_0 * x, \
|
|
wneuper@3737
|
981 |
\ M_b x = -1 * q_0 * L ^^^ 2 / 2 + q_0 * L / 1 * x + -1 * q_0 / 2 * x ^^^ 2,\
|
|
wneuper@3737
|
982 |
\ y' x = \
|
|
wneuper@3737
|
983 |
\ -3 * q_0 * L ^^^ 2 / (-6 * EI) * x + 3 * L * q_0 / (-6 * EI) * x ^^^ 2 +\
|
|
wneuper@3737
|
984 |
\ -1 * q_0 / (-6 * EI) * x ^^^ 3, \
|
|
wneuper@3737
|
985 |
\ y x = \
|
|
wneuper@3737
|
986 |
\ -6 * q_0 * L ^^^ 2 / (-24 * EI) * x ^^^ 2 + \
|
|
wneuper@3737
|
987 |
\ 4 * L * q_0 / (-24 * EI) * x ^^^ 3 + \
|
|
wneuper@3737
|
988 |
\ -1 * q_0 / (-24 * EI) * x ^^^ 4]";
|
|
wneuper@3737
|
989 |
val srls = append_rls "erls_IntegrierenUndK.." e_rls
|
|
wneuper@3737
|
990 |
[Calc("Tools.rhs", eval_rhs"eval_rhs_"),
|
|
wneuper@3737
|
991 |
Calc ("Atools.ident",eval_ident "#ident_"),
|
|
wneuper@3737
|
992 |
Thm ("last_thmI",num_str last_thmI),
|
|
wneuper@3737
|
993 |
Thm ("if_True",num_str if_True),
|
|
wneuper@3737
|
994 |
Thm ("if_False",num_str if_False)
|
|
wneuper@3737
|
995 |
]
|
|
wneuper@3737
|
996 |
;
|
|
wneuper@3737
|
997 |
val t = str2term "last [1,2,3,4]";
|
|
wneuper@3737
|
998 |
trace_rewrite := true;
|
|
wneuper@3737
|
999 |
val Some (e1__,_) = rewrite_set_ thy false srls t;
|
|
wneuper@3737
|
1000 |
trace_rewrite := false;
|
|
wneuper@3737
|
1001 |
term2str e1__;
|
|
wneuper@3737
|
1002 |
|
|
wneuper@3737
|
1003 |
trace_script := true;
|
|
wneuper@3737
|
1004 |
trace_script := false;
|
|
wneuper@3737
|
1005 |
|
|
wneuper@3737
|
1006 |
|
|
wneuper@3737
|
1007 |
"----------- investigate normalforms in biegelinien --------------";
|
|
wneuper@3737
|
1008 |
"----------- investigate normalforms in biegelinien --------------";
|
|
wneuper@3737
|
1009 |
"----------- investigate normalforms in biegelinien --------------";
|
|
wneuper@3737
|
1010 |
"----- coming from integration:";
|
|
wneuper@3737
|
1011 |
val Q = str2term "Q x = c + -1 * q_0 * x";
|
|
wneuper@3737
|
1012 |
val M_b = str2term "M_b x = c_2 + c * x + -1 * q_0 / 2 * x ^^^ 2";
|
|
wneuper@3737
|
1013 |
val y' = str2term "y' x = c_3 + 1 / (-1 * EI) * (c_2 * x + c / 2 * x ^^^ 2 + -1 * q_0 / 6 * x ^^^ 3)";
|
|
wneuper@3737
|
1014 |
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)";
|
|
wneuper@3737
|
1015 |
(*^^^ 1 / (-1 * EI) NOT distributed - ok! ^^^^^^^^^^^^^^^^^^^^^^^*)
|
|
wneuper@3737
|
1016 |
|
|
wneuper@3737
|
1017 |
"----- functions comming from:";
|