2 author: Walther Neuper 050826
3 (c) due to copyright terms
5 trace_rewrite := false;
6 "-----------------------------------------------------------------";
7 "table of contents -----------------------------------------------";
8 "-----------------------------------------------------------------";
9 "----------- the rules -------------------------------------------";
10 "----------- IntegrierenUndKonstanteBestimmen by rewriting -------";
11 "----------- simplify_leaf for this script -----------------------";
12 "----------- Bsp 7.27 me -----------------------------------------";
13 "----------- Bsp 7.27 autoCalculate ------------------------------";
14 "----------- SubProblem (_,[vonBelastungZu,Biegelinien] ----------";
15 "----------- SubProblem (_,[setzeRandbedingungen,Biegelinien] ----";
16 "----------- method [Biegelinien,setzeRandbedingungenEin] + exec -";
17 "----------- IntegrierenUndKonstanteBestimmen2: Bsp.7.70. --------";
18 "----------- investigate normalforms in biegelinien --------------";
19 "-----------------------------------------------------------------";
20 "-----------------------------------------------------------------";
21 "-----------------------------------------------------------------";
23 val thy = @{theory "Biegelinie"};
24 val ctxt = thy2ctxt' "Biegelinie";
25 fun str2term str = (Thm.term_of o the o (parse thy)) str;
26 fun term2s t = term_to_string'' "Biegelinie" t;
28 fst (the (rewrite_ thy tless_true e_rls true thm str));
30 "----------- the rules -------------------------------------------";
31 "----------- the rules -------------------------------------------";
32 "----------- the rules -------------------------------------------";
33 val t = rewrit @{thm Belastung_Querkraft} (str2term "- qq x = - q_0"); term2s t;
34 if term2s t = "Q' x = - q_0" then ()
35 else error "/biegelinie.sml: Belastung_Querkraft";
37 val t = rewrit @{thm Querkraft_Moment} (str2term "Q x = - q_0 * x + c"); term2s t;
38 if term2s t = "M_b' x = - q_0 * x + c" then ()
39 else error "/biegelinie.sml: Querkraft_Moment";
41 val t = rewrit @{thm Moment_Neigung} (str2term "M_b x = -q_0 * x^^^2/2 + q_0/2 *L*x");
43 if term2s t = "- EI * y'' x = - q_0 * x ^^^ 2 / 2 + q_0 / 2 * L * x" then ()
44 else error "biegelinie.sml: Moment_Neigung";
46 "----------- IntegrierenUndKonstanteBestimmen by rewriting -------";
47 "----------- IntegrierenUndKonstanteBestimmen by rewriting -------";
48 "----------- IntegrierenUndKonstanteBestimmen by rewriting -------";
49 "----------- IntegrierenUndKonstanteBestimmen by rewriting -------";
50 val t = str2term "M_b x = L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2";
51 val t = rewrit @{thm Moment_Neigung} t;
52 if term2s t = "- EI * y'' x = L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2" then ()
53 else error "Moment_Neigung broken";
54 (* was I * ?y'' x = L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2"
55 before declaring "y''" as a constant *)
57 val t = rewrit @{thm make_fun_explicit} t;
58 if term2s t = "y'' x = 1 / - EI * (L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2)" then ()
59 else error "make_fun_explicit broken";
61 "----------- simplify_leaf for this script -----------------------";
62 "----------- simplify_leaf for this script -----------------------";
63 "----------- simplify_leaf for this script -----------------------";
64 val srls = Rls {id="srls_IntegrierenUnd..",
66 rew_ord = ("termlessI",termlessI),
67 erls = append_rls "erls_in_srls_IntegrierenUnd.." e_rls
68 [(*for asm in NTH_CONS ...*)
69 Calc ("Orderings.ord_class.less",eval_equ "#less_"),
70 (*2nd NTH_CONS pushes n+-1 into asms*)
71 Calc("Groups.plus_class.plus", eval_binop "#add_")
73 srls = Erls, calc = [], errpatts = [],
74 rules = [Thm ("NTH_CONS",num_str @{thm NTH_CONS}),
75 Calc("Groups.plus_class.plus", eval_binop "#add_"),
76 Thm ("NTH_NIL",num_str @{thm NTH_NIL}),
77 Calc("Tools.lhs", eval_lhs "eval_lhs_"),
78 Calc("Tools.rhs", eval_rhs "eval_rhs_"),
79 Calc("Atools.argument'_in", eval_argument_in "Atools.argument'_in")
82 val rm_ = str2term"[M_b 0 = 0, M_b L = 0]";
83 val M__ = str2term"M_b x = -1 * x ^^^ 2 / 2 + x * c + c_2";
84 val SOME (e1__,_) = rewrite_set_ thy false srls
85 (str2term "(NTH::[real,bool list]=>bool) 1 " $ rm_);
86 if term2str e1__ = "M_b 0 = 0" then () else error "biegelinie.sml simplify NTH 1 rm_";
89 rewrite_set_ thy false srls
90 (str2term"argument_in (lhs (M_b 0 = 0))");
91 if term2str x1__ = "0" then ()
92 else error "biegelinie.sml simplify argument_in (lhs (M_b 0 = 0)";
94 (*trace_rewrite := true; ..stopped Test_Isac.thy*)
97 "----------- Bsp 7.27 me -----------------------------------------";
98 "----------- Bsp 7.27 me -----------------------------------------";
99 "----------- Bsp 7.27 me -----------------------------------------";
100 val fmz = ["Traegerlaenge L","Streckenlast q_0","Biegelinie y",
101 "RandbedingungenBiegung [y 0 = 0, y L = 0]",
102 "RandbedingungenMoment [M_b 0 = 0, M_b L = 0]",
103 "FunktionsVariable x"];
105 ("Biegelinie",["MomentBestimmte","Biegelinien"],
106 ["IntegrierenUndKonstanteBestimmen"]);
107 val p = e_pos'; val c = [];
108 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
109 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
110 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
111 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
112 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
113 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
115 val pits = get_obj g_pbl pt (fst p);writeln (itms2str_ ctxt pits);
116 (*if itms2str_ ctxt pits = ... all 5 model-items*)
117 val mits = get_obj g_met pt (fst p); writeln (itms2str_ ctxt mits);
118 if itms2str_ ctxt mits = "[]" then ()
119 else error "biegelinie.sml: Bsp 7.27 #2";
121 val (p,_,f,nxt,_,pt) = me nxt p c pt;
122 case nxt of (_,Add_Given "FunktionsVariable x") => ()
123 | _ => error "biegelinie.sml: Bsp 7.27 #4a";
125 val (p,_,f,nxt,_,pt) = me nxt p c pt;
126 val mits = get_obj g_met pt (fst p);writeln (itms2str_ ctxt mits);
127 (*if itms2str_ ctxt mits = ... all 6 guard-items*)
128 case nxt of (_, Apply_Method ["IntegrierenUndKonstanteBestimmen"]) => ()
129 | _ => error "biegelinie.sml: Bsp 7.27 #4b";
131 "===== Apply_Method IntegrierenUndKonstanteBestimmen ============================";
132 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
133 case pt of Nd (PblObj _, [Nd _]) => ((*Apply_Method + Take*))
134 | _ => error "biegelinie.sml: Bsp 7.27 #4c";
135 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
136 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
139 (_,Subproblem ("Biegelinie", ["named", "integrate", "function"])) => ()
140 | _ => error "biegelinie.sml: Bsp 7.27 #4c";
141 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
142 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
143 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
144 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
145 case nxt of (_, Apply_Method ["diff", "integration", "named"]) => ()
146 | _ => error "biegelinie.sml: Bsp 7.27 #5";
147 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
148 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
149 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
151 ("Check_Postcond", Check_Postcond ["named", "integrate", "function"]) => ()
152 | _ => error "biegelinie.sml: Bsp 7.27 #5a";
154 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
155 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
157 (_, Subproblem ("Biegelinie", ["named", "integrate", "function"]))=>()
158 | _ => error "biegelinie.sml: Bsp 7.27 #5b";
160 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
161 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
162 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
163 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
164 case nxt of (_, Apply_Method ["diff", "integration","named"]) => ()
165 | _ => error "biegelinie.sml: Bsp 7.27 #6";
167 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
168 val (p,_,f,nxt,_,pt) = me nxt p c pt(*nxt = Check_Postcond ["named", "int..*);
170 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
171 case nxt of (_, Substitute ["x = 0"]) => ()
172 | _ => error "biegelinie.sml: Bsp 7.27 #7";
174 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
175 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
176 if f2str f = "0 = c_2 + c * 0 + -1 * q_0 / 2 * 0 ^^^ 2" then ()
177 else error "biegelinie.sml: Bsp 7.27 #8";
179 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
180 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
181 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
182 if f2str f = "0 = c_2 + c * L + -1 * q_0 / 2 * L ^^^ 2" then ()
183 else error "biegelinie.sml: Bsp 7.27 #9";
185 (*val nxt = (+, Subproblem ("Biegelinie", ["normalize", ..lin..sys]))*)
186 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
187 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
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;
191 case nxt of (_, Apply_Method ["EqSystem", "normalize", "2x2"]) => ()
192 | _ => error "biegelinie.sml: Bsp 7.27 #10";
194 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
195 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
196 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
197 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
198 (*val nxt = Subproblem ["triangular", "2x2", "LINEAR", "system"]*)
199 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
200 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
201 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
202 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
203 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
204 case nxt of (_, Apply_Method["EqSystem", "top_down_substitution", "2x2"]) => ()
205 | _ => error "biegelinie.sml: Bsp 7.27 #11";
206 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
207 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
208 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
209 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
210 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
211 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
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 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
215 case nxt of (_, Check_Postcond ["normalize", "2x2", "LINEAR", "system"]) => ()
216 | _ => error "biegelinie.sml: Bsp 7.27 #12";
218 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
219 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
220 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
221 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
222 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
223 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
225 (_, Subproblem ("Biegelinie", ["named", "integrate", "function"]))=>()
226 | _ => error "biegelinie.sml: Bsp 7.27 #13";
228 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
229 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
230 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
231 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
232 case nxt of (_, Apply_Method ["diff", "integration", "named"]) => ()
233 | _ => error "biegelinie.sml: Bsp 7.27 #14";
235 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
236 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
237 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
239 (_, Check_Postcond ["named", "integrate", "function"]) => ()
240 | _ => error "biegelinie.sml: Bsp 7.27 #15";
242 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
244 "y' x = c + 1 / (-1 * EI) * (L * q_0 / 4 * x ^^^ 2 + -1 * q_0 / 6 * x ^^^ 3)"
245 then () else error "biegelinie.sml: Bsp 7.27 #16 f";
247 (_, Subproblem ("Biegelinie", ["named", "integrate", "function"]))=>()
248 | _ => error "biegelinie.sml: Bsp 7.27 #16";
250 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
251 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
252 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
253 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
254 case nxt of (_, Apply_Method ["diff", "integration", "named"]) => ()
255 | _ => error "biegelinie.sml: Bsp 7.27 #17";
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;
260 "y x =\nc_2 + c * x +\n\
261 \1 / (-1 * EI) * (L * q_0 / 12 * x ^^^ 3 + -1 * q_0 / 24 * x ^^^ 4)"
262 then () else error "biegelinie.sml: Bsp 7.27 #18 f";
264 (_, Check_Postcond ["named", "integrate", "function"]) => ()
265 | _ => error "biegelinie.sml: Bsp 7.27 #18";
267 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
268 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
269 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
270 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
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;
275 ("Biegelinie", ["normalize", "2x2", "LINEAR", "system"])) => ()
276 | _ => error "biegelinie.sml: Bsp 7.27 #19";
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 val (p,_,f,nxt,_,pt) = me nxt p c pt;
282 case nxt of (_, Apply_Method ["EqSystem", "normalize", "2x2"]) => ()
283 | _ => error "biegelinie.sml: Bsp 7.27 #20";
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 if f2str f = "[c_2 = 0, L * c + c_2 = -1 * q_0 * L ^^^ 4 / (-24 * EI)]" then ()
290 else error "biegelinie.sml: Bsp 7.27 #21 f";
293 ("Biegelinie", ["triangular", "2x2", "LINEAR", "system"])) =>()
294 | _ => error "biegelinie.sml: Bsp 7.27 #21";
295 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
296 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
297 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
298 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
299 val (p,_,f,nxt,_,pt) = me nxt p c pt;
300 case nxt of (_, Apply_Method["EqSystem", "top_down_substitution", "2x2"]) => ()
301 | _ => error "biegelinie.sml: Bsp 7.27 #22";
302 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
303 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
304 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
305 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
306 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
307 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
308 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
309 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
310 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
311 case nxt of (_, Check_Postcond ["normalize", "2x2", "LINEAR", "system"]) => ()
312 | _ => error "biegelinie.sml: Bsp 7.27 #23";
314 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
315 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
316 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
317 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
318 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
320 "y x =\n-1 * q_0 * L ^^^ 4 / (-24 * EI * L) * x +\n\
321 \(2 * L * q_0 / (-1 * 24 * EI) * x ^^^ 3 +\n\
322 \ -1 * q_0 / (-1 * 24 * EI) * x ^^^ 4)" then ()
323 else error "biegelinie.sml: Bsp 7.27 #24 f";
324 case nxt of ("End_Proof'", End_Proof') => ()
325 | _ => error "biegelinie.sml: Bsp 7.27 #24";
328 (*(([], Frm), Problem (Biegelinie.thy, [MomentBestimmte, Biegelinien])),
329 (([1], Frm), q_ x = q_0),
330 (([1], Res), - q_ x = - q_0),
331 (([2], Res), Q' x = - q_0),
332 (([3], Pbl), Integrate (- q_0, x)),
333 (([3,1], Frm), Q x = Integral - q_0 D x),
334 (([3,1], Res), Q x = -1 * q_0 * x + c),
335 (([3], Res), Q x = -1 * q_0 * x + c),
336 (([4], Res), M_b' x = -1 * q_0 * x + c),
337 (([5], Pbl), Integrate (-1 * q_0 * x + c, x)),
338 (([5,1], Frm), M_b x = Integral -1 * q_0 * x + c D x),
339 (([5,1], Res), M_b x = -1 * q_0 * x ^^^ 2 / 2 + x * c + c_2),
340 (([5], Res), M_b x = -1 * q_0 * x ^^^ 2 / 2 + x * c + c_2),
341 (([6], Res), M_b 0 = -1 * q_0 * 0 ^^^ 2 / 2 + 0 * c + c_2),
342 (([7], Res), 0 = -1 * q_0 * 0 ^^^ 2 / 2 + 0 * c + c_2),
343 (([8], Res), M_b L = -1 * q_0 * L ^^^ 2 / 2 + L * c + c_2),
344 (([9], Res), 0 = -1 * q_0 * L ^^^ 2 / 2 + L * c + c_2),
345 (([10], Pbl), solveSystem [0 = -1 * q_0 * L ^^^ 2 / 2 + L * c + c_2] [c_2]),
346 (([10,1], Frm), [0 = -1 * q_0 * 0 ^^^ 2 / 2 + 0 * c + c_2,
347 0 = -1 * q_0 * L ^^^ 2 / 2 + L * c + c_2]),
348 (([10,1], Res), [0 = c_2, 0 = -1 * (q_0 * L ^^^ 2) / 2 + (L * c + c_2)]),
349 (([10,2], Res), [c_2 = 0, L * c + c_2 = 0 + -1 * (-1 * (q_0 * L ^^^ 2) / 2)]),
350 (([10,3], Res), [c_2 = 0, L * c + c_2 = q_0 * L ^^^ 2 / 2]),
351 (([10,4], Pbl), solveSystem [L * c + c_2 = q_0 * L ^^^ 2 / 2] [c_2]),
352 (([10,4,1], Frm), L * c + c_2 = q_0 * L ^^^ 2 / 2),
353 (([10,4,1], Res), L * c + 0 = q_0 * L ^^^ 2 / 2),
354 (([10,4,2], Res), L * c = q_0 * L ^^^ 2 / 2),
355 (([10,4,3], Res), c = q_0 * L ^^^ 2 / 2 / L),
356 (([10,4,4], Res), c = L * q_0 / 2),
357 (([10,4,5], Res), [c = L * q_0 / 2, c_2 = 0]),
358 (([10,4], Res), [c = L * q_0 / 2, c_2 = 0]),
359 (([10], Res), [c = L * q_0 / 2, c_2 = 0]),
360 (([11], Res), M_b x = -1 * q_0 * x ^^^ 2 / 2 + x * (L * q_0 / 2) + 0),
361 (([12], Res), M_b x = L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2),
362 (([13], Res), EI * y'' x = L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2),
363 (([14], Res), y'' x = 1 / EI * (L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2)),
364 (([15], Pbl), Integrate (1 / EI * (L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2), x)),
365 (([15,1], Frm), y' x = Integral 1 / EI * (L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2) D x),
366 (([15,1], Res), y' x =
367 (Integral L * q_0 * x / 2 D x + Integral -1 * q_0 * x ^^^ 2 / 2 D x) / EI +
370 "----------- Bsp 7.27 autoCalculate ------------------------------";
371 "----------- Bsp 7.27 autoCalculate ------------------------------";
372 "----------- Bsp 7.27 autoCalculate ------------------------------";
374 CalcTree [(["Traegerlaenge L","Streckenlast q_0","Biegelinie y",
375 "RandbedingungenBiegung [y 0 = 0, y L = 0]",
376 "RandbedingungenMoment [M_b 0 = 0, M_b L = 0]",
377 "FunktionsVariable x"],
379 ["MomentBestimmte","Biegelinien"],
380 ["IntegrierenUndKonstanteBestimmen"]))];
382 autoCalculate 1 CompleteCalcHead;
384 fetchProposedTactic 1 (*->"Apply_Method" IntegrierenUndKonstanteBestimmen*);
386 > val (_,Apply_Method' (_, NONE, ScrState is), _)::_ = tacis;
390 autoCalculate 1 (Step 1) (*->GENERATED ([1], Frm)*);
391 val ((pt,_),_) = get_calc 1;
392 case pt of Nd (PblObj _, [Nd _]) => ((*Apply_Method + Take*))
393 | _ => error "biegelinie.sml: Bsp 7.27 autoCalculate#4c";
395 autoCalculate 1 CompleteCalc;
396 val ((pt,p),_) = get_calc 1;
397 if p = ([], Res) andalso length (children pt) = 23 andalso
398 term2str (get_obj g_res pt (fst p)) =
399 "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)"
400 then () else error "biegelinie.sml: 1st biegelin.7.27 changed";
402 val (unc, del, gen) = (([],Pbl), ([],Pbl), ([],Res));
403 getFormulaeFromTo 1 unc gen 1 (*only level 1*) false;
406 (*check all formulae for getTactic*)
407 getTactic 1 ([1],Frm) (*see smltest/../reverse-rew.sml*);
408 getTactic 1 ([5],Res) (*tac2xml: not impl. for Substitute ["x = 0"]*);
409 getTactic 1 ([6],Res) (* ---"--- ["M_b 0 = 0"]*);
410 getTactic 1 ([7],Res) (*!!!!!Take!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!*);
411 getTactic 1 ([8],Frm) (*tac2xml: not impl. for Substitute ["x = L"]*);
412 getTactic 1 ([8],Res) (* ---"--- ["M_b L = 0"]*);
415 "----------- SubProblem (_,[vonBelastungZu,Biegelinien] ----------";
416 "----------- SubProblem (_,[vonBelastungZu,Biegelinien] ----------";
417 "----------- SubProblem (_,[vonBelastungZu,Biegelinien] ----------";
419 ["Streckenlast q_0","FunktionsVariable x",
420 "Funktionen [Q x = c + -1 * q_0 * x, \
421 \M_b x = c_2 + c * x + -1 * q_0 / 2 * x ^^^ 2,\
422 \ y' x = c_3 + 1 / (-1 * EI) * (c_2 * x + c / 2 * x ^^^ 2 + -1 * q_0 / 6 * x ^^^ 3),\
423 \ 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)]"];
424 val (dI',pI',mI') = ("Biegelinie", ["vonBelastungZu","Biegelinien"],
425 ["Biegelinien","ausBelastung"]);
426 val p = e_pos'; val c = [];
427 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
428 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
429 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
430 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
431 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
432 case nxt of ("Apply_Method", Apply_Method ["Biegelinien", "ausBelastung"]) => ()
433 | _ => error "biegelinie.sml met2 b";
435 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f = "q_ x = q_0";
436 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f = "- q_ x = - q_0";
437 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f = "Q' x = - q_0";
438 case nxt of (_, Subproblem (_, ["named", "integrate", "function"])) => ()
439 | _ => error "biegelinie.sml met2 c";
441 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
442 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
443 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
444 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
445 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
447 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f = "Q x = c + -1 * q_0 * x";
448 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f = "Q x = c + -1 * q_0 * x";
449 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f = "M_b' x = c + -1 * q_0 * x";
450 case nxt of (_,Subproblem (_, ["named", "integrate", "function"])) => ()
451 | _ => error "biegelinie.sml met2 d";
453 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
454 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
455 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
456 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
457 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f =
458 "M_b x = Integral c + -1 * q_0 * x D x";
459 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f =
460 "M_b x = c_2 + c * x + -1 * q_0 / 2 * x ^^^ 2";
461 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f =
462 "M_b x = c_2 + c * x + -1 * q_0 / 2 * x ^^^ 2";
463 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f =
464 "- EI * y'' x = c_2 + c * x + -1 * q_0 / 2 * x ^^^ 2";
465 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f =
466 "y'' x = 1 / - EI * (c_2 + c * x + -1 * q_0 / 2 * x ^^^ 2)";
467 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
468 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
469 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
470 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
471 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f =
472 "y' x = Integral 1 / - EI * (c_2 + c * x + -1 * q_0 / 2 * x ^^^ 2) D x";
473 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f =
474 "y' x = Integral 1 / (-1 * EI) * (c_2 + c * x + -1 * q_0 / 2 * x ^^^ 2) D x";
475 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f =
476 "y' x =\nc_3 + 1 / (-1 * EI) * (c_2 * x + c / 2 * x ^^^ 2 + -1 * q_0 / 6 * x ^^^ 3)";
477 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f =
478 "y' x =\nc_3 + 1 / (-1 * EI) * (c_2 * x + c / 2 * x ^^^ 2 + -1 * q_0 / 6 * x ^^^ 3)";
479 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
480 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
481 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
482 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
483 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f =
484 "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";
485 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f =
486 "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)";
487 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f =
488 "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)";
489 val (p,_,f,nxt,_,pt) = me nxt p c pt;
491 "[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)]"
492 then case nxt of ("End_Proof'", End_Proof') => ()
493 | _ => error "biegelinie.sml met2 e 1"
494 else error "biegelinie.sml met2 e 2";
496 "----------- SubProblem (_,[setzeRandbedingungen,Biegelinien] ----";
497 "----------- SubProblem (_,[setzeRandbedingungen,Biegelinien] ----";
498 "----------- SubProblem (_,[setzeRandbedingungen,Biegelinien] ----";
499 val fmz = ["functionEq (M_b x = c_2 + c * x + -1 * q_0 / 2 * x ^^^ 2)",
500 "substitution (M_b L = 0)",
502 val (dI',pI',mI') = ("Biegelinie", ["makeFunctionTo","equation"],
503 ["Equation","fromFunction"]);
504 val p = e_pos'; val c = [];
505 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
506 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
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;
511 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f =
512 "M_b x = c_2 + c * x + -1 * q_0 / 2 * x ^^^ 2";
513 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f =
514 "M_b L = c_2 + c * L + -1 * q_0 / 2 * L ^^^ 2";
515 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f =
516 "0 = c_2 + c * L + -1 * q_0 / 2 * L ^^^ 2";
517 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
518 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
519 if (* f2str f = "0 = c_2 + L * c + -1 * q_0 / 2 * L ^^^ 2" CHANGE NOT considered, already on leave*)
520 f2str f = "0 = (2 * c_2 + 2 * L * c + -1 * L ^^^ 2 * q_0) / 2"
521 then case nxt of ("End_Proof'", End_Proof') => ()
522 | _ => error "biegelinie.sml: SubProblem (_,[setzeRandbed 1"
523 else error "biegelinie.sml: SubProblem (_,[setzeRandbed 2";
526 "----------- method [Biegelinien,setzeRandbedingungenEin] + exec -";
527 "----------- method [Biegelinien,setzeRandbedingungenEin] + exec -";
528 "----------- method [Biegelinien,setzeRandbedingungenEin] + exec -";
529 "----- check the scripts syntax";
530 "----- execute script by interpreter: setzeRandbedingungenEin";
531 val fmz = ["Funktionen [Q x = c + -1 * q_0 * x," ^
532 "M_b x = c_2 + c * x + -1 * q_0 / 2 * x ^^^ 2," ^
533 "y' x = c_3 + 1 / (-1 * EI) * (c_2 * x + c / 2 * x ^^^ 2 + -1 * q_0 / 6 * x ^^^ 3)," ^
534 "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)]",
535 "Randbedingungen [y 0 = 0, y L = 0, M_b 0 = 0, M_b L = 0]",
536 "Gleichungen equ_s"];
537 val (dI',pI',mI') = ("Biegelinie", ["setzeRandbedingungen","Biegelinien"],
538 ["Biegelinien","setzeRandbedingungenEin"]);
539 val p = e_pos'; val c = [];
540 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
541 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
542 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
543 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
544 val (p,_,f,nxt,_,pt) = me nxt p c pt;
546 "--- before 1.subpbl [Equation, fromFunction]";
547 val (p,_,f,nxt,_,pt) = me nxt p c pt;
548 case nxt of (_, Apply_Method ["Biegelinien", "setzeRandbedingungenEin"])=>()
549 | _ => error "biegelinie.sml: met setzeRandbed*Ein aa";
550 "----- Randbedingung y 0 = 0 in SUBpbl with met [Equation, fromFunction]";
551 val (p,_,f,nxt,_,pt) = me nxt p c pt;
552 if (#1 o (get_obj g_fmz pt)) (fst p) =
553 ["functionEq\n (y x =\n c_4 + c_3 * x +\n 1 / (-1 * EI) *" ^
554 "\n (c_2 / 2 * x ^^^ 2 + c / 6 * x ^^^ 3 + -1 * q_0 / 24 * x ^^^ 4))",
555 "substitution (y 0 = 0)", "equality equ'''"] then ()
556 else error "biegelinie.sml met setzeRandbed*Ein bb";
557 (writeln o istate2str) (get_istate pt p);
558 "--- after 1.subpbl [Equation, fromFunction]";
560 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;val (p,_,f,nxt,_,pt) = me nxt p c pt;
563 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
564 case nxt of (_, Apply_Method["Equation", "fromFunction"]) => ()
565 | _ => error "biegelinie.sml met2 ff";
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; val (p,_,f,nxt,_,pt) = me nxt p c pt;
569 val (p,_,f,nxt,_,pt) = me nxt p c pt;
570 case nxt of (_, Check_Postcond ["makeFunctionTo", "equation"]) => ()
571 | _ => error "biegelinie.sml met2 gg";
573 "--- before 2.subpbl [Equation, fromFunction]";
574 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f = "0 = c_4 + 0 / (-1 * EI)" ;
575 case nxt of (_,Subproblem (_, ["makeFunctionTo", "equation"])) => ()
576 | _ => error "biegelinie.sml met2 hh";
577 "--- after 1st arrival at 2.subpbl [Equation, fromFunction]";
579 val (p,_,f,nxt,_,pt) = me nxt p c pt;
580 if (#1 o (get_obj g_fmz pt)) (fst p) =
581 ["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))",
582 "substitution (y L = 0)", "equality equ'''"] then ()
583 else error "biegelinie.sml metsetzeRandbed*Ein bb ";
584 val (p,_,f,nxt,_,pt) = me nxt p c pt;
585 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
586 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
588 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
589 case nxt of (_, Apply_Method["Equation", "fromFunction"]) => ()
590 | _ => error "biegelinie.sml met2 ii";
591 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)";
592 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)";
593 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)";
594 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)" ;
595 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)";
596 case nxt of (_,Subproblem (_, ["makeFunctionTo", "equation"])) => ()
597 | _ => error "biegelinie.sml met2 jj";
599 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
600 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
601 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
602 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
603 case nxt of (_, Apply_Method ["Equation", "fromFunction"])=>()
604 | _ => error "biegelinie.sml met2 kk";
606 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*);
607 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f = "0 = c_2 + c * 0 + -1 * q_0 / 2 * 0 ^^^ 2";
608 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f = "0 = c_2";
609 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f = "0 = c_2";
610 val (p,_,f,nxt,_,pt) = me nxt p c pt;
611 (*========== inhibit exn WN1130722 Isabelle2012-->13 thehier? works in Test_Some===
613 case nxt of (_, Subproblem (_, ["makeFunctionTo", "equation"])) => ()
614 | _ => error "biegelinie.sml met2 ll";
616 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
617 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
618 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
619 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
620 case nxt of (_, Apply_Method ["Equation", "fromFunction"])=>()
621 | _ => error "biegelinie.sml met2 mm";
623 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";
624 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";
625 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f = "0 = c_2 + c * L + -1 * q_0 / 2 * L ^^^ 2";
626 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";
627 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";
628 case nxt of (_, Check_Postcond ["setzeRandbedingungen", "Biegelinien"]) => ()
629 | _ => error "biegelinie.sml met2 nn";
630 val (p,_,f,nxt,_,pt) = me nxt p c pt;
631 if nxt = ("End_Proof'", End_Proof') andalso f2str f =
632 (* "[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]" *)
633 "[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]"
634 then () else error "biegelinie.sml met2 oo";
635 ============ inhibit exn WN1130722 Isabelle2012-->13 thehier? works in Test_Some=*)
637 "----------- IntegrierenUndKonstanteBestimmen2: Bsp.7.70. --------";
638 "----------- IntegrierenUndKonstanteBestimmen2: Bsp.7.70. --------";
639 "----------- IntegrierenUndKonstanteBestimmen2: Bsp.7.70. --------";
640 "----- Bsp 7.70 with me";
641 val fmz = ["Traegerlaenge L","Streckenlast q_0","Biegelinie y",
642 "Randbedingungen [y 0 = 0, y L = 0, M_b 0 = 0, M_b L = 0]",
643 "FunktionsVariable x"];
644 val (dI',pI',mI') = ("Biegelinie", ["Biegelinien"],
645 ["IntegrierenUndKonstanteBestimmen2"]);
646 val p = e_pos'; val c = [];
647 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
648 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
649 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
650 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
651 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
652 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
653 (*========== inhibit exn WN1130722 Isabelle2012-->13 thehier? works in Test_Some===
654 if nxt = ("Apply_Method", Apply_Method ["IntegrierenUndKonstanteBestimmen2"])
655 then () else error "biegelinie.sml met2 a";
657 (*** actual arg(s) missing for '["(#Find, (Funktionen, funs_))"]' i.e. should be 'copy-named' by '*_._'
659 #a# "Script Biegelinie2Script ..
660 " ... (SubProblem (Biegelinie_,[vonBelastungZu,Biegelinien], " ^
661 " [Biegelinien,ausBelastung]) " ^
662 " [REAL q__, REAL v_]); "
664 #b# prep_met ... (["Biegelinien","ausBelastung"],
665 ... ("#Given" ,["Streckenlast q__","FunktionsVariable v_v"]),
666 "Script Belastung2BiegelScript (q__::real) (v_v::real) = "
668 #a#b# BOTH HAVE 2 ARGUMENTS q__ and v_v ...OK
669 ##########################################################################
670 BUT THE (#Find, (Funktionen, funs_)) IS NOT COPYNAMED BY funs___ !!!3*_!!!
671 ##########################################################################*)
672 "further 'me' see ----- SubProblem (_,[vonBelastungZu,Biegelinien] -------" ^
673 " ----- SubProblem (_,[setzeRandbedingungen,Biegelinien] -";
676 "----- Bsp 7.70 with autoCalculate";
677 CalcTree [(["Traegerlaenge L","Streckenlast q_0","Biegelinie y",
678 "Randbedingungen [Q 0 = q_0 * L, M_b L = 0, y 0 = 0, y' 0 = 0]",
679 "FunktionsVariable x"],
680 ("Biegelinie", ["Biegelinien"],
681 ["IntegrierenUndKonstanteBestimmen2"]))];
683 autoCalculate 1 CompleteCalc;
684 val ((pt,p),_) = get_calc 1; show_pt pt;
685 if p = ([], Res) andalso term2str (get_obj g_res pt (fst p)) =
686 "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 ()
687 else error "biegelinie.sml: diff.behav.7.70 with autoCalculate";
689 val is = get_istate pt ([],Res); writeln (istate2str is);
690 val t = str2term (" last " ^
691 "[Q x = L * q_0 + -1 * q_0 * x, " ^
692 " M_b x = -1 * q_0 * L ^^^ 2 / 2 + q_0 * L / 1 * x + -1 * q_0 / 2 * x ^^^ 2," ^
694 " -3 * q_0 * L ^^^ 2 / (-6 * EI) * x + 3 * L * q_0 / (-6 * EI) * x ^^^ 2 +" ^
695 " -1 * q_0 / (-6 * EI) * x ^^^ 3, " ^
697 " -6 * q_0 * L ^^^ 2 / (-24 * EI) * x ^^^ 2 + " ^
698 " 4 * L * q_0 / (-24 * EI) * x ^^^ 3 + " ^
699 " -1 * q_0 / (-24 * EI) * x ^^^ 4]");
700 val srls = append_rls "erls_IntegrierenUndK.." e_rls
701 [Calc("Tools.rhs", eval_rhs"eval_rhs_"),
702 Calc ("Atools.ident",eval_ident "#ident_"),
703 Thm ("last_thmI",num_str @{thm last_thmI}),
704 Thm ("if_True",num_str @{thm if_True}),
705 Thm ("if_False",num_str @{thm if_False})
708 val t = str2term "last [1,2,3,4]";
709 (*trace_rewrite := true; ..stopped Test_Isac.thy*)
710 val SOME (e1__,_) = rewrite_set_ thy false srls t;
711 trace_rewrite := false;
713 ============ inhibit exn WN1130722 Isabelle2012-->13 thehier? works in Test_Some=*)
715 "----------- investigate normalforms in biegelinien --------------";
716 "----------- investigate normalforms in biegelinien --------------";
717 "----------- investigate normalforms in biegelinien --------------";
718 "----- coming from integration:";
719 val Q = str2term "Q x = c + -1 * q_0 * x";
720 val M_b = str2term "M_b x = c_2 + c * x + -1 * q_0 / 2 * x ^^^ 2";
721 val y' = str2term "y' x = c_3 + 1 / (-1 * EI) * (c_2 * x + c / 2 * x ^^^ 2 + -1 * q_0 / 6 * x ^^^ 3)";
722 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)";
723 (*^^^ 1 / (-1 * EI) NOT distributed - ok! ^^^^^^^^^^^^^^^^^^^^^^^*)
725 "----- functions comming from:";