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

   authors: Walther Neuper 2002, 2006

  (c) due to copyright terms

use"ME/rewtools.sml";

use"rewtools.sml";

*)

(***.reverse rewriting.***)

(*.derivation for insertin one level of nodes into the calctree.*)

type deriv  = (term * rule * (term *term list)) list;

fun trta2str (t,r,(t',a)) = "\n("^(term2str t)^", "^(rule2str' r)^", ("^

			    (term2str t')^", "^(terms2str a)^"))";

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

val deriv2str = trtas2str;

fun rta2str (r,(t,a)) = "\n("^(rule2str' r)^", ("^

			    (term2str t)^", "^(terms2str a)^"))";

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

val deri2str = rtas2str;

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

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

  see tests 

  --- OLD compute rlsthmsNOTisac by eq_thmID ---

  --- compute val rlsthmsNOTisac ---

*)

fun sym_thm thm =

    let 

        val (deriv, {thy = thy, tags = tags, maxidx = maxidx, 

                     shyps = shyps, hyps = hyps, tpairs = tpairs, 

                     prop = prop}) = 

	    Thm.rep_thm_G thm;

        val (lhs,rhs) = (dest_equals' o strip_trueprop 

		         o Logic.strip_imp_concl) prop;

        val prop' = case strip_imp_prems' prop of

		        NONE => Trueprop $ (mk_equality (rhs, lhs))

		      | SOME cs => 

		        ins_concl cs (Trueprop $ (mk_equality (rhs, lhs)));

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

(*

  (sym RS real_mult_div_cancel1) handle e => print_exn e;

Exception THM 1 raised:

RSN: no unifiers

"?s = ?t ==> ?t = ?s"

"?k ~= 0 ==> ?k * ?m / (?k * ?n) = ?m / ?n"

  val thm = real_mult_div_cancel1;

  val prop = (#prop o rep_thm) thm;

  atomt prop;

  val ppp = Logic.strip_imp_concl prop;

  atomt ppp;

  ((#prop o rep_thm o sym_thm o sym_thm) thm) = (#prop o rep_thm) thm;

val it = true : bool

  ((sym_thm o sym_thm) thm) = thm;

val it = true : bool

  val thm = real_le_anti_sym;

  ((sym_thm o sym_thm) thm) = thm;

val it = true : bool

  val thm = real_minus_zero;

  ((sym_thm o sym_thm) thm) = thm;

val it = true : bool

*)

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

fun sym_trm trm =

    let val (lhs,rhs) = (dest_equals' o strip_trueprop

		         o Logic.strip_imp_concl) trm;

        val trm' = case strip_imp_prems' trm of

		        NONE => mk_equality (rhs, lhs)

		      | SOME cs => 

		        ins_concl cs (mk_equality (rhs, lhs));

    in trm' end;

(*ML {*

val trm = @{term "k ~= 0 ==> k * m / (k * n) = m / n"};

(tracing o 

 (term_to_string')) (sym_trm trm);

"~ k = (0::'a) ==> m / n = k * m / (k * n)"

*}*)

(* 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:rule list) ro(*rew_ord*) goal tt = 

  let 

    datatype switch = Appl | Noap

    fun rew_once lim rts t Noap [] = 

        (case goal of NONE => rts | SOME g => error ("make_deriv: no derivation for " ^ 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 (! lim_deriv) ^

        "with deriv =\n"); tracing (deriv2str rts); rts)

      else

        case r of

          Thm (thmid, tm) => 

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

            case rewrite_ thy ro erls true tm t of

              NONE => rew_once lim rts t apno rs'

            | SOME (t', a') =>

              (if ! trace_rewrite then tracing ("### rewrites to: " ^ term2str t') else ();

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

        | Calc (c as (op_,_)) => 

          let 

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

            val t = uminus_to_string t

          in 

            case get_calculation_ thy c t of

              NONE => rew_once lim rts t apno rs'

            | SOME (thmid, tm) => 

              (let

                val SOME (t', a') = rewrite_ thy ro erls true tm t

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

                val r' = Thm (thmid, tm)

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

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

          end

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

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

          (case 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');           

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

fun sym_drop (thmID : thmID) =

    case Symbol.explode thmID of

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

      | id => thmID;

fun is_sym (thmID : thmID) =

    case Symbol.explode thmID of

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

      | id => false;

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

  by applying make_deriv, rev_deriv'; see concat_deriv*)

fun sym_rls Erls = Erls

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

    Rls {id="sym_"^id, scr=scr, calc=calc, errpatts=errpatts, erls=erls, srls=srls, 

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

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

    Seq {id="sym_"^id, scr=scr, calc=calc, errpatts=errpatts,  erls=erls, srls=srls, 

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

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

    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 (Thm (thmID, thm)) =

    let

      val thm' = sym_thm thm

      val thmID' = case Symbol.explode thmID of

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

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

      | _ => "sym_" ^ thmID

    in Thm (thmID', thm') end

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

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

(*

  val th =  Thm ("real_one_collect",num_str @{thm real_one_collect});

  sym_rule th;

val th =

  Thm ("real_one_collect","?m is_const ==> ?n + ?m * ?n = (1 + ?m) * ?n")

  : rule

ML> val it =

  Thm ("sym_real_one_collect","?m is_const ==> (1 + ?m) * ?n = ?n + ?m * ?n")*)

(*version for reverse rewrite used before 040214*)

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

(* val (thy, erls, rs, ro, goal, t) = (thy, eval_rls, rules, ro, NONE, t');

   *)

fun reverse_deriv thy erls (rs:rule list) ro(*rew_ord*) goal t =

    (rev o (map rev_deriv)) (make_deriv thy erls (rs:rule list) ro goal t);

(*

  val rev_rew = reverse_deriv thy e_rls ; 

  tracing(rtas2str rev_rew);

*)

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

  | eq_Thm (Thm (id1,_), _) = false

  | eq_Thm (Rls_ r1, Rls_ r2) = id_rls r1 = id_rls r2

  | eq_Thm (Rls_ r1, _) = false

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

				(rule2str r1)^"' '"^(rule2str r2)^"'");

fun distinct_Thm r = gen_distinct eq_Thm r;

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

    handle _ => false;

(***. context to thy concerning rewriting .***)

(*.create the unique handles and filenames for the theory-data.*)

fun part2filename str = part2guh str ^ ".xml" : filename;

fun thy2filename thy' = thy2guh thy' ^ ".xml" : filename;

fun thypart2filename thy' = thypart2guh thy' ^ ".xml" : filename;

fun thm2filename (isa_thyID: string * thyID) thmID =

    (thm2guh isa_thyID thmID) ^ ".xml" : filename;

fun rls2filename (isa, thyID) rls' =

    rls2guh (isa, thyID) rls' ^ ".xml" : filename;

fun cal2filename (isa, thyID:thyID) calID = 

    cal2guh (isa, thyID:thyID) calID ^ ".xml" : filename;

fun ord2filename (isa, thyID:thyID) (rew_ord':rew_ord') =

    ord2guh (isa, thyID:thyID) (rew_ord':rew_ord') ^ ".xml" : filename;

(**.set up isab_thm_thy in Isac.ML.**)

fun rearrange (thyID, (thmID, thm)) = (thmID, (thyID, Thm.prop_of thm));

(* WN120320: reconsider design since thmID and thyID can be retrieved from thm: *)

fun rearrange' (thmID, thm) =

  (thmID_of_derivation_name thmID,

    (thyID_of_derivation_name thmID, Thm.prop_of thm)): (thmID * (thyID * term));

fun rearrange_inv (thmID, (thyID, term)) = (thyID, (thmID, term));

(*================= version before Isbelle2002 --> 2011 ===========================

(*.lookup the missing theorems in some thy (of Isabelle).*)

fun make_isa missthms thy =

    map (pair (theory2thyID thy)) 

	((inter eq_thmI) missthms [] (*Global_Theory.all_thms_of thy WN11xxxx: THIS IS TOO EXPENSIVE*)) 

	: (thyID * (thmID * Thm.thm)) list;

(*.separate handling of sym_thms.*)

fun make_isab rlsthmsNOTisac isab_thys = 

    let fun les ((s1,_), (s2,_)) = (s1 : string) < s2

	val notsym = filter_out (is_sym o #1) rlsthmsNOTisac

	val notsym_isab = (flat o (map (make_isa notsym))) isab_thys

	val sym = filter (is_sym o #1) rlsthmsNOTisac

	val symsym = map ((apfst sym_drop) o (apsnd sym_thm)) sym

	val symsym_isab = (flat o (map (make_isa symsym))) isab_thys

	val sym_isab = map (((apsnd o apfst) sym_drop) o 

			    ((apsnd o apsnd) sym_thm)) symsym_isab

	val isab = notsym_isab @ symsym_isab @ sym_isab

    in ((map rearrange) o (gen_sort les)) isab : (thmID * (thyID * term)) list

    end;

================= version before Isbelle2002 --> 2011 ===========================*)

(*================= trials while Isbelle2002 --> 2011 ===========================

  WN120320 update Isabelle2002 --> 2011 gave up with expensiveness of Global_Theory.all_thms_of;

  the code below is outcommented too due to problems with sym_*:

  version with term instead of thm, for Theory.axioms_of in isa02

fun make_isa missthms thy =

    map (pair (theory2thyID thy)) 

	((inter eq_thmI') missthms (Theory.axioms_of thy))

	: (thyID * (thmID * term)) list;

(* separate handling of sym_thms *)

fun make_isab rlsthmsNOTisac isab_thys = 

    let fun les ((s1,_), (s2,_)) = (s1 : string) < s2

	val notsym = filter_out (is_sym o #1) rlsthmsNOTisac

	val notsym_isab = (flat o (map (make_isa notsym))) isab_thys

	val sym = filter (is_sym o #1) rlsthmsNOTisac

	val symsym = map ((apfst sym_drop) o (apsnd sym_trm)) sym

	val symsym_isab = (flat o (map (make_isa symsym))) isab_thys

	val sym_isab = map (((apsnd o apfst) sym_drop) o 

			    ((apsnd o apsnd) sym_trm)) symsym_isab

	val isab = notsym_isab @ symsym_isab @ sym_isab

    in ((map rearrange) o (gen_sort les)) isab 

       : (thmID * (thyID * term)) list

    end;

================= trials while Isbelle2002 --> 2011 ===========================*)

(*================= cheap version without sym_* thms ===========================*)

fun make_isab rlsthmsNOTisac = map rearrange' rlsthmsNOTisac;

fun thy_containing_thm thmDeriv =

  let

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

  in

    if member op= isabthys' (thyID_of_derivation_name thmDeriv)

    then ("Isabelle", thyID_of_derivation_name thmDeriv)

    else ("IsacKnowledge", thyID_of_derivation_name thmDeriv)

  end;

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

fun thy_containing_rls (thy' : theory') (rls' : rls') =

  let

    val thy = Thy_Info.get_theory thy'

  in

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

      SOME (thy'', _) => (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' : theory') (sop : prog_calcID) =

  let

    val thy = Thy_Info.get_theory thy'

  in

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

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

    | _ => 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   : thyID,         (*for *2guh in sub-elems here .*)

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

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

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

	  reword  : 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  : rls'           (*ruleset for evaluating asms .*)

		    }						 

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

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

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

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

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

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

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

	  reword  : 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  : rls'           (*ruleset for evaluating asms .*)

		      }						 

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

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

	  rls     : 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   : thyID,         (*for *2guh in sub-elems here .*)

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

	  bdvs    : 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   : thyID,         (*for *2guh in sub-elems here .*)

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

	  applto  : term	   (*rewrite this formula        .*)

		    }						 

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

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

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

	  bdvs    : 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,p_) : pos') = get_obj g_tac pt p;

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

fun deriv_of_thm'' ((thmID, _) : thm'') =

  thmID |> Global_Theory.get_thm (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 Rewrite thm'') =

      let val thm_deriv = deriv_of_thm'' thm''

      in

      (case applicable_in pos pt tac of

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

          ContThm

           {thyID   = theory'2thyID thy',

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

            applto  = f,

            applat  = e_term,

            reword  = ord',

            asms    = [](*asms ~~ asms'*),

            lhs     = (e_term, e_term)(*(lhs, lhs')*),

            rhs     = (e_term, e_term)(*(rhs, rhs')*),

            result  = res,

            resasms = asm,

            asmrls  = id_rls erls}

       | Notappl _ =>

           let

             val pp = par_pblobj pt p

             val thy' = get_obj g_domID pt pp

             val f = case p_ of

                   Frm => get_obj g_form pt p

                 | Res => (fst o (get_obj g_result pt)) p | _ => error "context_thy 1"

           in

             ContNOrew

              {thyID   = theory'2thyID thy',

               thm_rls = 

                 thm2guh (thy_containing_thm thm_deriv) (thmID_of_derivation_name thm_deriv),

               applto  = f}

		       end

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

      end

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

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

      in

	    (case applicable_in pos pt tac of

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

	         let

             val thm_deriv = Thm.get_name_hint thm

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

	         in

	           ContThmInst

	            {thyID   = theory'2thyID thy',

	             thm     = 

	               thm2guh (thy_containing_thm thm_deriv) (thmID_of_derivation_name thm_deriv),

	             bdvs    = subst,

	             thminst = thminst,

	             applto  = f,

	             applat  = e_term,

	             reword  = ord',

	             asms    = [](*asms ~~ asms'*),

	             lhs     = (e_term, e_term)(*(lhs, lhs')*),

	             rhs     = (e_term, e_term)(*(rhs, rhs')*),

	             result  = res,

	             resasms = asm,

	             asmrls  = id_rls erls}

	         end

       | Notappl _ =>

           let

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

             val thm_deriv = Thm.get_name_hint thm

             val pp = par_pblobj pt p

             val thy' = get_obj g_domID pt pp

             val subst = subs2subst (assoc_thy thy') subs

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

             val f = case p_ of

                 Frm => get_obj g_form pt p

               | Res => (fst o (get_obj g_result pt)) p | _ => error "context_thy 2"

           in

             ContNOrewInst

              {thyID   = theory'2thyID thy',

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

               bdvs    = subst,

               thminst = thminst,

               applto  = f}

           end

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

      end

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

      (case applicable_in p pt tac of

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

           ContRls

            {thyID  = theory'2thyID thy',

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

             applto = f,	  

             result = res,	  

             asms   = asm}

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

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

      (case applicable_in p pt tac of

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

           ContRlsInst

            {thyID  = theory'2thyID thy',

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

             bdvs   = subst,

             applto = f,	  

             result = res,	  

             asms   = asm}

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

  | context_thy (_,p) tac =

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

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

fun thm_of_rule Erule = []

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

  | thm_of_rule (Calc _) = []

  | thm_of_rule (Cal1 _) = []

  | thm_of_rule (Rls_ rls) = thms_of_rls rls

and thms_of_rls Erls = []

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

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

  | thms_of_rls (Rrls _) = [];

(* val Hrls {thy_rls = (_, rls),...} =

       get_the ["IsacKnowledge", "Test", "Rulesets", "expand_binomtest"];

> thms_of_rls rls;

   *)

(*. 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 (r, Rls_ rls) = finds (get_rules rls)

	  | find r12 = eq_rule r12

	and finds [] = false

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

    in 

    (*tracing ("### contains_rule: r = "^rule2str r^", rls = "^rls2str rls);*)

    finds (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):rew_ord) erls (subst:subst) f (thm' as Thm(id, thm)) =

    if contains_bdv thm

    then case rewrite_inst_ thy ro erls false subst thm f of

	      SOME (f',_) =>[rule2tac thy subst thm']

	    | NONE => []

    else (case rewrite_ thy ro erls false thm f of

	      SOME (f',_) => [rule2tac thy [] thm']

	    | NONE => [])

  | try_rew thy _ _ _ f (cal as Calc c) = 

    (case get_calculation_ thy c f of

	      SOME (str, _) => [rule2tac thy [] cal]

      | NONE => [])

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

    (case get_calculation_ thy c f of

	      SOME (str, _) => [rule2tac thy [] cal]

      | NONE => [])

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

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

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

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

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

  | filter_appl_rews thy subst f (Rrls _) = [];

(*. 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 (Calculate scrID) =

    try_rew thy e_rew_ordX e_rls [] f (Calc (assoc_calc' thy scrID |> snd))

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

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

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

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

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

    filter_appl_rews thy [] f (assoc_rls rls')

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

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

  | atomic_appl_tacs _ _ _ _ tac = 

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

     []);

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

fun theID2filename (theID:theID) = theID2guh theID ^ ".xml" : filename;

fun guh2theID (guh: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 error ("guh '"^guh^"' does not begin with \

				     \exp_ | thy_ | pbl_ | met_")

       else let val chap = case isa of

				"isab_" => "Isabelle"

			      | "scri_" => "IsacScripts"

			      | "isac_" => "IsacKnowledge"

			      | _ => 

				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] : 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"

			     | str => 

			       error ("guh2theID: '"^guh^"' has '"^sect^

					    "' instead -thm- | -rls- | \

					    \-cal- | -ord-")

		   in [chap, implode thyID, sect', implode 

						       (takerest (5, rest'))]

		   end

	    end	

    end;

(*> guh2theID "thy_isac_Biegelinie-Theorems";

val it = ["IsacKnowledge", "Biegelinie", "Theorems"] : theID

> guh2theID "thy_scri_ListC-thm-zip_Nil";

val it = ["IsacScripts", "ListC", "Theorems", "zip_Nil"] : theID*)

fun guh2filename (guh : guh) = guh ^ ".xml" : filename;

(*..*)

fun guh2rewtac (guh:guh) ([] : subs) =

    let val [isa, thy, sect, xstr] = guh2theID guh

    in case sect of

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

	 | "Rulesets" => Rewrite_Set xstr

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

    end

  | guh2rewtac (guh:guh) subs =

    let val [isa, thy, sect, xstr] = guh2theID guh

    in case sect of

        "Theorems" => 

          Rewrite_Inst (subs, (xstr, assoc_thm'' (assoc_thy thy) xstr))

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

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

    end;

(*> guh2rewtac "thy_isac_Test-thm-constant_mult_square" [];

val it = Rewrite ("constant_mult_square", "") : tac

> guh2rewtac "thy_isac_Test-thm-risolate_bdv_add" ["(bdv, x)"];

val it = Rewrite_Inst (["(bdv, x)"], ("risolate_bdv_add", "")) : tac

> guh2rewtac "thy_isac_Test-rls-Test_simplify" [];

val it = Rewrite_Set "Test_simplify" : tac

> guh2rewtac "thy_isac_Test-rls-isolate_bdv" ["(bdv, x)"];

val it = Rewrite_Set_Inst (["(bdv, x)"], "isolate_bdv") : tac*)

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

(* val guh = "thy_isac_Test-rls-Test_simplify";

   *)

fun no_thycontext (guh : guh) = (guh2theID guh; false)

    handle _ => true;

(*> has_thycontext  "thy_isac_Test";

if has_thycontext  "thy_isac_Test" then "OK" else "NOTOK";

 *)

(*.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*)

(* val (ScrState (env,_,_,_,_,_), _, guh) = (is, "dummy", guh);

   *)

fun subs_from (ScrState (env,_,_,_,_,_)) _ (guh:guh) =

    let val theID as [isa, thyID, sect, xstr] = guh2theID guh

    in case sect of

	   "Theorems" => 

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

	   in if contains_bdv thm

	      then let val formal_arg = str2term "v_"

		       val value = subst_atomic env formal_arg

		   in ["(bdv," ^ term2str value ^ ")"]:subs end

	      else []

	   end

	 | "Rulesets" => 

	   let val rules = (get_rules o assoc_rls) xstr

	   in if contain_bdv rules

	      then let val formal_arg = str2term"v_"

		       val value = subst_atomic env formal_arg

		   in ["(bdv,"^term2str value^")"]:subs end

	      else []

	   end

    end;

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

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

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", _) $ Free (str, _) $ _) $ _) =

           if 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: subs option, []: subst)

    | SOME tm =>

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

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

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

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

        in (SOME (subst2subs subst), subst) end

          (*"SOME [(bdv,v_v)]": term --> ["(bdv,v_v)"]: string list*)

  end;

(* use"ME/rewtools.sml";

   *)