(* 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}) = 

 	    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 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, 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, 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", thmID_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;

 (*..*)

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

 (* val (Rewrite' (thy', ord', erls, _, (thmID,_), f, (res,asm))) = tac';

    *)

 fun context_thy (pt, pos as (p,p_)) (tac as Rewrite (thmID,_)) =

       (case applicable_in pos pt tac of

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

           let 

             val thmDeriv = "WN120320: AT Isa2009-2-->11 BROKEN"

             val thy = assoc_thy thy'

             val thm = (norm o #prop o rep_thm o (Global_Theory.get_thm thy)) thmID

           in

             ContThm

              {thyID   = theory'2thyID thy',

               thm     =

                 thm2guh (thy_containing_thm thmDeriv) (thmID_of_derivation_name thmDeriv),

               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 thmDeriv = "WN120320: AT Isa2009-2-->11 BROKEN"

              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

            in

              ContNOrew

               {thyID   = theory'2thyID thy',

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

                applto  = f}

 		       end)

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

 	    (case applicable_in pos pt tac of

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

 	         let

              val thmDeriv = "WN120320: get this from a reference variable ?!?"

 	           val thm = (norm o #prop o rep_thm o (Global_Theory.get_thm (assoc_thy thy'))) thmID

 	           val thminst = inst_bdv subst thm

 	         in

 	           ContThmInst

 	            {thyID   = theory'2thyID thy',

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

 	             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 thmDeriv = "WN120320: get this from a reference variable ?!?"

              val pp = par_pblobj pt p

              val thy' = get_obj g_domID pt pp

              val subst = subs2subst (assoc_thy thy') subs

              val thm = (norm o #prop o rep_thm o (Global_Theory.get_thm (assoc_thy thy'))) thmID

              val thminst = inst_bdv subst thm

              val f = case p_ of

                  Frm => get_obj g_form pt p

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

            in

              ContNOrewInst

               {thyID   = theory'2thyID thy',

                thm_rls =

                  "WN120320: thm2guh (thy_containing_thm thmDeriv) (thmID_of_derivation_name thmDeriv)",

                bdvs    = subst,

                thminst = thminst,

                applto  = f}

            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    = "WN120320:  rls2guh (thy_containing_rls thy' rls') rls'",

              applto = f,	  

              result = res,	  

              asms   = asm})

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

       (case applicable_in p pt tac of

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

            ContRlsInst

             {thyID  = theory'2thyID thy',

              rls    = "WN120320: rls2guh (thy_containing_rls thy' rls') rls'",

              bdvs   = subst,

              applto = f,	  

              result = res,	  

              asms   = asm});

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

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

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

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

 (* val 

    *)

 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' as (thmID, _))) =

     try_rew thy (ro, assoc_rew_ord ro) erls [] f 

 	    (Thm (thmID, assoc_thm' thy thm'))

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

     try_rew thy (ro, assoc_rew_ord ro) erls (subs2subst thy subs) f 

 	    (Thm (thmID, assoc_thm' thy 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, "")

 	 | "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, ""))

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

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

     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";

    *)