1 (* Title: "MathEngBasic/tactic.sml"
2 Author: Walther Neuper 170121
3 (c) due to copyright terms
5 Tactics; tac_ for interaction with frontend, input for internal use.
7 Regular expression for search:
8 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
14 Add_Find' of TermC.as_string * Model_Def.i_model
15 | Add_Given' of TermC.as_string * Model_Def.i_model
16 | Add_Relation' of TermC.as_string * Model_Def.i_model
17 (*RM*)| Del_Find' of TermC.as_string | Del_Given' of TermC.as_string | Del_Relation' of TermC.as_string
18 | Model_Problem' of Problem.id * Model_Def.i_model * Model_Def.i_model
19 | Refine_Problem' of Problem.id * (Model_Def.i_model * Pre_Conds_Def.T)
20 | Refine_Tacitly' of Problem.id * Problem.id * ThyC.id * MethodC.id * Model_Def.i_model
21 | Specify_Method' of MethodC.id * Model_Def.o_model * Model_Def.i_model
22 | Specify_Problem' of Problem.id * (bool * (Model_Def.i_model * Pre_Conds_Def.T))
23 | Specify_Theory' of ThyC.id
24 (* ^^^^^--------------------- for specify-phase, for solve-phase ---------------------vvvvv*)
25 | Apply_Method' of MethodC.id * term option * Istate_Def.T * Proof.context
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 * Celem.result
29 | Derive' of Rule_Set.T
32 | Or_to_List' of term * term
33 | Rewrite' of ThyC.id * Rewrite_Ord.id * Rule_Set.T * bool * ThmC.T * term * Celem.result
34 | Rewrite_Inst' of ThyC.id * Rewrite_Ord.id * Rule_Set.T * bool * subst * ThmC.T * term * Celem.result
35 | Rewrite_Set' of ThyC.id * bool * Rule_Set.T * term * Celem.result
36 | Rewrite_Set_Inst' of ThyC.id * bool * subst * Rule_Set.T * term * Celem.result
37 | Subproblem' of References_Def.T * Model_Def.o_model * term * Model_Def.form_model * Proof.context * term
38 | Substitute' of Rewrite_Ord.function * Rule_Set.T * Subst.as_eqs * term * term
39 (*RM*)| Tac_ of theory * string * string * string
41 | End_Detail' of Celem.result
42 | Begin_Trans' of term | End_Trans' of Celem.result
45 val string_of: Proof.context -> T -> string
48 Add_Find of TermC.as_string | Add_Given of TermC.as_string
49 | Add_Relation of TermC.as_string
50 | Del_Find of TermC.as_string | Del_Given of TermC.as_string | Del_Relation of TermC.as_string
52 | Refine_Problem of Problem.id
53 | Refine_Tacitly of Problem.id
54 | Specify_Method of MethodC.id
55 | Specify_Problem of Problem.id
56 | Specify_Theory of ThyC.id
57 (* ^^^^^--------------------- for specify-phase, for solve-phase ---------------------vvvvv*)
58 | Apply_Method of MethodC.id
60 | Check_Postcond of Problem.id
61 | Check_elementwise of TermC.as_string
62 | Derive of Rule_Set.id
67 | Rewrite_Inst of Subst.input * ThmC.T
68 | Rewrite_Set of Rule_Set.id
69 | Rewrite_Set_Inst of Subst.input * Rule_Set.id
70 | Subproblem of ThyC.id * Problem.id
71 | Substitute of Subst.input
73 | Take of TermC.as_string
75 | Begin_Trans | End_Trans
79 val subst_adapt_to_type: Proof.context -> subst_input -> Subst.T
81 val input_to_string : Proof.context -> input -> string
82 val tac2IDstr : input -> string
83 val is_empty : input -> bool
85 val eq_tac : input * input -> bool
86 val is_rewtac : input -> bool
87 val is_rewset : input -> bool
88 val rls_of : input -> Rule_Set.id
89 val rule2tac : Proof.context -> Env.T -> Rule.rule -> input
90 val applicable : Proof.context -> string -> Rule_Set.T -> term -> input ->input list
91 val for_specify: input -> bool
93 val input_from_T : Proof.context -> T -> input
94 val result : Proof.context -> T -> term
95 val creates_assms: Proof.context -> T -> term list
96 val insert_assumptions: T -> Proof.context -> Proof.context
97 val for_specify': T -> bool
101 structure Tactic(**): TACTIC(**) =
105 (** conversion from input-terms to terms in \<open>Calc.T\<close> **)
107 A Tactic are input with string-arguments;
108 while parsing these require \<open>adapt_to_type\<close> for \<open>Calc.T\<close>.
110 type subst_input = string list
111 val dummyT = TFree ("'a", ["HOL.type"]);
113 fun subst_adapt_to_type ctxt subst = (subst
114 |> map (ParseC.term_opt ctxt)
116 |> map TermC.isapair2pair (*replace by HOLogic.strip_tuple etc*)
117 |> map (apfst HOLogic.dest_string)
118 |> map (apfst (fn str => (TermC.mk_Free (str, dummyT))))
119 |> map (fn (t1, t2) =>
120 (ParseC.adapt_term_to_type ctxt t1, ParseC.adapt_term_to_type ctxt t2)))
121 handle TERM _ => raise TERM ("Tactic.subst_adapt_to_type: wrong argument " ^ strs2str' subst, [])
124 (** tactics for user at front-end **)
127 Add_Find of TermC.as_string | Add_Given of TermC.as_string | Add_Relation of TermC.as_string
128 | Del_Find of TermC.as_string | Del_Given of TermC.as_string | Del_Relation of TermC.as_string
130 | Refine_Problem of Problem.id
131 | Refine_Tacitly of Problem.id
132 | Specify_Method of MethodC.id
133 | Specify_Problem of Problem.id
134 | Specify_Theory of ThyC.id
135 (* ^^^^^--------------------- for specify-phase, for solve-phase ---------------------vvvvv*)
136 | Apply_Method of MethodC.id
137 | Calculate of string
138 | Check_Postcond of Problem.id
139 | Check_elementwise of TermC.as_string
140 | Derive of Rule_Set.id
145 | Rewrite_Inst of Subst.input * ThmC.T
146 | Rewrite_Set of Rule_Set.id
147 | Rewrite_Set_Inst of Subst.input * Rule_Set.id
148 | Subproblem of ThyC.id * Problem.id
149 | Substitute of Subst.input
150 (*RM*)| Tac of string
151 | Take of TermC.as_string
153 | Begin_Trans | End_Trans
156 fun input_to_string ctxt ma = case ma of
157 Model_Problem => "Model_Problem "
158 | Refine_Tacitly pblID => "Refine_Tacitly " ^ strs2str pblID
159 | Refine_Problem pblID => "Refine_Problem " ^ strs2str pblID
160 | Add_Given cterm' => "Add_Given " ^ cterm'
161 | Del_Given cterm' => "Del_Given " ^ cterm'
162 | Add_Find cterm' => "Add_Find " ^ cterm'
163 | Del_Find cterm' => "Del_Find " ^ cterm'
164 | Add_Relation cterm' => "Add_Relation " ^ cterm'
165 | Del_Relation cterm' => "Del_Relation " ^ cterm'
167 | Specify_Theory domID => "Specify_Theory " ^ quote domID
168 | Specify_Problem pblID => "Specify_Problem " ^ strs2str pblID
169 | Specify_Method metID => "Specify_Method " ^ strs2str metID
170 | Apply_Method metID => "Apply_Method " ^ strs2str metID
171 | Check_Postcond pblID => "Check_Postcond " ^ strs2str pblID
172 | Free_Solve => "Free_Solve"
174 | Rewrite_Inst (subs, (id, thm)) => "Rewrite_Inst " ^
175 (pair2str (subs2str subs, spair2str (id, thm |> Thm.prop_of |> UnparseC.term ctxt)))
176 | Rewrite (id, thm) => "Rewrite " ^
177 spair2str (id, thm |> Thm.prop_of |> UnparseC.term ctxt)
178 | Rewrite_Set_Inst (subs, rls) =>
179 "Rewrite_Set_Inst " ^ pair2str (subs2str subs, quote rls)
180 | Rewrite_Set rls => "Rewrite_Set " ^ quote rls
181 | Begin_Trans => "Begin_Trans"
182 | End_Trans => "End_Trans"
183 | End_Detail => "End_Detail"
184 | Derive rls' => "Derive " ^ rls'
185 | Calculate op_ => "Calculate " ^ op_
186 | Substitute sube => "Substitute " ^ Subst.string_eqs_to_string sube
188 | Take cterm' => "Take " ^ quote cterm'
189 | Subproblem (domID, pblID) => "Subproblem " ^ pair2str (domID, strs2str pblID)
191 | Check_elementwise cterm'=> "Check_elementwise " ^ quote cterm'
192 | Or_to_List => "Or_to_List "
194 | Empty_Tac => "Empty_Tac"
195 (*RM*)| Tac string => "Tac " ^ string(*RM*)
196 | End_Proof' => "input End_Proof'";
198 fun tac2IDstr ma = case ma of
199 Model_Problem => "Model_Problem"
200 | Refine_Tacitly _ => "Refine_Tacitly"
201 | Refine_Problem _ => "Refine_Problem"
202 | Add_Given _ => "Add_Given"
203 | Del_Given _ => "Del_Given"
204 | Add_Find _ => "Add_Find"
205 | Del_Find _ => "Del_Find"
206 | Add_Relation _ => "Add_Relation"
207 | Del_Relation _ => "Del_Relation"
209 | Specify_Theory _ => "Specify_Theory"
210 | Specify_Problem _ => "Specify_Problem"
211 | Specify_Method _ => "Specify_Method"
212 | Apply_Method _ => "Apply_Method"
213 | Check_Postcond _ => "Check_Postcond"
214 | Free_Solve => "Free_Solve"
216 | Rewrite_Inst _ => "Rewrite_Inst"
217 | Rewrite _ => "Rewrite"
218 | Rewrite_Set_Inst _ => "Rewrite_Set_Inst"
219 | Rewrite_Set _ => "Rewrite_Set"
220 | Derive _ => "Derive "
221 | Calculate _ => "Calculate "
222 | Substitute _ => "Substitute"
225 | Subproblem _ => "Subproblem"
227 | Check_elementwise _ => "Check_elementwise"
228 | Or_to_List => "Or_to_List "
230 | Empty_Tac => "Empty_Tac"
232 | End_Proof' => "End_Proof'"
233 | _ => "input_to_string not impl. for ?!";
235 fun is_empty input = case input of Empty_Tac => true | _ => false
237 fun eq_tac (Rewrite (id1, _), Rewrite (id2, _)) = id1 = id2
238 | eq_tac (Rewrite_Inst (_, (id1, _)), Rewrite_Inst (_, (id2, _))) = id1 = id2
239 | eq_tac (Rewrite_Set id1, Rewrite_Set id2) = id1 = id2
240 | eq_tac (Rewrite_Set_Inst (_, id1), Rewrite_Set_Inst (_, id2)) = id1 = id2
241 | eq_tac (Calculate id1, Calculate id2) = id1 = id2
244 fun is_rewset (Rewrite_Set_Inst _) = true
245 | is_rewset (Rewrite_Set _) = true
246 | is_rewset _ = false;
247 fun is_rewtac (Rewrite _) = true
248 | is_rewtac (Rewrite_Inst _) = true
249 | is_rewtac input = is_rewset input;
252 fun rls_of (Rewrite_Set_Inst (_, rls)) = rls
253 | rls_of (Rewrite_Set rls) = rls
254 | rls_of input = raise ERROR ("rls_of: called with input \"" ^ tac2IDstr input ^ "\"");
256 fun rule2tac ctxt _ (Rule.Eval (opID, _)) =
257 Calculate (get_calc_prog_id ctxt opID)
258 | rule2tac _ [] (Rule.Thm thm'') = Rewrite thm''
259 | rule2tac ctxt subst (Rule.Thm thm'') =
260 Rewrite_Inst (Subst.T_to_input ctxt subst, thm'')
261 | rule2tac _ [] (Rule.Rls_ rls) = Rewrite_Set (Rule_Set.id rls)
262 | rule2tac ctxt subst (Rule.Rls_ rls) =
263 Rewrite_Set_Inst (Subst.T_to_input ctxt subst, (Rule_Set.id rls))
264 | rule2tac ctxt _ rule =
265 raise ERROR ("rule2tac: called with \"" ^ Rule.to_string ctxt rule ^ "\"");
267 (* try if a rewrite-rule is applicable to a given formula;
268 in case of rule-sets (recursivley) collect all _atomic_ rewrites *)
269 fun try_rew ctxt ((_, ro) : Rewrite_Ord.T) asm_rls (subst : subst) f (thm' as Rule.Thm (_, thm)) =
270 if Auto_Prog.contains_bdv thm
271 then case Rewrite.rewrite_inst_ ctxt ro asm_rls false subst thm f of
272 SOME _ => [rule2tac ctxt subst thm']
274 else (case Rewrite.rewrite_ ctxt ro asm_rls false thm f of
275 SOME _ => [rule2tac ctxt [] thm']
277 | try_rew ctxt _ _ _ f (cal as Rule.Eval c) =
278 (case Eval.adhoc_thm ctxt c f of
279 SOME _ => [rule2tac ctxt [] cal]
281 | try_rew ctxt _ _ _ f (cal as Rule.Cal1 c) =
282 (case Eval.adhoc_thm ctxt c f of
283 SOME _ => [rule2tac ctxt [] cal]
285 | try_rew thy _ _ subst f (Rule.Rls_ rls) = filter_appl_rews thy subst f rls
286 | try_rew _ _ _ _ _ _ = raise ERROR "try_rew: uncovered case"
287 and filter_appl_rews thy subst f (Rule_Def.Repeat {rew_ord = ro, asm_rls, rules, ...}) =
288 distinct eq_tac (flat (map (try_rew thy ro asm_rls subst f) rules))
289 | filter_appl_rews thy subst f (Rule_Set.Sequence {rew_ord = ro, asm_rls, rules,...}) =
290 distinct eq_tac (flat (map (try_rew thy ro asm_rls subst f) rules))
291 | filter_appl_rews _ _ _ (Rule_Set.Rrls _) = []
292 | filter_appl_rews _ _ _ _ = raise ERROR "filter_appl_rews: uncovered case"
294 (* decide if a tactic is applicable to a given formula;
295 in case of Rewrite_Set* go down to _atomic_ rewrite-tactics *)
296 fun applicable ctxt _ _ f (Calculate scrID) =
297 try_rew ctxt Rewrite_Ord.empty Rule_Set.empty [] f
298 (Rule.Eval (get_calc ctxt scrID |> snd))
299 | applicable ctxt ro asm_rls f (Rewrite thm'') =
300 try_rew ctxt (ro, get_rew_ord ctxt ro) asm_rls [] f (Rule.Thm thm'')
301 | applicable ctxt ro asm_rls f (Rewrite_Inst (subs, thm'')) =
302 try_rew ctxt (ro, get_rew_ord ctxt ro) asm_rls
303 (subst_adapt_to_type ctxt subs) f (Rule.Thm thm'')
305 | applicable ctxt _ _ f (Rewrite_Set rls') =
306 filter_appl_rews ctxt [] f (get_rls ctxt rls')
307 | applicable ctxt _ _ f (Rewrite_Set_Inst (subs, rls')) =
308 filter_appl_rews ctxt (subst_adapt_to_type ctxt subs) f (get_rls ctxt rls')
309 | applicable ctxt _ _ _ tac =
310 (tracing ("### applicable: not impl. for tac = '" ^ input_to_string ctxt tac ^ "'"); []);
313 (** tactics for internal use **)
316 Add_Find' of TermC.as_string * Model_Def.i_model | Add_Given' of TermC.as_string * Model_Def.i_model
317 | Add_Relation' of TermC.as_string * Model_Def.i_model (* for Step.do_next *)
318 (*RM*)| Del_Find' of TermC.as_string | Del_Given' of TermC.as_string | Del_Relation' of TermC.as_string
319 | Model_Problem' of (* first step in specify-phase *)
320 Problem.id * (* id in the Know_Store *)
321 Model_Def.i_model * (* the model for the Problem *)
322 Model_Def.i_model (* the model for the method *)
323 | Refine_Problem' of Problem.id * (Model_Def.i_model * Pre_Conds_Def.T)
325 Problem.id * (* the original id in the Know_Store *)
326 Problem.id * (* the id of the refined Problem *)
327 ThyC.id * (* the id of the refined theory *)
328 MethodC.id * (* the id of the refined MethodC *)
329 Model_Def.i_model (* RM 9.03: remains [] for Model_Problem recognizing its activation *)
330 | Specify_Method' of MethodC.id * Model_Def.o_model * Model_Def.i_model
331 | Specify_Problem' of Problem.id *
332 (bool * (* all preconditions evaluate to True *)
333 (Model_Def.i_model * (* the model checked for the input id *)
334 Pre_Conds_Def.T)) (* individual preconditions marked true/false *)
335 | Specify_Theory' of ThyC.id
336 (* ^^^^^--------------------- for specify-phase, for solve-phase ---------------------vvvvv*)
337 | Apply_Method' of (* last step in specifu-phse, switch to solve-phase *)
338 MethodC.id * (* id in the Know_Store *)
339 term option * (* first formula in the (sub-)Problem TODO: rm option *)
340 Istate_Def.T * (* for starting the Program *)
341 Proof.context (* for starting the Program *)
342 | Calculate' of ThyC.id * string * term * (term * ThmC.T)
343 | Check_Postcond' of (* last step in solving a (sub-)Problem *)
344 Problem.id * (* id of the Problem to be checked *)
345 term (* return value of the program *)
346 | Check_elementwise' of(* DEPRECATED, made idle for Calc.T in df00a2b5c4cc *)
347 term * (* the current formula: [x=1,x=...] *)
348 string * (* the pred from Check_elementwise *)
349 Celem.result (* composed from (1) and (2): {x. pred} *)
350 | Derive' of Rule_Set.T(* for Test_Out.embed_deriv *)
353 | Or_to_List' of term * term
354 | Rewrite' of ThyC.id * Rewrite_Ord.id * Rule_Set.T * bool * ThmC.T * term * Celem.result
355 | Rewrite_Inst' of ThyC.id * Rewrite_Ord.id * Rule_Set.T * bool * subst * ThmC.T * term * Celem.result
356 | Rewrite_Set' of ThyC.id * bool * Rule_Set.T * term * Celem.result
357 | Rewrite_Set_Inst' of ThyC.id * bool * subst * Rule_Set.T * term * Celem.result
358 | Subproblem' of (* switch from solve-phase to specify-phase *)
359 References_Def.T * (* specification of the SubProblem *)
360 (Model_Def.o_model) * (* original model, filled in associate Subproblem' *)
361 term * (* headline of calc-head, filled -"- *)
362 Model_Def.form_model * (* string list from arguments of the calling Program*)
363 Proof.context * (* for the specify-phase *)
364 term (* Subproblem (thyID, pbl) OR CAS_Cmd *)
365 | Substitute' of (* substitute variables (TODO: from the context) *)
366 Rewrite_Ord.function *(* for re-calculation *)
367 Rule_Set.T * (* for re-calculation *)
368 Subst.as_eqs * (* the substitution: terms of type bool *)
369 term * (* to be substituted into *)
370 term (* resulting from the substitution *)
371 (*RM*)| Tac_ of theory * string * string * string
373 | End_Detail' of Celem.result (* for intermediate steps into Rewrite_Set *)
374 | Begin_Trans' of term (* for intermediate steps into Rewrite_Set *)
375 | End_Trans' of Celem.result (* for intermediate steps into Rewrite_Set *)
378 fun string_of ctxt ma = case ma of
379 Model_Problem' (pblID, _, _) => "Model_Problem' " ^ strs2str pblID
380 | Refine_Tacitly'(p, prefin, domID, metID, _) => "Refine_Tacitly' (" ^ strs2str p ^ ", " ^
381 strs2str prefin ^ ", " ^ domID ^ ", " ^ strs2str metID ^ ", pbl-itms)"
382 | Refine_Problem' _ => "Refine_Problem' (" ^ (*matchs2str ms*)"..." ^ ")"
383 | Add_Given' _ => "Add_Given' "(*^cterm'*)
384 | Del_Given' _ => "Del_Given' "(*^cterm'*)
385 | Add_Find' _ => "Add_Find' "(*^cterm'*)
386 | Del_Find' _ => "Del_Find' "(*^cterm'*)
387 | Add_Relation' _ => "Add_Relation' "(*^cterm'*)
388 | Del_Relation' _ => "Del_Relation' "(*^cterm'*)
390 | Specify_Theory' domID => "Specify_Theory' " ^ quote domID
391 | Specify_Problem' (pI, (ok, _)) => "Specify_Problem' " ^
392 spair2str (strs2str pI, spair2str (bool2str ok, spair2str ("itms2str_ itms", "items2str where_")))
393 | Specify_Method' (pI, oris, _) => "Specify_Method' (" ^
394 MethodC.id_to_string pI ^ ", " ^ Model_Def.o_model_to_string ctxt oris ^ ", )"
396 | Apply_Method' (metID, _, _, _) => "Apply_Method' " ^ strs2str metID
397 | Check_Postcond' (pblID, scval) => "Check_Postcond' " ^
398 (spair2str (strs2str pblID, UnparseC.term ctxt scval))
400 | Free_Solve' => "Free_Solve'"
402 | Rewrite_Inst' (*subs,thm'*) _ => "Rewrite_Inst' "(*^(pair2str (subs2str subs, spair2str thm'))*)
403 | Rewrite' _(*thm'*) => "Rewrite' "(*^(spair2str thm')*)
404 | Rewrite_Set_Inst' _(*subs,thm'*) => "Rewrite_Set_Inst' "(*^(pair2str (subs2str subs, quote rls))*)
405 | Rewrite_Set' (thy', pasm, rls', f, (f', asm)) => "Rewrite_Set' (" ^ thy' ^ ", " ^ bool2str pasm ^
406 ", " ^ Rule_Set.id rls' ^ ", " ^ UnparseC.term ctxt f ^ ",(" ^
407 UnparseC.term ctxt f' ^ ", " ^ UnparseC.terms ctxt asm ^ "))"
408 | End_Detail' _ => "End_Detail' xxx"
410 | Derive' rls => "Derive' " ^ Rule_Set.id rls
411 | Calculate' _ => "Calculate' "
412 | Substitute' _ => "Substitute' "(*^(subs2str subs)*)
414 | Take' _(*cterm'*) => "Take' "(*^(quote cterm' )*)
415 | Subproblem' _(*(spec, oris, _, _, _, pbl_form)*) =>
416 "Subproblem' "(*^(pair2str (domID, strs2str ,))*)
418 | Empty_Tac_ => "Empty_Tac_"
419 | Tac_ (_, form, id, result) => "Tac_ (thy," ^ form ^ ", " ^ id ^ ", " ^ result ^ ")"
421 | Begin_Trans' _ => "Begin_Trans' xxx"
422 | End_Trans' _ => "End_Trans' xxx"
423 | End_Proof'' => "End_Trans' xxx"
424 | _ => "string_of not impl. for arg";
426 fun input_from_T _ (Refine_Tacitly' (pI, _, _, _, _)) = Refine_Tacitly pI
427 | input_from_T _ (Model_Problem' (_, _, _)) = Model_Problem
428 | input_from_T _ (Add_Given' (t, _)) = Add_Given t
429 | input_from_T _ (Add_Find' (t, _)) = Add_Find t
430 | input_from_T _ (Add_Relation' (t, _)) = Add_Relation t
432 | input_from_T _ (Specify_Theory' dI) = Specify_Theory dI
433 | input_from_T _ (Specify_Problem' (dI, _)) = Specify_Problem dI
434 | input_from_T _ (Specify_Method' (dI, _, _)) = Specify_Method dI
436 | input_from_T _ (Rewrite' (_, _, _, _, thm, _, _)) = Rewrite thm
437 | input_from_T ctxt (Rewrite_Inst' (_, _, _, _, sub, thm, _, _)) =
438 Rewrite_Inst (Subst.T_to_input ctxt sub, thm)
440 | input_from_T _ (Rewrite_Set' (_, _, rls, _, _)) = Rewrite_Set (Rule_Set.id rls)
441 | input_from_T ctxt (Rewrite_Set_Inst' (_, _, sub, rls, _, _)) =
442 Rewrite_Set_Inst (Subst.T_to_input ctxt sub, Rule_Set.id rls)
444 | input_from_T _ (Calculate' (_, op_, _, _)) = Calculate (op_)
445 | input_from_T _ (Check_elementwise' (_, pred, _)) = Check_elementwise pred
447 | input_from_T _ (Or_to_List' _) = Or_to_List
448 | input_from_T ctxt (Take' term) = Take (UnparseC.term ctxt term)
449 | input_from_T ctxt (Substitute' (_, _, subte, _, _)) = Substitute (Subst.eqs_to_input ctxt subte)
450 | input_from_T _ (Tac_ (_, _, id, _)) = Tac id
452 | input_from_T _ (Subproblem' ((domID, pblID, _), _, _, _,_ ,_)) = Subproblem (domID, pblID)
453 | input_from_T _ (Check_Postcond' (pblID, _)) = Check_Postcond pblID
454 | input_from_T _ Empty_Tac_ = Empty_Tac
455 | input_from_T ctxt m = raise ERROR (": not impl. for " ^ string_of ctxt m);
457 fun res _ (Rewrite_Inst' (_ , _, _, _, _, _, _, res)) = res
458 | res _ (Rewrite' (_, _, _, _, _, _, res)) = res
459 | res _ (Rewrite_Set_Inst' (_, _, _, _, _, res)) = res
460 | res _ (Rewrite_Set' (_, _, _, _, res)) = res
461 | res _ (Calculate' (_, _, _, (t, _))) = (t, [])
462 | res _ (Check_elementwise' (_, _, res)) = res
463 | res _ (Subproblem' (_, _, _, _, _, t)) = (t, [])
464 | res _ (Take' t) = (t, [])
465 | res _ (Substitute' (_, _, _, _, t)) = (t, [])
466 | res _ (Or_to_List' (_, t)) = (t, [])
467 | res ctxt m = raise ERROR ("result: not impl.for " ^ string_of ctxt m)
469 fun result ctxt tac = (fst o (res ctxt)) tac;
470 fun creates_assms ctxt tac = (snd o (res ctxt)) tac;
472 (*fun insert_assumptions tac ctxt = ContextC.insert_assumptions (creates_assms tac) ctxt*)
473 fun insert_assumptions tac ctxt = ContextC.insert_assumptions (creates_assms ctxt tac) ctxt
475 fun for_specify (Add_Find _) = true
476 | for_specify (Add_Given _) = true
477 | for_specify (Add_Relation _) = true
478 | for_specify (Del_Find _) = true
479 | for_specify (Del_Given _) = true
480 | for_specify (Del_Relation _) = true
481 | for_specify Model_Problem = true
482 | for_specify (Refine_Problem _) = true
483 | for_specify (Refine_Tacitly _) = true
484 | for_specify (Specify_Method _) = true
485 | for_specify (Specify_Problem _) = true
486 | for_specify (Specify_Theory _) = true
487 | for_specify _ = false
489 fun for_specify' (Add_Find' _) = true
490 | for_specify' (Add_Given' _) = true
491 | for_specify' (Add_Relation' _) = true
492 | for_specify' (Del_Find' _) = true
493 | for_specify' (Del_Given' _) = true
494 | for_specify' (Del_Relation' _) = true
495 | for_specify' (Model_Problem' _) = true
496 | for_specify' (Refine_Problem' _) = true
497 | for_specify' (Refine_Tacitly' _) = true
498 | for_specify' (Specify_Method' _) = true
499 | for_specify' (Specify_Problem' _) = true
500 | for_specify' (Specify_Theory' _) = true
501 | for_specify' _ = false