2 imports "Isac.Build_Isac" "$ISABELLE_ISAC_TEST/Tools/isac/ADDTESTS/accumulate-val/Lucas_Interpreter"
5 ML \<open>open ML_System\<close>
9 open Test_Code; CalcTreeTEST;
10 open LItool; arguments_from_model;
18 open Error_Pattern_Def;
20 open Ctree; append_problem;
26 open Auto_Prog; rule2stac;
33 open Solve; (* NONE *)
34 open ContextC; transfer_asms_from_to;
35 open Tactic; (* NONE *)
38 open P_Model; (* NONE *)
43 open Rule_Set; Sequence;
51 (**)ML_file "BridgeJEdit/vscode-example.sml"(**)
53 section \<open>code for copy & paste ===============================================================\<close>
55 "~~~~~ fun xxx , args:"; val () = ();
56 "~~~~~ and xxx , args:"; val () = ();
57 "~~~~~ from fun xxx \<longrightarrow>fun yyy \<longrightarrow>fun zzz , return:"; val () = ();
58 (*if*) (*then*); (*else*); (*case*) (*of*); (*return value*); (*in*) (*end*);
60 ^ "xxx" (*+*) (*+++*) (*!for return!*) (*isa*) (*REP*) (**)
61 \<close> ML \<open> (*//---------------- adhoc inserted ------------------------------------------------\\*)
63 \<close> ML \<open> (*\\---------------- adhoc inserted ------------------------------------------------//*)
64 \<close> ML \<open> (*//---------------- adhoc copied up -----------------------------------------------\\*)
66 \<close> ML \<open> (*\\---------------- adhoc copied up -----------------------------------------------//*)
67 (*/------------------- step into XXXXX -----------------------------------------------------\*)
68 (*-------------------- stop step into XXXXX -------------------------------------------------*)
69 (*\------------------- step into XXXXX -----------------------------------------------------/*)
70 (*-------------------- contiue step into XXXXX ----------------------------------------------*)
71 (*/------------------- check entry to XXXXX ------------------------------------------------\*)
72 (*\------------------- check entry to XXXXX ------------------------------------------------/*)
73 (*/------------------- check within XXXXX --------------------------------------------------\*)
74 (*\------------------- check within XXXXX --------------------------------------------------/*)
75 (*/------------------- check result of XXXXX -----------------------------------------------\*)
76 (*\------------------- check result of XXXXX -----------------------------------------------/*)
78 (*/------------------- build new fun XXXXX -------------------------------------------------\*)
79 (*\------------------- build new fun XXXXX -------------------------------------------------/*)
80 (**** chapter ############################################################################ ****)
81 (*** section ============================================================================== ***)
82 (** subsection ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ **)
83 (* subsubsection ............................................................................ *)
91 declare [[show_types]]
92 declare [[show_sorts]]
93 find_theorems "?a <= ?a"
99 ML_command \<open>Pretty.writeln prt\<close>
100 declare [[ML_print_depth = 999]]
101 declare [[ML_exception_trace]]
104 section \<open>===================================================================================\<close>
111 section \<open>===== "Specify/cas-command.sml" ==================================================\<close>
115 "----------- start Calculation with CAS_Cmd ----------------------------------------------------";
116 "----------- start Calculation with CAS_Cmd ----------------------------------------------------";
117 "----------- start Calculation with CAS_Cmd ----------------------------------------------------";
120 val (dI',pI',mI') = References.empty;
122 CalcTreeTEST [(fmz, (dI',pI',mI'))]
124 "~~~~~ fun CalcTreeTEST, args:"; val [(fmz, sp): Formalise.T] = [(fmz, (dI',pI',mI'))];
125 "~~~~~ fun nxt_specify_init_calc , args:"; val (fmz : Formalise.model, (dI, pI, mI) : References.T) = (fmz, sp);
126 val thy = ThyC.get_theory dI;
128 (*if*) mI = ["no_met"]; (*else*)
132 pI = ["empty_probl_id"];
134 mI = ["empty_meth_id"];
139 \<close> text \<open>
140 replaceFormula 1 "Simplify (2*a + 3*a)";
146 section \<open>===== "Interpret/lucas-interpreter.sml" ==========================================\<close>
150 (* Title: "Interpret/lucas-interpreter.sml"
151 Author: Walther Neuper
152 (c) due to copyright terms
155 "-----------------------------------------------------------------------------------------------";
156 "table of contents -----------------------------------------------------------------------------";
157 "-----------------------------------------------------------------------------------------------";
158 "----------- Take as 1st stac in program -------------------------------------------------------";
159 "----------- re-build: fun locate_input_tactic -------------------------------------------------";
160 "----------- fun locate_input_tactic Helpless, NOT applicable ----------------------------------";
161 "----------- re-build: fun find_next_step, mini ------------------------------------------------";
162 "----------- re-build: fun locate_input_term ---------------------------------------------------";
163 "-----------------------------------------------------------------------------------------------";
164 "-----------------------------------------------------------------------------------------------";
165 "-----------------------------------------------------------------------------------------------";
167 "----------- Take as 1st stac in program -------------------------------------------------------";
168 "----------- Take as 1st stac in program -------------------------------------------------------";
169 "----------- Take as 1st stac in program -------------------------------------------------------";
170 "compare --- Apply_Method with initial Take by Step.do_next --- in test/../step-solve ----------";
171 val p = e_pos'; val c = [];
172 val (p,_,f,nxt,_,pt) =
174 [(["functionTerm (x \<up> 2 + 1)", "integrateBy x", "antiDerivative FF"],
175 ("Integrate", ["integrate", "function"], ["diff", "integration"]))];
176 val (p,_,f,nxt,_,pt) = me nxt p c pt; (*nxt = ("Tac ", ...) --> Add_Given...*)
177 val (p,_,f,nxt,_,pt) = me nxt p c pt;
178 val (p,_,f,nxt,_,pt) = me nxt p c pt;
179 val (p,_,f,nxt,_,pt) = me nxt p c pt;
180 val (p,_,f,nxt,_,pt) = me nxt p c pt;
181 val (p,_,f,nxt,_,pt) = me nxt p c pt;
182 val (p,_,f,nxt,_,pt) = me nxt p c pt;
183 case nxt of (Apply_Method ["diff", "integration"]) => ()
184 | _ => error "integrate.sml -- me method [diff,integration] -- spec";
185 "----- step 8: returns nxt = Rewrite_Set_Inst ([\"(''bdv'', x)\"],\"integration\")";
187 "~~~~~ fun me, args:"; val (tac, (p:pos'), _, (pt:ctree)) = (nxt, p, c, pt);
188 "~~~~~ fun Step.by_tactic, args:"; val (tac, (ptp as (pt, p))) = (tac, (pt,p));
189 val Applicable.Yes m = Step.check tac (pt, p);
190 (*if*) Tactic.for_specify' m; (*false*)
191 "~~~~~ fun loc_solve_ , args:"; val (m, (pt,pos)) = (m, ptp);
193 "~~~~~ fun Step_Solve.by_tactic , args:"; val (m as Apply_Method' (mI, _, _, ctxt), (pt, (pos as (p,_))))
195 val {srls, ...} = MethodC.from_store mI;
196 val itms = case get_obj I pt p of
197 PblObj {meth=itms, ...} => itms
198 | _ => error "solve Apply_Method: uncovered case get_obj"
199 val thy' = get_obj g_domID pt p;
200 val thy = ThyC.get_theory thy';
201 val srls = LItool.get_simplifier (pt, pos)
202 val (is, env, ctxt, sc) = case LItool.init_pstate srls ctxt itms mI of
203 (is as Istate.Pstate {env, ...}, ctxt, sc) => (is, env, ctxt, sc)
204 | _ => error "solve Apply_Method: uncovered case init_pstate";
205 (*+*)pstate2str (the_pstate is) = "([\"\n(f_f, x \<up> 2 + 1)\",\"\n(v_v, x)\"], [], empty, NONE, \n??.empty, ORundef, false, true)";
206 val ini = LItool.implicit_take sc env;
209 val NONE = (*case*) ini (*of*);
210 val Next_Step (is', ctxt', m') =
211 LI.find_next_step sc (pt, (p, Res)) is ctxt;
212 (*+*)pstate2str (the_pstate is') = "([\"\n(f_f, x \<up> 2 + 1)\",\"\n(v_v, x)\"], [R,L,R], empty, NONE, \nIntegral x \<up> 2 + 1 D x, ORundef, false, false)";
213 val Safe_Step (_, _, Take' _) = (*case*)
214 locate_input_tactic sc (pt, (p, Res)) is' ctxt' m' (*of*);
215 "~~~~~ fun locate_input_tactic , args:"; val ((Prog prog), cstate, istate, ctxt, tac)
216 = (sc, (pt, (p, Res)), is', ctxt', m');
218 (*case*) scan_to_tactic1 (prog, (cstate, ctxt, tac)) istate (*of*);
219 "~~~~~ fun scan_to_tactic1 , args:"; val ((prog, (cctt as ((_, p), _, _))), (Istate.Pstate (ist as {path, ...})))
220 = ((prog, (cstate, ctxt, tac)), istate);
221 (*if*) path = [] orelse ((last_elem o fst) p = 0 andalso snd p = Res) (*then*);
223 val Accept_Tac1 (_, _, Take' _) =
224 scan_dn1 cctt (ist |> set_path [R] |> set_or ORundef) (Program.body_of prog);
225 "~~~~~ fun scan_dn1 , args:"; val (xxx, ist, (Const (\<^const_name>\<open>Let\<close>, _) $ e $ (Abs (id, T, b))))
226 = (cctt, (ist |> set_path [R] |> set_or ORundef), (Program.body_of prog));
228 (*+*) if UnparseC.term e = "Take (Integral f_f D v_v)" then () else error "scan_dn1 Integral changed";
231 scan_dn1 xxx (ist |> path_down [L, R]) e (*of*);
232 (*======= end of scanning tacticals, a leaf =======*)
233 "~~~~~ fun scan_dn1 , args:"; val (((pt, p), ctxt, tac), (ist as {eval, or, ...}), t)
234 = (xxx, (ist |> path_down [L, R]), e);
235 val (Program.Tac stac, a') = check_leaf "locate" ctxt eval (get_subst ist) t;
239 "----------- re-build: fun locate_input_tactic -------------------------------------------------";
240 "----------- re-build: fun locate_input_tactic -------------------------------------------------";
241 "----------- re-build: fun locate_input_tactic -------------------------------------------------";
242 val fmz = ["equality (x+1=(2::real))", "solveFor x", "solutions L"];
243 val (dI',pI',mI') = ("Test", ["sqroot-test", "univariate", "equation", "test"],
244 ["Test", "squ-equ-test-subpbl1"]);
245 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
246 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
247 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
248 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
249 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
250 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
251 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
252 (*[], Met*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = (_, Apply_Method ["Test", "squ-equ-test-subpbl1"])*);
253 (*[1], Frm*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = ("Rewrite_Set", Rewrite_Set "norm_equation")*)
255 (*//------------------ begin step into ------------------------------------------------------\\*)
256 (*[1], Res*)val (p'''''_''',_,f,nxt'''''_''',_,pt'''''_''') = me nxt p [] pt; (*nxt = Rewrite_Set "Test_simplify"*)
258 "~~~~~ fun me , args:"; val (tac, p, _(*NEW remove*), pt) = (nxt, p, [], pt);
260 (** )val (***)xxxx(***) ( *("ok", (_, _, (pt, p))) =( **) (*case*)
261 Step.by_tactic tac (pt,p) (*of*);
262 "~~~~~ fun by_tactic , args:"; val (tac, (ptp as (pt, p))) = (tac, (pt,p));
263 val Applicable.Yes m = (*case*) Solve_Step.check tac (pt, p) (*of*);
264 (*if*) Tactic.for_specify' m; (*false*)
266 (** )val (***)xxxxx_x(***) ( *(msg, cs') =( **)
267 Step_Solve.by_tactic m ptp;
268 "~~~~~ fun by_tactic , args:"; val (m, (pt, po as (p, p_))) = (m, ptp);
269 (*+*)val (pt'''''_', (p'''''_', p_'''''_')) = (pt, (p, p_));
270 (*if*) MethodC.id_empty = get_obj g_metID pt (par_pblobj pt p); (*else*)
271 val thy' = get_obj g_domID pt (par_pblobj pt p);
272 val (is, sc) = LItool.resume_prog thy' (p,p_) pt;
274 locate_input_tactic sc (pt, po) (fst is) (snd is) m;
275 "~~~~~ fun locate_input_tactic , args:"; val (Prog prog, cstate, istate, ctxt, tac)
276 = (sc, (pt, po), (fst is), (snd is), m);
277 val srls = get_simplifier cstate;
279 (** )val Accept_Tac1 ((is as (_,_,_,_,_,strong_ass), ctxt, ss as((tac', _, ctree, pos', _) :: _))) =( **)
280 (*case*) scan_to_tactic1 (prog, (cstate, ctxt, tac)) istate (*of*);
281 "~~~~~ fun scan_to_tactic1 , args:"; val ((prog, (cctt as ((_, p), _, _))), (Istate.Pstate (ist as {path, ...})))
282 = ((prog, (cstate, ctxt, tac)), istate);
283 (*if*) path = [] orelse ((last_elem o fst) p = 0 andalso snd p = Res) (*then*);
285 (** )val xxxxx_xx = ( **)
286 scan_dn1 cctt (ist |> set_path [R] |> set_or ORundef) (Program.body_of prog);
287 "~~~~~ fun scan_dn1 , args:"; val (xxx, ist, (Const (\<^const_name>\<open>Let\<close>, _) $ e $ (Abs (id, T, b))))
288 = (cctt, (ist |> set_path [R] |> set_or ORundef), (Program.body_of prog));
290 (*case*) scan_dn1 xxx (ist |> path_down [L, R]) e (*of*);
291 "~~~~~ fun scan_dn1 , args:"; val ((xxx as (cstate, _, _)), ist, (Const (\<^const_name>\<open>Chain\<close>(*1*), _) $ e1 $ e2 $ a))
292 = (xxx, (ist |> path_down [L, R]), e);
294 (*case*) scan_dn1 xxx (ist |> path_down_form ([L, L, R], a)) e1 (*of*);
295 "~~~~~ fun scan_dn1 , args:"; val (xxx, ist, (Const (\<^const_name>\<open>Try\<close>(*2*), _) $ e))
296 = (xxx, (ist |> path_down_form ([L, L, R], a)), e1);
298 (*case*) scan_dn1 xxx (ist |> path_down [R]) e (*of*);
299 (*======= end of scanning tacticals, a leaf =======*)
300 "~~~~~ fun scan_dn1 , args:"; val (((pt, p), ctxt, tac), (ist as {env, eval, or, ...}), t)
301 = (xxx, (ist |> path_down [R]), e);
302 val (Program.Tac stac, a') =
303 (*case*) check_leaf "locate" ctxt eval (get_subst ist) t (*of*);
304 val LItool.Associated (m, v', ctxt) =
305 (*case*) associate pt ctxt (m, stac) (*of*);
307 Accept_Tac1 (ist |> set_subst_true (a', v'), ctxt, m) (*return value*);
308 "~~~~~ from scan_dn1 to scan_to_tactic1 return val:"; val (xxxxx_xx)
309 = (Accept_Tac1 (ist |> set_subst_true (a', v'), ctxt, m));
311 "~~~~~ from scan_to_tactic1 to fun locate_input_tactic return val:"; val Accept_Tac1 ((ist as {assoc, ...}), ctxt, tac')
312 = (Accept_Tac1 (ist |> set_subst_true (a', v'), ctxt, m));
313 (*if*) LibraryC.assoc (*then*);
315 Safe_Step (Istate.Pstate ist, ctxt, tac') (*return value*);
316 "~~~~~ from locate_input_tactic to fun Step_Solve.by_tactic return:"; val Safe_Step (istate, ctxt, tac)
317 = (*xxxxx_xx*)(**)Safe_Step (Istate.Pstate ist, ctxt, tac')(**);
319 (*+*)val (pt, po as (p, p_)) = (pt'''''_', (p'''''_', p_'''''_')); (* from begin of by_tactic *)
320 val (p'', _, _,pt') =
321 Step.add tac (istate, ctxt) (pt, (lev_on p, Pbl));
324 ("ok", ([(Tactic.input_from_T tac, tac, (p'', (istate, ctxt)))],
325 [(*ctree NOT cut*)], (pt', p''))) (*return value*);
326 "~~~~~ from Step_Solve.by_tactic \<longrightarrow> Step.by_tactic return:"; val ((msg, cs' : Calc.state_post))
327 = ("ok", ([(Tactic.input_from_T tac, tac, (p'', (istate, ctxt)) )],
328 [(*ctree NOT cut*)], (pt', p'')));
330 "~~~~~ from Step.by_tactic to me return:"; val (("ok", (_, _, (pt, p)))) = (*** )xxxx( ***) ("ok", cs');
332 (case Step.do_next p ((pt, Pos.e_pos'), []) of
333 ("ok", (ts as (_, _, _) :: _, _, _)) => ("", ts)
334 | ("helpless", _) => ("helpless: cannot propose tac", [])
335 | ("no-fmz-spec", _) => error "no-fmz-spec"
336 | ("end-of-calculation", (ts, _, _)) => ("", ts)
337 | _ => error "me: uncovered case")
338 handle ERROR msg => raise ERROR msg
341 tacis as (_::_) => let val (tac, _, _) = last_elem tacis in tac end
342 | _ => if p = ([], Pos.Res) then Tactic.End_Proof' else Tactic.Empty_Tac;
344 (p, [] : NEW, TESTg_form (pt, p), (Tactic.tac2IDstr tac, tac), Celem.Sundef, pt);
345 "~~~~~ from me to TOOPLEVEL return:"; val (p,_,f,nxt,_,pt)
346 = (*** )xxx( ***) (p, [] : NEW, TESTg_form (pt, p), (Tactic.tac2IDstr tac, tac), Celem.Sundef, pt);
348 (*//--------------------- check results from modified me ----------------------------------\\*)
349 if p = ([2], Res) andalso
350 pr_ctree pr_short pt = ". ----- pblobj -----\n1. x + 1 = 2\n2. x + 1 = 2\n"
352 (case nxt of ("Rewrite_Set", Rewrite_Set "Test_simplify") => ()
354 else error "check results from modified me CHANGED";
355 (*\\--------------------- check results from modified me ----------------------------------//*)
357 "~~~~~ from me to TOPLEVEL return:"; val (p,_,f,nxt,_,pt) = (*** )xxx( ***) (**)(p, 000, f, nxt, 000, pt)(**);
358 (*\\------------------ end step into --------------------------------------------------------//*)
360 (*[3], Res*)val (p,_,f,nxt,_,pt) = me nxt'''''_''' p'''''_''' [] pt'''''_'''; (*nxt = Subproblem ("Test", ["LINEAR", "univariate", "equation", "test"])*)
361 (*[3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Model_Problem*)
362 (*[3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Add_Given "equality (- 1 + x = 0)"*)
363 (*[3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Add_Given "solveFor x"*)
364 (*[3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Add_Find "solutions x_i"*)
365 (*[3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Specify_Theory "Test"*)
366 (*[3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Specify_Problem ["LINEAR", "univariate", "equation", "test"]*)
367 (*[3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Specify_Method ["Test", "solve_linear"]*)
368 (*[3], Met*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Apply_Method ["Test", "solve_linear"]*)
369 (*[3, 1], Frm*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Rewrite_Set_Inst (["(''bdv'', x)"], "isolate_bdv")*)
370 (*[3, 1], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Rewrite_Set "Test_simplify"*)
371 (*[3, 2], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Check_Postcond ["LINEAR", "univariate", "equation", "test"]*)
372 (*[3], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Check_elementwise "Assumptions"*)
373 (*[4], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Check_Postcond ["sqroot-test", "univariate", "equation", "test"]*)
374 (*[], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = End_Proof'*)
376 (*/--------------------- final test ----------------------------------\\*)
377 if p = ([], Res) andalso f2str f = "[x = 1]" andalso pr_ctree pr_short pt =
378 ". ----- pblobj -----\n" ^
380 "2. x + 1 + - 1 * 2 = 0\n" ^
381 "3. ----- pblobj -----\n" ^
382 "3.1. - 1 + x = 0\n" ^
383 "3.2. x = 0 + - 1 * - 1\n" ^
385 then case nxt of End_Proof' => () | _ => error "re-build: fun locate_input_tactic changed 1"
386 else error "re-build: fun locate_input_tactic changed 2";
389 "----------- fun locate_input_tactic Helpless, NOT applicable ----------------------------------";
390 "----------- fun locate_input_tactic Helpless, NOT applicable ----------------------------------";
391 "----------- fun locate_input_tactic Helpless, NOT applicable ----------------------------------";
392 (*cp from -- try fun applyTactics ------- *)
393 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(["Term (5*e + 6*f - 8*g - 9 - 7*e - 4*f + 10*g + 12)",
395 ("PolyMinus",["plus_minus", "polynom", "vereinfachen"],
396 ["simplification", "for_polynomials", "with_minus"]))];
397 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
398 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
399 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
400 (*[1], Frm*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Rewrite_Set "ordne_alphabetisch"*)
402 (*+*)val Test_Out.FormKF "5 * e + 6 * f - 8 * g - 9 - 7 * e - 4 * f + 10 * g + 12" = f
404 (*[1], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Rewrite_Set "fasse_zusammen"*)
406 (*+*)if map Tactic.input_to_string (specific_from_prog pt p) =
407 ["Rewrite (\"subtrahiere_x_plus_minus\", \"\<lbrakk>?l is_num; ?m is_num\<rbrakk>\n\<Longrightarrow> ?x + ?m * ?v - ?l * ?v = ?x + (?m - ?l) * ?v\")",
408 "Rewrite (\"subtrahiere_x_minus_plus\", \"\<lbrakk>?l is_num; ?m is_num\<rbrakk>\n\<Longrightarrow> ?x - ?m * ?v + ?l * ?v = ?x + (- ?m + ?l) * ?v\")",
409 (*this is new since ThmC.numerals_to_Free.-----\\*)
411 then () else error "specific_from_prog ([1], Res) 1 CHANGED";
412 (*[2], Res*)val ("ok", (_, _, ptp as (pt, p))) = Step.by_tactic (hd (specific_from_prog pt p)) (pt, p);
414 (*+*)if map Tactic.input_to_string (specific_from_prog pt p) = [
415 "Rewrite (\"tausche_minus\", \"\<lbrakk>?b ist_monom; ?a kleiner ?b\<rbrakk>\n\<Longrightarrow> ?b - ?a = - ?a + ?b\")",
416 "Rewrite (\"subtrahiere_x_plus_minus\", \"\<lbrakk>?l is_num; ?m is_num\<rbrakk>\n\<Longrightarrow> ?x + ?m * ?v - ?l * ?v = ?x + (?m - ?l) * ?v\")",
417 "Rewrite (\"subtrahiere_x_minus_plus\", \"\<lbrakk>?l is_num; ?m is_num\<rbrakk>\n\<Longrightarrow> ?x - ?m * ?v + ?l * ?v = ?x + (- ?m + ?l) * ?v\")",
418 (*this is new since ThmC.numerals_to_Free.-----\\*)
420 (*this is new since ThmC.numerals_to_Free.-----//*)
422 then () else error "specific_from_prog ([1], Res) 2 CHANGED";
423 (* = ([3], Res)*)val ("ok", (_, _, ptp as (pt, p))) = Step.by_tactic (hd (specific_from_prog pt p)) (pt, p);
425 (*//----------------- exception PTREE "get_obj f EmptyPtree" raised --------------------------\\*)
426 (**)val ("ok", ([(Rewrite ("tausche_minus", _), _, _)], _, _)) = (*isa*)
427 Step.by_tactic (hd (specific_from_prog pt p)) (pt, p);
428 "~~~~~ fun by_tactic , args:"; val (tac, (ptp as (pt, p))) = (hd (specific_from_prog pt p), (pt, p));
429 val Applicable.Yes m = (*case*) Solve_Step.check tac (pt, p) (*of*);
430 (*if*) Tactic.for_specify' m; (*false*)
432 (**) val ("ok", ([(Rewrite ("tausche_minus", _), _, _)], _, _)) = (*isa*)
433 Step_Solve.by_tactic m (pt, p);
434 "~~~~~ fun by_tactic , args:"; val (m, (pt, po as (p, p_))) = (m, (pt, p));
435 (*if*) MethodC.id_empty = get_obj g_metID pt (par_pblobj pt p) (*else*);
436 val thy' = get_obj g_domID pt (par_pblobj pt p);
437 val (is, sc) = LItool.resume_prog thy' (p,p_) pt;
439 (*case*) locate_input_tactic sc (pt, po) (fst is) (snd is) m (*of*);
440 "~~~~~ fun locate_input_tactic , args:"; val ((Rule.Prog prog), (cstate as (pt, (*?*)pos(*?*))), istate, ctxt, tac)
441 = (sc, (pt, po), (fst is), (snd is), m);
442 val srls = LItool.get_simplifier cstate (*TODO: shift into Istate.T*);
444 (*case*) scan_to_tactic1 (prog, (cstate, ctxt, tac)) istate (*of*);
445 "~~~~~ fun scan_to_tactic1 , args:"; val ((prog, (cctt as ((_, p), _, _))), (Istate.Pstate (ist as {path, ...})))
446 = ((prog, (cstate, ctxt, tac)), istate);
447 (*if*) path = [] orelse ((last_elem o fst) p = 0 andalso snd p = Res) (*else*);
449 go_scan_up1 (prog, cctt) ist;
450 "~~~~~ fun go_scan_up1 , args:"; val ((pcct as (prog, _)), (ist as {path, ...}))
451 = ((prog, cctt), ist);
452 (*if*) 1 < length path (*then*);
455 scan_up1 pcct (ist |> path_up) (TermC.sub_at (path_up' path) prog);
456 "~~~~~ and scan_up1 , args:"; val (pcct, ist, (Const (\<^const_name>\<open>Try\<close>(*2*), _) $ _))
457 = (pcct, (ist |> path_up), (TermC.sub_at (path_up' path) prog));
459 go_scan_up1 pcct ist;
460 "~~~~~ and go_scan_up1 , args:"; val ((pcct as (prog, _)), (ist as {path, ...}))
462 (*if*) 1 < length path (*then*);
464 scan_up1 pcct (ist |> path_up) (TermC.sub_at (path_up' path) prog);
465 "~~~~~ and scan_up1 , args:"; val ((pcct as (prog, cct as (cstate, _, _))), ist,
466 (Const (\<^const_name>\<open>Chain\<close>(*3*), _) $ _ ))
467 = (pcct, (ist |> path_up), (TermC.sub_at (path_up' path) prog));
468 val e2 = check_Seq_up ist prog
470 (*case*) scan_dn1 cct (ist |> path_up_down [R] |> set_or ORundef) e2 (*of*);
471 "~~~~~ fun scan_dn1 , args:"; val (yyy, ist, (Const (\<^const_name>\<open>Chain\<close>(*2*), _) $ e1 $ e2))
472 = (cct, (ist |> path_up_down [R] |> set_or ORundef), e2);
474 (*case*) scan_dn1 cct (ist |> path_down [L, R]) e1 (*of*);
475 "~~~~~ fun scan_dn1 , args:"; val (xxx, ist, (Const (\<^const_name>\<open>Try\<close>(*2*), _) $ e))
476 = (cct, (ist |> path_down [L, R]), e1);
478 (*case*) scan_dn1 cct (ist |> path_down [R]) e (*of*);
479 (*======= end of scanning tacticals, a leaf =======*)
480 "~~~~~ fun scan_dn1 , args:"; val ((cct as (_, ctxt, _)), (ist as {eval, ...}), t)
481 = (cct, (ist |> path_down [R]), e);
482 (*if*) Tactical.contained_in t (*else*);
483 val (Program.Tac prog_tac, form_arg) = (*case*)
484 LItool.check_leaf "locate" ctxt eval (get_subst ist) t (*of*);
486 check_tac1 cct ist (prog_tac, form_arg);
487 "~~~~~ fun check_tac1 , args:"; val (((pt, p), ctxt, tac), (ist as {act_arg, or, ...}), (prog_tac, form_arg)) =
488 (cct, ist, (prog_tac, form_arg));
489 val LItool.Not_Associated = (*case*)
490 LItool.associate pt ctxt (tac, prog_tac) (*of*);
491 val _(*ORundef*) = (*case*) or (*of*);
493 (*+*)Solve_Step.check (LItool.tac_from_prog pt (ThyC.get_theory "Isac_Knowledge") prog_tac) (pt, p);
495 val Applicable.Yes m' =
496 (*case*) Solve_Step.check (LItool.tac_from_prog pt (ThyC.get_theory "Isac_Knowledge") prog_tac) (pt, p) (*of*);
498 Reject_Tac1 (ist |> set_subst_false (form_arg, Tactic.result m'), ctxt, tac)
499 (*return from check_tac1*);
500 "~~~~~ from fun check_tac1 \<longrightarrow>fun scan_dn1 \<longrightarrow>fun scan_dn1 \<longrightarrow>fun locate_input_tactic , return:"; val (Reject_Tac1 _) =
501 (Reject_Tac1 (ist |> set_subst_false (form_arg, Tactic.result m'), ctxt, tac));
503 val Test_Out.FormKF "- 9 + 12 + 5 * e - 7 * e + 6 * f - 4 * f - 8 * g + 10 * g" = f;
507 "----------- re-build: fun find_next_step, mini ------------------------------------------------";
508 "----------- re-build: fun find_next_step, mini ------------------------------------------------";
509 "----------- re-build: fun find_next_step, mini ------------------------------------------------";
510 val fmz = ["Term (a + a ::real)", "normalform n_n"];
511 val (dI',pI',mI') = ("Poly",["polynomial", "simplification"],["simplification", "for_polynomials"]);
512 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
513 (*[], Pbl*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, Pos.e_pos'), []);(*Model_Problem*)
514 (*[], Pbl*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, Pos.e_pos'), []);(*Specify_Theory "Poly"*)
515 (*[], Pbl*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, Pos.e_pos'), []);(*Specify_Problem ["polynomial", "simplification"]*)
516 (*[], Met*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []);(*Specify_Method ["simplification", "for_polynomials"]*)
517 (*1], Frm*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []);(*Apply_Method ["simplification", "for_polynomials"]*)
518 (*[1], Res*)val (_, ([(tac'''''_', _, _)], _, (pt'''''_', p'''''_'))) =
520 Step.do_next p ((pt, e_pos'), []);(*Rewrite_Set "norm_Poly"*)
521 (*//------------------ go into 1 ------------------------------------------------------------\\*)
522 "~~~~~ fun do_next , args:"; val ((ip as (_, p_)), (ptp as (pt, p), tacis))
523 = (p, ((pt, e_pos'), []));
524 val pIopt = Ctree.get_pblID (pt, ip);
525 (*if*) ip = ([], Res) (*else*);
526 val _ = (*case*) tacis (*of*);
527 val SOME _ = (*case*) pIopt (*of*);
528 (*if*) member op = [Pos.Pbl, Pos.Met] p_ (*else*);
530 val ("ok", ([(Rewrite_Set "norm_Poly", _, _)], _, (_, ([1], Res)))) =
531 Step_Solve.do_next (pt, ip);
532 "~~~~~ and do_next , args:"; val (ptp as (pt, pos as (p, p_))) = (pt, ip);
533 (*if*) MethodC.id_empty = get_obj g_metID pt (par_pblobj pt p) (*else*);
534 val thy' = get_obj g_domID pt (par_pblobj pt p);
535 val ((ist, ctxt), sc) = LItool.resume_prog thy' (p,p_) pt;
537 val Next_Step (_, _, Rewrite_Set' ("Poly", _, Rule_Set.Sequence {id = "norm_Poly", ...}, _, _)) =
538 LI.find_next_step sc (pt, pos) ist ctxt (*of*);
539 "~~~~~ fun find_next_step , args:"; val ((Rule.Prog prog), (ptp as(pt, (p, _))), (Pstate ist), ctxt)
540 = (sc, (pt, pos), ist, ctxt);
542 val Accept_Tac (Rewrite_Set' ("Poly", _, Rule_Set.Sequence {id = "norm_Poly", ...}, _, _), _, _) =
543 (*case*) scan_to_tactic (prog, (ptp, ctxt)) (Pstate ist) (*of*);
544 "~~~~~ fun scan_to_tactic , args:"; val ((prog, cc), (Pstate (ist as {path, ...})))
545 = ((prog, (ptp, ctxt)), (Pstate ist));
546 (*if*) path = [] (*then*);
548 val Accept_Tac (Rewrite_Set' ("Poly", _, Rule_Set.Sequence {id = "norm_Poly", ...}, _, _), _, _) =
549 scan_dn cc (trans_scan_dn ist) (Program.body_of prog);
550 "~~~~~ fun scan_dn , args:"; val ((cc as (_, ctxt)), (ist as {eval, ...}), t)
551 = (cc, (trans_scan_dn ist), (Program.body_of prog));
552 (*if*) Tactical.contained_in t (*else*);
553 val (Program.Tac prog_tac, form_arg) = (*case*) LItool.check_leaf "next " ctxt eval (get_subst ist) t (*of*);
555 val Accept_Tac (Rewrite_Set' ("Poly", _, Rule_Set.Sequence {id = "norm_Poly", ...}, _, _), _, _) =
556 check_tac cc ist (prog_tac, form_arg) (*return from xxx*);
557 "~~~~~ from fun scan_dn\<longrightarrow>fun scan_to_tactic\<longrightarrow>fun find_next_step, return:"; val (Accept_Tac (tac, ist, ctxt))
558 = (check_tac cc ist (prog_tac, form_arg));
560 Next_Step (Pstate ist, Tactic.insert_assumptions tac ctxt, tac) (*return from find_next_step*);
561 "~~~~~ from fun find_next_step\<longrightarrow>and do_next\<longrightarrow>fun zzz, return:"; val (Next_Step (ist, ctxt, tac))
562 = (Next_Step (Pstate ist, Tactic.insert_assumptions tac ctxt, tac));
564 LI.by_tactic tac (ist, Tactic.insert_assumptions tac ctxt) ptp (*return from and do_next*);
565 "~~~~~ from and do_next\<longrightarrow>fun do_next\<longrightarrow>toplevel, return:"; val (_, ([(tac''''', _, _)], _, (pt''''', p''''')))
566 = (LI.by_tactic tac (ist, Tactic.insert_assumptions tac ctxt) ptp);
567 (*\\------------------ end of go into 1 -----------------------------------------------------//*)
569 (*[], Res*)val (_, ([(tac''''', _, _)], _, (pt''''', p'''''))) =
571 Step.do_next p'''''_' ((pt'''''_', Pos.e_pos'), []);(* Check_Postcond ["polynomial", "simplification"]*)
572 (*//------------------ go into 2 ------------------------------------------------------------\\*)
573 "~~~~~ fun do_next , args:"; val ((ip as (_, p_)), (ptp as (pt, p), tacis))
574 = (p''''', ((pt''''', e_pos'), []));
575 val pIopt = Ctree.get_pblID (pt, ip);
576 (*if*) ip = ([], Res) (*else*);
577 val _ = (*case*) tacis (*of*);
578 val SOME _ = (*case*) pIopt (*of*);
579 (*if*) member op = [Pos.Pbl, Pos.Met] p_ (*else*);
581 val ("ok", ([(Check_Postcond ["polynomial", "simplification"], _, _)], _, (_, ([], Res)))) =
582 Step_Solve.do_next (pt, ip);
583 "~~~~~ and do_next , args:"; val (ptp as (pt, pos as (p, p_))) = (pt, ip);
584 (*if*) MethodC.id_empty = get_obj g_metID pt (par_pblobj pt p) (*else*);
585 val thy' = get_obj g_domID pt (par_pblobj pt p);
586 val ((ist, ctxt), sc) = LItool.resume_prog thy' (p,p_) pt;
588 (** )val End_Program (ist, tac) =
589 ( *case*) LI.find_next_step sc (pt, pos) ist ctxt (*of*);
590 "~~~~~ fun find_next_step , args:"; val ((Rule.Prog prog), (ptp as(pt, (p, _))), (Pstate ist), ctxt)
591 = (sc, (pt, pos), ist, ctxt);
593 (* val Term_Val (Const (\<^const_name>\<open>times\<close>, _) $ Free ("2", _) $ Free ("a", _))*)
594 (** )val Term_Val prog_result =
595 ( *case*) scan_to_tactic (prog, (ptp, ctxt)) (Pstate ist) (*of*);
596 "~~~~~ fun scan_to_tactic , args:"; val ((prog, cc), (Pstate (ist as {path, ...})))
597 = ((prog, (ptp, ctxt)), (Pstate ist));
598 (*if*) path = [] (*else*);
600 go_scan_up (prog, cc) (trans_scan_up ist |> set_found);
601 "~~~~~ fun go_scan_up , args:"; val ((pcc as (sc, _)), (ist as {path, act_arg, found_accept, ...}))
602 = ((prog, cc), (trans_scan_up ist(*|> set_found !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!! *)));
603 (*if*) path = [R] (*then*);
604 (*if*) found_accept = true (*then*);
606 Term_Val act_arg (*return from go_scan_up*);
607 "~~~~~ from fun go_scan_up\<longrightarrow>fun scan_to_tactic, return:"; val (Term_Val prog_result) = (Term_Val act_arg);
609 Term_Val prog_result (*return from scan_to_tactic*);
610 "~~~~~ from fun scan_to_tactic\<longrightarrow>fun find_next_step, return:"; val (Term_Val prog_result) = (Term_Val prog_result);
611 val (true, p', _) = (*case*) parent_node pt p (*of*);
612 val (_, pblID, _) = get_obj g_spec pt p';
614 End_Program (Pstate ist, Tactic.Check_Postcond' (pblID, prog_result))
615 (*return from find_next_step*);
616 "~~~~~ from fun find_next_step\<longrightarrow>and do_next\<longrightarrow>fun zzz, return:"; val (End_Program (ist, tac))
617 = (End_Program (Pstate ist, Tactic.Check_Postcond' (pblID,prog_result)));
618 val _ = (*case*) tac (*of*);
620 val ("ok", ([(Check_Postcond ["polynomial", "simplification"], _, _)], _, (_, ([], Res))))
621 = LI.by_tactic tac (ist, ctxt) ptp (*return from and do_next*);
622 "~~~~~ from and do_next\<longrightarrow>top level, return:"; val (_, ([(tac''''', _, _)], _, (pt''''', p''''')))
623 = (LI.by_tactic tac (ist, ctxt) ptp);
624 (*\\------------------ end of go into 2 -----------------------------------------------------//*)
626 (*[], Und*)val (msg, ([], _, (pt, p))) = Step.do_next p''''' ((pt''''', Pos.e_pos'), []);(**)
628 Test_Tool.show_pt_tac pt; (*[
629 ([], Frm), Simplify (a + a)
630 . . . . . . . . . . Apply_Method ["simplification", "for_polynomials"],
632 . . . . . . . . . . Rewrite_Set "norm_Poly",
634 . . . . . . . . . . Check_Postcond ["polynomial", "simplification"],
637 (*/--- final test ---------------------------------------------------------------------------\\*)
638 val (res, asm) = (get_obj g_result pt (fst p));
640 if UnparseC.term res = "2 * a" andalso map UnparseC.term asm = []
641 andalso p = ([], Und) andalso msg = "end-of-calculation"
642 andalso pr_ctree pr_short pt = ". ----- pblobj -----\n1. a + a\n"
644 case tac''''' of Check_Postcond ["polynomial", "simplification"] => ()
645 | _ => error "re-build: fun find_next_step, mini 1"
646 else error "re-build: fun find_next_step, mini 2"
650 "----------- re-build: fun locate_input_term ---------------------------------------------------";
651 "----------- re-build: fun locate_input_term ---------------------------------------------------";
652 "----------- re-build: fun locate_input_term ---------------------------------------------------";
654 ----------- appendFormula: on Res + late deriv ------------------------------------------------*)
655 val fmz = ["equality (x+1=(2::real))", "solveFor x", "solutions L"];
656 val (dI',pI',mI') = ("Test", ["sqroot-test", "univariate", "equation", "test"],
657 ["Test", "squ-equ-test-subpbl1"]);
658 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
659 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
660 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
661 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
662 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
663 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
664 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
666 (*[], Met*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*Apply_Method ["Test", "squ-equ-test-subpbl1"]*);
668 (*[1], Frm*)val (p,_,f,nxt,_,pt) = me nxt p [] pt;(*Rewrite_Set "norm_equation"*)
669 (*+*)if f2str f = "x + 1 = 2" then () else error "locate_input_term at ([1], Frm) CHANGED";
671 (*[1], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt;(*Rewrite_Set "Test_simplify"*)
672 (*+*)if f2str f = "x + 1 + - 1 * 2 = 0" then () else error "locate_input_term at ([1], Frm) CHANGED";
674 Test_Tool.show_pt_tac pt; (*[
675 ([], Frm), solve (x + 1 = 2, x)
676 . . . . . . . . . . Apply_Method ["Test", "squ-equ-test-subpbl1"],
677 ([1], Frm), x + 1 = 2
678 . . . . . . . . . . Rewrite_Set "norm_equation",
679 ([1], Res), x + 1 + - 1 * 2 = 0 ///Check_Postcond..ERROR*)
681 (*//---------- appendFormula 1 "x = 1" \<longrightarrow> Step_Solve.inform \<longrightarrow> LI.locate_input_term ----------\\*)
682 "~~~~~ fun appendFormula , args:"; val ((*cI, *) ifo: TermC.as_string) = ((**) "x = 1");
683 val cs = (*get_calc cI*) ((pt, p), [(*nxt, nxt_, (pos, (ist, ctxt))*)])
684 val pos = (*get_pos cI 1*) p
687 (*+*)val ptp''''' = (pt, p);
688 (*+*)if snd ptp''''' = ([1], Res) then () else error "old_cs changed";
689 (*+*)Test_Tool.show_pt_tac pt; (*[
690 (*+*)([], Frm), solve (x + 1 = 2, x)
691 (*+*). . . . . . . . . . Apply_Method ["Test", "squ-equ-test-subpbl1"],
692 (*+*)([1], Frm), x + 1 = 2
693 (*+*). . . . . . . . . . Rewrite_Set "norm_equation",
694 (*+*)([1], Res), x + 1 + - 1 * 2 = 0 ///Check_Postcond*)
696 val ("ok", cs' as (_, _, ptp')) =
697 (*case*) Step.do_next pos cs (*of*);
702 Proof_Context.theory_of (Ctree.get_ctxt pt p) (*= Isac.Test*)
706 (*+*)Step_Solve.by_term ptp' (encode ifo)
708 Failed to parse term*)
710 val ("ok", (_(*use in DG !!!*), [], ptp''''' as (pt''''', p'''''))) = (*case*)
711 Step_Solve.by_term ptp' (encode ifo) (*of*);
712 "~~~~~ fun Step_Solve.by_term , args:"; val ((pt, pos as (p, _)), istr)
713 = (ptp', (encode ifo));
716 (*case*) TermC.parseNEW (get_ctxt pt pos) istr (*of*);
717 val pos_pred = lev_back(*'*) pos
718 val f_pred = Ctree.get_curr_formula (pt, pos_pred);
719 val f_succ = Ctree.get_curr_formula (pt, pos);
720 (*if*) f_succ = f_in (*else*);
722 (*case*) CAS_Cmd.input f_in (*of*);
724 (*old* ) val (_, _, metID) = get_obj g_spec pt (par_pblobj pt p)
725 (*old*) val {scr = prog, ...} = MethodC.from_store metID
726 (*old*) val istate = get_istate_LI pt pos
727 (*old*) val ctxt = get_ctxt pt pos
728 val LI.Found_Step (cstate'''''_', _(*istate*), _(*ctxt*)) = (*case*)
729 LI.locate_input_term prog (pt, pos) istate ctxt f_in (*of*);
730 "~~~~~ fun locate_input_term , args:"; val ((Rule.Prog _), ((pt, pos) : Calc.T), (_ : Istate.T), (_ : Proof.context), tm)
731 = (prog, (pt, pos), istate, ctxt, f_in);
735 (*NEW*) LI.locate_input_term (pt, pos) f_in (*of*);
736 "~~~~~ fun locate_input_term , args:"; val ((pt, pos), tm) = ((pt, pos), f_in);
737 val pos_pred = Pos.lev_back' pos (*f_pred ---"step pos cs"---> f_succ in appendFormula*)
739 val ("ok", (_, _, cstate as (pt', pos'))) =
740 (*case*) compare_step ([], [], (pt, pos_pred)) tm (*of*);
743 Found_Step (cstate, get_istate_LI pt' pos', get_ctxt pt' pos') (*return from locate_input_term*);
745 (*NEW*) Found_Step cstate (*return from locate_input_term*);
746 (*LI.Found_Step ( *)cstate(*, _(*istate*), _(*ctxt*))( *return from locate_input_term*);
747 "~~~~~ from fun locate_input_term\<longrightarrow>fun Step_Solve.by_term, return:"; val ("ok", (_(*use in DG !!!*), c, ptp as (_, p)))
748 = (("ok" , ([], [], cstate (* already contains istate, ctxt *))));
750 ("ok", ((*_ use in DG !!!,*) c, ptp(* as (_*), p))(*)*)(*return from Step_Solve.by_term*);
751 "~~~~~ from fun Step_Solve.by_term\<longrightarrow>(fun appendFormula)!toplevel, return:"; val ("ok", (_(*use in DG !!!*), [], ptp''''' as (pt''''', p''''')))
752 = ("ok", ([], [], ptp));
754 (*fun me requires nxt...*)
755 Step.do_next p''''' (ptp''''', []);
756 val ("ok", ([(nxt'''''_' as Check_Postcond ["LINEAR", "univariate", "equation", "test"], _, _)], _,
757 (pt'''''_', p'''''_'))) = Step.do_next p''''' (ptp''''', [])
758 (*\\---------- appendFormula 1 "x = 1" \<longrightarrow> Step_Solve.inform \<longrightarrow> LI.locate_input_term ----------//*)
760 (*//----- REPLACED BY appendFormula 1 "x = 1" \<longrightarrow> Step_Solve.inform \<longrightarrow> LI.locate_input_term -----\\* )
761 (*[2], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Subproblem ("Test", ["LINEAR", "univariate", "equation", "test"])*)
762 (*[3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Model_Problem*)
763 (*[3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Add_Given "equality (- 1 + x = 0)"*)
764 (*[3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Add_Given "solveFor x"*)
765 (*[3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Add_Find "solutions x_i"*)
766 (*[3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Specify_Theory "Test"*)
767 (*[3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Specify_Problem ["LINEAR", "univariate", "equation", "test"]*)
768 (*[3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Specify_Method ["Test", "solve_linear"]*)
769 (*[3], Met*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Apply_Method ["Test", "solve_linear"]*)
770 (*[3, 1], Frm*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Rewrite_Set_Inst (["(''bdv'', x)"], "isolate_bdv")*)
771 (*[3, 1], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Rewrite_Set "Test_simplify"*)
772 (*[3, 2], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Check_Postcond ["LINEAR", "univariate", "equation", "test"]*)
773 ( *\\----- REPLACED BY appendFormula 1 "x = 1" \<longrightarrow> Step_Solve.inform \<longrightarrow> LI.locate_input_term -----//*)
775 (*[3], Res*)val (p,_,f,nxt,_,pt) = me nxt'''''_' p'''''_' [] pt'''''_'; (*nxt = Check_elementwise "Assumptions"*)
776 (*[4], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Check_Postcond ["sqroot-test", "univariate", "equation", "test"]*)
777 (*[], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = End_Proof'*)
780 (*/--- final test ---------------------------------------------------------------------------\\*)
781 if p = ([], Res) andalso f2str f = "[x = 1]" andalso pr_ctree pr_short pt =
782 ". ----- pblobj -----\n" ^
784 "2. x + 1 + - 1 * 2 = 0\n" ^
785 "3. ----- pblobj -----\n" ^
786 "3.1. - 1 + x = 0\n" ^
787 "3.2. x = 0 + - 1 * - 1\n" ^
788 "3.2.1. x = 0 + - 1 * - 1\n" ^
789 "3.2.2. x = 0 + 1\n" (*ATTENTION: see complete Calc below*)
790 then case nxt of End_Proof' => () | _ => error "re-build: fun locate_input_term CHANGED 1"
791 else error "re-build: fun locate_input_term CHANGED 2";
793 Test_Tool.show_pt_tac pt; (*[
794 ([], Frm), solve (x + 1 = 2, x)
795 . . . . . . . . . . Apply_Method ["Test", "squ-equ-test-subpbl1"],
796 ([1], Frm), x + 1 = 2
797 . . . . . . . . . . Rewrite_Set "norm_equation",
798 ([1], Res), x + 1 + - 1 * 2 = 0
799 . . . . . . . . . . Rewrite_Set "Test_simplify",
800 ([2], Res), - 1 + x = 0
801 . . . . . . . . . . Subproblem (Test, ["LINEAR", "univariate", "equation", "test"]),
802 ([3], Pbl), solve (- 1 + x = 0, x)
803 . . . . . . . . . . Apply_Method ["Test", "solve_linear"],
804 ([3,1], Frm), - 1 + x = 0
805 . . . . . . . . . . Rewrite_Set_Inst ([(''bdv'', x)], "isolate_bdv"),
806 ([3,1], Res), x = 0 + - 1 * - 1
807 . . . . . . . . . . Derive Test_simplify,
808 ([3,2,1], Frm), x = 0 + - 1 * - 1
809 . . . . . . . . . . Rewrite ("#: - 1 * - 1 = 1", "- 1 * - 1 = 1"),
810 ([3,2,1], Res), x = 0 + 1
811 . . . . . . . . . . Rewrite ("radd_0", "0 + ?k = ?k"),
812 ([3,2,2], Res), x = 1
813 . . . . . . . . . . Tactic.input_to_string not impl. for ?!,
815 . . . . . . . . . . Check_Postcond ["LINEAR", "univariate", "equation", "test"],
817 . . . . . . . . . . Check_Postcond ["sqroot-test", "univariate", "equation", "test"],
818 ([], Res), [x = 1]]*)
824 section \<open>===================================================================================\<close>
831 section \<open>code for copy & paste ===============================================================\<close>
833 "~~~~~ fun xxx , args:"; val () = ();
834 "~~~~~ and xxx , args:"; val () = ();
835 "~~~~~ from xxx to yyy return val:"; val ((*yyy*)) = ((*xxx*));
836 (*if*) (*then*); (*else*); (*case*) (*of*); (*return value*); (*in*) (*end*);