(* Title:  Tactics; tac_ for interaction with frontend, input for internal use.

   Author: Walther Neuper 170121

   (c) due to copyright terms

regular expression for search:

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

*)

signature TACTIC =

sig

  datatype T =

    Add_Find' of TermC.as_string * Model_Def.i_model | Add_Given' of TermC.as_string * Model_Def.i_model 

  | Add_Relation' of TermC.as_string * Model_Def.i_model

(*RM*)| Del_Find' of TermC.as_string | Del_Given' of TermC.as_string | Del_Relation' of TermC.as_string

  | Model_Problem' of Problem.id * Model_Def.i_model * Model_Def.i_model

  | Refine_Problem' of Problem.id * (Model_Def.i_model * Pre_Conds_Def.T)

  | Refine_Tacitly' of Problem.id * Problem.id * ThyC.id * MethodC.id * Model_Def.i_model

  | Specify_Method' of MethodC.id * Model_Def.o_model * Model_Def.i_model

  | Specify_Problem' of Problem.id * (bool * (Model_Def.i_model * Pre_Conds_Def.T))

  | Specify_Theory' of ThyC.id

  (* ^^^^^--------------------- for specify-phase, for solve-phase ---------------------vvvvv*)

  | Apply_Method' of MethodC.id * term option * Istate_Def.T * Proof.context

  | Calculate' of ThyC.id * string * term * (term * ThmC.T)

  | Check_Postcond' of Problem.id * term

  | Check_elementwise' of term * TermC.as_string * Celem.result

  | Derive' of Rule_Set.T    

  | Empty_Tac_

  | Free_Solve'

  | Or_to_List' of term * term

  | Rewrite' of ThyC.id * Rewrite_Ord.id * Rule_Set.T * bool * ThmC.T * term * Celem.result

  | Rewrite_Inst' of ThyC.id * Rewrite_Ord.id * Rule_Set.T * bool * subst * ThmC.T * term * Celem.result

  | Rewrite_Set' of ThyC.id * bool * Rule_Set.T * term * Celem.result

  | Rewrite_Set_Inst' of ThyC.id * bool * subst * Rule_Set.T * term * Celem.result

  | Subproblem' of References_Def.T * Model_Def.o_model * term * Model_Def.form_model * Proof.context * term

  | Substitute' of Rewrite_Ord.function * Rule_Set.T * Subst.as_eqs * term * term

(*RM*)| Tac_ of theory * string * string * string

  | Take' of term

  | End_Detail' of Celem.result

  | Begin_Trans' of term | End_Trans' of Celem.result

  | End_Proof''

  val string_of: T -> string

  datatype input =

    Add_Find of TermC.as_string | Add_Given of TermC.as_string

  | Add_Relation of TermC.as_string

  | Del_Find of TermC.as_string | Del_Given of TermC.as_string | Del_Relation of TermC.as_string

  | Model_Problem

  | Refine_Problem of Problem.id

  | Refine_Tacitly of Problem.id

  | Specify_Method of MethodC.id

  | Specify_Problem of Problem.id

  | Specify_Theory of ThyC.id

  (* ^^^^^--------------------- for specify-phase, for solve-phase ---------------------vvvvv*)

  | Apply_Method of MethodC.id

  | Calculate of string

  | Check_Postcond of Problem.id

  | Check_elementwise of TermC.as_string

  | Derive of Rule_Set.id

  | Empty_Tac

  | Free_Solve

  | Or_to_List

  | Rewrite of ThmC.T

  | Rewrite_Inst of Subst.input * ThmC.T

  | Rewrite_Set of Rule_Set.id

  | Rewrite_Set_Inst of Subst.input * Rule_Set.id

  | Subproblem of ThyC.id * Problem.id

  | Substitute of Subst.input

(*RM*)| Tac of string

  | Take of TermC.as_string

  | End_Detail

  | Begin_Trans | End_Trans

  | End_Proof';

  val input_to_string : input -> string

  val tac2IDstr : input -> string

  val is_empty : input -> bool

  val eq_tac : input * input -> bool

  val is_rewtac : input -> bool

  val is_rewset : input -> bool

  val rls_of : input -> Rule_Set.id

  val rule2tac : Proof.context -> Env.T ->  Rule.rule -> input

  val applicable : Proof.context -> string -> Rule_Set.T -> term -> input ->input list

  val for_specify: input -> bool

  val input_from_T : T -> input

  val result : T -> term

  val creates_assms: T -> term list

  val insert_assumptions: T -> Proof.context -> Proof.context

  val for_specify': T -> bool

end

(**)

structure Tactic(**): TACTIC(**) =

struct

(**)

(** tactics for user at front-end **)

datatype input =

    Add_Find of TermC.as_string | Add_Given of TermC.as_string | Add_Relation of TermC.as_string

  | Del_Find of TermC.as_string | Del_Given of TermC.as_string | Del_Relation of TermC.as_string

  | Model_Problem

  | Refine_Problem of Problem.id

  | Refine_Tacitly of Problem.id

  | Specify_Method of MethodC.id

  | Specify_Problem of Problem.id

  | Specify_Theory of ThyC.id

  (* ^^^^^--------------------- for specify-phase, for solve-phase ---------------------vvvvv*)

  | Apply_Method of MethodC.id

  | Calculate of string

  | Check_Postcond of Problem.id

  | Check_elementwise of TermC.as_string

  | Derive of Rule_Set.id

  | Empty_Tac

  | Free_Solve

  | Or_to_List

  | Rewrite of ThmC.T

  | Rewrite_Inst of Subst.input * ThmC.T

  | Rewrite_Set of Rule_Set.id

  | Rewrite_Set_Inst of Subst.input * Rule_Set.id

  | Subproblem of ThyC.id * Problem.id

  | Substitute of Subst.input

(*RM*)| Tac of string

  | Take of TermC.as_string

  | End_Detail

  | Begin_Trans | End_Trans

  | End_Proof';

fun input_to_string ma = case ma of

    Model_Problem           => "Model_Problem "

  | Refine_Tacitly pblID    => "Refine_Tacitly " ^ strs2str pblID 

  | Refine_Problem pblID    => "Refine_Problem " ^ strs2str pblID 

  | Add_Given cterm'        => "Add_Given " ^ cterm'

  | Del_Given cterm'        => "Del_Given " ^ cterm'

  | Add_Find cterm'         => "Add_Find " ^ cterm'

  | Del_Find cterm'         => "Del_Find " ^ cterm'

  | Add_Relation cterm'     => "Add_Relation " ^ cterm'

  | Del_Relation cterm'     => "Del_Relation " ^ cterm'

  | Specify_Theory domID    => "Specify_Theory " ^ quote domID

  | Specify_Problem pblID   => "Specify_Problem " ^ strs2str pblID

  | Specify_Method metID    => "Specify_Method " ^ strs2str metID

  | Apply_Method metID      => "Apply_Method " ^ strs2str metID

  | Check_Postcond pblID    => "Check_Postcond " ^ strs2str pblID

  | Free_Solve              => "Free_Solve"

  | Rewrite_Inst (subs, (id, thm)) =>

    "Rewrite_Inst " ^ (pair2str (subs2str subs, spair2str (id, thm |> Thm.prop_of |> UnparseC.term)))

  | Rewrite (id, thm) => "Rewrite " ^ spair2str (id, thm |> Thm.prop_of |> UnparseC.term)

  | Rewrite_Set_Inst (subs, rls) => 

    "Rewrite_Set_Inst " ^ pair2str (subs2str subs, quote rls)

  | Rewrite_Set rls         => "Rewrite_Set " ^ quote rls

  | Begin_Trans              => "Begin_Trans"

  | End_Trans              => "End_Trans"

  | End_Detail              => "End_Detail"

  | Derive rls'             => "Derive " ^ rls'

  | Calculate op_           => "Calculate " ^ op_

  | Substitute sube         => "Substitute " ^ Subst.string_eqs_to_string sube	     

  | Take cterm'             => "Take " ^ quote cterm'

  | Subproblem (domID, pblID) => "Subproblem " ^ pair2str (domID, strs2str pblID)

  | Check_elementwise cterm'=> "Check_elementwise " ^ quote cterm'

  | Or_to_List              => "Or_to_List "

  | Empty_Tac               => "Empty_Tac"

(*RM*)| Tac string              => "Tac " ^ string(*RM*)

  | End_Proof'              => "input End_Proof'";

fun tac2IDstr ma = case ma of

    Model_Problem => "Model_Problem"

  | Refine_Tacitly _ => "Refine_Tacitly"

  | Refine_Problem _ => "Refine_Problem"

  | Add_Given _ => "Add_Given"

  | Del_Given _ => "Del_Given"

  | Add_Find _ => "Add_Find"

  | Del_Find _ => "Del_Find"

  | Add_Relation _ => "Add_Relation"

  | Del_Relation _ => "Del_Relation"

  | Specify_Theory _ => "Specify_Theory"

  | Specify_Problem _ => "Specify_Problem"

  | Specify_Method _ => "Specify_Method"

  | Apply_Method _ => "Apply_Method"

  | Check_Postcond _ => "Check_Postcond"

  | Free_Solve => "Free_Solve"

  | Rewrite_Inst _ => "Rewrite_Inst"

  | Rewrite _ => "Rewrite"

  | Rewrite_Set_Inst _ => "Rewrite_Set_Inst"

  | Rewrite_Set _ => "Rewrite_Set"

  | Derive _ => "Derive "

  | Calculate _ => "Calculate "

  | Substitute _ => "Substitute" 

  | Take _ => "Take"

  | Subproblem _ => "Subproblem"

  | Check_elementwise _ => "Check_elementwise"

  | Or_to_List => "Or_to_List "

  | Empty_Tac => "Empty_Tac"

  | Tac _ => "Tac "

  | End_Proof' => "End_Proof'"

  | _ => "input_to_string not impl. for ?!";

fun is_empty input = case input of Empty_Tac => true | _ => false

fun eq_tac (Rewrite (id1, _), Rewrite (id2, _)) = id1 = id2

  | eq_tac (Rewrite_Inst (_, (id1, _)), Rewrite_Inst (_, (id2, _))) = id1 = id2

  | eq_tac (Rewrite_Set id1, Rewrite_Set id2) = id1 = id2

  | eq_tac (Rewrite_Set_Inst (_, id1), Rewrite_Set_Inst (_, id2)) = id1 = id2

  | eq_tac (Calculate id1, Calculate id2) = id1 = id2

  | eq_tac _ = false

fun is_rewset (Rewrite_Set_Inst _) = true

  | is_rewset (Rewrite_Set _) = true 

  | is_rewset _ = false;

fun is_rewtac (Rewrite _) = true

  | is_rewtac (Rewrite_Inst _) = true

  | is_rewtac input = is_rewset input;

fun rls_of (Rewrite_Set_Inst (_, rls)) = rls

  | rls_of (Rewrite_Set rls) = rls

  | rls_of input = raise ERROR ("rls_of: called with input \"" ^ tac2IDstr input ^ "\"");

fun rule2tac ctxt _ (Rule.Eval (opID, _)) = Calculate (assoc_calc (Proof_Context.theory_of ctxt) opID)

  | rule2tac _ [] (Rule.Thm thm'') = Rewrite thm''

  | rule2tac _ subst (Rule.Thm thm'') = 

    Rewrite_Inst (Subst.T_to_input subst, thm'')

  | rule2tac _ [] (Rule.Rls_ rls) = Rewrite_Set (Rule_Set.id rls)

  | rule2tac _ subst (Rule.Rls_ rls) = 

    Rewrite_Set_Inst (Subst.T_to_input subst, (Rule_Set.id rls))

  | rule2tac _ _ rule = 

    raise ERROR ("rule2tac: called with \"" ^ Rule.to_string rule ^ "\"");

(* try if a rewrite-rule is applicable to a given formula; 

   in case of rule-sets (recursivley) collect all _atomic_ rewrites *) 

fun try_rew ctxt ((_, ro) : Rewrite_Ord.T) erls (subst : subst) f (thm' as Rule.Thm (_, thm)) =

    if Auto_Prog.contains_bdv thm

    then case Rewrite.rewrite_inst_ ctxt ro erls false subst thm f of

	    SOME _ => [rule2tac ctxt subst thm']

	  | NONE => []

    else (case Rewrite.rewrite_ ctxt ro erls false thm f of

	    SOME _ => [rule2tac ctxt [] thm']

	  | NONE => [])

  | try_rew ctxt _ _ _ f (cal as Rule.Eval c) = 

    (case Eval.adhoc_thm (Proof_Context.theory_of ctxt) c f of

	    SOME _ => [rule2tac ctxt [] cal]

    | NONE => [])

  | try_rew ctxt _ _ _ f (cal as Rule.Cal1 c) = 

    (case Eval.adhoc_thm (Proof_Context.theory_of ctxt) c f of

	      SOME _ => [rule2tac ctxt [] cal]

      | NONE => [])

  | try_rew thy _ _ subst f (Rule.Rls_ rls) = filter_appl_rews thy subst f rls

  | try_rew _ _ _ _ _ _ = raise ERROR "try_rew: uncovered case"

and filter_appl_rews thy subst f (Rule_Def.Repeat {rew_ord = ro, erls, rules, ...}) = 

    distinct eq_tac (flat (map (try_rew thy ro erls subst f) rules))

  | filter_appl_rews thy subst f (Rule_Set.Sequence {rew_ord = ro, erls, rules,...}) = 

    distinct eq_tac (flat (map (try_rew thy ro erls subst f) rules))

  | filter_appl_rews _ _ _ (Rule_Set.Rrls _) = []

  | filter_appl_rews _ _ _ _ = raise ERROR "filter_appl_rews: uncovered case"

(* decide if a tactic is applicable to a given formula; 

   in case of Rewrite_Set* go down to _atomic_ rewrite-tactics *)

fun applicable ctxt _ _ f (Calculate scrID) =

    try_rew ctxt Rewrite_Ord.empty Rule_Set.empty [] f 

      (Rule.Eval (assoc_calc' (Proof_Context.theory_of ctxt) scrID |> snd))

  | applicable ctxt ro erls f (Rewrite thm'') =

    try_rew ctxt (ro, assoc_rew_ord (Proof_Context.theory_of ctxt) ro) erls [] f (Rule.Thm thm'')

  | applicable ctxt ro erls f (Rewrite_Inst (subs, thm'')) =

    try_rew ctxt (ro, assoc_rew_ord (Proof_Context.theory_of ctxt) ro) erls 

      (Subst.T_from_input ctxt subs) f (Rule.Thm thm'')

  | applicable thy _ _ f (Rewrite_Set rls') =

    filter_appl_rews thy [] f (assoc_rls rls')

  | applicable thy _ _ f (Rewrite_Set_Inst (subs, rls')) =

    filter_appl_rews thy (Subst.T_from_input thy subs) f (assoc_rls rls')

  | applicable _ _ _ _ tac = 

    (tracing ("### applicable: not impl. for tac = '" ^ input_to_string tac ^ "'"); []);

(** tactics for internal use **)

  datatype T =

    Add_Find' of TermC.as_string * Model_Def.i_model | Add_Given' of TermC.as_string * Model_Def.i_model 

  | Add_Relation' of TermC.as_string * Model_Def.i_model (* for Step.do_next    *)

(*RM*)| Del_Find' of TermC.as_string | Del_Given' of TermC.as_string | Del_Relation' of TermC.as_string

  | Model_Problem' of  (* first step in specify-phase                        *)

      Problem.id *     (* id in the Know_Store                               *)

      Model_Def.i_model * (* the model for the Problem                          *)

      Model_Def.i_model   (* the model for the method                           *)

  | Refine_Problem' of Problem.id * (Model_Def.i_model * Pre_Conds_Def.T)

  | Refine_Tacitly' of                                                      

      Problem.id *       (* the original id in the Know_Store                *)

      Problem.id *       (* the id of the refined Problem                    *)

      ThyC.id *          (* the id of the refined theory                     *)

      MethodC.id *        (* the id of the refined MethodC                     *)

      Model_Def.i_model     (* RM 9.03: remains [] for Model_Problem recognizing its activation *)

  | Specify_Method' of MethodC.id * Model_Def.o_model * Model_Def.i_model

  | Specify_Problem' of Problem.id * 

      (bool *                  (* all preconditions evaluate to True         *)

        (Model_Def.i_model *      (* the model checked for the input id         *)

          Pre_Conds_Def.T)) (* individual preconditions marked true/false *)

  | Specify_Theory' of ThyC.id

  (* ^^^^^--------------------- for specify-phase, for solve-phase ---------------------vvvvv*)

  | Apply_Method' of   (* last step in specifu-phse, switch to solve-phase   *)

      MethodC.id *      (* id in the Know_Store                               *)

      term option *    (* first formula in the (sub-)Problem TODO: rm option *)           

      Istate_Def.T *   (* for starting the Program                           *)

      Proof.context    (* for starting the Program                           *)

  | Calculate' of ThyC.id * string * term * (term * ThmC.T)

  | Check_Postcond' of   (* last step in solving a (sub-)Problem             *)

      Problem.id *       (* id of the Problem to be checked                  *)

      term               (* return value of the program                      *)

  | Check_elementwise' of(* DEPRECATED, made idle for Calc.T in df00a2b5c4cc *)

      term *             (* the current formula: [x=1,x=...]                 *)

      string *           (* the pred from Check_elementwise                  *)

      Celem.result       (* composed from (1) and (2): {x. pred}             *)

  | Derive' of Rule_Set.T(* for Test_Out.embed_deriv                         *)

  | Empty_Tac_

  | Free_Solve'

  | Or_to_List' of term * term

  | Rewrite' of ThyC.id * Rewrite_Ord.id * Rule_Set.T * bool * ThmC.T * term * Celem.result

  | Rewrite_Inst' of ThyC.id * Rewrite_Ord.id * Rule_Set.T * bool * subst * ThmC.T * term * Celem.result

  | Rewrite_Set' of ThyC.id * bool * Rule_Set.T * term * Celem.result

  | Rewrite_Set_Inst' of ThyC.id * bool * subst * Rule_Set.T * term * Celem.result

  | Subproblem' of       (* switch from solve-phase to specify-phase         *)

      References_Def.T *           (* specification of the SubProblem                  *)

  		(Model_Def.o_model) * (* original model, filled in associate Subproblem'  *)

  		term *             (* headline of calc-head, filled -"-                *)

  		Model_Def.form_model *       (* string list from arguments of the calling Program*)

      Proof.context *    (* for the specify-phase                            *)

  		term               (* Subproblem (thyID, pbl) OR CAS_Cmd               *)  

  | Substitute' of       (* substitute variables (TODO: from the context)    *)    

      Rewrite_Ord.function *(* for re-calculation                               *)

      Rule_Set.T *       (* for re-calculation                               *)

      Subst.as_eqs *     (* the substitution: terms of type bool             *)

      term *             (* to be substituted into                           *)

      term               (* resulting from the substitution                  *)

(*RM*)| Tac_ of theory * string * string * string

  | Take' of term

  | End_Detail' of Celem.result (* for intermediate steps into Rewrite_Set   *)

  | Begin_Trans' of term        (* for intermediate steps into Rewrite_Set   *)

  | End_Trans' of Celem.result  (* for intermediate steps into Rewrite_Set   *)

  | End_Proof''

fun string_of ma = case ma of

    Model_Problem' (pblID, _, _) => "Model_Problem' " ^ strs2str pblID

  | Refine_Tacitly'(p, prefin, domID, metID, _) => "Refine_Tacitly' (" ^ strs2str p ^ ", " ^

    strs2str prefin ^ ", " ^ domID ^ ", " ^ strs2str metID ^ ", pbl-itms)"

  | Refine_Problem' _ => "Refine_Problem' (" ^ (*matchs2str ms*)"..." ^ ")"

  | Add_Given' _ => "Add_Given' "(*^cterm'*)

  | Del_Given' _ => "Del_Given' "(*^cterm'*)

  | Add_Find' _ => "Add_Find' "(*^cterm'*)

  | Del_Find' _ => "Del_Find' "(*^cterm'*)

  | Add_Relation' _ => "Add_Relation' "(*^cterm'*)

  | Del_Relation' _ => "Del_Relation' "(*^cterm'*)

  | Specify_Theory' domID => "Specify_Theory' " ^ quote domID

  | Specify_Problem' (pI, (ok, _)) =>  "Specify_Problem' " ^ 

    spair2str (strs2str pI, spair2str (bool2str ok, spair2str ("itms2str_ itms", "items2str pre")))

  | Specify_Method' (pI, oris, _) => "Specify_Method' (" ^ 

    MethodC.id_to_string pI ^ ", " ^ Model_Def.o_model_to_string oris ^ ", )"

  | Apply_Method' (metID, _, _, _) => "Apply_Method' " ^ strs2str metID

  | Check_Postcond' (pblID, scval) => "Check_Postcond' " ^

      (spair2str (strs2str pblID, UnparseC.term scval))

  | Free_Solve' => "Free_Solve'"

  | Rewrite_Inst' (*subs,thm'*) _ => "Rewrite_Inst' "(*^(pair2str (subs2str subs, spair2str thm'))*)

  | Rewrite' _(*thm'*) => "Rewrite' "(*^(spair2str thm')*)

  | Rewrite_Set_Inst' _(*subs,thm'*) => "Rewrite_Set_Inst' "(*^(pair2str (subs2str subs, quote rls))*)

  | Rewrite_Set' (thy', pasm, rls', f, (f', asm)) => "Rewrite_Set' (" ^ thy' ^ ", " ^ bool2str pasm ^

    ", " ^ Rule_Set.id rls' ^ ", " ^ UnparseC.term f ^ ",(" ^ UnparseC.term f' ^ ", " ^ UnparseC.terms asm ^ "))"

  | End_Detail' _ => "End_Detail' xxx"

  | Derive' rls => "Derive' " ^ Rule_Set.id rls

  | Calculate'  _ => "Calculate' "

  | Substitute' _ => "Substitute' "(*^(subs2str subs)*)    

  | Take' _(*cterm'*) => "Take' "(*^(quote cterm'	)*)

  | Subproblem' _(*(spec, oris, _, _, _, pbl_form)*) => 

    "Subproblem' "(*^(pair2str (domID, strs2str ,))*)

  | Empty_Tac_ => "Empty_Tac_"

  | Tac_ (_, form, id, result) => "Tac_ (thy," ^ form ^ ", " ^ id ^ ", " ^ result ^ ")"

  | Begin_Trans' _ => "Begin_Trans' xxx"

  | End_Trans' _ => "End_Trans' xxx"

  | End_Proof'' => "End_Trans' xxx"

  | _  => "string_of not impl. for arg";

fun input_from_T (Refine_Tacitly' (pI, _, _, _, _)) = Refine_Tacitly pI

  | input_from_T (Model_Problem' (_, _, _)) = Model_Problem

  | input_from_T (Add_Given' (t, _)) = Add_Given t

  | input_from_T (Add_Find' (t, _)) = Add_Find t

  | input_from_T (Add_Relation' (t, _)) = Add_Relation t

  | input_from_T (Specify_Theory' dI) = Specify_Theory dI

  | input_from_T (Specify_Problem' (dI, _)) = Specify_Problem dI

  | input_from_T (Specify_Method' (dI, _, _)) = Specify_Method dI

  | input_from_T (Rewrite' (_, _, _, _, thm, _, _)) = Rewrite thm

  | input_from_T (Rewrite_Inst' (_, _, _, _, sub, thm, _, _)) = Rewrite_Inst (Subst.T_to_input sub, thm)

  | input_from_T (Rewrite_Set' (_, _, rls, _, _)) = Rewrite_Set (Rule_Set.id rls)

  | input_from_T (Rewrite_Set_Inst' (_, _, sub, rls, _, _)) = 

    Rewrite_Set_Inst (Subst.T_to_input sub, Rule_Set.id rls)

  | input_from_T (Calculate' (_, op_, _, _)) = Calculate (op_)

  | input_from_T (Check_elementwise' (_, pred, _)) = Check_elementwise pred

  | input_from_T (Or_to_List' _) = Or_to_List

  | input_from_T (Take' term) = Take (UnparseC.term term)

  | input_from_T (Substitute' (_, _, subte, _, _)) = Substitute (Subst.eqs_to_input subte) 

  | input_from_T (Tac_ (_, _, id, _)) = Tac id

  | input_from_T (Subproblem' ((domID, pblID, _), _, _, _,_ ,_)) = Subproblem (domID, pblID)

  | input_from_T (Check_Postcond' (pblID, _)) = Check_Postcond pblID

  | input_from_T Empty_Tac_ = Empty_Tac

  | input_from_T m = raise ERROR (": not impl. for "^(string_of m));

fun res (Rewrite_Inst' (_ , _, _, _, _, _, _, res)) = res

  | res (Rewrite' (_, _, _, _, _, _, res)) = res

  | res (Rewrite_Set_Inst' (_, _, _, _, _, res)) = res

  | res (Rewrite_Set' (_, _, _, _, res)) = res

  | res (Calculate' (_, _, _, (t, _))) = (t, [])

  | res (Check_elementwise' (_, _, res)) = res

  | res (Subproblem' (_, _, _, _, _, t)) = (t, [])

  | res (Take' t) = (t, [])

  | res (Substitute' (_, _, _, _, t)) = (t, [])

  | res (Or_to_List' (_,  t)) = (t, [])

  | res m = raise ERROR ("result: not impl.for " ^ string_of m)

(*fun result m = (fst o res) m; TODO*)

fun result tac = (fst o res) tac;

fun creates_assms tac = (snd o res) tac;

fun insert_assumptions tac ctxt  = ContextC.insert_assumptions (creates_assms tac) ctxt

fun for_specify (Add_Find _) = true

  | for_specify (Add_Given _) = true

  | for_specify (Add_Relation _) = true

  | for_specify (Del_Find _) = true

  | for_specify (Del_Given _) = true

  | for_specify (Del_Relation _) = true

  | for_specify Model_Problem  = true

  | for_specify (Refine_Problem _) = true

  | for_specify (Refine_Tacitly _) = true

  | for_specify (Specify_Method _) = true

  | for_specify (Specify_Problem _) = true

  | for_specify (Specify_Theory _) = true

  | for_specify _ = false

fun for_specify' (Add_Find' _) = true

  | for_specify' (Add_Given' _) = true

  | for_specify' (Add_Relation' _) = true

  | for_specify' (Del_Find' _) = true

  | for_specify' (Del_Given' _) = true

  | for_specify' (Del_Relation' _) = true

  | for_specify' (Model_Problem' _) = true

  | for_specify' (Refine_Problem' _) = true

  | for_specify' (Refine_Tacitly' _) = true

  | for_specify' (Specify_Method' _) = true

  | for_specify' (Specify_Problem' _) = true

  | for_specify' (Specify_Theory' _) = true

  | for_specify' _ = false

(**)end(**)