comment tactics in struct. (only)
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
16 (*RM*)| Del_Find' of TermC.as_string | Del_Given' of TermC.as_string | Del_Relation' of TermC.as_string
17 (*RM*)| Init_Proof' of TermC.as_string list * Spec.T
18 | Model_Problem' of Problem.id * Model.itm list * Model.itm list
19 | Refine_Problem' of Problem.id * (Model.itm list * (bool * term) list)
20 | Refine_Tacitly' of Problem.id * Problem.id * ThyC.id * Method.id * Model.itm list
21 | Specify_Method' of Method.id * Model.ori list * Model.itm list
22 | Specify_Problem' of Problem.id * (bool * (Model.itm list * (bool * term) list))
23 | Specify_Theory' of ThyC.id
24 (* ^^^^^--------------------- for specify-phase, for solve-phase ---------------------vvvvv*)
26 | Calculate' of ThyC.id * string * term * (term * ThmC.T)
27 | Check_Postcond' of Problem.id * term
28 | Check_elementwise' of term * TermC.as_string * Selem.result
29 (*RM*)| Derive' of Rule_Set.T
32 (*RM* )| Apply_Assumption of TermC.as_string list( *RM*)
33 | Or_to_List' of term * term
34 | Rewrite' of ThyC.id * Rewrite_Ord.rew_ord' * Rule_Set.T * bool * ThmC.T * term * Selem.result
35 | Rewrite_Inst' of ThyC.id * Rewrite_Ord.rew_ord' * Rule_Set.T * bool * subst * ThmC.T * term * Selem.result
36 | Rewrite_Set' of ThyC.id * bool * Rule_Set.T * term * Selem.result
37 | Rewrite_Set_Inst' of ThyC.id * bool * subst * Rule_Set.T * term * Selem.result
38 | Subproblem' of Spec.T * Model.ori list * term * Selem.fmz_ * Proof.context * term
39 | Substitute' of Rule_Def.rew_ord_ * Rule_Set.T * Subst.as_eqs * term * term
40 (*RM*)| Tac_ of theory * string * string * string
42 (*RM* )| Take_Inst of TermC.as_string( *RM*)
43 (*RM*)| Begin_Sequ' | Begin_Trans' of term
44 (*RM*)| Split_And' of term | Split_Or' of term | Split_Intersect' of term
45 (*RM*)| Conclude_And' of term | Conclude_Or' of term | Collect_Trues' of term
46 (*RM*)| End_Sequ' | End_Trans' of Selem.result
47 (*RM*)| End_Ruleset' of term | End_Intersect' of term | End_Proof''
48 (*RM*)| Detail_Set' of ThyC.id * bool * Rule_Set.T * term * Selem.result
49 (*RM*)| Detail_Set_Inst' of ThyC.id * bool * subst * Rule_Set.T * term * Selem.result
50 (*RM*)| End_Detail' of Selem.result;
52 val string_of: T -> string
55 Add_Find of TermC.as_string | Add_Given of TermC.as_string
56 | Add_Relation of TermC.as_string
57 | Apply_Method of Method.id
58 | Del_Find of TermC.as_string | Del_Given of TermC.as_string | Del_Relation of TermC.as_string
59 | Init_Proof of TermC.as_string list * Spec.T
61 | Refine_Problem of Problem.id
62 | Refine_Tacitly of Problem.id
63 | Specify_Method of Method.id
64 | Specify_Problem of Problem.id
65 | Specify_Theory of ThyC.id
66 (* ^^^^^--------------------- for specify-phase, for solve-phase ---------------------vvvvv*)
67 | CAScmd of TermC.as_string
69 | Check_Postcond of Problem.id
70 | Check_elementwise of TermC.as_string
71 (*RM*)| Derive of Rule_Set.id(*RM*)
74 (*RM*)| Apply_Assumption of TermC.as_string list
77 | Rewrite_Inst of Subst.input * ThmC.T
78 | Rewrite_Set of Rule_Set.id
79 | Rewrite_Set_Inst of Subst.input * Rule_Set.id
80 | Subproblem of ThyC.id * Problem.id
81 | Substitute of Subst.input
83 | Take of TermC.as_string
84 (*RM*)| Take_Inst of TermC.as_string
85 (*RM*)| Begin_Sequ | Begin_Trans
86 (*RM*)| Split_And | Split_Or | Split_Intersect
87 (*RM*)| Conclude_And | Conclude_Or | Collect_Trues
88 (*RM*)| End_Sequ | End_Trans
89 (*RM*)| End_Ruleset | End_Subproblem | End_Intersect
90 (*RM*)| Detail_Set of Rule_Set.id
91 (*RM*)| Detail_Set_Inst of Subst.input * Rule_Set.id
95 val input_to_string : input -> string
96 val tac2IDstr : input -> string
97 val is_empty : input -> bool
99 val eq_tac : input * input -> bool
100 val is_rewtac : input -> bool
101 val is_rewset : input -> bool
102 val rls_of : input -> Rule_Set.id
103 val rule2tac : theory -> (term * term) list -> Rule.rule -> input
104 val applicable : theory -> string -> Rule_Set.T -> term -> input ->input list
105 val for_specify: input -> bool
107 val input_from_T : T -> input
108 val result : T -> term
109 val creates_assms: T -> term list
110 val insert_assumptions: T -> Proof.context -> Proof.context
111 val for_specify': T -> bool
113 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
115 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
117 ( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
119 (*----- unused code, kept as hints to design ideas ---------------------------------------------*)
124 structure Tactic(**): TACTIC(**) =
128 (** tactics for user at front-end **)
131 Add_Find of TermC.as_string | Add_Given of TermC.as_string | Add_Relation of TermC.as_string
132 | Apply_Method of Method.id
133 | Del_Find of TermC.as_string | Del_Given of TermC.as_string | Del_Relation of TermC.as_string
134 | Init_Proof of TermC.as_string list * Spec.T
136 | Refine_Problem of Problem.id
137 | Refine_Tacitly of Problem.id
138 | Specify_Method of Method.id
139 | Specify_Problem of Problem.id
140 | Specify_Theory of ThyC.id
141 (* ^^^^^--------------------- for specify-phase, for solve-phase ---------------------vvvvv*)
142 | CAScmd of TermC.as_string
143 | Calculate of string
144 | Check_Postcond of Problem.id
145 | Check_elementwise of TermC.as_string
146 (*RM*)| Derive of Rule_Set.id
149 (*RM*)| Apply_Assumption of TermC.as_string list
152 | Rewrite_Inst of Subst.input * ThmC.T
153 | Rewrite_Set of Rule_Set.id
154 | Rewrite_Set_Inst of Subst.input * Rule_Set.id
155 | Subproblem of ThyC.id * Problem.id
156 | Substitute of Subst.input
157 (*RM*)| Tac of string
158 | Take of TermC.as_string
159 (*RM*)| Take_Inst of TermC.as_string
160 (*RM*)| Begin_Sequ | Begin_Trans
161 (*RM*)| Split_And | Split_Or | Split_Intersect
162 (*RM*)| Conclude_And | Conclude_Or | Collect_Trues
163 (*RM*)| End_Sequ | End_Trans
164 (*RM*)| End_Ruleset | End_Subproblem | End_Intersect
165 (*RM*)| Detail_Set of Rule_Set.id
166 (*RM*)| Detail_Set_Inst of Subst.input * Rule_Set.id
170 fun input_to_string ma = case ma of
171 Init_Proof (ppc, spec) =>
172 "Init_Proof "^(pair2str (strs2str ppc, Spec.to_string spec))
173 | Model_Problem => "Model_Problem "
174 | Refine_Tacitly pblID => "Refine_Tacitly " ^ strs2str pblID
175 | Refine_Problem pblID => "Refine_Problem " ^ strs2str pblID
176 | Add_Given cterm' => "Add_Given " ^ cterm'
177 | Del_Given cterm' => "Del_Given " ^ cterm'
178 | Add_Find cterm' => "Add_Find " ^ cterm'
179 | Del_Find cterm' => "Del_Find " ^ cterm'
180 | Add_Relation cterm' => "Add_Relation " ^ cterm'
181 | Del_Relation cterm' => "Del_Relation " ^ cterm'
183 | Specify_Theory domID => "Specify_Theory " ^ quote domID
184 | Specify_Problem pblID => "Specify_Problem " ^ strs2str pblID
185 | Specify_Method metID => "Specify_Method " ^ strs2str metID
186 | Apply_Method metID => "Apply_Method " ^ strs2str metID
187 | Check_Postcond pblID => "Check_Postcond " ^ strs2str pblID
188 | Free_Solve => "Free_Solve"
190 | Rewrite_Inst (subs, (id, thm)) =>
191 "Rewrite_Inst " ^ (pair2str (subs2str subs, spair2str (id, thm |> Thm.prop_of |> UnparseC.term)))
192 | Rewrite (id, thm) => "Rewrite " ^ spair2str (id, thm |> Thm.prop_of |> UnparseC.term)
193 | Rewrite_Set_Inst (subs, rls) =>
194 "Rewrite_Set_Inst " ^ pair2str (subs2str subs, quote rls)
195 | Rewrite_Set rls => "Rewrite_Set " ^ quote rls
196 | Detail_Set rls => "Detail_Set " ^ quote rls
197 | Detail_Set_Inst (subs, rls) => "Detail_Set_Inst " ^ pair2str (subs2str subs, quote rls)
198 | End_Detail => "End_Detail"
199 | Derive rls' => "Derive " ^ rls'
200 | Calculate op_ => "Calculate " ^ op_
201 | Substitute sube => "Substitute " ^ Subst.string_eqs_to_string sube
202 | Apply_Assumption ct's => "Apply_Assumption " ^ strs2str ct's
204 | Take cterm' => "Take " ^ quote cterm'
205 | Take_Inst cterm' => "Take_Inst " ^ quote cterm'
206 | Subproblem (domID, pblID) => "Subproblem " ^ pair2str (domID, strs2str pblID)
207 | End_Subproblem => "End_Subproblem"
208 | CAScmd cterm' => "CAScmd " ^ quote cterm'
210 | Check_elementwise cterm'=> "Check_elementwise " ^ quote cterm'
211 | Or_to_List => "Or_to_List "
212 | Collect_Trues => "Collect_Trues"
214 | Empty_Tac => "Empty_Tac"
215 | Tac string => "Tac " ^ string
216 | End_Proof' => "input End_Proof'"
217 | _ => "input_to_string not impl. for ?!";
219 fun tac2IDstr ma = case ma of
220 Model_Problem => "Model_Problem"
221 | Refine_Tacitly _ => "Refine_Tacitly"
222 | Refine_Problem _ => "Refine_Problem"
223 | Add_Given _ => "Add_Given"
224 | Del_Given _ => "Del_Given"
225 | Add_Find _ => "Add_Find"
226 | Del_Find _ => "Del_Find"
227 | Add_Relation _ => "Add_Relation"
228 | Del_Relation _ => "Del_Relation"
230 | Specify_Theory _ => "Specify_Theory"
231 | Specify_Problem _ => "Specify_Problem"
232 | Specify_Method _ => "Specify_Method"
233 | Apply_Method _ => "Apply_Method"
234 | Check_Postcond _ => "Check_Postcond"
235 | Free_Solve => "Free_Solve"
237 | Rewrite_Inst _ => "Rewrite_Inst"
238 | Rewrite _ => "Rewrite"
239 | Rewrite_Set_Inst _ => "Rewrite_Set_Inst"
240 | Rewrite_Set _ => "Rewrite_Set"
241 | Detail_Set _ => "Detail_Set"
242 | Detail_Set_Inst _ => "Detail_Set_Inst"
243 | Derive _ => "Derive "
244 | Calculate _ => "Calculate "
245 | Substitute _ => "Substitute"
246 | Apply_Assumption _ => "Apply_Assumption"
249 | Take_Inst _ => "Take_Inst"
250 | Subproblem _ => "Subproblem"
251 | End_Subproblem => "End_Subproblem"
252 | CAScmd _ => "CAScmd"
254 | Check_elementwise _ => "Check_elementwise"
255 | Or_to_List => "Or_to_List "
256 | Collect_Trues => "Collect_Trues"
258 | Empty_Tac => "Empty_Tac"
260 | End_Proof' => "End_Proof'"
261 | _ => "input_to_string not impl. for ?!";
263 fun is_empty input = case input of Empty_Tac => true | _ => false
265 fun eq_tac (Rewrite (id1, _), Rewrite (id2, _)) = id1 = id2
266 | eq_tac (Rewrite_Inst (_, (id1, _)), Rewrite_Inst (_, (id2, _))) = id1 = id2
267 | eq_tac (Rewrite_Set id1, Rewrite_Set id2) = id1 = id2
268 | eq_tac (Rewrite_Set_Inst (_, id1), Rewrite_Set_Inst (_, id2)) = id1 = id2
269 | eq_tac (Calculate id1, Calculate id2) = id1 = id2
272 fun is_rewset (Rewrite_Set_Inst _) = true
273 | is_rewset (Rewrite_Set _) = true
274 | is_rewset _ = false;
275 fun is_rewtac (Rewrite _) = true
276 | is_rewtac (Rewrite_Inst _) = true
277 | is_rewtac input = is_rewset input;
280 fun rls_of (Rewrite_Set_Inst (_, rls)) = rls
281 | rls_of (Rewrite_Set rls) = rls
282 | rls_of input = error ("rls_of: called with input \"" ^ tac2IDstr input ^ "\"");
284 fun rule2tac thy _ (Rule.Eval (opID, _)) = Calculate (assoc_calc thy opID)
285 | rule2tac _ [] (Rule.Thm thm'') = Rewrite thm''
286 | rule2tac _ subst (Rule.Thm thm'') =
287 Rewrite_Inst (Subst.T_to_input subst, thm'')
288 | rule2tac _ [] (Rule.Rls_ rls) = Rewrite_Set (Rule_Set.id rls)
289 | rule2tac _ subst (Rule.Rls_ rls) =
290 Rewrite_Set_Inst (Subst.T_to_input subst, (Rule_Set.id rls))
291 | rule2tac _ _ rule =
292 error ("rule2tac: called with \"" ^ Rule.to_string rule ^ "\"");
294 (* try if a rewrite-rule is applicable to a given formula;
295 in case of rule-sets (recursivley) collect all _atomic_ rewrites *)
296 fun try_rew thy ((_, ro) : Rewrite_Ord.rew_ord) erls (subst : subst) f (thm' as Rule.Thm (_, thm)) =
297 if Auto_Prog.contains_bdv thm
298 then case Rewrite.rewrite_inst_ thy ro erls false subst thm f of
299 SOME _ => [rule2tac thy subst thm']
301 else (case Rewrite.rewrite_ thy ro erls false thm f of
302 SOME _ => [rule2tac thy [] thm']
304 | try_rew thy _ _ _ f (cal as Rule.Eval c) =
305 (case Eval.adhoc_thm thy c f of
306 SOME _ => [rule2tac thy [] cal]
308 | try_rew thy _ _ _ f (cal as Rule.Cal1 c) =
309 (case Eval.adhoc_thm thy c f of
310 SOME _ => [rule2tac thy [] cal]
312 | try_rew thy _ _ subst f (Rule.Rls_ rls) = filter_appl_rews thy subst f rls
313 | try_rew _ _ _ _ _ _ = error "try_rew: uncovered case"
314 and filter_appl_rews thy subst f (Rule_Def.Repeat {rew_ord = ro, erls, rules, ...}) =
315 gen_distinct eq_tac (flat (map (try_rew thy ro erls subst f) rules))
316 | filter_appl_rews thy subst f (Rule_Set.Sequence {rew_ord = ro, erls, rules,...}) =
317 gen_distinct eq_tac (flat (map (try_rew thy ro erls subst f) rules))
318 | filter_appl_rews _ _ _ (Rule_Set.Rrls _) = []
319 | filter_appl_rews _ _ _ _ = error "filter_appl_rews: uncovered case"
321 (* decide if a tactic is applicable to a given formula;
322 in case of Rewrite_Set* go down to _atomic_ rewrite-tactics *)
323 fun applicable thy _ _ f (Calculate scrID) =
324 try_rew thy Rewrite_Ord.e_rew_ordX Rule_Set.empty [] f (Rule.Eval (assoc_calc' thy scrID |> snd))
325 | applicable thy ro erls f (Rewrite thm'') =
326 try_rew thy (ro, Rewrite_Ord.assoc_rew_ord ro) erls [] f (Rule.Thm thm'')
327 | applicable thy ro erls f (Rewrite_Inst (subs, thm'')) =
328 try_rew thy (ro, Rewrite_Ord.assoc_rew_ord ro) erls (Subst.T_from_input thy subs) f (Rule.Thm thm'')
330 | applicable thy _ _ f (Rewrite_Set rls') =
331 filter_appl_rews thy [] f (assoc_rls rls')
332 | applicable thy _ _ f (Rewrite_Set_Inst (subs, rls')) =
333 filter_appl_rews thy (Subst.T_from_input thy subs) f (assoc_rls rls')
334 | applicable _ _ _ _ tac =
335 (tracing ("### applicable: not impl. for tac = '" ^ input_to_string tac ^ "'"); []);
338 (** tactics for internal use **)
341 Add_Find' of TermC.as_string * Model.itm list | Add_Given' of TermC.as_string * Model.itm list
342 | Add_Relation' of TermC.as_string * Model.itm list (* for Step.do_next *)
343 | Apply_Method' of (* last step in specifu-phse, switch to solve-phase *)
344 Method.id * (* id in the Know_Store *)
345 term option * (* first formula in the (sub-)Problem TODO: rm option *)
346 Istate_Def.T * (* for starting the Program *)
347 Proof.context (* for starting the Program *)
348 (*RM*)| Del_Find' of TermC.as_string | Del_Given' of TermC.as_string | Del_Relation' of TermC.as_string
349 (*RM*)| Init_Proof' of TermC.as_string list * Spec.T
350 | Model_Problem' of (* first step in specify-phase *)
351 Problem.id * (* id in the Know_Store *)
352 Model.itm list * (* the model for the Problem *)
353 Model.itm list (* the model for the method *)
354 | Refine_Problem' of Problem.id * (Model.itm list * (bool * term) list)
356 Problem.id * (* the original id in the Know_Store *)
357 Problem.id * (* the id of the refined Problem *)
358 ThyC.id * (* the id of the refined theory *)
359 Method.id * (* the id of the refined Method *)
360 Model.itm list (* RM 9.03: remains [] for Model_Problem recognizing its activation *)
361 | Specify_Method' of Method.id * Model.ori list * Model.itm list
362 | Specify_Problem' of Problem.id *
363 (bool * (* all preconditions evaluate to True *)
364 (Model.itm list * (* the model checked for the input id *)
365 (bool * term) list)) (* individual preconditions marked true/false *)
366 | Specify_Theory' of ThyC.id
367 (* ^^^^^--------------------- for specify-phase, for solve-phase ---------------------vvvvv*)
369 | Calculate' of ThyC.id * string * term * (term * ThmC.T)
370 | Check_Postcond' of (* last step in solving a (sub-)Problem *)
371 Problem.id * (* id of the Problem to be checked *)
372 term (* return value of the program *)
373 | Check_elementwise' of(* DEPRECATED, made idle for Calc.T in df00a2b5c4cc *)
374 term * (* the current formula: [x=1,x=...] *)
375 string * (* the pred from Check_elementwise *)
376 Selem.result (* composed from (1) and (2): {x. pred} *)
377 (*RM*)| Derive' of Rule_Set.T
380 (*RM* )| Apply_Assumption of TermC.as_string list( *RM*)
381 | Or_to_List' of term * term
382 | Rewrite' of ThyC.id * Rewrite_Ord.rew_ord' * Rule_Set.T * bool * ThmC.T * term * Selem.result
383 | Rewrite_Inst' of ThyC.id * Rewrite_Ord.rew_ord' * Rule_Set.T * bool * subst * ThmC.T * term * Selem.result
384 | Rewrite_Set' of ThyC.id * bool * Rule_Set.T * term * Selem.result
385 | Rewrite_Set_Inst' of ThyC.id * bool * subst * Rule_Set.T * term * Selem.result
386 | Subproblem' of (* switch from solve-phase to specify-phase *)
387 Spec.T * (* specification of the SubProblem *)
388 (Model.ori list) * (* original model, filled in associate Subproblem' *)
389 term * (* headline of calc-head, filled -"- *)
390 Selem.fmz_ * (* string list from arguments of the calling Program*)
391 Proof.context * (* for the specify-phase *)
392 term (* Subproblem (thyID, pbl) OR CAS_Cmd *)
393 | Substitute' of (* substitute variables (TODO: from the context) *)
394 Rule_Def.rew_ord_ *(* for re-calculation *)
395 Rule_Set.T * (* for re-calculation *)
396 Subst.as_eqs * (* the substitution: terms of type bool *)
397 term * (* to be substituted into *)
398 term (* resulting from the substitution *)
399 (*RM*)| Tac_ of theory * string * string * string
401 (*RM*)| Begin_Sequ' | Begin_Trans' of term
402 (*RM*)| Split_And' of term | Split_Or' of term | Split_Intersect' of term
403 (*RM*)| Conclude_And' of term | Conclude_Or' of term | Collect_Trues' of term
404 (*RM*)| End_Sequ' | End_Trans' of Selem.result
405 (*RM*)| End_Ruleset' of term | End_Intersect' of term | End_Proof''
406 (*RM*)| Detail_Set' of ThyC.id * bool * Rule_Set.T * term * Selem.result
407 (*RM*)| Detail_Set_Inst' of ThyC.id * bool * subst * Rule_Set.T * term * Selem.result
408 (*RM*)| End_Detail' of Selem.result;
410 fun string_of ma = case ma of
411 Init_Proof' (ppc, spec) => "Init_Proof' " ^ pair2str (strs2str ppc, Spec.to_string spec)
412 | Model_Problem' (pblID, _, _) => "Model_Problem' " ^ strs2str pblID
413 | Refine_Tacitly'(p, prefin, domID, metID, _) => "Refine_Tacitly' (" ^ strs2str p ^ ", " ^
414 strs2str prefin ^ ", " ^ domID ^ ", " ^ strs2str metID ^ ", pbl-itms)"
415 | Refine_Problem' _ => "Refine_Problem' (" ^ (*matchs2str ms*)"..." ^ ")"
416 | Add_Given' _ => "Add_Given' "(*^cterm'*)
417 | Del_Given' _ => "Del_Given' "(*^cterm'*)
418 | Add_Find' _ => "Add_Find' "(*^cterm'*)
419 | Del_Find' _ => "Del_Find' "(*^cterm'*)
420 | Add_Relation' _ => "Add_Relation' "(*^cterm'*)
421 | Del_Relation' _ => "Del_Relation' "(*^cterm'*)
423 | Specify_Theory' domID => "Specify_Theory' " ^ quote domID
424 | Specify_Problem' (pI, (ok, _)) => "Specify_Problem' " ^
425 spair2str (strs2str pI, spair2str (bool2str ok, spair2str ("itms2str_ itms", "items2str pre")))
426 | Specify_Method' (pI, oris, _) => "Specify_Method' (" ^
427 Method.id_to_string pI ^ ", " ^ Model.oris2str oris ^ ", )"
429 | Apply_Method' (metID, _, _, _) => "Apply_Method' " ^ strs2str metID
430 | Check_Postcond' (pblID, scval) => "Check_Postcond' " ^
431 (spair2str (strs2str pblID, UnparseC.term scval))
433 | Free_Solve' => "Free_Solve'"
435 | Rewrite_Inst' (*subs,thm'*) _ => "Rewrite_Inst' "(*^(pair2str (subs2str subs, spair2str thm'))*)
436 | Rewrite' _(*thm'*) => "Rewrite' "(*^(spair2str thm')*)
437 | Rewrite_Set_Inst' _(*subs,thm'*) => "Rewrite_Set_Inst' "(*^(pair2str (subs2str subs, quote rls))*)
438 | Rewrite_Set' (thy', pasm, rls', f, (f', asm)) => "Rewrite_Set' (" ^ thy' ^ "," ^ bool2str pasm ^
439 "," ^ Rule_Set.id rls' ^ "," ^ UnparseC.term f ^ ",(" ^ UnparseC.term f' ^ "," ^ UnparseC.terms asm ^ "))"
440 | End_Detail' _ => "End_Detail' xxx"
441 | Detail_Set' _ => "Detail_Set' xxx"
442 | Detail_Set_Inst' _ => "Detail_Set_Inst' xxx"
444 | Derive' rls => "Derive' " ^ Rule_Set.id rls
445 | Calculate' _ => "Calculate' "
446 | Substitute' _ => "Substitute' "(*^(subs2str subs)*)
448 | Take' _(*cterm'*) => "Take' "(*^(quote cterm' )*)
449 | Subproblem' _(*(spec, oris, _, _, _, pbl_form)*) =>
450 "Subproblem' "(*^(pair2str (domID, strs2str ,))*)
451 | CAScmd' _(*cterm'*) => "CAScmd' "(*^(quote cterm')*)
453 | Empty_Tac_ => "Empty_Tac_"
454 | Tac_ (_, form, id, result) => "Tac_ (thy," ^ form ^ "," ^ id ^ "," ^ result ^ ")"
455 | _ => "string_of not impl. for arg";
457 fun input_from_T (Refine_Tacitly' (pI, _, _, _, _)) = Refine_Tacitly pI
458 | input_from_T (Model_Problem' (_, _, _)) = Model_Problem
459 | input_from_T (Add_Given' (t, _)) = Add_Given t
460 | input_from_T (Add_Find' (t, _)) = Add_Find t
461 | input_from_T (Add_Relation' (t, _)) = Add_Relation t
463 | input_from_T (Specify_Theory' dI) = Specify_Theory dI
464 | input_from_T (Specify_Problem' (dI, _)) = Specify_Problem dI
465 | input_from_T (Specify_Method' (dI, _, _)) = Specify_Method dI
467 | input_from_T (Rewrite' (_, _, _, _, thm, _, _)) = Rewrite thm
468 | input_from_T (Rewrite_Inst' (_, _, _, _, sub, thm, _, _)) = Rewrite_Inst (Subst.T_to_input sub, thm)
470 | input_from_T (Rewrite_Set' (_, _, rls, _, _)) = Rewrite_Set (Rule_Set.id rls)
471 | input_from_T (Detail_Set' (_, _, rls, _, _)) = Detail_Set (Rule_Set.id rls)
473 | input_from_T (Rewrite_Set_Inst' (_, _, sub, rls, _, _)) =
474 Rewrite_Set_Inst (Subst.T_to_input sub, Rule_Set.id rls)
475 | input_from_T (Detail_Set_Inst' (_, _, sub, rls, _, _)) =
476 Detail_Set_Inst (Subst.T_to_input sub, Rule_Set.id rls)
478 | input_from_T (Calculate' (_, op_, _, _)) = Calculate (op_)
479 | input_from_T (Check_elementwise' (_, pred, _)) = Check_elementwise pred
481 | input_from_T (Or_to_List' _) = Or_to_List
482 | input_from_T (Take' term) = Take (UnparseC.term term)
483 | input_from_T (Substitute' (_, _, subte, _, _)) = Substitute (Subst.eqs_to_input subte)
484 | input_from_T (Tac_ (_, _, id, _)) = Tac id
486 | input_from_T (Subproblem' ((domID, pblID, _), _, _, _,_ ,_)) = Subproblem (domID, pblID)
487 | input_from_T (Check_Postcond' (pblID, _)) = Check_Postcond pblID
488 | input_from_T Empty_Tac_ = Empty_Tac
489 | input_from_T m = raise ERROR (": not impl. for "^(string_of m));
491 fun res (Rewrite_Inst' (_ , _, _, _, _, _, _, res)) = res
492 | res (Rewrite' (_, _, _, _, _, _, res)) = res
493 | res (Rewrite_Set_Inst' (_, _, _, _, _, res)) = res
494 | res (Rewrite_Set' (_, _, _, _, res)) = res
495 | res (Calculate' (_, _, _, (t, _))) = (t, [])
496 | res (Check_elementwise' (_, _, res)) = res
497 | res (Subproblem' (_, _, _, _, _, t)) = (t, [])
498 | res (Take' t) = (t, [])
499 | res (Substitute' (_, _, _, _, t)) = (t, [])
500 | res (Or_to_List' (_, t)) = (t, [])
501 | res m = raise ERROR ("result: not impl.for " ^ string_of m)
503 (*fun result m = (fst o res) m; TODO*)
504 fun result tac = (fst o res) tac;
505 fun creates_assms tac = (snd o res) tac;
507 fun insert_assumptions tac ctxt = ContextC.insert_assumptions (creates_assms tac) ctxt
509 fun for_specify (Init_Proof _) = true
510 | for_specify Model_Problem = true
511 | for_specify (Refine_Tacitly _) = true
512 | for_specify (Refine_Problem _) = true
513 | for_specify (Add_Given _) = true
514 | for_specify (Del_Given _) = true
515 | for_specify (Add_Find _) = true
516 | for_specify (Del_Find _) = true
517 | for_specify (Add_Relation _) = true
518 | for_specify (Del_Relation _) = true
519 | for_specify (Specify_Theory _) = true
520 | for_specify (Specify_Problem _) = true
521 | for_specify (Specify_Method _) = true
522 | for_specify _ = false
523 fun for_specify' (Init_Proof' _) = true
524 | for_specify' (Model_Problem' _) = true
525 | for_specify' (Refine_Tacitly' _) = true
526 | for_specify' (Refine_Problem' _) = true
527 | for_specify' (Add_Given' _) = true
528 | for_specify' (Del_Given' _) = true
529 | for_specify' (Add_Find' _) = true
530 | for_specify' (Del_Find' _) = true
531 | for_specify' (Add_Relation' _) = true
532 | for_specify' (Del_Relation' _) = true
533 | for_specify' (Specify_Theory' _) = true
534 | for_specify' (Specify_Problem' _) = true
535 | for_specify' (Specify_Method' _) = true
536 | for_specify' _ = false