wneuper@59571: (* Title:  Tactics; tac_ for interaction with frontend, input for internal use.
wneuper@59304:    Author: Walther Neuper 170121
wneuper@59304:    (c) due to copyright terms
wneuper@59304: 
wneuper@59304: regular expression for search:
wneuper@59304: 
walther@59812: 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
wneuper@59304: 
wneuper@59304: *)
wneuper@59298: signature TACTIC =
wneuper@59298: sig
walther@59846:   datatype T =
walther@59846:     Add_Find' of Rule.cterm' * Model.itm list | Add_Given' of Rule.cterm' * Model.itm list 
walther@59846:   | Add_Relation' of Rule.cterm' * Model.itm list
walther@59846:   | Apply_Method' of Celem.metID * term option * Istate_Def.T * Proof.context
walther@59846: 
walther@59846:   | Begin_Sequ' | Begin_Trans' of term
walther@59846:   | Split_And' of term | Split_Or' of term | Split_Intersect' of term
walther@59846:   | Conclude_And' of term | Conclude_Or' of term | Collect_Trues' of term
walther@59846:   | End_Sequ' | End_Trans' of Selem.result
walther@59846:   | End_Ruleset' of term | End_Intersect' of term | End_Proof''
walther@59846: 
walther@59846:   | CAScmd' of term
walther@59846:   | Calculate' of Rule.theory' * string * term * (term * Celem.thm')
walther@59846:   | Check_Postcond' of Celem.pblID * term
walther@59846:   | Check_elementwise' of term * Rule.cterm' * Selem.result
walther@59846:   | Del_Find' of Rule.cterm' | Del_Given' of Rule.cterm' | Del_Relation' of Rule.cterm'
walther@59846: 
walther@59850:   | Derive' of Rule_Set.rls      
walther@59850:   | Detail_Set' of Rule.theory' * bool * Rule_Set.rls * term * Selem.result
walther@59850:   | Detail_Set_Inst' of Rule.theory' * bool * Rule.subst * Rule_Set.rls * term * Selem.result
walther@59846:   | End_Detail' of Selem.result
walther@59846: 
walther@59846:   | Empty_Tac_
walther@59846:   | Free_Solve'
walther@59846: 
walther@59846:   | Init_Proof' of Rule.cterm' list * Celem.spec
walther@59846:   | Model_Problem' of Celem.pblID * Model.itm list * Model.itm list
walther@59846:   | Or_to_List' of term * term
walther@59846:   | Refine_Problem' of Celem.pblID * (Model.itm list * (bool * term) list)
walther@59846:   | Refine_Tacitly' of Celem.pblID * Celem.pblID * Rule.domID * Celem.metID * Model.itm list
walther@59846: 
walther@59850:   | Rewrite' of Rule.theory' * Rule_Def.rew_ord' * Rule_Set.rls * bool * Celem.thm'' * term * Selem.result
walther@59850:   | Rewrite_Inst' of Rule.theory' * Rule_Def.rew_ord' * Rule_Set.rls * bool * Rule.subst * Celem.thm'' * term * Selem.result
walther@59850:   | Rewrite_Set' of Rule.theory' * bool * Rule_Set.rls * term * Selem.result
walther@59850:   | Rewrite_Set_Inst' of Rule.theory' * bool * Rule.subst * Rule_Set.rls * term * Selem.result
walther@59846: 
walther@59846:   | Specify_Method' of Celem.metID * Model.ori list * Model.itm list
walther@59846:   | Specify_Problem' of Celem.pblID * (bool * (Model.itm list * (bool * term) list))
walther@59846:   | Specify_Theory' of Rule.domID
walther@59846:   | Subproblem' of
walther@59846:       Celem.spec * Model.ori list *
walther@59846:       term *          (* CAScmd, e.g. "solve (-1 + x = 0, x)" *)
walther@59846:       Selem.fmz_ *    (* either input to root-probl.  or derived from prog. in ???  *)
walther@59846:       (*Istate.T *       ?       *)
walther@59846:       Proof.context * (* derived from prog. in ???  *)
walther@59846:       term            (* ?UNUSED, e.g."Subproblem\n (''Test'',\n  ??.\<^const>String.char.Char ''LINEAR'' ''univariate'' ''equation''\n   ''test'')" *)
walther@59850:   | Substitute' of Rule_Def.rew_ord_ * Rule_Set.rls * Selem.subte * term * term
walther@59846:   | Tac_ of theory * string * string * string
walther@59846:   | Take' of term
walther@59812:   val string_of: T -> string
walther@59741: 
walther@59846:   datatype input =
walther@59846:     Add_Find of Rule.cterm' | Add_Given of Rule.cterm' | Add_Relation of Rule.cterm'
walther@59846:   | Apply_Assumption of Rule.cterm' list
walther@59846:   | Apply_Method of Celem.metID
walther@59846:   (*/--- TODO: re-design ? -----------------------------------------------------------------\*)
walther@59846:   | Begin_Sequ | Begin_Trans
walther@59846:   | Split_And | Split_Or | Split_Intersect
walther@59846:   | Conclude_And | Conclude_Or | Collect_Trues
walther@59846:   | End_Sequ | End_Trans
walther@59846:   | End_Ruleset | End_Subproblem | End_Intersect | End_Proof'
walther@59846:   (*\--- TODO: re-design ? -----------------------------------------------------------------/*)
walther@59846:   | CAScmd of Rule.cterm'
walther@59846:   | Calculate of string
walther@59846:   | Check_Postcond of Celem.pblID
walther@59846:   | Check_elementwise of Rule.cterm'
walther@59846:   | Del_Find of Rule.cterm' | Del_Given of Rule.cterm' | Del_Relation of Rule.cterm'
walther@59846: 
walther@59850:   | Derive of Rule_Set.rls'
walther@59850:   | Detail_Set of Rule_Set.rls'
walther@59850:   | Detail_Set_Inst of Selem.subs * Rule_Set.rls'
walther@59846:   | End_Detail
walther@59846: 
walther@59846:   | Empty_Tac
walther@59846:   | Free_Solve
walther@59846: 
walther@59846:   | Init_Proof of Rule.cterm' list * Celem.spec
walther@59846:   | Model_Problem
walther@59846:   | Or_to_List
walther@59846:   | Refine_Problem of Celem.pblID
walther@59846:   | Refine_Tacitly of Celem.pblID
walther@59846: 
walther@59846:   | Rewrite of Celem.thm''
walther@59846:   | Rewrite_Inst of Selem.subs * Celem.thm''
walther@59850:   | Rewrite_Set of Rule_Set.rls'
walther@59850:   | Rewrite_Set_Inst of Selem.subs * Rule_Set.rls'
walther@59846: 
walther@59846:   | Specify_Method of Celem.metID
walther@59846:   | Specify_Problem of Celem.pblID
walther@59846:   | Specify_Theory of Rule.domID
walther@59846:   | Subproblem of Rule.domID * Celem.pblID
walther@59846: 
walther@59846:   | Substitute of Selem.sube
walther@59846:   | Tac of string
walther@59846:   | Take of Rule.cterm' | Take_Inst of Rule.cterm'
walther@59846:   val input_to_string : input -> string
walther@59812:   val tac2IDstr : input -> string
walther@59844:   val is_empty : input -> bool
wneuper@59302: 
walther@59728:   val eq_tac : input * input -> bool
walther@59728:   val is_rewtac : input -> bool
walther@59728:   val is_rewset : input -> bool
walther@59850:   val rls_of : input -> Rule_Set.rls'
walther@59728:   val rule2tac : theory -> (term * term) list ->  Rule.rule -> input
walther@59704:   val input_from_T : T -> input
walther@59728:   val result : T -> term
walther@59728:   val creates_assms: T -> term list
walther@59728:   val insert_assumptions: T -> Proof.context -> Proof.context
walther@59749:   val for_specify: input -> bool
walther@59749:   val for_specify': T -> bool
walther@59735: 
wneuper@59310: (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
wneuper@59310:   (* NONE *)
walther@59785: (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
wneuper@59310:   (* NONE *)
walther@59785: ( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
wneuper@59298: 
wneuper@59310: (*----- unused code, kept as hints to design ideas ---------------------------------------------*)
wneuper@59310:   (* NONE *)
wneuper@59298: end
wneuper@59298: 
walther@59728: (**)
wneuper@59571: structure Tactic(**): TACTIC(**) =
wneuper@59298: struct
walther@59728: (**)
wneuper@59298: 
walther@59846: (* tactics for user at front-end.
walther@59846:    input propagates the construction of the calc-tree;
walther@59846:    there are
walther@59846:    (a) 'specsteps' for the specify-phase, and others for the solve-phase
walther@59846:    (b) those of the solve-phase are 'initac's and others;
walther@59846:        initacs start with a formula different from the preceding formula.
walther@59846:    see 'type tac_' for the internal representation of tactics
walther@59846: *)
walther@59846: datatype input =
walther@59846:     Add_Find of Rule.cterm' | Add_Given of Rule.cterm' | Add_Relation of Rule.cterm'
walther@59846:   | Apply_Assumption of Rule.cterm' list
walther@59846:   | Apply_Method of Celem.metID
walther@59846:     (* creates an "istate" in PblObj.env; in case of "implicit_take" 
walther@59846:       creates a formula at ((lev_on o lev_dn) p, Frm) and in this "ppobj.loc"
walther@59846:       a "SOME istate" at fst of "loc".
walther@59846:       As each step (in the solve-phase) has a resulting formula (at the front-end)
walther@59846:       Apply_Method also does the 1st step in the script (an "initac") if there is no "implicit_take" *)  
walther@59846:   (*/--- TODO: re-design ? -----------------------------------------------------------------\*)
walther@59846:   | Begin_Sequ | Begin_Trans
walther@59846:   | Split_And | Split_Or | Split_Intersect
walther@59846:   | Conclude_And | Conclude_Or | Collect_Trues
walther@59846:   | End_Sequ | End_Trans
walther@59846:   | End_Ruleset | End_Subproblem (* WN0509 drop *) | End_Intersect | End_Proof'
walther@59846:   (*\--- TODO: re-design ? -----------------------------------------------------------------/*)
walther@59846:   | CAScmd of Rule.cterm'
walther@59846:   | Calculate of string
walther@59846:   | Check_Postcond of Celem.pblID
walther@59846:   | Check_elementwise of Rule.cterm'
walther@59846:   | Del_Find of Rule.cterm' | Del_Given of Rule.cterm' | Del_Relation of Rule.cterm'
wneuper@59302: 
walther@59850:   | Derive of Rule_Set.rls'                 (* WN0509 drop *)
walther@59850:   | Detail_Set of Rule_Set.rls'             (* WN0509 drop *)
walther@59850:   | Detail_Set_Inst of Selem.subs * Rule_Set.rls' (* WN0509 drop *)
walther@59846:   | End_Detail                     (* WN0509 drop *)
walther@59846: 
walther@59846:   | Empty_Tac
walther@59846:   | Free_Solve
walther@59846: 
walther@59846:   | Init_Proof of Rule.cterm' list * Celem.spec
walther@59846:   | Model_Problem
walther@59846:   | Or_to_List
walther@59846:   | Refine_Problem of Celem.pblID
walther@59846:   | Refine_Tacitly of Celem.pblID
walther@59846: 
walther@59846:    (* rewrite-tactics can transport a (thmID, thm) to and (!) from the java-front-end
walther@59846:      because there all the thms are present with both (thmID, thm)
walther@59846:      (where user-views can show both or only one of (thmID, thm)),
walther@59846:      and thm is created from ThmID by assoc_thm'' when entering isabisac *)
walther@59846:   | Rewrite of Celem.thm''
walther@59846:   | Rewrite_Inst of Selem.subs * Celem.thm''
walther@59850:   | Rewrite_Set of Rule_Set.rls'
walther@59850:   | Rewrite_Set_Inst of Selem.subs * Rule_Set.rls'
walther@59846: 
walther@59846:   | Specify_Method of Celem.metID
walther@59846:   | Specify_Problem of Celem.pblID
walther@59846:   | Specify_Theory of Rule.domID
walther@59846:   | Subproblem of Rule.domID * Celem.pblID (* WN0509 drop *)
walther@59846: 
walther@59846:   | Substitute of Selem.sube
walther@59846:   | Tac of string               (* WN0509 drop *)
walther@59846:   | Take of Rule.cterm' | Take_Inst of Rule.cterm'
walther@59846: 
walther@59846: fun input_to_string ma = case ma of
walther@59846:     Init_Proof (ppc, spec)  => 
walther@59846:       "Init_Proof "^(pair2str (strs2str ppc, Celem.spec2str spec))
walther@59846:   | Model_Problem           => "Model_Problem "
walther@59846:   | Refine_Tacitly pblID    => "Refine_Tacitly " ^ strs2str pblID 
walther@59846:   | Refine_Problem pblID    => "Refine_Problem " ^ strs2str pblID 
walther@59846:   | Add_Given cterm'        => "Add_Given " ^ cterm'
walther@59846:   | Del_Given cterm'        => "Del_Given " ^ cterm'
walther@59846:   | Add_Find cterm'         => "Add_Find " ^ cterm'
walther@59846:   | Del_Find cterm'         => "Del_Find " ^ cterm'
walther@59846:   | Add_Relation cterm'     => "Add_Relation " ^ cterm'
walther@59846:   | Del_Relation cterm'     => "Del_Relation " ^ cterm'
walther@59846: 
walther@59846:   | Specify_Theory domID    => "Specify_Theory " ^ quote domID
walther@59846:   | Specify_Problem pblID   => "Specify_Problem " ^ strs2str pblID
walther@59846:   | Specify_Method metID    => "Specify_Method " ^ strs2str metID
walther@59846:   | Apply_Method metID      => "Apply_Method " ^ strs2str metID
walther@59846:   | Check_Postcond pblID    => "Check_Postcond " ^ strs2str pblID
walther@59846:   | Free_Solve              => "Free_Solve"
walther@59846: 
walther@59846:   | Rewrite_Inst (subs, (id, thm)) =>
walther@59846:     "Rewrite_Inst " ^ (pair2str (subs2str subs, spair2str (id, thm |> Thm.prop_of |> Rule.term2str)))
walther@59846:   | Rewrite (id, thm) => "Rewrite " ^ spair2str (id, thm |> Thm.prop_of |> Rule.term2str)
walther@59846:   | Rewrite_Set_Inst (subs, rls) => 
walther@59846:     "Rewrite_Set_Inst " ^ pair2str (subs2str subs, quote rls)
walther@59846:   | Rewrite_Set rls         => "Rewrite_Set " ^ quote rls
walther@59846:   | Detail_Set rls          => "Detail_Set " ^ quote rls
walther@59846:   | Detail_Set_Inst (subs, rls) =>  "Detail_Set_Inst " ^ pair2str (subs2str subs, quote rls)
walther@59846:   | End_Detail              => "End_Detail"
walther@59846:   | Derive rls'             => "Derive " ^ rls' 
walther@59846:   | Calculate op_           => "Calculate " ^ op_ 
walther@59846:   | Substitute sube         => "Substitute " ^ Selem.sube2str sube	     
walther@59846:   | Apply_Assumption ct's   => "Apply_Assumption " ^ strs2str ct's
walther@59846: 
walther@59846:   | Take cterm'             => "Take " ^ quote cterm'
walther@59846:   | Take_Inst cterm'        => "Take_Inst " ^ quote cterm'
walther@59846:   | Subproblem (domID, pblID) => "Subproblem " ^ pair2str (domID, strs2str pblID)
walther@59846:   | End_Subproblem          => "End_Subproblem"
walther@59846:   | CAScmd cterm'           => "CAScmd " ^ quote cterm'
walther@59846: 
walther@59846:   | Check_elementwise cterm'=> "Check_elementwise " ^ quote cterm'
walther@59846:   | Or_to_List              => "Or_to_List "
walther@59846:   | Collect_Trues           => "Collect_Trues"
walther@59846: 
walther@59846:   | Empty_Tac               => "Empty_Tac"
walther@59846:   | Tac string              => "Tac " ^ string
walther@59846:   | End_Proof'              => "input End_Proof'"
walther@59846:   | _                       => "input_to_string not impl. for ?!";
walther@59846: 
walther@59846: fun tac2IDstr ma = case ma of
walther@59846:     Model_Problem => "Model_Problem"
walther@59846:   | Refine_Tacitly _ => "Refine_Tacitly"
walther@59846:   | Refine_Problem _ => "Refine_Problem"
walther@59846:   | Add_Given _ => "Add_Given"
walther@59846:   | Del_Given _ => "Del_Given"
walther@59846:   | Add_Find _ => "Add_Find"
walther@59846:   | Del_Find _ => "Del_Find"
walther@59846:   | Add_Relation _ => "Add_Relation"
walther@59846:   | Del_Relation _ => "Del_Relation"
walther@59846: 
walther@59846:   | Specify_Theory _ => "Specify_Theory"
walther@59846:   | Specify_Problem _ => "Specify_Problem"
walther@59846:   | Specify_Method _ => "Specify_Method"
walther@59846:   | Apply_Method _ => "Apply_Method"
walther@59846:   | Check_Postcond _ => "Check_Postcond"
walther@59846:   | Free_Solve => "Free_Solve"
walther@59846: 
walther@59846:   | Rewrite_Inst _ => "Rewrite_Inst"
walther@59846:   | Rewrite _ => "Rewrite"
walther@59846:   | Rewrite_Set_Inst _ => "Rewrite_Set_Inst"
walther@59846:   | Rewrite_Set _ => "Rewrite_Set"
walther@59846:   | Detail_Set _ => "Detail_Set"
walther@59846:   | Detail_Set_Inst _ => "Detail_Set_Inst"
walther@59846:   | Derive _ => "Derive "
walther@59846:   | Calculate _ => "Calculate "
walther@59846:   | Substitute _ => "Substitute" 
walther@59846:   | Apply_Assumption _ => "Apply_Assumption"
walther@59846: 
walther@59846:   | Take _ => "Take"
walther@59846:   | Take_Inst _ => "Take_Inst"
walther@59846:   | Subproblem _ => "Subproblem"
walther@59846:   | End_Subproblem => "End_Subproblem"
walther@59846:   | CAScmd _ => "CAScmd"
walther@59846: 
walther@59846:   | Check_elementwise _ => "Check_elementwise"
walther@59846:   | Or_to_List => "Or_to_List "
walther@59846:   | Collect_Trues => "Collect_Trues"
walther@59846: 
walther@59846:   | Empty_Tac => "Empty_Tac"
walther@59846:   | Tac _ => "Tac "
walther@59846:   | End_Proof' => "End_Proof'"
walther@59846:   | _ => "input_to_string not impl. for ?!";
walther@59846: 
walther@59846: fun is_empty input = case input of Empty_Tac => true | _ => false
wneuper@59302: 
wneuper@59302: fun eq_tac (Rewrite (id1, _), Rewrite (id2, _)) = id1 = id2
wneuper@59302:   | eq_tac (Rewrite_Inst (_, (id1, _)), Rewrite_Inst (_, (id2, _))) = id1 = id2
wneuper@59302:   | eq_tac (Rewrite_Set id1, Rewrite_Set id2) = id1 = id2
wneuper@59302:   | eq_tac (Rewrite_Set_Inst (_, id1), Rewrite_Set_Inst (_, id2)) = id1 = id2
wneuper@59302:   | eq_tac (Calculate id1, Calculate id2) = id1 = id2
wneuper@59302:   | eq_tac _ = false
wneuper@59302: 
wneuper@59302: fun is_rewset (Rewrite_Set_Inst _) = true
wneuper@59302:   | is_rewset (Rewrite_Set _) = true 
wneuper@59302:   | is_rewset _ = false;
wneuper@59302: fun is_rewtac (Rewrite _) = true
wneuper@59302:   | is_rewtac (Rewrite_Inst _) = true
wneuper@59571:   | is_rewtac input = is_rewset input;
wneuper@59302: 
wneuper@59302: 
wneuper@59302: fun rls_of (Rewrite_Set_Inst (_, rls)) = rls
wneuper@59302:   | rls_of (Rewrite_Set rls) = rls
walther@59846:   | rls_of input = error ("rls_of: called with input \"" ^ tac2IDstr input ^ "\"");
wneuper@59302: 
walther@59773: fun rule2tac thy _ (Rule.Num_Calc (opID, _)) = Calculate (assoc_calc thy opID)
wneuper@59416:   | rule2tac _ [] (Rule.Thm thm'') = Rewrite thm''
wneuper@59416:   | rule2tac _ subst (Rule.Thm thm'') = 
wneuper@59302:     Rewrite_Inst (Selem.subst2subs subst, thm'')
walther@59850:   | rule2tac _ [] (Rule.Rls_ rls) = Rewrite_Set (Rule_Set.id_rls rls)
wneuper@59416:   | rule2tac _ subst (Rule.Rls_ rls) = 
walther@59850:     Rewrite_Set_Inst (Selem.subst2subs subst, (Rule_Set.id_rls rls))
wneuper@59302:   | rule2tac _ _ rule = 
walther@59850:     error ("rule2tac: called with \"" ^ Rule_Set.rule2str rule ^ "\"");
wneuper@59302: 
walther@59846: (* tactics for for internal use, compare "input" for user at the front-end.
walther@59846:   tac_ contains results from check in 'fun applicable_in'.
walther@59846:   This is useful for costly results, e.g. from rewriting;
walther@59846:   however, these results might be changed by Scripts like
walther@59846:       "      eq = (Rewrite_Set ''ansatz_rls'' False) eql;" ^
walther@59846:       "      eq = (Rewrite_Set equival_trans False) eq;" ^
walther@59846:   TODO.WN120106 ANALOGOUSLY TO Substitute':
walther@59846:   So tac_ contains the term t the result was calculated from
walther@59846:   in order to compare t with t' possibly changed by "Expr "
walther@59846:   and re-calculate result if t<>t'
walther@59846:   TODO.WN161219: replace *every* cterm' by term
walther@59846: *)
walther@59846:   datatype T =
walther@59846:     Add_Find' of Rule.cterm' * Model.itm list | Add_Given' of Rule.cterm' * Model.itm list 
walther@59846:   | Add_Relation' of Rule.cterm' * Model.itm list
walther@59846:   | Apply_Method' of (* creates the 1st step visible in a (sub-) comprising
walther@59846:                       * tactic Apply_Method metID
walther@59846:                       * formula term                                        *)
walther@59846:       Celem.metID *  (* key for KEStore                                     *)
walther@59846:       term option *  (* the first formula of Calc.T. TODO: rm option        *)           
walther@59846:       Istate_Def.T * (* for the newly started program                       *)
walther@59846:       Proof.context  (* for the newly started program                       *)
walther@59846:   (*/--- TODO: re-design ? -----------------------------------------------------------------\*)
walther@59846:   | Begin_Sequ' | Begin_Trans' of term
walther@59846:   | Split_And' of term | Split_Or' of term | Split_Intersect' of term
walther@59846:   | Conclude_And' of term | Conclude_Or' of term | Collect_Trues' of term
walther@59846:   | End_Sequ' | End_Trans' of Selem.result
walther@59846:   | End_Ruleset' of term | End_Intersect' of term | End_Proof''
walther@59846:   (*\--- TODO: re-design ? -----------------------------------------------------------------/*)
walther@59846:   | CAScmd' of term
walther@59846:   | Calculate' of Rule.theory' * string * term * (term * Celem.thm')
walther@59846:   | Check_Postcond' of Celem.pblID *
walther@59846:     term         (* returnvalue of program in solve *)
walther@59846:   | Check_elementwise' of (* DEPRECATED, made idle for Calc.T in df00a2b5c4cc *)
walther@59846:     term *       (* (1) the current formula: [x=1,x=...]                      *)
walther@59846:     string *     (* (2) the pred from Check_elementwise                       *)
walther@59846:     Selem.result (* (3) composed from (1) and (2): {x. pred}                  *)
walther@59846:   | Del_Find' of Rule.cterm' | Del_Given' of Rule.cterm' | Del_Relation' of Rule.cterm'
wneuper@59302: 
walther@59850:   | Derive' of Rule_Set.rls
walther@59850:   | Detail_Set' of Rule.theory' * bool * Rule_Set.rls * term * Selem.result
walther@59850:   | Detail_Set_Inst' of Rule.theory' * bool * Rule.subst * Rule_Set.rls * term * Selem.result
walther@59846:   | End_Detail' of Selem.result
walther@59846: 
walther@59846:   | Empty_Tac_
walther@59846:   | Free_Solve'
walther@59846: 
walther@59846:   | Init_Proof' of Rule.cterm' list * Celem.spec
walther@59846:   | Model_Problem' of (* first step in specifying   *)
walther@59846:     Celem.pblID *     (* key into KEStore           *)
walther@59846:     Model.itm list *  (* the 'untouched' pbl        *)
walther@59846:     Model.itm list    (* the casually completed met *)
walther@59846:   | Or_to_List' of term * term
walther@59846:   | Refine_Problem' of Celem.pblID * (Model.itm list * (bool * term) list)
walther@59846:   | Refine_Tacitly' of
walther@59846:     Celem.pblID *     (* input                                                                *)
walther@59846:     Celem.pblID *     (* the refined from applicable_in                                       *)
walther@59846:     Rule.domID *      (* from new pbt?! filled in specify                                     *)
walther@59846:     Celem.metID *     (* from new pbt?! filled in specify                                     *)
walther@59846:     Model.itm list    (* drop ! 9.03: remains [] for Model_Problem recognizing its activation *)
walther@59850:   | Rewrite' of Rule.theory' * Rule_Def.rew_ord' * Rule_Set.rls * bool * Celem.thm'' * term * Selem.result
walther@59850:   | Rewrite_Inst' of Rule.theory' * Rule_Def.rew_ord' * Rule_Set.rls * bool * Rule.subst * Celem.thm'' * term * Selem.result
walther@59850:   | Rewrite_Set' of Rule.theory' * bool * Rule_Set.rls * term * Selem.result
walther@59850:   | Rewrite_Set_Inst' of Rule.theory' * bool * Rule.subst * Rule_Set.rls * term * Selem.result
walther@59846: 
walther@59846:   | Specify_Method' of Celem.metID * Model.ori list * Model.itm list
walther@59846:   | Specify_Problem' of Celem.pblID * 
walther@59846:     (bool *                  (* matches	                                  *)
walther@59846:       (Model.itm list *      (* ppc	                                      *)
walther@59846:         (bool * term) list)) (* preconditions marked true/false           *)
walther@59846:   | Specify_Theory' of Rule.domID
walther@59846:   | Subproblem' of
walther@59846:     Celem.spec * 
walther@59846: 		(Model.ori list) *       (* filled in associate Subproblem'           *)
walther@59846: 		term *                   (* filled -"-, headline of calc-head         *)
walther@59846: 		Selem.fmz_ *             (* string list from arguments                *)
walther@59846:     Proof.context *          (* for specify-phase                         *)
walther@59846: 		term                     (* Subproblem (thyID, pbl) OR cascmd         *)  
walther@59846:   | Substitute' of           
walther@59850:     Rule_Def.rew_ord_ *          (* for re-calculation                        *)
walther@59850:     Rule_Set.rls *               (* for re-calculation                        *)
walther@59846:     Selem.subte *            (* the 'substitution': terms of type bool    *)
walther@59846:     term *                   (* to be substituted into                    *)
walther@59846:     term                     (* resulting from the substitution           *)
walther@59846:   | Tac_ of theory * string * string * string
walther@59846:   | Take' of term
walther@59846: 
walther@59846: fun string_of ma = case ma of
walther@59846:     Init_Proof' (ppc, spec)  => "Init_Proof' " ^ pair2str (strs2str ppc, Celem.spec2str spec)
walther@59846:   | Model_Problem' (pblID, _, _) => "Model_Problem' " ^ strs2str pblID
walther@59846:   | Refine_Tacitly'(p, prefin, domID, metID, _) => "Refine_Tacitly' (" ^ strs2str p ^ ", " ^
walther@59846:     strs2str prefin ^ ", " ^ domID ^ ", " ^ strs2str metID ^ ", pbl-itms)"
walther@59846:   | Refine_Problem' _ => "Refine_Problem' (" ^ (*matchs2str ms*)"..." ^ ")"
walther@59846:   | Add_Given' _ => "Add_Given' "(*^cterm'*)
walther@59846:   | Del_Given' _ => "Del_Given' "(*^cterm'*)
walther@59846:   | Add_Find' _ => "Add_Find' "(*^cterm'*)
walther@59846:   | Del_Find' _ => "Del_Find' "(*^cterm'*)
walther@59846:   | Add_Relation' _ => "Add_Relation' "(*^cterm'*)
walther@59846:   | Del_Relation' _ => "Del_Relation' "(*^cterm'*)
walther@59846: 
walther@59846:   | Specify_Theory' domID => "Specify_Theory' " ^ quote domID
walther@59846:   | Specify_Problem' (pI, (ok, _)) =>  "Specify_Problem' " ^ 
walther@59846:     spair2str (strs2str pI, spair2str (bool2str ok, spair2str ("itms2str_ itms", "items2str pre")))
walther@59846:   | Specify_Method' (pI, oris, _) => "Specify_Method' (" ^ 
walther@59846:     Celem.metID2str pI ^ ", " ^ Model.oris2str oris ^ ", )"
walther@59846: 
walther@59846:   | Apply_Method' (metID, _, _, _) => "Apply_Method' " ^ strs2str metID
walther@59846:   | Check_Postcond' (pblID, scval) => "Check_Postcond' " ^
walther@59846:       (spair2str (strs2str pblID, Rule.term2str scval))
walther@59846: 
walther@59846:   | Free_Solve' => "Free_Solve'"
walther@59846: 
walther@59846:   | Rewrite_Inst' (*subs,thm'*) _ => "Rewrite_Inst' "(*^(pair2str (subs2str subs, spair2str thm'))*)
walther@59846:   | Rewrite' _(*thm'*) => "Rewrite' "(*^(spair2str thm')*)
walther@59846:   | Rewrite_Set_Inst' _(*subs,thm'*) => "Rewrite_Set_Inst' "(*^(pair2str (subs2str subs, quote rls))*)
walther@59846:   | Rewrite_Set' (thy', pasm, rls', f, (f', asm)) => "Rewrite_Set' (" ^ thy' ^ "," ^ bool2str pasm ^
walther@59850:     "," ^ Rule_Set.id_rls rls' ^ "," ^ Rule.term2str f ^ ",(" ^ Rule.term2str f' ^ "," ^ Rule.terms2str asm ^ "))"
walther@59846:   | End_Detail' _ => "End_Detail' xxx"
walther@59846:   | Detail_Set' _ => "Detail_Set' xxx"
walther@59846:   | Detail_Set_Inst' _ => "Detail_Set_Inst' xxx"
walther@59846: 
walther@59850:   | Derive' rls => "Derive' " ^ Rule_Set.id_rls rls
walther@59846:   | Calculate'  _ => "Calculate' "
walther@59846:   | Substitute' _ => "Substitute' "(*^(subs2str subs)*)    
walther@59846: 
walther@59846:   | Take' _(*cterm'*) => "Take' "(*^(quote cterm'	)*)
walther@59846:   | Subproblem' _(*(spec, oris, _, _, _, pbl_form)*) => 
walther@59846:     "Subproblem' "(*^(pair2str (domID, strs2str ,))*)
walther@59846:   | CAScmd' _(*cterm'*) => "CAScmd' "(*^(quote cterm')*)
walther@59846: 
walther@59846:   | Empty_Tac_ => "Empty_Tac_"
walther@59846:   | Tac_ (_, form, id, result) => "Tac_ (thy," ^ form ^ "," ^ id ^ "," ^ result ^ ")"
walther@59846:   | _  => "string_of not impl. for arg";
wneuper@59302: 
walther@59704: fun input_from_T (Refine_Tacitly' (pI, _, _, _, _)) = Refine_Tacitly pI
walther@59704:   | input_from_T (Model_Problem' (_, _, _)) = Model_Problem
walther@59704:   | input_from_T (Add_Given' (t, _)) = Add_Given t
walther@59704:   | input_from_T (Add_Find' (t, _)) = Add_Find t
walther@59704:   | input_from_T (Add_Relation' (t, _)) = Add_Relation t
walther@59704:  
walther@59704:   | input_from_T (Specify_Theory' dI) = Specify_Theory dI
walther@59704:   | input_from_T (Specify_Problem' (dI, _)) = Specify_Problem dI
walther@59704:   | input_from_T (Specify_Method' (dI, _, _)) = Specify_Method dI
walther@59704:   
walther@59704:   | input_from_T (Rewrite' (_, _, _, _, thm, _, _)) = Rewrite thm
walther@59704:   | input_from_T (Rewrite_Inst' (_, _, _, _, sub, thm, _, _)) = Rewrite_Inst (Selem.subst2subs sub, thm)
walther@59704: 
walther@59850:   | input_from_T (Rewrite_Set' (_, _, rls, _, _)) = Rewrite_Set (Rule_Set.id_rls rls)
walther@59850:   | input_from_T (Detail_Set' (_, _, rls, _, _)) = Detail_Set (Rule_Set.id_rls rls)
walther@59704: 
walther@59704:   | input_from_T (Rewrite_Set_Inst' (_, _, sub, rls, _, _)) = 
walther@59850:     Rewrite_Set_Inst (Selem.subst2subs sub, Rule_Set.id_rls rls)
walther@59704:   | input_from_T (Detail_Set_Inst' (_, _, sub, rls, _, _)) = 
walther@59850:     Detail_Set_Inst (Selem.subst2subs sub, Rule_Set.id_rls rls)
walther@59704: 
walther@59704:   | input_from_T (Calculate' (_, op_, _, _)) = Calculate (op_)
walther@59704:   | input_from_T (Check_elementwise' (_, pred, _)) = Check_elementwise pred
walther@59704: 
walther@59704:   | input_from_T (Or_to_List' _) = Or_to_List
walther@59704:   | input_from_T (Take' term) = Take (Rule.term2str term)
walther@59704:   | input_from_T (Substitute' (_, _, subte, _, _)) = Substitute (Selem.subte2sube subte) 
walther@59704:   | input_from_T (Tac_ (_, _, id, _)) = Tac id
walther@59704: 
walther@59704:   | input_from_T (Subproblem' ((domID, pblID, _), _, _, _,_ ,_)) = Subproblem (domID, pblID)
walther@59704:   | input_from_T (Check_Postcond' (pblID, _)) = Check_Postcond pblID
walther@59704:   | input_from_T Empty_Tac_ = Empty_Tac
walther@59846:   | input_from_T m = raise ERROR (": not impl. for "^(string_of m));
walther@59704: 
walther@59728: fun res (Rewrite_Inst' (_ , _, _, _, _, _, _, res)) = res
walther@59728:   | res (Rewrite' (_, _, _, _, _, _, res)) = res
walther@59728:   | res (Rewrite_Set_Inst' (_, _, _, _, _, res)) = res
walther@59728:   | res (Rewrite_Set' (_, _, _, _, res)) = res
walther@59728:   | res (Calculate' (_, _, _, (t, _))) = (t, [])
walther@59728:   | res (Check_elementwise' (_, _, res)) = res
walther@59728:   | res (Subproblem' (_, _, _, _, _, t)) = (t, [])
walther@59728:   | res (Take' t) = (t, [])
walther@59728:   | res (Substitute' (_, _, _, _, t)) = (t, [])
walther@59728:   | res (Or_to_List' (_,  t)) = (t, [])
walther@59846:   | res m = raise ERROR ("result: not impl.for " ^ string_of m)
walther@59728: 
walther@59728: (*fun result m = (fst o res) m; TODO*)
walther@59728: fun result tac = (fst o res) tac;
walther@59728: fun creates_assms tac = (snd o res) tac;
walther@59728: 
walther@59728: fun insert_assumptions tac ctxt  = ContextC.insert_assumptions (creates_assms tac) ctxt
walther@59728: 
walther@59749: fun for_specify (Init_Proof _) = true
walther@59749:   | for_specify Model_Problem  = true
walther@59749:   | for_specify (Refine_Tacitly _) = true
walther@59749:   | for_specify (Refine_Problem _) = true
walther@59749:   | for_specify (Add_Given _) = true
walther@59749:   | for_specify (Del_Given _) = true
walther@59749:   | for_specify (Add_Find _) = true
walther@59749:   | for_specify (Del_Find _) = true
walther@59749:   | for_specify (Add_Relation _) = true
walther@59749:   | for_specify (Del_Relation _) = true
walther@59749:   | for_specify (Specify_Theory _) = true
walther@59749:   | for_specify (Specify_Problem _) = true
walther@59749:   | for_specify (Specify_Method _) = true
walther@59749:   | for_specify _ = false
walther@59749: fun for_specify' (Init_Proof' _) = true
walther@59749:   | for_specify' (Model_Problem' _) = true
walther@59749:   | for_specify' (Refine_Tacitly' _) = true
walther@59749:   | for_specify' (Refine_Problem' _) = true
walther@59749:   | for_specify' (Add_Given' _) = true
walther@59749:   | for_specify' (Del_Given' _) = true
walther@59749:   | for_specify' (Add_Find' _) = true
walther@59749:   | for_specify' (Del_Find' _) = true
walther@59749:   | for_specify' (Add_Relation' _) = true
walther@59749:   | for_specify' (Del_Relation' _) = true
walther@59749:   | for_specify' (Specify_Theory' _) = true
walther@59749:   | for_specify' (Specify_Problem' _) = true
walther@59749:   | for_specify' (Specify_Method' _) = true
walther@59749:   | for_specify' _ = false
walther@59749: 
walther@59728: (**)end(**)