*)

 *)

 signature REWRITE_TOOLS =

 signature REWRITE_TOOLS =

 sig

 sig

   type deriv

   type deriv

   datatype contthy

   datatype contthy

      | EContThy

      | EContThy

   val get_tac_checked : Ctree.ctree -> Ctree.pos' -> Tac.tac

   val get_tac_checked : Ctree.ctree -> Ctree.pos' -> Tac.tac

   val context_thy : Ctree.state -> Tac.tac -> contthy

   val context_thy : Ctree.state -> Tac.tac -> contthy

     term option -> term -> deriv

     term option -> term -> deriv

   val thy_containing_thm : string -> string * string

   val thy_containing_thm : string -> string * string

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

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

   (*  NONE *)

   (*  NONE *)

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

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

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

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

   val eq_Thm : rule * rule -> bool

   val eq_Thm : rule * rule -> bool

   val deriv2str : (term * rule * (term * term list)) list -> string val deriv_of_thm'' : thm'' -> string

   val deriv2str : (term * rule * (term * term list)) list -> string val deriv_of_thm'' : thm'' -> string

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

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

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

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

   val sym_trm : term -> term

   val sym_trm : term -> term

 end 

 end 

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

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

 struct

 struct

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

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

  *  (5) FIXME 

  *  (5) FIXME 

 .*)

 .*)

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

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

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

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

     ( term *      (* resulting from rule application                              *)

     ( term *      (* resulting from rule application                              *)

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

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

   list            (*                                                              *) 

   list            (*                                                              *) 

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

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

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

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

 val deriv2str = trtas2str

 val deriv2str = trtas2str

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

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

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

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

 val deri2str = rtas2str

 val deri2str = rtas2str

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

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

   WN120320: reconsider the desing including the java front-end with html representation;

   WN120320: reconsider the desing including the java front-end with html representation;

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

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

 WN060825 too complicated for the intended use by cancel_, common_nominator_

 WN060825 too complicated for the intended use by cancel_, common_nominator_

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

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

  -- replaced below *)

  -- replaced below *)

   let 

   let 

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

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

     fun rew_once _ rts t Noap [] = 

     fun rew_once _ rts t Noap [] = 

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

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

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

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

       | rew_once lim rts t apno rs' =

       | rew_once lim rts t apno rs' =

         (case goal of 

         (case goal of 

           NONE => rew_or_calc lim rts t apno rs'

           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')

         | 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')) =

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

       if lim < 0 

       if lim < 0 

         tracing (deriv2str rts); rts)

         tracing (deriv2str rts); rts)

       else

       else

         (case r of

         (case r of

             case Rewrite.rewrite_ thy ro erls true tm t of

             case Rewrite.rewrite_ thy ro erls true tm t of

               NONE => rew_once lim rts t apno rs'

               NONE => rew_once lim rts t apno rs'

             | SOME (t', a') =>

             | SOME (t', a') =>

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

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

           let 

           let 

             val t = TermC.uminus_to_string t

             val t = TermC.uminus_to_string t

           in 

           in 

             case Calc.adhoc_thm thy c t of

             case Calc.adhoc_thm thy c t of

               NONE => rew_once lim rts t apno rs'

               NONE => rew_once lim rts t apno rs'

             | SOME (thmid, tm) => 

             | SOME (thmid, tm) => 

               (let

               (let

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

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

                   SOME ta => ta

                   SOME ta => ta

                 | NONE => error "adhoc_thm: NONE"

                 | NONE => error "adhoc_thm: NONE"

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

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

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

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

           end

           end

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

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

           (case Rewrite.rewrite_set_ thy true rls t of

           (case Rewrite.rewrite_set_ thy true rls t of

             NONE => rew_once lim rts t apno rs'

             NONE => rew_once lim rts t apno rs'

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

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

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

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

   case Symbol.explode thmID of

   case Symbol.explode thmID of

   | _ => thmID

   | _ => thmID

   case Symbol.explode thmID of

   case Symbol.explode thmID of

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

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

   | _ => false;

   | _ => false;

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

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

   by applying make_deriv, rev_deriv'; see concat_deriv*)

   by applying make_deriv, rev_deriv'; see concat_deriv*)

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

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

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

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

       prepat = prepat, rew_ord = rew_ord}

       prepat = prepat, rew_ord = rew_ord}

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

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

   let

   let

     val thm' = sym_thm thm

     val thm' = sym_thm thm

     val thmID' = case Symbol.explode thmID of

     val thmID' = case Symbol.explode thmID of

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

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

     | _ => "sym_" ^ thmID

     | _ => "sym_" ^ thmID

 (*version for reverse rewrite used before 040214*)

 (*version for reverse rewrite used before 040214*)

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

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

 fun distinct_Thm r = gen_distinct eq_Thm r

 fun distinct_Thm r = gen_distinct eq_Thm r

   handle ERROR _ => false

   handle ERROR _ => false

 fun thy_containing_thm thmDeriv =

 fun thy_containing_thm thmDeriv =

   let

   let

   in

   in

   end

   end

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

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

   let

   let

   in

   in

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

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

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

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

   end

   end

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

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

   let

   let

   in

   in

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

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

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

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

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

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

   end

   end

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

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

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

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

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

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

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

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

    	}						 

    	}						 

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

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

     }						 

     }						 

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

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

    	}						 

    	}						 

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

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

    	}						 

    	}						 

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

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

    	}						 

    	}						 

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

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

    	}						 

    	}						 

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

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

    pass other tacs unchanged.*)

    pass other tacs unchanged.*)

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

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

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

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

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

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

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

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

     let val thm_deriv = deriv_of_thm'' thm''

     let val thm_deriv = deriv_of_thm'' thm''

     in

     in

     (case Applicable.applicable_in pos pt tac of

     (case Applicable.applicable_in pos pt tac of

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

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

         ContThm

         ContThm

      | Chead.Notappl _ =>

      | Chead.Notappl _ =>

          let

          let

            val pp = Ctree.par_pblobj pt p

            val pp = Ctree.par_pblobj pt p

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

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

            val f = case p_ of

            val f = case p_ of

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

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

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

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

            | _ => error "context_thy: uncovered position"

            | _ => error "context_thy: uncovered position"

          in

          in

            ContNOrew

            ContNOrew

              thm_rls = 

              thm_rls = 

              applto  = f}

              applto  = f}

 		     end

 		     end

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

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

     end

     end

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

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

     in

     in

 	  (case Applicable.applicable_in pos pt tac of

 	  (case Applicable.applicable_in pos pt tac of

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

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

 	       let

 	       let

            val thm_deriv = Thm.get_name_hint thm

            val thm_deriv = Thm.get_name_hint thm

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

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

 	       in

 	       in

 	         ContThmInst

 	         ContThmInst

 	           thm = 

 	           thm = 

 	       end

 	       end

      | Chead.Notappl _ =>

      | Chead.Notappl _ =>

          let

          let

            val thm_deriv = Thm.get_name_hint thm

            val thm_deriv = Thm.get_name_hint thm

            val pp = Ctree.par_pblobj pt p

            val pp = Ctree.par_pblobj pt p

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

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

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

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

            val f = case p_ of

            val f = case p_ of

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

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

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

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

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

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

          in

          in

            ContNOrewInst

            ContNOrewInst

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

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

          end

          end

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

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

     end

     end

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

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

     (case Applicable.applicable_in p pt tac of

     (case Applicable.applicable_in p pt tac of

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

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

          ContRls

          ContRls

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

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

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

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

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

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

     (case Applicable.applicable_in p pt tac of

     (case Applicable.applicable_in p pt tac of

        Chead.Appl (Tac.Rewrite_Set_Inst' (thy', _, subst, _, f, (res,asm))) =>

        Chead.Appl (Tac.Rewrite_Set_Inst' (thy', _, subst, _, f, (res,asm))) =>

          ContRlsInst

          ContRlsInst

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

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

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

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

   | context_thy (_, p) tac =

   | context_thy (_, p) tac =

       error ("context_thy: not for tac " ^ Tac.tac2str tac ^ " at " ^ Ctree.pos'2str p)

       error ("context_thy: not for tac " ^ Tac.tac2str tac ^ " at " ^ Ctree.pos'2str p)

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

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

 fun thm_of_rule Erule = []

 fun thm_of_rule Erule = []

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

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

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

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

 fun contains_rule r rls = 

 fun contains_rule r rls = 

   let 

   let 

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

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

       | find r12 = eq_rule r12

       | find r12 = eq_rule r12

     and*) finds [] = false

     and*) finds [] = false

   in 

   in 

   end

   end

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

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

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

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

     if LTool.contains_bdv thm

     if LTool.contains_bdv thm

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

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

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

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

 	  | NONE => []

 	  | NONE => []

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

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

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

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

 	  | NONE => [])

 	  | NONE => [])

     (case Calc.adhoc_thm thy c f of

     (case Calc.adhoc_thm thy c f of

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

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

     | NONE => [])

     | NONE => [])

     (case Calc.adhoc_thm thy c f of

     (case Calc.adhoc_thm thy c f of

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

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

       | NONE => [])

       | NONE => [])

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

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

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

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

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

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

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

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

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

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

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

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

 fun atomic_appl_tacs thy _ _ f (Tac.Calculate scrID) =

 fun atomic_appl_tacs thy _ _ f (Tac.Calculate scrID) =

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

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

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

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

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

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

     filter_appl_rews thy [] f (assoc_rls rls')

     filter_appl_rews thy [] f (assoc_rls rls')

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

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

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

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

   | atomic_appl_tacs _ _ _ _ tac = 

   | atomic_appl_tacs _ _ _ _ tac = 

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

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

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

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

   let

   let

     val guh' = Symbol.explode guh

     val guh' = Symbol.explode guh

     val part = implode (take_fromto 1 4 guh')

     val part = implode (take_fromto 1 4 guh')

     val isa = implode (take_fromto 5 9 guh')

     val isa = implode (take_fromto 5 9 guh')

   in

   in

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

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

         val rest = takerest (9, guh') 

         val rest = takerest (9, guh') 

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

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

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

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

 	    in case implode rest' of

 	    in case implode rest' of

       | "" => [chap, implode thyID]

       | "" => [chap, implode thyID]

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

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

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

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

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

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

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

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

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

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

 		    end

 		    end

 	    end	

 	    end	

     end

     end

 fun guh2rewtac guh [] =

 fun guh2rewtac guh [] =

     let

     let

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

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

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

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

       | _ => error "guh2rewtac: uncovered case"

       | _ => error "guh2rewtac: uncovered case"

     in case sect of

     in case sect of

     | "Rulesets" => Tac.Rewrite_Set xstr

     | "Rulesets" => Tac.Rewrite_Set xstr

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

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

     end

     end

   | guh2rewtac guh subs =

   | guh2rewtac guh subs =

     let

     let

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

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

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

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

       | _ => error "guh2rewtac: uncovered case"

       | _ => error "guh2rewtac: uncovered case"

     in case sect of

     in case sect of

       "Theorems" => 

       "Theorems" => 

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

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

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

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

     end

     end

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

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

   handle ERROR _ => true;

   handle ERROR _ => true;

 (* get the substitution of bound variables for matchTheory:

 (* get the substitution of bound variables for matchTheory:

    # lookup the thm|rls' in the script

    # lookup the thm|rls' in the script

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

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

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

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

    # otherwise []

    # otherwise []

    WN060617 hack assuming that all scripts use only one bound variable

    WN060617 hack assuming that all scripts use only one bound variable

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

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

     let

     let

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

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

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

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

       | _ => error "subs_from: uncovered case"

       | _ => error "subs_from: uncovered case"

     in

     in

       case sect of

       case sect of

         "Theorems" => 

         "Theorems" => 

           in

           in

             if LTool.contains_bdv thm

             if LTool.contains_bdv thm

             then

             then

               let

               let

                 val formal_arg = TermC.str2term "v_"

                 val formal_arg = TermC.str2term "v_"

                 val value = subst_atomic env formal_arg

                 val value = subst_atomic env formal_arg

             else []

             else []

 	        end

 	        end

   	  | "Rulesets" => 

   	  | "Rulesets" => 

         let

         let

         in

         in

           if LTool.contain_bdv rules

           if LTool.contain_bdv rules

           then

           then

             let

             let

               val formal_arg = TermC.str2term "v_"

               val formal_arg = TermC.str2term "v_"

               val value = subst_atomic env formal_arg

               val value = subst_atomic env formal_arg

           else []

           else []

         end

         end

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

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

     end

     end

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

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

     returns a substitution: subst for rewriting and another: sube for Rewrite: *)

     returns a substitution: subst for rewriting and another: sube for Rewrite: *)

 fun get_bdv_subst prog env =

 fun get_bdv_subst prog env =

   let

   let

         if TermC.is_bdv_subst t then SOME t else NONE

         if TermC.is_bdv_subst t then SOME t else NONE

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

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

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

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

   in

   in

     case scan prog of

     case scan prog of

     | SOME tm =>

     | SOME tm =>

         let val subst = tm |> subst_atomic env |> TermC.isalist2list |> map TermC.isapair2pair

         let val subst = tm |> subst_atomic env |> TermC.isalist2list |> map TermC.isapair2pair

           (* "[(bdv,v_v)]": term

           (* "[(bdv,v_v)]": term

                           |> "[(bdv,x)]": term |> ["(bdv,x)"]: term list

                           |> "[(bdv,x)]": term |> ["(bdv,x)"]: term list

                                                          |> [("bdv","x")]: (term * term) list *)

                                                          |> [("bdv","x")]: (term * term) list *)