1 (* tests on systems of equations |
|
2 author: Walther Neuper |
|
3 050826, |
|
4 (c) due to copyright terms |
|
5 |
|
6 use"../smltest/IsacKnowledge/eqsystem.sml"; |
|
7 use"eqsystem.sml"; |
|
8 *) |
|
9 val thy = EqSystem.thy; |
|
10 |
|
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 "-----------------------------------------------------------------"; |
|
33 |
|
34 |
|
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"; |
|
40 |
|
41 if occur_exactly_in [str2term"c", str2term"c_2"] all t |
|
42 then () else raise error "eqsystem.sml occur_exactly_in 1"; |
|
43 |
|
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"; |
|
46 |
|
47 if not (occur_exactly_in [str2term"c_2"] all t) |
|
48 then () else raise error "eqsystem.sml occur_exactly_in 3"; |
|
49 |
|
50 |
|
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]"; |
|
56 |
|
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]"; |
|
62 |
|
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]"; |
|
68 |
|
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]"; |
|
73 |
|
74 val t = |
|
75 str2term |
|
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]"; |
|
81 |
|
82 |
|
83 "----------- problems --------------------------------------------"; |
|
84 "----------- problems --------------------------------------------"; |
|
85 "----------- problems --------------------------------------------"; |
|
86 val t = str2term "length_ [x+y=1,y=2] = 2"; |
|
87 atomty t; |
|
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_") |
|
93 ]; |
|
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"; |
|
97 |
|
98 val SOME t = parse EqSystem.thy "solution L"; |
|
99 atomty (term_of t); |
|
100 val SOME t = parse Biegelinie.thy "solution L"; |
|
101 atomty (term_of t); |
|
102 |
|
103 val t = str2term |
|
104 "(tl (tl (tl vs_))) from_ vs_ occur_exactly_in (nth_ 1 (es_::bool list))"; |
|
105 atomty t; |
|
106 val t = str2term |
|
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])"; |
|
109 val SOME (t,_) = |
|
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_") |
|
119 ]) t; |
|
120 if t = HOLogic.true_const then () |
|
121 else raise error "eqsystem.sml ..occur_exactly_in (nth_ 1 [c_4.."; |
|
122 |
|
123 |
|
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"; |
|
132 |
|
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"; |
|
136 |
|
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"; |
|
140 |
|
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"; |
|
145 |
|
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"; |
|
149 |
|
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"; |
|
153 |
|
154 |
|
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"; |
|
165 |
|
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"; |
|
169 |
|
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"; |
|
173 |
|
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"; |
|
177 |
|
178 |
|
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*); |
|
183 val t = |
|
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"; |
|
191 |
|
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"; |
|
195 |
|
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"; |
|
199 |
|
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"; |
|
203 |
|
204 val xxx = rewrite_set_ thy true order_system t; |
|
205 if is_none xxx |
|
206 then () else raise error "eqsystem.sml rewrite in 2x2 simplify_System.3b"; |
|
207 |
|
208 |
|
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"; |
|
219 |
|
220 val SOME (e2__,_) = |
|
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"; |
|
224 |
|
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"; |
|
228 |
|
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"; |
|
233 |
|
234 if not (ord_simplify_System |
|
235 false thy [] |
|
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"; |
|
239 |
|
240 trace_rewrite:=true; |
|
241 trace_rewrite:=false; |
|
242 |
|
243 |
|
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")]; |
|
256 val SOME (t,_) = |
|
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"; |
|
261 |
|
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"; |
|
267 |
|
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"; |
|
274 |
|
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"; |
|
281 |
|
282 |
|
283 "----------- script [EqSystem,normalize,2x2] ---------------------"; |
|
284 "----------- script [EqSystem,normalize,2x2] ---------------------"; |
|
285 "----------- script [EqSystem,normalize,2x2] ---------------------"; |
|
286 val str = |
|
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_ \ |
|
290 \ in ([]))"; |
|
291 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str; |
|
292 val 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])\ |
|
297 \ []))"; |
|
298 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str; |
|
299 val 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_]))" |
|
305 ; |
|
306 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str; |
|
307 val 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_]))" |
|
313 ; |
|
314 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str; |
|
315 val 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_]))" |
|
321 ; |
|
322 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str; |
|
323 val 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_]))" |
|
331 ; |
|
332 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str; |
|
333 val 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_]))" |
|
343 ; |
|
344 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str; |
|
345 val 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_]))" |
|
355 ; |
|
356 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str; |
|
357 val 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_]))" |
|
368 ; |
|
369 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str; |
|
370 val 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_]))" |
|
380 ; |
|
381 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str; |
|
382 (*---^^^-OK-----------------------------------------------------------------*) |
|
383 (*---vvv-NOT ok-------------------------------------------------------------*) |
|
384 |
|
385 |
|
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 --"; |
|
389 val str = |
|
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_ \ |
|
393 \ in ([]))"; |
|
394 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str; |
|
395 val str = |
|
396 "Script SolveSystemScript (es_::bool list) (vs_::real list) = \ |
|
397 \ (let e1__ = Take (hd es_) \ |
|
398 \ in ([]))"; |
|
399 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str; |
|
400 val str = |
|
401 "Script SolveSystemScript (es_::bool list) (vs_::real list) = \ |
|
402 \ (let e1__ = Take (hd es_); \ |
|
403 \ e1__ = Take (hd es_) \ |
|
404 \ in ([]))"; |
|
405 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str; |
|
406 val str = |
|
407 "Script SolveSystemScript (es_::bool list) (vs_::real list) = \ |
|
408 \ (let e1__ = Take (hd es_); \ |
|
409 \ e1__ = (Take (hd es_))\ |
|
410 \ in ([]))"; |
|
411 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str; |
|
412 val str = |
|
413 "Script SolveSystemScript (es_::bool list) (vs_::real list) = \ |
|
414 \ (let e1__ = Take (hd es_); \ |
|
415 \ e1__ = ((Rewrite_Set order_system False)) e1__\ |
|
416 \ in ([]))"; |
|
417 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str; |
|
418 (*--------------------------------------------------------------------------*) |
|
419 val str = |
|
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 (*--------------------------------------------------------------------------*) |
|
424 val str = |
|
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__\ |
|
429 \ in ([]))"; |
|
430 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str; |
|
431 val 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__\ |
|
438 \ in ([]))"; |
|
439 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str; |
|
440 val 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__\ |
|
447 \ in ([]))"; |
|
448 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str; |
|
449 val 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_)) \ |
|
457 \ in ([]))"; |
|
458 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str; |
|
459 val 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__ \ |
|
468 \ in ([]))"; |
|
469 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str; |
|
470 val 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__ \ |
|
479 \ in ([]))"; |
|
480 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str; |
|
481 val 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__ \ |
|
494 \ in [e1__, e2__])" |
|
495 ; |
|
496 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str; |
|
497 val 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__ \ |
|
513 \ in [e1__, e2__])" |
|
514 ; |
|
515 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str; |
|
516 (*---^^^-OK-----------------------------------------------------------------*) |
|
517 val str = |
|
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__)" |
|
534 ; |
|
535 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str; |
|
536 (*---vvv-NOT ok-------------------------------------------------------------*) |
|
537 atomty sc; |
|
538 |
|
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 --"; |
|
542 val str = |
|
543 "Script SolveSystemScript (es_::bool list) (vs_::real list) = \ |
|
544 \ (let es__ = Take es_; \ |
|
545 \ e1__ = hd es__\ |
|
546 \ in ([]))" |
|
547 ; |
|
548 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str; |
|
549 val str = |
|
550 "Script SolveSystemScript (es_::bool list) (vs_::real list) = \ |
|
551 \ (let es__ = Take es_; \ |
|
552 \ e1__ = hd es__; \ |
|
553 \ e2__ = hd (tl es__)\ |
|
554 \ in ([]))" |
|
555 ; |
|
556 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str; |
|
557 val str = |
|
558 "Script SolveSystemScript (es_::bool list) (vs_::real list) = \ |
|
559 \ (let es__ = Take es_; \ |
|
560 \ e1__ = hd es__; \ |
|
561 \ e2__ = hd (tl es__);\ |
|
562 \ es__ = [1=2,3=4]\ |
|
563 \ in ([]))" |
|
564 ; |
|
565 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str; |
|
566 val str = |
|
567 "Script SolveSystemScript (es_::bool list) (vs_::real list) = \ |
|
568 \ (let es__ = Take es_; \ |
|
569 \ e1__ = hd es__; \ |
|
570 \ e2__ = hd (tl es__);\ |
|
571 \ es__ = [e1__,e2__]\ |
|
572 \ in ([]))" |
|
573 ; |
|
574 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str; |
|
575 val str = |
|
576 "Script SolveSystemScript (es_::bool list) (vs_::real list) = \ |
|
577 \ (let es__ = Take es_; \ |
|
578 \ e1__ = hd 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__ \ |
|
583 \ in ([]))" |
|
584 ; |
|
585 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str; |
|
586 val str = |
|
587 "Script SolveSystemScript (es_::bool list) (vs_::real list) = \ |
|
588 \ (let es__ = Take es_; \ |
|
589 \ e1__ = hd 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__ \ |
|
596 \ in ([]))" |
|
597 ; |
|
598 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str; |
|
599 val str = |
|
600 "Script SolveSystemScript (es_::bool list) (vs_::real list) = \ |
|
601 \ (let es__ = Take es_; \ |
|
602 \ e1__ = hd 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__ \ |
|
611 \ in ([]))" |
|
612 ; |
|
613 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str; |
|
614 val str = |
|
615 "Script SolveSystemScript (es_::bool list) (vs_::real list) = \ |
|
616 \ (let es__ = Take es_; \ |
|
617 \ e1__ = hd 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__ \ |
|
626 \ in es__)" |
|
627 ; |
|
628 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str; |
|
629 val str = |
|
630 "Script SolveSystemScript (es_::bool list) (vs_::real list) = \ |
|
631 \ (let es__ = Take es_; \ |
|
632 \ e1__ = hd 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__)" |
|
641 ; |
|
642 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str; |
|
643 (*---^^^-OK-----------------------------------------------------------------*) |
|
644 val str = |
|
645 "Script SolveSystemScript (es_::bool list) (vs_::real list) = \ |
|
646 \ (let es__ = Take es_; \ |
|
647 \ e1__ = hd 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__)" |
|
658 ; |
|
659 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str; |
|
660 (*---vvv-NOT ok-------------------------------------------------------------*) |
|
661 atomty sc; |
|
662 |
|
663 |
|
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"], |
|
674 With = [], |
|
675 Given = |
|
676 [Correct |
|
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]"], |
|
679 Where = [], |
|
680 Relate = []})] => () |
|
681 | _ => raise error "eqsystem.sml refine ['normalize','2x2'...]"; |
|
682 |
|
683 |
|
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 [_,_, |
|
688 Matches |
|
689 (["triangular", "2x2", "linear", "system"], |
|
690 {Find = [Correct "solution L"], |
|
691 With = [], |
|
692 Given = |
|
693 [Correct |
|
694 "equalities [c_2 = 0, L * c + c_2 = q_0 * L ^^^ 2 / 2]", |
|
695 Correct "solveForVars [c, c_2]"], |
|
696 Where = |
|
697 [Correct |
|
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]", |
|
699 Correct |
|
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]"], |
|
701 Relate = []})] => () |
|
702 | _ => raise error "eqsystem.sml refine ['triangular','2x2'...]"; |
|
703 |
|
704 |
|
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"]; |
|
711 (*... resulted in |
|
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]"]*) |
|
714 |
|
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]"; |
|
717 trace_rewrite:=true; |
|
718 val SOME (t',_) = rewrite_set_ thy false prls_triangular t; |
|
719 (*found:... |
|
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"] |
|
727 |
|
728 ... i.e Calc ("op +", eval_binop "#add_") was missing in erls_prls_triangular*) |
|
729 trace_rewrite:=false; |
|
730 (*WN051014------------------------------------------------------------------*) |
|
731 |
|
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,\ |
|
735 \ 0 = c_4, \ |
|
736 \ 0 = c_3]", |
|
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; |
|
741 *) |
|
742 (*print_depth 6; matches; print_depth 3;*) |
|
743 case matches of |
|
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*) |
|
752 |
|
753 val fmz = ["equalities [L * q_0 = c, \ |
|
754 \ 0 = (2 * c_2 + 2 * L * c + -1 * L ^^^ 2 * q_0) / 2,\ |
|
755 \ 0 = c_3, \ |
|
756 \ 0 = c_4]", |
|
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; |
|
760 *) |
|
761 case matches of |
|
762 [Matches (["triangular", "4x4", "linear", "system"], _)] => () |
|
763 | _ => raise error "eqsystem.sml: refine relaxed triangular sys Matches"; |
|
764 val matches = refine fmz ["linear","system"]; |
|
765 |
|
766 |
|
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"]; |
|
775 trace_rewrite:=true; |
|
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"'*) |
|
780 |
|
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)); |
|
785 *) |
|
786 > show_types:=true; term2str (hd where_); show_types:=false; |
|
787 val it = "length_ (es_::real list) = (2::real)" : string |
|
788 |
|
789 =========================================================================\ |
|
790 -------fun prep_pbt |
|
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*)) |
|
796 ], |
|
797 append_rls "e_rls" e_rls [(*for preds in where_*)], |
|
798 SOME "solveSystem es_ vs_", |
|
799 [])); |
|
800 *) |
|
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~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ |
|
807 |
|
808 > val {where_,...} = get_pbt ["2x2", "linear","system"]; |
|
809 > show_types:=true; term2str (hd where_); show_types:=false; |
|
810 |
|
811 =========================================================================/ |
|
812 |
|
813 |
|
814 |
|
815 -----fun refin' ff: |
|
816 > (writeln o (itms2str_ (thy2ctxt "Isac"))) itms; |
|
817 [ |
|
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]))] |
|
824 |
|
825 > (writeln o pres2str) pre'; |
|
826 [ |
|
827 (false, length_ es_ = 2), |
|
828 (true, length_ [c, c_2] = 2)] |
|
829 |
|
830 ----- fun match_oris': |
|
831 > (writeln o (itms2str_ (thy2ctxt "Isac"))) itms; |
|
832 > (writeln o pres2str) pre'; |
|
833 ..as in refin' |
|
834 |
|
835 ----- fun check_preconds' |
|
836 > (writeln o env2str) env; |
|
837 [" |
|
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])"," |
|
840 (vs_, [c, c_2])"," |
|
841 (ss___, L)"] |
|
842 |
|
843 > val es_ = (fst o hd) env; |
|
844 val es_ = Free ("es_", "bool List.list") : Term.term |
|
845 |
|
846 > val pre1 = hd pres; |
|
847 atomty pre1; |
|
848 *** |
|
849 *** Const (op =, [real, real] => bool) |
|
850 *** . Const (ListG.length_, real list => real) |
|
851 *** . . Free (es_, real list) |
|
852 ~~~~~~~~~~~~~~~~~~~^^^^^^^^^ should be bool list~~~~~~~~~~~~~~~~~~~ |
|
853 *** . Free (2, real) |
|
854 *** |
|
855 |
|
856 THE REASON WAS A non-type-constrained variable IN #WHERE OF PROBLEM |
|
857 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ |
|
858 *) |
|
859 |
|
860 |
|
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"]; |
|
867 val (dI',pI',mI') = |
|
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"; |
|
878 |
|
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; |
|
885 case nxt of |
|
886 (_, Subproblem ("Biegelinie.thy", ["triangular", "2x2", "linear",_])) => () |
|
887 | _ => raise error "eqsystem.sml me [EqSystem,normalize,2x2] SubProblem"; |
|
888 |
|
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; |
|
893 case nxt of |
|
894 (_, Specify_Method ["EqSystem", "top_down_substitution", "2x2"]) => () |
|
895 | _ => raise error "eqsystem.sml me [EqSys...2x2] top_down_substitution"; |
|
896 |
|
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; |
|
900 (*[ |
|
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___]))] |
|
904 *) |
|
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; |
|
913 case nxt of |
|
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"; |
|
920 case nxt of |
|
921 (_, End_Proof') => () |
|
922 | _ => raise error "eqsystem.sml me [EqSys...2x2] finished End_Proof'"; |
|
923 |
|
924 |
|
925 "----------- me [linear,system] ..normalize..top_down_sub..-------"; |
|
926 "----------- me [linear,system] ..normalize..top_down_sub..-------"; |
|
927 "----------- me [linear,system] ..normalize..top_down_sub..-------"; |
|
928 val fmz = |
|
929 ["equalities\ |
|
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"]; |
|
935 val (dI',pI',mI') = |
|
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; |
|
951 if 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"; |
|
954 case nxt of |
|
955 (_, Subproblem ("Biegelinie.thy", ["triangular", "2x2", "linear",_])) => () |
|
956 | _ => raise error "eqsystem.sml me [linear,system] SubProblem b"; |
|
957 |
|
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; |
|
962 case nxt of |
|
963 (_, Specify_Method ["EqSystem", "top_down_substitution", "2x2"]) => () |
|
964 | _ => raise error "eqsystem.sml me [EqSys...2x2] top_down_substitution b"; |
|
965 |
|
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; |
|
969 (*[ |
|
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___]))] |
|
973 *) |
|
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; |
|
982 case nxt of |
|
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; |
|
987 if 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"; |
|
990 case nxt of |
|
991 (_, End_Proof') => () |
|
992 | _ => raise error "eqsystem.sml me [EqSys...2x2] finished End_Proof'" b; |
|
993 |
|
994 |
|
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")]; |
|
1002 "------- Bsp 7.27"; |
|
1003 states:=[]; |
|
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"]))]; |
|
1009 moveActiveRoot 1; |
|
1010 (* |
|
1011 trace_script := true; autoCalculate 1 CompleteCalc; trace_script := false; |
|
1012 ##7.27## ordered substs |
|
1013 c_4 c_2 |
|
1014 c c_2 c_3 c_4 c c_2 1->2: c |
|
1015 c_2 c_4 |
|
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), \ |
|
1019 \ 0 = c_2, \ |
|
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; |
|
1022 term2str 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]"; |
|
1024 |
|
1025 |
|
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; |
|
1029 val SOME (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"; |
|
1033 (* |
|
1034 val SOME (t,_) = rewrite_set_inst_ thy false subst isolate_bdvs_4x4 t; |
|
1035 term2str t; |
|
1036 val SOME (t,_) = rewrite_set_inst_ thy false subst simplify_System t; |
|
1037 term2str t; |
|
1038 val SOME (t,_) = rewrite_set_ thy false order_system t; |
|
1039 term2str t; |
|
1040 *) |
|
1041 |
|
1042 "------- Bsp 7.28 ---------------vvvvvvvvvvvvv Momentenlinie postponed"; |
|
1043 states:=[]; |
|
1044 CalcTree [(["Traegerlaenge L","Momentenlinie (-q_0 / L * x^3 / 6)", |
|
1045 "Biegelinie y", |
|
1046 "Randbedingungen [y L = 0, y' L = 0]", |
|
1047 "FunktionsVariable x"], |
|
1048 ("Biegelinie.thy", ["vonMomentenlinieZu","Biegelinien"], |
|
1049 ["Biegelinien", "AusMomentenlinie"]))]; |
|
1050 moveActiveRoot 1; |
|
1051 (* |
|
1052 trace_script := true; autoCalculate 1 CompleteCalc; trace_script := false; |
|
1053 *) |
|
1054 |
|
1055 "------- Bsp 7.69"; |
|
1056 states:=[]; |
|
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"] ))]; |
|
1062 moveActiveRoot 1; |
|
1063 (* |
|
1064 trace_script := true; autoCalculate 1 CompleteCalc; trace_script := false; |
|
1065 ##7.69## ordered subst 2x2 |
|
1066 c_4 c_3 |
|
1067 c c_2 c_3 c_4 c c_2 c_3 1:c_3 -> 2:c c_2 2: c c_2 |
|
1068 c_3 c_4 |
|
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)]"; |
|
1074 |
|
1075 "------- Bsp 7.70"; |
|
1076 states:=[]; |
|
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"] ))]; |
|
1082 moveActiveRoot 1; |
|
1083 (* |
|
1084 trace_script := true; autoCalculate 1 CompleteCalc; trace_script := false; |
|
1085 ##7.70## |subst |
|
1086 c | |
|
1087 c c_2 |1:c -> 2:c_2 |
|
1088 c_3 | |
|
1089 c_4 | GOON test methods @@@@@@@@@@@@@@@@@@@@@@@@@@@*) |
|
1090 |
|
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,\ |
|
1094 \ 0 = c_4, \ |
|
1095 \ 0 = c_3]"; |
|
1096 val SOME (t,_) = |
|
1097 rewrite_ thy e_rew_ord e_rls false (num_str commute_0_equality) t; |
|
1098 val SOME (t,_) = |
|
1099 rewrite_ thy e_rew_ord e_rls false (num_str commute_0_equality) t; |
|
1100 val SOME (t,_) = |
|
1101 rewrite_ thy e_rew_ord e_rls false (num_str commute_0_equality) t; |
|
1102 term2str 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]"; |
|
1104 val SOME (t,_) = |
|
1105 rewrite_set_inst_ thy false subst simplify_System_parenthesized t; |
|
1106 term2str 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; |
|
1109 term2str 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]"; |
|
1111 val SOME (t,_) = |
|
1112 rewrite_set_inst_ thy false subst simplify_System_parenthesized t; |
|
1113 |
|
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"; |
|
1118 |
|
1119 |
|
1120 "----- 7.70 with met normalize: "; |
|
1121 val fmz = ["equalities \ |
|
1122 \[L * q_0 = c, \ |
|
1123 \ 0 = (2 * c_2 + 2 * L * c + -1 * L ^^^ 2 * q_0) / 2,\ |
|
1124 \ 0 = c_4, \ |
|
1125 \ 0 = c_3]", |
|
1126 "solveForVars [c, c_2, c_3, c_4]", "solution L"]; |
|
1127 val (dI',pI',mI') = |
|
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; |
|
1142 |
|
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; |
|
1145 |
|
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 --------------------------------------------------------------------------*) |
|
1153 |
|
1154 "----- 7.70 with met top_down_: "; |
|
1155 "--- scr [EqSystem,top_down_substitution,4x4] -- a saved trial"; |
|
1156 (*---vvv-this script failed with if ?!?-------------------------------------*) |
|
1157 val str = |
|
1158 "Script SolveSystemScript (es_::bool list) (vs_::real list) = \ |
|
1159 \ (let e1_ = hd es_; \ |
|
1160 \ v1_ = hd vs_; \ |
|
1161 \ xxx = if lhs e1_ =!= v1_ \ |
|
1162 \ then 0=0 \ |
|
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_ \ |
|
1169 \ in [e1_, e2_])"; |
|
1170 (*val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;*) |
|
1171 val str = |
|
1172 "Script SolveSystemScript (es_::bool list) (vs_::real list) = \ |
|
1173 \ (let e1_ = hd es_; \ |
|
1174 \ v1_ = hd vs_; \ |
|
1175 \ e2_ = Take (hd (tl es_)); \ |
|
1176 \ e2_ = (Substitute [e1__]) e2_ \ |
|
1177 \ in [e1_, e2_])"; |
|
1178 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str; |
|
1179 (*---^^^-OK-----------------------------------------------------------------*) |
|
1180 (*---vvv-NOT ok-------------------------------------------------------------*) |
|
1181 val str = |
|
1182 "Script SolveSystemScript (es_::bool list) (vs_::real list) = \ |
|
1183 \ (let e1_ = hd es_; \ |
|
1184 \ v1_ = hd vs_; \ |
|
1185 \ xxx = if ((lhs e1_) =!= v1_) then 1 else 2; \ |
|
1186 \ e2_ = Take (hd (tl es_)); \ |
|
1187 \ e2_ = (Substitute [e1__]) e2_ \ |
|
1188 \ in [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; |
|
1192 |
|
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; |
|
1196 |
|
1197 "--- scr [EqSystem,top_down_substitution,4x4] -- adapted only to 7.70"; |
|
1198 val str = |
|
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; |
|
1211 val 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; |
|
1224 val 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; |
|
1237 val 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__] \ |
|
1249 \ in [])" |
|
1250 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str; |
|
1251 val 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; |
|
1265 val 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-----------------------------------------------------------------*) |
|
1282 val str = |
|
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; |
|
1299 |
|
1300 |
|
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"]; |
|
1305 val (dI',pI',mI') = |
|
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"; |
|
1324 |
|
1325 |
|
1326 "------- Bsp 7.71"; |
|
1327 states:=[]; |
|
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"] ))]; |
|
1333 moveActiveRoot 1; |
|
1334 (* |
|
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)]"; |
|
1345 |
|
1346 "------- Bsp 7.72a ---------------vvvvvvvvvvvvv Momentenlinie postponed"; |
|
1347 states:=[]; |
|
1348 CalcTree [(["Traegerlaenge L", |
|
1349 "Momentenlinie ((q_0 * L)/ 6 * x - q_0 /(6 * L) * x^3)", |
|
1350 "Biegelinie y", |
|
1351 "Randbedingungen [y 0 = 0, y L = 0]", |
|
1352 "FunktionsVariable x"], |
|
1353 ("Biegelinie.thy", ["vonMomentenlinieZu","Biegelinien"], |
|
1354 ["Biegelinien", "AusMomentenlinie"]))]; |
|
1355 moveActiveRoot 1; |
|
1356 (* |
|
1357 trace_script := true; autoCalculate 1 CompleteCalc; trace_script := false; |
|
1358 *) |
|
1359 |
|
1360 "------- Bsp 7.72b"; |
|
1361 states:=[]; |
|
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"] ))]; |
|
1367 moveActiveRoot 1; |
|
1368 (* |
|
1369 trace_script := true; autoCalculate 1 CompleteCalc; trace_script := false; |
|
1370 ##7.72b## |ord. |subst.singles |ord.triang. |
|
1371 c_2 | | |c_2 |
|
1372 c c_2 | |1:c_2 -> 2':c |c_2 c |
|
1373 c_4 | | | |
|
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)]"; |
|
1379 |
|
1380 "------- Bsp 7.73 ---------------vvvvvvvvvvvvv Momentenlinie postponed"; |
|
1381 states:=[]; |
|
1382 CalcTree [(["Traegerlaenge L","Momentenlinie ???",(*description unclear*) |
|
1383 "Biegelinie y", |
|
1384 "Randbedingungen [y L = 0, y' L = 0]", |
|
1385 "FunktionsVariable x"], |
|
1386 ("Biegelinie.thy", ["vonMomentenlinieZu","Biegelinien"], |
|
1387 ["Biegelinien", "AusMomentenlinie"]))]; |
|
1388 moveActiveRoot 1; |
|
1389 (* |
|
1390 trace_script := true; autoCalculate 1 CompleteCalc; trace_script := false; |
|
1391 *) |
|
1392 |
|
1393 |
|
1394 "----------- 4x4 systems from Biegelinie -------------------------"; |
|
1395 "----------- 4x4 systems from Biegelinie -------------------------"; |
|
1396 "----------- 4x4 systems from Biegelinie -------------------------"; |
|
1397 (*GOON replace this test with 7.70 *) |
|
1398 "----- Bsp 7.27"; |
|
1399 val fmz = ["equalities \ |
|
1400 \[0 = c_4, \ |
|
1401 \ 0 = c_4 + L * c_3 +(12 * L ^^^ 2 * c_2 + 4 * L ^^^ 3 * c + -1 * L ^^^ 4 * q_0) / (-24 * EI), \ |
|
1402 \ 0 = c_2, \ |
|
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"]; |
|
1405 val (dI',pI',mI') = |
|
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; |
|
1416 "[0 = c_4, \ |
|
1417 \ 0 = c_4 + L * c_3 +\n (12 * L ^^^ 2 * c_2 + 4 * L ^^^ 3 * c + -1 * L ^^^ 4 * q_0) / (-24 * EI), \ |
|
1418 \ 0 = c_2, \ |
|
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; |
|
1424 "[0 = c_4, \ |
|
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))), \ |
|
1429 \ 0 = c_2, \ |
|
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; |
|
1434 "[c_4 = 0,\ |
|
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),\ |
|
1436 \ c_2 = 0, \ |
|
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; |
|
1439 |
|
1440 ---------------------------------------------------------------------*) |
|
1441 |
|
1442 (* |
|
1443 use"../smltest/IsacKnowledge/eqsystem.sml"; |
|
1444 use"eqsystem.sml"; |
|
1445 *) |
|