1 (* Title: Tactics; tac_ for interaction with frontend, input for internal use.
2 Author: Walther Neuper 170121
3 (c) due to copyright terms
5 regular expression for search:
7 Add_Find|Add_Given|Add_Relation|Apply_Assumption|Apply_Method|Begin_Sequ|Begin_Trans|Split_And|Split_Or|Split_Intersect|Conclude_And|Conclude_Or|Collect_Trues|End_Sequ|End_Trans|End_Ruleset|End_Subproblem|End_Intersect|End_Proof|CAScmd|Calculate|Check_Postcond|Check_elementwise|Del_Find|Del_Given|Del_Relation|Derive|Detail_Set|Detail_Set_Inst|End_Detail|Empty_Tac|Free_Solve|Init_Proof|Model_Problem Or_to_List|Refine_Problem|Refine_Tacitly| Rewrite|Rewrite_Asm|Rewrite_Inst|Rewrite_Set|Rewrite_Set_Inst|Specify_Method|Specify_Problem|Specify_Theory|Subproblem|Substitute|Tac|Take|Take_Inst
13 Add_Find' of Rule.cterm' * Model.itm list | Add_Given' of Rule.cterm' * Model.itm list
14 | Add_Relation' of Rule.cterm' * Model.itm list
15 | Apply_Assumption' of term list * term
16 | Apply_Method' of Celem.metID * term option * Istate_Def.T * Proof.context
18 | Begin_Sequ' | Begin_Trans' of term
19 | Split_And' of term | Split_Or' of term | Split_Intersect' of term
20 | Conclude_And' of term | Conclude_Or' of term | Collect_Trues' of term
21 | End_Sequ' | End_Trans' of Selem.result
22 | End_Ruleset' of term | End_Subproblem' of term | End_Intersect' of term | End_Proof''
25 | Calculate' of Rule.theory' * string * term * (term * Celem.thm')
26 | Check_Postcond' of Celem.pblID * Selem.result
27 | Check_elementwise' of term * Rule.cterm' * Selem.result
28 | Del_Find' of Rule.cterm' | Del_Given' of Rule.cterm' | Del_Relation' of Rule.cterm'
31 | Detail_Set' of Rule.theory' * bool * Rule.rls * term * Selem.result
32 | Detail_Set_Inst' of Rule.theory' * bool * Rule.subst * Rule.rls * term * Selem.result
33 | End_Detail' of Selem.result
38 | Init_Proof' of Rule.cterm' list * Celem.spec
39 | Model_Problem' of Celem.pblID * Model.itm list * Model.itm list
40 | Or_to_List' of term * term
41 | Refine_Problem' of Celem.pblID * (Model.itm list * (bool * term) list)
42 | Refine_Tacitly' of Celem.pblID * Celem.pblID * Rule.domID * Celem.metID * Model.itm list
44 | Rewrite' of Rule.theory' * Rule.rew_ord' * Rule.rls * bool * Celem.thm'' * term * Selem.result
45 | Rewrite_Asm' of Rule.theory' * Rule.rew_ord' * Rule.rls * bool * Celem.thm'' * term * Selem.result
46 | Rewrite_Inst' of Rule.theory' * Rule.rew_ord' * Rule.rls * bool * Rule.subst * Celem.thm'' * term * Selem.result
47 | Rewrite_Set' of Rule.theory' * bool * Rule.rls * term * Selem.result
48 | Rewrite_Set_Inst' of Rule.theory' * bool * Rule.subst * Rule.rls * term * Selem.result
50 | Specify_Method' of Celem.metID * Model.ori list * Model.itm list
51 | Specify_Problem' of Celem.pblID * (bool * (Model.itm list * (bool * term) list))
52 | Specify_Theory' of Rule.domID
53 | Subproblem' of Celem.spec * Model.ori list * term * Selem.fmz_ * Proof.context * term
54 | Substitute' of Rule.rew_ord_ * Rule.rls * Selem.subte * term * term
55 | Tac_ of theory * string * string * string
56 | Take' of term | Take_Inst' of term
57 val string_of : T -> string
60 Add_Find of Rule.cterm' | Add_Given of Rule.cterm' | Add_Relation of Rule.cterm'
61 | Apply_Assumption of Rule.cterm' list
62 | Apply_Method of Celem.metID
63 (*/--- TODO: re-design ? -----------------------------------------------------------------\*)
64 | Begin_Sequ | Begin_Trans
65 | Split_And | Split_Or | Split_Intersect
66 | Conclude_And | Conclude_Or | Collect_Trues
67 | End_Sequ | End_Trans
68 | End_Ruleset | End_Subproblem | End_Intersect | End_Proof'
69 (*\--- TODO: re-design ? -----------------------------------------------------------------/*)
70 | CAScmd of Rule.cterm'
72 | Check_Postcond of Celem.pblID
73 | Check_elementwise of Rule.cterm'
74 | Del_Find of Rule.cterm' | Del_Given of Rule.cterm' | Del_Relation of Rule.cterm'
77 | Detail_Set of Rule.rls'
78 | Detail_Set_Inst of Selem.subs * Rule.rls'
84 | Init_Proof of Rule.cterm' list * Celem.spec
87 | Refine_Problem of Celem.pblID
88 | Refine_Tacitly of Celem.pblID
90 | Rewrite of Celem.thm''
91 | Rewrite_Asm of Celem.thm''
92 | Rewrite_Inst of Selem.subs * Celem.thm''
93 | Rewrite_Set of Rule.rls'
94 | Rewrite_Set_Inst of Selem.subs * Rule.rls'
96 | Specify_Method of Celem.metID
97 | Specify_Problem of Celem.pblID
98 | Specify_Theory of Rule.domID
99 | Subproblem of Rule.domID * Celem.pblID
101 | Substitute of Selem.sube
103 | Take of Rule.cterm' | Take_Inst of Rule.cterm'
104 val tac2str : input -> string
106 val eq_tac : input * input -> bool
107 val is_empty_tac : input -> bool
108 val is_rewtac : input -> bool
109 val is_rewset : input -> bool
110 val rls_of : input -> Rule.rls'
111 val tac2IDstr : input -> string
112 val rule2tac : theory -> (term * term) list -> Rule.rule -> input
113 val input_from_T : T -> input
114 val result : T -> term
115 val creates_assms: T -> term list
116 val insert_assumptions: T -> Proof.context -> Proof.context
118 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
120 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
122 ( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
124 (*----- unused code, kept as hints to design ideas ---------------------------------------------*)
129 structure Tactic(**): TACTIC(**) =
133 (* tactics for user at front-end.
134 input propagates the construction of the calc-tree;
136 (a) 'specsteps' for the specify-phase, and others for the solve-phase
137 (b) those of the solve-phase are 'initac's and others;
138 initacs start with a formula different from the preceding formula.
139 see 'type tac_' for the internal representation of tactics
142 Add_Find of Rule.cterm' | Add_Given of Rule.cterm' | Add_Relation of Rule.cterm'
143 | Apply_Assumption of Rule.cterm' list
144 | Apply_Method of Celem.metID
145 (* creates an "istate" in PblObj.env; in case of "init_form"
146 creates a formula at ((lev_on o lev_dn) p, Frm) and in this "ppobj.loc"
147 a "SOME istate" at fst of "loc".
148 As each step (in the solve-phase) has a resulting formula (at the front-end)
149 Apply_Method also does the 1st step in the script (an "initac") if there is no "init_form" *)
150 (*/--- TODO: re-design ? -----------------------------------------------------------------\*)
151 | Begin_Sequ | Begin_Trans
152 | Split_And | Split_Or | Split_Intersect
153 | Conclude_And | Conclude_Or | Collect_Trues
154 | End_Sequ | End_Trans
155 | End_Ruleset | End_Subproblem (* WN0509 drop *) | End_Intersect | End_Proof'
156 (*\--- TODO: re-design ? -----------------------------------------------------------------/*)
157 | CAScmd of Rule.cterm'
158 | Calculate of string
159 | Check_Postcond of Celem.pblID
160 | Check_elementwise of Rule.cterm'
161 | Del_Find of Rule.cterm' | Del_Given of Rule.cterm' | Del_Relation of Rule.cterm'
163 | Derive of Rule.rls' (* WN0509 drop *)
164 | Detail_Set of Rule.rls' (* WN0509 drop *)
165 | Detail_Set_Inst of Selem.subs * Rule.rls' (* WN0509 drop *)
166 | End_Detail (* WN0509 drop *)
171 | Init_Proof of Rule.cterm' list * Celem.spec
174 | Refine_Problem of Celem.pblID
175 | Refine_Tacitly of Celem.pblID
177 (* rewrite-tactics can transport a (thmID, thm) to and (!) from the java-front-end
178 because there all the thms are present with both (thmID, thm)
179 (where user-views can show both or only one of (thmID, thm)),
180 and thm is created from ThmID by assoc_thm'' when entering isabisac *)
181 | Rewrite of Celem.thm''
182 | Rewrite_Asm of Celem.thm''
183 | Rewrite_Inst of Selem.subs * Celem.thm''
184 | Rewrite_Set of Rule.rls'
185 | Rewrite_Set_Inst of Selem.subs * Rule.rls'
187 | Specify_Method of Celem.metID
188 | Specify_Problem of Celem.pblID
189 | Specify_Theory of Rule.domID
190 | Subproblem of Rule.domID * Celem.pblID (* WN0509 drop *)
192 | Substitute of Selem.sube
193 | Tac of string (* WN0509 drop *)
194 | Take of Rule.cterm' | Take_Inst of Rule.cterm'
196 fun tac2str ma = case ma of
197 Init_Proof (ppc, spec) =>
198 "Init_Proof "^(pair2str (strs2str ppc, Celem.spec2str spec))
199 | Model_Problem => "Model_Problem "
200 | Refine_Tacitly pblID => "Refine_Tacitly " ^ strs2str pblID
201 | Refine_Problem pblID => "Refine_Problem " ^ strs2str pblID
202 | Add_Given cterm' => "Add_Given " ^ cterm'
203 | Del_Given cterm' => "Del_Given " ^ cterm'
204 | Add_Find cterm' => "Add_Find " ^ cterm'
205 | Del_Find cterm' => "Del_Find " ^ cterm'
206 | Add_Relation cterm' => "Add_Relation " ^ cterm'
207 | Del_Relation cterm' => "Del_Relation " ^ cterm'
209 | Specify_Theory domID => "Specify_Theory " ^ quote domID
210 | Specify_Problem pblID => "Specify_Problem " ^ strs2str pblID
211 | Specify_Method metID => "Specify_Method " ^ strs2str metID
212 | Apply_Method metID => "Apply_Method " ^ strs2str metID
213 | Check_Postcond pblID => "Check_Postcond " ^ strs2str pblID
214 | Free_Solve => "Free_Solve"
216 | Rewrite_Inst (subs, (id, thm)) =>
217 "Rewrite_Inst " ^ (pair2str (subs2str subs, spair2str (id, thm |> Thm.prop_of |> Rule.term2str)))
218 | Rewrite (id, thm) => "Rewrite " ^ spair2str (id, thm |> Thm.prop_of |> Rule.term2str)
219 | Rewrite_Asm (id, thm) => "Rewrite_Asm " ^ spair2str (id, thm |> Thm.prop_of |> Rule.term2str)
220 | Rewrite_Set_Inst (subs, rls) =>
221 "Rewrite_Set_Inst " ^ pair2str (subs2str subs, quote rls)
222 | Rewrite_Set rls => "Rewrite_Set " ^ quote rls
223 | Detail_Set rls => "Detail_Set " ^ quote rls
224 | Detail_Set_Inst (subs, rls) => "Detail_Set_Inst " ^ pair2str (subs2str subs, quote rls)
225 | End_Detail => "End_Detail"
226 | Derive rls' => "Derive " ^ rls'
227 | Calculate op_ => "Calculate " ^ op_
228 | Substitute sube => "Substitute " ^ Selem.sube2str sube
229 | Apply_Assumption ct's => "Apply_Assumption " ^ strs2str ct's
231 | Take cterm' => "Take " ^ quote cterm'
232 | Take_Inst cterm' => "Take_Inst " ^ quote cterm'
233 | Subproblem (domID, pblID) => "Subproblem " ^ pair2str (domID, strs2str pblID)
234 | End_Subproblem => "End_Subproblem"
235 | CAScmd cterm' => "CAScmd " ^ quote cterm'
237 | Check_elementwise cterm'=> "Check_elementwise " ^ quote cterm'
238 | Or_to_List => "Or_to_List "
239 | Collect_Trues => "Collect_Trues"
241 | Empty_Tac => "Empty_Tac"
242 | Tac string => "Tac " ^ string
243 | End_Proof' => "input End_Proof'"
244 | _ => "tac2str not impl. for ?!";
246 fun is_empty_tac input = case input of Empty_Tac => true | _ => false
248 fun eq_tac (Rewrite (id1, _), Rewrite (id2, _)) = id1 = id2
249 | eq_tac (Rewrite_Inst (_, (id1, _)), Rewrite_Inst (_, (id2, _))) = id1 = id2
250 | eq_tac (Rewrite_Set id1, Rewrite_Set id2) = id1 = id2
251 | eq_tac (Rewrite_Set_Inst (_, id1), Rewrite_Set_Inst (_, id2)) = id1 = id2
252 | eq_tac (Calculate id1, Calculate id2) = id1 = id2
255 fun is_rewset (Rewrite_Set_Inst _) = true
256 | is_rewset (Rewrite_Set _) = true
257 | is_rewset _ = false;
258 fun is_rewtac (Rewrite _) = true
259 | is_rewtac (Rewrite_Inst _) = true
260 | is_rewtac (Rewrite_Asm _) = true
261 | is_rewtac input = is_rewset input;
263 fun tac2IDstr ma = case ma of
264 Model_Problem => "Model_Problem"
265 | Refine_Tacitly _ => "Refine_Tacitly"
266 | Refine_Problem _ => "Refine_Problem"
267 | Add_Given _ => "Add_Given"
268 | Del_Given _ => "Del_Given"
269 | Add_Find _ => "Add_Find"
270 | Del_Find _ => "Del_Find"
271 | Add_Relation _ => "Add_Relation"
272 | Del_Relation _ => "Del_Relation"
274 | Specify_Theory _ => "Specify_Theory"
275 | Specify_Problem _ => "Specify_Problem"
276 | Specify_Method _ => "Specify_Method"
277 | Apply_Method _ => "Apply_Method"
278 | Check_Postcond _ => "Check_Postcond"
279 | Free_Solve => "Free_Solve"
281 | Rewrite_Inst _ => "Rewrite_Inst"
282 | Rewrite _ => "Rewrite"
283 | Rewrite_Asm _ => "Rewrite_Asm"
284 | Rewrite_Set_Inst _ => "Rewrite_Set_Inst"
285 | Rewrite_Set _ => "Rewrite_Set"
286 | Detail_Set _ => "Detail_Set"
287 | Detail_Set_Inst _ => "Detail_Set_Inst"
288 | Derive _ => "Derive "
289 | Calculate _ => "Calculate "
290 | Substitute _ => "Substitute"
291 | Apply_Assumption _ => "Apply_Assumption"
294 | Take_Inst _ => "Take_Inst"
295 | Subproblem _ => "Subproblem"
296 | End_Subproblem => "End_Subproblem"
297 | CAScmd _ => "CAScmd"
299 | Check_elementwise _ => "Check_elementwise"
300 | Or_to_List => "Or_to_List "
301 | Collect_Trues => "Collect_Trues"
303 | Empty_Tac => "Empty_Tac"
305 | End_Proof' => "End_Proof'"
306 | _ => "tac2str not impl. for ?!";
308 fun rls_of (Rewrite_Set_Inst (_, rls)) = rls
309 | rls_of (Rewrite_Set rls) = rls
310 | rls_of input = error ("rls_of: called with input \"" ^ tac2IDstr input ^ "\"");
312 fun rule2tac thy _ (Rule.Calc (opID, _)) = Calculate (assoc_calc thy opID)
313 | rule2tac _ [] (Rule.Thm thm'') = Rewrite thm''
314 | rule2tac _ subst (Rule.Thm thm'') =
315 Rewrite_Inst (Selem.subst2subs subst, thm'')
316 | rule2tac _ [] (Rule.Rls_ rls) = Rewrite_Set (Rule.id_rls rls)
317 | rule2tac _ subst (Rule.Rls_ rls) =
318 Rewrite_Set_Inst (Selem.subst2subs subst, (Rule.id_rls rls))
319 | rule2tac _ _ rule =
320 error ("rule2tac: called with \"" ^ Rule.rule2str rule ^ "\"");
322 (* tactics for for internal use, compare "input" for user at the front-end.
323 tac_ contains results from check in 'fun applicable_in'.
324 This is useful for costly results, e.g. from rewriting;
325 however, these results might be changed by Scripts like
326 " eq = (Rewrite_Set ''ansatz_rls'' False) eql;" ^
327 " eq = (Rewrite_Set equival_trans False) eq;" ^
328 TODO.WN120106 ANALOGOUSLY TO Substitute':
329 So tac_ contains the term t the result was calculated from
330 in order to compare t with t' possibly changed by "Expr "
331 and re-calculate result if t<>t'
332 TODO.WN161219: replace *every* cterm' by term
335 Add_Find' of Rule.cterm' * Model.itm list | Add_Given' of Rule.cterm' * Model.itm list
336 | Add_Relation' of Rule.cterm' * Model.itm list
337 | Apply_Assumption' of term list * term
338 | Apply_Method' of Celem.metID * term option * Istate_Def.T * Proof.context
339 (*/--- TODO: re-design ? -----------------------------------------------------------------\*)
340 | Begin_Sequ' | Begin_Trans' of term
341 | Split_And' of term | Split_Or' of term | Split_Intersect' of term
342 | Conclude_And' of term | Conclude_Or' of term | Collect_Trues' of term
343 | End_Sequ' | End_Trans' of Selem.result
344 | End_Ruleset' of term | End_Subproblem' of term | End_Intersect' of term | End_Proof''
345 (*\--- TODO: re-design ? -----------------------------------------------------------------/*)
347 | Calculate' of Rule.theory' * string * term * (term * Celem.thm')
348 | Check_Postcond' of Celem.pblID *
349 Selem.result (* returnvalue of script in solve *)
350 | Check_elementwise' of (*special case:*)
351 term * (* (1) the current formula: [x=1,x=...] *)
352 string * (* (2) the pred from Check_elementwise *)
353 Selem.result (* (3) composed from (1) and (2): {x. pred} *)
354 | Del_Find' of Rule.cterm' | Del_Given' of Rule.cterm' | Del_Relation' of Rule.cterm'
356 | Derive' of Rule.rls
357 | Detail_Set' of Rule.theory' * bool * Rule.rls * term * Selem.result
358 | Detail_Set_Inst' of Rule.theory' * bool * Rule.subst * Rule.rls * term * Selem.result
359 | End_Detail' of Selem.result
364 | Init_Proof' of Rule.cterm' list * Celem.spec
365 | Model_Problem' of Celem.pblID *
366 Model.itm list * (* the 'untouched' pbl *)
367 Model.itm list (* the casually completed met *)
368 | Or_to_List' of term * term
369 | Refine_Problem' of Celem.pblID * (Model.itm list * (bool * term) list)
371 Celem.pblID * (* input*)
372 Celem.pblID * (* the refined from applicable_in *)
373 Rule.domID * (* from new pbt?! filled in specify *)
374 Celem.metID * (* from new pbt?! filled in specify *)
375 Model.itm list (* drop ! 9.03: remains [] for Model_Problem recognizing its activation *)
376 | Rewrite' of Rule.theory' * Rule.rew_ord' * Rule.rls * bool * Celem.thm'' * term * Selem.result
377 | Rewrite_Asm' of Rule.theory' * Rule.rew_ord' * Rule.rls * bool * Celem.thm'' * term * Selem.result
378 | Rewrite_Inst' of Rule.theory' * Rule.rew_ord' * Rule.rls * bool * Rule.subst * Celem.thm'' * term * Selem.result
379 | Rewrite_Set' of Rule.theory' * bool * Rule.rls * term * Selem.result
380 | Rewrite_Set_Inst' of Rule.theory' * bool * Rule.subst * Rule.rls * term * Selem.result
382 | Specify_Method' of Celem.metID * Model.ori list * Model.itm list
383 | Specify_Problem' of Celem.pblID *
384 (bool * (* matches *)
385 (Model.itm list * (* ppc *)
386 (bool * term) list)) (* preconditions *)
387 | Specify_Theory' of Rule.domID
390 (Model.ori list) * (* filled in associate Subproblem' *)
391 term * (* filled -"-, headline of calc-head *)
393 Proof.context * (* DEPRECATED shifted into loc for all ppobj *)
394 term (* Subproblem (thyID, pbl) OR cascmd *)
396 Rule.rew_ord_ * (* for re-calculation *)
397 Rule.rls * (* for re-calculation *)
398 Selem.subte * (* the 'substitution': terms of type bool *)
399 term * (* to be substituted into *)
400 term (* resulting from the substitution *)
401 | Tac_ of theory * string * string * string
402 | Take' of term | Take_Inst' of term
404 fun string_of ma = case ma of
405 Init_Proof' (ppc, spec) => "Init_Proof' " ^ pair2str (strs2str ppc, Celem.spec2str spec)
406 | Model_Problem' (pblID, _, _) => "Model_Problem' " ^ strs2str pblID
407 | Refine_Tacitly'(p, prefin, domID, metID, _) => "Refine_Tacitly' (" ^ strs2str p ^ ", " ^
408 strs2str prefin ^ ", " ^ domID ^ ", " ^ strs2str metID ^ ", pbl-itms)"
409 | Refine_Problem' _ => "Refine_Problem' (" ^ (*matchs2str ms*)"..." ^ ")"
410 | Add_Given' _ => "Add_Given' "(*^cterm'*)
411 | Del_Given' _ => "Del_Given' "(*^cterm'*)
412 | Add_Find' _ => "Add_Find' "(*^cterm'*)
413 | Del_Find' _ => "Del_Find' "(*^cterm'*)
414 | Add_Relation' _ => "Add_Relation' "(*^cterm'*)
415 | Del_Relation' _ => "Del_Relation' "(*^cterm'*)
417 | Specify_Theory' domID => "Specify_Theory' " ^ quote domID
418 | Specify_Problem' (pI, (ok, _)) => "Specify_Problem' " ^
419 spair2str (strs2str pI, spair2str (bool2str ok, spair2str ("itms2str_ itms", "items2str pre")))
420 | Specify_Method' (pI, oris, _) => "Specify_Method' (" ^
421 Celem.metID2str pI ^ ", " ^ Model.oris2str oris ^ ", )"
423 | Apply_Method' (metID, _, _, _) => "Apply_Method' " ^ strs2str metID
424 | Check_Postcond' (pblID, (scval, asm)) => "Check_Postcond' " ^
425 (spair2str (strs2str pblID, spair2str (Rule.term2str scval, Rule.terms2str asm)))
427 | Free_Solve' => "Free_Solve'"
429 | Rewrite_Inst' (*subs,thm'*) _ => "Rewrite_Inst' "(*^(pair2str (subs2str subs, spair2str thm'))*)
430 | Rewrite' _(*thm'*) => "Rewrite' "(*^(spair2str thm')*)
431 | Rewrite_Asm' _(*thm'*) => "Rewrite_Asm' "(*^(spair2str thm')*)
432 | Rewrite_Set_Inst' _(*subs,thm'*) => "Rewrite_Set_Inst' "(*^(pair2str (subs2str subs, quote rls))*)
433 | Rewrite_Set' (thy', pasm, rls', f, (f', asm)) => "Rewrite_Set' (" ^ thy' ^ "," ^ bool2str pasm ^
434 "," ^ Rule.id_rls rls' ^ "," ^ Rule.term2str f ^ ",(" ^ Rule.term2str f' ^ "," ^ Rule.terms2str asm ^ "))"
435 | End_Detail' _ => "End_Detail' xxx"
436 | Detail_Set' _ => "Detail_Set' xxx"
437 | Detail_Set_Inst' _ => "Detail_Set_Inst' xxx"
439 | Derive' rls => "Derive' " ^ Rule.id_rls rls
440 | Calculate' _ => "Calculate' "
441 | Substitute' _ => "Substitute' "(*^(subs2str subs)*)
442 | Apply_Assumption' _(* ct's*) => "Apply_Assumption' "(*^(strs2str ct's)*)
444 | Take' _(*cterm'*) => "Take' "(*^(quote cterm' )*)
445 | Take_Inst' _(*cterm'*) => "Take_Inst' "(*^(quote cterm' )*)
446 | Subproblem' _(*(spec, oris, _, _, _, pbl_form)*) =>
447 "Subproblem' "(*^(pair2str (domID, strs2str ,))*)
448 | End_Subproblem' _ => "End_Subproblem'"
449 | CAScmd' _(*cterm'*) => "CAScmd' "(*^(quote cterm')*)
451 | Empty_Tac_ => "Empty_Tac_"
452 | Tac_ (_, form, id, result) => "Tac_ (thy," ^ form ^ "," ^ id ^ "," ^ result ^ ")"
453 | _ => "string_of not impl. for arg";
455 fun input_from_T (Refine_Tacitly' (pI, _, _, _, _)) = Refine_Tacitly pI
456 | input_from_T (Model_Problem' (_, _, _)) = Model_Problem
457 | input_from_T (Add_Given' (t, _)) = Add_Given t
458 | input_from_T (Add_Find' (t, _)) = Add_Find t
459 | input_from_T (Add_Relation' (t, _)) = Add_Relation t
461 | input_from_T (Specify_Theory' dI) = Specify_Theory dI
462 | input_from_T (Specify_Problem' (dI, _)) = Specify_Problem dI
463 | input_from_T (Specify_Method' (dI, _, _)) = Specify_Method dI
465 | input_from_T (Rewrite' (_, _, _, _, thm, _, _)) = Rewrite thm
466 | input_from_T (Rewrite_Inst' (_, _, _, _, sub, thm, _, _)) = Rewrite_Inst (Selem.subst2subs sub, thm)
468 | input_from_T (Rewrite_Set' (_, _, rls, _, _)) = Rewrite_Set (Rule.id_rls rls)
469 | input_from_T (Detail_Set' (_, _, rls, _, _)) = Detail_Set (Rule.id_rls rls)
471 | input_from_T (Rewrite_Set_Inst' (_, _, sub, rls, _, _)) =
472 Rewrite_Set_Inst (Selem.subst2subs sub, Rule.id_rls rls)
473 | input_from_T (Detail_Set_Inst' (_, _, sub, rls, _, _)) =
474 Detail_Set_Inst (Selem.subst2subs sub, Rule.id_rls rls)
476 | input_from_T (Calculate' (_, op_, _, _)) = Calculate (op_)
477 | input_from_T (Check_elementwise' (_, pred, _)) = Check_elementwise pred
479 | input_from_T (Or_to_List' _) = Or_to_List
480 | input_from_T (Take' term) = Take (Rule.term2str term)
481 | input_from_T (Substitute' (_, _, subte, _, _)) = Substitute (Selem.subte2sube subte)
482 | input_from_T (Tac_ (_, _, id, _)) = Tac id
484 | input_from_T (Subproblem' ((domID, pblID, _), _, _, _,_ ,_)) = Subproblem (domID, pblID)
485 | input_from_T (Check_Postcond' (pblID, _)) = Check_Postcond pblID
486 | input_from_T Empty_Tac_ = Empty_Tac
487 | input_from_T m = error (": not impl. for "^(string_of m));
489 fun res (Rewrite_Inst' (_ , _, _, _, _, _, _, res)) = res
490 | res (Rewrite' (_, _, _, _, _, _, res)) = res
491 | res (Rewrite_Set_Inst' (_, _, _, _, _, res)) = res
492 | res (Rewrite_Set' (_, _, _, _, res)) = res
493 | res (Calculate' (_, _, _, (t, _))) = (t, [])
494 | res (Check_elementwise' (_, _, res)) = res
495 | res (Subproblem' (_, _, _, _, _, t)) = (t, [])
496 | res (Take' t) = (t, [])
497 | res (Substitute' (_, _, _, _, t)) = (t, [])
498 | res (Or_to_List' (_, t)) = (t, [])
499 | res m = raise ERROR ("result: not impl.for " ^ string_of m)
501 (*fun result m = (fst o res) m; TODO*)
502 fun result tac = (fst o res) tac;
503 fun creates_assms tac = (snd o res) tac;
505 fun insert_assumptions tac ctxt = ContextC.insert_assumptions (creates_assms tac) ctxt