conditional compilation via system option "isac_test" and antiquotation \<^isac_test>CARTOUCHE:
option is provided in session ROOT, or interactively via $ISABELLE_HOME_USER/etc/preferences (i.e. Isabelle/jEdit plugin preferences);
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_Method|Begin_Sequ|Begin_Trans|Split_And|Split_Or|Split_Intersect|Conclude_And|Conclude_Or|End_Sequ|End_Trans|End_Ruleset|End_Subproblem|End_Intersect|End_Proof|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_Def.i_model | Add_Given' of TermC.as_string * Model_Def.i_model
14 | Add_Relation' of TermC.as_string * Model_Def.i_model
15 (*RM*)| Del_Find' of TermC.as_string | Del_Given' of TermC.as_string | Del_Relation' of TermC.as_string
16 | Model_Problem' of Problem.id * Model_Def.i_model * Model_Def.i_model
17 | Refine_Problem' of Problem.id * (Model_Def.i_model * Pre_Conds_Def.T)
18 | Refine_Tacitly' of Problem.id * Problem.id * ThyC.id * MethodC.id * Model_Def.i_model
19 | Specify_Method' of MethodC.id * Model_Def.o_model * Model_Def.i_model
20 | Specify_Problem' of Problem.id * (bool * (Model_Def.i_model * Pre_Conds_Def.T))
21 | Specify_Theory' of ThyC.id
22 (* ^^^^^--------------------- for specify-phase, for solve-phase ---------------------vvvvv*)
23 | Apply_Method' of MethodC.id * term option * Istate_Def.T * Proof.context
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 * Celem.result
27 | Derive' of Rule_Set.T
30 | Or_to_List' of term * term
31 | Rewrite' of ThyC.id * Rewrite_Ord.rew_ord' * Rule_Set.T * bool * ThmC.T * term * Celem.result
32 | Rewrite_Inst' of ThyC.id * Rewrite_Ord.rew_ord' * Rule_Set.T * bool * subst * ThmC.T * term * Celem.result
33 | Rewrite_Set' of ThyC.id * bool * Rule_Set.T * term * Celem.result
34 | Rewrite_Set_Inst' of ThyC.id * bool * subst * Rule_Set.T * term * Celem.result
35 | Subproblem' of References_Def.T * Model_Def.o_model * term * Model_Def.form_model * Proof.context * term
36 | Substitute' of Rule_Def.rew_ord_ * Rule_Set.T * Subst.as_eqs * term * term
37 (*RM*)| Tac_ of theory * string * string * string
39 | End_Detail' of Celem.result
40 | Begin_Trans' of term | End_Trans' of Celem.result
43 val string_of: T -> string
46 Add_Find of TermC.as_string | Add_Given of TermC.as_string
47 | Add_Relation of TermC.as_string
48 | Del_Find of TermC.as_string | Del_Given of TermC.as_string | Del_Relation of TermC.as_string
50 | Refine_Problem of Problem.id
51 | Refine_Tacitly of Problem.id
52 | Specify_Method of MethodC.id
53 | Specify_Problem of Problem.id
54 | Specify_Theory of ThyC.id
55 (* ^^^^^--------------------- for specify-phase, for solve-phase ---------------------vvvvv*)
56 | Apply_Method of MethodC.id
58 | Check_Postcond of Problem.id
59 | Check_elementwise of TermC.as_string
60 | Derive of Rule_Set.id
65 | Rewrite_Inst of Subst.input * ThmC.T
66 | Rewrite_Set of Rule_Set.id
67 | Rewrite_Set_Inst of Subst.input * Rule_Set.id
68 | Subproblem of ThyC.id * Problem.id
69 | Substitute of Subst.input
71 | Take of TermC.as_string
73 | Begin_Trans | End_Trans
76 val input_to_string : input -> string
77 val tac2IDstr : input -> string
78 val is_empty : input -> bool
80 val eq_tac : input * input -> bool
81 val is_rewtac : input -> bool
82 val is_rewset : input -> bool
83 val rls_of : input -> Rule_Set.id
84 val rule2tac : theory -> (term * term) list -> Rule.rule -> input
85 val applicable : theory -> string -> Rule_Set.T -> term -> input ->input list
86 val for_specify: input -> bool
88 val input_from_T : T -> input
89 val result : T -> term
90 val creates_assms: T -> term list
91 val insert_assumptions: T -> Proof.context -> Proof.context
92 val for_specify': T -> bool
96 structure Tactic(**): TACTIC(**) =
100 (** tactics for user at front-end **)
103 Add_Find of TermC.as_string | Add_Given of TermC.as_string | Add_Relation of TermC.as_string
104 | Del_Find of TermC.as_string | Del_Given of TermC.as_string | Del_Relation of TermC.as_string
106 | Refine_Problem of Problem.id
107 | Refine_Tacitly of Problem.id
108 | Specify_Method of MethodC.id
109 | Specify_Problem of Problem.id
110 | Specify_Theory of ThyC.id
111 (* ^^^^^--------------------- for specify-phase, for solve-phase ---------------------vvvvv*)
112 | Apply_Method of MethodC.id
113 | Calculate of string
114 | Check_Postcond of Problem.id
115 | Check_elementwise of TermC.as_string
116 | Derive of Rule_Set.id
121 | Rewrite_Inst of Subst.input * ThmC.T
122 | Rewrite_Set of Rule_Set.id
123 | Rewrite_Set_Inst of Subst.input * Rule_Set.id
124 | Subproblem of ThyC.id * Problem.id
125 | Substitute of Subst.input
126 (*RM*)| Tac of string
127 | Take of TermC.as_string
129 | Begin_Trans | End_Trans
132 fun input_to_string ma = case ma of
133 Model_Problem => "Model_Problem "
134 | Refine_Tacitly pblID => "Refine_Tacitly " ^ strs2str pblID
135 | Refine_Problem pblID => "Refine_Problem " ^ strs2str pblID
136 | Add_Given cterm' => "Add_Given " ^ cterm'
137 | Del_Given cterm' => "Del_Given " ^ cterm'
138 | Add_Find cterm' => "Add_Find " ^ cterm'
139 | Del_Find cterm' => "Del_Find " ^ cterm'
140 | Add_Relation cterm' => "Add_Relation " ^ cterm'
141 | Del_Relation cterm' => "Del_Relation " ^ cterm'
143 | Specify_Theory domID => "Specify_Theory " ^ quote domID
144 | Specify_Problem pblID => "Specify_Problem " ^ strs2str pblID
145 | Specify_Method metID => "Specify_Method " ^ strs2str metID
146 | Apply_Method metID => "Apply_Method " ^ strs2str metID
147 | Check_Postcond pblID => "Check_Postcond " ^ strs2str pblID
148 | Free_Solve => "Free_Solve"
150 | Rewrite_Inst (subs, (id, thm)) =>
151 "Rewrite_Inst " ^ (pair2str (subs2str subs, spair2str (id, thm |> Thm.prop_of |> UnparseC.term)))
152 | Rewrite (id, thm) => "Rewrite " ^ spair2str (id, thm |> Thm.prop_of |> UnparseC.term)
153 | Rewrite_Set_Inst (subs, rls) =>
154 "Rewrite_Set_Inst " ^ pair2str (subs2str subs, quote rls)
155 | Rewrite_Set rls => "Rewrite_Set " ^ quote rls
156 | Begin_Trans => "Begin_Trans"
157 | End_Trans => "End_Trans"
158 | End_Detail => "End_Detail"
159 | Derive rls' => "Derive " ^ rls'
160 | Calculate op_ => "Calculate " ^ op_
161 | Substitute sube => "Substitute " ^ Subst.string_eqs_to_string sube
163 | Take cterm' => "Take " ^ quote cterm'
164 | Subproblem (domID, pblID) => "Subproblem " ^ pair2str (domID, strs2str pblID)
166 | Check_elementwise cterm'=> "Check_elementwise " ^ quote cterm'
167 | Or_to_List => "Or_to_List "
169 | Empty_Tac => "Empty_Tac"
170 (*RM*)| Tac string => "Tac " ^ string(*RM*)
171 | End_Proof' => "input End_Proof'"
172 | _ => "input_to_string not impl. for ?!";
174 fun tac2IDstr ma = case ma of
175 Model_Problem => "Model_Problem"
176 | Refine_Tacitly _ => "Refine_Tacitly"
177 | Refine_Problem _ => "Refine_Problem"
178 | Add_Given _ => "Add_Given"
179 | Del_Given _ => "Del_Given"
180 | Add_Find _ => "Add_Find"
181 | Del_Find _ => "Del_Find"
182 | Add_Relation _ => "Add_Relation"
183 | Del_Relation _ => "Del_Relation"
185 | Specify_Theory _ => "Specify_Theory"
186 | Specify_Problem _ => "Specify_Problem"
187 | Specify_Method _ => "Specify_Method"
188 | Apply_Method _ => "Apply_Method"
189 | Check_Postcond _ => "Check_Postcond"
190 | Free_Solve => "Free_Solve"
192 | Rewrite_Inst _ => "Rewrite_Inst"
193 | Rewrite _ => "Rewrite"
194 | Rewrite_Set_Inst _ => "Rewrite_Set_Inst"
195 | Rewrite_Set _ => "Rewrite_Set"
196 | Derive _ => "Derive "
197 | Calculate _ => "Calculate "
198 | Substitute _ => "Substitute"
201 | Subproblem _ => "Subproblem"
203 | Check_elementwise _ => "Check_elementwise"
204 | Or_to_List => "Or_to_List "
206 | Empty_Tac => "Empty_Tac"
208 | End_Proof' => "End_Proof'"
209 | _ => "input_to_string not impl. for ?!";
211 fun is_empty input = case input of Empty_Tac => true | _ => false
213 fun eq_tac (Rewrite (id1, _), Rewrite (id2, _)) = id1 = id2
214 | eq_tac (Rewrite_Inst (_, (id1, _)), Rewrite_Inst (_, (id2, _))) = id1 = id2
215 | eq_tac (Rewrite_Set id1, Rewrite_Set id2) = id1 = id2
216 | eq_tac (Rewrite_Set_Inst (_, id1), Rewrite_Set_Inst (_, id2)) = id1 = id2
217 | eq_tac (Calculate id1, Calculate id2) = id1 = id2
220 fun is_rewset (Rewrite_Set_Inst _) = true
221 | is_rewset (Rewrite_Set _) = true
222 | is_rewset _ = false;
223 fun is_rewtac (Rewrite _) = true
224 | is_rewtac (Rewrite_Inst _) = true
225 | is_rewtac input = is_rewset input;
228 fun rls_of (Rewrite_Set_Inst (_, rls)) = rls
229 | rls_of (Rewrite_Set rls) = rls
230 | rls_of input = raise ERROR ("rls_of: called with input \"" ^ tac2IDstr input ^ "\"");
232 fun rule2tac thy _ (Rule.Eval (opID, _)) = Calculate (assoc_calc thy opID)
233 | rule2tac _ [] (Rule.Thm thm'') = Rewrite thm''
234 | rule2tac _ subst (Rule.Thm thm'') =
235 Rewrite_Inst (Subst.T_to_input subst, thm'')
236 | rule2tac _ [] (Rule.Rls_ rls) = Rewrite_Set (Rule_Set.id rls)
237 | rule2tac _ subst (Rule.Rls_ rls) =
238 Rewrite_Set_Inst (Subst.T_to_input subst, (Rule_Set.id rls))
239 | rule2tac _ _ rule =
240 raise ERROR ("rule2tac: called with \"" ^ Rule.to_string rule ^ "\"");
242 (* try if a rewrite-rule is applicable to a given formula;
243 in case of rule-sets (recursivley) collect all _atomic_ rewrites *)
244 fun try_rew thy ((_, ro) : Rewrite_Ord.rew_ord) erls (subst : subst) f (thm' as Rule.Thm (_, thm)) =
245 if Auto_Prog.contains_bdv thm
246 then case Rewrite.rewrite_inst_ thy ro erls false subst thm f of
247 SOME _ => [rule2tac thy subst thm']
249 else (case Rewrite.rewrite_ thy ro erls false thm f of
250 SOME _ => [rule2tac thy [] thm']
252 | try_rew thy _ _ _ f (cal as Rule.Eval c) =
253 (case Eval.adhoc_thm thy c f of
254 SOME _ => [rule2tac thy [] cal]
256 | try_rew thy _ _ _ f (cal as Rule.Cal1 c) =
257 (case Eval.adhoc_thm thy c f of
258 SOME _ => [rule2tac thy [] cal]
260 | try_rew thy _ _ subst f (Rule.Rls_ rls) = filter_appl_rews thy subst f rls
261 | try_rew _ _ _ _ _ _ = raise ERROR "try_rew: uncovered case"
262 and filter_appl_rews thy subst f (Rule_Def.Repeat {rew_ord = ro, erls, rules, ...}) =
263 distinct eq_tac (flat (map (try_rew thy ro erls subst f) rules))
264 | filter_appl_rews thy subst f (Rule_Set.Sequence {rew_ord = ro, erls, rules,...}) =
265 distinct eq_tac (flat (map (try_rew thy ro erls subst f) rules))
266 | filter_appl_rews _ _ _ (Rule_Set.Rrls _) = []
267 | filter_appl_rews _ _ _ _ = raise ERROR "filter_appl_rews: uncovered case"
269 (* decide if a tactic is applicable to a given formula;
270 in case of Rewrite_Set* go down to _atomic_ rewrite-tactics *)
271 fun applicable thy _ _ f (Calculate scrID) =
272 try_rew thy Rewrite_Ord.e_rew_ordX Rule_Set.empty [] f (Rule.Eval (assoc_calc' thy scrID |> snd))
273 | applicable thy ro erls f (Rewrite thm'') =
274 try_rew thy (ro, Rewrite_Ord.assoc_rew_ord ro) erls [] f (Rule.Thm thm'')
275 | applicable thy ro erls f (Rewrite_Inst (subs, thm'')) =
276 try_rew thy (ro, Rewrite_Ord.assoc_rew_ord ro) erls (Subst.T_from_input thy subs) f (Rule.Thm thm'')
278 | applicable thy _ _ f (Rewrite_Set rls') =
279 filter_appl_rews thy [] f (assoc_rls rls')
280 | applicable thy _ _ f (Rewrite_Set_Inst (subs, rls')) =
281 filter_appl_rews thy (Subst.T_from_input thy subs) f (assoc_rls rls')
282 | applicable _ _ _ _ tac =
283 (tracing ("### applicable: not impl. for tac = '" ^ input_to_string tac ^ "'"); []);
286 (** tactics for internal use **)
289 Add_Find' of TermC.as_string * Model_Def.i_model | Add_Given' of TermC.as_string * Model_Def.i_model
290 | Add_Relation' of TermC.as_string * Model_Def.i_model (* for Step.do_next *)
291 (*RM*)| Del_Find' of TermC.as_string | Del_Given' of TermC.as_string | Del_Relation' of TermC.as_string
292 | Model_Problem' of (* first step in specify-phase *)
293 Problem.id * (* id in the Know_Store *)
294 Model_Def.i_model * (* the model for the Problem *)
295 Model_Def.i_model (* the model for the method *)
296 | Refine_Problem' of Problem.id * (Model_Def.i_model * Pre_Conds_Def.T)
298 Problem.id * (* the original id in the Know_Store *)
299 Problem.id * (* the id of the refined Problem *)
300 ThyC.id * (* the id of the refined theory *)
301 MethodC.id * (* the id of the refined MethodC *)
302 Model_Def.i_model (* RM 9.03: remains [] for Model_Problem recognizing its activation *)
303 | Specify_Method' of MethodC.id * Model_Def.o_model * Model_Def.i_model
304 | Specify_Problem' of Problem.id *
305 (bool * (* all preconditions evaluate to True *)
306 (Model_Def.i_model * (* the model checked for the input id *)
307 Pre_Conds_Def.T)) (* individual preconditions marked true/false *)
308 | Specify_Theory' of ThyC.id
309 (* ^^^^^--------------------- for specify-phase, for solve-phase ---------------------vvvvv*)
310 | Apply_Method' of (* last step in specifu-phse, switch to solve-phase *)
311 MethodC.id * (* id in the Know_Store *)
312 term option * (* first formula in the (sub-)Problem TODO: rm option *)
313 Istate_Def.T * (* for starting the Program *)
314 Proof.context (* for starting the Program *)
315 | Calculate' of ThyC.id * string * term * (term * ThmC.T)
316 | Check_Postcond' of (* last step in solving a (sub-)Problem *)
317 Problem.id * (* id of the Problem to be checked *)
318 term (* return value of the program *)
319 | Check_elementwise' of(* DEPRECATED, made idle for Calc.T in df00a2b5c4cc *)
320 term * (* the current formula: [x=1,x=...] *)
321 string * (* the pred from Check_elementwise *)
322 Celem.result (* composed from (1) and (2): {x. pred} *)
323 | Derive' of Rule_Set.T(* for Test_Out.embed_deriv *)
326 | Or_to_List' of term * term
327 | Rewrite' of ThyC.id * Rewrite_Ord.rew_ord' * Rule_Set.T * bool * ThmC.T * term * Celem.result
328 | Rewrite_Inst' of ThyC.id * Rewrite_Ord.rew_ord' * Rule_Set.T * bool * subst * ThmC.T * term * Celem.result
329 | Rewrite_Set' of ThyC.id * bool * Rule_Set.T * term * Celem.result
330 | Rewrite_Set_Inst' of ThyC.id * bool * subst * Rule_Set.T * term * Celem.result
331 | Subproblem' of (* switch from solve-phase to specify-phase *)
332 References_Def.T * (* specification of the SubProblem *)
333 (Model_Def.o_model) * (* original model, filled in associate Subproblem' *)
334 term * (* headline of calc-head, filled -"- *)
335 Model_Def.form_model * (* string list from arguments of the calling Program*)
336 Proof.context * (* for the specify-phase *)
337 term (* Subproblem (thyID, pbl) OR CAS_Cmd *)
338 | Substitute' of (* substitute variables (TODO: from the context) *)
339 Rule_Def.rew_ord_ *(* for re-calculation *)
340 Rule_Set.T * (* for re-calculation *)
341 Subst.as_eqs * (* the substitution: terms of type bool *)
342 term * (* to be substituted into *)
343 term (* resulting from the substitution *)
344 (*RM*)| Tac_ of theory * string * string * string
346 | End_Detail' of Celem.result (* for intermediate steps into Rewrite_Set *)
347 | Begin_Trans' of term (* for intermediate steps into Rewrite_Set *)
348 | End_Trans' of Celem.result (* for intermediate steps into Rewrite_Set *)
351 fun string_of ma = case ma of
352 Model_Problem' (pblID, _, _) => "Model_Problem' " ^ strs2str pblID
353 | Refine_Tacitly'(p, prefin, domID, metID, _) => "Refine_Tacitly' (" ^ strs2str p ^ ", " ^
354 strs2str prefin ^ ", " ^ domID ^ ", " ^ strs2str metID ^ ", pbl-itms)"
355 | Refine_Problem' _ => "Refine_Problem' (" ^ (*matchs2str ms*)"..." ^ ")"
356 | Add_Given' _ => "Add_Given' "(*^cterm'*)
357 | Del_Given' _ => "Del_Given' "(*^cterm'*)
358 | Add_Find' _ => "Add_Find' "(*^cterm'*)
359 | Del_Find' _ => "Del_Find' "(*^cterm'*)
360 | Add_Relation' _ => "Add_Relation' "(*^cterm'*)
361 | Del_Relation' _ => "Del_Relation' "(*^cterm'*)
363 | Specify_Theory' domID => "Specify_Theory' " ^ quote domID
364 | Specify_Problem' (pI, (ok, _)) => "Specify_Problem' " ^
365 spair2str (strs2str pI, spair2str (bool2str ok, spair2str ("itms2str_ itms", "items2str pre")))
366 | Specify_Method' (pI, oris, _) => "Specify_Method' (" ^
367 MethodC.id_to_string pI ^ ", " ^ Model_Def.o_model_to_string oris ^ ", )"
369 | Apply_Method' (metID, _, _, _) => "Apply_Method' " ^ strs2str metID
370 | Check_Postcond' (pblID, scval) => "Check_Postcond' " ^
371 (spair2str (strs2str pblID, UnparseC.term scval))
373 | Free_Solve' => "Free_Solve'"
375 | Rewrite_Inst' (*subs,thm'*) _ => "Rewrite_Inst' "(*^(pair2str (subs2str subs, spair2str thm'))*)
376 | Rewrite' _(*thm'*) => "Rewrite' "(*^(spair2str thm')*)
377 | Rewrite_Set_Inst' _(*subs,thm'*) => "Rewrite_Set_Inst' "(*^(pair2str (subs2str subs, quote rls))*)
378 | Rewrite_Set' (thy', pasm, rls', f, (f', asm)) => "Rewrite_Set' (" ^ thy' ^ ", " ^ bool2str pasm ^
379 ", " ^ Rule_Set.id rls' ^ ", " ^ UnparseC.term f ^ ",(" ^ UnparseC.term f' ^ ", " ^ UnparseC.terms asm ^ "))"
380 | End_Detail' _ => "End_Detail' xxx"
382 | Derive' rls => "Derive' " ^ Rule_Set.id rls
383 | Calculate' _ => "Calculate' "
384 | Substitute' _ => "Substitute' "(*^(subs2str subs)*)
386 | Take' _(*cterm'*) => "Take' "(*^(quote cterm' )*)
387 | Subproblem' _(*(spec, oris, _, _, _, pbl_form)*) =>
388 "Subproblem' "(*^(pair2str (domID, strs2str ,))*)
390 | Empty_Tac_ => "Empty_Tac_"
391 | Tac_ (_, form, id, result) => "Tac_ (thy," ^ form ^ ", " ^ id ^ ", " ^ result ^ ")"
393 | Begin_Trans' _ => "Begin_Trans' xxx"
394 | End_Trans' _ => "End_Trans' xxx"
395 | End_Proof'' => "End_Trans' xxx"
396 | _ => "string_of not impl. for arg";
398 fun input_from_T (Refine_Tacitly' (pI, _, _, _, _)) = Refine_Tacitly pI
399 | input_from_T (Model_Problem' (_, _, _)) = Model_Problem
400 | input_from_T (Add_Given' (t, _)) = Add_Given t
401 | input_from_T (Add_Find' (t, _)) = Add_Find t
402 | input_from_T (Add_Relation' (t, _)) = Add_Relation t
404 | input_from_T (Specify_Theory' dI) = Specify_Theory dI
405 | input_from_T (Specify_Problem' (dI, _)) = Specify_Problem dI
406 | input_from_T (Specify_Method' (dI, _, _)) = Specify_Method dI
408 | input_from_T (Rewrite' (_, _, _, _, thm, _, _)) = Rewrite thm
409 | input_from_T (Rewrite_Inst' (_, _, _, _, sub, thm, _, _)) = Rewrite_Inst (Subst.T_to_input sub, thm)
411 | input_from_T (Rewrite_Set' (_, _, rls, _, _)) = Rewrite_Set (Rule_Set.id rls)
412 | input_from_T (Rewrite_Set_Inst' (_, _, sub, rls, _, _)) =
413 Rewrite_Set_Inst (Subst.T_to_input sub, Rule_Set.id rls)
415 | input_from_T (Calculate' (_, op_, _, _)) = Calculate (op_)
416 | input_from_T (Check_elementwise' (_, pred, _)) = Check_elementwise pred
418 | input_from_T (Or_to_List' _) = Or_to_List
419 | input_from_T (Take' term) = Take (UnparseC.term term)
420 | input_from_T (Substitute' (_, _, subte, _, _)) = Substitute (Subst.eqs_to_input subte)
421 | input_from_T (Tac_ (_, _, id, _)) = Tac id
423 | input_from_T (Subproblem' ((domID, pblID, _), _, _, _,_ ,_)) = Subproblem (domID, pblID)
424 | input_from_T (Check_Postcond' (pblID, _)) = Check_Postcond pblID
425 | input_from_T Empty_Tac_ = Empty_Tac
426 | input_from_T m = raise ERROR (": not impl. for "^(string_of m));
428 fun res (Rewrite_Inst' (_ , _, _, _, _, _, _, res)) = res
429 | res (Rewrite' (_, _, _, _, _, _, res)) = res
430 | res (Rewrite_Set_Inst' (_, _, _, _, _, res)) = res
431 | res (Rewrite_Set' (_, _, _, _, res)) = res
432 | res (Calculate' (_, _, _, (t, _))) = (t, [])
433 | res (Check_elementwise' (_, _, res)) = res
434 | res (Subproblem' (_, _, _, _, _, t)) = (t, [])
435 | res (Take' t) = (t, [])
436 | res (Substitute' (_, _, _, _, t)) = (t, [])
437 | res (Or_to_List' (_, t)) = (t, [])
438 | res m = raise ERROR ("result: not impl.for " ^ string_of m)
440 (*fun result m = (fst o res) m; TODO*)
441 fun result tac = (fst o res) tac;
442 fun creates_assms tac = (snd o res) tac;
444 fun insert_assumptions tac ctxt = ContextC.insert_assumptions (creates_assms tac) ctxt
446 fun for_specify (Add_Find _) = true
447 | for_specify (Add_Given _) = true
448 | for_specify (Add_Relation _) = true
449 | for_specify (Del_Find _) = true
450 | for_specify (Del_Given _) = true
451 | for_specify (Del_Relation _) = true
452 | for_specify Model_Problem = true
453 | for_specify (Refine_Problem _) = true
454 | for_specify (Refine_Tacitly _) = true
455 | for_specify (Specify_Method _) = true
456 | for_specify (Specify_Problem _) = true
457 | for_specify (Specify_Theory _) = true
458 | for_specify _ = false
460 fun for_specify' (Add_Find' _) = true
461 | for_specify' (Add_Given' _) = true
462 | for_specify' (Add_Relation' _) = true
463 | for_specify' (Del_Find' _) = true
464 | for_specify' (Del_Given' _) = true
465 | for_specify' (Del_Relation' _) = true
466 | for_specify' (Model_Problem' _) = true
467 | for_specify' (Refine_Problem' _) = true
468 | for_specify' (Refine_Tacitly' _) = true
469 | for_specify' (Specify_Method' _) = true
470 | for_specify' (Specify_Problem' _) = true
471 | for_specify' (Specify_Theory' _) = true
472 | for_specify' _ = false