(* 

    authors: Walther Neuper 2002, 2006

   (c) due to copyright terms

 tools for rewriting, reverse rewriting, context to thy concerning rewriting

 *)

 signature REWRITE_TOOLS =

 sig

   type deriv

   val contains_rule : Rule.rule -> Rule_Set.T -> bool

   val atomic_appl_tacs : theory -> string -> Rule_Set.T -> term -> Tactic.input -> Tactic.input list

   val thy_containing_rls : ThyC.theory' -> Rule_Set.identifier -> string * ThyC.theory'

   val thy_containing_cal : ThyC.theory' -> Exec_Def.prog_calcID -> string * string

   datatype contthy

   = ContNOrew of {applto: term, thm_rls: Celem.guh, thyID: ThyC.thyID}

      | ContNOrewInst of {applto: term, bdvs: Rule.subst, thm_rls: Celem.guh, thminst: term, thyID: ThyC.thyID}

      | ContRls of {applto: term, asms: term list, result: term, rls: Celem.guh, thyID: ThyC.thyID}

      | ContRlsInst of {applto: term, asms: term list, bdvs: Rule.subst, result: term, rls: Celem.guh, thyID: ThyC.thyID}

      | ContThm of {applat: term, applto: term, asmrls: Rule_Set.identifier, asms: (term * term) list,

        lhs: term * term, resasms: term list, result: term, reword: Rule_Def.rew_ord', rhs: term * term,

        thm: Celem.guh, thyID: ThyC.thyID}

      | ContThmInst of {applat: term, applto: term, asmrls: Rule_Set.identifier, asms: (term * term) list,

        bdvs: Rule.subst, lhs: term * term, resasms: term list, result: term, reword: Rule_Def.rew_ord',

        rhs: term * term, thm: Celem.guh, thminst: term, thyID: ThyC.thyID}

      | EContThy

   val guh2filename : Celem.guh -> Celem.filename

   val is_sym : Celem.thmID -> bool

   val sym_drop : Celem.thmID -> Celem.thmID

   val sym_rls : Rule_Set.T -> Rule_Set.T

   val sym_rule : Rule.rule -> Rule.rule

   val thms_of_rls : Rule_Set.T -> Rule.rule list

   val theID2filename : Celem.theID -> Celem.filename

   val no_thycontext : Celem.guh -> bool

   val subs_from : Istate.T -> 'a -> Celem.guh -> Selem.subs

   val guh2rewtac : Celem.guh -> Selem.subs -> Tactic.input

   val get_tac_checked : Ctree.ctree -> Pos.pos' -> Tactic.input

   val context_thy : Calc.T -> Tactic.input -> contthy

   val distinct_Thm : Rule.rule list -> Rule.rule list

   val eq_Thms : string list -> Rule.rule -> bool

   val make_deriv : theory -> Rule_Set.T -> Rule.rule list -> ((term * term) list -> term * term -> bool) ->

     term option -> term -> deriv

   val reverse_deriv : theory -> Rule_Set.T -> Rule.rule list -> ((term * term) list -> term * term -> bool) ->

     term option -> term -> (Rule.rule * (term * term list)) list

   val get_bdv_subst : term -> (term * term) list -> Selem.subs option * Rule.subst

   val thy_containing_thm : string -> string * string

   val guh2theID : Celem.guh -> Celem.theID

 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)

   (*  NONE *)

 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )

   val trtas2str : (term * Rule.rule * (term * term list)) list -> string

   val eq_Thm : Rule.rule * Rule.rule -> bool

   val deriv2str : (term * Rule.rule * (term * term list)) list -> string

   val deriv_of_thm'' : Celem.thm'' -> string

 ( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)

 (*----- unused code, kept as hints to design ideas ---------------------------------------------*)

   val deri2str : (Rule.rule * (term * term list)) list -> string

   val sym_trm : term -> term

 end 

 (**)

 structure Rtools(**): REWRITE_TOOLS(**) =

 struct

 (**)

 (*** reverse rewriting ***)

 (*. a '_deriv'ation is constructed during 'reverse rewring' by an Rrls       *

  *  of for connecting a user-input formula with the current calc-state.	     *

  *# It is somewhat incompatible with the rest of the math-engine:	     *

  *  (1) it is not created by a script					     *

  *  (2) thus there cannot be another user-input within a derivation	     *

  *# It suffers particularily from the not-well-foundedness of the math-engine*

  *  (1) FIXME other branchtyptes than Transitive will change 'embed_deriv'   *

  *  (2) FIXME and eventually 'compare_step' (ie. the script interpreter)     *

  *  (3) FIXME and eventually 'lev_back'                                      *

  *# SOME improvements are evident FIXME.040215 '_deriv'ation:	             *

  *  (1) FIXME nest Rls_ in 'make_deriv'					     *

  *  (2) FIXME do the not-reversed part in 'make_deriv' by scripts -- thus    *

  *	user-input will become possible in this part of a derivation	     *

  *  (3) FIXME do (2) only if a derivation has been found -- for efficiency,  *

  *	while a non-derivable inform requires to step until End_Proof'	     *

  *  (4) FIXME find criteria on when _not_ to step until End_Proof'           *

  *  (5) FIXME 

 .*)

 type deriv =      (* derivation for insertin one level of nodes into the Ctree *) 

   ( term *        (* where the rule is applied to                              *)

     Rule.rule *   (* rule to be applied                                        *)

     ( term *      (* resulting from rule application                           *)

       term list)) (* assumptions resulting from rule application               *)

   list

 fun trta2str (t, r, (t', a)) =

   "\n(" ^ Rule.term2str t ^ ", " ^ Rule_Set.rule2str' r ^ ", (" ^ Rule.term2str t' ^ ", " ^ Rule.terms2str a ^ "))"

 fun trtas2str trtas = (strs2str o (map trta2str)) trtas

 val deriv2str = trtas2str

 fun rta2str (r, (t, a)) =

   "\n(" ^ Rule_Set.rule2str' r ^ ", (" ^ Rule.term2str t ^ ", " ^ Rule.terms2str a ^ "))"

 fun rtas2str rtas = (strs2str o (map rta2str)) rtas

 val deri2str = rtas2str

 (* A1==>...==> An ==> (Lhs = Rhs) goes to A1 ==>...==> An ==> (Rhs = Lhs) *)

 fun sym_thm thm =

   let 

     val (deriv,

       {cert = cert, tags = tags, maxidx = maxidx, shyps = shyps, hyps = hyps, tpairs = tpairs, 

       prop = prop}) = Thm.rep_thm_G thm

     val (lhs, rhs) = (TermC.dest_equals o TermC.strip_trueprop o Logic.strip_imp_concl) prop

     val prop' = case TermC.strip_imp_prems' prop of

         NONE => HOLogic.Trueprop $ (TermC.mk_equality (rhs, lhs))

       | SOME cs => TermC.ins_concl cs (HOLogic.Trueprop $ (TermC.mk_equality (rhs, lhs)))

   in Thm.assbl_thm deriv cert tags maxidx shyps hyps tpairs prop' end

 (* WN100910 weaker than fun sym_thm for Theory.axioms_of in isa02 *)

 fun sym_trm trm =

   let

     val (lhs, rhs) = (TermC.dest_equals o TermC.strip_trueprop o Logic.strip_imp_concl) trm

     val trm' = case TermC.strip_imp_prems' trm of

 	      NONE => TermC.mk_equality (rhs, lhs)

 	    | SOME cs => TermC.ins_concl cs (TermC.mk_equality (rhs, lhs))

   in trm' end

 (* derive normalform of a rls, or derive until SOME goal,

    and record rules applied and rewrites.

 val it = fn

   : theory

     -> rls

     -> rule list

     -> rew_ord       : the order of this rls, which 1 theorem of is used 

                        for rewriting 1 single step (?14.4.03)

     -> term option   : 040214 ??? use for "derive until SOME goal" ??? 

     -> term 

     -> (term *       : to this term ...

         rule * 	     : ... this rule is applied yielding ...

         (term *      : ... this term ...

          term list)) : ... under these assumptions.

        list          :

 returns empty list for a normal form

 FIXME.WN040214: treats rules as in Rls, _not_ as in Seq

 WN060825 too complicated for the intended use by cancel_, common_nominator_

 and unreflectedly adapted to extension of rules by Rls_: returns Rls_("sym_simpl..

  -- replaced below *)

 fun make_deriv thy erls rs ro goal tt = 

   let 

     datatype switch = Appl | Noap (* unify with version in rewrite.sml *)

     fun rew_once _ rts t Noap [] = 

         (case goal of NONE => rts | SOME _ => error ("make_deriv: no derivation for " ^ Rule.term2str t))

       | rew_once lim rts t Appl [] = rew_once lim rts t Noap rs

         (*| Seq _ => rts) FIXXXXXME 14.3.03*)

       | rew_once lim rts t apno rs' =

         (case goal of 

           NONE => rew_or_calc lim rts t apno rs'

         | SOME g => if g = t then rts else rew_or_calc lim rts t apno rs')

     and rew_or_calc lim rts t apno (rrs' as (r :: rs')) =

       if lim < 0 

       then (tracing ("make_deriv exceeds " ^ int2str (! Celem.lim_deriv) ^ "with deriv =\n");

         tracing (deriv2str rts); rts)

       else

         (case r of

           Rule.Thm (thmid, tm) => 

             (if not (! Celem.trace_rewrite) then () else tracing ("### trying thm \"" ^ thmid ^ "\"");

             case Rewrite.rewrite_ thy ro erls true tm t of

               NONE => rew_once lim rts t apno rs'

             | SOME (t', a') =>

               (if ! Celem.trace_rewrite then tracing ("=== rewrites to: " ^ Rule.term2str t') else ();

               rew_once (lim - 1) (rts @ [(t, r, (t', a'))]) t' Appl rrs'))

         | Rule.Num_Calc (c as (op_, _)) => 

           let 

             val _ = if not (! Celem.trace_rewrite) then () else tracing ("### trying calc. \"" ^ op_^"\"")

             val t = TermC.uminus_to_string t

           in 

             case Num_Calc.adhoc_thm thy c t of

               NONE => rew_once lim rts t apno rs'

             | SOME (thmid, tm) => 

               (let

                 val (t', a') = case Rewrite.rewrite_ thy ro erls true tm t of

                   SOME ta => ta

                 | NONE => error "adhoc_thm: NONE"

                 val _ = if not (! Celem.trace_rewrite) then () else tracing("=== calc. to: " ^ Rule.term2str t')

                 val r' = Rule.Thm (thmid, tm)

               in rew_once (lim - 1) (rts @ [(t, r', (t', a'))]) t' Appl rrs' end) 

                 handle _ => error "derive_norm, Num_Calc: no rewrite"

           end

       (*| Cal1 (cc as (op_,_)) => ... WN080222 see rewrite__set_: see 7df94616c1bd and earlier*)

         | Rule.Rls_ rls =>           (* WN060829: CREATES "sym_rlsID", see 7df94616c1bd and earlier*)

           (case Rewrite.rewrite_set_ thy true rls t of

             NONE => rew_once lim rts t apno rs'

           | SOME (t', a') => rew_once (lim - 1) (rts @ [(t, r, (t', a'))]) t' Appl rrs')

         | rule => error ("rew_once: uncovered case " ^ Rule_Set.rule2str rule))

     | rew_or_calc _ _ _ _ [] = error "rew_or_calc: called with []"

   in rew_once (! Celem.lim_deriv) [] tt Noap rs end

 fun sym_drop thmID =

   case Symbol.explode thmID of

 	  "s" :: "y" :: "m" :: "_" :: id => implode id

   | _ => thmID

 fun is_sym thmID =

   case Symbol.explode thmID of

 	  "s" :: "y" :: "m" :: "_" :: _ => true

   | _ => false;

 (*FIXXXXME.040219: detail has to handle Rls id="sym_..." 

   by applying make_deriv, rev_deriv'; see concat_deriv*)

 fun sym_rls Rule_Set.Empty = Rule_Set.Empty

   | sym_rls (Rule_Def.Repeat {id, scr, calc, errpatts, erls, srls, rules, rew_ord, preconds}) =

     Rule_Def.Repeat {id = "sym_" ^ id, scr = scr, calc = calc, errpatts = errpatts, erls = erls, srls = srls, 

       rules = rules, rew_ord = rew_ord, preconds = preconds}

   | sym_rls (Rule_Set.Seqence {id, scr, calc, errpatts, erls, srls, rules, rew_ord, preconds}) =

     Rule_Set.Seqence {id = "sym_" ^ id, scr = scr, calc = calc, errpatts = errpatts, erls = erls, srls = srls, 

       rules = rules, rew_ord = rew_ord, preconds = preconds}

   | sym_rls (Rule_Set.Rrls {id, scr, calc, errpatts, erls, prepat, rew_ord}) = 

     Rule_Set.Rrls {id = "sym_" ^ id, scr = scr, calc = calc,  errpatts = errpatts, erls = erls,

       prepat = prepat, rew_ord = rew_ord}

 (* toggles sym_* and keeps "#:" for ad-hoc calculations *)

 fun sym_rule (Rule.Thm (thmID, thm)) =

   let

     val thm' = sym_thm thm

     val thmID' = case Symbol.explode thmID of

       "s" :: "y" :: "m" :: "_" :: id => implode id

     | "#" :: ":" :: _ => "#: " ^ Rule.string_of_thmI thm'

     | _ => "sym_" ^ thmID

   in Rule.Thm (thmID', thm') end

 | sym_rule (Rule.Rls_ rls) = Rule.Rls_ (sym_rls rls) (* TODO? handle with interSteps ? *)

 | sym_rule r = error ("sym_rule: not for " ^  Rule_Set.rule2str r)

 (*version for reverse rewrite used before 040214*)

 fun rev_deriv (t, r, (_, a)) = (sym_rule r, (t, a));

 fun reverse_deriv thy erls rs ro goal t =

     (rev o (map rev_deriv)) (make_deriv thy erls rs ro goal t)

 fun eq_Thm (Rule.Thm (id1, _), Rule.Thm (id2,_)) = id1 = id2

   | eq_Thm (Rule.Thm (_, _), _) = false

   | eq_Thm (Rule.Rls_ r1, Rule.Rls_ r2) = Rule_Set.id_rls r1 = Rule_Set.id_rls r2

   | eq_Thm (Rule.Rls_ _, _) = false

   | eq_Thm (r1, r2) = error ("eq_Thm: called with '" ^ Rule_Set.rule2str r1 ^ "' '" ^ Rule_Set.rule2str r2 ^ "'")

 fun distinct_Thm r = gen_distinct eq_Thm r

 fun eq_Thms thmIDs thm = (member op = thmIDs (Celem.id_of_thm thm))

   handle ERROR _ => false

 fun thy_containing_thm thmDeriv =

   let

     val isabthys' = map Context.theory_name (Celem.isabthys ());

   in

     if member op= isabthys' (Celem.thyID_of_derivation_name thmDeriv)

     then ("Isabelle", Celem.thyID_of_derivation_name thmDeriv)

     else ("IsacKnowledge", Celem.thyID_of_derivation_name thmDeriv)

   end

 (* which theory in ancestors of thy' contains a ruleset *)

 fun thy_containing_rls thy' rls' =

   let

     val thy = ThyC.Thy_Info_get_theory thy'

   in

     case AList.lookup op= (KEStore_Elems.get_rlss thy) rls' of

       SOME (thy'', _) => (Celem.partID' thy'', thy'')

     | _ => error ("thy_containing_rls : rls '" ^ rls' ^ "' not in ancestors of thy '" ^ thy' ^ "'")

   end

 (* this function cannot work as long as the datastructure does not contain thy' *)

 fun thy_containing_cal thy' sop =

   let

     val thy = ThyC.Thy_Info_get_theory thy'

   in

     case AList.lookup op= (KEStore_Elems.get_calcs thy) sop of

       SOME (_(*"Groups.plus_class.plus"*), _) => ("IsacKnowledge", "Base_Tools")

     | _ => error ("thy_containing_cal : rls '" ^ sop ^ "' not in ancestors of thy '" ^ thy' ^ "'")

   end

 (* packing return-values to matchTheory, contextToThy for xml-generation *)

 datatype contthy =  (*also an item from KEStore on Browser ...........#*)

 	EContThy   (* not from KEStore ..............................*)

   | ContThm of (* a theorem in contex ===========================*)

     {thyID   : ThyC.thyID,      (* for *2guh in sub-elems here        .*)

      thm     : Celem.guh,       (* theorem in the context             .*)

      applto  : term,	          (* applied to formula ...             .*)

      applat  : term,	          (* ...  with lhs inserted             .*)

      reword  : Rule_Def.rew_ord',   (* order used for rewrite             .*)

      asms    : (term            (* asumption instantiated             .*)

    	   * term) list,            (* asumption evaluated                .*)

      lhs     : term             (* lhs of the theorem ...             #*)

    	   * term,                  (* ... instantiated                   .*)

      rhs     : term             (* rhs of the theorem ...             #*)

    	   * term,                  (* ... instantiated                   .*)

      result  : term,	          (* resulting from the rewrite         .*)

      resasms : term list,       (* ... with asms stored               .*)

      asmrls  : Rule_Set.identifier        (* ruleset for evaluating asms        .*)

    	}						 

   | ContThmInst of (* a theorem with bdvs in contex ============ *)

     {thyID   : ThyC.thyID,      (*for *2guh in sub-elems here         .*)

      thm     : Celem.guh,       (*theorem in the context              .*)

      bdvs    : Rule.subst,      (*bound variables to modify...        .*)

      thminst : term,            (*... theorem instantiated            .*)

      applto  : term,	          (*applied to formula ...              .*)

      applat  : term,	          (*...  with lhs inserted              .*)

      reword  : Rule_Def.rew_ord',   (*order used for rewrite              .*)

      asms    : (term            (*asumption instantiated              .*)

    	   * term) list,            (*asumption evaluated                 .*)

      lhs     : term             (*lhs of the theorem ...              #*)

    	   * term,                  (*... instantiated                    .*)

      rhs     : term             (*rhs of the theorem ...              #*)

    	   * term,                  (*... instantiated                    .*)

      result  : term,	          (*resulting from the rewrite          .*)

      resasms : term list,       (*... with asms stored                .*)

      asmrls  : Rule_Set.identifier        (*ruleset for evaluating asms         .*)

     }						 

   | ContRls of (* a rule set in contex ========================= *)

     {thyID   : ThyC.thyID,      (*for *2guh in sub-elems here         .*)

      rls     : Celem.guh,       (*rule set in the context             .*)

      applto  : term,	          (*rewrite this formula                .*)

      result  : term,	          (*resulting from the rewrite          .*)

      asms    : term list        (*... with asms stored                .*)

    	}						 

   | ContRlsInst of (* a rule set with bdvs in contex =========== *)

 	{thyID   : ThyC.thyID,        (*for *2guh in sub-elems here         .*)

 	 rls     : Celem.guh,         (*rule set in the context             .*)

 	 bdvs    : Rule.subst,        (*for bound variables in thms         .*)

 	 applto  : term,	            (*rewrite this formula                .*)

 	 result  : term,	            (*resulting from the rewrite          .*)

 	 asms    : term list          (*... with asms stored                .*)

    	}						 

   | ContNOrew of (* no rewrite for thm or rls ================== *)

     {thyID   : ThyC.thyID,      (*for *2guh in sub-elems here         .*)

      thm_rls : Celem.guh,       (*thm or rls in the context           .*)

      applto  : term	            (*rewrite this formula                .*)

    	}						 

   | ContNOrewInst of (* no rewrite for some instantiation ====== *)

     {thyID   : ThyC.thyID,      (*for *2guh in sub-elems here         .*)

      thm_rls : Celem.guh,       (*thm or rls in the context           .*)

      bdvs    : Rule.subst,      (*for bound variables in thms         .*)

      thminst : term,            (*... theorem instantiated            .*)

      applto  : term	            (*rewrite this formula                .*)

    	}						 

 (*.check a rewrite-tac for bdv (RL always used *_Inst !) TODO.WN060718

    pass other tacs unchanged.*)

 fun get_tac_checked pt ((p, _) : Pos.pos') = Ctree.get_obj Ctree.g_tac pt p;

 (* create a derivation-name, eg. ("refl", _) --> "HOL.refl"*)

 fun deriv_of_thm'' (thmID, _) =

   thmID |> Global_Theory.get_thm (ThyC.Isac ()) |> Thm.get_name_hint

 (* get the formula f at ptp rewritten by the Rewrite_* already applied to f *)

 fun context_thy (pt, pos as (p,p_)) (tac as Tactic.Rewrite thm'') =

     let val thm_deriv = deriv_of_thm'' thm''

     in

     (case Applicable.applicable_in pos pt tac of

       Applicable.Appl (Tactic.Rewrite' (thy', ord', erls, _, _, f, (res,asm))) =>

         ContThm

          {thyID = ThyC.theory'2thyID thy',

           thm = Celem.thm2guh (thy_containing_thm thm_deriv) (Celem.thmID_of_derivation_name thm_deriv),

           applto = f, applat  = Rule.e_term, reword  = ord',

           asms = [](*asms ~~ asms'*), lhs = (Rule.e_term, Rule.e_term)(*(lhs, lhs')*), rhs = (Rule.e_term, Rule.e_term)(*(rhs, rhs')*),

           result = res, resasms = asm, asmrls  = Rule_Set.id_rls erls}

      | Applicable.Notappl _ =>

          let

            val pp = Ctree.par_pblobj pt p

            val thy' = Ctree.get_obj Ctree.g_domID pt pp

            val f = case p_ of

              Pos.Frm => Ctree.get_obj Ctree.g_form pt p

            | Pos.Res => (fst o (Ctree.get_obj Ctree.g_result pt)) p 

            | _ => error "context_thy: uncovered position"

          in

            ContNOrew

             {thyID   = ThyC.theory'2thyID thy',

              thm_rls = 

                Celem.thm2guh (thy_containing_thm thm_deriv) (Celem.thmID_of_derivation_name thm_deriv),

              applto  = f}

 		     end

      | _ => error "context_thy..Rewrite: uncovered case 2")

     end

   | context_thy (pt, pos as (p, p_)) (tac as Tactic.Rewrite_Inst (subs, (thmID, _))) =

     let val thm = Global_Theory.get_thm (ThyC.Isac ()) thmID

     in

 	  (case Applicable.applicable_in pos pt tac of

 	     Applicable.Appl (Tactic.Rewrite_Inst' (thy', ord', erls, _, subst, _, f, (res, asm))) =>

 	       let

            val thm_deriv = Thm.get_name_hint thm

            val thminst = TermC.inst_bdv subst ((Num_Calc.norm o #prop o Thm.rep_thm) thm)

 	       in

 	         ContThmInst

 	          {thyID = ThyC.theory'2thyID thy',

 	           thm = 

 	             Celem.thm2guh (thy_containing_thm thm_deriv) (Celem.thmID_of_derivation_name thm_deriv),

 	           bdvs = subst, thminst = thminst, applto  = f, applat  = Rule.e_term, reword  = ord',

 	           asms = [](*asms ~~ asms'*), lhs = (Rule.e_term, Rule.e_term)(*(lhs, lhs')*), rhs = (Rule.e_term, Rule.e_term)(*(rhs, rhs')*),

 	           result = res, resasms = asm, asmrls  = Rule_Set.id_rls erls}

 	       end

      | Applicable.Notappl _ =>

          let

            val thm = Global_Theory.get_thm (ThyC.Isac ()(*WN141021 assoc_thy thy' ERROR*)) thmID

            val thm_deriv = Thm.get_name_hint thm

            val pp = Ctree.par_pblobj pt p

            val thy' = Ctree.get_obj Ctree.g_domID pt pp

            val subst = Selem.subs2subst (Celem.assoc_thy thy') subs

            val thminst = TermC.inst_bdv subst ((Num_Calc.norm o #prop o Thm.rep_thm) thm)

            val f = case p_ of

                Pos.Frm => Ctree.get_obj Ctree.g_form pt p

              | Pos.Res => (fst o (Ctree.get_obj Ctree.g_result pt)) p 

              | _ => error "context_thy: uncovered case 3"

          in

            ContNOrewInst

             {thyID = ThyC.theory'2thyID thy',

              thm_rls = Celem.thm2guh (thy_containing_thm thm_deriv) (Celem.thmID_of_derivation_name thm_deriv),

              bdvs = subst, thminst = thminst, applto = f}

          end

       | _ => error "context_thy..Rewrite_Inst: uncovered case 4")

     end

   | context_thy (pt, p) (tac as Tactic.Rewrite_Set rls') =

     (case Applicable.applicable_in p pt tac of

        Applicable.Appl (Tactic.Rewrite_Set' (thy', _, _(*rls*), f, (res,asm))) =>

          ContRls

           {thyID = ThyC.theory'2thyID thy',

            rls = Celem.rls2guh (thy_containing_rls thy' rls') rls',

            applto = f, result = res, asms = asm}

      | _ => error ("context_thy Rewrite_Set: not for Applicable.Notappl"))

   | context_thy (pt,p) (tac as Tactic.Rewrite_Set_Inst (_(*subs*), rls')) = 

     (case Applicable.applicable_in p pt tac of

        Applicable.Appl (Tactic.Rewrite_Set_Inst' (thy', _, subst, _, f, (res,asm))) =>

          ContRlsInst

           {thyID = ThyC.theory'2thyID thy',

            rls = Celem.rls2guh (thy_containing_rls thy' rls') rls',

            bdvs = subst, applto = f, result = res, asms = asm}

      | _ => error ("context_thy Rewrite_Set_Inst: not for Applicable.Notappl"))

   | context_thy (_, p) tac =

       error ("context_thy: not for tac " ^ Tactic.input_to_string tac ^ " at " ^ Pos.pos'2str p)

 (* get all theorems in a rule set (recursivley containing rule sets) *)

 fun thm_of_rule Rule.Erule = []

   | thm_of_rule (thm as Rule.Thm _) = [thm]

   | thm_of_rule (Rule.Num_Calc _) = []

   | thm_of_rule (Rule.Cal1 _) = []

   | thm_of_rule (Rule.Rls_ rls) = thms_of_rls rls

 and thms_of_rls Rule_Set.Empty = []

   | thms_of_rls (Rule_Def.Repeat {rules,...}) = (flat o (map  thm_of_rule)) rules

   | thms_of_rls (Rule_Set.Seqence {rules,...}) = (flat o (map  thm_of_rule)) rules

   | thms_of_rls (Rule_Set.Rrls _) = []

 (* check if a rule is contained in a rule-set (recursivley down in Rls_);

    this rule can even be a rule-set itself                             *)

 fun contains_rule r rls = 

   let 

     fun (*find (_, Rls_ rls) = finds (get_rules rls)

       | find r12 = eq_rule r12

     and*) finds [] = false

     | finds (r1 :: rs) = if Rule_Set.eq_rule (r, r1) then true else finds rs

   in 

     finds (Rule_Set.get_rules rls) 

   end

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

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

 fun try_rew thy ((_, ro) : Rule_Def.rew_ord) erls (subst : Rule.subst) f (thm' as Rule.Thm (_, thm)) =

     if Auto_Prog.contains_bdv thm

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

 	    SOME _ => [Tactic.rule2tac thy subst thm']

 	  | NONE => []

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

 	    SOME _ => [Tactic.rule2tac thy [] thm']

 	  | NONE => [])

   | try_rew thy _ _ _ f (cal as Rule.Num_Calc c) = 

     (case Num_Calc.adhoc_thm thy c f of

 	    SOME _ => [Tactic.rule2tac thy [] cal]

     | NONE => [])

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

     (case Num_Calc.adhoc_thm thy c f of

 	      SOME _ => [Tactic.rule2tac thy [] cal]

       | NONE => [])

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

   | try_rew _ _ _ _ _ _ = error "try_rew: uncovered case"

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

     gen_distinct Tactic.eq_tac (flat (map (try_rew thy ro erls subst f) rules))

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

     gen_distinct Tactic.eq_tac (flat (map (try_rew thy ro erls subst f) rules))

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

   | filter_appl_rews _ _ _ _ = 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 atomic_appl_tacs thy _ _ f (Tactic.Calculate scrID) =

     try_rew thy Rule.e_rew_ordX Rule_Set.empty [] f (Rule.Num_Calc (assoc_calc' thy scrID |> snd))

   | atomic_appl_tacs thy ro erls f (Tactic.Rewrite thm'') =

     try_rew thy (ro, Rule.assoc_rew_ord ro) erls [] f (Rule.Thm thm'')

   | atomic_appl_tacs thy ro erls f (Tactic.Rewrite_Inst (subs, thm'')) =

     try_rew thy (ro, Rule.assoc_rew_ord ro) erls (Selem.subs2subst thy subs) f (Rule.Thm thm'')

   | atomic_appl_tacs thy _ _ f (Tactic.Rewrite_Set rls') =

     filter_appl_rews thy [] f (assoc_rls rls')

   | atomic_appl_tacs thy _ _ f (Tactic.Rewrite_Set_Inst (subs, rls')) =

     filter_appl_rews thy (Selem.subs2subst thy subs) f (assoc_rls rls')

   | atomic_appl_tacs _ _ _ _ tac = 

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

 (* filenames not only for thydata, but also for thy's etc *)

 fun theID2filename theID = Celem.theID2guh theID ^ ".xml"

 fun guh2theID guh =

   let

     val guh' = Symbol.explode guh

     val part = implode (take_fromto 1 4 guh')

     val isa = implode (take_fromto 5 9 guh')

   in

     if not (member op = ["exp_", "thy_", "pbl_", "met_"] part)

     then raise ERROR ("guh '" ^ guh ^ "' does not begin with exp_ | thy_ | pbl_ | met_")

     else

       let

   	    val chap = case isa of

   		  "isab_" => "Isabelle"

   		| "scri_" => "IsacScripts"

   		| "isac_" => "IsacKnowledge"

   		| _ =>

   		  raise ERROR ("guh2theID: '" ^ guh ^ "' does not have isab_ | scri_ | isac_ at position 5..9")

         val rest = takerest (9, guh') 

         val thyID = takewhile [] (not o (curry op= "-")) rest

         val rest' = dropuntil (curry op = "-") rest

 	    in case implode rest' of

 		    "-part" => [chap] : Celem.theID

       | "" => [chap, implode thyID]

       | "-Theorems" => [chap, implode thyID, "Theorems"]

       | "-Rulesets" => [chap, implode thyID, "Rulesets"]

       | "-Operations" => [chap, implode thyID, "Operations"]

       | "-Orders" => [chap, implode thyID, "Orders"]

       | _ => 

 		    let val sect = implode (take_fromto 1 5 rest')

 		       val sect' = case sect of

 			       "-thm-" => "Theorems"

 			     | "-rls-" => "Rulesets"

 			     | "-cal-" => "Operations"

 			     | "-ord-" => "Orders"

 			     | _ =>

 			     raise ERROR ("guh2theID: '" ^ guh ^ "' has '" ^ sect ^ "' instead -thm- | -rls- | -cal- | -ord-")

 		    in

 		      [chap, implode thyID, sect', implode (takerest (5, rest'))]

 		    end

 	    end	

     end

 fun guh2filename guh = guh ^ ".xml";

 fun guh2rewtac guh [] =

     let

       val (_, thy, sect, xstr) = case guh2theID guh of

         [isa, thy, sect, xstr] => (isa, thy, sect, xstr)

       | _ => error "guh2rewtac: uncovered case"

     in case sect of

       "Theorems" => Tactic.Rewrite (xstr, Rewrite.assoc_thm'' (Celem.assoc_thy thy) xstr)

     | "Rulesets" => Tactic.Rewrite_Set xstr

     | _ => error ("guh2rewtac: not impl. for '"^xstr^"'") 

     end

   | guh2rewtac guh subs =

     let

       val (_, thy, sect, xstr) = case guh2theID guh of

         [isa, thy, sect, xstr] => (isa, thy, sect, xstr)

       | _ => error "guh2rewtac: uncovered case"

     in case sect of

       "Theorems" => 

         Tactic.Rewrite_Inst (subs, (xstr, Rewrite.assoc_thm'' (Celem.assoc_thy thy) xstr))

     | "Rulesets" => Tactic.Rewrite_Set_Inst (subs,  xstr)

     | str => error ("guh2rewtac: not impl. for '" ^ str ^ "'") 

     end

 (* the front-end may request a context for any element of the hierarchy *)

 fun no_thycontext guh = (guh2theID guh; false)

   handle ERROR _ => true;

 (* get the substitution of bound variables for matchTheory:

    # lookup the thm|rls' in the script

    # take the [(bdv, v_),..] from the respective Rewrite_(Set_)Inst

    # instantiate this subs with the istates env to [(bdv, x),..]

    # otherwise []

    WN060617 hack assuming that all scripts use only one bound variable

    and use 'v_' as the formal argument for this bound variable*)

 fun subs_from (Istate.Pstate (pst as {env, ...})) _ guh =

     let

       val (_, _, thyID, sect, xstr) = case guh2theID guh of

         theID as [isa, thyID, sect, xstr] => (theID, isa, thyID, sect, xstr)

       | _ => error "subs_from: uncovered case"

     in

       case sect of

         "Theorems" => 

           let val thm = Global_Theory.get_thm (Celem.assoc_thy (ThyC.thyID2theory' thyID)) xstr

           in

             if Auto_Prog.contains_bdv thm

             then

               let

                 val formal_arg = TermC.str2term "v_"      

                 val value = subst_atomic env formal_arg

               in ["(''bdv''," ^ Rule.term2str value ^ ")"] : Selem.subs end

             else []

 	        end

   	  | "Rulesets" => 

         let

           val rules = (Rule_Set.get_rules o assoc_rls) xstr

         in

           if Auto_Prog.contain_bdv rules

           then

             let

               val formal_arg = TermC.str2term "v_"

               val value = subst_atomic env formal_arg

             in ["(''bdv''," ^ Rule.term2str value ^ ")"] : Selem.subs end

           else []

         end

       | str => error ("subs_from: uncovered case with " ^ str)

     end

   | subs_from _ _  guh = error ("subs_from: uncovered case with " ^ guh)

 (* get a substitution for "bdv*" from the current program and environment.

     returns a substitution: sube for tac, subst for tac_, i.e. for rewriting *)

 fun get_bdv_subst prog env =

   let

     fun scan (Const _) = NONE

       | scan (Free _) = NONE

       | scan (Var _) = NONE

       | scan (Bound _) = NONE

       | scan (t as Const ("List.list.Cons", _) $ (Const ("Product_Type.Pair", _) $ _ $ _) $ _) =

         if TermC.is_bdv_subst t then SOME t else NONE

       | scan (Abs (_, _, body)) = scan body

       | scan (t1 $ t2) = case scan t1 of NONE => scan t2 | SOME subst => SOME subst

   in

     case scan prog of

       NONE => (NONE: Selem.subs option, []: Rule.subst)

     | SOME tm =>

         let val subst = subst_atomic env tm

         in (SOME (Selem.subst'_to_sube subst), Selem.subst'_to_subst subst) end

   end

 end