1 (* Title: "Interpret/lucas-interpreter.sml"
3 (c) due to copyright terms
6 "-----------------------------------------------------------------------------------------------";
7 "table of contents -----------------------------------------------------------------------------";
8 "-----------------------------------------------------------------------------------------------";
9 "----------- Take as 1st stac in program -------------------------------------------------------";
10 "----------- re-build: fun locate_input_tactic -------------------------------------------------";
11 "----------- fun locate_input_tactic Helpless, but applicable ----------------------------------";
12 "----------- re-build: fun find_next_step, mini ------------------------------------------------";
13 "----------- re-build: fun locate_input_term ---------------------------------------------------";
14 "-----------------------------------------------------------------------------------------------";
15 "-----------------------------------------------------------------------------------------------";
16 "-----------------------------------------------------------------------------------------------";
18 "----------- Take as 1st stac in program -------------------------------------------------------";
19 "----------- Take as 1st stac in program -------------------------------------------------------";
20 "----------- Take as 1st stac in program -------------------------------------------------------";
21 "compare --- Apply_Method with initial Take by Step.do_next --- in test/../step-solve ----------";
22 val p = e_pos'; val c = [];
23 val (p,_,f,nxt,_,pt) =
25 [(["functionTerm (x^^^2 + 1)", "integrateBy x", "antiDerivative FF"],
26 ("Integrate", ["integrate","function"], ["diff","integration"]))];
27 val (p,_,f,nxt,_,pt) = me nxt p c pt; (*nxt = ("Tac ", ...) --> Add_Given...*)
28 val (p,_,f,nxt,_,pt) = me nxt p c pt;
29 val (p,_,f,nxt,_,pt) = me nxt p c pt;
30 val (p,_,f,nxt,_,pt) = me nxt p c pt;
31 val (p,_,f,nxt,_,pt) = me nxt p c pt;
32 val (p,_,f,nxt,_,pt) = me nxt p c pt;
33 val (p,_,f,nxt,_,pt) = me nxt p c pt;
34 case nxt of (Apply_Method ["diff", "integration"]) => ()
35 | _ => error "integrate.sml -- me method [diff,integration] -- spec";
36 "----- step 8: returns nxt = Rewrite_Set_Inst ([\"(''bdv'', x)\"],\"integration\")";
38 "~~~~~ fun me, args:"; val (tac, (p:pos'), _, (pt:ctree)) = (nxt, p, c, pt);
39 "~~~~~ fun Step.by_tactic, args:"; val (tac, (ptp as (pt, p))) = (tac, (pt,p));
40 val Applicable.Yes m = Step.check tac (pt, p);
41 (*if*) Tactic.for_specify' m; (*false*)
42 "~~~~~ fun loc_solve_ , args:"; val (m, (pt,pos)) = (m, ptp);
44 "~~~~~ fun Step_Solve.by_tactic , args:"; val (m as Apply_Method' (mI, _, _, ctxt), (pt, (pos as (p,_))))
46 val {srls, ...} = Method.from_store mI;
47 val itms = case get_obj I pt p of
48 PblObj {meth=itms, ...} => itms
49 | _ => error "solve Apply_Method: uncovered case get_obj"
50 val thy' = get_obj g_domID pt p;
51 val thy = ThyC.get_theory thy';
52 val srls = LItool.get_simplifier (pt, pos)
53 val (is, env, ctxt, sc) = case LItool.init_pstate srls ctxt itms mI of
54 (is as Istate.Pstate {env, ...}, ctxt, sc) => (is, env, ctxt, sc)
55 | _ => error "solve Apply_Method: uncovered case init_pstate";
56 (*+*)pstate2str (the_pstate is) = "([\"\n(f_f, x ^^^ 2 + 1)\",\"\n(v_v, x)\"], [], empty, NONE, \n??.empty, ORundef, false, true)";
57 val ini = LItool.implicit_take sc env;
60 val NONE = (*case*) ini (*of*);
61 val Next_Step (is', ctxt', m') =
62 LI.find_next_step sc (pt, (p, Res)) is ctxt;
63 (*+*)pstate2str (the_pstate is') = "([\"\n(f_f, x ^^^ 2 + 1)\",\"\n(v_v, x)\"], [R,L,R], empty, NONE, \nIntegral x ^^^ 2 + 1 D x, ORundef, false, false)";
64 val Safe_Step (_, _, Take' _) = (*case*)
65 locate_input_tactic sc (pt, (p, Res)) is' ctxt' m' (*of*);
66 "~~~~~ fun locate_input_tactic , args:"; val ((Prog prog), cstate, istate, ctxt, tac)
67 = (sc, (pt, (p, Res)), is', ctxt', m');
69 (*case*) scan_to_tactic1 (prog, (cstate, ctxt, tac)) istate (*of*);
70 "~~~~~ fun scan_to_tactic1 , args:"; val ((prog, (cctt as ((_, p), _, _))), (Istate.Pstate (ist as {path, ...})))
71 = ((prog, (cstate, ctxt, tac)), istate);
72 (*if*) path = [] orelse ((last_elem o fst) p = 0 andalso snd p = Res) (*then*);
74 val Accept_Tac1 (_, _, Take' _) =
75 scan_dn1 cctt (ist |> set_path [R] |> set_or ORundef) (Program.body_of prog);
76 "~~~~~ fun scan_dn1 , args:"; val (xxx, ist, (Const ("HOL.Let", _) $ e $ (Abs (id, T, b))))
77 = (cctt, (ist |> set_path [R] |> set_or ORundef), (Program.body_of prog));
79 (*+*) if UnparseC.term e = "Take (Integral f_f D v_v)" then () else error "scan_dn1 Integral changed";
82 scan_dn1 xxx (ist |> path_down [L, R]) e (*of*);
83 (*======= end of scanning tacticals, a leaf =======*)
84 "~~~~~ fun scan_dn1 , args:"; val (((pt, p), ctxt, tac), (ist as {eval, or, ...}), t)
85 = (xxx, (ist |> path_down [L, R]), e);
86 val (Program.Tac stac, a') = check_leaf "locate" ctxt eval (get_subst ist) t;
90 "----------- re-build: fun locate_input_tactic -------------------------------------------------";
91 "----------- re-build: fun locate_input_tactic -------------------------------------------------";
92 "----------- re-build: fun locate_input_tactic -------------------------------------------------";
93 val fmz = ["equality (x+1=(2::real))", "solveFor x","solutions L"];
94 val (dI',pI',mI') = ("Test", ["sqroot-test","univariate","equation","test"],
95 ["Test","squ-equ-test-subpbl1"]);
96 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
97 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
98 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
99 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
100 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
101 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
102 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
103 (*[], Met*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = (_, Apply_Method ["Test", "squ-equ-test-subpbl1"])*);
104 (*[1], Frm*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = ("Rewrite_Set", Rewrite_Set "norm_equation")*)
106 (*//------------------ begin step into ------------------------------------------------------\\*)
107 (*[1], Res*)val (p'''''_''',_,f,nxt'''''_''',_,pt'''''_''') = me nxt p [] pt; (*nxt = Rewrite_Set "Test_simplify"*)
109 "~~~~~ fun me , args:"; val (tac, p, _(*NEW remove*), pt) = (nxt, p, [], pt);
111 (** )val (***)xxxx(***) ( *("ok", (_, _, (pt, p))) =( **) (*case*)
112 Step.by_tactic tac (pt,p) (*of*);
113 "~~~~~ fun by_tactic , args:"; val (tac, (ptp as (pt, p))) = (tac, (pt,p));
114 val Applicable.Yes m = (*case*) Solve_Step.check tac (pt, p) (*of*);
115 (*if*) Tactic.for_specify' m; (*false*)
117 (** )val (***)xxxxx_x(***) ( *(msg, cs') =( **)
118 Step_Solve.by_tactic m ptp;
119 "~~~~~ fun by_tactic , args:"; val (m, (pt, po as (p, p_))) = (m, ptp);
120 (*+*)val (pt'''''_', (p'''''_', p_'''''_')) = (pt, (p, p_));
121 (*if*) Method.id_empty = get_obj g_metID pt (par_pblobj pt p); (*else*)
122 val thy' = get_obj g_domID pt (par_pblobj pt p);
123 val (is, sc) = LItool.resume_prog thy' (p,p_) pt;
125 locate_input_tactic sc (pt, po) (fst is) (snd is) m;
126 "~~~~~ fun locate_input_tactic , args:"; val (Prog prog, cstate, istate, ctxt, tac)
127 = (sc, (pt, po), (fst is), (snd is), m);
128 val srls = get_simplifier cstate;
130 (** )val Accept_Tac1 ((is as (_,_,_,_,_,strong_ass), ctxt, ss as((tac', _, ctree, pos', _) :: _))) =( **)
131 (*case*) scan_to_tactic1 (prog, (cstate, ctxt, tac)) istate (*of*);
132 "~~~~~ fun scan_to_tactic1 , args:"; val ((prog, (cctt as ((_, p), _, _))), (Istate.Pstate (ist as {path, ...})))
133 = ((prog, (cstate, ctxt, tac)), istate);
134 (*if*) path = [] orelse ((last_elem o fst) p = 0 andalso snd p = Res) (*then*);
136 (** )val xxxxx_xx = ( **)
137 scan_dn1 cctt (ist |> set_path [R] |> set_or ORundef) (Program.body_of prog);
138 "~~~~~ fun scan_dn1 , args:"; val (xxx, ist, (Const ("HOL.Let", _) $ e $ (Abs (id, T, b))))
139 = (cctt, (ist |> set_path [R] |> set_or ORundef), (Program.body_of prog));
141 (*case*) scan_dn1 xxx (ist |> path_down [L, R]) e (*of*);
142 "~~~~~ fun scan_dn1 , args:"; val ((xxx as (cstate, _, _)), ist, (Const ("Tactical.Chain"(*1*), _) $ e1 $ e2 $ a))
143 = (xxx, (ist |> path_down [L, R]), e);
145 (*case*) scan_dn1 xxx (ist |> path_down_form ([L, L, R], a)) e1 (*of*);
146 "~~~~~ fun scan_dn1 , args:"; val (xxx, ist, (Const ("Tactical.Try"(*2*), _) $ e))
147 = (xxx, (ist |> path_down_form ([L, L, R], a)), e1);
149 (*case*) scan_dn1 xxx (ist |> path_down [R]) e (*of*);
150 (*======= end of scanning tacticals, a leaf =======*)
151 "~~~~~ fun scan_dn1 , args:"; val (((pt, p), ctxt, tac), (ist as {env, eval, or, ...}), t)
152 = (xxx, (ist |> path_down [R]), e);
153 val (Program.Tac stac, a') =
154 (*case*) check_leaf "locate" ctxt eval (get_subst ist) t (*of*);
155 val LItool.Associated (m, v', ctxt) =
156 (*case*) associate pt ctxt (m, stac) (*of*);
158 Accept_Tac1 (ist |> set_subst_true (a', v'), ctxt, m) (*return value*);
159 "~~~~~ from scan_dn1 to scan_to_tactic1 return val:"; val (xxxxx_xx)
160 = (Accept_Tac1 (ist |> set_subst_true (a', v'), ctxt, m));
162 "~~~~~ from scan_to_tactic1 to fun locate_input_tactic return val:"; val Accept_Tac1 ((ist as {assoc, ...}), ctxt, tac')
163 = (Accept_Tac1 (ist |> set_subst_true (a', v'), ctxt, m));
164 (*if*) LibraryC.assoc (*then*);
166 Safe_Step (Istate.Pstate ist, ctxt, tac') (*return value*);
167 "~~~~~ from locate_input_tactic to fun Step_Solve.by_tactic return:"; val Safe_Step (istate, ctxt, tac)
168 = (*xxxxx_xx*)(**)Safe_Step (Istate.Pstate ist, ctxt, tac')(**);
170 (*+*)val (pt, po as (p, p_)) = (pt'''''_', (p'''''_', p_'''''_')); (* from begin of by_tactic *)
171 val (p'', _, _,pt') =
172 Step.add tac (istate, ctxt) (pt, (lev_on p, Pbl));
175 ("ok", ([(Tactic.input_from_T tac, tac, (p'', (istate, ctxt)))],
176 [(*ctree NOT cut*)], (pt', p''))) (*return value*);
177 "~~~~~ from Step_Solve.by_tactic \<longrightarrow> Step.by_tactic return:"; val ((msg, cs' : Calc.state_post))
178 = ("ok", ([(Tactic.input_from_T tac, tac, (p'', (istate, ctxt)) )],
179 [(*ctree NOT cut*)], (pt', p'')));
181 "~~~~~ from Step.by_tactic to me return:"; val (("ok", (_, _, (pt, p)))) = (*** )xxxx( ***) ("ok", cs');
183 (case Step.do_next p ((pt, Pos.e_pos'), []) of
184 ("ok", (ts as (_, _, _) :: _, _, _)) => ("", ts)
185 | ("helpless", _) => ("helpless: cannot propose tac", [])
186 | ("no-fmz-spec", _) => error "no-fmz-spec"
187 | ("end-of-calculation", (ts, _, _)) => ("", ts)
188 | _ => error "me: uncovered case")
189 handle ERROR msg => raise ERROR msg
192 tacis as (_::_) => let val (tac, _, _) = last_elem tacis in tac end
193 | _ => if p = ([], Pos.Res) then Tactic.End_Proof' else Tactic.Empty_Tac;
195 (p, [] : NEW, TESTg_form (pt, p), (Tactic.tac2IDstr tac, tac), Celem.Sundef, pt);
196 "~~~~~ from me to TOOPLEVEL return:"; val (p,_,f,nxt,_,pt)
197 = (*** )xxx( ***) (p, [] : NEW, TESTg_form (pt, p), (Tactic.tac2IDstr tac, tac), Celem.Sundef, pt);
199 (*//--------------------- check results from modified me ----------------------------------\\*)
200 if p = ([2], Res) andalso
201 pr_ctree pr_short pt = ". ----- pblobj -----\n1. x + 1 = 2\n2. x + 1 = 2\n"
203 (case nxt of ("Rewrite_Set", Rewrite_Set "Test_simplify") => ()
205 else error "check results from modified me CHANGED";
206 (*\\--------------------- check results from modified me ----------------------------------//*)
208 "~~~~~ from me to TOPLEVEL return:"; val (p,_,f,nxt,_,pt) = (*** )xxx( ***) (**)(p, 000, f, nxt, 000, pt)(**);
209 (*\\------------------ end step into --------------------------------------------------------//*)
211 (*[3], Res*)val (p,_,f,nxt,_,pt) = me nxt'''''_''' p'''''_''' [] pt'''''_'''; (*nxt = Subproblem ("Test", ["LINEAR", "univariate", "equation", "test"])*)
212 (*[3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Model_Problem*)
213 (*[3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Add_Given "equality (-1 + x = 0)"*)
214 (*[3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Add_Given "solveFor x"*)
215 (*[3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Add_Find "solutions x_i"*)
216 (*[3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Specify_Theory "Test"*)
217 (*[3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Specify_Problem ["LINEAR", "univariate", "equation", "test"]*)
218 (*[3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Specify_Method ["Test", "solve_linear"]*)
219 (*[3], Met*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Apply_Method ["Test", "solve_linear"]*)
220 (*[3, 1], Frm*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Rewrite_Set_Inst (["(''bdv'', x)"], "isolate_bdv")*)
221 (*[3, 1], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Rewrite_Set "Test_simplify"*)
222 (*[3, 2], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Check_Postcond ["LINEAR", "univariate", "equation", "test"]*)
223 (*[3], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Check_elementwise "Assumptions"*)
224 (*[4], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Check_Postcond ["sqroot-test", "univariate", "equation", "test"]*)
225 (*[], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = End_Proof'*)
227 (*/--------------------- final test ----------------------------------\\*)
228 if p = ([], Res) andalso f2str f = "[x = 1]" andalso pr_ctree pr_short pt =
229 ". ----- pblobj -----\n" ^
231 "2. x + 1 + -1 * 2 = 0\n" ^
232 "3. ----- pblobj -----\n" ^
233 "3.1. -1 + x = 0\n" ^
234 "3.2. x = 0 + -1 * -1\n" ^
236 then case nxt of End_Proof' => () | _ => error "re-build: fun locate_input_tactic changed 1"
237 else error "re-build: fun locate_input_tactic changed 2";
240 "----------- fun locate_input_tactic Helpless, but applicable ----------------------------------";
241 "----------- fun locate_input_tactic Helpless, but applicable ----------------------------------";
242 "----------- fun locate_input_tactic Helpless, but applicable ----------------------------------";
243 (*cp from -- try fun applyTactics ------- *)
244 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(["Term (5*e + 6*f - 8*g - 9 - 7*e - 4*f + 10*g + 12)",
246 ("PolyMinus",["plus_minus","polynom","vereinfachen"],
247 ["simplification","for_polynomials","with_minus"]))];
248 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
249 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
250 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
251 (*[1], Frm*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Rewrite_Set "ordne_alphabetisch"*)
252 (*[1], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Rewrite_Set "fasse_zusammen"*)
254 (*+*)if map Tactic.input_to_string (specific_from_prog pt p) =
255 ["Rewrite (\"subtrahiere_x_plus_minus\", \"\<lbrakk>?l is_const; ?m is_const\<rbrakk>\n\<Longrightarrow> ?x + ?m * ?v - ?l * ?v = ?x + (?m - ?l) * ?v\")",
256 "Rewrite (\"subtrahiere_x_minus_plus\", \"\<lbrakk>?l is_const; ?m is_const\<rbrakk>\n\<Longrightarrow> ?x - ?m * ?v + ?l * ?v = ?x + (- ?m + ?l) * ?v\")"]
257 then () else error "specific_from_prog ([1], Res) CHANGED";
258 (*[2], Res*)val ("ok", (_, _, ptp as (pt, p))) = Step.by_tactic (hd (specific_from_prog pt p)) (pt, p);
260 (*+*)if map Tactic.input_to_string (specific_from_prog pt p) =
261 ["Rewrite (\"tausche_minus\", \"\<lbrakk>?b ist_monom; ?a kleiner ?b\<rbrakk>\n\<Longrightarrow> ?b - ?a = - ?a + ?b\")", "Rewrite (\"tausche_plus_minus\", \"?b kleiner ?c \<Longrightarrow> ?a + ?c - ?b = ?a - ?b + ?c\")",
262 "Rewrite (\"subtrahiere_x_plus_minus\", \"\<lbrakk>?l is_const; ?m is_const\<rbrakk>\n\<Longrightarrow> ?x + ?m * ?v - ?l * ?v = ?x + (?m - ?l) * ?v\")",
263 "Rewrite (\"subtrahiere_x_minus_plus\", \"\<lbrakk>?l is_const; ?m is_const\<rbrakk>\n\<Longrightarrow> ?x - ?m * ?v + ?l * ?v = ?x + (- ?m + ?l) * ?v\")", "Calculate MINUS"]
264 then () else error "specific_from_prog ([1], Res) CHANGED";
265 (* = ([3], Res)*)val ("ok", (_, _, ptp as (pt, p))) = Step.by_tactic (hd (specific_from_prog pt p)) (pt, p);
267 (*//----------------- exception PTREE "get_obj f EmptyPtree" raised --------------------------\\*)
268 (** )val ("ok", (_, _, ptp as (pt, p))) =( **)
269 Step.by_tactic (hd (specific_from_prog pt p)) (pt, p);
270 "~~~~~ fun by_tactic , args:"; val (tac, (ptp as (pt, p))) = (hd (specific_from_prog pt p), (pt, p));
271 val Applicable.Yes m = (*case*) Solve_Step.check tac (pt, p) (*of*);
272 (*if*) Tactic.for_specify' m; (*false*)
274 Step_Solve.by_tactic m (pt, p);
275 "~~~~~ fun by_tactic , args:"; val (m, (pt, po as (p, p_))) = (m, (pt, p));
276 (*if*) Method.id_empty = get_obj g_metID pt (par_pblobj pt p) (*else*);
277 val thy' = get_obj g_domID pt (par_pblobj pt p);
278 val (is, sc) = LItool.resume_prog thy' (p,p_) pt;
280 (*case*) locate_input_tactic sc (pt, po) (fst is) (snd is) m (*of*);
281 "~~~~~ fun locate_input_tactic , args:"; val ((Rule.Prog prog), (cstate as (pt, (*?*)pos(*?*))), istate, ctxt, tac)
282 = (sc, (pt, po), (fst is), (snd is), m);
283 val srls = LItool.get_simplifier cstate (*TODO: shift into Istate.T*);
285 (*case*) scan_to_tactic1 (prog, (cstate, ctxt, tac)) istate (*of*);
286 "~~~~~ fun scan_to_tactic1 , args:"; val ((prog, (cctt as ((_, p), _, _))), (Istate.Pstate (ist as {path, ...})))
287 = ((prog, (cstate, ctxt, tac)), istate);
288 (*if*) path = [] orelse ((last_elem o fst) p = 0 andalso snd p = Res) (*else*);
290 go_scan_up1 (prog, cctt) ist;
291 "~~~~~ and go_scan_up1 , args:"; val ((yyy as (prog, _)), (ist as {path, ...}))
292 = ((prog, cctt), ist);
293 (*if*) 1 < length path (*then*);
295 scan_up1 yyy (ist |> path_up) (at_location (path_up' path) prog);
296 "~~~~~ fun scan_up1 , args:"; val (yyy, ist, (Const ("Tactical.Try"(*2*), _) $ _))
297 = (yyy, (ist |> path_up), (at_location (path_up' path) prog));
300 "~~~~~ and go_scan_up1 , args:"; val ((yyy as (prog, _)), (ist as {path, ...}))
302 (*if*) 1 < length path (*then*);
304 scan_up1 yyy (ist |> path_up) (at_location (path_up' path) prog);
305 "~~~~~ fun scan_up1 , args:"; val ((yyy as (prog, xxx as (cstate, _, _))), ist,
306 (Const ("Tactical.Chain"(*3*), _) $ _ ))
307 = (yyy, (ist |> path_up), (at_location (path_up' path) prog));
308 val e2 = check_Seq_up ist prog
310 (*case*) scan_dn1 xxx (ist |> path_up_down [R] |> set_or ORundef) e (*of*);
311 "~~~~~ fun scan_dn1 , args:"; val (yyy, ist, (Const ("Tactical.Chain"(*2*), _) $ _ $ _))
312 = (xxx, (ist |> path_up_down [R] |> set_or ORundef), e2);
314 (*case*) scan_dn1 xxx (ist |> path_down [L, R]) e1 (*of*);
315 "~~~~~ fun scan_dn1 , args:"; val (xxx, ist, (Const ("Tactical.Try"(*2*), _) $ e))
316 = (xxx, (ist |> path_down [L, R]), e1);
318 (*case*) scan_dn1 xxx (ist |> path_down [R]) e (*of*);
319 (*======= end of scanning tacticals, a leaf =======*)
320 "~~~~~ fun scan_dn1 , args:"; val (((pt, p), ctxt, tac), (ist as {eval, act_arg, or, ...}), t)
321 = (xxx, (ist |> path_down [R]), e);
322 val (Program.Tac stac, a') = (*case*) check_leaf "locate" ctxt eval (get_subst ist) t (*of*);
323 val Not_Associated = (*case*) associate pt ctxt (tac, stac) (*of*);
324 val ORundef = (*case*) or (*of*);
325 val Applicable.No "norm_equation not applicable" =
326 (*case*) Solve_Step.check (LItool.tac_from_prog pt (ThyC.get_theory "Isac_Knowledge") stac) (pt, p) (*of*);
328 (Term_Val1 act_arg) (* return value *);
330 val Rewrite' ("PolyMinus", "tless_true", _, _, ("tausche_minus",_ (*"?b ist_monom \<Longrightarrow> ?a kleiner ?b \<Longrightarrow> ?b - ?a = - ?a + ?b"*)),
334 "([\"\n(t_t, 5 * e + 6 * f - 8 * g - 9 - 7 * e - 4 * f + 10 * g + 12)\"], [R,L,R,R,L,R,R], empty, SOME t_t, \n" ^
335 "- (8 * g) + (- 9 + 12 + 5 * e - 7 * e + (6 - 4) * f) + 10 * g, ORundef, true, false)"
337 UnparseC.term t = "- (8 * g) + (- 9 + 12 + 5 * e - 7 * e + (6 - 4) * f) + 10 * g"
339 UnparseC.term res = "- (8 * g) + (- 9 + 12 + 5 * e - 7 * e + (- 4 + 6) * f) + 10 * g"
341 UnparseC.terms asm = "[\"4 kleiner 6\",\"6 ist_monom\"]"
342 then () else error "locate_input_tactic Helpless, but applicable CHANGED";
345 "----------- re-build: fun find_next_step, mini ------------------------------------------------";
346 "----------- re-build: fun find_next_step, mini ------------------------------------------------";
347 "----------- re-build: fun find_next_step, mini ------------------------------------------------";
348 val fmz = ["Term (a + a ::real)", "normalform n_n"];
349 val (dI',pI',mI') = ("Poly",["polynomial","simplification"],["simplification","for_polynomials"]);
350 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
351 (*[], Pbl*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, Pos.e_pos'), []);(*Model_Problem*)
352 (*[], Pbl*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, Pos.e_pos'), []);(*Specify_Theory "Poly"*)
353 (*[], Pbl*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, Pos.e_pos'), []);(*Specify_Problem ["polynomial", "simplification"]*)
354 (*[], Met*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []);(*Specify_Method ["simplification", "for_polynomials"]*)
355 (*1], Frm*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []);(*Apply_Method ["simplification", "for_polynomials"]*)
356 (*[1], Res*)val (_, ([(tac'''''_', _, _)], _, (pt'''''_', p'''''_'))) =
358 Step.do_next p ((pt, e_pos'), []);(*Rewrite_Set "norm_Poly"*)
359 (*//------------------ go into 1 ------------------------------------------------------------\\*)
360 "~~~~~ fun do_next , args:"; val ((ip as (_, p_)), (ptp as (pt, p), tacis))
361 = (p, ((pt, e_pos'), []));
362 val pIopt = Ctree.get_pblID (pt, ip);
363 (*if*) ip = ([], Res) (*else*);
364 val _ = (*case*) tacis (*of*);
365 val SOME _ = (*case*) pIopt (*of*);
366 (*if*) Library.member op = [Pos.Pbl, Pos.Met] p_ (*else*);
368 val ("ok", ([(Rewrite_Set "norm_Poly", _, _)], _, (_, ([1], Res)))) =
369 Step_Solve.do_next (pt, ip);
370 "~~~~~ and do_next , args:"; val (ptp as (pt, pos as (p, p_))) = (pt, ip);
371 (*if*) Method.id_empty = get_obj g_metID pt (par_pblobj pt p) (*else*);
372 val thy' = get_obj g_domID pt (par_pblobj pt p);
373 val ((ist, ctxt), sc) = LItool.resume_prog thy' (p,p_) pt;
375 val Next_Step (_, _, Rewrite_Set' ("Poly", _, Rule_Set.Sequence {id = "norm_Poly", ...}, _, _)) =
376 LI.find_next_step sc (pt, pos) ist ctxt (*of*);
377 "~~~~~ fun find_next_step , args:"; val ((Rule.Prog prog), (ptp as(pt, (p, _))), (Pstate ist), ctxt)
378 = (sc, (pt, pos), ist, ctxt);
380 val Accept_Tac (Rewrite_Set' ("Poly", _, Rule_Set.Sequence {id = "norm_Poly", ...}, _, _), _, _) =
381 (*case*) scan_to_tactic (prog, (ptp, ctxt)) (Pstate ist) (*of*);
382 "~~~~~ fun scan_to_tactic , args:"; val ((prog, cc), (Pstate (ist as {path, ...})))
383 = ((prog, (ptp, ctxt)), (Pstate ist));
384 (*if*) path = [] (*then*);
386 val Accept_Tac (Rewrite_Set' ("Poly", _, Rule_Set.Sequence {id = "norm_Poly", ...}, _, _), _, _) =
387 scan_dn cc (trans_scan_dn ist) (Program.body_of prog);
388 "~~~~~ fun scan_dn , args:"; val ((cc as (_, ctxt)), (ist as {eval, ...}), t)
389 = (cc, (trans_scan_dn ist), (Program.body_of prog));
390 (*if*) Tactical.contained_in t (*else*);
391 val (Program.Tac prog_tac, form_arg) = (*case*) LItool.check_leaf "next " ctxt eval (get_subst ist) t (*of*);
393 val Accept_Tac (Rewrite_Set' ("Poly", _, Rule_Set.Sequence {id = "norm_Poly", ...}, _, _), _, _) =
394 check_tac cc ist (prog_tac, form_arg) (*return from xxx*);
395 "~~~~~ from fun scan_dn\<longrightarrow>fun scan_to_tactic\<longrightarrow>fun find_next_step, return:"; val (Accept_Tac (tac, ist, ctxt))
396 = (check_tac cc ist (prog_tac, form_arg));
398 Next_Step (Pstate ist, Tactic.insert_assumptions tac ctxt, tac) (*return from find_next_step*);
399 "~~~~~ from fun find_next_step\<longrightarrow>and do_next\<longrightarrow>fun zzz, return:"; val (Next_Step (ist, ctxt, tac))
400 = (Next_Step (Pstate ist, Tactic.insert_assumptions tac ctxt, tac));
402 LI.by_tactic tac (ist, Tactic.insert_assumptions tac ctxt) ptp (*return from and do_next*);
403 "~~~~~ from and do_next\<longrightarrow>fun do_next\<longrightarrow>toplevel, return:"; val (_, ([(tac''''', _, _)], _, (pt''''', p''''')))
404 = (LI.by_tactic tac (ist, Tactic.insert_assumptions tac ctxt) ptp);
405 (*\\------------------ end of go into 1 -----------------------------------------------------//*)
407 (*[], Res*)val (_, ([(tac''''', _, _)], _, (pt''''', p'''''))) =
409 Step.do_next p'''''_' ((pt'''''_', Pos.e_pos'), []);(* Check_Postcond ["polynomial", "simplification"]*)
410 (*//------------------ go into 2 ------------------------------------------------------------\\*)
411 "~~~~~ fun do_next , args:"; val ((ip as (_, p_)), (ptp as (pt, p), tacis))
412 = (p''''', ((pt''''', e_pos'), []));
413 val pIopt = Ctree.get_pblID (pt, ip);
414 (*if*) ip = ([], Res) (*else*);
415 val _ = (*case*) tacis (*of*);
416 val SOME _ = (*case*) pIopt (*of*);
417 (*if*) Library.member op = [Pos.Pbl, Pos.Met] p_ (*else*);
419 val ("ok", ([(Check_Postcond ["polynomial", "simplification"], _, _)], _, (_, ([], Res)))) =
420 Step_Solve.do_next (pt, ip);
421 "~~~~~ and do_next , args:"; val (ptp as (pt, pos as (p, p_))) = (pt, ip);
422 (*if*) Method.id_empty = get_obj g_metID pt (par_pblobj pt p) (*else*);
423 val thy' = get_obj g_domID pt (par_pblobj pt p);
424 val ((ist, ctxt), sc) = LItool.resume_prog thy' (p,p_) pt;
426 (** )val End_Program (ist, tac) =
427 ( *case*) LI.find_next_step sc (pt, pos) ist ctxt (*of*);
428 "~~~~~ fun find_next_step , args:"; val ((Rule.Prog prog), (ptp as(pt, (p, _))), (Pstate ist), ctxt)
429 = (sc, (pt, pos), ist, ctxt);
431 (* val Term_Val (Const ("Groups.times_class.times", _) $ Free ("2", _) $ Free ("a", _))*)
432 (** )val Term_Val prog_result =
433 ( *case*) scan_to_tactic (prog, (ptp, ctxt)) (Pstate ist) (*of*);
434 "~~~~~ fun scan_to_tactic , args:"; val ((prog, cc), (Pstate (ist as {path, ...})))
435 = ((prog, (ptp, ctxt)), (Pstate ist));
436 (*if*) path = [] (*else*);
438 go_scan_up (prog, cc) (trans_scan_up ist |> set_found);
439 "~~~~~ fun go_scan_up , args:"; val ((pcc as (sc, _)), (ist as {path, act_arg, found_accept, ...}))
440 = ((prog, cc), (trans_scan_up ist(*|> set_found !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!! *)));
441 (*if*) path = [R] (*then*);
442 (*if*) found_accept = true (*then*);
444 Term_Val act_arg (*return from go_scan_up*);
445 "~~~~~ from fun go_scan_up\<longrightarrow>fun scan_to_tactic, return:"; val (Term_Val prog_result) = (Term_Val act_arg);
447 Term_Val prog_result (*return from scan_to_tactic*);
448 "~~~~~ from fun scan_to_tactic\<longrightarrow>fun find_next_step, return:"; val (Term_Val prog_result) = (Term_Val prog_result);
449 val (true, p', _) = (*case*) parent_node pt p (*of*);
450 val (_, pblID, _) = get_obj g_spec pt p';
452 End_Program (Pstate ist, Tactic.Check_Postcond' (pblID, prog_result))
453 (*return from find_next_step*);
454 "~~~~~ from fun find_next_step\<longrightarrow>and do_next\<longrightarrow>fun zzz, return:"; val (End_Program (ist, tac))
455 = (End_Program (Pstate ist, Tactic.Check_Postcond' (pblID,prog_result)));
456 val _ = (*case*) tac (*of*);
458 val ("ok", ([(Check_Postcond ["polynomial", "simplification"], _, _)], _, (_, ([], Res))))
459 = LI.by_tactic tac (ist, ctxt) ptp (*return from and do_next*);
460 "~~~~~ from and do_next\<longrightarrow>top level, return:"; val (_, ([(tac''''', _, _)], _, (pt''''', p''''')))
461 = (LI.by_tactic tac (ist, ctxt) ptp);
462 (*\\------------------ end of go into 2 -----------------------------------------------------//*)
464 (*[], Und*)val (msg, ([], _, (pt, p))) = Step.do_next p''''' ((pt''''', Pos.e_pos'), []);(**)
467 ([], Frm), Simplify (a + a)
468 . . . . . . . . . . Apply_Method ["simplification","for_polynomials"],
470 . . . . . . . . . . Rewrite_Set "norm_Poly",
472 . . . . . . . . . . Check_Postcond ["polynomial","simplification"],
475 (*/--- final test ---------------------------------------------------------------------------\\*)
476 val (res, asm) = (get_obj g_result pt (fst p));
477 if UnparseC.term res = "2 * a" andalso map UnparseC.term asm = []
478 andalso p = ([], Und) andalso msg = "end-of-calculation"
479 andalso pr_ctree pr_short pt = ". ----- pblobj -----\n1. a + a\n"
481 case tac''''' of Check_Postcond ["polynomial", "simplification"] => ()
482 | _ => error "re-build: fun find_next_step, mini 1"
483 else error "re-build: fun find_next_step, mini 2"
486 "----------- re-build: fun locate_input_term ---------------------------------------------------";
487 "----------- re-build: fun locate_input_term ---------------------------------------------------";
488 "----------- re-build: fun locate_input_term ---------------------------------------------------";
490 ----------- appendFormula: on Res + late deriv ------------------------------------------------*)
491 val fmz = ["equality (x+1=(2::real))", "solveFor x","solutions L"];
492 val (dI',pI',mI') = ("Test", ["sqroot-test","univariate","equation","test"],
493 ["Test","squ-equ-test-subpbl1"]);
494 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
495 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
496 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
497 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
498 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
499 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
500 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
501 (*[], Met*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*Apply_Method ["Test", "squ-equ-test-subpbl1"]*);
503 (*[1], Frm*)val (p,_,f,nxt,_,pt) = me nxt p [] pt;(*Rewrite_Set "norm_equation"*)
504 (*+*)if f2str f = "x + 1 = 2" then () else error "locate_input_term at ([1], Frm) CHANGED";
506 (*[1], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt;(*Rewrite_Set "Test_simplify"*)
507 (*+*)if f2str f = "x + 1 + -1 * 2 = 0" then () else error "locate_input_term at ([1], Frm) CHANGED";
510 ([], Frm), solve (x + 1 = 2, x)
511 . . . . . . . . . . Apply_Method ["Test","squ-equ-test-subpbl1"],
512 ([1], Frm), x + 1 = 2
513 . . . . . . . . . . Rewrite_Set "norm_equation",
514 ([1], Res), x + 1 + -1 * 2 = 0 ///Check_Postcond..ERROR*)
516 (*//---------- appendFormula 1 "x = 1" \<longrightarrow> Step_Solve.inform \<longrightarrow> LI.locate_input_term ----------\\*)
517 "~~~~~ fun appendFormula , args:"; val ((*cI, *) ifo: TermC.as_string) = ((**) "x = 1");
518 val cs = (*get_calc cI*) ((pt, p), [(*nxt, nxt_, (pos, (ist, ctxt))*)])
519 val pos = (*get_pos cI 1*) p
521 (*+*)val ptp''''' = (pt, p);
522 (*+*)if snd ptp''''' = ([1], Res) then () else error "old_cs changed";
523 (*+*)show_pt_tac pt; (*[
524 (*+*)([], Frm), solve (x + 1 = 2, x)
525 (*+*). . . . . . . . . . Apply_Method ["Test","squ-equ-test-subpbl1"],
526 (*+*)([1], Frm), x + 1 = 2
527 (*+*). . . . . . . . . . Rewrite_Set "norm_equation",
528 (*+*)([1], Res), x + 1 + -1 * 2 = 0 ///Check_Postcond*)
530 val ("ok", cs' as (_, _, ptp')) =
531 (*case*) Step.do_next pos cs (*of*);
533 val ("ok", (_(*use in DG !!!*), [], ptp''''' as (pt''''', p'''''))) = (*case*)
534 Step_Solve.by_term ptp' (encode ifo) (*of*);
535 "~~~~~ fun Step_Solve.by_term , args:"; val ((pt, pos as (p, _)), istr)
536 = (ptp', (encode ifo));
538 (*case*) TermC.parse (ThyC.get_theory "Isac_Knowledge") istr (*of*);
539 val f_in = Thm.term_of f_in
540 val pos_pred = lev_back(*'*) pos
541 val f_pred = Ctree.get_curr_formula (pt, pos_pred);
542 val f_succ = Ctree.get_curr_formula (pt, pos);
543 (*if*) f_succ = f_in (*else*);
545 (*case*) P_Specific.cas_input f_in (*of*);
547 (*old* ) val (_, _, metID) = get_obj g_spec pt (par_pblobj pt p)
548 (*old*) val {scr = prog, ...} = Method.from_store metID
549 (*old*) val istate = get_istate_LI pt pos
550 (*old*) val ctxt = get_ctxt pt pos
551 val LI.Found_Step (cstate'''''_', _(*istate*), _(*ctxt*)) = (*case*)
552 LI.locate_input_term prog (pt, pos) istate ctxt f_in (*of*);
553 "~~~~~ fun locate_input_term , args:"; val ((Rule.Prog _), ((pt, pos) : Calc.T), (_ : Istate.T), (_ : Proof.context), tm)
554 = (prog, (pt, pos), istate, ctxt, f_in);
557 (*NEW*) LI.locate_input_term (pt, pos) f_in (*of*);
558 "~~~~~ fun locate_input_term , args:"; val ((pt, pos), tm) = ((pt, pos), f_in);
559 val pos_pred = Pos.lev_back' pos (*f_pred ---"step pos cs"---> f_succ in appendFormula*)
561 val ("ok", (_, _, cstate as (pt', pos'))) =
562 (*case*) compare_step ([], [], (pt, pos_pred)) tm (*of*);
565 Found_Step (cstate, get_istate_LI pt' pos', get_ctxt pt' pos') (*return from locate_input_term*);
567 (*NEW*) Found_Step cstate (*return from locate_input_term*);
568 (*LI.Found_Step ( *)cstate(*, _(*istate*), _(*ctxt*))( *return from locate_input_term*);
569 "~~~~~ from fun locate_input_term\<longrightarrow>fun Step_Solve.by_term, return:"; val ("ok", (_(*use in DG !!!*), c, ptp as (_, p)))
570 = (("ok" , ([], [], cstate (* already contains istate, ctxt *))));
572 ("ok", ((*_ use in DG !!!,*) c, ptp(* as (_*), p))(*)*)(*return from Step_Solve.by_term*);
573 "~~~~~ from fun Step_Solve.by_term\<longrightarrow>(fun appendFormula)!toplevel, return:"; val ("ok", (_(*use in DG !!!*), [], ptp''''' as (pt''''', p''''')))
574 = ("ok", ([], [], ptp));
576 (*fun me requires nxt...*)
577 Step.do_next p''''' (ptp''''', []);
578 val ("ok", ([(nxt'''''_' as Check_Postcond ["LINEAR", "univariate", "equation", "test"], _, _)], _,
579 (pt'''''_', p'''''_'))) = Step.do_next p''''' (ptp''''', [])
580 (*\\---------- appendFormula 1 "x = 1" \<longrightarrow> Step_Solve.inform \<longrightarrow> LI.locate_input_term ----------//*)
582 (*//----- REPLACED BY appendFormula 1 "x = 1" \<longrightarrow> Step_Solve.inform \<longrightarrow> LI.locate_input_term -----\\* )
583 (*[2], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Subproblem ("Test", ["LINEAR", "univariate", "equation", "test"])*)
584 (*[3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Model_Problem*)
585 (*[3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Add_Given "equality (-1 + x = 0)"*)
586 (*[3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Add_Given "solveFor x"*)
587 (*[3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Add_Find "solutions x_i"*)
588 (*[3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Specify_Theory "Test"*)
589 (*[3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Specify_Problem ["LINEAR", "univariate", "equation", "test"]*)
590 (*[3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Specify_Method ["Test", "solve_linear"]*)
591 (*[3], Met*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Apply_Method ["Test", "solve_linear"]*)
592 (*[3, 1], Frm*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Rewrite_Set_Inst (["(''bdv'', x)"], "isolate_bdv")*)
593 (*[3, 1], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Rewrite_Set "Test_simplify"*)
594 (*[3, 2], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Check_Postcond ["LINEAR", "univariate", "equation", "test"]*)
595 ( *\\----- REPLACED BY appendFormula 1 "x = 1" \<longrightarrow> Step_Solve.inform \<longrightarrow> LI.locate_input_term -----//*)
597 (*[3], Res*)val (p,_,f,nxt,_,pt) = me nxt'''''_' p'''''_' [] pt'''''_'; (*nxt = Check_elementwise "Assumptions"*)
598 (*[4], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Check_Postcond ["sqroot-test", "univariate", "equation", "test"]*)
599 (*[], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = End_Proof'*)
601 (*/--- final test ---------------------------------------------------------------------------\\*)
602 if p = ([], Res) andalso f2str f = "[x = 1]" andalso pr_ctree pr_short pt =
603 ". ----- pblobj -----\n" ^
605 "2. x + 1 + -1 * 2 = 0\n" ^
606 "3. ----- pblobj -----\n" ^
607 "3.1. -1 + x = 0\n" ^
608 "3.2. x = 0 + -1 * -1\n" ^
609 "3.2.1. x = 0 + -1 * -1\n" ^
610 "3.2.2. x = 0 + 1\n" (*ATTENTION: see complete Calc below*)
611 then case nxt of End_Proof' => () | _ => error "re-build: fun locate_input_term CHANGED 1"
612 else error "re-build: fun locate_input_term CHANGED 2";
615 ([], Frm), solve (x + 1 = 2, x)
616 . . . . . . . . . . Apply_Method ["Test","squ-equ-test-subpbl1"],
617 ([1], Frm), x + 1 = 2
618 . . . . . . . . . . Rewrite_Set "norm_equation",
619 ([1], Res), x + 1 + -1 * 2 = 0
620 . . . . . . . . . . Rewrite_Set "Test_simplify",
621 ([2], Res), -1 + x = 0
622 . . . . . . . . . . Subproblem (Test, ["LINEAR","univariate","equation","test"]),
623 ([3], Pbl), solve (-1 + x = 0, x)
624 . . . . . . . . . . Apply_Method ["Test","solve_linear"],
625 ([3,1], Frm), -1 + x = 0
626 . . . . . . . . . . Rewrite_Set_Inst ([(''bdv'', x)], "isolate_bdv"),
627 ([3,1], Res), x = 0 + -1 * -1
628 . . . . . . . . . . Derive Test_simplify,
629 ([3,2,1], Frm), x = 0 + -1 * -1
630 . . . . . . . . . . Rewrite ("#: -1 * -1 = 1", "-1 * -1 = 1"),
631 ([3,2,1], Res), x = 0 + 1
632 . . . . . . . . . . Rewrite ("radd_0", "0 + ?k = ?k"),
633 ([3,2,2], Res), x = 1
634 . . . . . . . . . . Tactic.input_to_string not impl. for ?!,
636 . . . . . . . . . . Check_Postcond ["LINEAR","univariate","equation","test"],
638 . . . . . . . . . . Check_Postcond ["sqroot-test","univariate","equation","test"],
639 ([], Res), [x = 1]]*)