intermed. test/../biegelinie.sml
+ meeting dmeindl: Rational2.thy
2 author: Walther Neuper 050826
3 (c) due to copyright terms
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 "----------- method [Biegelinien,setzeRandbedingungenEin]FAST ----";
18 "----------- IntegrierenUndKonstanteBestimmen2: Bsp.7.70. --------";
19 "----------- investigate normalforms in biegelinien --------------";
20 "-----------------------------------------------------------------";
21 "-----------------------------------------------------------------";
22 "-----------------------------------------------------------------";
24 val thy = @{theory "Biegelinie"};
25 val ctxt = thy2ctxt' "Biegelinie";
26 fun str2term str = (term_of o the o (parse thy)) str;
27 fun term2s t = Print_Mode.setmp [] (Syntax.string_of_term (thy2ctxt' "Biegelinie")) t;
29 fst (the (rewrite_ thy tless_true e_rls true thm str));
31 "----------- the rules -------------------------------------------";
32 "----------- the rules -------------------------------------------";
33 "----------- the rules -------------------------------------------";
34 val t = rewrit @{thm Belastung_Querkraft} (str2term "- qq x = - q_0"); term2s t;
35 if term2s t = "Q' x = - q_0" then ()
36 else error "/biegelinie.sml: Belastung_Querkraft";
38 val t = rewrit @{thm Querkraft_Moment} (str2term "Q x = - q_0 * x + c"); term2s t;
39 if term2s t = "M_b' x = - q_0 * x + c" then ()
40 else error "/biegelinie.sml: Querkraft_Moment";
42 val t = rewrit @{thm Moment_Neigung} (str2term "M_b x = -q_0 * x^^^2/2 + q_0/2 *L*x");
44 if term2s t = "- EI * y'' x = - q_0 * x ^^^ 2 / 2 + q_0 / 2 * L * x" then ()
45 else error "biegelinie.sml: Moment_Neigung";
47 "----------- IntegrierenUndKonstanteBestimmen by rewriting -------";
48 "----------- IntegrierenUndKonstanteBestimmen by rewriting -------";
49 "----------- IntegrierenUndKonstanteBestimmen by rewriting -------";
50 "----------- IntegrierenUndKonstanteBestimmen by rewriting -------";
51 val t = str2term "M_b x = L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2";
52 val t = rewrit @{thm Moment_Neigung} t;
53 if term2s t = "- EI * y'' x = L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2" then ()
54 else error "Moment_Neigung broken";
55 (* was I * ?y'' x = L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2"
56 before declaring "y''" as a constant *)
58 val t = rewrit @{thm make_fun_explicit} t;
59 if term2s t = "y'' x = 1 / - EI * (L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2)" then ()
60 else error "make_fun_explicit broken";
62 "----------- simplify_leaf for this script -----------------------";
63 "----------- simplify_leaf for this script -----------------------";
64 "----------- simplify_leaf for this script -----------------------";
65 val srls = Rls {id="srls_IntegrierenUnd..",
67 rew_ord = ("termlessI",termlessI),
68 erls = append_rls "erls_in_srls_IntegrierenUnd.." e_rls
69 [(*for asm in NTH_CONS ...*)
70 Calc ("Orderings.ord_class.less",eval_equ "#less_"),
71 (*2nd NTH_CONS pushes n+-1 into asms*)
72 Calc("Groups.plus_class.plus", eval_binop "#add_")
74 srls = Erls, calc = [],
75 rules = [Thm ("NTH_CONS",num_str @{thm NTH_CONS}),
76 Calc("Groups.plus_class.plus", eval_binop "#add_"),
77 Thm ("NTH_NIL",num_str @{thm NTH_NIL}),
78 Calc("Tools.lhs", eval_lhs "eval_lhs_"),
79 Calc("Tools.rhs", eval_rhs "eval_rhs_"),
80 Calc("Atools.argument'_in", eval_argument_in "Atools.argument'_in")
83 val rm_ = str2term"[M_b 0 = 0, M_b L = 0]";
84 val M__ = str2term"M_b x = -1 * x ^^^ 2 / 2 + x * c + c_2";
85 val SOME (e1__,_) = rewrite_set_ thy false srls
86 (str2term "(NTH::[real,bool list]=>bool) 1 " $ rm_);
87 if term2str e1__ = "M_b 0 = 0" then () else error "biegelinie.sml simplify NTH 1 rm_";
90 rewrite_set_ thy false srls
91 (str2term"argument_in (lhs (M_b 0 = 0))");
92 if term2str x1__ = "0" then ()
93 else error "biegelinie.sml simplify argument_in (lhs (M_b 0 = 0)";
98 "----------- Bsp 7.27 me -----------------------------------------";
99 "----------- Bsp 7.27 me -----------------------------------------";
100 "----------- Bsp 7.27 me -----------------------------------------";
101 val fmz = ["Traegerlaenge L","Streckenlast q_0","Biegelinie y",
102 "RandbedingungenBiegung [y 0 = 0, y L = 0]",
103 "RandbedingungenMoment [M_b 0 = 0, M_b L = 0]",
104 "FunktionsVariable x"];
106 ("Biegelinie",["MomentBestimmte","Biegelinien"],
107 ["IntegrierenUndKonstanteBestimmen"]);
108 val p = e_pos'; val c = [];
109 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
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;
114 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
116 val pits = get_obj g_pbl pt (fst p);writeln (itms2str_ ctxt pits);
117 (*if itms2str_ ctxt pits = ... all 5 model-items*)
118 val mits = get_obj g_met pt (fst p); writeln (itms2str_ ctxt mits);
119 if itms2str_ ctxt mits = "[]" then ()
120 else error "biegelinie.sml: Bsp 7.27 #2";
122 val (p,_,f,nxt,_,pt) = me nxt p c pt;
123 case nxt of (_,Add_Given "FunktionsVariable x") => ()
124 | _ => error "biegelinie.sml: Bsp 7.27 #4a";
126 val (p,_,f,nxt,_,pt) = me nxt p c pt;
127 val mits = get_obj g_met pt (fst p);writeln (itms2str_ ctxt mits);
128 (*if itms2str_ ctxt mits = ... all 6 guard-items*)
129 case nxt of (_, Apply_Method ["IntegrierenUndKonstanteBestimmen"]) => ()
130 | _ => error "biegelinie.sml: Bsp 7.27 #4b";
132 "===== Apply_Method IntegrierenUndKonstanteBestimmen ============================";
133 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
134 case pt of Nd (PblObj _, [Nd _]) => ((*Apply_Method + Take*))
135 | _ => error "biegelinie.sml: Bsp 7.27 #4c";
136 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
137 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
139 (*=== inhibit exn 110722=============================================================
141 (_,Subproblem ("Biegelinie", ["named", "integrate", "function"])) => ()
142 | _ => error "biegelinie.sml: Bsp 7.27 #4c";
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 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
146 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
147 case nxt of (_, Apply_Method ["diff", "integration", "named"]) => ()
148 | _ => error "biegelinie.sml: Bsp 7.27 #5";
149 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
150 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
151 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
153 ("Check_Postcond", Check_Postcond ["named", "integrate", "function"]) => ()
154 | _ => error "biegelinie.sml: Bsp 7.27 #5a";
156 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
157 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
159 (_, Subproblem ("Biegelinie", ["named", "integrate", "function"]))=>()
160 | _ => error "biegelinie.sml: Bsp 7.27 #5b";
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 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
165 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
166 case nxt of (_, Apply_Method ["diff", "integration","named"]) => ()
167 | _ => error "biegelinie.sml: Bsp 7.27 #6";
169 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
170 val (p,_,f,nxt,_,pt) = me nxt p c pt(*nxt = Check_Postcond ["named", "int..*);
172 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
173 case nxt of (_, Substitute ["x = 0"]) => ()
174 | _ => error "biegelinie.sml: Bsp 7.27 #7";
176 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
177 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
178 if f2str f = "0 = c_2 + c * 0 + -1 * q_0 / 2 * 0 ^^^ 2" then ()
179 else error "biegelinie.sml: Bsp 7.27 #8";
181 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
182 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
183 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
184 if f2str f = "0 = c_2 + c * L + -1 * q_0 / 2 * L ^^^ 2" then ()
185 else error "biegelinie.sml: Bsp 7.27 #9";
187 (*val nxt = (+, Subproblem ("Biegelinie", ["normalize", ..lin..sys]))*)
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;
193 case nxt of (_, Apply_Method ["EqSystem", "normalize", "2x2"]) => ()
194 | _ => error "biegelinie.sml: Bsp 7.27 #10";
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 (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
199 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
200 (*val nxt = Subproblem ["triangular", "2x2", "linear", "system"]*)
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 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
205 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
206 case nxt of (_, Apply_Method["EqSystem", "top_down_substitution", "2x2"]) => ()
207 | _ => error "biegelinie.sml: Bsp 7.27 #11";
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 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
216 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
217 case nxt of (_, Check_Postcond ["normalize", "2x2", "linear", "system"]) => ()
218 | _ => error "biegelinie.sml: Bsp 7.27 #12";
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;
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;
227 (_, Subproblem ("Biegelinie", ["named", "integrate", "function"]))=>()
228 | _ => error "biegelinie.sml: Bsp 7.27 #13";
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 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
233 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
234 case nxt of (_, Apply_Method ["diff", "integration", "named"]) => ()
235 | _ => error "biegelinie.sml: Bsp 7.27 #14";
237 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
238 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
239 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
241 (_, Check_Postcond ["named", "integrate", "function"]) => ()
242 | _ => error "biegelinie.sml: Bsp 7.27 #15";
244 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
246 "y' x = c + 1 / (-1 * EI) * (L * q_0 / 4 * x ^^^ 2 + -1 * q_0 / 6 * x ^^^ 3)"
247 then () else error "biegelinie.sml: Bsp 7.27 #16 f";
249 (_, Subproblem ("Biegelinie", ["named", "integrate", "function"]))=>()
250 | _ => error "biegelinie.sml: Bsp 7.27 #16";
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 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
255 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
256 case nxt of (_, Apply_Method ["diff", "integration", "named"]) => ()
257 | _ => error "biegelinie.sml: Bsp 7.27 #17";
259 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
260 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
262 "y x =\nc_2 + c * x +\n\
263 \1 / (-1 * EI) * (L * q_0 / 12 * x ^^^ 3 + -1 * q_0 / 24 * x ^^^ 4)"
264 then () else error "biegelinie.sml: Bsp 7.27 #18 f";
266 (_, Check_Postcond ["named", "integrate", "function"]) => ()
267 | _ => error "biegelinie.sml: Bsp 7.27 #18";
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;
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;
277 ("Biegelinie", ["normalize", "2x2", "linear", "system"])) => ()
278 | _ => error "biegelinie.sml: Bsp 7.27 #19";
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;val (p,_,f,nxt,_,pt) = me nxt p c pt;
282 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
283 val (p,_,f,nxt,_,pt) = me nxt p c pt;
284 case nxt of (_, Apply_Method ["EqSystem", "normalize", "2x2"]) => ()
285 | _ => error "biegelinie.sml: Bsp 7.27 #20";
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 if f2str f = "[c_2 = 0, L * c + c_2 = -1 * q_0 * L ^^^ 4 / (-24 * EI)]" then ()
292 else error "biegelinie.sml: Bsp 7.27 #21 f";
295 ("Biegelinie", ["triangular", "2x2", "linear", "system"])) =>()
296 | _ => error "biegelinie.sml: Bsp 7.27 #21";
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;val (p,_,f,nxt,_,pt) = me nxt p c pt;
300 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
301 val (p,_,f,nxt,_,pt) = me nxt p c pt;
302 case nxt of (_, Apply_Method["EqSystem", "top_down_substitution", "2x2"]) => ()
303 | _ => error "biegelinie.sml: Bsp 7.27 #22";
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 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
312 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
313 case nxt of (_, Check_Postcond ["normalize", "2x2", "linear", "system"]) => ()
314 | _ => error "biegelinie.sml: Bsp 7.27 #23";
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;
319 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
320 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
322 "y x =\n-1 * q_0 * L ^^^ 4 / (-24 * EI * L) * x +\n\
323 \(2 * L * q_0 / (-1 * 24 * EI) * x ^^^ 3 +\n\
324 \ -1 * q_0 / (-1 * 24 * EI) * x ^^^ 4)" then ()
325 else error "biegelinie.sml: Bsp 7.27 #24 f";
326 case nxt of ("End_Proof'", End_Proof') => ()
327 | _ => error "biegelinie.sml: Bsp 7.27 #24";
328 === inhibit exn 110722=============================================================*)
331 (*(([], Frm), Problem (Biegelinie.thy, [MomentBestimmte, Biegelinien])),
332 (([1], Frm), q_ x = q_0),
333 (([1], Res), - q_ x = - q_0),
334 (([2], Res), Q' x = - q_0),
335 (([3], Pbl), Integrate (- q_0, x)),
336 (([3,1], Frm), Q x = Integral - q_0 D x),
337 (([3,1], Res), Q x = -1 * q_0 * x + c),
338 (([3], Res), Q x = -1 * q_0 * x + c),
339 (([4], Res), M_b' x = -1 * q_0 * x + c),
340 (([5], Pbl), Integrate (-1 * q_0 * x + c, x)),
341 (([5,1], Frm), M_b x = Integral -1 * q_0 * x + c D x),
342 (([5,1], Res), M_b x = -1 * q_0 * x ^^^ 2 / 2 + x * c + c_2),
343 (([5], Res), M_b x = -1 * q_0 * x ^^^ 2 / 2 + x * c + c_2),
344 (([6], Res), M_b 0 = -1 * q_0 * 0 ^^^ 2 / 2 + 0 * c + c_2),
345 (([7], Res), 0 = -1 * q_0 * 0 ^^^ 2 / 2 + 0 * c + c_2),
346 (([8], Res), M_b L = -1 * q_0 * L ^^^ 2 / 2 + L * c + c_2),
347 (([9], Res), 0 = -1 * q_0 * L ^^^ 2 / 2 + L * c + c_2),
348 (([10], Pbl), solveSystem [0 = -1 * q_0 * L ^^^ 2 / 2 + L * c + c_2] [c_2]),
349 (([10,1], Frm), [0 = -1 * q_0 * 0 ^^^ 2 / 2 + 0 * c + c_2,
350 0 = -1 * q_0 * L ^^^ 2 / 2 + L * c + c_2]),
351 (([10,1], Res), [0 = c_2, 0 = -1 * (q_0 * L ^^^ 2) / 2 + (L * c + c_2)]),
352 (([10,2], Res), [c_2 = 0, L * c + c_2 = 0 + -1 * (-1 * (q_0 * L ^^^ 2) / 2)]),
353 (([10,3], Res), [c_2 = 0, L * c + c_2 = q_0 * L ^^^ 2 / 2]),
354 (([10,4], Pbl), solveSystem [L * c + c_2 = q_0 * L ^^^ 2 / 2] [c_2]),
355 (([10,4,1], Frm), L * c + c_2 = q_0 * L ^^^ 2 / 2),
356 (([10,4,1], Res), L * c + 0 = q_0 * L ^^^ 2 / 2),
357 (([10,4,2], Res), L * c = q_0 * L ^^^ 2 / 2),
358 (([10,4,3], Res), c = q_0 * L ^^^ 2 / 2 / L),
359 (([10,4,4], Res), c = L * q_0 / 2),
360 (([10,4,5], Res), [c = L * q_0 / 2, c_2 = 0]),
361 (([10,4], Res), [c = L * q_0 / 2, c_2 = 0]),
362 (([10], Res), [c = L * q_0 / 2, c_2 = 0]),
363 (([11], Res), M_b x = -1 * q_0 * x ^^^ 2 / 2 + x * (L * q_0 / 2) + 0),
364 (([12], Res), M_b x = L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2),
365 (([13], Res), EI * y'' x = L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2),
366 (([14], Res), y'' x = 1 / EI * (L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2)),
367 (([15], Pbl), Integrate (1 / EI * (L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2), x)),
368 (([15,1], Frm), y' x = Integral 1 / EI * (L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2) D x),
369 (([15,1], Res), y' x =
370 (Integral L * q_0 * x / 2 D x + Integral -1 * q_0 * x ^^^ 2 / 2 D x) / EI +
373 "----------- Bsp 7.27 autoCalculate ------------------------------";
374 "----------- Bsp 7.27 autoCalculate ------------------------------";
375 "----------- Bsp 7.27 autoCalculate ------------------------------";
377 CalcTree [(["Traegerlaenge L","Streckenlast q_0","Biegelinie y",
378 "RandbedingungenBiegung [y 0 = 0, y L = 0]",
379 "RandbedingungenMoment [M_b 0 = 0, M_b L = 0]",
380 "FunktionsVariable x"],
382 ["MomentBestimmte","Biegelinien"],
383 ["IntegrierenUndKonstanteBestimmen"]))];
385 autoCalculate 1 CompleteCalcHead;
387 fetchProposedTactic 1 (*->"Apply_Method" IntegrierenUndKonstanteBestimmen*);
389 > val (_,Apply_Method' (_, NONE, ScrState is), _)::_ = tacis;
393 autoCalculate 1 (Step 1) (*->GENERATED ([1], Frm)*);
394 val ((pt,_),_) = get_calc 1;
395 case pt of Nd (PblObj _, [Nd _]) => ((*Apply_Method + Take*))
396 | _ => error "biegelinie.sml: Bsp 7.27 autoCalculate#4c";
398 autoCalculate 1 CompleteCalc;
399 val ((pt,p),_) = get_calc 1;
400 (*=== inhibit exn 110722=============================================================
401 if p = ([], Res) andalso length (children pt) = 23 andalso
402 term2str (get_obj g_res pt (fst p)) =
403 "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)"
404 then () else error "biegelinie.sml: 1st biegelin.7.27 changed";
405 === inhibit exn 110722=============================================================*)
407 val (unc, del, gen) = (([],Pbl), ([],Pbl), ([],Res));
408 getFormulaeFromTo 1 unc gen 1 (*only level 1*) false;
411 (*check all formulae for getTactic*)
412 getTactic 1 ([1],Frm) (*see smltest/../reverse-rew.sml*);
413 getTactic 1 ([5],Res) (*tac2xml: not impl. for Substitute ["x = 0"]*);
414 getTactic 1 ([6],Res) (* ---"--- ["M_b 0 = 0"]*);
415 getTactic 1 ([7],Res) (*!!!!!Take!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!*);
416 getTactic 1 ([8],Frm) (*tac2xml: not impl. for Substitute ["x = L"]*);
417 getTactic 1 ([8],Res) (* ---"--- ["M_b L = 0"]*);
420 "----------- SubProblem (_,[vonBelastungZu,Biegelinien] ----------";
421 "----------- SubProblem (_,[vonBelastungZu,Biegelinien] ----------";
422 "----------- SubProblem (_,[vonBelastungZu,Biegelinien] ----------";
424 ["Streckenlast q_0","FunktionsVariable x",
425 "Funktionen [Q x = c + -1 * q_0 * x, \
426 \M_b x = c_2 + c * x + -1 * q_0 / 2 * x ^^^ 2,\
427 \ y' x = c_3 + 1 / (-1 * EI) * (c_2 * x + c / 2 * x ^^^ 2 + -1 * q_0 / 6 * x ^^^ 3),\
428 \ 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)]"];
429 val (dI',pI',mI') = ("Biegelinie", ["vonBelastungZu","Biegelinien"],
430 ["Biegelinien","ausBelastung"]);
431 val p = e_pos'; val c = [];
432 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
433 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
434 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
435 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
436 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
437 if nxt = ("Apply_Method", Apply_Method ["Biegelinien", "ausBelastung"])
438 then () else error "biegelinie.sml met2 b";
439 (*=== inhibit exn 110722=============================================================
441 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f = "q_ x = q_0";
442 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f = "- q_ x = - q_0";
443 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f = "Q' x = - q_0";
444 case nxt of (_, Subproblem (_, ["named", "integrate", "function"])) => ()
445 | _ => error "biegelinie.sml met2 c";
447 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
448 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
449 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
450 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
451 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
453 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f = "Q x = c + -1 * q_0 * x";
454 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f = "Q x = c + -1 * q_0 * x";
455 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f = "M_b' x = c + -1 * q_0 * x";
456 case nxt of (_,Subproblem (_, ["named", "integrate", "function"])) => ()
457 | _ => error "biegelinie.sml met2 d";
459 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
460 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
461 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
462 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
463 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f =
464 "M_b x = Integral c + -1 * q_0 * x D x";
465 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f =
466 "M_b x = c_2 + c * x + -1 * q_0 / 2 * x ^^^ 2";
467 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f =
468 "M_b x = c_2 + c * x + -1 * q_0 / 2 * x ^^^ 2";
469 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f =
470 "- EI * y'' x = c_2 + c * x + -1 * q_0 / 2 * x ^^^ 2";
471 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f =
472 "y'' x = 1 / - EI * (c_2 + c * x + -1 * q_0 / 2 * x ^^^ 2)";
473 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
474 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
475 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
476 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
477 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f =
478 "y' x = Integral 1 / - EI * (c_2 + c * x + -1 * q_0 / 2 * x ^^^ 2) D x";
479 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f =
480 "y' x = Integral 1 / (-1 * EI) * (c_2 + c * x + -1 * q_0 / 2 * x ^^^ 2) D x";
481 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f =
482 "y' x =\nc_3 + 1 / (-1 * EI) * (c_2 * x + c / 2 * x ^^^ 2 + -1 * q_0 / 6 * x ^^^ 3)";
483 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f =
484 "y' x =\nc_3 + 1 / (-1 * EI) * (c_2 * x + c / 2 * x ^^^ 2 + -1 * q_0 / 6 * x ^^^ 3)";
485 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
486 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
487 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
488 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
489 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f =
490 "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";
491 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f =
492 "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)";
493 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f =
494 "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)";
495 val (p,_,f,nxt,_,pt) = me nxt p c pt;
496 if nxt = ("End_Proof'", End_Proof') andalso f2str f =
497 "[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 ()
498 else error "biegelinie.sml met2 e";
499 === inhibit exn 110722=============================================================*)
503 "----------- SubProblem (_,[setzeRandbedingungen,Biegelinien] ----";
504 "----------- SubProblem (_,[setzeRandbedingungen,Biegelinien] ----";
505 "----------- SubProblem (_,[setzeRandbedingungen,Biegelinien] ----";
507 "Script Function2Equality (fun_::bool) (sub_::bool) =\
510 (*=== inhibit exn 110722=============================================================
511 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
513 "Script Function2Equality (fun_::bool) (sub_::bool) =\
514 \ (let v_v = argument_in (lhs fun_)\
515 \ in (equ___::bool))"
517 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
519 "Script Function2Equality (fun_::bool) (sub_::bool) =\
520 \ (let v_v = argument_in (lhs fun_);\
521 \ (equ_) = (Substitute [sub_]) fun_\
524 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
526 "Script Function2Equality (fun_::bool) (sub_::bool) =\
527 \ (let v_v = argument_in (lhs fun_);\
528 \ equ_ = (Substitute [sub_]) fun_\
529 \ in (Rewrite_Set_Inst [(bdv, v_v)] make_ratpoly_in False) equ_)"
531 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
532 === inhibit exn 110722=============================================================*)
535 (*(M_b x = c_2 + c * x + -1 * q_0 / 2 * x ^^^ 2) (M_b L = 0) -->
536 0 = c_2 + c * L + -1 * q_0 / 2 * L ^^^ 2*)
537 "Script Function2Equality (fun_::bool) (sub_::bool) =\
538 \ (let bdv_ = argument_in (lhs fun_);\
539 \ val_ = argument_in (lhs sub_);\
540 \ equ_ = (Substitute [bdv_ = val_]) fun_;\
541 \ equ_ = (Substitute [sub_]) fun_\
542 \ in (Rewrite_Set_Inst [(bdv_, v_v)] make_ratpoly_in False) equ_)"
544 (*=== inhibit exn 110722=============================================================
545 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
548 val fmz = ["functionEq (M_b x = c_2 + c * x + -1 * q_0 / 2 * x ^^^ 2)",
549 "substitution (M_b L = 0)",
551 val (dI',pI',mI') = ("Biegelinie", ["makeFunctionTo","equation"],
552 ["Equation","fromFunction"]);
553 val p = e_pos'; val c = [];
554 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
555 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
556 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
557 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
558 val (p,_,f,nxt,_,pt) = me nxt p c pt;
560 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f =
561 "M_b x = c_2 + c * x + -1 * q_0 / 2 * x ^^^ 2";
562 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f =
563 "M_b L = c_2 + c * L + -1 * q_0 / 2 * L ^^^ 2";
564 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f =
565 "0 = c_2 + c * L + -1 * q_0 / 2 * L ^^^ 2";
566 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
567 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
568 if nxt = ("End_Proof'", End_Proof') andalso
569 (* f2str f = "0 = c_2 + L * c + -1 * q_0 / 2 * L ^^^ 2"
570 CHANGE NOT considered, already on leave*)
571 f2str f = "0 = (2 * c_2 + 2 * L * c + -1 * L ^^^ 2 * q_0) / 2"
572 then () else error "biegelinie.sml: SubProblem (_,[setzeRandbed";
573 === inhibit exn 110722=============================================================*)
576 "----------- method [Biegelinien,setzeRandbedingungenEin] + exec -";
577 "----------- method [Biegelinien,setzeRandbedingungenEin] + exec -";
578 "----------- method [Biegelinien,setzeRandbedingungenEin] + exec -";
579 "----- check the scripts syntax";
581 "Script SetzeRandbedScript (funs_::bool list) (beds_::bool list) =\
582 \ (let b1 = Take (nth_ 1 beds_)\
583 \ in (equs_::bool list))"
585 (*=== inhibit exn 110722=============================================================
587 (*show_types := true;*)
588 val funs_ = str2term "funs_::bool list";
590 "[Q x = c + -1 * q_0 * x,\
591 \M_b x = c_2 + c * x + -1 * q_0 / 2 * x ^^^ 2,\
592 \y' x = c_3 + 1 / (-1 * EI) * (c_2 * x + c / 2 * x ^^^ 2 + -1 * q_0 / 6 * x ^^^ 3),\
593 \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)]";
594 val rb_ = str2term "rb_::bool list";
595 val rb = str2term "[y 0 = 0, y L = 0, M_b 0 = 0, M_b L = 0]";
597 "--- script expression 1";
598 val screxp1_ = str2term "Take (nth_ 1 (rb_::bool list))";
599 val screxp1 = subst_atomic [(rb_, rb)] screxp1_; term2str screxp1;
600 val SOME (b1,_) = rewrite_set_ (theory "Isac") false srls2 screxp1; term2str b1;
601 if term2str b1 = "Take (y 0 = 0)" then ()
602 else error "biegelinie.sml: rew. Bieglie2 --1";
603 val b1 = str2term "(y 0 = 0)";
605 "--- script expression 2";
606 val screxp2_ = str2term "filter (sameFunId (lhs b1_)) funs_";
607 val b1_ = str2term "b1_::bool";
608 val screxp2 = subst_atomic [(b1_,b1),(funs_,funs)] screxp2_; term2str screxp2;
609 val SOME (fs,_) = rewrite_set_ (theory "Isac") false srls2 screxp2; term2str fs;
610 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 ()
611 else error "biegelinie.sml: rew. Bieglie2 --2";
613 "--- script expression 3";
614 val screxp3_ = str2term "SubProblem (Biegelinie_,[makeFunctionTo,equation],\
615 \ [Equation,fromFunction]) \
616 \ [BOOL (hd fs_), BOOL b1_]";
617 val fs_ = str2term "fs_::bool list";
618 val screxp3 = subst_atomic [(fs_,fs),(b1_,b1)] screxp3_;
619 writeln (term2str screxp3);
620 val SOME (equ,_) = rewrite_set_ (theory "Isac") false srls2 screxp3;
621 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 ()
622 else error "biegelinie.sml: rew. Bieglie2 --3";
623 writeln (term2str equ);
625 (Biegelinie_, [makeFunctionTo, equation], [Equation, fromFunction])
630 (c_2 / 2 * x ^^^ 2 + c / 6 * x ^^^ 3 + -1 * q_0 / 24 * x ^^^ 4)),
633 === inhibit exn 110722=============================================================*)
636 "----- execute script by interpreter: setzeRandbedingungenEin";
637 val fmz = ["Funktionen [Q x = c + -1 * q_0 * x,\
638 \M_b x = c_2 + c * x + -1 * q_0 / 2 * x ^^^ 2,\
639 \y' x = c_3 + 1 / (-1 * EI) * (c_2 * x + c / 2 * x ^^^ 2 + -1 * q_0 / 6 * x ^^^ 3),\
640 \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)]",
641 "Randbedingungen [y 0 = 0, y L = 0, M_b 0 = 0, M_b L = 0]",
642 "Gleichungen equs___"];
643 val (dI',pI',mI') = ("Biegelinie", ["setzeRandbedingungen","Biegelinien"],
644 ["Biegelinien","setzeRandbedingungenEin"]);
645 val p = e_pos'; val c = [];
646 (*=== inhibit exn 110722=============================================================
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;
653 "--- before 1.subpbl [Equation, fromFunction]";
654 val (p,_,f,nxt,_,pt) = me nxt p c pt;
655 case nxt of (_, Apply_Method ["Biegelinien", "setzeRandbedingungenEin"])=>()
656 | _ => error "biegelinie.sml: met setzeRandbed*Ein aa";
657 "----- Randbedingung y 0 = 0 in SUBpbl with met [Equation, fromFunction]";
658 val (p,_,f,nxt,_,pt) = me nxt p c pt;
659 if (#1 o (get_obj g_fmz pt)) (fst p) =
660 ["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))",
661 "substitution (y 0 = 0)", "equality equ___"] then ()
662 else error "biegelinie.sml met setzeRandbed*Ein bb";
663 (writeln o istate2str) (get_istate pt p);
664 "--- after 1.subpbl [Equation, fromFunction]";
666 val (p,_,f,nxt,_,pt) = me nxt p c pt;
667 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
668 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
669 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
670 case nxt of (_, Apply_Method["Equation", "fromFunction"]) => ()
671 | _ => error "biegelinie.sml met2 ff";
672 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f =
673 "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)";
674 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
675 val (p,_,f,nxt,_,pt) = me nxt p c pt;
676 case nxt of (_, Check_Postcond ["makeFunctionTo", "equation"]) => ()
677 | _ => error "biegelinie.sml met2 gg";
679 "--- before 2.subpbl [Equation, fromFunction]";
680 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f = "0 = c_4 + 0 / (-1 * EI)" ;
681 case nxt of (_,Subproblem (_, ["makeFunctionTo", "equation"])) => ()
682 | _ => error "biegelinie.sml met2 hh";
683 "--- after 1st arrival at 2.subpbl [Equation, fromFunction]";
685 val (p,_,f,nxt,_,pt) = me nxt p c pt;
686 if (#1 o (get_obj g_fmz pt)) (fst p) =
687 ["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))",
688 "substitution (y L = 0)", "equality equ___"] then ()
689 else error "biegelinie.sml metsetzeRandbed*Ein bb ";
690 val (p,_,f,nxt,_,pt) = me nxt p c pt;
691 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
692 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
694 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
695 case nxt of (_, Apply_Method["Equation", "fromFunction"]) => ()
696 | _ => error "biegelinie.sml met2 ii";
697 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)";
698 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)";
699 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)";
700 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)" ;
701 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)";
702 case nxt of (_,Subproblem (_, ["makeFunctionTo", "equation"])) => ()
703 | _ => error "biegelinie.sml met2 jj";
705 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
706 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
707 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
708 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
709 case nxt of (_, Apply_Method ["Equation", "fromFunction"])=>()
710 | _ => error "biegelinie.sml met2 kk";
712 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*);
713 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f = "0 = c_2 + c * 0 + -1 * q_0 / 2 * 0 ^^^ 2";
714 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f = "0 = c_2";
715 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f = "0 = c_2";
716 val (p,_,f,nxt,_,pt) = me nxt p c pt;
717 case nxt of (_,Subproblem (_, ["makeFunctionTo", "equation"])) => ()
718 | _ => error "biegelinie.sml met2 ll";
720 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
721 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
722 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
723 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
724 case nxt of (_, Apply_Method ["Equation", "fromFunction"])=>()
725 | _ => error "biegelinie.sml met2 mm";
727 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";
728 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";
729 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f = "0 = c_2 + c * L + -1 * q_0 / 2 * L ^^^ 2";
730 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";
731 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";
732 case nxt of (_, Check_Postcond ["setzeRandbedingungen", "Biegelinien"]) => ()
733 | _ => error "biegelinie.sml met2 nn";
734 val (p,_,f,nxt,_,pt) = me nxt p c pt;
735 if nxt = ("End_Proof'", End_Proof') andalso f2str f =
736 (* "[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]" *)
737 "[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]"
738 then () else error "biegelinie.sml met2 oo";
739 === inhibit exn 110722=============================================================*)
742 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
743 val (p,_,f,nxt,_,pt) = me nxt p c pt;
744 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
747 "----------- method [Biegelinien,setzeRandbedingungenEin]FAST ----";
748 "----------- method [Biegelinien,setzeRandbedingungenEin]FAST ----";
749 "----------- method [Biegelinien,setzeRandbedingungenEin]FAST ----";
751 "Script SetzeRandbedScript (funs_::bool list) (rb_::bool list) = \
752 \ (let b1_ = nth_ 1 rb_; \
753 \ (fs_::bool list) = filter_sameFunId (lhs b1_) funs_; \
755 \ (SubProblem (Biegelinie_,[makeFunctionTo,equation],\
756 \ [Equation,fromFunction]) \
757 \ [BOOL (hd fs_), BOOL b1_]) \
758 \ in [e1_,e2_,e3_,e4_])"
763 "----------- IntegrierenUndKonstanteBestimmen2: Bsp.7.70. --------";
764 "----------- IntegrierenUndKonstanteBestimmen2: Bsp.7.70. --------";
765 "----------- IntegrierenUndKonstanteBestimmen2: Bsp.7.70. --------";
768 "Script Belastung2BiegelScript (q__::real) (v_v::real) = \
769 \ (let q___ = Take (q_ v_v = q__); \
770 \ q___ = ((Rewrite sym_real_minus_eq_cancel True) @@ \
771 \ (Rewrite Belastung_Querkraft True)) q___; \
773 \ (SubProblem (Biegelinie_,[named,integrate,function], \
774 \ [diff,integration,named]) \
775 \ [REAL (rhs q___), REAL v_v, real_REAL Q]); \
776 \ M__ = Rewrite Querkraft_Moment True Q__; \
778 \ (SubProblem (Biegelinie_,[named,integrate,function], \
779 \ [diff,integration,named]) \
780 \ [REAL (rhs M__), REAL v_v, real_REAL M_b]); \
781 \ N__ = ((Rewrite Moment_Neigung False) @@ \
782 \ (Rewrite make_fun_explicit False)) M__; \
784 \ (SubProblem (Biegelinie_,[named,integrate,function], \
785 \ [diff,integration,named]) \
786 \ [REAL (rhs N__), REAL v_v, real_REAL y']); \
788 \ (SubProblem (Biegelinie_,[named,integrate,function], \
789 \ [diff,integration,named]) \
790 \ [REAL (rhs N__), REAL v_v, real_REAL y]) \
791 \ in [Q__, M__, N__, B__])"
793 (*=== inhibit exn 110722=============================================================
794 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
796 "----- Bsp 7.70 with me";
797 val fmz = ["Traegerlaenge L","Streckenlast q_0","Biegelinie y",
798 "Randbedingungen [y 0 = 0, y L = 0, M_b 0 = 0, M_b L = 0]",
799 "FunktionsVariable x"];
800 val (dI',pI',mI') = ("Biegelinie", ["Biegelinien"],
801 ["IntegrierenUndKonstanteBestimmen2"]);
802 val p = e_pos'; val c = [];
803 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
804 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
805 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
806 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
807 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
808 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
809 if nxt = ("Apply_Method", Apply_Method ["IntegrierenUndKonstanteBestimmen2"])
810 then () else error "biegelinie.sml met2 a";
812 (*** actual arg(s) missing for '["(#Find, (Funktionen, funs_))"]' i.e. should be 'copy-named' by '*_._'
814 #a# "Script Biegelinie2Script ..
815 \ ... (SubProblem (Biegelinie_,[vonBelastungZu,Biegelinien], \
816 \ [Biegelinien,ausBelastung]) \
817 \ [REAL q__, REAL v_]); \
819 #b# prep_met ... (["Biegelinien","ausBelastung"],
820 ... ("#Given" ,["Streckenlast q__","FunktionsVariable v_v"]),
821 "Script Belastung2BiegelScript (q__::real) (v_v::real) = \
823 #a#b# BOTH HAVE 2 ARGUMENTS q__ and v_v ...OK
824 ##########################################################################
825 BUT THE (#Find, (Funktionen, funs_)) IS NOT COPYNAMED BY funs___ !!!3*_!!!
826 ##########################################################################*)
827 === inhibit exn 110722=============================================================*)
828 "further 'me' see ----- SubProblem (_,[vonBelastungZu,Biegelinien] -------\
829 \ ----- SubProblem (_,[setzeRandbedingungen,Biegelinien] -";
831 "----- Bsp 7.70 with autoCalculate";
832 CalcTree [(["Traegerlaenge L","Streckenlast q_0","Biegelinie y",
833 "Randbedingungen [Q 0 = q_0 * L, M_b L = 0, y 0 = 0, y' 0 = 0]",
834 "FunktionsVariable x"],
835 ("Biegelinie", ["Biegelinien"],
836 ["IntegrierenUndKonstanteBestimmen2"]))];
838 autoCalculate 1 CompleteCalc;
839 val ((pt,p),_) = get_calc 1; show_pt pt;
840 (*=== inhibit exn 110722=============================================================
841 if p = ([], Res) andalso term2str (get_obj g_res pt (fst p)) =
842 "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 ()
843 else error "biegelinie.sml: diff.behav.7.70 with autoCalculate";
844 ===== inhibit exn 110722===========================================================*)
846 val is = get_istate pt ([],Res); writeln (istate2str is);
847 val t = str2term " last \
848 \[Q x = L * q_0 + -1 * q_0 * x, \
849 \ M_b x = -1 * q_0 * L ^^^ 2 / 2 + q_0 * L / 1 * x + -1 * q_0 / 2 * x ^^^ 2,\
851 \ -3 * q_0 * L ^^^ 2 / (-6 * EI) * x + 3 * L * q_0 / (-6 * EI) * x ^^^ 2 +\
852 \ -1 * q_0 / (-6 * EI) * x ^^^ 3, \
854 \ -6 * q_0 * L ^^^ 2 / (-24 * EI) * x ^^^ 2 + \
855 \ 4 * L * q_0 / (-24 * EI) * x ^^^ 3 + \
856 \ -1 * q_0 / (-24 * EI) * x ^^^ 4]";
857 val srls = append_rls "erls_IntegrierenUndK.." e_rls
858 [Calc("Tools.rhs", eval_rhs"eval_rhs_"),
859 Calc ("Atools.ident",eval_ident "#ident_"),
860 Thm ("last_thmI",num_str @{thm last_thmI}),
861 Thm ("if_True",num_str @{thm if_True}),
862 Thm ("if_False",num_str @{thm if_False})
865 val t = str2term "last [1,2,3,4]";
866 trace_rewrite := true;
867 val SOME (e1__,_) = rewrite_set_ thy false srls t;
868 trace_rewrite := false;
871 trace_script := true;
872 trace_script := false;
874 "----------- investigate normalforms in biegelinien --------------";
875 "----------- investigate normalforms in biegelinien --------------";
876 "----------- investigate normalforms in biegelinien --------------";
877 "----- coming from integration:";
878 val Q = str2term "Q x = c + -1 * q_0 * x";
879 val M_b = str2term "M_b x = c_2 + c * x + -1 * q_0 / 2 * x ^^^ 2";
880 val y' = str2term "y' x = c_3 + 1 / (-1 * EI) * (c_2 * x + c / 2 * x ^^^ 2 + -1 * q_0 / 6 * x ^^^ 3)";
881 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)";
882 (*^^^ 1 / (-1 * EI) NOT distributed - ok! ^^^^^^^^^^^^^^^^^^^^^^^*)
884 "----- functions comming from:";