updated "op +", "op -", "op *". "HOL.divide" in src & test
find . -type f -exec sed -i s/"\"op +\""/"\"Groups.plus_class.plus\""/g {} \;
find . -type f -exec sed -i s/"\"op -\""/"\"Groups.minus_class.minus\""/g {} \;
find . -type f -exec sed -i s/"\"op *\""/"\"Groups.times_class.times\""/g {} \;
find . -type f -exec sed -i s/"\"HOL.divide\""/"\"Rings.inverse_class.divide\""/g {} \;
2 author: Walther Neuper 050826
3 (c) due to copyright terms
5 use"../smltest/IsacKnowledge/biegelinie.sml";
8 val thy = Biegelinie.thy;
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 "-----------------------------------------------------------------";
30 "----------- the rules -------------------------------------------";
31 "----------- the rules -------------------------------------------";
32 "----------- the rules -------------------------------------------";
33 fun str2term str = (term_of o the o (parse Biegelinie.thy)) str;
34 fun term2s t = Syntax.string_of_term (thy2ctxt' "Biegelinie") t;
36 fst (the (rewrite_ Biegelinie.thy tless_true e_rls true thm str));
38 val t = rewrit Belastung_Querkraft (str2term "- q_ x = - q_0"); term2s t;
39 if term2s t = "Q' x = - q_0" then ()
40 else raise error "/biegelinie.sml: Belastung_Querkraft";
42 val t = rewrit Querkraft_Moment (str2term "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";
46 val t = rewrit Moment_Neigung (str2term "M_b x = -q_0 * x^^^2/2 + q_0/2 *L*x");
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";
52 "----------- Script [IntegrierenUndKonstanteBestimmen] -----------";
53 "----------- Script [IntegrierenUndKonstanteBestimmen] -----------";
54 "----------- Script [IntegrierenUndKonstanteBestimmen] -----------";
56 "Script BiegelinieScript \
57 \(l_::real) (q__::real) (v_v::real) (b_::real=>real) \
58 \(rb_::bool list) (rm_::bool list) = \
59 \ (let q___ = Take (q_ v_v = q__); \
60 \ q___ = ((Rewrite sym_real_minus_eq_cancel True) @@ \
61 \ (Rewrite Belastung_Querkraft True)) q___; \
63 \ (SubProblem (Biegelinie_,[named,integrate,function], \
64 \ [diff,integration,named]) \
65 \ [REAL (rhs q___), REAL v_v, real_REAL Q]); \
66 \ Q__ = Rewrite Querkraft_Moment True Q__; \
68 \ (SubProblem (Biegelinie_,[named,integrate,function], \
69 \ [diff,integration,named]) \
70 \ [REAL (rhs Q__), REAL v_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__ ; \
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]]); \
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 ------------------------*)
92 \ (SubProblem (Biegelinie_,[named,integrate,function], \
93 \ [diff,integration,named]) \
94 \ [REAL (rhs M__), REAL v_v, real_REAL y']); \
96 \ (SubProblem (Biegelinie_,[named,integrate,function], \
97 \ [diff,integration,named]) \
98 \ [REAL (rhs N__), REAL v_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__ ; \
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]]); \
112 \ B__ = ((Substitute c_1_2__) @@ \
113 \ (Rewrite_Set_Inst [(bdv, x)] make_ratpoly_in False)) B__ \
116 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
117 (*---^^^-OK-----------------------------------------------------------------*)
118 (*---vvv-NOTok--------------------------------------------------------------*)
122 (* use"../smltest/IsacKnowledge/biegelinie.sml";
125 "----------- IntegrierenUndKonstanteBestimmen by rewriting -------";
126 "----------- IntegrierenUndKonstanteBestimmen by rewriting -------";
127 "----------- IntegrierenUndKonstanteBestimmen by rewriting -------";
128 val t = str2term "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;
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..",
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("Groups.plus_class.plus", eval_binop "#add_")
147 srls = Erls, calc = [],
148 rules = [Thm ("nth_Cons_",num_str @{thm nth_Cons_}),
149 Calc("Groups.plus_class.plus", eval_binop "#add_"),
150 Thm ("nth_Nil_",num_str @{thm 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")
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";
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_";
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)";
172 trace_rewrite:=false;
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"];
184 ("Biegelinie",["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;
194 val pits = get_obj g_pbl pt (fst p);writeln (itms2str_ ctxt pits);
195 (*if itms2str_ ctxt pits = ... all 5 model-items*)
196 val mits = get_obj g_met pt (fst p); writeln (itms2str_ ctxt mits);
197 if itms2str_ ctxt mits = "[]" then ()
198 else raise error "biegelinie.sml: Bsp 7.27 #2";
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_ ctxt mits);
205 (*if itms2str_ ctxt mits = ... all 6 guard-items*)
206 case nxt of (_, Apply_Method ["IntegrierenUndKonstanteBestimmen"]) => ()
207 | _ => raise error "biegelinie.sml: Bsp 7.27 #4b";
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;
216 (_,Subproblem ("Biegelinie", ["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;
228 ("Check_Postcond", Check_Postcond ["named", "integrate", "function"]) => ()
229 | _ => raise error "biegelinie.sml: Bsp 7.27 #5a";
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;
234 (_, Subproblem ("Biegelinie", ["named", "integrate", "function"]))=>()
235 | _ => raise error "biegelinie.sml: Bsp 7.27 #5b";
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";
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..*);
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";
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";
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";
262 (*val nxt = (+, Subproblem ("Biegelinie", ["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";
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";
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;
302 (_, Subproblem ("Biegelinie", ["named", "integrate", "function"]))=>()
303 | _ => raise error "biegelinie.sml: Bsp 7.27 #13";
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";
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;
316 (_, Check_Postcond ["named", "integrate", "function"]) => ()
317 | _ => raise error "biegelinie.sml: Bsp 7.27 #15";
319 val (p,_,f,nxt,_,pt) = me nxt p c pt; 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";
324 (_, Subproblem ("Biegelinie", ["named", "integrate", "function"]))=>()
325 | _ => raise error "biegelinie.sml: Bsp 7.27 #16";
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";
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;
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";
341 (_, Check_Postcond ["named", "integrate", "function"]) => ()
342 | _ => raise error "biegelinie.sml: Bsp 7.27 #18";
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;
352 ("Biegelinie", ["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";
370 ("Biegelinie", ["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";
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;
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";
404 (* use"../smltest/IsacKnowledge/biegelinie.sml";
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 +
449 "----------- Bsp 7.27 autoCalculate ------------------------------";
450 "----------- Bsp 7.27 autoCalculate ------------------------------";
451 "----------- Bsp 7.27 autoCalculate ------------------------------";
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"],
458 ["MomentBestimmte","Biegelinien"],
459 ["IntegrierenUndKonstanteBestimmen"]))];
461 autoCalculate 1 CompleteCalcHead;
463 fetchProposedTactic 1 (*->"Apply_Method" IntegrierenUndKonstanteBestimmen*);
465 > val (_,Apply_Method' (_, NONE, ScrState is), _)::_ = tacis;
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";
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";
481 val (unc, del, gen) = (([],Pbl), ([],Pbl), ([],Res));
482 getFormulaeFromTo 1 unc gen 1 (*only level 1*) false;
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"]*);
494 "----------- SubProblem (_,[vonBelastungZu,Biegelinien] ----------";
495 "----------- SubProblem (_,[vonBelastungZu,Biegelinien] ----------";
496 "----------- SubProblem (_,[vonBelastungZu,Biegelinien] ----------";
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", ["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";
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";
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;
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";
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";
575 "----------- SubProblem (_,[setzeRandbedingungen,Biegelinien] ----";
576 "----------- SubProblem (_,[setzeRandbedingungen,Biegelinien] ----";
577 "----------- SubProblem (_,[setzeRandbedingungen,Biegelinien] ----";
579 "Script Function2Equality (fun_::bool) (sub_::bool) =\
582 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
584 "Script Function2Equality (fun_::bool) (sub_::bool) =\
585 \ (let v_v = argument_in (lhs fun_)\
586 \ in (equ___::bool))"
588 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
590 "Script Function2Equality (fun_::bool) (sub_::bool) =\
591 \ (let v_v = argument_in (lhs fun_);\
592 \ (equ_) = (Substitute [sub_]) fun_\
595 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
597 "Script Function2Equality (fun_::bool) (sub_::bool) =\
598 \ (let v_v = argument_in (lhs fun_);\
599 \ equ_ = (Substitute [sub_]) fun_\
600 \ in (Rewrite_Set_Inst [(bdv, v_v)] make_ratpoly_in False) equ_)"
602 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
603 (*---^^^-OK-----------------------------------------------------------------*)
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_v)] make_ratpoly_in False) equ_)"
614 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
615 (*---vvv-NOTok--------------------------------------------------------------*)
618 val fmz = ["functionEq (M_b x = c_2 + c * x + -1 * q_0 / 2 * x ^^^ 2)",
619 "substitution (M_b L = 0)",
621 val (dI',pI',mI') = ("Biegelinie", ["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;
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";
645 "----------- method [Biegelinien,setzeRandbedingungenEin] + exec -";
646 "----------- method [Biegelinien,setzeRandbedingungenEin] + exec -";
647 "----------- method [Biegelinien,setzeRandbedingungenEin] + exec -";
648 "----- check the scripts syntax";
650 "Script SetzeRandbedScript (funs_::bool list) (beds_::bool list) =\
651 \ (let b1 = Take (nth_ 1 beds_)\
652 \ in (equs_::bool list))"
654 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
656 "Script SetzeRandbedScript (funs_::bool list) (beds_::bool list) =\
657 \ (let b1_ = Take (nth_ 1 beds_); \
658 \ fs_ = filter (sameFunId (lhs b1_)) funs_; \
660 \ in (equs_::bool list))"
662 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
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;
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_; \
676 \ in (equs_::bool list))"
678 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
680 "Script SetzeRandbedScript (funs_::bool list) (rb_::bool list) =\
681 \ (let b1_ = Take (nth_ 1 rb_); \
682 \ fs_ = filter (sameFunId (lhs b1_)) funs_; \
684 \ (SubProblem (Biegelinie_,[makeFunctionTo,equation],\
685 \ [Equation,fromFunction]) \
686 \ [BOOL (hd fs_), BOOL b1_]) \
689 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
691 "Script SetzeRandbedScript (funs_::bool list) (rb_::bool list) =\
692 \ (let b1_ = Take (nth_ 1 rb_); \
693 \ fs_ = filter (sameFunId (lhs b1_)) funs_; \
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_; \
701 \ (SubProblem (Biegelinie_,[makeFunctionTo,equation],\
702 \ [Equation,fromFunction]) \
703 \ [BOOL (hd fs_), BOOL b2_]) \
706 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
707 (*---vvv-NOTok--------------------------------------------------------------*)
708 (*---^^^-OK-----------------------------------------------------------------*)
711 "----- execute script by manual rewriting";
712 (*show_types := true;*)
713 val funs_ = str2term "funs_::bool list";
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]";
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)";
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";
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);
750 (Biegelinie_, [makeFunctionTo, equation], [Equation, fromFunction])
755 (c_2 / 2 * x ^^^ 2 + c / 6 * x ^^^ 3 + -1 * q_0 / 24 * x ^^^ 4)),
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", ["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;
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]";
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";
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]";
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;
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";
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";
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";
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";
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";
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;
869 "----------- method [Biegelinien,setzeRandbedingungenEin]FAST ----";
870 "----------- method [Biegelinien,setzeRandbedingungenEin]FAST ----";
871 "----------- method [Biegelinien,setzeRandbedingungenEin]FAST ----";
872 (*---^^^-OK-----------------------------------------------------------------*)
873 (*---vvv-NOTok--------------------------------------------------------------*)
875 "Script SetzeRandbedScript (funs_::bool list) (rb_::bool list) = \
876 \ (let b1_ = nth_ 1 rb_; \
877 \ (fs_::bool list) = filter_sameFunId (lhs b1_) funs_; \
879 \ (SubProblem (Biegelinie_,[makeFunctionTo,equation],\
880 \ [Equation,fromFunction]) \
881 \ [BOOL (hd fs_), BOOL b1_]) \
882 \ in [e1_,e2_,e3_,e4_])"
884 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
885 (*---vvv-NOTok--------------------------------------------------------------*)
887 "Script SetzeRandbedScript (funs_::bool list) (rb_::bool list) = \
888 \ (let b1_ = nth_ 1 rb_; \
889 \ fs_ = filter_sameFunId (lhs b1_) funs_; \
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_; \
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_; \
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_; \
909 \ (SubProblem (Biegelinie_,[makeFunctionTo,equation],\
910 \ [Equation,fromFunction]) \
911 \ [BOOL (hd fs_), BOOL b4_]) \
912 \ in [e1_,e2_,e3_,e4_])"
914 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
918 "----------- IntegrierenUndKonstanteBestimmen2: Bsp.7.70. --------";
919 "----------- IntegrierenUndKonstanteBestimmen2: Bsp.7.70. --------";
920 "----------- IntegrierenUndKonstanteBestimmen2: Bsp.7.70. --------";
923 "Script Belastung2BiegelScript (q__::real) (v_v::real) = \
924 \ (let q___ = Take (q_ v_v = q__); \
925 \ q___ = ((Rewrite sym_real_minus_eq_cancel True) @@ \
926 \ (Rewrite Belastung_Querkraft True)) q___; \
928 \ (SubProblem (Biegelinie_,[named,integrate,function], \
929 \ [diff,integration,named]) \
930 \ [REAL (rhs q___), REAL v_v, real_REAL Q]); \
931 \ M__ = Rewrite Querkraft_Moment True Q__; \
933 \ (SubProblem (Biegelinie_,[named,integrate,function], \
934 \ [diff,integration,named]) \
935 \ [REAL (rhs M__), REAL v_v, real_REAL M_b]); \
936 \ N__ = ((Rewrite Moment_Neigung False) @@ \
937 \ (Rewrite make_fun_explicit False)) M__; \
939 \ (SubProblem (Biegelinie_,[named,integrate,function], \
940 \ [diff,integration,named]) \
941 \ [REAL (rhs N__), REAL v_v, real_REAL y']); \
943 \ (SubProblem (Biegelinie_,[named,integrate,function], \
944 \ [diff,integration,named]) \
945 \ [REAL (rhs N__), REAL v_v, real_REAL y]) \
946 \ in [Q__, M__, N__, B__])"
948 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
949 (*---^^^-OK-----------------------------------------------------------------*)
950 (*---vvv-NOTok--------------------------------------------------------------*)
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", ["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";
969 (*** actual arg(s) missing for '["(#Find, (Funktionen, funs_))"]' i.e. should be 'copy-named' by '*_._'
971 #a# "Script Biegelinie2Script ..
972 \ ... (SubProblem (Biegelinie_,[vonBelastungZu,Biegelinien], \
973 \ [Biegelinien,ausBelastung]) \
974 \ [REAL q__, REAL v_]); \
976 #b# prep_met ... (["Biegelinien","ausBelastung"],
977 ... ("#Given" ,["Streckenlast q__","FunktionsVariable v_v"]),
978 "Script Belastung2BiegelScript (q__::real) (v_v::real) = \
980 #a#b# BOTH HAVE 2 ARGUMENTS q__ and v_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] -";
987 "----- Bsp 7.70 with autoCalculate";
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", ["Biegelinien"],
993 ["IntegrierenUndKonstanteBestimmen2"]))];
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";
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,\
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, \
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 @{thm last_thmI}),
1016 Thm ("if_True",num_str @{thm if_True}),
1017 Thm ("if_False",num_str @{thm if_False})
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;
1026 trace_script := true;
1027 trace_script := false;
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! ^^^^^^^^^^^^^^^^^^^^^^^*)
1040 "----- functions comming from:";