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