1 (* Title: Knowledge/eqsystem-1.sml
2 author: Walther Neuper 050826,
3 (c) due to copyright terms
6 "-----------------------------------------------------------------------------------------------";
7 "table of contents -----------------------------------------------------------------------------";
8 "-----------------------------------------------------------------------------------------------";
9 "Knowledge/eqsystem-1.sml";
10 "----------- occur_exactly_in ---------------------------------------------------equsystem-1.sml";
11 "----------- problems -----------------------------------------------------------equsystem-1.sml";
12 "----------- rewrite-order ord_simplify_System ----------------------------------equsystem-1.sml";
13 "----------- rewrite in [EqSystem,normalise,2x2] --------------------------------equsystem-1.sml";
14 "----------- rewrite example from 2nd [EqSystem,normalise,2x2] ------------------equsystem-1.sml";
15 "----------- rewrite in [EqSystem,top_down_substitution,2x2] --------------------equsystem-1.sml";
16 "----------- rewrite in [EqSystem,normalise,4x4] --------------------------------equsystem-1.sml";
17 "----------- script [EqSystem,top_down_substitution,2x2] Vers.1 -----------------equsystem-1.sml";
18 "----------- refine [linear,system]----------------------------------------------equsystem-1.sml";
19 "----------- refine [2x2,linear,system] search error-----------------------------equsystem-1.sml";
20 "----------- me [EqSystem,normalise,2x2], refine Subproblem ---------------------equsystem-1.sml";
21 "Knowledge/eqsystem-1a.sml";
22 "----------- me [EqSystem,normalise,2x2], refine Subproblem, step into istate---equsystem-1a.sml";
23 "Knowledge/eqsystem-2.sml";
24 "----------- me [linear,system] ..normalise..top_down_sub..----------------------equsystem-2.sml";
25 "----------- all systems from Biegelinie ----------------------------------------equsystem-2.sml";
26 "----------- 4x4 systems from Biegelinie ----------------------------------------equsystem-2.sml";
27 "-----------------------------------------------------------------------------------------------";
28 "-----------------------------------------------------------------------------------------------";
29 "-----------------------------------------------------------------------------------------------";
31 val thy = @{theory "EqSystem"};
32 val ctxt = Proof_Context.init_global thy;
34 (*//----- would cover new code above ---\\* )
42 ( *\\----- would cover new code above ---//*)
44 "----------- occur_exactly_in ------------------------------------";
45 "----------- occur_exactly_in ------------------------------------";
46 "----------- occur_exactly_in ------------------------------------";
47 val all = [ParseC.parse_test @{context}"c", ParseC.parse_test @{context}"c_2", ParseC.parse_test @{context}"c_3"];
48 val t = ParseC.parse_test @{context}"0 = - 1 * q_0 * L \<up> 2 / 2 + L * c + c_2";
50 if occur_exactly_in [ParseC.parse_test @{context}"c", ParseC.parse_test @{context}"c_2"] all t
51 then () else error "eqsystem.sml occur_exactly_in 1";
53 if not (occur_exactly_in [ParseC.parse_test @{context}"c", ParseC.parse_test @{context}"c_2", ParseC.parse_test @{context}"c_3"] all t)
54 then () else error "eqsystem.sml occur_exactly_in 2";
56 if not (occur_exactly_in [ParseC.parse_test @{context}"c_2"] all t)
57 then () else error "eqsystem.sml occur_exactly_in 3";
59 val t = ParseC.parse_test @{context}"[c,c_2] from [c,c_2,c_3] occur_exactly_in - 1 * q_0 * L \<up> 2 / 2 + L * c + c_2";
60 eval_occur_exactly_in 0 "EqSystem.occur_exactly_in" t 0;
61 val SOME (str, t') = eval_occur_exactly_in 0 "EqSystem.occur_exactly_in" t 0;
62 if str = "[c, c_2] from [c, c_2,\n" ^
63 " c_3] occur_exactly_in - 1 * q_0 * L \<up> 2 / 2 + L * c + c_2 = True"
64 then () else error "eval_occur_exactly_in [c, c_2]";
66 val t = ParseC.parse_test @{context} ("[c,c_2,c_3] from [c,c_2,c_3] occur_exactly_in " ^
67 "- 1 * q_0 * L \<up> 2 / 2 + L * c + c_2");
68 val SOME (str, t') = eval_occur_exactly_in 0 "EqSystem.occur_exactly_in" t 0;
69 if str = "[c, c_2,\n c_3] from [c, c_2,\n" ^
70 " c_3] occur_exactly_in - 1 * q_0 * L \<up> 2 / 2 + L * c + c_2 = False"
71 then () else error "eval_occur_exactly_in [c, c_2, c_3]";
73 val t = ParseC.parse_test @{context}"[c_2] from [c,c_2,c_3] occur_exactly_in \
74 \- 1 * q_0 * L \<up> 2 / 2 + L * c + c_2";
75 val SOME (str, t') = eval_occur_exactly_in 0 "EqSystem.occur_exactly_in" t 0;
76 if str = "[c_2] from [c, c_2,\n" ^
77 " c_3] occur_exactly_in - 1 * q_0 * L \<up> 2 / 2 + L * c + c_2 = False"
78 then () else error "eval_occur_exactly_in [c, c_2, c_3]";
80 val t = ParseC.parse_test @{context}"[] from [c,c_2,c_3] occur_exactly_in 0";
81 val SOME (str, t') = eval_occur_exactly_in 0 "EqSystem.occur_exactly_in" t 0;
82 if str = "[] from [c, c_2, c_3] occur_exactly_in 0 = True" then ()
83 else error "eval_occur_exactly_in [c, c_2, c_3]";
86 ParseC.parse_test @{context}
87 "[] from [c, c_2, c_3, c_4] occur_exactly_in - 1 * (q_0 * L \<up> 2) /2";
88 val SOME (str, t') = eval_occur_exactly_in 0 "EqSystem.occur_exactly_in" t 0;
89 if str = "[] from [c, c_2, c_3, c_4] occur_exactly_in \
90 \- 1 * (q_0 * L \<up> 2) / 2 = True" then ()
91 else error "eval_occur_exactly_in [c, c_2, c_3, c_4]";
94 "----------- problems --------------------------------------------";
95 "----------- problems --------------------------------------------";
96 "----------- problems --------------------------------------------";
97 val t = ParseC.parse_test @{context} "Length [x+y=1,y=2] = 2";
98 val testrls = Rule_Set.append_rules "testrls" Rule_Set.empty
99 [(Thm ("LENGTH_NIL", @{thm LENGTH_NIL})),
100 (Thm ("LENGTH_CONS", @{thm LENGTH_CONS})),
101 Eval (\<^const_name>\<open>plus\<close>, Calc_Binop.numeric "#add_"),
102 Eval (\<^const_name>\<open>HOL.eq\<close>, eval_equal "#equal_")
104 val SOME (t',_) = rewrite_set_ ctxt false testrls t;
105 if UnparseC.term @{context} t' = "True" then ()
106 else error "eqsystem.sml: length_ [x+y=1,y=2] = 2";
108 val SOME t = ParseC.term_opt ctxt "solution LL";
109 TermC.atom_trace_detail @{context} t;
110 val SOME t = ParseC.term_opt ctxt "solution LL";
111 TermC.atom_trace_detail @{context} t;
113 val t = ParseC.parse_test @{context}
114 "(tl (tl (tl v_s))) from v_s occur_exactly_in (NTH 1 (e_s::bool list))";
115 TermC.atom_trace_detail @{context} t;
116 val t = ParseC.parse_test @{context} ("(tl (tl (tl [c, c_2, c_3, c_4]))) from [c, c_2, c_3, c_4] occur_exactly_in " ^
117 "(NTH 1 [c_4 = 1, 2 = 2, 3 = 3, 4 = 4])");
118 (*----- broken in child of.1790e1073acc : eliminate "handle _ => ..." from Rewrite.rewrite -----\\
119 assume flawed test setup hidden by "handle _ => ..."
120 ERROR rewrite__set_ called with 'Erls' for '1 < 1'
122 rewrite_set_ ctxt true
123 (Rule_Set.append_rules "prls_" Rule_Set.empty
124 [Thm ("NTH_CONS",ThmC.numerals_to_Free @{thm NTH_CONS}),
125 Thm ("NTH_NIL",ThmC.numerals_to_Free @{thm NTH_NIL}),
126 Thm ("TL_CONS",ThmC.numerals_to_Free @{thm tl_Cons}),
127 Thm ("TL_NIL",ThmC.numerals_to_Free @{thm tl_Nil}),
128 Eval ("EqSystem.occur_exactly_in", eval_occur_exactly_in "#eval_occur_exactly_in_")
130 if t = @{term True} then ()
131 else error "eqsystem.sml ..occur_exactly_in (nth_ 1 [c_4..";
132 broken in child of.1790e1073acc : eliminate "handle _ => ..." from Rewrite.rewrite ---//*)
135 "----------- rewrite-order ord_simplify_System -------------------";
136 "----------- rewrite-order ord_simplify_System -------------------";
137 "----------- rewrite-order ord_simplify_System -------------------";
138 "M_b x = c * x + - 1 * q_0 * (x \<up> 2 / 2) + c_2";
139 "--- add.commute ---"; (* ... add.commute cf. b42e334c97ee *)
140 if ord_simplify_System false ctxt [] (ParseC.parse_test @{context}"- 1 * q_0 * (x \<up> 2 / 2)",
141 ParseC.parse_test @{context}"c * x") then ()
142 else error "integrate.sml, (- 1 * q_0 * (x \<up> 2 / 2)) < (c * x) not#1";
144 if ord_simplify_System false ctxt [] (ParseC.parse_test @{context}"- 1 * q_0 * (x \<up> 2 / 2)",
145 ParseC.parse_test @{context}"c_2") then ()
146 else error "integrate.sml, (- 1 * q_0 * (x \<up> 2 / 2)) < (c_2) not#2";
148 if ord_simplify_System false ctxt [] (ParseC.parse_test @{context}"c * x",
149 ParseC.parse_test @{context}"c_2") then ()
150 else error "integrate.sml, (c * x) < (c_2) not#3";
152 "--- mult.commute ---";
153 if ord_simplify_System false ctxt [] (ParseC.parse_test @{context}"x * c",
154 ParseC.parse_test @{context}"c * x") then ()
155 else error "integrate.sml, (x * c) < (c * x) not#4";
157 if ord_simplify_System false ctxt [] (ParseC.parse_test @{context}"- 1 * q_0 * (x \<up> 2 / 2) * c",
158 ParseC.parse_test @{context}"- 1 * q_0 * c * (x \<up> 2 / 2)")
159 then () else error "integrate.sml, (. * .) < (. * .) not#5";
161 if ord_simplify_System false ctxt [] (ParseC.parse_test @{context}"- 1 * q_0 * (x \<up> 2 / 2) * c",
162 ParseC.parse_test @{context}"c * - 1 * q_0 * (x \<up> 2 / 2)")
163 then () else error "integrate.sml, (. * .) < (. * .) not#6";
166 "----------- rewrite in [EqSystem,normalise,2x2] -----------------";
167 "----------- rewrite in [EqSystem,normalise,2x2] -----------------";
168 "----------- rewrite in [EqSystem,normalise,2x2] -----------------";
169 val t = ParseC.parse_test @{context}"[0 = - 1 * q_0 * L \<up> 2 / 2 + L * c + c_2,\
170 \0 = - 1 * q_0 * 0 \<up> 2 / 2 + 0 * c + c_2]";
171 val bdvs = [(ParseC.parse_test @{context}"bdv_1",ParseC.parse_test @{context}"c"),
172 (ParseC.parse_test @{context}"bdv_2",ParseC.parse_test @{context}"c_2")];
173 val SOME (t,_) = rewrite_set_inst_ ctxt true bdvs simplify_System_parenthesized t;
174 if UnparseC.term @{context} t = "[0 = - 1 * q_0 * L \<up> 2 / 2 + (L * c + c_2), 0 = c_2]"
175 then () else error "eqsystem.sml rewrite in 2x2 simplify_System_par.1";
177 val SOME (t,_) = rewrite_set_inst_ ctxt true bdvs isolate_bdvs t;
178 if UnparseC.term @{context} t = "[L * c + c_2 = 0 + - 1 * (- 1 * q_0 * L \<up> 2 / 2), c_2 = 0]"
179 then () else error "eqsystem.sml rewrite in 2x2 isolate_bdvs";
181 val SOME (t,_)= rewrite_set_inst_ ctxt true bdvs simplify_System t;
182 if UnparseC.term @{context} t = "[L * c + c_2 = q_0 * L \<up> 2 / 2, c_2 = 0]"
183 then () else error "eqsystem.sml rewrite in 2x2 simplify_System_par.2";
185 "--- 3--- see EqSystem.thy (*..if replaced by 'and' ...*)";
186 val SOME (t,_) = rewrite_set_ ctxt true order_system t;
187 if UnparseC.term @{context} t = "[c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2]"
188 then () else error "eqsystem.sml rewrite in 2x2 simplify_System_par.3";
191 "----------- rewrite example from 2nd [EqSystem,normalise,2x2] ---";
192 "----------- rewrite example from 2nd [EqSystem,normalise,2x2] ---";
193 "----------- rewrite example from 2nd [EqSystem,normalise,2x2] ---";
194 val thy = @{theory "Isac_Knowledge"} (*because of Undeclared constant "Biegelinie.EI*);
195 val ctxt = Proof_Context.init_global thy;
197 ParseC.parse_test @{context}"[0 = c_2 + c * 0 + 1 / EI * (L * q_0 / 12 * 0 \<up> 3 + \
198 \ - 1 * q_0 / 24 * 0 \<up> 4),\
199 \ 0 = c_2 + c * L + 1 / EI * (L * q_0 / 12 * L \<up> 3 + \
200 \ - 1 * q_0 / 24 * L \<up> 4)]";
201 val SOME (t, _) = rewrite_set_ ctxt true norm_Rational t;
202 if UnparseC.term @{context} t = (*BEFORE "eliminate ThmC.numerals_to_Free"..
203 "[c_2 = 0, 0 = q_0 * L \<up> 4 / (24 * EI) + (L * c + c_2)]"*)
204 "[0 = c_2, 0 = (24 * c_2 + 24 * L * c + L \<up> 4 * q_0) / 24]"
205 then () else error "eqsystem.sml rewrite in 2x2 simplify_System_par.0b";
207 val SOME(t, _)= rewrite_set_inst_ ctxt true bdvs simplify_System_parenthesized t;
208 if UnparseC.term @{context} t = (*BEFORE "eliminate ThmC.numerals_to_Free"..
209 "[c_2 = 0, 0 = q_0 * L \<up> 4 / (24 * EI) + (L * c + c_2)]"*)
210 "[0 = c_2, 0 = q_0 * L \<up> 4 / 24 + (L * c + c_2)]"
211 then () else error "eqsystem.sml rewrite in 2x2 simplify_System_par.1b";
213 val SOME (t,_) = rewrite_set_inst_ ctxt true bdvs isolate_bdvs t;
214 if UnparseC.term @{context} t = (*BEFORE "eliminate ThmC.numerals_to_Free"..
215 "[c_2 = 0, L * c + c_2 = 0 + - 1 * (q_0 * L \<up> 4 / (24 * EI))]"*)
216 "[c_2 = 0, L * c + c_2 = 0 + - 1 * (q_0 * L \<up> 4 / 24)]"
217 then () else error "eqsystem.sml rewrite in 2x2 isolate_bdvs b";
219 val SOME(t,_)= rewrite_set_inst_ ctxt true bdvs simplify_System t;
220 if UnparseC.term @{context} t = (*BEFORE "eliminate ThmC.numerals_to_Free"..
221 "[c_2 = 0, L * c + c_2 = - 1 * q_0 * L \<up> 4 / (24 * EI)]"*)
222 "[c_2 = 0, L * c + c_2 = - 1 * q_0 * L \<up> 4 / 24]"
223 then () else error "eqsystem.sml rewrite in 2x2 simplify_System.2b";
225 val xxx = rewrite_set_ ctxt true order_system t;
227 then () else error "eqsystem.sml rewrite in 2x2 simplify_System.3b";
230 "----------- rewrite in [EqSystem,top_down_substitution,2x2] -----";
231 "----------- rewrite in [EqSystem,top_down_substitution,2x2] -----";
232 "----------- rewrite in [EqSystem,top_down_substitution,2x2] -----";
233 val e1__ = ParseC.parse_test @{context} "c_2 = 77";
234 val e2__ = ParseC.parse_test @{context} "L * c + c_2 = q_0 * L \<up> 2 / 2";
235 val bdvs = [(ParseC.parse_test @{context}"bdv_1",ParseC.parse_test @{context}"c"),
236 (ParseC.parse_test @{context}"bdv_2",ParseC.parse_test @{context}"c_2")];
237 val SOME (e2__,_) = rewrite_terms_ ctxt Rewrite_Ord.function_empty Rule_Set.Empty [e1__] e2__;
238 if UnparseC.term @{context} e2__ = "L * c + 77 = q_0 * L \<up> 2 / 2" then ()
239 else error "eqsystem.sml top_down_substitution,2x2] subst";
242 rewrite_set_inst_ ctxt true bdvs simplify_System_parenthesized e2__;
243 if UnparseC.term @{context} e2__ = "77 + L * c = q_0 * L \<up> 2 / 2" then ()
244 else error "eqsystem.sml top_down_substitution,2x2] simpl_par";
246 val SOME (e2__,_) = rewrite_set_inst_ ctxt true bdvs isolate_bdvs e2__;
247 if UnparseC.term @{context} e2__ = "c = (q_0 * L \<up> 2 / 2 + - 1 * 77) / L" then ()
248 else error "eqsystem.sml top_down_substitution,2x2] isolate";
250 val t = ParseC.parse_test @{context} "[c_2 = 77, c = (q_0 * L \<up> 2 / 2 + - 1 * 77) / L]";
251 val SOME (t,_) = rewrite_set_ ctxt true order_system t;
252 if UnparseC.term @{context} t = "[c = (q_0 * L \<up> 2 / 2 + - 1 * 77) / L, c_2 = 77]" then ()
253 else error "eqsystem.sml top_down_substitution,2x2] order_system";
255 if not (ord_simplify_System
257 (ParseC.parse_test @{context}"[c_2 = 77, c = (q_0 * L \<up> 2 / 2 + - 1 * 77) / L]",
258 ParseC.parse_test @{context}"[c = (q_0 * L \<up> 2 / 2 + - 1 * 77) / L, c_2 = 77]"))
259 then () else error "eqsystem.sml, order_result rew_ord";
262 "----------- rewrite in [EqSystem,normalise,4x4] -----------------";
263 "----------- rewrite in [EqSystem,normalise,4x4] -----------------";
264 "----------- rewrite in [EqSystem,normalise,4x4] -----------------";
265 (*STOPPED.WN06?: revise rewrite in [EqSystem,normalise,4x4] from before 0609*)
266 val t = ParseC.parse_test @{context} (
267 "[(0::real) = - 1 * q_0 * 0 \<up> 2 / 2 + 0 * c_3 + c_4, " ^
268 "(0::real) = - 1 * q_0 * L \<up> 2 / 2 + L * c_3 + c_4, " ^
269 "c + c_2 + c_3 + c_4 = 0, " ^
270 "c_2 + c_3 + c_4 = 0]");
271 val bdvs = [(ParseC.parse_test @{context}"bdv_1::real",ParseC.parse_test @{context}"c::real"),
272 (ParseC.parse_test @{context}"bdv_2::real",ParseC.parse_test @{context}"c_2::real"),
273 (ParseC.parse_test @{context}"bdv_3::real",ParseC.parse_test @{context}"c_3::real"),
274 (ParseC.parse_test @{context}"bdv_4::real",ParseC.parse_test @{context}"c_4::real")];
276 rewrite_set_inst_ ctxt true bdvs simplify_System_parenthesized t;
277 if UnparseC.term @{context} t = "[0 = c_4, 0 = - 1 * q_0 * L \<up> 2 / 2 + (L * c_3 + c_4),\n c + (c_2 + (c_3 + c_4)) = 0, c_2 + (c_3 + c_4) = 0]"
278 then () else error "eqsystem.sml rewrite in 4x4 simplify_System_paren";
280 val SOME (t, _) = rewrite_set_inst_ ctxt true bdvs isolate_bdvs t;
281 if UnparseC.term @{context} t = "[c_4 = 0, \
282 \L * c_3 + c_4 = 0 + - 1 * (- 1 * q_0 * L \<up> 2 / 2),\n \
283 \c + (c_2 + (c_3 + c_4)) = 0, c_2 + (c_3 + c_4) = 0]"
284 then () else error "eqsystem.sml rewrite in 4x4 isolate_bdvs";
286 val SOME(t, _)= rewrite_set_inst_ ctxt true bdvs simplify_System_parenthesized t;
287 if UnparseC.term @{context} t = "[c_4 = 0,\
288 \ L * c_3 + c_4 = q_0 * L \<up> 2 / 2,\
289 \ c + (c_2 + (c_3 + c_4)) = 0,\n\
290 \ c_2 + (c_3 + c_4) = 0]"
291 then () else error "eqsystem.sml rewrite in 4x4 simplify_System_p..2";
293 val SOME (t, _) = rewrite_set_ ctxt true order_system t;
294 if UnparseC.term @{context} t = "[c_4 = 0,\
295 \ L * c_3 + c_4 = q_0 * L \<up> 2 / 2,\
296 \ c_2 + (c_3 + c_4) = 0,\n\
297 \ c + (c_2 + (c_3 + c_4)) = 0]"
298 then () else error "eqsystem.sml rewrite in 4x4 order_system";
301 "----------- refine [linear,system]-------------------------------";
302 "----------- refine [linear,system]-------------------------------";
303 "----------- refine [linear,system]-------------------------------";
305 ["equalities [0 = - 1 * q_0 * 0 \<up> 2 / 2 + 0 * c + c_2," ^
306 "0 = - 1 * q_0 * L \<up> 2 / 2 + L * c + (c_2::real)]",
307 "solveForVars [c, c_2]", "solution LL"];
309 (*WN120313 in "solution L" above "Refine.by_formalise @{context} fmz ["LINEAR", "system"]" caused an error...*)
310 "~~~~~ fun Refine.refine , args:"; val ((fmz: Formalise.model), (pblID:Problem.id)) = (fmz, ["LINEAR", "system"]);
311 "~~~~~ fun check_match' , args:"; val ((pblRD: Problem.id_reverse), fmz, pbls, ((Store.Node (pI, [py], [])): Problem.T Store.node)) =
312 ((rev o tl) pblID, fmz, [(*match list*)],
313 ((Store.Node ("LINEAR", [Problem.from_store ctxt ["LINEAR", "system"]], [])): Problem.T Store.node));
314 val {thy, model, where_, where_rls, ...} = py ;
315 "~~~~~ fun O_Model.init, args:"; val (thy, fmz, pbt) = (thy, fmz, model);
316 val (ts, ctxt) = ContextC.init_while_parsing fmz thy;
317 "~~~~~ fun declare_constraints, args:"; val (t, ctxt) = (nth 1 fmz, ctxt);
318 fun get_vars ((v,T)::vs) = (case raw_explode v |> Library.read_int of
319 (_, _::_) => (Free (v,T)::get_vars vs)
320 | (_, [] ) => get_vars vs) (*filter out nums as long as
321 we have Free ("123",_)*)
323 t = "equalities [0 = - 1 * q_0 * 0 \<up> 2 / 2 + 0 * c + c_2,"^
324 "0 = - 1 * q_0 * L \<up> 2 / 2 + L * c + (c_2::real)]";
325 val ts = Term.add_frees (Syntax.read_term ctxt t) [] |> get_vars;
326 val ctxt = Variable.declare_constraints (nth 1 ts) ctxt;
327 val ctxt = Variable.declare_constraints (nth 2 ts) ctxt;
328 val ctxt = Variable.declare_constraints (nth 3 ts) ctxt;
329 val ctxt = Variable.declare_constraints (nth 4 ts) ctxt;
330 val t = nth 2 fmz; t = "solveForVars [c, c_2]";
331 val ts = Term.add_frees (Syntax.read_term ctxt t) [] |> get_vars;
332 val ctxt = Variable.declare_constraints (nth 1 ts) ctxt;
333 val t = nth 3 fmz; t = "solution LL";
334 (*(Syntax.read_term ctxt t);
335 Type unification failed: Clash of types "real" and "_ list"
336 Type error in application: incompatible operand type
338 Operator: solution :: bool list \<Rightarrow> toreall
339 Operand: L :: real ========== L was already present in equalities ========== *)
341 "===== case 1 =====";
342 val matches = Refine.by_formalise @{context} fmz ["LINEAR", "system"];
344 [Matches (["LINEAR", "system"], _), (*Matches*)
345 Matches (["2x2", "LINEAR", "system"], _), (*NoMatch !--> continue search !*)
346 NoMatch (["triangular", "2x2", "LINEAR", "system"], _), (**)
347 Matches (["normalise", "2x2", "LINEAR", "system"], (**)
348 {Find = [P_Model.Correct "solution LL"], With = [], (**)
349 Given = [P_Model.Correct "equalities\n [0 = - 1 * q_0 * 0 \<up> 2 / 2 + 0 * c + c_2,\n 0 = - 1 * q_0 * L \<up> 2 / 2 + L * c + c_2]",
350 P_Model.Correct "solveForVars [c, c_2]"],
353 | _ => error "eqsystem.sml Refine.refine ['normalise','2x2'...]";
355 "===== case 2 =====";
356 val fmz = ["equalities [c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2]",
357 "solveForVars [c, c_2]", "solution LL"];
358 val matches = Refine.by_formalise @{context} fmz ["LINEAR", "system"];
359 case matches of [_,_,
361 (["triangular", "2x2", "LINEAR", "system"],
362 {Find = [P_Model.Correct "solution LL"],
365 [P_Model.Correct "equalities [c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2]",
366 P_Model.Correct "solveForVars [c, c_2]"],
367 Where = [P_Model.Correct
368 "tl [c, c_2] from [c, c_2] occur_exactly_in NTH 1\n [c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2]",
370 "[c, c_2] from [c, c_2] occur_exactly_in NTH 2\n [c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2]"],
372 | _ => error "eqsystem.sml Refine.refine ['triangular','2x2'...]";
374 (*WN051014-----------------------------------------------------------------------------------\\
375 the above 'val matches = Refine.by_formalise @{context} fmz ["LINEAR", "system"]'
376 didn't work anymore; we investigated in these steps:*)
377 val fmz = ["equalities [c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2]",
378 "solveForVars [c, c_2]", "solution LL"];
379 val matches = Refine.by_formalise @{context} fmz ["triangular", "2x2", "LINEAR", "system"];
381 False "[c, c_2] from_ [c, c_2] occur_exactly_in nth_ 2\n
382 [c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2]"]*)
383 val t = ParseC.parse_test @{context} ("[c, c_2] from [c, c_2] occur_exactly_in NTH 2" ^
384 "[c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2]");
386 val SOME (t', _) = rewrite_set_ ctxt false prls_triangular t;
389 ### eval asms: 1 < 2 + - 1
390 ==> nth_ (2 + - 1) [L * c + c_2 = q_0 * L \<up> 2 / 2] =
391 nth_ (2 + - 1 + - 1) []
392 #### rls: erls_prls_triangular on: 1 < 2 + - 1
393 ##### try calc: op <'
394 ### asms accepted: ["1 < 2 + - 1"] stored: ["1 < 2 + - 1"]
396 ... i.e Eval ("Groups.plus_class.plus", Calc_Binop.numeric "#add_") was missing in erls_prls_triangular*)
397 (*--------------------------------------------------------------------------------------------//*)
400 "===== case 3: relaxed preconditions for triangular system =====";
401 val fmz = ["equalities [L * q_0 = c, \
402 \ 0 = (2 * c_2 + 2 * L * c + - 1 * L \<up> 2 * q_0) / 2,\
405 "solveForVars [c, c_2, c_3, c_4]", "solution LL"];
406 (*============ inhibit exn WN120314 TODO: investigate type error (same) in these 2 cases:
407 probably exn thrown by fun declare_constraints
408 /-------------------------------------------------------\
409 Type unification failed
410 Type error in application: incompatible operand type
412 Operator: op # c_3 :: 'a list \<Rightarrow> 'a list
413 Operand: [c_4] :: 'b list
414 \-------------------------------------------------------/
415 val TermC.matches = Refine.refine fmz ["LINEAR", "system"];
416 case TermC.matches of
417 [M_Match.Matches (["LINEAR", "system"], _),
418 M_Match.NoMatch (["2x2", "LINEAR", "system"], _),
419 M_Match.NoMatch (["3x3", "LINEAR", "system"], _),
420 M_Match.Matches (["4x4", "LINEAR", "system"], _),
421 M_Match.NoMatch (["triangular", "4x4", "LINEAR", "system"], _),
422 M_Match.Matches (["normalise", "4x4", "LINEAR", "system"], _)] => ()
423 | _ => error "eqsystem.sml: Refine.refine relaxed triangular sys M_Match.NoMatch";
424 (*WN060914 does NOT match, because 3rd and 4th equ are not ordered*)
426 "===== case 4 =====";
427 val fmz = ["equalities [L * q_0 = c, \
428 \ 0 = (2 * c_2 + 2 * L * c + - 1 * L \<up> 2 * q_0) / 2,\
431 "solveForVars [c, c_2, c_3, c_4]", "solution LL"];
432 val TermC.matches = Refine.refine fmz ["triangular", "4x4", "LINEAR", "system"];
433 case TermC.matches of
434 [M_Match.Matches (["triangular", "4x4", "LINEAR", "system"], _)] => ()
435 | _ => error "eqsystem.sml: Refine.refine relaxed triangular sys M_Match.NoMatch";
436 val TermC.matches = Refine.refine fmz ["LINEAR", "system"];
437 ============ inhibit exn WN120314 ==============================================*)
440 "----------- Refine.refine [2x2,linear,system] search error--------------";
441 "----------- Refine.refine [2x2,linear,system] search error--------------";
442 "----------- Refine.refine [2x2,linear,system] search error--------------";
443 (*didn't go into ["2x2", "LINEAR", "system"];
444 we investigated in these steps:*)
445 val fmz = ["equalities [0 = - 1 * q_0 * 0 \<up> 2 / 2 + 0 * c + c_2,\
446 \0 = - 1 * q_0 * L \<up> 2 / 2 + L * c + c_2]",
447 "solveForVars [c, c_2]", "solution LL"];
448 val matches = Refine.by_formalise @{context} fmz ["2x2", "LINEAR", "system"];
449 (*default_print_depth 11;*) TermC.matches; (*default_print_depth 3;*)
450 (*brought: 'False "length_ es_ = 2"'*)
452 (*-----fun check_match' (pblRD:Problem.id_reverse) fmz pbls ((Store.Node (pI,[py],[])):pbt Store.store) =
453 (* val ((pblRD:Problem.id_reverse), fmz, pbls, ((Store.Node (pI,[py],[])):pbt Store.store)) =
454 (rev ["LINEAR", "system"], fmz, [(*match list*)],
455 ((Store.Node ("2x2",[Problem.from_store ["2x2", "LINEAR", "system"]],[])):pbt Store.store));
457 > show_types:=true; UnparseC.term @{context} (hd where_); show_types:=false;
458 val it = "length_ (es_::real list) = (2::real)" : string
460 =========================================================================\
461 -------fun Problem.prep_input
462 (* val (thy, (pblID, dsc_dats: (string * (string list)) list,
463 ev:rls, ca: string option, metIDs:metID list)) =
464 (EqSystem.thy, (["system"],
465 [("#Given" ,["equalities es_", "solveForVars v_s"]),
466 ("#Find" ,["solution ss___"](*___ is copy-named*))
468 Rule_Set.append_rules "empty" Rule_Set.empty [(*for preds in where_*)],
469 SOME "solveSystem es_ v_s",
472 > val [("#Given", [equalities_es_, "solveForVars v_s"])] = gi;
473 val equalities_es_ = "equalities es_" : string
474 > val (dd, ii) = ((Model_Pattern.split_descriptor ctxt) o Thm.term_of o the o (TermC.parse thy)) equalities_es_;
475 > show_types:=true; UnparseC.term @{context} ii; show_types:=false;
476 val it = "es_::bool list" : string
477 ~~~~~~~~~~~~~~~ \<up> \<up> \<up> OK~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
479 > val {where_,...} = Problem.from_store ["2x2", "LINEAR", "system"];
480 > show_types:=true; UnparseC.term @{context} (hd where_); show_types:=false;
482 =========================================================================/
484 -----fun check_match' ff:
485 > (writeln o (I_Model.to_string (Proof_Context.init_global @{theory Isac_Knowledge}))) itms;
487 (1 ,[1] ,true ,#Given ,Cor equalities
488 [0 = - 1 * q_0 * 0 \<up> 2 / 2 + 0 * c + c_2,
489 0 = - 1 * q_0 * L \<up> 2 / 2 + L * c + c_2] ,(es_, [[0 = - 1 * q_0 * 0 \<up> 2 / 2 + 0 * c + c_2,
490 0 = - 1 * q_0 * L \<up> 2 / 2 + L * c + c_2]])),
491 (2 ,[1] ,true ,#Given ,Cor solveForVars [c, c_2] ,(v_s, [[c, c_2]])),
492 (3 ,[1] ,true ,#Find ,Cor solution L ,(ss___, [L]))]
494 > (writeln o pres2str) pre';
496 (false, length_ es_ = 2),
497 (true, length_ [c, c_2] = 2)]
500 > (writeln o (I_Model.to_string (Proof_Context.init_global @{theory Isac_Knowledge}))) itms;
501 > (writeln o pres2str) pre';
504 ----- fun check in Pre_Conds.
505 > (writeln o env2str) env;
507 (es_, [0 = - 1 * q_0 * 0 \<up> 2 / 2 + 0 * c + c_2,
508 0 = - 1 * q_0 * L \<up> 2 / 2 + L * c + c_2])", "
512 > val es_ = (fst o hd) env;
513 val es_ = Free ("es_", "bool List.list") : Term.term
515 > val pre1 = hd pres;
516 TermC.atom_trace_detail @{context} pre1;
518 *** Const (op =, [real, real] => bool)
519 *** . Const (ListG.length_, real list => real)
520 *** . . Free (es_, real list)
521 ~~~~~~~~~~~~~~~~~~~ \<up> \<up> \<up> should be bool list~~~~~~~~~~~~~~~~~~~
525 THE REASON WAS A non-type-constrained variable IN #WHERE OF PROBLEM
526 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
532 "----------- me [EqSystem,normalise,2x2], refine Subproblem ------------------------------------";
533 "----------- me [EqSystem,normalise,2x2], refine Subproblem ------------------------------------";
534 "----------- me [EqSystem,normalise,2x2], refine Subproblem ------------------------------------";
535 val model = ["equalities [0 = - 1 * q_0 * 0 \<up> 2 / 2 + 0 * c + c_2," ^
536 "0 = - 1 * q_0 * L \<up> 2 / 2 + L * c + c_2]",
537 "solveForVars [c, c_2]", "solution LL"];
539 ("Biegelinie",["normalise", "2x2", "LINEAR", "system"],
540 ["EqSystem", "normalise", "2x2"]);
541 val p = e_pos'; val c = [];
542 val (p,_,f,nxt,_,pt) = Test_Code.init_calc @{context} [(model, refs)];
543 val Model_Problem = nxt
544 val (p,_,f,nxt,_,pt) = me nxt p c pt;
545 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
546 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
547 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
548 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
549 val Apply_Method ["EqSystem", "normalise", "2x2"] = nxt
550 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
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; val Subproblem ("Biegelinie", ["triangular", "2x2", "LINEAR", "system"]) = nxt
556 val (p,_,f,nxt,_,pt) = me nxt p c pt; val Model_Problem = nxt
557 val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Given "equalities [c_2 = 0]" = nxt
558 val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Given "equalities [c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2]" = nxt
560 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
561 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
562 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
563 val Specify_Method ["EqSystem", "top_down_substitution", "2x2"] = nxt
564 val (p,_,f,nxt,_,pt) = me nxt p c pt;
565 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
566 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
567 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
568 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
569 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
570 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
571 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
572 val (p,_,f,nxt,_,pt) = me nxt p c pt; val Check_Postcond ["triangular", "2x2", "LINEAR", "system"] = nxt
574 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
575 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
576 (* final test ... ----------------------------------------------------------------------------*)
577 if f2str f = "[c = L * q_0 / 2, c_2 = 0]" then ()
578 else error "eqsystem.sml me [EqSys...2x2] finished f2str f";
582 | _ => error "eqsystem.sml me [EqSys...2x2] finished End_Proof'";
584 Test_Tool.show_pt pt (*[
585 (([], Frm), solveSystem
586 [[0 = - 1 * q_0 * 0 \<up> 2 div 2 + 0 * c + c_2],
587 [0 = - 1 * q_0 * L \<up> 2 div 2 + L * c + c_2]]
589 (([1], Frm), [0 = - 1 * q_0 * 0 \<up> 2 / 2 + 0 * c + c_2,
590 0 = - 1 * q_0 * L \<up> 2 / 2 + L * c + c_2]),
591 (([1], Res), [0 = c_2, 0 = (2 * c_2 + 2 * L * c + - 1 * L \<up> 2 * q_0) / 2]),
592 (([2], Res), [0 = c_2, 0 = - 1 * q_0 * L \<up> 2 / 2 + (L * c + c_2)]),
593 (([3], Res), [c_2 = 0, L * c + c_2 = 0 + - 1 * (- 1 * q_0 * L \<up> 2 / 2)]),
594 (([4], Res), [c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2]),
595 (([5], Pbl), solveSystem [L * c + c_2 = q_0 * L \<up> 2 / 2] [c_2]),
596 (([5, 1], Frm), L * c + c_2 = q_0 * L \<up> 2 / 2),
597 (([5, 1], Res), L * c + 0 = q_0 * L \<up> 2 / 2),
598 (([5, 2], Res), L * c = q_0 * L \<up> 2 / 2),
599 (([5, 3], Res), c = q_0 * L \<up> 2 / 2 / L),
600 (([5, 4], Res), c = L * q_0 / 2),
601 (([5, 5], Frm), [c_2 = 0, c = L * q_0 / 2]),
602 (([5, 5], Res), [c = L * q_0 / 2, c_2 = 0]),
603 (([5], Res), [c = L * q_0 / 2, c_2 = 0]),
604 (([], Res), [c = L * q_0 / 2, c_2 = 0])]