1 (* Title: Knowledge/eqsystem-1.sml
2 author: Walther Neuper 050826,
3 (c) due to copyright terms
6 "-----------------------------------------------------------------";
7 "table of contents -----------------------------------------------";
8 "-----------------------------------------------------------------";
9 "----------- occur_exactly_in ------------------------------------";
10 "----------- problems --------------------------------------------";
11 "----------- rewrite-order ord_simplify_System -------------------";
12 "----------- rewrite in [EqSystem,normalise,2x2] -----------------";
13 "----------- rewrite example from 2nd [EqSystem,normalise,2x2] ---";
14 "----------- rewrite in [EqSystem,top_down_substitution,2x2] -----";
15 "----------- rewrite in [EqSystem,normalise,4x4] -----------------";
16 "----------- script [EqSystem,top_down_substitution,2x2] Vers.1 --";
17 "----------- refine [linear,system]-------------------------------";
18 "----------- refine [2x2,linear,system] search error--------------";
19 (*^^^--- eqsystem-1.sml #####################################################################*)
20 "----------- me [EqSystem,normalise,2x2], refine Subproblem ------------------------------------";
21 (*^^^--- eqsystem-1a.sml #####################################################################
22 vvv--- eqsystem-2.sml #####################################################################*)
23 "----------- me [linear,system] ..normalise..top_down_sub..-------";
24 "----------- all systems from Biegelinie -------------------------";
25 "----------- 4x4 systems from Biegelinie -------------------------";
26 "-----------------------------------------------------------------";
27 "-----------------------------------------------------------------";
28 "-----------------------------------------------------------------";
30 val thy = @{theory "EqSystem"};
31 val ctxt = Proof_Context.init_global thy;
33 "----------- occur_exactly_in ------------------------------------";
34 "----------- occur_exactly_in ------------------------------------";
35 "----------- occur_exactly_in ------------------------------------";
36 val all = [TermC.str2term"c", TermC.str2term"c_2", TermC.str2term"c_3"];
37 val t = TermC.str2term"0 = - 1 * q_0 * L \<up> 2 / 2 + L * c + c_2";
39 if occur_exactly_in [TermC.str2term"c", TermC.str2term"c_2"] all t
40 then () else error "eqsystem.sml occur_exactly_in 1";
42 if not (occur_exactly_in [TermC.str2term"c", TermC.str2term"c_2", TermC.str2term"c_3"] all t)
43 then () else error "eqsystem.sml occur_exactly_in 2";
45 if not (occur_exactly_in [TermC.str2term"c_2"] all t)
46 then () else error "eqsystem.sml occur_exactly_in 3";
48 val t = TermC.str2term"[c,c_2] from [c,c_2,c_3] occur_exactly_in - 1 * q_0 * L \<up> 2 / 2 + L * c + c_2";
49 eval_occur_exactly_in 0 "EqSystem.occur_exactly_in" t 0;
50 val SOME (str, t') = eval_occur_exactly_in 0 "EqSystem.occur_exactly_in" t 0;
51 if str = "[c, c_2] from [c, c_2,\n" ^
52 " c_3] occur_exactly_in - 1 * q_0 * L \<up> 2 / 2 + L * c + c_2 = True"
53 then () else error "eval_occur_exactly_in [c, c_2]";
55 val t = TermC.str2term ("[c,c_2,c_3] from [c,c_2,c_3] occur_exactly_in " ^
56 "- 1 * q_0 * L \<up> 2 / 2 + L * c + c_2");
57 val SOME (str, t') = eval_occur_exactly_in 0 "EqSystem.occur_exactly_in" t 0;
58 if str = "[c, c_2,\n c_3] from [c, c_2,\n" ^
59 " c_3] occur_exactly_in - 1 * q_0 * L \<up> 2 / 2 + L * c + c_2 = False"
60 then () else error "eval_occur_exactly_in [c, c_2, c_3]";
62 val t = TermC.str2term"[c_2] from [c,c_2,c_3] occur_exactly_in \
63 \- 1 * q_0 * L \<up> 2 / 2 + L * c + c_2";
64 val SOME (str, t') = eval_occur_exactly_in 0 "EqSystem.occur_exactly_in" t 0;
65 if str = "[c_2] from [c, c_2,\n" ^
66 " c_3] occur_exactly_in - 1 * q_0 * L \<up> 2 / 2 + L * c + c_2 = False"
67 then () else error "eval_occur_exactly_in [c, c_2, c_3]";
69 val t = TermC.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 error "eval_occur_exactly_in [c, c_2, c_3]";
76 "[] from [c, c_2, c_3, c_4] occur_exactly_in - 1 * (q_0 * L \<up> 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 \<up> 2) / 2 = True" then ()
80 else error "eval_occur_exactly_in [c, c_2, c_3, c_4]";
82 "----------- problems --------------------------------------------";
83 "----------- problems --------------------------------------------";
84 "----------- problems --------------------------------------------";
85 val t = TermC.str2term "Length [x+y=1,y=2] = 2";
87 val testrls = Rule_Set.append_rules "testrls" Rule_Set.empty
88 [(Thm ("LENGTH_NIL", @{thm LENGTH_NIL})),
89 (Thm ("LENGTH_CONS", @{thm LENGTH_CONS})),
90 Eval (\<^const_name>\<open>plus\<close>, Calc_Binop.numeric "#add_"),
91 Eval (\<^const_name>\<open>HOL.eq\<close>,eval_equal "#equal_")
93 val SOME (t',_) = rewrite_set_ ctxt false testrls t;
94 if UnparseC.term t' = "True" then ()
95 else error "eqsystem.sml: length_ [x+y=1,y=2] = 2";
97 val SOME t = TermC.parseNEW ctxt "solution LL";
99 val SOME t = TermC.parseNEW ctxt "solution LL";
102 val t = TermC.str2term
103 "(tl (tl (tl v_s))) from v_s occur_exactly_in (NTH 1 (e_s::bool list))";
105 val t = TermC.str2term ("(tl (tl (tl [c, c_2, c_3, c_4]))) from [c, c_2, c_3, c_4] occur_exactly_in " ^
106 "(NTH 1 [c_4 = 1, 2 = 2, 3 = 3, 4 = 4])");
107 (*----- broken in child of.1790e1073acc : eliminate "handle _ => ..." from Rewrite.rewrite -----\\
108 assume flawed test setup hidden by "handle _ => ..."
109 ERROR rewrite__set_ called with 'Erls' for '1 < 1'
111 rewrite_set_ ctxt true
112 (Rule_Set.append_rules "prls_" Rule_Set.empty
113 [Thm ("NTH_CONS",ThmC.numerals_to_Free @{thm NTH_CONS}),
114 Thm ("NTH_NIL",ThmC.numerals_to_Free @{thm NTH_NIL}),
115 Thm ("TL_CONS",ThmC.numerals_to_Free @{thm tl_Cons}),
116 Thm ("TL_NIL",ThmC.numerals_to_Free @{thm tl_Nil}),
117 Eval ("EqSystem.occur_exactly_in", eval_occur_exactly_in "#eval_occur_exactly_in_")
119 if t = @{term True} then ()
120 else error "eqsystem.sml ..occur_exactly_in (nth_ 1 [c_4..";
121 broken in child of.1790e1073acc : eliminate "handle _ => ..." from Rewrite.rewrite ---//*)
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 \<up> 2 / 2) + c_2";
128 "--- add.commute ---"; (* ... add.commute cf. b42e334c97ee *)
129 if ord_simplify_System false thy [] (TermC.str2term"- 1 * q_0 * (x \<up> 2 / 2)",
130 TermC.str2term"c * x") then ()
131 else error "integrate.sml, (- 1 * q_0 * (x \<up> 2 / 2)) < (c * x) not#1";
133 if ord_simplify_System false thy [] (TermC.str2term"- 1 * q_0 * (x \<up> 2 / 2)",
134 TermC.str2term"c_2") then ()
135 else error "integrate.sml, (- 1 * q_0 * (x \<up> 2 / 2)) < (c_2) not#2";
137 if ord_simplify_System false thy [] (TermC.str2term"c * x",
138 TermC.str2term"c_2") then ()
139 else error "integrate.sml, (c * x) < (c_2) not#3";
141 "--- mult.commute ---";
142 if ord_simplify_System false thy [] (TermC.str2term"x * c",
143 TermC.str2term"c * x") then ()
144 else error "integrate.sml, (x * c) < (c * x) not#4";
146 if ord_simplify_System false thy [] (TermC.str2term"- 1 * q_0 * (x \<up> 2 / 2) * c",
147 TermC.str2term"- 1 * q_0 * c * (x \<up> 2 / 2)")
148 then () else error "integrate.sml, (. * .) < (. * .) not#5";
150 if ord_simplify_System false thy [] (TermC.str2term"- 1 * q_0 * (x \<up> 2 / 2) * c",
151 TermC.str2term"c * - 1 * q_0 * (x \<up> 2 / 2)")
152 then () else error "integrate.sml, (. * .) < (. * .) not#6";
155 "----------- rewrite in [EqSystem,normalise,2x2] -----------------";
156 "----------- rewrite in [EqSystem,normalise,2x2] -----------------";
157 "----------- rewrite in [EqSystem,normalise,2x2] -----------------";
158 val t = TermC.str2term"[0 = - 1 * q_0 * L \<up> 2 / 2 + L * c + c_2,\
159 \0 = - 1 * q_0 * 0 \<up> 2 / 2 + 0 * c + c_2]";
160 val bdvs = [(TermC.str2term"bdv_1",TermC.str2term"c"),
161 (TermC.str2term"bdv_2",TermC.str2term"c_2")];
162 val SOME (t,_) = rewrite_set_inst_ ctxt true bdvs simplify_System_parenthesized t;
163 if UnparseC.term t = "[0 = - 1 * q_0 * L \<up> 2 / 2 + (L * c + c_2), 0 = c_2]"
164 then () else error "eqsystem.sml rewrite in 2x2 simplify_System_par.1";
166 val SOME (t,_) = rewrite_set_inst_ ctxt true bdvs isolate_bdvs t;
167 if UnparseC.term t = "[L * c + c_2 = 0 + - 1 * (- 1 * q_0 * L \<up> 2 / 2), c_2 = 0]"
168 then () else error "eqsystem.sml rewrite in 2x2 isolate_bdvs";
170 val SOME (t,_)= rewrite_set_inst_ ctxt true bdvs simplify_System t;
171 if UnparseC.term t = "[L * c + c_2 = q_0 * L \<up> 2 / 2, c_2 = 0]"
172 then () else error "eqsystem.sml rewrite in 2x2 simplify_System_par.2";
174 "--- 3--- see EqSystem.thy (*..if replaced by 'and' ...*)";
175 val SOME (t,_) = rewrite_set_ ctxt true order_system t;
176 if UnparseC.term t = "[c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2]"
177 then () else error "eqsystem.sml rewrite in 2x2 simplify_System_par.3";
179 "----------- rewrite example from 2nd [EqSystem,normalise,2x2] ---";
180 "----------- rewrite example from 2nd [EqSystem,normalise,2x2] ---";
181 "----------- rewrite example from 2nd [EqSystem,normalise,2x2] ---";
182 val thy = @{theory "Isac_Knowledge"} (*because of Undeclared constant "Biegelinie.EI*);
183 val ctxt = Proof_Context.init_global thy;
185 TermC.str2term"[0 = c_2 + c * 0 + 1 / EI * (L * q_0 / 12 * 0 \<up> 3 + \
186 \ - 1 * q_0 / 24 * 0 \<up> 4),\
187 \ 0 = c_2 + c * L + 1 / EI * (L * q_0 / 12 * L \<up> 3 + \
188 \ - 1 * q_0 / 24 * L \<up> 4)]";
189 val SOME (t, _) = rewrite_set_ ctxt true norm_Rational t;
190 if UnparseC.term t = (*BEFORE "eliminate ThmC.numerals_to_Free"..
191 "[c_2 = 0, 0 = q_0 * L \<up> 4 / (24 * EI) + (L * c + c_2)]"*)
192 "[0 = c_2, 0 = (24 * c_2 + 24 * L * c + L \<up> 4 * q_0) / 24]"
193 then () else error "eqsystem.sml rewrite in 2x2 simplify_System_par.0b";
195 val SOME(t, _)= rewrite_set_inst_ ctxt true bdvs simplify_System_parenthesized t;
196 if UnparseC.term t = (*BEFORE "eliminate ThmC.numerals_to_Free"..
197 "[c_2 = 0, 0 = q_0 * L \<up> 4 / (24 * EI) + (L * c + c_2)]"*)
198 "[0 = c_2, 0 = q_0 * L \<up> 4 / 24 + (L * c + c_2)]"
199 then () else error "eqsystem.sml rewrite in 2x2 simplify_System_par.1b";
201 val SOME (t,_) = rewrite_set_inst_ ctxt true bdvs isolate_bdvs t;
202 if UnparseC.term t = (*BEFORE "eliminate ThmC.numerals_to_Free"..
203 "[c_2 = 0, L * c + c_2 = 0 + - 1 * (q_0 * L \<up> 4 / (24 * EI))]"*)
204 "[c_2 = 0, L * c + c_2 = 0 + - 1 * (q_0 * L \<up> 4 / 24)]"
205 then () else error "eqsystem.sml rewrite in 2x2 isolate_bdvs b";
207 val SOME(t,_)= rewrite_set_inst_ ctxt true bdvs simplify_System t;
208 if UnparseC.term t = (*BEFORE "eliminate ThmC.numerals_to_Free"..
209 "[c_2 = 0, L * c + c_2 = - 1 * q_0 * L \<up> 4 / (24 * EI)]"*)
210 "[c_2 = 0, L * c + c_2 = - 1 * q_0 * L \<up> 4 / 24]"
211 then () else error "eqsystem.sml rewrite in 2x2 simplify_System.2b";
213 val xxx = rewrite_set_ ctxt true order_system t;
215 then () else error "eqsystem.sml rewrite in 2x2 simplify_System.3b";
218 "----------- rewrite in [EqSystem,top_down_substitution,2x2] -----";
219 "----------- rewrite in [EqSystem,top_down_substitution,2x2] -----";
220 "----------- rewrite in [EqSystem,top_down_substitution,2x2] -----";
221 val e1__ = TermC.str2term "c_2 = 77";
222 val e2__ = TermC.str2term "L * c + c_2 = q_0 * L \<up> 2 / 2";
223 val bdvs = [(TermC.str2term"bdv_1",TermC.str2term"c"),
224 (TermC.str2term"bdv_2",TermC.str2term"c_2")];
225 val SOME (e2__,_) = rewrite_terms_ ctxt Rewrite_Ord.function_empty Rule_Set.Empty [e1__] e2__;
226 if UnparseC.term e2__ = "L * c + 77 = q_0 * L \<up> 2 / 2" then ()
227 else error "eqsystem.sml top_down_substitution,2x2] subst";
230 rewrite_set_inst_ ctxt true bdvs simplify_System_parenthesized e2__;
231 if UnparseC.term e2__ = "77 + L * c = q_0 * L \<up> 2 / 2" then ()
232 else error "eqsystem.sml top_down_substitution,2x2] simpl_par";
234 val SOME (e2__,_) = rewrite_set_inst_ ctxt true bdvs isolate_bdvs e2__;
235 if UnparseC.term e2__ = "c = (q_0 * L \<up> 2 / 2 + - 1 * 77) / L" then ()
236 else error "eqsystem.sml top_down_substitution,2x2] isolate";
238 val t = TermC.str2term "[c_2 = 77, c = (q_0 * L \<up> 2 / 2 + - 1 * 77) / L]";
239 val SOME (t,_) = rewrite_set_ ctxt true order_system t;
240 if UnparseC.term t = "[c = (q_0 * L \<up> 2 / 2 + - 1 * 77) / L, c_2 = 77]" then ()
241 else error "eqsystem.sml top_down_substitution,2x2] order_system";
243 if not (ord_simplify_System
245 (TermC.str2term"[c_2 = 77, c = (q_0 * L \<up> 2 / 2 + - 1 * 77) / L]",
246 TermC.str2term"[c = (q_0 * L \<up> 2 / 2 + - 1 * 77) / L, c_2 = 77]"))
247 then () else error "eqsystem.sml, order_result rew_ord";
250 "----------- rewrite in [EqSystem,normalise,4x4] -----------------";
251 "----------- rewrite in [EqSystem,normalise,4x4] -----------------";
252 "----------- rewrite in [EqSystem,normalise,4x4] -----------------";
253 (*STOPPED.WN06?: revise rewrite in [EqSystem,normalise,4x4] from before 0609*)
254 val t = TermC.str2term (
255 "[(0::real) = - 1 * q_0 * 0 \<up> 2 / 2 + 0 * c_3 + c_4, " ^
256 "(0::real) = - 1 * q_0 * L \<up> 2 / 2 + L * c_3 + c_4, " ^
257 "c + c_2 + c_3 + c_4 = 0, " ^
258 "c_2 + c_3 + c_4 = 0]");
259 val bdvs = [(TermC.str2term"bdv_1::real",TermC.str2term"c::real"),
260 (TermC.str2term"bdv_2::real",TermC.str2term"c_2::real"),
261 (TermC.str2term"bdv_3::real",TermC.str2term"c_3::real"),
262 (TermC.str2term"bdv_4::real",TermC.str2term"c_4::real")];
264 rewrite_set_inst_ ctxt true bdvs simplify_System_parenthesized t;
265 if UnparseC.term 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]"
266 then () else error "eqsystem.sml rewrite in 4x4 simplify_System_paren";
268 val SOME (t, _) = rewrite_set_inst_ ctxt true bdvs isolate_bdvs t;
269 if UnparseC.term t = "[c_4 = 0, \
270 \L * c_3 + c_4 = 0 + - 1 * (- 1 * q_0 * L \<up> 2 / 2),\n \
271 \c + (c_2 + (c_3 + c_4)) = 0, c_2 + (c_3 + c_4) = 0]"
272 then () else error "eqsystem.sml rewrite in 4x4 isolate_bdvs";
274 val SOME(t, _)= rewrite_set_inst_ ctxt true bdvs simplify_System_parenthesized t;
275 if UnparseC.term t = "[c_4 = 0,\
276 \ L * c_3 + c_4 = q_0 * L \<up> 2 / 2,\
277 \ c + (c_2 + (c_3 + c_4)) = 0,\n\
278 \ c_2 + (c_3 + c_4) = 0]"
279 then () else error "eqsystem.sml rewrite in 4x4 simplify_System_p..2";
281 val SOME (t, _) = rewrite_set_ ctxt true order_system t;
282 if UnparseC.term t = "[c_4 = 0,\
283 \ L * c_3 + c_4 = q_0 * L \<up> 2 / 2,\
284 \ c_2 + (c_3 + c_4) = 0,\n\
285 \ c + (c_2 + (c_3 + c_4)) = 0]"
286 then () else error "eqsystem.sml rewrite in 4x4 order_system";
288 "----------- refine [linear,system]-------------------------------";
289 "----------- refine [linear,system]-------------------------------";
290 "----------- refine [linear,system]-------------------------------";
292 ["equalities [0 = - 1 * q_0 * 0 \<up> 2 / 2 + 0 * c + c_2," ^
293 "0 = - 1 * q_0 * L \<up> 2 / 2 + L * c + (c_2::real)]",
294 "solveForVars [c, c_2]", "solution LL"];
296 (*WN120313 in "solution L" above "Refine.refine_PIDE @{context} fmz ["LINEAR", "system"]" caused an error...*)
297 "~~~~~ fun Refine.refine , args:"; val ((fmz: Formalise.model), (pblID:Problem.id)) = (fmz, ["LINEAR", "system"]);
298 "~~~~~ fun refin' , args:"; val ((pblRD: Problem.id_reverse), fmz, pbls, ((Store.Node (pI, [py], [])): Problem.T Store.node)) =
299 ((rev o tl) pblID, fmz, [(*match list*)],
300 ((Store.Node ("LINEAR", [Problem.from_store ctxt ["LINEAR", "system"]], [])): Problem.T Store.node));
301 val {thy, ppc, where_, prls, ...} = py ;
302 "~~~~~ fun O_Model.init, args:"; val (thy, fmz, pbt) = (thy, fmz, ppc);
303 val ctxt = Proof_Context.init_global thy;
304 "~~~~~ fun declare_constraints, args:"; val (t, ctxt) = (nth 1 fmz, ctxt);
305 fun get_vars ((v,T)::vs) = (case raw_explode v |> Library.read_int of
306 (_, _::_) => (Free (v,T)::get_vars vs)
307 | (_, [] ) => get_vars vs) (*filter out nums as long as
308 we have Free ("123",_)*)
310 t = "equalities [0 = - 1 * q_0 * 0 \<up> 2 / 2 + 0 * c + c_2,"^
311 "0 = - 1 * q_0 * L \<up> 2 / 2 + L * c + (c_2::real)]";
312 val ts = Term.add_frees (Syntax.read_term ctxt t) [] |> get_vars;
313 val ctxt = Variable.declare_constraints (nth 1 ts) ctxt;
314 val ctxt = Variable.declare_constraints (nth 2 ts) ctxt;
315 val ctxt = Variable.declare_constraints (nth 3 ts) ctxt;
316 val ctxt = Variable.declare_constraints (nth 4 ts) ctxt;
317 val t = nth 2 fmz; t = "solveForVars [c, c_2]";
318 val ts = Term.add_frees (Syntax.read_term ctxt t) [] |> get_vars;
319 val ctxt = Variable.declare_constraints (nth 1 ts) ctxt;
320 val t = nth 3 fmz; t = "solution LL";
321 (*(Syntax.read_term ctxt t);
322 Type unification failed: Clash of types "real" and "_ list"
323 Type error in application: incompatible operand type
325 Operator: solution :: bool list \<Rightarrow> toreall
326 Operand: L :: real ========== L was already present in equalities ========== *)
328 "===== case 1 =====";
329 val matches = Refine.refine_PIDE @{context} fmz ["LINEAR", "system"];
331 [M_Match.Matches (["LINEAR", "system"], _), (*Matches*)
332 M_Match.Matches (["2x2", "LINEAR", "system"], _), (*NoMatch ! GOON !*)
333 M_Match.NoMatch (["triangular", "2x2", "LINEAR", "system"], _), (**)
334 M_Match.Matches (["normalise", "2x2", "LINEAR", "system"], (**)
335 {Find = [Correct "solution LL"], With = [], (**)
336 Given = [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]",
337 Correct "solveForVars [c, c_2]"],
340 | _ => error "eqsystem.sml Refine.refine ['normalise','2x2'...]";
342 "===== case 2 =====";
343 val fmz = ["equalities [c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2]",
344 "solveForVars [c, c_2]", "solution LL"];
345 val matches = Refine.refine_PIDE @{context} fmz ["LINEAR", "system"];
346 case matches of [_,_,
348 (["triangular", "2x2", "LINEAR", "system"],
349 {Find = [Correct "solution LL"],
352 [Correct "equalities [c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2]",
353 Correct "solveForVars [c, c_2]"],
355 "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]",
357 "[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]"],
359 | _ => error "eqsystem.sml Refine.refine ['triangular','2x2'...]";
361 (*WN051014-----------------------------------------------------------------------------------\\
362 the above 'val matches = Refine.refine_PIDE @{context} fmz ["LINEAR", "system"]'
363 didn't work anymore; we investigated in these steps:*)
364 val fmz = ["equalities [c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2]",
365 "solveForVars [c, c_2]", "solution LL"];
366 val matches = Refine.refine_PIDE @{context} fmz ["triangular", "2x2", "LINEAR", "system"];
368 False "[c, c_2] from_ [c, c_2] occur_exactly_in nth_ 2\n
369 [c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2]"]*)
370 val t = TermC.str2term ("[c, c_2] from [c, c_2] occur_exactly_in NTH 2" ^
371 "[c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2]");
373 val SOME (t', _) = rewrite_set_ ctxt false prls_triangular t;
376 ### eval asms: 1 < 2 + - 1
377 ==> nth_ (2 + - 1) [L * c + c_2 = q_0 * L \<up> 2 / 2] =
378 nth_ (2 + - 1 + - 1) []
379 #### rls: erls_prls_triangular on: 1 < 2 + - 1
380 ##### try calc: op <'
381 ### asms accepted: ["1 < 2 + - 1"] stored: ["1 < 2 + - 1"]
383 ... i.e Eval ("Groups.plus_class.plus", Calc_Binop.numeric "#add_") was missing in erls_prls_triangular*)
384 (*--------------------------------------------------------------------------------------------//*)
387 "===== case 3: relaxed preconditions for triangular system =====";
388 val fmz = ["equalities [L * q_0 = c, \
389 \ 0 = (2 * c_2 + 2 * L * c + - 1 * L \<up> 2 * q_0) / 2,\
392 "solveForVars [c, c_2, c_3, c_4]", "solution LL"];
393 (*============ inhibit exn WN120314 TODO: investigate type error (same) in these 2 cases:
394 probably exn thrown by fun declare_constraints
395 /-------------------------------------------------------\
396 Type unification failed
397 Type error in application: incompatible operand type
399 Operator: op # c_3 :: 'a list \<Rightarrow> 'a list
400 Operand: [c_4] :: 'b list
401 \-------------------------------------------------------/
402 val TermC.matches = Refine.refine fmz ["LINEAR", "system"];
403 case TermC.matches of
404 [M_Match.Matches (["LINEAR", "system"], _),
405 M_Match.NoMatch (["2x2", "LINEAR", "system"], _),
406 M_Match.NoMatch (["3x3", "LINEAR", "system"], _),
407 M_Match.Matches (["4x4", "LINEAR", "system"], _),
408 M_Match.NoMatch (["triangular", "4x4", "LINEAR", "system"], _),
409 M_Match.Matches (["normalise", "4x4", "LINEAR", "system"], _)] => ()
410 | _ => error "eqsystem.sml: Refine.refine relaxed triangular sys M_Match.NoMatch";
411 (*WN060914 does NOT match, because 3rd and 4th equ are not ordered*)
413 "===== case 4 =====";
414 val fmz = ["equalities [L * q_0 = c, \
415 \ 0 = (2 * c_2 + 2 * L * c + - 1 * L \<up> 2 * q_0) / 2,\
418 "solveForVars [c, c_2, c_3, c_4]", "solution LL"];
419 val TermC.matches = Refine.refine fmz ["triangular", "4x4", "LINEAR", "system"];
420 case TermC.matches of
421 [M_Match.Matches (["triangular", "4x4", "LINEAR", "system"], _)] => ()
422 | _ => error "eqsystem.sml: Refine.refine relaxed triangular sys M_Match.NoMatch";
423 val TermC.matches = Refine.refine fmz ["LINEAR", "system"];
424 ============ inhibit exn WN120314 ==============================================*)
426 "----------- Refine.refine [2x2,linear,system] search error--------------";
427 "----------- Refine.refine [2x2,linear,system] search error--------------";
428 "----------- Refine.refine [2x2,linear,system] search error--------------";
429 (*didn't go into ["2x2", "LINEAR", "system"];
430 we investigated in these steps:*)
431 val fmz = ["equalities [0 = - 1 * q_0 * 0 \<up> 2 / 2 + 0 * c + c_2,\
432 \0 = - 1 * q_0 * L \<up> 2 / 2 + L * c + c_2]",
433 "solveForVars [c, c_2]", "solution LL"];
434 val matches = Refine.refine_PIDE @{context} fmz ["2x2", "LINEAR", "system"];
435 (*default_print_depth 11;*) TermC.matches; (*default_print_depth 3;*)
436 (*brought: 'False "length_ es_ = 2"'*)
438 (*-----fun refin' (pblRD:Problem.id_reverse) fmz pbls ((Store.Node (pI,[py],[])):pbt Store.store) =
439 (* val ((pblRD:Problem.id_reverse), fmz, pbls, ((Store.Node (pI,[py],[])):pbt Store.store)) =
440 (rev ["LINEAR", "system"], fmz, [(*match list*)],
441 ((Store.Node ("2x2",[Problem.from_store ["2x2", "LINEAR", "system"]],[])):pbt Store.store));
443 > show_types:=true; UnparseC.term (hd where_); show_types:=false;
444 val it = "length_ (es_::real list) = (2::real)" : string
446 =========================================================================\
447 -------fun Problem.prep_input
448 (* val (thy, (pblID, dsc_dats: (string * (string list)) list,
449 ev:rls, ca: string option, metIDs:metID list)) =
450 (EqSystem.thy, (["system"],
451 [("#Given" ,["equalities es_", "solveForVars v_s"]),
452 ("#Find" ,["solution ss___"](*___ is copy-named*))
454 Rule_Set.append_rules "empty" Rule_Set.empty [(*for preds in where_*)],
455 SOME "solveSystem es_ v_s",
458 > val [("#Given", [equalities_es_, "solveForVars v_s"])] = gi;
459 val equalities_es_ = "equalities es_" : string
460 > val (dd, ii) = (split_did o Thm.term_of o the o (TermC.parse thy)) equalities_es_;
461 > show_types:=true; UnparseC.term ii; show_types:=false;
462 val it = "es_::bool list" : string
463 ~~~~~~~~~~~~~~~ \<up> \<up> \<up> OK~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
465 > val {where_,...} = Problem.from_store ["2x2", "LINEAR", "system"];
466 > show_types:=true; UnparseC.term (hd where_); show_types:=false;
468 =========================================================================/
471 > (writeln o (I_Model.to_string (Proof_Context.init_global @{theory Isac_Knowledge}))) itms;
473 (1 ,[1] ,true ,#Given ,Cor equalities
474 [0 = - 1 * q_0 * 0 \<up> 2 / 2 + 0 * c + c_2,
475 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,
476 0 = - 1 * q_0 * L \<up> 2 / 2 + L * c + c_2]])),
477 (2 ,[1] ,true ,#Given ,Cor solveForVars [c, c_2] ,(v_s, [[c, c_2]])),
478 (3 ,[1] ,true ,#Find ,Cor solution L ,(ss___, [L]))]
480 > (writeln o pres2str) pre';
482 (false, length_ es_ = 2),
483 (true, length_ [c, c_2] = 2)]
485 ----- fun match_oris':
486 > (writeln o (I_Model.to_string (Proof_Context.init_global @{theory Isac_Knowledge}))) itms;
487 > (writeln o pres2str) pre';
490 ----- fun check in Pre_Conds.
491 > (writeln o env2str) env;
493 (es_, [0 = - 1 * q_0 * 0 \<up> 2 / 2 + 0 * c + c_2,
494 0 = - 1 * q_0 * L \<up> 2 / 2 + L * c + c_2])", "
498 > val es_ = (fst o hd) env;
499 val es_ = Free ("es_", "bool List.list") : Term.term
501 > val pre1 = hd pres;
504 *** Const (op =, [real, real] => bool)
505 *** . Const (ListG.length_, real list => real)
506 *** . . Free (es_, real list)
507 ~~~~~~~~~~~~~~~~~~~ \<up> \<up> \<up> should be bool list~~~~~~~~~~~~~~~~~~~
511 THE REASON WAS A non-type-constrained variable IN #WHERE OF PROBLEM
512 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
515 "----------- me [EqSystem,normalise,2x2], refine Subproblem ------------------------------------";
516 "----------- me [EqSystem,normalise,2x2], refine Subproblem ------------------------------------";
517 "----------- me [EqSystem,normalise,2x2], refine Subproblem ------------------------------------";
518 val fmz = ["equalities [0 = - 1 * q_0 * 0 \<up> 2 / 2 + 0 * c + c_2,\
519 \0 = - 1 * q_0 * L \<up> 2 / 2 + L * c + c_2]",
520 "solveForVars [c, c_2]", "solution LL"];
522 ("Biegelinie",["normalise", "2x2", "LINEAR", "system"],
523 ["EqSystem", "normalise", "2x2"]);
524 val p = e_pos'; val c = [];
525 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
526 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
527 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
528 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
529 val (p,_,f,nxt,_,pt) = me nxt p c pt;
530 case nxt of Specify_Method ["EqSystem", "normalise", "2x2"] => ()
531 | _ => error "eqsystem.sml [EqSystem,normalise,2x2] specify";
533 val (p,_,f,nxt,_,pt) = me nxt p c pt;
534 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
535 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*);
536 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
537 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
538 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
540 (Subproblem ("Biegelinie", ["triangular", "2x2", "LINEAR",_])) => ()
541 | _ => error "eqsystem.sml me [EqSystem,normalise,2x2] SubProblem";
543 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
544 val (p,_,f,nxt,_,pt) = me nxt p c pt;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;
548 (Specify_Method ["EqSystem", "top_down_substitution", "2x2"]) => ()
549 | _ => error "eqsystem.sml me [EqSys...2x2] top_down_substitution";
551 val (p,_,f,nxt,_,pt) = me nxt p c pt;
552 val PblObj {probl,...} = get_obj I pt [5];
553 (writeln o (I_Model.to_string (Proof_Context.init_global @{theory Isac_Knowledge}))) probl;
555 (1 ,[1] ,true ,#Given ,Cor equalities [c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2] ,(es_, [[c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2]])),
556 (2 ,[1] ,true ,#Given ,Cor solveForVars [c, c_2] ,(v_s, [[c, c_2]])),
557 (3 ,[1] ,true ,#Find ,Cor solution ss___ ,(ss___, [ss___]))]
559 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
560 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
561 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
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 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
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;
568 (Check_Postcond ["triangular", "2x2", "LINEAR", "system"]) => ()
569 | _ => error "eqsystem.sml me Subpbl .[EqSys...2x2] finished";
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 if f2str f = "[c = L * q_0 / 2, c_2 = 0]" then ()
573 else error "eqsystem.sml me [EqSys...2x2] finished f2str f";
576 | _ => error "eqsystem.sml me [EqSys...2x2] finished End_Proof'";