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_Inst|Rewrite_Set|Rewrite_Set_Inst|Specify_Method|Specify_Problem|Specify_Theory|Subproblem|Substitute|Tac|Take|Take_Inst
13 Add_Find' of TermC.as_string * Model.itm list | Add_Given' of TermC.as_string * Model.itm list
14 | Add_Relation' of TermC.as_string * Model.itm list
15 | Apply_Method' of Method.id * term option * Istate_Def.T * Proof.context
17 | Begin_Sequ' | Begin_Trans' of term
18 | Split_And' of term | Split_Or' of term | Split_Intersect' of term
19 | Conclude_And' of term | Conclude_Or' of term | Collect_Trues' of term
20 | End_Sequ' | End_Trans' of Selem.result
21 | End_Ruleset' of term | End_Intersect' of term | End_Proof''
24 | Calculate' of ThyC.id * string * term * (term * ThmC.T)
25 | Check_Postcond' of Problem.id * term
26 | Check_elementwise' of term * TermC.as_string * Selem.result
27 | Del_Find' of TermC.as_string | Del_Given' of TermC.as_string | Del_Relation' of TermC.as_string
29 | Derive' of Rule_Set.T
30 | Detail_Set' of ThyC.id * bool * Rule_Set.T * term * Selem.result
31 | Detail_Set_Inst' of ThyC.id * bool * subst * Rule_Set.T * term * Selem.result
32 | End_Detail' of Selem.result
37 | Init_Proof' of TermC.as_string list * Spec.T
38 | Model_Problem' of Problem.id * Model.itm list * Model.itm list
39 | Or_to_List' of term * term
40 | Refine_Problem' of Problem.id * (Model.itm list * (bool * term) list)
41 | Refine_Tacitly' of Problem.id * Problem.id * ThyC.id * Method.id * Model.itm list
43 | Rewrite' of ThyC.id * Rewrite_Ord.rew_ord' * Rule_Set.T * bool * ThmC.T * term * Selem.result
44 | Rewrite_Inst' of ThyC.id * Rewrite_Ord.rew_ord' * Rule_Set.T * bool * subst * ThmC.T * term * Selem.result
45 | Rewrite_Set' of ThyC.id * bool * Rule_Set.T * term * Selem.result
46 | Rewrite_Set_Inst' of ThyC.id * bool * subst * Rule_Set.T * term * Selem.result
48 | Specify_Method' of Method.id * Model.ori list * Model.itm list
49 | Specify_Problem' of Problem.id * (bool * (Model.itm list * (bool * term) list))
50 | Specify_Theory' of ThyC.id
52 Spec.T * Model.ori list *
53 term * (* CAScmd, e.g. "solve (-1 + x = 0, x)" *)
54 Selem.fmz_ * (* either input to root-probl. or derived from prog. in ??? *)
56 Proof.context * (* derived from prog. in ??? *)
57 term (* ?UNUSED, e.g."Subproblem\n (''Test'',\n ??.\<^const>String.char.Char ''LINEAR'' ''univariate'' ''equation''\n ''test'')" *)
58 | Substitute' of Rule_Def.rew_ord_ * Rule_Set.T * Subst.as_eqs * term * term
59 | Tac_ of theory * string * string * string
61 val string_of: T -> string
64 Add_Find of TermC.as_string | Add_Given of TermC.as_string | Add_Relation of TermC.as_string
65 | Apply_Assumption of TermC.as_string list
66 | Apply_Method of Method.id
67 (*/--- TODO: re-design ? -----------------------------------------------------------------\*)
68 | Begin_Sequ | Begin_Trans
69 | Split_And | Split_Or | Split_Intersect
70 | Conclude_And | Conclude_Or | Collect_Trues
71 | End_Sequ | End_Trans
72 | End_Ruleset | End_Subproblem | End_Intersect | End_Proof'
73 (*\--- TODO: re-design ? -----------------------------------------------------------------/*)
74 | CAScmd of TermC.as_string
76 | Check_Postcond of Problem.id
77 | Check_elementwise of TermC.as_string
78 | Del_Find of TermC.as_string | Del_Given of TermC.as_string | Del_Relation of TermC.as_string
80 | Derive of Rule_Set.id
81 | Detail_Set of Rule_Set.id
82 | Detail_Set_Inst of Subst.input * Rule_Set.id
88 | Init_Proof of TermC.as_string list * Spec.T
91 | Refine_Problem of Problem.id
92 | Refine_Tacitly of Problem.id
95 | Rewrite_Inst of Subst.input * ThmC.T
96 | Rewrite_Set of Rule_Set.id
97 | Rewrite_Set_Inst of Subst.input * Rule_Set.id
99 | Specify_Method of Method.id
100 | Specify_Problem of Problem.id
101 | Specify_Theory of ThyC.id
102 | Subproblem of ThyC.id * Problem.id
104 | Substitute of Subst.input
106 | Take of TermC.as_string | Take_Inst of TermC.as_string
107 val input_to_string : input -> string
108 val tac2IDstr : input -> string
109 val is_empty : input -> bool
111 val eq_tac : input * input -> bool
112 val is_rewtac : input -> bool
113 val is_rewset : input -> bool
114 val rls_of : input -> Rule_Set.id
115 val rule2tac : theory -> (term * term) list -> Rule.rule -> input
116 val applicable : theory -> string -> Rule_Set.T -> term -> input ->input list
117 val for_specify: input -> bool
119 val input_from_T : T -> input
120 val result : T -> term
121 val creates_assms: T -> term list
122 val insert_assumptions: T -> Proof.context -> Proof.context
123 val for_specify': T -> bool
125 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
127 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
129 ( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
131 (*----- unused code, kept as hints to design ideas ---------------------------------------------*)
136 structure Tactic(**): TACTIC(**) =
140 (** tactics for user at front-end **)
142 (* tactics for user at front-end.
143 input propagates the construction of the calc-tree;
145 (a) 'specsteps' for the specify-phase, and others for the solve-phase
146 (b) those of the solve-phase are 'initac's and others;
147 initacs start with a formula different from the preceding formula.
148 see 'type tac_' for the internal representation of tactics
151 Add_Find of TermC.as_string | Add_Given of TermC.as_string | Add_Relation of TermC.as_string
152 | Apply_Assumption of TermC.as_string list
153 | Apply_Method of Method.id
154 (* creates an "istate" in PblObj.env; in case of "implicit_take"
155 creates a formula at ((lev_on o lev_dn) p, Frm) and in this "ppobj.loc"
156 a "SOME istate" at fst of "loc".
157 As each step (in the solve-phase) has a resulting formula (at the front-end)
158 Apply_Method also does the 1st step in the script (an "initac") if there is no "implicit_take" *)
159 (*/--- TODO: re-design ? -----------------------------------------------------------------\*)
160 | Begin_Sequ | Begin_Trans
161 | Split_And | Split_Or | Split_Intersect
162 | Conclude_And | Conclude_Or | Collect_Trues
163 | End_Sequ | End_Trans
164 | End_Ruleset | End_Subproblem (* WN0509 drop *) | End_Intersect | End_Proof'
165 (*\--- TODO: re-design ? -----------------------------------------------------------------/*)
166 | CAScmd of TermC.as_string
167 | Calculate of string
168 | Check_Postcond of Problem.id
169 | Check_elementwise of TermC.as_string
170 | Del_Find of TermC.as_string | Del_Given of TermC.as_string | Del_Relation of TermC.as_string
172 | Derive of Rule_Set.id (* WN0509 drop *)
173 | Detail_Set of Rule_Set.id (* WN0509 drop *)
174 | Detail_Set_Inst of Subst.input * Rule_Set.id (* WN0509 drop *)
175 | End_Detail (* WN0509 drop *)
180 | Init_Proof of TermC.as_string list * Spec.T
183 | Refine_Problem of Problem.id
184 | Refine_Tacitly of Problem.id
186 (* rewrite-tactics can transport a (thmID, thm) to and (!) from the java-front-end
187 because there all the thms are present with both (thmID, thm)
188 (where user-views can show both or only one of (thmID, thm)),
189 and thm is created from ThmID by assoc_thm'' when entering isabisac *)
191 | Rewrite_Inst of Subst.input * ThmC.T
192 | Rewrite_Set of Rule_Set.id
193 | Rewrite_Set_Inst of Subst.input * Rule_Set.id
195 | Specify_Method of Method.id
196 | Specify_Problem of Problem.id
197 | Specify_Theory of ThyC.id
198 | Subproblem of ThyC.id * Problem.id (* WN0509 drop *)
200 | Substitute of Subst.input
201 | Tac of string (* WN0509 drop *)
202 | Take of TermC.as_string | Take_Inst of TermC.as_string
204 fun input_to_string ma = case ma of
205 Init_Proof (ppc, spec) =>
206 "Init_Proof "^(pair2str (strs2str ppc, Spec.to_string spec))
207 | Model_Problem => "Model_Problem "
208 | Refine_Tacitly pblID => "Refine_Tacitly " ^ strs2str pblID
209 | Refine_Problem pblID => "Refine_Problem " ^ strs2str pblID
210 | Add_Given cterm' => "Add_Given " ^ cterm'
211 | Del_Given cterm' => "Del_Given " ^ cterm'
212 | Add_Find cterm' => "Add_Find " ^ cterm'
213 | Del_Find cterm' => "Del_Find " ^ cterm'
214 | Add_Relation cterm' => "Add_Relation " ^ cterm'
215 | Del_Relation cterm' => "Del_Relation " ^ cterm'
217 | Specify_Theory domID => "Specify_Theory " ^ quote domID
218 | Specify_Problem pblID => "Specify_Problem " ^ strs2str pblID
219 | Specify_Method metID => "Specify_Method " ^ strs2str metID
220 | Apply_Method metID => "Apply_Method " ^ strs2str metID
221 | Check_Postcond pblID => "Check_Postcond " ^ strs2str pblID
222 | Free_Solve => "Free_Solve"
224 | Rewrite_Inst (subs, (id, thm)) =>
225 "Rewrite_Inst " ^ (pair2str (subs2str subs, spair2str (id, thm |> Thm.prop_of |> UnparseC.term)))
226 | Rewrite (id, thm) => "Rewrite " ^ spair2str (id, thm |> Thm.prop_of |> UnparseC.term)
227 | Rewrite_Set_Inst (subs, rls) =>
228 "Rewrite_Set_Inst " ^ pair2str (subs2str subs, quote rls)
229 | Rewrite_Set rls => "Rewrite_Set " ^ quote rls
230 | Detail_Set rls => "Detail_Set " ^ quote rls
231 | Detail_Set_Inst (subs, rls) => "Detail_Set_Inst " ^ pair2str (subs2str subs, quote rls)
232 | End_Detail => "End_Detail"
233 | Derive rls' => "Derive " ^ rls'
234 | Calculate op_ => "Calculate " ^ op_
235 | Substitute sube => "Substitute " ^ Subst.string_eqs_to_string sube
236 | Apply_Assumption ct's => "Apply_Assumption " ^ strs2str ct's
238 | Take cterm' => "Take " ^ quote cterm'
239 | Take_Inst cterm' => "Take_Inst " ^ quote cterm'
240 | Subproblem (domID, pblID) => "Subproblem " ^ pair2str (domID, strs2str pblID)
241 | End_Subproblem => "End_Subproblem"
242 | CAScmd cterm' => "CAScmd " ^ quote cterm'
244 | Check_elementwise cterm'=> "Check_elementwise " ^ quote cterm'
245 | Or_to_List => "Or_to_List "
246 | Collect_Trues => "Collect_Trues"
248 | Empty_Tac => "Empty_Tac"
249 | Tac string => "Tac " ^ string
250 | End_Proof' => "input End_Proof'"
251 | _ => "input_to_string not impl. for ?!";
253 fun tac2IDstr ma = case ma of
254 Model_Problem => "Model_Problem"
255 | Refine_Tacitly _ => "Refine_Tacitly"
256 | Refine_Problem _ => "Refine_Problem"
257 | Add_Given _ => "Add_Given"
258 | Del_Given _ => "Del_Given"
259 | Add_Find _ => "Add_Find"
260 | Del_Find _ => "Del_Find"
261 | Add_Relation _ => "Add_Relation"
262 | Del_Relation _ => "Del_Relation"
264 | Specify_Theory _ => "Specify_Theory"
265 | Specify_Problem _ => "Specify_Problem"
266 | Specify_Method _ => "Specify_Method"
267 | Apply_Method _ => "Apply_Method"
268 | Check_Postcond _ => "Check_Postcond"
269 | Free_Solve => "Free_Solve"
271 | Rewrite_Inst _ => "Rewrite_Inst"
272 | Rewrite _ => "Rewrite"
273 | Rewrite_Set_Inst _ => "Rewrite_Set_Inst"
274 | Rewrite_Set _ => "Rewrite_Set"
275 | Detail_Set _ => "Detail_Set"
276 | Detail_Set_Inst _ => "Detail_Set_Inst"
277 | Derive _ => "Derive "
278 | Calculate _ => "Calculate "
279 | Substitute _ => "Substitute"
280 | Apply_Assumption _ => "Apply_Assumption"
283 | Take_Inst _ => "Take_Inst"
284 | Subproblem _ => "Subproblem"
285 | End_Subproblem => "End_Subproblem"
286 | CAScmd _ => "CAScmd"
288 | Check_elementwise _ => "Check_elementwise"
289 | Or_to_List => "Or_to_List "
290 | Collect_Trues => "Collect_Trues"
292 | Empty_Tac => "Empty_Tac"
294 | End_Proof' => "End_Proof'"
295 | _ => "input_to_string not impl. for ?!";
297 fun is_empty input = case input of Empty_Tac => true | _ => false
299 fun eq_tac (Rewrite (id1, _), Rewrite (id2, _)) = id1 = id2
300 | eq_tac (Rewrite_Inst (_, (id1, _)), Rewrite_Inst (_, (id2, _))) = id1 = id2
301 | eq_tac (Rewrite_Set id1, Rewrite_Set id2) = id1 = id2
302 | eq_tac (Rewrite_Set_Inst (_, id1), Rewrite_Set_Inst (_, id2)) = id1 = id2
303 | eq_tac (Calculate id1, Calculate id2) = id1 = id2
306 fun is_rewset (Rewrite_Set_Inst _) = true
307 | is_rewset (Rewrite_Set _) = true
308 | is_rewset _ = false;
309 fun is_rewtac (Rewrite _) = true
310 | is_rewtac (Rewrite_Inst _) = true
311 | is_rewtac input = is_rewset input;
314 fun rls_of (Rewrite_Set_Inst (_, rls)) = rls
315 | rls_of (Rewrite_Set rls) = rls
316 | rls_of input = error ("rls_of: called with input \"" ^ tac2IDstr input ^ "\"");
318 fun rule2tac thy _ (Rule.Eval (opID, _)) = Calculate (assoc_calc thy opID)
319 | rule2tac _ [] (Rule.Thm thm'') = Rewrite thm''
320 | rule2tac _ subst (Rule.Thm thm'') =
321 Rewrite_Inst (Subst.T_to_input subst, thm'')
322 | rule2tac _ [] (Rule.Rls_ rls) = Rewrite_Set (Rule_Set.id rls)
323 | rule2tac _ subst (Rule.Rls_ rls) =
324 Rewrite_Set_Inst (Subst.T_to_input subst, (Rule_Set.id rls))
325 | rule2tac _ _ rule =
326 error ("rule2tac: called with \"" ^ Rule.to_string rule ^ "\"");
328 (* try if a rewrite-rule is applicable to a given formula;
329 in case of rule-sets (recursivley) collect all _atomic_ rewrites *)
330 fun try_rew thy ((_, ro) : Rewrite_Ord.rew_ord) erls (subst : subst) f (thm' as Rule.Thm (_, thm)) =
331 if Auto_Prog.contains_bdv thm
332 then case Rewrite.rewrite_inst_ thy ro erls false subst thm f of
333 SOME _ => [rule2tac thy subst thm']
335 else (case Rewrite.rewrite_ thy ro erls false thm f of
336 SOME _ => [rule2tac thy [] thm']
338 | try_rew thy _ _ _ f (cal as Rule.Eval c) =
339 (case Eval.adhoc_thm thy c f of
340 SOME _ => [rule2tac thy [] cal]
342 | try_rew thy _ _ _ f (cal as Rule.Cal1 c) =
343 (case Eval.adhoc_thm thy c f of
344 SOME _ => [rule2tac thy [] cal]
346 | try_rew thy _ _ subst f (Rule.Rls_ rls) = filter_appl_rews thy subst f rls
347 | try_rew _ _ _ _ _ _ = error "try_rew: uncovered case"
348 and filter_appl_rews thy subst f (Rule_Def.Repeat {rew_ord = ro, erls, rules, ...}) =
349 gen_distinct eq_tac (flat (map (try_rew thy ro erls subst f) rules))
350 | filter_appl_rews thy subst f (Rule_Set.Sequence {rew_ord = ro, erls, rules,...}) =
351 gen_distinct eq_tac (flat (map (try_rew thy ro erls subst f) rules))
352 | filter_appl_rews _ _ _ (Rule_Set.Rrls _) = []
353 | filter_appl_rews _ _ _ _ = error "filter_appl_rews: uncovered case"
355 (* decide if a tactic is applicable to a given formula;
356 in case of Rewrite_Set* go down to _atomic_ rewrite-tactics *)
357 fun applicable thy _ _ f (Calculate scrID) =
358 try_rew thy Rewrite_Ord.e_rew_ordX Rule_Set.empty [] f (Rule.Eval (assoc_calc' thy scrID |> snd))
359 | applicable thy ro erls f (Rewrite thm'') =
360 try_rew thy (ro, Rewrite_Ord.assoc_rew_ord ro) erls [] f (Rule.Thm thm'')
361 | applicable thy ro erls f (Rewrite_Inst (subs, thm'')) =
362 try_rew thy (ro, Rewrite_Ord.assoc_rew_ord ro) erls (Subst.T_from_input thy subs) f (Rule.Thm thm'')
364 | applicable thy _ _ f (Rewrite_Set rls') =
365 filter_appl_rews thy [] f (assoc_rls rls')
366 | applicable thy _ _ f (Rewrite_Set_Inst (subs, rls')) =
367 filter_appl_rews thy (Subst.T_from_input thy subs) f (assoc_rls rls')
368 | applicable _ _ _ _ tac =
369 (tracing ("### applicable: not impl. for tac = '" ^ input_to_string tac ^ "'"); []);
372 (** tactics for internal use **)
374 (* tactics for for internal use, compare "input" for user at the front-end.
375 tac_ contains results from check in 'fun applicable_in'.
376 This is useful for costly results, e.g. from rewriting;
377 however, these results might be changed by Scripts like
378 " eq = (Rewrite_Set ''ansatz_rls'' False) eql;" ^
379 " eq = (Rewrite_Set equival_trans False) eq;" ^
380 TODO.WN120106 ANALOGOUSLY TO Substitute':
381 So tac_ contains the term t the result was calculated from
382 in order to compare t with t' possibly changed by "Expr "
383 and re-calculate result if t<>t'
384 TODO.WN161219: replace *every* cterm' by term
387 Add_Find' of TermC.as_string * Model.itm list | Add_Given' of TermC.as_string * Model.itm list
388 | Add_Relation' of TermC.as_string * Model.itm list
389 | Apply_Method' of (* creates the 1st step visible in a (sub-) comprising
390 * tactic Apply_Method metID
392 Method.id * (* key for Know_Store *)
393 term option * (* the first formula of Calc.T. TODO: rm option *)
394 Istate_Def.T * (* for the newly started program *)
395 Proof.context (* for the newly started program *)
396 (*/--- TODO: re-design ? -----------------------------------------------------------------\*)
397 | Begin_Sequ' | Begin_Trans' of term
398 | Split_And' of term | Split_Or' of term | Split_Intersect' of term
399 | Conclude_And' of term | Conclude_Or' of term | Collect_Trues' of term
400 | End_Sequ' | End_Trans' of Selem.result
401 | End_Ruleset' of term | End_Intersect' of term | End_Proof''
402 (*\--- TODO: re-design ? -----------------------------------------------------------------/*)
404 | Calculate' of ThyC.id * string * term * (term * ThmC.T)
405 | Check_Postcond' of Problem.id *
406 term (* returnvalue of program in solve *)
407 | Check_elementwise' of (* DEPRECATED, made idle for Calc.T in df00a2b5c4cc *)
408 term * (* (1) the current formula: [x=1,x=...] *)
409 string * (* (2) the pred from Check_elementwise *)
410 Selem.result (* (3) composed from (1) and (2): {x. pred} *)
411 | Del_Find' of TermC.as_string | Del_Given' of TermC.as_string | Del_Relation' of TermC.as_string
413 | Derive' of Rule_Set.T
414 | Detail_Set' of ThyC.id * bool * Rule_Set.T * term * Selem.result
415 | Detail_Set_Inst' of ThyC.id * bool * subst * Rule_Set.T * term * Selem.result
416 | End_Detail' of Selem.result
421 | Init_Proof' of TermC.as_string list * Spec.T
422 | Model_Problem' of (* first step in specifying *)
423 Problem.id * (* key into Know_Store *)
424 Model.itm list * (* the 'untouched' pbl *)
425 Model.itm list (* the casually completed met *)
426 | Or_to_List' of term * term
427 | Refine_Problem' of Problem.id * (Model.itm list * (bool * term) list)
429 Problem.id * (* input *)
430 Problem.id * (* the refined from applicable_in *)
431 ThyC.id * (* from new pbt?! filled in specify *)
432 Method.id * (* from new pbt?! filled in specify *)
433 Model.itm list (* drop ! 9.03: remains [] for Model_Problem recognizing its activation *)
434 | Rewrite' of ThyC.id * Rewrite_Ord.rew_ord' * Rule_Set.T * bool * ThmC.T * term * Selem.result
435 | Rewrite_Inst' of ThyC.id * Rewrite_Ord.rew_ord' * Rule_Set.T * bool * subst * ThmC.T * term * Selem.result
436 | Rewrite_Set' of ThyC.id * bool * Rule_Set.T * term * Selem.result
437 | Rewrite_Set_Inst' of ThyC.id * bool * subst * Rule_Set.T * term * Selem.result
439 | Specify_Method' of Method.id * Model.ori list * Model.itm list
440 | Specify_Problem' of Problem.id *
441 (bool * (* matches *)
442 (Model.itm list * (* ppc *)
443 (bool * term) list)) (* preconditions marked true/false *)
444 | Specify_Theory' of ThyC.id
447 (Model.ori list) * (* filled in associate Subproblem' *)
448 term * (* filled -"-, headline of calc-head *)
449 Selem.fmz_ * (* string list from arguments *)
450 Proof.context * (* for specify-phase *)
451 term (* Subproblem (thyID, pbl) OR cascmd *)
453 Rule_Def.rew_ord_ * (* for re-calculation *)
454 Rule_Set.T * (* for re-calculation *)
455 Subst.as_eqs * (* the 'substitution': terms of type bool *)
456 term * (* to be substituted into *)
457 term (* resulting from the substitution *)
458 | Tac_ of theory * string * string * string
461 fun string_of ma = case ma of
462 Init_Proof' (ppc, spec) => "Init_Proof' " ^ pair2str (strs2str ppc, Spec.to_string spec)
463 | Model_Problem' (pblID, _, _) => "Model_Problem' " ^ strs2str pblID
464 | Refine_Tacitly'(p, prefin, domID, metID, _) => "Refine_Tacitly' (" ^ strs2str p ^ ", " ^
465 strs2str prefin ^ ", " ^ domID ^ ", " ^ strs2str metID ^ ", pbl-itms)"
466 | Refine_Problem' _ => "Refine_Problem' (" ^ (*matchs2str ms*)"..." ^ ")"
467 | Add_Given' _ => "Add_Given' "(*^cterm'*)
468 | Del_Given' _ => "Del_Given' "(*^cterm'*)
469 | Add_Find' _ => "Add_Find' "(*^cterm'*)
470 | Del_Find' _ => "Del_Find' "(*^cterm'*)
471 | Add_Relation' _ => "Add_Relation' "(*^cterm'*)
472 | Del_Relation' _ => "Del_Relation' "(*^cterm'*)
474 | Specify_Theory' domID => "Specify_Theory' " ^ quote domID
475 | Specify_Problem' (pI, (ok, _)) => "Specify_Problem' " ^
476 spair2str (strs2str pI, spair2str (bool2str ok, spair2str ("itms2str_ itms", "items2str pre")))
477 | Specify_Method' (pI, oris, _) => "Specify_Method' (" ^
478 Method.id_to_string pI ^ ", " ^ Model.oris2str oris ^ ", )"
480 | Apply_Method' (metID, _, _, _) => "Apply_Method' " ^ strs2str metID
481 | Check_Postcond' (pblID, scval) => "Check_Postcond' " ^
482 (spair2str (strs2str pblID, UnparseC.term scval))
484 | Free_Solve' => "Free_Solve'"
486 | Rewrite_Inst' (*subs,thm'*) _ => "Rewrite_Inst' "(*^(pair2str (subs2str subs, spair2str thm'))*)
487 | Rewrite' _(*thm'*) => "Rewrite' "(*^(spair2str thm')*)
488 | Rewrite_Set_Inst' _(*subs,thm'*) => "Rewrite_Set_Inst' "(*^(pair2str (subs2str subs, quote rls))*)
489 | Rewrite_Set' (thy', pasm, rls', f, (f', asm)) => "Rewrite_Set' (" ^ thy' ^ "," ^ bool2str pasm ^
490 "," ^ Rule_Set.id rls' ^ "," ^ UnparseC.term f ^ ",(" ^ UnparseC.term f' ^ "," ^ UnparseC.terms asm ^ "))"
491 | End_Detail' _ => "End_Detail' xxx"
492 | Detail_Set' _ => "Detail_Set' xxx"
493 | Detail_Set_Inst' _ => "Detail_Set_Inst' xxx"
495 | Derive' rls => "Derive' " ^ Rule_Set.id rls
496 | Calculate' _ => "Calculate' "
497 | Substitute' _ => "Substitute' "(*^(subs2str subs)*)
499 | Take' _(*cterm'*) => "Take' "(*^(quote cterm' )*)
500 | Subproblem' _(*(spec, oris, _, _, _, pbl_form)*) =>
501 "Subproblem' "(*^(pair2str (domID, strs2str ,))*)
502 | CAScmd' _(*cterm'*) => "CAScmd' "(*^(quote cterm')*)
504 | Empty_Tac_ => "Empty_Tac_"
505 | Tac_ (_, form, id, result) => "Tac_ (thy," ^ form ^ "," ^ id ^ "," ^ result ^ ")"
506 | _ => "string_of not impl. for arg";
508 fun input_from_T (Refine_Tacitly' (pI, _, _, _, _)) = Refine_Tacitly pI
509 | input_from_T (Model_Problem' (_, _, _)) = Model_Problem
510 | input_from_T (Add_Given' (t, _)) = Add_Given t
511 | input_from_T (Add_Find' (t, _)) = Add_Find t
512 | input_from_T (Add_Relation' (t, _)) = Add_Relation t
514 | input_from_T (Specify_Theory' dI) = Specify_Theory dI
515 | input_from_T (Specify_Problem' (dI, _)) = Specify_Problem dI
516 | input_from_T (Specify_Method' (dI, _, _)) = Specify_Method dI
518 | input_from_T (Rewrite' (_, _, _, _, thm, _, _)) = Rewrite thm
519 | input_from_T (Rewrite_Inst' (_, _, _, _, sub, thm, _, _)) = Rewrite_Inst (Subst.T_to_input sub, thm)
521 | input_from_T (Rewrite_Set' (_, _, rls, _, _)) = Rewrite_Set (Rule_Set.id rls)
522 | input_from_T (Detail_Set' (_, _, rls, _, _)) = Detail_Set (Rule_Set.id rls)
524 | input_from_T (Rewrite_Set_Inst' (_, _, sub, rls, _, _)) =
525 Rewrite_Set_Inst (Subst.T_to_input sub, Rule_Set.id rls)
526 | input_from_T (Detail_Set_Inst' (_, _, sub, rls, _, _)) =
527 Detail_Set_Inst (Subst.T_to_input sub, Rule_Set.id rls)
529 | input_from_T (Calculate' (_, op_, _, _)) = Calculate (op_)
530 | input_from_T (Check_elementwise' (_, pred, _)) = Check_elementwise pred
532 | input_from_T (Or_to_List' _) = Or_to_List
533 | input_from_T (Take' term) = Take (UnparseC.term term)
534 | input_from_T (Substitute' (_, _, subte, _, _)) = Substitute (Subst.eqs_to_input subte)
535 | input_from_T (Tac_ (_, _, id, _)) = Tac id
537 | input_from_T (Subproblem' ((domID, pblID, _), _, _, _,_ ,_)) = Subproblem (domID, pblID)
538 | input_from_T (Check_Postcond' (pblID, _)) = Check_Postcond pblID
539 | input_from_T Empty_Tac_ = Empty_Tac
540 | input_from_T m = raise ERROR (": not impl. for "^(string_of m));
542 fun res (Rewrite_Inst' (_ , _, _, _, _, _, _, res)) = res
543 | res (Rewrite' (_, _, _, _, _, _, res)) = res
544 | res (Rewrite_Set_Inst' (_, _, _, _, _, res)) = res
545 | res (Rewrite_Set' (_, _, _, _, res)) = res
546 | res (Calculate' (_, _, _, (t, _))) = (t, [])
547 | res (Check_elementwise' (_, _, res)) = res
548 | res (Subproblem' (_, _, _, _, _, t)) = (t, [])
549 | res (Take' t) = (t, [])
550 | res (Substitute' (_, _, _, _, t)) = (t, [])
551 | res (Or_to_List' (_, t)) = (t, [])
552 | res m = raise ERROR ("result: not impl.for " ^ string_of m)
554 (*fun result m = (fst o res) m; TODO*)
555 fun result tac = (fst o res) tac;
556 fun creates_assms tac = (snd o res) tac;
558 fun insert_assumptions tac ctxt = ContextC.insert_assumptions (creates_assms tac) ctxt
560 fun for_specify (Init_Proof _) = true
561 | for_specify Model_Problem = true
562 | for_specify (Refine_Tacitly _) = true
563 | for_specify (Refine_Problem _) = true
564 | for_specify (Add_Given _) = true
565 | for_specify (Del_Given _) = true
566 | for_specify (Add_Find _) = true
567 | for_specify (Del_Find _) = true
568 | for_specify (Add_Relation _) = true
569 | for_specify (Del_Relation _) = true
570 | for_specify (Specify_Theory _) = true
571 | for_specify (Specify_Problem _) = true
572 | for_specify (Specify_Method _) = true
573 | for_specify _ = false
574 fun for_specify' (Init_Proof' _) = true
575 | for_specify' (Model_Problem' _) = true
576 | for_specify' (Refine_Tacitly' _) = true
577 | for_specify' (Refine_Problem' _) = true
578 | for_specify' (Add_Given' _) = true
579 | for_specify' (Del_Given' _) = true
580 | for_specify' (Add_Find' _) = true
581 | for_specify' (Del_Find' _) = true
582 | for_specify' (Add_Relation' _) = true
583 | for_specify' (Del_Relation' _) = true
584 | for_specify' (Specify_Theory' _) = true
585 | for_specify' (Specify_Problem' _) = true
586 | for_specify' (Specify_Method' _) = true
587 | for_specify' _ = false