1 (* tests on systems of equations
4 (c) due to copyright terms
6 use"../smltest/IsacKnowledge/eqsystem.sml";
9 val thy = EqSystem.thy;
11 "-----------------------------------------------------------------";
12 "table of contents -----------------------------------------------";
13 "-----------------------------------------------------------------";
14 "----------- occur_exactly_in ------------------------------------";
15 "----------- problems --------------------------------------------";
16 "----------- rewrite-order ord_simplify_System -------------------";
17 "----------- rewrite in [EqSystem,normalize,2x2] -----------------";
18 "----------- rewrite example from 2nd [EqSystem,normalize,2x2] ---";
19 "----------- rewrite in [EqSystem,top_down_substitution,2x2] -----";
20 "----------- rewrite in [EqSystem,normalize,4x4] -----------------";
21 "----------- script [EqSystem,normalize,2x2] ---------------------";
22 "----------- script [EqSystem,top_down_substitution,2x2] Vers.1 --";
23 "----------- script [EqSystem,top_down_substitution,2x2] Vers.2 --";
24 "----------- refine [linear,system]-------------------------------";
25 "----------- refine [2x2,linear,system] search error--------------";
26 "----------- me [EqSystem,normalize,2x2] -------------------------";
27 "----------- me [linear,system] ..normalize..top_down_sub..-------";
28 "----------- all systems from Biegelinie -------------------------";
29 "----------- 4x4 systems from Biegelinie -------------------------";
30 "-----------------------------------------------------------------";
31 "-----------------------------------------------------------------";
32 "-----------------------------------------------------------------";
35 "----------- occur_exactly_in ------------------------------------";
36 "----------- occur_exactly_in ------------------------------------";
37 "----------- occur_exactly_in ------------------------------------";
38 val all = [str2term"c", str2term"c_2", str2term"c_3"];
39 val t = str2term"0 = -1 * q_0 * L ^^^ 2 / 2 + L * c + c_2";
41 if occur_exactly_in [str2term"c", str2term"c_2"] all t
42 then () else raise error "eqsystem.sml occur_exactly_in 1";
44 if not (occur_exactly_in [str2term"c", str2term"c_2", str2term"c_3"] all t)
45 then () else raise error "eqsystem.sml occur_exactly_in 2";
47 if not (occur_exactly_in [str2term"c_2"] all t)
48 then () else raise error "eqsystem.sml occur_exactly_in 3";
51 val t = str2term"[c,c_2] from_ [c,c_2,c_3] occur_exactly_in \
52 \-1 * q_0 * L ^^^ 2 / 2 + L * c + c_2";
53 val Some (str, t') = eval_occur_exactly_in 0 "EqSystem.occur'_exactly'_in" t 0;
54 if str = "[c, c_2] from_ [c, c_2,\n c_3] occur_exactly_in -1 * q_0 * L ^^^ 2 / 2 + L * c + c_2 = True" then ()
55 else raise error "eval_occur_exactly_in [c, c_2]";
57 val t = str2term"[c,c_2,c_3] from_ [c,c_2,c_3] occur_exactly_in \
58 \-1 * q_0 * L ^^^ 2 / 2 + L * c + c_2";
59 val Some (str, t') = eval_occur_exactly_in 0 "EqSystem.occur'_exactly'_in" t 0;
60 if str = "[c, c_2,\n c_3] from_ [c, c_2,\n c_3] occur_exactly_in -1 * q_0 * L ^^^ 2 / 2 + L * c + c_2 = False" then ()
61 else raise error "eval_occur_exactly_in [c, c_2, c_3]";
63 val t = str2term"[c_2] from_ [c,c_2,c_3] occur_exactly_in \
64 \-1 * q_0 * L ^^^ 2 / 2 + L * c + c_2";
65 val Some (str, t') = eval_occur_exactly_in 0 "EqSystem.occur'_exactly'_in" t 0;
66 if str = "[c_2] from_ [c, c_2,\n c_3] occur_exactly_in -1 * q_0 * L ^^^ 2 / 2 + L * c + c_2 = False" then ()
67 else raise error "eval_occur_exactly_in [c, c_2, c_3]";
69 val t = str2term"[] from_ [c,c_2,c_3] occur_exactly_in 0";
70 val Some (str, t') = eval_occur_exactly_in 0 "EqSystem.occur'_exactly'_in" t 0;
71 if str = "[] from_ [c, c_2, c_3] occur_exactly_in 0 = True" then ()
72 else raise error "eval_occur_exactly_in [c, c_2, c_3]";
76 "[] from_ [c, c_2, c_3, c_4] occur_exactly_in -1 * (q_0 * L ^^^ 2) /2";
77 val Some (str, t') = eval_occur_exactly_in 0 "EqSystem.occur'_exactly'_in" t 0;
78 if str = "[] from_ [c, c_2, c_3, c_4] occur_exactly_in \
79 \-1 * (q_0 * L ^^^ 2) / 2 = True" then ()
80 else raise error "eval_occur_exactly_in [c, c_2, c_3, c_4]";
83 "----------- problems --------------------------------------------";
84 "----------- problems --------------------------------------------";
85 "----------- problems --------------------------------------------";
86 val t = str2term "length_ [x+y=1,y=2] = 2";
88 val testrls = append_rls "testrls" e_rls
89 [(Thm ("length_Nil_",num_str length_Nil_)),
90 (Thm ("length_Cons_",num_str length_Cons_)),
91 Calc ("op +", eval_binop "#add_"),
92 Calc ("op =",eval_equal "#equal_")
94 val Some (t',_) = rewrite_set_ thy false testrls t;
95 if term2str t' = "True" then ()
96 else raise error "eqsystem.sml: length_ [x+y=1,y=2] = 2";
98 val Some t = parse EqSystem.thy "solution L";
100 val Some t = parse Biegelinie.thy "solution L";
104 "(tl (tl (tl vs_))) from_ vs_ occur_exactly_in (nth_ 1 (es_::bool list))";
107 "(tl (tl (tl [c,c_2,c_3,c_4]))) from_ [c,c_2,c_3,c_4] occur_exactly_in \
108 \(nth_ 1 [c_4 = 1, 2=2,3=3,4=4])";
110 rewrite_set_ thy true
111 (append_rls "prls_" e_rls
112 [Thm ("nth_Cons_",num_str nth_Cons_),
113 Thm ("nth_Nil_",num_str nth_Nil_),
114 Thm ("tl_Cons",num_str tl_Cons),
115 Thm ("tl_Nil",num_str tl_Nil),
116 Calc ("EqSystem.occur'_exactly'_in",
117 eval_occur_exactly_in
118 "#eval_occur_exactly_in_")
120 if t = HOLogic.true_const then ()
121 else raise error "eqsystem.sml ..occur_exactly_in (nth_ 1 [c_4..";
124 "----------- rewrite-order ord_simplify_System -------------------";
125 "----------- rewrite-order ord_simplify_System -------------------";
126 "----------- rewrite-order ord_simplify_System -------------------";
127 "M_b x = c * x + -1 * q_0 * (x ^^^ 2 / 2) + c_2";
128 "--- add_commute ---";
129 if ord_simplify_System false thy [] (str2term"-1 * q_0 * (x ^^^ 2 / 2)",
130 str2term"c * x") then ()
131 else raise error "integrate.sml, (-1 * q_0 * (x ^^^ 2 / 2)) < (c * x) not#1";
133 if ord_simplify_System false thy [] (str2term"-1 * q_0 * (x ^^^ 2 / 2)",
134 str2term"c_2") then ()
135 else raise error "integrate.sml, (-1 * q_0 * (x ^^^ 2 / 2)) < (c_2) not#2";
137 if ord_simplify_System false thy [] (str2term"c * x",
138 str2term"c_2") then ()
139 else raise error "integrate.sml, (c * x) < (c_2) not#3";
141 "--- mult_commute ---";
142 if ord_simplify_System false thy [] (str2term"x * c",
143 str2term"c * x") then ()
144 else raise error "integrate.sml, (x * c) < (c * x) not#4";
146 if ord_simplify_System false thy [] (str2term"-1 * q_0 * (x ^^^ 2 / 2) * c",
147 str2term"-1 * q_0 * c * (x ^^^ 2 / 2)")
148 then () else raise error "integrate.sml, (. * .) < (. * .) not#5";
150 if ord_simplify_System false thy [] (str2term"-1 * q_0 * (x ^^^ 2 / 2) * c",
151 str2term"c * -1 * q_0 * (x ^^^ 2 / 2)")
152 then () else raise error "integrate.sml, (. * .) < (. * .) not#6";
155 "----------- rewrite in [EqSystem,normalize,2x2] -----------------";
156 "----------- rewrite in [EqSystem,normalize,2x2] -----------------";
157 "----------- rewrite in [EqSystem,normalize,2x2] -----------------";
158 val t = str2term"[0 = -1 * q_0 * L ^^^ 2 / 2 + L * c + c_2,\
159 \0 = -1 * q_0 * 0 ^^^ 2 / 2 + 0 * c + c_2]";
160 val bdvs = [(str2term"bdv_1",str2term"c"),
161 (str2term"bdv_2",str2term"c_2")];
162 val Some(t,_)= rewrite_set_inst_ thy true bdvs simplify_System_parenthesized t;
163 if term2str t = "[0 = -1 * q_0 * L ^^^ 2 / 2 + (L * c + c_2), 0 = c_2]"
164 then () else raise error "eqsystem.sml rewrite in 2x2 simplify_System_par.1";
166 val Some (t,_) = rewrite_set_inst_ thy true bdvs isolate_bdvs t;
167 if term2str t = "[L * c + c_2 = 0 + -1 * (-1 * q_0 * L ^^^ 2 / 2), c_2 = 0]"
168 then () else raise error "eqsystem.sml rewrite in 2x2 isolate_bdvs";
170 val Some(t,_)= rewrite_set_inst_ thy true bdvs simplify_System t;
171 if term2str t = "[L * c + c_2 = q_0 * L ^^^ 2 / 2, c_2 = 0]"
172 then () else raise error "eqsystem.sml rewrite in 2x2 simplify_System_par.2";
174 val Some (t,_) = rewrite_set_ thy true order_system t;
175 if term2str t = "[c_2 = 0, L * c + c_2 = q_0 * L ^^^ 2 / 2]"
176 then () else raise error "eqsystem.sml rewrite in 2x2 simplify_System_par.3";
179 "----------- rewrite example from 2nd [EqSystem,normalize,2x2] ---";
180 "----------- rewrite example from 2nd [EqSystem,normalize,2x2] ---";
181 "----------- rewrite example from 2nd [EqSystem,normalize,2x2] ---";
182 val thy = Isac.thy (*because of Undeclared constant "Biegelinie.EI*);
184 str2term"[0 = c_2 + c * 0 + 1 / EI * (L * q_0 / 12 * 0 ^^^ 3 + \
185 \ -1 * q_0 / 24 * 0 ^^^ 4),\
186 \ 0 = c_2 + c * L + 1 / EI * (L * q_0 / 12 * L ^^^ 3 + \
187 \ -1 * q_0 / 24 * L ^^^ 4)]";
188 val Some (t,_) = rewrite_set_ thy true norm_Rational t;
189 if term2str t="[0 = c_2, 0 = c_2 + L * c + L ^^^ 4 * q_0 / (EI * 24)]"
190 then () else raise error "eqsystem.sml rewrite in 2x2 simplify_System_par.0b";
192 val Some(t,_)= rewrite_set_inst_ thy true bdvs simplify_System_parenthesized t;
193 if term2str t = "[0 = c_2, 0 = q_0 * L ^^^ 4 / (24 * EI) + (L * c + c_2)]"
194 then () else raise error "eqsystem.sml rewrite in 2x2 simplify_System_par.1b";
196 val Some (t,_) = rewrite_set_inst_ thy true bdvs isolate_bdvs t;
197 if term2str t = "[c_2 = 0, L * c + c_2 = 0 + -1 * (q_0 * L ^^^ 4 / (24 * EI))]"
198 then () else raise error "eqsystem.sml rewrite in 2x2 isolate_bdvs b";
200 val Some(t,_)= rewrite_set_inst_ thy true bdvs simplify_System t;
201 if term2str t = "[c_2 = 0, L * c + c_2 = -1 * q_0 * L ^^^ 4 / (24 * EI)]"
202 then () else raise error "eqsystem.sml rewrite in 2x2 simplify_System.2b";
204 val xxx = rewrite_set_ thy true order_system t;
206 then () else raise error "eqsystem.sml rewrite in 2x2 simplify_System.3b";
209 "----------- rewrite in [EqSystem,top_down_substitution,2x2] -----";
210 "----------- rewrite in [EqSystem,top_down_substitution,2x2] -----";
211 "----------- rewrite in [EqSystem,top_down_substitution,2x2] -----";
212 val e1__ = str2term "c_2 = 77";
213 val e2__ = str2term "L * c + c_2 = q_0 * L ^^^ 2 / 2";
214 val bdvs = [(str2term"bdv_1",str2term"c"),
215 (str2term"bdv_2",str2term"c_2")];
216 val Some (e2__,_) = rewrite_terms_ thy dummy_ord Erls [e1__] e2__;
217 if term2str e2__ = "L * c + 77 = q_0 * L ^^^ 2 / 2" then ()
218 else raise error "eqsystem.sml top_down_substitution,2x2] subst";
221 rewrite_set_inst_ thy true bdvs simplify_System_parenthesized e2__;
222 if term2str e2__ = "77 + L * c = q_0 * L ^^^ 2 / 2" then ()
223 else raise error "eqsystem.sml top_down_substitution,2x2] simpl_par";
225 val Some (e2__,_) = rewrite_set_inst_ thy true bdvs isolate_bdvs e2__;
226 if term2str e2__ = "c = (q_0 * L ^^^ 2 / 2 + -1 * 77) / L" then ()
227 else raise error "eqsystem.sml top_down_substitution,2x2] isolate";
229 val t = str2term "[c_2 = 77, c = (q_0 * L ^^^ 2 / 2 + -1 * 77) / L]";
230 val Some (t,_) = rewrite_set_ thy true order_system t;
231 if term2str t = "[c = (q_0 * L ^^^ 2 / 2 + -1 * 77) / L, c_2 = 77]" then ()
232 else raise error "eqsystem.sml top_down_substitution,2x2] order_system";
234 if not (ord_simplify_System
236 (str2term"[c_2 = 77, c = (q_0 * L ^^^ 2 / 2 + -1 * 77) / L]",
237 str2term"[c = (q_0 * L ^^^ 2 / 2 + -1 * 77) / L, c_2 = 77]"))
238 then () else raise error "eqsystem.sml, order_result rew_ord";
241 trace_rewrite:=false;
244 "----------- rewrite in [EqSystem,normalize,4x4] -----------------";
245 "----------- rewrite in [EqSystem,normalize,4x4] -----------------";
246 "----------- rewrite in [EqSystem,normalize,4x4] -----------------";
247 (*GOON??: revise rewrite in [EqSystem,normalize,4x4] from before 0609*)
248 val t = str2term"[0 = -1 * q_0 * 0 ^^^ 2 / 2 + 0 * c_3 + c_4,\
249 \0 = -1 * q_0 * L ^^^ 2 / 2 + L * c_3 + c_4,\
250 \c + c_2 + c_3 + c_4 = 0,\
251 \c_2 + c_3 + c_4 = 0]";
252 val bdvs = [(str2term"bdv_1",str2term"c"),
253 (str2term"bdv_2",str2term"c_2"),
254 (str2term"bdv_3",str2term"c_3"),
255 (str2term"bdv_4",str2term"c_4")];
257 rewrite_set_inst_ thy true bdvs simplify_System_parenthesized t;
258 if term2str t = "[0 = c_4, 0 = -1 * q_0 * L ^^^ 2 / 2 + (L * c_3 + c_4),\n\
259 \ c + (c_2 + (c_3 + c_4)) = 0, c_2 + (c_3 + c_4) = 0]"
260 then () else raise error "eqsystem.sml rewrite in 4x4 simplify_System_paren";
262 val Some (t,_) = rewrite_set_inst_ thy true bdvs isolate_bdvs t;
263 if term2str t = "[c_4 = 0, \
264 \L * c_3 + c_4 = 0 + -1 * (-1 * q_0 * L ^^^ 2 / 2),\n \
265 \c + (c_2 + (c_3 + c_4)) = 0, c_2 + (c_3 + c_4) = 0]"
266 then () else raise error "eqsystem.sml rewrite in 4x4 isolate_bdvs";
268 val Some(t,_)= rewrite_set_inst_ thy true bdvs simplify_System_parenthesized t;
269 if term2str t = "[c_4 = 0,\
270 \ L * c_3 + c_4 = q_0 * L ^^^ 2 / 2,\
271 \ c + (c_2 + (c_3 + c_4)) = 0,\n\
272 \ c_2 + (c_3 + c_4) = 0]"
273 then () else raise error "eqsystem.sml rewrite in 4x4 simplify_System_p..2";
275 val Some (t,_) = rewrite_set_ thy true order_system t;
276 if term2str t = "[c_4 = 0,\
277 \ L * c_3 + c_4 = q_0 * L ^^^ 2 / 2,\
278 \ c_2 + (c_3 + c_4) = 0,\n\
279 \ c + (c_2 + (c_3 + c_4)) = 0]"
280 then () else raise error "eqsystem.sml rewrite in 4x4 order_system";
283 "----------- script [EqSystem,normalize,2x2] ---------------------";
284 "----------- script [EqSystem,normalize,2x2] ---------------------";
285 "----------- script [EqSystem,normalize,2x2] ---------------------";
287 "Script SolveSystemScript (es_::bool list) (vs_::real list) = \
288 \ (let es__ = (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
289 \ simplify_System_parenthesized False) es_ \
291 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
293 "Script SolveSystemScript (es_::bool list) (vs_::real list) = \
294 \ (let es__ = (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
295 \ simplify_System_parenthesized False) es_ \
296 \ in (SubProblem (Biegelinie_,[linear,system],[no_met])\
298 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
300 "Script SolveSystemScript (es_::bool list) (vs_::real list) = \
301 \ (let es__ = (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
302 \ simplify_System_parenthesized False) es_ \
303 \ in (SubProblem (Biegelinie_,[linear,system],[no_met])\
304 \ [bool_list_ es__, real_list_ vs_]))"
306 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
308 "Script SolveSystemScript (es_::bool list) (vs_::real list) = \
309 \ (let es__ = Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
310 \ simplify_System_parenthesized False) es_ \
311 \ in (SubProblem (Biegelinie_,[linear,system],[no_met])\
312 \ [bool_list_ es__, real_list_ vs_]))"
314 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
316 "Script SolveSystemScript (es_::bool list) (vs_::real list) = \
317 \ (let es__ = (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
318 \ simplify_System_parenthesized False)) es_ \
319 \ in (SubProblem (Biegelinie_,[linear,system],[no_met])\
320 \ [bool_list_ es__, real_list_ vs_]))"
322 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
324 "Script SolveSystemScript (es_::bool list) (vs_::real list) = \
325 \ (let es__ = ((Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
326 \ simplify_System_parenthesized False)) @@\
327 \ (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
328 \ simplify_System_parenthesized False))) es_\
329 \ in (SubProblem (Biegelinie_,[linear,system],[no_met])\
330 \ [bool_list_ es__, real_list_ vs_]))"
332 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
334 "Script SolveSystemScript (es_::bool list) (vs_::real list) = \
335 \ (let es__ = ((Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
336 \ simplify_System_parenthesized False)) @@\
337 \ (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
338 \ simplify_System_parenthesized False)) @@\
339 \ (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
340 \ simplify_System_parenthesized False))) es_\
341 \ in (SubProblem (Biegelinie_,[linear,system],[no_met])\
342 \ [bool_list_ es__, real_list_ vs_]))"
344 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
346 "Script SolveSystemScript (es_::bool list) (vs_::real list) = \
347 \ (let es__ = ((Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
348 \ simplify_System_parenthesized False)) @@\
349 \ (Try (Rewrite_Set_Inst [] isolate_bdvs False)) @@\
350 \ (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
351 \ simplify_System_parenthesized False)) @@\
352 \ (Try (Rewrite_Set order_system False))) es_\
353 \ in (SubProblem (Biegelinie_,[linear,system],[no_met])\
354 \ [bool_list_ es__, real_list_ vs_]))"
356 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
358 "Script SolveSystemScript (es_::bool list) (vs_::real list) = \
359 \ (let es__ = ((Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
360 \ simplify_System_parenthesized False)) @@\
361 \ (Try (Rewrite_Set_Inst [(bdv_1, hd vs_)]\
362 \ isolate_bdvs False)) @@\
363 \ (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
364 \ simplify_System_parenthesized False)) @@\
365 \ (Try (Rewrite_Set order_system False))) es_\
366 \ in (SubProblem (Biegelinie_,[linear,system],[no_met])\
367 \ [bool_list_ es__, real_list_ vs_]))"
369 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
371 "Script SolveSystemScript (es_::bool list) (vs_::real list) = \
372 \ (let es__ = ((Try (Rewrite_Set simplify_System_parenthesized False)) @@\
373 \ (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
374 \ isolate_bdvs False)) @@\
375 \ (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
376 \ simplify_System_parenthesized False)) @@\
377 \ (Try (Rewrite_Set order_system False))) es_\
378 \ in (SubProblem (Biegelinie_,[linear,system],[no_met])\
379 \ [bool_list_ es__, real_list_ vs_]))"
381 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
382 (*---^^^-OK-----------------------------------------------------------------*)
383 (*---vvv-NOT ok-------------------------------------------------------------*)
386 "----------- script [EqSystem,top_down_substitution,2x2] Vers.1 --";
387 "----------- script [EqSystem,top_down_substitution,2x2] Vers.1 --";
388 "----------- script [EqSystem,top_down_substitution,2x2] Vers.1 --";
390 "Script SolveSystemScript (es_::bool list) (vs_::real list) = \
391 \ (let es__ = (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
392 \ simplify_System_parenthesized False) es_ \
394 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
396 "Script SolveSystemScript (es_::bool list) (vs_::real list) = \
397 \ (let e1__ = Take (hd es_) \
399 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
401 "Script SolveSystemScript (es_::bool list) (vs_::real list) = \
402 \ (let e1__ = Take (hd es_); \
403 \ e1__ = Take (hd es_) \
405 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
407 "Script SolveSystemScript (es_::bool list) (vs_::real list) = \
408 \ (let e1__ = Take (hd es_); \
409 \ e1__ = (Take (hd es_))\
411 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
413 "Script SolveSystemScript (es_::bool list) (vs_::real list) = \
414 \ (let e1__ = Take (hd es_); \
415 \ e1__ = ((Rewrite_Set order_system False)) e1__\
417 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
418 (*--------------------------------------------------------------------------*)
420 "(Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
421 \ isolate_bdvs False) (e1__::bool)";
422 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
423 (*--------------------------------------------------------------------------*)
425 "Script SolveSystemScript (es_::bool list) (vs_::real list) = \
426 \ (let e1__ = Take (hd es_); \
427 \ e1__ = ((Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
428 \ isolate_bdvs False)) e1__\
430 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
432 "Script SolveSystemScript (es_::bool list) (vs_::real list) = \
433 \ (let e1__ = Take (hd es_); \
434 \ e1__ = ((Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
435 \ isolate_bdvs False)) @@\
436 \ (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
437 \ simplify_System False)) e1__\
439 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
441 "Script SolveSystemScript (es_::bool list) (vs_::real list) = \
442 \ (let e1__ = Take (hd es_); \
443 \ e1__ = ((Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
444 \ isolate_bdvs False)) @@\
445 \ (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
446 \ simplify_System False))) e1__\
448 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
450 "Script SolveSystemScript (es_::bool list) (vs_::real list) = \
451 \ (let e1__ = Take (hd es_); \
452 \ e1__ = ((Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
453 \ isolate_bdvs False)) @@ \
454 \ (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
455 \ simplify_System False))) e1__; \
456 \ e2__ = Take (hd (tl es_)) \
458 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
460 "Script SolveSystemScript (es_::bool list) (vs_::real list) = \
461 \ (let e1__ = Take (hd es_); \
462 \ e1__ = ((Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
463 \ isolate_bdvs False)) @@ \
464 \ (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
465 \ simplify_System False))) e1__; \
466 \ e2__ = Take (hd (tl es_)); \
467 \ e2__ = Substitute [e1__] e2__ \
469 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
471 "Script SolveSystemScript (es_::bool list) (vs_::real list) = \
472 \ (let e1__ = Take (hd es_); \
473 \ e1__ = ((Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
474 \ isolate_bdvs False)) @@ \
475 \ (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
476 \ simplify_System False))) e1__; \
477 \ e2__ = Take (hd (tl es_)); \
478 \ e2__ = ((Substitute [e1__])) e2__ \
480 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
482 "Script SolveSystemScript (es_::bool list) (vs_::real list) = \
483 \ (let e1__ = Take (hd es_); \
484 \ e1__ = ((Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
485 \ isolate_bdvs False)) @@ \
486 \ (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
487 \ simplify_System False))) e1__; \
488 \ e2__ = Take (hd (tl es_)); \
489 \ e2__ = ((Substitute [e1__]) @@ \
490 \ (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
491 \ isolate_bdvs False)) @@ \
492 \ (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
493 \ simplify_System False))) e2__ \
496 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
498 "Script SolveSystemScript (es_::bool list) (vs_::real list) = \
499 \ (let e1__ = Take (hd es_); \
500 \ e1__ = ((Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
501 \ isolate_bdvs False)) @@ \
502 \ (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
503 \ simplify_System False))) e1__; \
504 \ e2__ = Take (hd (tl es_)); \
505 \ e2__ = ((Substitute [e1__]) @@ \
506 \ (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
507 \ simplify_System_parenthesized False)) @@ \
508 \ (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
509 \ isolate_bdvs False)) @@ \
510 \ (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
511 \ simplify_System False)) @@ \
512 \ (Try (Rewrite_Set order_system False))) e2__ \
515 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
516 (*---^^^-OK-----------------------------------------------------------------*)
518 "Script SolveSystemScript (es_::bool list) (vs_::real list) = \
519 \ (let e1__ = Take (hd es_); \
520 \ e1__ = ((Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
521 \ isolate_bdvs False)) @@ \
522 \ (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
523 \ simplify_System False))) e1__; \
524 \ e2__ = Take (hd (tl es_)); \
525 \ e2__ = ((Substitute [e1__]) @@ \
526 \ (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
527 \ simplify_System_parenthesized False)) @@ \
528 \ (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
529 \ isolate_bdvs False)) @@ \
530 \ (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
531 \ simplify_System False))) e2__; \
532 \ es__ = Take [e1__, e2__]\
533 \ in (Try (Rewrite_Set order_system False)) es__)"
535 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
536 (*---vvv-NOT ok-------------------------------------------------------------*)
539 "----------- script [EqSystem,top_down_substitution,2x2] Vers.2 --";
540 "----------- script [EqSystem,top_down_substitution,2x2] Vers.2 --";
541 "----------- script [EqSystem,top_down_substitution,2x2] Vers.2 --";
543 "Script SolveSystemScript (es_::bool list) (vs_::real list) = \
544 \ (let es__ = Take es_; \
548 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
550 "Script SolveSystemScript (es_::bool list) (vs_::real list) = \
551 \ (let es__ = Take es_; \
553 \ e2__ = hd (tl es__)\
556 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
558 "Script SolveSystemScript (es_::bool list) (vs_::real list) = \
559 \ (let es__ = Take es_; \
561 \ e2__ = hd (tl es__);\
565 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
567 "Script SolveSystemScript (es_::bool list) (vs_::real list) = \
568 \ (let es__ = Take es_; \
570 \ e2__ = hd (tl es__);\
571 \ es__ = [e1__,e2__]\
574 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
576 "Script SolveSystemScript (es_::bool list) (vs_::real list) = \
577 \ (let es__ = Take es_; \
579 \ e2__ = hd (tl es__);\
580 \ es__ = [e1__, Substitute [e1__] e2__];\
581 \ es__ = (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
582 \ simplify_System False)) es__ \
585 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
587 "Script SolveSystemScript (es_::bool list) (vs_::real list) = \
588 \ (let es__ = Take es_; \
590 \ e2__ = hd (tl es__);\
591 \ es__ = [e1__, Substitute [e1__] e2__];\
592 \ es__ = ((Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
593 \ isolate_bdvs False)) @@ \
594 \ (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
595 \ simplify_System False))) es__ \
598 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
600 "Script SolveSystemScript (es_::bool list) (vs_::real list) = \
601 \ (let es__ = Take es_; \
603 \ e2__ = hd (tl es__);\
604 \ es__ = [e1__, Substitute [e1__] e2__];\
605 \ es__ = ((Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
606 \ simplify_System_parenthesized False)) @@ \
607 \ (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
608 \ isolate_bdvs False)) @@ \
609 \ (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
610 \ simplify_System False))) es__ \
613 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
615 "Script SolveSystemScript (es_::bool list) (vs_::real list) = \
616 \ (let es__ = Take es_; \
618 \ e2__ = hd (tl es__); \
619 \ es__ = [e1__, Substitute [e1__] e2__]; \
620 \ es__ = ((Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
621 \ simplify_System_parenthesized False)) @@ \
622 \ (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
623 \ isolate_bdvs False)) @@ \
624 \ (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
625 \ simplify_System False))) es__ \
628 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
630 "Script SolveSystemScript (es_::bool list) (vs_::real list) = \
631 \ (let es__ = Take es_; \
633 \ e2__ = hd (tl es__); \
634 \ es__ = [e1__, Substitute [e1__] e2__] \
635 \ in ((Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
636 \ simplify_System_parenthesized False)) @@ \
637 \ (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))] \
638 \ isolate_bdvs False)) @@ \
639 \ (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
640 \ simplify_System False))) es__)"
642 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
643 (*---^^^-OK-----------------------------------------------------------------*)
645 "Script SolveSystemScript (es_::bool list) (vs_::real list) = \
646 \ (let es__ = Take es_; \
648 \ e2__ = hd (tl es__); \
649 \ es__ = [e1__, Substitute [e1__] e2__] "^
650 (* this ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ is a script-'Expr'
651 which is not yet searched for 'STac's; thus this script does not yet work*)
652 " in ((Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
653 \ simplify_System_parenthesized False)) @@ \
654 \ (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))] \
655 \ isolate_bdvs False)) @@ \
656 \ (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
657 \ simplify_System False))) es__)"
659 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
660 (*---vvv-NOT ok-------------------------------------------------------------*)
664 "----------- refine [linear,system]-------------------------------";
665 "----------- refine [linear,system]-------------------------------";
666 "----------- refine [linear,system]-------------------------------";
667 val fmz = ["equalities [0 = -1 * q_0 * 0 ^^^ 2 / 2 + 0 * c + c_2,\
668 \0 = -1 * q_0 * L ^^^ 2 / 2 + L * c + c_2]",
669 "solveForVars [c, c_2]", "solution L"];
670 val matches = refine fmz ["linear","system"];
671 case matches of [_,_,_,
672 Matches (["normalize", "2x2", "linear", "system"],
673 {Find = [Correct "solution L"],
677 "equalities\n [0 = -1 * q_0 * 0 ^^^ 2 / 2 + 0 * c + c_2,\n 0 = -1 * q_0 * L ^^^ 2 / 2 + L * c + c_2]",
678 Correct "solveForVars [c, c_2]"],
681 | _ => raise error "eqsystem.sml refine ['normalize','2x2'...]";
684 val fmz = ["equalities [c_2 = 0, L * c + c_2 = q_0 * L ^^^ 2 / 2]",
685 "solveForVars [c, c_2]", "solution L"];
686 val matches = refine fmz ["linear","system"];
687 case matches of [_,_,
689 (["triangular", "2x2", "linear", "system"],
690 {Find = [Correct "solution L"],
694 "equalities [c_2 = 0, L * c + c_2 = q_0 * L ^^^ 2 / 2]",
695 Correct "solveForVars [c, c_2]"],
698 "tl [c, c_2] from_ [c, c_2] occur_exactly_in nth_ 1\n [c_2 = 0, L * c + c_2 = q_0 * L ^^^ 2 / 2]",
700 "[c, c_2] from_ [c, c_2] occur_exactly_in nth_ 2\n [c_2 = 0, L * c + c_2 = q_0 * L ^^^ 2 / 2]"],
702 | _ => raise error "eqsystem.sml refine ['triangular','2x2'...]";
705 (*WN051014----------------------------------------------------------------
706 the above 'val matches = refine fmz ["linear","system"]'
707 didn't work anymore; we investigated in these steps:*)
708 val fmz = ["equalities [c_2 = 0, L * c + c_2 = q_0 * L ^^^ 2 / 2]",
709 "solveForVars [c, c_2]", "solution L"];
710 val matches = refine fmz ["triangular", "2x2", "linear","system"];
712 False "[c, c_2] from_ [c, c_2] occur_exactly_in nth_ 2\n
713 [c_2 = 0, L * c + c_2 = q_0 * L ^^^ 2 / 2]"]*)
715 val t = str2term"[c, c_2] from_ [c, c_2] occur_exactly_in nth_ 2\
716 \[c_2 = 0, L * c + c_2 = q_0 * L ^^^ 2 / 2]";
718 val Some (t',_) = rewrite_set_ thy false prls_triangular t;
720 ## try thm: nth_Cons_
721 ### eval asms: 1 < 2 + - 1
722 ==> nth_ (2 + - 1) [L * c + c_2 = q_0 * L ^^^ 2 / 2] =
723 nth_ (2 + - 1 + - 1) []
724 #### rls: erls_prls_triangular on: 1 < 2 + - 1
725 ##### try calc: op <'
726 ### asms accepted: ["1 < 2 + - 1"] stored: ["1 < 2 + -1"]
728 ... i.e Calc ("op +", eval_binop "#add_") was missing in erls_prls_triangular*)
729 trace_rewrite:=false;
730 (*WN051014------------------------------------------------------------------*)
732 "----- relaxed preconditions for triangular system";
733 val fmz = ["equalities [L * q_0 = c, \
734 \ 0 = (2 * c_2 + 2 * L * c + -1 * L ^^^ 2 * q_0) / 2,\
737 "solveForVars [c, c_2, c_3, c_4]", "solution L"];
738 val matches = refine fmz ["linear","system"];
739 (* trace_rewrite := true;
740 trace_rewrite := false;
742 (*print_depth 6; matches; print_depth 3;*)
744 [Matches (["linear", "system"], _),
745 NoMatch (["2x2", "linear", "system"], _),
746 NoMatch (["3x3", "linear", "system"], _),
747 Matches (["4x4", "linear", "system"], _),
748 NoMatch (["triangular", "4x4", "linear", "system"], _),
749 Matches (["normalize", "4x4", "linear", "system"], _)] => ()
750 | _ => raise error "eqsystem.sml: refine relaxed triangular sys NoMatch";
751 (*WN060914 does NOT match, because 3rd and 4th equ are not ordered*)
753 val fmz = ["equalities [L * q_0 = c, \
754 \ 0 = (2 * c_2 + 2 * L * c + -1 * L ^^^ 2 * q_0) / 2,\
757 "solveForVars [c, c_2, c_3, c_4]", "solution L"];
758 val matches = refine fmz ["triangular", "4x4", "linear","system"];
759 (* print_depth 11; matches; print_depth 3;
762 [Matches (["triangular", "4x4", "linear", "system"], _)] => ()
763 | _ => raise error "eqsystem.sml: refine relaxed triangular sys Matches";
764 val matches = refine fmz ["linear","system"];
767 "----------- refine [2x2,linear,system] search error--------------";
768 "----------- refine [2x2,linear,system] search error--------------";
769 "----------- refine [2x2,linear,system] search error--------------";
770 (*didn't go into ["2x2", "linear", "system"];
771 we investigated in these steps:*)
772 val fmz = ["equalities [0 = -1 * q_0 * 0 ^^^ 2 / 2 + 0 * c + c_2,\
773 \0 = -1 * q_0 * L ^^^ 2 / 2 + L * c + c_2]",
774 "solveForVars [c, c_2]", "solution L"];
776 val matches = refine fmz ["2x2", "linear","system"];
777 trace_rewrite:=false;
778 print_depth 11; matches; print_depth 3;
779 (*brought: 'False "length_ es_ = 2"'*)
781 (*-----fun refin' (pblRD:pblRD) fmz pbls ((Ptyp (pI,[py],[])):pbt ptyp) =
782 (* val ((pblRD:pblRD), fmz, pbls, ((Ptyp (pI,[py],[])):pbt ptyp)) =
783 (rev ["linear","system"], fmz, [(*match list*)],
784 ((Ptyp ("2x2",[get_pbt ["2x2","linear","system"]],[])):pbt ptyp));
786 > show_types:=true; term2str (hd where_); show_types:=false;
787 val it = "length_ (es_::real list) = (2::real)" : string
789 =========================================================================\
791 (* val (thy, (pblID, dsc_dats: (string * (string list)) list,
792 ev:rls, ca: string option, metIDs:metID list)) =
793 (EqSystem.thy, (["system"],
794 [("#Given" ,["equalities es_", "solveForVars vs_"]),
795 ("#Find" ,["solution ss___"](*___ is copy-named*))
797 append_rls "e_rls" e_rls [(*for preds in where_*)],
798 Some "solveSystem es_ vs_",
801 > val [("#Given", [equalities_es_, "solveForVars vs_"])] = gi;
802 val equalities_es_ = "equalities es_" : string
803 > val (dd, ii) = (split_did o term_of o the o (parse thy)) equalities_es_;
804 > show_types:=true; term2str ii; show_types:=false;
805 val it = "es_::bool list" : string
806 ~~~~~~~~~~~~~~~^^^^^^^^^ OK~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
808 > val {where_,...} = get_pbt ["2x2", "linear","system"];
809 > show_types:=true; term2str (hd where_); show_types:=false;
811 =========================================================================/
816 > (writeln o (itms2str_ (thy2ctxt "Isac"))) itms;
818 (1 ,[1] ,true ,#Given ,Cor equalities
819 [0 = -1 * q_0 * 0 ^^^ 2 / 2 + 0 * c + c_2,
820 0 = -1 * q_0 * L ^^^ 2 / 2 + L * c + c_2] ,(es_, [[0 = -1 * q_0 * 0 ^^^ 2 / 2 + 0 * c + c_2,
821 0 = -1 * q_0 * L ^^^ 2 / 2 + L * c + c_2]])),
822 (2 ,[1] ,true ,#Given ,Cor solveForVars [c, c_2] ,(vs_, [[c, c_2]])),
823 (3 ,[1] ,true ,#Find ,Cor solution L ,(ss___, [L]))]
825 > (writeln o pres2str) pre';
827 (false, length_ es_ = 2),
828 (true, length_ [c, c_2] = 2)]
830 ----- fun match_oris':
831 > (writeln o (itms2str_ (thy2ctxt "Isac"))) itms;
832 > (writeln o pres2str) pre';
835 ----- fun check_preconds'
836 > (writeln o env2str) env;
838 (es_, [0 = -1 * q_0 * 0 ^^^ 2 / 2 + 0 * c + c_2,
839 0 = -1 * q_0 * L ^^^ 2 / 2 + L * c + c_2])","
843 > val es_ = (fst o hd) env;
844 val es_ = Free ("es_", "bool List.list") : Term.term
846 > val pre1 = hd pres;
849 *** Const (op =, [real, real] => bool)
850 *** . Const (ListG.length_, real list => real)
851 *** . . Free (es_, real list)
852 ~~~~~~~~~~~~~~~~~~~^^^^^^^^^ should be bool list~~~~~~~~~~~~~~~~~~~
856 THE REASON WAS A non-type-constrained variable IN #WHERE OF PROBLEM
857 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
861 "----------- me [EqSystem,normalize,2x2] -------------------------";
862 "----------- me [EqSystem,normalize,2x2] -------------------------";
863 "----------- me [EqSystem,normalize,2x2] -------------------------";
864 val fmz = ["equalities [0 = -1 * q_0 * 0 ^^^ 2 / 2 + 0 * c + c_2,\
865 \0 = -1 * q_0 * L ^^^ 2 / 2 + L * c + c_2]",
866 "solveForVars [c, c_2]", "solution L"];
868 ("Biegelinie.thy",["normalize", "2x2", "linear", "system"],
869 ["EqSystem","normalize","2x2"]);
870 val p = e_pos'; val c = [];
871 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
872 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
873 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
874 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
875 val (p,_,f,nxt,_,pt) = me nxt p c pt;
876 case nxt of ("Specify_Method",_) => ()
877 | _ => raise error "eqsystem.sml [EqSystem,normalize,2x2] specify";
879 val (p,_,f,nxt,_,pt) = me nxt p c pt;
880 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
881 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f(*["(bdv_1, c)", "(bdv_2, hd (tl [c, c_2] ... corrected srls; ran only AFTER use"RCODE-root.sml", store_met was NOT SUFFICIENT*);
882 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
883 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
884 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
886 (_, Subproblem ("Biegelinie.thy", ["triangular", "2x2", "linear",_])) => ()
887 | _ => raise error "eqsystem.sml me [EqSystem,normalize,2x2] SubProblem";
889 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
890 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
891 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
892 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
894 (_, Specify_Method ["EqSystem", "top_down_substitution", "2x2"]) => ()
895 | _ => raise error "eqsystem.sml me [EqSys...2x2] top_down_substitution";
897 val (p,_,f,nxt,_,pt) = me nxt p c pt;
898 val PblObj {probl,...} = get_obj I pt [5];
899 (writeln o (itms2str_ (thy2ctxt "Isac"))) probl;
901 (1 ,[1] ,true ,#Given ,Cor equalities [c_2 = 0, L * c + c_2 = q_0 * L ^^^ 2 / 2] ,(es_, [[c_2 = 0, L * c + c_2 = q_0 * L ^^^ 2 / 2]])),
902 (2 ,[1] ,true ,#Given ,Cor solveForVars [c, c_2] ,(vs_, [[c, c_2]])),
903 (3 ,[1] ,true ,#Find ,Cor solution ss___ ,(ss___, [ss___]))]
905 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
906 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
907 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
908 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
909 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
910 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
911 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
912 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
914 (_, Check_Postcond ["triangular", "2x2", "linear", "system"]) => ()
915 | _ => raise error "eqsystem.sml me Subpbl .[EqSys...2x2] finished";
916 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
917 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
918 if f2str f = "[c = L * q_0 / 2, c_2 = 0]" then ()
919 else raise error "eqsystem.sml me [EqSys...2x2] finished f2str f";
921 (_, End_Proof') => ()
922 | _ => raise error "eqsystem.sml me [EqSys...2x2] finished End_Proof'";
925 "----------- me [linear,system] ..normalize..top_down_sub..-------";
926 "----------- me [linear,system] ..normalize..top_down_sub..-------";
927 "----------- me [linear,system] ..normalize..top_down_sub..-------";
930 \[0 = c_2 + c * 0 + 1 / EI * (L * q_0 / 12 * 0 ^^^ 3 + \
931 \ -1 * q_0 / 24 * 0 ^^^ 4),\
932 \ 0 = c_2 + c * L + 1 / EI * (L * q_0 / 12 * L ^^^ 3 + \
933 \ -1 * q_0 / 24 * L ^^^ 4)]",
934 "solveForVars [c, c_2]", "solution L"];
936 ("Biegelinie.thy",["linear", "system"], ["no_met"]);
937 val p = e_pos'; val c = [];
938 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
939 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
940 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
941 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
942 val (p,_,f,nxt,_,pt) = me nxt p c pt;
943 case nxt of (_,Specify_Method ["EqSystem", "normalize", "2x2"]) => ()
944 | _ => raise error "eqsystem.sml [linear,system] specify b";
945 val (p,_,f,nxt,_,pt) = me nxt p c pt;
946 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
947 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
948 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
949 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
950 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
952 "[c_2 = 0, L * c + c_2 = -1 * q_0 * L ^^^ 4 / (24 * EI)]"
953 then () else raise error "eqsystem.sml me simpl. before SubProblem b";
955 (_, Subproblem ("Biegelinie.thy", ["triangular", "2x2", "linear",_])) => ()
956 | _ => raise error "eqsystem.sml me [linear,system] SubProblem b";
958 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
959 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
960 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
961 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
963 (_, Specify_Method ["EqSystem", "top_down_substitution", "2x2"]) => ()
964 | _ => raise error "eqsystem.sml me [EqSys...2x2] top_down_substitution b";
966 val (p,_,f,nxt,_,pt) = me nxt p c pt;
967 val PblObj {probl,...} = get_obj I pt [5];
968 (writeln o (itms2str_ (thy2ctxt "Isac"))) probl;
970 (1 ,[1] ,true ,#Given ,Cor equalities [c_2 = 0, L * c + c_2 = q_0 * L ^^^ 2 / 2] ,(es_, [[c_2 = 0, L * c + c_2 = q_0 * L ^^^ 2 / 2]])),
971 (2 ,[1] ,true ,#Given ,Cor solveForVars [c, c_2] ,(vs_, [[c, c_2]])),
972 (3 ,[1] ,true ,#Find ,Cor solution ss___ ,(ss___, [ss___]))]
974 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
975 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
976 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
977 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
978 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
979 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
980 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
981 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
983 (_, Check_Postcond ["triangular", "2x2", "linear", "system"]) => ()
984 | _ => raise error "eqsystem.sml me Subpbl .[EqSys...2x2] finished b";
985 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
986 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
988 "[c = -1 * q_0 * L ^^^ 4 / (24 * EI * L), c_2 = 0]"
989 then () else raise error "eqsystem.sml me [EqSys...2x2] finished f2str f b";
991 (_, End_Proof') => ()
992 | _ => raise error "eqsystem.sml me [EqSys...2x2] finished End_Proof'" b;
995 "----------- all systems from Biegelinie -------------------------";
996 "----------- all systems from Biegelinie -------------------------";
997 "----------- all systems from Biegelinie -------------------------";
998 val subst = [(str2term "bdv_1", str2term "c"),
999 (str2term "bdv_2", str2term "c_2"),
1000 (str2term "bdv_3", str2term "c_3"),
1001 (str2term "bdv_4", str2term "c_4")];
1004 CalcTree [(["Traegerlaenge L","Streckenlast q_0","Biegelinie y",
1005 "Randbedingungen [y 0 = 0, y L = 0, M_b 0 = 0, M_b L = 0]",
1006 "FunktionsVariable x"],
1007 ("Biegelinie.thy", ["Biegelinien"],
1008 ["IntegrierenUndKonstanteBestimmen2"]))];
1011 trace_script := true; autoCalculate 1 CompleteCalc; trace_script := false;
1012 ##7.27## ordered substs
1014 c c_2 c_3 c_4 c c_2 1->2: c
1016 c c_2 c c_2 c_3 c_4 [2':c, 1:c_2, 3:c_4] -> 4:c_3*)
1017 val t = str2term"[0 = c_4, \
1018 \ 0 = c_4 + L * c_3 +(12 * L ^^^ 2 * c_2 + 4 * L ^^^ 3 * c + -1 * L ^^^ 4 * q_0) / (-24 * EI), \
1020 \ 0 = (2 * c_2 + 2 * L * c + -1 * L ^^^ 2 * q_0) / 2]";
1021 val Some (t',_) = rewrite_set_ thy false isolate_bdvs_4x4 t;
1023 "[c_4 = 0,\n (12 * L ^^^ 2 * c_2 + 4 * L ^^^ 3 * c + -1 * L ^^^ 4 * q_0) / (-24 * EI) =\n 0 + -1 * (c_4 + L * c_3),\n c_2 = 0, (2 * c_2 + 2 * L * c + -1 * L ^^^ 2 * q_0) / 2 = 0]";
1026 "----- 7.27 go through the rewrites in met_eqsys_norm_4x4";
1027 val t = str2term "0 = (2 * c_2 + 2 * L * c + -1 * L ^^^ 2 * q_0) / 2";
1028 val None = rewrite_set_ thy false norm_Rational t;
1030 rewrite_set_inst_ thy false subst simplify_System_parenthesized t;
1031 term2str t = "0 = -1 * q_0 * L ^^^ 2 / 2 + (L * c + c_2)";
1032 "--- isolate_bdvs_4x4";
1034 val Some (t,_) = rewrite_set_inst_ thy false subst isolate_bdvs_4x4 t;
1036 val Some (t,_) = rewrite_set_inst_ thy false subst simplify_System t;
1038 val Some (t,_) = rewrite_set_ thy false order_system t;
1042 "------- Bsp 7.28 ---------------vvvvvvvvvvvvv Momentenlinie postponed";
1044 CalcTree [(["Traegerlaenge L","Momentenlinie (-q_0 / L * x^3 / 6)",
1046 "Randbedingungen [y L = 0, y' L = 0]",
1047 "FunktionsVariable x"],
1048 ("Biegelinie.thy", ["vonMomentenlinieZu","Biegelinien"],
1049 ["Biegelinien", "AusMomentenlinie"]))];
1052 trace_script := true; autoCalculate 1 CompleteCalc; trace_script := false;
1057 CalcTree [(["Traegerlaenge L","Streckenlast q_0","Biegelinie y",
1058 "Randbedingungen [y 0 = 0, y L = 0, y' 0 = 0, y' L = 0]",
1059 "FunktionsVariable x"],
1060 ("Biegelinie.thy", ["Biegelinien"],
1061 ["IntegrierenUndKonstanteBestimmen2"] ))];
1064 trace_script := true; autoCalculate 1 CompleteCalc; trace_script := false;
1065 ##7.69## ordered subst 2x2
1067 c c_2 c_3 c_4 c c_2 c_3 1:c_3 -> 2:c c_2 2: c c_2
1069 c c_2 c_3 c c_2 c_3 c_4 3:c_4 -> 4:c c_2 c_3 1:c_3 -> 4:c c_2*)
1070 val t = str2term"[0 = c_4 + 0 / (-1 * EI), \
1071 \ 0 = c_4 + L * c_3 + (12 * L ^^^ 2 * c_2 + 4 * L ^^^ 3 * c + -1 * L ^^^ 4 * q_0) / (-24 * EI), \
1072 \ 0 = c_3 + 0 / (-1 * EI), \
1073 \ 0 = c_3 + (6 * L * c_2 + 3 * L ^^^ 2 * c + -1 * L ^^^ 3 * q_0) / (-6 * EI)]";
1077 CalcTree [(["Traegerlaenge L","Streckenlast q_0","Biegelinie y",
1078 "Randbedingungen [Q 0 = q_0 * L, M_b L = 0, y 0 = 0, y' 0 = 0]",
1079 "FunktionsVariable x"],
1080 ("Biegelinie.thy", ["Biegelinien"],
1081 ["IntegrierenUndKonstanteBestimmen2"] ))];
1084 trace_script := true; autoCalculate 1 CompleteCalc; trace_script := false;
1089 c_4 | GOON test methods @@@@@@@@@@@@@@@@@@@@@@@@@@@*)
1091 "----- 7.70 go through the rewrites in met_eqsys_norm_4x4";
1092 val t = str2term"[L * q_0 = c, \
1093 \ 0 = (2 * c_2 + 2 * L * c + -1 * L ^^^ 2 * q_0) / 2,\
1097 rewrite_ thy e_rew_ord e_rls false (num_str commute_0_equality) t;
1099 rewrite_ thy e_rew_ord e_rls false (num_str commute_0_equality) t;
1101 rewrite_ thy e_rew_ord e_rls false (num_str commute_0_equality) t;
1103 "[L * q_0 = c, (2 * c_2 + 2 * L * c + -1 * L ^^^ 2 * q_0) / 2 = 0, c_4 = 0,\n c_3 = 0]";
1105 rewrite_set_inst_ thy false subst simplify_System_parenthesized t;
1107 "[L * q_0 = c, -1 * q_0 * L ^^^ 2 / 2 + (L * c + c_2) = 0, c_4 = 0, c_3 = 0]";
1108 val Some (t,_) = rewrite_set_inst_ thy false subst isolate_bdvs_4x4 t;
1110 "[c = (-1 * (L * q_0) + 0) / -1,\n L * c + c_2 = -1 * (-1 * q_0 * L ^^^ 2 / 2) + 0, c_4 = 0, c_3 = 0]";
1112 rewrite_set_inst_ thy false subst simplify_System_parenthesized t;
1114 term2str t ="[c = L * q_0, L * c + c_2 = q_0 * L ^^^ 2 / 2, c_4 = 0, c_3 = 0]";
1115 val Some (t,_) = rewrite_set_ thy false order_system t;
1116 if term2str t ="[c = L * q_0, L * c + c_2 = q_0 * L ^^^ 2 / 2, c_3 = 0, c_4 = 0]" then ()
1117 else raise error "eqsystem.sml: exp 7.70 normalize 4x4 by rewrite changed";
1120 "----- 7.70 with met normalize: ";
1121 val fmz = ["equalities \
1123 \ 0 = (2 * c_2 + 2 * L * c + -1 * L ^^^ 2 * q_0) / 2,\
1126 "solveForVars [c, c_2, c_3, c_4]", "solution L"];
1128 ("Biegelinie.thy",["linear", "system"],["no_met"]);
1129 val p = e_pos'; val c = [];
1130 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
1131 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1132 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1133 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1134 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1135 case nxt of (_,Apply_Method ["EqSystem", "normalize", "4x4"]) => ()
1136 | _ => raise error "eqsystem.sml [EqSystem,normalize,4x4] specify";
1137 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
1138 "bbbbbbbbbbbbbbbbbbbbbbbbbbbbb outcommented vvvvvvvvvvvvvvvvvvvvvv";
1139 (*vvvWN080102 Exception- Match raised
1140 since assod Rewrite .. Rewrite'_Set
1141 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
1143 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
1144 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
1146 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
1147 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
1148 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
1149 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
1150 if f2str f ="[c = L * q_0, L * c + c_2 = q_0 * L ^^^ 2 / 2, c_3 = 0, c_4 = 0]"
1151 then () else raise error "eqsystem.sml: exp 7.70 normalize 4x4 by met changed";
1152 --------------------------------------------------------------------------*)
1154 "----- 7.70 with met top_down_: ";
1155 "--- scr [EqSystem,top_down_substitution,4x4] -- a saved trial";
1156 (*---vvv-this script failed with if ?!?-------------------------------------*)
1158 "Script SolveSystemScript (es_::bool list) (vs_::real list) = \
1159 \ (let e1_ = hd es_; \
1161 \ xxx = if lhs e1_ =!= v1_ \
1163 \ else let e1_ = Take e1_; \
1164 \ e1_ = (Rewrite_Set_Inst [(bdv_1, hd vs_), \
1165 \ (bdv_2, hd (tl vs_))] \
1166 \ isolate_bdvs False) e1_; \
1167 \ e2_ = Take (hd (tl es_)); \
1168 \ e2_ = (Substitute [e1__]) e2_ \
1170 (*val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;*)
1172 "Script SolveSystemScript (es_::bool list) (vs_::real list) = \
1173 \ (let e1_ = hd es_; \
1175 \ e2_ = Take (hd (tl es_)); \
1176 \ e2_ = (Substitute [e1__]) e2_ \
1178 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
1179 (*---^^^-OK-----------------------------------------------------------------*)
1180 (*---vvv-NOT ok-------------------------------------------------------------*)
1182 "Script SolveSystemScript (es_::bool list) (vs_::real list) = \
1183 \ (let e1_ = hd es_; \
1185 \ xxx = if ((lhs e1_) =!= v1_) then 1 else 2; \
1186 \ e2_ = Take (hd (tl es_)); \
1187 \ e2_ = (Substitute [e1__]) e2_ \
1189 (*val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;*)
1190 val str = "if lhs e1_ =!= v1_ then 1 else 2";
1191 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
1193 val str = "let xxx = (if lhs e1_ =!= v1_ then 1 else 2) in xxx";
1194 (*val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;*)
1195 atomty sc; term2str sc;
1197 "--- scr [EqSystem,top_down_substitution,4x4] -- adapted only to 7.70";
1199 "Script SolveSystemScript (es_::bool list) (vs_::real list) = \
1200 \ (let e2__ = Take (hd (tl es_)); \
1201 \ e2__ = ((Substitute [e1__]) @@ \
1202 \ (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
1203 \ simplify_System_parenthesized False)) @@ \
1204 \ (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
1205 \ isolate_bdvs False)) @@ \
1206 \ (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
1207 \ simplify_System False))) e2__;\
1208 \ es__ = Take [e1__, e2__] \
1209 \ in (Try (Rewrite_Set order_system False)) es__)"
1210 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
1212 "Script SolveSystemScript (es_::bool list) (vs_::real list) = \
1213 \ (let e2__ = Take (nth_ 2 es_); \
1214 \ e2__ = ((Substitute [e1__]) @@ \
1215 \ (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
1216 \ simplify_System_parenthesized False)) @@ \
1217 \ (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
1218 \ isolate_bdvs False)) @@ \
1219 \ (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]\
1220 \ simplify_System False))) e2__;\
1221 \ es__ = Take [e1__, e2__] \
1222 \ in (Try (Rewrite_Set order_system False)) es__)"
1223 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
1225 "Script SolveSystemScript (es_::bool list) (vs_::real list) = \
1226 \ (let e2__ = Take (nth_ 2 es_); \
1227 \ e2__ = ((Substitute [e1__]) @@ \
1228 \ (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, nth_ 2 vs_)] \
1229 \ simplify_System_parenthesized False)) @@ \
1230 \ (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, nth_ 2 vs_)]\
1231 \ isolate_bdvs False)) @@ \
1232 \ (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, nth_ 2 vs_)]\
1233 \ simplify_System False))) e2__;\
1234 \ es__ = Take [e1__, e2__] \
1235 \ in (Try (Rewrite_Set order_system False)) es__)"
1236 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
1238 "Script SolveSystemScript (es_::bool list) (vs_::real list) = \
1239 \ (let e2__ = Take (nth_ 2 es_); \
1240 \ e2__ = ((Substitute [e1__]) @@ \
1241 \ (Try (Rewrite_Set_Inst [(bdv_1,nth_ 1 vs_),(bdv_2,nth_ 2 vs_),\
1242 \ (bdv_3,nth_ 3 vs_),(bdv_4,nth_ 4 vs_)]\
1243 \ simplify_System_parenthesized False)) @@ \
1244 \ (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, nth_ 2 vs_)] \
1245 \ isolate_bdvs False)) @@ \
1246 \ (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, nth_ 2 vs_)] \
1247 \ norm_Rational False))) e2__; \
1248 \ es__ = Take [e1__, e2__] \
1250 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
1252 "Script SolveSystemScript (es_::bool list) (vs_::real list) = \
1253 \ (let e2_ = Take (nth_ 2 es_); \
1254 \ e2_ = ((Substitute [e1_]) @@ \
1255 \ (Try (Rewrite_Set_Inst [(bdv_1,nth_ 1 vs_),(bdv_2,nth_ 2 vs_),\
1256 \ (bdv_3,nth_ 3 vs_),(bdv_4,nth_ 4 vs_)]\
1257 \ simplify_System_parenthesized False)) @@ \
1258 \ (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, nth_ 2 vs_)] \
1259 \ isolate_bdvs False)) @@ \
1260 \ (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, nth_ 2 vs_)] \
1261 \ norm_Rational False))) e2_; \
1262 \ es_ = Take [e1_, e2_] \
1263 \ in [e1_, e2_,e3_, e4_])"
1264 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
1266 "Script SolveSystemScript (es_::bool list) (vs_::real list) = \
1267 \ (let e2_ = Take (nth_ 2 es_); \
1268 \ e2_ = ((Substitute [e1_]) @@ \
1269 \ (Try (Rewrite_Set_Inst [(bdv_1,nth_ 1 vs_),(bdv_2,nth_ 2 vs_),\
1270 \ (bdv_3,nth_ 3 vs_),(bdv_4,nth_ 4 vs_)]\
1271 \ simplify_System_parenthesized False)) @@ \
1272 \ (Try (Rewrite_Set_Inst [(bdv_1,nth_ 1 vs_),(bdv_2,nth_ 2 vs_),\
1273 \ (bdv_3,nth_ 3 vs_),(bdv_4,nth_ 4 vs_)]\
1274 \ isolate_bdvs False)) @@ \
1275 \ (Try (Rewrite_Set_Inst [(bdv_1,nth_ 1 vs_),(bdv_2,nth_ 2 vs_),\
1276 \ (bdv_3,nth_ 3 vs_),(bdv_4,nth_ 4 vs_)]\
1277 \ norm_Rational False))) e2_; \
1278 \ es_ = Take [e1_, e2_] \
1279 \ in [e1_, e2_,e3_, e4_])"
1280 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
1281 (*---^^^-OK-----------------------------------------------------------------*)
1283 "Script SolveSystemScript (es_::bool list) (vs_::real list) = \
1284 \ (let e2_ = Take (nth_ 2 es_); \
1285 \ e2_ = ((Substitute [e1_]) @@ \
1286 \ (Try (Rewrite_Set_Inst [(bdv_1,nth_ 1 vs_),(bdv_2,nth_ 2 vs_),\
1287 \ (bdv_3,nth_ 3 vs_),(bdv_4,nth_ 4 vs_)]\
1288 \ simplify_System_parenthesized False)) @@ \
1289 \ (Try (Rewrite_Set_Inst [(bdv_1,nth_ 1 vs_),(bdv_2,nth_ 2 vs_),\
1290 \ (bdv_3,nth_ 3 vs_),(bdv_4,nth_ 4 vs_)]\
1291 \ isolate_bdvs False)) @@ \
1292 \ (Try (Rewrite_Set_Inst [(bdv_1,nth_ 1 vs_),(bdv_2,nth_ 2 vs_),\
1293 \ (bdv_3,nth_ 3 vs_),(bdv_4,nth_ 4 vs_)]\
1294 \ norm_Rational False))) e2_ \
1295 \ in [e1_, e2_, nth_ 3 es_, nth_ 4 es_])"
1296 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
1297 (*---vvv-NOT ok-------------------------------------------------------------*)
1298 atomty sc; term2str sc;
1301 "----- 7.70 with met top_down_: me";
1302 val fmz = ["equalities \
1303 \[c = L * q_0, L * c + c_2 = q_0 * L ^^^ 2 / 2, c_3 = 0, c_4 = 0]",
1304 "solveForVars [c, c_2, c_3, c_4]", "solution L"];
1306 ("Biegelinie.thy",["linear", "system"],["no_met"]);
1307 val p = e_pos'; val c = [];
1308 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
1309 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1310 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1311 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1312 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1313 case nxt of (_,Apply_Method ["EqSystem", "top_down_substitution", "4x4"]) => ()
1314 | _ => raise error "eqsystem.sml [EqSystem,top_down_,4x4] specify";
1315 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
1316 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
1317 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
1318 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
1319 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
1320 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
1321 if nxt = ("End_Proof'", End_Proof') andalso
1322 f2str f = "[c = L * q_0, c_2 = -1 * L ^^^ 2 * q_0 / 2, c_3 = 0, c_4 = 0]"
1323 then () else raise error "eqsystem.sml: 7.70 with met top_down_: me";
1328 CalcTree [(["Traegerlaenge L","Streckenlast q_0","Biegelinie y",
1329 "Randbedingungen [M_b L = 0, y 0 = 0, y L = 0, y' 0 = 0]",
1330 "FunktionsVariable x"],
1331 ("Biegelinie.thy", ["Biegelinien"],
1332 ["IntegrierenUndKonstanteBestimmen2"] ))];
1335 trace_script := true; autoCalculate 1 CompleteCalc; trace_script := false;
1336 ##7.71## |ordered |subst.singles (recurs) |2x2 |diagonal
1337 c c_2 |c c_2 |1' |1': c c_2 |
1338 c_4 | c_3 |2:c_3 -> 4' :c c_2 c_4 | |
1339 c c_2 c_3 c_4 | c_4 |3' | |
1340 c_3 |c c_2 c_3 c_4 |3:c_4 -> 4'':c c_2 |4'':c c_2 | *)
1341 val t = str2term"[0 = (2 * c_2 + 2 * L * c + -1 * L ^^^ 2 * q_0) / 2, \
1342 \ 0 = c_4 + 0 / (-1 * EI), \
1343 \ 0 = c_4 + L * c_3 +(12 * L ^^^ 2 * c_2 + 4 * L ^^^ 3 * c + -1 * L ^^^ 4 * q_0) /(-24 * EI),\
1344 \ 0 = c_3 + 0 / (-1 * EI)]";
1346 "------- Bsp 7.72a ---------------vvvvvvvvvvvvv Momentenlinie postponed";
1348 CalcTree [(["Traegerlaenge L",
1349 "Momentenlinie ((q_0 * L)/ 6 * x - q_0 /(6 * L) * x^3)",
1351 "Randbedingungen [y 0 = 0, y L = 0]",
1352 "FunktionsVariable x"],
1353 ("Biegelinie.thy", ["vonMomentenlinieZu","Biegelinien"],
1354 ["Biegelinien", "AusMomentenlinie"]))];
1357 trace_script := true; autoCalculate 1 CompleteCalc; trace_script := false;
1360 "------- Bsp 7.72b";
1362 CalcTree [(["Traegerlaenge L","Streckenlast (q_0 / L * x)","Biegelinie y",
1363 "Randbedingungen [M_b 0 = 0, M_b L = 0, y 0 = 0, y L = 0]",
1364 "FunktionsVariable x"],
1365 ("Biegelinie.thy", ["Biegelinien"],
1366 ["IntegrierenUndKonstanteBestimmen2"] ))];
1369 trace_script := true; autoCalculate 1 CompleteCalc; trace_script := false;
1370 ##7.72b## |ord. |subst.singles |ord.triang.
1372 c c_2 | |1:c_2 -> 2':c |c_2 c
1374 c c_2 c_3 c_4 | |3:c_4 -> 4':c c_2 c_3 |c_2 c c_3*)
1375 val t = str2term"[0 = c_2, \
1376 \ 0 = (6 * c_2 + 6 * L * c + -1 * L ^^^ 2 * q_0) / 6, \
1377 \ 0 = c_4 + 0 / (-1 * EI), \
1378 \ 0 = c_4 + L * c_3 + (60 * L ^^^ 2 * c_2 + 20 * L ^^^ 3 * c + -1 * L ^^^ 4 * q_0) / (-120 * EI)]";
1380 "------- Bsp 7.73 ---------------vvvvvvvvvvvvv Momentenlinie postponed";
1382 CalcTree [(["Traegerlaenge L","Momentenlinie ???",(*description unclear*)
1384 "Randbedingungen [y L = 0, y' L = 0]",
1385 "FunktionsVariable x"],
1386 ("Biegelinie.thy", ["vonMomentenlinieZu","Biegelinien"],
1387 ["Biegelinien", "AusMomentenlinie"]))];
1390 trace_script := true; autoCalculate 1 CompleteCalc; trace_script := false;
1394 "----------- 4x4 systems from Biegelinie -------------------------";
1395 "----------- 4x4 systems from Biegelinie -------------------------";
1396 "----------- 4x4 systems from Biegelinie -------------------------";
1397 (*GOON replace this test with 7.70 *)
1399 val fmz = ["equalities \
1401 \ 0 = c_4 + L * c_3 +(12 * L ^^^ 2 * c_2 + 4 * L ^^^ 3 * c + -1 * L ^^^ 4 * q_0) / (-24 * EI), \
1403 \ 0 = (2 * c_2 + 2 * L * c + -1 * L ^^^ 2 * q_0) / 2]",
1404 "solveForVars [c, c_2, c_3, c_4]", "solution L"];
1406 ("Biegelinie.thy",["normalize", "4x4", "linear", "system"],
1407 ["EqSystem","normalize","4x4"]);
1408 val p = e_pos'; val c = [];
1409 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
1410 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
1411 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
1412 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
1413 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
1414 "------------------------------------------- Apply_Method...";
1415 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
1417 \ 0 = c_4 + L * c_3 +\n (12 * L ^^^ 2 * c_2 + 4 * L ^^^ 3 * c + -1 * L ^^^ 4 * q_0) / (-24 * EI), \
1419 \ 0 = (2 * c_2 + 2 * L * c + -1 * L ^^^ 2 * q_0) / 2]";
1420 (*vvvWN080102 Exception- Match raised
1421 since assod Rewrite .. Rewrite'_Set
1422 "------------------------------------------- simplify_System_parenthesized...";
1423 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
1425 \ 0 = -1 * q_0 * L ^^^ 4 / (-24 * EI) + \
1426 \ (4 * L ^^^ 3 * c / (-24 * EI) + \
1427 \ (12 * L ^^^ 2 * c_2 / (-24 * EI) + \
1428 \ (L * c_3 + c_4))), \
1430 \ 0 = -1 * q_0 * L ^^^ 2 / 2 + (L * c + c_2)]";
1431 (*? "(4 * L ^^^ 3 / (-24 * EI) * c" statt "(4 * L ^^^ 3 * c / (-24 * EI)" ?*)
1432 "------------------------------------------- isolate_bdvs...";
1433 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
1435 \ c_4 = 0 + -1 * (-1 * q_0 * L ^^^ 4 / (-24 * EI)) + -1 * (4 * L ^^^ 3 * c / (-24 * EI)) + -1 * (12 * L ^^^ 2 * c_2 / (-24 * EI)) + -1 * (L * c_3),\
1437 \ c_2 = 0 + -1 * (-1 * q_0 * L ^^^ 2 / 2) + -1 * (L * c)]";
1438 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
1440 ---------------------------------------------------------------------*)
1443 use"../smltest/IsacKnowledge/eqsystem.sml";