Test_Isac works again, perfectly ..
# the same tests works as in 8df4b6196660 (the *child* of "Test_Isac works...")
# ..EXCEPT those marked with "exception Div raised"
# for general state of tests see Test_Isac section {* history of tests *}.
1 (* tests on systems of equations
2 author: Walther Neuper 050826,
3 (c) due to copyright terms
6 trace_rewrite := false;
7 "-----------------------------------------------------------------";
8 "table of contents -----------------------------------------------";
9 "-----------------------------------------------------------------";
10 "----------- occur_exactly_in ------------------------------------";
11 "----------- problems --------------------------------------------";
12 "----------- rewrite-order ord_simplify_System -------------------";
13 "----------- rewrite in [EqSystem,normalize,2x2] -----------------";
14 "----------- rewrite example from 2nd [EqSystem,normalize,2x2] ---";
15 "----------- rewrite in [EqSystem,top_down_substitution,2x2] -----";
16 "----------- rewrite in [EqSystem,normalize,4x4] -----------------";
17 "----------- script [EqSystem,top_down_substitution,2x2] Vers.1 --";
18 "----------- refine [linear,system]-------------------------------";
19 "----------- refine [2x2,linear,system] search error--------------";
20 "----------- me [EqSystem,normalize,2x2] -------------------------";
21 "----------- me [linear,system] ..normalize..top_down_sub..-------";
22 "----------- all systems from Biegelinie -------------------------";
23 "----------- 4x4 systems from Biegelinie -------------------------";
24 "-----------------------------------------------------------------";
25 "-----------------------------------------------------------------";
26 "-----------------------------------------------------------------";
28 val thy = @{theory "EqSystem"};
29 val ctxt = Proof_Context.init_global thy;
31 "----------- occur_exactly_in ------------------------------------";
32 "----------- occur_exactly_in ------------------------------------";
33 "----------- occur_exactly_in ------------------------------------";
34 val all = [str2term"c", str2term"c_2", str2term"c_3"];
35 val t = str2term"0 = -1 * q_0 * L ^^^ 2 / 2 + L * c + c_2";
37 if occur_exactly_in [str2term"c", str2term"c_2"] all t
38 then () else error "eqsystem.sml occur_exactly_in 1";
40 if not (occur_exactly_in [str2term"c", str2term"c_2", str2term"c_3"] all t)
41 then () else error "eqsystem.sml occur_exactly_in 2";
43 if not (occur_exactly_in [str2term"c_2"] all t)
44 then () else error "eqsystem.sml occur_exactly_in 3";
46 val t = str2term"[c,c_2] from [c,c_2,c_3] occur_exactly_in -1 * q_0 * L ^^^ 2 / 2 + L * c + c_2";
47 eval_occur_exactly_in 0 "EqSystem.occur'_exactly'_in" t 0;
48 val SOME (str, t') = eval_occur_exactly_in 0 "EqSystem.occur'_exactly'_in" t 0;
49 if str = "[c, c_2] from [c, c_2,\n" ^
50 " c_3] occur_exactly_in -1 * q_0 * L ^^^ 2 / 2 + L * c + c_2 = True"
51 then () else error "eval_occur_exactly_in [c, c_2]";
53 val t = str2term ("[c,c_2,c_3] from [c,c_2,c_3] occur_exactly_in " ^
54 "-1 * q_0 * L ^^^ 2 / 2 + L * c + c_2");
55 val SOME (str, t') = eval_occur_exactly_in 0 "EqSystem.occur'_exactly'_in" t 0;
56 if str = "[c, c_2,\n c_3] from [c, c_2,\n" ^
57 " c_3] occur_exactly_in -1 * q_0 * L ^^^ 2 / 2 + L * c + c_2 = False"
58 then () else error "eval_occur_exactly_in [c, c_2, c_3]";
60 val t = str2term"[c_2] from [c,c_2,c_3] occur_exactly_in \
61 \-1 * q_0 * L ^^^ 2 / 2 + L * c + c_2";
62 val SOME (str, t') = eval_occur_exactly_in 0 "EqSystem.occur'_exactly'_in" t 0;
63 if str = "[c_2] from [c, c_2,\n" ^
64 " c_3] occur_exactly_in -1 * q_0 * L ^^^ 2 / 2 + L * c + c_2 = False"
65 then () else error "eval_occur_exactly_in [c, c_2, c_3]";
67 val t = str2term"[] from [c,c_2,c_3] occur_exactly_in 0";
68 val SOME (str, t') = eval_occur_exactly_in 0 "EqSystem.occur'_exactly'_in" t 0;
69 if str = "[] from [c, c_2, c_3] occur_exactly_in 0 = True" then ()
70 else error "eval_occur_exactly_in [c, c_2, c_3]";
74 "[] from [c, c_2, c_3, c_4] occur_exactly_in -1 * (q_0 * L ^^^ 2) /2";
75 val SOME (str, t') = eval_occur_exactly_in 0 "EqSystem.occur'_exactly'_in" t 0;
76 if str = "[] from [c, c_2, c_3, c_4] occur_exactly_in \
77 \-1 * (q_0 * L ^^^ 2) / 2 = True" then ()
78 else error "eval_occur_exactly_in [c, c_2, c_3, c_4]";
80 "----------- problems --------------------------------------------";
81 "----------- problems --------------------------------------------";
82 "----------- problems --------------------------------------------";
83 val t = str2term "LENGTH [x+y=1,y=2] = 2";
85 val testrls = append_rls "testrls" e_rls
86 [(Thm ("LENGTH_NIL",num_str @{thm LENGTH_NIL})),
87 (Thm ("LENGTH_CONS",num_str @{thm LENGTH_CONS})),
88 Calc ("Groups.plus_class.plus", eval_binop "#add_"),
89 Calc ("HOL.eq",eval_equal "#equal_")
91 val SOME (t',_) = rewrite_set_ thy false testrls t;
92 if term2str t' = "True" then ()
93 else error "eqsystem.sml: length_ [x+y=1,y=2] = 2";
95 val SOME t = parse thy "solution LL";
97 val SOME t = parse thy "solution LL";
101 "(tl (tl (tl v_s))) from v_s occur_exactly_in (NTH 1 (e_s::bool list))";
103 val t = str2term ("(tl (tl (tl [c, c_2, c_3, c_4]))) from [c, c_2, c_3, c_4] occur_exactly_in " ^
104 "(NTH 1 [c_4 = 1, 2 = 2, 3 = 3, 4 = 4])");
106 rewrite_set_ thy true
107 (append_rls "prls_" e_rls
108 [Thm ("NTH_CONS",num_str @{thm NTH_CONS}),
109 Thm ("NTH_NIL",num_str @{thm NTH_NIL}),
110 Thm ("TL_CONS",num_str @{thm tl_Cons}),
111 Thm ("TL_NIL",num_str @{thm tl_Nil}),
112 Calc ("EqSystem.occur'_exactly'_in", eval_occur_exactly_in "#eval_occur_exactly_in_")
114 if t = @{term True} then ()
115 else error "eqsystem.sml ..occur_exactly_in (nth_ 1 [c_4..";
117 "----------- rewrite-order ord_simplify_System -------------------";
118 "----------- rewrite-order ord_simplify_System -------------------";
119 "----------- rewrite-order ord_simplify_System -------------------";
120 "M_b x = c * x + -1 * q_0 * (x ^^^ 2 / 2) + c_2";
121 "--- add_commute ---";
122 if ord_simplify_System false thy [] (str2term"-1 * q_0 * (x ^^^ 2 / 2)",
123 str2term"c * x") then ()
124 else error "integrate.sml, (-1 * q_0 * (x ^^^ 2 / 2)) < (c * x) not#1";
126 if ord_simplify_System false thy [] (str2term"-1 * q_0 * (x ^^^ 2 / 2)",
127 str2term"c_2") then ()
128 else error "integrate.sml, (-1 * q_0 * (x ^^^ 2 / 2)) < (c_2) not#2";
130 if ord_simplify_System false thy [] (str2term"c * x",
131 str2term"c_2") then ()
132 else error "integrate.sml, (c * x) < (c_2) not#3";
134 "--- mult_commute ---";
135 if ord_simplify_System false thy [] (str2term"x * c",
136 str2term"c * x") then ()
137 else error "integrate.sml, (x * c) < (c * x) not#4";
139 if ord_simplify_System false thy [] (str2term"-1 * q_0 * (x ^^^ 2 / 2) * c",
140 str2term"-1 * q_0 * c * (x ^^^ 2 / 2)")
141 then () else error "integrate.sml, (. * .) < (. * .) not#5";
143 if ord_simplify_System false thy [] (str2term"-1 * q_0 * (x ^^^ 2 / 2) * c",
144 str2term"c * -1 * q_0 * (x ^^^ 2 / 2)")
145 then () else error "integrate.sml, (. * .) < (. * .) not#6";
148 "----------- rewrite in [EqSystem,normalize,2x2] -----------------";
149 "----------- rewrite in [EqSystem,normalize,2x2] -----------------";
150 "----------- rewrite in [EqSystem,normalize,2x2] -----------------";
151 val t = str2term"[0 = -1 * q_0 * L ^^^ 2 / 2 + L * c + c_2,\
152 \0 = -1 * q_0 * 0 ^^^ 2 / 2 + 0 * c + c_2]";
153 val bdvs = [(str2term"bdv_1",str2term"c"),
154 (str2term"bdv_2",str2term"c_2")];
155 val SOME(t,_)= rewrite_set_inst_ thy true bdvs simplify_System_parenthesized t;
156 if term2str t = "[0 = -1 * q_0 * L ^^^ 2 / 2 + (L * c + c_2), 0 = c_2]"
157 then () else error "eqsystem.sml rewrite in 2x2 simplify_System_par.1";
159 val SOME (t,_) = rewrite_set_inst_ thy true bdvs isolate_bdvs t;
160 if term2str t = "[L * c + c_2 = 0 + -1 * (-1 * q_0 * L ^^^ 2 / 2), c_2 = 0]"then () else error "eqsystem.sml rewrite in 2x2 isolate_bdvs";
162 val SOME(t,_)= rewrite_set_inst_ thy true bdvs simplify_System t;
163 if term2str t = "[L * c + c_2 = q_0 * L ^^^ 2 / 2, c_2 = 0]"
164 then () else error "eqsystem.sml rewrite in 2x2 simplify_System_par.2";
166 "--- 3--- see EqSystem.thy (*..if replaced by 'and' ...";
167 val SOME (t,_) = rewrite_set_ thy true order_system t;
168 if term2str t = "[c_2 = 0, L * c + c_2 = q_0 * L ^^^ 2 / 2]"
169 then () else error "eqsystem.sml rewrite in 2x2 simplify_System_par.3";
172 "----------- rewrite example from 2nd [EqSystem,normalize,2x2] ---";
173 "----------- rewrite example from 2nd [EqSystem,normalize,2x2] ---";
174 "----------- rewrite example from 2nd [EqSystem,normalize,2x2] ---";
175 val thy = @{theory "Isac"} (*because of Undeclared constant "Biegelinie.EI*);
177 str2term"[0 = c_2 + c * 0 + 1 / EI * (L * q_0 / 12 * 0 ^^^ 3 + \
178 \ -1 * q_0 / 24 * 0 ^^^ 4),\
179 \ 0 = c_2 + c * L + 1 / EI * (L * q_0 / 12 * L ^^^ 3 + \
180 \ -1 * q_0 / 24 * L ^^^ 4)]";
181 val SOME (t,_) = rewrite_set_ thy true norm_Rational t;
182 if term2str t="[0 = c_2, 0 = c_2 + L * c + L ^^^ 4 * q_0 / (EI * 24)]"
183 then () else error "eqsystem.sml rewrite in 2x2 simplify_System_par.0b";
185 val SOME(t,_)= rewrite_set_inst_ thy true bdvs simplify_System_parenthesized t;
186 if term2str t = "[0 = c_2, 0 = q_0 * L ^^^ 4 / (24 * EI) + (L * c + c_2)]"
187 then () else error "eqsystem.sml rewrite in 2x2 simplify_System_par.1b";
189 val SOME (t,_) = rewrite_set_inst_ thy true bdvs isolate_bdvs t;
190 if term2str t = "[c_2 = 0, L * c + c_2 = 0 + -1 * (q_0 * L ^^^ 4 / (24 * EI))]"
191 then () else error "eqsystem.sml rewrite in 2x2 isolate_bdvs b";
193 val SOME(t,_)= rewrite_set_inst_ thy true bdvs simplify_System t;
194 if term2str t = "[c_2 = 0, L * c + c_2 = -1 * q_0 * L ^^^ 4 / (24 * EI)]"
195 then () else error "eqsystem.sml rewrite in 2x2 simplify_System.2b";
197 val xxx = rewrite_set_ thy true order_system t;
199 then () else error "eqsystem.sml rewrite in 2x2 simplify_System.3b";
202 "----------- rewrite in [EqSystem,top_down_substitution,2x2] -----";
203 "----------- rewrite in [EqSystem,top_down_substitution,2x2] -----";
204 "----------- rewrite in [EqSystem,top_down_substitution,2x2] -----";
205 val e1__ = str2term "c_2 = 77";
206 val e2__ = str2term "L * c + c_2 = q_0 * L ^^^ 2 / 2";
207 val bdvs = [(str2term"bdv_1",str2term"c"),
208 (str2term"bdv_2",str2term"c_2")];
209 val SOME (e2__,_) = rewrite_terms_ thy dummy_ord Erls [e1__] e2__;
210 if term2str e2__ = "L * c + 77 = q_0 * L ^^^ 2 / 2" then ()
211 else error "eqsystem.sml top_down_substitution,2x2] subst";
214 rewrite_set_inst_ thy true bdvs simplify_System_parenthesized e2__;
215 if term2str e2__ = "77 + L * c = q_0 * L ^^^ 2 / 2" then ()
216 else error "eqsystem.sml top_down_substitution,2x2] simpl_par";
218 val SOME (e2__,_) = rewrite_set_inst_ thy true bdvs isolate_bdvs e2__;
219 if term2str e2__ = "c = (q_0 * L ^^^ 2 / 2 + -1 * 77) / L" then ()
220 else error "eqsystem.sml top_down_substitution,2x2] isolate";
222 val t = str2term "[c_2 = 77, c = (q_0 * L ^^^ 2 / 2 + -1 * 77) / L]";
223 val SOME (t,_) = rewrite_set_ thy true order_system t;
224 if term2str t = "[c = (q_0 * L ^^^ 2 / 2 + -1 * 77) / L, c_2 = 77]" then ()
225 else error "eqsystem.sml top_down_substitution,2x2] order_system";
227 if not (ord_simplify_System
229 (str2term"[c_2 = 77, c = (q_0 * L ^^^ 2 / 2 + -1 * 77) / L]",
230 str2term"[c = (q_0 * L ^^^ 2 / 2 + -1 * 77) / L, c_2 = 77]"))
231 then () else error "eqsystem.sml, order_result rew_ord";
234 trace_rewrite:=false;
237 "----------- rewrite in [EqSystem,normalize,4x4] -----------------";
238 "----------- rewrite in [EqSystem,normalize,4x4] -----------------";
239 "----------- rewrite in [EqSystem,normalize,4x4] -----------------";
240 (*STOPPED.WN06?: revise rewrite in [EqSystem,normalize,4x4] from before 0609*)
241 val t = str2term"[0 = -1 * q_0 * 0 ^^^ 2 / 2 + 0 * c_3 + c_4,\
242 \0 = -1 * q_0 * L ^^^ 2 / 2 + L * c_3 + c_4,\
243 \c + c_2 + c_3 + c_4 = 0,\
244 \c_2 + c_3 + c_4 = 0]";
245 val bdvs = [(str2term"bdv_1",str2term"c"),
246 (str2term"bdv_2",str2term"c_2"),
247 (str2term"bdv_3",str2term"c_3"),
248 (str2term"bdv_4",str2term"c_4")];
250 rewrite_set_inst_ thy true bdvs simplify_System_parenthesized t;
251 if term2str t = "[0 = c_4, 0 = -1 * q_0 * L ^^^ 2 / 2 + (L * c_3 + c_4),\n\
252 \ c + (c_2 + (c_3 + c_4)) = 0, c_2 + (c_3 + c_4) = 0]"
253 then () else error "eqsystem.sml rewrite in 4x4 simplify_System_paren";
255 val SOME (t,_) = rewrite_set_inst_ thy true bdvs isolate_bdvs t;
256 if term2str t = "[c_4 = 0, \
257 \L * c_3 + c_4 = 0 + -1 * (-1 * q_0 * L ^^^ 2 / 2),\n \
258 \c + (c_2 + (c_3 + c_4)) = 0, c_2 + (c_3 + c_4) = 0]"
259 then () else error "eqsystem.sml rewrite in 4x4 isolate_bdvs";
261 val SOME(t,_)= rewrite_set_inst_ thy true bdvs simplify_System_parenthesized t;
262 if term2str t = "[c_4 = 0,\
263 \ L * c_3 + c_4 = q_0 * L ^^^ 2 / 2,\
264 \ c + (c_2 + (c_3 + c_4)) = 0,\n\
265 \ c_2 + (c_3 + c_4) = 0]"
266 then () else error "eqsystem.sml rewrite in 4x4 simplify_System_p..2";
268 val SOME (t,_) = rewrite_set_ thy true order_system t;
269 if term2str t = "[c_4 = 0,\
270 \ L * c_3 + c_4 = q_0 * L ^^^ 2 / 2,\
271 \ c_2 + (c_3 + c_4) = 0,\n\
272 \ c + (c_2 + (c_3 + c_4)) = 0]"
273 then () else error "eqsystem.sml rewrite in 4x4 order_system";
275 "----------- refine [linear,system]-------------------------------";
276 "----------- refine [linear,system]-------------------------------";
277 "----------- refine [linear,system]-------------------------------";
279 ["equalities [0 = -1 * q_0 * 0 ^^^ 2 / 2 + 0 * c + c_2," ^
280 "0 = -1 * q_0 * L ^^^ 2 / 2 + L * c + (c_2::real)]",
281 "solveForVars [c, c_2]", "solution LL"];
283 (*WN120313 in "solution L" above "refine fmz ["linear","system"]" caused an error...*)
284 "~~~~~ fun refine, args:"; val ((fmz:fmz_), (pblID:pblID)) = (fmz, ["linear","system"]);
285 "~~~~~ fun refin', args:"; val ((pblRD: pblRD), fmz, pbls, ((Ptyp (pI, [py], [])): pbt ptyp)) =
286 ((rev o tl) pblID, fmz, [(*match list*)],
287 ((Ptyp ("linear", [get_pbt ["linear","system"]], [])): pbt ptyp));
288 val {thy, ppc, where_, prls, ...} = py ;
289 "~~~~~ fun prep_ori, args:"; val (fmz, thy, pbt) = (fmz, thy, ppc);
290 (* val ctxt = Proof_Context.init_global thy |> fold declare_constraints fmz;*)
291 val ctxt = Proof_Context.init_global thy;
292 "~~~~~ fun declare_constraints, args:"; val (t, ctxt) = (nth 1 fmz, ctxt);
293 fun get_vars ((v,T)::vs) = (case raw_explode v |> Library.read_int of
294 (_, _::_) => (Free (v,T)::get_vars vs)
295 | (_, [] ) => get_vars vs) (*filter out nums as long as
296 we have Free ("123",_)*)
298 t = "equalities [0 = -1 * q_0 * 0 ^^^ 2 / 2 + 0 * c + c_2,"^
299 "0 = -1 * q_0 * L ^^^ 2 / 2 + L * c + (c_2::real)]";
300 val ts = Term.add_frees (Syntax.read_term ctxt t) [] |> get_vars;
301 val ctxt = Variable.declare_constraints (nth 1 ts) ctxt;
302 val ctxt = Variable.declare_constraints (nth 2 ts) ctxt;
303 val ctxt = Variable.declare_constraints (nth 3 ts) ctxt;
304 val ctxt = Variable.declare_constraints (nth 4 ts) ctxt;
305 val t = nth 2 fmz; t = "solveForVars [c, c_2]";
306 val ts = Term.add_frees (Syntax.read_term ctxt t) [] |> get_vars;
307 val ctxt = Variable.declare_constraints (nth 1 ts) ctxt;
308 val t = nth 3 fmz; t = "solution LL";
309 (*(Syntax.read_term ctxt t);
310 Type unification failed: Clash of types "real" and "_ list"
311 Type error in application: incompatible operand type
313 Operator: solution :: bool list \<Rightarrow> toreall
314 Operand: L :: real ========== L was already present in equalities ========== *)
316 "===== case 1 =====";
317 val matches = refine fmz ["linear","system"];
319 [Matches (["linear", "system"], _),
320 Matches (["2x2", "linear", "system"], _),
321 NoMatch (["triangular", "2x2", "linear", "system"], _),
322 Matches (["normalize", "2x2", "linear", "system"],
323 {Find = [Correct "solution LL"],
327 "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]",
328 Correct "solveForVars [c, c_2]"],
331 | _ => error "eqsystem.sml refine ['normalize','2x2'...]";
333 "===== case 2 =====";
334 val fmz = ["equalities [c_2 = 0, L * c + c_2 = q_0 * L ^^^ 2 / 2]",
335 "solveForVars [c, c_2]", "solution LL"];
336 val matches = refine fmz ["linear","system"];
337 case matches of [_,_,
339 (["triangular", "2x2", "linear", "system"],
340 {Find = [Correct "solution LL"],
343 [Correct "equalities [c_2 = 0, L * c + c_2 = q_0 * L ^^^ 2 / 2]",
344 Correct "solveForVars [c, c_2]"],
346 "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]",
348 "[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]"],
350 | _ => error "eqsystem.sml refine ['triangular','2x2'...]";
352 (*WN051014----------------------------------------------------------------
353 the above 'val matches = refine fmz ["linear","system"]'
354 didn't work anymore; we investigated in these steps:*)
355 val fmz = ["equalities [c_2 = 0, L * c + c_2 = q_0 * L ^^^ 2 / 2]",
356 "solveForVars [c, c_2]", "solution LL"];
357 val matches = refine fmz ["triangular", "2x2", "linear","system"];
359 False "[c, c_2] from_ [c, c_2] occur_exactly_in nth_ 2\n
360 [c_2 = 0, L * c + c_2 = q_0 * L ^^^ 2 / 2]"]*)
361 val t = str2term ("[c, c_2] from [c, c_2] occur_exactly_in NTH 2" ^
362 "[c_2 = 0, L * c + c_2 = q_0 * L ^^^ 2 / 2]");
363 trace_rewrite := false;
364 val SOME (t',_) = rewrite_set_ thy false prls_triangular t;
367 ### eval asms: 1 < 2 + - 1
368 ==> nth_ (2 + - 1) [L * c + c_2 = q_0 * L ^^^ 2 / 2] =
369 nth_ (2 + - 1 + - 1) []
370 #### rls: erls_prls_triangular on: 1 < 2 + - 1
371 ##### try calc: op <'
372 ### asms accepted: ["1 < 2 + - 1"] stored: ["1 < 2 + -1"]
374 ... i.e Calc ("Groups.plus_class.plus", eval_binop "#add_") was missing in erls_prls_triangular*)
375 trace_rewrite:=false;
377 "===== case 3: relaxed preconditions for triangular system =====";
378 val fmz = ["equalities [L * q_0 = c, \
379 \ 0 = (2 * c_2 + 2 * L * c + -1 * L ^^^ 2 * q_0) / 2,\
382 "solveForVars [c, c_2, c_3, c_4]", "solution LL"];
383 (*============ inhibit exn WN120314 TODO: investigate type error (same) in these 2 cases:
384 probably exn thrown by fun declare_constraints
385 /-------------------------------------------------------\
386 Type unification failed
387 Type error in application: incompatible operand type
389 Operator: op # c_3 :: 'a list \<Rightarrow> 'a list
390 Operand: [c_4] :: 'b list
391 \-------------------------------------------------------/
392 val matches = refine fmz ["linear","system"];
394 [Matches (["linear", "system"], _),
395 NoMatch (["2x2", "linear", "system"], _),
396 NoMatch (["3x3", "linear", "system"], _),
397 Matches (["4x4", "linear", "system"], _),
398 NoMatch (["triangular", "4x4", "linear", "system"], _),
399 Matches (["normalize", "4x4", "linear", "system"], _)] => ()
400 | _ => error "eqsystem.sml: refine relaxed triangular sys NoMatch";
401 (*WN060914 does NOT match, because 3rd and 4th equ are not ordered*)
403 "===== case 4 =====";
404 val fmz = ["equalities [L * q_0 = c, \
405 \ 0 = (2 * c_2 + 2 * L * c + -1 * L ^^^ 2 * q_0) / 2,\
408 "solveForVars [c, c_2, c_3, c_4]", "solution LL"];
409 val matches = refine fmz ["triangular", "4x4", "linear","system"];
411 [Matches (["triangular", "4x4", "linear", "system"], _)] => ()
412 | _ => error "eqsystem.sml: refine relaxed triangular sys Matches";
413 val matches = refine fmz ["linear","system"];
414 ============ inhibit exn WN120314 ==============================================*)
416 "----------- refine [2x2,linear,system] search error--------------";
417 "----------- refine [2x2,linear,system] search error--------------";
418 "----------- refine [2x2,linear,system] search error--------------";
419 (*didn't go into ["2x2", "linear", "system"];
420 we investigated in these steps:*)
421 val fmz = ["equalities [0 = -1 * q_0 * 0 ^^^ 2 / 2 + 0 * c + c_2,\
422 \0 = -1 * q_0 * L ^^^ 2 / 2 + L * c + c_2]",
423 "solveForVars [c, c_2]", "solution LL"];
424 trace_rewrite := false;
425 val matches = refine fmz ["2x2", "linear","system"];
426 trace_rewrite:=false;
427 print_depth 11; matches; print_depth 3;
428 (*brought: 'False "length_ es_ = 2"'*)
430 (*-----fun refin' (pblRD:pblRD) fmz pbls ((Ptyp (pI,[py],[])):pbt ptyp) =
431 (* val ((pblRD:pblRD), fmz, pbls, ((Ptyp (pI,[py],[])):pbt ptyp)) =
432 (rev ["linear","system"], fmz, [(*match list*)],
433 ((Ptyp ("2x2",[get_pbt ["2x2","linear","system"]],[])):pbt ptyp));
435 > show_types:=true; term2str (hd where_); show_types:=false;
436 val it = "length_ (es_::real list) = (2::real)" : string
438 =========================================================================\
440 (* val (thy, (pblID, dsc_dats: (string * (string list)) list,
441 ev:rls, ca: string option, metIDs:metID list)) =
442 (EqSystem.thy, (["system"],
443 [("#Given" ,["equalities es_", "solveForVars v_s"]),
444 ("#Find" ,["solution ss___"](*___ is copy-named*))
446 append_rls "e_rls" e_rls [(*for preds in where_*)],
447 SOME "solveSystem es_ v_s",
450 > val [("#Given", [equalities_es_, "solveForVars v_s"])] = gi;
451 val equalities_es_ = "equalities es_" : string
452 > val (dd, ii) = (split_did o term_of o the o (parse thy)) equalities_es_;
453 > show_types:=true; term2str ii; show_types:=false;
454 val it = "es_::bool list" : string
455 ~~~~~~~~~~~~~~~^^^^^^^^^ OK~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
457 > val {where_,...} = get_pbt ["2x2", "linear","system"];
458 > show_types:=true; term2str (hd where_); show_types:=false;
460 =========================================================================/
463 > (writeln o (itms2str_ (thy2ctxt @{theory Isac}))) itms;
465 (1 ,[1] ,true ,#Given ,Cor equalities
466 [0 = -1 * q_0 * 0 ^^^ 2 / 2 + 0 * c + c_2,
467 0 = -1 * q_0 * L ^^^ 2 / 2 + L * c + c_2] ,(es_, [[0 = -1 * q_0 * 0 ^^^ 2 / 2 + 0 * c + c_2,
468 0 = -1 * q_0 * L ^^^ 2 / 2 + L * c + c_2]])),
469 (2 ,[1] ,true ,#Given ,Cor solveForVars [c, c_2] ,(v_s, [[c, c_2]])),
470 (3 ,[1] ,true ,#Find ,Cor solution L ,(ss___, [L]))]
472 > (writeln o pres2str) pre';
474 (false, length_ es_ = 2),
475 (true, length_ [c, c_2] = 2)]
477 ----- fun match_oris':
478 > (writeln o (itms2str_ (thy2ctxt @{theory Isac}))) itms;
479 > (writeln o pres2str) pre';
482 ----- fun check_preconds'
483 > (writeln o env2str) env;
485 (es_, [0 = -1 * q_0 * 0 ^^^ 2 / 2 + 0 * c + c_2,
486 0 = -1 * q_0 * L ^^^ 2 / 2 + L * c + c_2])","
490 > val es_ = (fst o hd) env;
491 val es_ = Free ("es_", "bool List.list") : Term.term
493 > val pre1 = hd pres;
496 *** Const (op =, [real, real] => bool)
497 *** . Const (ListG.length_, real list => real)
498 *** . . Free (es_, real list)
499 ~~~~~~~~~~~~~~~~~~~^^^^^^^^^ should be bool list~~~~~~~~~~~~~~~~~~~
503 THE REASON WAS A non-type-constrained variable IN #WHERE OF PROBLEM
504 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
507 "----------- me [EqSystem,normalize,2x2] -------------------------";
508 "----------- me [EqSystem,normalize,2x2] -------------------------";
509 "----------- me [EqSystem,normalize,2x2] -------------------------";
510 val fmz = ["equalities [0 = -1 * q_0 * 0 ^^^ 2 / 2 + 0 * c + c_2,\
511 \0 = -1 * q_0 * L ^^^ 2 / 2 + L * c + c_2]",
512 "solveForVars [c, c_2]", "solution LL"];
514 ("Biegelinie",["normalize", "2x2", "linear", "system"],
515 ["EqSystem","normalize","2x2"]);
516 val p = e_pos'; val c = [];
517 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
518 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
519 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
520 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
521 val (p,_,f,nxt,_,pt) = me nxt p c pt;
522 case nxt of ("Specify_Method",_) => ()
523 | _ => error "eqsystem.sml [EqSystem,normalize,2x2] specify";
525 val (p,_,f,nxt,_,pt) = me nxt p c pt;
526 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
527 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*);
528 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
529 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
530 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
532 (_, Subproblem ("Biegelinie", ["triangular", "2x2", "linear",_])) => ()
533 | _ => error "eqsystem.sml me [EqSystem,normalize,2x2] SubProblem";
535 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
536 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
537 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
538 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
540 (_, Specify_Method ["EqSystem", "top_down_substitution", "2x2"]) => ()
541 | _ => error "eqsystem.sml me [EqSys...2x2] top_down_substitution";
543 val (p,_,f,nxt,_,pt) = me nxt p c pt;
544 val PblObj {probl,...} = get_obj I pt [5];
545 (writeln o (itms2str_ (thy2ctxt @{theory Isac}))) probl;
547 (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]])),
548 (2 ,[1] ,true ,#Given ,Cor solveForVars [c, c_2] ,(v_s, [[c, c_2]])),
549 (3 ,[1] ,true ,#Find ,Cor solution ss___ ,(ss___, [ss___]))]
551 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
552 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
553 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
554 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
555 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
556 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
557 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
558 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
560 (_, Check_Postcond ["triangular", "2x2", "linear", "system"]) => ()
561 | _ => error "eqsystem.sml me Subpbl .[EqSys...2x2] finished";
562 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
563 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
564 if f2str f = "[c = L * q_0 / 2, c_2 = 0]" then ()
565 else error "eqsystem.sml me [EqSys...2x2] finished f2str f";
567 (_, End_Proof') => ()
568 | _ => error "eqsystem.sml me [EqSys...2x2] finished End_Proof'";
570 "----------- me [linear,system] ..normalize..top_down_sub..-------";
571 "----------- me [linear,system] ..normalize..top_down_sub..-------";
572 "----------- me [linear,system] ..normalize..top_down_sub..-------";
575 \[0 = c_2 + c * 0 + 1 / EI * (L * q_0 / 12 * 0 ^^^ 3 + \
576 \ -1 * q_0 / 24 * 0 ^^^ 4),\
577 \ 0 = c_2 + c * L + 1 / EI * (L * q_0 / 12 * L ^^^ 3 + \
578 \ -1 * q_0 / 24 * L ^^^ 4)]",
579 "solveForVars [c, c_2]", "solution LL"];
581 ("Biegelinie",["linear", "system"], ["no_met"]);
582 val p = e_pos'; val c = [];
583 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
584 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
585 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
586 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
587 val (p,_,f,nxt,_,pt) = me nxt p c pt;
588 case nxt of (_,Specify_Method ["EqSystem", "normalize", "2x2"]) => ()
589 | _ => error "eqsystem.sml [linear,system] specify b";
590 val (p,_,f,nxt,_,pt) = me nxt p c pt;
591 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
592 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
593 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
594 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
595 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
597 "[c_2 = 0, L * c + c_2 = -1 * q_0 * L ^^^ 4 / (24 * EI)]"
598 then () else error "eqsystem.sml me simpl. before SubProblem b";
600 (_, Subproblem ("Biegelinie", ["triangular", "2x2", "linear",_])) => ()
601 | _ => error "eqsystem.sml me [linear,system] SubProblem b";
603 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
604 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
605 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
606 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
608 (_, Specify_Method ["EqSystem", "top_down_substitution", "2x2"]) => ()
609 | _ => error "eqsystem.sml me [EqSys...2x2] top_down_substitution b";
611 val (p,_,f,nxt,_,pt) = me nxt p c pt;
612 val PblObj {probl,...} = get_obj I pt [5];
613 (writeln o (itms2str_ (thy2ctxt @{theory Isac}))) probl;
615 (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]])),
616 (2 ,[1] ,true ,#Given ,Cor solveForVars [c, c_2] ,(v_s, [[c, c_2]])),
617 (3 ,[1] ,true ,#Find ,Cor solution ss___ ,(ss___, [ss___]))]
619 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
620 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
621 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
622 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
623 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
624 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
625 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
626 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
628 (_, Check_Postcond ["triangular", "2x2", "linear", "system"]) => ()
629 | _ => error "eqsystem.sml me Subpbl .[EqSys...2x2] finished b";
630 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
631 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
633 "[c = -1 * q_0 * L ^^^ 4 / (24 * EI * L), c_2 = 0]"
634 then () else error "eqsystem.sml me [EqSys...2x2] finished f2str f b";
636 (_, End_Proof') => ()
637 | _ => error "eqsystem.sml me [EqSys...2x2] finished End_Proof'";
640 "----------- all systems from Biegelinie -------------------------";
641 "----------- all systems from Biegelinie -------------------------";
642 "----------- all systems from Biegelinie -------------------------";
643 val thy = @{theory Isac}
645 [(str2term "bdv_1", str2term "c"), (str2term "bdv_2", str2term "c_2"),
646 (str2term "bdv_3", str2term "c_3"), (str2term "bdv_4", str2term "c_4")];
651 ["Traegerlaenge L","Streckenlast q_0","Biegelinie y",
652 "Randbedingungen [y 0 = 0, y L = 0, M_b 0 = 0, M_b L = 0]", "FunktionsVariable x"],
653 ("Biegelinie", ["Biegelinien"], ["IntegrierenUndKonstanteBestimmen2"]))];
656 trace_script := true; autoCalculate 1 CompleteCalc; trace_script := false;
657 ##7.27## ordered substs
659 c c_2 c_3 c_4 c c_2 1->2: c
661 c c_2 c c_2 c_3 c_4 [2':c, 1:c_2, 3:c_4] -> 4:c_3*)
664 "0 = c_4 + L * c_3 +(12 * L ^^^ 2 * c_2 + 4 * L ^^^ 3 * c + -1 * L ^^^ 4 * q_0) / (-24 * EI), " ^
666 "0 = (2 * c_2 + 2 * L * c + -1 * L ^^^ 2 * q_0) / 2]");
667 val SOME (t, _) = rewrite_set_ thy false isolate_bdvs_4x4 t;
669 "[c_4 = 0,\n (12 * L ^^^ 2 * c_2 + 4 * L ^^^ 3 * c + -1 * L ^^^ 4 * q_0) / (-24 * EI) =\n -1 * (c_4 + L * c_3) + 0,\n c_2 = 0, (2 * c_2 + 2 * L * c + -1 * L ^^^ 2 * q_0) / 2 = 0]"
670 then () else error "Bsp 7.27";
672 "----- Bsp 7.27 go through the rewrites in met_eqsys_norm_4x4";
673 val t = str2term "0 = (2 * c_2 + 2 * L * c + -1 * L ^^^ 2 * q_0) / 2";
674 val NONE = rewrite_set_ thy false norm_Rational t;
676 rewrite_set_inst_ thy false subst simplify_System_parenthesized t;
677 if term2str t = "0 = -1 * q_0 * L ^^^ 2 / 2 + (L * c + c_2)"
678 then () else error "Bsp 7.27 go through the rewrites in met_eqsys_norm_4x4";
680 "--- isolate_bdvs_4x4";
682 val SOME (t,_) = rewrite_set_inst_ thy false subst isolate_bdvs_4x4 t;
684 val SOME (t,_) = rewrite_set_inst_ thy false subst simplify_System t;
686 val SOME (t,_) = rewrite_set_ thy false order_system t;
690 "------- Bsp 7.28 ---------------vvvvvvvvvvvvv Momentenlinie postponed";
692 CalcTree [((*WN130908 <ERROR> error in kernel </ERROR>*)
693 ["Traegerlaenge L","Momentenlinie (-q_0 / L * x^^^3 / 6)",
695 "Randbedingungen [y L = 0, y' L = 0]",
696 "FunktionsVariable x"],
697 ("Biegelinie", ["vonMomentenlinieZu","Biegelinien"],
698 ["Biegelinien", "AusMomentenlinie"]))];
701 trace_script := true; autoCalculate 1 CompleteCalc; trace_script := false;
707 ["Traegerlaenge L", "Streckenlast q_0", "Biegelinie y",
708 "Randbedingungen [y 0 = 0, y L = 0, y' 0 = 0, y' L = 0]", "FunktionsVariable x"],
709 ("Biegelinie", ["Biegelinien"], ["IntegrierenUndKonstanteBestimmen2"]))];
712 trace_script := true; autoCalculate 1 CompleteCalc; trace_script := false;
713 ##7.69## ordered subst 2x2
715 c c_2 c_3 c_4 c c_2 c_3 1:c_3 -> 2:c c_2 2: c c_2
717 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*)
719 ("[0 = c_4 + 0 / (-1 * EI), " ^
720 "0 = c_4 + L * c_3 + (12 * L ^^^ 2 * c_2 + 4 * L ^^^ 3 * c + -1 * L ^^^ 4 * q_0) / (-24 * EI), " ^
721 "0 = c_3 + 0 / (-1 * EI), " ^
722 "0 = c_3 + (6 * L * c_2 + 3 * L ^^^ 2 * c + -1 * L ^^^ 3 * q_0) / (-6 * EI)]");
727 ["Traegerlaenge L", "Streckenlast q_0", "Biegelinie y",
728 "Randbedingungen [Q 0 = q_0 * L, M_b L = 0, y 0 = 0, y' 0 = 0]", "FunktionsVariable x"],
729 ("Biegelinie", ["Biegelinien"], ["IntegrierenUndKonstanteBestimmen2"] ))];
732 trace_script := true; autoCalculate 1 CompleteCalc; trace_script := false;
737 c_4 | STOPPED.WN06? test methods @@@@@@@@@@@@@@@@@@@@@@@*)
739 "----- 7.70 go through the rewrites in met_eqsys_norm_4x4";
742 "0 = (2 * c_2 + 2 * L * c + -1 * L ^^^ 2 * q_0) / 2, " ^
745 val SOME (t,_) = rewrite_ thy e_rew_ord e_rls false (num_str @{thm commute_0_equality}) t;
746 val SOME (t,_) = rewrite_ thy e_rew_ord e_rls false (num_str @{thm commute_0_equality}) t;
747 val SOME (t,_) = rewrite_ thy e_rew_ord e_rls false (num_str @{thm commute_0_equality}) t;
749 "[L * q_0 = c, (2 * c_2 + 2 * L * c + -1 * L ^^^ 2 * q_0) / 2 = 0, c_4 = 0,\n c_3 = 0]"
750 then () else error "7.70 go through the rewrites in met_eqsys_norm_4x4, 1";
752 val SOME (t,_) = rewrite_set_inst_ thy false subst simplify_System_parenthesized t;
753 if term2str t = "[L * q_0 = c, -1 * q_0 * L ^^^ 2 / 2 + (L * c + c_2) = 0, c_4 = 0, c_3 = 0]"
754 then () else error "7.70 go through the rewrites in met_eqsys_norm_4x4, 2";
756 val SOME (t,_) = rewrite_set_inst_ thy false subst isolate_bdvs_4x4 t;
758 "[c = (-1 * (L * q_0) + 0) / -1,\n" ^
759 " L * c + c_2 = -1 * (-1 * q_0 * L ^^^ 2 / 2) + 0, c_4 = 0, c_3 = 0]"
760 then () else error "7.70 go through the rewrites in met_eqsys_norm_4x4, 3";
762 val SOME (t,_) = rewrite_set_inst_ thy false subst simplify_System_parenthesized t;
763 if term2str t = "[c = -1 * L * q_0 / -1, L * c + c_2 = q_0 * L ^^^ 2 / 2, c_4 = 0, c_3 = 0]"
764 then () else error "7.70 go through the rewrites in met_eqsys_norm_4x4, 4";
766 val SOME (t, _) = rewrite_set_ thy false order_system t;
767 if term2str t = "[c = -1 * L * q_0 / -1, L * c + c_2 = q_0 * L ^^^ 2 / 2, c_3 = 0, c_4 = 0]"
768 then () else error "eqsystem.sml: exp 7.70 normalize 4x4 by rewrite changed";
770 "----- 7.70 with met normalize: ";
771 val fmz = ["equalities" ^
773 "0 = (2 * c_2 + 2 * L * c + -1 * L ^^^ 2 * q_0) / 2, " ^
775 "0 = c_3]", "solveForVars [c, c_2, c_3, c_4]", "solution LL"];
776 val (dI',pI',mI') = ("Biegelinie",["linear", "system"], ["no_met"]);
777 val p = e_pos'; val c = [];
779 (*============ inhibit exn WN120314 TODO: investigate type error (same as above)==
780 in next but one test below the same type error.
781 /-------------------------------------------------------\
782 Type unification failed
783 Type error in application: incompatible operand type
785 Operator: op # c_3 :: 'a list \<Rightarrow> 'a list
786 Operand: [c_4] :: 'b list
787 \-------------------------------------------------------/
789 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
790 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
791 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
792 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
793 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
794 case nxt of (_,Apply_Method ["EqSystem", "normalize", "4x4"]) => ()
795 | _ => error "eqsystem.sml [EqSystem,normalize,4x4] specify";
796 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
798 "----- outcommented before Isabelle2002 --> 2011 -------------------------";
799 (*-----------------------------------vvvWN080102 Exception- Match raised
800 since assod Rewrite .. Rewrite'_Set
801 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
803 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
804 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
806 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
807 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
808 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
809 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
810 if f2str f ="[c = L * q_0, L * c + c_2 = q_0 * L ^^^ 2 / 2, c_3 = 0, c_4 = 0]"
811 then () else error "eqsystem.sml: exp 7.70 normalize 4x4 by met changed";
812 --------------------------------------------------------------------------*)
814 "----- 7.70 with met top_down_: me";
815 val fmz = ["equalities \
816 \[c = L * q_0, L * c + c_2 = q_0 * L ^^^ 2 / 2, c_3 = 0, c_4 = 0]",
817 "solveForVars [c, c_2, c_3, c_4]", "solution LL"];
819 ("Biegelinie",["linear", "system"],["no_met"]);
820 val p = e_pos'; val c = [];
821 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
822 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
823 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
824 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
825 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
826 case nxt of (_,Apply_Method ["EqSystem", "top_down_substitution", "4x4"]) => ()
827 | _ => error "eqsystem.sml [EqSystem,top_down_,4x4] specify";
828 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
829 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
830 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
831 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
832 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
833 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
834 if nxt = ("End_Proof'", End_Proof') andalso
835 f2str f = "[c = L * q_0, c_2 = -1 * L ^^^ 2 * q_0 / 2, c_3 = 0, c_4 = 0]"
836 then () else error "eqsystem.sml: 7.70 with met top_down_: me";
837 ============ inhibit exn WN120314 ==============================================*)
841 CalcTree [(["Traegerlaenge L","Streckenlast q_0","Biegelinie y",
842 "Randbedingungen [M_b L = 0, y 0 = 0, y L = 0, y' 0 = 0]",
843 "FunktionsVariable x"],
844 ("Biegelinie", ["Biegelinien"],
845 ["IntegrierenUndKonstanteBestimmen2"] ))];
848 trace_script := true; autoCalculate 1 CompleteCalc; trace_script := false;
849 ##7.71## |ordered |subst.singles (recurs) |2x2 |diagonal
850 c c_2 |c c_2 |1' |1': c c_2 |
851 c_4 | c_3 |2:c_3 -> 4' :c c_2 c_4 | |
852 c c_2 c_3 c_4 | c_4 |3' | |
853 c_3 |c c_2 c_3 c_4 |3:c_4 -> 4'':c c_2 |4'':c c_2 | *)
854 val t = str2term"[0 = (2 * c_2 + 2 * L * c + -1 * L ^^^ 2 * q_0) / 2, \
855 \ 0 = c_4 + 0 / (-1 * EI), \
856 \ 0 = c_4 + L * c_3 +(12 * L ^^^ 2 * c_2 + 4 * L ^^^ 3 * c + -1 * L ^^^ 4 * q_0) /(-24 * EI),\
857 \ 0 = c_3 + 0 / (-1 * EI)]";
859 "------- Bsp 7.72a ---------------vvvvvvvvvvvvv Momentenlinie postponed";
861 CalcTree [(["Traegerlaenge L",
862 "Momentenlinie ((q_0 * L)/ 6 * x - q_0 /(6 * L) * x^3)",
864 "Randbedingungen [y 0 = 0, y L = 0]",
865 "FunktionsVariable x"],
866 ("Biegelinie", ["vonMomentenlinieZu","Biegelinien"],
867 ["Biegelinien", "AusMomentenlinie"]))];
870 trace_script := true; autoCalculate 1 CompleteCalc; trace_script := false;
875 CalcTree [(["Traegerlaenge L","Streckenlast (q_0 / L * x)","Biegelinie y",
876 "Randbedingungen [M_b 0 = 0, M_b L = 0, y 0 = 0, y L = 0]",
877 "FunktionsVariable x"],
878 ("Biegelinie", ["Biegelinien"],
879 ["IntegrierenUndKonstanteBestimmen2"] ))];
882 trace_script := true; autoCalculate 1 CompleteCalc; trace_script := false;
883 ##7.72b## |ord. |subst.singles |ord.triang.
885 c c_2 | |1:c_2 -> 2':c |c_2 c
887 c c_2 c_3 c_4 | |3:c_4 -> 4':c c_2 c_3 |c_2 c c_3*)
888 val t = str2term"[0 = c_2, \
889 \ 0 = (6 * c_2 + 6 * L * c + -1 * L ^^^ 2 * q_0) / 6, \
890 \ 0 = c_4 + 0 / (-1 * EI), \
891 \ 0 = c_4 + L * c_3 + (60 * L ^^^ 2 * c_2 + 20 * L ^^^ 3 * c + -1 * L ^^^ 4 * q_0) / (-120 * EI)]";
893 "------- Bsp 7.73 ---------------vvvvvvvvvvvvv Momentenlinie postponed";
895 CalcTree [(["Traegerlaenge L","Momentenlinie ???",(*description unclear*)
897 "Randbedingungen [y L = 0, y' L = 0]",
898 "FunktionsVariable x"],
899 ("Biegelinie", ["vonMomentenlinieZu","Biegelinien"],
900 ["Biegelinien", "AusMomentenlinie"]))];
903 trace_script := true; autoCalculate 1 CompleteCalc; trace_script := false;
906 "----------- 4x4 systems from Biegelinie -------------------------";
907 "----------- 4x4 systems from Biegelinie -------------------------";
908 "----------- 4x4 systems from Biegelinie -------------------------";
909 (*STOPPED.WN08?? replace this test with 7.70 *)
911 val fmz = ["equalities \
913 \ 0 = c_4 + L * c_3 +(12 * L ^^^ 2 * c_2 + 4 * L ^^^ 3 * c + -1 * L ^^^ 4 * q_0) / (-24 * EI), \
915 \ 0 = (2 * c_2 + 2 * L * c + -1 * L ^^^ 2 * q_0) / 2]",
916 "solveForVars [c, c_2, c_3, c_4]", "solution LL"];
918 ("Biegelinie",["normalize", "4x4", "linear", "system"],
919 ["EqSystem","normalize","4x4"]);
920 val p = e_pos'; val c = [];
921 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
922 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
923 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
924 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
925 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
926 "------------------------------------------- Apply_Method...";
927 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
929 \ 0 = c_4 + L * c_3 +\n (12 * L ^^^ 2 * c_2 + 4 * L ^^^ 3 * c + -1 * L ^^^ 4 * q_0) / (-24 * EI), \
931 \ 0 = (2 * c_2 + 2 * L * c + -1 * L ^^^ 2 * q_0) / 2]";
932 (*vvvWN080102 Exception- Match raised
933 since assod Rewrite .. Rewrite'_Set
934 "------------------------------------------- simplify_System_parenthesized...";
935 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
937 \ 0 = -1 * q_0 * L ^^^ 4 / (-24 * EI) + \
938 \ (4 * L ^^^ 3 * c / (-24 * EI) + \
939 \ (12 * L ^^^ 2 * c_2 / (-24 * EI) + \
940 \ (L * c_3 + c_4))), \
942 \ 0 = -1 * q_0 * L ^^^ 2 / 2 + (L * c + c_2)]";
943 (*? "(4 * L ^^^ 3 / (-24 * EI) * c" statt "(4 * L ^^^ 3 * c / (-24 * EI)" ?*)
944 "------------------------------------------- isolate_bdvs...";
945 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
947 \ 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),\
949 \ c_2 = 0 + -1 * (-1 * q_0 * L ^^^ 2 / 2) + -1 * (L * c)]";
950 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
952 ---------------------------------------------------------------------*)